def rlen

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:232

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/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E

232def rlen(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +sig: List<&2, U32>, a: Bool, b: Bool, +ha: {B.has_len(32n, h) == a : Bool}, +hb: {B.has_len(65n, sig) == b : Bool}) -> {E.recover_len(h, sig, Bool.and(a, b)) == ES.recover_len(one, h, sig, Bool.and(a, b)) : Maybe<&2, List<&2, U32>>}:
233  match a b:
234    case True{} True{}:
235      rsig(one, h1, h, ha, sig, hb)
236    case True{} False{}:
237      {==}
238    case False{} _:
239      {==}