From 1aa76f6ff48bf50a263a4d84a83a17be7cfc601b Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Dec 2024 22:55:57 +0100 Subject: [PATCH] adding further in_keys lemmas --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 4 ++++ 1 file changed, 4 insertions(+) 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 index cc7b7701df..175d859b81 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -127,6 +127,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] 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] + // 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]