

eqtype AbsDom := @T | @V<int>; /* integers in word range */

sel interval: int -> [int]; // function that gives the intervall from 0 till argument

op pow{!n: int} (a: int): int := for (!i: int) in interval(!n) : * a; // at the moment we would need to define the function that gives the interval from 1..n

const MAX := pow{32}(256); // 115792089237316195423570985008687907853269984665640564039457584007913129639936

op absadd(a: AbsDom, b: AbsDom): AbsDom := match (a, b) with | (@V(x), @V(y)) => @V((x + y) mod MAX) | _ => @T ;
op abseq(a:AbsDom, b:AbsDom): bool := match (a, b) with | (@V(x), @V(y)) => x = y | _ => true;
op concat{!l:int}(a:int, b:int): int := a * pow{!l}(256) + b; // Do we need to perform a modulo operation here?
op concatAbs{!l:int}(a:AbsDom, b:AbsDom): AbsDom := match (a, b) with | (@V(x), @V(y)) => @V(concat{!l}(x, y)) | _ => @T;

sel idsAndPcsForOpcode: int -> [int*int]; // the set of (id, pc) combinations for a given opcode
sel idsAndPcsAndJumpDestsForOpcode: int -> [int*int*int]; // the set of (id, pc, j) combinations for a given opcode
sel jumpDestsForID: int -> [int]; // the set of (id, j) pairs such that j is a valid jump destination for contract with id

pred MState{int*int}: int * array<AbsDom> * int * int; // <id, pc>: size, stack, aw, cd
pred Mem{int*int}: AbsDom * AbsDom * int; // <id, pc>: pos, v, cd
pred Exc{int}: int; // cd, predicate signalizing exceptional halting
pred Code{int}: int * AbsDom; // pc + value, maybe we want to get rid of this as it would actually not be needed

pred FunnyFun{}: int;

/* rule for addition */
rule opAdd :=
	for (!id: int, !pc: int) in idsAndPcsForOpcode(1) // 1 is the numeric value of opcode ADD
	let
		macro #StackSizeCheck := MState{!id, !pc}(?size, ?sa, ?aw, ?cd), ?size > 1,
		macro #StackSizeCheckArg($size:int, $sa: array<AbsDom>, $aw: int, $cd:int) := MState{!id, !pc}($size, $sa, $aw, $cd), $size > 1
	in
	clause [?x: AbsDom, ?y:AbsDom, ?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		#StackSizeCheck, ?x = select ?sa (?size -1), ?y = select ?sa (?size -2)
		=> MState{!id, !pc +1}(?size-1, store ?sa (?size-2) (absadd(?x,?y)), ?aw, ?cd),
	clause [?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int, ?pos: AbsDom, ?v: AbsDom]
		#StackSizeCheckArg(?size, ?sa, ?aw, ?cd), Mem{!id, !pc}(?pos, ?v, ?cd)
		=> Mem{!id, !pc}(?pos, ?v, ?cd),
	clause [?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		MState{!id, !pc}(?size, ?sa, ?aw, ?cd), ?size < 2
		=> Exc{2}(?cd); //TODO 2

/* rule for push */

// For now just the simple case that there are enough opcodes still available
rule opPush1 :=
	for (!id: int, !pc:int) in idsAndPcsForOpcode(96)
	clause [?v: AbsDom, ?v1: AbsDom, ?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		MState{!id, !pc}(?size, ?sa, ?aw, ?cd), ?size < 1024, Code{!id}(!pc + 1, ?v1) , ?v = concatAbs{31}(?v1, @V(0))
		=> MState{!id, !pc + 2}(?size + 1, store ?sa ?size ?v, ?aw, ?cd);

//Idea probably with a fitting selector that gives the values for (id, pc) we can also make a general push n rule (using the general sum)


/* rule for jumping */
rule opJump :=
	for (!id: int, !pc: int, !j: int) in idsAndPcsAndJumpDestsForOpcode(86) // 86 is the numeric value of opcode JUMP
	let
		macro #StackSizeAndJumpDestCheck :=
			MState{!id, !pc}(?size, ?sa, ?aw, ?cd), ?size > 0, ?i=select ?sa (?size-1),
			match ?i with |@V(x) => for (!k : int)  in jumpDestsForID(!id) : || x = !k | _ => true //  is it ok to have the dependency here between !id and !k here?
	in
	clause [?i: AbsDom, ?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		#StackSizeAndJumpDestCheck, abseq(?i, @V(!j))
		=> MState{!id, !j}(?size-1, ?sa, ?aw, ?cd),
	clause [?pos: AbsDom, ?v: AbsDom, ?i: AbsDom, ?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		#StackSizeAndJumpDestCheck, abseq(?i, @V(!j)), Mem{!id, !pc}(?pos, ?v, ?cd)
		=> Mem{!id, !pc}(?pos, ?v, ?cd),
	clause [?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		MState{!id, !pc}(?size, ?sa, ?aw, ?cd), ?size < 1
		=> Exc{!id}(?cd),//TODO 2
	clause [?i: AbsDom, ?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		MState{!id, !pc}(?size, ?sa, ?aw, ?cd), ?i=select ?sa (?size-1), match ?i with |@V(x) => for (!k : int)  in jumpDestsForID(!id) : && x != !k | _ => true
		=> Exc{!id}(?cd),//TODO 2
	clause [?sa: array<AbsDom>, ?size:int, ?aw:int, ?cd: int]
		MState{!id, !pc}(?size, ?sa, ?aw, ?cd) // actually this rule subsumes all the ones before (this only holds for the simplified setting that ignores the gas)
		=> Exc{!id}(?cd)
		;

rule unitRuleBaseCase :=
    clause
    true
        => FunnyFun(1)
        ;

rule unitRule :=
    clause [?i : int]
        FunnyFun(?i)
        => FunnyFun(?i+1)
        ;

