Skip to main content

krabka_verified/quota/
request.rs

1use creusot_std::prelude::*;
2
3/// Convert a whole-token request to storage units, limited by the whole tokens
4/// the balance holds.
5///
6/// Saturating the multiplication cannot grant a fractional token or reduce the
7/// largest representable whole-token grant.
8///
9/// # Panics
10/// Panics if `units_per_token` is zero.
11#[requires(units_per_token@ > 0)]
12#[ensures(result@ <= total@ && result@ % units_per_token@ == 0)]
13#[ensures(result@ / units_per_token@ == if requested@ <= total@ / units_per_token@ {
14    requested@
15} else { total@ / units_per_token@ })]
16#[ensures(result@ == (if requested@ <= total@ / units_per_token@ {
17    requested@
18} else { total@ / units_per_token@ }) * units_per_token@)]
19#[must_use]
20pub fn quota_whole_request(requested: u64, total: u64, units_per_token: u64) -> u64 {
21    requested
22        .saturating_mul(units_per_token)
23        .min(total - total % units_per_token)
24}