proofs/lib/lemmas/proofs/map_routing.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Map_routing

4 imports

import Base
import ./map_insert.bend as I
import ./map_lookup.bend as L
import ./invariants.bend as R

Laws

law false_true proved
Also proved in bend-mathlib as bool.false_ne_true: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.false_ne_true`.
source · line 14 · raw

@e:{False{} == True{} : Bool} -> Empty

law and_left proved
Also proved in bend-mathlib as bool.eq_true_of_and_left: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.eq_true_of_and_left`.
source · line 21 · raw

@a:Bool -> @b:Bool -> @e:{Bool.and(a, b) == True{} : Bool} -> {a == True{} : Bool}

law and_right proved
Also proved in bend-mathlib as bool.eq_true_of_and_right: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.eq_true_of_and_right`.
source · line 33 · raw

@a:Bool -> @b:Bool -> @e:{Bool.and(a, b) == True{} : Bool} -> {b == True{} : Bool}

law equal_bit provedsource · line 45 · raw

@bit:Bool -> @side:Bool -> @e:{Bool.not(Bool.xor(bit, side)) == True{} : Bool} -> {bit == side : Bool}

law route_projection provedsource · line 70 · raw

@r:Pair(String, Bool) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/invariants.bit_value(r) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.route_bit(r) : Bool}

law routed_certificate provedsource · line 78 · raw

@-V:Data -> @tree:Map<&2, V> -> @+pos:Nat -> @+side:Bool -> @+e:{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/invariants.routed(V, tree, pos, side) == True{} : Bool} -> routed(V, tree, pos, side)

law member_routed provedsource · line 105 · raw

@-V:Data -> @tree:Map<&2, Maybe<&2, V>> -> @+key:String -> @+value:V -> @+pos:Nat -> @+side:Bool -> @routes:routed(Maybe<&2, V>, tree, pos, side) -> @member:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, tree, key, value) -> {Map.bit(key, pos) == (key, side) : Pair(String, Bool)}

law duplicate_member provedsource · line 140 · raw

@-V:Data -> @tree:Map<&2, Maybe<&2, V>> -> @+key:String -> @+value:V -> @member:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, tree, key, value) -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, tree, key, value), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, tree, key, value))

Structural duplication of a membership witness; no unrestricted Type cast.

law lookup_left provedsource · line 163 · raw

@-V:Data -> @+lo:Map<&2, Maybe<&2, V>> -> @+hi:Map<&2, Maybe<&2, V>> -> @+p:Nat -> @+key:String -> @+value:V -> @routes:routed(Maybe<&2, V>, lo, p, False{}) -> @induction:(@member:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, lo, key, value) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.lookup(Maybe<&2, V>, None{}, lo, key) == Some{value} : Maybe<&2, V>}) -> @copies:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, lo, key, value), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, lo, key, value)) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.lookup(Maybe<&2, V>, None{}, MNode{p, lo, hi}, key) == Some{value} : Maybe<&2, V>}

Converse of native lookup soundness. The routing premise is structural and is separately derived from the actual executable critbit predicate below.

law lookup_right provedsource · line 178 · raw

@-V:Data -> @+lo:Map<&2, Maybe<&2, V>> -> @+hi:Map<&2, Maybe<&2, V>> -> @+p:Nat -> @+key:String -> @+value:V -> @routes:routed(Maybe<&2, V>, hi, p, True{}) -> @induction:(@member:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, hi, key, value) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.lookup(Maybe<&2, V>, None{}, hi, key) == Some{value} : Maybe<&2, V>}) -> @copies:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, hi, key, value), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, hi, key, value)) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.lookup(Maybe<&2, V>, None{}, MNode{p, lo, hi}, key) == Some{value} : Maybe<&2, V>}

law member_lookup provedsource · line 193 · raw

@-V:Data -> @tree:Map<&2, Maybe<&2, V>> -> @+key:String -> @+value:V -> @invariant:valid(Maybe<&2, V>, tree) -> @member:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, tree, key, value) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.lookup(Maybe<&2, V>, None{}, tree, key) == Some{value} : Maybe<&2, V>}

law critbit_certificate provedsource · line 218 · raw

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

law critbit_member_lookup provedsource · line 240 · raw

@-V:Data -> @+tree:Map<&2, Maybe<&2, V>> -> @key:String -> @value:V -> @invariant:{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/invariants.critbit(Maybe<&2, V>, tree) == True{} : Bool} -> @member:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_lookup.leaf(V, tree, key, value) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_insert.lookup(Maybe<&2, V>, None{}, tree, key) == Some{value} : Maybe<&2, V>}

Definitions

def truth source · line 7 · raw

@b:Bool -> Type

Logical forms of the existing executable routing predicates.

def routed source · line 61 · raw

@-V:Data -> @tree:Map<&2, V> -> @pos:Nat -> @side:Bool -> Type

def valid source · line 96 · raw

@-V:Data -> @tree:Map<&2, V> -> Type

This weaker property is precisely the part of critbit needed for lookup. The full discriminator/prefix property remains required for insertion preservation.

def copies_left source · line 131 · raw

@-A:Type -> @-B:Type -> @pair:Pair(A, A) -> Pair(Either<&1, &1, A, B>, Either<&1, &1, A, B>)

def copies_right source · line 135 · raw

@-A:Type -> @-B:Type -> @pair:Pair(B, B) -> Pair(Either<&1, &1, A, B>, Either<&1, &1, A, B>)