proofs/containers/hash_table/get.bend
bend-collections-laws-containers@1.0.0.0 · 132 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as HS
10import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as IV
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_impl.bend as PI
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_all.bend as PA
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as ST
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/lookup.bend as LK
20
21# get: the implementation's get is the specification's get.
22
23# at most half full: fewer entries than buckets
24def load_lt_c(+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}:
25 match c:
26 case True{}:
27 hc
28 case False{}:
29 +h1 = N.double_le(m, a, N.not_lt_le(a, m, hc))
30 +h2 = N.le_trans(Nat.double(m), Nat.double(a), m, h1, h)
31 +h3 = L.subst(Nat, z => {Nat.is_le(z, m) == True{} : Bool}, Nat.double(m), Nat.add(m, m), NA.double_self(m), h2)
32 Empty.absurd({Nat.is_lt(a, m) == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(Nat.add(m, m), m), False{}, Equal.sym(Bool, Nat.is_le(Nat.add(m, m), m), True{}, h3), N.lt_not_le(m, Nat.add(m, m), L.subst(Nat, z => {Nat.is_lt(z, Nat.add(m, m)) == True{} : Bool}, Nat.add(0n, m), m, {==}, N.lt_add_r2(0n, m, m, hm))))))
33
34def load_lt(+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}:
35 load_lt_c(a, m, hm, h, Nat.is_lt(a, m), {==})
36
37def res_e0(+bs: List<&2, B.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: {B.cluster(bs, n, mask) == True{} : Bool}, +ho: {B.all_lt(B.PHome{bs, mask, key, h}, n) == True{} : Bool}, e: IV.Empty0(bs, n)) -> B.ResOK(bs, n, h, key, B.pf(key, bs, n, n, B.mstep(key, B.at(bs, h)), h)):
38 match e:
39 case Tuple{+e0, Tuple{+he0, +hz0}}:
40 IV.pf_ok_n(bs, n, hn, mask, key, h, hh, cl, ho, e0, he0, hz0)
41
42# the probe facts for key in a table satisfying the invariant
43def res_of(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +key: String) -> B.ResOK(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, B.pf(key, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), UD.v(HS.bucket(K.kword(key), CY.msk(k))))), UD.v(HS.bucket(K.kword(key), CY.msk(k))))):
44 +bs = TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k))
45 +nb = SC.pow2(k)
46 +hn = N.succ_le_lt(0n, nb, N.pow2_pos(k))
47 +cn = N.eq_from_is_eq(UD.v(n), IV.occn(bs, nb), ST.g_cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg))
48 +hocc = L.subst(Nat, z => {Nat.is_lt(z, nb) == True{} : Bool}, UD.v(n), IV.occn(bs, nb), cn, load_lt(UD.v(n), nb, hn, ST.g_cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg)))
49 res_e0(bs, nb, hn, CY.msk(k), key, UD.v(HS.bucket(K.kword(key), CY.msk(k))), PA.home_lt(K.kword(key), k), ST.g_cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), IV.home_all(bs, sd, CY.msk(k), key, nb, ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), nb, N.le_refl(nb)), IV.find_empty(bs, nb, hocc))
50
51# a full bucket holding key: its link is not 0, its slot is in the arena, and
52# the slot holds a value
53def bf_ok(+sd: Nat, +lv: List<&2, Bool>, +fr: Nat, +key: String, +b: B.Bk, +hw: {B.wb(sd, b) == True{} : Bool}, +hl: {B.live_b(lv, fr, b) == True{} : Bool}, +hk: {B.hold(key, b) == True{} : Bool}) -> {Bool.not(U32.is_eq(B.lnk(b), 0)) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(B.lnk(b))), SC.pow2(sd)) == True{} : Bool} & {B.nthb(lv, UD.v(H.slot(B.lnk(b)))) == True{} : Bool}):
54 match b:
55 case B.BE{}:
56 Empty.absurd({Bool.not(U32.is_eq(B.lnk(B.BE{}), 0)) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(B.lnk(B.BE{}))), SC.pow2(sd)) == True{} : Bool} & {B.nthb(lv, UD.v(H.slot(B.lnk(B.BE{})))) == True{} : Bool}), L.false_true(hk))
57 case B.BF{+x, +l, +k}:
58 +hw2 = L.and_right(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(x, K.kword(k)), Bool.not(U32.is_eq(l, 0))), hw)
59 (L.and_right(U32.is_eq(x, K.kword(k)), Bool.not(U32.is_eq(l, 0)), hw2), (L.and_left(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(x, K.kword(k)), Bool.not(U32.is_eq(l, 0))), hw), L.and_left(B.nthb(lv, UD.v(H.slot(l))), Nat.is_lt(UD.v(H.slot(l)), fr), hl)))
60
61def get_end(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +key: String, +dflt: V, +K2: AR.Tree<String>, +sk: String, +w: U32, +e: Nat, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> {H.get_f(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, (PI.fd_of(B.REnd{e}, AR.thaw(U32, tabT), AR.thaw(String, K2), sk), w)) == (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & V}:
62 Equal.cong(Maybe<&2, V>, H.HashMap<&2, V> & V, z => (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get_m(~V, dflt, z)), None{}, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), None{}, LK.lookup_none(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), key, SC.pow2(k), hno)))
63
64def get_val(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +key: String, +dflt: V, +K2: AR.Tree<String>, +l: U32, +lhs: Maybe<&2, V>, +mv: Maybe<&2, V>, +hmv: {ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))) == mv : Maybe<&2, V>}, +hlive: {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool}, +hlk: {S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key) == ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))) : Maybe<&2, V>}) -> {H.get_fin(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), H.get_v(V, dflt, (AR.thaw(Maybe<&2, V>, vsT), mv))) == (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & V}:
65 match mv:
66 case None{}:
67 Empty.absurd({H.get_fin(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), H.get_v(V, dflt, (AR.thaw(Maybe<&2, V>, vsT), None{}))) == (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & V}, L.true_false(Equal.trans(Bool, True{}, B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))), False{}, Equal.sym(Bool, B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))), True{}, hlive), Equal.trans(Bool, B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))), ST.some_b(~V, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), False{}, ST.lvs_nth(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), Equal.cong(Maybe<&2, V>, Bool, z => ST.some_b(~V, z), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), None{}, hmv)))))
68 case Some{+v}:
69 Equal.cong(Maybe<&2, V>, H.HashMap<&2, V> & V, z => (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get_m(~V, dflt, z)), Some{v}, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), Some{v}, Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), Some{v}, hlk, hmv)))
70
71def get_hit3(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +key: String, +dflt: V, +K2: AR.Tree<String>, +l: U32, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +hr: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +hlive: {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool}, +hlk: {S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key) == ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))) : Maybe<&2, V>}, +z: Bool, +hz: {U32.is_eq(l, 0) == z : Bool}, +hzf: {z == False{} : Bool}) -> {H.get_hit(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, l, z) == (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & V}:
72 match z:
73 case True{}:
74 Empty.absurd({H.get_hit(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, l, True{}) == (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & V}, L.true_false(hzf))
75 case False{}:
76 +mv = ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))
77 +hlen = L.subst(Nat, zz => {Nat.is_lt(UD.v(H.slot(l)), zz) == True{} : Bool}, SC.pow2(sd), SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT)), Equal.sym(Nat, SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT)), SC.pow2(sd), AR.slots_length(Maybe<&2, V>, sd, vsT, pv)), hr)
78 +ga = AR.get(Maybe<&2, V>, sd, vsT, H.slot(l), mv, hsd, hr, ST.nthm_some(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), hlen), pv)
79 Equal.trans(H.HashMap<&2, V> & V, H.get_fin(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), H.get_v(V, dflt, Array.get(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l)))), H.get_fin(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), H.get_v(V, dflt, (AR.thaw(Maybe<&2, V>, vsT), mv))), (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)),
80 Equal.cong(Array<Maybe<&2, V>> & Maybe<&2, V>, H.HashMap<&2, V> & V, rr => H.get_fin(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), H.get_v(V, dflt, rr)), Array.get(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l)), (AR.thaw(Maybe<&2, V>, vsT), mv), ga),
81 get_val(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, key, dflt, K2, l, mv, mv, {==}, hlive, hlk))
82
83def get_hit2(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +key: String, +dflt: V, +K2: AR.Tree<String>, +sk: String, +w: U32, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)) == l : U32}, bf: {Bool.not(U32.is_eq(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)), 0)) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)))), SC.pow2(sd)) == True{} : Bool} & {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i))))) == True{} : Bool})) -> {H.get_f(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, (PI.fd_of(B.RHit{i, l}, AR.thaw(U32, tabT), AR.thaw(String, K2), sk), w)) == (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & V}:
84 match bf:
85 case Tuple{nz, Tuple{hr0, hlv0}}:
86 +nz2 = L.subst(U32, zz => {Bool.not(U32.is_eq(zz, 0)) == True{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)), l, hl, nz)
87 +hr = L.subst(U32, zz => {Nat.is_lt(UD.v(H.slot(zz)), SC.pow2(sd)) == True{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)), l, hl, hr0)
88 +hlv = L.subst(U32, zz => {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(zz))) == True{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)), l, hl, hlv0)
89 +hlk = L.subst(U32, zz => {S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key) == ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(zz))) : Maybe<&2, V>}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i)), l, hl, LK.lookup_hit(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), key, SC.pow2(k), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), i, hi, hk))
90 get_hit3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, key, dflt, K2, l, ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), ST.g_cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), hr, hlv, hlk, U32.is_eq(l, 0), {==}, K.not_true_eq(U32.is_eq(l, 0), nz2))
91
92def get_r(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +key: String, +dflt: V, +K2: AR.Tree<String>, +sk: String, +w: U32, +h: Nat, +r: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), h, key, r)) -> {H.get_f(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), sk), w)) == (H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}, S.get(~V, dflt, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & V}:
93 match r:
94 case B.RHit{+i, +l}:
95 (+hi, rest) = hres
96 (+hk, hl) = rest
97 get_hit2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg, key, dflt, K2, sk, w, i, l, hi, hk, hl, bf_ok(sd, ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh), key, B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), i), B.all_inst(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), i, hi), B.all_inst(B.PLive{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh)}, SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), i, hi), hk))
98 case B.REnd{+e}:
99 (he, rest) = hres
100 (hz, rest2) = rest
101 (hp, hno) = rest2
102 get_end(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg, key, dflt, K2, sk, w, e, hno)
103
104# ---- the operation ----
105
106def GetOK(~V: Data, +sh: ST.Sh<V>, +dflt: V, +key: String, r: H.HashMap<&2, V> & V) -> Type:
107 Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.get(~V, dflt, ST.model(~V, sh), key)) : H.HashMap<&2, V> & V} & ({ST.good(~V, sh2) == True{} : Bool} & {ST.model(~V, sh2) == ST.model(~V, sh) : List<&2, S.Entry<V>>})>
108
109def get_po(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +dflt: V, +key: String, +r: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r), po: PA.ProbeOK(tabT, sd, AR.slots(String, ksT), PA.stored(key), K.kword(key), r, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key))) -> GetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, dflt, key, H.get(V, dflt, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key)):
110 match po:
111 case Tuple{+K2, Tuple{+e, rest}}:
112 (+hsl2, pk2) = rest
113 +kl = AR.slots(String, ksT)
114 +pkT = ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, AR.perfect(String, sd, ksT), vsT, nxT, hg)
115 +hgT = L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, b, vsT, nxT) == True{} : Bool}, AR.perfect(String, sd, ksT), True{}, pkT, hg)
116 +g2 = L.subst(List<&2, String>, z => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, z, AR.perfect(String, sd, K2), vsT, nxT) == True{} : Bool}, kl, AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), kl, hsl2), L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, b, vsT, nxT) == True{} : Bool}, True{}, AR.perfect(String, sd, K2), Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2), hgT))
117 +m2 = Equal.cong(List<&2, String>, List<&2, S.Entry<V>>, z => ST.absm(~V, TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), AR.slots(String, K2), kl, hsl2)
118 +eq = Equal.trans(H.HashMap<&2, V> & V, H.get_f(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), H.get_f(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), S.get(~V, dflt, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key)),
119 Equal.cong(H.Found & U32, H.HashMap<&2, V> & V, pr => H.get_f(V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), dflt, pr), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key), (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)), e),
120 get_r(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, AR.perfect(String, sd, ksT), vsT, nxT, hg, key, dflt, K2, PA.stored(key), K.kword(key), UD.v(HS.bucket(K.kword(key), CY.msk(k))), r, hres))
121 (ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}, (eq, (g2, m2)))
122
123# THEOREM: get is the specification's get; the map and its model are kept.
124def get_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +dflt: V, +key: String) -> GetOK(~V, sh, dflt, key, H.get(V, dflt, ST.real(~V, sh), key)):
125 match sh:
126 case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:
127 +kl = AR.slots(String, ksT)
128 +pk = AR.perfect(String, sd, ksT)
129 +ck = ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg)
130 +hk31 = L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ck)
131 +r = B.pf(key, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(K.kword(key), CY.msk(k))))), UD.v(HS.bucket(K.kword(key), CY.msk(k))))
132 get_po(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, dflt, key, r, res_of(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg, key), PA.probe_ok(1n, {==}, k, hk31, tabT, ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), sd, ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), kl, ksT, {==}, ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), key))