Module broker 

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

Keeping these small arithmetic decisions here lets Creusot prove the exact executable bodies used by the asynchronous broker.

Structs

DeleteRecordsTrimFacts

Offset facts used to admit one DeleteRecords trim.

FetchVisibility

Visibility bounds and response watermarks for one Fetch partition.

FetchWatermarks

The partition offsets one Fetch visibility decision reads.

PreferredLeaderChange

What a preferred-leader rebalance scan observed about one change it wants to submit.

ReplicaFetchFacts

What a follower knows about one row of a Fetch response when it decides what that row may change.

Enums

DeleteRecordsTrimApplication

The next idempotent step while reconciling WAL and local trim frontiers.

DeleteRecordsTrimDecision

The complete boundary decision for one DeleteRecords trim.

FindCoordinatorAdmission

The complete per-key admission outcome for FindCoordinator.

ReplicaFetchMutation

The only direct mutation class selected from one follower Fetch response.

Functions

delete_records_trim_application

Choose one monotonic trim step, with WAL ordered before the local log.

delete_records_trim_decision

Admit a trim and cap it at every logical deletion frontier.

effective_share_backlog

fetch_visibility

Compute Kafka’s consumer/follower Fetch visibility window.

find_coordinator_admission

Decide whether one FindCoordinator key may proceed to coordinator lookup.

java_string_hash_partition

Java String.hashCode over UTF-16 code units, followed by Kafka’s Utils.abs(hash) % partition_count coordinator selection.

preferred_rebalance_admission

Admit one preferred-leader rebalance batch only when it is nonempty, within the per-tick election cap, and every change in it is a KIP-460 preferred election.

replica_fetch_mutation

Fence one follower Fetch response row against its in-flight request epoch, its current metadata target and any reported leader identity; then select one exclusive response action.

unclean_recovery_commit_admission

Admit an unclean-election commit only against the exact partition snapshot used to select its winner.