def to_le32

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

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/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F

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), {==}))))