def va

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

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/field.bend as F
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/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

108def va(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +inf: Bool, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.verify_aff(r, inf, a) == SS.check_r(FS.value(one, r), inf, PA.av(one, a)) : Bool}:
109  match a:
110    case P.Affine{+x, +y}:
111      +hx = SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha))
112      %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(_, 0n), F.eq(x, r))) == Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(FS.value(one, y), 2n), 0n), Nat.is_eq(FS.value(one, x), FS.value(one, r)))) : Bool}
113      %Equal.sym(Bool, F.eq(x, r), Nat.is_eq(FS.value(one, x), FS.value(one, r)), FW.eq_f(one, h1, x, r, hx, hr)) : {Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(FS.value(one, y), 2n), 0n), _)) == Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(FS.value(one, y), 2n), 0n), Nat.is_eq(FS.value(one, x), FS.value(one, r)))) : Bool}
114      {==}