From 9fb83a9778af719065a4be373219b998b5135513 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 24 Apr 2026 11:59:54 +0100 Subject: [PATCH 1/7] research: add TermMax buy-XT single-segment case study Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/TermMaxGuarantee.jsx | 106 ++++ data/research.js | 10 + ...termmax-order-v2-buy-xt-single-segment.jsx | 469 ++++++++++++++++++ 3 files changed, 585 insertions(+) create mode 100644 components/research/TermMaxGuarantee.jsx create mode 100644 pages/research/termmax-order-v2-buy-xt-single-segment.jsx diff --git a/components/research/TermMaxGuarantee.jsx b/components/research/TermMaxGuarantee.jsx new file mode 100644 index 0000000..af2a61a --- /dev/null +++ b/components/research/TermMaxGuarantee.jsx @@ -0,0 +1,106 @@ +import { useState, useEffect, useRef } from 'react' +import { ExternalLinkIcon } from './ExternalLink' + +const FORMAL_GUARANTEE = + '∀ s amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)' + +export default function TermMaxGuarantee({ specsHref }) { + const [showEnglish, setShowEnglish] = useState(true) + const timerRef = useRef(null) + + useEffect(() => { + timerRef.current = setTimeout(() => setShowEnglish(false), 5000) + return () => clearTimeout(timerRef.current) + }, []) + + const handleToggle = () => { + if (timerRef.current) { + clearTimeout(timerRef.current) + timerRef.current = null + } + setShowEnglish((prev) => !prev) + } + + return ( +
+ + +
+
+ + {FORMAL_GUARANTEE} + +
+
+

+ After a single-segment exact-input swap of debt tokens for XT, the + on-chain virtual XT reserve decreases by exactly the amount the + pricing curve computes. +

+
+
+ +

+ Names are simplified on purpose:{' '} + amountIn is the exact + debt-token input. +
+ virtualXtReserve is the + on-chain XT reserve before the swap. +
+ + singleSegmentBuyXtTokenAmtOut(...) + {' '} + is the curve-computed XT output, a pure function of the reserve, input, + fee ratio, liquidity, and curve offset. +

+ +
+ + View Lean + + +
+
+ ) +} diff --git a/data/research.js b/data/research.js index 07d639e..5775a56 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'termmax-order-v2-buy-xt-single-segment', + title: 'TermMax Single-Segment Buy-XT Reserve Integrity', + subtitle: + 'Formally verified reserve-update integrity of the single-segment debtToken-to-XT swap path.', + description: + 'How we proved that the single-segment buy-XT path in TermMax OrderV2 updates the virtual XT reserve by exactly the curve-computed output amount, using Verity and Lean 4.', + date: '2026-04-24', + tag: 'Case study' + }, { slug: 'midas-feed-growth-safety', title: 'Midas Growth-Aware Feed Safety Guarantees', diff --git a/pages/research/termmax-order-v2-buy-xt-single-segment.jsx b/pages/research/termmax-order-v2-buy-xt-single-segment.jsx new file mode 100644 index 0000000..fd4d248 --- /dev/null +++ b/pages/research/termmax-order-v2-buy-xt-single-segment.jsx @@ -0,0 +1,469 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import CodeBlock from '../../components/research/CodeBlock' +import Disclosure from '../../components/research/Disclosure' +import ExternalLink from '../../components/research/ExternalLink' +import Hypothesis from '../../components/research/Hypothesis' +import TermMaxGuarantee from '../../components/research/TermMaxGuarantee' +import { getSortedResearch } from '../../lib/getSortedResearch' + +const BENCHMARK_COMMIT_HASH = + 'f70d95716422175702266c0153e4d063c399a5d8' + +const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark +cd verity-benchmark +git checkout ${BENCHMARK_COMMIT_HASH} +lake build Benchmark.Cases.TermMax.OrderV2BuyXtSingleSegment.Compile` + +const UPSTREAM_ORDER_V2 = + 'https://github.com/term-structure/termmax-contract-v2/blob/64bd47b98e064c7fb91ab4a59b70520e0ec285d5/contracts/v2/TermMaxOrderV2.sol' +const UPSTREAM_CURVE = + 'https://github.com/term-structure/termmax-contract-v2/blob/64bd47b98e064c7fb91ab4a59b70520e0ec285d5/contracts/v1/lib/TermMaxCurve.sol' +const UPSTREAM_MATH = + 'https://github.com/term-structure/termmax-contract-v2/blob/64bd47b98e064c7fb91ab4a59b70520e0ec285d5/contracts/v1/lib/MathLib.sol' + +const BENCHMARK_REPO = + 'https://github.com/lfglabs-dev/verity-benchmark' + +const BENCHMARK_COMMIT = + `https://github.com/lfglabs-dev/verity-benchmark/blob/${BENCHMARK_COMMIT_HASH}` + +const CASE_PATH = 'Benchmark/Cases/TermMax/OrderV2BuyXtSingleSegment' +const CONTRACT_LINK = `${BENCHMARK_COMMIT}/${CASE_PATH}/Contract.lean` +const SPECS_LINK = `${BENCHMARK_COMMIT}/${CASE_PATH}/Specs.lean` +const PROOFS_LINK = `${BENCHMARK_COMMIT}/${CASE_PATH}/Proofs.lean` +const CASE_LINK = `${BENCHMARK_COMMIT}/${CASE_PATH}` + +export default function TermMaxOrderV2BuyXtSingleSegmentPage() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'termmax-order-v2-buy-xt-single-segment' + ) + + return ( + <> + + + TermMax Single-Segment Buy-XT Reserve Integrity | Research | LFG Labs + + + + +
+ + +
+

+ TermMax Single-Segment Buy-XT Reserve Integrity +

+
+ +
+ +

+ TermMax (by{' '} + + Term Structure + + ) is a fixed-rate lending protocol. Users trade between debt tokens + and XT (extended tokens) through on-chain order books, where pricing + is governed by a bonding curve parameterized by liquidity, a + time-dependent interest factor, and configurable fee ratios. +

+

+ The{' '} + + TermMaxOrderV2 + {' '} + contract's{' '} + 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. +

+
+ +
+

+ Why this matters +

+

+ 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 call stack here is deep: eight Solidity functions across three + files, with fee deductions, signed-integer arithmetic, and a + constant-product-style curve formula. The proof guarantees that the + full stack produces a reserve update arithmetically faithful to the + curve formula. No intermediate rounding, fee deduction, or storage + read silently shifts the reserve away from the expected value. +

+ +

+ 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. +
    • +
  • + The{' '} + 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. +

+ +
+ +
+

+ How this was modeled +

+

+ The benchmark extracts eight Solidity functions across three source + files ( + + TermMaxOrderV2.sol + + ,{' '} + + TermMaxCurve.sol + + ,{' '} + + MathLib.sol + + ) into a single Verity contract block. Each Solidity helper is kept + as a separate Verity function to preserve the call structure of the + original code. +

+

+ The model is specialized to a single curve segment ( + cuts.length == 1{' '} + with{' '} + + cuts[0].xtReserve == 0 + + ). This is the base case for the curve iteration: the Solidity + reverse-iteration loop executes exactly once, and the cross-cut + branch becomes an explicit{' '} + + revert InsufficientLiquidity() + + . +

+ +

+ Each simplification is a documented Verity DSL gap, verified + against the Verity macro source. The full list with line-level + references is in{' '} + Contract.lean. +

+
    +
  • + Nested arrays (G1):{' '} + + CurveCut[] memory cuts + {' '} + cannot exist as a Verity parameter or storage field. The single + active cut is passed as scalar parameters, and the single-cut + constraint is made explicit. +
    • +
  • + Higher-order parameters (G2): Solidity + function-pointer arguments ( + + function(...) func + + ) cannot be passed.{' '} + + _swapAndUpdateReserves + {' '} + and{' '} + _buyToken are + specialized to their concrete{' '} + _buyXt /{' '} + _buyXtStep{' '} + callees. +
    • +
  • + Library calls (G3):{' '} + + TermMaxCurve.buyXt + + ,{' '} + cutsReverseIter, + and{' '} + + calcIntervalProps + {' '} + are inlined as helper functions. +
    • +
  • + External Lean defs (G4):{' '} + + MathLib.plusInt256 + {' '} + is inlined as an if-then-else. +
    • +
  • + Named structs (G5):{' '} + OrderConfig,{' '} + CurveCut, and{' '} + FeeConfig{' '} + fields are passed as named scalar parameters. +
    • +
  • + Int256 storage (G6):{' '} + Int256 is fully + supported as a parameter type but not as a storage field. The + curve offset enters as a function parameter, so the typing is + faithful. +
    • +
  • + Checked arithmetic (G7): Solidity 0.8 overflow + reverts are not automatic in Verity. Successful-execution + preconditions in the proof play the role of{' '} + Panic(0x11). +
    • +
+ + + {VERIFY_COMMAND} +

+ If the build succeeds, the proofs are correct.{' '} + + Source repository + +

+ +
+ +
+

+ Proof status +

+

+ This case has one headline theorem in Lean 4. The corresponding + proof file in the{' '} + + Verity benchmark repository + {' '} + is sorry-free, so + the claim below is accepted by Lean's kernel rather than by + informal review. +

+
+ + + + + + + + + + + + + +
+ Guarantee + + Status +
+ virtualXtReserve′ = virtualXtReserve − curveOutput + + proven +
+
+

+ View specs in Lean + View proofs in Lean +

+
+ +
+

+ Assumptions +

+

+ The proof uses zero axioms. The five hypotheses below are + preconditions for successful execution — each mirrors an explicit + check or implicit requirement in the Solidity source. +

+
    + + The Solidity entry point skips the swap body when the input is + zero. The model covers the non-trivial execution path. + + + The function uses a{' '} + nonReentrant{' '} + modifier. The lock must be open (not already held by a prior + call) for the swap to execute. + + + The curve formula divides the liquidity squared by the virtual XT + reserve (after applying the curve offset). A zero virtual reserve + would cause a division-by-zero revert. + + + The computed XT output cannot exceed the available reserve. In the + Solidity source, exceeding this triggers{' '} + + revert InsufficientLiquidity() + + . + + + The net output (XT received plus debt tokens returned) must meet + the caller's minimum. In the Solidity source, failing this + triggers{' '} + + revert UnexpectedAmount(minTokenOut, netOut) + + . + +
+

+ View specs in Lean + View proofs in Lean +

+
+ +
+

+ Learn more +

+

+ Upstream Solidity contracts:{' '} + + TermMaxOrderV2.sol + + {', '} + + TermMaxCurve.sol + + {', '} + + MathLib.sol + + . +

+

+ + Full case directory + + {' in the Verity benchmark repository.'} +

+

+ + Verity benchmark repository + + {', which contains the formal specification, machine-checked proofs, and the broader benchmark suite this case belongs to.'} +

+

+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +

+
+ + {otherResearch.length > 0 && ( +
+

+ More research +

+
+ {otherResearch.map((r) => ( + + ))} +
+
+ )} +
+ + + ) +} From 1e55a680ac6d44459e2e7c7edd04fc30c453a1d0 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 24 Apr 2026 12:13:50 +0100 Subject: [PATCH 2/7] fix: simplify guarantee English and clarify curveOutput Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/TermMaxGuarantee.jsx | 27 ++++++++++++------------ 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/components/research/TermMaxGuarantee.jsx b/components/research/TermMaxGuarantee.jsx index af2a61a..9e97010 100644 --- a/components/research/TermMaxGuarantee.jsx +++ b/components/research/TermMaxGuarantee.jsx @@ -2,7 +2,7 @@ import { useState, useEffect, useRef } from 'react' import { ExternalLinkIcon } from './ExternalLink' const FORMAL_GUARANTEE = - '∀ s amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)' + 'virtualXtReserve′ = virtualXtReserve − curveOutput(daysToMaturity, virtualXtReserve, amountIn, fees, curve)' export default function TermMaxGuarantee({ specsHref }) { const [showEnglish, setShowEnglish] = useState(true) @@ -68,26 +68,27 @@ export default function TermMaxGuarantee({ specsHref }) { aria-hidden={!showEnglish} >

- After a single-segment exact-input swap of debt tokens for XT, the - on-chain virtual XT reserve decreases by exactly the amount the - pricing curve computes. + When a user swaps debt tokens for XT, the reserve goes down by + exactly what the pricing curve says it should. Not one wei more, not + one wei less.

- Names are simplified on purpose:{' '} - amountIn is the exact - debt-token input. -
virtualXtReserve is the - on-chain XT reserve before the swap. + on-chain XT reserve before the swap.{' '} + virtualXtReserve′ is its + value after.
+ curveOutput(...){' '} + is the number of XT tokens the bonding curve says the user should + receive. It is a pure function: reserve minus k / (reserve + + input), adjusted for time-to-maturity and fees. In Lean it is called{' '} - singleSegmentBuyXtTokenAmtOut(...) - {' '} - is the curve-computed XT output, a pure function of the reserve, input, - fee ratio, liquidity, and curve offset. + singleSegmentBuyXtTokenAmtOut + + .

From 86f9c86c9501876a43ca69308edb77d408ada6df Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 24 Apr 2026 12:16:45 +0100 Subject: [PATCH 3/7] fix: use real spec name in formal guarantee, drop extra tagline Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/TermMaxGuarantee.jsx | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/components/research/TermMaxGuarantee.jsx b/components/research/TermMaxGuarantee.jsx index 9e97010..3bb0393 100644 --- a/components/research/TermMaxGuarantee.jsx +++ b/components/research/TermMaxGuarantee.jsx @@ -2,7 +2,7 @@ import { useState, useEffect, useRef } from 'react' import { ExternalLinkIcon } from './ExternalLink' const FORMAL_GUARANTEE = - 'virtualXtReserve′ = virtualXtReserve − curveOutput(daysToMaturity, virtualXtReserve, amountIn, fees, curve)' + '∀ s amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)' export default function TermMaxGuarantee({ specsHref }) { const [showEnglish, setShowEnglish] = useState(true) @@ -69,26 +69,23 @@ export default function TermMaxGuarantee({ specsHref }) { >

When a user swaps debt tokens for XT, the reserve goes down by - exactly what the pricing curve says it should. Not one wei more, not - one wei less. + exactly what the pricing curve says it should.

- virtualXtReserve is the - on-chain XT reserve before the swap.{' '} - virtualXtReserve′ is its - value after. + virtualXtReserve /{' '} + virtualXtReserve′: the + on-chain XT reserve before / after the swap.
- curveOutput(...){' '} - is the number of XT tokens the bonding curve says the user should - receive. It is a pure function: reserve minus k / (reserve + - input), adjusted for time-to-maturity and fees. In Lean it is called{' '} - singleSegmentBuyXtTokenAmtOut + singleSegmentBuyXtTokenAmtOut(...) - . + : a pure Lean function modeled from the Solidity source that computes + how many XT tokens the bonding curve yields for a given input + (reserve − k / (reserve + input), + adjusted for time-to-maturity and fees).

From a8740e0f6e4c4e858924c1d4a719aee203c67394 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 24 Apr 2026 14:14:02 +0100 Subject: [PATCH 4/7] fix: shorten footnotes, remove em dashes, clarify single-segment Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/TermMaxGuarantee.jsx | 10 +++--- ...termmax-order-v2-buy-xt-single-segment.jsx | 33 +++++++------------ 2 files changed, 15 insertions(+), 28 deletions(-) diff --git a/components/research/TermMaxGuarantee.jsx b/components/research/TermMaxGuarantee.jsx index 3bb0393..569a82b 100644 --- a/components/research/TermMaxGuarantee.jsx +++ b/components/research/TermMaxGuarantee.jsx @@ -76,16 +76,14 @@ export default function TermMaxGuarantee({ specsHref }) {

virtualXtReserve /{' '} - virtualXtReserve′: the - on-chain XT reserve before / after the swap. + virtualXtReserve′: XT + reserve before / after.
singleSegmentBuyXtTokenAmtOut(...) - : a pure Lean function modeled from the Solidity source that computes - how many XT tokens the bonding curve yields for a given input - (reserve − k / (reserve + input), - adjusted for time-to-maturity and fees). + : how many XT the curve says the user gets. Modeled in Lean from the + Solidity source.

diff --git a/pages/research/termmax-order-v2-buy-xt-single-segment.jsx b/pages/research/termmax-order-v2-buy-xt-single-segment.jsx index fd4d248..1dcbe38 100644 --- a/pages/research/termmax-order-v2-buy-xt-single-segment.jsx +++ b/pages/research/termmax-order-v2-buy-xt-single-segment.jsx @@ -103,24 +103,16 @@ export default function TermMaxOrderV2BuyXtSingleSegmentPage() {

Why this matters

-

+

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 + 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 call stack here is deep: eight Solidity functions across three - files, with fee deductions, signed-integer arithmetic, and a - constant-product-style curve formula. The proof guarantees that the - full stack produces a reserve update arithmetically faithful to the - curve formula. No intermediate rounding, fee deduction, or storage - read silently shifts the reserve away from the expected value. -

The modeled call stack follows the{' '} @@ -193,17 +185,14 @@ export default function TermMaxOrderV2BuyXtSingleSegmentPage() { original code.

- The model is specialized to a single curve segment ( - cuts.length == 1{' '} + 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{' '} - cuts[0].xtReserve == 0 - - ). This is the base case for the curve iteration: the Solidity - reverse-iteration loop executes exactly once, and the cross-cut - branch becomes an explicit{' '} - - revert InsufficientLiquidity() + InsufficientLiquidity() .

@@ -344,8 +333,8 @@ export default function TermMaxOrderV2BuyXtSingleSegmentPage() {

The proof uses zero axioms. The five hypotheses below are - preconditions for successful execution — each mirrors an explicit - check or implicit requirement in the Solidity source. + preconditions for successful execution. Each one mirrors an + explicit check or implicit requirement in the Solidity source.

    Date: Fri, 24 Apr 2026 14:17:59 +0100 Subject: [PATCH 5/7] fix: rewrite simplifications as real model scope, not DSL gaps Co-Authored-By: Claude Opus 4.6 (1M context) --- ...termmax-order-v2-buy-xt-single-segment.jsx | 84 ++++++------------- 1 file changed, 27 insertions(+), 57 deletions(-) diff --git a/pages/research/termmax-order-v2-buy-xt-single-segment.jsx b/pages/research/termmax-order-v2-buy-xt-single-segment.jsx index 1dcbe38..1d57134 100644 --- a/pages/research/termmax-order-v2-buy-xt-single-segment.jsx +++ b/pages/research/termmax-order-v2-buy-xt-single-segment.jsx @@ -198,79 +198,49 @@ export default function TermMaxOrderV2BuyXtSingleSegmentPage() {

    - Each simplification is a documented Verity DSL gap, verified - against the Verity macro source. The full list with line-level - references is in{' '} + The model faithfully reproduces the Solidity logic, but with a + few deliberate simplifications. The full details are documented + in{' '} Contract.lean.

    • - Nested arrays (G1):{' '} - - CurveCut[] memory cuts - {' '} - cannot exist as a Verity parameter or storage field. The single - active cut is passed as scalar parameters, and the single-cut - constraint is made explicit. -
      • -
    • - Higher-order parameters (G2): Solidity - function-pointer arguments ( - - function(...) func - - ) cannot be passed.{' '} - - _swapAndUpdateReserves - {' '} - and{' '} - _buyToken are - specialized to their concrete{' '} - _buyXt /{' '} - _buyXtStep{' '} - callees. + Single curve segment only. The Solidity + contract supports multiple curve segments and iterates over + them. This model covers exactly one segment. Multi-segment + swaps are not covered.
    • - Library calls (G3):{' '} + One swap direction. Only the{' '} + debtToken → XT{' '} + path is modeled. The other token-pair branches of{' '} - TermMaxCurve.buyXt - - ,{' '} - cutsReverseIter, - and{' '} - - calcIntervalProps + swapExactTokenToToken {' '} - are inlined as helper functions. + are not included.
    • - External Lean defs (G4):{' '} + Access control omitted. The{' '} - MathLib.plusInt256 + onlyBorrowingIsAllowed {' '} - is inlined as an if-then-else. -
      • -
    • - Named structs (G5):{' '} - OrderConfig,{' '} - CurveCut, and{' '} - FeeConfig{' '} - fields are passed as named scalar parameters. + modifier does not touch the reserve, so it is left out without + weakening the guarantee.
    • - Int256 storage (G6):{' '} - Int256 is fully - supported as a parameter type but not as a storage field. The - curve offset enters as a function parameter, so the typing is - faithful. -
      • -
    • - Checked arithmetic (G7): Solidity 0.8 overflow - reverts are not automatic in Verity. Successful-execution - preconditions in the proof play the role of{' '} - Panic(0x11). + Post-swap side effects omitted. Token + transfers, rebalancing, and events all happen after the + reserve write and are guarded by{' '} + 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. +

    {VERIFY_COMMAND} From 2610b650462a48ba397da6cb913cb0355328e864 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 24 Apr 2026 14:24:53 +0100 Subject: [PATCH 6/7] fix: drop redundant s from formal guarantee line Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/TermMaxGuarantee.jsx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/research/TermMaxGuarantee.jsx b/components/research/TermMaxGuarantee.jsx index 569a82b..0806926 100644 --- a/components/research/TermMaxGuarantee.jsx +++ b/components/research/TermMaxGuarantee.jsx @@ -2,7 +2,7 @@ import { useState, useEffect, useRef } from 'react' import { ExternalLinkIcon } from './ExternalLink' const FORMAL_GUARANTEE = - '∀ s amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)' + '∀ amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)' export default function TermMaxGuarantee({ specsHref }) { const [showEnglish, setShowEnglish] = useState(true) From ec3342bddadb00c8e6d3423c36eb78ff655a94aa Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 24 Apr 2026 14:25:36 +0100 Subject: [PATCH 7/7] fix: restore s in formal guarantee, add footnote explaining it Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/TermMaxGuarantee.jsx | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/components/research/TermMaxGuarantee.jsx b/components/research/TermMaxGuarantee.jsx index 0806926..28e3325 100644 --- a/components/research/TermMaxGuarantee.jsx +++ b/components/research/TermMaxGuarantee.jsx @@ -2,7 +2,7 @@ import { useState, useEffect, useRef } from 'react' import { ExternalLinkIcon } from './ExternalLink' const FORMAL_GUARANTEE = - '∀ amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)' + '∀ s amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)' export default function TermMaxGuarantee({ specsHref }) { const [showEnglish, setShowEnglish] = useState(true) @@ -75,6 +75,9 @@ export default function TermMaxGuarantee({ specsHref }) {

+ s: the contract state + (storage) at the time of the swap. +
virtualXtReserve /{' '} virtualXtReserve′: XT reserve before / after.