field_spec.lean

/-
  Specifications file for field_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.bigint_spec
import starkware.cairo.common.cairo_secp.constants_spec

import starkware.cairo.common.math_spec

import starkware.cairo.common.cairo_secp.bigint3_spec

open starkware.cairo.common.cairo_secp.bigint3
open starkware.cairo.common.math
open starkware.cairo.common.cairo_secp.bigint
open starkware.cairo.common.cairo_secp.constants

namespace starkware.cairo.common.cairo_secp.field

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

-- End of automatically generated prelude.


/-
-- Function: unreduced_mul
-/

/- unreduced_mul autogenerated specification -/

-- Do not change this definition.
def auto_spec_unreduced_mul (mem : F → F) (κ : ℕ) (a b : BigInt3 mem) (ρ_res_low : UnreducedBigInt3 mem) : Prop :=
  18 ≤ κ ∧
  ρ_res_low = {
    d0 := a.d0 * b.d0 + (a.d1 * b.d2 + a.d2 * b.d1) * (4 * SECP_REM),
    d1 := a.d0 * b.d1 + a.d1 * b.d0 + (a.d2 * b.d2) * (4 * SECP_REM),
    d2 := a.d0 * b.d2 + a.d1 * b.d1 + a.d2 * b.d0
  }

-- You may change anything in this definition except the name and arguments.
def spec_unreduced_mul (mem : F → F) (κ : ℕ) (a b : BigInt3 mem) (ρ_res_low : UnreducedBigInt3 mem) : Prop :=
  ∀ x y : bigint3, a = x.toBigInt3 → b = y.toBigInt3 →
    ρ_res_low = (x.mul y).toUnreducedBigInt3

/- unreduced_mul soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_unreduced_mul
    {mem : F → F}
    (κ : ℕ)
    (a b : BigInt3 mem) (ρ_res_low : UnreducedBigInt3 mem)
    (h_auto : auto_spec_unreduced_mul mem κ a b ρ_res_low) :
  spec_unreduced_mul mem κ a b ρ_res_low :=
begin
  intros x y aeq beq,
  apply eq.trans h_auto.2,
  rw [bigint3.mul, aeq, beq], simp [bigint3.toBigInt3, bigint3.toUnreducedBigInt3]
end

/-
-- Function: unreduced_sqr
-/

/- unreduced_sqr autogenerated specification -/

-- Do not change this definition.
def auto_spec_unreduced_sqr (mem : F → F) (κ : ℕ) (a : BigInt3 mem) (ρ_res_low : UnreducedBigInt3 mem) : Prop :=
  ∃ twice_d0 : F, twice_d0 = a.d0 * 2 ∧
  13 ≤ κ ∧
  ρ_res_low = {
    d0 := a.d0 * a.d0 + (a.d1 * a.d2) * (2 * 4 * SECP_REM),
    d1 := twice_d0 * a.d1 + (a.d2 * a.d2) * (4 * SECP_REM),
    d2 := twice_d0 * a.d2 + a.d1 * a.d1
  }

-- You may change anything in this definition except the name and arguments.
def spec_unreduced_sqr (mem : F → F) (κ : ℕ) (a : BigInt3 mem) (ρ_res_low : UnreducedBigInt3 mem) : Prop :=
  ∀ x : bigint3, a = x.toBigInt3 →
    ρ_res_low = (x.sqr).toUnreducedBigInt3

/- unreduced_sqr soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_unreduced_sqr
    {mem : F → F}
    (κ : ℕ)
    (a : BigInt3 mem) (ρ_res_low : UnreducedBigInt3 mem)
    (h_auto : auto_spec_unreduced_sqr mem κ a ρ_res_low) :
  spec_unreduced_sqr mem κ a ρ_res_low :=
begin
  rintros x xeq,
  rcases h_auto with ⟨twice_d0, rfl, _, rfl⟩,
  subst xeq,
  ext; simp [bigint3.toUnreducedBigInt3, bigint3.toBigInt3, bigint3.sqr, bigint3.mul, int.cast_mul, SECP_REM]; ring
end

/-
-- Function: verify_zero
-/

/- verify_zero autogenerated specification -/

