Make command coverage execution-backed

BACKLOG.md

@@ -48,11 +48,10 @@ records, generated release manifests, or the owning docs named above.
 
 | Status | ID | Scope | Completion condition |
 |---|---|---|---|
-| NEXT | COVERAGE-01 | Replace command proof-route candidates with an owner-admitted executable oracle ledger; static route records are explicitly non-semantic. | `CommandCoverageInventory` consumes a separate execution-backed owner ledger whose rows bind `commandRef`, selector, concrete falsification event, assertion oracle, expected public outcome, and owner invariant; an independently authored versioned counterfeit corpus covers every shipped policy, evidence class, identity coordinate, and single or correlated substitution axis with positive controls and exact expected decisions; until then route metadata, prose, legacy source markers, test existence, and failure-capable AST nodes emit only declared routes or `proof_route_candidate`, candidate-route closure remains blocking, and semantic execution evidence remains an explicit non-claim. |
 | NEXT | COMPACT-01 | Replace compact proof caller labels and synthetic counts with an honest declaration-only schema/profile. | One atomic schema/profile cutover prefixes caller-owned proof and mutation fields with `declared`, removes checked/finding counts without independent evidence owners, rejects collapsed witness roles, updates every compact producer and consumer, and proves exact role and round-trip closure without claiming execution or assurance. |
 | NEXT | SOURCE-MODEL-01 | Define one representation-neutral typed requirement-source v2 model before selecting a source syntax. | A private bounded model admits atomic requirement identities, grouped authoring, premises, scenarios, definitions, vocabulary, lifecycle, references, and deterministic normalization; an independently authored field/variant completeness manifest plus mutant corpus proves every normative field reaches each required downstream owner, with no production parser or persisted normalized mirror. |
 | BLOCKED | SOURCE-CODEC-01 | Select at most one compact source codec without creating dual authority. | After `SOURCE-MODEL-01`, one versioned experiment manifest freezes disjoint role sets: the flat-v1 baseline control, grouped-model ablations, and exactly complete grouped-JSON plus at most one complete restricted-DSL codec candidate over the same model. Only codec candidates can win the predeclared replacement relation; controls and ablations measure causality and cannot become production grammars. A newly discovered candidate requires a new manifest version and complete experiment. A frozen corpus and strict `Replace(candidate, grouped-json)` predicate cover grammar completeness, safety, semantic parity, diagnostics, canonical bytes, review accuracy, token cost, diff amplification, parse/format cost, and unknowns. Every metric is classified exactly once by a versioned registry with role, direction, baseline pair, aggregation, material threshold, primary decision requirement, and missing-observation semantics; duplicate or unclassified metrics fail admission, hard constraints cannot trade off, report-only metrics cannot decide replacement, promised byte/token reductions must be materially better, and bounded diff/parse costs must be noninferior. If grouped JSON fails its hard gate, retain the current flat v1 source and perform no v2 cutover; otherwise select the restricted text candidate only when it is the unique strict replacement, while a tie, unknown, incomparability, or non-material improvement selects grouped JSON. The losing parser and formatter are deleted before experiment closeout, and production admits exactly one grammar. |
-| BLOCKED | SOURCE-CUTOVER-01 | Migrate self-hosted requirement sources only after one codec, the typed v2 model, nested structural contracts, and the complete evidence counterfeit corpus pass their gates. | `COVERAGE-01` and `SCHEMA-01` are complete; a digest-bound clause ledger proves representation-only equality or owner-reviewed semantic decomposition for every legacy requirement; all bindings/scenarios/contracts/context/diff/graph/browser owners cut over atomically; v1 admission and the losing codec are removed; and active-v1 inventory is zero. |
+| BLOCKED | SOURCE-CUTOVER-01 | Migrate self-hosted requirement sources only after one codec, the typed v2 model, nested structural contracts, and the complete evidence counterfeit corpus pass their gates. | The `REQ-PROOFKIT-QUALITY-010` execution-backed command-oracle closure and `SCHEMA-01` are complete; a digest-bound clause ledger proves representation-only equality or owner-reviewed semantic decomposition for every legacy requirement; all bindings/scenarios/contracts/context/diff/graph/browser owners cut over atomically; v1 admission and the losing codec are removed; and active-v1 inventory is zero. |
 | BLOCKED | SCHEMA-01 | Replace root-shape-only public contracts with one independent complete nested structural-contract owner. | A versioned schema owner covers nested fields, variants, cardinalities, bounds, enums, defaults, duplicate and unknown-field policy, and cross-field constraints; generated artifacts pass parity against an independently authored completeness manifest and mutant corpus without becoming semantic or policy authority. |
 | BLOCKED | SOURCE-PILOT-01 | Validate the selected source-v2 model and agent routing against heterogeneous external repositories without mutating them. | At least two independent repository classes complete no-push dual runs whose frozen inputs compare incumbent and candidate mapping, diagnostics, token cost, authoring accuracy, proof-route gaps, and rollback; unresolved parity or authority gaps keep incumbent owners active. |
 | BLOCKED | GOVERNANCE-01 | Evaluate a generic explicit-inventory governance-observation command without promoting one consumer's policy into Proofkit; detailed candidate contract is retained in [issue #64](https://github.com/research-engineering/agentic-proofkit/issues/64). | A sanitized reproducible fixture detects one named failure without classifying its false-positive counterexample, existing owners are proven insufficient, and either a second independent consumer reproduces the predicate or the owner admits recurring first-consumer cost; otherwise retire the candidate. |

