def fin_g

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/psign.bend:112
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend as Psign
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

112# the end of signing on scalars r, s0 of values rv, sv
113def 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}:
114  %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}
115  %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}
116  %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}
117  %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}
118  %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}
119  %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}
120  %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}
121  %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}
122  %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}
123  %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}
124  %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}
125  %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}
126  %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}
127  %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}
128  %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}
129  %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}
130  %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}
131  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)

Used by (1)

bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign:fin_v