evm.lem

(*                                                                          *)
(* Copyright 2016 Sami Mäkelä                                               *)
(* Copyright 2016 Yoichi Hirai                                              *)
(*                                                                          *)
(* 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 List
open import Word
open import Word256
open import Word160
open import Word8
open import Word4
open import Keccak

type w8 = word8
(* The frequently used machine word types are named here.  For example, address *)
(* is the type of 160-bit machine words.  The type w256 is the type of EVM machine words. *)

type address = word160

val sintFromW256 : w256 -> integer
let sintFromW256 = word256ToInteger

val uint : w256 -> integer
let uint w = integerFromNatural (word256ToNatural w)
declare isabelle target_rep function uint = `Word.uint`

val uintFromW8 : w8 -> integer
let uintFromW8 w = integerFromNatural (word8ToNatural w)
declare isabelle target_rep function uintFromW8 = `Word.uint`

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

val absnat : w256 -> nat
let absnat w = natFromInteger (word256ToInteger w)

val byteFromNat : nat -> byte
let byteFromNat = word8FromNat

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

val w256_of_bl : list bool -> w256
let w256_of_bl = word256FromBoollist

val w256_to_address : w256 -> address
let w256_to_address w = word160FromNatural (word256ToNatural w)
declare isabelle target_rep function w256_to_address = `Word.ucast`

val address_to_w256 : address -> w256
let address_to_w256 w = word256FromNatural (word160ToNatural w)
declare isabelle target_rep function address_to_w256 = `Word.ucast`

val w256_to_byte : w256 -> byte
let w256_to_byte w = word8FromNatural (word256ToNatural w)
declare isabelle target_rep function w256_to_byte = `Word.ucast`

val byte_to_w256 : byte -> w256
let byte_to_w256 w = word256FromNat (word8ToNat w)
declare isabelle target_rep function byte_to_w256 = `Word.ucast`

val word_rsplit256 : w256 -> list byte
let word_rsplit256 w = (word_rsplit_aux (boolListFromWord256 w) 32)
declare isabelle target_rep function word_rsplit256 = `word_rsplit`

val get_byte : w256 -> w256 -> w256
let get_byte position w =
  if uint position >= 32 then 0 else
  match List.index (word_rsplit256 w) (natFromInteger (uint position)) with
  | Nothing -> 0
  | Just (a:byte) -> byte_to_w256 a
  end

(* log256floor takes a logarithm (base 256) of an integer and takes floor *)

val log2 : integer -> integer
let rec log2 x =
  if x <= 1 then 0
  else 1 + log2 (x / 2)
declare coq target_rep function log2 = `Z.log2`
declare termination_argument log2 = automatic

val log256floor : integer -> integer
let rec {isabelle; hol; ocaml} log256floor x =
  if x <= 255 then 0
  else 1 + log256floor (x / 256)
let {coq} log256floor x = log2 x / 8
declare termination_argument log256floor = automatic

val word_exp : integer -> natural -> integer
let rec {isabelle;hol;ocaml} word_exp i n =
  match n with
  | 0 -> 1
  | _ ->
      let half = n / 2 in
      let modulo = natFromNatural (n mod 2) in
      let recur = word_exp i half in
         ((i ** modulo) * recur * recur) mod (2 ** 256)
  end
let rec {coq} word_exp i n =
  match n with
  | 0 -> 1
  | n+1 -> (word_exp i n * i) mod (2 ** 256)
  end
declare termination_argument word_exp = automatic

(* In EVM, the memory contains one byte for each machine word (offset). *)
(* The storage contains one machine word for each machine word (index). *)
(* As we will see, the memory is cleared for every invocation of smart contracts. *)
(* The storage is persistent for an account. *)

type memory = w256 -> byte
type storage = w256 -> w256

(* Looking up a number of bytes from the memory: *)
val cut_memory_aux : w256 -> natural -> memory -> list byte
let rec cut_memory_aux idx n memory = match n with
  | 0 -> []
  | n + 1 -> memory idx :: cut_memory_aux (idx + 1) n memory
end
declare termination_argument cut_memory_aux = automatic

val iota : w256 -> natural -> list w256 -> list w256
let rec iota start n rev_acc =
  match n with
  | 0 -> reverse rev_acc
  | x + 1 -> iota (start + 1) x (start :: rev_acc)
  end
declare termination_argument iota = automatic

val cut_memory_aux_alt : w256 -> natural -> memory -> list byte
let cut_memory_aux_alt idx n memory = List.map memory (iota idx n [])

val cut_memory : w256 -> w256 -> memory -> list byte
let cut_memory idx n memory = cut_memory_aux_alt idx (word256ToNatural n) memory

val put_return_values_aux : memory -> list byte -> integer -> natural -> memory
let rec put_return_values_aux orig lst b s = match s with
  | 0 -> orig
  | s + 1 ->
  match lst with
  | [] -> orig
  | h :: t -> put_return_values_aux (fun addr -> if addr = word256FromInteger b then h else orig addr) t (b + 1) s
  end
end
declare termination_argument put_return_values_aux = automatic

val put_return_values : memory -> list byte -> integer -> integer -> memory
let put_return_values orig lst b s =
  if s <= 0 then orig else put_return_values_aux orig lst b (naturalFromInteger s)

(* The storage is modelled as a function.  For example, the empty storage *)
(* is a function that returns zero for every index.  Initially all accounts come with *)
(* the empty storage. *)

val empty_storage : storage
let empty_storage _ = 0


type network =
  Frontier
| Homestead
| EIP150
| EIP158
| Metropolis


val network_of_block_number : integer -> network
let network_of_block_number bn =
  if bn < 115 * 100 * 100 then Frontier
  else if bn < 3 * 821 * 10 * 100 then Homestead
  else if bn < 5 * 5 * 107 * 10 * 100 then EIP150
  else EIP158
(* This needs to be updated when a new fork is planned. *)

val at_least_eip150 : network -> bool
let at_least_eip150 n =
  match n with
    Frontier -> false
  | Homestead -> false
  | EIP150 -> true
  | EIP158 -> true
  | Metropolis -> true
  end

val before_homestead : network -> bool
let before_homestead n =
  match n with
    Frontier -> true
  | Homestead -> false
  | EIP150 -> false
  | EIP158 -> false
  | Metropolis -> false
  end


(* This section lists the EVM instructions and their byte representations. *)
(* I also introduce an assertion instruction, whose byte representation is empty. *)
(* The assertion instruction is a statement about the state of the EVM at *)
(* that position of the program. *)


(****** What used to be Instructions.thy ******)

(* In Isabelle/HOL, it is expensive to define a single inductive type *)
(* that contains all instructions.  When I do it, Isabelle/HOL automatically proves every *)
(* instruction is different from any other instruction, but this process has the computational *)
(* complexity of the square of the number of instructions.  Instead, I define multiple *)
(* smaller inductive types and unify them at the end.  *)


(* (delta, alpha) is the (consumption, production) on thae stack. *)
type stack_numbers = (int * int)


(* subsection "Bit Operations" *)


(* The following clause defines a type called \textit{bits\_inst}. *)
(* The type has five elements.  It is automatically understood that nothing else *)
(* belongs to this type.  It is also understood that every one of these five elements *)
(* is different from any of the other four. *)

(* Some instructions have \textit{inst\_} in front because names like AND, *)
(* OR and XOR are taken by the machine word library. *)

(* The instructions have different arities.  They might consume some elements on the stack, *)
(* and produce some elements on the stack.  However, the arity of the instructions are not specified *)
(* in this section. *)

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 *)

(* These instructions are represented by the following bytes. *)
(* Most opcodes are a single byte. *)

val bits_inst_code : bits_inst -> byte
let bits_inst_code inst = match inst with
| inst_AND -> 0X16
| inst_OR -> 0X17
| inst_XOR -> 0X18
| inst_NOT -> 0X19
| BYTE -> 0X1a
end

val bits_stack_nums : bits_inst -> stack_numbers
let bits_stack_nums inst = match inst with
| inst_AND -> (2, 1)
| inst_OR -> (2, 1)
| inst_XOR -> (2, 1)
| inst_NOT -> (1, 1)
| BYTE -> (2, 1)
end

(* subsection "Signed Arithmetics" *)

(* More similar definitions follow.  Below are instructions for signed arithmetics.
The operations common to signed and unsigned are listed further below in the
Unsigned Arithmetics section. *)

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 inst = match inst with
| SDIV -> 0X05
| SMOD -> 0X07
| SGT -> 0X13
| SLT -> 0X12
| SIGNEXTEND -> 0X0b
end

val sarith_inst_nums : sarith_inst -> stack_numbers
let sarith_inst_nums inst = match inst with
| SDIV -> (2, 1)
| SMOD -> (2, 1)
| SGT -> (2, 1)
| SLT -> (2, 1)
| SIGNEXTEND -> (2, 1)
end

(* subsection "Unsigned Arithmetics" *)

(* The names GT, EQ and LT are taken in the Cmp library *)
(* (which will be used for AVL trees). *)

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 inst = match inst with
| ADD -> 0X01
| MUL -> 0X02
| SUB -> 0X03
| DIV -> 0X04
| MOD -> 0X06
| ADDMOD -> 0X08
| MULMOD -> 0X09
| EXP -> 0X0a
| inst_GT -> 0X11
| inst_LT -> 0X10
| inst_EQ -> 0X14
| ISZERO -> 0X15
| SHA3 -> 0X20
end

val arith_inst_numbers : arith_inst -> stack_numbers
let arith_inst_numbers inst = match inst with
| ADD -> (2, 1)
| MUL -> (2, 1)
| SUB -> (2, 1)
| DIV -> (2, 1)
| MOD -> (2, 1)
| ADDMOD -> (3, 1)
| MULMOD -> (3, 1)
| EXP -> (2, 1)
| inst_GT -> (2, 1)
| inst_LT -> (2, 1)
| inst_EQ -> (2, 1)
| ISZERO -> (1, 1)
| SHA3 -> (2, 1)
end


(* subsection "Informational Instructions" *)

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 inst = match inst with
| ADDRESS -> 0X30
| BALANCE -> 0X31
| ORIGIN -> 0X32
| CALLVALUE -> 0X34
| CALLDATASIZE -> 0X36
| CALLER -> 0X33
| CODESIZE -> 0X38
| GASPRICE -> 0X3a
| EXTCODESIZE -> 0X3b
| BLOCKHASH -> 0X40
| COINBASE -> 0X41
| TIMESTAMP -> 0X42
| NUMBER -> 0X43
| DIFFICULTY -> 0X44
| GASLIMIT -> 0X45
| GAS -> 0X5a
end

