memcpy_spec.lean

import starkware.cairo.lean.semantics.soundness.prelude

namespace starkware.cairo.common.memcpy

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

-- End of automatically generated prelude.

namespace memcpy

@[reducible] def φ_LoopFrame.dst := 0
@[reducible] def φ_LoopFrame.src := 1
@[ext] structure LoopFrame (mem : F → F) :=
  (dst : F) (src : F)
@[reducible] def φ_LoopFrame.SIZE := 2
@[reducible] def LoopFrame.SIZE := 2
@[ext] structure π_LoopFrame (mem : F → F) :=
  (σ_ptr : F) (dst : F) (src : F)
  (h_dst : dst = mem (σ_ptr + φ_LoopFrame.dst))
  (h_src : src = mem (σ_ptr + φ_LoopFrame.src))
@[reducible] def π_LoopFrame.SIZE := 2
@[reducible] def cast_LoopFrame (mem : F → F) (p : F) : LoopFrame mem := {
  dst := mem (p + φ_LoopFrame.dst),
  src := mem (p + φ_LoopFrame.src)
}
@[reducible] def cast_π_LoopFrame (mem : F → F) (p : F) : π_LoopFrame mem := {
  σ_ptr := p,
  dst := mem (p + φ_LoopFrame.dst),
  src := mem (p + φ_LoopFrame.src),
  h_dst := rfl,
  h_src := rfl
}
instance π_LoopFrame_to_F {mem : F → F} : has_coe (π_LoopFrame mem) F := ⟨λ s, s.σ_ptr⟩
@[ext] lemma eq_LoopFrame_ptr {mem : F → F} {x y : π_LoopFrame mem} : x.σ_ptr = y.σ_ptr → x = y :=
begin
  intros h_p, ext,
  exact h_p,
  try { ext }, repeat { rw [x.h_dst, y.h_dst, h_p] },
  try { ext }, repeat { rw [x.h_src, y.h_src, h_p] }
end
lemma eq_LoopFrame_π_cast {mem : F → F} {x y : F} :
  cast_π_LoopFrame mem x = cast_π_LoopFrame mem y ↔ x = y :=
begin
  apply iff.intro, intro h, cases h, refl, intro h, rw [h],
end
lemma eq_LoopFrame_π_ptr_cast {mem : F → F} {x : π_LoopFrame mem} {y : F} :
  x = cast_π_LoopFrame mem y ↔ x.σ_ptr = y :=
begin
  apply iff.intro, intro h, cases h, refl, intro h, ext, rw [←h]
end
lemma coe_LoopFrame_π_cast {mem : F → F} {x : F} :(↑(cast_π_LoopFrame mem x) : F) = x := rfl

end memcpy

-- Holds at beginning and end of the loop.
def memcpy_block4_invariant (mem : F → F) (ap : F) (dst src len : F) : Prop :=
  ∃ n : ℕ,
    mem (ap - 2) = dst + ↑n ∧
    mem (ap - 1) = src + ↑n ∧
    ∀ i < n, mem (dst + i) = mem (src + i)

-- You may change anything in this definition except the name and arguments.
def spec_memcpy_block4 (mem : F → F) (κ : ℕ) (ap dst src len : F) : Prop :=
  memcpy_block4_invariant mem ap dst src len →
    ∃ m : ℕ, len = ↑m ∧ ∀ i < m, mem (dst + i) = mem (src + i)

/- memcpy block 4 autogenerated block specification -/

-- Do not change this definition.
def auto_spec_memcpy_block4 (mem : F → F) (κ : ℕ) (ap dst src len : F) : Prop :=
  ∃ frame : memcpy.LoopFrame mem, frame = memcpy.cast_LoopFrame mem (ap - memcpy.LoopFrame.SIZE) ∧
  mem frame.dst = mem frame.src ∧
  ∃ continue_copying : F,
  ∃ next_frame : memcpy.π_LoopFrame mem, next_frame = memcpy.cast_π_LoopFrame mem (ap + 1 + 1) ∧
  next_frame.dst = frame.dst + 1 ∧
  next_frame.src = frame.src + 1 ∧
  ((continue_copying = 0 ∧
    len = next_frame.src - src ∧
    7 ≤ κ) ∨
   (continue_copying ≠ 0 ∧
    ∃ (κ₁ : ℕ), spec_memcpy_block4 mem κ₁ (ap + 4) dst src len ∧
    κ₁ + 5 ≤ κ))

