def r_small
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:57
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec
import Base
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/field.bend as F
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/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
57def r_small(+pp: Nat, +k: U32, +hk: {Nat.is_le(v(k), 255n) == True{} : Bool}) -> RL.R(pp, F.small(k), v(k)):
58 (L.and_intro(Nat.is_le(v(k), 255n), LM.okb(31n, K.rep(31n, 0, Nil{}), 255n), hk, {==}), G.c_eq(pp, FS.value(F.small(k)), v(k), Equal.trans(Nat, FS.value(F.small(k)), Nat.add(v(k), 0n), v(k), {==}, N.add_zero(v(k)))))