Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit e53b2901 authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for gmap_view_auth change

parent fc53d921
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.9.1" & < "8.11~") | (= "dev") }
"coq-iris" { (= "dev.2020-10-14.0.dc793c10") | (= "dev") }
"coq-iris" { (= "dev.2020-10-21.1.4b3d541a") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "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