def m256

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

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/math/u64/u64div.bend as PD

174def m256(+x: Nat) -> {Nat.mul(x, 256n) == C.shift(8n, x) : Nat}:
175  PD.mul_pow(1n, {==}, 8n, x, 256n, {==})