def identity_rel
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pdec.bend:174
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend as Pdec
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
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/src/crypto/ed25519/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as PR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC
174def identity_rel(+pp: Nat) -> PR.Rp(pp, PT.identity(), SE.identity()):
175 PR.mk(pp, F.zero(), F.one(), F.one(), F.zero(), 0n, 1n, 1n, 0n, PC.r_zero(pp), PC.r_one(pp), PC.r_one(pp), PC.r_zero(pp))