src/crypto/secp256k1.bend

bend-collections-laws-crypto@1.0.0.0 · 117 lines · 19 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend as Sch
4
5# secp256k1 signatures: ECDSA (SEC 1 v2 section 4.1) with RFC 6979
6# deterministic nonces and low-S output, public key recovery (Ethereum's
7# ecrecover), Ethereum addresses, and BIP-340 Schnorr signatures.
8#
9# Byte convention: bytes are U32 values below 256; keys, hashes and
10# signatures are byte lists of their standard lengths, and a malformed one
11# is rejected as a value (None / False), never a crash.
12#
13#   generate_keypair(seed)        secret = the 32-byte seed if 1 <= seed < n,
14#                                 public = its 33-byte compressed SEC 1 key
15#   generate_keypair_os()         the same from IO.random_u32 (drawn again
16#                                 while the seed is not a valid key)
17#   public_key(sk, compressed)    33-byte (02/03) or 65-byte (04) SEC 1 key
18#   sign(sk, hash32)              Signature{r, s, v}: RFC 6979 nonce, low s,
19#                                 v the recovery id 0..3
20#   sign_compact(sk, hash32)      r || s || v, 65 bytes
21#   verify(pk, hash32, sig64)     SEC 1 verification of r || s (high s allowed)
22#   verify_strict(pk, h, sig64)   the same, high s rejected (BIP 146 LOW_S)
23#   recover(hash32, sig65)        the 65-byte public key of r || s || id
24#   eth_address(pk65)             the 20-byte Ethereum address
25#   ecrecover(input)              Ethereum's precompile 0x01: 128 bytes
26#                                 hash || v || r || s -> the address word
27#   schnorr_pubkey(sk)            BIP-340 32-byte x-only public key
28#   schnorr_sign(sk, msg, aux32)  BIP-340 64-byte signature
29#   schnorr_verify(pk32, msg, sig64)
30#
31# Every function is proved equal to its specification
32# (spec/crypto/secp256k1/, transcribed from SEC 1/SEC 2, RFC 6979 and
33# BIP-340) for every input: proofs/crypto/secp256k1/, clauses in
34# docs/CRYPTO_CONTRACTS.md. Scalar multiplication by secrets and all
35# secret-dependent arithmetic are branch-free (masked selection over
36# complete formulas); Bend has no timing model, so constant time is by
37# construction, not proved.
38
39type Keypair is Data:
40  Keypair{secret: List<&2, U32>, public: List<&2, U32>}
41
42def keypair_of(+seed: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, Keypair>:
43  match m:
44    case None{}: None{}
45    case Some{pk}: Some{Keypair{seed, pk}}
46
47def generate_keypair(+seed: List<&2, U32>) -> Maybe<&2, Keypair>:
48  keypair_of(seed, E.public_key(seed, True{}))
49
50def word_bytes(+w: U32, rest: List<&2, U32>) -> List<&2, U32>:
51  U32.and(w, 255) <> U32.and(U32.shrn(w, 8n), 255) <> U32.and(U32.shrn(w, 16n), 255) <> U32.shrn(w, 24n) <> rest
52
53def random_bytes(n: Nat, acc: List<&2, U32>) -> IO(List<&2, U32>):
54  match n:
55    case 0n:
56      IO.pure(List<&2, U32>, acc)
57    case 1n+m:
58      do IO<List<&2, U32>>:
59        w : U32 <- IO.try(U32, IO.random_u32())
60        rest : List<&2, U32> <- random_bytes(m, acc)
61        return word_bytes(w, rest)
62
63def os_retry(fuel: Nat, m: Maybe<&2, Keypair>) -> IO(Maybe<&2, Keypair>):
64  match fuel m:
65    case _ Some{kp}:
66      IO.pure(Maybe<&2, Keypair>, Some{kp})
67    case 0n None{}:
68      IO.pure(Maybe<&2, Keypair>, None{})
69    case 1n+f None{}:
70      do IO<Maybe<&2, Keypair>>:
71        seed : List<&2, U32> <- random_bytes(8n, Nil{})
72        kp : Maybe<&2, Keypair> <- os_retry(f, generate_keypair(seed))
73        return kp
74
75# 32 bytes of the operating system's random source (getrandom, arc4random,
76# crypto.getRandomValues) as the seed; a seed outside [1, n - 1] (chance
77# 2^-128) is drawn again, up to 8 times
78def generate_keypair_os() -> IO(Maybe<&2, Keypair>):
79  os_retry(8n, None{})
80
81def public_key(+sk: List<&2, U32>, compressed: Bool) -> Maybe<&2, List<&2, U32>>:
82  E.public_key(sk, compressed)
83
84def sign(+sk: List<&2, U32>, +hash: List<&2, U32>) -> Maybe<&2, E.Signature>:
85  E.sign(sk, hash)
86
87def compact(m: Maybe<&2, E.Signature>) -> Maybe<&2, List<&2, U32>>:
88  match m:
89    case None{}: None{}
90    case Some{E.Signature{r, s, v}}: Some{List.append(&2, U32, r, List.append(&2, U32, s, [v]))}
91
92def sign_compact(+sk: List<&2, U32>, +hash: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
93  compact(E.sign(sk, hash))
94
95def verify(+pk: List<&2, U32>, +hash: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
96  E.verify(pk, hash, sig)
97
98def verify_strict(+pk: List<&2, U32>, +hash: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
99  E.verify_strict(pk, hash, sig)
100
101def recover(+hash: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
102  E.recover(hash, sig)
103
104def eth_address(+pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
105  E.eth_address(pk)
106
107def ecrecover(input: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
108  E.ecrecover(input)
109
110def schnorr_pubkey(+sk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
111  Sch.pubkey(sk)
112
113def schnorr_sign(+sk: List<&2, U32>, +msg: List<&2, U32>, +aux: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
114  Sch.sign(sk, msg, aux)
115
116def schnorr_verify(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
117  Sch.verify(pk, msg, sig)