def to_be32

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

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

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