Linear decay

A quantity that decays linearly from peak at the start of a window to 0 at the end. Outside the window, the value is 0.

This pattern recurs across Solana DeFi:

• Withdrawal-penalty curves in farm contracts: penalty is peak if you unstake at the start of the lock, 0 at maturity.
• Linear vesting: complementary shape; the claimable amount is peak − decay.
• Liquidation-incentive bonuses that decay over time.
• Time-weighted voting power approaching a sunset.

The Lean model below is a single def over Nat (the spec layer); a UInt64 wrapper plus the no-overflow proof lives in a follow-up file.

Main definitions

• Solanalib.Finance.LinearDecay.value — the decaying quantity at a given time.

Main statements

• value_le_peak — bounded above by peak.
• value_antitone_in_window — within the window, value is non-increasing in tNow.
• value_at_begin — at the left boundary, value equals peak.
• value_at_end — at or after the right boundary, value is 0.

Each theorem maps to a specific refactor-bug class:

Theorem	Bug class it catches
value_le_peak	Penalty growing larger than configured (mul/div re-ordering)
value_antitone_in_window	Subtraction direction flipped in the numerator
value_at_begin	Off-by-one on the lock-start guard
value_at_end	Off-by-one on the maturity guard (> vs ≥)

The function is not monotonically antitone globally — at tNow = tBegin it jumps from 0 (outside-window) to peak (inside-window). The honest monotonicity statement (value_antitone_in_window) restricts both timestamps to the locking window.

def Solanalib.Finance.LinearDecay.value (tBegin tNow tEnd peak : Nat) : Nat

The value of a linearly-decaying quantity at time tNow, given the window [tBegin, tEnd) and the peak peak.

Inside the window, the value is peak * (tEnd - tNow) / (tEnd - tBegin). Outside (before tBegin or at/after tEnd), it's 0.

Equations

• Solanalib.Finance.LinearDecay.value tBegin tNow tEnd peak = if tNow < tBegin then 0 else if tEnd ≤ tNow then 0 else peak * (tEnd - tNow) / (tEnd - tBegin)

Theorems

theorem Solanalib.Finance.LinearDecay.value_le_peak (tBegin tNow tEnd peak : Nat) : value tBegin tNow tEnd peak ≤ peak

P1 — Bounded. The decay never exceeds the configured peak.

theorem Solanalib.Finance.LinearDecay.value_antitone_in_window (tBegin tEnd peak : Nat) {t₁ t₂ : Nat} (h_begin : tBegin ≤ t₁) (h_order : t₁ ≤ t₂) (h_end : t₂ < tEnd) : value tBegin t₂ tEnd peak ≤ value tBegin t₁ tEnd peak

P2 — Antitone in tNow (within the window). If t₁ ≤ t₂ and both fall inside the locking window, then value at t₂ is at most value at t₁.

The global function is not monotonically antitone — at tNow = tBegin it jumps from 0 (outside) to peak (inside). The honest statement restricts to in-window timestamps.

theorem Solanalib.Finance.LinearDecay.value_at_begin (tBegin tEnd peak : Nat) (h : tBegin < tEnd) : value tBegin tBegin tEnd peak = peak

P3a — Value at start. At tNow = tBegin (with a non-degenerate window), the value equals the configured peak.

theorem Solanalib.Finance.LinearDecay.value_at_end (tBegin tEnd peak : Nat) : value tBegin tEnd tEnd peak = 0

P3b — Value at end. At or after the right boundary, the value is 0.

WindowedDecay constructor

LinearDecay.toWindowedDecay bundles the value function with its four proof obligations into a WindowedDecay value. Every generic theorem about WindowedDecay (e.g. WindowedDecay.complementary_*) applies automatically to any value produced by this constructor.

def Solanalib.Finance.LinearDecay.toWindowedDecay (tBegin tEnd peak : Nat) : WindowedDecay

Construct the bundled WindowedDecay view of a linear decay. The function-side is value; the four proof obligations are discharged by the corresponding value_* theorems.

Equations

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