A proof harness beyond compare_functions

You rebuilt percent_change from the pseudocode in Section 4.6, kept the long the decompiler offered, and ten hand-written tests pass. Section 7.1 showed that rea can only tell you whether two Ghidra texts match. The proof that your rebuild equals the original has to come from a harness you run yourself. Lesson 36 builds one in the Python standard library.

The capture kit ran that harness over ledger-x86_64-O1.o and recorded four files under 17-. When you finish this section, you can run both legs of the harness over your rebuild and read the mismatch rows and the byte report. You can then say which hazard class or which relocation each failure names.

What compare_functions can see

compare_functions compares two analyze_function records in eight dimensions: identity, pseudocode, assembly, comments, calls, references, strings_names, and cfg (the capture). The pseudocode and assembly dimensions are a bounded line diff of two strings. The status is unknown when the diff takes more than 100 ms or more than 10,000 edits. The assembly dimension carries two fixed limitations:

              "dimension": "assembly",
              "left_count": 161,
              "right_count": 161,
              "evidence_links": [
                "ev_b492c85e…",
                "ev_142cc943…"
              ],
              "limitations": [
                "Exact provider text is compared without address or generated-name normalization; layout-only differences do not establish a behavior change.",
                "Assembly is opaque provider text; relocation normalization is unavailable."
              ],
              "status": "unchanged",

For total the same comparison reported changed in five dimensions (the capture). The pseudocode grew from 300 to 2,904 characters and the assembly from 336 to 1,866. The two records came from one source line compiled at -O1 and -O2. A text comparison therefore says nothing about behaviour in either direction. The same function can print as different text, and a wrong function can print as the same text.

rea 6.7.0 has no compiler replay and no relocation-aware byte comparison. The two legs below are the part rea leaves to you.

Leg one: execute and compare

Input grid: the list of input cells the harness feeds to the original and to the rebuild. Each class of cells stands for one hazard the listing shows. The lesson's input_grid() takes every pair of ten before values and seven after values for percent_change, and 22 scores for grade, 92 cells in all. Each cell has a class, and the class says why it exists.

{
  "cells": 92,
  "classes": {
    "overflow": 32,
    "negative": 17,
    "boundary": 14,
    "plain": 12,
    "zero guard": 7,
    "negative truncation": 5,
    "beyond the switch": 2,
    "rounding": 2,
    "trap": 1
  },
  …
}

The zero guard cells take the before == 0 branch. The negative cells check that division truncates toward zero, so -9 / 10 is 0 and -10 / 10 is -1. The rounding cells check that the multiply happens before the divide. The overflow cells make (after - before) * 100 exceed 32 bits. The one trap cell makes the wrapped product equal INT_MIN with before equal to -1.

For grade, the boundary cells sit on both sides of 60, 70, 80, 90, and 100. The two cells beyond the switch are 110 and INT_MAX.

The harness compiles ledger.c and one candidate per function into one program with the lesson's driver.c. The candidate is renamed with -Dpercent_change=cand_percent_change -Dgrade=cand_grade, so both versions link under different names. The driver reads one cell per line, prints both results, and turns a SIGFPE into the value trap.

The ELF object cannot run on the Mac that recorded the capture. The oracle there is ledger.c compiled natively at -O1, and the report says so in original_kind: fixture-source. The capture ran two pairs. The plausible pair is percent_change_wide.c, the pseudocode's long, with grade_thresholds.c, four if statements on 90, 80, 70, and 60:

int percent_change(int before, int after) {
    if (before == 0) return 0;
    return (int)(((long)after - before) * 100 / before);
}

  "candidates": {
    "percent_change": "phases/13-tools-and-protocols/36-rebuild-and-prove-equal/code/fixtures/candidates/percent_change_wide.c",
    "grade": "phases/13-tools-and-protocols/36-rebuild-and-prove-equal/code/fixtures/candidates/grade_thresholds.c"
  },
  "original": "fixtures/ledger.c compiled with the host clang at -O1",
  "original_kind": "fixture-source",
  "host": "aarch64 Darwin",
  "arch": "aarch64",
  "naive_passed": true,
  "cells": 92,
  "mismatches": [
    {
      "function": "percent_change",
      "args": [
        3,
        2147483647
      ],
      "kind": "overflow",
      "original": -133,
      "candidate": -1431655899,
      "match": false
    },
    …
    {
      "function": "grade",
      "args": [
        110
      ],
      "kind": "beyond the switch",
      "original": 0,
      "candidate": 4,
      "match": false
    },
    …
  ],

All ten naive cases pass, and 28 of the 92 cells fail. The 26 percent_change failures are all overflow cells with |before| > 1. The original wraps the product to 32 bits and then divides, and the long rebuild divides the unwrapped product. For before equal to 1 or -1 the two agree by accident, because the 64-bit quotient truncates back to the wrapped value. The two grade failures are 110 and INT_MAX. The original switch has no case for tens of 11 and above and returns 0, and the threshold rebuild returns 4.

