morluto/rea

Fork 0

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

[GH-ISSUE #8274] [Design] Make real Ghidra and Kuna workflow regressions a visible CI gate #6518

New issue

Open

opened 2026-11-01 21:11:51 +00:00 by bsakaguchi · 14 comments

bsakaguchi commented

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

Owner

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

Before submitting

I searched the open and closed issues and pull requests for a related discussion.
I understand the contribution scope must be reviewed before integration; open questions are welcome here.
This discussion does not include credentials, private samples, or sensitive target data.

Decision needed

What real-provider CLI/MCP regression workflows should run as a reliable, explicitly reported Ghidra/Kuna gate for relevant changes, and which heavier cases belong in scheduled or manual qualification?

Context and evidence

At source revision e6d061897, the testing guide already prioritizes public real-provider workflows, then production-boundary integration and producer goldens. verify:ghidra and verify:kuna exist and have meaningful real-provider checks. In the inspected workflows, normal CI conditionally calls the verified Ghidra bridge compilation/probe workflow; the separate real Windows Ghidra workflow is repository_dispatch only. I found no CI workflow invocation of the POSIX host-native verify:ghidra or verify:kuna scripts. This is a workflow/source observation, not proof that nobody runs those scripts elsewhere.

The distinction matters for observed regressions:

The host-native real Ghidra verifier itself failed at the default MCP request limit on one macOS run; an isolated retained-reference experiment passed the lane while retaining its assertions. See #8172.
A real-provider naming check asserts one first-wins conflicting batch. Reversing object order and using dependent distinct names exposed differing outcomes in #8238. A real E2E test still needs an oracle for the intended contract; this example is not a claim that the existing assertion is useless.
#8226 records mixed Kuna batch behavior and per-item provenance gaps; #8225 records an existing-project MIPS failure despite fresh-import controls. These scenarios need regressions at their producing and public boundaries once their contracts/fixes are settled.

Expected interaction with targets

Read source-owned fixtures, launch caller-supplied or CI-provisioned analysis tools, and write owned temporary projects/caches; no target execution is required for these examples.

Boundary details (optional)

Distinguish required, optional, skipped, unavailable and failed lanes in the check result. Pin or verify provider and JDK versions, clean owned resources, preserve caller-owned artifacts, and avoid treating fake providers as real-provider proof. Keep existing authority boundaries and do not commit binary/project artifacts. Test goals should be selected from analyst workflows and independent expected facts, not raw API coverage.

Options and tradeoffs

Evaluate a bounded Linux real Ghidra/Kuna public-workflow smoke gate for relevant PRs plus broader scheduled/manual cross-format and lifecycle qualification. Establish install/licensing and hosted-runner availability before prescribing a required gate. Maintain failure-path integration tests and producer goldens where real tools cannot reliably trigger the condition. Existing focused tests may be removed only after a stronger check retains their distinct failure coverage.

Verification available so far

I have a prototype or observed results.

Success criteria and open questions

Map concrete changes to required and optional real-provider scenarios and show the exact workflow, host, provider versions and result in PR checks; missing prerequisites must not appear as a successful real-provider run.
Add meaningful public CLI/MCP workflows and independent fixtures for agreed regressions, including partial failures, saved projects, cleanup/recovery and evidence handoffs where applicable. Keep scenarios scoped to actual supported authority.
Demonstrate failure detection against the original bug or a controlled mutation, and verify positive and negative controls. Decide ownership of deliberately injected rare-failure cases separately from unmodified-provider E2E cases.
Measure completed representative CI runs and provider acquisition costs before setting required coverage or time budgets; NOT_ENOUGH_INFO for CI cost and availability today.

References

Related implementation issues: #8172, #8238, #8226, #8225, #8169. This is a testing-gate and scenario-selection discussion; it does not propose resolving those behavior contracts by assertion alone.

Originally created by @morluto on GitHub (Oct 31, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/8274 ### Before submitting - [x] I searched the open and closed issues and pull requests for a related discussion. - [x] I understand the contribution scope must be reviewed before integration; open questions are welcome here. - [x] This discussion does not include credentials, private samples, or sensitive target data. ### Decision needed What real-provider CLI/MCP regression workflows should run as a reliable, explicitly reported Ghidra/Kuna gate for relevant changes, and which heavier cases belong in scheduled or manual qualification? ### Context and evidence At source revision `e6d061897`, [the testing guide](https://github.com/morluto/rea/blob/e6d0618979f0df3f1d5db218b0fc7b5e6a9cf3f9/docs/testing.md#choose-verification-for-the-change) already prioritizes public real-provider workflows, then production-boundary integration and producer goldens. `verify:ghidra` and `verify:kuna` exist and have meaningful real-provider checks. In the inspected workflows, normal CI conditionally calls the verified Ghidra bridge compilation/probe workflow; the separate real Windows Ghidra workflow is `repository_dispatch` only. I found no CI workflow invocation of the POSIX host-native `verify:ghidra` or `verify:kuna` scripts. This is a workflow/source observation, not proof that nobody runs those scripts elsewhere. The distinction matters for observed regressions: * The host-native real Ghidra verifier itself failed at the default MCP request limit on one macOS run; an isolated retained-reference experiment passed the lane while retaining its assertions. See [#8172](https://github.com/morluto/rea/issues/8172#issuecomment-6540579267). * A [real-provider naming check](https://github.com/morluto/rea/blob/e6d0618979f0df3f1d5db218b0fc7b5e6a9cf3f9/scripts/lib/real-ghidra-namespace-annotations.mjs#L233-L253) asserts one first-wins conflicting batch. Reversing object order and using dependent distinct names exposed differing outcomes in [#8238](https://github.com/morluto/rea/issues/8238#issuecomment-6540637118). A real E2E test still needs an oracle for the intended contract; this example is not a claim that the existing assertion is useless. * [#8226](https://github.com/morluto/rea/issues/8226) records mixed Kuna batch behavior and per-item provenance gaps; [#8225](https://github.com/morluto/rea/issues/8225) records an existing-project MIPS failure despite fresh-import controls. These scenarios need regressions at their producing and public boundaries once their contracts/fixes are settled. ### Expected interaction with targets Read source-owned fixtures, launch caller-supplied or CI-provisioned analysis tools, and write owned temporary projects/caches; no target execution is required for these examples. ### Boundary details (optional) Distinguish required, optional, skipped, unavailable and failed lanes in the check result. Pin or verify provider and JDK versions, clean owned resources, preserve caller-owned artifacts, and avoid treating fake providers as real-provider proof. Keep existing authority boundaries and do not commit binary/project artifacts. Test goals should be selected from analyst workflows and independent expected facts, not raw API coverage. ### Options and tradeoffs Evaluate a bounded Linux real Ghidra/Kuna public-workflow smoke gate for relevant PRs plus broader scheduled/manual cross-format and lifecycle qualification. Establish install/licensing and hosted-runner availability before prescribing a required gate. Maintain failure-path integration tests and producer goldens where real tools cannot reliably trigger the condition. Existing focused tests may be removed only after a stronger check retains their distinct failure coverage. ### Verification available so far I have a prototype or observed results. ### Success criteria and open questions 1. Map concrete changes to required and optional real-provider scenarios and show the exact workflow, host, provider versions and result in PR checks; missing prerequisites must not appear as a successful real-provider run. 2. Add meaningful public CLI/MCP workflows and independent fixtures for agreed regressions, including partial failures, saved projects, cleanup/recovery and evidence handoffs where applicable. Keep scenarios scoped to actual supported authority. 3. Demonstrate failure detection against the original bug or a controlled mutation, and verify positive and negative controls. Decide ownership of deliberately injected rare-failure cases separately from unmodified-provider E2E cases. 4. Measure completed representative CI runs and provider acquisition costs before setting required coverage or time budgets; `NOT_ENOUGH_INFO` for CI cost and availability today. ### References Related implementation issues: #8172, #8238, #8226, #8225, #8169. This is a testing-gate and scenario-selection discussion; it does not propose resolving those behavior contracts by assertion alone.

bsakaguchi added the

enhancement

triage

labels

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

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

Upstream harness is a separate testing layer

I built decomp_test_dbg from the exact upstream v1.986 source tag (cb2279cab17fb8be9b7b005c3df9955eea78b551) and used it with the installed Kuna 1.986 test wrapper, that tag's test corpus, and the release-extracted SLEIGH tree. Three selected XML cases (forloop1, bitfields, ccmp) produced 36/36 passing data assertions. A deliberately impossible, temporary baseline made the same wrapper exit 1 with PARITY FAIL and the missing sentinel in regressed; the JSON's inner harness returncode remained 0 because the harness itself passed. No baseline was rewritten.

The wrapper warned that the two executables are different builds: release CLI version 1.986 versus source-built debug harness version 0.1.0; both reported source fingerprint de15b95c1300618b. The harness runs its own linked engine, so this is a selected upstream source-built-engine test and a CLI wrapper/exit-status control, not proof that REA or the installed release's decompiler engine passed these cases. It also does not cover REA Evidence, session lifecycle, or public CLI/MCP integration. The released package did not include this separate harness.

For the proposed REA gate, upstream tests can complement but cannot replace a real public REA workflow against the provisioned provider. If an upstream test wrapper is ever used in automation, check its process exit status as well as the JSON fields; the deliberately failed baseline demonstrates why the nested harness return code alone is insufficient. This was one local bounded check, not a CI cost measurement or a proposal to run the complete upstream suite.

@morluto commented on GitHub (Oct 31, 2026): ### Upstream harness is a separate testing layer I built `decomp_test_dbg` from the exact upstream `v1.986` source tag (`cb2279cab17fb8be9b7b005c3df9955eea78b551`) and used it with the installed Kuna 1.986 `test` wrapper, that tag's test corpus, and the release-extracted SLEIGH tree. Three selected XML cases (`forloop1`, `bitfields`, `ccmp`) produced 36/36 passing data assertions. A deliberately impossible, temporary baseline made the same wrapper exit 1 with `PARITY FAIL` and the missing sentinel in `regressed`; the JSON's inner harness `returncode` remained 0 because the harness itself passed. No baseline was rewritten. The wrapper warned that the two executables are **different builds**: release CLI version `1.986` versus source-built debug harness version `0.1.0`; both reported source fingerprint `de15b95c1300618b`. The harness runs its own linked engine, so this is a selected upstream source-built-engine test and a CLI wrapper/exit-status control, **not** proof that REA or the installed release's decompiler engine passed these cases. It also does not cover REA Evidence, session lifecycle, or public CLI/MCP integration. The released package did not include this separate harness. For the proposed REA gate, upstream tests can complement but cannot replace a real public REA workflow against the provisioned provider. If an upstream `test` wrapper is ever used in automation, check its process exit status as well as the JSON fields; the deliberately failed baseline demonstrates why the nested harness return code alone is insufficient. This was one local bounded check, not a CI cost measurement or a proposal to run the complete upstream suite.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

Dependent-function cache control with real Ghidra

On REA b43c329df779708e43ae297f498a844e45d9c923 / Ghidra 12.1.4, I exercised a source-owned arm64 Mach-O where _evaluate calls _adjust, and _adjust reads _global_count. A real MCP session first requested both functions' pseudocode and the caller's complete dossier twice. After an ephemeral rename of _adjust to audit_cached_callee, the next caller pseudocode and caller dossier showed the new callee name. After renaming the data label to audit_cached_global, the next callee pseudocode showed the new global name. The same address-only call graph remained unchanged, as expected for name-only edits. The original retained caller dossier remained retrievable and still showed the old name as historical Evidence. All calls and close succeeded; the target hash was unchanged and it was not executed.

This is a positive cross-function cache-invalidation control, not evidence of a stale-result bug or of general concurrency/alias handling. The existing real-provider verifier already primes inventories before a same-function edit and checks the edited dossier; a future workflow regression could additionally assert dependent caller/callee renderings and retained historical Evidence without replacing those checks. The session snapshot remains a distinct immutable feature; this test did not save one after editing. No timing or autonomous-agent behavior was measured.

@morluto commented on GitHub (Oct 31, 2026): ### Dependent-function cache control with real Ghidra On REA `b43c329df779708e43ae297f498a844e45d9c923` / Ghidra 12.1.4, I exercised a source-owned arm64 Mach-O where `_evaluate` calls `_adjust`, and `_adjust` reads `_global_count`. A real MCP session first requested both functions' pseudocode and the caller's complete dossier twice. After an ephemeral rename of `_adjust` to `audit_cached_callee`, the next caller pseudocode **and** caller dossier showed the new callee name. After renaming the data label to `audit_cached_global`, the next callee pseudocode showed the new global name. The same address-only call graph remained unchanged, as expected for name-only edits. The original retained caller dossier remained retrievable and still showed the old name as historical Evidence. All calls and close succeeded; the target hash was unchanged and it was not executed. This is a positive cross-function cache-invalidation control, not evidence of a stale-result bug or of general concurrency/alias handling. The existing real-provider verifier already primes inventories before a same-function edit and checks the edited dossier; a future workflow regression could additionally assert dependent caller/callee renderings and retained historical Evidence without replacing those checks. The session snapshot remains a distinct immutable feature; this test did not save one after editing. No timing or autonomous-agent behavior was measured.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

A real-provider test-gap control for #8277, without changing the suite:

The existing host-native Ghidra verifier's verifyUnresolvedCallEvidence is meaningful E2E coverage: it checks a function-pointer parameter with no reported target and expects partial coverage, an unresolved call, and an unknown path. I compiled the repository's actual tests/conformance/ghidra/inventory.c on macOS arm64 and exercised that assertion subset through real Ghidra 12.1.4/REA stdio MCP. It passed: one unresolved call, partial coverage, goal_status: unknown, and a residual unknown. This was the assertion subset, not a run of the complete verifier.

I then built a separate x86-64 ELF containing both a call through an unknown function argument and the writable-slot sequence from #8277. On the same binary and Ghidra session, the targetless argument call gave the same partial/unknown result, while the call with one reported resolved-indirect candidate returned complete coverage and not_reached for the distinct target written into the slot. Both fixtures' digests stayed unchanged; neither was executed. The difference is not evidence that testing was absent: the existing test selects the targetless case and does not exercise this resolved-candidate-plus-other-possible-target shape.

A regression for the second shape needs its own oracle: retain the reported candidate while ensuring an unproven alternative is not ruled out. It should not blindly assert that a resolved candidate belongs in the existing unresolved_calls array, whose semantics may differ. A real public-workflow fixture can provide the independent slot/write/control facts; controlled boundary tests can cover cases a real provider cannot reliably reproduce. No CI execution or cross-platform coverage is claimed by this control.

@morluto commented on GitHub (Oct 31, 2026): A real-provider test-gap control for #8277, without changing the suite: The existing host-native Ghidra verifier's [`verifyUnresolvedCallEvidence`](https://github.com/morluto/rea/blob/b43c329df779708e43ae297f498a844e45d9c923/scripts/lib/native-value-e2e.mjs#L345-L395) is meaningful E2E coverage: it checks a function-pointer parameter with no reported target and expects partial coverage, an unresolved call, and an unknown path. I compiled the repository's actual `tests/conformance/ghidra/inventory.c` on macOS arm64 and exercised that assertion subset through real Ghidra 12.1.4/REA stdio MCP. It passed: one unresolved call, partial coverage, `goal_status: unknown`, and a residual unknown. This was the assertion subset, not a run of the complete verifier. I then built a separate x86-64 ELF containing both a call through an unknown function argument and the writable-slot sequence from #8277. On the **same binary and Ghidra session**, the targetless argument call gave the same partial/unknown result, while the call with one reported `resolved-indirect` candidate returned complete coverage and `not_reached` for the distinct target written into the slot. Both fixtures' digests stayed unchanged; neither was executed. The difference is not evidence that testing was absent: the existing test selects the targetless case and does not exercise this resolved-candidate-plus-other-possible-target shape. A regression for the second shape needs its own oracle: retain the reported candidate while ensuring an unproven alternative is not ruled out. It should not blindly assert that a resolved candidate belongs in the existing `unresolved_calls` array, whose semantics may differ. A real public-workflow fixture can provide the independent slot/write/control facts; controlled boundary tests can cover cases a real provider cannot reliably reproduce. No CI execution or cross-platform coverage is claimed by this control.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

Another concrete real-provider coverage distinction, following Kuna #1349 and REA #8328:

REA's real-Kuna verifier genuinely tests stripped binaries: it builds a source fixture, records function addresses from the unstripped image, strips a copy, and checks that each original address remains in the provider inventory and can be queried (fixture setup, address checks). This is useful coverage of stripped code recovery, not an export-name oracle.
On a copy of that source-owned verifier executable, this host's default strip left only __mh_execute_header in the export list. Separately, default strip on a source-owned dylib removed conventional symbols while keeping its function and data export-trie names. In real current-main MCP/Kuna tests on the original dylib and the copies stripped with default strip and strip -N, all three exposed the same function address and address-selected pseudocode; the exact export name resolved only on the original, while inspect_macho reported it on all three. The first exploratory name query omitted the leading underscore and failed even on the original; the corrected comparison used the exact export spelling.
Upstream's macho_stripped_main.py intentionally clears the export trie for its LC_MAIN recovery test. That fixture serves a different purpose from a retained-export test; this observation does not establish the full upstream test inventory.

A useful additional regression would exercise a tool-produced stripped dylib with function and data exports, independently inspect its export trie, and check name-to-address handoff and callable-versus-data uncertainty through the public workflow. A no-export stripped control remains valuable. This was a targeted real MCP comparison, not a rerun of the entire verifier or CI, and no target was executed.

@morluto commented on GitHub (Oct 31, 2026): Another concrete real-provider coverage distinction, following [Kuna #1349](https://github.com/Noelo-Lab/kuna/issues/1349#issuecomment-6545127851) and REA #8328: - REA's real-Kuna verifier genuinely tests stripped binaries: it builds a source fixture, records function addresses from the unstripped image, strips a copy, and checks that each original address remains in the provider inventory and can be queried ([fixture setup](https://github.com/morluto/rea/blob/a989c0e458c91af177e097abd7be0fd021b0401d/scripts/verify-real-kuna.mjs#L531-L556), [address checks](https://github.com/morluto/rea/blob/a989c0e458c91af177e097abd7be0fd021b0401d/scripts/verify-real-kuna.mjs#L311-L340)). This is useful coverage of stripped code recovery, not an export-name oracle. - On a copy of that source-owned verifier executable, this host's default `strip` left only `__mh_execute_header` in the export list. Separately, default `strip` on a source-owned dylib removed conventional symbols while keeping its function and data export-trie names. In real current-main MCP/Kuna tests on the original dylib and the copies stripped with default `strip` and `strip -N`, all three exposed the same function address and address-selected pseudocode; the exact export name resolved only on the original, while `inspect_macho` reported it on all three. The first exploratory name query omitted the leading underscore and failed even on the original; the corrected comparison used the exact export spelling. - Upstream's [`macho_stripped_main.py`](https://github.com/Noelo-Lab/kuna/blob/d85e7cc46fef8e241e6b81525d3be19fce82f970/decompiler/crates/kuna-analysis/tests/fixtures/macho_stripped_main.py#L1-L16) intentionally clears the export trie for its `LC_MAIN` recovery test. That fixture serves a different purpose from a retained-export test; this observation does not establish the full upstream test inventory. A useful additional regression would exercise a tool-produced stripped dylib with function and data exports, independently inspect its export trie, and check name-to-address handoff and callable-versus-data uncertainty through the public workflow. A no-export stripped control remains valuable. This was a targeted real MCP comparison, not a rerun of the entire verifier or CI, and no target was executed.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

On current main 60149282fcfc05ac32fbc94434c107710120da6f, I locally applied open PR #8258's exact two files and ran the real host-native Ghidra verifier: it passed on macOS arm64 / Ghidra 12.1.4 / JDK 21 with explicit JAVA_HOME, reporting four fixture variants, 433 successful and 52 rejected boundary calls, cleanup:complete, and verified no remaining descendants. This is an actual combined-tree run, not hosted CI. Main without #8258 previously failed the comparison input allowance (#8172); the JDK discovery issue #8171 is separate.

The passing lane is meaningful but its oracle does not establish the two currently reproduced properties:

scripts/lib/native-value-e2e.mjs checks the shape of each node's evidence_id and looks up three top-level records in the bundle, but it does not resolve all per-node/procedure/edge IDs after warm snapshot replay. The real warm test in #8282 finds both procedure IDs missing offline.
The same verifier has a real unresolved callback assertion expecting partial coverage and an unknown path. The reported-candidate plus writable alternate in #8277 is a different input: main reports a candidate and a definite negative despite the separate state-flow evidence. An isolated conservative producer experiment changed the forward negative to unknown while keeping a reached candidate and direct control, but did not solve reverse coverage.

A useful real public-workflow regression should check both positive and negative controls and actual Evidence closure, rather than only an ID regex or only targetless callbacks. The current conditional ghidra_bridge CI job does compile against a pinned SDK and runs real focused ARM/Thumb and decode probes; I did not find the full POSIX verify:ghidra or verify:kuna commands invoked by the checked workflow sources. The separate Windows lane is dispatch-triggered. This source inspection is not evidence about any external/private CI or manual runs.

@morluto commented on GitHub (Oct 31, 2026): On current main `60149282fcfc05ac32fbc94434c107710120da6f`, I locally applied open PR #8258's exact two files and ran the real host-native Ghidra verifier: it passed on macOS arm64 / Ghidra 12.1.4 / JDK 21 with explicit `JAVA_HOME`, reporting four fixture variants, 433 successful and 52 rejected boundary calls, `cleanup:complete`, and verified no remaining descendants. This is an actual combined-tree run, not hosted CI. Main without #8258 previously failed the comparison input allowance (#8172); the JDK discovery issue #8171 is separate. The passing lane is meaningful but its oracle does not establish the two currently reproduced properties: - `scripts/lib/native-value-e2e.mjs` checks the shape of each node's `evidence_id` and looks up three top-level records in the bundle, but it does not resolve all per-node/procedure/edge IDs after warm snapshot replay. The real warm test in #8282 finds both procedure IDs missing offline. - The same verifier has a real unresolved callback assertion expecting partial coverage and an unknown path. The reported-candidate plus writable alternate in #8277 is a different input: main reports a candidate and a definite negative despite the separate state-flow evidence. An isolated conservative producer experiment changed the forward negative to unknown while keeping a reached candidate and direct control, but did not solve reverse coverage. A useful real public-workflow regression should check both positive and negative controls and actual Evidence closure, rather than only an ID regex or only targetless callbacks. The current conditional `ghidra_bridge` CI job does compile against a pinned SDK and runs real focused ARM/Thumb and decode probes; I did not find the full POSIX `verify:ghidra` or `verify:kuna` commands invoked by the checked workflow sources. The separate Windows lane is dispatch-triggered. This source inspection is not evidence about any external/private CI or manual runs.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

A further real-provider lane now has a complete local control: on main 60149282, npm run verify:ghidra:swift passed on macOS arm64 with Swift 6.3.2, Ghidra 12.1.4 and explicit JDK 21. Its report covered debug and without-dSYM Swift inventories and the source-owned string-literal and unresolved-jump fixtures; verifier lineage reported no descendants. This is one host and is not a hosted-CI pass. The earlier compilation failure is fixed by merged #8325; full details: #8188.

A source search of .github/workflows and scripts/ci for the literal verify:ghidra:swift / verify-real-ghidra-swift found no named invocation on this revision. That is a limited configuration observation, not proof about external CI or dynamically generated commands. It may be useful when deciding which real-provider lanes are visible as gates.

@morluto commented on GitHub (Oct 31, 2026): A further real-provider lane now has a complete local control: on main `60149282`, `npm run verify:ghidra:swift` passed on macOS arm64 with Swift 6.3.2, Ghidra 12.1.4 and explicit JDK 21. Its report covered debug and without-dSYM Swift inventories and the source-owned string-literal and unresolved-jump fixtures; verifier lineage reported no descendants. This is one host and is not a hosted-CI pass. The earlier compilation failure is fixed by merged #8325; full details: #8188. A source search of `.github/workflows` and `scripts/ci` for the literal `verify:ghidra:swift` / `verify-real-ghidra-swift` found no named invocation on this revision. That is a limited configuration observation, not proof about external CI or dynamically generated commands. It may be useful when deciding which real-provider lanes are visible as gates.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

A concrete example of why a passing real-provider lane is not, by itself, an independent correctness oracle:

On current REA main 60149282, npm run verify:kuna passed with real Kuna 1.986 on its source-owned symbolized/stripped fixture and reported complete cleanup and no remaining verifier descendants. I separately rebuilt its exact fixture source, verified it is byte-for-byte the same source text as the current script, and inspected its Mach-O instructions with otool. Four BL sites in main were at 0x100000540, 0x10000054c, 0x100000558, and 0x100000568 on this build.

For each site, direct Kuna xrefs --to <site> reported a data edge from the site to itself, and real REA/Kuna MCP returned that same source address. REA/Ghidra inspect_native_instruction decoded each as a direct call to a different destination, and Ghidra xrefs to each site returned no reference. This matches the independently investigated upstream issue Kuna #1334; it is not a claim that self-references are always wrong. The rebuilt fixture SHA-256 was unchanged and it was never executed.

Source inspection explains the gap for this case: the current real lane checks that expected code entries are present and verifies incoming references to those function entries. Its native-xref comparison checks REA's projection against the same Kuna producer, not a separately established reference oracle. It does not query the four instruction addresses as targets, so producer and adapter can agree on an erroneous self-edge without failing that check. This is a scope of the exercised test, not evidence that the lane has no value or no independent checks elsewhere.

A targeted public-workflow regression can include known call-site xref negatives and a legitimate self-address positive control, while keeping REA-to-provider projection checks and the existing lifecycle coverage. The tested binary is a separate rebuild of identical fixture source, not the ephemeral binary retained from the verifier run; exact addresses are build-specific. One host/release is not a prevalence measurement.

@morluto commented on GitHub (Oct 31, 2026): A concrete example of why a passing real-provider lane is not, by itself, an independent correctness oracle: On current REA main `60149282`, `npm run verify:kuna` passed with real Kuna 1.986 on its source-owned symbolized/stripped fixture and reported complete cleanup and no remaining verifier descendants. I separately rebuilt its exact fixture source, verified it is byte-for-byte the same source text as the current script, and inspected its Mach-O instructions with `otool`. Four `BL` sites in `main` were at `0x100000540`, `0x10000054c`, `0x100000558`, and `0x100000568` on this build. For each site, direct Kuna `xrefs --to <site>` reported a `data` edge from the site to itself, and real REA/Kuna MCP returned that same source address. REA/Ghidra `inspect_native_instruction` decoded each as a direct call to a different destination, and Ghidra xrefs to each site returned no reference. This matches the independently investigated upstream issue [Kuna #1334](https://github.com/Noelo-Lab/kuna/issues/1334); it is not a claim that self-references are always wrong. The rebuilt fixture SHA-256 was unchanged and it was never executed. Source inspection explains the gap for this case: the current real lane checks that expected code entries are present and verifies incoming references to those **function entries**. Its native-xref comparison checks REA's projection against the same Kuna producer, not a separately established reference oracle. It does not query the four instruction addresses as targets, so producer and adapter can agree on an erroneous self-edge without failing that check. This is a scope of the exercised test, not evidence that the lane has no value or no independent checks elsewhere. A targeted public-workflow regression can include known call-site xref negatives and a legitimate self-address positive control, while keeping REA-to-provider projection checks and the existing lifecycle coverage. The tested binary is a separate rebuild of identical fixture source, not the ephemeral binary retained from the verifier run; exact addresses are build-specific. One host/release is not a prevalence measurement.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

Another concrete test-selection example: #8349 reproduces real Ghidra decompile-directory profile and layout mismatch errors via MCP/CLI. The safety boundary works and output files are preserved, but the generic recovery does not identify the mismatch. On current main, the 59-test source suite and the selected CLI/MCP boundary suites all pass; the existing mismatch assertion checks only that the fixture-provider rejection says does not match, while the CLI test uses fake Kuna for successful resume. Checked real-provider verifier sources have no decompile_all invocation.

A public workflow regression should start with a real export, assert a matching resume, induce a different known profile or layout, check both the intact outputs and the agent-facing error/recovery, and include malformed-journal handling. Profile differences and session edits are distinct: the mixed-state Ghidra example in #8260 intentionally stays within one profile and should not be silently rewritten. This is a proposed test after the behavior contract is settled, not an assertion that a new required CI lane is currently affordable.

@morluto commented on GitHub (Oct 31, 2026): Another concrete test-selection example: [#8349](https://github.com/morluto/rea/issues/8349) reproduces real Ghidra decompile-directory profile and layout mismatch errors via MCP/CLI. The safety boundary works and output files are preserved, but the generic recovery does not identify the mismatch. On current main, the 59-test source suite and the selected CLI/MCP boundary suites all pass; the existing mismatch assertion checks only that the fixture-provider rejection says `does not match`, while the CLI test uses fake Kuna for successful resume. Checked real-provider verifier sources have no `decompile_all` invocation. A public workflow regression should start with a real export, assert a matching resume, induce a different known profile or layout, check both the intact outputs and the agent-facing error/recovery, and include malformed-journal handling. Profile differences and session edits are distinct: the mixed-state Ghidra example in #8260 intentionally stays within one profile and should not be silently rewritten. This is a proposed test after the behavior contract is settled, not an assertion that a new required CI lane is currently affordable.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

A concrete real-provider regression candidate: #8362 reproduces a two-hop direct static call path that REA/Kuna 1.986 reports as not_reached with complete coverage, even though explicit Kuna disassembly and Ghidra identify the missing edge. Both MCP output schema profiles reproduce it; an ordinary direct-call positive control succeeds. The existing verifyKunaReferences checks an ordinary expected caller and reached path; that check has a useful oracle but does not exercise this section/inventory boundary.

Proposed test after settling the coverage contract: a source-built fixture with the two-hop path, an ordinary direct positive and unrelated control, and an assertion on the resulting uncertainty or recovered evidence through the public workflow. This is evidence for scenario selection, not proof that any existing CI lane ran or failed on this fixture.

@morluto commented on GitHub (Oct 31, 2026): A concrete real-provider regression candidate: #8362 reproduces a two-hop direct static call path that REA/Kuna 1.986 reports as `not_reached` with complete coverage, even though explicit Kuna disassembly and Ghidra identify the missing edge. Both MCP output schema profiles reproduce it; an ordinary direct-call positive control succeeds. The existing [`verifyKunaReferences`](https://github.com/morluto/rea/blob/d54a4661da20382ad8456564a08569fdd24131c5/scripts/lib/kuna-reference-verifier.mjs#L67-L83) checks an ordinary expected caller and reached path; that check has a useful oracle but does not exercise this section/inventory boundary. Proposed test after settling the coverage contract: a source-built fixture with the two-hop path, an ordinary direct positive and unrelated control, and an assertion on the resulting uncertainty or recovered evidence through the public workflow. This is evidence for scenario selection, not proof that any existing CI lane ran or failed on this fixture.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

Positive real-provider workflow evidence for test selection: on REA d54a4661da20382ad8456564a08569fdd24131c5 / Ghidra 12.1.4, I compared public MCP search_bytes against an independent byte-array oracle on an unexecuted 59-byte x86-64 raw fixture. Twelve bounded cases matched exactly, including overlapping matches split across pages, whole-byte wildcards, partial masks, wildcard-plus-mask, excluded and included end boundaries, an absent pattern, and first/last-byte matches. The 12 cases used 39 search calls; all returned addresses mapped to the expected source offsets. Calls used the full advertised SDK output schema. A separate public CLI masked-wildcard query matched the same oracle; target SHA-256 add538a96842a7f77d0f9993d540f4aba9a92e48e452dbf20ca1596f6ce5f94b was unchanged.

The existing real raw verifier already checks a 1,005-match continuation, one partial mask and overlapping matches in a single page. This additional run checks overlap across page boundaries and combined mask/wildcard semantics against an independent finite oracle. It is evidence that these cases worked on this provider/host, not a found bug or architecture-wide proof. If a regression is added to a provider gate, the small fixture and oracle could be adapted without replacing existing malformed-input and lifecycle coverage; no new repository test has been committed in this check.

@morluto commented on GitHub (Oct 31, 2026): Positive real-provider workflow evidence for test selection: on REA `d54a4661da20382ad8456564a08569fdd24131c5` / Ghidra 12.1.4, I compared public MCP `search_bytes` against an independent byte-array oracle on an unexecuted 59-byte x86-64 raw fixture. Twelve bounded cases matched exactly, including overlapping matches split across pages, whole-byte wildcards, partial masks, wildcard-plus-mask, excluded and included end boundaries, an absent pattern, and first/last-byte matches. The 12 cases used 39 search calls; all returned addresses mapped to the expected source offsets. Calls used the full advertised SDK output schema. A separate public CLI masked-wildcard query matched the same oracle; target SHA-256 `add538a96842a7f77d0f9993d540f4aba9a92e48e452dbf20ca1596f6ce5f94b` was unchanged. The existing [real raw verifier](https://github.com/morluto/rea/blob/d54a4661da20382ad8456564a08569fdd24131c5/scripts/verify-real-ghidra-raw.mjs#L253-L305) already checks a 1,005-match continuation, one partial mask and overlapping matches in a single page. This additional run checks overlap *across* page boundaries and combined mask/wildcard semantics against an independent finite oracle. It is evidence that these cases worked on this provider/host, not a found bug or architecture-wide proof. If a regression is added to a provider gate, the small fixture and oracle could be adapted without replacing existing malformed-input and lifecycle coverage; no new repository test has been committed in this check.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Oct 31, 2026):

Another real-provider example for this testing discussion: #8374 found that Ghidra search_strings and search_procedures dropped facts present on the corresponding list rows, and trace_feature consequently lost them. The existing host-native verifier did exercise real Ghidra search, but its long-literal assertion explicitly expected an {address,value} row; the simulated adapter fixtures likewise encoded the unqualified shape. That is a case where an existing E2E check alone was not a sufficient oracle.

Draft PR #8376 adds a real public-MCP check that compares the exact list row with the search row and trace match for a string, internal function, external function and an available thunk. Against base d54a4661 the check failed at the first missing string qualification; with the change it passed all four in the tested macOS arm64 fixture. The updated full host-native Ghidra lane passed on the PR commit with the separate #8172 retained-Evidence verifier workaround applied in an isolated checkout: debug, stripped, type-layout and jump-table fixtures, 441 successful and 52 rejected boundary calls, and complete cleanup. The regular unmodified-base lane still stops at #8172. No target was executed.

This suggests selecting cross-workflow invariants and negative controls for the real-provider gate, rather than treating tool invocation or a captured old output shape as sufficient. The case is one host/provider and does not replace malformed-output, cancellation or cleanup tests, nor establish a CI runtime budget.

@morluto commented on GitHub (Oct 31, 2026): Another real-provider example for this testing discussion: #8374 found that Ghidra `search_strings` and `search_procedures` dropped facts present on the corresponding list rows, and `trace_feature` consequently lost them. The existing host-native verifier did exercise real Ghidra search, but its long-literal assertion explicitly expected an `{address,value}` row; the simulated adapter fixtures likewise encoded the unqualified shape. That is a case where **an existing E2E check alone was not a sufficient oracle**. Draft PR #8376 adds a real public-MCP check that compares the exact list row with the search row and trace match for a string, internal function, external function and an available thunk. Against base `d54a4661` the check failed at the first missing string qualification; with the change it passed all four in the tested macOS arm64 fixture. The updated full host-native Ghidra lane passed on the PR commit with the separate #8172 retained-Evidence verifier workaround applied in an isolated checkout: debug, stripped, type-layout and jump-table fixtures, 441 successful and 52 rejected boundary calls, and complete cleanup. The regular unmodified-base lane still stops at #8172. No target was executed. This suggests selecting cross-workflow invariants and negative controls for the real-provider gate, rather than treating tool invocation or a captured old output shape as sufficient. The case is one host/provider and does not replace malformed-output, cancellation or cleanup tests, nor establish a CI runtime budget.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Nov 1, 2026):

Selection completeness control for the real Kuna lane

I compared the selection behavior with REA's current real-provider verifier, using clean main 6e9ee97a, verified Kuna 1.986 on macOS arm64, and an owned x86-64 ELF target pair. verify-real-kuna.mjs --targets <dir> --functions sequence,rea_missing_selection exited 1 before running the fixture lane, reported the missing function, and reported cleanup complete with verified process lineage and no remaining descendants. The same command with --functions sequence passed the complete lane: source-owned Mach-O fixture, its stripped copy, the caller-supplied ELF, and its stripped copy, with cleanup complete and no remaining descendants. The targets were statically analyzed, not executed.

This is a useful negative/positive real-lane control for this one selection boundary. REA does not invoke kuna test in the searched source, scripts, workflows and non-generated docs; its verifier has its own explicit check that every requested function was found somewhere among caller targets. That global check does not claim every named function occurs in every target. The upstream test wrapper's different partial-selection behavior is tracked separately in Noelo-Lab/kuna#1375; the two test suites exercise different engines and contracts.

@morluto commented on GitHub (Nov 1, 2026): ### Selection completeness control for the real Kuna lane I compared the selection behavior with REA's current real-provider verifier, using clean main `6e9ee97a`, verified Kuna 1.986 on macOS arm64, and an owned x86-64 ELF target pair. `verify-real-kuna.mjs --targets <dir> --functions sequence,rea_missing_selection` exited 1 before running the fixture lane, reported the missing function, and reported cleanup complete with verified process lineage and no remaining descendants. The same command with `--functions sequence` passed the complete lane: source-owned Mach-O fixture, its stripped copy, the caller-supplied ELF, and its stripped copy, with cleanup complete and no remaining descendants. The targets were statically analyzed, not executed. This is a useful negative/positive real-lane control for this one selection boundary. REA does not invoke `kuna test` in the searched source, scripts, workflows and non-generated docs; its verifier has its own explicit check that every requested function was found somewhere among caller targets. That global check does not claim every named function occurs in every target. The upstream test wrapper's different partial-selection behavior is tracked separately in [Noelo-Lab/kuna#1375](https://github.com/Noelo-Lab/kuna/issues/1375); the two test suites exercise different engines and contracts.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Nov 1, 2026):

Real-provider test-selection control for #8171: on main 6e9ee97a, with JAVA_HOME unset and JDK 21 on PATH, the real Ghidra 12.1.4 COM verifier completed its public CLI/stdio MCP workflow with unchanged fixture and complete cleanup. The general verifier previously failed with that setup because its direct launcher lost the inspected JDK; a deliberately invalid explicit JAVA_HOME was separately rejected despite the valid PATH JDK. Details and the proposed full-lane regression are in #8171. A green real-provider lane therefore cannot establish another lane’s setup handoff; this is one host, and the general lane also needs the independent #8172 fix before a full completion assertion.

@morluto commented on GitHub (Nov 1, 2026): Real-provider test-selection control for #8171: on main `6e9ee97a`, with `JAVA_HOME` unset and JDK 21 on `PATH`, the real Ghidra 12.1.4 COM verifier completed its public CLI/stdio MCP workflow with unchanged fixture and complete cleanup. The general verifier previously failed with that setup because its direct launcher lost the inspected JDK; a deliberately invalid explicit `JAVA_HOME` was separately rejected despite the valid PATH JDK. Details and the proposed full-lane regression are in #8171. A green real-provider lane therefore cannot establish another lane’s setup handoff; this is one host, and the general lane also needs the independent #8172 fix before a full completion assertion.

bsakaguchi commented

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

Author

Owner

@morluto commented on GitHub (Nov 1, 2026):

Distinguish real-provider workflow checks from agent-routing evaluation

Source check on REA main 6e9ee97a: the existing nativeProviderScenario is a useful open/close and missing-provider routing/cleanup check. It explicitly sets requiresEvidence: false, accepts the documented provider_unavailable outcome, and does not grade free-form answer correctness. The client verification guide likewise says it does not establish real native-engine analysis. This is a documented scope boundary, not a false pass against its current contract.

One possible additional, opt-in scenario is a real Ghidra or Kuna investigation on a source-owned target with independently established facts and a bounded counterexample, checking the agent's actual selected tools, source citations, unknowns, and cleanup. Keep unavailable providers reported as skipped/unavailable rather than a successful engine evaluation, and preserve the existing no-provider routing scenario. Establish credentials, cost, host/provider availability, grading and authorization before making it a gate. The scripted provider workflows and prompt comparison in #8435 did not measure autonomous selection; no real-agent evaluation was run for this observation.

@morluto commented on GitHub (Nov 1, 2026): ### Distinguish real-provider workflow checks from agent-routing evaluation Source check on REA main `6e9ee97a`: the existing [`nativeProviderScenario`](https://github.com/morluto/rea/blob/6e9ee97a69cb16c7150d8b550e705cba055ee4f0/tests/evaluation/model-evals/AgentEvaluationScenarios.ts#L34-L65) is a useful open/close and missing-provider routing/cleanup check. It explicitly sets `requiresEvidence: false`, accepts the documented `provider_unavailable` outcome, and does not grade free-form answer correctness. The [client verification guide](https://github.com/morluto/rea/blob/6e9ee97a69cb16c7150d8b550e705cba055ee4f0/docs/client-verification.md#agent-evaluation-and-conformance-records) likewise says it does not establish real native-engine analysis. This is a documented scope boundary, not a false pass against its current contract. One possible additional, opt-in scenario is a real Ghidra or Kuna investigation on a source-owned target with independently established facts and a bounded counterexample, checking the agent's actual selected tools, source citations, unknowns, and cleanup. Keep unavailable providers reported as skipped/unavailable rather than a successful engine evaluation, and preserve the existing no-provider routing scenario. Establish credentials, cost, host/provider availability, grading and authorization before making it a gate. The scripted provider workflows and prompt comparison in #8435 did not measure autonomous selection; no real-agent evaluation was run for this observation.

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

morluto/rea#6518

No description provided.

Rows
Columns