Crate krabka_verified 

Formally verified pure kernels shared by Krabka crates.

These synchronous kernels have Creusot contracts proved under their stated preconditions. Host state, concurrency, and I/O remain outside that boundary. See docs/verification.md and docs/proof-contract-audit.md.

Re-exports

pub use audit::AuditCheckpointAdmission;

pub use audit::AuditLossMarkerAdmission;

pub use audit::SpoolAppendDecision;

pub use audit::audit_checkpoint_admission;

pub use audit::audit_loss_marker_admission;

pub use audit::spool_append_decision;

pub use authz::AclDecision;

pub use authz::AclOperationKind;

pub use authz::AclPatternKind;

pub use authz::acl_decision;

pub use authz::acl_identity_match;

pub use authz::acl_operation_match;

pub use authz::acl_resource_match;

pub use barrier::BarrierCutClassification;

pub use barrier::BarrierMarkerFenceDecision;

pub use barrier::BarrierMarkerFenceFacts;

pub use barrier::BarrierPlacementDecision;

pub use barrier::BarrierTargetCountDecision;

pub use barrier::barrier_cut_classification;

pub use barrier::barrier_marker_fence_decision;

pub use barrier::barrier_placement_decision;

pub use barrier::barrier_target_count_decision;

pub use break_glass::BreakGlassAdmission;

pub use break_glass::break_glass_admission;

pub use break_glass::select_break_glass_candidate;

pub use break_glass_persistence::BreakGlassConsumptionDecision;

pub use break_glass_persistence::BreakGlassConsumptionFacts;

pub use break_glass_persistence::BreakGlassLocalActionDecision;

pub use break_glass_persistence::BreakGlassLocalActionFacts;

pub use break_glass_persistence::BreakGlassLocalSpendState;

pub use break_glass_persistence::BreakGlassProposalState;

pub use break_glass_persistence::break_glass_consumption_decision;

pub use break_glass_persistence::break_glass_local_action_decision;

pub use broker::DeleteRecordsTrimApplication;

pub use broker::DeleteRecordsTrimDecision;

pub use broker::DeleteRecordsTrimFacts;

pub use broker::FetchVisibility;

pub use broker::FetchWatermarks;

pub use broker::ReplicaFetchMutation;

pub use broker::delete_records_trim_application;

pub use broker::delete_records_trim_decision;

pub use broker::effective_share_backlog;

pub use broker::fetch_visibility;

pub use broker::preferred_rebalance_admission;

pub use broker::replica_fetch_mutation;

pub use broker::unclean_recovery_commit_admission;

pub use chain::ChainStep;

pub use chain::chain_step;

pub use chain::select_chain_tip;

pub use checkpoint::checkpoint_id_newer;

pub use checkpoint::checkpoint_id_retained;

pub use checkpoint::latest_checkpoint_index;

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_has_quorum;

pub use consensus::election_jitter_ms;

pub use consensus::log_is_up_to_date;

pub use consensus::majority_size;

pub use consensus::recompute_high_watermark;

pub use delegation_token::TokenCreateDecision;

pub use delegation_token::TokenDeadlines;

pub use delegation_token::TokenExpireDecision;

pub use delegation_token::TokenMutationDecision;

pub use delegation_token::TokenMutationFacts;

pub use delegation_token::TokenMutationKind;

pub use delegation_token::TokenMutationState;

pub use delegation_token::TokenRenewDecision;

pub use delegation_token::create_token_deadlines;

pub use delegation_token::expire_token_deadline;

pub use delegation_token::renew_token_expiry;

pub use delegation_token::token_mutation_decision;

pub use delivery::coalesce_delivery_range;

pub use delivery::delivery_watermark_advance;

pub use delivery::scheduled_delivery_visible;

pub use directory::DirectoryAssignmentDecision;

pub use directory::DirectoryResponseDecision;

pub use directory::directory_assignment_decision;

pub use directory::directory_response_decision;

pub use diskless::DisklessBatchStep;

pub use diskless::DisklessTrimDecision;

pub use diskless::diskless_batch_step;

pub use diskless::diskless_logical_range;

