Add Certora specs (#9)

* Add Certora specs

* Add spec for L2GovernanceRelay.relay

* Minor changes

* Use no optimization for mocks and aux

* use mathint

* Minor change

* More rules

* Fix typo

* Fix typo

* Improve PATH compatibility

.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 }}

.gitignore

@@ -12,3 +12,6 @@ docs/
 
 # Dotenv file
 .env
+
+# Certora
+.certora_internal

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,)

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"
+}

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";
+}

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"
+}

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";
+}

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"
+}