val info_inst_numbers : info_inst -> stack_numbers
let info_inst_numbers inst = match inst with
| ADDRESS -> (0, 1)
| BALANCE -> (1, 1)
| ORIGIN -> (0, 1)
| CALLER -> (0, 1)
| CALLVALUE -> (0, 1)
| CALLDATASIZE -> (0, 1)
| CODESIZE -> (0, 1)
| GASPRICE -> (0, 1)
| EXTCODESIZE -> (1, 1)
| BLOCKHASH -> (1, 1)
| COINBASE -> (0, 1)
| TIMESTAMP -> (0, 1)
| NUMBER -> (0, 1)
| DIFFICULTY -> (0, 1)
| GASLIMIT -> (0, 1)
| GAS -> (0, 1)
end

(* subsection "Duplicating Stack Elements" *)

(* There are sixteen instructions for duplicating a stack element.  These instructions take *)
(* a stack element and duplicate it on top of the stack. *)

type nibble = word4

type dup_inst = nibble

val dup_inst_code : dup_inst -> byte
let dup_inst_code m =
  (word8FromInt (word4ToUInt m) + 0X80)

val dup_inst_numbers : dup_inst -> stack_numbers
let dup_inst_numbers m = (word4ToUInt m, word4ToUInt m + 1)

(* subsection {* Memory Operations *} *)

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 inst = match inst with
| MLOAD -> 0X51
| MSTORE -> 0X52
| MSTORE8 -> 0X53
| CALLDATACOPY -> 0X37
| CODECOPY -> 0X39
| EXTCODECOPY -> 0X3c
| MSIZE -> 0X59
end

val memory_inst_numbers : memory_inst -> stack_numbers
let memory_inst_numbers inst = match inst with
| MLOAD        -> (1, 1)
| MSTORE       -> (2, 0)
| MSTORE8      -> (2, 0)
| CALLDATACOPY -> (3, 0)
| CODECOPY     -> (3, 0)
| EXTCODECOPY  -> (4, 0)
| MSIZE        -> (0, 1)
end

(* subsection {* Storage Operations *} *)

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 inst = match inst with
| SLOAD -> 0X54
| SSTORE -> 0X55
end

val storage_inst_numbers : storage_inst -> stack_numbers
let storage_inst_numbers inst = match inst with
| SLOAD -> (1, 1)
| SSTORE -> (2, 0)
end

(* subsection {* Program-Counter Instructions *} *)

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. *)

 (* experimental subroutine instructions *)
type evm15_inst =
 | JUMPIF of w8 * w8
 | JUMPTO of w8 * w8
 | JUMPSUB of w8 * w8
 | BEGINSUB of w8 * w8 * w8 * w8
 | RETURNSUB
 | GETLOCAL of w8 * w8
 | PUTLOCAL of w8 * w8

(* If a jump occurs to a location where @{term JUMPDEST} is not found, the execution fails. *)
(* 0xB0 JUMPTO
 * 0xB1 JUMPIF
 * 0XB2 JUMPSUB
 * 0xB4 JUMPSUBV
 * 0xB5 BEGINSUB
 * 0xB6 BEGINDATA
 * 0xB8 RETURNSUB
 * 0xB9 PUTLOCAL
 * 0xBA GETLOCAL*)
val pc_inst_code : pc_inst -> byte
let pc_inst_code inst = match inst with
| JUMP -> 0X56
| JUMPI -> 0X57
| PC -> 0X58
| JUMPDEST -> 0X5b
end

val evm15_inst_code : evm15_inst -> list byte
let evm15_inst_code inst = match inst with
| JUMPTO a1 a2 -> [0XB0; a1; a2]
| JUMPIF a1 a2 -> [0XB1; a1; a2]
| JUMPSUB a1 a2 -> [0XB2; a1; a2]
| BEGINSUB a1 a2 r1 r2 -> [0XB5; a1; a2; r1; r2]
| RETURNSUB -> [0XB8]
| GETLOCAL a1 a2 -> [0XB9; a1; a2]
| PUTLOCAL a1 a2 -> [0XB8; a1; a2]
end

val pc_inst_numbers : pc_inst -> stack_numbers
let pc_inst_numbers inst = match inst with
| JUMP -> (1, 0)
| JUMPI -> (2, 0)
| PC -> (0, 1)
| JUMPDEST -> (0, 0)
end

val evm15_inst_numbers : evm15_inst -> stack_numbers
let evm15_inst_numbers inst = match inst with
| JUMPTO _ _ -> (0, 0)
| JUMPIF _ _ -> (1, 0)
| JUMPSUB _ _ -> (0, 0)
| BEGINSUB _ _ _ _-> (0, 0)
| RETURNSUB -> (0, 0)
| GETLOCAL _ _ -> (0, 1)
| PUTLOCAL _ _ -> (1, 0)
end


(* subsection {* Stack Instructions *} *)

(* The PUSH instructions have longer byte representations than the other instructions *)
(* because they contain immediate values. *)
(* Here the immediate value is represented by a list of bytes.  Depending on the *)
(* length of the list, the PUSH operation takes different opcodes. *)

