[P4suta]

Why

An owner needs an explicit execution window while retaining the proof campaign's inventory-derived safety cap.
A stopped container loses diagnostics and leaves the parent without individual harness names.
The prepared Kani image's readiness probe uses a different user and executable from the actual campaign.
Combined string, graph, and arithmetic proofs also need a checked correspondence to their production implementations.

Changes

Add proofs --window-seconds without extending the campaign safety cap or the installed owner limit.
Keep the existing full-inventory default and the 60-second limit for each harness.
Preserve stopped container diagnostics and identify every unvalidated production harness and rejecting probe.
Check the image's prepared standalone verifier and model checker versions through the same image user as the campaign.
Decompose the unfinished native obligations while retaining their declared input domains and properties.
The dependency decision checks every byte sequence up to 16 bytes and every Boolean classification input.
Bind the text projection, classification declarations, native postcondition, and arbitrary-input harness to their exact Rust source before and after every campaign.
Keep the eight text fixtures as complementary boundary evidence.
Partition the graph proof into zero, one, two, and three members with arbitrary parent values.
Compose the full-domain arithmetic helper and zero-input proofs with generated Lean coverage and minimality theorems.
Bind both refinements and their regressions to the verifier identity and compiled-source checks.
The proposed decision records identify the standard-library and verifier trust boundaries.

Validation

The normal project gate passes on the composed implementation, including strict workspace Clippy, all 113 real-Git workflow regressions, and 16 profile manifests.
The real Docker boundary test confirms memory and time limits and retained pre-stop diagnostics.
The prepared-image readiness regression verifies the actual standalone verifier and model checker versions.
The source-binding regressions reject changed conversions, constants, enum comparisons, domains, assumptions, shadowed identifiers, missing or duplicate obligations, and mid-run source changes.
The verifier identity regression checks every engine input.
The actual pinned Lean package builds with warnings refused, reports all 19 expected axiom sets, and passes fresh kernel replay for all six modules.
The immutable selected-source Kani campaign remains incomplete after the bounded container reached its 2 GiB memory limit within the 900-second owner window.
The parent names all 132 unvalidated selections and grants no accepted campaign or cache evidence.
An earlier manually stopped attempt also supplies no accepted evidence.
The complete native release campaign remains unrun.
The selected-module completion, cache replay, and complete campaign acceptance remain open in #354.

Closes #440.

Related to #354.

@coderabbitai ignore

[P4suta]

The scoped native runtime rollout completed from merged commit 6d70aa8ffadaaed23a75f28100d535fa74dbc150 on macOS, Linux, and Windows.
At each rollout check, the installed runtime and PR workflow reported source hash acb22ad1b07e346252f28552abcde9a379e6397c49516efc9148328f1cb81911.
The Mac installation uses a separate clean checkout to preserve unrelated owner work in progress.
The native owner maps keep their existing local entries.
The normal source-update hooks on Linux and Windows refuse PR-skill redeployment because unrelated installed managed skills differ from their recorded catalog.
The refusal preserves those skills before any replacement.
Direct source comparisons confirm that the installed PR skill already matches the reviewed source on all three hosts.
The scoped runtime installation completes independently.

Each installed Git guard accepted the saved dependency report through its installed companion for committed source 05ce0eaf073ec6b0f024438ec7ea112f5e5d50d9 during that verification.
Each report probe validated 134 selected candidates with zero nonfatal report notices.
This establishes source attribution and installed pairing rather than current dependency freshness.
The native job runner also reports retained-trash cleanup refusals, which remain separate from the successful report probes.

The final Mac inspection found different runtime and PR workflow binaries from the checkout containing unrelated work in progress.
They report revision e901cb39e364842a3bf55bc39cfe5b5829a009d2 and source hash fc76bfcf3b1c21d941578c308bd533f41b887893042d2a39baca782ffc991baa.
The completed rollout checks don't verify this replacement.
The unrelated work remains preserved, and current Mac runtime acceptance remains pending.

The selected Kani campaign remains incomplete and supplies no completed campaign or cache evidence.
The remaining acceptance stays open in #354, #355, and #216.
The full native mutation campaign and repository-wide consumer audit also remain pending in #195 and #121.