docs/proofkit-contract-map.md

@@ -46,7 +46,7 @@ owner boundaries. It is not a second command-family inventory.
 | Selective planning | `changed-path-set`, `requirement-impact-input-compose`, `impact`, `selective-gate-plan`, `selective-gate-evidence`, `selective-gate-obligation-decision-input`, `proof-obligation-algebra`, `obligation-decision` | changed paths, base/current requirement sources, base/current single-binding-per-requirement proof contracts, generated-artifact policy, local environment policy, proof-like path policy, scan obligation ownership, planned receipts, obligation routes, obligation algebra records | fail-closed impact input composition, fail-closed planning, receipt comparison, obligation algebra admission, bounded agent packets | git diff truth, repository scanning, command execution, producer trust, final admission | composed impact input, plan, evidence report, obligation algebra report, or obligation input |
 | Receipts and producers | `proof-receipt-admission`, `receipt-producer-admission`, `receipt-currentness-scope`, `receipt-trust-class`, `producer-policy-self-proof` | receipt sets, producer policy, scope/currentness facts, trust classes | receipt shape, producer/receipt compatibility, self-proof diagnostics | producer authentication, freshness policy, CI trust roots | receipt/provenance report |
 | Release and deployment | `release-authority`, `external-consumer`, `registry-consumer-proof-input-compose`, `registry-consumer`, `deployment-evidence-admission`, `completion-criteria`, `branch-authority`, `readiness-closeout` | package facts, tarball/registry facts, explicit primitive registry/install/smoke facts, deployment evidence, criteria, branch facts | artifact/channel boundary checks, registry-consumer input composition, release diagnostics, falsifiable criteria shape | package publication, registry fetch, package-manager execution, deployment, rollback, approval | composed input, release/deployment/readiness report |
-| Supply-chain and quality | `self-check`, release workflow, `npm run release:sbom`, `npm run self:coverage`, `npm run go:actionlint`, `npm run go:bench` | release artifacts, source workflows, specs, bindings, witness plans, explicit benchmark invocation | deterministic self-check report shape, SBOM candidate evidence, coverage metrics, workflow lint routing, benchmark entrypoints | public-source provenance, vulnerability triage, license approval, CI run admission, release approval | self-check report, SBOM, metrics report, CI signal, or benchmark output |
+| Supply-chain and quality | `self-check`, release workflow, `npm run release:sbom`, `npm run self:coverage`, `npm run go:actionlint`, `npm run go:bench` | release artifacts, source workflows, specs, bindings, witness plans, command-oracle candidate inventory, independently authored counterfeit corpus, explicit benchmark invocation | deterministic self-check report shape, SBOM candidate evidence, exact-file materialized-snapshot package-scoped selected-test execution, production-owner counterfeit decisions, strict one-read and current-owner command-oracle diagnostic admission, execution-backed coverage metrics, workflow lint routing, benchmark entrypoints | assertion-branch execution, mutation adequacy, producer authentication, public-source provenance, vulnerability triage, license approval, CI run admission, release approval | self-check report, SBOM, command-oracle diagnostic, metrics report, CI signal, or benchmark output |
 
 The `npm run release:sbom`, `npm run self:coverage`, `npm run go:actionlint`,
 and `npm run go:bench` routes above are maintainer commands for a source

