Updated semantics and worked on rules

parent 4f51005a
Pipeline #6998 canceled with stages
This diff is collapsed.
This diff is collapsed.
...@@ -37,9 +37,9 @@ Inductive expr := ...@@ -37,9 +37,9 @@ Inductive expr :=
| CAS (e0 : expr) (e1 : expr) (e2 : expr) | CAS (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr) | FAA (e1 : expr) (e2 : expr)
(* Process *) (* Process *)
| Start (c e : expr) | Start (e : expr)
(* Channels *) (* Channels *)
| NewChan (* | NewChan *)
| Send (c e : expr) | Send (c e : expr)
| Recv (c : expr). | Recv (c : expr).
...@@ -68,8 +68,8 @@ Fixpoint to_expr (e : expr) : dist_lang.expr := ...@@ -68,8 +68,8 @@ Fixpoint to_expr (e : expr) : dist_lang.expr :=
| Store e1 e2 => dist_lang.Store (to_expr e1) (to_expr e2) | Store e1 e2 => dist_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => dist_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2) | CAS e0 e1 e2 => dist_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| FAA e1 e2 => dist_lang.FAA (to_expr e1) (to_expr e2) | FAA e1 e2 => dist_lang.FAA (to_expr e1) (to_expr e2)
| Start c e => dist_lang.Start (to_expr c) (to_expr e) | Start e => dist_lang.Start (to_expr e)
| NewChan => dist_lang.NewChan (* | NewChan => dist_lang.NewChan *)
| Send c e => dist_lang.Send (to_expr c) (to_expr e) | Send c e => dist_lang.Send (to_expr c) (to_expr e)
| Recv c => dist_lang.Recv (to_expr c) | Recv c => dist_lang.Recv (to_expr c)
end. end.
...@@ -108,9 +108,9 @@ Ltac of_expr e := ...@@ -108,9 +108,9 @@ Ltac of_expr e :=
constr:(CAS e0 e1 e2) constr:(CAS e0 e1 e2)
| dist_lang.FAA ?e1 ?e2 => | dist_lang.FAA ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2) let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| dist_lang.Start ?e1 ?e2 => | dist_lang.Start ?e =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Start e1 e2) let e := of_expr e in constr:(Start e)
| dist_lang.NewChan => constr:(NewChan) (* | dist_lang.NewChan => constr:(NewChan) *)
| dist_lang.Send ?e1 ?e2 => | dist_lang.Send ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Send e1 e2) let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Send e1 e2)
| dist_lang.Recv ?e => | dist_lang.Recv ?e =>
...@@ -130,10 +130,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool := ...@@ -130,10 +130,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
| Val _ _ _ | ClosedExpr _ => true | Val _ _ _ | ClosedExpr _ => true
| Var x => bool_decide (x X) | Var x => bool_decide (x X)
| Rec f x e => is_closed (f :b: x :b: X) e | Rec f x e => is_closed (f :b: x :b: X) e
| Lit _ | NewChan => true | Lit _ (* | NewChan *) => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Recv e => | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Start e | Recv e =>
is_closed X e is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | Start e1 e2 | Send e1 e2=> | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | Send e1 e2=>
is_closed X e1 && is_closed X e2 is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 => | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2 is_closed X e0 && is_closed X e1 && is_closed X e2
...@@ -195,8 +195,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr := ...@@ -195,8 +195,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Store e1 e2 => Store (subst x es e1) (subst x es e2) | Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2) | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
| FAA e1 e2 => FAA (subst x es e1) (subst x es e2) | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
| Start e1 e2 => Start (subst x es e1) (subst x es e2) | Start e => Start (subst x es e)
| NewChan => NewChan (* | NewChan => NewChan *)
| Send e1 e2 => Send (subst x es e1) (subst x es e2) | Send e1 e2 => Send (subst x es e1) (subst x es e2)
| Recv e => Recv (subst x es e) | Recv e => Recv (subst x es e)
end. end.
...@@ -218,32 +218,31 @@ Definition is_atomic (e : expr) := ...@@ -218,32 +218,31 @@ Definition is_atomic (e : expr) :=
| Fork _ => true | Fork _ => true
(* Make "skip" atomic *) (* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => true | App (Rec _ _ (Lit _)) (Lit _) => true
| NewChan => true (* | NewChan => true *)
(* | Start e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2)) (* WRONG *) *) (* | Start e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2)) (* WRONG *) *)
| Start c _ => bool_decide (is_Some (to_val c) is_Some (to_val e)) | Start e => bool_decide (is_Some (to_val e))
| Send c e => bool_decide (is_Some (to_val c) is_Some (to_val e)) | Send c e => bool_decide (is_Some (to_val c) is_Some (to_val e))
(* | Recv c => bool_decide (is_Some (to_val c)) *) (* | Recv c => bool_decide (is_Some (to_val c)) *)
| _ => false | _ => false
end. end.
Lemma my_test_lemma e σ e' σ' pe : head_step'' e σ e' σ' pe -> True.
Proof.
intro Hstep.
inverse_head''.
Qed.
Definition is_atomic'' (e : pexpr) := is_atomic e.2. Definition is_atomic'' (e : pexpr) := is_atomic e.2.
Lemma is_atomic_correct s e : is_atomic'' e Atomic s (to_expr'' e). Lemma is_atomic_correct s e : is_atomic'' e Atomic s (to_expr'' e).
Proof. Proof.
intros He. unfold is_atomic'' in He. unfold to_expr''. destruct e. simpl in *. intros He. unfold is_atomic'' in He. unfold to_expr''. destruct e. simpl in *.
apply strongly_atomic_atomic, ectx_language_atomic. apply strongly_atomic_atomic, ectx_language_atomic.
- intros σ e' σ' ef Hstep. simpl in *. apply to_val_val''. - intros σ e' σ' ef Hstep''. simpl in *. apply to_val_val''.
revert Hstep. inversion 1. inverse_head''; try (revert Hstep; destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
+ revert H8. inversion 1;
first(revert H16; (* head_step case *)
destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto; inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto;
unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto); unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto);
repeat(revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//); revert Hstep'; destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto).
(* * (* destruct e. *) simpl in *. subst. unfold to_expr in H9. destruct e; try inversion H9; try inversion He. *)
+ revert Hstep.
destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
- apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill. unfold fill_item'' in Hfill. apply to_val_val''. inversion Hfill. - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill. unfold fill_item'' in Hfill. apply to_val_val''. inversion Hfill.
destruct e'. simpl in *. (* inversion Hfill. inversion H1. *) destruct e'. simpl in *. (* inversion Hfill. inversion H1. *)
...@@ -340,7 +339,7 @@ Ltac reshape_expr e tac := ...@@ -340,7 +339,7 @@ Ltac reshape_expr e tac :=
| CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0 | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
| FAA ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FaaRCtx v1 :: K) e2) | FAA ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FaaRCtx v1 :: K) e2)
| FAA ?e1 ?e2 => go (FaaLCtx e2 :: K) e1 | FAA ?e1 ?e2 => go (FaaLCtx e2 :: K) e1
| Start ?e1 ?e2 => go (StartCtx e2 :: K) e1 | Start ?e => go (StartCtx :: K) e
| Send ?e1 ?e2 => go (SendLCtx e2 :: K) e1 | Send ?e1 ?e2 => go (SendLCtx e2 :: K) e1
| Send ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (SendRCtx v1 :: K) e2) | Send ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (SendRCtx v1 :: K) e2)
| Recv ?e => go (RecvCtx :: K) e | Recv ?e => go (RecvCtx :: K) e
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.dist_lang Require Export lifting.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
adequate s e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro. iExists gen_heap_ctx. iFrame "Hh".
iApply (Hwp (HeapG _ _ _)).
Qed.
This diff is collapsed.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
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.
wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth auth.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ mcounterG Σ.
Proof. solve_inG. Qed.
Section mono_proof.
Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
( n, own γ ( (n : mnat)) l #n)%I.
Definition mcounter (l : loc) (n : nat) : iProp Σ :=
( γ, inv N (mcounter_inv γ l) own γ ( (n : mnat)))%I.
(** The main proofs. *)
Global Instance mcounter_persistent l n : Persistent (mcounter l n).
Proof. apply _. Qed.
Lemma newcounter_mono_spec :
{{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
Qed.
Lemma incr_mono_spec l n :
{{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
Proof.
iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "[#Hinv Hγf]".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf"). apply: auth_frag_mono.
by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
rewrite {3}/mcounter; eauto 10.
Qed.
Lemma read_mono_spec l j :
{{{ mcounter l j }}} read #l {{{ i, RET #i; j i%nat mcounter l i }}}.
Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
Qed.
End mono_proof.
(** Counter with contributions *)
Class ccounterG Σ :=
CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
Definition ccounterΣ : gFunctors :=
#[GFunctor (frac_authR natR)].
Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ ccounterG Σ.
Proof. solve_inG. Qed.
Section contrib_spec.
Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
( n, own γ (! n) l #n)%I.
Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
inv N (ccounter_inv γ l).
Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
own γ (!{q} n).
(** The main proofs. *)
Lemma ccounter_op γ q1 q2 n1 n2 :
ccounter γ (q1 + q2) (n1 + n2) ccounter γ q1 n1 ccounter γ q2 n2.
Proof. by rewrite /ccounter frag_auth_op -own_op. Qed.
Lemma newcounter_contrib_spec (R : iProp Σ) :
{{{ True }}} newcounter #()
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
Qed.
Lemma incr_contrib_spec γ l q n :
{{{ ccounter_ctx γ l ccounter γ q n }}} incr #l
{{{ RET #(); ccounter γ q (S n) }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
Qed.
Lemma read_contrib_spec γ l q n :
{{{ ccounter_ctx γ l ccounter γ q n }}} read #l
{{{ c, RET #c; n c%nat ccounter γ q n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
Qed.
Lemma read_contrib_spec_1 γ l n :
{{{ ccounter_ctx γ l ccounter γ 1 n }}} read #l
{{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
by iApply "HΦ".
Qed.
End contrib_spec.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
Set Default Proof Using "Type".
Structure lock Σ `{!heapG Σ} := Lock {
(* -- operations -- *)
newlock : val;
acquire : val;
release : val;
(* -- predicates -- *)
(* name is used to associate locked with is_lock *)
name : Type;
is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
locked (γ: name) : iProp Σ;
(* -- general properties -- *)
is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
locked_timeless γ : Timeless (locked γ);
locked_exclusive γ : locked γ - locked γ - False;
(* -- operation specs -- *)
newlock_spec N (R : iProp Σ) :
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
acquire_spec N γ lk R :
{{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ R }}};
release_spec N γ lk R :
{{{ is_lock N γ lk R locked γ R }}} release lk {{{ RET #(); True }}}
}.
Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
Arguments release {_ _} _.
Arguments is_lock {_ _} _ _ _ _ _.
Arguments locked {_ _} _ _.
Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
Proper (() ==> ()) (is_lock L N γ lk) := ne_proper _.
From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Import uPred.
Definition parN : namespace := nroot .@ "par".
Definition par : val :=
λ: "fs",
let: "handle" := spawn (Fst "fs") in
let: "v2" := Snd "fs" #() in
let: "v1" := join "handle" in
("v1", "v2").
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !spawnG Σ}.
(* Notice that this allows us to strip a later *after* the two Ψ have been
brought together. That is strictly stronger than first stripping a later
and then merging them, as demonstrated by [tests/joining_existentials.v].
This is why these are not Texan triples. *)
Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) e (f1 f2 : val) (Φ : val iProp Σ)
`{Hef : !IntoVal e (f1,f2)} :
WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} -
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP par e {{ Φ }}.
Proof.
apply of_to_val in Hef as <-. iIntros "Hf1 Hf2 HΦ".
rewrite /par /=. wp_let. wp_proj.
wp_apply (spawn_spec parN with "Hf1").
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
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 Σ) :
WP e1 {{ Ψ1 }} - WP e2 {{ Ψ2 }} -
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP e1 ||| e2 {{ Φ }}.
Proof.
iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]").
by wp_let. by wp_let. auto.
Qed.
End proof.
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Set Default Proof Using "Type".
Definition spawn : val :=
λ: "f",
let: "c" := ref NONE in
Fork ("c" <- SOME ("f" #())) ;; "c".
Definition join : val :=
rec: "join" "c" :=
match: !"c" with
SOME "x" => "x"
| NONE => "join" "c"
end.
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( lv, l lv (lv = NONEV
w, lv = SOMEV w (Ψ w own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( γ, own γ (Excl ()) inv N (spawn_inv γ l Ψ))%I.
Global Instance spawn_inv_ne n γ l :
Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
Proof. solve_proper. Qed.
Global Instance join_handle_ne n l :
Proper (pointwise_relation val (dist n) ==> dist n) (join_handle l).
Proof. solve_proper. Qed.
(** The main proofs. *)
Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) `{Hef : !IntoVal e f} :
{{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
apply of_to_val in Hef as <-. iIntros (Φ) "Hf HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork; simpl. iSplitR "Hf".
- wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
Lemma join_spec (Ψ : val iProp Σ) l :
{{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
Proof.
iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
- iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. by iApply "HΦ".
+ iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
Qed.
End proof.
Typeclasses Opaque join_handle.