* Atomicity of expressions is defined semantically

* Values are considered as atomic expressions (this does not hurt, and
  this makes the proofs of atomicity simpler).

heap_lang/heap.v

@@ -153,12 +153,12 @@ Section heap.
     to_val e = Some v → nclose heapN ⊆ E →
     heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
-    iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx.
+    iIntros (?%of_to_val ?) "[#Hinv HΦ]". subst. rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
-    iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
+    iApply wp_alloc_pst. iFrame "Hheap". iNext.
     iIntros (l) "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
     iFrame "Hheap". iSplitR; first iPureIntro.
@@ -173,7 +173,7 @@ Section heap.
   Proof.
     iIntros (?) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hl".
@@ -186,9 +186,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    iIntros (??) "[#Hh [Hl HΦ]]".
+    iIntros (?%of_to_val ?) "[#Hh [Hl HΦ]]". subst.
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
@@ -202,9 +202,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (????) "[#Hh [Hl HΦ]]".
+    iIntros (?%of_to_val ?%of_to_val ??) "[#Hh [Hl HΦ]]". subst.
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite of_heap_singleton_op //. iFrame "Hl".
@@ -217,9 +217,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (???) "[#Hh [Hl HΦ]]".
+    iIntros (?%of_to_val ?%of_to_val ?) "[#Hh [Hl HΦ]]". subst.
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".

heap_lang/lang.v

@@ -273,19 +273,6 @@ Inductive head_step : expr → state → expr → state → option (expr) → Pr
      σ !! l = Some v1 →
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
 
-(** Atomic expressions *)
-Definition atomic (e: expr) :=
-  match e with
-  | Alloc e => is_Some (to_val e)
-  | Load e => is_Some (to_val e)
-  | Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
-  | CAS e0 e1 e2 =>
-     is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
-  (* Make "skip" atomic *)
-  | App (Rec _ _ (Lit _)) (Lit _) => True
-  | _ => False
-  end.
-
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
 Proof.
@@ -310,22 +297,6 @@ Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma atomic_not_val e : atomic e → to_val e = None.
-Proof. by destruct e. Qed.
-
-Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
-Proof.
-  intros. destruct Ki; simplify_eq/=; destruct_and?;
-    repeat (simpl || case_match || contradiction); eauto.
-Qed.
-
-Lemma atomic_step e1 σ1 e2 σ2 ef :
-  atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
-Proof.
-  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
-  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
-Qed.
-
 Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
   head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
@@ -391,13 +362,11 @@ Program Instance heap_ectxi_lang :
   EctxiLanguage
     (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
-  fill_item := heap_lang.fill_item;
-  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
+  fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
 |}.
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
-  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
-  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
-  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
+  heap_lang.val_stuck, heap_lang.fill_item_val, heap_lang.fill_item_no_val_inj,
+  heap_lang.head_ctx_step_val.
 
 Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
 

heap_lang/lifting.v

@@ -23,13 +23,12 @@ Lemma wp_bindi {E e} Ki Φ :
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ e v Φ :
-  to_val e = Some v →
+Lemma wp_alloc_pst E σ v Φ :
   ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
-  ⊢ WP Alloc e @ E {{ Φ }}.
+  ⊢ WP Alloc (of_val v) @ E {{ Φ }}.
 Proof.
-  iIntros (?)  "[HP HΦ]".
-  iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto).
+  iIntros "[HP HΦ]".
+  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto with fsaV.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
   subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
@@ -40,36 +39,37 @@ Lemma wp_load_pst E σ l v Φ :
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
-    last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
+    last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
 Qed.
 
-Lemma wp_store_pst E σ l e v v' Φ :
-  to_val e = Some v → σ !! l = Some v' →
+Lemma wp_store_pst E σ l v v' Φ :
+  σ !! l = Some v' →
   ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
-  ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
 Proof.
-  intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
-    ?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto.
+  intros ?.
+  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
+    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
-Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
+Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
+  σ !! l = Some v' → v' ≠ v1 →
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
-  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
-    ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; by eauto 10.
+  intros ??.
+  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
+    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
-Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
+Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
+  σ !! l = Some v1 →
   ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
-  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
-    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; by eauto 10.
+  intros ?. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
+    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto).
+  solve_atomic.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)

heap_lang/tactics.v

@@ -183,10 +183,20 @@ Definition atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → heap_lang.atomic (to_expr e).
+Lemma atomic_correct e : atomic e → ectx_language.atomic (to_expr e).
 Proof.
