1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/math/generic.bend as SG
4	import ../../../spec/math/fixed.bend as SF
5	import ../../../src/math/w64.bend as X
6	import ../../../src/math/u64.bend as WU
7	import ../../../src/math/fixed.bend as F
8	import ../../lib/nat.bend as N
9	import ../../lib/logic.bend as L
10	import ../../lib/list.bend as LL
11	import ../../lib/u32.bend as U3
12	import ../../lib/u32div.bend as UD
13	import ./width.bend as WW
14	import ./w64add.bend as WA
15	import ./w64sh.bend as SH
16	import ./shrn.bend as SHN
17	import ./u32laws.bend as LW
18	import ./fixgen.bend as G
19	import ./fix32.bend as P32
20	
21	# to_bytes / from_bytes (Python int.to_bytes / int.from_bytes, Rust
22	# to_le_bytes / from_le_bytes) for U32 and U64 against spec/math/fixed.bend:
23	# byte k is the base-256 digit low(8, high(8k, x)); parsing is Horner's
24	# rule b0 + 256 (b1 + 256 (...)) with every partial value bounded by
25	# 2^(8j), so no step overflows; digits split at any byte boundary
26	# (Mathlib Nat.digits_append).
27	
28	def v(+x: U32) -> Nat:
29	  U32.to_nat(x)
30	
31	def con_eq(+x: Nat, +y: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>, +ex: {x == y : Nat}, +ets: {xs == ys : List<&2, Nat>}) -> {Con{x, xs} == Con{y, ys} : List<&2, Nat>}:
32	  Equal.trans(List<&2, Nat>, Con{x, xs}, Con{y, xs}, Con{y, ys}, Equal.cong(Nat, List<&2, Nat>, t => Con{t, xs}, x, y, ex), Equal.cong(List<&2, Nat>, List<&2, Nat>, t => Con{y, t}, xs, ys, ets))
33	
34	# ---- to_bytes ----
35	
36	def byte_v(+x: U32, +k: Nat) -> {v(F.byte32(x, k)) == C.low(8n, C.high(Nat.mul(8n, k), v(x))) : Nat}:
37	  +y = U32.shrn(x, Nat.mul(8n, k))
38	  Equal.trans(Nat, v(U32.mod(y, 256)), Nat.mod(v(y), 256n), C.low(8n, C.high(Nat.mul(8n, k), v(x))), UD.mod_nat(y, 256, {==}), Equal.trans(Nat, Nat.mod(v(y), 256n), Nat.mod(C.high(Nat.mul(8n, k), v(x)), 256n), C.low(8n, C.high(Nat.mul(8n, k), v(x))), Equal.cong(Nat, Nat, t => Nat.mod(t, 256n), v(y), C.high(Nat.mul(8n, k), v(x)), SHN.shrn_high(x, Nat.mul(8n, k))), Equal.sym(Nat, C.low(8n, C.high(Nat.mul(8n, k), v(x))), Nat.mod(C.high(Nat.mul(8n, k), v(x)), 256n), G.low_mod(8n, C.high(Nat.mul(8n, k), v(x)), 255n, {==}))))
39	
40	def to_le32(+x: U32) -> {SF.nats(F.u32_to_bytes_le(x)) == SF.le_digits(4n, v(x)) : List<&2, Nat>}:
41	  con_eq(v(F.byte32(x, 0n)), C.low(8n, v(x)), [v(F.byte32(x, 1n)), v(F.byte32(x, 2n)), v(F.byte32(x, 3n))], SF.le_digits(3n, C.high(8n, v(x))), byte_v(x, 0n),
42	    con_eq(v(F.byte32(x, 1n)), C.low(8n, C.high(8n, v(x))), [v(F.byte32(x, 2n)), v(F.byte32(x, 3n))], SF.le_digits(2n, C.high(8n, C.high(8n, v(x)))), byte_v(x, 1n),
43	      con_eq(v(F.byte32(x, 2n)), C.low(8n, C.high(8n, C.high(8n, v(x)))), [v(F.byte32(x, 3n))], SF.le_digits(1n, C.high(8n, C.high(8n, C.high(8n, v(x))))), byte_v(x, 2n),
44	        con_eq(v(F.byte32(x, 3n)), C.low(8n, C.high(8n, C.high(8n, C.high(8n, v(x))))), [], [], byte_v(x, 3n), {==}))))
45	
46	def to_be32(+x: U32) -> {SF.nats(F.u32_to_bytes_be(x)) == C.reverse(Nat, SF.le_digits(4n, v(x))) : List<&2, Nat>}:
47	  con_eq(v(F.byte32(x, 3n)), C.low(8n, C.high(8n, C.high(8n, C.high(8n, v(x))))), [v(F.byte32(x, 2n)), v(F.byte32(x, 1n)), v(F.byte32(x, 0n))], [C.low(8n, C.high(8n, C.high(8n, v(x)))), C.low(8n, C.high(8n, v(x))), C.low(8n, v(x))], byte_v(x, 3n),
48	    con_eq(v(F.byte32(x, 2n)), C.low(8n, C.high(8n, C.high(8n, v(x)))), [v(F.byte32(x, 1n)), v(F.byte32(x, 0n))], [C.low(8n, C.high(8n, v(x))), C.low(8n, v(x))], byte_v(x, 2n),
49	      con_eq(v(F.byte32(x, 1n)), C.low(8n, C.high(8n, v(x))), [v(F.byte32(x, 0n))], [C.low(8n, v(x))], byte_v(x, 1n),
50	        con_eq(v(F.byte32(x, 0n)), C.low(8n, v(x)), [], [], byte_v(x, 0n), {==}))))
51	
52	def u32_to_le(+a: U32) -> SF.ToBytes.le(~U32, ~SG.u32_val, ~F.u32_to_bytes_le, 4n, a):
53	  to_le32(a)
54	
55	def u32_to_be(+a: U32) -> SF.ToBytes.be(~U32, ~SG.u32_val, ~F.u32_to_bytes_be, 4n, a):
56	  to_be32(a)
57	
58	# ---- from_bytes: one Horner digit at a time ----
59	
60	# every value in r fits k bits
61	def bnd(+k: Nat, r: Maybe<&2, Nat>) -> Bool:
62	  match r:
63	    case Some{+n}:
64	      C.fits(k, n)
65	    case None{}:
66	      True{}
67	
68	def fb(+b: U32) -> {C.fits(8n, v(b)) == F.is_byte(b) : Bool}:
69	  Equal.trans(Bool, C.fits(8n, v(b)), Nat.is_lt(v(b), 256n), F.is_byte(b), WW.fits_lt(8n, v(b)), Equal.sym(Bool, U32.is_lt(b, 256), Nat.is_lt(v(b), 256n), U3.is_lt_nat(b, 256)))
70	
71	# b + 256 z fits 8 + k bits (Horner's step)
72	def step_fits(+k: Nat, +b: Nat, +z: Nat, +hb: {C.fits(8n, b) == True{} : Bool}, +hz: {C.fits(k, z) == True{} : Bool}) -> {C.fits(Nat.add(8n, k), Nat.add(b, C.shift(8n, z))) == True{} : Bool}:
73	  WW.limbs_fit(8n, k, b, z, hb, hz)
74	
75	def to32(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, +n: Nat, +h: {C.fits(Nat.add(8n, k), n) == True{} : Bool}) -> {C.fits(32n, n) == True{} : Bool}:
76	  SH.fits_mono(Nat.add(8n, k), 32n, n, hk, h)
77	
78	def step32(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, +z: U32, +hz: {C.fits(k, v(z)) == True{} : Bool}, +b: U32, +hb: {C.fits(8n, v(b)) == True{} : Bool}) -> {v(U32.add(b, U32.mul(z, 256))) == Nat.add(v(b), C.shift(8n, v(z))) : Nat}:
79	  +sz = C.shift(8n, v(z))
80	  +f0 = Equal.trans(Bool, C.fits(32n, sz), C.fits(32n, Nat.add(0n, sz)), True{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), sz, Nat.add(0n, sz), Equal.sym(Nat, Nat.add(0n, sz), sz, P32.zero_add(sz))), to32(k, hk, Nat.add(0n, sz), step_fits(k, 0n, v(z), {==}, hz)))
81	  +em = Equal.trans(Nat, v(U32.mul(z, 256)), C.low(32n, Nat.mul(v(z), 256n)), sz, P32.mul_low(z, 256), Equal.trans(Nat, C.low(32n, Nat.mul(v(z), 256n)), C.low(32n, sz), sz, Equal.cong(Nat, Nat, t => C.low(32n, t), Nat.mul(v(z), 256n), sz, Equal.sym(Nat, sz, Nat.mul(v(z), 256n), WW.shift_mul(8n, v(z)))), WW.low_fit(32n, sz, f0)))
82	  +ea = Equal.trans(Nat, v(U32.add(b, U32.mul(z, 256))), C.low(32n, Nat.add(v(b), v(U32.mul(z, 256)))), C.low(32n, Nat.add(v(b), sz)), P32.add_low(b, U32.mul(z, 256)), Equal.cong(Nat, Nat, t => C.low(32n, Nat.add(v(b), t)), v(U32.mul(z, 256)), sz, em))
83	  Equal.trans(Nat, v(U32.add(b, U32.mul(z, 256))), C.low(32n, Nat.add(v(b), sz)), Nat.add(v(b), sz), ea, WW.low_fit(32n, Nat.add(v(b), sz), to32(k, hk, Nat.add(v(b), sz), step_fits(k, v(b), v(z), hb, hz))))
84	
85	def d32_some(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, +z: U32, +hz: {C.fits(k, v(z)) == True{} : Bool}, +b: U32, +c: Bool, +hc: {F.is_byte(b) == c : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, c, b)) == SF.digit_on(Some{v(z)}, C.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}:
86	  match c:
87	    case True{}:
88	      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), True{}, fb(b), hc)
89	      %Equal.sym(Bool, C.fits(8n, v(b)), True{}, hb) : {SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, True{}, b)) == SF.digit_on(Some{v(z)}, _, v(b)) : Maybe<&2, Nat>}
90	      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, v(U32.add(b, U32.mul(z, 256))), Nat.add(v(b), C.shift(8n, v(z))), step32(k, hk, z, hz, b, hb))
91	    case False{}:
92	      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), False{}, fb(b), hc)
93	      %Equal.sym(Bool, C.fits(8n, v(b)), False{}, hb) : {SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, False{}, b)) == SF.digit_on(Some{v(z)}, _, v(b)) : Maybe<&2, Nat>}
94	      {==}
95	
96	def d32_sbnd(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, +z: U32, +hz: {C.fits(k, v(z)) == True{} : Bool}, +b: U32, +c: Bool, +hc: {F.is_byte(b) == c : Bool}) -> {bnd(Nat.add(8n, k), SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, c, b))) == True{} : Bool}:
97	  match c:
98	    case True{}:
99	      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), True{}, fb(b), hc)
100	      %Equal.sym(Nat, v(U32.add(b, U32.mul(z, 256))), Nat.add(v(b), C.shift(8n, v(z))), step32(k, hk, z, hz, b, hb)) : {C.fits(Nat.add(8n, k), _) == True{} : Bool}
101	      step_fits(k, v(b), v(z), hb, hz)
102	    case False{}:
103	      {==}
104	
105	def d32_val(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, r: Maybe<&2, U32>, +hr: {bnd(k, SF.mval(~U32, ~SG.u32_val, r)) == True{} : Bool}, +b: U32) -> {SF.mval(~U32, ~SG.u32_val, F.dig32(r, F.is_byte(b), b)) == SF.digit_on(SF.mval(~U32, ~SG.u32_val, r), C.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}:
106	  match r:
107	    case Some{+z}:
108	      d32_some(k, hk, z, hr, b, F.is_byte(b), {==})
109	    case None{}:
110	      {==}
111	
112	def d32_bnd(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, r: Maybe<&2, U32>, +hr: {bnd(k, SF.mval(~U32, ~SG.u32_val, r)) == True{} : Bool}, +b: U32) -> {bnd(Nat.add(8n, k), SF.mval(~U32, ~SG.u32_val, F.dig32(r, F.is_byte(b), b))) == True{} : Bool}:
113	  match r:
114	    case Some{+z}:
115	      d32_sbnd(k, hk, z, hr, b, F.is_byte(b), {==})
116	    case None{}:
117	      {==}
118	
119	def from4_ok(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> {SF.mval(~U32, ~SG.u32_val, F.from4(b0, b1, b2, b3)) == SF.from_le(4n, [v(b0), v(b1), v(b2), v(b3)]) : Maybe<&2, Nat>}:
120	  +r0 = {Some{0} : Maybe<&2, U32>}
121	  +r1 = F.dig32(r0, F.is_byte(b3), b3)
122	  +r2 = F.dig32(r1, F.is_byte(b2), b2)
123	  +r3 = F.dig32(r2, F.is_byte(b1), b1)
124	  +M0 = SF.mval(~U32, ~SG.u32_val, r0)
125	  +M1 = SF.mval(~U32, ~SG.u32_val, r1)
126	  +M2 = SF.mval(~U32, ~SG.u32_val, r2)
127	  +M3 = SF.mval(~U32, ~SG.u32_val, r3)
128	  +f0 = C.fits(8n, v(b0))
129	  +f1 = C.fits(8n, v(b1))
130	  +f2 = C.fits(8n, v(b2))
131	  +f3 = C.fits(8n, v(b3))
132	  +bd1 = d32_bnd(0n, {==}, r0, {==}, b3)
133	  +bd2 = d32_bnd(8n, {==}, r1, bd1, b2)
134	  +bd3 = d32_bnd(16n, {==}, r2, bd2, b1)
135	  +S1 = SF.digit_on(M0, f3, v(b3))
136	  +S2 = SF.digit_on(S1, f2, v(b2))
137	  +S3 = SF.digit_on(S2, f1, v(b1))
138	  +e1 = d32_val(0n, {==}, r0, {==}, b3)
139	  +e2 = Equal.trans(Maybe<&2, Nat>, M2, SF.digit_on(M1, f2, v(b2)), S2, d32_val(8n, {==}, r1, bd1, b2), Equal.cong(Maybe<&2, Nat>, Maybe<&2, Nat>, t => SF.digit_on(t, f2, v(b2)), M1, S1, e1))
140	  +e3 = Equal.trans(Maybe<&2, Nat>, M3, SF.digit_on(M2, f1, v(b1)), S3, d32_val(16n, {==}, r2, bd2, b1), Equal.cong(Maybe<&2, Nat>, Maybe<&2, Nat>, t => SF.digit_on(t, f1, v(b1)), M2, S2, e2))
141	  Equal.trans(Maybe<&2, Nat>, SF.mval(~U32, ~SG.u32_val, F.dig32(r3, F.is_byte(b0), b0)), SF.digit_on(M3, f0, v(b0)), SF.digit_on(S3, f0, v(b0)), d32_val(24n, {==}, r3, bd3, b0), Equal.cong(Maybe<&2, Nat>, Maybe<&2, Nat>, t => SF.digit_on(t, f0, v(b0)), M3, S3, e3))
142	
143	# any other length parses to None
144	def fl_len(+k: Nat, xs: List<&2, Nat>, +h: {Nat.is_eq(C.length(Nat, xs), k) == False{} : Bool}) -> {SF.from_le(k, xs) == None{} : Maybe<&2, Nat>}:
145	  match k xs:
146	    case 0n Nil{}:
147	      Empty.absurd({SF.from_le(0n, Nil{}) == None{} : Maybe<&2, Nat>}, L.true_false(h))
148	    case 0n Con{+x, t}:
149	      {==}
150	    case 1n+ +p Nil{}:
151	      {==}
152	    case 1n+ +p Con{+x, t}:
153	      %Equal.sym(Maybe<&2, Nat>, SF.from_le(p, t), None{}, fl_len(p, t, h)) : {SF.digit_on(_, C.fits(8n, x), x) == None{} : Maybe<&2, Nat>}
154	      {==}
155	
156	def rev_none(+k: Nat, +xs: List<&2, Nat>, +h: {Nat.is_eq(C.length(Nat, xs), k) == False{} : Bool}) -> {SF.from_le(k, C.reverse(Nat, xs)) == None{} : Maybe<&2, Nat>}:
157	  fl_len(k, C.reverse(Nat, xs), Equal.trans(Bool, Nat.is_eq(C.length(Nat, C.reverse(Nat, xs)), k), Nat.is_eq(C.length(Nat, xs), k), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, k), C.length(Nat, C.reverse(Nat, xs)), C.length(Nat, xs), LL.length_rev(Nat, xs)), h))
158	
159	# the list cases: exactly four bytes, or None on both sides
160	def fle4(+b0: U32, +b1: U32, +b2: U32, +b3: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_le(Con{b0, Con{b1, Con{b2, Con{b3, t}}}})) == SF.from_le(4n, SF.nats(Con{b0, Con{b1, Con{b2, Con{b3, t}}}})) : Maybe<&2, Nat>}:
161	  match t:
162	    case Nil{}:
163	      from4_ok(b0, b1, b2, b3)
164	    case Con{+b4, t5}:
165	      {==}
166	
167	def fle3(+b0: U32, +b1: U32, +b2: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_le(Con{b0, Con{b1, Con{b2, t}}})) == SF.from_le(4n, SF.nats(Con{b0, Con{b1, Con{b2, t}}})) : Maybe<&2, Nat>}:
168	  match t:
169	    case Nil{}:
170	      {==}
171	    case Con{+b3, t4}:
172	      fle4(b0, b1, b2, b3, t4)
173	
174	def fle2(+b0: U32, +b1: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_le(Con{b0, Con{b1, t}})) == SF.from_le(4n, SF.nats(Con{b0, Con{b1, t}})) : Maybe<&2, Nat>}:
175	  match t:
176	    case Nil{}:
177	      {==}
178	    case Con{+b2, t3}:
179	      fle3(b0, b1, b2, t3)
180	
181	def fle1(+b0: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_le(Con{b0, t})) == SF.from_le(4n, SF.nats(Con{b0, t})) : Maybe<&2, Nat>}:
182	  match t:
183	    case Nil{}:
184	      {==}
185	    case Con{+b1, t2}:
186	      fle2(b0, b1, t2)
187	
188	def u32_from_le(bs: List<&2, U32>) -> SF.FromBytes.le(~U32, ~SG.u32_val, ~F.u32_from_bytes_le, 4n, bs):
189	  match bs:
190	    case Nil{}:
191	      {==}
192	    case Con{+b0, t}:
193	      fle1(b0, t)
194	
195	def fbe4(+b3: U32, +b2: U32, +b1: U32, +b0: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_be(Con{b3, Con{b2, Con{b1, Con{b0, t}}}})) == SF.from_le(4n, C.reverse(Nat, SF.nats(Con{b3, Con{b2, Con{b1, Con{b0, t}}}}))) : Maybe<&2, Nat>}:
196	  match t:
197	    case Nil{}:
198	      from4_ok(b0, b1, b2, b3)
199	    case Con{+b4, t5}:
200	      Equal.sym(Maybe<&2, Nat>, SF.from_le(4n, C.reverse(Nat, SF.nats(Con{b3, Con{b2, Con{b1, Con{b0, Con{b4, t5}}}}}))), None{}, rev_none(4n, SF.nats(Con{b3, Con{b2, Con{b1, Con{b0, Con{b4, t5}}}}}), {==}))
201	
202	def fbe3(+b3: U32, +b2: U32, +b1: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_be(Con{b3, Con{b2, Con{b1, t}}})) == SF.from_le(4n, C.reverse(Nat, SF.nats(Con{b3, Con{b2, Con{b1, t}}}))) : Maybe<&2, Nat>}:
203	  match t:
204	    case Nil{}:
205	      {==}
206	    case Con{+b0, t4}:
207	      fbe4(b3, b2, b1, b0, t4)
208	
209	def fbe2(+b3: U32, +b2: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_be(Con{b3, Con{b2, t}})) == SF.from_le(4n, C.reverse(Nat, SF.nats(Con{b3, Con{b2, t}}))) : Maybe<&2, Nat>}:
210	  match t:
211	    case Nil{}:
212	      {==}
213	    case Con{+b1, t3}:
214	      fbe3(b3, b2, b1, t3)
215	
216	def fbe1(+b3: U32, t: List<&2, U32>) -> {SF.mval(~U32, ~SG.u32_val, F.u32_from_bytes_be(Con{b3, t})) == SF.from_le(4n, C.reverse(Nat, SF.nats(Con{b3, t}))) : Maybe<&2, Nat>}:
217	  match t:
218	    case Nil{}:
219	      {==}
220	    case Con{+b2, t2}:
221	      fbe2(b3, b2, t2)
222	
223	def u32_from_be(bs: List<&2, U32>) -> SF.FromBytes.be(~U32, ~SG.u32_val, ~F.u32_from_bytes_be, 4n, bs):
224	  match bs:
225	    case Nil{}:
226	      {==}
227	    case Con{+b3, t}:
228	      fbe1(b3, t)
229	
230	# ---- U64: digits split at the limb boundary ----
231	
232	def w8(k: Nat) -> Nat:
233	  match k:
234	    case 0n:
235	      0n
236	    case 1n+p:
237	      Nat.add(8n, w8(p))
238	
239	def fits0(+n: Nat, +h: {C.fits(0n, n) == True{} : Bool}) -> {n == 0n : Nat}:
240	  N.eq_from_is_eq(n, 0n, h)
241	
242	def dsplit(+a: Nat, +b: Nat, +lo: Nat, +hi: Nat, +hlo: {C.fits(w8(a), lo) == True{} : Bool}) -> {SF.le_digits(Nat.add(a, b), Nat.add(lo, C.shift(w8(a), hi))) == C.append(Nat, SF.le_digits(a, lo), SF.le_digits(b, hi)) : List<&2, Nat>}:
243	  match a:
244	    case 0n:
245	      %Equal.sym(Nat, lo, 0n, fits0(lo, hlo)) : {SF.le_digits(b, Nat.add(_, hi)) == SF.le_digits(b, hi) : List<&2, Nat>}
246	      {==}
247	    case 1n+ +p:
248	      +Q = C.shift(w8(p), hi)
249	      +ets = Equal.trans(List<&2, Nat>, SF.le_digits(Nat.add(p, b), C.high(8n, Nat.add(lo, C.shift(8n, Q)))), SF.le_digits(Nat.add(p, b), Nat.add(C.high(8n, lo), Q)), C.append(Nat, SF.le_digits(p, C.high(8n, lo)), SF.le_digits(b, hi)), Equal.cong(Nat, List<&2, Nat>, t => SF.le_digits(Nat.add(p, b), t), C.high(8n, Nat.add(lo, C.shift(8n, Q))), Nat.add(C.high(8n, lo), Q), WW.high_add_shift(8n, lo, Q)), dsplit(p, b, C.high(8n, lo), hi, SH.fits_high(8n, w8(p), lo, hlo)))
250	      %Equal.sym(Nat, C.shift(Nat.add(8n, w8(p)), hi), C.shift(8n, Q), WW.shift_comp(8n, w8(p), hi)) : {SF.le_digits(Nat.add(1n+p, b), Nat.add(lo, _)) == C.append(Nat, SF.le_digits(1n+p, lo), SF.le_digits(b, hi)) : List<&2, Nat>}
251	      con_eq(C.low(8n, Nat.add(lo, C.shift(8n, Q))), C.low(8n, lo), SF.le_digits(Nat.add(p, b), C.high(8n, Nat.add(lo, C.shift(8n, Q)))), C.append(Nat, SF.le_digits(p, C.high(8n, lo)), SF.le_digits(b, hi)), WW.low_add_shift(8n, lo, Q), ets)
252	
253	def u64_to_le(+a: WU.U64) -> SF.ToBytes.le(~WU.U64, ~SG.u64_val, ~F.u64_to_bytes_le, 8n, a):
254	  match a:
255	    case WU.U64{+l, +h}:
256	      +A = SF.nats(F.u32_to_bytes_le(l))
257	      +B = SF.nats(F.u32_to_bytes_le(h))
258	      +e1 = Equal.trans(List<&2, Nat>, C.append(Nat, A, B), C.append(Nat, SF.le_digits(4n, v(l)), B), C.append(Nat, SF.le_digits(4n, v(l)), SF.le_digits(4n, v(h))), Equal.cong(List<&2, Nat>, List<&2, Nat>, t => C.append(Nat, t, B), A, SF.le_digits(4n, v(l)), to_le32(l)), Equal.cong(List<&2, Nat>, List<&2, Nat>, t => C.append(Nat, SF.le_digits(4n, v(l)), t), B, SF.le_digits(4n, v(h)), to_le32(h)))
259	      Equal.trans(List<&2, Nat>, C.append(Nat, A, B), C.append(Nat, SF.le_digits(4n, v(l)), SF.le_digits(4n, v(h))), SF.le_digits(Nat.add(4n, 4n), Nat.add(v(l), C.shift(w8(4n), v(h)))), e1, Equal.sym(List<&2, Nat>, SF.le_digits(Nat.add(4n, 4n), Nat.add(v(l), C.shift(w8(4n), v(h)))), C.append(Nat, SF.le_digits(4n, v(l)), SF.le_digits(4n, v(h))), dsplit(4n, 4n, v(l), v(h), LW.vb(l))))
260	
261	def u64_to_be(+a: WU.U64) -> SF.ToBytes.be(~WU.U64, ~SG.u64_val, ~F.u64_to_bytes_be, 8n, a):
262	  match a:
263	    case WU.U64{+l, +h}:
264	      +Dl = SF.le_digits(4n, v(l))
265	      +Dh = SF.le_digits(4n, v(h))
266	      +A = SF.nats(F.u32_to_bytes_be(h))
267	      +B = SF.nats(F.u32_to_bytes_be(l))
268	      +e1 = Equal.trans(List<&2, Nat>, C.append(Nat, A, B), C.append(Nat, C.reverse(Nat, Dh), B), C.append(Nat, C.reverse(Nat, Dh), C.reverse(Nat, Dl)), Equal.cong(List<&2, Nat>, List<&2, Nat>, t => C.append(Nat, t, B), A, C.reverse(Nat, Dh), to_be32(h)), Equal.cong(List<&2, Nat>, List<&2, Nat>, t => C.append(Nat, C.reverse(Nat, Dh), t), B, C.reverse(Nat, Dl), to_be32(l)))
269	      +e2 = Equal.sym(List<&2, Nat>, C.reverse(Nat, C.append(Nat, Dl, Dh)), C.append(Nat, C.reverse(Nat, Dh), C.reverse(Nat, Dl)), LL.rev_append(Nat, Dl, Dh))
270	      +e3 = Equal.cong(List<&2, Nat>, List<&2, Nat>, t => C.reverse(Nat, t), C.append(Nat, Dl, Dh), SF.le_digits(Nat.add(4n, 4n), Nat.add(v(l), C.shift(w8(4n), v(h)))), Equal.sym(List<&2, Nat>, SF.le_digits(Nat.add(4n, 4n), Nat.add(v(l), C.shift(w8(4n), v(h)))), C.append(Nat, Dl, Dh), dsplit(4n, 4n, v(l), v(h), LW.vb(l))))
271	      Equal.trans(List<&2, Nat>, C.append(Nat, A, B), C.append(Nat, C.reverse(Nat, Dh), C.reverse(Nat, Dl)), C.reverse(Nat, SF.le_digits(Nat.add(4n, 4n), Nat.add(v(l), C.shift(w8(4n), v(h))))), e1, Equal.trans(List<&2, Nat>, C.append(Nat, C.reverse(Nat, Dh), C.reverse(Nat, Dl)), C.reverse(Nat, C.append(Nat, Dl, Dh)), C.reverse(Nat, SF.le_digits(Nat.add(4n, 4n), Nat.add(v(l), C.shift(w8(4n), v(h))))), e2, e3))
272	
273	# ---- U64 from_bytes: Horner's rule on U64 values ----
274	
275	def to64(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, +n: Nat, +h: {C.fits(Nat.add(8n, k), n) == True{} : Bool}) -> {C.fits(64n, n) == True{} : Bool}:
276	  SH.fits_mono(Nat.add(8n, k), 64n, n, hk, h)
277	
278	def step64(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, +z: WU.U64, +hz: {C.fits(k, SG.u64_val(z)) == True{} : Bool}, +b: U32, +hb: {C.fits(8n, v(b)) == True{} : Bool}) -> {SG.u64_val(X.add(WU.U64{b, 0}, X.mul(z, WU.U64{256, 0}))) == Nat.add(v(b), C.shift(8n, SG.u64_val(z))) : Nat}:
279	  +vz = SG.u64_val(z)
280	  +sz = C.shift(8n, vz)
281	  +mz = X.mul(z, WU.U64{256, 0})
282	  +bz = {WU.U64{b, 0} : WU.U64}
283	  +f0 = Equal.trans(Bool, C.fits(64n, sz), C.fits(64n, Nat.add(0n, sz)), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, t), sz, Nat.add(0n, sz), Equal.sym(Nat, Nat.add(0n, sz), sz, P32.zero_add(sz))), to64(k, hk, Nat.add(0n, sz), step_fits(k, 0n, vz, {==}, hz)))
284	  +em = Equal.trans(Nat, SG.u64_val(mz), C.low(64n, Nat.mul(vz, 256n)), sz, WA.mul_value(z, WU.U64{256, 0}), Equal.trans(Nat, C.low(64n, Nat.mul(vz, 256n)), C.low(64n, sz), sz, Equal.cong(Nat, Nat, t => C.low(64n, t), Nat.mul(vz, 256n), sz, Equal.sym(Nat, sz, Nat.mul(vz, 256n), WW.shift_mul(8n, vz))), WW.low_fit(64n, sz, f0)))
285	  +eb2 = Equal.trans(Nat, SG.u64_val(bz), Nat.add(v(b), 0n), v(b), {==}, N.add_zero(v(b)))
286	  +ea = Equal.trans(Nat, SG.u64_val(X.add(bz, mz)), C.low(64n, Nat.add(SG.u64_val(bz), SG.u64_val(mz))), C.low(64n, Nat.add(v(b), sz)), WA.add_value(bz, mz), Equal.trans(Nat, C.low(64n, Nat.add(SG.u64_val(bz), SG.u64_val(mz))), C.low(64n, Nat.add(v(b), SG.u64_val(mz))), C.low(64n, Nat.add(v(b), sz)), Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(t, SG.u64_val(mz))), SG.u64_val(bz), v(b), eb2), Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(v(b), t)), SG.u64_val(mz), sz, em)))
287	  Equal.trans(Nat, SG.u64_val(X.add(bz, mz)), C.low(64n, Nat.add(v(b), sz)), Nat.add(v(b), sz), ea, WW.low_fit(64n, Nat.add(v(b), sz), to64(k, hk, Nat.add(v(b), sz), step_fits(k, v(b), vz, hb, hz))))
288	
289	def d64_some(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, +z: WU.U64, +hz: {C.fits(k, SG.u64_val(z)) == True{} : Bool}, +b: U32, +c: Bool, +hc: {F.is_byte(b) == c : Bool}) -> {SF.mval(~WU.U64, ~SG.u64_val, F.dig64(Some{z}, c, b)) == SF.digit_on(Some{SG.u64_val(z)}, C.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}:
290	  match c:
291	    case True{}:
292	      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), True{}, fb(b), hc)
293	      %Equal.sym(Bool, C.fits(8n, v(b)), True{}, hb) : {SF.mval(~WU.U64, ~SG.u64_val, F.dig64(Some{z}, True{}, b)) == SF.digit_on(Some{SG.u64_val(z)}, _, v(b)) : Maybe<&2, Nat>}
294	      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, SG.u64_val(X.add(WU.U64{b, 0}, X.mul(z, WU.U64{256, 0}))), Nat.add(v(b), C.shift(8n, SG.u64_val(z))), step64(k, hk, z, hz, b, hb))
295	    case False{}:
296	      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), False{}, fb(b), hc)
297	      %Equal.sym(Bool, C.fits(8n, v(b)), False{}, hb) : {SF.mval(~WU.U64, ~SG.u64_val, F.dig64(Some{z}, False{}, b)) == SF.digit_on(Some{SG.u64_val(z)}, _, v(b)) : Maybe<&2, Nat>}
298	      {==}
299	
300	def d64_sbnd(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, +z: WU.U64, +hz: {C.fits(k, SG.u64_val(z)) == True{} : Bool}, +b: U32, +c: Bool, +hc: {F.is_byte(b) == c : Bool}) -> {bnd(Nat.add(8n, k), SF.mval(~WU.U64, ~SG.u64_val, F.dig64(Some{z}, c, b))) == True{} : Bool}:
301	  match c:
302	    case True{}:
303	      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), True{}, fb(b), hc)
304	      %Equal.sym(Nat, SG.u64_val(X.add(WU.U64{b, 0}, X.mul(z, WU.U64{256, 0}))), Nat.add(v(b), C.shift(8n, SG.u64_val(z))), step64(k, hk, z, hz, b, hb)) : {C.fits(Nat.add(8n, k), _) == True{} : Bool}
305	      step_fits(k, v(b), SG.u64_val(z), hb, hz)
306	    case False{}:
307	      {==}
308	
309	def d64_val(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, r: Maybe<&2, WU.U64>, +hr: {bnd(k, SF.mval(~WU.U64, ~SG.u64_val, r)) == True{} : Bool}, +b: U32) -> {SF.mval(~WU.U64, ~SG.u64_val, F.dig64(r, F.is_byte(b), b)) == SF.digit_on(SF.mval(~WU.U64, ~SG.u64_val, r), C.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}:
310	  match r:
311	    case Some{+z}:
312	      d64_some(k, hk, z, hr, b, F.is_byte(b), {==})
313	    case None{}:
314	      {==}
315	
316	def d64_bnd(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, r: Maybe<&2, WU.U64>, +hr: {bnd(k, SF.mval(~WU.U64, ~SG.u64_val, r)) == True{} : Bool}, +b: U32) -> {bnd(Nat.add(8n, k), SF.mval(~WU.U64, ~SG.u64_val, F.dig64(r, F.is_byte(b), b))) == True{} : Bool}:
317	  match r:
318	    case Some{+z}:
319	      d64_sbnd(k, hk, z, hr, b, F.is_byte(b), {==})
320	    case None{}:
321	      {==}
322	
323	# one Horner step on both sides, carrying the bound
324	def hstep(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, r: Maybe<&2, WU.U64>, +S: Maybe<&2, Nat>, +es: {SF.mval(~WU.U64, ~SG.u64_val, r) == S : Maybe<&2, Nat>}, +hr: {bnd(k, SF.mval(~WU.U64, ~SG.u64_val, r)) == True{} : Bool}, +b: U32) -> {SF.mval(~WU.U64, ~SG.u64_val, F.dig64(r, F.is_byte(b), b)) == SF.digit_on(S, C.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}:
325	  Equal.trans(Maybe<&2, Nat>, SF.mval(~WU.U64, ~SG.u64_val, F.dig64(r, F.is_byte(b), b)), SF.digit_on(SF.mval(~WU.U64, ~SG.u64_val, r), C.fits(8n, v(b)), v(b)), SF.digit_on(S, C.fits(8n, v(b)), v(b)), d64_val(k, hk, r, hr, b), Equal.cong(Maybe<&2, Nat>, Maybe<&2, Nat>, t => SF.digit_on(t, C.fits(8n, v(b)), v(b)), SF.mval(~WU.U64, ~SG.u64_val, r), S, es))
326	
327	def from8_ok(+b0: U32, +b1: U32, +b2: U32, +b3: U32, +b4: U32, +b5: U32, +b6: U32, +b7: U32) -> {SF.mval(~WU.U64, ~SG.u64_val, F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(Some{WU.U64{0, 0}}, F.is_byte(b7), b7), F.is_byte(b6), b6), F.is_byte(b5), b5), F.is_byte(b4), b4), F.is_byte(b3), b3), F.is_byte(b2), b2), F.is_byte(b1), b1), F.is_byte(b0), b0)) == SF.from_le(8n, [v(b0), v(b1), v(b2), v(b3), v(b4), v(b5), v(b6), v(b7)]) : Maybe<&2, Nat>}:
328	  +r0 = {Some{WU.U64{0, 0}} : Maybe<&2, WU.U64>}
329	  +r1 = F.dig64(r0, F.is_byte(b7), b7)
330	  +r2 = F.dig64(r1, F.is_byte(b6), b6)
331	  +r3 = F.dig64(r2, F.is_byte(b5), b5)
332	  +r4 = F.dig64(r3, F.is_byte(b4), b4)
333	  +r5 = F.dig64(r4, F.is_byte(b3), b3)
334	  +r6 = F.dig64(r5, F.is_byte(b2), b2)
335	  +r7 = F.dig64(r6, F.is_byte(b1), b1)
336	  +S0 = {Some{0n} : Maybe<&2, Nat>}
337	  +S1 = SF.digit_on(S0, C.fits(8n, v(b7)), v(b7))
338	  +S2 = SF.digit_on(S1, C.fits(8n, v(b6)), v(b6))
339	  +S3 = SF.digit_on(S2, C.fits(8n, v(b5)), v(b5))
340	  +S4 = SF.digit_on(S3, C.fits(8n, v(b4)), v(b4))
341	  +S5 = SF.digit_on(S4, C.fits(8n, v(b3)), v(b3))
342	  +S6 = SF.digit_on(S5, C.fits(8n, v(b2)), v(b2))
343	  +S7 = SF.digit_on(S6, C.fits(8n, v(b1)), v(b1))
344	  +c1 = d64_bnd(0n, {==}, r0, {==}, b7)
345	  +c2 = d64_bnd(8n, {==}, r1, c1, b6)
346	  +c3 = d64_bnd(16n, {==}, r2, c2, b5)
347	  +c4 = d64_bnd(24n, {==}, r3, c3, b4)
348	  +c5 = d64_bnd(32n, {==}, r4, c4, b3)
349	  +c6 = d64_bnd(40n, {==}, r5, c5, b2)
350	  +c7 = d64_bnd(48n, {==}, r6, c6, b1)
351	  +e1 = hstep(0n, {==}, r0, S0, {==}, {==}, b7)
352	  +e2 = hstep(8n, {==}, r1, S1, e1, c1, b6)
353	  +e3 = hstep(16n, {==}, r2, S2, e2, c2, b5)
354	  +e4 = hstep(24n, {==}, r3, S3, e3, c3, b4)
355	  +e5 = hstep(32n, {==}, r4, S4, e4, c4, b3)
356	  +e6 = hstep(40n, {==}, r5, S5, e5, c5, b2)
357	  +e7 = hstep(48n, {==}, r6, S6, e6, c6, b1)
358	  hstep(56n, {==}, r7, S7, e7, c7, b0)
359	
360	# the list cases at U64: exactly eight bytes, or None on both sides
361	
362	def gle8(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, Con{x7, t}}}}}}}})) == SF.from_le(8n, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, Con{x7, t}}}}}}}})) : Maybe<&2, Nat>}:
363	  match t:
364	    case Nil{}:
365	      from8_ok(x0, x1, x2, x3, x4, x5, x6, x7)
366	    case Con{+x8, t9}:
367	      {==}
368	
369	def gle7(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, t}}}}}}})) == SF.from_le(8n, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, t}}}}}}})) : Maybe<&2, Nat>}:
370	  match t:
371	    case Nil{}:
372	      {==}
373	    case Con{+x7, tn}:
374	      gle8(x0, x1, x2, x3, x4, x5, x6, x7, tn)
375	
376	def gle6(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, t}}}}}})) == SF.from_le(8n, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, t}}}}}})) : Maybe<&2, Nat>}:
377	  match t:
378	    case Nil{}:
379	      {==}
380	    case Con{+x6, tn}:
381	      gle7(x0, x1, x2, x3, x4, x5, x6, tn)
382	
383	def gle5(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, t}}}}})) == SF.from_le(8n, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, t}}}}})) : Maybe<&2, Nat>}:
384	  match t:
385	    case Nil{}:
386	      {==}
387	    case Con{+x5, tn}:
388	      gle6(x0, x1, x2, x3, x4, x5, tn)
389	
390	def gle4(+x0: U32, +x1: U32, +x2: U32, +x3: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, Con{x1, Con{x2, Con{x3, t}}}})) == SF.from_le(8n, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, t}}}})) : Maybe<&2, Nat>}:
391	  match t:
392	    case Nil{}:
393	      {==}
394	    case Con{+x4, tn}:
395	      gle5(x0, x1, x2, x3, x4, tn)
396	
397	def gle3(+x0: U32, +x1: U32, +x2: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, Con{x1, Con{x2, t}}})) == SF.from_le(8n, SF.nats(Con{x0, Con{x1, Con{x2, t}}})) : Maybe<&2, Nat>}:
398	  match t:
399	    case Nil{}:
400	      {==}
401	    case Con{+x3, tn}:
402	      gle4(x0, x1, x2, x3, tn)
403	
404	def gle2(+x0: U32, +x1: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, Con{x1, t}})) == SF.from_le(8n, SF.nats(Con{x0, Con{x1, t}})) : Maybe<&2, Nat>}:
405	  match t:
406	    case Nil{}:
407	      {==}
408	    case Con{+x2, tn}:
409	      gle3(x0, x1, x2, tn)
410	
411	def gle1(+x0: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_le(Con{x0, t})) == SF.from_le(8n, SF.nats(Con{x0, t})) : Maybe<&2, Nat>}:
412	  match t:
413	    case Nil{}:
414	      {==}
415	    case Con{+x1, tn}:
416	      gle2(x0, x1, tn)
417	
418	def u64_from_le(bs: List<&2, U32>) -> SF.FromBytes.le(~WU.U64, ~SG.u64_val, ~F.u64_from_bytes_le, 8n, bs):
419	  match bs:
420	    case Nil{}:
421	      {==}
422	    case Con{+x0, t}:
423	      gle1(x0, t)
424	
425	def gbe8(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, Con{x7, t}}}}}}}})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, Con{x7, t}}}}}}}}))) : Maybe<&2, Nat>}:
426	  match t:
427	    case Nil{}:
428	      from8_ok(x7, x6, x5, x4, x3, x2, x1, x0)
429	    case Con{+x8, t9}:
430	      Equal.sym(Maybe<&2, Nat>, SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, Con{x7, Con{x8, t9}}}}}}}}}))), None{}, rev_none(8n, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, Con{x7, Con{x8, t9}}}}}}}}}), {==}))
431	
432	def gbe7(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, t}}}}}}})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, Con{x6, t}}}}}}}))) : Maybe<&2, Nat>}:
433	  match t:
434	    case Nil{}:
435	      {==}
436	    case Con{+x7, tn}:
437	      gbe8(x0, x1, x2, x3, x4, x5, x6, x7, tn)
438	
439	def gbe6(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, t}}}}}})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, Con{x5, t}}}}}}))) : Maybe<&2, Nat>}:
440	  match t:
441	    case Nil{}:
442	      {==}
443	    case Con{+x6, tn}:
444	      gbe7(x0, x1, x2, x3, x4, x5, x6, tn)
445	
446	def gbe5(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, t}}}}})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, Con{x4, t}}}}}))) : Maybe<&2, Nat>}:
447	  match t:
448	    case Nil{}:
449	      {==}
450	    case Con{+x5, tn}:
451	      gbe6(x0, x1, x2, x3, x4, x5, tn)
452	
453	def gbe4(+x0: U32, +x1: U32, +x2: U32, +x3: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, Con{x1, Con{x2, Con{x3, t}}}})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, Con{x2, Con{x3, t}}}}))) : Maybe<&2, Nat>}:
454	  match t:
455	    case Nil{}:
456	      {==}
457	    case Con{+x4, tn}:
458	      gbe5(x0, x1, x2, x3, x4, tn)
459	
460	def gbe3(+x0: U32, +x1: U32, +x2: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, Con{x1, Con{x2, t}}})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, Con{x2, t}}}))) : Maybe<&2, Nat>}:
461	  match t:
462	    case Nil{}:
463	      {==}
464	    case Con{+x3, tn}:
465	      gbe4(x0, x1, x2, x3, tn)
466	
467	def gbe2(+x0: U32, +x1: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, Con{x1, t}})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, Con{x1, t}}))) : Maybe<&2, Nat>}:
468	  match t:
469	    case Nil{}:
470	      {==}
471	    case Con{+x2, tn}:
472	      gbe3(x0, x1, x2, tn)
473	
474	def gbe1(+x0: U32, t: List<&2, U32>) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_from_bytes_be(Con{x0, t})) == SF.from_le(8n, C.reverse(Nat, SF.nats(Con{x0, t}))) : Maybe<&2, Nat>}:
475	  match t:
476	    case Nil{}:
477	      {==}
478	    case Con{+x1, tn}:
479	      gbe2(x0, x1, tn)
480	
481	def u64_from_be(bs: List<&2, U32>) -> SF.FromBytes.be(~WU.U64, ~SG.u64_val, ~F.u64_from_bytes_be, 8n, bs):
482	  match bs:
483	    case Nil{}:
484	      {==}
485	    case Con{+x0, t}:
486	      gbe1(x0, t)