/-
File: signature_recover_public_key_nondet_bigint3_soundness.lean

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

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

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

/- starkware.cairo.common.cairo_secp.bigint.nondet_bigint3 autogenerated soundness theorem -/

theorem auto_sound_nondet_bigint3
    -- arguments
    (range_check_ptr : F)
    -- code is in memory at σ.pc
    (h_mem : mem_at mem code_nondet_bigint3 σ.pc)
    -- input arguments on the stack
    (hin_range_check_ptr : range_check_ptr = mem (σ.fp - 3))
    -- conclusion
  : ensures_ret mem σ (λ κ τ,
      τ.ap = σ.ap + 8 ∧
      ∃ μ ≤ κ, rc_ensures mem (rc_bound F) μ (mem (σ.fp - 3)) (mem $ τ.ap - 4)
        (spec_nondet_bigint3 mem κ range_check_ptr (mem (τ.ap - 4)) (cast_BigInt3 mem (τ.ap - 3)))) :=
begin
  apply ensures_of_ensuresb, intro νbound,
  have h_mem_rec := h_mem,
  unpack_memory code_nondet_bigint3 at h_mem with ⟨hpc0, hpc1, hpc2, hpc3, hpc4, hpc5, hpc6, hpc7, hpc8, hpc9, hpc10, hpc11⟩,
  -- let (ap reference)
  apply of_register_state,
  intros regstate_res regstateeq_res,
  generalize' hl_rev_res: cast_BigInt3 mem (regstate_res.ap + 5) = res,
  have hl_res := hl_rev_res.symm,
  rw [regstateeq_res] at hl_res, try { dsimp at hl_res },
  -- const
  set! MAX_SUM := (232113757366008801543585789 : F) with hc_MAX_SUM,
  -- compound assert eq
  step_assert_eq hpc0 hpc1 with temp0,
  step_assert_eq hpc2 with temp1,
  step_assert_eq hpc3 with temp2,
  step_assert_eq hpc4 with temp3,
  step_assert_eq hpc5 with temp4,
  have a0: mem (range_check_ptr) = MAX_SUM - (res.d0 + res.d1 + res.d2), {
    apply assert_eq_reduction temp4.symm,
    try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps }, try { simp only [temp0, temp1, temp2, (eq_sub_of_eq_add temp3)] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
  },
  try { dsimp at a0 }, try { arith_simps at a0 },
  clear temp0 temp1 temp2 temp3 temp4,
  -- tempvar
  step_assert_eq hpc6 hpc7 with tv_range_check_ptr0,
  generalize' hl_rev_range_check_ptr₁: (range_check_ptr + 4 : F) = range_check_ptr₁,
  have hl_range_check_ptr₁ := hl_rev_range_check_ptr₁.symm, clear hl_rev_range_check_ptr₁,
  have htv_range_check_ptr₁: range_check_ptr₁ = _, {
    apply eq.symm, apply eq.trans tv_range_check_ptr0,
      try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁] },
      try { dsimp [cast_BigInt3] },
      try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
  clear tv_range_check_ptr0,
  try { dsimp at hl_range_check_ptr₁ }, try { arith_simps at hl_range_check_ptr₁ },
  -- assert eq
  step_assert_eq hpc8 with temp0,
  have a8: mem (range_check_ptr₁ - 3) = res.d0, {
    apply assert_eq_reduction temp0.symm,
    try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
  },
  try { dsimp at a8 }, try { arith_simps at a8 },
  clear temp0,
  -- assert eq
  step_assert_eq hpc9 with temp0,
  have a9: mem (range_check_ptr₁ - 2) = res.d1, {
    apply assert_eq_reduction temp0.symm,
    try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
  },
  try { dsimp at a9 }, try { arith_simps at a9 },
  clear temp0,
  -- assert eq
  step_assert_eq hpc10 with temp0,
  have a10: mem (range_check_ptr₁ - 1) = res.d2, {
    apply assert_eq_reduction temp0.symm,
    try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] },
    try { dsimp [cast_BigInt3] },
    try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
  },
  try { dsimp at a10 }, try { arith_simps at a10 },
  clear temp0,
  -- return
  step_ret hpc11,
  -- finish
  step_done, use_only [rfl, rfl],
  split, refl,
  -- range check condition
  use_only (4+0+0), split,
  linarith [],
  split,
  { arith_simps,
    rw [←htv_range_check_ptr₁, hl_range_check_ptr₁, hin_range_check_ptr],
    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_nondet_bigint3 mem _ range_check_ptr _ _,
  { apply sound_nondet_bigint3, apply auto_spec },
  -- prove the auto generated assertion
  dsimp [auto_spec_nondet_bigint3],
  try { norm_num1 }, try { arith_simps },
  use_only [res],
  use [MAX_SUM, hc_MAX_SUM],
  use_only [a0],
  cases rc_h_range_check_ptr' (0) (by norm_num1) with n hn, arith_simps at hn,
  use_only [n], { simp only [a0.symm, hin_range_check_ptr], arith_simps, exact hn },
  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₁' },
  use_only [range_check_ptr₁, hl_range_check_ptr₁],
  use_only [a8],
  cases rc_h_range_check_ptr' (1) (by norm_num1) with n hn, arith_simps at hn,
  use_only [n], { simp only [a8.symm, hl_range_check_ptr₁, hin_range_check_ptr], arith_simps, exact hn },
  use_only [a9],
  cases rc_h_range_check_ptr' (2) (by norm_num1) with n hn, arith_simps at hn,
  use_only [n], { simp only [a9.symm, hl_range_check_ptr₁, hin_range_check_ptr], arith_simps, exact hn },
  use_only [a10],
  cases rc_h_range_check_ptr' (3) (by norm_num1) with n hn, arith_simps at hn,
  use_only [n], { simp only [a10.symm, hl_range_check_ptr₁, hin_range_check_ptr], arith_simps, exact hn },
  try { split, linarith },
  try { ensures_simps; try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] }, },
  try { dsimp [cast_BigInt3] },
  try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
end

