Commit d698a0c4 authored by Dan Frumin's avatar Dan Frumin
Browse files

Add FAA to the type system

parent cc7a5daf
......@@ -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
......
......@@ -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.
......@@ -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.
......
......@@ -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.
......
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 *)
].
......@@ -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 : τ
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment