Commit ed4ac088 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' of gitlab.inria.fr:gmevel/iris-time-proofs into master

parents 831f06c7 e53b2901
......@@ -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-10-14.0.dc793c10") | (= "dev") }
"coq-iris" { (= "dev.2020-10-21.1.4b3d541a") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -833,13 +833,13 @@ Section Soundness.
(* … now we have to prove a WP. *)
set σ' := S«σ».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth (<[ := #M]> σ') gmap_view_frag (DfracOwn 1) #M))
iMod (own_alloc (gmap_view_auth 1 (<[ := #M]> σ') gmap_view_frag (DfracOwn 1) #M))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* allocate the ghost state associated with ℓ: *)
iAssert (|==> γ,
......
......@@ -422,13 +422,13 @@ Section Soundness.
(* … now we have to prove a WP. *)
set σ' := S«σ».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth (<[ := #k]> σ') gmap_view_frag (DfracOwn 1) #k))
iMod (own_alloc (gmap_view_auth 1 (<[ := #k]> σ') gmap_view_frag (DfracOwn 1) #k))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc k) as (γ) "[Hγ● Hγ◯]".
......
......@@ -246,13 +246,13 @@ Proof.
* we settle the needed invariant TC_invariant. *)
set σ' := S«σ1».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth (<[ := #m]> σ') gmap_view_frag (DfracOwn 1) #m))
iMod (own_alloc (gmap_view_auth 1 (<[ := #m]> σ') gmap_view_frag (DfracOwn 1) #m))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc m) as (γ) "[Hγ● Hγ◯]".
......
......@@ -319,13 +319,13 @@ Section Soundness.
(* … now we have to prove a WP. *)
set σ' := S«σ».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth (<[ := #(nmax-1)%nat]> σ') gmap_view_frag (DfracOwn 1) #(nmax-1)%nat))
iMod (own_alloc (gmap_view_auth 1 (<[ := #(nmax-1)%nat]> σ') gmap_view_frag (DfracOwn 1) #(nmax-1)%nat))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
......
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