def vlen

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

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/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/bytes.bend as BY
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE

196def vlen(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, a: Bool, b: Bool, +ha: {B.has_len(32n, pk) == a : Bool}, +hb: {B.has_len(64n, sig) == b : Bool}) -> {SC.verify_len(pk, m, sig, Bool.and(a, b)) == SS.verify_len(one, pk, m, sig, Bool.and(a, b)) : Bool}:
197  match a b:
198    case True{} True{}:
199      +hl = BY.of_be_limbs(one, h1, pk, ha)
200      %Equal.sym(Nat, CV.os2ip(pk), FS.value(one, B.of_be(pk)), Equal.sym(Nat, FS.value(one, B.of_be(pk)), CV.os2ip(pk), BY.of_be_value(one, h1, pk))) : {SC.verify_p(pk, m, sig, SC.lift_x(B.of_be(pk))) == SS.verify_p(one, pk, m, sig, SS.lift_x(one, _)) : Bool}
201      %Equal.sym(Maybe<&2, CV.SPoint>, SS.lift_x(one, FS.value(one, B.of_be(pk))), PE.mpv(one, SC.lift_x(B.of_be(pk))), Equal.sym(Maybe<&2, CV.SPoint>, PE.mpv(one, SC.lift_x(B.of_be(pk))), SS.lift_x(one, FS.value(one, B.of_be(pk))), lx(one, h1, B.of_be(pk), hl))) : {SC.verify_p(pk, m, sig, SC.lift_x(B.of_be(pk))) == SS.verify_p(one, pk, m, sig, _) : Bool}
202      vp(one, h1, pk, m, sig, hb, SC.lift_x(B.of_be(pk)), lx_r(one, h1, B.of_be(pk), hl))
203    case True{} False{}:
204      {==}
205    case False{} _:
206      {==}