reverting changes to #lookup

runtimeverification · Dec 27, 2024 · f941e96 · f941e96
1 parent 8547eb8
commit f941e96
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 27 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
@@ -407,18 +407,12 @@ Storage/Memory Lookup
 `#lookup*` looks up a key in a map and returns 0 if the key doesn't exist, otherwise returning its value.
 
 ```k
-    syntax Int ::= #lookup ( Map , Int ) [symbol(lookup), function, total, smtlib(lookup)]
- // --------------------------------------------------------------------------------------
-
-    // #lookup when key is present in map
-    rule #lookup( M:Map, K:Int ) => #if isInt( M:Map [ K ] ) #then { M:Map [ K ] }:>Int modInt pow256 #else 0 #fi
-      requires K in_keys( M:Map )
-      [priority(20), preserves-definedness]
-
-    // #lookup when key is absent in map
-    rule #lookup( M:Map, K:Int ) => 0
-      requires notBool K in_keys( M:Map )
-      [priority(25), preserves-definedness]
+    syntax Int ::= #lookup        ( Map , Int ) [symbol(lookup), function, total, smtlib(lookup)]
+ // ---------------------------------------------------------------------------------------------
+    rule [#lookup.some]:   #lookup( (KEY |-> VAL:Int) _M, KEY ) => VAL modInt pow256
+    rule [#lookup.none]:   #lookup(                    M, KEY ) => 0                 requires notBool KEY in_keys(M)
+    //Impossible case, for completeness
+    rule [#lookup.notInt]: #lookup( (KEY |-> VAL    ) _M, KEY ) => 0                 requires notBool isInt(VAL)
 ```
 
 Substate Log

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -117,29 +117,21 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
     rule         keccak( _ ) <Int pow256 => true [simplification]
 
   // ########################
-  // Map and #lookup
+  // Map Reasoning
   // ########################
 
-    rule [lookup-lb]:                    0 <=Int #lookup( _:Map , _ ) => true [simplification, smt-lemma]
-    rule [lookup-up]: #lookup( _:Map , _ )  <Int pow256               => true [simplification, smt-lemma]
-
-    // Symbolic lookup of map update
-    rule ( _:Map [ K1 <- V ] ):Map [ K2 ] => V            requires         K1 ==K K2 [simplification(45), preserves-definedness]
-    rule ( M:Map [ K1 <- _ ] ):Map [ K2 ] => M:Map [ K2 ] requires notBool K1 ==K K2 [simplification(45), preserves-definedness]
-
-    // Symbolic membership of map concat
-    rule K1 in_keys( ( K2 |-> _ ) _:Map ) => true          requires         K1 ==K K2 [simplification(45), preserves-definedness]
-    rule K1 in_keys( ( K2 |-> _ ) M:Map ) => K1 in_keys(M) requires notBool K1 ==K K2 [simplification(45), preserves-definedness]
+    rule 0 <=Int #lookup( _M:Map , _ )             => true [simplification, smt-lemma]
+    rule         #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
 
-    // Symbolic membership of map update
-    rule K1 in_keys( _:Map [ K2 <- _ ] ) => true          requires         K1 ==K K2 [simplification(45), preserves-definedness]
-    rule K1 in_keys( M:Map [ K2 <- _ ] ) => K1 in_keys(M) requires notBool K1 ==K K2 [simplification(45), preserves-definedness]
+    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 notBool ( K1 ==Int K2 ) [simplification]
+    rule #lookup ( (K1:Int |-> _) M:Map, K2:Int) => #lookup ( M         , K2 ) requires notBool ( K1 ==Int K2 ) [simplification]
 
     rule M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] ==K M:Map [ I2 <- V2 ] [ I1 <- V1 ] => true
       requires notBool ( I1 ==Int I2 )
       [simplification]
 
- // Hardcoded #addrFromPrivateKey simplifications, see: https://github.com/runtimeverification/haskell-backend/issues/3573
+  // Hardcoded #addrFromPrivateKey simplifications, see: https://github.com/runtimeverification/haskell-backend/issues/3573
     rule #addrFromPrivateKey("0x0000000000000000000000000000000000000000000000000000000000000001") => 721457446580647751014191829380889690493307935711 [priority(40), concrete]
 
   // ########################