From d83287f41c8a5e6f006fdd09f97a86ee1ae6d800 Mon Sep 17 00:00:00 2001 From: iperev Date: Sun, 6 Sep 2026 15:59:31 +0200 Subject: [PATCH 1/5] feat: add bounded browser evidence inspection --- .../proofkit-spec-proof-core/overview.md | 10 + .../requirements.v1.json | 52 +++ internal/command/requirementbrowser/assets.go | 15 + .../assets/workspace-coverage.js | 113 ++++++ .../assets/workspace-diff.js | 66 ++++ .../assets/workspace-graph.js | 301 ++++++++++++++ .../assets/workspace-handoff.js | 135 +++++++ .../assets/workspace-icons.js | 2 + .../assets/workspace-json.js | 20 + .../assets/workspace-panels.js | 23 +- .../assets/workspace-requests.js | 9 +- .../requirementbrowser/assets/workspace.css | 50 ++- .../requirementbrowser/assets/workspace.js | 289 ++++++-------- .../requirementbrowser/http_handler.go | 51 ++- .../command/requirementbrowser/server_test.go | 118 +----- .../command/requirementbrowser/workspace.go | 7 +- .../requirementbrowser/workspace_coverage.go | 45 +++ .../workspace_coverage_test.go | 202 ++++++++++ .../workspace_graph_test.go | 104 +++++ .../requirementbrowser/workspace_lookup.go | 7 +- .../workspace_lookup_admission_test.go | 5 + .../requirementbrowser/workspace_page.go | 2 +- .../requirementbrowser/workspace_test.go | 5 +- .../output_admission.go | 12 + .../requirementgraph/reference_projection.go | 30 ++ .../reference_projection_test.go | 28 ++ .../testsupport/browserfixture/coverage.go | 254 ++++++++++++ internal/testsupport/browserfixture/graph.go | 58 +++ internal/tools/browsertestserver/main.go | 10 + package-lock.json | 4 +- package.json | 4 +- proofkit/requirement-bindings.json | 210 ++++++++++ proofkit/witness-plan.json | 1 + release/change-record.v2.json | 18 +- scripts/browser-evidence-models.test.mjs | 81 ++++ scripts/browser-runtime-proof-inputs.v1.json | 1 + scripts/browser-workspace-requests.test.mjs | 60 ++- .../workspace-evidence-layout.spec.mjs | 61 +++ tests/browser/workspace-evidence.spec.mjs | 226 +++++++++++ tests/browser/workspace-graph.spec.mjs | 165 ++++++++ tests/browser/workspace-locking.spec.mjs | 73 +++- tests/browser/workspace-paging.spec.mjs | 17 +- tests/browser/workspace-test-harness.mjs | 8 + tests/browser/workspace.spec.mjs | 370 ++++-------------- 44 files changed, 2690 insertions(+), 632 deletions(-) create mode 100644 internal/command/requirementbrowser/assets/workspace-coverage.js create mode 100644 internal/command/requirementbrowser/assets/workspace-diff.js create mode 100644 internal/command/requirementbrowser/assets/workspace-graph.js create mode 100644 internal/command/requirementbrowser/assets/workspace-handoff.js create mode 100644 internal/command/requirementbrowser/assets/workspace-json.js create mode 100644 internal/command/requirementbrowser/workspace_coverage.go create mode 100644 internal/command/requirementbrowser/workspace_coverage_test.go create mode 100644 internal/command/requirementbrowser/workspace_graph_test.go create mode 100644 internal/command/requirementgraph/reference_projection.go create mode 100644 internal/command/requirementgraph/reference_projection_test.go create mode 100644 internal/testsupport/browserfixture/coverage.go create mode 100644 internal/testsupport/browserfixture/graph.go create mode 100644 scripts/browser-evidence-models.test.mjs create mode 100644 tests/browser/workspace-evidence-layout.spec.mjs create mode 100644 tests/browser/workspace-evidence.spec.mjs create mode 100644 tests/browser/workspace-graph.spec.mjs diff --git a/docs/specs/proofkit-spec-proof-core/overview.md b/docs/specs/proofkit-spec-proof-core/overview.md index 0a30e36..f122bb7 100644 --- a/docs/specs/proofkit-spec-proof-core/overview.md +++ b/docs/specs/proofkit-spec-proof-core/overview.md @@ -214,6 +214,16 @@ execution receipts, and merge policy. distinct error actions, and responsive native panels preserve keyboard focus, source selection, and drafts without promoting presentation authority. +- `REQ-PROOFKIT-SPEC-038`: Coverage joins the complete lookup cohort to admitted + coverage rows, preserves both proof modes and the shared fragment contract, + and never interprets an absent row as a failed requirement. +- `REQ-PROOFKIT-SPEC-039`: graph inspection preserves primary and boundary sets, + typed off-page references, evidence planes and accessible bounded navigation. +- `REQ-PROOFKIT-SPEC-040`: handoff preview and explicit export preserve exact + server bytes, source identity, drafts and independent generation/lock state. +- `REQ-PROOFKIT-SPEC-041`: diff summaries count only admitted page changes and + retain distinct global counts, source identities and full disclosed values. + ## Non-Claims - This spec does not claim consumer repository adoption. diff --git a/docs/specs/proofkit-spec-proof-core/requirements.v1.json b/docs/specs/proofkit-spec-proof-core/requirements.v1.json index 57b1242..8ee03e5 100644 --- a/docs/specs/proofkit-spec-proof-core/requirements.v1.json +++ b/docs/specs/proofkit-spec-proof-core/requirements.v1.json @@ -737,6 +737,58 @@ "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []}, "deferral": null, "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true} + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-038", + "ownerId": "proofkit.spec-proof-core", + "invariant": "Workspace Coverage uses the admitted lookup cohort and a left join to owner-admitted coverage rows. Matching reported and not-reported counts partition the complete filtered requirement cohort before bounded paging; an absent projection, a zero-row projection and a missing row remain distinct. Missing rows are Not reported, never inferred failures. One child membership count and one batched detached selection preserve complete compact and structured row fields without cloning the full matching cohort. The shared seven-key coverage fragment and existing review-context and handoff projections remain unchanged; only the new private browser response copies proofMode from the admitted full report. Whole rows and original anchors survive the 16 MiB page bound. Coverage filters refresh Coverage. Ask about evidence commits the explicit source anchor, shows the existing inspector idempotently and prefills only an exactly empty question; no draft is overwritten or submitted, and locked or pending actions remain unavailable.", + "claimLevel": "blocking", + "riskClass": "high", + "proofBindingRefs": ["proofkit/requirement-bindings.json"], + "nonClaimRefs": ["NC-PROOFKIT-SPEC-038"], + "nonClaims": ["Coverage presentation does not execute witnesses, authenticate declared evidence, infer a verdict for absent rows, or approve merge, release, rollout or production readiness."], + "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []}, + "deferral": null, + "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true} + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "ownerId": "proofkit.spec-proof-core", + "invariant": "Workspace graph inspection preserves the graph owner's node, edge and evidence-plane identities, primary-window and incident-edge selection, and endpoint boundary closure. The page exposes exact primary IDs and child-owned typed parentNodeId, fromNodeId, toNodeId and codeNodeId references with canonical target offsets and included or outside_page dispositions. Structural references do not infer edges or recursively fetch ancestors. Explicit target following resets local filters and relation offset and selects only a current-generation returned target. The default browser window requests 64 primary nodes and 128 incident edges, admitting at most 192 returned nodes. Plane filtering retains edges only with visible endpoints; selected-node neighborhood shows undirected distance-one neighbors and their induced directed edges, preserving parallel identities. Hidden selection clears selection and neighborhood with visible focus recovery. Global, returned-page and visible counts remain distinct. Source coordinate text preserves exact admitted numeric tokens, including unverified ranges beyond JavaScript's safe integer domain; missing native precision support yields a sanitized unavailable view rather than rounded values. Deterministic bounded layout and keyboard-accessible records preserve inspectability without witness or source-edit authority.", + "claimLevel": "blocking", + "riskClass": "high", + "proofBindingRefs": ["proofkit/requirement-bindings.json"], + "nonClaimRefs": ["NC-PROOFKIT-SPEC-039"], + "nonClaims": ["A displayed topology, local filter or layout is not evidence of source completeness, proof truth, native execution, publication, rollout or production readiness. Browser-emulated mobile interaction does not certify physical devices or operating-system behavior."], + "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []}, + "deferral": null, + "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true} + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-040", + "ownerId": "proofkit.spec-proof-core", + "invariant": "A workspace question packet keeps the existing source-bound handoff structure, Unicode code-point coordinates and immutable snapshot authority while using compact server-owned JSON bytes. One request acquisition retains the raw response text separately from the parsed preview. Explicit copy and download use the exact original text including its final newline, never reserialization of parsed JavaScript numbers. Preview detail resolves exactly one included requirement by annotation.anchor.requirementId, not targetId or original-file array index; missing or ambiguous detail stays unavailable. A content-generation transition clears preview and export and rejects obsolete success or failure carriers, while independent POST exclusion releases only on settlement and cannot clear a request lock. Late clipboard effects cannot label a replacement packet. Denied clipboard or export preserves the draft and exact-text fallback; download URLs are cleaned up. No browser operation rereads live source or promotes the packet to proof authority.", + "claimLevel": "blocking", + "riskClass": "high", + "proofBindingRefs": ["proofkit/requirement-bindings.json"], + "nonClaimRefs": ["NC-PROOFKIT-SPEC-040"], + "nonClaims": ["A question packet does not establish live checkout freshness, native witness execution, agent delivery, annotation persistence, merge approval or production readiness. Already exported bytes are not revoked by later view changes."], + "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []}, + "deferral": null, + "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true} + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-041", + "ownerId": "proofkit.spec-proof-core", + "invariant": "Workspace semantic diff summaries derive only from the admitted returned change page: change count, distinct entity count and the exact change-class partition. Risk changes count only scalar changes at the exact riskClass field pointer; record addition or removal containing risk data is not a risk transition. Lifecycle changes use the owner change class. Risk and lifecycle are overlapping facets, not an asserted partition. Page summaries remain distinct from available, selected and omitted change counts and both source snapshot identities. Full before and after values remain available through disclosure without reinterpreting scalar, set, map, lifecycle or entity semantics or inventing a breaking-change verdict.", + "claimLevel": "blocking", + "riskClass": "high", + "proofBindingRefs": ["proofkit/requirement-bindings.json"], + "nonClaimRefs": ["NC-PROOFKIT-SPEC-041"], + "nonClaims": ["Diff counts, risk labels and presentation do not determine compatibility, source authenticity, witness truth, merge approval, publication or production readiness."], + "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []}, + "deferral": null, + "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true} } ], "nonClaims": [ diff --git a/internal/command/requirementbrowser/assets.go b/internal/command/requirementbrowser/assets.go index 8e6cddf..7c17470 100644 --- a/internal/command/requirementbrowser/assets.go +++ b/internal/command/requirementbrowser/assets.go @@ -17,8 +17,23 @@ var workspacePanelsJavaScript []byte //go:embed assets/workspace-requests.js var workspaceRequestsJavaScript []byte +//go:embed assets/workspace-json.js +var workspaceJSONJavaScript []byte + //go:embed assets/workspace-navigation.js var workspaceNavigationJavaScript []byte +//go:embed assets/workspace-coverage.js +var workspaceCoverageJavaScript []byte + +//go:embed assets/workspace-diff.js +var workspaceDiffJavaScript []byte + +//go:embed assets/workspace-graph.js +var workspaceGraphJavaScript []byte + +//go:embed assets/workspace-handoff.js +var workspaceHandoffJavaScript []byte + //go:embed assets/workspace.css var workspaceCSS []byte diff --git a/internal/command/requirementbrowser/assets/workspace-coverage.js b/internal/command/requirementbrowser/assets/workspace-coverage.js new file mode 100644 index 0000000..2ccf9ac --- /dev/null +++ b/internal/command/requirementbrowser/assets/workspace-coverage.js @@ -0,0 +1,113 @@ +// @ts-check + +import {icon} from "./workspace-icons.js"; + +/** @param {HTMLElement} container @param {any} projection @param {(requirement: any, opener: HTMLButtonElement) => void} ask */ +export function renderCoveragePage(container, projection, ask) { + const summary = document.createElement("p"); + summary.className = "page-summary"; + summary.dataset.coverageSummary = ""; + summary.textContent = `${projection.matchingReportedRequirementCount} reported; ${projection.matchingNotReportedRequirementCount} not reported in ${projection.matchingRequirementCount} matching requirements. Mode: ${projection.proofMode}.`; + container.append(summary); + const list = document.createElement("ul"); + list.className = "coverage-matrix"; + list.setAttribute("aria-label", "Requirement coverage"); + for (const requirement of projection.requirements) { + const row = requirement.coverage; + const item = document.createElement("li"); + const article = document.createElement("article"); + article.className = "coverage-record"; + article.dataset.requirementId = requirement.requirementId; + const identity = document.createElement("div"); + const title = document.createElement("h3"); + title.className = "caller-text"; + title.textContent = requirement.requirementId; + const invariant = document.createElement("p"); + invariant.className = "caller-text"; + invariant.dataset.anchorId = requirement.anchor.anchorId; + invariant.textContent = requirement.invariant; + identity.append(title, invariant); + const state = document.createElement("dl"); + state.className = "coverage-state"; + addField(state, "Coverage", row === null ? "Not reported" : row.coverageState); + if (row !== null) { + addField(state, "Evidence class", row.evidenceClass); + addField(state, "Claim", row.claimLevel); + addField(state, "Lifecycle", row.lifecycleState); + addField(state, "Scenarios", String(row.scenarioCount)); + addField(state, "Tests", String(row.tests.length)); + addField(state, projection.proofMode === "compact" ? "Declared routes" : "Witness references", String(projection.proofMode === "compact" ? row.declaredWitnessRoutes.length : row.witnessRefs.length)); + } + const actions = document.createElement("div"); + actions.className = "coverage-actions"; + const question = document.createElement("button"); + question.type = "button"; + question.dataset.protectedRequest = ""; + question.dataset.evidenceQuestion = ""; + question.append(icon("message-square"), document.createTextNode("Ask about evidence")); + question.addEventListener("click", () => { if (!question.disabled) ask(requirement, question); }); + actions.append(question); + const details = document.createElement("details"); + details.className = "coverage-details"; + const label = document.createElement("summary"); + label.textContent = "Declared evidence and boundaries"; + details.append(label); + details.addEventListener("toggle", () => { + if (!details.open || details.querySelector("[data-coverage-detail]")) return; + const body = document.createElement("div"); + body.dataset.coverageDetail = ""; + const ownership = document.createElement("p"); + ownership.className = "caller-text"; + ownership.textContent = `Owner: ${requirement.ownerId}.`; + body.append(ownership); + if (row !== null) { + const fields = document.createElement("dl"); + for (const [name, values] of [["Commands", row.commandIds], ["Environments", row.environmentClasses], ["Verify commands", row.verifyCommands], ["Failures", row.failures]]) addField(fields, name, values.length === 0 ? "None reported" : values.join("\n")); + body.append(fields); + if (projection.proofMode === "structured") { + const proof = document.createElement("p"); + proof.textContent = `Proof state: ${row.proofState}.`; + body.append(proof); + } + for (const [name, values] of [["Scenarios", row.scenarios], ["Tests", row.tests], [projection.proofMode === "compact" ? "Declared witness routes" : "Witness references", projection.proofMode === "compact" ? row.declaredWitnessRoutes : row.witnessRefs]]) { + const group = document.createElement("details"); + const summary = document.createElement("summary"); + summary.textContent = `${name} (${values.length})`; + const records = document.createElement("pre"); + // Secondary owner records retain nested oracle and falsifier fields. + records.textContent = JSON.stringify(values, null, 2); + group.append(summary, records); + body.append(group); + } + } + const boundaries = document.createElement("ul"); + for (const text of [...requirement.sourceNonClaims, ...requirement.nonClaims, ...(row?.nonClaims ?? [])]) { + const entry = document.createElement("li"); + entry.className = "caller-text"; + entry.textContent = text; + boundaries.append(entry); + } + body.append(boundaries); + details.append(body); + }); + article.append(identity, state, actions, details); + item.append(article); + list.append(item); + } + if (projection.requirements.length === 0) { + const empty = document.createElement("p"); + empty.textContent = "No requirements matched the admitted query."; + container.append(empty); + } + container.append(list); +} + +/** @param {HTMLDListElement} list @param {string} label @param {string} text */ +function addField(list, label, text) { + const term = document.createElement("dt"); + term.textContent = label; + const value = document.createElement("dd"); + value.className = "caller-text"; + value.textContent = text; + list.append(term, value); +} diff --git a/internal/command/requirementbrowser/assets/workspace-diff.js b/internal/command/requirementbrowser/assets/workspace-diff.js new file mode 100644 index 0000000..b1744de --- /dev/null +++ b/internal/command/requirementbrowser/assets/workspace-diff.js @@ -0,0 +1,66 @@ +// @ts-check + +/** @param {any[]} changes */ +export function summarizeDiffPage(changes) { + const entities = new Set(); + /** @type {Map} */ + const classes = new Map(); + let riskChanges = 0; + let lifecycleChanges = 0; + for (const change of changes) { + entities.add(change.entityId); + classes.set(change.changeClass, (classes.get(change.changeClass) ?? 0) + 1); + const entityPointer = String(change.entityId).replaceAll("~", "~0").replaceAll("/", "~1"); + if (change.entityKind === "requirement" && change.changeClass === "scalar_changed" && change.jsonPointer === `/requirements/${entityPointer}/riskClass`) riskChanges++; + if (change.changeClass === "lifecycle_transition") lifecycleChanges++; + } + return { + changeCount: changes.length, entityCount: entities.size, riskChanges, lifecycleChanges, + byClass: [...classes].sort(([left], [right]) => left < right ? -1 : left > right ? 1 : 0), + }; +} + +/** @param {HTMLElement} container @param {any[]} changes */ +export function renderDiffPage(container, changes) { + const summary = summarizeDiffPage(changes); + const heading = document.createElement("h3"); + heading.textContent = "Changes on this page"; + const counts = document.createElement("p"); + counts.className = "page-summary"; + counts.dataset.diffSummary = ""; + counts.textContent = `Changes: ${summary.changeCount}; requirements: ${summary.entityCount}; risk changes: ${summary.riskChanges}; lifecycle changes: ${summary.lifecycleChanges}.`; + const partition = document.createElement("ul"); + partition.className = "diff-class-counts"; + partition.setAttribute("aria-label", "Change classes on this page"); + for (const [kind, count] of summary.byClass) { + const item = document.createElement("li"); + item.textContent = `${kind}: ${count}`; + partition.append(item); + } + container.append(heading, counts, partition); + for (const change of changes) { + const article = document.createElement("article"); + article.dataset.changeId = change.changeId; + const title = document.createElement("h3"); + title.textContent = `${change.changeClass}: ${change.entityId}`; + title.className = "caller-text"; + const pointer = document.createElement("p"); + pointer.className = "caller-text"; + pointer.textContent = change.jsonPointer; + const details = document.createElement("details"); + const label = document.createElement("summary"); + label.textContent = "Before and after"; + details.append(label); + details.addEventListener("toggle", () => { + if (!details.open || details.querySelector("pre")) return; + const identity = document.createElement("p"); + identity.className = "caller-text"; + identity.textContent = `Source digests: ${change.baseSourceDigest ?? "not-recorded"} -> ${change.currentSourceDigest ?? "not-recorded"}`; + const values = document.createElement("pre"); + values.textContent = `${JSON.stringify(change.before, null, 2)}\n->\n${JSON.stringify(change.after, null, 2)}`; + details.append(identity, values); + }); + article.append(title, pointer, details); + container.append(article); + } +} diff --git a/internal/command/requirementbrowser/assets/workspace-graph.js b/internal/command/requirementbrowser/assets/workspace-graph.js new file mode 100644 index 0000000..15b22e8 --- /dev/null +++ b/internal/command/requirementbrowser/assets/workspace-graph.js @@ -0,0 +1,301 @@ +// @ts-check + +import {icon} from "./workspace-icons.js"; +import {workspaceScalarText} from "./workspace-json.js"; + +export const GRAPH_PAGE = Object.freeze({maxRecords: 64, maxEdges: 128}); +export const GRAPH_PLANES = Object.freeze([ + {id: "specification_coverage", label: "Specifications"}, + {id: "proof_coverage", label: "Proof declarations"}, + {id: "code_traceability", label: "Code"}, + {id: "native_execution_coverage", label: "Native execution"}, +]); + +/** @param {{nodes: any[], edges: any[]}} graph @param {Set} planes @param {string | null} selectedId @param {boolean} neighborhood */ +export function visibleGraphPage(graph, planes, selectedId, neighborhood) { + let nodes = graph.nodes.filter(node => planes.has(node.evidencePlane)); + const admittedIDs = new Set(nodes.map(node => node.nodeId)); + let edges = graph.edges.filter(edge => planes.has(edge.evidencePlane) && admittedIDs.has(edge.fromNodeId) && admittedIDs.has(edge.toNodeId)); + if (!admittedIDs.has(selectedId)) { selectedId = null; neighborhood = false; } + if (neighborhood && selectedId !== null) { + const neighbors = new Set([selectedId]); + for (const edge of edges) { + if (edge.fromNodeId === selectedId) neighbors.add(edge.toNodeId); + if (edge.toNodeId === selectedId) neighbors.add(edge.fromNodeId); + } + nodes = nodes.filter(node => neighbors.has(node.nodeId)); + edges = edges.filter(edge => neighbors.has(edge.fromNodeId) && neighbors.has(edge.toNodeId)); + } + return {nodes, edges, selectedId, neighborhood}; +} + +/** @param {any[]} nodes */ +export function graphPagePositions(nodes) { + const rows = [0, 0, 0, 0]; + /** @type {Map} */ + const positions = new Map(); + const ordered = [...nodes].sort((a, b) => a.nodeId < b.nodeId ? -1 : a.nodeId > b.nodeId ? 1 : 0); + for (const node of ordered) { + const column = GRAPH_PLANES.findIndex(plane => plane.id === node.evidencePlane); + if (column < 0) throw new Error("Unknown admitted evidence plane"); + positions.set(node.nodeId, {x: 12 + column * 260, y: 48 + rows[column]++ * 116}); + } + return {positions, width: 1040, height: Math.max(180, 60 + Math.max(...rows) * 116)}; +} + +/** @param {HTMLElement} container @param {any} graph @param {{follow: (offset: number, id: string) => void, reconcile: () => void, initialId?: string | null}} options */ +export function renderGraphPage(container, graph, options) { + let planes = new Set(GRAPH_PLANES.map(plane => plane.id)); + let selectedId = options.initialId ?? null; + let neighborhood = false; + const primaryIDs = new Set(graph.primaryNodeIds); + const controls = document.createElement("fieldset"); + controls.className = "graph-filters"; + const legend = document.createElement("legend"); + legend.textContent = "Evidence planes"; + controls.append(legend); + /** @type {Map} */ + const checkboxes = new Map(); + for (const plane of GRAPH_PLANES) { + const label = document.createElement("label"); + const checkbox = document.createElement("input"); + checkbox.type = "checkbox"; + checkbox.checked = true; + checkboxes.set(plane.id, checkbox); + checkbox.addEventListener("change", () => { + if (checkbox.checked) planes.add(plane.id); else planes.delete(plane.id); + update(checkbox); + }); + label.append(checkbox, document.createTextNode(plane.label)); + controls.append(label); + } + const neighborhoodLabel = document.createElement("label"); + const neighborhoodInput = document.createElement("input"); + neighborhoodInput.type = "checkbox"; + neighborhoodInput.addEventListener("change", () => { neighborhood = neighborhoodInput.checked; update(neighborhoodInput); }); + neighborhoodLabel.append(neighborhoodInput, document.createTextNode("Selected node and neighbors")); + controls.append(neighborhoodLabel); + const counts = document.createElement("p"); + counts.className = "page-summary"; + counts.dataset.graphCounts = ""; + const announcement = document.createElement("p"); + announcement.setAttribute("role", "status"); + announcement.setAttribute("aria-live", "polite"); + const viewport = document.createElement("div"); + viewport.className = "graph-viewport"; + viewport.setAttribute("role", "region"); + viewport.setAttribute("aria-label", "Traceability graph viewport"); + viewport.tabIndex = 0; + const inspector = document.createElement("section"); + inspector.className = "graph-inspector"; + inspector.setAttribute("aria-label", "Selected graph node"); + const records = document.createElement("details"); + records.className = "graph-records"; + records.open = true; + const recordLabel = document.createElement("summary"); + recordLabel.textContent = "Node and relation records"; + records.append(recordLabel); + const recordBody = document.createElement("div"); + records.append(recordBody); + container.append(controls, counts, announcement, viewport, inspector, records); + + /** @param {string} id @param {boolean} [reveal] */ + function select(id, reveal = false) { + if (reveal) { + planes = new Set(GRAPH_PLANES.map(plane => plane.id)); + for (const checkbox of checkboxes.values()) checkbox.checked = true; + neighborhood = false; + } + selectedId = id; + update(undefined, id); + } + + /** @param {HTMLElement} [fallback] @param {string} [focusTarget] */ + function update(fallback, focusTarget) { + const start = performance.now(); + const focused = document.activeElement; + const focusedNode = focusTarget ?? (focused instanceof HTMLElement ? focused.dataset.graphSelect : undefined); + const recordFocused = focused !== null && (recordBody.contains(focused) || inspector.contains(focused)); + const oldSelection = selectedId; + const visible = visibleGraphPage(graph, planes, selectedId, neighborhood); + selectedId = visible.selectedId; + neighborhood = visible.neighborhood; + neighborhoodInput.checked = neighborhood; + neighborhoodInput.disabled = selectedId === null; + if (oldSelection !== null && selectedId === null) announcement.textContent = "Selection cleared by evidence-plane filters."; + else announcement.textContent = selectedId === null ? "No node selected." : `Selected ${selectedId}.`; + counts.textContent = `Available: ${graph.availableNodeCount} nodes, ${graph.availableEdgeCount} relations. Returned page: ${graph.primaryNodeCount} primary and ${graph.boundaryNodeCount} boundary nodes, ${graph.selectedEdgeCount} relations. Visible in this returned page: ${visible.nodes.length} nodes, ${visible.edges.length} relations.`; + const {positions, width, height} = graphPagePositions(visible.nodes); + const canvas = document.createElement("div"); + canvas.className = "graph-canvas"; + canvas.style.width = `${width}px`; + canvas.style.height = `${height}px`; + for (let column = 0; column < GRAPH_PLANES.length; column++) { + const heading = document.createElement("p"); + heading.className = "graph-plane-heading"; + heading.textContent = GRAPH_PLANES[column].label; + heading.style.left = `${12 + column * 260}px`; + canvas.append(heading); + } + const svg = document.createElementNS("http://www.w3.org/2000/svg", "svg"); + svg.setAttribute("aria-hidden", "true"); + svg.setAttribute("viewBox", `0 0 ${width} ${height}`); + svg.setAttribute("width", String(width)); + svg.setAttribute("height", String(height)); + svg.dataset.nodeIds = visible.nodes.map(node => node.nodeId).join(" "); + svg.dataset.edgeIds = visible.edges.map(edge => edge.edgeId).join(" "); + const defs = document.createElementNS(svg.namespaceURI, "defs"); + const marker = document.createElementNS(svg.namespaceURI, "marker"); + for (const [key, value] of Object.entries({id: "graph-arrow", viewBox: "0 0 10 10", refX: "9", refY: "5", markerWidth: "6", markerHeight: "6", orient: "auto-start-reverse"})) marker.setAttribute(key, value); + const arrow = document.createElementNS(svg.namespaceURI, "path"); + arrow.setAttribute("d", "M 0 0 L 10 5 L 0 10 z"); + marker.append(arrow); defs.append(marker); svg.append(defs); + for (const edge of visible.edges) { + const from = positions.get(edge.fromNodeId), to = positions.get(edge.toNodeId); + if (!from || !to) throw new Error("Visible edge endpoint is unavailable"); + const dx = to.x - from.x, dy = to.y - from.y; + const boundary = Math.min(120 / Math.abs(dx), 48 / Math.abs(dy)); + const line = document.createElementNS(svg.namespaceURI, "line"); + for (const [key, value] of Object.entries({"data-edge-id": edge.edgeId, x1: String(from.x + 120 + dx * boundary), y1: String(from.y + 48 + dy * boundary), x2: String(to.x + 120 - dx * boundary), y2: String(to.y + 48 - dy * boundary), "marker-end": "url(#graph-arrow)"})) line.setAttribute(key, value); + svg.append(line); + } + canvas.append(svg); + /** @type {Map} */ + const nodeButtons = new Map(); + for (const node of visible.nodes) { + const position = positions.get(node.nodeId); + if (!position) throw new Error("Node position is unavailable"); + const button = nodeButton(node); + button.classList.add("graph-node"); + button.style.left = `${position.x}px`; + button.style.top = `${position.y}px`; + button.dataset.plane = node.evidencePlane; + button.dataset.boundary = String(!primaryIDs.has(node.nodeId)); + button.setAttribute("aria-pressed", String(selectedId === node.nodeId)); + nodeButtons.set(node.nodeId, button); + canvas.append(button); + } + viewport.replaceChildren(canvas); + recordBody.replaceChildren(); + const nodes = document.createElement("ul"); + nodes.setAttribute("aria-label", "Admitted traceability nodes"); + for (const node of visible.nodes) { + const item = document.createElement("li"); + item.dataset.identity = node.nodeId; + const button = nodeButton(node); + button.setAttribute("aria-pressed", String(selectedId === node.nodeId)); + item.append(button); + nodes.append(item); + } + const edges = document.createElement("ul"); + edges.setAttribute("aria-label", "Admitted traceability edges"); + for (const edge of visible.edges) { + const item = document.createElement("li"); + item.dataset.identity = edge.edgeId; + item.append(edgeRecord(edge, visible)); + edges.append(item); + } + recordBody.append(nodes, edges); + inspector.replaceChildren(); + const selected = visible.nodes.find(node => node.nodeId === selectedId); + if (selected) { + const title = document.createElement("h3"); + title.className = "caller-text"; + title.textContent = selected.label; + const kind = document.createElement("p"); + kind.textContent = primaryIDs.has(selected.nodeId) ? "Primary node" : "Endpoint boundary node"; + inspector.append(title, kind, fields(selected)); + appendReferences(inspector, "node", selected.nodeId, visible); + for (const [direction, key] of [["Incoming", "toNodeId"], ["Outgoing", "fromNodeId"]]) { + const heading = document.createElement("h4"); + heading.textContent = `${direction} relations in this page`; + const list = document.createElement("ul"); + for (const edge of graph.edges.filter((/** @type {any} */ edge) => edge[key] === selected.nodeId)) { + const item = document.createElement("li"); + item.append(edgeRecord(edge, visible)); + list.append(item); + } + if (!list.children.length) { const item = document.createElement("li"); item.textContent = "None returned"; list.append(item); } + inspector.append(heading, list); + } + } else { + const empty = document.createElement("p"); empty.textContent = "No node selected."; inspector.append(empty); + } + options.reconcile(); + if (focusedNode) { + const replacement = nodeButtons.get(focusedNode); + const recordButton = [...recordBody.querySelectorAll("button")].find(button => button.dataset.graphSelect === focusedNode); + if (recordButton && (recordFocused || window.getComputedStyle(viewport).display === "none")) { records.open = true; recordButton.focus(); } + else if (replacement) replacement.focus(); + else if (fallback?.isConnected) fallback.focus(); + else recordBody.querySelector("button")?.focus(); + } + viewport.dataset.commitMilliseconds = String(performance.now() - start); + } + + /** @param {any} node */ + function nodeButton(node) { + const button = document.createElement("button"); + button.type = "button"; + button.dataset.graphSelect = node.nodeId; + button.title = `${node.label}: ${node.nodeId}`; + const label = document.createElement("span"); label.className = "graph-node-label caller-text"; label.textContent = node.label; + const identity = document.createElement("span"); identity.className = "graph-node-identity caller-text"; identity.textContent = node.nodeId; + button.append(label, identity); + button.addEventListener("click", () => select(node.nodeId)); + return button; + } + + /** @param {any} record */ + function fields(record) { + const list = document.createElement("dl"); + list.className = "graph-record-fields"; + for (const [key, value] of Object.entries(record)) { + const term = document.createElement("dt"); term.textContent = key; + const detail = document.createElement("dd"); detail.className = "caller-text"; + detail.textContent = Array.isArray(value) ? value.map(workspaceScalarText).join(", ") : workspaceScalarText(value); + list.append(term, detail); + } + return list; + } + + /** @param {any} edge @param {ReturnType} visible */ + function edgeRecord(edge, visible) { + const details = document.createElement("details"); + const summary = document.createElement("summary"); + summary.className = "caller-text"; + summary.textContent = `${edge.edgeKind}: ${edge.fromNodeId} -> ${edge.toNodeId}`; + details.append(summary); + details.addEventListener("toggle", () => { + if (!details.open || details.querySelector("dl")) return; + details.append(fields(edge)); + appendReferences(details, "edge", edge.edgeId, visible); + options.reconcile(); + }); + return details; + } + + /** @param {HTMLElement} parent @param {string} kind @param {string} id @param {ReturnType} visible */ + function appendReferences(parent, kind, id, visible) { + const visibleIDs = new Set(visible.nodes.map(node => node.nodeId)); + for (const ref of graph.references.filter((/** @type {any} */ ref) => ref.recordKind === kind && ref.recordId === id)) { + const button = document.createElement("button"); + button.type = "button"; + button.className = "graph-reference"; + const outside = ref.disposition === "outside_page"; + const hidden = !outside && !visibleIDs.has(ref.targetNodeId); + const label = document.createElement("bdi"); + label.textContent = `${ref.field}: ${ref.targetNodeId} (${outside ? "outside page" : hidden ? "hidden by filters" : "included"})`; + button.append(icon("arrow-right"), label); + if (outside) button.dataset.protectedRequest = ""; + button.addEventListener("click", () => { + if (button.disabled) return; + if (outside) options.follow(ref.targetOffset, ref.targetNodeId); + else select(ref.targetNodeId, hidden); + }); + parent.append(button); + } + } + + update(); +} diff --git a/internal/command/requirementbrowser/assets/workspace-handoff.js b/internal/command/requirementbrowser/assets/workspace-handoff.js new file mode 100644 index 0000000..4ab08ae --- /dev/null +++ b/internal/command/requirementbrowser/assets/workspace-handoff.js @@ -0,0 +1,135 @@ +// @ts-check + +import {icon} from "./workspace-icons.js"; + +/** @param {any} packet @param {string} requirementId */ +export function resolveHandoffRequirement(packet, requirementId) { + const sources = packet?.context?.projections?.requirementSources; + const matches = Array.isArray(sources) ? sources.flatMap(source => + Array.isArray(source.requirements) ? source.requirements.filter((/** @type {any} */ requirement) => requirement.requirementId === requirementId) : []) : []; + return {state: matches.length === 1 ? "found" : matches.length === 0 ? "unavailable" : "ambiguous", requirement: matches.length === 1 ? matches[0] : null}; +} + +/** @param {HTMLElement} preview @param {HTMLElement} carrier @param {HTMLElement} status */ +export function initializeHandoffPreview(preview, carrier, status) { + let generation = 0; + /** @type {Set} */ + const urls = new Set(); + + function clear() { + generation++; + preview.replaceChildren(); + carrier.replaceChildren(); + for (const url of urls) URL.revokeObjectURL(url); + urls.clear(); + } + + /** @param {string} text @param {any} packet */ + function show(text, packet) { + clear(); + const currentGeneration = generation; + const current = () => generation === currentGeneration && preview.isConnected; + carrier.textContent = text; + const controls = document.createElement("div"); + controls.className = "handoff-export-controls"; + const copy = document.createElement("button"); + copy.type = "button"; + copy.append(icon("copy"), document.createTextNode("Copy JSON")); + copy.addEventListener("click", async () => { + if (!current() || copy.disabled) return; + copy.disabled = true; + try { + if (!navigator.clipboard?.writeText) throw new Error("Clipboard unavailable"); + await navigator.clipboard.writeText(text); + if (current()) status.textContent = "Exact handoff JSON copied."; + } catch { + if (current()) { + status.textContent = "Clipboard unavailable. Exact JSON remains available below."; + const disclosure = carrier.closest("details"); + if (disclosure) disclosure.open = true; + } + } finally { + if (current()) copy.disabled = false; + } + }); + const download = document.createElement("button"); + download.type = "button"; + download.append(icon("download"), document.createTextNode("Download JSON")); + download.addEventListener("click", () => { + if (!current()) return; + const anchor = document.createElement("a"); + let url = ""; + try { + url = URL.createObjectURL(new Blob([text], {type: "application/json;charset=utf-8"})); + urls.add(url); + anchor.href = url; + anchor.download = "proofkit-question.json"; + anchor.hidden = true; + document.body.append(anchor); + anchor.click(); + } catch { + if (current()) { + status.textContent = "Download unavailable. Exact JSON remains available below."; + const disclosure = carrier.closest("details"); + if (disclosure) disclosure.open = true; + } + } finally { + anchor.remove(); + // Release after the explicit activation's default action has run. + if (url) setTimeout(() => { URL.revokeObjectURL(url); urls.delete(url); }, 0); + } + }); + controls.append(copy, download); + preview.append(controls); + for (const annotation of packet.annotations ?? []) { + const article = document.createElement("article"); + const heading = document.createElement("h4"); + heading.className = "caller-text"; + heading.textContent = annotation.anchor.requirementId; + const question = document.createElement("p"); + question.className = "caller-text"; + question.textContent = annotation.question; + const quote = document.createElement("blockquote"); + quote.className = "caller-text"; + quote.textContent = annotation.exactQuote; + const coordinates = document.createElement("p"); + coordinates.textContent = `Code points ${annotation.startCodePoint}-${annotation.endCodePoint}`; + const details = document.createElement("details"); + const label = document.createElement("summary"); + label.textContent = "Included requirement and source"; + details.append(label); + details.addEventListener("toggle", () => { + if (!details.open || details.querySelector("[data-handoff-detail]")) return; + const resolved = resolveHandoffRequirement(packet, annotation.anchor.requirementId); + const invariant = document.createElement("p"); + invariant.dataset.handoffDetail = resolved.state; + invariant.className = "caller-text"; + invariant.textContent = resolved.state === "found" ? resolved.requirement.invariant : `Requirement detail ${resolved.state} in this packet.`; + const identity = document.createElement("p"); + identity.className = "caller-text"; + identity.textContent = `${annotation.anchor.jsonPointer}\n${annotation.anchor.sourceDigest}`; + details.append(invariant, identity); + }); + article.append(heading, question, quote, coordinates, details); + preview.append(article); + } + const boundary = document.createElement("details"); + const label = document.createElement("summary"); + label.textContent = "Packet identity and authority"; + const identity = document.createElement("p"); + identity.className = "caller-text"; + identity.textContent = `${packet.handoffKind}; ${packet.instructionAuthority}; source text: ${packet.sourceTextAuthority}.`; + const refs = document.createElement("p"); + refs.className = "caller-text"; + refs.textContent = (packet.snapshotRefs ?? []).map((/** @type {any} */ ref) => `${ref.role}: ${ref.snapshotId}`).join("\n"); + const nonClaims = document.createElement("ul"); + for (const text of packet.nonClaims ?? []) { + const item = document.createElement("li"); + item.textContent = text; + nonClaims.append(item); + } + boundary.append(label, identity, refs, nonClaims); + preview.append(boundary); + } + return {clear, show}; +} diff --git a/internal/command/requirementbrowser/assets/workspace-icons.js b/internal/command/requirementbrowser/assets/workspace-icons.js index db7e100..00fba20 100644 --- a/internal/command/requirementbrowser/assets/workspace-icons.js +++ b/internal/command/requirementbrowser/assets/workspace-icons.js @@ -50,6 +50,8 @@ SOFTWARE. /** @type {Record][]>} */ const nodes = { + copy: [["rect", {width: "14", height: "14", x: "8", y: "8", rx: "2", ry: "2"}], ["path", {d: "M4 16c-1.1 0-2-.9-2-2V4c0-1.1.9-2 2-2h10c1.1 0 2 .9 2 2"}]], + download: [["path", {d: "M12 15V3"}], ["path", {d: "M21 15v4a2 2 0 0 1-2 2H5a2 2 0 0 1-2-2v-4"}], ["path", {d: "m7 10 5 5 5-5"}]], "panel-left": [["rect", {width: "18", height: "18", x: "3", y: "3", rx: "2"}], ["path", {d: "M9 3v18"}]], "panel-right": [["rect", {width: "18", height: "18", x: "3", y: "3", rx: "2"}], ["path", {d: "M15 3v18"}]], search: [["path", {d: "m21 21-4.34-4.34"}], ["circle", {cx: "11", cy: "11", r: "8"}]], diff --git a/internal/command/requirementbrowser/assets/workspace-json.js b/internal/command/requirementbrowser/assets/workspace-json.js new file mode 100644 index 0000000..d85193a --- /dev/null +++ b/internal/command/requirementbrowser/assets/workspace-json.js @@ -0,0 +1,20 @@ +// @ts-check + +/** @param {string} source @returns {any} */ +export function parseWorkspaceJSON(source) { + const rawJSON = Reflect.get(JSON, "rawJSON"); + const isRawJSON = Reflect.get(JSON, "isRawJSON"); + return JSON.parse(source, (_key, value, context = /** @type {{source?: string}} */ ({})) => { + if (typeof value !== "number") return value; + if (typeof context.source !== "string") throw new SyntaxError("Exact numeric observation is unavailable"); + if (Number.isSafeInteger(value) && String(value) === context.source) return value; + if (typeof rawJSON !== "function" || typeof isRawJSON !== "function") throw new SyntaxError("Exact numeric observation is unavailable"); + return rawJSON(context.source); + }); +} + +/** @param {any} value @returns {string} */ +export function workspaceScalarText(value) { + const isRawJSON = Reflect.get(JSON, "isRawJSON"); + return typeof isRawJSON === "function" && isRawJSON(value) ? value.rawJSON : String(value); +} diff --git a/internal/command/requirementbrowser/assets/workspace-panels.js b/internal/command/requirementbrowser/assets/workspace-panels.js index a67132c..d543e48 100644 --- a/internal/command/requirementbrowser/assets/workspace-panels.js +++ b/internal/command/requirementbrowser/assets/workspace-panels.js @@ -47,12 +47,20 @@ export function initializePanels(commitSelection) { close(panel); return; } + show(name, opener); + } + + /** @param {"navigation" | "inspector"} name @param {HTMLElement} opener */ + function show(name, opener) { + const panel = panels[name]; openers.set(panel, opener); - if (mobile.matches) { - for (const other of Object.values(panels)) close(other, false); - panel.showModal(); - } else { - panel.show(); + if (!panel.open) { + if (mobile.matches) { + for (const other of Object.values(panels)) close(other, false); + panel.showModal(); + } else { + panel.show(); + } } synchronize(); const initial = panel.querySelector(name === "inspector" ? "#annotation-question" : "#requirement-search"); @@ -94,5 +102,8 @@ export function initializePanels(commitSelection) { } mobile.addEventListener("change", changeLayout); changeLayout(); - return {closeNavigation: () => { if (mobile.matches) close(navigation); }}; + return { + closeNavigation: () => { if (mobile.matches) close(navigation); }, + showInspector: (/** @type {HTMLElement} */ opener) => show("inspector", opener), + }; } diff --git a/internal/command/requirementbrowser/assets/workspace-requests.js b/internal/command/requirementbrowser/assets/workspace-requests.js index 900b18e..191a9ed 100644 --- a/internal/command/requirementbrowser/assets/workspace-requests.js +++ b/internal/command/requirementbrowser/assets/workspace-requests.js @@ -1,5 +1,7 @@ // @ts-check +import {parseWorkspaceJSON} from "./workspace-json.js"; + export class WorkspaceRequestError extends Error { /** @param {number} status */ constructor(status) { @@ -10,6 +12,11 @@ export class WorkspaceRequestError extends Error { /** @param {string} path @param {RequestInit} init @returns {Promise} */ export async function fetchWorkspaceJSON(path, init) { + return (await fetchWorkspaceResponse(path, init)).value; +} + +/** @param {string} path @param {RequestInit} init @returns {Promise<{text: string, value: any}>} */ +export async function fetchWorkspaceResponse(path, init) { /** @type {string} */ let body; try { @@ -20,7 +27,7 @@ export async function fetchWorkspaceJSON(path, init) { if (init.signal?.aborted || error instanceof WorkspaceRequestError) throw error; throw new WorkspaceRequestError(0); } - return JSON.parse(body); + return {text: body, value: parseWorkspaceJSON(body)}; } /** @param {unknown} error @param {boolean} optional */ diff --git a/internal/command/requirementbrowser/assets/workspace.css b/internal/command/requirementbrowser/assets/workspace.css index 024658c..45aa838 100644 --- a/internal/command/requirementbrowser/assets/workspace.css +++ b/internal/command/requirementbrowser/assets/workspace.css @@ -94,6 +94,8 @@ article h3 { font-family: ui-monospace, monospace; color: var(--muted-text); fon [data-anchor-id] { font-size: 1.0625rem; line-height: 1.65; margin: .75rem 0; max-inline-size: 75ch; } .requirement-boundary { margin: .75rem 0; color: var(--muted-text); font-size: .8125rem; } .page-summary { font-size: .8125rem; color: var(--muted-text); } +details.projection-boundary { margin-block: 1rem; color: var(--muted-text); font-size: .8125rem; } +details.projection-boundary > summary { min-block-size: 2.75rem; padding-block: .625rem; } .workspace-panel { position: sticky; top: 4.25rem; @@ -128,15 +130,48 @@ article h3 { font-family: ui-monospace, monospace; color: var(--muted-text); fon #submit-question { margin-top: .75rem; } #handoff-status { font-size: .8125rem; } #handoff-packet { font-size: .75rem; } +#handoff-output summary { min-block-size: 2.75rem; padding-block: .625rem; } pre { margin: 0; max-width: 100%; overflow-wrap: anywhere; white-space: pre-wrap; } .graph-viewport, .table-viewport { border: 1px solid var(--border); min-width: 0; max-width: 100%; overflow: auto; } .graph-viewport { max-height: 42rem; } .table-viewport { margin-block: 1rem; } -.graph-viewport svg { display: block; min-width: 50rem; width: 100%; max-width: none; } +.graph-canvas { position: relative; } +.graph-canvas > svg { position: absolute; inset: 0; pointer-events: none; } +.graph-plane-heading { position: absolute; top: 0; width: 240px; font-size: .8125rem; font-weight: 650; } +.graph-node { position: absolute; width: 240px; height: 96px; display: flex; flex-direction: column; align-items: start; text-align: start; overflow: hidden; } +.graph-node[data-boundary="true"] { border-style: dashed; } +.graph-node[data-plane="proof_coverage"] { border-inline-start: 4px solid #77589b; } +.graph-node[data-plane="code_traceability"] { border-inline-start: 4px solid #387080; } +.graph-node[data-plane="native_execution_coverage"] { border-inline-start: 4px solid #8a681a; } +.graph-node-label, .graph-node-identity { display: -webkit-box; -webkit-box-orient: vertical; -webkit-line-clamp: 2; overflow: hidden; max-width: 100%; } +.graph-node-identity { color: var(--muted-text); font-size: .75rem; } +.graph-filters { display: flex; flex-wrap: wrap; gap: .5rem 1rem; border: 0; padding: 0; margin: 1rem 0; } +.graph-filters legend { font-size: .875rem; font-weight: 650; } +.graph-filters label { display: inline-flex; align-items: center; gap: .5rem; min-height: 2.75rem; margin: 0; } +.graph-filters input { width: 1.125rem; height: 1.125rem; min-height: 0; flex: 0 0 1.125rem; } +.graph-records { margin-block: 1rem; } +.graph-records ul, .graph-inspector ul { list-style: none; padding: 0; } +.graph-records li, .graph-inspector li { margin-block: .5rem; } +.graph-records [data-graph-select] { display: flex; flex-direction: column; align-items: start; width: 100%; text-align: start; } +.graph-record-fields, .coverage-state { display: grid; grid-template-columns: minmax(0, 1fr) minmax(0, 2fr); gap: .25rem .75rem; font-size: .8125rem; } +dt { font-weight: 600; overflow-wrap: anywhere; } +dd { margin: 0; min-width: 0; overflow-wrap: anywhere; white-space: pre-wrap; } +.graph-reference { max-width: 100%; margin-block: .25rem; text-align: start; } +.graph-inspector { border-block: 1px solid var(--border); margin-block: 1rem; } +.caller-text { unicode-bidi: plaintext; overflow-wrap: anywhere; } +.coverage-matrix { list-style: none; padding: 0; margin: 0; } +.coverage-record { display: grid; grid-template-columns: minmax(0, 2fr) minmax(0, 1fr); gap: .5rem 1rem; } +.coverage-actions, .coverage-details { grid-column: 1 / -1; } +.coverage-details details { margin-block: .5rem; } +.coverage-details pre { margin-top: .5rem; font-size: .8125rem; } +.diff-class-counts { display: flex; flex-wrap: wrap; gap: .5rem 1rem; list-style: none; padding: 0; font-size: .8125rem; } +.handoff-export-controls { display: flex; flex-wrap: wrap; gap: .5rem; } +#handoff-preview article h4 { margin-block: .5rem; font-size: .8125rem; } +#handoff-preview p, #handoff-preview li, #handoff-preview blockquote { font-size: .8125rem; } +#handoff-preview blockquote { margin-inline: 0; border-inline-start: 2px solid var(--border); padding-inline-start: .75rem; } [data-select-anchor][aria-pressed="true"] { outline: 3px solid var(--focus); outline-offset: 2px; } -.graph-viewport svg rect { fill: var(--surface); stroke: var(--border); } .graph-viewport svg line { stroke: var(--text); stroke-width: 1.5; } -.graph-viewport svg text { fill: var(--text); font-size: 13px; } +.graph-viewport svg path { fill: var(--text); } table { border-collapse: collapse; min-width: 100%; width: max-content; } th, td { border: 1px solid var(--border); max-width: 24rem; padding: .5rem; text-align: left; } @@ -163,20 +198,23 @@ th, td { border: 1px solid var(--border); max-width: 24rem; padding: .5rem; text max-width: calc(100% - 1rem); height: 100dvh; max-height: 100dvh; - padding: 1rem; + padding: max(1rem, env(safe-area-inset-top)) max(1rem, env(safe-area-inset-right)) max(1rem, env(safe-area-inset-bottom)) max(1rem, env(safe-area-inset-left)); } #workspace-inspector { inset: 0 0 0 auto; } .workspace-panel::backdrop { background: #00000080; } .view-controls button { flex: 1 1 auto; min-width: 0; padding: .5rem .375rem; } .view-controls .workspace-icon { display: none; } } +@media (max-width: 48rem) { + .graph-viewport { display: none; } + .coverage-record { grid-template-columns: minmax(0, 1fr); } +} @media (prefers-reduced-motion: reduce) { *, *::before, *::after { scroll-behavior: auto; } } @media (forced-colors: active) { .product-bar, .workspace-panel, article, button, input, select, textarea, .graph-viewport, .table-viewport, th, td { border-color: CanvasText; } button:focus-visible, input:focus-visible, select:focus-visible, textarea:focus-visible, summary:focus-visible, [tabindex="0"]:focus-visible, [data-select-anchor][aria-pressed="true"] { outline-color: Highlight; } - .graph-viewport svg rect { fill: Canvas; stroke: CanvasText; } .graph-viewport svg line { stroke: CanvasText; } - .graph-viewport svg text { fill: CanvasText; } + .graph-viewport svg path { fill: CanvasText; } } diff --git a/internal/command/requirementbrowser/assets/workspace.js b/internal/command/requirementbrowser/assets/workspace.js index 745e3f0..abb9af6 100644 --- a/internal/command/requirementbrowser/assets/workspace.js +++ b/internal/command/requirementbrowser/assets/workspace.js @@ -4,11 +4,16 @@ import {emptySelectionState, transitionSelection} from "./selection-authority.js import {decorateIcons, icon} from "./workspace-icons.js"; import {initializePanels} from "./workspace-panels.js"; import {initializeNavigation} from "./workspace-navigation.js"; -import {fetchWorkspaceJSON, workspaceFailure} from "./workspace-requests.js"; +import {fetchWorkspaceJSON, fetchWorkspaceResponse, workspaceFailure} from "./workspace-requests.js"; +import {renderCoveragePage} from "./workspace-coverage.js"; +import {renderDiffPage} from "./workspace-diff.js"; +import {GRAPH_PAGE, renderGraphPage} from "./workspace-graph.js"; +import {initializeHandoffPreview} from "./workspace-handoff.js"; export {}; /** @typedef {import("./selection-authority.js").SelectionTarget} SelectionTarget */ +/** @typedef {"specifications" | "coverage" | "diff" | "graph"} WorkspaceView */ const capabilityElement = document.querySelector('meta[name="proofkit-browser-capability"]'); if (!(capabilityElement instanceof HTMLMetaElement)) throw new Error("Missing browser capability"); @@ -19,6 +24,9 @@ const headers = {"Content-Type": "application/json", "X-Proofkit-Browser-Capabil const contentElement = document.querySelector("#workspace-content"); if (!(contentElement instanceof HTMLElement)) throw new Error("Missing workspace content region"); const content = /** @type {HTMLElement} */ (contentElement); +const recovery = document.createElement("div"); +recovery.id = "workspace-recovery"; +content.before(recovery); const authorityElement = document.querySelector("#workspace-authority"); if (!(authorityElement instanceof HTMLElement)) throw new Error("Missing workspace authority boundary"); @@ -36,6 +44,8 @@ let activeViewController = null; let selectionState = emptySelectionState(); let requestsLocked = false; let handoffPending = false; +/** @type {"specifications" | "coverage"} */ +let lookupView = "specifications"; /** @type {import("./workspace-navigation.js").LookupFilters} */ let activeFilters = Object.freeze({}); @@ -50,7 +60,7 @@ function setWorkspaceState(state) { document.body.dataset.state = state; } -/** @param {"specifications" | "diff" | "graph"} activeView */ +/** @param {WorkspaceView} activeView */ function setActiveView(activeView) { for (const control of document.querySelectorAll("[data-view]")) { if (!(control instanceof HTMLButtonElement)) continue; @@ -69,12 +79,12 @@ function handoffUnavailable() { function reconcileRequestControls() { for (const control of document.querySelectorAll("[data-protected-request]")) { if (control instanceof HTMLButtonElement || control instanceof HTMLInputElement || control instanceof HTMLSelectElement) { - control.disabled = control === submit ? handoffUnavailable() : requestsLocked; + control.disabled = control === submit || control.hasAttribute("data-evidence-question") ? handoffUnavailable() : requestsLocked; } } } -/** @param {"specifications" | "diff" | "graph"} state */ +/** @param {WorkspaceView} state */ function completeContentView(state) { reconcileRequestControls(); content.setAttribute("aria-busy", "false"); @@ -123,54 +133,69 @@ async function post(path, body, signal) { return fetchWorkspaceJSON(path, {method: "POST", headers, body: JSON.stringify(body), signal}); } -/** @param {string} title @param {string} requestPrefix @param {"specifications" | "diff" | "graph"} view */ -function beginView(title, requestPrefix, view) { +/** @param {string} title @param {string} requestPrefix @param {WorkspaceView} view @param {boolean} [focusContent] */ +function beginView(title, requestPrefix, view, focusContent = false) { + const restoreFocus = focusContent || document.activeElement !== null && content.contains(document.activeElement); activeViewController?.abort(); activeViewController = new AbortController(); const requestId = nextRequestId(requestPrefix); activeRequestId = requestId; clearSelection(); - packetView.replaceChildren(); + handoffPreview.clear(); setActiveView(view); setWorkspaceState(`${view}-loading`); content.replaceChildren(); content.setAttribute("aria-busy", "true"); const heading = document.createElement("h2"); heading.textContent = title; + heading.tabIndex = -1; const status = document.createElement("p"); status.setAttribute("role", "status"); status.setAttribute("aria-live", "polite"); status.dataset.state = "loading"; status.textContent = "Loading admitted data..."; content.append(heading, status); - return {requestId, signal: activeViewController.signal, status}; + if (restoreFocus) heading.focus(); + const focusAfterCommit = () => { + if (restoreFocus && heading.isConnected && activeRequestId === requestId && (document.activeElement === document.body || document.activeElement === heading)) heading.focus(); + }; + return {requestId, signal: activeViewController.signal, status, focusAfterCommit}; +} + +/** @param {ReturnType} failure */ +function applyFailureLock(failure) { + if (!failure.lock) return; + requestsLocked = true; + reconcileRequestControls(); + navigation.cancel(); + if (failure.action === "reload" && !recovery.hasChildNodes()) { + const action = document.createElement("button"); + action.type = "button"; + action.title = failure.message; + action.append(icon("refresh-cw"), document.createTextNode("Reload workspace")); + action.addEventListener("click", () => window.location.reload()); + recovery.append(action); + } } /** @param {unknown} error @param {HTMLElement} container @param {() => void} retry @param {boolean} [optional] */ function showFailure(error, container, retry, optional = false) { const failure = workspaceFailure(error, optional); - if (failure.lock) { - requestsLocked = true; - reconcileRequestControls(); - navigation.cancel(); - } + applyFailureLock(failure); const message = document.createElement("p"); message.setAttribute("role", "alert"); message.dataset.state = failure.kind; message.textContent = failure.message; container.append(message); - if (failure.action === "none") return; + if (failure.action === "none" || failure.lock) return; const action = document.createElement("button"); action.type = "button"; - if (failure.action === "retry") { - action.dataset.protectedRequest = ""; - action.disabled = requestsLocked; - } - action.append(icon("refresh-cw"), document.createTextNode(failure.action === "retry" ? "Retry" : "Reload workspace")); + action.dataset.protectedRequest = ""; + action.disabled = requestsLocked; + action.append(icon("refresh-cw"), document.createTextNode("Retry")); action.addEventListener("click", () => { if (!action.isConnected) return; - if (failure.action === "reload") window.location.reload(); - else if (!requestsLocked) retry(); + if (!requestsLocked) retry(); }); container.append(action); } @@ -196,6 +221,7 @@ function admitCurrentViewResponse(response, requestId, signal) { /** @param {number} [offset] @param {import("./workspace-navigation.js").LookupFilters} [filters] @param {number[]} [history] */ async function renderSpecifications(offset = 0, filters = activeFilters, history = []) { if (requestsLocked) return; + lookupView = "specifications"; activeFilters = filters; const query = Object.freeze({...filters, maxRecords: 64, offset}); const {requestId, signal, status} = beginView("Specifications", "browser.specifications", "specifications"); @@ -257,7 +283,7 @@ async function renderSpecifications(offset = 0, filters = activeFilters, history return; } content.append(list); - appendRequirementPaging(offset, response.projection.selectedRequirementCount ?? 0, response.projection.matchingRequirementCount ?? 0, filters, history); + appendRequirementPaging("specifications", offset, response.projection.selectedRequirementCount ?? 0, response.projection.matchingRequirementCount ?? 0, filters, history); completeContentView("specifications"); } catch (error) { if (signal.aborted || requestId !== activeRequestId) return; @@ -265,6 +291,41 @@ async function renderSpecifications(offset = 0, filters = activeFilters, history } } +/** @param {number} [offset] @param {import("./workspace-navigation.js").LookupFilters} [filters] @param {number[]} [history] */ +async function renderCoverage(offset = 0, filters = activeFilters, history = []) { + if (requestsLocked) return; + lookupView = "coverage"; + activeFilters = filters; + const query = Object.freeze({...filters, maxRecords: 64, offset}); + const {requestId, signal, status} = beginView("Coverage", "browser.coverage", "coverage"); + if (!manifest.coverageAvailable) { + content.setAttribute("aria-busy", "false"); + setWorkspaceState("coverage-unavailable"); + status.dataset.state = "unavailable"; + status.textContent = "No admitted coverage report was supplied."; + return; + } + try { + const response = await post("/api/v1/coverage", {requestId, snapshotId: manifest.snapshotId, query}, signal); + if (!admitCurrentViewResponse(response, requestId, signal)) return; + status.remove(); + const projection = response.projection; + appendProjectionBoundary(projection.coverageAuthority, projection.nonClaims, [`Coverage input: ${projection.sourceViewInputId}.`], true); + renderCoveragePage(content, projection, (requirement, opener) => { + if (handoffUnavailable()) return; + selectionState = transitionSelection(selectionState, {kind: "button", targets: [{anchorId: requirement.anchor.anchorId, exactQuote: requirement.invariant, startCodePoint: 0, endCodePoint: [...requirement.invariant].length}]}); + announceSelection(); + if (questionInput.value === "") questionInput.value = `What evidence supports ${requirement.requirementId}?`; + panels.showInspector(opener); + }); + appendRequirementPaging("coverage", offset, projection.selectedRequirementCount, projection.matchingRequirementCount, filters, history); + completeContentView("coverage"); + } catch (error) { + if (signal.aborted || requestId !== activeRequestId) return; + failView(status, error, () => void renderCoverage(offset, filters, history), true); + } +} + /** @param {number} [offset] */ async function renderDiff(offset = 0) { if (requestsLocked) return; @@ -284,20 +345,7 @@ async function renderDiff(offset = 0) { `Base snapshot: ${response.projection.baseSnapshotId} (expected-digest coverage: ${response.projection.baseExpectedDigestCoverage}).`, `Current snapshot: ${response.projection.currentSnapshotId} (expected-digest coverage: ${response.projection.currentExpectedDigestCoverage}).`, ]); - for (const change of response.projection.changes ?? []) { - const article = document.createElement("article"); - article.dataset.changeId = change.changeId; - const title = document.createElement("h3"); - title.textContent = `${change.changeClass}: ${change.entityId}`; - const pointer = document.createElement("p"); - pointer.textContent = change.jsonPointer; - const sourceDigests = document.createElement("p"); - sourceDigests.textContent = `Source digests: ${change.baseSourceDigest ?? "not-recorded"} -> ${change.currentSourceDigest ?? "not-recorded"}`; - const values = document.createElement("pre"); - values.textContent = `${JSON.stringify(change.before, null, 2)}\n->\n${JSON.stringify(change.after, null, 2)}`; - article.append(title, pointer, sourceDigests, values); - content.append(article); - } + renderDiffPage(content, response.projection.changes ?? []); appendPagingControls("diff", offset, response.projection.selectedChangeCount ?? 0, response.projection.availableChangeCount ?? 0); completeContentView("diff"); } catch (error) { @@ -306,10 +354,10 @@ async function renderDiff(offset = 0) { } } -/** @param {number} [offset] */ -async function renderGraph(offset = 0, edgeOffset = 0) { +/** @param {number} [offset] @param {number} [edgeOffset] @param {string | null} [initialId] */ +async function renderGraph(offset = 0, edgeOffset = 0, initialId = null) { if (requestsLocked) return; - const {requestId, signal, status} = beginView("Traceability graph", "browser.graph", "graph"); + const {requestId, signal, status, focusAfterCommit} = beginView("Traceability graph", "browser.graph", "graph", initialId !== null); if (!manifest.graphAvailable) { content.setAttribute("aria-busy", "false"); setWorkspaceState("graph-unavailable"); @@ -318,88 +366,36 @@ async function renderGraph(offset = 0, edgeOffset = 0) { return; } try { - const response = await post("/api/v1/graph", {requestId, snapshotId: manifest.snapshotId, query: {edgeOffset, maxEdges: 2048, maxRecords: 256, offset}}, signal); + const response = await post("/api/v1/graph", {requestId, snapshotId: manifest.snapshotId, query: {...GRAPH_PAGE, edgeOffset, offset}}, signal); if (!admitCurrentViewResponse(response, requestId, signal)) return; status.remove(); const graph = response.projection; appendProjectionBoundary(graph.authority, graph.nonClaims ?? [], [`Source snapshot: ${graph.sourceSnapshotId}.`]); - const nodes = /** @type {any[]} */ (graph.nodes ?? []); - const edges = /** @type {any[]} */ (graph.edges ?? []); - const positions = new Map(nodes.map((node, index) => [node.nodeId, {x: 28 + (index % 2) * 390, y: 28 + Math.floor(index / 2) * 76}])); - const svg = document.createElementNS("http://www.w3.org/2000/svg", "svg"); - svg.setAttribute("role", "img"); - svg.setAttribute("aria-label", "Non-authoritative layout of admitted traceability nodes and edges"); - svg.setAttribute("viewBox", `0 0 800 ${Math.max(180, Math.ceil(nodes.length / 2) * 76 + 40)}`); - svg.dataset.nodeIds = nodes.map((node) => node.nodeId).join(" "); - svg.dataset.edgeIds = edges.map((edge) => edge.edgeId).join(" "); - for (const edge of edges) { - const from = positions.get(edge.fromNodeId); - const to = positions.get(edge.toNodeId); - if (!from || !to) throw new Error("Graph edge endpoint is not present in admitted nodes"); - const line = document.createElementNS(svg.namespaceURI, "line"); - line.setAttribute("data-edge-id", edge.edgeId); - line.setAttribute("x1", String(from.x + 180)); - line.setAttribute("y1", String(from.y + 24)); - line.setAttribute("x2", String(to.x + 180)); - line.setAttribute("y2", String(to.y + 24)); - svg.append(line); - } - for (const node of nodes) { - const position = positions.get(node.nodeId); - if (!position) throw new Error("Graph node position is unavailable"); - const group = document.createElementNS(svg.namespaceURI, "g"); - group.setAttribute("data-node-id", node.nodeId); - const box = document.createElementNS(svg.namespaceURI, "rect"); - box.setAttribute("x", String(position.x)); - box.setAttribute("y", String(position.y)); - box.setAttribute("width", "350"); - box.setAttribute("height", "48"); - box.setAttribute("rx", "4"); - const label = document.createElementNS(svg.namespaceURI, "text"); - label.setAttribute("x", String(position.x + 10)); - label.setAttribute("y", String(position.y + 29)); - const fullLabel = `${node.evidencePlane}: ${node.label}`; - label.textContent = [...fullLabel].length > 48 ? `${[...fullLabel].slice(0, 47).join("")}...` : fullLabel; - const accessibleLabel = document.createElementNS(svg.namespaceURI, "title"); - accessibleLabel.textContent = fullLabel; - group.append(accessibleLabel, box, label); - svg.append(group); - } - const viewport = document.createElement("div"); - viewport.className = "graph-viewport"; - viewport.setAttribute("role", "region"); - viewport.setAttribute("aria-label", "Traceability graph viewport"); - viewport.tabIndex = 0; - viewport.append(svg); - content.append(viewport, graphTable( - "Admitted traceability nodes", - ["Node", "Kind", "Evidence plane", "Source", "Authority", "Currentness", "Verification", "State", "Producer"], - nodes.map((node) => [node.nodeId, node.kind, node.evidencePlane, node.sourceId, node.authorityClass, node.currentnessState, node.rangeVerification, node.state, node.producerId]), - "node", - )); - content.append(graphTable( - "Admitted traceability edges", - ["Edge", "Kind", "From", "To", "Authority", "Currentness", "Evidence"], - edges.map((edge) => [edge.edgeId, edge.edgeKind, edge.fromNodeId, edge.toNodeId, edge.authorityClass, edge.currentnessState, displayList(edge.evidenceRefs)]), - "edge", - )); + if (initialId !== null && !graph.nodes.some((/** @type {any} */ node) => node.nodeId === initialId)) throw new Error("Referenced node is unavailable in its canonical page"); + renderGraphPage(content, graph, { + follow: (targetOffset, targetId) => void renderGraph(targetOffset, 0, targetId), + reconcile: reconcileRequestControls, + initialId, + }); appendPagingControls("graph", offset, graph.primaryNodeCount ?? 0, graph.availableNodeCount ?? 0); appendGraphEdgeControls(offset, edgeOffset, graph.selectedEdgeCount ?? 0, graph.availableIncidentEdgeCount ?? 0); completeContentView("graph"); + focusAfterCommit(); } catch (error) { if (signal.aborted || requestId !== activeRequestId) return; - failView(status, error, () => void renderGraph(offset, edgeOffset), true); + failView(status, error, () => void renderGraph(offset, edgeOffset, initialId), true); } } -/** @param {number} offset @param {number} selected @param {number} matching @param {import("./workspace-navigation.js").LookupFilters} filters @param {number[]} history */ -function appendRequirementPaging(offset, selected, matching, filters, history) { +/** @param {"specifications" | "coverage"} view @param {number} offset @param {number} selected @param {number} matching @param {import("./workspace-navigation.js").LookupFilters} filters @param {number[]} history */ +function appendRequirementPaging(view, offset, selected, matching, filters, history) { + const render = view === "coverage" ? renderCoverage : renderSpecifications; const summary = document.createElement("p"); summary.className = "page-summary"; - summary.textContent = `Showing ${selected === 0 ? 0 : offset + 1}-${offset + selected} of ${matching} specifications records.`; + summary.textContent = `Showing ${selected === 0 ? 0 : offset + 1}-${offset + selected} of ${matching} ${view} records.`; content.append(summary); const controls = document.createElement("nav"); - controls.setAttribute("aria-label", "specifications pages"); + controls.setAttribute("aria-label", `${view} pages`); /** @param {string} label @param {string} symbol @param {() => void} action */ function add(label, symbol, action) { const button = document.createElement("button"); @@ -409,8 +405,8 @@ function appendRequirementPaging(offset, selected, matching, filters, history) { button.addEventListener("click", action); controls.append(button); } - if (history.length > 0) add("Previous specifications page", "arrow-left", () => void renderSpecifications(history.at(-1) ?? 0, filters, history.slice(0, -1))); - if (offset + selected < matching) add("Next specifications page", "arrow-right", () => void renderSpecifications(offset + selected, filters, [...history, offset])); + if (history.length > 0) add(`Previous ${view} page`, "arrow-left", () => void render(history.at(-1) ?? 0, filters, history.slice(0, -1))); + if (offset + selected < matching) add(`Next ${view} page`, "arrow-right", () => void render(offset + selected, filters, [...history, offset])); content.append(controls); } @@ -423,7 +419,7 @@ function appendPagingControls(view, offset, selectedCount, availableCount) { if (offset === 0 && selectedCount >= availableCount) return; const controls = document.createElement("nav"); controls.setAttribute("aria-label", `${view} pages`); - const pageSize = view === "diff" ? 512 : 256; + const pageSize = view === "diff" ? 512 : GRAPH_PAGE.maxRecords; if (offset > 0) { const previous = document.createElement("button"); previous.type = "button"; @@ -457,7 +453,7 @@ function appendGraphEdgeControls(nodeOffset, edgeOffset, selectedCount, availabl previous.type = "button"; previous.dataset.protectedRequest = ""; previous.textContent = "Previous graph relation page"; - previous.addEventListener("click", () => void renderGraph(nodeOffset, Math.max(0, edgeOffset - 2048))); + previous.addEventListener("click", () => void renderGraph(nodeOffset, Math.max(0, edgeOffset - GRAPH_PAGE.maxEdges))); controls.append(previous); } if (edgeOffset + selectedCount < availableCount) { @@ -471,46 +467,6 @@ function appendGraphEdgeControls(nodeOffset, edgeOffset, selectedCount, availabl content.append(controls); } -/** @param {string} captionText @param {string[]} headings @param {string[][]} rows @param {string} identityKind */ -function graphTable(captionText, headings, rows, identityKind) { - const viewport = document.createElement("div"); - viewport.className = "table-viewport"; - viewport.setAttribute("role", "region"); - viewport.setAttribute("aria-label", `${captionText} table viewport`); - viewport.tabIndex = 0; - const table = document.createElement("table"); - table.dataset.identityKind = identityKind; - const caption = document.createElement("caption"); - caption.textContent = captionText; - const head = document.createElement("thead"); - const headRow = document.createElement("tr"); - for (const label of headings) { - const cell = document.createElement("th"); - cell.textContent = label; - headRow.append(cell); - } - head.append(headRow); - const body = document.createElement("tbody"); - for (const values of rows) { - const row = document.createElement("tr"); - row.dataset.identity = values[0] ?? ""; - for (const value of values) { - const cell = document.createElement("td"); - cell.textContent = value ?? ""; - row.append(cell); - } - body.append(row); - } - table.append(caption, head, body); - viewport.append(table); - return viewport; -} - -/** @param {unknown} value */ -function displayList(value) { - return Array.isArray(value) ? value.join(", ") : value; -} - /** @param {HTMLUListElement} list @param {unknown[]} values */ function appendTextItems(list, values) { for (const value of values) { @@ -520,13 +476,13 @@ function appendTextItems(list, values) { } } -/** @param {unknown} authority @param {unknown[]} nonClaims @param {string[]} details */ -function appendProjectionBoundary(authority, nonClaims, details) { - const section = document.createElement("section"); +/** @param {unknown} authority @param {unknown[]} nonClaims @param {string[]} details @param {boolean} [collapsed] */ +function appendProjectionBoundary(authority, nonClaims, details, collapsed = false) { + const section = document.createElement(collapsed ? "details" : "section"); section.className = "projection-boundary"; section.setAttribute("aria-label", "Projection boundary"); - const heading = document.createElement("h3"); - heading.textContent = "Projection boundary"; + const heading = document.createElement(collapsed ? "summary" : "h3"); + heading.textContent = collapsed ? `Derived coverage: ${String(authority)}` : "Projection boundary"; const authorityText = document.createElement("p"); authorityText.textContent = `Authority: ${String(authority)}.`; section.append(heading, authorityText); @@ -544,6 +500,7 @@ function appendProjectionBoundary(authority, nonClaims, details) { document.querySelectorAll("[data-view]").forEach((button) => button.addEventListener("click", () => { if (!(button instanceof HTMLButtonElement)) return; if (button.dataset.view === "specifications") void renderSpecifications(); + if (button.dataset.view === "coverage") void renderCoverage(); if (button.dataset.view === "diff") void renderDiff(); if (button.dataset.view === "graph") void renderGraph(); })); @@ -551,13 +508,15 @@ document.querySelectorAll("[data-view]").forEach((button) => button.addEventList const questionInputElement = document.querySelector("#annotation-question"); const statusElement = document.querySelector("#handoff-status"); const packetElement = document.querySelector("#handoff-packet"); +const previewElement = document.querySelector("#handoff-preview"); 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"); +if (!(questionInputElement instanceof HTMLTextAreaElement) || !(statusElement instanceof HTMLElement) || !(packetElement instanceof HTMLElement) || !(previewElement 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 handoffPreview = initializeHandoffPreview(previewElement, packetView, status); const submit = /** @type {HTMLButtonElement} */ (submitElement); const selectedContext = /** @type {HTMLUListElement} */ (selectedContextElement); const clearSelectionButton = /** @type {HTMLButtonElement} */ (clearSelectionElement); @@ -646,16 +605,20 @@ submit.addEventListener("click", async () => { status.setAttribute("aria-live", "polite"); status.textContent = "Creating handoff packet..."; try { - const packet = await post("/api/v1/handoff", {annotations: selectionState.targets.map((target) => ({...target, question}))}); - packetView.textContent = JSON.stringify(packet, null, 2); + const response = await fetchWorkspaceResponse("/api/v1/handoff", {method: "POST", headers, body: JSON.stringify({annotations: selectionState.targets.map((target) => ({...target, question}))})}); + if (submissionViewRequestId !== activeRequestId) return; + handoffPreview.show(response.text, response.value); status.textContent = "Handoff packet created."; - if (submissionViewRequestId === activeRequestId) setWorkspaceState("handoff-result"); - } catch { - packetView.replaceChildren(); + setWorkspaceState("handoff-result"); + } catch (error) { + const failure = workspaceFailure(error); + applyFailureLock(failure); + if (submissionViewRequestId !== activeRequestId) return; + handoffPreview.clear(); status.setAttribute("role", "alert"); status.setAttribute("aria-live", "assertive"); - status.textContent = "The handoff packet could not be created."; - if (submissionViewRequestId === activeRequestId) setWorkspaceState("handoff-failed"); + status.textContent = failure.lock ? failure.message : "The handoff packet could not be created."; + setWorkspaceState("handoff-failed"); } finally { handoffPending = false; reconcileRequestControls(); @@ -667,7 +630,7 @@ const panels = initializePanels(commitSelection); const navigation = initializeNavigation({ post, nextRequestId, - select(filters) { void renderSpecifications(0, filters); panels.closeNavigation(); }, + select(filters) { void (lookupView === "coverage" ? renderCoverage(0, filters) : renderSpecifications(0, filters)); panels.closeNavigation(); }, fail: showFailure, locked: () => requestsLocked, }); diff --git a/internal/command/requirementbrowser/http_handler.go b/internal/command/requirementbrowser/http_handler.go index 03bc096..cb3aa9c 100644 --- a/internal/command/requirementbrowser/http_handler.go +++ b/internal/command/requirementbrowser/http_handler.go @@ -14,6 +14,7 @@ import ( "strings" "github.com/research-engineering/agentic-proofkit/internal/command/requirementcontext" + "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/admit" "github.com/research-engineering/agentic-proofkit/internal/kernel/digest" @@ -65,8 +66,18 @@ func browserHandler(view string, rendered renderedView, expectedAuthority, capab serveWorkspaceAsset(response, method, workspacePanelsJavaScript, "text/javascript; charset=utf-8") case "/assets/workspace-requests.js": serveWorkspaceAsset(response, method, workspaceRequestsJavaScript, "text/javascript; charset=utf-8") + case "/assets/workspace-json.js": + serveWorkspaceAsset(response, method, workspaceJSONJavaScript, "text/javascript; charset=utf-8") case "/assets/workspace-navigation.js": serveWorkspaceAsset(response, method, workspaceNavigationJavaScript, "text/javascript; charset=utf-8") + case "/assets/workspace-coverage.js": + serveWorkspaceAsset(response, method, workspaceCoverageJavaScript, "text/javascript; charset=utf-8") + case "/assets/workspace-diff.js": + serveWorkspaceAsset(response, method, workspaceDiffJavaScript, "text/javascript; charset=utf-8") + case "/assets/workspace-graph.js": + serveWorkspaceAsset(response, method, workspaceGraphJavaScript, "text/javascript; charset=utf-8") + case "/assets/workspace-handoff.js": + serveWorkspaceAsset(response, method, workspaceHandoffJavaScript, "text/javascript; charset=utf-8") case "/assets/workspace.css": serveWorkspaceAsset(response, method, workspaceCSS, "text/css; charset=utf-8") case "/api/v1/manifest": @@ -89,7 +100,7 @@ func browserHandler(view string, rendered renderedView, expectedAuthority, capab } defer releaseWorkspaceRequest(workspaceRequests) serveWorkspaceQuery(response, request, expectedOrigin, capability, rendered.workspace) - case "/api/v1/requirements", "/api/v1/navigation": + case "/api/v1/requirements", "/api/v1/navigation", "/api/v1/coverage": if method != http.MethodPost { methodNotAllowed(response, method, "POST") return @@ -171,7 +182,15 @@ func serveWorkspaceRequirements(response http.ResponseWriter, request *http.Requ writeAPIError(response, request.Method, queryErr) return } - page = workspaceLookupPage(session.Lookup, query) + if request.URL.Path == "/api/v1/coverage" { + if session.Snapshot.Coverage == nil { + response.WriteHeader(http.StatusNotFound) + return + } + page = workspaceCoveragePage(session, query) + } else { + page = workspaceLookupPage(session.Lookup, query) + } } body, err := page.encode(requestID, session.SnapshotID, maxWorkspaceLookupResponseBytes) if err != nil { @@ -356,11 +375,26 @@ func graphWindow(full map[string]any, query projectionQuery) (map[string]any, st selectedIDs[edge["toNodeId"].(string)] = struct{}{} } selectedNodes := make([]any, 0, len(selectedIDs)) - for _, raw := range nodes { - if _, ok := selectedIDs[raw.(map[string]any)["nodeId"].(string)]; ok { + targetOffsets := make(map[string]int, len(nodes)) + for offset, raw := range nodes { + id := raw.(map[string]any)["nodeId"].(string) + targetOffsets[id] = offset + if _, ok := selectedIDs[id]; ok { selectedNodes = append(selectedNodes, raw) } } + references := []any{} + for _, ref := range requirementgraph.NodeReferences(selectedNodes, selectedEdges) { + disposition := "outside_page" + if _, included := selectedIDs[ref.TargetNodeID]; included { + disposition = "included" + } + references = append(references, map[string]any{ + "disposition": disposition, "field": ref.Field, "recordId": ref.RecordID, + "recordKind": ref.RecordKind, "targetNodeId": ref.TargetNodeID, + "targetOffset": targetOffsets[ref.TargetNodeID], + }) + } availableEdges := len(full["edges"].([]any)) omittedNodes := len(nodes) - len(selectedNodes) omittedPrimaryNodes := len(nodes) - len(primaryNodes) @@ -384,7 +418,9 @@ func graphWindow(full map[string]any, query projectionQuery) (map[string]any, st "omittedNodeCount": omittedNodes, "omittedPrimaryNodeCount": omittedPrimaryNodes, "primaryNodeCount": len(primaryNodes), + "primaryNodeIds": workspaceSortedSet(primaryIDs), "projectionKind": "proofkit.requirement-traceability-graph-fragment", + "references": references, "selectedEdgeCount": len(selectedEdges), "selectedNodeCount": len(selectedNodes), "sourceGraphId": full["graphId"], @@ -490,13 +526,18 @@ func serveHandoff(response http.ResponseWriter, request *http.Request, expectedO writeBody(response, request.Method, []byte("invalid handoff\n")) return } + body, err := stablejson.MarshalLayout(packet, stablejson.LayoutCompact) + if err != nil { + response.WriteHeader(http.StatusInternalServerError) + return + } if oneShot { if !terminal.TryCommit(packet) { response.WriteHeader(http.StatusConflict) return } } - serveWorkspaceJSON(response, request.Method, packet) + serveWorkspaceJSONBytes(response, request.Method, body) } func browserCapability() (string, error) { diff --git a/internal/command/requirementbrowser/server_test.go b/internal/command/requirementbrowser/server_test.go index 0d6182a..a8efaa0 100644 --- a/internal/command/requirementbrowser/server_test.go +++ b/internal/command/requirementbrowser/server_test.go @@ -17,6 +17,7 @@ import ( "time" "github.com/research-engineering/agentic-proofkit/internal/kernel/admission" + "github.com/research-engineering/agentic-proofkit/internal/testsupport/browserfixture" "github.com/research-engineering/agentic-proofkit/internal/testsupport/commandcoverage" ) @@ -702,122 +703,9 @@ func proofInput(t *testing.T) any { func coverageInput(t *testing.T) any { t.Helper() - input, err := admission.DecodeJSON(strings.NewReader(`{ - "schemaVersion": 2, - "viewInputId": "proofkit.browser.coverage.view", - "requirementSource": { - "schemaVersion": 1, - "sourceId": "proofkit.browser.coverage.source", - "specPackagePath": "docs/specs/browser-coverage", - "overviewPath": "docs/specs/browser-coverage/overview.md", - "requirementsPath": "docs/specs/browser-coverage/requirements.v1.json", - "requirements": [ - { - "requirementId": "REQ-BROWSER-COVERAGE-001", - "ownerId": "browser.coverage", - "invariant": "Coverage browser views render test evidence for each requirement.", - "claimLevel": "blocking", - "riskClass": "high", - "proofBindingRefs": ["proofkit/browser-coverage-bindings.json"], - "nonClaimRefs": [], - "nonClaims": ["Coverage browser fixture does not execute tests."], - "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []}, - "deferral": null, - "updatePolicy": { - "reviewOwnerId": "browser.coverage", - "requiresImpactDeclaration": true, - "requiresProofBindingReview": true - } - } - ], - "nonClaims": ["Coverage browser source fixture does not own native tests."] - }, - "requirementProofBinding": { - "schemaVersion": 1, - "bindingId": "proofkit.browser.coverage.binding", - "requirements": [ - { - "requirementId": "REQ-BROWSER-COVERAGE-001", - "ownerId": "browser.coverage", - "specPath": "docs/specs/browser-coverage/requirements.v1.json", - "claimLevel": "blocking", - "proofState": "witness_backed", - "nonClaims": ["Coverage browser binding fixture does not execute witnesses."] - } - ], - "bindings": [ - { - "requirementId": "REQ-BROWSER-COVERAGE-001", - "scenarioId": "proofkit.browser.coverage.scenario", - "witnessId": "proofkit.browser.coverage.witness", - "witnessKind": "contract", - "witnessPath": "internal/browser_coverage_test.go", - "commandIds": ["proofkit.browser.coverage.command"], - "environmentClasses": ["local-go"] - } - ], - "witnessCommands": [ - { - "commandId": "proofkit.browser.coverage.command", - "command": "go test ./internal/command/requirementbrowser", - "environmentClass": "local-go" - } - ], - "selection": {"changedPaths": [], "ownerIds": [], "requirementIds": []}, - "nonClaims": ["Coverage browser binding fixture does not prove command pass evidence."] - }, - "compactProofContract": null, - "ownerInvariantRegistry": null, - "coverageUniverse": { - "schemaVersion": 1, - "universeId": "proofkit.browser.coverage.universe", - "authority": "caller_owned_inventory", - "completenessDeclaration": "selected_owner_surfaces", - "ownerIds": ["browser.coverage"], - "codeSurfaces": [{"surfaceId": "browser.coverage.code", "ownerId": "browser.coverage", "path": "internal/command/requirementbrowser"}], - "specSurfaces": [{"surfaceId": "browser.coverage.spec", "ownerId": "browser.coverage", "path": "docs/specs/browser-coverage/requirements.v1.json"}], - "testSurfaces": [{"surfaceId": "browser.coverage.test", "ownerId": "browser.coverage", "path": "internal/command/requirementbrowser/server_test.go"}], - "commandRefs": ["proofkit.browser.coverage.command"], - "nonClaims": ["Coverage browser universe is selected-owner scope only."] - }, - "testEvidenceInventory": { - "schemaVersion": 1, - "inventoryId": "proofkit.browser.coverage.inventory", - "authority": "caller_owned_inventory", - "entries": [ - { - "testId": "test.browser.coverage.semantic", - "selector": "go test ./internal/command/requirementbrowser -run TestStartServerServesExplicitCoverageViews", - "sourcePath": "internal/command/requirementbrowser/server_test.go", - "ownerId": "browser.coverage", - "evidenceClass": "declared_semantic_falsifier_route", - "requirementRefs": ["REQ-BROWSER-COVERAGE-001"], - "ownerInvariantRefs": [], - "commandRefs": ["proofkit.browser.coverage.command"], - "witnessRefs": ["proofkit.browser.coverage.witness"], - "falsifier": { - "falsifierId": "falsifier.browser.coverage", - "negativeCaseId": "case.browser.coverage.route-only", - "wrongImplementationClassId": "wrong.browser.coverage.no-test-detail", - "dominanceGroup": "browser.coverage", - "supersedes": [] - }, - "oracle": { - "oracleId": "oracle.browser.coverage", - "oracleKind": "html_contains_test_detail", - "expectedPublicOutcome": "rendered report contains semantic test detail", - "assertionSummary": "Route-only evidence remains insufficient." - }, - "nonClaims": [] - } - ], - "nonClaims": ["Coverage browser inventory fixture does not execute native tests."] - }, - "localEnvironmentPolicy": null, - "options": {"scope": "graph"} -}`), 1<<20) + input, err := browserfixture.CoverageInput("structured") if err != nil { - t.Fatalf("decode coverage fixture: %v", err) + t.Fatal(err) } return input } diff --git a/internal/command/requirementbrowser/workspace.go b/internal/command/requirementbrowser/workspace.go index 82c2b5e..35a78cb 100644 --- a/internal/command/requirementbrowser/workspace.go +++ b/internal/command/requirementbrowser/workspace.go @@ -85,7 +85,8 @@ func buildWorkspace(raw any) (workspaceSession, string, error) { } manifest := map[string]any{ "authority": "presentation_adapter", - "availableViews": []any{"specifications", "diff", "graph"}, + "availableViews": []any{"specifications", "coverage", "diff", "graph"}, + "coverageAvailable": snapshot.Coverage != nil, "diffAvailable": diff != nil, "expectedDigestCoverage": snapshot.ExpectedDigestCoverage, "graphAvailable": graph != nil, @@ -211,12 +212,12 @@ func workspaceHTML(workspaceID string) string {

