def mod256

bend-collections-laws-math@1.0.0.0 · proofs/math/random/wrappers.bend:164

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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as AR

164def mod256(+n: Nat) -> {Nat.mod(n, 256n) == C.low(8n, n) : Nat}:
165  +q = C.high(8n, n)
166  +r = C.low(8n, n)
167  +e = Equal.trans(Nat, n, Nat.add(r, C.shift(8n, q)), Nat.add(Nat.mul(q, 256n), r), WW.low_high(8n, n),
168    Equal.trans(Nat, Nat.add(r, C.shift(8n, q)), Nat.add(C.shift(8n, q), r), Nat.add(Nat.mul(q, 256n), r), N.add_comm(r, C.shift(8n, q)),
169      Equal.cong(Nat, Nat, z => Nat.add(z, r), C.shift(8n, q), Nat.mul(q, 256n), WW.shift_mul(8n, q))))
170  Equal.trans(Nat, Nat.mod(n, 256n), Nat.mod(Nat.add(Nat.mul(q, 256n), r), 256n), r,
171    Equal.cong(Nat, Nat, z => Nat.mod(z, 256n), n, Nat.add(Nat.mul(q, 256n), r), e),
172    AR.mod_of(q, 255n, r, WW.lt_of_fits(8n, r, WW.low_fits(8n, n))))