Make compact proof contracts declaration-only

BACKLOG.md

@@ -48,7 +48,6 @@ records, generated release manifests, or the owning docs named above.
 
 | Status | ID | Scope | Completion condition |
 |---|---|---|---|
-| 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. | 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. |

docs/proofkit-contract-map.md

@@ -41,9 +41,9 @@ owner boundaries. It is not a second command-family inventory.
 |---|---|---|---|---|---|
 | Adoption and scaffolding | `init`, `adoption-contract-envelope`, `adoption-workflow-plan`, `adoption-checklist`, `adoption-doctor`, `gradual-adoption`, `gradual-adoption-bootstrap`, `gradual-adoption-guidance`, `capability-map-admission`, `pilot-admission`, `scaffold-profile-plan`, `scaffold-project-structure`, `stack-preset` | adoption intent, aggregate adoption contract envelope, checklist facts, target paths, owner routes, caller-extracted stale authority vocabulary facts, explicit pre-spec capability observations, pilot records, stack preset id, optional init preset id | dry-run route selection, aggregate contract-envelope admission, deterministic starter plans, checklist/report admission, bounded guidance envelopes, dry-run manifests, pre-spec trust-mode admission, adoption gap and stale-authority classification, pilot shape admission | final files, final requirements, rollout policy, text extraction from files, code observation extraction, pilot truth | selected child output, plan, report, seed packet, or agent envelope |
 | Requirement source | `capability-map-admission`, `requirement-authoring-plan`, `requirement-source-admission`, `requirement-source-transition`, `spec-overview-claims`, `requirement-spec-tree`, `requirement-spec-tree-view`, `requirement-source-view`, `requirement-browser-server` | `requirements.v1.json`, caller-owned capability maps, caller-owned authoring facts, overview claim extraction, explicit spec hierarchy, view options | candidate seed admission, candidate-only authoring packets, source-shape admission, lifecycle checks, explicit tree topology/source-ref admission, shared safe renderer fragments, presentation-only views | requirement meaning, extraction completeness, Markdown extraction completeness, hierarchy ownership, proof adequacy, file materialization | capability map report, authoring packet, source report, spec-tree report, rendered view, or browser presentation |
-| Requirement proof binding | `requirement-bindings`, `binding-partition`, `proof-slice`, `evidence-graph`, `requirement-proof-resolver`, `requirement-proof-source-set`, `requirement-proof-view`, `spec-proof-bundle-admission` | requirement records, bindings, witness commands, source-set facts, receipt reports, partition policy | graph validation, binding partition projection, compact slices, typed compact proof contract projections, resolver projections, bundle linkage checks | test semantics, witness execution, proof freshness, merge policy | proof report, partition report, slice, lookup graph, or view |
+| Requirement proof binding | `requirement-bindings`, `binding-partition`, `proof-slice`, `evidence-graph`, `requirement-proof-resolver`, `requirement-proof-source-set`, `requirement-proof-view`, `spec-proof-bundle-admission` | requirement records, bindings, witness commands, source-set facts, receipt reports, partition policy | graph validation, binding partition projection, compact slices, declaration-only compact route projection with full binding identity and role-qualified witness routes, resolver projection, bundle linkage checks | selector resolution, oracle quality, witness execution, mutation adequacy, finding completeness, proof freshness, trust, assurance, merge policy | proof report, partition report, slice, declaration lookup graph, or view |
 | Test inventory and coverage | `test-evidence-inventory`, `test-evidence-inventory --projection discovery-draft`, `test-evidence-inventory --normalized-inventory`, `requirement-coverage-input-compose`, `requirement-coverage-view`, `requirement-browser-server --view coverage` | caller-owned direct or source-set test inventory, caller-owned explicit test discovery facts, declared quality findings, requirement source, proof binding or compact proof contract, coverage universe, optional owner-invariant registry, aggregate coverage compose input | strict inventory/source-set admission, candidate-only discovery draft projection, fail-closed normalized inventory projection, deterministic coverage-view input composition from explicit facts, missing declared assertion-signal and declared-quality classification, bounded agent action guidance, requirement/test/command/owner-invariant joins, nonsemantic command-evidence classification, stable coverage failure/warning classifications, presentation-only coverage view | inventory completeness, oracle quality, test quality, test discovery extraction, native test execution, receipt freshness, producer trust, merge policy | candidate inventory guidance, inventory report, normalized inventory data product, coverage-view input, coverage view, or browser presentation |
