Skip to content

Rewynth 0.4.0: compare the next state

Latest

Choose a tag to compare

@nazeeh111 nazeeh111 released this 16 Oct 08:35
0042974

An edit can return the right value while losing the state update needed by the next call. Rewynth now recovers and jointly compares an ARM64 function’s return and every word of its declared state buffer.

  • Recover, edit and compare bounded state transitions through the CLI and workbench.
  • Inspect complete counterexamples and exact 64-bit memory traces; save and reopen the full workspace.
  • Export a portable pure-transition C function.
  • Run the included PCG32 lesson to see a lost-store edit rejected despite an equal immediate return. The unchanged upstream source is attributed and included.

The supported contract is one pointer to 1–3 fixed 64-bit words, with at most four logical inputs. Unsupported addressing and stateful inversion refuse explicitly. This is a bounded instruction model, not general binary equivalence or a native pointer ABI.

Validation includes 37 frozen states across 74 native calls, independent review, desktop/mobile interaction, source-exact wheel and sdist checks, and a fresh installed-package lesson. See the state-transition guide and validation notes for scope.

Install the downloaded wheel in a Python 3.11+ virtual environment, then run rewynth serve. macOS and Linux support data-only ARM64 analysis. The wheel requires Capstone 5.0.6 and Z3 4.15.3.0; it is not a dependency bundle. SHA256SUMS covers both distribution archives.