Commit 439b7943 authored by Ralf Jung's avatar Ralf Jung

bump Iris for comparison changes

parent 2ae8b292
Pipeline #17889 passed with stage
in 15 minutes and 10 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
"coq-iris" { (= "dev.2019-06-18.8.72595700") | (= "dev") }
]
......@@ -297,7 +297,8 @@ Section proofs.
{ wp_lam; wp_pures. by iApply "HΨ". }
wp_lam; wp_pures. wp_apply wp_assert.
rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks"; case_bool_decide.
wp_apply (mset_member_spec with "Hlocks"); first done.
iIntros "Hlocks"; case_bool_decide.
{ destruct (HX (#(cloc_base cl), #n)%V) as (cl'&[= <-]&?); first done.
destruct (Hlocked n); first by (apply lookup_lt_is_Some_2; lia).
destruct cl; simplify_eq/=. by rewrite /cloc_plus /= Z.add_0_r. }
......@@ -336,7 +337,7 @@ Section proofs.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
iMod (full_locking_heap_store_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply (mset_add_spec with "[$]"); first done.
wp_apply (mset_add_spec with "[$]"); [done..|].
iIntros "Hlocks /="; wp_pures.
wp_load; wp_pures.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
......@@ -367,7 +368,8 @@ Section proofs.
{ intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
iMod (full_locking_heap_load_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); [done..|].
iIntros "Hlocks /=".
rewrite bool_decide_false //.
wp_op. iSplit; first done. iNext; wp_seq.
wp_load; wp_match.
......
......@@ -107,15 +107,18 @@ Proof.
Qed.
Lemma llist_member_spec hd vs v :
{{{ is_list hd vs }}} llist_member v hd {{{ RET #(bool_decide (v vs)); True }}}.
{{{ is_list hd vs }}}
llist_member v hd
{{{ RET #(bool_decide (val_for_compare v (val_for_compare <$> vs))); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
{ wp_lam; wp_pures. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam; wp_pures.
destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
destruct (bool_decide_reflect (val_for_compare v' = val_for_compare v)) as [->|?]; wp_if.
{ rewrite (bool_decide_true (_ _ :: _)); last by left. by iApply "HΦ". }
wp_proj. wp_let. iApply ("IH" with "[//]"). destruct (bool_decide_reflect (v vs)).
wp_proj. wp_let. iApply ("IH" with "[//]").
destruct (bool_decide_reflect (val_for_compare v (val_for_compare <$> vs))).
- by rewrite bool_decide_true; last by right.
- by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
Qed.
......
......@@ -323,6 +323,9 @@ Section properties.
Qed.
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.
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 :
to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
......
......@@ -4,7 +4,7 @@ From iris_c.lib Require Import list.
Definition is_mset `{heapG Σ} (v : val) (X : gset val) : iProp Σ :=
( (l : loc) hd vs,
v = #l X = list_to_set vs is_list hd vs NoDup vs l hd)%I.
v = #l X = list_to_set (val_for_compare <$> vs) is_list hd vs NoDup vs l hd)%I.
Definition mset_create : val := λ: <>, ref (lnil #()).
......@@ -20,6 +20,14 @@ Definition mset_add : val := λ: "x" "xs",
Definition mset_clear : val := λ: "xs",
"xs" <- lnil #().
Lemma val_for_compare_in_set v vs :
val_for_compare v list_to_set (C:=gset val) (val_for_compare <$> vs)
v vs.
Proof.
intros Hnin Hin. apply Hnin. rewrite elem_of_list_to_set.
eapply elem_of_list_fmap. eauto.
Qed.
Section mset.
Context `{heapG Σ}.
Implicit Types x v : val.
......@@ -34,31 +42,35 @@ Section mset.
Lemma mset_member_spec x e v X :
IntoVal e v
val_for_compare v = v
{{{ is_mset x X }}}
mset_member e x
{{{ RET #(bool_decide (v X)); is_mset x X }}}.
Proof.
iIntros (<- Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
iIntros (<- Hvc Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
wp_lam; wp_pures. wp_load. wp_let.
wp_apply (llist_member_spec with "[//]"). iIntros "_".
rewrite (bool_decide_iff _ (v vs)); last set_solver.
iApply "HΦ". iExists l, hd, vs; auto.
rewrite (bool_decide_iff _ (v val_for_compare <$> vs)); last set_solver.
rewrite Hvc. iApply "HΦ". iExists l, hd, vs; auto.
Qed.
Lemma mset_add_spec x e v X :
IntoVal e v
val_for_compare v = v
v X
{{{ is_mset x X }}}
mset_add e x
{{{ RET #(); is_mset x ({[v]} X) }}}.
Proof.
iIntros (<- Φ ?) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
iIntros (<- Hvc ? Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
wp_lam. wp_pures. wp_load. wp_let. wp_apply wp_assert.
wp_apply (llist_member_spec with "[//]"); iIntros "_".
rewrite bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
rewrite Hvc bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
iApply "HΦ". iExists l, hd', (v :: vs). iFrame "Hl".
rewrite NoDup_cons. iPureIntro; set_solver.
rewrite NoDup_cons fmap_cons Hvc. assert (v vs).
{ eapply val_for_compare_in_set. rewrite Hvc. done. }
iPureIntro; set_solver.
Qed.
Lemma mset_clear_spec x X :
......
......@@ -396,7 +396,7 @@ Definition dbase_lit_eq (dl1 dl2 : dbase_lit) : dbool :=
| dLitInt _, (dLitUnit | dLitBool _)
| dLitBool _, (dLitInt _ | dLitUnit)
| dLitUnit, (dLitInt _ | dLitBool _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2))
| _, _ => dBoolUnknown (bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2)))
end.
Arguments dbase_lit_eq !_ !_ / : simpl nomatch.
......@@ -410,7 +410,7 @@ Fixpoint dval_eq (E : known_locs) (dv1 dv2 : dval) : dbool :=
| dNone, (dLitV _ | dPairV _ _ | dLocV _)
| dPairV _ _, (dNone | dLitV _ | dLocV _)
| dLocV _, (dNone | dLitV _ | dPairV _ _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (dval_interp E dv1 = dval_interp E dv2))
| _, _ => dBoolUnknown (bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2)))
end.
Arguments dval_eq _ !_ !_ / : simpl nomatch.
......@@ -588,7 +588,7 @@ Qed.
Lemma dbase_lit_eq_correct dl1 dl2 :
dbool_interp (dbase_lit_eq dl1 dl2) =
bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2).
bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2)).
Proof.
destruct dl1, dl2=> //=.
- rewrite dint_eq_correct. apply bool_decide_iff. naive_solver congruence.
......@@ -597,13 +597,13 @@ Qed.
Lemma dval_eq_correct E dv1 dv2 :
dbool_interp (dval_eq E dv1 dv2) =
bool_decide (dval_interp E dv1 = dval_interp E dv2).
bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2)).
Proof.
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 dbool_and_correct. rewrite IHdv2_1 IHdv2_2.
repeat case_bool_decide; intuition congruence.
- rewrite dloc_eq_correct.
- rewrite dloc_eq_correct !cloc_to_val_for_compare.
apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.
......
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