Commit dd0a95de by David Swasey

### Use `stuck e σ` rather than `¬ progressive e σ`.

parent 10c5a51c
 ... ... @@ -40,7 +40,7 @@ Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) (φ : val adequate_safe t2 σ2 e2 : s = not_stuck → rtc step ([e1], σ1) (t2, σ2) → e2 ∈ t2 → progressive e2 σ2 e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2) }. Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ : ... ... @@ -133,7 +133,7 @@ Proof. Qed. Lemma wp_safe E e σ Φ : world' E σ -∗ WP e @ E {{ Φ }} ==∗ ▷ ⌜progressive e σ⌝. world' E σ -∗ WP e @ E {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝. Proof. rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H". destruct (to_val e) as [v|] eqn:?. ... ... @@ -145,7 +145,7 @@ Qed. Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 → world σ1 ∗ WP e1 {{ Φ }} ∗ wptp not_stuck t1 ⊢ ▷^(S (S n)) ⌜progressive e2 σ2⌝. ⊢ ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝. Proof. intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono. iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq. ... ...
 ... ... @@ -100,8 +100,8 @@ Section ectx_language. ∃ e' σ' efs, head_step e σ e' σ' efs. Definition head_irreducible (e : expr Λ) (σ : state Λ) := ∀ e' σ' efs, ¬head_step e σ e' σ' efs. Definition head_progressive (e : expr Λ) (σ : state Λ) := is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ. Definition head_stuck (e : expr Λ) (σ : state Λ) := to_val e = None ∧ ∀ K e', e = fill K e' → head_irreducible e' σ. (* All non-value redexes are at the root. In other words, all sub-redexes are values. *) ... ... @@ -165,12 +165,12 @@ Section ectx_language. rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible. Qed. Lemma progressive_head_progressive e σ : progressive e σ → head_progressive e σ. Lemma head_stuck_stuck e σ : head_stuck e σ → sub_redexes_are_values e → stuck e σ. Proof. case=>[?|Hred]; first by left. right. move: Hred=> [] e' [] σ' [] efs [] K e1' e2' EQ EQ' Hstep. subst. exists K, e1'. split; first done. by exists e2', σ', efs. move=>[] ? Hirr ?. split; first done. apply prim_head_irreducible; last done. apply (Hirr empty_ectx). by rewrite fill_empty. Qed. Lemma ectx_language_atomic s e : ... ...
 ... ... @@ -12,7 +12,7 @@ Implicit Types v : val Λ. Implicit Types e : expr Λ. Hint Resolve head_prim_reducible head_reducible_prim_step. Hint Resolve (reducible_not_val _ inhabitant). Hint Resolve progressive_head_progressive. Hint Resolve head_stuck_stuck. Lemma wp_lift_head_step {s E Φ} e1 : to_val e1 = None → ... ... @@ -30,11 +30,12 @@ Qed. Lemma wp_lift_head_stuck E Φ e : to_val e = None → (∀ σ, state_interp σ ={E,∅}=∗ ⌜¬ head_progressive e σ⌝) sub_redexes_are_values e → (∀ σ, state_interp σ ={E,∅}=∗ ⌜head_stuck e σ⌝) ⊢ WP e @ E ?{{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_stuck; first done. iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto. iIntros (??) "H". iApply wp_lift_stuck; first done. iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto. Qed. Lemma wp_lift_pure_head_step {s E E' Φ} e1 : ... ... @@ -52,13 +53,13 @@ Qed. Lemma wp_lift_pure_head_stuck E Φ e : to_val e = None → (∀ K e1 σ1 e2 σ2 efs, e = fill K e1 → ¬ head_step e1 σ1 e2 σ2 efs) → sub_redexes_are_values e → (∀ σ, head_stuck e σ) → WP e @ E ?{{ Φ }}%I. Proof using Hinh. iIntros (Hnv Hnstep). iApply wp_lift_head_stuck; first done. iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|]. iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver. iModIntro. iPureIntro. case; first by rewrite Hnv; case. move=>[] K [] e1 [] Hfill [] e2 [] σ2 [] efs /= Hstep. exact: Hnstep. by auto. Qed. Lemma wp_lift_atomic_head_step {s E Φ} e1 : ... ...
 ... ... @@ -83,8 +83,8 @@ Section language. ∃ e' σ' efs, prim_step e σ e' σ' efs. Definition irreducible (e : expr Λ) (σ : state Λ) := ∀ e' σ' efs, ¬prim_step e σ e' σ' efs. Definition progressive (e : expr Λ) (σ : state Λ) := is_Some (to_val e) ∨ reducible e σ. Definition stuck (e : expr Λ) (σ : state Λ) := to_val e = None ∧ irreducible e σ. (* [Atomic not_stuck]: This (weak) form of atomicity is enough to open invariants when WP ensures safety, i.e., programs never can get stuck. We have an example in ... ...
 ... ... @@ -26,13 +26,12 @@ Qed. Lemma wp_lift_stuck E Φ e : to_val e = None → (∀ σ, state_interp σ ={E,∅}=∗ ⌜¬ progressive e σ⌝) (∀ σ, state_interp σ ={E,∅}=∗ ⌜stuck e σ⌝) ⊢ WP e @ E ?{{ Φ }}. Proof. rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ". iMod ("H" with "Hσ") as "Hstuck". iDestruct "Hstuck" as %Hstuck. iModIntro. iSplit; first done. iIntros "!>" (e2 σ2 efs) "%". exfalso. apply Hstuck. right. by exists e2, σ2, efs. iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done. iIntros "!>" (e2 σ2 efs) "%". by case: (Hirr e2 σ2 efs). Qed. (** Derived lifting lemmas. *) ... ... @@ -53,12 +52,12 @@ Proof. Qed. Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e : (∀ σ, ¬ progressive e σ) → (∀ σ, stuck e σ) → True ⊢ WP e @ E ?{{ Φ }}. Proof. iIntros (Hstuck) "_". iApply wp_lift_stuck. - destruct(to_val e) as [v|] eqn:He; last done. exfalso. apply (Hstuck inhabitant). left. by exists v. rewrite -He. by case: (Hstuck inhabitant). - iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_". by set_solver. by auto. Qed. ... ...
 ... ... @@ -103,14 +103,14 @@ Section lifting. Qed. Lemma ownP_lift_stuck E Φ e : (|={E,∅}=> ∃ σ, ⌜¬ progressive e σ⌝ ∗ ▷ ownP σ) (|={E,∅}=> ∃ σ, ⌜stuck e σ⌝ ∗ ▷ ownP σ) ⊢ WP e @ E ?{{ Φ }}. Proof. iIntros "H". destruct (to_val e) as [v|] eqn:EQe. - apply of_to_val in EQe as <-; iApply fupd_wp. iMod "H" as (σ1) "[#H _]"; iDestruct "H" as %Hstuck; exfalso. by apply Hstuck; left; rewrite to_of_val; exists v. - iApply wp_lift_stuck; [done|]; iIntros (σ1) "Hσ". - apply of_to_val in EQe as <-. iApply fupd_wp. iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso. by rewrite to_of_val in Hnv. - iApply wp_lift_stuck; [done|]. iIntros (σ1) "Hσ". iMod "H" as (σ1') "(% & >Hσf)". by iDestruct (ownP_eq with "Hσ Hσf") as %->. Qed. ... ... @@ -201,7 +201,7 @@ Section ectx_lifting. Implicit Types e : expr Λ. Hint Resolve head_prim_reducible head_reducible_prim_step. Hint Resolve (reducible_not_val _ inhabitant). Hint Resolve progressive_head_progressive. Hint Resolve head_stuck_stuck. Lemma ownP_lift_head_step s E Φ e1 : to_val e1 = None → ... ... @@ -217,11 +217,12 @@ Section ectx_lifting. Qed. Lemma ownP_lift_head_stuck E Φ e : (|={E,∅}=> ∃ σ, ⌜¬ head_progressive e σ⌝ ∗ ▷ ownP σ) sub_redexes_are_values e → (|={E,∅}=> ∃ σ, ⌜head_stuck e σ⌝ ∗ ▷ ownP σ) ⊢ WP e @ E ?{{ Φ }}. Proof. iIntros "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]". iModIntro. iExists σ. iFrame "Hσ". by eauto. iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]". iExists σ. by auto. Qed. Lemma ownP_lift_pure_head_step s E Φ e1 : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!