Commit d2e5a8c0 authored by Ralf Jung's avatar Ralf Jung

bump Iris; fix for persistent points-to

parent 25decc5a
......@@ -19,3 +19,5 @@ _opam
.coq-native/
build-dep/
*.crashcoqide
.Makefile.coq.d
.nia.cache
......@@ -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.2020-11-27.0.f0f9f3b6") | (= "dev") }
"coq-iris" { (= "dev.2020-12-18.3.e7bfdf12") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -20,13 +20,12 @@ Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
}.
(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=val) l dq v%V)
(at level 20, dq at level 50, format "l ↦{ dq } v") : bi_scope.
Notation "l ↦{# q } v" := (mapsto (L:=loc) (V:=val) l (DfracOwn q) v%V)
(at level 20, q at level 50, format "l ↦{# q } v") : bi_scope.
Notation "l ↦ v" :=
(mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
Notation "l ↦{ q } -" := ( v, l {q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
(mapsto (L:=loc) (V:=val) l (DfracOwn 1) v%V) (at level 20) : bi_scope.
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
......@@ -171,8 +170,8 @@ Proof.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_load s E l q v :
{{{ l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
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 %?.
......
......@@ -128,7 +128,7 @@ Notation Phi := (Phi 1).
client. *)
Definition mapsto_M M : iProp Σ :=
([ map] l c M, from_option (mapsto l 1) False (val_of_content c))%I.
([ map] l c M, from_option (mapsto l (DfracOwn 1)) False (val_of_content c))%I.
Definition UF D R V : iProp Σ :=
( F K M,
......
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