Manuals / Reverse Engineering 101 / Part 7 · Rebuild and Prove
7.1

verify_reconstruction

verify_reconstruction grades each declared claim against one comparison record, and its pass says the provider text matched, never that two functions are equal.

You have two builds of ledger.c on disk, the -O1 and the -O2 executables, and two compare_functions records from Section 5.5. You want rea to tell you whether total is the same function in both. The tool for that question is verify_reconstruction, and the capture called it once, with four claims, and got two passes and two failures. When you finish this section, you can write a specification of structural claims and read the status rea returns for each claim. You can also say what a pass does and does not prove.

The specification

Specification: the input of verify_reconstruction: a name and a list of at least one claim. Each claim has a claim_id, a title, a kind, a dimension, and a comparison_evidence_id (the capture). The last one is the ev_ id of one comparison record already in the session. The kind names the producer of that record. A behavioral claim points at a compare_process_captures record, a structural-function claim at a compare_functions record, and a structural-artifact claim at a compare_artifacts record. A structural-function claim names one of nine dimensions: overall, identity, pseudocode, assembly, comments, calls, references, strings_names, or cfg.

The capture kit built four claims over the two comparison records of Section 5.5: pseudocode and assembly for percent_change, and pseudocode and assembly for total.

the specification the capture sentjsonFull log
{
  "request": {
    "jsonrpc": "2.0",
    "id": 22,
    "method": "tools/call",
    "params": {
      "name": "verify_reconstruction",
      "arguments": {
        "specification": {
          "name": "ledger functions rebuilt at -O2 against the -O1 build",
          "claims": [
            {
              "claim_id": "percent-change-pseudocode",
              "title": "percent_change: the Ghidra pseudocode is the same text in the -O1 and -O2 builds",
              "kind": "structural-function",
              "dimension": "pseudocode",
              "comparison_evidence_id": "ev_2161e17a…"
            },
            …
            {
              "claim_id": "total-assembly",
              "title": "total: the Ghidra assembly is the same text in the -O1 and -O2 builds",
              "kind": "structural-function",
              "dimension": "assembly",
              "comparison_evidence_id": "ev_40ba96d8…"
            }
          ]
        }
      }
    }
  },
  …
}
The second and third claims are cut. The response follows the request in the same file.

The tool has no CLI command. It is one of the 65 MCP tools without a CLI command, so a one-shot rea call cannot run it. Over MCP the handler takes the bundle of the current connection with session.exportEvidenceBundle() and verifies the specification against it. A claim whose comparison id is not in that bundle fails the whole call with Missing comparison Evidence. A comparison whose two sources are not analyze_function records fails the source check.

That rule explains the order of the capture. close_binary at step 15 cleared the retained records of the -O1 target. The two -O1 dossiers came back into the ledger at steps 20 and 21. compare_functions records its two inline inputs before it records the comparison. The import_evidence_bundle call at step 23 then reported imported: 6 and total: 15 (the capture). Bundle O1 holds eight records, and the two comparisons had already restored two of them.

What rea returned

The response is an Evidence record like every other result, with subject: null, provider rea-reconstruction-verifier version 1, predicate rea.reconstruction-verification, confidence: "derived", and authority: "analyst-inference". The parameters hold the SHA-256 of the specification and the claim ids, so the id of the record changes when a claim changes.

