Library EVMOpSem.evm
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 Lem.lem_list.
Require Export Lem.lem_list.
Require Import Lem.lem_word.
Require Export Lem.lem_word.
Require Import word256.
Require Export word256.
Require Import word160.
Require Export word160.
Require Import word8.
Require Export word8.
Require Import word4.
Require Export word4.
Require Import keccak.
Require Export keccak.
Definition address : Type := word160 .
Definition address_default: address := word160_default.
Definition sintFromW256 : (Bvector 256) -> Z := (two_compl_value 255).
Definition uint (w : (Bvector 256) ) : Z := (Z.pred (Z.pos (P_of_succ_nat (word256ToNatural w)))).
Definition absnat (w : (Bvector 256) ) : nat := Z.abs_nat ( ((two_compl_value 255 w))).
Definition byteFromNat : nat -> word8 := word8FromNat.
Definition w256_of_bl : list (bool ) -> (Bvector 256) := word256FromBoollist.
Definition w256_to_address (w : (Bvector 256) ) : word160 := word160FromNatural (word256ToNatural w).
Definition address_to_w256 (w : word160 ) : (Bvector 256) := word256FromNatural (word160ToNatural w).
Definition w256_to_byte (w : (Bvector 256) ) : word8 := word8FromNatural (word256ToNatural w).
Definition byte_to_w256 (w : word8 ) : (Bvector 256) := word256FromNat (word8ToNat w).
Definition word_rsplit256 (w : (Bvector 256) ) : list (byte ):= (word_rsplit_aux (boolListFromWord256 w)( 32%nat)).
Definition get_byte (position : (Bvector 256) ) (w : (Bvector 256) ) : (Bvector 256) :=
if int_gteb (uint position)((Z.pred (Z.pos (P_of_succ_nat 32%nat)))) then(word256FromNumeral 0%nat) else
match ( lem_list.index (word_rsplit256 w) (Z.abs_nat ( (uint position)))) with
| None =>(word256FromNumeral 0%nat)
| Some a => byte_to_w256 a
end.
Definition log256floor (x : Z ) : Z := Z.div (Z.log2 (x : Z ) : Z ) ((Z.pred (Z.pos (P_of_succ_nat 8%nat))) : Z ).
Program Fixpoint word_exp (i : Z ) (n : nat ) : Z :=
match ( n) with
| 0%nat =>(Z.pred (Z.pos (P_of_succ_nat 1%nat)))
|S (n) => Coq.ZArith.Zdiv.Zmod ( Coq.ZArith.BinInt.Z.mul(word_exp i n) i) ( Coq.ZArith.Zpower.Zpower_nat((Z.pred (Z.pos (P_of_succ_nat 2%nat))))( 256%nat))
end.
Definition memory : Type := w256 -> byte .
Definition memory_default: memory := (fun (x118 : w256 ) => byte_default).
Definition storage : Type := w256 -> w256 .
Definition storage_default: storage := (fun (x117 : w256 ) => w256_default).
Program Fixpoint cut_memory_aux (idx : (Bvector 256) ) (n : nat ) (memory1 : (Bvector 256) -> word8 ) : list (word8 ):= match ( n) with
| 0%nat => []
| S (n) => memory1 idx :: cut_memory_aux ( word256Add idx(word256FromNumeral 1%nat)) n memory1
end.
Program Fixpoint iota0 (start : (Bvector 256) ) (n : nat ) (rev_acc : list ((Bvector 256) )) : list ((Bvector 256) ):=
match ( n) with
| 0%nat => List.rev rev_acc
| S (x) => iota0 ( word256Add start(word256FromNumeral 1%nat)) x (start :: rev_acc)
end.
Definition cut_memory_aux_alt (idx : (Bvector 256) ) (n : nat ) (memory1 : (Bvector 256) -> word8 ) : list (word8 ):= List.map memory1 (iota0 idx n []).
Definition cut_memory (idx : (Bvector 256) ) (n : (Bvector 256) ) (memory1 : w256 -> byte ) : list (byte ):= cut_memory_aux_alt idx (word256ToNatural n) memory1.
Program Fixpoint put_return_values_aux (orig : (Bvector 256) -> word8 ) (lst : list (word8 )) (b : Z ) (s : nat ) : (Bvector 256) -> word8 := match ( s) with
| 0%nat => orig
| S (s) =>
match ( lst) with
| [] => orig
| h :: t => put_return_values_aux (fun (addr : (Bvector 256) ) => if classical_boolean_equivalence addr (word256FromInteger b) then h else orig addr) t ( Coq.ZArith.BinInt.Z.add b((Z.pred (Z.pos (P_of_succ_nat 1%nat))))) s
end
end.
Definition put_return_values (orig : w256 -> byte ) (lst : list (byte )) (b : Z ) (s : Z ) : w256 -> byte :=
if int_lteb s((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then orig else put_return_values_aux orig lst b (Z.abs_nat s).
Definition empty_storage ( _ : (Bvector 256) ) : (Bvector 256) := (word256FromNumeral 0%nat).
Inductive network : Type :=
Frontier: network
| Homestead: network
| EIP150: network
| EIP158: network
| Metropolis: network .
Definition network_default: network := Frontier.
Definition network_of_block_number (bn : Z ) : network :=
if int_ltb bn (Coq.ZArith.BinInt.Z.mul (Coq.ZArith.BinInt.Z.mul((Z.pred (Z.pos (P_of_succ_nat 115%nat))))((Z.pred (Z.pos (P_of_succ_nat 100%nat)))))((Z.pred (Z.pos (P_of_succ_nat 100%nat))))) then Frontier
else if int_ltb bn (Coq.ZArith.BinInt.Z.mul (Coq.ZArith.BinInt.Z.mul (Coq.ZArith.BinInt.Z.mul((Z.pred (Z.pos (P_of_succ_nat 3%nat))))((Z.pred (Z.pos (P_of_succ_nat 821%nat)))))((Z.pred (Z.pos (P_of_succ_nat 10%nat)))))((Z.pred (Z.pos (P_of_succ_nat 100%nat))))) then Homestead
else if int_ltb bn (Coq.ZArith.BinInt.Z.mul (Coq.ZArith.BinInt.Z.mul (Coq.ZArith.BinInt.Z.mul (Coq.ZArith.BinInt.Z.mul((Z.pred (Z.pos (P_of_succ_nat 5%nat))))((Z.pred (Z.pos (P_of_succ_nat 5%nat)))))((Z.pred (Z.pos (P_of_succ_nat 107%nat)))))((Z.pred (Z.pos (P_of_succ_nat 10%nat)))))((Z.pred (Z.pos (P_of_succ_nat 100%nat))))) then EIP150
else EIP158.
Definition at_least_eip150 (n : network ) : bool :=
match ( n) with
Frontier => false
| Homestead => false
| EIP150 => true
| EIP158 => true
| Metropolis => true
end.
Definition before_homestead (n : network ) : bool :=
match ( n) with
Frontier => true
| Homestead => false
| EIP150 => false
| EIP158 => false
| Metropolis => false
end.
Definition stack_numbers : Type := ((Z * Z ) % type).
Definition stack_numbers_default: stack_numbers := (Z_default, Z_default).
Inductive bits_inst : Type :=
| inst_AND: bits_inst
| inst_OR: bits_inst
| inst_XOR: bits_inst
| inst_NOT: bits_inst
| BYTE: bits_inst .
Definition bits_inst_default: bits_inst := inst_AND.
Definition bits_inst_code (inst1 : bits_inst ) : word8 := match ( inst1) with
| inst_AND =>(word8FromNumeral 22%nat)
| inst_OR =>(word8FromNumeral 23%nat)
| inst_XOR =>(word8FromNumeral 24%nat)
| inst_NOT =>(word8FromNumeral 25%nat)
| BYTE =>(word8FromNumeral 26%nat)
end.
Definition bits_stack_nums (inst1 : bits_inst ) : (Z *Z ) % type:= match ( inst1) with
| inst_AND => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| inst_OR => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| inst_XOR => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| inst_NOT => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| BYTE => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
end.
Inductive sarith_inst : Type :=
| SDIV: sarith_inst
| SMOD: sarith_inst
| SGT: sarith_inst
| SLT: sarith_inst
| SIGNEXTEND: sarith_inst .
Definition sarith_inst_default: sarith_inst := SDIV.
Definition sarith_inst_code (inst1 : sarith_inst ) : word8 := match ( inst1) with
| SDIV =>(word8FromNumeral 5%nat)
| SMOD =>(word8FromNumeral 7%nat)
| SGT =>(word8FromNumeral 19%nat)
| SLT =>(word8FromNumeral 18%nat)
| SIGNEXTEND =>(word8FromNumeral 11%nat)
end.
Definition sarith_inst_nums (inst1 : sarith_inst ) : (Z *Z ) % type:= match ( inst1) with
| SDIV => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SMOD => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SGT => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SLT => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SIGNEXTEND => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
end.
Inductive arith_inst : Type :=
| ADD: arith_inst
| MUL: arith_inst
| SUB: arith_inst
| DIV: arith_inst
| MOD: arith_inst
| ADDMOD: arith_inst
| MULMOD: arith_inst
| EXP: arith_inst
| inst_GT: arith_inst
| inst_EQ: arith_inst
| inst_LT: arith_inst
| ISZERO: arith_inst
| SHA3: arith_inst .
Definition arith_inst_default: arith_inst := ADD.
Definition arith_inst_code (inst1 : arith_inst ) : word8 := match ( inst1) with
| ADD =>(word8FromNumeral 1%nat)
| MUL =>(word8FromNumeral 2%nat)
| SUB =>(word8FromNumeral 3%nat)
| DIV =>(word8FromNumeral 4%nat)
| MOD =>(word8FromNumeral 6%nat)
| ADDMOD =>(word8FromNumeral 8%nat)
| MULMOD =>(word8FromNumeral 9%nat)
| EXP =>(word8FromNumeral 10%nat)
| inst_GT =>(word8FromNumeral 17%nat)
| inst_LT =>(word8FromNumeral 16%nat)
| inst_EQ =>(word8FromNumeral 20%nat)
| ISZERO =>(word8FromNumeral 21%nat)
| SHA3 =>(word8FromNumeral 32%nat)
end.
Definition arith_inst_numbers (inst1 : arith_inst ) : (Z *Z ) % type:= match ( inst1) with
| ADD => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| MUL => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SUB => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| DIV => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| MOD => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| ADDMOD => ((Z.pred (Z.pos (P_of_succ_nat 3%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| MULMOD => ((Z.pred (Z.pos (P_of_succ_nat 3%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| EXP => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| inst_GT => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| inst_LT => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| inst_EQ => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| ISZERO => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SHA3 => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
end.
Inductive info_inst : Type :=
ADDRESS: info_inst
| BALANCE: info_inst
| ORIGIN: info_inst
| CALLER: info_inst
| CALLVALUE: info_inst
| CALLDATASIZE: info_inst
| CODESIZE: info_inst
| GASPRICE: info_inst
| EXTCODESIZE: info_inst
| BLOCKHASH: info_inst
| COINBASE: info_inst
| TIMESTAMP: info_inst
| NUMBER: info_inst
| DIFFICULTY: info_inst
| GASLIMIT: info_inst
| GAS: info_inst .
Definition info_inst_default: info_inst := ADDRESS.
Definition info_inst_code (inst1 : info_inst ) : word8 := match ( inst1) with
| ADDRESS =>(word8FromNumeral 48%nat)
| BALANCE =>(word8FromNumeral 49%nat)
| ORIGIN =>(word8FromNumeral 50%nat)
| CALLVALUE =>(word8FromNumeral 52%nat)
| CALLDATASIZE =>(word8FromNumeral 54%nat)
| CALLER =>(word8FromNumeral 51%nat)
| CODESIZE =>(word8FromNumeral 56%nat)
| GASPRICE =>(word8FromNumeral 58%nat)
| EXTCODESIZE =>(word8FromNumeral 59%nat)
| BLOCKHASH =>(word8FromNumeral 64%nat)
| COINBASE =>(word8FromNumeral 65%nat)
| TIMESTAMP =>(word8FromNumeral 66%nat)
| NUMBER =>(word8FromNumeral 67%nat)
| DIFFICULTY =>(word8FromNumeral 68%nat)
| GASLIMIT =>(word8FromNumeral 69%nat)
| GAS =>(word8FromNumeral 90%nat)
end.
Definition info_inst_numbers (inst1 : info_inst ) : (Z *Z ) % type:= match ( inst1) with
| ADDRESS => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| BALANCE => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| ORIGIN => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| CALLER => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| CALLVALUE => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| CALLDATASIZE => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| CODESIZE => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| GASPRICE => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| EXTCODESIZE => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| BLOCKHASH => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| COINBASE => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| TIMESTAMP => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| NUMBER => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| DIFFICULTY => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| GASLIMIT => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| GAS => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
end.
Definition nibble : Type := word4 .
Definition nibble_default: nibble := word4_default.
Definition dup_inst : Type := nibble .
Definition dup_inst_default: dup_inst := nibble_default.
Definition dup_inst_code (m : word4 ) : word8 :=
( word8Add(word8FromInt (word4ToUInt m))(word8FromNumeral 128%nat)).
Definition dup_inst_numbers (m : word4 ) : (Z *Z ) % type:= (word4ToUInt m, Coq.ZArith.BinInt.Z.add (word4ToUInt m)((Z.pred (Z.pos (P_of_succ_nat 1%nat))))).
Inductive memory_inst : Type :=
| MLOAD: memory_inst
| MSTORE: memory_inst
| MSTORE8: memory_inst
| CALLDATACOPY: memory_inst
| CODECOPY: memory_inst
| EXTCODECOPY: memory_inst
| MSIZE: memory_inst .
Definition memory_inst_default: memory_inst := MLOAD.
Definition memory_inst_code (inst1 : memory_inst ) : word8 := match ( inst1) with
| MLOAD =>(word8FromNumeral 81%nat)
| MSTORE =>(word8FromNumeral 82%nat)
| MSTORE8 =>(word8FromNumeral 83%nat)
| CALLDATACOPY =>(word8FromNumeral 55%nat)
| CODECOPY =>(word8FromNumeral 57%nat)
| EXTCODECOPY =>(word8FromNumeral 60%nat)
| MSIZE =>(word8FromNumeral 89%nat)
end.
Definition memory_inst_numbers (inst1 : memory_inst ) : (Z *Z ) % type:= match ( inst1) with
| MLOAD => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| MSTORE => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| MSTORE8 => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| CALLDATACOPY => ((Z.pred (Z.pos (P_of_succ_nat 3%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| CODECOPY => ((Z.pred (Z.pos (P_of_succ_nat 3%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| EXTCODECOPY => ((Z.pred (Z.pos (P_of_succ_nat 4%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| MSIZE => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
end.
Inductive storage_inst : Type :=
| SLOAD: storage_inst
| SSTORE: storage_inst .
Definition storage_inst_default: storage_inst := SLOAD.
Definition storage_inst_code (inst1 : storage_inst ) : word8 := match ( inst1) with
| SLOAD =>(word8FromNumeral 84%nat)
| SSTORE =>(word8FromNumeral 85%nat)
end.
Definition storage_inst_numbers (inst1 : storage_inst ) : (Z *Z ) % type:= match ( inst1) with
| SLOAD => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SSTORE => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
end.
Inductive pc_inst : Type :=
| JUMP: pc_inst
| JUMPI: pc_inst
| PC: pc_inst
| JUMPDEST: pc_inst .
Definition pc_inst_default: pc_inst := JUMP.
Definition pc_inst_code (inst1 : pc_inst ) : word8 := match ( inst1) with
| JUMP =>(word8FromNumeral 86%nat)
| JUMPI =>(word8FromNumeral 87%nat)
| PC =>(word8FromNumeral 88%nat)
| JUMPDEST =>(word8FromNumeral 91%nat)
end.
Definition pc_inst_numbers (inst1 : pc_inst ) : (Z *Z ) % type:= match ( inst1) with
| JUMP => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| JUMPI => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| PC => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| JUMPDEST => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
end.
Inductive stack_inst : Type :=
| POP: stack_inst
| PUSH_N: list byte -> stack_inst
| CALLDATALOAD: stack_inst .
Definition stack_inst_default: stack_inst := POP.
Definition stack_inst_code (inst1 : stack_inst ) : list (word8 ):= match ( inst1) with
| POP => [(word8FromNumeral 80%nat)]
| PUSH_N lst =>
if nat_ltb (List.length lst)( 1%nat) then [(word8FromNumeral 96%nat);(word8FromNumeral 0%nat)]
else if nat_gtb (List.length lst)( 32%nat) then [(word8FromNumeral 96%nat);(word8FromNumeral 0%nat)]
else (@ List.app _)[ word8Add(byteFromNat (List.length lst))(word8FromNumeral 95%nat)] lst
| CALLDATALOAD => [(word8FromNumeral 53%nat)]
end.
Definition stack_inst_numbers (inst1 : stack_inst ) : (Z *Z ) % type:= match ( inst1) with
| POP => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| PUSH_N _ => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| CALLDATALOAD => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
end.
Definition swap_inst : Type := nibble .
Definition swap_inst_default: swap_inst := nibble_default.
Definition swap_inst_code (m : word4 ) : word8 :=
( word8Add(word8FromInt (word4ToUInt m))(word8FromNumeral 144%nat)).
Definition swap_inst_numbers (m : word4 ) : (Z *Z ) % type:=
( Coq.ZArith.BinInt.Z.add(word4ToUInt m)((Z.pred (Z.pos (P_of_succ_nat 1%nat)))), Coq.ZArith.BinInt.Z.add (word4ToUInt m)((Z.pred (Z.pos (P_of_succ_nat 1%nat))))).
Inductive log_inst : Type :=
| LOG0: log_inst
| LOG1: log_inst
| LOG2: log_inst
| LOG3: log_inst
| LOG4: log_inst .
Definition log_inst_default: log_inst := LOG0.
Definition log_inst_code (inst1 : log_inst ) : word8 := match ( inst1) with
| LOG0 =>(word8FromNumeral 160%nat)
| LOG1 =>(word8FromNumeral 161%nat)
| LOG2 =>(word8FromNumeral 162%nat)
| LOG3 =>(word8FromNumeral 163%nat)
| LOG4 =>(word8FromNumeral 164%nat)
end.
Definition log_inst_numbers (inst1 : log_inst ) : (Z *Z ) % type:= match ( inst1) with
| LOG0 => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| LOG1 => ((Z.pred (Z.pos (P_of_succ_nat 3%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| LOG2 => ((Z.pred (Z.pos (P_of_succ_nat 4%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| LOG3 => ((Z.pred (Z.pos (P_of_succ_nat 5%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| LOG4 => ((Z.pred (Z.pos (P_of_succ_nat 6%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
end.
Inductive misc_inst : Type :=
| STOP: misc_inst
| CREATE: misc_inst
| CALL: misc_inst
| CALLCODE: misc_inst
| DELEGATECALL: misc_inst
| RETURN: misc_inst
| SUICIDE: misc_inst .
Definition misc_inst_default: misc_inst := STOP.
Definition misc_inst_code (inst1 : misc_inst ) : word8 := match ( inst1) with
| STOP =>(word8FromNumeral 0%nat)
| CREATE =>(word8FromNumeral 240%nat)
| CALL =>(word8FromNumeral 241%nat)
| CALLCODE =>(word8FromNumeral 242%nat)
| RETURN =>(word8FromNumeral 243%nat)
| DELEGATECALL =>(word8FromNumeral 244%nat)
| SUICIDE =>(word8FromNumeral 255%nat)
end.
Definition misc_inst_numbers (inst1 : misc_inst ) : (Z *Z ) % type:= match ( inst1) with
| STOP => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| CREATE => ((Z.pred (Z.pos (P_of_succ_nat 3%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| CALL => ((Z.pred (Z.pos (P_of_succ_nat 7%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| CALLCODE => ((Z.pred (Z.pos (P_of_succ_nat 7%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| RETURN => ((Z.pred (Z.pos (P_of_succ_nat 2%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| DELEGATECALL => ((Z.pred (Z.pos (P_of_succ_nat 6%nat))),(Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| SUICIDE => ((Z.pred (Z.pos (P_of_succ_nat 1%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
end.
Inductive inst : Type :=
| Unknown: byte -> inst
| Bits: bits_inst -> inst
| Sarith: sarith_inst -> inst
| Arith: arith_inst -> inst
| Info: info_inst -> inst
| Dup: dup_inst -> inst
| Memory: memory_inst -> inst
| Storage: storage_inst -> inst
| Pc: pc_inst -> inst
| Stack: stack_inst -> inst
| Swap: swap_inst -> inst
| Log: log_inst -> inst
| Misc: misc_inst -> inst .
Definition inst_default: inst := Unknown byte_default.
Definition maybe_to_list {a : Type} (m : option a ) : list a:= match ( m) with
| None => []
| Some s => [s]
end.
Definition inst_code (inst1 : inst ) : list (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 => stack_inst_code s
| Swap s => [swap_inst_code s]
| Log l => [log_inst_code l]
| Misc m => [misc_inst_code m]
end.
Definition inst_stack_numbers (i : inst ) : (Z *Z ) % type:= match ( i) with
| Unknown _ => ((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat))))
| 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
end.
Definition inst_size (i : inst ) : Z := (Z.pred (Z.pos (P_of_succ_nat (List.length (inst_code i))))).
Definition Gzero : Z := (Z.pred (Z.pos (P_of_succ_nat 0%nat))).
Definition Gbase : Z := (Z.pred (Z.pos (P_of_succ_nat 2%nat))).
Definition Gverylow : Z := (Z.pred (Z.pos (P_of_succ_nat 3%nat))).
Definition Glow : Z := (Z.pred (Z.pos (P_of_succ_nat 5%nat))).
Definition Gmid : Z := (Z.pred (Z.pos (P_of_succ_nat 8%nat))).
Definition Ghigh : Z := (Z.pred (Z.pos (P_of_succ_nat 10%nat))).
Definition homestead_block : Z := Coq.ZArith.BinInt.Z.mul((Z.pred (Z.pos (P_of_succ_nat 1150%nat))))((Z.pred (Z.pos (P_of_succ_nat 1000%nat)))).
Definition Gextcode (net : network ) : Z :=
if at_least_eip150 net then(Z.pred (Z.pos (P_of_succ_nat 700%nat))) else(Z.pred (Z.pos (P_of_succ_nat 20%nat))).
Definition Gbalance (n : network ) : Z :=
if at_least_eip150 n then(Z.pred (Z.pos (P_of_succ_nat 400%nat))) else(Z.pred (Z.pos (P_of_succ_nat 20%nat))).
Definition Gsload (n : network ) : Z :=
if at_least_eip150 n then(Z.pred (Z.pos (P_of_succ_nat 200%nat))) else(Z.pred (Z.pos (P_of_succ_nat 50%nat))).
Definition Gjumpdest : Z := (Z.pred (Z.pos (P_of_succ_nat 1%nat))).
Definition Gsset : Z := (Z.pred (Z.pos (P_of_succ_nat 20000%nat))).
Definition Gsreset : Z := (Z.pred (Z.pos (P_of_succ_nat 5000%nat))).
Definition Rsclear : Z := (Z.pred (Z.pos (P_of_succ_nat 15000%nat))).
Definition Rsuicide : Z := (Z.pred (Z.pos (P_of_succ_nat 24000%nat))).
Definition Gsuicide (n : network ) : Z :=
if at_least_eip150 n then(Z.pred (Z.pos (P_of_succ_nat 5000%nat))) else(Z.pred (Z.pos (P_of_succ_nat 0%nat))).
Definition Gcreate : Z := (Z.pred (Z.pos (P_of_succ_nat 32000%nat))).
Definition Gcodedeposit : Z := (Z.pred (Z.pos (P_of_succ_nat 200%nat))).
Definition Gcall (net : network ) : Z :=
if at_least_eip150 net then(Z.pred (Z.pos (P_of_succ_nat 700%nat))) else(Z.pred (Z.pos (P_of_succ_nat 40%nat))).
Definition Gcallvalue : Z := (Z.pred (Z.pos (P_of_succ_nat 9000%nat))).
Definition Gcallstipend : Z := (Z.pred (Z.pos (P_of_succ_nat 2300%nat))).
Definition Gnewaccount : Z := (Z.pred (Z.pos (P_of_succ_nat 25000%nat))).
Definition Gexp : Z := (Z.pred (Z.pos (P_of_succ_nat 10%nat))).
Definition Gexpbyte (net : network ) : Z :=
if at_least_eip150 net then(Z.pred (Z.pos (P_of_succ_nat 50%nat))) else(Z.pred (Z.pos (P_of_succ_nat 10%nat))).
Definition Gmemory : Z := (Z.pred (Z.pos (P_of_succ_nat 3%nat))).
Definition Gtxcreate : Z := (Z.pred (Z.pos (P_of_succ_nat 32000%nat))).
Definition Gtxdatazero : Z := (Z.pred (Z.pos (P_of_succ_nat 4%nat))).
Definition Gtxdatanonzero : Z := (Z.pred (Z.pos (P_of_succ_nat 68%nat))).
Definition Gtransaction : Z := (Z.pred (Z.pos (P_of_succ_nat 21000%nat))).
Definition Glog : Z := (Z.pred (Z.pos (P_of_succ_nat 375%nat))).
Definition Glogdata : Z := (Z.pred (Z.pos (P_of_succ_nat 8%nat))).
Definition Glogtopic : Z := (Z.pred (Z.pos (P_of_succ_nat 375%nat))).
Definition Gsha3 : Z := (Z.pred (Z.pos (P_of_succ_nat 30%nat))).
Definition Gsha3word : Z := (Z.pred (Z.pos (P_of_succ_nat 6%nat))).
Definition Gcopy : Z := (Z.pred (Z.pos (P_of_succ_nat 3%nat))).
Definition Gblockhash : Z := (Z.pred (Z.pos (P_of_succ_nat 20%nat))).
Record call_env : Type := {
callenv_gaslimit : w256 ;
callenv_value : w256 ;
callenv_data : list byte ;
callenv_caller : address ;
callenv_timestamp : w256 ;
callenv_blocknum : w256 ;
callenv_balance : address -> w256
}.
Notation "{[ r 'with' 'callenv_gaslimit' := e ]}" := ({| callenv_gaslimit := e; callenv_value := callenv_value r; callenv_data := callenv_data r; callenv_caller := callenv_caller r; callenv_timestamp := callenv_timestamp r; callenv_blocknum := callenv_blocknum r; callenv_balance := callenv_balance r |}).
Notation "{[ r 'with' 'callenv_value' := e ]}" := ({| callenv_value := e; callenv_gaslimit := callenv_gaslimit r; callenv_data := callenv_data r; callenv_caller := callenv_caller r; callenv_timestamp := callenv_timestamp r; callenv_blocknum := callenv_blocknum r; callenv_balance := callenv_balance r |}).
Notation "{[ r 'with' 'callenv_data' := e ]}" := ({| callenv_data := e; callenv_gaslimit := callenv_gaslimit r; callenv_value := callenv_value r; callenv_caller := callenv_caller r; callenv_timestamp := callenv_timestamp r; callenv_blocknum := callenv_blocknum r; callenv_balance := callenv_balance r |}).
Notation "{[ r 'with' 'callenv_caller' := e ]}" := ({| callenv_caller := e; callenv_gaslimit := callenv_gaslimit r; callenv_value := callenv_value r; callenv_data := callenv_data r; callenv_timestamp := callenv_timestamp r; callenv_blocknum := callenv_blocknum r; callenv_balance := callenv_balance r |}).
Notation "{[ r 'with' 'callenv_timestamp' := e ]}" := ({| callenv_timestamp := e; callenv_gaslimit := callenv_gaslimit r; callenv_value := callenv_value r; callenv_data := callenv_data r; callenv_caller := callenv_caller r; callenv_blocknum := callenv_blocknum r; callenv_balance := callenv_balance r |}).
Notation "{[ r 'with' 'callenv_blocknum' := e ]}" := ({| callenv_blocknum := e; callenv_gaslimit := callenv_gaslimit r; callenv_value := callenv_value r; callenv_data := callenv_data r; callenv_caller := callenv_caller r; callenv_timestamp := callenv_timestamp r; callenv_balance := callenv_balance r |}).
Notation "{[ r 'with' 'callenv_balance' := e ]}" := ({| callenv_balance := e; callenv_gaslimit := callenv_gaslimit r; callenv_value := callenv_value r; callenv_data := callenv_data r; callenv_caller := callenv_caller r; callenv_timestamp := callenv_timestamp r; callenv_blocknum := callenv_blocknum r |}).
Definition call_env_default: call_env := {| callenv_gaslimit := w256_default; callenv_value := w256_default; callenv_data := DAEMON; callenv_caller := address_default; callenv_timestamp := w256_default; callenv_blocknum := w256_default; callenv_balance := (fun (x116 : address ) => w256_default) |}.
Record return_result : Type := {
return_data : list byte ;
return_balance : address -> w256
}.
Notation "{[ r 'with' 'return_data' := e ]}" := ({| return_data := e; return_balance := return_balance r |}).
Notation "{[ r 'with' 'return_balance' := e ]}" := ({| return_balance := e; return_data := return_data r |}).
Definition return_result_default: return_result := {| return_data := DAEMON; return_balance := (fun (x115 : address ) => w256_default) |}.
Inductive environment_action : Type :=
| EnvironmentCall: call_env -> environment_action
| EnvironmentRet: return_result -> environment_action
| EnvironmentFail: environment_action .
Definition environment_action_default: environment_action := EnvironmentCall call_env_default.
Record call_arguments : Type := {
callarg_gas : w256 ;
callarg_code : address ;
callarg_recipient : address ;
callarg_value : w256 ;
callarg_data : list byte ;
callarg_output_begin : w256 ;
callarg_output_size : w256
}.
Notation "{[ r 'with' 'callarg_gas' := e ]}" := ({| callarg_gas := e; callarg_code := callarg_code r; callarg_recipient := callarg_recipient r; callarg_value := callarg_value r; callarg_data := callarg_data r; callarg_output_begin := callarg_output_begin r; callarg_output_size := callarg_output_size r |}).
Notation "{[ r 'with' 'callarg_code' := e ]}" := ({| callarg_code := e; callarg_gas := callarg_gas r; callarg_recipient := callarg_recipient r; callarg_value := callarg_value r; callarg_data := callarg_data r; callarg_output_begin := callarg_output_begin r; callarg_output_size := callarg_output_size r |}).
Notation "{[ r 'with' 'callarg_recipient' := e ]}" := ({| callarg_recipient := e; callarg_gas := callarg_gas r; callarg_code := callarg_code r; callarg_value := callarg_value r; callarg_data := callarg_data r; callarg_output_begin := callarg_output_begin r; callarg_output_size := callarg_output_size r |}).
Notation "{[ r 'with' 'callarg_value' := e ]}" := ({| callarg_value := e; callarg_gas := callarg_gas r; callarg_code := callarg_code r; callarg_recipient := callarg_recipient r; callarg_data := callarg_data r; callarg_output_begin := callarg_output_begin r; callarg_output_size := callarg_output_size r |}).
Notation "{[ r 'with' 'callarg_data' := e ]}" := ({| callarg_data := e; callarg_gas := callarg_gas r; callarg_code := callarg_code r; callarg_recipient := callarg_recipient r; callarg_value := callarg_value r; callarg_output_begin := callarg_output_begin r; callarg_output_size := callarg_output_size r |}).
Notation "{[ r 'with' 'callarg_output_begin' := e ]}" := ({| callarg_output_begin := e; callarg_gas := callarg_gas r; callarg_code := callarg_code r; callarg_recipient := callarg_recipient r; callarg_value := callarg_value r; callarg_data := callarg_data r; callarg_output_size := callarg_output_size r |}).
Notation "{[ r 'with' 'callarg_output_size' := e ]}" := ({| callarg_output_size := e; callarg_gas := callarg_gas r; callarg_code := callarg_code r; callarg_recipient := callarg_recipient r; callarg_value := callarg_value r; callarg_data := callarg_data r; callarg_output_begin := callarg_output_begin r |}).
Definition call_arguments_default: call_arguments := {| callarg_gas := w256_default; callarg_code := address_default; callarg_recipient := address_default; callarg_value := w256_default; callarg_data := DAEMON; callarg_output_begin := w256_default; callarg_output_size := w256_default |}.
Record create_arguments : Type := {
createarg_value : w256 ;
createarg_code : list byte
}.
Notation "{[ r 'with' 'createarg_value' := e ]}" := ({| createarg_value := e; createarg_code := createarg_code r |}).
Notation "{[ r 'with' 'createarg_code' := e ]}" := ({| createarg_code := e; createarg_value := createarg_value r |}).
Definition create_arguments_default: create_arguments := {| createarg_value := w256_default; createarg_code := DAEMON |}.
Inductive failure_reason : Type :=
| OutOfGas: failure_reason
| TooLongStack: failure_reason
| TooShortStack: failure_reason
| InvalidJumpDestination: failure_reason
| ShouldNotHappen: failure_reason .
Definition failure_reason_default: failure_reason := OutOfGas.
Inductive contract_action : Type :=
| ContractCall: call_arguments -> contract_action
| ContractDelegateCall: call_arguments -> contract_action
| ContractCreate: create_arguments -> contract_action
| ContractFail: list failure_reason -> contract_action
| ContractSuicide: address -> contract_action
| ContractReturn: list byte -> contract_action .
Definition contract_action_default: contract_action := ContractCall call_arguments_default.
Record program : Type := {
program_content : Z -> option inst ;
program_length : Z
}.
Notation "{[ r 'with' 'program_content' := e ]}" := ({| program_content := e; program_length := program_length r |}).
Notation "{[ r 'with' 'program_length' := e ]}" := ({| program_length := e; program_content := program_content r |}).
Definition program_default: program := {| program_content := (fun (x114 : Z ) => DAEMON); program_length := Z_default |}.
Definition empty_program : program := {|program_content := (fun ( _ : Z ) => None);program_length :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))))
|}.
Definition program_of_lst (lst : list (inst )) (program_content_formatter : list (inst ) -> Z -> option (inst ) ) : program := {|program_content := (program_content_formatter lst);program_length := ((Z.pred (Z.pos (P_of_succ_nat (List.length lst)))))
|}.
Definition program_as_natural_map (p : program ) (idx : nat ) : word8 :=
match ((program_content p) ((Z.pred (Z.pos (P_of_succ_nat idx))))) with
| None =>(word8FromNumeral 0%nat)
| Some inst1 =>
match ( lem_list.index (inst_code inst1)( 0%nat)) with
| None =>(word8FromNumeral 0%nat)
| Some a => a
end
end.
Record block_info : Type := {
block_blockhash : w256 -> w256 ;
block_coinbase : address ;
block_timestamp : w256 ;
block_number : w256 ;
block_difficulty : w256 ;
block_gaslimit : w256
}.
Notation "{[ r 'with' 'block_blockhash' := e ]}" := ({| block_blockhash := e; block_coinbase := block_coinbase r; block_timestamp := block_timestamp r; block_number := block_number r; block_difficulty := block_difficulty r; block_gaslimit := block_gaslimit r |}).
Notation "{[ r 'with' 'block_coinbase' := e ]}" := ({| block_coinbase := e; block_blockhash := block_blockhash r; block_timestamp := block_timestamp r; block_number := block_number r; block_difficulty := block_difficulty r; block_gaslimit := block_gaslimit r |}).
Notation "{[ r 'with' 'block_timestamp' := e ]}" := ({| block_timestamp := e; block_blockhash := block_blockhash r; block_coinbase := block_coinbase r; block_number := block_number r; block_difficulty := block_difficulty r; block_gaslimit := block_gaslimit r |}).
Notation "{[ r 'with' 'block_number' := e ]}" := ({| block_number := e; block_blockhash := block_blockhash r; block_coinbase := block_coinbase r; block_timestamp := block_timestamp r; block_difficulty := block_difficulty r; block_gaslimit := block_gaslimit r |}).
Notation "{[ r 'with' 'block_difficulty' := e ]}" := ({| block_difficulty := e; block_blockhash := block_blockhash r; block_coinbase := block_coinbase r; block_timestamp := block_timestamp r; block_number := block_number r; block_gaslimit := block_gaslimit r |}).
Notation "{[ r 'with' 'block_gaslimit' := e ]}" := ({| block_gaslimit := e; block_blockhash := block_blockhash r; block_coinbase := block_coinbase r; block_timestamp := block_timestamp r; block_number := block_number r; block_difficulty := block_difficulty r |}).
Definition block_info_default: block_info := {| block_blockhash := (fun (x113 : w256 ) => w256_default); block_coinbase := address_default; block_timestamp := w256_default; block_number := w256_default; block_difficulty := w256_default; block_gaslimit := w256_default |}.
Record log_entry : Type := {
log_addr : address ;
log_topics : list w256 ;
log_data : list byte
}.
Notation "{[ r 'with' 'log_addr' := e ]}" := ({| log_addr := e; log_topics := log_topics r; log_data := log_data r |}).
Notation "{[ r 'with' 'log_topics' := e ]}" := ({| log_topics := e; log_addr := log_addr r; log_data := log_data r |}).
Notation "{[ r 'with' 'log_data' := e ]}" := ({| log_data := e; log_addr := log_addr r; log_topics := log_topics r |}).
Definition log_entry_default: log_entry := {| log_addr := address_default; log_topics := DAEMON; log_data := DAEMON |}.
Record variable_ctx : Type := {
vctx_stack : list w256 ;
vctx_memory : memory ;
vctx_memory_usage : Z ;
vctx_storage : storage ;
vctx_pc : Z ;
vctx_balance : address -> w256 ;
vctx_caller : address ;
vctx_value_sent : w256 ;
vctx_data_sent : list byte ;
vctx_storage_at_call : storage ;
vctx_balance_at_call : address -> w256 ;
vctx_origin : address ;
vctx_ext_program : address -> program ;
vctx_block : block_info ;
vctx_gas : Z ;
vctx_account_existence : address -> bool ;
vctx_touched_storage_index : list w256 ;
vctx_logs : list log_entry ;
vctx_refund : Z ;
vctx_gasprice : w256
}.
Notation "{[ r 'with' 'vctx_stack' := e ]}" := ({| vctx_stack := e; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_memory' := e ]}" := ({| vctx_memory := e; vctx_stack := vctx_stack r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_memory_usage' := e ]}" := ({| vctx_memory_usage := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_storage' := e ]}" := ({| vctx_storage := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_pc' := e ]}" := ({| vctx_pc := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_balance' := e ]}" := ({| vctx_balance := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_caller' := e ]}" := ({| vctx_caller := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_value_sent' := e ]}" := ({| vctx_value_sent := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_data_sent' := e ]}" := ({| vctx_data_sent := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_storage_at_call' := e ]}" := ({| vctx_storage_at_call := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_balance_at_call' := e ]}" := ({| vctx_balance_at_call := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_origin' := e ]}" := ({| vctx_origin := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_ext_program' := e ]}" := ({| vctx_ext_program := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_block' := e ]}" := ({| vctx_block := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_gas' := e ]}" := ({| vctx_gas := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_account_existence' := e ]}" := ({| vctx_account_existence := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_touched_storage_index' := e ]}" := ({| vctx_touched_storage_index := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_logs' := e ]}" := ({| vctx_logs := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_refund := vctx_refund r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_refund' := e ]}" := ({| vctx_refund := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_gasprice := vctx_gasprice r |}).
Notation "{[ r 'with' 'vctx_gasprice' := e ]}" := ({| vctx_gasprice := e; vctx_stack := vctx_stack r; vctx_memory := vctx_memory r; vctx_memory_usage := vctx_memory_usage r; vctx_storage := vctx_storage r; vctx_pc := vctx_pc r; vctx_balance := vctx_balance r; vctx_caller := vctx_caller r; vctx_value_sent := vctx_value_sent r; vctx_data_sent := vctx_data_sent r; vctx_storage_at_call := vctx_storage_at_call r; vctx_balance_at_call := vctx_balance_at_call r; vctx_origin := vctx_origin r; vctx_ext_program := vctx_ext_program r; vctx_block := vctx_block r; vctx_gas := vctx_gas r; vctx_account_existence := vctx_account_existence r; vctx_touched_storage_index := vctx_touched_storage_index r; vctx_logs := vctx_logs r; vctx_refund := vctx_refund r |}).
Definition variable_ctx_default: variable_ctx := {| vctx_stack := DAEMON; vctx_memory := memory_default; vctx_memory_usage := Z_default; vctx_storage := storage_default; vctx_pc := Z_default; vctx_balance := (fun (x109 : address ) => w256_default); vctx_caller := address_default; vctx_value_sent := w256_default; vctx_data_sent := DAEMON; vctx_storage_at_call := storage_default; vctx_balance_at_call := (fun (x110 : address ) => w256_default); vctx_origin := address_default; vctx_ext_program := (fun (x111 : address ) => program_default); vctx_block := block_info_default; vctx_gas := Z_default; vctx_account_existence := (fun (x112 : address ) => bool_default); vctx_touched_storage_index := DAEMON; vctx_logs := DAEMON; vctx_refund := Z_default; vctx_gasprice := w256_default |}.
Record constant_ctx : Type := {
cctx_program : program ;
cctx_this : address ;
cctx_hash_filter : list byte -> bool
}.
Notation "{[ r 'with' 'cctx_program' := e ]}" := ({| cctx_program := e; cctx_this := cctx_this r; cctx_hash_filter := cctx_hash_filter r |}).
Notation "{[ r 'with' 'cctx_this' := e ]}" := ({| cctx_this := e; cctx_program := cctx_program r; cctx_hash_filter := cctx_hash_filter r |}).
Notation "{[ r 'with' 'cctx_hash_filter' := e ]}" := ({| cctx_hash_filter := e; cctx_program := cctx_program r; cctx_this := cctx_this r |}).
Definition constant_ctx_default: constant_ctx := {| cctx_program := program_default; cctx_this := address_default; cctx_hash_filter := (fun (x108 : list byte ) => bool_default) |}.
Inductive instruction_result : Type :=
| InstructionContinue: variable_ctx -> instruction_result
| InstructionToEnvironment:
contract_action
-> variable_ctx
-> option ((Z * Z ) % type) -> instruction_result .
Definition instruction_result_default: instruction_result := InstructionContinue variable_ctx_default.
Definition instruction_failure_result (v : variable_ctx ) (reasons : list (failure_reason )) : instruction_result :=
InstructionToEnvironment (ContractFail reasons) v None.
Definition instruction_return_result (x : list (byte )) (v : variable_ctx ) : instruction_result :=
InstructionToEnvironment (ContractReturn x) v None.
Definition gas (v : variable_ctx ) : (Bvector 256) := word256FromInteger(vctx_gas v).
Definition M (s : Z ) (f : (Bvector 256) ) (l : (Bvector 256) ) : Z :=
if classical_boolean_equivalence l(word256FromNumeral 0%nat) then s else Z.max s ( Z.div( Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.add(uint f) (uint l))((Z.pred (Z.pos (P_of_succ_nat 31%nat)))))((Z.pred (Z.pos (P_of_succ_nat 32%nat))))).
Definition update_balance (a : word160 ) (f : (Bvector 256) -> (Bvector 256) ) (orig : word160 -> (Bvector 256) ) (x : word160 ) : (Bvector 256) := if classical_boolean_equivalence x a then f (orig a) else orig x.
Definition vctx_pop_stack (n : nat ) (v : variable_ctx ) : variable_ctx :=
{[ v with vctx_stack := drop n(vctx_stack v) ]}.
Definition vctx_update_storage (idx : (Bvector 256) ) (vall : (Bvector 256) ) (v : variable_ctx ) : variable_ctx :=
{[ v with vctx_storage := (fun (x : (Bvector 256) ) => if classical_boolean_equivalence x idx then vall else(vctx_storage v) x) ]}.
Definition vctx_next_instruction (v : variable_ctx ) (c : constant_ctx ) : option (inst ) :=
match ((program_content (cctx_program c))(vctx_pc v)) with
| Some i => Some i
| None => Some (Misc STOP)
end.
Definition vctx_advance_pc (c : constant_ctx ) (v : variable_ctx ) : variable_ctx :=
{[ v with vctx_pc :=
(match ( vctx_next_instruction v c) with
| None => Coq.ZArith.BinInt.Z.add(vctx_pc v)((Z.pred (Z.pos (P_of_succ_nat 1%nat))))
| Some inst1 => Coq.ZArith.BinInt.Z.add(vctx_pc v) ( (inst_size inst1)) end) ]}.
Definition stack_0_0_op (v : variable_ctx ) (c : constant_ctx ) : instruction_result := InstructionContinue (vctx_advance_pc c v).
Definition stack_0_1_op (v : variable_ctx ) (c : constant_ctx ) (w : (Bvector 256) ) : instruction_result :=
InstructionContinue (vctx_advance_pc c {[ v with vctx_stack := w ::(vctx_stack v) ]}).
Definition stack_1_1_op (v : variable_ctx ) (c : constant_ctx ) (f : (Bvector 256) -> (Bvector 256) ) : instruction_result := match ((vctx_stack v)) with
| [] => instruction_failure_result v [TooShortStack]
| h :: t => InstructionContinue (vctx_advance_pc c {[ v with vctx_stack := f h :: t ]})
end.
Definition stack_2_1_op (v : variable_ctx ) (c : constant_ctx ) (f : (Bvector 256) -> (Bvector 256) -> (Bvector 256) ) : instruction_result := match ((vctx_stack v)) with
| operand0 :: operand1 :: rest =>
InstructionContinue
(vctx_advance_pc c {[ v with vctx_stack := f operand0 operand1 :: rest ]})
| _ => instruction_failure_result v [TooShortStack]
end.
Definition stack_3_1_op (v : variable_ctx ) (c : constant_ctx ) (f : (Bvector 256) -> (Bvector 256) -> (Bvector 256) -> (Bvector 256) ) : instruction_result := match ((vctx_stack v)) 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.
Definition vctx_stack_default (idx : Z ) (v : variable_ctx ) : (Bvector 256) :=
match ( lem_list.index(vctx_stack v) (Z.abs_nat idx)) with
| Some w => w
| None =>(word256FromNumeral 0%nat)
end.
Definition new_memory_consumption (i : inst ) (original_memory_usage : Z ) (s0 : (Bvector 256) ) (s1 : (Bvector 256) ) (s2 : (Bvector 256) ) (s3 : (Bvector 256) ) (s4 : (Bvector 256) ) (s5 : (Bvector 256) ) (s6 : (Bvector 256) ) : Z :=
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(word256FromNumeral 32%nat)
| Memory MSTORE =>
M original_memory_usage s0(word256FromNumeral 32%nat)
| Memory MSTORE8 =>
M original_memory_usage s0(word256FromNumeral 1%nat)
| 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.
Definition check_refund (oldv : (Bvector 256) ) (newv : (Bvector 256) ) : Z := if unsafe_structural_inequality oldv(word256FromNumeral 0%nat) && classical_boolean_equivalence newv(word256FromNumeral 0%nat) then(Z.pred (Z.pos (P_of_succ_nat 15000%nat))) else(Z.pred (Z.pos (P_of_succ_nat 0%nat))).
Definition sstore (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| addr :: vl :: stack_tail =>
InstructionContinue (vctx_advance_pc c
(vctx_update_storage addr vl
{[ {[
{[ v with vctx_refund := Coq.ZArith.BinInt.Z.add (vctx_refund v)
(check_refund ((vctx_storage v) addr) vl) ]} with vctx_touched_storage_index :=
addr :: (vctx_touched_storage_index v) ]} with vctx_stack := stack_tail ]}))
| _ => instruction_failure_result v [TooShortStack]
end.
Definition jump (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| [] => instruction_failure_result v [TooShortStack]
| pos :: tl =>
let v_new := {[ {[ v with vctx_pc := uint pos ]} with vctx_stack := tl ]} in
match ( vctx_next_instruction v_new c) with
| Some( Pc JUMPDEST) => InstructionContinue v_new
| _ => instruction_failure_result v [InvalidJumpDestination]
end
end.
Definition blockedInstructionContinue (v : variable_ctx ) ( _ : bool ) : instruction_result := InstructionContinue v.
Definition blocked_jump (v : variable_ctx ) (c : constant_ctx ) ( _ : bool ) : instruction_result := jump v c.
Definition strict_if {a : Type} (b : bool ) (x : bool -> a) (y : bool -> a) : a:= if b then x true else y true.
Definition jumpi (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| pos :: cond :: rest =>
let new_env := {[ v with vctx_stack := pos :: rest ]} in
strict_if ( classical_boolean_equivalence cond(word256FromNumeral 0%nat))
(blockedInstructionContinue (vctx_advance_pc c (vctx_pop_stack( 2%nat) v)))
(blocked_jump new_env c)
| _ => instruction_failure_result v [TooShortStack]
end.
Definition datasize (v : variable_ctx ) : (Bvector 256) := word256FromNat (List.length(vctx_data_sent v)).
Definition byte_list_fill_right (filled : word8 ) (target : nat ) (orig : list (word8 )) : list (word8 ):=
if nat_gteb (List.length orig) target then orig else
let filling_len := Coq.Init.Peano.minus target (List.length orig) in
(@ List.app _) orig (replicate filling_len filled).
Definition constant_mark (lst : list (byte )) : list (byte ):= lst.
Definition read_word_from_bytes (idx : nat ) (lst : list (word8 )) : (Bvector 256) :=
if nat_lteb ( (List.length lst)) idx then(word256FromNumeral 0%nat)
else
word_of_bytes
(byte_list_fill_right(word8FromNumeral 0%nat)( 32%nat)
(take( 32%nat) (drop ( idx) lst))).
Definition cut_data (v : variable_ctx ) (idx : (Bvector 256) ) : (Bvector 256) := read_word_from_bytes (word256ToNatural idx)(vctx_data_sent v).
Program Fixpoint cut_natural_map (idx : nat ) (n : nat ) (nmap : nat -> word8 ) : list (word8 ):= match ( n) with
| 0%nat => []
| S (n) => nmap idx :: cut_natural_map ( Coq.Init.Peano.plus idx( 1%nat)) n nmap
end.
Definition Cnew (value1 : (Bvector 256) ) (emp : bool ) : Z := if emp then Gnewaccount else(Z.pred (Z.pos (P_of_succ_nat 0%nat))).
Definition Cxfer (value1 : (Bvector 256) ) : Z := if classical_boolean_equivalence value1(word256FromNumeral 0%nat) then(Z.pred (Z.pos (P_of_succ_nat 0%nat))) else Gcallvalue.
Definition Cextra (value1 : (Bvector 256) ) (emp : bool ) (net : network ) : Z := Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.add (Gcall net) (Cxfer value1)) (Cnew value1 emp).
Definition L (x : Z ) : Z := Coq.ZArith.BinInt.Z.sub x (Z.div x((Z.pred (Z.pos (P_of_succ_nat 64%nat))))).
Definition Cgascap (mu0 : (Bvector 256) ) (mu2 : (Bvector 256) ) (emp : bool ) (remaining_gas : Z ) (net : network ) (memu_extra : Z ) : Z :=
if int_gteb remaining_gas (Coq.ZArith.BinInt.Z.add (Cextra mu2 emp net) memu_extra) then
Z.min (L ( Coq.ZArith.BinInt.Z.sub (Coq.ZArith.BinInt.Z.sub remaining_gas (Cextra mu2 emp net)) memu_extra)) (uint mu0)
else
uint mu0.
Definition Ccallgas (mu0 : (Bvector 256) ) (mu1 : (Bvector 256) ) (mu2 : (Bvector 256) ) (emp : bool ) (remaining_gas : Z ) (net : network ) (memu_extra : Z ) : Z := Coq.ZArith.BinInt.Z.add
( if at_least_eip150 net then Cgascap mu0 mu2 emp remaining_gas net memu_extra else uint mu0)
( if classical_boolean_equivalence mu2(word256FromNumeral 0%nat) then(Z.pred (Z.pos (P_of_succ_nat 0%nat))) else Gcallstipend ).
Definition Ccall (mu0 : (Bvector 256) ) (mu1 : (Bvector 256) ) (mu2 : (Bvector 256) ) (emp : bool ) (remaining_gas : Z ) (net : network ) (memu_extra : Z ) : Z := Coq.ZArith.BinInt.Z.add
( if at_least_eip150 net then Cgascap mu0 mu2 emp remaining_gas net memu_extra else (Z.pred (Z.pos (P_of_succ_nat (word256ToNatural mu0)))) )
(Cextra mu2 emp net).
Definition Cmem (a : Z ) : Z := Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.mul Gmemory a) ( Z.div (Coq.ZArith.BinInt.Z.mul a a)((Z.pred (Z.pos (P_of_succ_nat 512%nat))))).
Definition Csstore (orig : (Bvector 256) ) (newer : (Bvector 256) ) : Z := if negb ( classical_boolean_equivalence newer(word256FromNumeral 0%nat)) && classical_boolean_equivalence orig(word256FromNumeral 0%nat) then Gsset else Gsreset.
Definition Csuicide (recipient_empty : bool ) (net : network ) : Z := Coq.ZArith.BinInt.Z.add
(Gsuicide net) (if recipient_empty && at_least_eip150 net then Gnewaccount else(Z.pred (Z.pos (P_of_succ_nat 0%nat)))).
Definition vctx_next_instruction_default (v : variable_ctx ) (c : constant_ctx ) : inst :=
match ( vctx_next_instruction v c) with
| Some i => i
| None => Misc STOP
end.
Definition vctx_recipient (v : variable_ctx ) (c : constant_ctx ) : word160 :=
match ( vctx_next_instruction_default v c) with
| Misc SUICIDE => w256_to_address (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) v)
| Misc CALL => w256_to_address (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 1%nat)))) v)
| Misc CALLCODE =>(cctx_this c)
| Misc DELEGATECALL =>(cctx_this c)
| _ =>word160FromNumeral 0%nat
end.
Definition calc_memu_extra (orig_memory_usage : Z ) (s0 : (Bvector 256) ) (s1 : (Bvector 256) ) (s2 : (Bvector 256) ) (s3 : (Bvector 256) ) (s4 : (Bvector 256) ) (s5 : (Bvector 256) ) (s6 : (Bvector 256) ) : Z := Coq.ZArith.BinInt.Z.sub
(Cmem (new_memory_consumption (Misc CALL) orig_memory_usage s0 s1 s2 s3 s4 s5 s6)) (Cmem orig_memory_usage).
Definition calc_memu_extra2 (v : variable_ctx ) (s0 : (Bvector 256) ) (s1 : (Bvector 256) ) (s2 : (Bvector 256) ) (s3 : (Bvector 256) ) (s4 : (Bvector 256) ) (s5 : (Bvector 256) ) (s6 : (Bvector 256) ) : Z := Coq.ZArith.BinInt.Z.sub (Cmem (new_memory_consumption (Misc DELEGATECALL)(vctx_memory_usage v) s0 s1 s2 s3 s4 s5 s6)) (Cmem(vctx_memory_usage v)).
Definition call (net : network ) (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| g :: r :: value1 :: in_begin :: in_size :: out_begin :: out_size :: rest =>
InstructionToEnvironment (ContractCall
{|callarg_gas := (word256FromInteger (Ccallgas g r value1
(negb ((vctx_account_existence v) (vctx_recipient v c)))(vctx_gas
v) net (calc_memu_extra(vctx_memory_usage v) g r value1 in_begin in_size out_begin out_size)));callarg_code := (w256_to_address r);callarg_recipient := (w256_to_address r);callarg_value := value1;callarg_data := (cut_memory in_begin in_size(vctx_memory v));callarg_output_begin := out_begin;callarg_output_size := out_size |})
( {[{[ (vctx_advance_pc c v) with vctx_balance := update_balance(cctx_this c) (fun (orig : (Bvector 256) ) => word256Minus orig value1)(vctx_balance v) ]} with vctx_stack := rest ]})
(Some
(uint out_begin, uint out_size))
| _ => instruction_failure_result v [TooShortStack]
end.
Definition delegatecall (net : network ) (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| e0 :: e1 :: e3 :: e4 :: e5 :: e6 :: rest =>
InstructionToEnvironment
(ContractDelegateCall
{|callarg_gas := (word256FromInteger (Ccallgas e0 e1(word256FromNumeral 0%nat)
(negb ((vctx_account_existence v) (vctx_recipient v c)))(vctx_gas v) net (calc_memu_extra2 v e0 e1 e3 e4 e5 e6 (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 6%nat)))) v))));callarg_code := (w256_to_address e1);callarg_recipient := (w256_to_address e1);callarg_value :=(vctx_value_sent v);callarg_data := (cut_memory e3 e4(vctx_memory v));callarg_output_begin := e5;callarg_output_size := e6 |})
({[ (vctx_advance_pc c v) with vctx_stack := rest ]})
(Some
(uint e5, uint e6))
| _ => instruction_failure_result v [TooShortStack]
end.
Definition callcode (net : network ) (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| e0 :: e1 :: e2 :: e3 :: e4 :: e5 :: e6 :: rest =>
InstructionToEnvironment
(ContractCall
{|callarg_gas := (word256FromInteger (Ccallgas e0 e1 e2
(negb ((vctx_account_existence v) (vctx_recipient v c)))(vctx_gas v) net
(calc_memu_extra(vctx_memory_usage v) e0 e1 e2 e3 e4 e5 e6)));callarg_code := (w256_to_address e1);callarg_recipient :=(cctx_this c);callarg_value := e2;callarg_data := (cut_memory e3 e4(vctx_memory v));callarg_output_begin := e5;callarg_output_size := e6 |})
({[ (vctx_advance_pc c v) with vctx_stack := rest ]})
(Some (uint e5, uint e6))
| _ => instruction_failure_result v [TooShortStack]
end.
Definition create (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| vl :: code_start :: code_len :: rest =>
let code := cut_memory code_start code_len(vctx_memory v) in
InstructionToEnvironment
(ContractCreate
{|createarg_value := vl;createarg_code := code |})
({[ (vctx_advance_pc c v) with vctx_stack := rest ]})
(Some
((Z.pred (Z.pos (P_of_succ_nat 0%nat))),(Z.pred (Z.pos (P_of_succ_nat 0%nat)))))
| _ => instruction_failure_result v [TooShortStack]
end.
Definition vctx_returned_bytes (v : variable_ctx ) : list (word8 ):= match ((vctx_stack v)) with
| e0 :: e1 :: _ => cut_memory e0 e1(vctx_memory v)
| _ => []
end.
Definition ret (v : variable_ctx ) ( _ : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| _ :: _ :: _ =>
InstructionToEnvironment (ContractReturn (vctx_returned_bytes v))
v
None
| _ => instruction_failure_result v [TooShortStack]
end.
Definition stop (v : variable_ctx ) ( _ : constant_ctx ) : instruction_result :=
InstructionToEnvironment (ContractReturn []) v None.
Definition pop (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| _ :: tl => InstructionContinue (vctx_advance_pc c {[ v with vctx_stack := tl ]})
| [] => instruction_failure_result v [TooShortStack]
end.
Definition general_dup (n : word4 ) (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ( lem_list.index(vctx_stack v) (word4ToNat n)) with
| None => instruction_failure_result v [TooShortStack]
| Some duplicated => InstructionContinue (vctx_advance_pc c {[ v with vctx_stack := duplicated ::(vctx_stack v) ]})
end.
Definition store_byte_list_memory (pos : (Bvector 256) ) (lst : list (word8 )) (orig : (Bvector 256) -> word8 ) (p : (Bvector 256) ) : word8 := match ( index lst ( (word256ToNatural (word256Minus p pos)))) with
| Some e => e
| None => orig p
end.
Definition store_word_memory (pos : (Bvector 256) ) (vl : (Bvector 256) ) (mem : w256 -> byte ) : w256 -> byte :=
store_byte_list_memory pos (word_rsplit256 vl) mem.
Definition mstore (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| pos :: vl :: rest =>
let new_memory := store_word_memory pos vl(vctx_memory v) in
InstructionContinue (vctx_advance_pc c
{[ {[ v with vctx_memory := new_memory ]} with vctx_stack := rest ]})
| _ => instruction_failure_result v [TooShortStack]
end.
Definition mload (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| pos :: rest =>
let value1 := read_word_from_bytes( 0%nat) (cut_memory pos(word256FromNumeral 32%nat)(vctx_memory v)) in
InstructionContinue
(vctx_advance_pc c {[ v with vctx_stack := value1 :: rest ]})
| _ => instruction_failure_result v [TooShortStack]
end.
Definition mstore8 (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| pos :: vl :: rest =>
let new_memory := (fun (p : (Bvector 256) ) => if classical_boolean_equivalence p pos then w256_to_byte vl else(vctx_memory v) p) in
InstructionContinue (vctx_advance_pc c
{[ {[ v with vctx_memory := new_memory ]} with vctx_stack := rest ]})
| _ => instruction_failure_result v [TooShortStack]
end.
Definition input_as_natural_map (lst : list (word8 )) (idx : nat ) : word8 :=
let idx := (Z.pred (Z.pos (P_of_succ_nat idx))) in
if int_gtb((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) idx then(word8FromNumeral 0%nat)
else if int_lteb ((Z.pred (Z.pos (P_of_succ_nat (List.length lst))))) idx then(word8FromNumeral 0%nat)
else
match ( lem_list.index lst (Z.abs_nat ( idx))) with
| None =>(word8FromNumeral 0%nat)
| Some a => a
end.
Definition calldatacopy (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| dst_start :: src_start :: len :: rest =>
let data := cut_natural_map (word256ToNatural src_start) (word256ToNatural len) (input_as_natural_map(vctx_data_sent v)) in
let new_memory := store_byte_list_memory dst_start data(vctx_memory v) in
InstructionContinue (vctx_advance_pc c
{[ {[ v with vctx_memory := new_memory ]} with vctx_stack := rest ]})
| _ => instruction_failure_result v [TooShortStack]
end.
Definition codecopy (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| dst_start :: src_start :: len :: rest =>
let data := cut_natural_map (word256ToNatural src_start) (word256ToNatural len)
(program_as_natural_map(cctx_program c)) in
let new_memory := store_byte_list_memory dst_start data(vctx_memory v) in
InstructionContinue (vctx_advance_pc c
{[ {[ v with vctx_memory := new_memory ]} with vctx_stack := rest ]})
| _ => instruction_failure_result v [TooShortStack]
end.
Definition extcodecopy (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| addr :: dst_start :: src_start :: len :: rest =>
let data := cut_natural_map (word256ToNatural src_start) (word256ToNatural len)
(program_as_natural_map
((vctx_ext_program v) (w256_to_address addr))) in
let new_memory := store_byte_list_memory dst_start data(vctx_memory v) in
InstructionContinue (vctx_advance_pc c
{[ {[ v with vctx_memory := new_memory ]} with vctx_stack := rest ]})
| _ => instruction_failure_result v [TooShortStack]
end.
Definition pc (v : variable_ctx ) (c : constant_ctx ) : instruction_result :=
InstructionContinue (vctx_advance_pc c
{[ v with vctx_stack := word256FromInteger(vctx_pc v) ::(vctx_stack v) ]}).
Definition create_log_entry (n : nat ) (v : variable_ctx ) (c : constant_ctx ) : log_entry :=
{|log_addr :=(cctx_this c)
;log_topics := (drop( 2%nat) (take ( Coq.Init.Peano.plus n( 2%nat))(vctx_stack v)))
;log_data := (vctx_returned_bytes v)
|}.
Definition log (n : nat ) (v : variable_ctx ) (c : constant_ctx ) : instruction_result :=
let new_log_entry := create_log_entry n v c in
InstructionContinue
(vctx_advance_pc c (vctx_pop_stack (Coq.Init.Peano.plus n( 2%nat))
{[ v with vctx_logs := new_log_entry ::(vctx_logs v) ]})).
Definition list_swap {a : Type} (n : nat ) (lst : list a) : option (list a) := match ( (index lst n, index lst( 0%nat))) with
| (Some n_th, Some first) => Some (lem_list.concat [[n_th]; take ( Coq.Init.Peano.minus n( 1%nat)) (drop( 1%nat) lst); [first]; drop ( Coq.Init.Peano.plus( 1%nat) n) lst])
| _ => None
end.
Definition swap (n : nat ) (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ( list_swap ( Coq.Init.Peano.plus n( 1%nat))(vctx_stack v)) with
| None => instruction_failure_result v [TooShortStack]
| Some new_stack => InstructionContinue (vctx_advance_pc c {[ v with vctx_stack := new_stack ]})
end.
Definition sha3 (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| start :: len :: rest =>
let lst := cut_memory start len(vctx_memory v) in
if negb ((cctx_hash_filter c) 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.
Definition suicide (v : variable_ctx ) (c : constant_ctx ) : instruction_result := match ((vctx_stack v)) with
| dst :: _ =>
InstructionToEnvironment (ContractSuicide (w256_to_address dst)) v None
| _ => instruction_failure_result v [TooShortStack]
end.
Definition thirdComponentOfC (i : inst ) (s0 : (Bvector 256) ) (s1 : (Bvector 256) ) (s2 : (Bvector 256) ) (s3 : (Bvector 256) ) (recipient_empty : bool ) (orig_val : (Bvector 256) ) (new_val : (Bvector 256) ) (remaining_gas : Z ) (net : network ) : Z -> Z := fun (memu_extra : Z ) =>
match ( i) with
| Storage SSTORE => Csstore orig_val new_val
| Arith EXP => Coq.ZArith.BinInt.Z.add Gexp (if classical_boolean_equivalence s1(word256FromNumeral 0%nat) then(Z.pred (Z.pos (P_of_succ_nat 0%nat))) else Coq.ZArith.BinInt.Z.mul (Gexpbyte net) ( Coq.ZArith.BinInt.Z.add((Z.pred (Z.pos (P_of_succ_nat 1%nat)))) (log256floor (uint s1 : Z ))))
| Memory CALLDATACOPY => Coq.ZArith.BinInt.Z.add Gverylow (Coq.ZArith.BinInt.Z.mul Gcopy ( Z.div( Coq.ZArith.BinInt.Z.add(uint s2)((Z.pred (Z.pos (P_of_succ_nat 31%nat)))))((Z.pred (Z.pos (P_of_succ_nat 32%nat))))))
| Memory CODECOPY => Coq.ZArith.BinInt.Z.add Gverylow (Coq.ZArith.BinInt.Z.mul Gcopy ( Z.div( Coq.ZArith.BinInt.Z.add(uint s2)((Z.pred (Z.pos (P_of_succ_nat 31%nat)))))((Z.pred (Z.pos (P_of_succ_nat 32%nat))))))
| Memory EXTCODECOPY => Coq.ZArith.BinInt.Z.add (Gextcode net) (Coq.ZArith.BinInt.Z.mul Gcopy ( Z.div( Coq.ZArith.BinInt.Z.add(uint s3)((Z.pred (Z.pos (P_of_succ_nat 31%nat)))))((Z.pred (Z.pos (P_of_succ_nat 32%nat))))))
| Log LOG0 => Coq.ZArith.BinInt.Z.add Glog (Coq.ZArith.BinInt.Z.mul Glogdata (uint s1))
| Log LOG1 => Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.add Glog (Coq.ZArith.BinInt.Z.mul Glogdata (uint s1))) Glogtopic
| Log LOG2 => Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.add Glog (Coq.ZArith.BinInt.Z.mul Glogdata (uint s1))) (Coq.ZArith.BinInt.Z.mul((Z.pred (Z.pos (P_of_succ_nat 2%nat)))) Glogtopic)
| Log LOG3 => Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.add Glog (Coq.ZArith.BinInt.Z.mul Glogdata (uint s1))) (Coq.ZArith.BinInt.Z.mul((Z.pred (Z.pos (P_of_succ_nat 3%nat)))) Glogtopic)
| Log LOG4 => Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.add Glog (Coq.ZArith.BinInt.Z.mul Glogdata (uint s1))) (Coq.ZArith.BinInt.Z.mul((Z.pred (Z.pos (P_of_succ_nat 4%nat)))) 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(Z.pred (Z.pos (P_of_succ_nat 0%nat))) else Ccall s0 s1(word256FromNumeral 0%nat) recipient_empty remaining_gas net memu_extra
| Misc SUICIDE => Csuicide recipient_empty net
| Misc CREATE => Gcreate
| Arith SHA3 => Coq.ZArith.BinInt.Z.add Gsha3 (Coq.ZArith.BinInt.Z.mul Gsha3word ( Z.div( Coq.ZArith.BinInt.Z.add(uint s1)((Z.pred (Z.pos (P_of_succ_nat 31%nat)))))((Z.pred (Z.pos (P_of_succ_nat 32%nat))))))
| 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
| _ =>(Z.pred (Z.pos (P_of_succ_nat 0%nat)))
end.
Definition C (old_memory_consumption : Z ) (new_memory_consumption1 : Z ) (i : inst ) (s0 : (Bvector 256) ) (s1 : (Bvector 256) ) (s2 : (Bvector 256) ) (s3 : (Bvector 256) ) (recipient_empty : bool ) (orig : (Bvector 256) ) (new_val : (Bvector 256) ) (remaining_gas : Z ) (net : network ) : Z := Coq.ZArith.BinInt.Z.add (Coq.ZArith.BinInt.Z.sub
(Cmem new_memory_consumption1) (Cmem old_memory_consumption))
(thirdComponentOfC i s0 s1 s2 s3 recipient_empty orig new_val remaining_gas net ( Coq.ZArith.BinInt.Z.sub(Cmem new_memory_consumption1) (Cmem old_memory_consumption))).
Definition meter_gas (i : inst ) (v : variable_ctx ) (c : constant_ctx ) (net : network ) : Z :=
let musage := Z.max((Z.pred (Z.pos (P_of_succ_nat 0%nat))))(vctx_memory_usage v)
in C musage
(new_memory_consumption i musage (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 1%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 2%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 3%nat)))) v)
(vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 4%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 5%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 6%nat)))) v))
i
(vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 1%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 2%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 3%nat)))) v)
(negb ((vctx_account_existence v) (vctx_recipient v c))) ((vctx_storage v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) v))
(vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 1%nat)))) v)(vctx_gas v) net.
Definition check_resources (v : variable_ctx ) (c : constant_ctx ) (s : list ((Bvector 256) )) (i : inst ) (net : network ) : bool :=
match ( inst_stack_numbers i) with
| (consumed, produced) =>
( int_lteb (Coq.ZArith.BinInt.Z.sub (Coq.ZArith.BinInt.Z.add((Z.pred (Z.pos (P_of_succ_nat (List.length s))))) produced) consumed)((Z.pred (Z.pos (P_of_succ_nat 1024%nat))))) &&
( int_lteb(meter_gas i v c net)(vctx_gas v))
end.
Definition subtract_gas (consumption : Z ) (memory_usage : Z ) (orig : instruction_result ) : instruction_result :=
match ( orig) with
| InstructionContinue v =>
InstructionContinue ( {[{[ v with vctx_memory_usage := memory_usage ]} with vctx_gas := Coq.ZArith.BinInt.Z.sub(vctx_gas v) consumption ]})
| InstructionToEnvironment act v opt1 =>
InstructionToEnvironment act ( {[{[v with vctx_memory_usage := memory_usage ]} with vctx_gas := Coq.ZArith.BinInt.Z.sub(vctx_gas v) consumption ]}) opt1
end.
Definition signextend (len : (Bvector 256) ) (w : (Bvector 256) ) : (Bvector 256) :=
if int_gteb (uint len)((Z.pred (Z.pos (P_of_succ_nat 31%nat)))) then
w
else
let len : nat := Coq.Init.Peano.mult( 8%nat) ( Coq.Init.Peano.plus( (word256ToNatural len))( 1%nat)) in
let mask : (Bvector 256) := word256Minus (word256Power(word256FromNumeral 2%nat) len)(word256FromNumeral 1%nat) in
let masked : (Bvector 256) := word256Land w mask in
let middle : (Bvector 256) := word256Power(word256FromNumeral 2%nat) ( Coq.Init.Peano.minus len( 1%nat)) in
if w256Less masked middle then masked
else word256Minus (word256Minus masked middle) middle.
Definition instruction_sem (v : variable_ctx ) (c : constant_ctx ) (inst1 : inst ) (net : network ) : instruction_result :=
subtract_gas (meter_gas inst1 v c net) (new_memory_consumption inst1(vctx_memory_usage v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 1%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 2%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 3%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 4%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 5%nat)))) v) (vctx_stack_default((Z.pred (Z.pos (P_of_succ_nat 6%nat)))) v))
(match ( inst1) 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(vctx_storage v)
| Storage SSTORE => sstore v c
| Pc JUMPI => jumpi v c
| Pc JUMP => jump v c
| Pc JUMPDEST => stack_0_0_op v c
| Info CALLDATASIZE => stack_0_1_op v c (datasize v)
| Stack CALLDATALOAD => stack_1_1_op v c (cut_data v)
| Info CALLER => stack_0_1_op v c (address_to_w256(vctx_caller v))
| Arith ADD => stack_2_1_op v c (fun (a : (Bvector 256) ) (b : (Bvector 256) ) => word256Add a b)
| Arith SUB => stack_2_1_op v c (fun (a : (Bvector 256) ) (b : (Bvector 256) ) => word256Minus a b)
| Arith ISZERO => stack_1_1_op v c (fun (a : (Bvector 256) ) => if classical_boolean_equivalence a(word256FromNumeral 0%nat) then(word256FromNumeral 1%nat) else(word256FromNumeral 0%nat))
| 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(block_gaslimit (vctx_block v))
| Arith inst_GT => stack_2_1_op v c (fun (a : (Bvector 256) ) (b : (Bvector 256) ) => if word256UGT a b then(word256FromNumeral 1%nat) else(word256FromNumeral 0%nat))
| Arith inst_EQ => stack_2_1_op v c (fun (a : (Bvector 256) ) (b : (Bvector 256) ) => if classical_boolean_equivalence a b then(word256FromNumeral 1%nat) else(word256FromNumeral 0%nat))
| Bits inst_AND => stack_2_1_op v c (fun (a : (Bvector 256) ) (b : (Bvector 256) ) => word256Land a b)
| Bits inst_OR => stack_2_1_op v c (fun (a : (Bvector 256) ) (b : (Bvector 256) ) => word256Lor a b)
| Bits inst_XOR => stack_2_1_op v c (fun (a : (Bvector 256) ) (b : (Bvector 256) ) => word256Lxor a b)
| Bits inst_NOT => stack_1_1_op v c (fun (a : (Bvector 256) ) => word256Lnot a)
| Bits BYTE => stack_2_1_op v c get_byte
| Sarith SDIV => stack_2_1_op v c
(fun (n : (Bvector 256) ) (divisor : (Bvector 256) ) => if classical_boolean_equivalence divisor(word256FromNumeral 0%nat) then(word256FromNumeral 0%nat) else
let divisor := sintFromW256 divisor in
let n := sintFromW256 n in
let min_int : Z := (Coq.ZArith.BinInt.Z.sub Z0 ( Coq.ZArith.Zpower.Zpower_nat((Z.pred (Z.pos (P_of_succ_nat 2%nat))))( 255%nat))) in
if Z.eqb n min_int && Z.eqb divisor ((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) then word256FromInteger min_int else
if int_ltb divisor((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then
(if int_ltb n((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then
word256FromInteger ( Z.div( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) n) ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) divisor))
else
word256FromInteger ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) ( Z.div n ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) divisor)))
)
else
(if int_ltb n((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then
word256FromInteger ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) ( Z.div( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) n) divisor))
else
word256FromInteger ( Z.div n divisor))
)
| Sarith SMOD => stack_2_1_op v c
(fun (n : (Bvector 256) ) (divisor : (Bvector 256) ) => if classical_boolean_equivalence divisor(word256FromNumeral 0%nat) then(word256FromNumeral 0%nat) else
let divisor := sintFromW256 divisor in
let n := sintFromW256 n in
if int_ltb divisor((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then
(if int_ltb n((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then
word256FromInteger ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) ( Coq.ZArith.Zdiv.Zmod( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) n) ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) divisor)))
else
word256FromInteger ( Coq.ZArith.Zdiv.Zmod n ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) divisor))
)
else
(if int_ltb n((Z.pred (Z.pos (P_of_succ_nat 0%nat)))) then
word256FromInteger ( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) ( Coq.ZArith.Zdiv.Zmod( Coq.ZArith.BinInt.Z.mul((Coq.ZArith.BinInt.Z.sub Z0 ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) n) divisor))
else
word256FromInteger ( Coq.ZArith.Zdiv.Zmod n divisor))
)
| Sarith SGT => stack_2_1_op v c
(fun (elm0 : (Bvector 256) ) (elm1 : (Bvector 256) ) => if w256Greater elm0 elm1 then(word256FromNumeral 1%nat) else(word256FromNumeral 0%nat))
| Sarith SLT => stack_2_1_op v c
(fun (elm0 : (Bvector 256) ) (elm1 : (Bvector 256) ) => if w256Less elm0 elm1 then(word256FromNumeral 1%nat) else(word256FromNumeral 0%nat))
| Sarith SIGNEXTEND => stack_2_1_op v c signextend
| Arith MUL => stack_2_1_op v c
(fun (a : (Bvector 256) ) (b : (Bvector 256) ) => word256Mult a b)
| Arith DIV => stack_2_1_op v c
(fun (a : (Bvector 256) ) (divisor : (Bvector 256) ) => (if classical_boolean_equivalence divisor(word256FromNumeral 0%nat) then(word256FromNumeral 0%nat) else word256FromInteger ( Z.div(uint a) (uint divisor))))
| Arith MOD => stack_2_1_op v c
(fun (a : (Bvector 256) ) (divisor : (Bvector 256) ) => (if classical_boolean_equivalence divisor(word256FromNumeral 0%nat) then(word256FromNumeral 0%nat) else
word256FromInteger ( Coq.ZArith.Zdiv.Zmod(uint a) (uint divisor))
))
| Arith ADDMOD => stack_3_1_op v c
(fun (a : (Bvector 256) ) (b : (Bvector 256) ) (divisor : (Bvector 256) ) =>
(if classical_boolean_equivalence divisor(word256FromNumeral 0%nat) then(word256FromNumeral 0%nat) else word256FromInteger ( Coq.ZArith.Zdiv.Zmod( Coq.ZArith.BinInt.Z.add(uint a) (uint b)) (uint divisor))))
| Arith MULMOD => stack_3_1_op v c
(fun (a : (Bvector 256) ) (b : (Bvector 256) ) (divisor : (Bvector 256) ) =>
(if classical_boolean_equivalence divisor(word256FromNumeral 0%nat) then(word256FromNumeral 0%nat) else word256FromInteger ( Coq.ZArith.Zdiv.Zmod( Coq.ZArith.BinInt.Z.mul(uint a) (uint b)) (uint divisor))))
| Arith EXP => stack_2_1_op v c (fun (a : (Bvector 256) ) (exponent : (Bvector 256) ) => word256FromInteger (word_exp (uint a) (word256ToNatural exponent)))
| Arith inst_LT => stack_2_1_op v c (fun (arg0 : (Bvector 256) ) (arg1 : (Bvector 256) ) => if word256UGT arg1 arg0 then(word256FromNumeral 1%nat) else(word256FromNumeral 0%nat))
| Arith SHA3 => sha3 v c
| Info ADDRESS => stack_0_1_op v c (address_to_w256(cctx_this c))
| Info BALANCE => stack_1_1_op v c (fun (addr : (Bvector 256) ) =>(vctx_balance v) (w256_to_address addr))
| Info ORIGIN => stack_0_1_op v c (address_to_w256(vctx_origin v))
| Info CALLVALUE => stack_0_1_op v c(vctx_value_sent v)
| Info CODESIZE => stack_0_1_op v c (word256FromInteger(program_length (cctx_program c)))
| Info GASPRICE => stack_0_1_op v c(vctx_gasprice v)
| Info EXTCODESIZE => stack_1_1_op v c
(fun (arg : (Bvector 256) ) => word256FromInteger(program_length ((vctx_ext_program v) (w256_to_address arg))))
| Info BLOCKHASH => stack_1_1_op v c(block_blockhash (vctx_block v))
| Info COINBASE => stack_0_1_op v c (address_to_w256(block_coinbase (vctx_block v)))
| Info TIMESTAMP => stack_0_1_op v c(block_timestamp (vctx_block v))
| Info NUMBER => stack_0_1_op v c(block_number (vctx_block v))
| Info DIFFICULTY => stack_0_1_op v c(block_difficulty (vctx_block v))
| 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%nat) v c
| Log LOG1 => log( 1%nat) v c
| Log LOG2 => log( 2%nat) v c
| Log LOG3 => log( 3%nat) v c
| Log LOG4 => log( 4%nat) 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 ( word256Minus(gas v)(word256FromNumeral 2%nat))
| Memory MSIZE => stack_0_1_op v c ( word256Mult(word256FromNumeral 32%nat) (word256FromInteger(vctx_memory_usage v)))
end).
Definition next_state (stopper : instruction_result -> unit ) (c : constant_ctx ) (net : network ) (pr : instruction_result ) : instruction_result :=
match ( pr) with
| InstructionToEnvironment _ _ _ =>
match ( stopper pr) with tt => pr end
| InstructionContinue v =>
match ( vctx_next_instruction v c) with
| None => InstructionToEnvironment (ContractFail [ShouldNotHappen]) v None
| Some i =>
if check_resources v c(vctx_stack v) i net then
instruction_sem v c i net
else
InstructionToEnvironment (ContractFail
(match ( inst_stack_numbers i) with
| (consumed, produced) =>
(@ List.app _)(if ( int_lteb (Coq.ZArith.BinInt.Z.sub (Coq.ZArith.BinInt.Z.add((Z.pred (Z.pos (P_of_succ_nat (List.length(vctx_stack v)))))) produced) consumed)((Z.pred (Z.pos (P_of_succ_nat 1024%nat))))) then [] else [TooLongStack]) (if int_lteb (meter_gas i v c net)(vctx_gas v) then [] else [OutOfGas])
end
))
v None
end
end.
Program Fixpoint program_sem (stopper : instruction_result -> unit ) (c : constant_ctx ) (fuel : nat ) (net : network ) (pr : instruction_result ) : instruction_result :=
match ( fuel) with
| 0%nat => pr
| S (fuel_pred) => program_sem stopper c fuel_pred net (next_state stopper c net pr)
end.
Record account_state : Type := {
account_address : address ;
account_storage : storage ;
account_code : program ;
account_balance : w256 ;
account_ongoing_calls : list ((variable_ctx * Z * Z ) % type);
account_killed : bool
}.
Notation "{[ r 'with' 'account_address' := e ]}" := ({| account_address := e; account_storage := account_storage r; account_code := account_code r; account_balance := account_balance r; account_ongoing_calls := account_ongoing_calls r; account_killed := account_killed r |}).
Notation "{[ r 'with' 'account_storage' := e ]}" := ({| account_storage := e; account_address := account_address r; account_code := account_code r; account_balance := account_balance r; account_ongoing_calls := account_ongoing_calls r; account_killed := account_killed r |}).
Notation "{[ r 'with' 'account_code' := e ]}" := ({| account_code := e; account_address := account_address r; account_storage := account_storage r; account_balance := account_balance r; account_ongoing_calls := account_ongoing_calls r; account_killed := account_killed r |}).
Notation "{[ r 'with' 'account_balance' := e ]}" := ({| account_balance := e; account_address := account_address r; account_storage := account_storage r; account_code := account_code r; account_ongoing_calls := account_ongoing_calls r; account_killed := account_killed r |}).
Notation "{[ r 'with' 'account_ongoing_calls' := e ]}" := ({| account_ongoing_calls := e; account_address := account_address r; account_storage := account_storage r; account_code := account_code r; account_balance := account_balance r; account_killed := account_killed r |}).
Notation "{[ r 'with' 'account_killed' := e ]}" := ({| account_killed := e; account_address := account_address r; account_storage := account_storage r; account_code := account_code r; account_balance := account_balance r; account_ongoing_calls := account_ongoing_calls r |}).
Definition account_state_default: account_state := {| account_address := address_default; account_storage := storage_default; account_code := program_default; account_balance := w256_default; account_ongoing_calls := DAEMON; account_killed := bool_default |}.
Definition build_cctx (a : account_state ) : constant_ctx :=
{|cctx_program :=(account_code a);cctx_this :=(account_address a);cctx_hash_filter := (fun ( _ : list (byte )) => true) |}.
Definition is_call_like (i : option (inst ) ) : bool := ( (maybeEqualBy classical_boolean_equivalence i (Some (Misc CALL))) || ((maybeEqualBy classical_boolean_equivalence i (Some (Misc DELEGATECALL)))
|| ((maybeEqualBy classical_boolean_equivalence i (Some (Misc CALLCODE))) || (maybeEqualBy classical_boolean_equivalence i (Some (Misc CREATE)))))).
Definition build_vctx_failed (a : account_state ) : option (variable_ctx ) := match ((account_ongoing_calls a)) with
| [] => None
| (recovered, _, _) :: _ =>
if is_call_like ((program_content ((account_code a))) ( Coq.ZArith.BinInt.Z.sub(vctx_pc recovered)((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) then
Some ({[ recovered with vctx_stack :=(word256FromNumeral 0%nat) ::(vctx_stack recovered) ]})
else None
end.
Definition account_state_pop_ongoing_call (orig : account_state ) : account_state := match ((account_ongoing_calls orig)) with
| _ :: tl => {[ orig with account_ongoing_calls := tl ]}
| _ => {[ orig with account_ongoing_calls := [] ]}
end.
Definition empty_account (addr : word160 ) : account_state :=
{|account_address := addr;account_storage := empty_storage;account_code := empty_program;account_balance :=(word256FromNumeral 0%nat);account_ongoing_calls := [];account_killed := false
|}.
Definition update_account_state (prev : account_state ) (act : contract_action ) (v : variable_ctx ) (v_opt : option ((Z *Z ) % type) ) : account_state :=
let st := (match ( act) with ContractFail _ =>(vctx_storage_at_call v) | _ =>(vctx_storage v) end) in
let bal := (match ( act) with ContractFail _ =>(vctx_balance_at_call v) | _ =>(vctx_balance v) end) in {[ {[ {[
{[ prev with account_killed :=
(match ( act) with ContractSuicide _ => true
| _ =>(account_killed prev) end)
]} with account_ongoing_calls :=
(match ( v_opt) with None =>(account_ongoing_calls prev)
| Some (i, s) => (v, i, s) ::(account_ongoing_calls prev) end) ]} with account_balance := (match ( act) with ContractFail _ =>(account_balance prev)
| _ => bal(account_address prev) end) ]} with account_storage := st ]}.
Definition contract_behavior : Type := ( contract_action * (account_state -> bool )) % type.
Definition contract_behavior_default: contract_behavior := (contract_action_default, (fun (x107 : account_state ) => bool_default)).
Record response_to_environment : Type := {
when_called : call_env -> contract_behavior ;
when_returned : return_result -> contract_behavior ;
when_failed : contract_behavior
}.
Notation "{[ r 'with' 'when_called' := e ]}" := ({| when_called := e; when_returned := when_returned r; when_failed := when_failed r |}).
Notation "{[ r 'with' 'when_returned' := e ]}" := ({| when_returned := e; when_called := when_called r; when_failed := when_failed r |}).
Notation "{[ r 'with' 'when_failed' := e ]}" := ({| when_failed := e; when_called := when_called r; when_returned := when_returned r |}).
Definition response_to_environment_default: response_to_environment := {| when_called := (fun (x105 : call_env ) => contract_behavior_default); when_returned := (fun (x106 : return_result ) => contract_behavior_default); when_failed := contract_behavior_default |}.
Definition empty_memory : (Bvector 256) -> word8 := (fun ( _ : (Bvector 256) ) =>(word8FromNumeral 0%nat)).
Inductive build_vctx_called: (account_state) -> (call_env) -> (variable_ctx) -> Prop :=
| vctx_called: forall bal a env origin gasprice ext block gas0 existence, ( int_gteb
((two_compl_value 255(block_number block))) (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))))):Prop) -> ( classical_boolean_equivalence
( bal(account_address a))(account_balance a):Prop) -> build_vctx_called a env
{|vctx_stack := [];vctx_memory := empty_memory;vctx_memory_usage :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));vctx_storage :=(account_storage a);vctx_pc :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));vctx_balance := (fun (addr:address ) =>
if classical_boolean_equivalence addr(account_address a)
then word256Add (bal(account_address a))(callenv_value env) else bal addr);vctx_caller :=(callenv_caller env);vctx_value_sent :=(callenv_value env);vctx_data_sent :=(callenv_data env);vctx_storage_at_call :=(account_storage a);vctx_balance_at_call := bal;vctx_origin := origin;vctx_gasprice := gasprice;vctx_ext_program := ext;vctx_block := block;vctx_gas := gas0;vctx_account_existence := existence;vctx_touched_storage_index := [];vctx_refund :=((Z.pred (Z.pos (P_of_succ_nat 0%nat))));vctx_logs := []
|}.
Inductive build_vctx_returned: (account_state) -> (return_result) -> (variable_ctx) -> Prop :=
| vctx_returned: forall a_code v_pc new_bal a_bal a_addr a_storage v_stack v_memory v_memory_usage v_storage v_balance v_caller v_value v_data v_init_storage v_init_balance v_origin v_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 ((program_content a_code) ( Coq.ZArith.BinInt.Z.sub v_pc((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))):Prop) -> (word256UGE new_bal a_bal:Prop) -> build_vctx_returned
{|account_address := a_addr
;account_storage := a_storage
;account_code := a_code
;account_balance := a_bal
;account_ongoing_calls :=
(({|vctx_stack := v_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
|}
r
({|vctx_stack :=((word256FromNumeral 1%nat) :: v_stack)
;vctx_memory :=
(put_return_values v_memory(return_data r) 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 ( _ : (Bvector 256) ) => new_bal)(return_balance r))
;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
|}).
Print Assumptions instruction_sem.