def u64_to_le

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

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/math/typed/u32laws.bend as LW

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