Commit d0f42b2a by Robbert Krebbers

### Get rid of `irisG'`.

parent 2a806d70
 ... ... @@ -179,7 +179,7 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ : (|={⊤}=> ∃ (stateI : state Λ → list (observation Λ) → nat → iProp Σ) (fork_post : iProp Σ), let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in (* This could be strengthened so that φ also talks about the number of forked-off threads *) stateI σ κs 0 ∗ WP e @ s; ⊤ {{ v, ∀ σ m, stateI σ [] m ={⊤,∅}=∗ ⌜φ v σ⌝ }})%I) → ... ... @@ -190,19 +190,19 @@ Proof. eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S. iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]". iApply step_fupd_intro; first done. iModIntro. iApply (@wptp_result _ _ (IrisG _ _ _ Hinv stateI fork_post) with "[Hσ] [Hwp]"); eauto. iApply (@wptp_result _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] [Hwp]"); eauto. iApply (wp_wand with "Hwp"). iIntros (v) "H"; iIntros (σ'). iApply "H". - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?. eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S. iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]". iApply step_fupd_intro; first done. iModIntro. iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto. iApply (@wptp_safe _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto. Qed. Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ : (∀ `{Hinv : invG Σ} κs, (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ, let _ : irisG Λ Σ := IrisG _ _ _ Hinv (λ σ κs _, stateI σ κs) True%I in let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) True%I in stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) → adequate s e σ (λ v _, φ v). Proof. ... ... @@ -218,7 +218,7 @@ Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ : (|={⊤}=> ∃ (stateI : state Λ → list (observation Λ) → nat → iProp Σ) (fork_post : iProp Σ), let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v, let m := length vs in stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) → ... ... @@ -229,7 +229,7 @@ Proof. eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S. iMod Hwp as (stateI fork_post) "[Hσ Hwp]". iApply step_fupd_intro; first done. iModIntro. iApply (@wptp_all_result _ _ (IrisG _ _ _ Hinv stateI fork_post) iApply (@wptp_all_result _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] [Hwp]"); eauto. by rewrite right_id_L. Qed. ... ... @@ -238,7 +238,7 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ : (|={⊤}=> ∃ (stateI : state Λ → list (observation Λ) → nat → iProp Σ) (fork_post : iProp Σ), let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in stateI σ1 (κs ++ κs') 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 κs' (pred (length t2)) ={⊤,∅}=∗ ⌜φ⌝))%I) → rtc erased_step ([e], σ1) (t2, σ2) → ... ... @@ -248,7 +248,7 @@ Proof. apply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S. iMod (Hwp Hinv κs []) as (Istate fork_post) "(Hσ & Hwp & Hclose)". iApply step_fupd_intro; first done. iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate fork_post) iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate fork_post) with "Hclose [Hσ] [Hwp]"); eauto. Qed. ... ... @@ -259,7 +259,7 @@ Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ : (|={⊤}=> ∃ (stateI : state Λ → list (observation Λ) → nat → iProp Σ) (fork_post : iProp Σ), let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 κs' (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) → rtc erased_step ([e], σ1) (t2, σ2) → ... ...
 ... ... @@ -5,36 +5,34 @@ From iris.algebra Require Import auth. From iris.proofmode Require Import tactics classes. Set Default Proof Using "Type". Class ownPG' (Λstate Λobservation : Type) (Σ : gFunctors) := OwnPG { Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG { ownP_invG : invG Σ; ownP_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate)))); ownP_inG :> inG Σ (authR (optionUR (exclR (stateC Λ)))); ownP_name : gname; }. Notation ownPG Λ Σ := (ownPG' (state Λ) (observation Λ) Σ). Instance ownPG_irisG `{ownPG' Λstate Λobservation Σ} : irisG' Λstate Λobservation Σ := { Instance ownPG_irisG `{ownPG Λ Σ} : irisG Λ Σ := { iris_invG := ownP_invG; state_interp σ κs _ := (own ownP_name (● (Excl' (σ:leibnizC Λstate))))%I; state_interp σ κs _ := own ownP_name (● (Excl' σ))%I; fork_post := True%I; }. Global Opaque iris_invG. Definition ownPΣ (Λstate : Type) : gFunctors := Definition ownPΣ (Λ : language) : gFunctors := #[invΣ; GFunctor (authR (optionUR (exclR (leibnizC Λstate))))]. GFunctor (authR (optionUR (exclR (stateC Λ))))]. Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG { Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG { ownPPre_invG :> invPreG Σ; ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate)))) ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ)))) }. Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ). Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ → ownPPreG' Λstate Σ. Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ. Proof. solve_inG. Qed. (** Ownership *) Definition ownP `{ownPG' Λstate Λobservation Σ} (σ : Λstate) : iProp Σ := own ownP_name (◯ (Excl' (σ:leibnizC Λstate))). Definition ownP `{ownPG Λ Σ} (σ : state Λ) : iProp Σ := own ownP_name (◯ (Excl' σ)). Typeclasses Opaque ownP. Instance: Params (@ownP) 3. ... ... @@ -46,12 +44,10 @@ Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ : Proof. intros Hwp. apply (wp_adequacy Σ _). iIntros (? κs). iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]"; first done. iModIntro. iExists (λ σ κs, own γσ (● (Excl' (σ:leibnizC _))))%I. iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]"; first done. iModIntro. iExists (λ σ κs, own γσ (● (Excl' σ)))%I. iFrame "Hσ". iApply (Hwp (OwnPG _ _ _ _ _ γσ)). rewrite /ownP. iFrame. iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame. Qed. Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ : ... ... @@ -63,11 +59,10 @@ Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ : Proof. intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //. iIntros (? κs κs'). iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done. iExists (λ σ κs' _, own γσ (● (Excl' (σ:leibnizC _))))%I, True%I. iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done. iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, True%I. iFrame "Hσ". iMod (Hwp (OwnPG _ _ _ _ _ γσ) with "[Hσf]") as "[\$ H]"; iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[\$ H]"; first by rewrite /ownP; iFrame. iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP. iDestruct (own_valid_2 with "Hσ Hσf") ... ... @@ -90,7 +85,7 @@ Section lifting. Qed. Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False. Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed. Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) (observation Λ) Σ _ σ). Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ). Proof. rewrite /ownP; apply _. Qed. Lemma ownP_lift_step s E Φ e1 : ... ...
 ... ... @@ -63,8 +63,8 @@ Proof. iRevert (t1) "IH1"; iRevert (t2) "H2". iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1". rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ2 n Hstep) "Hσ1". destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' ?? Hstep]; simplify_eq/=. apply app_eq_inv in H as [(t&?&?)|(t&?&?)]; subst. destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' [=Ht ?] ? Hstep]; simplify_eq/=. apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst. - destruct t as [|e1' ?]; simplify_eq/=. + iMod ("IH2" with "[%] Hσ1") as (n2) "(\$ & Hσ & IH2 & _)". { by eapply step_atomic with (t1:=[]). } ... ... @@ -119,13 +119,13 @@ Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ : (|={⊤}=> ∃ (stateI : state Λ → list (observation Λ) → nat → iProp Σ) (fork_post : iProp Σ), let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }])%I) → sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *) Proof. intros Hwp. apply (soundness (M:=iResUR Σ) _ 2); simpl. apply (fupd_plain_soundness ⊤ _)=> Hinv. iMod (Hwp) as (stateI fork_post) "[Hσ H]". iApply (@twptp_total _ _ (IrisG _ _ _ Hinv stateI fork_post) with "Hσ"). by iApply (@twp_twptp _ _ (IrisG _ _ _ Hinv stateI fork_post)). iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ"). by iApply (@twp_twptp _ _ (IrisG _ _ Hinv stateI fork_post)). Qed.
 ... ... @@ -5,7 +5,7 @@ From iris.proofmode Require Import base tactics classes. Set Default Proof Using "Type". Import uPred. Class irisG' (Λstate Λobservation : Type) (Σ : gFunctors) := IrisG { Class irisG (Λ : language) (Σ : gFunctors) := IrisG { iris_invG :> invG Σ; (** The state interpretation is an invariant that should hold in between each ... ... @@ -13,14 +13,13 @@ Class irisG' (Λstate Λobservation : Type) (Σ : gFunctors) := IrisG { the remaining observations, and [nat] is the number of forked-off threads (not the total number of threads, which is one higher because there is always a main thread). *) state_interp : Λstate → list Λobservation → nat → iProp Σ; state_interp : state Λ → list (observation Λ) → nat → iProp Σ; (** A fixed postcondition for any forked-off thread. For most languages, e.g. heap_lang, this will simply be [True]. However, it is useful if one wants to keep track of resources precisely, as in e.g. Iron. *) fork_post : iProp Σ; }. Notation irisG Λ Σ := (irisG' (state Λ) (observation Λ) Σ). Global Opaque iris_invG. Definition wp_pre `{irisG Λ Σ} (s : stuckness) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!