-  destruct e; simpl; repeat (case_match; try done);
-    naive_solver eauto using to_val_is_Some.
+  intros He. split.
+  - intros σ e' σ' ef.
+    destruct e; simpl; try done; repeat (case_match; try done);
+    inversion 1; rewrite ?to_of_val; eauto. subst.
+    unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
+  - intros K e' Hfill Hnotval. destruct K as [|Ki K]; [done|exfalso].
+    apply (fill_not_val K), eq_None_not_Some in Hnotval. apply Hnotval. simpl.
+    revert He. destruct e; simpl; try done; repeat (case_match; try done);
+    rewrite ?bool_decide_spec;
+    destruct Ki; inversion Hfill; subst; clear Hfill;
+    try naive_solver eauto using to_val_is_Some.
+    move=> _ /=; destruct decide as [|Nclosed]; [by eauto | by destruct Nclosed].
 Qed.
 End W.
 
@@ -214,16 +224,15 @@ Ltac solve_to_val :=
 
 Ltac solve_atomic :=
   try match goal with
-  | |- context E [language.atomic ?e] =>
-     let X := context E [atomic e] in change X
+  | |- language.atomic ?e => apply ectx_language_atomic
   end;
   match goal with
-  | |- atomic ?e =>
+  | |- ectx_language.atomic ?e =>
      let e' := W.of_expr e in change (atomic (W.to_expr e'));
      apply W.atomic_correct; vm_compute; exact I
   end.
-Hint Extern 0 (atomic _) => solve_atomic : fsaV.
 Hint Extern 0 (language.atomic _) => solve_atomic : fsaV.
+Hint Extern 0 (ectx_language.atomic _) => solve_atomic : fsaV.
 
 (** Substitution *)
 Ltac simpl_subst :=

program_logic/ectx_language.v

@@ -11,7 +11,6 @@ Class EctxLanguage (expr val ectx state : Type) := {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
@@ -34,16 +33,6 @@ Class EctxLanguage (expr val ectx state : Type) := {
     to_val e1 = None →
     head_step e1' σ1 e2 σ2 ef →
     exists K'', K' = comp_ectx K K'';
-
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    head_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2);
-  atomic_fill e K :
-    atomic (fill K e) →
-    to_val e = None →
-    K = empty_ectx;
 }.
 
 Arguments of_val {_ _ _ _ _} _.
@@ -51,7 +40,6 @@ Arguments to_val {_ _ _ _ _} _.
 Arguments empty_ectx {_ _ _ _ _}.
 Arguments comp_ectx {_ _ _ _ _} _ _.
 Arguments fill {_ _ _ _ _} _ _.
-Arguments atomic {_ _ _ _ _} _.
 Arguments head_step {_ _ _ _ _} _ _ _ _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
@@ -62,9 +50,6 @@ Arguments fill_comp {_ _ _ _ _} _ _ _.
 Arguments fill_not_val {_ _ _ _ _} _ _ _.
 Arguments ectx_positive {_ _ _ _ _} _ _ _.
 Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
-Arguments atomic_not_val {_ _ _ _ _} _ _.
-Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments atomic_fill {_ _ _ _ _} _ _ _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section ectx_language.
@@ -74,6 +59,10 @@ Section ectx_language.
   Definition head_reducible (e : expr) (σ : state) :=
     ∃ e' σ' ef, head_step e σ e' σ' ef.
 
