From iris.algebra Require Import cmra updates.

(** Support of our resource algebra *)

Inductive SF := TODO.


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

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

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

Local Instance SF_pcore_instance : PCore SF := λ _, None.


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


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

Canonical Structure SFO : ofe := leibnizO SF.


(** Axioms of resource algebras are satisfied *)

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


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

Canonical Structure SFR : cmra := discreteR SF SF_ra_mixin.


(* Without this [valid _] is not known to be pure
-- not sure why it is needed since [halfR] *)
Global Instance SF_cmra_discrete : CmraDiscrete SFR :=
  discrete_cmra_discrete _ _.


(** Required laws *)

(* There exists an instantiation of [S], [S], [SF] such that all the proofs
below go through, but you are allowed to adapt the proofs to your
definitions. *)

(* [S] and [F] can also be constructors of [SF], in which case remove the following lines *)

Definition S := TODO.
Definition F := TODO.

Lemma SF_valid_S : valid S.
Proof.
  done.
Qed.

Lemma SF_invalid_SF : ¬ valid (S ⋅ F).
Proof.
  tauto.
Qed.

Lemma SF_F_F: F ⋅ F = F.
Proof.
  done.
Qed.

Lemma SF_update : S ~~> F.
Proof.
  intros n []; done.
Qed.

End SF_proofs.




(** USAGE 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 SF_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 Σ}.

(* Finally, our SF relation algebra *)
Context `{inG Σ SFR}.

Local Existing Instance spin_lock.


(** Our lock invariant is an iris proposition *)

Definition R γ r : iProp Σ := r ↦ #0 ∗ own γ S  ∨  r ↦ #1 ∗ own γ F.


(** Left thread *)

Definition left_thread (l r : expr) : expr :=
  acquire l;;
  r <- !r;;
  release l.

Lemma left_thread_correct γl γ r l :
  {{{ is_lock γl l (R γ r) }}}
    left_thread l #r
  {{{ RET #(); is_lock γl l (R γ r) }}}.
Proof.
  (* postcondition-passing style *)
  iIntros (post) "#Hlock return".

  (* acquiring the lock means acquiring [R] *)
  unfold left_thread.
  wp_apply (acquire_spec with "Hlock") as "(Hlocked & Hr)".
  wp_pures.

  (* to perform the load and store we need to expose [r ↦ _] *)
  iDestruct "Hr" as "[(Hr & HS) | (Hr & HF)]".
  - wp_load.
    wp_store.
    wp_apply (release_spec with "[Hr HS $Hlocked $Hlock]") as "Hr".
    { iLeft; iFrame. }
    by iApply "return".
  - wp_load.
    wp_store.
    wp_apply (release_spec with "[Hr HF $Hlocked $Hlock]") as "Hr".
    { iRight; iFrame. }
    by iApply "return".
Qed.


(** Right thread *)

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

Lemma right_thread_correct γl γ r l :
  {{{ is_lock γl l (R γ r) }}}
    right_thread l #r
  {{{ RET #(); is_lock γl l (R γ r) ∗ own γ F }}}.
Proof.
  iIntros (post) "#Hlock return".

  unfold right_thread.
  wp_apply (acquire_spec with "Hlock") as "(Hlocked & Hr)".
  wp_pures.

  iDestruct "Hr" as "[(Hr & HS) | (Hr & HF)]".
  - wp_store.
    iMod (own_update _ _ F with "HS") as "HF". exact SF_update.
    rewrite -{2}SF_F_F.
    iDestruct "HF" as "(HF1 & HF2)".
    wp_apply (release_spec with "[Hr HF1 $Hlocked $Hlock]") as "Hr".
    { iRight; iFrame. }
    by iApply "return"; iFrame.
  - wp_store.
    rewrite -{2}SF_F_F.
    iDestruct "HF" as "(HF1 & HF2)".
    wp_apply (release_spec with "[Hr HF1 $Hlocked $Hlock]") as "Hr".
    { iRight; iFrame. }
    by iApply "return"; iFrame.
Qed.


(** Proof of full program *)

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

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 S) as (γ) "Hg". done.

  (* Massage the hypotheses to establish the lock invariant [R] *)
  iAssert (R γ r) with "[Hr Hg]" as "HR".
  { iLeft. 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
        (λ _, ⌜True⌝%I) (* left postcondition *)
        (λ _, own γ F) (* right postcondition *)
    ) with "[] []")
    as (? ?) "(Post_thread_1 & Post_thread_2)". (* postconditions reintroduced after the par *)
  { (* Precondition of left thread *)
    wp_pure.
    iApply (left_thread_correct with "[$Hlock]").
    auto. }
  { (* of right thread *)
    wp_pure.
    iApply (right_thread_correct with "[$Hlock]").
    iNext.
    iIntros "(#Hlock' & HF)". iApply "HF".
  }

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

  (* Acquire the lock again *)
  iNext.
  wp_pures.
  wp_apply (acquire_spec with "Hlock") as "(Hlocked & Hr)".

  (* We reach the assert *)
  wp_pures.
  wp_apply wp_assert.
  (* precondition of assert: the expression evaluates to true *)

  (* We extract [r↦x+y] from the lock invariant to perform the load  *)
  iDestruct "Hr" as "[(Hr & HS) | (Hr & HF)]".
  - wp_load.

    (* Ghost manipulation to get [S ⋅ F] (invalid) *)
    iCombine "Post_thread_2" "HS" as "Hg" gives %Hvalid.
    compute in Hvalid.
    tauto.
  - wp_load.
    wp_pures.
    iModIntro. iSplit; auto.
    by iApply "return".
Qed.

End SF_proofs.