提交 #10

import Auto

import Loom.MonadAlgebras.NonDetT.Extract
import Loom.MonadAlgebras.WP.Tactic
import Loom.MonadAlgebras.WP.DoNames'

import CaseStudies.Velvet.Std
import CaseStudies.TestingUtil

open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames

@[reducible]
def addr := ℤ

@[reducible]
def path (h : addr → addr) (x : addr) (l : List addr) (y : addr) :=
  match l with
  | [] => x = y
  | a :: t => a ≠ 0 ∧ x = a ∧ path h (h a) t y

@[reducible]
def distinct (l : List addr) :=
  match l with
  | [] => ⊤
  | a :: t => (∀ x, x ∈ t → x ≠ a) ∧ distinct t

@[reducible]
def distPath (h : addr → addr) (x : addr) (l : List addr) (y : addr) :=
  path h x l y ∧ distinct l

theorem distinct_sublist (l1 l2 : List addr) :
  distinct (l1 ++ l2) → distinct l1
:= by
  intro h
  induction l1 with
  | nil => simp [distinct]
  | cons a t ih =>
    simp [distinct] at *
    have ⟨ h1, h2 ⟩ := h
    constructor
    . intro x hx
      apply h1
      left
      exact hx
    . apply ih
      exact h2

theorem distPath_null (h : addr → addr) (x : addr) (Ps Qs : List addr) :
  distPath h x Ps 0 → distPath h x Qs 0 → Ps = Qs
:= by
  intro hP hQ
  induction Ps generalizing x Qs with
  | nil =>
    simp [distPath, path] at hP
    cases Qs with
    | nil => rfl
    | cons b Qs' =>
      simp [distPath, path] at hQ
      rw [hP] at hQ
      rcases hQ with ⟨⟨hb_ne, hb_eq, _⟩, _⟩
      rw [←hb_eq] at hb_ne
      contradiction
  | cons a Ps' ih =>
    cases Qs with
    | nil =>
      simp [distPath, path] at hP hQ
      rw [hQ] at hP
      rcases hP with ⟨⟨ha_ne, ha_eq, _⟩, _⟩
      rw [←ha_eq] at ha_ne
      contradiction
    | cons b Qs' =>
      simp [distPath, path] at hP hQ
      rcases hP with ⟨⟨ha_ne, hxa, hP_path⟩, hP_dist⟩
      rcases hQ with ⟨⟨hb_ne, hxb, hQ_path⟩, hQ_dist⟩
      have : a = b := by rw [←hxa, ←hxb]
      subst b
      congr
      apply ih (h a)
      . exact ⟨ hP_path, hP_dist.2 ⟩
      . rw [hxa] at hQ_path
        exact ⟨ hQ_path, hQ_dist.2 ⟩

theorem distPath_sublist_aux1 (h : addr → addr) (x : addr) (Ps Qs : List addr) (y : addr) :
  y ≠ 0 → distPath h x Qs y → distPath h x Ps 0 →
  distinct Ps
:= by
  intros p q r
  simp [distPath] at r
  let ⟨ _, r2 ⟩ := r
  exact r2

theorem distPath_sublist_aux2 (h : addr → addr) (x : addr) (Ps Qs : List addr) (y : addr) :
  y ≠ 0 → distPath h x Qs y → distPath h x Ps 0 →
  ∃ Q, Ps = Qs ++ [y] ++ Q
:= by
  intro hy hQs hPs
  induction Qs generalizing x Ps with
  | nil =>
    simp [distPath, path] at hQs
    rw [hQs] at hPs
    cases Ps with
    | nil =>
      simp [distPath, path] at hPs
      contradiction
    | cons p Ps' =>
      simp [distPath, path] at hPs
      rcases hPs with ⟨ ⟨ hp_ne, hp_eq, hPs_path ⟩, hPs_dist ⟩
      exists Ps'
      simp
      exact hp_eq.symm
  | cons a Qs' ih =>
    simp [distPath, path] at hQs
    rcases hQs with ⟨ ⟨ ha_ne, ha_eq, hQs_path ⟩, hQs_dist ⟩
    subst a
    cases Ps with
    | nil =>
      simp [distPath, path] at hPs
      rw [hPs] at ha_ne
      contradiction
    | cons p Ps' =>
      simp [distPath, path] at hPs
      rcases hPs with ⟨ ⟨ hp_ne, hp_eq, hPs_path ⟩, hPs_dist ⟩
      subst p
      have hQs_sub : distPath h (h x) Qs' y := by
        simp [distPath]
        exact ⟨ hQs_path, hQs_dist.2 ⟩
      have hPs_sub : distPath h (h x) Ps' 0 := by
        simp [distPath]
        exact ⟨ hPs_path, hPs_dist.2 ⟩
      have ⟨ Q, hQ ⟩ := ih (h x) Ps' hQs_sub hPs_sub
      exists Q
      simp [hQ]

