signature_spec.lean

/-
  Specifications file for signature_spec.cairo

  Do not modify the constant definitions, structure definitions, or automatic specifications.
  Do not change the name or arguments of the user specifications and soundness theorems.

  You may freely move the definitions around in the file.
  You may add definitions and theorems wherever you wish in this file.
-/
import starkware.cairo.lean.semantics.soundness.prelude
import starkware.cairo.common.cairo_secp.ec_spec
import starkware.cairo.common.cairo_secp.bigint_spec
import starkware.cairo.common.cairo_secp.constants_spec
import starkware.cairo.common.cairo_secp.field_spec
import starkware.cairo.common.math_spec

import starkware.cairo.common.cairo_secp.ec_point_spec
import starkware.cairo.common.cairo_secp.bigint3_spec

open starkware.cairo.common.cairo_secp.ec_point
open starkware.cairo.common.cairo_secp.bigint3
open starkware.cairo.common.cairo_secp.ec
open starkware.cairo.common.cairo_secp.bigint
open starkware.cairo.common.cairo_secp.constants
open starkware.cairo.common.cairo_secp.field
open starkware.cairo.common.math

namespace starkware.cairo.common.cairo_secp.signature

variables {F : Type} [field F] [decidable_eq F] [prelude_hyps F]

--variables {secpF : Type} [secp_field secpF]

-- End of automatically generated prelude.

/-
-- Function: get_generator_point
-/

/- get_generator_point autogenerated specification -/

def gen_point {F : Type} [field F] [decidable_eq F] [prelude_hyps F] (mem : F → F) : EcPoint mem :=
  ⟨⟨17117865558768631194064792,
    12501176021340589225372855,
    9198697782662356105779718⟩,
   ⟨6441780312434748884571320,
     57953919405111227542741658,
     5457536640262350763842127⟩⟩

def gen_point_data (F : Type) [field F] [decidable_eq F] [prelude_hyps F] (mem : F → F)
    (secpF : Type) [secp_field secpF]:
  BddECPointData secpF (gen_point mem) :=
{ ix := ⟨17117865558768631194064792,
         12501176021340589225372855,
         9198697782662356105779718⟩,
  iy := ⟨6441780312434748884571320,
         57953919405111227542741658,
         5457536640262350763842127⟩,
  ixbdd := begin
             rw [bigint3.bounded, BASE], simp_int_casts,
             repeat { rw [abs_of_nonneg] },
             repeat { norm_num }
            end,
  iybdd := begin
             rw [bigint3.bounded, BASE], simp_int_casts,
             repeat { rw [abs_of_nonneg] },
             repeat { norm_num }
            end,
  ptxeq := by { rw [gen_point, bigint3.toBigInt3], simp_int_casts, exact ⟨rfl, rfl, rfl⟩ },
  ptyeq := by { rw [gen_point, bigint3.toBigInt3], simp_int_casts, exact ⟨rfl, rfl, rfl⟩ },
  onEC :=
    begin
      right,
      rw [←int.cast_pow, ←int.cast_pow, (show (7 : secpF) = (7 : int), by simp_int_casts),
        ←int.cast_add, char_p.int_cast_eq_int_cast secpF SECP_PRIME, bigint3.val, bigint3.val,
        SECP_PRIME_eq, int.modeq, BASE, SECP_REM],
      dsimp, simp_int_casts, norm_num,
    end }

-- Do not change this definition.
def auto_spec_get_generator_point (mem : F → F) (κ : ℕ) (ρ_point : EcPoint mem) : Prop :=
  7 ≤ κ ∧
  ρ_point = {
    x := { d0 := 17117865558768631194064792, d1 := 12501176021340589225372855, d2 := 9198697782662356105779718 },
    y := { d0 := 6441780312434748884571320, d1 := 57953919405111227542741658, d2 := 5457536640262350763842127 }
  }

-- You may change anything in this definition except the name and arguments.
def spec_get_generator_point (mem : F → F) (κ : ℕ) (ρ_point : EcPoint mem) : Prop :=
  ρ_point = gen_point mem

/- get_generator_point soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_get_generator_point
    {mem : F → F}
    (κ : ℕ)
    (ρ_point : EcPoint mem)
    (h_auto : auto_spec_get_generator_point mem κ ρ_point) :
  spec_get_generator_point mem κ ρ_point :=
begin
  exact h_auto.2
end

-- Function: div_mod_n

/- div_mod_n autogenerated specification -/

