1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/array.bend as AR
5	import ../../../spec/lib/common.bend as SC
6	import ../../../spec/containers/lru.bend as SP
7	import ../../lib/u32div.bend as UD
8	import ../../../src/math/u64.bend as W
9	import ../../../src/containers/lru.bend as LR
10	import ./state.bend as ST
11	import ./meta.bend as MT
12	import ./basic.bend as BA
13	import ../../lib/list.bend as LL
14	import ../../lib/words32.bend as W32
15	import ../../lib/u32_tree.bend as UT
16	
17	# bump: a counter's 64-bit increment in the meta words.
18	
19	
20	def BumpOK(+mT: AR.Tree<U32>, +i: Nat, r: Array<U32>) -> Type:
21	  Sigma<&1, &1, AR.Tree<U32>, m2 => {r == AR.thaw(U32, m2) : Array<U32>} & ({AR.perfect(U32, 5n, m2) == True{} : Bool} & ({ST.w64(AR.slots(U32, m2), i) == SP.inc64(ST.w64(AR.slots(U32, mT), i)) : W.U64} & Sigma<&1, &1, U32, x => Sigma<&1, &1, U32, y => {AR.slots(U32, m2) == SC.update(U32, SC.update(U32, AR.slots(U32, mT), i, x), 1n+i, y) : List<&2, U32>}>>))>
22	
23	
24	def lt_i(+i: Nat, +hi: {Nat.is_lt(1n+i, 32n) == True{} : Bool}) -> {Nat.is_lt(i, 32n) == True{} : Bool}:
25	  N.lt_trans(i, 1n+i, 32n, N.lt_succ(i), hi)
26	
27	def vlt(+x: U32, +i: Nat, +h: {UD.v(x) == i : Nat}, +hi: {Nat.is_lt(i, 32n) == True{} : Bool}) -> {Nat.is_lt(UD.v(x), SC.pow2(5n)) == True{} : Bool}:
28	  L.subst(Nat, z => {Nat.is_lt(z, 32n) == True{} : Bool}, i, UD.v(x), Equal.sym(Nat, UD.v(x), i, h), hi)
29	
30	def ne_si(+i: Nat) -> {Nat.is_eq(i, 1n+i) == False{} : Bool}:
31	  N.is_eq_lt(i, 1n+i, N.lt_succ(i))
32	
33	def s1_of(+mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +c: U32, +i: Nat, +hi: {Nat.is_lt(1n+i, 32n) == True{} : Bool}, +hI: {UD.v(U32.add(16, U32.shl(c))) == i : Nat}, +hJ: {UD.v(U32.add(17, U32.shl(c))) == 1n+i : Nat}) -> {AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))) == SC.update(U32, AR.slots(U32, mT), i, U32.inc(W32.nth0(AR.slots(U32, mT), i))) : List<&2, U32>}:
34	  +hIb = vlt(U32.add(16, U32.shl(c)), i, hI, lt_i(i, hi))
35	  Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), SC.update(U32, AR.slots(U32, mT), UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), SC.update(U32, AR.slots(U32, mT), i, U32.inc(W32.nth0(AR.slots(U32, mT), i))), UT.uset_s(5n, mT, pm, UD.v(U32.add(16, U32.shl(c))), hIb, U32.inc(W32.nth0(AR.slots(U32, mT), i))), Equal.cong(Nat, List<&2, U32>, z => SC.update(U32, AR.slots(U32, mT), z, U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(16, U32.shl(c))), i, hI))
36	
37	# writing a word's own value changes nothing
38	def upd_id(+xs: List<&2, U32>, +j: Nat) -> {SC.update(U32, xs, j, W32.nth0(xs, j)) == xs : List<&2, U32>}:
39	  match xs j:
40	    case Nil{} _:
41	      {==}
42	    case Con{+h, +t} 0n:
43	      {==}
44	    case Con{+h, +t} 1n+p:
45	      LL.cons_cong(U32, h, SC.update(U32, t, p, W32.nth0(t, p)), t, upd_id(t, p))
46	
47	# no wrap of the low word
48	def bump_nw(+mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +c: U32, +i: Nat, +hi: {Nat.is_lt(1n+i, 32n) == True{} : Bool}, +hI: {UD.v(U32.add(16, U32.shl(c))) == i : Nat}, +hJ: {UD.v(U32.add(17, U32.shl(c))) == 1n+i : Nat}, +hz: {U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0) == False{} : Bool}) -> BumpOK(mT, i, LR.bump_hi(Array.set(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(W32.nth0(AR.slots(U32, mT), i))), c, False{})):
49	  +hIb = vlt(U32.add(16, U32.shl(c)), i, hI, lt_i(i, hi))
50	  +a1 = UT.uset_a(5n, {==}, mT, pm, U32.add(16, U32.shl(c)), hIb, U32.inc(W32.nth0(AR.slots(U32, mT), i)))
51	  +p1 = UT.uset_p(5n, mT, pm, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))
52	  +s1 = s1_of(mT, pm, c, i, hi, hI, hJ)
53	  +e0 = MT.nth_same(5n, mT, pm, i, lt_i(i, hi), U32.inc(W32.nth0(AR.slots(U32, mT), i)), AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), s1)
54	  +e1 = MT.nth_other(mT, i, U32.inc(W32.nth0(AR.slots(U32, mT), i)), AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), s1, 1n+i, ne_si(i))
55	  +r = L.subst(Bool, z => {W.U64{U32.inc(W32.nth0(AR.slots(U32, mT), i)), W32.nth0(AR.slots(U32, mT), 1n+i)} == SP.inc_hi(U32.inc(W32.nth0(AR.slots(U32, mT), i)), W32.nth0(AR.slots(U32, mT), 1n+i), z) : W.U64}, False{}, U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0), Equal.sym(Bool, U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0), False{}, hz), {==})
56	  +ew = Equal.trans(W.U64, ST.w64(AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), i), W.U64{U32.inc(W32.nth0(AR.slots(U32, mT), i)), W32.nth0(AR.slots(U32, mT), 1n+i)}, SP.inc64(ST.w64(AR.slots(U32, mT), i)), BA.w64_eq_l(AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), i, U32.inc(W32.nth0(AR.slots(U32, mT), i)), W32.nth0(AR.slots(U32, mT), 1n+i), e0, e1), r)
57	  +U = SC.update(U32, AR.slots(U32, mT), i, U32.inc(W32.nth0(AR.slots(U32, mT), i)))
58	  +eu = Equal.trans(List<&2, U32>, SC.update(U32, U, 1n+i, W32.nth0(AR.slots(U32, mT), 1n+i)), SC.update(U32, U, 1n+i, W32.nth0(U, 1n+i)), U, Equal.cong(U32, List<&2, U32>, z => SC.update(U32, U, 1n+i, z), W32.nth0(AR.slots(U32, mT), 1n+i), W32.nth0(U, 1n+i), Equal.sym(U32, W32.nth0(U, 1n+i), W32.nth0(AR.slots(U32, mT), 1n+i), W32.nth0_upd_other(AR.slots(U32, mT), i, 1n+i, U32.inc(W32.nth0(AR.slots(U32, mT), i)), ne_si(i)))), upd_id(U, 1n+i))
59	  (AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), (a1, (p1, (ew, (U32.inc(W32.nth0(AR.slots(U32, mT), i)), (W32.nth0(AR.slots(U32, mT), 1n+i), Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), U, SC.update(U32, U, 1n+i, W32.nth0(AR.slots(U32, mT), 1n+i)), s1, Equal.sym(List<&2, U32>, SC.update(U32, U, 1n+i, W32.nth0(AR.slots(U32, mT), 1n+i)), U, eu))))))))
60	
61	# the low word wraps: the high word is incremented too
62	def bump_w(+mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +c: U32, +i: Nat, +hi: {Nat.is_lt(1n+i, 32n) == True{} : Bool}, +hI: {UD.v(U32.add(16, U32.shl(c))) == i : Nat}, +hJ: {UD.v(U32.add(17, U32.shl(c))) == 1n+i : Nat}, +hz: {U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0) == True{} : Bool}) -> BumpOK(mT, i, LR.bump_hi(Array.set(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(W32.nth0(AR.slots(U32, mT), i))), c, True{})):
63	  +hIb = vlt(U32.add(16, U32.shl(c)), i, hI, lt_i(i, hi))
64	  +hJb = vlt(U32.add(17, U32.shl(c)), 1n+i, hJ, hi)
65	  +a1 = UT.uset_a(5n, {==}, mT, pm, U32.add(16, U32.shl(c)), hIb, U32.inc(W32.nth0(AR.slots(U32, mT), i)))
66	  +p1 = UT.uset_p(5n, mT, pm, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))
67	  +s1 = s1_of(mT, pm, c, i, hi, hI, hJ)
68	  +g1 = L.subst(Nat, z => {Array.get(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), U32.add(17, U32.shl(c))) == (AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), z)) : Array<U32> & U32}, UD.v(U32.add(17, U32.shl(c))), 1n+i, hJ, UT.uget(5n, {==}, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), p1, U32.add(17, U32.shl(c)), hJb))
69	  +eh = MT.nth_other(mT, i, U32.inc(W32.nth0(AR.slots(U32, mT), i)), AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), s1, 1n+i, ne_si(i))
70	  +g2 = Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), U32.add(17, U32.shl(c))), (AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), 1n+i)), (AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), W32.nth0(AR.slots(U32, mT), 1n+i)), g1, Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), z), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), 1n+i), W32.nth0(AR.slots(U32, mT), 1n+i), eh))
71	  +a2 = UT.uset_a(5n, {==}, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), p1, U32.add(17, U32.shl(c)), hJb, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))
72	  +p2 = UT.uset_p(5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), p1, UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))
73	  +s2 = Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), 1n+i, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), UT.uset_s(5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), p1, UD.v(U32.add(17, U32.shl(c))), hJb, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), Equal.cong(Nat, List<&2, U32>, z => SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), z, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), UD.v(U32.add(17, U32.shl(c))), 1n+i, hJ))
74	  +ea = Equal.trans(Array<U32>, LR.bump_hi_go(U32.add(17, U32.shl(c)), Array.get(U32, Array.set(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(W32.nth0(AR.slots(U32, mT), i))), U32.add(17, U32.shl(c)))), LR.bump_hi_go(U32.add(17, U32.shl(c)), (AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), W32.nth0(AR.slots(U32, mT), 1n+i))), AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))), Equal.trans(Array<U32>, LR.bump_hi_go(U32.add(17, U32.shl(c)), Array.get(U32, Array.set(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(W32.nth0(AR.slots(U32, mT), i))), U32.add(17, U32.shl(c)))), LR.bump_hi_go(U32.add(17, U32.shl(c)), Array.get(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), U32.add(17, U32.shl(c)))), LR.bump_hi_go(U32.add(17, U32.shl(c)), (AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), W32.nth0(AR.slots(U32, mT), 1n+i))), Equal.cong(Array<U32>, Array<U32>, z => LR.bump_hi_go(U32.add(17, U32.shl(c)), Array.get(U32, z, U32.add(17, U32.shl(c)))), Array.set(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(W32.nth0(AR.slots(U32, mT), i))), AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), a1), Equal.cong(Array<U32> & U32, Array<U32>, z => LR.bump_hi_go(U32.add(17, U32.shl(c)), z), Array.get(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), U32.add(17, U32.shl(c))), (AR.thaw(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), W32.nth0(AR.slots(U32, mT), 1n+i)), g2)), a2)
75	  +e0 = Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))), i), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), i), U32.inc(W32.nth0(AR.slots(U32, mT), i)), MT.nth_other(AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), 1n+i, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), s2, i, N.is_eq_sym_false(i, 1n+i, ne_si(i))), MT.nth_same(5n, mT, pm, i, lt_i(i, hi), U32.inc(W32.nth0(AR.slots(U32, mT), i)), AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), s1))
76	  +e1 = MT.nth_same(5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), p1, 1n+i, hi, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), s2)
77	  +r = L.subst(Bool, z => {W.U64{U32.inc(W32.nth0(AR.slots(U32, mT), i)), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))} == SP.inc_hi(U32.inc(W32.nth0(AR.slots(U32, mT), i)), W32.nth0(AR.slots(U32, mT), 1n+i), z) : W.U64}, True{}, U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0), Equal.sym(Bool, U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0), True{}, hz), {==})
78	  +ew = Equal.trans(W.U64, ST.w64(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))), i), W.U64{U32.inc(W32.nth0(AR.slots(U32, mT), i)), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))}, SP.inc64(ST.w64(AR.slots(U32, mT), i)), BA.w64_eq_l(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))), i, U32.inc(W32.nth0(AR.slots(U32, mT), i)), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)), e0, e1), r)
79	  (AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), (ea, (p2, (ew, (U32.inc(W32.nth0(AR.slots(U32, mT), i)), (U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)), Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i))), UD.v(U32.add(17, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i)))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), 1n+i, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), i, U32.inc(W32.nth0(AR.slots(U32, mT), i))), 1n+i, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), s2, Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, 1n+i, U32.inc(W32.nth0(AR.slots(U32, mT), 1n+i))), AR.slots(U32, AR.upd(U32, 5n, mT, UD.v(U32.add(16, U32.shl(c))), U32.inc(W32.nth0(AR.slots(U32, mT), i)))), SC.update(U32, AR.slots(U32, mT), i, U32.inc(W32.nth0(AR.slots(U32, mT), i))), s1))))))))
80	
81	def bump_c(+mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +c: U32, +i: Nat, +hi: {Nat.is_lt(1n+i, 32n) == True{} : Bool}, +hI: {UD.v(U32.add(16, U32.shl(c))) == i : Nat}, +hJ: {UD.v(U32.add(17, U32.shl(c))) == 1n+i : Nat}, +z: Bool, +hz: {U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0) == z : Bool}) -> BumpOK(mT, i, LR.bump_hi(Array.set(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c)), U32.inc(W32.nth0(AR.slots(U32, mT), i))), c, z)):
82	  match z:
83	    case False{}:
84	      bump_nw(mT, pm, c, i, hi, hI, hJ, hz)
85	    case True{}:
86	      bump_w(mT, pm, c, i, hi, hI, hJ, hz)
87	
88	# THEOREM (bump): counter c's words i, i + 1 become the 64-bit increment of
89	# their value; every other meta word is kept.
90	def bump_ok(+mT: AR.Tree<U32>, +pm: {AR.perfect(U32, 5n, mT) == True{} : Bool}, +c: U32, +i: Nat, +hi: {Nat.is_lt(1n+i, 32n) == True{} : Bool}, +hI: {UD.v(U32.add(16, U32.shl(c))) == i : Nat}, +hJ: {UD.v(U32.add(17, U32.shl(c))) == 1n+i : Nat}) -> BumpOK(mT, i, LR.bump(c, AR.thaw(U32, mT))):
91	  +hIb = vlt(U32.add(16, U32.shl(c)), i, hI, lt_i(i, hi))
92	  +g = L.subst(Nat, z => {Array.get(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c))) == (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), z)) : Array<U32> & U32}, UD.v(U32.add(16, U32.shl(c))), i, hI, UT.uget(5n, {==}, mT, pm, U32.add(16, U32.shl(c)), hIb))
93	  +E = Equal.cong(Array<U32> & U32, Array<U32>, r => LR.bump_lo(c, r), Array.get(U32, AR.thaw(U32, mT), U32.add(16, U32.shl(c))), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), i)), g)
94	  L.subst(Array<U32>, r => BumpOK(mT, i, r), LR.bump_lo(c, (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), i))), LR.bump(c, AR.thaw(U32, mT)), Equal.sym(Array<U32>, LR.bump(c, AR.thaw(U32, mT)), LR.bump_lo(c, (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), i))), E), bump_c(mT, pm, c, i, hi, hI, hJ, U32.is_eq(U32.inc(W32.nth0(AR.slots(U32, mT), i)), 0), {==}))