~/bend-docscommunity

src/crypto/secp256k1/ecdsa.bend checks

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

8 imports
import Base
import ../mac.bend as MAC
import ../keccak/keccak.bend as K
import ./limbs.bend as L
import ./field.bend as F
import ./scalar.bend as S
import ./point.bend as P
import ./bytes.bend as B

Types

type Signature source · line 19 · raw

Data

type Drbg source · line 35 · raw

Data

type Attempt source · line 75 · raw

Data

type Hash source · line 307 · raw

Data

The hash of addresses, as a value (only Keccak-256 exists), so that the proofs can keep it folded

Definitions

def scalar_ok source · line 25 · raw

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

1 <= x < n

def hash_scalar source · line 30 · raw

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

a 32-byte string as a scalar mod n (bits2int with qlen = hlen = 256, reduced: SEC 1 section 4.1.3 step 5, RFC 6979 section 2.3.2)

def hmac source · line 40 · raw

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

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

def cat source · line 45 · raw

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

def fill source · line 48 · raw

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

def drbg_v source · line 51 · raw

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

def drbg_step source · line 56 · raw

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

steps b-g: V = 0x01..., K = 0x00..., then two HMAC rounds over V || 0x00 || int2octets(x) || bits2octets(h1) and V || 0x01 || ...

def drbg_second source · line 59 · raw

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

def drbg_init source · line 63 · raw

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

def drbg_next source · line 67 · raw

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

step h.3: K = HMAC_K(V || 0x00), V = HMAC_K(V)

def b2n source · line 72 · raw

@b:Bool -> Nat

def finish_if source · line 79 · raw

@bad:Bool -> @+sig:Signature -> Attempt

def finish source · line 87 · raw

@+z:List<&2, Nat> -> @+d:List<&2, Nat> -> @+k:List<&2, Nat> -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> Attempt

r = x(R) mod n, s = k^-1 (z + r d) mod n, made low (s > n / 2 is replaced by n - s, which flips the parity bit of the recovery id); the recovery id is the parity of y(R), plus 2 when x(R) >= n

def attempt_aff source · line 95 · raw

@+z:List<&2, Nat> -> @+d:List<&2, Nat> -> @+k:List<&2, Nat> -> @a:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Affine -> Attempt

def attempt_ok source · line 99 · raw

@+z:List<&2, Nat> -> @+d:List<&2, Nat> -> @+k:List<&2, Nat> -> @ok:Bool -> Attempt

def attempt source · line 105 · raw

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

the candidate k = bits2int(V) (RFC 6979 step h.3): used when 1 <= k < n

def sign_loop source · line 114 · raw

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

step h: the candidate V; a k outside [1, n - 1], or one giving r = 0 or s = 0 (SEC 1 section 4.1.3 steps 3 and 6), is replaced by the next candidate: K = HMAC_K(V || 0x00), V = HMAC_K(V), V = HMAC_K(V). The loop stops after fuel candidates (the chance that even 2 are needed is below 2^-127).

def sign_drbg source · line 124 · raw

@+z:List<&2, Nat> -> @+d:List<&2, Nat> -> @g:Drbg -> Maybe<&2, Signature>

def secret_if source · line 130 · raw

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

def secret source · line 136 · raw

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

the secret key d, when 1 <= d < n

def sign_d source · line 142 · raw

@+h:List<&2, U32> -> @m:Maybe<&2, List<&2, Nat>> -> Maybe<&2, Signature>

sign with a valid secret scalar d: x = int2octets(d), h1' = bits2octets(h) = int2octets(bits2int(h) mod n)

def sign_h source · line 149 · raw

@+sk:List<&2, U32> -> @+h:List<&2, U32> -> @ok:Bool -> Maybe<&2, Signature>

def sign source · line 155 · raw

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

the low-S signature of a 32-byte hash under a 32-byte secret key

def public_point source · line 160 · raw

@+d:List<&2, Nat> -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Point

def pk_of source · line 163 · raw

@compressed:Bool -> @+q:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Point -> List<&2, U32>

def public_key_d source · line 168 · raw

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

def public_key source · line 174 · raw

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

