From iris.heap_lang Require Import proofmode notation.

Section examples. Context `{!heapGS Σ}.

(** [null] specificities *)
Definition null : loc := Loc 0.

(* [malloc] is just like normal allocation but returns a non-null location *)
Definition malloc : val :=
  λ: "n" "v",
    if: #0 < "n" then
      let: "l" := AllocN "n" "v" in
      if: "l" = #null then AllocN "n" "v" else "l"
    else #(Loc 91).

Lemma malloc_spec (n : Z) (v : val):
  {{{ True }}}
    malloc #n v
  {{{ (l : loc), RET #l; l ↦∗ replicate (Z.to_nat n) v ∗ ⌜l ≠ null⌝ }}}.
Proof.
  iIntros (Φ) "_ ret". wp_lam. wp_pures.
  case_bool_decide.
  - wp_alloc l as "Hl". lia. wp_pures.
    destruct (decide (l = null)) as [-> | nl].
    + wp_if. wp_alloc l' as "Hl'". lia. iApply "ret".
      assert (Z.to_nat n = S (Z.to_nat (n - 1))) as -> by lia.
      rewrite /= !array_cons.
      iModIntro; iSplit; iFrame.
      iDestruct "Hl" as "(? & _)".
      iDestruct "Hl'" as "(? & _)".
      iApply (pointsto_ne with "[$] [$]").
    + rewrite bool_decide_eq_false_2. 2: congruence.
      wp_if. iApply "ret"; auto.
  - wp_if. iApply "ret".
    assert (Z.to_nat n = 0) as -> by lia. rewrite /array /=. auto.
Qed.


(** [Mlist] related to [listof] *)

Fixpoint Mlist (L : list Z) (p : loc) : iProp Σ :=
  match L with
  | nil => ⌜ p = null ⌝
  | x :: L' => ∃ p' : loc, ⌜ p ≠ null ⌝ ∗ p ↦ #x ∗ (p +ₗ 1) ↦ #p' ∗ Mlist L' p'
  end%I.

Fixpoint listof {A} (R : A → val → iProp Σ) (L : list A) (p : loc) : iProp Σ :=
  match L with
  | nil => ⌜ p = null ⌝
  | X :: L' => ∃ p' : loc, ⌜ p ≠ null ⌝ ∗ (∃ x, p ↦ x ∗ R X x) ∗ (p +ₗ 1) ↦ #p' ∗ listof R L' p'
  end%I.

Definition isz (z : Z) : val → iProp Σ := λ v, ⌜v = #z⌝%I.

Lemma Mlistof_listof_Z p L : Mlist L p ⊣⊢ listof isz L p.
Proof.
  induction L as [ | z L ] in p |- *. auto.
  simpl.
  iSplit; iIntros "(%p' & ? & A & ?)"; iExists p';
    rewrite IHL; iFrame; auto.
  iDestruct "A" as "(% & ? & ->)"; auto.
Qed.


(** New list cell, first-order spec *)

Definition cons : val :=
  λ: "v1" "v2",
    let: "p" := malloc #2 #() in
    "p" <- "v1";;
    "p" +ₗ #1 <- "v2";;
    "p".

Lemma cons_correct v1 v2 :
  {{{ True }}} cons v1 v2 {{{ (l : loc), RET #l; ⌜l ≠ null⌝ ∗ l ↦ v1 ∗ (l +ₗ 1) ↦ v2 }}}.
Proof.
  iIntros (φ) "_ ret". wp_lam; wp_pures.
  wp_apply (malloc_spec 2 with "[]") as (l) "(Hl & %)". iPureIntro. lia.
  rewrite !array_cons. iDestruct "Hl" as "(Hl0 & Hl1 & _)".
  wp_store. wp_store. iApply "ret". iFrame. auto.
Qed.


Section about_listof.

Context {A} (R : A → val → iProp Σ).

Lemma cons_listof p' x X L :
  {{{ R X x ∗ listof R L p' }}}
    cons x #p'
  {{{ (p : loc), RET #p; listof R (X :: L) p }}}.
Proof.
  iIntros (φ) "(Hx & Hp') ret".
  wp_apply (cons_correct with "[$]") as (l) "(% & Hl & Hl1)".
  iApply "ret". simpl. iExists p'. iFrame. auto.
Qed.

Definition uncons : val :=
  λ: "p",
    (!"p", !("p" +ₗ #1)).

Lemma uncons_listof p X L :
  {{{ listof R (X :: L) p }}}
    uncons #p
  {{{ (x : val) (p' : loc), RET (x, #p'); R X x ∗ listof R L p' }}}.
Proof.
  iIntros (φ) "Hp ret". simpl.
  iDestruct "Hp" as (p' Hp) "((%x & Hp & Hx) & Hp1 & Hp')".
  wp_lam. wp_load. wp_load. wp_pures. iApply "ret". iFrame. auto.
Qed.

Lemma head_listof p X L :
  {{{ listof R (X :: L) p }}}
    !#p
  {{{ (x : val), RET x; R X x ∗ ∀ Y, R Y x -∗ listof R (Y :: L) p }}}.
Proof.
  iIntros (φ) "Hp ret". simpl listof at 1.
  iDestruct "Hp" as (p' Hp) "((%x & Hp & Hx) & Hp1 & Hp')".
  wp_load. iApply "ret". iFrame. iModIntro.
  iIntros "%Y Hy". simpl. iExists p'. iFrame. auto.
Qed.


Definition miter : val :=
  rec: "miter" "f" "p" :=
    if: "p" = #null then
      #()
    else
      "f" !"p";;
      "miter" "f" !("p" +ₗ #1).

Definition iter_spec_1 (it : val) := ∀ (f : val) l (I : list A → iProp Σ),
  (∀ X x s, {{{ I (X :: s) ∗ R X x }}} f x {{{ RET #(); I s ∗ R X x }}}) →
  ∀ p, {{{ listof R l p ∗ I l }}} it f #p {{{ RET #(); listof R l p ∗ I [] }}}.

Lemma miter_correct_1 : iter_spec_1 miter.
Proof.
  iIntros (f l I Hf p φ) "(Hp & i) ret".
  iInduction l as [ | X l ] "IH" forall (p).
  - iDestruct "Hp" as %->. wp_rec. wp_pures. iApply "ret". auto.
  - simpl listof at 3. iDestruct "Hp" as "(%p' & %Hp' & (%x & Hp & Hx) & Hp1 & Hp')".
    wp_rec. wp_pures. case_bool_decide. congruence. wp_pures. wp_load.
    wp_apply (Hf with "[$i $Hx]") as "(i & Hx)". wp_pures. wp_load.
    wp_apply ("IH" with "Hp' i") as "(Hp' & i)". iApply "ret". by iFrame.
Qed.

Definition iter_spec_2 (it : val) := ∀ (f : val) l (J : list A → list A → iProp Σ),
  (∀ X x k s, {{{ J (X :: s) k ∗ R X x }}} f x {{{ Y, RET #(); J s (k ++ [Y]) ∗ R Y x }}}) →
  ∀ p, {{{ listof R l p ∗ J l [] }}} it f #p {{{ l', RET #(); listof R l' p ∗ J [] l' }}}.

Lemma miter_correct_2 : iter_spec_2 miter.
Proof.
  (* Generalize slightly for the induction *)
  cut (∀ (f : val) l (J : list A → list A → iProp Σ),
          (∀ X x k s, {{{ J (X :: s) k ∗ R X x }}} f x {{{ Y, RET #(); J s (k ++ [Y]) ∗ R Y x }}}) →
          ∀ nnil p, {{{ listof R l p ∗ J l nnil }}} miter f #p {{{ l', RET #(); listof R l' p ∗ J [] (nnil ++ l') }}}).
  { intros H f l J Hf; apply (H f l J Hf nil). }
  iIntros (f l J Hf nnil p φ) "(Hp & j) ret".
  iInduction l as [ | X l ] "IH" forall (p nnil).
  - iDestruct "Hp" as %->. wp_rec. wp_pures. iApply ("ret" $! []). rewrite app_nil_r. auto.
  - simpl listof at 3. iDestruct "Hp" as "(%p' & %Hp' & (%x & Hp & Hx) & Hp1 & Hp')".
    wp_rec. wp_pures. case_bool_decide. congruence. wp_pures. wp_load.
    wp_apply (Hf with "[$j $Hx]") as (Y) "(j & Hx)". wp_pures. wp_load.
    wp_apply ("IH" with "[$Hp'] [$j]") as (l') "(Hp' & j)". iApply "ret".
    rewrite -app_assoc. by iFrame.
Qed.

End about_listof.

End examples.