requires "evm.k"
module LTL
imports BOOL
imports SET
imports LIST
configuration
<ltl>
<formula> $LTLFORMULA:LTLFormula </formula>
<eventsId> .EventId </eventsId>
<events> .Set </events>
<trace> .List </trace>
</ltl>
syntax EventId ::= ".EventId"
syntax KItem ::= EventId "{" Set "}"
syntax KItem ::= LTLFormula
syntax LTLFormula ::= LTLderive ( LTLFormula , Set ) [function]
syntax LTLEvent
syntax LTLAtom ::= "True"
| "False"
rule LTLderive(LTLA:LTLAtom, _) => LTLA
syntax LTLFormula ::= "(" LTLFormula ")" [bracket]
| LTLAtom
| LTLEvent
rule LTLderive(E:LTLEvent, ES) => True requires E in ES
rule LTLderive(E:LTLEvent, ES) => False requires notBool E in ES
syntax LTLFormula ::= "~" LTLFormula
| LTLFormula "\\/" LTLFormula
| LTLFormula "/\\" LTLFormula
rule ~ True => False [anywhere]
rule ~ False => True [anywhere]
rule True \/ FORM2 => True [anywhere]
rule FORM1 \/ True => True [anywhere]
rule False \/ FORM2 => FORM2 [anywhere]
rule FORM1 \/ False => FORM1 [anywhere]
rule True /\ FORM2 => FORM2 [anywhere]
rule FORM1 /\ True => FORM1 [anywhere]
rule False /\ FORM2 => False [anywhere]
rule FORM1 /\ False => False [anywhere]
rule LTLderive(~ FORM , ES) => ~ LTLderive(FORM, ES)
rule LTLderive(FORM1 \/ FORM2 , ES) => LTLderive(FORM1, ES) \/ LTLderive(FORM2, ES)
rule LTLderive(FORM1 /\ FORM2 , ES) => LTLderive(FORM1, ES) /\ LTLderive(FORM2, ES)
syntax LTLFormula ::= LTLFormula "->" LTLFormula [macro]
rule FORM1 -> FORM2 => (~ FORM1) \/ FORM2
syntax LTLFormula ::= "always" LTLFormula
| "eventually" LTLFormula
rule LTLderive(always FORM, ES) => LTLderive(FORM, ES) /\ always FORM
rule LTLderive(eventually FORM, ES) => LTLderive(FORM, ES) \/ eventually FORM
syntax LTLFormula ::= LTLterminate ( LTLFormula ) [function]
rule LTLterminate(~ FORM1) => ~ LTLterminate(FORM1)
rule LTLterminate(FORM1 /\ FORM2) => LTLterminate(FORM1) /\ LTLterminate(FORM2)
rule LTLterminate(FORM1 \/ FORM2) => LTLterminate(FORM1) \/ LTLterminate(FORM2)
rule LTLterminate(always _) => True
rule LTLterminate(eventually _) => False
endmodule
module KEVM-LTL
imports EVM
imports LTL
configuration
<kevm-ltl>
<kevm/>
<ltl/>
</kevm-ltl>
syntax EthereumSimulation ::= EthereumCommand | EthereumCommand EthereumSimulation
rule <k> ETC:EthereumCommand ETS:EthereumSimulation => ETC ~> ETS ... </k>
syntax JSON ::= OpCodes | Int
syntax EthereumCommand ::= "load" JSON | "start"
rule <k> load { "gas" : GAVAIL , "code" : OPS:OpCodes , .JSONList } => . ... </k>
<gas> _ => GAVAIL </gas>
<program> _ => #asMapOpCodes(OPS) </program>
<exit-code> _ => 0 </exit-code>
rule <k> start => #execute ... </k>
syntax OpCodes ::= UNSAFEADD ( Int , Int ) [function]
| SAFEADD ( Int , Int ) [function]
rule UNSAFEADD(X, Y) => PUSH(32, X) ; PUSH(32, Y) ; ADD ; .OpCodes
rule SAFEADD(X, Y) => PUSH(32, X) ; PUSH(32, Y) ; ADD ; PUSH(32, 0) ; MSTORE
; PUSH(32, X) ; PUSH(32, 0) ; MLOAD ; GT ; PUSH(32, 372) ; JUMPI
; PUSH(32, Y) ; PUSH(32, 0) ; MLOAD ; GT ; PUSH(32, 372) ; JUMPI
; PUSH(32, 0) ; PUSH(32, 0) ; REVERT
; JUMPDEST ; PUSH(32, 0) ; MLOAD ; .OpCodes
syntax EventId ::= Int
rule <k> #execute ... </k>
<pc> PCOUNT </pc>
<formula> FORM => LTLderive(FORM, EVENTS) </formula>
<eventsId> EID => PCOUNT </eventsId>
<events> EVENTS => .Set </events>
<trace> TRACE:List (.List => ListItem(EID { EVENTS })) </trace>
requires EID =/=K PCOUNT
[priority(24)]
rule <k> #halt </k>
<formula> FORM => LTLderive(FORM, EVENTS) </formula>
<eventsId> EID => .EventId </eventsId>
<events> EVENTS => .Set </events>
<trace> TRACE:List (.List => ListItem(EID { EVENTS })) </trace>
requires EID =/=K .EventId
[priority(24)]
rule <k> #halt </k>
<formula> FORM => LTLterminate(FORM) </formula>
<eventsId> .EventId </eventsId>
requires notBool isLTLAtom(FORM)
syntax LTLEvent ::= "overflow"
rule <k> ADD W0 W1 ... </k>
<events> EVENTS (.Set => SetItem(overflow)) </events>
requires notBool overflow in EVENTS
andBool W0 +Word W1 =/=Int W0 +Int W1
[priority(24)]
syntax LTLEvent ::= "revert"
rule <k> REVERT _ _ ... </k>
<events> EVENTS (.Set => SetItem(revert)) </events>
requires notBool revert in EVENTS
[priority(24)]
syntax LTLEvent ::= "invalid"
rule <k> INVALID ... </k>
<events> EVENTS (.Set => SetItem(invalid)) </events>
requires notBool invalid in EVENTS
[priority(24)]
endmodule