the SEC 1 encoding of [d] G (33 bytes compressed, 65 uncompressed)

def verify_rs source · line 181 · raw

@+q:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Point -> @+z:List<&2, Nat> -> @+r:List<&2, Nat> -> @+s:List<&2, Nat> -> Bool

u1 = z w, u2 = r w with w = s^-1; R = [u1] G + [u2] Q must not be the point at infinity and x(R) mod n must be r

def verify_ok source · line 186 · raw

@+q:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Point -> @+z:List<&2, Nat> -> @+r:List<&2, Nat> -> @+s:List<&2, Nat> -> @ok:Bool -> Bool

def verify_q source · line 191 · raw

@+h:List<&2, U32> -> @+sig:List<&2, U32> -> @strict:Bool -> @m:Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Point> -> Bool

def verify_len source · line 199 · raw

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

def verify_with source · line 204 · raw

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

def verify source · line 209 · raw

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

SEC 1 verification of a 64-byte r || s against a SEC 1 public key (33 or 65 bytes); high s is accepted, as SEC 1 and OpenSSL do

def verify_strict source · line 214 · raw

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

the same, rejecting s > n / 2 (Bitcoin's BIP 62/146 LOW_S rule, Ethereum's homestead rule for transactions)

def recover_q source · line 219 · raw

@+q:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Point -> @inf:Bool -> Maybe<&2, List<&2, U32>>

def recover_r source · line 226 · raw

@+z:List<&2, Nat> -> @+r:List<&2, Nat> -> @+s:List<&2, Nat> -> @m:Maybe<&2, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.Point> -> Maybe<&2, List<&2, U32>>

Q = r^-1 (s R - z G), with R the point of x-coordinate r + n j (j = id / 2) and y parity id mod 2

def recover_x source · line 234 · raw

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

def cn_fe source · line 240 · raw

List<&2, Nat>

c_n = 2^256 - n and c_p = 2^256 - p as 16-limb field elements

def cp_fe source · line 243 · raw

List<&2, Nat>

def rn_fe source · line 247 · raw

@+r:List<&2, Nat> -> List<&2, Nat>

(r + n) mod p = (r - c_n + 2^256) mod p = (r - c_n + c_p) mod p

def recover_ok source · line 252 · raw

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

x = r + j n with j = id / 2. For j = 1, r + n must be below p: then (r + n) mod p = r + n >= n, while a wrapped r + n - p is below r < n

def recover_sig source · line 260 · raw

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

def recover_len source · line 266 · raw

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

def recover source · line 276 · raw

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

the 65-byte uncompressed public key that signed the 32-byte hash, from a 65-byte r || s || id with id in 0..3 (go-ethereum's crypto.Ecrecover; Ethereum's precompile passes id = v - 27); None when r or s is not in [1, n - 1], x(R) is not a field element on the curve, or Q is infinity. High s is accepted, as the precompile does.

def word source · line 282 · raw

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

little-endian U32 words of bytes (a missing byte reads as 0)

def words source · line 285 · raw

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

def pack source · line 290 · raw

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

def unpack source · line 295 · raw

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

def digest_bytes source · line 300 · raw

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

def hash source · line 310 · raw

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

def keccak64 source · line 315 · raw

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

the hash of 64 bytes

def eth_if source · line 318 · raw

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

def eth_go source · line 323 · raw

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

def eth_with source · line 328 · 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 335 · raw

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

the 20-byte Ethereum address of a 65-byte uncompressed public key: the last 20 bytes of Keccak-256 of its 64 coordinate bytes

def zeros_ok source · line 340 · raw

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

def eth_word source · line 345 · raw

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

def addr_word source · line 350 · raw

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

def ecrecover_v source · line 355 · raw

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

def ecrecover_in source · line 360 · raw

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

def ecrecover source · line 370 · raw

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

The precompile's semantics (Ethereum yellow paper appendix E): the input, zero-padded or cut to 128 bytes, is hash || v || r || s (32 bytes each, big-endian); v must be 27 or 28. The output is the 32-byte word holding the signer's address, or None (the precompile's empty output) when v, r or s is invalid or no key is recovered.