def u64_to_be

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbytes.bend:261

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

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))