Upstream lemmas from Wormhole engagement

include/kframework/lemmas/bitwise-simplification.k

@@ -12,6 +12,9 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule A |Int 0 => A [simplification]
     rule A |Int A => A [simplification]
 
+    rule  1 |Int _  ==Int 0          => false [simplification]    
+    rule (A |Int B) ==Int (B |Int A) => true  [simplification, smt-lemma]
+
   // ###########################################################################
   // bit-and
   // ###########################################################################
@@ -20,6 +23,8 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule _ &Int 0 => 0 [simplification]
     rule A &Int A => A [simplification]
 
+    rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification]  
+
     rule chop ( ( maxUInt48 &Int X:Int ) *Int Y:Int ) => ( maxUInt48 &Int X:Int ) *Int Y
       requires 0 <=Int X andBool 0 <=Int Y andBool Y <=Int pow208 [simplification]
 
@@ -40,7 +45,20 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule [bitwise-and-lt]:       (X &Int Y) <Int Z      => true requires 0 <=Int X andBool 0 <=Int Y andBool (X <Int Z orBool Y <Int Z)          [simplification]
     rule [bitwise-or-lt-pow256]: (X |Int Y) <Int pow256 => true requires 0 <=Int X andBool 0 <=Int Y andBool X <Int pow256 andBool Y <Int pow256 [simplification]
 
+   // We should probably generalize the simplifications below for relevant powers of two.
+    rule notMaxUInt8   &Int X => 0 requires #rangeUInt(  8, X) [simplification]
+    rule notMaxUInt16  &Int X => 0 requires #rangeUInt( 16, X) [simplification]
+    rule notMaxUInt32  &Int X => 0 requires #rangeUInt( 32, X) [simplification]
+    rule notMaxUInt64  &Int X => 0 requires #rangeUInt( 64, X) [simplification]
     rule notMaxUInt160 &Int X => 0 requires #rangeUInt(160, X) [simplification]
+
+    rule notMaxUInt240 &Int (X <<Int 240) => X <<Int 240 requires #rangeUInt(16, X) [simplification]
+    rule notMaxUInt248 &Int (X <<Int 248) => X <<Int 248 requires #rangeUInt( 8, X) [simplification]
+
+    rule maxUInt8   &Int (X |Int (  notMaxUInt8 &Int Y:Int)) => X requires #rangeUInt(  8, X) andBool 0 <=Int Y [simplification]
+    rule maxUInt16  &Int (X |Int ( notMaxUInt16 &Int Y:Int)) => X requires #rangeUInt( 16, X) andBool 0 <=Int Y [simplification]
+    rule maxUInt32  &Int (X |Int ( notMaxUInt32 &Int Y:Int)) => X requires #rangeUInt( 32, X) andBool 0 <=Int Y [simplification]
+    rule maxUInt64  &Int (X |Int ( notMaxUInt64 &Int Y:Int)) => X requires #rangeUInt( 64, X) andBool 0 <=Int Y [simplification]  
     rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int Y:Int)) => X requires #rangeUInt(160, X) andBool 0 <=Int Y [simplification]
 
     rule [lengthBytes-upInt-32-lower-bound]:
@@ -52,4 +70,16 @@ module BITWISE-SIMPLIFICATION [symbolic]
       lengthBytes(X) +Int 32 >Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true
       [simplification, smt-lemma]
 
+  // ###########################################################################
+  // shift
+  // ###########################################################################
+
+    rule (X <<Int  16) <Int pow256 => true requires #rangeUInt(240, X) [simplification]
+    rule (X <<Int 240) <Int pow256 => true requires #rangeUInt( 16, X) [simplification]
+    rule (X <<Int 248) <Int pow256 => true requires #rangeUInt(  8, X) [simplification]
+
+    rule (X <<Int 16) ==Int (X *Int pow16) => true requires 0 <=Int X [simplification, smt-lemma]
+
+    rule 0 <=Int (X <<Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification]
+
 endmodule

