Lagoon Guardrails PPS Compliance

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 this 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.

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

Proof status

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

• guardrails_positive_upper_onlyproven
• guardrails_positive_boundedproven
• guardrails_nonnegative_lower_rejects_decreaseproven
• guardrails_negative_boundedproven
• guardrails_exact_complianceproven

Assumptions

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.

• successfulSolidityArithmeticScopeSuccessful Solidity arithmetic only

  Benchmark/Cases/Lagoon/Guardrails/Specs.lean

  The exact-compliance theorem applies when 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 correspond to Solidity 0.8 revert cases. The int256.min exclusion matches the policy-setting guard and avoids an unsuccessful negative-branch negation.

• pure_function_sliceOnly GuardrailsLib.isCompliant is modeled

  Benchmark/Cases/Lagoon/Guardrails/Contract.lean

  The proof does not trust part of isCompliant; it verifies the arithmetic Boolean returned by the library once concrete inputs are supplied. It 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.