spec/crypto/secp256k1/field.bend checks
raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/field.bend as Field
2 imports
import Base import ../../lib/common.bend as C
Definitions
def digits source · line 19 · raw
@+one:Nat -> @ds:List<&2, Nat> -> Nat
a number from its little-endian radix-2^16 digits, each scaled by one: digits(1, [d0, d1, ...]) = d0 + 2^16 d1 + ...
def w256 source · line 27 · raw
@+one:Nat -> Nat
2^256
def cp source · line 31 · raw
@+one:Nat -> Nat
2^256 - p = 2^32 + 977, and p
def prime source · line 34 · raw
@+one:Nat -> Nat
def cn source · line 38 · raw
@+one:Nat -> Nat
2^256 - n = 432420386565659656852420866390673177327, and n
def order source · line 41 · raw
@+one:Nat -> Nat
def madd source · line 46 · raw
@+m:Nat -> @a:Nat -> @b:Nat -> Nat
def msub source · line 50 · raw
@+m:Nat -> @a:Nat -> @b:Nat -> Nat
a - b mod m
def mneg source · line 53 · raw
@+m:Nat -> @a:Nat -> Nat
def mmul source · line 56 · raw
@+m:Nat -> @a:Nat -> @b:Nat -> Nat
def mpow source · line 59 · raw
@+m:Nat -> @a:Nat -> @e:Nat -> Nat
def minv source · line 63 · raw
@+m:Nat -> @a:Nat -> Nat
a^(m - 2): for a prime m the inverse of a nonzero a (Fermat); 0 for 0
def fsqrt source · line 68 · raw
@+m:Nat -> @a:Nat -> Nat
a^((p + 1) / 4): a square root of a whenever a is a square mod p (p = 3 mod 4)
def value source · line 74 · raw
@+one:Nat -> @xs:List<&2, Nat> -> Nat
the value of little-endian radix-2^16 limbs
def limbs16 source · line 78 · raw
@+one:Nat -> @n:Nat -> @xs:List<&2, Nat> -> Bool
exactly 16 limbs, each below 2^16
def reduced source · line 90 · raw
@+one:Nat -> @+m:Nat -> @+xs:List<&2, Nat> -> Bool
a reduced element mod m: 16 limbs below 2^16 of value below m