Crate storage 

Effect side of persistence: Ledger on disk, CAS, in-memory derived views, git checkpoints, queues. Implements kernel ports; holds no policy.

Structs

Attribution

AttributionReport

BlockOrigin

The run and the building a block was put for.

Bundle

Export and restore. A namespace rather than a value: neither direction holds state between calls.

Cas

ChainHalt

The verdict a writer shares with the proof of its history: once set it stays, and it carries the reason every refused write repeats.

ChainSnapshot

What a fold held after the line at seq, and the chain hash that names that line.

Checkpoint

DigestCache

Drift

How far a branch has run from the upstream it tracks.

EventQueue

FilePatch

One file’s patch, with what could not be shown named rather than silently dropped.

FileWork

What putting a tree in place cost the filesystem, counted by the code that did the work (crates/storage/spec/Worktree.lean §8-31).

HotView

JsonlLedger

The durable Ledger. See the module doc for the contract.

Landing

What one merge writes down: four values that arrive together and are meaningless apart - a subject with nobody’s provenance under it says who merged nothing. reviewed_by_person adds one Reviewed-by: Name <email> trailer, and only when this repository’s git config also carries user.name and user.email: the city does not invent a person’s name.

LedgerIndex

seq → (segment file name, byte offset of the line start).

LineCheck

Chain state between two lines: what the next line must continue.

LineReader

Reads single lines by seq, holding one segment open across reads.

Located

Where a line sits in the history and whose it is.

Manifest

What a bundle claims to contain. Checked on restore, so a truncated or half-copied bundle is refused rather than restored quietly.

ModelChoice

The model a run was given, and the thinking budget it was asked for.

OpenReport

What open found and repaired, and what its tail recovery read and checked (crates/storage/spec/Jsonl.lean §8-34).

PatchLine

One line of patch text, as a reader may see it.

PlannedMerge

A merge that has been decided and not yet made.

ProofCount

What one proof read and computed: counts rather than time, so a test can hold them at two sizes of history.

ProofRecords

Where a city’s records live, and whether this holder may write them.

Proven

A proof’s verdict, what it cost, and the first record it could not write, which changes no verdict.

Provenance

Who made a commit, and on whose behalf.

QueueItem

Resident

Entries in the order they were placed, each owned by one run and named by its address on disk.

RunHot

RunWaiting

What a run waits for: the room it spoke to and the instant on the city’s clock at which it stops waiting.

Sessions

The slices over one city’s Ledger.

TailLine

One line of the ledger, newest first: its bytes and what it is.

TailLines

The ledger’s lines from the newest back. The walk ends after the oldest line, or after the first failure it yields.

TailTruncation

Unpriced

The model calls that came back with no authoritative amount. They add nothing to total, so without this count a city whose provider never prices a call reads the same as a city that never ran one; the tokens are the one measure of their use the ledger does hold.

Withheld

One line that was not echoed, and why.

WorkingStatus

Where a repository stands right now.

WorktreeLease

A live tree: what it is called, where it is, and what it costs.

WorktreeName

A node’s name for its tree. A newtype because this string becomes a directory name and a git reference: the two ways it can be malformed are checked once, here.

Worktrees

The city’s trees.

WriteTarget

A write target the city has cleared: no alias at the name or at any directory above it, so a write here lands exactly where the name says.

Enums

AliasKind

The aliases one name can be. On Windows a junction and a symbolic link are both reparse points and file_type().is_symlink() answers true for either, which is why they share a variant: refusing the family is one rule, not one rule per reparse tag. The third member of the family - the hard link - is a regular file whose link count is above one (crates/storage/spec/Alias.lean §8-25, crates/storage/Spec.lean §3).

BaseProgress

How far a base checkpoint has got, reported as each step lands.

ChainAudit

What walking the whole chain found.

CheckedLine

A line that passed: a typed record, or an explicitly ignorable line from a newer vocabulary that still counts in the chain.

Head

The far end of the comparison.

LineFault

Why a line did not pass, in the order the check asks.

QueueLane

Which lane a queue serves. The lanes differ in their accounting names and nothing else; the day they differ in behaviour is the day they become separate modules, and that exit condition is stated here rather than discovered later.

Refreshed

What one LedgerIndex::refresh did, and what it lifted off the disk doing it.

RunPhase

A Run’s phase as the hot view sees it. Freezing is terminal here: the ledger may keep appending to a frozen Run’s history, but the phase never travels backwards.

SnapshotFit

Whether the line a positioned read found at the snapshot’s seq is the line the snapshot was cut at.

SnapshotStart

Where a start folds from: the state after a snapshot and the lines past it, or genesis and the reason no snapshot served.

StorageError

Crate root error; crosses the crate boundary only via StorageError::into_ax.

StoredSnapshot

What the snapshot directory holds.

WholeFold

Why a start could not resume from the snapshot.

Constants

MANIFEST

The name of the file that states what a bundle holds.

RECENT_FROZEN

How many frozen runs the hot view holds besides every active one, and so how many a city view carries. A bound on the size of an answer on the wire, not a machine reading, so it is a constant (crates/storage/spec/Hot.lean §8-5).

RESIDENT_TOTAL_BYTES

The whole read-back budget: 12 MiB for the views and the side index and 12 MiB of read-back, the figure Memory.lean’s budget table proposes until a reading replaces it.

Functions

audit_chain

Walk every complete line of the ledger in dir from genesis, each through the one per-line check, reading no record and writing none. Read-only; holds one segment at a time.

between

What moved between base and head, one row per file, path order.

blob_at

The blob at addr in the tree of commit oid, or None when that place in the commit is not a file (a directory, a submodule, nothing).

ledger_segments_at

The ledger segments in dir, in the order they must be read.

line_check_version

The rule version a record is written and accepted under.

of_file

The patch text of one file between base and head.

open_restored

Opens the restored ledger, so the city is one a writer can continue.

parents_of

Each commit’s parents, in the order the commit object states them; None for an oid the repository does not hold. The repository is opened once for the whole list.

prove_chain

Prove the ledger in dir from genesis, taking a segment’s record in place of checking its prefix line by line when the record’s rule version, entry state and digest all match, and writing a record for every segment proved when records may be written.

read_line

Judge one line (without its newline) as a record this build reads, without the chain: the same answer LineCheck::advance gives about the line’s own bytes, for a reader that reached the line through an index whose fold already walked the chain.

read_raw_lines_at

Every complete line of the ledger in dir, copied out. For callers that keep the lines themselves (fork, replay, fixtures); a fold that wants only what the lines say walks LedgerIndex::folding instead.

read_snapshot

Read the snapshot dir holds.

recorded_effort

How an effort nobody asked for is recorded: as Effort::None.

start_from_snapshot

Decide where folding the ledger in ledger_dir starts, given the snapshot in snapshot_dir and the fold rules’ fold_version.

tail_after

Where folding goes on after snapshot, which the caller has already read and accepted: the lines after its seq when its line still sits there, or genesis with the reason it does not.

working_status

What stands between base and the disk under scope, and where the repository itself stands.

write_snapshot

Write snapshot into dir (created when absent), replacing the one there.

Type Aliases

WriteObserver

The write-path observer: what a live reader (the control surface’s event stream) installs to hear each line once it is durable.