Pschn.sk_v: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend as Pschn Lines 230-247 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&start_line=230&end_line=247 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/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/scalarops.bend as SO 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 def sk_v(+one: Nat, +h1: {one == 1n : Nat}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: List<&2, Nat>, +hk0: {FS.reduced(one, FS.order(one), k0) == True{} : Bool}, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.sign_k(d, pb, m, k0, a) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), PA.av(one, a)) : Maybe<&2, List<&2, U32>>}: match a: case P.Affine{+rx, +ry}: +hrx = ax_l(one, rx, ry, ha) +hk = even_r(one, h1, ry, k0, hk0) +he = th_r(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))) +hm = SO.mul_r(one, h1, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d, he, hd) +hs = SO.add_r(one, h1, S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d), hk, hm) %Equal.sym(List<&2, U32>, B.to_be(rx), CV.i2osp(32n, FS.value(one, rx)), tbv(one, h1, rx, hrx)) : {SC.sign_fin(pb, m, List.append(&2, U32, _, B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, B.to_be(rx), List.append(&2, U32, pb, m))))), d))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(List<&2, U32>, B.to_be(rx), CV.i2osp(32n, FS.value(one, rx)), tbv(one, h1, rx, hrx)) : {SC.sign_fin(pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, _, List.append(&2, U32, pb, m))))), d))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(List<&2, U32>, SC.tag_challenge(), SS.tag_challenge(), tc()) : {SC.sign_fin(pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, List<&2, U32>>, SC.sign_fin(pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))))), SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))))), sfin(one, h1, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)))))) : {_ == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(List<&2, U32>, B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))), CV.i2osp(32n, FS.value(one, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)))), tbv(one, h1, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)), SL.sl16(one, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)), hs))) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), _)) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(Nat, FS.value(one, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))), FS.madd(FS.order(one), FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), FS.value(one, S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))), SO.add_v(one, h1, S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d), hk, hm)) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, _))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(Nat, FS.value(one, S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)), FS.mmul(FS.order(one), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))))), FS.value(one, d)), SO.mul_v(one, h1, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d, he, hd)) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), _)))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(Nat, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))))), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), th_v(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), FS.mmul(FS.order(one), _, FS.value(one, d)))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} %Equal.sym(Nat, FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), even_v(one, h1, ry, k0, hk0)) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), _, FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>} {==} Uses (48): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=ared https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=av https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=ax_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=even_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=even_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=sfin https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=tbv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=tc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=th_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=th_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=add_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=add_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=mul_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=mul_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=sl16 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=i2osp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=os2ip https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=madd https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=mmul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=order https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=reduced https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=even https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=sign_fin https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=sign_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=tag_challenge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=tagged https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=of_be https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=to_be https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=Affine https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=neg https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=reduce https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=select https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=is_odd https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=sign_fin https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=sign_k https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=tag_challenge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=tagged