-| 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 |
+| 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 declaration-only proof contracts with zero or more scenario bindings per requirement, 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, binding-aware fan-out, 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, 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 |

docs/specs/proofkit-spec-proof-core/overview.md

@@ -16,14 +16,13 @@ execution receipts, and merge policy.
   or scanning overview prose as authority; one shipped, marker-bounded example
   is parsed as bounded expansion-free literal shell words and executed through
   the installed current product as a first valid input.
-- `REQ-PROOFKIT-SPEC-002`: requirement proof binding reports validate
-  caller-owned requirement-to-witness mappings, require compact scenarios to be
-  admitted `surface_id::stable_anchor` identities, require compact witness
-  selectors to use `repo/path::stable_anchor` identities, admit caller-owned
-  source-set fragments and selected-source resolver projections, and derive
-  typed compact proof contract projections for surfaces, scenarios, witnesses,
-  commands, environment classes, conformance facts, and falsification routes
-  without executing witnesses or deciding proof freshness.
+- `REQ-PROOFKIT-SPEC-002`: compact proof route declarations preserve the full
+  requirement/surface/scenario binding identity and role-qualified witness-route
+  identity, preserve each route's JSON-safe non-negative resolution order, admit
+  declaration-only v2 contracts plus source-set v2 and fragment v3 inputs, retain
+  distinct positive and falsification roles even for one shared selector, and
+  reject legacy proof-state, synthetic evidence counts, collapsed roles, and
+  identity-loss projections without claiming execution or assurance.
 - `REQ-PROOFKIT-SPEC-003`: witness planning accepts caller-owned structured
   command metadata, scheduler constraints, environment classes, and
   binding-derived command projections only through admitted witness vocabulary
@@ -79,11 +78,13 @@ execution receipts, and merge policy.
   serving with one exact supported-view vocabulary without accepting
   caller-owned raw HTML or making rendered output authoritative.
 - `REQ-PROOFKIT-SPEC-010`: requirement impact input composition converts
-  caller-owned base/current requirement sources, single-current-binding compact
-  proof contracts, changed-path facts, generated-artifact policy, local
-  environment policy, and proof-like path policy into a direct `impact` input
-  without scanning repositories, executing witnesses, or becoming a second
-  impact evaluator.
+  caller-owned base/current requirement sources, compact proof contracts with
+  one or more current bindings per active blocking requirement, changed-path
+  facts, generated-artifact policy, local environment policy, and proof-like
+  path policy into a direct `impact` input, treating every referenced surface
+  semantic change as a change to every referencing binding under the
+  proof-binding source-path policy, without scanning repositories, executing
+  witnesses, or becoming a second impact evaluator.
 - `REQ-PROOFKIT-SPEC-011`: adoption contract envelope admission validates a
   complete caller-owned aggregate adoption envelope, selects one child route
   through orthogonal CLI flags, rejects repeated single-value mode or pilot

docs/specs/proofkit-spec-proof-core/requirements.v1.json

