signature_recover_public_key_get_point_from_x_soundness.lean

/-
File: signature_recover_public_key_get_point_from_x_soundness.lean

Autogenerated file.
-/
import starkware.cairo.lean.semantics.soundness.hoare
import .signature_recover_public_key_code
import ..signature_recover_public_key_spec
import .signature_recover_public_key_unreduced_sqr_soundness
import .signature_recover_public_key_reduce_soundness
import .signature_recover_public_key_validate_reduced_field_element_soundness
import .signature_recover_public_key_unreduced_mul_soundness
open tactic

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

variables {F : Type} [field F] [decidable_eq F] [prelude_hyps F]
variable  mem : F → F
variable  σ : register_state F

/- starkware.cairo.common.cairo_secp.signature.get_point_from_x autogenerated soundness theorem -/

theorem auto_sound_get_point_from_x
    -- arguments
    (range_check_ptr : F) (x : BigInt3 mem) (v : F)
    -- code is in memory at σ.pc
    (h_mem : mem_at mem code_get_point_from_x σ.pc)
    -- all dependencies are in memory
    (h_mem_0 : mem_at mem code_assert_nn (σ.pc  - 751))
    (h_mem_1 : mem_at mem code_assert_le (σ.pc  - 747))
    (h_mem_2 : mem_at mem code_assert_nn_le (σ.pc  - 742))
    (h_mem_4 : mem_at mem code_nondet_bigint3 (σ.pc  - 719))
    (h_mem_5 : mem_at mem code_unreduced_mul (σ.pc  - 707))
    (h_mem_6 : mem_at mem code_unreduced_sqr (σ.pc  - 687))
    (h_mem_7 : mem_at mem code_verify_zero (σ.pc  - 671))
    (h_mem_9 : mem_at mem code_reduce (σ.pc  - 612))
    (h_mem_10 : mem_at mem code_validate_reduced_field_element (σ.pc  - 599))
    -- input arguments on the stack
    (hin_range_check_ptr : range_check_ptr = mem (σ.fp - 7))
    (hin_x : x = cast_BigInt3 mem (σ.fp - 6))
    (hin_v : v = mem (σ.fp - 3))
    -- conclusion
  : ensures_ret mem σ (λ κ τ,
      ∃ μ ≤ κ, rc_ensures mem (rc_bound F) μ (mem (σ.fp - 7)) (mem $ τ.ap - 7)
        (spec_get_point_from_x mem κ range_check_ptr x v (mem (τ.ap - 7)) (cast_EcPoint  mem (τ.ap - 6)))) :=
