1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../spec/containers/lru.bend as SP
6	import ../../lib/u32div.bend as UD
7	import ../../../src/math/u64.bend as W
8	import ../../../src/containers/hash_table.bend as H
9	import ../hash_table/table.bend as TB
10	import ../hash_table/buckets.bend as B
11	import ../hash_table/state.bend as HT
12	import ./state.bend as ST
13	import ./idx.bend as ID
14	import ../../lib/nat_list.bend as NL
15	import ../../lib/links.bend as LK
16	import ../../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	
33	def 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	
36	def 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	
39	def 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	
42	def 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)
46	def 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	
53	def 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
59	def 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
70	def 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
91	def 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
114	def 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	
127	def 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	
141	def 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	
144	def 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	
147	def 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	
158	def 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	
167	def 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	
175	def 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	
182	def 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