proofs/lib/lemmas/proofs/map_insert_critbit.bend checks

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

11 imports

import Base
import ./string_compare.bend as N
import ./invariants.bend as Inv
import ./map_insert.bend as I
import ./map_difference.bend as D
import ./map_splice_critbit.bend as Splice
import ./map_insert_before.bend as Before
import ./map_insert_descent.bend as Descent
import ./map_seek_discriminator.bend as Discriminator
import ./map_critbit_parts.bend as Parts
import ./map_routing.bend as R

Laws

law order_lift provedsource · line 17 · raw

@+a:Nat -> @+b:Nat -> @order:Order(a, b) -> Order(1n+a, 1n+b)

law total_order provedsource · line 28 · raw

@a:Nat -> @b:Nat -> Order(a, b)

law equal_impossible provedsource · line 39 · raw

@-V:Data -> @+lo:Map<&2, V> -> @+hi:Map<&2, V> -> @+position:Nat -> @+key:String -> @+stored:String -> @distinct:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_difference.different(key, stored) -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, MNode{position, lo, hi}, key)) == Some{stored} : Maybe<&2, String>} -> @equal:{Map.diff(key, stored) == position : Nat} -> @parts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_critbit_parts.NodeFacts(V, position, lo, hi) -> Empty

law node_case provedsource · line 55 · raw

@-V:Data -> @+lo:Map<&2, V> -> @+hi:Map<&2, V> -> @+position:Nat -> @+key:String -> @+stored:String -> @+value:V -> @order:Order(Map.diff(key, stored), position) -> @distinct:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_difference.different(key, stored) -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, MNode{position, lo, hi}, key)) == Some{stored} : Maybe<&2, String>} -> @valid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, MNode{position, lo, hi}) == True{} : Bool} -> @lp:(@_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, lo) == True{} : Bool} -> @_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, lo, key)) == Some{stored} : Maybe<&2, String>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.ins(&2, V, lo, key, value, Map.diff(key, stored))) == True{} : Bool}) -> @hp:(@_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, hi) == True{} : Bool} -> @_:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, hi, key)) == Some{stored} : Maybe<&2, String>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.ins(&2, V, hi, key, value, Map.diff(key, stored))) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.ins(&2, V, MNode{position, lo, hi}, key, value, Map.diff(key, stored))) == True{} : Bool}

law leaf provedsource · line 79 · raw

@-V:Data -> @+key:String -> @+stored:String -> @+actual:String -> @value:V -> @old:V -> @distinct:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_difference.different(key, stored) -> @found:{Some{actual} == Some{stored} : Maybe<&2, String>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.ins(&2, V, MLeaf{actual, old}, key, value, Map.diff(key, stored))) == True{} : Bool}

law unequal_distinct provedsource · line 94 · raw

@+key:String -> @+stored:String -> @unequal:{String.eq(key, stored) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_difference.different(key, stored)

law insertion_at_seek provedsource · line 104 · raw

@-V:Data -> @tree:Map<&2, V> -> @+key:String -> @+stored:String -> @+value:V -> @+unequal:{String.eq(key, stored) == False{} : Bool} -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, tree, key)) == Some{stored} : Maybe<&2, String>} -> @valid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, tree) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(V, Map.ins(&2, V, tree, key, value, Map.diff(key, stored))) == True{} : Bool}

Full insertion critbit preservation at the leaf selected by actual seek. The public Map.set bridge must additionally handle replacement and empty seek.

Definitions

def Order source · line 14 · raw

@+a:Nat -> @+b:Nat -> Type

Constructive total ordering; neither an order oracle nor a public premise.