Stage 4 checked EPR reconstruction

.design/basis/09-option-result.md

@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 7b575ed2f4bd06939345f719add8203a17ba950cfed98c54afcccfaf4f972d8d (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 46202bede5f263fcedce4791f1994cb1c74efc06c9016b3115239deec7653cd3 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/ast.rs
 governs: thermite-syntax/src/parser.rs
 governs: thermite-spec/src/validator.rs
@@ -15,6 +15,10 @@ thesis-refs:
   - thermite-design.md §6
 -->
 
+> **Gate G4 re-audit (2026-07-29).** Stage 4 adds automatic clause routing in
+> `forge/src/check.rs`; the Option/Result syntax, validation, and lowering
+> contracts in this document are unchanged.
+
 ## Summary
 
 Cluster **C7** (crosslink **#95**) adds the two foundational error-handling

.design/basis/11-ergonomics.md

@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 7b575ed2f4bd06939345f719add8203a17ba950cfed98c54afcccfaf4f972d8d (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 46202bede5f263fcedce4791f1994cb1c74efc06c9016b3115239deec7653cd3 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/parser.rs
 governs: thermite-syntax/src/ast.rs
 governs: thermite-lower/src/lower.rs
@@ -12,6 +12,10 @@ thesis-refs:
   - thermite-design.md §2.3
 -->
 
+> **Gate G4 re-audit (2026-07-29).** The new automatic reconstruction overlay in
+> `forge/src/check.rs` is downstream of parsing and lowering. It does not change
+> any C10 desugaring or proof obligation.
+
 ## Summary
 
 C10 adds five binding/control-flow ergonomics that AI agents reach for

.design/basis/12-mutual-recursion.md

@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: aa6746d229f9a7270ad26aa17cf3184850b7ef2ae764bd5820a24d7b044f320b (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 3158984f966b99063a28ce692db077fbdde6e4b6bc4a1969ae56d4a1dac282a6 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 governs: thermite-lower/src/lower.rs
 thesis-refs:
@@ -12,6 +12,9 @@ thesis-refs:
   - thermite-design.md §7
 -->
 
+> **Gate G4 re-audit (2026-07-29).** Stage 4 changes the post-check proof routing
+> only. Mutual-recursion admission, decreases checks, and lowering are unchanged.
+
 ## Summary
 
 This cluster (crosslink #113) COMPLETES the deferral pinned in

.design/forge/audit-manifest.md

@@ -3,7 +3,7 @@
 tier: 3-component
 status: draft
 audited-sha: 1cc9d97c6c5d7eab6109561834db77f2ef4b57ab (re-pinned 2026-06-16: forge workflow status rows now render from canonical registry IDs; behavior unchanged; RFC #17)  (prior: 488103d4382815b85141d17bc01b60917ba744e7 (#274 — lean_fragment membership report; REQ-7..10 SHIPPED, audit.rs verified-current))
-audited-content-sha256: 3d6979af1e56a8ecc1f6964fc27da1b2869e1b2cc8502f1cda4d19c9ce58e4aa
+audited-content-sha256: f07b4f4149f471a3c37d5443a6e1178e3e7deec4845c9941a327a9aa5f65150f
 governs: forge/src/audit.rs
 thesis-refs:
   - thermite-design.md §6
@@ -28,17 +28,16 @@ trust statement whose centerpiece is the **enumerable trusted computing base**
 the toolchain identity. `grep slag` over a codebase and the audit manifest's TCB
 section are the same complete inventory of fiat-trusted code (§8).
 
-This is **greenfield**: there is no `forge audit` command, no `forge/src/audit.rs`,
-and no aggregate `AuditManifest` schema in `forge` today (verified below — the
-only existing aggregate, `AssuranceManifest`, is a render-time level/scope
-headline, not the §6/§9 audit deliverable). ALL the underlying per-fn data ships
-(it is this component's *input*, never re-derived). REQ-1..REQ-6 are **SHIPPED**
-(`forge/src/audit.rs` + the `forge audit` verb in `cli.rs`), verified by
-`forge/tests/audit_conformance.rs` against `conformance/audit/cases.json`;
-tracked by **crosslink issue #15** (v0.3, milestone #3 Battery). The **#274
-amendment** adds the LEAN-FRAGMENT MEMBERSHIP REPORT (REQ-7..REQ-10, all
-**NOT-STARTED**, blocker #274) — a per-function, informational section answering:
-would `--engine lean` attempt this fn, and if not, what is the structured refusal.
+The command and v1 schema are shipped in `forge/src/audit.rs`. The manifest
+aggregates existing per-function certificates; it does not recompute their
+verdicts. REQ-1..REQ-10 are covered by the conformance cases and the Lean
+fragment probe described below.
+
+Gate G4 adds one backward-compatible residual-trust field:
+`residual_trust.s2_relation_array_residuals`. It is zero for the admitted S₂.0
+relation/array surface. The accompanying `unsupported_fragments` list now names
+only genuine boundaries: formulas rejected by the S₂.0 classifier and
+quantifier-free leaves outside the checked QF_LIA/QF_BV source surface.
 
 ## Decided scope
 

.design/forge/check.md

@@ -3,7 +3,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 7158542241ba3b8ca86da4db7fb43ceee2f6c22a91177671bb5ea5b3b2f8450b (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 1d510c2fa2abf3818702f3908d8b13066e318dc80d12d45d5c069f971fe21d62 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 thesis-refs:
   - thermite-design.md §5.1
@@ -105,6 +105,21 @@ REQ status table).
 > property are both unchanged — only the source of `<stem>` moved. Pin:
 > `forge/tests/divergence_harness_names_checked_item.rs`.
 
+> **Amendment 2026-07-29 (Gate G4 automatic reconstruction).**
+> The normal CLI path selects `EngineSelection::Auto`. After the ordinary
+> Verus/Lean pass, routing is per clause: `@bvN` clauses take the checked
+> bit-vector path and admitted S₂.0 relation/array clauses take EPR
+> reconstruction through the canonical `S2Recon` bridge. A successful Lean
+> replay upgrades that clause to L4. A false clause returns a checked finite
+> countermodel; timeouts, missing tools, and reconstruction failures remain
+> named failures. `--engine verus` is the explicit legacy diagnostic path.
+> Programmatic `check_file` and `CheckOptions::default` remain the legacy
+> Verus-only entries for callers that require byte-stable certificates.
+> Result-bearing clauses are classified after substituting the source body
+> through nested call and method expressions. If that grounded body is outside
+> S₂.0, the ordinary verifier certificate is retained; EPR must not invent an
+> unconstrained `result` value.
+
 The stages, in order, are:
 
 ```

.design/forge/cli.md

@@ -4,7 +4,7 @@
 tier: 3-component
 status: shipped
 audited-sha: 5ae0816c042debb01c70eb9b89c775837f0c0f24 (content-sha256 re-pinned 2026-06-23 for stage-3 REQ-7 / AC-8 (#349), the automated Rust→Lean obligation exporter: the change to this doc's governed file (cli.rs) is the additive `forge smt-export [<file>] [--out <path>]` subcommand (`Command::SmtExport` → `run_smt_export`, emitting the `(P_prod) ⟺ (P_ref)` `by smt` Lean theorems + `#print axioms` probes via `lean_smt_export.rs`); every other subcommand + flag parse is unchanged. The legacy commit pin stays at the 5ae0816c stable-main ancestor; only the active content-sha256 digest moves. prior: 2026-06-21 stage-2 REQ-8 / AC-8 (#330) `forge strat-faithful-tv`; 2026-06-20 stage-2 REQ-4 / AC-4 (#326) `forge strat-tv` + `ForgeError::StratDifferential`; 2026-06-18 umbrella REQ-2c / AC-4 rotating-seed `--seed` flag on `forge tv`; §6 metrics dashboard `--metrics` value)
-audited-content-sha256: 19ee007ec4e8bfdaed609662ab91486543b0ce3be348a40ddc1a77f3d48d9cce
+audited-content-sha256: f5fda77ede58ab4a768d552e6946a26f8048f51c372c8ac9b54b5c71b9961cdb
 governs: forge/src/cli.rs
 thesis-refs:
   - thermite-design.md §5
@@ -62,6 +62,10 @@ What the old doc never saw, grouped (each verb cites its issue in the code):
   clause. QF_LIA uses `smt`; `@bvN` clauses use literal `BitVec N` terms and
   kernel-checked normalization lemmas. With no file, the command emits the canonical
   demo batch.
+- **Gate G4 automatic reconstruction** — plain `forge check` now selects
+  `EngineSelection::Auto`. The ordinary backend pass is followed by per-clause
+  checked BV and EPR reconstruction when the source clause is eligible.
+  `--engine verus` retains the legacy byte-identical diagnostic path.
 
 ## Requirements
 
@@ -174,7 +178,8 @@ What the old doc never saw, grouped (each verb cites its issue in the code):
 - AC-5: `ForgeError` wrapping round-trips inner diagnostics
   (`aggregation_preserves_inner_diagnostics`) and every variant maps to
   `EXIT_ENVIRONMENT` (`errors_map_to_environment_exit_code`).
-- AC-6: `--engine verus` is byte-identical to the default path
+- AC-6: `--engine verus` is byte-identical to the legacy Verus path; the
+  no-flag CLI path now selects automatic routing
   (`engine_verus_flag_is_byte_identical_oracle` in
   `forge/tests/engine_attribution.rs`); a Proven ⊕ witnessed-Refuted
   disagreement halts (`proven_refuted_disagreement_halts` in `engine.rs`
@@ -261,7 +266,7 @@ a reader cannot mistake it for an oracle field.
 | REQ-5 (typed exit codes) | SHIPPED | `pub const EXIT_VERIFICATION_FAILURE: u8 = 1` / `EXIT_ENVIRONMENT: u8 = 2` in `cli.rs`; `run_check`/`run_audit` gate on `matches!(.., ProjectAssurance::Certified(_))`; `run_repair` on `report.all_upgraded()`; the TV trio on `counts.divergent == 0`; `fn exit_code in cli.rs` maps every `ForgeError` to `EXIT_ENVIRONMENT`. Verification: `errors_map_to_environment_exit_code`, `broken_contract_is_reported_failure_with_counterexample` (exit 1), `divergence_audit_check2_exit_swallow.rs` (the TV exit discipline). |
 | REQ-6 (no panics; Result discipline) | SHIPPED | every `run_*`/`parse_args` path returns `Result<_, ForgeError>`; no `unwrap`/`expect`/`panic!` outside `#[cfg(test)]` in `cli.rs`. Verification: clippy `-D warnings` + the anti-pattern gate in the gauntlet (HEAD commit `93d3cbc0` chain is gauntlet-green). |
 | REQ-7 (`forge new` scaffold) | SHIPPED | `pub fn scaffold_project in cli.rs` writes `forge.toml`/`forge.lock` (`seed = {DEFAULT_SOLVER_SEED}`)/`THERMITE.skill.pin`; non-empty target → `ForgeError::Usage("… refusing to overwrite")`. Non-test consumer: `fn dispatch` (`Command::New` arm). Verification: `scaffold_writes_layout_and_refuses_clobber`. |
-| REQ-8 (`check` flags + engine routing) | SHIPPED | `Command::Check { file, json, level, rlimit, mutation_floor, engine }`; `fn run_check` four-way route: default → `check::check_file` (cache-canonical), explicit options → `check::check_file_with_options`, `(CheckLevel::L3, sel)` lean/auto → `check::check_file_with_engine` (REQ-5 disagreement → `ForgeError::SoundnessAlarm`), `(CheckLevel::L2, _)` → `check::check_l2_file`. Verification: `parses_rlimit_flag`/`parses_mutation_floor_flag`/`parses_level_flag`, `engine_flag_parsing` + `engine_verus_flag_is_byte_identical_oracle` (`engine_attribution.rs`), `proven_refuted_disagreement_halts` (`engine.rs`). |
+| REQ-8 (`check` flags + engine routing) | SHIPPED | `Command::Check { file, json, level, rlimit, mutation_floor, engine }`; the parser defaults `engine` to `Auto`, and `fn run_check` sends normal L3 checks through `check_file_with_engine` for per-clause BV/EPR routing. Explicit `--engine verus` uses the byte-stable legacy entries; `(CheckLevel::L2, _)` uses `check_l2_file`. Verification: the flag parser tests, `engine_verus_flag_is_byte_identical_oracle`, automatic-route tests, and the engine disagreement halt. |
 | REQ-9 (usage-banner currency, #257) | SHIPPED | `fn usage_text in cli.rs` names all 14 verbs and the full flag surface including `[--engine verus|lean|auto]` — added by commit `6368550a` ("forge usage banner gains [--engine verus|lean|auto] (drift fix)"). Non-test consumer: `parse_args`'s no-verb and unknown-verb arms. Verification: `usage_errors` exercises both arms; `l2_check.rs` checks the banner rejects a bogus `--level`. |
 | REQ-10 (project assurance display, #10) | SHIPPED | `fn render_assurance in cli.rs` prints per-fn `lowered-assurance:` lines + the `project assurance:` headline; `run_check` computes `AssuranceManifest::aggregate(&certs)` once for both the display and the exit gate. Verification: `render_assurance_shows_headline_and_lowered_flags`, `render_assurance_shows_failed_headline`. |
 

.design/lower/boundary-composition.md

@@ -2,14 +2,18 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: aa6746d229f9a7270ad26aa17cf3184850b7ef2ae764bd5820a24d7b044f320b (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 3158984f966b99063a28ce692db077fbdde6e4b6bc4a1969ae56d4a1dac282a6 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-lower/src/lower.rs, forge/src/check.rs
 thesis-refs:
   - thermite-design.md §9
   - thermite-design.md §8
   - thermite-design.md §6
 -->
 
+> **Gate G4 re-audit (2026-07-29).** Automatic BV/EPR reconstruction is an
+> additive per-clause overlay after the ordinary check. Boundary/slag weaving
+> and verify-through-the-contract semantics remain unchanged.
+
 ## Summary
 
 `thermite-design.md` §9 promises composition: "if `g` calls `f` only through