Psign.fin_g: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend as Psign Lines 112-131 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend&start_line=112&end_line=131 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/ecdsa.bend as ES 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/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/ecdsa.bend as E 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/sel.bend as SL import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE # the end of signing on scalars r, s0 of values rv, sv def fin_g(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s0: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s0) == True{} : Bool}, +x: List<&2, Nat>, +y: List<&2, Nat>, +rv: Nat, +hrv: {FS.value(one, r) == rv : Nat}, +sv: Nat, +hsv: {FS.value(one, s0) == sv : Nat}) -> {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(rv, 0n), Nat.is_eq(sv, 0n)), List.append(&2, U32, CV.i2osp(32n, rv), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}: %Equal.sym(Nat, rv, FS.value(one, r), Equal.sym(Nat, FS.value(one, r), rv, hrv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(_, 0n), Nat.is_eq(sv, 0n)), List.append(&2, U32, CV.i2osp(32n, rv), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, rv, FS.value(one, r), Equal.sym(Nat, FS.value(one, r), rv, hrv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(sv, 0n)), List.append(&2, U32, CV.i2osp(32n, _), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(_, 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(_)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), _)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(_)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Bool, S.is_zero(r), Nat.is_eq(FS.value(one, r), 0n), FW.is_zero_s(one, h1, r)) : {matt(E.finish_if(Bool.or(_, S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Bool, S.is_zero(s0), Nat.is_eq(FS.value(one, s0), 0n), FW.is_zero_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), _), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(List<&2, U32>, B.to_be(r), CV.i2osp(32n, FS.value(one, r)), tbv(one, h1, r, SL.sl16(one, r, hr))) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{_, B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Bool, S.is_high(s0), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FW.is_high_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), B.to_be(S.select(E.b2n(_), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(List<&2, U32>, B.to_be(S.select(E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0)))), S.neg(s0), s0)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), sel_v(one, h1, Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), s0, hs)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), _, U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Bool, S.is_high(s0), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FW.is_high_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(_)), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Bool, S.is_high(s0), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FW.is_high_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(F.parity(y), E.b2n(_)), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Bool, S.lt_n(x), Nat.is_lt(FS.value(one, x), FS.order(one)), FW.lt_n_s(one, h1, x)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(_)), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(Nat.is_lt(FS.value(one, x), FS.order(one)))), 2n), Nat.sub(Nat.add(_, E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(Nat.is_lt(FS.value(one, x), FS.order(one)))), 2n), Nat.sub(Nat.add(Nat.mod(FS.value(one, y), 2n), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(_, E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} %Equal.sym(Nat, Nat.add(Nat.mul(E.b2n(Bool.not(Nat.is_lt(FS.value(one, x), FS.order(one)))), 2n), Nat.sub(Nat.add(Nat.mod(FS.value(one, y), 2n), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(Nat.mod(FS.value(one, y), 2n), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))), Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))), id_v(Nat.is_lt(FS.value(one, x), FS.order(one)), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n), PE.mod2_lt(FS.value(one, y)))) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(_)})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt} bad_v(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))}) Uses (46): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or 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=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend&name=is_high_s https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend&name=is_zero_s https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend&name=lt_n_s https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend&name=parity_f https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend&name=mod2_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend&name=bad_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend&name=id_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend&name=matt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend&name=sel_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend&name=tbv 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/ecdsa.bend&name=Attempt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=finish_if https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=flip https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=ge2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=low 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/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/ecdsa.bend&name=Signature https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=b2n https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=finish_if https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend&name=parity https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=is_high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=is_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=lt_n 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=select