~/bend-docscommunity

proofs/lib/lemmas/proofs/map_delete_critbit.bend checks

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

9 imports
import Base
import ./map_bridge.bend as MB
import ./invariants.bend as Inv
import ./string_compare.bend as N
import ./map_insert.bend as I
import ./map_critbit_parts.bend as Parts
import ./map_delete_below.bend as Below
import ./map_delete_common.bend as Common
import ./map_route_boolean.bend as Routes

Laws

law low provedsource · line 11 · raw

@-V:Data -> @+p:Nat -> @+hi:Map<&2, V> -> @r:Pair(Map<&2, V>, Maybe<&2, V>) -> @prefix:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r)), Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r)), p) == True{} : Bool} -> @other_nonempty:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.nonempty(V, hi) == True{} : Bool} -> @lb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.below(V, Map.del.fin(&2, V, r), p) == True{} : Bool} -> @hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.below(V, hi, p) == True{} : Bool} -> @lr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.routed(V, Map.del.fin(&2, V, r), p, False{}) == True{} : Bool} -> @hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.routed(V, hi, p, True{}) == True{} : Bool} -> @lv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del.fin(&2, V, r)) == True{} : Bool} -> @hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, hi) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r))) == True{} : Bool}

law high provedsource · line 35 · raw

@-V:Data -> @+p:Nat -> @+lo:Map<&2, V> -> @r:Pair(Map<&2, V>, Maybe<&2, V>) -> @prefix:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r)), Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r)), p) == True{} : Bool} -> @other_nonempty:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.nonempty(V, lo) == True{} : Bool} -> @lb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.below(V, lo, p) == True{} : Bool} -> @hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.below(V, Map.del.fin(&2, V, r), p) == True{} : Bool} -> @lr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.routed(V, lo, p, False{}) == True{} : Bool} -> @hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.routed(V, Map.del.fin(&2, V, r), p, True{}) == True{} : Bool} -> @lv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, lo) == True{} : Bool} -> @hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del.fin(&2, V, r)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r))) == True{} : Bool}

law leaf provedsource · line 59 · raw

@-V:Data -> @value:V -> @key:String -> @stored:String -> @tag:Cmp -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, ((key, stored), tag)))) == True{} : Bool}

law branch provedsource · line 72 · raw

@-V:Data -> @+p:Nat -> @+lo:Map<&2, V> -> @+hi:Map<&2, V> -> @+key:String -> @bit:Bool -> @+route:{Map.bit(key, p) == (key, bit) : Pair(String, Bool)} -> @parts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_critbit_parts.NodeFacts(V, p, lo, hi) -> @lp:(@_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, lo) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del(&2, V, lo, key)) == True{} : Bool}) -> @hp:(@_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, hi) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del(&2, V, hi, key)) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del(&2, V, MNode{p, lo, hi}, key)) == True{} : Bool}

law preserves_critbit provedsource · line 113 · raw

@-V:Data -> @tree:Map<&2, V> -> @+key:String -> @valid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, tree) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.del(&2, V, tree, key)) == True{} : Bool}

Full executable critbit preservation: prefix, ordering, routing, nonempty children and recursive validity, not only the weaker lookup-routing predicate.