proofs/containers/lru/dll.bend
bend-collections-laws-containers@1.0.0.0 · 188 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
8import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
17
18# The recency and free lists under writes to lk: reads after a write, frame
19# lemmas, and re-targeting a segment's ends.
20
21
22# ---- Bool helpers ----
23
24
25
26
27
28
29
30
31# ---- reads after a write ----
32
33def lw_same(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h: {Nat.is_lt(ST.off(y, o), SC.length(U32, ll)) == True{} : Bool}) -> {ST.lw(SC.update(U32, ll, ST.off(y, o), v), y, o) == v : U32}:
34 W32.nth0_upd_same(ll, ST.off(y, o), v, h)
35
36def lw_other(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +x: Nat, +o2: Nat, +ho2: {Nat.is_lt(o2, 8n) == True{} : Bool}, +hne: {Bool.or(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2))) == True{} : Bool}) -> {ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, o2) == ST.lw(ll, x, o2) : U32}:
37 W32.nth0_upd_other(ll, ST.off(y, o), ST.off(x, o2), v, ID.off_ne(y, x, o, o2, ho, ho2, hne))
38
39def ne_slot(+y: Nat, +x: Nat, +o: Nat, +o2: Nat, +h: {Nat.is_eq(y, x) == False{} : Bool}) -> {Bool.or(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2))) == True{} : Bool}:
40 NL.or_tl(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2)), NL.not_f(Nat.is_eq(y, x), h))
41
42def ne_word(+y: Nat, +x: Nat, +o: Nat, +o2: Nat, +h: {Nat.is_eq(o, o2) == False{} : Bool}) -> {Bool.or(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2))) == True{} : Bool}:
43 NL.or_tr(Bool.not(Nat.is_eq(y, x)), Bool.not(Nat.is_eq(o, o2)), NL.not_f(Nat.is_eq(o, o2), h))
44
45# a link word (o < 2) is not a data word (2 <= o2)
46def lo_hi(+o: Nat, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +o2: Nat, +h2: {Nat.is_le(2n, o2) == True{} : Bool}) -> {Nat.is_eq(o, o2) == False{} : Bool}:
47 N.is_eq_lt(o, o2, N.lt_le_trans(o, 2n, o2, h01, h2))
48
49# y differs from x
50
51# ---- segments ----
52
53def seg_c(+l1: List<&2, U32>, +l2: List<&2, U32>, +s: Nat, +t: List<&2, Nat>, +p: U32, +q: U32, +e0: {ST.lw(l1, s, 0n) == ST.lw(l2, s, 0n) : U32}, +e1: {ST.lw(l1, s, 1n) == ST.lw(l2, s, 1n) : U32}, +ec: {ST.seg(l1, t, LK.lnk(s), q) == ST.seg(l2, t, LK.lnk(s), q) : Bool}) -> {ST.seg(l1, Con{s, t}, p, q) == ST.seg(l2, Con{s, t}, p, q) : Bool}:
54 +r1 = L.subst(U32, z => {Bool.and(U32.is_eq(z, p), Bool.and(U32.is_eq(ST.lw(l2, s, 1n), LK.fst_or(t, q)), ST.seg(l2, t, LK.lnk(s), q))) == ST.seg(l2, Con{s, t}, p, q) : Bool}, ST.lw(l2, s, 0n), ST.lw(l1, s, 0n), Equal.sym(U32, ST.lw(l1, s, 0n), ST.lw(l2, s, 0n), e0), {==})
55 +r2 = L.subst(U32, z => {Bool.and(U32.is_eq(ST.lw(l1, s, 0n), p), Bool.and(U32.is_eq(z, LK.fst_or(t, q)), ST.seg(l2, t, LK.lnk(s), q))) == ST.seg(l2, Con{s, t}, p, q) : Bool}, ST.lw(l2, s, 1n), ST.lw(l1, s, 1n), Equal.sym(U32, ST.lw(l1, s, 1n), ST.lw(l2, s, 1n), e1), r1)
56 L.subst(Bool, z => {Bool.and(U32.is_eq(ST.lw(l1, s, 0n), p), Bool.and(U32.is_eq(ST.lw(l1, s, 1n), LK.fst_or(t, q)), z)) == ST.seg(l2, Con{s, t}, p, q) : Bool}, ST.seg(l2, t, LK.lnk(s), q), ST.seg(l1, t, LK.lnk(s), q), Equal.sym(Bool, ST.seg(l1, t, LK.lnk(s), q), ST.seg(l2, t, LK.lnk(s), q), ec), r2)
57
58# a write to a slot off the segment leaves it
59def seg_fs(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +sl: List<&2, Nat>, +p: U32, +q: U32, +hy: {NL.memn(y, sl) == False{} : Bool}) -> {ST.seg(SC.update(U32, ll, ST.off(y, o), v), sl, p, q) == ST.seg(ll, sl, p, q) : Bool}:
60 match sl:
61 case Nil{}:
62 {==}
63 case Con{+s, +t}:
64 +hys = NL.ne_sym(s, y, NL.or_ff_l(Nat.is_eq(s, y), NL.memn(y, t), hy))
65 seg_c(SC.update(U32, ll, ST.off(y, o), v), ll, s, t, p, q, lw_other(ll, y, o, v, ho, s, 0n, {==}, ne_slot(y, s, o, 0n, hys)), lw_other(ll, y, o, v, ho, s, 1n, {==}, ne_slot(y, s, o, 1n, hys)), seg_fs(ll, y, o, v, ho, t, LK.lnk(s), q, NL.or_ff_r(Nat.is_eq(s, y), NL.memn(y, t), hy)))
66
67
68
69# a segment splits at an append
70def seg_app(+ll: List<&2, U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +p: U32, +q: U32) -> {ST.seg(ll, SC.append(Nat, a, b), p, q) == Bool.and(ST.seg(ll, a, p, LK.fst_or(b, q)), ST.seg(ll, b, LK.last_or(a, p), q)) : Bool}:
71 match a:
72 case Nil{}:
73 {==}
74 case Con{+h, +t}:
75 +E0 = U32.is_eq(ST.lw(ll, h, 0n), p)
76 +F = LK.fst_or(b, q)
77 +Y = ST.seg(ll, t, LK.lnk(h), F)
78 +Z = ST.seg(ll, b, LK.last_or(t, LK.lnk(h)), q)
79 +e1 = Equal.cong(U32, Bool, z => Bool.and(E0, Bool.and(U32.is_eq(ST.lw(ll, h, 1n), z), ST.seg(ll, SC.append(Nat, t, b), LK.lnk(h), q))), LK.fst_or(SC.append(Nat, t, b), q), LK.fst_or(t, F), LK.fst_app(t, b, q))
80 +e2 = Equal.cong(Bool, Bool, z => Bool.and(E0, Bool.and(U32.is_eq(ST.lw(ll, h, 1n), LK.fst_or(t, F)), z)), ST.seg(ll, SC.append(Nat, t, b), LK.lnk(h), q), Bool.and(Y, Z), seg_app(ll, t, b, LK.lnk(h), q))
81 Equal.trans(Bool, ST.seg(ll, SC.append(Nat, Con{h, t}, b), p, q), Bool.and(E0, Bool.and(U32.is_eq(ST.lw(ll, h, 1n), LK.fst_or(t, F)), ST.seg(ll, SC.append(Nat, t, b), LK.lnk(h), q))), Bool.and(Bool.and(E0, Bool.and(U32.is_eq(ST.lw(ll, h, 1n), LK.fst_or(t, F)), Y)), Z), e1, Equal.trans(Bool, Bool.and(E0, Bool.and(U32.is_eq(ST.lw(ll, h, 1n), LK.fst_or(t, F)), ST.seg(ll, SC.append(Nat, t, b), LK.lnk(h), q))), Bool.and(E0, Bool.and(U32.is_eq(ST.lw(ll, h, 1n), LK.fst_or(t, F)), Bool.and(Y, Z))), Bool.and(Bool.and(E0, Bool.and(U32.is_eq(ST.lw(ll, h, 1n), LK.fst_or(t, F)), Y)), Z), e2, NL.and3(E0, U32.is_eq(ST.lw(ll, h, 1n), LK.fst_or(t, F)), Y, Z)))
82
83# the last slot of a, t after a
84
85
86
87
88# a member differs from a non-member
89
90# re-target the last slot's next
91def segq(+ll: List<&2, U32>, +t: List<&2, Nat>, +a: Nat, +p: U32, +x: U32, +y: U32, +hs: {ST.seg(ll, Con{a, t}, p, x) == True{} : Bool}, +hn: {NL.nodupn(Con{a, t}) == True{} : Bool}, +hl: {Nat.is_lt(ST.off(NL.lastn(t, a), 1n), SC.length(U32, ll)) == True{} : Bool}) -> {ST.seg(SC.update(U32, ll, ST.off(NL.lastn(t, a), 1n), y), Con{a, t}, p, y) == True{} : Bool}:
92 match t:
93 case Nil{}:
94 +e0 = lw_other(ll, a, 1n, y, {==}, a, 0n, {==}, ne_word(a, a, 1n, 0n, {==}))
95 +h0 = L.and_left(U32.is_eq(ST.lw(ll, a, 0n), p), Bool.and(U32.is_eq(ST.lw(ll, a, 1n), x), True{}), hs)
96 +h0b = L.subst(U32, z => {U32.is_eq(z, p) == True{} : Bool}, ST.lw(ll, a, 0n), ST.lw(SC.update(U32, ll, ST.off(a, 1n), y), a, 0n), Equal.sym(U32, ST.lw(SC.update(U32, ll, ST.off(a, 1n), y), a, 0n), ST.lw(ll, a, 0n), e0), h0)
97 +h1b = L.subst(U32, z => {U32.is_eq(z, y) == True{} : Bool}, y, ST.lw(SC.update(U32, ll, ST.off(a, 1n), y), a, 1n), Equal.sym(U32, ST.lw(SC.update(U32, ll, ST.off(a, 1n), y), a, 1n), y, lw_same(ll, a, 1n, y, {==}, hl)), LK.u_refl(y))
98 L.and_intro(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(a, 1n), y), a, 0n), p), Bool.and(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(a, 1n), y), a, 1n), y), True{}), h0b, L.and_intro(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(a, 1n), y), a, 1n), y), True{}, h1b, {==}))
99 case Con{+b, +t2}:
100 +z = NL.lastn(t2, b)
101 +hna = L.and_left(Bool.not(NL.memn(a, Con{b, t2})), NL.nodupn(Con{b, t2}), hn)
102 +hza = NL.ne_mem(a, z, Con{b, t2}, hna, NL.lastn_mem(t2, b))
103 +e0 = lw_other(ll, z, 1n, y, {==}, a, 0n, {==}, ne_slot(z, a, 1n, 0n, hza))
104 +e1 = lw_other(ll, z, 1n, y, {==}, a, 1n, {==}, ne_slot(z, a, 1n, 1n, hza))
105 +h0 = L.and_left(U32.is_eq(ST.lw(ll, a, 0n), p), Bool.and(U32.is_eq(ST.lw(ll, a, 1n), LK.lnk(b)), ST.seg(ll, Con{b, t2}, LK.lnk(a), x)), hs)
106 +hr = L.and_right(U32.is_eq(ST.lw(ll, a, 0n), p), Bool.and(U32.is_eq(ST.lw(ll, a, 1n), LK.lnk(b)), ST.seg(ll, Con{b, t2}, LK.lnk(a), x)), hs)
107 +h1 = L.and_left(U32.is_eq(ST.lw(ll, a, 1n), LK.lnk(b)), ST.seg(ll, Con{b, t2}, LK.lnk(a), x), hr)
108 +hst = L.and_right(U32.is_eq(ST.lw(ll, a, 1n), LK.lnk(b)), ST.seg(ll, Con{b, t2}, LK.lnk(a), x), hr)
109 +h0b = L.subst(U32, w => {U32.is_eq(w, p) == True{} : Bool}, ST.lw(ll, a, 0n), ST.lw(SC.update(U32, ll, ST.off(z, 1n), y), a, 0n), Equal.sym(U32, ST.lw(SC.update(U32, ll, ST.off(z, 1n), y), a, 0n), ST.lw(ll, a, 0n), e0), h0)
110 +h1b = L.subst(U32, w => {U32.is_eq(w, LK.lnk(b)) == True{} : Bool}, ST.lw(ll, a, 1n), ST.lw(SC.update(U32, ll, ST.off(z, 1n), y), a, 1n), Equal.sym(U32, ST.lw(SC.update(U32, ll, ST.off(z, 1n), y), a, 1n), ST.lw(ll, a, 1n), e1), h1)
111 L.and_intro(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(z, 1n), y), a, 0n), p), Bool.and(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(z, 1n), y), a, 1n), LK.lnk(b)), ST.seg(SC.update(U32, ll, ST.off(z, 1n), y), Con{b, t2}, LK.lnk(a), y)), h0b, L.and_intro(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(z, 1n), y), a, 1n), LK.lnk(b)), ST.seg(SC.update(U32, ll, ST.off(z, 1n), y), Con{b, t2}, LK.lnk(a), y), h1b, segq(ll, t2, b, LK.lnk(a), x, y, hst, L.and_right(Bool.not(NL.memn(a, Con{b, t2})), NL.nodupn(Con{b, t2}), hn), hl)))
112
113# re-target the first slot's prev
114def segp(+ll: List<&2, U32>, +b: Nat, +t: List<&2, Nat>, +x: U32, +q: U32, +y: U32, +hs: {ST.seg(ll, Con{b, t}, x, q) == True{} : Bool}, +hn: {NL.nodupn(Con{b, t}) == True{} : Bool}, +hl: {Nat.is_lt(ST.off(b, 0n), SC.length(U32, ll)) == True{} : Bool}) -> {ST.seg(SC.update(U32, ll, ST.off(b, 0n), y), Con{b, t}, y, q) == True{} : Bool}:
115 +l2 = SC.update(U32, ll, ST.off(b, 0n), y)
116 +hr = L.and_right(U32.is_eq(ST.lw(ll, b, 0n), x), Bool.and(U32.is_eq(ST.lw(ll, b, 1n), LK.fst_or(t, q)), ST.seg(ll, t, LK.lnk(b), q)), hs)
117 +h1 = L.and_left(U32.is_eq(ST.lw(ll, b, 1n), LK.fst_or(t, q)), ST.seg(ll, t, LK.lnk(b), q), hr)
118 +hst = L.and_right(U32.is_eq(ST.lw(ll, b, 1n), LK.fst_or(t, q)), ST.seg(ll, t, LK.lnk(b), q), hr)
119 +hbt = L.not_true(NL.memn(b, t), L.and_left(Bool.not(NL.memn(b, t)), NL.nodupn(t), hn))
120 +h0b = L.subst(U32, w => {U32.is_eq(w, y) == True{} : Bool}, y, ST.lw(l2, b, 0n), Equal.sym(U32, ST.lw(l2, b, 0n), y, lw_same(ll, b, 0n, y, {==}, hl)), LK.u_refl(y))
121 +h1b = L.subst(U32, w => {U32.is_eq(w, LK.fst_or(t, q)) == True{} : Bool}, ST.lw(ll, b, 1n), ST.lw(l2, b, 1n), Equal.sym(U32, ST.lw(l2, b, 1n), ST.lw(ll, b, 1n), lw_other(ll, b, 0n, y, {==}, b, 1n, {==}, ne_word(b, b, 0n, 1n, {==}))), h1)
122 +hstb = L.subst(Bool, w => {w == True{} : Bool}, ST.seg(ll, t, LK.lnk(b), q), ST.seg(l2, t, LK.lnk(b), q), Equal.sym(Bool, ST.seg(l2, t, LK.lnk(b), q), ST.seg(ll, t, LK.lnk(b), q), seg_fs(ll, b, 0n, y, {==}, t, LK.lnk(b), q, hbt)), hst)
123 L.and_intro(U32.is_eq(ST.lw(l2, b, 0n), y), Bool.and(U32.is_eq(ST.lw(l2, b, 1n), LK.fst_or(t, q)), ST.seg(l2, t, LK.lnk(b), q)), h0b, L.and_intro(U32.is_eq(ST.lw(l2, b, 1n), LK.fst_or(t, q)), ST.seg(l2, t, LK.lnk(b), q), h1b, hstb))
124
125# ---- the free list ----
126
127def fll_fs(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +fl: List<&2, Nat>, +hy: {NL.memn(y, fl) == False{} : Bool}) -> {ST.fll(SC.update(U32, ll, ST.off(y, o), v), fl) == ST.fll(ll, fl) : Bool}:
128 match fl:
129 case Nil{}:
130 {==}
131 case Con{+s, +t}:
132 +hys = NL.ne_sym(s, y, NL.or_ff_l(Nat.is_eq(s, y), NL.memn(y, t), hy))
133 +e1 = lw_other(ll, y, o, v, ho, s, 1n, {==}, ne_slot(y, s, o, 1n, hys))
134 +ih = fll_fs(ll, y, o, v, ho, t, NL.or_ff_r(Nat.is_eq(s, y), NL.memn(y, t), hy))
135 +r1 = L.subst(U32, z => {Bool.and(U32.is_eq(z, LK.fst_or(t, 0)), ST.fll(ll, t)) == ST.fll(ll, Con{s, t}) : Bool}, ST.lw(ll, s, 1n), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 1n), Equal.sym(U32, ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 1n), ST.lw(ll, s, 1n), e1), {==})
136 L.subst(Bool, z => {Bool.and(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 1n), LK.fst_or(t, 0)), z) == ST.fll(ll, Con{s, t}) : Bool}, ST.fll(ll, t), ST.fll(SC.update(U32, ll, ST.off(y, o), v), t), Equal.sym(Bool, ST.fll(SC.update(U32, ll, ST.off(y, o), v), t), ST.fll(ll, t), ih), r1)
137
138# ---- data words: writes to link words (o < 2) leave them ----
139
140
141def lw_hi(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +x: Nat, +o2: Nat, +ho2: {Nat.is_lt(o2, 8n) == True{} : Bool}, +h2: {Nat.is_le(2n, o2) == True{} : Bool}) -> {ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, o2) == ST.lw(ll, x, o2) : U32}:
142 lw_other(ll, y, o, v, ho, x, o2, ho2, ne_word(y, x, o, o2, lo_hi(o, h01, o2, h2)))
143
144def skey_fr(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +kl: List<&2, String>, +x: Nat) -> {ST.skey(SC.update(U32, ll, ST.off(y, o), v), kl, x) == ST.skey(ll, kl, x) : String}:
145 Equal.cong(U32, String, z => TB.keyof(z, TB.nths(kl, x)), ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 2n), ST.lw(ll, x, 2n), lw_hi(ll, y, o, v, ho, h01, x, 2n, {==}, {==}))
146
147def sent_fr(~V: Data, +ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +kl: List<&2, String>, +x: Nat, +m: Maybe<&2, V>) -> {ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, m) == ST.sent_m(~V, ll, kl, x, m) : List<&2, SP.Ent<V>>}:
148 match m:
149 case None{}:
150 {==}
151 case Some{+w}:
152 +r1 = L.subst(String, z => {Con{SP.LE{z, w, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 3n), W.U64{ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 4n), ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.skey(SC.update(U32, ll, ST.off(y, o), v), kl, x), ST.skey(ll, kl, x), skey_fr(ll, y, o, v, ho, h01, kl, x), {==})
153 +r2 = L.subst(U32, z => {Con{SP.LE{ST.skey(ll, kl, x), w, z, W.U64{ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 4n), ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 3n), ST.lw(ll, x, 3n), lw_hi(ll, y, o, v, ho, h01, x, 3n, {==}, {==}), r1)
154 +r3 = L.subst(U32, z => {Con{SP.LE{ST.skey(ll, kl, x), w, ST.lw(ll, x, 3n), W.U64{z, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 4n), ST.lw(ll, x, 4n), lw_hi(ll, y, o, v, ho, h01, x, 4n, {==}, {==}), r2)
155 +r4 = L.subst(U32, z => {Con{SP.LE{ST.skey(ll, kl, x), w, ST.lw(ll, x, 3n), W.U64{ST.lw(ll, x, 4n), z}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n), ST.lw(ll, x, 5n), lw_hi(ll, y, o, v, ho, h01, x, 5n, {==}, {==}), r3)
156 Equal.sym(List<&2, SP.Ent<V>>, ST.sent_m(~V, ll, kl, x, Some{w}), ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}), r4)
157
158def es_fr(~V: Data, +ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +sl: List<&2, Nat>) -> {ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, sl) == ST.es(~V, ll, kl, el, sl) : List<&2, SP.Ent<V>>}:
159 match sl:
160 case Nil{}:
161 {==}
162 case Con{+s, +t}:
163 +m = HT.nthm(~V, el, s)
164 +a = Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, z, ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t)), ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, s, m), ST.sent_m(~V, ll, kl, s, m), sent_fr(~V, ll, y, o, v, ho, h01, kl, s, m))
165 Equal.trans(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, s, m), ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t)), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t)), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), ST.es(~V, ll, kl, el, t)), a, Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), z), ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t), ST.es(~V, ll, kl, el, t), es_fr(~V, ll, y, o, v, ho, h01, kl, el, t)))
166
167def has_fr(~V: Data, +ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +bs: List<&2, B.Bk>, +m: Nat, +sl: List<&2, Nat>) -> {ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), sl) == ST.hasall(~V, bs, m, ll, sl) : Bool}:
168 match sl:
169 case Nil{}:
170 {==}
171 case Con{+s, +t}:
172 +e = Equal.cong(U32, Bool, z => ST.anyb(bs, m, LK.lnk(s), z), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 2n), ST.lw(ll, s, 2n), lw_hi(ll, y, o, v, ho, h01, s, 2n, {==}, {==}))
173 Equal.trans(Bool, Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 2n)), ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t)), Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t)), Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, bs, m, ll, t)), Equal.cong(Bool, Bool, z => Bool.and(z, ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t)), ST.anyb(bs, m, LK.lnk(s), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 2n)), ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), e), Equal.cong(Bool, Bool, z => Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), z), ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t), ST.hasall(~V, bs, m, ll, t), has_fr(~V, ll, y, o, v, ho, h01, bs, m, t)))
174
175def bslb_fr(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +sl: List<&2, Nat>, +b: B.Bk) -> {ST.bslb(sl, SC.update(U32, ll, ST.off(y, o), v), b) == ST.bslb(sl, ll, b) : Bool}:
176 match b:
177 case B.BE{}:
178 {==}
179 case B.BF{+w, +l, +k}:
180 Equal.cong(U32, Bool, z => Bool.and(NL.memn(UD.v(H.slot(l)), sl), U32.is_eq(z, w)), ST.lw(SC.update(U32, ll, ST.off(y, o), v), UD.v(H.slot(l)), 2n), ST.lw(ll, UD.v(H.slot(l)), 2n), lw_hi(ll, y, o, v, ho, h01, UD.v(H.slot(l)), 2n, {==}, {==}))
181
182def bsl_fr(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h01: {Nat.is_lt(o, 2n) == True{} : Bool}, +bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +m: Nat) -> {ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), m) == ST.bsl(bs, sl, ll, m) : Bool}:
183 match m:
184 case 0n:
185 {==}
186 case 1n+j:
187 Equal.trans(Bool, Bool.and(ST.bslb(sl, SC.update(U32, ll, ST.off(y, o), v), B.at(bs, j)), ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j)), Bool.and(ST.bslb(sl, ll, B.at(bs, j)), ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j)), Bool.and(ST.bslb(sl, ll, B.at(bs, j)), ST.bsl(bs, sl, ll, j)), Equal.cong(Bool, Bool, z => Bool.and(z, ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j)), ST.bslb(sl, SC.update(U32, ll, ST.off(y, o), v), B.at(bs, j)), ST.bslb(sl, ll, B.at(bs, j)), bslb_fr(ll, y, o, v, ho, h01, sl, B.at(bs, j))), Equal.cong(Bool, Bool, z => Bool.and(ST.bslb(sl, ll, B.at(bs, j)), z), ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j), ST.bsl(bs, sl, ll, j), bsl_fr(ll, y, o, v, ho, h01, bs, sl, j)))
188