def rc0

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:140

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/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
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/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K
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/rconst.bend as RC

140def rc0(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.recover_ok(z, r, s, 0n, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, True{}) : Maybe<&2, List<&2, U32>>}:
141  %Equal.sym(List<&2, Nat>, L.select(0n, E.rn_fe(r), r), r, SL.sel0(one, 16n, E.rn_fe(r), r, SL.l16(one, E.rn_fe(r), x1_r(one, h1, r, hr)), SL.sl16(one, r, hr))) : {E.recover_x(z, r, s, 0n, _, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
142  %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
143  %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), 0n), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
144  %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, _, Nat.is_lt(Nat.add(FS.value(one, r), 0n), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
145  %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), Nat.is_lt(_, FS.prime(one))) : Maybe<&2, List<&2, U32>>}
146  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), Nat.is_lt(FS.value(one, r), _)) : Maybe<&2, List<&2, U32>>}
147  %Equal.sym(Bool, Nat.is_lt(FS.value(one, r), 1n+K.pp(one)), True{}, r_lt_pp(one, h1, r, hr)) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), _) : Maybe<&2, List<&2, U32>>}
148  rxg(one, h1, z, hz, r, hr, s, hs, 0n, r, rp_red(one, h1, r, hr), FS.value(one, r), Equal.sym(Nat, Nat.mod(FS.value(one, r), 1n+K.pp(one)), FS.value(one, r), RC.mod_small(K.pp(one), FS.value(one, r), r_lt_pp(one, h1, r, hr))), True{}, r_lt_pp(one, h1, r, hr))