~/bend-docscommunity

proofs/containers/hash_table/speclem.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/speclem.bend as Speclem

4 imports
import Base
import ../../lib/logic.bend as L
import ../../../spec/containers/hash_table.bend as S
import ./keys.bend as K

Definitions

def eq_tr source · line 23 · raw

@+a:String -> @+b:String -> @+c:String -> @+hab:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b) == True{} : Bool} -> @+e:Bool -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(b, c) == e : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, c) == e : Bool}

two keys equal to the same key are equal to each other, by str_eq

def eq_tr2 source · line 27 · raw

@+j:String -> @+key:String -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, q) : Bool}

comparing with keys equal by str_eq agrees

def or_false_l source · line 80 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.or(a, b) == False{} : Bool} -> {a == False{} : Bool}

def or_false_r source · line 87 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.or(a, b) == False{} : Bool} -> {b == False{} : Bool}

Templates

template pick_t source · line 8 · raw

@-A:Data -> @+c:Bool -> @+h:{c == True{} : Bool} -> @+x:A -> @+y:A -> {Bool.pick(A, c, x, y) == x : A}

template pick_f source · line 15 · raw

@-A:Data -> @+c:Bool -> @+h:{c == False{} : Bool} -> @+x:A -> @+y:A -> {Bool.pick(A, c, x, y) == y : A}

template ls_same_c source · line 32 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, key) == c : Bool} -> @rec:(@hc2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, key) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x), q) == Some{x} : Maybe<&2, V>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{key, x} <> t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x)), q) == Some{x} : Maybe<&2, V>}

template lookup_set_same source · line 42 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x), q) == Some{x} : Maybe<&2, V>}

looking up the key just set (or any key equal to it)

template ls_other_c source · line 49 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == False{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, key) == c : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, q) : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{key, x} <> t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x)), q) == Bool.pick(Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, q), Some{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, q)) : Maybe<&2, V>}

template lookup_set_other source · line 58 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, q) : Maybe<&2, V>}

setting key leaves every other key's lookup

template lr_other_c source · line 65 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == False{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, key) == c : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, q) : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key)), q) == Bool.pick(Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, q), Some{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, q)) : Maybe<&2, V>}

template lookup_remove_other source · line 73 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, q) : Maybe<&2, V>}

removing key leaves every other key's lookup

template lookup_not_mem source · line 95 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+q:String -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, q) == None{} : Maybe<&2, V>}

a key not among the keys has no value

template lr_same_c source · line 102 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == True{} : Bool} -> @+hnm:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, t))) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, key) == c : Bool} -> @rec:(@hc2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, key) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key), q) == None{} : Maybe<&2, V>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key)), q) == None{} : Maybe<&2, V>}

template lookup_remove_same source · line 112 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+q:String -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key), q) == None{} : Maybe<&2, V>}

with keys unique, a removed key has no value

template none_pick source · line 121 · raw

@-V:Data -> @+c:Bool -> @+v:V -> @+r:Maybe<&2, V> -> @+h:{Bool.pick(Maybe<&2, V>, c, Some{v}, r) == None{} : Maybe<&2, V>} -> Pair({c == False{} : Bool}, {r == None{} : Maybe<&2, V>})

template ssn_c source · line 128 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+c:Bool -> @+hc:{c == False{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, t) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{key, x} <> t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x))) == 2n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, t) : Nat}

template size_set_new source · line 136 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, key) == None{} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m) : Nat}

setting an absent key adds one entry

template sso_c source · line 145 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+v0:V -> @+c:Bool -> @+h:{Bool.pick(Maybe<&2, V>, c, Some{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, key)) == Some{v0} : Maybe<&2, V>} -> @rec:(@h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, key) == Some{v0} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, t) : Nat}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{key, x} <> t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, t, key, x))) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, t) : Nat}

template size_set_old source · line 153 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+v0:V -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, key) == Some{v0} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m) : Nat}

setting a present key keeps the size

template sro_c source · line 160 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+v0:V -> @+c:Bool -> @+h:{Bool.pick(Maybe<&2, V>, c, Some{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, key)) == Some{v0} : Maybe<&2, V>} -> @rec:(@h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, t, key) == Some{v0} : Maybe<&2, V>} -> {1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, t) : Nat}) -> {1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key))) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, t) : Nat}

template size_remove_old source · line 168 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+v0:V -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, key) == Some{v0} : Maybe<&2, V>} -> {1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m) : Nat}

removing a present key drops one entry

template rn_c source · line 175 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+c:Bool -> @+hc:{c == False{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key) == t : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>} -> {Bool.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>, c, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, t, key)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.E{j, v} <> t : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>}

template remove_none source · line 183 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, key) == None{} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key) == m : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>}

removing an absent key changes nothing