R13: A run's inputs are data: equal recorded inputs give equal replay observationsreq:R13
- Open, after other work (Config, route B: designed and not implemented (decisions rows 51 and 83)): load inputs, the environment snapshot and the seed: designed (the 2026-09-10 Config route B), not implemented (decisions rows 51, 83)
- Open, after other work (Config, route B: it restates the typed load when Config lands): supplied values fit the admitted load requirements: restates M5 (loadsTyped, the retired ledger's typedState_load) when Config lands
- Open, not triaged: the service half of the signature as a recorded input: Built carries the row table only (decisions row 21)
- Open, worded as a proposed claim: clock-unit-compatibility (proposed claim; translation-simulation): exact nanoseconds inside, with every recorded millisecond input kept in meaning by an explicit conversion; public nanosecond readings wait for the target's bigint contract (decisions rows 83, 231)
Requirement R13: A run's inputs are dataabout:req:R13
This page explains requirement R13 in Effect4. It covers what the requirement asks for execution inputs, why first-order replay matters, and how the property is checked.
What the requirement asksabout:req:R13:what-it-asks
Requirement R13 demands that every input influencing an execution run is first-order data (docs/core/system-map. §8, DB-01):
- Congruence: equal recorded program syntax, typing signatures, profiles, budgets, tapes, and load values yield equal replay observations.
- Value admission: supplied load values fit admitted load requirements.
- Replay from journal: an execution replays from its recorded journal without calling external hosts (
journal_replays). - Pure decision tapes: decision sequences contain first-order branch choices rather than host functions or promises.
Host closures, uninspected promises, and hidden runtime objects never enter program state.
Why it mattersabout:req:R13:why-it-matters
Distributed and concurrent programs often fail in ways that are difficult to reproduce when inputs depend on ambient system state.
If a runtime allows unrecorded closures or implicit clocks to steer execution, recorded traces cannot reproduce defects reliably.
With every input held as first-order data, a recorded run replays exactly, and a counterexample is a value that can be stored and shared.
How it is checkedabout:req:R13:how-it-is-checked
The requirement is checked by proving replay theorems and congruence over journals and tapes:
- Journal replay is stated by
journal_replaysinsrc/Effect4/Laws/Run..lean - Tape cut replay is stated by
tapeFrom_cut_replays(src/Effect4/Laws/Run/Tape.).lean - Tape position replay is stated by
tapeFrom_position_replaysin the same file. - Reached history congruence is stated by
reached_historyinsrc/Effect4/Laws/Run/Frame..lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- Host Session Protocol proved, 5 nodes → No concept
- No concept proved, 1 nodes
- Translation & Simulation proved, 5 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
journal_replays | proved | — | — |
reached | proved | — | — |
reached_history | proved | — | — |
tapeFrom_append | proved | — | — |
tapeFrom_cut | proved | — | — |
tapeFrom_cut_replays | proved | — | tape_replays, tapeFrom_cut |
tapeFrom_position_replays | proved | — | tape_replays |
history | proved | — | reached_history |
keeps | proved | — | — |
replays | proved | — | journal_replays |
tape_replays | proved | — | — |