Update dependency: deps/kontrol_release (#48)

* deps/kontrol_release: Set Version 1.0.2 * deps/kontrol_release: Set Version 1.0.3 * deps/kontrol_release: Set Version 1.0.4 * deps/kontrol_release: Set Version 1.0.5 * deps/kontrol_release: Set Version 1.0.6 * deps/kontrol_release: Set Version 1.0.7 * deps/kontrol_release: Set Version 1.0.8 * deps/kontrol_release: Set Version 1.0.9 * deps/kontrol_release: Set Version 1.0.10 * deps/kontrol_release: Set Version 1.0.11 * deps/kontrol_release: Set Version 1.0.12 * deps/kontrol_release: Set Version 1.0.17 * deps/kontrol_release: Set Version 1.0.18 * deps/kontrol_release: Set Version 1.0.19 * deps/kontrol_release: Set Version 1.0.21 * deps/kontrol_release: Set Version 1.0.22 * deps/kontrol_release: Set Version 1.0.23 * deps/kontrol_release: Set Version 1.0.24 * deps/kontrol_release: Set Version 1.0.25 * deps/kontrol_release: Set Version 1.0.26 * deps/kontrol_release: Set Version 1.0.27 * deps/kontrol_release: Set Version 1.0.28 * deps/kontrol_release: Set Version 1.0.29 * deps/kontrol_release: Set Version 1.0.30 * deps/kontrol_release: Set Version 1.0.31 * deps/kontrol_release: Set Version 1.0.32 * adapting lemmas * increasing parallelisation * deps/kontrol_release: Set Version 1.0.33 * deps/kontrol_release: Set Version 1.0.34 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
runtimeverification · Sep 26, 2024 · 641ac35 · 641ac35
1 parent 1087635
commit 641ac35
Show file tree

Hide file tree

Showing 6 changed files with 59 additions and 190 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -20,7 +20,7 @@ jobs:
         with:
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
           fetch-depth: 0
-      
+
       - name: 'Get Kontrol Version'
         run: |
           set -euo pipefail
@@ -43,7 +43,7 @@ jobs:
       - name: 'Run Kontrol'
         run: |
           # Run the following in the running docker container
-          docker exec -u user ${{ env.repository_basename }}-ci bash -c './test/run-kevm.sh'
+          docker exec -u user ${{ env.repository_basename }}-ci bash -c 'kontrol build; kontrol prove --maintenance-rate 128'
 
       - name: 'Stop Docker Container'
         if: always()

diff --git a/deps/kontrol_release b/deps/kontrol_release
@@ -1 +1 @@
-1.0.1
+1.0.34
diff --git a/kontrol.toml b/kontrol.toml
@@ -0,0 +1,50 @@
+[build.default]
+foundry-project-root       = '.'
+regen                      = true
+rekompile                  = true
+verbose                    = false
+debug                      = false
+require                    = 'test/solady-lemmas.k'
+module-import              = 'FixedPointMathLibVerification:SOLADY-LEMMAS'
+ast                        = true
+auxiliary-lemmas           = true
+
+[prove.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 100000
+max-iterations             = 10000
+reinit                     = false
+cse                        = false
+workers                    = 1
+max-frontier-parallel      = 16
+maintenance-rate           = 128
+assume-defined             = true
+no-log-rewrites            = true
+kore-rpc-command           = 'kore-rpc-booster --no-post-exec-simplify'
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 16000
+smt-retry-limit            = 0
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+auto_abstract              = true
+run-constructor            = false
+match-test                 = [
+        "FixedPointMathLibVerification.testMulWad(uint256,uint256)",
+        "FixedPointMathLibVerification.testMulWadUp",
+        "FixedPointMathLibVerification.testLog2"
+    ]
+ast                        = true
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = true
+debug                      = false
diff --git a/test/run-kevm.sh b/test/run-kevm.sh
diff --git a/test/run-kontrol.sh b/test/run-kontrol.sh
diff --git a/test/solady-lemmas.k b/test/solady-lemmas.k
@@ -96,11 +96,11 @@ module SOLADY-LEMMAS
       requires 0 <=Int A andBool A <Int B
       [simplification]
 
-    rule A *Int B <Int C => A <Int C /Int B
+    rule B *Int A <Int C => A <Int C /Int B
       requires C modInt B ==Int 0
       [simplification, concrete(B, C)]
 
-    rule A <=Int B *Int C => A /Int C <=Int B
+    rule A <=Int C *Int B => A /Int C <=Int B
       requires A modInt C ==Int 0
       [simplification, concrete(A, C)]
 
@@ -114,22 +114,22 @@ module SOLADY-LEMMAS
     syntax Int ::= "cachedBytesConstant" [alias]
     rule cachedBytesConstant => 6928917744019834342450304135053993530982274426945361611473370484834304
 
-    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 0
+    rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 0
       requires 0 <=Int Y andBool Y <Int 32
        andBool ( Y <=Int 1 orBool Y >=Int 16 )
       [simplification]
 
-    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 1
+    rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 1
       requires 0 <=Int Y andBool Y <Int 32
        andBool 1 <Int Y andBool Y <=Int 3
       [simplification]
 
-    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 2
+    rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 2
       requires 0 <=Int Y andBool Y <Int 32
        andBool 3 <Int Y andBool Y <=Int 7
       [simplification]
 
-    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 3
+    rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 3
       requires 0 <=Int Y andBool Y <Int 32
        andBool 7 <Int Y andBool Y <=Int 15
       [simplification]