SERGIO RODRIGUEZOne check.
Two machine forms.
Four pure functions. Two compiler builds.
One boundary the machine does not check for you.
01 / THE RECOVERED PROGRAM
Follow the branch.
The graph and listing come from Ghidra.
Choose a function and compare the builds.
Select a recovered function when the report loads.
CONTROL FLOW
—Edges follow recorded destinations. Layout is editorial; instruction addresses remain unchanged.
RECOVERED C
—Loading analysis…
ASSEMBLY / BYTES
—Loading listing…
Default Ghidra type inference. Exported function names survive in this fixture; original parameter names and types were not supplied to the decompiler. Recovered C is an interpretation, not recovered source text.
02 / CHALLENGE THE PREDICATE
A small input.
A different answer.
Unsigned addition can wrap before the comparison. The corrected predicate bounds the offset before subtraction.
These editable inputs run the equivalent arithmetic in your browser. The recorded native DLL tests are a separate result below.
03 / THE EXECUTION RECORD
Put the result
under inspection.
| Build | Byte inputs | Range triples | Legacy false accepts | Corrected errors |
|---|
What ran
Clang compiled the same original C source at O0 and O2 into x64 DLLs with no entry point, imports or I/O. Python called their four exported functions. Ghidra imported each build and exported decompiled C, instructions and basic-block destinations.
What the result covers
All 256 byte values. For ranges: every triple from 12 boundary values, plus 20,000 seeded random triples. The reference adds with Python integers, which do not wrap. The full 32-bit triple space was not exhausted.
What it does not establish
These are controlled fixtures. They do not demonstrate a vulnerability in a third-party product, memory corruption, exploitation, trading performance or the behavior of an unknown executable.
Inspect provenance, build hashes & reproducibility
Loading manifest…
04 / WHY THE TWO VIEWS MATTER
The graph can shrink.
The mistake can remain.
Optimization can replace branch-shaped source with conditional moves, flag operations or straight-line instructions. A smaller control-flow graph is a compiler result. It does not establish a stronger validation rule.
Switch from O0 to O2, compare the exact instruction listing, then try total=16, offset=4294967295, count=2. The native regression record keeps the same counterexample visible in both builds. The corrected comparison avoids forming the wrapping sum.
The same distinction appears in Boolean decoding: “nonzero” is a predicate; “canonical encoded byte” is a format constraint. Native execution and decompilation provide complementary evidence, with their assumptions stated separately.