WithdrawalCap: a stateful sliding-window rate limiter

The first stateful primitive in Solanalib. Where WindowedDecay / GrowthCurve / MonotoneSequence describe pure functions of time, WithdrawalCap describes a resource that mutates: an accumulator tracking how much has been withdrawn in the current time window, plus the window-start timestamp that resets on interval elapse.

This is the per-reserve last line of defence against drain attacks in lending protocols.

Bug classes the theorems catch

Theorem	Bug class
remaining_le_capacity	Saturating-arithmetic underflow on the remaining calculation
tryAdd_preserves_invariant	current escaping above capacity after a successful add
tryAdd_rejects_over_cap	Off-by-one on the boundary check
interval_reset_idempotent	First add of a new interval forgetting to zero the accumulator

Design notes

• Invariant current ≤ capacity is not embedded in the structure; it's a Prop-valued predicate preserved by tryAdd. Keeps the structure a plain record (no proof obligation at construction).
• Time arithmetic happens at the .toNat level via the Timestamp bridge — UInt64 subtraction would underflow if a caller passed now < windowStart; the .toNat form truncates to 0, which yields "not elapsed" — the safe default.
• intervalSeconds = 0 models a disabled cap — tryAdd is a no-op returning ok c unchanged. Matches Kamino's on-chain behaviour.

structure Solanalib.Finance.WithdrawalCap : Type

A per-reserve withdrawal cap. intervalSeconds = 0 disables the cap.

• capacity : Timestamp

  Maximum lamports addable per window.

• intervalSeconds : Timestamp

  Window length in seconds. 0 disables the cap.

• current : Timestamp

  Lamports added so far in the current window.

• windowStart : Timestamp

  Wall-clock timestamp when the current window started.

@[implicit_reducible]

instance Solanalib.Finance.instReprWithdrawalCap : Repr WithdrawalCap

Equations

• Solanalib.Finance.instReprWithdrawalCap = { reprPrec := Solanalib.Finance.instReprWithdrawalCap.repr }

def Solanalib.Finance.instReprWithdrawalCap.repr : WithdrawalCap → TimestampUnchecked → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Solanalib.Finance.instDecidableEqWithdrawalCap : DecidableEq WithdrawalCap

Equations

• Solanalib.Finance.instDecidableEqWithdrawalCap = Solanalib.Finance.instDecidableEqWithdrawalCap.decEq

def Solanalib.Finance.instDecidableEqWithdrawalCap.decEq (x✝ x✝¹ : WithdrawalCap) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Solanalib.Finance.WithdrawalCap.Invariant (c : WithdrawalCap) : Prop

The invariant a well-formed WithdrawalCap should satisfy.

Equations

• c.Invariant = (c.current ≤ c.capacity)

@[implicit_reducible]

instance Solanalib.Finance.WithdrawalCap.instDecidableInvariant (c : WithdrawalCap) : Decidable c.Invariant

Equations

• c.instDecidableInvariant = id inferInstance

def Solanalib.Finance.WithdrawalCap.IsElapsed (c : WithdrawalCap) (now : Timestamp) : Prop

Has the current window elapsed at time now? Computed at the .toNat level so the comparison cannot underflow.

Equations

• c.IsElapsed now = (c.windowStart.toNat + c.intervalSeconds.toNat ≤ now.toNat)

@[implicit_reducible]

instance Solanalib.Finance.WithdrawalCap.instDecidableIsElapsed (c : WithdrawalCap) (now : Timestamp) : Decidable (c.IsElapsed now)

Equations

• c.instDecidableIsElapsed now = id inferInstance

def Solanalib.Finance.WithdrawalCap.remaining (c : WithdrawalCap) (now : Timestamp) : Timestamp

The maximum amount that can still be added in the current window.

