def byte_v

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

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/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SHN
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G

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