-- Do not change this definition.
def auto_spec_verify_zero (mem : F → F) (κ : ℕ) (range_check_ptr : F) (val : UnreducedBigInt3 mem) (ρ_range_check_ptr : F) : Prop :=
  ∃ q : F,
  ∃ q_biased : F,
  q_biased = q + 2 ^ 127 ∧
  mem range_check_ptr = q_biased ∧
  is_range_checked (rc_bound F) (q_biased) ∧
  ∃ r1 : F, r1 = (val.d0 + q * SECP_REM) / (BASE : ℤ) ∧
  mem (range_check_ptr + 1) = r1 + 2 ^ 127 ∧
  is_range_checked (rc_bound F) (r1 + 2 ^ 127) ∧
  ∃ r2 : F, r2 = (val.d1 + r1) / (BASE : ℤ) ∧
  mem (range_check_ptr + 2) = r2 + 2 ^ 127 ∧
  is_range_checked (rc_bound F) (r2 + 2 ^ 127) ∧
  val.d2 = q * ((BASE : ℤ) / (4 : ℤ)) - r2 ∧
  ∃ range_check_ptr₁ : F, range_check_ptr₁ = range_check_ptr + 3 ∧
  15 ≤ κ ∧
  ρ_range_check_ptr = range_check_ptr₁

-- You may change anything in this definition except the name and arguments.
def spec_verify_zero (mem : F → F) (κ : ℕ) (range_check_ptr : F) (val : UnreducedBigInt3 mem) (ρ_range_check_ptr : F) : Prop :=
  ∀ ix : bigint3, val = ix.toUnreducedBigInt3 → ix.bounded (2^250) → ix.val % SECP_PRIME = 0

/- verify_zero soundness theorem -/

