Module restore 

§12.2 · bounded-tail restore.

One entry point, restore_operation, running the spec’s ladder in the spec’s order:

load latest checkpoint
→ verify checkpoint version/digests/operation/genesis/covered head
→ restore logical state
→ replay and verify checkpoint tail
→ load committed records after through_step_seq
→ verify record chain and step digests
→ replay bounded post-checkpoint tail
→ expose pending effects or terminal

Three properties are load-bearing, and each is a reaction to how the historical resume path failed:

1. There is no second state machine. With a checkpoint or without one, the replay goes through the same prepare/commit fold every live transition goes through, and the driver plans every replayed input exactly as it planned it the first time. The retired recovery path had a separate replay mode, and the two drifted. Here, “restore from genesis” is literally restore_operation with no checkpoint — KernelTransaction::rebuild_from_records — and nothing else.
2. The restore verifies itself. After the logical state is installed and before a single tail input is replayed, the restored runtime is re-projected and the projection is digested. It must equal the checkpoint’s state_digest. A hydration that forgets a field therefore produces a refusal instead of a subtly incomplete runtime.
3. The cost is the tail, not the run. RestoreCost counts what was read, and the count is bounded by the tail bounds plus whatever the journal holds above through_step_seq — never by how long the operation has been running. That is the property §12 exists for, and long_run_restore_cost_is_bounded_by_the_tail measures it rather than asserting it.

Structs

RestoreCost

What a restore actually read.

RestoredOperation

A canonical runtime: the transaction and the driver that plans for it.

Functions

restore_operation

§12.2 · restore one operation from its latest checkpoint plus the records above it.