add typing rule for ptrdiff on array

theories/lang/lang.v

@@ -244,9 +244,10 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
     val_to_loc v1 = Some l1 →
     val_to_loc v2 = Some l2 →
     l1.1 = l2.1 →
+    0 < ly.(ly_size) →
     valid_ptr l1 σ.(st_heap) →
     valid_ptr l2 σ.(st_heap) →
-    val_of_Z ((l1.2 - l1.2) `div` ly.(ly_size)) ptrdiff_t None = Some v →
+    val_of_Z ((l1.2 - l2.2) `div` ly.(ly_size)) ptrdiff_t None = Some v →
     eval_bin_op (PtrDiffOp ly) PtrOp PtrOp σ v1 v2 v
 | RelOpPNull v1 v2 σ l v op b p a:
     val_to_loc v1 = Some l →

theories/lang/lifting.v

@@ -535,6 +535,38 @@ Proof.
   iModIntro. iMod "HE". by iFrame.
 Qed.
 
+Lemma wp_ptr_diff Φ vl1 l1 vl2 l2 ly vo:
+  val_to_loc vl1 = Some l1 →
+  val_to_loc vl2 = Some l2 →
+  val_of_Z ((l1.2 - l2.2) `div` ly.(ly_size)) ptrdiff_t None = Some vo →
+  l1.1 = l2.1 →
+  0 < ly.(ly_size) →
+  loc_in_bounds l1 0 -∗
+  loc_in_bounds l2 0 -∗
+  (alloc_alive_loc l1 ∧ ▷ Φ vo) -∗
+  WP Val vl1 sub_ptr{ly , PtrOp, PtrOp} Val vl2 {{ Φ }}.
+Proof.
+  iIntros (Hvl1 Hvl2 Hvo ??) "Hl1 Hl2 HΦ".
+  iApply wp_binop_det. iIntros (σ) "Hσ".
+  destruct (decide (valid_ptr l1 σ.(st_heap))). 2: {
+    iDestruct "HΦ" as "[Ha _]".
+    by iMod (alloc_alive_loc_to_valid_ptr with "Hl1 Ha Hσ") as %?.
+  }
+  destruct (decide (valid_ptr l2 σ.(st_heap))). 2: {
+    iDestruct "HΦ" as "[Ha _]".
+    iMod (alloc_alive_loc_to_valid_ptr with "Hl2 [Ha] Hσ") as %?; [|done].
+    by iApply alloc_alive_loc_mono.
+  }
+  iDestruct "HΦ" as "[_ ?]".
+  iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
+  iSplit. {
+    iPureIntro. split.
+    - inversion 1; by simplify_eq.
+    - move => ->. by apply: PtrDiffOpPP.
+  }
+  iModIntro. iMod "HE". by iFrame.
+Qed.
+
 Lemma wp_get_member Φ vl l sl n E:
   val_to_loc vl = Some l →
   is_Some (index_of sl.(sl_members) n) →

theories/typing/array.v

@@ -307,6 +307,42 @@ Section array.
     TypedBinOp v (v ◁ᵥ i @ int it)%I l (l ◁ₗ{β} array_ptr ly base idx len) (PtrNegOffsetOp ly) (IntOp it) PtrOp :=
     λ T, i2p (type_bin_op_neg_offset_array_ptr l β T ly it v i idx len base).
 
+  Lemma type_bin_op_diff_array_ptr_array l1 β l2 T ly idx (len : nat) tys:
+    (l1 ◁ₗ{β} array_ptr ly l2 idx len -∗
+     ⌜0 < ly.(ly_size)⌝ ∗
+     ⌜0 < length tys⌝ ∗
+     ⌜idx ≤ max_int ptrdiff_t⌝ ∗
+     (∀ ty, ⌜tys !! 0%nat = Some ty⌝ -∗ l2 ◁ₗ{β} ty -∗ alloc_alive_loc l2 ∗ True) ∧
+     (l2 ◁ₗ{β} array ly tys -∗ T (i2v idx ptrdiff_t) (t2mt (idx @ int ptrdiff_t)))) -∗
+     typed_bin_op l1 (l1 ◁ₗ{β} array_ptr ly l2 idx len) l2 (l2 ◁ₗ{β} array ly tys) (PtrDiffOp ly) PtrOp PtrOp T.
+  Proof.
+    iIntros "HT (->&%&%&#Hlib) Hl2" (Φ) "HΦ".
+    iDestruct ("HT" with "[$Hlib//]") as (? ? ?) "HT".
+    have /(val_of_Z_is_Some None) [vo Hvo] : idx ∈ ptrdiff_t. {
+      split; [|done].
+      rewrite /min_int/=/int_half_modulus/=/bits_per_int/bytes_per_int/=/bits_per_byte. lia.
+    }
+    rewrite /i2v Hvo/=.
+    iApply wp_ptr_diff; [by apply: val_to_of_loc|by apply: val_to_of_loc| |done|done| | |].
+    { rewrite /= Z.add_simpl_l Z.mul_comm Z.div_mul //. lia. }
+    { iApply (loc_in_bounds_offset with "Hlib"); simpl; unfold addr in *; [done|nia|].
+      rewrite {2}/ly_size/=. nia. }
+    { iApply (loc_in_bounds_shorten with "Hlib"). lia. }
+    iSplit. {
+      iDestruct "HT" as "[HT _]".
+      destruct tys as [|ty tys] => //=.
+      iDestruct "Hl2" as "(?&?&[Hty _])".
+      rewrite offset_loc_0. iApply alloc_alive_loc_mono; [simpl; done|].
+      iDestruct ("HT" with "[//] Hty") as "[$ _]". }
+    iDestruct "HT" as "[_ HT]". iSpecialize ("HT" with "Hl2").
+    iModIntro. iApply "HΦ"; [|iApply "HT"].
+    iPureIntro. by apply: val_to_of_Z.
+  Qed.
+  Global Instance type_bin_op_diff_array_ptr_array_inst (l1 : loc) β l2 ly idx (len : nat) tys:
+    TypedBinOp l1 (l1 ◁ₗ{β} array_ptr ly l2 idx len)%I l2 (l2 ◁ₗ{β} array ly tys) (PtrDiffOp ly) PtrOp PtrOp :=
+    λ T, i2p (type_bin_op_diff_array_ptr_array l1 β l2 T ly idx len tys).
+
+
   Lemma subsume_array_ptr_alloc_alive β l ly base idx len T:
     alloc_alive_loc base ∗ T -∗
     subsume (l ◁ₗ{β} array_ptr ly base idx len) (alloc_alive_loc l) T.