type stack_inst =
  | POP (* throwing away the topmost element of the stack *)
  | PUSH_N of list byte (* 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 inst = match inst with
| POP -> [0X50]
| PUSH_N lst ->
     if length lst < 1 then [0X60; 0X00] (* this case should not exist *)
     else if length lst > 32 then [0X60; 0X00] (* this case should not exist *)
     else [byteFromNat (length lst) + 0X5f] ++ lst
| CALLDATALOAD -> [0X35]
end

val stack_inst_numbers : stack_inst -> stack_numbers
let stack_inst_numbers inst = match inst with
| POP -> (1, 0)
| PUSH_N _ -> (0, 1)
| CALLDATALOAD -> (1, 1)
end

type swap_inst = nibble

val swap_inst_code : swap_inst -> byte
let swap_inst_code m =
  (word8FromInt (word4ToUInt m) + 0X90)

val swap_inst_numbers : swap_inst -> stack_numbers
let swap_inst_numbers m =
(word4ToUInt m + 1, word4ToUInt m + 1)

(* subsection {* Logging Instructions *} *)

(* There are instructions for logging events with different number of arguments. *)

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

val log_inst_code : log_inst -> byte
let log_inst_code inst = match inst with
| LOG0 -> 0Xa0
| LOG1 -> 0Xa1
| LOG2 -> 0Xa2
| LOG3 -> 0Xa3
| LOG4 -> 0Xa4
end

val log_inst_numbers : log_inst -> stack_numbers
let log_inst_numbers inst = match inst with
| LOG0 -> (2, 0)
| LOG1 -> (3, 0)
| LOG2 -> (4, 0)
| LOG3 -> (5, 0)
| LOG4 -> (6, 0)
end

(* subsection {* Miscellaneous Instructions *} *)

(* This section contains the instructions that alter the account-wise control flow. *)
(* In other words, they cause communication between accounts (or at least interaction with *)
(* other accounts' code). *)

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 inst = match inst with
| STOP -> 0X00
| CREATE -> 0Xf0
| CALL -> 0Xf1
| CALLCODE -> 0Xf2
| RETURN -> 0Xf3
| DELEGATECALL -> 0Xf4
| SUICIDE -> 0Xff
end

val misc_inst_numbers : misc_inst -> stack_numbers
let misc_inst_numbers inst = match inst with
| STOP         -> (0, 0)
| CREATE       -> (3, 1)
| CALL         -> (7, 1)
| CALLCODE     -> (7, 1)
| RETURN       -> (2, 0)
| DELEGATECALL -> (6, 1)
| SUICIDE      -> (1, 0)
end

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
  | Evm15 of evm15_inst

(* subsection {* The Whole Instruction Set *} *)

(* The small inductive sets above are here combined into a single type. *)

let maybe_to_list m = match m with
 | Nothing -> []
 | Just s -> [s]
end

val inst_code : inst -> list byte
let inst_code inst = match inst with
| Unknown byte -> [byte]
| 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 -> [dup_inst_code d]
| Memory m -> [memory_inst_code m]
| Storage s -> [storage_inst_code s]
| Pc p -> [pc_inst_code p]
| Stack s -> stack_inst_code s
| Swap s -> [swap_inst_code s]
| Log l -> [log_inst_code l]
| Misc m -> [misc_inst_code m]
| Evm15 e -> evm15_inst_code e
end

val inst_stack_numbers : inst -> stack_numbers
let inst_stack_numbers i = match i with
| Unknown _ -> (0, 0)
| Bits b -> bits_stack_nums b
| Sarith s -> sarith_inst_nums s
| Arith a -> arith_inst_numbers a
| Info i' -> info_inst_numbers i'
| Dup d -> dup_inst_numbers d
| Memory m -> memory_inst_numbers m
| Storage s -> storage_inst_numbers s
| Pc p -> pc_inst_numbers p
| Stack s -> stack_inst_numbers s
| Swap s -> swap_inst_numbers s
| Log l -> log_inst_numbers l
| Misc m -> misc_inst_numbers m
| Evm15 e -> evm15_inst_numbers e
end


(* The size of an opcode is useful for parsing a hex representation of an *)
(* EVM code.  *)

val inst_size : inst -> int
let inst_size i = intFromNat (length (inst_code i))

(* section "Gas schedule" *)

val Gzero : integer
let Gzero = 0

val Gbase : integer
let Gbase = 2

val Gverylow : integer
let Gverylow = 3

val Glow : integer
let Glow = 5

val Gmid : integer
let Gmid = 8

val Ghigh : integer
let Ghigh = 10

val eip150_block : integer
let inline eip150_block = 2463*1000

val homestead_block : integer
let homestead_block = 1150*1000

val Gextcode : network -> integer
let Gextcode net =
  if at_least_eip150 net then 700 else 20

val Gbalance : network -> integer
let Gbalance n =
  if at_least_eip150 n then 400 else 20

val Gsload : network -> integer
let Gsload n =
  if at_least_eip150 n then 200 else 50

val Gjumpdest : integer
let Gjumpdest = 1

val Gsset : integer
let Gsset = 20000

val Gsreset : integer
let Gsreset = 5000

val Rsclear : integer
let Rsclear = 15000

val Rsuicide : integer
let Rsuicide = 24000

val Gsuicide : network -> integer
let Gsuicide n =
  if at_least_eip150 n then 5000 else 0

val Gcreate : integer
let Gcreate = 32000

val Gcodedeposit : integer
let Gcodedeposit = 200

val Gcall : network -> integer
let Gcall net =
  if at_least_eip150 net then 700 else 40

val Gcallvalue : integer
let Gcallvalue = 9000

val Gcallstipend : integer
let Gcallstipend = 2300

val Gnewaccount : integer
let Gnewaccount = 25000

val Gexp : integer
let Gexp = 10

val Gexpbyte : network -> integer
let Gexpbyte net =
  if at_least_eip150 net then 50 else 10

val Gmemory : integer
let Gmemory = 3

val Gtxcreate : integer
let Gtxcreate = 32000

val Gtxdatazero : integer
let Gtxdatazero = 4

val Gtxdatanonzero : integer
let Gtxdatanonzero = 68

val Gtransaction : integer
let Gtransaction = 21000

val Glog : integer
let Glog = 375

val Glogdata : integer
let Glogdata = 8

val Glogtopic : integer
let Glogtopic = 375

val Gsha3 : integer
let Gsha3 = 30

val Gsha3word : integer
let Gsha3word = 6

val Gcopy : integer
let Gcopy = 3

val Gblockhash : integer
let Gblockhash = 20


(* section "A Contract Centric View of the EVM" *)

(* subsection "The Interaction between the Contract and the Environment" *)

(* In this development, the EVM execution is seen as an interaction between a single contract *)
(* and the environment.  The environment can call into the contract.  The contract can reply by just *)
(* finishing or failing, but it can also call an account\footnote{This might be the same account as our *)
(* invocation, but still the deeper calls is part of the world.}.  When our contract execution calls an account, *)
(* this is seen as an action towards the environment, because the environment then has to decide the *)
(* result of this call.  The environment can say that the call finished successfully or exceptionally. *)
(* The environment can also say that the call resulted in a reentrancy.  In other words, *)
(* the environment can call the contract again and change the storage and the balance of our contract. *)
(* The whole process is captured as a game between the environment and the contract. *)

(* subsubsection "The Environment's Moves" *)

(* The environment can call into our contract. *)
(* Then the environment provides our\footnote{ *)
(* The contract's behavior is controlled by a concrete code, but the environment's behavior is unrestricted.*)
(* So when I get emotional I call the contract ``our'' contract. *)
(* } contract *)
(* with the following information. *)

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

(* After our contract calls accounts, the environment can make those accounts *)
(* return into our contracts.  The return value is not under control of our current *)
(* contract, so it is the environment's move.  In that case, the environment provides the *)
(* following information. *)

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

(* Even our account's balance (and its storage) might have changed at this moment. *)
(* @{typ return_result} type is also used when our contract returns, as we will see. *)

(* With these definitions now we can define the environment's actions.  In addition to call and return, *)
(* there is another clause for failing back to the account.  This happens when our contract calls *)
(* an account but the called account fails. *)

(* When our contract deploys a smart contract, our contract should provide the following *)
(* information. *)

type environment_action =
| EnvironmentCall of call_env (* the environment calls into the account *)
| EnvironmentRet of return_result (* the environment returns back to the account *)
| EnvironmentFail (* the environment fails back to the account. *)


(* subsubsection "The Contract's Moves" *)

(* After being invoked, the contract can respond by calling an account, creating (or deploying)
a smart contract, destroying itself, returning, or failing.  When the contract calls an account,
the contract provides the following information.*)

(* When our contract deploys a smart contract, our contract should provide the following
information. *)

(* The contract's moves are summarized as follows. *)

type call_arguments = <|
  callarg_gas : w256; (* 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 : w256; (* The amount of Eth sent along *)
  callarg_data : list byte; (* The data sent along *)
  callarg_output_begin : w256; (* The beginning of the memory region where the output data should be written. *)
  callarg_output_size : w256; (* The size of the memory regions where the output data should be written. *)
|>

type create_arguments = <|
  createarg_value : w256; (* The value sent to the account *)
  createarg_code : list byte; (* The code that deploys the runtime code. *)
|>

type failure_reason =
| OutOfGas
| TooLongStack
| TooShortStack
| InvalidJumpDestination
| ShouldNotHappen

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

(* subsection "Program Representation" *)

(* For performance reasons, the instructions can be stored in a binary tree that allows *)
(* looking up instructions from the program counters. *)

type program = <|
  program_content : integer -> maybe inst; (* a way to look up instructions from positions *)
  program_length  : integer; (* the length of the program in bytes *)
|>

(* The empty program is easy to define. *)

val empty_program : program
let empty_program = <|
  program_content = (fun _ -> Nothing);
  program_length = 0
|>


(* subsection "Translating an Instruction List into a Program" *)

(* subsubsection {* Translating a list of instructions into a program *} *)

(* The results of the above translations are packed together in a record. *)
(* For efficiency reasons, the program content is going to be packed as *)
(* an AVL tree, but this particular encoding is not part of the Lem definition. *)
(* So such encoders are parametrised here. *)

val program_of_lst : list inst -> (list inst -> (integer -> maybe inst)) -> program
let program_of_lst lst program_content_formatter = <|
  program_content = program_content_formatter lst;
  program_length = integerFromNat (length lst);
|>

(* subsection {* Program as a Byte Sequence *} *)

(* For CODECOPY instruction, the program must be seen as a byte-indexed read-only memory. *)
(* Such a memory is here implemented by a lookup on an AVL tree.*)

val program_as_natural_map : program -> natural -> byte
let program_as_natural_map p idx =
   match p.program_content (integerFromNatural idx) with
   | Nothing -> 0
   | Just inst ->
      match List.index (inst_code inst) 0 with
      | Nothing -> 0
      | Just a -> a
      end
   end

(* Execution Environments *)

(* I model an instruction as a function that takes environments and modifies some parts of them. *)

(* The execution of an EVM program happens in a block, and the following information about *)
(* the block should be available. *)

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


(* A log entry is something like this. *)
type log_entry = <|
  log_addr   : address;
  log_topics : list w256;
  log_data   : list byte;
|>


(* The variable context contains information that is relatively volatile. *)

type variable_ctx = <|
  vctx_stack : list w256;
  vctx_return_stack : list integer;
  vctx_frame_stack : list nat;
  vctx_memory : memory;
  vctx_memory_usage : integer; (* the current memory usage *)
  vctx_storage : storage;
  vctx_pc : integer; (* the program counter *)
  vctx_balance : address -> w256; (* balances of all accounts *)
  vctx_caller : address; (* the caller's address *)
  vctx_value_sent : w256; (* the amount of Eth sent along the current invocation *)
  vctx_data_sent : list byte; (* the data sent along the current invocation *)
  vctx_storage_at_call : storage; (* the storage content at the invocation*)
  vctx_balance_at_call : address -> w256; (* the balances at the invocation *)
  vctx_origin : address; (* the external account that started the current transaction *)
  vctx_ext_program : address -> program; (* the codes of all accounts *)
  vctx_block : block_info; (* the current block *)
  vctx_gas : integer; (* remaining gas before the instruction *)
  vctx_account_existence : address -> bool;
  vctx_touched_storage_index : list w256;
  vctx_logs : list log_entry; (* stored newest first *)
  vctx_refund : integer;
  vctx_gasprice : w256;
|>

(* The constant context contains information that is rather stable. *)
type constant_ctx = <|
  cctx_program : program; (* the code in the account under verification. *)
  cctx_this : address; (* the address of the account under verification. *)
  cctx_hash_filter : list byte -> bool;
|>

(* subsection {* The Result of an Instruction *} *)

(* The result of program execution is microscopically defined by results of instruction *)
(* executions.  The execution of a single instruction can result in the following cases: *)

type instruction_result =
| InstructionContinue of variable_ctx (* the execution should continue. *)
| InstructionToEnvironment of
  (* the execution has stopped; either for the moment just calling out another account, or *)
  (* finally finishing the current invocation *)
    contract_action   (* the contract's move *)
  * variable_ctx      (* the last venv *)
  * maybe (integer * integer) (* the variable environment to return to *)

(* When the contract fails, the result of the instruction always looks like this: *)
val instruction_failure_result : variable_ctx -> list failure_reason -> instruction_result
let instruction_failure_result v reasons =
  InstructionToEnvironment (ContractFail reasons) v Nothing

(* When the contract returns, the result of the instruction always looks like this: *)
val instruction_return_result : list byte -> variable_ctx -> instruction_result
let instruction_return_result x v =
  InstructionToEnvironment (ContractReturn x) v Nothing

(* subsection {* Useful Functions for Defining EVM Operations *} *)

(* Currently the GAS instruction is modelled to return random numbers. *)
(* The random number is not known to be of any value. *)
(* However, the value is not unknown enough in this formalization because *)
(* the value is only dependent on the variable environment (which does not *)
(* keep track of the remaining gas).  This is not a problem as long as *)
(* we are analyzing a single invocation of a loopless contract, but *)
(* gas accounting is a planned feature. *)

val gas : variable_ctx -> w256
let gas v = word256FromInteger v.vctx_gas

(* This $M$ function is defined at the end of H.1.\,in the yellow paper. *)
(* This function is useful for updating the memory usage counter. *)

val M : integer -> w256 -> w256 -> integer
let M s f l =
  if l = 0 then s else max s ((uint f + uint l + 31) div 32)

(* Updating a balance of a single account:  *)
val update_balance : address -> (w256 -> w256) -> (address -> w256) -> (address -> w256)
let update_balance a f orig x = if x = a then f (orig a) else orig x

(* Popping stack elements: *)
val vctx_pop_stack : nat -> variable_ctx -> variable_ctx
let vctx_pop_stack n v =
 <| v with vctx_stack = drop n v.vctx_stack |>

(* Updating the storage at an index: *)
val vctx_update_storage : w256 -> w256-> variable_ctx -> variable_ctx
let vctx_update_storage idx vall v =
  <| v with vctx_storage = (fun x -> if x = idx then vall else v.vctx_storage x) |>

(* Peeking the next instruction: *)
val vctx_next_instruction : variable_ctx -> constant_ctx -> maybe inst
let vctx_next_instruction v c =
  match c.cctx_program.program_content v.vctx_pc with
  | Just i -> Just i
  | Nothing -> Just (Misc STOP)
  end

(* Advancing the program counter: *)
val vctx_advance_pc : constant_ctx -> variable_ctx -> variable_ctx
let vctx_advance_pc c v =
  <| v with vctx_pc =
     (match vctx_next_instruction v c with
     | Nothing -> v.vctx_pc + 1
     | Just inst -> v.vctx_pc + integerFromInt (inst_size inst) end) |>

(* No-op, which just advances the program counter: *)
val stack_0_0_op : variable_ctx -> constant_ctx -> instruction_result
let stack_0_0_op v c = InstructionContinue (vctx_advance_pc c v)

(* A general pattern of operations that pushes one element onto the stack:  *)
val stack_0_1_op : variable_ctx -> constant_ctx -> w256 -> instruction_result
let stack_0_1_op v c w =
   InstructionContinue (vctx_advance_pc c <| v with vctx_stack = w :: v.vctx_stack |>)


(* A general pattern of operations that transforms the topmost element of the stack: *)
val stack_1_1_op : variable_ctx -> constant_ctx -> (w256 -> w256) -> instruction_result
let stack_1_1_op v c f = match v.vctx_stack with
  | [] -> instruction_failure_result v [TooShortStack]
  | h :: t -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = f h :: t |>)
end

(* A general pattern of operations that take two words and produce one word: *)
val stack_2_1_op : variable_ctx -> constant_ctx -> (w256 -> w256 -> w256) -> instruction_result
let stack_2_1_op v c f = match v.vctx_stack with
 | operand0 :: operand1 :: rest ->
       InstructionContinue
         (vctx_advance_pc c <| v with vctx_stack = f operand0 operand1 :: rest |>)
  | _ -> instruction_failure_result v [TooShortStack]
end

(* A general pattern of operations that take three words and produce one word: *)
val stack_3_1_op : variable_ctx -> constant_ctx -> (w256 -> w256 -> w256 -> w256) -> instruction_result
let stack_3_1_op v c f = match v.vctx_stack with
 | operand0 :: operand1 :: operand2 :: rest ->
       InstructionContinue
         (vctx_advance_pc c <| v with vctx_stack = f operand0 operand1 operand2 :: rest |>)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* Retrieve value of a stack element, or 0 if non-existent: *)
val vctx_stack_default : int -> variable_ctx -> w256
let vctx_stack_default idx v =
  match List.index v.vctx_stack (natFromInt idx) with
  | Just w -> w
  | Nothing -> 0
  end

(* Calculate active memory (i.e. vctx_memory_usage) after the execution of an instruction: *)
val new_memory_consumption : inst -> integer -> w256 -> w256 -> w256 -> w256 -> w256 -> w256 -> w256 -> integer
let new_memory_consumption i original_memory_usage s0 s1 s2 s3 s4 s5 s6 =
  match i with
  | Arith SHA3 -> M original_memory_usage s0 s1
  | Memory CALLDATACOPY ->
    M original_memory_usage s0 s2
  | Memory CODECOPY ->
    M original_memory_usage s0 s2
  | Memory EXTCODECOPY ->
    M original_memory_usage s1 s3
  | Memory MLOAD ->
    M original_memory_usage s0 32
  | Memory MSTORE ->
    M original_memory_usage s0 32
  | Memory MSTORE8 ->
    M original_memory_usage s0 1
  | Misc CREATE ->
    M original_memory_usage s1 s2
  | Misc CALL ->
    M (M original_memory_usage s3 s4) s5 s6
  | Misc CALLCODE ->
    M (M original_memory_usage s3 s4) s5 s6
  | Misc DELEGATECALL ->
    M (M original_memory_usage s2 s3) s4 s5
  | Misc RETURN ->
    M original_memory_usage s0 s1
  | Log _ -> M original_memory_usage s0 s1
  | _ -> original_memory_usage
  end

(* subsection {* Definition of EVM Operations *} *)

val check_refund : w256 -> w256 -> integer
let check_refund oldv newv = if oldv <> 0 && newv = 0 then 15000 else 0

(* SSTORE changes the storage so it does not fit into any of the patterns defined above. *)

val sstore : variable_ctx -> constant_ctx -> instruction_result
let sstore v c = match v.vctx_stack with
 | addr :: vl :: stack_tail ->
      InstructionContinue (vctx_advance_pc c
        (vctx_update_storage addr vl
           <| v with vctx_stack = stack_tail; vctx_touched_storage_index = addr :: v.vctx_touched_storage_index;
                     vctx_refund = v.vctx_refund + check_refund (v.vctx_storage addr) vl |>))
 | _ -> instruction_failure_result v [TooShortStack]
end

val combine_w8s_to_uint: w8 -> w8 -> integer
let combine_w8s_to_uint v1 v2 =
        (uintFromW8 v1 * 256 + uintFromW8 v2)

(* The JUMP instruction has the following meaning.  When it cannot find the JUMPDEST instruction *)
(* at the destination, the execution fails. *)
val jumpto : variable_ctx -> constant_ctx -> w8 -> w8 -> instruction_result
let jumpto v c a1 a2 =
    let v_new = <| v with vctx_pc = combine_w8s_to_uint a1 a2 |> in
    match vctx_next_instruction v_new c with
      | Just (Pc JUMPDEST) -> InstructionContinue v_new
      | _ -> instruction_failure_result v [InvalidJumpDestination]
    end

val jump : variable_ctx -> constant_ctx -> instruction_result
let jump v c = match v.vctx_stack with
 | [] -> instruction_failure_result v [TooShortStack]
 | pos :: tl ->
     let v_new = <| v with vctx_stack = tl; vctx_pc = uint pos |> in
     match vctx_next_instruction v_new c with
      | Just (Pc JUMPDEST) -> InstructionContinue v_new
      | _ -> instruction_failure_result v [InvalidJumpDestination]
     end
end

(* This function is a reminiscent of my struggle with the Isabelle/HOL simplifier. *)
(* The second argument has no meaning but to control the Isabelle/HOL simplifier. *)

val blockedInstructionContinue : variable_ctx -> bool -> instruction_result
let blockedInstructionContinue v _ = InstructionContinue v

(* This is another reminiscent of my struggle against the Isabelle/HOL simplifier. *)
(* Again, the simplifier is not allowed to expand the definition unless the second argument *)
(* is known to be @{term True}.*)

val blocked_jump : variable_ctx -> constant_ctx -> bool -> instruction_result
let blocked_jump v c _ = jump v c

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

(* The JUMPI instruction is implemented using the JUMP instruction. *)
val jumpi : variable_ctx -> constant_ctx -> instruction_result
let jumpi v c = match v.vctx_stack with
 | pos :: cond :: rest ->
    let new_env = <| v with vctx_stack = pos :: rest |> in
    strict_if (cond = 0)
           (blockedInstructionContinue (vctx_advance_pc c (vctx_pop_stack 2 v)))
           (blocked_jump new_env c)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* The JUMPIF instruction is implemented using the JUMP instruction. *)
val jumpif : variable_ctx -> constant_ctx -> w8 -> w8 -> instruction_result
let jumpif v c a1 a2 = match v.vctx_stack with
 | cond :: rest ->
    let new_env = <| v with vctx_stack = rest |> in
    if cond = 0 then
           InstructionContinue (vctx_advance_pc c new_env)
    else
           jumpto new_env c a1 a2
 | _ -> instruction_failure_result v [TooShortStack]
end

(* Looking up the call data size takes this work: *)
val datasize : variable_ctx -> w256
let datasize v = word256FromNat (length v.vctx_data_sent)

val byte_list_fill_right : byte -> nat -> list byte -> list byte
let byte_list_fill_right filled target orig =
  if length orig >= target then orig else
  let filling_len = target - length orig in
  append orig (replicate filling_len filled)

val constant_mark : list byte -> list byte
let constant_mark lst = lst

(* Looking up a word from a list of bytes: *)
val read_word_from_bytes : natural -> list byte -> w256
let read_word_from_bytes idx lst =
  if naturalFromNat (length lst) <= idx then 0
  else
    word_of_bytes
    (byte_list_fill_right 0 32
        (take 32 (drop (natFromNatural idx) lst)))

val cut_data : variable_ctx -> w256 -> w256
let cut_data v idx = read_word_from_bytes (word256ToNatural idx) v.vctx_data_sent

val cut_natural_map : natural -> natural -> (natural -> byte) -> list byte
let rec cut_natural_map idx n nmap = match n with
 | 0 -> []
 | n + 1 -> nmap idx :: cut_natural_map (idx + 1) n nmap
end
declare termination_argument cut_natural_map = automatic

(* Cnew is the funciton denoted as C_\text{\tiny NEW} in the yellow paper.*)
(* However, it takes the sent value and a boolean indicating emptiness of the recipient. *)
val Cnew : w256 -> bool -> integer
let Cnew value emp = if emp (* && not (value = 0) *) then Gnewaccount else 0

(* Cxfer is the function denoted as C_\text{\tiny XFER} in the yellow paper. *)
val Cxfer : w256 -> integer
let Cxfer value = if value = 0 then 0 else Gcallvalue

(* Cextra is the function denoted as C_\text{\tiny EXTRA} in the yellow paper. *)
(* However, it takes a word indicating the transferred value, and a boolean indicating emptiness *)
val Cextra : w256 -> bool -> network -> integer
let Cextra value emp net = Gcall net + Cxfer value + Cnew value emp

(* L is the function denoted as L in the yellow paper. *)
val L : integer -> integer
let L x = x - x / 64

(* Cgascap is the function denoted as C_{\text{\tiny GASCAP}} in the yellow paper. *)
(* However, it takes the two topmost stack elements,
   a boolean indicating emptiness of the recipient, and the remaining gas of the caller *)
val Cgascap : w256 -> w256 -> bool -> integer -> network -> integer -> integer
let Cgascap mu0 mu2 emp remaining_gas net memu_extra =
  if remaining_gas >= Cextra mu2 emp net + memu_extra then
    integerMin (L (remaining_gas - Cextra mu2 emp net - memu_extra)) (uint mu0)
  else
    uint mu0

(* Ccallgas is the function denoted as C_{\text{\tiny CALLGAS}} in the yellow paper. *)
(* However, it takes the three topmost stack elements,
   a boolean indicating emptiness of the recipient, and the remaining gas of the caller *)
val Ccallgas : w256 -> w256 -> w256 -> bool -> integer -> network -> integer -> integer
let Ccallgas mu0 mu1 mu2 emp remaining_gas net memu_extra =
  ( if at_least_eip150 net then Cgascap mu0 mu2 emp remaining_gas net memu_extra else uint mu0) +
  ( if mu2 = 0 then 0 else Gcallstipend )

(* Ccall is the function denoted as C_{\text{\tiny CALL}} *)
(* However, it takes the three topmost stack elements, a boolean indicating
   emptiness of the recipient, and the remaining gas of the caller *)
val Ccall : w256 -> w256 -> w256 -> bool -> integer -> network -> integer -> integer
let Ccall mu0 mu1 mu2 emp remaining_gas net memu_extra =
  ( if at_least_eip150 net then Cgascap mu0 mu2 emp remaining_gas net memu_extra else integerFromNatural (word256ToNatural mu0) ) +
  Cextra mu2 emp net

(* Cmem is the function denoted as C_{mem} in the yellow paper. *)
val Cmem : integer -> integer
let Cmem a = Gmemory * a + (a * a / 512)

(* Csstore is the function denoted as C_\text{\tiny SSTORE} in the yellow paper. *)
(* However, it takes the original word in the storage and the newly stored word. *)
val Csstore : w256 -> w256 -> integer
let Csstore orig newer = if not (newer = 0) && orig = 0 then Gsset else Gsreset

(* Csuicide is the function denoted as C_\text{\tiny SUICIDE} in the yellow paper. *)
(* However, it takes a boolean indicating new account creation. *)
val Csuicide : bool -> network -> integer
let Csuicide recipient_empty net =
  Gsuicide net + (if recipient_empty && at_least_eip150 net then Gnewaccount else 0)

val vctx_next_instruction_default : variable_ctx -> constant_ctx -> inst
let vctx_next_instruction_default v c =
    match vctx_next_instruction v c with
    | Just i -> i
    | Nothing -> Misc STOP
    end

val vctx_recipient : variable_ctx -> constant_ctx -> address
let vctx_recipient v c =
  match vctx_next_instruction_default v c with
  | Misc SUICIDE -> w256_to_address (vctx_stack_default 0 v)
  | Misc CALL -> w256_to_address (vctx_stack_default 1 v)
  | Misc CALLCODE -> c.cctx_this
  | Misc DELEGATECALL -> c.cctx_this
  | _ -> 0
  end



let calc_memu_extra orig_memory_usage s0 s1 s2 s3 s4 s5 s6 =
  Cmem (new_memory_consumption (Misc CALL) orig_memory_usage s0 s1 s2 s3 s4 s5 s6) - Cmem orig_memory_usage
let calc_memu_extra2 v s0 s1 s2 s3 s4 s5 s6 = Cmem (new_memory_consumption (Misc DELEGATECALL) v.vctx_memory_usage s0 s1 s2 s3 s4 s5 s6) - Cmem v.vctx_memory_usage

(* CALL instruction results in @{term ContractCall} action when there are enough stack elements *)
(* (and gas, when we introduce the gas accounting). *)
val call : network -> variable_ctx -> constant_ctx -> instruction_result
let call net v c = match v.vctx_stack with
 | g :: r :: value :: in_begin :: in_size :: out_begin :: out_size :: rest ->
     InstructionToEnvironment (ContractCall
         <| callarg_gas = word256FromInteger (Ccallgas g r value
                     (not (v.vctx_account_existence (vctx_recipient v c)))
                     v.vctx_gas net (calc_memu_extra v.vctx_memory_usage g r value in_begin in_size out_begin out_size));
            callarg_code = w256_to_address r;
            callarg_recipient = w256_to_address r;
            callarg_value = value;
            callarg_data = cut_memory in_begin in_size v.vctx_memory;
            callarg_output_begin = out_begin;
            callarg_output_size = out_size |>)
        (<| (vctx_advance_pc c v) with
           vctx_stack = rest;
           vctx_balance = update_balance c.cctx_this (fun orig -> orig - value) v.vctx_balance |>)
        (Just (* saving the variable environment for timing *)
           (uint out_begin, uint out_size))
  | _ -> instruction_failure_result v [TooShortStack]
end

(* DELEGATECALL is slightly different. *)
val delegatecall : network -> variable_ctx -> constant_ctx -> instruction_result
let delegatecall net v c = match v.vctx_stack with
 | e0 :: e1 :: e3 :: e4 :: e5 :: e6 :: rest ->
       InstructionToEnvironment
         (ContractDelegateCall
           <| callarg_gas = word256FromInteger (Ccallgas e0 e1 0
                     (not (v.vctx_account_existence (vctx_recipient v c))) v.vctx_gas net (calc_memu_extra2 v e0 e1 e3 e4 e5 e6 (vctx_stack_default 6 v)));
              callarg_code = w256_to_address e1;
              callarg_recipient = w256_to_address e1;
              callarg_value = v.vctx_value_sent;
              callarg_data = cut_memory e3 e4 v.vctx_memory;
              callarg_output_begin = e5;
              callarg_output_size = e6 |>)
          (<| (vctx_advance_pc c v) with vctx_stack = rest |>)
          (Just (* save the variable environment for returns *)
            (uint e5, uint e6))
  | _ -> instruction_failure_result v [TooShortStack]
end

(* CALLCODE is another variant. *)
val callcode : network -> variable_ctx -> constant_ctx -> instruction_result
let callcode net v c = match v.vctx_stack with
 | e0 :: e1 :: e2 :: e3 :: e4 :: e5 :: e6 :: rest ->
       InstructionToEnvironment
         (ContractCall
           <| callarg_gas = word256FromInteger (Ccallgas e0 e1 e2
                     (not (v.vctx_account_existence (vctx_recipient v c))) v.vctx_gas net
                     (calc_memu_extra v.vctx_memory_usage e0 e1 e2 e3 e4 e5 e6));
              callarg_code = w256_to_address e1;
              callarg_recipient = c.cctx_this;
              callarg_value = e2;
              callarg_data = cut_memory e3 e4 v.vctx_memory;
              callarg_output_begin = e5;
              callarg_output_size = e6 |>)
          (<| (vctx_advance_pc c v) with
                  vctx_stack = rest |>)
          (Just (* saving the variable environment *) (uint e5, uint e6))
  | _ -> instruction_failure_result v [TooShortStack]
end

(* CREATE is also similar because the instruction causes execution on another account. *)
val create : variable_ctx -> constant_ctx -> instruction_result
let create v c = match v.vctx_stack with
  | vl :: code_start :: code_len :: rest ->
        let code = cut_memory code_start code_len v.vctx_memory in
        InstructionToEnvironment
           (ContractCreate
             <| createarg_value = vl; createarg_code = code |>)
            (<| (vctx_advance_pc c v) with vctx_stack = rest |>)
            (Just (* when returning to this invocation, use the following variable environment *)
              (0, 0))
  | _ -> instruction_failure_result v [TooShortStack]
end

(* For implementing RETURN, I need to cut a region from the memory
according to the stack elements: *)

let vctx_returned_bytes v = match v.vctx_stack with
 | e0 :: e1 :: _ -> cut_memory e0 e1 v.vctx_memory
 | _ -> []
end

(* RETURN is modeled like this: *)
val ret : variable_ctx -> constant_ctx -> instruction_result
let ret v _ =  match v.vctx_stack with
 | _ :: _ :: _ ->
     InstructionToEnvironment (ContractReturn (vctx_returned_bytes v))
                           v
                           Nothing (* No possibility of ever returning to this invocation. *)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* STOP is simpler than RETURN: *)
val stop : variable_ctx -> constant_ctx -> instruction_result
let stop v _ =
    InstructionToEnvironment (ContractReturn []) v Nothing

(* POP removes the topmost element of the stack: *)
val pop : variable_ctx -> constant_ctx -> instruction_result
let pop v c = match v.vctx_stack with
 | _ :: tl -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = tl |>)
 | [] -> instruction_failure_result v [TooShortStack]
end

(* The DUP instructions: *)
val general_dup : nibble -> variable_ctx -> constant_ctx -> instruction_result
let general_dup n v c = match List.index v.vctx_stack (word4ToNat n) with
  | Nothing -> instruction_failure_result v [TooShortStack]
  | Just duplicated -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = duplicated :: v.vctx_stack |>)
end

(* A utility function for storing a list of bytes in the memory: *)
val store_byte_list_memory : w256 -> list byte -> memory -> memory
let {isabelle;hol;coq} store_byte_list_memory pos lst orig p = match index lst (natFromNatural (word256ToNatural (p-pos))) with
 | Just e -> e
 | Nothing -> orig p
end

let {ocaml} store_byte_list_memory pos lst orig p =
  if word256UGE (p - pos) (word256FromNat (length lst)) then orig p else
  match index lst (natFromNatural (word256ToNatural (p-pos))) with
  | Just e -> e
  | Nothing -> orig p
  end

(* Using the function above, it is straightforward to store a byte in the memory. *)
val store_word_memory : w256 -> w256 -> memory -> memory
let store_word_memory pos vl mem =
   store_byte_list_memory pos (word_rsplit256 vl) mem

(* MSTORE writes one word to the memory: *)
val mstore : variable_ctx -> constant_ctx -> instruction_result
let mstore v c = match v.vctx_stack with
  | pos :: vl :: rest ->
       let new_memory = store_word_memory pos vl v.vctx_memory in
       InstructionContinue (vctx_advance_pc c
         <| v with vctx_stack = rest; vctx_memory = new_memory |>)
  | _ -> instruction_failure_result v [TooShortStack]
end

(* MLOAD reads one word from the memory: *)
val mload : variable_ctx -> constant_ctx -> instruction_result
let mload v c = match v.vctx_stack with
 | pos :: rest ->
      let value = read_word_from_bytes 0 (cut_memory pos 32 v.vctx_memory) in
      InstructionContinue
        (vctx_advance_pc c <| v with vctx_stack = value :: rest |>)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* MSTORE8 writes one byte to the memory: *)
val mstore8 : variable_ctx -> constant_ctx -> instruction_result
let mstore8 v c = match v.vctx_stack with
 | pos :: vl :: rest ->
   let new_memory = (fun p -> if p = pos then w256_to_byte vl else v.vctx_memory p) in
   InstructionContinue (vctx_advance_pc c
          <| v with vctx_stack = rest;
                    vctx_memory = new_memory |>)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* For CALLDATACOPY, I need to look at the caller's data as memory. *)
val input_as_natural_map : list byte -> natural -> byte
let input_as_natural_map lst (idx : natural) =
  let idx = integerFromNatural idx in
  if 0 > idx then 0
  else if integerFromNat (length lst) <= idx then 0
  else
    match List.index lst (natFromInteger idx) with
    | Nothing -> 0
    | Just a -> a
    end

(* CALLDATACOPY: *)
val calldatacopy : variable_ctx -> constant_ctx -> instruction_result
let calldatacopy v c = match v.vctx_stack with
 | dst_start :: src_start :: len :: rest ->
       let data = cut_natural_map (word256ToNatural src_start) (word256ToNatural len) (input_as_natural_map v.vctx_data_sent) in
       let new_memory = store_byte_list_memory dst_start data v.vctx_memory in
       InstructionContinue (vctx_advance_pc c
         <| v with vctx_stack = rest; vctx_memory = new_memory |>)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* CODECOPY copies a region of the currently running code to the memory: *)
val codecopy : variable_ctx -> constant_ctx -> instruction_result
let codecopy v c = match v.vctx_stack with
 | dst_start :: src_start :: len :: rest ->
     let data = cut_natural_map (word256ToNatural src_start) (word256ToNatural len)
                  (program_as_natural_map c.cctx_program) in
     let new_memory = store_byte_list_memory dst_start data v.vctx_memory in
     InstructionContinue (vctx_advance_pc c
       <| v with vctx_stack = rest; vctx_memory = new_memory |>)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* EXTCODECOPY copies a region of the code of an arbitrary account.: *)
val extcodecopy : variable_ctx -> constant_ctx -> instruction_result
let extcodecopy v c = match v.vctx_stack with
 | addr :: dst_start :: src_start :: len :: rest ->
     let data = cut_natural_map (word256ToNatural src_start) (word256ToNatural len)
                  (program_as_natural_map
                    (v.vctx_ext_program (w256_to_address addr))) in
     let new_memory = store_byte_list_memory dst_start data v.vctx_memory in
     InstructionContinue (vctx_advance_pc c
       <| v with vctx_stack = rest; vctx_memory = new_memory |>)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* PC instruction could be implemented by @{term stack_0_1_op}: *)
