morluto/rea

Fork 0

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

[GH-ISSUE #8405] [Design] Report omitted caller targets in the real Kuna verifier #6587

New issue

Open

opened 2026-11-01 21:12:28 +00:00 by bsakaguchi · 2 comments

bsakaguchi commented

2026-11-01 21:12:28 +00:00

Owner

Originally created by @morluto on GitHub (Nov 1, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/8405

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

Should the real Kuna verifier's report explicitly list caller-supplied binary pairs omitted because none of the requested function names appeared in their symbol inventories, and show requested-versus-found names per examined pair?

Context and evidence

On clean main 6e9ee97a, macOS arm64, Node 24.22.1, and real Kuna 1.986, I created three owned Mach-O binary pairs, each with a symbolized file and a stripped copy:

Caller directory	Requested symbols observed by `nm`	Reported verification
`left`	`audit_left`	Both binaries, `audit_left`
`right`	`audit_right`	Both binaries, `audit_right`
`unmatched`	Neither requested name	No result entry

node scripts/verify-real-kuna.mjs --targets <matrix> --functions audit_left,audit_right exited 0 with status: "passed". The report listed the four matching caller variants and the built-in fixture pair. It listed the tested function name for each reported variant, but did not include unmatched or a skipped-target reason. Cleanup was complete, process lineage verified, and no descendants remained. All six caller binary hashes were unchanged; none was executed.

The current documentation explicitly says names missing from every supplied target cause refusal. That global selection behavior is deliberate evidence here, not a claim the verifier promises each function in every binary. A separate mixed known-plus-globally-missing selection correctly failed as documented (#8274). The gap is that a reader of the JSON report alone cannot see an examined caller pair that was omitted, or distinguish its unmatched selection from an absent input. nm absence is not proof the binary contains no such code.

Expected interaction with targets

Read caller-supplied binaries, run the selected local analysis provider and build the existing owned fixture; write only temporary verifier artifacts and an explicitly requested report. Do not execute targets.

Boundary details

Preserve the existing valid use case where requested functions are distributed across different caller binaries. Report exact selected names and binary identity, distinguish no matching symbol from failed inspection or an absent stripped counterpart, and do not infer code absence from symbol inventory. Keep the cleanup and process-lineage result.

Options and tradeoffs

Compare adding a bounded per-pair selection/omission section with requiring a caller-selected coverage policy. A blanket requirement that every requested name occur in every binary would change the current global-selection semantics and may reject useful matrices. The result already includes matched function rows for binaries it verifies; avoid duplicating those observations without need.

Verification available so far

I have a prototype or observed results.

Success criteria and open questions

Exercise a mixed matrix where names are distributed across binaries, an unmatched pair, all names absent, and a failed symbol inspection; verify every examined pair has a truthful disposition in both successful and failed reports, and preserve complete cleanup. Other hosts, --compare-ghidra, nonregular entries, failed nm, and large matrices were not tested in this control.

References

Related real-provider coverage and the globally missing-name negative control: #8274. The independently observed upstream test-selection behavior is Noelo-Lab/kuna#1375 and uses a different harness/contract. Last known good: NOT_ENOUGH_INFO.

@gensokyo-dev @kaoru0822-kitauji @N0zoM1z0

Originally created by @morluto on GitHub (Nov 1, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/8405 ### 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 Should the real Kuna verifier's report explicitly list caller-supplied binary pairs omitted because none of the requested function names appeared in their symbol inventories, and show requested-versus-found names per examined pair? ### Context and evidence On clean main `6e9ee97a`, macOS arm64, Node 24.22.1, and real Kuna 1.986, I created three owned Mach-O binary pairs, each with a symbolized file and a stripped copy: | Caller directory | Requested symbols observed by `nm` | Reported verification | | --- | --- | --- | | `left` | `audit_left` | Both binaries, `audit_left` | | `right` | `audit_right` | Both binaries, `audit_right` | | `unmatched` | Neither requested name | No result entry | `node scripts/verify-real-kuna.mjs --targets <matrix> --functions audit_left,audit_right` exited 0 with `status: "passed"`. The report listed the four matching caller variants and the built-in fixture pair. It listed the tested function name for each reported variant, but did not include `unmatched` or a skipped-target reason. Cleanup was complete, process lineage verified, and no descendants remained. All six caller binary hashes were unchanged; none was executed. The current documentation explicitly says names missing from **every** supplied target cause refusal. That global selection behavior is deliberate evidence here, not a claim the verifier promises each function in every binary. A separate mixed known-plus-globally-missing selection correctly failed as documented (#8274). The gap is that a reader of the JSON report alone cannot see an examined caller pair that was omitted, or distinguish its unmatched selection from an absent input. `nm` absence is not proof the binary contains no such code. ### Expected interaction with targets Read caller-supplied binaries, run the selected local analysis provider and build the existing owned fixture; write only temporary verifier artifacts and an explicitly requested report. Do not execute targets. ### Boundary details Preserve the existing valid use case where requested functions are distributed across different caller binaries. Report exact selected names and binary identity, distinguish no matching symbol from failed inspection or an absent stripped counterpart, and do not infer code absence from symbol inventory. Keep the cleanup and process-lineage result. ### Options and tradeoffs Compare adding a bounded per-pair selection/omission section with requiring a caller-selected coverage policy. A blanket requirement that every requested name occur in every binary would change the current global-selection semantics and may reject useful matrices. The result already includes matched function rows for binaries it verifies; avoid duplicating those observations without need. ### Verification available so far I have a prototype or observed results. ### Success criteria and open questions Exercise a mixed matrix where names are distributed across binaries, an unmatched pair, all names absent, and a failed symbol inspection; verify every examined pair has a truthful disposition in both successful and failed reports, and preserve complete cleanup. Other hosts, `--compare-ghidra`, nonregular entries, failed `nm`, and large matrices were not tested in this control. ### References Related real-provider coverage and the globally missing-name negative control: #8274. The independently observed upstream test-selection behavior is [Noelo-Lab/kuna#1375](https://github.com/Noelo-Lab/kuna/issues/1375) and uses a different harness/contract. Last known good: NOT_ENOUGH_INFO. @gensokyo-dev @kaoru0822-kitauji @N0zoM1z0

bsakaguchi added the

enhancement

triage

labels

2026-11-01 21:12:28 +00:00

bsakaguchi commented

2026-11-01 21:12:28 +00:00

Author

Owner

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

Cross-provider comparison control

I repeated the owned three-pair matrix with --compare-ghidra, real Kuna 1.986 and Ghidra 12.1.4/JDK 21 on macOS arm64. The verifier again returned passed with complete cleanup and verified process lineage. For left and left.stripped, both providers' result rows named only audit_left; for right and its stripped copy, both named only audit_right. The unmatched pair remained absent from the results for both providers. All six caller binary hashes were unchanged, and the targets were not executed.

This confirms the omission occurs before provider comparison in this control. It does not establish a decompilation mismatch, require each name in each binary, or measure any performance difference. The results entries for selected pairs already identify the functions each provider ran; the unresolved reporting question is how to preserve examined-but-unselected pairs and their reason.

@morluto commented on GitHub (Nov 1, 2026): ### Cross-provider comparison control I repeated the owned three-pair matrix with `--compare-ghidra`, real Kuna 1.986 and Ghidra 12.1.4/JDK 21 on macOS arm64. The verifier again returned passed with complete cleanup and verified process lineage. For `left` and `left.stripped`, both providers' result rows named only `audit_left`; for `right` and its stripped copy, both named only `audit_right`. The unmatched pair remained absent from the results for both providers. All six caller binary hashes were unchanged, and the targets were not executed. This confirms the omission occurs before provider comparison in this control. It does not establish a decompilation mismatch, require each name in each binary, or measure any performance difference. The `results` entries for selected pairs already identify the functions each provider ran; the unresolved reporting question is how to preserve examined-but-unselected pairs and their reason.

bsakaguchi commented

2026-11-01 21:12:28 +00:00

Author

Owner

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

Draft #8406 implements an explicit caller-target symbol-scan report while retaining the documented global-selection policy. It records selected and unmatched examined binaries, and retains a failed inspection with earlier entries and an incomplete scan marker. The scan is limited to non-.stripped entries in immediate flavor directories; results remains the source for which variants actually completed verification.

On macOS arm64, the real Kuna 1.986 / Ghidra 12.1.4 mixed matrix passed with the unmatched pair present in both stdout and --report, unchanged target hashes, and complete cleanup. A controlled failing nm wrapper produced a failed report with the earlier selected target, the failing input, and symbol_scan_complete: false; cleanup completed. This failure was injected, and the provider analysis lane did not start in that control. Four targeted boundary tests, check:fast, and docs:check passed on the final change; the new report assertion failed against main. Windows/Linux hosts and large matrices remain unverified.

@morluto commented on GitHub (Nov 1, 2026): Draft #8406 implements an explicit caller-target symbol-scan report while retaining the documented global-selection policy. It records selected and unmatched examined binaries, and retains a failed inspection with earlier entries and an incomplete scan marker. The scan is limited to non-`.stripped` entries in immediate flavor directories; `results` remains the source for which variants actually completed verification. On macOS arm64, the real Kuna 1.986 / Ghidra 12.1.4 mixed matrix passed with the unmatched pair present in both stdout and `--report`, unchanged target hashes, and complete cleanup. A controlled failing `nm` wrapper produced a failed report with the earlier selected target, the failing input, and `symbol_scan_complete: false`; cleanup completed. This failure was injected, and the provider analysis lane did not start in that control. Four targeted boundary tests, `check:fast`, and `docs:check` passed on the final change; the new report assertion failed against main. Windows/Linux hosts and large matrices remain unverified.

bsakaguchi referenced this issue

2026-11-01 21:47:27 +00:00

[PR #6587] [CLOSED] fix(setup): write the native OpenCode table inherited from any layer #7380

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#6587

No description provided.

Rows
Columns