Module run 

The run driver: dispatch, turns, freeze — the single authority for the event sequence a run leaves behind. The real city and citysim call this same code, so the simulator’s byte fixtures are evidence about production rather than about a second implementation of the same idea.

Time arrives through the now hook and is never sampled here. The caller decides what a clock is: a counter in the simulator, the one sanctioned wall-clock sample in bin::assembly.

crates/runtime/spec/Run.lean proves what the event sequence must hold (§8-15): handoff_written and run_frozen close every run, once.

Structs

Active

An active run: turns may still be taken.

Charter

What run_started records about a run, and whom every line of the run is written as.

Conclusion

What a harness’s answer leaves for the run to write: the tree as it stood when the harness stopped, what it answered, and the handoff.

Frozen

A frozen run. There is no method back to Active: waking an old run is not something this type can spell, and resume takes a Handoff rather than a run.

HarnessRun

A harness run between its opening and its freeze.

Run

RunHooks

The things the driver cannot decide for itself. Closures rather than traits: no second implementation exists yet, and this library introduces a trait at a seam that already has one.

RunPlan

Everything constant about one run. Assembled by the caller, because what a prefix contains and which tools exist are decisions of the city that dispatches, not of the loop that runs.

Enums

Advance

What one turn did. Exhaustive on purpose: a new ending has to make every caller say what it does about it.

Cut

Why the city cut a harness’s turn short.

SafePoint

Where the driver stops to ask whether anything arrived. The turn layer owns three cancellation-safe points; this enum is how the driver names them to a caller that knows nothing about turn internals.

Functions

drive

Dispatch, turn until an ending, freeze. The loop is here rather than in each caller because the ending rules — an empty wave concludes, a cancellation is an ending too — are the part that must not drift between the city and the simulator.