val pc : variable_ctx -> constant_ctx -> instruction_result
let pc v c =
   InstructionContinue (vctx_advance_pc c
     <| v with vctx_stack = word256FromInteger v.vctx_pc :: v.vctx_stack|>)

val create_log_entry : nat -> variable_ctx -> constant_ctx -> log_entry
let create_log_entry n v c =
  <| log_addr = c.cctx_this
   ; log_topics = drop 2 (take (n + 2) v.vctx_stack)
   ; log_data = vctx_returned_bytes v
  |>

(* Logging is currently no-op, until some property about event logging is wanted. *)
val log : nat -> variable_ctx -> constant_ctx -> instruction_result
let log n v c =
   let new_log_entry = create_log_entry n v c in
   InstructionContinue
    (vctx_advance_pc c (vctx_pop_stack (n+2)
       <| v with vctx_logs = new_log_entry ::  v.vctx_logs |>))

(* For SWAP operations, I first define a swap operations on lists. *)
val list_swap : forall 'a. nat -> list 'a -> maybe (list 'a)
let list_swap n lst = match (index lst n, index lst 0) with
 | (Just n_th, Just first) -> Just (List.concat [[n_th]; take (n - 1) (drop 1 lst); [first]; drop (1 + n) lst])
 | _ -> Nothing
end

(* Using this, I can specify the SWAP operations: *)
val swap : nat -> variable_ctx -> constant_ctx -> instruction_result
let swap n v c = match list_swap (n + 1) v.vctx_stack with
 | Nothing -> instruction_failure_result v [TooShortStack]
 | Just new_stack -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = new_stack |>)
