proofs/crypto/secp256k1/peth.bend

bend-collections-laws-crypto@1.0.0.0 · 96 lines · 11 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/peth.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/laws.bend as KL
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/proof.bend as KPF
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
10
11# Ethereum addresses of
12# src/crypto/secp256k1/ecdsa.bend against spec/crypto/secp256k1/ecdsa.bend.
13# The hash is a parameter (kf) on both sides: the steps are proved for
14# any two equal hash functions, which keeps Keccak itself folded, and are
15# instantiated with the Keccak-256 implementation and specification.
16
17def words_v(n: Nat, +bs: List<&2, U32>) -> {E.words(n, bs) == ES.words(n, bs) : List<&2, U32>}:
18  match n:
19    case 0n:
20      {==}
21    case 1n+ +k:
22      %Equal.sym(List<&2, U32>, B.tail(bs), CV.after(1n, bs), BL.tail_after(bs)) : {E.word(B.head(bs), B.head(_), B.head(B.suffix(2n, bs)), B.head(B.suffix(3n, bs))) <> E.words(k, B.suffix(4n, bs)) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
23      %Equal.sym(List<&2, U32>, B.suffix(2n, bs), CV.after(2n, bs), BL.suffix_after(2n, bs)) : {E.word(B.head(bs), B.head(CV.after(1n, bs)), B.head(_), B.head(B.suffix(3n, bs))) <> E.words(k, B.suffix(4n, bs)) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
24      %Equal.sym(List<&2, U32>, B.suffix(3n, bs), CV.after(3n, bs), BL.suffix_after(3n, bs)) : {E.word(B.head(bs), B.head(CV.after(1n, bs)), B.head(CV.after(2n, bs)), B.head(_)) <> E.words(k, B.suffix(4n, bs)) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
25      %Equal.sym(List<&2, U32>, B.suffix(4n, bs), CV.after(4n, bs), BL.suffix_after(4n, bs)) : {E.word(B.head(bs), B.head(CV.after(1n, bs)), B.head(CV.after(2n, bs)), B.head(CV.after(3n, bs))) <> E.words(k, _) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
26      %Equal.sym(U32, B.head(bs), CV.head(bs), BL.head_eq(bs)) : {E.word(_, B.head(CV.after(1n, bs)), B.head(CV.after(2n, bs)), B.head(CV.after(3n, bs))) <> E.words(k, CV.after(4n, bs)) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
27      %Equal.sym(U32, B.head(CV.after(1n, bs)), CV.head(CV.after(1n, bs)), BL.head_eq(CV.after(1n, bs))) : {E.word(CV.head(bs), _, B.head(CV.after(2n, bs)), B.head(CV.after(3n, bs))) <> E.words(k, CV.after(4n, bs)) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
28      %Equal.sym(U32, B.head(CV.after(2n, bs)), CV.head(CV.after(2n, bs)), BL.head_eq(CV.after(2n, bs))) : {E.word(CV.head(bs), CV.head(CV.after(1n, bs)), _, B.head(CV.after(3n, bs))) <> E.words(k, CV.after(4n, bs)) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
29      %Equal.sym(U32, B.head(CV.after(3n, bs)), CV.head(CV.after(3n, bs)), BL.head_eq(CV.after(3n, bs))) : {E.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), _) <> E.words(k, CV.after(4n, bs)) == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
30      %Equal.sym(List<&2, U32>, E.words(k, CV.after(4n, bs)), ES.words(k, CV.after(4n, bs)), words_v(k, CV.after(4n, bs))) : {E.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> _ == ES.word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> ES.words(k, CV.after(4n, bs)) : List<&2, U32>}
31      {==}
32
33def pack_v(ws: List<&2, U32>, +i: U32, a: Array<U32>) -> {E.pack(ws, i, a) == ES.pack(ws, i, a) : Array<U32>}:
34  match ws:
35    case Nil{}:
36      {==}
37    case +w <> t:
38      pack_v(t, U32.inc(i), Array.set(U32, a, i, w))
39
40def unpack_v(ws: List<&1, U32>) -> {E.unpack(ws) == ES.unpack(ws) : List<&2, U32>}:
41  match ws:
42    case Nil{}:
43      {==}
44    case +w <> t:
45      Equal.cong(List<&2, U32>, List<&2, U32>, l => U32.and(w, 255) <> U32.and(U32.shrn(w, 8n), 255) <> U32.and(U32.shrn(w, 16n), 255) <> U32.shrn(w, 24n) <> l, E.unpack(t), ES.unpack(t), unpack_v(t))
46
47def digest_v(m: Maybe<&1, Array<U32>>) -> {E.digest_bytes(m) == ES.digest_bytes(m) : List<&2, U32>}:
48  match m:
49    case None{}:
50      {==}
51    case Some{a}:
52      unpack_v(Array.to_list(~U32, a))
53
54def k64_v(+h1: E.Hash, +h2: ES.Hash, e: @a:Array<U32> -> @l:Nat -> {E.hash(h1, a, l) == ES.hash(h2, a, l) : Maybe<&1, Array<U32>>}, +bs: List<&2, U32>) -> {E.keccak64(h1, bs) == ES.keccak64(h2, bs) : List<&2, U32>}:
55  %Equal.sym(List<&2, U32>, E.words(16n, bs), ES.words(16n, bs), words_v(16n, bs)) : {E.digest_bytes(E.hash(h1, E.pack(_, 0, Array.new(U32, 4n, 0)), 64n)) == ES.digest_bytes(ES.hash(h2, ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n)) : List<&2, U32>}
56  %Equal.sym(Array<U32>, E.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), pack_v(ES.words(16n, bs), 0, Array.new(U32, 4n, 0))) : {E.digest_bytes(E.hash(h1, _, 64n)) == ES.digest_bytes(ES.hash(h2, ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n)) : List<&2, U32>}
57  %Equal.sym(Maybe<&1, Array<U32>>, E.hash(h1, ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n), ES.hash(h2, ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n), e(ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n)) : {E.digest_bytes(_) == ES.digest_bytes(ES.hash(h2, ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n)) : List<&2, U32>}
58  digest_v(ES.hash(h2, ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n))
59
60def eth_if_v(b: Bool, +dg: List<&2, U32>) -> {E.eth_if(b, dg) == ES.eth_if(b, dg) : Maybe<&2, List<&2, U32>>}:
61  match b:
62    case True{}:
63      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, B.suffix(12n, dg), CV.after(12n, dg), BL.suffix_after(12n, dg))
64    case False{}:
65      {==}
66
67def ew_is(+h: E.Hash, pk: List<&2, U32>) -> {E.eth_with(h, pk) == E.eth_go(h, pk) : Maybe<&2, List<&2, U32>>}:
68  match pk:
69    case Nil{}:
70      {==}
71    case b <> t:
72      {==}
73
74def sw_is(+h: ES.Hash, pk: List<&2, U32>) -> {ES.eth_with(h, pk) == ES.eth_go(h, pk) : Maybe<&2, List<&2, U32>>}:
75  match pk:
76    case Nil{}:
77      {==}
78    case b <> t:
79      {==}
80
81def eth_with_v(+h1: E.Hash, +h2: ES.Hash, e: @a:Array<U32> -> @l:Nat -> {E.hash(h1, a, l) == ES.hash(h2, a, l) : Maybe<&1, Array<U32>>}, +pk: List<&2, U32>) -> {E.eth_with(h1, pk) == ES.eth_with(h2, pk) : Maybe<&2, List<&2, U32>>}:
82  %Equal.sym(Maybe<&2, List<&2, U32>>, E.eth_with(h1, pk), E.eth_go(h1, pk), ew_is(h1, pk)) : {_ == ES.eth_with(h2, pk) : Maybe<&2, List<&2, U32>>}
83  %Equal.sym(Maybe<&2, List<&2, U32>>, ES.eth_with(h2, pk), ES.eth_go(h2, pk), sw_is(h2, pk)) : {E.eth_go(h1, pk) == _ : Maybe<&2, List<&2, U32>>}
84  %Equal.sym(Bool, B.has_len(65n, pk), CV.length_is(65n, pk), BL.hl_is(65n, pk)) : {E.eth_if(Bool.and(_, U32.is_eq(B.head(pk), 4)), E.keccak64(h1, B.tail(pk))) == ES.eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), ES.keccak64(h2, CV.after(1n, pk))) : Maybe<&2, List<&2, U32>>}
85  %Equal.sym(U32, B.head(pk), CV.head(pk), BL.head_eq(pk)) : {E.eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(_, 4)), E.keccak64(h1, B.tail(pk))) == ES.eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), ES.keccak64(h2, CV.after(1n, pk))) : Maybe<&2, List<&2, U32>>}
86  %Equal.sym(List<&2, U32>, B.tail(pk), CV.after(1n, pk), BL.tail_after(pk)) : {E.eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), E.keccak64(h1, _)) == ES.eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), ES.keccak64(h2, CV.after(1n, pk))) : Maybe<&2, List<&2, U32>>}
87  %Equal.sym(List<&2, U32>, E.keccak64(h1, CV.after(1n, pk)), ES.keccak64(h2, CV.after(1n, pk)), k64_v(h1, h2, e, CV.after(1n, pk))) : {E.eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), _) == ES.eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), ES.keccak64(h2, CV.after(1n, pk))) : Maybe<&2, List<&2, U32>>}
88  eth_if_v(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), ES.keccak64(h2, CV.after(1n, pk)))
89
90# the Keccak-256 implementation is its specification
91def kk(a: Array<U32>, +l: Nat) -> {E.hash(E.Keccak256{}, a, l) == ES.hash(ES.Keccak256{}, a, l) : Maybe<&1, Array<U32>>}:
92  KL.ethereum_keccak256(a, l)
93
94def eth_address_v(+pk: List<&2, U32>) -> {E.eth_address(pk) == ES.eth_address(pk) : Maybe<&2, List<&2, U32>>}:
95  eth_with_v(E.Keccak256{}, ES.Keccak256{}, a => l => kk(a, l), pk)
96