evm.ml

(*Generated by Lem from evm.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 Lem_pervasives
open Lem_word
open Word256
open Word160
open Word8

type uint = word256
type address = word160
type byte = word8

(*val sintFromW256 : uint -> int*)
let sintFromW256:word256 ->int=  word256ToInt

(*val uint : uint -> int*)
let uint w:int=  ((word256ToNat w))

(*
val word256ToNat : uint -> nat
let word256ToNat = word256ToNat
*)

(*val absnat : uint -> nat*)
let absnat w:int=  (abs (word256ToInt w))

(*val byteFromNat : nat -> byte*)
let byteFromNat:int ->word8=  word8FromNat

(*
val word_of_int : int -> uint
let word_of_int = word256FromInt
*)

(*val uint_of_bl : list bool -> uint*)
let uint_of_bl:(bool)list ->word256=  word256FromBoollist

(*val uint_to_address : uint -> address*)
let uint_to_address w:word160=  (word160FromNat (word256ToNat w))

(*val address_to_uint : address -> uint*)
let address_to_uint w:word256=  (word256FromNat (word160ToNat w))

(*val uint_to_byte : uint -> byte*)
let uint_to_byte w:word8=  (word8FromNat (word256ToNat w))

(*val byte_to_uint : byte -> uint*)
let byte_to_uint w:word256=  (word256FromNat (word8ToNat w))

(*val keccac : list byte -> uint*)
let keccac _:word256= (word256FromNumeral 0)

(*val test_bit : uint -> nat -> bool*)
let test_bit w n:bool=  
 (if word256Land w ( word256Lsr(word256FromNumeral 1) n) =word256FromNumeral 0 then false
  else true)

(*val word_rsplit_aux : list bool -> nat -> list byte*)
let rec word_rsplit_aux lst n:(word8)list= 
  (
  if(n =  0) then ([]) else
    (let n0 =(Nat_num.nat_monus n ( 1)) in
     word8FromBoollist (take ( 8) lst) :: word_rsplit_aux (drop ( 8) lst) n0))

(*val word_rsplit : uint -> list byte*)
let word_rsplit w:(byte)list=  (word_rsplit_aux (boolListFromWord256 w)( 32))

(*val address_to_bytes : address -> list byte*)
let address_to_bytes w:(byte)list=  (word_rsplit_aux (boolListFromWord160 w)( 20))

(*val get_byte : uint -> uint -> uint*)
let get_byte position w:word256=  
 ((match Lem_list.list_index (word_rsplit w) (absnat position) with
  | None ->word256FromNumeral 0
  | Some (a:byte) -> byte_to_uint a
  ))

type memory = uint -> byte
type storage = uint -> uint

(*val empty_storage : storage*)
let empty_storage _:word256= (word256FromNumeral 0)

type aenv = {
  aenv_stack : uint list;
  aenv_memory : memory;
  aenv_storage : storage;
  aenv_balance : address -> uint;
  aenv_caller : address;
  aenv_value_sent : uint;
  aenv_data_sent : byte list;
  aenv_storage_at_call : storage;
  aenv_balance_at_call : address -> uint;
  aenv_this : address;
  aenv_origin : address;
}

type bits_inst =
| Inst_AND (* bitwise AND *)
| Inst_OR  (* bitwise OR *)
| Inst_XOR (* bitwise exclusive or *)
| Inst_NOT (* bitwise negation *)
| BYTE     (* taking one byte out of a word *)

(*val bits_inst_code : bits_inst -> byte*)
let bits_inst_code inst1:word8=  ((match inst1 with
| Inst_AND ->word8FromNumeral 0X16
| Inst_OR ->word8FromNumeral 0X17
| Inst_XOR ->word8FromNumeral 0X18
| Inst_NOT ->word8FromNumeral 0X19
| BYTE ->word8FromNumeral 0X1a
))


type sarith_inst =
| SDIV (* signed division *)
| SMOD (* signed modulo *)
| SGT  (* signed greater-than *)
| SLT  (* signed less-than *)
| SIGNEXTEND (* extend the size of a signed number *)

(*val sarith_inst_code : sarith_inst -> byte*)
let sarith_inst_code inst1:word8=  ((match inst1 with
| SDIV ->word8FromNumeral 0X05
| SMOD ->word8FromNumeral 0X07
| SGT ->word8FromNumeral 0X13
| SLT ->word8FromNumeral 0X12
| SIGNEXTEND ->word8FromNumeral 0X0b
))

type arith_inst =
| ADD (* addition *)
| MUL (* multiplication *)
| SUB (* subtraction *) 
| DIV (* unsigned division *)
| MOD (* unsigned modulo *)
| ADDMOD (* addition under modulo *)
| MULMOD (* multiplication under modulo *)
| EXP (* exponentiation *)
| Inst_GT (* unsigned greater-than *)
| Inst_EQ (* equality *)
| Inst_LT (* unsigned less-than *)
| ISZERO (* if zero, returns one *)
| SHA3 (* Keccak 256, dispite the name *)

(*val arith_inst_code : arith_inst -> byte*)
let arith_inst_code inst1:word8=  ((match inst1 with
| ADD ->word8FromNumeral 0X01
| MUL ->word8FromNumeral 0X02
| SUB ->word8FromNumeral 0X03
| DIV ->word8FromNumeral 0X04
| MOD ->word8FromNumeral 0X06
| ADDMOD ->word8FromNumeral 0X08
| MULMOD ->word8FromNumeral 0X09
| EXP ->word8FromNumeral 0X0a
| Inst_GT ->word8FromNumeral 0X11
| Inst_LT ->word8FromNumeral 0X10
| Inst_EQ ->word8FromNumeral 0X14
| ISZERO ->word8FromNumeral 0X15
| SHA3 ->word8FromNumeral 0X20
))

type info_inst =
    ADDRESS (* The address of the account currently running *)
  | BALANCE (* The Eth balance of the specified account *)
  | ORIGIN (* The address of the external account that started the transaction *)
  | CALLER (* The immediate caller of this invocation *)
  | CALLVALUE (* The Eth amount sent along this invocation *)
  | CALLDATASIZE (* The number of bytes sent along this invocation *)
  | CODESIZE (* The number of bytes in the code of the account currently running *)
  | GASPRICE (* The current gas price *)
  | EXTCODESIZE (* The size of a code of the specified account *)
  | BLOCKHASH (* The block hash of a specified block among the recent blocks. *)
  | COINBASE (* The address of the miner that validates the current block. *)
  | TIMESTAMP (* The date and time of the block. *)
  | NUMBER (* The block number *)
  | DIFFICULTY (* The current difficulty *)
  | GASLIMIT (* The current block gas limit *)
  | GAS (* The remaining gas for the current execution. This changes after every instruction
  is executed.  *)
  
(*val info_inst_code : info_inst -> byte*)
let info_inst_code inst1:word8=  ((match inst1 with
| ADDRESS ->word8FromNumeral 0X30
| BALANCE ->word8FromNumeral 0X31
| ORIGIN ->word8FromNumeral 0X32
| CALLVALUE ->word8FromNumeral 0X34
| CALLDATASIZE ->word8FromNumeral 0X36
| CALLER ->word8FromNumeral 0X33
| CODESIZE ->word8FromNumeral 0X38
| GASPRICE ->word8FromNumeral 0X3a
| EXTCODESIZE ->word8FromNumeral 0X3b
| BLOCKHASH ->word8FromNumeral 0X40
| COINBASE ->word8FromNumeral 0X41
| TIMESTAMP ->word8FromNumeral 0X42
| NUMBER ->word8FromNumeral 0X43
| DIFFICULTY ->word8FromNumeral 0X44
| GASLIMIT ->word8FromNumeral 0X45
| GAS ->word8FromNumeral 0X5a
))

type dup_inst = byte

(*val dup_inst_code : dup_inst -> maybe byte*)
let dup_inst_code m1:(word8)option=   
 (if w8Less m1(word8FromNumeral 1) then None (*-- There is no DUP0 instruction. *)
   else if w8Greater m1(word8FromNumeral 16) then None (* -- There are no DUP16 instruction and on. *)
   else Some ( word8Add m1(word8FromNumeral 0X7f)))

type memory_inst =
| MLOAD (* reading one machine word from the memory, beginning from the specified offset *)
| MSTORE (* writing one machine word to the memory *)
| MSTORE8 (* writing one byte to the memory *)
| CALLDATACOPY (* copying the caller's data to the memory *)
| CODECOPY (* copying a part of the currently running code to the memory *)
| EXTCODECOPY (* copying a part of the code of the specified account *)
| MSIZE (* the size of the currently used region of the memory. *)

(*val memory_inst_code : memory_inst -> byte*)
let memory_inst_code inst1:word8=  ((match inst1 with
| MLOAD ->word8FromNumeral 0X51
| MSTORE ->word8FromNumeral 0X52
| MSTORE8 ->word8FromNumeral 0X53
| CALLDATACOPY ->word8FromNumeral 0X37
| CODECOPY ->word8FromNumeral 0X39
| EXTCODECOPY ->word8FromNumeral 0X3c
| MSIZE ->word8FromNumeral 0X59
))

type storage_inst =
| SLOAD (* reading one word from the storage *)
| SSTORE (* writing one word to the storage *)

(*val storage_inst_code : storage_inst -> byte*)
let storage_inst_code inst1:word8=  ((match inst1 with
| SLOAD ->word8FromNumeral 0X54
| SSTORE ->word8FromNumeral 0X55
))

type pc_inst =
 | JUMP (* jumping to the specified location in the code *)
 | JUMPI (* jumping to the specified location in the code if a condition is met *)
 | PC (* the current location in the code *)
 | JUMPDEST (* a no-op instruction located to indicate jump destinations. *)

(*val pc_inst_code : pc_inst -> byte*)
let pc_inst_code inst1:word8=  ((match inst1 with
| JUMP ->word8FromNumeral 0X56
| JUMPI ->word8FromNumeral 0X57
| PC ->word8FromNumeral 0X58
| JUMPDEST ->word8FromNumeral 0X5b
))

type stack_inst =
  | POP (* throwing away the topmost element of the stack *)
  | PUSH_N of byte list (* pushing an element to the stack *)
  | CALLDATALOAD (* pushing a word to the stack, taken from the caller's data *)

(*val stack_inst_code : stack_inst -> list byte*)
let stack_inst_code inst1:(word8)list=  ((match inst1 with
| POP -> [word8FromNumeral 0X50]
| PUSH_N lst ->
     if List.length lst < 1 then []
     else if List.length lst > 32 then []
     else  List.rev_append (List.rev [ word8Add(byteFromNat (List.length lst))(word8FromNumeral 0X5f)]) lst
| CALLDATALOAD -> [word8FromNumeral 0X35]
))

type swap_inst = byte

(*val swap_inst_code : swap_inst -> maybe byte*)
let swap_inst_code m1:(word8)option=  
 (if w8Less m1(word8FromNumeral 1) then None else
  if w8Greater m1(word8FromNumeral 16) then None else
  Some ( word8Add m1(word8FromNumeral 0X8f)))

type log_inst =
| LOG0
| LOG1
| LOG2
| LOG3
| LOG4

(*val log_inst_code : log_inst -> byte*)
let log_inst_code inst1:word8=  ((match inst1 with
| LOG0 ->word8FromNumeral 0Xa0
| LOG1 ->word8FromNumeral 0Xa1
| LOG2 ->word8FromNumeral 0Xa2
| LOG3 ->word8FromNumeral 0Xa3
| LOG4 ->word8FromNumeral 0Xa4
))

type misc_inst =
  | STOP (* finishing the execution normally, with the empty return data *)
  | CREATE (* deploying some code in an account *)
  | CALL (* calling (i.e. sending a message to) an account *)
  | CALLCODE (* calling into this account, but the executed code can be some other account's *)
  | DELEGATECALL (* calling into this account, the executed code can be some other account's
                       but the sent value and the sent data are unchanged. *)
  | RETURN (* finishing the execution normally with data *)
  | SUICIDE (* send all remaining Eth balance to the specified account,
                  finishing the execution normally, and flagging the current account for deletion *)

(*val misc_inst_code : misc_inst -> byte*)
let misc_inst_code inst1:word8=  ((match inst1 with
| STOP ->word8FromNumeral 0X00
| CREATE ->word8FromNumeral 0Xf0
| CALL ->word8FromNumeral 0Xf1
| CALLCODE ->word8FromNumeral 0Xf2
| RETURN ->word8FromNumeral 0Xf3
| DELEGATECALL ->word8FromNumeral 0Xf4
| SUICIDE ->word8FromNumeral 0Xff
))

type annotation = aenv -> bool

type inst =
  | Unknown of byte
  | Bits of bits_inst
  | Sarith of sarith_inst
  | Arith of arith_inst
  | Info of info_inst
  | Dup of dup_inst
  | Memory of memory_inst
  | Storage of storage_inst
  | Pc of pc_inst
  | Stack of stack_inst
  | Swap of swap_inst
  | Log of log_inst
  | Misc of misc_inst
  | Annotation of annotation

let maybe_to_list m1:'a list=  ((match m1 with
 | None -> []
 | Some s -> [s]
))

(*val inst_code : inst -> list byte*)
let inst_code inst1:(word8)list=  ((match inst1 with
| Unknown byte1 -> [byte1]
| Bits b -> [bits_inst_code b]
| Sarith s -> [sarith_inst_code s]
| Arith a -> [arith_inst_code a]
| Info i -> [info_inst_code i]
| Dup d -> maybe_to_list (dup_inst_code d)
| Memory m1 -> [memory_inst_code m1]
| Storage s -> [storage_inst_code s]
| Pc p -> [pc_inst_code p]
| Stack s -> stack_inst_code s
| Swap s -> maybe_to_list (swap_inst_code s)
| Log l -> [log_inst_code l]
| Misc m1 -> [misc_inst_code m1]
| Annotation _ -> []
))

(*val inst_size : inst -> nat*)
let inst_size i:int=  (List.length (inst_code i))

(*val drop_bytes : list inst -> nat -> list inst*)
let rec drop_bytes prg n:(inst)list=  ((match (prg, n) with
| (prg, 0) -> prg
| (Stack (PUSH_N v) :: rest, bytes) -> drop_bytes rest ( Nat_num.nat_monus (Nat_num.nat_monus bytes( 1)) (List.length v))
| (Annotation _ :: rest, bytes) -> drop_bytes rest bytes
| (_ :: rest, bytes) -> drop_bytes rest ( Nat_num.nat_monus bytes( 1))
| _ -> []
))

(*val program_size : list inst -> nat*)
let rec program_size lst:int=  ((match lst with
| i :: rest -> inst_size i + program_size rest
| [] -> 0
))

(*val program_code : list inst -> list byte*)
let rec program_code lst:(word8)list=  ((match lst with
| [] -> []
| inst1 :: rest ->  List.rev_append (List.rev (inst_code inst1)) (program_code rest)
))

type call_env = {
  callenv_gaslimit : uint; (* the current block's gas limit *)
  callenv_value : uint; (* the amount of Eth sent along*)
  callenv_data : byte list; (* the data sent along *)
  callenv_caller : address; (* the caller's address *)
  callenv_timestamp : uint; (* the timestamp of the current block *)
  callenv_blocknum : uint; (* the block number of the current block *)
  callenv_balance : address -> uint; (* the balances of all accounts. *)
}

type return_result = {
  return_data : byte list; (* the returned data *)
  return_balance : address -> uint (* the balance of all accounts at the moment of the return*)
}

type world_action =
| WorldCall of call_env (* the world calls into the account *)
| WorldRet of return_result (* the world returns back to the account *)
| WorldFail (* the world fails back to the account. *)

type call_arguments = {
  callarg_gas : uint; (* The portion of the remaining gas that the callee is allowed to use *)
  callarg_code : address; (* The code that executes during the call *)
  callarg_recipient : address; (* The recipient of the call, whose balance and the storage are modified. *)
  callarg_value : uint; (* The amount of Eth sent along *)
  callarg_data : byte list; (* The data sent along *)
  callarg_output_begin : uint; (* The beginning of the memory region where the output data should be written. *)
  callarg_output_size : uint; (* The size of the memory regions where the output data should be written. *)
}

type create_arguments = {
  createarg_value : uint; (* The value sent to the account *)
  createarg_code : byte list; (* The code that deploys the runtime code. *)
}

type contract_action =
| ContractCall of call_arguments (* calling an account *)
| ContractCreate of create_arguments (* deploying a smart contract *)
| ContractFail (* failing back to the caller *)
| ContractSuicide (* destroying itself and returning back to the caller *)
| ContractReturn of byte list (* normally returning back to the caller *)

type program = {
  program_content : (int, inst) Pmap.map; (* a binary search tree that allows looking up instructions from positions *)
  program_length  : int; (* the length of the program in bytes *)
  program_annotation : int -> annotation list; (* a mapping from positions to annotations *)
}

(*val store_byte_list_in_program : nat -> list byte -> map nat inst -> map nat inst*)
let rec store_byte_list_in_program pos lst orig:((int),(inst))Pmap.map=  ((match lst with
 | [] -> orig
 | h :: t -> store_byte_list_in_program (pos + 1) t (Pmap.add pos (Unknown h) orig)
))

(*val program_content_of_lst : nat -> list inst -> map nat inst*)
let rec program_content_of_lst pos lst:((int),(inst))Pmap.map=  ((match lst with
| [] -> (Pmap.empty compare)
| Stack (PUSH_N bytes) :: rest ->
   store_byte_list_in_program (pos + 1) bytes 
     (Pmap.add pos (Stack (PUSH_N bytes))
          (program_content_of_lst ((pos + 1) + List.length bytes) rest))
| Annotation _  :: rest -> program_content_of_lst pos rest
| i :: rest -> Pmap.add pos i (program_content_of_lst (pos + 1) rest)
))

(*val prepend_annotation : nat -> annotation -> (nat -> list annotation) -> (nat -> list annotation)*)
let prepend_annotation pos annot orig p:(aenv ->bool)list=  (if pos = p then annot :: orig p else orig p)

(*val program_annotation_of_lst : nat -> list inst -> nat -> list annotation*)
let rec program_annotation_of_lst pos lst:int ->(aenv ->bool)list=  ((match lst with
| [] -> (fun _ -> [])
| Annotation annot :: rest -> prepend_annotation pos annot (program_annotation_of_lst pos rest)
| i :: rest -> program_annotation_of_lst (pos + inst_size i) rest
))

(*val program_of_lst : list inst -> program*)
let program_of_lst lst:program=  ({
  program_content = (program_content_of_lst( 0) lst);
  program_length = (List.length lst);
  program_annotation = (program_annotation_of_lst( 0) lst);
})

(*val program_as_memory : program -> memory*)
let program_as_memory p idx:word8=   
 ((match Pmap.lookup (word256ToNat idx) p.program_content with
   | None ->word8FromNumeral 0
   | Some inst1 ->
      (match Lem_list.list_index (inst_code inst1)( 0) with
      | None ->word8FromNumeral 0
      | Some a -> a
      )
   ))

type block_info = {
  block_blockhash : uint -> uint; (* this captures the whole BLOCKHASH operation *)
  block_coinbase : address; (* the miner who validates the block *)
  block_timestamp : uint;
  block_number : uint; (* the blocknumber of the block *)
  block_difficulty : uint;
  block_gaslimit : uint; (* the block gas imit *)
  block_gasprice : uint;
}


type variable_env = {
  venv_stack : uint list;
  venv_memory : memory;
  venv_memory_usage : int; (* the current memory usage *)
  venv_storage : storage;
  venv_pc : int; (* the program counter *)
  venv_balance : address -> uint; (* balances of all accounts *)
  venv_caller : address; (* the caller's address *)
  venv_value_sent : uint; (* the amount of Eth sent along the current invocation *)
  venv_data_sent : byte list; (* the data sent along the current invocation *)
  venv_storage_at_call : storage; (* the storage content at the invocation*)
  venv_balance_at_call : address -> uint; (* the balances at the invocation *)
  venv_origin : address; (* the external account that started the current transaction *)
  venv_ext_program : address -> program; (* the codes of all accounts *)
  venv_block : block_info; (* the current block *)
}

type constant_env = {
  cenv_program : program; (* the code in the account under verification. *)
  cenv_this : address; (* the address of the account under verification. *)
}

type instruction_result =
| InstructionContinue of variable_env (* the execution should continue. *)
| InstructionAnnotationFailure (* the annotation turned out to be false. *)
| InstructionToWorld of contract_action * storage * (address -> uint) *  (variable_env * int * int)option (* the variable environment to return to *)

(*val instruction_failure_result : variable_env -> instruction_result*)
let instruction_failure_result v:instruction_result=  
 (InstructionToWorld( ContractFail, v.venv_storage_at_call, v.venv_balance_at_call, None))

(*val instruction_return_result : list byte -> variable_env -> instruction_result*)
let instruction_return_result x v:instruction_result=  
 (InstructionToWorld( (ContractReturn x), v.venv_storage, v.venv_balance, None))

(*val gas : variable_env -> uint*)
let gas _:word256= (word256FromNumeral 30000)

(*val M : nat -> uint -> uint -> nat*)
let m s f l:int=  
 (if l =word256FromNumeral 0 then s else max s (((word256ToNat f + word256ToNat l) + 31) / 32))

(*val update_balance : address -> (uint -> uint) -> (address -> uint) -> (address -> uint)*)
let update_balance a f orig x:word256=  (if x = a then f (orig a) else orig a)

(*val venv_pop_stack : nat -> variable_env -> variable_env*)
let rec venv_pop_stack n v:variable_env= 
  (
  if(n =  0) then v else
    (let n1 =(Nat_num.nat_monus n ( 1)) in
     (match(n1, v.venv_stack) with
         (_, _ :: tl) -> venv_pop_stack n1 { v with venv_stack = tl }
       | (_,_) -> v
     )))

(*val venv_stack_top : variable_env -> maybe uint*)
let venv_stack_top v:(word256)option=  ((match v.venv_stack with
 | h :: _ -> Some h
 | [] -> None
))

(*val venv_update_storage : uint -> uint-> variable_env -> variable_env*)
let venv_update_storage idx vall v:variable_env=  
 ({ v with venv_storage = (fun x -> if x = idx then vall else v.venv_storage x) })

(*val venv_next_instruction : variable_env -> constant_env -> maybe inst*)
let venv_next_instruction v c:(inst)option=   
 (Pmap.lookup v.venv_pc c.cenv_program.program_content)

(*val venv_advance_pc : constant_env -> variable_env -> variable_env*)
let venv_advance_pc c v:variable_env=  ((match venv_next_instruction v c with
 | None -> { v with venv_pc = (v.venv_pc + 1) }
 | Some inst1 -> { v with venv_pc = (v.venv_pc + inst_size inst1) }
))

(*val stack_0_0_op : variable_env -> constant_env -> instruction_result*)
let stack_0_0_op v c:instruction_result=  (InstructionContinue (venv_advance_pc c v))

(*val stack_0_1_op : variable_env -> constant_env -> uint -> instruction_result*)
let stack_0_1_op v c w:instruction_result=   
 (InstructionContinue (venv_advance_pc c { v with venv_stack = (w :: v.venv_stack) }))


(*val stack_1_1_op : variable_env -> constant_env -> (uint -> uint) -> instruction_result*)
let stack_1_1_op v c f:instruction_result=  ((match v.venv_stack with
  | [] -> instruction_failure_result v
  | h :: t -> InstructionContinue (venv_advance_pc c { v with venv_stack = (f h :: t) })
))

(*val stack_1_2_op : variable_env -> constant_env -> (uint -> uint * uint) -> instruction_result*)
let stack_1_2_op v c f:instruction_result=  ((match v.venv_stack with
 | [] -> instruction_failure_result v
 | h :: t ->
     let (new0, new1) = (f h) in
     InstructionContinue (venv_advance_pc c { v with venv_stack = (new0 :: (new1 :: t)) })
))

(*val stack_2_1_op : variable_env -> constant_env -> (uint -> uint -> uint) -> instruction_result*)
let stack_2_1_op v c f:instruction_result=  ((match v.venv_stack with
 | operand0 :: operand1 :: rest ->
       InstructionContinue
         (venv_advance_pc c { v with venv_stack = (f operand0 operand1 :: rest) })
  | _ -> instruction_failure_result v
))

(*val stack_3_1_op : variable_env -> constant_env -> (uint -> uint -> uint -> uint) -> instruction_result*)
let stack_3_1_op v c f:instruction_result=  ((match v.venv_stack with
 | operand0 :: operand1 :: operand2 :: rest ->
       InstructionContinue
         (venv_advance_pc c { v with venv_stack = (f operand0 operand1 operand2 :: rest) })
 | _ -> instruction_failure_result v
))

(*val sstore : variable_env -> constant_env -> instruction_result*)
let sstore v c:instruction_result=  ((match v.venv_stack with
 | addr :: vl :: stack_tail ->
      InstructionContinue (venv_advance_pc c
        (venv_update_storage addr vl { v with venv_stack = stack_tail }))
 | _ -> instruction_failure_result v
))

(*val build_aenv : variable_env -> constant_env -> aenv*)
let build_aenv v c:aenv=  ({
  aenv_stack = (v.venv_stack);
  aenv_memory = (v.venv_memory);
  aenv_storage = (v.venv_storage);
  aenv_balance = (v.venv_balance);
  aenv_caller = (v.venv_caller);
  aenv_value_sent = (v.venv_value_sent);
  aenv_data_sent = (v.venv_data_sent);
  aenv_storage_at_call = (v.venv_storage_at_call);
  aenv_balance_at_call = (v.venv_balance_at_call);
  aenv_this = (c.cenv_this);
  aenv_origin = (v.venv_origin);
})

(*val eval_annotation : annotation -> variable_env -> constant_env -> instruction_result*)
let eval_annotation anno v c:instruction_result=   
 (if anno (build_aenv v c) then InstructionContinue (venv_advance_pc c v)
    else InstructionAnnotationFailure)

(*val jump : variable_env -> constant_env -> instruction_result*)
let jump v c:instruction_result=  ((match v.venv_stack with
 | [] -> instruction_failure_result v
 | pos :: tl ->
     let v_new = ({ v with venv_stack = tl; venv_pc = (word256ToNat pos) }) in
     (match venv_next_instruction v_new c with
      | Some (Pc JUMPDEST) -> InstructionContinue v_new
      | _ -> instruction_failure_result v
     )
))

(*val blockedInstructionContinue : variable_env -> bool -> instruction_result*)
let blockedInstructionContinue v _:instruction_result=  (InstructionContinue v)

(*val blocked_jump : variable_env -> constant_env -> bool -> instruction_result*)
let blocked_jump v c _:instruction_result=  (jump v c)

(*val strict_if : forall 'a. bool -> (bool -> 'a) -> (bool -> 'a) -> 'a*)
let strict_if b x y:'a=  (if b then x true else y true)

(*val jumpi : variable_env -> constant_env -> instruction_result*)
let jumpi v c:instruction_result=  ((match v.venv_stack with
 | pos :: cond :: rest ->
    let new_env = ({ v with venv_stack = (pos :: rest) }) in
    strict_if (cond =word256FromNumeral 0)
           (blockedInstructionContinue (venv_advance_pc c (venv_pop_stack( 2) v)))
           (blocked_jump new_env c)
 | _ -> instruction_failure_result v
))

(*val datasize : variable_env -> uint*)
let datasize v:word256=  (word256FromNat (List.length v.venv_data_sent))

(*val word_of_bytes : list byte -> uint*)
let word_of_bytes lst:word256=  (word256FromBoollist (List.concat (map boolListFromWord8 lst)))

(*val address_of_bytes : list byte -> address*)
let address_of_bytes lst:word160=  (word160FromBoollist (List.concat (map boolListFromWord8 lst)))

(*val read_word_from_bytes : nat -> list byte -> uint*)
let read_word_from_bytes idx lst:word256=  (word_of_bytes (take( 32) (drop idx lst)))

(*val cut_data : variable_env -> uint -> uint*)
let cut_data v idx:word256=  (read_word_from_bytes (word256ToNat idx) v.venv_data_sent)

(*val cut_memory : uint -> nat -> (uint -> byte) -> list byte*)
let rec cut_memory idx n memory1:(word8)list= 
  (
  if(n =  0) then ([]) else
    (let n0 =(Nat_num.nat_monus n ( 1)) in
     memory1 idx ::
       cut_memory ( word256Add idx (word256FromNumeral 1)) n0 memory1))

(*val call : variable_env -> constant_env -> instruction_result*)
let call v c:instruction_result=  ((match v.venv_stack with
 | e0 :: e1 :: e2 :: e3 :: e4 :: e5 :: e6 :: rest ->
     if w256Less (v.venv_balance c.cenv_this) e2 then instruction_failure_result v
     else
       InstructionToWorld( (ContractCall
         { callarg_gas = e0;
            callarg_code = (uint_to_address e1);
            callarg_recipient = (uint_to_address e1);
            callarg_value = e2;
            callarg_data = (cut_memory e3 (word256ToNat e4) v.venv_memory);
            callarg_output_begin = e5;
            callarg_output_size = e6 }),
        v.venv_storage,
        (update_balance c.cenv_this (fun orig -> word256Minus orig e2) v.venv_balance),
        (Some (* saving the variable environment for timing *)
          ({ (venv_advance_pc c v) with
           venv_stack = rest;
           venv_balance = (update_balance c.cenv_this (fun orig -> word256Minus orig e2) v.venv_balance);
           venv_memory_usage = (m (m v.venv_memory_usage e3 e4) e5 e6) }, absnat e5, absnat e6)))
  | _ -> instruction_failure_result v
))

(*val delegatecall : variable_env -> constant_env -> instruction_result*)
let delegatecall v c:instruction_result=  ((match v.venv_stack with
 | e0 :: e1 :: e3 :: e4 :: e5 :: e6 :: rest ->
    if w256Less (v.venv_balance c.cenv_this) v.venv_value_sent then instruction_failure_result v
     else
       InstructionToWorld(
         (ContractCall
           { callarg_gas = e0;
              callarg_code = (uint_to_address e1);
              callarg_recipient = (uint_to_address e1);
              callarg_value = (v.venv_value_sent);
              callarg_data = (cut_memory e3 (word256ToNat e4) v.venv_memory);
              callarg_output_begin = e5;
              callarg_output_size = e6 }),
          v.venv_storage, v.venv_balance,
          (Some (* save the variable environment for returns *)
            ({ (venv_advance_pc c v) with venv_stack = rest; venv_memory_usage = (m (m v.venv_memory_usage e3 e4) e5 e6) }, absnat e5, absnat e6)))
  | _ -> instruction_failure_result v
))

(*val callcode : variable_env -> constant_env -> instruction_result*)
let callcode v c:instruction_result=  ((match v.venv_stack with
 | e0 :: e1 :: e2 :: e3 :: e4 :: e5 :: e6 :: rest ->
    if w256Less (v.venv_balance c.cenv_this) e2 then
       instruction_failure_result v
     else
       InstructionToWorld(
         (ContractCall
           { callarg_gas = e0;
              callarg_code = (uint_to_address e1);
              callarg_recipient = (c.cenv_this);
              callarg_value = e2;
              callarg_data = (cut_memory e3 (word256ToNat e4) v.venv_memory);
              callarg_output_begin = e5;
              callarg_output_size = e6 }),
          v.venv_storage,
          (update_balance c.cenv_this (fun orig -> word256Minus orig e2) v.venv_balance),
          (Some (* saving the variable environment *)
            ({ (venv_advance_pc c v) with
                  venv_stack = rest;
                  venv_memory_usage = (m (m v.venv_memory_usage e3 e4) e5 e6);
                  venv_balance = (update_balance c.cenv_this (fun orig -> word256Minus orig e2) v.venv_balance) }, absnat e5, absnat e6)))
  | _ -> instruction_failure_result v
))

(*val create : variable_env -> constant_env -> instruction_result*)
let create v c:instruction_result=  ((match v.venv_stack with
  | vl :: code_start :: code_len :: rest ->
      if w256Less (v.venv_balance c.cenv_this) vl then instruction_failure_result v else
      let code = (cut_memory code_start (word256ToNat code_len) v.venv_memory) in
      let new_balance = (update_balance c.cenv_this (fun orig -> word256Minus orig vl) v.venv_balance) in
      InstructionToWorld(
           (ContractCreate
             { createarg_value = vl; createarg_code = code }),
            v.venv_storage, new_balance,
            (Some (* when returning to this invocation, use the following variable environment *)
              ({ (venv_advance_pc c v) with venv_stack = rest;
                 venv_balance = new_balance;
                 venv_memory_usage = (m v.venv_memory_usage code_start code_len) }, 0, 0)))
  | _ -> instruction_failure_result v
))

let venv_returned_bytes v:(word8)list=  ((match v.venv_stack with
 | e0 :: e1 :: _ -> cut_memory e0 (word256ToNat e1) v.venv_memory
 | _ -> []
))

(*val ret : variable_env -> constant_env -> instruction_result*)
let ret v _:instruction_result=   ((match v.venv_stack with
 | e0 :: e1 :: _ ->
     let new_v = ({ v with venv_memory_usage = (m v.venv_memory_usage e0 e1) }) in
     InstructionToWorld( (ContractReturn (venv_returned_bytes new_v)),
                           v.venv_storage, v.venv_balance,
                           None) (* No possibility of ever returning to this invocation. *)
 | _ -> instruction_failure_result v
))

(*val stop : variable_env -> constant_env -> instruction_result*)
let stop v _:instruction_result=  (InstructionToWorld( (ContractReturn []), v.venv_storage, v.venv_balance, None))

(*val pop : variable_env -> constant_env -> instruction_result*)
let pop v c:instruction_result=  ((match v.venv_stack with
 | _ :: tl -> InstructionContinue (venv_advance_pc c { v with venv_stack = tl })
 | [] -> InstructionContinue (venv_advance_pc c v)
))

(*val general_dup : nat -> variable_env -> constant_env -> instruction_result*)
let general_dup n v c:instruction_result=  ((match Lem_list.list_index v.venv_stack ( Nat_num.nat_monus n( 1)) with
  | None -> instruction_failure_result v
  | Some duplicated -> InstructionContinue (venv_advance_pc c { v with venv_stack = (duplicated :: v.venv_stack) })
))

(*val store_byte_list_memory : uint -> list byte -> memory -> memory*)
let rec store_byte_list_memory pos lst orig:word256 ->word8=  ((match lst with
 | [] -> orig
 | h :: t ->
     store_byte_list_memory ( word256Add pos(word256FromNumeral 1)) t (fun p -> if pos = p then h else orig p)
))

(*val store_word_memory : uint -> uint -> memory -> memory*)
let store_word_memory pos vl mem:uint ->byte=   
 (store_byte_list_memory pos (word_rsplit vl) mem)

(*val mstore : variable_env -> constant_env -> instruction_result*)
let mstore v c:instruction_result=  ((match v.venv_stack with
  | pos :: vl :: rest ->
       let new_memory = (store_word_memory pos vl v.venv_memory) in
       InstructionContinue (venv_advance_pc c
         { v with venv_stack = rest; venv_memory = new_memory;
           venv_memory_usage = (m v.venv_memory_usage pos(word256FromNumeral 32))
          })
  | _ -> instruction_failure_result v
))

(*val mload : variable_env -> constant_env -> instruction_result*)
let mload v c:instruction_result=  ((match v.venv_stack with
 | pos :: rest ->
      let value = (read_word_from_bytes( 0) (cut_memory pos( 32) v.venv_memory)) in
      InstructionContinue (venv_advance_pc c { v with venv_stack = (value :: rest); venv_memory_usage = (m v.venv_memory_usage pos(word256FromNumeral 32)) })
 | _ -> instruction_failure_result v
))

(*val mstore8 : variable_env -> constant_env -> instruction_result*)
let mstore8 v c:instruction_result=  ((match v.venv_stack with
 | pos :: vl :: rest ->
   let new_memory = (fun p -> if p = pos then uint_to_byte vl else v.venv_memory p) in
   InstructionContinue (venv_advance_pc c
          { v with venv_stack = rest; venv_memory_usage = (m v.venv_memory_usage pos(word256FromNumeral 8));
                    venv_memory = new_memory })
 | _ -> instruction_failure_result v
))

(*val input_as_memory : list byte -> memory*)
let input_as_memory lst idx:word8=  ((match Lem_list.list_index lst (absnat idx) with
 | None ->word8FromNumeral 0
 | Some a -> a
))

(*val calldatacopy : variable_env -> constant_env -> instruction_result*)
let calldatacopy v c:instruction_result=  ((match v.venv_stack with
 | dst_start :: src_start :: len :: rest ->
       let data = (cut_memory src_start (absnat len) (input_as_memory v.venv_data_sent)) in
       let new_memory = (store_byte_list_memory dst_start data v.venv_memory) in
       InstructionContinue (venv_advance_pc c
         { v with venv_stack = rest; venv_memory = new_memory;
            venv_memory_usage = (m v.venv_memory_usage dst_start len) })
 | _ -> instruction_failure_result v
))

(*val codecopy : variable_env -> constant_env -> instruction_result*)
let codecopy v c:instruction_result=  ((match v.venv_stack with
 | dst_start :: src_start :: len :: rest ->
     let data = (cut_memory src_start (absnat len)
                  (program_as_memory c.cenv_program)) in
     let new_memory = (store_byte_list_memory dst_start data v.venv_memory) in
     InstructionContinue (venv_advance_pc c
       { v with venv_stack = rest; venv_memory = new_memory;
                 venv_memory_usage = (m v.venv_memory_usage dst_start len) })
 | _ -> instruction_failure_result v
))

(*val extcodecopy : variable_env -> constant_env -> instruction_result*)
let extcodecopy v c:instruction_result=  ((match v.venv_stack with
 | addr :: dst_start :: src_start :: len :: rest ->
     let data = (cut_memory src_start (absnat len)
                  (program_as_memory
                    (v.venv_ext_program (uint_to_address addr)))) in
     let new_memory = (store_byte_list_memory dst_start data v.venv_memory) in
     InstructionContinue (venv_advance_pc c
       { v with venv_stack = rest; venv_memory = new_memory;
                 venv_memory_usage = (m v.venv_memory_usage dst_start len) })
 | _ -> instruction_failure_result v
))

(*val pc : variable_env -> constant_env -> instruction_result*)
let pc v c:instruction_result=   
 (InstructionContinue (venv_advance_pc c
     { v with venv_stack = (word256FromNat v.venv_pc :: v.venv_stack)}))

(*val log : nat -> variable_env -> constant_env -> instruction_result*)
let log n v c:instruction_result=   
 (InstructionContinue (venv_advance_pc c (venv_pop_stack (n+ 2) v)))

(*val list_swap : forall 'a. nat -> list 'a -> maybe (list 'a)*)
let list_swap n lst:('a list)option=  ((match (list_index lst n, list_index lst( 0)) with
 | (Some n_th, Some first) -> Some (List.concat [[n_th]; take ( Nat_num.nat_monus n( 1)) (drop( 1) lst); [first]; drop ( 1 + n) lst])
 | _ -> None
))

(*val swap : nat -> variable_env -> constant_env -> instruction_result*)
let swap n v c:instruction_result=  ((match list_swap n v.venv_stack with
 | None -> instruction_failure_result v
 | Some new_stack -> InstructionContinue (venv_advance_pc c { v with venv_stack = new_stack })
))

(*val sha3 : variable_env -> constant_env -> instruction_result*)
let sha3 v c:instruction_result=  ((match v.venv_stack with
 | start :: len :: rest ->
      InstructionContinue (
        venv_advance_pc c { v with venv_stack = (keccac (cut_memory start (word256ToNat len) v.venv_memory) :: rest);
                                    venv_memory_usage = (m v.venv_memory_usage start len) })
 | _ -> instruction_failure_result v
))

(*val suicide : variable_env -> constant_env -> instruction_result*)
let suicide v c:instruction_result=  ((match v.venv_stack with
 | dst :: _ ->
     let new_balance addr=        
 (if addr = c.cenv_this then word256FromNumeral 0 else
        if addr = uint_to_address dst then word256Add (v.venv_balance c.cenv_this) (v.venv_balance addr) else 
        v.venv_balance addr) in
     InstructionToWorld( ContractSuicide, v.venv_storage, new_balance, None)
 | _ -> instruction_failure_result v
))

(*val instruction_sem : variable_env -> constant_env -> inst -> instruction_result*)
let instruction_sem v c inst1:instruction_result=  ((match inst1 with
| Stack (PUSH_N lst) -> stack_0_1_op v c (word_of_bytes lst)
| Unknown _ -> instruction_failure_result v
| Storage SLOAD -> stack_1_1_op v c v.venv_storage
| Storage SSTORE -> sstore v c
| Pc JUMPI -> jumpi v c
| Pc JUMP -> jump v c
| Pc JUMPDEST -> stack_0_0_op v c
| Info CALLDATASIZE -> stack_0_1_op v c (datasize v)
| Stack CALLDATALOAD -> stack_1_1_op v c (cut_data v)
| Info CALLER -> stack_0_1_op v c (address_to_uint v.venv_caller)
| Arith ADD -> stack_2_1_op v c (fun a b -> word256Add a b)
| Arith SUB -> stack_2_1_op v c (fun a b -> word256Minus a b)
| Arith ISZERO -> stack_1_1_op v c (fun a -> if a =word256FromNumeral 0 then word256FromNumeral 1 else word256FromNumeral 0)
| Misc CALL -> call v c
| Misc RETURN -> ret v c
| Misc STOP -> stop v c
| Dup n -> general_dup (word8ToNat n) v c
| Stack POP -> pop v c
| Info GASLIMIT -> stack_0_1_op v c v.venv_block.block_gaslimit
| Arith Inst_GT -> stack_2_1_op v c (fun a b -> if word256UGT a b then word256FromNumeral 1 else word256FromNumeral 0)
| Arith Inst_EQ -> stack_2_1_op v c (fun a b -> if a = b then word256FromNumeral 1 else word256FromNumeral 0)
| Annotation a -> eval_annotation a v c
| Bits Inst_AND -> stack_2_1_op v c (fun a b -> word256Land a b)
| Bits Inst_OR -> stack_2_1_op v c (fun a b -> word256Lor a b)
| Bits Inst_XOR -> stack_2_1_op v c (fun a b -> word256Lxor a b)
| Bits Inst_NOT -> stack_1_1_op v c (fun a -> word256Negate a)
| Bits BYTE ->
    stack_2_1_op v c get_byte
| Sarith SDIV -> stack_2_1_op v c
     (fun n divisor -> if divisor =word256FromNumeral 0 then word256FromNumeral 0 else
                        word256FromInt ( Nat_num.int_div(sintFromW256 n) (sintFromW256 divisor)))
| Sarith SMOD -> stack_2_1_op v c
     (fun n divisor -> if divisor =word256FromNumeral 0 then word256FromNumeral 0 else
                       word256FromInt ( Nat_num.int_mod(sintFromW256 n) (sintFromW256 divisor)))
| Sarith SGT -> stack_2_1_op v c
     (fun elm0 elm1 -> if w256Greater elm0 elm1 then word256FromNumeral 1 else word256FromNumeral 0)
| Sarith SLT -> stack_2_1_op v c
     (fun elm0 elm1 -> if w256Less elm0 elm1 then word256FromNumeral 1 else word256FromNumeral 0)
| Sarith SIGNEXTEND -> stack_2_1_op v c
     (fun len orig ->
        uint_of_bl (Lem_list.map (fun i ->
          if i <=( 256 -( 8 * (uint len + 1)))
          then test_bit orig (abs ( 256 -( 8 * (uint len + 1))))
          else test_bit orig (abs i)
        ) (Lem_list.genlist (fun x -> x)( 256)))
     )
| Arith MUL -> stack_2_1_op v c
     (fun a b -> word256Mult a b)
| Arith DIV -> stack_2_1_op v c
     (fun a divisor -> (if divisor =word256FromNumeral 0 then word256FromNumeral 0 else word256IntegerDivision a divisor))
| Arith MOD -> stack_2_1_op v c
     (fun a divisor -> (if divisor =word256FromNumeral 0 then word256FromNumeral 0 else word256Remainder a divisor))
| Arith ADDMOD -> stack_3_1_op v c
     (fun a b divisor ->
         (if divisor =word256FromNumeral 0 then word256FromNumeral 0 else word256Remainder ( word256Add a b) divisor))
| Arith MULMOD -> stack_3_1_op v c
     (fun a b divisor ->
         (if divisor =word256FromNumeral 0 then word256FromNumeral 0 else word256Remainder ( word256Mult a b) divisor))
| Arith EXP -> stack_2_1_op v c (fun a exponent -> word256FromInt ( intPow(uint a) (word256ToNat exponent)))
| Arith Inst_LT -> stack_2_1_op v c (fun arg0 arg1 -> if w256Less arg0 arg1 then word256FromNumeral 1 else word256FromNumeral 0)
| Arith SHA3 -> sha3 v c
| Info ADDRESS -> stack_0_1_op v c (address_to_uint c.cenv_this)
| Info BALANCE -> stack_1_1_op v c (fun addr -> v.venv_balance (uint_to_address addr))
| Info ORIGIN -> stack_0_1_op v c (address_to_uint v.venv_origin)
| Info CALLVALUE -> stack_0_1_op v c v.venv_value_sent
| Info CODESIZE -> stack_0_1_op v c (word256FromNat c.cenv_program.program_length)
| Info GASPRICE -> stack_0_1_op v c v.venv_block.block_gasprice
| Info EXTCODESIZE -> stack_1_1_op v c
     (fun arg -> word256FromNat (v.venv_ext_program (uint_to_address arg)).program_length)
| Info BLOCKHASH -> stack_1_1_op v c v.venv_block.block_blockhash
| Info COINBASE -> stack_0_1_op v c (address_to_uint v.venv_block.block_coinbase)
| Info TIMESTAMP -> stack_0_1_op v c v.venv_block.block_timestamp
| Info NUMBER -> stack_0_1_op v c v.venv_block.block_number
| Info DIFFICULTY -> stack_0_1_op v c v.venv_block.block_difficulty
| Memory MLOAD -> mload v c
| Memory MSTORE -> mstore v c
| Memory MSTORE8 -> mstore8 v c
| Memory CALLDATACOPY -> calldatacopy v c
| Memory CODECOPY -> codecopy v c
| Memory EXTCODECOPY -> extcodecopy v c
| Pc PC -> pc v c
| Log LOG0 -> log( 0) v c
| Log LOG1 -> log( 1) v c
| Log LOG2 -> log( 2) v c
| Log LOG3 -> log( 3) v c
| Log LOG4 -> log( 4) v c
| Swap n -> swap (word8ToNat n) v c
| Misc CREATE -> create v c
| Misc CALLCODE -> callcode v c
| Misc SUICIDE -> suicide v c
| Misc DELEGATECALL -> delegatecall v c
| Info GAS -> stack_0_1_op v c (gas v)
| Memory MSIZE -> stack_0_1_op v c (word256FromNat v.venv_memory_usage)
))

type program_result =
| ProgramStepRunOut
| ProgramToWorld of contract_action * storage * (address -> uint) *  (variable_env * int * int)option
| ProgramInvalid
| ProgramAnnotationFailure
| ProgramInit of call_env

(*val check_annotations : variable_env -> constant_env -> bool*)
let check_annotations v c:bool=  
 (let annots = (c.cenv_program.program_annotation v.venv_pc) in
  List.for_all (fun annot -> annot (build_aenv v c)) annots)

(*val program_sem : variable_env -> constant_env -> nat -> nat -> program_result*)
(*val blocked_program_sem : variable_env -> constant_env -> nat -> nat -> bool -> program_result*)

let rec program_sem v c tiny_step remaining_steps:program_result= 
  (
  if(remaining_steps =  0) then ProgramStepRunOut else
    (let remaining_steps0 =(Nat_num.nat_monus remaining_steps ( 1)) in
     if tiny_step <=  0 then
       ProgramToWorld ( ContractFail , v.venv_storage_at_call ,
         v.venv_balance_at_call , None ) else
       if not (check_annotations v c) then ProgramAnnotationFailure else
         (match venv_next_instruction v c with
               | None -> ProgramStepRunOut
           | Some i ->
         (match instruction_sem v c i with
               | InstructionContinue new_v ->
         (strict_if (new_v.venv_pc > v.venv_pc)
            (blocked_program_sem new_v c ( Nat_num.nat_monus tiny_step ( 1))
               (remaining_steps0 +  1))
            (blocked_program_sem new_v c c.cenv_program.program_length
               remaining_steps0))
           | InstructionToWorld ( a , st , bal , opt_pushed_v ) -> ProgramToWorld
                                                                    ( 
                                                                   a , 
                                                                   st , 
                                                                   bal ,
                                                                    opt_pushed_v
                                                                    )
           | _ -> ProgramInvalid
         )
         )))
and blocked_program_sem v c l p _:program_result=  (program_sem v c l p)

(*val program_sem_blocked : variable_env -> constant_env -> nat -> nat -> bool -> program_result*)

let program_sem_blocked v c internal externl _ : program_result =  (program_sem v c internal externl)

type account_state = {
  account_address : address;
  account_storage : storage;
  account_code : program;
  account_balance : uint;
  account_ongoing_calls : (variable_env * int * int) list;
  account_killed : bool;
}

(*val build_cenv : account_state -> constant_env*)
let build_cenv a:constant_env=  
 ({ cenv_program = (a.account_code); cenv_this = (a.account_address) })

(*val is_call_like : maybe inst -> bool*)
let is_call_like i:bool=  ( (Lem.option_equal (=)i (Some (Misc CALL))) || ((Lem.option_equal (=) i (Some (Misc DELEGATECALL))) 
                 || ((Lem.option_equal (=) i (Some (Misc CALLCODE))) || (Lem.option_equal (=) i (Some (Misc CREATE))))))

(*val build_venv_failed : account_state -> maybe variable_env*)
let build_venv_failed a:(variable_env)option=  ((match a.account_ongoing_calls with
 | [] -> None
 | (recovered,_,_) :: _ ->
      if is_call_like (Pmap.lookup ( Nat_num.nat_monus recovered.venv_pc( 1)) a.account_code.program_content) then
      Some ({ recovered with venv_stack =(word256FromNumeral 0 :: recovered.venv_stack) }) (* 0 is pushed, indicating failure*)
      else None
))

(*val account_state_pop_ongoing_call : account_state -> account_state*)
let account_state_pop_ongoing_call orig:account_state=  ((match orig.account_ongoing_calls with
 | _ :: tl -> { orig with account_ongoing_calls = tl }
 | _ -> { orig with account_ongoing_calls = ([]) }
))

(*val empty_program : program*)
let empty_program:program=  ({
  program_content = (Pmap.empty compare);
  program_length =( 0);
  program_annotation = (fun _ -> [])
})

(*val empty_account : address -> account_state*)
let empty_account addr:account_state= 
 ({ account_address = addr;
    account_storage = empty_storage;
   account_code = empty_program;
   account_balance =(word256FromNumeral 0);
   account_ongoing_calls = ([]);
   account_killed = false;
 })

(*val update_account_state : account_state -> contract_action -> storage -> (address -> uint) -> maybe (variable_env*nat*nat) -> account_state*)
let update_account_state prev act st bal v_opt:account_state=   
 ({ prev with 
     account_storage = st;
     account_balance = ((match act with ContractFail -> prev.account_balance
                                   |  _ -> bal prev.account_address ));
     account_ongoing_calls =
                        ((match v_opt with None -> prev.account_ongoing_calls
                                     | Some pushed -> pushed :: prev.account_ongoing_calls ));
     account_killed =
       ((match act with ContractSuicide -> true
                  | _ -> prev.account_killed ))
    })

type contract_behavior = contract_action * (account_state -> bool)

type response_to_world = {
  when_called : call_env -> contract_behavior;
  when_returned : return_result -> contract_behavior;
  when_failed : contract_behavior;
}

(*val empty_memory : memory*)
let empty_memory:word256 ->word8=  (fun _ ->word8FromNumeral 0)

(*indreln [build_venv_called : account_state -> call_env -> variable_env -> bool]
  venv_called : forall bal a env origin ext block.
    (Instance_Basic_classes_Eq_var.=) (bal a.account_address) (a.account_balance) ==>
    build_venv_called a env
 <| venv_stack = []; (* The stack is initialized for every invocation *)
    venv_memory = empty_memory; (* The memory is also initialized for every invocation *)
     venv_memory_usage = 0; (* The memory usage is initialized. *)
     venv_storage = a.account_storage; (* The storage is taken from the account state *)
     venv_pc = 0; (* The program counter is initialized to zero *)
     venv_balance = (fun (addr:address) -> if (Instance_Basic_classes_Eq_var.=) addr (a.account_address) then (Instance_Num_NumAdd_Word256_word256.+) (bal a.account_address) (env.callenv_value) else bal addr); 
                        (* The balance is arbitrary, except that the balance of this account
                           is as specified in the account state plus the sent amount. *)
     venv_caller = env.callenv_caller; (* the caller is specified by the world *)
     venv_value_sent = env.callenv_value; (* the sent value is specified by the world *)
     venv_data_sent = env.callenv_data; (* the sent data is specified by the world *)
     venv_storage_at_call = a.account_storage; (* the snapshot of the storage is remembered in case of failure *)
     venv_balance_at_call = bal; (* the snapshot of the balance is remembered in case of failure *)
     venv_origin = origin; (* the origin of the transaction is arbitrarily chosen *)
     venv_ext_program = ext; (* the codes of the external programs are arbitrary. *)
     venv_block = block; (* the block information is chosen arbitrarily. *)
   |>*)

(*val put_return_values : memory -> list byte -> nat -> nat -> memory*)
let rec put_return_values orig lst b s:word256 ->word8=  
 (if s <= 0 then orig else
  (match lst with
  | [] -> orig
  | h :: t -> put_return_values (fun addr -> if addr = word256FromNat b then h else orig addr) t (b + 1) ( Nat_num.nat_monus s( 1))
  ))

(*indreln [build_venv_returned : account_state -> return_result -> variable_env -> bool]
venv_returned:
  forall new_bal a_bal a_code v_pc a_addr a_storage v_stack v_memory v_memory_usage v_storage v_balance v_caller v_value v_data v_init_storage v_init_balance
         v_origin v_ext_program v_block mem_start mem_size  a_ongoing_rest a_killed r.
  is_call_like (Map.lookup ((Instance_Num_NumMinus_nat.-) v_pc 1) a_code.program_content) &&
  (Instance_Basic_classes_Ord_Word256_word256.>=) new_bal a_bal ==> (* the balance might have increased from the account state *)
  build_venv_returned
     <| account_address = a_addr;
       account_storage = a_storage;
       account_code = a_code;
       account_balance = a_bal;
       account_ongoing_calls =
         (<| venv_stack = v_stack;
          venv_memory = v_memory;
          venv_memory_usage = v_memory_usage;
          venv_storage = v_storage;
          venv_pc = v_pc;
          venv_balance = v_balance;
          venv_caller = v_caller;
          venv_value_sent = v_value;
          venv_data_sent = v_data;
          venv_storage_at_call = v_init_storage;
          venv_balance_at_call = v_init_balance;
          venv_origin = v_origin;
          venv_ext_program = v_ext_program;
          venv_block = v_block;
         |>, mem_start, mem_size) :: a_ongoing_rest;
       account_killed = a_killed
     |>
     r
     <|  venv_stack = 1 :: v_stack; (* 1 is pushed, indicating a return *)
        venv_memory = put_return_values v_memory r.return_data mem_start mem_size;
        venv_memory_usage = v_memory_usage;
        venv_storage = a_storage;
        venv_pc = v_pc;
        venv_balance = (update_balance a_addr
                            (fun _ -> new_bal) r.return_balance);
        venv_caller = v_caller;
        venv_value_sent = v_value;
        venv_data_sent = v_data;
        venv_storage_at_call = v_init_storage;
        venv_balance_at_call = v_init_balance;
        venv_origin = v_origin;
        venv_ext_program = v_ext_program;
        venv_block = v_block;
     |>*)
(*
val respond_to_call_correctly : (call_env -> contract_behavior) -> account_state -> bool
let respond_to_call_correctly c a =
  (forall call_env initial_venv resulting_action final_state_pred.
     build_venv_called a call_env initial_venv -->
         (* The specification says the execution should result in these *)
         c call_env = (resulting_action, final_state_pred) -->
         (forall steps. (* and for any number of steps *)
           ( let r = program_sem initial_venv (build_cenv a) a.account_code.program_length steps in
             (* either more steps are necessary, or *)
             r = ProgramStepRunOut ||
             (* the result matches the specification *)
             (exists pushed_venv st bal.
              r = ProgramToWorld resulting_action st bal pushed_venv &&
              final_state_pred
                (update_account_state a resulting_action st bal pushed_venv))
           )))

val respond_to_return_correctly : (return_result -> contract_behavior) -> account_state -> bool
let respond_to_return_correctly r a =
   (forall rr initial_venv final_state_pred resulting_action.
       build_venv_returned a rr initial_venv -->
       r rr = (resulting_action, final_state_pred) -->
       (forall steps.
          (let r = program_sem initial_venv (build_cenv a) a.account_code.program_length steps in
           r = ProgramStepRunOut ||
           (exists pushed_venv st bal.
            r = ProgramToWorld resulting_action st bal pushed_venv &&
            final_state_pred
              (update_account_state (account_state_pop_ongoing_call a) resulting_action st bal pushed_venv))
          )))

val respond_to_fail_correctly : contract_behavior -> account_state -> bool
let respond_to_fail_correctly f a =
   (forall initial_venv final_state_pred resulting_action.
      Just initial_venv = build_venv_failed a -->
      f = (resulting_action, final_state_pred) -->
      (forall steps.
        ( let r = program_sem initial_venv (build_cenv a) a.account_code.program_length steps in
          r = ProgramStepRunOut ||
          (exists pushed_venv st bal.
             r = ProgramToWorld resulting_action st bal pushed_venv &&
             final_state_pred (update_account_state (account_state_pop_ongoing_call a) resulting_action st bal pushed_venv)))))

indreln [account_state_responds_to_world : (account_state -> bool) -> response_to_world -> bool]
AccountStep: forall precond c r f.
  (forall a. precond a --> respond_to_call_correctly c a) &&
   (forall a. precond a --> respond_to_return_correctly r a) &&
   (forall a. precond a --> respond_to_fail_correctly f a) ==>
   account_state_responds_to_world precond <| when_called = c; when_returned = r; when_failed = f |>

*)