pub use diskless::diskless_object_reclaimable;

pub use diskless::diskless_retention_prefix;

pub use diskless::diskless_span_extension;

pub use diskless::diskless_trim_decision;

pub use epoch::exact_epoch_successor;

pub use features::FeatureUpdateDecision;

pub use features::feature_update_decision;

pub use freeze::FreezeIdentityState;

pub use freeze::FreezeMutationDecision;

pub use freeze::FreezeMutationKind;

pub use freeze::FreezeReplacementDecision;

pub use freeze::FreezeReplacementFacts;

pub use freeze::FreezeScopeDecision;

pub use freeze::FreezeScopeRank;

pub use freeze::FreezeSignatureDecision;

pub use freeze::FreezeSignatureFacts;

pub use freeze::FreezeStoredState;

pub use freeze::freeze_mutation_decision;

pub use freeze::freeze_refuses;

pub use freeze::freeze_replacement_decision;

pub use freeze::freeze_scope_decision;

pub use freeze::freeze_signature_decision;

pub use freeze::freeze_timestamp_in_window;

pub use group_migration::GroupMigrationDirection;

pub use group_migration::GroupMigrationRecordAction;

pub use group_migration::GroupMigrationRecordPlan;

pub use group_migration::classic_upgrade_epoch;

pub use group_migration::consumer_downgrade_epoch;

pub use group_migration::group_migration_record_plan;

pub use jwks::JwksCacheDecision;

pub use jwks::JwksCacheFacts;

pub use jwks::JwksOnDemandDecision;

pub use jwks::jwks_cache_admission;

pub use jwks::jwks_on_demand_refresh_decision;

pub use jwks::jwks_publication_generations;

pub use leader_epoch::EpochEntry;

pub use leader_epoch::epoch_and_offset_for_entries;

pub use list_offsets::ListOffsetsBoundDecision;

pub use list_offsets::ListOffsetsBoundFacts;

pub use list_offsets::ListOffsetsEarliestFacts;

pub use list_offsets::ListOffsetsEpochDecision;

pub use list_offsets::ListOffsetsKind;

pub use list_offsets::ListOffsetsSelectionDecision;

pub use list_offsets::ListOffsetsSelectionFacts;

pub use list_offsets::list_offsets_bound_decision;

pub use list_offsets::list_offsets_earliest;

pub use list_offsets::list_offsets_epoch_decision;

pub use list_offsets::list_offsets_kind;

pub use list_offsets::list_offsets_selection_decision;

pub use local_recovery::LocalRecoveryStep;

pub use local_recovery::LocalRecoverySwapAction;

pub use local_recovery::local_recovery_batch_step;

pub use local_recovery::local_recovery_index_frontier;

pub use local_recovery::local_recovery_sealed_last;

pub use local_recovery::local_recovery_segment_chain;

pub use local_recovery::local_recovery_swap_action;

pub use log_index::offset_index_lookup;

pub use log_index::offset_index_position_at_or_after;

pub use log_index::time_index_lookup;

pub use oauth::OAuthAuthenticationKind;

pub use oauth::OAuthExpiryPresence;

pub use oauth::OAuthPrincipalMatch;

pub use oauth::OAuthSessionCap;

pub use oauth::OAuthSessionDecision;

pub use oauth::OAuthSessionFacts;

pub use oauth::oauth_session_admission;

pub use offset_allocator::reserve_offsets;

pub use offset_allocator::wal_reservation_epoch_ready;

pub use offset_allocator::wal_reservation_frontier;

pub use offset_allocator::wal_reservation_response;

pub use opa::OpaAuthorizationDecision;

pub use opa::OpaCacheAdmission;

pub use opa::OpaCacheExpiry;

pub use opa::opa_cache_admission;

pub use opa::opa_cache_expiry;

pub use opa::opa_error_decision;

pub use produce::ProduceBatchAdmission;

pub use produce::produce_batch_admission;

pub use produce::produce_durability_frontier;

pub use producer::ProducerDecision;

pub use producer::ProducerEntryFacts;

pub use producer::RetainedSequenceRange;

