fix: check --json missing-file envelope and MPI hygiene (#1449)

## Summary

Multi-perspective improvement cycle (2026-08-02) on a clean main.

- **Agent JSON purity:** `assura check --json` on a missing path no
longer emits a bare diagnostic array. It uses the same report object as
a normal check (`diagnostics`, `file_info`, `layer`, `verification`)
with code `A01000`.
- **SMT:** Evolution unmodelable path uses
`VerificationResult::unknown_not_encoded` instead of an open-coded
limitation string.
- **Docs:** MASTER-PLAN recount (201,160 LOC / 5,781 tests / 31 demos /
6 MCP tools); error-codes index adds `A01000` and clarifies `A0510x`;
DESIGN closed-loop doc records `ir_verify` MCP + `assura ir --verify`.
- **Deps:** clap 4.6.5, rmcp 3.1.0.
- **Tests:** Integration coverage for the JSON envelope; stronger
if-encode unit asserts.

## Test plan

- [x] `cargo test -p assura --test cli_integration
check_missing_file_json_envelope --locked`
- [x] `cargo test -p assura-smt --lib evolution_ --locked`
- [x] `cargo test -p assura --lib if_encodes --locked` (subset)
- [x] `bash scripts/guards.sh`
- [x] Live: `assura --json check /nonexistent` returns object envelope
- [ ] CI green on this PR

## Follow-ups (not in this PR)

- #1448 rowan 0.16 → 0.17 major evaluation
- #1410 / #1411 human launch outreach
- #436 cvc5-rs upstream

---------

Signed-off-by: Sebastien Tardif <sebtardif@ncf.ca>

Author: SebTardif

Cargo.lock

@@ -1,12 +1,12 @@
 # Assura Development Status
 
-> 164,785 lines of Rust, 4,925 tests, **21 workspace members** (re-counted 2026-07-04 via `scripts/count-crates.sh`).
+> 201,160 lines of Rust, 5,781 tests, **21 workspace members** (re-counted 2026-08-02 via `scripts/count-crates.sh`).
 
 ## What Works Today
 
 | Capability | Status |
 |------------|--------|
-| Parse `.assura` contracts | 24 demos, 157 test fixtures |
+| Parse `.assura` contracts | 31 demos, 187 test fixtures |
 | Name resolution with stdlib prelude types | Done |
 | Type checking with 60+ checkers across all 50 spec features | Done |
 | Z3 verification of requires/ensures/invariant clauses | Done |
@@ -15,7 +15,7 @@
 | WASM codegen (`--target wasm`) | Done |
 | IR prompt generation for AI coding agents | Done |
 | IR parsing, structural validation, and SMT verification | Done |
-| MCP server (5 tools) | Done |
+| MCP server (6 tools: check, infer, explain, type_map, ir_prompt, ir_verify) | Done |
 | gRPC server with streaming verification (5 RPCs) | Done |
 | LSP server (hover, completion, go-to-def, symbols) | Done |
 | VS Code extension (TextMate grammar + LSP client) | Done |
@@ -36,28 +36,28 @@ Workspace members only (`Cargo.toml` `members = ["crates/*"]` with
 
 | Crate (package) | LOC | Tests | Role |
 |-----------------|-----|-------|------|
-| assura-parser | 9,597 | 188 | Lexer (logos) + recursive-descent parser (rowan CST), Pratt expressions |
-| assura-ast | 2,942 | 39 | Canonical AST, DeclVisitor, ExprVisitor, ExprFolder |
-| assura-resolve | 5,767 | 184 | Scope analysis, imports, stdlib prelude injection |
-| assura-types | 43,305 | 1,704 | 60+ checkers in CHECKER_PIPELINE, all 50 spec features |
-| assura-smt | 53,152 | 1,245 | Z3 + CVC5, Layer 2 verifier, prophecy/liveness/weak-memory, IR exec |
-| assura-codegen | 15,867 | 658 | Multi-file Rust projects, proptest gen, WASM, IR body substitution |
-| assura-pipeline | 2,103 | 66 | Canonical compile/compile_full/verify_typed/run_at |
+| assura-parser | 10,402 | 209 | Lexer (logos) + recursive-descent parser (rowan CST), Pratt expressions |
+| assura-ast | 3,162 | 46 | Canonical AST, DeclVisitor, ExprVisitor, ExprFolder |
+| assura-resolve | 6,095 | 189 | Scope analysis, imports, stdlib prelude injection |
+| assura-types | 44,727 | 1,750 | 60+ checkers in CHECKER_PIPELINE, all 50 spec features |
+| assura-smt | 59,594 | 1,348 | Z3 + CVC5, Layer 2 verifier, prophecy/liveness/weak-memory, IR exec |
+| assura-codegen | 16,706 | 670 | Multi-file Rust projects, proptest gen, WASM, IR body substitution |
+| assura-pipeline | 2,379 | 71 | Canonical compile/compile_full/verify_typed/run_at |
 | assura-config | 1,299 | 53 | assura.toml, VerifyOptions, CompilerConfig |
-| assura-diagnostics | 4,163 | 73 | Error codes, ariadne + JSON rendering |
-| assura (dir: assura-cli) | 12,910 | 283 | CLI binary: check, build, init, fmt, infer, … |
+| assura-diagnostics | 4,224 | 75 | Error codes, ariadne + JSON rendering |
+| assura (dir: assura-cli) | 38,774 | 937 | CLI binary: check, build, init, fmt, infer, check-rust, … |
 | assura-lsp | 1,965 | 55 | Language server (tower-lsp) |
 | assura-server | 809 | 27 | gRPC + HTTP/JSON API |
-| assura-mcp | 841 | 28 | MCP server for AI agent integration |
-| assura-fmt | 648 | 52 | Formatter |
-| assura-macros | 1,973 | 58 | Proc macros (`#[contract]`, `#[trust]`) |
+| assura-mcp | 865 | 28 | MCP server for AI agent integration |
+| assura-fmt | 741 | 53 | Formatter |
+| assura-macros | 1,974 | 58 | Proc macros (`#[contract]`, `#[trust]`) |
 | assura-stdlib | 409 | 18 | Stdlib modules (math, string, collections, …) |
 | assura-rust-analyzer | 2,514 | 92 | Syn-based Rust source parser for contract inference |
 | assura-test-support | 376 | 10 | Shared test helpers |
 | assura-bench | 421 | 0 | Criterion benchmarks |
 | assura-runtime | 262 | 10 | Runtime support for contracts |
 | assura-llm | 3,462 | 82 | LLM provider abstraction for auto-implement / suggest |
-| **Total** | **164,785** | **4,925** | |
+| **Total** | **201,160** | **5,781** | |
 
 `crates/assura-driver` is **excluded** from the workspace (exploratory rustc
 driver). Refresh counts with `bash scripts/count-crates.sh`.

MASTER-PLAN.md

@@ -103,9 +103,20 @@ pub(crate) fn run_check(opts: CheckOptions<'_>) {
 
     let (source, display_name) = read_source_arg(filename).unwrap_or_else(|e| {
         if output_mode == OutputMode::Json {
+            // Match the normal check --json envelope so agents can always
+            // parse `{diagnostics, file_info, ...}` (not a bare diag array).
             let diag = assura_diagnostics::Diagnostic::error("A01000", format!("{e}"), 0..0)
                 .with_file(filename);
-            println!("{}", serde_json::to_string_pretty(&[diag]).unwrap());
+            let report = serde_json::json!({
+                "diagnostics": [diag],
+                "file_info": {
+                    "file": filename,
+                    "success": false,
+                },
+                "layer": compiler_config.verify.layer,
+                "verification": [],
+            });
+            println!("{}", serde_json::to_string_pretty(&report).unwrap());
         } else {
             eprintln!("Error: {filename}: {e}");
         }

crates/assura-cli/src/check/run.rs

@@ -1932,14 +1932,16 @@ fn simple_nested_if_in_then() {
 
 #[test]
 fn unary_neg_if_encodes() {
-    let ir = try_ir_from_rust_body("U", &px(), Some("i64"), "-(if x > 0 { x } else { 1 })");
-    assert!(ir.is_some(), "unary if");
+    let ir = try_ir_from_rust_body("U", &px(), Some("i64"), "-(if x > 0 { x } else { 1 })")
+        .expect("unary if should encode");
+    assert!(ir.contains("then #") || ir.contains("neg"), "{ir}");
 }
 
 #[test]
 fn method_on_if_encodes() {
-    let ir = try_ir_from_rust_body("M", &px(), Some("i64"), "(if x > 0 { x } else { 1 }).abs()");
-    assert!(ir.is_some(), "method on if");
+    let ir = try_ir_from_rust_body("M", &px(), Some("i64"), "(if x > 0 { x } else { 1 }).abs()")
+        .expect("method on if should encode");
+    assert!(ir.contains("then #") || ir.contains("abs"), "{ir}");
 }
 
 #[test]
@@ -1963,8 +1965,9 @@ fn cast_of_if_encodes() {
         &px(),
         Some("i64"),
         "(if x > 0 { x } else { 0 }) as i64",
-    );
-    assert!(ir.is_some(), "cast of if");
+    )
+    .expect("cast of if should encode");
+    assert!(ir.contains("then #"), "{ir}");
 }
 
 #[test]
@@ -1984,8 +1987,9 @@ fn if_as_method_arg_encodes() {
         &pxy,
         Some("i64"),
         "x.saturating_add(if y > 0 { 1 } else { 0 })",
-    );
-    assert!(ir.is_some(), "if as method arg: {ir:?}");
+    )
+    .expect("if as method arg should encode");
+    assert!(ir.contains("then #") || ir.contains("add"), "{ir}");
 }
 
 #[test]

crates/assura-cli/src/check/rust_body_ir/tests.rs

@@ -2844,6 +2844,33 @@ fn check_watch_missing_path_json() {
     assert_eq!(v["watch"], true);
 }
 
+/// `check --json` on a missing file must use the same report envelope as a
+/// normal check (object with `diagnostics` / `file_info`), not a bare array.
+#[test]
+fn check_missing_file_json_envelope() {
+    let out = Command::new(assura_bin())
+        .args(["check", "/no/such/check/path.assura", "--json"])
+        .output()
+        .expect("failed to run assura check --json missing");
+    assert_eq!(
+        out.status.code(),
+        Some(2),
+        "missing path should exit 2: stdout={} stderr={}",
+        String::from_utf8_lossy(&out.stdout),
+        String::from_utf8_lossy(&out.stderr)
+    );
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    let v: serde_json::Value =
+        serde_json::from_str(&stdout).expect("missing path --json must be a JSON object");
+    assert!(v.is_object(), "expected object envelope, got: {stdout}");
+    assert_eq!(v["file_info"]["success"], false);
+    assert_eq!(v["file_info"]["file"], "/no/such/check/path.assura");
+    let diags = v["diagnostics"].as_array().expect("diagnostics array");
+    assert_eq!(diags.len(), 1);
+    assert_eq!(diags[0]["code"], "A01000");
+    assert!(v["verification"].is_array());
+}
+
 #[test]
 fn check_showcase_only_filters_by_header() {
     let tmp = unique_temp("assura_showcase_only");

crates/assura-cli/tests/cli_integration.rs

@@ -218,7 +218,7 @@ impl LlmProvider for MockProvider {
         Ok(serde_json::to_string(&serde_json::json!({
             "suggestions": []
         }))
-        .unwrap())
+        .expect("static JSON object always serializes"))
     }
 
     fn model_id(&self) -> &str {

crates/assura-llm/src/provider.rs

@@ -148,10 +148,7 @@ fn check_implication(
         let all_exprs: Vec<&&SpExpr> = antecedents.iter().chain(consequents.iter()).collect();
         for expr in &all_exprs {
             if expr_has_unmodelable_features(expr) {
-                return VerificationResult::Unknown {
-                    clause_desc: desc.to_string(),
-                    reason: "clause uses features not yet encoded in SMT".into(),
-                };
+                return VerificationResult::unknown_not_encoded(desc, "clause uses features");
             }
         }
 

crates/assura-smt/src/entry/evolution.rs

@@ -251,15 +251,14 @@ The pieces exist but are not connected:
 | JSON output | `VerificationSummary` | Works (JSON-serializable) |
 | IR prompt generation | `render_ir_prompt` / `ir_prompt_contexts_for_typed` | Works |
 | Heuristic IR generation | `ir_generate::generate_ir_sidecar_text` | Works (pattern detection) |
-| MCP server | `assura-mcp` (5 tools) | Works, but no IR verify tool |
+| MCP server | `assura-mcp` (6 tools) | Works: check, infer, explain, type_map, ir_prompt, **ir_verify** |
+| CLI IR + SMT | `assura ir --verify` / `--verify-only` | Works (requires `--contract`) |
 
-**Missing connections:**
+**Remaining gaps (not blocking the closed loop):**
 
-1. No MCP tool to submit IR text and get verification results
-2. `assura ir` command does not run SMT verification
-3. No counterexample-to-IR-slot mapping
-4. No structured repair hints
-5. No multi-turn protocol with progress tracking
+1. No counterexample-to-IR-slot mapping
+2. No structured repair hints beyond Unknown/CE reasons
+3. No multi-turn protocol with progress tracking
 
 ---
 

docs/DESIGN-AI-VERIFICATION-LOOP.md

@@ -26,7 +26,7 @@
 | A12xxx | types | assura-types | checks/concurrency.rs, checkers/security/ |
 | A13xxx | types | assura-types | checks/numeric.rs, domain/numeric.rs |
 | A31xxx | types | assura-types | checks/core.rs (liveness prove/fairness) |
-| A05 (impl) | smt+cli | assura-smt / assura-cli | `A05100` SMT inconclusive / limitation |
+| A05 (impl) | smt+cli | assura-smt / assura-cli | `A05100` CE, `A05101` timeout, `A05102` known limitation, `A05103` inconclusive |
 
 ## Codes from SPEC §7.2 (plus a few high-traffic impl codes)
 
@@ -104,8 +104,8 @@
 | A22003 | ? | ? | Unbounded allocation detected | No allocation bound proved | Complexity Bounds (A22xxx) | rg code in crates |
 | A05100 | smt+cli | assura-smt / assura-cli | SMT counterexample found (verification failed) | Fix the contract (real violation) | (impl) | check/report.rs |
 | A05101 | cli | assura-cli | SMT solver timed out | Increase `--timeout` | (impl) | check/report.rs |
-| A05102 | cli | assura-cli | Known compiler limitation (warning, exit 0) | No action needed | (impl) | check/report.rs |
-| A05103 | cli | assura-cli | Solver inconclusive (error, exit 1) | Simplify the contract | (impl) | check/report.rs |
+| A05102 | cli | assura-cli | Known compiler limitation (warning, exit 0; error under `--strict`) | Simplify ensures, add IR, or ignore until encoding lands | (impl) | check/report.rs |
+| A05103 | cli | assura-cli | Solver inconclusive (error, exit 1) | Simplify the contract or raise `--timeout` | (impl) | check/report.rs |
 | A10002 | types | assura-types | Match on unknown scrutinee without wildcard | (implementation; see CLI/SMT Unknown policy) | (impl) | checks/meta.rs (match exhaustiveness) |
 
 ## High-traffic implementation codes (not always in SPEC §7.2 table above)
@@ -115,6 +115,7 @@ this table over guessing the phase.
 
 | Code | Phase | Primary crate | Typical meaning | Start in tree |
 |------|-------|---------------|-----------------|---------------|
+| A01000 | cli/pipeline | assura-cli / assura-pipeline | Source file read/IO failure | check/run.rs, pipeline |
 | A02006 | resolve | assura-resolve | Duplicate import | imports.rs |
 | A02007 | resolve | assura-resolve | Unused import | unused.rs |
 | A02008 | resolve | assura-resolve | Invalid import path segment | imports.rs |