Commit 1f589858 authored by Robbert Krebbers's avatar Robbert Krebbers

Iris 3.0: invariants and weakest preconditions encoded in the logic.

This commit features:

- A simpler model. The recursive domain equation no longer involves a triple
  containing invariants, physical state and ghost state, but just ghost state.
  Invariants and physical state are encoded using (higher-order) ghost state.

- (Primitive) view shifts are formalized in the logic and all properties about
  it are proven in the logic instead of the model. Instead, the core logic
  features only a notion of raw view shifts which internalizing performing frame
  preserving updates.

- A better behaved notion of mask changing view shifts. In particular, we no
  longer have side-conditions on transitivity of view shifts, and we have a
  rule for introduction of mask changing view shifts |={E1,E2}=> P with
  E2 ⊆ E1 which allows to postpone performing a view shift.

- The weakest precondition connective is formalized in the logic using Banach's
  fixpoint. All properties about the connective are proven in the logic instead
  of directly in the model.

- Adequacy is proven in the logic and uses a primitive form of adequacy for
  uPred that only involves raw views shifts and laters.

Some remarks:

- I have removed binary view shifts. I did not see a way to describe all rules
  of the new mask changing view shifts using those.
- There is no longer the need for the notion of "frame shifting assertions" and
  these are thus removed. The rules for Hoare triples are thus also stated in
  terms of primitive view shifts.

TODO:

- Maybe rename primitive view shift into something more sensible
- Figure out a way to deal with closed proofs (see the commented out stuff in
  tests/heap_lang and tests/barrier_client).
