proofs/math/typed/fixbytes.bend

bend-collections-laws-math@1.0.0.0 · 486 lines · 60 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
4import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
5import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as LL
11import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3
12import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SHN
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/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
28def v(+x: U32) -> Nat:
29  U32.to_nat(x)
30
31def 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
36def 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
40def 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
46def 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
52def u32_to_le(+a: U32) -> SF.ToBytes.le(~U32, ~SG.u32_val, ~F.u32_to_bytes_le, 4n, a):
53  to_le32(a)
54
55def 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
61def 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
68def 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)
72def 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
75def 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
78def 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
85def 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
96def 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
105def 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
112def 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
119def 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
144def 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
156def 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
160def 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
167def 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
174def 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
181def 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
188def 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
195def 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
202def 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
209def 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
216def 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
223def 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
232def w8(k: Nat) -> Nat:
233  match k:
234    case 0n:
235      0n
236    case 1n+p:
237      Nat.add(8n, w8(p))
238
239def fits0(+n: Nat, +h: {C.fits(0n, n) == True{} : Bool}) -> {n == 0n : Nat}:
240  N.eq_from_is_eq(n, 0n, h)
241
242def 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
253def 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
261def 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
275def 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
278def 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
289def 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
300def 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
309def 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
316def 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
324def 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
327def 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
362def 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
369def 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
376def 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
383def 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
390def 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
397def 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
404def 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
411def 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
418def 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
425def 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
432def 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
439def 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
446def 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
453def 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
460def 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
467def 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
474def 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
481def 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)