Support arithmetic in quantifier predicates via pure expression inlining

[feliperodri]

Enables arithmetic operations (+, -, *, %) inside forall! and exists! predicates, and adds typed quantifier variables. Previously, any arithmetic in a quantifier body was rejected by CBMC as a "side effect."

Resolves #4135 — This branch adds typed quantifier variables (|d: u64 in (lo, hi)|), removing the usize restriction.

Problem

CBMC requires quantifier bodies to be side-effect-free. But even i + 1 in Rust compiles to OverflowResultPlus wrapped in a StatementExpression, which CBMC rejects. This meant quantifiers could only contain comparisons, not meaningful arithmetic predicates.

Solution

Pure expression inlining infrastructure (goto_ctx.rs)

The inline_as_pure_expr function handles the checked arithmetic pattern end-to-end:

1. StatementExpression flattening: Collects Decl assignments and resolves intermediate variables, eliminating the statement wrapper.
2. Struct field extraction: Member(Struct([f0, f1, ...]), "N") → fN, avoiding invalid .member() calls on intermediate structs.
3. Overflow simplification: Member(OverflowResultPlus(a, b), "result") → Plus(a, b). Same for Minus and Mult. The overflow check is dropped (sound for symbolic evaluation in quantifier bodies).

Note: This infrastructure is #[allow(dead_code)] in this PR. It is used by the follow-up quantifier-pointer-arithmetic branch which adds pointer arithmetic intrinsic lowering. In this PR, the existing handle_quantifiers post-pass handles all function call inlining.

Quantifier codegen (hooks.rs)

• build_quantifier_predicate extracts the closure body and substitutes parameters directly, producing a side-effect-free expression for simple predicates (comparisons, logical operators).
• Returns Option<Expr> — when the substituted expression still contains side effects (e.g., StatementExpression from checked arithmetic or pointer operations like wrapping_byte_offset), it returns None. This is because substitute_symbol does not recurse into StatementExpression nodes.
• When None is returned, the caller falls back to find_closure_call_expr, which creates a closure function call. The handle_quantifiers post-pass (in compiler_interface.rs) then inlines this call after all functions are codegen'd — the same approach used on main.
• extract_return_expr refactored with ReturnExpr enum (Symbol/Direct) for clarity.
• Graceful fallback with gcx.tcx.dcx().warn() instead of assert! ICE when parameter count is unexpected.

Typed quantifier variables (kani_core/src/lib.rs)

Added |d: u64 in (lo, hi)| syntax to forall! and exists!:

kani::forall!(|d: u64 in (1, n)| x % d == 0)

Uses $t:tt capture since $t:ty cannot be followed by in in macro rules.

RFC update

Updated rfc/src/rfcs/0010-quantifiers.md Detailed Design section with the implementation approach, soundness notes, and typed variable syntax.

Example

#[kani::loop_invariant(
    a > 0
    && kani::forall!(|d: u64 in (1, a.saturating_add(1))|
        d == 0 || ((x % d == 0 && y % d == 0)
        == (a % d == 0 && b % d == 0)))
)]

This GCD loop invariant (with typed u64 variable, saturating_add, modulo, equality, and logical operators) verifies successfully with Z3 in ~0.5s.

Testing

• New tests:
  • arithmetic.rs — 5 harnesses testing +, -, *, % in quantifier bodies
  • typed_variables.rs — 2 harnesses testing |i: u64 in ...| syntax
  • gcd_invariant.rs — GCD loop invariant with typed variable and modulo
• Existing tests that use pointer arithmetic (contracts_fail, multiple_quantifiers, for_loop_for_zip, for_loop_for_tuple_with_quantifiers) continue to work via the fallback path.

Design: Two-path quantifier codegen

Predicate type	Path	Example
Simple (no side effects)	Direct substitution in build_quantifier_predicate	|i in (0,n)| a[i] > 0
Complex (checked arithmetic, pointer ops)	Fallback to closure call → handle_quantifiers post-pass	|k in (0,8)| *ptr.wrapping_byte_offset(k)

The is_side_effect() check on the substituted expression determines which path is taken. This ensures:

• Simple predicates get clean, direct codegen.
• Complex predicates use the post-pass inlining from main.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[feliperodri]

The three quantifier tests that use pointer arithmetic in predicates (array.rs, contracts.rs, from_raw_parts.rs) are marked as fixme in this PR because they require lowering pointer arithmetic intrinsics (wrapping_add, wrapping_byte_offset, arith_offset) to CBMC pointer expressions. These tests were already broken on main, this is not a regression.

I'll address this in a follow-up PR (quantifier-pointer-arithmetic) which adds special-case handling in inline_call_as_pure_expr to lower these intrinsics directly to CBMC Plus expressions. That PR will also address #4263 and #4310.

[feliperodri]

The Kani Extra failure is unrelated to the changes in this PR. It should not impact the review of this PR.

Here is a deep-dive into the CI failure in more details:

The main concern: s2n-quic/quic/s2n-quic-core/inet::checksum::tests::differential. The benchcomp WARNING already calls this out: solver_runtime went from ~176s to ~299s, a ~70% regression. Total verification time jumped from ~219s to ~342s. The program steps and VCCs are identical, so this isn't a structural change, the solver is just having a harder time with the same formula. This is the most significant regression in the set.

Secondary regressions worth noting

Benchmark	Metric	Old	New	Change
s2n-quic/.../sliding_window::test::insert_test	solver_runtime	58.4s	81.9s	+40%
s2n-quic/.../u32_u16_differential	solver_runtime	11.3s	16.3s	+44%
s2n-quic/.../cmsg::round_trip_test	solver_runtime	229s	296s	+29%
misc/display_trait/fast	solver_runtime	44.2s	58.3s	+32%
s2n-quic/.../rtt_estimator::weighted_average_test	solver_runtime	73.1s	82.6s	+13%
vec/box_dyn/main	solver_runtime	1.02s	1.34s	+31%

Improvements (kani_new is faster)

Benchmark	Metric	Old	New	Change
btreeset/insert_multi	solver_runtime	5.07s	2.56s	-49%
s2n-quic/.../vectored_copy_fuzz_test	solver_runtime	257s	165s	-36%
s2n-quic/.../cmsg::iter_test	solver_runtime	12.9s	11.3s	-13%
s2n-quic/.../cmsg::collect_test	solver_runtime	83.4s	77.2s	-7%
misc/display_trait/slow	verification_time	110s	104s	-6%

Summary

The pattern is almost entirely in solver_runtime: symex times and program structure (steps/VCCs) are essentially unchanged.