Feature/foundry to kontrol

.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
 

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
 ----------------
 

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 #