Stored backups; moved new CMRA's to lib, proved half of proc CMRA

parent 38cc4832
Pipeline #7811 failed with stages
in 0 seconds
......@@ -51,6 +51,8 @@ theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/counter_examples.v
theories/base_logic/lib/fractional.v
theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/gen_proc.v
theories/base_logic/lib/gen_dist.v
theories/base_logic/lib/core.v
theories/base_logic/lib/fancy_updates_from_vs.v
theories/program_logic/adequacy.v
......
This diff is collapsed.
From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic Require Export gen_heap.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import fractional.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
Definition to_auth {A} (a : A) : auth A :=
{| authoritative := Excl' a; auth_own := a |}.
Definition to_excl {A} (a : A) : excl A := Excl a.
(* Process state *)
Definition gen_procUR (L V : Type) `{Countable L} : ucmraT :=
gmapUR L (gen_heapUR L V).
Definition to_gen_proc {L V} `{Countable L} (σ : (gmap L (gmap L V))) : gen_procUR L V :=
(* fmap (λ h, (fmap (λ v, (1%Qp, to_agree (v : leibnizC V))) h)) σ. *)
fmap (λ h, to_gen_heap h) σ.
(** The CMRA we need. *)
Class gen_procG (L V : Type) (Σ :gFunctors) `{Countable L} := GenProcG {
gen_proc_inG :> inG Σ (authR (gen_procUR L V)); (* Why authR? *)
gen_proc_name : gname
}.
Arguments gen_proc_name {_ _ _ _ _} _ : assert.
Class gen_procPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
{ gen_proc_preG_inG :> inG Σ (authR (gen_procUR L V)) }.
Definition gen_procΣ (L V : Type) `{Countable L} : gFunctors :=
#[GFunctor (authR (gen_procUR L V))].
Instance subG_gen_procPreG {Σ L V} `{Countable L} :
subG (gen_procΣ L V) Σ gen_procPreG L V Σ.
Proof. solve_inG. Qed.
Section proc_definitions.
Context `{pG : gen_procG L V Σ}.
Definition gen_proc_ctx (σ : gmap L (gmap L V)) : iProp Σ :=
own (gen_proc_name pG) ( (to_gen_proc σ)) (* ∗ gen_heap_ctx (snd σ) *).
Inductive proc_mapping : Type :=
| pinit : L -> proc_mapping
| pmap : L -> L -> Qp -> V -> proc_mapping
.
Definition proc_match (pm : proc_mapping) :
gen_procUR L V :=
match pm with
| pinit p => {[ p := ]}
| pmap p l q v => {[ p := {[ l := (q, to_agree (v : leibnizC V))]} ]}
end.
Definition proc_mapsto_def (pm : proc_mapping) : iProp Σ :=
own (gen_proc_name pG) ( (proc_match pm) ).
(* Definition proc_mapsto_def (p : L) (l : L) (q:Qp) (v : V) : iProp Σ := *)
(* own (gen_proc_name pG) (◯ {[ p := {[ l := (q, to_agree (v : leibnizC V)) ]} ]}). *)
(* Definition proc_mapsto_def (pid : L) (h : gmap L V) : iProp Σ := *)
(* own (gen_proc_name pG) (◯ {[ pid := to_gen_heap h ]}). *)
Definition proc_mapsto_aux : seal (@proc_mapsto_def). by eexists. Qed.
Definition proc_mapsto := unseal proc_mapsto_aux.
Definition proc_mapsto_eq : @proc_mapsto = @proc_mapsto_def := seal_eq proc_mapsto_aux.
End proc_definitions.
Local Notation "l p↦{ p }{ q } v" :=
(proc_mapsto (pmap p l q v)) (at level 20).
Local Notation "l p↦{ p } v" :=
(l p{p}{1} v)%I (at level 20).
Local Notation "l p↦{ p }{ q } -" :=
( v, l p{p}{q} v)%I (at level 20) : uPred_scope.
Local Notation "l p↦{ p } -" :=
( v, l p{p} v)%I (at level 20) : uPred_scope.
Local Notation "< p >" :=
(proc_mapsto (pinit p)) (at level 20).
Section to_gen_proc.
Context (L V : Type) `{Countable L}.
Implicit Types σ : gmap L (gmap L V).
(** Conversion to heaps and back *)
Lemma to_gen_proc_valid σ : to_gen_proc σ.
Proof.
simpl. intros l. rewrite lookup_fmap. case (σ !! l); try reflexivity. intro g'. intros l'. rewrite lookup_fmap. by case (g' !! l').
Qed.
Lemma lookup_to_gen_proc_None σ l : σ !! l = None (to_gen_proc σ) !! l = None.
Proof. by rewrite /to_gen_proc lookup_fmap=> ->. Qed.
Lemma gen_proc_singleton_included σ (p:L) (l:L) (q:Qp) (v:V):
{[p := {[l := (q, to_agree v)]}]} (to_gen_proc σ) match (σ !! p) with None => None | Some(h) => h !! l end = Some v.
Proof.
rewrite singleton_included=> -[ah].
rewrite /to_gen_proc lookup_fmap fmap_Some_equiv => -[h'].
move=> /Some_included_total. destruct h'. destruct H0. rewrite H1.
intro.
rewrite H0.
revert H2.
apply gen_heap_singleton_included.
Qed.
Lemma to_gen_proc_insert (p:L) (l:L) (v:V) (σ : gmap L (gmap L V)) :
to_gen_proc (<[ p := match (σ !! p) with None => <[l:=v]> | Some(h) => <[l:=v]>h end]>σ) = <[ p := match (σ !! p) with None => <[l:=(1%Qp, to_agree (v:leibnizC V))]>(to_gen_heap ) | Some(h) => <[l:=(1%Qp, to_agree (v:leibnizC V))]>(to_gen_heap h) end]> (to_gen_proc σ).
Proof. destruct (σ !! p).
- rewrite /to_gen_proc fmap_insert.
assert (to_gen_heap (<[l:=v]>g) = <[l:=(1%Qp, to_agree v)]> (to_gen_heap g)).
apply to_gen_heap_insert.
rewrite H0. reflexivity.
- rewrite /to_gen_proc fmap_insert.
assert ((to_gen_heap ((<[l := v]>):(gmap L V))) = ((<[l := (1%Qp, to_agree v)]>(to_gen_heap )):(gen_heapUR L V))). by rewrite /to_gen_heap fmap_insert. rewrite H0. reflexivity. Qed.
Lemma to_gen_proc_delete p l σ :
to_gen_proc (match σ !! p with None => σ | Some(h) => <[p := delete l h]>σ end) =
match σ !! p with None => (to_gen_proc σ) | Some(h) => <[p := delete l (to_gen_heap h)]>(to_gen_proc σ) end.
Proof.
destruct (σ !! p); try eauto.
- rewrite /to_gen_proc fmap_insert.
assert (to_gen_heap (delete l g) = delete l (to_gen_heap g)). apply to_gen_heap_delete. rewrite H0. reflexivity.
Qed.
End to_gen_proc.
Lemma gen_proc_init `{gen_procPreG L V Σ} σ :
(|==> _ : gen_procG L V Σ, gen_proc_ctx σ)%I.
Proof.
iMod (own_alloc ( to_gen_proc σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_gen_proc_valid. }
iModIntro. by iExists (GenProcG L V Σ _ _ _ γ).
Qed.
(* Construction beyond this point! *)
Section gen_heap.
Context `{gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
Implicit Types h g : gen_heapUR L V.
Implicit Types l : L.
Implicit Types v : V.
(** General properties of mapsto *)
Global Instance mapsto_timeless l q v : Timeless (l {q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
Proof.
intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
op_singleton pair_op agree_idemp.
Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q.
Proof. split. done. apply _. Qed.
Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
Proof.
apply wand_intro_r.
rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
Global Instance ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
Proof.
intros p q. iSplit.
- iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
- iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
Qed.
Global Instance ex_mapsto_as_fractional l q :
AsFractional (l {q} -) (λ q, l {q} -)%I q.
Proof. split. done. apply _. Qed.
Lemma mapsto_valid l q v : l {q} v - q.
Proof.
rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
by apply pure_mono=> /auth_own_valid /singleton_valid [??].
Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - (q1 + q2)%Qp.
Proof.
iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
iApply (mapsto_valid l _ v2). by iFrame.
Qed.
Lemma gen_heap_alloc σ l v :
σ !! l = None gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ) l v.
Proof.
iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
by apply lookup_to_gen_heap_None. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed.
Lemma gen_heap_dealloc σ l v :
gen_heap_ctx σ - l v == gen_heap_ctx (delete l σ).
Proof.
iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
rewrite to_gen_heap_delete. iApply (own_update_2 with "Hσ Hl").
eapply auth_update_dealloc, (delete_singleton_local_update _ _ _).
Qed.
Lemma gen_heap_valid σ l q v : gen_heap_ctx σ - l {q} v - ⌜σ !! l = Some v.
Proof.
iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2; auto.
Qed.
Lemma gen_heap_update σ l v1 v2 :
gen_heap_ctx σ - l v1 == gen_heap_ctx (<[l:=v2]>σ) l v2.
Proof.
iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
by rewrite /to_gen_heap lookup_fmap Hl. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed.
End gen_heap.
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic Require Export gen_heap.
From iris.base_logic Require Export gen_dist.
From iris.program_logic Require Export weakestpre lifting.
From iris.program_logic Require Import ectx_lifting.
From iris.dist_lang Require Export lang.
......@@ -38,7 +38,7 @@ Import uPred.
(* Class distG Σ := DistG { *)
(* distG_invG : invG Σ; *)
(* distG_gen_distG :> gen_distG loc val Σ *)
(* distG_gen_distG :> gen_distG proc_id val Σ *)
(* }. *)
(* Instance distG_irisG `{distG Σ} : irisG dist_lang Σ := { *)
......@@ -47,29 +47,16 @@ Import uPred.
(* }. *)
(* Global Opaque iris_invG. *)
(* ---------- Definition of dist CMRA based on heap CMRA ------------------- *)
(* --------- Actual Stuff --------- *)
Definition gen_distUR (L V : Type) `{Countable L} : ucmraT :=
prodUR (gen_heapUR L (gen_heapUR L V)) (gen_heapUR L (list V * list V)).
Definition to_gen_dist {L V} `{Countable L} (σ : ((gmap L (gmap L V)) * (gmap L (list V * list V)))) : gen_distUR L V :=
((fmap (λ v, (1%Qp, to_agree (to_gen_heap v))) σ.1),
(to_gen_heap σ.2)).
Class gen_distG (L V : Type) (Σ :gFunctors) `{Countable L} := Gen_DistG {
gen_dist_inG :> inG Σ (authR (gen_distUR L V)); (* Why authR? *)
gen_dist_name : gname
}.
Arguments gen_dist_name {_ _ _ _ _} _ : assert.
Section definitions.
Context `{dG : gen_distG L V Σ}.
Definition gen_dist_ctx (σ : (gmap L (gmap L V)) * (gmap L (list V * list V))) : iProp Σ :=
own (gen_dist_name dG) ( (to_gen_dist σ)) (* ∗ gen_heap_ctx (snd σ) *).
End definitions.
(* Class gen_distG (L V : Type) (Σ :gFunctors) `{Countable L} := Gen_DistG { *)
(* gen_dist_inG :> inG Σ (authR (gen_distUR L V)); (* Why authR? *) *)
(* gen_dist_name : gname *)
(* }. *)
Class distG Σ := DistG {
distG_invG : invG Σ;
distG_gen_distG :> gen_distG loc val Σ
distG_gen_distG :> gen_distG positive val Σ
}.
Instance distG_irisG `{distG Σ} : irisG dist_lang Σ := {
......@@ -79,13 +66,33 @@ Instance distG_irisG `{distG Σ} : irisG dist_lang Σ := {
Global Opaque iris_invG.
(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
Notation "l ↦ v" :=
(mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : uPred_scope.
Notation "l ↦{ q } -" := ( v, l {q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : uPred_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.
(* Local Notation "l p↦{ p }{ q } v" := *)
(* (dist_mapsto (inl (p, l, q, v))) (at level 20). *)
(* Local Notation "l p↦{ p } v" := *)
(* (l p↦{p}{1} v)%I (at level 20). *)
(* Local Notation "l p↦{ p }{ q } -" := *)
(* (∃ v, l p↦{p}{q} v)%I (at level 20) : uPred_scope. *)
(* Local Notation "l p↦{ p } -" := *)
(* (∃ v, l p↦{p} v)%I (at level 20) : uPred_scope. *)
(* Local Notation "l c↦ [ a , b ]" := *)
(* (dist_mapsto (inr (l, (a,b)))) (at level 20). *)
(* Local Notation "l c↦ -" := *)
(* (∃ l r, l c↦ [l,r])%I (at level 20) : uPred_scope. *)
Local Notation "{ x , .. , y }{ p }" :=
(dist_mapsto (inl (p, foldr (fun lv m => <[lv.1 := lv.2]>m) () ((cons x .. (cons y nil) ..))))).
Local Notation "{ }{ p }" :=
(dist_mapsto (inl (p, ))).
Local Notation "l ↦ v" :=
(l,v) (at level 20).
Local Notation "l ↦ -" :=
( v, (l,v)) (at level 20).
Local Notation "l c↦ [ a , b ]" :=
(dist_mapsto (inr (l, (a,b)))) (at level 20).
Local Notation "l c↦ -" :=
( l r, l c [l,r])%I (at level 20) : uPred_scope.
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
......@@ -142,7 +149,6 @@ Local Hint Resolve alloc_fresh''.
Local Hint Resolve to_of_val.
Local Hint Resolve to_of_val''.
Section lifting.
Context `{distG Σ}.
Implicit Types P Q : iProp Σ.
......@@ -152,12 +158,57 @@ Implicit Types σ : state''.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork s E (e:pexpr) Φ :
Φ (e.1, LitV LitUnit) WP e @ s; {{ _, True }} WP (e.1, Fork e.2) @ s; E {{ Φ }}.
{ }{e.1} Φ (e.1, LitV LitUnit) WP e @ s; {{ _, True }} WP (e.1, Fork e.2) @ s; E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step ((e.1, Fork e.2):pexpr) (e.1, Lit LitUnit) [e]) //=.
rewrite -(wp_lift_head_step ((e.1, Fork e.2):pexpr)).
- iIntros "[e1 Hfork]" (σ) "H". iApply fupd_frame_l. iSplit.
+ unfold head_reducible. simpl. iExists (e.1, Lit $ LitUnit). iExists σ. iExists ([e]).
admit.
+ iApply step_fupd_intro.
rewrite -step_fupd_intro //. *)
- simpl. destruct e. simpl. unfold to_val''. simpl. reflexivity.
rewrite -(wp_lift_pure_det_head_step ((e.1, Fork e.2):pexpr) (e.1, Lit LitUnit) [e]) //=; eauto.
- rewrite -step_fupd_intro //. rewrite later_sep.
rewrite <- (wp_value _ _ _ ((e.1, Lit _):pexpr)). rewrite right_id //. reflexivity.
- intros. unfold head_reducible. simpl. exists (e.1, Lit LitUnit). exists σ1. exists [e]. destruct e. destruct σ1. simpl. apply ExprS' with h. unfold state_match. eauto. repeat econstructor. apply ExprS. apply ForkS.
- intros. inv_head_step''. destruct e. inversion H4. inversion H6. inversion H7. eauto.
Qed.
(* (** Base axioms for core primitives of the language: Stateless reductions *) *)
(* Lemma wp_fork s E (e:pexpr) Φ : *)
(* ▷ Φ (e.1, LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP (e.1, Fork e.2) @ s; E {{ Φ }}. *)
(* Proof. *)
(* rewrite -(wp_lift_pure_det_head_step ((e.1, Fork e.2):pexpr) (e.1, Lit LitUnit) [e]) //=; eauto. *)
(* - rewrite -step_fupd_intro //. rewrite later_sep. *)
(* rewrite <- (wp_value _ _ _ ((e.1, Lit _):pexpr)). rewrite right_id //. reflexivity. *)
(* - intros. unfold head_reducible. simpl. exists (e.1, Lit LitUnit). exists σ1. exists [e]. destruct e. destruct σ1. simpl. apply ExprPS' with (match h !! l with Some (σ) => σ | None => ∅ end) [e]. unfold state_match. eauto. repeat econstructor. apply ExprS. apply ForkS. *)
(* - intros. inv_head_step''. destruct e. inversion H4. inversion H6. inversion H7. eauto. *)
(* Qed. *)
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork s E (e:pexpr) Φ σh :
(* {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}. *)
(* ▷ Φ (e.1, LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ {{{ True }}} (e.1, Fork e.2) @ s; E {{{ RET (e.1, LitV LitUnit); Φ (e.1, LitV LitUnit) }}}. *)
(e.1 σh) Φ (e.1, LitV LitUnit) WP e @ s; {{ _, True }} WP (e.1, Fork e.2) @ s; E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step ((e.1, Fork e.2):pexpr) (e.1, Lit LitUnit) [e]) //=; eauto.
(* iIntros (<-%of_to_val Φ) ">Hl HΦ". *)
rewrite -(wp_lift_pure_det_head_step ((e.1, Fork e.2):pexpr) (e.1, Lit LitUnit) [e]) //=.
rewrite -(wp_lift_head_step ((e.1, Fork e.2):pexpr)).
- iIntros "[e1 Hfork]" (σ) "H". iApply fupd_frame_l. iSplit.
+ unfold head_reducible. simpl. iExists (e.1, Lit $ LitUnit). iExists σ. iExists ([e]).
admit.
+ iApply step_fupd_intro.
rewrite -step_fupd_intro //. *)
- simpl. destruct e. simpl. unfold to_val''. simpl. reflexivity.
rewrite -(wp_lift_pure_det_head_step ((e.1, Fork e.2):pexpr) (e.1, Lit LitUnit) [e]) //=; eauto.
- rewrite -step_fupd_intro //. rewrite later_sep.
rewrite <- (wp_value _ _ _ ((e.1, Lit _):pexpr)). rewrite right_id //. reflexivity.
- intros. unfold head_reducible. simpl. exists (e.1, Lit LitUnit). exists σ1. exists [e]. destruct e. destruct σ1. simpl. apply ExprPS' with (match h !! l with Some (σ) => σ | None => end) [e]. unfold state_match. eauto. repeat econstructor. apply ExprS. apply ForkS.
- intros. unfold head_reducible. simpl. exists (e.1, Lit LitUnit). exists σ1. exists [e]. destruct e. destruct σ1. simpl. apply ExprS' with h. unfold state_match. eauto. repeat econstructor. apply ExprS. apply ForkS.
- intros. inv_head_step''. destruct e. inversion H4. inversion H6. inversion H7. eauto.
Qed.
......
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.
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".