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 index 9c1efd77d1..0d8c9e096c 100644 --- 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,18 @@ 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)] - | #lookupMemory ( Map , Int ) [symbol(lookupMemory), function, total, smtlib(lookupMemory)] - // --------------------------------------------------------------------------------------------------------- - 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) - - rule [#lookupMemory.some]: #lookupMemory( (KEY |-> VAL:Int) _M, KEY ) => VAL modInt 256 - rule [#lookupMemory.none]: #lookupMemory( M, KEY ) => 0 requires notBool KEY in_keys(M) - //Impossible case, for completeness - rule [#lookupMemory.notInt]: #lookupMemory( (KEY |-> VAL ) _M, KEY ) => 0 requires notBool isInt(VAL) + 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] ``` 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 index 87cfc4ffd4..cc7b7701df 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 @@ -117,17 +117,19 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] rule keccak( _ ) true [simplification] // ######################## - // Map Reasoning + // Map and #lookup // ######################## - rule [lookup-lb-lt]: X:Int true requires X true requires X <=Int 0 [simplification] - rule [lookup-ub-lt]: #lookup( _M:Map , _ ) true requires maxUInt256 true requires maxUInt256 <=Int X [simplification] + rule [lookup-lb]: 0 <=Int #lookup( _:Map , _ ) => true [simplification, smt-lemma] + rule [lookup-up]: #lookup( _:Map , _ ) 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] - 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] + // 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 M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] ==K M:Map [ I2 <- V2 ] [ I1 <- V1 ] => true requires notBool ( I1 ==Int I2 ) diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k index d50b7af092..5a16925e7c 100644 --- a/tests/specs/functional/lemmas-spec.k +++ b/tests/specs/functional/lemmas-spec.k @@ -34,6 +34,12 @@ module LEMMAS-SPEC // Arithmetic // ---------- + claim runLemma(#rangeUInt(256, #lookup(M, KX) -Int #lookup(M, KY))) => doneLemma(true) ... + requires #rangeUInt(256, X) andBool X ==Int #lookup(M, KX) + andBool #rangeUInt(256, Y) andBool Y ==Int #lookup(M, KY) + andBool #rangeUInt(256, Z) andBool Z ==Int #lookup(M, _KZ) + andBool #rangeUInt(256, (X -Int Y) -Int Z) + claim [address-reprojection]: runLemma(((maxUInt160 &Int ((368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)) modInt pow256)) modInt pow160)) => doneLemma(368263281805664599098893944405654396525700029268) ... requires #rangeUInt(256, X) diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k index 4b9741f330..cf400bac8b 100644 --- a/tests/specs/mcd/verification.k +++ b/tests/specs/mcd/verification.k @@ -264,12 +264,14 @@ module LEMMAS-MCD [symbolic] rule #WordPackAddrUInt48UInt48(ADDR, maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow160), UINT48_2) => #WordPackAddrUInt48UInt48(ADDR, 0, UINT48_2) requires maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow160) ==Int 0 [simplification] // ######################## - // Map and #lookup - // ######################## + // Map + // ######################## rule M:Bytes [ K <- V ] [ K' <- V' ] => M [ K' <- V' ] [ K <- V ] requires K' M [ K' <- V' ] [ K := BUF ] requires K' M requires #lookup(M, K) ==Int V [simplification] + rule M [ K := BUF:Bytes ] [ K' := BUF':Bytes ] => M [ K := (#range(BUF , 0 , K' -Int K )) ] [ K' := BUF' ] requires K true [simplification, smt-lemma] - rule #lookup( _M:Map , _ ) true [simplification, smt-lemma] - - rule M [ K <- V ] => M requires #lookup(M, K) ==Int V [simplification] - // ######################## // Arithmetic // ########################