def ge_p
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as Pointimport Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
132# y >= p: the carry of y + 2^256 - p is not 0
133def ge_p(+y: List<&2, U32>) -> Bool:
134 Bool.not(U32.is_eq(F.cr_out(F.carry(F.addl(y, F.comp_p()), 0)), 0))
Uses (9)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point:decode
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec:decode_rel
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec:dec_y_rel
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec:dec_y_rel_core
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec:ge_p_eq