proofs/containers/hash_table/keysw.bend
bend-collections-laws-containers@1.0.0.0 · 248 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/u32.bend as U
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/containers/hash_table.bend as H
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/strings.bend as STR
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/arr.bend as AX
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as ST
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/grow.bend as GR
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insa.bend as IA
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/arena.bend as AN
21import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
22
23# keys: the walk from the last bucket down lists every key in bucket order,
24# which is the order of the model's entries.
25
26
27# the key of a bucket, as a list
28def kof(b: B.Bk) -> List<&2, String>:
29 match b:
30 case B.BE{}:
31 Nil{}
32 case B.BF{w, l, k}:
33 Con{k, Nil{}}
34
35# the keys of buckets j .. j + m - 1
36def kb(+bs: List<&2, B.Bk>, +m: Nat, +j: Nat) -> List<&2, String>:
37 match m:
38 case 0n:
39 Nil{}
40 case 1n+p:
41 SC.append(String, kof(B.at(bs, j)), kb(bs, p, 1n+j))
42
43# ---- the model's keys ----
44
45def keys_app(~V: Data, +a: List<&2, S.Entry<V>>, +b: List<&2, S.Entry<V>>) -> {S.keys(~V, SC.append(S.Entry<V>, a, b)) == SC.append(String, S.keys(~V, a), S.keys(~V, b)) : List<&2, String>}:
46 match a:
47 case Nil{}:
48 {==}
49 case Con{S.E{+j, +v}, +t}:
50 Equal.cong(List<&2, String>, List<&2, String>, z => Con{j, z}, S.keys(~V, SC.append(S.Entry<V>, t, b)), SC.append(String, S.keys(~V, t), S.keys(~V, b)), keys_app(~V, t, b))
51
52def ek_m(~V: Data, +k: String, +m: Maybe<&2, V>, +h: {ST.some_b(~V, m) == True{} : Bool}) -> {S.keys(~V, ST.ent_m(~V, k, m)) == Con{k, Nil{}} : List<&2, String>}:
53 match m:
54 case None{}:
55 Empty.absurd({S.keys(~V, ST.ent_m(~V, k, None{})) == Con{k, Nil{}} : List<&2, String>}, L.false_true(h))
56 case Some{v}:
57 {==}
58
59def ent_keys(~V: Data, +b: B.Bk, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +h: {B.live_b(ST.lvs(~V, vsl), fr, b) == True{} : Bool}) -> {S.keys(~V, ST.ent(~V, b, vsl)) == kof(b) : List<&2, String>}:
60 match b:
61 case B.BE{}:
62 {==}
63 case B.BF{w, +l, +k}:
64 +t = UD.v(H.slot(l))
65 +hs = Equal.trans(Bool, ST.some_b(~V, ST.nthm(~V, vsl, t)), B.nthb(ST.lvs(~V, vsl), t), True{}, Equal.sym(Bool, B.nthb(ST.lvs(~V, vsl), t), ST.some_b(~V, ST.nthm(~V, vsl, t)), ST.lvs_nth(~V, vsl, t)), L.and_left(B.nthb(ST.lvs(~V, vsl), t), Nat.is_lt(t, fr), h))
66 ek_m(~V, k, ST.nthm(~V, vsl, t), hs)
67
68# THEOREM: the model's keys are the buckets' keys in bucket order
69def keys_absm(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +n: Nat, +hl: {B.all_lt(B.PLive{bs, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}) -> {S.keys(~V, ST.absm(~V, bs, vsl, m, j)) == kb(bs, m, j) : List<&2, String>}:
70 match m:
71 case 0n:
72 {==}
73 case 1n+p:
74 +hj = IA.idx_lt(j, p, n, hjm)
75 Equal.trans(List<&2, String>, S.keys(~V, ST.absm(~V, bs, vsl, 1n+p, j)), SC.append(String, S.keys(~V, ST.ent(~V, B.at(bs, j), vsl)), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), kb(bs, 1n+p, j), keys_app(~V, ST.ent(~V, B.at(bs, j), vsl), ST.absm(~V, bs, vsl, p, 1n+j)),
76 Equal.trans(List<&2, String>, SC.append(String, S.keys(~V, ST.ent(~V, B.at(bs, j), vsl)), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), SC.append(String, kof(B.at(bs, j)), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), kb(bs, 1n+p, j), Equal.cong(List<&2, String>, List<&2, String>, z => SC.append(String, z, S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), S.keys(~V, ST.ent(~V, B.at(bs, j), vsl)), kof(B.at(bs, j)), ent_keys(~V, B.at(bs, j), vsl, fr, B.all_inst(B.PLive{bs, ST.lvs(~V, vsl), fr}, n, hl, j, hj))),
77 Equal.cong(List<&2, String>, List<&2, String>, z => SC.append(String, kof(B.at(bs, j)), z), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j)), kb(bs, p, 1n+j), keys_absm(~V, bs, vsl, fr, n, hl, p, 1n+j, IA.idx_next(j, p, n, hjm)))))
78
79# ---- the walk ----
80
81
82def WStep(+tabT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +q: Nat, +kk: U32, +KT: AR.Tree<String>) -> Type:
83 Sigma<&1, &1, AR.Tree<String>, K2 => {H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}) == H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)} : H.Walk} & ({AR.slots(String, K2) == kl : List<&2, String>} & {AR.perfect(String, sd, K2) == True{} : Bool})>
84
85def acc_eq(+bs: List<&2, B.Bk>, +n: Nat, +q: Nat, +hq: {Nat.is_lt(q, n) == True{} : Bool}) -> {kb(bs, Nat.sub(n, q), q) == SC.append(String, kof(B.at(bs, q)), kb(bs, Nat.sub(n, 1n+q), 1n+q)) : List<&2, String>}:
86 +r = Nat.sub(n, 1n+q)
87 +e1 = N.sub_add(n, 1n+q, N.lt_succ_le_succ(q, n, hq))
88 +e2 = Equal.trans(Nat, Nat.add(q, 1n+r), 1n+Nat.add(q, r), n, N.add_succ(q, r), e1)
89 +e3 = L.subst(Nat, z => {Nat.sub(z, q) == 1n+r : Nat}, Nat.add(q, 1n+r), n, e2, N.add_sub_cancel(q, 1n+r))
90 Equal.cong(Nat, List<&2, String>, z => kb(bs, z, q), Nat.sub(n, q), 1n+r, e3)
91
92def w_ew(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {UD.v(U32.shl(kk)) == Nat.double(q) : Nat}:
93 +hh = L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+k)) == True{} : Bool}, q, UD.v(kk), Equal.sym(Nat, UD.v(kk), q, hkk), N.double_lt_bit(True{}, q, SC.pow2(k), hq))
94 Equal.trans(Nat, UD.v(U32.shl(kk)), Nat.double(UD.v(kk)), Nat.double(q), AX.ix_w(kk, 1n+k, hk31, hh), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(kk), q, hkk))
95
96def w_el(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {UD.v(U32.inc(U32.shl(kk))) == 1n+Nat.double(q) : Nat}:
97 +hh = L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+k)) == True{} : Bool}, q, UD.v(kk), Equal.sym(Nat, UD.v(kk), q, hkk), N.double_lt_bit(True{}, q, SC.pow2(k), hq))
98 Equal.trans(Nat, UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(UD.v(kk)), 1n+Nat.double(q), AX.ix_l(kk, 1n+k, hk31, hh), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), UD.v(kk), q, hkk))
99
100def w_get(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)) == (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))) : Array<U32> & U32}:
101 +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(q), UD.v(U32.shl(kk)), Equal.sym(Nat, UD.v(U32.shl(kk)), Nat.double(q), w_ew(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), N.lt_trans(Nat.double(q), 1n+Nat.double(q), SC.pow2(1n+k), N.lt_succ(Nat.double(q)), N.double_lt_bit(True{}, q, SC.pow2(k), hq)))
102 Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(kk)))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), AX.getw(1n+k, tabT, U32.shl(kk), hk31, hi, pt), Equal.cong(Nat, Array<U32> & U32, z => (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), z)), UD.v(U32.shl(kk)), Nat.double(q), w_ew(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)))
103
104def w_getl(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(kk))) == (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))) : Array<U32> & U32}:
105 +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(q), UD.v(U32.inc(U32.shl(kk))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(q), w_el(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), N.double_lt_bit(True{}, q, SC.pow2(k), hq))
106 Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(kk))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(kk))))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), AX.getw(1n+k, tabT, U32.inc(U32.shl(kk)), hk31, hi, pt), Equal.cong(Nat, Array<U32> & U32, z => (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), z)), UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(q), w_el(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)))
107
108def w_at(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == c : Bool}) -> {B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q) == TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, c) : B.Bk}:
109 Equal.trans(B.Bk, B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q), TB.dec(AR.slots(U32, tabT), kl, q), TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, c), TB.at_buckets(AR.slots(U32, tabT), kl, SC.pow2(k), q, hq), Equal.cong(Bool, B.Bk, z => TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, z), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), c, hc))
110
111def w_accx(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +b: B.Bk, +hb: {B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q) == b : B.Bk}) -> {kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q) == SC.append(String, kof(b), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)) : List<&2, String>}:
112 Equal.trans(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), SC.append(String, kof(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q)), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), SC.append(String, kof(b), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), acc_eq(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), q, hq), Equal.cong(B.Bk, List<&2, String>, y => SC.append(String, kof(y), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q), b, hb))
113
114def nth_upd_same(+xs: List<&2, String>, +i: Nat, +v: String, +h: {Nat.is_lt(i, SC.length(String, xs)) == True{} : Bool}) -> {SC.nth(String, SC.update(String, xs, i, v), i) == Some{v} : Maybe<&2, String>}:
115 match xs i:
116 case Nil{} _:
117 Empty.absurd({SC.nth(String, SC.update(String, Nil{}, i, v), i) == Some{v} : Maybe<&2, String>}, N.lt_zero_absurd(i, h))
118 case Con{x, t} 0n:
119 {==}
120 case Con{x, t} 1n+p:
121 nth_upd_same(t, p, v, h)
122
123
124def w_long(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool}, +hs: {H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))) == False{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
125 +hb = w_at(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, False{}, hc)
126 +hw = L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q), TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{}), hb, B.all_inst(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k), hwell, q, hq))
127 +hsp = L.and_left(Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SC.pow2(sd)), Bool.and(U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), K.kword(TB.keyof(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))))), Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), 0))), hw)
128 +hx = L.subst(List<&2, String>, z => {SC.nth(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))) == Some{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))} : Maybe<&2, String>}, kl, AR.slots(String, KT), Equal.sym(List<&2, String>, AR.slots(String, KT), kl, hsl), TB.nths_some(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), AN.len_eq_lt(String, kl, sd, hlen, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), hsp)))
129 +esw = AR.swap(String, sd, KT, H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), SNil{}, TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), hsd, hsp, hx, pk)
130 +p1 = AR.upd_perfect(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, pk)
131 +es1 = AR.upd_slots(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, hsp, pk)
132 +hx1 = L.subst(List<&2, String>, z => {SC.nth(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))) == Some{SNil{}} : Maybe<&2, String>}, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), Equal.sym(List<&2, String>, AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), es1), nth_upd_same(AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, AN.len_eq_lt(String, AR.slots(String, KT), sd, AR.slots_length(String, sd, KT, pk), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), hsp)))
133 +est = AR.set(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), SNil{}, hsd, hsp, hx1, p1)
134 +ek = Equal.cong(Bool, String, b => TB.keyof_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), b), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), False{}, hs)
135 +eacc = Equal.trans(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), SC.append(String, kof(TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{})), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, w_accx(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{}), hb), Equal.cong(String, List<&2, String>, z => Con{z, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, TB.keyof(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), ek))
136 +xeq = Equal.cong(List<&2, String>, String, z => TB.nths(z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), AR.slots(String, KT), kl, hsl)
137 +e1 = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0)), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_w(AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), w_get(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), Equal.cong(Bool, H.Walk, c => H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), False{}, hc))
138 +e2 = Equal.trans(H.Walk, H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.wk_kind(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), Equal.cong(Bool, H.Walk, c => H.wk_kind(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), False{}, hs), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(kk))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), w_getl(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)))
139 +e3 = Equal.cong(Array<String> & String, H.Walk, r => H.wk_copy(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.swap(String, AR.thaw(String, KT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), SNil{}), (AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), esw)
140 +e4 = Equal.cong(String, H.Walk, x => H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(x)), TB.nths(AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), xeq)
141 +e5 = Equal.cong(String & String, H.Walk, r => H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), r), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), (TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), STR.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))))
142 +e6 = Equal.cong(Array<String>, H.Walk, a => H.WK{AR.thaw(U32, tabT), a, Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, Array.set(String, AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), est)
143 +e7 = Equal.cong(List<&2, String>, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), z}, Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Equal.sym(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, eacc))
144 +eq = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e1, Equal.trans(H.Walk, H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e2, Equal.trans(H.Walk, H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e3, Equal.trans(H.Walk, H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, {==}, Equal.trans(H.Walk, H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.WK{AR.thaw(U32, tabT), Array.set(String, AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e5, Equal.trans(H.Walk, H.WK{AR.thaw(U32, tabT), Array.set(String, AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e6, e7))))))
145 +es2 = AR.upd_slots(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), hsp, p1)
146 +esl = Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), SC.update(String, AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, es2, Equal.trans(List<&2, String>, SC.update(String, AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SC.update(String, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, Equal.cong(List<&2, String>, List<&2, String>, z => SC.update(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), es1), Equal.trans(List<&2, String>, SC.update(String, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, TB.upd_upd(AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), Equal.trans(List<&2, String>, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SC.update(String, kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, Equal.cong(List<&2, String>, List<&2, String>, z => SC.update(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), AR.slots(String, KT), kl, hsl), TB.upd_self(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))))))
147 (AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), (eq, (esl, AR.upd_perfect(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), p1))))
148
149def w_short(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool}, +hs: {H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))) == True{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
150 +hb = w_at(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, False{}, hc)
151 +ek = Equal.cong(Bool, String, b => TB.keyof_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), b), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), True{}, hs)
152 +eacc = Equal.trans(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), SC.append(String, kof(TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{})), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, w_accx(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{}), hb), Equal.cong(String, List<&2, String>, z => Con{z, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, TB.keyof(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, ek))
153 +e1 = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0)), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_w(AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), w_get(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), Equal.cong(Bool, H.Walk, c => H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), False{}, hc))
154 +e2 = Equal.cong(Bool, H.Walk, c => H.wk_kind(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), True{}, hs)
155 +e3 = Equal.cong(List<&2, String>, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), z}, Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Equal.sym(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, eacc))
156 (KT, (Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e1, Equal.trans(H.Walk, H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e2, e3)), (hsl, pk)))
157
158def w_empty(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == True{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
159 +hb = w_at(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, True{}, hc)
160 +e1 = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0)), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), True{}), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_w(AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), w_get(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), Equal.cong(Bool, H.Walk, c => H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), True{}, hc))
161 +e2 = Equal.cong(List<&2, String>, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), z}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Equal.sym(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), w_accx(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, B.BE{}, hb)))
162 (KT, (Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), True{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e1, e2), (hsl, pk)))
163
164def w_full(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool}, +d: Bool, +hd: {H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))) == d : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
165 match d:
166 case True{}:
167 w_short(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc, hd)
168 case False{}:
169 w_long(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc, hd)
170
171def w_c(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == c : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
172 match c:
173 case True{}:
174 w_empty(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc)
175 case False{}:
176 w_full(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc, H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), {==})
177
178# THEOREM: one step of the walk prepends bucket q's key
179def wstep(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
180 w_c(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), {==})
181
182
183def WalkOK(+tabT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +q: Nat, +kk: U32, +KT: AR.Tree<String>) -> Type:
184 Sigma<&1, &1, AR.Tree<String>, K2 => {H.wk_go(1n+q, kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}) == H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), 0n)} : H.Walk} & ({AR.slots(String, K2) == kl : List<&2, String>} & {AR.perfect(String, sd, K2) == True{} : Bool})>
185
186def walk_0(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +kk: U32, +KT: AR.Tree<String>, st: WStep(tabT, kl, k, sd, 0n, kk, KT)) -> WalkOK(tabT, kl, k, sd, 0n, kk, KT):
187 match st:
188 case Tuple{+K2, Tuple{+e1, rest}}:
189 (+hs2, pk2) = rest
190 (K2, (Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n), 1n)}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 0n), 0n)}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), 0n)}, e1, Equal.cong(Nat, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), z, 0n)}, Nat.sub(SC.pow2(k), 0n), SC.pow2(k), N.sub_zero(SC.pow2(k)))), (hs2, pk2)))
191
192def walk_s2(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +p: Nat, +kk: U32, +KT: AR.Tree<String>, +K2: AR.Tree<String>, +e1: {H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 2n+p), 2n+p)}) == H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+p), 1n+p)} : H.Walk}, wo: WalkOK(tabT, kl, k, sd, p, U32.sub(kk, 1), K2)) -> WalkOK(tabT, kl, k, sd, 1n+p, kk, KT):
193 match wo:
194 case Tuple{+K3, Tuple{+e2, rest}}:
195 (+hs3, pk3) = rest
196 (K3, (Equal.trans(H.Walk, H.wk_go(2n+p, kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 2n+p), 2n+p)}), H.wk_go(1n+p, U32.sub(kk, 1), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+p), 1n+p)}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K3), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), 0n)}, Equal.cong(H.Walk, H.Walk, w => H.wk_go(1n+p, U32.sub(kk, 1), w), H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 2n+p), 2n+p)}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+p), 1n+p)}, e1), e2), (hs3, pk3)))
197
198def walk_s(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +p: Nat, +kk: U32, +KT: AR.Tree<String>, st: WStep(tabT, kl, k, sd, 1n+p, kk, KT), rec: @+K2: AR.Tree<String> -> @+hs2: {AR.slots(String, K2) == kl : List<&2, String>} -> @+pk2: {AR.perfect(String, sd, K2) == True{} : Bool} -> WalkOK(tabT, kl, k, sd, p, U32.sub(kk, 1), K2)) -> WalkOK(tabT, kl, k, sd, 1n+p, kk, KT):
199 match st:
200 case Tuple{+K2, Tuple{+e1, rest}}:
201 (+hs2, pk2) = rest
202 walk_s2(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, p, kk, KT, K2, e1, rec(K2, hs2, pk2))
203
204# THEOREM: the walk over buckets q, q - 1, .., 0 lists every key in bucket order
205def walk(+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}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> WalkOK(tabT, kl, k, sd, q, kk, KT):
206 match q:
207 case 0n:
208 walk_0(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, kk, KT, wstep(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, 0n, hq, kk, hkk, KT, hsl, pk))
209 case 1n+p:
210 +hle = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+p, UD.v(kk), Equal.sym(Nat, UD.v(kk), 1n+p, hkk), N.zero_le(p))
211 +hk2 = Equal.trans(Nat, UD.v(U32.sub(kk, 1)), Nat.sub(UD.v(kk), 1n), p, U.sub_nat(kk, 1, hle), Equal.trans(Nat, Nat.sub(UD.v(kk), 1n), Nat.sub(1n+p, 1n), p, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), UD.v(kk), 1n+p, hkk), N.sub_zero(p)))
212 walk_s(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, p, kk, KT, wstep(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, 1n+p, hq, kk, hkk, KT, hsl, pk), K2 => hs2 => pk2 => walk(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, p, N.lt_trans(p, 1n+p, SC.pow2(k), N.lt_succ(p), hq), U32.sub(kk, 1), hk2, K2, hs2, pk2))
213
214# ---- the operation ----
215
216def KeysOK(~V: Data, +sh: ST.Sh<V>, r: H.HashMap<&2, V> & List<&2, String>) -> Type:
217 Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.keys(~V, ST.model(~V, sh))) : H.HashMap<&2, V> & List<&2, String>} & ({ST.good(~V, sh2) == True{} : Bool} & {ST.model(~V, sh2) == ST.model(~V, sh) : List<&2, S.Entry<V>>})>
218
219
220def keys_w(~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}, wo: WalkOK(tabT, AR.slots(String, ksT), k, sd, UD.v(CY.msk(k)), CY.msk(k), ksT), +ew: {H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}) == H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k)))}) : H.Walk}) -> KeysOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, H.keys(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}))):
221 match wo:
222 case Tuple{+K2, Tuple{+e2, rest}}:
223 (+hs2, pk2) = rest
224 +kl = AR.slots(String, ksT)
225 +pkT = ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)
226 +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)
227 +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, hs2), 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))
228 +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, hs2)
229 +ek = Equal.sym(List<&2, String>, S.keys(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n), keys_absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), 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, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), SC.pow2(k), 0n, N.le_refl(SC.pow2(k))))
230 +ea = Equal.trans(H.Walk, H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k)))}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n)}, ew, e2)
231 +eb = Equal.cong(H.Walk, H.HashMap<&2, V> & List<&2, String>, w => H.keys_fin(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), w), H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n)}, ea)
232 +ec = Equal.cong(List<&2, String>, H.HashMap<&2, V> & List<&2, String>, z => (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), z), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n), S.keys(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})), ek)
233 (ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}, (Equal.trans(H.HashMap<&2, V> & List<&2, String>, H.keys(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})), (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n)), (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), S.keys(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}))), eb, ec), (g2, m2)))
234
235# THEOREM: keys lists the model's keys in order and keeps the map and its model
236def keys_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> KeysOK(~V, sh, H.keys(&2, V, ST.real(~V, sh))):
237 match sh:
238 case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:
239 +ck = ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)
240 +hk31 = L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ck)
241 +a0 = GR.mskv(k, N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==})))
242 +eq0 = Equal.trans(Nat, 1n+UD.v(CY.msk(k)), Nat.add(UD.v(CY.msk(k)), 1n), SC.pow2(k), Equal.sym(Nat, Nat.add(UD.v(CY.msk(k)), 1n), 1n+UD.v(CY.msk(k)), N.add_comm(UD.v(CY.msk(k)), 1n)), a0)
243 +hq0 = L.subst(Nat, z => {Nat.is_lt(UD.v(CY.msk(k)), z) == True{} : Bool}, 1n+UD.v(CY.msk(k)), SC.pow2(k), eq0, N.lt_succ(UD.v(CY.msk(k))))
244 +ef = Equal.trans(Nat, U32.to_nat(U32.inc(CY.msk(k))), SC.pow2(k), 1n+UD.v(CY.msk(k)), PA.fuel_eq(1n, {==}, k, hk31), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), eq0))
245 +esub = Equal.trans(Nat, Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), Nat.sub(1n+UD.v(CY.msk(k)), 1n+UD.v(CY.msk(k))), 0n, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n+UD.v(CY.msk(k))), SC.pow2(k), 1n+UD.v(CY.msk(k)), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), eq0)), N.sub_self(UD.v(CY.msk(k))))
246 +eacc = Equal.cong(Nat, List<&2, String>, z => kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), z, 1n+UD.v(CY.msk(k))), 0n, Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), Equal.sym(Nat, Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 0n, esub))
247 +ew = Equal.trans(H.Walk, H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k)))}), Equal.cong(Nat, H.Walk, f => H.wk_go(f, CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), U32.to_nat(U32.inc(CY.msk(k))), 1n+UD.v(CY.msk(k)), ef), Equal.cong(List<&2, String>, H.Walk, z => H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), z}), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), 0n, 1n+UD.v(CY.msk(k))), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k))), eacc))
248 keys_w(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, walk(1n, {==}, k, hk31, tabT, ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), AR.slots(String, ksT), sd, ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), AR.slots_length(String, sd, ksT, ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), UD.v(CY.msk(k)), hq0, CY.msk(k), {==}, ksT, {==}, ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ew)