proofs/crypto/secp256k1/peth.bend source
proofs/crypto/secp256k1/peth.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/peth.src; edit the .srcimport Baseimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../spec/crypto/secp256k1/ecdsa.bend as ESimport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../../src/crypto/secp256k1/ecdsa.bend as Eimport ../keccak/laws.bend as KLimport ../keccak/proof.bend as KPFimport ./blist.bend as BL# Ethereum addresses of# src/crypto/secp256k1/ecdsa.bend against spec/crypto/secp256k1/ecdsa.bend.# The hash is a parameter (kf) on both sides: the steps are proved for# any two equal hash functions, which keeps Keccak itself folded, and are# instantiated with the Keccak-256 implementation and specification.def words_v(n: Nat, +bs: List<&2, U32>) -> {E.words(n, bs) == ES.words(n, bs) : List<&2, U32>}: match n: case 0n: {==} case 1n+ +k: %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} {==}def pack_v(ws: List<&2, U32>, +i: U32, a: Array<U32>) -> {E.pack(ws, i, a) == ES.pack(ws, i, a) : Array<U32>}: match ws: case Nil{}: {==} case +w <> t: pack_v(t, U32.inc(i), Array.set(U32, a, i, w))def unpack_v(ws: List<&1, U32>) -> {E.unpack(ws) == ES.unpack(ws) : List<&2, U32>}: match ws: case Nil{}: {==} case +w <> t: 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))def digest_v(m: Maybe<&1, Array<U32>>) -> {E.digest_bytes(m) == ES.digest_bytes(m) : List<&2, U32>}: match m: case None{}: {==} case Some{a}: unpack_v(Array.to_list(~U32, a))def 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>}: %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>} %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>} %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>} digest_v(ES.hash(h2, ES.pack(ES.words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n))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>>}: match b: case True{}: 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)) case False{}: {==}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>>}: match pk: case Nil{}: {==} case b <> t: {==}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>>}: match pk: case Nil{}: {==} case b <> t: {==}def 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>>}: %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} eth_if_v(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), ES.keccak64(h2, CV.after(1n, pk)))# the Keccak-256 implementation is its specificationdef kk(a: Array<U32>, +l: Nat) -> {E.hash(E.Keccak256{}, a, l) == ES.hash(ES.Keccak256{}, a, l) : Maybe<&1, Array<U32>>}: KL.ethereum_keccak256(a, l)def eth_address_v(+pk: List<&2, U32>) -> {E.eth_address(pk) == ES.eth_address(pk) : Maybe<&2, List<&2, U32>>}: eth_with_v(E.Keccak256{}, ES.Keccak256{}, a => l => kk(a, l), pk)