Module reverse 

Reversibility classification of the ISA — the static substrate for running the whole language backward (forward ; reverse ≡ identity), the software prerequisite for the adiabatic / sub-Landauer chip. Locked by tests/reverse_op_lock.rs. Reversibility classification of the bytecode ISA — the static substrate for running the whole language BACKWARD (forward ; reverse ≡ identity).

Because the register-VM opcode set is the chip ISA, a reversibility strategy for every op is the software prerequisite for adiabatic / sub-Landauer hardware that recycles charge instead of erasing it. Every instruction lands in exactly one of four working strategies (or the empty NonReversible census), and reversibility is EXHAUSTIVE on Op with NO wildcard arm — a new instruction cannot compile until it is classified, so reversibility can never be silently broken. The tests/reverse_op_lock.rs catalog lock enforces the census, the monotone zero-garbage floor, and inverse well-formedness.

This module is the STATIC half. The behavioural half — a reverse executor proving forward ; reverse restores the exact initial state, with the history tape at zero bytes for the abelian core — lands in R1+ (vm::journal, Vm::run_reverse).

Enums

EffectKind

The family of observable effect a RevClass::Effectful op performs — determines how far reversal can go before it hits a named barrier.

InverseSpec

How a RevClass::Bijection op inverts — the zero-garbage inverse recipe.

JournalKind

What a RevClass::Journaled op must record on the history tape to be reversible — the minimal destroyed information (Bennett/Landauer embedding), not a full state snapshot.

RevClass

How an op participates in reversible execution. Four working strategies plus a census bucket that MUST stay empty. Copy so a lock can classify every variant without allocation.

ReverseMode

The reversibility fidelity ⇄ space ⇄ time point a recording run is asked to hit — the pebbling knob (vm/pebble.rs). The tape is only as large as the mode demands.

Functions

external_effect_barrier

Whether the reverse executor supports op yet — the GROWING reversible subset. R1 covers the abelian core (RevSwap, zero garbage), straight-line scalar compute (overwritten_reg), the global write/read, output, and program stop. A program containing any other op declines recording with a clear error rather than silently mis-reversing; the subset expands (control flow, collections, effects) in R2/R3. If op is a truly-EXTERNAL effect that cannot be un-done — the honest Landauer wall, an already-sent network message can’t be un-sent — name the irreversibility barrier. None for reversible ops and for internally-modeled effects (buffered output, in-process channels, the clock) that DO reverse. This turns an irreversibility into a NAMED, enumerable boundary instead of a generic “unsupported”, so the reverse executor never silently pretends the world can be rewound.

is_reversible_supported

mutated_collection_reg

Whether forward execution RECORDS a history-tape delta for op — i.e. it destroys data a reverse pass must restore. Exactly the ops that write a global/output line or a scalar register. The DUAL of the reverse pass’s pop condition: record_op pushes iff this is true, and run_reverse pops iff this is true, so the tape stays aligned. A RevClass::Bijection op is never here — it self-inverts with no tape entry (the zero-garbage core). The single collection register an op mutates IN PLACE (push / index-set / add / remove) — for the ops reversed by restoring the pristine pre-mutation snapshot (super::journal::JournalEntry::CollectionMutate). None for non-mutating ops and for ListPop (which ALSO writes a dst — it carries its own combined entry). Journaling this register’s value forces the op’s copy-on-write, so the original stays pristine for the reverse.

overwritten_reg

The single register an op OVERWRITES with a fresh value — its data destination — for the ops whose only state effect is that write and whose operands survive. Reverse execution restores this register’s prior value from the tape. None for ops that write a global / heap object / output line instead (handled separately) or write nothing.

records

reverse_reads

The registers a REVERSE step reads from the live machine (not from the tape) when undoing op — so their values must be intact at reverse time. Journaled overwrites restore their destination straight from the tape and read NOTHING live, so they contribute none; only the Bijection ops (which recompute in place) and the collection/CRDT reverses (which read the live handle) do. Eliding a journal entry for a register in this set could corrupt a later reverse-read, so the pebbler treats membership here as “must keep”. Keep in lockstep with the reverse executor.

reversibility

★ THE STATIC REVERSIBILITY CATALOG ★ — the single source of truth for how every VM bytecode op is run backward. EXHAUSTIVE on Op (no _ arm): adding an instruction fails to compile until it is classified, so no op can silently escape a reversibility strategy. Keep this in lockstep with the reverse executor (vm::journal / Vm::run_reverse, R1+) — the behavioural roundtrip lock proves they agree.

reversible_builtin

Whether a builtin is PURE — a deterministic function of its arguments, reversible by restoring the destination and the cleared argument registers. Excludes the wire-subsystem builtins, which touch external sinks or run shipped code (effects the store snapshot cannot reverse).