begin
  apply ensures_of_ensuresb, intro νbound,
  have h_mem_rec := h_mem,
  unpack_memory code_get_point_from_x at h_mem with ⟨hpc0, hpc1, hpc2, hpc3, hpc4, hpc5, hpc6, hpc7, hpc8, hpc9, hpc10, hpc11, hpc12, hpc13, hpc14, hpc15, hpc16, hpc17, hpc18, hpc19, hpc20, hpc21, hpc22, hpc23, hpc24, hpc25, hpc26, hpc27, hpc28, hpc29, hpc30, hpc31, hpc32, hpc33, hpc34, hpc35, hpc36, hpc37, hpc38, hpc39, hpc40, hpc41, hpc42, hpc43, hpc44, hpc45, hpc46, hpc47, hpc48, hpc49, hpc50, hpc51, hpc52, hpc53, hpc54, hpc55, hpc56, hpc57, hpc58, hpc59, hpc60, hpc61, hpc62, hpc63, hpc64, hpc65⟩,
  -- ap += 6
  step_advance_ap hpc0 hpc1,
  -- function call
  step_assert_eq hpc2 with arg0,
  step_assert_eq hpc3 with arg1,
  step_sub hpc4 (auto_sound_assert_nn mem _ range_check_ptr v _ _ _),
  { rw hpc5, norm_num2, exact h_mem_0 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  intros κ_call6 ap6 h_call6,
  rcases h_call6 with ⟨h_call6_ap_offset, h_call6⟩,
  rcases h_call6 with ⟨rc_m6, rc_mle6, hl_range_check_ptr₁, h_call6⟩,
  mkdef htv_range_check_ptr₁ : range_check_ptr₁ = (mem (ap6 - 1)),
  simp only [←htv_range_check_ptr₁] at h_call6,
  try { simp only [arg0 ,arg1] at hl_range_check_ptr₁ },
  try { rw [←htv_range_check_ptr₁] at hl_range_check_ptr₁ }, try { rw [←hin_range_check_ptr] at hl_range_check_ptr₁ },
  try { simp only [arg0 ,arg1] at h_call6 },
  rw [hin_range_check_ptr] at h_call6,
  clear arg0 arg1,
  -- function call
  step_assert_eq hpc6 with arg0,
  step_assert_eq hpc7 with arg1,
  step_assert_eq hpc8 with arg2,
  step_sub hpc9 (auto_sound_unreduced_sqr mem _ x _ _),
  { rw hpc10, norm_num2, exact h_mem_6 },
  { try { ext } ; {
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁] },
      try { dsimp [cast_BigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2] },
      try { simp only [h_call6_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call11 ap11 h_call11,
  rcases h_call11 with ⟨h_call11_ap_offset, h_call11⟩,
  mkdef htv_x_square : x_square = (cast_UnreducedBigInt3 mem (ap11 - 3)),
  simp only [←htv_x_square] at h_call11,
  clear arg0 arg1 arg2,
  -- function call
  step_assert_eq hpc11 with arg0,
  step_assert_eq hpc12 with arg1,
  step_assert_eq hpc13 with arg2,
  step_assert_eq hpc14 with arg3,
  step_sub hpc15 (auto_sound_reduce mem _ range_check_ptr₁ x_square _ _ _ _ _),
  { rw hpc16, norm_num2, exact h_mem_9 },
  { rw hpc16, norm_num2, exact h_mem_4 },
  { rw hpc16, norm_num2, exact h_mem_7 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square] },
    try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3] },
    try { simp only [h_call6_ap_offset, h_call11_ap_offset] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  { try { ext } ; {
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square] },
      try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call17 ap17 h_call17,
  rcases h_call17 with ⟨h_call17_ap_offset, h_call17⟩,
  rcases h_call17 with ⟨rc_m17, rc_mle17, hl_range_check_ptr₂, h_call17⟩,
  mkdef htv_range_check_ptr₂ : range_check_ptr₂ = (mem (ap17 - 4)),
  simp only [←htv_range_check_ptr₂] at h_call17,
  mkdef htv_x_square_reduced : x_square_reduced = (cast_BigInt3 mem (ap17 - 3)),
  simp only [←htv_x_square_reduced] at h_call17,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3] at hl_range_check_ptr₂ },
  try { rw [h_call11_ap_offset] at hl_range_check_ptr₂ }, try { arith_simps at hl_range_check_ptr₂ },
  try { rw [←htv_range_check_ptr₂] at hl_range_check_ptr₂ }, try { rw [←htv_range_check_ptr₁] at hl_range_check_ptr₂ },
  try { simp only [arg0 ,arg1 ,arg2 ,arg3] at h_call17 },
  try { rw [h_call11_ap_offset] at h_call17 }, try { arith_simps at h_call17 },
  rw [←htv_range_check_ptr₁, hl_range_check_ptr₁, hin_range_check_ptr] at h_call17,
  clear arg0 arg1 arg2 arg3,
  -- function call
  step_assert_eq hpc17 with arg0,
  step_assert_eq hpc18 with arg1,
  step_assert_eq hpc19 with arg2,
  step_assert_eq hpc20 with arg3,
  step_assert_eq hpc21 with arg4,
  step_assert_eq hpc22 with arg5,
  step_sub hpc23 (auto_sound_unreduced_mul mem _ x x_square_reduced _ _ _),
  { rw hpc24, norm_num2, exact h_mem_5 },
  { try { ext } ; {
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced] },
      try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  { try { ext } ; {
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced] },
      try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call25 ap25 h_call25,
  rcases h_call25 with ⟨h_call25_ap_offset, h_call25⟩,
  mkdef htv_x_cube : x_cube = (cast_UnreducedBigInt3 mem (ap25 - 3)),
  simp only [←htv_x_cube] at h_call25,
  clear arg0 arg1 arg2 arg3 arg4 arg5,
  -- local var
  step_assert_eq hpc25 with temp0,
  step_assert_eq hpc26 with temp1,
  step_assert_eq hpc27 with temp2,
  have lc_x_cube: x_cube = (cast_UnreducedBigInt3 mem (σ.fp)), {
    try { ext } ; {
      try { simp only [htv_x_cube] },
      try { dsimp [cast_UnreducedBigInt3] },
      try { arith_simps }, try { simp only [temp0, temp1, temp2] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  clear temp0 temp1 temp2,
  -- function call
  step_assert_eq hpc28 with arg0,
  step_sub hpc29 (auto_sound_nondet_bigint3 mem _ range_check_ptr₂ _ _),
  { rw hpc30, norm_num2, exact h_mem_4 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube] },
    try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
    try { arith_simps }, try { simp only [arg0] },
    try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  intros κ_call31 ap31 h_call31,
  rcases h_call31 with ⟨h_call31_ap_offset, h_call31⟩,
  rcases h_call31 with ⟨rc_m31, rc_mle31, hl_range_check_ptr₃, h_call31⟩,
  mkdef htv_range_check_ptr₃ : range_check_ptr₃ = (mem (ap31 - 4)),
  simp only [←htv_range_check_ptr₃] at h_call31,
  mkdef htv_y : y = (cast_BigInt3 mem (ap31 - 3)),
  simp only [←htv_y] at h_call31,
  try { simp only [arg0] at hl_range_check_ptr₃ },
  try { rw [h_call25_ap_offset] at hl_range_check_ptr₃ }, try { arith_simps at hl_range_check_ptr₃ },
  try { rw [←htv_range_check_ptr₃] at hl_range_check_ptr₃ }, try { rw [←htv_range_check_ptr₂] at hl_range_check_ptr₃ },
  try { simp only [arg0] at h_call31 },
  try { rw [h_call25_ap_offset] at h_call31 }, try { arith_simps at h_call31 },
  rw [←htv_range_check_ptr₂, hl_range_check_ptr₂, hl_range_check_ptr₁, hin_range_check_ptr] at h_call31,
  clear arg0,
  -- local var
  step_assert_eq hpc31 with temp0,
  step_assert_eq hpc32 with temp1,
  step_assert_eq hpc33 with temp2,
  have lc_y: y = (cast_BigInt3 mem (σ.fp + 3)), {
    try { ext } ; {
      try { simp only [htv_y] },
      try { dsimp [cast_BigInt3] },
      try { arith_simps }, try { simp only [temp0, temp1, temp2] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  clear temp0 temp1 temp2,
  -- function call
  step_assert_eq hpc34 with arg0,
  step_assert_eq hpc35 with arg1,
  step_assert_eq hpc36 with arg2,
  step_assert_eq hpc37 with arg3,
  step_sub hpc38 (auto_sound_validate_reduced_field_element mem _ range_check_ptr₃ y _ _ _ _ _ _),
  { rw hpc39, norm_num2, exact h_mem_10 },
  { rw hpc39, norm_num2, exact h_mem_0 },
  { rw hpc39, norm_num2, exact h_mem_1 },
  { rw hpc39, norm_num2, exact h_mem_2 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y] },
    try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3] },
    try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  { try { ext } ; {
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y] },
      try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call40 ap40 h_call40,
  rcases h_call40 with ⟨rc_m40, rc_mle40, hl_range_check_ptr₄, h_call40⟩,
  mkdef htv_range_check_ptr₄ : range_check_ptr₄ = (mem (ap40 - 1)),
  simp only [←htv_range_check_ptr₄] at h_call40,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3] at hl_range_check_ptr₄ },
  try { rw [←htv_range_check_ptr₄] at hl_range_check_ptr₄ }, try { rw [←htv_range_check_ptr₃] at hl_range_check_ptr₄ },
  try { simp only [arg0 ,arg1 ,arg2 ,arg3] at h_call40 },
  rw [←htv_range_check_ptr₃, hl_range_check_ptr₃, hl_range_check_ptr₂, hl_range_check_ptr₁, hin_range_check_ptr] at h_call40,
  clear arg0 arg1 arg2 arg3,
  -- function call
  step_assert_eq hpc40 with arg0,
  step_assert_eq hpc41 with arg1,
  step_assert_eq hpc42 hpc43 with arg2,
  have h_δ40_c0 : ∀ x : F, x / (2 : ℤ) = x * (-1809251394333065606848661391547535052811553607665798349986546028067936010240 : ℤ),
  { intro x,  apply div_eq_mul_inv', apply PRIME.int_cast_mul_eq_one, rw [PRIME], try { simp_int_casts }, norm_num1 },
  have h_δ40_c0_fz : ∀ x : F, x / 2 = x / (2 : ℤ), { intro x, norm_cast }, 
  step_sub hpc44 (auto_sound_assert_nn mem _ range_check_ptr₄ ((y.d0 + v) / (2 : ℤ)) _ _ _),
  { rw hpc45, norm_num2, exact h_mem_0 },
  { try { simp only [h_δ40_c0_fz, h_δ40_c0] }, try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y, htv_range_check_ptr₄] },
    try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2] },
    try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  { try { simp only [h_δ40_c0_fz, h_δ40_c0] }, try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y, htv_range_check_ptr₄] },
    try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2] },
    try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  intros κ_call46 ap46 h_call46,
  rcases h_call46 with ⟨h_call46_ap_offset, h_call46⟩,
  rcases h_call46 with ⟨rc_m46, rc_mle46, hl_range_check_ptr₅, h_call46⟩,
  mkdef htv_range_check_ptr₅ : range_check_ptr₅ = (mem (ap46 - 1)),
  simp only [←htv_range_check_ptr₅] at h_call46,
  try { simp only [arg0 ,arg1 ,arg2] at hl_range_check_ptr₅ },
  try { rw [←htv_range_check_ptr₅] at hl_range_check_ptr₅ }, try { rw [←htv_range_check_ptr₄] at hl_range_check_ptr₅ },
  try { simp only [arg0 ,arg1 ,arg2] at h_call46 },
  rw [←htv_range_check_ptr₄, hl_range_check_ptr₄, hl_range_check_ptr₃, hl_range_check_ptr₂, hl_range_check_ptr₁, hin_range_check_ptr] at h_call46,
  clear arg0 arg1 arg2,
  -- function call
  step_assert_eq hpc46 with arg0,
  step_assert_eq hpc47 with arg1,
  step_assert_eq hpc48 with arg2,
  step_sub hpc49 (auto_sound_unreduced_sqr mem _ y _ _),
  { rw hpc50, norm_num2, exact h_mem_6 },
  { try { ext } ; {
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y, htv_range_check_ptr₄, htv_range_check_ptr₅] },
      try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset, h_call46_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call51 ap51 h_call51,
  rcases h_call51 with ⟨h_call51_ap_offset, h_call51⟩,
  mkdef htv_y_square : y_square = (cast_UnreducedBigInt3 mem (ap51 - 3)),
  simp only [←htv_y_square] at h_call51,
  clear arg0 arg1 arg2,
  -- function call
  step_assert_eq hpc51 hpc52 with arg0,
  step_assert_eq hpc53 with arg1,
  step_assert_eq hpc54 with arg2,
  step_assert_eq hpc55 with arg3,
  step_assert_eq hpc56 with arg4,
  step_sub hpc57 (auto_sound_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
  } _ _ _),
  { rw hpc58, norm_num2, exact h_mem_7 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y, htv_range_check_ptr₄, htv_range_check_ptr₅, htv_y_square] },
    try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1, (eq_sub_of_eq_add arg2), (eq_sub_of_eq_add arg3), (eq_sub_of_eq_add arg4)] },
    try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset, h_call46_ap_offset, h_call51_ap_offset] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  { try { ext } ; {
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y, htv_range_check_ptr₄, htv_range_check_ptr₅, htv_y_square] },
      try { dsimp [cast_BigInt3, cast_UnreducedBigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, (eq_sub_of_eq_add arg2), (eq_sub_of_eq_add arg3), (eq_sub_of_eq_add arg4)] },
      try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset, h_call46_ap_offset, h_call51_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call59 ap59 h_call59,
  rcases h_call59 with ⟨h_call59_ap_offset, h_call59⟩,
  rcases h_call59 with ⟨rc_m59, rc_mle59, hl_range_check_ptr₆, h_call59⟩,
  mkdef htv_range_check_ptr₆ : range_check_ptr₆ = (mem (ap59 - 1)),
  simp only [←htv_range_check_ptr₆] at h_call59,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4] at hl_range_check_ptr₆ },
  try { rw [h_call51_ap_offset] at hl_range_check_ptr₆ }, try { arith_simps at hl_range_check_ptr₆ },
  try { rw [←htv_range_check_ptr₆] at hl_range_check_ptr₆ }, try { rw [←htv_range_check_ptr₅] at hl_range_check_ptr₆ },
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4] at h_call59 },
  try { rw [h_call51_ap_offset] at h_call59 }, try { arith_simps at h_call59 },
  rw [←htv_range_check_ptr₅, hl_range_check_ptr₅, hl_range_check_ptr₄, hl_range_check_ptr₃, hl_range_check_ptr₂, hl_range_check_ptr₁, hin_range_check_ptr] at h_call59,
  clear arg0 arg1 arg2 arg3 arg4,
  -- return
  step_assert_eq hpc59 with hret0,
  step_assert_eq hpc60 with hret1,
  step_assert_eq hpc61 with hret2,
  step_assert_eq hpc62 with hret3,
  step_assert_eq hpc63 with hret4,
  step_assert_eq hpc64 with hret5,
  step_ret hpc65,
  -- finish
  step_done, use_only [rfl, rfl],
  -- range check condition
  use_only (rc_m6+rc_m17+rc_m31+rc_m40+rc_m46+rc_m59+0+0), split,
  linarith [rc_mle6, rc_mle17, rc_mle31, rc_mle40, rc_mle46, rc_mle59],
  split,
  { try { norm_num1 }, arith_simps, try { simp only [hret0 ,hret1 ,hret2 ,hret3 ,hret4 ,hret5] },
    try { rw [←htv_range_check_ptr₆] }, try { rw [hl_range_check_ptr₆] }, try { rw [←htv_range_check_ptr₅] }, try { rw [hl_range_check_ptr₅] }, try { rw [←htv_range_check_ptr₄] }, try { rw [hl_range_check_ptr₄] }, try { rw [←htv_range_check_ptr₃] }, try { rw [hl_range_check_ptr₃] }, try { rw [←htv_range_check_ptr₂] }, try { rw [hl_range_check_ptr₂] }, try { rw [←htv_range_check_ptr₁] }, try { rw [hl_range_check_ptr₁] }, try { rw [hin_range_check_ptr] },
    try { ring_nf }, try { arith_simps, refl <|> norm_cast }, try { refl } },
  intro rc_h_range_check_ptr, repeat { rw [add_assoc] at rc_h_range_check_ptr },
  have rc_h_range_check_ptr' := range_checked_add_right rc_h_range_check_ptr,
  -- Final Proof
  -- user-provided reduction
  suffices auto_spec: auto_spec_get_point_from_x mem _ range_check_ptr x v _ _,
  { apply sound_get_point_from_x, apply auto_spec },
  -- prove the auto generated assertion
  dsimp [auto_spec_get_point_from_x],
  try { norm_num1 }, try { arith_simps },
  use_only [κ_call6],
  use_only [range_check_ptr₁],
  have rc_h_range_check_ptr₁ := range_checked_offset' rc_h_range_check_ptr,
  have rc_h_range_check_ptr₁' := range_checked_add_right rc_h_range_check_ptr₁, try { norm_cast at rc_h_range_check_ptr₁' },
  have spec6 := h_call6 rc_h_range_check_ptr',
    try { rw [←hin_range_check_ptr] at spec6 }, try { rw [←htv_range_check_ptr₁] at spec6 },
  try { dsimp at spec6, arith_simps at spec6 },
  use_only [spec6],
  use_only [κ_call11],
  use_only [x_square],
  try { dsimp at h_call11, arith_simps at h_call11 },
  try { use_only [h_call11] },
  use_only [κ_call17],
  use_only [range_check_ptr₂],
  use_only [x_square_reduced],
  have rc_h_range_check_ptr₂ := range_checked_offset' rc_h_range_check_ptr₁,
  have rc_h_range_check_ptr₂' := range_checked_add_right rc_h_range_check_ptr₂, try { norm_cast at rc_h_range_check_ptr₂' },
  have spec17 := h_call17 rc_h_range_check_ptr₁',
    try { rw [←hin_range_check_ptr] at spec17 }, try { rw [←hl_range_check_ptr₁] at spec17 }, try { rw [←htv_range_check_ptr₂] at spec17 },
  try { dsimp at spec17, arith_simps at spec17 },
  use_only [spec17],
  use_only [κ_call25],
  use_only [x_cube],
  try { dsimp at h_call25, arith_simps at h_call25 },
  try { use_only [h_call25] },
  use_only [κ_call31],
  use_only [range_check_ptr₃],
  use_only [y],
  have rc_h_range_check_ptr₃ := range_checked_offset' rc_h_range_check_ptr₂,
  have rc_h_range_check_ptr₃' := range_checked_add_right rc_h_range_check_ptr₃, try { norm_cast at rc_h_range_check_ptr₃' },
  have spec31 := h_call31 rc_h_range_check_ptr₂',
    try { rw [←hin_range_check_ptr] at spec31 }, try { rw [←hl_range_check_ptr₁] at spec31 }, try { rw [←hl_range_check_ptr₂] at spec31 }, try { rw [←htv_range_check_ptr₃] at spec31 },
  try { dsimp at spec31, arith_simps at spec31 },
  use_only [spec31],
  use_only [κ_call40],
  use_only [range_check_ptr₄],
  have rc_h_range_check_ptr₄ := range_checked_offset' rc_h_range_check_ptr₃,
  have rc_h_range_check_ptr₄' := range_checked_add_right rc_h_range_check_ptr₄, try { norm_cast at rc_h_range_check_ptr₄' },
  have spec40 := h_call40 rc_h_range_check_ptr₃',
    try { rw [←hin_range_check_ptr] at spec40 }, try { rw [←hl_range_check_ptr₁] at spec40 }, try { rw [←hl_range_check_ptr₂] at spec40 }, try { rw [←hl_range_check_ptr₃] at spec40 }, try { rw [←htv_range_check_ptr₄] at spec40 },
  try { dsimp at spec40, arith_simps at spec40 },
  use_only [spec40],
  use_only [κ_call46],
  use_only [range_check_ptr₅],
  have rc_h_range_check_ptr₅ := range_checked_offset' rc_h_range_check_ptr₄,
  have rc_h_range_check_ptr₅' := range_checked_add_right rc_h_range_check_ptr₅, try { norm_cast at rc_h_range_check_ptr₅' },
  have spec46 := h_call46 rc_h_range_check_ptr₄',
    try { rw [←hin_range_check_ptr] at spec46 }, try { rw [←hl_range_check_ptr₁] at spec46 }, try { rw [←hl_range_check_ptr₂] at spec46 }, try { rw [←hl_range_check_ptr₃] at spec46 }, try { rw [←hl_range_check_ptr₄] at spec46 }, try { rw [←htv_range_check_ptr₅] at spec46 },
  try { dsimp at spec46, arith_simps at spec46 },
  use_only [spec46],
  use_only [κ_call51],
  use_only [y_square],
  try { dsimp at h_call51, arith_simps at h_call51 },
  try { use_only [h_call51] },
  use_only [κ_call59],
  use_only [range_check_ptr₆],
  have rc_h_range_check_ptr₆ := range_checked_offset' rc_h_range_check_ptr₅,
  have rc_h_range_check_ptr₆' := range_checked_add_right rc_h_range_check_ptr₆, try { norm_cast at rc_h_range_check_ptr₆' },
  have spec59 := h_call59 rc_h_range_check_ptr₅',
    try { rw [←hin_range_check_ptr] at spec59 }, try { rw [←hl_range_check_ptr₁] at spec59 }, try { rw [←hl_range_check_ptr₂] at spec59 }, try { rw [←hl_range_check_ptr₃] at spec59 }, try { rw [←hl_range_check_ptr₄] at spec59 }, try { rw [←hl_range_check_ptr₅] at spec59 }, try { rw [←htv_range_check_ptr₆] at spec59 },
  try { dsimp at spec59, arith_simps at spec59 },
  use_only [spec59],
  try { split, trivial <|> linarith },
  try { ensures_simps; try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_x, hin_v, htv_range_check_ptr₁, htv_x_square, htv_range_check_ptr₂, htv_x_square_reduced, htv_x_cube, lc_x_cube, htv_range_check_ptr₃, htv_y, lc_y, htv_range_check_ptr₄, htv_range_check_ptr₅, htv_y_square, htv_range_check_ptr₆] }, },
  try { dsimp [cast_BigInt3, cast_UnreducedBigInt3, cast_EcPoint] },
  try { arith_simps }, try { simp only [hret0, hret1, hret2, hret3, hret4, hret5] },
  try { simp only [h_call6_ap_offset, h_call11_ap_offset, h_call17_ap_offset, h_call25_ap_offset, h_call31_ap_offset, h_call46_ap_offset, h_call51_ap_offset, h_call59_ap_offset] },
  try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
end