end

(* SHA3 instruciton in the EVM is actually Keccak 256. *)
val sha3 : variable_ctx -> constant_ctx -> instruction_result
let sha3 v c = match v.vctx_stack with
 | start :: len :: rest ->
      let lst = cut_memory start len v.vctx_memory in
      if not (c.cctx_hash_filter lst) then instruction_failure_result v [OutOfGas] else
      InstructionContinue (
        vctx_advance_pc c
           <| v with vctx_stack = keccak lst :: rest |>)
 | _ -> instruction_failure_result v [TooShortStack]
end

(* The SUICIDE instruction involves value transfer. *)
val suicide : variable_ctx -> constant_ctx -> instruction_result
let suicide v c = match v.vctx_stack with
 | dst :: _ ->
     InstructionToEnvironment (ContractSuicide (w256_to_address dst)) v Nothing
 | _ -> instruction_failure_result v [TooShortStack]
end


(* subsection {* Resource Checking *} *)



(* thirdComponentOfC is the third component in the definition of C (the gas function). *)
(* However, it takes the next instruction, the four topmost stack elements,
   a boolean indicating emptiness of the recipient, an original word of sstore, a new word of sstore, and the remaining gas of the caller. *)
val thirdComponentOfC : inst -> w256 -> w256 -> w256 -> w256 -> bool -> w256 -> w256 -> integer -> network -> integer -> integer
let thirdComponentOfC i s0 s1 s2 s3 recipient_empty orig_val new_val remaining_gas net = fun memu_extra ->
  match i with
  | Storage SSTORE -> Csstore orig_val new_val
  | Arith EXP -> Gexp + if s1 = 0 then 0 else Gexpbyte net * (1 + log256floor (uint s1))
  | Memory CALLDATACOPY -> Gverylow + Gcopy * ((uint s2 + 31) / 32)
  | Memory CODECOPY -> Gverylow + Gcopy * ((uint s2 + 31) / 32)
  | Memory EXTCODECOPY -> Gextcode net + Gcopy * ((uint s3 + 31) / 32)
  | Log LOG0 -> Glog + Glogdata * uint s1
  | Log LOG1 -> Glog + Glogdata * uint s1 + Glogtopic
  | Log LOG2 -> Glog + Glogdata * uint s1 + 2 * Glogtopic
  | Log LOG3 -> Glog + Glogdata * uint s1 + 3 * Glogtopic
  | Log LOG4 -> Glog + Glogdata * uint s1 + 4 * Glogtopic
  | Misc CALL
    -> Ccall s0 s1 s2 recipient_empty remaining_gas net memu_extra
  | Misc CALLCODE
    -> Ccall s0 s1 s2 recipient_empty remaining_gas net memu_extra
  | Misc DELEGATECALL
    -> if before_homestead net then 0 else Ccall s0 s1 0  recipient_empty remaining_gas net memu_extra
  | Misc SUICIDE -> Csuicide recipient_empty net
  | Misc CREATE -> Gcreate
  | Arith SHA3 -> Gsha3 + Gsha3word * ((uint s1 + 31) / 32)
  | Pc JUMPDEST -> Gjumpdest
  | Storage SLOAD -> Gsload net
  | Misc STOP -> Gzero
  | Misc RETURN -> Gzero
  | Info ADDRESS -> Gbase
  | Info ORIGIN -> Gbase
  | Info CALLER -> Gbase
  | Info CALLVALUE -> Gbase
  | Info CALLDATASIZE -> Gbase
  | Info CODESIZE -> Gbase
  | Info GASPRICE -> Gbase
  | Info COINBASE -> Gbase
  | Info TIMESTAMP -> Gbase
  | Info NUMBER -> Gbase
  | Info DIFFICULTY -> Gbase
  | Info GASLIMIT -> Gbase
  | Stack POP -> Gbase
  | Pc PC -> Gbase
  | Memory MSIZE -> Gbase
  | Info GAS -> Gbase
  | Arith ADD -> Gverylow
  | Arith SUB -> Gverylow
  | Bits inst_NOT -> Gverylow
  | Arith inst_LT -> Gverylow
  | Arith inst_GT -> Gverylow
  | Sarith SLT -> Gverylow
  | Sarith SGT -> Gverylow
  | Arith inst_EQ -> Gverylow
  | Arith ISZERO -> Gverylow
  | Bits inst_AND -> Gverylow
  | Bits inst_OR -> Gverylow
  | Bits inst_XOR -> Gverylow
  | Bits BYTE -> Gverylow
  | Stack CALLDATALOAD -> Gverylow
  | Memory MLOAD -> Gverylow
  | Memory MSTORE -> Gverylow
  | Memory MSTORE8 -> Gverylow
  | Stack (PUSH_N _) -> Gverylow
  | Dup _ -> Gverylow
  | Swap _ -> Gverylow
  | Arith MUL -> Glow
  | Arith DIV -> Glow
  | Sarith SDIV -> Glow
  | Arith MOD -> Glow
  | Sarith SMOD -> Glow
  | Sarith SIGNEXTEND -> Glow
  | Arith ADDMOD -> Gmid
  | Arith MULMOD -> Gmid
  | Pc JUMP -> Gmid
  | Pc JUMPI -> Ghigh
  | Info EXTCODESIZE -> Gextcode net
  | Info BALANCE -> Gbalance net
  | Info BLOCKHASH -> Gblockhash
  | Evm15 (JUMPTO _ _) -> Gmid
  | Evm15 (JUMPIF _ _) -> Ghigh
  | Evm15 (JUMPSUB _ _) -> Ghigh
  | Evm15 (BEGINSUB _ _ _ _) -> Gjumpdest
  | Evm15 RETURNSUB -> Ghigh
  | Evm15 (GETLOCAL _ _) -> Glow
  | Evm15 (PUTLOCAL _ _) -> Glow
  | _ -> 0 (* How is this case dealt in the yellow paper *)
  end

