def le255

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/fold.bend:57

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

57# 255 <= 2^27 (= 2^8 2^19)
58def le255(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {Nat.is_le(255n, WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}:
59  +a = N.lt_le(255n, 256n, {==})
60  +b = L.subst(Nat, z => {Nat.is_le(255n, z) == True{} : Bool}, 256n, WD.sc(8n, one), LM.k256(one, h1), a)
61  +c = M.sc_mono(k, 8n, one)
62  N.le_trans(255n, WD.sc(8n, one), WD.sc(Nat.add(k, 8n), one), b, c)