Skip to content

Commit

Permalink
use mathint
Browse files Browse the repository at this point in the history
  • Loading branch information
@sunbreak1211
sunbreak1211 committed Oct 19, 2024
1 parent 4ec1189 commit e11132d
Show file tree
Hide file tree
Showing 3 changed files with 38 additions and 38 deletions.
36 changes: 18 additions & 18 deletions certora/L1TokenBridge.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ rule close() {

close(e);

uint256 isOpenAfter = isOpen();
mathint isOpenAfter = isOpen();

assert isOpenAfter == 0, "Assert 1";
}
Expand Down Expand Up @@ -204,8 +204,8 @@ rule bridgeERC20(address _localToken, address _remoteToken, uint256 _amount, uin
require e.msg.sender != escrow;

bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, e.msg.sender, _amount, _extraData);
uint256 localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
uint256 localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
mathint localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
// ERC20 assumption
require gem.totalSupply >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;

Expand All @@ -214,8 +214,8 @@ rule bridgeERC20(address _localToken, address _remoteToken, uint256 _amount, uin
address lastTargetAfter = l1messenger.lastTarget();
bytes32 lastMessageHashAfter = l1messenger.lastMessageHash();
uint32 lastMinGasLimitAfter = l1messenger.lastMinGasLimit();
uint256 localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
uint256 localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);
mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
mathint localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);

assert lastTargetAfter == otherBridge, "Assert 1";
assert lastMessageHashAfter == message, "Assert 2";
Expand All @@ -233,8 +233,8 @@ rule bridgeERC20_revert(address _localToken, address _remoteToken, uint256 _amou

address escrow = escrow();

uint256 localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
uint256 localTokenBalanceOfEscrow = gem.balanceOf(escrow);
mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
mathint localTokenBalanceOfEscrow = gem.balanceOf(escrow);

// ERC20 assumption
require gem.totalSupply() >= localTokenBalanceOfSender + localTokenBalanceOfEscrow;
Expand Down Expand Up @@ -264,8 +264,8 @@ rule bridgeERC20To(address _localToken, address _remoteToken, address _to, uint2
require e.msg.sender != escrow;

bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, _to, _amount, _extraData);
uint256 localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
uint256 localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
mathint localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
// ERC20 assumption
require gem.totalSupply >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;

Expand All @@ -274,8 +274,8 @@ rule bridgeERC20To(address _localToken, address _remoteToken, address _to, uint2
address lastTargetAfter = l1messenger.lastTarget();
bytes32 lastMessageHashAfter = l1messenger.lastMessageHash();
uint32 lastMinGasLimitAfter = l1messenger.lastMinGasLimit();
uint256 localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
uint256 localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);
mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
mathint localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);

assert lastTargetAfter == otherBridge, "Assert 1";
assert lastMessageHashAfter == message, "Assert 2";
Expand All @@ -293,8 +293,8 @@ rule bridgeERC20To_revert(address _localToken, address _remoteToken, address _to

address escrow = escrow();

uint256 localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
uint256 localTokenBalanceOfEscrow = gem.balanceOf(escrow);
mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
mathint localTokenBalanceOfEscrow = gem.balanceOf(escrow);

// ERC20 assumption
require gem.totalSupply() >= localTokenBalanceOfSender + localTokenBalanceOfEscrow;
Expand All @@ -319,16 +319,16 @@ rule finalizeBridgeERC20(address _localToken, address _remoteToken, address _fro

address escrow = escrow();

uint256 localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
uint256 localTokenBalanceOfToBefore = gem.balanceOf(_to);
mathint localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
mathint localTokenBalanceOfToBefore = gem.balanceOf(_to);

// ERC20 assumption
require gem.totalSupply() >= localTokenBalanceOfEscrowBefore + localTokenBalanceOfToBefore;

finalizeBridgeERC20(e, _localToken, _remoteToken, _from, _to, _amount, _extraData);

uint256 localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);
uint256 localTokenBalanceOfToAfter = gem.balanceOf(_to);
mathint localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);
mathint localTokenBalanceOfToAfter = gem.balanceOf(_to);

