~/bend-docscommunity

proofs/containers/lru/insp.bend source

proofs/containers/lru/insp.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32alg.bend as Aimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/math/u64.bend as Wimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/table.bend as TBimport ../hash_table/buckets.bend as Bimport ../hash_table/cyc.bend as CYimport ../hash_table/keys.bend as Kimport ./state.bend as STimport ./bump.bend as BUimport ./bumpsh.bend as BSimport ./gone.bend as GOimport ./unlink.bend as ULimport ../../../src/math/hash.bend as HSimport ../hash_table/probe_all.bend as PAimport ./read.bend as RDimport ./ins.bend as ICimport ./ins1.bend as I1import ./idx.bend as IDimport ../../lib/u32.bend as Uimport ../hash_table/insert.bend as ISimport ../hash_table/modn.bend as Mimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# add, a new key: the slot, from the free list's head or the next fresh one.# ---- lists ----def 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}:  match xs:    case Nil{}:      {==}    case Con{+x, +t}:      +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))      +ne = N.is_eq_lt(x, fr, hx)      +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))      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), {==}))def 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}:  match c:    case True{}:      +exy = N.eq_from_is_eq(x, y, hc)      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)))    case False{}:      {==}# a vacant slot is off the list of live slotsdef 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}:  match xs:    case Nil{}:      {==}    case Con{+x, +t}:      +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))      +ne = nv_c(~V, el, x, y, hx, hy, Nat.is_eq(x, y), {==})      +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)      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), {==}))# ---- the next fresh slot, when the arena has room ----def 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{})):  +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg)  +hsd1 = UL.sd1(sd, hsd)  +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)  +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))  +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))  +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))  +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))  +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))  +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))))  +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))))  +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))  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)  +ea = UT.uset_a(5n, {==}, mT, pm, 0, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))  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)# THEOREM (add, a fresh slot with room)def 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{})):  match fl:    case Nil{}:      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)    case Con{+s0, +tl}:      +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg)      +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))      +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))      +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))      +hz0 = L.subst(U32, z => {U32.is_eq(z, 0) == True{} : Bool}, free, LK.lnk(s0), ef, hfz)      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)))# ---- the free list's head ----def 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))))):  +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg)  +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))  +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)  +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))  +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))  +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))  +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))  +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)  +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)  +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)  +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)  +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))  +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)  +hsfl = NL.not_t_f(NL.memn(s0, tl), L.and_left(Bool.not(NL.memn(s0, tl)), NL.nodupn(tl), hnd0))  +hfnd = L.and_right(Bool.not(NL.memn(s0, tl)), NL.nodupn(tl), hnd0)  +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))  +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))  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)  +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)  +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))  +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)  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)# THEOREM (add, the free list's head)def 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))))):  match fl:    case Nil{}:      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)))    case Con{+s0, +tl}:      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)