(* C is the function defined in the yellow paper as C.  This represents the gas consumption of an instruction. *)
(* It takes the new memory consumption, the old memory consumption, the next instruction the four
   topmost stack elements, a boolean indicating emptiness of the recipient, an original word of sstore,
   a new word of sstore, and the remaining gas of the caller. *)
val C : integer -> integer -> inst -> w256 -> w256 -> w256 -> w256 -> bool -> w256 -> w256 -> integer -> network -> integer
let C old_memory_consumption new_memory_consumption i s0 s1 s2 s3 recipient_empty orig new_val remaining_gas net =
  Cmem new_memory_consumption  - Cmem old_memory_consumption +
  thirdComponentOfC i s0 s1 s2 s3 recipient_empty orig new_val remaining_gas net (Cmem new_memory_consumption - Cmem old_memory_consumption)

val meter_gas : inst -> variable_ctx -> constant_ctx -> network -> integer
let meter_gas i v c net =
  let musage = max 0 v.vctx_memory_usage
  in C musage
   (new_memory_consumption i musage (vctx_stack_default 0 v) (vctx_stack_default 1 v) (vctx_stack_default 2 v) (vctx_stack_default 3 v)
      (vctx_stack_default 4 v) (vctx_stack_default 5 v) (vctx_stack_default 6 v))
      i
    (vctx_stack_default 0 v) (vctx_stack_default 1 v) (vctx_stack_default 2 v) (vctx_stack_default 3 v)
    (not (v.vctx_account_existence (vctx_recipient v c))) (v.vctx_storage (vctx_stack_default 0 v))
    (vctx_stack_default 1 v) v.vctx_gas net

val check_resources : variable_ctx -> constant_ctx -> list w256 -> inst -> network -> bool
let check_resources v c s i net =
  match inst_stack_numbers i with
  | (consumed, produced) ->
    (intFromNat (length s) + produced - consumed <= 1024) &&
    (meter_gas i v c net <= v.vctx_gas)
  end


val subtract_gas : integer -> integer -> instruction_result -> instruction_result
let subtract_gas consumption memory_usage orig =
  match orig with
  | InstructionContinue v ->
    InstructionContinue (<| v with vctx_gas = v.vctx_gas - consumption; vctx_memory_usage = memory_usage |>)
  | InstructionToEnvironment act v opt ->
    InstructionToEnvironment act (<|v with vctx_gas = v.vctx_gas - consumption; vctx_memory_usage = memory_usage |>) opt
  end

val signextend : w256 -> w256 -> w256
let signextend len w =
  if uint len >= 31 then
    w
  else
    let len : nat = 8 * ((natFromNatural (word256ToNatural len)) + 1) in
    let mask : word256 = 2 ** len - 1 in
    let masked : word256 = w land mask in
    let middle : word256 = 2 ** (len - 1) in
    if masked < middle then masked
    else masked - middle - middle

val combine_w8s_to_nat: w8 -> w8 -> nat
let combine_w8s_to_nat v1 v2 =
  natFromNatural (word8ToNatural v1) * 256 + natFromNatural (word8ToNatural v2)

val jumpsub : variable_ctx -> constant_ctx -> w8 -> w8 -> instruction_result
let jumpsub v c a1 a2 =
  let new_pc = combine_w8s_to_uint a1 a2 in
  let pc =  v.vctx_pc in
  let v_new = <| v  with vctx_return_stack = pc + integerFromInt (inst_size (Evm15 (JUMPSUB a1 a2))) :: v.vctx_return_stack ;
                     vctx_pc = new_pc |> in
  match vctx_next_instruction v_new c with
    | Just (Evm15 (BEGINSUB _ _ _ _)) -> InstructionContinue v_new
    | _ -> instruction_failure_result v [InvalidJumpDestination]
  end

val beginsub : variable_ctx -> constant_ctx -> w8 -> w8 -> w8 -> w8 -> instruction_result
let beginsub v c na1 na2 _ _ =
  let nargs = combine_w8s_to_nat na1 na2 in
  let sp = List.length (v.vctx_stack) in
  (* sp - nargs == number of elements on the stack before the arguments were pushed *)
  if sp >= nargs then
    let v = <| v  with vctx_frame_stack = (sp - nargs) :: v.vctx_frame_stack |> in
    stack_0_0_op v c
  else
    instruction_failure_result v [TooShortStack]

