Skip to content

GitLab

Commit 274019f4 authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Bump coq-iris version; Finish updating program_logic/ files.

parent 99e241f1
Hide whitespace changes
Inline Side-by-side
opam
View file @ 274019f4
......@@ -7,5 +7,5 @@ remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/fri" ]
depends: [
"coq" { >= "8.7" }
"coq-stdpp" { (>= "1.1.0") | (>= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-02-26.0") }
"coq-iris" { (= "branch.gen_proofmode.2018-02-27.1") }
]
theories/algebra/auth.v
View file @ 274019f4
From fri.algebra Require Export excl local_updates.
From fri.algebra Require Import upred updates.
From fri.algebra Require Import upred upred_bi updates.
Import uPred.
Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /.
......@@ -200,7 +201,7 @@ Qed.
Canonical Structure authUR :=
UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
Global Instance auth_frag_persistent a : cmra.Persistent a → cmra.Persistent (◯ a).
Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
(** Internalized properties *)
......@@ -215,17 +216,19 @@ Lemma auth_validI {M} (x : auth A) :
end : uPred M).
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
Lemma auth_validI' {M} (x : auth A) :
(⧆✓ x)%IP ⊣⊢ (match authoritative x with
(⧆✓ x) ⊣⊢ (match authoritative x with
| Excl' a => ⧆(∃ b, a ≡ auth_own x ⋅ b) ∧ ⧆✓ a
| None => ⧆✓ auth_own x
| ExclBot' => False
end : uPred M).
Proof.
rewrite auth_validI.
destruct x as [[[]|]]; simpl; rewrite ?uPred.affine_and; auto.
apply (anti_symm (⊢)); auto using uPred.affine_elim, uPred.False_elim.
destruct x as [[[]|]]; simpl.
- rewrite bi.affinely_and; auto.
- apply (anti_symm (⊢)); auto using bi.affinely_elim, bi.False_elim.
- auto.
Qed.
Unset Printing Notations.
Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
......
theories/algebra/upred_bi.v
View file @ 274019f4
From fri.algebra Require Import upred.
From iris.bi Require Export bi.
From iris.proofmode Require Import classes class_instances.
Import uPred.
......@@ -391,4 +392,28 @@ Proof.
rewrite -Haff. eauto.
Qed.
*)
End ATimeless_uPred.
\ No newline at end of file
Global Instance into_sep_affinely_later P Q1 Q2 :
IntoSep P Q1 Q2 → Affine Q1 → Affine Q2 →
IntoSep (bi_affinely (▷ P)) (bi_affinely (▷ Q1)) (bi_affinely (▷ Q2)).
Proof.
intros Hsep HA1 HA2.
rewrite /IntoSep.
rewrite Hsep.
rewrite -(affine_affinely Q1) -{1}(affine_affinely Q1).
rewrite -(affine_affinely Q2) -{1}(affine_affinely Q2).
rewrite -!uPred_affine_bi_affinely.
unfold_bi. by rewrite affine_later_distrib.
Qed.
End ATimeless_uPred.
Global Instance into_except_0_affine_later {PROP : sbi} (P : PROP):
ATimeless P → IntoExcept0 (⧆▷ P) (⧆P).
Proof.
by rewrite /ATimeless/IntoExcept0 => ->.
Qed.
Global Instance into_pure_valid {M: ucmraT} `{CMRADiscrete A} (a : A) :
IntoPure (✓ a : uPred M)%I (✓ a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
theories/heap_lang/lifting.v
View file @ 274019f4
From fri.program_logic Require Export weakestpre stepshifts.
From fri.algebra Require Export upred.
From fri.program_logic Require Export weakestpre.
From fri.program_logic Require Import ownership ectx_lifting. (* for ownP *)
From fri.heap_lang Require Export lang.
From fri.heap_lang Require Import tactics.
From fri.proofmode Require Import weakestpre pstepshifts.
From iris.proofmode Require Import tactics.
Import uPred.
Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
......
theories/program_logic/auth.v
View file @ 274019f4
......@@ -96,11 +96,6 @@ Section auth.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!AffineFrameShiftAssertion fsaV fsa}.
Global Instance into_except_0_affine_later {PROP : sbi} (P : PROP):
ATimeless P → IntoExcept0 (⧆▷ P) (⧆P).
Proof.
by rewrite /ATimeless/IntoExcept0 => ->.
Qed.
Lemma auth_afsa E N (Ψ : V → iPropG Λ Σ) γ a :
fsaV → nclose N ⊆ E →
......@@ -111,29 +106,24 @@ Section auth.
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "H" "_".
iDestruct "H" as "[Hγ Hφ]".
iMod "Hγ".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affine_elim (own γ _)).
iDestruct (own_valid with "#Hγ") as "Hvalid".
iInv "Hinv" as (a') "[Hγ Hφ]" "_".
iMod "Hγ". iMod "Hγf". iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affinely_elim (own γ _)).
iDestruct (own_valid with "Hγ") as "#Hvalid".
iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl.
iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_afsa_afsa. iApply afsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ". iSplitL ""; first by iPureIntro.
rewrite -?uPred_affine_bi_affinely.
by rewrite -affine_affine_later. }
iIntros "@". iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iIntros "@". iNext. iExists (b ⋅ af). by iFrame.
iAlways. iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
iMod (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
{ set_solver. }
iModIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iAlways. iNext. iExists (b ⋅ af). by iFrame.
Qed.
(* TODO: move to classes.v *)
Global Instance from_assumption_affine p P Q:
FromAssumption p P Q → FromAssumption p (⧆P) Q.
Proof. destruct p; by rewrite /FromAssumption /= ?affine_elim. Qed.
Lemma auth_afsa_alt E N (Ψ : V → iPropG Λ Σ) γ a :
fsaV → nclose N ⊆ E →
auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ (∀ af,
......@@ -143,23 +133,23 @@ Proof. destruct p; by rewrite /FromAssumption /= ?affine_elim. Qed.
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affine_elim (own γ _)).
iDestruct (own_valid with "#Hγ") as "Hvalid".
iInv "Hinv" as (a') "[Hγ Hφ]" "_".
iMod "Hγ"; iMod "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affinely_elim (own γ _)).
iDestruct (own_valid with "Hγ") as "#Hvalid".
iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl.
iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_afsa_afsa.
iDestruct ("HΨ" $! af with "[Hφ]") as (b) "(%&HΨ)".
{ iSplitL ""; first done. iIntros "@". iNext. iAssumption. }
iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
{ iSplitL ""; first done. iAlways. iNext. iAssumption. }
iMod (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iSpecialize ("HΨ" with "Hγf").
iApply afsa_wand_r. iSplitL "HΨ".
{ iClear "Hinv". iClear "Hvalid". iAssumption. }
iIntros "@". iIntros (v) "HL". iDestruct "HL" as "(Hφ & HΨ)".
iPvsIntro. iSplitL "Hφ Hγ".
- iIntros "@". rewrite /auth_inv.
iAlways. iIntros (v) "HL". iDestruct "HL" as "(Hφ & HΨ)".
iModIntro. iSplitL "Hφ Hγ".
- iAlways. rewrite /auth_inv.
iNext. iExists (b ⋅ af). by iFrame "Hφ".
- iAssumption.
Qed.
......
theories/program_logic/ghost_ownership.v
View file @ 274019f4
......@@ -58,6 +58,9 @@ Qed.
Global Instance into_sep_own γ a1 a2:
IntoSep (own γ (a1 ⋅ a2)) (own γ a1) (own γ a2).
Proof. rewrite /IntoSep own_op //=. Qed.
Global Instance from_sep_own γ a1 a2:
FromSep (own γ (a1 ⋅ a2)) (own γ a1) (own γ a2).
Proof. rewrite /FromSep own_op //=. Qed.
Lemma own_valid γ a : own γ a ⊢ ⧆✓ a.
Proof.
......
theories/program_logic/pstepshifts.v
View file @ 274019f4
......@@ -298,4 +298,9 @@ Proof.
Qed.
Tactic Notation "iPsvs" open_constr(lem) :=
iApply (psvs_wand with lem); iAlways; iIntros lem.
\ No newline at end of file
let t :=
lazymatch lem with
| ITrm ?t _ _ => t
| _ => lem
end in
iSpecialize lem; iApply (psvs_wand with t); iAlways; iIntros t.
\ No newline at end of file
theories/program_logic/pviewshifts.v
View file @ 274019f4
......@@ -509,3 +509,22 @@ Proof.
intros. rewrite pvs_frame_r. done.
Qed.
Global Instance elim_modal_fsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ:
FrameShiftAssertion fsaV fsa →
ElimModal True (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
Proof.
rewrite /ElimModal => FSA H.
iIntros "(H1&H2)".
iApply fsa_pvs_fsa.
iMod "H1"; first by set_solver. iModIntro. by iApply "H2".
Qed.
Global Instance elim_modal_afsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ:
AffineFrameShiftAssertion fsaV fsa →
ElimModal True (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
Proof.
rewrite /ElimModal => FSA H.
iIntros "(H1&H2)".
iApply afsa_pvs_afsa.
iMod "H1"; first by set_solver. iModIntro. by iApply "H2".
Qed.
\ No newline at end of file
theories/program_logic/refine.v
View file @ 274019f4
From stdpp Require Export set.
From fri.algebra Require Import dra cmra_tactics.
From fri.program_logic Require Import
From fri.algebra Require Import upred dra cmra_tactics.
From fri.program_logic Require Import pstepshifts
language wsat refine_raw refine_raw_adequacy hoare ownership.
From fri.proofmode Require Import pviewshifts pstepshifts invariants.
From iris.proofmode Require Import tactics.
Import uPred.
(* A cleaner version of results about the refinement monoid. The
......@@ -23,9 +24,9 @@ Context `{refineG Λ Σ sΛ Kd}.
(* Asserts ownership of physical state sσ in source language *)
Definition ownSP (sσ: state sΛ) :=
(⧆(∃ ts cs ixs, owne (refine sΛ Kd master ∅ (cs ++ [(ts, sσ)]) ixs)))%I.
Instance ownSP_affine sσ: AffineP (ownSP sσ).
Instance ownSP_affine sσ: Affine (ownSP sσ).
Proof. rewrite /ownSP; apply _. Qed.
Instance ownSP_atimeless sσ: ATimelessP (ownSP sσ).
Instance ownSP_atimeless sσ: ATimeless (ownSP sσ).
Proof. rewrite /ownSP; apply _. Qed.
(* Ownership of thread i executing expression e *)
......@@ -40,14 +41,14 @@ Import uPred.
Lemma ownSP_ownSP sσ sσ': (ownSP sσ ★ ownSP sσ') ⊢ False.
Proof.
rewrite /ownSP /master_own_exact.
rewrite ?affine_elim.
rewrite !bi.affinely_elim.
rewrite ?sep_exist_r. apply exist_elim=> ts.
rewrite ?sep_exist_r. apply exist_elim=> cs.
rewrite ?sep_exist_r. apply exist_elim=> ixs.
rewrite ?sep_exist_l. apply exist_elim=> ts'.
rewrite ?sep_exist_l. apply exist_elim=> cs'.
rewrite ?sep_exist_l. apply exist_elim=> ixs'.
rewrite -owne_op owne_valid affine_elim. apply valid_elim.
rewrite -owne_op owne_valid bi.affinely_elim. apply valid_elim.
inversion 1 as (_&_&Hdisj).
inversion Hdisj.
Qed.
......@@ -66,40 +67,41 @@ Proof.
rewrite ?sep_exist_l. apply exist_elim=> c'.
rewrite ?sep_exist_l. apply exist_elim=> cs'.
rewrite ?sep_exist_l. apply exist_elim=> ixs'.
rewrite ?sep_elim_r.
iIntros "((_&H1)&(_&H2))".
iCombine "H1" "H2" as "H".
rewrite -ownle_op ownle_valid_l.
rewrite valid_elim. rewrite affine_elim. rewrite sep_False; auto.
inversion 1 as (_&_&Hdisj).
inversion Hdisj as [?????? Hdisj' | |]. clear -Hdisj'. set_solver.
- intros Hneq. rewrite pure_equiv //= -emp_True ?left_id //=.
rewrite valid_elim.
* iDestruct "H" as "(%&?)". done.
* inversion 1 as (_&_&Hdisj).
inversion Hdisj as [?????? Hdisj' | |]. clear -Hdisj'. set_solver.
- intros Hneq. iIntros "(H1&H2)". iFrame. iPureIntro. done.
Qed.
Lemma ownT_ownSP_step_nofork N' E i e sσ e' sσ':
nsteps (prim_step_nofork sΛ) N' (e, sσ) (e', sσ') →
(1 ≤ N' ∧ N' ≤ Kd) →
(ownT i e ★ ownSP sσ) ⊢ |={E}=>> ownT i e' ★ ownSP sσ'.
(ownT i e ★ ownSP sσ) ⊢ (|={E}=>> ownT i e' ★ ownSP sσ').
Proof.
iIntros (Hnsteps Hbound).
iIntros "(Hown1&Hown2)".
rewrite /ownT /ownSP.
iDestruct "Hown1" as (c cs ixs) "(%&Hown1)".
rewrite ?affine_exist. iDestruct "Hown2" as (ts') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (cs') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (ixs') "Hown2".
rewrite bi.affinely_exist. iDestruct "Hown2" as (ts') "Hown2".
rewrite bi.affinely_exist. iDestruct "Hown2" as (cs') "Hown2".
rewrite bi.affinely_exist. iDestruct "Hown2" as (ixs') "Hown2".
destruct c as (ts&sσ0).
efeed pose proof (owne_stepP refine_alt_triv) as Hshift0.
{ eapply snap_master_stepshift_nofork; eauto. }
iPoseProof Hshift0 as "Hshift".
- rewrite (affine_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
- rewrite (bi.affinely_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
iPsvs ("Hshift" with "Hown").
iDestruct "~" as (r' rl') "(%&Hownr&Hownrl)".
iDestruct "Hshift" as (r' rl') "(%&Hownr&Hownrl)".
destruct H1 as (cs''&ts''&ixs''&Hnth_error''&Hr'_equiv&Hrl'_equiv).
rewrite Hr'_equiv. rewrite Hrl'_equiv.
iPvsIntro.
iSplitL "Hownrl".
* iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl"; auto.
* iExists ts''. apply affine_intro; first apply _.
iSplitR "Hownrl"; auto.
* iExists ts''. iAlways.
iExists cs'', ixs''; auto.
Qed.
......@@ -150,21 +152,20 @@ Proof.
efeed pose proof (owne_stepP refine_alt_triv) as Hshift0.
{ eapply snap_master_simple_fork; eauto using refine_Knz. }
iPoseProof Hshift0 as "Hshift"; eauto.
- rewrite (affine_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
- rewrite (affinely_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
iPsvs ("Hshift" with "Hown").
iDestruct "~" as (r' rl') "(%&Hownr&Hownrl)".
iDestruct "Hshift" as (r' rl') "(%&Hownr&Hownrl)".
destruct H1 as (i'&cs''&ts''&ixs''&Hnth_error''&Hnth_error2''&Hr'_equiv&Hrl'_equiv).
rewrite Hr'_equiv. rewrite Hrl'_equiv.
rewrite ownle_op. iDestruct "Hownrl" as "(Hownrl1&Hownrl2)".
iPvsIntro.
iExists i'.
iSplitL "Hownrl1".
* iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl1"; auto.
iSplitR "Hownrl1"; auto.
* iSplitL "Hownrl2".
** iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl2"; auto.
** apply affine_intro; first apply _. iExists ts'', cs'', ixs''; auto.
iSplitR "Hownrl2"; auto.
** iAlways. iExists ts'', cs'', ixs''; auto.
Qed.
Lemma ownT_ownSP_step_fork_ctx `{LanguageCtx sΛ K} E i e sσ e' sσ' ef:
......@@ -174,6 +175,15 @@ Proof.
intros Hprim. eapply ownT_ownSP_step_fork; eauto using fill_step.
Qed.
Lemma own_value_stopped P V ES sσ' k:
nth_error ES k = Some (of_val V) →
(snapshot_ownl _ _ {[k]} (ES, sσ') ★ ⧆ P) ⊢ uPred_stopped.
Proof.
intros. rewrite -?uPred_affine_bi_affinely. eapply own_value_stopped.
- apply (refine_Knz).
- eauto.
Qed.
Lemma ownT_val_stopped i v P:
(ownT i (of_val v) ★ ⧆P) ⊢ uPred_stopped.
Proof.
......@@ -182,14 +192,10 @@ Proof.
rewrite sep_exist_r. apply exist_elim=> cs.
rewrite sep_exist_r. apply exist_elim=> ixs.
rewrite -assoc.
apply pure_elim_sep_l=>Hnth.
destruct V.
etransitivity; last eapply own_value_stopped; eauto.
- rewrite /snapshot_ownl.
rewrite -(exist_intro cs).
rewrite -(exist_intro ixs).
eauto.
- eapply (refine_Knz).
iIntros "(%&?&?)".
iApply own_value_stopped; eauto. iFrame.
by iExists cs, ixs.
Qed.
End refine_lemmas.
......@@ -214,16 +220,15 @@ Lemma init_ownT E σ:
Proof.
rewrite /ownT. iIntros "H1". iExists ([E], σ). iExists ([]). iExists [].
rewrite ownle_eq. iFrame "H1".
rewrite pure_equiv //= -emp_True; auto.
by iPureIntro.
Qed.
Lemma init_ownSP E σ:
ownG (to_globalFe (refine sΛ Kd master ∅ ([([E], σ)]) []))
⊢ ownSP σ.
Proof.
rewrite /ownSP. iIntros "H1". apply affine_intro; first apply _.
iExists [E]. iExists ([]). iExists [].
rewrite owne_eq // app_nil_l.
rewrite /ownSP. iIntros "H1". iAlways.
iExists [E], ([]), []. rewrite owne_eq // app_nil_l.
Qed.
......@@ -244,11 +249,10 @@ Proof.
rewrite Hht; apply ht_mono.
- repeat apply sep_mono; auto.
* rewrite /ownT /snapshot_ownl_exact.
rewrite -(exist_intro ([E], sσ)) -(exist_intro []) -(exist_intro []).
rewrite (pure_equiv) //= -emp_True left_id //=.
* rewrite /ownSP /master_own_exact.
apply affine_intro; first apply _.
rewrite -(exist_intro ([E])) -(exist_intro []) -(exist_intro []) //=.
iIntros "H". iExists ([E], sσ), [], [].
iFrame; by iPureIntro.
* rewrite /ownSP /master_own_exact. iIntros.
iAlways. by iExists [E], [], [].
- intros v'.
rewrite /ownT /snapshot_ownl.
apply exist_elim=> V.
......@@ -256,12 +260,13 @@ Proof.
rewrite sep_exist_r. apply exist_elim=> cs.
rewrite sep_exist_r. apply exist_elim=> ixs.
rewrite -assoc.
apply pure_elim_sep_l=>Hnth.
iIntros "(Hp&H1&H2)".
iDestruct "Hp" as %Hnth.
destruct c as (ts&sσ').
destruct ts as [| t ts']; simpl in Hnth; first congruence.
inversion Hnth; subst.
rewrite -(exist_intro V) -(exist_intro ts') -(exist_intro sσ').
rewrite -(exist_intro cs) -(exist_intro ixs) //=.
iExists V, ts', sσ'. iFrame.
by iExists cs, ixs.
Qed.
(* Adequacy theorem for diverging executions of target expression *)
......@@ -277,11 +282,10 @@ Proof.
rewrite Hht; apply ht_mono.
- repeat apply sep_mono; auto.
* rewrite /ownT /snapshot_ownl_exact.
rewrite -(exist_intro ([E], sσ)) -(exist_intro []) -(exist_intro []).
rewrite (pure_equiv) //= -emp_True left_id //=.
* rewrite /ownSP /master_own_exact.
apply affine_intro; first apply _.
rewrite -(exist_intro ([E])) -(exist_intro []) -(exist_intro []) //=.
iIntros "H". iExists ([E], sσ), [], [].
iFrame; by iPureIntro.
* rewrite /ownSP /master_own_exact. iIntros.
iAlways. by iExists [E], [], [].
- intros v'.
rewrite /ownT /snapshot_ownl.
apply exist_elim=> V.
......@@ -289,12 +293,13 @@ Proof.
rewrite sep_exist_r. apply exist_elim=> cs.
rewrite sep_exist_r. apply exist_elim=> ixs.
rewrite -assoc.
apply pure_elim_sep_l=>Hnth.
iIntros "(Hp&H1&H2)".
iDestruct "Hp" as %Hnth.
destruct c as (ts&sσ').
destruct ts as [| t ts']; simpl in Hnth; first congruence.
inversion Hnth; subst.
rewrite -(exist_intro V) -(exist_intro ts') -(exist_intro sσ').
rewrite -(exist_intro cs) -(exist_intro ixs) //=.
iExists V, ts', sσ'. iFrame.
by iExists cs, ixs.
Qed.
(* Bundle previous 2 results + safety result from adequacy.v to get safe refinement: *)
......
theories/program_logic/refine_ectx.v
View file @ 274019f4
From fri.algebra Require Import dra cmra_tactics.
From fri.algebra Require Import upred dra cmra_tactics.
From fri.program_logic Require Import
language ectx_language wsat refine_raw refine_raw_adequacy hoare ownership.
From fri.proofmode Require Import pviewshifts pstepshifts invariants.
From iris.proofmode Require Import tactics.
Import uPred.
(* A cleaner version of results about the refinement monoid. The
......@@ -29,8 +30,8 @@ Require fri.program_logic.refine.
(* Asserts ownership of physical state sσ in source language *)
Definition ownSP (sσ: state) := refine.ownSP _ sσ.
Instance ownSP_affine sσ: AffineP (ownSP sσ). apply _. Qed.
Instance ownSP_atimeless sσ: ATimelessP (ownSP sσ). apply _. Qed.
Instance ownSP_affine sσ: Affine (ownSP sσ). apply _. Qed.
Instance ownSP_atimeless sσ: ATimeless (ownSP sσ). apply _. Qed.
(* Ownership of thread i executing expression e *)
Definition ownT (i: nat) (e: expr) (K: ectx):=
......
theories/program_logic/refine_ectx_delay.v
View file @ 274019f4
From fri.algebra Require Import dra cmra_tactics.
From fri.algebra Require Import upred dra cmra_tactics.
From fri.program_logic Require Import
language nat_delayed_language ectx_language wsat refine_raw refine_raw_adequacy
hoare ownership.
From fri.proofmode Require Import pviewshifts pstepshifts invariants.
From iris.proofmode Require Import tactics.
Import uPred.
(* A version of refine_ectx bundled with the delayed language so that
......@@ -23,8 +24,8 @@ Require fri.program_logic.refine.
(* Asserts ownership of physical state sσ in source language *)
Definition ownSP (sσ: delayed_state _) := refine.ownSP _ sσ.
Instance ownSP_affine sσ: AffineP (ownSP sσ). apply _. Qed.
Instance ownSP_atimeless sσ: ATimelessP (ownSP sσ). apply _. Qed.
Instance ownSP_affine sσ: Affine (ownSP sσ). apply _. Qed.
Instance ownSP_atimeless sσ: ATimeless (ownSP sσ). apply _. Qed.
(* Ownership of thread i executing expression e in ectx K with d delay steps remaining *)
Definition ownT (i: nat) (e: expr) (K: ectx) (d: nat):=
......@@ -211,22 +212,21 @@ Proof.
**** replace (S k + d') with (S (k + d')); last omega.
eapply nsteps_l; last eapply IHk.
econstructor; auto.
** rewrite (affine_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
** rewrite (affinely_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
iPsvs ("Hshift" with "Hown").
iDestruct "~" as (r' rl') "(%&Hownr&Hownrl)".
iDestruct "Hshift" as (r' rl') "(%&Hownr&Hownrl)".
destruct H1 as (i'&cs''&ts''&ixs''&Hnth_error''&Hnth_error2''&Hr'_equiv&Hrl'_equiv).
rewrite Hr'_equiv. rewrite Hrl'_equiv.
rewrite ownle_op. iDestruct "Hownrl" as "(Hownrl1&Hownrl2)".
iPvsIntro.
iExists i'.
iSplitL "Hownrl1".
*** iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl1"; auto.
iSplitR "Hownrl1"; auto.
*** iSplitL "Hownrl2".
**** iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl2"; auto.
rewrite fill_empty pure_equiv //= -emp_True; auto.
**** apply affine_intro; first apply _. iExists ts'', cs'', ixs''; auto.
iSplitR "Hownrl2"; auto.
iPureIntro; rewrite fill_empty //=.
**** iAlways. iExists ts'', cs'', ixs''; auto.
Qed.
Lemma ownT_ownSP_delay E i e K d d' sσ:
......
theories/program_logic/refine_raw_adequacy.v
View file @ 274019f4
......@@ -2424,7 +2424,8 @@ threads. then, argue that this means all threads are stopped using step_block_or
as [r' (Hr'&?)]; rewrite ?right_id_L; auto.
{ rewrite map_length. split; omega. }
{ set_solver. }
destruct Hr' as (V&ES&sσ'&(r1&r2&?rl1&rl2&Heqr&Heqrl&Hownl&(HΦ&Haff))).
move: Hr'. uPred.unseal => Hr'.
destruct Hr' as (V&ES&sσ'&(r1&r2&?rl1&rl2&Heqr&Heqrl&Hownl&(Haff&HΦ))).
rewrite Haff ?right_id in Heqrl *=>Heqrl.
rewrite -Heqrl /snapshot_ownl in Hownl *. uPred.unseal.
intros (cfg1&idxs1 &Hownl%ownle_interp_extract); simpl in *; auto.
......@@ -2977,6 +2978,8 @@ threads. then, argue that this means all threads are stopped using step_block_or
apply uPred.exist_elim=>V.
apply uPred.exist_elim=>Es.
apply uPred.exist_elim=>sσ'.
rewrite /snapshot_ownl.
rewrite -uPred_affine_bi_affinely.
eapply (own_value_stopped (Φ v V)); eauto.
- (* I need to show fairness preserving is transitive, then we need to show
......
theories/program_logic/sts.v
View file @ 274019f4
From fri.algebra Require Export sts upred_tactics.
From fri.program_logic Require Export invariants ghost_ownership.
From fri.proofmode Require Import invariants ghost_ownership pstepshifts.
From iris.proofmode Require Import tactics.
Import uPred.
(** The CMRA we need. *)
......@@ -35,11 +35,11 @@ Section definitions.
Proof. solve_proper. Qed.
Global Instance sts_ownS_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) sts_ownS.
Proof. solve_proper. Qed.