KEVM Optimizations
These optimizations work on the LLVM and Haskell backend and are generated by the script ./optimizer/optimizations.sh
.
requires "evm.md"
module EVM-OPTIMIZATIONS-LEMMAS [kore, symbolic]
imports EVM
rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification]
rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I <Int #sizeWordStack(WS) [simplification]
rule #stackUnderflow(WS, N) => false requires N <=Int #sizeWordStack(WS) [simplification]
endmodule
module EVM-OPTIMIZATIONS [kore]
imports EVM
imports EVM-OPTIMIZATIONS-LEMMAS
// {OPTIMIZATIONS}
endmodule