Merge branch 'rk/substitution'

.gitlab-ci.yml

@@ -11,6 +11,7 @@ buildjob:
   only:
   - master
   - jh_simplified_resources
+  - rk/substitution
   artifacts:
     paths:
     - build-time.txt

_CoqProject

@@ -88,7 +88,6 @@ heap_lang/wp_tactics.v
 heap_lang/lifting.v
 heap_lang/derived.v
 heap_lang/notation.v
-heap_lang/substitution.v
 heap_lang/heap.v
 heap_lang/lib/spawn.v
 heap_lang/lib/par.v

heap_lang/derived.v

@@ -17,31 +17,31 @@ Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
-Lemma wp_lam E x ef e v Φ :
-  to_val e = Some v →
+Lemma wp_lam E x ef e Φ :
+  is_Some (to_val e) → Closed (x :b: []) ef →
   ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}.
 Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
 
-Lemma wp_let E x e1 e2 v Φ :
-  to_val e1 = Some v →
+Lemma wp_let 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 {{ Φ }}.
 Proof. apply wp_lam. Qed.
 
-Lemma wp_seq E e1 e2 v Φ :
-  to_val e1 = Some v →
+Lemma wp_seq E e1 e2 Φ :
+  is_Some (to_val e1) → Closed [] e2 →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. intros ?. by rewrite -wp_let. Qed.
+Proof. intros ??. by rewrite -wp_let. Qed.
 
 Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq // -wp_value //. Qed.
+Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
 
-Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ :
-  to_val e0 = Some v0 →
+Lemma wp_match_inl 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 {{ Φ }}.
 Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
 
-Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
-  to_val e0 = Some v0 →
+Lemma wp_match_inr 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 {{ Φ }}.
 Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
 

heap_lang/lib/assert.v

-From iris.heap_lang Require Export derived.
-From iris.heap_lang Require Import wp_tactics substitution notation.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
 
-Definition Assert {X} (e : expr X) : expr X :=
-  if: e then #() else #0 #0. (* #0 #0 is unsafe *)
+Definition assert : val :=
+  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
+(* just below ;; *)
+Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
+Global Opaque assert.
 
-Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
-  WExpr H e er → WExpr H (Assert e) (Assert er) := _.
-Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) e er :
-  WSubst x es H e er → WSubst x es H (Assert e) (Assert er).
-Proof. intros; red. by rewrite /Assert /wsubst -/wsubst; f_equal/=. Qed.
-Typeclasses Opaque Assert.
-
-Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) :
-  ▷ Φ #() ⊢ WP Assert #true {{ Φ }}.
-Proof. by rewrite -wp_if_true -wp_value. Qed.
-
-Lemma wp_assert' {Σ} (Φ : val → iProp heap_lang Σ) e :
-  WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}.
+Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
+  WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e {{ Φ }}.
 Proof.
-  rewrite /Assert. wp_focus e; apply wp_mono=>v.
-  apply uPred.pure_elim_l=>->. apply wp_assert.
+  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
+  iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
+  wp_if. done.
 Qed.

heap_lang/lib/barrier/barrier.v

 From iris.heap_lang Require Export notation.
 
 Definition newbarrier : val := λ: <>, ref #0.
-Definition signal : val := λ: "x", '"x" <- #1.
+Definition signal : val := λ: "x", "x" <- #1.
 Definition wait : val :=
-  rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
+  rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
 Global Opaque newbarrier signal wait.

heap_lang/lib/counter.v

@@ -8,9 +8,9 @@ Import uPred.
 Definition newcounter : val := λ: <>, ref #0.
 Definition inc : val :=
   rec: "inc" "l" :=
-    let: "n" := !'"l" in
-    if: CAS '"l" '"n" (#1 + '"n") then #() else '"inc" '"l".
-Definition read : val := λ: "l", !'"l".
+    let: "n" := !"l" in
+    if: CAS "l" "n" (#1 + "n") then #() else "inc" "l".
+Definition read : val := λ: "l", !"l".
 Global Opaque newcounter inc get.
 
 (** The CMRA we need. *)
@@ -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. }

heap_lang/lib/lock.v

@@ -6,8 +6,8 @@ Import uPred.
 Definition newlock : val := λ: <>, ref #false.
 Definition acquire : val :=
   rec: "acquire" "l" :=
-    if: CAS '"l" #false #true then #() else '"acquire" '"l".
-Definition release : val := λ: "l", '"l" <- #false.
+    if: CAS "l" #false #true then #() else "acquire" "l".
+Definition release : val := λ: "l", "l" <- #false.
 Global Opaque newlock acquire release.
 
 (** The CMRA we need. *)

heap_lang/lib/par.v

@@ -2,18 +2,14 @@ From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
-Definition par {X} : expr X :=
+Definition par : val :=
   λ: "fs",
-    let: "handle" := ^spawn (Fst '"fs") in
-    let: "v2" := Snd '"fs" #() in
-    let: "v1" := ^join '"handle" in
-    Pair '"v1" '"v2".
+    let: "handle" := spawn (Fst "fs") in
+    let: "v2" := Snd "fs" #() in
+    let: "v1" := join "handle" in
+    Pair "v1" "v2".
 Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
 Infix "||" := Par : expr_scope.
-
-Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
-Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
-  WSubst x es H par par := do_wsubst_closed _ x es H _.
 Global Opaque par.
 
 Section proof.
@@ -36,13 +32,14 @@ Proof.
   iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
 Qed.
 
-Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
+Lemma wp_par (Ψ1 Ψ2 : val → iProp)
+    (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp) :
   heapN ⊥ N →
   (heap_ctx heapN ★ WP e1 {{ Ψ1 }} ★ WP e2 {{ Ψ2 }} ★
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP e1 || e2 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto.
+  iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
   iFrame "Hh H". iSplitL "H1"; by wp_let.
 Qed.
 End proof.

heap_lang/lib/spawn.v

@@ -5,13 +5,13 @@ Import uPred.
 
 Definition spawn : val :=
   λ: "f",
-    let: "c" := ref (InjL #0) in
-    Fork ('"c" <- InjR ('"f" #())) ;; '"c".
+    let: "c" := ref NONE in
+    Fork ("c" <- SOME ("f" #())) ;; "c".
 Definition join : val :=
   rec: "join" "c" :=
-    match: !'"c" with
-      InjR "x" => '"x"
-    | InjL <>  => '"join" '"c"
+    match: !"c" with
+      SOME "x" => "x"
+    | NONE => "join" "c"
     end.
 Global Opaque spawn join.
 
@@ -33,8 +33,8 @@ Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
-  (∃ lv, l ↦ lv ★ (lv = InjLV #0 ∨
-                   ∃ v, lv = InjRV v ★ (Ψ v ∨ own γ (Excl ()))))%I.
+  (∃ lv, l ↦ lv ★ (lv = NONEV ∨
+                   ∃ v, lv = SOMEV v ★ (Ψ v ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp) : iProp :=
   (heapN ⊥ N ★ ∃ γ, heap_ctx heapN ★ own γ (Excl ()) ★
@@ -60,13 +60,13 @@ Proof.
   wp_let. wp_alloc l as "Hl". wp_let.
   iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
-  { iNext. iExists (InjLV #0). iFrame; eauto. }
+  { iNext. iExists NONEV. iFrame; eauto. }
   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 (InjRV v). iFrame. eauto.
+    iExists (SOMEV v). iFrame. eauto.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :

heap_lang/lifting.v

@@ -10,7 +10,7 @@ Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
-Implicit Types ef : option (expr []).
+Implicit Types ef : option expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
@@ -81,12 +81,13 @@ Proof.
   rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
 Qed.
 
-Lemma wp_rec E f x erec e1 e2 v2 Φ :
+Lemma wp_rec E f x erec e1 e2 Φ :
   e1 = Rec f x erec →
-  to_val e2 = Some v2 →
+  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 {{ Φ }}.
 Proof.
-  intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
+  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
     (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
     intros; inv_head_step; eauto.
 Qed.
@@ -121,35 +122,35 @@ Proof.
     ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_fst E e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+Lemma wp_fst E e1 v1 e2 Φ :
+  to_val e1 = Some v1 → is_Some (to_val e2) →
   ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
+  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_snd E e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+Lemma wp_snd E e1 e2 v2 Φ :
+  is_Some (to_val e1) → to_val e2 = Some v2 →
   ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
+  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_case_inl E e0 v0 e1 e2 Φ :
-  to_val e0 = Some v0 →
+Lemma wp_case_inl E e0 e1 e2 Φ :
+  is_Some (to_val e0) →
   ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
+  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
     (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_case_inr E e0 v0 e1 e2 Φ :
-  to_val e0 = Some v0 →
+Lemma wp_case_inr E e0 e1 e2 Φ :
+  is_Some (to_val e0) →
   ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
+  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
     (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 End lifting.

heap_lang/notation.v

@@ -24,6 +24,8 @@ Coercion LitLoc : loc >-> base_lit.
 Coercion App : expr >-> Funclass.
 Coercion of_val : val >-> expr.
 
+Coercion Var : string >-> expr.
+
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : binder_scope.
 
@@ -32,9 +34,6 @@ properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
 
-Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
-Notation "^ e" := (wexpr' e) (at level 8, format "^ e") : expr_scope.
-
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
 Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
@@ -115,6 +114,6 @@ Notation SOMEV x := (InjRV x).
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200) : expr_scope.
-Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 |  'end'" :=
+Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.

heap_lang/substitution.v

-From iris.heap_lang Require Export lang.
-Import heap_lang.
-
-(** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
-can be tuned by declaring [WExpr] and [WSubst] instances. *)
-
-(** * Weakening *)
-Class WExpr {X Y} (H : X `included` Y) (e : expr X) (er : expr Y) :=
-  do_wexpr : wexpr H e = er.
-Hint Mode WExpr + + + + - : typeclass_instances.
-
-(* Variables *)
-Hint Extern 0 (WExpr _ (Var ?y) _) =>
-  apply var_proof_irrel : typeclass_instances.
-
-(* Rec *)
-Instance do_wexpr_rec_true {X Y f y e} {H : X `included` Y} er :
-  WExpr (wexpr_rec_prf H) e er → WExpr H (Rec f y e) (Rec f y er) | 10.
-Proof. intros; red; f_equal/=. by etrans; [apply wexpr_proof_irrel|]. Qed.
-
-(* Values *)
-Instance do_wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e er :
-  WExpr (transitivity H1 H2) e er → WExpr H2 (wexpr H1 e) er | 0.
-Proof. by rewrite /WExpr wexpr_wexpr'. Qed.
-Instance do_wexpr_closed_closed (H : [] `included` []) e : WExpr H e e | 1.
-Proof. apply wexpr_id. Qed.
-Instance do_wexpr_closed_wexpr Y (H : [] `included` Y) e :
-  WExpr H e (wexpr' e) | 2.
-Proof. apply wexpr_proof_irrel. Qed.
-
-(* Boring connectives *)
-Section do_wexpr.
-Context {X Y : list string} (H : X `included` Y).
-Notation W := (WExpr H).
-
-(* Ground terms *)
-Global Instance do_wexpr_lit l : W (Lit l) (Lit l).
-Proof. done. Qed.
-Global Instance do_wexpr_app e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (App e1 e2) (App e1r e2r).
-Proof. intros; red; f_equal/=; apply: do_wexpr. Qed.
-Global Instance do_wexpr_unop op e er : W e er → W (UnOp op e) (UnOp op er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_binop op e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (BinOp op e1 e2) (BinOp op e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_if e0 e1 e2 e0r e1r e2r :
-  W e0 e0r → W e1 e1r → W e2 e2r → W (If e0 e1 e2) (If e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_pair e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (Pair e1 e2) (Pair e1r e2r).
-Proof. by intros ??; red; f_equal/=. Qed.
-Global Instance do_wexpr_fst e er : W e er → W (Fst e) (Fst er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_snd e er : W e er → W (Snd e) (Snd er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_injL e er : W e er → W (InjL e) (InjL er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_injR e er : W e er → W (InjR e) (InjR er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_case e0 e1 e2 e0r e1r e2r :
-  W e0 e0r → W e1 e1r → W e2 e2r → W (Case e0 e1 e2) (Case e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_fork e er : W e er → W (Fork e) (Fork er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_alloc e er : W e er → W (Alloc e) (Alloc er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_load e er : W e er → W (Load e) (Load er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_store e1 e2 e1r e2r :
-  W e1 e1r → W e2 e2r → W (Store e1 e2) (Store e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wexpr_cas e0 e1 e2 e0r e1r e2r :
-  W e0 e0r → W e1 e1r → W e2 e2r → W (CAS e0 e1 e2) (CAS e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-End do_wexpr.
-
-(** * WSubstitution *)
-Class WSubst {X Y} (x : string) (es : expr []) H (e : expr X) (er : expr Y) :=
-  do_wsubst : wsubst x es H e = er.
-Hint Mode WSubst + + + + + + - : typeclass_instances.
-
-Lemma do_wsubst_closed (e: ∀ {X}, expr X) {X Y} x es (H : X `included` x :: Y) :
-  (∀ X, WExpr (included_nil X) e e) → WSubst x es H e e.
-Proof.
-  rewrite /WSubst /WExpr=> He. rewrite -(He X) wsubst_wexpr'.
-  by rewrite (wsubst_closed _ _ _ _ _ (included_nil _)); last set_solver.
-Qed.
-
-(* Variables *)
-Lemma do_wsubst_var_eq {X Y x es} {H : X `included` x :: Y} `{VarBound x X} er :
-  WExpr (included_nil _) es er → WSubst x es H (Var x) er.
-Proof.
-  intros; red; simpl. case_decide; last done.
-  by etrans; [apply wexpr_proof_irrel|].
-Qed.
-Hint Extern 0 (WSubst ?x ?v _ (Var ?y) _) => first
-  [ apply var_proof_irrel
-  | apply do_wsubst_var_eq ] : typeclass_instances.
-
-(** Rec *)
-Lemma do_wsubst_rec_true {X Y x es f y e} {H : X `included` x :: Y}
-    (Hfy : BNamed x ≠ f ∧ BNamed x ≠ y) er :
-  WSubst x es (wsubst_rec_true_prf H Hfy) e er →
-  WSubst x es H (Rec f y e) (Rec f y er).
-Proof.
-  intros ?; red; f_equal/=; case_decide; last done.
-  by etrans; [apply wsubst_proof_irrel|].
-Qed.
-Lemma do_wsubst_rec_false {X Y x es f y e} {H : X `included` x :: Y}
-    (Hfy : ¬(BNamed x ≠ f ∧ BNamed x ≠ y)) er :
-  WExpr (wsubst_rec_false_prf H Hfy) e er →
-  WSubst x es H (Rec f y e) (Rec f y er).
-Proof.
-  intros; red; f_equal/=; case_decide; first done.
-  by etrans; [apply wexpr_proof_irrel|].
-Qed.
-
-Ltac bool_decide_no_check := apply (bool_decide_unpack _); vm_cast_no_check I.
-Hint Extern 0 (WSubst ?x ?v _ (Rec ?f ?y ?e) _) =>
-  match eval vm_compute in (bool_decide (BNamed x ≠ f ∧ BNamed x ≠ y)) with
-  | true => eapply (do_wsubst_rec_true ltac:(bool_decide_no_check))
-  | false => eapply (do_wsubst_rec_false ltac:(bool_decide_no_check))
-  end : typeclass_instances.
-
-(* Values *)
-Instance do_wsubst_wexpr X Y Z x es
-    (H1 : X `included` Y) (H2 : Y `included` x :: Z) e er :
-  WSubst x es (transitivity H1 H2) e er → WSubst x es H2 (wexpr H1 e) er | 0.
-Proof. by rewrite /WSubst wsubst_wexpr'. Qed.
-Instance do_wsubst_closed_closed x es (H : [] `included` [x]) e :
-  WSubst x es H e e | 1.
-Proof. apply wsubst_closed_nil. Qed.
-Instance do_wsubst_closed_wexpr Y x es (H : [] `included` x :: Y) e :
-  WSubst x es H e (wexpr' e) | 2.
-Proof. apply wsubst_closed, not_elem_of_nil. Qed.
-
-(* Boring connectives *)
-Section wsubst.
-Context {X Y} (x : string) (es : expr []) (H : X `included` x :: Y).
-Notation Sub := (WSubst x es H).
-
-(* Ground terms *)
-Global Instance do_wsubst_lit l : Sub (Lit l) (Lit l).
-Proof. done. Qed.
-Global Instance do_wsubst_app e1 e2 e1r e2r :
-  Sub e1 e1r → Sub e2 e2r → Sub (App e1 e2) (App e1r e2r).
-Proof. intros; red; f_equal/=; apply: do_wsubst. Qed.
-Global Instance do_wsubst_unop op e er : Sub e er → Sub (UnOp op e) (UnOp op er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_binop op e1 e2 e1r e2r :
-  Sub e1 e1r → Sub e2 e2r → Sub (BinOp op e1 e2) (BinOp op e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_if e0 e1 e2 e0r e1r e2r :
-  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (If e0 e1 e2) (If e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_pair e1 e2 e1r e2r :
-  Sub e1 e1r → Sub e2 e2r → Sub (Pair e1 e2) (Pair e1r e2r).
-Proof. by intros ??; red; f_equal/=. Qed.
-Global Instance do_wsubst_fst e er : Sub e er → Sub (Fst e) (Fst er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_snd e er : Sub e er → Sub (Snd e) (Snd er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_injL e er : Sub e er → Sub (InjL e) (InjL er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_injR e er : Sub e er → Sub (InjR e) (InjR er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_case e0 e1 e2 e0r e1r e2r :
-  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (Case e0 e1 e2) (Case e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_fork e er : Sub e er → Sub (Fork e) (Fork er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_alloc e er : Sub e er → Sub (Alloc e) (Alloc er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_load e er : Sub e er → Sub (Load e) (Load er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_store e1 e2 e1r e2r :
-  Sub e1 e1r → Sub e2 e2r → Sub (Store e1 e2) (Store e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_wsubst_cas e0 e1 e2 e0r e1r e2r :
-  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (CAS e0 e1 e2) (CAS e0r e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-End wsubst.
-
-(** * The tactic *)
-Lemma do_subst {X} (x: string) (es: expr []) (e: expr (x :: X)) (er: expr X) :
-  WSubst x es (λ _, id) e er → subst x es e = er.
-Proof. done. Qed.
-
-Ltac simpl_subst :=
-  repeat match goal with
-  | |- context [subst ?x ?es ?e] => progress rewrite (@do_subst _ x es e)
-  | |- _ => progress csimpl
-  end.
-Arguments wexpr : simpl never.
-Arguments subst : simpl never.
-Arguments wsubst : simpl never.

heap_lang/tactics.v

-From iris.heap_lang Require Export substitution.
+From iris.heap_lang Require Export lang.
 From iris.prelude Require Import fin_maps.
 Import heap_lang.
 
+(** We define an alternative representation of expressions in which the
+embedding of values and closed expressions is explicit. By reification of
+expressions into this type we can implementation substitution, closedness
+checking, atomic checking, and conversion into values, by computation. *)
+Module W.
+Inductive expr :=
+  | Val (v : val)
+  | ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Rec (f x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* Base types and their operations *)
+  | Lit (l : base_lit)
+  | UnOp (op : un_op) (e : expr)
+  | BinOp (op : bin_op) (e1 e2 : expr)
+  | If (e0 e1 e2 : expr)
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : expr) (e2 : expr)
+  (* Concurrency *)
+  | Fork (e : expr)
+  (* Heap *)
+  | Alloc (e : expr)
+  | Load (e : expr)
+  | Store (e1 : expr) (e2 : expr)
+  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
+
+Fixpoint to_expr (e : expr) : heap_lang.expr :=
+  match e with
+  | Val v => of_val v
+  | ClosedExpr e _ => e
+  | Var x => heap_lang.Var x
+  | Rec f x e => heap_lang.Rec f x (to_expr e)
+  | App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
+  | Lit l => heap_lang.Lit l
+  | UnOp op e => heap_lang.UnOp op (to_expr e)
+  | BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
+  | If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
+  | Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
+  | Fst e => heap_lang.Fst (to_expr e)
+  | Snd e => heap_lang.Snd (to_expr e)
+  | InjL e => heap_lang.InjL (to_expr e)
+  | InjR e => heap_lang.InjR (to_expr e)
+  | Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
+  | Fork e => heap_lang.Fork (to_expr e)
+  | Alloc e => heap_lang.Alloc (to_expr e)
+  | Load e => heap_lang.Load (to_expr e)
+  | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
+  | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
+  end.
+
+Ltac of_expr e :=
+  lazymatch e with
+  | heap_lang.Var ?x => constr:(Var x)
+  | heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
+  | heap_lang.App ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
+  | heap_lang.Lit ?l => constr:(Lit l)
+  | heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
+  | heap_lang.BinOp ?op ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
+  | heap_lang.If ?e0 ?e1 ?e2 =>
+     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
+     constr:(If e0 e1 e2)
+  | heap_lang.Pair ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
+  | heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
+  | heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
+  | heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
+  | heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
+  | heap_lang.Case ?e0 ?e1 ?e2 =>
+     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
+     constr:(Case e0 e1 e2)
+  | heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
+  | heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
+  | heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
+  | heap_lang.Store ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
+  | heap_lang.CAS ?e0 ?e1 ?e2 =>
+     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
+     constr:(CAS e0 e1 e2)
+  | to_expr ?e => e
+  | of_val ?v => constr:(Val v)
+  | _ => constr:(ltac:(
+     match goal with H : Closed [] e |- _ => exact (@ClosedExpr e H) end))
+  end.
+
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Val _ | ClosedExpr _ _ => true
+  | Var x => bool_decide (x ∈ X)
+  | Rec f x e => is_closed (f :b: x :b: X) e
+  | Lit _ => true
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
+     is_closed X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
+     is_closed X e1 && is_closed X e2
+  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
+     is_closed X e0 && is_closed X e1 && is_closed X e2
+  end.
+Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e).
+Proof.
+  revert X.
+  induction e; naive_solver eauto using is_closed_of_val, is_closed_weaken_nil.
+Qed.
+
+(* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
+constructors are only generated for closed expressions of which we know nothing
+about apart from being closed. Notice that the reverse implication of
+[to_val_Some] thus does not hold. *)
+Fixpoint to_val (e : expr) : option val :=
+  match e with
+  | Val v => Some v
+  | Rec f x e =>
+     if decide (is_closed (f :b: x :b: []) e) is left H
+     then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) else None
+  | Lit l => Some (LitV l)
+  | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
+  | InjL e => InjLV <$> to_val e
+  | InjR e => InjRV <$> to_val e
+  | _ => None
+  end.
+Lemma to_val_Some e v :
+  to_val e = Some v → heap_lang.to_val (to_expr e) = Some v.
+Proof.
+  revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
+  - do 2 f_equal. apply proof_irrel.
+  - exfalso. unfold Closed in *; eauto using is_closed_correct.
+Qed.
+Lemma to_val_is_Some e :
+  is_Some (to_val e) → is_Some (heap_lang.to_val (to_expr e)).
+Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
+
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Val v => Val v
+  | ClosedExpr e H => @ClosedExpr e H
+  | Var y => if decide (x = y) then es else Var y
+  | Rec f y e =>
+     Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | Lit l => Lit l
+  | UnOp op e => UnOp op (subst x es e)
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
+  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
+  | Fst e => Fst (subst x es e)
+  | Snd e => Snd (subst x es e)
+  | InjL e => InjL (subst x es e)
+  | InjR e => InjR (subst x es e)
+  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
+  | Fork e => Fork (subst x es e)
+  | Alloc e => Alloc (subst x es e)
+  | Load e => Load (subst x es e)
+  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
+  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
+  end.
+Lemma to_expr_subst x er e :
+  to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
+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 :=
+  match goal with
+  | |- Closed ?X ?e =>
+     let e' := W.of_expr e in change (Closed X (W.to_expr e'));
+     apply W.is_closed_correct; vm_compute; exact I
+  end.
+Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
+
+Ltac solve_to_val :=
+  try match goal with
+  | |- context E [language.to_val ?e] =>
+     let X := context E [to_val e] in change X
+  end;
+  match goal with
+  | |- to_val ?e = Some ?v =>
+     let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
+     apply W.to_val_Some; simpl; reflexivity
+  | |- is_Some (to_val ?e) =>
+     let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
+     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;
+  repeat match goal with
+  | |- context [subst ?x ?er ?e] =>
+      let er' := W.of_expr er in let e' := W.of_expr e in
+      change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
+      rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
+  end;
+  unfold W.to_expr.
+Arguments W.to_expr : simpl never.
+Arguments subst : simpl never.
+
 (** 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
@@ -25,7 +261,6 @@ Ltac reshape_val e tac :=
   let rec go e :=
   match e with
   | of_val ?v => v
-  | wexpr' ?e => go e
   | Rec ?f ?x ?e => constr:(RecV f x e)
   | Lit ?l => constr:(LitV l)
   | Pair ?e1 ?e2 =>

heap_lang/wp_tactics.v

 From iris.algebra Require Export upred_tactics.
-From iris.heap_lang Require Export tactics derived substitution.
+From iris.heap_lang Require Export tactics derived.
 Import uPred.
 
 (** wp-specific helper tactics *)
@@ -9,7 +9,15 @@ Ltac wp_bind K :=
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
-Ltac wp_done := rewrite /= ?to_of_val; fast_done.
+(* Solves side-conditions generated by the wp tactics *)
+Ltac wp_done :=
+  match goal with
+  | |- Closed _ _ => solve_closed
+  | |- is_Some (to_val _) => solve_to_val
+  | |- to_val _ = Some _ => solve_to_val
+  | |- language.to_val _ = Some _ => solve_to_val
+  | _ => fast_done
+  end.
 
 (* sometimes, we will have to do a final view shift, so only apply
 pvs_intro if we obtain a consecutive wp *)

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;

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;

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;

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 Λ Σ.

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