assert escrow != _to => localTokenBalanceOfEscrowAfter == localTokenBalanceOfEscrowBefore - _amount, "Assert 1";
assert escrow != _to => localTokenBalanceOfToAfter == localTokenBalanceOfToBefore + _amount, "Assert 2";
Expand All @@ -346,7 +346,7 @@ rule finalizeBridgeERC20_revert(address _localToken, address _remoteToken, addre
address xDomainMessageSender = l1messenger.xDomainMessageSender();
address escrow = escrow();

uint256 localTokenBalanceOfEscrow = gem.balanceOf(escrow);
mathint localTokenBalanceOfEscrow = gem.balanceOf(escrow);

// ERC20 assumption
require gem.totalSupply() >= localTokenBalanceOfEscrow + gem.balanceOf(_to);
Expand Down
2 changes: 1 addition & 1 deletion certora/L2GovernanceRelay.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ definition addrZero() returns address = 0x00000000000000000000000000000000000000

persistent ghost bool called;
persistent ghost address calledAddr;
persistent ghost uint256 dataLength;
persistent ghost mathint dataLength;
persistent ghost bool success;
hook DELEGATECALL(uint256 g, address addr, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc {
called = true;
Expand Down
38 changes: 19 additions & 19 deletions certora/L2TokenBridge.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ rule close() {

close(e);

uint256 isOpenAfter = isOpen();
mathint isOpenAfter = isOpen();

assert isOpenAfter == 0, "Assert 1";
}
Expand Down Expand Up @@ -203,8 +203,8 @@ rule bridgeERC20(address _localToken, address _remoteToken, uint256 _amount, uin
address otherBridge = otherBridge();

bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, e.msg.sender, _amount, _extraData);
uint256 localTokenTotalSupplyBefore = gem.totalSupply();
uint256 localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
mathint localTokenTotalSupplyBefore = gem.totalSupply();
mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
// ERC20 assumption
require localTokenTotalSupplyBefore >= localTokenBalanceOfSenderBefore;

Expand All @@ -213,8 +213,8 @@ rule bridgeERC20(address _localToken, address _remoteToken, uint256 _amount, uin
address lastTargetAfter = l2messenger.lastTarget();
bytes32 lastMessageHashAfter = l2messenger.lastMessageHash();
uint32 lastMinGasLimitAfter = l2messenger.lastMinGasLimit();
uint256 localTokenTotalSupplyAfter = gem.totalSupply();
uint256 localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
mathint localTokenTotalSupplyAfter = gem.totalSupply();
mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);

assert lastTargetAfter == otherBridge, "Assert 1";
assert lastMessageHashAfter == message, "Assert 2";
Expand All @@ -231,8 +231,8 @@ rule bridgeERC20_revert(address _localToken, address _remoteToken, uint256 _amou
address l1ToL2TokenRemoteToken = l1ToL2Token(_remoteToken);
mathint maxWithdrawsLocatOken = maxWithdraws(_localToken);

uint256 localTokenTotalSupply = gem.totalSupply();
uint256 localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
mathint localTokenTotalSupply = gem.totalSupply();
mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
// ERC20 assumption
require localTokenTotalSupply >= localTokenBalanceOfSender;
// User assumptions
Expand Down Expand Up @@ -260,8 +260,8 @@ rule bridgeERC20To(address _localToken, address _remoteToken, address _to, uint2
address otherBridge = otherBridge();

bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, _to, _amount, _extraData);
uint256 localTokenTotalSupplyBefore = gem.totalSupply();
uint256 localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
mathint localTokenTotalSupplyBefore = gem.totalSupply();
mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
// ERC20 assumption
require localTokenTotalSupplyBefore >= localTokenBalanceOfSenderBefore;

Expand All @@ -270,8 +270,8 @@ rule bridgeERC20To(address _localToken, address _remoteToken, address _to, uint2
address lastTargetAfter = l2messenger.lastTarget();
bytes32 lastMessageHashAfter = l2messenger.lastMessageHash();
uint32 lastMinGasLimitAfter = l2messenger.lastMinGasLimit();
uint256 localTokenTotalSupplyAfter = gem.totalSupply();
uint256 localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
mathint localTokenTotalSupplyAfter = gem.totalSupply();
mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);

assert lastTargetAfter == otherBridge, "Assert 1";
assert lastMessageHashAfter == message, "Assert 2";
Expand All @@ -288,8 +288,8 @@ rule bridgeERC20To_revert(address _localToken, address _remoteToken, address _to
address l1ToL2TokenRemoteToken = l1ToL2Token(_remoteToken);
mathint maxWithdrawsLocatOken = maxWithdraws(_localToken);

uint256 localTokenTotalSupply = gem.totalSupply();
uint256 localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
mathint localTokenTotalSupply = gem.totalSupply();
mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
// ERC20 assumption
require localTokenTotalSupply >= localTokenBalanceOfSender;
// User assumptions
Expand All @@ -313,15 +313,15 @@ rule finalizeBridgeERC20(address _localToken, address _remoteToken, address _fro

require _localToken == gem;

uint256 localTokenTotalSupplyBefore = gem.totalSupply();
uint256 localTokenBalanceOfToBefore = gem.balanceOf(_to);
mathint localTokenTotalSupplyBefore = gem.totalSupply();
mathint localTokenBalanceOfToBefore = gem.balanceOf(_to);
// ERC20 assumption
require localTokenTotalSupplyBefore >= localTokenBalanceOfToBefore;

finalizeBridgeERC20(e, _localToken, _remoteToken, _from, _to, _amount, _extraData);

uint256 localTokenTotalSupplyAfter = gem.totalSupply();
uint256 localTokenBalanceOfToAfter = gem.balanceOf(_to);
mathint localTokenTotalSupplyAfter = gem.totalSupply();
mathint localTokenBalanceOfToAfter = gem.balanceOf(_to);

assert localTokenTotalSupplyAfter == localTokenTotalSupplyBefore + _amount, "Assert 1";
assert localTokenBalanceOfToAfter == localTokenBalanceOfToBefore + _amount, "Assert 2";
Expand All @@ -337,8 +337,8 @@ rule finalizeBridgeERC20_revert(address _localToken, address _remoteToken, addre
address otherBridge = otherBridge();
address xDomainMessageSender = l2messenger.xDomainMessageSender();

uint256 localTokenTotalSupply = gem.totalSupply();
uint256 localTokenBalanceOfTo = gem.balanceOf(_to);
mathint localTokenTotalSupply = gem.totalSupply();
mathint localTokenBalanceOfTo = gem.balanceOf(_to);
// ERC20 assumption
require localTokenTotalSupply >= localTokenBalanceOfTo;
// Practical assumption
Expand Down

0 comments on commit e11132d

Please sign in to comment.