From c33269482e7329ff7db43ae6e5484be93b5e2e30 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 24 Sep 2024 13:58:40 -0700 Subject: [PATCH] fv lock bids reverts fix --- certora/specs/termAuctionBidLocker/locking.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/specs/termAuctionBidLocker/locking.spec b/certora/specs/termAuctionBidLocker/locking.spec index 26a51e3..c77ad05 100644 --- a/certora/specs/termAuctionBidLocker/locking.spec +++ b/certora/specs/termAuctionBidLocker/locking.spec @@ -311,7 +311,7 @@ rule lockBidsRevertConditions( // support for 2 collateral tokens TermAuctionBidLockerHarness.TermAuctionBid existingBid = harnessGetInternalBids(bidSubmissions[0].id); - require(existingBid.amount == 0 => existingBid.collateralTokens[0] == 0 && existingBid.collateralTokens[1] == 0); // nonexistent bid will not have existing collateral due to minimum bid requirement. + require(existingBid.amount == 0 => existingBid.collateralAmounts[0] == 0 && existingBid.collateralAmounts[1] == 0); // nonexistent bid will not have existing collateral due to minimum bid requirement. require(existingBid.collateralTokens[0] == lockingAuctionCollateralTokenOne); require(existingBid.collateralTokens[1] == lockingAuctionCollateralTokenTwo); require existingBid.collateralTokens.length == 2; @@ -543,7 +543,7 @@ rule lockBidsWithReferralRevertConditions( // support for 2 collateral tokens TermAuctionBidLockerHarness.TermAuctionBid existingBid = harnessGetInternalBids(bidSubmissions[0].id); - require(existingBid.amount == 0 => existingBid.collateralTokens[0] == 0 && existingBid.collateralTokens[1] == 0); // nonexistent bid will not have existing collateral due to minimum bid requirement. + require(existingBid.amount == 0 => existingBid.collateralAmounts[0] == 0 && existingBid.collateralAmounts[1] == 0); // nonexistent bid will not have existing collateral due to minimum bid requirement. require(existingBid.collateralTokens[0] == lockingAuctionCollateralTokenOne); require(existingBid.collateralTokens[1] == lockingAuctionCollateralTokenTwo); require existingBid.collateralTokens.length == 2; @@ -716,7 +716,7 @@ rule lockRolloverBidRevertConditions( ) { bool lockingPaused = lockingPaused(); // LockingPaused bool auctionNotOpen = e.block.timestamp > revealTime(); // AuctionNotOpen - bool nonExistentBid = harnessGetInternalBids(bid.id).amount == 0 && bid.amount == 0; // NonExistentBid + bool nonExistentBid = harnessGetInternalBids(bid.id).amount == 0; // NonExistentBid bool maxBidCountReached = bid.amount != 0 && bidCount() >= MAX_BID_COUNT(); // MaxBidCountReached bool nonRolloverBid = bid.amount != 0 && !bid.isRollover; // NonRolloverBid bool bidAmountTooLow = bid.amount != 0 && bid.amount < minimumTenderAmount(); // BidAmountTooLow @@ -724,7 +724,7 @@ rule lockRolloverBidRevertConditions( bool isExpectedToRevert = lockingPaused || auctionNotOpen || nonExistentBid || maxBidCountReached || nonRolloverBid || bidAmountTooLow || invalidPurchaseToken; - lockRolloverBid(e, bid); + lockRolloverBid@withrevert(e, bid); assert lastReverted == isExpectedToRevert, "lockRolloverBid should revert when one of the revert conditions is reached";