krabka_verified/
lib.rs

1//! Formally verified pure kernels shared by Krabka crates.
2//!
3//! These synchronous kernels have Creusot contracts proved under their stated
4//! preconditions. Host state, concurrency, and I/O remain outside that boundary.
5//! See `docs/verification.md` and `docs/proof-contract-audit.md`.
6#![doc(html_root_url = "https://docs.rs/krabka-verified/1.1.0")]
7// Rust's backend does not see names used only in Creusot contracts, and treats
8// the grouping parentheses in Pearlite expressions as redundant Rust syntax.
9#![cfg_attr(creusot, allow(unused_imports, unused_parens))]
10
11macro_rules! creusot_open_spec {
12    ($item:item) => {
13        #[cfg(creusot)]
14        // cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
15        #[cfg_attr(test, mutants::skip)]
16        #[logic(open)]
17        $item
18    };
19}
20pub(crate) use creusot_open_spec;
21
22pub mod audit;
23pub mod authz;
24pub mod barrier;
25pub mod break_glass;
26pub mod break_glass_persistence;
27pub mod broker;
28pub mod chain;
29pub mod checkpoint;
30pub mod compaction;
31// Split so that clippy's test exemptions see the theorems as test code.
32#[cfg(test)]
33mod composition;
34#[cfg(all(creusot, not(test)))]
35mod composition;
36pub mod consensus;
37pub mod delegation_token;
38pub mod delivery;
39pub mod directory;
40pub mod diskless;
41pub mod epoch;
42pub mod features;
43pub mod freeze;
44pub mod group_migration;
45pub mod isr;
46pub mod jwks;
47pub mod leader_epoch;
48pub mod list_offsets;
49pub mod local_recovery;
50pub mod log_index;
51pub mod oauth;
52pub mod offset_allocator;
53pub mod opa;
54pub mod produce;
55pub mod producer;
56pub mod producer_id;
57pub mod producer_snapshot;
58pub mod quorum_state;
59pub mod quota;
60pub mod raft;
61pub mod reassignment;
62pub mod reconfiguration;
63pub mod recovery;
64pub mod registration;
65pub mod remote_metadata;
66pub mod remote_read;
67pub mod remote_txn;
68pub mod restore;
69pub mod restore_sidecar;
70pub mod retention;
71pub mod schema;
72pub mod scram;
73#[cfg(creusot)]
74mod sequence;
75pub mod share;
76pub mod snapshot;
77pub mod stamp;
78pub mod storage;
79pub mod stretch;
80pub mod throttle;
81pub mod timestamp;
82pub mod transaction;
83pub mod uniform_assignor;
84pub mod vote;
85pub mod voter_set;
86pub mod wal;
87pub mod worm;
88
89pub use {
90    audit::{
91        AuditCheckpointAdmission, AuditLossMarkerAdmission, SpoolAppendDecision,
92        audit_checkpoint_admission, audit_loss_marker_admission, spool_append_decision,
93    },
94    authz::{
95        AclDecision, AclOperationKind, AclPatternKind, acl_decision, acl_identity_match,
96        acl_operation_match, acl_resource_match,
97    },
98    barrier::{
99        BarrierCutClassification, BarrierMarkerFenceDecision, BarrierMarkerFenceFacts,
100        BarrierPlacementDecision, BarrierTargetCountDecision, barrier_cut_classification,
101        barrier_marker_fence_decision, barrier_placement_decision, barrier_target_count_decision,
102    },
103    break_glass::{BreakGlassAdmission, break_glass_admission, select_break_glass_candidate},
104    break_glass_persistence::{
105        BreakGlassConsumptionDecision, BreakGlassConsumptionFacts, BreakGlassLocalActionDecision,
106        BreakGlassLocalActionFacts, BreakGlassLocalSpendState, BreakGlassProposalState,
107        break_glass_consumption_decision, break_glass_local_action_decision,
108    },
109    broker::{
110        DeleteRecordsTrimApplication, DeleteRecordsTrimDecision, DeleteRecordsTrimFacts,
111        FetchVisibility, FetchWatermarks, ReplicaFetchMutation, delete_records_trim_application,
112        delete_records_trim_decision, effective_share_backlog, fetch_visibility,
113        preferred_rebalance_admission, replica_fetch_mutation, unclean_recovery_commit_admission,
114    },
115    chain::{ChainStep, chain_step, select_chain_tip},
116    checkpoint::{checkpoint_id_newer, checkpoint_id_retained, latest_checkpoint_index},
117    compaction::{
118        BatchMeta, RecordMeta, RetainDecision, TxnDataState, compute_horizon, retain_decision,
119    },
120    consensus::{
121        election_has_quorum, election_jitter_ms, log_is_up_to_date, majority_size,
122        recompute_high_watermark,
123    },
124    delegation_token::{
125        TokenCreateDecision, TokenDeadlines, TokenExpireDecision, TokenMutationDecision,
126        TokenMutationFacts, TokenMutationKind, TokenMutationState, TokenRenewDecision,
127        create_token_deadlines, expire_token_deadline, renew_token_expiry, token_mutation_decision,
128    },
129    delivery::{coalesce_delivery_range, delivery_watermark_advance, scheduled_delivery_visible},
130    directory::{
131        DirectoryAssignmentDecision, DirectoryResponseDecision, directory_assignment_decision,
132        directory_response_decision,
133    },
134    diskless::{
135        DisklessBatchStep, DisklessTrimDecision, diskless_batch_step, diskless_logical_range,
136        diskless_object_reclaimable, diskless_retention_prefix, diskless_span_extension,
137        diskless_trim_decision,
138    },
139    epoch::exact_epoch_successor,
140    features::{FeatureUpdateDecision, feature_update_decision},
141    freeze::{
142        FreezeIdentityState, FreezeMutationDecision, FreezeMutationKind, FreezeReplacementDecision,
143        FreezeReplacementFacts, FreezeScopeDecision, FreezeScopeRank, FreezeSignatureDecision,
144        FreezeSignatureFacts, FreezeStoredState, freeze_mutation_decision, freeze_refuses,
145        freeze_replacement_decision, freeze_scope_decision, freeze_signature_decision,
146        freeze_timestamp_in_window,
147    },
148    group_migration::{
149        GroupMigrationDirection, GroupMigrationRecordAction, GroupMigrationRecordPlan,
150        classic_upgrade_epoch, consumer_downgrade_epoch, group_migration_record_plan,
151    },
152    jwks::{
153        JwksCacheDecision, JwksCacheFacts, JwksOnDemandDecision, jwks_cache_admission,
154        jwks_on_demand_refresh_decision, jwks_publication_generations,
155    },
156    leader_epoch::{EpochEntry, epoch_and_offset_for_entries},
157    list_offsets::{
158        ListOffsetsBoundDecision, ListOffsetsBoundFacts, ListOffsetsEarliestFacts,
159        ListOffsetsEpochDecision, ListOffsetsKind, ListOffsetsSelectionDecision,
160        ListOffsetsSelectionFacts, list_offsets_bound_decision, list_offsets_earliest,
161        list_offsets_epoch_decision, list_offsets_kind, list_offsets_selection_decision,
162    },
163    local_recovery::{
164        LocalRecoveryStep, LocalRecoverySwapAction, local_recovery_batch_step,
165        local_recovery_index_frontier, local_recovery_sealed_last, local_recovery_segment_chain,
166        local_recovery_swap_action,
167    },
168    log_index::{offset_index_lookup, offset_index_position_at_or_after, time_index_lookup},
169    oauth::{
170        OAuthAuthenticationKind, OAuthExpiryPresence, OAuthPrincipalMatch, OAuthSessionCap,
171        OAuthSessionDecision, OAuthSessionFacts, oauth_session_admission,
172    },
173    offset_allocator::{
174        reserve_offsets, wal_reservation_epoch_ready, wal_reservation_frontier,
175        wal_reservation_response,
176    },
177    opa::{
178        OpaAuthorizationDecision, OpaCacheAdmission, OpaCacheExpiry, opa_cache_admission,
179        opa_cache_expiry, opa_error_decision,
180    },
181    produce::{ProduceBatchAdmission, produce_batch_admission, produce_durability_frontier},
182    producer::{
183        ProducerDecision, ProducerEntryFacts, RetainedSequenceRange, decrement_sequence,
184        increment_sequence, producer_decision,
185    },
186    producer_id::{
187        ProducerIdBlockAllocationDecision, ProducerIdBlockPlan, producer_id_block_allocation,
188    },
189    producer_snapshot::{
190        ProducerReloadRange, producer_snapshot_entry_valid, producer_snapshot_latest_index,
191        producer_snapshot_reload_keeps, producer_snapshot_reload_log_start,
192        producer_snapshot_replay_start, producer_snapshot_stray, producer_snapshot_strays,
193    },
194    quorum_state::{
195        QuorumStateLoadDecision, QuorumStateWriteDecision, quorum_state_load_decision,
196        quorum_state_write_decision,
197    },
198    quota::{
199        IpQuotaPrecedence, QuotaCandidatePresence, UserClientQuotaFacts, UserClientQuotaPrecedence,
200        ip_quota_precedence, user_client_quota_precedence,
201    },
202    raft::{FetchResponseMutation, fetch_response_mutation, metadata_record_offset_deltas},
203    reassignment::{
204        ReassignmentAction, ReassignmentSetMembership, reassignment_action,
205        reassignment_plan_admission, reassignment_set_membership,
206    },
207    reconfiguration::{
208        VoterChangeKind, VoterReconfigurationDecision, VoterReconfigurationPlan,
209        voter_reconfiguration_decision,
210    },
211    recovery::{
212        BarrierRecoveryFinalizeDecision, BarrierRecoveryFoldAction, BarrierRecoveryRecordKind,
213        ReplayCursorDecision, ReplayRecordDecision, barrier_recovery_finalize_decision,
214        barrier_recovery_fold_action, replay_batch_cursor_decision, replay_cursor_decision,
215        replay_record_decision, should_capture_first_downgrade,
216    },
217    registration::{BrokerHeartbeatDecision, broker_heartbeat_decision},
218    remote_metadata::{remote_metadata_partition, remote_metadata_resume_cursor},
219    remote_read::{
220        remote_read_relative_offset, remote_time_index_candidate_count,
221        tiered_earliest_finished_index, tiered_latest_finished_index, tiered_owning_epoch_index,
222    },
223    remote_txn::{RemoteTxnOverlapDecision, remote_txn_overlap_decision},
224    restore::{
225        RestoreBatchFrame, RestoreContentExclusions, RestoreExclusions, RestoreFilterDecision,
226        RestoreLayout, RestoreProducer, RestoreReconcileDecision, RestoreRecordDeltas,
227        RestoreSnapshotState, RestoreTimestampType, restore_archive_reconcile,
228        restore_batch_filter_decision, restore_batch_past_offset_bound, restore_batch_step,
229        restore_record_coordinates, restore_record_selected, restore_rewritten_batch_header,
230        restore_rewritten_record,
231    },
232    restore_sidecar::{
233        RestoreAbortedTxn, RestoreSegmentExtent, restore_index_frontier,
234        restore_leader_epoch_entry_valid, restore_offset_index_entry_valid,
235        restore_producer_ids_strict, restore_time_index_entry_valid, restore_txn_index_entry_valid,
236    },
237    retention::{barrier_cut_expired, local_retention_prefix, retention_delete_target},
238    schema::{
239        SchemaBatchAdmission, SchemaFailureDecision, SchemaFailureKind, SchemaFieldAction,
240        SchemaFieldRole, schema_batch_admission, schema_failure_decision, schema_field_action,
241        schema_frame_id,
242    },
243    scram::{
244        ScramAlterationDecision, ScramAlterationFacts, ScramAlterationKind, ScramPriorState,
245        scram_alteration_decision,
246    },
247    share::{
248        ShareOffsetMutationDecision, ShareOffsetMutationGate, share_offset_mutation_decision,
249        share_prune_frontier,
250    },
251    snapshot::{
252        SnapshotChunkDecision, SnapshotInstallDecision, snapshot_chunk_admission,
253        snapshot_install_decision, snapshot_prune_admission,
254    },
255    stamp::{
256        covering_stamp_range_index, exact_stamp_range_index, stamp_range_insertion_index,
257        stamp_ranges_valid,
258    },
259    storage::{
260        LocalTruncationPlan, RemoteCacheAction, future_log_swap_admission,
261        local_append_coordinates, local_truncation_plan, remote_cache_action,
262        remote_partition_delete_transition, remote_segment_transition, truncation_batch_retained,
263        truncation_frontier, truncation_relative_offset,
264    },
265    stretch::{
266        min_insync_is_site_loss_safe, quorum_survives_any_single_site_loss, site_loss_survivors,
267    },
268    timestamp::{
269        earliest_max_timestamp_index, first_timestamp_index, timestamp_record_coordinates,
270        timestamp_scan_next, timestamp_scan_window,
271    },
272    transaction::{
273        IdleTransactionState, NO_TRANSACTION_TIMEOUT_MS, TransactionCompletionDecision,
274        TransactionIdentity, TransactionMarkerMaterializationDecision,
275        TransactionReaperCompletionDecision, TransactionSnapshot, aborted_transaction_interval,
276        aborted_transaction_overlaps, first_unstable_offset, should_abort_idle_transaction,
277        transaction_completion_decision, transaction_marker_closes,
278        transaction_marker_materialization_decision, transaction_reaper_completion_decision,
279    },
280    vote::{
281        VoteAdmissionDecision, VoteEncodeDecision, VoteWireDecision, vote_admission_decision,
282        vote_encode_decision, vote_wire_decision,
283    },
284    voter_set::{
285        VoterSetWireDecision, VoterWireDecision, voter_set_wire_decision, voter_wire_decision,
286    },
287    wal::{WalFetchAdmission, exact_wal_batch_range, select_wal_voter_index, wal_fetch_admission},
288    worm::{
289        WormDigestFacts, WormObjectAvailabilityFacts, WormObjectIdentityFacts,
290        WormObjectSetDecision, WormObjectSetFacts, WormSignatureDecision, worm_object_set_decision,
291        worm_signature_decision,
292    },
293};
krabka_verified/lib.rs

krabka_verified/
lib.rs
