Commit 2abfd22c authored by Robbert Krebbers's avatar Robbert Krebbers

Use `gen_proofmode`.

parent 4e5128c0
......@@ -5,7 +5,6 @@ theories/lib/mset.v
theories/lib/flock.v
theories/lib/locking_heap.v
theories/lib/U.v
theories/lib/unlock_classes.v
theories/c_translation/monad.v
theories/c_translation/lifting.v
theories/c_translation/proofmode.v
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "dev.2018-04-27.2.1ab890fc") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-04-25.1.8a0ff185") | (= "dev") }
]
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac auth.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Export locking_heap mset flock.
From iris_c.lib Require Export locking_heap flock.
From iris_c.c_translation Require Export monad.
Section lifting.
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import adequacy spin_lock assert par.
From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import mset flock locking_heap.
(* M A := ref (list loc) → Mutex → A *)
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import locking_heap mset flock.
From iris_c.lib Require Export unlock_classes.
From iris_c.c_translation Require Export monad lifting.
From iris.proofmode Require Import coq_tactics.
......@@ -15,7 +12,7 @@ Lemma tac_awp_pure `{locking_heapG Σ, heapG Σ, flockG Σ} Δ Δ' K e1 e2 e φ
envs_entails Δ' (awp (fill K e2) R Φ)
envs_entails Δ (awp e R Φ).
Proof.
rewrite /envs_entails=> -> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite envs_entails_eq=> -> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -awp_pure //.
Qed.
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import monad lifting proofmode.
......@@ -83,7 +82,7 @@ Section proofs.
iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]".
iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX").
{ iIntros "Hus". iApply "HΦ". by iFrame. }
{ rewrite -big_sepM_insert_override; eauto. }
{ rewrite -bi.big_sepM_insert_override; eauto. }
Qed.
Lemma a_fill R Ψ Φ K e :
......@@ -105,7 +104,7 @@ Section proofs.
iIntros (v) "H /=". rewrite /a_seq_bind. awp_lam. awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
awp_lam. iApply awp_bind. iApply a_seq_spec.
iUnlock. by awp_lam.
iModIntro. by awp_lam.
Qed.
Lemma a_load_spec R (l : loc) (v : val) Φ :
......@@ -160,14 +159,14 @@ Section proofs.
wp_let. wp_alloc l as "Hl".
iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
{ remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
iExFalso. rewrite (bi.big_sepM_lookup _ σ l _); last eauto.
iDestruct "Hls" as (v') "Hl'".
by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
iDestruct "Hl" as "[Hl Hl']".
iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
iModIntro. iFrame "HR". iSplitR "HΦ Hl'".
- iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
+ rewrite big_sepM_insert; eauto. iFrame. eauto.
+ rewrite bi.big_sepM_insert; eauto. iFrame. eauto.
+ iPureIntro. by rewrite locked_locs_alloc_unlocked.
- by iApply "HΦ".
Qed.
......@@ -213,7 +212,7 @@ iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]".
do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
iDestruct "Hv" as "[Hv Hl]".
rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
......@@ -223,7 +222,7 @@ iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
iSpecialize ("Hls" with "[Hl']"); eauto.
wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv".
- iExists ({[#l]} X),(<[l:=LLvl]> σ). iFrame. iSplitL.
+ rewrite -big_sepM_insert_override; eauto.
+ rewrite -bi.big_sepM_insert_override; eauto.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
......
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import flock locking_heap.
From iris.proofmode Require Import modalities classes.
Section contents.
Context `{heapG Σ, flockG Σ, locking_heapG Σ}.
......@@ -12,7 +12,7 @@ Section contents.
([ list] x ls, x.1 L x.2)
(([ list] x ls, x.1 U x.2) - P))%I.
Lemma U_mono P Q : (P Q) (U P) (U Q).
Lemma U_mono P Q : (P Q) U P U Q.
Proof.
intros HPQ.
unfold U. iDestruct 1 as (ls) "[Hls HP]".
......@@ -22,15 +22,15 @@ Section contents.
Lemma U_intro P : P U P.
Proof.
iIntros "HP". iExists [].
rewrite !big_sepL_nil. eauto.
rewrite !bi.big_sepL_nil. eauto.
Qed.
Lemma U_multiplicative P Q : (U P) (U Q) (U (P Q)).
Lemma U_sep_2 P Q : U P U Q U (P Q).
Proof.
iIntros "[HP HQ]".
iDestruct "HP" as (ls1) "[HP1 HP2]".
iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
iExists (ls1++ls2). rewrite !big_sepL_app. iFrame.
iExists (ls1++ls2). rewrite !bi.big_sepL_app. iFrame.
iIntros "[HP1 HQ1]". iSplitL "HP1 HP2".
- by iApply "HP2".
- by iApply "HQ2".
......@@ -38,9 +38,25 @@ Section contents.
Lemma U_unlock l v : l L v U (l U v).
Proof.
iIntros "Hl". iExists [(l,v)].
rewrite !big_sepL_cons !big_sepL_nil !right_id.
iFrame. simpl. iIntros "Hl". iFrame.
iIntros "Hl". iExists [(l,v)]. iIntros "/= {$Hl} [$ _]".
Qed.
Class IntoUnlock (P Q : iProp Σ) := into_unlock : P U Q.
Global Instance into_unlock_intro P : IntoUnlock (U P) P.
Proof. rewrite /IntoUnlock. reflexivity. Qed.
Global Instance into_unlock_id P : IntoUnlock P P | 10.
Proof. apply U_intro. Qed.
Global Instance into_unlock_unlock l v : IntoUnlock (l L v)%I (l U v)%I | 0.
Proof. apply U_unlock. Qed.
Lemma modality_U_mixin :
modality_mixin U MIEnvId (MIEnvTransform IntoUnlock).
Proof.
split; simpl; eauto using bi.equiv_entails_sym, U_intro,
U_mono, U_sep_2 with typeclass_instances.
Qed.
Definition modality_U := Modality _ modality_U_mixin.
Global Instance from_modal_later P : FromModal modality_U (U P) (U P) P.
Proof. by rewrite /FromModal. Qed.
End contents.
......@@ -3,7 +3,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock.
From iris.base_logic.lib Require Import cancelable_invariants.
From iris.algebra Require Import auth excl frac.
From iris.base_logic.lib Require Import fractional.
From iris.bi.lib Require Import fractional.
Inductive lockstate :=
| Locked : frac lockstate
......
......@@ -57,17 +57,17 @@ Section definitions.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
End definitions.
Local Notation "l ↦[ x ] v" := (mapsto l x v)
(at level 20, x at level 50, format "l ↦[ x ] v") : uPred_scope.
Local Notation "l ↦L v" := (l [LLvl] v)%I
(at level 20, format "l ↦L v") : uPred_scope.
Local Notation "l ↦U v" := (l [ULvl] v)%I
(at level 20, format "l ↦U v") : uPred_scope.
Local Notation "l ↦L -" := ( v, l L v)%I
(at level 20, format "l ↦L -") : uPred_scope.
Local Notation "l ↦U -" := ( v, l U v)%I
(at level 20, format "l ↦U -") : uPred_scope.
Notation "l ↦[ x ] v" := (mapsto l x v)
(at level 20, x at level 50, format "l ↦[ x ] v") : bi_scope.
Notation "l ↦L v" := (l [LLvl] v)%I
(at level 20, format "l ↦L v") : bi_scope.
Notation "l ↦U v" := (l [ULvl] v)%I
(at level 20, format "l ↦U v") : bi_scope.
Notation "l ↦L -" := ( v, l L v)%I
(at level 20, format "l ↦L -") : bi_scope.
Notation "l ↦U -" := ( v, l U v)%I
(at level 20, format "l ↦U -") : bi_scope.
Lemma to_locking_heap_valid (σ : gmap loc level) : to_locking_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
......@@ -203,15 +203,3 @@ Section properties.
by iDestruct "Hauth" as "[$ $]".
Qed.
End properties.
Notation "l ↦[ x ] v" := (mapsto l x v)
(at level 20, x at level 50, format "l ↦[ x ] v") : uPred_scope.
Notation "l ↦L v" := (l [LLvl] v)%I
(at level 20, format "l ↦L v") : uPred_scope.
Notation "l ↦U v" := (l [ULvl] v)%I
(at level 20, format "l ↦U v") : uPred_scope.
Notation "l ↦L -" := ( v, l L v)%I
(at level 20, format "l ↦L -") : uPred_scope.
Notation "l ↦U -" := ( v, l U v)%I
(at level 20, format "l ↦U -") : uPred_scope.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris_c.lib Require Export locking_heap U.
Import uPred.
Section classes.
Context `{heapG Σ, locking_heapG Σ}.
Class IntoUnlock (P Q : iProp Σ) :=
into_unlock : P U Q.
Class FromUnlock (P Q : iProp Σ) :=
from_unlock : U Q P.
Global Instance into_unlock_intro P : IntoUnlock (U P) P.
Proof. rewrite /IntoUnlock. reflexivity. Qed.
Global Instance into_unlock_id P : IntoUnlock P P | 10.
Proof. apply U_intro. Qed.
Global Instance into_unlock_unlock l v : IntoUnlock (l L v)%I (l U v)%I | 0.
Proof. apply U_unlock. Qed.
Global Instance from_unlock_unlock P : FromUnlock (U P) P.
Proof. rewrite /FromUnlock. reflexivity. Qed.
Class IntoUnlockEnv (Γ1 Γ2 : env (iProp Σ)) :=
into_unlock_env : env_Forall2 IntoUnlock Γ1 Γ2.
Class IntoUnlockEnvs (Δ1 Δ2 : envs (iResUR Σ)) := {
into_unlock_persistent: [] (env_persistent Δ1) [] (env_persistent Δ2);
into_unlocks_wf : envs_wf Δ1 envs_wf Δ2;
into_unlock_spatial: IntoUnlockEnv (env_spatial Δ1) (env_spatial Δ2)
}.
Global Instance into_unlock_env_nil : IntoUnlockEnv Enil Enil.
Proof. constructor. Qed.
Global Instance into_unlock_env_snoc Γ1 Γ2 i P Q :
IntoUnlockEnv Γ1 Γ2 IntoUnlock P Q
IntoUnlockEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.
Global Instance into_unlock_envs Γp Γs1 Γs2 :
IntoUnlockEnv Γs1 Γs2
IntoUnlockEnvs (Envs Γp Γs1) (Envs Γp Γs2).
Proof.
split; try done.
destruct 1; constructor; try naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
Qed.
Lemma into_unlock_env_sound Δ1 Δ2 :
IntoUnlockEnv Δ1 Δ2 [] Δ1 U ([] Δ2).
Proof.
intros Hs; simpl.
induction Hs; simpl.
- apply U_intro.
- rewrite -U_multiplicative. by apply uPred.sep_mono.
Qed.
Lemma into_unlock_envs_sound Δ1 Δ2 :
IntoUnlockEnvs Δ1 Δ2 of_envs Δ1 U (of_envs Δ2).
Proof.
intros [Hp Hs]; rewrite /of_envs /= -!U_multiplicative.
repeat apply uPred.sep_mono; try apply uPred.persistently_mono.
- rewrite -U_intro. apply uPred.pure_mono. apply Hs.
- rewrite -U_intro. by rewrite Hp.
- by apply into_unlock_env_sound.
Qed.
Lemma tac_unlock Δ Δ' Q Q' :
FromUnlock Q Q'
IntoUnlockEnvs Δ Δ'
envs_entails Δ' Q' envs_entails Δ Q.
Proof.
rewrite /envs_entails=> Hf ? HQ.
rewrite into_unlock_envs_sound.
rewrite /FromUnlock in Hf. rewrite -Hf.
by apply U_mono.
Qed.
End classes.
Tactic Notation "iUnlock" :=
iStartProof;
let P := match goal with |- envs_entails _ ?P => P end in
eapply tac_unlock;
[apply _ || fail "iUnlock:" P "does not contain U"
|apply _
|lazy beta (* remove beta redexes caused by removing laters under binders*)].
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import monad lifting proofmode translation.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
......@@ -16,7 +14,7 @@ Section test.
iIntros "Hl".
iApply awp_bind.
iApply a_seq_spec.
iUnlock.
iModIntro.
awp_lam.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment