Time Travel over Typed Effects: Backwards Replay, Forward Replay and Execution Bisect

Pitch

A language that requires every effect to declare an inverse, or be classed as an emission, already holds the data for a reverse debugger. The checker verifies an inverse's presence and shape, not its correctness, and the honest version of that debugger makes one claim: the inverses ran newest first, and nothing about state being restored.

Abstract

Reverse debuggers usually capture every memory write or require an invertible language. We observe that a runtime with inverse-or-emit effects already keeps, per live component, an ordered accumulator of registered inverses and a compiler-derived classification of which steps cannot be inverted. We build time travel on that accumulator in revl's Python reference tier: a captured timeline of effects, provisions, emissions, compensations and boundaries; step-back, which runs the registered inverses newest first down to a chosen step while leaving the component alive; forward replay, which re-invokes the provided-service calls that produced the tail; and bisect, a binary search over the timeline for the first step at which a predicate flips, in at most ceil(log2 N) + 2 evaluations (the test checks this on one 32-insert timeline). Each inverse is wrapped in a single-flight cell shared with the runtime's own teardown, so an early step-back and a later unload run each inverse once and unload still reports no residue. The system states one guarantee, a guarantee field carried in its step-back, timeline and bisect reports, and refuses by default to unwind across an uncompensated emission. We state what it cannot promise: an inverse is not an undo of the world, compensation is not inversion, forward replay re-runs rather than restores, and bisect trusts the registered inverses and labels its answer unverified. The engine has 49 tests, 13 of them against the real runtime. We discuss the design, the refusals, and the gap between a replay viewport and a state-restoration claim.

Problem and claim

Stepping back normally costs a full trace or an invertible language. Debuggers that offer reverse execution rarely say what they do not restore, and tools that undo effects on a live system risk reporting success while a committed external write still stands.

The claim has two parts. First, a runtime whose effects register inverses in a LIFO accumulator (G4, G7 in the docs) gets partial unwinding, inspection of the unwound prefix, and a log-time search for free, without changing emitted code. Second, the useful contribution is the discipline: a two-sentence guarantee, a refusal that moves irreversibility from a footnote to a decision, and a bisect report that carries its own trust bound.

This is not a claim that stepping back restores program state, and not a claim about the other five tiers.

Contributions

1. Step-back over the inverse accumulator newest first, leaving the component live, with a single-flight cell per inverse shared with teardown so unload after step-back remains residue-free (docs/replay.md:61-64,82-91; test_real_cordis_step_back_then_unload_still_leaves_no_residue, tests/test_replay.py:929).
2. A two-sentence guarantee, replay.GUARANTEE, returned in the guarantee field of reports, with a test that no step-back report key contains "restor" (backends/python/replay.py:256-260; tests/test_replay.py:697).
3. A refusal rule: step-back refuses by default when the range contains an uncompensated emission, refuses totally (nothing runs), and force is the explicit override; compensation is reported as its own step kind and appends a new emission step (docs/replay.md:130-177; tests/test_replay.py:445,474,946,963).
4. Forward replay that re-invokes provided-service calls and reports activation-body steps as notReplayable instead of faking them (docs/replay.md:179-202; tests/test_replay.py:522,540).
5. Execution bisect: a git-bisect-style search for the first step at which a predicate over the inspect view flips, with a report that carries a verified or unverified status for the effects on the path (backends/python/replay.py:853-1000; tests/test_replay.py:585-683; docs/replay.md:297-349).
6. Trace capture that the docs say leaves emitted output byte-identical (the golden files are cited, not opened here): a wrapper around each component's apply passes a delegating context (docs/replay.md:215-232).

Related work

Evidence on main

Tree: revl main at commit 45bec431f.

Numbers that exist

• tests/test_replay.py: 49 test functions (rg -c "^def test"), 13 @needs_cordis decorators, each on a real-runtime test (tests/test_replay.py:897-1113). The 14th textual match is in the module docstring at line 13. This matches the doc's split of 36 stub tests and 13 real-runtime tests (docs/replay.md:355-368).
• Bisect bound: at most ceil(log2 N) + 2 evaluations, tested on a timeline built by _notes_timeline(32) (tests/test_replay.py:585-612). No larger N and no timing.
• tests/test_time_coeffect.py: 54 test functions. Not run.
• No measurements of trace-capture overhead, timeline size, or bisect speedup on real compositions.

Paper outline

1. Introduction: reverse execution without a trace, and the cost of overclaiming restoration.
2. Background: inverse-or-emit effects, the LIFO accumulator, compensation (A5).
3. Model: step kinds, timeline, the four operations.
4. The guarantee and its refusals: the two sentences, force, compensation versus inversion.
5. Forward replay and what it cannot re-enter.
6. Bisect: predicate scope, complexity, monotonicity, unverified status.
7. Trace capture without changing emitted code; classification assumptions.
8. Evaluation: overhead, scale, case study or user study (to be run).
9. Related work.
10. Limits and the WAL-based, cross-process half (see P19).

Threats to validity and limits

• The docs state the central bound: "stepping back to step k does not put the program in the state it was in at step k" (docs/replay.md:107-111). Under correct inverses the two coincide; the runtime never checks.
• Not caught: a wrong or partial undo, state reachable through a handed-out reference, anything outside the process, and values derived from a clock (docs/replay.md:113-119).
• Forward replay cannot re-enter activation-body steps; the remedy is reload (docs/replay.md:186-202).
• Trace capture is opt-in at load and not retroactive (docs/replay.md:204-213).
• Host extern emission fn calls do not appear as emission steps; their compensation shows up as an ordinary inverse (docs/replay.md:253-258).
• Compensation is identified by source adjacency of emitted lines, an assumption about emitter shape (docs/replay.md:240-247).
• Bisect assumes a monotone predicate and "still returns a flip boundary, but not provably the first" otherwise (docs/replay.md:320-322). It evaluates the predicate over inspect(k) reconstructed from the timeline (backends/python/replay.py:869-880), not over a re-executed program.
• Python tier only; the doc says nothing has been ported to the other five tiers (docs/replay.md:410-412).
• Doc statements this paper does not copy: docs/replay.md:12 is headed "Why this exists here and nowhere else" (an unchecked comparative claim), and docs/replay.md:299 says step_back k "restores any prefix", which contradicts docs/replay.md:107-111.
• The test named test_real_cordis_step_back_restores_state_and_leaves_it_live (tests/test_replay.py:912) checks one component after one step-back. Its name says "restores"; its assertions are cited, not its name, and it is not evidence of restoration in general.
• One cordis-py gap affects async bodies' failure state; the doc attributes it to the runtime, not to replay (docs/replay.md:391-401).
• The revl replay command (src/revl/cli/parser.py:1924-1967) reports replay-mode readiness over a durable write-ahead log and "runs nothing"; it is a different mechanism and is not claimed here.
• backends/python/replay.py also contains write-ahead log and recovery code beyond what docs/replay.md covers; this draft does not claim any of that.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 30 checked, 13 corrected.

Cite this draft

@misc{revlp18,
  author       = {Thomas Moussajee},
  title        = {Time Travel over Typed Effects: Backwards Replay, Forward Replay and Execution Bisect},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P18.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.