~/bend-docscommunity

proofs/crypto/secp256k1/pscal.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as Pscal

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pscal.src; edit the .src

14 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
import ../../../src/crypto/secp256k1/scalar.bend as S
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../../src/crypto/secp256k1/ecdsa.bend as E
import ../../lib/nat.bend as N
import ./limbs.bend as LV
import ./fprot.bend as FR
import ./scalarops.bend as SO
import ./fwrap.bend as FW
import ./bytes.bend as BY

Definitions

def scalar_ok_v source · line 20 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.scalar_ok(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.scalar_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x)) : Bool}

def ev512 source · line 26 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool}

a 16-limb value is below 2^512

def sred_v source · line 31 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(x)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one)) : Nat}

x mod n for a 16-limb x

def sred_r source · line 37 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(x)) == True{} : Bool}

def hash_v source · line 41 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.hash_scalar(h)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.hash_scalar(one, h) : Nat}

def hash_r source · line 46 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.hash_scalar(h)) == True{} : Bool}