def vok

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

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/schnorr.bend as SS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
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/point.bend as PT

143def vok(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hlr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +s: List<&2, Nat>, +hls: {FS.limbs16(one, 16n, s) == True{} : Bool}, +e: List<&2, Nat>, +he: {FS.reduced(one, FS.order(one), e) == True{} : Bool}, +pp: P.Point, +hp: {PT.pred(one, pp) == True{} : Bool}, a: Bool, b: Bool, +ha: {Nat.is_lt(FS.value(one, r), FS.prime(one)) == a : Bool}, +hb: {Nat.is_lt(FS.value(one, s), FS.order(one)) == b : Bool}) -> {SC.verify_ok(r, s, e, pp, Bool.and(a, b)) == SS.verify_ok(one, FS.value(one, r), FS.value(one, s), FS.value(one, e), PT.pv(one, pp), Bool.and(a, b)) : Bool}:
144  match a b:
145    case True{} True{}:
146      vrs(one, h1, r, hlr, s, red_n(one, s, hls, hb), e, he, pp, hp)
147    case True{} False{}:
148      {==}
149    case False{} _:
150      {==}