Recover and compare bounded ARM64 state transitions

.github/workflows/ci.yml

@@ -52,3 +52,5 @@ jobs:
           python -c "import json; f=json.load(open('branches.json')); e=json.load(open('branch-trace.json')); assert f['reconstruction']['status']=='verified_model'; assert e['witness']['output_u32']==4095; assert e['witness']['trace'][-1]['kind']=='return'; print('Installed conditional recovery and trace passed')"
       - name: Runnable conditional lesson against the installed package
         run: python examples/conditional_lab.py --output branch-lab
+      - name: Installed bounded state-transition lesson
+        run: python examples/state_lab.py --output state-lab

README.md

@@ -1,12 +1,16 @@
 # Rewynth
 
-**Turn compiled integer behavior into source you can run forward or backward.**
+**Recover compiled behavior. Catch edits that break the next call.**
+
+[![Python 3.11+](https://img.shields.io/badge/Python-3.11%2B-3776AB?logo=python&logoColor=white)](pyproject.toml) [![Local ARM64 analysis](https://img.shields.io/badge/ARM64-local_analysis-7259D9)](docs/state-transitions.md) [![Verify](https://github.com/nazeeh111/Rewynth/actions/workflows/ci.yml/badge.svg)](https://github.com/nazeeh111/Rewynth/actions/workflows/ci.yml) [![MIT](https://img.shields.io/badge/License-MIT-45474B)](LICENSE)
 
 Rewynth is a local laboratory for recovering selected ARM64 functions, editing their semantics, finding counterexamples and deriving reusable inverse programs. It reads the original machine instructions as data. No model API, account or cloud service is required.
 
-The shipped demonstrations reconstruct image-processing kernels, branching integer transforms and an xxHash mixing function from actual compiled bytes. Branching examples retain guards, multiple returns and shared exits in editable source. A backward program derived from the mixer computes an original 32-bit input from its output without making a new solver query. This reverses the **avalanche transform**, not the complete variable-length xxHash algorithm.
+Declare a small state buffer and recover its return plus every post-state word. An edit can return the same value but skip an update needed by the next call. Joint comparison exposes that counterexample. The complete [state-transition lesson](docs/state-transitions.md) uses the unchanged PCG32 routine compiled locally from independently authored source.
+
+The other shipped demonstrations reconstruct image-processing kernels, branching integer transforms and an xxHash mixing function from actual compiled bytes. Branching examples retain guards, multiple returns and shared exits in editable source. A backward program derived from the mixer computes an original 32-bit input from its output without making a new solver query. This reverses the **avalanche transform**, not the complete variable-length xxHash algorithm.
 
-![Actual installed Rewynth workbench](docs/workbench.png)
+![Actual Rewynth comparison: same return, different next state](docs/state-workbench.png)
 
 ## Run it
 
@@ -20,11 +24,21 @@ python3 -m venv .venv
 .venv/bin/rewynth serve
 ```
 
-Open `http://127.0.0.1:6343/` and choose **Load real compiled example**. There is also a wheel on the [release page](https://github.com/nazeeh111/Rewynth/releases); install that downloaded wheel inside a virtual environment instead of cloning.
+Open `http://127.0.0.1:6343/` and choose **Load PCG32 bounded state example**. There is also a wheel on the [release page](https://github.com/nazeeh111/Rewynth/releases); install that downloaded wheel inside a virtual environment instead of cloning.
 
 To inspect your own artifact, use a thin, little-endian ARM64 Mach-O or ELF with named code symbols. Select the function and explicitly declare its 32- or 64-bit word size and one to four argument registers. Narrow the input domain when the intended use requires it. The workbench binds results to both artifact and function-byte digests.
 
-## A complete experiment
+## Compare a stateful edit
+
+Recover the PCG32 example. In the editable JSON, replace the first `memory` expression with `"x0"` and keep the return unchanged. Choose **Find a counterexample**: both returns agree, but `memory[0]` differs. Reset the edit, trace your inputs, export the pure transition C, or save the workspace.
+
+```sh
+.venv/bin/python examples/state_lab.py --output state-lab
+```
+
+This runnable lesson produces recovered source, the lost-store control and evidence. It reads the artifact as data. The original library has no demonstrated bug; the lost update is our edit. [Memory declarations, input order, safe edits, export and limits](docs/state-transitions.md).
+
+## A register-only experiment
 
 1. Select `_kernel_avalanche`, one argument, all input patterns. Recover its editable source and inspect the actual instructions.
 2. Choose **Derive inverse program**. Inspect the extracted reversible chain and its proof records.
@@ -46,7 +60,7 @@ rewynth derive_inverse --example-wide --function _splitmix64_step --arguments 1
 rewynth evaluate --example-wide --function _splitmix64_step --arguments 1 --word-bits 64 --inputs 0x123456789abcdef0
 ```
 
-[Word-width, exact JSON and workspace contracts](docs/64bit.md) describe the interfaces. Version 1 workspaces reopen as 32-bit; new version 2 workspaces retain the selected width and exact query text. The original 32-bit example is unchanged.
+[Word-width, exact JSON and workspace contracts](docs/64bit.md) describe the interfaces. Version 1 workspaces reopen as 32-bit; new version 3 workspaces retain the selected width, memory declaration and exact query text; version 2 remains readable. The original 32-bit example is unchanged.
 
 ## Recover a function with branches
 
@@ -89,15 +103,15 @@ saves actual results; this figure explains their scope.
 
 **Recovery:** Capstone decodes the selected instructions. Rewynth translates its supported 32- and 64-bit register operations into Z3 expressions over bit-vectors (fixed-width machine words), preserving arithmetic flags and conditions. Compact semantic families solve for missing parameters and refine failed hypotheses using solver-produced counterexamples. A general bit-linear learner probes basis vectors, groups the inferred mask/shift/XOR contributions, then checks the complete candidate. Nonlinear functions use a bounded general semantics-to-source fallback. Recovered source uses prior-only bindings to keep shared expressions readable.
 
-**Falsification:** the solver asks whether an input inside the explicit domain makes the original model and edited source produce different output bits. A satisfiable query returns the input, both outputs and a register trace. SAT means a contradicting input exists; UNSAT means no such input exists in the declared model and domain. UNKNOWN means the solver did not decide within its limits. A timeout stays unknown. An empty test set or a handful of successful examples never becomes an equivalence claim.
+**Falsification:** the solver asks whether an input inside the explicit domain makes the original model and edited source produce different return bits or declared post-state words. A satisfiable query returns the input, both outputs, full post-state in memory mode and an instruction trace. SAT means a contradicting input exists; UNSAT means no such input exists in the declared model and domain. UNKNOWN means the solver did not decide within its limits. A timeout stays unknown. An empty test set or a handful of successful examples never becomes an equivalence claim.
 
 **Inverse programs:** the engine extracts a reversible single-input chain directly from the lifted expression. It derives modular inverses of odd multipliers and reverses constant addition/subtraction/XOR, constant rotations, full-width bit reversal and self-XOR shifts. Exact chain binding and both directions of every primitive must be checked before compositional inversion is accepted. Whole-expression checks are recorded separately, including timeouts. Lossy operations, unsupported chains and restricted input domains do not receive an all-input inverse claim.
 
 The reusable inverse is computed from the recovered program. The separate **Find an input** operation can also solve a particular output constraint for supported non-bijective or multiple-input functions.
 
 ## Scope is explicit
 
-This is a **bounded instruction-model result**, not a formally verified CPU lifter, whole-program decompiler or calling-convention inference system. You select the 32- or 64-bit word size, argument registers and returned `w0` or `x0` bits. In 64-bit mode, writes to a `w` register correctly zero its upper `x` bits; flags and shift masks follow each instruction's operand width. Direct conditional branches and shared return paths are supported when their control-flow graph has no directed cycle. A branch may target a lower address without forming a loop. Memory, calls, loops, indirect control flow, floating point, SIMD, ARM64e and unsupported instructions are rejected. Code with unresolved relocations is rejected before analysis. Stripped-symbol and universal-binary boundary recovery are outside this release.
+This is a **bounded instruction-model result**, not a formally verified CPU lifter, whole-program decompiler or calling-convention inference system. You select the 32- or 64-bit word size, argument registers and returned `w0` or `x0` bits. In 64-bit mode, writes to a `w` register correctly zero its upper `x` bits; flags and shift masks follow each instruction's operand width. Direct conditional branches and shared return paths are supported when their control-flow graph has no directed cycle. A branch may target a lower address without forming a loop. Memory is rejected by default. Explicit 64-bit memory mode supports one pointer and 1–3 little-endian words, with at most four logical scalar/state inputs and concrete in-bounds accesses. Its comparison covers the entire declared post-state and X0 at one documented synthetic base. Arbitrary/symbolic pointers, stack/global memory, indexed accesses, writeback, atomics and stateful inverse operations remain unsupported. Calls, loops, indirect control flow, floating point, SIMD, ARM64e and unsupported instructions are rejected. Code with unresolved relocations is rejected before analysis. Stripped-symbol and universal-binary boundary recovery are outside this release.
 
 The source language wraps arithmetic modulo 2³² or 2⁶⁴ and masks shift counts to 0–31 or 0–63. Browser computation uses exact BigInt values; 64-bit HTTP inputs and domain bounds must be strings so JSON numbers cannot silently lose bits. Signed and unsigned comparisons are distinct. Imports are never loaded for native execution. CPU comparisons execute only identified public or owned test fixtures and generated C.
 

THIRD_PARTY_NOTICES.md

@@ -72,3 +72,14 @@ and related and neighboring rights to this software to the public domain
 worldwide. This software is distributed without any warranty.
 
 See <http://creativecommons.org/publicdomain/zero/1.0/>. */
+
+## PCG32 original state-transition example
+
+Copyright 2014 Melissa O'Neill. Original pcg_basic.c and pcg_basic.h from
+imneme/pcg-c-basic revision bc39cd76ac3d541e618606bcc6e1e5ba5e5e6aa3
+are preserved as pcg-basic-upstream.c and pcg_basic.h. The shipped pcg-basic.o
+is compiled locally from those unchanged sources. Apache License 2.0 applies
+to these files and the derived object; the complete license is retained in
+src/native_recovery/resources/examples/pcg-APACHE-2.0.txt. The upstream source
+notice is preserved. This example is not an upstream defect or endorsement.
+Rewynth's original implementation remains under its existing MIT license.

docs/64bit.md

@@ -12,7 +12,7 @@ Output values outside JavaScript's safe integer range are hexadecimal strings. W
 {"operation":"evaluate","artifact":"<artifact SHA-256>","symbol":"_splitmix64_step","arity":1,"word_bits":64,"inputs":["0x123456789abcdef0"],"domain":[null]}
 ```
 
-Workspace version 2 stores word size, exact textual queries, original bytes and edits. Version 1 is explicitly 32-bit. Reopening never treats old proof evidence as a fresh comparison. Changing word size invalidates the comparison, inverse program and trace.
+Workspace versions 2 and 3 store word size, exact textual queries, original bytes and edits. Version 1 is explicitly 32-bit. Reopening never treats old proof evidence as a fresh comparison. Changing word size invalidates the comparison, inverse program and trace.
 
 ## The real fixture boundary
 
@@ -23,3 +23,5 @@ Prior state zero produces full output `0xe220a8397b1dcdaf`. A derived inverse re
 Proofs apply to the implemented selected-word instruction model. Exact chain binding and both directions of each supported primitive are required for compositional acceptance. Whole nonlinear composition checks can remain UNKNOWN. Native comparisons exercise only identified licensed/owned fixtures and generated C, never an uploaded artifact.
 
 Source and binary hashes, immutable upstream identity and full notices are in `resources/examples/wide-provenance.json` and packaged third-party notices. Do not reuse a fixture digest after recompilation changes its bytes.
+
+Version 3 also stores an optional bounded-memory declaration. [State-transition contracts](state-transitions.md) define logical input order, full post-state comparison and pure C exports. Versions 1 and 2 remain readable as register-only workspaces.

docs/architecture.md

@@ -27,3 +27,7 @@ Thin ARM64 artifact
 The solver and lifter are trusted parts of the model, not themselves formally verified by these checks. Independent native tests compare identified fixtures and generated C with model results. Those observations support specific tested instruction forms and do not establish correctness of arbitrary imported programs.
 
 `control_flow.py` decodes reachable instructions, validates direct targets and topologically orders the graph. The lifter merges register values and flags under their execution guards instead of enumerating paths. Registers or flags missing on an incoming path remain unavailable. Multiple returns combine into one output expression; concrete traces filter guards and retain the actual branch/write/return order. A backward address edge is allowed when the directed graph remains acyclic. The existing 128-instruction and editable-expression bounds remain in force, with at most 256 graph edges.
+
+## Declared state transitions
+
+The same acyclic lifter can carry one finite little-endian memory region alongside registers and flags. Each incoming path merges all declared words, and each return captures the full post-state. `transitions.py` translates and jointly compares architectural X0 plus every post-state word. Scalar-only proof and inverse APIs refuse these models. Public request normalization and workspace v3 retain the machine-to-logical input mapping. [The full contract](state-transitions.md) records bounds and unsupported addressing.

docs/state-transitions.md

@@ -0,0 +1,112 @@
+# Preserve the next call, too
+
+A function can return the right value and leave the wrong state for its next
+call. Rewynth can recover, edit and compare a small declared ARM64 memory
+transition. It checks architectural X0 and every declared post-state word
+together. Imported machine code is read as data and never executed.
+
+## Run the complete example
+
+After installing Rewynth, run:
+
+```sh
+python examples/state_lab.py --output state-lab
+```
+
+The example uses the unchanged `pcg32_random_r` function from Melissa O'Neill's
+[PCG C basic library](https://github.com/imneme/pcg-c-basic/tree/bc39cd76ac3d541e618606bcc6e1e5ba5e5e6aa3).
+It writes recovered `transition.json`, portable `transition.c`, an original
+`lost-store.json` edit, and `evidence.json`. Use a fresh output directory to
+preserve existing results. The edit retains the immediate return but drops
+the state update. A joint comparison must report `sat` with `memory[0]`
+different; comparing only the return would miss this.
+
+This is a controlled, source-available example compiled locally, not an
+independently published binary or an upstream bug. PCG already has advance
+and rewind facilities. This workflow demonstrates state-aware recovery and
+editing, not random-generator quality or unique seed recovery.
+
+## Workbench
+
+Run `rewynth serve`, open its loopback address and select **Load PCG32 bounded state example**. Recover the transition. The input labels map `x0` to the initial
+state word and `x1` to the increment word. To try the lost update, replace
+the first entry in `memory` with `"x0"`, keeping the return unchanged. Compare
+the edit. The counterexample shows the same returned value and different
+post-state. Reset the expression to recover the original transition.
+
+Save a workspace to retain the artifact bytes, pointer declaration, exact
+inputs and editable transition. Workspaces use version 3; older register-only
+versions 1 and 2 remain readable. Reopened results require a fresh comparison.
+Export C to use the recovered pure transition, or export evidence to retain
+the model assumptions, artifact identity and witness.
+
+## CLI and logical inputs
+
+```sh
+rewynth recover --example-memory --function _pcg32_random_r \
+  --arguments 1 --word-bits 64 --memory-argument 0 --memory-words 2
+
+rewynth evaluate --example-memory --function _pcg32_random_r \
+  --arguments 1 --word-bits 64 --memory-argument 0 --memory-words 2 \
+  --inputs 0x853c49e6748fea9b 0xda3e39cb94b95bdb
+
+rewynth verify --example-memory --function _pcg32_random_r \
+  --arguments 1 --word-bits 64 --memory-argument 0 --memory-words 2 \
+  --expression state-lab/lost-store.json
+```
+
+`--arguments` counts machine argument registers. The memory argument is a
+pointer register indexed from zero. Its address is supplied by the model,
+not by the input list. Logical inputs are the remaining scalar registers
+in register order, followed by the initial 64-bit memory words in address
+order. Both `--inputs` and `--domain` use this logical order. At most four
+logical inputs are supported. In the PCG example, one pointer register
+becomes two logical state inputs. HTTP requests carry 64-bit values as
+decimal or hexadecimal strings to preserve every bit.
+
+## Edit and export contract
+
+The editable document has exactly two fields:
+
+```json
+{
+  "return": "x0 + 1",
+  "memory": ["x0 + 1", "x1"]
+}
+```
+
+This small illustrative transition is not PCG. Each string uses the existing
+[safe expression language](source-language.md). Outputs are simultaneous:
+all expressions read the original inputs. Every memory word needs an
+expression, even if unchanged. The whole document is at most 64 KiB; each
+expanded expression retains the 256-node and depth-24 bounds. Duplicate or
+unknown fields, missing words, arbitrary code and boolean outputs refuse.
+
+Generated C accepts the logical `uint64_t` inputs and returns a
+`rewynth_state` structure with `result` and `memory[]`. It does not dereference
+an input pointer or replace the native function ABI. The exported return is
+architectural X0, including zero extension when the last result write is W0.
+It expresses the implemented model, not a certificate for every CPU.
+
+## Explicit memory boundary
+
+Memory is opt-in and available only in 64-bit register mode. Declare one
+pointer and 1–3 consecutive little-endian 64-bit words. The pointer is bound
+to the synthetic address `0x100000000`. Equality covers that declared model,
+not arbitrary base addresses, alias layouts, stack or global memory.
+Only concrete, in-bounds fixed-displacement loads/stores are supported.
+Symbolic/indexed addresses, writeback, undeclared accesses, calls, loops and
+unsupported instruction forms refuse. The entire declared post-state is
+compared, not only bytes that happened to be written. Inverse queries and
+inverse programs explicitly refuse memory mode.
+
+`unsat` means no joint difference was found possible under the declared
+domain and implemented semantics. `sat` supplies a counterexample. `unknown`
+or a refusal supplies no equivalence conclusion. The existing 20-second
+owned analysis process and solver budgets remain in force.
+
+Symbolic memory and binary comparison are established techniques. For larger
+programs or richer side effects, evaluate mature tools such as
+[angr](https://docs.angr.io/en/latest/core-concepts/states.html) and
+[cozy](https://github.com/draperlaboratory/cozy). Rewynth's contribution here
+is the bounded artifact-to-editable-transition workflow.