def pp

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/consts.bend:100

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS

100# p = 1 + pp, m + c = 2^256
101def pp(+one: Nat) -> Nat:
102  Nat.sub(C.shift(256n, one), Nat.add(FS.cp(one), 1n))