bump Iris

opam

@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-05-28.0.daeeaf05") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-07-04.2.34f64c8d") | (= "dev") }
 ]

theories/lang/lang.v

@@ -637,14 +637,14 @@ Proof.
 Qed.
 
 (* Define some derived forms *)
-Notation Lam xl e := (Rec BAnon xl e).
-Notation Let x e1 e2 := (App (Lam [x] e2) [e1]).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV xl e := (RecV BAnon xl e).
+Notation Lam xl e := (Rec BAnon xl e) (only parsing).
+Notation Let x e1 e2 := (App (Lam [x] e2) [e1]) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation LamV xl e := (RecV BAnon xl e) (only parsing).
 Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
 Notation SeqCtx e2 := (LetCtx BAnon e2).
 Notation Skip := (Seq (Lit LitPoison) (Lit LitPoison)).
 Coercion lit_of_bool : bool >-> base_lit.
-Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))).
+Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))) (only parsing).
 Notation Newlft := (Lit LitPoison) (only parsing).
 Notation Endlft := Skip (only parsing).

theories/lang/lib/spawn.v

@@ -66,7 +66,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   {{{ ∀ c, finish_handle c Ψ -∗ WP f [ #c] {{ _, True }} }}}
     spawn [e] {{{ c, RET #c; join_handle c Ψ }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=.
+  iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
   wp_let. wp_alloc l as "Hl" "H†". wp_let.
   iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
   iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.

theories/lang/lifting.v

@@ -88,7 +88,10 @@ Global Instance pure_rec e f xl erec erec' el :
   Closed (f :b: xl +b+ []) erec →
   DoSubstL (f :: xl) (e :: el) erec erec' →
   PureExec True (App e el) erec'.
-Proof. rewrite /AsRec /DoSubstL=> -> /TCForall_Forall ???. solve_pure_exec. Qed.
+Proof.
+  rewrite /AsRec /DoSubstL=> -> /TCForall_Forall Hel ??. solve_pure_exec.
+  eapply Forall_impl; [exact Hel|]. intros e' [v <-]. rewrite to_of_val; eauto.
+Qed.
 
 Global Instance pure_le n1 n2 :
   PureExec True (BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)))
@@ -189,7 +192,7 @@ Lemma wp_write_sc E l e v v' :
   {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
   {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iMod (heap_write _ _ _  v with "Hσ Hv") as "[Hσ Hv]".
   iModIntro; iSplit; first by eauto.
@@ -202,7 +205,7 @@ Lemma wp_write_na E l e v v' :
   {{{ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
   {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) ">Hv HΦ".
+  iIntros (<- Φ) ">Hv HΦ".
   iApply wp_lift_head_step; auto. iIntros (σ1) "Hσ".
   iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
   iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
@@ -222,7 +225,7 @@ Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
     CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
   {{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) ">Hv HΦ".
+  iIntros (<- ? Φ) ">Hv HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
   iModIntro; iSplit; first by eauto.
@@ -236,7 +239,7 @@ Lemma wp_cas_suc E l lit1 e2 lit2 :
     CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
   {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) ">Hv HΦ".
+  iIntros (<- ? Φ) ">Hv HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iModIntro; iSplit; first (destruct lit1; by eauto).
@@ -266,7 +269,7 @@ Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
   {{{ RET LitV (LitInt 0);
       l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
+  iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
   iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
@@ -284,7 +287,7 @@ Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
       if b is true then l ↦ LitV (LitLoc l2)
       else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll) }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) ">Hv HΦ".
+  iIntros (<- Φ) ">Hv HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
@@ -336,14 +339,13 @@ Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el))
                     WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
     WP App f ((of_val <$> vs) ++ el) @ E {{ Φ }}.
 Proof.
-  intros [vf Hf]. revert vs Ql.
+  intros [vf <-]. revert vs Ql.
   induction el as [|e el IH]=>/= vs Ql; inv_vec Ql; simpl.
   - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r /=. by iApply "H".
   - iIntros (Q Ql) "[He Hl] HΦ".
-    assert (App f ((of_val <$> vs) ++ e :: el) = fill_item (AppRCtx vf vs el) e)
-      as -> by rewrite /= (of_to_val f) //.
+    change (App (of_val vf) ((of_val <$> vs) ++ e :: el)) with (fill_item (AppRCtx vf vs el) e).
     iApply wp_bind. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
-    rewrite cons_middle (assoc app) -(fmap_app _ _ [v]) (of_to_val f) //.
+    rewrite cons_middle (assoc app) -(fmap_app _ _ [v]).
     iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
     iApply ("HΦ" $! (v:::vl)). iFrame.
 Qed.

theories/lang/proofmode.v

 From iris.program_logic Require Export weakestpre.
-From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
 From lrust.lang Require Export tactics lifting.
 From iris.program_logic Require Import lifting.
@@ -11,7 +11,7 @@ Lemma tac_wp_value `{lrustG Σ} Δ E Φ e v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
 
-Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
+Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
 
 Lemma tac_wp_pure `{lrustG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
@@ -30,9 +30,9 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
-    [simpl; apply _                 (* PureExec *)
+    [simpl; iSolveTC                (* PureExec *)
     |try done                       (* The pure condition for PureExec *)
-    |apply _                        (* IntoLaters *)
+    |iSolveTC                       (* IntoLaters *)
     |simpl_subst; try wp_value_head (* new goal *)])
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
   | _ => fail "wp_pure: not a 'wp'"
@@ -55,7 +55,7 @@ Tactic Notation "wp_eq_loc" :=
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
      reshape_expr e ltac:(fun K e' => eapply (tac_wp_eq_loc K));
-       [apply _|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
+       [iSolveTC|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
@@ -105,7 +105,7 @@ Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
 Proof.
   rewrite envs_entails_eq=> ?? HΔ. rewrite -wp_bind.
   eapply wand_apply; first exact:wp_alloc.
-  rewrite -persistent_and_sep. apply and_intro; first auto with I.
+  rewrite -persistent_and_sep. apply and_intro; first by auto.
   rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
   apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
   rewrite sep_and. apply pure_elim_l=> Hn. apply wand_elim_r'.
@@ -185,7 +185,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc K _ _ _ H Hf))
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     [try fast_done
-    |apply _
+    |iSolveTC
     |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
      first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
      (* If Hsz is "constant Z = nat", change that to an equation on nat and
@@ -197,7 +197,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
                (* Substitute only if we have a literal nat. *)
                match goal with Hsz : S _ = _ |- _ => subst sz end));
       eexists; split;
-        [env_cbv; reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
+        [pm_reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
         |simpl; try wp_value_head]]
   | _ => fail "wp_alloc: not a 'wp'"
   end.
@@ -213,13 +213,13 @@ Tactic Notation "wp_free" :=
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free K))
       |fail 1 "wp_free: cannot find 'Free' in" e];
     [try fast_done
-    |apply _
+    |iSolveTC
     |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
      iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
      iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |try fast_done
     |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
   | _ => fail "wp_free: not a 'wp'"
@@ -234,7 +234,7 @@ Tactic Notation "wp_read" :=
       |fail 1 "wp_read: cannot find 'Read' in" e];
     [(right; fast_done) || (left; fast_done) ||
      fail "wp_read: order is neither Na2Ord nor ScOrd"
-    |apply _
+    |iSolveTC
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
     |simpl; try wp_value_head]
@@ -246,14 +246,14 @@ Tactic Notation "wp_write" :=
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [apply _|..])
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [iSolveTC|..])
       |fail 1 "wp_write: cannot find 'Write' in" e];
     [(right; fast_done) || (left; fast_done) ||
      fail "wp_write: order is neither Na2Ord nor ScOrd"
-    |apply _
+    |iSolveTC
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
   | _ => fail "wp_write: not a 'wp'"
   end.

theories/lang/races.v

@@ -12,14 +12,14 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
 | Access_read ord l σ :
     next_access_head (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
 | Access_write ord l e σ :
-    AsVal e →
+    is_Some (to_val e) →
     next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
 | Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
-    IntoVal e1 (LitV lit1) → IntoVal e2 (LitV lit2) →
+    to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
     lit_neq lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
 | Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
-    IntoVal e1 (LitV lit1) → IntoVal e2 (LitV lit2) →
+    to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
     lit_eq σ lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
 | Access_free n l σ i :
@@ -95,7 +95,7 @@ Lemma next_access_head_reducible_state e σ a l :
 Proof.
   intros Ha (e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
   - destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
-    eapply CasStuckS; done.
+    by eapply CasStuckS.
   - exfalso. eapply Hrednonstuck; last done.
     eapply CasStuckS; done.
   - match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
@@ -106,7 +106,7 @@ Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 a l :
   head_step e1 σ1 e2 σ2 ef →
   next_access_head e2 σ2 (a, Na2Ord) l.
 Proof.
-  intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor; apply _.
+  intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor; by rewrite to_of_val.
 Qed.
 
 Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' a1 a2 l :

theories/lang/tactics.v

@@ -107,15 +107,16 @@ Definition to_val (e : expr) : option val :=
   | _ => None
   end.
 Lemma to_val_Some e v :
-  to_val e = Some v → lang.to_val (to_expr e) = Some v.
+  to_val e = Some v → of_val v = W.to_expr e.
 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.
+  revert v. induction e; intros; simplify_option_eq; auto using of_to_val.
 Qed.
 Lemma to_val_is_Some e :
-  is_Some (to_val e) → is_Some (lang.to_val (to_expr e)).
+  is_Some (to_val e) → ∃ v, of_val v = to_expr e.
 Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
+Lemma to_val_is_Some' e :
+  is_Some (to_val e) → is_Some (lang.to_val (to_expr e)).
+Proof. intros [v ?]%to_val_is_Some. exists v. rewrite -to_of_val. by f_equal. Qed.
 
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
@@ -164,7 +165,7 @@ Proof.
     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.
+    try naive_solver eauto using to_val_is_Some'.
 Qed.
 End W.
 
@@ -176,23 +177,22 @@ Ltac solve_closed :=
   end.
 Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 
-Ltac solve_to_val :=
-  rewrite /IntoVal /AsVal;
-  try match goal with
-  | |- context E [language.to_val ?e] =>
-     let X := context E [to_val e] in change X
-  end;
+Ltac solve_into_val :=
   match goal with
-  | |- to_val ?e = Some ?v =>
-     let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
+  | |- IntoVal ?e ?v =>
+     let e' := W.of_expr e in change (of_val v = W.to_expr e');
      apply W.to_val_Some; simpl; unfold W.to_expr;
      ((unlock; exact eq_refl) || (idtac; exact eq_refl))
-  | |- is_Some (to_val ?e) =>
-     let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
+  end.
+Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
+
+Ltac solve_as_val :=
+  match goal with
+  | |- AsVal ?e =>
+     let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
-Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances.
-Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
+Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with

theories/typing/function.v

@@ -249,8 +249,8 @@ Section typing.
              WP k [of_val ret] {{ _, cont_postcondition }}) -∗
     WP (call: p ps → k) {{ _, cont_postcondition }}.
   Proof.
-    iIntros (HE [k' Hk']) "#LFT #HE Htl HL Hκs Hf Hargs Hk". rewrite -(of_to_val k k') //.
-    clear dependent k. wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
+    iIntros (HE [k' <-]) "#LFT #HE Htl HL Hκs Hf Hargs Hk".
+    wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#☠ ;; #☠) ;; k' ["_r"])%V⌝):::
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
             with "[Hargs]").
@@ -402,7 +402,7 @@ Section typing.
                      (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn fp).
   Proof.
-    iIntros (<-%of_to_val ->) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
+    iIntros (<- ->) "#Hbody /=". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
     iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.

theories/typing/type_context.v

@@ -38,12 +38,13 @@ Section type_context.
   Lemma wp_eval_path E p v :
     eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
   Proof.
-    revert v; induction p; intros v; cbn -[to_val];
-      try (simpl; intros ?; simplify_eq; by iApply wp_value); [].
-    destruct op; try discriminate; [].
+    revert v; induction p; intros v; try done.
+    { intros [=]. by iApply wp_value. }
+    { move=> /of_to_val=> ?. by iApply wp_value. }
+    simpl. destruct op; try discriminate; [].
     destruct p2; try (intros ?; by iApply wp_value); [].
     destruct l; try (intros ?; by iApply wp_value); [].
-    destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
+    destruct (eval_path p1); try done.
     destruct v0; try discriminate; [].
     destruct l; try discriminate; [].
     intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").