Add pointer comparison to the language & typing system

theories/F_mu_ref_conc/lang.v

@@ -109,6 +109,7 @@ Module lang.
     | Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b))
     | Eq, LitV (Nat a), LitV (Nat b) => Some $ if eq_nat_dec a b then LitV (Bool true) else LitV (Bool false)
     | Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b))
+    | Eq, LitV (Loc l1), LitV (Loc l2) => Some $ if decide (l1 = l2) then LitV (Bool true) else LitV (Bool false)
     | Le, LitV (Nat a), LitV (Nat b) => Some $ if le_dec a b then LitV (Bool true) else LitV (Bool false)
     | Lt, LitV (Nat a), LitV (Nat b) => Some $ if lt_dec a b then LitV (Bool true) else LitV (Bool false)
     | Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b))
@@ -365,7 +366,7 @@ Module lang.
       to_val e0 = Some v0 →
       e' = App e2 e0 →
       head_step (Case (InjR e0) e1 e2) σ e' σ []
-  (* nat bin op *)
+  (* bin op *)
   | BinOpS op e1 e2 v1 v2 v σ :
       to_val e1 = Some v1 →
       to_val e2 = Some v2 →

theories/F_mu_ref_conc/rules.v

@@ -46,6 +46,18 @@ Section mapsto.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
+  Lemma mapsto_valid l q v : l ↦ᵢ{q} v -∗ ✓ q.
+  Proof.
+    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
+    by apply pure_mono=> /auth_own_valid /singleton_valid [??].
+  Qed.
+
+  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦ᵢ{q1} v1 -∗ l ↦ᵢ{q2} v2 -∗ ✓ (q1 + q2)%Qp.
+  Proof.
+    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
+    iApply (mapsto_valid l _ v2). by iFrame.
+  Qed.
+
   Lemma mapsto_half_combine l v1 v2 :
     l ↦ᵢ{1/2} v1 -∗ l ↦ᵢ{1/2} v2 -∗ ⌜v1 = v2⌝ ∗ l ↦ᵢ v1.
   Proof.
