def rsig
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:210
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Prec
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
210def 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>>}:
211 +hlr = BY.of_be_limbs(one, h1, B.prefix(32n, sig), pl1(sig, hsig))
212 +hls = BY.of_be_limbs(one, h1, B.prefix(32n, B.suffix(32n, sig)), pl2(sig, hsig))
213 %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>>}
214 %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>>}
215 %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>>}
216 %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>>}
217 %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>>}
218 %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>>}
219 %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>>}
220 %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>>}
221 %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>>}
222 %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>>}
223 %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>>}
224 %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>>}
225 %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>>}
226 %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>>}
227 %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>>}
228 %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>>}
229 %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>>}
230 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), {==}, {==}, {==})