Rewynth 0.1.0: compiled behavior, runnable backward

Rewynth turns supported compiled ARM64 integer functions into editable source, counterexamples and reusable inverse programs. It runs locally with Capstone and Z3, without a paid API or account.

The shipped xxHash32 avalanche demonstration derives a backward program: desired output 0xdeadbeef produces input 0x471f246e. The original identified ARM64 fixture returns 0xdeadbeef for that input on actual hardware. This reverses the 32-bit avalanche transform, not the complete xxHash algorithm.

• Read named functions from bounded thin ARM64 Mach-O or ELF artifacts as data.
• Recover supported 32-bit register semantics, edit a bounded source language, obtain a concrete disagreement and register trace, and export standalone defined C.
• Derive reusable inverse programs for supported reversible chains. Save and reopen original bytes, argument/domain declarations and edits; recovered proof status is recomputed.
• Local workbench and CLI; cancelable bounded analysis; unsupported instructions and unresolved relocations fail explicitly.

Installation

Python 3.11 or newer, macOS or Linux. Download the wheel below and install it in a virtual environment:

python3 -m venv .venv
.venv/bin/python -m pip install ./rewynth-0.1.0-py3-none-any.whl
.venv/bin/rewynth serve

Open http://127.0.0.1:6343/, load the compiled example and select _kernel_avalanche with one argument. Choose Derive inverse program, then run backward from a desired output. The source distribution and source installation instructions are also available. No PyPI publication is claimed.

Verification and scope

Hosted CI passed on Linux Python 3.11/3.14 and ARM64 macOS Python 3.12 at commit 5298ba1949e0b85ffa8c41375248ca82c4b9c0bf. Each job ran the 39-test suite and installed CLI recovery/inverse checks. Three native fixture tests are explicitly skipped on Linux.

Three derived inverse programs passed 12,060 native roundtrip assertions. The six forward fixtures and instruction checks have separate validation records. Counts overlap and do not represent universal coverage.

Inverse acceptance requires exact chain binding and both directions of each primitive to be UNSAT under the implemented model. Whole nonlinear composition checks timed out and are reported as UNKNOWN, not exhaustive solver proofs. The attached evidence preserves these outcomes.

This is a bounded instruction-model laboratory, not a formally verified ARM CPU, whole-program decompiler or general binary inverter. One to four explicitly declared 32-bit arguments, returned w0 bits, named code symbols and supported straight-line register operations only. Memory, calls, loops, 64-bit operands, floating point and SIMD are rejected. Imported artifacts are never executed. Only identified public or owned test fixtures and generated C were executed during validation.

Original project code is MIT. Example excerpts retain stb MIT and xxHash BSD-2-Clause notices with pinned provenance. The generated inverse C includes attribution and its artifact digest. Built and tested with Codex assistance.