def low_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:244

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/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

244# low 8 bits of x + 2^16 r: those of x
245def low_v(+x: Nat, +r: Nat) -> {C.low(8n, Nat.add(x, C.shift(16n, r))) == Nat.mod(x, 256n) : Nat}:
246  %Equal.sym(Nat, C.shift(16n, r), C.shift(8n, C.shift(8n, r)), Equal.sym(Nat, C.shift(8n, C.shift(8n, r)), C.shift(16n, r), SR.shift_shift(8n, 8n, r))) : {C.low(8n, Nat.add(x, _)) == Nat.mod(x, 256n) : Nat}
247  %Equal.sym(Nat, C.low(8n, Nat.add(x, C.shift(8n, C.shift(8n, r)))), C.low(8n, x), WW.low_add_shift(8n, x, C.shift(8n, r))) : {_ == Nat.mod(x, 256n) : Nat}
248  low8(x)