spike(research): MIRAI feasibility scaffold for rivet-core (#191)#264
Draft
spike(research): MIRAI feasibility scaffold for rivet-core (#191)#264
Conversation
Picks up the feasibility-spike sub-AC proposed in the [2026-04-26 triage comment](#191 (comment)). Lands the procedural deliverables now; first-pass diagnostics from a live `cargo mirai` run will follow as a separate commit on this branch. Headline finding: the issue body references `facebookexperimental/MIRAI`, which was archived 2024-08-22 and is read-only. Active maintenance lives at `endorlabs/MIRAI` (latest v1.1.12, 2025-03-04, nightly-2025-01-10 toolchain pin). The runner script and the report target the fork and flag the substitution explicitly so the issue can be retargeted. Changes: - scripts/research/mirai-on-rivet-core.sh - Idempotent install + analysis runner. Pins MIRAI tag, nightly toolchain (with rustc-dev / rust-src / llvm-tools-preview), and output paths in one place. - --install-only short-circuit for setup-without-analysis. - --target {store|proofs|all} for selective re-runs. - Writes diagnostics to results/mirai/<target>.txt for committed artefact-driven reporting. - docs/research/mirai-prototype-report.md - Validated install procedure (the part the script automates) + explicit Endor-Labs-fork substitution callout for #191. - Section stubs for "Code paths analysed", "Properties MIRAI flagged", "Side-by-side comparison with existing Kani proofs", "Integration cost assessment", "Verdict", "Go/no-go for CI gate". - Report frames the three possible outcomes upfront so the run's output drops directly into one of them. Out of scope for this commit: - First-pass diagnostics (`results/mirai/<target>.txt`) — a live run is required; the install pipeline takes 10-15 min to compile the checker on a 4-core box, then minutes per analysis target. - Findings summary on the V&V hub (#184 Phase 5) — gated on the diagnostics + verdict landing first. Refs: FEAT-001
9 tasks
Automated review for PR #264pulseengine/rivet: Verdict: 💬 Comment Summary: The feasibility report for the MIRAI prototype on rivet-core has been approved. The install procedure is validated, and the first-pass analysis output and comparative verdict against Kani are TODO placeholders to be filled by a follow-up run of the runner script. Findings: 0 mechanical (rivet) · 1 from local AI model. Findings (1):
Generated by a local AI model and post-validated against a strict JSON contract. Each finding includes the verbatim line being criticised — verify by reading the file at the cited location. Reviewed at |
Live spike completed; verdict is outcome 3 of the three framed in the
prior commit ("install irreproducible against rivet stable toolchain").
What ran:
- rustup toolchain install nightly-2025-01-10 (with rustc-dev / rust-src
/ llvm-tools-preview): clean.
- git clone --branch v1.1.12 endorlabs/MIRAI: clean.
- cargo install --locked --path ./checker: 17m 40s, clean. Installed
/root/.cargo/bin/{mirai, cargo-mirai}.
- mirai --version: needs LD_LIBRARY_PATH pointing at the nightly's lib/
dir (librustc_driver linkage quirk). Documented in the report.
- cargo mirai --lib on rivet-core: TWO independent blockers, both
upstream-pin-related, both captured under results/mirai/:
1. results/mirai/run-msrv.txt — rivet-core's rust-version=1.89
refused; the pinned nightly is rustc 1.86.0-nightly (2025-01-09).
2. results/mirai/run-let-chains.txt — even with
--ignore-rust-version, spar-annex (pulled via the spar external)
uses stabilized let_chains, gated as #![feature(let_chains)] on
any pre-mid-2025 nightly.
Verdict: hold the prototype until endorlabs/MIRAI bumps its
rust-toolchain.toml past let_chains stabilization (rustc ≥ 1.88,
nightly ≥ ~2025-04). At that point scripts/research/mirai-on-rivet-core.sh
is a one-shot resumption.
This is the intended exit per the prior triage's spike scope:
"if install fails, the spike output is itself the verdict." The
runner script is preserved in scripts/research/ so the experiment
resumes in minutes rather than hours when the upstream pin moves.
Refs: FEAT-001
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
⚠️ Performance Alert ⚠️
Possible performance regression was detected for benchmark 'Rivet Criterion Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.
| Benchmark suite | Current: 67fb0f0 | Previous: 08b87f8 | Ratio |
|---|---|---|---|
traceability_matrix/1000 |
61014 ns/iter (± 221) |
44661 ns/iter (± 159) |
1.37 |
query/10000 |
118545 ns/iter (± 693) |
92475 ns/iter (± 909) |
1.28 |
This comment was automatically generated by workflow using github-action-benchmark.
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Picks up the feasibility-spike sub-AC proposed in the 2026-04-26 triage comment on #191. The spike ran end-to-end this session and reached a clear negative verdict: MIRAI's pinned toolchain cannot build today's rivet-core. Two independent blockers, both upstream and both captured in committed artefacts under
results/mirai/.Status: ready for review as a spike report. Still draft because the natural next step (resume the prototype after upstream MIRAI bumps its nightly pin) is a follow-up; this PR's job is to record the procedure and the verdict.
Headline findings
facebookexperimental/MIRAIwas archived 2024-08-22; live fork isendorlabs/MIRAI(latest v1.1.12, 2025-03-04,nightly-2025-01-10).cargo install --locked --path ./checker(17m 40s on a 4-core box) +LD_LIBRARY_PATHpointing at the nightly'slib/dir for the rustc_driver linkage quirk.rivet-core/Cargo.tomldeclaresrust-version = "1.89"; cargo refuses against the MIRAI-pinnedrustc 1.86.0-nightly.--ignore-rust-version,spar-annex(via thesparexternal) uses stable-since-1.88let_chainssyntax that the pre-stabilization nightly rejects.rust-toolchain.tomlpastlet_chainsstabilization (rustc ≥ 1.88; nightly ≥ ~2025-04). At that point the runner script is a one-shot resumption.Acceptance — feasibility-spike sub-AC
docs/research/mirai-prototype-report.md§"Install procedure (validated)" + the script. Procedure works as a build pipeline; the toolchain pin is the upstream blocker, not the procedure.mirai-on-rivet-corescript inscripts/research/—scripts/research/mirai-on-rivet-core.sh, idempotent, supports--install-onlyand--target {store|proofs|all}.results/mirai/<target>.txt(committed) — three files committed:install-summary.txt,run-msrv.txt,run-let-chains.txt. They are the spike's output and capture the failure mode.Out of scope
Test plan
bash -n scripts/research/mirai-on-rivet-core.sh— syntax clean.rustup toolchain install nightly-2025-01-10 --component rustc-dev …— succeeded.git clone --depth 1 --branch v1.1.12 https://github.com/endorlabs/MIRAI.git— succeeded.cargo install --locked --path ./checker— succeeded in 17m 40s.cargo mirai --libagainstrivet-core— failed deterministically with the two captured errors. The failure is the spike's verdict.Note on the issue retarget
If the maintainer agrees with the Endor-Labs-fork substitution and the "hold" verdict, the issue body's MIRAI link and the parent V&V hub's #191 phase-5 row should be updated. Happy to file the edit as a follow-up.
🤖 Generated with Claude Code — issue-triage agent run 2026-05-07.