def shn_ge

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/reduce.bend:50

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

50# 2^256 c >= 2^256 when c >= 1
51def shn_ge(+one: Nat, +c: Nat, +h: {Nat.is_le(one, c) == True{} : Bool}) -> {Nat.is_le(LM.shn(32n, one), LM.shn(32n, c)) == True{} : Bool}:
52  AR.sc_le(256n, one, c, h)