Polaris Bonding Curve Reserve-Ratio Invariant

Polaris Finance uses a bonding curve for pETH: users buy pETH by adding a reserve token, and sells or burns move the system back along the same curve. The contract keeps two reserve checkpoints: the live curve point used for trading, and a floor point used when the fee router burns supply.

This case asks a narrow accounting question: after each successful update, do those two stored checkpoints still agree with the curve's reserve formula? Polaris' Foundry invariant calls that zero reserve-ratio deviation. In source terms, each stored reserve balance should match the rounded result of _getBalanceFromReserveRatio.

We modeled the state-changing surface around that invariant: initialization, user buys, user sells, and fee-router floor burns. The benchmark checks that these transitions keep the two stored curve points aligned with the modeled reserve helper, with an explicit linked external boundary for PRB/ABDK fixed-point pow.

Why It Matters

Polaris prices trades from stored curve checkpoints. If a transition updates supply but stores the wrong reserve value, future buys, sells, or floor burns can be priced from a stale or inconsistent point on the curve, causing mispriced buys and sells.

This proof checks that the modeled successful trading and fee-burn paths keep those stored checkpoints aligned with the modeled reserve helper. It is an accounting-integrity proof for Polaris' curve state, not a solvency, custody, ERC-20 balance, or fixed-point math proof.

How This Was Modeled and Proven

We modeled BaseBondingCurve in Verity. The model keeps the storage slots that determine the invariant: virtualBalance, floorSupply, floorBalance, aggregate totalSupply, fee percentage, and initialization state.

The source helper computes (A * pow(supply, B + 1) + 1e18 - 1) / (B + 1). The current model computes the helper's outer arithmetic: it calls a linked curvePow boundary, multiplies the result by A, and performs the source rounding division by B + 1. The theorem statements no longer receive raw pow outputs or assume atrustedCurvePowOutput witness.

This keeps the proof boundary visible: the benchmark checks that the operation sequence computes the modeled helper balance around the linked pow boundary and writes it to the right storage slot. It does not re-derive the PRB/ABDK pow algorithm or its bit-level rounding behavior.

git clone --branch polaris-bonding-curve-reserve-ratio https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Polaris.BondingCurve.Proofs

Assumptions

The benchmark makes these proof boundaries explicit.

• curvePowlinked boundary for PRB/ABDK fixed-point pow

  PRB/ABDK fixed-point exponentiation

  The source computes pow(supply, B + 1) through PRB or ABDK fixed-point math. The benchmark represents that library call as a linked boundary and verifies the Polaris helper arithmetic around it: A * pow and the helper's (left + 1e18 - 1) / (B + 1) division.

• successful pathguards, authorization, and checked arithmetic hold

  Solidity 0.8 execution

  Nonzero amount checks, fee-router authorization, fee branch selection, and overflow/underflow preconditions are modeled as successful-path guards or theorem hypotheses. The sell fee is named separately from the net burn, and fee-router burns reduce aggregate supply while increasing floor supply by the same amount.

View specs in LeanView proofs in Lean

Learn more

Upstream Solidity source: BaseBondingCurve.sol and PRBBondingCurve.sol.

Source helper and deviation formulas: _getBalanceFromReserveRatio and reserveRatioDeviation.

Foundry invariant: BondingCurveInvariants.t.sol.

Verity contract model and full case directory.

What is a formal proof? A short explanation for non-specialists.