pub use producer::decrement_sequence;

pub use producer::increment_sequence;

pub use producer::producer_decision;

pub use producer_id::ProducerIdBlockAllocationDecision;

pub use producer_id::ProducerIdBlockPlan;

pub use producer_id::producer_id_block_allocation;

pub use producer_snapshot::ProducerReloadRange;

pub use producer_snapshot::producer_snapshot_entry_valid;

pub use producer_snapshot::producer_snapshot_latest_index;

pub use producer_snapshot::producer_snapshot_reload_keeps;

pub use producer_snapshot::producer_snapshot_reload_log_start;

pub use producer_snapshot::producer_snapshot_replay_start;

pub use producer_snapshot::producer_snapshot_stray;

pub use producer_snapshot::producer_snapshot_strays;

pub use quorum_state::QuorumStateLoadDecision;

pub use quorum_state::QuorumStateWriteDecision;

pub use quorum_state::quorum_state_load_decision;

pub use quorum_state::quorum_state_write_decision;

pub use quota::IpQuotaPrecedence;

pub use quota::QuotaCandidatePresence;

pub use quota::UserClientQuotaFacts;

pub use quota::UserClientQuotaPrecedence;

pub use quota::ip_quota_precedence;

pub use quota::user_client_quota_precedence;

pub use raft::FetchResponseMutation;

pub use raft::fetch_response_mutation;

pub use raft::metadata_record_offset_deltas;

pub use reassignment::ReassignmentAction;

pub use reassignment::ReassignmentSetMembership;

pub use reassignment::reassignment_action;

pub use reassignment::reassignment_plan_admission;

pub use reassignment::reassignment_set_membership;

pub use reconfiguration::VoterChangeKind;

pub use reconfiguration::VoterReconfigurationDecision;

pub use reconfiguration::VoterReconfigurationPlan;

pub use reconfiguration::voter_reconfiguration_decision;

pub use recovery::BarrierRecoveryFinalizeDecision;

pub use recovery::BarrierRecoveryFoldAction;

pub use recovery::BarrierRecoveryRecordKind;

pub use recovery::ReplayCursorDecision;

pub use recovery::ReplayRecordDecision;

pub use recovery::barrier_recovery_finalize_decision;

pub use recovery::barrier_recovery_fold_action;

pub use recovery::replay_batch_cursor_decision;

pub use recovery::replay_cursor_decision;

pub use recovery::replay_record_decision;

pub use recovery::should_capture_first_downgrade;

pub use registration::BrokerHeartbeatDecision;

pub use registration::broker_heartbeat_decision;

pub use remote_metadata::remote_metadata_partition;

pub use remote_metadata::remote_metadata_resume_cursor;

pub use remote_read::remote_read_relative_offset;

pub use remote_read::remote_time_index_candidate_count;

pub use remote_read::tiered_earliest_finished_index;

pub use remote_read::tiered_latest_finished_index;

pub use remote_read::tiered_owning_epoch_index;

pub use remote_txn::RemoteTxnOverlapDecision;

pub use remote_txn::remote_txn_overlap_decision;

pub use restore::RestoreBatchFrame;

pub use restore::RestoreContentExclusions;

pub use restore::RestoreExclusions;

pub use restore::RestoreFilterDecision;

pub use restore::RestoreLayout;

pub use restore::RestoreProducer;

pub use restore::RestoreReconcileDecision;

pub use restore::RestoreRecordDeltas;

pub use restore::RestoreSnapshotState;

pub use restore::RestoreTimestampType;

pub use restore::restore_archive_reconcile;

pub use restore::restore_batch_filter_decision;

pub use restore::restore_batch_past_offset_bound;

pub use restore::restore_batch_step;

pub use restore::restore_record_coordinates;

pub use restore::restore_record_selected;

pub use restore::restore_rewritten_batch_header;

pub use restore::restore_rewritten_record;

pub use restore_sidecar::RestoreAbortedTxn;

pub use restore_sidecar::RestoreSegmentExtent;

pub use restore_sidecar::restore_index_frontier;

pub use restore_sidecar::restore_leader_epoch_entry_valid;

