Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions docs/proofkit-contract-map.md
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,7 @@ Semantic context routes are `requirement-context-compose`,
| Does a TypeScript package public API match a caller-owned manifest? | `agent-route` with `goal: "verify_typescript_public_api"` and explicit `typescript_public_api_manifest` plus `typescript_public_api_repo_root`, then `typescript-public-api-surfaces --repo-root <caller-selected-root>` | The manifest must name each referenced `package.json`, sorted-unique export conditions, and a non-JSX `.ts`, `.mts`, or `.cts` `sourcePath` whose canonical target has the same admitted extension class. The bounded scanner accepts only the fail-closed export grammar in `proofkit/cli-contract.v2.json`; it does not parse unrestricted TypeScript or TSX, infer conventional layouts, or prove compiler output provenance, checkout freshness, package-manager truth, or merge readiness. |
| Receipts are available for planned checks. | `selective-gate-evidence --agent-envelope`; then materialize a caller-owned `obligation_decision_input` from the evidence output plus command routes, currentness, and trust facts; then run `selective-gate-obligation-decision-input`; then materialize the resulting `obligation_decision` input and run `obligation-decision --agent-envelope` | Escalate on missing, stale, invalid, untrusted, blocked, unavailable, or unknown-scope evidence. |
| Human inspection, semantic comparison, or traceability navigation is needed. | `requirement-source-view`, `requirement-proof-view`, `requirement-coverage-view`, `requirement-spec-tree-view`, `requirement-semantic-diff`, `requirement-traceability-graph`, or `requirement-browser-server` | Semantic diff compares admitted owner fields rather than lines. Traceability keeps specification, proof, code, and native execution evidence planes separate. Browser and rendered outputs remain presentation only unless the consumer admits a tracked artifact freshness gate. |
| Find a requirement in a large admitted workspace. | `requirement-browser-server --view workspace --serve --input <workspace-input>`; use Browse to select a descendant scope, owner, lifecycle, or literal search, then inspect the bounded result page. | Search covers the whole admitted cohort before paging, not just visible rows. Selection retains original source anchors; handoff adds context closure through its owner. Browse and Inspector become mutually exclusive native panels on smaller viewports. Retry preserves the failed operation, while stale snapshots require explicit reload. The browser does not execute agents or turn a lookup count into proof coverage. |
| Temporary external document lifecycle facts, generated views, or rendered views need authority classification. | `document-lifecycle-boundary` | Treat lifecycle records as caller-owned metadata. Temporary design docs and implementation plans are not retained repository authority unless rewritten into deterministic specs, proof bindings, tests, package-public docs, or backlog rows. |
| A JavaScript/TypeScript consumer needs less wrapper code. | `json-report-cli-adapter-source --language typescript --format json` | Generated adapter source is caller-owned after materialization. The consumer still owns package pin, binary path, repo paths, local policy, and freshness proof. It is a CLI runner adapter, not a separate SDK authority. |
| A Python consumer needs Proofkit from Python tooling. | Install the Python package when available and invoke the same CLI/JSON contract. | The Python package is a runner wrapper over the Go CLI, not a Python SDK or alternate schema owner. |
Expand Down
7 changes: 7 additions & 0 deletions docs/specs/proofkit-spec-proof-core/overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -207,6 +207,13 @@ execution receipts, and merge policy.
change-plan route replacement, and omitted-route policy to one breaking
release record without reinterpreting the frozen prior edge.

- `REQ-PROOFKIT-SPEC-036`: full-cohort requirement lookup intersects literal
search, owner, lifecycle, and typed descendant scope before byte-bounded
paging; navigation and handoff preserve their distinct identities and closure.
- `REQ-PROOFKIT-SPEC-037`: generation-owned requests, exact explicit Retry,
distinct error actions, and responsive native panels preserve keyboard
focus, source selection, and drafts without promoting presentation authority.

## Non-Claims

