From b5b10a187e467ee3ff923cbbbf25a6f007b188ad Mon Sep 17 00:00:00 2001
From: Ike Mulder <me@ikemulder.nl>
Date: Fri, 28 Feb 2025 19:43:12 +0000
Subject: [PATCH 1/9] Update Iris to version dev.2025-02-27.1.c773500a
---
coq-diaframe.opam | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/coq-diaframe.opam b/coq-diaframe.opam
index 545edaf6..ea73887e 100644
--- a/coq-diaframe.opam
+++ b/coq-diaframe.opam
@@ -7,7 +7,7 @@ authors: "Ike Mulder <me@ikemulder.nl>"
homepage: "https://gitlab.mpi-sws.org/iris/diaframe/"
bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
- "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2025-01-31.0.1bb4eba3" ) | = "dev" | = "4.1.0" }
+ "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2025-02-27.1.c773500a" ) | = "dev" | = "4.1.0" }
"coq" { >= "8.19" & < "8.21~" }
]
build: [make "-j%{jobs}%" "diaframe"]
--
GitLab
From 6aa8667fa8ce3fb484cf3fb0a496c896098626d3 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sun, 2 Mar 2025 12:47:44 +0100
Subject: [PATCH 2/9] Update iris and supplements
---
supplements/coq-diaframe-actris.opam | 2 +-
supplements/coq-diaframe-iris-examples.opam | 2 +-
supplements/coq-diaframe-reloc.opam | 2 +-
supplements/coq-diaframe-simuliris.opam | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/supplements/coq-diaframe-actris.opam b/supplements/coq-diaframe-actris.opam
index e496587e..e6a609e1 100644
--- a/supplements/coq-diaframe-actris.opam
+++ b/supplements/coq-diaframe-actris.opam
@@ -10,7 +10,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
"coq-diaframe-heap-lang" {= version}
"coq" { = "8.20.0" }
- "coq-actris" { = "dev.2025-01-24.0.f9d06c7b" | = "~dev" }
+ "coq-actris" { = "dev.2025-02-27.0.316a5108" | = "~dev" }
]
build: [make "-j%{jobs}%" "diaframe-actris"]
install: [make "install-diaframe-actris"]
diff --git a/supplements/coq-diaframe-iris-examples.opam b/supplements/coq-diaframe-iris-examples.opam
index 7a49ba08..7a6815c0 100644
--- a/supplements/coq-diaframe-iris-examples.opam
+++ b/supplements/coq-diaframe-iris-examples.opam
@@ -10,7 +10,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
"coq" { = "8.20.0" }
"coq-diaframe-heap-lang" {= version}
- "coq-iris-examples" { = "dev.2025-01-25.0.e5afd885" | = "~dev" }
+ "coq-iris-examples" { = "dev.2025-02-05.0.9806de16" | = "~dev" }
]
build: [make "-j%{jobs}%" "diaframe-iris-examples"]
install: [make "install-diaframe-iris-examples"]
diff --git a/supplements/coq-diaframe-reloc.opam b/supplements/coq-diaframe-reloc.opam
index a694d941..c81710ac 100644
--- a/supplements/coq-diaframe-reloc.opam
+++ b/supplements/coq-diaframe-reloc.opam
@@ -14,7 +14,7 @@ depends: [
"coq-reloc"
]
pin-depends: [
- ["coq-reloc.dev" "git+https://gitlab.mpi-sws.org/iris/reloc#828ae710"]
+ ["coq-reloc.dev" "git+https://gitlab.mpi-sws.org/iris/reloc#13701476"]
]
build: [make "-j%{jobs}%" "diaframe-reloc"]
install: [make "install-diaframe-reloc"]
diff --git a/supplements/coq-diaframe-simuliris.opam b/supplements/coq-diaframe-simuliris.opam
index 3a5a2baf..8000d0d3 100644
--- a/supplements/coq-diaframe-simuliris.opam
+++ b/supplements/coq-diaframe-simuliris.opam
@@ -13,7 +13,7 @@ depends: [
"coq-simuliris"
]
pin-depends: [
- ["coq-simuliris.dev" "git+https://gitlab.mpi-sws.org/iris/simuliris#b7030e3a"]
+ ["coq-simuliris.dev" "git+https://gitlab.mpi-sws.org/iris/simuliris#4099b244"]
]
build: [make "-j%{jobs}%" "diaframe-simuliris"]
install: [make "install-diaframe-simuliris"]
--
GitLab
From a7c4d317bb9516fd94fee195cbd959551b3670f5 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sun, 2 Mar 2025 13:48:56 +0100
Subject: [PATCH 3/9] Bot -> Invalid rename, fixpoint move
---
diaframe/lib/greatest_fixpoint.v | 2 +-
diaframe/lib/own_hints.v | 8 ++++----
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/diaframe/lib/greatest_fixpoint.v b/diaframe/lib/greatest_fixpoint.v
index 47603039..20a5318b 100644
--- a/diaframe/lib/greatest_fixpoint.v
+++ b/diaframe/lib/greatest_fixpoint.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi telescopes lib.fixpoint.
+From iris.bi Require Export bi telescopes lib.fixpoint_mono.
From iris.proofmode Require Import proofmode environments classes_make.
From diaframe Require Import proofmode_base.
diff --git a/diaframe/lib/own_hints.v b/diaframe/lib/own_hints.v
index eab37a4a..6db9f939 100644
--- a/diaframe/lib/own_hints.v
+++ b/diaframe/lib/own_hints.v
@@ -335,7 +335,7 @@ From stdpp Require Import telescopes.
Section other.
Global Instance excl_inhabited {A : ofe} : Inhabited (exclR A).
- Proof. split. by apply ExclBot. Qed.
+ Proof. split. by apply ExclInvalid. Qed.
Global Arguments option_unit_instance /.
@@ -998,14 +998,14 @@ Section validity.
by iRewrite "Ha".
Qed.
Global Instance sum_inl_inr_invalid_op {A B : cmra} (a : A) (b : B) Σ :
- IsValidOp (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
+ IsValidOp (CsumInvalid) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
Proof.
split; rewrite /op /= /cmra_op //=; eauto.
rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
rewrite /validN /= /cmra_validN //=.
Qed.
Global Instance sum_inr_inl_invalid_op {A B : cmra} (a : A) (b : B) Σ :
- IsValidOp (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
+ IsValidOp (CsumInvalid) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
Proof.
split; rewrite /op /= /cmra_op //=; eauto.
rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
@@ -1482,7 +1482,7 @@ Section validity.
Qed.
Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ:
- IsValidOp ExclBot a1 a2 Σ False%I.
+ IsValidOp ExclInvalid a1 a2 Σ False%I.
Proof. split; rewrite excl_validI /=; eauto. Qed. *)
Lemma excl_subtract {O : ofe} (o1 o2 : O) : (* this one is bad for recursive instances *)
TCIf (SolveSepSideCondition (¬ (o1 ≡ o2))) False TCTrue →
--
GitLab
From 95fd712afc099c6ce382f93bcce09cba9e284ba4 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sun, 2 Mar 2025 13:58:12 +0100
Subject: [PATCH 4/9] Fixed lib.fixpoint in do_lob
---
diaframe/lib/do_lob.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/diaframe/lib/do_lob.v b/diaframe/lib/do_lob.v
index 764ae6a1..cea460dd 100644
--- a/diaframe/lib/do_lob.v
+++ b/diaframe/lib/do_lob.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi telescopes lib.laterable lib.fixpoint.
+From iris.bi Require Export bi telescopes lib.laterable lib.fixpoint_mono.
From iris.proofmode Require Import proofmode environments.
From diaframe Require Import proofmode_base utils_ltac2.
--
GitLab
From 74f173153680013a35d7d229333c82fe164ccd7c Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sun, 2 Mar 2025 14:08:15 +0100
Subject: [PATCH 5/9] Another bot -> invalid rename
---
diaframe/lib/own/proofmode_instances.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/diaframe/lib/own/proofmode_instances.v b/diaframe/lib/own/proofmode_instances.v
index 6622ed9e..e4bd391e 100644
--- a/diaframe/lib/own/proofmode_instances.v
+++ b/diaframe/lib/own/proofmode_instances.v
@@ -383,7 +383,7 @@ Section recursive.
by iRewrite "Ha".
Qed.
Global Instance sum_inl_inr_invalid_op {A B : cmra} (a : A) (b : B) Σ :
- IsValidOp (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
+ IsValidOp (CsumInvalid) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
Proof.
split; rewrite /op /= /cmra_op //=; eauto. (* TODO: need proper access to unsealing lemma's *)
uPred_primitive.unseal.
@@ -391,7 +391,7 @@ Section recursive.
rewrite /validN /= /cmra_validN //=.
Qed.
Global Instance sum_inr_inl_invalid_op {A B : cmra} (a : A) (b : B) Σ :
- IsValidOp (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
+ IsValidOp (CsumInvalid) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
Proof.
split; rewrite /op /= /cmra_op //=; eauto.
uPred_primitive.unseal.
@@ -660,7 +660,7 @@ Section recursive.
Qed.
Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ:
- IsValidOp ExclBot a1 a2 Σ False%I.
+ IsValidOp ExclInvalid a1 a2 Σ False%I.
Proof. split; rewrite excl_validI /=; eauto. Qed.
Global Instance excl_included_merge {O : ofe} (o1 o2 : excl O) {Σ} :
IsIncludedMerge o1 o2 (Σ := Σ) False%I.
@@ -1029,4 +1029,4 @@ Section recursive.
iSplit => //.
Qed.
-End recursive.
\ No newline at end of file
+End recursive.
--
GitLab
From 34609e415f1248b40fff9ea6b46f5b4358a36c35 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sat, 5 Apr 2025 17:56:37 +0100
Subject: [PATCH 6/9] Naive changes for transfinite iris update
---
coq-diaframe.opam | 2 +-
supplements/coq-diaframe-actris.opam | 2 +-
supplements/coq-diaframe-iris-examples.opam | 2 +-
supplements/coq-diaframe-lambda-rust.opam | 4 ++--
supplements/coq-diaframe-reloc.opam | 2 +-
supplements/coq-diaframe-simuliris.opam | 2 +-
supplements/diaframe_reloc/atomic_post_update.v | 15 ++++++++-------
7 files changed, 15 insertions(+), 14 deletions(-)
diff --git a/coq-diaframe.opam b/coq-diaframe.opam
index ea73887e..1a7a7da2 100644
--- a/coq-diaframe.opam
+++ b/coq-diaframe.opam
@@ -7,7 +7,7 @@ authors: "Ike Mulder <me@ikemulder.nl>"
homepage: "https://gitlab.mpi-sws.org/iris/diaframe/"
bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
- "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2025-02-27.1.c773500a" ) | = "dev" | = "4.1.0" }
+ "coq-iris" { (>= "dev.2025-03-28.0.fa344cbe" & <= "dev.2025-03-31.0.017605dd" ) | = "dev" }
"coq" { >= "8.19" & < "8.21~" }
]
build: [make "-j%{jobs}%" "diaframe"]
diff --git a/supplements/coq-diaframe-actris.opam b/supplements/coq-diaframe-actris.opam
index e6a609e1..4865fca6 100644
--- a/supplements/coq-diaframe-actris.opam
+++ b/supplements/coq-diaframe-actris.opam
@@ -10,7 +10,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
"coq-diaframe-heap-lang" {= version}
"coq" { = "8.20.0" }
- "coq-actris" { = "dev.2025-02-27.0.316a5108" | = "~dev" }
+ "coq-actris" { = "dev.2025-03-28.0.c9249305" | = "~dev" }
]
build: [make "-j%{jobs}%" "diaframe-actris"]
install: [make "install-diaframe-actris"]
diff --git a/supplements/coq-diaframe-iris-examples.opam b/supplements/coq-diaframe-iris-examples.opam
index 7a6815c0..b7ecde10 100644
--- a/supplements/coq-diaframe-iris-examples.opam
+++ b/supplements/coq-diaframe-iris-examples.opam
@@ -10,7 +10,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
"coq" { = "8.20.0" }
"coq-diaframe-heap-lang" {= version}
- "coq-iris-examples" { = "dev.2025-02-05.0.9806de16" | = "~dev" }
+ "coq-iris-examples" { = "dev.2025-03-28.1.593cca1f" | = "~dev" }
]
build: [make "-j%{jobs}%" "diaframe-iris-examples"]
install: [make "install-diaframe-iris-examples"]
diff --git a/supplements/coq-diaframe-lambda-rust.opam b/supplements/coq-diaframe-lambda-rust.opam
index f050f141..2bcecc1a 100644
--- a/supplements/coq-diaframe-lambda-rust.opam
+++ b/supplements/coq-diaframe-lambda-rust.opam
@@ -13,8 +13,8 @@ depends: [
"coq-lambda-rust"
]
pin-depends: [
- ["coq-lambda-rust.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#f55b9243"]
- ["coq-lifetime-logic.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#f55b9243"]
+ ["coq-lambda-rust.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#fca004c4"]
+ ["coq-lifetime-logic.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#fca004c4"]
]
build: [make "-j%{jobs}%" "diaframe-lambda-rust"]
diff --git a/supplements/coq-diaframe-reloc.opam b/supplements/coq-diaframe-reloc.opam
index c81710ac..fc060200 100644
--- a/supplements/coq-diaframe-reloc.opam
+++ b/supplements/coq-diaframe-reloc.opam
@@ -14,7 +14,7 @@ depends: [
"coq-reloc"
]
pin-depends: [
- ["coq-reloc.dev" "git+https://gitlab.mpi-sws.org/iris/reloc#13701476"]
+ ["coq-reloc.dev" "git+https://gitlab.mpi-sws.org/iris/reloc#37a694fd"]
]
build: [make "-j%{jobs}%" "diaframe-reloc"]
install: [make "install-diaframe-reloc"]
diff --git a/supplements/coq-diaframe-simuliris.opam b/supplements/coq-diaframe-simuliris.opam
index 8000d0d3..348eef9a 100644
--- a/supplements/coq-diaframe-simuliris.opam
+++ b/supplements/coq-diaframe-simuliris.opam
@@ -13,7 +13,7 @@ depends: [
"coq-simuliris"
]
pin-depends: [
- ["coq-simuliris.dev" "git+https://gitlab.mpi-sws.org/iris/simuliris#4099b244"]
+ ["coq-simuliris.dev" "git+https://gitlab.mpi-sws.org/iris/simuliris#771b052a"]
]
build: [make "-j%{jobs}%" "diaframe-simuliris"]
install: [make "install-diaframe-simuliris"]
diff --git a/supplements/diaframe_reloc/atomic_post_update.v b/supplements/diaframe_reloc/atomic_post_update.v
index 45bd1bf0..feea205a 100644
--- a/supplements/diaframe_reloc/atomic_post_update.v
+++ b/supplements/diaframe_reloc/atomic_post_update.v
@@ -1,4 +1,5 @@
From iris.bi Require Export bi telescopes lib.atomic.
+From iris.bi Require Import fixpoint_mono
From iris.proofmode Require Import tactics notation reduction.
From iris.program_logic Require Import weakestpre lifting atomic.
From diaframe Require Import proofmode_base.
@@ -28,7 +29,7 @@ Section atomic_post_acc.
Definition atomic_post_update_pre (Ψ : () → PROP) (_ : ()) : PROP :=
atomic_post_acc Eo Ei Ef α (Ψ ()) β Φ.
- Instance atomic_post_update_pre_mono : fixpoint.BiMonoPred atomic_post_update_pre.
+ Instance atomic_post_update_pre_mono : BiMonoPred atomic_post_update_pre.
Proof.
constructor.
- iIntros (P1 P2 ??) "#HP12". iIntros ([]) "AU".
@@ -42,7 +43,7 @@ Section atomic_post_acc.
Qed.
Definition atomic_post_update_def :=
- fixpoint.bi_greatest_fixpoint atomic_post_update_pre ().
+ bi_greatest_fixpoint atomic_post_update_pre ().
End atomic_post_acc.
(** Seal it *)
@@ -66,14 +67,14 @@ Section lemmas.
rewrite atomic.atomic_update_unseal /atomic.atomic_update_def.
rewrite atomic_post_update_eq /atomic_post_update_def.
apply (anti_symm _).
- - iApply (fixpoint.greatest_fixpoint_strong_mono with "[]").
+ - iApply (greatest_fixpoint_strong_mono with "[]").
{ apply atomic_update_pre_mono. }
iIntros "!>" (F' []).
rewrite /atomic_post_update_pre /atomic_update_pre.
rewrite /atomic_acc /atomic_post_acc.
iMod 1 as "[%x [Hα Hx]]".
iExists _. by iFrame.
- - iApply (fixpoint.greatest_fixpoint_strong_mono with "[]").
+ - iApply (greatest_fixpoint_strong_mono with "[]").
{ apply atomic_update_pre_mono. }
iIntros "!>" (F' []).
rewrite /atomic_post_update_pre /atomic_update_pre.
@@ -101,7 +102,7 @@ Section lemmas.
Proof.
rewrite atomic_post_update_eq /atomic_post_update_def.
iIntros "HΦ #(Ha & Hf)".
- iApply (fixpoint.greatest_fixpoint_strong_mono with "[] HΦ").
+ iApply (greatest_fixpoint_strong_mono with "[] HΦ").
iIntros "!>" (F' []).
rewrite /atomic_post_update_pre /atomic_post_acc.
iMod 1 as "[%x [Hα Hx]]".
@@ -160,10 +161,10 @@ Section lemmas.
move => Htrue P Q /=.
iIntros "[>[$ H] HQ] !>".
rewrite {2}atomic_post_update_eq /atomic_post_update_def.
- iApply (fixpoint.greatest_fixpoint_coiter _ (λ _, _) with "[] [H HQ]"); last iAccu.
+ iApply (greatest_fixpoint_coiter _ (λ _, _) with "[] [H HQ]"); last iAccu.
iIntros "!>" ([]) "[HAU HQ]".
rewrite /atomic_post_update_pre /atomic_post_acc.
- rewrite atomic_post_update_eq {1}/atomic_post_update_def fixpoint.greatest_fixpoint_unfold /atomic_post_update_pre /atomic_post_acc.
+ rewrite atomic_post_update_eq {1}/atomic_post_update_def greatest_fixpoint_unfold /atomic_post_update_pre /atomic_post_acc.
iMod "HAU" as "[%x [HP Hr]]".
iExists _. by iFrame.
Qed.
--
GitLab
From ad4c0188b7f34e859247fc80874a90cb1e6da594 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sat, 5 Apr 2025 23:04:12 +0100
Subject: [PATCH 7/9] Update attempt to transfinite Iris
---
diaframe/hint_search/instances_base.v | 12 +++++------
diaframe/lib/own/proofmode_instances.v | 3 ++-
diaframe/lib/own_hints.v | 30 +++++++++++++++-----------
diaframe/steps/verify_tac.v | 4 ++--
diaframe_heap_lang/base_hints.v | 2 +-
tests/modalities.ref | 2 +-
6 files changed, 29 insertions(+), 24 deletions(-)
diff --git a/diaframe/hint_search/instances_base.v b/diaframe/hint_search/instances_base.v
index 4747a49b..e430d107 100644
--- a/diaframe/hint_search/instances_base.v
+++ b/diaframe/hint_search/instances_base.v
@@ -74,10 +74,10 @@ Section biabd_instances.
iApply "H". by iRight.
Qed.
- Global Instance biabd_emp_valid {TTl TTr} p P Q M R S :
- AsEmpValid (BiAbd (TTl := TTl) (TTr := TTr) p P Q M R S) (∀.. (ttl : TTl), □?p P ∗ (tele_app R ttl) -∗ M $ ∃.. (ttr : TTr), tele_app Q ttr ∗ tele_app (tele_app S ttl) ttr).
+ Global Instance biabd_emp_valid {TTl TTr} d p P Q M R S :
+ AsEmpValid d (BiAbd (TTl := TTl) (TTr := TTr) p P Q M R S) (∀.. (ttl : TTl), □?p P ∗ (tele_app R ttl) -∗ M $ ∃.. (ttr : TTr), tele_app Q ttr ∗ tele_app (tele_app S ttl) ttr).
Proof.
- split.
+ split => _.
- rewrite /BiAbd /= => /tforall_forall HPQ.
iIntros (ttl) "HPR". rewrite HPQ //.
- rewrite /BiAbd tforall_forall /= => HPQ ttl.
@@ -124,10 +124,10 @@ Section abduction_instances.
HINT1 P ✱ [ emp ] ⊫ [id]; P | 50.
Proof. by rewrite /Abduct /= right_id. Qed.
- Global Instance abduct_emp_valid {TT} p P Q M R :
- AsEmpValid (Abduct (TT := TT) p P Q M R) (□?p P ∗ R -∗ M $ ∃.. (tt : TT), tele_app Q tt)%I.
+ Global Instance abduct_emp_valid {TT} d p P Q M R :
+ AsEmpValid d (Abduct (TT := TT) p P Q M R) (□?p P ∗ R -∗ M $ ∃.. (tt : TT), tele_app Q tt)%I.
Proof.
- split; rewrite /Abduct /=.
+ split => _; rewrite /Abduct /=.
- move => -> //. iIntros "$".
- move => HPQ. iApply HPQ.
Qed.
diff --git a/diaframe/lib/own/proofmode_instances.v b/diaframe/lib/own/proofmode_instances.v
index e4bd391e..1ad8d44a 100644
--- a/diaframe/lib/own/proofmode_instances.v
+++ b/diaframe/lib/own/proofmode_instances.v
@@ -6,7 +6,8 @@ From diaframe.lib.own Require Import proofmode_classes.
(* TODO: Remove this file once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/771 is merged *)
-Local Instance includedI_into_pure `{CmraDiscrete A} (a b : A) {Σ} : IntoPure (PROP := iPropI Σ) (a ≼ b)%I (a ≼ b).
+Local Instance includedI_into_pure `{@CmraDiscrete natSI A} (a b : A) {Σ} :
+ IntoPure (PROP := iPropI Σ) (a ≼ b)%I (a ≼ b).
Proof.
rewrite /IntoPure. iDestruct 1 as (c) "%"; iPureIntro.
by eexists.
diff --git a/diaframe/lib/own_hints.v b/diaframe/lib/own_hints.v
index 6db9f939..59aacd25 100644
--- a/diaframe/lib/own_hints.v
+++ b/diaframe/lib/own_hints.v
@@ -3,12 +3,12 @@ From iris.algebra Require Import local_updates excl auth lib.frac_auth csum.
(* Diaframe hint library aimed at automatically deriving good hints for owned propositions.
Supports most of the (recursive) building blocks for cmra's found in iris.algebra *)
-Class FindLocalUpdate {A : cmra} (x x' y y' : A) (φ : Prop) :=
+Class FindLocalUpdate {SI : sidx} {A : cmra} (x x' y y' : A) (φ : Prop) :=
find_local_update : φ → (x, y) ~l~> (x', y').
-Global Hint Mode FindLocalUpdate ! ! ! - - - : typeclass_instances.
+Global Hint Mode FindLocalUpdate + ! ! ! - - - : typeclass_instances.
Section base_local_updates.
- Lemma find_local_update_incomparable {A : ucmra} (x x' : A) :
+ Lemma find_local_update_incomparable {SI : sidx} {A : ucmra} (x x' : A) :
Cancelable x →
(* This is needed to find things like
(Some (Cinl x), Some (Cinl x)) ~l~> (Some (Cinr x'), Some (Cinr x'))
@@ -34,7 +34,7 @@ Section base_local_updates.
but its useful/fast for cmras which do not have that: nat, positive, GSet, GMultiset. how to improve..?
Proof. done. Qed. *)
- Global Instance find_local_update_from_prod_both {A B : cmra} (x1 x1' y1 y1' : A) (x2 x2' y2 y2' : B) φ1 φ2 :
+ Global Instance find_local_update_from_prod_both {SI : sidx} {A B : cmra} (x1 x1' y1 y1' : A) (x2 x2' y2 y2' : B) φ1 φ2 :
FindLocalUpdate x1 x1' y1 y1' φ1 →
FindLocalUpdate x2 x2' y2 y2' φ2 →
FindLocalUpdate (x1, x2) (x1', x2') (y1, y2) (y1', y2') (φ1 ∧ φ2) | 150.
@@ -43,7 +43,7 @@ Section base_local_updates.
apply prod_local_update' => //.
Qed.
- Global Instance find_local_update_from_prod_left {A B : cmra} (x1 x1' y1 y1' : A) (x2 y2 : B) φ :
+ Global Instance find_local_update_from_prod_left {SI : sidx} {A B : cmra} (x1 x1' y1 y1' : A) (x2 y2 : B) φ :
FindLocalUpdate x1 x1' y1 y1' φ →
FindLocalUpdate (x1, x2) (x1', x2) (y1, y2) (y1', y2) φ | 160.
Proof.
@@ -51,7 +51,7 @@ Section base_local_updates.
apply prod_local_update_1 => //.
Qed.
- Global Instance find_local_update_from_prod_right {A B : cmra} (x1 y1 : A) (x2 x2' y2 y2' : B) φ :
+ Global Instance find_local_update_from_prod_right {SI : sidx} {A B : cmra} (x1 y1 : A) (x2 x2' y2 y2' : B) φ :
FindLocalUpdate x2 x2' y2 y2' φ →
FindLocalUpdate (x1, x2) (x1, x2') (y1, y2) (y1, y2') φ | 160.
Proof.
@@ -59,32 +59,32 @@ Section base_local_updates.
apply prod_local_update_2 => //.
Qed.
- Global Instance find_local_update_some {A : cmra} (x x' y y' : A) φ :
+ Global Instance find_local_update_some {SI : sidx} {A : cmra} (x x' y y' : A) φ :
FindLocalUpdate x x' y y' φ →
FindLocalUpdate (Some x) (Some x') (Some y) (Some y') φ | 210.
Proof. move => H /H H'. by apply option_local_update. Qed.
- Global Instance find_local_update_exclusive {A : ofe} (x x' y : exclR A) :
+ Global Instance find_local_update_exclusive {SI : sidx} {A : ofe} (x x' y : exclR A) :
FindLocalUpdate x x' y x' (✓ x') | 150.
Proof. move => Hx1 Hx2. by apply exclusive_local_update. Qed.
- Global Instance sum_inl_find_local_update {A1 A2 : cmra} (x x' y y' : A1) φ :
+ Global Instance sum_inl_find_local_update {SI : sidx} {A1 A2 : cmra} (x x' y y' : A1) φ :
FindLocalUpdate x x' y y' φ →
FindLocalUpdate (Cinl (B:=A2) x) (Cinl x') (Cinl y) (Cinl y') φ | 150.
Proof. move => H /H H'. by apply csum_local_update_l. Qed.
- Global Instance sum_inr_find_local_update {A1 A2 : cmra} (x x' y y' : A1) φ :
+ Global Instance sum_inr_find_local_update {SI : sidx} {A1 A2 : cmra} (x x' y y' : A1) φ :
FindLocalUpdate x x' y y' φ →
FindLocalUpdate (Cinr (A:=A2) x) (Cinr x') (Cinr y) (Cinr y') φ | 150.
Proof. move => H /H H'. by apply csum_local_update_r. Qed.
- Global Instance sum_inl_inr_swap_local_update {A1 A2 : cmra} (x : A1) (x' : A2) :
+ Global Instance sum_inl_inr_swap_local_update {SI : sidx} {A1 A2 : cmra} (x : A1) (x' : A2) :
Cancelable (Some $ Cinl (B :=A2) x) →
FindLocalUpdate (Some $ Cinl (B:=A2) x) (Some $ Cinr (A:=A1) x') (Some $ Cinl (B:=A2) x)
(Some $ Cinr (A:=A1) x') (✓ x') | 160.
Proof. eapply (find_local_update_incomparable (A := optionUR $ csumR A1 A2)). Qed.
- Global Instance sum_inr_inl_swap_local_update {A1 A2 : cmra} (x : A1) (x' : A2) :
+ Global Instance sum_inr_inl_swap_local_update {SI : sidx} {A1 A2 : cmra} (x : A1) (x' : A2) :
Cancelable (Some $ Cinr (A :=A2) x) →
FindLocalUpdate (Some $ Cinr (A:=A2) x) (Some $ Cinl (B:=A1) x') (Some $ Cinr (A:=A2) x)
(Some $ Cinl (B:=A1) x') (✓ x') | 160.
@@ -92,10 +92,11 @@ Section base_local_updates.
End base_local_updates.
-Class AsCmraUnit {A : ucmra} (x : A) :=
+Class AsCmraUnit {SI : sidx} {A : ucmra} (x : A) :=
as_cmra_unit : x = ε.
Section base_as_unit.
+ Context {SI : sidx}.
Implicit Types A : ucmra.
Global Instance unit_as_unit {A} : AsCmraUnit (A := A) ε | 99.
@@ -117,6 +118,8 @@ From iris.algebra Require Import numbers.
From diaframe Require Import solve_defs util_classes.
Section number_updates.
+ Context {SI : sidx}.
+
Global Instance natO_local_update (x x' y : nat) :
FindLocalUpdate x x' y (x' + y - x) (x ≤ x' + y) | 150.
Proof.
@@ -233,6 +236,7 @@ End number_updates.
From iris.algebra Require Import gset.
Section set_updates.
+ Context {SI : sidx}.
Context `{Countable K}.
Implicit Types X Y : gset K.
diff --git a/diaframe/steps/verify_tac.v b/diaframe/steps/verify_tac.v
index e6c8234e..98d538b6 100644
--- a/diaframe/steps/verify_tac.v
+++ b/diaframe/steps/verify_tac.v
@@ -15,8 +15,8 @@ Ltac inside_step :=
lazymatch goal with
| |- subG _ _ → _ => solve_inG
| |- IntoWand2 _ _ _ _ => rewrite /IntoWand2 /=; iStartProof
- | |- forall n : nat, respectful (dist n) (dist n) ?P ?P => solve_proper
- | |- forall n : nat, respectful (dist_later n) (dist n) ?P ?P => solve_contractive
+ | |- respectful (dist ?n) (dist ?n) ?P ?P => solve_proper
+ | |- respectful (dist_later ?n) (dist ?n) ?P ?P => solve_contractive
| |- (∀ a, _) =>
intros a;
inside_step
diff --git a/diaframe_heap_lang/base_hints.v b/diaframe_heap_lang/base_hints.v
index 79ac03ba..fbb5c420 100644
--- a/diaframe_heap_lang/base_hints.v
+++ b/diaframe_heap_lang/base_hints.v
@@ -308,7 +308,7 @@ Section instances.
Lemma array_from_shorter vs1 vs2 l l' q :
SolveSepSideCondition (0 < length vs1 ≤ length vs2) →
ComputeOffsetLoc l (length vs1) l' →
- HINT l ↦∗{q} vs1 ✱ [- ; ⌜take (length vs1) vs2 = vs1⌠∗ l' ↦∗{q} (list.drop (length vs1) vs2) ] ⊫ [id];
+ HINT l ↦∗{q} vs1 ✱ [- ; ⌜take (length vs1) vs2 = vs1⌠∗ l' ↦∗{q} (drop (length vs1) vs2) ] ⊫ [id];
l ↦∗{q} vs2 ✱ [emp].
Proof.
rewrite /SolveSepSideCondition => Hl <- /=.
diff --git a/tests/modalities.ref b/tests/modalities.ref
index c5213d18..3381a4ed 100644
--- a/tests/modalities.ref
+++ b/tests/modalities.ref
@@ -18,4 +18,4 @@ No applicable tactic.
(∨)
Q ∗ R
The command has indeed failed with message:
-Uncaught Ltac2 exception: Tactic_failure None
+Uncaught Ltac2 exception: Tactic_failure (None)
--
GitLab
From 567885ab4c7f364be91a48419336ccb1ef4fd41e Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sat, 5 Apr 2025 23:26:36 +0100
Subject: [PATCH 8/9] Fix test case
---
tests/modalities.ref | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tests/modalities.ref b/tests/modalities.ref
index 3381a4ed..c5213d18 100644
--- a/tests/modalities.ref
+++ b/tests/modalities.ref
@@ -18,4 +18,4 @@ No applicable tactic.
(∨)
Q ∗ R
The command has indeed failed with message:
-Uncaught Ltac2 exception: Tactic_failure (None)
+Uncaught Ltac2 exception: Tactic_failure None
--
GitLab
From af82c11584f6d73776fc7471b7d90c3c1a9ab7b5 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sun, 6 Apr 2025 10:48:14 +0100
Subject: [PATCH 9/9] Missed a dot
---
supplements/diaframe_reloc/atomic_post_update.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/supplements/diaframe_reloc/atomic_post_update.v b/supplements/diaframe_reloc/atomic_post_update.v
index feea205a..63241359 100644
--- a/supplements/diaframe_reloc/atomic_post_update.v
+++ b/supplements/diaframe_reloc/atomic_post_update.v
@@ -1,5 +1,5 @@
From iris.bi Require Export bi telescopes lib.atomic.
-From iris.bi Require Import fixpoint_mono
+From iris.bi Require Import fixpoint_mono.
From iris.proofmode Require Import tactics notation reduction.
From iris.program_logic Require Import weakestpre lifting atomic.
From diaframe Require Import proofmode_base.
--
GitLab