krabka_verified/quota/debt_cap.rs
1use creusot_std::prelude::*;
2
3/// Greatest representable whole micro-token debt earned during this wait.
4///
5/// The caller converts its time bound to the clock's nanosecond resolution;
6/// carried fractional credit can only repay this conservative cap sooner.
7#[ensures(result@ == (wait_nanos@ * rate@ / 1_000_000_000).min(u64::MAX@))]
8#[must_use]
9pub fn quota_debt_cap(wait_nanos: u128, rate: u64) -> u64 {
10 let Some(numerator) = wait_nanos.checked_mul(u128::from(rate)) else {
11 return u64::MAX;
12 };
13 (numerator / 1_000_000_000).min(18_446_744_073_709_551_615) as u64
14}