def dm256

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:177

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

177# n == (n mod 256) + 2^8 (n div 256)
178def dm256(+n: Nat) -> {Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))) == n : Nat}:
179  +e = Equal.sym(Nat, n, Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), NR.dm_eq(255n, n))
180  +e2 = Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n)), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), M.cong_r(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n)), Nat.mul(Nat.div(n, 256n), 256n), Equal.sym(Nat, Nat.mul(Nat.div(n, 256n), 256n), C.shift(8n, Nat.div(n, 256n)), m256(Nat.div(n, 256n)))), NA.add_comm(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n)))
181  Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), n, e2, e)