· 2 min read
A token bucket on integers: what property tests check
How rate-gate computes a token bucket without floats, why milli-tokens, and which three properties the proptest property tests prove.
A rate limiter looks simple until rounding arrives. Store tokens as floats and the error accumulates, and two instances of the algorithm can diverge on the same data. In rate-gate (Rust, axum) tokens are kept in milli-tokens: an integer where 1000 equals one token.
What is computed
The bucket stores a number of milli-tokens and the moment of the last refill. On a check, the refill is elapsed * refill, capped at capacity, then cost is subtracted (it may be above 1). If there are not enough tokens the service answers allowed: false and computes retry_after_ms, how long to wait for the needed tokens, and reset_ms, when the bucket will be full.
Time is passed to the pure functions as a parameter, so tests can "wind" it without sleeping.
Three properties
The property tests (proptest) check laws, not examples:
- over any period the bucket grants at most
capacity + refill * elapsed; - a burst with no time passing does not exceed capacity;
- the sliding-window estimate never exceeds the limit.
The README has no story of a bug being found, and I do not invent one: the point of the properties is that they catch a class of rounding and overflow errors, not one specific bug.
What this does not guarantee
- State lives in the memory of one instance: replicas do not share it.
- The sliding window is approximate: a weighted sum of the current and previous windows, rounded up, that is conservatively.
- The 30-second snapshot is not transactional: after a crash the limits become slightly looser.