spec/crypto/secp256k1/ecdsa.bend checks

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

5 imports

import Base
import ../hmac.bend as HM
import ../keccak/main.bend as KS
import ./field.bend as FS
import ./curve.bend as CV

Types

type Drbg source · line 44 · raw

Data

Drbg

@k:List<&2, U32> -> @v:List<&2, U32> -> Drbg

type Attempt source · line 70 · raw

Data

Retry
```
Attempt
```
Sig
```
@sig:List<&2, U32> -> Attempt
```

type Hash source · line 274 · raw

Data

The hash of addresses: Keccak-256 (spec/crypto/keccak/main.bend, 24 rounds), named by a value so that the proofs can keep it folded

Keccak256
```
Hash
```

Definitions

def p source · line 19 · raw

@+one:Nat -> Nat

def n source · line 22 · raw

@+one:Nat -> Nat

def cat source · line 25 · raw

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

def fill source · line 28 · raw

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

def i2osp32 source · line 31 · raw

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

def scalar_ok source · line 35 · raw

@+one:Nat -> @+x:Nat -> Bool

1 <= x < n

def hash_scalar source · line 39 · raw

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

e = bits2int(H) mod n (SEC 1 4.1.3 step 5; RFC 6979 2.3.2)

def hmac source · line 48 · raw

@key:List<&2, U32> -> @msg:List<&2, U32> -> List<&2, U32>

