From 0e605cfd494c3689692cff90915c7ba1cf03b2c1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Nov 2019 11:07:44 +0100
Subject: [PATCH] Bump Iris and fix compilation with Coq master.
Due to changes to Coq's import mechanism, I now made sure that
Autusubst is imported first. This caused various things to break,
which I patched up.
---
opam | 2 +-
theories/examples/par.v | 10 ++---
theories/examples/symbol.v | 4 +-
theories/examples/various.v | 52 ++++++++++++-------------
theories/logic/adequacy.v | 2 +-
theories/logic/spec_ra.v | 2 +-
theories/prelude/asubst.v | 5 +--
theories/typing/contextual_refinement.v | 5 +--
theories/typing/interp.v | 2 +-
theories/typing/soundness.v | 2 +-
theories/typing/types.v | 4 +-
11 files changed, 43 insertions(+), 47 deletions(-)
diff --git a/opam b/opam
index 645f50a..193e3a0 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
- "coq-iris" { (= "dev.2019-10-25.0.bbd38120") | (= "dev") }
+ "coq-iris" { (= "dev.2019-11-07.1.891124d6") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/examples/par.v b/theories/examples/par.v
index b23b34e..f102f15 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -60,7 +60,7 @@ Section rules.
iApply (refines_bind with "He").
iIntros (v v') "Hv". simpl.
repeat rel_pure_l.
- rel_bind_l (join _).
+ rel_bind_l (spawn.join _).
iApply refines_wp_l.
iApply (join_spec with "hndl").
iNext. iIntros (?) "_". simpl.
@@ -104,7 +104,7 @@ Section rules.
rewrite {3}refines_eq /refines_def. iIntros (Ï) "#HÏ".
iIntros (j K) "Hj". iModIntro.
tp_bind j e2.
- pose (C:=(AppRCtx (λ: "v2", let: "v1" := join #c2 in ("v1", "v2")) :: K)).
+ pose (C:=(AppRCtx (λ: "v2", let: "v1" := spawn.join #c2 in ("v1", "v2")) :: K)).
fold C.
pose (N:=nroot.@"par").
wp_bind (spawn _).
@@ -119,7 +119,7 @@ Section rules.
iMod ("He1" with "HÏ Hi") as "He1".
iApply (wp_wand with "He1").
iIntros (v1). iDestruct 1 as (v2) "[Hi Hv]".
- wp_pures. wp_bind (join _).
+ wp_pures. wp_bind (spawn.join _).
iApply (join_spec with "l_hndl").
iNext. iIntros (w1). iDestruct 1 as (w2) "[Hj Hw]".
unfold C. iSimpl in "Hi". iSimpl in "Hj".
@@ -128,7 +128,7 @@ Section rules.
(* TODO: better tp_pure tactics *)
tp_pure j (Lam _ _). simpl.
tp_rec j. simpl.
- tp_bind j (join _). unlock join.
+ tp_bind j (spawn.join _). unlock spawn.join.
tp_pure j (App _ #c2). simpl.
iApply fupd_wp. tp_load j. simpl.
tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
@@ -172,7 +172,7 @@ Section rules.
(* TODO: better tp_pure tactics *)
tp_pure j (Lam _ _). simpl.
tp_rec j. simpl.
- tp_bind j (join _). unlock join.
+ tp_bind j (spawn.join _). unlock spawn.join.
tp_pure j (App _ #c2). simpl.
tp_load j. simpl.
tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 7117295..e3d70b1 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -266,7 +266,7 @@ Section proof.
iMod (same_size with "[$Ha $Hf]") as "[Ha #Hf]".
iMod (inc_size with "Ha") as "Ha".
iDestruct "Hs2" as "[Hs2 Hs2']".
- replace (m' + 1) with (Z.of_nat (S m')); last lia.
+ replace (m' + 1)%Z with (Z.of_nat (S m')); last lia.
iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
{ iNext. iExists _,_. by iFrame. }
rel_load_l. repeat rel_pure_l.
@@ -345,7 +345,7 @@ Section proof.
iMod (same_size with "[$Ha $Hf]") as "[Ha #Hf]".
iMod (inc_size with "Ha") as "Ha".
iDestruct "Hs2" as "[Hs2 Hs2']".
- replace (m' + 1) with (Z.of_nat (S m')); last lia.
+ replace (m' + 1)%Z with (Z.of_nat (S m')); last lia.
iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
{ iNext. iExists _,_. by iFrame. }
rel_load_l. repeat rel_pure_l.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index b884eb7..ad6bd1e 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -236,7 +236,7 @@ Section proofs.
compute in Hfoo. eauto. }
iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
{ iNext. iExists (S n).
- replace (Z.of_nat (S n)) with (n + 1) by lia.
+ replace (Z.of_nat (S n)) with (n + 1)%Z by lia.
iFrame. }
repeat rel_pure_l. repeat rel_pure_r.
rel_store_l_atomic. clear n'.
@@ -250,7 +250,7 @@ Section proofs.
rel_store_r.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (S n).
- replace (Z.of_nat (S n)) with (n + 1) by lia.
+ replace (Z.of_nat (S n)) with (n + 1)%Z by lia.
iFrame. iLeft. iFrame. }
rel_values. }
- rel_pure_l. rel_pure_r. iApply refines_arrow.
@@ -389,27 +389,27 @@ Section proofs.
iApply ("Hcl" with "[-]"); iNext.
+ iExists n. iLeft. iFrame.
+ iExists (n-1)%nat. iRight.
- replace (Z.of_nat (n-1)%nat) with (Z.of_nat n - 1) by lia.
- replace (n - 1 + 1) with (Z.of_nat n) by lia.
+ replace (Z.of_nat (n - 1)) with (Z.of_nat n - 1)%Z by lia.
+ replace (n - 1 + 1)%Z with (Z.of_nat n) by lia.
iFrame. }
{ iIntros "[Hc1 Hc] _".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
- rel_apply_r (FG_increment_r with "Hc2"). iIntros "Hc2".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (n + 1)%nat.
- replace (Z.of_nat (n + 1)%nat) with (Z.of_nat n + 1) by lia.
+ replace (Z.of_nat (n + 1)) with (Z.of_nat n + 1)%Z by lia.
iLeft; iFrame. }
rel_values.
- - replace (Z.of_nat n - 1) with (Z.of_nat (n - 1)%nat) by lia.
+ - replace (Z.of_nat n - 1)%Z with (Z.of_nat (n - 1)) by lia.
rel_apply_r (FG_increment_r with "Hc2"). iIntros "Hc2".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists n. iRight; iFrame.
- by replace ((n - 1)%nat + 1) with (Z.of_nat n) by lia. }
+ by replace ((n - 1)%nat + 1)%Z with (Z.of_nat n) by lia. }
rel_values. }
- - iModIntro. iExists (n+1)%nat.
- replace (Z.of_nat n + 1) with (Z.of_nat (n+1)) by lia. iFrame.
+ - iModIntro. iExists (n + 1)%nat.
+ replace (Z.of_nat n + 1)%Z with (Z.of_nat (n + 1)) by lia. iFrame.
iSplitL "Hc2 Ht".
- { iRight. replace ((n + 1)%nat - 1) with (Z.of_nat n) by lia.
+ { iRight. replace ((n + 1)%nat - 1)%Z with (Z.of_nat n) by lia.
iFrame. iDestruct "Ht" as "[$ $]".
iPureIntro. lia. }
iSplit.
@@ -418,8 +418,8 @@ Section proofs.
+ iExists (S n). iLeft.
replace (Z.of_nat (n + 1)) with (Z.of_nat (S n)) by lia. iFrame.
+ iExists n. iRight. iFrame.
- replace (Z.of_nat (n + 1)) with (Z.of_nat n + 1) by lia.
- replace (n + 1 - 1) with (Z.of_nat n) by lia.
+ replace (Z.of_nat (n + 1)) with (Z.of_nat n + 1)%Z by lia.
+ replace (n + 1 - 1)%Z with (Z.of_nat n) by lia.
iFrame. }
{ iIntros "[Hc1 Hc] _".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
@@ -427,16 +427,16 @@ Section proofs.
iIntros "Hc2".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (S (S n)).
- replace ((n+1)%nat + 1) with (Z.of_nat (S (S n))) by lia.
+ replace ((n+1)%nat + 1)%Z with (Z.of_nat (S (S n))) by lia.
iLeft; iFrame. }
rel_values.
- - replace ((n + 1)%nat + 1) with (Z.of_nat (S n) + 1) by lia.
- replace ((n + 1)%nat - 1) with (Z.of_nat n) by lia.
+ - replace ((n + 1)%nat + 1)%Z with (Z.of_nat (S n) + 1)%Z by lia.
+ replace ((n + 1)%nat - 1)%Z with (Z.of_nat n) by lia.
rel_apply_r (FG_increment_r with "Hc2").
iIntros "Hc2".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (S n). iRight. iFrame.
- by replace (n + 1) with (Z.of_nat (S n)) by lia. }
+ by replace (n + 1)%Z with (Z.of_nat (S n)) by lia. }
rel_values. }
Qed.
@@ -464,8 +464,8 @@ Section proofs.
iDestruct 1 as (m) "[Hc1 Hc2]".
iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]";
[iExists m; iLeft | iExists (m - 1)%nat; iRight]; iFrame.
- replace ((m - 1)%nat + 1) with (Z.of_nat m) by lia.
- replace (Z.of_nat (m - 1)%nat) with (Z.of_nat m - 1) by lia.
+ replace ((m - 1)%nat + 1)%Z with (Z.of_nat m) by lia.
+ replace (Z.of_nat (m - 1)) with (Z.of_nat m - 1)%Z by lia.
iFrame.
Qed.
@@ -490,7 +490,7 @@ Section proofs.
iMod (shoot γ with "Hp") as "#Hs".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists m. iRight. iFrame.
- replace (Z.of_nat (S m)) with (Z.of_nat m + 1) by lia. by iFrame. }
+ replace (Z.of_nat (S m)) with (Z.of_nat m + 1)%Z by lia. by iFrame. }
iApply (refines_seq lrel_unit).
{ iApply (refines_app with "Hg").
rel_values. }
@@ -551,18 +551,18 @@ Section proofs.
iAlways.
iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
iModIntro; last first.
- { iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1) by lia.
+ { iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z by lia.
iFrame. iSplitL "Hc2 Ht Ht'2".
- { iRight. simpl. replace (n + 1 - 1) with (Z.of_nat n) by lia.
- iFrame. iPureIntro. omega. }
+ { iRight. simpl. replace (n + 1 - 1)%Z with (Z.of_nat n) by lia.
+ iFrame. iPureIntro. lia. }
iSplit.
- iIntros. iApply "Hcl". iApply close_i6.
- iNext. iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1) by lia.
+ iNext. iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z by lia.
iFrame.
- iIntros "[Hc1 Hc2] Ht".
rel_pure_l. rel_pure_l.
- replace (n + 1 + 1) with (Z.of_nat (S (S n))) by lia.
- replace (n + 1) with (Z.of_nat (S n)) by lia.
+ replace (n + 1 + 1)%Z with (Z.of_nat (S (S n))) by lia.
+ replace (n + 1)%Z with (Z.of_nat (S n)) by lia.
iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
}
{ iExists n. iFrame "Hc1". iSplitL "Hc2 Ht".
@@ -572,7 +572,7 @@ Section proofs.
iNext. iExists _; iFrame.
- iIntros "[Hc1 Hc2] Ht".
rel_pure_l. rel_pure_l.
- replace (n + 1) with (Z.of_nat (S n)) by lia.
+ replace (n + 1)%Z with (Z.of_nat (S n)) by lia.
iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
}
Qed.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index caa0974..5e771d3 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -67,7 +67,7 @@ Theorem refines_typesafety Σ `{relocPreG Σ} e e' e1
(A : ∀ `{relocG Σ}, lrel Σ) thp σ σ' :
(∀ `{relocG Σ}, REL e << e' : A) →
rtc erased_step ([e], σ) (thp, σ') → e1 ∈ thp →
- is_Some (to_val e1) ∨ reducible e1 σ'.
+ not_stuck e1 σ'.
Proof.
intros Hlog ??.
cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h) ∧ True)); first (intros [_ ?]; eauto).
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 9f481b0..e56bdb6 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -81,7 +81,7 @@ Section conversions.
Qed.
Lemma tpool_lookup_Some tp j e : to_tpool tp !! j = Excl' e → tp !! j = Some e.
Proof. rewrite tpool_lookup fmap_Some. naive_solver. Qed.
- Hint Resolve tpool_lookup_Some.
+ Hint Resolve tpool_lookup_Some : core.
Lemma to_tpool_insert tp j e :
j < length tp →
diff --git a/theories/prelude/asubst.v b/theories/prelude/asubst.v
index 15e1b7c..a53f6b9 100644
--- a/theories/prelude/asubst.v
+++ b/theories/prelude/asubst.v
@@ -1,9 +1,6 @@
(** Autosubst helper lemmata *)
-From stdpp Require Export base numbers.
-From Coq.ssr Require Export ssreflect.
-Global Open Scope general_if_scope.
-(* ^ otherwise ssreflects overwrites `if` *)
From Autosubst Require Export Autosubst.
+From iris.algebra Require Export base.
Section Autosubst_Lemmas.
Context {term : Type} {Ids_term : Ids term}
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 40dc478..7ff8d31 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -1,11 +1,10 @@
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** Notion of contextual refinement & proof that it is a precongruence wrt the logical relation *)
+From Autosubst Require Import Autosubst.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From reloc.typing Require Export types interp fundamental.
-From Autosubst Require Import Autosubst.
-
Inductive ctx_item :=
(* λ-rec *)
| CTX_Rec (f x: binder)
@@ -155,7 +154,7 @@ Inductive typed_ctx_item :
| TP_CTX_Unfold Γ τ :
typed_ctx_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
| TP_CTX_TLam Γ τ :
- typed_ctx_item CTX_TLam (subst (ren (+1%nat)) <$> Γ) τ Γ (TForall τ)
+ typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Γ) τ Γ (TForall τ)
| TP_CTX_TApp Γ τ τ' :
typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
(* | TP_CTX_Pack Γ τ τ' : *)
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 21cf35a..8db15c5 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -1,11 +1,11 @@
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** Interpretations for System F_mu_ref types *)
+From Autosubst Require Import Autosubst.
From iris.algebra Require Export list.
From iris.proofmode Require Import tactics.
From reloc.typing Require Export types.
From reloc.logic Require Import model.
From reloc.prelude Require Import properness asubst.
-From Autosubst Require Import Autosubst.
(** * Interpretation of types *)
Section semtypes.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index e22a0b8..5a22da8 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -27,7 +27,7 @@ Qed.
Theorem logrel_typesafety Σ `{relocPreG Σ} e e' τ thp σ σ' :
(∀ `{relocG Σ} Δ, {⊤;Δ;∅} ⊨ e ≤log≤ e : τ) →
rtc erased_step ([e], σ) (thp, σ') → e' ∈ thp →
- is_Some (to_val e') ∨ reducible e' σ'.
+ not_stuck e' σ'.
Proof.
intros Hlog ??.
cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))); first (intros [_ ?]; eauto).
diff --git a/theories/typing/types.v b/theories/typing/types.v
index ecc67ba..b2fa1d2 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -1,8 +1,8 @@
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** (Syntactic) Typing for System F_mu_ref with existential types and concurrency *)
+From Autosubst Require Export Autosubst.
From stdpp Require Export stringmap.
From iris.heap_lang Require Export lang notation metatheory.
-From Autosubst Require Export Autosubst.
(** * Types *)
Inductive type :=
@@ -143,7 +143,7 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
| TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
| TUnpack e1 x e2 Ï„ Ï„2 :
Γ ⊢ₜ e1 : TExists τ →
- <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (subst (ren (+1%nat)) τ2) →
+ <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (Autosubst_Classes.subst (ren (+1%nat)) τ2) →
Γ ⊢ₜ (unpack: x := e1 in e2) : τ2
| TFork e : Γ ⊢ₜ e : TUnit → Γ ⊢ₜ Fork e : TUnit
| TAlloc e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ
--
GitLab