-- Do not change this definition.
def auto_spec_div_mod_n (mem : F → F) (κ : ℕ) (range_check_ptr : F) (a b : BigInt3 mem) (ρ_range_check_ptr : F) (ρ_res : BigInt3 mem) : Prop :=
  ∃ (κ₁ : ℕ) (range_check_ptr₁ : F) (res : BigInt3 mem), spec_nondet_bigint3 mem κ₁ range_check_ptr range_check_ptr₁ res ∧
  ∃ (κ₂ : ℕ) (range_check_ptr₂ : F) (k : BigInt3 mem), spec_nondet_bigint3 mem κ₂ range_check_ptr₁ range_check_ptr₂ k ∧
  ∃ (κ₃ : ℕ) (res_b : UnreducedBigInt5 mem), spec_bigint_mul mem κ₃ res b res_b ∧
  ∃ n : BigInt3 mem, n = {
    d0 := N0,
    d1 := N1,
    d2 := N2
  } ∧
  ∃ (κ₄ : ℕ) (k_n : UnreducedBigInt5 mem), spec_bigint_mul mem κ₄ k n k_n ∧
  ∃ carry1 : F, carry1 = (res_b.d0 - k_n.d0 - a.d0) / (BASE : ℤ) ∧
  mem (range_check_ptr₂ + 0) = carry1 + 2 ^ 127 ∧
  is_range_checked (rc_bound F) (carry1 + 2 ^ 127) ∧
  ∃ carry2 : F, carry2 = (res_b.d1 - k_n.d1 - a.d1 + carry1) / (BASE : ℤ) ∧
  mem (range_check_ptr₂ + 1) = carry2 + 2 ^ 127 ∧
  is_range_checked (rc_bound F) (carry2 + 2 ^ 127) ∧
  ∃ carry3 : F, carry3 = (res_b.d2 - k_n.d2 - a.d2 + carry2) / (BASE : ℤ) ∧
  mem (range_check_ptr₂ + 2) = carry3 + 2 ^ 127 ∧
  is_range_checked (rc_bound F) (carry3 + 2 ^ 127) ∧
  ∃ carry4 : F, carry4 = (res_b.d3 - k_n.d3 + carry3) / (BASE : ℤ) ∧
  mem (range_check_ptr₂ + 3) = carry4 + 2 ^ 127 ∧
  is_range_checked (rc_bound F) (carry4 + 2 ^ 127) ∧
  res_b.d4 - k_n.d4 + carry4 = 0 ∧
  ∃ range_check_ptr₃ : F, range_check_ptr₃ = range_check_ptr₂ + 4 ∧
  κ₁ + κ₂ + κ₃ + κ₄ + 48 ≤ κ ∧
  ρ_range_check_ptr = range_check_ptr₃ ∧
  ρ_res = res

-- You may change anything in this definition except the name and arguments.
def spec_div_mod_n (mem : F → F) (κ : ℕ) (range_check_ptr : F) (a b : BigInt3 mem) (ρ_range_check_ptr : F) (ρ_res : BigInt3 mem) : Prop :=
  ∀ ia : bigint3,
    ia.bounded (3 * BASE - 1) →
    a = ia.toBigInt3 →
  ∀ ib : bigint3,
    ib.bounded (3 * BASE - 1) →
    b = ib.toBigInt3 →
  ∃ ires : bigint3,
    ires.bounded (3 * BASE - 1) ∧
    ρ_res = ires.toBigInt3 ∧
    ires.val * ib.val ≡ ia.val [ZMOD secp_n]

/- div_mod_n soundness theorem -/

def iN0 : ℤ := N0
def iN1 : ℤ := N1
def iN2 : ℤ := N2

def secp_in : bigint3 := ⟨iN0, iN1, iN2⟩

def nBASE := BASE

--theorem secp_in_toBigInt3 : secp_in.toBigInt3 = secp_n := rfl

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_div_mod_n
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (a b : BigInt3 mem) (ρ_range_check_ptr : F) (ρ_res : BigInt3 mem)
    (h_auto : auto_spec_div_mod_n mem κ range_check_ptr a b ρ_range_check_ptr ρ_res) :
  spec_div_mod_n mem κ range_check_ptr a b ρ_range_check_ptr ρ_res :=