pub use restore_sidecar::restore_offset_index_entry_valid;

pub use restore_sidecar::restore_producer_ids_strict;

pub use restore_sidecar::restore_time_index_entry_valid;

pub use restore_sidecar::restore_txn_index_entry_valid;

pub use retention::barrier_cut_expired;

pub use retention::local_retention_prefix;

pub use retention::retention_delete_target;

pub use schema::SchemaBatchAdmission;

pub use schema::SchemaFailureDecision;

pub use schema::SchemaFailureKind;

pub use schema::SchemaFieldAction;

pub use schema::SchemaFieldRole;

pub use schema::schema_batch_admission;

pub use schema::schema_failure_decision;

pub use schema::schema_field_action;

pub use schema::schema_frame_id;

pub use scram::ScramAlterationDecision;

pub use scram::ScramAlterationFacts;

pub use scram::ScramAlterationKind;

pub use scram::ScramPriorState;

pub use scram::scram_alteration_decision;

pub use share::ShareOffsetMutationDecision;

pub use share::ShareOffsetMutationGate;

pub use share::share_offset_mutation_decision;

pub use share::share_prune_frontier;

pub use snapshot::SnapshotChunkDecision;

pub use snapshot::SnapshotInstallDecision;

pub use snapshot::snapshot_chunk_admission;

pub use snapshot::snapshot_install_decision;

pub use snapshot::snapshot_prune_admission;

pub use stamp::covering_stamp_range_index;

pub use stamp::exact_stamp_range_index;

pub use stamp::stamp_range_insertion_index;

pub use stamp::stamp_ranges_valid;

pub use storage::LocalTruncationPlan;

pub use storage::RemoteCacheAction;

pub use storage::future_log_swap_admission;

pub use storage::local_append_coordinates;

pub use storage::local_truncation_plan;

pub use storage::remote_cache_action;

pub use storage::remote_partition_delete_transition;

pub use storage::remote_segment_transition;

pub use storage::truncation_batch_retained;

pub use storage::truncation_frontier;

pub use storage::truncation_relative_offset;

pub use stretch::min_insync_is_site_loss_safe;

pub use stretch::quorum_survives_any_single_site_loss;

pub use stretch::site_loss_survivors;

pub use timestamp::earliest_max_timestamp_index;

pub use timestamp::first_timestamp_index;

pub use timestamp::timestamp_record_coordinates;

pub use timestamp::timestamp_scan_next;

pub use timestamp::timestamp_scan_window;

pub use transaction::IdleTransactionState;

pub use transaction::NO_TRANSACTION_TIMEOUT_MS;

pub use transaction::TransactionCompletionDecision;

pub use transaction::TransactionIdentity;

pub use transaction::TransactionMarkerMaterializationDecision;

pub use transaction::TransactionReaperCompletionDecision;

pub use transaction::TransactionSnapshot;

pub use transaction::aborted_transaction_interval;

pub use transaction::aborted_transaction_overlaps;

pub use transaction::first_unstable_offset;

pub use transaction::should_abort_idle_transaction;

pub use transaction::transaction_completion_decision;

pub use transaction::transaction_marker_closes;

pub use transaction::transaction_marker_materialization_decision;

pub use transaction::transaction_reaper_completion_decision;

pub use vote::VoteAdmissionDecision;

pub use vote::VoteEncodeDecision;

pub use vote::VoteWireDecision;

pub use vote::vote_admission_decision;

pub use vote::vote_encode_decision;

pub use vote::vote_wire_decision;

pub use voter_set::VoterSetWireDecision;

pub use voter_set::VoterWireDecision;

pub use voter_set::voter_set_wire_decision;

pub use voter_set::voter_wire_decision;

pub use wal::WalFetchAdmission;

pub use wal::exact_wal_batch_range;

pub use wal::select_wal_voter_index;

pub use wal::wal_fetch_admission;

pub use worm::WormDigestFacts;

pub use worm::WormObjectAvailabilityFacts;

pub use worm::WormObjectIdentityFacts;

pub use worm::WormObjectSetDecision;

pub use worm::WormObjectSetFacts;

