[GH-ISSUE #2222] [Bug] compare_functions treats incomplete call coverage as unchanged #741

New issue

Closed

opened 2026-10-15 18:27:51 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

2026-10-15 18:27:51 +00:00

Owner

Originally created by @dakjdakd on GitHub (Oct 12, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/2222

The problem

compare_functions can report that two functions have unchanged calls even when one of the source observations explicitly says that its call relationships are unknown or only partially covered. It also ignores call sites recorded in unresolved_calls. An equal list of resolved callers and callees therefore becomes an equality claim without the coverage needed to support that claim.

This is especially misleading for empty lists. A provider that cannot observe a call graph may return no resolved callers or callees and retain an explanation in relationship_coverage. Comparing that observation with another empty list currently produces calls.status = "unchanged". If the other seven comparison dimensions match, the overall comparison is also unchanged.

The effect reaches reconstruction verification. A finite structural-function claim with dimension: "calls" can pass using that comparison, even though the underlying source does not establish an equal call set. The same problem applies to an overall unchanged claim. A valid Evidence digest authenticates the observation and its provenance; it does not turn its unknown or partial coverage into proof of equality.

The implementation is available in the accompanying draft pull request.

Environment and affected boundary

Field	Observed context
Affected source revision	`e4d3e1399d9cd4932653e7015a1bf8589e56029d` (`origin/main` before the fix).
Validated fix revision	`f2c956e2b34f133537969250746a1df3f2854d97`.
Development runtime	Node.js 24.18.0 and npm 11.16.0 on Windows.
Product area	Function Evidence comparison and finite reconstruction verification; related IDA dossier coverage aggregation.
Public interface	MCP `compare_functions` followed by `verify_reconstruction`, using complete inline Evidence and retained session records.
Earliest affected stage	The calls projection discards recorded coverage before comparing resolved collections. The related producer path overwrites caller coverage while assembling an IDA dossier.
Provider evidence used locally	Recorded IDA replies at the production runner boundary; no installed IDA, Ghidra, or Hopper engine was exercised.

Smallest trigger and observable output

Use two independent, artifact-bound analyze_function Evidence records with compatible function identities and otherwise equal dossier facets. Both records have empty callers and callees. The left record explicitly reports complete coverage; the right record reports unknown coverage. The relevant source fields are:

{
  "left": {
    "operation": "analyze_function",
    "relationship_coverage": { "status": "complete" },
    "normalized_result": { "callers": [], "callees": [] }
  },
  "right": {
    "operation": "analyze_function",
    "relationship_coverage": {
      "status": "unknown",
      "reason": "Call graph unavailable."
    },
    "normalized_result": { "callers": [], "callees": [] }
  }
}

These are projections of full, authenticated Evidence records, rather than a standalone request that omits required Evidence and dossier fields. Submit the complete records to compare_functions as left and right.

Before the fix, the relevant result fields are:

{
  "status": "unchanged",
  "summary": { "unchanged": 8, "changed": 0, "unknown": 0 },
  "dimensions": [
    {
    "dimension": "calls",
    "status": "unchanged",
    "conclusion_kind": "derived_relationship",
    "left_count": 0,
    "right_count": 0,
    "limitations": []
    }
  ]
}

The snippet selects the calls element from the actual dimensions array; the other seven dimensions are omitted for readability. The expected result preserves the unresolved coverage:

{
  "status": "unknown",
  "summary": { "unchanged": 7, "changed": 0, "unknown": 1 },
  "dimensions": [
    {
    "dimension": "calls",
    "status": "unknown",
    "conclusion_kind": "unresolved_branch",
    "left_digest": null,
    "right_digest": null,
    "left_count": 0,
    "right_count": 0,
    "limitations": ["Right: Call graph unavailable."]
    }
  ]
}

The source Evidence links remain attached to the dimension. The unknown dimension is also present in changes, and the MCP workflow retains an open function-comparison unknown backed by both source observations.

For a single calls claim against this pair, the relevant verification output must change from:

{
  "status": "pass",
  "summary": { "total": 1, "passed": 1, "failed": 0, "unknown": 0 },
  "claims": { "items": [{ "dimension": "calls", "status": "pass", "observed_status": "unchanged" }] }
}

to:

{
  "status": "unknown",
  "summary": { "total": 1, "passed": 0, "failed": 0, "unknown": 1 },
  "claims": { "items": [{ "dimension": "calls", "status": "unknown", "observed_status": "unknown" }] }
}

These verification examples are also selected-field projections. Full results retain the comparison ID, exact left and right Evidence IDs, source links, unknown IDs, and diagnostics.

Why this happens

The defect is in the interpretation of source facts, rather than MCP transport or Evidence serialization. On the affected base, compareCalls builds a projection containing only each caller or callee's direction and name. It checks address-derived names and then compares the sorted projections. Neither the Evidence envelope's relationship_coverage nor the dossier's unresolved_calls participates in that decision.

verifyReconstruction validates the comparison identity, source closure, source kinds, and qualifying authority. It then reads the retained comparison status. Before this correction, it has no source-level calls coverage check for an older, valid comparison record that says unchanged.

There is a related producer defect in IdaOperationRunner.dossier. The dossier reads callers and then callees through a shared mutable relationshipCoverage property. Modern caller reads correctly report that direct callers are unknown because upstream xrefs do not establish direct call relationships. The subsequent callee read can overwrite that state with complete. It can also replace the caller explanation with a callee-only partial state. The final dossier Evidence then loses the uncertainty of one half of the relationship set.

This violates the existing tool design contract: missing coverage remains unknown, provider-observed direct relationships must remain distinct from unresolved edges, and completeness cannot be inferred from an empty result.

Required semantics

Coverage applies to the provider-observed direct relationship set. complete means that set was returned without a known read limit; it does not prove every possible runtime edge.

Source fact	Required comparison behavior
`relationship_coverage` is absent in historical input or parsed as `null`	Accept the Evidence, but keep calls unknown with a missing-coverage explanation.
Coverage is `unknown`	Keep calls unknown and retain the provider's reason and any diagnostics.
Coverage is `partial`	Keep calls unknown and retain the explicit limitations and any diagnostics.
`unresolved_calls` contains recorded call sites	Keep calls unknown even when the resolved relationship set has complete coverage; retain each address and reason.
Both sources have complete coverage and no recorded unresolved sites	Compare the observed collections using the existing stable-name and ordering rules.
Complete coverage includes execution caveats or diagnostics	Do not infer incomplete relationship coverage from those caveats alone.

An older dossier may omit unresolved_calls; the repair should not invent a new required dossier field or claim that omission records an explicit empty unresolved-site list. Explicit complete relationship coverage can still support comparison of the observed set. Conversely, omitted coverage must not silently become complete.

The same interpretation should have one owner shared by comparison and reconstruction verification. A previously retained comparison with a valid digest and observed_status: "unchanged" must remain usable, but an incomplete source must prevent calls or overall equality claims from passing. The verifier should preserve that old observed status and explain why the claim is now unknown, rather than rewriting the historical Evidence.

An already confirmed overall changed result must remain a counterexample. For example, an independently observed assembly difference should still fail an overall claim even if source call coverage is unknown. Calls-specific claims still require comparable call coverage. Other finite dimensions, such as pseudocode, should not become unknown merely because the specification did not ask them to prove call equality.

Regression coverage and verification scope

The fix has been exercised through domain semantics, the production IDA runner with recorded provider replies, and public MCP comparison/verification calls. The focused command completed with 7 suites and 144 passing tests:

npm run test:focused -- src/domain/functionComparison.test.ts src/domain/reconstructionVerification.functionSources.test.ts src/domain/reconstructionVerification.test.ts tests/boundary/mcp/functionComparisonMcp.test.ts tests/boundary/mcp/comparisonUnknownsMcp.test.ts src/ida/IdaOperationRunner.test.ts src/ida/IdaCallGraph.test.ts

The meaningful regressions cover missing, unknown, and partial coverage on either comparison side; equal empty collections; recorded unresolved call sites alongside resolved callees; complete observations with execution caveats; MCP source retention and residual unknowns; older unchanged comparisons used for calls and overall verification; preservation of unrelated finite-dimension claims; preservation of a confirmed overall changed counterexample; and IDA aggregation when a later callee reply is complete or partial.

The comparison regressions would fail on the affected source because the empty projections are equal. The legacy verification regressions would pass incorrectly on the affected source. The recorded IDA regressions would expose the caller state being overwritten by the callee state.

Static, documentation, and discovery validation is recorded in the corresponding PR. This local run does not establish behavior of installed Hopper, Ghidra, or IDA engines. Real-provider and full Windows native session coverage remain outside the recorded-provider and MCP boundary evidence described here.

Originally created by @dakjdakd on GitHub (Oct 12, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/2222 ## The problem `compare_functions` can report that two functions have unchanged calls even when one of the source observations explicitly says that its call relationships are unknown or only partially covered. It also ignores call sites recorded in `unresolved_calls`. An equal list of resolved callers and callees therefore becomes an equality claim without the coverage needed to support that claim. This is especially misleading for empty lists. A provider that cannot observe a call graph may return no resolved callers or callees and retain an explanation in `relationship_coverage`. Comparing that observation with another empty list currently produces `calls.status = "unchanged"`. If the other seven comparison dimensions match, the overall comparison is also `unchanged`. The effect reaches reconstruction verification. A finite `structural-function` claim with `dimension: "calls"` can pass using that comparison, even though the underlying source does not establish an equal call set. The same problem applies to an overall unchanged claim. A valid Evidence digest authenticates the observation and its provenance; it does not turn its unknown or partial coverage into proof of equality. The implementation is available in the accompanying [draft pull request](https://github.com/morluto/rea/pull/2223). ## Environment and affected boundary | Field | Observed context | | --- | --- | | Affected source revision | `e4d3e1399d9cd4932653e7015a1bf8589e56029d` (`origin/main` before the fix). | | Validated fix revision | `f2c956e2b34f133537969250746a1df3f2854d97`. | | Development runtime | Node.js 24.18.0 and npm 11.16.0 on Windows. | | Product area | Function Evidence comparison and finite reconstruction verification; related IDA dossier coverage aggregation. | | Public interface | MCP `compare_functions` followed by `verify_reconstruction`, using complete inline Evidence and retained session records. | | Earliest affected stage | The calls projection discards recorded coverage before comparing resolved collections. The related producer path overwrites caller coverage while assembling an IDA dossier. | | Provider evidence used locally | Recorded IDA replies at the production runner boundary; no installed IDA, Ghidra, or Hopper engine was exercised. | ## Smallest trigger and observable output Use two independent, artifact-bound `analyze_function` Evidence records with compatible function identities and otherwise equal dossier facets. Both records have empty `callers` and `callees`. The left record explicitly reports complete coverage; the right record reports unknown coverage. The relevant source fields are: ```json { "left": { "operation": "analyze_function", "relationship_coverage": { "status": "complete" }, "normalized_result": { "callers": [], "callees": [] } }, "right": { "operation": "analyze_function", "relationship_coverage": { "status": "unknown", "reason": "Call graph unavailable." }, "normalized_result": { "callers": [], "callees": [] } } } ``` These are projections of full, authenticated Evidence records, rather than a standalone request that omits required Evidence and dossier fields. Submit the complete records to `compare_functions` as `left` and `right`. Before the fix, the relevant result fields are: ```json { "status": "unchanged", "summary": { "unchanged": 8, "changed": 0, "unknown": 0 }, "dimensions": [ { "dimension": "calls", "status": "unchanged", "conclusion_kind": "derived_relationship", "left_count": 0, "right_count": 0, "limitations": [] } ] } ``` The snippet selects the calls element from the actual `dimensions` array; the other seven dimensions are omitted for readability. The expected result preserves the unresolved coverage: ```json { "status": "unknown", "summary": { "unchanged": 7, "changed": 0, "unknown": 1 }, "dimensions": [ { "dimension": "calls", "status": "unknown", "conclusion_kind": "unresolved_branch", "left_digest": null, "right_digest": null, "left_count": 0, "right_count": 0, "limitations": ["Right: Call graph unavailable."] } ] } ``` The source Evidence links remain attached to the dimension. The unknown dimension is also present in `changes`, and the MCP workflow retains an open `function-comparison` unknown backed by both source observations. For a single calls claim against this pair, the relevant verification output must change from: ```json { "status": "pass", "summary": { "total": 1, "passed": 1, "failed": 0, "unknown": 0 }, "claims": { "items": [{ "dimension": "calls", "status": "pass", "observed_status": "unchanged" }] } } ``` to: ```json { "status": "unknown", "summary": { "total": 1, "passed": 0, "failed": 0, "unknown": 1 }, "claims": { "items": [{ "dimension": "calls", "status": "unknown", "observed_status": "unknown" }] } } ``` These verification examples are also selected-field projections. Full results retain the comparison ID, exact left and right Evidence IDs, source links, unknown IDs, and diagnostics. ## Why this happens The defect is in the interpretation of source facts, rather than MCP transport or Evidence serialization. On the affected base, [`compareCalls`](https://github.com/morluto/rea/blob/e4d3e1399d9cd4932653e7015a1bf8589e56029d/src/domain/functionComparisonDimensions.ts) builds a projection containing only each caller or callee's direction and name. It checks address-derived names and then compares the sorted projections. Neither the Evidence envelope's `relationship_coverage` nor the dossier's `unresolved_calls` participates in that decision. [`verifyReconstruction`](https://github.com/morluto/rea/blob/e4d3e1399d9cd4932653e7015a1bf8589e56029d/src/domain/reconstructionVerification.ts) validates the comparison identity, source closure, source kinds, and qualifying authority. It then reads the retained comparison status. Before this correction, it has no source-level calls coverage check for an older, valid comparison record that says `unchanged`. There is a related producer defect in [`IdaOperationRunner.dossier`](https://github.com/morluto/rea/blob/e4d3e1399d9cd4932653e7015a1bf8589e56029d/src/ida/IdaOperationRunner.ts). The dossier reads callers and then callees through a shared mutable `relationshipCoverage` property. Modern caller reads correctly report that direct callers are unknown because upstream xrefs do not establish direct call relationships. The subsequent callee read can overwrite that state with `complete`. It can also replace the caller explanation with a callee-only partial state. The final dossier Evidence then loses the uncertainty of one half of the relationship set. This violates the existing [tool design contract](https://github.com/morluto/rea/blob/e4d3e1399d9cd4932653e7015a1bf8589e56029d/docs/tool-design.md): missing coverage remains unknown, provider-observed direct relationships must remain distinct from unresolved edges, and completeness cannot be inferred from an empty result. ## Required semantics Coverage applies to the provider-observed direct relationship set. `complete` means that set was returned without a known read limit; it does not prove every possible runtime edge. | Source fact | Required comparison behavior | | --- | --- | | `relationship_coverage` is absent in historical input or parsed as `null` | Accept the Evidence, but keep calls unknown with a missing-coverage explanation. | | Coverage is `unknown` | Keep calls unknown and retain the provider's reason and any diagnostics. | | Coverage is `partial` | Keep calls unknown and retain the explicit limitations and any diagnostics. | | `unresolved_calls` contains recorded call sites | Keep calls unknown even when the resolved relationship set has complete coverage; retain each address and reason. | | Both sources have complete coverage and no recorded unresolved sites | Compare the observed collections using the existing stable-name and ordering rules. | | Complete coverage includes execution caveats or diagnostics | Do not infer incomplete relationship coverage from those caveats alone. | An older dossier may omit `unresolved_calls`; the repair should not invent a new required dossier field or claim that omission records an explicit empty unresolved-site list. Explicit complete relationship coverage can still support comparison of the observed set. Conversely, omitted coverage must not silently become complete. The same interpretation should have one owner shared by comparison and reconstruction verification. A previously retained comparison with a valid digest and `observed_status: "unchanged"` must remain usable, but an incomplete source must prevent calls or overall equality claims from passing. The verifier should preserve that old observed status and explain why the claim is now unknown, rather than rewriting the historical Evidence. An already confirmed overall `changed` result must remain a counterexample. For example, an independently observed assembly difference should still fail an overall claim even if source call coverage is unknown. Calls-specific claims still require comparable call coverage. Other finite dimensions, such as pseudocode, should not become unknown merely because the specification did not ask them to prove call equality. ## Regression coverage and verification scope The fix has been exercised through domain semantics, the production IDA runner with recorded provider replies, and public MCP comparison/verification calls. The focused command completed with **7 suites and 144 passing tests**: ```sh npm run test:focused -- src/domain/functionComparison.test.ts src/domain/reconstructionVerification.functionSources.test.ts src/domain/reconstructionVerification.test.ts tests/boundary/mcp/functionComparisonMcp.test.ts tests/boundary/mcp/comparisonUnknownsMcp.test.ts src/ida/IdaOperationRunner.test.ts src/ida/IdaCallGraph.test.ts ``` The meaningful regressions cover missing, unknown, and partial coverage on either comparison side; equal empty collections; recorded unresolved call sites alongside resolved callees; complete observations with execution caveats; MCP source retention and residual unknowns; older unchanged comparisons used for calls and overall verification; preservation of unrelated finite-dimension claims; preservation of a confirmed overall changed counterexample; and IDA aggregation when a later callee reply is complete or partial. The comparison regressions would fail on the affected source because the empty projections are equal. The legacy verification regressions would pass incorrectly on the affected source. The recorded IDA regressions would expose the caller state being overwritten by the callee state. Static, documentation, and discovery validation is recorded in the corresponding PR. This local run does not establish behavior of installed Hopper, Ghidra, or IDA engines. Real-provider and full Windows native session coverage remain outside the recorded-provider and MCP boundary evidence described here.

bsakaguchi

2026-10-15 18:27:51 +00:00