HMAC-SHA256 (the key is looked at first; the value is HM.hmac's)

def update_v source · line 53 · raw

@+k:List<&2, U32> -> @+v:List<&2, U32> -> Drbg

def update source · line 57 · raw

@+k:List<&2, U32> -> @+v:List<&2, U32> -> @+tag:U32 -> @+seed:List<&2, U32> -> Drbg

K = HMAC_K(V || tag || seed), V = HMAC_K(V)

def update2 source · line 60 · raw

@d:Drbg -> @+seed:List<&2, U32> -> Drbg

def drbg_init source · line 65 · raw

@+seed:List<&2, U32> -> Drbg

steps b-g, with seed = int2octets(x) || bits2octets(h1)

def flip source · line 75 · raw

@b:Bool -> @+par:Nat -> Nat

0 or 1 when b is

def low source · line 80 · raw

@high:Bool -> @+m:Nat -> @+s:Nat -> Nat

def ge2 source · line 85 · raw

@b:Bool -> Nat

def finish_if source · line 90 · raw

@bad:Bool -> @+sig:List<&2, U32> -> Attempt

def finish source · line 99 · raw

@+one:Nat -> @+e:Nat -> @+d:Nat -> @+k:Nat -> @a:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SAffine -> Attempt

R = (x, y) = [k] G, r = x mod n, s = k^-1 (e + r d) mod n; r = 0 or s = 0 means another k. s > n / 2 (n is odd: n < 2 s) becomes n - s. The recovery id is (y mod 2) + 2 (x >= n), with its low bit flipped when s was replaced.

def attempt_ok source · line 108 · raw

@+one:Nat -> @+e:Nat -> @+d:Nat -> @+k:Nat -> @ok:Bool -> Attempt

def attempt source · line 114 · raw

@+one:Nat -> @+e:Nat -> @+d:Nat -> @+v:List<&2, U32> -> Attempt

step h.3: k = bits2int(T) with T = V, used when 1 <= k < n

def sign_loop source · line 120 · raw

@fuel:Nat -> @+one:Nat -> @+e:Nat -> @+d:Nat -> @+k:List<&2, U32> -> @+v:List<&2, U32> -> @att:Attempt -> Maybe<&2, List<&2, U32>>

step h, with the retry of step h.3 (K = HMAC_K(V || 0x00), V = HMAC_K(V)) before the next V = HMAC_K(V); at most fuel candidates

def sign_drbg source · line 130 · raw

@+one:Nat -> @+e:Nat -> @+d:Nat -> @g:Drbg -> Maybe<&2, List<&2, U32>>

def sign_d source · line 136 · raw

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

def sign source · line 144 · raw

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

sign(sk, H): d = OS2IP(sk) must be a 32-byte key with 1 <= d < n, H 32 bytes

def pk_of source · line 149 · raw

@+one:Nat -> @compressed:Bool -> @+q:0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SPoint -> List<&2, U32>

def public_d source · line 154 · raw

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

def public_key source · line 160 · raw

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

the SEC 1 encoding of Q = [d] G

def verify_rs source · line 167 · raw

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

u1 = e s^-1, u2 = r s^-1, R = [u1] G + [u2] Q; valid when R is not the point at infinity and x(R) mod n = r

def verify_ok source · line 173 · raw

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

def verify_q source · line 179 · raw

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

r and s in [1, n - 1]; strict verification also rejects s > n / 2

def verify_len source · line 187 · raw

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

def verify source · line 193 · raw

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

verify(Q, H, r || s): Q a SEC 1 public key, H 32 bytes, r || s 64 bytes

def recover_q_if source · line 198 · raw

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

def recover_q source · line 203 · raw

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

def recover_r source · line 207 · raw

@+one:Nat -> @+e:Nat -> @+r:Nat -> @+s:Nat -> @mr:Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.SPoint> -> Maybe<&2, List<&2, U32>>

Q = r^-1 (s R - e G) = [-e r^-1] G + [s r^-1] R

def recover_x_if source · line 217 · raw

@+one:Nat -> @+e:Nat -> @+r:Nat -> @+s:Nat -> @+id:Nat -> @+x:Nat -> @ok:Bool -> Maybe<&2, List<&2, U32>>

R: the point of x-coordinate x = r + j n (j = id / 2, x < p) whose y has parity id mod 2

def recover_x source · line 222 · raw

@+one:Nat -> @+e:Nat -> @+r:Nat -> @+s:Nat -> @+id:Nat -> Maybe<&2, List<&2, U32>>

def recover_ok source · line 226 · raw

@+one:Nat -> @+e:Nat -> @+r:Nat -> @+s:Nat -> @+id:Nat -> @ok:Bool -> Maybe<&2, List<&2, U32>>

def recover_len source · line 231 · raw

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

def recover source · line 242 · raw

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

the 65-byte uncompressed key recovered from H (32 bytes) and r || s || id (65 bytes, id in 0..3)

def word source · line 249 · raw

@+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @+b3:U32 -> U32

Keccak-256 (spec/crypto/keccak/main.bend) of bytes packed into little-endian U32 words, as its interface takes them

def words source · line 252 · raw

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

def pack source · line 257 · raw

@ws:List<&2, U32> -> @+i:U32 -> @a:Array<U32> -> Array<U32>

def unpack source · line 262 · raw

@ws:List<&1, U32> -> List<&2, U32>

def digest_bytes source · line 267 · raw

@m:Maybe<&1, Array<U32>> -> List<&2, U32>

def hash source · line 277 · raw

@+h:Hash -> @a:Array<U32> -> @length:Nat -> Maybe<&1, Array<U32>>

def keccak64 source · line 281 · raw

@+h:Hash -> @+bs:List<&2, U32> -> List<&2, U32>

def eth_if source · line 285 · raw

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

address = the last 20 bytes of Keccak-256(x || y) of an uncompressed key

def eth_go source · line 290 · raw

@+h:Hash -> @+pk:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def eth_with source · line 295 · raw

@+h:Hash -> @pk:List<&2, U32> -> Maybe<&2, List<&2, U32>>

(the key is looked at first, so that the proof checker keeps an unknown address folded)

def eth_address source · line 300 · raw

@+pk:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def word_of source · line 303 · raw

@m:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, U32>>

def addr_word source · line 308 · raw

@m:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, U32>>

def all_zero source · line 313 · raw

@bs:List<&2, U32> -> Bool

def ecrecover_v source · line 318 · raw

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

def ecrecover_in source · line 323 · raw

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

def ecrecover source · line 332 · raw

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

ECRECOVER (precompile 0x01): the input zero-padded or cut to 128 bytes is H || v || r || s, v a 32-byte big-endian word that must be 27 or 28; the output is the address word (12 zero bytes, then the address) of the key recovered with id v - 27, or nothing