krabka_verified/quota/
refill.rs

1use {super::quota_credit, creusot_std::prelude::*};
2
3/// Credit elapsed nanoseconds at a micro-token rate, retaining the fractional
4/// micro-token numerator.
5///
6/// Repay debt before filling the bucket, and discard the fraction when the
7/// bucket reaches its burst. The caller claims the whole elapsed interval
8/// together with the returned state.
9#[requires(fraction@ < 1_000_000_000)]
10#[requires(available@ <= burst@ && (available@ == 0 || debt@ == 0))]
11#[ensures(result.0@ <= burst@ && (result.0@ == 0 || result.1@ == 0))]
12#[ensures(result.2@ < 1_000_000_000)]
13#[ensures({
14    let credit = (elapsed@ * rate@ + fraction@) / 1_000_000_000;
15    result.1@ == if credit <= debt@ { debt@ - credit } else { 0 }
16})]
17#[ensures({
18    let credit = (elapsed@ * rate@ + fraction@) / 1_000_000_000;
19    let paid = if credit <= debt@ { credit } else { debt@ };
20    result.0@ == crate::throttle::capped(available@, credit - paid, burst@)
21})]
22#[ensures(result.2@ == if result.0@ == burst@ && result.1@ == 0 { 0 }
23    else { (elapsed@ * rate@ + fraction@) % 1_000_000_000 })]
24#[ensures({
25    let balance = (available@ - debt@) * 1_000_000_000 + fraction@ + elapsed@ * rate@;
26    (result.0@ - result.1@) * 1_000_000_000 + result.2@
27        == if balance <= burst@ * 1_000_000_000 { balance } else { burst@ * 1_000_000_000 }
28})]
29#[must_use]
30pub fn quota_refill(
31    available: u64,
32    debt: u64,
33    fraction: u64,
34    elapsed: u64,
35    rate: u64,
36    burst: u64,
37) -> (u64, u64, u64) {
38    let numerator = u128::from(elapsed) * u128::from(rate) + u128::from(fraction);
39    let credit = numerator / 1_000_000_000;
40    // The explicit u64 bound keeps the narrowing visible to Clippy.
41    let paid = credit.min(u128::from(debt)).min(18_446_744_073_709_551_615) as u64;
42    let excess = (credit - u128::from(paid))
43        .min(u128::from(burst))
44        .min(18_446_744_073_709_551_615) as u64;
45    let repaid = quota_credit(available, debt, paid, burst);
46    let filled = quota_credit(repaid.0, repaid.1, excess, burst);
47    let fraction = if filled.0 == burst && filled.1 == 0 {
48        0
49    } else {
50        (numerator % 1_000_000_000) as u64
51    };
52    (filled.0, filled.1, fraction)
53}
krabka_verified/quota/refill.rs

krabka_verified/quota/
refill.rs
