Lagoon Guardrails PPS Compliance

\texttt{scope}

successfulSolidityArithmeticScope
The successful Solidity execution scope: lowerRate is not int256.min, divisors are nonzero, and the branch-specific multiplication chain does not overflow.

\Rightarrow\;

\texttt{isCompliant}=\mathrm{true}

isCompliant
The modeled GuardrailsLib.isCompliant decision.

\;\Longleftrightarrow\;

\texttt{insideGuardrails}

annualizedVariationInsideGuardrails
The readable interval predicate in Specs.lean, split on whether PPS increased or decreased.

$\text{A PPS update}$ PPS update
The candidate move from currentPps to nextPps. is accepted exactly when its $\text{annualized PPS movement}$ annualized PPS movement
The 1e18-scaled PPS change multiplied by floor(ONE_YEAR / timePast), then divided by currentPps. stays inside the configured $\text{guardrail interval}$ guardrail interval
The upperRate caps increases. The signed lowerRate either requires a minimum increase when nonnegative or permits a bounded decrease when negative..

View Lean

Lagoon provides infrastructure for tokenized vaults. Its v0.6.0 guardrail library checks whether a new vault price per share is still inside the vault's configured annualized movement limits. The function this case verifies is isCompliant.

Why It Matters

PPS is the exchange rate that turns vault shares into underlying assets. A stale, mistaken, or hostile PPS update can change how much value depositors and redeemers receive. Guardrails are the local arithmetic check that decides whether the proposed movement is acceptable before the surrounding vault logic relies on it.

The risk is asymmetric. A positive jump must be no greater than the upper rate, unless the lower rate is also nonnegative, in which case the increase must clear both sides of the configured interval. A negative move is accepted only when the lower rate is negative and the decrease stays within its magnitude. The proof checks that the Boolean returned by the library matches exactly that interval reading.

How This Was Modeled and Proven

We modeled the guardrail arithmetic in Verity Benchmark, with helper functions named after the Solidity quantities: ppsIncreaseVariationNat, ppsDecreaseVariationNat, isCompliant, and successfulSolidityArithmeticScope. The public specification is in Specs.lean; the reference proof is in Proofs.lean.

The proof expands the model and splits on the same cases as the library: increasing PPS versus decreasing PPS, and negative versus nonnegative lower rate. In the increase branch it proves the Boolean comparison is equivalent to the required upper-bound or interval check. In the decrease branch it proves nonnegative lower rates reject the move, while negative lower rates accept exactly when the decrease is no larger than the signed lower-rate magnitude.

Scope

The case targets Lagoon v0.6.0 at commit a8e73f5a5276aa4047b901083cbce127d7f7b470. The modeled unit of value at risk is the PPS movement passed to isCompliant.

The proof covers the pure arithmetic decision in GuardrailsLib.isCompliant: positive movement, negative movement, signed lower-rate handling, and the exact correspondence between the returned Boolean and the readable guardrail predicate.

Out of scope: storage layout, events, role checks, activation gating, vault accounting, and the policy-setting path in updateGuardrails. Those layers can determine which inputs reach the library; this case verifies what the library decides once those inputs are supplied.

Proof artifacts

Contract.lean contains the source-shaped arithmetic model.
Specs.lean contains the readable guardrail predicates.
Proofs.lean proves all five benchmark theorems with no axioms and no sorry placeholders.
The case directory includes the compile target and generated task prompts.

The reference proof is complete under the successful Solidity arithmetic scope below. The focused Lean build target passes:

Function	Theorem	Status
isCompliant	guardrails_positive_upper_only	Proven
isCompliant	guardrails_positive_bounded	Proven
isCompliant	guardrails_nonnegative_lower_rejects_decrease	Proven
isCompliant	guardrails_negative_bounded	Proven
isCompliant	guardrails_exact_compliance	Proven

Verify it yourself

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
git checkout d51f5b83a33754ab32747fa0e7e6398c0f6e8fa4
lake build Benchmark.Cases.Lagoon.Guardrails.Proofs

Hypotheses

No axiom is introduced in the Lagoon proof. The items below state the proof scope: the arithmetic executions covered, the boundary of the modeled library slice, and the external setup this local theorem does not try to prove.

only non-reverting arithmetic is covered
Benchmark/Cases/Lagoon/Guardrails/Specs.lean
The exact-compliance theorem covers successful Solidity arithmetic only: lowerRate is not int256.min, currentPps and timePast are nonzero, and the branch-specific multiplication chain does not overflow. The nonzero-divisor and overflow conditions match Solidity 0.8 revert cases. The int256.min exclusion matches the policy-setting guard and avoids an unsuccessful negative-branch negation.
only the isCompliant check is modeled
Benchmark/Cases/Lagoon/Guardrails/Contract.lean
Only GuardrailsLib.isCompliant is modeled. No part of it is trusted: the proof verifies the arithmetic Boolean it returns once concrete inputs are supplied. The proof trusts the surrounding Lagoon flow to provide those intended inputs and to enforce policy setup. Storage, events, access control, activation checks, and whole-vault execution are out of scope.

Learn More

More case studies

Kuru V2 Shared Withdrawal Budget

After any batch of ordinary withdrawals, the withdrawal budget drops by exactly what was paid out, whichever accounts or tokens were used.

for

Dromos MetaDEX Allocation Conservation

In the root-ledger model, chain allocations sum to committed voting power.

for

KPK Shares Settlement Accounting

A successful kpkShares settlement batch processes each eligible request at most once and accounts exactly for its fees, shares and asset transfers.

for