The unconditional checks CI job checks proof-review.json, including when content selection skips the expensive .NET and formal jobs. The record binds reviewed implementation, conformance evidence, proofs, generated kernels, verifier/solver pins, build targets and proof tooling to their exact text content. A changed input fails until its review record is updated. This is an enforceable freshness requirement, not an attestation of reviewer identity or judgment, an automated C# refinement proof, or a storage qualification receipt.
check-proof-review.ps1 defines two mandatory boundaries:
implementation includes the mapped journal, replacement, descriptor, range/read and lifecycle sources. It also discovers generated verification sources and textual calls to the shipped kernels listed in Get-NativeKernelNames and their BinaryBuffer/StreamRead adapters. Cited conformance evidence is hashed with the source.proof-trust includes every Dafny source, the exact proof/dependency inventory, Dafny and bundled-Z3 pins, executable projection and audit policy, their regression tests, required CI lane, compiler/runtime targets and the documented model/storage boundary.The production source-name inventory is recorded independently of source contents. Adding, deleting or moving any library C# source, including hidden files, requires a classification review, even when it does not call a kernel. A new kernel or explicit adapter caller must also be added to the implementation input set. Changes to unrelated existing C# file contents do not require a proof receipt update. The inventory detects changes in names; source inspection determines whether a new helper must join the explicit mapped-source set. Aliases, indirection and handwritten operations are not a machine-checked call graph.
Hashes use UTF-8 text with CRLF normalized to LF. Input paths are repository-relative and case-sensitive; duplicates, escaping paths, missing inputs and omitted new proof sources refuse. Evidence references must exist locally and are included in the checked content set. The receipt does not hash itself.
This policy is the continuing maintenance obligation for proof claims and their evidence. It applies whenever a change affects a behavior in the scope inventory, its evidence and remaining obligations, or a trusted contract. Review is required even when the edited file is outside the receipt’s explicit inputs. The freshness gate detects its declared content and source-name changes; it does not discover every semantic dependency, verify specification adequacy or establish reviewer judgment. An unchanged theorem name or a passing receipt is insufficient reason to skip review.
The person preparing a change identifies the affected inventory entries and evidence-map rows before integration. The integrator reviews the settled diff, its evidence and the resulting claim. Record durable contracts, scope decisions and evidence in the design/proof documentation and review receipt; record the change itself in its commit. Keep concrete unfinished work in the root plan. Continuing maintenance does not need a permanently open plan checkbox.
| Trigger | Required review and evidence | Acceptance before integration or claim promotion |
|---|---|---|
| Mapped production code, effect adapters, exception/cancellation handling, or a new, moved or deleted production source | Review entry preconditions, supported success/refusal behavior, effect sequencing and actual returned outcomes, ownership/generation authority, bounds/resource lifetime and progress. Classify alternate, fallback, failure and retry paths against the inventory, including changes reached through an unlisted helper. Update the mapping, conformance evidence and explicit remaining contracts. | Exact review inputs and source-name inventory are current after source inspection; focused production regressions cover affected transitions and refusal classes; the settled-main CI gates pass. A manual mapping or tested trace retains that evidence level until executable verification or machine-checked refinement covers it. |
| A specification, proof, native representation, fault relation, resource bound, precondition, or scope exclusion changes | Reassess the stated property and the composition with callers/callees. Check reachable initial states, satisfiable preconditions and independently described supported success and refusal examples. Inspect witnesses, counterexamples and negative mutation controls. Check repeated interruptions and separate eventual progress under eventually successful exclusive effects from safety under failed effects. Explain any narrowed scope and retain displaced implementation, compatibility and platform obligations as concrete open work. | No stronger precondition, broad refusal or unreachable success case silently removes required behavior. Every proof and normal-source dependency remains in the exact manifest; the pinned verifier, audit, negative controls and generated freshness pass when proof/generated-source/tooling changes require them. Existing independent format and production evidence remains applicable. |
| Dafny, Z3, verifier/solver pins, source policy, compiler projection, C# compiler/SDK or relevant build options change | Review upstream provenance, versions, platform asset/digest changes, generated method bodies, accepted language/translation constructs and compiler/runtime assumptions. For verifier-distribution updates, use fresh external installations and qualify Windows and Linux as required by the tool update policy. Review the solver, normal-source dependencies, audit and negative controls together. | Changed proof tooling passes verification, audit, both negative controls and exact generated freshness; relevant focused tooling tests pass. All shipping targets and mandatory analyzer, test, trimming/NativeAOT and package gates still pass with unchanged shipping dependency/runtime requirements. A toolchain upgrade alone does not prove compiler correctness. |
| A deployed .NET runtime/BCL, OS, filesystem/device, I/O implementation or coordination contract changes | Review the affected API implementation/source and qualification evidence against exact bytes/length effects, partial/failed outcomes, flush fences, restart quiescence, namespace discovery/persistence, canonical identity and cooperative exclusion. Revisit the storage contract, caller-stream capabilities and platform scope. | Named platform claims are supported by applicable evidence; otherwise retain the scoped limitation and explicit E4/F6/I15/V7 work. Process kills, synthetic namespace loss and content flush success do not qualify physical power-loss durability or directory persistence. Evidence for one OS/filesystem/device combination does not qualify another. |
| A native format interpretation, supported form, expression/collation rule, malformed-input classification, corpus fixture or fixture hash changes | Record provenance, producing engine/version, immutable hashes and expected values. Compare actual Microsoft-authored or native-accepted controls, including independently described success/refusal cases, with parser/writer behavior. Revisit bounds, error policy and preservation/reclamation assumptions that depend on the interpretation. | Focused regression and applicable DAO read/write/compact checks support the changed behavior. Golden-byte changes receive independent native review before approval. Distinguish Microsoft evidence, independent implementations, library round trips and synthetic mutations; missing engines/fixtures remain gaps, and guarded skips do not establish interoperability. |
| Conformance/native/platform evidence is removed, replaced, weakened or found invalid; an inventory entry or evidence link changes | Recheck the exact properties and paths the evidence supported, including alternate/fallback paths and fault cases. Update the evidence map and claims together; preserve useful refusing traces and diagnostics. Reassess assumptions that depended on the invalidated observation. | Every retained claim has current supporting evidence of the stated kind. Unresolved gaps have self-contained plan items with cause, dependencies and acceptance conditions; deleting a test or receipt does not discharge the obligation. |
| README, API or design wording introduces or broadens a guarantee | Trace the exact advertised surface, native forms, property, fault model and platform scope through the inventory and evidence map. Separate executable verification, abstract-only proofs, manual correspondence, tested production behavior and qualified physical durability. Review composition and residual trust, including specification/verifier soundness and effect/crypto/compiler assumptions. | Promote only the exact supported claim after its implementation and platform criteria hold. Keep format/expression/native-compatibility statuses Partial until E1/E2 and feature evidence establish the stronger claim. Isolated kernels, proof volume, successful hashes and pending CI do not justify complete-path or whole-library guarantees. |
main SHA; report the run URL, SHA and completed verdict. Native and platform checks remain independent requirements when their named behavior changes. Pending jobs and guarded skips are not successful evidence.PLAN.md.Reconsider F* only for a concrete production boundary where its extraction or trust tradeoff could improve on the existing Dafny approach. Record the boundary, current unresolved obligation, proposed executable/refinement path, effect adapters, added trust and maintenance cost, and the evidence that would demonstrate improvement. Compare against extending the current verified boundary before adding another representation or protocol. Retain Dafny when no concrete benefit is established. Verification-only F* remains possible, but any choice must preserve the managed shipping targets, runtime requirements and dependency graph; considering an alternative does not permit unchecked contracts or weaken the existing gates. Record a justified future decision in durable design documentation rather than maintaining an indefinite plan checkbox.
Before changing hashes, inspect the source diff and update the affected boundary’s concrete obligations, conformance and remainingAssumptions explanation. Keep the boundary and production correspondence consistent.
For mapped storage or lifecycle code, review admission before effects, journal/database flush ordering, uncertain outcomes, lease/receipt authority, cleanup ownership, conditional replay markers, generation invalidation and snapshot/savepoint behavior as relevant. State which executable decisions are proved, which production traces were exercised, and which returned-I/O or namespace effects remain contracts. Add or change the exact conformance evidence paths rather than treating successful arithmetic proofs as validation of handwritten loops.
For a verifier, solver, compiler pin or trust-tooling update, inspect upstream provenance and the version/asset/digest changes. Review the policy, compiler projection, normal-source dependencies, negative controls and platform execution evidence together. Reinstall changed verifier distributions into fresh external directories and run verification, audit, both negative controls and generated freshness; qualify Windows and Linux distributions as required by the tool update policy. A hash update alone does not satisfy that policy.
The reviewed projection’s three controller inlining annotations are an explicit target-metadata transformation. Review its exact-signature matcher, fixed BCL attribute and unchanged generated bodies together. Raw runtime references or source-emitted inlining metadata still refuse; the two named long-value controllers and the byte-batch usage-map controller are the only recipients. Recovery and other array-loop methods receive no hints. Compiler/JIT/AOT behavior remains trusted, and the hint’s advisory timing effect requires hosted controls alongside the ordinary proof/build gates.
Record only the reviewed final input hashes and current production-name inventory digest. There is intentionally no blanket accept or receipt-refresh mode in the gate. Existing Get-ProofReviewHash, Get-ProofReviewInputs and Get-ProofReviewInventoryHash functions provide deterministic calculations; using them to calculate a hash does not perform the required review. Do not mark pending hosted checks as successful in the committed explanation.
Run a focused development check in a fresh external directory:
pwsh -NoProfile -File scripts/check-proof-review.ps1 `
-OutputDirectory (Join-Path ([IO.Path]::GetTempPath()) ('jdw-review-' + [guid]::NewGuid().ToString('N')))
pwsh -NoProfile -File scripts/tests/proof-review.tests.ps1
pwsh -NoProfile -File scripts/tests/verify-proofs.tests.ps1
pwsh -NoProfile -File scripts/tests/formal-workflow.tests.ps1
The ordinary settled-main CI gate remains required. Review receipts supplement the existing proof, analyzer, framework, trimming/NativeAOT and interoperability gates.
The proof-trust-review artifact retains review.json with the review-freshness verdict, including the refusing input or inventory mismatch. The formal-verification artifact retains verifier/auditor stdout and stderr, audit reports, exact expected-negative-control sources, and per-process JSON with command arguments, exit status and timeout/launch failure details. Both artifacts have 30-day retention and upload after failed gates. Cancellation and hosting service failures can still prevent artifact upload.
A genuine proof-gate failure additionally emits failure.json, recording the failure, hosted SHA when available, input hashes and retained diagnostics. Its inputs/ directory copies regular local proof and normal-source dependency files, proof/tool manifests, verifier scripts and generated kernels needed to inspect that failed attempt. Linked files and paths through linked directories are refused without copying their targets; refused or failed snapshots are recorded separately. If receipt retention itself fails, failure-receipt.error.txt records the supplemental error where possible and the original verifier failure remains the reported failure. An incomplete attempt never emits a successful summary.json. Existing result directories refuse reuse, preserving earlier failures for comparison.
The deliberately false theorem must fail verification, and the assumed theorem must trigger audit rejection. Their failure output is expected evidence that the controls work; those files remain external to the admitted proof inventory. A failure.json describes a real gate failure and explicitly distinguishes it from these expected controls. Checked counterexample lemmas in the admitted models remain ordinary proved sources and receive the same review and freshness checks as positive properties.