begin
  intros ia iabdd aeq ib ibbdd beq,
  rcases h_auto with ⟨_, _, res, hres, _, _, k, hk, _, res_b, hres_b, n, neq, _, k_n, hk_n,
    carry1, carry1eq, _, hcarry1,
    carry2, carry2eq, _, hcarry2,
    carry3, carry3eq, _, hcarry3,
    carry4, carry4eq, _, hcarry4,
    diff_eq, _, _, _, _, ρ_res_eq⟩,
  rcases nondet_bigint3_corr hres with ⟨ires, reseq, ires_bdd⟩,
  rcases nondet_bigint3_corr hk with ⟨ik, keq, ik_bdd⟩,
  change _ = _ at hres_b,
  change _ = _ at hk_n,
  rcases rc_to_int hcarry1 with ⟨icarry1, carry1eq', carry1_bdd⟩,
  rcases rc_to_int hcarry2 with ⟨icarry2, carry2eq', carry2_bdd⟩,
  rcases rc_to_int hcarry3 with ⟨icarry3, carry3eq', carry3_bdd⟩,
  rcases rc_to_int hcarry4 with ⟨icarry4, carry4eq', carry4_bdd⟩,
  have BASEnonneg : 0 ≤ (BASE : ℤ) := int.coe_zero_le BASE,
  have iN0nonneg : 0 ≤ iN0 := int.coe_zero_le _,
  have iN1nonneg : 0 ≤ iN1 := int.coe_zero_le _,
  have iN2nonneg : 0 ≤ iN2 := int.coe_zero_le _,
  have absBASEeq : abs (BASE : ℤ) = BASE := abs_of_nonneg BASEnonneg,
  have BASEnz : ((BASE : ℤ) : F) ≠ 0,
  { suffices : ((2 : ℤ) : F) ≠ 0,
      by simpa using this,
    haveI : char_p F PRIME := prelude_hyps.charF,
    rw [ne, char_p.int_cast_eq_zero_iff F PRIME, PRIME],
    simp_int_casts, norm_num },
  have aux3 : ∀ {x y : F}, x = y / (BASE : ℤ) → x * 2 ^ 86 = y,
  { intros x y xeq,
    rw [eq_div_iff BASEnz, int.cast_coe_nat, BASE] at xeq,
    simp only [nat.cast_bit0, nat.cast_one, nat.cast_pow] at xeq,
    exact xeq },
  have secp_in_toBigInt3 : secp_in.toBigInt3 = n,
  { rw [neq, bigint3.toBigInt3, secp_in], dsimp,
    rw [iN0, iN1, iN2, int.cast_coe_nat, int.cast_coe_nat, int.cast_coe_nat] },
  have : (((((ires.bigint5_mul ib).sub (ik.bigint5_mul secp_in)).sub ia.to_bigint5).add
          ⟨0, icarry1, icarry2, icarry3, 0⟩).toUnreducedBigInt5 : UnreducedBigInt5 mem) =
      bigint5.toUnreducedBigInt5
        (⟨icarry1*BASE, icarry2*BASE, icarry3*BASE, icarry4*BASE, -icarry4⟩),
  { rw [bigint5.toUnreducedBigInt5_add, bigint5.toUnreducedBigInt5_sub,
        bigint5.toUnreducedBigInt5_sub, bigint3.bigint5_mul_toUnreducedBigInt5,
        bigint3.bigint5_mul_toUnreducedBigInt5],
    conv { to_rhs, rw [bigint5.toUnreducedBigInt5], simp },
    rw [←carry1eq', aux3 carry1eq, ←carry2eq', aux3 carry2eq, ←carry3eq', aux3 carry3eq,
      ←carry4eq', aux3 carry4eq, ←reseq, ←keq, ←beq, ←hres_b, secp_in_toBigInt3, ←hk_n,
      bigint3.to_bigint5_to_Unreduced_BigInt5, ←aeq],
    simp [UnreducedBigInt5.sub, UnreducedBigInt5.add,
      starkware.cairo.common.cairo_secp.bigint.bigint3.to_bigint5, bigint5.toUnreducedBigInt5,
        BigInt3.toUnreducedBigInt5],
    simp [carry1eq', carry2eq', carry3eq', eq_sub_of_add_eq diff_eq] },
  have eq :  ((((ires.bigint5_mul ib).sub (ik.bigint5_mul secp_in)).sub ia.to_bigint5).add
          ⟨0, icarry1, icarry2, icarry3, 0⟩) =
        ⟨icarry1*BASE, icarry2*BASE, icarry3*BASE, icarry4*BASE, -icarry4⟩,
  { apply bigint5.toUnreducedBigInt5_eq_of_sub_bounded this,
    have : (2^127 : ℤ) * BASE + (3 * (3 * BASE - 1)^2 +
      (3 * (3 * (BASE - 1))^2) + (3 * BASE - 1) + 2^127) ≤ PRIME - 1,
    { rw [PRIME, BASE], simp_int_casts, norm_num },
    apply bigint5.bounded_of_bounded_of_le _ this,
    apply bigint5.bounded_sub,
    { simp [bigint5.bounded, abs_mul, absBASEeq],
      use [carry1_bdd, carry2_bdd, carry3_bdd, carry4_bdd],
      apply le_trans carry4_bdd, norm_num },
    apply bigint5.bounded_add, swap,
    { simp [bigint5.bounded],
      use [carry1_bdd, carry2_bdd, carry3_bdd] },
    apply bigint5.bounded_sub _ (bigint3.to_bigint5_bounded iabdd),
    apply bigint5.bounded_sub,
    apply bigint3.bounded_bigint5_mul (bigint3.bounded_of_bounded_of_le ires_bdd bound_slack) ibbdd,
    apply bigint3.bounded_bigint5_mul ik_bdd,
    rw [secp_in, bigint3.bounded], dsimp,
    simp [abs_of_nonneg iN0nonneg, abs_of_nonneg iN1nonneg, abs_of_nonneg iN2nonneg],
    simp [iN0, iN1, iN2],
    norm_num,  },
  have : ires.val * ib.val = ik.val * secp_n + ia.val,
  { simp only [bigint3.val, secp_n, int.cast_add, int.coe_nat_add, int.coe_nat_mul],
    rw [int.coe_nat_pow BASE 2],
    set iBASE := (BASE : ℤ),
    simp only [bigint3.bigint5_mul, bigint5.add, bigint5.sub, bigint3.to_bigint5, secp_in, add_zero, sub_zero] at eq,
    rcases eq with ⟨eq1, eq2, eq3, eq4, eq5⟩,
    rw [←iN0, ←iN1, ←iN2],
    transitivity (ires.i2 * ib.i2 * iBASE * iBASE * iBASE * iBASE) +
      (ires.i2 * iBASE ^ 2 * (ib.i1 * iBASE + ib.i0)) +
      (ires.i1 * iBASE + ires.i0) * (ib.i2 * iBASE ^ 2 + ib.i1 * iBASE + ib.i0),
    rw [pow_two], ring,
    rw [eq_add_of_sub_eq eq5, add_mul, add_mul, add_mul],
    rw [←neg_mul_eq_neg_mul, ←eq4, neg_add],
    simp only [add_mul _ _ iBASE],
    rw [←neg_mul_eq_neg_mul icarry3, ←eq3, neg_add],
    simp only [add_mul _ _ iBASE],
    rw [←neg_mul_eq_neg_mul icarry2, ←eq2, neg_add],
    simp only [add_mul _ _ iBASE],
    rw [←neg_mul_eq_neg_mul icarry1, ←eq1],
    ring },
  use ires,
  split, apply bigint3.bounded_of_bounded_of_le ires_bdd bound_slack,
  use ρ_res_eq.trans reseq,
  rw [this, int.modeq, add_comm, int.add_mul_mod_self]
end

/-
-- Function: get_point_from_x
-/

/- get_point_from_x autogenerated specification -/

-- Do not change this definition.
def auto_spec_get_point_from_x (mem : F → F) (κ : ℕ) (range_check_ptr : F) (x : BigInt3 mem) (v ρ_range_check_ptr : F) (ρ_point : EcPoint mem) : Prop :=
  ∃ (κ₁ : ℕ) (range_check_ptr₁ : F), spec_assert_nn mem κ₁ range_check_ptr v range_check_ptr₁ ∧
  ∃ (κ₂ : ℕ) (x_square : UnreducedBigInt3 mem), spec_unreduced_sqr mem κ₂ x x_square ∧
  ∃ (κ₃ : ℕ) (range_check_ptr₂ : F) (x_square_reduced : BigInt3 mem), spec_reduce mem κ₃ range_check_ptr₁ x_square range_check_ptr₂ x_square_reduced ∧
  ∃ (κ₄ : ℕ) (x_cube : UnreducedBigInt3 mem), spec_unreduced_mul mem κ₄ x x_square_reduced x_cube ∧
  ∃ (κ₅ : ℕ) (range_check_ptr₃ : F) (y : BigInt3 mem), spec_nondet_bigint3 mem κ₅ range_check_ptr₂ range_check_ptr₃ y ∧
  ∃ (κ₆ : ℕ) (range_check_ptr₄ : F), spec_validate_reduced_field_element mem κ₆ range_check_ptr₃ y range_check_ptr₄ ∧
  ∃ (κ₇ : ℕ) (range_check_ptr₅ : F), spec_assert_nn mem κ₇ range_check_ptr₄ ((y.d0 + v) / (2 : ℤ)) range_check_ptr₅ ∧
  ∃ (κ₈ : ℕ) (y_square : UnreducedBigInt3 mem), spec_unreduced_sqr mem κ₈ y y_square ∧
  ∃ (κ₉ : ℕ) (range_check_ptr₆ : F), spec_verify_zero mem κ₉ range_check_ptr₅ {
    d0 := x_cube.d0 + BETA - y_square.d0,
    d1 := x_cube.d1 - y_square.d1,
    d2 := x_cube.d2 - y_square.d2
  } range_check_ptr₆ ∧
  κ₁ + κ₂ + κ₃ + κ₄ + κ₅ + κ₆ + κ₇ + κ₈ + κ₉ + 54 ≤ κ ∧
  ρ_range_check_ptr = range_check_ptr₆ ∧
  ρ_point = {
    x := x,
    y := y
  }

theorem aux {a b c : ℕ} (h : a + b = 2 * c) : a % 2 = b % 2 :=
begin
  have : a + 2 * b = 2 * c + b,
  { nth_rewrite 0 (two_mul b),
    rw [←add_assoc, h] },
  have h' := congr_arg (λ n : ℕ, n % 2) this,
  dsimp at h',
  rw [nat.add_mul_mod_self_left, add_comm, nat.add_mul_mod_self_left] at h',
  exact h'
end

-- You may change anything in this definition except the name and arguments.
def spec_get_point_from_x (mem : F → F) (κ : ℕ) (range_check_ptr : F) (x : BigInt3 mem) (v ρ_range_check_ptr : F) (ρ_point : EcPoint mem) : Prop :=
   ∀ (secpF : Type) [hsecp : secp_field secpF],
   by exactI
      x ≠ ⟨0, 0, 0⟩ →
      ∀ ix : bigint3,
        ix.bounded (3 * BASE - 1) →
        x = ix.toBigInt3 →
        ∃ nv : ℕ,
          nv < rc_bound F ∧
          v = ↑nv ∧
        ∃ iyval : ℕ,
          iyval < SECP_PRIME ∧
          nv % 2 = iyval % 2 ∧
        ∃ h : @on_ec secpF _ (ix.val, iyval),
        ∃ hres : BddECPointData secpF ρ_point,
          hres.toECPoint = ECPoint.AffinePoint ⟨_, _, h⟩

/- get_point_from_x soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_get_point_from_x
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (x : BigInt3 mem) (v ρ_range_check_ptr : F) (ρ_point : EcPoint mem)
    (h_auto : auto_spec_get_point_from_x mem κ range_check_ptr x v ρ_range_check_ptr ρ_point) :
  spec_get_point_from_x mem κ range_check_ptr x v ρ_range_check_ptr ρ_point :=
begin
  intros secpF _,
  resetI,
  intros xnez ix ixbdd xeq,
  rcases h_auto with
    ⟨_, _, h_nn_v,
    _, x_square, h_x_square,
    _, _, x_square_reduced, h_x_square_reduced,
    _, x_cube, h_x_cube,
    _, _, y, h_nondet_bigint3_y,
    _, _, h_validate_reduced_y,
    _, _, h_nn_y_v_div,
    _, y_square, h_unreduced_y_square,
    _, _, h_verify_zero,
    _, _, ρ_point_eq⟩,
  rcases h_nn_v with ⟨nv, nvlt, veq⟩,
  have x_square_eq := h_x_square ix xeq,
  have : ix.sqr.bounded (2 ^ 249),
  { apply bigint3.bounded_of_bounded_of_le
      (bigint3.bounded_sqr ixbdd),
    rw [BASE, SECP_REM], simp_int_casts, norm_num },
  rcases h_x_square_reduced ix.sqr this x_square_eq with
    ⟨ixsqr', ixsqr'bdd, hixsqr', x_square_reduced_eq⟩,
  have x_cube_eq := h_x_cube ix ixsqr' xeq x_square_reduced_eq,
  rcases nondet_bigint3_corr h_nondet_bigint3_y with ⟨iy, yeq, iybdd⟩,
  rcases h_validate_reduced_y with ⟨n0, n1, n2, n0le, n1le, n2le, yvallt, yeq'⟩,
  rcases h_nn_y_v_div with ⟨nydiv, nydivlt, ydiveq⟩,
  have : y.d0 + v = ↑(2 * nydiv),
  { rw [mul_comm, nat.cast_mul],
    symmetry, simp,
    rw [← (eq_div_iff (PRIME.two_ne_zero F)), ← ydiveq],
    simp },
  have : n0 + nv = 2 * nydiv,
  { rw [yeq', veq, ← nat.cast_add] at this,
    apply nat.cast_inj_of_lt_char _ _ this,
    apply lt_of_le_of_lt (add_le_add n0le (le_of_lt nvlt)),
    apply lt_of_le_of_lt (add_le_add_left (rc_bound_hyp F) _),
    rw [BASE, PRIME.char_eq, PRIME],
    norm_num,
    apply lt_of_le_of_lt,
    apply nat.mul_le_mul_left 2
      (le_trans (le_of_lt nydivlt) (rc_bound_hyp F)),
    rw [PRIME.char_eq, PRIME], norm_num },
  have n02eqmv2 : n0 % 2 = nv % 2 := aux this,
  let  iy' : bigint3 := ⟨n0, n1, n2⟩,
  have iy'bdd : iy'.bounded (3 * ↑BASE - 1),
  { suffices : iy'.bounded BASE,
    { apply bigint3.bounded_of_bounded_of_le this,
      rw BASE, simp_int_casts, norm_num },
    simp only [bigint3.bounded, nat.abs_cast, int.coe_nat_le],
    split, { apply le_trans n0le tsub_le_self },
    split, { apply le_trans n1le tsub_le_self },
    apply le_trans n2le,
    norm_num [P2, BASE] },
  have yeq'' : y = iy'.toBigInt3,
  { rw [yeq', bigint3.toBigInt3], dsimp [iy'],
    simp only [int.cast_coe_nat, eq_self_iff_true, and_self] },
  have y_square_eq := h_unreduced_y_square iy' yeq'',
  let idiff := ((ix.mul ixsqr').add ⟨7,0,0⟩).sub iy'.sqr,
  have hidiff1 : idiff.toUnreducedBigInt3 = ⟨x_cube.d0 + ↑BETA - y_square.d0, x_cube.d1 - y_square.d1, x_cube.d2 - y_square.d2⟩,
  { simp [idiff, BETA, bigint3.toUnreducedBigInt3_add, bigint3.toUnreducedBigInt3_sub, x_cube_eq, y_square_eq],
    simp [bigint3.toUnreducedBigInt3, UnreducedBigInt3.add, UnreducedBigInt3.sub] },
  have hidiff2 : idiff.bounded (2 ^ 250),
  { suffices : idiff.bounded ((3 * BASE - 1)^2 * (8 * SECP_REM + 1) + 7 +
      (3 * BASE - 1)^2 * (8 * SECP_REM + 1)),
    { apply bigint3.bounded_of_bounded_of_le this,
     rw [BASE, SECP_REM], simp_int_casts, norm_num },
    apply bigint3.bounded_sub,
    apply bigint3.bounded_add,
    apply bigint3.bounded_mul ixbdd (bigint3.bounded_of_bounded_of_le ixsqr'bdd bound_slack),
    { simp [bigint3.bounded], rw abs_of_nonneg; norm_num },
    apply bigint3.bounded_sqr iy'bdd },
  have := h_verify_zero idiff hidiff1.symm hidiff2,
  have h_on_ec : on_ec ((ix.val : secpF), iy'.val),
  { simp [on_ec],
    suffices : (↑(iy'.val ^ 2) : secpF) = ↑(ix.val ^ 3 + 7),
    { simpa using this },
    rw [char_p.int_cast_eq_int_cast secpF SECP_PRIME, int.modeq],
    symmetry,
    rw [int.mod_eq_mod_iff_mod_sub_eq_zero, ←this],
    dsimp [idiff],
    rw [bigint3.sub_val, bigint3.add_val],
    apply int.modeq.sub,
    apply int.modeq.add,
    rw [pow_succ],
    apply int.modeq.symm,
    apply int.modeq.trans,
    apply bigint3.mul_val,
    apply int.modeq.mul_left,
    apply int.modeq.trans hixsqr',
    apply bigint3.sqr_val,
    { simp [bigint3.val] },
    apply int.modeq.symm,
    apply bigint3.sqr_val },
  have iy'valeq : (↑(n2 * BASE ^ 2 + n1 * BASE + n0) : secpF) = iy'.val,
  { dsimp [iy'], simp [bigint3.val] },
  use [nv, nvlt, veq, n2 * BASE ^ 2 + n1 * BASE + n0, yvallt],
  split,
  { rw [←n02eqmv2, nat.add_mod, nat.add_mod (n2 * _), nat.mul_mod, BASE],
    norm_num,
    rw [nat.add_mod, nat.mul_mod],
    norm_num },
  rw iy'valeq,
  use h_on_ec,
  rw ρ_point_eq,
  use ⟨ix, iy', ixbdd, iy'bdd, xeq, yeq'', or.inr h_on_ec⟩,
  simp [BddECPointData.toECPoint, dif_neg xnez]
end


/-
-- Function: recover_public_key
-/

/- recover_public_key autogenerated specification -/

-- Do not change this definition.
def auto_spec_recover_public_key (mem : F → F) (κ : ℕ) (range_check_ptr : F) (msg_hash r s : BigInt3 mem) (v ρ_range_check_ptr : F) (ρ_public_key_point : EcPoint mem) : Prop :=
  ∃ (κ₁ : ℕ) (range_check_ptr₁ : F) (r_point : EcPoint mem), spec_get_point_from_x mem κ₁ range_check_ptr r v range_check_ptr₁ r_point ∧
  ∃ (κ₂ : ℕ) (generator_point : EcPoint mem), spec_get_generator_point mem κ₂  generator_point ∧
  ∃ (κ₃ : ℕ) (range_check_ptr₂ : F) (u1 : BigInt3 mem), spec_div_mod_n mem κ₃ range_check_ptr₁ msg_hash r range_check_ptr₂ u1 ∧
  ∃ (κ₄ : ℕ) (range_check_ptr₃ : F) (u2 : BigInt3 mem), spec_div_mod_n mem κ₄ range_check_ptr₂ s r range_check_ptr₃ u2 ∧
  ∃ (κ₅ : ℕ) (range_check_ptr₄ : F) (point1 : EcPoint mem), spec_ec_mul mem κ₅ range_check_ptr₃ generator_point u1 range_check_ptr₄ point1 ∧
  ∃ (κ₆ : ℕ) (range_check_ptr₅ : F) (minus_point1 : EcPoint mem), spec_ec_negate mem κ₆ range_check_ptr₄ point1 range_check_ptr₅ minus_point1 ∧
  ∃ (κ₇ : ℕ) (range_check_ptr₆ : F) (point2 : EcPoint mem), spec_ec_mul mem κ₇ range_check_ptr₅ r_point u2 range_check_ptr₆ point2 ∧
  ∃ (κ₈ : ℕ) (range_check_ptr₇ : F) (public_key_point : EcPoint mem), spec_ec_add mem κ₈ range_check_ptr₆ minus_point1 point2 range_check_ptr₇ public_key_point ∧
  κ₁ + κ₂ + κ₃ + κ₄ + κ₅ + κ₆ + κ₇ + κ₈ + 77 ≤ κ ∧
  ρ_range_check_ptr = range_check_ptr₇ ∧
  ρ_public_key_point = public_key_point

-- You may change anything in this definition except the name and arguments.
def spec_recover_public_key (mem : F → F) (κ : ℕ) (range_check_ptr : F) (msg_hash r s : BigInt3 mem) (v ρ_range_check_ptr : F) (ρ_public_key_point : EcPoint mem) : Prop :=
  ∀ (secpF : Type) [secp_field secpF], by exactI
  r ≠ ⟨0, 0, 0⟩ →
  ∀ ir : bigint3,
    ir.bounded (3 * BASE - 1) →
    r = ir.toBigInt3 →
  ∀ is : bigint3,
    is.bounded (3 * BASE - 1) →
    s = is.toBigInt3 →
  ∀ imsg : bigint3,
    imsg.bounded (3 * BASE - 1) →
    msg_hash = imsg.toBigInt3 →
  ∃ nv : ℕ,
    nv < rc_bound F ∧
    v = ↑nv ∧
  ∃ iu1 iu2 : ℤ,
    iu1 * ir.val ≡ imsg.val [ZMOD secp_n] ∧
    iu2 * ir.val ≡ is.val [ZMOD secp_n] ∧
  ∃ ny : ℕ,
    ny < SECP_PRIME ∧
    nv ≡ ny [MOD 2] ∧
  ∃ h_on_ec : @on_ec secpF _ (ir.val, ny),
  ∃ hpoint  : BddECPointData secpF ρ_public_key_point,
    hpoint.toECPoint =
      -(iu1 • (gen_point_data F mem secpF).toECPoint) +
        iu2 • ECPoint.AffinePoint ⟨ir.val, ny, h_on_ec⟩

/- recover_public_key soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_recover_public_key
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (msg_hash r s : BigInt3 mem) (v ρ_range_check_ptr : F) (ρ_public_key_point : EcPoint mem)
    (h_auto : auto_spec_recover_public_key mem κ range_check_ptr msg_hash r s v ρ_range_check_ptr ρ_public_key_point) :
  spec_recover_public_key mem κ range_check_ptr msg_hash r s v ρ_range_check_ptr ρ_public_key_point :=
begin
  intros secpF _ rnez ir irbdd req is isbdd iseq imsg imsgbdd msgeq,
  resetI,
  rcases h_auto with ⟨_, _, r_point, hr_point,
    _, generator, hgenerator,
    _, _, u1, hu1,
    _, _, u2, hu2,
    _, _, point1, hpoint1,
    _, _, minus_point1, hminus_point1,
    _, _, point2, hpoint2,
    _, _, public_key_point, hpublic_key_point,
    _, _, rfl⟩,
  rcases hr_point secpF rnez ir irbdd req with ⟨nv, nvlt, veq, iy, iybdd, iy2, hiy, hr_point', ireq⟩,
  rw spec_get_generator_point at hgenerator,
  subst hgenerator,
  rcases hu1 imsg imsgbdd msgeq ir irbdd req with ⟨iu1, iu1bdd, u1eq, hu1'⟩,
  rcases hu2 is isbdd iseq ir irbdd req with ⟨iu2, iu2bdd, u2eq, hu2'⟩,
  have : (gen_point mem).x ≠ ⟨0, 0, 0⟩,
  { simp [gen_point],
    intros eq _ _,
    suffices : (17117865558768631194064792 : ℤ) = 0,
    { norm_num at this },
    haveI : char_p F PRIME := prelude_hyps.charF,
    apply int.cast_eq_zero_of_lt_char F PRIME,
    { simp_int_casts, exact eq },
    rw [abs_of_nonneg, PRIME],
    simp_int_casts, norm_num, norm_num },
  rcases hpoint1 secpF this (gen_point_data F mem secpF) with
    ⟨n10, n10lt, n10eq, n11, n11lt, n11eq, n12, n12lt, n12eq, hpoint1', hpoint1eq⟩,
  rcases spec_ec_negate'_of_spec_ec_negate hminus_point1 secpF hpoint1' with
    ⟨hminus_point1', hminus_point1_eq⟩,
  have : r_point.x ≠ ⟨0, 0, 0⟩,
  { intro hcontr,
    rw [BddECPointData.toECPoint, dif_pos hcontr] at ireq,
    contradiction },
  rcases hpoint2 secpF this hr_point' with
    ⟨n20, n20lt, n20eq, n21, n21lt, n21eq, n22, n22lt, n22eq, hpoint2', hpoint2eq⟩,
  rcases hpublic_key_point secpF hminus_point1' hpoint2' with ⟨hret, hreteq⟩,
  refine ⟨nv, nvlt, veq, _, _, hu1', hu2', iy, iybdd, iy2, hiy, hret, _⟩,
  rw [hreteq, hminus_point1_eq, hpoint1eq, hpoint2eq, ireq],
  have aux : ∀ {i : ℤ} {n : ℕ}, abs i ≤ 3 * BASE - 1 → n < 2^86 → (i : F) = (n : F) → i = n,
  { intros i n hi hn hin,
    have : (i : F) = ((n : ℤ) : F),
    { rw hin, simp },
    apply PRIME.int_coe_inj this,
    have : (2^86 : ℤ) + (3 * BASE - 1) < PRIME,
    { simp only [PRIME], simp_int_casts, norm_num },
    apply lt_of_le_of_lt _ this,
    apply le_trans,
    apply abs_sub,
    apply add_le_add _ hi,
    rw abs_of_nonneg (int.coe_zero_le _),
    apply le_of_lt,
    norm_cast, exact hn },
  simp [u1eq, u2eq, bigint3.toBigInt3] at n10eq n11eq n12eq n20eq n21eq n22eq,
  have : iu1.val = ↑(2 ^ 172 * n12 + 2 ^ 86 * n11 + n10),
  { rw [bigint3.val], simp,
    rw [aux iu1bdd.1 n10lt n10eq, aux iu1bdd.2.1 n11lt n11eq,
        aux iu1bdd.2.2 (lt_of_lt_of_le n12lt (by norm_num)) n12eq ],
        ring },
  rw [this, nsmul_eq_smul_cast ℤ],
  have : iu2.val = ↑(2 ^ 172 * n22 + 2 ^ 86 * n21 + n20),
  { rw [bigint3.val], simp,
    rw [aux iu2bdd.1 n20lt n20eq, aux iu2bdd.2.1 n21lt n21eq,
        aux iu2bdd.2.2 (lt_of_lt_of_le n22lt (by norm_num)) n22eq ],
        ring },
  rw [this, nsmul_eq_smul_cast ℤ]
end


end starkware.cairo.common.cairo_secp.signature