feat(quantifiers): Support pointer arithmetic in quantifier predicates

Lower known pointer arithmetic intrinsics (wrapping_add, wrapping_byte_offset,
arith_offset, offset) directly to CBMC pointer Plus expressions in the pure
expression inliner. These intrinsics have no GOTO body to inline, so they
need special handling in inline_call_as_pure_expr.

This enables quantifier predicates like:
  forall!(|i in (0, len)| unsafe { *ptr.wrapping_byte_offset(i as isize) == 0 })

Changes:
- goto_ctx.rs: Recognize pointer arithmetic intrinsics by name and emit
  ptr.plus(offset) directly
- rfc/0010-quantifiers.md: Document pointer arithmetic intrinsic lowering
  in the Detailed Design section
- tests/kani/Quantifiers/pointer_arithmetic.rs: Dedicated test with 3
  harnesses (wrapping_byte_offset forall/exists, wrapping_add forall)

Author: feliperodri

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -512,6 +512,23 @@ impl GotocCtx<'_, '_> {
             return original_expr.clone();
         }
 
+        // Lower known pointer arithmetic intrinsics directly to CBMC expressions.
+        // These intrinsics have no GOTO body to inline, so we handle them specially.
+        // We check that the function name contains a pointer-type path segment to
+        // avoid false-positives on user-defined functions with similar names.
+        // TODO: Replace name-based heuristic with a proper intrinsic registry
+        // (e.g., matching on DefId or a dedicated KaniIntrinsic enum) for
+        // robustness against mangling variations.
+        let fn_name = fn_id.to_string();
+        let is_ptr_fn = fn_name.contains("::ptr::") || fn_name.contains("const_ptr");
+        let is_ptr_arith = is_ptr_fn
+            && (fn_name.contains("wrapping_add") || fn_name.contains("wrapping_byte_offset"));
+        if is_ptr_arith && arguments.len() >= 2 && arguments[0].typ().is_pointer() {
+            let ptr = self.inline_as_pure_expr(&arguments[0], visited);
+            let offset = self.inline_as_pure_expr(&arguments[1], visited);
+            return ptr.plus(offset);
+        }
+
         let function_body = self.symbol_table.lookup(*fn_id).and_then(|sym| match &sym.value {
             SymbolValues::Stmt(stmt) => Some(stmt.clone()),
             _ => None,

rfc/src/rfcs/0010-quantifiers.md

@@ -234,6 +234,15 @@ To solve this, Kani generates **pure expression trees** for quantifier bodies:
    are inlined by looking up the function body in the symbol table, resolving its
    return expression, and substituting parameters — producing a pure expression.
 
+5. **Pointer arithmetic intrinsic lowering**: Wrapping pointer arithmetic functions
+   (`wrapping_byte_offset`, `wrapping_add`) are compiler intrinsics with no GOTO body
+   to inline. The inliner recognizes these by name and lowers them directly to CBMC
+   `Plus` expressions on pointers. Non-wrapping variants (`offset`, `add`) are not
+   supported because they trigger CBMC bounds checks inside quantifier bodies. Example:
+   ```rust
+   kani::forall!(|i in (0, len)| unsafe { *ptr.wrapping_byte_offset(i as isize) == 0 })
+   ```
+
 ### Typed quantifier variables
 
 The `forall!` and `exists!` macros support an optional type annotation:

tests/kani/Quantifiers/pointer_arithmetic.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
+
+//! Tests for pointer arithmetic inside quantifier predicates.
+//! These exercise the intrinsic lowering in `inline_call_as_pure_expr`
+//! which converts wrapping_byte_offset/wrapping_add to CBMC Plus.
+//!
+//! Quantifier ranges are half-open: `|i in (lo, hi)|` means `lo <= i < hi`.
+//! All ranges below match the array lengths to stay in-bounds.
+
+#[kani::proof]
+fn check_wrapping_byte_offset_forall() {
+    let arr: [u8; 8] = [0; 8];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::forall!(|i in (0, 8)| *ptr.wrapping_byte_offset(i as isize) == 0));
+    }
+}
+
+#[kani::proof]
+fn check_wrapping_byte_offset_exists() {
+    let arr: [u8; 8] = [0, 0, 0, 42, 0, 0, 0, 0];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::exists!(|i in (0, 8)| *ptr.wrapping_byte_offset(i as isize) == 42));
+    }
+}
+
+#[kani::proof]
+fn check_wrapping_add_forall() {
+    let arr: [u32; 4] = [10, 20, 30, 40];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::forall!(|i in (0, 4)| *ptr.wrapping_add(i) >= 10));
+    }
+}
+
+/// Tests `ptr.wrapping_add(i)` with a different element type (u8 vs u32).
+#[kani::proof]
+fn check_wrapping_add_u8_forall() {
+    let arr: [u8; 4] = [1, 2, 3, 4];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::forall!(|i in (0, 4)| *ptr.wrapping_add(i) > 0));
+    }
+}