def rxg

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

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/point.bend as P
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/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as RC

79def rxg(+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}, +id: Nat, +x: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}, +xv: Nat, +hxv: {FS.value(one, x) == Nat.mod(xv, 1n+K.pp(one)) : Nat}, c: Bool, +hc: {Nat.is_lt(xv, 1n+K.pp(one)) == c : Bool}) -> {E.recover_x(z, r, s, id, x, c) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), id, xv, c) : Maybe<&2, List<&2, U32>>}:
80  match c:
81    case True{}:
82      +e = Equal.trans(Nat, FS.value(one, x), Nat.mod(xv, 1n+K.pp(one)), xv, hxv, RC.mod_small(K.pp(one), xv, hc))
83      %Equal.sym(Nat, xv, FS.value(one, x), Equal.sym(Nat, FS.value(one, x), xv, e)) : {E.recover_r(z, r, s, P.decompress(x, Nat.mod(id, 2n))) == ES.recover_r(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), CV.decompress(FS.prime(one), _, Nat.mod(id, 2n))) : Maybe<&2, List<&2, U32>>}
84      %Equal.sym(Maybe<&2, CV.SPoint>, CV.decompress(FS.prime(one), FS.value(one, x), Nat.mod(id, 2n)), PE.mpv(one, P.decompress(x, Nat.mod(id, 2n))), Equal.sym(Maybe<&2, CV.SPoint>, PE.mpv(one, P.decompress(x, Nat.mod(id, 2n))), CV.decompress(FS.prime(one), FS.value(one, x), Nat.mod(id, 2n)), PE.decompress_v(one, h1, x, Nat.mod(id, 2n), hx, PE.mod2_lt(id)))) : {E.recover_r(z, r, s, P.decompress(x, Nat.mod(id, 2n))) == ES.recover_r(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), _) : Maybe<&2, List<&2, U32>>}
85      rr(one, h1, z, hz, r, hr, s, hs, P.decompress(x, Nat.mod(id, 2n)), PE.decompress_r(one, h1, x, Nat.mod(id, 2n), hx, PE.mod2_lt(id)))
86    case False{}:
87      {==}