From a9884f6a12cc656529bc32075cb5426ff725c6c8 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Tue, 7 Mar 2023 11:57:46 +0100
Subject: [PATCH] fixes for iris/iris!886 and iris/iris!896
---
coq-gpfsl.opam | 2 +-
coq-orc11.opam | 2 +-
gpfsl-examples/lock/proof_ticket_lock_gps.v | 10 +++++-----
gpfsl-examples/queue/proof_ms_gps.v | 4 ++--
gpfsl/gps/surface_iPP.v | 2 +-
gpfsl/gps/surface_iSP.v | 8 ++++----
gpfsl/gps/surface_vSP.v | 8 ++++----
7 files changed, 18 insertions(+), 18 deletions(-)
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 74302c16..ecbbd060 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [
- "coq-iris" { (= "dev.2022-11-30.1.e52255ba") | (= "dev") }
+ "coq-iris" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
"coq-orc11" {= version}
]
diff --git a/coq-orc11.opam b/coq-orc11.opam
index 4073fa0a..282de8d1 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
depends: [
- "coq-stdpp" { (= "dev.2022-11-30.0.ffa862a8") | (= "dev") }
+ "coq-stdpp" { (= "dev.2023-02-04.0.7125e166") | (= "dev") }
]
build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl-examples/lock/proof_ticket_lock_gps.v b/gpfsl-examples/lock/proof_ticket_lock_gps.v
index a7e76fca..44bd1a55 100644
--- a/gpfsl-examples/lock/proof_ticket_lock_gps.v
+++ b/gpfsl-examples/lock/proof_ticket_lock_gps.v
@@ -46,7 +46,7 @@ Definition Waiting M n : gset nat :=
filter (λ i, ∃ t, M !! i = Excl2 t ∧ n ≤ t) (dom M).
Definition Ws M n : nat := size (Waiting M n).
-Definition ns_tkt_bound M t n : Prop :=
+Definition ns_tkt_bound M t n : Prop :=
n ≤ t ∧ t ≤ n + Ws M n
∧ ∀ (i k: nat), M !! i = Excl2 k →
(k < t) ∧ ∀ (j: nat), M !! j = Excl2 k → i = j.
@@ -254,7 +254,7 @@ Proof.
split; [|split; first lia; split].
* eapply Z.le_lt_trans; first by apply LE2.
apply Z.add_lt_le_mono; [lia|]. by apply Waiting_size_le.
- * rewrite Nat2Z.inj_succ Nat2Z.inj_add Zplus_assoc_reverse
+ * rewrite Nat2Z.inj_succ Nat2Z.inj_add Zplus_assoc_reverse
(Z.add_comm 1) Zplus_assoc.
apply Zplus_le_compat_r. etrans; first apply LE2.
assert (Eqs :=
@@ -283,7 +283,7 @@ Proof.
{ rewrite disjoint_singleton_l /Waiting elem_of_filter.
rewrite Ini. move => [[? [[<-] ?]] _]. lia. }
rewrite Nat2Z.inj_add size_singleton Nat2Z.inj_add
- (Z.add_comm 1) Zplus_assoc.
+ (Z.add_comm 1) Zplus_assoc.
by apply Zplus_le_compat_r. }
* by apply ns_inj_insert.
- exists n. split; [done|split]; first by right.
@@ -300,7 +300,7 @@ Proof.
{ rewrite disjoint_singleton_l /Waiting elem_of_filter.
rewrite Ini. move => [[? [//]]]. }
rewrite Nat2Z.inj_add size_singleton Nat2Z.inj_add
- (Z.add_comm 1) Zplus_assoc.
+ (Z.add_comm 1) Zplus_assoc.
by apply Zplus_le_compat_r. }
* by apply ns_inj_insert.
Qed.
@@ -370,7 +370,7 @@ Proof.
apply bi.sep_ne; [done|].
repeat (apply bi.exist_ne => ?).
apply GPS_iSP_Writer_contractive; [done|].
- destruct n; [done|by simpl].
+ dist_later_fin_intro. eapply H; si_solver.
Qed.
Definition NSP P γ : interpO Σ natProtocol := fixpoint (NSP' P γ).
diff --git a/gpfsl-examples/queue/proof_ms_gps.v b/gpfsl-examples/queue/proof_ms_gps.v
index cc332bd1..f885eb5a 100644
--- a/gpfsl-examples/queue/proof_ms_gps.v
+++ b/gpfsl-examples/queue/proof_ms_gps.v
@@ -82,8 +82,8 @@ Proof.
do 2 apply bi.exist_ne => ?.
apply bi.sep_ne; [done|].
do 2 (apply bi.exist_ne => ?).
- apply GPS_iPP_contractive. destruct n => //.
- by apply H.
+ apply GPS_iPP_contractive.
+ dist_later_fin_intro. eapply H; si_solver.
Qed.
Definition Link : ∀ γ, interpO Σ LinkProtocol := fixpoint Link'.
diff --git a/gpfsl/gps/surface_iPP.v b/gpfsl/gps/surface_iPP.v
index e25f9156..c225d538 100644
--- a/gpfsl/gps/surface_iPP.v
+++ b/gpfsl/gps/surface_iPP.v
@@ -274,7 +274,7 @@ Global Instance GPS_iPP_contractive l t s v γ :
Contractive (λ IP, GPS_iPP IP l t s v γ).
Proof.
move => n ???. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
- destruct n; [done|]. by apply GPS_PPInv_ne.
+ dist_later_fin_intro. apply GPS_PPInv_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_iPP_ne l t s v γ :
NonExpansive (λ IP, GPS_iPP IP l t s v γ).
diff --git a/gpfsl/gps/surface_iSP.v b/gpfsl/gps/surface_iSP.v
index c3602849..016b2089 100644
--- a/gpfsl/gps/surface_iSP.v
+++ b/gpfsl/gps/surface_iSP.v
@@ -328,7 +328,7 @@ Global Instance GPS_iSP_Writer_contractive n l t s v γ :
(λ IP IPC, GPS_iSP_Writer IP IPC l t s v γ).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_iSP_Writer_ne l t s v γ :
NonExpansive2 (λ IP IPC, GPS_iSP_Writer IP IPC l t s v γ).
@@ -348,7 +348,7 @@ Global Instance GPS_iSP_Reader_contractive n l t s v γ :
(λ IP IPC, GPS_iSP_Reader IP IPC l t s v γ).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_iSP_Reader_ne l t s v γ :
NonExpansive2 (λ IP IPC, GPS_iSP_Reader IP IPC l t s v γ).
@@ -368,7 +368,7 @@ Global Instance GPS_iSP_SharedReader_contractive n l t s v q γ :
(λ IP IPC, GPS_iSP_SharedReader IP IPC l t s v q γ).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_iSP_SharedReader_ne l t s v q γ :
NonExpansive2 (λ IP IPC, GPS_iSP_SharedReader IP IPC l t s v q γ).
@@ -388,7 +388,7 @@ Global Instance GPS_iSP_SharedWriter_contractive n l t s v γ :
(λ IP IPC, GPS_iSP_SharedWriter IP IPC l t s v γ).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_iSP_SharedWriter_ne l t s v γ :
NonExpansive2 (λ IP IPC, GPS_iSP_SharedWriter IP IPC l t s v γ).
diff --git a/gpfsl/gps/surface_vSP.v b/gpfsl/gps/surface_vSP.v
index 220176fc..6f41cc45 100644
--- a/gpfsl/gps/surface_vSP.v
+++ b/gpfsl/gps/surface_vSP.v
@@ -148,7 +148,7 @@ Global Instance GPS_vSP_Writer_contractive n l t s v γ γi :
(λ IP IPC, GPS_vSP_Writer IP IPC l t s v γ γi).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_vSP_Writer_ne IPC l t s v γ γi :
NonExpansive2 (λ IP IPC, GPS_vSP_Writer IP IPC l t s v γ γi).
@@ -168,7 +168,7 @@ Global Instance GPS_vSP_Reader_contractive n l t s v γ γi :
(λ IP IPC, GPS_vSP_Reader IP IPC l t s v γ γi).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_vSP_Reader_ne l t s v γ γi :
NonExpansive2 (λ IP IPC, GPS_vSP_Reader IP IPC l t s v γ γi).
@@ -188,7 +188,7 @@ Global Instance GPS_vSP_SharedReader_contractive n l t s v q γ γi :
(λ IP IPC, GPS_vSP_SharedReader IP IPC l t s v q γ γi).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_vSP_SharedReader_ne l t s v q γ γi :
NonExpansive2 (λ IP IPC, GPS_vSP_SharedReader IP IPC l t s v q γ γi).
@@ -208,7 +208,7 @@ Global Instance GPS_vSP_SharedWriter_contractive n l t s v γ γi :
(λ IP IPC, GPS_vSP_SharedWriter IP IPC l t s v γ γi).
Proof.
move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
- destruct n; [done|]. by apply GPS_INV_ne.
+ dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
Qed.
Global Instance GPS_vSP_SharedWriter_ne l t s v γ γi :
NonExpansive2 (λ IP IPC, GPS_vSP_SharedWriter IP IPC l t s v γ γi).
--
GitLab