def low_all

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/scalar2.bend:67

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/spec/crypto/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

67def low_all(+bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {C.low(X.bitlen(bs), FS.value(bs)) == FS.value(bs) : Nat}:
68  WI.low_fit(X.bitlen(bs), FS.value(bs), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), C.high(X.bitlen(bs), FS.value(bs)), 0n, byte_fits(bs, hb)))