Add dummy verification

packages/contracts-bedrock/foundry.toml

@@ -59,3 +59,21 @@ runs = 512
 
 [profile.lite]
 optimizer = false
+
+################################################################
+#                         PROFILE: KONTROL                     #
+################################################################
+
+[profile.kontrol]
+src = 'src/L1'
+out = 'kout'
+test = 'test/kontrol'
+script = 'scripts-kontrol'
+remappings = [
+  '@openzeppelin/contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/contracts',
+  '@openzeppelin/contracts/=lib/openzeppelin-contracts/contracts',
+  '@rari-capital/solmate/=lib/solmate',
+  '@cwia/=lib/clones-with-immutable-args/src',
+  'forge-std/=lib/forge-std/src',
+  'ds-test/=lib/forge-std/lib/ds-test/src'
+]

packages/contracts-bedrock/test/kontrol/Counter.t.sol

+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+/* import {Test} from "forge-std/Test.sol"; */
+import {Counter} from "src/L1/Counter.sol";
+import {OptimismPortal} from "src/L1/OptimismPortal.sol";
+
+contract CounterTest {
+
+    Counter counter;
+    OptimismPortal optimismPortal;
+
+
+    function setUp() public {
+        counter = new Counter();
+        optimismPortal = new OptimismPortal();
+    }
+
+    function test_SetNumber(uint256 x) public {
+        counter.setNumber(x);
+        require(counter.number() == x, "Not equal");
+    }
+}

packages/contracts-bedrock/test/kontrol/kontrol/pausability-lemmas.k

+requires "evm.md"
+requires "foundry.md"
+
+module PAUSABILITY-LEMMAS
+    imports BOOL
+    imports FOUNDRY
+    imports INFINITE-GAS
+    imports INT-SYMBOLIC
+
+// Your lemmas go here
+
+endmodule

packages/contracts-bedrock/test/kontrol/kontrol/run-kontrol.sh

+#!/bin/bash
+
+set -euxo pipefail
+
+FOUNDRY_PROFILE=kontrol
+
+kontrol_build() {
+    kontrol build                     \
+            --verbose                 \
+            --require ${lemmas}       \
+            --module-import ${module} \
+            ${rekompile}
+}
+
+kontrol_prove() {
+    kontrol prove                              \
+            --max-depth ${max_depth}           \
+            --max-iterations ${max_iterations} \
+            --smt-timeout ${smt_timeout}       \
+            --bmc-depth ${bmc_depth}           \
+            --workers ${workers}               \
+            ${reinit}                          \
+            ${bug_report}                      \
+            ${break_on_calls}                  \
+            ${auto_abstract}                   \
+            ${tests}                           \
+            ${use_booster}
+}
+
+###
+# kontrol build options
+###
+# NOTE: This script should be executed from the `contracts-bedrock` directory
+lemmas=test/kontrol/kontrol/pausability-lemmas.k
+base_module=PAUSABILITY-LEMMAS
+module=CounterTest:${base_module}
+
+rekompile=--rekompile
+rekompile=
+
+###
+# kontrol prove options
+###
+max_depth=10000
+
+max_iterations=10000
+
+smt_timeout=100000
+
+bmc_depth=10
+
+workers=2
+
+reinit=--reinit
+reinit=
+
+break_on_calls=--no-break-on-calls
+# break_on_calls=
+
+auto_abstract=--auto-abstract-gas
+# auto_abstract=
+
+bug_report=--bug-report
+bug_report=
+
+use_booster=--use-booster
+# use_booster=
+
+# List of tests to symbolically execute
+tests=""
+tests+="--match-test CounterTest.test_SetNumber "
+
+kontrol_build
+kontrol_prove

packages/contracts-bedrock/verify

+./test/kontrol/kontrol/run-kontrol.sh 2>&1 | tee test/kontrol/kontrol/log.out