Move to intall-kontrol action and run kontrol intead of foundry

.github/workflows/test.yml

@@ -1,4 +1,4 @@
-name: test
+name: Kontrol CI Demo
 
 on: workflow_dispatch
 
@@ -10,25 +10,18 @@ jobs:
     strategy:
       fail-fast: true
 
-    name: Foundry project
-    runs-on: ubuntu-latest
+    name: Kontrol Demo Project
+    runs-on: [self-hosted, linux, normal]
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
+      - name: Install Kontrol
+        uses: runtimeverification/install-kontrol@v1.0.0
         with:
-          version: nightly
+          version: latest
 
-      - name: Run Forge build
+      - name: Run Kontrol Tests
         run: |
-          forge --version
-          forge build --sizes
-        id: build
-
-      - name: Run Forge tests
-        run: |
-          forge test -vvv
-        id: test
+          ./run-kontrol.sh

README.md

@@ -49,7 +49,7 @@ This repository contains the OpenZeppelin ERC20 (took from the latest commit at
 - the [`src`](./src) directory contains the Solidity source code.
 - the [`test`](./test) directory contains the Foundry property tests.
 - the [`exclude`](./exclude) file contains proofs that are expected to fail.
-- the [`doit`](./doit) file contains examples of Kontrol commands that you can use.
+- the [`run-kontrol.sh`](./run-kontrol.sh) file contains examples of Kontrol commands that you can use.
 - the [`erc20.sh`](./erc20.sh) file contains a script that runs all the ERC20 proofs and times them.
 
 ### Contracts

doit → run-kontrol.sh

@@ -62,10 +62,10 @@ verbose=
 verbose=--verbose
 
 break_on_calls=--break-on-calls
-break_on_calls=
+# break_on_calls=
 
 bug_report=--bug-report
-bug_report=
+# bug_report=
 
 # Uncomment these lines as needed
 # pkill kore-rpc || true
@@ -101,7 +101,7 @@ kontrol_prove -j9                                              \
 # date
 # kontrol_prove --reinit
 # date
-# kontrol_prove --reinit
+# kontrol_prove --reinitf
 # date
 # 
 # test=AssertTest.test_sum_1000