Module replay 

Offline replay: re-verifies a Ledger without re-executing anything. The second and last minting point for EventRef.

Refusals are fail-closed and name the 1-based line: a higher v and an unknown kind without ig:true speak direction (E_LOG_VERSION_UNSUPPORTED, written by a newer sprawling); a broken chain, a seq gap or non-canonical bytes are storage integrity (E_CAS_CORRUPT). Lines with ig:true and an unknown kind skip the typed parse but still count in the chain — the chain covers raw bytes, not meanings.

Structs

DanglingCalls

The crash-recovery detection half of resume, fed one verified record at a time so it rides the pass that verifies the chain: a tool_called with no later tool_result in the same run is a call whose outcome is unknown, and so is a call its own run followed with another call before any result.

VerifiedLedger

A verified sequence: raw bytes plus their verified reading. Forking consumes this type, never raw lines — a fork of an unverified sequence is unrepresentable (crates/runtime/Spec.lean §10).

Enums

VerifiedLine

One verified line: a typed record with its ref echo, or an explicitly ignorable line from a future vocabulary.

Functions

fold_ledger_dir

A2 folded instead of kept: each record the per-line check reads is lent to each and dropped, so what stays resident is one segment’s bytes and one record rather than every raw line and every record. The same pass builds the LedgerIndex it returns, which covers exactly the history each saw.

outcome_unknown_draft

The repair half: the tool_result draft that closes a dangling call with E_TOOL_OUTCOME_UNKNOWN. The resume path appends it before any new turn — the account never shows a call without an outcome.

rebuild_prefix

A15: recompute the four segment hashes from a prompt_assembled payload plus the same source documents, and check them against the recorded ones. The concatenation rule (join separator, truncation marker) is reused from prefix — one authority, no second copy.

rebuild_shape

A15 over one request’s cache shape: rebuild it from two records - prompt_shape_compared for the tool table and the conversation, and for the four segments the run’s most recent prompt_assembled at or before that line, because a run records prompt_assembled once and prompt_shape_compared once per request - re-derive what moved since the request before it, and refuse either line when the rebuild disagrees with what was written down. A replay re-derives an attribution; it does not trust one.

verify_ledger_dir

A2 over a durable ledger directory; strictly read-only.

verify_lines

A2: offline chain verification over raw lines, through the one per-line check storage::LineCheck owns.