theorem distPath_sublist (h : addr → addr) (x : addr) (Ps Qs : List addr) (y : addr) :
  y ≠ 0 → distPath h x Qs y → distPath h x Ps 0 →
  (∃ Q, Ps = Qs ++ [y] ++ Q) ∧ distinct Ps
:= by
  intros p q r
  split_ands
  . apply distPath_sublist_aux2 <;> trivial
  . apply distPath_sublist_aux1 <;> trivial

theorem distPath_hd (h : addr → addr) (x y : addr) (Ps : List addr) :
  x ≠ y → distPath h x Ps y → ∃ Qs, Ps = x :: Qs
:= by
  intros hNeq hPs
  cases Ps with
  | nil =>
    simp [distPath, path] at hPs
    contradiction
  | cons a t =>
    simp [distPath, path] at hPs
    exists t
    grind

theorem distPath_tl (h : addr → addr) (x : addr) (Ps : List addr) :
  x ≠ 0 → distPath h x (x :: Ps) 0 → distPath h (h x) Ps 0
:= by
  intros
  simp_all [distPath, path, distinct]

theorem distPath_next (h : addr → addr) (x : addr) (Qs : List addr) (y : addr) :
  y ≠ 0 → distPath h x Qs y → distinct (Qs ++ [y]) → distPath h x (Qs ++ [y]) (h y)
