From 9ef37d07f8ff3cfe6b9187ede7335477268b07d9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 28 Jun 2019 22:12:05 +0200
Subject: [PATCH] bump Iris; adjust for removal of val_for_compare and partial
EqOp
---
opam | 2 +-
theories/logatom/conditional_increment/cinc.v | 2 +-
theories/logatom/elimination_stack/stack.v | 9 +--
theories/logatom/proph_erasure.v | 75 +++++++++++--------
theories/logatom/treiber2.v | 2 +-
theories/logrel_heaplang/ltyping.v | 9 ++-
6 files changed, 54 insertions(+), 45 deletions(-)
diff --git a/opam b/opam
index 7976e0d3..31209ec9 100644
--- a/opam
+++ b/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.2019-06-27.2.1b53e5dd") | (= "dev") }
+ "coq-iris" { (= "dev.2019-07-01.1.6e79f000") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index 15cf9724..694e4558 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -419,7 +419,7 @@ Section conditional_counter.
iModIntro. iSplitL "Hc Hrest Hl'". { eauto 10 with iFrame. }
(* two equal proofs depending on value of b1 *)
wp_pures.
- destruct (bool_decide (val_for_compare b = #true));
+ destruct (bool_decide (b = #true));
wp_alloc Hl_new as "Hl_new"; wp_pures;
iApply (complete_failing_thread
with "InvC InvS HQ Hl_new"); done.
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 5b824184..1df2057c 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -106,10 +106,6 @@ Section stack.
Local Instance stack_elem_to_val_inj : Inj (=) (=) stack_elem_to_val.
Proof. rewrite /Inj /stack_elem_to_val=>??. repeat case_match; congruence. Qed.
- Lemma stack_elem_to_val_for_compare rep :
- val_for_compare (stack_elem_to_val rep) = stack_elem_to_val rep.
- Proof. destruct rep; done. Qed.
-
Fixpoint list_inv (l : list val) (rep : option loc) : iProp :=
match l with
| nil => ⌜rep = NoneâŒ
@@ -207,7 +203,7 @@ Section stack.
awp_apply cas_spec; [by destruct stack_rep|].
iInv stackN as (stack_rep' offer_rep l) "(>Hs◠& >H↦ & Hlist & Hoffer)".
iAaccIntro with "H↦"; first by eauto 10 with iFrame.
- iIntros "H↦". rewrite !stack_elem_to_val_for_compare.
+ iIntros "H↦".
destruct (decide (stack_elem_to_val stack_rep' = stack_elem_to_val stack_rep)) as
[->%stack_elem_to_val_inj|_].
- (* The CAS succeeded. Update everything accordingly. *)
@@ -303,7 +299,6 @@ Section stack.
iInv stackN as (stack_rep offer_rep l) "(>Hs◠& >H↦ & Hlist & Hrem)".
iAaccIntro with "H↦"; first by eauto 10 with iFrame.
iIntros "H↦". change (InjRV #tail) with (stack_elem_to_val (Some tail)).
- rewrite !stack_elem_to_val_for_compare.
destruct (decide (stack_elem_to_val stack_rep = stack_elem_to_val (Some tail))) as
[->%stack_elem_to_val_inj|_].
+ (* CAS succeeded! It must still be the same head element in the list,
@@ -338,7 +333,7 @@ Section stack.
iDestruct "Hoff" as (Poff Qoff γo) "[#Hoinv #AUoff]".
iInv offerN as (offer_st) "[>Hoff↦ Hoff]".
iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame.
- iIntros "Hoff↦". simpl.
+ iIntros "Hoff↦".
destruct (decide (#(offer_state_rep offer_st) = #0)) as [Heq|_]; last first.
{ (* CAS failed, we don't do a thing. *)
iSplitR "AU"; first by eauto 10 with iFrame.
diff --git a/theories/logatom/proph_erasure.v b/theories/logatom/proph_erasure.v
index 93670cb0..a46bc708 100644
--- a/theories/logatom/proph_erasure.v
+++ b/theories/logatom/proph_erasure.v
@@ -29,7 +29,7 @@ Fixpoint erase_expr (e : expr) : expr :=
| Store e1 e2 => Store (erase_expr e1) (erase_expr e2)
| CmpXchg e0 e1 e2 => CmpXchg (erase_expr e0) (erase_expr e1) (erase_expr e2)
| FAA e1 e2 => FAA (erase_expr e1) (erase_expr e2)
- | NewProph => Skip
+ | NewProph => ((λ: <>, #LitErased)%V #())
| Resolve e0 e1 e2 => Fst (Fst (erase_expr e0, erase_expr e1, erase_expr e2))
end
with
@@ -38,7 +38,7 @@ erase_val (v : val) : val :=
| LitV l =>
LitV
match l with
- | LitProphecy p => LitUnit
+ | LitProphecy p => LitErased
| _ => l
end
| RecV f x e => RecV f x (erase_expr e)
@@ -185,24 +185,29 @@ Proof. rewrite /is_safe /reducible /=. eauto 10 using head_prim_step. Qed.
Lemma prim_step_safe e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → is_safe e σ.
Proof. rewrite /is_safe /reducible /=. eauto 10. Qed.
-Lemma val_for_compare_erase v1 v2 :
- val_for_compare v1 = val_for_compare v2 ↔
- val_for_compare (erase_val v1) = val_for_compare (erase_val v2).
+Lemma val_is_unboxed_erased v :
+ val_is_unboxed (erase_val v) ↔ val_is_unboxed v.
Proof.
- revert v2; induction v1; induction v2; split; intros Ho; simpl in *;
- repeat case_match; simpl in *; simplify_eq; eauto; firstorder.
+ destruct v; rewrite /= /lit_is_unboxed; repeat (done || simpl; case_match).
Qed.
-
-Lemma val_for_compare_erase_bdec v1 v2 :
- bool_decide (val_for_compare v1 = val_for_compare v2) =
- bool_decide (val_for_compare (erase_val v1) = val_for_compare (erase_val v2)).
-Proof. by apply bool_decide_iff; rewrite val_for_compare_erase. Qed.
-
-Lemma vals_cmpxchg_compare_safe_erase v1 v2 :
- vals_cmpxchg_compare_safe (erase_val v1) (erase_val v2) ↔
- vals_cmpxchg_compare_safe v1 v2.
+Lemma vals_compare_safe_erase v1 v2 :
+ vals_compare_safe (erase_val v1) (erase_val v2) ↔
+ vals_compare_safe v1 v2.
+Proof. rewrite /vals_compare_safe !val_is_unboxed_erased. done. Qed.
+Lemma vals_compare v1 v2 :
+ vals_compare_safe v1 v2 →
+ (v1 = v2) ↔ (erase_val v1 = erase_val v2).
+Proof.
+ destruct v1, v2; rewrite /= /lit_is_unboxed;
+ repeat (done || (by intros [[] | []]) || simpl; case_match).
+Qed.
+(* Rewrite with [vals_compare] does not work, so derive a version
+that wraps it in [bool_decide], that can be rewritten. *)
+Lemma vals_compare_bdec v1 v2 :
+ vals_compare_safe v1 v2 →
+ bool_decide (v1 = v2) = bool_decide (erase_val v1 = erase_val v2).
Proof.
- by destruct v1; destruct v2; repeat (done || simpl; case_match).
+ intros ?. eapply bool_decide_iff. apply vals_compare. done.
Qed.
(** if un_op_eval succeeds on erased value,
@@ -228,10 +233,14 @@ Proof.
simplify_eq; simpl in *; simplify_eq; eauto.
- eexists _; split; eauto; simpl.
erewrite bool_decide_iff; first by eauto.
- by rewrite val_for_compare_erase.
+ apply vals_compare. done.
- repeat f_equal.
erewrite bool_decide_iff; first by eauto.
- by rewrite -val_for_compare_erase.
+ symmetry. apply vals_compare. done.
+ - exfalso. match goal with H: ¬_ |- _ => apply H end.
+ eapply vals_compare_safe_erase. done.
+ - exfalso. match goal with H: ¬_ |- _ => apply H end.
+ eapply vals_compare_safe_erase. done.
Qed.
Lemma erase_heap_lookup h l : (erase_heap h) !! l = None ↔ h !! l = None.
@@ -332,7 +341,7 @@ Proof.
first match goal with
| |- head_step NewProph _ _ _ _ _ => by apply new_proph_id_fresh
| _ => by econstructor;
- eauto using erase_heap_lookup, val_for_compare_erase
+ eauto using erase_heap_lookup
end;
try rewrite -val_for_compare_erase;
rewrite ?erase_expr_subst' /erase_state ?erase_heap_insert /=;
@@ -344,21 +353,21 @@ Proof.
rewrite ?erase_heap_insert /=; eauto using erase_state_init.
- (* case of CmpXchg succeeding *)
match goal with
- | H : bool_decide (val_for_compare (erase_val _)
- = val_for_compare (erase_val _)) = _ |- _ =>
- rename H into Hvfc; rewrite -val_for_compare_erase_bdec in Hvfc
+ | H : bool_decide (erase_val _ = erase_val _) = _ |- _ =>
+ rename H into Hvfc
end.
+ rewrite -vals_compare_bdec in Hvfc; last by eapply vals_compare_safe_erase.
eexists _, _, _, _; simpl; split.
- { econstructor; first rewrite -vals_cmpxchg_compare_safe_erase; eauto. }
+ { econstructor; eauto. rewrite -vals_compare_safe_erase //. }
rewrite Hvfc /erase_state ?erase_heap_insert /=; eauto.
- (* case of CmpXchg failing *)
match goal with
- | H : bool_decide (val_for_compare (erase_val _)
- = val_for_compare (erase_val _)) = _ |- _ =>
- rename H into Hvfc; rewrite -val_for_compare_erase_bdec in Hvfc
+ | H : bool_decide (erase_val _ = erase_val _) = _ |- _ =>
+ rename H into Hvfc
end.
+ rewrite -vals_compare_bdec in Hvfc; last by eapply vals_compare_safe_erase.
eexists _, _, _, _; simpl; split.
- { econstructor; first rewrite -vals_cmpxchg_compare_safe_erase; eauto. }
+ { econstructor; eauto. rewrite -vals_compare_safe_erase //. }
rewrite Hvfc; eauto.
Qed.
@@ -655,21 +664,21 @@ Proof.
match goal with | H : is_Some _ |- _ => inversion H end.
do 3 eexists; apply head_prim_step; econstructor.
by rewrite /erase_state /state_upd_heap /= erase_heap_lookup' H0; eauto.
- - (* CAS-fail *)
+ - (* CmpXchg *)
match goal with
- | H : vals_cmpxchg_compare_safe ?A ?B |- _ =>
- destruct (bool_decide (val_for_compare A = val_for_compare B)) eqn:Heqvls
+ | H : vals_compare_safe ?A ?B |- _ =>
+ destruct (bool_decide (A = B)) eqn:Heqvls
end.
+ do 3 eexists; apply head_prim_step;
econstructor; last (by eauto);
- first (by apply vals_cmpxchg_compare_safe_erase); [].
+ last (by apply vals_compare_safe_erase); [].
match goal with
| H : heap _ !! _ = _ |- _ =>
by rewrite /erase_state /state_upd_heap /= erase_heap_lookup' H
end.
+ do 3 eexists; apply head_prim_step;
econstructor; last (by eauto);
- first (by apply vals_cmpxchg_compare_safe_erase); [].
+ last (by apply vals_compare_safe_erase); [].
match goal with
| H : heap _ !! _ = _ |- _ =>
by rewrite /erase_state /state_upd_heap /= erase_heap_lookup' H
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 50a2d615..50af9322 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -280,7 +280,7 @@ Proof.
(* And conclude the proof easily, after some computation steps. *)
wp_pures. iExact "H".
- (* The CAS failed. *)
- wp_cmpxchg_fail. { case u, w; simpl; congruence. }
+ wp_cmpxchg_fail. { exact: not_inj. }
{ case u, w; simpl; eauto. (* Administrative stuff. *) }
(* We can eliminate the modality. *)
iModIntro. iSplitL "Hγ◠Hl HPhys"; first by eauto 10 with iFrame.
diff --git a/theories/logrel_heaplang/ltyping.v b/theories/logrel_heaplang/ltyping.v
index a442e293..621b62ec 100644
--- a/theories/logrel_heaplang/ltyping.v
+++ b/theories/logrel_heaplang/ltyping.v
@@ -160,8 +160,13 @@ Section types_properties.
Proof. iIntros (v). by iDestruct 1 as (i ->) "?". Qed.
(* Operator typing *)
- Global Instance lty_bin_op_eq A : LTyBinOp EqOp A A lty_bool.
- Proof. iIntros (v1 v2) "_ _". rewrite /bin_op_eval /lty_car /=. eauto. Qed.
+ Global Instance lty_bin_op_eq A : LTyUnboxed A → LTyBinOp EqOp A A lty_bool.
+ Proof.
+ iIntros (? v1 v2) "A1 _". rewrite /bin_op_eval /lty_car /=.
+ iDestruct (lty_unboxed with "A1") as %Hunb.
+ rewrite decide_True; last solve_vals_compare_safe.
+ eauto.
+ Qed.
Global Instance lty_bin_op_arith op :
TCElemOf op [PlusOp; MinusOp; MultOp; QuotOp; RemOp;
AndOp; OrOp; XorOp; ShiftLOp; ShiftROp] →
--
GitLab