Function recompute_high_watermark 

pub fn recompute_high_watermark(
    log_end: i64,
    follower_offsets: &[i64],
    majority: usize,
    epoch_start_offset: i64,
    current_hwm: i64,
    leader_counts: bool,
) -> i64

The HWM as the majority-th largest match offset across the leader’s own log end, when leader_counts, and every follower’s acknowledged fetch offset.

The leader-completeness rule of Raft Fig.8 and KIP-595 gates this value: the HWM may only advance once the majority offset is strictly past epoch_start_offset. The HWM never regresses below current_hwm.

When leader_counts is false (a leader that its own VotersRecord removed), the followers alone must be able to reach majority, which is the second precondition.

The function computes the majority-th largest by its definition, and not by a sort. That definition is the greatest member m of {log_end} U follower_offsets with at least majority members >= m. Voter counts are tiny, at most about 7, and the Creusot proof quantifies over a loop that mirrors the definition.