module Tests

open FStar.List.Tot
open Solution

(* Test cases *) 
let empty_gs: gstate = fun a -> (0, (fun p -> 0),  []) 
let code1 = [PUSH 2; PUSH 1; LE; JUMPI 5; STOP; PUSH 5; RETURN] 
let ts1: tenv = 0 
let cs1 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (0, 0, code1) , empty_gs)]
let cs1_res1: callstack = Exec [( (15, 6, (fun p -> 0), [5]) , (0, 0, code1) , empty_gs)] (* after 5 steps *) 
let cs1_res2: callstack = Ter (HaltState empty_gs 5 14) []

val test1: unit -> 
Lemma (ensures ((nsteps 5 ts1 cs1 == cs1_res1) /\ (nsteps 6 ts1 cs1 == cs1_res2)))
let test1 () = () 


let code2 = [PUSH 1; PUSH 2; PUSH 0; POP; AND; PUSH 5; MSTORE; PUSH 5; MLOAD] 
let ts2: tenv = 0 
let cs2 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (0, 0, code2) , empty_gs)]
let cs2_res1: callstack = Exec [( (15, 5, (fun p -> 0), [1]) , (0, 0, code2) , empty_gs)] (* after 5 steps *) 
let cs2_res2: callstack = Exec [( (11, 9, (update (fun p -> 0) 5 1), [1]) , (0, 0, code2) , empty_gs)] (* after 9 steps *) 


#set-options "--max_fuel 20 --z3rlimit 10"
val test2: unit -> 
Lemma (ensures (nsteps 5 ts2 cs2 == cs2_res1) /\ (nsteps 9 ts2 cs2 == cs2_res2))
let test2 () = () 
#reset-options 


let code3 = [PUSH 7; BALANCE; TIMESTAMP; SSTORE; PUSH 5; SLOAD; SLOAD] 
let gs3:gstate = update #account #address  (fun _ -> (0, (fun _ -> 0), [])) 7 (42,(fun n -> n+1), []) 
let ts3: tenv = 6 
let cs3 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (7, 0, code3) , gs3)]
let cs3_res1: callstack = Exec [( (17, 3, (fun p -> 0), [6;42]) , (7, 0, code3) , gs3 )] (* after 3 steps *) 
let cs3_res2: callstack = Exec [( (16, 4, (fun p -> 0), []) , (7, 0, code3) , update #account #address gs3 7 (42, update (fun n -> n+1) 6 42, []))] (* after 4 steps *) 
let cs3_res3: callstack = Exec [( (13, 7, (fun p -> 0), [42]) , (7, 0, code3) , update #account #address gs3 7 (42, update (fun n -> n+1) 6 42, []))] (* after 7 steps *) 
//let cs3_res2: callstack = Exec [( (11, 9, (update (fun p -> 0) 5 1), [1]) , (0, 0, code3) , empty_gs)] (* after 9 steps *) 

#set-options "--max_fuel 20 --z3rlimit 10"
val test3: unit -> 
Lemma (ensures ((nsteps 3 ts3 cs3 == cs3_res1) /\ (nsteps 4 ts3 cs3 == cs3_res2) /\ (nsteps 7 ts3 cs3 == cs3_res3)))
let test3 () = () 
#reset-options 


let code4_1 = [PUSH 9; PUSH 7; PUSH 1; BALANCE ; PUSH 2; CALL; POP; PUSH 9; MLOAD] 
let code4_2 = [INPUT; PUSH 1; ADD; RETURN]
let gs4:gstate = update #account #address (update #account #address  (fun _ -> (0, (fun _ -> 0), [])) 1 (42,(fun _ -> 0), code4_1)) 2 (1337, (fun _ -> 0),code4_2) 
let gs4_upd:gstate = update #account #address (update #account #address gs4 2 (1337 + 42,(fun _ -> 0), code4_2)) 1 (0, (fun _ -> 0),code4_1) 
let ts4: tenv = 0 
let cs4 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (1, 0, code4_1) , gs4)]
let cs4_res0: callstack = Exec [( (15, 5, (fun p -> 0), [2;42;7;9]) , (1, 0, code4_1) , gs4 )] (* after 5 steps *) 
let cs4_res1: callstack = Exec [( (14, 0, (fun p -> 0), []) , (2, 7, code4_2) , gs4_upd );( (15, 5, (fun p -> 0), [2;42;7;9]) , (1, 0, code4_1) , gs4)] (* after 6 steps *) 
let cs4_res2: callstack = Exec [( (11, 3, (fun p -> 0), [8]) , (2, 7, code4_2) , gs4_upd );( (15, 5, (fun p -> 0), [2;42;7;9]) , (1, 0, code4_1) , gs4)] (* after 9 steps *) 
let cs4_res3: callstack = Exec [( (10, 6, update (fun p -> 0) 9 8, [1]) , (1, 0, code4_1) , gs4_upd )] (* after 11 steps *) 
let cs4_res4: callstack = Exec [( (7, 9, update (fun p -> 0) 9 8, [8]) , (1, 0, code4_1) , gs4_upd )] (* after 14 steps *) 

#set-options "--max_fuel 40 --z3rlimit 60"


val test4: unit -> 
Lemma (ensures (
  nsteps 5 ts4 cs4 == cs4_res0 /\
  nsteps 6 ts4 cs4 == cs4_res1 /\
  nsteps 9 ts4 cs4 == cs4_res2 /\
  nsteps 11 ts4 cs4 == cs4_res3 /\
  nsteps 14 ts4 cs4 == cs4_res4 
  ))
let test4 () = () 
#reset-options