streamlining lookup simplifications

runtimeverification · Nov 2, 2023 · 61fac3d · 61fac3d
1 parent efed1fc
commit 61fac3d
Showing 1 changed file with 0 additions and 6 deletions.
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
@@ -86,15 +86,9 @@ module LEMMAS [symbolic]
   // Map Reasoning
   // ########################
 
-    rule keys(.Map)             => .Set                    [simplification]
-    rule keys(M [ K <- _V ])    => keys(M) |Set SetItem(K) [simplification]
-    rule keys(M [ K <- undef ]) => keys(M) -Set SetItem(K) [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, X:Int) => 0 requires notBool (X:Int in keys(M):Set) [simplification]
-
     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]