From iris.algebra Require Import cmra updates.

(** Support of our resource algebra *)

Inductive H := TODO.


(** Resource algebra operations: composition, valid, core *)

Local Instance H_op_instance : Op H :=
  λ x y,
    match x, y with
    | _, _ => TODO
    end.

Local Instance H_valid_instance : Valid H := λ x,
  match x with
  | _ => (* TODO *) False
  end.

Local Instance H_pcore_instance : PCore H := λ _, None.


Section H_proofs.
Context {SI : sidx}.
(* Above line can be removed on older versions of iris if sidx is not found *)


(** Declare the equivalence on [H] as the equality *)

Canonical Structure HO : ofe := leibnizO H.


(** Axioms of resource algebras are satisfied *)

Lemma H_ra_mixin : RAMixin H.
Proof.
  split; try discriminate.
  - solve_proper.
  - solve_proper.
  - intros [] [] []; reflexivity.
  - intros [] []; reflexivity.
  - intros [] [] Hvalid; inversion Hvalid || exact I.
Qed.


(** Declare [H] as an (cm)RA *)

Canonical Structure HR : cmra := discreteR H H_ra_mixin.


(** Required laws *)

(* There exists an instanciation of [h0], [h1], [H] such that all the proofs
below go through, but you are allowed to adapt the proofs to your
definitions. *)

(* [h0] and [h1] can also be constructors of [H], in which case remove the following lines *)

Definition h0 := TODO.
Definition h1 := TODO.


Lemma H_valid_h0 : valid (h0 ⋅ h0).
Proof.
  done.
Qed.

Lemma H_update : h0 ⋅ h0 ~~> h1 ⋅ h1.
Proof.
  intros n []; done.
Qed.

Lemma H_agree : ∀ x y : H, valid (x ⋅ y) → x = y.
Proof.
  intros [] []; compute; tauto.
Qed.

End H_proofs.





(** Usage of [H] in a proof *)


From iris.base_logic.lib Require Import invariants own.
From iris.heap_lang Require Import proofmode notation par assert lib.spin_lock.

Section H_proofs.

(** Our proofs require the functor [Σ] to contain several features *)

(* The heap used in the toy language semantics *)
Context `{!heapGS_gen hlc Σ}.

(* Spawn/join's ghost resources to encode [e1 ||| e2] *)
Context `{spawnG Σ}.

(* The RA used in spinlock *)
Context `{!spin_lockG Σ}.

(* We could use our custom relation algebra: option H * option H *)
Definition oHoHR := prodR (optionR HR) (optionR HR).
Context `{inG Σ oHoHR}.

(* But let us use H with using ghost allocation instead of product + option *)
Context `{inG Σ HR}.

Local Existing Instance spin_lock.

Definition R γ1 γ2 r : iProp Σ :=
  ∃ i j : nat, r ↦ #(i + j) ∗ own γ1 (h i) ∗ own γ2 (h j).


(** Each thread *)

Definition expr_incr (l r : expr) : expr :=
  acquire l;;
  r <- !r + #1;;
  release l.

Lemma expr_incr_correct γl γ1 γ2 γ r l :
  (γ = γ1 \/ γ = γ2) ->
  {{{ is_lock γl l (R γ1 γ2 r) ∗ own γ h0 }}}
    expr_incr l #r
  {{{ RET #(); is_lock γl l (R γ1 γ2 r) ∗ own γ h1 }}}.
Proof.
  (* postcondition-passing style *)
  iIntros (Hγ post) "(#Hlock & Hg) return".

  (* acquiring the lock means acquiring [R] *)
  unfold expr_incr.
  wp_apply (acquire_spec with "Hlock") as "(Hlocked & Hr)".
  (* TODO -- see file [ra_SF.v] for examples of proofs *)
Qed.


(** Proof of full program *)

Definition program : val :=
  λ: <>,
    let: "r" := ref #0 in
    let: "l" := newlock #() in
    (expr_incr "l" "r" ||| expr_incr "l" "r");;
    acquire "l";;
    assert: (!"r" = #2).

Lemma incr2_spec :
  {{{ True }}}
    program #()
  {{{ RET #(); True }}}.
Proof.
  iIntros (post) "_ return".
  wp_lam.
  wp_alloc r as "Hr".
  wp_let.

  (* Before calling [newlock] we allocate our ghost state *)
  iMod (own_alloc (h 0 ⋅ h 0)) as (γ1) "(H1 & H1')". done.
  iMod (own_alloc (h 0 ⋅ h 0)) as (γ2) "(H2 & H2')". done.

  (* Massage the hypotheses to establish the lock invariant [R] *)
  iAssert (R γ1 γ2 r) with "[Hr H1 H2]" as "HR".
  { iExists 0, 0. iFrame. }

  (* Allocate the lock, losing [R] *)
  wp_apply (newlock_spec with "HR") as (lock γl) "#Hlock".
  wp_let.

  (* parallel composition is a call to the [par] function with thunks *)
  wp_pures.

  (* Rule for parallel composition *)
  wp_apply ((
      par_spec
        (λ _, own γ1 (h 1)) (* left postcondition *)
        (λ _, own γ2 (h 1)) (* right postcondition *)
    ) with "[H1'] [H2']") (* what hyps we give each thread *)
    as (? ?) "(Post1 & Post2)". (* postconditions reintroduced after the par *)
  { (* Precondition of left thread *)
    (* TODO *)
  }
  { (* of right thread *)
    (* TODO *)
  }

  (* the postconditions of each threads are now hypotheses *)

  (* TODO *)
Qed.

End H_proofs.