Commit 515d13eb authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Bump

parent 47438a79
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-iris" { (= "dev.2021-03-03.2.f38829da") | (= "dev") }
"coq-iris" { (= "dev.2021-03-06.3.b0708b01") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -15,8 +15,10 @@ Class heapG Σ := HeapG {
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ κs _ := gen_heap_interp σ;
fork_post _ := True%I
state_interp σ _ κs _ := gen_heap_interp σ;
num_laters_per_step _ := 0%nat;
fork_post _ := True%I;
state_interp_mono _ _ _ _ := fupd_intro _ _
}.
(** Override the notations so that scopes and coercions work out *)
......@@ -155,7 +157,7 @@ Lemma wp_fork s E e Φ :
WP e @ s; {{ _, True }} - Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
Proof.
iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
iIntros (σ1 ? κ κs n) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
......@@ -164,7 +166,7 @@ Lemma wp_alloc s E v :
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by auto.
iIntros (σ1 ? κ κs n) "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Φ".
......@@ -174,7 +176,7 @@ Lemma wp_load s E l dq v :
{{{ l {dq} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {dq} v }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 ? κ κs n) "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Φ".
Qed.
......@@ -185,7 +187,7 @@ Lemma wp_store s E l v' v :
Proof.
iIntros (Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 ? κ κs n) "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=>//. iFrame. by iApply "HΦ".
......@@ -197,7 +199,7 @@ Lemma wp_cas_fail s E l q v' v1 v2 :
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 ? κ κs n) "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Φ".
Qed.
......@@ -208,7 +210,7 @@ Lemma wp_cas_suc s E l v1 v2 :
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 ? κ κs n) "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=>//. iFrame. by iApply "HΦ".
......@@ -219,7 +221,7 @@ Lemma wp_faa s E l i1 i2 :
{{{ RET LitV (LitInt i1); l LitV (LitInt (i1 + i2)) }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 ? κ κs n) "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=>//. iFrame. by iApply "HΦ".
......
Supports Markdown
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