Library EVMOpSem.block
Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.
Require Import Lem.coqharness.
Open Scope nat_scope.
Open Scope string_scope.
Require Import Lem.lem_pervasives.
Require Export Lem.lem_pervasives.
Require Import word8.
Require Export word8.
Require Import word160.
Require Export word160.
Require Import word256.
Require Export word256.
Require Import keccak.
Require Export keccak.
Require Import evm.
Require Export evm.
Require Import rlplem.
Require Export rlplem.
Record transaction : Type := {
tr_from : address ;
tr_to : option address ;
tr_gas_limit : w256 ;
tr_gas_price : w256 ;
tr_value : w256 ;
tr_nonce : w256 ;
tr_data : list word8
}.
Notation "{[ r 'with' 'tr_from' := e ]}" := ({| tr_from := e; tr_to := tr_to r; tr_gas_limit := tr_gas_limit r; tr_gas_price := tr_gas_price r; tr_value := tr_value r; tr_nonce := tr_nonce r; tr_data := tr_data r |}).
Notation "{[ r 'with' 'tr_to' := e ]}" := ({| tr_to := e; tr_from := tr_from r; tr_gas_limit := tr_gas_limit r; tr_gas_price := tr_gas_price r; tr_value := tr_value r; tr_nonce := tr_nonce r; tr_data := tr_data r |}).
Notation "{[ r 'with' 'tr_gas_limit' := e ]}" := ({| tr_gas_limit := e; tr_from := tr_from r; tr_to := tr_to r; tr_gas_price := tr_gas_price r; tr_value := tr_value r; tr_nonce := tr_nonce r; tr_data := tr_data r |}).
Notation "{[ r 'with' 'tr_gas_price' := e ]}" := ({| tr_gas_price := e; tr_from := tr_from r; tr_to := tr_to r; tr_gas_limit := tr_gas_limit r; tr_value := tr_value r; tr_nonce := tr_nonce r; tr_data := tr_data r |}).
Notation "{[ r 'with' 'tr_value' := e ]}" := ({| tr_value := e; tr_from := tr_from r; tr_to := tr_to r; tr_gas_limit := tr_gas_limit r; tr_gas_price := tr_gas_price r; tr_nonce := tr_nonce r; tr_data := tr_data r |}).
Notation "{[ r 'with' 'tr_nonce' := e ]}" := ({| tr_nonce := e; tr_from := tr_from r; tr_to := tr_to r; tr_gas_limit := tr_gas_limit r; tr_gas_price := tr_gas_price r; tr_value := tr_value r; tr_data := tr_data r |}).
Notation "{[ r 'with' 'tr_data' := e ]}" := ({| tr_data := e; tr_from := tr_from r; tr_to := tr_to r; tr_gas_limit := tr_gas_limit r; tr_gas_price := tr_gas_price r; tr_value := tr_value r; tr_nonce := tr_nonce r |}).
Definition transaction_default: transaction := {| tr_from := address_default; tr_to := DAEMON; tr_gas_limit := w256_default; tr_gas_price := w256_default; tr_value := w256_default; tr_nonce := w256_default; tr_data := DAEMON |}.
Record block_account : Type := {
block_account_address : address ;
block_account_storage : storage ;
block_account_code : program ;
block_account_balance : w256 ;
block_account_nonce : w256 ;
block_account_exists : bool ;
block_account_hascode : bool
}.
Notation "{[ r 'with' 'block_account_address' := e ]}" := ({| block_account_address := e; block_account_storage := block_account_storage r; block_account_code := block_account_code r; block_account_balance := block_account_balance r; block_account_nonce := block_account_nonce r; block_account_exists := block_account_exists r; block_account_hascode := block_account_hascode r |}).
Notation "{[ r 'with' 'block_account_storage' := e ]}" := ({| block_account_storage := e; block_account_address := block_account_address r; block_account_code := block_account_code r; block_account_balance := block_account_balance r; block_account_nonce := block_account_nonce r; block_account_exists := block_account_exists r; block_account_hascode := block_account_hascode r |}).
Notation "{[ r 'with' 'block_account_code' := e ]}" := ({| block_account_code := e; block_account_address := block_account_address r; block_account_storage := block_account_storage r; block_account_balance := block_account_balance r; block_account_nonce := block_account_nonce r; block_account_exists := block_account_exists r; block_account_hascode := block_account_hascode r |}).
Notation "{[ r 'with' 'block_account_balance' := e ]}" := ({| block_account_balance := e; block_account_address := block_account_address r; block_account_storage := block_account_storage r; block_account_code := block_account_code r; block_account_nonce := block_account_nonce r; block_account_exists := block_account_exists r; block_account_hascode := block_account_hascode r |}).
Notation "{[ r 'with' 'block_account_nonce' := e ]}" := ({| block_account_nonce := e; block_account_address := block_account_address r; block_account_storage := block_account_storage r; block_account_code := block_account_code r; block_account_balance := block_account_balance r; block_account_exists := block_account_exists r; block_account_hascode := block_account_hascode r |}).
Notation "{[ r 'with' 'block_account_exists' := e ]}" := ({| block_account_exists := e; block_account_address := block_account_address r; block_account_storage := block_account_storage r; block_account_code := block_account_code r; block_account_balance := block_account_balance r; block_account_nonce := block_account_nonce r; block_account_hascode := block_account_hascode r |}).
Notation "{[ r 'with' 'block_account_hascode' := e ]}" := ({| block_account_hascode := e; block_account_address := block_account_address r; block_account_storage := block_account_storage r; block_account_code := block_account_code r; block_account_balance := block_account_balance r; block_account_nonce := block_account_nonce r; block_account_exists := block_account_exists r |}).
Definition block_account_default: block_account := {| block_account_address := address_default; block_account_storage := storage_default; block_account_code := program_default; block_account_balance := w256_default; block_account_nonce := w256_default; block_account_exists := bool_default; block_account_hascode := bool_default |}.
Definition build_cctx0 (a : block_account ) : constant_ctx :=
{|cctx_program :=(block_account_code a);cctx_this :=(block_account_address a);cctx_hash_filter := (fun ( _ : list (keccak.byte )) => true) |}.
Definition empty_account0 (addr : word160 ) : block_account := {|block_account_address := addr;block_account_storage := empty_storage;block_account_code := empty_program;block_account_balance :=(word256FromNumeral 0%nat);block_account_exists := false;block_account_nonce :=(word256FromNumeral 0%nat);block_account_hascode := true
|}.
Definition world_state : Type := address -> block_account .
Definition world_state_default: world_state := (fun (x120 : address ) => block_account_default).
Definition empty_state {a : Type} ( _ : a) : address -> block_account := empty_account0.
Record receipt : Type := {
receipt_state : world_state ;
receipt_cumulative_gas : w256 ;
receipt_bloom : w256 ;
receipt_logs : list log_entry
}.
Notation "{[ r 'with' 'receipt_state' := e ]}" := ({| receipt_state := e; receipt_cumulative_gas := receipt_cumulative_gas r; receipt_bloom := receipt_bloom r; receipt_logs := receipt_logs r |}).
Notation "{[ r 'with' 'receipt_cumulative_gas' := e ]}" := ({| receipt_cumulative_gas := e; receipt_state := receipt_state r; receipt_bloom := receipt_bloom r; receipt_logs := receipt_logs r |}).
Notation "{[ r 'with' 'receipt_bloom' := e ]}" := ({| receipt_bloom := e; receipt_state := receipt_state r; receipt_cumulative_gas := receipt_cumulative_gas r; receipt_logs := receipt_logs r |}).
Notation "{[ r 'with' 'receipt_logs' := e ]}" := ({| receipt_logs := e; receipt_state := receipt_state r; receipt_cumulative_gas := receipt_cumulative_gas r; receipt_bloom := receipt_bloom r |}).
Definition receipt_default: receipt := {| receipt_state := world_state_default; receipt_cumulative_gas := w256_default; receipt_bloom := w256_default; receipt_logs := DAEMON |}.
Definition start_env (a : block_account ) (state : word160 -> block_account ) (args : call_arguments ) (caller : word160 ) (origin : word160 ) (gasprice : (Bvector 256) ) (block : block_info ) : variable_ctx :=
{|vctx_stack := [];vctx_memory := empty_memory;vctx_memory_usage :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));vctx_storage :=(block_account_storage a);vctx_pc :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));vctx_balance := (fun (addr:address ) =>(block_account_balance (state addr)));vctx_caller := caller;vctx_value_sent :=(callarg_value args);vctx_data_sent :=(callarg_data args);vctx_storage_at_call :=(block_account_storage a);vctx_balance_at_call := (fun (addr:address ) =>(block_account_balance (state addr)));vctx_origin := origin;vctx_gasprice := gasprice;vctx_ext_program := (fun (addr:address ) =>(block_account_code (state addr)));vctx_block := block;vctx_gas := (uint(callarg_gas args));vctx_account_existence := (fun (addr:address ) =>(block_account_exists (state addr)));vctx_touched_storage_index := [];vctx_logs := [];vctx_refund :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))))
|}.
Definition create_env (a : block_account ) (state : word160 -> block_account ) (value1 : (Bvector 256) ) (data : list (keccak.byte )) (gas1 : Z ) (caller : word160 ) (origin : word160 ) (gasprice : (Bvector 256) ) (block : block_info ) : variable_ctx :=
{|vctx_stack := [];vctx_memory := empty_memory;vctx_memory_usage :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));vctx_storage :=(block_account_storage a);vctx_pc :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));vctx_balance := (fun (addr:address ) =>(block_account_balance (state addr)));vctx_caller := caller;vctx_value_sent := value1;vctx_data_sent := data;vctx_storage_at_call :=(block_account_storage a);vctx_balance_at_call := (fun (addr:address ) =>(block_account_balance (state addr)));vctx_origin := origin;vctx_gasprice := gasprice;vctx_ext_program := (fun (addr:address ) =>(block_account_code (state addr)));vctx_block := block;vctx_gas := gas1;vctx_account_existence := (fun (addr:address ) =>(block_account_exists (state addr)));vctx_touched_storage_index := [];vctx_logs := [];vctx_refund :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))))
|}.
Definition vctx_update_from_world (v : variable_ctx ) (a : block_account ) (state : word160 -> block_account ) (called_v : variable_ctx ) : variable_ctx := {|vctx_storage :=(block_account_storage a);vctx_balance := (fun (addr:address ) =>(block_account_balance (state addr)));vctx_ext_program := (fun (addr:address ) =>(block_account_code (state addr)));vctx_gas := (Coq.ZArith.BinInt.Z.add(vctx_gas v)(vctx_gas called_v));vctx_refund := (Coq.ZArith.BinInt.Z.add(vctx_refund v)(vctx_refund called_v));vctx_logs := ((@ List.app _)(vctx_logs v)(vctx_logs called_v));vctx_account_existence := (fun (addr:address ) =>(block_account_exists (state addr)));vctx_stack :=(vctx_stack v);vctx_memory :=(vctx_memory v);vctx_memory_usage :=(vctx_memory_usage v);vctx_pc :=(vctx_pc v);vctx_caller :=(vctx_caller v);vctx_value_sent :=(vctx_value_sent v);vctx_data_sent :=(vctx_data_sent v);vctx_storage_at_call :=(vctx_storage_at_call v);vctx_balance_at_call :=(vctx_balance_at_call v);vctx_origin :=(vctx_origin v);vctx_gasprice :=(vctx_gasprice v);vctx_block :=(vctx_block v);vctx_touched_storage_index :=(vctx_touched_storage_index v)
|}.
Definition byte_to_inst (b : word8 ) : inst := match ( word8ToNat b) with
| 0%nat => Misc STOP
| 22%nat => Bits inst_AND
| 23%nat => Bits inst_OR
| 24%nat => Bits inst_XOR
| 25%nat => Bits inst_NOT
| 26%nat => Bits BYTE
| 240%nat => Misc CREATE
| 241%nat => Misc CALL
| 242%nat => Misc CALLCODE
| 243%nat => Misc RETURN
| 244%nat => Misc DELEGATECALL
| 255%nat => Misc SUICIDE
| 160%nat => Log LOG0
| 161%nat => Log LOG1
| 162%nat => Log LOG2
| 163%nat => Log LOG3
| 164%nat => Log LOG4
| 53%nat => Stack CALLDATALOAD
| 80%nat => Stack POP
| 86%nat => Pc JUMP
| 87%nat => Pc JUMPI
| 88%nat => Pc PC
| 91%nat => Pc JUMPDEST
| 84%nat => Storage SLOAD
| 85%nat => Storage SSTORE
| 81%nat => Memory MLOAD
| 82%nat => Memory MSTORE
| 83%nat => Memory MSTORE8
| 55%nat => Memory CALLDATACOPY
| 57%nat => Memory CODECOPY
| 60%nat => Memory EXTCODECOPY
| 89%nat => Memory MSIZE
| 128%nat => Dup(word4.word4FromNumeral 0%nat)
| 129%nat => Dup(word4.word4FromNumeral 1%nat)
| 130%nat => Dup(word4.word4FromNumeral 2%nat)
| 131%nat => Dup(word4.word4FromNumeral 3%nat)
| 132%nat => Dup(word4.word4FromNumeral 4%nat)
| 133%nat => Dup(word4.word4FromNumeral 5%nat)
| 134%nat => Dup(word4.word4FromNumeral 6%nat)
| 135%nat => Dup(word4.word4FromNumeral 7%nat)
| 136%nat => Dup(word4.word4FromNumeral 8%nat)
| 137%nat => Dup(word4.word4FromNumeral 9%nat)
| 138%nat => Dup(word4.word4FromNumeral 10%nat)
| 139%nat => Dup(word4.word4FromNumeral 11%nat)
| 140%nat => Dup(word4.word4FromNumeral 12%nat)
| 141%nat => Dup(word4.word4FromNumeral 13%nat)
| 142%nat => Dup(word4.word4FromNumeral 14%nat)
| 143%nat => Dup(word4.word4FromNumeral 15%nat)
| 144%nat => Swap(word4.word4FromNumeral 0%nat)
| 145%nat => Swap(word4.word4FromNumeral 1%nat)
| 146%nat => Swap(word4.word4FromNumeral 2%nat)
| 147%nat => Swap(word4.word4FromNumeral 3%nat)
| 148%nat => Swap(word4.word4FromNumeral 4%nat)
| 149%nat => Swap(word4.word4FromNumeral 5%nat)
| 150%nat => Swap(word4.word4FromNumeral 6%nat)
| 151%nat => Swap(word4.word4FromNumeral 7%nat)
| 152%nat => Swap(word4.word4FromNumeral 8%nat)
| 153%nat => Swap(word4.word4FromNumeral 9%nat)
| 154%nat => Swap(word4.word4FromNumeral 10%nat)
| 155%nat => Swap(word4.word4FromNumeral 11%nat)
| 156%nat => Swap(word4.word4FromNumeral 12%nat)
| 157%nat => Swap(word4.word4FromNumeral 13%nat)
| 158%nat => Swap(word4.word4FromNumeral 14%nat)
| 159%nat => Swap(word4.word4FromNumeral 15%nat)
| 48%nat => Info ADDRESS
| 49%nat => Info BALANCE
| 50%nat => Info ORIGIN
| 52%nat => Info CALLVALUE
| 54%nat => Info CALLDATASIZE
| 51%nat => Info CALLER
| 56%nat => Info CODESIZE
| 58%nat => Info GASPRICE
| 59%nat => Info EXTCODESIZE
| 64%nat => Info BLOCKHASH
| 65%nat => Info COINBASE
| 66%nat => Info TIMESTAMP
| 67%nat => Info NUMBER
| 68%nat => Info DIFFICULTY
| 69%nat => Info GASLIMIT
| 90%nat => Info GAS
| 1%nat => Arith ADD
| 2%nat => Arith MUL
| 3%nat => Arith SUB
| 4%nat => Arith DIV
| 6%nat => Arith MOD
| 8%nat => Arith ADDMOD
| 9%nat => Arith MULMOD
| 10%nat => Arith EXP
| 17%nat => Arith inst_GT
| 16%nat => Arith inst_LT
| 20%nat => Arith inst_EQ
| 21%nat => Arith ISZERO
| 32%nat => Arith SHA3
| 5%nat => Sarith SDIV
| 7%nat => Sarith SMOD
| 19%nat => Sarith SGT
| 18%nat => Sarith SLT
| 11%nat => Sarith SIGNEXTEND
| _ =>
if w8Greater b(word8FromNumeral 95%nat) && w8LessEqual b(word8Add(word8FromNumeral 95%nat)(word8FromNumeral 32%nat)) then Stack (PUSH_N (replicate (Z.abs_nat (word8ToInt (word8Minus b(word8FromNumeral 95%nat))))(word8FromNumeral 0%nat))) else
Unknown b
end.
Definition inst_to_byte (inst1 : inst ) : word8 := match ( inst1) with
| Unknown byte2 => byte2
| 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 => match ( index (stack_inst_code s)( 0%nat)) with None =>(word8FromNumeral 0%nat) | Some x => x end
| Swap s => swap_inst_code s
| Log l => log_inst_code l
| Misc m => misc_inst_code m
end.
Program Fixpoint fix_push (lst : list (inst )) : list (inst ):= match ( lst) with
| [] => []
| Stack( PUSH_N lst) :: tl => Stack (PUSH_N (List.map inst_to_byte (take (List.length lst) tl))) :: fix_push tl
| a :: tl => a :: fix_push tl
end.
Definition bytelist_to_instlist (lst : list (word8 )) : list (inst ):= fix_push (List.map byte_to_inst lst).
Inductive stack_hint : Type :=
| NoHint: stack_hint
| CreateAddress: address -> stack_hint
| ReturnTo: Z -> Z -> stack_hint .
Definition stack_hint_default: stack_hint := NoHint.
Record global : Type := {
g_orig : world_state ;
g_stack : list ((world_state * variable_ctx * constant_ctx * stack_hint ) % type);
g_current : world_state ;
g_cctx : constant_ctx ;
g_killed : list address ;
g_vmstate : instruction_result ;
g_create : bool
}.
Notation "{[ r 'with' 'g_orig' := e ]}" := ({| g_orig := e; g_stack := g_stack r; g_current := g_current r; g_cctx := g_cctx r; g_killed := g_killed r; g_vmstate := g_vmstate r; g_create := g_create r |}).
Notation "{[ r 'with' 'g_stack' := e ]}" := ({| g_stack := e; g_orig := g_orig r; g_current := g_current r; g_cctx := g_cctx r; g_killed := g_killed r; g_vmstate := g_vmstate r; g_create := g_create r |}).
Notation "{[ r 'with' 'g_current' := e ]}" := ({| g_current := e; g_orig := g_orig r; g_stack := g_stack r; g_cctx := g_cctx r; g_killed := g_killed r; g_vmstate := g_vmstate r; g_create := g_create r |}).
Notation "{[ r 'with' 'g_cctx' := e ]}" := ({| g_cctx := e; g_orig := g_orig r; g_stack := g_stack r; g_current := g_current r; g_killed := g_killed r; g_vmstate := g_vmstate r; g_create := g_create r |}).
Notation "{[ r 'with' 'g_killed' := e ]}" := ({| g_killed := e; g_orig := g_orig r; g_stack := g_stack r; g_current := g_current r; g_cctx := g_cctx r; g_vmstate := g_vmstate r; g_create := g_create r |}).
Notation "{[ r 'with' 'g_vmstate' := e ]}" := ({| g_vmstate := e; g_orig := g_orig r; g_stack := g_stack r; g_current := g_current r; g_cctx := g_cctx r; g_killed := g_killed r; g_create := g_create r |}).
Notation "{[ r 'with' 'g_create' := e ]}" := ({| g_create := e; g_orig := g_orig r; g_stack := g_stack r; g_current := g_current r; g_cctx := g_cctx r; g_killed := g_killed r; g_vmstate := g_vmstate r |}).
Definition global_default: global := {| g_orig := world_state_default; g_stack := DAEMON; g_current := world_state_default; g_cctx := constant_ctx_default; g_killed := DAEMON; g_vmstate := instruction_result_default; g_create := bool_default |}.
Record tr_result : Type := {
f_state : world_state ;
f_killed : list address ;
f_gas : Z ;
f_refund : Z ;
f_logs : list log_entry
}.
Notation "{[ r 'with' 'f_state' := e ]}" := ({| f_state := e; f_killed := f_killed r; f_gas := f_gas r; f_refund := f_refund r; f_logs := f_logs r |}).
Notation "{[ r 'with' 'f_killed' := e ]}" := ({| f_killed := e; f_state := f_state r; f_gas := f_gas r; f_refund := f_refund r; f_logs := f_logs r |}).
Notation "{[ r 'with' 'f_gas' := e ]}" := ({| f_gas := e; f_state := f_state r; f_killed := f_killed r; f_refund := f_refund r; f_logs := f_logs r |}).
Notation "{[ r 'with' 'f_refund' := e ]}" := ({| f_refund := e; f_state := f_state r; f_killed := f_killed r; f_gas := f_gas r; f_logs := f_logs r |}).
Notation "{[ r 'with' 'f_logs' := e ]}" := ({| f_logs := e; f_state := f_state r; f_killed := f_killed r; f_gas := f_gas r; f_refund := f_refund r |}).
Definition tr_result_default: tr_result := {| f_state := world_state_default; f_killed := DAEMON; f_gas := Z_default; f_refund := Z_default; f_logs := DAEMON |}.
Inductive global_state : Type :=
| Unimplemented: global_state
| Continue: global -> global_state
| Finished: tr_result -> global_state .
Definition global_state_default: global_state := Unimplemented.
Definition get_hint : option ((Z *Z ) % type) -> stack_hint :=
fun (x : option ((Z *Z ) % type) ) =>
match (x) with | Some (a, b) => ReturnTo a b | None => NoHint end.
Definition opt : Type := (nat -> option inst ).
Definition opt_default: opt := (fun (x119 : nat ) => DAEMON).
Definition make_opt (lst : list (byte0 )) : nat -> option (inst ) :=
let bytes := bytelist_to_instlist lst in
(fun (x : nat ) => lem_list.index bytes x).
Definition get_opt (m : nat -> option (inst ) ) (x : nat ) : option (inst ) := m x.
Definition codemap (lst : list (byte0 )) : Z -> option (inst ) :=
let m := make_opt lst in
(fun (x : Z ) => if int_ltb x((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then None else get_opt m (Z.abs_nat ( x))).
Definition make_program (bytes : list (byte0 )) : program := {|program_length := ((Z.pred (Z.pos (P_of_succ_nat (List.length bytes)))));program_content := (codemap bytes) |}.
Definition set_account_code (acc : block_account ) (bytes : list (byte0 )) : block_account := {[ acc with block_account_code := make_program bytes ]}.
Definition update_world (state : word160 -> block_account ) (a_addr : word160 ) (n_acc : block_account ) (a : word160 ) : block_account := if classical_boolean_equivalence a a_addr then n_acc else state a.
Definition sub_balance (state : word160 -> block_account ) (addr : word160 ) (value1 : (Bvector 256) ) : address -> block_account :=
let acc := state addr in
let acc := {[ acc with block_account_balance := word256Minus(block_account_balance acc) value1 ]} in
update_world state addr acc.
Definition add_balance (state : word160 -> block_account ) (addr : word160 ) (value1 : (Bvector 256) ) : address -> block_account :=
let acc := state addr in
let acc := {[ acc with block_account_balance := word256Add(block_account_balance acc) value1 ]} in
update_world state addr acc.
Definition update_return (state : address -> block_account ) (addr : word160 ) (v : variable_ctx ) : address -> block_account :=
update_world state addr ({[ (state addr) with block_account_storage :=(vctx_storage v) ]}).
Definition transfer_balance (state : word160 -> block_account ) (addr : word160 ) (recv : word160 ) (v : (Bvector 256) ) : address -> block_account :=
let state := sub_balance state addr v in
add_balance state recv v.
Definition update_call (state : word160 -> block_account ) (addr : word160 ) (args : call_arguments ) : address -> block_account := transfer_balance state addr(callarg_recipient args)(callarg_value args).
Definition update_nonce (state : word160 -> block_account ) (addr : word160 ) : address -> block_account :=
let acc := state addr in
update_world state addr ({[ acc with block_account_nonce := word256Add(block_account_nonce acc)(word256FromNumeral 1%nat) ]}).
Definition create_account (n_state : word160 -> block_account ) (new_addr : word160 ) (bytes : list (word8 )) : address -> block_account :=
let new_acc := {[ (n_state new_addr) with block_account_exists := true ]} in
let new_acc := set_account_code new_acc bytes in
update_world n_state new_addr new_acc.
Definition calc_address (addr : word160 ) (nonce : (Bvector 256) ) : word160 := w256_to_address (keccak (RLP (Node [RLP_address addr; RLP_w256 nonce]))).
Definition step (net : network ) : global_state -> global_state :=
fun (x : global_state ) =>
match (x) with | Finished st => Finished st | Unimplemented =>
Unimplemented | Continue global1 => let orig :=(g_orig global1) in
let c :=(g_cctx global1) in let state :=(g_current global1) in
match ((g_vmstate global1)) with
| InstructionToEnvironment act v stuff =>
match ( act) with | ContractCall args =>
if w160Less (callarg_recipient args) (word160FromNumeral 256%nat) then
Unimplemented else
let n_state := update_return state (cctx_this c) v in
if word256ULT (block_account_balance (n_state (cctx_this c)))
(callarg_value args) ||
nat_gtb (List.length (g_stack global1)) ( 1023%nat) then
let nv := {[ {[ v with vctx_gas := Coq.ZArith.BinInt.Z.add
(vctx_gas v)
(uint (callarg_gas args)) ]} with vctx_stack :=
(word256FromNumeral 0%nat) :: (vctx_stack v) ]} in
Continue
( {[{[ global1 with g_vmstate := InstructionContinue nv ]} with g_current := n_state ]})
else
let n_state := update_call n_state (cctx_this c) args in
let acc := n_state (callarg_recipient args) in
let cctx := {|cctx_this :=(callarg_recipient args);cctx_program :=(block_account_code (
n_state (callarg_code args)));cctx_hash_filter :=(cctx_hash_filter c) |} in
let nv := start_env acc n_state args (cctx_this c)
(vctx_origin v) (vctx_gasprice v) (vctx_block v) in
Continue
( {[ {[ {[{[ global1 with g_vmstate:=InstructionContinue nv ]} with g_cctx:=cctx ]} with g_current:=n_state ]} with g_stack:=(
(state,v,c,get_hint stuff) :: (g_stack global1)) ]})
| ContractDelegateCall args =>
let n_state := update_return state (cctx_this c) v in
if nat_gtb (List.length (g_stack global1)) ( 1023%nat) then
let nv := {[ {[ v with vctx_gas := Coq.ZArith.BinInt.Z.add
(vctx_gas v)
(uint (callarg_gas args)) ]} with vctx_stack :=
(word256FromNumeral 0%nat) :: (vctx_stack v) ]} in
Continue
( {[{[ global1 with g_vmstate := InstructionContinue nv ]} with g_current := n_state ]})
else
let acc := n_state (cctx_this c) in
let cctx := {|cctx_this :=(cctx_this c);cctx_program :=(block_account_code (
n_state (callarg_code args)));cctx_hash_filter :=(cctx_hash_filter c) |} in
let nv := start_env acc n_state args (vctx_caller v)
(vctx_origin v) (vctx_gasprice v) (vctx_block v) in
Continue
( {[ {[ {[{[ global1 with g_vmstate:=InstructionContinue nv ]} with g_cctx:=cctx ]} with g_current:=n_state ]} with g_stack:=(
(state,v,c,get_hint stuff) :: (g_stack global1)) ]})
| ContractCreate args =>
let addr := calc_address (cctx_this c)
(block_account_nonce (state (cctx_this c))) in
if word256ULT (block_account_balance (state (cctx_this c)))
(createarg_value args) ||
(nat_gtb (List.length (g_stack global1)) ( 1023%nat) ||
(block_account_exists (state addr))) then
let nv := {[ v with vctx_stack :=(word256FromNumeral 0%nat) ::
(vctx_stack v) ]} in
Continue
( {[{[ global1 with g_vmstate := InstructionContinue nv ]} with g_current := state ]})
else
let state := update_nonce state (cctx_this c) in
let n_state := update_return state (cctx_this c) v in
let old_acc := n_state addr in
let old_balance :=(block_account_balance old_acc) in
let acc := empty_account0 addr in
let acc := {[ {[ acc with block_account_exists := true ]} with block_account_balance := old_balance ]} in
let cctx := {|cctx_this := addr;cctx_program := (make_program
(createarg_code args));cctx_hash_filter :=(cctx_hash_filter c) |} in
let n_state := update_world n_state addr acc in
let n_state := transfer_balance n_state (cctx_this c) addr
(createarg_value args) in let passed_gas : Z :=
if int_gteb ((two_compl_value 255 (block_number (vctx_block v))))
(Coq.ZArith.BinInt.Z.mul
((Z.pred (Z.pos (P_of_succ_nat 2463%nat))))
((Z.pred (Z.pos (P_of_succ_nat 1000%nat))))) then
L (vctx_gas v) else (vctx_gas v) in
let remaining_gas := Coq.ZArith.BinInt.Z.sub (vctx_gas v) passed_gas in
let nv := create_env acc n_state (createarg_value args) []
passed_gas (cctx_this c) (vctx_origin v)
(vctx_gasprice v) (vctx_block v) in
let v := {[ v with vctx_gas := remaining_gas ]} in
Continue
( {[ {[ {[{[ global1 with g_vmstate:=InstructionContinue nv ]} with g_cctx:=cctx ]} with g_current:=n_state ]} with g_stack:=(
(state,v,c,CreateAddress addr) :: (g_stack global1)) ]})
| ContractFail _ =>
match ((g_stack global1)) with | [] =>
Finished
{|f_state:=orig;f_killed:=[];f_gas:=((Z.pred
(Z.pos
(P_of_succ_nat 0%nat))));f_refund:=(
(Z.pred (Z.pos (P_of_succ_nat 0%nat))));f_logs := [] |}
| (oldstate, v, c, _) :: rest =>
let v := {[ v with vctx_stack :=(word256FromNumeral 0%nat) ::
(vctx_stack v) ]} in
Continue
( {[ {[ {[{[ global1 with g_vmstate:=InstructionContinue v ]} with g_cctx:=c ]} with g_current:=oldstate ]} with g_stack:=rest ]})
end | ContractSuicide dst =>
let n_dst := {[ (state dst) with block_account_balance := word256Add
(block_account_balance (
state
dst))
(block_account_balance (
state
(cctx_this c))) ]} in
let acc := {[ (state (cctx_this c)) with block_account_balance :=(
word256FromNumeral 0%nat) ]} in
let state := update_world (update_world state dst n_dst) (cctx_this c)
acc in
let killed :=(cctx_this c) :: (g_killed global1) in
match ((g_stack global1)) with | [] =>
Finished
({|f_state := state;f_killed := killed;f_refund :=(vctx_refund v);f_gas :=(vctx_gas v);f_logs :=(vctx_logs v) |})
| (_, nv, nc, is_new) :: rest =>
let n_state := match ( is_new) with | CreateAddress new_addr =>
create_account state new_addr [] | _ => state end in
if beq_nat (List.length rest) ( 0%nat) && (g_create global1) then
Finished
{|f_state:=n_state;f_killed:=killed;f_gas:=(vctx_gas v);f_refund:=(vctx_refund v);f_logs :=(vctx_logs v) |}
else
let acc := n_state (cctx_this nc) in
let nv := {[ nv with vctx_stack :=(word256FromNumeral 1%nat) ::
(vctx_stack nv) ]} in
let nv := vctx_update_from_world nv acc n_state v in
Continue
( {[ {[ {[ {[{[ global1 with g_killed := killed ]} with g_vmstate:=
InstructionContinue nv ]} with g_cctx:=nc ]} with g_current:=n_state ]} with g_stack:=rest ]})
end | ContractReturn bytes =>
let n_state := update_return state (cctx_this c) v in
match ((g_stack global1)) with | [] =>
Finished
{|f_state := n_state;f_killed :=(g_killed global1);f_refund :=(vctx_refund v);f_gas :=(vctx_gas v);f_logs :=(vctx_logs v) |}
| (_, nv, c, ReturnTo mem_start mem_size) :: rest =>
let acc := n_state (cctx_this c) in
let nv := {[ {[ nv with vctx_memory := put_return_values
(vctx_memory nv) bytes
mem_start mem_size ]} with vctx_stack :=
(word256FromNumeral 1%nat) :: (vctx_stack nv) ]} in
let nv := vctx_update_from_world nv (acc : block_account ) n_state v in
Continue
( {[ {[ {[{[ global1 with g_vmstate:=InstructionContinue nv ]} with g_cctx:=c ]} with g_current:=n_state ]} with g_stack:=rest ]})
| (old_state, nv, c, CreateAddress new_addr) :: rest =>
if (list_equal_by classical_boolean_equivalence bytes []) &&
(beq_nat (List.length rest) ( 0%nat) && (g_create global1)) then
Finished
{|f_state:=n_state;f_killed:=(g_killed global1);f_gas:=(vctx_gas v);f_refund:=(vctx_refund v);f_logs :=(vctx_logs v) |}
else
match (
if int_ltb (vctx_gas v)
((Z.pred
(Z.pos
(P_of_succ_nat
(Coq.Init.Peano.mult ( 200%nat) (List.length bytes))))))
&&
int_lteb homestead_block
((two_compl_value 255 (block_number (vctx_block v)))) then
(old_state, {[ v with vctx_gas :=(Z.pred
(Z.pos (P_of_succ_nat 0%nat))) ]},(
word256FromNumeral 0%nat)) else
if int_ltb (vctx_gas v)
((Z.pred
(Z.pos
(P_of_succ_nat
(Coq.Init.Peano.mult ( 200%nat)
(List.length bytes)))))) then
(n_state, v,(word256FromNumeral 0%nat)) else
(create_account n_state new_addr bytes, {[ v with vctx_gas :=
Coq.ZArith.BinInt.Z.sub (vctx_gas v)
((Z.pred
(Z.pos
(P_of_succ_nat
(Coq.Init.Peano.mult ( 200%nat) (List.length bytes)))))) ]},
address_to_w256 new_addr)) with (n_state, v, ret1) =>
let acc := n_state (cctx_this c) in
let nv := {[ nv with vctx_stack := ret1 :: (vctx_stack nv) ]} in
let nv := vctx_update_from_world nv acc n_state v in
Continue
( {[ {[ {[{[ global1 with g_vmstate:=InstructionContinue nv ]} with g_cctx:=c ]} with g_current:=n_state ]} with g_stack:=rest ]})
end | _ => Unimplemented end end | a =>
Continue
({[ global1 with g_vmstate := next_state
(fun ( _ : instruction_result ) => tt)
c net a ]}) end end.
Program Fixpoint txdatacost (lst : list (word8 )) : Z := match ( lst) with
| [] =>(Z.pred (Z.pos (P_of_succ_nat 0%nat)))
| b::lst => Coq.ZArith.BinInt.Z.add (if classical_boolean_equivalence b(word8FromNumeral 0%nat) then(Z.pred (Z.pos (P_of_succ_nat 4%nat))) else(Z.pred (Z.pos (P_of_succ_nat 68%nat)))) (txdatacost lst)
end.
Definition calc_igas (tr : transaction ) (block : block_info ) : Z :=
let igas := Coq.ZArith.BinInt.Z.add((Z.pred (Z.pos (P_of_succ_nat 21000%nat)))) (txdatacost(tr_data tr)) in
if int_ltb ((two_compl_value 255(block_number block))) homestead_block then igas else
match ((tr_to tr)) with
| None => Coq.ZArith.BinInt.Z.add igas((Z.pred (Z.pos (P_of_succ_nat 32000%nat))))
| Some _ => igas
end.
Definition nothing_happens (state : word160 -> block_account ) (tr : transaction ) : tr_result := {|f_state:=(sub_balance state(tr_from tr) ( word256Mult(tr_gas_price tr)(tr_gas_limit tr)));f_killed:=[];f_logs := [];f_gas:=(uint(tr_gas_limit tr));f_refund:=((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) |}.
Definition start_transaction (tr : transaction ) (state : word160 -> block_account ) (block : block_info ) : global_state :=
let s_acc := state(tr_from tr) in
let gas_value := Coq.Init.Peano.mult (word256ToNatural(tr_gas_price tr)) (word256ToNatural(tr_gas_limit tr)) in
let igas := calc_igas tr block in
let nothing := Finished (nothing_happens state tr) in
if unsafe_structural_inequality(tr_nonce tr)(block_account_nonce s_acc) then nothing else
if nat_ltb (word256ToNatural(block_account_balance s_acc)) (Coq.Init.Peano.plus (word256ToNatural(tr_value tr)) gas_value) then nothing else
let gas_value := word256Mult(tr_gas_price tr)(tr_gas_limit tr) in
if nat_ltb (word256ToNatural(block_gaslimit block)) (word256ToNatural(tr_gas_limit tr)) then nothing else
if nat_ltb (word256ToNatural(tr_gas_limit tr)) (Z.abs_nat igas) then nothing else
match ((tr_to tr)) with
| None =>
if (list_equal_by classical_boolean_equivalence(tr_data tr) []) && (classical_boolean_equivalence(tr_gas_limit tr)(word256FromNumeral 0%nat) && classical_boolean_equivalence(tr_gas_price tr)(word256FromNumeral 0%nat)) then nothing else
if (list_equal_by classical_boolean_equivalence(tr_data tr) []) && classical_boolean_equivalence(tr_gas_price tr)(word256FromNumeral 0%nat) then Finished {|f_state:=(update_nonce state(tr_from tr));f_killed:=[];f_gas:=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));f_refund:=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));f_logs := [] |} else
let s_acc := {[ s_acc with block_account_balance := word256Minus(block_account_balance s_acc) gas_value ]} in
let n_state := update_world state(tr_from tr) s_acc in
if (list_equal_by classical_boolean_equivalence(tr_data tr) []) then
Finished {|f_state:=(update_nonce n_state(tr_from tr));f_killed:=[];f_gas:= (Coq.ZArith.BinInt.Z.sub ((two_compl_value 255(tr_gas_limit tr))) igas);f_refund:=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));f_logs:=[] |} else
let v := create_env s_acc n_state(word256FromNumeral 0%nat) []
((two_compl_value 255 ( word256Minus(tr_gas_limit tr) (word256FromInteger igas))))(tr_from tr)(tr_from tr)(tr_gas_price tr) block in
let c := build_cctx0 s_acc in
let args := {|createarg_value :=(tr_value tr);createarg_code :=(tr_data tr) |} in
let act := ContractCreate args in
Continue ({|g_create := true;g_orig := n_state;g_stack := [];g_current := n_state;g_cctx := c;g_vmstate := (InstructionToEnvironment act v None);g_killed := [] |})
| Some addr =>
let s_acc := {[ {[ s_acc with block_account_balance := word256Minus(block_account_balance s_acc) gas_value ]} with block_account_nonce := word256Add(block_account_nonce s_acc)(word256FromNumeral 1%nat) ]} in
let state2 := update_world state(tr_from tr) s_acc in
if nat_ltb (word256ToNatural(block_account_balance s_acc)) (word256ToNatural(tr_value tr)) then nothing else
let s_acc := {[ s_acc with block_account_balance := word256Minus(block_account_balance s_acc)(tr_value tr) ]} in
let n_state := update_world state(tr_from tr) s_acc in
let acc := n_state addr in
let acc := {[ acc with block_account_balance := word256Add(block_account_balance acc)(tr_value tr) ]} in
let n_state := update_world n_state addr acc in
let v := create_env acc n_state(tr_value tr)(tr_data tr) ( Coq.ZArith.BinInt.Z.sub(uint(tr_gas_limit tr)) igas)(tr_from tr)(tr_from tr)(tr_gas_price tr) block in
let c := build_cctx0 acc in
Continue ({|g_create := false;g_orig := state2;g_stack := [];g_current := n_state;g_cctx := c;g_vmstate := (InstructionContinue v);g_killed := [] |})
end.
Program Fixpoint kill_accounts (state : address -> block_account ) (killed : list (word160 )) : address -> block_account := match ( killed) with
| [] => state
| a::rest => kill_accounts (update_world state a (empty_account0 a)) rest
end.
Definition refund_selfdestruct : nat := 24000%nat.
Definition end_transaction (f : tr_result ) (tr : transaction ) (block : block_info ) : address -> block_account :=
let state := kill_accounts(f_state f)(f_killed f) in
let refund := Coq.Init.Peano.plus (Coq.Init.Peano.mult ( (List.length(f_killed f))) refund_selfdestruct) (Z.abs_nat(f_refund f)) in
let r := Coq.Init.Peano.plus (Z.abs_nat(f_gas f)) (nat_min refund ( Nat.div( Coq.Init.Peano.minus(word256ToNatural(tr_gas_limit tr)) (Z.abs_nat(f_gas f)))( 2%nat))) in
let refund_sum := word256FromNatural ( Coq.Init.Peano.mult r (word256ToNatural(tr_gas_price tr))) in
let state := add_balance state(tr_from tr) refund_sum in
add_balance state(block_coinbase block) ( word256Minus (word256Mult(tr_gas_limit tr)(tr_gas_price tr)) refund_sum).