- This spec does not claim consumer repository adoption.
Expand Down
26 changes: 26 additions & 0 deletions docs/specs/proofkit-spec-proof-core/requirements.v1.json
Original file line number Diff line number Diff line change
Expand Up @@ -711,6 +711,32 @@
"lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
"deferral": null,
"updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
},
{
"requirementId": "REQ-PROOFKIT-SPEC-036",
"ownerId": "proofkit.spec-proof-core",
"invariant": "Workspace lookup indexes immutable admitted requirement sources once, preserves each original source digest and snapshot JSON pointer, and intersects search, owner, lifecycle, and selected-node descendant scope before stable requirement-ID paging. Scope uses only requirement-role source-ID references, never overview or path-digest aliases or inferred ancestor membership. Search applies Unicode trimming and simple lowercase independently to ID, owner, and invariant, without normalization or cross-field concatenation, after 1024-byte and 256-code-point admission bounds. Available A, matching M, and selected S counts yield filtered A-M, page-omitted M-S, and total-omitted A-S counts. Lookup does not expand lifecycle closure; handoff delegates closure to the existing context owner. Navigation projects only the root or one admitted parent's ordered child window; both lookup routes cap compact response bytes at 16 MiB without truncating invariant text and reject an unfit first row before output. Browser navigation retains at most 256 rows with explicit recovery of discarded sibling pages, while requirement paging returns to actual visited offsets rather than assuming fixed response length.",
"claimLevel": "blocking",
"riskClass": "high",
"proofBindingRefs": ["proofkit/requirement-bindings.json"],
"nonClaimRefs": ["NC-PROOFKIT-SPEC-036"],
"nonClaims": ["Lookup fragments do not establish source completeness outside the admitted snapshot, lifecycle-closed context, proof coverage, native execution, provider freshness, merge approval, or production readiness. Private browser HTTP routes are not a separately supported public SDK."],
"lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
"deferral": null,
"updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
},
{
"requirementId": "REQ-PROOFKIT-SPEC-037",
"ownerId": "proofkit.spec-proof-core",
"invariant": "The workspace has one content-generation owner and independent identity-bound navigation requests. Superseded, aborted, or collapsed-branch replies cannot replace current content, selection, focus, or request authority. Retry requires explicit activation and repeats the immutable failed method, route, snapshot, and complete query with a new request ID; unsent form edits do not alter it. Sanitized errors distinguish correction (400), denied and locked without Retry (403), stale and locked with explicit reload (409), explicit Retry for transport/429/5xx, and optional versus required unavailability (404). Responsive panels use one native modal at a time at or below 64rem, restore visible opener focus on close, and release modality on desktop resize while preserving the question draft. Inspector entry commits source selection before moving focus; content transitions clear targets and displayed packets. Navigation render commits preserve a focused node/action identity and derive protected-control state from current authority. Native page focus stays inside the open modal without trapping browser chrome. Invariants precede lazily expanded owner/non-claim details and remain source-bound through Unicode selection and handoff.",
"claimLevel": "blocking",
"riskClass": "high",
"proofBindingRefs": ["proofkit/requirement-bindings.json"],
"nonClaimRefs": ["NC-PROOFKIT-SPEC-037"],
"nonClaims": ["Browser runtime witnesses cover the admitted Playwright Chromium, Firefox, and WebKit scenarios, not all browser preferences, assistive technologies, operating-system themes, branded Safari behavior, complete WCAG conformance, annotation persistence, agent execution, or provider delivery."],
"lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
"deferral": null,
"updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
}
],
"nonClaims": [
Expand Down
2 changes: 1 addition & 1 deletion internal/app/cli_contract_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import (
)

const (
cliContractPublicABISHA256 = "527ffbc7e261d4ac0f91cc81db0a390ec5aa2c4f18593671bbc1f92f3ed83c70"
cliContractPublicABISHA256 = "679a9152618bff6c848bacea0aaf2ae09bef24f7d6176add1733248a287225ae"
maxAggregateFileReadBytesForContractTest = 64 << 20
maxPackageManifestBytesForContractTest = 256 << 10
maxSourceFileBytesForContractTest = 8 << 20
Expand Down
4 changes: 2 additions & 2 deletions internal/app/command_contract_generated.go

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

12 changes: 12 additions & 0 deletions internal/command/requirementbrowser/assets.go
Original file line number Diff line number Diff line change
Expand Up @@ -8,5 +8,17 @@ var workspaceJavaScript []byte
//go:embed assets/selection-authority.js
var selectionAuthorityJavaScript []byte

//go:embed assets/workspace-icons.js
var workspaceIconsJavaScript []byte

//go:embed assets/workspace-panels.js
var workspacePanelsJavaScript []byte

//go:embed assets/workspace-requests.js
var workspaceRequestsJavaScript []byte

//go:embed assets/workspace-navigation.js
var workspaceNavigationJavaScript []byte

//go:embed assets/workspace.css
var workspaceCSS []byte
Loading
Loading