Specification hierarchy

-
+
Derived view

Authority boundary

Loading admitted authority...

    Loading workspace

    Loading admitted manifest...

    Ask about selection

    Selected source text

      -

      Handoff packet

      `, +

      Handoff packet

      Exact JSON
      `, "\n", }, "") } diff --git a/internal/command/requirementbrowser/workspace_coverage.go b/internal/command/requirementbrowser/workspace_coverage.go new file mode 100644 index 0000000..cef3951 --- /dev/null +++ b/internal/command/requirementbrowser/workspace_coverage.go @@ -0,0 +1,45 @@ +package requirementbrowser + +import "github.com/research-engineering/agentic-proofkit/internal/command/requirementcoverageview" + +// Coverage joins admitted rows after the shared filter algebra. The membership +// scan counts the complete matching cohort; only item candidates are cloned. +func workspaceCoveragePage(session *workspaceSession, query workspaceLookupQuery) workspacePage { + matches := session.Lookup.matchingRequirements(query) + matchingIDs := make(map[string]struct{}, len(matches)) + for _, position := range matches { + matchingIDs[session.Lookup.Rows[position].Requirement.RequirementID] = struct{}{} + } + coverage := session.Snapshot.Coverage + reported := requirementcoverageview.CountSelectedRequirements(coverage, matchingIDs) + start := min(query.Page.Offset, len(matches)) + end := start + min(query.Page.MaxRecords, len(matches)-start) + candidates := make(map[string]struct{}, end-start) + for _, position := range matches[start:end] { + candidates[session.Lookup.Rows[position].Requirement.RequirementID] = struct{}{} + } + fragment := requirementcoverageview.SelectRequirements(coverage, candidates) + byID := make(map[string]any, len(candidates)) + for _, raw := range fragment["requirementCoverage"].([]any) { + byID[raw.(map[string]any)["requirementId"].(string)] = raw + } + page := workspaceRequirementPage(session.Lookup, matches, query.Page) + requirementRow, requirementProjection := page.Row, page.Projection + page.Row = func(position int) map[string]any { + row := requirementRow(position) + row["coverage"] = byID[row["requirementId"].(string)] + return row + } + page.Projection = func(rows []any) (map[string]any, string) { + projection, state := requirementProjection(rows) + projection["projectionKind"] = "proofkit.requirement-browser-coverage-fragment" + projection["coverageAuthority"] = fragment["authority"] + projection["nonClaims"] = coverage["nonClaims"] + projection["proofMode"] = coverage["proofMode"] + projection["sourceViewInputId"] = fragment["sourceViewInputId"] + projection["matchingReportedRequirementCount"] = reported + projection["matchingNotReportedRequirementCount"] = len(matches) - reported + return projection, state + } + return page +} diff --git a/internal/command/requirementbrowser/workspace_coverage_test.go b/internal/command/requirementbrowser/workspace_coverage_test.go new file mode 100644 index 0000000..3914b77 --- /dev/null +++ b/internal/command/requirementbrowser/workspace_coverage_test.go @@ -0,0 +1,202 @@ +package requirementbrowser + +import ( + "bytes" + "encoding/json" + "fmt" + "net/http" + "net/http/httptest" + "reflect" + "slices" + "strings" + "testing" + + "github.com/research-engineering/agentic-proofkit/internal/command/requirementcontext" + "github.com/research-engineering/agentic-proofkit/internal/command/requirementcoverageview" + "github.com/research-engineering/agentic-proofkit/internal/kernel/admission" + "github.com/research-engineering/agentic-proofkit/internal/testsupport/browserfixture" +) + +func coverageWorkspaceFixture(t *testing.T, mode string, empty bool) map[string]any { + t.Helper() + value, err := browserfixture.CoverageWorkspace(mode, empty) + if err != nil { + t.Fatal(err) + } + return value +} + +func TestWorkspaceCoveragePairedModesPreserveWholeOwnerRows(t *testing.T) { + for _, mode := range []string{"compact", "structured"} { + t.Run(mode, func(t *testing.T) { + input := coverageWorkspaceFixture(t, mode, false) + session, _, err := buildWorkspace(input) + if err != nil { + t.Fatal(err) + } + handle, capability := startWorkspaceTestServer(t, input, false) + response := postWorkspaceJSON(t, handle.URL+"api/v1/coverage", capability, map[string]any{ + "requestId": "coverage.paired", "snapshotId": handle.SnapshotID, "query": map[string]any{"maxRecords": json.Number("1")}, + }) + projection := response["projection"].(map[string]any) + if projection["proofMode"] != mode || projection["coverageAuthority"] != "lookup_fragment_only" || session.Manifest["coverageAvailable"] != true { + t.Fatal("browser mode or coverage boundary changed") + } + assertWorkspaceRowIDs(t, projection["requirements"], "requirementId", []string{"REQ-BROWSER-COVERAGE-001"}) + got := projection["requirements"].([]any)[0].(map[string]any)["coverage"] + want := session.Snapshot.Coverage["requirementCoverage"].([]any)[0] + if !reflect.DeepEqual(got, want) { + t.Fatal("bounded browser projection lost a nested owner field") + } + for key, want := range map[string]int{ + "availableRequirementCount": 2, "matchingRequirementCount": 2, "selectedRequirementCount": 1, + "matchingReportedRequirementCount": 1, "matchingNotReportedRequirementCount": 1, + "filteredOutRequirementCount": 0, "pageOmittedRequirementCount": 1, "omittedRequirementCount": 1, + } { + if projection[key] != json.Number(fmt.Sprint(want)) { + t.Fatalf("%s = %v, want %d", key, projection[key], want) + } + } + anchor := projection["requirements"].([]any)[0].(map[string]any)["anchor"].(map[string]any) + if anchor["jsonPointer"] != "/projections/requirementSources/1/requirements/0/invariant" { + t.Fatal("coverage page rebased its source anchor") + } + selected := map[string]struct{}{"REQ-BROWSER-COVERAGE-001": {}} + fragment := requirementcoverageview.SelectRequirements(session.Snapshot.Coverage, selected) + assertOriginalCoverageFragmentKeys(t, fragment) + slice, err := requirementcontext.SliceSnapshot(session.Snapshot, map[string]any{"profile": "review", "requirementIds": []any{"REQ-BROWSER-COVERAGE-001"}}, "test.coverage.review") + if err != nil { + t.Fatal(err) + } + assertOriginalCoverageFragmentKeys(t, slice["projections"].(map[string]any)["coverage"].(map[string]any)) + packet := postWorkspaceJSON(t, handle.URL+"api/v1/handoff", capability, map[string]any{ + "annotations": []any{map[string]any{"anchorId": "requirement:REQ-BROWSER-COVERAGE-001:invariant", "startCodePoint": 0, "endCodePoint": 8, "exactQuote": "Coverage", "question": "Which evidence is declared?"}}, + }) + assertOriginalCoverageFragmentKeys(t, packet["context"].(map[string]any)["projections"].(map[string]any)["coverage"].(map[string]any)) + fragment["requirementCoverage"].([]any)[0].(map[string]any)["tests"].([]any)[0].(map[string]any)["nonClaims"] = []any{"Changed local clone."} + if reflect.DeepEqual(fragment["requirementCoverage"].([]any)[0], want) { + t.Fatal("detachment falsifier did not change its local row") + } + if !reflect.DeepEqual(session.Snapshot.Coverage["requirementCoverage"].([]any)[0], got) { + t.Fatal("selected fragment aliases the owner snapshot") + } + }) + } +} + +func assertOriginalCoverageFragmentKeys(t *testing.T, fragment map[string]any) { + t.Helper() + keys := make([]string, 0, len(fragment)) + for key := range fragment { + keys = append(keys, key) + } + slices.Sort(keys) + want := []string{"authority", "nonClaims", "requirementCoverage", "requirementCoverageCount", "schemaVersion", "sourceViewInputId", "viewKind"} + if !reflect.DeepEqual(keys, want) { + t.Fatalf("shared fragment contract changed: %v", keys) + } +} + +func TestWorkspaceCoverageFiltersBeforeCountingAndBytePaging(t *testing.T) { + session, _, err := buildWorkspace(coverageWorkspaceFixture(t, "compact", false)) + if err != nil { + t.Fatal(err) + } + for _, row := range []struct { + query map[string]any + id string + reported, missing int + }{ + {map[string]any{"offset": json.Number("1")}, "REQ-CONSUMER-001", 1, 1}, + {map[string]any{"ownerId": "browser.fixture.owner"}, "REQ-CONSUMER-001", 0, 1}, + {map[string]any{"searchText": "Coverage browser"}, "REQ-BROWSER-COVERAGE-001", 1, 0}, + } { + query, err := admitWorkspaceLookupQuery(row.query, session.Lookup) + if err != nil { + t.Fatal(err) + } + page := workspaceCoveragePage(&session, query) + encoded, err := page.encode("coverage.page", session.SnapshotID, maxWorkspaceLookupResponseBytes) + if err != nil { + t.Fatal(err) + } + response, err := admission.DecodeJSON(bytes.NewReader(encoded), int64(len(encoded))) + if err != nil { + t.Fatal(err) + } + projection := response.(map[string]any)["projection"].(map[string]any) + assertWorkspaceRowIDs(t, projection["requirements"], "requirementId", []string{row.id}) + if projection["matchingReportedRequirementCount"] != json.Number(fmt.Sprint(row.reported)) || projection["matchingNotReportedRequirementCount"] != json.Number(fmt.Sprint(row.missing)) { + t.Fatal("coverage counted the retained page instead of the filtered cohort") + } + if row.id == "REQ-CONSUMER-001" && projection["requirements"].([]any)[0].(map[string]any)["coverage"] != nil { + t.Fatal("missing row was converted into a coverage verdict") + } + } + page := workspaceCoveragePage(&session, workspaceLookupQuery{Page: projectionQuery{MaxRecords: 2}}) + full, err := page.encode("coverage.bytes", session.SnapshotID, maxWorkspaceLookupResponseBytes) + if err != nil { + t.Fatal(err) + } + bounded, err := page.encode("coverage.bytes", session.SnapshotID, len(full)-1) + if err != nil { + t.Fatal(err) + } + value, err := admission.DecodeJSON(bytes.NewReader(bounded), int64(len(bounded))) + if err != nil { + t.Fatal(err) + } + projection := value.(map[string]any)["projection"].(map[string]any) + if len(bounded) >= len(full) || projection["selectedRequirementCount"] != json.Number("1") { + t.Fatal("encoded budget failed to retain exactly one whole row") + } + got := projection["requirements"].([]any)[0].(map[string]any)["coverage"] + if !reflect.DeepEqual(got, session.Snapshot.Coverage["requirementCoverage"].([]any)[0]) { + t.Fatal("byte cut truncated a row") + } + if _, err := page.encode("coverage.bytes", session.SnapshotID, 1); err == nil { + t.Fatal("oversized metadata admitted") + } +} + +func TestWorkspaceCoverageAbsentAndAdmittedZeroRemainDistinct(t *testing.T) { + for _, mode := range []string{"compact", "structured"} { + session, _, err := buildWorkspace(coverageWorkspaceFixture(t, mode, true)) + if err != nil { + t.Fatal(err) + } + page := workspaceCoveragePage(&session, workspaceLookupQuery{Page: projectionQuery{MaxRecords: 2}}) + projection, _ := page.Projection([]any{page.Row(0)}) + if session.Manifest["coverageAvailable"] != true || projection["proofMode"] != mode || projection["matchingReportedRequirementCount"] != 0 || projection["matchingNotReportedRequirementCount"] != 1 { + t.Fatal("zero-row projection was treated as unavailable") + } + } + session, _, err := buildWorkspace(workspaceFixture(t)) + if err != nil { + t.Fatal(err) + } + if session.Manifest["coverageAvailable"] != false { + t.Fatal("absent coverage became available") + } + handle, capability := startWorkspaceTestServer(t, workspaceFixture(t), false) + request := httptest.NewRequest(http.MethodPost, "/api/v1/coverage", strings.NewReader(fmt.Sprintf(`{"query":{},"requestId":"coverage.absent","snapshotId":%q}`, handle.SnapshotID))) + request.Header.Set("Origin", "http://workspace.local") + request.Header.Set("Content-Type", "application/json") + request.Header.Set("X-Proofkit-Browser-Capability", capability) + response := httptest.NewRecorder() + serveWorkspaceRequirements(response, request, "http://workspace.local", capability, &session) + if response.Code != http.StatusNotFound { + t.Fatalf("absent coverage status %d", response.Code) + } + slice, err := requirementcontext.SliceSnapshot(session.Snapshot, map[string]any{"profile": "review", "requirementIds": []any{"REQ-CONSUMER-001"}}, "test.absent.review") + if err != nil { + t.Fatal(err) + } + if _, present := slice["projections"].(map[string]any)["coverage"]; present { + t.Fatal("review invented absent coverage") + } + packet := postWorkspaceJSON(t, handle.URL+"api/v1/handoff", capability, map[string]any{"annotations": []any{map[string]any{"anchorId": "requirement:REQ-CONSUMER-001:invariant", "startCodePoint": 0, "endCodePoint": 3, "exactQuote": "The", "question": "What is declared?"}}}) + if _, present := packet["context"].(map[string]any)["projections"].(map[string]any)["coverage"]; present { + t.Fatal("handoff invented absent coverage") + } +} diff --git a/internal/command/requirementbrowser/workspace_graph_test.go b/internal/command/requirementbrowser/workspace_graph_test.go new file mode 100644 index 0000000..05e34a5 --- /dev/null +++ b/internal/command/requirementbrowser/workspace_graph_test.go @@ -0,0 +1,104 @@ +package requirementbrowser + +import ( + "maps" + "reflect" + "testing" + + "github.com/research-engineering/agentic-proofkit/internal/testsupport/browserfixture" +) + +func TestGraphWindowDistinguishesOffPageParentsWithoutInferringEdges(t *testing.T) { + input, err := browserfixture.Workspace() + if err != nil { + t.Fatal(err) + } + topology := input["graphInput"].(map[string]any)["codeTopology"].(map[string]any) + nodes := topology["nodes"].([]any) + file := maps.Clone(nodes[0].(map[string]any)) + file["nodeId"], file["parentNodeId"], file["abstractionLevel"] = "code.file", "code.repository", "file" + symbol := maps.Clone(file) + symbol["nodeId"], symbol["parentNodeId"], symbol["abstractionLevel"] = "code.symbol", "code.file", "symbol" + nodes[1].(map[string]any)["parentNodeId"] = "code.symbol" + topology["nodes"] = append(nodes, file, symbol) + session, _, err := buildWorkspace(input) + if err != nil { + t.Fatal(err) + } + for _, pair := range [][2]string{{"code:code.retry", "code:code.symbol"}, {"code:code.symbol", "code:code.file"}, {"code:code.file", "code:code.repository"}} { + page, _ := graphWindow(session.Graph, projectionQuery{Offset: graphNodeOffset(t, session.Graph, pair[0]), MaxRecords: 1, MaxEdges: 1, EdgeOffset: 80_000}) + if !reflect.DeepEqual(page["primaryNodeIds"], []any{pair[0]}) || page["selectedNodeCount"] != 1 || page["selectedEdgeCount"] != 0 || page["boundaryNodeCount"] != 0 { + t.Fatal("parent reference expanded endpoint selection") + } + refs := page["references"].([]any) + if len(refs) != 1 { + t.Fatalf("parent reference count %d", len(refs)) + } + ref := refs[0].(map[string]any) + want := map[string]any{"disposition": "outside_page", "field": "parentNodeId", "recordId": pair[0], "recordKind": "node", "targetNodeId": pair[1], "targetOffset": graphNodeOffset(t, session.Graph, pair[1])} + if !reflect.DeepEqual(ref, want) { + t.Fatalf("parent disposition: %v", ref) + } + followed, _ := graphWindow(session.Graph, projectionQuery{Offset: ref["targetOffset"].(int), MaxRecords: 1, MaxEdges: 1}) + if !reflect.DeepEqual(followed["primaryNodeIds"], []any{pair[1]}) { + t.Fatal("follow offset opened a different target") + } + } +} + +func TestGraphWindowKeepsAuxiliaryCodeTargetSeparateFromEndpoints(t *testing.T) { + input, err := browserfixture.Workspace() + if err != nil { + t.Fatal(err) + } + session, _, err := buildWorkspace(input) + if err != nil { + t.Fatal(err) + } + primary := "requirement:REQ-CONSUMER-001" + incidentOffset := 0 + for _, raw := range session.Graph["edges"].([]any) { + edge := raw.(map[string]any) + if edge["fromNodeId"] != primary && edge["toNodeId"] != primary { + continue + } + if edge["edgeKind"] != "observed_by" { + incidentOffset++ + continue + } + page, _ := graphWindow(session.Graph, projectionQuery{Offset: graphNodeOffset(t, session.Graph, primary), MaxRecords: 1, MaxEdges: 1, EdgeOffset: incidentOffset}) + assertWorkspaceRowIDs(t, page["edges"], "edgeId", []string{edge["edgeId"].(string)}) + if !reflect.DeepEqual(page["primaryNodeIds"], []any{primary}) || page["boundaryNodeCount"] != 1 || page["selectedNodeCount"] != 2 { + t.Fatal("auxiliary reference changed endpoint closure") + } + seen := map[string]bool{} + for _, rawRef := range page["references"].([]any) { + ref := rawRef.(map[string]any) + field := ref["field"].(string) + seen[field] = true + wantDisposition := "included" + if field == "codeNodeId" { + wantDisposition = "outside_page" + } + if ref["recordId"] != edge["edgeId"] || ref["recordKind"] != "edge" || ref["targetNodeId"] != edge[field] || ref["disposition"] != wantDisposition || ref["targetOffset"] != graphNodeOffset(t, session.Graph, edge[field].(string)) { + t.Fatal("edge reference lost record, field, target or disposition") + } + } + if !reflect.DeepEqual(seen, map[string]bool{"codeNodeId": true, "fromNodeId": true, "toNodeId": true}) { + t.Fatal("edge reference field closure is incomplete") + } + return + } + t.Fatal("authored observation fixture is missing") +} + +func graphNodeOffset(t *testing.T, graph map[string]any, id string) int { + t.Helper() + for offset, raw := range graph["nodes"].([]any) { + if raw.(map[string]any)["nodeId"] == id { + return offset + } + } + t.Fatalf("fixture target %s is absent", id) + return 0 +} diff --git a/internal/command/requirementbrowser/workspace_lookup.go b/internal/command/requirementbrowser/workspace_lookup.go index b447919..9b4ee13 100644 --- a/internal/command/requirementbrowser/workspace_lookup.go +++ b/internal/command/requirementbrowser/workspace_lookup.go @@ -207,9 +207,12 @@ func (row workspaceRequirement) value() map[string]any { } func workspaceLookupPage(index workspaceLookupIndex, query workspaceLookupQuery) workspacePage { - matches := index.matchingRequirements(query) + return workspaceRequirementPage(index, index.matchingRequirements(query), query.Page) +} + +func workspaceRequirementPage(index workspaceLookupIndex, matches []int, query projectionQuery) workspacePage { return workspacePage{ - Count: len(matches), Offset: query.Page.Offset, Limit: query.Page.MaxRecords, RowsKey: "requirements", + Count: len(matches), Offset: query.Offset, Limit: query.MaxRecords, RowsKey: "requirements", Row: func(position int) map[string]any { return index.Rows[matches[position]].value() }, Projection: func(rows []any) (map[string]any, string) { state := "complete" diff --git a/internal/command/requirementbrowser/workspace_lookup_admission_test.go b/internal/command/requirementbrowser/workspace_lookup_admission_test.go index ddc6c1f..dadcd43 100644 --- a/internal/command/requirementbrowser/workspace_lookup_admission_test.go +++ b/internal/command/requirementbrowser/workspace_lookup_admission_test.go @@ -37,6 +37,11 @@ func TestWorkspaceLookupAdmissionRejectsWithoutDisclosureOrSessionMutation(t *te {"requirements", map[string]any{"ownerId": nil}}, {"requirements", map[string]any{"lifecycleState": "invented"}}, {"requirements", map[string]any{"lifecycleState": nil}}, + {"coverage", map[string]any{"searchText": sentinel}}, + {"coverage", map[string]any{sentinel: true}}, + {"coverage", map[string]any{"nodeId": "spec.unknown"}}, + {"coverage", map[string]any{"ownerId": "owner.unknown"}}, + {"coverage", map[string]any{"lifecycleState": "invented"}}, {"navigation", map[string]any{"parentNodeId": "spec.unknown"}}, {"navigation", map[string]any{"parentNodeId": nil}}, {"navigation", map[string]any{"maxRecords": json.Number("129")}}, diff --git a/internal/command/requirementbrowser/workspace_page.go b/internal/command/requirementbrowser/workspace_page.go index 4f98b29..c054d63 100644 --- a/internal/command/requirementbrowser/workspace_page.go +++ b/internal/command/requirementbrowser/workspace_page.go @@ -9,7 +9,7 @@ import ( const maxWorkspaceLookupResponseBytes = 16 << 20 -// Both private lookup routes share the encoded-page budget, not row semantics. +// Private lookup routes share the encoded-page budget, not row semantics. type workspacePage struct { Count int Offset int diff --git a/internal/command/requirementbrowser/workspace_test.go b/internal/command/requirementbrowser/workspace_test.go index a17a950..5ad4c28 100644 --- a/internal/command/requirementbrowser/workspace_test.go +++ b/internal/command/requirementbrowser/workspace_test.go @@ -82,7 +82,7 @@ func TestWorkspaceServerEnforcesCapabilityAndBuildsSourceBoundHandoff(t *testing } body, _ := io.ReadAll(handoffResponse.Body) _ = handoffResponse.Body.Close() - if handoffResponse.StatusCode != http.StatusOK || !bytes.Contains(body, []byte(`"handoffKind": "proofkit.requirement-browser-question"`)) { + if handoffResponse.StatusCode != http.StatusOK || bytes.Count(body, []byte("\n")) != 1 || body[len(body)-1] != '\n' { t.Fatalf("handoff status=%d body=%s", handoffResponse.StatusCode, body) } packet, err := admission.DecodeJSON(bytes.NewReader(body), int64(len(body))) @@ -90,6 +90,9 @@ func TestWorkspaceServerEnforcesCapabilityAndBuildsSourceBoundHandoff(t *testing t.Fatal(err) } packetRecord := packet.(map[string]any) + if packetRecord["handoffKind"] != "proofkit.requirement-browser-question" { + t.Fatal("compact handoff lost its owner identity") + } annotation := packetRecord["annotations"].([]any)[0].(map[string]any) anchor := annotation["anchor"].(map[string]any) if anchor["jsonPointer"] != "/projections/requirementSources/0/requirements/0/invariant" || anchor["sourceDigest"] != "sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" || packetRecord["snapshotRefs"].([]any)[0].(map[string]any)["snapshotId"] != handle.SnapshotID { diff --git a/internal/command/requirementcoverageview/output_admission.go b/internal/command/requirementcoverageview/output_admission.go index bf80984..0810330 100644 --- a/internal/command/requirementcoverageview/output_admission.go +++ b/internal/command/requirementcoverageview/output_admission.go @@ -126,6 +126,18 @@ func SelectRequirements(output map[string]any, selected map[string]struct{}) map } } +// CountSelectedRequirements counts membership in an owner-admitted output +// without materializing the selected nested evidence rows. +func CountSelectedRequirements(output map[string]any, selected map[string]struct{}) int { + count := 0 + for _, raw := range output["requirementCoverage"].([]any) { + if _, ok := selected[raw.(map[string]any)["requirementId"].(string)]; ok { + count++ + } + } + return count +} + func admitCoverageOutputRows(record map[string]any, rowsKey, countKey, idKey, proofMode string) error { rows, ok := record[rowsKey].([]any) if !ok { diff --git a/internal/command/requirementgraph/reference_projection.go b/internal/command/requirementgraph/reference_projection.go new file mode 100644 index 0000000..9e2a812 --- /dev/null +++ b/internal/command/requirementgraph/reference_projection.go @@ -0,0 +1,30 @@ +package requirementgraph + +// NodeReference identifies a graph-node pointer, not a source or witness ID. +type NodeReference struct { + RecordKind string + RecordID string + Field string + TargetNodeID string +} + +// NodeReferences projects known pointer fields from records selected from an +// owner-admitted output. It neither re-admits a partial graph nor creates edges. +func NodeReferences(nodes, edges []any) []NodeReference { + refs := make([]NodeReference, 0) + for _, raw := range nodes { + node := raw.(map[string]any) + if parent, present := node["parentNodeId"]; present { + refs = append(refs, NodeReference{"node", node["nodeId"].(string), "parentNodeId", parent.(string)}) + } + } + for _, raw := range edges { + edge := raw.(map[string]any) + for _, field := range []string{"codeNodeId", "fromNodeId", "toNodeId"} { + if target, present := edge[field]; present { + refs = append(refs, NodeReference{"edge", edge["edgeId"].(string), field, target.(string)}) + } + } + } + return refs +} diff --git a/internal/command/requirementgraph/reference_projection_test.go b/internal/command/requirementgraph/reference_projection_test.go new file mode 100644 index 0000000..406785e --- /dev/null +++ b/internal/command/requirementgraph/reference_projection_test.go @@ -0,0 +1,28 @@ +package requirementgraph + +import ( + "reflect" + "testing" +) + +func TestNodeReferencesPreserveTypedRecordAndFieldIdentity(t *testing.T) { + node := map[string]any{"nodeId": "code.child", "parentNodeId": "code.parent", "sourceId": "not-a-node"} + edge := map[string]any{"edgeId": "edge.observation", "codeNodeId": "code.child", "fromNodeId": "requirement.r", "toNodeId": "execution.e", "evidenceRefs": []any{"not-a-node"}} + got := NodeReferences([]any{node}, []any{edge}) + want := []NodeReference{ + {"node", "code.child", "parentNodeId", "code.parent"}, + {"edge", "edge.observation", "codeNodeId", "code.child"}, + {"edge", "edge.observation", "fromNodeId", "requirement.r"}, + {"edge", "edge.observation", "toNodeId", "execution.e"}, + } + if !reflect.DeepEqual(got, want) { + t.Fatalf("typed references: %v", got) + } + node["parentNodeId"], edge["codeNodeId"] = "changed", "changed" + if !reflect.DeepEqual(got, want) { + t.Fatal("reference projection aliases the input") + } + if len(NodeReferences(nil, nil)) != 0 { + t.Fatal("empty selection invented a reference") + } +} diff --git a/internal/testsupport/browserfixture/coverage.go b/internal/testsupport/browserfixture/coverage.go new file mode 100644 index 0000000..9cd6985 --- /dev/null +++ b/internal/testsupport/browserfixture/coverage.go @@ -0,0 +1,254 @@ +package browserfixture + +import ( + "encoding/json" + "fmt" + "sort" + "strings" + + "github.com/research-engineering/agentic-proofkit/internal/command/requirementcoverageview" + "github.com/research-engineering/agentic-proofkit/internal/command/requirementsourceadmission" + "github.com/research-engineering/agentic-proofkit/internal/command/requirementspectree" + "github.com/research-engineering/agentic-proofkit/internal/kernel/admission" + "github.com/research-engineering/agentic-proofkit/internal/kernel/digest" + "github.com/research-engineering/agentic-proofkit/internal/kernel/stablejson" +) + +// CoverageInput keeps native server and browser witnesses on the same authored +// input, not on a hand-assembled approximation of the coverage output schema. +func CoverageInput(mode string) (map[string]any, error) { + if mode != "structured" && mode != "compact" { + return nil, fmt.Errorf("unsupported coverage fixture mode") + } + value, err := admission.DecodeJSON(strings.NewReader(`{ + "schemaVersion": 2, + "viewInputId": "proofkit.browser.coverage.view", + "requirementSource": { + "schemaVersion": 1, + "sourceId": "proofkit.browser.coverage.source", + "specPackagePath": "docs/specs/browser-coverage", + "overviewPath": "docs/specs/browser-coverage/overview.md", + "requirementsPath": "docs/specs/browser-coverage/requirements.v1.json", + "requirements": [ + { + "requirementId": "REQ-BROWSER-COVERAGE-001", + "ownerId": "browser.coverage", + "invariant": "Coverage browser views render test evidence for each requirement.", + "claimLevel": "blocking", + "riskClass": "high", + "proofBindingRefs": ["proofkit/browser-coverage-bindings.json"], + "nonClaimRefs": [], + "nonClaims": ["Coverage browser fixture does not execute tests."], + "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []}, + "deferral": null, + "updatePolicy": { + "reviewOwnerId": "browser.coverage", + "requiresImpactDeclaration": true, + "requiresProofBindingReview": true + } + } + ], + "nonClaims": ["Coverage browser source fixture does not own native tests."] + }, + "requirementProofBinding": { + "schemaVersion": 1, + "bindingId": "proofkit.browser.coverage.binding", + "requirements": [ + { + "requirementId": "REQ-BROWSER-COVERAGE-001", + "ownerId": "browser.coverage", + "specPath": "docs/specs/browser-coverage/requirements.v1.json", + "claimLevel": "blocking", + "proofState": "witness_backed", + "nonClaims": ["Coverage browser binding fixture does not execute witnesses."] + } + ], + "bindings": [ + { + "requirementId": "REQ-BROWSER-COVERAGE-001", + "scenarioId": "proofkit.browser.coverage.scenario", + "witnessId": "proofkit.browser.coverage.witness", + "witnessKind": "contract", + "witnessPath": "internal/browser_coverage_test.go", + "commandIds": ["proofkit.browser.coverage.command"], + "environmentClasses": ["local-go"] + } + ], + "witnessCommands": [ + { + "commandId": "proofkit.browser.coverage.command", + "command": "go test ./internal/command/requirementbrowser", + "environmentClass": "local-go" + } + ], + "selection": {"changedPaths": [], "ownerIds": [], "requirementIds": []}, + "nonClaims": ["Coverage browser binding fixture does not prove command pass evidence."] + }, + "compactProofContract": null, + "ownerInvariantRegistry": null, + "coverageUniverse": { + "schemaVersion": 1, + "universeId": "proofkit.browser.coverage.universe", + "authority": "caller_owned_inventory", + "completenessDeclaration": "selected_owner_surfaces", + "ownerIds": ["browser.coverage"], + "codeSurfaces": [{"surfaceId": "browser.coverage.code", "ownerId": "browser.coverage", "path": "internal/command/requirementbrowser"}], + "specSurfaces": [{"surfaceId": "browser.coverage.spec", "ownerId": "browser.coverage", "path": "docs/specs/browser-coverage/requirements.v1.json"}], + "testSurfaces": [{"surfaceId": "browser.coverage.test", "ownerId": "browser.coverage", "path": "internal/command/requirementbrowser/server_test.go"}], + "commandRefs": ["proofkit.browser.coverage.command"], + "nonClaims": ["Coverage browser universe is selected-owner scope only."] + }, + "testEvidenceInventory": { + "schemaVersion": 1, + "inventoryId": "proofkit.browser.coverage.inventory", + "authority": "caller_owned_inventory", + "entries": [ + { + "testId": "test.browser.coverage.semantic", + "selector": "go test ./internal/command/requirementbrowser -run TestStartServerServesExplicitCoverageViews", + "sourcePath": "internal/command/requirementbrowser/server_test.go", + "ownerId": "browser.coverage", + "evidenceClass": "declared_semantic_falsifier_route", + "requirementRefs": ["REQ-BROWSER-COVERAGE-001"], + "ownerInvariantRefs": [], + "commandRefs": ["proofkit.browser.coverage.command"], + "witnessRefs": ["proofkit.browser.coverage.witness"], + "falsifier": { + "falsifierId": "falsifier.browser.coverage", + "negativeCaseId": "case.browser.coverage.route-only", + "wrongImplementationClassId": "wrong.browser.coverage.no-test-detail", + "dominanceGroup": "browser.coverage", + "supersedes": [] + }, + "oracle": { + "oracleId": "oracle.browser.coverage", + "oracleKind": "html_contains_test_detail", + "expectedPublicOutcome": "rendered report contains semantic test detail", + "assertionSummary": "Route-only evidence remains insufficient." + }, + "nonClaims": [] + } + ], + "nonClaims": ["Coverage browser inventory fixture does not execute native tests."] + }, + "localEnvironmentPolicy": null, + "options": {"scope": "graph"} +}`), 1<<20) + if err != nil { + return nil, err + } + input := value.(map[string]any) + if mode == "compact" { + input["requirementProofBinding"] = nil + input["localEnvironmentPolicy"] = map[string]any{"authority": "caller_provided", "localEnvironmentClasses": []any{"local-go"}} + input["testEvidenceInventory"].(map[string]any)["entries"].([]any)[0].(map[string]any)["witnessRefs"] = []any{} + command := []any{"go test ./internal/command/requirementbrowser"} + input["compactProofContract"] = map[string]any{ + "schema_version": json.Number("2"), "authority_state": "caller_owned_declaration", + "contract_id": "proofkit.browser.coverage.compact", "contract_kind": "requirement_proof_route_declaration", + "normalization_profile": "proofkit.compact.declaration.v2", + "non_claims": []any{"Compact fixture does not execute native witnesses."}, + "surface_columns": []any{"surface_id", "required_environment_classes", "preconditioned_environment_classes"}, + "surfaces": []any{[]any{"browser.coverage", []any{"local-go"}, []any{}}}, + "witness_columns": []any{"selector", "environment_classes", "verify_commands", "resolution_order_index"}, + "binding_columns": []any{"requirement_id", "surface_id", "scenario_id", "invariant_role", "owned_invariant", "blocking_status", "required_environment_classes", "positive_witness", "falsification_witness", "verify_commands", "declared_mutation_resistance_claim_id"}, + "bindings": []any{[]any{ + "REQ-BROWSER-COVERAGE-001", "browser.coverage", "browser.coverage::scenario", "contract", "browser.coverage.invariant", "blocking", []any{"local-go"}, + []any{"internal/browser_coverage_test.go::positive", []any{"local-go"}, command, json.Number("0")}, + []any{"internal/browser_coverage_test.go::falsification", []any{"local-go"}, command, json.Number("1")}, + command, "browser.coverage.mutation-claim", + }}, + } + } + return input, nil +} + +// CoverageWorkspace includes one unreported requirement alongside an actual +// owner-produced coverage report. Empty reports remain admitted present inputs. +func CoverageWorkspace(mode string, empty bool) (map[string]any, error) { + input, err := CoverageInput(mode) + if err != nil { + return nil, err + } + source := input["requirementSource"] + if empty { + source = nil + input["requirementSource"].(map[string]any)["requirements"] = []any{} + input["testEvidenceInventory"].(map[string]any)["entries"] = []any{} + if mode == "compact" { + input["compactProofContract"].(map[string]any)["bindings"] = []any{} + } else { + binding := input["requirementProofBinding"].(map[string]any) + binding["requirements"], binding["bindings"], binding["witnessCommands"] = []any{}, []any{}, []any{} + } + } + raw, _, err := requirementcoverageview.BuildJSON(input, requirementcoverageview.Options{}) + if err != nil { + return nil, err + } + coverage, err := requirementcoverageview.AdmitOutput(raw) + if err != nil { + return nil, err + } + workspace, err := Workspace() + if err != nil { + return nil, err + } + current := workspace["context"].(map[string]any) + projections := current["projections"].(map[string]any) + projections["coverage"] = coverage + sources := current["sources"].([]any) + if source != nil { + projections["requirementSources"] = append(projections["requirementSources"].([]any), source) + node := projections["specTree"].(map[string]any)["nodes"].([]any)[0].(map[string]any) + node["sourceRefs"] = append(node["sourceRefs"].([]any), map[string]any{"sourceId": "proofkit.browser.coverage.source", "sourceRefId": "spec.root.coverage", "sourceRefKind": "source_id", "sourceRole": "requirements"}) + sources = append(sources, map[string]any{ + "currentDigest": digest.SHA256TextRef("coverage source fixture"), "kind": "requirement_source", "nodeId": "spec.root", + "path": "docs/specs/browser-coverage/requirements.v1.json", "sourceRef": "proofkit.browser.coverage.source", "sourceRole": "requirements", + }) + } + encoded, err := stablejson.Marshal(coverage) + if err != nil { + return nil, err + } + sources = append(sources, map[string]any{"currentDigest": digest.SHA256TextRef(string(encoded)), "kind": "coverage", "path": "proofkit/browser-coverage.json", "sourceRef": "coverage:proofkit.browser.coverage.view"}) + sort.Slice(sources, func(i, j int) bool { + return sources[i].(map[string]any)["sourceRef"].(string) < sources[j].(map[string]any)["sourceRef"].(string) + }) + current["sources"] = sources + canonicalSources := []any{} + for _, value := range projections["requirementSources"].([]any) { + result, err := requirementsourceadmission.Evaluate(value) + if err != nil { + return nil, err + } + if result.ExitCode != 0 { + return nil, fmt.Errorf("coverage fixture source failed admission") + } + canonicalSources = append(canonicalSources, requirementsourceadmission.SourceValue(result.Source)) + } + projections["requirementSources"] = canonicalSources + tree, err := requirementspectree.Evaluate(projections["specTree"]) + if err != nil { + return nil, err + } + if tree.ExitCode != 0 { + return nil, fmt.Errorf("coverage fixture tree failed admission") + } + projections["specTree"] = requirementspectree.TreeValue(tree.Tree) + // Empty expected digests belong to the identity projection, not input fields. + identitySources := make([]any, 0, len(sources)) + for _, rawSource := range sources { + identitySource := map[string]any{"expectedDigest": ""} + for key, value := range rawSource.(map[string]any) { + identitySource[key] = value + } + identitySources = append(identitySources, identitySource) + } + identity, err := stablejson.Marshal(map[string]any{"catalogId": current["catalogId"], "sources": identitySources, "projections": projections}) + if err != nil { + return nil, err + } + current["snapshotId"] = digest.SHA256TextRef(string(identity)) + return workspace, nil +} diff --git a/internal/testsupport/browserfixture/graph.go b/internal/testsupport/browserfixture/graph.go new file mode 100644 index 0000000..ab676f2 --- /dev/null +++ b/internal/testsupport/browserfixture/graph.go @@ -0,0 +1,58 @@ +package browserfixture + +import ( + "encoding/json" + "fmt" +) + +func GraphNumericWorkspace() (map[string]any, error) { + workspace, err := Workspace() + if err != nil { + return nil, err + } + graph := workspace["graphInput"].(map[string]any) + delete(graph, "codeSources") + for _, raw := range graph["codeTopology"].(map[string]any)["nodes"].([]any) { + node := raw.(map[string]any) + if node["abstractionLevel"] == "source_range" { + node["byteStart"] = json.Number("9007199254740992") + node["byteEnd"] = json.Number("9007199254740993") + node["currentnessState"] = "unverified" + } + } + return workspace, nil +} + +// GraphCapacityWorkspace permits a native 64-primary, 128-boundary window. +// The selected requirements each have two distinct caller-reported records. +func GraphCapacityWorkspace() (map[string]any, error) { + workspace, err := LookupWorkspace() + if err != nil { + return nil, err + } + base, err := Workspace() + if err != nil { + return nil, err + } + graph := base["graphInput"].(map[string]any) + graph["context"] = workspace["context"] + topology := graph["codeTopology"].(map[string]any) + topology["edges"] = []any{} + coverage := make([]any, 0, 128) + for index := range 64 { + requirementID := "REQ-A" + if index > 0 { + requirementID = fmt.Sprintf("REQ-B-%03d", index-1) + } + for ordinal := range 2 { + coverage = append(coverage, map[string]any{ + "authorityClass": "caller_reported", "codeNodeId": "code.retry", + "currentnessState": "unverified", "evidenceRef": fmt.Sprintf("capacity.evidence.%03d.%d", index, ordinal), + "producerId": "capacity.runner", "requirementId": requirementID, "state": "failed", + }) + } + } + topology["nativeCoverage"] = coverage + workspace["graphInput"] = graph + return workspace, nil +} diff --git a/internal/tools/browsertestserver/main.go b/internal/tools/browsertestserver/main.go index 1cd75ff..a8d4acd 100644 --- a/internal/tools/browsertestserver/main.go +++ b/internal/tools/browsertestserver/main.go @@ -20,6 +20,16 @@ func main() { build = browserfixture.PagingWorkspace } else if len(os.Args) == 2 && os.Args[1] == "--capacity" { build = browserfixture.CapacityWorkspace + } else if len(os.Args) == 2 && os.Args[1] == "--graph-capacity" { + build = browserfixture.GraphCapacityWorkspace + } else if len(os.Args) == 2 && os.Args[1] == "--graph-numeric" { + build = browserfixture.GraphNumericWorkspace + } else if len(os.Args) == 2 && os.Args[1] == "--coverage-compact" { + build = func() (map[string]any, error) { return browserfixture.CoverageWorkspace("compact", false) } + } else if len(os.Args) == 2 && os.Args[1] == "--coverage-structured" { + build = func() (map[string]any, error) { return browserfixture.CoverageWorkspace("structured", false) } + } else if len(os.Args) == 2 && os.Args[1] == "--coverage-empty" { + build = func() (map[string]any, error) { return browserfixture.CoverageWorkspace("compact", true) } } else if len(os.Args) != 1 { fatal(errors.New("unsupported browser fixture selector")) } diff --git a/package-lock.json b/package-lock.json index f4b70cd..e660f78 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,12 +1,12 @@ { "name": "@research-engineering/agentic-proofkit", - "version": "0.12.0", + "version": "0.13.0", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "@research-engineering/agentic-proofkit", - "version": "0.12.0", + "version": "0.13.0", "cpu": [ "arm64", "x64" diff --git a/package.json b/package.json index 9870012..c15e9a9 100644 --- a/package.json +++ b/package.json @@ -1,7 +1,7 @@ { "name": "@research-engineering/agentic-proofkit", "description": "Reusable proof profile, report, graph, and witness-planning primitives.", - "version": "0.12.0", + "version": "0.13.0", "type": "module", "license": "MIT", "sideEffects": false, @@ -36,7 +36,7 @@ "build": "go run ./internal/tools/packagebuild", "check": "npm run npm:version && npm run source-hygiene && npm run command-contract:check && npm run command-family:check && npm run text-policy && npm run mermaid:check && npm run go:check && npm run browser:check && npm run package:artifact && npm run self:receipt && npm run self:coverage && npm run release:closeout", "browser:check": "npm run browser:static-check && npm run browser:test", - "browser:static-check": "tsc -p tsconfig.browser.json && node --test scripts/browser-proof-execution.test.mjs scripts/browser-proof-inputs.test.mjs scripts/browser-selection-authority.test.mjs scripts/browser-workspace-requests.test.mjs scripts/diagnostic-entrypoints.test.mjs scripts/stable-json.test.mjs", + "browser:static-check": "tsc -p tsconfig.browser.json && node --test scripts/browser-evidence-models.test.mjs scripts/browser-proof-execution.test.mjs scripts/browser-proof-inputs.test.mjs scripts/browser-selection-authority.test.mjs scripts/browser-workspace-requests.test.mjs scripts/diagnostic-entrypoints.test.mjs scripts/stable-json.test.mjs", "browser:test": "go run ./internal/tools/browserproofverify --run", "command-family:check": "go run ./internal/tools/commandfamilygen --check", "go:actionlint": "go tool actionlint", diff --git a/proofkit/requirement-bindings.json b/proofkit/requirement-bindings.json index 126f02b..eebec6f 100644 --- a/proofkit/requirement-bindings.json +++ b/proofkit/requirement-bindings.json @@ -800,6 +800,38 @@ "proofState": "witness_backed", "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."] }, + { + "requirementId": "REQ-PROOFKIT-SPEC-038", + "ownerId": "proofkit.spec-proof-core", + "specPath": "docs/specs/proofkit-spec-proof-core/requirements.v1.json", + "claimLevel": "blocking", + "proofState": "witness_backed", + "nonClaims": ["Coverage presentation does not execute witnesses, authenticate declared evidence, infer a verdict for absent rows, or approve merge, release, rollout or production readiness."] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "ownerId": "proofkit.spec-proof-core", + "specPath": "docs/specs/proofkit-spec-proof-core/requirements.v1.json", + "claimLevel": "blocking", + "proofState": "witness_backed", + "nonClaims": ["A displayed topology, local filter or layout is not evidence of source completeness, proof truth, native execution, publication, rollout or production readiness. Browser-emulated mobile interaction does not certify physical devices or operating-system behavior."] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-040", + "ownerId": "proofkit.spec-proof-core", + "specPath": "docs/specs/proofkit-spec-proof-core/requirements.v1.json", + "claimLevel": "blocking", + "proofState": "witness_backed", + "nonClaims": ["A question packet does not establish live checkout freshness, native witness execution, agent delivery, annotation persistence, merge approval or production readiness. Already exported bytes are not revoked by later view changes."] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-041", + "ownerId": "proofkit.spec-proof-core", + "specPath": "docs/specs/proofkit-spec-proof-core/requirements.v1.json", + "claimLevel": "blocking", + "proofState": "witness_backed", + "nonClaims": ["Diff counts, risk labels and presentation do not determine compatibility, source authenticity, witness truth, merge approval, publication or production readiness."] + }, { "requirementId": "REQ-PROOFKIT-WORKFLOW-001", "ownerId": "proofkit.agent-workflow", @@ -5555,6 +5587,184 @@ "commandIds": ["proofkit.browser-check"], "environmentClasses": ["local-node-browser"] }, + { + "requirementId": "REQ-PROOFKIT-SPEC-038", + "scenarioId": "proofkit.spec-proof-core.coverage-owner-join", + "witnessId": "proofkit.coverage-owner-join.falsifier", + "witnessKind": "contract", + "witnessPath": "internal/command/requirementbrowser/workspace_coverage_test.go", + "commandIds": [ + "proofkit.go-test" + ], + "environmentClasses": [ + "local-go" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-038", + "scenarioId": "proofkit.spec-proof-core.coverage-native-interaction", + "witnessId": "proofkit.coverage-native-interaction.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-evidence.spec.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "scenarioId": "proofkit.spec-proof-core.graph-reference-owner", + "witnessId": "proofkit.graph-reference-owner.falsifier", + "witnessKind": "contract", + "witnessPath": "internal/command/requirementgraph/reference_projection_test.go", + "commandIds": [ + "proofkit.go-test" + ], + "environmentClasses": [ + "local-go" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "scenarioId": "proofkit.spec-proof-core.graph-reference-window", + "witnessId": "proofkit.graph-reference-window.falsifier", + "witnessKind": "contract", + "witnessPath": "internal/command/requirementbrowser/workspace_graph_test.go", + "commandIds": [ + "proofkit.go-test" + ], + "environmentClasses": [ + "local-go" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "scenarioId": "proofkit.spec-proof-core.graph-model-algebra", + "witnessId": "proofkit.graph-model-algebra.falsifier", + "witnessKind": "technical", + "witnessPath": "scripts/browser-evidence-models.test.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "scenarioId": "proofkit.spec-proof-core.graph-native-interaction", + "witnessId": "proofkit.graph-native-interaction.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-graph.spec.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "scenarioId": "proofkit.spec-proof-core.graph-native-reflow", + "witnessId": "proofkit.graph-native-reflow.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-evidence-layout.spec.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-039", + "scenarioId": "proofkit.spec-proof-core.graph-numeric-observation", + "witnessId": "proofkit.graph-numeric-observation.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-graph.spec.mjs", + "commandIds": ["proofkit.browser-check"], + "environmentClasses": ["local-node-browser"] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-040", + "scenarioId": "proofkit.spec-proof-core.handoff-whole-packet", + "witnessId": "proofkit.handoff-whole-packet.falsifier", + "witnessKind": "contract", + "witnessPath": "internal/command/requirementbrowser/workspace_test.go", + "commandIds": [ + "proofkit.go-test" + ], + "environmentClasses": [ + "local-go" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-040", + "scenarioId": "proofkit.spec-proof-core.handoff-exact-carrier", + "witnessId": "proofkit.handoff-exact-carrier.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-evidence.spec.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-040", + "scenarioId": "proofkit.spec-proof-core.handoff-pending-lock", + "witnessId": "proofkit.handoff-pending-lock.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-locking.spec.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-040", + "scenarioId": "proofkit.spec-proof-core.handoff-native-reflow", + "witnessId": "proofkit.handoff-native-reflow.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-evidence-layout.spec.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-041", + "scenarioId": "proofkit.spec-proof-core.diff-class-facets", + "witnessId": "proofkit.diff-class-facets.falsifier", + "witnessKind": "technical", + "witnessPath": "scripts/browser-evidence-models.test.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, + { + "requirementId": "REQ-PROOFKIT-SPEC-041", + "scenarioId": "proofkit.spec-proof-core.diff-native-page", + "witnessId": "proofkit.diff-native-page.falsifier", + "witnessKind": "technical", + "witnessPath": "tests/browser/workspace-paging.spec.mjs", + "commandIds": [ + "proofkit.browser-check" + ], + "environmentClasses": [ + "local-node-browser" + ] + }, { "requirementId": "REQ-PROOFKIT-QUALITY-022", "scenarioId": "proofkit.supply-chain-quality.browser-static-and-runtime-proof", diff --git a/proofkit/witness-plan.json b/proofkit/witness-plan.json index a56d795..736949b 100644 --- a/proofkit/witness-plan.json +++ b/proofkit/witness-plan.json @@ -790,6 +790,7 @@ "package.json", "playwright.config.mjs", "proofkit/witness-plan.json", + "scripts/browser-evidence-models.test.mjs", "scripts/browser-proof-execution.mjs", "scripts/browser-proof-execution.test.mjs", "scripts/browser-proof-inputs.mjs", diff --git a/release/change-record.v2.json b/release/change-record.v2.json index 682339b..b2d052b 100644 --- a/release/change-record.v2.json +++ b/release/change-record.v2.json @@ -1,21 +1,21 @@ { "schemaVersion": 2, - "previousVersion": "0.11.0", - "version": "0.12.0", + "previousVersion": "0.12.0", + "version": "0.13.0", "changeClass": "compatible", "breakingChanges": [], "additions": [ { - "changeId": "proofkit.browser.lookup", - "summary": "Search and filter the complete admitted requirement cohort before bounded paging, navigate ordered specification children, and preserve original source anchors and exact omission counts without loading the full snapshot into the browser." + "changeId": "proofkit.browser.coverage-inspection", + "summary": "Inspect compact or structured coverage beside original source-bound requirements, distinguish missing evidence from reported verdicts, preserve complete evidence and non-claims in disclosures, and ask an explicit evidence question without replacing an existing draft." }, { - "changeId": "proofkit.browser.request-recovery", - "summary": "Distinguish correction, denied, stale, unavailable and retryable failures. Explicit Retry preserves the failed route, snapshot and complete page query, while superseded requests cannot restore stale content or request authority." + "changeId": "proofkit.browser.diff-and-graph-inspection", + "summary": "Show exact diff-page class, entity, risk and lifecycle counts. Inspect a bounded traceability diagram and equivalent records with local evidence-plane and neighborhood filters, preserved directed relations, exact numeric source coordinates, explicit outside-page references and deliberate target-page navigation." }, { - "changeId": "proofkit.browser.responsive-shell", - "summary": "Add compact Browse and Inspector panels with native modal behavior on smaller viewports, stable keyboard focus, retained question drafts, source-bound Unicode selection and lazy boundary details." + "changeId": "proofkit.browser.handoff-inspection", + "summary": "Preview included source-bound handoff context by stable requirement identity and explicitly copy or download the exact compact server JSON. Obsolete view or clipboard results cannot replace current output; independent pending exclusion and denied or stale request locks survive settlement, with one workspace reload action for a stale session." } ], "migration": { @@ -36,7 +36,7 @@ "TSX source parsing remains unsupported.", "Managed integration baselines are cooperative byte/mode bookkeeping, not authenticated origin or protection against coordinated same-user edits. File lifecycle does not prove native host discovery, instruction loading, or approved-launcher invocation.", "Desired-absence journals and newly retained terminal receipts use schema v2. Earlier binaries reject these records without effects. Present-only v1 plan/journal bytes and historical recovery remain supported; finishing recovery does not enable downgrade of retained v2 receipts.", - "Browser lookup and navigation are presentation-only fragments, not proof coverage or an external HTTP SDK. Annotations are session-bound; browser controls do not edit specifications or execute agents." + "Browser lookup, coverage, diff and graph fragments are derived presentation, not authenticated evidence, proof execution or an external HTTP SDK. Local graph filters apply only to the returned page; absent coverage is not a verdict. Exact numeric observation requires native JSON source-token and raw-value support; unsupported clients show unavailable instead of rounded coordinates. Annotations are session-bound and exported bytes are not revoked by later navigation; browser controls do not edit specifications or execute agents." ], "rollback": { "strategy": "previous_admitted_version" diff --git a/scripts/browser-evidence-models.test.mjs b/scripts/browser-evidence-models.test.mjs new file mode 100644 index 0000000..a465b91 --- /dev/null +++ b/scripts/browser-evidence-models.test.mjs @@ -0,0 +1,81 @@ +import assert from "node:assert/strict"; +import test from "node:test"; +import {summarizeDiffPage} from "../internal/command/requirementbrowser/assets/workspace-diff.js"; +import {GRAPH_PAGE, GRAPH_PLANES, graphPagePositions, visibleGraphPage} from "../internal/command/requirementbrowser/assets/workspace-graph.js"; +import {resolveHandoffRequirement} from "../internal/command/requirementbrowser/assets/workspace-handoff.js"; + +test("diff page classes partition changes while risk and lifecycle remain independent facets", () => { + const changes = [ + {entityId: "REQ-A", entityKind: "requirement", changeClass: "scalar_changed", jsonPointer: "/requirements/REQ-A/riskClass"}, + {entityId: "REQ-A", entityKind: "requirement", changeClass: "scalar_changed", jsonPointer: "/requirements/REQ-A/invariant"}, + {entityId: "REQ-B", entityKind: "requirement", changeClass: "entity_added", after: {riskClass: "high"}}, + {entityId: "REQ-C", entityKind: "requirement", changeClass: "entity_removed", before: {riskClass: "high"}}, + {entityId: "REQ-C", entityKind: "requirement", changeClass: "lifecycle_transition"}, + {entityId: "REQ-D", entityKind: "requirement", changeClass: "set_changed", jsonPointer: "/requirements/REQ-D/riskClass"}, + {entityId: "REQ-A", entityKind: "source", changeClass: "scalar_changed", jsonPointer: "/requirements/REQ-A/riskClass"}, + {entityId: "REQ-A", entityKind: "requirement", changeClass: "scalar_changed", jsonPointer: "/requirements/REQ-X/riskClass"}, + ]; + const summary = summarizeDiffPage(changes); + assert.deepEqual(summary, {changeCount: 8, entityCount: 4, riskChanges: 1, lifecycleChanges: 1, byClass: [["entity_added", 1], ["entity_removed", 1], ["lifecycle_transition", 1], ["scalar_changed", 4], ["set_changed", 1]]}); + assert.equal(summary.byClass.reduce((count, [, value]) => count + value, 0), changes.length); + assert.deepEqual(summarizeDiffPage([]), {changeCount: 0, entityCount: 0, riskChanges: 0, lifecycleChanges: 0, byClass: []}); + assert.equal(summarizeDiffPage([{entityId: "A/~", entityKind: "requirement", changeClass: "scalar_changed", jsonPointer: "/requirements/A~1~0/riskClass"}]).riskChanges, 1); +}); + +const spec = "specification_coverage", code = "code_traceability", proof = "proof_coverage", native = "native_execution_coverage"; +const graph = { + nodes: [ + {nodeId: "a", evidencePlane: spec}, {nodeId: "b", evidencePlane: code}, + {nodeId: "c", evidencePlane: proof}, {nodeId: "d", evidencePlane: code}, + {nodeId: "e", evidencePlane: native}, {nodeId: "isolated", evidencePlane: spec}, + ], + edges: [ + {edgeId: "ab1", fromNodeId: "a", toNodeId: "b", evidencePlane: code}, + {edgeId: "ab2", fromNodeId: "b", toNodeId: "a", evidencePlane: code}, + {edgeId: "ac", fromNodeId: "a", toNodeId: "c", evidencePlane: proof}, + {edgeId: "bc", fromNodeId: "b", toNodeId: "c", evidencePlane: code}, + {edgeId: "bd", fromNodeId: "b", toNodeId: "d", evidencePlane: code}, + {edgeId: "ae", fromNodeId: "a", toNodeId: "e", evidencePlane: native}, + ], +}; +const allPlanes = new Set(GRAPH_PLANES.map(plane => plane.id)); +const identities = page => ({nodes: page.nodes.map(node => node.nodeId), edges: page.edges.map(edge => edge.edgeId), selectedId: page.selectedId, neighborhood: page.neighborhood}); + +test("graph visibility closes endpoints and preserves induced directed parallel relations", () => { + const original = JSON.stringify(graph); + // Opaque helper graphs are broader than current Go-built edge/plane pairs. + // These defensive operand tests do not prove source-built reachability. + assert.deepEqual(identities(visibleGraphPage(graph, new Set([spec, code]), null, false)), {nodes: ["a", "b", "d", "isolated"], edges: ["ab1", "ab2", "bd"], selectedId: null, neighborhood: false}); + assert.deepEqual(identities(visibleGraphPage(graph, new Set([code]), null, false)), {nodes: ["b", "d"], edges: ["bd"], selectedId: null, neighborhood: false}); + assert.deepEqual(identities(visibleGraphPage(graph, allPlanes, "a", true)), {nodes: ["a", "b", "c", "e"], edges: ["ab1", "ab2", "ac", "bc", "ae"], selectedId: "a", neighborhood: true}); + assert.deepEqual(identities(visibleGraphPage(graph, new Set([spec, code]), "a", true)), {nodes: ["a", "b"], edges: ["ab1", "ab2"], selectedId: "a", neighborhood: true}); + assert.deepEqual(identities(visibleGraphPage(graph, new Set([spec]), "b", true)), {nodes: ["a", "isolated"], edges: [], selectedId: null, neighborhood: false}); + assert.deepEqual(identities(visibleGraphPage(graph, allPlanes, "isolated", true)), {nodes: ["isolated"], edges: [], selectedId: "isolated", neighborhood: true}); + assert.deepEqual(identities(visibleGraphPage(graph, new Set(), "a", true)), {nodes: [], edges: [], selectedId: null, neighborhood: false}); + assert.equal(JSON.stringify(graph), original); + assert.equal(visibleGraphPage(graph, allPlanes, null, true).neighborhood, false); +}); + +test("maximum graph page layout is stable, bounded and non-overlapping", () => { + assert.deepEqual(GRAPH_PAGE, {maxRecords: 64, maxEdges: 128}); + const nodes = Array.from({length: 192}, (_, index) => ({nodeId: `node.${String(index).padStart(3, "0")}`, evidencePlane: GRAPH_PLANES[index % 4].id})); + const layout = graphPagePositions(nodes); + assert.deepEqual(graphPagePositions([...nodes].reverse()), layout); + assert.equal(layout.positions.size, 192); + for (const [id, position] of layout.positions) { + assert(position.x >= 0 && position.x + 240 <= layout.width); + assert(position.y >= 0 && position.y + 96 <= layout.height); + for (const [otherId, other] of layout.positions) if (id !== otherId) assert(position.x + 240 <= other.x || other.x + 240 <= position.x || position.y + 96 <= other.y || other.y + 96 <= position.y); + } + assert.equal(graphPagePositions([]).height, 180); +}); + +test("handoff detail resolution uses requirement identity rather than unsliced source offsets", () => { + const requirement = {requirementId: "REQ-B", invariant: "Selected requirement."}; + const source = {requirements: [requirement]}; + const packet = {context: {projections: {requirementSources: [source]}}}; + assert.deepEqual(resolveHandoffRequirement(packet, "REQ-B"), {state: "found", requirement}); + assert.deepEqual(resolveHandoffRequirement(packet, "REQ-A"), {state: "unavailable", requirement: null}); + packet.context.projections.requirementSources.push({requirements: [{...requirement}]}); + assert.deepEqual(resolveHandoffRequirement(packet, "REQ-B"), {state: "ambiguous", requirement: null}); +}); diff --git a/scripts/browser-runtime-proof-inputs.v1.json b/scripts/browser-runtime-proof-inputs.v1.json index 2f8062e..aa96092 100644 --- a/scripts/browser-runtime-proof-inputs.v1.json +++ b/scripts/browser-runtime-proof-inputs.v1.json @@ -11,6 +11,7 @@ "package.json", "playwright.config.mjs", "proofkit/witness-plan.json", + "scripts/browser-evidence-models.test.mjs", "scripts/browser-proof-execution.mjs", "scripts/browser-proof-execution.test.mjs", "scripts/browser-proof-inputs.mjs", diff --git a/scripts/browser-workspace-requests.test.mjs b/scripts/browser-workspace-requests.test.mjs index 42d46af..3f33b59 100644 --- a/scripts/browser-workspace-requests.test.mjs +++ b/scripts/browser-workspace-requests.test.mjs @@ -2,7 +2,8 @@ import assert from "node:assert/strict"; import {createServer} from "node:http"; import test from "node:test"; -import {fetchWorkspaceJSON, workspaceFailure, WorkspaceRequestError} from "../internal/command/requirementbrowser/assets/workspace-requests.js"; +import {fetchWorkspaceJSON, fetchWorkspaceResponse, workspaceFailure, WorkspaceRequestError} from "../internal/command/requirementbrowser/assets/workspace-requests.js"; +import {workspaceScalarText} from "../internal/command/requirementbrowser/assets/workspace-json.js"; async function endpoint(t, respond) { const received = Promise.withResolvers(); @@ -77,6 +78,20 @@ test("a successful complete JSON body retains its admitted value", async t => { assert.deepEqual(await fetchWorkspaceJSON(fixture.url, {}), {requestId: "request.example", rows: [1]}); }); +test("the raw response carrier preserves exact numeric and escaped JSON bytes", async t => { + const body = '{"number":9007199254740993,"escaped":"\\u0061","text":"\\u{1F642}"}\n'.replace("\\u{1F642}", "\\ud83d\\ude42"); + let calls = 0; + const fixture = await endpoint(t, response => { + calls++; + response.writeHead(200, {"Content-Type": "application/json"}); + response.end(body); + }); + const result = await fetchWorkspaceResponse(fixture.url, {}); + assert.equal(result.text, body); + assert.notEqual(JSON.stringify(result.value) + "\n", body); + assert.equal(calls, 1); +}); + test("HTTP status owns recovery before an unconsumed malformed body", async t => { const fixture = await endpoint(t, response => { response.writeHead(409, {"Content-Type": "application/json", "Content-Length": "200"}); @@ -89,3 +104,46 @@ test("HTTP status owns recovery before an unconsumed malformed body", async t => message: "The workspace snapshot has changed.", action: "reload", lock: true, kind: "stale", }); }); + +test("HTTP numeric observations retain exact tokens and native scalar branding", async t => { + const body = '{"start":9007199254740992,"end":9007199254740993,"safe":9007199254740991,"zero":0,"string":"9007199254740993","nested":[1.0000000000000001,1e-400,-0,1e400,-9007199254740993,0.123456789012345678901],"unbranded":{"rawJSON":"17"}}'; + const fixture = await endpoint(t, response => response.end(body)); + const {value, text} = await fetchWorkspaceResponse(fixture.url, {}); + assert.equal(text, body); + assert.equal(JSON.stringify(value), body); + assert.equal(workspaceScalarText(value.start), "9007199254740992"); + assert.equal(workspaceScalarText(value.end), "9007199254740993"); + assert.equal(value.safe, 9007199254740991); + assert.equal(value.zero, 0); + assert.equal(typeof value.string, "string"); + assert.equal(value.string, "9007199254740993"); + assert.equal(JSON.isRawJSON(value.unbranded), false); + assert.equal(workspaceScalarText(value.unbranded), "[object Object]"); + for (const raw of [value.start, value.end, ...value.nested]) { + assert.equal(JSON.isRawJSON(raw), true); + assert.equal(Object.isFrozen(raw), true); + assert.equal(Object.getPrototypeOf(raw), null); + } +}); + +test("missing native numeric factories fail closed without a rounded success", async t => { + const fixture = await endpoint(t, response => response.end("9007199254740993")); + for (const name of ["rawJSON", "isRawJSON"]) { + const descriptor = Object.getOwnPropertyDescriptor(JSON, name); + assert(descriptor); + try { + Object.defineProperty(JSON, name, {...descriptor, value: undefined}); + const error = await fetchWorkspaceJSON(fixture.url, {}).catch(error => error); + assert(error instanceof SyntaxError); + assert.deepEqual(workspaceFailure(error), {message: "The admitted workspace is unavailable.", action: "none", lock: false, kind: "unavailable"}); + } finally { Object.defineProperty(JSON, name, descriptor); } + } +}); + +test("missing reviver source context cannot admit rounded numeric observations", async t => { + const nativeParse = JSON.parse; + t.mock.method(JSON, "parse", (source, reviver) => typeof reviver === "function" ? nativeParse(source, (key, value) => reviver(key, value)) : nativeParse(source, reviver)); + assert.deepEqual(JSON.parse('{"unrelated":1}'), {unrelated: 1}); + const fixture = await endpoint(t, response => response.end("1.0000000000000001")); + await assert.rejects(fetchWorkspaceJSON(fixture.url, {}), {name: "SyntaxError", message: "Exact numeric observation is unavailable"}); +}); diff --git a/tests/browser/workspace-evidence-layout.spec.mjs b/tests/browser/workspace-evidence-layout.spec.mjs new file mode 100644 index 0000000..94bba63 --- /dev/null +++ b/tests/browser/workspace-evidence-layout.spec.mjs @@ -0,0 +1,61 @@ +import {expect} from "@playwright/test"; +import {coverageTest as test} from "./workspace-test-harness.mjs"; +import {openWorkspace} from "./workspace-navigation-harness.mjs"; +import {analyzeAxe, assertAxeTestComplete, initializeAxe} from "./axe-harness.mjs"; + +const viewports = [ + {width: 320, height: 640, view: "coverage", colorScheme: "light"}, + {width: 390, height: 844, view: "graph", colorScheme: "dark"}, + {width: 844, height: 390, view: "coverage", colorScheme: "light"}, + {width: 768, height: 1024, view: "graph", colorScheme: "light"}, + {width: 1280, height: 800, view: "coverage", colorScheme: "dark"}, + {width: 1920, height: 1080, view: "graph", colorScheme: "light"}, + {width: 640, height: 400, view: "coverage", colorScheme: "light"}, +]; + +for (const viewport of viewports) { + test(`evidence ${viewport.view} reflows at ${viewport.width}x${viewport.height} ${viewport.colorScheme}`, async ({compactURL, page}, testInfo) => { + await page.setViewportSize({width: viewport.width, height: viewport.height}); + await page.emulateMedia({colorScheme: viewport.colorScheme, reducedMotion: "reduce"}); + await initializeAxe(page); + const errors = []; + page.on("pageerror", error => errors.push(error.message)); + await openWorkspace(page, compactURL); + await page.getByRole("button", {name: viewport.view === "coverage" ? "Coverage" : "Traceability", exact: true}).click(); + await expect(page.locator("body")).toHaveAttribute("data-state", viewport.view); + expect(await page.evaluate(() => document.documentElement.scrollWidth <= innerWidth + 1)).toBe(true); + if (viewport.view === "coverage") { + const ask = page.locator(".coverage-record").first().getByRole("button", {name: "Ask about evidence", exact: true}); + await ask.focus(); + await page.keyboard.press("Enter"); + const question = page.getByRole("textbox", {name: "Question", exact: true}); + await expect(question).toBeFocused(); + await question.fill("Keep \u{1F680} e\u0301 and \u05d0\u05d1 unchanged."); + await page.getByRole("button", {name: "Create handoff packet", exact: true}).click(); + await expect(page.locator("#handoff-status")).toHaveText("Handoff packet created."); + await expect(page.getByRole("button", {name: "Copy JSON", exact: true})).toBeVisible(); + await expect(page.getByRole("button", {name: "Download JSON", exact: true})).toBeVisible(); + await expect(question).toHaveValue("Keep \u{1F680} e\u0301 and \u05d0\u05d1 unchanged."); + const bounds = await page.locator("#workspace-inspector").evaluate(element => ({width: element.clientWidth, scroll: element.scrollWidth})); + expect(bounds.scroll).toBeLessThanOrEqual(bounds.width + 1); + if (viewport.width <= 1024) { + await page.getByRole("button", {name: "Close inspector", exact: true}).click(); + await expect(ask).toBeFocused(); + } + } else { + const records = page.getByRole("list", {name: "Admitted traceability nodes"}); + const first = records.getByRole("button").first(); + await first.focus(); + await page.keyboard.press("Enter"); + await expect(first).toBeFocused(); + await expect(page.locator(".graph-inspector > dl")).toBeVisible(); + await expect(page.getByRole("region", {name: "Traceability graph viewport"})).toBeVisible({visible: viewport.width > 768}); + expect(await page.evaluate(() => document.documentElement.scrollWidth <= innerWidth + 1)).toBe(true); + } + expect((await analyzeAxe(page)).violations).toEqual([]); + assertAxeTestComplete(page); + expect(errors).toEqual([]); + await page.evaluate(() => window.scrollTo(0, 0)); + await testInfo.attach("evidence-viewport.png", {body: await page.screenshot(), contentType: "image/png"}); + }); +} diff --git a/tests/browser/workspace-evidence.spec.mjs b/tests/browser/workspace-evidence.spec.mjs new file mode 100644 index 0000000..48bf774 --- /dev/null +++ b/tests/browser/workspace-evidence.spec.mjs @@ -0,0 +1,226 @@ +import {expect} from "@playwright/test"; +import {coverageTest, test} from "./workspace-test-harness.mjs"; +import {openWorkspace} from "./workspace-navigation-harness.mjs"; +import {analyzeAxe, assertAxeTestComplete, initializeAxe} from "./axe-harness.mjs"; + +async function openCoverage(page, url) { + await openWorkspace(page, url); + await expect(page.locator("#workspace-content")).toHaveAttribute("aria-busy", "false"); + const response = page.waitForResponse(response => response.url().endsWith("/api/v1/coverage") && response.request().method() === "POST"); + await page.getByRole("button", {name: "Coverage", exact: true}).click(); + const packet = await (await response).json(); + await expect(page.locator("body")).toHaveAttribute("data-state", "coverage"); + return packet.projection; +} + +for (const mode of ["compact", "structured"]) { + coverageTest(`coverage ${mode} preserves reported and unreported evidence without a verdict upgrade`, async ({compactURL, structuredURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + await initializeAxe(page); + const projection = await openCoverage(page, mode === "compact" ? compactURL : structuredURL); + expect(projection.proofMode).toBe(mode); + const boundary = page.locator("details.projection-boundary"); + await expect(boundary).not.toHaveAttribute("open"); + await boundary.locator("summary").click(); + await expect(boundary.locator("li")).toHaveText(projection.nonClaims); + await boundary.locator("summary").click(); + await expect(page.locator("[data-coverage-summary]")).toHaveText(`1 reported; 1 not reported in 2 matching requirements. Mode: ${mode}.`); + const rows = page.locator(".coverage-record"); + await expect(rows).toHaveCount(2); + for (const requirement of projection.requirements) { + const row = rows.filter({has: page.getByRole("heading", {name: requirement.requirementId, exact: true})}); + const state = row.locator(".coverage-state"); + await expect(row.locator("[data-anchor-id]")).toHaveText(requirement.invariant); + await expect(row.locator("[data-anchor-id]")).toHaveAttribute("data-anchor-id", requirement.anchor.anchorId); + if (requirement.coverage === null) { + await expect(state.locator("dt")).toHaveText(["Coverage"]); + await expect(state.locator("dd")).toHaveText(["Not reported"]); + } else { + const evidence = requirement.coverage; + await expect(state.locator("dd")).toHaveText([evidence.coverageState, evidence.evidenceClass, evidence.claimLevel, evidence.lifecycleState, String(evidence.scenarioCount), String(evidence.tests.length), String((mode === "compact" ? evidence.declaredWitnessRoutes : evidence.witnessRefs).length)]); + await row.locator(".coverage-details > summary").click(); + await expect(row.locator(".coverage-details")).toContainText("Route-only evidence remains insufficient."); + expect(await row.locator(".coverage-details pre").allTextContents()).toEqual([evidence.scenarios, evidence.tests, mode === "compact" ? evidence.declaredWitnessRoutes : evidence.witnessRefs].map(value => JSON.stringify(value, null, 2))); + await expect(row.locator(".coverage-details")).toContainText(requirement.sourceNonClaims[0]); + } + } + expect((await analyzeAxe(page)).violations).toEqual([]); + assertAxeTestComplete(page); + }); + + coverageTest(`coverage ${mode} question action uses an explicit anchor without overwriting a draft`, async ({compactURL, structuredURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + const projection = await openCoverage(page, mode === "compact" ? compactURL : structuredURL); + const requirement = projection.requirements.find(row => row.coverage !== null); + const row = page.locator(`.coverage-record[data-requirement-id="${requirement.requirementId}"]`); + const ask = row.getByRole("button", {name: "Ask about evidence", exact: true}); + const question = page.getByRole("textbox", {name: "Question", exact: true}); + let submissions = 0; + page.on("request", request => { if (request.url().endsWith("/api/v1/handoff")) submissions++; }); + await ask.focus(); + await page.keyboard.press("Enter"); + await expect(question).toBeFocused(); + await expect(question).toHaveValue(`What evidence supports ${requirement.requirementId}?`); + for (const draft of [" ", "Keep my question \u{1F680}."]) { + await question.fill(draft); + await ask.click(); + await expect(question).toBeFocused(); + await expect(question).toHaveValue(draft); + await expect(page.locator("#workspace-inspector")).toBeVisible(); + } + expect(submissions).toBe(0); + const response = page.waitForResponse(response => response.url().endsWith("/api/v1/handoff")); + await page.getByRole("button", {name: "Create handoff packet"}).click(); + const raw = await (await response).text(); + await expect(page.locator("#handoff-packet")).toHaveText(raw, {useInnerText: false}); + const packet = JSON.parse(raw); + expect(packet.annotations.map(annotation => ({id: annotation.anchor.requirementId, quote: annotation.exactQuote, question: annotation.question}))).toEqual([{id: requirement.requirementId, quote: requirement.invariant, question: "Keep my question \u{1F680}."}]); + await page.locator("#handoff-preview article details > summary").click(); + await expect(page.locator('[data-handoff-detail="found"]')).toHaveText(requirement.invariant); + expect(submissions).toBe(1); + await page.getByRole("searchbox").fill("REQ-CONSUMER-001"); + await page.getByRole("button", {name: "Search requirements", exact: true}).click(); + await expect(page.locator("body")).toHaveAttribute("data-state", "coverage"); + await expect(page.locator(".coverage-record")).toHaveAttribute("data-requirement-id", "REQ-CONSUMER-001"); + await expect(page.locator("[data-coverage-summary]")).toHaveText(`0 reported; 1 not reported in 1 matching requirements. Mode: ${mode}.`); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + }); +} + +coverageTest("an admitted empty coverage report differs from an absent report", async ({emptyCoverageURL, baseURL, page}) => { + const projection = await openCoverage(page, emptyCoverageURL); + expect(projection.proofMode).toBe("compact"); + await expect(page.locator("[data-coverage-summary]")).toHaveText("0 reported; 1 not reported in 1 matching requirements. Mode: compact."); + await expect(page.locator(".coverage-state dd")).toHaveText(["Not reported"]); + await openWorkspace(page, baseURL); + await page.getByRole("button", {name: "Coverage", exact: true}).click(); + await expect(page.locator("body")).toHaveAttribute("data-state", "coverage-unavailable"); + await expect(page.locator("#workspace-content")).toContainText("No admitted coverage report was supplied."); + await expect(page.locator("[data-coverage-summary]")).toHaveCount(0); +}); + +coverageTest("a newly committed coverage view preserves independent handoff exclusion", async ({compactURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + const barrier = Promise.withResolvers(); + const started = Promise.withResolvers(); + let posts = 0; + await page.route("**/api/v1/handoff", async route => { + posts++; + const response = await route.fetch(); + started.resolve(); + await barrier.promise; + await route.fulfill({response}); + }); + try { + await openWorkspace(page, compactURL); + await page.getByRole("button", {name: "Select invariant", exact: true}).first().click(); + const question = page.getByRole("textbox", {name: "Question", exact: true}); + await question.fill("Keep pending question."); + const submit = page.getByRole("button", {name: "Create handoff packet", exact: true}); + await submit.click(); + await started.promise; + await page.getByRole("button", {name: "Coverage", exact: true}).click(); + await expect(page.locator("body")).toHaveAttribute("data-state", "coverage"); + const actions = page.locator("[data-evidence-question]"); + await expect(actions).toHaveCount(2); + expect(await actions.evaluateAll(items => items.every(item => item.disabled))).toBe(true); + await actions.first().dispatchEvent("click"); + await expect(page.locator("#selected-context li")).toHaveCount(0); + await expect(question).toHaveValue("Keep pending question."); + expect(posts).toBe(1); + barrier.resolve(); + await expect(submit).toBeEnabled(); + await expect(actions.first()).toBeEnabled(); + await expect(page.locator("#handoff-packet")).toBeEmpty(); + } finally { barrier.resolve(); } +}); + +test("handoff preview, clipboard and real download preserve the exact response carrier", async ({baseURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + await page.addInitScript(() => { + globalThis.__copiedPackets = []; + Object.defineProperty(navigator, "clipboard", {value: {writeText: async text => { globalThis.__copiedPackets.push(text); }}}); + globalThis.__createdURLs = []; + globalThis.__revokedURLs = []; + const create = URL.createObjectURL.bind(URL), revoke = URL.revokeObjectURL.bind(URL); + URL.createObjectURL = blob => { const url = create(blob); globalThis.__createdURLs.push(url); return url; }; + URL.revokeObjectURL = url => { globalThis.__revokedURLs.push(url); return revoke(url); }; + }); + await openWorkspace(page, baseURL); + await page.getByRole("button", {name: "Select invariant", exact: true}).click(); + await page.getByRole("textbox", {name: "Question", exact: true}).fill("Keep quote \u{1F680} and context separate."); + const response = page.waitForResponse(response => response.url().endsWith("/api/v1/handoff")); + await page.getByRole("button", {name: "Create handoff packet"}).click(); + const raw = await (await response).text(); + await expect(page.locator("#handoff-status")).toHaveText("Handoff packet created."); + expect(await page.locator("#handoff-packet").textContent()).toBe(raw); + expect(raw.endsWith("\n")).toBe(true); + expect(raw.split("\n")).toHaveLength(2); + await page.getByRole("button", {name: "Copy JSON", exact: true}).click(); + await expect(page.locator("#handoff-status")).toHaveText("Exact handoff JSON copied."); + expect(await page.evaluate(() => globalThis.__copiedPackets)).toEqual([raw]); + const downloadable = page.waitForEvent("download"); + await page.getByRole("button", {name: "Download JSON", exact: true}).click(); + const download = await downloadable; + expect(download.suggestedFilename()).toBe("proofkit-question.json"); + const chunks = []; + for await (const chunk of await download.createReadStream()) chunks.push(chunk); + expect(Buffer.concat(chunks).equals(Buffer.from(raw))).toBe(true); + await expect.poll(() => page.evaluate(() => globalThis.__revokedURLs.length)).toBe(1); + expect(await page.evaluate(() => globalThis.__revokedURLs)).toEqual(await page.evaluate(() => globalThis.__createdURLs)); + await page.getByRole("button", {name: "Diff", exact: true}).click(); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + await expect(page.locator("#handoff-packet")).toBeEmpty(); +}); + +test("unavailable export effects preserve a selectable exact JSON fallback", async ({baseURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + await page.addInitScript(() => { + Object.defineProperty(navigator, "clipboard", {value: {writeText: async () => { throw new Error("private clipboard detail"); }}}); + URL.createObjectURL = () => { throw new Error("private download detail"); }; + }); + await openWorkspace(page, baseURL); + await page.getByRole("button", {name: "Select invariant", exact: true}).click(); + const question = page.getByRole("textbox", {name: "Question", exact: true}); + await question.fill("Keep my draft and exact packet."); + const response = page.waitForResponse(response => response.url().endsWith("/api/v1/handoff")); + await page.getByRole("button", {name: "Create handoff packet"}).click(); + const raw = await (await response).text(); + const disclosure = page.locator("#handoff-output details").filter({has: page.locator("#handoff-packet")}); + for (const effect of ["Copy", "Download"]) { + if (await disclosure.getAttribute("open") !== null) await disclosure.locator("summary").click(); + await page.getByRole("button", {name: `${effect} JSON`, exact: true}).click(); + await expect(disclosure).toHaveAttribute("open"); + expect(await page.locator("#handoff-packet").textContent()).toBe(raw); + await expect(page.locator("#handoff-status")).toHaveText(`${effect === "Copy" ? "Clipboard" : effect} unavailable. Exact JSON remains available below.`); + } + await expect(question).toHaveValue("Keep my draft and exact packet."); + await expect(page.locator("body")).not.toContainText("private clipboard detail"); + await expect(page.locator("body")).not.toContainText("private download detail"); +}); + +for (const outcome of ["resolved", "rejected"]) { + test(`a late ${outcome} clipboard effect cannot label a newer view`, async ({baseURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + await page.addInitScript(() => { + Object.defineProperty(navigator, "clipboard", {value: {writeText: () => new Promise((resolve, reject) => { globalThis.__clipboardRelease = {resolve, reject}; })}}); + }); + await openWorkspace(page, baseURL); + await page.getByRole("button", {name: "Select invariant"}).click(); + const question = page.getByRole("textbox", {name: "Question", exact: true}); + await question.fill("Do not erase this draft."); + await page.getByRole("button", {name: "Create handoff packet"}).click(); + await page.getByRole("button", {name: "Copy JSON", exact: true}).click(); + await expect(page.getByRole("button", {name: "Copy JSON", exact: true})).toBeDisabled(); + await page.getByRole("button", {name: "Diff", exact: true}).click(); + await expect(page.locator("body")).toHaveAttribute("data-state", "diff"); + await page.evaluate(async outcome => { + if (outcome === "resolved") globalThis.__clipboardRelease.resolve(); else globalThis.__clipboardRelease.reject(new Error("private clipboard failure")); + await new Promise(resolve => setTimeout(resolve, 0)); + }, outcome); + await expect(page.locator("#handoff-status")).toHaveText("No source-bound text selected."); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + await expect(question).toHaveValue("Do not erase this draft."); + await expect(page.locator("body")).not.toContainText("private clipboard failure"); + }); +} diff --git a/tests/browser/workspace-graph.spec.mjs b/tests/browser/workspace-graph.spec.mjs new file mode 100644 index 0000000..0f5be0c --- /dev/null +++ b/tests/browser/workspace-graph.spec.mjs @@ -0,0 +1,165 @@ +import {expect} from "@playwright/test"; +import {capacityTest, test} from "./workspace-test-harness.mjs"; +import {openWorkspace} from "./workspace-navigation-harness.mjs"; +import {analyzeAxe, assertAxeTestComplete, initializeAxe} from "./axe-harness.mjs"; + +async function openGraph(page, url) { + await openWorkspace(page, url); + const response = page.waitForResponse(response => response.url().endsWith("/api/v1/graph")); + await page.getByRole("button", {name: "Traceability", exact: true}).click(); + const graph = (await (await response).json()).projection; + await expect(page.locator("body")).toHaveAttribute("data-state", "graph"); + return graph; +} + +async function identities(page, kind) { + return page.getByRole("list", {name: `Admitted traceability ${kind}`}).locator(":scope > li").evaluateAll(items => items.map(item => item.dataset.identity)); +} + +test("graph filters retain evidence scope, directed neighborhood and a keyboard record equivalent", async ({baseURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + await initializeAxe(page); + const graph = await openGraph(page, baseURL); + const requirementID = "requirement:REQ-CONSUMER-001"; + const button = page.locator(`.graph-records button[data-graph-select="${requirementID}"]`); + await button.focus(); + await page.keyboard.press("Enter"); + await expect(button).toBeFocused(); + await page.getByRole("checkbox", {name: "Selected node and neighbors", exact: true}).check(); + const retained = new Set([requirementID]); + for (const edge of graph.edges) { + if (edge.fromNodeId === requirementID) retained.add(edge.toNodeId); + if (edge.toNodeId === requirementID) retained.add(edge.fromNodeId); + } + expect(await identities(page, "nodes")).toEqual(graph.nodes.filter(node => retained.has(node.nodeId)).map(node => node.nodeId)); + expect(await identities(page, "edges")).toEqual(graph.edges.filter(edge => retained.has(edge.fromNodeId) && retained.has(edge.toNodeId)).map(edge => edge.edgeId)); + const specifications = page.getByRole("checkbox", {name: "Specifications", exact: true}); + await specifications.focus(); + await page.keyboard.press("Space"); + await expect(specifications).toBeFocused(); + await expect(page.getByRole("checkbox", {name: "Selected node and neighbors", exact: true})).not.toBeChecked(); + await expect(page.getByRole("checkbox", {name: "Selected node and neighbors", exact: true})).toBeDisabled(); + await expect(page.getByRole("region", {name: "Selected graph node"})).toHaveText("No node selected."); + const visible = new Set(graph.nodes.filter(node => node.evidencePlane !== "specification_coverage").map(node => node.nodeId)); + expect(await identities(page, "edges")).toEqual(graph.edges.filter(edge => edge.evidencePlane !== "specification_coverage" && visible.has(edge.fromNodeId) && visible.has(edge.toNodeId)).map(edge => edge.edgeId)); + await expect(page.locator("[data-graph-counts]")).toContainText(`Available: ${graph.availableNodeCount} nodes, ${graph.availableEdgeCount} relations.`); + for (const name of ["Proof declarations", "Code", "Native execution"]) await page.getByRole("checkbox", {name, exact: true}).uncheck(); + expect(await identities(page, "nodes")).toEqual([]); + expect(await identities(page, "edges")).toEqual([]); + await expect(page.locator("[data-graph-counts]")).toContainText("Visible in this returned page: 0 nodes, 0 relations."); + expect((await analyzeAxe(page)).violations).toEqual([]); + assertAxeTestComplete(page); +}); + +test("an outside-page parent follows its canonical offset without synthesizing a relation", async ({baseURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + const requests = []; + await page.route("**/api/v1/graph", async route => { + const body = route.request().postDataJSON(); + requests.push(body); + const query = requests.length === 1 ? {offset: 1, edgeOffset: 80000, maxRecords: 1, maxEdges: 1} : body.query; + await route.fulfill({response: await route.fetch({postData: {...body, query}})}); + }); + const graph = await openGraph(page, baseURL); + expect(graph.nodes.map(node => node.nodeId)).toEqual(["code:code.retry"]); + expect(graph.edges).toEqual([]); + await page.locator('.graph-records button[data-graph-select="code:code.retry"]').click(); + const parent = page.getByRole("button", {name: "parentNodeId: code:code.repository (outside page)", exact: true}); + await expect(parent).toBeVisible(); + expect(requests).toHaveLength(1); + await parent.click(); + await expect(page.getByRole("region", {name: "Selected graph node"})).toContainText("code:code.repository"); + expect(requests).toHaveLength(2); + expect(requests[1].query).toEqual({offset: 0, edgeOffset: 0, maxRecords: 64, maxEdges: 128}); + await expect(page.getByRole("heading", {name: "Traceability graph", exact: true})).toBeFocused(); +}); + +test("included structural targets hidden by filters are revealed locally without a fetch", async ({baseURL, page}) => { + await page.setViewportSize({width: 1920, height: 1080}); + let requests = 0; + page.on("request", request => { if (request.url().endsWith("/api/v1/graph")) requests++; }); + const graph = await openGraph(page, baseURL); + const execution = graph.nodes.find(node => node.evidencePlane === "native_execution_coverage"); + await page.locator(`.graph-records button[data-graph-select="${execution.nodeId}"]`).click(); + await page.getByRole("checkbox", {name: "Code", exact: true}).uncheck(); + const details = page.locator(".graph-inspector li details").first(); + await details.locator("summary").click(); + const link = details.getByRole("button", {name: "codeNodeId: code:code.retry (hidden by filters)", exact: true}); + await link.focus(); + await page.keyboard.press("Enter"); + await expect(page.getByRole("region", {name: "Selected graph node"})).toContainText("code:code.retry"); + await expect(page.getByRole("checkbox", {name: "Code", exact: true})).toBeChecked(); + await expect(page.locator('.graph-records button[data-graph-select="code:code.retry"]')).toBeFocused(); + expect(requests).toBe(1); +}); + +capacityTest("maximum admitted graph page remains bounded, inspectable and below the commit budget", async ({graphCapacityURL, page}, testInfo) => { + await page.setViewportSize({width: 1920, height: 1080}); + const samples = []; + await page.route("**/api/v1/graph", async route => { + const body = route.request().postDataJSON(); + await route.fulfill({response: await route.fetch({postData: {...body, query: {offset: 130, edgeOffset: 64, maxRecords: 64, maxEdges: 128}}})}); + }); + const graph = await openGraph(page, graphCapacityURL); + expect(graph.primaryNodeCount).toBe(64); + expect(graph.boundaryNodeCount).toBe(128); + expect(graph.nodes).toHaveLength(192); + expect(graph.edges).toHaveLength(128); + const buttons = page.locator(".graph-canvas > button"); + await expect(buttons).toHaveCount(192); + expect(await identities(page, "nodes")).toEqual(graph.nodes.map(node => node.nodeId)); + expect(await identities(page, "edges")).toEqual(graph.edges.map(edge => edge.edgeId)); + const viewport = page.getByRole("region", {name: "Traceability graph viewport"}); + samples.push(Number(await viewport.getAttribute("data-commit-milliseconds"))); + for (const index of [0, 63, 128, 191]) { + await page.locator(`.graph-records button[data-graph-select="${graph.nodes[index].nodeId}"]`).click(); + await expect(page.locator(".graph-inspector > dl dt")).toHaveText(Object.keys(graph.nodes[index])); + samples.push(Number(await viewport.getAttribute("data-commit-milliseconds"))); + } + expect(samples.every(value => Number.isFinite(value) && value > 0 && value <= 100)).toBe(true); + await testInfo.attach("graph-page-commit-distribution.json", {body: JSON.stringify({nodes: 192, edges: 128, milliseconds: samples}), contentType: "application/json"}); +}); + +capacityTest("Go-built unverified coordinates retain exact HTTP and DOM values or fail closed", async ({graphNumericURL, page}) => { + await openWorkspace(page, graphNumericURL); + const response = page.waitForResponse(response => response.url().endsWith("/api/v1/graph")); + await page.getByRole("button", {name: "Traceability", exact: true}).click(); + const body = await (await response).text(); + const wire = JSON.parse(body, (key, value, context) => key === "byteStart" || key === "byteEnd" ? context.source : value); + const range = wire.projection.nodes.find(node => node.nodeId === "code:code.retry"); + expect([range.byteStart, range.byteEnd]).toEqual(["9007199254740992", "9007199254740993"]); + await page.locator('.graph-records button[data-graph-select="code:code.retry"]').click(); + const inspector = page.getByRole("region", {name: "Selected graph node"}); + await expect(inspector.locator('dt:has-text("byteStart") + dd')).toHaveText("9007199254740992"); + await expect(inspector.locator('dt:has-text("byteEnd") + dd')).toHaveText("9007199254740993"); + await expect(inspector.locator('dt:has-text("rangeVerification") + dd')).toHaveText("unverified"); + await expect(inspector.locator('dt:has-text("currentnessState") + dd')).toHaveText("unverified"); + + await page.evaluate(() => Reflect.set(JSON, "rawJSON", undefined)); + await page.getByRole("button", {name: "Specifications", exact: true}).click(); + await expect(page.locator("body")).toHaveAttribute("data-state", "specifications"); + await page.getByRole("button", {name: "Traceability", exact: true}).click(); + await expect(page.getByText("The admitted workspace is unavailable.", {exact: true})).toBeVisible(); + await expect(page.locator(".graph-inspector")).toHaveCount(0); +}); + +test("native numeric observation preserves fractional tokens, strings and control values", async ({baseURL, page}) => { + const body = '{"start":9007199254740992,"end":9007199254740993,"safe":9007199254740991,"zero":0,"string":"9007199254740993","nested":[1.0000000000000001,1e-400,-0,1e400,-9007199254740993,0.123456789012345678901],"unbranded":{"rawJSON":"17"}}'; + await page.route("**/numeric-observation-fixture", route => route.fulfill({status: 200, contentType: "application/json", body})); + await openWorkspace(page, baseURL); + const observed = await page.evaluate(async () => { + const {fetchWorkspaceResponse} = await import("/assets/workspace-requests.js"); + const {workspaceScalarText} = await import("/assets/workspace-json.js"); + const {text, value} = await fetchWorkspaceResponse("/numeric-observation-fixture", {}); + return { + text, serialized: JSON.stringify(value), start: workspaceScalarText(value.start), end: workspaceScalarText(value.end), + safe: value.safe, zero: value.zero, stringType: typeof value.string, string: value.string, + unbranded: workspaceScalarText(value.unbranded), frozen: Object.isFrozen(value.end), + }; + }); + expect(observed).toEqual({ + text: body, serialized: body, start: "9007199254740992", end: "9007199254740993", + safe: 9007199254740991, zero: 0, stringType: "string", string: "9007199254740993", + unbranded: "[object Object]", frozen: true, + }); +}); diff --git a/tests/browser/workspace-locking.spec.mjs b/tests/browser/workspace-locking.spec.mjs index 9bd1f94..ed834b5 100644 --- a/tests/browser/workspace-locking.spec.mjs +++ b/tests/browser/workspace-locking.spec.mjs @@ -29,14 +29,11 @@ for (const outcome of [200, 400]) { expect(await handoff.count()).toBe(1); handoff.release(); + await handoff.settled(); const packet = page.locator("#handoff-packet"); - if (outcome === 200) { - await expect(page.locator("#handoff-status")).toHaveText("Handoff packet created."); - expect(JSON.parse(await packet.textContent()).annotations.map(item => item.question)).toEqual(["First pending question."]); - } else { - await expect(page.locator("#handoff-status")).toHaveText("The handoff packet could not be created."); - await expect(packet).toBeEmpty(); - } + await expect(packet).toBeEmpty(); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + await expect(page.locator("#handoff-status")).toHaveText("1 source-bound target(s) selected."); await expect(question).toHaveValue("Second intentional question."); await expect(submit).toBeEnabled(); await submit.click(); @@ -66,7 +63,12 @@ for (const status of [403, 409]) { const message = status === 403 ? "Access to this workspace was denied." : "The workspace snapshot has changed."; await expect(page.locator("#workspace-content [role=alert]")).toHaveText(message); }; - const expectHandoff = () => expect(page.locator("#handoff-status")).toHaveText("Handoff packet created."); + const expectHandoff = async () => { + await handoff.settled(); + await expect(page.locator("#handoff-packet")).toBeEmpty(); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + await expect(page.locator("#handoff-status")).toHaveText("No source-bound text selected."); + }; if (first === "handoff") { handoff.release(); await expectHandoff(); @@ -93,30 +95,67 @@ for (const status of [403, 409]) { } } +for (const status of [403, 409]) { + for (const refresh of [false, true]) { + test(`handoff ${status} locks requests in the ${refresh ? "new" : "submitting"} view`, async ({baseURL, page}) => { + const handoff = await holdFirstHandoff(page, status); + try { + await startPendingHandoff(page, baseURL, handoff.started); + if (refresh) { + await page.getByRole("button", {name: "Specifications", exact: true}).click(); + await expect(page.locator("#workspace-content")).toHaveAttribute("aria-busy", "false"); + } + handoff.release(); + await handoff.settled(); + const submit = page.getByRole("button", {name: "Create handoff packet", exact: true}); + await expect(submit).toBeDisabled(); + expect(await page.locator("[data-protected-request]").evaluateAll(items => items.every(item => item.disabled))).toBe(true); + await expect(page.locator("body")).toHaveAttribute("data-state", refresh ? "specifications" : "handoff-failed"); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + await expect(page.locator("#handoff-packet")).toBeEmpty(); + await expect(page.getByRole("textbox", {name: "Question", exact: true})).toHaveValue("First pending question."); + await expect(page.getByRole("button", {name: "Reload workspace", exact: true})).toHaveCount(status === 409 ? 1 : 0); + await submit.dispatchEvent("click"); + expect(await handoff.count()).toBe(1); + await expect(page.locator("body")).not.toContainText("private handoff detail"); + } finally { handoff.release(); } + }); + } +} + async function holdFirstHandoff(page, outcome) { const barrier = Promise.withResolvers(); const started = Promise.withResolvers(); await page.addInitScript(() => { const nativeFetch = globalThis.fetch.bind(globalThis); globalThis.__handoffFetchCount = 0; - globalThis.fetch = (input, init) => { + globalThis.__handoffSettled = 0; + globalThis.fetch = async (input, init) => { const url = new URL(typeof input === "string" ? input : input.url, location.href); - if (url.pathname === "/api/v1/handoff") globalThis.__handoffFetchCount += 1; - return nativeFetch(input, init); + if (url.pathname !== "/api/v1/handoff") return nativeFetch(input, init); + globalThis.__handoffFetchCount += 1; + const response = await nativeFetch(input, init); + const settled = () => setTimeout(() => { globalThis.__handoffSettled++; }, 0); + if (!response.ok) settled(); + else { + const read = response.text.bind(response); + response.text = async () => { const text = await read(); settled(); return text; }; + } + return response; }; }); let count = 0; await page.route("**/api/v1/handoff", async route => { count += 1; if (count !== 1) return route.continue(); - const response = outcome === 200 ? await route.fetch() : - await route.fetch({postData: {...route.request().postDataJSON(), annotations: []}}); - expect(response.status()).toBe(outcome); + const response = outcome === 200 ? await route.fetch() : outcome === 400 ? + await route.fetch({postData: {...route.request().postDataJSON(), annotations: []}}) : null; + if (response) expect(response.status()).toBe(outcome); started.resolve(); await barrier.promise; - return route.fulfill({response}); + return response ? route.fulfill({response}) : route.fulfill({status: outcome, body: "private handoff detail"}); }); - return {release: barrier.resolve, started: started.promise, count: () => page.evaluate(() => globalThis.__handoffFetchCount)}; + return {release: barrier.resolve, started: started.promise, count: () => page.evaluate(() => globalThis.__handoffFetchCount), settled: () => page.waitForFunction(() => globalThis.__handoffSettled >= 1)}; } async function startPendingHandoff(page, url, started) { @@ -189,7 +228,7 @@ async function assertLockedContentCommit(page, url, view, status) { await expect(page.locator("#workspace-content article > p").first()).toHaveText("/requirements/REQ-CONSUMER-001/riskClass"); } else { await expect(page.getByRole("button", {name: "Previous graph relation page", exact: true})).toBeVisible(); - await expect(page.locator('table[data-identity-kind="edge"] tbody tr')).toHaveCount(1); + await expect(page.getByRole("list", {name: "Admitted traceability edges"}).locator(":scope > li")).toHaveCount(1); } const controls = page.locator("[data-protected-request]"); expect(await controls.evaluateAll(elements => elements.filter(element => !element.disabled).map(element => element.textContent))).toEqual([]); diff --git a/tests/browser/workspace-paging.spec.mjs b/tests/browser/workspace-paging.spec.mjs index 5a75378..38639d4 100644 --- a/tests/browser/workspace-paging.spec.mjs +++ b/tests/browser/workspace-paging.spec.mjs @@ -37,20 +37,25 @@ for (const view of ["diff", "graph"]) { body: { requestId: expect.stringMatching(new RegExp(`^browser\\.${view}\\.`)), snapshotId: expect.stringMatching(/^sha256:[0-9a-f]{64}$/), - query: view === "diff" ? {offset: 1, maxRecords: 512} : {offset: 1, edgeOffset: 1, maxRecords: 256, maxEdges: 2048}, + query: view === "diff" ? {offset: 1, maxRecords: 512} : {offset: 1, edgeOffset: 1, maxRecords: 64, maxEdges: 128}, }, }); } expect(failedAttempts[1].body.snapshotId).toBe(failedAttempts[0].body.snapshotId); expect(failedAttempts[1].body.requestId).not.toBe(failedAttempts[0].body.requestId); if (view === "diff") { + await expect(page.locator("[data-diff-summary]")).toHaveText("Changes: 1; requirements: 1; risk changes: 1; lifecycle changes: 0."); + await expect(page.getByRole("list", {name: "Change classes on this page"})).toHaveText("scalar_changed: 1"); await expect(page.locator("#workspace-content article > p").first()).toHaveText("/requirements/REQ-CONSUMER-001/riskClass"); - await expect(page.locator("#workspace-content article > pre")).toHaveText('"high"\n->\n"medium"'); + await page.getByText("Before and after", {exact: true}).click(); + await expect(page.locator("#workspace-content article pre")).toHaveText('"high"\n->\n"medium"'); } else { - await expect(page.locator('table[data-identity-kind="node"] tbody tr')).toHaveCount(2); - expect(await page.locator('table[data-identity-kind="node"] tbody tr').evaluateAll(rows => rows.map(row => row.dataset.identity))).toEqual(["code:code.repository", "code:code.retry"]); - await expect(page.locator('table[data-identity-kind="edge"] tbody tr')).toHaveCount(1); - await expect(page.locator('table[data-identity-kind="edge"] tbody td').nth(1)).toHaveText("contains"); + const nodes = page.getByRole("list", {name: "Admitted traceability nodes"}).locator(":scope > li"); + await expect(nodes).toHaveCount(2); + expect(await nodes.evaluateAll(rows => rows.map(row => row.dataset.identity))).toEqual(["code:code.repository", "code:code.retry"]); + const edges = page.getByRole("list", {name: "Admitted traceability edges"}).locator(":scope > li"); + await expect(edges).toHaveCount(1); + await expect(edges.locator("summary")).toHaveText("contains: code:code.repository -> code:code.retry"); } }); } diff --git a/tests/browser/workspace-test-harness.mjs b/tests/browser/workspace-test-harness.mjs index 7b6b4af..7a9d057 100644 --- a/tests/browser/workspace-test-harness.mjs +++ b/tests/browser/workspace-test-harness.mjs @@ -28,6 +28,14 @@ export const pagingTest = test.extend({ export const capacityTest = test.extend({ capacityURL: [async ({}, use) => { await withFixture("--capacity", use); }, {scope: "worker"}], + graphCapacityURL: [async ({}, use) => { await withFixture("--graph-capacity", use); }, {scope: "worker"}], + graphNumericURL: [async ({}, use) => { await withFixture("--graph-numeric", use); }, {scope: "worker"}], +}); + +export const coverageTest = test.extend({ + compactURL: [async ({}, use) => { await withFixture("--coverage-compact", use); }, {scope: "worker"}], + structuredURL: [async ({}, use) => { await withFixture("--coverage-structured", use); }, {scope: "worker"}], + emptyCoverageURL: [async ({}, use) => { await withFixture("--coverage-empty", use); }, {scope: "worker"}], }); async function withFixture(selector, use) { diff --git a/tests/browser/workspace.spec.mjs b/tests/browser/workspace.spec.mjs index 7e66f0d..9bb26f5 100644 --- a/tests/browser/workspace.spec.mjs +++ b/tests/browser/workspace.spec.mjs @@ -35,15 +35,6 @@ async function expectCSS(locator, properties) { expect(completed).toEqual(plan); } -async function expectAllCSS(locator, properties) { - const propertyNames = Object.keys(properties); - const actual = await locator.evaluateAll((elements, names) => elements.map((element) => { - const computed = window.getComputedStyle(element); - return Object.fromEntries(names.map((name) => [name, computed.getPropertyValue(name)])); - }), propertyNames); - expect(actual).toEqual(actual.map(() => properties)); -} - function assertAssertionPlanFalsifiers() { const first = Object.freeze({property: "opacity", value: "1"}); const second = Object.freeze({property: "filter", value: "none"}); @@ -56,64 +47,6 @@ function assertAssertionPlanFalsifiers() { ]) expect(mutant).not.toEqual(plan); } -async function expectVisibleTable(table, caption, headers, rows) { - const viewport = table.locator(".."); - await expect(table).toBeVisible(); - const commonStyles = { - opacity: "1", - filter: "none", - "clip-path": "none", - "mask-image": "none", - "content-visibility": "visible", - zoom: "1", - "animation-name": "none", - "transition-duration": "0s", - "transition-delay": "0s", - }; - for (const element of [ - viewport, - table, - table.locator(":scope > thead"), - table.locator(":scope > thead > tr"), - table.locator(":scope > tbody"), - ]) { - await expect(element).toBeVisible(); - await expectCSS(element, commonStyles); - } - const captionLocator = table.locator(":scope > caption"); - await expect(captionLocator).toHaveText(caption); - const headerCells = table.locator(":scope > thead > tr > th"); - await expect(headerCells).toHaveText(headers); - const bodyRows = table.locator(":scope > tbody > tr"); - await expect(bodyRows).toHaveCount(rows.length); - await expect(table.locator(":scope > tbody > tr:visible")).toHaveCount(rows.length); - for (let rowIndex = 0; rowIndex < rows.length; rowIndex += 1) { - const row = bodyRows.nth(rowIndex); - await expect(row).toBeVisible(); - await expect(row.locator(":scope > td")).toHaveText(rows[rowIndex]); - } - await expectAllCSS(bodyRows, commonStyles); - const textElements = table.locator("caption, th, td"); - const textCount = 1 + headers.length + rows.reduce((count, row) => count + row.length, 0); - await expect(textElements).toHaveCount(textCount); - await expect(table.locator("caption:visible, th:visible, td:visible")).toHaveCount(textCount); - await expectAllCSS(textElements, { - opacity: "1", - color: "rgb(32, 37, 34)", - "font-size": "16px", - "font-size-adjust": "none", - "-webkit-text-security": "none", - "text-transform": "none", - filter: "none", - "clip-path": "none", - "mask-image": "none", - "content-visibility": "visible", - zoom: "1", - "animation-name": "none", - "transition-duration": "0s", - "transition-delay": "0s", - }); -} const axeTest = test.extend({ axePage: async ({page}, use) => { @@ -323,7 +256,7 @@ for (const row of workspaceStateMatrix) { const packetRegion = page.getByRole("region", {name: "Handoff packet"}); await expect(packetRegion).toBeVisible(); if (row.packetState === "result") { - await expect(packetRegion.locator("pre")).toContainText('"state": "submitted"'); + expect(JSON.parse(await packetRegion.locator("pre").textContent()).state).toBe("submitted"); } else { await expect(packetRegion.locator("pre")).toBeEmpty(); } @@ -563,7 +496,7 @@ test("handoff packet output never creates a zero-value keyboard stop", async ({b await page.getByRole("textbox", {name: "Question"}).fill("Is the handoff output still readable?"); await page.getByRole("button", {name: "Create handoff packet"}).click(); await expect(page.locator("body")).toHaveAttribute("data-state", "handoff-result"); - await expect(packet).toContainText('"state": "submitted"'); + await expect(packet).toHaveText('{"state":"submitted"}'); await expectNotFocusable(); handoffFails = true; @@ -602,6 +535,7 @@ test("workspace renders admitted views and creates a keyboard-authorized handoff const selectInvariant = page.getByRole("button", {name: "Select invariant"}); const specificationsView = page.getByRole("button", {name: "Specifications"}); const diffView = page.getByRole("button", {name: "Diff"}); + const coverageView = page.getByRole("button", {name: "Coverage", exact: true}); await expect(specificationsView).toHaveAttribute("aria-current", "page"); await specificationsView.focus(); await page.keyboard.press("Tab"); @@ -613,16 +547,16 @@ test("workspace renders admitted views and creates a keyboard-authorized handoff await expect(authoritySummary).toBeFocused(); await specificationsView.focus(); await page.keyboard.press("Alt+Tab"); - await expect(diffView).toBeFocused(); + await expect(coverageView).toBeFocused(); await page.keyboard.press("Alt+Shift+Tab"); await expect(specificationsView).toBeFocused(); } else { - await expect(diffView).toBeFocused(); + await expect(coverageView).toBeFocused(); await page.keyboard.press("Shift+Tab"); await expect(specificationsView).toBeFocused(); } } else { - await expect(diffView).toBeFocused(); + await expect(coverageView).toBeFocused(); await page.keyboard.press("Shift+Tab"); await expect(specificationsView).toBeFocused(); } @@ -638,13 +572,14 @@ test("workspace renders admitted views and creates a keyboard-authorized handoff await page.getByRole("button", {name: "Create handoff packet"}).click(); await expect(page.getByRole("status")).toContainText("Handoff packet created"); const packetRegion = page.getByRole("region", {name: "Handoff packet"}); - await expect(packetRegion).toContainText('"state": "submitted"'); + await expect(packetRegion).toContainText('"state":"submitted"'); await expect(packetRegion).toContainText("retry \u{1F680}"); await page.getByRole("button", {name: "Diff"}).click(); await expect(diffView).toHaveAttribute("aria-current", "page"); await expect(specificationsView).not.toHaveAttribute("aria-current", "page"); await expect(page.getByRole("heading", {name: /scalar_changed/})).toBeVisible(); + await page.getByText("Before and after", {exact: true}).click(); await expect(page.getByText(/Source digests: sha256:/)).toBeVisible(); const diffBoundary = page.locator(".projection-boundary"); await expect(diffBoundary).toContainText("lookup_fragment_only"); @@ -719,214 +654,57 @@ test("workspace renders admitted views and creates a keyboard-authorized handoff const edges = projection.edges; const nodeIDs = nodes.map((node) => node.nodeId); const edgeIDs = edges.map((edge) => edge.edgeId); - const graph = page.getByRole("img", {name: /traceability nodes and edges/}); + const graph = page.locator(".graph-canvas > svg"); const graphViewport = page.getByRole("region", {name: "Traceability graph viewport"}); await expect(graphViewport).toBeVisible(); - await expect(graph).toBeVisible(); + await expect(graph).toHaveAttribute("aria-hidden", "true"); await expect(graph).toHaveAttribute("data-node-ids", nodeIDs.join(" ")); await expect(graph).toHaveAttribute("data-edge-ids", edgeIDs.join(" ")); - const expectedHeight = Math.max(180, Math.ceil(nodes.length / 2) * 76 + 40); - await expect(graph).toHaveAttribute("viewBox", `0 0 800 ${expectedHeight}`); - await expectCSS(graphViewport, { - display: "block", - visibility: "visible", - opacity: "1", - "overflow-x": "auto", - "overflow-y": "auto", - transform: "none", - translate: "none", - rotate: "none", - scale: "none", - "offset-path": "none", - zoom: "1", - "content-visibility": "visible", - filter: "none", - "clip-path": "none", - "mask-image": "none", - "animation-name": "none", - "transition-duration": "0s", - "transition-delay": "0s", - }); - await expectCSS(graph, { - display: "block", - visibility: "visible", - opacity: "1", - "min-width": "800px", - height: /^(?:1[89]\d|[2-9]\d{2,})(?:\.\d+)?px$/, - transform: "none", - translate: "none", - rotate: "none", - scale: "none", - "offset-path": "none", - zoom: "1", - "content-visibility": "visible", - filter: "none", - "clip-path": "none", - "mask-image": "none", - "animation-name": "none", - "transition-duration": "0s", - "transition-delay": "0s", - }); - for (const ancestor of [ - page.locator("html"), - page.locator("body"), - page.locator("body > main"), - page.locator("#workspace-content"), - ]) { - await expectCSS(ancestor, { - "animation-name": "none", - "transition-duration": "0s", - "transition-delay": "0s", - }); + const buttons = page.locator(".graph-canvas > button[data-graph-select]"); + await expect(buttons).toHaveCount(nodes.length); + const primaryIDs = new Set(projection.primaryNodeIds); + const nativeFields = page.locator(".graph-inspector > dl"); + for (let index = 0; index < nodes.length; index++) { + const node = nodes[index]; + const button = buttons.nth(index); + await expect(button).toHaveAttribute("data-graph-select", node.nodeId); + await expect(button).toHaveAttribute("data-plane", node.evidencePlane); + await expect(button).toHaveAttribute("data-boundary", String(!primaryIDs.has(node.nodeId))); + await expect(button.locator(".graph-node-label")).toHaveText(node.label); + await expect(button.locator(".graph-node-identity")).toHaveText(node.nodeId); + await expect(button).toHaveAttribute("title", `${node.label}: ${node.nodeId}`); + await button.focus(); + await page.keyboard.press("Enter"); + await expect(page.locator(`.graph-canvas > button[data-graph-select="${node.nodeId}"]`)).toBeFocused(); + await expect(nativeFields.locator("dt")).toHaveText(Object.keys(node)); + await expect(nativeFields.locator("dd")).toHaveText(Object.values(node).map(value => Array.isArray(value) ? value.join(", ") : String(value))); + await expectCSS(nativeFields, {visibility: "visible", opacity: "1", filter: "none", "clip-path": "none", "content-visibility": "visible"}); } - await expect(page.locator("animate, animateColor, animateMotion, animateTransform, discard, set")).toHaveCount(0); - const positions = new Map(nodes.map((node, index) => [ - node.nodeId, - {x: 28 + (index % 2) * 390, y: 28 + Math.floor(index / 2) * 76}, - ])); - const rootChildren = graph.locator(":scope > *"); - await expect(rootChildren).toHaveCount(edges.length + nodes.length); - for (let index = 0; index < edges.length; index += 1) { + const nodeRecords = page.getByRole("list", {name: "Admitted traceability nodes"}).locator(":scope > li"); + const edgeRecords = page.getByRole("list", {name: "Admitted traceability edges"}).locator(":scope > li"); + await expectIdentityOrder(nodeRecords, nodeIDs); + await expectIdentityOrder(edgeRecords, edgeIDs); + for (let index = 0; index < edges.length; index++) { const edge = edges[index]; - const from = positions.get(edge.fromNodeId); - const to = positions.get(edge.toNodeId); - expect(from).toBeDefined(); - expect(to).toBeDefined(); - const line = graph.locator(`:scope > line:nth-child(${index + 1})`); + const details = edgeRecords.nth(index).locator("details"); + await details.locator("summary").click(); + await expect(details.locator("dt")).toHaveText(Object.keys(edge)); + await expect(details.locator("dd")).toHaveText(Object.values(edge).map(value => Array.isArray(value) ? value.join(", ") : String(value))); + const line = graph.locator(":scope > line").nth(index); await expect(line).toHaveAttribute("data-edge-id", edge.edgeId); - const coordinates = { - x1: String(from.x + 180), - y1: String(from.y + 24), - x2: String(to.x + 180), - y2: String(to.y + 24), - }; - expect(coordinates.x1 !== coordinates.x2 || coordinates.y1 !== coordinates.y2).toBe(true); - for (const [name, value] of Object.entries(coordinates)) { - await expect(line).toHaveAttribute(name, value); - } - await expect(line.locator(":scope > *")).toHaveCount(0); - await expectCSS(line, { - display: /^(?:inline|block)$/, - visibility: "visible", - opacity: "1", - stroke: "rgb(32, 37, 34)", - "stroke-opacity": "1", - "stroke-width": "1.5px", - "stroke-dasharray": "none", - transform: "none", - translate: "none", - rotate: "none", - scale: "none", - "offset-path": "none", - zoom: "1", - "content-visibility": "visible", - filter: "none", - "clip-path": "none", - "mask-image": "none", - "animation-name": "none", - "transition-duration": "0s", - "transition-delay": "0s", - }); + await expect(line).toHaveAttribute("marker-end", "url(#graph-arrow)"); + const geometry = await line.evaluate(element => ["x1", "y1", "x2", "y2"].map(name => Number(element.getAttribute(name)))); + expect(geometry.every(Number.isFinite)).toBe(true); + expect(geometry[0] !== geometry[2] || geometry[1] !== geometry[3]).toBe(true); + await expectCSS(line, {visibility: "visible", opacity: "1", stroke: "rgb(32, 37, 34)", "stroke-width": "1.5px", filter: "none", "clip-path": "none"}); } - for (let index = 0; index < nodes.length; index += 1) { - const node = nodes[index]; - const position = positions.get(node.nodeId); - const group = graph.locator(`:scope > g:nth-child(${edges.length + index + 1})`); - await expect(group).toHaveAttribute("data-node-id", node.nodeId); - await expect(group.locator(":scope > *")).toHaveCount(3); - const title = group.locator(":scope > title:nth-child(1)"); - const rect = group.locator(":scope > rect:nth-child(2)"); - const text = group.locator(":scope > text:nth-child(3)"); - const fullLabel = `${node.evidencePlane}: ${node.label}`; - const visibleLabel = [...fullLabel].length > 48 ? `${[...fullLabel].slice(0, 47).join("")}...` : fullLabel; - await expect(title).toHaveText(fullLabel); - await expect(text).toHaveText(visibleLabel); - await expect(title.locator(":scope > *")).toHaveCount(0); - await expect(text.locator(":scope > *")).toHaveCount(0); - for (const [name, value] of Object.entries({ - x: String(position.x), - y: String(position.y), - width: "350", - height: "48", - rx: "4", - })) await expect(rect).toHaveAttribute(name, value); - await expect(rect.locator(":scope > *")).toHaveCount(0); - await expect(text).toHaveAttribute("x", String(position.x + 10)); - await expect(text).toHaveAttribute("y", String(position.y + 29)); - for (const name of ["dx", "dy", "textLength", "lengthAdjust", "rotate"]) { - await expect(text).not.toHaveAttribute(name, /(?:)/); - } - await expectCSS(rect, { - display: /^(?:inline|block)$/, - visibility: "visible", - opacity: "1", - fill: "rgb(245, 246, 245)", - "fill-opacity": "1", - stroke: "rgb(119, 134, 125)", - "stroke-opacity": "1", - x: `${position.x}px`, - y: `${position.y}px`, - width: "350px", - height: "48px", - rx: "4px", - ry: "auto", - }); - await expectCSS(text, { - display: /^(?:inline|block)$/, - visibility: "visible", - opacity: "1", - fill: "rgb(32, 37, 34)", - "fill-opacity": "1", - "font-size": "13px", - "font-size-adjust": "none", - "text-anchor": "start", - direction: "ltr", - "writing-mode": "horizontal-tb", - "dominant-baseline": "auto", - "letter-spacing": "normal", - "word-spacing": "0px", - "text-transform": "none", - "-webkit-text-security": "none", - }); - for (const element of [group, rect, text]) { - await expectCSS(element, { - display: /^(?:inline|block)$/, - visibility: "visible", - opacity: "1", - transform: "none", - translate: "none", - rotate: "none", - scale: "none", - "offset-path": "none", - zoom: "1", - "content-visibility": "visible", - filter: "none", - "clip-path": "none", - "mask-image": "none", - "animation-name": "none", - "transition-duration": "0s", - "transition-delay": "0s", - }); - } + const boxes = await buttons.evaluateAll(elements => elements.map(element => ({x: element.offsetLeft, y: element.offsetTop, width: element.offsetWidth, height: element.offsetHeight}))); + for (let i = 0; i < boxes.length; i++) for (let j = i + 1; j < boxes.length; j++) { + const a = boxes[i], b = boxes[j]; + expect(a.x + a.width <= b.x || b.x + b.width <= a.x || a.y + a.height <= b.y || b.y + b.height <= a.y).toBe(true); } - const nodeRows = nodes.map((node) => [ - node.nodeId, node.kind, node.evidencePlane, node.sourceId, node.authorityClass, - node.currentnessState, node.rangeVerification, node.state, node.producerId, - ].map((value) => value ?? "")); - const edgeRows = edges.map((edge) => [ - edge.edgeId, edge.edgeKind, edge.fromNodeId, edge.toNodeId, - edge.authorityClass, edge.currentnessState, - Array.isArray(edge.evidenceRefs) ? edge.evidenceRefs.join(", ") : (edge.evidenceRefs ?? ""), - ].map((value) => value ?? "")); - const nodeTable = page.locator('table[data-identity-kind="node"]'); - const edgeTable = page.locator('table[data-identity-kind="edge"]'); - await expectVisibleTable(nodeTable, "Admitted traceability nodes", - ["Node", "Kind", "Evidence plane", "Source", "Authority", "Currentness", "Verification", "State", "Producer"], nodeRows); - await expectVisibleTable(edgeTable, "Admitted traceability edges", - ["Edge", "Kind", "From", "To", "Authority", "Currentness", "Evidence"], edgeRows); - await expectIdentityOrder(nodeTable.locator("tbody tr"), nodeIDs); - await expectIdentityOrder(edgeTable.locator("tbody tr"), edgeIDs); - await expect(graph.locator(`:scope > g:nth-child(${edges.length + 1}) > title`)).toContainText(sentinel); + await expect(buttons.first()).toContainText(sentinel); + await expect(page.locator("animate, animateColor, animateMotion, animateTransform")).toHaveCount(0); } finally { const stateBeforeCleanup = graphAttemptState; graphAttemptState = "closing"; @@ -949,24 +727,30 @@ test("workspace renders admitted views and creates a keyboard-authorized handoff expect(graphResponses).toHaveLength(1); expect(graphAttemptState).toBe("detached"); } - const repositoryRow = page.locator('table[data-identity-kind="node"] tbody tr[data-identity="code:code.repository"]'); - await expect(repositoryRow).toContainText("stale"); - const rangeRow = page.locator('table[data-identity-kind="node"] tbody tr[data-identity="code:code.retry"]'); - await expect(rangeRow).toContainText("source_range"); - await expect(rangeRow).toContainText("verified"); - const candidateRow = page.locator('table[data-identity-kind="node"] tbody tr').filter({hasText: "browser.fixture.candidate-runner"}); - await expect(candidateRow).toContainText("caller_reported"); - await expect(candidateRow).toContainText("unverified"); - await expect(candidateRow).toContainText("failed"); - const executionRow = page.locator('table[data-identity-kind="node"] tbody tr').filter({hasText: "browser.fixture.runner"}); - await expect(executionRow).toContainText("receipt_admitted"); - await expect(executionRow).toContainText("current"); - await expect(executionRow).toContainText("passed"); - const traceEdgeRow = page.locator('table[data-identity-kind="edge"] tbody tr').filter({hasText: "browser.fixture.trace"}); + const inspector = page.getByRole("region", {name: "Selected graph node"}); + const selectNode = async id => { await page.locator(`.graph-records button[data-graph-select="${id}"]`).click(); }; + await selectNode("code:code.repository"); + await expect(inspector).toContainText("stale"); + await selectNode("code:code.retry"); + await expect(inspector).toContainText("source_range"); + await expect(inspector).toContainText("verified"); + const nodes = graphResponses[0].body.projection.nodes; + await selectNode(nodes.find(node => node.producerId === "browser.fixture.candidate-runner").nodeId); + await expect(inspector).toContainText("caller_reported"); + await expect(inspector).toContainText("unverified"); + await expect(inspector).toContainText("failed"); + await selectNode(nodes.find(node => node.producerId === "browser.fixture.runner").nodeId); + await expect(inspector).toContainText("receipt_admitted"); + await expect(inspector).toContainText("current"); + await expect(inspector).toContainText("passed"); + const traceEdge = graphResponses[0].body.projection.edges.find(edge => edge.evidenceRefs?.includes("browser.fixture.trace")); + expect(traceEdge).toBeDefined(); + const traceEdgeRow = page.getByRole("list", {name: "Admitted traceability edges"}).locator(`:scope > li[data-identity="${traceEdge.edgeId}"]`); + if (!(await traceEdgeRow.locator("details").evaluate(element => element.open))) await traceEdgeRow.locator("summary").click(); await expect(traceEdgeRow).toContainText("owner_admitted"); await expect(traceEdgeRow).toContainText("current"); await expect(page.locator(".projection-boundary")).toContainText("does not infer code topology"); - await expect(page.getByRole("img", {name: /traceability nodes and edges/}).locator("title").filter({hasText: /deliberately long traceability label/})).toHaveCount(1); + await expect(page.locator(".graph-canvas > button").filter({hasText: /deliberately long traceability label/})).toHaveCount(1); expect(consoleErrors).toEqual([]); }); @@ -1148,11 +932,13 @@ for (const handoffOutcome of [ await expect(page.locator("body")).toHaveAttribute("data-state", "diff"); await expect(page.getByRole("button", {name: "Diff"})).toHaveAttribute("aria-current", "page"); + await expect(page.getByRole("button", {name: "Create handoff packet"})).toBeDisabled(); releaseHandoff(); - await expect(page.getByText(handoffOutcome.expectedStatus, {exact: true})).toBeVisible(); - if (handoffOutcome.name === "successful") { - await expect(page.getByRole("region", {name: "Handoff packet"}).locator("pre")).toContainText('"state": "submitted"'); - } + await expect(page.getByRole("button", {name: "Create handoff packet"})).toBeEnabled(); + await expect(page.getByText(handoffOutcome.expectedStatus, {exact: true})).toHaveCount(0); + await expect(page.locator("#handoff-packet")).toBeEmpty(); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + await expect(page.getByRole("textbox", {name: "Question"})).toHaveValue("Does a newer view retain its state?"); await expect(page.locator("body")).toHaveAttribute("data-state", "diff"); await expect(page.getByRole("button", {name: "Diff"})).toHaveAttribute("aria-current", "page"); }); @@ -1259,7 +1045,7 @@ async function assertReflow(page, row) { }); expect(result.documentOverflow).toBeLessThanOrEqual(1); expect(result.viewTitles).toEqual([ - {title: "Specifications", lines: 1}, {title: "Diff", lines: 1}, {title: "Traceability", lines: 1}, + {title: "Specifications", lines: 1}, {title: "Coverage", lines: 1}, {title: "Diff", lines: 1}, {title: "Traceability", lines: 1}, ]); const unlabelledOverflow = result.internal.filter((viewport) => !["graph-viewport", "table-viewport"].includes(viewport.className) || From d83e39c4e755cc9fbd247dfc8c8056a2d82c2cdd Mon Sep 17 00:00:00 2001 From: iperev Date: Sun, 6 Sep 2026 17:40:11 +0200 Subject: [PATCH 2/5] test: close native graph and handoff observer gaps --- .../testsupport/browserfixture/fixture.go | 5 +- tests/browser/workspace-evidence.spec.mjs | 58 +++++++++++++++---- tests/browser/workspace.spec.mjs | 37 +++++++++++- 3 files changed, 86 insertions(+), 14 deletions(-) diff --git a/internal/testsupport/browserfixture/fixture.go b/internal/testsupport/browserfixture/fixture.go index 63e264a..c953b56 100644 --- a/internal/testsupport/browserfixture/fixture.go +++ b/internal/testsupport/browserfixture/fixture.go @@ -38,7 +38,10 @@ func workspace(currentRisk string) (map[string]any, error) { graphInput := map[string]any{ "codeSources": []any{map[string]any{"content": code, "path": "src/retry.go"}}, "codeTopology": map[string]any{ - "edges": []any{map[string]any{"authorityClass": "owner_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRefs": []any{"browser.fixture.trace"}, "requirementId": RequirementID}}, + "edges": []any{ + map[string]any{"authorityClass": "owner_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRefs": []any{"browser.fixture.trace"}, "requirementId": RequirementID}, + map[string]any{"authorityClass": "owner_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRefs": []any{"browser.fixture.parallel-trace"}, "requirementId": RequirementID}, + }, "nativeCoverage": []any{ map[string]any{"authorityClass": "caller_reported", "codeNodeId": "code.retry", "currentnessState": "unverified", "evidenceRef": "browser.fixture.candidate", "producerId": "browser.fixture.candidate-runner", "requirementId": RequirementID, "state": "failed"}, map[string]any{"authorityClass": "receipt_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRef": "browser.fixture.execution", "producerId": "browser.fixture.runner", "requirementId": RequirementID, "state": "passed"}, diff --git a/tests/browser/workspace-evidence.spec.mjs b/tests/browser/workspace-evidence.spec.mjs index 48bf774..90b16c2 100644 --- a/tests/browser/workspace-evidence.spec.mjs +++ b/tests/browser/workspace-evidence.spec.mjs @@ -199,28 +199,66 @@ test("unavailable export effects preserve a selectable exact JSON fallback", asy await expect(page.locator("body")).not.toContainText("private download detail"); }); -for (const outcome of ["resolved", "rejected"]) { - test(`a late ${outcome} clipboard effect cannot label a newer view`, async ({baseURL, page}) => { +for (const outcome of ["resolved", "rejected"]) for (const newer of ["view", "packet"]) { + test(`a late ${outcome} clipboard effect cannot label a newer ${newer}`, async ({baseURL, page}) => { await page.setViewportSize({width: 1920, height: 1080}); await page.addInitScript(() => { - Object.defineProperty(navigator, "clipboard", {value: {writeText: () => new Promise((resolve, reject) => { globalThis.__clipboardRelease = {resolve, reject}; })}}); + globalThis.__clipboardCalls = []; + Object.defineProperty(navigator, "clipboard", {value: {writeText: text => { + let resolve, reject; + const promise = new Promise((accept, deny) => { resolve = accept; reject = deny; }); + globalThis.__clipboardCalls.push({text, resolve, reject, settled: promise.catch(() => {})}); + return promise; + }}}); }); await openWorkspace(page, baseURL); await page.getByRole("button", {name: "Select invariant"}).click(); const question = page.getByRole("textbox", {name: "Question", exact: true}); await question.fill("Do not erase this draft."); + const firstResponse = page.waitForResponse(response => response.url().endsWith("/api/v1/handoff")); await page.getByRole("button", {name: "Create handoff packet"}).click(); + const firstRaw = await (await firstResponse).text(); await page.getByRole("button", {name: "Copy JSON", exact: true}).click(); await expect(page.getByRole("button", {name: "Copy JSON", exact: true})).toBeDisabled(); - await page.getByRole("button", {name: "Diff", exact: true}).click(); - await expect(page.locator("body")).toHaveAttribute("data-state", "diff"); + expect(await page.evaluate(() => globalThis.__clipboardCalls.map(call => call.text))).toEqual([firstRaw]); + let secondRaw; + if (newer === "view") { + await page.getByRole("button", {name: "Diff", exact: true}).click(); + await expect(page.locator("body")).toHaveAttribute("data-state", "diff"); + } else { + await question.fill("Preserve packet B and its draft."); + const secondResponse = page.waitForResponse(response => response.url().endsWith("/api/v1/handoff")); + await page.getByRole("button", {name: "Create handoff packet"}).click(); + secondRaw = await (await secondResponse).text(); + expect(secondRaw).not.toBe(firstRaw); + await expect(page.locator("#handoff-status")).toHaveText("Handoff packet created."); + expect(await page.locator("#handoff-packet").textContent()).toBe(secondRaw); + await page.getByRole("button", {name: "Copy JSON", exact: true}).click(); + await expect(page.getByRole("button", {name: "Copy JSON", exact: true})).toBeDisabled(); + expect(await page.evaluate(() => globalThis.__clipboardCalls.map(call => call.text))).toEqual([firstRaw, secondRaw]); + } await page.evaluate(async outcome => { - if (outcome === "resolved") globalThis.__clipboardRelease.resolve(); else globalThis.__clipboardRelease.reject(new Error("private clipboard failure")); - await new Promise(resolve => setTimeout(resolve, 0)); + const call = globalThis.__clipboardCalls[0]; + if (outcome === "resolved") call.resolve(); else call.reject(new Error("private clipboard failure")); + await call.settled; }, outcome); - await expect(page.locator("#handoff-status")).toHaveText("No source-bound text selected."); - await expect(page.locator("#handoff-preview")).toBeEmpty(); - await expect(question).toHaveValue("Do not erase this draft."); + if (newer === "view") { + await expect(page.locator("#handoff-status")).toHaveText("No source-bound text selected."); + await expect(page.locator("#handoff-preview")).toBeEmpty(); + await expect(question).toHaveValue("Do not erase this draft."); + } else { + await expect(page.locator("#handoff-status"), "packet B status ignores old Copy settlement").toHaveText("Handoff packet created."); + expect(await page.locator("#handoff-packet").textContent()).toBe(secondRaw); + await expect(question).toHaveValue("Preserve packet B and its draft."); + await expect(page.getByRole("button", {name: "Copy JSON", exact: true})).toBeDisabled(); + await expect(page.getByRole("button", {name: "Download JSON", exact: true})).toBeEnabled(); + await page.evaluate(async () => { const call = globalThis.__clipboardCalls[1]; call.resolve(); await call.settled; }); + await expect(page.locator("#handoff-status")).toHaveText("Exact handoff JSON copied."); + expect(await page.locator("#handoff-packet").textContent(), "settled packet B carrier").toBe(secondRaw); + await expect(question).toHaveValue("Preserve packet B and its draft."); + await expect(page.getByRole("button", {name: "Download JSON", exact: true})).toBeEnabled(); + await expect(page.getByRole("button", {name: "Copy JSON", exact: true})).toBeEnabled(); + } await expect(page.locator("body")).not.toContainText("private clipboard failure"); }); } diff --git a/tests/browser/workspace.spec.mjs b/tests/browser/workspace.spec.mjs index 9bb26f5..714299d 100644 --- a/tests/browser/workspace.spec.mjs +++ b/tests/browser/workspace.spec.mjs @@ -654,6 +654,7 @@ test("workspace renders admitted views and creates a keyboard-authorized handoff const edges = projection.edges; const nodeIDs = nodes.map((node) => node.nodeId); const edgeIDs = edges.map((edge) => edge.edgeId); + expect(edges.some((edge, index) => edges.slice(index + 1).some(other => edge.edgeId !== other.edgeId && edge.fromNodeId === other.fromNodeId && edge.toNodeId === other.toNodeId)), "source fixture preserves owner-distinct parallel relations").toBe(true); const graph = page.locator(".graph-canvas > svg"); const graphViewport = page.getByRole("region", {name: "Traceability graph viewport"}); await expect(graphViewport).toBeVisible(); @@ -684,21 +685,51 @@ test("workspace renders admitted views and creates a keyboard-authorized handoff const edgeRecords = page.getByRole("list", {name: "Admitted traceability edges"}).locator(":scope > li"); await expectIdentityOrder(nodeRecords, nodeIDs); await expectIdentityOrder(edgeRecords, edgeIDs); + const nativeGraph = await graph.evaluate(svg => ({ + boxes: Array.from(svg.parentElement.querySelectorAll(":scope > button[data-graph-select]"), element => { + const rect = element.getBoundingClientRect(); + return {id: element.dataset.graphSelect, x: rect.left, y: rect.top, width: rect.width, height: rect.height}; + }), + lines: Array.from(svg.querySelectorAll("line"), line => { + const matrix = line.getScreenCTM(); + if (!matrix) throw new Error("Native line coordinate system is unavailable"); + const start = new DOMPoint(line.x1.baseVal.value, line.y1.baseVal.value).matrixTransform(matrix); + const end = new DOMPoint(line.x2.baseVal.value, line.y2.baseVal.value).matrixTransform(matrix); + return {id: line.dataset.edgeId, raw: ["x1", "y1", "x2", "y2"].map(name => Number(line.getAttribute(name))), points: [start.x, start.y, end.x, end.y]}; + }), + })); + expect(nativeGraph.lines.map(line => line.id), "complete native line identities").toEqual(edgeIDs); + const boxes = nativeGraph.boxes; + const boxesByID = new Map(boxes.map(box => [box.id, box])); + expect([...boxesByID.keys()]).toEqual(nodeIDs); + for (const box of boxes) { + expect([box.x, box.y, box.width, box.height].every(Number.isFinite)).toBe(true); + expect(box.width).toBeGreaterThan(0); + expect(box.height).toBeGreaterThan(0); + } for (let index = 0; index < edges.length; index++) { const edge = edges[index]; const details = edgeRecords.nth(index).locator("details"); await details.locator("summary").click(); await expect(details.locator("dt")).toHaveText(Object.keys(edge)); await expect(details.locator("dd")).toHaveText(Object.values(edge).map(value => Array.isArray(value) ? value.join(", ") : String(value))); - const line = graph.locator(":scope > line").nth(index); + const line = graph.locator("line").nth(index); await expect(line).toHaveAttribute("data-edge-id", edge.edgeId); await expect(line).toHaveAttribute("marker-end", "url(#graph-arrow)"); - const geometry = await line.evaluate(element => ["x1", "y1", "x2", "y2"].map(name => Number(element.getAttribute(name)))); + const geometry = nativeGraph.lines[index].points; + expect(nativeGraph.lines[index].raw.every(Number.isFinite)).toBe(true); expect(geometry.every(Number.isFinite)).toBe(true); expect(geometry[0] !== geometry[2] || geometry[1] !== geometry[3]).toBe(true); + for (const [role, id, x, y] of [["source", edge.fromNodeId, geometry[0], geometry[1]], ["target", edge.toNodeId, geometry[2], geometry[3]]]) { + const box = boxesByID.get(id); + expect(box, `${role} endpoint node`).toBeDefined(); + const tolerance = 0.5; + const inside = x >= box.x - tolerance && x <= box.x + box.width + tolerance && y >= box.y - tolerance && y <= box.y + box.height + tolerance; + const perimeter = Math.min(Math.abs(x - box.x), Math.abs(x - box.x - box.width), Math.abs(y - box.y), Math.abs(y - box.y - box.height)) <= tolerance; + expect(inside && perimeter, `${role} endpoint of ${edge.edgeId} touches ${id}`).toBe(true); + } await expectCSS(line, {visibility: "visible", opacity: "1", stroke: "rgb(32, 37, 34)", "stroke-width": "1.5px", filter: "none", "clip-path": "none"}); } - const boxes = await buttons.evaluateAll(elements => elements.map(element => ({x: element.offsetLeft, y: element.offsetTop, width: element.offsetWidth, height: element.offsetHeight}))); for (let i = 0; i < boxes.length; i++) for (let j = i + 1; j < boxes.length; j++) { const a = boxes[i], b = boxes[j]; expect(a.x + a.width <= b.x || b.x + b.width <= a.x || a.y + a.height <= b.y || b.y + b.height <= a.y).toBe(true); From ecbeadb310bca2354a788ad3af70698f97d706a8 Mon Sep 17 00:00:00 2001 From: iperev Date: Sun, 6 Sep 2026 17:56:10 +0200 Subject: [PATCH 3/5] fix: synchronize browser evidence contract source bindings --- internal/app/cli_contract_test.go | 2 +- internal/app/command_contract_generated.go | 8 ++++---- internal/command/stackpreset/preset_ids_generated.go | 2 +- proofkit/cli-contract.v2.json | 12 ++++++------ 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/internal/app/cli_contract_test.go b/internal/app/cli_contract_test.go index 337f910..16c7410 100644 --- a/internal/app/cli_contract_test.go +++ b/internal/app/cli_contract_test.go @@ -24,7 +24,7 @@ import ( ) const ( - cliContractPublicABISHA256 = "679a9152618bff6c848bacea0aaf2ae09bef24f7d6176add1733248a287225ae" + cliContractPublicABISHA256 = "3fea991fd7ef956c6e2252e909aa4a01ffaf453c8cf3ae1c6ba8df4fe9521cb1" maxAggregateFileReadBytesForContractTest = 64 << 20 maxPackageManifestBytesForContractTest = 256 << 10 maxSourceFileBytesForContractTest = 8 << 20 diff --git a/internal/app/command_contract_generated.go b/internal/app/command_contract_generated.go index b376a79..50ebb97 100644 --- a/internal/app/command_contract_generated.go +++ b/internal/app/command_contract_generated.go @@ -1,7 +1,7 @@ // Code generated by internal/tools/commandcontractgen; DO NOT EDIT. package app -const commandContractSourceSHA256 = "187b115fbdb47c8e88154e118a414a1f9e779c7663eec8a4a09c843a71bd61e9" +const commandContractSourceSHA256 = "e73b37ff7bbef58b81289c13a28b34bbe4fbe42b198e52fc897aa6e1847fb80c" type generatedCommandContractMetadata struct { InputContractSHA256 string @@ -67,11 +67,11 @@ var generatedCommandContractMetadataByName = map[string]generatedCommandContract "repository-inventory": {InputContractSHA256: "", InputSchemaSummary: []string(nil), OutputContractSHA256: "sha256:4a6fc5b5ef55090854e70927494d220afdee0ae234de4f61a720a6018865f02f", FlagChoices: map[string][]string{}, RouteTokens: []string{"repository-inventory"}}, "requirement-authoring-plan": {InputContractSHA256: "sha256:208d7d47109dee1ec355ae3970937690ae528a9cc0cb0eb885d7cc72d843f1e8", InputSchemaSummary: []string{"schemaVersion=1", "root-shape-only definition proofkit.requirement-authoring-plan.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:e995d289c4a44310add784bbafa5a3a50ec305c3809a89506dd3b49914fbe28f", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-authoring-plan"}}, "requirement-bindings": {InputContractSHA256: "sha256:4771b7ed1e23b20c983060deb8f8e65391052f0e5a61cf0f5c67c0e73b8fc5dd", InputSchemaSummary: []string{"schemaVersion=1", "root-shape-only definition proofkit.requirement-bindings.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:7821c7b23ff2c0ca83c64039c22400d90660cad73a60b9afb46829c539c61168", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-bindings"}}, - "requirement-browser-server": {InputContractSHA256: "sha256:0bd65165c4c8c56a66081d1db4caabf5814957706c23ae4868bc68eadbc460d5", InputSchemaSummary: []string{"workspace mode: schemaVersion=2", "workspace mode: workspaceId", "workspace mode: context=proofkit.requirement-context schemaVersion=2 with strict v1 adapter", "workspace mode: diffInput=proofkit.requirement-semantic-diff-input schemaVersion=2 (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", "root-shape-only definition proofkit.requirement-browser-server.input.v3.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:08ea562adc8fdbfb8bc30851a91b7f64d00d35e193b13475e6f98d83b8aaa528", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-browser-server"}}, + "requirement-browser-server": {InputContractSHA256: "sha256:c6a3ac09a55f21c7201ba828ac1d1d6140c292f54695a4422957540945f11c91", InputSchemaSummary: []string{"workspace mode: schemaVersion=2", "workspace mode: workspaceId", "workspace mode: context=proofkit.requirement-context schemaVersion=2 with strict v1 adapter", "workspace mode: diffInput=proofkit.requirement-semantic-diff-input schemaVersion=2 (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", "root-shape-only definition proofkit.requirement-browser-server.input.v3.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:a6b8b2886cd303fa306656d4be8a20c4f3046056989a49788c0f6e93ad09410b", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-browser-server"}}, "requirement-context-compose": {InputContractSHA256: "sha256:3b06ebca2a07d01b34005d915918b8a7743ef8175901ee8dd0a37ecfb6ee80fe", InputSchemaSummary: []string{"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", "root-shape-only definition proofkit.requirement-context-compose.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:a2b8bf00d2308628e1835fe890dc6e9c4f402c531726f0bdaffad1d7100a7466", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-context-compose"}}, "requirement-context-slice": {InputContractSHA256: "sha256:883e864e44944270f7b85c013635835e5e1f1a49a7fd7ca3ebe860c7b56da601", InputSchemaSummary: []string{"schemaVersion=1", "sliceId", "context=proofkit.requirement-context schemaVersion=2 with strict v1 adapter", "query.profile=routing|specification|proof|coverage|review", "query.nodeIds[]|requirementIds[]|ownerIds[]|lifecycleStates[]", "query.maxDepth=0..512", "query.maxNodes=1..4096", "query.maxRequirements=1..16384", "root-shape-only definition proofkit.requirement-context-slice.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:971f78ec94bb29a24057343ccfb3d1192134d2ac88968aab5193e3d64ac87506", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-context-slice"}}, "requirement-coverage-input-compose": {InputContractSHA256: "sha256:1980d1fc5c3c3cfe08f557e3c55f7128de5bae0d9b25bd2a46d7c6e47db73faa", InputSchemaSummary: []string{"schemaVersion=2", "root-shape-only definition proofkit.requirement-coverage-input-compose.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:3a8686e91f3a229b273531d9c03cb6ce86ec76b66f8c35c6ca7f361b6e5eeaff", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-coverage-input-compose"}}, - "requirement-coverage-view": {InputContractSHA256: "sha256:40b06176f12dc9ec92226d7c01be53df5aa2b0e949a7791a894c8cf148e44b21", InputSchemaSummary: []string{"schemaVersion=2", "root-shape-only definition proofkit.requirement-coverage-view.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:4ec6c0bb6d616d23b777e59721a3ff045e6b447401333300031d641218c926bf", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-coverage-view"}}, + "requirement-coverage-view": {InputContractSHA256: "sha256:202dfbf2b9929a9244ba067a6a57af361e8f7da245625d3d53f13d73e04f14e3", InputSchemaSummary: []string{"schemaVersion=2", "root-shape-only definition proofkit.requirement-coverage-view.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:b5784b98b903ef9bf9ddbac047592c32baeda96a83c3e426dee51d64d3846269", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-coverage-view"}}, "requirement-impact-input-compose": {InputContractSHA256: "sha256:c80c57489205004f92603fec541ce3d36dd0d9b65109dcfefb97bcfb07b90679", InputSchemaSummary: []string{"schemaVersion=2", "root-shape-only definition proofkit.requirement-impact-input-compose.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:b0b689f4d0b5bafc52c6041a2aa3583c9c8628aa0f13a0f0d7c42a610ed1a0d6", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-impact-input-compose"}}, "requirement-proof-resolver": {InputContractSHA256: "sha256:7ffedf651fbeda57f11f780373ae8f2b15dd587ce3aaddf739a092bc4835f2c5", InputSchemaSummary: []string{"schemaVersion=2", "root-shape-only definition proofkit.requirement-proof-resolver.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:d6b1fbbf4a7fe3624c64f88c8e316fd927df8f35355198962110dab41113bc94", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-proof-resolver"}}, "requirement-proof-source-set": {InputContractSHA256: "sha256:e00367ea2c9b700b46756d112868fd14d20ca337d71c2032e7fb8ea0b11cf0ce", InputSchemaSummary: []string{"canonicalEnvelope", "schemaVersion", "sourceSet", "sources", "root-shape-only definition proofkit.requirement-proof-source-set.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:9889e93cf457ecacfd673bd1aa148740b549ae614bb8c1e56ce5bb9fb387bdea", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-proof-source-set"}}, @@ -82,7 +82,7 @@ var generatedCommandContractMetadataByName = map[string]generatedCommandContract "requirement-source-view": {InputContractSHA256: "sha256:0819889f9bfaddefe0555250612ef5f4d9172899b04d427d48b0420d765c00ad", InputSchemaSummary: []string{"schemaVersion=1", "root-shape-only definition proofkit.requirement-source-view.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:2f29bd1edea7c3e930a143c2f96c229a0a199e52c89367302c414759bf660c44", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-source-view"}}, "requirement-spec-tree": {InputContractSHA256: "sha256:96876589778a1cf1bc3f41fa33ad86de502db05886ba620ecbee59225060e315", InputSchemaSummary: []string{"schemaVersion", "treeId", "rootNodeId", "callerAnnotations", "nodes", "edges", "overlays", "root-shape-only definition proofkit.requirement-spec-tree.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:a027461411b8614288186df2c014a9e5303f905f0fb4cfc9b3ed6439790ae547", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-spec-tree"}}, "requirement-spec-tree-view": {InputContractSHA256: "sha256:9e725fc145c437e0f9cdea0deed86189da855cc7d0350d33e59c80d34d91c03a", InputSchemaSummary: []string{"schemaVersion", "treeId", "rootNodeId", "callerAnnotations", "nodes", "edges", "overlays", "root-shape-only definition proofkit.requirement-spec-tree-view.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:ba9b258e45d485936ddbfd76f7a7c43a5ae5760a4fe6da56bce4a45afd4221e6", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-spec-tree-view"}}, - "requirement-traceability-graph": {InputContractSHA256: "sha256:b93bf9f9884452e4c7ae72b181efff4dd5fa4781ba62284a311d41c54bdc2ad7", InputSchemaSummary: []string{"schemaVersion=2", "graphId", "context=proofkit.requirement-context schemaVersion=2 with strict v1 adapter", "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", "root-shape-only definition proofkit.requirement-traceability-graph.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:64b0c190c64a016f3c31a60f6e2327d5fa9f6f834ff83540be690e790e9595ab", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-traceability-graph"}}, + "requirement-traceability-graph": {InputContractSHA256: "sha256:9a67442525f4831a6d24a189cb0040d3ab0478bf70c5d1e219fa41b6592a7818", InputSchemaSummary: []string{"schemaVersion=2", "graphId", "context=proofkit.requirement-context schemaVersion=2 with strict v1 adapter", "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", "root-shape-only definition proofkit.requirement-traceability-graph.input.v2.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:28035f0124497a1456e180490cddc05064af3fafaa617f079b417b82bbc623c3", FlagChoices: map[string][]string{}, RouteTokens: []string{"requirement-traceability-graph"}}, "scaffold-profile-plan": {InputContractSHA256: "sha256:bc2a9dc33664fc0555bb5c4b67c6c2caa451995f7bcb1b8add8ea8a8aabd88a6", InputSchemaSummary: []string{"schemaVersion=1", "root-shape-only definition proofkit.scaffold-profile-plan.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:3d5d6584ef88c14534333e62b677ecac73d5bae659edf71893faa7ab1068659c", FlagChoices: map[string][]string{}, RouteTokens: []string{"scaffold-profile-plan"}}, "scaffold-project-structure": {InputContractSHA256: "sha256:0db5eca08d353a8d314908a34d8293c947a9d208e280353d9784b489576ec55a", InputSchemaSummary: []string{"schemaVersion=1", "root-shape-only definition proofkit.scaffold-project-structure.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:79950f8b779b00616be24b2d7e28021a83e9414881676ae86ab467940d36e6cb", FlagChoices: map[string][]string{}, RouteTokens: []string{"scaffold-project-structure"}}, "secret-scan": {InputContractSHA256: "sha256:bf2f193e382bc1bf709031be6d9d9c913264e1c5865b926ae7d72ac14ea35324", InputSchemaSummary: []string{"files", "nonClaims", "reportId", "schemaVersion", "root-shape-only definition proofkit.secret-scan.input.v1.root-shape; nested fields, types, and cardinalities are non-claims"}, OutputContractSHA256: "sha256:25ec4640a71e0ce30709b3215535439561d671de9b5be8228b710ab556e0fd8a", FlagChoices: map[string][]string{}, RouteTokens: []string{"secret-scan"}}, diff --git a/internal/command/stackpreset/preset_ids_generated.go b/internal/command/stackpreset/preset_ids_generated.go index 9e8c5d4..40d2e82 100644 --- a/internal/command/stackpreset/preset_ids_generated.go +++ b/internal/command/stackpreset/preset_ids_generated.go @@ -1,6 +1,6 @@ // Code generated by internal/tools/commandcontractgen; DO NOT EDIT. package stackpreset -const presetContractSourceSHA256 = "187b115fbdb47c8e88154e118a414a1f9e779c7663eec8a4a09c843a71bd61e9" +const presetContractSourceSHA256 = "e73b37ff7bbef58b81289c13a28b34bbe4fbe42b198e52fc897aa6e1847fb80c" var presetIDs = []string{"agentic_runtime_repo", "generated_docs_contract_repo", "python_service", "python_typescript_service", "typescript_monorepo", "typescript_workspace"} diff --git a/proofkit/cli-contract.v2.json b/proofkit/cli-contract.v2.json index 9bc1659..59cd8e0 100644 --- a/proofkit/cli-contract.v2.json +++ b/proofkit/cli-contract.v2.json @@ -4939,7 +4939,7 @@ "rootDefinitionDigest": "sha256:e6af5b9edb1284ab2ff2f1a276a6b924127b99810cd9446bffbc971f638a0997", "nativeSource": { "path": "internal/command/requirementbrowser", - "canonicalDigest": "sha256:2f6113b67ba6bbddac190b232ff5788aa48cd9dbec2a73f057a6152a2020b49e", + "canonicalDigest": "sha256:308099bac0caa0aa309a9f236182a6a09e0caac6fb5c7c07679fa471d1ee590c", "evidenceClass": "source_checkout" }, "nativeAdmissionWitnessSelector": { @@ -4976,7 +4976,7 @@ "rootDefinitionDigest": "sha256:c2e7d851c7928560d4267fe85ebc0ae61e33c4c0ef15f7f7b01deb73bb80eda7", "nativeSource": { "path": "internal/command/requirementbrowser", - "canonicalDigest": "sha256:2f6113b67ba6bbddac190b232ff5788aa48cd9dbec2a73f057a6152a2020b49e", + "canonicalDigest": "sha256:308099bac0caa0aa309a9f236182a6a09e0caac6fb5c7c07679fa471d1ee590c", "evidenceClass": "source_checkout" }, "nativeOutputWitnessSelector": { @@ -5381,7 +5381,7 @@ "rootDefinitionDigest": "sha256:2365e4778d6c24c0af9507ce93bfba0a89c4ba9ece8da1c5b25b4581d6b80fa1", "nativeSource": { "path": "internal/command/requirementcoverageview", - "canonicalDigest": "sha256:5a60148d843025a2ad7a2b72566792778120fc7979c5ec9c9db8dcac42e7dffd", + "canonicalDigest": "sha256:2649d149fc0615ef1991656fcc62c32a8332009cbedff0a6f165746d744f0915", "evidenceClass": "source_checkout" }, "nativeOutputWitnessSelector": { @@ -5415,7 +5415,7 @@ "rootDefinitionDigest": "sha256:f42c9218c861b1e30ec3692fa0097da393e36eea2049d4aac1a05a8b0a40d81d", "nativeSource": { "path": "internal/command/requirementcoverageview", - "canonicalDigest": "sha256:5a60148d843025a2ad7a2b72566792778120fc7979c5ec9c9db8dcac42e7dffd", + "canonicalDigest": "sha256:2649d149fc0615ef1991656fcc62c32a8332009cbedff0a6f165746d744f0915", "evidenceClass": "source_checkout" }, "nativeAdmissionWitnessSelector": { @@ -6344,7 +6344,7 @@ "rootDefinitionDigest": "sha256:6487ff537380d1cbffe5a72b9688e9ce6baffa218e76f8dbbfe8f50d14509219", "nativeSource": { "path": "internal/command/requirementgraph", - "canonicalDigest": "sha256:330cc4ceef881c5ad8cfac76c0c9876ed65e897d5ffe631e01c8625d35b09fa3", + "canonicalDigest": "sha256:26836d1c497ccf3f8609dfc6e4559f24c1a5f767e15114af955f97ab26238926", "evidenceClass": "source_checkout" }, "nativeAdmissionWitnessSelector": { @@ -6382,7 +6382,7 @@ "rootDefinitionDigest": "sha256:37d07abc4d9122176ffab9842b5d85fbfdbe068ee9e4097da8fc21206aae1d47", "nativeSource": { "path": "internal/command/requirementgraph", - "canonicalDigest": "sha256:330cc4ceef881c5ad8cfac76c0c9876ed65e897d5ffe631e01c8625d35b09fa3", + "canonicalDigest": "sha256:26836d1c497ccf3f8609dfc6e4559f24c1a5f767e15114af955f97ab26238926", "evidenceClass": "source_checkout" }, "nativeOutputWitnessSelector": { From 9027f2cdd135c5f7b37e07f9985f379faef17b5d Mon Sep 17 00:00:00 2001 From: iperev Date: Sun, 6 Sep 2026 18:24:04 +0200 Subject: [PATCH 4/5] test: bind release notes to current browser capabilities --- internal/tools/releasechange/record_test.go | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/internal/tools/releasechange/record_test.go b/internal/tools/releasechange/record_test.go index a82ab1b..23a0fd5 100644 --- a/internal/tools/releasechange/record_test.go +++ b/internal/tools/releasechange/record_test.go @@ -197,9 +197,9 @@ func TestCurrentChangeRecordNamesReviewedSemanticChanges(t *testing.T) { var currentBreakingChanges = []Change{} var currentAdditions = []Change{ - {ChangeID: "proofkit.browser.lookup", Summary: "Search and filter the complete admitted requirement cohort before bounded paging, navigate ordered specification children, and preserve original source anchors and exact omission counts without loading the full snapshot into the browser."}, - {ChangeID: "proofkit.browser.request-recovery", Summary: "Distinguish correction, denied, stale, unavailable and retryable failures. Explicit Retry preserves the failed route, snapshot and complete page query, while superseded requests cannot restore stale content or request authority."}, - {ChangeID: "proofkit.browser.responsive-shell", Summary: "Add compact Browse and Inspector panels with native modal behavior on smaller viewports, stable keyboard focus, retained question drafts, source-bound Unicode selection and lazy boundary details."}, + {ChangeID: "proofkit.browser.coverage-inspection", Summary: "Inspect compact or structured coverage beside original source-bound requirements, distinguish missing evidence from reported verdicts, preserve complete evidence and non-claims in disclosures, and ask an explicit evidence question without replacing an existing draft."}, + {ChangeID: "proofkit.browser.diff-and-graph-inspection", Summary: "Show exact diff-page class, entity, risk and lifecycle counts. Inspect a bounded traceability diagram and equivalent records with local evidence-plane and neighborhood filters, preserved directed relations, exact numeric source coordinates, explicit outside-page references and deliberate target-page navigation."}, + {ChangeID: "proofkit.browser.handoff-inspection", Summary: "Preview included source-bound handoff context by stable requirement identity and explicitly copy or download the exact compact server JSON. Obsolete view or clipboard results cannot replace current output; independent pending exclusion and denied or stale request locks survive settlement, with one workspace reload action for a stale session."}, } var currentMigrationSteps = []string{} @@ -222,7 +222,7 @@ func validateCurrentChangeRecord(record Record, notes string) error { func currentExpectedReleaseNotes() string { lines := []string{ - "# @research-engineering/agentic-proofkit 0.12.0", + "# @research-engineering/agentic-proofkit 0.13.0", "", "## Breaking Contract Changes", "", @@ -267,14 +267,14 @@ func currentExpectedReleaseNotes() string { "- TSX source parsing remains unsupported.", "- Managed integration baselines are cooperative byte/mode bookkeeping, not authenticated origin or protection against coordinated same-user edits. File lifecycle does not prove native host discovery, instruction loading, or approved-launcher invocation.", "- Desired-absence journals and newly retained terminal receipts use schema v2. Earlier binaries reject these records without effects. Present-only v1 plan/journal bytes and historical recovery remain supported; finishing recovery does not enable downgrade of retained v2 receipts.", - "- Browser lookup and navigation are presentation-only fragments, not proof coverage or an external HTTP SDK. Annotations are session-bound; browser controls do not edit specifications or execute agents.", + "- Browser lookup, coverage, diff and graph fragments are derived presentation, not authenticated evidence, proof execution or an external HTTP SDK. Local graph filters apply only to the returned page; absent coverage is not a verdict. Exact numeric observation requires native JSON source-token and raw-value support; unsupported clients show unavailable instead of rounded coordinates. Annotations are session-bound and exported bytes are not revoked by later navigation; browser controls do not edit specifications or execute agents.", "", "## Install", "", "Primary npm channel:", "", "```bash", - "npm install --save-dev --save-exact @research-engineering/agentic-proofkit@0.12.0", + "npm install --save-dev --save-exact @research-engineering/agentic-proofkit@0.13.0", "```", "", "Pre-1.0 npm consumers must keep this dependency exact-pinned.", @@ -286,7 +286,7 @@ func currentExpectedReleaseNotes() string { "## Rollback", "", "- First follow the migration and persistent-state compatibility restrictions above; changing a package pin does not roll back repository state.", - "- Pin npm consumers to the previous admitted version 0.11.0 with `npm install --save-dev --save-exact @research-engineering/agentic-proofkit@0.11.0`.", + "- Pin npm consumers to the previous admitted version 0.12.0 with `npm install --save-dev --save-exact @research-engineering/agentic-proofkit@0.12.0`.", "- Treat local package artifacts as candidates until registry identity is proven.", ) return strings.Join(lines, "\n") + "\n" From dc8fe6b7b2ceacf6b2480078ed4b14403aa2943b Mon Sep 17 00:00:00 2001 From: iperev Date: Sun, 6 Sep 2026 19:10:51 +0200 Subject: [PATCH 5/5] test: isolate graph paging from parallel trace fixtures --- internal/testsupport/browserfixture/fixture.go | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/internal/testsupport/browserfixture/fixture.go b/internal/testsupport/browserfixture/fixture.go index c953b56..e6dd997 100644 --- a/internal/testsupport/browserfixture/fixture.go +++ b/internal/testsupport/browserfixture/fixture.go @@ -13,14 +13,14 @@ import ( const RequirementID = "REQ-CONSUMER-001" func Workspace() (map[string]any, error) { - return workspace("high") + return workspace("high", true) } func PagingWorkspace() (map[string]any, error) { - return workspace("medium") + return workspace("medium", false) } -func workspace(currentRisk string) (map[string]any, error) { +func workspace(currentRisk string, parallelTrace bool) (map[string]any, error) { base, err := snapshot("The system preserves the original semantic identity.", "high") if err != nil { return nil, err @@ -35,13 +35,14 @@ func workspace(currentRisk string) (map[string]any, error) { } code := "package retry\n\nfunc Retry() {}\n" start := strings.Index(code, "func Retry") + traceEdges := []any{map[string]any{"authorityClass": "owner_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRefs": []any{"browser.fixture.trace"}, "requirementId": RequirementID}} + if parallelTrace { + traceEdges = append(traceEdges, map[string]any{"authorityClass": "owner_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRefs": []any{"browser.fixture.parallel-trace"}, "requirementId": RequirementID}) + } graphInput := map[string]any{ "codeSources": []any{map[string]any{"content": code, "path": "src/retry.go"}}, "codeTopology": map[string]any{ - "edges": []any{ - map[string]any{"authorityClass": "owner_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRefs": []any{"browser.fixture.trace"}, "requirementId": RequirementID}, - map[string]any{"authorityClass": "owner_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRefs": []any{"browser.fixture.parallel-trace"}, "requirementId": RequirementID}, - }, + "edges": traceEdges, "nativeCoverage": []any{ map[string]any{"authorityClass": "caller_reported", "codeNodeId": "code.retry", "currentnessState": "unverified", "evidenceRef": "browser.fixture.candidate", "producerId": "browser.fixture.candidate-runner", "requirementId": RequirementID, "state": "failed"}, map[string]any{"authorityClass": "receipt_admitted", "codeNodeId": "code.retry", "currentnessState": "current", "evidenceRef": "browser.fixture.execution", "producerId": "browser.fixture.runner", "requirementId": RequirementID, "state": "passed"},