From d698a0c45d07699fccee04594f4c97b9ccdc0f3b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 6 Mar 2020 13:56:59 +0100
Subject: [PATCH] Add FAA to the type system
---
_CoqProject | 1 +
theories/reloc.v | 2 +-
theories/typing/contextual_refinement.v | 32 +++++++---
theories/typing/fundamental.v | 25 ++++++++
theories/typing/tactics.v | 84 +++++++++++++++++++++++++
theories/typing/types.v | 71 ++++++++++++++-------
6 files changed, 186 insertions(+), 29 deletions(-)
create mode 100644 theories/typing/tactics.v
diff --git a/_CoqProject b/_CoqProject
index 50b5c06..3bd069d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -30,6 +30,7 @@ theories/typing/types.v
theories/typing/interp.v
theories/typing/fundamental.v
theories/typing/contextual_refinement.v
+theories/typing/tactics.v
theories/typing/soundness.v
theories/reloc.v
diff --git a/theories/reloc.v b/theories/reloc.v
index 9e4e1d3..fed94d6 100644
--- a/theories/reloc.v
+++ b/theories/reloc.v
@@ -2,4 +2,4 @@ From iris.heap_lang Require Export lang notation proofmode.
From iris.proofmode Require Export tactics.
From reloc.logic Require Export proofmode.tactics proofmode.spec_tactics model.
From reloc.logic Require Export rules derived compatibility.
-From reloc.typing Require Export interp soundness.
+From reloc.typing Require Export interp tactics soundness.
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index e604379..74c7248 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -39,9 +39,8 @@ Inductive ctx_item :=
| CTX_CmpXchgL (e1 : expr) (e2 : expr)
| CTX_CmpXchgM (e0 : expr) (e2 : expr)
| CTX_CmpXchgR (e0 : expr) (e1 : expr)
- | CTX_FAAL (e1 : expr) (e2 : expr)
- | CTX_FAAM (e0 : expr) (e2 : expr)
- | CTX_FAAR (e0 : expr) (e1 : expr)
+ | CTX_FAAL (e1 : expr)
+ | CTX_FAAR (e0 : expr)
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
@@ -88,9 +87,8 @@ Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
| CTX_CmpXchgL e1 e2 => CmpXchg e e1 e2
| CTX_CmpXchgM e0 e2 => CmpXchg e0 e e2
| CTX_CmpXchgR e0 e1 => CmpXchg e0 e1 e
- | CTX_FAAL e1 e2 => FAA e e1 e2
- | CTX_FAAM e0 e2 => FAA e0 e e2
- | CTX_FAAR e0 e1 => FAA e0 e1 e
+ | CTX_FAAL e1 => FAA e e1
+ | CTX_FAAR e0 => FAA e0 e
(* Recursive & polymorphic types *)
| CTX_Fold => e
| CTX_Unfold => rec_unfold e
@@ -181,7 +179,13 @@ Inductive typed_ctx_item :
| TP_CTX_StoreR Γ e1 τ :
typed Γ e1 (Tref τ) →
typed_ctx_item (CTX_StoreR e1) Γ τ Γ TUnit
- | TP_CTX_CasL Γ e1 e2 τ :
+ | TP_CTX_FAAL Γ e2 :
+ Γ ⊢ₜ e2 : TNat →
+ typed_ctx_item (CTX_FAAL e2) Γ (Tref TNat) Γ TNat
+ | TP_CTX_FAAR Γ e1 :
+ Γ ⊢ₜ e1 : Tref TNat →
+ typed_ctx_item (CTX_FAAR e1) Γ TNat Γ TNat
+ | TP_CTX_CasL Γ e1 e2 τ :
EqType τ → UnboxedType τ →
typed Γ e1 τ → typed Γ e2 τ →
typed_ctx_item (CTX_CmpXchgL e1 e2) Γ (Tref τ) Γ (TProd τ TBool)
@@ -287,6 +291,14 @@ Proof.
eapply typed_ctx_compose; eauto.
Qed.
+
+Definition ctx_equiv Γ e1 e2 τ :=
+ (Γ ⊨ e1 ≤ctx≤ e2 : τ) ∧ (Γ ⊨ e2 ≤ctx≤ e1 : τ).
+
+Notation "Γ ⊨ e '=ctx=' e' : τ" :=
+ (ctx_equiv Γ e e' τ) (at level 100, e, e' at next level, τ at level 200).
+
+
Section bin_log_related_under_typed_ctx.
Context `{relocG Σ}.
@@ -371,6 +383,12 @@ Section bin_log_related_under_typed_ctx.
+ iApply (bin_log_related_store with "[]");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ + iApply bin_log_related_FAA;
+ try (by iApply fundamental); eauto.
+ iApply (IHK with "Hrel").
+ + iApply bin_log_related_FAA;
+ try (by iApply fundamental); eauto.
+ iApply (IHK with "Hrel").
+ iApply (bin_log_related_CmpXchg with "[] []");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index f11af98..009e8fd 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -274,6 +274,29 @@ Section fundamental.
- by iApply "IH2".
Qed.
+ Lemma bin_log_related_FAA Δ Γ e1 e2 e1' e2' :
+ ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref TNat) -∗
+ ({Δ;Γ} ⊨ e2 ≤log≤ e2' : TNat) -∗
+ {Δ;Γ} ⊨ FAA e1 e2 ≤log≤ FAA e1' e2' : TNat.
+ Proof.
+ iIntros "IH1 IH2".
+ intro_clause.
+ rel_bind_ap e2 e2' "IH2" v2 v2' "#IH2".
+ rel_bind_ap e1 e1' "IH1" v1 v1' "#IH1".
+ iDestruct "IH1" as (l l') "(% & % & Hinv)"; simplify_eq/=.
+ iDestruct "IH2" as (n) "[% %]". simplify_eq.
+ rel_apply_l refines_faa_l.
+ iInv (relocN .@ "ref" .@ (l,l')) as (v1 v1') "[Hv1 [>Hv2 #>Hv]]" "Hclose".
+ iDestruct "Hv" as (n1) "[% %]"; simplify_eq.
+ iModIntro. iExists _; iFrame. iNext.
+ iIntros "Hl".
+ (* TODO: tactics for these operations *)
+ rel_apply_r (refines_faa_r with "Hv2"). iIntros "Hv2".
+ iMod ("Hclose" with "[-]") as "_".
+ { iNext. iExists _,_. iFrame. iExists _; iSplit; eauto. }
+ rel_values.
+ Qed.
+
Lemma bin_log_related_CmpXchg Δ Γ e1 e2 e3 e1' e2' e3' τ
(HEqτ : EqType τ)
(HUbτ : UnboxedType τ) :
@@ -518,6 +541,8 @@ Section fundamental.
+ iApply bin_log_related_alloc; by iApply fundamental.
+ iApply bin_log_related_load; by iApply fundamental.
+ iApply bin_log_related_store; by iApply fundamental.
+ + iApply bin_log_related_FAA; eauto;
+ by iApply fundamental.
+ iApply bin_log_related_CmpXchg; eauto;
by iApply fundamental.
- intros Hv. destruct Hv; simpl.
diff --git a/theories/typing/tactics.v b/theories/typing/tactics.v
new file mode 100644
index 0000000..817fb07
--- /dev/null
+++ b/theories/typing/tactics.v
@@ -0,0 +1,84 @@
+From reloc.typing Require Export types contextual_refinement.
+
+Lemma tac_ctx_bind_l e' C Γ e t τ :
+ e = fill_ctx C e' →
+ ctx_refines Γ (fill_ctx C e') t τ →
+ ctx_refines Γ e t τ.
+Proof. intros; subst; assumption. Qed.
+
+Lemma tac_ctx_bind_r e' C Γ e t τ :
+ e = fill_ctx C e' →
+ ctx_refines Γ t (fill_ctx C e') τ →
+ ctx_refines Γ t e τ.
+Proof. intros; subst; assumption. Qed.
+
+Ltac reshape_expr_ctx e tac :=
+ let rec go K e :=
+ match e with
+ | _ => tac (reverse K) e
+ (* Base lambda calculus *)
+
+ | Rec ?f ?x ?e => add_item (CTX_Rec f x) K e
+ | App ?e1 ?e2 => add_item (CTX_AppL e2) K e1
+ | App ?e1 ?e2 => add_item (CTX_AppR e1) K e2
+ (* Base types and their operations *)
+ | UnOp ?op ?e => add_item (UnOpCtx op) K e
+ | BinOp ?op ?e1 ?e2 => add_item (CTX_BinOpL op e2) K e1
+ | BinOp ?op ?e1 ?e2 => add_item (CTX_BinOpR op e1) K e2
+ | If ?e0 ?e1 ?e2 => add_item (CTX_IfL e1 e2) K e0
+ | If ?e0 ?e1 ?e2 => add_item (CTX_IfM e0 e2) K e1
+ | If ?e0 ?e1 ?e2 => add_item (CTX_IfR e0 e1) K e2
+ (* Products *)
+ | Pair ?e1 ?e2 => add_item (CTX_PairL e2) K e1
+ | Pair ?e1 ?e2 => add_item (CTX_PairR e1) K e2
+ | Fst ?e => add_item CTX_Fst K e
+ | Snd ?e => add_item CTX_Snd K e
+ (* Sums *)
+ | InjL ?e => add_item CTX_InjL K e
+ | InjR ?e => add_item CTX_InjR K e
+ | Case ?e0 ?e1 ?e2 => add_item (CTX_CaseL e1 e2) K e0
+ | Case ?e0 ?e1 ?e2 => add_item (CTX_CaseM e0 e2) K e1
+ | Case ?e0 ?e1 ?e2 => add_item (CTX_CaseR e0 e1) K e2
+ (* Concurrency *)
+ | Fork ?e => add_item CTX_Fork K e
+ (* Heap *)
+ | Alloc ?e => add_item CTX_Alloc K e
+ | Load ?e => add_item CTX_Load K e
+ | Store ?e1 ?e2 => add_item (CTX_StoreR e1) K e2
+ | Store ?e1 ?e2 => add_item (CTX_StoreL e2) K e1
+ (* Compare-exchange *)
+ | CmpXchg ?e0 ?e1 ?e2 => add_item (CTX_CmpXchgL e1 e2) K e0
+ | CmpXchg ?e0 ?e1 ?e2 => add_item (CTX_CmpXchgM e0 e2) K e1
+ | CmpXchg ?e0 ?e1 ?e2 => add_item (CTX_CmpXchgR e0 e1) K e2
+ | FAA ?e0 ?e1 => add_item (CTX_FAAL e1) K e0
+ | FAA ?e0 ?e1 => add_item (CTX_FAAR e0) K e1
+ end
+ with add_item Ki K e := go (Ki :: K) e
+ in
+ go (@nil ctx_item) e.
+
+Ltac ctx_bind_helper :=
+ simpl;
+ lazymatch goal with
+ | |- fill_ctx ?K ?e = fill_ctx _ ?efoc =>
+ reshape_expr_ctx e ltac:(fun K' e' =>
+ unify e' efoc;
+ let K'' := eval cbn[app] in (K' ++ K) in
+ replace (fill_ctx K e) with (fill_ctx K'' e') by (by rewrite ?fill_ctx_app))
+ | |- ?e = fill_ctx _ ?efoc =>
+ reshape_expr_ctx e ltac:(fun K' e' =>
+ unify e' efoc;
+ replace e with (fill_ctx K' e') by (by rewrite ?fill_ctx_app))
+ end; reflexivity.
+
+Tactic Notation "ctx_bind_l" open_constr(efoc) :=
+ eapply (tac_ctx_bind_l efoc);
+ [ ctx_bind_helper
+ | (* new goal *)
+ ].
+
+Tactic Notation "ctx_bind_r" open_constr(efoc) :=
+ eapply (tac_ctx_bind_r efoc);
+ [ ctx_bind_helper
+ | (* new goal *)
+ ].
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 64f5f1a..c94c6d6 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -106,9 +106,12 @@ Inductive typed : stringmap type → expr → type → Prop :=
| Val_typed Γ v τ :
⊢ᵥ v : τ →
Γ ⊢ₜ Val v : τ
- | Unit_typed Γ : Γ ⊢ₜ #() : TUnit
- | Nat_typed Γ (n : nat) : Γ ⊢ₜ # n : TNat
- | Bool_typed Γ (b : bool) : Γ ⊢ₜ # b : TBool
+ | Unit_typed Γ :
+ Γ ⊢ₜ #() : TUnit
+ | Nat_typed Γ (n : nat) :
+ Γ ⊢ₜ #n : TNat
+ | Bool_typed Γ (b : bool) :
+ Γ ⊢ₜ #b : TBool
| BinOp_typed_nat Γ op e1 e2 τ :
Γ ⊢ₜ e1 : TNat → Γ ⊢ₜ e2 : TNat →
binop_nat_res_type op = Some τ →
@@ -120,39 +123,65 @@ Inductive typed : stringmap type → expr → type → Prop :=
| RefEq_typed Γ e1 e2 τ :
Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : Tref τ →
Γ ⊢ₜ BinOp EqOp e1 e2 : TBool
- | Pair_typed Γ e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 → Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2
- | Fst_typed Γ e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Fst e : τ1
- | Snd_typed Γ e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Snd e : τ2
- | InjL_typed Γ e τ1 τ2 : Γ ⊢ₜ e : τ1 → Γ ⊢ₜ InjL e : TSum τ1 τ2
- | InjR_typed Γ e τ1 τ2 : Γ ⊢ₜ e : τ2 → Γ ⊢ₜ InjR e : TSum τ1 τ2
+ | Pair_typed Γ e1 e2 τ1 τ2 :
+ Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 →
+ Γ ⊢ₜ (e1, e2) : τ1 * τ2
+ | Fst_typed Γ e τ1 τ2 :
+ Γ ⊢ₜ e : τ1 * τ2 →
+ Γ ⊢ₜ Fst e : τ1
+ | Snd_typed Γ e τ1 τ2 :
+ Γ ⊢ₜ e : τ1 * τ2 →
+ Γ ⊢ₜ Snd e : τ2
+ | InjL_typed Γ e τ1 τ2 :
+ Γ ⊢ₜ e : τ1 →
+ Γ ⊢ₜ InjL e : τ1 + τ2
+ | InjR_typed Γ e τ1 τ2 :
+ Γ ⊢ₜ e : τ2 →
+ Γ ⊢ₜ InjR e : τ1 + τ2
| Case_typed Γ e0 e1 e2 τ1 τ2 τ3 :
- Γ ⊢ₜ e0 : TSum τ1 τ2 →
- Γ ⊢ₜ e1 : TArrow τ1 τ3 →
- Γ ⊢ₜ e2 : TArrow τ2 τ3 →
+ Γ ⊢ₜ e0 : τ1 + τ2 →
+ Γ ⊢ₜ e1 : (τ1 → τ3) →
+ Γ ⊢ₜ e2 : (τ2 → τ3) →
Γ ⊢ₜ Case e0 e1 e2 : τ3
| If_typed Γ e0 e1 e2 τ :
- Γ ⊢ₜ e0 : TBool → Γ ⊢ₜ e1 : τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ If e0 e1 e2 : τ
+ Γ ⊢ₜ e0 : TBool →
+ Γ ⊢ₜ e1 : τ →
+ Γ ⊢ₜ e2 : τ →
+ Γ ⊢ₜ If e0 e1 e2 : τ
| Rec_typed Γ f x e τ1 τ2 :
- <[f:=TArrow τ1 τ2]>(<[x:=τ1]>Γ) ⊢ₜ e : τ2 →
- Γ ⊢ₜ Rec f x e : TArrow τ1 τ2
+ <[f:=(τ1 → τ2)%ty]>(<[x:=τ1]>Γ) ⊢ₜ e : τ2 →
+ Γ ⊢ₜ (rec: f x := e) : (τ1 → τ2)
| App_typed Γ e1 e2 τ1 τ2 :
- Γ ⊢ₜ e1 : TArrow τ1 τ2 → Γ ⊢ₜ e2 : τ1 → Γ ⊢ₜ App e1 e2 : τ2
+ Γ ⊢ₜ e1 : (τ1 → τ2) →
+ Γ ⊢ₜ e2 : τ1 →
+ Γ ⊢ₜ e1 e2 : τ2
| TLam_typed Γ e τ :
⤉ Γ ⊢ₜ e : τ →
- Γ ⊢ₜ (Λ: e) : TForall τ
- | TApp_typed Γ e τ τ' : Γ ⊢ₜ e : TForall τ →
+ Γ ⊢ₜ (Λ: e) : ∀: τ
+ | TApp_typed Γ e τ τ' :
+ Γ ⊢ₜ e : (∀: τ) →
Γ ⊢ₜ e #() : τ.[τ'/]
- | TFold Γ e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜe : TRec τ
- | TUnfold Γ e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ rec_unfold e : τ.[TRec τ/]
- | TPack Γ e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
+ | TFold Γ e τ :
+ Γ ⊢ₜ e : τ.[(μ: τ)%ty/] →
+ Γ ⊢ₜ e : (μ: τ)
+ | TUnfold Γ e τ :
+ Γ ⊢ₜ e : (μ: τ)%ty →
+ Γ ⊢ₜ rec_unfold e : τ.[(μ: τ)%ty/]
+ | TPack Γ e τ τ' :
+ Γ ⊢ₜ e : τ.[τ'/] →
+ Γ ⊢ₜ e : (∃: τ)
| TUnpack Γ e1 x e2 τ τ2 :
- Γ ⊢ₜ e1 : TExists τ →
+ Γ ⊢ₜ e1 : (∃: τ) →
<[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 τ
| TLoad Γ e τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ Load e : τ
| TStore Γ e e' τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ e' : τ → Γ ⊢ₜ Store e e' : TUnit
+ | TFAA Γ e1 e2 :
+ Γ ⊢ₜ e1 : Tref TNat →
+ Γ ⊢ₜ e2 : TNat →
+ Γ ⊢ₜ FAA e1 e2 : TNat
| TCmpXchg Γ e1 e2 e3 τ :
EqType τ → UnboxedType τ →
Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
--
GitLab