From 0e60fa20f833bf4b2e20c9cfe41725b805b7f7af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Mar 2021 17:22:50 +0100
Subject: [PATCH] more comments explaining the weakened typing rule
---
theories/typing/examples/nonlexical.v | 4 +++-
theories/typing/programs.v | 17 +++++++++++++++--
2 files changed, 18 insertions(+), 3 deletions(-)
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 36a28ed6..7e78bb31 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -116,7 +116,9 @@ Section non_lexical.
iIntros (unwrap'). simpl_subst.
iApply (type_letcall ()); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_jump; solve_typing.
- - iApply (type_equivalize_lft _ _ _ _ [_; _; _; _; _; _; _; _]).
+ - (* Use lifetime equalization to replace one lifetime by another:
+ [&uniq{κ} V] becomes [&uniq{m} V] in the type of [o +ₗ #1]. *)
+ iApply (type_equivalize_lft _ _ _ _ [_; _; _; _; _; _; _; _]).
{ iIntros (tid) "#LFT #Hκ1 #Hκ2 ($ & Href & $ & $ & $ & $ & $ & $ & _)".
rewrite -tctx_interp_singleton.
iApply (type_incl_tctx_incl with "[] Href").
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 60b717af..220bd01c 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -119,8 +119,21 @@ Section typing_rules.
typed_body E L C T e -∗ typed_body E L C T e.
Proof. done. Qed.
- (** This version is *weaker* than what was in the original paper;
- it had to be adjusted for GhostCell. *)
+ (** This lemma can replace [κ1] by [κ2] and vice versa in positions that
+ respect "semantic lifetime equivalence"; in particular, lifetimes of
+ references can be adjusted this way. However, it cannot replace lifetimes in
+ other type constructors, as those might only respect *syntactic* lifetime
+ equivalence. This lemma is *weaker* than what was in the original paper where
+ lifetimes could be replaced everywhere; it had to be adjusted for GhostCell.
+ See [typing.lib.diverging_static] for an example of how
+ [type_equivalize_lft_static] without this restriction ciuld be used to subvert
+ branding.
+
+ This is technically not a proper typing rule since the type system has no way
+ to express "subtyping wrt semantic lifetime inclusion". However, there is no
+ fundamental reason that we could not also reflect all these semantic facts on
+ the syntactic side, it would just be very clunky (and note that in Coq we do
+ not reflect this syntactic side anway). *)
Lemma type_equivalize_lft E L C T1 T2 κ1 κ2 e :
(∀ tid, lft_ctx -∗ κ1 ⊑ κ2 -∗ κ2 ⊑ κ1 -∗ tctx_interp tid T1 -∗ tctx_interp tid T2) →
(⊢ typed_body E L C T2 e) →
--
GitLab