typing for unary operations and pointer equality

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)

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.

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;

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.