The delay bound backs off linearly from the initial timeout to the maximum timeout

Proved

OpenSearchPreVote.maxDelay_schedule

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

cluster-coordinationconsensuselasticsearchelection-schedulerformal-verificationleader-electionopensearchpaxospre-voteraftzen2

For valid scheduler settings s:

maxDelay s 0 = s.initialTimeout;
maxDelay s k ≤ maxDelay s k' whenever k ≤ k';
for every k with maxDelay s k < s.maxTimeout, maxDelay s (k + 1) is maxDelay s k + s.backoffTime or s.maxTimeout;
maxDelay s k = s.maxTimeout for every k ≥ s.maxTimeout (the number maxTimeout used as an attempt count: since backoffTime ≥ 1, the bound has reached the maximum by then).

Preamble

import Definitions.Def_OpenSearchPreVote
open OpenSearchCoordination OpenSearchPreVote

Formal statement

theorem OpenSearchPreVote.maxDelay_schedule (s : SchedulerSettings) (hs : s.Valid) :
    maxDelay s 0 = s.initialTimeout ∧ (∀ k k', k ≤ k' → maxDelay s k ≤ maxDelay s k') ∧
    (∀ k, maxDelay s k < s.maxTimeout → maxDelay s (k + 1) = maxDelay s k + s.backoffTime ∨
      maxDelay s (k + 1) = s.maxTimeout) ∧
    ∀ k, s.maxTimeout ≤ k → maxDelay s k = s.maxTimeout := by sorry

Source

OpenSearch b2a54ba5c0defba3d1d20423e911d4bf920bab19: PreVoteCollector (state line 79, start 111-115, update 128-131, handlePreVoteRequest 133-163, PreVotingRound 175-300, handlePreVoteResponse 225-279, close 296-299): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/PreVoteCollector.java#L66-L301; Coordinator (updateMaxTermSeen lines 560-581, startElection 583-602, nodeMayWinElection 628-633, getPreVoteResponse 873-879, handleJoin 1267-1299, startElectionScheduler 1567-1618, the preVoteCollector.update calls 516, 653, 777, 801, 839, 1157): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/Coordinator.java#L560-L633; ElectionSchedulerFactory (settings lines 85-115, constructor check 133-143, nonNegative 159-161, toPositiveLongAtMost 169-172, scheduleNextElection 195-241): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/ElectionSchedulerFactory.java#L62-L254; ElectionStrategy.isElectionQuorum (lines 68-88): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/ElectionStrategy.java#L68-L88; the messages PreVoteRequest.java and PreVoteResponse.java in the same directory; CoordinationState (handleStartJoin, handleJoin) as transcribed by the OpenSearchCoordination mission

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5 (independent sub-agent, blind: Lean code + auditor instructions only)

Read-back: `OpenSearchPreVote.maxDelay_schedule`

Notions used

Scheduler settings. A settings value $s$ is four natural numbers: $\mathrm{initialTimeout}$ , $\mathrm{backoffTime}$ , $\mathrm{maxTimeout}$ and $\mathrm{duration}$ (milliseconds, per the docstring). $\mathrm{Valid}(s)$ is the conjunction:

$1 \le \mathrm{initialTimeout} \le 10000$ ;
$1 \le \mathrm{backoffTime} \le 60000$ ;
$200 \le \mathrm{maxTimeout} \le 300000$ ;
$\mathrm{initialTimeout} \le \mathrm{maxTimeout}$ ;
$1 \le \mathrm{duration} \le 300000$ .

Delay bound. $\mathrm{maxDelay}(s, k) = \min(s.\mathrm{maxTimeout},\ s.\mathrm{initialTimeout} + k\cdot s.\mathrm{backoffTime})$ , in natural-number arithmetic.

1. Declaration

Binders and hypothesis.

$s$ : scheduler settings;
$hs$ : $\mathrm{Valid}(s)$ .

Conclusion. Four conjuncts:

$\mathrm{maxDelay}(s, 0) = s.\mathrm{initialTimeout}$ .
$\forall k\, k',\ k \le k' \rightarrow \mathrm{maxDelay}(s, k) \le \mathrm{maxDelay}(s, k')$ : the bound is monotone in the attempt index.
$\forall k,\ \mathrm{maxDelay}(s, k) < s.\mathrm{maxTimeout} \rightarrow \big(\mathrm{maxDelay}(s, k+1) = \mathrm{maxDelay}(s, k) + s.\mathrm{backoffTime} \;\vee\; \mathrm{maxDelay}(s, k+1) = s.\mathrm{maxTimeout}\big)$ . While below the cap, the next bound is one back-off step larger or equals the cap.
$\forall k,\ s.\mathrm{maxTimeout} \le k \rightarrow \mathrm{maxDelay}(s, k) = s.\mathrm{maxTimeout}$ . For every attempt index at least $\mathrm{maxTimeout}$ , the bound equals the cap.

2. What is not constrained

Conjunct 4 is loose. It compares an attempt index $k$ with the millisecond value $\mathrm{maxTimeout}$ . It is true because $\mathrm{backoffTime} \ge 1$ gives $k \cdot \mathrm{backoffTime} \ge k$ .
- The real saturation point is earlier: the first $k$ with $\mathrm{initialTimeout} + k\cdot\mathrm{backoffTime} \ge \mathrm{maxTimeout}$ , that is, $k = \lceil (\mathrm{maxTimeout} - \mathrm{initialTimeout})/\mathrm{backoffTime}\rceil$ .
- With the defaults ( $100$ , $100$ , $10000$ ) the bound first reaches $10000$ at $k = 99$ , which I checked by evaluation. Conjunct 4 asserts saturation only from $k = 10000$ .
- Conjuncts 2 and 4 together do imply $\mathrm{maxDelay}(s, k) \le \mathrm{maxTimeout}$ for every $k$ .
Conjunct 3 is a disjunction. It does not say which alternative holds. Read alone, it would allow a jump straight to $\mathrm{maxTimeout}$ even when one back-off step would stay below the cap. The exact value, $\min(\mathrm{maxTimeout}, \mathrm{maxDelay}(s, k) + \mathrm{backoffTime})$ , comes from the definition and is not stated. When $\mathrm{maxDelay}(s, k) + \mathrm{backoffTime} = \mathrm{maxTimeout}$ , both alternatives hold.
Which parts of $\mathrm{Valid}$ matter. As far as I can see:
- conjunct 1 needs only $\mathrm{initialTimeout} \le \mathrm{maxTimeout}$ ;
- conjunct 4 needs only $\mathrm{backoffTime} \ge 1$ ;
- conjuncts 2 and 3 hold for all settings.
The numeric bounds of $\mathrm{Valid}$ and the field $\mathrm{duration}$ play no role.
What is not stated. Nothing is said about the actual (random) delays, only about their bound $\mathrm{maxDelay}$ .
Vacuity. None. $\mathrm{Valid}$ is satisfiable, for example by the defaults $\langle 100, 100, 10000, 500\rangle$ .

3. Plain-language summary

For valid scheduler settings, the per-attempt delay bound starts at the initial timeout and never decreases. While it is below the maximum timeout, each attempt raises it by exactly the back-off time or brings it to the maximum. It equals the maximum timeout for every attempt index at least as large as the maximum timeout's numeric value, which is a loose saturation bound compared with where the cap is actually reached.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by pitimespi · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph