WIP: port F_mu_ref_conc to new Iris

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2018-10-05.4.464c2449") | (= "dev") }
+  "coq-iris" { (= "dev.2018-10-22.2.46e20e91") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/logrel/F_mu_ref_conc/context_refinement.v

@@ -191,8 +191,8 @@ Definition ctx_refines (Γ : list type)
   typed Γ e τ ∧ typed Γ e' τ ∧
   ∀ K thp σ v,
   typed_ctx K Γ τ [] TUnit →
-  rtc step ([fill_ctx K e], ∅) (of_val v :: thp, σ) →
-  ∃ thp' σ' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ').
+  rtc erased_step ([fill_ctx K e], ∅) (of_val v :: thp, σ) →
+  ∃ thp' σ' v', rtc erased_step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ').
 Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
   (ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
 

theories/logrel/F_mu_ref_conc/lang.v

@@ -172,62 +172,62 @@ Module F_mu_ref_conc.
 
   Definition state : Type := gmap loc val.
 
-  Inductive head_step : expr → state → expr → state → list expr → Prop :=
+  Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
   (* β *)
   | BetaS e1 e2 v2 σ :
       to_val e2 = Some v2 →
-      head_step (App (Rec e1) e2) σ e1.[(Rec e1), e2/] σ []
+      head_step (App (Rec e1) e2) σ [] e1.[(Rec e1), e2/] σ []
   (* Products *)
   | FstS e1 v1 e2 v2 σ :
       to_val e1 = Some v1 → to_val e2 = Some v2 →
-      head_step (Fst (Pair e1 e2)) σ e1 σ []
+      head_step (Fst (Pair e1 e2)) σ [] e1 σ []
   | SndS e1 v1 e2 v2 σ :
       to_val e1 = Some v1 → to_val e2 = Some v2 →
-      head_step (Snd (Pair e1 e2)) σ e2 σ []
+      head_step (Snd (Pair e1 e2)) σ [] e2 σ []
   (* Sums *)
   | CaseLS e0 v0 e1 e2 σ :
       to_val e0 = Some v0 →
-      head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ []
+      head_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
   | CaseRS e0 v0 e1 e2 σ :
       to_val e0 = Some v0 →
-      head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ []
+      head_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
     (* nat bin op *)
   | BinOpS op a b σ :
-      head_step (BinOp op (#n a) (#n b)) σ (of_val (binop_eval op a b)) σ []
+      head_step (BinOp op (#n a) (#n b)) σ [] (of_val (binop_eval op a b)) σ []
   (* If then else *)
   | IfFalse e1 e2 σ :
-      head_step (If (#♭ false) e1 e2) σ e2 σ []
+      head_step (If (#♭ false) e1 e2) σ [] e2 σ []
   | IfTrue e1 e2 σ :
-      head_step (If (#♭ true) e1 e2) σ e1 σ []
+      head_step (If (#♭ true) e1 e2) σ [] e1 σ []
   (* Recursive Types *)
   | Unfold_Fold e v σ :
       to_val e = Some v →
-      head_step (Unfold (Fold e)) σ e σ []
+      head_step (Unfold (Fold e)) σ [] e σ []
   (* Polymorphic Types *)
   | TBeta e σ :
-      head_step (TApp (TLam e)) σ e σ []
+      head_step (TApp (TLam e)) σ [] e σ []
   (* Concurrency *)
   | ForkS e σ:
-      head_step (Fork e) σ Unit σ [e]
+      head_step (Fork e) σ [] Unit σ [e]
   (* Reference Types *)
   | AllocS e v σ l :
      to_val e = Some v → σ !! l = None →
-     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) []
+     head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) []
   | LoadS l v σ :
      σ !! l = Some v →
-     head_step (Load (Loc l)) σ (of_val v) σ []
+     head_step (Load (Loc l)) σ [] (of_val v) σ []
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Loc l) e) σ Unit (<[l:=v]>σ) []
+     head_step (Store (Loc l) e) σ [] Unit (<[l:=v]>σ) []
   (* Compare and swap *)
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some vl → vl ≠ v1 →
-     head_step (CAS (Loc l) e1 e2) σ (#♭ false) σ []
+     head_step (CAS (Loc l) e1 e2) σ [] (#♭ false) σ []
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some v1 →
-     head_step (CAS (Loc l) e1 e2) σ (#♭ true) (<[l:=v2]>σ) [].
+     head_step (CAS (Loc l) e1 e2) σ [] (#♭ true) (<[l:=v2]>σ) [].
 
   (** Basic properties about the language *)
   Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -248,12 +248,12 @@ Module F_mu_ref_conc.
   Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
   Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.
 
-  Lemma val_stuck e1 σ1 e2 σ2 ef :
-    head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+  Lemma val_stuck e1 σ1 κs e2 σ2 ef :
+    head_step e1 σ1 κs e2 σ2 ef → to_val e1 = None.
   Proof. destruct 1; naive_solver. 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).
+  Lemma head_ctx_step_val Ki e σ1 κs e2 σ2 ef :
+    head_step (fill_item Ki e) σ1 κs e2 σ2 ef → is_Some (to_val e).
   Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
 
   Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -268,10 +268,10 @@ Module F_mu_ref_conc.
 
   Lemma alloc_fresh e v σ :
     let l := fresh (dom (gset loc) σ) in
-    to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) [].
+    to_val e = Some v → head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) [].
   Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 
-  Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+  Lemma val_head_stuck e1 σ1 κs e2 σ2 efs : head_step e1 σ1 κs e2 σ2 efs → to_val e1 = None.
   Proof. destruct 1; naive_solver. Qed.
 
   Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.

theories/logrel/F_mu_ref_conc/rules.v

@@ -16,7 +16,7 @@ Class heapIG Σ := HeapIG {
 
 Instance heapIG_irisG `{heapIG Σ} : irisG F_mu_ref_conc_lang Σ := {
   iris_invG := heapI_invG;
-  state_interp := gen_heap_ctx
+  state_interp σ κs := gen_heap_ctx σ
 }.
 Global Opaque iris_invG.
 
@@ -38,14 +38,14 @@ Section lang_rules.
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
   | H : _ = of_val ?v |- _ =>
      is_var v; destruct v; first[discriminate H|injection H as H]
-  | H : head_step ?e _ _ _ _ |- _ =>
+  | 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 (atomic _) => solve_atomic.
-  Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
+  Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
 
   Local Hint Constructors head_step.
   Local Hint Resolve alloc_fresh.
@@ -57,7 +57,7 @@ Section lang_rules.
     {{{ True }}} Alloc e @ E {{{ l, RET (LocV l); l ↦ᵢ v }}}.
   Proof.
     iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-    iIntros (σ1) "Hσ !>"; iSplit; first by auto.
+    iIntros (σ1 ??) "Hσ !>"; iSplit; first by auto.
     iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
     iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
     iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -67,7 +67,7 @@ Section lang_rules.
   {{{ ▷ l ↦ᵢ{q} v }}} Load (Loc l) @ 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 %?.
+    iIntros (σ1 ??) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
     iSplit; first by eauto.
     iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
     iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -80,7 +80,7 @@ Section lang_rules.
   Proof.
     iIntros (<- Φ) ">Hl HΦ".
     iApply wp_lift_atomic_head_step_no_fork; auto.
-    iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+    iIntros (σ1 ??) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
     iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
     iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
     iModIntro. iSplit=>//. by iApply "HΦ".
@@ -93,7 +93,7 @@ Section lang_rules.
   Proof.
     iIntros (<- <- ? Φ) ">Hl HΦ".
     iApply wp_lift_atomic_head_step_no_fork; auto.
-    iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+    iIntros (σ1 ??) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
     iSplit; first by eauto.
     iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
     iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -106,7 +106,7 @@ Section lang_rules.
   Proof.
     iIntros (<- <- Φ) ">Hl HΦ".
     iApply wp_lift_atomic_head_step_no_fork; auto.
-    iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+    iIntros (σ1 ??) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
     iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
     iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
     iModIntro. iSplit=>//. by iApply "HΦ".

theories/logrel/F_mu_ref_conc/rules_binary.v

@@ -31,7 +31,7 @@ Section definitionsS.
 
   Definition spec_inv (ρ : cfg F_mu_ref_conc_lang) : iProp Σ :=
     (∃ tp σ, own cfg_name (● (to_tpool tp, to_gen_heap σ))
-                 ∗ ⌜rtc step ρ (tp,σ)⌝)%I.
+                 ∗ ⌜rtc erased_step ρ (tp,σ)⌝)%I.
   Definition spec_ctx (ρ : cfg F_mu_ref_conc_lang) : iProp Σ :=
     inv specN (spec_inv ρ).
 
@@ -135,24 +135,24 @@ Section cfg.
   Local Hint Resolve to_tpool_insert'.
   Local Hint Resolve tpool_singleton_included.
 
-  Lemma step_insert K tp j e σ e' σ' efs :
-    tp !! j = Some (fill K e) → head_step e σ e' σ' efs →
-    step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
+  Lemma step_insert K tp j e σ κ e' σ' efs :
+    tp !! j = Some (fill K e) → head_step e σ κ e' σ' efs →
+    erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
   Proof.
     intros. rewrite -(take_drop_middle tp j (fill K e)) //.
     rewrite insert_app_r_alt take_length_le ?Nat.sub_diag /=;
       eauto using lookup_lt_Some, Nat.lt_le_incl.
-    rewrite -(assoc_L (++)) /=.
+    rewrite -(assoc_L (++)) /=. eexists.
     eapply step_atomic; eauto. by apply: Ectx_step'.
   Qed.
 
-  Lemma step_insert_no_fork K tp j e σ e' σ' :
-    tp !! j = Some (fill K e) → head_step e σ e' σ' [] →
-    step (tp, σ) (<[j:=fill K e']> tp, σ').
+  Lemma step_insert_no_fork K tp j e σ κ e' σ' :
+    tp !! j = Some (fill K e) → head_step e σ κ e' σ' [] →
+    erased_step (tp, σ) (<[j:=fill K e']> tp, σ').
   Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
 
   Lemma step_pure E ρ j K e e' :
-    (∀ σ, head_step e σ e' σ []) →
+    (∀ σ, head_step e σ [] e' σ []) →
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
   Proof.

theories/logrel/F_mu_ref_conc/soundness_binary.v

@@ -7,13 +7,13 @@ From iris_examples.logrel.F_mu_ref_conc Require Import soundness_unary.
 Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
     e e' τ v thp hp :
   (∀ `{heapIG Σ, cfgSG Σ}, [] ⊨ e ≤log≤ e' : τ) →
-  rtc step ([e], ∅) (of_val v :: thp, hp) →
-  (∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp')).
+  rtc erased_step ([e], ∅) (of_val v :: thp, hp) →
+  (∃ thp' hp' v', rtc erased_step ([e'], ∅) (of_val v' :: thp', hp')).
 Proof.
   intros Hlog Hsteps.
-  cut (adequate NotStuck e ∅ (λ _ _, ∃ thp' h v, rtc step ([e'], ∅) (of_val v :: thp', h))).
+  cut (adequate NotStuck e ∅ (λ _ _, ∃ thp' h v, rtc erased_step ([e'], ∅) (of_val v :: thp', h))).
   { destruct 1; naive_solver. }
-  eapply (wp_adequacy Σ _); iIntros (Hinv).
+  eapply (wp_adequacy Σ _); iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
   { apply (auth_auth_valid _ (to_gen_heap_valid _ _ ∅)). }
   iMod (own_alloc (● (to_tpool [e'], ∅)
@@ -23,7 +23,7 @@ Proof.
   iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
   set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
-  iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
+  iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
   iApply wp_fupd. iApply wp_wand_r.
   iSplitL.
   iPoseProof ((Hlog _ _ [] [] ([e'], ∅)) with "[$Hcfg]") as "Hrel".

theories/logrel/F_mu_ref_conc/soundness_unary.v

@@ -10,14 +10,14 @@ Class heapPreIG Σ := HeapPreIG {
 
 Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
   (∀ `{heapIG Σ}, [] ⊨ e : τ) →
-  rtc step ([e], σ) (thp, σ') → e' ∈ thp →
+  rtc erased_step ([e], σ) (thp, σ') → e' ∈ thp →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
-  eapply (wp_adequacy Σ _). iIntros (Hinv).
+  eapply (wp_adequacy Σ _). iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
   { apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
-  iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
+  iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
   set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
   iApply (wp_wand with "[]").
   - rewrite -(empty_env_subst e).
@@ -27,7 +27,7 @@ Qed.
 
 Corollary type_soundness e τ e' thp σ σ' :
   [] ⊢ₜ e : τ →
-  rtc step ([e], σ) (thp, σ') → e' ∈ thp →
+  rtc erased_step ([e], σ) (thp, σ') → e' ∈ thp →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
   intros ??. set (Σ := #[invΣ ; gen_heapΣ loc F_mu_ref_conc.val]).