Module log_index 

Sparse-index lookup kernels.

These kernels come out of the OffsetIndex and TimeIndex of krabka-log, so that Creusot can verify them. They use hand-rolled binary searches, the canonical Creusot loop, and not binary_search_by_key. The proofs thus do not depend on a model of the std search.

Structs

IndexEntry

A decoded sparse-index key and the coordinate it selects.

Functions

offset_index_lookup

The position of the last entry at or below target, or zero. Entries must be strictly sorted by relative offset.

offset_index_position_at_or_after

The byte position of the first entry at or after target.

time_index_lookup

The relative offset of the last entry at or below target, or zero. Timestamps must be nondecreasing; equal timestamps are allowed.

time_index_scan_start

A safe sparse starting offset for a forward scan seeking timestamp >= target.

Type Aliases

OffsetEntry

TimeEntry