Commit da7641e9 authored by Ralf Jung's avatar Ralf Jung

bump Iris; adjust for partial EqOp

parent 5574a80a
Pipeline #19763 failed with stage
in 12 minutes and 30 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [ depends: [
"coq-iris" { (= "dev.2019-06-28.2.5b3f7de1") | (= "dev") } "coq-iris" { (= "dev.2019-07-01.1.6e79f000") | (= "dev") }
] ]
...@@ -62,7 +62,7 @@ Tactic Notation "cwp_pure" open_constr(efoc) := ...@@ -62,7 +62,7 @@ Tactic Notation "cwp_pure" open_constr(efoc) :=
eapply (tac_cwp_pure _ _ _ _ _ (fill K e')); eapply (tac_cwp_pure _ _ _ _ _ (fill K e'));
[tac_bind_helper (* e = fill K e' *) [tac_bind_helper (* e = fill K e' *)
|apply _ (* PureExec *) |apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *) |try solve_vals_compare_safe (* The pure condition for PureExec *)
|apply _ (* IntoLaters *) |apply _ (* IntoLaters *)
|simpl |simpl
]) ])
......
...@@ -323,9 +323,6 @@ Section properties. ...@@ -323,9 +323,6 @@ Section properties.
Qed. Qed.
Global Instance cloc_to_val_inj : Inj (=) (=) cloc_to_val. Global Instance cloc_to_val_inj : Inj (=) (=) cloc_to_val.
Proof. intros cl1 cl2 Hcl. apply (inj Some). by rewrite -!cloc_of_to_val Hcl. Qed. Proof. intros cl1 cl2 Hcl. apply (inj Some). by rewrite -!cloc_of_to_val Hcl. Qed.
Lemma cloc_to_val_for_compare cl :
val_for_compare (cloc_to_val cl) = cloc_to_val cl.
Proof. rewrite /cloc_to_val. unlock. done. Qed.
Lemma to_locking_heap_insert σ cl lv v : Lemma to_locking_heap_insert σ cl lv v :
to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ). to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
......
...@@ -396,7 +396,7 @@ Definition dbase_lit_eq (dl1 dl2 : dbase_lit) : dbool := ...@@ -396,7 +396,7 @@ Definition dbase_lit_eq (dl1 dl2 : dbase_lit) : dbool :=
| dLitInt _, (dLitUnit | dLitBool _) | dLitInt _, (dLitUnit | dLitBool _)
| dLitBool _, (dLitInt _ | dLitUnit) | dLitBool _, (dLitInt _ | dLitUnit)
| dLitUnit, (dLitInt _ | dLitBool _) => dBoolKnown false (* different known constructors *) | dLitUnit, (dLitInt _ | dLitBool _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2))) | _, _ => dBoolUnknown (bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2))
end. end.
Arguments dbase_lit_eq !_ !_ / : simpl nomatch. Arguments dbase_lit_eq !_ !_ / : simpl nomatch.
...@@ -410,12 +410,30 @@ Fixpoint dval_eq (E : known_locs) (dv1 dv2 : dval) : dbool := ...@@ -410,12 +410,30 @@ Fixpoint dval_eq (E : known_locs) (dv1 dv2 : dval) : dbool :=
| dNone, (dLitV _ | dPairV _ _ | dLocV _) | dNone, (dLitV _ | dPairV _ _ | dLocV _)
| dPairV _ _, (dNone | dLitV _ | dLocV _) | dPairV _ _, (dNone | dLitV _ | dLocV _)
| dLocV _, (dNone | dLitV _ | dPairV _ _) => dBoolKnown false (* different known constructors *) | dLocV _, (dNone | dLitV _ | dPairV _ _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2))) | _, _ => dBoolUnknown (bool_decide (dval_interp E dv1 = dval_interp E dv2))
end. end.
Arguments dval_eq _ !_ !_ / : simpl nomatch. Arguments dval_eq _ !_ !_ / : simpl nomatch.
Definition dbase_lit_unboxed (dl : dbase_lit) : bool :=
match dl with
| dLitUnknown l => bool_decide (lit_is_unboxed l)
| _ => true
end.
Definition dval_unboxed (dv : dval) : bool :=
match dv with
| dLitV dl => dbase_lit_unboxed dl
| dValUnknown v => bool_decide (val_is_unboxed v)
| _ => false
end.
Definition dbin_op_eval (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval := Definition dbin_op_eval (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
if decide (op = EqOp) then Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2 else if decide (op = EqOp) then
if dval_unboxed dv1 || dval_unboxed dv2 then
Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2
else
None
else
match dv1, dv2 with match dv1, dv2 with
| dLitV (dLitInt di1), dLitV (dLitInt di2) => dLitV <$> dbin_op_eval_int op di1 di2 | dLitV (dLitInt di1), dLitV (dLitInt di2) => dLitV <$> dbin_op_eval_int op di1 di2
| dLitV (dLitBool db1), dLitV (dLitBool db2) => dLitV <$> dbin_op_eval_bool op db1 db2 | dLitV (dLitBool db1), dLitV (dLitBool db2) => dLitV <$> dbin_op_eval_bool op db1 db2
...@@ -568,6 +586,32 @@ Proof. ...@@ -568,6 +586,32 @@ Proof.
rewrite H. apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)]. rewrite H. apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed. Qed.
Lemma dbase_lit_unboxed_correct dl :
dbase_lit_unboxed dl = true
lit_is_unboxed (dbase_lit_interp dl).
Proof.
destruct dl; intros; simplify_eq/=; [done..|].
eapply bool_decide_eq_true_1. done.
Qed.
Lemma dval_unboxed_correct E dv :
dval_unboxed dv = true
val_is_unboxed (dval_interp E dv).
Proof.
destruct dv; intros; simplify_eq/=.
- exact: dbase_lit_unboxed_correct.
- exact: bool_decide_eq_true_1.
Qed.
Lemma dvals_compare_safe_correct E dv1 dv2 :
dval_unboxed dv1 || dval_unboxed dv2 = true
vals_compare_safe (dval_interp E dv1) (dval_interp E dv2).
Proof.
destruct (dval_unboxed dv1) eqn:Hdv1.
- intros _. left. exact: dval_unboxed_correct.
- simpl. intros Hdv2. right. exact: dval_unboxed_correct.
Qed.
Lemma dbin_op_eval_int_correct op di1 di2 dl : Lemma dbin_op_eval_int_correct op di1 di2 dl :
dbin_op_eval_int op di1 di2 = Some dl dbin_op_eval_int op di1 di2 = Some dl
bin_op_eval_int op (dint_interp di1) (dint_interp di2) = Some (dbase_lit_interp dl). bin_op_eval_int op (dint_interp di1) (dint_interp di2) = Some (dbase_lit_interp dl).
...@@ -588,7 +632,7 @@ Qed. ...@@ -588,7 +632,7 @@ Qed.
Lemma dbase_lit_eq_correct dl1 dl2 : Lemma dbase_lit_eq_correct dl1 dl2 :
dbool_interp (dbase_lit_eq dl1 dl2) = dbool_interp (dbase_lit_eq dl1 dl2) =
bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2)). bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2).
Proof. Proof.
destruct dl1, dl2=> //=. destruct dl1, dl2=> //=.
- rewrite dint_eq_correct. apply bool_decide_iff. naive_solver congruence. - rewrite dint_eq_correct. apply bool_decide_iff. naive_solver congruence.
...@@ -597,13 +641,13 @@ Qed. ...@@ -597,13 +641,13 @@ Qed.
Lemma dval_eq_correct E dv1 dv2 : Lemma dval_eq_correct E dv1 dv2 :
dbool_interp (dval_eq E dv1 dv2) = dbool_interp (dval_eq E dv1 dv2) =
bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2)). bool_decide (dval_interp E dv1 = dval_interp E dv2).
Proof. Proof.
revert dv1. induction dv2; intros []=> //=; try by rewrite cloc_to_val_eq. revert dv1. induction dv2; intros []=> //=; try by rewrite cloc_to_val_eq.
- rewrite dbase_lit_eq_correct. apply bool_decide_iff. naive_solver congruence. - rewrite dbase_lit_eq_correct. apply bool_decide_iff. naive_solver congruence.
- rewrite dbool_and_correct. rewrite IHdv2_1 IHdv2_2. - rewrite dbool_and_correct. rewrite IHdv2_1 IHdv2_2.
repeat case_bool_decide; intuition congruence. repeat case_bool_decide; intuition congruence.
- rewrite dloc_eq_correct !cloc_to_val_for_compare. - rewrite dloc_eq_correct.
apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)]. apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed. Qed.
...@@ -611,8 +655,10 @@ Lemma dbin_op_eval_correct E op dv1 dv2 dw : ...@@ -611,8 +655,10 @@ Lemma dbin_op_eval_correct E op dv1 dv2 dw :
dbin_op_eval E op dv1 dv2 = Some dw dbin_op_eval E op dv1 dv2 = Some dw
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E dw). bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E dw).
Proof. Proof.
rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)); simplify_eq/=. rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)). simplify_eq/=.
{ by rewrite dval_eq_correct. } { destruct (dval_unboxed dv1 || dval_unboxed dv2) eqn:Hdv; last done.
rewrite decide_True; last exact: dvals_compare_safe_correct.
simplify_eq/=. by rewrite dval_eq_correct. }
destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq. destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq.
- by erewrite dbin_op_eval_int_correct by done. - by erewrite dbin_op_eval_int_correct by done.
- by erewrite dbin_op_eval_bool_correct by done. - by erewrite dbin_op_eval_bool_correct by done.
...@@ -677,7 +723,9 @@ Lemma dbin_op_eval_Some_wf E dv1 dv2 op dw: ...@@ -677,7 +723,9 @@ Lemma dbin_op_eval_Some_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2 dval_wf E dw. dval_wf E dv1 dval_wf E dv2 dval_wf E dw.
Proof. Proof.
rewrite /dbin_op_eval; intros; simplify_option_eq; auto. rewrite /dbin_op_eval; intros; simplify_option_eq; auto.
destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq; auto. - destruct (dval_unboxed dv1 || dval_unboxed dv2) eqn:Hdv; last done.
simplify_eq/=. done.
- destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq; auto.
Qed. Qed.
Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw: Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment