From 2966b4daea77170d8eb83f44b2da59bc1888f4a1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jul 2016 18:19:39 +0200
Subject: [PATCH] Solve atomic also using reification/vm_compute.

I also reverted 7952bca41 since there is no need for atomic to be a
boolean predicate anymore. Moreover, I introduced a hint database
fsaV for solving side-conditions related to FSAs, in particular,
side-conditions related to expressions being atomic.
---
 heap_lang/lang.v               | 14 +++++++-------
 heap_lang/lib/counter.v        | 10 ++++++----
 heap_lang/lib/spawn.v          |  2 +-
 heap_lang/tactics.v            | 30 ++++++++++++++++++++++++++++++
 heap_lang/wp_tactics.v         |  2 --
 program_logic/ectx_language.v  |  2 +-
 program_logic/ectxi_language.v |  2 +-
 program_logic/language.v       |  2 +-
 program_logic/pviewshifts.v    |  3 +++
 proofmode/invariants.v         |  4 ++--
 proofmode/sts.v                |  2 +-
 11 files changed, 53 insertions(+), 20 deletions(-)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 51787af1c..4ef1e428c 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -274,16 +274,16 @@ Inductive head_step : expr → state → expr → state → option (expr) → Pr
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
 
 (** Atomic expressions *)
-Definition atomic (e: expr) : bool :=
+Definition atomic (e: expr) :=
   match e with
-  | Alloc e => bool_decide (is_Some (to_val e))
-  | Load e => bool_decide (is_Some (to_val e))
-  | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
+  | 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 =>
-    bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val 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
+  | App (Rec _ _ (Lit _)) (Lit _) => True
+  | _ => False
   end.
 
 (** Basic properties about the language *)
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 4940525af..b85548f38 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -49,11 +49,12 @@ Lemma inc_spec l j (Φ : val → iProp) :
 Proof.
   iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
   iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)".
-  wp_focus (! _)%E; iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  wp_focus (! _)%E.
+  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
   iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
   wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
-  wp_let; wp_op.
-  wp_focus (CAS _ _ _); iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  wp_let; wp_op. wp_focus (CAS _ _ _).
+  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
   iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
   destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
   - wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
@@ -74,7 +75,8 @@ Lemma read_spec l j (Φ : val → iProp) :
   ⊢ WP read #l {{ Φ }}.
 Proof.
   iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)".
-  rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  rewrite /read. wp_let.
+  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
   iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
   wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
   { iPureIntro; apply mnat_local_update; abstract lia. }
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index fd74020d3..e90308b4e 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -64,7 +64,7 @@ Proof.
   wp_apply wp_fork. iSplitR "Hf".
   - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
   - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
-    iInv N as (v') "[Hl _]"; first wp_done.
+    iInv N as (v') "[Hl _]".
     wp_store. iPvsIntro. iSplit; [iNext|done].
     iExists (SOMEV v). iFrame. eauto.
 Qed.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index c93e8bfb6..b994e7c58 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -163,6 +163,23 @@ Proof.
   induction e; simpl; repeat case_decide;
     f_equal; auto using is_closed_nil_subst, is_closed_of_val, eq_sym.
 Qed.
+
+Definition atomic (e : expr) :=
+  match e with
+  | Alloc e => bool_decide (is_Some (to_val e))
+  | Load e => bool_decide (is_Some (to_val e))
+  | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
+  | CAS e0 e1 e2 =>
+     bool_decide (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.
+Lemma atomic_correct e : atomic e → heap_lang.atomic (to_expr e).
+Proof.
+  destruct e; simpl; repeat (case_match; try done);
+    naive_solver eauto using to_val_is_Some.
+Qed.
 End W.
 
 Ltac solve_closed :=
@@ -187,6 +204,19 @@ Ltac solve_to_val :=
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
 
+Ltac solve_atomic :=
+  try match goal with
+  | |- context E [language.atomic ?e] =>
+     let X := context E [atomic e] in change X
+  end;
+  match goal with
+  | |- 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.
+
 (** Substitution *)
 Ltac simpl_subst :=
   csimpl;
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 8fef1f925..361b83a3a 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -16,8 +16,6 @@ Ltac wp_done :=
   | |- is_Some (to_val _) => solve_to_val
   | |- to_val _ = Some _ => solve_to_val
   | |- language.to_val _ = Some _ => solve_to_val
-  | |- Is_true (atomic _) => rewrite /= ?to_of_val; fast_done
-  | |- Is_true (language.atomic _) => rewrite /= ?to_of_val; fast_done
   | _ => fast_done
   end.
 
diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v
index 8d275b0f3..161f41ea4 100644
--- a/program_logic/ectx_language.v
+++ b/program_logic/ectx_language.v
@@ -11,7 +11,7 @@ Class EctxLanguage (expr val ectx state : Type) := {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  atomic : expr → bool;
+  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
diff --git a/program_logic/ectxi_language.v b/program_logic/ectxi_language.v
index a40a3c175..b09713b0e 100644
--- a/program_logic/ectxi_language.v
+++ b/program_logic/ectxi_language.v
@@ -9,7 +9,7 @@ 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 → bool;
+  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
diff --git a/program_logic/language.v b/program_logic/language.v
index d361644f2..fb97505aa 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -6,7 +6,7 @@ Structure language := Language {
   state : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  atomic : expr → bool;
+  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;
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index ea19b2a12..df3207507 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -243,6 +243,9 @@ Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
   fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊢ fsa E (λ a, Φ a ★ P)
 }.
 
+(* Used to solve side-conditions related to [fsaV] *)
+Create HintDb fsaV.
+
 Section fsa.
 Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
 Implicit Types Φ Ψ : A → iProp Λ Σ.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index 9d563ad01..46fb3cf1e 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -38,7 +38,7 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa with _ _ _ _ N H _ _;
     [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
-    |try fast_done (* atomic *)
+    |trivial with fsaV
     |solve_ndisj
     |iAssumption || fail "iInv: invariant" N "not found"
     |env_cbv; reflexivity
@@ -64,7 +64,7 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
     [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
-    |try fast_done (* atomic *)
+    |trivial with fsaV
     |solve_ndisj
     |iAssumption || fail "iOpenInv: invariant" N "not found"
     |let P := match goal with |- TimelessP ?P => P end in
diff --git a/proofmode/sts.v b/proofmode/sts.v
index c0c469b06..60dfe21be 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -38,7 +38,7 @@ Tactic Notation "iSts" constr(H) "as"
   end;
     [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iSts: cannot viewshift in goal" P
-    |try fast_done (* atomic *)
+    |auto with fsaV
     |iAssumptionCore || fail "iSts:" H "not found"
     |iAssumption || fail "iSts: invariant not found"
     |solve_ndisj
-- 
GitLab