1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/array.bend as AR
5	import ../../../spec/lib/common.bend as SC
6	import ../../lib/u32div.bend as UD
7	import ../../lib/word.bend as WD
8	import ../../../src/containers/hash_table.bend as H
9	import ../../../src/containers/lru.bend as LR
10	import ../hash_table/keys.bend as K
11	import ../hash_table/table.bend as TB
12	import ../hash_table/buckets.bend as B
13	import ../hash_table/arr.bend as AX
14	import ../hash_table/probe_impl.bend as PI
15	import ../hash_table/cyc.bend as CY
16	import ../hash_table/qprobe.bend as QP
17	import ../../lib/words32.bend as W32
18	
19	# The fused one-character remove loop qrm is the model probe B.pf followed by
20	# the removal at the bucket it finds (nothing when it finds none).
21	
22	
23	def qrm_of(~V: Data, r: B.Res, tab: Array<U32>, +mask: U32, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ks: Array<String>, ents: Array<Maybe<&2, V>>, lk: Array<U32>) -> LR.LRU<&2, V> & Maybe<&2, V>:
24	  match r:
25	    case B.RHit{+at, +l}:
26	      LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, m, H.del_at(tab, mask, U32.from_nat(at)), ks, ents, lk}, H.slot(l), 2)
27	    case B.REnd{at}:
28	      (LR.F{cap, n, head, tail, free, m, tab, ks, ents, lk}, None{})
29	
30	def rq0(~V: Data, +cap: U32, +nn: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +key: String, +bs: List<&2, B.Bk>, +nb: Nat, +mask: U32, +w: U32, +i: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(UD.v(i), SC.pow2(k)) == True{} : Bool}, +ms: B.MS) -> {LR.qrm(&2, V, 0n, QP.qstep_of(ms, AR.thaw(U32, tabT)), mask, w, i, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, nb, 0n, ms, UD.v(i)), AR.thaw(U32, tabT), mask, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}:
31	  match ms:
32	    case B.MEnd{}:
33	      {==}
34	    case B.MHit{+l}:
35	      Equal.cong(U32, LR.LRU<&2, V> & Maybe<&2, V>, z => LR.drop_slot(&2, V, LR.F{cap, nn, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), mask, z), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(l), 2), i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, PI.from_v(i, k, hk, hi)))
36	    case B.MNext{}:
37	      {==}
38	
39	def rq1(~V: Data, +cap: U32, +nn: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +key: String, +bs: List<&2, B.Bk>, +nb: Nat, +mask: U32, +w: U32, +i: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(UD.v(i), SC.pow2(k)) == True{} : Bool}, +p: Nat, +hnext: {UD.v(H.bnext(i, mask)) == Nat.mod(1n+UD.v(i), nb) : Nat}, +rec: {LR.qrm(&2, V, p, H.qstep(AR.thaw(U32, tabT), H.bnext(i, mask), w), mask, w, H.bnext(i, mask), cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, nb, p, B.mstep(key, B.at(bs, UD.v(H.bnext(i, mask)))), UD.v(H.bnext(i, mask))), AR.thaw(U32, tabT), mask, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}, +ms: B.MS) -> {LR.qrm(&2, V, 1n+p, QP.qstep_of(ms, AR.thaw(U32, tabT)), mask, w, i, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, nb, 1n+p, ms, UD.v(i)), AR.thaw(U32, tabT), mask, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}:
40	  match ms:
41	    case B.MEnd{}:
42	      {==}
43	    case B.MHit{+l}:
44	      Equal.cong(U32, LR.LRU<&2, V> & Maybe<&2, V>, z => LR.drop_slot(&2, V, LR.F{cap, nn, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), mask, z), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(l), 2), i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, PI.from_v(i, k, hk, hi)))
45	    case B.MNext{}:
46	      L.subst(Nat, z => {LR.qrm(&2, V, p, H.qstep(AR.thaw(U32, tabT), H.bnext(i, mask), w), mask, w, H.bnext(i, mask), cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, nb, p, B.mstep(key, B.at(bs, z)), z), AR.thaw(U32, tabT), mask, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}, UD.v(H.bnext(i, mask)), Nat.mod(1n+UD.v(i), nb), hnext, rec)
47	
48	
49	# THEOREM: the fused loop is the model probe then the removal
50	def qrm_ok(~V: Data, +cap: U32, +nn: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +sd: Nat, +kl0: List<&2, String>, +c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +f: Nat, +i: U32, +hi: {Nat.is_lt(UD.v(i), SC.pow2(k)) == True{} : Bool}) -> {LR.qrm(&2, V, f, H.qstep(AR.thaw(U32, tabT), i, H.short_word(c)), CY.msk(k), H.short_word(c), i, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(SCon{Chr{c}, SNil{}}, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), f, B.mstep(SCon{Chr{c}, SNil{}}, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(i))), UD.v(i)), AR.thaw(U32, tabT), CY.msk(k), cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}:
51	  match f:
52	    case 0n:
53	      +tb = AR.slots(U32, tabT)
54	      +n = SC.pow2(k)
55	      +bs = TB.buckets(tb, kl0, n)
56	      +w = H.short_word(c)
57	      +key = {SCon{Chr{c}, SNil{}} : String}
58	      +hb = N.double_lt_bit(True{}, UD.v(i), SC.pow2(k), hi)
59	      +ew = AX.ix_w(i, 1n+k, hk31, hb)
60	      +el = AX.ix_l(i, 1n+k, hk31, hb)
61	      +hwb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(UD.v(i)), UD.v(U32.shl(i)), Equal.sym(Nat, UD.v(U32.shl(i)), Nat.double(UD.v(i)), ew), N.lt_trans(Nat.double(UD.v(i)), 1n+Nat.double(UD.v(i)), SC.pow2(1n+k), N.lt_succ(Nat.double(UD.v(i))), hb))
62	      +hlb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(UD.v(i)), UD.v(U32.inc(U32.shl(i))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(i))), 1n+Nat.double(UD.v(i)), el), hb)
63	      +x = W32.nth0(tb, UD.v(U32.shl(i)))
64	      +l = W32.nth0(tb, UD.v(U32.inc(U32.shl(i))))
65	      +dx = PI.dec_ix(tb, kl0, UD.v(i), UD.v(U32.shl(i)), UD.v(U32.inc(U32.shl(i))), ew, el)
66	      +dat = TB.at_buckets(tb, kl0, n, UD.v(i), hi)
67	      +dd = Equal.trans(B.Bk, B.at(bs, UD.v(i)), TB.dec(tb, kl0, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dat, Equal.sym(B.Bk, TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), TB.dec(tb, kl0, UD.v(i)), dx))
68	      +hwb = L.subst(B.Bk, b => {B.wb(sd, b) == True{} : Bool}, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd, B.all_inst(B.PWell{bs, sd}, n, hwell, UD.v(i), hi))
69	      +hvI = Pair.snd({B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, {B.implies(Bool.not(U32.is_eq(x, 0)), B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(TB.nths(kl0, UD.v(H.slot(l))))))) == True{} : Bool}, PI.wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
70	      +ms = QP.qdec(w, x, l)
71	      +em = Equal.trans(B.MS, ms, B.mstep(key, TB.dec_c(x, l, kl0, U32.is_eq(x, 0))), B.mstep(key, B.at(bs, UD.v(i))), QP.qdecide(c, hc, x, l, kl0, hvI), Equal.cong(B.Bk, B.MS, b => B.mstep(key, b), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), B.at(bs, UD.v(i)), Equal.sym(B.Bk, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd)))
72	      +es = QP.qstep(1n+k, tabT, i, w, hk31, pt, hwb0, hlb0)
73	      +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==}))
74	      +p3 = rq0(~V, cap, nn, head, tail, free, mT, ksT, eT, lkT, tabT, key, bs, n, CY.msk(k), w, i, k, hk32, hi, ms)
75	      +p2 = L.subst(B.MS, m => {LR.qrm(&2, V, 0n, QP.qstep_of(ms, AR.thaw(U32, tabT)), CY.msk(k), H.short_word(c), i, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, n, 0n, m, UD.v(i)), AR.thaw(U32, tabT), CY.msk(k), cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}, ms, B.mstep(key, B.at(bs, UD.v(i))), em, p3)
76	      L.subst(H.QStep, s => {LR.qrm(&2, V, 0n, s, CY.msk(k), H.short_word(c), i, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, n, 0n, B.mstep(key, B.at(bs, UD.v(i))), UD.v(i)), AR.thaw(U32, tabT), CY.msk(k), cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}, QP.qstep_of(ms, AR.thaw(U32, tabT)), H.qstep(AR.thaw(U32, tabT), i, w), Equal.sym(H.QStep, H.qstep(AR.thaw(U32, tabT), i, w), QP.qstep_of(ms, AR.thaw(U32, tabT)), es), p2)
77	    case 1n+p:
78	      +tb = AR.slots(U32, tabT)
79	      +n = SC.pow2(k)
80	      +bs = TB.buckets(tb, kl0, n)
81	      +w = H.short_word(c)
82	      +key = {SCon{Chr{c}, SNil{}} : String}
83	      +hb = N.double_lt_bit(True{}, UD.v(i), SC.pow2(k), hi)
84	      +ew = AX.ix_w(i, 1n+k, hk31, hb)
85	      +el = AX.ix_l(i, 1n+k, hk31, hb)
86	      +hwb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(UD.v(i)), UD.v(U32.shl(i)), Equal.sym(Nat, UD.v(U32.shl(i)), Nat.double(UD.v(i)), ew), N.lt_trans(Nat.double(UD.v(i)), 1n+Nat.double(UD.v(i)), SC.pow2(1n+k), N.lt_succ(Nat.double(UD.v(i))), hb))
87	      +hlb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(UD.v(i)), UD.v(U32.inc(U32.shl(i))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(i))), 1n+Nat.double(UD.v(i)), el), hb)
88	      +x = W32.nth0(tb, UD.v(U32.shl(i)))
89	      +l = W32.nth0(tb, UD.v(U32.inc(U32.shl(i))))
90	      +dx = PI.dec_ix(tb, kl0, UD.v(i), UD.v(U32.shl(i)), UD.v(U32.inc(U32.shl(i))), ew, el)
91	      +dat = TB.at_buckets(tb, kl0, n, UD.v(i), hi)
92	      +dd = Equal.trans(B.Bk, B.at(bs, UD.v(i)), TB.dec(tb, kl0, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dat, Equal.sym(B.Bk, TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), TB.dec(tb, kl0, UD.v(i)), dx))
93	      +hwb = L.subst(B.Bk, b => {B.wb(sd, b) == True{} : Bool}, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd, B.all_inst(B.PWell{bs, sd}, n, hwell, UD.v(i), hi))
94	      +hvI = Pair.snd({B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, {B.implies(Bool.not(U32.is_eq(x, 0)), B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(TB.nths(kl0, UD.v(H.slot(l))))))) == True{} : Bool}, PI.wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
95	      +ms = QP.qdec(w, x, l)
96	      +em = Equal.trans(B.MS, ms, B.mstep(key, TB.dec_c(x, l, kl0, U32.is_eq(x, 0))), B.mstep(key, B.at(bs, UD.v(i))), QP.qdecide(c, hc, x, l, kl0, hvI), Equal.cong(B.Bk, B.MS, b => B.mstep(key, b), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), B.at(bs, UD.v(i)), Equal.sym(B.Bk, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd)))
97	      +es = QP.qstep(1n+k, tabT, i, w, hk31, pt, hwb0, hlb0)
98	      +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==}))
99	      +hks = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k), N.lt_le_trans(SC.pow2(k), SC.pow2(1n+k), WD.sc(32n, one), N.pow2_lt_succ(k), W32.pow_le32(one, h1, 1n+k, hk31)))
100	      +hi1 = L.subst(Nat, z => {Nat.is_lt(UD.v(i), z) == True{} : Bool}, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k), hi)
101	      +hnext = Equal.trans(Nat, UD.v(H.bnext(i, CY.msk(k))), Nat.mod(1n+UD.v(i), WD.sc(k, one)), Nat.mod(1n+UD.v(i), n), CY.next_val(one, h1, k, i, hks, hi1), Equal.cong(Nat, Nat, z => Nat.mod(1n+UD.v(i), z), WD.sc(k, one), SC.pow2(k), Equal.sym(Nat, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k))))
102	      +hi2 = L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, Nat.mod(1n+UD.v(i), n), UD.v(H.bnext(i, CY.msk(k))), Equal.sym(Nat, UD.v(H.bnext(i, CY.msk(k))), Nat.mod(1n+UD.v(i), n), hnext), PI.mod_lt(n, N.succ_le_lt(0n, n, N.pow2_pos(k)), 1n+UD.v(i)))
103	      +p3 = rq1(~V, cap, nn, head, tail, free, mT, ksT, eT, lkT, tabT, key, bs, n, CY.msk(k), w, i, k, hk32, hi, p, hnext, qrm_ok(~V, cap, nn, head, tail, free, mT, ksT, eT, lkT, one, h1, k, hk31, tabT, pt, sd, kl0, c, hc, hwell, p, H.bnext(i, CY.msk(k)), hi2), ms)
104	      +p2 = L.subst(B.MS, m => {LR.qrm(&2, V, 1n+p, QP.qstep_of(ms, AR.thaw(U32, tabT)), CY.msk(k), H.short_word(c), i, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, n, 1n+p, m, UD.v(i)), AR.thaw(U32, tabT), CY.msk(k), cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}, ms, B.mstep(key, B.at(bs, UD.v(i))), em, p3)
105	      L.subst(H.QStep, s => {LR.qrm(&2, V, 1n+p, s, CY.msk(k), H.short_word(c), i, cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) == qrm_of(~V, B.pf(key, bs, n, 1n+p, B.mstep(key, B.at(bs, UD.v(i))), UD.v(i)), AR.thaw(U32, tabT), CY.msk(k), cap, nn, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}, QP.qstep_of(ms, AR.thaw(U32, tabT)), H.qstep(AR.thaw(U32, tabT), i, w), Equal.sym(H.QStep, H.qstep(AR.thaw(U32, tabT), i, w), QP.qstep_of(ms, AR.thaw(U32, tabT)), es), p2)