Feature/foundry to kontrol (#17)

* Move to intall-kontrol action and run kontrol intead of foundry * Fix bash script run-kontrol.sh bugs * Run on pull request Co-authored-by: Palina Tolmach <[email protected]> * Adding new git submodule to track kontrol cheatcodes repository * Updating ReadME documentation, run-kontrol script formatting and steps to follow the README example more closely. Adding some media files for Example showing * Fixing table of contents for quick links in docs * Upgrade install-kontrol to latest version, installs forge / foundry as part of kontrol action --------- Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Palina Tolmach <[email protected]>
runtimeverification · Apr 3, 2024 · 498529c · 498529c
1 parent bb9586b
commit 498529c
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 17 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -21,7 +21,7 @@ jobs:
           submodules: recursive
 
       - name: Install Kontrol
-        uses: runtimeverification/[email protected].0
+        uses: runtimeverification/[email protected].1
         with:
           version: latest
 

diff --git a/README.md b/README.md
@@ -14,13 +14,25 @@ However, they should be reproducible on Windows using the [Windows Subsystem for
 <span style="color:red">Note that the instructions are for linux systems.</span>
 
 
-# Table of Content
+# Table of Contents
+- [Highlights](#highlights)
 - [Machine Setup](#machine-setup)
+  - [Installing Foundry](#installing-foundry)
+  - [Installing KONTROL](#installing-kontrol)
+  - [Repository contents](#repository-contents)
 - [Test Breakdown](#test-breakdown)
-- [Property Testing Using Foundry](#property-testing-using-foundry)
-
-
-
+  - [Contracts](#contracts)
+  - [Tests](#tests)
+- [Property Testing Using Foundry ( Forge )](#property-testing-using-foundry--forge-)
+  - [Build with Forge](#build-with-forge)
+  - [Run Tests with Foundry](#run-tests-with-foundry)
+- [Property Verification using KEVM ( Kontrol )](#property-verification-using-kevm--kontrol-)
+  - [Build with kontrol](#build-with-kontrol)
+  - [Run the Proofs](#run-the-proofs)
+- [Insights by Kontrol](#insights-by-kontrol)
+  - [Kontrol List](#kontrol-list)
+  - [Kontrol View](#kontrol-view)
+
 # Machine Setup
 
 Installing Foundry
@@ -93,16 +105,13 @@ In the [`test`](./test) subdirectory, you will find tests of varying difficulty:
 - `token.t.sol`: Tests of `token.sol`.
 - `exclusiveToken.t.sol`: Tests of `exclusiveToken.t.sol`.
 
-Property Testing Using Foundry
-------------------------------
+# Property Testing Using Foundry ( Forge )
 
 We will use foundry for:
 
 - Building the project (i.e. compiling the files), and
 - Running the property tests on randomized inputs.
 
-# Build the Project (Kontrol / Forge)
-
 Build with Forge
 ----------------
 
@@ -205,8 +214,6 @@ For example:
       Core(s) per socket:  4
       Socket(s):           1
   ```   
-<span style="color:red">Better suggestions? ^^</span>
-
 # Insights by Kontrol
 
 Kontrol List

diff --git a/run-kontrol.sh b/run-kontrol.sh
@@ -57,10 +57,9 @@ kontrol_section_edge() {
 kontrol_build --require lemmas.k --module-import ERC20:DEMO-LEMMAS --verbose
 kontrol_list
 kontrol_prove -j8 \
-            --verbose \
             --bug-report=BUGREPORT.bug \
-            --match-test Examples.test_assert_bool_failing
-            # --match-test Examples.test_assert_bool_passing\
+            --match-test Examples.test_assert_bool_failing \
+            --match-test Examples.test_assert_bool_passing
             # --match-test Examples.test_wmul_increasing_overflow\
             # --match-test Examples.test_wmul_increasing\
             # --match-test Examples.test_wmul_increasing_positive\
@@ -92,8 +91,9 @@ kontrol_show --verbose
 ################
 # Modify Nodes #
 ################
-kontrol_remove_node 4b6c47..d6d6d3
-kontrol_prove --reinit
+# kontrol_remove_node 4b6c47..d6d6d3
+# kontrol_prove --reinit
+
 
 ##############################
 # Additional Reinit Examples #