Add ptr arithmetic and comparison

theories/c_translation/derived.v

@@ -105,6 +105,30 @@ Section derived.
     iSpecialize ("HΨ" with "HR").
     iApply (awp_wand with "HΨ"). eauto with iFrame.
   Qed.
+
+  Lemma a_ptr_add_ret R Φ Ψ2 e1 e2 :
+    AWP e2 @ R {{ Ψ2 }} -∗
+    AWP e1 @ R {{ v1, ▷ ∀ v2, Ψ2 v2 -∗ ∃ cl (n : nat),
+                         ⌜ v1 = cloc_to_val cl ⌝ ∗
+                         ⌜ v2 = #n ⌝ ∗
+                         Φ (cloc_to_val (cl.1, cl.2+n)%nat) }} -∗
+    AWP a_ptr_add e1 e2 @ R {{ Φ }}.
+  Proof.
+    iIntros "He2 HΦ". rewrite /a_ptr_add.
+    awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1". awp_lam.
+    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
+    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
+    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
+    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ".
+    destruct cl as [l o]. simpl.
+    iApply awp_bind. iApply (a_bin_op_spec _ _ (λ v, ⌜v = #o⌝)%I (λ v, ⌜v = #n⌝)%I); repeat awp_proj;
+    try by (iApply awp_ret; wp_value_head).
+    iNext. iIntros (? ? -> ->). iExists #(o+n); iSplit; eauto.
+    awp_let. repeat awp_proj. iApply awp_ret; wp_value_head.
+    rewrite -Nat2Z.inj_add.
+    iApply "HΦ".
+  Qed.
+
 End derived.
 
 Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.

theories/c_translation/translation.v

@@ -102,6 +102,22 @@ Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
 Definition a_invoke: val := λ: "f" "arg",
   a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
 
+Definition a_ptr_add : val := λ: "x" "y",
+  "lo" ←ᶜ ("x" |||ᶜ "y");;ᶜ
+  "o'" ←ᶜ ((a_ret (Snd (Fst "lo")) +ᶜ (a_ret (Snd "lo")))) ;;ᶜ
+  a_ret (Fst (Fst "lo"), "o'").
+
+Definition a_ptr_lt : val := λ: "x" "y",
+  "pq" ←ᶜ ("x" |||ᶜ "y");;ᶜ
+  let: "p" := Fst "pq" in
+  let: "q" := Snd "pq" in
+  ifᶜ ((a_ret (Fst "p")) ==ᶜ (a_ret (Fst "q")))
+  { (a_ret (Snd "p")) <ᶜ (a_ret (Snd "q")) }
+  elseᶜ { ♯false }.
+
+Notation "e1 +∗ᶜ e2" := (a_ptr_add e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 <∗ᶜ e2" := (a_ptr_lt e1%E e2%E)  (at level 80) : expr_scope.
+
 Section proofs.
   Context `{amonadG Σ}.
 
@@ -416,6 +432,68 @@ Section proofs.
     iRight. iSplit; eauto. by awp_seq.
   Qed.
 
+
+  Lemma a_ptr_add_spec R Φ Ψ2 e1 e2 :
+    AWP e2 @ R {{ Ψ2 }} -∗
+    AWP e1 @ R {{ v1, ▷ ∀ v2, Ψ2 v2 -∗ ∃ cl (n : nat),
+                         ⌜ v1 = cloc_to_val cl ⌝ ∗
+                         ⌜ v2 = #n ⌝ ∗
+                         Φ (cloc_to_val (cl.1, cl.2+n)%nat) }} -∗
+    AWP a_ptr_add e1 e2 @ R {{ Φ }}.
+  Proof.
+    iIntros "He2 HΦ". rewrite /a_ptr_add.
+    awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1". awp_lam.
+    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
+    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
+    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
+    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ".
+    destruct cl as [l o]. simpl.
+    iApply awp_bind. iApply (a_bin_op_spec _ _ (λ v, ⌜v = #o⌝)%I (λ v, ⌜v = #n⌝)%I); repeat awp_proj;
+    try by (iApply awp_ret; wp_value_head).
+    iNext. iIntros (? ? -> ->). iExists #(o+n); iSplit; eauto.
+    awp_let. repeat awp_proj. iApply awp_ret; wp_value_head.
+    rewrite -Nat2Z.inj_add.
+    iApply "HΦ".
+  Qed.
+
+  Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
+    AWP e1 @ R {{ Ψ1 }} -∗
+    AWP e2 @ R {{ v2, ▷ ∀ v1, Ψ1 v1 -∗ ∃ p q,
+                         ⌜ v1 = cloc_to_val p ⌝ ∗
+                         ⌜ v2 = cloc_to_val q ⌝ ∗
+                         Φ #(cloc_lt p q) }} -∗
+    AWP a_ptr_lt e1 e2 @ R {{ Φ }}.
+  Proof.
+    iIntros "He1 HΦ". rewrite /a_ptr_add.
+    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
+    awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2". awp_lam.
+    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
+    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
+    iDestruct ("Hv2" with "Hv1") as (p q -> ->) "HΦ".
+    do 2 (awp_proj; awp_let).
+    iApply a_if_spec'.
+    iApply (a_bin_op_spec _ _ (λ v, ⌜v = #p.1⌝)%I (λ v, ⌜v = #q.1⌝)%I);
+      try by (awp_proj; iApply awp_ret; wp_value_head).
+    iNext. iIntros (? ? -> ->).
+    destruct p as [pl po], q as [ql qo]. simpl.
+    destruct (decide (pl = ql)) as [->|?].
+    - iExists #true. iSplit; first iPureIntro.
+      { unfold bin_op_eval. simpl. by rewrite bool_decide_true. }
+      iLeft; iSplit; eauto. awp_proj.
+      iApply (a_bin_op_spec _ _ (λ v, ⌜v = #po⌝)%I (λ v, ⌜v = #qo⌝)%I);
+        try by (try awp_proj; iApply awp_ret; wp_value_head).
+      iNext. iIntros (? ? -> ->).
+      destruct (decide (po < qo)%nat) as [?|?].
+      + iExists #true. compute[cloc_lt bin_op_eval]. simpl. rewrite !bool_decide_true; eauto.
+        by apply Nat2Z.inj_lt.
+      + iExists #false. compute[cloc_lt bin_op_eval]. simpl. rewrite bool_decide_true; eauto.
+        rewrite !bool_decide_false; eauto. intros Hfoo%Nat2Z.inj_lt. done.
+    - iExists #false. iSplit; first iPureIntro.
+      { unfold bin_op_eval. simpl. rewrite bool_decide_false; naive_solver. }
+      iRight. iSplit; eauto. iApply awp_ret; wp_value_head.
+      compute[cloc_lt]. rewrite bool_decide_false; naive_solver.
+  Qed.
+
   Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
     I -∗
     □ (I -∗ AWP c @ R {{ v, (⌜v = #false⌝ ∧ U (Φ #())) ∨

theories/lib/locking_heap.v

@@ -62,6 +62,10 @@ Instance cloc_eq_dec : EqDecision cloc | 0 := _.
 Instance cloc_countable : Countable cloc | 0 := _.
 Instance cloc_inhabited : Inhabited cloc | 0 := _.
 
+(** Pointer arithmetic *)
+Definition cloc_lt (p q : cloc) : bool :=
+  (bool_decide (p.1 = q.1) && bool_decide (p.2 < q.2)).
+
 Definition locking_heapUR : ucmraT :=
   gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).