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