def ecv

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pecr.bend:37

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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as PR

37def ecv(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +rs: List<&2, U32>, +v: U32, ok: Bool) -> {E.ecrecover_v(h, rs, v, ok) == ES.ecrecover_v(one, h, rs, v, ok) : Maybe<&2, List<&2, U32>>}:
38  match ok:
39    case True{}:
40      %Equal.sym(Maybe<&2, List<&2, U32>>, E.recover(h, List.append(&2, U32, rs, [U32.sub(v, 27)])), ES.recover(one, h, List.append(&2, U32, rs, [U32.sub(v, 27)])), PR.recover_v(one, h1, h, List.append(&2, U32, rs, [U32.sub(v, 27)]))) : {E.addr_word(_) == ES.addr_word(ES.recover(one, h, List.append(&2, U32, rs, [U32.sub(v, 27)]))) : Maybe<&2, List<&2, U32>>}
41      aw_v(ES.recover(one, h, List.append(&2, U32, rs, [U32.sub(v, 27)])))
42    case False{}:
43      {==}