When disabled, returns the largest representable Lamports (so callers treating remaining as a hint won't refuse a valid add). When the window has elapsed, returns the full capacity. Otherwise returns capacity − current.

Equations

• c.remaining now = if c.intervalSeconds.toNat = 0 then UInt64.ofNat (UInt64.size - 1) else if c.IsElapsed now then c.capacity else c.capacity - c.current

inductive Solanalib.Finance.WithdrawalCap.TryAdd : Type

The result of attempting to add to the cap.

• ok (c' : WithdrawalCap) : TryAdd

  Success: the post-operation cap state.

• capReached : TryAdd

  The add would have exceeded the cap; no state change.

def Solanalib.Finance.WithdrawalCap.instReprTryAdd.repr : TryAdd → TimestampUnchecked → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Solanalib.Finance.WithdrawalCap.instReprTryAdd : Repr TryAdd

Equations

• Solanalib.Finance.WithdrawalCap.instReprTryAdd = { reprPrec := Solanalib.Finance.WithdrawalCap.instReprTryAdd.repr }

def Solanalib.Finance.WithdrawalCap.instDecidableEqTryAdd.decEq (x✝ x✝¹ : TryAdd) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Solanalib.Finance.WithdrawalCap.instDecidableEqTryAdd.decEq (Solanalib.Finance.WithdrawalCap.TryAdd.ok c') Solanalib.Finance.WithdrawalCap.TryAdd.capReached = isFalse ⋯
• Solanalib.Finance.WithdrawalCap.instDecidableEqTryAdd.decEq Solanalib.Finance.WithdrawalCap.TryAdd.capReached (Solanalib.Finance.WithdrawalCap.TryAdd.ok c') = isFalse ⋯
• Solanalib.Finance.WithdrawalCap.instDecidableEqTryAdd.decEq Solanalib.Finance.WithdrawalCap.TryAdd.capReached Solanalib.Finance.WithdrawalCap.TryAdd.capReached = isTrue ⋯

@[implicit_reducible]

instance Solanalib.Finance.WithdrawalCap.instDecidableEqTryAdd : DecidableEq TryAdd

Equations

• Solanalib.Finance.WithdrawalCap.instDecidableEqTryAdd = Solanalib.Finance.WithdrawalCap.instDecidableEqTryAdd.decEq

def Solanalib.Finance.WithdrawalCap.tryAdd (c : WithdrawalCap) (amount now : Timestamp) : TryAdd

Try to add amount lamports to the cap at time now.

Three branches:

1. Disabled (intervalSeconds = 0): no-op, return ok c.
2. Window elapsed: reset to a fresh window and check whether amount alone exceeds capacity.
3. Mid-window: check whether current + amount exceeds capacity.

Equations

• One or more equations did not get rendered due to their size.

Theorems

theorem Solanalib.Finance.WithdrawalCap.remaining_le_capacity (c : WithdrawalCap) (now : Timestamp) (h_inv : c.Invariant) (h_enabled : c.intervalSeconds.toNat ≠ 0) : c.remaining now ≤ c.capacity

P1 — Bounded remaining. When the cap is enabled and the invariant holds, remaining never exceeds capacity.

theorem Solanalib.Finance.WithdrawalCap.tryAdd_preserves_invariant (c : WithdrawalCap) (amount now : Timestamp) (h_inv : c.Invariant) {c' : WithdrawalCap} (h_ok : c.tryAdd amount now = TryAdd.ok c') : c'.Invariant

P2 — tryAdd preserves the invariant.

theorem Solanalib.Finance.WithdrawalCap.tryAdd_rejects_over_cap_midwindow (c : WithdrawalCap) (amount now : Timestamp) (h_enabled : c.intervalSeconds.toNat ≠ 0) (h_not_elapsed : ¬c.IsElapsed now) (h_over : c.current.toNat + amount.toNat > c.capacity.toNat) : c.tryAdd amount now = TryAdd.capReached

P3 — tryAdd rejects over-cap requests in mid-window.

theorem Solanalib.Finance.WithdrawalCap.tryAdd_rejects_over_cap_at_reset (c : WithdrawalCap) (amount now : Timestamp) (h_enabled : c.intervalSeconds.toNat ≠ 0) (h_elapsed : c.IsElapsed now) (h_over : amount.toNat > c.capacity.toNat) : c.tryAdd amount now = TryAdd.capReached

P3' — tryAdd rejects over-cap requests at interval reset. After a window elapses, an add still rejects if amount alone exceeds capacity.

theorem Solanalib.Finance.WithdrawalCap.interval_reset_idempotent (c : WithdrawalCap) (amount now : Timestamp) (h_enabled : c.intervalSeconds.toNat ≠ 0) (h_elapsed : c.IsElapsed now) (h_fits : amount.toNat ≤ c.capacity.toNat) {c' : WithdrawalCap} (h_ok : c.tryAdd amount now = TryAdd.ok c') : c'.current = amount ∧ c'.windowStart = now

P4 — Interval-reset idempotence. After the window elapses, a successful add zeroes the previous accumulator and starts a fresh window: c'.current = amount and c'.windowStart = now.