Commit 3a991bae by David Swasey

### Rename pbit, progress, noprogress to stuckness, not_stuck, maybe_stuck.

parent b3eb5903
 ... ... @@ -14,9 +14,9 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val]. Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ. Proof. solve_inG. Qed. Definition heap_adequacy Σ `{heapPreG Σ} p e σ φ : (∀ `{heapG Σ}, WP e @ p; ⊤ {{ v, ⌜φ v⌝ }}%I) → adequate p e σ φ. Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ : (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) → adequate s e σ φ. Proof. intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "". iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh". ... ...
 ... ... @@ -62,18 +62,18 @@ Implicit Types efs : list expr. Implicit Types σ : state. (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *) Lemma wp_bind {p E e} K Φ : WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill K e @ p; E {{ Φ }}. Lemma wp_bind {s E e} K Φ : WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }} ⊢ WP fill K e @ s; E {{ Φ }}. Proof. exact: wp_ectx_bind. Qed. Lemma wp_bindi {p E e} Ki Φ : WP e @ p; E {{ v, WP fill_item Ki (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill_item Ki e @ p; E {{ Φ }}. Lemma wp_bindi {s E e} Ki Φ : WP e @ s; E {{ v, WP fill_item Ki (of_val v) @ s; E {{ Φ }} }} ⊢ WP fill_item Ki e @ s; E {{ Φ }}. Proof. exact: weakestpre.wp_bind. Qed. (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork p E e Φ : ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ p; ⊤ {{ _, True }} ⊢ WP Fork e @ p; E {{ Φ }}. Lemma wp_fork s E e Φ : ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto. - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id. ... ... @@ -132,9 +132,9 @@ Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} : Proof. solve_pure_exec. Qed. (** Heap *) Lemma wp_alloc p E e v : Lemma wp_alloc s E e v : IntoVal e v → {{{ True }}} Alloc e @ p; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}. {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}. Proof. iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (σ1) "Hσ !>"; iSplit; first by auto. ... ... @@ -143,8 +143,8 @@ Proof. iModIntro; iSplit=> //. iFrame. by iApply "HΦ". Qed. Lemma wp_load p E l q v : {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ p; E {{{ RET v; l ↦{q} v }}}. Lemma wp_load s E l q v : {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}. Proof. iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. ... ... @@ -153,9 +153,9 @@ Proof. iModIntro; iSplit=> //. iFrame. by iApply "HΦ". Qed. Lemma wp_store p E l v' e v : Lemma wp_store s E l v' e v : IntoVal e v → {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ p; E {{{ RET LitV LitUnit; l ↦ v }}}. {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l ↦ v }}}. Proof. iIntros (<-%of_to_val Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. ... ... @@ -165,9 +165,9 @@ Proof. iModIntro. iSplit=>//. by iApply "HΦ". Qed. Lemma wp_cas_fail p E l q v' e1 v1 e2 : Lemma wp_cas_fail s E l q v' e1 v1 e2 : IntoVal e1 v1 → AsVal e2 → v' ≠ v1 → {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ p; E {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E {{{ RET LitV (LitBool false); l ↦{q} v' }}}. Proof. iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) ">Hl HΦ". ... ... @@ -177,9 +177,9 @@ Proof. iModIntro; iSplit=> //. iFrame. by iApply "HΦ". Qed. Lemma wp_cas_suc p E l e1 v1 e2 v2 : Lemma wp_cas_suc s E l e1 v1 e2 v2 : IntoVal e1 v1 → IntoVal e2 v2 → {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ p; E {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E {{{ RET LitV (LitBool true); l ↦ v2 }}}. Proof. iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ". ... ...
 ... ... @@ -5,21 +5,21 @@ From iris.heap_lang Require Export tactics lifting. Set Default Proof Using "Type". Import uPred. Lemma tac_wp_pure `{heapG Σ} K Δ Δ' p E e1 e2 φ Φ : Lemma tac_wp_pure `{heapG Σ} K Δ Δ' s E e1 e2 φ Φ : PureExec φ e1 e2 → φ → IntoLaterNEnvs 1 Δ Δ' → envs_entails Δ' (WP fill K e2 @ p; E {{ Φ }}) → envs_entails Δ (WP fill K e1 @ p; E {{ Φ }}). envs_entails Δ' (WP fill K e2 @ s; E {{ Φ }}) → envs_entails Δ (WP fill K e1 @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=. rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //. by rewrite -ectx_lifting.wp_ectx_bind_inv. Qed. Lemma tac_wp_value `{heapG Σ} Δ p E Φ e v : Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v : IntoVal e v → envs_entails Δ (Φ v) → envs_entails Δ (WP e @ p; E {{ Φ }}). envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed. Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta]. ... ... @@ -27,7 +27,7 @@ Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta]. Tactic Notation "wp_pure" open_constr(efoc) := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => reshape_expr e ltac:(fun K e' => | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' => unify e' efoc; eapply (tac_wp_pure K); [simpl; apply _ (* PureExec *) ... ... @@ -52,9 +52,9 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _). Tactic Notation "wp_case" := wp_pure (Case _ _ _). Tactic Notation "wp_match" := wp_case; wp_let. Lemma tac_wp_bind `{heapG Σ} K Δ p E Φ e : envs_entails Δ (WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }})%I → envs_entails Δ (WP fill K e @ p; E {{ Φ }}). Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e : envs_entails Δ (WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }})%I → envs_entails Δ (WP fill K e @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed. Ltac wp_bind_core K := ... ... @@ -66,7 +66,7 @@ Ltac wp_bind_core K := Tactic Notation "wp_bind" open_constr(efoc) := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K) || fail "wp_bind: cannot find" efoc "in" e | _ => fail "wp_bind: not a 'wp'" ... ... @@ -79,13 +79,13 @@ Implicit Types P Q : iProp Σ. Implicit Types Φ : val → iProp Σ. Implicit Types Δ : envs (iResUR Σ). Lemma tac_wp_alloc Δ Δ' p E j K e v Φ : Lemma tac_wp_alloc Δ Δ' s E j K e v Φ : IntoVal e v → IntoLaterNEnvs 1 Δ Δ' → (∀ l, ∃ Δ'', envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧ envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ p; E {{ Φ }})) → envs_entails Δ (WP fill K (Alloc e) @ p; E {{ Φ }}). envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }})) → envs_entails Δ (WP fill K (Alloc e) @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc. ... ... @@ -94,11 +94,11 @@ Proof. by rewrite right_id HΔ'. Qed. Lemma tac_wp_load Δ Δ' p E i K l q v Φ : Lemma tac_wp_load Δ Δ' s E i K l q v Φ : IntoLaterNEnvs 1 Δ Δ' → envs_lookup i Δ' = Some (false, l ↦{q} v)%I → envs_entails Δ' (WP fill K (of_val v) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ p; E {{ Φ }}). envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ???. rewrite -wp_bind. eapply wand_apply; first exact: wp_load. ... ... @@ -106,13 +106,13 @@ Proof. by apply later_mono, sep_mono_r, wand_mono. Qed. Lemma tac_wp_store Δ Δ' Δ'' p E i K l v e v' Φ : Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ : IntoVal e v' → IntoLaterNEnvs 1 Δ Δ' → envs_lookup i Δ' = Some (false, l ↦ v)%I → envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' → envs_entails Δ'' (WP fill K (Lit LitUnit) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ p; E {{ Φ }}). envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ?????. rewrite -wp_bind. eapply wand_apply; first by eapply wp_store. ... ... @@ -120,12 +120,12 @@ Proof. rewrite right_id. by apply later_mono, sep_mono_r, wand_mono. Qed. Lemma tac_wp_cas_fail Δ Δ' p E i K l q v e1 v1 e2 Φ : Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ : IntoVal e1 v1 → AsVal e2 → IntoLaterNEnvs 1 Δ Δ' → envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 → envs_entails Δ' (WP fill K (Lit (LitBool false)) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ p; E {{ Φ }}). envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ??????. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail. ... ... @@ -133,13 +133,13 @@ Proof. by apply later_mono, sep_mono_r, wand_mono. Qed. Lemma tac_wp_cas_suc Δ Δ' Δ'' p E i K l v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ : IntoVal e1 v1 → IntoVal e2 v2 → IntoLaterNEnvs 1 Δ Δ' → envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 → envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' → envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ p; E {{ Φ }}). envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}). Proof. rewrite /envs_entails=> ???????; subst. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc. ... ... @@ -151,7 +151,7 @@ End heap. Tactic Notation "wp_apply" open_constr(lem) := iPoseProofCore lem as false true (fun H => lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' => wp_bind_core K; iApplyHyp H; try iNext; simpl) || lazymatch iTypeOf H with ... ... @@ -163,7 +163,7 @@ Tactic Notation "wp_apply" open_constr(lem) := Tactic Notation "wp_alloc" ident(l) "as" constr(H) := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..]) ... ... @@ -182,7 +182,7 @@ Tactic Notation "wp_alloc" ident(l) := Tactic Notation "wp_load" := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K)) |fail 1 "wp_load: cannot find 'Load' in" e]; ... ... @@ -196,7 +196,7 @@ Tactic Notation "wp_load" := Tactic Notation "wp_store" := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..]) ... ... @@ -212,7 +212,7 @@ Tactic Notation "wp_store" := Tactic Notation "wp_cas_fail" := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..]) ... ... @@ -228,7 +228,7 @@ Tactic Notation "wp_cas_fail" := Tactic Notation "wp_cas_suc" := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?p ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..]) ... ...
 ... ... @@ -34,24 +34,24 @@ Proof. Qed. (* Program logic adequacy *) Record adequate {Λ} (p : pbit) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := { Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := { adequate_result t2 σ2 v2 : rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2; adequate_safe t2 σ2 e2 : p = progress → s = not_stuck → rtc step ([e1], σ1) (t2, σ2) → e2 ∈ t2 → progressive e2 σ2 }. Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ : adequate progress e1 σ1 φ → adequate not_stuck e1 σ1 φ → rtc step ([e1], σ1) (t2, σ2) → Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3). Proof. intros Had ?. destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|]. apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2). destruct (adequate_safe progress e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)]; destruct (adequate_safe not_stuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)]; rewrite ?eq_None_not_Some; auto. { exfalso. eauto. } destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto. ... ... @@ -68,12 +68,12 @@ Implicit Types Φs : list (val Λ → iProp Σ). Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I (only parsing). Notation world σ := (world' ⊤ σ) (only parsing). Notation wptp p t := ([∗ list] ef ∈ t, WP ef @ p; ⊤ {{ _, True }})%I. Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I. Lemma wp_step p E e1 σ1 e2 σ2 efs Φ : Lemma wp_step s E e1 σ1 e2 σ2 efs Φ : prim_step e1 σ1 e2 σ2 efs → world' E σ1 ∗ WP e1 @ p; E {{ Φ }} ==∗ ▷ |==> ◇ (world' E σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ wptp p efs). world' E σ1 ∗ WP e1 @ s; E {{ Φ }} ==∗ ▷ |==> ◇ (world' E σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs). Proof. rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]". rewrite (val_stuck e1 σ1 e2 σ2 efs) // fupd_eq /fupd_def. ... ... @@ -82,10 +82,10 @@ Proof. iMod ("H" \$! e2 σ2 efs with "[%] [\$Hw \$HE]") as ">(\$ & \$ & \$ & \$)"; auto. Qed. Lemma wptp_step p e1 t1 t2 σ1 σ2 Φ : Lemma wptp_step s e1 t1 t2 σ1 σ2 Φ : step (e1 :: t1,σ1) (t2, σ2) → world σ1 ∗ WP e1 @ p; ⊤ {{ Φ }} ∗ wptp p t1 ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ p; ⊤ {{ Φ }} ∗ wptp p t2'). world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'). Proof. iIntros (Hstep) "(HW & He & Ht)". destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=. ... ... @@ -96,11 +96,11 @@ Proof. iApply wp_step; eauto with iFrame. Qed. Lemma wptp_steps p n e1 t1 t2 σ1 σ2 Φ : Lemma wptp_steps s n e1 t1 t2 σ1 σ2 Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → world σ1 ∗ WP e1 @ p; ⊤ {{ Φ }} ∗ wptp p t1 ⊢ world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢ Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 @ p; ⊤ {{ Φ }} ∗ wptp p t2'). ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'). Proof. revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=. { inversion_clear 1; iIntros "?"; eauto 10. } ... ... @@ -122,9 +122,9 @@ Proof. by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH. Qed. Lemma wptp_result p n e1 t1 v2 t2 σ1 σ2 φ : Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ : nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) → world σ1 ∗ WP e1 @ p; ⊤ {{ v, ⌜φ v⌝ }} ∗ wptp p t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝. world σ1 ∗ WP e1 @ s; ⊤ {{ v, ⌜φ v⌝ }} ∗ wptp s t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝. Proof. intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono. iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq. ... ... @@ -144,7 +144,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 progress t1 world σ1 ∗ WP e1 {{ Φ }} ∗ wptp not_stuck t1 ⊢ ▷^(S (S n)) ⌜progressive e2 σ2⌝. Proof. intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono. ... ... @@ -154,9 +154,9 @@ Proof. - iMod (wp_safe with "Hw [Htp]") as "\$". by iApply (big_sepL_elem_of with "Htp"). Qed. Lemma wptp_invariance p n e1 e2 t1 t2 σ1 σ2 φ Φ : Lemma wptp_invariance s n e1 e2 t1 t2 σ1 σ2 φ Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 @ p; ⊤ {{ Φ }} ∗ wptp p t1 (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢ ▷^(S (S n)) ⌜φ⌝. Proof. intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later. ... ... @@ -167,12 +167,12 @@ Proof. Qed. End adequacy. Theorem wp_adequacy Σ Λ `{invPreG Σ} p e σ φ : Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ : (∀ `{Hinv : invG Σ}, (|={⊤}=> ∃ stateI : state Λ → iProp Σ, let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in stateI σ ∗ WP e @ p; ⊤ {{ v, ⌜φ v⌝ }})%I) → adequate p e σ φ. stateI σ ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) → adequate s e σ φ. Proof. intros Hwp; split. - intros t2 σ2 v2 [n ?]%rtc_nsteps. ... ... @@ -181,7 +181,7 @@ Proof. rewrite fupd_eq in Hwp; iMod (Hwp with "[\$Hw \$HE]") as ">(Hw & HE & Hwp)". iDestruct "Hwp" as (Istate) "[HI Hwp]". iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame. - destruct p; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?. - destruct s; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?. eapply (soundness (M:=iResUR Σ) _ (S (S n))). iMod wsat_alloc as (Hinv) "[Hw HE]". rewrite fupd_eq in Hwp; iMod (Hwp with "[\$Hw \$HE]") as ">(Hw & HE & Hwp)". ... ... @@ -189,11 +189,11 @@ Proof. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame. Qed. Theorem wp_invariance Σ Λ `{invPreG Σ} p e σ1 t2 σ2 φ : Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ : (∀ `{Hinv : invG Σ}, (|={⊤}=> ∃ stateI : state Λ → iProp Σ, let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in stateI σ1 ∗ WP e @ p; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) → stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) → rtc step ([e], σ1) (t2, σ2) → φ. Proof. ... ...
 ... ... @@ -6,7 +6,7 @@ Set Default Proof Using "Type". Section wp. Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}. Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}. Implicit Types p : pbit. Implicit Types s : stuckness. Implicit Types P : iProp Σ. Implicit Types Φ : val → iProp Σ. Implicit Types v : val. ... ... @@ -15,27 +15,27 @@ Hint Resolve head_prim_reducible head_reducible_prim_step. Hint Resolve (reducible_not_val _ inhabitant). Hint Resolve progressive_head_progressive. Lemma wp_ectx_bind {p E e} K Φ : WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill K e @ p; E {{ Φ }}. Lemma wp_ectx_bind {s E e} K Φ : WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }} ⊢ WP fill K e @ s; E {{ Φ }}. Proof. apply: weakestpre.wp_bind. Qed. Lemma wp_ectx_bind_inv {p E Φ} K e : WP fill K e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}. Lemma wp_ectx_bind_inv {s E Φ} K e : WP fill K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }}. Proof. apply: weakestpre.wp_bind_inv. Qed. Lemma wp_lift_head_step {p E Φ} e1 : Lemma wp_lift_head_step {s E Φ} e1 : to_val e1 = None → (∀ σ1, state_interp σ1 ={E,∅}=∗ ⌜head_reducible e1 σ1⌝ ∗ ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗ state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }}) ⊢ WP e1 @ p; E {{ Φ }}. state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }}) ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[% H]"; iModIntro. iSplit; first by destruct p; eauto. iNext. iIntros (e2 σ2 efs) "%". iSplit; first by destruct s; eauto. iNext. iIntros (e2 σ2 efs) "%". iApply "H"; eauto. Qed. ... ... @@ -48,15 +48,15 @@ Proof. iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto. Qed. Lemma wp_lift_pure_head_step {p E E' Φ} e1 : Lemma wp_lift_pure_head_step {s E E' Φ} e1 : (∀ σ1, head_reducible e1 σ1) → (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) → (|={E,E'}▷=> ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ → WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }}) ⊢ WP e1 @ p; E {{ Φ }}. WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }}) ⊢ WP e1 @ s; E {{ Φ }}. Proof using Hinh. iIntros (??) "H". iApply wp_lift_pure_step; eauto. { by destruct p; auto. } { by destruct s; auto. } iApply (step_fupd_wand with "H"); iIntros "H". iIntros (????). iApply "H"; eauto. Qed. ... ... @@ -72,28 +72,28 @@ Proof using Hinh. move=>[] K [] e1 [] Hfill [] e2 [] σ2 [] efs /= Hstep. exact: Hnstep. Qed. Lemma wp_lift_atomic_head_step {p E Φ} e1 : Lemma wp_lift_atomic_head_step {s E Φ} e1 : to_val e1 = None → (∀ σ1, state_interp σ1 ={E}=∗ ⌜head_reducible e1 σ1⌝ ∗ ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗ state_interp σ2 ∗ default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }}) ⊢ WP e1 @ p; E {{ Φ }}. default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }}) ⊢ WP e1 @ s; E