Commit f02baee6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Move HeapLang `head_step` tactics and `Atomic`/`PureExec` instances to their own files.

parent a15dc76f
......@@ -141,6 +141,7 @@ iris/proofmode/modality_instances.v
iris_heap_lang/locations.v
iris_heap_lang/lang.v
iris_heap_lang/class_instances.v
iris_heap_lang/metatheory.v
iris_heap_lang/tactics.v
iris_heap_lang/primitive_laws.v
......
From iris.program_logic Require Export language.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics notation.
From iris.prelude Require Import options.
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.
(** * Instances of the [Atomic] class *)
Section atomic.
Local Ltac solve_atomic :=
apply strongly_atomic_atomic, ectx_language_atomic;
[inversion 1; naive_solver
|apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
Global Instance rec_atomic s f x e : Atomic s (Rec f x e).
Proof. solve_atomic. Qed.
Global Instance pair_atomic s v1 v2 : Atomic s (Pair (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Global Instance injl_atomic s v : Atomic s (InjL (Val v)).
Proof. solve_atomic. Qed.
Global Instance injr_atomic s v : Atomic s (InjR (Val v)).
Proof. solve_atomic. Qed.
(** The instance below is a more general version of [Skip] *)
Global Instance beta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
Proof. destruct f, x; solve_atomic. Qed.
Global Instance unop_atomic s op v : Atomic s (UnOp op (Val v)).
Proof. solve_atomic. Qed.
Global Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Global Instance if_true_atomic s v1 e2 :
Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
Proof. solve_atomic. Qed.
Global Instance if_false_atomic s e1 v2 :
Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
Proof. solve_atomic. Qed.
Global Instance fst_atomic s v : Atomic s (Fst (Val v)).
Proof. solve_atomic. Qed.
Global Instance snd_atomic s v : Atomic s (Snd (Val v)).
Proof. solve_atomic. Qed.
Global Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
Global Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
Proof. solve_atomic. Qed.
Global Instance free_atomic s v : Atomic s (Free (Val v)).
Proof. solve_atomic. Qed.
Global Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Global Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Global Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Global Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Global Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
Global Instance resolve_atomic s e v1 v2 :
Atomic s e Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
- subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
- rewrite fill_app. rewrite fill_app in Hfill.
assert ( v, Val v = fill Ks e1' False) as fill_absurd.
{ intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
destruct K; (inversion Hfill; clear Hfill; subst; try
match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
+ destruct s; intro Hs; simpl in *.
* destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
* apply irreducible_resolve. by rewrite fill_app in Hs.
+ econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
Qed.
End atomic.
(** * Instances of the [PureExec] class *)
(** The behavior of the various [wp_] tactics with regard to lambda differs in
the following way:
- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.
To realize this behavior, we define the class [AsRecV v f x erec], which takes a
value [v] as its input, and turns it into a [RecV f x erec] via the instance
[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
not if [v] contains a lambda/rec that is hidden behind a definition.
To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
as_recv : v = RecV f x erec.
Global Hint Mode AsRecV ! - - - : typeclass_instances.
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Global Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
apply AsRecV_recv : typeclass_instances.
Section pure_exec.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_recc f x (erec : expr) :
PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
Global Instance pure_pairc (v1 v2 : val) :
PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
Proof. solve_pure_exec. Qed.
Global Instance pure_injlc (v : val) :
PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
Proof. solve_pure_exec. Qed.
Global Instance pure_injrc (v : val) :
PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
Global Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.
Global Instance pure_unop op v v' :
PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
Proof. solve_pure_exec. Qed.
Global Instance pure_binop op v1 v2 v' :
PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
Proof. solve_pure_exec. Qed.
(* Higher-priority instance for [EqOp]. *)
Global Instance pure_eqop v1 v2 :
PureExec (vals_compare_safe v1 v2) 1
(BinOp EqOp (Val v1) (Val v2))
(Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
Proof.
intros Hcompare.
cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
{ intros. revert Hcompare. solve_pure_exec. }
rewrite /bin_op_eval /= decide_True //.
Qed.
Global Instance pure_if_true e1 e2 :
PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
Proof. solve_pure_exec. Qed.
Global Instance pure_if_false e1 e2 :
PureExec True 1 (If (Val $ LitV $ LitBool false) e1 e2) e2.
Proof. solve_pure_exec. Qed.
Global Instance pure_fst v1 v2 :
PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
Proof. solve_pure_exec. Qed.
Global Instance pure_snd v1 v2 :
PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl v e1 e2 :
PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr v e1 e2 :
PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
Proof. solve_pure_exec. Qed.
End pure_exec.
(** This file proves the basic laws of the HeapLang program logic by applying
the Iris lifting lemmas. *)
From stdpp Require Import fin_maps.
From iris.algebra Require Import auth gmap.
From iris.proofmode Require Import tactics.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Export class_instances.
From iris.heap_lang Require Import tactics notation.
From iris.prelude Require Import options.
......@@ -59,187 +57,6 @@ Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
Notation "l ↦_ I v" := (inv_mapsto_own l v I%stdpp%type)
(at level 20, I at level 9, format "l ↦_ I v") : bi_scope.
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
operations. This tactic is slightly ad-hoc and tuned for proving our lifting
lemmas. *)
Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : head_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
(* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : core.
Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.
Local Ltac solve_atomic :=
apply strongly_atomic_atomic, ectx_language_atomic;
[inversion 1; naive_solver
|apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
Instance rec_atomic s f x e : Atomic s (Rec f x e).
Proof. solve_atomic. Qed.
Instance pair_atomic s v1 v2 : Atomic s (Pair (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance injl_atomic s v : Atomic s (InjL (Val v)).
Proof. solve_atomic. Qed.
Instance injr_atomic s v : Atomic s (InjR (Val v)).
Proof. solve_atomic. Qed.
(** The instance below is a more general version of [Skip] *)
Instance beta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
Proof. destruct f, x; solve_atomic. Qed.
Instance unop_atomic s op v : Atomic s (UnOp op (Val v)).
Proof. solve_atomic. Qed.
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance if_true_atomic s v1 e2 : Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
Proof. solve_atomic. Qed.
Instance if_false_atomic s e1 v2 : Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
Proof. solve_atomic. Qed.
Instance fst_atomic s v : Atomic s (Fst (Val v)).
Proof. solve_atomic. Qed.
Instance snd_atomic s v : Atomic s (Snd (Val v)).
Proof. solve_atomic. Qed.
Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
Proof. solve_atomic. Qed.
Instance free_atomic s v : Atomic s (Free (Val v)).
Proof. solve_atomic. Qed.
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
Instance resolve_atomic s e v1 v2 :
Atomic s e Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
- subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
- rewrite fill_app. rewrite fill_app in Hfill.
assert ( v, Val v = fill Ks e1' False) as fill_absurd.
{ intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
destruct K; (inversion Hfill; clear Hfill; subst; try
match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
+ destruct s; intro Hs; simpl in *.
* destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
* apply irreducible_resolve. by rewrite fill_app in Hs.
+ econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
Qed.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
(** The behavior of the various [wp_] tactics with regard to lambda differs in
the following way:
- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.
To realize this behavior, we define the class [AsRecV v f x erec], which takes a
value [v] as its input, and turns it into a [RecV f x erec] via the instance
[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
not if [v] contains a lambda/rec that is hidden behind a definition.
To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
as_recv : v = RecV f x erec.
Global Hint Mode AsRecV ! - - - : typeclass_instances.
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Global Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
apply AsRecV_recv : typeclass_instances.
Instance pure_recc f x (erec : expr) :
PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
Instance pure_pairc (v1 v2 : val) :
PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
Proof. solve_pure_exec. Qed.
Instance pure_injlc (v : val) :
PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
Proof. solve_pure_exec. Qed.
Instance pure_injrc (v : val) :
PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.
Instance pure_unop op v v' :
PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
Proof. solve_pure_exec. Qed.
Instance pure_binop op v1 v2 v' :
PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
Proof. solve_pure_exec. Qed.
(* Higher-priority instance for [EqOp]. *)
Instance pure_eqop v1 v2 :
PureExec (vals_compare_safe v1 v2) 1
(BinOp EqOp (Val v1) (Val v2))
(Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
Proof.
intros Hcompare.
cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
{ intros. revert Hcompare. solve_pure_exec. }
rewrite /bin_op_eval /= decide_True //.
Qed.
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
Proof. solve_pure_exec. Qed.
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool false) e1 e2) e2.
Proof. solve_pure_exec. Qed.
Instance pure_fst v1 v2 :
PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
Proof. solve_pure_exec. Qed.
Instance pure_snd v1 v2 :
PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
Proof. solve_pure_exec. Qed.
Instance pure_case_inl v e1 e2 :
PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
Proof. solve_pure_exec. Qed.
Instance pure_case_inr v e1 e2 :
PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
Proof. solve_pure_exec. Qed.
Section lifting.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
......@@ -268,15 +85,15 @@ Lemma wp_fork s E e Φ :
WP e @ s; {{ _, True }} - Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
Proof.
iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto with head_step.
iIntros "!>" (v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
Lemma twp_fork s E e Φ :
WP e @ s; [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
Proof.
iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto with head_step.
iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
......@@ -405,7 +222,7 @@ Lemma twp_allocN_seq s E v n :
(l + (i : nat)) v meta_token (l + (i : nat)) }]].
Proof.
iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (gen_heap_alloc_big _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
as "(Hσ & Hl & Hm)".
......@@ -423,7 +240,7 @@ Lemma wp_allocN_seq s E v n :
(l + (i : nat)) v meta_token (l + (i : nat)) }}}.
Proof.
iIntros (Hn Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
iApply twp_allocN_seq; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
iApply twp_allocN_seq; [by auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_alloc s E v :
......@@ -436,7 +253,7 @@ Lemma wp_alloc s E v :
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l v meta_token l }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
iApply twp_alloc; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
iApply twp_alloc; [by auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_free s E l v :
......@@ -444,25 +261,27 @@ Lemma twp_free s E l v :
[[{ RET LitV LitUnit; True }]].
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_free s E l v :
{{{ l v }}} Free (Val $ LitV (LitLoc l)) @ s; E
{{{ RET LitV LitUnit; True }}}.
Proof.
iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
iApply (twp_free with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_load s E l dq v :
[[{ l {dq} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {dq} v }]].
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_load s E l dq v :
......@@ -477,17 +296,18 @@ Lemma twp_store s E l v' v :
[[{ RET LitV LitUnit; l v }]].
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_store s E l v' v :
{{{ l v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
{{{ RET LitV LitUnit; l v }}}.
Proof.
iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_store with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
iApply (twp_store with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
......@@ -496,10 +316,11 @@ Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
[[{ RET PairV v' (LitV $ LitBool false); l {dq} v' }]].
Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (κ v2' σ2 efs Hstep); inv_head_step.
rewrite bool_decide_false //.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
iModIntro; iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cmpxchg_fail s E l dq v' v1 v2 :
v' v1 vals_compare_safe v' v1
......@@ -507,7 +328,7 @@ Lemma wp_cmpxchg_fail s E l dq v' v1 v2 :
{{{ RET PairV v' (LitV $ LitBool false); l {dq} v' }}}.
Proof.
iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_cmpxchg_fail with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
iApply (twp_cmpxchg_fail with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_cmpxchg_suc s E l v1 v2 v' :
......@@ -516,11 +337,12 @@ Lemma twp_cmpxchg_suc s E l v1 v2 v' :
[[{ RET PairV v' (LitV $ LitBool true); l v2 }]].
Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (κ v2' σ2 efs Hstep); inv_head_step.
rewrite bool_decide_true //.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cmpxchg_suc s E l v1 v2 v' :
v' = v1 vals_compare_safe v' v1
......@@ -528,7 +350,7 @@ Lemma wp_cmpxchg_suc s E l v1 v2 v' :
{{{ RET PairV v' (LitV $ LitBool true); l v2 }}}.