Add Certora specs (#13)

* Add Certora specs

* Improve PATH compatibility

.github/workflows/certora.yml

@@ -0,0 +1,45 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        arbitrum-token-bridge:
+          - l1-token-gateway
+          - l2-token-gateway
+
+    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.arbitrum-token-bridge }}
+        run: make certora-${{ matrix.arbitrum-token-bridge }} results=1
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

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

Makefile

@@ -0,0 +1,3 @@
+PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.8.21:$(PATH)
+certora-l1-token-gateway :; PATH=${PATH} certoraRun certora/L1TokenGateway.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-l2-token-gateway :; PATH=${PATH} certoraRun certora/L2TokenGateway.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)

certora/L1TokenGateway.conf

@@ -0,0 +1,37 @@
+{
+    "files": [
+        "src/L1TokenGateway.sol",
+        "certora/harness/Auxiliar.sol",
+        "test/mocks/InboxMock.sol",
+        "test/mocks/InboxMock.sol:BridgeMock",
+        "test/mocks/InboxMock.sol:OutboxMock",
+        "test/mocks/GemMock.sol",
+        "certora/harness/ImplementationMock.sol"
+    ],
+    "solc": "solc-0.8.21",
+    "solc_optimize_map": {
+        "L1TokenGateway": "200",
+        "Auxiliar": "0",
+        "InboxMock": "0",
+        "BridgeMock": "0",
+        "OutboxMock": "0",
+        "GemMock": "0",
+        "ImplementationMock": "0"
+    },
+    "link": [
+        "L1TokenGateway:inbox=InboxMock",
+        "InboxMock:bridge=BridgeMock",
+        "BridgeMock:activeOutbox=OutboxMock"
+    ],
+    "verify": "L1TokenGateway:certora/L1TokenGateway.spec",
+    "rule_sanity": "basic",
+    "multi_assert_check": true,
+    "parametric_contracts": ["L1TokenGateway"],
+    "build_cache": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "512",
+    "prover_args": [
+        "-enableStorageSplitting false"
+    ],
+    "msg": "L1TokenGateway"
+}