:= by
  intro hy hQs hDist
  induction Qs generalizing x with
  | nil =>
    simp [distPath, path, distinct] at hQs
    simp [distPath, path, distinct]
    exact ⟨ hy, hQs ⟩
  | cons a Qs' ih =>
    simp [distPath, path, distinct] at hQs hDist ⊢
    rcases hQs with ⟨ ⟨ ha_ne, hxa, hPath' ⟩, hDistQs ⟩
    constructor
    . constructor
      . exact ha_ne
      . constructor
        . exact hxa
        . have hSub : distPath h (h a) Qs' y := ⟨ hPath', hDistQs.2 ⟩
          have hDistSub : distinct (Qs' ++ [y]) := hDist.2
          have hRes := ih (h a) hSub hDistSub
          exact hRes.1
    . exact hDist

theorem distPath_cycle (h : addr → addr) (x : addr) (Ls Ps : List addr) :
  x ≠ 0 → distPath h x Ls 0 → distPath h x Ps x → Ps = []
:= by
  intros hNe hLs hPs
  have h1 := distPath_sublist _ _ _ _ _ hNe hPs hLs
  cases Ls with
  | nil =>
    simp [distPath, path] at hLs
    contradiction
  | cons a t =>
    simp [distPath, path] at hLs
    have ⟨ ⟨ h2, h3, h4 ⟩, h5 ⟩ := hLs
    simp [h3] at *
    have ⟨ ⟨ q, h6 ⟩, d ⟩ := h1
    (
      cases Ps with
      | nil => rfl
      | cons a2 h2 =>
        simp_all
        grind
    )

theorem distPath_eq (h : addr → addr) (x : addr) (Ls Ps Qs : List addr) (y : addr) :
  distPath h x Ls 0 → distPath h x Ps y → distPath h x Qs y → Ps = Qs
:= by
  intros hLs hPs hQs
  induction Ls generalizing Qs Ps x y with
  | nil =>
    simp [distPath, path] at hLs
    simp [hLs] at *
    cases Ps with
    | nil => (
      cases Qs with
      | nil => rfl
      | cons a2 t2 =>
        simp [distPath, path] at hQs
        grind
      )
    | cons a1 t1 =>
      simp [distPath, path] at hPs
      grind
  | cons a t ih =>
    have hLs' := hLs
    simp [distPath, path] at hLs
    have ⟨ ⟨ h1, h2, h3 ⟩, h4 ⟩ := hLs
    rw [←h2] at h1
    if e : x = y then
      simp [e] at *
      have h5 := distPath_cycle _ _ _ _ h1 hLs' hPs
      have h6 := distPath_cycle _ _ _ _ h1 hLs' hQs
      simp [h5, h6]
    else
      have ⟨ q1, h5 ⟩ := distPath_hd _ _ _ _ e hPs
      have ⟨ q2, h6 ⟩ := distPath_hd _ _ _ _ e hQs
      simp [h5, h6]
      have h7 : distPath h (h x) t 0 := (by
        constructor <;> grind
      )
      rw [h5] at hPs
      rw [h6] at hQs
      simp [distPath, path] at hPs
      simp [distPath, path] at hQs
      simp_all
      have ⟨ h8, h9 ⟩ := hPs
      have ⟨ h10, h11 ⟩ := hQs
      simp [distPath] at h7
      have ⟨ h12, h13 ⟩ := h7
      simp [distinct] at h9
      simp [distinct] at h11
      have h14 := ih _ _ _ _ h12 h8 h9.right h10 h11.right
      exact h14

theorem distPath_next2 (h : addr → addr) (x : addr) (Ls Ps Qs : List addr) (y : addr) :
  y ≠ 0 → distPath h x Ls 0 → distPath h x Ps y → distPath h x Qs (h y) → Qs = Ps ++ [y]
:= by
  intros hNe hLs hPs hQs
  have ⟨ ⟨ a, h01 ⟩, h02 ⟩ := distPath_sublist _ _ _ _ _ hNe hPs hLs
  rw [h01] at h02
  have h1 := distinct_sublist _ _ h02
  have h2 := distPath_next _ _ _ _  hNe hPs h1
  have h3 := distPath_eq _ _ _ _ _ _ hLs hQs h2
  exact h3

theorem path_irrelevant (h : addr → addr) (y x z : addr) (Q : List addr) :
  distinct (y :: Q) → path h x Q 0 → path (Function.update h y z) x Q 0
:= by
  intros hd hp
  induction Q generalizing x with
  | nil =>
    grind
  | cons a t ih =>
    specialize ih (h x)
    simp [path] at hp
    simp_all
    constructor
    . grind
    . constructor
      . rfl
      . simp [distinct] at hd
        simp_all

theorem distPath_cons (h : addr → addr) (x : addr) (Q : List addr) :
  x ≠ 0 → distinct (x :: Q) → distPath h (h x) Q 0 → distPath h x (x :: Q) 0
:= by
  grind

theorem del_one (h : addr → addr) (x y ya : addr) (P Q : List addr) :
  distPath h x (P ++ [y] ++ [ya] ++ Q) 0 → distPath (Function.update h y (h ya)) x (P ++ [y] ++ Q) 0
:= by
  intros hP
  induction P generalizing x with
  | nil =>
    simp [distPath, path] at hP
    simp_all
    constructor
    . constructor
      . grind
      . constructor
        . rfl
        . simp
          apply path_irrelevant <;> grind
    . grind
  | cons a t ih =>
    specialize ih (h x)
    unfold distPath at hP
    have ⟨ h1, h2 ⟩ := hP
    simp_all
    apply distPath_cons
    . grind
    . grind
    . have e : a ≠ y := by grind
      simp_all
      exact ih

method mem_alloc
  (saddr : addr → addr) (block_size : addr → ℕ) (mut next : addr → addr)
  (mut free_list : addr) (size : ℕ)
  (Ps : List addr)
return (mem : addr)
  require distPath next free_list Ps 0
  ensures ∀ b, List.find? (fun x => block_size x ≥ size) Ps = some b →
          mem = b ∧ distPath next free_list (List.erase Ps b) 0
do
  if free_list = 0 then
    return 0
  else
    if block_size free_list ≥ size then
      let res := free_list
      free_list := next free_list
      return res
    else
      let mut q := free_list
      let mut p := next free_list
      while p ≠ 0 ∧ block_size p < size
      invariant distPath next free_list Ps 0
      invariant ∃ Qs, distPath next free_list Qs p ∧ ∀ a, a ∈ Qs → block_size a < size
      invariant p = next q
      invariant ∃ Qs, distPath next free_list Qs q
      invariant q ≠ 0
      do
        q := p
        p := next p
      if p ≠ 0 then
        next := Function.update next q (next p)
        return p
      else
        return 0

prove_correct mem_alloc by
  loom_solve
  . intros b h
    cases Ps <;> simp_all
  . intros b h
    cases Ps <;> simp_all
    apply distPath_tl <;> grind
  . let ⟨ Qs, ⟨ ih1, ih2 ⟩ ⟩ := invariant_2
    exists (Qs ++ [p])
    simp_all
    apply And.intro
    . apply distPath_next <;> try grind
      let ⟨ ⟨ Q, h1 ⟩, h2 ⟩ := distPath_sublist nextOld free_listOld Ps Qs (nextOld q) a_4 ih1 (And.intro a_2 a_3)
      rw [h1] at h2
      apply (distinct_sublist (Qs ++ [nextOld q]) Q)
      exact h2
    . grind
  . exists [free_listOld]
    simp_all
    apply And.intro
    . grind
    . simp [distinct]
  . exists []
  . intros b h
    simp_all
    let ⟨ i11, i12 ⟩ := i_1
    let ⟨ Qs, ⟨ h1, h2 ⟩ ⟩ := invariant_2
    simp_all
    have ⟨ ⟨ Q, t1 ⟩, t2 ⟩ := distPath_sublist nextOld free_listOld Ps Qs i if_pos h1 (And.intro a_2 a_3)
    apply And.intro
    . grind
    . have tmp : i = b := by grind
      rw [tmp] at t1
      have tmp2 : Ps.erase b = Qs ++ Q := by grind
      rw [tmp2]
      let ⟨ L, t3 ⟩ := invariant_4
      rewrite [<- i_1] at h1
      have eq := distPath_next2 nextOld free_listOld Ps L Qs q_1 invariant_5 (And.intro a_2 a_3) t3 h1
      rw [eq]
      apply del_one
      grind
  . intros b h
    simp_all
    let ⟨ Qs, ⟨ ih1, ih2 ⟩ ⟩ := invariant_2
    apply distPath_null nextOld free_listOld Ps at ih1 <;> grind