~/bend-docscommunity

proofs/containers/hash_table/proof.bend checks

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

20 imports
import Base
import ../../../spec/containers/hash_table.bend as S
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/hash_table.bend as H
import ./state.bend as ST
import ./new.bend as NW
import ./get.bend as G
import ./has.bend as HA
import ./size.bend as SZ
import ./set.bend as ST2
import ./setok.bend as SO
import ./pop.bend as PO
import ./keysw.bend as KW
import ./keys.bend as K
import ./speclem.bend as SL
import ../../lib/logic.bend as L
import ../../lib/array.bend as AR
import ./poplem.bend as PL
import ./table.bend as TB
import ../../lib/u32div.bend as UD

Definitions

def key_refl source · line 79 · raw

@+a:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Equivalent_Keys.key_refl(a)

---- key equivalence ----

def key_sym source · line 82 · raw

@+a:String -> @+b:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Equivalent_Keys.key_sym(a, b)

def key_trans source · line 85 · raw

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

def key_same source · line 89 · raw

@+a:String -> @+b:String -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Equivalent_Keys.key_same(a, b, h)

equivalent keys are the same string

Templates

template new_ok source · line 50 · raw

@-V:Data -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.new(&2, V) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/new.empty(V)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/new.empty(V)) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/new.empty(V)) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>}))

template get_ok source · line 53 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+dflt:V -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/get.GetOK(V, sh, dflt, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key))

template has_ok source · line 56 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/has.HasOK(V, sh, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.has(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key))

template size_ok source · line 59 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.size(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.size(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh)))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, U32)}, {U32.to_nat(Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.size(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh)))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh)) : Nat})

template set_ok source · line 62 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+cap:Nat -> @+hc30:{Nat.is_le(cap, 30n) == True{} : Bool} -> @+hcap:{Nat.is_le(Nat.double(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, sh, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.set(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key, x))

template pop_ok source · line 65 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/pop.PopOK(V, sh, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.pop(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key))

template del_ok source · line 68 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/pop.DelOK(V, sh, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.del(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key))

template keys_ok source · line 71 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keysw.KeysOK(V, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.keys(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh)))

template key_respect source · line 93 · raw

@-A:Data -> @-f:(@_:String -> A) -> @+a:String -> @+b:String -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Equivalent_Keys.key_respect(A, f, a, b, h)

and so every function of a key (the hash included) agrees on them

template mh_c source · line 97 · raw

@-V:Data -> @+j:String -> @+v:V -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+q:String -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, q) == c : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, t, q) : Bool} -> {Bool.or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(j, q), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.is_some(V, 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))) : Bool}

---- facts about the specification ----

template mem_has source · line 107 · raw

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

a key is in the key sequence exactly when the model has it

template keys_len source · line 115 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m) : Nat}

the key sequence is as long as the map

template none_of source · line 123 · raw

@-V:Data -> @+mv:Maybe<&2, V> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.is_some(V, mv) == False{} : Bool} -> {mv == None{} : Maybe<&2, V>}

has is false exactly when the lookup is None

template ssp source · line 130 · raw

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

template size_set source · line 140 · raw

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

set grows the map by one exactly when the key was absent

template srp source · line 143 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+mv:Maybe<&2, V> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, key) == mv : Maybe<&2, V>} -> {Bool.pick(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, m, key), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key)), 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}

template size_remove source · line 153 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> {Bool.pick(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, m, key), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key)), 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}

remove shrinks the map by one exactly when the key was present

template hso_c source · line 156 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+q:String -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x), q) == Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m))) : Bool}

template hro_c source · line 165 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+q:String -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m)) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key), q) == Bool.and(Bool.not(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m))) : Bool}

template model_nodup source · line 175 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh))) == True{} : Bool}

---- the invariant keeps keys unique ----

template keys_post source · line 180 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.KeysPost(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh))

template KeysContract source · line 184 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, List<&2, String>) -> Type

keys returns the key sequence and changes nothing

template kc_from source · line 187 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, List<&2, String>) -> @ko:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keysw.KeysOK(V, sh, r) -> KeysContract(V, sh, r)

