proofs/containers/lru/insp.bend
bend-collections-laws-containers@1.0.0.0 · 136 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/u32alg.bend as A
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/lru.bend as SP
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/u64.bend as W
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/src/containers/lru.bend as LR
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/keys.bend as K
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bump.bend as BU
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bumpsh.bend as BS
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/gone.bend as GO
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
21import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as HS
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_all.bend as PA
23
24import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/read.bend as RD
25import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/ins.bend as IC
26import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/ins1.bend as I1
27import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
28import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
29import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insert.bend as IS
30import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/modn.bend as M
31import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
32import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
33import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
34import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
35
36# add, a new key: the slot, from the free list's head or the next fresh one.
37
38
39
40# ---- lists ----
41
42def nm_lt(~V: Data, +xs: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +h: {ST.slok(~V, xs, fr, el) == True{} : Bool}) -> {NL.memn(fr, xs) == False{} : Bool}:
43 match xs:
44 case Nil{}:
45 {==}
46 case Con{+x, +t}:
47 +hx = L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h))
48 +ne = N.is_eq_lt(x, fr, hx)
49 +ih = nm_lt(~V, t, fr, el, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h))
50 L.subst(Bool, z => {Bool.or(z, NL.memn(fr, t)) == False{} : Bool}, False{}, Nat.is_eq(x, fr), Equal.sym(Bool, Nat.is_eq(x, fr), False{}, ne), L.subst(Bool, z => {Bool.or(False{}, z) == False{} : Bool}, False{}, NL.memn(fr, t), Equal.sym(Bool, NL.memn(fr, t), False{}, ih), {==}))
51
52def nv_c(~V: Data, +el: List<&2, Maybe<&2, V>>, +x: Nat, +y: Nat, +hx: {ST.live(~V, el, x) == True{} : Bool}, +hy: {ST.live(~V, el, y) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(x, y) == c : Bool}) -> {c == False{} : Bool}:
53 match c:
54 case True{}:
55 +exy = N.eq_from_is_eq(x, y, hc)
56 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, ST.live(~V, el, y), False{}, L.subst(Nat, z => {True{} == ST.live(~V, el, z) : Bool}, x, y, exy, Equal.sym(Bool, ST.live(~V, el, x), True{}, hx)), hy)))
57 case False{}:
58 {==}
59
60# a vacant slot is off the list of live slots
61def nm_vac(~V: Data, +xs: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +h: {ST.slok(~V, xs, fr, el) == True{} : Bool}, +y: Nat, +hy: {ST.live(~V, el, y) == False{} : Bool}) -> {NL.memn(y, xs) == False{} : Bool}:
62 match xs:
63 case Nil{}:
64 {==}
65 case Con{+x, +t}:
66 +hx = L.and_right(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h))
67 +ne = nv_c(~V, el, x, y, hx, hy, Nat.is_eq(x, y), {==})
68 +ih = nm_vac(~V, t, fr, el, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h), y, hy)
69 L.subst(Bool, z => {Bool.or(z, NL.memn(y, t)) == False{} : Bool}, False{}, Nat.is_eq(x, y), Equal.sym(Bool, Nat.is_eq(x, y), False{}, ne), L.subst(Bool, z => {Bool.or(False{}, z) == False{} : Bool}, False{}, NL.memn(y, t), Equal.sym(Bool, NL.memn(y, t), False{}, ih), {==}))
70
71# ---- the next fresh slot, when the arena has room ----
72
73
74def ipf_n(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(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))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +free2: U32, +hf2: {U32.is_eq(free2, 0) == True{} : Bool}, +hr: {U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)) == True{} : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), True{})):
75 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg)
76 +hsd1 = UL.sd1(sd, hsd)
77 +pm = ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)
78 +ehs = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ST.g_csize(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))
79 +hs0 = L.subst(Nat, z => {Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ehs, Equal.trans(Bool, Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), True{}, Equal.sym(Bool, U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U.is_lt_nat(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), hr))
80 +hsn = nm_lt(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))
81 +ei = W32.inc_val(one, h1, W32.nth0(AR.slots(U32, mT), 0n), W32.bound32(one, h1, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sd, hsd1, hs0))
82 +eln = N.eq_from_is_eq(Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))
83 +ecnt = Equal.trans(Nat, Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), 0n), SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), N.add_zero(SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}}))), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), 1n+SC.length(Nat, sl), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), I1.len_snoc(sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Equal.trans(Nat, 1n+SC.length(Nat, sl), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), Equal.cong(Nat, Nat, z => 1n+z, SC.length(Nat, sl), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.trans(Nat, SC.length(Nat, sl), Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.sym(Nat, Nat.add(SC.length(Nat, sl), 0n), SC.length(Nat, sl), N.add_zero(SC.length(Nat, sl))), eln)), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ei))))
84 +hsfr = L.subst(Nat, z => {Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ei), N.lt_succ(UD.v(W32.nth0(AR.slots(U32, mT), 0n))))
85 +hfr2 = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(sd)) == True{} : Bool}, 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ei), N.lt_succ_le_succ(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), hs0))
86 ok = IC.ins_core(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg, one, h1, key, hno, e, he, hz, hp, hroom, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), W32.nth0(AR.slots(U32, mT), 0n), {==}, hs0, hsn, Nil{}, free2, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)), hf2, {==}, {==}, {==}, IS.eq_is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), 0n), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), ecnt), {==}, hsfr, N.lt_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), hsfr), hfr2, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), UT.uset_p(5n, mT, pm, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), UT.uset_s(5n, mT, pm, 0n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), v, t, lo, hi)
87 +ea = UT.uset_a(5n, {==}, mT, pm, 0, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))
88 L.subst(Array<U32>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.put_slot(&2, V, cap, n, head, tail, free2, z, AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})), AR.thaw(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), Array.set(U32, AR.thaw(U32, mT), 0, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), Equal.sym(Array<U32>, Array.set(U32, AR.thaw(U32, mT), 0, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), AR.thaw(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), ea), ok)
89
90# THEOREM (add, a fresh slot with room)
91def ip_fresh(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(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))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +free2: U32, +hf2: {U32.is_eq(free2, 0) == True{} : Bool}, +hfz: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)) == True{} : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), True{})):
92 match fl:
93 case Nil{}:
94 ipf_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, free2, hf2, hr)
95 case Con{+s0, +tl}:
96 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg)
97 +hf0 = L.and_left(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0))), ST.flok(~V, tl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
98 +hs0 = N.lt_le_trans(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), L.and_left(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), hf0), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
99 +ef = A.eq_of(free, LK.lnk(s0), ST.g_cfree(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
100 +hz0 = L.subst(U32, z => {U32.is_eq(z, 0) == True{} : Bool}, free, LK.lnk(s0), ef, hfz)
101 Empty.absurd(BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), True{})), L.false_true(Equal.trans(Bool, False{}, U32.is_eq(LK.lnk(s0), 0), True{}, Equal.sym(Bool, U32.is_eq(LK.lnk(s0), 0), False{}, UL.lnk_nz(one, h1, s0, sd, hsd, hs0)), hz0)))
102
103# ---- the free list's head ----
104
105
106def ipl_c(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +s0: Nat, +tl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(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))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free))))):
107 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg)
108 +hf0 = L.and_left(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0))), ST.flok(~V, tl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
109 +hsfr = L.and_left(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), hf0)
110 +hvac = NL.not_t_f(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0), L.and_right(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), hf0))
111 +hs0 = N.lt_le_trans(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), hsfr, ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
112 +ef = A.eq_of(free, LK.lnk(s0), ST.g_cfree(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
113 +hsv = Equal.trans(Nat, UD.v(H.slot(free)), UD.v(H.slot(LK.lnk(s0))), s0, Equal.cong(U32, Nat, z => UD.v(H.slot(z)), free, LK.lnk(s0), ef), UL.ix_o(one, h1, s0, sd, hsd, hs0))
114 +hsn = nm_vac(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg), s0, hvac)
115 +hfll0 = ST.g_cfll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg)
116 +hfree = L.and_left(U32.is_eq(ST.lw(AR.slots(U32, lkT), s0, 1n), LK.fst_or(tl, 0)), ST.fll(AR.slots(U32, lkT), tl), hfll0)
117 +hfll = L.and_right(U32.is_eq(ST.lw(AR.slots(U32, lkT), s0, 1n), LK.fst_or(tl, 0)), ST.fll(AR.slots(U32, lkT), tl), hfll0)
118 +hfl = L.and_right(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0))), ST.flok(~V, tl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
119 +hnd0 = ST.g_cfnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg)
120 +hsfl = NL.not_t_f(NL.memn(s0, tl), L.and_left(Bool.not(NL.memn(s0, tl)), NL.nodupn(tl), hnd0))
121 +hfnd = L.and_right(Bool.not(NL.memn(s0, tl)), NL.nodupn(tl), hnd0)
122 +ecf = N.eq_from_is_eq(Nat.add(SC.length(Nat, sl), 1n+SC.length(Nat, tl)), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))
123 +ecnt = Equal.trans(Nat, Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{s0, Nil{}})), SC.length(Nat, tl)), Nat.add(1n+SC.length(Nat, sl), SC.length(Nat, tl)), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, SC.length(Nat, tl)), SC.length(Nat, SC.append(Nat, sl, Con{s0, Nil{}})), 1n+SC.length(Nat, sl), I1.len_snoc(sl, s0)), Equal.trans(Nat, 1n+Nat.add(SC.length(Nat, sl), SC.length(Nat, tl)), Nat.add(SC.length(Nat, sl), 1n+SC.length(Nat, tl)), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.sym(Nat, Nat.add(SC.length(Nat, sl), 1n+SC.length(Nat, tl)), 1n+Nat.add(SC.length(Nat, sl), SC.length(Nat, tl)), N.add_succ(SC.length(Nat, sl), SC.length(Nat, tl))), ecf))
124 ok = IC.ins_core(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg, one, h1, key, hno, e, he, hz, hp, hroom, s0, H.slot(free), hsv, hs0, hsn, tl, ST.lw(AR.slots(U32, lkT), s0, 1n), W32.nth0(AR.slots(U32, mT), 0n), hfree, hfll, hfl, hfnd, IS.eq_is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{s0, Nil{}})), SC.length(Nat, tl)), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ecnt), hsfl, hsfr, N.le_refl(UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg), mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg), Equal.sym(List<&2, U32>, SC.update(U32, AR.slots(U32, mT), 0n, W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(U32, mT), BU.upd_id(AR.slots(U32, mT), 0n)), v, t, lo, hi)
125 +hsu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s0, UD.v(H.slot(free)), Equal.sym(Nat, UD.v(H.slot(free)), s0, hsv), hs0)
126 +i1 = Equal.trans(Nat, UD.v(LR.nidx(H.slot(free))), ST.off(UD.v(H.slot(free)), 1n), ST.off(s0, 1n), ID.w1(one, h1, H.slot(free), sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 1n), UD.v(H.slot(free)), s0, hsv))
127 +er = GO.rd(one, h1, lkT, sd, hsd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg), LR.nidx(H.slot(free)), s0, 1n, {==}, hs0, i1)
128 L.subst(Array<U32> & U32, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, z)), (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s0, 1n)), Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free))), Equal.sym(Array<U32> & U32, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free))), (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s0, 1n)), er), ok)
129
130# THEOREM (add, the free list's head)
131def ip_free(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(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))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +hfz: {U32.is_eq(free, 0) == False{} : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free))))):
132 match fl:
133 case Nil{}:
134 Empty.absurd(BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free))))), L.true_false(Equal.trans(Bool, True{}, U32.is_eq(free, 0), False{}, Equal.sym(Bool, U32.is_eq(free, 0), True{}, ST.g_cfree(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), hfz)))
135 case Con{+s0, +tl}:
136 ipl_c(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, s0, tl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi)