MIRAI prototype — evaluate abstract interpretation on RTOS kernel primitives (ring_buf, scheduler, atomics)

[avrabe]

Part of the V&V coverage initiative — Phase 5 (Abstract Interpretation).

Context

Abstract interpretation is the one layer of the PulseEngine V&V chain we do not yet run — the third DO-333 technique class alongside theorem proving (Lean / Rocq) and bounded model checking (Kani). We are running three weekend-scale prototypes across sigil, gale, and rivet to see what property classes AI catches on our actual code before committing to a long-term investment.

gale is the second prototype target. It is attractive because the kernel primitives are heavy in modular integer arithmetic (RingBuf indices, priority counters, atomic wraparound), which is exactly where abstract interpretation shines. The code is stable, Rust-pure for the primitives we care about, and already has strong Kani + Lean + proptest baselines to compare against.

Tool

MIRAI — abstract interpreter for Rust MIR from Meta. Research-grade, low recent activity, open source. Designed for Rust; covers integer overflow, panic reachability, and some memory properties.

Target code paths

• lib/utils/ring_buffer.c Rust port — index arithmetic (wraparound, modular, consumer/producer)
• Scheduling primitives — priority counters, run-queue index math
• Atomic operations — counter arithmetic in the lock-free paths

Property classes to watch for: integer overflow in counters, modular-arithmetic boundary errors, out-of-bounds index computations, panic-freedom on corner inputs (empty buffer, full buffer, capacity 0, max capacity).

Acceptance

• MIRAI installed hermetically (pinned binary or Nix) and running on gale primitive code
• Report committed at docs/research/mirai-prototype-report.md documenting:
  • Which code paths were analyzed
  • Properties MIRAI flagged (true positives, false positives, false negatives vs hand-inspection)
  • Side-by-side comparison with existing Kani harnesses and Lean invariant specs — overlap vs distinct findings
  • Integration cost assessment
  • Verdict: signal worth integration cost?
  • Go / no-go for MIRAI as a CI gate on gale
• Findings summary posted back to V&V hub (rivet#184) under Phase 5

Related

• Sibling prototypes (parallel experiments): pulseengine/sigil, pulseengine/rivet
• Long-term follow-up: pulseengine/rules_lean — Charon-based value analysis pass on LLBC
• V&V coverage hub: rivet#184

Non-goals

• Production adoption. Evaluation only.
• Replacing Kani or Lean. Abstract interpretation is complementary — expected to catch classes neither currently covers well (integer overflow across call graphs, numerical precision).