the verification record, head and summaryjsonFull log
      "structuredContent": {
        "evidence_id": "ev_ccbaea4b…",
        "subject": null,
        "provider": {
          "id": "rea-reconstruction-verifier",
          "name": "REA reconstruction verifier",
          "version": "1"
        },
        …
        "normalized_result": {
          "status": "fail",
          "specification_sha256": "9e8d22fa…",
          "summary": {
            "total": 4,
            "passed": 2,
            "failed": 2,
            "unknown": 0,
            "behavioral": 0,
            "structural": 4
          },
          …
          "limitations": [
            "Pass means every declared claim passed; it does not establish global implementation equivalence."
          ]
        },
        "confidence": "derived",
        "authority": "analyst-inference",
        …
The analysis_profile, the per-claim items, the probes, and the evidence links are cut.

The overall status follows one rule: fail when any claim failed, otherwise unknown when any claim is unresolved, otherwise pass. The summary counts the claims by status and by kind. The record's own limitations add "Artifact identity is unavailable for this observation.", which createEvidence appends to any record without a subject.

The status of one claim

Claim status: pass, fail, or unknown, computed from three inputs in a fixed order. First, any limitation makes the claim unknown. A limitation comes from the authority of the sources.

Incomplete call coverage in a source dossier is also a limitation. It applies to a calls claim, and to an overall claim with no other changed dimension. Second, an observed status of changed, added, removed, or contradiction makes the claim fail. Third, an observed status of unknown or truncated, or an open residual unknown on the comparison, makes the claim unknown. In all other cases the claim is pass.

For a structural-function claim the observed status is the status of the named dimension in the comparison record.

the total-assembly claimjsonFull log
                "claim_id": "total-assembly",
                "kind": "structural-function",
                "dimension": "assembly",
                "status": "fail",
                "observed_status": "changed",
                "comparison_evidence_id": "ev_40ba96d8…",
                "left_evidence_ids": [
                  "ev_a1fe53ff…"
                ],
                "right_evidence_ids": [
                  "ev_bfe3275b…"
                ],
                …
                "unknown_ids": [
                  "unk_823f4184…"
                ],
                "limitations": [
                  "Artifact identity is unavailable for this observation.",
                  …
                  "Residual unknown: Function comparison is changed (comparison ev_40ba96d8…)",
                  …
                ]
The evidence_links array and 28 of the 30 limitation strings are cut. The Residual unknown line is the one this claim adds to the limitations of the comparison record.

The two percent_change claims pass, although the comparison record ev_2161e17a is unknown overall. Each claim reads only its own dimension, and ev_2161e17a reports both pseudocode and assembly unchanged. Its one unknown dimension is references. The residual unknown it opened names only overall and references, so neither claim lists it in unknown_ids. A claim on references or on overall would have read unknown.

The two total claims fail because ev_40ba96d8 reports changed for pseudocode and assembly, and five of its eight dimensions changed in all. The unknown_ids entry is not something the verifier invented. compare_functions records a residual unknown whenever its status is not unchanged, with the question Function comparison is changed (comparison ev_...) and severity medium for a change. The verifier found that unknown in the bundle, listed its id on both total claims, and copied its question into the limitations. The claim still reads fail, because a changed observation outranks an open unknown in the order above.

Had a claim come out unknown, the call would have recorded one more unknown of its own. When the overall status is unknown, the handler records the question "Does the reconstruction satisfy every declared claim?" with the probes the verifier recommends. A pass and a fail record nothing new, and recommended_probes was empty here.

Fig. 7.1four claims over two comparison recordstree
Four claims over two comparison records A tree. The verification record ev_ccbaea4b at the top has status fail with two passed and two failed claims. Its left column holds the two percent_change claims, pseudocode and assembly, both pass with observed_status unchanged, pointing at the comparison record ev_2161e17a whose left side is ev_b492c85e from ledger-arm64-O1 and right side ev_142cc943 from ledger-arm64-O2. That comparison is unknown on references, and its residual unknown names only overall and references, so neither claim lists it. The right column holds the two total claims, both fail with observed_status changed, pointing at the comparison record ev_40ba96d8 with sides ev_a1fe53ff and ev_bfe3275b, which recorded the residual unknown unk_823f4184, Function comparison is changed. verify_reconstruction ev_ccbaea4b status fail: 2 passed, 2 failed, 0 unknown percent-change-pseudocode status pass, observed_status unchanged percent-change-assembly status pass, observed_status unchanged comparison_evidence_id compare_functions ev_2161e17a left ev_b492c85e (ledger-arm64-O1) right ev_142cc943 (ledger-arm64-O2) unknown_ids empty no unknown in the claim scope its unknown names overall and references total-pseudocode status fail, observed_status changed total-assembly status fail, observed_status changed comparison_evidence_id compare_functions ev_40ba96d8 left ev_a1fe53ff (ledger-arm64-O1) right ev_bfe3275b (ledger-arm64-O2) unknown_ids unk_823f4184 Function comparison is changed (medium)
Each claim takes its status from one dimension of one comparison record, and the total claims also carry the unknown that compare_functions recorded. Read top down. The verification record cites four claims, each claim cites one comparison record, and each comparison record cites a left and a right dossier. Amber claims passed and dashed rose claims failed. Ids are cut to their first eight hex digits.

What a pass does not prove

The fixed limitation of every verification record says it: "Pass means every declared claim passed; it does not establish global implementation equivalence.". The claim a structural-function dimension can pass is "same provider text", because compare_functions line-diffs the pseudocode and the assembly that Ghidra printed. The pseudocode and assembly dimensions carry a caveat in every comparison record: "Exact provider text is compared without address or generated-name normalization; layout-only differences do not establish a behavior change." The assembly dimension adds: "Assembly is opaque provider text; relocation normalization is unavailable." (the capture). Nothing in rea 6.7.0 runs a function or compiles one. A passed claim says that two decompiler outputs matched line for line, and a failed claim says they did not.

Two consequences follow for the ledger fixture. The total claims failed although both builds came from the same source line. -O2 unrolled the loop into 62 instructions where -O1 had 13 (the captures). Different text does not mean different behaviour.

The reverse holds too. A rebuild with a wrong constant in a lookup table has the same assembly text as the original. The text never shows the one data byte that differs, so a text claim can pass on a wrong function. Section 7.2 builds the two checks that settle both cases.

The rea repository has a wider verifier for its own use. The readiness page of the rea docs describes npm run verify:readiness, a nine-stage conformance run with a stage named verify-reconstruction-closure, and says what it is:

Its aggregation rule is the one to copy into your own harness:

rea (rea-agents) with the Ghidra provider rea-agents 6.7.0, Ghidra 12.1.4 · 27dc42d · 2026-10-18 · Edition 2026.10