signature_recover_public_key_recover_public_key_soundness.lean

/-
File: signature_recover_public_key_recover_public_key_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_ec_negate_soundness
import .signature_recover_public_key_get_point_from_x_soundness
import .signature_recover_public_key_ec_mul_soundness
import .signature_recover_public_key_get_generator_point_soundness
import .signature_recover_public_key_div_mod_n_soundness
open tactic

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

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.recover_public_key autogenerated soundness theorem -/

theorem auto_sound_recover_public_key
    -- arguments
    (range_check_ptr : F) (msg_hash r s : BigInt3 mem) (v : F)
    -- code is in memory at σ.pc
    (h_mem : mem_at mem code_recover_public_key σ.pc)
    -- all dependencies are in memory
    (h_mem_0 : mem_at mem code_assert_nn (σ.pc  - 817))
    (h_mem_1 : mem_at mem code_assert_le (σ.pc  - 813))
    (h_mem_2 : mem_at mem code_assert_nn_le (σ.pc  - 808))
    (h_mem_3 : mem_at mem code_bigint_mul (σ.pc  - 799))
    (h_mem_4 : mem_at mem code_nondet_bigint3 (σ.pc  - 785))
    (h_mem_5 : mem_at mem code_unreduced_mul (σ.pc  - 773))
    (h_mem_6 : mem_at mem code_unreduced_sqr (σ.pc  - 753))
    (h_mem_7 : mem_at mem code_verify_zero (σ.pc  - 737))
    (h_mem_8 : mem_at mem code_is_zero (σ.pc  - 714))
    (h_mem_9 : mem_at mem code_reduce (σ.pc  - 678))
    (h_mem_10 : mem_at mem code_validate_reduced_field_element (σ.pc  - 665))
    (h_mem_11 : mem_at mem code_ec_negate (σ.pc  - 625))
    (h_mem_12 : mem_at mem code_compute_doubling_slope (σ.pc  - 609))
    (h_mem_13 : mem_at mem code_compute_slope (σ.pc  - 565))
    (h_mem_14 : mem_at mem code_ec_double (σ.pc  - 541))
    (h_mem_15 : mem_at mem code_fast_ec_add (σ.pc  - 468))
    (h_mem_16 : mem_at mem code_ec_add (σ.pc  - 381))
    (h_mem_17 : mem_at mem code_ec_mul_inner (σ.pc  - 325))
    (h_mem_18 : mem_at mem code_ec_mul (σ.pc  - 224))
    (h_mem_19 : mem_at mem code_get_generator_point (σ.pc  - 144))
    (h_mem_20 : mem_at mem code_div_mod_n (σ.pc  - 131))
    (h_mem_21 : mem_at mem code_get_point_from_x (σ.pc  - 66))
    -- input arguments on the stack
    (hin_range_check_ptr : range_check_ptr = mem (σ.fp - 13))
    (hin_msg_hash : msg_hash = cast_BigInt3 mem (σ.fp - 12))
    (hin_r : r = cast_BigInt3 mem (σ.fp - 9))
    (hin_s : s = cast_BigInt3 mem (σ.fp - 6))
    (hin_v : v = mem (σ.fp - 3))
    -- conclusion
  : ensures_ret mem σ (λ κ τ,
      ∃ μ ≤ κ, rc_ensures mem (rc_bound F) μ (mem (σ.fp - 13)) (mem $ τ.ap - 7)
        (spec_recover_public_key mem κ range_check_ptr msg_hash r s 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_recover_public_key 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, hpc66, hpc67, hpc68, hpc69, hpc70, hpc71, hpc72, hpc73, hpc74, hpc75, hpc76, hpc77, hpc78, hpc79, hpc80, hpc81, hpc82, hpc83, hpc84, hpc85⟩,
  -- ap += 15
  step_advance_ap hpc0 hpc1,
  -- function call
  step_assert_eq hpc2 with arg0,
  step_assert_eq hpc3 with arg1,
  step_assert_eq hpc4 with arg2,
  step_assert_eq hpc5 with arg3,
  step_assert_eq hpc6 with arg4,
  step_sub hpc7 (auto_sound_get_point_from_x mem _ range_check_ptr r v _ _ _ _ _ _ _ _ _ _ _ _ _),
  { rw hpc8, norm_num2, exact h_mem_21 },
  { rw hpc8, norm_num2, exact h_mem_0 },
  { rw hpc8, norm_num2, exact h_mem_1 },
  { rw hpc8, norm_num2, exact h_mem_2 },
  { rw hpc8, norm_num2, exact h_mem_4 },
  { rw hpc8, norm_num2, exact h_mem_5 },
  { rw hpc8, norm_num2, exact h_mem_6 },
  { rw hpc8, norm_num2, exact h_mem_7 },
  { rw hpc8, norm_num2, exact h_mem_9 },
  { rw hpc8, norm_num2, exact h_mem_10 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4] },
    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_msg_hash, hin_r, hin_s, hin_v] },
      try { dsimp [cast_BigInt3] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  intros κ_call9 ap9 h_call9,
  rcases h_call9 with ⟨rc_m9, rc_mle9, hl_range_check_ptr₁, h_call9⟩,
  mkdef htv_range_check_ptr₁ : range_check_ptr₁ = (mem (ap9 - 7)),
  simp only [←htv_range_check_ptr₁] at h_call9,
  mkdef htv_r_point : r_point = (cast_EcPoint mem (ap9 - 6)),
  simp only [←htv_r_point] at h_call9,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4] 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 ,arg2 ,arg3 ,arg4] at h_call9 },
  rw [hin_range_check_ptr] at h_call9,
  clear arg0 arg1 arg2 arg3 arg4,
  -- local var
  step_assert_eq hpc9 with temp0,
  step_assert_eq hpc10 with temp1,
  step_assert_eq hpc11 with temp2,
  step_assert_eq hpc12 with temp3,
  step_assert_eq hpc13 with temp4,
  step_assert_eq hpc14 with temp5,
  have lc_r_point: r_point = (cast_EcPoint mem (σ.fp)), {
    try { ext } ; {
      try { simp only [htv_r_point] },
      try { dsimp [cast_EcPoint, cast_BigInt3] },
      try { arith_simps }, try { simp only [temp0, temp1, temp2, temp3, temp4, temp5] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  clear temp0 temp1 temp2 temp3 temp4 temp5,
  -- function call
  step_sub hpc15 (auto_sound_get_generator_point mem _  _),
  { rw hpc16, norm_num2, exact h_mem_19 },
  intros κ_call17 ap17 h_call17,
  rcases h_call17 with ⟨h_call17_ap_offset, h_call17⟩,
  mkdef htv_generator_point : generator_point = (cast_EcPoint mem (ap17 - 6)),
  simp only [←htv_generator_point] at h_call17,
  clear ,
  -- 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_assert_eq hpc23 with arg6,
  step_sub hpc24 (auto_sound_div_mod_n mem _ range_check_ptr₁ msg_hash r _ _ _ _ _ _),
  { rw hpc25, norm_num2, exact h_mem_20 },
  { rw hpc25, norm_num2, exact h_mem_3 },
  { rw hpc25, norm_num2, exact h_mem_4 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point] },
    try { dsimp [cast_BigInt3, cast_EcPoint] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6] },
    try { simp only [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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6] },
      try { simp only [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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6] },
      try { simp only [h_call17_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call26 ap26 h_call26,
  rcases h_call26 with ⟨h_call26_ap_offset, h_call26⟩,
  rcases h_call26 with ⟨rc_m26, rc_mle26, hl_range_check_ptr₂, h_call26⟩,
  mkdef htv_range_check_ptr₂ : range_check_ptr₂ = (mem (ap26 - 4)),
  simp only [←htv_range_check_ptr₂] at h_call26,
  mkdef htv_u1 : u1 = (cast_BigInt3 mem (ap26 - 3)),
  simp only [←htv_u1] at h_call26,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4 ,arg5 ,arg6] at hl_range_check_ptr₂ },
  try { rw [h_call17_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 ,arg5 ,arg6] at h_call26 },
  try { rw [h_call17_ap_offset] at h_call26 }, try { arith_simps at h_call26 },
  rw [←htv_range_check_ptr₁, hl_range_check_ptr₁, hin_range_check_ptr] at h_call26,
  clear arg0 arg1 arg2 arg3 arg4 arg5 arg6,
  -- function call
  step_assert_eq hpc26 with arg0,
  step_assert_eq hpc27 with arg1,
  step_assert_eq hpc28 with arg2,
  step_assert_eq hpc29 with arg3,
  step_assert_eq hpc30 with arg4,
  step_assert_eq hpc31 with arg5,
  step_assert_eq hpc32 with arg6,
  step_sub hpc33 (auto_sound_div_mod_n mem _ range_check_ptr₂ s r _ _ _ _ _ _),
  { rw hpc34, norm_num2, exact h_mem_20 },
  { rw hpc34, norm_num2, exact h_mem_3 },
  { rw hpc34, norm_num2, exact h_mem_4 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1] },
    try { dsimp [cast_BigInt3, cast_EcPoint] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6] },
    try { simp only [h_call17_ap_offset, h_call26_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6] },
      try { simp only [h_call17_ap_offset, h_call26_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call35 ap35 h_call35,
  rcases h_call35 with ⟨h_call35_ap_offset, h_call35⟩,
  rcases h_call35 with ⟨rc_m35, rc_mle35, hl_range_check_ptr₃, h_call35⟩,
  mkdef htv_range_check_ptr₃ : range_check_ptr₃ = (mem (ap35 - 4)),
  simp only [←htv_range_check_ptr₃] at h_call35,
  mkdef htv_u2 : u2 = (cast_BigInt3 mem (ap35 - 3)),
  simp only [←htv_u2] at h_call35,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4 ,arg5 ,arg6] 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 ,arg5 ,arg6] at h_call35 },
  rw [←htv_range_check_ptr₂, hl_range_check_ptr₂, hl_range_check_ptr₁, hin_range_check_ptr] at h_call35,
  clear arg0 arg1 arg2 arg3 arg4 arg5 arg6,
  -- local var
  step_assert_eq hpc35 with temp0,
  step_assert_eq hpc36 with temp1,
  step_assert_eq hpc37 with temp2,
  have lc_u2: u2 = (cast_BigInt3 mem (σ.fp + 6)), {
    try { ext } ; {
      try { simp only [htv_u2] },
      try { dsimp [cast_BigInt3] },
      try { arith_simps }, try { simp only [temp0, temp1, temp2] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  clear temp0 temp1 temp2,
  -- function call
  step_assert_eq hpc38 with arg0,
  step_assert_eq hpc39 with arg1,
  step_assert_eq hpc40 with arg2,
  step_assert_eq hpc41 with arg3,
  step_assert_eq hpc42 with arg4,
  step_assert_eq hpc43 with arg5,
  step_assert_eq hpc44 with arg6,
  step_assert_eq hpc45 with arg7,
  step_assert_eq hpc46 with arg8,
  step_assert_eq hpc47 with arg9,
  step_sub hpc48 (auto_sound_ec_mul mem _ range_check_ptr₃ generator_point u1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _),
  { rw hpc49, norm_num2, exact h_mem_18 },
  { rw hpc49, norm_num2, exact h_mem_4 },
  { rw hpc49, norm_num2, exact h_mem_5 },
  { rw hpc49, norm_num2, exact h_mem_6 },
  { rw hpc49, norm_num2, exact h_mem_7 },
  { rw hpc49, norm_num2, exact h_mem_8 },
  { rw hpc49, norm_num2, exact h_mem_12 },
  { rw hpc49, norm_num2, exact h_mem_13 },
  { rw hpc49, norm_num2, exact h_mem_14 },
  { rw hpc49, norm_num2, exact h_mem_15 },
  { rw hpc49, norm_num2, exact h_mem_16 },
  { rw hpc49, norm_num2, exact h_mem_17 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2] },
    try { dsimp [cast_BigInt3, cast_EcPoint] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9] },
    try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call50 ap50 h_call50,
  rcases h_call50 with ⟨rc_m50, rc_mle50, hl_range_check_ptr₄, h_call50⟩,
  mkdef htv_range_check_ptr₄ : range_check_ptr₄ = (mem (ap50 - 7)),
  simp only [←htv_range_check_ptr₄] at h_call50,
  mkdef htv_point1 : point1 = (cast_EcPoint mem (ap50 - 6)),
  simp only [←htv_point1] at h_call50,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4 ,arg5 ,arg6 ,arg7 ,arg8 ,arg9] 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 ,arg5 ,arg6 ,arg7 ,arg8 ,arg9] at h_call50 },
  rw [←htv_range_check_ptr₃, hl_range_check_ptr₃, hl_range_check_ptr₂, hl_range_check_ptr₁, hin_range_check_ptr] at h_call50,
  clear arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9,
  -- function call
  step_sub hpc50 (auto_sound_ec_negate mem _ range_check_ptr₄ point1 _ _ _ _ _),
  { rw hpc51, norm_num2, exact h_mem_11 },
  { rw hpc51, norm_num2, exact h_mem_4 },
  { rw hpc51, norm_num2, exact h_mem_7 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1] },
    try { dsimp [cast_BigInt3, cast_EcPoint] },
    try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call52 ap52 h_call52,
  rcases h_call52 with ⟨h_call52_ap_offset, h_call52⟩,
  rcases h_call52 with ⟨rc_m52, rc_mle52, hl_range_check_ptr₅, h_call52⟩,
  mkdef htv_range_check_ptr₅ : range_check_ptr₅ = (mem (ap52 - 7)),
  simp only [←htv_range_check_ptr₅] at h_call52,
  mkdef htv_minus_point1 : minus_point1 = (cast_EcPoint mem (ap52 - 6)),
  simp only [←htv_minus_point1] at h_call52,
  try { rw [←htv_range_check_ptr₅] at hl_range_check_ptr₅ }, try { rw [←htv_range_check_ptr₄] at hl_range_check_ptr₅ },
  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_call52,
  clear ,
  -- local var
  step_assert_eq hpc52 with temp0,
  step_assert_eq hpc53 with temp1,
  step_assert_eq hpc54 with temp2,
  step_assert_eq hpc55 with temp3,
  step_assert_eq hpc56 with temp4,
  step_assert_eq hpc57 with temp5,
  have lc_minus_point1: minus_point1 = (cast_EcPoint mem (σ.fp + 9)), {
    try { ext } ; {
      try { simp only [htv_minus_point1] },
      try { dsimp [cast_EcPoint, cast_BigInt3] },
      try { arith_simps }, try { simp only [temp0, temp1, temp2, temp3, temp4, temp5] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  clear temp0 temp1 temp2 temp3 temp4 temp5,
  -- function call
  step_assert_eq hpc58 with arg0,
  step_assert_eq hpc59 with arg1,
  step_assert_eq hpc60 with arg2,
  step_assert_eq hpc61 with arg3,
  step_assert_eq hpc62 with arg4,
  step_assert_eq hpc63 with arg5,
  step_assert_eq hpc64 with arg6,
  step_assert_eq hpc65 with arg7,
  step_assert_eq hpc66 with arg8,
  step_assert_eq hpc67 with arg9,
  step_sub hpc68 (auto_sound_ec_mul mem _ range_check_ptr₅ r_point u2 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _),
  { rw hpc69, norm_num2, exact h_mem_18 },
  { rw hpc69, norm_num2, exact h_mem_4 },
  { rw hpc69, norm_num2, exact h_mem_5 },
  { rw hpc69, norm_num2, exact h_mem_6 },
  { rw hpc69, norm_num2, exact h_mem_7 },
  { rw hpc69, norm_num2, exact h_mem_8 },
  { rw hpc69, norm_num2, exact h_mem_12 },
  { rw hpc69, norm_num2, exact h_mem_13 },
  { rw hpc69, norm_num2, exact h_mem_14 },
  { rw hpc69, norm_num2, exact h_mem_15 },
  { rw hpc69, norm_num2, exact h_mem_16 },
  { rw hpc69, norm_num2, exact h_mem_17 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1, htv_range_check_ptr₅, htv_minus_point1, lc_minus_point1] },
    try { dsimp [cast_BigInt3, cast_EcPoint] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9] },
    try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1, htv_range_check_ptr₅, htv_minus_point1, lc_minus_point1] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1, htv_range_check_ptr₅, htv_minus_point1, lc_minus_point1] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call70 ap70 h_call70,
  rcases h_call70 with ⟨rc_m70, rc_mle70, hl_range_check_ptr₆, h_call70⟩,
  mkdef htv_range_check_ptr₆ : range_check_ptr₆ = (mem (ap70 - 7)),
  simp only [←htv_range_check_ptr₆] at h_call70,
  mkdef htv_point2 : point2 = (cast_EcPoint mem (ap70 - 6)),
  simp only [←htv_point2] at h_call70,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4 ,arg5 ,arg6 ,arg7 ,arg8 ,arg9] 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 ,arg5 ,arg6 ,arg7 ,arg8 ,arg9] at h_call70 },
  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_call70,
  clear arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9,
  -- function call
  step_assert_eq hpc70 with arg0,
  step_assert_eq hpc71 with arg1,
  step_assert_eq hpc72 with arg2,
  step_assert_eq hpc73 with arg3,
  step_assert_eq hpc74 with arg4,
  step_assert_eq hpc75 with arg5,
  step_assert_eq hpc76 with arg6,
  step_assert_eq hpc77 with arg7,
  step_assert_eq hpc78 with arg8,
  step_assert_eq hpc79 with arg9,
  step_assert_eq hpc80 with arg10,
  step_assert_eq hpc81 with arg11,
  step_assert_eq hpc82 with arg12,
  step_sub hpc83 (auto_sound_ec_add mem _ range_check_ptr₆ minus_point1 point2 _ _ _ _ _ _ _ _ _ _ _ _ _),
  { rw hpc84, norm_num2, exact h_mem_16 },
  { rw hpc84, norm_num2, exact h_mem_4 },
  { rw hpc84, norm_num2, exact h_mem_5 },
  { rw hpc84, norm_num2, exact h_mem_6 },
  { rw hpc84, norm_num2, exact h_mem_7 },
  { rw hpc84, norm_num2, exact h_mem_8 },
  { rw hpc84, norm_num2, exact h_mem_12 },
  { rw hpc84, norm_num2, exact h_mem_13 },
  { rw hpc84, norm_num2, exact h_mem_14 },
  { rw hpc84, norm_num2, exact h_mem_15 },
  { try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1, htv_range_check_ptr₅, htv_minus_point1, lc_minus_point1, htv_range_check_ptr₆, htv_point2] },
    try { dsimp [cast_BigInt3, cast_EcPoint] },
    try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12] },
    try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1, htv_range_check_ptr₅, htv_minus_point1, lc_minus_point1, htv_range_check_ptr₆, htv_point2] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_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_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1, htv_range_check_ptr₅, htv_minus_point1, lc_minus_point1, htv_range_check_ptr₆, htv_point2] },
      try { dsimp [cast_BigInt3, cast_EcPoint] },
      try { arith_simps }, try { simp only [arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12] },
      try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_ap_offset] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
  intros κ_call85 ap85 h_call85,
  rcases h_call85 with ⟨rc_m85, rc_mle85, hl_range_check_ptr₇, h_call85⟩,
  mkdef htv_range_check_ptr₇ : range_check_ptr₇ = (mem (ap85 - 7)),
  simp only [←htv_range_check_ptr₇] at h_call85,
  mkdef htv_public_key_point : public_key_point = (cast_EcPoint mem (ap85 - 6)),
  simp only [←htv_public_key_point] at h_call85,
  try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4 ,arg5 ,arg6 ,arg7 ,arg8 ,arg9 ,arg10 ,arg11 ,arg12] 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 ,arg5 ,arg6 ,arg7 ,arg8 ,arg9 ,arg10 ,arg11 ,arg12] at h_call85 },
  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₂, hl_range_check_ptr₁, hin_range_check_ptr] at h_call85,
  clear arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11 arg12,
  -- return
  step_ret hpc85,
  -- finish
  step_done, use_only [rfl, rfl],
  -- range check condition
  use_only (rc_m9+rc_m26+rc_m35+rc_m50+rc_m52+rc_m70+rc_m85+0+0), split,
  linarith [rc_mle9, rc_mle26, rc_mle35, rc_mle50, rc_mle52, rc_mle70, rc_mle85],
  split,
  { try { norm_num1 }, arith_simps,
    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 [←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_recover_public_key mem _ range_check_ptr msg_hash r s v _ _,
  { apply sound_recover_public_key, apply auto_spec },
  -- prove the auto generated assertion
  dsimp [auto_spec_recover_public_key],
  try { norm_num1 }, try { arith_simps },
  use_only [κ_call9],
  use_only [range_check_ptr₁],
  use_only [r_point],
  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 spec9 := h_call9 rc_h_range_check_ptr',
    try { rw [←hin_range_check_ptr] at spec9 }, try { rw [←htv_range_check_ptr₁] at spec9 },
  try { dsimp at spec9, arith_simps at spec9 },
  use_only [spec9],
  use_only [κ_call17],
  use_only [generator_point],
  try { dsimp at h_call17, arith_simps at h_call17 },
  try { use_only [h_call17] },
  use_only [κ_call26],
  use_only [range_check_ptr₂],
  use_only [u1],
  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 spec26 := h_call26 rc_h_range_check_ptr₁',
    try { rw [←hin_range_check_ptr] at spec26 }, try { rw [←hl_range_check_ptr₁] at spec26 }, try { rw [←htv_range_check_ptr₂] at spec26 },
  try { dsimp at spec26, arith_simps at spec26 },
  use_only [spec26],
  use_only [κ_call35],
  use_only [range_check_ptr₃],
  use_only [u2],
  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 spec35 := h_call35 rc_h_range_check_ptr₂',
    try { rw [←hin_range_check_ptr] at spec35 }, try { rw [←hl_range_check_ptr₁] at spec35 }, try { rw [←hl_range_check_ptr₂] at spec35 }, try { rw [←htv_range_check_ptr₃] at spec35 },
  try { dsimp at spec35, arith_simps at spec35 },
  use_only [spec35],
  use_only [κ_call50],
  use_only [range_check_ptr₄],
  use_only [point1],
  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 spec50 := h_call50 rc_h_range_check_ptr₃',
    try { rw [←hin_range_check_ptr] at spec50 }, try { rw [←hl_range_check_ptr₁] at spec50 }, try { rw [←hl_range_check_ptr₂] at spec50 }, try { rw [←hl_range_check_ptr₃] at spec50 }, try { rw [←htv_range_check_ptr₄] at spec50 },
  try { dsimp at spec50, arith_simps at spec50 },
  use_only [spec50],
  use_only [κ_call52],
  use_only [range_check_ptr₅],
  use_only [minus_point1],
  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 spec52 := h_call52 rc_h_range_check_ptr₄',
    try { rw [←hin_range_check_ptr] at spec52 }, try { rw [←hl_range_check_ptr₁] at spec52 }, try { rw [←hl_range_check_ptr₂] at spec52 }, try { rw [←hl_range_check_ptr₃] at spec52 }, try { rw [←hl_range_check_ptr₄] at spec52 }, try { rw [←htv_range_check_ptr₅] at spec52 },
  try { dsimp at spec52, arith_simps at spec52 },
  use_only [spec52],
  use_only [κ_call70],
  use_only [range_check_ptr₆],
  use_only [point2],
  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 spec70 := h_call70 rc_h_range_check_ptr₅',
    try { rw [←hin_range_check_ptr] at spec70 }, try { rw [←hl_range_check_ptr₁] at spec70 }, try { rw [←hl_range_check_ptr₂] at spec70 }, try { rw [←hl_range_check_ptr₃] at spec70 }, try { rw [←hl_range_check_ptr₄] at spec70 }, try { rw [←hl_range_check_ptr₅] at spec70 }, try { rw [←htv_range_check_ptr₆] at spec70 },
  try { dsimp at spec70, arith_simps at spec70 },
  use_only [spec70],
  use_only [κ_call85],
  use_only [range_check_ptr₇],
  use_only [public_key_point],
  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 spec85 := h_call85 rc_h_range_check_ptr₆',
    try { rw [←hin_range_check_ptr] at spec85 }, try { rw [←hl_range_check_ptr₁] at spec85 }, try { rw [←hl_range_check_ptr₂] at spec85 }, try { rw [←hl_range_check_ptr₃] at spec85 }, try { rw [←hl_range_check_ptr₄] at spec85 }, try { rw [←hl_range_check_ptr₅] at spec85 }, try { rw [←hl_range_check_ptr₆] at spec85 }, try { rw [←htv_range_check_ptr₇] at spec85 },
  try { dsimp at spec85, arith_simps at spec85 },
  use_only [spec85],
  try { split, trivial <|> linarith },
  try { ensures_simps; try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_msg_hash, hin_r, hin_s, hin_v, htv_range_check_ptr₁, htv_r_point, lc_r_point, htv_generator_point, htv_range_check_ptr₂, htv_u1, htv_range_check_ptr₃, htv_u2, lc_u2, htv_range_check_ptr₄, htv_point1, htv_range_check_ptr₅, htv_minus_point1, lc_minus_point1, htv_range_check_ptr₆, htv_point2, htv_range_check_ptr₇, htv_public_key_point] }, },
  try { dsimp [cast_BigInt3, cast_EcPoint] },
  try { simp only [h_call17_ap_offset, h_call26_ap_offset, h_call35_ap_offset, h_call52_ap_offset] },
  try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
end