pub use worm::WormSignatureDecision;

pub use worm::worm_object_set_decision;

pub use worm::worm_signature_decision;

Modules

audit

Pure admission and sync-cadence arithmetic for the audit spool.

authz

Kafka ACL precedence and SASL session/request admission.

barrier

Barrier target, marker-fence, and cut-classification decisions.

break_glass

Break-glass proposal admission and deterministic selection.

break_glass_persistence

Break-glass consumption and local-action persistence decisions.

broker

Pure, safety-critical decision kernels used by krabka-broker.

chain

Sequence and link continuity shared by append-only integrity chains.

checkpoint

KRaft checkpoint selection and retention decisions.

compaction

KIP-534 log-compaction decision core.

consensus

KIP-595 consensus decision kernels, extracted from krabka-kraft-core so Creusot can verify them (the host crate’s Instant/async surface is untranslatable).

delegation_token

KIP-48 delegation-token deadline decisions.

delivery

Scheduled-delivery visibility kernels.

directory

Replica-directory assignment and controller-response decisions.

diskless

Pure local-trim decision for the diskless WAL flusher.

epoch

Exact, overflow-safe advancement for signed metadata epochs.

features

Feature-finalization admission for one UpdateFeatures row.

freeze

Topic-freeze signature, scope, and replacement decisions.

group_migration

Classic and consumer group migration admission and durable record plans.

isr

Classic Kafka ISR decisions: AlterPartition validation on the controller, ISR maintenance and follower catch-up tracking on the partition leader, and the high-watermark computation.

jwks

JWKS cache freshness and on-demand refresh decisions.

leader_epoch

KIP-101/320 leader-epoch divergence lookup kernel: Kafka’s LeaderEpochFileCache.endOffsetFor.

list_offsets

End-to-end ListOffsets request and visibility decisions.

local_recovery

Local-log segment-chain and torn-tail recovery decisions.

log_index

Sparse-index lookup kernels.

oauth

OAuth session-lifetime and reauthentication admission.

offset_allocator

Pure offset-reservation kernel for diskless WAL sequencers.

opa

OPA authorization-cache admission and error policy.

produce

Produce batch-header admission.

producer

Idempotent-producer sequence arithmetic and deduplication decision.

producer_id

Producer-ID block allocation fencing and exact range construction.

producer_snapshot

Producer-snapshot selection, validation, replay, and deletion decisions.

quorum_state

KRaft quorum-state persistence admission.

quota

Kafka quota-entity precedence and quota bucket debt accounting.

raft

Pure KRaft offset-frontier and half-open-window kernels.

reassignment

Partition-reassignment transition decisions.

reconfiguration

KRaft voter-reconfiguration admission and result shape.

recovery

Controller recovery replay-bound decisions.

registration

Broker heartbeat admission decisions.

remote_metadata

KIP-405 remote-log metadata topic partitioning.

remote_read

Remote-segment admission and relative-offset arithmetic.

remote_txn

Inclusive interval integrity for remote aborted-transaction indexes.

restore

Batch-offset continuity, record placement, and rewrite admission for offline restore verification.

restore_sidecar

Restore-side validation of archived sparse indexes and state sidecars.

retention

Retention-prefix selection for the local log and the remote tier.

schema

Schema-registry failure classification and fail-open admission.

scram

SCRAM credential alteration planning decisions.

share

Share-group state pruning and offset-mutation decisions.

snapshot

Snapshot-transfer chunk admission.

stamp

Commit-stamp range-index decisions.

storage

Storage-transition admission decisions.

stretch

Durability arithmetic for a stretch cluster.

throttle

Pure token-bucket consume arithmetic.

timestamp

Timestamp-scan selection and progress kernels.

transaction

Transaction-completion fencing after the EndTxn marker fan-out.

uniform_assignor

Uniform group-assignor kernels (KIP-848 UniformAssignor).

vote

KIP-595 Vote wire and membership admission decisions.

voter_set

KRaft voter-set wire admission.

wal

Diskless WAL admission decisions.

worm

Admission decisions for signed WORM manifests and their object sets.