include/kframework/lemmas/bytes-simplification.k

@@ -66,6 +66,11 @@ module BYTES-SIMPLIFICATION [symbolic]
       requires 0 <=Int W1 andBool 0 <=Int W2
       [simplification]
 
+    rule #buf(32 , #asWord(B:Bytes)) => B requires lengthBytes(B) ==Int 32 [simplification]
+
+    rule #buf(32, X <<Int 248) => #buf(1, X) +Bytes #buf(31, 0) requires #rangeUInt( 8, X) [simplification]
+    rule #buf(32, X <<Int 240) => #buf(2, X) +Bytes #buf(30, 0) requires #rangeUInt(16, X) [simplification]
+
     // #range
 
     rule [range-empty]:

include/kframework/word.md

@@ -241,20 +241,32 @@ The maximum and minimum values of each type are defined below.
     rule maxUFixed128x10 =>  3402823669209384634633746074317682114550000000000                              /* ( 2^128 - 1) * 10^10 */
 
     syntax Int ::= "notMaxUInt5"   [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE0 */
+                 | "notMaxUInt8"   [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00 */
+                 | "notMaxUInt16"  [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000 */
+                 | "notMaxUInt32"  [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000 */
+                 | "notMaxUInt64"  [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000000000000000 */
                  | "notMaxUInt96"  [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF000000000000000000000000 */
                  | "notMaxUInt128" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000000000000000000000000000 */
                  | "notMaxUInt160" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFF0000000000000000000000000000000000000000 */
                  | "notMaxUInt192" [alias] /* FFFFFFFFFFFFFFFF000000000000000000000000000000000000000000000000 */
                  | "notMaxUInt208" [alias] /* FFFFFFFFFFFF0000000000000000000000000000000000000000000000000000 */
                  | "notMaxUInt224" [alias] /* FFFFFFFF00000000000000000000000000000000000000000000000000000000 */
+                 | "notMaxUInt240" [alias] /* FFFF000000000000000000000000000000000000000000000000000000000000 */
+                 | "notMaxUInt248" [alias] /* FF00000000000000000000000000000000000000000000000000000000000000 */
  // -------------------------------------------------------------------------------------------------------------
     rule notMaxUInt5   => 115792089237316195423570985008687907853269984665640564039457584007913129639904
+    rule notMaxUInt8 => 115792089237316195423570985008687907853269984665640564039457584007913129639680
+    rule notMaxUInt16 => 115792089237316195423570985008687907853269984665640564039457584007913129574400
+    rule notMaxUInt32 => 115792089237316195423570985008687907853269984665640564039457584007908834672640
+    rule notMaxUInt64 => 115792089237316195423570985008687907853269984665640564039439137263839420088320
     rule notMaxUInt96  => 115792089237316195423570985008687907853269984665561335876943319670319585689600
     rule notMaxUInt128 => 115792089237316195423570985008687907852929702298719625575994209400481361428480
     rule notMaxUInt160 => 115792089237316195423570985007226406215939081747436879206741300988257197096960
     rule notMaxUInt192 => 115792089237316195417293883273301227089434195242432897623355228563449095127040
     rule notMaxUInt208 => 115792089237315784047431654707177369110974345328014318355491175612947292487680
     rule notMaxUInt224 => 115792089210356248756420345214020892766250353992003419616917011526809519390720
+    rule notMaxUInt240 => 115790322390251417039241401711187164934754157181743688420499462401711837020160
+    rule notMaxUInt248 => 115339776388732929035197660848497720713218148788040405586178452820382218977280
 
     syntax Int ::= "eth"         [macro]
                  | "maxBlockNum" [macro] /* 7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF == (2 ^ 256) - (2 ^ 255) - 1 */

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.186"
+version = "1.0.187"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

package/debian/changelog

@@ -1,4 +1,4 @@
-kevm (1.0.186) unstable; urgency=medium
+kevm (1.0.187) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-1.0.186
+1.0.187