Prec.rc3: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Prec
Lines 173-184 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&start_line=173&end_line=184

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

def 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>>}:
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  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)), {==})

Uses (38):
  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=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=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.add
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=np
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=order_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=pp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=prime_eq
  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/prec.bend&name=r_lt_n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=rfl_b
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=rxg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=x1_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=x1_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=m1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=n_lt_p
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=rn_cond
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=l16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=sel1
  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/ecdsa.bend&name=recover_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=recover_x_if
  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=prime
  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/ecdsa.bend&name=recover_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=recover_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=rn_fe
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=select
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=lt_n