Commit 815412f8 by David Swasey

### Generalize basic heap_lang proof rules for progress bits.

parent 1847520d
 ... ... @@ -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 Σ} e σ φ : (∀ `{heapG Σ}, WP e {{ v, ⌜φ v⌝ }}%I) → adequate progress e σ φ. Definition heap_adequacy Σ `{heapPreG Σ} p e σ φ : (∀ `{heapG Σ}, WP e @ p; ⊤ {{ v, ⌜φ v⌝ }}%I) → adequate p e σ φ. Proof. intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "". iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh". ... ...
 ... ... @@ -47,7 +47,7 @@ Ltac inv_head_step := inversion H; subst; clear H end. Local Hint Extern 0 (atomic _) => solve_atomic. Local Hint Extern 0 (strongly_atomic _) => solve_atomic. Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl. Local Hint Constructors head_step. ... ... @@ -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 {E e} K Φ : WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. 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 {{ Φ }}. Proof. exact: wp_ectx_bind. Qed. Lemma wp_bindi {E e} Ki Φ : WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢ WP fill_item Ki e @ E {{ Φ }}. 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 {{ Φ }}. Proof. exact: weakestpre.wp_bind. Qed. (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e Φ : ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. Lemma wp_fork p E e Φ : ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ p; ⊤ {{ _, True }} ⊢ WP Fork e @ p; 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 E e v : Lemma wp_alloc p E e v : IntoVal e v → {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}. {{{ True }}} Alloc e @ p; 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 E l q v : {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l ↦{q} v }}}. Lemma wp_load p E l q v : {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ p; 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 E l v' e v : Lemma wp_store p E l v' e v : IntoVal e v → {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}. {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ p; 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 E l q v' e1 v1 e2 : Lemma wp_cas_fail p E l q v' e1 v1 e2 : IntoVal e1 v1 → AsVal e2 → v' ≠ v1 → {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ p; 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 E l e1 v1 e2 v2 : Lemma wp_cas_suc p E l e1 v1 e2 v2 : IntoVal e1 v1 → IntoVal e2 v2 → {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ p; 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 Δ Δ' E e1 e2 φ Φ : Lemma tac_wp_pure `{heapG Σ} K Δ Δ' p E e1 e2 φ Φ : PureExec φ e1 e2 → φ → IntoLaterNEnvs 1 Δ Δ' → envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) → envs_entails Δ (WP fill K e1 @ E {{ Φ }}). envs_entails Δ' (WP fill K e2 @ p; E {{ Φ }}) → envs_entails Δ (WP fill K e1 @ p; 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 Σ} Δ E Φ e v : Lemma tac_wp_value `{heapG Σ} Δ p E Φ e v : IntoVal e v → envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}). envs_entails Δ (Φ v) → envs_entails Δ (WP e @ p; 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 progress ?E ?e ?Q) => reshape_expr e ltac:(fun K e' => | |- envs_entails _ (wp ?p ?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 Δ E Φ e : envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I → envs_entails Δ (WP fill K e @ E {{ Φ }}). 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 {{ Φ }}). 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 progress ?E ?e ?Q) => | |- envs_entails _ (wp ?p ?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 Δ Δ' E j K e v Φ : Lemma tac_wp_alloc Δ Δ' p 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)) @ E {{ Φ }})) → envs_entails Δ (WP fill K (Alloc e) @ E {{ Φ }}). envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ p; E {{ Φ }})) → envs_entails Δ (WP fill K (Alloc e) @ p; 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 Δ Δ' E i K l q v Φ : Lemma tac_wp_load Δ Δ' p 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) @ E {{ Φ }}) → envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}). envs_entails Δ' (WP fill K (of_val v) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ p; 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 Δ Δ' Δ'' E i K l v e v' Φ : Lemma tac_wp_store Δ Δ' Δ'' p 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) @ E {{ Φ }}) → envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}). envs_entails Δ'' (WP fill K (Lit LitUnit) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ p; 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 Δ Δ' E i K l q v e1 v1 e2 Φ : Lemma tac_wp_cas_fail Δ Δ' p 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)) @ E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}). envs_entails Δ' (WP fill K (Lit (LitBool false)) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ p; 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 Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_suc Δ Δ' Δ'' p 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)) @ E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}). envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ p; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ p; 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 progress ?E ?e ?Q) => | |- envs_entails _ (wp ?p ?E ?e ?Q) => reshape_expr e ltac:(fun K e' => wp_bind_core K; iApplyHyp H; try iNext; simpl) || lazymatch iTypeOf H with ... ... @@ -163,10 +163,10 @@ Tactic Notation "wp_apply" open_constr(lem) := Tactic Notation "wp_alloc" ident(l) "as" constr(H) := iStartProof; lazymatch goal with | |- envs_entails _ (wp progress ?E ?e ?Q) => | |- envs_entails _ (wp ?p ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ H K); [apply _|..]) eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..]) |fail 1 "wp_alloc: cannot find 'Alloc' in" e]; [apply _ |first [intros l | fail 1 "wp_alloc:" l "not fresh"]; ... ... @@ -182,9 +182,9 @@ Tactic Notation "wp_alloc" ident(l) := Tactic Notation "wp_load" := iStartProof; lazymatch goal with | |- envs_entails _ (wp progress ?E ?e ?Q) => | |- envs_entails _ (wp ?p ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K)) [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K)) |fail 1 "wp_load: cannot find 'Load' in" e]; [apply _ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in ... ... @@ -196,10 +196,10 @@ Tactic Notation "wp_load" := Tactic Notation "wp_store" := iStartProof; lazymatch goal with | |- envs_entails _ (wp progress ?E ?e ?Q) => | |- envs_entails _ (wp ?p ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ K); [apply _|..]) eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..]) |fail 1 "wp_store: cannot find 'Store' in" e]; [apply _ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in ... ... @@ -212,10 +212,10 @@ Tactic Notation "wp_store" := Tactic Notation "wp_cas_fail" := iStartProof; lazymatch goal with | |- envs_entails _ (wp progress ?E ?e ?Q) => | |- envs_entails _ (wp ?p ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..]) eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..]) |fail 1 "wp_cas_fail: cannot find 'CAS' in" e]; [apply _ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in ... ... @@ -228,10 +228,10 @@ Tactic Notation "wp_cas_fail" := Tactic Notation "wp_cas_suc" := iStartProof; lazymatch goal with | |- envs_entails _ (wp progress ?E ?e ?Q) => | |- envs_entails _ (wp ?p ?E ?e ?Q) => first [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..]) eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..]) |fail 1 "wp_cas_suc: cannot find 'CAS' in" e]; [apply _ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in ... ...
 ... ... @@ -187,9 +187,9 @@ Definition is_atomic (e : expr) := | App (Rec _ _ (Lit _)) (Lit _) => true | _ => false end. Lemma is_atomic_correct e : is_atomic e → Atomic (to_expr e). Lemma is_atomic_correct e : is_atomic e → StronglyAtomic (to_expr e). Proof. intros He. apply strongly_atomic_atomic, ectx_language_strong_atomic. intros He. apply ectx_language_strong_atomic. - intros σ e' σ' ef Hstep; simpl in *. revert Hstep. destruct e=> //=; repeat (simplify_eq/=; case_match=>//); inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. ... ... @@ -226,10 +226,14 @@ Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances. Ltac solve_atomic := match goal with | |- StronglyAtomic ?e => let e' := W.of_expr e in change (StronglyAtomic (W.to_expr e')); apply W.is_atomic_correct; vm_compute; exact I | |- Atomic ?e => let e' := W.of_expr e in change (Atomic (W.to_expr e')); apply W.is_atomic_correct; vm_compute; exact I apply strongly_atomic_atomic, W.is_atomic_correct; vm_compute; exact I end. Hint Extern 10 (StronglyAtomic _) => solve_atomic : typeclass_instances. Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances. (** Substitution *) ... ...
 ... ... @@ -96,21 +96,23 @@ Proof. by iIntros (e' efs' σ (_&->&->)%Hpuredet). Qed. Lemma wp_pure_step_fupd `{Inhabited (state Λ)} E E' e1 e2 φ Φ : Lemma wp_pure_step_fupd `{Inhabited (state Λ)} p E E' e1 e2 φ Φ : PureExec φ e1 e2 → φ → (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}. (|={E,E'}▷=> WP e2 @ p; E {{ Φ }}) ⊢ WP e1 @ p; E {{ Φ }}. Proof. iIntros ([??] Hφ) "HWP". iApply (wp_lift_pure_det_step with "[HWP]"); [|naive_solver|naive_solver|]. iApply (wp_lift_pure_det_step with "[HWP]"). - apply (reducible_not_val _ inhabitant). by auto. - destruct p; naive_solver. - naive_solver. - by rewrite big_sepL_nil right_id. Qed. Lemma wp_pure_step_later `{Inhabited (state Λ)} E e1 e2 φ Φ : Lemma wp_pure_step_later `{Inhabited (state Λ)} p E e1 e2 φ Φ : PureExec φ e1 e2 → φ → ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}. ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}. Proof. intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //. Qed. ... ...
Supports Markdown
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