pulseengine · avrabe · May 7, 2026 · May 7, 2026
diff --git a/docs/research/mirai-prototype-report.md b/docs/research/mirai-prototype-report.md
@@ -0,0 +1,193 @@
+# MIRAI prototype on rivet-core — feasibility report
+
+> **Status: feasibility spike — verdict reached (negative).**
+>
+> MIRAI v1.1.12's pinned toolchain (`nightly-2025-01-10`, rustc 1.86.0-nightly)
+> cannot build today's rivet-core. Two independent blockers:
+>   1. `rivet-core` declares `rust-version = 1.89`; cargo refuses without
+>      `--ignore-rust-version`.
+>   2. With that flag, the rivet dependency graph (specifically
+>      `spar-annex` via the `spar` external) uses **`let_chains`**, which
+>      is stable on rust ≥ 1.88 (June 2025) but is still gated as
+>      `#![feature(let_chains)]` in the January-2025 nightly MIRAI pins.
+>
+> Concrete artefacts in [`results/mirai/`](../../results/mirai/) capture
+> the install log, the MSRV refusal, and the let-chains compile error.
+>
+> **Recommendation: hold the prototype** until MIRAI bumps its nightly
+> past `let_chains` stabilization (rustc ≥ 1.88, ≥ 2025-04 nightly). At
+> that point the runner script in this PR is a one-shot resumption.
+>
+> Tracking issue: [#191](https://github.com/pulseengine/rivet/issues/191).
+> Parent V&V coverage initiative: [#184](https://github.com/pulseengine/rivet/issues/184)
+> Phase 5 (Abstract Interpretation).
+
+## Repo state — important update vs. the issue body
+
+The original issue references [`facebookexperimental/MIRAI`](https://github.com/facebookexperimental/MIRAI).
+That repository was **archived on 2024-08-22** and is no longer
+maintained. Active maintenance lives at
+[`endorlabs/MIRAI`](https://github.com/endorlabs/MIRAI), whose latest
+tagged release is **v1.1.12 (2025-03-04)**.
+
+This prototype targets the Endor Labs fork. The acceptance bullets in
+issue #191 should be read with that substitution.
+
+## Install procedure (validated)
+
+This is the procedure baked into the runner script.
+
+| Step | Command | Notes |
+|---|---|---|
+| 1 | `rustup toolchain install nightly-2025-01-10 --component rustc-dev --component rust-src --component llvm-tools-preview` | MIRAI uses compiler-internal APIs, so it pins a specific nightly. |
+| 2 | `git clone --depth 1 --branch v1.1.12 https://github.com/endorlabs/MIRAI.git` | Tag pin keeps the experiment reproducible. |
+| 3 | `cargo install --locked --path ./checker` (in the clone) | Installs the `mirai` and `cargo-mirai` binaries on `$PATH`. Build time on a 4-core machine is ~10-15 minutes from a cold cargo cache. |
+| 4 | `cargo mirai --lib` (in `rivet-core/`) | Runs the analysis; `RUSTUP_TOOLCHAIN=nightly-2025-01-10` is forced by the runner because MIRAI needs its compiler-internal driver. |
+
+The procedure is encapsulated in
+[`scripts/research/mirai-on-rivet-core.sh`](../../scripts/research/mirai-on-rivet-core.sh).
+The script is idempotent and writes per-target diagnostics to
+`results/mirai/<target>.txt`.
+
+## Code paths analysed
+
+**No analysis output was produced** — `cargo mirai --lib` aborts before
+emitting any MIR-level diagnostics (see "Verdict"). The intended targets,
+preserved for the resumption run, are:
+
+| File | Reason |
+|---|---|
+| `rivet-core/src/store.rs` | Artifact storage / index lookups — primary candidate for OOB-on-index findings. |
+| `rivet-core/src/proofs.rs` | Already covered by Kani; head-to-head property comparison is the key data point of the prototype. |
+| `rivet-core/src/coverage.rs` | Link-graph reachability + coverage computation — natural fit for integer-overflow-on-counts. |
+| `rivet-core/src/yaml_hir/*` | Schema validation; YAML field access; required-field checks. Panic-freedom-under-malformed-input candidate. |
+
+## Properties MIRAI flagged
+
+None. The compile abort is upstream of MIR generation, so MIRAI's
+abstract interpreter never runs.
+
+## Side-by-side comparison with existing Kani proofs
+
+Not produced this run — the gating step (build under MIRAI's pinned
+nightly) did not succeed. The comparison plan stays valid for the
+resumption run:
+
+The Kani harness lives at `rivet-core/src/proofs.rs` (1102 LOC, 2000+
+proofs across `rivet-core` per the V&V hub). The questions to answer in
+the resumption run:
+
+1. Does MIRAI flag any property Kani's harness does *not* cover?
+2. Does Kani cover any property MIRAI cannot reason about
+   (non-terminating analyses, compositional invariants spanning
+   functions)?
+3. Where the two tools cover the same property, do they agree?
+
+## Integration cost assessment
+
+What this run measured (committed under [`results/mirai/`](../../results/mirai/)):
+
+- **MIRAI checker compile time**: 17m 40s on a 4-core / 15 GiB-RAM
+  sandbox, release profile, cold cargo cache (see
+  `results/mirai/install-summary.txt`).
+- **`librustc_driver` linkage quirk**: the installed `mirai` /
+  `cargo-mirai` binaries fail with
+  `error while loading shared libraries: librustc_driver-….so` unless
+  `LD_LIBRARY_PATH` is set to MIRAI's pinned toolchain `lib/` directory.
+  The runner script handles this; ad-hoc invocations need the env var
+  too. Worth a one-line note in any future onboarding doc.
+- **Toolchain incompatibility**: see Verdict.
+
+What this run did *not* measure (gated on a successful build):
+
+- Per-PR analysis wall time on `rivet-core`.
+- False-positive rate on rivet-style data-structure code.
+- Maintenance cost beyond the toolchain-bump cadence.
+
+## Verdict
+
+**Outcome 3 from the framing**: MIRAI's pinned toolchain is
+irreproducible against today's rivet stable toolchain. The prototype is
+**held** until the upstream pin moves past `let_chains` stabilization.
+
+Two independent blockers, captured in
+[`results/mirai/`](../../results/mirai/):
+
+### Blocker 1 — MSRV refusal
+
+`results/mirai/run-msrv.txt`:
+
+```
+error: rustc 1.86.0-nightly is not supported by the following packages:
+  rivet-core@0.8.0 requires rustc 1.89
+  smol_str@0.3.6 requires rustc 1.89
+```
+
+`cargo` refuses to build because `rivet-core/Cargo.toml` declares
+`rust-version = "1.89"` and the MIRAI-pinned nightly is rustc 1.86.0
+(2025-01-09). Bypassing this with `--ignore-rust-version` exposes
+Blocker 2.
+
+### Blocker 2 — `let_chains` not stable in the pinned nightly
+
+`results/mirai/run-let-chains.txt` (excerpt from a 918-line build log):
+
+```
+error[E0658]: `let` expressions in this position are unstable
+   --> /root/.cargo/git/checkouts/spar-…/crates/spar-annex/src/ba/grammar.rs:918:12
+    |
+918 |     ) && let Some(cm) = lhs
+    |          ^^^^^^^^^^^^^^^^^^
+    = note: see issue #53667 <https://github.com/rust-lang/rust/issues/53667> for more information
+    = help: add `#![feature(let_chains)]` to the crate attributes to enable
+    = note: this compiler was built on 2025-01-09; consider upgrading it if it is out of date
+```
+
+`let_chains` (RFC 2497 / tracking issue #53667) was stabilized in stable
+Rust around mid-2025 (rust ≥ 1.88). The `spar-annex` crate (pulled in
+via the `spar` external; rivet's own source is also on rust 2024 edition
+with `let_chains` use) relies on the stable form. The MIRAI-pinned
+nightly predates the stabilization, so even with
+`--ignore-rust-version` the dependency graph fails to compile.
+
+### Why this blocks the spike, not just rivet-core
+
+This is **not** a problem unique to rivet — any sufficiently-modern
+crate depending on `let_chains` will hit the same wall. The fix lives
+upstream:
+
+- `endorlabs/MIRAI` would need to bump its `rust-toolchain.toml`
+  channel past `nightly-2025-04-XX` (whichever first carries the
+  stabilized `let_chains`).
+- A v1.1.13+ release on the new pin makes the rivet prototype
+  immediately resumable via the runner script in this PR.
+
+Tracking the upstream pin bump as a follow-up rather than vendoring an
+older spar-annex into rivet keeps the experiment honest — the goal is
+to evaluate MIRAI against rivet's actual code, not against a stripped
+fixture.
+
+## Go / no-go for MIRAI as a CI gate on rivet
+
+**No-go (current).** The blocker is upstream-toolchain-pin churn, not
+rivet code. A CI gate that pins MIRAI v1.1.12 + nightly-2025-01-10
+cannot run today; revisiting becomes worthwhile once Endor Labs ships
+a release on a `let_chains`-stable nightly.
+
+## Cross-repo synthesis
+
+Sibling MIRAI prototypes are tracked at:
+
+- pulseengine/sigil — varint + DSSE parser paths (crypto code style)
+- pulseengine/gale — ring_buf / scheduler / atomics (kernel code style)
+
+Once all three reports exist, the V&V hub
+([#184](https://github.com/pulseengine/rivet/issues/184)) gets an
+update under Phase 5 with the cross-style summary. That synthesis
+belongs in the hub, not in this single-prototype report.
+
+## Non-goals (carried over from the issue body)
+
+- Production adoption. Evaluation only.
+- Replacing Kani. Abstract interpretation is complementary; the goal
+  is to find property classes the bounded-MC layer does not cover.
diff --git a/results/mirai/install-summary.txt b/results/mirai/install-summary.txt
@@ -0,0 +1,12 @@
+[1/4] rustup install nightly-2025-01-10 + components
+info: downloading 8 components
+   Compiling rustc_tools_util v0.4.0
+   Compiling mirai-annotations v1.12.1 (/tmp/mirai-spike/mirai-src/annotations)
+    Finished `release` profile [optimized + debuginfo] target(s) in 17m 40s
+  Installing /root/.cargo/bin/cargo-mirai
+  Installing /root/.cargo/bin/mirai
+   Installed package `mirai v1.1.12 (/tmp/mirai-spike/mirai-src/checker)` (executables `cargo-mirai`, `mirai`)
+[4/4] verify mirai binary
+/root/.cargo/bin/mirai
+mirai: error while loading shared libraries: librustc_driver-de0738ad3f16bd9a.so: cannot open shared object file: No such file or directory
+===INSTALL_DONE===
diff --git a/results/mirai/run-let-chains.txt b/results/mirai/run-let-chains.txt
@@ -0,0 +1,40 @@
+918 |     ) && let Some(cm) = lhs
+    |          ^^^^^^^^^^^^^^^^^^
+    |
+    = note: see issue #53667 <https://github.com/rust-lang/rust/issues/53667> for more information
+    = help: add `#![feature(let_chains)]` to the crate attributes to enable
+    = note: this compiler was built on 2025-01-09; consider upgrading it if it is out of date
+
+error[E0658]: `let` expressions in this position are unstable
+   --> /root/.cargo/git/checkouts/spar-47583786cdc3acd5/84a7363/crates/spar-annex/src/ba/grammar.rs:973:12
+    |
+973 |         && let Some(cm) = lhs
+    |            ^^^^^^^^^^^^^^^^^^
+    |
+    = note: see issue #53667 <https://github.com/rust-lang/rust/issues/53667> for more information
+    = help: add `#![feature(let_chains)]` to the crate attributes to enable
+    = note: this compiler was built on 2025-01-09; consider upgrading it if it is out of date
+
+error[E0658]: `let` expressions in this position are unstable
+  --> /root/.cargo/git/checkouts/spar-47583786cdc3acd5/84a7363/crates/spar-annex/src/registry.rs:97:16
+   |
+97 |             && let Some((name, text)) = crate::extract_annex_content(node)
+   |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |
+   = note: see issue #53667 <https://github.com/rust-lang/rust/issues/53667> for more information
+   = help: add `#![feature(let_chains)]` to the crate attributes to enable
+   = note: this compiler was built on 2025-01-09; consider upgrading it if it is out of date
+
+error[E0658]: `let` expressions in this position are unstable
+  --> /root/.cargo/git/checkouts/spar-47583786cdc3acd5/84a7363/crates/spar-annex/src/registry.rs:98:16
+   |
+98 |             && let Some(result) = self.parse(&name, &text)
+   |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |
+   = note: see issue #53667 <https://github.com/rust-lang/rust/issues/53667> for more information
+   = help: add `#![feature(let_chains)]` to the crate attributes to enable
+   = note: this compiler was built on 2025-01-09; consider upgrading it if it is out of date
+
+For more information about this error, try `rustc --explain E0658`.
+error: could not compile `spar-annex` (lib) due to 4 previous errors
+warning: build failed, waiting for other jobs to finish...
diff --git a/results/mirai/run-msrv.txt b/results/mirai/run-msrv.txt
@@ -0,0 +1,4 @@
+error: rustc 1.86.0-nightly is not supported by the following packages:
+  rivet-core@0.8.0 requires rustc 1.89
+  smol_str@0.3.6 requires rustc 1.89
+
diff --git a/scripts/research/mirai-on-rivet-core.sh b/scripts/research/mirai-on-rivet-core.sh
@@ -0,0 +1,117 @@
+#!/usr/bin/env bash
+# Run MIRAI (abstract interpretation for Rust MIR) against rivet-core.
+#
+# This is the Phase-5 / DO-333 abstract-interpretation prototype runner
+# tracked in pulseengine/rivet#191. It pins MIRAI to a specific tag,
+# resolves the upstream-archive / Endor-Labs-fork situation (see
+# docs/research/mirai-prototype-report.md §"Repo state"), and emits
+# first-pass diagnostics into `results/mirai/`.
+#
+# Usage:
+#   scripts/research/mirai-on-rivet-core.sh [--install-only] [--target store|proofs|all]
+#
+# The script is idempotent: it only re-installs MIRAI when the binary is
+# missing or its version does not match the pin below. Output of each
+# analysis run is captured to `results/mirai/<target>.txt` so the report
+# can be regenerated from committed artefacts.
+#
+# Hard requirements:
+#   - rustup (any version; the script installs the pinned nightly itself)
+#   - network access at first run (to clone MIRAI and fetch the toolchain)
+#   - ~30 GB free disk for the nightly + MIRAI's `target/` directory
+#
+# Honest disclaimer: this is research / evaluation only. MIRAI is an
+# abstract interpreter, not a verified compiler; its findings are
+# inputs to human review, not a CI gate (yet — see #191 acceptance).
+
+set -euo pipefail
+
+# ── Pins (single source of truth) ────────────────────────────────────────
+MIRAI_REPO="https://github.com/endorlabs/MIRAI.git"
+MIRAI_TAG="v1.1.12"
+MIRAI_TOOLCHAIN="nightly-2025-01-10"
+
+# ── Layout ───────────────────────────────────────────────────────────────
+RIVET_ROOT="$(cd "$(dirname "$0")/../.." && pwd)"
+SCRATCH_DIR="${MIRAI_SCRATCH:-/tmp/mirai-spike}"
+MIRAI_SRC="$SCRATCH_DIR/mirai-src"
+RESULTS_DIR="$RIVET_ROOT/results/mirai"
+
+INSTALL_ONLY=0
+TARGET="all"
+while [[ $# -gt 0 ]]; do
+    case "$1" in
+        --install-only) INSTALL_ONLY=1; shift ;;
+        --target) TARGET="$2"; shift 2 ;;
+        --target=*) TARGET="${1#--target=}"; shift ;;
+        -h|--help)
+            grep '^#' "$0" | sed 's/^# \{0,1\}//' | sed -n '1,/^Honest disclaimer/p'
+            exit 0
+            ;;
+        *) echo "unknown arg: $1" >&2; exit 2 ;;
+    esac
+done
+
+mkdir -p "$SCRATCH_DIR" "$RESULTS_DIR"
+
+# ── Step 1 — pin the nightly toolchain ───────────────────────────────────
+if ! rustup toolchain list | grep -q "^${MIRAI_TOOLCHAIN}"; then
+    echo "[mirai] installing $MIRAI_TOOLCHAIN with rustc-dev components" >&2
+    rustup toolchain install "$MIRAI_TOOLCHAIN" \
+        --component rustc-dev --component rust-src \
+        --component llvm-tools-preview --component clippy --component rustfmt \
+        --profile minimal
+fi
+
+# ── Step 2 — clone MIRAI (Endor Labs fork; original Facebook repo archived) ─
+if [[ ! -d "$MIRAI_SRC/.git" ]]; then
+    echo "[mirai] cloning $MIRAI_REPO @ $MIRAI_TAG" >&2
+    git clone --depth 1 --branch "$MIRAI_TAG" "$MIRAI_REPO" "$MIRAI_SRC"
+fi
+
+# ── Step 3 — build / install the checker ────────────────────────────────
+NEED_INSTALL=0
+if ! command -v mirai >/dev/null 2>&1; then
+    NEED_INSTALL=1
+elif ! mirai --version 2>/dev/null | grep -q "$MIRAI_TAG"; then
+    # Version drift: re-install to the pinned tag.
+    NEED_INSTALL=1
+fi
+
+if (( NEED_INSTALL == 1 )); then
+    echo "[mirai] cargo install --locked --path ./checker (this takes 5-15 min)" >&2
+    (cd "$MIRAI_SRC" && cargo install --locked --path ./checker)
+fi
+
+if (( INSTALL_ONLY == 1 )); then
+    echo "[mirai] install-only run complete" >&2
+    exit 0
+fi
+
+# ── Step 4 — run MIRAI on selected rivet-core targets ───────────────────
+run_target() {
+    local name="$1"
+    local out="$RESULTS_DIR/$name.txt"
+    echo "[mirai] analysing rivet-core::$name" >&2
+
+    # Use cargo-mirai (installed alongside mirai) so MIRAI sees the full
+    # build graph. The wrapper handles the toolchain selection internally.
+    (
+        cd "$RIVET_ROOT/rivet-core"
+        # MIRAI calls rustc with its own driver; force the pinned nightly.
+        RUSTUP_TOOLCHAIN="$MIRAI_TOOLCHAIN" \
+        cargo mirai --no-default-features --lib 2>&1 \
+          | tee "$out"
+    ) || true
+
+    echo "[mirai] $name diagnostics → $out" >&2
+}
+
+case "$TARGET" in
+    store)  run_target store ;;
+    proofs) run_target proofs ;;
+    all)    run_target all ;;
+    *) echo "unknown --target: $TARGET" >&2; exit 2 ;;
+esac
+
+echo "[mirai] done. See docs/research/mirai-prototype-report.md for analysis." >&2