morluto/rea

Fork 0

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

[PR #1672] [CLOSED] feat(ghidra): surface instruction-backed prototype conflicts #4743

New issue

Closed

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

bsakaguchi commented

2026-10-31 00:54:35 +00:00

Owner

📋 Pull Request Information

Original PR: https://github.com/morluto/rea/pull/1672
Author: @Y0UW1SH
Created: 10/11/2026
Status: ❌ Closed

Base: main ← Head: feat/native-prototype-diagnostics-1244

📝 Commits (10+)

bc72044 feat(ghidra): surface instruction-backed prototype conflicts
5b6c3e0 fix(ghidra): preserve signature provenance in prototype diagnostics
3fac376 fix(ghidra): exclude caller zeroing from prototype evidence
cfaea3a fix(ghidra): retain prototype verifier resources after failed cleanup
fc01c24 fix(ghidra): resolve prototype diagnostic review findings
ed0d95a style(ghidra): format prototype review follow-up
f39ab0c fix(ghidra): bound prototype probes and preserve caller fact semantics
088381b fix(ghidra): keep controls executable and retained diagnostic provenance truthful
e1ae40c chore: merge main into PR 1672
ea67a33 fix(ghidra): bound prototype cleanup diagnostics

📊 Changes

25 files changed (+2729 additions, -40 deletions)

View changed files

📝 bridge/ghidra/ReaGhidraBridge.java (+5 -0)
➕ bridge/ghidra/ReaGhidraPrototypeDiagnostics.java (+434 -0)
📝 docs/ghidra-provider.md (+40 -1)
📝 docs/testing.md (+1 -0)
📝 package.json (+2 -0)
➕ scripts/verify-ghidra-prototype-diagnostics-assertions.mjs (+356 -0)
➕ scripts/verify-ghidra-prototype-diagnostics.d.mts (+28 -0)
➕ scripts/verify-ghidra-prototype-diagnostics.mjs (+447 -0)
📝 scripts/verify-real-ghidra-switch.mjs (+12 -6)
📝 scripts/verify-real-ghidra.mjs (+62 -19)
📝 src/application/native/NativeApiInspection.test.ts (+67 -2)
📝 src/application/native/NativeApiInspection.ts (+17 -1)
📝 src/domain/analysisView/analysisView.test.ts (+76 -0)
📝 src/domain/analysisView/nativeFunctionView.ts (+15 -0)
📝 src/domain/ghidraValues.fixture.ts (+4 -0)
📝 src/domain/native/nativeApiBoundary.ts (+38 -2)
📝 src/ghidra/GhidraAnalysisProfile.ts (+3 -0)
📝 src/ghidra/GhidraFunctionValues.test.ts (+97 -0)
📝 src/ghidra/GhidraFunctionValues.ts (+25 -6)
📝 tests/boundary/mcp/ghidraNativeApiMcp.test.ts (+88 -2)

...and 5 more files

📄 Description

Summary

Addresses #1244.

Native API dossiers now keep bounded x86-32 instruction diagnostics next to the recovered types, signature source and confidence.

Conflicts: stack reads and return cleanup can contradict a recovered prototype.
Observations: x87 operations and EAX forwarding stay observations, with explicit unknowns.

CLI and MCP inspection and the selected views carry these facts. Older retained Evidence remains readable.

Problem and expected behavior

#1244 reproduced two cases with real Ghidra on main. In both, a confident-looking inferred signature hides conflicting instruction evidence:

0x406400 has a no-argument signature, but its instructions read the first stack argument and do x87 arithmetic before a conversion helper.
0x401b10 has four inferred stdcall arguments (16 bytes), but it returns with RET 20.

Previously the analyst had to find these conflicts by reading assembly. Now analyze_function and inspect_native_api return native_api.prototype_diagnostics. Each diagnostic has:

a conflict or observation classification;
the inferred claim;
the stack-read, return, branch or call-site evidence addresses;
the residual unknowns.

prototype_check_limitations records the checks' scope and any exhausted budget, even when nothing is found. A diagnostic is not proof of a source declaration: cleanup bytes do not establish an argument count, and EAX forwarding does not establish a return type.

Change and scope

Producer (bridge/ghidra/ReaGhidraPrototypeDiagnostics.java, called from ReaGhidraBridge.java). It works from Ghidra's listing and raw p-code.
- Entry stack reads are compared with recovered parameter storage and compiler-model slots.
- Near-return cleanup is compared with explicit compiler-model cleanup or the recovered stack extent.
- Shared epilogues are followed for at most 16 simple instructions, without expanding owned-body ranges.
- EAX forwarding and x87 operations are recorded as observations.
- Entry-prefix checks stop at 256 instructions, 2,048 raw p-code operations or 256 facts. Cleanup and forwarding each keep at most 256 candidates or facts. Every budget that is reached is reported as a limitation.
Contract (src/domain/native/nativeApiBoundary.ts). It adds the diagnostic schema plus a retained-boundary variant, so Evidence written before this change still validates.
Projection (NativeApiInspection.ts, nativeFunctionView.ts). It carries diagnostics, limitations and their residual unknowns into CLI/MCP inspection and the selected native API and assembly views. Older Evidence reports "Instruction/prototype consistency was not recorded in this Evidence."
Profile (GhidraAnalysisProfile.ts). It adds prototype_consistency_evidence: bounded-x86-32-listing-pcode-v6, so earlier cached observations are not reused.
Verification. A new verify:ghidra:prototype uses source-owned ELF32 assembly controls (tests/conformance/ghidra/prototype-conflicts.S) and a producer probe. It also runs in the Linux host verifier.
Not included:
- architectures other than x86-32, which report consistency as unknown;
- interprocedural or alias propagation;
- inferring a source signature, signedness or compiler identity;
- executing target instructions.

Review fixes:

Run host toolchain preflight before allocating fixtures, and protect every later setup step with cleanup. If a launched provider cannot be retired, keep the workspace and its owner.
Confirm the MCP transport's actual close event before releasing the workspace. Keep the transport and the close observation for retries, without changing SDK negotiation or shutdown.
Check explicit compiler-model cleanup independently of custom stack-slot allocation.
Preserve unknown epilogue ownership in cleanup and EAX-forwarding observations. An unowned tail target cannot establish a prototype conflict.
Count only in-body returns and external direct branches against the cleanup budget.
Require a nonempty check scope in current Ghidra output, while keeping older retained Evidence readable.
Normalize x86-32 stack-pointer aliases modulo 2^32 for both reads and writes, which prevents false conflicts after pointer wraparound.
Distinguish natural ELF/GCC calling conventions from seeded Windows controls in the public verifier, with a separate clean caller-cleaned control.
Bound caller-reference evidence for return-register observations, and preserve unknown cleanup as unknown. Both were raised in dandgabr's review.

Follow the contribution scope.
Unresolved scope, authority, side effects, or required verification block
integration. Link the required maintainer scope decision for new providers or
capabilities involving target execution, injection, mutation, or protection
recovery; ordinary fixes within existing boundaries may state "not applicable".
Draft PRs may leave the scope decision pending and the readiness and merge checklists
unchecked. Maintainers can help resolve open questions.

Contract and boundary impact

Semantic owner and earliest changed stage: the Ghidra bridge producer. nativeApiBoundary.ts owns the schema, and NativeApiInspection.ts and nativeFunctionView.ts own the projections.
Contribution scope fit and linked maintainer decision: static analysis inside the existing Ghidra provider, for the enhancement filed in #1244. No new provider, target execution, injection, mutation or protection recovery is involved, so a separate scope decision is not applicable. A maintainer labelled the PR and marked it ready for review on 2026-10-13.
CLI and MCP/tool-catalog contract: analyze_function and inspect_native_api gain native_api.prototype_diagnostics and prototype_check_limitations. So does annotate_native_function, which returns the same dossier. Input schemas and descriptions are unchanged; output schemas grow (see Completed-task cost).
Provider, bridge, target-format, or platform compatibility: Ghidra bridge only. The checks support x86-32; other architectures report consistency as unknown.
Evidence, artifact, provenance, or reconstruction contract:
- Diagnostics are conflict or observation, and each carries residual unknowns.
- Evidence retained before this change still parses, and its missing check is reported as unknown.
- The profile revision means snapshots cached before this change are not reused.
Target selection, authority, upstream behavior, and cleanup details (if applicable): target handling is unchanged. Verifier cleanup is hardened: transport close is observed before the workspace is released, and the owner is kept on failure.
Generated metadata (docs/public/product-catalog.json), package, or installation impact: catalogs regenerate from the source contracts and are not committed. package.json adds verify:ghidra:prototype. docs/ghidra-provider.md and docs/testing.md are updated.

Expected effects (check known effects; use documentation-only on its own).
Unchecked items do not establish absence; leave uncertainties visible.

Read existing files or captured data. (The checks read the program already loaded in the caller's Ghidra session.)
Launch or attach to a process. (No new launch: the checks run inside the existing Ghidra session. The verifier still launches Ghidra and assembles its controls with GNU as/ld, as REA's other verifiers do.)
Inject instrumentation or run scripts/code. (Not applicable: target instructions never execute. The checks read Ghidra's listing and raw p-code.)
Change process memory, registers, files, or configuration. (Not applicable: executable bytes stay unchanged, and the verifier asserts this.)
Contact network services.
Recover protected code or work around protections. (Not applicable: the change reports prototype-consistency facts only.)
Documentation or usability only; no target interaction.
Not sure yet; investigation or maintainer guidance needed.

Evidence and regression coverage

Tests added or updated:
- NativeApiInspection.test.ts, analysisView.test.ts, GhidraFunctionValues.test.ts and ghidraNativeApiMcp.test.ts: diagnostics, limitations and residual unknowns through inspection, the selected views and MCP; older Evidence without the fields.
- sessionMcp.test.ts: the session workflow now inherits the shared suite timeout.
- prototypeVerifierCleanup.test.ts and prototypeVerifierTransport.test.ts: verifier setup failure, transport-close observation and retained ownership.
- verify-ghidra-prototype-diagnostics.mjs (with its assertions) and tests/conformance/ghidra/prototype-conflicts.S: 34 seeded producer controls covering conflicting and matching stack inputs and cleanup, written slots, conditional pointers, ABI padding, shared epilogues, tail calls and EAX overwrite/forwarding. CLI/MCP parity runs on natural ELF output.
Base reproduction or other evidence:
- The two #1244 cases were reproduced with real Ghidra on main.
- The Java findings and the wrapped-alias false conflicts reproduced before their fixes.
- Independent run by @CassieFox23 on Linux, Node 24.18.0 and 26.11.1, Ghidra 12.1.4: the 7 PR test files (127 tests) and the real Ghidra check (34 producer controls, then CLI and MCP) passed. For the same assembled file, main reports no prototype findings and this branch does.
User-visible CLI/MCP output (if applicable): from that independent run, inspect-native-api prototype findings per control function, main → head. CLI and MCP matched on every function.

Function main Head

Stack and x87 none 3

Cleanup conflict none 1

Cleanup control none 1

Stack control none 0

Forward return none 1

Overwrite return none 0
- The cleanup-conflict function reports one conflict: its RET cleans 20 bytes, but 16 were recovered.
- The stack and x87 function reports a stack-read conflict, an x87 observation and an EAX forwarding observation.
- On natural ELF metadata, rea_cleanup_control is also a conflict, as the assertions expect. Only the seeded Windows probe makes it a clean control.
Remaining proof gaps:
- No Windows target or host, and no macOS.
- Ghidra time and memory, and token counts on real outputs with diagnostics, are not yet measured. They have been requested; see Completed-task cost.
- The spawn-failure assertion in prototypeVerifierTransport.test.ts fails on Windows hosts; see Validation.

Function	`main`	Head
Stack and x87	none	3
Cleanup conflict	none	1
Cleanup control	none	1
Stack control	none	0
Forward return	none	1
Overwrite return	none	0

For evidence-bearing changes:

Observed, derived, and inferred claims remain distinguishable. Diagnostics are classified as conflict or observation, and each carries residual unknowns.
Artifact identity, source provenance, and failed attempts remain preserved. Signature source and confidence are unchanged, and older Evidence stays readable.
Unsupported, incomplete, unavailable, or uncertain outcomes remain visible. Unsupported architectures, exhausted budgets and unowned epilogues are reported as limitations or observations.

Completed-task cost

Per AGENTS.md "Performance". Measured locally without Ghidra, against main 633e4ff43 and this head df532779a. Tokens are cl100k_base counts (tiktoken 0.13.0) over serialized JSON, not hosted-model billing.

Measurement	`main`	Head	Change
Tool catalog, name + description + input schema (207 tools)	195,649	195,649	0
Tool catalog including output schemas	807,491	809,207	+1,716 (+0.21%)
`inspect_native_api` result, x86-32 function, no diagnostics	510	997	+487 (+95%)
Dossier `native_api` in `analyze_function`, same function	396	565	+169
`inspect_native_api` result, other architecture	510	577	+67

Catalog. Output schemas grow by about 570 tokens each for analyze_function, annotate_native_function and inspect_native_api.
Per-result rows. These use the repository dossier fixture with the producer's exact limitation strings, so they are the fixed cost every function pays before any diagnostic. Each diagnostic then adds its evidence and residual unknowns.
Where the fixed cost comes from. Three x86-32 limitation paragraphs (about 160 tokens) are emitted for every x86-32 function. inspect_native_api repeats them three times:
- in boundary.prototype_check_limitations;
- in the preserve_residual_unknowns substep;
- in residual_unknowns.
The last two copies follow the existing residual-unknown pattern. If maintainers prefer, a follow-up could emit the fixed text once per result, or as stable identifiers. This PR does not change it.
Cache. The new profile revision means snapshots cached before this change are recomputed once after upgrade.
Not yet measured. Ghidra analysis wall time, CPU and peak process-family memory, main against head, cold and warm, plus token counts on real outputs with diagnostics. This host has no Ghidra set up for REA. I've asked @CassieFox23, who already ran the real verifier, and will add the results here.

Validation performed

Windows 11 x64, Node 24.21.0. Head df532779a is 105daea5a merged with main 633e4ff43, with no conflicts.

npm run test:local -- src/application/native/NativeApiInspection.test.ts src/domain/analysisView/analysisView.test.ts src/ghidra/GhidraFunctionValues.test.ts: 115 passed.
npm run test:focused -- tests/boundary/mcp/ghidraNativeApiMcp.test.ts tests/boundary/mcp/sessionMcp.test.ts tests/process-global/prototypeVerifierCleanup.test.ts tests/process-global/prototypeVerifierTransport.test.ts: 14 passed, 4 skipped, 1 failed.
- The failure is prototypeVerifierTransport "observes transport closure when the server cannot spawn". On Windows, the MCP client reports "Connection closed" for a missing executable instead of ENOENT.
- It fails the same way on the pre-merge head 105daea5a on this host, and it passes on Linux (CI and the independent run). Making that assertion Windows-safe is a known gap.
npm run check:fast, npm run format:check, npm run docs:check, npm run mcp-catalog:check, npm run knip and npm run verify:test-discovery: all passed.
Completed-task cost: the token measurements above.

Earlier validation, before the merge with main:

CI follow-up 105daea5.
- The macOS session workflow exceeded its test-specific 10-second limit in run 38636461493, so it now inherits the existing 30-second suite deadline (60 s under coverage).
- Fresh macOS CI then passed all 225 tests, with four named skips.
- CI run 38640169972 passed all 35 jobs. The separate Go metadata, packet-capture and signal-recording workflows also passed.
Follow-up cd61a7f. 93 focused tests and npm run check passed. The actual MCP SDK/SIGKILL regression failed before the fix and passed afterward.
Ghidra producer checks.
- Ghidra 12.1.4 with JDK 21 passed all 34 seeded production-producer controls and the retained-Evidence projections.
- Six semantic checks on natural ELF/GCC output and six exploratory direct controls also passed.
- The full real-provider CLI/MCP verifier was blocked in the author's container. The independent run above completed it.

Compatibility, safety, and release

Breaking changes or migration steps: none. The new fields are additive, and Evidence retained without them still validates and reports the check as not recorded.
Real Hopper/Ghidra, browser, or OS coverage:
- Real Ghidra 12.1.4 on Linux, by the author and in the independent run.
- CI covers the Ghidra lanes.
- No Windows target or host, and no macOS Ghidra run.
Package or release metadata impact: catalogs regenerate. verify:ghidra:prototype is new.
Security, privacy, process, or containment review:
- Target instructions never execute, and executable bytes are verified unchanged.
- Producer work is bounded by the budgets above.
- The verifier keeps workspace ownership when cleanup cannot be confirmed.

Author readiness

Human owner: @Y0UW1SH

I reviewed the final diff and relevant existing code, understand the change and its edge cases, and take responsibility for the complete PR, including AI-assisted work.
I checked the evidence above, confirmed it supports the current change, and recorded meaningful validation gaps.
I declare this PR ready for initial maintainer review.

Before merge

This PR addresses a concrete problem or an agreed enhancement. (#1244, with two cases reproduced on main.)
Material scope and authority questions are resolved, and any required maintainer scope decision covers the final diff. (Static analysis inside the existing Ghidra provider, so no scope decision is required; see Contract and boundary impact.)
The PR has one focused outcome and the title follows type(scope): outcome.
Related issue is linked, or the reason for not linking one is stated above. (#1244.)
Tests cover changed observable behavior and meaningful failure paths.
Owning docs, contracts, and generated metadata are updated where needed. (docs/ghidra-provider.md, docs/testing.md and the boundary schema; catalogs are generated by CI.)
User-visible CLI/MCP changes include representative output. (Pending: per-function counts from a real Ghidra run are above, but no raw inspect-native-api JSON from a real run is included yet.)
I checked the final diff for secrets, unrelated cleanup, and unsupported claims. (25 files, all part of this change; no secrets found.)

_{🔄 This issue represents a GitHub Pull Request. It cannot be merged through Gitea due to API limitations.}

## 📋 Pull Request Information **Original PR:** https://github.com/morluto/rea/pull/1672 **Author:** [@Y0UW1SH](https://github.com/Y0UW1SH) **Created:** 10/11/2026 **Status:** ❌ Closed **Base:** `main` ← **Head:** `feat/native-prototype-diagnostics-1244` --- ### 📝 Commits (10+) - [`bc72044`](https://github.com/morluto/rea/commit/bc72044419ad77d998b83a57f05aff299ec9cc67) feat(ghidra): surface instruction-backed prototype conflicts - [`5b6c3e0`](https://github.com/morluto/rea/commit/5b6c3e091137fa675086eb4a41b8ed7317e6bed0) fix(ghidra): preserve signature provenance in prototype diagnostics - [`3fac376`](https://github.com/morluto/rea/commit/3fac37633eec3712d51600a4b3a513db76cfafd7) fix(ghidra): exclude caller zeroing from prototype evidence - [`cfaea3a`](https://github.com/morluto/rea/commit/cfaea3a501f2bbd28a44211063969c5c6f71cd72) fix(ghidra): retain prototype verifier resources after failed cleanup - [`fc01c24`](https://github.com/morluto/rea/commit/fc01c24d9df4e2734065a684cd5a10edf764d019) fix(ghidra): resolve prototype diagnostic review findings - [`ed0d95a`](https://github.com/morluto/rea/commit/ed0d95a15e149938aa734355763af2d8e8f7f13b) style(ghidra): format prototype review follow-up - [`f39ab0c`](https://github.com/morluto/rea/commit/f39ab0c4dffd77ba21ad0a2bfc7f8c62185dbe46) fix(ghidra): bound prototype probes and preserve caller fact semantics - [`088381b`](https://github.com/morluto/rea/commit/088381b011b232e6a3cf4e0f56183de7d18e1237) fix(ghidra): keep controls executable and retained diagnostic provenance truthful - [`e1ae40c`](https://github.com/morluto/rea/commit/e1ae40c6c86d812a3bfb71965ee3975d7f6577be) chore: merge main into PR 1672 - [`ea67a33`](https://github.com/morluto/rea/commit/ea67a33b840057fcfe4db4a9587a6da7d4001403) fix(ghidra): bound prototype cleanup diagnostics ### 📊 Changes **25 files changed** (+2729 additions, -40 deletions) <details> <summary>View changed files</summary> 📝 `bridge/ghidra/ReaGhidraBridge.java` (+5 -0) ➕ `bridge/ghidra/ReaGhidraPrototypeDiagnostics.java` (+434 -0) 📝 `docs/ghidra-provider.md` (+40 -1) 📝 `docs/testing.md` (+1 -0) 📝 `package.json` (+2 -0) ➕ `scripts/verify-ghidra-prototype-diagnostics-assertions.mjs` (+356 -0) ➕ `scripts/verify-ghidra-prototype-diagnostics.d.mts` (+28 -0) ➕ `scripts/verify-ghidra-prototype-diagnostics.mjs` (+447 -0) 📝 `scripts/verify-real-ghidra-switch.mjs` (+12 -6) 📝 `scripts/verify-real-ghidra.mjs` (+62 -19) 📝 `src/application/native/NativeApiInspection.test.ts` (+67 -2) 📝 `src/application/native/NativeApiInspection.ts` (+17 -1) 📝 `src/domain/analysisView/analysisView.test.ts` (+76 -0) 📝 `src/domain/analysisView/nativeFunctionView.ts` (+15 -0) 📝 `src/domain/ghidraValues.fixture.ts` (+4 -0) 📝 `src/domain/native/nativeApiBoundary.ts` (+38 -2) 📝 `src/ghidra/GhidraAnalysisProfile.ts` (+3 -0) 📝 `src/ghidra/GhidraFunctionValues.test.ts` (+97 -0) 📝 `src/ghidra/GhidraFunctionValues.ts` (+25 -6) 📝 `tests/boundary/mcp/ghidraNativeApiMcp.test.ts` (+88 -2) _...and 5 more files_ </details> ### 📄 Description ## Summary Addresses #1244. Native API dossiers now keep bounded x86-32 instruction diagnostics next to the recovered types, signature source and confidence. - **Conflicts:** stack reads and return cleanup can contradict a recovered prototype. - **Observations:** x87 operations and EAX forwarding stay observations, with explicit unknowns. CLI and MCP inspection and the selected views carry these facts. Older retained Evidence remains readable. ## Problem and expected behavior #1244 reproduced two cases with real Ghidra on `main`. In both, a confident-looking inferred signature hides conflicting instruction evidence: - `0x406400` has a no-argument signature, but its instructions read the first stack argument and do x87 arithmetic before a conversion helper. - `0x401b10` has four inferred stdcall arguments (16 bytes), but it returns with `RET 20`. Previously the analyst had to find these conflicts by reading assembly. Now `analyze_function` and `inspect_native_api` return `native_api.prototype_diagnostics`. Each diagnostic has: - a `conflict` or `observation` classification; - the inferred claim; - the stack-read, return, branch or call-site evidence addresses; - the residual unknowns. `prototype_check_limitations` records the checks' scope and any exhausted budget, even when nothing is found. A diagnostic is not proof of a source declaration: cleanup bytes do not establish an argument count, and EAX forwarding does not establish a return type. ## Change and scope - **Producer** (`bridge/ghidra/ReaGhidraPrototypeDiagnostics.java`, called from `ReaGhidraBridge.java`). It works from Ghidra's listing and raw p-code. - Entry stack reads are compared with recovered parameter storage and compiler-model slots. - Near-return cleanup is compared with explicit compiler-model cleanup or the recovered stack extent. - Shared epilogues are followed for at most 16 simple instructions, without expanding owned-body ranges. - EAX forwarding and x87 operations are recorded as observations. - Entry-prefix checks stop at 256 instructions, 2,048 raw p-code operations or 256 facts. Cleanup and forwarding each keep at most 256 candidates or facts. Every budget that is reached is reported as a limitation. - **Contract** (`src/domain/native/nativeApiBoundary.ts`). It adds the diagnostic schema plus a retained-boundary variant, so Evidence written before this change still validates. - **Projection** (`NativeApiInspection.ts`, `nativeFunctionView.ts`). It carries diagnostics, limitations and their residual unknowns into CLI/MCP inspection and the selected native API and assembly views. Older Evidence reports "Instruction/prototype consistency was not recorded in this Evidence." - **Profile** (`GhidraAnalysisProfile.ts`). It adds `prototype_consistency_evidence: bounded-x86-32-listing-pcode-v6`, so earlier cached observations are not reused. - **Verification.** A new `verify:ghidra:prototype` uses source-owned ELF32 assembly controls (`tests/conformance/ghidra/prototype-conflicts.S`) and a producer probe. It also runs in the Linux host verifier. - **Not included:** - architectures other than x86-32, which report consistency as unknown; - interprocedural or alias propagation; - inferring a source signature, signedness or compiler identity; - executing target instructions. Review fixes: - Run host toolchain preflight before allocating fixtures, and protect every later setup step with cleanup. If a launched provider cannot be retired, keep the workspace and its owner. - Confirm the MCP transport's actual close event before releasing the workspace. Keep the transport and the close observation for retries, without changing SDK negotiation or shutdown. - Check explicit compiler-model cleanup independently of custom stack-slot allocation. - Preserve unknown epilogue ownership in cleanup and EAX-forwarding observations. An unowned tail target cannot establish a prototype conflict. - Count only in-body returns and external direct branches against the cleanup budget. - Require a nonempty check scope in current Ghidra output, while keeping older retained Evidence readable. - Normalize x86-32 stack-pointer aliases modulo 2^32 for both reads and writes, which prevents false conflicts after pointer wraparound. - Distinguish natural ELF/GCC calling conventions from seeded Windows controls in the public verifier, with a separate clean caller-cleaned control. - Bound caller-reference evidence for return-register observations, and preserve unknown cleanup as unknown. Both were raised in dandgabr's review. Follow the [contribution scope](https://github.com/morluto/rea/blob/main/CONTRIBUTING.md#contribution-scope). Unresolved scope, authority, side effects, or required verification block integration. Link the required maintainer scope decision for new providers or capabilities involving target execution, injection, mutation, or protection recovery; ordinary fixes within existing boundaries may state "not applicable". Draft PRs may leave the scope decision pending and the readiness and merge checklists unchecked. Maintainers can help resolve open questions. ## Contract and boundary impact - Semantic owner and earliest changed stage: the Ghidra bridge producer. `nativeApiBoundary.ts` owns the schema, and `NativeApiInspection.ts` and `nativeFunctionView.ts` own the projections. - Contribution scope fit and linked maintainer decision: static analysis inside the existing Ghidra provider, for the enhancement filed in #1244. No new provider, target execution, injection, mutation or protection recovery is involved, so a separate scope decision is not applicable. A maintainer labelled the PR and marked it ready for review on 2026-10-13. - CLI and MCP/tool-catalog contract: `analyze_function` and `inspect_native_api` gain `native_api.prototype_diagnostics` and `prototype_check_limitations`. So does `annotate_native_function`, which returns the same dossier. Input schemas and descriptions are unchanged; output schemas grow (see Completed-task cost). - Provider, bridge, target-format, or platform compatibility: Ghidra bridge only. The checks support x86-32; other architectures report consistency as unknown. - Evidence, artifact, provenance, or reconstruction contract: - Diagnostics are `conflict` or `observation`, and each carries residual unknowns. - Evidence retained before this change still parses, and its missing check is reported as unknown. - The profile revision means snapshots cached before this change are not reused. - Target selection, authority, upstream behavior, and cleanup details (if applicable): target handling is unchanged. Verifier cleanup is hardened: transport close is observed before the workspace is released, and the owner is kept on failure. - Generated metadata (`docs/public/product-catalog.json`), package, or installation impact: catalogs regenerate from the source contracts and are not committed. `package.json` adds `verify:ghidra:prototype`. `docs/ghidra-provider.md` and `docs/testing.md` are updated. Expected effects (check known effects; use documentation-only on its own). Unchecked items do not establish absence; leave uncertainties visible. - [x] Read existing files or captured data. (The checks read the program already loaded in the caller's Ghidra session.) - [ ] Launch or attach to a process. (No new launch: the checks run inside the existing Ghidra session. The verifier still launches Ghidra and assembles its controls with GNU `as`/`ld`, as REA's other verifiers do.) - [ ] Inject instrumentation or run scripts/code. (Not applicable: target instructions never execute. The checks read Ghidra's listing and raw p-code.) - [ ] Change process memory, registers, files, or configuration. (Not applicable: executable bytes stay unchanged, and the verifier asserts this.) - [ ] Contact network services. - [ ] Recover protected code or work around protections. (Not applicable: the change reports prototype-consistency facts only.) - [ ] Documentation or usability only; no target interaction. - [ ] Not sure yet; investigation or maintainer guidance needed. ## Evidence and regression coverage - Tests added or updated: - `NativeApiInspection.test.ts`, `analysisView.test.ts`, `GhidraFunctionValues.test.ts` and `ghidraNativeApiMcp.test.ts`: diagnostics, limitations and residual unknowns through inspection, the selected views and MCP; older Evidence without the fields. - `sessionMcp.test.ts`: the session workflow now inherits the shared suite timeout. - `prototypeVerifierCleanup.test.ts` and `prototypeVerifierTransport.test.ts`: verifier setup failure, transport-close observation and retained ownership. - `verify-ghidra-prototype-diagnostics.mjs` (with its assertions) and `tests/conformance/ghidra/prototype-conflicts.S`: 34 seeded producer controls covering conflicting and matching stack inputs and cleanup, written slots, conditional pointers, ABI padding, shared epilogues, tail calls and EAX overwrite/forwarding. CLI/MCP parity runs on natural ELF output. - Base reproduction or other evidence: - The two #1244 cases were reproduced with real Ghidra on `main`. - The Java findings and the wrapped-alias false conflicts reproduced before their fixes. - [Independent run by @CassieFox23](https://github.com/morluto/rea/pull/1672#issuecomment-6182755718) on Linux, Node 24.18.0 and 26.11.1, Ghidra 12.1.4: the 7 PR test files (127 tests) and the real Ghidra check (34 producer controls, then CLI and MCP) passed. For the same assembled file, `main` reports no prototype findings and this branch does. - User-visible CLI/MCP output (if applicable): from that independent run, `inspect-native-api` prototype findings per control function, `main` → head. CLI and MCP matched on every function. | Function | `main` | Head | | --------------- | -----: | ---: | | Stack and x87 | none | 3 | | Cleanup conflict | none | 1 | | Cleanup control | none | 1 | | Stack control | none | 0 | | Forward return | none | 1 | | Overwrite return | none | 0 | - The cleanup-conflict function reports one conflict: its `RET` cleans 20 bytes, but 16 were recovered. - The stack and x87 function reports a stack-read conflict, an x87 observation and an EAX forwarding observation. - On natural ELF metadata, `rea_cleanup_control` is also a conflict, as the assertions expect. Only the seeded Windows probe makes it a clean control. - Remaining proof gaps: - No Windows target or host, and no macOS. - Ghidra time and memory, and token counts on real outputs with diagnostics, are not yet measured. They have been requested; see Completed-task cost. - The spawn-failure assertion in `prototypeVerifierTransport.test.ts` fails on Windows hosts; see Validation. For evidence-bearing changes: - [x] Observed, derived, and inferred claims remain distinguishable. Diagnostics are classified as `conflict` or `observation`, and each carries residual unknowns. - [x] Artifact identity, source provenance, and failed attempts remain preserved. Signature source and confidence are unchanged, and older Evidence stays readable. - [x] Unsupported, incomplete, unavailable, or uncertain outcomes remain visible. Unsupported architectures, exhausted budgets and unowned epilogues are reported as limitations or observations. ## Completed-task cost Per AGENTS.md "Performance". Measured locally without Ghidra, against `main` `633e4ff43` and this head `df532779a`. Tokens are `cl100k_base` counts (tiktoken 0.13.0) over serialized JSON, not hosted-model billing. | Measurement | `main` | Head | Change | | ---------------------------------------------------------------- | ------: | ----: | ------: | | Tool catalog, name + description + input schema (207 tools) | 195,649 | 195,649 | 0 | | Tool catalog including output schemas | 807,491 | 809,207 | +1,716 (+0.21%) | | `inspect_native_api` result, x86-32 function, no diagnostics | 510 | 997 | +487 (+95%) | | Dossier `native_api` in `analyze_function`, same function | 396 | 565 | +169 | | `inspect_native_api` result, other architecture | 510 | 577 | +67 | - **Catalog.** Output schemas grow by about 570 tokens each for `analyze_function`, `annotate_native_function` and `inspect_native_api`. - **Per-result rows.** These use the repository dossier fixture with the producer's exact limitation strings, so they are the fixed cost every function pays before any diagnostic. Each diagnostic then adds its evidence and residual unknowns. - **Where the fixed cost comes from.** Three x86-32 limitation paragraphs (about 160 tokens) are emitted for every x86-32 function. `inspect_native_api` repeats them three times: - in `boundary.prototype_check_limitations`; - in the `preserve_residual_unknowns` substep; - in `residual_unknowns`. The last two copies follow the existing residual-unknown pattern. If maintainers prefer, a follow-up could emit the fixed text once per result, or as stable identifiers. This PR does not change it. - **Cache.** The new profile revision means snapshots cached before this change are recomputed once after upgrade. - **Not yet measured.** Ghidra analysis wall time, CPU and peak process-family memory, `main` against head, cold and warm, plus token counts on real outputs with diagnostics. This host has no Ghidra set up for REA. I've asked @CassieFox23, who already ran the real verifier, and will add the results here. ## Validation performed Windows 11 x64, Node 24.21.0. Head `df532779a` is `105daea5a` merged with `main` `633e4ff43`, with no conflicts. - `npm run test:local -- src/application/native/NativeApiInspection.test.ts src/domain/analysisView/analysisView.test.ts src/ghidra/GhidraFunctionValues.test.ts`: 115 passed. - `npm run test:focused -- tests/boundary/mcp/ghidraNativeApiMcp.test.ts tests/boundary/mcp/sessionMcp.test.ts tests/process-global/prototypeVerifierCleanup.test.ts tests/process-global/prototypeVerifierTransport.test.ts`: 14 passed, 4 skipped, 1 failed. - The failure is `prototypeVerifierTransport` "observes transport closure when the server cannot spawn". On Windows, the MCP client reports "Connection closed" for a missing executable instead of `ENOENT`. - It fails the same way on the pre-merge head `105daea5a` on this host, and it passes on Linux (CI and the independent run). Making that assertion Windows-safe is a known gap. - `npm run check:fast`, `npm run format:check`, `npm run docs:check`, `npm run mcp-catalog:check`, `npm run knip` and `npm run verify:test-discovery`: all passed. - Completed-task cost: the token measurements above. Earlier validation, before the merge with `main`: - **CI follow-up `105daea5`.** - The macOS session workflow exceeded its test-specific 10-second limit in run 38636461493, so it now inherits the existing 30-second suite deadline (60 s under coverage). - Fresh macOS CI then passed all 225 tests, with four named skips. - [CI run 38640169972](https://github.com/morluto/rea/actions/runs/38640169972) passed all 35 jobs. The separate Go metadata, packet-capture and signal-recording workflows also passed. - **Follow-up `cd61a7f`.** 93 focused tests and `npm run check` passed. The actual MCP SDK/SIGKILL regression failed before the fix and passed afterward. - **Ghidra producer checks.** - Ghidra 12.1.4 with JDK 21 passed all 34 seeded production-producer controls and the retained-Evidence projections. - Six semantic checks on natural ELF/GCC output and six exploratory direct controls also passed. - The full real-provider CLI/MCP verifier was blocked in the author's container. The independent run above completed it. ## Compatibility, safety, and release - Breaking changes or migration steps: none. The new fields are additive, and Evidence retained without them still validates and reports the check as not recorded. - Real Hopper/Ghidra, browser, or OS coverage: - Real Ghidra 12.1.4 on Linux, by the author and in the independent run. - CI covers the Ghidra lanes. - No Windows target or host, and no macOS Ghidra run. - Package or release metadata impact: catalogs regenerate. `verify:ghidra:prototype` is new. - Security, privacy, process, or containment review: - Target instructions never execute, and executable bytes are verified unchanged. - Producer work is bounded by the budgets above. - The verifier keeps workspace ownership when cleanup cannot be confirmed. ## Author readiness  Human owner: @Y0UW1SH - [x] I reviewed the final diff and relevant existing code, understand the change and its edge cases, and take responsibility for the complete PR, including AI-assisted work. - [x] I checked the evidence above, confirmed it supports the current change, and recorded meaningful validation gaps. - [x] I declare this PR ready for initial maintainer review. ## Before merge  - [x] This PR addresses a concrete problem or an agreed enhancement. (#1244, with two cases reproduced on `main`.) - [x] Material scope and authority questions are resolved, and any required maintainer scope decision covers the final diff. (Static analysis inside the existing Ghidra provider, so no scope decision is required; see Contract and boundary impact.) - [x] The PR has one focused outcome and the title follows `type(scope): outcome`. - [x] Related issue is linked, or the reason for not linking one is stated above. (#1244.) - [x] Tests cover changed observable behavior and meaningful failure paths. - [x] Owning docs, contracts, and generated metadata are updated where needed. (`docs/ghidra-provider.md`, `docs/testing.md` and the boundary schema; catalogs are generated by CI.) - [ ] User-visible CLI/MCP changes include representative output. (Pending: per-function counts from a real Ghidra run are above, but no raw `inspect-native-api` JSON from a real run is included yet.) - [x] I checked the final diff for secrets, unrelated cleanup, and unsupported claims. (25 files, all part of this change; no secrets found.) --- <sub>🔄 This issue represents a GitHub Pull Request. It cannot be merged through Gitea due to API limitations.</sub>

bsakaguchi

2026-10-31 00:54:35 +00:00