/- memcpy block 4 soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_memcpy_block4
    {mem : F → F}
    (κ : ℕ)
    (ap dst src len : F)
    (h_auto : auto_spec_memcpy_block4 mem κ ap dst src len) :
  spec_memcpy_block4 mem κ ap dst src len :=
begin
  intro h,
  rcases h with ⟨n, h_dst, h_src, h_all⟩,
  rcases h_auto with ⟨frame, h_frame, h_dst_eq_src, cc, next_frame, h_next_frame, h_next_dst, h_next_src, h_next⟩,
  simp [memcpy.cast_LoopFrame, memcpy.LoopFrame.ext_iff, sub_add_eq_add_neg_add] at h_frame,
  norm_num1 at h_frame, simp only [←sub_eq_add_neg] at h_frame,
  have h_inv : ∀ i < n + 1, mem (dst + ↑i) = mem (src + ↑i),
  { intros i ilt,
    rcases (lt_or_eq_of_le (nat.le_of_lt_succ ilt)) with ilt | rfl,
    { apply h_all i ilt },
    rw [←h_dst, ←h_src, ←h_frame.1, ←h_frame.2, h_dst_eq_src] },
  rcases h_next with ⟨ccz, h_len_eq⟩ | ⟨ccnz, _, h_loop⟩,
  { use n + 1, split,
    { rw [h_len_eq.1, h_next_src], rw [h_frame.2, h_src, nat.cast_add, nat.cast_one],
      abel },
    exact h_inv },
  apply h_loop.1,
  simp [memcpy.cast_π_LoopFrame, memcpy.π_LoopFrame.ext_iff, add_assoc] at h_next_frame,
  norm_num1 at h_next_frame,
  use n + 1,
  simp only [add_sub_assoc, nat.cast_add, nat.cast_one], norm_num1,
  rw [←h_next_frame.2.1, ←h_next_frame.2.2, h_next_dst, h_next_src, h_frame.1, h_frame.2,
        h_dst, h_src],
  split, { abel },
  split, { abel },
  exact h_inv
end

/-
-- Function: memcpy
-/

/- memcpy autogenerated specification -/

-- Do not change this definition.
def auto_spec_memcpy (mem : F → F) (κ : ℕ) (dst src len : F) : Prop :=
  ((len = 0 ∧
    2 ≤ κ) ∨
   (len ≠ 0 ∧
    ∃ frame : memcpy.LoopFrame mem, frame = {
      dst := dst,
      src := src
    } ∧
    ∃ (ap : F),
    frame = memcpy.cast_LoopFrame mem (ap - 2) ∧
    ∃ (κ₁ : ℕ), auto_spec_memcpy_block4 mem κ₁ ap dst src len ∧
    κ₁ + 3 ≤ κ))

-- You may change anything in this definition except the name and arguments.
def spec_memcpy (mem : F → F) (κ : ℕ) (dst src len : F) : Prop :=
  ∃ n : ℕ, len = ↑n ∧ ∀ i < n, mem (dst + i) = mem (src + i)

/- memcpy soundness theorem -/

-- Do not change the statement of this theorem. You may change the proof.
theorem sound_memcpy
    {mem : F → F}
    (κ : ℕ)
    (dst src len : F)
    (h_auto : auto_spec_memcpy mem κ dst src len) :
  spec_memcpy mem κ dst src len :=
begin
  rcases h_auto with ⟨h_len, _⟩ | ⟨h_len, frame, h_frame, ap, h_frame', _, h_block4⟩,
  { use 0, simp [h_len] },
  apply (sound_memcpy_block4 _ _ _ _ _ h_block4.1),
  use 0, simp,
  simp [h_frame, memcpy.cast_LoopFrame, memcpy.π_LoopFrame.ext_iff] at h_frame',
  simp [h_frame', sub_eq_add_neg, add_assoc], norm_num
end


end starkware.cairo.common.memcpy