# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/peth.src; edit the .src
import Base
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../../src/crypto/secp256k1/ecdsa.bend as E
import ../keccak/laws.bend as KL
import ../keccak/proof.bend as KPF
import ./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 specification
def 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)