+ {FORMAL_GUARANTEE}
+
+ + When a user swaps debt tokens for XT, the reserve goes down by + exactly what the pricing curve says it should. +
+
+ s: the contract state
+ (storage) at the time of the swap.
+
+ virtualXtReserve /{' '}
+ virtualXtReserve′: XT
+ reserve before / after.
+
+
+ singleSegmentBuyXtTokenAmtOut(...)
+
+ : how many XT the curve says the user gets. Modeled in Lean from the
+ Solidity source.
+
+ TermMax (by{' '}
+
+ The{' '}
+ swapExactTokenToToken{' '}
+ function is the entry point for exact-input swaps. This case study
+ isolates the{' '}
+ debtToken → XT path
+ on a single curve segment: the path a user takes when borrowing
+ against a single liquidity position. The proof tracks the full call
+ stack from the swap entry point down through the curve library and
+ confirms that the on-chain reserve update matches the curve
+ computation exactly.
+
+ The{' '}
+ virtualXtReserve is
+ the accounting variable that tracks how much XT liquidity remains in
+ the order. Every subsequent swap prices off this value. If the
+ reserve update diverges from the curve computation, even by one
+ wei, all future swaps on that order will price off an incorrect
+ base, and the order's implied interest rate will drift from its
+ configured curve.
+
+ The modeled call stack follows the{' '}
+ debtToken → XT{' '}
+ branch of{' '}
+
+ swapExactTokenToToken
+ {' '}
+ through every internal helper down to the curve computation:
+
+ swapExactTokenToToken
+ {' '}
+ → _swapAndUpdateReserves{' '}
+ → _buyXt{' '}
+ → _buyToken{' '}
+ → _buyXtStep{' '}
+ → TermMaxCurve.buyXt{' '}
+ → cutsReverseIter{' '}
+ → calcIntervalProps
+ MathLib.plusInt256{' '}
+ (signed-integer addition on uint256) is also modeled.
+ nonReentrant{' '}
+ modifier is included. The reentrancy lock is modeled as a
+ separate storage slot.
+
+ Out of scope: other token-pair branches of{' '}
+
+ swapExactTokenToToken
+
+ , access control (
+
+ onlyBorrowingIsAllowed
+
+ ), token transfers, rebalancing, events, and multi-segment curve
+ iteration.
+
+ The benchmark extracts eight Solidity functions across three source
+ files (
+
+ TermMax's curve can have multiple segments, each with its own
+ liquidity parameters. This model covers the case where there is
+ exactly one segment. That means the Solidity loop that iterates
+ over segments runs exactly once, and if the swap needs more
+ liquidity than that single segment provides, the contract reverts
+ with{' '}
+
+ InsufficientLiquidity()
+
+ .
+
+ The model faithfully reproduces the Solidity logic, but with a
+ few deliberate simplifications. The full details are documented
+ in{' '}
+
debtToken → XT{' '}
+ path is modeled. The other token-pair branches of{' '}
+
+ swapExactTokenToToken
+ {' '}
+ are not included.
+
+ onlyBorrowingIsAllowed
+ {' '}
+ modifier does not touch the reserve, so it is left out without
+ weakening the guarantee.
+ nonReentrant,
+ so they cannot affect the proven property.
+ + A few cosmetic differences also exist: struct fields are passed + as individual parameters instead of structs, and library + functions are inlined as helpers. These change the shape of the + code but not its logic. +
+
+ If the build succeeds, the proofs are correct.{' '}
+
+ This case has one headline theorem in Lean 4. The corresponding
+ proof file in the{' '}
+ sorry-free, so
+ the claim below is accepted by Lean's kernel rather than by
+ informal review.
+
| + Guarantee + | ++ Status + | +
|---|---|
| + virtualXtReserve′ = virtualXtReserve − curveOutput + | ++ proven + | +
+
+ The proof uses zero axioms. The five hypotheses below are + preconditions for successful execution. Each one mirrors an + explicit check or implicit requirement in the Solidity source. +
+nonReentrant{' '}
+ modifier. The lock must be open (not already held by a prior
+ call) for the swap to execute.
+
+ revert InsufficientLiquidity()
+
+ .
+
+ revert UnexpectedAmount(minTokenOut, netOut)
+
+ .
+
+
+ Upstream Solidity contracts:{' '}
+
+
+
+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +
+