Commit 4096ec43 authored by David Swasey's avatar David Swasey

Generalize basic heap_lang proof rules for progress bits.

parent 0ed2f614
......@@ -13,9 +13,9 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. intros [? ?]%subG_inv; split; apply _. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, True WP e {{ v, ⌜φ v }})
adequate progress e σ φ.
Definition heap_adequacy Σ `{heapPreG Σ} p e σ φ :
( `{heapG Σ}, True WP e @ p; {{ v, ⌜φ v }})
adequate p e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
......
......@@ -45,7 +45,7 @@ Ltac inv_head_step :=
inversion H; subst; clear H
end.
Local Hint Extern 0 (atomic _) => solve_atomic.
Local Hint Extern 0 (strong_atomic _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Constructors head_step.
......@@ -60,99 +60,99 @@ 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 later_sep -(wp_value _ _ _ (Lit _)) // big_sepL_singleton.
- intros; inv_head_step; eauto.
Qed.
Lemma wp_rec E f x erec e1 e2 Φ :
Lemma wp_rec p E f x erec e1 e2 Φ :
e1 = Rec f x erec
is_Some (to_val e2)
Closed (f :b: x :b: []) erec
WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
WP subst' x e2 (subst' f e1 erec) @ p; E {{ Φ }} WP App e1 e2 @ p; E {{ Φ }}.
Proof.
intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
(subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_un_op E op e v v' Φ :
Lemma wp_un_op p E op e v v' Φ :
to_val e = Some v
un_op_eval op v = Some v'
Φ v' WP UnOp op e @ E {{ Φ }}.
Φ v' WP UnOp op e @ p; E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (UnOp op _) (of_val v'))
-?wp_value'; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
Lemma wp_bin_op p E op e1 e2 v1 v2 v' Φ :
to_val e1 = Some v1 to_val e2 = Some v2
bin_op_eval op v1 v2 = Some v'
(Φ v') WP BinOp op e1 e2 @ E {{ Φ }}.
(Φ v') WP BinOp op e1 e2 @ p; E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val v'))
-?wp_value'; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_if_true E e1 e2 Φ :
WP e1 @ E {{ Φ }} WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Lemma wp_if_true p E e1 e2 Φ :
WP e1 @ p; E {{ Φ }} WP If (Lit (LitBool true)) e1 e2 @ p; E {{ Φ }}.
Proof.
apply wp_lift_pure_det_head_step_no_fork; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_if_false E e1 e2 Φ :
WP e2 @ E {{ Φ }} WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
Lemma wp_if_false p E e1 e2 Φ :
WP e2 @ p; E {{ Φ }} WP If (Lit (LitBool false)) e1 e2 @ p; E {{ Φ }}.
Proof.
apply wp_lift_pure_det_head_step_no_fork; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_fst E e1 v1 e2 Φ :
Lemma wp_fst p E e1 v1 e2 Φ :
to_val e1 = Some v1 is_Some (to_val e2)
Φ v1 WP Fst (Pair e1 e2) @ E {{ Φ }}.
Φ v1 WP Fst (Pair e1 e2) @ p; E {{ Φ }}.
Proof.
intros ? [v2 ?].
rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1) -?wp_value; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_snd E e1 e2 v2 Φ :
Lemma wp_snd p E e1 e2 v2 Φ :
is_Some (to_val e1) to_val e2 = Some v2
Φ v2 WP Snd (Pair e1 e2) @ E {{ Φ }}.
Φ v2 WP Snd (Pair e1 e2) @ p; E {{ Φ }}.
Proof.
intros [v1 ?] ?.
rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2) -?wp_value; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_case_inl E e0 e1 e2 Φ :
Lemma wp_case_inl p E e0 e1 e2 Φ :
is_Some (to_val e0)
WP App e1 e0 @ E {{ Φ }} WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
WP App e1 e0 @ p; E {{ Φ }} WP Case (InjL e0) e1 e2 @ p; E {{ Φ }}.
Proof.
intros [v0 ?].
rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e1 e0)); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_case_inr E e0 e1 e2 Φ :
Lemma wp_case_inr p E e0 e1 e2 Φ :
is_Some (to_val e0)
WP App e2 e0 @ E {{ Φ }} WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
WP App e2 e0 @ p; E {{ Φ }} WP Case (InjR e0) e1 e2 @ p; E {{ Φ }}.
Proof.
intros [v0 ?].
rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e2 e0)); eauto.
......@@ -160,9 +160,9 @@ Proof.
Qed.
(** Heap *)
Lemma wp_alloc E e v :
Lemma wp_alloc p E e v :
to_val e = Some 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.
......@@ -171,8 +171,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 %?.
......@@ -181,9 +181,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 :
to_val e = Some 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.
......@@ -193,9 +193,9 @@ Proof.
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
Lemma wp_cas_fail p E l q v' e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 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 <-%of_to_val ? Φ) ">Hl HΦ".
......@@ -205,9 +205,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 :
to_val e1 = Some v1 to_val e2 = Some 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Φ".
......@@ -219,59 +219,59 @@ Proof.
Qed.
(** Proof rules for derived constructs *)
Lemma wp_lam E x elam e1 e2 Φ :
Lemma wp_lam p E x elam e1 e2 Φ :
e1 = Lam x elam
is_Some (to_val e2)
Closed (x :b: []) elam
WP subst' x e2 elam @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
WP subst' x e2 elam @ p; E {{ Φ }} WP App e1 e2 @ p; E {{ Φ }}.
Proof. intros. by rewrite -(wp_rec _ _ BAnon) //. Qed.
Lemma wp_let E x e1 e2 Φ :
Lemma wp_let p E x e1 e2 Φ :
is_Some (to_val e1) Closed (x :b: []) e2
WP subst' x e1 e2 @ E {{ Φ }} WP Let x e1 e2 @ E {{ Φ }}.
WP subst' x e1 e2 @ p; E {{ Φ }} WP Let x e1 e2 @ p; E {{ Φ }}.
Proof. by apply wp_lam. Qed.
Lemma wp_seq E e1 e2 Φ :
Lemma wp_seq p E e1 e2 Φ :
is_Some (to_val e1) Closed [] e2
WP e2 @ E {{ Φ }} WP Seq e1 e2 @ E {{ Φ }}.
WP e2 @ p; E {{ Φ }} WP Seq e1 e2 @ p; E {{ Φ }}.
Proof. intros ??. by rewrite -wp_let. Qed.
Lemma wp_skip E Φ : Φ (LitV LitUnit) WP Skip @ E {{ Φ }}.
Lemma wp_skip p E Φ : Φ (LitV LitUnit) WP Skip @ p; E {{ Φ }}.
Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
Lemma wp_match_inl p E e0 x1 e1 x2 e2 Φ :
is_Some (to_val e0) Closed (x1 :b: []) e1
WP subst' x1 e0 e1 @ E {{ Φ }} WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
WP subst' x1 e0 e1 @ p; E {{ Φ }} WP Match (InjL e0) x1 e1 x2 e2 @ p; E {{ Φ }}.
Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
Lemma wp_match_inr p E e0 x1 e1 x2 e2 Φ :
is_Some (to_val e0) Closed (x2 :b: []) e2
WP subst' x2 e0 e2 @ E {{ Φ }} WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
WP subst' x2 e0 e2 @ p; E {{ Φ }} WP Match (InjR e0) x1 e1 x2 e2 @ p; E {{ Φ }}.
Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
Lemma wp_le E (n1 n2 : Z) P Φ :
Lemma wp_le p E (n1 n2 : Z) P Φ :
(n1 n2 P Φ (LitV (LitBool true)))
(n2 < n1 P Φ (LitV (LitBool false)))
P WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
P WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ p; E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 n2)); by eauto with omega.
Qed.
Lemma wp_lt E (n1 n2 : Z) P Φ :
Lemma wp_lt p E (n1 n2 : Z) P Φ :
(n1 < n2 P Φ (LitV (LitBool true)))
(n2 n1 P Φ (LitV (LitBool false)))
P WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
P WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ p; E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed.
Lemma wp_eq E e1 e2 v1 v2 P Φ :
Lemma wp_eq p E e1 e2 v1 v2 P Φ :
to_val e1 = Some v1 to_val e2 = Some v2
(v1 = v2 P Φ (LitV (LitBool true)))
(v1 v2 P Φ (LitV (LitBool false)))
P WP BinOp EqOp e1 e2 @ E {{ Φ }}.
P WP BinOp EqOp e1 e2 @ p; E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (v1 = v2)); by eauto.
......
......@@ -25,7 +25,7 @@ Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
Ltac wp_seq_head :=
lazymatch goal with
| |- _ wp progress ?E (Seq _ _) ?Q =>
| |- _ wp ?p ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; iNext
end.
......@@ -33,15 +33,15 @@ Ltac wp_finish := intros_revert ltac:(
rewrite /= ?to_of_val;
try iNext;
repeat lazymatch goal with
| |- _ wp progress ?E (Seq _ _) ?Q =>
| |- _ wp ?p ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; iNext
| |- _ wp progress ?E _ ?Q => wp_value_head
| |- _ wp ?p ?E _ ?Q => wp_value_head
end).
Tactic Notation "wp_value" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
| _ => fail "wp_value: not a wp"
end.
......@@ -56,7 +56,7 @@ Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
Tactic Notation "wp_rec" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
......@@ -69,7 +69,7 @@ Tactic Notation "wp_rec" :=
Tactic Notation "wp_lam" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind_core K; etrans;
......@@ -84,7 +84,7 @@ Tactic Notation "wp_seq" := wp_let.
Tactic Notation "wp_op" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
lazymatch eval hnf in e' with
| BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
| BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
......@@ -103,7 +103,7 @@ Tactic Notation "wp_op" :=
Tactic Notation "wp_proj" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
| Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
......@@ -114,7 +114,7 @@ Tactic Notation "wp_proj" :=
Tactic Notation "wp_if" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| If _ _ _ =>
wp_bind_core K;
......@@ -126,7 +126,7 @@ Tactic Notation "wp_if" :=
Tactic Notation "wp_match" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Case _ _ _ =>
wp_bind_core K;
......@@ -139,7 +139,7 @@ Tactic Notation "wp_match" :=
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind_core K
end) || fail "wp_bind: cannot find" efoc "in" e
......@@ -153,13 +153,13 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
Lemma tac_wp_alloc Δ Δ' p E j e v Φ :
to_val e = Some v
IntoLaterNEnvs 1 Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
(Δ'' Φ (LitV (LitLoc l))))
Δ WP Alloc e @ E {{ Φ }}.
Δ WP Alloc e @ p; E {{ Φ }}.
Proof.
intros ?? HΔ. eapply wand_apply; first exact: wp_alloc.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
......@@ -167,49 +167,49 @@ Proof.
by rewrite right_id HΔ'.
Qed.
Lemma tac_wp_load Δ Δ' E i l q v Φ :
Lemma tac_wp_load Δ Δ' p E i l q v Φ :
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
(Δ' Φ v)
Δ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Δ WP Load (Lit (LitLoc l)) @ p; E {{ Φ }}.
Proof.
intros. eapply wand_apply; first exact: wp_load.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
Lemma tac_wp_store Δ Δ' Δ'' p E i l v e v' Φ :
to_val e = Some v'
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
(Δ'' Φ (LitV LitUnit))
Δ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Δ WP Store (Lit (LitLoc l)) e @ p; E {{ Φ }}.
Proof.
intros. eapply wand_apply; first by eapply wp_store.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
Lemma tac_wp_cas_fail Δ Δ' p E i l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' Φ (LitV (LitBool false)))
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ p; E {{ Φ }}.
Proof.
intros. eapply wand_apply; first exact: wp_cas_fail.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
Lemma tac_wp_cas_suc Δ Δ' Δ'' p E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
(Δ'' Φ (LitV (LitBool true)))
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ p; E {{ Φ }}.
Proof.
intros; subst. eapply wand_apply; first exact: wp_cas_suc.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
......@@ -220,7 +220,7 @@ End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
| |- _ wp ?p ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApply lem; try iNext)
| _ => fail "wp_apply: not a 'wp'"
end.
......@@ -228,7 +228,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q =>
| |- _ wp ?p ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Alloc _ => wp_bind_core K end)
......@@ -250,7 +250,7 @@ Tactic Notation "wp_alloc" ident(l) :=
Tactic Notation "wp_load" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q =>
| |- _ wp ?p ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Load _ => wp_bind_core K end)
......@@ -266,7 +266,7 @@ Tactic Notation "wp_load" :=
Tactic Notation "wp_store" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q =>
| |- _ wp ?p ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Store _ _ => wp_bind_core K end)
......@@ -285,7 +285,7 @@ Tactic Notation "wp_store" :=
Tactic Notation "wp_cas_fail" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q =>
| |- _ wp ?p ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
......@@ -306,7 +306,7 @@ Tactic Notation "wp_cas_fail" :=
Tactic Notation "wp_cas_suc" :=
iStartProof;
lazymatch goal with
| |- _ wp progress ?E ?e ?Q =>
| |- _ wp ?p ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
......
......@@ -183,9 +183,9 @@ Definition atomic (e : expr) :=
| App (Rec _ _ (Lit _)) (Lit _) => true
| _ => false
end.
Lemma atomic_correct e : atomic e language.atomic (to_expr e).
Lemma atomic_correct e : atomic e language.strong_atomic (to_expr e).
Proof.
intros He. apply language.weaken_atomic, ectx_language_strong_atomic.
intros He. apply ectx_language_strong_atomic.
- intros σ e' σ' ef.
destruct e; simpl; try done; repeat (case_match; try done);
inversion 1; rewrite ?to_of_val; eauto. subst.
......@@ -224,13 +224,13 @@ Ltac solve_to_val :=
Ltac solve_atomic :=
match goal with
| |- language.atomic ?e =>
let e' := W.of_expr e in change (language.atomic (W.to_expr e'));
| |- language.strong_atomic ?e =>
let e' := W.of_expr e in change (language.strong_atomic (W.to_expr e'));
apply W.atomic_correct; vm_compute; exact I
end.
Hint Extern 10 (language.atomic _) => solve_atomic.
Hint Extern 10 (language.strong_atomic _) => solve_atomic.
(* For the side-condition of elim_upd_fupd_wp_atomic *)
Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
Hint Extern 10 (language.strong_atomic _) => solve_atomic : typeclass_instances.
(** Substitution *)
Ltac simpl_subst :=
......
Markdown is supported
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