v0.5.0 — execution as judge

The strongest grounding: verify a function reconstruction by running it, not reading it (the ExeBench / LLM4Decompile re-executability methodology).

Added

• behavior_equiv claim: the original function (offset into the binary, or inline code) and a candidate (expr over x0,x1,... or candidate_code hex) are run over shared inputs and their outputs compared. A mismatch returns a concrete counterexample input; agreement is reported honestly as "equivalent over N inputs (tested, not proven)".
• Runs on Unicorn (x86-64 SysV convention by default), no compiler or model needed to verify. Behavioral equivalence is the highest-weighted claim; inline originals are self-referential (weight 0).
• Safe expression evaluator; CLI prints the counterexample.

163 tests. pip install -U reverify