Rewynth0.2.0: recover and rewind64-bit state

Rewynth now recovers editable64-bit ARM64 programs and derives supported reusable inverses, with exact values throughout the browser and JSON boundary. The default32-bit API and original fixture remain unchanged.

Load 64-bit state rewind example, select _splitmix64_step, recover source and derive an inverse. Full output 0x161922c645ce50e8 rewinds to prior state 0x123456789abcdef0. The compiled native fixture and browser-local backward program agree. This is a marked pure adapter of public-domain SplitMix64, not its memory-based stateful routine. Initial-seed recovery additionally needs a known call position; no truncated-output/Raylib/xoshiro/cryptographic recovery claim.

Python3.11+, macOS orLinux. Install the downloadedwheel in a virtualenvironment, then run rewynth serve. Walkthrough. CLI:

rewynth derive_inverse --example-wide --function _splitmix64_step --arguments 1 --word-bits 64

• X-register semantics with W-write zero extension, instruction-width flags/shift masks and64-bit MOVK/bitfield operations.
• Boundededitable source, defineduint64C, solvercounterexamples and exact BigInt local backward execution.
• 64-bit HTTP input/domain values must be strings; lossy JSON numbers are rejected beforeworkersstart. Large results use exact hex strings.
• Workspaceversion2 retainswidth/text/bytes/edit; version1 remains32-bit and oldproofs neverbecome fresh verification.

PR1 merged at 864246f2ee2f3cf4ae7189ad5421a7ec29771d9c; merge tree exactlymatches reviewedfeature. HostedCI passed Linux3.11/3.14 and ARM64macOS3.12:59tests each plus installed32/64CLI checks. Linux explicitly skips five native fixture tests. Freshreview independently checked6,405CPU/model cases and33baseline32UNSAT comparisons. Rootproductexports checked1,590native/model/recompiledC cases and530inverse assertions; validation separates otherchecks and theirlimits. Counts overlap.

Exact chainbinding and localtwo-sidedprimitive proofs areUNSAT in the implemented model. Whole nonlinearcomposition checks remainUNKNOWN(timeout). The compiled wide_permute shape honestly remains unsupported for reusable inversion. No formallyverifiedCPU/wholeprogram/arbitrarybinary claim; memory,calls,loops,float/SIMD remainunsupported. Importedbytes neverrun natively. Native comparisons run only identifiedlicensed/ownedfixtures andgeneratedC.

OriginalMITcode, fullSplitMix64public-domain notice, pinnedwideprovenance, and all priorstb/xxHash notices retained. Built/testedwithCodex assistance. No PyPIpublicationclaimed.

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.