[GH-ISSUE #341] Run real-Hopper analyze_function dossier conformance #188

Open
opened 2026-10-15 18:22:14 +00:00 by bsakaguchi · 1 comment
Owner

Originally created by @morluto on GitHub (Jul 20, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/341

Coordinate with #54 to run the real-Hopper verifier for analyze_function dossiers: pseudocode, assembly, typed callers/callees, incoming/outgoing references, referenced strings/names, procedure-wide comments, and CFG successors.

Acceptance:

  • No field fabricates empty results for unsupported capabilities.
  • Collections report total/returned/truncated/continuation.
  • Real-Hopper fixtures prove non-empty reference, string, call-edge, comment, and CFG-successor cases.

Part of #31. Depends on #54.

Originally created by @morluto on GitHub (Jul 20, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/341 Coordinate with #54 to run the real-Hopper verifier for `analyze_function` dossiers: pseudocode, assembly, typed callers/callees, incoming/outgoing references, referenced strings/names, procedure-wide comments, and CFG successors. Acceptance: - No field fabricates empty results for unsupported capabilities. - Collections report total/returned/truncated/continuation. - Real-Hopper fixtures prove non-empty reference, string, call-edge, comment, and CFG-successor cases. Part of #31. Depends on #54.
Author
Owner

@BaaRai commented on GitHub (Oct 9, 2026):

I ran the real-Hopper conformance verifier end to end on Linux and can share the first complete run record for this issue's acceptance list. Everything below is from the pinned Hopper 6.4.2 Linux demo package (launcher SHA256 0294ced141cc373468ee22d8343e7dac41980cb05a937994ca81c9f09afe7ded, the build LinuxHopper.ts validates) in demo mode through the private-Xvfb lane, on Kali rolling (glibc 2.43, gcc 16.2.0, node 24.19), fixtures built from source on the host. This is a demo-licensed Linux run, so it does not replace the licensed macOS proof this issue still waits on, but it is real Hopper against the real verifier.

Run record (node scripts/verify-real-hopper-linux.mjs, run_id 566e00ec-8f4c-4ba2-99cd-096f4275da2f, observed 2026-10-09T13:24:37Z): exit 0, cleanShutdown: true, process lineage verified with zero retained descendants, unrelated-Hopper sentinel survived, 139-tool catalog parity, 171 successful plus 63 rejected boundary-contract calls, targets c / version-v2 / large.

Dossier acceptance facts that passed on real Hopper (Linux, ELF targets):

  • Named chains across main / rea_entry / rea_branch / rea_leaf with typed caller and callee identities, including the caller-of-entry and callee-of-branch edges (#342 scope).
  • Procedure-wide comments: the verifier's comment marker is written with set_comment and read back inside the dossier's comments collection.
  • Exact string references: REA_C_ENTRY and REA_C_LEAF appear in referenced_strings with typed provenance (encoding, encoding_status, termination, byte_length) and matching outgoing_references edges from the referencing instruction.
  • CFG successors with real addresses on the branch procedure, and non-empty bounded assembly for entry, branch, and leaf (#343 scope).
  • The assertion layer's value-only reference rejection and the global-name reference bound to the queried procedure address both held.

One verifier defect found and fixed: the navigation probe assumed the fixture's first instruction is longer than one byte. Kali's gcc (no -fcf-protection default) compiles rea_entry to push rbp; mov rbp,rsp, so the probed "interior" coordinate was itself an instruction boundary and the run rejected a correct bridge at the goto_address snap assertion. PR #1285 anchors the probe inside the first multi-byte instruction; with endbr64-style fixtures the same code runs the previous assertions unchanged (I verified both encodings end to end). The same + 1 interior pattern also sits in real-ghidra-boundaries.mjs's inspect_native_instruction probe; I left it alone since I could not execute that lane.

Two pinned-build string-typing boundaries the Linux demo exposes (these were the only parts of the oracle that cannot pass on this build, so I scoped them locally to complete the run):

  1. Long ASCII literals: unique-prefixed literals compiled at -O0 show typed up to 256 bytes whole; 300 to 512 bytes are typed as a 256-byte chunk (termination: "missing", provider display truncated with an ellipsis) followed by a remainder object; 1000 bytes and above are not typed at all, and no object intersects the literal's extent. The conformance fixture's 4120-byte literal therefore never enters list_strings or the dossier's referenced_strings, and the fragment-join oracle has no first fragment to join.
  2. Non-ASCII literals: REA_UTF8_é_😀, REA_LITERAL_…, and REA_LATIN1_ÿ are absent from the inventory while their ASCII neighbors are typed; the C fixture's whole inventory on this build is six objects (longest 25 bytes).

How would you like that boundary encoded? Options I can implement: shrink the long literal to a length the pinned Linux build types (at most 512 bytes) so the fragment-join path still exercises chunking on Linux, gate the long-literal and non-ASCII object oracles to darwin, or surface the pinned build's typing behavior as an explicit verifier-acknowledged limitation. The dossier facts above do not depend on these two cases, so #341's core acceptance is unaffected either way.

Full verifier JSON and the graduated-length probe data are available if useful.

<!-- gh-comment-id:6081900669 --> @BaaRai commented on GitHub (Oct 9, 2026): I ran the real-Hopper conformance verifier end to end on Linux and can share the first complete run record for this issue's acceptance list. Everything below is from the pinned Hopper 6.4.2 Linux demo package (launcher SHA256 `0294ced141cc373468ee22d8343e7dac41980cb05a937994ca81c9f09afe7ded`, the build `LinuxHopper.ts` validates) in demo mode through the private-Xvfb lane, on Kali rolling (glibc 2.43, gcc 16.2.0, node 24.19), fixtures built from source on the host. This is a demo-licensed Linux run, so it does not replace the licensed macOS proof this issue still waits on, but it is real Hopper against the real verifier. **Run record** (`node scripts/verify-real-hopper-linux.mjs`, run_id `566e00ec-8f4c-4ba2-99cd-096f4275da2f`, observed 2026-10-09T13:24:37Z): exit 0, `cleanShutdown: true`, process lineage verified with zero retained descendants, unrelated-Hopper sentinel survived, 139-tool catalog parity, 171 successful plus 63 rejected boundary-contract calls, targets `c` / `version-v2` / `large`. **Dossier acceptance facts that passed on real Hopper (Linux, ELF targets):** - Named chains across `main` / `rea_entry` / `rea_branch` / `rea_leaf` with typed caller and callee identities, including the caller-of-entry and callee-of-branch edges (#342 scope). - Procedure-wide comments: the verifier's comment marker is written with `set_comment` and read back inside the dossier's `comments` collection. - Exact string references: `REA_C_ENTRY` and `REA_C_LEAF` appear in `referenced_strings` with typed provenance (`encoding`, `encoding_status`, `termination`, `byte_length`) and matching `outgoing_references` edges from the referencing instruction. - CFG successors with real addresses on the branch procedure, and non-empty bounded assembly for entry, branch, and leaf (#343 scope). - The assertion layer's value-only reference rejection and the global-name reference bound to the queried procedure address both held. **One verifier defect found and fixed:** the navigation probe assumed the fixture's first instruction is longer than one byte. Kali's gcc (no `-fcf-protection` default) compiles `rea_entry` to `push rbp; mov rbp,rsp`, so the probed "interior" coordinate was itself an instruction boundary and the run rejected a correct bridge at the `goto_address` snap assertion. PR #1285 anchors the probe inside the first multi-byte instruction; with endbr64-style fixtures the same code runs the previous assertions unchanged (I verified both encodings end to end). The same `+ 1` interior pattern also sits in `real-ghidra-boundaries.mjs`'s `inspect_native_instruction` probe; I left it alone since I could not execute that lane. **Two pinned-build string-typing boundaries the Linux demo exposes** (these were the only parts of the oracle that cannot pass on this build, so I scoped them locally to complete the run): 1. Long ASCII literals: unique-prefixed literals compiled at `-O0` show typed up to 256 bytes whole; 300 to 512 bytes are typed as a 256-byte chunk (`termination: "missing"`, provider display truncated with an ellipsis) followed by a remainder object; 1000 bytes and above are not typed at all, and no object intersects the literal's extent. The conformance fixture's 4120-byte literal therefore never enters `list_strings` or the dossier's `referenced_strings`, and the fragment-join oracle has no first fragment to join. 2. Non-ASCII literals: `REA_UTF8_é_😀`, `REA_LITERAL_…`, and `REA_LATIN1_ÿ` are absent from the inventory while their ASCII neighbors are typed; the C fixture's whole inventory on this build is six objects (longest 25 bytes). How would you like that boundary encoded? Options I can implement: shrink the long literal to a length the pinned Linux build types (at most 512 bytes) so the fragment-join path still exercises chunking on Linux, gate the long-literal and non-ASCII object oracles to darwin, or surface the pinned build's typing behavior as an explicit verifier-acknowledged limitation. The dossier facts above do not depend on these two cases, so #341's core acceptance is unaffected either way. Full verifier JSON and the graduated-length probe data are available if useful.
Sign in to join this conversation.
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#188
No description provided.