docs/release-process.md

@@ -128,7 +128,16 @@ static analysis, workflow linting, vulnerability checks, npm package artifact
 creation, package artifact verification, Python wheel artifact creation, Python
 wheel verification, release SBOM, release manifest and checksum generation,
 outside-consumer binary smoke proof, self-hosting receipt validation, and
-coverage metrics generation.
+coverage metrics generation. Coverage generation runs the exact owner-selected
+Go tests through package-scoped argv vectors from an exact-file materialized
+source snapshot, evaluates the independently authored counterfeit corpus
+through production admission owners, and emits a command-oracle diagnostic
+plus coverage metrics v2 only while the candidate, corpus, runtime, and source
+identities remain current. Release closeout re-admits that diagnostic through
+its sole strict owner, binds its digest to the same canonical byte read, and
+revalidates current producer reachability. This local cooperative execution
+does not prove assertion-branch execution, mutation adequacy, producer
+authentication, or provider admission.
 
 The dry-run package identity proves candidate tarball shape only. It does not
 prove the bytes served by the registry after publish.

docs/specs/proofkit-supply-chain-quality/overview.md

@@ -58,15 +58,20 @@ vulnerability absence, or consumer rollout safety by itself.
 - `REQ-PROOFKIT-QUALITY-009`: performance-sensitive parser and serializer
   paths expose benchmark entrypoints without making wall-clock budgets a
   required PR gate before stable baselines exist.
-- `REQ-PROOFKIT-QUALITY-010`: coverage metrics report requirement, binding,
-  witness, CLI inventory linkage, and descriptor-owned command proof-route
-  candidates from admitted test-evidence-inventory rows, while critical
-  anti-vacuity scenarios retain exact closed selector inventories. Each linkage and route
-  conjunct has an independent fail-closed falsifier, and each source-checkout
-  selector resolves to a valid function in an active Go test file with its
-  exact executable command; static route metadata, prose, source markers, test
-  existence, and failure-capable syntax never become semantic falsifier
-  evidence.
+- `REQ-PROOFKIT-QUALITY-010`: coverage metrics keep static proof-route
+  candidates separate from an execution-backed command-oracle ledger. The
+  ledger runs exact selected Go tests through package-scoped argv vectors from
+  one exact-file materialized source snapshot, joins reserved lifecycle
+  attributes to every candidate identity, terminates bounded subprocesses on
+  cancellation or output overflow, confines atomic artifact publication and
+  invalidation to non-symlink repository paths, and fails closed on incomplete
+  command coverage or event, source, selection, producer-reachability, and
+  identity drift. A versioned counterfeit corpus owns checked-in expected
+  decisions for every required policy axis, evidence class, record coordinate,
+  and substitution axis; its mutations execute the production admission and
+  lifecycle owners rather than a generated expectation copy. Passing selected
+  tests does not prove assertion-branch execution, mutation adequacy, or
+  exhaustive command semantics.
 - `REQ-PROOFKIT-QUALITY-011`: CI separates the OS-independent full
   source/package gate from macOS platform smoke, executes the complete Go
   package set through its owner command, uses explicit hosted runner labels
@@ -102,12 +107,11 @@ vulnerability absence, or consumer rollout safety by itself.
   fields after validation.
 - `REQ-PROOFKIT-QUALITY-015`: the package gate includes an admitted release
   closeout completion-criteria report so unit tests alone cannot satisfy
-  release closeout, and coverage-metric re-admission uses overflow-safe exact
-  producer relations plus the complete command inventory, and compares both
-  coverage command projections with the actual `cli-contract.v2.json` command
-  inventory from the same source snapshot, so neither an impossible count
-  partition nor a coordinated same-size command substitution can satisfy
-  closeout.
+  release closeout. Coverage re-admission rejects candidate-only v1, requires
+  overflow-safe exact producer relations plus the complete command inventory,
+  and binds coverage v2 to the current command-oracle diagnostic through the
+  ledger owner's one-read canonical admission, current-owner revalidation, and
+  record, candidate-set, corpus, revision, and source-snapshot digests.
 - `REQ-PROOFKIT-QUALITY-016`: release platform targets use one private owner
   that projects platform suffixes, Go build targets, npm OS/CPU metadata,
   package tar entries, Python wheel tags, PyPI candidate completeness,