+  Definition atomic (e : expr) :=
+    (∀ σ e' σ' ef, head_step e σ e' σ' ef → is_Some (to_val e')) ∧
+    (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx).
+
   Inductive prim_step (e1 : expr) (σ1 : state)
       (e2 : expr) (σ2 : state) (ef : option expr) : Prop :=
     Ectx_step K e1' e2' :
@@ -84,6 +73,14 @@ Section ectx_language.
     prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
   Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
 
+  Lemma atomic_step e1 σ1 e2 σ2 ef :
+    atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
+  Proof. destruct 1 as [? _]; eauto. Qed.
+
+  Lemma atomic_fill e K :
+    atomic (fill K e) → to_val e = None → K = empty_ectx.
+  Proof. destruct 1 as [_ ?]; eauto. Qed.
+
   Lemma atomic_prim_step e1 σ1 e2 σ2 ef :
     atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
   Proof.
@@ -95,12 +92,9 @@ Section ectx_language.
   Canonical Structure ectx_lang : language := {|
     language.expr := expr; language.val := val; language.state := state;
     language.of_val := of_val; language.to_val := to_val;
-    language.atomic := atomic;
     language.prim_step := prim_step;
     language.to_of_val := to_of_val; language.of_to_val := of_to_val;
     language.val_stuck := val_prim_stuck;
-    language.atomic_not_val := atomic_not_val;
-    language.atomic_step := atomic_prim_step
   |}.
 
   (* Some lemmas about this language *)
@@ -111,6 +105,13 @@ Section ectx_language.
   Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ.
   Proof. intros (e'&σ'&ef&?). eexists e', σ', ef. by apply head_prim_step. Qed.
 
+  Lemma ectx_language_atomic e : atomic e → language.atomic e.
+  Proof.
+    intros Hatomic σ e' σ' ef [K e1' e2' -> -> Hstep].
+    assert (K = empty_ectx) as -> by eauto 10 using atomic_fill, val_stuck.
+    revert Hatomic; rewrite !fill_empty. intros. by eapply atomic_step.
+  Qed.
+
   Lemma head_reducible_prim_step e1 σ1 e2 σ2 ef :
     head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 ef →
     head_step e1 σ1 e2 σ2 ef.

program_logic/ectxi_language.v

@@ -9,7 +9,6 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
-  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
@@ -24,20 +23,11 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
 
   head_ctx_step_val Ki e σ1 e2 σ2 ef :
     head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e);
-
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    head_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2);
-  atomic_fill_item e Ki :
-    atomic (fill_item Ki e) → is_Some (to_val e)
 }.
 
 Arguments of_val {_ _ _ _ _} _.
 Arguments to_val {_ _ _ _ _} _.
 Arguments fill_item {_ _ _ _ _} _ _.
-Arguments atomic {_ _ _ _ _} _.
 Arguments head_step {_ _ _ _ _} _ _ _ _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
@@ -47,9 +37,6 @@ Arguments fill_item_val {_ _ _ _ _} _ _ _.
 Arguments fill_item_no_val_inj {_ _ _ _ _} _ _ _ _ _ _ _.
 Arguments head_ctx_step_val {_ _ _ _ _} _ _ _ _ _ _ _.
 Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
-Arguments atomic_not_val {_ _ _ _ _} _ _.
-Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments atomic_fill_item {_ _ _ _ _} _ _ _.
 
 Section ectxi_language.
   Context {expr val ectx_item state}
@@ -70,12 +57,6 @@ Section ectxi_language.
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
 
-  Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
-  Proof.
-    destruct K as [|Ki K]; [done|].
-    rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
-  Qed.
-
   (* When something does a step, and another decomposition of the same expression
   has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
   other words, [e] also contains the reducible expression *)
@@ -95,10 +76,9 @@ Section ectxi_language.
   Global Program Instance : EctxLanguage expr val ectx state :=
     (* For some reason, Coq always rejects the record syntax claiming I
        fixed fields of different records, even when I did not. *)
-    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill atomic head_step _ _ _ _ _ _ _ _ _ _ _ _.
+    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill head_step _ _ _ _ _ _ _ _ _.
   Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
-    atomic_not_val, atomic_step, fill_not_val, atomic_fill,
-    step_by_val, fold_right_app, app_eq_nil.
+    fill_not_val, step_by_val, fold_right_app, app_eq_nil.
 
   Global Instance ectxi_lang_ctx_item Ki :
     LanguageCtx (ectx_lang expr) (fill_item Ki).

program_logic/hoare_lifting.v

@@ -49,12 +49,12 @@ Proof.
   iApply (ht_lift_step E E _ (λ σ1', P ∧ σ1 = σ1')%I
            (λ e2 σ2 ef, ownP σ2 ★ ■ (is_Some (to_val e2) ∧ prim_step e1 σ1 e2 σ2 ef))%I
            (λ e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ P)%I);
-    try by (eauto using atomic_not_val).
+    try by (eauto using reducible_not_val).
   repeat iSplit.
   - iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro.
-    iSplit. by eauto using atomic_step. iFrame. by auto.
+    iSplit. by eauto. iFrame. by auto.
   - iIntros (? e2 σ2 ef) "! (%&Hown&HP&%)". iPvsIntro. subst.