noncomputable def rc_to_int {x : F} (h : is_range_checked (rc_bound F) (x + 2^127)) :
  { i : ℤ // x = i ∧ abs i ≤ 2^127 } :=
begin
  rcases classical.some_spec h with ⟨n_ltn, neq⟩,
  use ↑(classical.some h) - 2^127,
  split, { simp [neq.symm] },
  rw abs_le, split, { rw le_sub, simp },
  have h1 : classical.some h ≤ 2^128 := le_trans (le_of_lt n_ltn) (rc_bound_hyp F),
  apply le_trans (sub_le_sub_right (int.coe_nat_le.mpr h1) _),
  simp, norm_num
end

lemma BASE_calc_aux: (↑BASE : ℤ) / 4 * (↑BASE * ↑BASE) = ↑BASE^3 / 4 :=
begin
  rw [pow_succ, mul_comm _ (↑BASE^2), int.mul_div_assoc, mul_comm, pow_two],
  unfold BASE, norm_cast, norm_num
end

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_verify_zero
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (val : UnreducedBigInt3 mem) (ρ_range_check_ptr : F)
    (h_auto : auto_spec_verify_zero mem κ range_check_ptr val ρ_range_check_ptr) :
  spec_verify_zero mem κ range_check_ptr val ρ_range_check_ptr :=
begin
  rintros ⟨id0, id1, id2⟩ deq abs_id_le,
  rcases unreduced_bigint3_eqs deq with ⟨d0eq, d1eq, d2eq⟩,
  rcases h_auto with
  ⟨q, q_biased, rfl, _, rcq,
   r1, r1_eq, _, rcr1,
   r2, r2_eq, _, rcr2,
   d2_eq, _, ret0_eq⟩,
  rcases rc_to_int rcq with ⟨iq, qeq, abs_iq_le⟩,
  rcases rc_to_int rcr1 with ⟨ir1, r1eq, abs_ir1_le⟩,
  rcases rc_to_int rcr2 with ⟨ir2, r2eq, abs_ir2_le⟩,
  apply int.mod_eq_zero_of_dvd,
  use iq,
  have: r1 * ↑BASE = (val.d0 + q * ↑SECP_REM),
  { rw [r1_eq], field_simp [BASE_ne_zero_aux'] },
  have: (↑(ir1 * ↑BASE) : F) = ↑(id0 + iq * ↑SECP_REM),
  { simp only [qeq.symm, r1eq.symm, d0eq, this, int.cast_mul, int.cast_coe_nat, int.cast_add] },
  have e1 : ir1 * ↑BASE = id0 + iq * ↑SECP_REM,
  { apply PRIME.int_coe_inj this,
    have: abs (id0 + iq * ↑SECP_REM - (ir1 * ↑BASE)) ≤
      2^250 + 2^127 * ↑SECP_REM + 2^127 * ↑BASE,
    { rw sub_eq_add_neg,
      apply le_trans (abs_add _ _),
      apply add_le_add,
      apply le_trans (abs_add _ _),
      rw [abs_mul, abs_of_nonneg SECP_REM_nonneg],
      apply add_le_add abs_id_le.1,
      exact mul_le_mul_of_nonneg_right abs_iq_le SECP_REM_nonneg,
      rw [abs_neg, abs_mul, abs_of_nonneg BASE_nonneg],
      exact mul_le_mul_of_nonneg_right abs_ir1_le BASE_nonneg },
    apply lt_of_le_of_lt this,
    simp only [SECP_REM, BASE, PRIME], simp_int_casts, norm_num1 },
  have: (↑(ir2 * ↑BASE) : F) = ↑(id1 + ir1),
  { simp [r1eq.symm, r2eq.symm, r2_eq, d1eq], field_simp [BASE_ne_zero_aux'] },
  have e2 : ir2 * ↑BASE = id1 + ir1,
  { apply PRIME.int_coe_inj this,
    have: abs (id1 + ir1 - ir2 * ↑BASE) ≤ 2^250 + 2^127 + 2^127 * ↑BASE,
    { apply le_trans (abs_add _ _),
      apply add_le_add,
      apply le_trans (abs_add _ _),
      exact add_le_add abs_id_le.2.1 abs_ir1_le,
      rw [abs_neg, abs_mul, abs_of_nonneg BASE_nonneg],
      exact mul_le_mul_of_nonneg_right abs_ir2_le BASE_nonneg },
    apply lt_of_le_of_lt this,
    simp only [BASE, PRIME], simp_int_casts, norm_num1 },
  have: (4 : ℤ) ∣ ↑BASE, by { simp only [BASE], simp_int_casts, norm_num1 },
  have: (↑(iq * (↑BASE / 4)) : F) = ↑(id2 + ir2),
  { simp [qeq.symm, r2eq.symm, d2eq.symm, d2_eq, sub_mul, mul_assoc],
    rw [int.cast_div], simp, norm_num1, simp [PRIME.four_ne_zero F] },
  have e3 : iq * (↑BASE / 4) = id2 + ir2,
  { apply PRIME.int_coe_inj this,
    have: abs (id2 + ir2 - iq * (↑BASE / 4)) ≤ 2^250 + 2^127 + 2^127 * (↑BASE / 4),
    { apply le_trans (abs_add _ _),
      apply add_le_add,
      { apply le_trans (abs_add _ _),
        apply add_le_add abs_id_le.2.2 abs_ir2_le },
      rw [abs_neg, abs_mul, abs_of_nonneg BASE_div_4_nonneg],
      exact mul_le_mul_of_nonneg_right abs_iq_le BASE_div_4_nonneg },
    apply lt_of_le_of_lt this,
    simp only [BASE, PRIME], simp_int_casts, norm_num1 },
  have e4 := congr_arg (λ x, x * (↑BASE * ↑BASE : int)) e3,
  dsimp at e4,
  have: (↑BASE : ℤ) / 4 * (↑BASE * ↑BASE) = ↑BASE^3 / 4,
  { rw [pow_succ, mul_comm _ (↑BASE^2), int.mul_div_assoc, mul_comm, pow_two],
    unfold BASE, norm_cast, norm_num},
  rw [add_mul, ←mul_assoc ir2, e2, add_mul, e1, mul_assoc iq, this, ←sub_eq_zero] at e4,
  -- show bigint_val id0 id1 id2 = ((↑BASE : ℤ)^3 / 4 - ↑SECP_REM) * iq,
  rw [SECP_PRIME_eq, bigint3.val, ←sub_eq_zero, ←neg_eq_zero, ←e4, pow_two], ring
end

/-
-- Function: is_zero
-/

/- is_zero autogenerated specification -/

-- Do not change this definition.
def auto_spec_is_zero (mem : F → F) (κ : ℕ) (range_check_ptr : F) (x : SumBigInt3 mem) (ρ_range_check_ptr ρ_res : F) : Prop :=
  ∃ ιχ__temp40 : F,
  ((ιχ__temp40 ≠ 0 ∧
    ∃ (κ₁ : ℕ) (range_check_ptr₁ : F), spec_verify_zero mem κ₁ range_check_ptr {
      d0 := x.d0,
      d1 := x.d1,
      d2 := x.d2
    } range_check_ptr₁ ∧
    κ₁ + 9 ≤ κ ∧
    ρ_range_check_ptr = range_check_ptr₁ ∧
    ρ_res = 1) ∨
   (ιχ__temp40 = 0 ∧
    ∃ (κ₁ : ℕ) (range_check_ptr₁ : F) (x_inv : BigInt3 mem), spec_nondet_bigint3 mem κ₁ range_check_ptr range_check_ptr₁ x_inv ∧
    ∃ (κ₂ : ℕ) (x_x_inv : UnreducedBigInt3 mem), spec_unreduced_mul mem κ₂ {
      d0 := x.d0,
      d1 := x.d1,
      d2 := x.d2
    } x_inv x_x_inv ∧
    ∃ (κ₃ : ℕ) (range_check_ptr₂ : F), spec_verify_zero mem κ₃ range_check_ptr₁ {
      d0 := x_x_inv.d0 - 1,
      d1 := x_x_inv.d1,
      d2 := x_x_inv.d2
    } range_check_ptr₂ ∧
    κ₁ + κ₂ + κ₃ + 19 ≤ κ ∧
    ρ_range_check_ptr = range_check_ptr₂ ∧
    ρ_res = 0))

-- You may change anything in this definition except the name and arguments.
def spec_is_zero (mem : F → F) (κ : ℕ) (range_check_ptr : F) (x : SumBigInt3 mem) (ρ_range_check_ptr ρ_res : F) : Prop :=
  ∀ ix : bigint3, x = ix.toSumBigInt3 → ix.bounded (2^107) →
    ((ix.val % SECP_PRIME = 0 ∧ ρ_res = 1) ∨
      (ix.val % SECP_PRIME ≠ 0 ∧ ρ_res = 0))

/- is_zero soundness theorem -/

def bigint3.one : bigint3 := ⟨1, 0, 0⟩

theorem bigint3.one_val : bigint3.one.val = 1 :=
by simp [bigint3.one, bigint3.val]

theorem SECP_PRIME_gt_one : 1 < (SECP_PRIME : ℤ) :=
by { rw [SECP_PRIME_eq, BASE, SECP_REM], simp_int_casts, norm_num1 }

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_is_zero
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (x : SumBigInt3 mem) (ρ_range_check_ptr ρ_res : F)
    (h_auto : auto_spec_is_zero mem κ range_check_ptr x ρ_range_check_ptr ρ_res) :
  spec_is_zero mem κ range_check_ptr x ρ_range_check_ptr ρ_res :=
begin
  intros ix xeq ixbdd,
  rcases h_auto with ⟨ιχ__temp40, ⟨ιχ__temp40_nez, case_neg⟩ | ⟨ιχ__temp32_ez, case_pos⟩⟩,
  { rcases case_neg with ⟨_, _, h_verify_zero, _, _, ρ_res_eq⟩,
    have ixbdd' : ix.bounded (2^250),
    { apply bigint3.bounded_of_bounded_of_le ixbdd,
      norm_num },
    have := h_verify_zero ix (by rw xeq; refl) ixbdd',
    left, use [this, ρ_res_eq] },
  rcases case_pos with ⟨_, _, x_inv, h_x_inv, _, x_x_inv, h_x_x_inv, _, _, h_verify_zero, _, _, ρ_res_eq⟩,
  rcases nondet_bigint3_corr h_x_inv with ⟨ix_inv, x_inv_eq, ix_inv_bdd⟩,
  have := h_x_x_inv ix ix_inv (bigint3.eq_toBigInt3_iff_eq_toSumBigInt3.mp xeq) x_inv_eq,
  have : ((ix.mul ix_inv).sub bigint3.one).toUnreducedBigInt3 =
    {d0 := x_x_inv.d0 - 1, d1 := x_x_inv.d1, d2 := x_x_inv.d2},
  { rw this, simp [bigint3.toUnreducedBigInt3, bigint3.sub, bigint3.one], },
  have := h_verify_zero _ this.symm,
  have := this _,
  rw [bigint3.sub_val, bigint3.one_val, ←int.modeq_iff_sub_mod_eq_zero] at this,
  have h := (bigint3.mul_val _ _).symm.trans this,
  right,
  refine ⟨_, ρ_res_eq⟩,
  { intro ixval_mod_eq_zero,
    have : ix.val * ix_inv.val ≡ 0 [ZMOD ↑SECP_PRIME],
    { apply int.modeq.trans,
      apply int.modeq.mul (int.modeq_zero_iff.mpr ixval_mod_eq_zero) int.modeq.rfl,
      rw zero_mul },
    rw [int.modeq, int.zero_mod] at this,
    rw [int.modeq, this, int.mod_eq_of_lt] at h,
    apply zero_ne_one h,
    norm_num,
    exact SECP_PRIME_gt_one },
  have : ((2^107 : ℤ)^2 * (8 * SECP_REM + 1)) + 1 ≤ 2^250,
  { simp, norm_num },
  apply bigint3.bounded_of_bounded_of_le _ this,
  apply bigint3.bounded_sub, swap,
  { simp [bigint3.bounded, bigint3.one] },
  apply bigint3.bounded_mul ixbdd,
  apply bigint3.bounded_of_bounded_of_le ix_inv_bdd,
  norm_num
end

/-
-- Function: reduce
-/

/- reduce autogenerated specification -/

-- Do not change this definition.
def auto_spec_reduce (mem : F → F) (κ : ℕ) (range_check_ptr : F) (x : UnreducedBigInt3 mem) (ρ_range_check_ptr : F) (ρ_reduced_x : BigInt3 mem) : Prop :=
  ∃ (κ₁ : ℕ) (range_check_ptr₁ : F) (reduced_x : BigInt3 mem), spec_nondet_bigint3 mem κ₁ range_check_ptr range_check_ptr₁ reduced_x ∧
  ∃ (κ₂ : ℕ) (range_check_ptr₂ : F), spec_verify_zero mem κ₂ range_check_ptr₁ {
    d0 := x.d0 - reduced_x.d0,
    d1 := x.d1 - reduced_x.d1,
    d2 := x.d2 - reduced_x.d2
  } range_check_ptr₂ ∧
  κ₁ + κ₂ + 11 ≤ κ ∧
  ρ_range_check_ptr = range_check_ptr₂ ∧
  ρ_reduced_x = reduced_x

-- You may change anything in this definition except the name and arguments.
def spec_reduce (mem : F → F) (κ : ℕ) (range_check_ptr : F) (x : UnreducedBigInt3 mem) (ρ_range_check_ptr : F) (ρ_reduced_x : BigInt3 mem) : Prop :=
  ∀ ix : bigint3,
    -- We could get by with 2^250 - 3 * (BASE - 1).
    ix.bounded (2^249) →
    x = ix.toUnreducedBigInt3 →
    ∃ ix' : bigint3,
      ix'.bounded (3 * (BASE - 1)) ∧
      ix'.val ≡ ix.val [ZMOD SECP_PRIME] ∧
      ρ_reduced_x = ix'.toBigInt3


/- reduce soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_reduce
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (x : UnreducedBigInt3 mem) (ρ_range_check_ptr : F) (ρ_reduced_x : BigInt3 mem)
    (h_auto : auto_spec_reduce mem κ range_check_ptr x ρ_range_check_ptr ρ_reduced_x) :
  spec_reduce mem κ range_check_ptr x ρ_range_check_ptr ρ_reduced_x :=
begin
  intros ix ixbdd xeq,
  rcases h_auto with ⟨_, _, reduced_x, h_reduced_x, _, _, h_verify_zero, _, _, ρ_reduced_x_eq⟩,
  rcases nondet_bigint3_corr h_reduced_x with ⟨ix', reduced_x_eq, ix'bdd⟩,
  have : (ix.sub ix').val % SECP_PRIME = 0,
  { apply h_verify_zero,
    { rw [bigint3.toUnreducedBigInt3_sub, ←xeq, UnreducedBigInt3.sub, reduced_x_eq,
          bigint3.toUnreducedBigInt3, bigint3.toBigInt3] },
      have : (2^249 : ℤ) + 3 * (↑BASE - 1) ≤ 2^250,
      { simp, norm_num },
      apply bigint3.bounded_of_bounded_of_le _ this,
      exact bigint3.bounded_sub ixbdd ix'bdd },
  use [ix', ix'bdd],
  rw [bigint3.sub_val, ←int.mod_eq_mod_iff_mod_sub_eq_zero] at this,
  use this.symm,
  exact ρ_reduced_x_eq.trans reduced_x_eq
end

/-
-- Function: validate_reduced_field_element
-/

/- validate_reduced_field_element autogenerated specification -/

-- Do not change this definition.
def auto_spec_validate_reduced_field_element (mem : F → F) (κ : ℕ) (range_check_ptr : F) (val : BigInt3 mem) (ρ_range_check_ptr : F) : Prop :=
  ∃ (κ₁ : ℕ) (range_check_ptr₁ : F), spec_assert_nn_le mem κ₁ range_check_ptr val.d2 P2 range_check_ptr₁ ∧
  ∃ (κ₂ : ℕ) (range_check_ptr₂ : F), spec_assert_nn_le mem κ₂ range_check_ptr₁ val.d1 (BASE - 1) range_check_ptr₂ ∧
  ∃ (κ₃ : ℕ) (range_check_ptr₃ : F), spec_assert_nn_le mem κ₃ range_check_ptr₂ val.d0 (BASE - 1) range_check_ptr₃ ∧
  ((val.d2 = P2 ∧
    ((val.d1 = P1 ∧
      ∃ (κ₄ : ℕ) (range_check_ptr₄ : F), spec_assert_nn_le mem κ₄ range_check_ptr₃ val.d0 (P0 - 1) range_check_ptr₄ ∧
      κ₁ + κ₂ + κ₃ + κ₄ + 19 ≤ κ ∧
      ρ_range_check_ptr = range_check_ptr₄) ∨
     (val.d1 ≠ P1 ∧
      ∃ (κ₄ : ℕ) (range_check_ptr₄ : F), spec_assert_nn_le mem κ₄ range_check_ptr₃ val.d1 (P1 - 1) range_check_ptr₄ ∧
      κ₁ + κ₂ + κ₃ + κ₄ + 19 ≤ κ ∧
      ρ_range_check_ptr = range_check_ptr₄))) ∨
   (val.d2 ≠ P2 ∧
    κ₁ + κ₂ + κ₃ + 14 ≤ κ ∧
    ρ_range_check_ptr = range_check_ptr₃))

-- You may change anything in this definition except the name and arguments.
def spec_validate_reduced_field_element (mem : F → F) (κ : ℕ) (range_check_ptr : F) (val : BigInt3 mem) (ρ_range_check_ptr : F) : Prop :=
  ∃ n0 n1 n2 : ℕ,
    n0 ≤ BASE - 1 ∧
    n1 ≤ BASE - 1 ∧
    n2 ≤ P2 ∧
    n2 * BASE^2 + n1 * BASE + n0 < SECP_PRIME ∧
    val = ⟨n0, n1, n2⟩

/- validate_reduced_field_element soundness theorem -/

theorem P0_pos : 0 < P0 :=
by { rw P0, norm_num }

theorem P1_pos : 0 < P1 :=
by { rw P1, norm_num }

theorem P2_pos : 0 < P2 :=
by { rw P2, norm_num }

theorem BASE_pos : 0 < BASE :=
by { rw BASE, norm_num }

theorem coe_P0m1_eq :
  ((↑P0 : F) - 1 = ↑(P0 - 1)) :=
begin
  rw [nat.cast_sub, nat.cast_one],
  exact P0_pos,
end

theorem coe_P1m1_eq :
  ((↑P1 : F) - 1 = ↑(P1 - 1)) :=
begin
  rw [nat.cast_sub, nat.cast_one],
  exact P1_pos,
end

theorem coe_BASEm1_eq :
  ((↑BASE : F) - 1 = ↑(BASE - 1)) :=
begin
  rw [nat.cast_sub, nat.cast_one],
  exact BASE_pos,
end

theorem aux0 {m p : ℕ} (hm : m < rc_bound F) (hp : p < PRIME) (h : (m : F) = p) : m = p :=
begin
  apply @PRIME.nat_coe_field_inj F _ _ _ _ _ hp h,
  apply lt_of_lt_of_le hm,
  apply le_trans (rc_bound_hyp F),
  rw PRIME, norm_num
end

theorem aux1 {m n p : ℕ} (hm : m < rc_bound F) (hn : n < rc_bound F)
(hp : p < PRIME) (h : (↑(m + n) : F) = p) : m ≤ p :=
begin
  have : m + n = p,
  { apply @PRIME.nat_coe_field_inj F _ _ _ _ _ hp h,
    apply lt_of_lt_of_le (add_lt_add hm hn),
    apply le_trans (add_le_add (rc_bound_hyp F) (rc_bound_hyp F)),
    rw PRIME, norm_num },
  rw ←this,
  apply nat.le_add_right
end

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_validate_reduced_field_element
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (val : BigInt3 mem) (ρ_range_check_ptr : F)
    (h_auto : auto_spec_validate_reduced_field_element mem κ range_check_ptr val ρ_range_check_ptr) :
  spec_validate_reduced_field_element mem κ range_check_ptr val ρ_range_check_ptr :=
begin
  rcases h_auto with ⟨
    _, _, ⟨m2, n2, m2lt, n2lt, vald2eq, P2eq⟩,
    _, _, ⟨m1, n1, m1lt, n1lt, vald1eq, m1n1eq⟩,
    _, _, ⟨m0, n0, m0lt, n0lt, vald0eq, m0n0eq⟩,
    hcases⟩,
  have m2leP2 : m2 ≤ P2,
  { apply aux1 m2lt n2lt _ P2eq.symm,
    rw PRIME, norm_num },
  have m1leBASEm1 : m1 ≤ BASE - 1,
  { rw coe_BASEm1_eq at m1n1eq,
    apply aux1 m1lt n1lt _ m1n1eq.symm,
    rw [PRIME, BASE], norm_num },
  have m0leBASEm1 : m0 ≤ BASE - 1,
  { rw coe_BASEm1_eq at m0n0eq,
    apply aux1 m0lt n0lt _ m0n0eq.symm,
    rw [PRIME, BASE], norm_num },
  rcases hcases with ⟨d2eq, hcases⟩ | ⟨d2ne, _, _⟩,
  { have m2eqP2: m2 = P2,
    { apply aux0 m2lt _ (vald2eq.symm.trans d2eq),
      rw [PRIME, P2], norm_num },
    rcases hcases with
      ⟨d1eq, _, _, ⟨m0', n0', m0'lt, n0'lt, vald0eq', P0m1eq⟩, _, _⟩ |
      ⟨d1ne, _, _, ⟨m1', n1', m1'lt, n1'lt, vald1eq', P1m1eq⟩, _, _⟩,
    { have m1eqP1: m1 = P1,
      { apply aux0 m1lt _ (vald1eq.symm.trans d1eq),
        rw [PRIME, P1], norm_num },
      have m0'leP0m1 : m0' ≤ P0 - 1,
      { rw coe_P0m1_eq at P0m1eq,
        apply aux1 m0'lt n0'lt _ P0m1eq.symm,
        rw [PRIME, P0], norm_num },
      use [m0', m1, m2], split,
      { apply le_trans m0'leP0m1,
        rw [BASE, P0], norm_num },
      split,
      {  exact m1leBASEm1 },
      split,
      { rw m2eqP2 },
      split,
      { apply lt_of_le_of_lt,
        apply add_le_add_left m0'leP0m1,
        rw [m2eqP2, P2, m1eqP1, P1, P0, SECP_PRIME, BASE, SECP_REM],
        norm_num },
      rw BigInt3.ext_iff,
      use [vald0eq', vald1eq, vald2eq] },
    have m1'leP1m1 : m1' ≤ P1 - 1,
    { rw coe_P1m1_eq at P1m1eq,
      apply aux1 m1'lt n1'lt _ P1m1eq.symm,
      rw [PRIME, P1], norm_num },
    use [m0, m1', m2], split,
    use [m0leBASEm1],
    split,
    { apply le_trans m1'leP1m1,
      rw [BASE, P1], norm_num },
    split,
    { exact m2leP2 },
    split,
    { apply lt_of_le_of_lt,
      apply add_le_add,
      apply add_le_add_left,
      apply nat.mul_le_mul_right _ m1'leP1m1,
      exact m0leBASEm1,
      rw [m2eqP2, SECP_PRIME, SECP_REM, BASE, P2, P1], norm_num },
    rw BigInt3.ext_iff,
    use [vald0eq, vald1eq', vald2eq] },
  have : m2 ≠ P2,
  { intro h,
    apply d2ne,
    rw [vald2eq, h] },
  have m2leP2m1 : m2 ≤ P2 - 1,
  { apply nat.le_pred_of_lt,
    apply lt_of_le_of_ne m2leP2 this },
  use [m0, m1, m2, m0leBASEm1, m1leBASEm1, m2leP2],
  split,
  { apply lt_of_le_of_lt,
    apply add_le_add,
    apply add_le_add,
    apply nat.mul_le_mul_right _ m2leP2m1,
    apply nat.mul_le_mul_right _ m1leBASEm1,
    apply m0leBASEm1,
    rw [SECP_PRIME, SECP_REM, BASE, P2], norm_num },
  rw BigInt3.ext_iff,
  use [vald0eq, vald1eq, vald2eq]
end

/-
def spec_validate_reduced_field_element' (mem : F → F) (κ : ℕ) (range_check_ptr : F) (val : BigInt3 F) (ρ_range_check_ptr : F) : Prop :=
  ∃ ival : bigint3,
    ival.bounded ↑(BASE - 1) ∧
    ival.val < SECP_PRIME ∧
    val = ival.toBigInt3

theorem sound_validate_reduced_field_element'
    {mem : F → F}
    (κ : ℕ)
    (range_check_ptr : F) (val : BigInt3 F) (ρ_range_check_ptr : F)
    (h_auto : auto_spec_validate_reduced_field_element mem κ range_check_ptr val ρ_range_check_ptr) :
  spec_validate_reduced_field_element mem κ range_check_ptr val ρ_range_check_ptr :=
begin
  rcases h_auto with ⟨
    _, _, ⟨m2, n2, m2lt, n2lt, vald2eq, P2eq⟩,
    _, _, ⟨m1, n1, m1lt, n1lt, vald1eq, m1n1eq⟩,
    _, _, ⟨m0, n0, m0lt, n0lt, vald0eq, m0n0eq⟩,
    hcases⟩,
  have m2leP2 : m2 ≤ P2,
  { apply aux1 m2lt n2lt _ P2eq.symm,
    rw PRIME, norm_num },
  have m1leBASEm1 : m1 ≤ BASE - 1,
  { rw coe_BASEm1_eq at m1n1eq,
    apply aux1 m1lt n1lt _ m1n1eq.symm,
    rw [PRIME, BASE], norm_num },
  have m0leBASEm1 : m0 ≤ BASE - 1,
  { rw coe_BASEm1_eq at m0n0eq,
    apply aux1 m0lt n0lt _ m0n0eq.symm,
    rw [PRIME, BASE], norm_num },
  rcases hcases with ⟨d2eq, hcases⟩ | ⟨d2ne, _, _⟩,
  { have m2eqP2: m2 = P2,
    { apply aux0 m2lt _ (vald2eq.symm.trans d2eq),
      rw [PRIME, P2], norm_num },
    rcases hcases with
      ⟨d1eq, _, _, ⟨m0', n0', m0'lt, n0'lt, vald0eq', P0m1eq⟩, _, _⟩ |
      ⟨d1ne, _, _, ⟨m1', n1', m1'lt, n1'lt, vald1eq', P1m1eq⟩, _, _⟩,
    { have m1eqP1: m1 = P1,
      { apply aux0 m1lt _ (vald1eq.symm.trans d1eq),
        rw [PRIME, P1], norm_num },
      have m0'leP0m1 : m0' ≤ P0 - 1,
      { rw coe_P0m1_eq at P0m1eq,
        apply aux1 m0'lt n0'lt _ P0m1eq.symm,
        rw [PRIME, P0], norm_num },
      use ⟨m0', m1, m2⟩, split,
      { simp only [bigint3.bounded, int.coe_nat_le, int.coe_nat_abs],
        split,
        { apply le_trans m0'leP0m1,
          rw [BASE, P0], norm_num },
        split,
        {  exact m1leBASEm1 },
        rw [m2eqP2, BASE, P2], norm_num },
      split,
      { have : (m0' : ℤ) ≤ ↑(P0 - 1),
        { rw [int.coe_nat_le], exact m0'leP0m1 },
        rw [bigint3.val, m2eqP2, m1eqP1], dsimp,
        refine lt_of_le_of_lt (add_le_add_left this _) _,
        rw [P2, P1, P0, SECP_PRIME_eq, BASE, SECP_REM],
        simp_int_casts, norm_num },
      rw [bigint3.toBigInt3, BigInt3.ext_iff],
      dsimp,
      rw [vald0eq', d2eq, d1eq, m1eqP1, m2eqP2],
      exact ⟨rfl, rfl, rfl⟩ },
    have m1'leP1m1 : m1' ≤ P1 - 1,
    { rw coe_P1m1_eq at P1m1eq,
      apply aux1 m1'lt n1'lt _ P1m1eq.symm,
      rw [PRIME, P1], norm_num },
    use ⟨m0, m1', m2⟩, split,
    { simp only [bigint3.bounded, int.coe_nat_le, int.coe_nat_abs],
      use [m0leBASEm1],
      split,
      { apply le_trans m1'leP1m1,
        rw [BASE, P1], norm_num },
      rw [m2eqP2, BASE, P2], norm_num },
    split,
    { have h1: (m1' : ℤ) * BASE ≤ ↑(P1 - 1) * BASE,
      { apply mul_le_mul_of_nonneg_right _ (int.coe_nat_nonneg _),
        rw [int.coe_nat_le],
        exact m1'leP1m1 },
      have h2 : (m0 : ℤ) ≤ ↑(BASE - 1),
      { rw [int.coe_nat_le],
        exact m0leBASEm1 },
      rw [bigint3.val, m2eqP2], dsimp,
      apply lt_of_le_of_lt,
      apply add_le_add (add_le_add_left h1 _) h2,
      rw [P2, P1, SECP_PRIME_eq, BASE, SECP_REM],
      simp_int_casts, norm_num },
    rw [bigint3.toBigInt3, BigInt3.ext_iff],
    dsimp,
    rw [vald0eq, vald1eq', d2eq, m2eqP2],
    exact ⟨rfl, rfl, rfl⟩ },
  have : m2 ≠ P2,
  { intro h,
    apply d2ne,
    rw [vald2eq, h] },
  have m2leP2m1 : m2 ≤ P2 - 1,
  { apply nat.le_pred_of_lt,
    apply lt_of_le_of_ne m2leP2 this },
  use ⟨m0, m1, m2⟩,
  split,
  { simp only [bigint3.bounded, int.coe_nat_le, int.coe_nat_abs],
    use [m0leBASEm1, m1leBASEm1],
    apply le_trans m2leP2m1,
    rw [BASE, P2], norm_num },
  split,
  { rw bigint3.val, dsimp,
    have h0: (m2 : ℤ) * BASE^2 ≤ ↑(P2 - 1) * BASE^2,
    { apply mul_le_mul_of_nonneg_right _ (int.coe_nat_nonneg _),
      rw [int.coe_nat_le],
      exact m2leP2m1 },
    have h1: (m1 : ℤ) * BASE ≤ ↑(BASE - 1) * BASE,
    { apply mul_le_mul_of_nonneg_right _ (int.coe_nat_nonneg _),
      rw [int.coe_nat_le],
      exact m1leBASEm1 },
    have h2 : (m0 : ℤ) ≤ ↑(BASE - 1),
    { rw [int.coe_nat_le],
      exact m0leBASEm1 },
    apply lt_of_le_of_lt,
    apply add_le_add  (add_le_add h0 h1) h2,
    rw [int.coe_nat_sub, int.coe_nat_sub],
    rw [P2, SECP_PRIME_eq, BASE, SECP_REM],
    simp_int_casts, repeat { norm_num [BASE] } },
  rw [bigint3.toBigInt3, BigInt3.ext_iff],
  dsimp,
  use [vald0eq, vald1eq, vald2eq]
end
-/

end starkware.cairo.common.cairo_secp.field