Module ledger 

The Ledger port: the only write entrance to history (seam list, ARCHITECTURE section 3), plus the chain rule both adapters and replay share. The part crates/kernel/spec/Ledger.lean specifies this module.

Contract owned here:

• implementations own seq/prev assignment and byte production; callers never serialize. Ok(ref) means the record is durable in that adapter’s medium; Err means nothing observable was appended (torn bytes are the reopen path’s business).
• the chain hashes the canonical line bytes exactly, excluding the line terminator; the genesis line’s prev is 32 zero bytes.
• the port is write-only: production reads go through projections. The read-back needed for verification lives behind the conformance feature and never ships in the production surface.

Constants

GENESIS_PREV

prev of the genesis line: 64 zero hex digits.

Traits

Ledger

The only write entrance to history.

Functions

chain_hash

Chain rule: prev(line k+1) = blake3(canonical bytes of line k). One hash function, one home; jsonl, the in-memory ledger and replay all call this exact function.