val returnsub : variable_ctx -> constant_ctx -> instruction_result
let returnsub v _ = match (v.vctx_return_stack, v.vctx_frame_stack) with
 | (new_pc :: rs_tl, _ :: fs_tl) ->
    InstructionContinue (<| v with vctx_pc = new_pc; vctx_return_stack = rs_tl; vctx_frame_stack = fs_tl |>)
 | (_,_) -> instruction_failure_result v [TooShortStack]
end

val getlocal : variable_ctx -> constant_ctx -> w8 -> w8 -> instruction_result
let getlocal v c i1 i2 =
  let idx = combine_w8s_to_nat i1 i2 in
  match List.index v.vctx_frame_stack 0 with
  | Just fp ->
    let rev_stk = List.reverse (v.vctx_stack) in
    match List.index rev_stk (fp + idx) with
    | Just el ->
      stack_0_1_op v c el
    | _ -> instruction_failure_result v [TooShortStack]
    end
  | _ -> instruction_failure_result v [ShouldNotHappen]
 end

val putlocal : variable_ctx -> constant_ctx -> w8 -> w8 -> instruction_result
let putlocal v c i1 i2 =
  let idx = combine_w8s_to_nat i1 i2 in
  match List.index v.vctx_frame_stack 0 with
  | Just fp ->
    match v.vctx_stack with
    | el::stk ->
      let new_stk = List.reverse (List.update (List.reverse stk) (fp + idx) el) in
      let new_v = <| v with vctx_stack = new_stk |> in
      stack_0_1_op new_v c el
    | _ -> instruction_failure_result v [TooShortStack]
    end
  | _ -> instruction_failure_result v [ShouldNotHappen]
 end

(* Finally, using the above definitions, I can define a function that operates an instruction *)
(* on the execution environments. *)
val instruction_sem : variable_ctx -> constant_ctx -> inst -> network -> instruction_result
let instruction_sem v c inst net =
  subtract_gas (meter_gas inst v c net) (new_memory_consumption inst v.vctx_memory_usage (vctx_stack_default 0 v) (vctx_stack_default 1 v) (vctx_stack_default 2 v) (vctx_stack_default 3 v) (vctx_stack_default 4 v) (vctx_stack_default 5 v) (vctx_stack_default 6 v))
  (match inst with
  | Stack (PUSH_N lst) -> stack_0_1_op v c (word_of_bytes (constant_mark lst))
  | Unknown _ -> instruction_failure_result v [ShouldNotHappen]
  | Storage SLOAD -> stack_1_1_op v c v.vctx_storage
  | Storage SSTORE -> sstore v c
  | Pc JUMPI -> jumpi v c
  | Pc JUMP -> jump v c
  | Pc JUMPDEST -> stack_0_0_op v c
  | Evm15 (JUMPTO a1 a2) -> jumpto v c a1 a2
  | Evm15 (JUMPIF a1 a2) -> jumpif v c a1 a2
  | Evm15 (BEGINSUB na1 na2 nr1 nr2) -> beginsub v c na1 na2 nr1 nr2
  | Evm15 (JUMPSUB a1 a2) -> jumpsub v c a1 a2
  | Evm15 (RETURNSUB) -> returnsub v c
  | Evm15 (GETLOCAL i1 i2) -> getlocal v c i1 i2
  | Evm15 (PUTLOCAL i1 i2) -> putlocal v c i1 i2
  | 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_w256 v.vctx_caller)
  | Arith ADD -> stack_2_1_op v c (fun a b -> a + b)
  | Arith SUB -> stack_2_1_op v c (fun a b -> a - b)
  | Arith ISZERO -> stack_1_1_op v c (fun a -> if a = 0 then 1 else 0)
  | Misc CALL -> call net v c
  | Misc RETURN -> ret v c
  | Misc STOP -> stop v c
  | Dup n -> general_dup n v c
  | Stack POP -> pop v c
  | Info GASLIMIT -> stack_0_1_op v c v.vctx_block.block_gaslimit
  | Arith inst_GT -> stack_2_1_op v c (fun a b -> if word256UGT a b then 1 else 0)
  | Arith inst_EQ -> stack_2_1_op v c (fun a b -> if a = b then 1 else 0)
  | Bits inst_AND -> stack_2_1_op v c (fun a b -> a land b)
  | Bits inst_OR -> stack_2_1_op v c (fun a b -> a lor b)
  | Bits inst_XOR -> stack_2_1_op v c (fun a b -> a lxor b)
  | Bits inst_NOT -> stack_1_1_op v c (fun a -> lnot a)
  | Bits BYTE -> stack_2_1_op v c get_byte
  | Sarith SDIV -> stack_2_1_op v c
       (fun n divisor -> if divisor = 0 then 0 else
                         let divisor = sintFromW256 divisor in
                         let n = sintFromW256 n in
                         let min_int : integer = ~ (2 ** 255) in
                         if n = min_int && divisor = ~1 then word256FromInteger min_int else
                         if divisor < 0 then
                           (if n < 0 then
                              word256FromInteger ((~1 * n) div (~1 * divisor))
                            else
                              word256FromInteger (~1 * (n div (~1 * divisor)))
                           )
                         else
                           (if n < 0 then
                              word256FromInteger (~1 * ((~1 * n) div divisor))
                            else
                              word256FromInteger (n div divisor))
                           )
  | Sarith SMOD -> stack_2_1_op v c
       (fun n divisor -> if divisor = 0 then 0 else
                         let divisor = sintFromW256 divisor in
                         let n = sintFromW256 n in
                         if divisor < 0 then
                           (if n < 0 then
                              word256FromInteger (~1 * ((~1 * n) mod (~1 * divisor)))
                            else
                              word256FromInteger (n mod (~1 * divisor))
                           )
                         else
                           (if n < 0 then
                              word256FromInteger (~1 * ((~1 * n) mod divisor))
                            else
                              word256FromInteger (n mod divisor))
                           )
  | Sarith SGT -> stack_2_1_op v c
       (fun elm0 elm1 -> if elm0 > elm1 then 1 else 0)
  | Sarith SLT -> stack_2_1_op v c
       (fun elm0 elm1 -> if elm0 < elm1 then 1 else 0)
  | Sarith SIGNEXTEND -> stack_2_1_op v c signextend
  | Arith MUL -> stack_2_1_op v c
       (fun a b -> a * b)
  | Arith DIV -> stack_2_1_op v c
       (fun a divisor -> (if divisor = 0 then 0 else word256FromInteger ((uint a) div (uint divisor))))
  | Arith MOD -> stack_2_1_op v c
       (fun a divisor -> (if divisor = 0 then 0 else
            word256FromInteger ((uint a) mod (uint divisor))
        ))
  | Arith ADDMOD -> stack_3_1_op v c
       (fun a b divisor ->
           (if divisor = 0 then 0 else word256FromInteger ((uint a + uint b) mod (uint divisor))))
  | Arith MULMOD -> stack_3_1_op v c
       (fun a b divisor ->
           (if divisor = 0 then 0 else word256FromInteger ((uint a * uint b) mod (uint divisor))))
  | Arith EXP -> stack_2_1_op v c (fun a exponent -> word256FromInteger (word_exp (uint a) (word256ToNatural exponent)))
  | Arith inst_LT -> stack_2_1_op v c (fun arg0 arg1 -> if word256UGT arg1 arg0 then 1 else 0)
  | Arith SHA3 -> sha3 v c
  | Info ADDRESS -> stack_0_1_op v c (address_to_w256 c.cctx_this)
  | Info BALANCE -> stack_1_1_op v c (fun addr -> v.vctx_balance (w256_to_address addr))
  | Info ORIGIN -> stack_0_1_op v c (address_to_w256 v.vctx_origin)
  | Info CALLVALUE -> stack_0_1_op v c v.vctx_value_sent
  | Info CODESIZE -> stack_0_1_op v c (word256FromInteger c.cctx_program.program_length)
  | Info GASPRICE -> stack_0_1_op v c v.vctx_gasprice
  | Info EXTCODESIZE -> stack_1_1_op v c
       (fun arg -> word256FromInteger (v.vctx_ext_program (w256_to_address arg)).program_length)
  | Info BLOCKHASH -> stack_1_1_op v c v.vctx_block.block_blockhash
  | Info COINBASE -> stack_0_1_op v c (address_to_w256 v.vctx_block.block_coinbase)
  | Info TIMESTAMP -> stack_0_1_op v c v.vctx_block.block_timestamp
  | Info NUMBER -> stack_0_1_op v c v.vctx_block.block_number
  | Info DIFFICULTY -> stack_0_1_op v c v.vctx_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 (word4ToNat n) v c
  | Misc CREATE -> create v c
  | Misc CALLCODE -> callcode net v c
  | Misc SUICIDE -> suicide v c
  | Misc DELEGATECALL ->
     if before_homestead net then instruction_failure_result v [ShouldNotHappen] else delegatecall net v c
  | Info GAS -> stack_0_1_op v c (gas v - 2)
  | Memory MSIZE -> stack_0_1_op v c (32 * word256FromInteger v.vctx_memory_usage)
  end)

