compile.lem

(*
  Copyright 2016 Sami Mäkelä

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

open import Pervasives
open import Evm
open import Word8
open import Rlp

(*
let rec big_step c v = match v.venv_gas_left with
 | 0 -> ProgramStepRunOut
 | _ ->
   match venv_next_instruction v c with
    | Nothing -> ProgramStepRunOut
    | Just i ->
      match instruction_sem v c i with
      | InstructionContinue new_v -> big_step c new_v
      | InstructionToWorld a st bal opt_pushed_v -> ProgramToWorld a st bal opt_pushed_v
      | _ -> ProgramInvalid
      end
   end
end
*)

type program_state =
 | Continue of variable_env * nat * nat
 | Return of program_result

val program_step : constant_env -> program_state -> program_state
let program_step c st = match st with
| Continue v tiny_step remaining_steps ->
  match remaining_steps with
  | 0 -> Return ProgramStepRunOut
  | remaining_steps + 1 ->
   if tiny_step <= 0 then
     Return (ProgramToWorld ContractFail v.venv_storage_at_call v.venv_balance_at_call Nothing) else
   if not (check_annotations v c) then Return ProgramAnnotationFailure else
   match venv_next_instruction v c with
    | Nothing -> Return ProgramStepRunOut
    | Just i ->
      match instruction_sem v c i with
      | InstructionContinue new_v ->
         if new_v.venv_pc > v.venv_pc then Continue new_v (tiny_step - 1) (remaining_steps+1)
         else Continue new_v c.cenv_program.program_length remaining_steps
      | InstructionToWorld a st bal opt_pushed_v -> Return (ProgramToWorld a st bal opt_pushed_v)
      | _ -> Return ProgramInvalid
      end
   end
  end
| Return r -> Return r
end

val program_iter : constant_env -> program_state -> nat -> program_state
let rec program_iter c st n = match n with
 | n+1 -> program_iter c (program_step c st) n
 | 0 -> st
end
declare termination_argument program_iter = automatic

theorem program_iter_bigstep : forall x c v n k steps. (Return x = program_iter c (Continue v n k) steps) --> (program_sem v c n k = x)

(* expressions *)

type simple =
 | ImmedV of uint
(* | StackV of word8 *)
 | MemoryV of uint
 | StorageV of uint

let get_simple v expr = match expr with
 | ImmedV x -> Just x
(* | StackV b -> List.index v.venv_stack (word8ToNat b) *)
 | MemoryV addr -> Just (read_word_from_bytes 0 (cut_memory addr 32 v.venv_memory))
 | StorageV addr -> Just (v.venv_storage addr)
end

let compile_simple expr = match expr with
 | ImmedV uint -> [Stack (PUSH_N (word_rsplit uint))]
(* | StackV b -> [Dup b] *)
 | MemoryV addr -> [Stack (PUSH_N (word_rsplit addr)); Memory MLOAD]
 | StorageV addr -> [Stack (PUSH_N (word_rsplit addr)); Storage SLOAD]
end

let get_stack_top st = match st with
| ProgramToWorld _ _ _ (Just (<| venv_stack = top :: _ |>,_,_)) -> Just top
| _ -> Nothing
end

let eval_expr v addr prog =
  get_stack_top (program_sem (<| v with venv_pc = 0 |>) <| cenv_program = program_of_lst (prog ++ [Misc STOP]); cenv_this = addr |> 100 100)

theorem simple_correct : forall expr v addr. eval_expr v addr (compile_simple expr) = get_simple v expr

type binop = Add | Minus

type unop = Negate | LNot

let calc_unop op x = match op with
 | Negate -> ~x
 | LNot -> lnot x
end

let calc_binop op x y = match op with
 | Add -> x+y
 | Minus -> x-y
end

let lift_option f x = match x with
 | Just x -> Just (f x)
 | Nothing -> Nothing
end

let lift_option2 f x y = match (x,y) with
 | (Just x, Just y) -> Just (f x y)
 | _ -> Nothing
end

type expr =
 | Simple of simple
 | Binary of binop * expr * expr
 | Unary of unop * expr

let rec get_expr v expr = match expr with
 | Simple s -> get_simple v s
 | Unary op expr -> lift_option (calc_unop op) (get_expr v expr)
 | Binary op e1 e2 -> lift_option2 (calc_binop op) (get_expr v e1) (get_expr v e2)
end

let binop_inst op = match op with
 | Add -> [Arith ADD]
 | Minus -> [Arith SUB]
end

let unop_inst op = match op with
 | Negate -> compile_simple (ImmedV 0) ++ [Arith SUB]
 | LNot -> [Bits inst_NOT]
end

let rec compile_expr expr = match expr with
 | Simple s -> compile_simple s
 | Unary op expr -> compile_expr expr ++ unop_inst op
 | Binary op e1 e2 -> compile_expr e1 ++ compile_expr e2 ++ binop_inst op
end

theorem expr_correct : forall expr v addr. eval_expr v addr (compile_expr expr) = get_expr v expr