Crate crabka_verified 

Formally verified pure kernels shared by Crabka’s consensus and log crates.

Every function here is a total, synchronous, allocation-light kernel whose functional contract is proven with Creusot (see docs/verification.md). Host crates call through - there are no duplicate bodies anywhere.

Re-exports

pub use compaction::BatchMeta;

pub use compaction::RecordMeta;

pub use compaction::RetainDecision;

pub use compaction::TxnDataState;

pub use compaction::compute_horizon;

pub use compaction::retain_decision;

pub use consensus::election_jitter_ms;

pub use consensus::log_is_up_to_date;

pub use consensus::recompute_high_watermark;

pub use log_index::offset_index_lookup;

Modules

compaction

KIP-534 log-compaction decision core, extracted from crabka-log so Creusot can verify it. The host crate re-exports these; the stateright model in crabka-log/src/compact_model.rs drives these exact functions.

consensus

KIP-595 consensus decision kernels, extracted from crabka-kraft-core so Creusot can verify them (the host crate’s Instant/async surface is untranslatable). Contracts are added in a follow-up task; the bodies here are already written in the loop style the proofs need (no std sort).

log_index

Offset-index lookup kernel, extracted from crabka-log’s OffsetIndex so Creusot can verify it. Hand-rolled binary search (the canonical Creusot loop) instead of binary_search_by_key, so the proof doesn’t depend on std’s search being modeled.