1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/peth.src; edit the .src 2 import Base 3 import ../../../spec/crypto/secp256k1/curve.bend as CV 4 import ../../../spec/crypto/secp256k1/ecdsa.bend as ES 5 import ../../../src/crypto/secp256k1/bytes.bend as B 6 import ../../../src/crypto/secp256k1/ecdsa.bend as E 7 import ../keccak/laws.bend as KL 8 import ../keccak/proof.bend as KPF 9 import ./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 17 def 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 33 def pack_v(ws: List<&2, U32>, +i: U32, a: Array) -> {E.pack(ws, i, a) == ES.pack(ws, i, a) : Array}: 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 40 def 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 47 def digest_v(m: Maybe<&1, Array>) -> {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 54 def k64_v(+h1: E.Hash, +h2: ES.Hash, e: @a:Array -> @l:Nat -> {E.hash(h1, a, l) == ES.hash(h2, a, l) : Maybe<&1, Array>}, +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, 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>, 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 60 def 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 67 def 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 74 def 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 81 def eth_with_v(+h1: E.Hash, +h2: ES.Hash, e: @a:Array -> @l:Nat -> {E.hash(h1, a, l) == ES.hash(h2, a, l) : Maybe<&1, Array>}, +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 91 def kk(a: Array, +l: Nat) -> {E.hash(E.Keccak256{}, a, l) == ES.hash(ES.Keccak256{}, a, l) : Maybe<&1, Array>}: 92 KL.ethereum_keccak256(a, l) 93 94 def 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