diff --git a/docs/reconstruction-coverage.md b/docs/reconstruction-coverage.md index d9912db92d..12beb13ca5 100644 --- a/docs/reconstruction-coverage.md +++ b/docs/reconstruction-coverage.md @@ -41,3 +41,17 @@ neither a passing nor a failed package workflow. The evaluator preserves Evidence provenance and returns an actionable unknown when qualification is unavailable. It does not change the cited records to make their authority match a caller's declaration. + +## Function reconstruction claims + +`verify_reconstruction` evaluates declared claims over retained comparison +Evidence. An `overall` function claim includes active residual unknowns scoped +to any of that comparison's dimensions. For example, an open pseudocode +question keeps the overall claim `unknown` and retains its unknown ID and +recommended probe; an independent assembly claim can still pass. An unknown +scoped only to `overall` does not block every individual dimension. + +Selection uses each unknown's latest revision, its comparison identity and +Evidence references. Explicit unknown dependencies remain relevant across +dimensions. Unknowns for another comparison and resolved heads do not become +blockers merely because their source Evidence overlaps. diff --git a/src/domain/reconstructionUnknowns.test.ts b/src/domain/reconstructionUnknowns.test.ts index 9fa406b199..6286966f9a 100644 --- a/src/domain/reconstructionUnknowns.test.ts +++ b/src/domain/reconstructionUnknowns.test.ts @@ -71,3 +71,32 @@ it("keeps explicit dependencies while excluding unrelated scoped unknowns", () = other.unknown_id, ]); }); + +it("aggregates constituent unknowns without importing another comparison's scope", () => { + const scoped = (comparisonId: string) => + createResidualUnknown( + { + ...base, + question: "Unresolved pseudocode", + comparison_conclusion_scope: { + comparison_evidence_id: comparisonId, + dimensions: ["pseudocode"], + }, + relationships: [], + }, + ev("c"), + null, + ); + const own = scoped(ev("a")); + const foreign = scoped(ev("b")); + const heads = new Map([ + [own.unknown_id, own], + [foreign.unknown_id, foreign], + ]); + expect( + reconstructionClaimUnknowns(heads, ev("a"), [ev("b")], "overall"), + ).toEqual([own]); + expect( + reconstructionClaimUnknowns(heads, ev("a"), [ev("b")], "assembly"), + ).toEqual([]); +}); diff --git a/src/domain/reconstructionUnknowns.ts b/src/domain/reconstructionUnknowns.ts index c09e814eb0..64d40d0491 100644 --- a/src/domain/reconstructionUnknowns.ts +++ b/src/domain/reconstructionUnknowns.ts @@ -23,7 +23,7 @@ export const reconstructionUnknownHeads = ( return heads; }; -/** Find active unknowns that affect a comparison or one of its sources. */ +/** Overall claims include every scoped dimension; individual claims keep their scope. */ export const reconstructionClaimUnknowns = ( heads: ReadonlyMap, comparisonId: string, @@ -36,6 +36,7 @@ export const reconstructionClaimUnknowns = ( scope === undefined || (scope.comparison_evidence_id === comparisonId && (dimension === undefined || + dimension === "overall" || scope.dimensions.some( (scopedDimension) => scopedDimension === dimension, ))) diff --git a/src/domain/reconstructionVerification.ts b/src/domain/reconstructionVerification.ts index 3224f3604a..9aa7abdce0 100644 --- a/src/domain/reconstructionVerification.ts +++ b/src/domain/reconstructionVerification.ts @@ -153,15 +153,13 @@ const evaluateClaim = ( ...authorityLimitations(claim, sources, sides), ...callCoverage.blockers, ]; - const relatedUnknowns = reconstructionClaimUnknowns( + const relevantUnknowns = reconstructionClaimUnknowns( heads, comparison.evidence_id, allSourceIds, claim.dimension, ); - const relevantUnknowns = relatedUnknowns; const status = classify(observed, blockers, relevantUnknowns); - const displayedUnknowns = relevantUnknowns; return reconstructionClaimResultSchema.parse({ claim_id: claim.claim_id, kind: claim.kind, @@ -172,13 +170,13 @@ const evaluateClaim = ( left_evidence_ids: sides.left, right_evidence_ids: sides.right, evidence_links: uniqueSorted([comparison.evidence_id, ...allSourceIds]), - unknown_ids: displayedUnknowns.map(({ unknown_id: id }) => id), + unknown_ids: relevantUnknowns.map(({ unknown_id: id }) => id), limitations: uniqueSorted([ ...comparison.limitations, ...observation.limitations, ...blockers, ...callCoverage.diagnostics, - ...displayedUnknowns.map( + ...relevantUnknowns.map( ({ question }) => `Residual unknown: ${question}`, ), ]), diff --git a/tests/acceptance/tools/reconstructionScopedUnknowns.test.ts b/tests/acceptance/tools/reconstructionScopedUnknowns.test.ts new file mode 100644 index 0000000000..9ff527edda --- /dev/null +++ b/tests/acceptance/tools/reconstructionScopedUnknowns.test.ts @@ -0,0 +1,154 @@ +import { expect, it } from "vitest"; + +import { FUNCTION_COMPARISON_EXAMPLE } from "../../../src/contracts/functionComparisonExample.js"; +import { toolContract } from "../../../src/contracts/toolContracts.js"; +import { createEvidence, parseEvidence } from "../../../src/domain/evidence.js"; +import { reconstructionVerificationResultSchema } from "../../../src/domain/reconstructionVerificationSchemas.js"; +import { connectLocalToolsMcp } from "../../fixtures/localToolsMcp.js"; + +const unchangedRight = () => { + const left = FUNCTION_COMPARISON_EXAMPLE.left; + return createEvidence( + { path: "/fixture/rebuilt", sha256: "2".repeat(64), format: "mach-o" }, + left.provider, + { + operation: left.operation, + parameters: left.parameters, + result: left.normalized_result, + confidence: left.confidence, + authority: left.authority, + relationshipCoverage: { status: "complete" }, + }, + ); +}; + +const verify = async ( + call: Awaited>["call"], + comparisonId: string, + dimensions: readonly ("overall" | "pseudocode" | "assembly")[], +) => { + const response = await call("verify_reconstruction", { + specification: { + name: "Scoped function uncertainty", + claims: dimensions.map((dimension) => ({ + kind: "structural-function", + claim_id: dimension, + title: `Check ${dimension}`, + comparison_evidence_id: comparisonId, + dimension, + })), + }, + }); + expect(response.isError, JSON.stringify(response)).not.toBe(true); + return reconstructionVerificationResultSchema.parse( + parseEvidence(response.structuredContent).normalized_result, + ); +}; + +it.each(["pseudocode", "overall"] as const)( + "keeps an overall claim unknown for an active %s question through stdio MCP", + async (dimension) => { + const { call } = await connectLocalToolsMcp(); + const left = FUNCTION_COMPARISON_EXAMPLE.left; + const right = unchangedRight(); + const compared = await call("compare_functions", { left, right }); + expect(compared.isError, JSON.stringify(compared)).not.toBe(true); + const comparison = parseEvidence(compared.structuredContent); + expect(comparison.normalized_result).toMatchObject({ status: "unchanged" }); + const selectors = ["overall", "pseudocode", "assembly"] as const; + expect(await verify(call, comparison.evidence_id, selectors)).toMatchObject( + { + status: "pass", + summary: { total: 3, passed: 3, unknown: 0 }, + }, + ); + + const probe = { + operation: "analyze_function", + rationale: "Check the unresolved pseudocode condition.", + }; + const recorded = await call("record_unknown", { + question: "Does the compared implementation preserve the condition?", + severity: "high", + domain: "function-comparison", + supporting_evidence_ids: [comparison.evidence_id], + contradicting_evidence_ids: [], + required_authority: null, + required_confidence: "derived", + required_environment: null, + recommended_probes: [probe], + relationships: [], + comparison_conclusion_scope: { + comparison_evidence_id: comparison.evidence_id, + dimensions: [dimension], + }, + }); + expect(recorded.isError, JSON.stringify(recorded)).not.toBe(true); + const unknown = toolContract("record_unknown").outputSchema.parse( + recorded.structuredContent, + ).result; + const aggregate = await verify(call, comparison.evidence_id, ["overall"]); + expect(aggregate).toMatchObject({ + status: "unknown", + claims: { + items: [ + { observed_status: "unchanged", unknown_ids: [unknown.unknown_id] }, + ], + }, + recommended_probes: [ + { ...probe, claim_ids: ["overall"], unknown_ids: [unknown.unknown_id] }, + ], + }); + const selected = await verify(call, comparison.evidence_id, selectors); + expect(selected.claims.items).toEqual( + expect.arrayContaining([ + expect.objectContaining({ + claim_id: "assembly", + status: "pass", + unknown_ids: [], + }), + expect.objectContaining({ + claim_id: "pseudocode", + status: dimension === "pseudocode" ? "unknown" : "pass", + unknown_ids: dimension === "pseudocode" ? [unknown.unknown_id] : [], + }), + ]), + ); + + const resolved = await call("update_unknown", { + unknown_id: unknown.unknown_id, + expected_revision: unknown.revision, + status: "resolved", + severity: unknown.severity, + supporting_evidence_ids: unknown.supporting_evidence_ids, + contradicting_evidence_ids: unknown.contradicting_evidence_ids, + required_authority: unknown.required_authority, + required_confidence: unknown.required_confidence, + required_environment: unknown.required_environment, + recommended_probes: unknown.recommended_probes, + relationships: unknown.relationships, + resolution: { + disposition: "withdrawn", + rationale: "Question explicitly withdrawn for this control.", + evidence_ids: [], + }, + }); + expect(resolved.isError, JSON.stringify(resolved)).not.toBe(true); + expect( + await verify(call, comparison.evidence_id, ["overall"]), + ).toMatchObject({ + status: "pass", + claims: { items: [{ unknown_ids: [] }] }, + }); + const exported = await call("get_evidence_bundle", { detail: "complete" }); + const bundle = toolContract("get_evidence_bundle").outputSchema.parse( + exported.structuredContent, + ).result; + for (const source of [left, right, comparison]) + expect( + bundle.records.find( + ({ evidence_id }) => evidence_id === source.evidence_id, + ), + ).toEqual(source); + }, +);