From c5a3ab55308b2dcd03cbd8fa6358ceae2df25bb4 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 19 Jun 2020 14:23:59 +0200
Subject: [PATCH] typing for unary operations and pointer equality
---
theories/logic/adequacy.v | 5 +---
theories/typing/contextual_refinement.v | 36 +++++++++++++++++++------
theories/typing/fundamental.v | 34 +++++++++++++++++++++++
theories/typing/types.v | 32 +++++++++++++++++++---
4 files changed, 92 insertions(+), 15 deletions(-)
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index e82a01f..1f5ffc3 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -15,13 +15,10 @@ Definition relocΣ : gFunctors := #[heapΣ; authΣ cfgUR].
Instance subG_relocPreG {Σ} : subG relocΣ Σ → relocPreG Σ.
Proof. solve_inG. Qed.
-Definition pure_lrel `{relocG Σ} (P : val → val → Prop) :=
- @LRel Σ (λ v v', ⌜P v v'âŒ)%I _.
-
Lemma refines_adequate Σ `{relocPreG Σ}
(A : ∀ `{relocG Σ}, lrel Σ)
(P : val → val → Prop) e e' σ :
- (∀ `{relocG Σ}, ∀ v v', A v v' -∗ pure_lrel P v v') →
+ (∀ `{relocG Σ}, ∀ v v', A v v' -∗ ⌜P v v'âŒ) →
(∀ `{relocG Σ}, ⊢ REL e << e' : A) →
adequate NotStuck e σ
(λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h)
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index d9cbde3..3b2d943 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -116,6 +116,12 @@ Inductive typed_ctx_item :
typed Γ e1 (TArrow τ τ') →
typed_ctx_item (CTX_AppR e1) Γ τ Γ τ'
(* Base types and operations *)
+ | TP_CTX_UnOp_Nat op Γ τ :
+ unop_nat_res_type op = Some τ →
+ typed_ctx_item (CTX_UnOp op) Γ TNat Γ τ
+ | TP_CTX_UnOp_Bool op Γ τ :
+ unop_bool_res_type op = Some τ →
+ typed_ctx_item (CTX_UnOp op) Γ TBool Γ τ
| TP_CTX_BinOpL_Nat op Γ e2 τ :
typed Γ e2 TNat →
binop_nat_res_type op = Some τ →
@@ -132,6 +138,12 @@ Inductive typed_ctx_item :
typed Γ e1 TBool →
binop_bool_res_type op = Some τ →
typed_ctx_item (CTX_BinOpR op e1) Γ TBool Γ τ
+ | TP_CTX_BinOpL_PtrEq e2 Γ τ :
+ typed Γ e2 (ref τ) →
+ typed_ctx_item (CTX_BinOpL EqOp e2) Γ (ref τ) Γ TBool
+ | TP_CTX_BinOpR_PtrEq e1 Γ τ :
+ typed Γ e1 (ref τ) →
+ typed_ctx_item (CTX_BinOpR EqOp e1) Γ (ref τ) Γ TBool
| TP_CTX_IfL Γ e1 e2 τ :
typed Γ e1 τ → typed Γ e2 τ →
typed_ctx_item (CTX_IfL e1 e2) Γ (TBool) Γ τ
@@ -324,18 +336,26 @@ 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 "[]");
+ + iApply bin_log_related_nat_unop; eauto.
+ by iApply (IHK with "Hrel").
+ + iApply bin_log_related_bool_unop; eauto.
+ by iApply (IHK with "Hrel").
+ + iApply bin_log_related_nat_binop;
try (by iApply fundamental); eauto.
- iApply (IHK with "[Hrel]"); auto.
- + iApply (bin_log_related_nat_binop with "[]");
+ by iApply (IHK with "Hrel").
+ + iApply bin_log_related_nat_binop;
try (by iApply fundamental); eauto.
- iApply (IHK with "[Hrel]"); auto.
- + iApply (bin_log_related_bool_binop with "[]");
+ by iApply (IHK with "Hrel"); auto.
+ + iApply bin_log_related_bool_binop;
try (by iApply fundamental); eauto.
- iApply (IHK with "[Hrel]"); auto.
- + iApply (bin_log_related_bool_binop with "[]");
+ by iApply (IHK with "Hrel").
+ + iApply bin_log_related_bool_binop;
try (by iApply fundamental); eauto.
- iApply (IHK with "[Hrel]"); auto.
+ by iApply (IHK with "Hrel").
+ + iApply bin_log_related_ref_binop; try (by iApply fundamental).
+ by iApply (IHK with "Hrel").
+ + iApply bin_log_related_ref_binop; try (by iApply fundamental).
+ by iApply (IHK with "Hrel").
+ iApply (bin_log_related_if with "[] []");
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 02ac493..96abf5b 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -407,6 +407,36 @@ Section fundamental.
destruct op; inversion Hopv'; simplify_eq/=; eauto.
Qed.
+ Lemma bin_log_related_nat_unop Δ Γ op e e' τ :
+ unop_nat_res_type op = Some τ →
+ ({Δ;Γ} ⊨ e ≤log≤ e' : TNat) -∗
+ {Δ;Γ} ⊨ UnOp op e ≤log≤ UnOp op e' : τ.
+ Proof.
+ iIntros (Hopτ) "IH".
+ intro_clause.
+ rel_bind_ap e e' "IH" v v' "IH".
+ iDestruct "IH" as (n) "[% %]"; simplify_eq/=.
+ destruct (unop_nat_typed_safe op n _ Hopτ) as [v' Hopv'].
+ rel_pure_l. rel_pure_r.
+ value_case.
+ destruct op; inversion Hopv'; simplify_eq/=; try case_match; eauto.
+ Qed.
+
+ Lemma bin_log_related_bool_unop Δ Γ op e e' τ :
+ unop_bool_res_type op = Some τ →
+ ({Δ;Γ} ⊨ e ≤log≤ e' : TBool) -∗
+ {Δ;Γ} ⊨ UnOp op e ≤log≤ UnOp op e' : τ.
+ Proof.
+ iIntros (Hopτ) "IH".
+ intro_clause.
+ rel_bind_ap e e' "IH" v v' "IH".
+ iDestruct "IH" as (n) "[% %]"; simplify_eq/=.
+ destruct (unop_bool_typed_safe op n _ Hopτ) as [v' Hopv'].
+ rel_pure_l. rel_pure_r.
+ value_case.
+ destruct op; inversion Hopv'; simplify_eq/=; try case_match; eauto.
+ Qed.
+
Lemma bin_log_related_unfold Δ Γ e e' τ :
({Δ;Γ} ⊨ e ≤log≤ e' : μ: τ) -∗
{Δ;Γ} ⊨ rec_unfold e ≤log≤ rec_unfold e' : τ.[(TRec τ)/].
@@ -497,6 +527,10 @@ Section fundamental.
by iApply fundamental.
+ iApply bin_log_related_bool_binop; first done;
by iApply fundamental.
+ + iApply bin_log_related_nat_unop; first done.
+ by iApply fundamental.
+ + iApply bin_log_related_bool_unop; first done.
+ by iApply fundamental.
+ iApply bin_log_related_ref_binop;
by iApply fundamental.
+ iApply bin_log_related_pair;
diff --git a/theories/typing/types.v b/theories/typing/types.v
index a21d619..c57ddca 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -26,7 +26,7 @@ Inductive EqType : type → Prop :=
| EqTProd τ τ' : EqType τ → EqType τ' → EqType (TProd τ τ')
| EqSum τ τ' : EqType τ → EqType τ' → EqType (TSum τ τ').
-(** Which types are unboxed *)
+(** Which types are unboxed -- we can only do CAS on locations which hold unboxed types *)
Inductive UnboxedType : type → Prop :=
| UnboxedTUnit : UnboxedType TUnit
| UnboxedTNat : UnboxedType TNat
@@ -39,17 +39,27 @@ Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
-Fixpoint binop_nat_res_type (op : bin_op) : option type :=
+Definition binop_nat_res_type (op : bin_op) : option type :=
match op with
| MultOp => Some TNat | PlusOp => Some TNat | MinusOp => Some TNat
| EqOp => Some TBool | LeOp => Some TBool | LtOp => Some TBool
| _ => None
end.
-Fixpoint binop_bool_res_type (op : bin_op) : option type :=
+Definition binop_bool_res_type (op : bin_op) : option type :=
match op with
| XorOp => Some TBool | EqOp => Some TBool
| _ => None
end.
+Definition unop_nat_res_type (op : un_op) : option type :=
+ match op with
+ | MinusUnOp => Some TNat
+ | _ => None
+ end.
+Definition unop_bool_res_type (op : un_op) : option type :=
+ match op with
+ | NegOp => Some TBool
+ | _ => None
+ end.
Delimit Scope FType_scope with ty.
Bind Scope FType_scope with type.
@@ -118,6 +128,14 @@ Inductive typed : stringmap type → expr → type → Prop :=
Γ ⊢ₜ e1 : TBool → Γ ⊢ₜ e2 : TBool →
binop_bool_res_type op = Some τ →
Γ ⊢ₜ BinOp op e1 e2 : τ
+ | UnOp_typed_nat Γ op e τ :
+ Γ ⊢ₜ e : TNat →
+ unop_nat_res_type op = Some τ →
+ Γ ⊢ₜ UnOp op e : τ
+ | UnOp_typed_bool Γ op e τ :
+ Γ ⊢ₜ e : TBool →
+ unop_bool_res_type op = Some τ →
+ Γ ⊢ₜ UnOp op e : τ
| RefEq_typed Γ e1 e2 τ :
Γ ⊢ₜ e1 : ref τ → Γ ⊢ₜ e2 : ref τ →
Γ ⊢ₜ BinOp EqOp e1 e2 : TBool
@@ -214,3 +232,11 @@ Proof. destruct op; simpl; eauto. discriminate. Qed.
Lemma binop_bool_typed_safe (op : bin_op) (b1 b2 : bool) Ï„ :
binop_bool_res_type op = Some τ → is_Some (bin_op_eval op #b1 #b2).
Proof. destruct op; naive_solver. Qed.
+
+Lemma unop_nat_typed_safe (op : un_op) (n : Z) Ï„ :
+ unop_nat_res_type op = Some τ → is_Some (un_op_eval op #n).
+Proof. destruct op; simpl; eauto. Qed.
+
+Lemma unop_bool_typed_safe (op : un_op) (b : bool) Ï„ :
+ unop_bool_res_type op = Some τ → is_Some (un_op_eval op #b).
+Proof. destruct op; naive_solver. Qed.
--
GitLab