Update dependency: deps/kontrol_release

.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()

deps/kontrol_release

@@ -1 +1 @@
-1.0.1
+1.0.34

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

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]