def rc3

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

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/scalar.bend as S
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/consts.bend as K
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/rconst.bend as RC

173def rc3(+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, 3n, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, True{}) : Maybe<&2, List<&2, U32>>}:
174  %Equal.sym(List<&2, Nat>, L.select(1n, E.rn_fe(r), r), E.rn_fe(r), SL.sel1(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, 3n, _, Bool.not(S.lt_n(E.rn_fe(r)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
175  %Equal.sym(Bool, S.lt_n(E.rn_fe(r)), Nat.is_lt(FS.value(one, E.rn_fe(r)), FS.order(one)), FW.lt_n_s(one, h1, E.rn_fe(r))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(_)) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
176  %Equal.sym(Nat, FS.value(one, E.rn_fe(r)), Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), x1_v(one, h1, r, hr)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(_, FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
177  %Equal.sym(Nat, Nat.mul(1n, FS.order(one)), FS.order(one), RC.m1(FS.order(one))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
178  %Equal.sym(Nat, Nat.mul(1n, FS.order(one)), FS.order(one), RC.m1(FS.order(one))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), FS.order(one)), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
179  %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), _))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), FS.order(one)), Nat.is_lt(Nat.add(FS.value(one, r), FS.order(one)), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
180  %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), FS.order(one)), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
181  %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
182  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), _)) : Maybe<&2, List<&2, U32>>}
183  %Equal.sym(Bool, Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one))), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), RC.rn_cond(FS.value(one, r), 1n+K.np(one), K.pp(one), r_lt_n(one, h1, r, hr), RC.n_lt_p(one, h1), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), rfl_b(Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one))))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), _) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one))) : Maybe<&2, List<&2, U32>>}
184  rxg(one, h1, z, hz, r, hr, s, hs, 3n, E.rn_fe(r), x1_r(one, h1, r, hr), Nat.add(FS.value(one, r), 1n+K.np(one)), x1_v(one, h1, r, hr), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), {==})