template SetContract source · line 192 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+key:String -> @+x:V -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> Type

template set_same source · line 195 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+m2: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} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x), q) : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == Some{x} : Maybe<&2, V>}

template set_other source · line 198 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+m2: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} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x), q) : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, q) : Maybe<&2, V>}

template set_mem source · line 201 · raw

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

template set_post source · line 205 · raw

@-V:Data -> @-m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @-m2:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @-key:String -> @-x:V -> @-hp:Pair(@+q:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x), q) : Maybe<&2, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m, key, x)) : Nat}) -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m2)) == True{} : Bool} -> @hk:(@+hq0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, m, key) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m) : List<&2, String>}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Include.set_post(V, m, m2, key, x, hp, hnd, hk)

template sc_from source · line 212 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+key:String -> @+x:V -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, sh, key, x, r) -> SetContract(V, sh, key, x, r)

template PopContract source · line 219 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+key:String -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, Maybe<&2, V>) -> Type

template DelContract source · line 222 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+key:String -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> Type

template del_absent source · line 225 · raw

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

template del_other source · line 228 · raw

@-V:Data -> @+m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+m2: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} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key), q) : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m, q) : Maybe<&2, V>}

template del_mem source · line 231 · raw

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

template del_post source · line 235 · raw

@-V:Data -> @-m:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @-m2:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @-key:String -> @-hp:Pair(@+q:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key), q) : Maybe<&2, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.remove(V, m, key)) : Nat}) -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m)) == True{} : Bool} -> @+hnd2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, m2)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.DelPost(V, m, m2, key)

template pc_from source · line 243 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, Maybe<&2, V>) -> @po:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/pop.PopOK(V, sh, key, r) -> PopContract(V, sh, key, r)

template dc_from source · line 249 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> @po:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/pop.DelOK(V, sh, key, r) -> DelContract(V, sh, key, r)

template gv_of source · line 256 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+dflt:V -> @+key:String -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V) -> @ok:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/get.GetOK(V, sh, dflt, key, r) -> {Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), key) : V}

---- reads (SPARK's Element, Contains, Length, Empty_Map) ----

template element_value source · line 263 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+dflt:V -> @+key:String -> @+x:V -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), key) == Some{x} : Maybe<&2, V>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Element.element_value(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), key, x, hl, Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key)))

Element (Container, Key) = Element (Model, Key) when the key is present

template element_default source · line 269 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+dflt:V -> @+key:String -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), key) == None{} : Maybe<&2, V>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Element.element_default(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), key, dflt, hl, Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key)))

a missing key reads as the default (SPARK's Element has Pre => Contains)

template hv_of source · line 274 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+key:String -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, Bool) -> @ok:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/has.HasOK(V, sh, key, r) -> {Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, Bool, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), key) : Bool}

template contains_value source · line 281 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Contains.contains_value(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), key, Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.has(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key)))

Contains (Container, Key) = Has_Key (Model, Key)

template length_value source · line 285 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Length.length_value(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh), U32.to_nat(Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.size(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh)))))

Length (Container) = Length (Model), and Length = the number of keys

template length_frame source · line 289 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Length.length_frame(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.size(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh))))

Length does not change the map

template new_model source · line 293 · raw

@-V:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Empty_Map.new_model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/new.empty(V)))

Empty_Map: Length = 0 and no key is present

template new_length source · line 296 · raw

@-V:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Empty_Map.new_length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/new.empty(V)))

template new_absent source · line 300 · raw

@-V:Data -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Empty_Map.new_absent(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/new.empty(V)), key)

template set_contract source · line 306 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+cap:Nat -> @+hc30:{Nat.is_le(cap, 30n) == True{} : Bool} -> @+hcap:{Nat.is_le(Nat.double(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> SetContract(V, sh, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.set(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key, x))

template pop_contract source · line 309 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> PopContract(V, sh, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.pop(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key))

template del_contract source · line 312 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+key:String -> DelContract(V, sh, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.del(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key))

template keys_contract source · line 315 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> KeysContract(V, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.keys(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh)))