Struct LineReader 

pub struct LineReader<'index> { /* private fields */ }

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

One handle and one buffer serve the whole stretch, and a walk that goes forward never seeks at all — the position the previous line left is the position the next one wants. A jump from a known position moves relative to it, so a line that already sits in the buffer — the next line of one run, a few lines of other runs further on — is read without a seek or a refill. What this replaces opened the segment again for every line and then read it one byte at a time. Over a fifty-thousand record ledger on one windows-x86_64 NVMe machine (2026-09-02): 734 µs a line then, against 0.89 µs walking forward and 5.82 µs walking backward now.

This held handle is why line reading is the index’s one step outside Vfs (crates/storage/spec/Vfs.lean §8-15): the seam’s read_at opens the segment per call, which is the 734 µs this type exists to avoid. Nothing here writes, so the crash semantics the seam is there to model have nothing to say about it.

Implementations

impl LineReader<'_>

pub fn line_at(&mut self, seq: Seq) -> Result<Vec<u8>, StorageError>

One line, without its terminator. A seq absent from the index is a caller error, not a corrupt ledger.