proofs/lib/lemmas/proofs/map_shape.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_shape.bend as Map_shape

4 imports

import Base
import ./map_bridge.bend as MB
import ./map_insert.bend as I
import ./string_compare.bend as N

Laws

law lift_left provedsource · line 26 · raw

@-V:Data -> @+lo:Map<&2, V> -> @+hi:Map<&2, V> -> @+p:Nat -> @+key:String -> @+x:V -> @found:Maybe<&2, String> -> @e:{Map.bit(key, p) == (key, False{}) : Pair(String, Bool)} -> @cp:certificate(V, lo, key, x, found) -> certificate(V, MNode{p, lo, hi}, key, x, found)

law lift_right provedsource · line 46 · raw

@-V:Data -> @+lo:Map<&2, V> -> @+hi:Map<&2, V> -> @+p:Nat -> @+key:String -> @+x:V -> @found:Maybe<&2, String> -> @e:{Map.bit(key, p) == (key, True{}) : Pair(String, Bool)} -> @cp:certificate(V, hi, key, x, found) -> certificate(V, MNode{p, lo, hi}, key, x, found)

law branch provedsource · line 66 · raw

@-V:Data -> @+lo:Map<&2, V> -> @+hi:Map<&2, V> -> @+p:Nat -> @+key:String -> @x:V -> @bit:Bool -> @+e:{Map.bit(key, p) == (key, bit) : Pair(String, Bool)} -> @lp:certificate(V, lo, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, lo, key))) -> @hp:certificate(V, hi, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, hi, key))) -> certificate(V, MNode{p, lo, hi}, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)))

law replacement_shape provedsource · line 87 · raw

@-V:Data -> @m:Map<&2, V> -> @+key:String -> @+x:V -> certificate(V, m, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, m, key)))

law put_found_shape provedsource · line 104 · raw

@-V:Data -> @+m:Map<&2, V> -> @+key:String -> @+x:V -> @stored:String -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, m, key)) == Some{stored} : Maybe<&2, String>} -> {skeleton(V, Map.put(&2, V, m, key, x)) == skeleton(V, m) : Map<&2, Unit>}

Unlike the helper certificate, this conclusion is a concrete structural equality. The premise is actual seek's result, not an assumed Map.set law.

law keys_skeleton_go provedsource · line 116 · raw

@-V:Data -> @m:Map<&2, V> -> @+acc:List<&2, String> -> {Map.keys.go(&2, Unit, skeleton(V, m), acc) == Map.keys.go(&2, V, m, acc) : List<&2, String>}

law set_found_replaces provedsource · line 130 · raw

@-V:Data -> @+m:Map<&2, V> -> @+key:String -> @+x:V -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, m, key)) == Some{key} : Maybe<&2, String>} -> {Map.set(&2, V, m, key, x) == Map.put(&2, V, m, key, x) : Map<&2, V>}

law set_existing_shape provedsource · line 143 · raw

@-V:Data -> @+m:Map<&2, V> -> @+key:String -> @+x:V -> @+found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, m, key)) == Some{key} : Maybe<&2, String>} -> {skeleton(V, Map.set(&2, V, m, key, x)) == skeleton(V, m) : Map<&2, Unit>}

law set_existing_keys provedsource · line 153 · raw

@-V:Data -> @+m:Map<&2, V> -> @+key:String -> @+x:V -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, m, key)) == Some{key} : Maybe<&2, String>} -> {Map.keys(&2, V, Map.set(&2, V, m, key, x)) == Map.keys(&2, V, m) : List<&2, String>}

Definitions

def skeleton source · line 8 · raw

@-V:Data -> @m:Map<&2, V> -> Map<&2, Unit>

Value erasure records the existing native tree's full discriminators and keys. It is a proof observation, never a lookup or runtime storage representation.

def certificate source · line 19 · raw

@-V:Data -> @m:Map<&2, V> -> @key:String -> @x:V -> @found:Maybe<&2, String> -> Type

The native replacement helper creates a leaf on Tip. Its shape theorem must therefore be restricted to paths on which actual seek has found a leaf.