/* ============  Selector Functions ============ */

/*  === General Infrastructure === */
sel pcs: unit -> [int]; // gives all pcs of the contract
sel pcsForOpcode: int -> [int]; // gives all pcs for a certain opcode
sel argumentForPc: int -> [int]; // gives the argument for the opcode at pc (can only be invoked pcs containing a PUSH, JUMP or JUMPI)

/* ============ Opcodes ============= */

const ADD := 0;
const AND := 1;
const LE := 2;
const PUSH := 3;
const POP := 4; 
const MLOAD := 5;
const MSTORE := 6;
const SLOAD := 7;
const SSTORE := 8;
const TIMESTAMP := 9; 
const BALANCE := 10;
const INPUT := 11;
const ADDRESS := 12;
const GAS := 13;
const JUMP := 14; 
const JUMPI := 15;
const RETURN := 16;
const STOP := 17;
const FAIL := 18;
const CALL := 19; 

/* ============  Abstract Domain and abstract operations ============ */

eqtype AbsDom := @T | @V<int>; /* Abstract Domain: @T represents the top element, V(v) concrete elements of value v */

// operation that checks whether a value is concrete (not top)
op isConcrete(a:AbsDom): bool := match a with | @T => false | _ => true;  

//operation that extracts the concrete value from an abstract value (in case of @T it defaults to 0)
op extractConcrete(a:AbsDom): int := match a with | @V(x) => x | _ => 0;

op isAbstract(a:AbsDom): bool := ~ isConcrete(a);

op absAdd(a:AbsDom, b:AbsDom): AbsDom :=
	match (a, b) with
	| (@V(n), @V(m)) => @V(n+m)
	| _ => @T;

op absAnd(a:AbsDom, b:AbsDom): AbsDom :=
	match (a, b) with
	| (@V(n), @V(m)) => (n > 0 && m > 0) ? (@V(1)) : (@V(0))
	| _ => @T;

op absLe(a:AbsDom, b:AbsDom): AbsDom :=
	match (a, b) with
	| (@V(n), @V(m)) => (n <= m) ? (@V(1)) : (@V(0))
	| _ => @T;

/* ============  Predicates ============ */

pred ExState{int}: int * array<AbsDom> * array<AbsDom> * AbsDom * array<AbsDom> * bool; // Execution State: <pc>, size, stack, memory, input, storage, cl (call level)
pred Exc{}: bool; // Exceptional Halting: cl, predicate signalizing exceptional halting
pred Halt{}: array<AbsDom> * AbsDom * bool; // Successful Halting: storage, return value, cl


/* ============  Abstract Rules ============ */

rule exception :=
	for (!pc: int) in pcs()
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> Exc(?cl);

rule add :=
	for (!pc: int) in pcsForOpcode(ADD)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size > 1,
		?x = select ?sa (?size - 1),
		?y = select ?sa (?size - 2)
		=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAdd(?x, ?y)), ?mem, ?in, ?stor, ?cl);

rule and :=
	for (!pc: int) in pcsForOpcode(AND)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size > 1,
		?x = select ?sa (?size - 1),
		?y = select ?sa (?size - 2)
		=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAnd(?x, ?y)), ?mem, ?in, ?stor, ?cl);

rule le :=
	for (!pc: int) in pcsForOpcode(LE)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size > 1,
		?x = select ?sa (?size - 1),
		?y = select ?sa (?size - 2)
		=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absLe(?x, ?y)), ?mem, ?in, ?stor, ?cl);

rule push :=
	for (!pc: int) in pcsForOpcode(PUSH), (!v: int) in argumentForPc(!pc)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> ExState{!pc+1}(?size + 1, store ?sa ?size @V(!v), ?mem, ?in, ?stor, ?cl);

rule pop :=
	for (!pc: int) in pcsForOpcode(POP)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1
		=> ExState{!pc+1}(?size - 1, ?sa, ?mem, ?in, ?stor, ?cl);

