From iris.heap_lang Require Import proofmode notation.


(** In class, linked lists where represented by a null location for the empty
list, and a non-null location p such that p+0 points to the head of the list and
p+1 points to the tail of the list. In this file we try to stick to this
convention by assuming a null location, but this is not idiomatic in iris's toy
language Heaplang *)

Definition null : loc := Loc 0.


(** Syntax of [mlength] program *)

Definition mlength : val :=
  rec: "mlength" "p" :=
    if: "p" = #null then
      #0
    else
      let: "n'" := "mlength" !("p" +ₗ #1) in
      #1 + "n'".



(** Incantation asking Iris for the heap mapsto assertions *)
Section mlist_examples. Context `{!heapGS Σ}.


(** null is not special, so we wouldn't be able to prove p ⟼ v -∗ ⌜p ≠ null⌝.
Below, we bake it into the [Mlist] predicate instead of adding an axiom such as:

[Axiom mapsto_not_null : ∀ p v, p ↦ v ⊢ ⌜p ≠ null⌝.]

When allocating, we might get the null pointer, in which case we can just
allocate again to get another pointer, which must be not null this time *)

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.


(** Proof of [mlength] function *)

Lemma mlength_spec L (p : loc) :
  {{{ Mlist L p }}}
    mlength #p
  {{{ RET #(length L); Mlist L p }}}.
Proof.
  (* Iris's postcondition-passing style, we ignore [Φ] and [Hreturn] for now. *)
  (* [Hp] is the name of the important spatial hypothesis *)
  iIntros (Φ) "Hp Hreturn".

  (* We proceed by induction on [L], but we generalize on [p] by adding [∀ (p)] *)
  iInduction L as [ | x L' ] "IH" forall (p Φ).
  - (* rule [fix] in iris's heaplang is implemented by [wp_rec] *)
    wp_rec.

    (* [Mlist [] p] means that p is null, we can use it as a normal Rocq hypothesis *)
    simpl Mlist.
    iDestruct "Hp" as %Hp.

    (* pure deterministic reduction *)
    wp_pure.

    (* rule for if *)
    case_bool_decide as Hif; wp_if.
    (* the case for false is a contradiction *)
    2: congruence.

    (* case for true *)

    (* we need to return [length []] which is 0 *)
    iApply "Hreturn".
    iPureIntro.
    auto.

  - (* Inductive case: [L = x :: L'] *)

    (* unfolding Mlist *)
    simpl (Mlist (x :: L') p) at 1.

    (* Destruct the existential: rule EXISTS, introduces a Rocq variable *)
    iDestruct "Hp" as (p') "Hp".
    (* Destruct the hypothesis: rule PROP, introduces a Rocq hypothesis *)
    iDestruct "Hp" as (Hp) "Hp".
    (* Destruct the separating conjunction by naming each component *)
    iDestruct "Hp" as "(Hp0 & Hp1 & Hp')".

    (* Rule for fix *)
    wp_rec.
    (* Bind rule: same as using the A-normal form + using the rule for let *)
    wp_bind (#p = #null)%E. wp_pure.

    (* rule for if *)
    case_bool_decide as Hif; wp_if. congruence.

    (* rule for load *)
    wp_load.
    
    (* Induction hypothesis + frame *)
    (* Hp' is passed to IH, the rest is framed *)
    (* Hp'_post is the name we give to the postcondition *)
    wp_apply ("IH" with "Hp'") as "Hp'_post".

    (* again, applying rules for pure reductions: *)
    wp_pures.

    (* ignore this *)
    iModIntro.

    (* massaging goal to match the expected return value *)
    replace (1 + length L')%Z with (S (length L') : Z) by lia.
    iApply "Hreturn".

    (* reconstructing [Mlist (x :: L') p] *)
    simpl Mlist.
    iExists p'.

    (* applying the frame rule several times *)
    iFrame "Hp0".
    iFrame "Hp1".
    iFrame "Hp'_post".
    iPureIntro.
    auto.
Qed.

(** Proof of list_incr *)

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

Lemma list_incr_spec L (p : loc) :
  {{{ Mlist L p }}}
    list_incr #p
  {{{ RET #(); Mlist (map (Z.add 1) L) p }}}.
Proof.
  iIntros (Φ) "Hp Hreturn".
  iInduction L as [ | x L' ] "IH" forall (p Φ).
  - wp_rec.
    simpl.
    iDestruct "Hp" as %->.
    wp_pure.
    wp_if.
    iModIntro.
    iApply "Hreturn".
    iPureIntro.
    reflexivity.
  - simpl.
    iDestruct "Hp" as (p') "(% & Hp0 & Hp1 & Hp')".
    wp_rec.
    wp_pure.
    rewrite bool_decide_eq_false_2.
    2: now injection 1 as ->.
    wp_if.
    wp_load.
    wp_pure.
    wp_store.
    wp_load.
    wp_apply ("IH" with "Hp'") as "Hp'_post".
    iApply "Hreturn".
    iExists p'.
    iFrame. auto.
Qed.

End mlist_examples.