(* subsection {* Programs' Answer to the Environment *} *)

(* Execution of a program is harder than that of instructions.  The biggest difficulty is that *)
(* the length of the execution is arbitrary.  In Isabelle/HOL all functions must terminate, so I need *)
(* to prove the termination of program execution.  In priciple, I could have used gas, but I was *)
(* lazy to model gas at that moment, so I introduced an artificial step counter.  When I prove theorems *)
(* about smart contracts, the theorems are of the form ``for any value of the initial step counter, *)
(* this and that never happen.'' *)

val next_state: (instruction_result -> unit) -> constant_ctx -> network -> instruction_result -> instruction_result
let next_state stopper c net pr =
  match pr with
  | InstructionToEnvironment _ _ _ ->
    let () = stopper pr in pr
  | InstructionContinue v ->
     match vctx_next_instruction v c with
      | Nothing -> InstructionToEnvironment (ContractFail [ShouldNotHappen]) v Nothing
      | Just i ->
        (*
        prerr_endline ("Inst " ^ String.concat "," (List.map (fun x -> Z.format "%x" (word8ToNatural x)) (inst_code i)));
        *)
        if check_resources v c v.vctx_stack i net then
          instruction_sem v c i net
        else
          InstructionToEnvironment (ContractFail
              (match inst_stack_numbers i with
               | (consumed, produced) ->
                 (if (intFromNat (length v.vctx_stack) + produced - consumed <= 1024) then [] else [TooLongStack])
                  ++ (if meter_gas i v c net <= v.vctx_gas then [] else [OutOfGas])
               end
              ))
              v Nothing
     end
  end

(* The program execution takes a counter. *)
(* One counter is decremented for each instruction. *)
(* The other counter is decremented when a backward-jump happens. *)
(* This setup allows an easy termination proof. *)
(* Also, during the proofs, I can do case analysis on the number of backwad jumps *)
(* rather than the number of instructions. *)

val program_sem :  (instruction_result -> unit) -> constant_ctx -> nat -> network -> instruction_result -> instruction_result
let rec program_sem stopper c fuel net pr =
match fuel with
 | 0 -> pr
 | fuel_pred + 1 -> program_sem stopper c fuel_pred net (next_state stopper c net pr)
end
declare termination_argument program_sem = automatic


val program_sem_t: constant_ctx -> network -> instruction_result -> instruction_result
let rec ~{coq} program_sem_t c net p =
  match p with
  | InstructionToEnvironment _ _ _ -> p
  | InstructionContinue v ->
     match vctx_next_instruction v c with
      | Nothing -> InstructionToEnvironment (ContractFail [ShouldNotHappen]) v Nothing
      | Just i ->
        if check_resources v c v.vctx_stack i net then
          (* This if is required to prove that vctx_gas is stictly decreasing on program_sem's recursion *)
          (if v.vctx_gas <= 0 then
              instruction_sem v c i net
          else  program_sem_t c net (instruction_sem v c i net))
        else
          InstructionToEnvironment (ContractFail
              (match inst_stack_numbers i with
               | (consumed, produced) ->
                 (if (intFromNat (length v.vctx_stack) + produced - consumed <= 1024) then [] else [TooLongStack])
                  ++ (if meter_gas i v c net <= v.vctx_gas then [] else [OutOfGas])
               end
              ))
              v Nothing
     end
     end
declare termination_argument program_sem_t = manual


(* subsection {* Account's State *} *)

(* In the bigger picture, a contract invocation changes accounts' states. *)
(* An account has a storage, a piece of code and a balance. *)
(* Since I am interested in account states in the middle of a transaction, I also need to *)
(* keep track of the ongoing executions of a single account.  Also I need to keep track of *)
(* a flag indicating if the account has already marked for erasure. *)

type account_state = <|
  account_address : address;
  account_storage : storage;
  account_code : program;
  account_balance : w256;
  account_ongoing_calls : list (variable_ctx * integer * integer);
    (* the variable environments that are executing on this account, but waiting for calls to finish *)
  account_killed : bool;
    (* the boolean that indicates the account has executed SUICIDE in this transaction. *)
  (* The flag causes a destruction of the contract at the end of a transaction. *)
|>

(* subsection {* Environment Construction before EVM Execution *} *)

(* I need to connect the account state and the program execution environments. *)
(* First I construct program execution environments from an account state. *)

(* Similarly we can construct the constant environment. *)
(* Construction of the constant environment is much simpler than that of *)
(* a variable environment. *)

val build_cctx : account_state -> constant_ctx
let build_cctx a =
  <| cctx_program = a.account_code; cctx_this = a.account_address; cctx_hash_filter = (fun _ -> true) |>

(* Next we turn to the case where the environment returns back to the account after the account has *)
(* called an account.  In this case, the account should contain one ongoing execution that is waiting *)
(* for a call to return. *)

(* An instruction is ``call-like'' when it calls an account and waits for it to return. *)

val is_call_like : maybe inst -> bool
let is_call_like i = (i = Just (Misc CALL) || i = Just (Misc DELEGATECALL)
                 || i = Just (Misc CALLCODE) || i = Just (Misc CREATE))

val build_vctx_failed : account_state -> maybe variable_ctx
let build_vctx_failed a = match a.account_ongoing_calls with
 | [] -> Nothing
 | (recovered,_,_) :: _ ->
      if is_call_like ((a.account_code).program_content (recovered.vctx_pc - 1)) then
      Just (<| recovered with vctx_stack = 0 :: recovered.vctx_stack |>) (* 0 is pushed, indicating failure*)
      else Nothing
end

val account_state_pop_ongoing_call : account_state -> account_state
let account_state_pop_ongoing_call orig = match orig.account_ongoing_calls with
 | _ :: tl -> <| orig with account_ongoing_calls = tl |>
 | _ -> <| orig with account_ongoing_calls = [] |>
end

(* Second I define the empty account, which replaces an account that has *)
(* destroyed itself. *)

val empty_account : address -> account_state
let empty_account addr =
 <| account_address = addr;
    account_storage = empty_storage;
   account_code = empty_program;
   account_balance = 0;
   account_ongoing_calls = [];
   account_killed = false;
 |>

(* And after our contract makes a move, the account state is updated as follows. *)

val update_account_state :
  account_state -> contract_action -> variable_ctx -> maybe (integer * integer) -> account_state
let update_account_state prev act v v_opt =
   let st = (match act with ContractFail _ -> v.vctx_storage_at_call | _ -> v.vctx_storage end) in
   let bal = (match act with ContractFail _ -> v.vctx_balance_at_call | _ -> v.vctx_balance end) in
   <| prev with
     account_storage = st;
     account_balance = (match act with ContractFail _ -> prev.account_balance
                                   |  _ -> bal prev.account_address end);
     account_ongoing_calls =
                        (match v_opt with Nothing -> prev.account_ongoing_calls
                                     | Just (i, s) -> (v, i, s) :: prev.account_ongoing_calls end);
     account_killed =
       (match act with ContractSuicide _ -> true
                  | _ -> prev.account_killed end)
    |>

type contract_behavior = contract_action * (account_state -> bool)

type response_to_environment = <|
  when_called : call_env -> contract_behavior;
  when_returned : return_result -> contract_behavior;
  when_failed : contract_behavior;
|>

val empty_memory : memory
let empty_memory = (fun _ -> 0)

(* Given an account state and a call from the environment *)
(* we can judge if a variable environment is possible or not.*)
(* The block state is arbitrary.  This means we verify properties that hold*)
(* on whatever block numbers and whatever difficulties and so on.*)
(* The origin of the transaction is also considered arbitrary.*)


indreln [build_vctx_called : account_state -> call_env -> variable_ctx -> bool]
  vctx_called : forall bal a env origin gasprice ext block gas existence.
    word256ToInteger block.block_number >= eip150_block && (* only the newest version of EVM matters *)
    bal a.account_address = a.account_balance ==>
    build_vctx_called a env
 <| vctx_stack = []; (* The stack is initialized for every invocation *)
    vctx_return_stack = [~1];
    vctx_frame_stack = [0];
    vctx_memory = empty_memory; (* The memory is also initialized for every invocation *)
     vctx_memory_usage = 0; (* The memory usage is initialized. *)
     vctx_storage = a.account_storage; (* The storage is taken from the account state *)
     vctx_pc = 0; (* The program counter is initialized to zero *)
     vctx_balance = (fun (addr:address) ->
                         if addr = a.account_address
                           then 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. *)
     vctx_caller = env.callenv_caller; (* the caller is specified by the environment *)
     vctx_value_sent = env.callenv_value; (* the sent value is specified by the environment *)
     vctx_data_sent = env.callenv_data; (* the sent data is specified by the environment *)
     vctx_storage_at_call = a.account_storage; (* the snapshot of the storage is remembered in case of failure *)
     vctx_balance_at_call = bal; (* the snapshot of the balance is remembered in case of failure *)
     vctx_origin = origin; (* the origin of the transaction is arbitrarily chosen *)
     vctx_gasprice = gasprice; (* the gasprice of the transaction is arbitrarily chosen *)
     vctx_ext_program = ext; (* the codes of the external programs are arbitrary. *)
     vctx_block = block; (* the block information is chosen arbitrarily. *)
     vctx_gas = gas; (* the amount of gas is chosen arbitrarily. *)
     vctx_account_existence = existence; (* existence is chosen arbitrarily *)
     vctx_touched_storage_index = [];
     vctx_refund = 0;
     vctx_logs = []
   |>

(* When an account returns to our contract, the variable environment is *)
(* recovered from the stack of the ongoing calls.  However, due to reentrancy, *)
(* the balance and the storage of our contract might have changed.  So the *)
(* balance and the storage are taken from the account state provided. *)
(* Moreover, the balance of *)
(* our contract might increase because some other contracts might have destroyed themselves, *)
(* transferring value to our contract.*)

indreln [build_vctx_returned : account_state -> return_result -> variable_ctx -> bool]
vctx_returned:
   forall a_code v_pc new_bal a_bal a_addr a_storage v_stack v_return_stack v_frame_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_gasprice v_ext_program v_ext_program' v_block v_gas v_gas' mem_start mem_size
          r rest whichever v_ex v_ex' v_touched v_logs v_refund.
   (is_call_like (a_code.program_content (v_pc - 1))) &&
   (word256UGE new_bal a_bal) ==> (* the balance might have increased *)
   build_vctx_returned

     (* here is the first argument *)
     <| account_address = a_addr (* all elements are spelled out for performance *)
     ; account_storage = a_storage
     ; account_code = a_code
     ; account_balance = a_bal
     ; account_ongoing_calls =
         ((<| vctx_stack = v_stack
         ; vctx_return_stack = v_return_stack
         ; vctx_frame_stack = v_frame_stack
         ; vctx_memory = v_memory
         ; vctx_memory_usage = v_memory_usage
         ; vctx_storage = v_storage
         ; vctx_pc = v_pc
         ; vctx_balance = v_balance
         ; vctx_caller = v_caller
         ; vctx_value_sent = v_value
         ; vctx_data_sent = v_data
         ; vctx_storage_at_call = v_init_storage
         ; vctx_balance_at_call = v_init_balance
         ; vctx_origin = v_origin
         ; vctx_gasprice = v_gasprice
         ; vctx_ext_program = v_ext_program
         ; vctx_block = v_block
         ; vctx_gas = v_gas
         ; vctx_account_existence = v_ex
         ; vctx_touched_storage_index = v_touched
         ; vctx_logs = v_logs
         ; vctx_refund = v_refund
         |>, mem_start, mem_size) :: rest)
     ; account_killed = whichever
     |>

     (* here is the second argument *)
     r

     (* here is the third argument *)
     (<| vctx_stack = 1 :: v_stack (* 1 is pushed, indicating a return *)
       ; vctx_return_stack = v_return_stack
       ; vctx_frame_stack = v_frame_stack
       ; vctx_memory =
         put_return_values v_memory r.return_data mem_start mem_size
       ; vctx_memory_usage = v_memory_usage
       ; vctx_storage = a_storage
       ; vctx_pc = v_pc
       ; vctx_balance = (update_balance a_addr
                            (fun _ -> new_bal) r.return_balance)
       ; vctx_caller = v_caller
       ; vctx_value_sent = v_value
       ; vctx_data_sent = v_data
       ; vctx_storage_at_call = v_init_storage
       ; vctx_balance_at_call = v_init_balance
       ; vctx_origin = v_origin
       ; vctx_gasprice = v_gasprice
       ; vctx_ext_program = v_ext_program'
       ; vctx_block = v_block
       ; vctx_gas = v_gas' (* safe approximation.  saving proof space *)
       ; vctx_account_existence = v_ex'
       ; vctx_touched_storage_index = v_touched
       ; vctx_logs = v_logs
       ; vctx_refund = v_refund
      |>)