rule mstore :=
	for (!pc: int) in pcsForOpcode(MSTORE)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 2,
		?p = select ?sa (?size - 1),
		isConcrete(?p),
		?v = select ?sa (?size - 2)
		=> ExState{!pc+1}(?size - 2, ?sa, store ?mem extractConcrete(?p) ?v, ?in, ?stor, ?cl),
    	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 2,
		?p = select ?sa (?size - 1),
		isAbstract(?p)
		=> ExState{!pc+1}(?size - 2, ?sa, [@T], ?in, ?stor, ?cl);

rule mload :=
	for (!pc: int) in pcsForOpcode(MLOAD)
    	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1,
		?p = select ?sa (?size -1),
		isConcrete(?p),
		?v = select ?mem (extractConcrete(?p))
		=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1,
		?p = select ?sa (?size -1),
		isAbstract(?p)
		=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);

rule sload :=
	for (!pc: int) in pcsForOpcode(SLOAD)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?v: AbsDom, ?p: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1,
		?p = select ?sa (?size -1),
		isConcrete(?p),
		?v = select ?stor extractConcrete(?p)
		=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1,
		?p = select ?sa (?size -1),
		isAbstract(?p)
		=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);

rule sstore :=
	for (!pc: int) in pcsForOpcode(SSTORE)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 2,
		?p = select ?sa (?size -1),
		isConcrete(?p),
		?v = select ?sa (?size -2)
		=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, store ?stor extractConcrete(?p) ?v, ?cl),
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 2,
		?p = select ?sa (?size -1),
		isAbstract(?p)
		=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, [@T], ?cl);

rule timestamp :=
	for (!pc: int) in pcsForOpcode(TIMESTAMP)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);

rule balance :=
	for (!pc: int) in pcsForOpcode(BALANCE)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1
		=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);

rule input :=
	for (!pc: int) in pcsForOpcode(INPUT)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> ExState{!pc+1}(?size + 1, store ?sa ?size ?in, ?mem, ?in, ?stor, ?cl);

rule address :=
	for (!pc: int) in pcsForOpcode(ADDRESS)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);

rule gas :=
	for (!pc: int) in pcsForOpcode(GAS)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);

rule jump :=
	for (!pc: int) in pcsForOpcode(JUMP), (!j: int) in argumentForPc(!pc)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> ExState{!j}(?size, ?sa, ?mem, ?in, ?stor, ?cl);

rule jumpi :=
	for (!pc: int) in pcsForOpcode(JUMPI), (!j: int) in argumentForPc(!pc)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1,
		?p = select ?sa (?size - 1),
		(isAbstract(?p) || extractConcrete(?p) != 0)
		=> ExState{!j}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl),
    	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1,
		?p = select ?sa (?size - 1),
		(isAbstract(?p) || extractConcrete(?p) = 0)
		=> ExState{!pc+1}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl);

rule return :=
	for (!pc: int) in pcsForOpcode(RETURN)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size >= 1,
		?p = select ?sa (?size -1)
		=> Halt{}(?stor, ?p, ?cl);

rule stop :=
	for (!pc: int) in pcsForOpcode(STOP)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> Halt{}(?stor, @V(0), ?cl);

rule fail :=
	for (!pc: int) in pcsForOpcode(FAIL)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
		=> Exc(?cl);

rule call1 :=
	for (!pc: int) in pcsForOpcode(CALL)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size > 3
		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);

rule call2 :=
	for (!pc: int) in pcsForOpcode(CALL)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv:array<AbsDom>, ?r: AbsDom]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size > 3,
		Halt{}(?storInv, ?r, true)
		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);

rule call3 :=
	for (!pc: int) in pcsForOpcode(CALL)
	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
		?size > 3
		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);

/* ============  Initialization ============ */

rule initOp :=
	clause
		true 
		=> ExState{0}(0, [@V(0)], [@V(0)], @T, [@T], false); // execution starts at pc 0 in empty execution state