Simplify pointer arithmetic.

These is no need to do this stuff in the monad.

theories/c_translation/derived.v

@@ -132,30 +132,6 @@ 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

@@ -108,16 +108,14 @@ Notation "f ❲ a ❳ " :=
 
 Definition a_ptr_add : val := λ: "x" "y",
   "lo" ←ᶜ ("x" |||ᶜ "y");;ᶜ
-  "o'" ←ᶜ ((a_ret (Snd (Fst "lo")) +ᶜ (a_ret (Snd "lo")))) ;;ᶜ
+  let: "o'" := Snd (Fst "lo") + Snd "lo" in
   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 }.
+  if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #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.
 
@@ -435,13 +433,12 @@ 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) }} -∗
+                         Φ (cloc_to_val (cloc_add cl n)) }} -∗
     AWP a_ptr_add e1 e2 @ R {{ Φ }}.
   Proof.
     iIntros "He2 HΦ". rewrite /a_ptr_add.
@@ -449,14 +446,9 @@ Section proofs.
     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Φ".
+    iDestruct ("Hv1" with "Hv2") as ([l o] n -> ->) "HΦ /=".
+    do 3 awp_proj. awp_op. awp_let. do 2 awp_proj.
+    iApply awp_ret. iApply wp_value. by rewrite -Nat2Z.inj_add.
   Qed.
 
   Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
@@ -472,29 +464,17 @@ Section proofs.
     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.
+    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
+    do 2 (awp_proj; awp_let). do 2 awp_proj.
+    unfold cloc_lt; simpl. case_bool_decide as Hp; awp_op.
+    - destruct Hp as [-> ?%Nat2Z.inj_lt].
+      rewrite bool_decide_true //. awp_if. do 2 awp_proj.
+      iApply awp_ret. wp_op. rewrite bool_decide_true //.
+    - apply not_and_l_alt in Hp as [?|[? ->]].
+      + rewrite bool_decide_false; last congruence.
+        awp_if. iApply awp_ret. by iApply wp_value.
+      + rewrite bool_decide_true //. awp_if. iApply awp_ret. do 2 wp_proj.
+        wp_op. by rewrite bool_decide_false; last lia.
   Qed.
 
   Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :

theories/lib/locking_heap.v

@@ -62,10 +62,6 @@ 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)).
 
@@ -94,6 +90,9 @@ Section definitions.
   Definition locked_locs (σ : gmap cloc (lvl * val)) : gset cloc :=
     dom _ (filter (λ x, x.2.1 = LLvl) σ).
 
+  (** Pointer arithmetic *)
+  Definition cloc_lt (p q : cloc) : bool :=
+    bool_decide (p.1 = q.1 ∧ p.2 < q.2).
   Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i).
 
   Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2).