diff --git a/docs/research/mirai-prototype-report.md b/docs/research/mirai-prototype-report.md new file mode 100644 index 0000000..1b0d880 --- /dev/null +++ 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/.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 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 new file mode 100644 index 0000000..6d40d1d --- /dev/null +++ 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 new file mode 100644 index 0000000..978550b --- /dev/null +++ b/results/mirai/run-let-chains.txt @@ -0,0 +1,40 @@ +918 | ) && let Some(cm) = lhs + | ^^^^^^^^^^^^^^^^^^ + | + = note: see issue #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 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 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 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 new file mode 100644 index 0000000..f63e54d --- /dev/null +++ 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 new file mode 100755 index 0000000..02b1a56 --- /dev/null +++ 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/.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