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

.github/workflows/test.yml

@@ -1,34 +1,33 @@
-name: test
+name: Kontrol CI Demo
 
-on: workflow_dispatch
+on: 
+  pull_request:
+    branches:
+      - master
+
+  workflow_dispatch:
 
 env:
   FOUNDRY_PROFILE: ci
 
 jobs:
   check:
+    concurrency: kontrol-ci-demo
     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

@@ -1,52 +1,53 @@
+#!/usr/bin/env bash
 set -euxo pipefail
 
 kontrol_build() {
     kontrol build --require lemmas.k --module-import ERC20:DEMO-LEMMAS \
-            ${verbose}
+            "${verbose}"
 }
 
 kontrol_prove() {
-    kontrol prove ${verbose}     \ 
-            ${break_on_calls}    \
-            ${bug_report}        \
-            ${fail_fast} "$@"
+    kontrol prove "${verbose}"\
+            "${break_on_calls}"\
+            "${bug_report}"\
+            "$@"
 }
 
-kontrol_show() {
-    kontrol show ${verbose} ${test} "$@"
-}
+# kontrol_show() {
+#     kontrol show "${verbose}" "${test}" "$@"
+# }
 
-kontrol_to_dot() {
-    kontrol to-dot ${verbose} ${test} "$@"
-}
+# kontrol_to_dot() {
+#     kontrol to-dot "${verbose}" "${test}" "$@"
+# }
 
-kontrol_view() {
-    kontrol view-kcfg ${verbose} ${test} "$@"
-}
+# kontrol_view() {
+#     kontrol view-kcfg "${verbose}" "${test}" "$@"
+# }
 
-kontrol_list() {
-    kontrol list ${verbose} "$@"
-}
+# kontrol_list() {
+#     kontrol list "${verbose}" "$@"
+# }
 
-kontrol_remove_node() {
-    node_id="$1" ; shift
-    kontrol remove-node ${verbose} ${test} ${node_id} "$@"
-}
+# kontrol_remove_node() {
+#     node_id="$1" ; shift
+#     kontrol remove-node "${verbose}" "${test}" ${node_id} "$@"
+# }
 
-kontrol_simplify_node() {
-    node_id="$1" ; shift
-    kontrol simplify-node ${verbose} ${test} ${node_id} ${bug_report} "$@"
-}
+# kontrol_simplify_node() {
+#     node_id="$1" ; shift
+#     kontrol simplify-node "${verbose}" "${test}" ${node_id} "${bug_report}" "$@"
+# }
 
-kontrol_step_node() {
-    node_id="$1" ; shift
-    kontrol step-node ${verbose} ${test} ${node_id} ${bug_report} "$@"
-}
+# kontrol_step_node() {
+#     node_id="$1" ; shift
+#     kontrol step-node "${verbose}" "${test}" ${node_id} "${bug_report}" "$@"
+# }
 
-kontrol_section_edge() {
-    edge_id="$1" ; shift
-    kontrol section-edge ${verbose} ${test} ${edge_id} ${bug_report} "$@"
-}
+# kontrol_section_edge() {
+#     edge_id="$1" ; shift
+#     kontrol section-edge "${verbose}" "${test}" ${edge_id} "${bug_report}" "$@"
+# }
 
 #test=Examples.test_assert_bool_failing
 #test=Examples.test_assert_bool_passing
@@ -62,10 +63,10 @@ verbose=
 verbose=--verbose
 
 break_on_calls=--break-on-calls
-break_on_calls=
+# break_on_calls=
 
-bug_report=--bug-report
-bug_report=
+bug_report="--bug-report=BUGREPORT.bug"
+# bug_report=
 
 # Uncomment these lines as needed
 # pkill kore-rpc || true
@@ -101,7 +102,7 @@ kontrol_prove -j9                                              \
 # date
 # kontrol_prove --reinit
 # date
-# kontrol_prove --reinit
+# kontrol_prove --reinitf
 # date
 # 
 # test=AssertTest.test_sum_1000