Verify: Kani-prove the pure scalar core of the CEL engine (arithmetic + conversions)

[rrrodzilla]

Workstream: Verification · Part of #89

Context

The CEL engine is verified against the cel-spec conformance corpus (#90) — ~2,123 example-based tests. That proves the engine matches CEL on the cases the corpus enumerates. It does not prove the engine is total over the whole input domain. For a fail-closed ATO target, the residual risk is exactly the adversarial edge a finite corpus never enumerates: i64::MIN / -1, NaN → int, u64::MAX vs i64, range boundaries, etc.

Kani (bit-precise bounded model checker on CBMC) closes that gap: it proves a property holds for all inputs within a bound. Kani never enters the shipped binary or the dependency tree, so it adds zero FIPS/airgap surface — it strengthens the ADR-0002 "fully owned, fully verified" story without compromising it.

Scope (Tier 1 — the bullseye)

Kani harnesses over the pure, total scalar functions — best fit for symbolic execution (scalars, no strings, no heap, no recursion). These functions are already factored as pure helpers (eval/funcs/convert.rs documents itself as "exhaustively testable without the evaluator").

Target files:

• crates/schema-forge-cel/src/eval/ops.rs — arithmetic (Add/Sub/Mul/Div/Rem, unary Neg), heterogeneous numeric comparison, Timestamp ± Duration, Duration arithmetic.
• crates/schema-forge-cel/src/eval/funcs/convert.rs — int() / uint() / double() conversions, duration-nanos grouping.

Properties to prove, for every scalar input:

1. Totality — never panics (no unwrap/overflow-panic/unreachable).
2. No silent wrap/truncate — arithmetic returns the mathematically correct value or Err(Overflow); never a wrapped result.
3. Conversion soundness — out-of-range / NaN / ±Inf reject with Err, never a UB cast or silent saturation against CEL semantics.

Concrete first harnesses (each a known landmine, each ~5 lines of kani::any()):

• i64::MIN / -1 and i64::MIN % -1 → range error
• checked_neg(i64::MIN) overflow → error
• f64 → i64/u64 for NaN, ±Inf, and values just past 2^63/2^64 (mantissa-precision boundary)
• u64↔i64 mixed comparison — sign-correct across the full cross product, incl. u64 > i64::MAX
• TimeDelta add/sub and Timestamp ± Duration at the DateTime range edges → range error, not panic
• integer Add/Sub/Mul overflow → Err, never wrap (i64 and u64)

Approach

• Harnesses behind #[cfg(kani)] in schema-forge-cel; run via cargo kani as a separate, slow CI job (NOT the nextest gate).
• Use current Kani function contracts (#[kani::requires] / #[kani::ensures]) to state the fail-closed postcondition directly on each helper.
• Bound any recursive/loop proof with #[kani::unwind(N)] / loop contracts.

Non-goals (deliberately routed elsewhere)

• Lexer / parser (lexer.rs, parser.rs) — symbolic strings detonate CBMC. Cover the string front-end with the conformance corpus plus a cargo-fuzz differential target (parse → eval panic-freedom). Tracked separately.
• The recursive tree-walking evaluate over arbitrary ASTs — unbounded recursion; owned by the corpus + fuzzing (stack-depth DoS hardening already exists there).

Follow-on (later tiers, out of scope here)

• Tier 2: comparison total-order soundness (folded into Tier 1 above where cheap).
• Tier 3 (bounded, #[kani::unwind]): value/bridge.rs fail-closed contract (unsupported → Err, never Null); check::infer no-panic for bounded AST depth.

Acceptance

• cargo kani harnesses for the Tier 1 properties above, green.
• A CI job (separate from nextest) runs them; documented how to run locally.
• A short note (README or ADR) recording what Kani proves vs. what the corpus/fuzzing prove, so the division of assurance is auditable.

---

Dependencies: Engine core (#107/#108/#109) complete. Independent of the remaining capability work (#95). Soft.

[rrrodzilla]

Approach decided

1. Extract pure numeric kernels first. Refactor the scalar math out of the enum-dispatch in eval/ops.rs / eval/funcs/convert.rs into pure, total functions (fn checked_int_div(a: i64, b: i64) -> Result<i64, Overflow>, the f64 → int range/round kernel, the mixed u64/i64 compare kernel, the TimeDelta/DateTime range kernels). arithmetic()/compare()/the int()/uint()/double() dispatchers then just call the kernels. Kani verifies the kernels directly; the dispatch becomes correct-by-inspection. This is a test-covered refactor of code that currently passes the full conformance suite — behavior must not change (the 2,123-test gate is the guard).

2. Prove semantic-boundary correctness, not just panic-freedom. Each harness carries a small spec oracle (compute the expected value in i128/f64/with the CEL rounding rule) and asserts the kernel matches it across all symbolic inputs — proving the exact boundary where a conversion flips to a range error and that the rounding mode is half-away-from-zero everywhere. Panic-freedom falls out as a side effect.

3. Plain #[kani::proof] harnesses with assert! (version-stable). Adopt function contracts later only where compositional reuse pays for itself.

4. CI: path-filtered job on the self-hosted Govcraft runner. Runs cargo kani only when eval/ops.rs / eval/funcs/convert.rs (and the new kernel module) change. Separate from the nextest gate (Kani pins its own toolchain and is slow). Local-run instructions documented.

Sequencing: start after #95 lands. These files are disjoint from #95's work (#95 touches the AST-walker / dsl / acton side, not ops/convert), so there's no merge hazard — the wait is purely to avoid a third concurrent work thread.