Module ledger 

Event-sourced replay ledger and durable-execution obligations (PSP-8 System 11).

The ledger is an append-only, Merkle-chained event stream. Replay is deterministic over recorded observations: any nondeterministic observation a transition depends on is recorded before it is used, and the kernel refuses to commit a transition that references an observation lacking a ledger record. This structurally discharges the recording obligation at the SDK effect boundary rather than relying on convention.

The six durable-execution obligations (PSP-8 Def 9.1):

• R1 durable single-assignment outcomes (IdempotencyLog);
• R2 recorded nondeterminism (Ledger::record_observation);
• R3 deterministic transition (replay_accepted_trajectory);
• R4 unforgeable capability transport (crate::capability);
• R5 write-ahead external effects (ExternalEffectLog);
• R6 ordered non-commuting durable turns (crate::scheduler).

Structs

AuditReport

The result of a provider-free audit replay (PSP-9 system 14).

ExternalEffectLog

IdempotencyLog

R1 durable single-assignment outcomes. Every proposal/commit outcome is written once and never reassigned; redelivery of the same idempotency key with equivalent content returns the prior result, and key reuse for different content is invalid.

Ledger

The append-only, Merkle-chained event ledger.

LedgerRecord

One record in the Merkle-chained ledger.

Enums

ExternalEffectPhase

R5 write-ahead external effects: each irreversible external effect is bracketed by intent, result, and (where defined) compensation records under a stable idempotency key.

LedgerEvent

A ledgered event (PSP-8 System 11). Representative of the full event family; Custom carries any additional structured event.

ToolLoopBody

The shape of one tool_loop payload (PSP-10 Gate AD).

Functions

audit_replay

Fold the ledger deterministically with credentials absent by construction (nothing in the chain stores one), verifying every link.

content_hash

Hash arbitrary content (for observations and state witnesses).

entry_chain_hash

Compute the chained hash for a record. The chain hash of one ledger entry — sha256(prev_hash || sequence || canonical(event)). Public so external tooling and tests appending rows produce chain-valid entries; the ledger’s integrity comes from verification on read, never from this function being private.

replay_accepted_trajectory

Reconstruct the accepted trajectory deterministically from the recorded events (R3). Replay reads recorded observations rather than re-running nondeterministic sources.

require_recorded

Theorem 7’s recording obligation, adopted literally (PSP-9 system 14): the kernel refuses to commit any transition that depends on an unrecorded observation. Returns the observation hashes on success so the transition record can content-address them.

tool_loop_body

Classify one tool_loop payload by its envelope version.