morluto/rea

Fork 0

mirror of https://github.com/morluto/rea.git synced 2026-11-05 06:45:22 +00:00

[GH-ISSUE #6879] [Bug] Overall reconstruction verification ignores active unknowns scoped to a function dimension #4214

New issue

Closed

opened 2026-10-31 00:47:47 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

2026-10-31 00:47:47 +00:00

Owner

Originally created by @coygeek on GitHub (Oct 23, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/6879

Before submitting

I searched the open and closed issues for a related report.
I removed credentials, tokens, private paths, and sensitive target data.

Area

Evidence, artifacts, or reconstruction

Observed behavior

An overall structural-function claim returns pass with no unknown IDs even when its comparison has an open residual unknown scoped to pseudocode. A pseudocode claim on the same authenticated bundle returns unknown and cites that unknown. When only the overall claim is declared, the entire verification result is pass.

The probe executed the production verifyReconstruction domain boundary, created the comparison with the production comparator, and registered the unknown through InvestigationRecords.recordUnknown. No target binary, provider, CLI process, or MCP transport executed. The MCP handler obtains the session bundle and calls this same verifier; that reachability is source-derived, not an observed MCP run.

Reproduction

With this checkout's locked dependencies available, save the following as scoped-unknown-probe.mjs in a disposable directory. From the checkout root, with the pinned Node executable on PATH, run node --import "$PWD/node_modules/tsx/dist/loader.mjs" /tmp/scoped-unknown-probe.mjs (replace the final path with the saved file's path). It writes synthetic bundles and results beside itself. The imported public contract example supplies one complete function dossier; the second dossier has identical content and a distinct synthetic artifact digest.

import { pathToFileURL } from 'node:url';
import { resolve } from 'node:path';
import { writeFileSync } from 'node:fs';
const load=p=>import(pathToFileURL(resolve(p)).href);
const { createEvidence }=await load('src/domain/evidence.ts');
const { FUNCTION_COMPARISON_EXAMPLE }=await load('src/contracts/functionComparisonExample.ts');
const { parseFunctionEvidence }=await load('src/domain/functionDossierEvidence.ts');
const { compareFunctions }=await load('src/domain/functionComparison.ts');
const { FUNCTION_COMPARISON_PROVIDER }=await load('src/domain/comparisonEvidenceIdentity.ts');
const { InvestigationRecords }=await load('src/application/investigation/InvestigationRecords.ts');
const { verifyReconstruction }=await load('src/domain/reconstructionVerification.ts');
const left=FUNCTION_COMPARISON_EXAMPLE.left;
const right=createEvidence({path:'/tmp/function-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 snapshot=e=>{const r=parseFunctionEvidence(e,{operation:'compare_functions',path:[]});if(!r.ok)throw r.error;return r.value;};
const comparison=createEvidence(undefined,FUNCTION_COMPARISON_PROVIDER,{predicateType:'rea.function-comparison',operation:'compare_functions',parameters:{left_evidence_id:left.evidence_id,right_evidence_id:right.evidence_id},result:compareFunctions(snapshot(left),snapshot(right)),confidence:'derived',authority:'analyst-inference',evidenceLinks:[left.evidence_id,right.evidence_id]});
for(const scope of [null,['pseudocode'],['overall']]){
 const records=new InvestigationRecords();for(const e of [left,right,comparison]){const r=records.recordEvidence(e);if(!r.ok)throw r.error;}
 if(scope){const r=records.recordUnknown({question:'Does the compared pseudocode preserve the documented edge case?',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:[],relationships:[],comparison_conclusion_scope:{comparison_evidence_id:comparison.evidence_id,dimensions:scope}});if(!r.ok)throw r.error;}
 const bundle=records.exportEvidenceBundle();
 const specification={name:'Reconstruction',claims:['overall','pseudocode','assembly'].map(dimension=>({kind:'structural-function',claim_id:dimension,title:dimension,comparison_evidence_id:comparison.evidence_id,dimension}))};
 const result=verifyReconstruction(specification,bundle);
 const overallOnly=verifyReconstruction({...specification,claims:specification.claims.filter(c=>c.dimension==='overall')},bundle);
 const label=scope?.[0]??'none';
 writeFileSync(new URL('scope-'+label+'.json',import.meta.url),JSON.stringify({specification,bundle,result,overallOnly},null,2));
 console.log(JSON.stringify({scope,comparisonStatus:comparison.normalized_result.status,unknowns:bundle.unknowns.length,claims:result.claims.items.map(c=>({id:c.claim_id,status:c.status,unknowns:c.unknown_ids.length})),status:result.status,overallOnlyStatus:overallOnly.status}));
}

The final script ran once. It compares no unknown, a pseudocode-scoped unknown, and an explicitly overall-scoped unknown, checking both independent dimension claims and an overall-only specification.

Expected behavior

The overall claim should stay unknown while an active unknown affects one of the function dimensions aggregated by that comparison. It should cite the scoped unknown and retain a recommended probe. The independent assembly claim can remain pass; the no-unknown control should also remain pass.

The public verification contract promises that unresolved evidence stays unknown. The overall function observation uses the comparison's aggregate status over its dimensions. Passing that aggregate while one of its constituent dimensions has an acknowledged unresolved question contradicts that contract.

Impact and scope

A caller choosing the supported overall selector can obtain a clean reconstruction verification result despite a retained material question about a constituent function dimension. The specific-dimension selector exposes the same uncertainty. The sample establishes false closure for one unchanged synthetic function comparison; it does not establish real-provider behavior or downstream incidents.

Observed workaround: also declare the affected pseudocode claim. The same bundle then returns overall verification status unknown because that claim remains unknown, while the unrelated assembly claim stays pass. Alternatively, the executed explicitly-overall-scoped control blocks the aggregate claim, but changing the unknown's scope is not necessary to preserve the original question.

REA version

rea-agents package version 6.7.0; fixed main source SHA 3e7e102a518b9112a2a8aa0590ae6f6951fd0635. The source checkout, not installed REA, was tested.

Runtime and platform

Node.js v24.22.1; Linux x86_64; the clone's locked TSX loader and dependencies. No native analysis provider was involved.

Target and artifact context

Two synthetic function Evidence records with complete declared facet and relationship coverage, one unchanged derived comparison, and one analyst-authored residual unknown. Artifact paths and digest strings are inert fixture values; no target file was opened or executed.

Interface

Other

Earliest failure stage

Native analysis or reconstruction

Relevant output or evidence

Actual final-probe stdout:

{"scope":null,"comparisonStatus":"unchanged","unknowns":0,"claims":[{"id":"assembly","status":"pass","unknowns":0},{"id":"overall","status":"pass","unknowns":0},{"id":"pseudocode","status":"pass","unknowns":0}],"status":"pass","overallOnlyStatus":"pass"}
{"scope":["pseudocode"],"comparisonStatus":"unchanged","unknowns":1,"claims":[{"id":"assembly","status":"pass","unknowns":0},{"id":"overall","status":"pass","unknowns":0},{"id":"pseudocode","status":"unknown","unknowns":1}],"status":"unknown","overallOnlyStatus":"pass"}
{"scope":["overall"],"comparisonStatus":"unchanged","unknowns":1,"claims":[{"id":"assembly","status":"pass","unknowns":0},{"id":"overall","status":"unknown","unknowns":1},{"id":"pseudocode","status":"pass","unknowns":0}],"status":"unknown","overallOnlyStatus":"unknown"}

Evidence provenance: observed. Local verification: reproduced. Reproduction completeness: complete. In the middle row the all-claims specification is unknown solely because its pseudocode claim is unknown, but the same bundle's overall-only specification passes.

Source: unknown selection requires an exact dimension match, while claim evaluation passes the literal overall selector. It therefore excludes an unknown scoped only to pseudocode before classification.

Typed outcome or recovery expected

For the pseudocode-scoped bundle, the overall-only result should be unknown, include the active unknown ID, and recommend a probe. Retain pass without unknowns, unknown for the explicitly scoped pseudocode claim, and pass for the unrelated assembly claim.

Analysis or suspected cause

Source-derived explanation: reconstructionClaimUnknowns treats overall as an ordinary exact dimension name rather than selecting unknowns affecting constituent dimensions. The unknown itself and its mutation Evidence are valid and retained; selection removes it from the overall claim.

Additional context

The scoped unknown was registered through the application record owner, and its bundle passed authentication. No implementation was changed.

Triage assessment

Impact level: P2
Assessment status: supported
Impact basis: The executed production verifier returns pass for an aggregate claim while a constituent-dimension claim on the same authenticated bundle correctly remains unknown, allowing bounded false closure.
Workaround status: available
Workaround basis: Declaring the affected pseudocode dimension alongside overall was observed to keep the full verification status unknown and preserve its unknown citation.

Originally created by @coygeek on GitHub (Oct 23, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/6879 ### Before submitting - [x] I searched the open and closed issues for a related report. - [x] I removed credentials, tokens, private paths, and sensitive target data. ### Area Evidence, artifacts, or reconstruction ### Observed behavior An `overall` structural-function claim returns `pass` with no unknown IDs even when its comparison has an open residual unknown scoped to `pseudocode`. A `pseudocode` claim on the same authenticated bundle returns `unknown` and cites that unknown. When only the overall claim is declared, the entire verification result is `pass`. The probe executed the production `verifyReconstruction` domain boundary, created the comparison with the production comparator, and registered the unknown through `InvestigationRecords.recordUnknown`. No target binary, provider, CLI process, or MCP transport executed. [The MCP handler](https://github.com/morluto/rea/blob/3e7e102a518b9112a2a8aa0590ae6f6951fd0635/src/server/registerInvestigationTools.ts#L276-L306) obtains the session bundle and calls this same verifier; that reachability is source-derived, not an observed MCP run. ### Reproduction With this checkout's locked dependencies available, save the following as `scoped-unknown-probe.mjs` in a disposable directory. From the checkout root, with the pinned Node executable on PATH, run `node --import "$PWD/node_modules/tsx/dist/loader.mjs" /tmp/scoped-unknown-probe.mjs` (replace the final path with the saved file's path). It writes synthetic bundles and results beside itself. The imported public contract example supplies one complete function dossier; the second dossier has identical content and a distinct synthetic artifact digest. ```js import { pathToFileURL } from 'node:url'; import { resolve } from 'node:path'; import { writeFileSync } from 'node:fs'; const load=p=>import(pathToFileURL(resolve(p)).href); const { createEvidence }=await load('src/domain/evidence.ts'); const { FUNCTION_COMPARISON_EXAMPLE }=await load('src/contracts/functionComparisonExample.ts'); const { parseFunctionEvidence }=await load('src/domain/functionDossierEvidence.ts'); const { compareFunctions }=await load('src/domain/functionComparison.ts'); const { FUNCTION_COMPARISON_PROVIDER }=await load('src/domain/comparisonEvidenceIdentity.ts'); const { InvestigationRecords }=await load('src/application/investigation/InvestigationRecords.ts'); const { verifyReconstruction }=await load('src/domain/reconstructionVerification.ts'); const left=FUNCTION_COMPARISON_EXAMPLE.left; const right=createEvidence({path:'/tmp/function-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 snapshot=e=>{const r=parseFunctionEvidence(e,{operation:'compare_functions',path:[]});if(!r.ok)throw r.error;return r.value;}; const comparison=createEvidence(undefined,FUNCTION_COMPARISON_PROVIDER,{predicateType:'rea.function-comparison',operation:'compare_functions',parameters:{left_evidence_id:left.evidence_id,right_evidence_id:right.evidence_id},result:compareFunctions(snapshot(left),snapshot(right)),confidence:'derived',authority:'analyst-inference',evidenceLinks:[left.evidence_id,right.evidence_id]}); for(const scope of [null,['pseudocode'],['overall']]){ const records=new InvestigationRecords();for(const e of [left,right,comparison]){const r=records.recordEvidence(e);if(!r.ok)throw r.error;} if(scope){const r=records.recordUnknown({question:'Does the compared pseudocode preserve the documented edge case?',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:[],relationships:[],comparison_conclusion_scope:{comparison_evidence_id:comparison.evidence_id,dimensions:scope}});if(!r.ok)throw r.error;} const bundle=records.exportEvidenceBundle(); const specification={name:'Reconstruction',claims:['overall','pseudocode','assembly'].map(dimension=>({kind:'structural-function',claim_id:dimension,title:dimension,comparison_evidence_id:comparison.evidence_id,dimension}))}; const result=verifyReconstruction(specification,bundle); const overallOnly=verifyReconstruction({...specification,claims:specification.claims.filter(c=>c.dimension==='overall')},bundle); const label=scope?.[0]??'none'; writeFileSync(new URL('scope-'+label+'.json',import.meta.url),JSON.stringify({specification,bundle,result,overallOnly},null,2)); console.log(JSON.stringify({scope,comparisonStatus:comparison.normalized_result.status,unknowns:bundle.unknowns.length,claims:result.claims.items.map(c=>({id:c.claim_id,status:c.status,unknowns:c.unknown_ids.length})),status:result.status,overallOnlyStatus:overallOnly.status})); } ``` The final script ran once. It compares no unknown, a `pseudocode`-scoped unknown, and an explicitly `overall`-scoped unknown, checking both independent dimension claims and an overall-only specification. ### Expected behavior The overall claim should stay `unknown` while an active unknown affects one of the function dimensions aggregated by that comparison. It should cite the scoped unknown and retain a recommended probe. The independent `assembly` claim can remain `pass`; the no-unknown control should also remain `pass`. The [public verification contract](https://github.com/morluto/rea/blob/3e7e102a518b9112a2a8aa0590ae6f6951fd0635/src/contracts/sessionToolContracts.ts#L141-L144) promises that unresolved evidence stays unknown. The [overall function observation](https://github.com/morluto/rea/blob/3e7e102a518b9112a2a8aa0590ae6f6951fd0635/src/domain/reconstructionVerification.ts#L310-L325) uses the comparison's aggregate status over its dimensions. Passing that aggregate while one of its constituent dimensions has an acknowledged unresolved question contradicts that contract. ### Impact and scope A caller choosing the supported overall selector can obtain a clean reconstruction verification result despite a retained material question about a constituent function dimension. The specific-dimension selector exposes the same uncertainty. The sample establishes false closure for one unchanged synthetic function comparison; it does not establish real-provider behavior or downstream incidents. Observed workaround: also declare the affected `pseudocode` claim. The same bundle then returns overall verification status `unknown` because that claim remains unknown, while the unrelated assembly claim stays pass. Alternatively, the executed explicitly-overall-scoped control blocks the aggregate claim, but changing the unknown's scope is not necessary to preserve the original question. ### REA version `rea-agents` package version `6.7.0`; fixed main source SHA `3e7e102a518b9112a2a8aa0590ae6f6951fd0635`. The source checkout, not installed REA, was tested. ### Runtime and platform Node.js `v24.22.1`; Linux x86_64; the clone's locked TSX loader and dependencies. No native analysis provider was involved. ### Target and artifact context Two synthetic function Evidence records with complete declared facet and relationship coverage, one unchanged derived comparison, and one analyst-authored residual unknown. Artifact paths and digest strings are inert fixture values; no target file was opened or executed. ### Interface Other ### Earliest failure stage Native analysis or reconstruction ### Relevant output or evidence Actual final-probe stdout: ```jsonl {"scope":null,"comparisonStatus":"unchanged","unknowns":0,"claims":[{"id":"assembly","status":"pass","unknowns":0},{"id":"overall","status":"pass","unknowns":0},{"id":"pseudocode","status":"pass","unknowns":0}],"status":"pass","overallOnlyStatus":"pass"} {"scope":["pseudocode"],"comparisonStatus":"unchanged","unknowns":1,"claims":[{"id":"assembly","status":"pass","unknowns":0},{"id":"overall","status":"pass","unknowns":0},{"id":"pseudocode","status":"unknown","unknowns":1}],"status":"unknown","overallOnlyStatus":"pass"} {"scope":["overall"],"comparisonStatus":"unchanged","unknowns":1,"claims":[{"id":"assembly","status":"pass","unknowns":0},{"id":"overall","status":"unknown","unknowns":1},{"id":"pseudocode","status":"pass","unknowns":0}],"status":"unknown","overallOnlyStatus":"unknown"} ``` Evidence provenance: observed. Local verification: reproduced. Reproduction completeness: complete. In the middle row the all-claims specification is unknown solely because its pseudocode claim is unknown, but the same bundle's overall-only specification passes. Source: [unknown selection](https://github.com/morluto/rea/blob/3e7e102a518b9112a2a8aa0590ae6f6951fd0635/src/domain/reconstructionUnknowns.ts#L26-L42) requires an exact dimension match, while [claim evaluation](https://github.com/morluto/rea/blob/3e7e102a518b9112a2a8aa0590ae6f6951fd0635/src/domain/reconstructionVerification.ts#L161-L168) passes the literal `overall` selector. It therefore excludes an unknown scoped only to `pseudocode` before classification. ### Typed outcome or recovery expected For the pseudocode-scoped bundle, the overall-only result should be `unknown`, include the active unknown ID, and recommend a probe. Retain `pass` without unknowns, `unknown` for the explicitly scoped pseudocode claim, and `pass` for the unrelated assembly claim. ### Analysis or suspected cause Source-derived explanation: `reconstructionClaimUnknowns` treats overall as an ordinary exact dimension name rather than selecting unknowns affecting constituent dimensions. The unknown itself and its mutation Evidence are valid and retained; selection removes it from the overall claim. ### Additional context The scoped unknown was registered through the application record owner, and its bundle passed authentication. No implementation was changed. ## Triage assessment - Impact level: P2 - Assessment status: supported - Impact basis: The executed production verifier returns pass for an aggregate claim while a constituent-dimension claim on the same authenticated bundle correctly remains unknown, allowing bounded false closure. - Workaround status: available - Workaround basis: Declaring the affected pseudocode dimension alongside overall was observed to keep the full verification status unknown and preserve its unknown citation.

bsakaguchi closed this issue

2026-10-31 00:47:47 +00:00

bsakaguchi referenced this issue

2026-10-31 01:12:04 +00:00

[PR #4214] [CLOSED] fix(artifacts): reject directory targets for source maps (#4212) #6127

bsakaguchi referenced this issue

2026-11-01 21:11:07 +00:00

[GH-ISSUE #5654] [Tracker] Open PRs that can't merge yet: conflicts and red CI (October 2026) #3425