The equal pair is percent_change_mul_first.c, which is 100 * (after - before) / before, with grade_switch.c, the original source. It agrees on all 92 cells and the model of the listing disagrees with the observed original on none (the capture). One row of that file deserves a look:

    {
      "function": "percent_change",
      "args": [
        -1,
        536870911
      ],
      "kind": "trap",
      "original": -2147483648,
      "candidate": -2147483648,
      "match": true
    },

The difference is 536870912, the 32-bit product wraps to -2147483648, and the divisor is -1. On x86-64 IDIV raises the divide error exception, because the quotient does not fit in 32 bits. On AArch64 SDIV has no trap and returns -2147483648. The report records "arch": "aarch64" with the row, and a run of the same grid on a Linux x86-64 host records the string trap instead. The oracle depends on the architecture, so a proof names the host that ran it.

Leg two: recompile and compare bytes

Relocation masking: zeroing the bytes of every relocation field in both functions before comparing them. The two steps that follow compare the relocation records by offset, type, and target section, then read the bytes each relocation points at. The lesson's ElfObject reads the ELF64 object with struct.unpack_from, and mask_relocations(), prove_bytes(), and read_table() do the three steps. Without the first step a plain byte compare rejects a correct rebuild whose table sits at another offset. Without the third step it accepts a wrong one.

      "grade": {
        "section": ".text",
        "start": 16,
        "size": 46,
        "bytes": "4863c74869c0676666664889c148c1f92248c1e83f01c183c1fa31c083f904770c89c8488d0d000000008b0481c3",
        "relocations": [
          {
            "offset": 38,
            "type": "R_X86_64_PC32",
            "symbol": ".rodata",
            "addend": 16
          }
        ]
      },

grade is 46 bytes with one R_X86_64_PC32 relocation at offset 38, the displacement of the lea that loads the table address. In a RELA object the addend lives in the record and the four field bytes are zero. The hex above shows them as 00000000 before 8b0481c3. The target is .rodata+0x10, and because the field ends its instruction the CPU adds 4, so the table starts at .rodata+0x14. Each candidate was compiled with clang -target x86_64-unknown-linux-gnu -O1 -fno-asynchronous-unwind-tables -c, the fixture command, and compared with this entry.

      "candidate": "grade_case10_wrong",
      …
      "original_size": 46,
      "candidate_size": 46,
      "masked_equal": true,
      …
      "relocations_match": true,
      "relocations": [
        {
          "offset": 38,
          "type": "R_X86_64_PC32",
          "original_target": ".rodata+0x10",
          "candidate_target": ".rodata-0x4",
          "same_shape": true
        }
      ],
      …
      "status": "fail",
      "reasons": [
        "referenced constants differ: [1, 2, 3, 4, 4] vs [1, 2, 3, 4, 3]"
      ]

grade_case10_wrong.c returns 3 for case 10. Its 46 code bytes equal the original after masking, and its one relocation has the same offset, type, and section. Only the five table entries differ.

The addends differ in every grade candidate, +0x10 against -0x4. The original object holds the labels table of grade_label in .rodata before the switch table, and the candidate object does not. A different addend is a different offset, so the harness compares the shape of the record and then reads the table through it. Both tables read 1, 2, 3, 4, 4 for the two correct rebuilds.

Two rows say what a byte match means. percent_change_split.c has different source text and identical bytes, because clang treats signed overflow as undefined and folds the two multiplies into one. grade_table.c reaches the same table from an array index as the original does from a switch. A match proves that this compiler with these flags produced the same code from the candidate. It does not prove that the candidate is the original text.

Size is a diagnostic and never an acceptance. percent_change_wide is 26 bytes because movslq, imulq, cqto, and idivq replaced the 32-bit forms. The listing had shown the widths before any compile.

What the 2026 measurements add

The hazards in the grid are not special to this fixture. Liu, Raff, and Micinski measured eight decompilation systems in nine configurations in 2026 (arXiv 2609.05370). Candidates that passed every test of the benchmark still diverged on fuzzed inputs. That happened for 4.9 percent of them overall and for up to 13 percent in one system. The test set was 300 library functions and 287 functions with disclosed vulnerabilities. There the strongest refinement model raised Ghidra's build rate from 75 to 90 percent, and the behavioural match rate fell from 74 to 62 percent.

They traced the cause to invented fields, types, callees, and guards that replaced the visible unknowns a decompiler leaves behind. percent_change_wide.c is an invented type, and grade_thresholds.c is an invented guard. Both compile, both pass the ten naive cases, and both count as re-executable under a benchmark that recompiles and runs the assertions it includes. The authors propose per-function driver synthesis and fuzzing from the reference, which is leg one with a generated grid.

The lesson adds a third source for the constant check. The rea evidence pages describe a reconstruction project that compared instruction bytes while trusting the relocation target. A source literal of 0.0 passed against a target literal of 128.0 until the project audited 1,548 floating-point references. grade_case10_wrong.c is this manual's version of that defect, and read_table() is the audit.