~/bend-docscommunity

proofs/containers/hash_table/get.bend checks

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

19 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/math/hash.bend as HS
import ../../../src/containers/hash_table.bend as H
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./cyc.bend as CY
import ./inv.bend as IV
import ./probe_impl.bend as PI
import ./probe_all.bend as PA
import ./state.bend as ST
import ./lookup.bend as LK

Definitions

def load_lt_c source · line 24 · raw

@+a:Nat -> @+m:Nat -> @+hm:{Nat.is_lt(0n, m) == True{} : Bool} -> @+h:{Nat.is_le(Nat.double(a), m) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(a, m) == c : Bool} -> {Nat.is_lt(a, m) == True{} : Bool}

at most half full: fewer entries than buckets

def load_lt source · line 34 · raw

@+a:Nat -> @+m:Nat -> @+hm:{Nat.is_lt(0n, m) == True{} : Bool} -> @+h:{Nat.is_le(Nat.double(a), m) == True{} : Bool} -> {Nat.is_lt(a, m) == True{} : Bool}

def res_e0 source · line 37 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, n) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(bs, n, mask) == True{} : Bool} -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHome{bs, mask, key, h}, n) == True{} : Bool} -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.Empty0(bs, n) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.ResOK(bs, n, h, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, bs, n, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, h)), h))

def bf_ok source · line 53 · raw

@+sd:Nat -> @+lv:List<&2, Bool> -> @+fr:Nat -> @+key:String -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.wb(sd, b) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.live_b(lv, fr, b) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, b) == True{} : Bool} -> Pair({Bool.not(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b), 0)) == True{} : Bool}, Pair({Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nthb(lv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b)))) == True{} : Bool}))

a full bucket holding key: its link is not 0, its slot is in the arena, and the slot holds a value

Templates

template res_of source · line 43 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.goodF(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool} -> @+key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.ResOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))))

the probe facts for key in a table satisfying the invariant

template get_end source · line 61 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.goodF(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool} -> @+key:String -> @+dflt:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+sk:String -> @+w:U32 -> @+e:Nat -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get_f(V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), dflt, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_impl.fd_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.REnd{e}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), sk), w)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HM{n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V)}

template get_val source · line 64 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+key:String -> @+dflt:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+l:U32 -> @+lhs:Maybe<&2, V> -> @+mv:Maybe<&2, V> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))) == mv : Maybe<&2, V>} -> @+hlive:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nthb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))) == True{} : Bool} -> @+hlk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))) : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get_fin(V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get_v(V, dflt, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), mv))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HM{n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V)}

template get_hit3 source · line 71 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+key:String -> @+dflt:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+l:U32 -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool} -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hlive:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nthb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))) == True{} : Bool} -> @+hlk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))) : Maybe<&2, V>} -> @+z:Bool -> @+hz:{U32.is_eq(l, 0) == z : Bool} -> @+hzf:{z == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get_hit(V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), dflt, l, z) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HM{n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V)}

template get_hit2 source · line 83 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.goodF(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool} -> @+key:String -> @+dflt:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+sk:String -> @+w:U32 -> @+i:Nat -> @+l:U32 -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)) == l : U32} -> @bf:Pair({Bool.not(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)), 0)) == True{} : Bool}, Pair({Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nthb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i))))) == True{} : Bool})) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get_f(V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), dflt, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_impl.fd_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.RHit{i, l}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), sk), w)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HM{n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V)}

template get_r source · line 92 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.goodF(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool} -> @+key:String -> @+dflt:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+sk:String -> @+w:U32 -> @+h:Nat -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @hres:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.ResOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), h, key, r) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get_f(V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), dflt, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_impl.fd_of(r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), sk), w)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HM{n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, V)}

template GetOK source · line 106 · 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) -> Type

template get_po source · line 109 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool} -> @+dflt:V -> @+key:String -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @hres:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.ResOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), key, r) -> @po:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.ProbeOK(tabT, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.probe(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), key)) -> GetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, dflt, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key))

template get_ok source · line 124 · 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 -> GetOK(V, sh, dflt, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.get(V, dflt, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key))

THEOREM: get is the specification's get; the map and its model are kept.