Function gcra_decide 

pub fn gcra_decide(
    now_ms: u64,
    tac_ms: u64,
    emission_interval_ms: u64,
    burst_ms: u64,
) -> (bool, u64, u64)

Pure GCRA (Generic Cell Rate Algorithm) conformance decision.

This is the same math as the Redis GCRA Lua script in src/redis.rs (new_tat = max(tac, now) + emission, allow_at = new_tat - emission * burst), lifted out of the DashMap/Redis contexts so the decision core is a total, side-effect-free function that can be exhaustively model-checked with Kani (see tests/kani.rs).

Returns (allowed, retry_after_ms, remaining):

• allowed: whether the request conforms.
• retry_after_ms: milliseconds until the next request can conform; always 0 iff the request was allowed.
• remaining: reported remaining capacity, in [0, burst]; always 0 when the request was denied.

Argument contract

• now_ms / tac_ms: monotonic clock reading and the key’s stored theoretical arrival time (TAC). Every u64 input is handled without overflow or panic: all intermediate math is u128.
• emission_interval_ms: minimum spacing between conforming requests. 0 (sub-millisecond quotas) is clamped to 1 ms so the divisions below are well-defined.
• burst_ms: burst capacity in requests. 0 is strict GCRA: nothing conforms before a full interval has elapsed.