Prec.rsig: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Prec
Lines 210-230 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&start_line=210&end_line=230

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ

def rsig(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {B.has_len(32n, h) == True{} : Bool}, +sig: List<&2, U32>, +hsig: {B.has_len(65n, sig) == True{} : Bool}) -> {E.recover_sig(h, sig) == ES.recover_len(one, h, sig, True{}) : Maybe<&2, List<&2, U32>>}:
  +hlr = BY.of_be_limbs(one, h1, B.prefix(32n, sig), pl1(sig, hsig))
  +hls = BY.of_be_limbs(one, h1, B.prefix(32n, B.suffix(32n, sig)), pl2(sig, hsig))
  %Equal.sym(Bool, E.scalar_ok(B.of_be(B.prefix(32n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), SQ.scalar_ok_v(one, h1, B.of_be(B.prefix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(_, E.scalar_ok(B.of_be(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, CV.after(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Bool, E.scalar_ok(B.of_be(B.prefix(32n, B.suffix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig))))), SQ.scalar_ok_v(one, h1, B.of_be(B.prefix(32n, B.suffix(32n, sig))))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), _), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, CV.after(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, ES.hash_scalar(one, h), FS.value(one, E.hash_scalar(h)), Equal.sym(Nat, FS.value(one, E.hash_scalar(h)), ES.hash_scalar(one, h), SQ.hash_v(one, h1, h, hh))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, _, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, CV.after(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, _)), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, _)))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(_), CV.os2ip(CV.first(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(CV.first(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(_)), ES.scalar_ok(one, CV.os2ip(CV.first(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.first(32n, B.suffix(32n, sig)), B.prefix(32n, B.suffix(32n, sig)), Equal.sym(List<&2, U32>, B.prefix(32n, B.suffix(32n, sig)), CV.first(32n, B.suffix(32n, sig)), BL.prefix_first(32n, B.suffix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(_), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.first(32n, B.suffix(32n, sig)), B.prefix(32n, B.suffix(32n, sig)), Equal.sym(List<&2, U32>, B.prefix(32n, B.suffix(32n, sig)), CV.first(32n, B.suffix(32n, sig)), BL.prefix_first(32n, B.suffix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(_))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.after(64n, sig), B.suffix(64n, sig), Equal.sym(List<&2, U32>, B.suffix(64n, sig), CV.after(64n, sig), BL.suffix_after(64n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(_)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(List<&2, U32>, CV.after(64n, sig), B.suffix(64n, sig), Equal.sym(List<&2, U32>, B.suffix(64n, sig), CV.after(64n, sig), BL.suffix_after(64n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(_)), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(U32, CV.head(B.suffix(64n, sig)), B.head(B.suffix(64n, sig)), Equal.sym(U32, B.head(B.suffix(64n, sig)), CV.head(B.suffix(64n, sig)), BL.head_eq(B.suffix(64n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(_), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(U32, CV.head(B.suffix(64n, sig)), B.head(B.suffix(64n, sig)), Equal.sym(U32, B.head(B.suffix(64n, sig)), CV.head(B.suffix(64n, sig)), BL.head_eq(B.suffix(64n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(_), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), _, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, _), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), BY.of_be_value(one, h1, B.prefix(32n, B.suffix(32n, sig))))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), _, U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), BY.of_be_value(one, h1, B.prefix(32n, B.suffix(32n, sig))))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, _)), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>}
  rok(one, h1, E.hash_scalar(h), SQ.hash_r(one, h1, h, hh), B.of_be(B.prefix(32n, sig)), hlr, B.of_be(B.prefix(32n, B.suffix(32n, sig))), hls, U32.to_nat(B.head(B.suffix(64n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n), {==}, {==}, {==})

Uses (38):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend&name=head_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend&name=prefix_first
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend&name=suffix_after
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=of_be_limbs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=of_be_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=pl1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=pl2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=rok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=hash_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=hash_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=scalar_ok_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=after
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=head
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=os2ip
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=hash_scalar
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=recover_len
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=recover_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=scalar_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=has_len
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=head
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=of_be
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=prefix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=suffix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=hash_scalar
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=recover_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=recover_sig
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=scalar_ok