@@ -138,7 +150,7 @@ Section lang_rules.
     rewrite -(wp_lift_pure_det_head_step (Fork e) #() [e]) //=; eauto.
     - (* TODO typeclass inference fail *)
       erewrite <-(wp_value_fupd _ _ #()); eauto; last solve_to_val.
-      by rewrite -step_fupd_intro // right_id later_sep. 
+      by rewrite -step_fupd_intro // right_id later_sep.
     - intros; inv_head_step; eauto.
   Qed.
 
@@ -147,5 +159,5 @@ Section lang_rules.
   Lemma wp_bind {E e} K Φ :
     WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
   Proof. exact: wp_ectx_bind. Qed.
- 
+
 End lang_rules.

theories/F_mu_ref_conc/typing.v

@@ -55,6 +55,9 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
      Γ ⊢ₜ e1 : TBool → Γ ⊢ₜ e2 : TBool → 
      binop_bool_res_type op = Some τ →
      Γ ⊢ₜ BinOp op e1 e2 : τ
+  | RefEq_typed e1 e2 τ :
+     Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : Tref τ →
+     Γ ⊢ₜ BinOp Eq 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

theories/examples/stack/stack_rules.v

@@ -104,7 +104,7 @@ Section Rules_pre.
     iDestruct (own_valid with "Hown") as %Hvalid.
     destruct (h !! l) as [av|] eqn:Hhl.
     { iDestruct (big_sepM_lookup _ h l with "Hall") as "Hl'"; first done.
-      iDestruct (@mapsto_valid_2 loc val with "Hl Hl'") as %Hval.
+      iDestruct (mapsto_valid_2 with "Hl Hl'") as %Hval.
       cbv in Hval. exfalso; by apply Hval. }
     { iMod (own_update with "Hown") as "[Hown Hl']".
       eapply auth_update_alloc.

theories/logrel/fundamental_binary.v

@@ -49,10 +49,10 @@ Section masked.
     iDestruct "Hvv'" as %Hvv'.
     cbn-[env_subst].
     rewrite (env_subst_lookup (snd <$> vvs) x v'); last first.
-    { rewrite lookup_fmap. by rewrite Hvv'. } 
+    { rewrite lookup_fmap. by rewrite Hvv'. }
     rewrite (env_subst_lookup _ x v); last first.
-    { rewrite lookup_fmap. by rewrite Hvv'. } 
-    iModIntro. 
+    { rewrite lookup_fmap. by rewrite Hvv'. }
+    iModIntro.
     iApply wp_value. eauto.
   Qed.
 
@@ -81,7 +81,7 @@ Section masked.
     rel_bind_ap e2 e2' "IH2" v2 v2' "Hvv2".
     value_case.
     iExists _, _; eauto.
-    iSplit; simpl; eauto.  auto. 
+    iSplit; simpl; eauto. auto.
   Qed.
 
   Lemma bin_log_related_fst Δ Γ e e' τ1 τ2 :
@@ -305,6 +305,36 @@ Section masked.
     destruct op; simpl in Hopv'; simplify_eq/=; eauto.
   Qed.
 
+  Lemma bin_log_related_ref_binop Δ Γ e1 e2 e1' e2' τ :
+    ↑ logrelN ⊆ E →
+    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ -∗
+    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : Tref τ -∗
+    {E,E;Δ;Γ} ⊨ BinOp Eq e1 e2 ≤log≤ BinOp Eq e1' e2' : TBool.
+  Proof.
+    iIntros (?) "IH1 IH2".
+    rel_bind_ap e1 e1' "IH1" v1 v1' "#IH1".
+    rel_bind_ap e2 e2' "IH2" v2 v2' "#IH2".
+    iDestruct "IH1" as ([l1 l2]) "[% #Hl]"; simplify_eq/=.
+    iDestruct "IH2" as ([l1' l2']) "[% #Hl']"; simplify_eq/=.
+    rel_op_l.
+    rel_op_r.
+    destruct (decide (l1 = l1')) as [->|?].
+    - iApply fupd_logrel.
+      iMod (interp_ref_funct _ _ _ l1' l2 l2' with "[Hl Hl']") as %->.
+      { solve_ndisj. }
+      { iSplit; iExists (_,_); eauto. }
+      rewrite decide_left.
+      iModIntro.
+      value_case.
+    - destruct (decide (l2 = l2')) as [->|?].
+      + iApply fupd_logrel.
+        iMod (interp_ref_inj _ _ _ l2' l1 l1' with "[Hl Hl']") as %->.
+        { solve_ndisj. }
+        { iSplit; iExists (_,_); eauto. }
+        congruence.
+      + value_case.
+  Qed.
+
   Lemma bin_log_related_tlam Δ Γ e e' τ :
     Closed (dom _ Γ) e →
     Closed (dom _ Γ) e' →
@@ -582,6 +612,7 @@ Section masked.
     - by iApply bin_log_related_bool.
     - by iApply (bin_log_related_nat_binop with "[]").
     - by iApply (bin_log_related_bool_binop with "[]").
+    - by iApply bin_log_related_ref_binop.
     - by iApply (bin_log_related_pair with "[]").
     - by iApply bin_log_related_fst.
     - by iApply bin_log_related_snd.

theories/logrel/semtypes.v

 From iris.proofmode Require Import tactics.
-From iris_logrel.F_mu_ref_conc Require Export typing context_refinement.
+From iris_logrel.F_mu_ref_conc Require Import rules context_refinement.
+From iris_logrel.F_mu_ref_conc Require Export typing.
 From iris_logrel.logrel Require Export rules_threadpool.
 Import uPred.
 
@@ -56,22 +57,22 @@ Section semtypes.
       (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
     (∃ vv1 vv2, ⌜ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2))⌝ ∧
                 interp1 Δ vv1 ∧ interp2 Δ vv2)%I.
-  Solve Obligations with solve_proper. 
+  Solve Obligations with solve_proper.
 
   Program Definition interp_sum
       (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
     ((∃ vv, ⌜ww = (InjLV (vv.1), InjLV (vv.2))⌝ ∧ interp1 Δ vv) ∨
      (∃ vv, ⌜ww = (InjRV (vv.1), InjRV (vv.2))⌝ ∧ interp2 Δ vv))%I.
-  Solve Obligations with solve_proper. 
+  Solve Obligations with solve_proper.
 
   Program Definition interp_arrow (E1 E2 : coPset)
           (interp1 interp2 : listC D -n> D) : listC D -n> D :=
     λne Δ ww,
     (□ ∀ vv, interp1 Δ vv →
-             interp_expr E1 E2 
+             interp_expr E1 E2
                interp2 Δ (App (of_val (ww.1)) (of_val (vv.1)),
                           App (of_val (ww.2)) (of_val (vv.2))))%I.
-  Solve Obligations with solve_proper. 
+  Solve Obligations with solve_proper.
 
   Program Definition interp_forall (E1 E2 : coPset)
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
@@ -83,7 +84,7 @@ Section semtypes.
 
   Program Definition interp_exists
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
-    (∃ vv, ⌜ww = (PackV (vv.1), PackV (vv.2))⌝ 
+    (∃ vv, ⌜ww = (PackV (vv.1), PackV (vv.2))⌝
      ∧ ∃ τi : D, ⌜∀ ww, PersistentP (τi ww)⌝ ∧ interp (τi :: Δ) vv)%I.
   Solve Obligations with solve_proper.
 
@@ -114,11 +115,11 @@ Section semtypes.
 
   Program Definition interp_singleton (v v' : val) : listC D -n> D :=
     λne Δ ww, ⌜ww = (v,v')⌝%I.
-  Solve Obligations with solve_proper.       
+  Solve Obligations with solve_proper.
 
   Program Definition interp_iref
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
-    (∃ (ll : loc * loc), 
+    (∃ (ll : loc * loc),
        interp_ref (interp_singleton (LitV (Loc (ll.1))) (LitV (Loc (ll.2)))) Δ ww ∧
        inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
   Solve Obligations with solve_proper.
@@ -163,7 +164,7 @@ Section semtypes.
     - intros ww; simpl; properness; auto.
       rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
-      rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia. 
+      rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia.
     - unfold interp_expr.
       intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
     - intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
@@ -187,7 +188,7 @@ Section semtypes.
       rewrite !lookup_app_r; [|lia ..].
       destruct (x - length Δ1) as [|n] eqn:?; simpl.
       { symmetry. rewrite always_always. asimpl. apply (interp_weaken [] Δ1 Δ2 _ _ τ'). }
-      rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia. 
+      rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia.
     - unfold interp_expr.
       intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
     - intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
@@ -274,6 +275,40 @@ Section semtypes.
        inversion 1. by rewrite IH2.
   Qed.
 
+  (* The reference type relation is functional and injective.
+     Thanks to Amin. *)
+  Lemma interp_ref_funct E Δ τ (l l1 l2 : loc) :
+    ↑logN ⊆ E →
+    ⟦ Tref τ ⟧ Δ (#l, #l1) ∗ ⟦ Tref τ ⟧ Δ (#l, #l2)
+    ={E}=∗ ⌜l1 = l2⌝.
+  Proof.
+    iIntros (?) "[Hl1 Hl2] /=".
+    iDestruct "Hl1" as ([l' l1']) "[% #Hl1]". simplify_eq.
+    iDestruct "Hl2" as ([l l2']) "[% #Hl2]". simplify_eq.
+    destruct (decide (l1' = l2')) as [->|?]; eauto.
+    iInv (logN.@(l, l1')) as ([? ?]) "[>Hl ?]" "Hcl".
+    iInv (logN.@(l, l2')) as ([? ?]) "[>Hl' ?]" "Hcl'".
+    simpl. iExFalso.
+    iDestruct (rules.mapsto_valid_2 with "Hl Hl'") as %Hfoo.
+    compute in Hfoo. eauto.
+  Qed.
+
+  Lemma interp_ref_inj E Δ τ (l l1 l2 : loc) :
+    ↑logN ⊆ E →
+    ⟦ Tref τ ⟧ Δ (#l1, #l) ∗ ⟦ Tref τ ⟧ Δ (#l2, #l)
+    ={E}=∗ ⌜l1 = l2⌝.
+  Proof.
+    iIntros (?) "[Hl1 Hl2] /=".
+    iDestruct "Hl1" as ([l1' l']) "[% #Hl1]". simplify_eq.
+    iDestruct "Hl2" as ([l2' l]) "[% #Hl2]". simplify_eq.
+    destruct (decide (l1' = l2')) as [->|?]; eauto.
+    iInv (logN.@(l1', l)) as ([? ?]) "(? & >Hl & ?)" "Hcl".
+    iInv (logN.@(l2', l)) as ([? ?]) "(? & >Hl' & ?)" "Hcl'".
+    simpl. iExFalso.
+    iDestruct (mapsto_valid_2 with "Hl Hl'") as %Hfoo.
+    compute in Hfoo. eauto.
+  Qed.
+
   Lemma interp_ret E τ Δ e1 e2 v1 v2 :
     to_val e1 = Some v1 →
     to_val e2 = Some v2 →

theories/logrel/threadpool.v

 (* The threadpool RA *)
-From iris.algebra Require Import auth gmap agree list.
+From iris.algebra Require Import auth gmap agree list frac.
 From iris.base_logic Require Export gen_heap invariants fractional.
 From iris.proofmode Require Import tactics.
 From iris_logrel.F_mu_ref_conc Require Import lang.
@@ -142,6 +142,20 @@ Section mapsto.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
+  Lemma mapsto_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
+  Proof.
+    rewrite heapS_mapsto_eq /heapS_mapsto_def own_valid !uPred.discrete_valid.
+    apply pure_mono=> /auth_own_valid /= [_ Hfoo].
+    revert Hfoo. simpl. rewrite singleton_valid.
+    by intros [? _].
+  Qed.
+
+  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ✓ (q1 + q2)%Qp.
+  Proof.
+    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
+    iApply (mapsto_valid l _ v2). by iFrame.
+  Qed.
+
   Lemma mapsto_half_combine l v1 v2 :
     l ↦ₛ{1/2} v1 -∗ l ↦ₛ{1/2} v2 -∗ ⌜v1 = v2⌝ ∗ l ↦ₛ v1.
   Proof.