Module pebble 

Pebbling — the reverse-liveness pass that decides which journal entries a recording run actually NEEDS, driving the Bennett history tape toward the Landauer floor.

The idea. The tape is not fundamental. Most journaled bits are recomputable, not destroyed: a scratch temporary t = f(a,b) with its inputs still live is a pure function of live state, and reverse execution only reads live registers for Bijection ops (RevAdd’s place/delta, …) and collection reverses — every Journaled overwrite restores its destination straight from the tape without reading its operands. So a scratch write that only feeds Journaled results has an old value no reverse step ever reads; recording it was a naive-forward artifact. Eliding it is sound and shrinks the tape.

P1 rule (sound set-membership). A Journaled single-destination overwrite is Elided iff its register is (a) not program-observable — not named in its frame (CompiledProgram::named_regs / CompiledFunction::named_regs) — AND (b) never a reverse-read operand (crate::vm::reverse::reverse_reads). Both the recorder (crate::vm::Vm’s record_op) and the reverse executor consult the plan, so an elided entry is neither pushed nor popped.

Empty named_regs (hand-built bytecode / no name info) ⇒ everything is treated observable ⇒ nothing is elided ⇒ the reverse executor’s full-fidelity behaviour is preserved byte-for-byte.

Structs

PebbleReport

A static summary of a mode’s plan: how many Journaled entries survive vs. are elided.

Enums

JournalDecision

What the recorder should do with a Journaled write’s tape entry.

Functions

checkpoint_defs

The recomputable-chain intermediates to KEEP as checkpoints (corner 2) — the budget nodes that most shorten the reverse re-walk. An INTERMEDIATE is a recomputable node whose register is an input to another recomputable def in the same frame (so it sits inside a chain, not at its top). We checkpoint the intermediates CLOSEST to the chain tops (highest def_pc) first: keeping a node near the top caps every above-it read at a re-walk of length 1, the largest marginal saving per pebble (the Bennett “cache near the read” heuristic). budget = 0 ⇒ none (recompute everything).

frame_of

The function that owns pc — the one with the greatest entry_pc ≤ pc (Main is compiled first, then each function body appended contiguously; see vm/compiler.rs Pass 2a/2b). None = Main.

plan

Per-pc journaling decisions for a recording run in mode. FullState keeps everything (today’s behaviour, made explicit); the pebbling modes elide scratch whose destroyed value no reverse step reads. Indexed by absolute pc in CompiledProgram::code.

plan_budgeted

plan with an explicit pebble CHECKPOINT budget (corner 2). Under Adiabatic, budget recomputable chain intermediates are KEPT on the tape (journaled once — landauer = 0, since a recomputable scratch is first-def so its displaced value is Nothing) instead of upgraded to Recompute. A reverse step that reads a node above a checkpoint then re-walks only down to the nearest checkpoint, not to the chain root — the Bennett space-for-time trade. budget = 0 is the recompute-everything corner (O(1) tape, chain·reads time); higher budgets bound the re-walk length.

recomputable

Reverse-live scratch registers that can be RECOMPUTED on reverse instead of journaled — Bennett uncompute — keyed by the FRAME they live in (register numbers are frame-relative). Each is a SCRATCH register that some reverse step in its frame reads live (so Observable/FullState must journal it), with a SINGLE pure-arithmetic def whose inputs are STABLE within the frame, and that (via the frame-overlap bases) aliases NO Main-observable slot. Re-running the def during reverse with self.base set to the frame reconstructs it exactly. Returns (frame, register, def_pc, def_op). Dynamic dispatch (CallValue, unknown callee) yields nothing; recursion is handled via the bounded frame bases (corner 4) — each activation recomputes at its own live base.

report

Summarise the plan for mode — the count of Journaled writes kept vs. elided (the static space budget; the dynamic erased-byte floor comes from a recording run’s tape).