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

Merge commit 'f4619355'

parents 8786f3ef f4619355
......@@ -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
......
......@@ -288,4 +288,75 @@ Section rules.
End rules.
(* TODO: write out the contextual refinements *)
(** Separately, we prove that the ordering induced by ⊕ conincides with
contextual refinement. *)
Lemma Seq_typed Γ e1 e2 τ :
Γ e1 : TUnit
Γ e2 : τ
Γ (e1;;e2) : τ.
Proof. by repeat (econstructor; eauto). Qed.
Lemma or_equiv_refines_1 e t :
( e : TUnit)
( t : TUnit)
( e ctx t : TUnit)
( (e t) =ctx= t : TUnit).
Proof.
intros Te Tt Het. split; last first.
- eapply (ctx_refines_transitive _ _ _ (t e)%V).
+ eapply (refines_sound relocΣ).
iIntros (? Δ).
iApply (or_choice_1_r t t with "[]").
by iApply refines_typed.
+ eapply (refines_sound relocΣ).
iIntros (? Δ). rel_pures_r.
iApply or_comm; by iApply (refines_typed TUnit []).
- eapply (ctx_refines_transitive _ _ _ (t t)%E).
+ ctx_bind_l e.
ctx_bind_r t.
eapply (ctx_refines_congruence _ _ TUnit);
last eassumption.
{ cbn.
econstructor; cbn; eauto.
- econstructor; cbn; eauto.
econstructor; cbn; eauto.
- econstructor; cbn; eauto.
+ econstructor; cbn; eauto.
econstructor; cbn; eauto.
econstructor; cbn; eauto.
change Z0 with (Z.of_nat 0%nat).
econstructor; cbn; eauto.
econstructor; cbn; eauto.
* econstructor; cbn; eauto.
eapply Seq_typed.
** change 1%Z with (Z.of_nat 1%nat).
repeat (econstructor; cbn; eauto).
** repeat (econstructor; cbn; eauto).
* repeat (econstructor; cbn; eauto).
+ econstructor; cbn; eauto.
2:{ econstructor; cbn; eauto. }
enough (typed_ctx_item (CTX_Rec <> <>)
(binder_insert BAnon (TUnit TUnit)%ty
(binder_insert BAnon TUnit ( : stringmap type)))
TUnit (TUnit TUnit)).
{ by simpl in *. }
eapply (TP_CTX_Rec TUnit TUnit BAnon BAnon). }
+ eapply (refines_sound relocΣ).
iIntros (? Δ). rel_pures_l.
iApply or_idemp_l. by iApply (refines_typed TUnit []).
Qed.
Lemma or_equiv_refines_2 e t :
( e : TUnit)
( t : TUnit)
( (e t) =ctx= t : TUnit)
( e ctx t : TUnit).
Proof.
intros Te Tt [Het1 Het2].
eapply (ctx_refines_transitive _ _ _ (e t)%E); last assumption.
eapply (refines_sound relocΣ).
iIntros (? Δ).
rel_pures_r. iApply or_choice_1_r.
by iApply (refines_typed TUnit []).
Qed.
......@@ -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.
......@@ -6,14 +6,14 @@ From iris.proofmode Require Import tactics.
From reloc.typing Require Export types interp fundamental.
Inductive ctx_item :=
(* λ-rec *)
| CTX_Rec (f x: binder)
(* Base lambda calculus *)
| CTX_Rec (f x : binder)
| CTX_AppL (e2 : expr)
| CTX_AppR (e1 : expr)
(* Bin op *)
(* Base types and their operations *)
| CTX_UnOp (op : un_op)
| CTX_BinOpL (op : bin_op) (e2 : expr)
| CTX_BinOpR (op : bin_op) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
| CTX_IfR (e0 : expr) (e1 : expr)
......@@ -28,6 +28,19 @@ Inductive ctx_item :=
| CTX_CaseL (e1 : expr) (e2 : expr)
| CTX_CaseM (e0 : expr) (e2 : expr)
| CTX_CaseR (e0 : expr) (e1 : expr)
(* Concurrency *)
| CTX_Fork
(* Heap *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr)
(* Compare-exchange and FAA *)
| CTX_CmpXchgL (e1 : expr) (e2 : expr)
| CTX_CmpXchgM (e0 : expr) (e2 : expr)
| CTX_CmpXchgR (e0 : expr) (e1 : expr)
| CTX_FAAL (e1 : expr)
| CTX_FAAR (e0 : expr)
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
......@@ -35,55 +48,54 @@ Inductive ctx_item :=
| CTX_TLam
| CTX_TApp
(* Existential types *)
(* | CTX_Pack *)
(* | CTX_UnpackL (e' : expr) *)
(* | CTX_UnpackR (e : expr) *)
(* Concurrency *)
| CTX_Fork
(* Reference Types *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr)
(* Compare-exchange used for fine-grained concurrency *)
| CTX_CmpXchg_L (e1 : expr) (e2 : expr)
| CTX_CmpXchg_M (e0 : expr) (e2 : expr)
| CTX_CmpXchg_R (e0 : expr) (e1 : expr).
(* Nb: we do not have an explicit PACK operation *)
| CTX_UnpackL (x : binder) (e2 : expr)
| CTX_UnpackR (x : binder) (e1 : expr)
.
Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
match ctx with
(* Base lambda calculus *)
| CTX_Rec f x => Rec f x e
| CTX_AppL e2 => App e e2
| CTX_AppR e1 => App e1 e
(* Base types and operations *)
| CTX_UnOp op => UnOp op e
| CTX_BinOpL op e2 => BinOp op e e2
| CTX_BinOpR op e1 => BinOp op e1 e
| CTX_IfL e1 e2 => If e e1 e2
| CTX_IfM e0 e2 => If e0 e e2
| CTX_IfR e0 e1 => If e0 e1 e
(* Products *)
| CTX_PairL e2 => Pair e e2
| CTX_PairR e1 => Pair e1 e
| CTX_Fst => Fst e
| CTX_Snd => Snd e
(* Sums *)
| CTX_InjL => InjL e
| CTX_InjR => InjR e
| CTX_CaseL e1 e2 => Case e e1 e2
| CTX_CaseM e0 e2 => Case e0 e e2
| CTX_CaseR e0 e1 => Case e0 e1 e
| CTX_BinOpL op e2 => BinOp op e e2
| CTX_BinOpR op e1 => BinOp op e1 e
| CTX_IfL e1 e2 => If e e1 e2
| CTX_IfM e0 e2 => If e0 e e2
| CTX_IfR e0 e1 => If e0 e1 e
| CTX_Fold => e
| CTX_Unfold => rec_unfold e
| CTX_TLam => Λ: e
| CTX_TApp => TApp e
(* | CTX_Pack => Pack e *)
(* | CTX_UnpackL e1 => Unpack e e1 *)
(* | CTX_UnpackR e0 => Unpack e0 e *)
(* Concurrency *)
| CTX_Fork => Fork e
(* Heap & atomic CAS/FAA *)
| CTX_Alloc => Alloc e
| CTX_Load => Load e
| CTX_StoreL e2 => Store e e2
| CTX_StoreR e1 => Store e1 e
| CTX_CmpXchg_L e1 e2 => CmpXchg e e1 e2
| CTX_CmpXchg_M e0 e2 => CmpXchg e0 e e2
| CTX_CmpXchg_R e0 e1 => CmpXchg e0 e1 e
| 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 => FAA e e1
| CTX_FAAR e0 => FAA e0 e
(* Recursive & polymorphic types *)
| CTX_Fold => e
| CTX_Unfold => rec_unfold e
| CTX_TLam => Λ: e
| CTX_TApp => TApp e
| CTX_UnpackL x e1 => unpack: x:=e in e1
| CTX_UnpackR x e0 => unpack: x:=e0 in e
end.
Definition ctx := list ctx_item.
......@@ -94,6 +106,7 @@ Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
(** typed ctx *)
Inductive typed_ctx_item :
ctx_item stringmap type type stringmap type type Prop :=
(* Base lambda calculus *)
| TP_CTX_Rec Γ τ τ' f x :
typed_ctx_item (CTX_Rec f x) (<[f:=TArrow τ τ']>(<[x:=τ]>Γ)) τ' Γ (TArrow τ τ')
| TP_CTX_AppL Γ e2 τ τ' :
......@@ -102,6 +115,33 @@ Inductive typed_ctx_item :
| TP_CTX_AppR Γ e1 τ τ' :
typed Γ e1 (TArrow τ τ')
typed_ctx_item (CTX_AppR e1) Γ τ Γ τ'
(* Base types and operations *)
| TP_CTX_BinOpL_Nat op Γ e2 τ :
typed Γ e2 TNat
binop_nat_res_type op = Some τ
typed_ctx_item (CTX_BinOpL op e2) Γ TNat Γ τ
| TP_CTX_BinOpR_Nat op e1 Γ τ :
typed Γ e1 TNat
binop_nat_res_type op = Some τ
typed_ctx_item (CTX_BinOpR op e1) Γ TNat Γ τ
| TP_CTX_BinOpL_Bool op Γ e2 τ :
typed Γ e2 TBool
binop_bool_res_type op = Some τ
typed_ctx_item (CTX_BinOpL op e2) Γ TBool Γ τ
| TP_CTX_BinOpR_Bool op e1 Γ τ :
typed Γ e1 TBool
binop_bool_res_type op = Some τ
typed_ctx_item (CTX_BinOpR op e1) Γ TBool Γ τ
| TP_CTX_IfL Γ e1 e2 τ :
typed Γ e1 τ typed Γ e2 τ
typed_ctx_item (CTX_IfL e1 e2) Γ (TBool) Γ τ
| TP_CTX_IfM Γ e0 e2 τ :
typed Γ e0 (TBool) typed Γ e2 τ
typed_ctx_item (CTX_IfM e0 e2) Γ τ Γ τ
| TP_CTX_IfR Γ e0 e1 τ :
typed Γ e0 (TBool) typed Γ e1 τ
typed_ctx_item (CTX_IfR e0 e1) Γ τ Γ τ
(* Products *)
| TP_CTX_PairL Γ e2 τ τ' :
typed Γ e2 τ'
typed_ctx_item (CTX_PairL e2) Γ τ Γ (TProd τ τ')
......@@ -112,6 +152,7 @@ Inductive typed_ctx_item :
typed_ctx_item CTX_Fst Γ (TProd τ τ') Γ τ
| TP_CTX_Snd Γ τ τ' :
typed_ctx_item CTX_Snd Γ (TProd τ τ') Γ τ'
(* Sums *)
| TP_CTX_InjL Γ τ τ' :
typed_ctx_item CTX_InjL Γ τ Γ (TSum τ τ')
| TP_CTX_InjR Γ τ τ' :
......@@ -125,49 +166,10 @@ Inductive typed_ctx_item :
| TP_CTX_CaseR Γ e0 e1 τ1 τ2 τ' :
typed Γ e0 (TSum τ1 τ2) typed Γ e1 (TArrow τ1 τ')
typed_ctx_item (CTX_CaseR e0 e1) Γ (TArrow τ2 τ') Γ τ'
| TP_CTX_IfL Γ e1 e2 τ :
typed Γ e1 τ typed Γ e2 τ
typed_ctx_item (CTX_IfL e1 e2) Γ (TBool) Γ τ
| TP_CTX_IfM Γ e0 e2 τ :
typed Γ e0 (TBool) typed Γ e2 τ
typed_ctx_item (CTX_IfM e0 e2) Γ τ Γ τ
| TP_CTX_IfR Γ e0 e1 τ :
typed Γ e0 (TBool) typed Γ e1 τ
typed_ctx_item (CTX_IfR e0 e1) Γ τ Γ τ
| TP_CTX_BinOpL_Nat op Γ e2 τ :
typed Γ e2 TNat
binop_nat_res_type op = Some τ
typed_ctx_item (CTX_BinOpL op e2) Γ TNat Γ τ
| TP_CTX_BinOpR_Nat op e1 Γ τ :
typed Γ e1 TNat
binop_nat_res_type op = Some τ
typed_ctx_item (CTX_BinOpR op e1) Γ TNat Γ τ
| TP_CTX_BinOpL_Bool op Γ e2 τ :
typed Γ e2 TBool
binop_bool_res_type op = Some τ
typed_ctx_item (CTX_BinOpL op e2) Γ TBool Γ τ
| TP_CTX_BinOpR_Bool op e1 Γ τ :
typed Γ e1 TBool
binop_bool_res_type op = Some τ
typed_ctx_item (CTX_BinOpR op e1) Γ TBool Γ τ
| TP_CTX_Fold Γ τ :
typed_ctx_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
| TP_CTX_Unfold Γ τ :
typed_ctx_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
| TP_CTX_TLam Γ τ :
typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Γ) τ Γ (TForall τ)
| TP_CTX_TApp Γ τ τ' :
typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
(* | TP_CTX_Pack Γ τ τ' : *)
(* typed_ctx_item CTX_Pack Γ τ.[τ'/] Γ (TExists τ) *)
(* | TP_CTX_UnpackL e2 Γ τ τ2 : *)
(* typed (subst (ren (+1)) <$> Γ) e2 (TArrow τ (subst (ren (+1)) τ2)) → *)
(* typed_ctx_item (CTX_UnpackL e2) Γ (TExists τ) Γ τ2 *)
(* | TP_CTX_UnpackR e1 Γ τ τ2 : *)
(* typed Γ e1 (TExists τ) → *)
(* typed_ctx_item (CTX_UnpackR e1) (subst (ren (+1)) <$> Γ) (TArrow τ (subst (ren (+1)) τ2)) Γ τ2 *)
(* Concurrency *)
| TP_CTX_Fork Γ :
typed_ctx_item CTX_Fork Γ TUnit Γ TUnit
(* Heap *)
| TPCTX_Alloc Γ τ :
typed_ctx_item CTX_Alloc Γ τ Γ (Tref τ)
| TP_CTX_Load Γ τ :
......@@ -177,18 +179,44 @@ 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_CmpXchg_L e1 e2) Γ (Tref τ) Γ (TProd τ TBool)
typed_ctx_item (CTX_CmpXchgL e1 e2) Γ (Tref τ) Γ (TProd τ TBool)
| TP_CTX_CasM Γ e0 e2 τ :
EqType τ UnboxedType τ
typed Γ e0 (Tref τ) typed Γ e2 τ
typed_ctx_item (CTX_CmpXchg_M e0 e2) Γ τ Γ (TProd τ TBool)
typed_ctx_item (CTX_CmpXchgM e0 e2) Γ τ Γ (TProd τ TBool)
| TP_CTX_CasR Γ e0 e1 τ :
EqType τ UnboxedType τ
typed Γ e0 (Tref τ) typed Γ e1 τ
typed_ctx_item (CTX_CmpXchg_R e0 e1) Γ τ Γ (TProd τ TBool).
typed_ctx_item (CTX_CmpXchgR e0 e1) Γ τ Γ (TProd τ TBool)
(* Polymorphic & recursive types *)
| TP_CTX_Fold Γ τ :
typed_ctx_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
| TP_CTX_Unfold Γ τ :
typed_ctx_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
| TP_CTX_TLam Γ τ :
typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Γ) τ Γ (TForall τ)
| TP_CTX_TApp Γ τ τ' :
typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
(* | TP_CTX_Pack Γ τ τ' : *)
(* typed_ctx_item CTX_Pack Γ τ.[τ'/] Γ (TExists τ) *)
| TP_CTX_UnpackL x e2 Γ τ τ2 :
<[x:=τ]>( Γ) e2 : (Autosubst_Classes.subst (ren (+1%nat)) τ2)
typed_ctx_item (CTX_UnpackL x e2) Γ (TExists τ) Γ τ2
| TP_CTX_UnpackR x e1 Γ τ τ2 :
Γ e1 : TExists τ
typed_ctx_item (CTX_UnpackR x e1)
(<[x:=τ]>( Γ)) (Autosubst_Classes.subst (ren (+1%nat)) τ2)
Γ τ2
.
Inductive typed_ctx: ctx stringmap type type stringmap type type Prop :=
| TPCTX_nil Γ τ :
......@@ -263,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 Σ}.
......@@ -288,6 +324,27 @@ Section bin_log_related_under_typed_ctx.
+ iApply (bin_log_related_app _ _ _ _ _ _ τ2 with "[]").
by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_bool_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_bool_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_pair with "[]").
iApply (IHK with "[Hrel]"); auto.
by iApply fundamental.
......@@ -314,42 +371,6 @@ Section bin_log_related_under_typed_ctx.
by iApply fundamental.
by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_bool_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_bool_binop with "[]");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_fold with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_unfold with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tlam with "[]").
iIntros (τi). iAlways.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tapp' with "[]").
iApply (IHK with "[Hrel]"); auto.
(* + iApply bin_log_related_pack'. *)
(* iApply (IHK with "[Hrel]"); auto. *)
(* + iApply bin_log_related_unpack; try by (iIntros; fundamental). *)
(* iApply (IHK with "[Hrel]"); auto. *)
(* + iApply bin_log_related_unpack; try by (iIntros; fundamental). *)
(* iIntros. iApply (IHK with "[Hrel]"); auto. *)
+ iApply (bin_log_related_fork with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_alloc with "[]").
......@@ -362,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.
......@@ -371,5 +398,20 @@ Section bin_log_related_under_typed_ctx.
+ iApply (bin_log_related_CmpXchg with "[] []");
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_fold with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_unfold with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tlam with "[]").
iIntros (τi). iAlways.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tapp' with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_unpack.
* iApply (IHK with "[Hrel]"); auto.
* iIntros (A). by iApply fundamental.
+ iApply bin_log_related_unpack.
* by iApply fundamental.
* iIntros (A). iApply (IHK with "[Hrel]"); auto.
Qed.
End bin_log_related_under_typed_ctx.
......@@ -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