Repository navigation
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.