diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index bdb1128..fe19cf2 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -1011,18 +1011,7 @@ jobs:
--notes-file artifacts/release/release-notes.md \
--asset-names-file /tmp/proofkit-expected-release-assets.txt
cp /tmp/proofkit-release-view.json artifacts/release/github-release.json
- retained_evidence=(artifacts/release/github-release.json)
- if compgen -G "artifacts/attestations/*.json" >/dev/null; then
- while IFS= read -r evidence; do
- retained_evidence+=("$evidence")
- done < <(find artifacts/attestations -type f -name '*.json' | sort)
- fi
- mapfile -t retained_evidence < <(printf '%s\n' "${retained_evidence[@]}" | sort)
- : > artifacts/release/retained-evidence-checksums.sha256
- for evidence in "${retained_evidence[@]}"; do
- sum="$(sha256sum "$evidence" | awk '{print $1}')"
- printf '%s %s\n' "$sum" "$(basename "$evidence")" >> artifacts/release/retained-evidence-checksums.sha256
- done
+ go run ./internal/tools/releasepreflight retained-evidence --artifact-root artifacts
final_dir="$(mktemp -d)"
for asset in "${expected_assets[@]}"; do
asset_name="$(basename "$asset")"
@@ -1048,18 +1037,7 @@ jobs:
--tag "$GITHUB_REF_NAME" \
--notes-file artifacts/release/release-notes.md \
--asset-names-file /tmp/proofkit-expected-release-assets.txt
- retained_evidence=(artifacts/release/github-release.json)
- if compgen -G "artifacts/attestations/*.json" >/dev/null; then
- while IFS= read -r evidence; do
- retained_evidence+=("$evidence")
- done < <(find artifacts/attestations -type f -name '*.json' | sort)
- fi
- mapfile -t retained_evidence < <(printf '%s\n' "${retained_evidence[@]}" | sort)
- : > artifacts/release/retained-evidence-checksums.sha256
- for evidence in "${retained_evidence[@]}"; do
- sum="$(sha256sum "$evidence" | awk '{print $1}')"
- printf '%s %s\n' "$sum" "$(basename "$evidence")" >> artifacts/release/retained-evidence-checksums.sha256
- done
+ go run ./internal/tools/releasepreflight retained-evidence --artifact-root artifacts
final_dir="$(mktemp -d)"
for asset in "${expected_assets[@]}"; do
asset_name="$(basename "$asset")"
@@ -1095,7 +1073,7 @@ jobs:
artifacts/release/checksums.sha256
artifacts/release/github-release.json
artifacts/release/metadata-checksums.sha256
- artifacts/release/retained-evidence-checksums.sha256
+ artifacts/retained-evidence-checksums.sha256
artifacts/release/release-manifest.json
artifacts/release/release-notes.md
artifacts/release/sbom.cdx.json
diff --git a/BACKLOG.md b/BACKLOG.md
index 9e18b1d..18e81be 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -53,3 +53,4 @@ records, generated release manifests, or the owning docs named above.
| DEFERRED | VALUE-01 | Admit exact value-evidence comparisons only after a real producer and downstream consumer establish the public record boundary; detailed candidate contract is retained in [issue #65](https://github.com/research-engineering/agentic-proofkit/issues/65). | A real execution-receipt projection, baseline producer, and downstream consumer prove an exact producer-output-to-admission round trip plus compact/full-graph inclusion or an intentional omission non-claim; otherwise no public command is added. |
| BLOCKED | RELOCATION-01 | Add provenance-bounded witness relocation candidates without introducing a second binding path or trusting a caller-authored prior digest; detailed candidate contract is retained in [issue #66](https://github.com/research-engineering/agentic-proofkit/issues/66). | An owner-admitted content-addressed baseline binds witness id, prior path and digest, source revision, evidence class, authentication non-claims, and freshness non-claims; the scanner then proves the zero/one/many match partition while remaining non-current until fresh execution evidence exists. |
| BLOCKED | RELEASE-01 | Prove signed protected-tag release policy as provider-side release governance, not source-only intent. | Repository tag protection/ruleset and release workflow variables require signed annotated release tags; the next public release records provider-side evidence or the row is explicitly retired as an accepted non-claim. |
+| BLOCKED | RELEASE-02 | Retire the inaccurate PyPI `0.1.159` wheel compatibility and license projection without mutating immutable release history. | After a public replacement release proves macOS 12.0 wheel tags, embedded MIT license identity, npm/PyPI/GitHub byte closure, and installed-package smoke, yank PyPI `0.1.159` with an exact compatibility-and-license reason and retain provider evidence of the yank. |
diff --git a/README.md b/README.md
index cdfa1e3..0b78e0c 100644
--- a/README.md
+++ b/README.md
@@ -42,6 +42,8 @@ Python consumers use the Python package as a runner wrapper over the same Go
CLI, not as a Python SDK. Python projects should still treat CLI/JSON records,
exit codes, and package metadata as the public contract.
+Published Darwin binary distributions require macOS 12.0 or later.
+
## Project Boundary
`agentic-proofkit` is intended to provide reusable proof-workflow mechanics for
diff --git a/docs/release-process.md b/docs/release-process.md
index 8dac9b5..8445868 100644
--- a/docs/release-process.md
+++ b/docs/release-process.md
@@ -42,7 +42,11 @@ Go source
-> GitHub Release assets with checksums and SBOM for provenance lookup
```
-The repository-owned `release:manifest` tool creates `release-manifest.json`,
+The committed `release/change-record.v1.json` owns the reviewed, version-bound
+declaration of the public-contract delta, migration decision, platform
+requirements, known limitations, and rollback strategy. It does not infer
+change completeness from the source diff. The repository-owned
+`release:manifest` tool admits that record and creates `release-manifest.json`,
`checksums.sha256`, `metadata-checksums.sha256`, `sbom-subjects.sha256`,
release notes, and deterministic SBOM candidate evidence from explicit package,
registry, and release evidence. `checksums.sha256` covers distributable archive
@@ -77,18 +81,21 @@ Before publishing a version:
1. The source tree is clean.
2. `package.json` contains the exact new version.
-3. `package.json` repository, license, bin, exports, files, and publishConfig
+3. `release/change-record.v1.json` contains the same version and explicitly
+ classifies breaking changes, additions, migration, platform requirements,
+ known limitations, and rollback.
+4. `package.json` repository, license, bin, exports, files, and publishConfig
match the intended public package contract.
-4. The npm account has verified email and write-protective 2FA, or the package
+5. The npm account has verified email and write-protective 2FA, or the package
uses an admitted Trusted Publisher configuration.
-5. When `PROOFKIT_ENABLE_PYPI_PUBLISH=true`, the PyPI account has a normal or
+6. When `PROOFKIT_ENABLE_PYPI_PUBLISH=true`, the PyPI account has a normal or
pending Trusted Publisher configured for project `agentic-proofkit`,
repository `research-engineering/agentic-proofkit`, workflow `release.yml`, and
environment `pypi`.
-6. The release workflow is configured for the package, public npm registry, and
+7. The release workflow is configured for the package, public npm registry, and
release environments. PyPI release configuration is required only when the
PyPI channel is explicitly enabled.
-7. `npm run check` passes locally or the release candidate workflow provides
+8. `npm run check` passes locally or the release candidate workflow provides
equivalent current-head evidence.
## Candidate Proof
@@ -156,7 +163,10 @@ The `release` workflow must:
14. retain normalized GitHub Release metadata as workflow release evidence at
`artifacts/release/github-release.json` after byte-for-byte asset
verification, and bind it plus any attestation record with
- `artifacts/release/retained-evidence-checksums.sha256`. The release
+ `artifacts/retained-evidence-checksums.sha256`. The checksum manifest lives
+ at the retained artifact root and uses exact `release/...` and
+ `attestations/...` paths, so standard checksum verification executes against
+ the downloaded artifact layout without path rewriting. The release
manifest records GitHub Release channel data as candidate/archive inventory;
`github-release.json` owns post-create GitHub Release facts only inside
retained workflow evidence, not as a public release asset.
diff --git a/docs/specs/proofkit-spec-proof-core/overview.md b/docs/specs/proofkit-spec-proof-core/overview.md
index 2733891..e9cf8ce 100644
--- a/docs/specs/proofkit-spec-proof-core/overview.md
+++ b/docs/specs/proofkit-spec-proof-core/overview.md
@@ -108,10 +108,13 @@ execution receipts, and merge policy.
boundaries, and non-claims, then emits a bounded source-bound question packet
only after explicit user submission.
- `REQ-PROOFKIT-SPEC-022`: semantic diff compares admitted requirement fields
- by owner-declared scalar, set, and map semantics rather than textual order.
-- `REQ-PROOFKIT-SPEC-023`: traceability graphs preserve specification, proof,
- code traceability, and native execution as distinct evidence planes and
- accept code topology only as explicit caller-owned input.
+ by owner-declared scalar, set, map, and lifecycle semantics, covers entity
+ additions and removals, and remains closed under output re-admission.
+- `REQ-PROOFKIT-SPEC-023`: traceability graph input schema v2 preserves
+ specification, proof, code traceability, and native execution as distinct
+ evidence planes and accepts code topology only as explicit caller-owned input
+ with source-digest, parent-edge, abstraction-order, and pre-materialization
+ budget closure.
## Non-Claims
diff --git a/docs/specs/proofkit-spec-proof-core/requirements.v1.json b/docs/specs/proofkit-spec-proof-core/requirements.v1.json
index 7181b73..2f96344 100644
--- a/docs/specs/proofkit-spec-proof-core/requirements.v1.json
+++ b/docs/specs/proofkit-spec-proof-core/requirements.v1.json
@@ -533,7 +533,7 @@
{
"requirementId": "REQ-PROOFKIT-SPEC-022",
"ownerId": "proofkit.spec-proof-core",
- "invariant": "Requirement semantic diff compares two admitted context snapshots by stable requirement identity and owner-declared scalar, set, and map field classes, producing deterministic added, removed, and modified facts without textual diff, inferred move semantics, or authority over requirement meaning.",
+ "invariant": "Requirement semantic diff compares two admitted context snapshots by stable requirement identity and owner-declared scalar, set, map, and lifecycle field classes, producing canonically ordered added, removed, and modified facts that remain closed under output re-admission without textual diff, inferred move semantics, or authority over requirement meaning.",
"claimLevel": "blocking",
"riskClass": "medium",
"proofBindingRefs": ["proofkit/requirement-bindings.json"],
@@ -546,7 +546,7 @@
{
"requirementId": "REQ-PROOFKIT-SPEC-023",
"ownerId": "proofkit.spec-proof-core",
- "invariant": "Requirement traceability graph deterministically projects admitted specification and proof topology plus explicit caller-owned code topology while preserving specification, proof, code traceability, and native execution as distinct evidence planes and rejecting dangling topology references.",
+ "invariant": "Requirement traceability graph input schema v2 deterministically projects admitted specification and proof topology plus explicit caller-owned code topology while preserving specification, proof, code traceability, and native execution as distinct evidence planes; one typed topology validator rejects dangling endpoints, enforces the bijection between non-root parentNodeId facts and contains edges with broader parent abstraction, verifies every supplied code-source digest, and applies node, edge, and source-byte budgets before per-item semantic materialization.",
"claimLevel": "blocking",
"riskClass": "high",
"proofBindingRefs": ["proofkit/requirement-bindings.json"],
diff --git a/docs/specs/proofkit-supply-chain-quality/overview.md b/docs/specs/proofkit-supply-chain-quality/overview.md
index 6cc05e2..18cb715 100644
--- a/docs/specs/proofkit-supply-chain-quality/overview.md
+++ b/docs/specs/proofkit-supply-chain-quality/overview.md
@@ -98,6 +98,14 @@ vulnerability absence, or consumer rollout safety by itself.
routes, bounded server cleanup, repository-confined non-symlink proof
artifacts, and machine-admitted per-project rendered engine evidence without
runtime dependencies or a production bundler.
+- `REQ-PROOFKIT-QUALITY-023`: Python wheels independently bind advertised
+ platform compatibility to decoded executable bytes and carry Core Metadata
+ 2.4 plus an exact, RECORD-closed repository license payload.
+- `REQ-PROOFKIT-QUALITY-024`: a version-bound machine record declares the
+ reviewed public-contract change set and owns release-note content, while one
+ retained-evidence owner builds and verifies checksums against exact
+ downloadable artifact-relative paths without inferring change completeness
+ from the source diff.
## Non-Claims
diff --git a/docs/specs/proofkit-supply-chain-quality/requirements.v1.json b/docs/specs/proofkit-supply-chain-quality/requirements.v1.json
index 4685aae..c821471 100644
--- a/docs/specs/proofkit-supply-chain-quality/requirements.v1.json
+++ b/docs/specs/proofkit-supply-chain-quality/requirements.v1.json
@@ -294,6 +294,32 @@
"lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
"deferral": null,
"updatePolicy": {"reviewOwnerId": "proofkit.supply-chain-quality", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
+ },
+ {
+ "requirementId": "REQ-PROOFKIT-QUALITY-023",
+ "ownerId": "proofkit.supply-chain-quality",
+ "invariant": "Each Python wheel binds its embedded executable to the release binary digest, independently decodes Darwin Mach-O bytes so an advertised macOS platform minimum is never lower than the executable minimum, uses Core Metadata 2.4 License-Expression and License-File fields, carries an exact repository LICENSE copy under the wheel licenses directory, and closes every payload entry through RECORD.",
+ "claimLevel": "blocking",
+ "riskClass": "critical",
+ "proofBindingRefs": ["proofkit/requirement-bindings.json"],
+ "nonClaimRefs": ["NC-PROOFKIT-QUALITY-023"],
+ "nonClaims": ["This requirement does not claim execution on every accepted operating-system version, legal approval, registry publication, release approval, rollout approval, or production readiness."],
+ "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
+ "deferral": null,
+ "updatePolicy": {"reviewOwnerId": "proofkit.supply-chain-quality", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
+ },
+ {
+ "requirementId": "REQ-PROOFKIT-QUALITY-024",
+ "ownerId": "proofkit.supply-chain-quality",
+ "invariant": "Release metadata generation admits one version-bound machine-readable declaration of the reviewed public-contract change set and renders release notes as its exact projection, while one repository-owned retained-evidence builder and verifier checksum the exact final downloadable artifact topology with artifact-relative paths, reject unbound evidence files and symlink substitution, and fail release closeout on record, note, path, or digest drift.",
+ "claimLevel": "blocking",
+ "riskClass": "high",
+ "proofBindingRefs": ["proofkit/requirement-bindings.json"],
+ "nonClaimRefs": ["NC-PROOFKIT-QUALITY-024"],
+ "nonClaims": ["This requirement does not infer change-record completeness from source changes, make release notes approval authority, or prove provider publication, attestation authenticity, consumer adoption, rollout approval, or production readiness."],
+ "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
+ "deferral": null,
+ "updatePolicy": {"reviewOwnerId": "proofkit.supply-chain-quality", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
}
]
}
diff --git a/internal/app/command_coverage_routes.go b/internal/app/command_coverage_routes.go
index ab84c6b..df755bd 100644
--- a/internal/app/command_coverage_routes.go
+++ b/internal/app/command_coverage_routes.go
@@ -104,8 +104,8 @@ var commandCoverageRoutes = map[string][]commandCoverageRoute{
"repo-profile-admission": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/repoprofileadmission/repo_profile_admission_test.go", "TestBuildAdmitsValidRepoProfileAndRejectsRootPackageMismatch", semanticRouteProof("repo_profile_admission.build_admits_valid_repo_profile_and_rejects_root_package_mismatch", commandCoverageExpectedPublicOutcome), "Repo profile admission must reject mismatch between profile root package and observed package facts.")},
"requirement-bindings": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementbinding/projections_test.go", "TestBuildReportFailsUnknownRequirementBinding", semanticRouteProof("projections.build_report_fails_unknown_requirement_binding", commandCoverageExpectedPublicOutcome), "Requirement binding reports must fail closed when bindings reference unknown requirements.")},
"requirement-browser-server": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementbrowser/server_test.go", "TestStartServerFailsClosedForNonLoopbackHosts", semanticRouteProof("server.start_server_fails_closed_for_non_loopback_hosts", commandCoverageExpectedPublicOutcome), "Requirement browser server must reject non-loopback host binding."), directCLIRoute("internal/app/cli_abi_test.go", "TestRequirementBrowserServerSpecTreeCLIABI", semanticRouteProof("cli_abi.requirement_browser_server_spec_tree_cliabi", commandCoverageExpectedPublicOutcome), "Requirement browser server CLI ABI must admit explicit spec-tree view routing and emit a presentation-only browser plan.")},
- "requirement-context-compose": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementcontext/requirementcontext_test.go", "TestComposeAndSliceRoundTrip", semanticRouteProof("requirementcontext.compose_and_slice_round_trip", commandCoverageExpectedPublicOutcome), "Requirement context composition must read only an explicit catalog and produce a content-bound snapshot accepted unchanged by the slice owner.")},
- "requirement-context-slice": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementcontext/requirementcontext_test.go", "TestSliceRejectsTamperedSnapshotAndUnknownNode", semanticRouteProof("requirementcontext.slice_rejects_tampered_snapshot_and_unknown_node", commandCoverageExpectedPublicOutcome), "Requirement context slicing must reject stale snapshot identity and unknown explicit semantic targets.")},
+ "requirement-context-compose": {requiredInputAdmissionRoute, directCLIRoute("internal/app/requirement_context_cli_test.go", "TestRequirementContextCommandsComposeThroughWholeCLI", semanticRouteProof("requirement_context_cli.compose_through_whole_cli", commandCoverageExpectedPublicOutcome), "Requirement context composition must honor its explicit repository root and emit an owner-admitted snapshot through the public CLI."), packageFalsifierRoute("internal/command/requirementcontext/requirementcontext_test.go", "TestComposeAndSliceRoundTrip", semanticRouteProof("requirementcontext.compose_and_slice_round_trip", commandCoverageExpectedPublicOutcome), "Requirement context composition must read only an explicit catalog and produce a content-bound snapshot accepted unchanged by the slice owner.")},
+ "requirement-context-slice": {requiredInputAdmissionRoute, directCLIRoute("internal/app/requirement_context_cli_test.go", "TestRequirementContextCommandsComposeThroughWholeCLI", semanticRouteProof("requirement_context_cli.slice_through_whole_cli", commandCoverageExpectedPublicOutcome), "Requirement context slicing must consume the composed snapshot and emit the selected semantic fragment through the public CLI."), packageFalsifierRoute("internal/command/requirementcontext/requirementcontext_test.go", "TestSliceRejectsTamperedSnapshotAndUnknownNode", semanticRouteProof("requirementcontext.slice_rejects_tampered_snapshot_and_unknown_node", commandCoverageExpectedPublicOutcome), "Requirement context slicing must reject stale snapshot identity and unknown explicit semantic targets.")},
"requirement-coverage-input-compose": {
requiredInputAdmissionRoute,
packageFalsifierRoute("internal/command/requirementcoverageinput/requirementcoverageinput_test.go", "TestBuildComposesInputPreservesDeclaredUniverseAndAllowsDownstreamFailures", semanticRouteProof("requirementcoverageinput.build_composes_input_preserves_declared_universe_and_allows_downstream_failures", commandCoverageExpectedPublicOutcome), "Requirement coverage input composition must preserve declared universe facts while keeping downstream coverage failures separate from composition admission."),
@@ -116,7 +116,7 @@ var commandCoverageRoutes = map[string][]commandCoverageRoute{
"requirement-impact-input-compose": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementimpactinput/requirementimpactinput_test.go", "TestBuildComposesInputAndRoutesChangedBlockingRequirement", semanticRouteProof("requirementimpactinput.build_composes_input_and_routes_changed_blocking_requirement", commandCoverageExpectedPublicOutcome), "Requirement impact input composition must emit direct impact inputs from admitted caller-owned sources while preserving downstream impact semantics.")},
"requirement-proof-resolver": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementbinding/compact_contract_test.go", "TestBuildResolverRejectsUnscopedCompactIdentity", semanticRouteProof("compact_contract.build_resolver_rejects_unscoped_compact_identity", commandCoverageExpectedPublicOutcome), "Requirement proof resolver must fail closed on unscoped scenario ids and unadmitted witness selector identities."), packageFalsifierRoute("internal/command/requirementbinding/compact_contract_test.go", "TestBuildResolverEmitsNamedLookupFacts", semanticRouteProof("compact_contract.build_resolver_emits_named_lookup_facts", commandCoverageExpectedPublicOutcome), "Requirement proof resolver must emit deterministic named lookup facts for commands, environment classes, surfaces, scenarios, and witness selectors.")},
"requirement-proof-source-set": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementproofsourceset/requirementproofsourceset_test.go", "TestBuildSelectsSourceSetRowsAndEmitsResolverInput", semanticRouteProof("requirementproofsourceset.build_selects_source_set_rows_and_emits_resolver_input", commandCoverageExpectedPublicOutcome), "Requirement proof source-set normalization must select caller-owned source rows and emit resolver-compatible projections without scanning repositories.")},
- "requirement-semantic-diff": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementdiff/requirementdiff_test.go", "TestBuildClassifiesOwnerAwareRequirementChanges", semanticRouteProof("requirementdiff.build_classifies_owner_aware_requirement_changes", commandCoverageExpectedPublicOutcome), "Requirement semantic diff must compare admitted requirement fields by owner-declared field class instead of textual order.")},
+ "requirement-semantic-diff": {requiredInputAdmissionRoute, directCLIRoute("internal/app/requirement_context_cli_test.go", "TestRequirementContextCommandsComposeThroughWholeCLI", semanticRouteProof("requirement_context_cli.diff_through_whole_cli", commandCoverageExpectedPublicOutcome), "Requirement semantic diff must emit an owner-admitted change set through the public CLI."), packageFalsifierRoute("internal/command/requirementdiff/requirementdiff_test.go", "TestBuildCoversCompleteRequirementChangeAlgebra", semanticRouteProof("requirementdiff.build_covers_complete_requirement_change_algebra", commandCoverageExpectedPublicOutcome), "Requirement semantic diff must cover entity, scalar, set, map, and lifecycle changes and remain closed under output admission.")},
"requirement-proof-view": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementproofview/requirementproofview_test.go", "TestBuildMarkdownEscapesCallerControlledCompactFields", semanticRouteProof("requirementproofview.build_markdown_escapes_caller_controlled_compact_fields", commandCoverageExpectedPublicOutcome), "Requirement proof view must escape caller-controlled compact binding fields.")},
"requirement-authoring-plan": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementauthoringplan/requirement_authoring_plan_test.go", "TestBuildRejectsCandidateSourceAdmissionFailure", semanticRouteProof("requirement_authoring_plan.build_rejects_candidate_source_admission_failure", commandCoverageExpectedPublicOutcome), "Requirement authoring plans must keep candidate source previews candidate-only and fail closed when the composed source cannot pass requirement-source admission.")},
"requirement-source-admission": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementsourceadmission/requirementsourceadmission_test.go", "TestEvaluateRejectsBlockingRequirementWithoutProofRoute", semanticRouteProof("requirementsourceadmission.evaluate_rejects_blocking_requirement_without_proof_route", commandCoverageExpectedPublicOutcome), "Requirement source admission must reject blocking active requirements without proof binding routes.")},
@@ -124,7 +124,7 @@ var commandCoverageRoutes = map[string][]commandCoverageRoute{
"requirement-source-view": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementsourceview/requirementsourceview_test.go", "TestBuildMarkdownEscapesCallerControlledText", semanticRouteProof("requirementsourceview.build_markdown_escapes_caller_controlled_text", commandCoverageExpectedPublicOutcome), "Requirement source view must escape caller-controlled requirement text.")},
"requirement-spec-tree": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementspectree/requirementspectree_test.go", "TestBuildRejectsDAGAndStaleDigest", semanticRouteProof("requirementspectree.build_rejects_dagand_stale_digest", commandCoverageExpectedPublicOutcome), "Requirement spec tree admission must reject DAG topology and stale caller-provided source digest facts.")},
"requirement-spec-tree-view": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementspectree/requirementspectree_test.go", "TestBuildViewMarkdownAndHTMLAreDeterministicAndEscaped", semanticRouteProof("requirementspectree.build_view_markdown_and_htmlare_deterministic_and_escaped", commandCoverageExpectedPublicOutcome), "Requirement spec tree views must reuse admitted spec-tree input and escape caller-controlled text in deterministic HTML and Markdown projections.")},
- "requirement-traceability-graph": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/requirementgraph/requirementgraph_test.go", "TestBuildKeepsTraceabilityEvidencePlanesDistinct", semanticRouteProof("requirementgraph.build_keeps_traceability_evidence_planes_distinct", commandCoverageExpectedPublicOutcome), "Requirement traceability graph must keep specification, proof, code traceability, and native execution evidence planes distinct.")},
+ "requirement-traceability-graph": {requiredInputAdmissionRoute, directCLIRoute("internal/app/requirement_context_cli_test.go", "TestRequirementContextCommandsComposeThroughWholeCLI", semanticRouteProof("requirement_context_cli.graph_through_whole_cli", commandCoverageExpectedPublicOutcome), "Requirement traceability graph must emit an owner-admitted graph through the public CLI."), packageFalsifierRoute("internal/command/requirementgraph/requirementgraph_test.go", "TestBuildKeepsTraceabilityEvidencePlanesDistinct", semanticRouteProof("requirementgraph.build_keeps_traceability_evidence_planes_distinct", commandCoverageExpectedPublicOutcome), "Requirement traceability graph must keep specification, proof, code traceability, and native execution evidence planes distinct."), packageFalsifierRoute("internal/command/requirementgraph/requirementgraph_test.go", "TestAdmitOutputRejectsDanglingAndIncoherentCodeParents", semanticRouteProof("requirementgraph.admit_output_rejects_dangling_and_incoherent_code_parents", commandCoverageExpectedPublicOutcome), "Requirement traceability graph output admission must reject dangling and incoherent code parent relations.")},
"scaffold-profile-plan": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/scaffoldprofileplan/scaffoldprofileplan_test.go", "TestBuildAcceptsCommandMatcherHints", semanticRouteProof("scaffoldprofileplan.build_accepts_command_matcher_hints", commandCoverageExpectedPublicOutcome), "Scaffold profile planning must preserve caller-reviewed command matcher hints as deterministic profile draft data.")},
"scaffold-project-structure": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/projectstructure/projectstructure_test.go", "TestBuildAdmitsProjectStructureScaffoldAndEmitsBoundedEnvelope", semanticRouteProof("projectstructure.build_admits_project_structure_scaffold_and_emits_bounded_envelope", commandCoverageExpectedPublicOutcome), "Project structure scaffold must emit deterministic source-report identity and bounded agent guidance without writing files."), packageFalsifierRoute("internal/command/projectstructure/projectstructure_test.go", "TestBuildRejectsProjectStructurePathDriftAndUnsafePaths", semanticRouteProof("projectstructure.build_rejects_project_structure_path_drift_and_unsafe_paths", commandCoverageExpectedPublicOutcome), "Project structure scaffold must reject unsafe paths and inconsistent bootstrap/profile proof paths.")},
"selective-gate-evidence": {requiredInputAdmissionRoute, packageFalsifierRoute("internal/command/selectivegateevidence/selectivegateevidence_test.go", "TestBuildRejectsMergeSatisfyingEvidenceWithoutProducerAdmission", semanticRouteProof("selectivegateevidence.build_rejects_merge_satisfying_evidence_without_producer_admission", commandCoverageExpectedPublicOutcome), "Selective gate evidence must reject merge-satisfying evidence without producer admission."), packageFalsifierRoute("internal/command/selectivegateevidence/selectivegateevidence_test.go", "TestBuildReportsMergeEvidenceWithoutApprovingMerge", semanticRouteProof("selectivegateevidence.build_reports_merge_evidence_without_approving_merge", commandCoverageExpectedPublicOutcome), "Selective gate evidence must report merge evidence facts without approving consumer-owned merge admission.")},
diff --git a/internal/app/command_descriptors.go b/internal/app/command_descriptors.go
index c1d7a0f..415e01b 100644
--- a/internal/app/command_descriptors.go
+++ b/internal/app/command_descriptors.go
@@ -114,22 +114,22 @@ var commandDescriptors = []commandDescriptor{
command("repo-profile-admission", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("repoprofileadmission")),
command("requirement-authoring-plan", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementauthoringplan")),
command("requirement-bindings", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementbinding")),
- command("requirement-browser-server", commandInputRequired, flags("--empty-local-environment-policy", "--host", "--input", "--input-pointer", "--local-environment-class", "--open", "--port", "--scope", "--serve", "--session-mode", "--session-timeout-seconds", "--view"), modes("json", "server"), ownerDirs("requirementbrowser"), withRunner(commandRunnerRequirementBrowserServer), withSemanticAppTests("TestRequirementBrowserServerSpecTreeCLIABI"), withRequiredFlags("--view"), withFlagValueRequirement("--session-mode", "one-shot-question", "--open", "--serve", "--view"), withInputSchemaSummary("workspace mode: schemaVersion=1", "workspace mode: workspaceId", "workspace mode: context=proofkit.requirement-context", "workspace mode: diffInput=proofkit.requirement-semantic-diff-input (optional)", "workspace mode: graphInput=proofkit.requirement-traceability-graph-input (optional)", "--session-mode values: browse|one-shot-question", "one-shot-question requires --view workspace --serve --open", "--session-timeout-seconds is 1..7200 and requires one-shot-question", "source|proof|coverage|spec-tree modes retain their owner input contracts")),
- command("requirement-context-compose", commandInputRequired, flags("--input", "--input-pointer", "--repo-root"), modes("json"), ownerDirs("requirementcontext"), withRunner(commandRunnerRequirementContextCompose), withScopeClass(commandScopeExplicitFileSystemScan), withRequiredFlags("--repo-root"), withInputSchemaSummary("schemaVersion=1", "catalogId", "specTree.path", "requirementSources[] (non-empty)", "requirementSources[].nodeId", "requirementSources[].path", "expectedSourceDigest (optional sha256 ref)", "proofBinding.path (optional)", "coverage.path (optional)", "exact catalog paths only; no discovery")),
- command("requirement-context-slice", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementcontext"), withInputSchemaSummary("schemaVersion=1", "sliceId", "context=proofkit.requirement-context", "query.profile=routing|specification|proof|coverage|review", "query.nodeIds[]|requirementIds[]|ownerIds[]|lifecycleStates[]", "query.maxDepth=0..512", "query.maxNodes=1..4096", "query.maxRequirements=1..16384")),
+ command("requirement-browser-server", commandInputRequired, flags("--empty-local-environment-policy", "--host", "--input", "--input-pointer", "--local-environment-class", "--open", "--port", "--scope", "--serve", "--session-mode", "--session-timeout-seconds", "--view"), modes("json", "server"), ownerDirs("requirementbrowser"), withRunner(commandRunnerRequirementBrowserServer), withSemanticAppTests("TestRequirementBrowserServerSpecTreeCLIABI"), withRequiredFlags("--view"), withFlagValueRequirement("--session-mode", "one-shot-question", "--open", "--serve", "--view"), withInputSchemaSummary("workspace mode: schemaVersion=1", "workspace mode: workspaceId", "workspace mode: context=proofkit.requirement-context", "workspace mode: diffInput=proofkit.requirement-semantic-diff-input (optional)", "workspace mode: graphInput=proofkit.requirement-traceability-graph-input schemaVersion=2 (optional)", "--session-mode values: browse|one-shot-question", "one-shot-question requires --view workspace --serve --open", "--session-timeout-seconds is 1..7200 and requires one-shot-question", "source|proof|coverage|spec-tree modes retain their owner input contracts")),
+ command("requirement-context-compose", commandInputRequired, flags("--input", "--input-pointer", "--repo-root"), modes("json"), ownerDirs("requirementcontext"), withRunner(commandRunnerRequirementContextCompose), withSemanticAppTests("TestRequirementContextCommandsComposeThroughWholeCLI"), withScopeClass(commandScopeExplicitFileSystemScan), withRequiredFlags("--repo-root"), withInputSchemaSummary("schemaVersion=1", "catalogId", "specTree.path", "requirementSources[] (non-empty)", "requirementSources[].nodeId", "requirementSources[].path", "expectedSourceDigest (optional sha256 ref)", "proofBinding.path (optional)", "coverage.path (optional)", "exact catalog paths only; no discovery")),
+ command("requirement-context-slice", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementcontext"), withSemanticAppTests("TestRequirementContextCommandsComposeThroughWholeCLI"), withInputSchemaSummary("schemaVersion=1", "sliceId", "context=proofkit.requirement-context", "query.profile=routing|specification|proof|coverage|review", "query.nodeIds[]|requirementIds[]|ownerIds[]|lifecycleStates[]", "query.maxDepth=0..512", "query.maxNodes=1..4096", "query.maxRequirements=1..16384")),
command("requirement-coverage-input-compose", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementcoverageinput")),
command("requirement-coverage-view", commandInputRequired, flags("--agent-envelope", "--format", "--input", "--input-pointer"), modes("html", "json", "markdown"), ownerDirs("requirementcoverageview"), withRunner(commandRunnerRequirementView), withAgentEnvelope()),
command("requirement-impact-input-compose", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementimpactinput")),
command("requirement-proof-resolver", commandInputRequired, flags("--empty-local-environment-policy", "--input", "--input-pointer", "--local-environment-class"), modes("json"), ownerDirs("requirementbinding"), withRunner(commandRunnerRequirementProofResolver), withExactlyOneOfFlags("--empty-local-environment-policy", "--local-environment-class")),
command("requirement-proof-source-set", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementproofsourceset")),
command("requirement-proof-view", commandInputRequired, flags("--empty-local-environment-policy", "--format", "--input", "--input-pointer", "--local-environment-class", "--scope"), modes("html", "json", "markdown"), ownerDirs("requirementproofview"), withRunner(commandRunnerRequirementView)),
- command("requirement-semantic-diff", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementdiff"), withInputSchemaSummary("schemaVersion=1", "diffId", "baseContext=proofkit.requirement-context", "currentContext=proofkit.requirement-context", "query.requirementIds[] (optional)", "query.ownerIds[] (optional)", "query.maxChanges=1..8192 (optional)")),
+ command("requirement-semantic-diff", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementdiff"), withSemanticAppTests("TestRequirementContextCommandsComposeThroughWholeCLI"), withInputSchemaSummary("schemaVersion=1", "diffId", "baseContext=proofkit.requirement-context", "currentContext=proofkit.requirement-context", "query.requirementIds[] (optional)", "query.ownerIds[] (optional)", "query.maxChanges=1..8192 (optional)")),
command("requirement-source-admission", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementsourceadmission")),
command("requirement-source-transition", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementsourcetransition")),
command("requirement-source-view", commandInputRequired, flags("--format", "--input", "--input-pointer"), modes("html", "json", "markdown"), ownerDirs("requirementsourceview"), withRunner(commandRunnerRequirementView)),
command("requirement-spec-tree", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementspectree")),
command("requirement-spec-tree-view", commandInputRequired, flags("--format", "--input", "--input-pointer", "--output"), modes("html", "json", "markdown"), ownerDirs("requirementspectree"), withRunner(commandRunnerRequirementView)),
- command("requirement-traceability-graph", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementgraph"), withInputSchemaSummary("schemaVersion=1", "graphId", "context=proofkit.requirement-context", "codeSources[].path+content (optional, bounded UTF-8)", "codeTopology.topologyId", "codeTopology.nodes[].abstractionLevel=repository|package|module|file|symbol|source_range", "codeTopology.nodes[].sourceDigest+currentnessState", "codeTopology.edges[].evidenceRefs+authorityClass+currentnessState", "codeTopology.nativeCoverage[].producerId+evidenceRef+authorityClass+currentnessState+state")),
+ command("requirement-traceability-graph", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("requirementgraph"), withSemanticAppTests("TestRequirementContextCommandsComposeThroughWholeCLI"), withInputSchemaSummary("schemaVersion=2", "graphId", "context=proofkit.requirement-context", "codeSources[].path+content (optional, bounded UTF-8)", "codeTopology.nodes[].abstractionLevel=repository|package|module|file|symbol|source_range", "codeTopology.nodes[].sourceDigest+currentnessState", "codeTopology.edges[].evidenceRefs+authorityClass+currentnessState", "codeTopology.nativeCoverage[].producerId+evidenceRef+authorityClass+currentnessState+state")),
command("scaffold-profile-plan", commandInputRequired, flags("--input", "--input-pointer"), modes("json"), ownerDirs("scaffoldprofileplan")),
command("scaffold-project-structure", commandInputRequired, flags("--agent-envelope", "--input", "--input-pointer"), modes("json"), ownerDirs("projectstructure"), withRunner(commandRunnerProjectStructure), withAgentEnvelope()),
command("selective-gate-evidence", commandInputRequired, flags("--agent-envelope", "--input", "--input-pointer"), modes("json"), ownerDirs("selectivegateevidence"), withRunner(commandRunnerPlanning), withAgentEnvelope()),
diff --git a/internal/app/requirement_context_cli_test.go b/internal/app/requirement_context_cli_test.go
new file mode 100644
index 0000000..5cd6049
--- /dev/null
+++ b/internal/app/requirement_context_cli_test.go
@@ -0,0 +1,138 @@
+package app
+
+import (
+ "bytes"
+ "context"
+ "encoding/json"
+ "os"
+ "path/filepath"
+ "testing"
+
+ "github.com/research-engineering/agentic-proofkit/internal/command/requirementcontext"
+ "github.com/research-engineering/agentic-proofkit/internal/command/requirementdiff"
+ "github.com/research-engineering/agentic-proofkit/internal/command/requirementgraph"
+ "github.com/research-engineering/agentic-proofkit/internal/kernel/admission"
+ "github.com/research-engineering/agentic-proofkit/internal/kernel/stablejson"
+ "github.com/research-engineering/agentic-proofkit/internal/testsupport/commandcoverage"
+)
+
+func TestRequirementContextCommandsComposeThroughWholeCLI(t *testing.T) {
+ commandcoverage.SemanticRoute(t, "proofkit.command_coverage.source_oracle.v1.078417255856588541640488533337296521071324425566921898314006295059346651375053")
+ commandcoverage.SemanticRoute(t, "proofkit.command_coverage.source_oracle.v1.026918779924949500817883735459777435749569395463462098851750112168717349371591")
+ commandcoverage.SemanticRoute(t, "proofkit.command_coverage.source_oracle.v1.037106612382996619981621102911104931496378404893868406197919247815645123874441")
+ commandcoverage.SemanticRoute(t, "proofkit.command_coverage.source_oracle.v1.023947615033231006584057272018250251823714544315759467896512469485975523531624")
+ root := t.TempDir()
+ tree := map[string]any{
+ "schemaVersion": json.Number("2"), "treeId": "consumer.spec-tree", "rootNodeId": "consumer.root",
+ "callerAnnotations": []any{}, "edges": []any{}, "overlays": []any{},
+ "nodes": []any{map[string]any{
+ "nodeId": "consumer.root", "nodeKind": "meta_spec", "label": "Consumer specification", "displayOrder": json.Number("1"),
+ "callerAnnotations": []any{},
+ "sourceRefs": []any{map[string]any{
+ "sourceRefId": "consumer.root.requirements", "sourceRefKind": "source_id",
+ "sourceRole": "requirements", "sourceId": "consumer.requirements",
+ }},
+ }},
+ }
+ requirementSource := cliRequirementSource("The CLI composes the baseline requirement context.")
+ writeCLIJSONFixture(t, root, "proofkit/spec-tree.json", tree)
+ writeCLIJSONFixture(t, root, "docs/specs/consumer/requirements.v1.json", requirementSource)
+ catalog := map[string]any{
+ "schemaVersion": json.Number("1"), "catalogId": "consumer.context",
+ "specTree": map[string]any{"path": "proofkit/spec-tree.json"},
+ "requirementSources": []any{map[string]any{
+ "nodeId": "consumer.root", "path": "docs/specs/consumer/requirements.v1.json",
+ }},
+ }
+
+ base := runAppJSON(t, []string{"requirement-context-compose", "--input", "-", "--repo-root", root}, catalog)
+ if _, err := requirementcontext.AdmitSnapshot(base); err != nil {
+ t.Fatalf("whole-CLI context output failed owner admission: %v", err)
+ }
+ slice := runAppJSON(t, []string{"requirement-context-slice", "--input", "-"}, map[string]any{
+ "schemaVersion": json.Number("1"), "sliceId": "consumer.context.slice", "context": base,
+ "query": map[string]any{"profile": "specification", "requirementIds": []any{"REQ-CONSUMER-001"}},
+ })
+ if slice["contextKind"] != "proofkit.requirement-context-slice" || slice["state"] != "selected" || slice["snapshotId"] != base["snapshotId"] {
+ t.Fatalf("unexpected whole-CLI context slice: %#v", slice)
+ }
+
+ requirementSource["requirements"].([]any)[0].(map[string]any)["invariant"] = "The CLI composes the current requirement context."
+ writeCLIJSONFixture(t, root, "docs/specs/consumer/requirements.v1.json", requirementSource)
+ current := runAppJSON(t, []string{"requirement-context-compose", "--input", "-", "--repo-root", root}, catalog)
+ diff := runAppJSON(t, []string{"requirement-semantic-diff", "--input", "-"}, map[string]any{
+ "schemaVersion": json.Number("1"), "diffId": "consumer.requirement.diff",
+ "baseContext": base, "currentContext": current,
+ })
+ if diff["changeCount"] != json.Number("1") {
+ t.Fatalf("whole-CLI semantic diff changeCount=%v, want 1", diff["changeCount"])
+ }
+ if _, err := requirementdiff.AdmitOutput(diff, current["snapshotId"].(string)); err != nil {
+ t.Fatalf("whole-CLI semantic diff failed owner admission: %v", err)
+ }
+
+ graph := runAppJSON(t, []string{"requirement-traceability-graph", "--input", "-"}, map[string]any{
+ "schemaVersion": json.Number("2"), "graphId": "consumer.requirement.graph", "context": current,
+ })
+ if _, err := requirementgraph.AdmitOutput(graph, current["snapshotId"].(string)); err != nil {
+ t.Fatalf("whole-CLI traceability graph failed owner admission: %v", err)
+ }
+}
+
+func cliRequirementSource(invariant string) map[string]any {
+ return map[string]any{
+ "schemaVersion": json.Number("1"), "sourceId": "consumer.requirements",
+ "specPackagePath": "docs/specs/consumer", "overviewPath": "docs/specs/consumer/overview.md",
+ "requirementsPath": "docs/specs/consumer/requirements.v1.json",
+ "requirements": []any{map[string]any{
+ "requirementId": "REQ-CONSUMER-001", "ownerId": "consumer.owner", "invariant": invariant,
+ "claimLevel": "blocking", "riskClass": "high",
+ "proofBindingRefs": []any{"proofkit/requirement-bindings.json"}, "nonClaimRefs": []any{"NC-CONSUMER-001"},
+ "nonClaims": []any{"This requirement does not approve merge."},
+ "lifecycle": map[string]any{"state": "active", "replacementRequirementIds": []any{}, "evidenceRefs": []any{}},
+ "deferral": nil,
+ "updatePolicy": map[string]any{"reviewOwnerId": "consumer.owner", "requiresImpactDeclaration": true, "requiresProofBindingReview": true},
+ }},
+ "nonClaims": []any{"This source does not execute proof witnesses."},
+ }
+}
+
+func runAppJSON(t *testing.T, args []string, input any) map[string]any {
+ t.Helper()
+ encoded, err := stablejson.Marshal(input)
+ if err != nil {
+ t.Fatal(err)
+ }
+ var stdout bytes.Buffer
+ var stderr bytes.Buffer
+ if exit := Run(context.Background(), args, bytes.NewReader(encoded), &stdout, &stderr); exit != 0 {
+ t.Fatalf("Run(%v) exit=%d stderr=%s stdout=%s", args, exit, stderr.String(), stdout.String())
+ }
+ if stderr.Len() != 0 {
+ t.Fatalf("Run(%v) wrote stderr on success: %s", args, stderr.String())
+ }
+ decoded, err := admission.DecodeJSON(bytes.NewReader(stdout.Bytes()), int64(stdout.Len()))
+ if err != nil {
+ t.Fatalf("Run(%v) emitted invalid JSON: %v", args, err)
+ }
+ record, ok := decoded.(map[string]any)
+ if !ok {
+ t.Fatalf("Run(%v) output is not an object", args)
+ }
+ return record
+}
+
+func writeCLIJSONFixture(t *testing.T, root, path string, value any) {
+ t.Helper()
+ encoded, err := stablejson.Marshal(value)
+ if err != nil {
+ t.Fatal(err)
+ }
+ target := filepath.Join(root, filepath.FromSlash(path))
+ if err := os.MkdirAll(filepath.Dir(target), 0o755); err != nil {
+ t.Fatal(err)
+ }
+ if err := os.WriteFile(target, encoded, 0o644); err != nil {
+ t.Fatal(err)
+ }
+}
diff --git a/internal/command/requirementbrowser/assets/selection-authority.js b/internal/command/requirementbrowser/assets/selection-authority.js
index 2d1d905..d9e6daa 100644
--- a/internal/command/requirementbrowser/assets/selection-authority.js
+++ b/internal/command/requirementbrowser/assets/selection-authority.js
@@ -1,8 +1,8 @@
// @ts-check
/** @typedef {{anchorId: string, exactQuote: string, startCodePoint: number, endCodePoint: number}} SelectionTarget */
-/** @typedef {{mode: "none" | "button" | "text", targets: SelectionTarget[]}} SelectionState */
-/** @typedef {{kind: "button" | "text", targets: SelectionTarget[]} | {kind: "collapse" | "clear"}} SelectionEvent */
+/** @typedef {{mode: "none" | "button" | "text" | "committed_text", targets: SelectionTarget[]}} SelectionState */
+/** @typedef {{kind: "button" | "text", targets: SelectionTarget[]} | {kind: "collapse" | "commit" | "clear"}} SelectionEvent */
/** @returns {SelectionState} */
export function emptySelectionState() {
@@ -17,6 +17,8 @@ export function transitionSelection(state, event) {
return selectionState("button", event.targets);
case "text":
return event.targets.length === 0 ? emptySelectionState() : selectionState("text", event.targets);
+ case "commit":
+ return state.mode === "text" ? selectionState("committed_text", state.targets) : state;
case "collapse":
return state.mode === "text" ? emptySelectionState() : state;
case "clear":
@@ -24,7 +26,7 @@ export function transitionSelection(state, event) {
}
}
-/** @param {"button" | "text"} mode @param {SelectionTarget[]} targets @returns {SelectionState} */
+/** @param {"button" | "text" | "committed_text"} mode @param {SelectionTarget[]} targets @returns {SelectionState} */
function selectionState(mode, targets) {
return {mode, targets: targets.map((target) => ({...target}))};
}
diff --git a/internal/command/requirementbrowser/assets/workspace.css b/internal/command/requirementbrowser/assets/workspace.css
index c53b0ae..c410b74 100644
--- a/internal/command/requirementbrowser/assets/workspace.css
+++ b/internal/command/requirementbrowser/assets/workspace.css
@@ -9,6 +9,8 @@ button { min-height: 2.5rem; }
article { border-top: 1px solid color-mix(in srgb, CanvasText 25%, transparent); padding: .75rem 0; }
aside { border-left: 1px solid CanvasText; }
textarea { box-sizing: border-box; min-height: 8rem; width: 100%; }
+#selected-context { padding-left: 1.25rem; }
+#selected-context li { overflow-wrap: anywhere; }
pre { max-width: 100%; overflow: auto; white-space: pre-wrap; }
svg { display: block; min-width: 50rem; width: 100%; }
.graph-viewport { border: 1px solid color-mix(in srgb, CanvasText 35%, transparent); max-height: 42rem; overflow: auto; }
diff --git a/internal/command/requirementbrowser/assets/workspace.js b/internal/command/requirementbrowser/assets/workspace.js
index ebbb6c8..5148840 100644
--- a/internal/command/requirementbrowser/assets/workspace.js
+++ b/internal/command/requirementbrowser/assets/workspace.js
@@ -395,10 +395,25 @@ document.querySelectorAll("[data-view]").forEach((button) => button.addEventList
if (button.dataset.view === "graph") void renderGraph();
}));
+const questionInputElement = document.querySelector("#annotation-question");
+const statusElement = document.querySelector("#handoff-status");
+const packetElement = document.querySelector("#handoff-packet");
+const submitElement = document.querySelector("#submit-question");
+const selectedContextElement = document.querySelector("#selected-context");
+const clearSelectionElement = document.querySelector("#clear-selection");
+if (!(questionInputElement instanceof HTMLTextAreaElement) || !(statusElement instanceof HTMLElement) || !(packetElement instanceof HTMLElement) || !(submitElement instanceof HTMLButtonElement) || !(selectedContextElement instanceof HTMLUListElement) || !(clearSelectionElement instanceof HTMLButtonElement)) throw new Error("Missing handoff controls");
+const questionInput = /** @type {HTMLTextAreaElement} */ (questionInputElement);
+const status = /** @type {HTMLElement} */ (statusElement);
+const packetView = /** @type {HTMLElement} */ (packetElement);
+const submit = /** @type {HTMLButtonElement} */ (submitElement);
+const selectedContext = /** @type {HTMLUListElement} */ (selectedContextElement);
+const clearSelectionButton = /** @type {HTMLButtonElement} */ (clearSelectionElement);
+
document.addEventListener("selectionchange", () => {
const selection = window.getSelection();
if (!selection || selection.isCollapsed || selection.rangeCount !== 1) {
- const nextState = transitionSelection(selectionState, {kind: "collapse"});
+ const focusedHandoffControl = document.activeElement === questionInput || document.activeElement === submit || document.activeElement === clearSelectionButton;
+ const nextState = transitionSelection(selectionState, {kind: focusedHandoffControl ? "commit" : "collapse"});
if (nextState !== selectionState) {
selectionState = nextState;
resetPressedSelectionControls();
@@ -430,17 +445,10 @@ document.addEventListener("selectionchange", () => {
announceSelection();
});
-const questionInputElement = document.querySelector("#annotation-question");
-const statusElement = document.querySelector("#handoff-status");
-const packetElement = document.querySelector("#handoff-packet");
-const submitElement = document.querySelector("#submit-question");
-if (!(questionInputElement instanceof HTMLTextAreaElement) || !(statusElement instanceof HTMLElement) || !(packetElement instanceof HTMLElement) || !(submitElement instanceof HTMLButtonElement)) throw new Error("Missing handoff controls");
-const questionInput = /** @type {HTMLTextAreaElement} */ (questionInputElement);
-const status = /** @type {HTMLElement} */ (statusElement);
-const packetView = /** @type {HTMLElement} */ (packetElement);
-const submit = /** @type {HTMLButtonElement} */ (submitElement);
-
function announceSelection() {
+ selectedContext.replaceChildren();
+ appendTextItems(selectedContext, selectionState.targets.map((target) => target.exactQuote));
+ clearSelectionButton.disabled = selectionState.targets.length === 0;
status.textContent = selectionState.targets.length === 0 ? "No source-bound text selected." : `${selectionState.targets.length} source-bound target(s) selected.`;
}
@@ -452,9 +460,23 @@ function clearSelection() {
selectionState = transitionSelection(selectionState, {kind: "clear"});
resetPressedSelectionControls();
const selection = window.getSelection();
- if (selection && !selection.isCollapsed) selection.removeAllRanges();
- status.textContent = "No source-bound text selected.";
+ selection?.removeAllRanges();
+ announceSelection();
+}
+
+function commitSelection() {
+ const nextState = transitionSelection(selectionState, {kind: "commit"});
+ if (nextState !== selectionState) {
+ selectionState = nextState;
+ announceSelection();
+ }
+}
+
+for (const control of [questionInput, submit]) {
+ control.addEventListener("pointerdown", commitSelection);
+ control.addEventListener("focus", commitSelection);
}
+clearSelectionButton.addEventListener("click", clearSelection);
submit.addEventListener("click", async () => {
if (submit.disabled) return;
const question = questionInput.value.trim();
@@ -475,4 +497,5 @@ submit.addEventListener("click", async () => {
}
});
+announceSelection();
void renderSpecifications();
diff --git a/internal/command/requirementbrowser/server.go b/internal/command/requirementbrowser/server.go
index 69f9b58..14d3651 100644
--- a/internal/command/requirementbrowser/server.go
+++ b/internal/command/requirementbrowser/server.go
@@ -153,30 +153,19 @@ func Serve(ctx context.Context, raw any, options Options, stdout io.Writer) erro
if err != nil {
return err
}
+ return serveHandle(ctx, handle, options, stdout)
+}
+
+func serveHandle(ctx context.Context, handle ServerHandle, options Options, stdout io.Writer) error {
+ if options.SessionMode == "one-shot-question" {
+ return serveOneShot(ctx, handle, options, stdout)
+ }
defer func() { _ = closeHandle(handle) }()
if options.Open {
if err := openBrowser(ctx, handle.URL); err != nil {
return err
}
}
- if options.SessionMode == "one-shot-question" {
- timeout := options.SessionTimeout
- if timeout == 0 {
- timeout = 30 * time.Minute
- }
- timer := time.NewTimer(timeout)
- defer timer.Stop()
- select {
- case packet := <-handle.Handoff:
- return writeOneShotPacket(stdout, packet, packet["state"] != "submitted")
- case <-timer.C:
- return commitOrReadTerminal(handle, terminalPacket("expired", handle), stdout)
- case <-ctx.Done():
- return commitOrReadTerminal(handle, terminalPacket("cancelled", handle), stdout)
- case err := <-handle.Done():
- return err
- }
- }
if _, err := fmt.Fprintf(stdout, "Proofkit requirement browser: %s\n", handle.URL); err != nil {
return err
}
@@ -191,12 +180,43 @@ func Serve(ctx context.Context, raw any, options Options, stdout io.Writer) erro
}
}
-func commitOrReadTerminal(handle ServerHandle, candidate map[string]any, stdout io.Writer) error {
+func serveOneShot(ctx context.Context, handle ServerHandle, options Options, stdout io.Writer) error {
+ if options.Open {
+ if err := openBrowser(ctx, handle.URL); err != nil {
+ return errors.Join(err, closeAndWaitServer(handle))
+ }
+ }
+ timeout := options.SessionTimeout
+ if timeout == 0 {
+ timeout = 30 * time.Minute
+ }
+ timer := time.NewTimer(timeout)
+ defer timer.Stop()
+ var packet map[string]any
+ select {
+ case packet = <-handle.Handoff:
+ case <-timer.C:
+ packet = commitOrReadTerminal(handle, terminalPacket("expired", handle))
+ case <-ctx.Done():
+ packet = commitOrReadTerminal(handle, terminalPacket("cancelled", handle))
+ case err := <-handle.Done():
+ return errors.Join(err, closeHandle(handle))
+ }
+ unsuccessful := packet["state"] != "submitted"
+ if cleanupErr := closeAndWaitServer(handle); cleanupErr != nil {
+ if unsuccessful {
+ return errors.Join(ErrOneShotTerminal, cleanupErr)
+ }
+ return cleanupErr
+ }
+ return writeOneShotPacket(stdout, packet, unsuccessful)
+}
+
+func commitOrReadTerminal(handle ServerHandle, candidate map[string]any) map[string]any {
if handle.terminal.TryCommit(candidate) {
- return writeOneShotPacket(stdout, candidate, true)
+ return candidate
}
- winner := <-handle.Handoff
- return writeOneShotPacket(stdout, winner, winner["state"] != "submitted")
+ return <-handle.Handoff
}
func terminalPacket(state string, handle ServerHandle) map[string]any {
@@ -254,6 +274,13 @@ func closeHandle(handle ServerHandle) error {
return handle.Close(ctx)
}
+func closeAndWaitServer(handle ServerHandle) error {
+ closeErr := closeHandle(handle)
+ waitCtx, cancel := context.WithTimeout(context.Background(), serverShutdownTimeout)
+ defer cancel()
+ return errors.Join(closeErr, waitServerDone(waitCtx, handle))
+}
+
func waitServerDone(ctx context.Context, handle ServerHandle) error {
select {
case err := <-handle.Done():
diff --git a/internal/command/requirementbrowser/server_test.go b/internal/command/requirementbrowser/server_test.go
index 4a30c44..2090d38 100644
--- a/internal/command/requirementbrowser/server_test.go
+++ b/internal/command/requirementbrowser/server_test.go
@@ -1,8 +1,10 @@
package requirementbrowser
import (
+ "bytes"
"context"
"encoding/json"
+ "errors"
"io"
"net"
"net/http"
@@ -349,6 +351,136 @@ func TestServerCloseForcesTerminationAfterGracefulDeadline(t *testing.T) {
}
}
+func TestServeOneShotWaitsForDoneBeforeWritingTerminalPacket(t *testing.T) {
+ handoff := make(chan map[string]any, 1)
+ handoff <- map[string]any{"state": "submitted"}
+ done := make(chan error, 1)
+ closeStarted := make(chan struct{})
+ closeCalls := 0
+ handle := ServerHandle{
+ Handoff: handoff,
+ close: func(context.Context) error {
+ closeCalls++
+ if closeCalls == 1 {
+ close(closeStarted)
+ }
+ return nil
+ },
+ done: done,
+ }
+ var stdout bytes.Buffer
+ result := make(chan error, 1)
+ go func() {
+ result <- serveHandle(t.Context(), handle, Options{SessionMode: "one-shot-question"}, &stdout)
+ }()
+ select {
+ case <-closeStarted:
+ case err := <-result:
+ t.Fatalf("Serve returned before cleanup started: %v", err)
+ case <-time.After(time.Second):
+ t.Fatal("Serve did not start cleanup")
+ }
+ if stdout.Len() != 0 {
+ t.Fatalf("stdout emitted before Done completed: %q", stdout.String())
+ }
+ select {
+ case err := <-result:
+ t.Fatalf("Serve returned before Done completed: %v", err)
+ default:
+ }
+ done <- nil
+ select {
+ case err := <-result:
+ if err != nil {
+ t.Fatalf("Serve() error = %v", err)
+ }
+ case <-time.After(time.Second):
+ t.Fatal("Serve did not return after Done completed")
+ }
+ if closeCalls != 1 {
+ t.Fatalf("Close calls = %d, want 1", closeCalls)
+ }
+ if got := stdout.String(); got != "{\"state\":\"submitted\"}\n" {
+ t.Fatalf("stdout = %q, want submitted packet", got)
+ }
+}
+
+func TestServeOneShotReturnsCleanupFailuresWithoutWritingTerminalPacket(t *testing.T) {
+ closeFailure := errors.New("close failure")
+ doneFailure := errors.New("done failure")
+ unreadDone := errors.New("unexpected second Done read")
+ handoff := make(chan map[string]any, 1)
+ handoff <- map[string]any{"state": "submitted"}
+ done := make(chan error, 2)
+ closeCalls := 0
+ handle := ServerHandle{
+ Handoff: handoff,
+ close: func(context.Context) error {
+ closeCalls++
+ done <- doneFailure
+ done <- unreadDone
+ return closeFailure
+ },
+ done: done,
+ }
+ var stdout bytes.Buffer
+ err := serveHandle(t.Context(), handle, Options{SessionMode: "one-shot-question"}, &stdout)
+ if !errors.Is(err, closeFailure) || !errors.Is(err, doneFailure) {
+ t.Fatalf("Serve() error = %v, want close and Done failures", err)
+ }
+ if stdout.Len() != 0 {
+ t.Fatalf("stdout emitted despite cleanup failure: %q", stdout.String())
+ }
+ if closeCalls != 1 {
+ t.Fatalf("Close calls = %d, want 1", closeCalls)
+ }
+ select {
+ case got := <-done:
+ if !errors.Is(got, unreadDone) {
+ t.Fatalf("Done first unread value = %v, want second-read sentinel", got)
+ }
+ default:
+ t.Fatal("Done was read more than once")
+ }
+}
+
+func TestServeOneShotDoesNotReadCompletedDoneTwice(t *testing.T) {
+ serveFailure := errors.New("serve failure")
+ closeFailure := errors.New("close failure")
+ unreadDone := errors.New("unexpected second Done read")
+ done := make(chan error, 2)
+ done <- serveFailure
+ done <- unreadDone
+ closeCalls := 0
+ handle := ServerHandle{
+ Handoff: make(chan map[string]any),
+ close: func(context.Context) error {
+ closeCalls++
+ return closeFailure
+ },
+ done: done,
+ }
+ var stdout bytes.Buffer
+ err := serveHandle(t.Context(), handle, Options{SessionMode: "one-shot-question"}, &stdout)
+ if !errors.Is(err, serveFailure) || !errors.Is(err, closeFailure) {
+ t.Fatalf("Serve() error = %v, want Serve and close failures", err)
+ }
+ if stdout.Len() != 0 {
+ t.Fatalf("stdout emitted after premature server completion: %q", stdout.String())
+ }
+ if closeCalls != 1 {
+ t.Fatalf("Close calls = %d, want 1", closeCalls)
+ }
+ select {
+ case got := <-done:
+ if !errors.Is(got, unreadDone) {
+ t.Fatalf("Done first unread value = %v, want second-read sentinel", got)
+ }
+ default:
+ t.Fatal("Done was read more than once")
+ }
+}
+
type readyWriter struct {
ready chan<- string
}
diff --git a/internal/command/requirementbrowser/workspace.go b/internal/command/requirementbrowser/workspace.go
index 4bb4fd0..a30ea77 100644
--- a/internal/command/requirementbrowser/workspace.go
+++ b/internal/command/requirementbrowser/workspace.go
@@ -222,7 +222,7 @@ func workspaceHTML(workspaceID string) string {
"",
"",
"",
- "",
+ "",
"