Lemmas on Boolean reasoning, set reasoning, map lookup

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.342"
+version = "1.0.343"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.342'
+VERSION: Final = '1.0.343'

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k

@@ -28,7 +28,7 @@ module LEMMAS [symbolic]
     rule         chop(_V) <Int pow256 => true        [simplification]
 
     rule X *Int Y <Int pow256 => true requires Y <=Int maxUInt256 /Int X [simplification]
-    rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification] 
+    rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]
 
   // ########################
   // Set Reasoning
@@ -37,6 +37,9 @@ module LEMMAS [symbolic]
     rule X in (SetItem(Y) _   ) => true      requires X  ==Int Y [simplification]
     rule X in (SetItem(Y) REST) => X in REST requires X =/=Int Y [simplification]
 
+    rule   ( S:Set |Set SetItem ( X )                      ) |Set SetItem( X ) => S [simplification]
+    rule ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) |Set SetItem( X ) => S [simplification]
+
   // ########################
   // Word Reasoning
   // ########################
@@ -56,8 +59,6 @@ module LEMMAS [symbolic]
     rule bool2Word(_B) |Int 1 => 1            [simplification]
     rule bool2Word( B) &Int 1 => bool2Word(B) [simplification]
 
-    rule notBool notBool B => B [simplification]
-
     // #newAddr range
     rule 0 <=Int #newAddr(_,_)             => true   [simplification]
     rule         #newAddr(_,_) <Int pow160 => true   [simplification]
@@ -80,12 +81,13 @@ module LEMMAS [symbolic]
   // Map Reasoning
   // ########################
 
-    rule #lookup ( _M:Map [ K1 <- V1 ] , K2 ) => #lookup ( K1 |-> V1 , K1 )  requires K1 ==Int  K2 [simplification]
-    rule #lookup (  M:Map [ K1 <- _  ] , K2 ) => #lookup ( M         , K2 )  requires K1 =/=Int K2 [simplification]
-
     rule 0 <=Int #lookup( _M:Map , _ )             => true [simplification, smt-lemma]
     rule         #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
 
+    rule #lookup ( _M:Map [ K1 <- V1 ] , K2 )    => #lookup ( K1 |-> V1 , K1 ) requires K1 ==Int  K2 [simplification]
+    rule #lookup (  M:Map [ K1 <- _  ] , K2 )    => #lookup ( M         , K2 ) requires K1 =/=Int K2 [simplification]
+    rule #lookup ( (K1:Int |-> _) M:Map, K2:Int) => #lookup ( M,          K2 ) requires K1 =/=Int K2 [simplification]
+
     rule M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] ==K M:Map [ I2 <- V2 ] [ I1 <- V1 ] => true
       requires I1 =/=Int I2
       [simplification]
@@ -217,6 +219,10 @@ module LEMMAS-HASKELL [symbolic, kore]
   // Boolean Logic
   // ########################
 
-    rule B ==Bool false => notBool B [simplification]
+    rule B ==Bool true  => B         [simplification, comm]
+    rule B ==Bool false => notBool B [simplification, comm]
+
+    rule notBool notBool B => B [simplification]
+
     rule (notBool (A andBool B)) andBool A => (notBool B) andBool A [simplification]
 endmodule

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md

@@ -21,7 +21,7 @@ Address/Hash Helpers
 -   `keccak` serves as a wrapper around the `Keccak256` in `KRYPTO`.
 
 ```k
-    syntax Int ::= keccak ( Bytes ) [function, total, smtlib(smt_keccak)]
+    syntax Int ::= keccak ( Bytes ) [function, total, injective, smtlib(smt_keccak)]
  // -------------------------------------------------------------------------
     rule [keccak]: keccak(WS) => #parseHexWord(Keccak256bytes(WS)) [concrete]
 ```

package/version

@@ -1 +1 @@
-1.0.342
+1.0.343