def k64_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/peth.bend:54

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E

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))