Proper handling of the unboxed types

Prior to this change there was a bit of a mess in handling of types on
which you can do `CAS` and which you can compare by equality.
This change adds typing rules that allow `CAS` on any unboxed types.

theories/logic/compatibility.v

@@ -124,5 +124,70 @@ Section compatibility.
     value_case.
   Qed.
 
+  Lemma refines_cmpxchg_ref A e1 e2 e3 e1' e2' e3' :
+    (REL e1 << e1' : lrel_ref (lrel_ref A)) -∗
+    (REL e2 << e2' : lrel_ref A) -∗
+    (REL e3 << e3' : lrel_ref A) -∗
+    REL (CmpXchg e1 e2 e3) << (CmpXchg e1' e2' e3') : lrel_prod (lrel_ref A) lrel_bool.
+  Proof.
+    iIntros "IH1 IH2 IH3".
+    rel_bind_l e3; rel_bind_r e3'.
+    iApply (refines_bind with "IH3").
+    iIntros (v3 v3') "#IH3".
+    rel_bind_l e2; rel_bind_r e2'.
+    iApply (refines_bind with "IH2").
+    iIntros (v2 v2') "#IH2".
+    rel_bind_l e1; rel_bind_r e1'.
+    iApply (refines_bind with "IH1").
+    iIntros (v1 v1') "#IH1 /=".
+    iPoseProof "IH1" as "IH1'".
+    iDestruct "IH1" as (l1 l2) "(% & % & Hinv)"; simplify_eq/=.
+    rewrite {2}/lrel_car /=.
+    iDestruct "IH2" as (r1 r2 -> ->) "Hr".
+    (* iDestruct "IH3" as (n1 n2 -> ->) "Hn". *)
+    rel_cmpxchg_l_atomic.
+    iInv (relocN .@ "ref" .@ (l1,l2)) as (v1 v2) "[Hl1 [>Hl2 #Hv]]" "Hclose".
+    iModIntro. iExists _; iFrame. simpl.
+    destruct (decide ((v1, v2) = (#r1, #r2))); simplify_eq/=.
+    - iSplitR; first by (iIntros (?); contradiction).
+      iIntros (?). iNext. iIntros "Hv1".
+      rel_cmpxchg_suc_r.
+      iMod ("Hclose" with "[-]").
+      { iNext. iExists _, _. by iFrame. }
+      rel_values. iExists _, _, _, _. do 2 (iSplitL; first done).
+      iFrame "Hv". iExists _. done.
+    - iSplit; iIntros (?); simplify_eq/=; iNext; iIntros "Hl1".
+      + destruct (decide (v2 = #r2)); simplify_eq/=.
+        * rewrite {5}/lrel_car. simpl.
+          iDestruct "Hv" as (r1' r2' ? ?) "#Hv". simplify_eq/=.
+          destruct (decide ((l1, l2) = (r1, r2'))); simplify_eq/=.
+          { iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
+            iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hl2") as %[]. }
+          destruct (decide ((l1, l2) = (r1', r2'))); simplify_eq/=.
+          ++ assert (r1' ≠ r1) by naive_solver.
+             iInv (relocN.@"ref".@(r1, r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
+             iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hl2") as %[].
+          ++ iInv (relocN.@"ref".@(r1, r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
+             iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(Hr1' & >Hr2' & Hrr')" "Hcl'".
+             iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hr2'") as %[].
+        * rel_cmpxchg_fail_r.
+          iMod ("Hclose" with "[-]").
+          { iNext; iExists _, _; by iFrame. }
+          rel_values. iModIntro. iExists _,_,_,_.
+          repeat iSplit; eauto.
+      + assert (v2 ≠ #r2) by naive_solver.
+        rewrite {5}/lrel_car. simpl.
+        iDestruct "Hv" as (r1' r2' ? ?) "#Hv". simplify_eq/=.
+        destruct (decide ((l1, l2) = (r1', r2'))); simplify_eq/=.
+        { iInv (relocN.@"ref".@(r1', r2)) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
+          iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hl1") as %[]. }
+        destruct (decide ((l1, l2) = (r1', r2))); simplify_eq/=.
+        { iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
+          iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hl1") as %[]. }
+        iInv (relocN.@"ref".@(r1', r2)) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
+        iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(>Hr1' & >Hr2' & Hrr')" "Hcl'".
+        iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hr1'") as %[].
+  Qed.
+
 End compatibility.
 

theories/typing/contextual_refinement.v

@@ -138,12 +138,14 @@ 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_BinOpL_UnboxedEq e2 Γ τ :
+     UnboxedType τ →
+     typed Γ e2 τ →
+     typed_ctx_item (CTX_BinOpL EqOp e2) Γ τ Γ TBool
+  | TP_CTX_BinOpR_UnboxedEq e1 Γ τ :
+     UnboxedType τ →
+     typed Γ e1 τ →
+     typed_ctx_item (CTX_BinOpR EqOp e1) Γ τ Γ TBool
   | TP_CTX_IfL Γ e1 e2 τ :
      typed Γ e1 τ → typed Γ e2 τ →
      typed_ctx_item (CTX_IfL e1 e2) Γ (TBool) Γ τ
@@ -198,15 +200,15 @@ Inductive typed_ctx_item :
      Γ ⊢ₜ e1 : TRef TNat →
      typed_ctx_item (CTX_FAAR e1) Γ TNat Γ TNat
   | TP_CTX_CasL Γ e1 e2 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      typed Γ e1 τ → typed Γ e2 τ →
      typed_ctx_item (CTX_CmpXchgL e1 e2) Γ (TRef τ) Γ (TProd τ TBool)
   | TP_CTX_CasM Γ e0 e2 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      typed Γ e0 (TRef τ) → typed Γ e2 τ →
      typed_ctx_item (CTX_CmpXchgM e0 e2) Γ τ Γ (TProd τ TBool)
   | TP_CTX_CasR Γ e0 e1 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      typed Γ e0 (TRef τ) → typed Γ e1 τ →
      typed_ctx_item (CTX_CmpXchgR e0 e1) Γ τ Γ (TProd τ TBool)
   (* Polymorphic & recursive types *)
@@ -238,7 +240,8 @@ Inductive typed_ctx: ctx → stringmap type → type → stringmap type → type
      typed_ctx K Γ1 τ1 Γ2 τ2 →
      typed_ctx (k :: K) Γ1 τ1 Γ3 τ3.
 
-(* Observable types are, at the moment, exactly the types which support equality. *)
+(* Observable types are, at the moment, exactly the unboxed types
+which support direct equality tests. *)
 Definition ObsType : type → Prop := λ τ, EqType τ ∧ UnboxedType τ.
 
 Definition ctx_refines (Γ : stringmap type)
@@ -504,9 +507,9 @@ Section bin_log_related_under_typed_ctx.
       + iApply bin_log_related_bool_binop;
           try (by iApply fundamental); eauto.
         by iApply (IHK with "Hrel").
-      + iApply bin_log_related_ref_binop; try (by iApply fundamental).
+      + iApply bin_log_related_unboxed_eq; try (eassumption || by iApply fundamental).
         by iApply (IHK with "Hrel").
-      + iApply bin_log_related_ref_binop; try (by iApply fundamental).
+      + iApply bin_log_related_unboxed_eq; try (eassumption || by iApply fundamental).
         by iApply (IHK with "Hrel").
       + iApply (bin_log_related_if with "[] []");
           try by iApply fundamental.

theories/typing/fundamental.v

@@ -288,7 +288,7 @@ Section fundamental.
     rel_values.
   Qed.
 
-  Lemma bin_log_related_CmpXchg Δ Γ e1 e2 e3 e1' e2' e3' τ
+  Lemma bin_log_related_CmpXchg_EqType Δ Γ e1 e2 e3 e1' e2' e3' τ
     (HEqτ : EqType τ)
     (HUbτ : UnboxedType τ) :
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
@@ -327,6 +327,24 @@ Section fundamental.
       iFrame "Hv". iExists _. done.
   Qed.
 
+  Lemma bin_log_related_CmpXchg Δ Γ e1 e2 e3 e1' e2' e3' τ
+    (HUbτ : UnboxedType τ) :
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
+    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
+    ({Δ;Γ} ⊨ e3 ≤log≤ e3' : τ) -∗
+    {Δ;Γ} ⊨ CmpXchg e1 e2 e3 ≤log≤ CmpXchg e1' e2' e3' : TProd τ TBool.
+  Proof.
+    cut (EqType τ ∨ ∃ τ', τ = TRef τ').
+    { intros [Hτ | [τ' ->]].
+      - by iApply bin_log_related_CmpXchg_EqType.
+      - iIntros "H1 H2 H3". intro_clause.
+        iSpecialize ("H1" with "Hvs").
+        iSpecialize ("H2" with "Hvs").
+        iSpecialize ("H3" with "Hvs").
+        iApply (refines_cmpxchg_ref with "H1 H2 H3"). }
+    by apply unboxed_type_ref_or_eqtype.
+  Qed.
+
   Lemma bin_log_related_alloc Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ) -∗
     {Δ;Γ} ⊨ Alloc e ≤log≤ Alloc e' : TRef τ.
@@ -342,31 +360,25 @@ Section fundamental.
     rel_values. iExists l, k. eauto.
   Qed.
 
-  Lemma bin_log_related_ref_binop Δ Γ e1 e2 e1' e2' τ :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
-    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : TRef τ) -∗
+  Lemma bin_log_related_unboxed_eq Δ Γ e1 e2 e1' e2' τ :
+    UnboxedType τ →
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : τ) -∗
+    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
     {Δ;Γ} ⊨ BinOp EqOp e1 e2 ≤log≤ BinOp EqOp e1' e2' : TBool.
   Proof.
-    iIntros "IH1 IH2".
+    iIntros (Hτ) "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 (l1 l2) "[% [% #Hl]]"; simplify_eq/=.
-    iDestruct "IH2" as (l1' l2') "[% [% #Hl']]"; simplify_eq/=.
+    iAssert (⌜val_is_unboxed v1⌝)%I as "%".
+    { rewrite !unboxed_type_sound //.
+      iDestruct "IH1" as "[$ _]". }
+    iAssert (⌜val_is_unboxed v2'⌝)%I as "%".
+    { rewrite !unboxed_type_sound //.
+      iDestruct "IH2" as "[_ $]". }
+    iMod (unboxed_type_eq with "IH1 IH2") as "%"; first done.
     rel_op_l. rel_op_r.
-    destruct (decide (l1 = l1')) as [->|?].
-    - iMod (interp_ref_funct _ _ l1' l2 l2' with "[Hl Hl']") as %->.
-      { solve_ndisj. }
-      { iSplit; iExists _,_; eauto. }
-      rewrite !bool_decide_true //.
-      value_case.
-    - destruct (decide (l2 = l2')) as [->|?].
-      + iMod (interp_ref_inj _ _ l2' l1 l1' with "[Hl Hl']") as %->.
-        { solve_ndisj. }
-        { iSplit; iExists _,_; eauto. }
-        congruence.
-      + rewrite !bool_decide_false //; try congruence.
-        value_case.
+    do 2 case_bool_decide; first [by rel_values | naive_solver].
   Qed.
 
   Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
@@ -531,7 +543,7 @@ Section fundamental.
         by iApply fundamental.
       + iApply bin_log_related_bool_unop; first done.
         by iApply fundamental.
-      + iApply bin_log_related_ref_binop;
+      + iApply bin_log_related_unboxed_eq; try done;
           by iApply fundamental.
       + iApply bin_log_related_pair;
           by iApply fundamental.

theories/typing/interp.v

@@ -74,6 +74,35 @@ Section semtypes.
       + iDestruct "H1" as "[% [% H1]]"; simplify_eq/=.
         rewrite IHHτ2. by iDestruct "H1" as "%"; subst.
   Qed.
+
+  Lemma unboxed_type_eq τ Δ v1 v2 w1 w2 :
+    UnboxedType τ →
+    interp τ Δ v1 v2 -∗
+    interp τ Δ w1 w2 -∗
+    |={⊤}=> ⌜v1 = w1 ↔ v2 = w2⌝.
+  Proof.
+    intros Hunboxed.
+    cut (EqType τ ∨ ∃ τ', τ = TRef τ').
+    { intros [Hτ | [τ' ->]].
+      - rewrite !eq_type_sound //.
+        iIntros "% %". iModIntro.
+        iPureIntro. naive_solver.
+      - rewrite /lrel_car /=.
+        iDestruct 1 as (l1 l2 -> ->) "Hl".
+        iDestruct 1 as (r1 r2 -> ->) "Hr".
+        destruct (decide (l1 = r1)); subst.
+        + destruct (decide (l2 = r2)); subst; first by eauto.
+          iInv (relocN.@"ref".@(r1, l2)) as (v1 v2) "(>Hr1 & >Hr2 & Hinv1)".
+          iInv (relocN.@"ref".@(r1, r2)) as (w1 w2) "(>Hr1' & >Hr2' & Hinv2)".
+          iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hr1'") as %[].
+        + destruct (decide (l2 = r2)); subst; last first.
+          { iModIntro. iPureIntro. naive_solver. }
+          iInv (relocN.@"ref".@(r1, r2)) as (v1 v2) "(>Hr1 & >Hr2 & Hinv1)".
+          iInv (relocN.@"ref".@(l1, r2)) as (w1 w2) "(>Hr1' & >Hr2' & Hinv2)".
+          iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hr2'") as %[]. }
+    by apply unboxed_type_ref_or_eqtype.
+  Qed.
+
 End semtypes.
 
 (** ** Properties of the type inrpretation w.r.t. the substitutions *)

theories/typing/soundness.v

@@ -8,7 +8,7 @@ Lemma logrel_adequate Σ `{relocPreG Σ}
    e e' τ (σ : state) :
   (∀ `{relocG Σ} Δ, ⊢ {⊤;Δ;∅} ⊨ e ≤log≤ e' : τ) →
   adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h)
-    ∧ (ObsType τ → v = v')).
+    ∧ (EqType τ → v = v')).
 Proof.
   intros Hlog.
   set (A := λ (HΣ : relocG Σ), interp τ []).
@@ -20,7 +20,6 @@ Proof.
     { iApply env_ltyped2_empty. }
     by rewrite !fmap_empty !subst_map_empty.
   - intros HΣ v v'. unfold A. iIntros "Hvv".
-    unfold ObsType. cbn.
     iIntros (Hτ). by iApply (eq_type_sound with "Hvv").
 Qed.
 
@@ -30,7 +29,7 @@ Theorem logrel_typesafety Σ `{relocPreG Σ} e e' τ thp σ σ' :
   not_stuck e' σ'.
 Proof.
   intros Hlog ??.
-  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))); first (intros [_ ?]; eauto).
+  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e], σ) (of_val v' :: thp', h) ∧ (EqType τ → v = v'))); first (intros [_ ?]; eauto).
   eapply logrel_adequate; eauto.
 Qed.
 
@@ -51,8 +50,8 @@ Lemma logrel_simul Σ `{relocPreG Σ}
   (∃ thp' hp' v', rtc erased_step ([e'], σ) (of_val v' :: thp', hp') ∧ (ObsType τ → v = v')).
 Proof.
   intros Hlog Hsteps.
-  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))).
-  { destruct 1; naive_solver. }
+  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h) ∧ (EqType τ → v = v'))).
+  { unfold ObsType. destruct 1; naive_solver. }
   eapply logrel_adequate; eauto.
 Qed.
 

theories/typing/types.v

@@ -18,7 +18,15 @@ Inductive type :=
   | TExists : {bind 1 of type} → type
   | TRef : type → type.
 
-(** Types which support direct equality test (which coincides with ctx equiv) *)
+(** 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
+  | UnboxedTBool : UnboxedType TBool
+  | UnboxedTRef τ : UnboxedType (TRef τ).
+
+(** Types which support direct equality test (which coincides with ctx equiv).
+    This is an auxiliary notion. *)
 Inductive EqType : type → Prop :=
   | EqTUnit : EqType TUnit
   | EqTNat : EqType TNat
@@ -26,12 +34,9 @@ Inductive EqType : type → Prop :=
   | EqTProd τ τ' : EqType τ → EqType τ' → EqType (TProd τ τ')
   | EqSum τ τ' : EqType τ → EqType τ' → EqType (TSum τ τ').
 
-(** 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
-  | UnboxedTBool : UnboxedType TBool
-  | UnboxedTRef τ : UnboxedType (TRef τ).
+Lemma unboxed_type_ref_or_eqtype τ :
+  UnboxedType τ → (EqType τ ∨ ∃ τ', τ = TRef τ').
+Proof. inversion 1; first [ left; by econstructor | right; naive_solver ]. Qed.
 
 (** Autosubst instances *)
 Instance Ids_type : Ids type. derive. Defined.
@@ -135,8 +140,9 @@ Inductive typed : stringmap type → expr → type → Prop :=
      Γ ⊢ₜ e : TBool →
      unop_bool_res_type op = Some τ →
      Γ ⊢ₜ UnOp op e : τ
-  | RefEq_typed Γ e1 e2 τ :
-     Γ ⊢ₜ e1 : ref τ → Γ ⊢ₜ e2 : ref τ →
+  | UnboxedEq_typed Γ e1 e2 τ :
+     UnboxedType τ →
+     Γ ⊢ₜ e1 : τ → Γ ⊢ₜ e2 : τ →
      Γ ⊢ₜ BinOp EqOp e1 e2 : TBool
   | Pair_typed Γ e1 e2 τ1 τ2 :
      Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 →
@@ -198,7 +204,7 @@ Inductive typed : stringmap type → expr → type → Prop :=
      Γ ⊢ₜ e2 : TNat →
      Γ ⊢ₜ FAA e1 e2 : TNat
   | TCmpXchg Γ e1 e2 e3 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      Γ ⊢ₜ e1 : ref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
      Γ ⊢ₜ CmpXchg e1 e2 e3 : τ * TBool
 with val_typed : val → type → Prop :=