def s1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pschn.bend:316

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/schnorr.bend as SS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
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/schnorr.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL

316def s1(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>, a: Bool, +ha: {B.has_len(32n, aux) == a : Bool}) -> {SC.sign_len(sk, m, aux, a) == SS.sign_ok(one, sk, m, aux, Bool.and(a, SS.secret_ok(one, sk))) : Maybe<&2, List<&2, U32>>}:
317  match a:
318    case True{}:
319      %Equal.sym(Bool, B.has_len(32n, sk), CV.length_is(32n, sk), BL.hl_is(32n, sk)) : {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), Bool.and(_, Bool.and(Bool.not(S.is_zero(B.of_be(sk))), S.lt_n(B.of_be(sk)))))) == SS.sign_ok(one, sk, m, aux, Bool.and(CV.length_is(32n, sk), Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}
320      s2(one, h1, sk, m, aux, CV.length_is(32n, sk), BL.hl_is(32n, sk))
321    case False{}:
322      {==}