diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 0000000..d5a9e7f
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,48 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+ certora:
+ name: Certora
+ runs-on: ubuntu-latest
+ strategy:
+ fail-fast: false
+ matrix:
+ op-token-bridge:
+ - escrow
+ - l1-governance-relay
+ - l2-governance-relay
+ - l1-token-bridge
+ - l2-token-bridge
+
+ steps:
+ - name: Checkout
+ uses: actions/checkout@v3
+ with:
+ submodules: recursive
+
+ - uses: actions/setup-java@v2
+ with:
+ distribution: 'zulu'
+ java-version: '11'
+ java-package: jre
+
+ - name: Set up Python 3.8
+ uses: actions/setup-python@v3
+ with:
+ python-version: 3.8
+
+ - name: Install solc-select
+ run: pip3 install solc-select
+
+ - name: Solc Select 0.8.21
+ run: solc-select install 0.8.21
+
+ - name: Install Certora
+ run: pip3 install certora-cli-beta
+
+ - name: Verify ${{ matrix.op-token-bridge }}
+ run: make certora-${{ matrix.op-token-bridge }} results=1
+ env:
+ CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/.gitignore b/.gitignore
index 85198aa..8c30259 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,3 +12,6 @@ docs/
# Dotenv file
.env
+
+# Certora
+.certora_internal
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..792cdea
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,6 @@
+PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.8.21:$(PATH)
+certora-escrow :; PATH=${PATH} certoraRun certora/Escrow.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-l1-governance-relay :; PATH=${PATH} certoraRun certora/L1GovernanceRelay.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-l2-governance-relay :; PATH=${PATH} certoraRun certora/L2GovernanceRelay.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-l1-token-bridge :; PATH=${PATH} certoraRun certora/L1TokenBridge.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-l2-token-bridge :; PATH=${PATH} certoraRun certora/L2TokenBridge.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
diff --git a/certora/Escrow.conf b/certora/Escrow.conf
new file mode 100644
index 0000000..bfd8c9e
--- /dev/null
+++ b/certora/Escrow.conf
@@ -0,0 +1,14 @@
+{
+ "files": [
+ "src/Escrow.sol",
+ "test/mocks/GemMock.sol"
+ ],
+ "solc": "solc-0.8.21",
+ "solc_optimize": "200",
+ "verify": "Escrow:certora/Escrow.spec",
+ "rule_sanity": "basic",
+ "multi_assert_check": true,
+ "parametric_contracts": ["Escrow"],
+ "build_cache": true,
+ "msg": "Escrow"
+}
diff --git a/certora/Escrow.spec b/certora/Escrow.spec
new file mode 100644
index 0000000..8be9bd3
--- /dev/null
+++ b/certora/Escrow.spec
@@ -0,0 +1,121 @@
+// Escrow.spec
+
+using GemMock as gem;
+
+methods {
+ // storage variables
+ function wards(address) external returns (uint256) envfree;
+ //
+ function gem.allowance(address,address) external returns (uint256) envfree;
+ //
+ function _.approve(address,uint256) external => DISPATCHER(true);
+}
+
+// Verify that each storage layout is only modified in the corresponding functions
+rule storageAffected(method f) {
+ env e;
+
+ address anyAddr;
+
+ mathint wardsBefore = wards(anyAddr);
+
+ calldataarg args;
+ f(e, args);
+
+ mathint wardsAfter = wards(anyAddr);
+
+ assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1";
+}
+
+// Verify correct storage changes for non reverting rely
+rule rely(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ rely(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 1, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on rely
+rule rely_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ rely@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting deny
+rule deny(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ deny(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 0, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on deny
+rule deny_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ deny@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting approve
+rule approve(address token, address spender, uint256 value) {
+ env e;
+
+ require token == gem;
+
+ approve(e, token, spender, value);
+
+ mathint allowance = gem.allowance(currentContract, spender);
+
+ assert allowance == to_mathint(value), "Assert 1";
+}
+
+// Verify revert rules on approve
+rule approve_revert(address token, address spender, uint256 value) {
+ env e;
+
+ require token == gem;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ approve@withrevert(e, token, spender, value);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
diff --git a/certora/L1GovernanceRelay.conf b/certora/L1GovernanceRelay.conf
new file mode 100644
index 0000000..39e7b1f
--- /dev/null
+++ b/certora/L1GovernanceRelay.conf
@@ -0,0 +1,23 @@
+{
+ "files": [
+ "src/L1GovernanceRelay.sol",
+ "certora/harness/Auxiliar.sol",
+ "test/mocks/MessengerMock.sol",
+ ],
+ "solc": "solc-0.8.21",
+ "solc_optimize_map": {
+ "L1GovernanceRelay": "200",
+ "Auxiliar": "0",
+ "MessengerMock": "0"
+ },
+ "link": [
+ "L1GovernanceRelay:messenger=MessengerMock"
+ ],
+ "verify": "L1GovernanceRelay:certora/L1GovernanceRelay.spec",
+ "rule_sanity": "basic",
+ "multi_assert_check": true,
+ "parametric_contracts": ["L1GovernanceRelay"],
+ "build_cache": true,
+ "optimistic_hashing": true,
+ "msg": "L1GovernanceRelay"
+}
diff --git a/certora/L1GovernanceRelay.spec b/certora/L1GovernanceRelay.spec
new file mode 100644
index 0000000..968bb51
--- /dev/null
+++ b/certora/L1GovernanceRelay.spec
@@ -0,0 +1,132 @@
+// L1GovernanceRelay.spec
+
+using Auxiliar as aux;
+using MessengerMock as l1messenger;
+
+methods {
+ // storage variables
+ function wards(address) external returns (uint256) envfree;
+ // immutables
+ function l2GovernanceRelay() external returns (address) envfree;
+ function messenger() external returns (address) envfree;
+ //
+ function aux.getGovMessageHash(address,bytes) external returns (bytes32) envfree;
+ function l1messenger.lastTarget() external returns (address) envfree;
+ function l1messenger.lastMessageHash() external returns (bytes32) envfree;
+ function l1messenger.lastMinGasLimit() external returns (uint32) envfree;
+ //
+ function _.sendMessage(address,bytes,uint32) external => DISPATCHER(true);
+}
+
+// Verify that each storage layout is only modified in the corresponding functions
+rule storageAffected(method f) {
+ env e;
+
+ address anyAddr;
+
+ mathint wardsBefore = wards(anyAddr);
+
+ calldataarg args;
+ f(e, args);
+
+ mathint wardsAfter = wards(anyAddr);
+
+ assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1";
+}
+
+// Verify correct storage changes for non reverting rely
+rule rely(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ rely(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 1, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on rely
+rule rely_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ rely@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting deny
+rule deny(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ deny(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 0, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on deny
+rule deny_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ deny@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting relay
+rule relay(address target, bytes targetData, uint32 minGasLimit) {
+ env e;
+
+ address l2GovernanceRelay = l2GovernanceRelay();
+
+ bytes32 message = aux.getGovMessageHash(target, targetData);
+
+ relay(e, target, targetData, minGasLimit);
+
+ address lastTargetAfter = l1messenger.lastTarget();
+ bytes32 lastMessageHashAfter = l1messenger.lastMessageHash();
+ uint32 lastMinGasLimitAfter = l1messenger.lastMinGasLimit();
+
+ assert lastTargetAfter == l2GovernanceRelay, "Assert 1";
+ assert lastMessageHashAfter == message, "Assert 2";
+ assert lastMinGasLimitAfter == minGasLimit, "Assert 3";
+}
+
+// Verify revert rules on relay
+rule relay_revert(address target, bytes targetData, uint32 minGasLimit) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ relay@withrevert(e, target, targetData, minGasLimit);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
diff --git a/certora/L1TokenBridge.conf b/certora/L1TokenBridge.conf
new file mode 100644
index 0000000..d0cf7cb
--- /dev/null
+++ b/certora/L1TokenBridge.conf
@@ -0,0 +1,31 @@
+{
+ "files": [
+ "src/L1TokenBridge.sol",
+ "certora/harness/Auxiliar.sol",
+ "test/mocks/MessengerMock.sol",
+ "test/mocks/GemMock.sol",
+ "certora/harness/ImplementationMock.sol"
+ ],
+ "solc": "solc-0.8.21",
+ "solc_optimize_map": {
+ "L1TokenBridge": "200",
+ "Auxiliar": "0",
+ "MessengerMock": "0",
+ "GemMock": "0",
+ "ImplementationMock": "0"
+ },
+ "link": [
+ "L1TokenBridge:messenger=MessengerMock"
+ ],
+ "verify": "L1TokenBridge:certora/L1TokenBridge.spec",
+ "rule_sanity": "basic",
+ "multi_assert_check": true,
+ "parametric_contracts": ["L1TokenBridge"],
+ "build_cache": true,
+ "optimistic_hashing": true,
+ "hashing_length_bound": "512",
+ "prover_args": [
+ "-enableStorageSplitting false"
+ ],
+ "msg": "L1TokenBridge"
+}
diff --git a/certora/L1TokenBridge.spec b/certora/L1TokenBridge.spec
new file mode 100644
index 0000000..a69eb9a
--- /dev/null
+++ b/certora/L1TokenBridge.spec
@@ -0,0 +1,487 @@
+// L1TokenBridge.spec
+
+using Auxiliar as aux;
+using MessengerMock as l1messenger;
+using GemMock as gem;
+
+methods {
+ // storage variables
+ function wards(address) external returns (uint256) envfree;
+ function l1ToL2Token(address) external returns (address) envfree;
+ function isOpen() external returns (uint256) envfree;
+ function escrow() external returns (address) envfree;
+ // immutables
+ function otherBridge() external returns (address) envfree;
+ function messenger() external returns (address) envfree;
+ // getter
+ function getImplementation() external returns (address) envfree;
+ //
+ function gem.allowance(address,address) external returns (uint256) envfree;
+ function gem.totalSupply() external returns (uint256) envfree;
+ function gem.balanceOf(address) external returns (uint256) envfree;
+ function aux.getBridgeMessageHash(address,address,address,address,uint256,bytes) external returns (bytes32) envfree;
+ function l1messenger.xDomainMessageSender() external returns (address) envfree;
+ function l1messenger.lastTarget() external returns (address) envfree;
+ function l1messenger.lastMessageHash() external returns (bytes32) envfree;
+ function l1messenger.lastMinGasLimit() external returns (uint32) envfree;
+ //
+ function _.proxiableUUID() external => DISPATCHER(true);
+ function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
+}
+
+definition INITIALIZABLE_STORAGE() returns uint256 = 0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00;
+definition IMPLEMENTATION_SLOT() returns uint256 = 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc;
+
+persistent ghost bool firstRead;
+persistent ghost mathint initializedBefore;
+persistent ghost bool initializingBefore;
+persistent ghost mathint initializedAfter;
+persistent ghost bool initializingAfter;
+hook ALL_SLOAD(uint256 slot) uint256 val {
+ if (slot == INITIALIZABLE_STORAGE() && firstRead) {
+ firstRead = false;
+ initializedBefore = val % (max_uint64 + 1);
+ initializingBefore = (val / 2^64) % (max_uint8 + 1) != 0;
+ } else if (slot == INITIALIZABLE_STORAGE()) {
+ initializedAfter = val % (max_uint64 + 1);
+ initializingAfter = (val / 2^64) % (max_uint8 + 1) != 0;
+ }
+}
+hook ALL_SSTORE(uint256 slot, uint256 val) {
+ if (slot == INITIALIZABLE_STORAGE()) {
+ initializedAfter = val % (max_uint64 + 1);
+ initializingAfter = (val / 2^64) % (max_uint8 + 1) != 0;
+ }
+}
+
+// Verify no more entry points exist
+rule entryPoints(method f) filtered { f -> !f.isView } {
+ env e;
+
+ calldataarg args;
+ f(e, args);
+
+ assert f.selector == sig:initialize().selector ||
+ f.selector == sig:upgradeToAndCall(address,bytes).selector ||
+ f.selector == sig:rely(address).selector ||
+ f.selector == sig:deny(address).selector ||
+ f.selector == sig:file(bytes32,address).selector ||
+ f.selector == sig:close().selector ||
+ f.selector == sig:registerToken(address,address).selector ||
+ f.selector == sig:bridgeERC20(address,address,uint256,uint32,bytes).selector ||
+ f.selector == sig:bridgeERC20To(address,address,address,uint256,uint32,bytes).selector ||
+ f.selector == sig:finalizeBridgeERC20(address,address,address,address,uint256,bytes).selector;
+}
+
+// Verify that each storage layout is only modified in the corresponding functions
+rule storageAffected(method f) filtered { f -> f.selector != sig:upgradeToAndCall(address, bytes).selector } {
+ env e;
+
+ address anyAddr;
+
+ initializedAfter = initializedBefore;
+
+ mathint wardsBefore = wards(anyAddr);
+ address l1ToL2TokenBefore = l1ToL2Token(anyAddr);
+ mathint isOpenBefore = isOpen();
+ address escrowBefore = escrow();
+
+ calldataarg args;
+ f(e, args);
+
+ mathint wardsAfter = wards(anyAddr);
+ address l1ToL2TokenAfter = l1ToL2Token(anyAddr);
+ mathint isOpenAfter = isOpen();
+ address escrowAfter = escrow();
+
+ assert initializedAfter != initializedBefore => f.selector == sig:initialize().selector, "Assert 1";
+ assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector || f.selector == sig:initialize().selector, "Assert 2";
+ assert l1ToL2TokenAfter != l1ToL2TokenBefore => f.selector == sig:registerToken(address,address).selector, "Assert 3";
+ assert isOpenAfter != isOpenBefore => f.selector == sig:close().selector || f.selector == sig:initialize().selector, "Assert 4";
+ assert escrowAfter != escrowBefore => f.selector == sig:file(bytes32,address).selector, "Assert 5";
+}
+
+// Verify correct storage changes for non reverting initialize
+rule initialize() {
+ env e;
+
+ address other;
+ require other != e.msg.sender;
+
+ mathint wardsOtherBefore = wards(other);
+
+ initialize(e);
+
+ mathint wardsSenderAfter = wards(e.msg.sender);
+ mathint wardsOtherAfter = wards(other);
+ mathint isOpenAfter = isOpen();
+
+ assert initializedAfter == 1, "Assert 1";
+ assert !initializingAfter, "Assert 2";
+ assert wardsSenderAfter == 1, "Assert 3";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 4";
+ assert isOpenAfter == 1, "Assert 5";
+}
+
+// Verify revert rules on initialize
+rule initialize_revert() {
+ env e;
+
+ firstRead = true;
+ mathint bridgeCodeSize = nativeCodesize[currentContract]; // This should actually be always > 0
+
+ initialize@withrevert(e);
+
+ bool initialSetup = initializedBefore == 0 && !initializingBefore;
+ bool construction = initializedBefore == 1 && bridgeCodeSize == 0;
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = !initialSetup && !construction;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting initialize
+rule upgradeToAndCall(address newImplementation, bytes data) {
+ env e;
+
+ require data.length == 0; // Avoid evaluating the delegatecCall part
+
+ upgradeToAndCall(e, newImplementation, data);
+
+ address implementationAfter = getImplementation();
+
+ assert implementationAfter == newImplementation, "Assert 1";
+}
+
+// Verify revert rules on upgradeToAndCall
+rule upgradeToAndCall_revert(address newImplementation, bytes data) {
+ env e;
+
+ require data.length == 0; // Avoid evaluating the delegatecCall part
+
+ address self = currentContract.__self;
+ address implementation = getImplementation();
+ mathint wardsSender = wards(e.msg.sender);
+ bytes32 newImplementationProxiableUUID = newImplementation.proxiableUUID(e);
+
+ upgradeToAndCall@withrevert(e, newImplementation, data);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = self == currentContract || implementation != self;
+ bool revert3 = wardsSender != 1;
+ bool revert4 = newImplementationProxiableUUID != to_bytes32(IMPLEMENTATION_SLOT());
+
+ assert lastReverted <=> revert1 || revert2 || revert3 ||
+ revert4, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting rely
+rule rely(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ rely(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 1, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on rely
+rule rely_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ rely@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting deny
+rule deny(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ deny(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 0, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on deny
+rule deny_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ deny@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting file
+rule file(bytes32 what, address data) {
+ env e;
+
+ file(e, what, data);
+
+ address escrowAfter = escrow();
+
+ assert escrowAfter == data, "Assert 1";
+}
+
+// Verify revert rules on file
+rule file_revert(bytes32 what, address data) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ file@withrevert(e, what, data);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+ bool revert3 = what != to_bytes32(0x657363726f770000000000000000000000000000000000000000000000000000);
+
+ assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting close
+rule close() {
+ env e;
+
+ close(e);
+
+ mathint isOpenAfter = isOpen();
+
+ assert isOpenAfter == 0, "Assert 1";
+}
+
+// Verify revert rules on close
+rule close_revert() {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ close@withrevert(e);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting registerToken
+rule registerToken(address l1Token, address l2Token) {
+ env e;
+
+ registerToken(e, l1Token, l2Token);
+
+ address l1ToL2TokenAfter = l1ToL2Token(l1Token);
+
+ assert l1ToL2TokenAfter == l2Token, "Assert 1";
+}
+
+// Verify revert rules on registerToken
+rule registerToken_revert(address l1Token, address l2Token) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ registerToken@withrevert(e, l1Token, l2Token);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting bridgeERC20
+rule bridgeERC20(address _localToken, address _remoteToken, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ address otherBridge = otherBridge();
+ address escrow = escrow();
+ require e.msg.sender != escrow;
+
+ bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, e.msg.sender, _amount, _extraData);
+ mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
+ mathint localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
+ // ERC20 assumption
+ require gem.totalSupply() >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;
+
+ bridgeERC20(e, _localToken, _remoteToken, _amount, _minGasLimit, _extraData);
+
+ address lastTargetAfter = l1messenger.lastTarget();
+ bytes32 lastMessageHashAfter = l1messenger.lastMessageHash();
+ uint32 lastMinGasLimitAfter = l1messenger.lastMinGasLimit();
+ mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
+ mathint localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);
+
+ assert lastTargetAfter == otherBridge, "Assert 1";
+ assert lastMessageHashAfter == message, "Assert 2";
+ assert lastMinGasLimitAfter == _minGasLimit, "Assert 3";
+ assert localTokenBalanceOfSenderAfter == localTokenBalanceOfSenderBefore - _amount, "Assert 4";
+ assert localTokenBalanceOfEscrowAfter == localTokenBalanceOfEscrowBefore + _amount, "Assert 5";
+}
+
+// Verify revert rules on bridgeERC20
+rule bridgeERC20_revert(address _localToken, address _remoteToken, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ mathint isOpen = isOpen();
+ address l1ToL2TokenLocalToken = l1ToL2Token(_localToken);
+
+ address escrow = escrow();
+
+ mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
+ mathint localTokenBalanceOfEscrow = gem.balanceOf(escrow);
+
+ // ERC20 assumption
+ require gem.totalSupply() >= localTokenBalanceOfSender + localTokenBalanceOfEscrow;
+ // User assumptions
+ require localTokenBalanceOfSender >= _amount;
+ require gem.allowance(e.msg.sender, currentContract) >= _amount;
+
+ bridgeERC20@withrevert(e, _localToken, _remoteToken, _amount, _minGasLimit, _extraData);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = nativeCodesize[e.msg.sender] != 0;
+ bool revert3 = isOpen != 1;
+ bool revert4 = _remoteToken == 0 || l1ToL2TokenLocalToken != _remoteToken;
+
+ assert lastReverted <=> revert1 || revert2 || revert3 ||
+ revert4, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting bridgeERC20To
+rule bridgeERC20To(address _localToken, address _remoteToken, address _to, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ address otherBridge = otherBridge();
+ address escrow = escrow();
+ require e.msg.sender != escrow;
+
+ bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, _to, _amount, _extraData);
+ mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
+ mathint localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
+ // ERC20 assumption
+ require gem.totalSupply() >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;
+
+ bridgeERC20To(e, _localToken, _remoteToken, _to, _amount, _minGasLimit, _extraData);
+
+ address lastTargetAfter = l1messenger.lastTarget();
+ bytes32 lastMessageHashAfter = l1messenger.lastMessageHash();
+ uint32 lastMinGasLimitAfter = l1messenger.lastMinGasLimit();
+ mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
+ mathint localTokenBalanceOfEscrowAfter = gem.balanceOf(escrow);
+
+ assert lastTargetAfter == otherBridge, "Assert 1";
+ assert lastMessageHashAfter == message, "Assert 2";
+ assert lastMinGasLimitAfter == _minGasLimit, "Assert 3";
+ assert localTokenBalanceOfSenderAfter == localTokenBalanceOfSenderBefore - _amount, "Assert 4";
+ assert localTokenBalanceOfEscrowAfter == localTokenBalanceOfEscrowBefore + _amount, "Assert 5";
+}
+
+// Verify revert rules on bridgeERC20To
+rule bridgeERC20To_revert(address _localToken, address _remoteToken, address _to, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ mathint isOpen = isOpen();
+ address l1ToL2TokenLocalToken = l1ToL2Token(_localToken);
+
+ address escrow = escrow();
+
+ mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
+ mathint localTokenBalanceOfEscrow = gem.balanceOf(escrow);
+
+ // ERC20 assumption
+ require gem.totalSupply() >= localTokenBalanceOfSender + localTokenBalanceOfEscrow;
+ // User assumptions
+ require localTokenBalanceOfSender >= _amount;
+ require gem.allowance(e.msg.sender, currentContract) >= _amount;
+
+ bridgeERC20To@withrevert(e, _localToken, _remoteToken, _to, _amount, _minGasLimit, _extraData);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = isOpen != 1;
+ bool revert3 = _remoteToken == 0 || l1ToL2TokenLocalToken != _remoteToken;
+
+ assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting finalizeBridgeERC20
+rule finalizeBridgeERC20(address _localToken, address _remoteToken, address _from, address _to, uint256 _amount, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ address escrow = escrow();
+
+ 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);
+
+ 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";
+ assert escrow == _to => localTokenBalanceOfEscrowAfter == localTokenBalanceOfEscrowBefore, "Assert 3";
+}
+
+// Verify revert rules on finalizeBridgeERC20
+rule finalizeBridgeERC20_revert(address _localToken, address _remoteToken, address _from, address _to, uint256 _amount, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ address messenger = messenger();
+ address otherBridge = otherBridge();
+ address xDomainMessageSender = l1messenger.xDomainMessageSender();
+ address escrow = escrow();
+
+ mathint localTokenBalanceOfEscrow = gem.balanceOf(escrow);
+
+ // ERC20 assumption
+ require gem.totalSupply() >= localTokenBalanceOfEscrow + gem.balanceOf(_to);
+ // Bridge assumption
+ require localTokenBalanceOfEscrow >= _amount;
+ // Set up assumption
+ require gem.allowance(escrow, currentContract) == max_uint256;
+
+ finalizeBridgeERC20@withrevert(e, _localToken, _remoteToken, _from, _to, _amount, _extraData);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = e.msg.sender != messenger || xDomainMessageSender != otherBridge;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
diff --git a/certora/L2GovernanceRelay.conf b/certora/L2GovernanceRelay.conf
new file mode 100644
index 0000000..fa08736
--- /dev/null
+++ b/certora/L2GovernanceRelay.conf
@@ -0,0 +1,21 @@
+{
+ "files": [
+ "src/L2GovernanceRelay.sol",
+ "test/mocks/MessengerMock.sol",
+ ],
+ "solc": "solc-0.8.21",
+ "solc_optimize_map": {
+ "L2GovernanceRelay": "200",
+ "MessengerMock": "0"
+ },
+ "link": [
+ "L2GovernanceRelay:messenger=MessengerMock"
+ ],
+ "verify": "L2GovernanceRelay:certora/L2GovernanceRelay.spec",
+ "rule_sanity": "basic",
+ "multi_assert_check": true,
+ "parametric_contracts": ["L2GovernanceRelay"],
+ "build_cache": true,
+ "optimistic_hashing": true,
+ "msg": "L2GovernanceRelay"
+}
diff --git a/certora/L2GovernanceRelay.spec b/certora/L2GovernanceRelay.spec
new file mode 100644
index 0000000..725971d
--- /dev/null
+++ b/certora/L2GovernanceRelay.spec
@@ -0,0 +1,51 @@
+// L2GovernanceRelay.spec
+
+using MessengerMock as l2messenger;
+
+methods {
+ // immutables
+ function l1GovernanceRelay() external returns (address) envfree;
+ function messenger() external returns (address) envfree;
+ //
+ function l2messenger.xDomainMessageSender() external returns (address) envfree;
+}
+
+persistent ghost bool called;
+persistent ghost address calledAddr;
+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;
+ calledAddr = addr;
+ dataLength = argsLength;
+ success = rc != 0;
+}
+
+// Verify correct storage changes for non reverting relay
+rule relay(address target, bytes targetData) {
+ env e;
+
+ relay(e, target, targetData);
+
+ assert called, "Assert 1";
+ assert calledAddr == target, "Assert 2";
+ assert dataLength == targetData.length, "Assert 3";
+ assert success, "Assert 4";
+}
+
+// Verify revert rules on relay
+rule relay_revert(address target, bytes targetData) {
+ env e;
+
+ address l1GovernanceRelay = l1GovernanceRelay();
+ address messenger = messenger();
+ address xDomainMessageSender = l2messenger.xDomainMessageSender();
+
+ relay@withrevert(e, target, targetData);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = e.msg.sender != messenger || xDomainMessageSender != l1GovernanceRelay;
+ bool revert3 = !success;
+
+ assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
+}
diff --git a/certora/L2TokenBridge.conf b/certora/L2TokenBridge.conf
new file mode 100644
index 0000000..f0db0b9
--- /dev/null
+++ b/certora/L2TokenBridge.conf
@@ -0,0 +1,31 @@
+{
+ "files": [
+ "src/L2TokenBridge.sol",
+ "certora/harness/Auxiliar.sol",
+ "test/mocks/MessengerMock.sol",
+ "test/mocks/GemMock.sol",
+ "certora/harness/ImplementationMock.sol"
+ ],
+ "solc": "solc-0.8.21",
+ "solc_optimize_map": {
+ "L2TokenBridge": "200",
+ "Auxiliar": "0",
+ "MessengerMock": "0",
+ "GemMock": "0",
+ "ImplementationMock": "0"
+ },
+ "link": [
+ "L2TokenBridge:messenger=MessengerMock"
+ ],
+ "verify": "L2TokenBridge:certora/L2TokenBridge.spec",
+ "rule_sanity": "basic",
+ "multi_assert_check": true,
+ "parametric_contracts": ["L2TokenBridge"],
+ "build_cache": true,
+ "optimistic_hashing": true,
+ "hashing_length_bound": "512",
+ "prover_args": [
+ "-enableStorageSplitting false"
+ ],
+ "msg": "L2TokenBridge"
+}
diff --git a/certora/L2TokenBridge.spec b/certora/L2TokenBridge.spec
new file mode 100644
index 0000000..5d6eb93
--- /dev/null
+++ b/certora/L2TokenBridge.spec
@@ -0,0 +1,478 @@
+// L2TokenBridge.spec
+
+using Auxiliar as aux;
+using MessengerMock as l2messenger;
+using GemMock as gem;
+
+methods {
+ // storage variables
+ function wards(address) external returns (uint256) envfree;
+ function l1ToL2Token(address) external returns (address) envfree;
+ function maxWithdraws(address) external returns (uint256) envfree;
+ function isOpen() external returns (uint256) envfree;
+ // immutables
+ function otherBridge() external returns (address) envfree;
+ function messenger() external returns (address) envfree;
+ // getter
+ function getImplementation() external returns (address) envfree;
+ //
+ function gem.wards(address) external returns (uint256) envfree;
+ function gem.allowance(address,address) external returns (uint256) envfree;
+ function gem.totalSupply() external returns (uint256) envfree;
+ function gem.balanceOf(address) external returns (uint256) envfree;
+ function aux.getBridgeMessageHash(address,address,address,address,uint256,bytes) external returns (bytes32) envfree;
+ function l2messenger.xDomainMessageSender() external returns (address) envfree;
+ function l2messenger.lastTarget() external returns (address) envfree;
+ function l2messenger.lastMessageHash() external returns (bytes32) envfree;
+ function l2messenger.lastMinGasLimit() external returns (uint32) envfree;
+ //
+ function _.proxiableUUID() external => DISPATCHER(true);
+ function _.burn(address,uint256) external => DISPATCHER(true);
+ function _.mint(address,uint256) external => DISPATCHER(true);
+}
+
+definition INITIALIZABLE_STORAGE() returns uint256 = 0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00;
+definition IMPLEMENTATION_SLOT() returns uint256 = 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc;
+
+persistent ghost bool firstRead;
+persistent ghost mathint initializedBefore;
+persistent ghost bool initializingBefore;
+persistent ghost mathint initializedAfter;
+persistent ghost bool initializingAfter;
+hook ALL_SLOAD(uint256 slot) uint256 val {
+ if (slot == INITIALIZABLE_STORAGE() && firstRead) {
+ firstRead = false;
+ initializedBefore = val % (max_uint64 + 1);
+ initializingBefore = (val / 2^64) % (max_uint8 + 1) != 0;
+ } else if (slot == INITIALIZABLE_STORAGE()) {
+ initializedAfter = val % (max_uint64 + 1);
+ initializingAfter = (val / 2^64) % (max_uint8 + 1) != 0;
+ }
+}
+hook ALL_SSTORE(uint256 slot, uint256 val) {
+ if (slot == INITIALIZABLE_STORAGE()) {
+ initializedAfter = val % (max_uint64 + 1);
+ initializingAfter = (val / 2^64) % (max_uint8 + 1) != 0;
+ }
+}
+
+// Verify no more entry points exist
+rule entryPoints(method f) filtered { f -> !f.isView } {
+ env e;
+
+ calldataarg args;
+ f(e, args);
+
+ assert f.selector == sig:initialize().selector ||
+ f.selector == sig:upgradeToAndCall(address,bytes).selector ||
+ f.selector == sig:rely(address).selector ||
+ f.selector == sig:deny(address).selector ||
+ f.selector == sig:close().selector ||
+ f.selector == sig:registerToken(address,address).selector ||
+ f.selector == sig:setMaxWithdraw(address,uint256).selector ||
+ f.selector == sig:bridgeERC20(address,address,uint256,uint32,bytes).selector ||
+ f.selector == sig:bridgeERC20To(address,address,address,uint256,uint32,bytes).selector ||
+ f.selector == sig:finalizeBridgeERC20(address,address,address,address,uint256,bytes).selector;
+}
+
+// Verify that each storage layout is only modified in the corresponding functions
+rule storageAffected(method f) filtered { f -> f.selector != sig:upgradeToAndCall(address, bytes).selector } {
+ env e;
+
+ address anyAddr;
+
+ initializedAfter = initializedBefore;
+
+ mathint wardsBefore = wards(anyAddr);
+ address l1ToL2TokenBefore = l1ToL2Token(anyAddr);
+ mathint maxWithdrawsBefore = maxWithdraws(anyAddr);
+ mathint isOpenBefore = isOpen();
+
+ calldataarg args;
+ f(e, args);
+
+ mathint wardsAfter = wards(anyAddr);
+ address l1ToL2TokenAfter = l1ToL2Token(anyAddr);
+ mathint maxWithdrawsAfter = maxWithdraws(anyAddr);
+ mathint isOpenAfter = isOpen();
+
+ assert initializedAfter != initializedBefore => f.selector == sig:initialize().selector, "Assert 1";
+ assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector || f.selector == sig:initialize().selector, "Assert 2";
+ assert l1ToL2TokenAfter != l1ToL2TokenBefore => f.selector == sig:registerToken(address,address).selector, "Assert 3";
+ assert maxWithdrawsAfter != maxWithdrawsBefore => f.selector == sig:setMaxWithdraw(address,uint256).selector, "Assert 4";
+ assert isOpenAfter != isOpenBefore => f.selector == sig:close().selector || f.selector == sig:initialize().selector, "Assert 5";
+}
+
+// Verify correct storage changes for non reverting initialize
+rule initialize() {
+ env e;
+
+ address other;
+ require other != e.msg.sender;
+
+ mathint wardsOtherBefore = wards(other);
+
+ initialize(e);
+
+ mathint wardsSenderAfter = wards(e.msg.sender);
+ mathint wardsOtherAfter = wards(other);
+ mathint isOpenAfter = isOpen();
+
+ assert initializedAfter == 1, "Assert 1";
+ assert !initializingAfter, "Assert 2";
+ assert wardsSenderAfter == 1, "Assert 3";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 4";
+ assert isOpenAfter == 1, "Assert 5";
+}
+
+// Verify revert rules on initialize
+rule initialize_revert() {
+ env e;
+
+ firstRead = true;
+ mathint bridgeCodeSize = nativeCodesize[currentContract]; // This should actually be always > 0
+
+ initialize@withrevert(e);
+
+ bool initialSetup = initializedBefore == 0 && !initializingBefore;
+ bool construction = initializedBefore == 1 && bridgeCodeSize == 0;
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = !initialSetup && !construction;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting initialize
+rule upgradeToAndCall(address newImplementation, bytes data) {
+ env e;
+
+ require data.length == 0; // Avoid evaluating the delegatecCall part
+
+ upgradeToAndCall(e, newImplementation, data);
+
+ address implementationAfter = getImplementation();
+
+ assert implementationAfter == newImplementation, "Assert 1";
+}
+
+// Verify revert rules on upgradeToAndCall
+rule upgradeToAndCall_revert(address newImplementation, bytes data) {
+ env e;
+
+ require data.length == 0; // Avoid evaluating the delegatecCall part
+
+ address self = currentContract.__self;
+ address implementation = getImplementation();
+ mathint wardsSender = wards(e.msg.sender);
+ bytes32 newImplementationProxiableUUID = newImplementation.proxiableUUID(e);
+
+ upgradeToAndCall@withrevert(e, newImplementation, data);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = self == currentContract || implementation != self;
+ bool revert3 = wardsSender != 1;
+ bool revert4 = newImplementationProxiableUUID != to_bytes32(IMPLEMENTATION_SLOT());
+
+ assert lastReverted <=> revert1 || revert2 || revert3 ||
+ revert4, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting rely
+rule rely(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ rely(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 1, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on rely
+rule rely_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ rely@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting deny
+rule deny(address usr) {
+ env e;
+
+ address other;
+ require other != usr;
+
+ mathint wardsOtherBefore = wards(other);
+
+ deny(e, usr);
+
+ mathint wardsUsrAfter = wards(usr);
+ mathint wardsOtherAfter = wards(other);
+
+ assert wardsUsrAfter == 0, "Assert 1";
+ assert wardsOtherAfter == wardsOtherBefore, "Assert 2";
+}
+
+// Verify revert rules on deny
+rule deny_revert(address usr) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ deny@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting close
+rule close() {
+ env e;
+
+ close(e);
+
+ mathint isOpenAfter = isOpen();
+
+ assert isOpenAfter == 0, "Assert 1";
+}
+
+// Verify revert rules on close
+rule close_revert() {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ close@withrevert(e);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting registerToken
+rule registerToken(address l1Token, address l2Token) {
+ env e;
+
+ registerToken(e, l1Token, l2Token);
+
+ address l1ToL2TokenAfter = l1ToL2Token(l1Token);
+
+ assert l1ToL2TokenAfter == l2Token, "Assert 1";
+}
+
+// Verify revert rules on registerToken
+rule registerToken_revert(address l1Token, address l2Token) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ registerToken@withrevert(e, l1Token, l2Token);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting setMaxWithdraw
+rule setMaxWithdraw(address l2Token, uint256 maxWithdraw) {
+ env e;
+
+ setMaxWithdraw(e, l2Token, maxWithdraw);
+
+ mathint maxWithdrawsAfter = maxWithdraws(l2Token);
+
+ assert maxWithdrawsAfter == maxWithdraw, "Assert 1";
+}
+
+// Verify revert rules on setMaxWithdraw
+rule setMaxWithdraw_revert(address l2Token, uint256 maxWithdraw) {
+ env e;
+
+ mathint wardsSender = wards(e.msg.sender);
+
+ setMaxWithdraw@withrevert(e, l2Token, maxWithdraw);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = wardsSender != 1;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting bridgeERC20
+rule bridgeERC20(address _localToken, address _remoteToken, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ address otherBridge = otherBridge();
+
+ bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, e.msg.sender, _amount, _extraData);
+ mathint localTokenTotalSupplyBefore = gem.totalSupply();
+ mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
+ // ERC20 assumption
+ require localTokenTotalSupplyBefore >= localTokenBalanceOfSenderBefore;
+
+ bridgeERC20(e, _localToken, _remoteToken, _amount, _minGasLimit, _extraData);
+
+ address lastTargetAfter = l2messenger.lastTarget();
+ bytes32 lastMessageHashAfter = l2messenger.lastMessageHash();
+ uint32 lastMinGasLimitAfter = l2messenger.lastMinGasLimit();
+ mathint localTokenTotalSupplyAfter = gem.totalSupply();
+ mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
+
+ assert lastTargetAfter == otherBridge, "Assert 1";
+ assert lastMessageHashAfter == message, "Assert 2";
+ assert lastMinGasLimitAfter == _minGasLimit, "Assert 3";
+ assert localTokenTotalSupplyAfter == localTokenTotalSupplyBefore - _amount, "Assert 4";
+ assert localTokenBalanceOfSenderAfter == localTokenBalanceOfSenderBefore - _amount, "Assert 5";
+}
+
+// Verify revert rules on bridgeERC20
+rule bridgeERC20_revert(address _localToken, address _remoteToken, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ mathint isOpen = isOpen();
+ address l1ToL2TokenRemoteToken = l1ToL2Token(_remoteToken);
+ mathint maxWithdrawsLocatOken = maxWithdraws(_localToken);
+
+ mathint localTokenTotalSupply = gem.totalSupply();
+ mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
+ // ERC20 assumption
+ require localTokenTotalSupply >= localTokenBalanceOfSender;
+ // User assumptions
+ require localTokenBalanceOfSender >= _amount;
+ require gem.allowance(e.msg.sender, currentContract) >= _amount;
+
+ bridgeERC20@withrevert(e, _localToken, _remoteToken, _amount, _minGasLimit, _extraData);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = nativeCodesize[e.msg.sender] != 0;
+ bool revert3 = isOpen != 1;
+ bool revert4 = _localToken == 0 || l1ToL2TokenRemoteToken != _localToken;
+ bool revert5 = _amount > maxWithdrawsLocatOken;
+
+ assert lastReverted <=> revert1 || revert2 || revert3 ||
+ revert4 || revert5, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting bridgeERC20To
+rule bridgeERC20To(address _localToken, address _remoteToken, address _to, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ address otherBridge = otherBridge();
+
+ bytes32 message = aux.getBridgeMessageHash(_localToken, _remoteToken, e.msg.sender, _to, _amount, _extraData);
+ mathint localTokenTotalSupplyBefore = gem.totalSupply();
+ mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
+ // ERC20 assumption
+ require localTokenTotalSupplyBefore >= localTokenBalanceOfSenderBefore;
+
+ bridgeERC20To(e, _localToken, _remoteToken, _to, _amount, _minGasLimit, _extraData);
+
+ address lastTargetAfter = l2messenger.lastTarget();
+ bytes32 lastMessageHashAfter = l2messenger.lastMessageHash();
+ uint32 lastMinGasLimitAfter = l2messenger.lastMinGasLimit();
+ mathint localTokenTotalSupplyAfter = gem.totalSupply();
+ mathint localTokenBalanceOfSenderAfter = gem.balanceOf(e.msg.sender);
+
+ assert lastTargetAfter == otherBridge, "Assert 1";
+ assert lastMessageHashAfter == message, "Assert 2";
+ assert lastMinGasLimitAfter == _minGasLimit, "Assert 3";
+ assert localTokenTotalSupplyAfter == localTokenTotalSupplyBefore - _amount, "Assert 4";
+ assert localTokenBalanceOfSenderAfter == localTokenBalanceOfSenderBefore - _amount, "Assert 5";
+}
+
+// Verify revert rules on bridgeERC20To
+rule bridgeERC20To_revert(address _localToken, address _remoteToken, address _to, uint256 _amount, uint32 _minGasLimit, bytes _extraData) {
+ env e;
+
+ mathint isOpen = isOpen();
+ address l1ToL2TokenRemoteToken = l1ToL2Token(_remoteToken);
+ mathint maxWithdrawsLocatOken = maxWithdraws(_localToken);
+
+ mathint localTokenTotalSupply = gem.totalSupply();
+ mathint localTokenBalanceOfSender = gem.balanceOf(e.msg.sender);
+ // ERC20 assumption
+ require localTokenTotalSupply >= localTokenBalanceOfSender;
+ // User assumptions
+ require localTokenBalanceOfSender >= _amount;
+ require gem.allowance(e.msg.sender, currentContract) >= _amount;
+
+ bridgeERC20To@withrevert(e, _localToken, _remoteToken, _to, _amount, _minGasLimit, _extraData);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = isOpen != 1;
+ bool revert3 = _localToken == 0 || l1ToL2TokenRemoteToken != _localToken;
+ bool revert4 = _amount > maxWithdrawsLocatOken;
+
+ assert lastReverted <=> revert1 || revert2 || revert3 ||
+ revert4, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting finalizeBridgeERC20
+rule finalizeBridgeERC20(address _localToken, address _remoteToken, address _from, address _to, uint256 _amount, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ mathint localTokenTotalSupplyBefore = gem.totalSupply();
+ mathint localTokenBalanceOfToBefore = gem.balanceOf(_to);
+ // ERC20 assumption
+ require localTokenTotalSupplyBefore >= localTokenBalanceOfToBefore;
+
+ finalizeBridgeERC20(e, _localToken, _remoteToken, _from, _to, _amount, _extraData);
+
+ mathint localTokenTotalSupplyAfter = gem.totalSupply();
+ mathint localTokenBalanceOfToAfter = gem.balanceOf(_to);
+
+ assert localTokenTotalSupplyAfter == localTokenTotalSupplyBefore + _amount, "Assert 1";
+ assert localTokenBalanceOfToAfter == localTokenBalanceOfToBefore + _amount, "Assert 2";
+}
+
+// Verify revert rules on finalizeBridgeERC20
+rule finalizeBridgeERC20_revert(address _localToken, address _remoteToken, address _from, address _to, uint256 _amount, bytes _extraData) {
+ env e;
+
+ require _localToken == gem;
+
+ address messenger = messenger();
+ address otherBridge = otherBridge();
+ address xDomainMessageSender = l2messenger.xDomainMessageSender();
+
+ mathint localTokenTotalSupply = gem.totalSupply();
+ mathint localTokenBalanceOfTo = gem.balanceOf(_to);
+ // ERC20 assumption
+ require localTokenTotalSupply >= localTokenBalanceOfTo;
+ // Practical assumption
+ require localTokenTotalSupply + _amount <= max_uint256;
+ // Set up assumption
+ require gem.wards(currentContract) == 1;
+
+ finalizeBridgeERC20@withrevert(e, _localToken, _remoteToken, _from, _to, _amount, _extraData);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = e.msg.sender != messenger || xDomainMessageSender != otherBridge;
+
+ assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
diff --git a/certora/harness/Auxiliar.sol b/certora/harness/Auxiliar.sol
new file mode 100644
index 0000000..03ca10d
--- /dev/null
+++ b/certora/harness/Auxiliar.sol
@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+pragma solidity ^0.8.21;
+
+interface GovernanceRelayLike {
+ function relay(address, bytes calldata) external;
+}
+
+interface BridgeLike {
+ function finalizeBridgeERC20(address, address, address, address, uint256, bytes calldata) external;
+}
+
+contract Auxiliar {
+ function getGovMessageHash(address target, bytes calldata targetData) public pure returns (bytes32) {
+ return keccak256(abi.encodeCall(GovernanceRelayLike.relay, (target, targetData)));
+ }
+
+ function getBridgeMessageHash(address token1, address token2, address sender, address to, uint256 amount, bytes calldata extraData) public pure returns (bytes32) {
+ return keccak256(abi.encodeCall(BridgeLike.finalizeBridgeERC20, (
+ token1,
+ token2,
+ sender,
+ to,
+ amount,
+ extraData
+ )));
+ }
+}
diff --git a/certora/harness/ImplementationMock.sol b/certora/harness/ImplementationMock.sol
new file mode 100644
index 0000000..ec2e28d
--- /dev/null
+++ b/certora/harness/ImplementationMock.sol
@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+pragma solidity ^0.8.21;
+
+contract ImplementationMock {
+ bytes32 public proxiableUUID;
+}
diff --git a/test/mocks/MessengerMock.sol b/test/mocks/MessengerMock.sol
index e744690..9a11ef0 100644
--- a/test/mocks/MessengerMock.sol
+++ b/test/mocks/MessengerMock.sol
@@ -1,24 +1,12 @@
// SPDX-License-Identifier: AGPL-3.0-or-later
-// Copyright (C) 2024 Dai Foundation
-//
-// This program is free software: you can redistribute it and/or modify
-// it under the terms of the GNU Affero General Public License as published by
-// the Free Software Foundation, either version 3 of the License, or
-// (at your option) any later version.
-//
-// This program is distributed in the hope that it will be useful,
-// but WITHOUT ANY WARRANTY; without even the implied warranty of
-// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-// GNU Affero General Public License for more details.
-//
-// You should have received a copy of the GNU Affero General Public License
-// along with this program. If not, see <https://www.gnu.org/licenses/>.
-
pragma solidity ^0.8.21;
contract MessengerMock {
address public xDomainMessageSender;
+ address public lastTarget;
+ bytes32 public lastMessageHash;
+ uint32 public lastMinGasLimit;
event SentMessage(address indexed target, address sender, bytes message, uint256 messageNonce, uint256 gasLimit);
@@ -26,7 +14,10 @@ contract MessengerMock {
xDomainMessageSender = xDomainMessageSender_;
}
- function sendMessage(address _target, bytes calldata _message, uint32 _minGasLimit) external payable {
- emit SentMessage(_target, msg.sender, _message, 0, _minGasLimit);
+ function sendMessage(address target, bytes calldata message, uint32 minGasLimit) external payable {
+ lastTarget = target;
+ lastMessageHash = keccak256(message);
+ lastMinGasLimit = minGasLimit;
+ emit SentMessage(target, msg.sender, message, 0, minGasLimit);
}
}