parent 6b6381fe
......@@ -66,13 +66,9 @@ program_logic/model.v
program_logic/adequacy.v
program_logic/lifting.v
program_logic/invariants.v
program_logic/viewshifts.v
program_logic/wsat.v
program_logic/ownership.v
program_logic/weakestpre.v
program_logic/weakestpre_fix.v
program_logic/pviewshifts.v
program_logic/resources.v
program_logic/hoare.v
program_logic/language.v
program_logic/ectx_language.v
......@@ -86,6 +82,7 @@ program_logic/sts.v
program_logic/namespaces.v
program_logic/boxes.v
program_logic/counter_examples.v
program_logic/iris.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
......@@ -105,7 +102,6 @@ heap_lang/lib/barrier/protocol.v
heap_lang/lib/barrier/proof.v
heap_lang/proofmode.v
tests/heap_lang.v
tests/program_logic.v
tests/one_shot.v
tests/joining_existentials.v
tests/proofmode.v
......@@ -122,6 +118,5 @@ proofmode/notation.v
proofmode/invariants.v
proofmode/weakestpre.v
proofmode/ghost_ownership.v
proofmode/sts.v
proofmode/classes.v
proofmode/class_instances.v
......@@ -12,9 +12,9 @@ Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
Section derived.
Context {Σ : iFunctor}.
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val iProp heap_lang Σ.
Context `{irisG heap_lang Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E x ef e Φ :
......
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.algebra Require Import upred_big_op gmap frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import weakestpre.
......@@ -13,7 +13,8 @@ Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
(** The CMRA we need. *)
Class heapG Σ := HeapG {
heap_inG :> authG heap_lang Σ heapUR;
heapG_iris_inG :> irisG heap_lang Σ;
heap_inG :> authG Σ heapUR;
heap_name : gname
}.
(** The Functor we need. *)
......@@ -25,16 +26,16 @@ Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd).
Section definitions.
Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
auth_own heap_name {[ l := (q, DecAgree v) ]}.
Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
Definition heap_mapsto := proj1_sig heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
proj2_sig heap_mapsto_aux.
Definition heap_inv (h : heapUR) : iPropG heap_lang Σ :=
Definition heap_inv (h : heapUR) : iProp Σ :=
ownP (of_heap h).
Definition heap_ctx : iPropG heap_lang Σ :=
Definition heap_ctx : iProp Σ :=
auth_ctx heap_name heapN heap_inv.
Global Instance heap_inv_proper : Proper (() ==> (⊣⊢)) heap_inv.
......@@ -44,9 +45,7 @@ Section definitions.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
Instance: Params (@heap_inv) 1.
Instance: Params (@heap_mapsto) 4.
Instance: Params (@heap_ctx) 2.
Instance: Params (@heap_inv) 2.
Notation "l ↦{ q } v" := (heap_mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
......@@ -54,8 +53,8 @@ Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : gFunctors}.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val iPropG heap_lang Σ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types σ : state.
Implicit Types h g : heapUR.
......@@ -103,15 +102,14 @@ Section heap.
Hint Resolve heap_store_valid.
(** Allocation *)
Lemma heap_alloc E σ :
authG heap_lang Σ heapUR nclose heapN E
Lemma heap_alloc `{irisG heap_lang Σ, authG Σ heapUR} E σ :
ownP σ ={E}=> _ : heapG Σ, heap_ctx [ map] lv σ, l v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro.
apply (auth_alloc (ownP of_heap) heapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim=> γ.
rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r.
rewrite -(exist_intro (HeapG _ _ _ γ)) /heap_ctx; apply and_mono_r.
rewrite heap_mapsto_eq /heap_mapsto_def /heap_name.
induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty; apply True_intro. }
......@@ -157,22 +155,21 @@ Section heap.
Proof. by rewrite heap_mapsto_op_half. Qed.
(** Weakest precondition *)
(* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
Lemma wp_alloc E e v Φ :
to_val e = Some v nclose heapN E
heap_ctx ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst. iFrame "Hheap". iNext.
iIntros (l) "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
iFrame "Hheap". iSplitR; first iPureIntro.
{ by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
iIntros "Hheap". iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
iVs (auth_empty heap_name) as "Hh".
iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto.
rewrite left_id /heap_inv. iDestruct "Hv" as %?.
iApply wp_alloc_pst. iFrame "Hh". iNext.
iIntros (l) "[% Hh]"; iVsIntro.
iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]").
{ rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
iFrame "Hh". iPureIntro.
by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
Qed.
Lemma wp_load E l q v Φ :
......@@ -180,14 +177,15 @@ Section heap.
heap_ctx l {q} v (l {q} v ={E}= Φ v)
WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros (?) "[#Hh [Hl HΦ]]".
iIntros (?) "[#Hinv [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
rewrite of_heap_singleton_op //. by iFrame.
iIntros "> Hown". iVsIntro. iVs ("Hclose" with "* [Hown]").
{ iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
by iApply "HΦ".
Qed.
Lemma wp_store E l v' e v Φ :
......@@ -195,15 +193,18 @@ Section heap.
heap_ctx l v' (l v ={E}= Φ (LitV LitUnit))
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
iIntros (<-%of_to_val ?) "[#Hinv [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
rewrite of_heap_singleton_op //; eauto. by iFrame.
iIntros "> Hl". iVsIntro.
iVs ("Hclose" $! {[l := (1%Qp, DecAgree v)]} with "[Hl]").
{ iSplit.
- iPureIntro; by apply singleton_local_update, exclusive_local_update.
- rewrite of_heap_singleton_op //; eauto. }
by iApply "HΦ".
Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
......@@ -213,12 +214,13 @@ Section heap.
Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
rewrite /heap_inv.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
rewrite of_heap_singleton_op //. by iFrame.
iIntros "> Hown". iVsIntro. iVs ("Hclose" with "* [Hown]").
{ iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
by iApply "HΦ".
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
......@@ -228,12 +230,15 @@ Section heap.
Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto.
rewrite /heap_inv.
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
rewrite of_heap_singleton_op //; eauto. by iFrame.
iIntros "> Hl". iVsIntro.
iVs ("Hclose" $! {[l := (1%Qp, DecAgree v2)]} with "[Hl]").
{ iSplit.
- iPureIntro; by apply singleton_local_update, exclusive_local_update.
- rewrite of_heap_singleton_op //; eauto. }
by iApply "HΦ".
Qed.
End heap.
......@@ -7,7 +7,7 @@ Definition assert : val :=
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Global Opaque assert.
Lemma wp_assert {Σ} E (Φ : val iProp heap_lang Σ) e `{!Closed [] e} :
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
......
This diff is collapsed.
From iris.algebra Require Export sts.
From iris.program_logic Require Import ghost_ownership.
From iris.prelude Require Export gmap.
(** The STS describing the main barrier protocol. Every state has an index-set
associated with it. These indices are actually [gname], because we use them
......
......@@ -5,13 +5,11 @@ From iris.heap_lang Require Import proofmode.
Import uPred.
Section spec.
Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
Context `{!heapG Σ} `{!barrierG Σ}.
Lemma barrier_spec (N : namespace) :
heapN N
recv send : loc iProp -n> iProp,
recv send : loc iProp Σ -n> iProp Σ,
( P, heap_ctx {{ True }} newbarrier #()
{{ v, l : loc, v = #l recv l P send l P }})
( l P, {{ send l P P }} signal #l {{ _, True }})
......
(* Monotone counter, but using an explicit CMRA instead of auth *)
From iris.program_logic Require Export global_functor.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
From iris.program_logic Require Import auth.
From iris.proofmode Require Import invariants ghost_ownership coq_tactics.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
Definition newcounter : val := λ: <>, ref #0.
Definition inc : val :=
......@@ -14,18 +12,17 @@ Definition read : val := λ: "l", !"l".
Global Opaque newcounter inc get.
(** The CMRA we need. *)
Class counterG Σ := CounterG { counter_tokG :> authG heap_lang Σ mnatUR }.
Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }.
Definition counterGF : gFunctorList := [authGF mnatUR].
Instance inGF_counterG `{H : inGFs heap_lang Σ counterGF} : counterG Σ.
Instance inGF_counterG `{H : inGFs Σ counterGF} : counterG Σ.
Proof. destruct H; split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !counterG Σ} (N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Definition counter_inv (l : loc) (n : mnat) : iProp := (l #n)%I.
Definition counter_inv (l : loc) (n : mnat) : iProp Σ := (l #n)%I.
Definition counter (l : loc) (n : nat) : iProp :=
Definition counter (l : loc) (n : nat) : iProp Σ :=
( γ, heapN N heap_ctx
auth_ctx γ N (counter_inv l) auth_own γ (n:mnat))%I.
......@@ -33,53 +30,56 @@ Definition counter (l : loc) (n : nat) : iProp :=
Global Instance counter_persistent l n : PersistentP (counter l n).
Proof. apply _. Qed.
Lemma newcounter_spec (R : iProp) Φ :
Lemma newcounter_spec (R : iProp Σ) Φ :
heapN N
heap_ctx ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}.
Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
iVs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
as (γ) "[#? Hγ]"; try by auto.
iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
iVsIntro. iApply "HΦ". rewrite /counter; eauto 10.
Qed.
Lemma inc_spec l j (Φ : val iProp) :
Lemma inc_spec l j (Φ : val iProp Σ) :
counter l j (counter l (S j) - Φ #()) WP inc #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "(% & #? & #Hγ & Hγf)".
wp_focus (! _)%E.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
wp_let; wp_op. wp_focus (CAS _ _ _).
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
rewrite {2}/counter_inv.
wp_load. iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto.
iVsIntro. wp_let; wp_op. wp_focus (CAS _ _ _).
iVs (auth_open (counter_inv l) with "[Hγf]") as (j'') "(% & Hl & Hclose)"; auto.
rewrite {2}/counter_inv.
destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
- wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
iExists (1 + j `max` j')%nat; iSplit.
{ iPureIntro. apply mnat_local_update. abstract lia. }
rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
rewrite Nat2Z.inj_succ -Z.add_1_l.
iIntros "{$Hl} Hγf". wp_if.
iPvsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto.
- wp_cas_suc; first (by do 3 f_equal).
iVs ("Hclose" $! (1 + j `max` j')%nat with "[Hl]") as "Hγf".
{ iSplit; [iPureIntro|iNext].
{ apply mnat_local_update. abstract lia. }
rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
by rewrite Nat2Z.inj_succ -Z.add_1_l. }
iVsIntro. wp_if.
iVsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia.
- wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]).
iPvsIntro. iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
wp_if. iApply ("IH" with "[Hγf] HΦ"). rewrite {3}/counter; eauto 10.
iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto.
iVsIntro. wp_if. iApply ("IH" with "[Hγf] HΦ"). rewrite {3}/counter; eauto 10.
Qed.
Lemma read_spec l j (Φ : val iProp) :
Lemma read_spec l j (Φ : val iProp Σ) :
counter l j ( i, (j i)%nat counter l i - Φ #i)
WP read #l {{ Φ }}.
Proof.
iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hγ & Hγf)".
rewrite /read. wp_let.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
{ iPureIntro; apply mnat_local_update; abstract lia. }
rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent; iIntros "{$Hl} Hγf".
iApply ("HΦ" with "[%]"); first abstract lia; rewrite /counter; eauto 10.
iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
wp_load.
iVs ("Hclose" $! (j `max` j') with "[Hl]") as "Hγf".
{ iSplit; [iPureIntro|iNext].
{ apply mnat_local_update; abstract lia. }
by rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent. }
iVsIntro. rewrite !mnat_op_max.
iApply ("HΦ" with "[%]"); first abstract lia. rewrite /counter; eauto 10.
Qed.
End proof.
From iris.program_logic Require Export global_functor.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
From iris.algebra Require Import excl.
Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
......@@ -12,22 +12,21 @@ Global Opaque newlock acquire release.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG heap_lang Σ (exclR unitC) }.
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ.
Instance inGF_lockG `{H : inGFs Σ lockGF} : lockG Σ.
Proof. destruct H. split. apply: inGF_inG. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp :=
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
( b : bool, l #b if b then True else own γ (Excl ()) R)%I.
Definition is_lock (l : loc) (R : iProp) : iProp :=
Definition is_lock (l : loc) (R : iProp Σ) : iProp Σ :=
( γ, heapN N heap_ctx inv N (lock_inv γ l R))%I.
Definition locked (l : loc) (R : iProp) : iProp :=
Definition locked (l : loc) (R : iProp Σ) : iProp Σ :=
( γ, heapN N heap_ctx
inv N (lock_inv γ l R) own γ (Excl ()))%I.
......@@ -45,37 +44,36 @@ Proof. apply _. Qed.
Lemma locked_is_lock l R : locked l R is_lock l R.
Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&?&_)"; eauto. Qed.
Lemma newlock_spec (R : iProp) Φ :
Lemma newlock_spec (R : iProp Σ) Φ :
heapN N
heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}.
Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros ">". iExists false. by iFrame. }
iPvsIntro. iApply "HΦ". iExists γ; eauto.
iVsIntro. iApply "HΦ". iExists γ; eauto.
Qed.
Lemma acquire_spec l R (Φ : val iProp) :
Lemma acquire_spec l R (Φ : val iProp Σ) :
is_lock l R (locked l R - R - Φ #()) WP acquire #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iPvsIntro; iSplitL "Hl".
+ iNext. iExists true; eauto.
+ wp_if. by iApply "IH".
- wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
+ iNext. iExists true; eauto.
+ wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto.
iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iVsIntro. wp_if. by iApply "IH".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto.
Qed.
Lemma release_spec R l (Φ : val iProp) :
Lemma release_spec R l (Φ : val iProp Σ) :
locked l R R Φ #() WP release #l {{ Φ }}.
Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)".
rewrite /release. wp_let. iInv N as (b) "[Hl _]".
wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
rewrite /release. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
......@@ -15,16 +15,15 @@ Global Opaque par.
Section proof.
Context `{!heapG Σ, !spawnG Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
Lemma par_spec (Ψ1 Ψ2 : val iProp) e (f1 f2 : val) (Φ : val iProp) :
Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) e (f1 f2 : val) (Φ : val iProp Σ) :
to_val e = Some (f1,f2)%V
(heap_ctx WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP par e {{ Φ }}.
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
rewrite /par. wp_value. iVsIntro. wp_let. wp_proj.
wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
......@@ -32,8 +31,8 @@ Proof.
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp)
(e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp) :
Lemma wp_par (Ψ1 Ψ2 : val iProp Σ)
(e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp Σ) :
(heap_ctx WP e1 {{ Ψ1 }} WP e2 {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP e1 || e2 {{ Φ }}.
......
From iris.program_logic Require Export global_functor.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
From iris.algebra Require Import excl.
Definition spawn : val :=
λ: "f",
......@@ -17,25 +17,22 @@ Global Opaque spawn join.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG {
spawn_tokG :> inG heap_lang Σ (exclR unitC);
}.
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
(** The functor we need. *)
Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
(* Show and register that they match. *)
Instance inGF_spawnG `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
Instance inGF_spawnG `{H : inGFs Σ spawnGF} : spawnG Σ.
Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp) : iProp :=
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( lv, l lv (lv = NONEV
v, lv = SOMEV v (Ψ v own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp) : iProp :=
Definition join_handle (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
(heapN N γ, heap_ctx own γ (Excl ())
inv N (spawn_inv γ l Ψ))%I.
......@@ -49,7 +46,7 @@ Global Instance join_handle_ne n l :
Proof. solve_proper. Qed.
(** The main proofs. *)
Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) :
Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) (Φ : val iProp Σ) :
to_val e = Some f
heapN N
heap_ctx WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l)
......@@ -57,29 +54,27 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
Proof.
iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
wp_let. wp_alloc l as "Hl". wp_let.
iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- iVsIntro. wp_seq. iVsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv N as (v') "[Hl _]".
wp_store. iPvsIntro. iSplit; [iNext|done].
iExists (SOMEV v). iFrame. eauto.
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) :
Lemma join_spec (Ψ : val iProp Σ) l (Φ : val iProp Σ) :
join_handle l Ψ ( v, Ψ v - Φ v) WP join #l {{ Φ }}.
Proof.
rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_match. iApply ("IH" with "Hγ Hv").
- iVs ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iVsIntro. wp_match. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]";