From 7a2ca79f2714b8e839cec2fe09152065cfdab077 Mon Sep 17 00:00:00 2001 From: Akshat Mittal Date: Wed, 18 Feb 2026 13:55:45 +0530 Subject: [PATCH 1/9] Certora WIP --- contracts/libraries/Fixed.sol | 3 ++- test/libraries/Fixed.test.ts | 20 ++++++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/contracts/libraries/Fixed.sol b/contracts/libraries/Fixed.sol index 699f64572..fef7903f9 100644 --- a/contracts/libraries/Fixed.sol +++ b/contracts/libraries/Fixed.sol @@ -250,7 +250,7 @@ library FixLib { /// @return x * y // as-ints: x * y/1e18 [division using ROUND, not FLOOR] function mul(uint192 x, uint192 y) internal pure returns (uint192) { - return mul(x, y, ROUND); + return mul(x, y, FLOOR); } /// Multiply this uint192 by a uint192 @@ -547,6 +547,7 @@ library FixLib { RoundingMode rounding ) internal pure returns (uint192) { if (a == 0) return 0; + if (a == FIX_MAX) return FIX_MAX; if (b == 0) return FIX_MAX; uint256 raw = _divrnd(FIX_ONE_256 * a, uint256(b), rounding); diff --git a/test/libraries/Fixed.test.ts b/test/libraries/Fixed.test.ts index 00114889a..bb5b1ab20 100644 --- a/test/libraries/Fixed.test.ts +++ b/test/libraries/Fixed.test.ts @@ -1195,4 +1195,24 @@ describe('In FixLib,', () => { expect(hi).to.equal(bn(0)) }) }) + + describe('Certora Regression Tests', () => { + it('safeMulDiv() may return 0 instead of FIX_MAX', async () => { + const factorization = 3n * 5n * 17n * 257n * 641n * 65537n * 274177n * 6700417n + + const a = bn(factorization) + const b = bn('22894341011050090868949881974522315437050433829130497') + const c = bn('1') + + // a * b / c here equals 2^256 - 1 + // M-01 in the report suggests that this may cause the function to return 0 + // Should be FIX_MAX however. This test confirms it. + + expect(await caller.safeMulDiv(a, b, c, CEIL)).to.equal(MAX_UINT192) + }) + + it('safeDiv() does not correctly propagate the FIX_MAX value', async () => { + expect(await caller.safeDiv(MAX_UINT192, bn('2e18'), ROUND)).to.equal(MAX_UINT192) + }) + }) }) From 41136fd72c3f6cc7b94f645db2863b9edcd230b9 Mon Sep 17 00:00:00 2001 From: Akshat Mittal Date: Fri, 20 Feb 2026 02:52:01 +0530 Subject: [PATCH 2/9] Fix M-01 --- contracts/libraries/Fixed.sol | 4 ++++ test/libraries/Fixed.test.ts | 14 ++++---------- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/contracts/libraries/Fixed.sol b/contracts/libraries/Fixed.sol index fef7903f9..f8550007f 100644 --- a/contracts/libraries/Fixed.sol +++ b/contracts/libraries/Fixed.sol @@ -592,6 +592,10 @@ library FixLib { r *= 2 - c_256 * r; result_256 = lo * r; + if (result_256 >= FIX_MAX) { + return FIX_MAX; + } + // Apply rounding if (rounding == CEIL) { if (mm != 0) result_256 += 1; diff --git a/test/libraries/Fixed.test.ts b/test/libraries/Fixed.test.ts index bb5b1ab20..462ef0718 100644 --- a/test/libraries/Fixed.test.ts +++ b/test/libraries/Fixed.test.ts @@ -1198,17 +1198,11 @@ describe('In FixLib,', () => { describe('Certora Regression Tests', () => { it('safeMulDiv() may return 0 instead of FIX_MAX', async () => { - const factorization = 3n * 5n * 17n * 257n * 641n * 65537n * 274177n * 6700417n + const xa = 2n ** 191n + 1n + const xb = 2n ** 192n - 2n + const xc = 2n ** 127n - const a = bn(factorization) - const b = bn('22894341011050090868949881974522315437050433829130497') - const c = bn('1') - - // a * b / c here equals 2^256 - 1 - // M-01 in the report suggests that this may cause the function to return 0 - // Should be FIX_MAX however. This test confirms it. - - expect(await caller.safeMulDiv(a, b, c, CEIL)).to.equal(MAX_UINT192) + expect(await caller.safeMulDiv(xa, xb, xc, CEIL)).to.equal(MAX_UINT192) }) it('safeDiv() does not correctly propagate the FIX_MAX value', async () => { From 66f26b90abcab3a25a6b5f5592bdd29a540bec45 Mon Sep 17 00:00:00 2001 From: Taylor Brent Date: Thu, 26 Feb 2026 18:38:17 -0500 Subject: [PATCH 3/9] .mul() protocol changes --- contracts/p0/BackingManager.sol | 2 +- contracts/p0/mixins/TradingLib.sol | 2 +- contracts/p1/BackingManager.sol | 2 +- contracts/p1/mixins/TradeLib.sol | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/contracts/p0/BackingManager.sol b/contracts/p0/BackingManager.sol index 752c94cca..f31b4ca94 100644 --- a/contracts/p0/BackingManager.sol +++ b/contracts/p0/BackingManager.sol @@ -176,7 +176,7 @@ contract BackingManagerP0 is TradingP0, IBackingManager { } } - uint192 needed = main.rToken().basketsNeeded().mul(FIX_ONE.plus(backingBuffer)); // {BU} + uint192 needed = main.rToken().basketsNeeded().mul(FIX_ONE.plus(backingBuffer), CEIL); // {BU} // Handout excess assets above what is needed, including any newly minted RToken RevenueTotals memory totals = main.distributor().totals(); diff --git a/contracts/p0/mixins/TradingLib.sol b/contracts/p0/mixins/TradingLib.sol index deea59f83..3b7482bcc 100644 --- a/contracts/p0/mixins/TradingLib.sol +++ b/contracts/p0/mixins/TradingLib.sol @@ -74,7 +74,7 @@ library TradingLibP0 { // Calculate equivalent buyAmount within [0, FIX_MAX] // {buyTok} = {sellTok} * {1} * {UoA/sellTok} / {UoA/buyTok} - uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage)).safeMulDiv( + uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage), CEIL).safeMulDiv( trade.prices.sellLow, trade.prices.buyHigh, CEIL diff --git a/contracts/p1/BackingManager.sol b/contracts/p1/BackingManager.sol index c2ddf852d..1bdca04b0 100644 --- a/contracts/p1/BackingManager.sol +++ b/contracts/p1/BackingManager.sol @@ -222,7 +222,7 @@ contract BackingManagerP1 is TradingP1, IBackingManager { rToken.mint(baskets - rToken.basketsNeeded()); } - uint192 needed = rToken.basketsNeeded().mul(FIX_ONE + backingBuffer); // {BU} + uint192 needed = rToken.basketsNeeded().mul(FIX_ONE + backingBuffer, CEIL); // {BU} // At this point, even though basketsNeeded may have changed, we are: // - We're fully collateralized diff --git a/contracts/p1/mixins/TradeLib.sol b/contracts/p1/mixins/TradeLib.sol index eab2df2c7..e66ca3911 100644 --- a/contracts/p1/mixins/TradeLib.sol +++ b/contracts/p1/mixins/TradeLib.sol @@ -73,7 +73,7 @@ library TradeLib { // Calculate equivalent buyAmount within [0, FIX_MAX] // {buyTok} = {sellTok} * {1} * {UoA/sellTok} / {UoA/buyTok} - uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage)).safeMulDiv( + uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage), CEIL).safeMulDiv( trade.prices.sellLow, trade.prices.buyHigh, CEIL From 3a8f46db28788ed6ee19522e338bce40219e306e Mon Sep 17 00:00:00 2001 From: Taylor Brent Date: Thu, 26 Feb 2026 18:55:31 -0500 Subject: [PATCH 4/9] FixLib tests --- test/libraries/Fixed.fuzz.test.ts | 2 +- test/libraries/Fixed.test.ts | 19 ++++++++++++------- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/test/libraries/Fixed.fuzz.test.ts b/test/libraries/Fixed.fuzz.test.ts index 550b8e662..948332c36 100644 --- a/test/libraries/Fixed.fuzz.test.ts +++ b/test/libraries/Fixed.fuzz.test.ts @@ -260,7 +260,7 @@ describe('FixLib Fuzzing', () => { await binaryOp( [192, 192, 192], caller.mul, - (x, y) => div(x * y, SCALE, RoundingMode.ROUND), + (x, y) => div(x * y, SCALE, RoundingMode.FLOOR), null ) }) diff --git a/test/libraries/Fixed.test.ts b/test/libraries/Fixed.test.ts index 462ef0718..ea1528087 100644 --- a/test/libraries/Fixed.test.ts +++ b/test/libraries/Fixed.test.ts @@ -504,7 +504,7 @@ describe('In FixLib,', () => { const table = commutes.flatMap(([a, b, c]) => [[a, b, c]]) for (const [a, b, c] of table) { expect(await caller.mul(fp(a), fp(b)), `mul(fp(${a}), fp(${b}))`).to.equal(fp(c)) - expect(await caller.safeMul(fp(a), fp(b), ROUND), `safeMul(fp(${a}), fp(${b}))`).to.equal( + expect(await caller.safeMul(fp(a), fp(b), FLOOR), `safeMul(fp(${a}), fp(${b}))`).to.equal( fp(c) ) } @@ -513,13 +513,14 @@ describe('In FixLib,', () => { function mulTest(x: string, y: string, result: string) { it(`mul(${x}, ${y}) == ${result}`, async () => { expect(await caller.mul(fp(x), fp(y))).to.equal(fp(result)) - expect(await caller.safeMul(fp(x), fp(y), ROUND)).to.equal(fp(result)) + expect(await caller.safeMul(fp(x), fp(y), FLOOR)).to.equal(fp(result)) }) } - mulTest('0.5e-9', '1e-9', '1e-18') mulTest('0.49e-9', '1e-9', '0') - mulTest('1.5e-9', '4.5e-8', '68e-18') + mulTest('0.9999999999e-9', '1e-9', '0') + mulTest('1e-9', '1e-9', '1e-18') + mulTest('1.5e-9', '4.5e-8', '67e-18') it('correctly multiplies at the extremes of its range', async () => { const table = [ @@ -531,8 +532,8 @@ describe('In FixLib,', () => { for (const [a, b, c] of table) { expect(await caller.mul(a, b), `mul(${a}, ${b})`).to.equal(c) expect(await caller.mul(b, a), `mul(${b}, ${a})`).to.equal(c) - expect(await caller.safeMul(a, b, ROUND), `safeMul(${b}, ${a})`).to.equal(c) - expect(await caller.safeMul(b, a, ROUND), `safeMul(${b}, ${a})`).to.equal(c) + expect(await caller.safeMul(a, b, FLOOR), `safeMul(${b}, ${a})`).to.equal(c) + expect(await caller.safeMul(b, a, FLOOR), `safeMul(${b}, ${a})`).to.equal(c) } }) @@ -626,7 +627,11 @@ describe('In FixLib,', () => { for (const [a, b, c] of table) { expect(await caller.div(a, b), `div((${a}, ${b})`).to.equal(c) - expect(await caller.safeDiv_(a, b, FLOOR), `safeDiv_((${a}, ${b}, FLOOR)`).to.equal(c) + + const safeResult = a === MAX_UINT192 ? MAX_UINT192 : c + expect(await caller.safeDiv_(a, b, FLOOR), `safeDiv_((${a}, ${b}, FLOOR)`).to.equal( + safeResult + ) } }) it('correctly rounds', async () => { From 2ba0bbb6e594af717e0151df7403b116459fba79 Mon Sep 17 00:00:00 2001 From: Taylor Brent Date: Thu, 26 Feb 2026 19:03:52 -0500 Subject: [PATCH 5/9] Facade .mul() changes --- contracts/facade/facets/ReadFacet.sol | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/contracts/facade/facets/ReadFacet.sol b/contracts/facade/facets/ReadFacet.sol index be038cf30..75a2f3a68 100644 --- a/contracts/facade/facets/ReadFacet.sol +++ b/contracts/facade/facets/ReadFacet.sol @@ -68,7 +68,10 @@ contract ReadFacet { uint192 mid = (low + high) / 2; // {UoA} = {tok} * {UoA/Tok} - depositsUoA[i] = shiftl_toFix(deposits[i], -int8(asset.erc20Decimals()), CEIL).mul(mid); + depositsUoA[i] = shiftl_toFix(deposits[i], -int8(asset.erc20Decimals()), CEIL).mul( + mid, + CEIL + ); } } @@ -355,7 +358,7 @@ contract ReadFacet { uint192 avg = (low + high) / 2; // {UoA} = {UoA} + {tok} - uoaNeeded += needed.mul(avg); + uoaNeeded += needed.mul(avg, CEIL); // {UoA} = {UoA} + {tok} * {UoA/tok} uoaHeldInBaskets += fixMin(needed, asset.bal(address(bm))).mul(avg); From c0696f5266eb44047281576c9513b8795895fcbe Mon Sep 17 00:00:00 2001 From: Taylor Brent Date: Thu, 26 Feb 2026 19:03:58 -0500 Subject: [PATCH 6/9] Recollateralization.test.ts --- test/Recollateralization.test.ts | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/Recollateralization.test.ts b/test/Recollateralization.test.ts index 023ab8406..10c01fdb8 100644 --- a/test/Recollateralization.test.ts +++ b/test/Recollateralization.test.ts @@ -2770,7 +2770,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => { await advanceTime(config.batchAuctionLength.add(100).toString()) // Run auctions - will end current, and will open a new auction to buy the remaining backup tokens - const buyAmtBidRSR: BigNumber = issueAmount.div(2).add(1) // other half to buy + const buyAmtBidRSR: BigNumber = issueAmount.div(2).add(2) // other half to buy await expectEvents(facadeTest.runAuctionsForAllTraders(rToken.address), [ { contract: backingManager, @@ -2805,7 +2805,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => { const t = await getTrade(backingManager, rsr.address) const sellAmtRSR = await t.initBal() - expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR.add(1)) + expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR) // Should have seized RSR expect(await rsr.balanceOf(stRSR.address)).to.equal(stakeAmount.sub(sellAmtRSR)) // Sent to market (auction) @@ -2841,19 +2841,19 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => { expect(await basketHandler.status()).to.equal(CollateralStatus.SOUND) expect(await basketHandler.fullyCollateralized()).to.equal(true) expect(await facadeTest.callStatic.totalAssetValue(rToken.address)).to.equal( - issueAmount.add(1) + issueAmount.add(2) ) expect(await token0.balanceOf(backingManager.address)).to.equal(0) expect(await backupToken1.balanceOf(backingManager.address)).to.equal(issueAmount.div(2)) expect(await backupToken2.balanceOf(backingManager.address)).to.equal( - issueAmount.div(2).add(1) + issueAmount.div(2).add(2) ) expect(await rToken.totalSupply()).to.equal(issueAmount) // Check backing changed await expectCurrentBacking({ tokens: newTokens, - quantities: [issueAmount.div(2), issueAmount.div(2).add(1)], + quantities: [issueAmount.div(2), issueAmount.div(2).add(2)], }) // Check price in USD of the current RToken - Remains the same From 2419f3510d7c4aa5a5ce48ea7d75f557105717da Mon Sep 17 00:00:00 2001 From: Taylor Brent Date: Thu, 26 Feb 2026 20:11:26 -0500 Subject: [PATCH 7/9] Recollateralization.test.ts --- test/Recollateralization.test.ts | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/Recollateralization.test.ts b/test/Recollateralization.test.ts index 10c01fdb8..962185af3 100644 --- a/test/Recollateralization.test.ts +++ b/test/Recollateralization.test.ts @@ -2935,7 +2935,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => { // Run auctions - will end current, and will open a new auction to sell RSR for collateral // 50e18 Tokens left to buy - Sets Buy amount as independent value - const buyAmtBidRSR: BigNumber = sellAmt.div(2).add(1) + const buyAmtBidRSR: BigNumber = sellAmt.div(2).add(2) await expectEvents(facadeTest.runAuctionsForAllTraders(rToken.address), [ { contract: backingManager, @@ -2964,7 +2964,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => { const t = await getTrade(backingManager, rsr.address) const sellAmtRSR = await t.initBal() - expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR.add(1)) + expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR) // Check state expect(await basketHandler.status()).to.equal(CollateralStatus.SOUND) @@ -3045,11 +3045,11 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => { expect(await basketHandler.status()).to.equal(CollateralStatus.SOUND) expect(await basketHandler.fullyCollateralized()).to.equal(true) expect(await facadeTest.callStatic.totalAssetValue(rToken.address)).to.equal( - issueAmount.add(1) // 1 attoTokens accumulated + issueAmount.add(2) // 2 attoTokens accumulated ) expect(await token0.balanceOf(backingManager.address)).to.equal(0) - expect(await backupToken1.balanceOf(backingManager.address)).to.equal(issueAmount.add(1)) - expect(await rToken.totalSupply()).to.equal(issueAmount.add(1)) // free minting + expect(await backupToken1.balanceOf(backingManager.address)).to.equal(issueAmount.add(2)) + expect(await rToken.totalSupply()).to.equal(issueAmount.add(2)) // free minting // Check price in USD of the current RToken - Remains the same await expectRTokenPrice(rTokenAsset.address, fp('1'), ORACLE_ERROR) From cefc427619cc6fcf6b24e9aaa14a2bad4d4a78b1 Mon Sep 17 00:00:00 2001 From: Taylor Brent Date: Thu, 26 Feb 2026 20:12:33 -0500 Subject: [PATCH 8/9] IssuancePremium.test.ts --- test/integration/mainnet-test/IssuancePremium.test.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/integration/mainnet-test/IssuancePremium.test.ts b/test/integration/mainnet-test/IssuancePremium.test.ts index 47da79ca6..88f8482ef 100644 --- a/test/integration/mainnet-test/IssuancePremium.test.ts +++ b/test/integration/mainnet-test/IssuancePremium.test.ts @@ -242,7 +242,7 @@ describeFork(`ETH+ Issuance Premium - Mainnet Forking P${IMPLEMENTATION}`, funct const rETHChange = newQs[2].sub(oldQs[2]).mul(fp('1')).div(oldQs[2]) expect(sfrxETHChange).to.be.closeTo(fp('0.0012'), fp('1e-4')) // sFraxETH +0.12% expect(wstETHChange).to.be.closeTo(fp('0.0001'), fp('1e-4')) // wstETH +0.01% - expect(rETHChange).to.be.equal(0) // rETH no change + expect(rETHChange).to.be.lte(3) // rETH no change }) it('from 4.0.0 to 4.0.0 at-peg', async () => { From 79fe8744049bcf04aca593dc4c681e52acde21f0 Mon Sep 17 00:00:00 2001 From: Taylor Brent Date: Thu, 26 Feb 2026 20:13:06 -0500 Subject: [PATCH 9/9] lint clean --- contracts/p0/BackingManager.sol | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/contracts/p0/BackingManager.sol b/contracts/p0/BackingManager.sol index f31b4ca94..2efc92896 100644 --- a/contracts/p0/BackingManager.sol +++ b/contracts/p0/BackingManager.sol @@ -176,7 +176,8 @@ contract BackingManagerP0 is TradingP0, IBackingManager { } } - uint192 needed = main.rToken().basketsNeeded().mul(FIX_ONE.plus(backingBuffer), CEIL); // {BU} + // {BU} + uint192 needed = main.rToken().basketsNeeded().mul(FIX_ONE.plus(backingBuffer), CEIL); // Handout excess assets above what is needed, including any newly minted RToken RevenueTotals memory totals = main.distributor().totals();