-    iFrame. iSplit; iPureIntro; auto. split; eauto using atomic_step.
+    iFrame. iSplit; iPureIntro; auto. split; eauto.
   - iIntros (e2 σ2 ef) "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
     iApply wp_value'. iExists σ2, ef. by iSplit.
   - done.

program_logic/language.v

@@ -6,26 +6,17 @@ Structure language := Language {
   state : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  atomic : expr → Prop;
   prim_step : expr → state → expr → state → option expr → Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
-  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    prim_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2)
+  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None
 }.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
-Arguments atomic {_} _.
 Arguments prim_step {_} _ _ _ _ _.
 Arguments to_of_val {_} _.
 Arguments of_to_val {_} _ _ _.
 Arguments val_stuck {_} _ _ _ _ _ _.
-Arguments atomic_not_val {_} _ _.
-Arguments atomic_step {_} _ _ _ _ _ _ _.
 
 Canonical Structure stateC Λ := leibnizC (state Λ).
 Canonical Structure valC Λ := leibnizC (val Λ).
@@ -39,6 +30,8 @@ Section language.
 
   Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' ef, prim_step e σ e' σ' ef.
+  Definition atomic (e : expr Λ) : Prop :=
+    ∀ σ e' σ' ef, prim_step e σ e' σ' ef → is_Some (to_val e').
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
@@ -50,8 +43,6 @@ Section language.
   Proof. intros <-. by rewrite to_of_val. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
-  Lemma atomic_of_val v : ¬atomic (of_val v).
-  Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
   Global Instance: Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 End language.

program_logic/lifting.v

@@ -67,10 +67,10 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
     ■ prim_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (??) "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val.
-  iPvsIntro. iExists σ1. repeat iSplit; eauto 10 using atomic_step.
+  iIntros (Hatom ?) "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); eauto using reducible_not_val.
+  iPvsIntro. iExists σ1. repeat iSplit; eauto 10.
   iFrame. iNext. iIntros (e2 σ2 ef) "[% Hσ2]".
-  edestruct @atomic_step as [v2 Hv%of_to_val]; eauto. subst e2.
+  edestruct Hatom as [v2 Hv%of_to_val]; eauto. subst e2.
   iDestruct ("Hwp" $! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto.
   iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val.
 Qed.

program_logic/weakestpre.v

@@ -160,20 +160,25 @@ Lemma wp_atomic E1 E2 e Φ :
   E2 ⊆ E1 → atomic e →
   (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof.
-  rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor.
-  eauto using atomic_not_val. intros k Ef σ1 rf ???.
-  destruct (Hvs (S k) Ef σ1 rf) as (r'&Hwp&?); auto.
-  destruct (wp_step_inv E2 Ef (pvs_def E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
-    as [Hsafe Hstep]; auto using atomic_not_val; [].
-  split; [done|]=> e2 σ2 ef ?.
-  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
-  destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
-    [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
-  rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
-  destruct (Hvs' k Ef σ2 (r2' ⋅ rf)) as (r3&[]); rewrite ?assoc; auto.
-  exists r3, r2'; split_and?; last done.
-  - by rewrite -assoc.
-  - constructor; apply pvs_intro; auto.
+  rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs.
+  destruct (to_val e) as [v|] eqn:Hvale.
+  - apply of_to_val in Hvale. subst e. eapply wp_pre_value. rewrite pvs_eq.
+    intros k Ef σ rf ???. destruct (Hvs k Ef σ rf) as (r'&Hwp&?); auto.
+    apply wp_value_inv in Hwp. rewrite pvs_eq in Hwp.
+    destruct (Hwp k Ef σ rf) as (r2'&HΦ&?); auto.
+  - apply wp_pre_step. done. intros k Ef σ1 rf ???.
+    destruct (Hvs (S k) Ef σ1 rf) as (r'&Hwp&?); auto.
+    destruct (wp_step_inv E2 Ef (pvs_def E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
+      as [Hsafe Hstep]; auto; [].
+    split; [done|]=> e2 σ2 ef ?.
+    destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
+    destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
+      [|destruct (He σ1 e2 σ2 ef); naive_solver].
+    rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
+    destruct (Hvs' k Ef σ2 (r2' ⋅ rf)) as (r3&[]); rewrite ?assoc; auto.
+    exists r3, r2'; split_and?; last done.
+    + by rewrite -assoc.
+    + constructor; apply pvs_intro; auto.
 Qed.
 Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }} ★ R ⊢ WP e @ E {{ v, Φ v ★ R }}.
 Proof.