@@ -35,7 +35,7 @@
     {
       "requirementId": "REQ-PROOFKIT-SPEC-002",
       "ownerId": "proofkit.spec-proof-core",
-      "invariant": "Requirement proof binding reports validate caller-owned requirement-to-witness mappings, require compact scenarios to use admitted surface_id::stable_anchor identities, require compact witness selectors to use admitted repo/path::stable_anchor identities, admit caller-owned source-set fragments and selected-source resolver projections, and derive typed compact proof contract projections for surfaces, scenarios, witnesses, commands, environment classes, conformance facts, and falsification routes without executing witnesses or deciding proof freshness.",
+      "invariant": "Requirement proof route declaration admission preserves each compact binding identity as requirementId, surfaceId, and scenarioId; preserves each witness route as bindingRecordId, role, selector, a JSON-safe non-negative resolutionOrderIndex, and witnessRouteId; admits exactly one positive and one falsification role even when both roles use the same selector; requires declaration-only v2 compact discriminators and admitted source-set v2 or fragment-v3 identities; rejects legacy proof-state, synthetic checked or finding counts, collapsed roles, and identity-loss projections; and derives only caller-owned declaration or lookup facts without executing witnesses or deciding selector resolution, oracle quality, mutation adequacy, proof freshness, trust, assurance, merge, rollout, or production readiness.",
       "claimLevel": "blocking",
       "riskClass": "high",
       "proofBindingRefs": [
@@ -45,7 +45,7 @@
         "NC-PROOFKIT-SPEC-002"
       ],
       "nonClaims": [
-        "This requirement does not claim native witness pass evidence, proof freshness, receipt authenticity, or merge approval."
+        "This requirement does not claim selector existence or resolution, oracle quality, native witness execution or pass evidence, mutation adequacy, finding completeness or absence, proof freshness, receipt authenticity, trust, assurance, merge approval, rollout approval, or production readiness."
       ],
       "lifecycle": {
         "state": "active",
@@ -251,7 +251,7 @@
     {
       "requirementId": "REQ-PROOFKIT-SPEC-010",
       "ownerId": "proofkit.spec-proof-core",
-      "invariant": "Requirement impact input composition converts caller-owned base and current requirement sources, single-current-binding compact proof contracts, changed-path facts, generated-artifact policy, local environment policy, and proof-like path policy into a direct impact command input while preserving downstream impact semantics and without scanning repositories, executing witnesses, deciding freshness, or becoming a second impact evaluator.",
+      "invariant": "Requirement impact input composition converts caller-owned base and current requirement sources, compact proof contracts with one or more current bindings per active blocking requirement, changed-path facts, generated-artifact policy, local environment policy, and proof-like path policy into a direct impact command input; treats every referenced surface semantic change as a change to every referencing binding under the proof-binding source-path policy; preserves downstream impact semantics; and does not scan repositories, execute witnesses, decide freshness, or become a second impact evaluator.",
       "claimLevel": "blocking",
       "riskClass": "high",
       "proofBindingRefs": [

go.mod

@@ -12,7 +12,11 @@ tool (
 
 require go.yaml.in/yaml/v4 v4.0.0-rc.3 // indirect
 
-require go.yaml.in/yaml/v3 v3.0.5
+require (
+	go.yaml.in/yaml/v3 v3.0.5
+	golang.org/x/mod v0.37.0
+	golang.org/x/tools v0.47.0
+)
 
 require (
 	github.com/BurntSushi/toml v1.6.0 // indirect
@@ -27,11 +31,9 @@ require (
 	github.com/rhysd/actionlint v1.7.12 // indirect
 	github.com/robfig/cron/v3 v3.0.1 // indirect
 	golang.org/x/exp/typeparams v0.0.0-20260611194520-c48552f49976 // indirect
-	golang.org/x/mod v0.37.0 // indirect
 	golang.org/x/sync v0.21.0 // indirect
 	golang.org/x/sys v0.46.0 // indirect
 	golang.org/x/telemetry v0.0.0-20260626140120-b709645a9e92 // indirect
-	golang.org/x/tools v0.47.0 // indirect
 	golang.org/x/vuln v1.5.0 // indirect
 	honnef.co/go/tools v0.7.0 // indirect
 )