Skip to content

Commit

Permalink
bringing back lookup smt lemmas
Browse files Browse the repository at this point in the history
  • Loading branch information
@PetarMax
PetarMax committed Dec 26, 2024
1 parent dd10d98 commit bffb8e5
Show file tree
Hide file tree
Showing 4 changed files with 32 additions and 27 deletions.
24 changes: 12 additions & 12 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 10 additions & 8 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,17 +117,19 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
rule keccak( _ ) <Int pow256 => true [simplification]

// ########################
// Map Reasoning
// Map and #lookup
// ########################

rule [lookup-lb-lt]: X:Int <Int #lookup( _M:Map , _ ) => true requires X <Int 0 [simplification]
rule [lookup-lb-le]: X:Int <=Int #lookup( _M:Map , _ ) => true requires X <=Int 0 [simplification]
rule [lookup-ub-lt]: #lookup( _M:Map , _ ) <Int X:Int => true requires maxUInt256 <Int X [simplification]
rule [lookup-ub-le]: #lookup( _M:Map , _ ) <=Int X:Int => true requires maxUInt256 <=Int X [simplification]
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]

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 )
Expand Down
6 changes: 6 additions & 0 deletions tests/specs/functional/lemmas-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,12 @@ module LEMMAS-SPEC
// Arithmetic
// ----------

claim <k> runLemma(#rangeUInt(256, #lookup(M, KX) -Int #lookup(M, KY))) => doneLemma(true) ... </k>
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]: <k> runLemma(((maxUInt160 &Int ((368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)) modInt pow256)) modInt pow160))
=> doneLemma(368263281805664599098893944405654396525700029268) ... </k>
requires #rangeUInt(256, X)
Expand Down
11 changes: 4 additions & 7 deletions tests/specs/mcd/verification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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' <Int K [simplification]
rule M [ K := BUF:Bytes ] [ K' <- V' ] => M [ K' <- V' ] [ K := BUF ] requires K' <Int K
orBool K +Int lengthBytes(BUF) <=Int K' [simplification]
rule M [ K <- V ] => 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 <Int K'
andBool K' <Int K +Int lengthBytes(BUF)
Expand All @@ -283,11 +285,6 @@ module LEMMAS-MCD [symbolic]
andBool K1 +Int lengthBytes(BUF11) <=Int K2 +Int lengthBytes(BUF2)
[simplification]

rule 0 <=Int #lookup( _M:Map , _ ) => true [simplification, smt-lemma]
rule #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]

rule M [ K <- V ] => M requires #lookup(M, K) ==Int V [simplification]

// ########################
// Arithmetic
// ########################
Expand Down

0 comments on commit bffb8e5

Please sign in to comment.