Two legs of one proof
Two columns of boxes read top down. Leg one, execute and compare: ledger.c is the original compiled natively at -O1, percent_change_wide.c is the candidate renamed cand_percent_change, driver.c links both into one program named differential, the input grid has 92 cells in 9 hazard classes, and the results are 28 mismatches for the plausible pair and 0 for the equal pair. Leg two, recompile and compare: grade in ledger-x86_64-O1.o is 46 bytes with one R_X86_64_PC32 relocation, grade_switch.c is compiled with clang for x86_64-unknown-linux-gnu at -O1, mask_relocations zeroes 4 bytes at offset 38 on both sides, the relocation records .rodata+0x10 and .rodata-0x4 have the same shape, read_table gives 1, 2, 3, 4, 4 on both sides, and grade_case10_wrong gives 1, 2, 3, 4, 3.
LEG ONE: EXECUTE AND COMPARE
LEG TWO: RECOMPILE AND COMPARE
ledger.c
the original, compiled natively at -O1
percent_change_wide.c
the candidate, renamed cand_percent_change
differential
driver.c links both into one program
input grid
92 cells in 9 hazard classes
ledger-x86_64-O1.o
grade: 46 bytes, one R_X86_64_PC32
grade_switch.c
clang -target x86_64-unknown-linux-gnu -O1
mask_relocations
zero 4 bytes at offset 38 on both sides
relocation records
.rodata+0x10 and .rodata-0x4, same shape
plausible pair
28 mismatches
equal pair
0 mismatches
read_table
1, 2, 3, 4, 4
grade_case10_wrong
1, 2, 3, 4, 3