~/bend-docscommunity

spec/crypto/secp256k1/schnorr.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/schnorr.bend as Schnorr

4 imports
import Base
import ../sha.bend as FIPS
import ./field.bend as FS
import ./curve.bend as CV

Definitions

def p source · line 12 · raw

@+one:Nat -> Nat

def n source · line 15 · raw

@+one:Nat -> Nat

def cat source · line 18 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> List<&2, U32>

def bytes32 source · line 21 · raw

@+x:Nat -> List<&2, U32>

def tagged_h source · line 24 · raw

@+th:List<&2, U32> -> @x:List<&2, U32> -> List<&2, U32>

def tagged source · line 28 · raw

@tag:List<&2, U32> -> @x:List<&2, U32> -> List<&2, U32>

hash_name(x) = SHA256(SHA256(name) || SHA256(name) || x), name in ASCII

def tag_aux source · line 32 · raw

List<&2, U32>

"BIP0340/aux", "BIP0340/nonce", "BIP0340/challenge"

def tag_nonce source · line 35 · raw

List<&2, U32>

def tag_challenge source · line 38 · raw

List<&2, U32>

def xor_bytes source · line 41 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> List<&2, U32>

def even_b source · line 47 · raw

@+m:Nat -> @b:Nat -> @+x:Nat -> Nat

n - x when y is odd (the key or nonce whose point has even y)

def even source · line 52 · raw

@+m:Nat -> @+y:Nat -> @+x:Nat -> Nat

def lift_if source · line 59 · raw

@+one:Nat -> @+x:Nat -> @ok:Bool -> Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SPoint>

lift_x(x): the point with x-coordinate x and even y, if x < p and x^3 + 7 is a square

def lift_x source · line 64 · raw

@+one:Nat -> @+x:Nat -> Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SPoint>

def check_r source · line 68 · raw

@+r:Nat -> @inf:Bool -> @a:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SAffine -> Bool

fail if is_infinite(R) or not has_even_y(R) or x(R) != r

def verify_rs source · line 73 · raw

@+one:Nat -> @+r:Nat -> @+s:Nat -> @+e:Nat -> @+pp:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SPoint -> Bool

R = s G - e P with e = int(hash_challenge(r || pk || m)) mod n

def verify_ok source · line 77 · raw

@+one:Nat -> @+r:Nat -> @+s:Nat -> @+e:Nat -> @+pp:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SPoint -> @ok:Bool -> Bool

def verify_p source · line 83 · raw

@+one:Nat -> @+pk:List<&2, U32> -> @+m:List<&2, U32> -> @+sig:List<&2, U32> -> @mp:Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SPoint> -> Bool

fail if r >= p or s >= n

def verify_len source · line 92 · raw

@+one:Nat -> @+pk:List<&2, U32> -> @+m:List<&2, U32> -> @+sig:List<&2, U32> -> @ok:Bool -> Bool

def verify source · line 98 · raw

@+one:Nat -> @+pk:List<&2, U32> -> @+m:List<&2, U32> -> @+sig:List<&2, U32> -> Bool

Verify(pk, m, sig): pk 32 bytes, sig 64 bytes, m any length

def secret_ok source · line 104 · raw

@+one:Nat -> @+sk:List<&2, U32> -> Bool

d' = int(sk), 1 <= d' <= n - 1

def pub_of source · line 107 · raw

@a:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SAffine -> List<&2, U32>

def pubkey_ok source · line 111 · raw

@+one:Nat -> @+sk:List<&2, U32> -> @ok:Bool -> Maybe<&2, List<&2, U32>>

def pubkey source · line 117 · raw

@+one:Nat -> @+sk:List<&2, U32> -> Maybe<&2, List<&2, U32>>

PubKey(sk) = bytes(d' G)

def sign_if source · line 122 · raw

@+sig:List<&2, U32> -> @ok:Bool -> Maybe<&2, List<&2, U32>>

sig = bytes(R) || bytes((k + e d) mod n); if Verify(bytes(P), m, sig) fails, abort

def sign_fin source · line 127 · raw

@+one:Nat -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+sig:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def sign_r source · line 132 · raw

@+one:Nat -> @+d:Nat -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+k0:Nat -> @ra:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SAffine -> Maybe<&2, List<&2, U32>>

R = k' G; k = k' if has_even_y(R), otherwise n - k'; e = int(hash_challenge(bytes(R) || bytes(P) || m)) mod n

def sign_kz source · line 141 · raw

@+one:Nat -> @+d:Nat -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+k0:Nat -> @zero:Bool -> Maybe<&2, List<&2, U32>>

k' = int(rand) mod n; fail if k' = 0

def sign_k source · line 146 · raw

@+one:Nat -> @+d:Nat -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+k0:Nat -> Maybe<&2, List<&2, U32>>

def sign_p source · line 151 · raw

@+one:Nat -> @+d0:Nat -> @+m:List<&2, U32> -> @+aux:List<&2, U32> -> @pa:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SAffine -> Maybe<&2, List<&2, U32>>

P = d' G; d = d' if has_even_y(P), otherwise n - d'; t = bytes(d) xor hash_aux(a); rand = hash_nonce(t || bytes(P) || m)

def sign_ok source · line 159 · raw

@+one:Nat -> @+sk:List<&2, U32> -> @+m:List<&2, U32> -> @+aux:List<&2, U32> -> @ok:Bool -> Maybe<&2, List<&2, U32>>

def sign source · line 167 · raw

@+one:Nat -> @+sk:List<&2, U32> -> @+m:List<&2, U32> -> @+aux:List<&2, U32> -> Maybe<&2, List<&2, U32>>

Sign(sk, m, a): sk and a 32 bytes, m any length