| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1848 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (116 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (120 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (121 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (327 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1017 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (40 entries) |
Global Index
A
abs [projection, in EVMOpSem.Lem.lem_num]absnat [definition, in EVMOpSem.evm]
account_state_pop_ongoing_call [definition, in EVMOpSem.evm]
account_state_default [definition, in EVMOpSem.evm]
account_killed [projection, in EVMOpSem.evm]
account_ongoing_calls [projection, in EVMOpSem.evm]
account_balance [projection, in EVMOpSem.evm]
account_code [projection, in EVMOpSem.evm]
account_storage [projection, in EVMOpSem.evm]
account_address [projection, in EVMOpSem.evm]
account_state [record, in EVMOpSem.evm]
ADD [constructor, in EVMOpSem.evm]
ADDMOD [constructor, in EVMOpSem.evm]
ADDRESS [constructor, in EVMOpSem.evm]
address [definition, in EVMOpSem.evm]
address_to_w256 [definition, in EVMOpSem.evm]
address_default [definition, in EVMOpSem.evm]
add_balance [definition, in EVMOpSem.block]
allDistinct [definition, in EVMOpSem.Lem.lem_list]
Arith [constructor, in EVMOpSem.evm]
arithmetic_right_shift [projection, in EVMOpSem.Lem.lem_word]
arith_inst_numbers [definition, in EVMOpSem.evm]
arith_inst_code [definition, in EVMOpSem.evm]
arith_inst_default [definition, in EVMOpSem.evm]
arith_inst_sind [definition, in EVMOpSem.evm]
arith_inst_rec [definition, in EVMOpSem.evm]
arith_inst_ind [definition, in EVMOpSem.evm]
arith_inst_rect [definition, in EVMOpSem.evm]
arith_inst [inductive, in EVMOpSem.evm]
at_least_eip150 [definition, in EVMOpSem.evm]
B
BALANCE [constructor, in EVMOpSem.evm]BD [definition, in EVMOpSem.rlplem]
BD_rev [definition, in EVMOpSem.rlplem]
BE [definition, in EVMOpSem.rlplem]
before_homestead [definition, in EVMOpSem.evm]
beq_nat [definition, in EVMOpSem.Lem.lem_num]
BE_nat [definition, in EVMOpSem.rlplem]
BE_rev_prim [definition, in EVMOpSem.rlplem]
big [definition, in EVMOpSem.keccak]
bigintersection [definition, in EVMOpSem.Lem.lem_set]
bigunion [definition, in EVMOpSem.Lem.lem_set]
binary_to_Z_to_binary [lemma, in EVMOpSem.Zdigits]
binary_value_pos [lemma, in EVMOpSem.Zdigits]
binary_value_Sn [lemma, in EVMOpSem.Zdigits]
binary_value [lemma, in EVMOpSem.Zdigits]
bind [definition, in EVMOpSem.Lem.lem_maybe]
Bits [constructor, in EVMOpSem.evm]
BitSeq [constructor, in EVMOpSem.Lem.lem_word]
bitSeqAdd [definition, in EVMOpSem.Lem.lem_word]
bitSeqAnd [definition, in EVMOpSem.Lem.lem_word]
bitSeqArithBinOp [definition, in EVMOpSem.Lem.lem_word]
bitSeqArithBinTest [definition, in EVMOpSem.Lem.lem_word]
bitSeqArithmeticShiftRight [definition, in EVMOpSem.Lem.lem_word]
bitSeqArithUnaryOp [definition, in EVMOpSem.Lem.lem_word]
bitSeqBinop [definition, in EVMOpSem.Lem.lem_word]
bitSeqBinopAux [definition, in EVMOpSem.Lem.coqharness]
bitSeqCompare [definition, in EVMOpSem.Lem.lem_word]
bitSeqDiv [definition, in EVMOpSem.Lem.lem_word]
bitSeqFromBoolList [definition, in EVMOpSem.Lem.lem_word]
bitSeqFromInt [definition, in EVMOpSem.Lem.lem_word]
bitSeqFromInteger [definition, in EVMOpSem.Lem.lem_word]
bitSeqFromNat [definition, in EVMOpSem.Lem.lem_word]
bitSeqFromNatural [definition, in EVMOpSem.Lem.lem_word]
bitSeqGreater [definition, in EVMOpSem.Lem.lem_word]
bitSeqGreaterEqual [definition, in EVMOpSem.Lem.lem_word]
bitSeqLess [definition, in EVMOpSem.Lem.lem_word]
bitSeqLessEqual [definition, in EVMOpSem.Lem.lem_word]
bitSeqLogicalShiftRight [definition, in EVMOpSem.Lem.lem_word]
bitSeqMax [definition, in EVMOpSem.Lem.lem_word]
bitSeqMin [definition, in EVMOpSem.Lem.lem_word]
bitSeqMinus [definition, in EVMOpSem.Lem.lem_word]
bitSeqMod [definition, in EVMOpSem.Lem.lem_word]
bitSeqMult [definition, in EVMOpSem.Lem.lem_word]
bitSeqNegate [definition, in EVMOpSem.Lem.lem_word]
bitSeqNot [definition, in EVMOpSem.Lem.lem_word]
bitSeqOr [definition, in EVMOpSem.Lem.lem_word]
bitSeqPow [definition, in EVMOpSem.Lem.lem_word]
bitSeqPred [definition, in EVMOpSem.Lem.lem_word]
bitSeqSetBit [definition, in EVMOpSem.Lem.lem_word]
bitSeqShiftLeft [definition, in EVMOpSem.Lem.lem_word]
bitSeqSucc [definition, in EVMOpSem.Lem.lem_word]
bitSeqTestBit [definition, in EVMOpSem.Lem.lem_word]
bitSequence [inductive, in EVMOpSem.Lem.lem_word]
bitSequence_default [definition, in EVMOpSem.Lem.lem_word]
bitSequence_sind [definition, in EVMOpSem.Lem.lem_word]
bitSequence_rec [definition, in EVMOpSem.Lem.lem_word]
bitSequence_ind [definition, in EVMOpSem.Lem.lem_word]
bitSequence_rect [definition, in EVMOpSem.Lem.lem_word]
bitSeqXor [definition, in EVMOpSem.Lem.lem_word]
bits_stack_nums [definition, in EVMOpSem.evm]
bits_inst_code [definition, in EVMOpSem.evm]
bits_inst_default [definition, in EVMOpSem.evm]
bits_inst_sind [definition, in EVMOpSem.evm]
bits_inst_rec [definition, in EVMOpSem.evm]
bits_inst_ind [definition, in EVMOpSem.evm]
bits_inst_rect [definition, in EVMOpSem.evm]
bits_inst [inductive, in EVMOpSem.evm]
bit_value [definition, in EVMOpSem.Zdigits]
block [library]
blockedInstructionContinue [definition, in EVMOpSem.evm]
blocked_jump [definition, in EVMOpSem.evm]
BLOCKHASH [constructor, in EVMOpSem.evm]
block_info_default [definition, in EVMOpSem.evm]
block_gaslimit [projection, in EVMOpSem.evm]
block_difficulty [projection, in EVMOpSem.evm]
block_number [projection, in EVMOpSem.evm]
block_timestamp [projection, in EVMOpSem.evm]
block_coinbase [projection, in EVMOpSem.evm]
block_blockhash [projection, in EVMOpSem.evm]
block_info [record, in EVMOpSem.evm]
block_account_default [definition, in EVMOpSem.block]
block_account_hascode [projection, in EVMOpSem.block]
block_account_exists [projection, in EVMOpSem.block]
block_account_nonce [projection, in EVMOpSem.block]
block_account_balance [projection, in EVMOpSem.block]
block_account_code [projection, in EVMOpSem.block]
block_account_storage [projection, in EVMOpSem.block]
block_account_address [projection, in EVMOpSem.block]
block_account [record, in EVMOpSem.block]
block_auxiliary [library]
boolCompare [definition, in EVMOpSem.Lem.lem_basic_classes]
boolListFrombitSeq [definition, in EVMOpSem.Lem.lem_word]
boolListFrombitSeqAux [definition, in EVMOpSem.Lem.lem_word]
boolListFromInteger [definition, in EVMOpSem.Lem.lem_word]
boolListFromNatural [definition, in EVMOpSem.Lem.coqharness]
boolListFromWord160 [definition, in EVMOpSem.word160]
boolListFromWord256 [definition, in EVMOpSem.word256]
boolListFromWord32 [definition, in EVMOpSem.word32]
boolListFromWord4 [definition, in EVMOpSem.word4]
boolListFromWord64 [definition, in EVMOpSem.word64]
boolListFromWord8 [definition, in EVMOpSem.word8]
bool_default [definition, in EVMOpSem.Lem.coqharness]
bool_of_Prop [definition, in EVMOpSem.Lem.coqharness]
bs_to_w160 [definition, in EVMOpSem.word160]
bs_to_w8 [definition, in EVMOpSem.word8]
bs_to_w4 [definition, in EVMOpSem.word4]
bs_to_w64 [definition, in EVMOpSem.word64]
bs_to_w32 [definition, in EVMOpSem.word32]
build_vctx_returned_sind [definition, in EVMOpSem.evm]
build_vctx_returned_ind [definition, in EVMOpSem.evm]
build_vctx_returned [inductive, in EVMOpSem.evm]
build_vctx_called_sind [definition, in EVMOpSem.evm]
build_vctx_called_ind [definition, in EVMOpSem.evm]
build_vctx_called [inductive, in EVMOpSem.evm]
build_vctx_failed [definition, in EVMOpSem.evm]
build_cctx [definition, in EVMOpSem.evm]
build_cctx0 [definition, in EVMOpSem.block]
byte [definition, in EVMOpSem.keccak]
BYTE [constructor, in EVMOpSem.evm]
byteFromNat [definition, in EVMOpSem.evm]
bytelist_to_instlist [definition, in EVMOpSem.block]
byte_default [definition, in EVMOpSem.keccak]
byte_list_fill_right [definition, in EVMOpSem.evm]
byte_to_w256 [definition, in EVMOpSem.evm]
byte_to_inst [definition, in EVMOpSem.block]
byte0 [definition, in EVMOpSem.rlplem]
byte0_default [definition, in EVMOpSem.rlplem]
C
C [definition, in EVMOpSem.evm]calc_memu_extra2 [definition, in EVMOpSem.evm]
calc_memu_extra [definition, in EVMOpSem.evm]
calc_igas [definition, in EVMOpSem.block]
calc_address [definition, in EVMOpSem.block]
call [definition, in EVMOpSem.evm]
CALL [constructor, in EVMOpSem.evm]
callarg_output_size [projection, in EVMOpSem.evm]
callarg_output_begin [projection, in EVMOpSem.evm]
callarg_data [projection, in EVMOpSem.evm]
callarg_value [projection, in EVMOpSem.evm]
callarg_recipient [projection, in EVMOpSem.evm]
callarg_code [projection, in EVMOpSem.evm]
callarg_gas [projection, in EVMOpSem.evm]
callcode [definition, in EVMOpSem.evm]
CALLCODE [constructor, in EVMOpSem.evm]
calldatacopy [definition, in EVMOpSem.evm]
CALLDATACOPY [constructor, in EVMOpSem.evm]
CALLDATALOAD [constructor, in EVMOpSem.evm]
CALLDATASIZE [constructor, in EVMOpSem.evm]
callenv_balance [projection, in EVMOpSem.evm]
callenv_blocknum [projection, in EVMOpSem.evm]
callenv_timestamp [projection, in EVMOpSem.evm]
callenv_caller [projection, in EVMOpSem.evm]
callenv_data [projection, in EVMOpSem.evm]
callenv_value [projection, in EVMOpSem.evm]
callenv_gaslimit [projection, in EVMOpSem.evm]
CALLER [constructor, in EVMOpSem.evm]
CALLVALUE [constructor, in EVMOpSem.evm]
call_arguments_default [definition, in EVMOpSem.evm]
call_arguments [record, in EVMOpSem.evm]
call_env_default [definition, in EVMOpSem.evm]
call_env [record, in EVMOpSem.evm]
catMaybes [definition, in EVMOpSem.Lem.lem_list]
Ccall [definition, in EVMOpSem.evm]
Ccallgas [definition, in EVMOpSem.evm]
cctx_hash_filter [projection, in EVMOpSem.evm]
cctx_this [projection, in EVMOpSem.evm]
cctx_program [projection, in EVMOpSem.evm]
Cextra [definition, in EVMOpSem.evm]
Cgascap [definition, in EVMOpSem.evm]
char_equal [definition, in EVMOpSem.Lem.coqharness]
check_resources [definition, in EVMOpSem.evm]
check_refund [definition, in EVMOpSem.evm]
chi [definition, in EVMOpSem.keccak]
chi_for_j [definition, in EVMOpSem.keccak]
classical_boolean_equivalence [definition, in EVMOpSem.Lem.coqharness]
cleanBitSeq [definition, in EVMOpSem.Lem.lem_word]
Cmem [definition, in EVMOpSem.evm]
Cnew [definition, in EVMOpSem.evm]
codecopy [definition, in EVMOpSem.evm]
CODECOPY [constructor, in EVMOpSem.evm]
codemap [definition, in EVMOpSem.block]
CODESIZE [constructor, in EVMOpSem.evm]
COHERENT_VALUE [section, in EVMOpSem.Zdigits]
COINBASE [constructor, in EVMOpSem.evm]
compare [projection, in EVMOpSem.Lem.lem_basic_classes]
concat [definition, in EVMOpSem.Lem.lem_list]
concat0 [definition, in EVMOpSem.Lem.lem_string]
conjunction [projection, in EVMOpSem.Lem.lem_word]
constant_mark [definition, in EVMOpSem.evm]
constant_ctx_default [definition, in EVMOpSem.evm]
constant_ctx [record, in EVMOpSem.evm]
Continue [constructor, in EVMOpSem.block]
ContractCall [constructor, in EVMOpSem.evm]
ContractCreate [constructor, in EVMOpSem.evm]
ContractDelegateCall [constructor, in EVMOpSem.evm]
ContractFail [constructor, in EVMOpSem.evm]
ContractReturn [constructor, in EVMOpSem.evm]
ContractSuicide [constructor, in EVMOpSem.evm]
contract_behavior_default [definition, in EVMOpSem.evm]
contract_behavior [definition, in EVMOpSem.evm]
contract_action_default [definition, in EVMOpSem.evm]
contract_action_sind [definition, in EVMOpSem.evm]
contract_action_rec [definition, in EVMOpSem.evm]
contract_action_ind [definition, in EVMOpSem.evm]
contract_action_rect [definition, in EVMOpSem.evm]
contract_action [inductive, in EVMOpSem.evm]
coqharness [library]
count_map [definition, in EVMOpSem.Lem.lem_list]
create [definition, in EVMOpSem.evm]
CREATE [constructor, in EVMOpSem.evm]
CreateAddress [constructor, in EVMOpSem.block]
createarg_code [projection, in EVMOpSem.evm]
createarg_value [projection, in EVMOpSem.evm]
create_log_entry [definition, in EVMOpSem.evm]
create_arguments_default [definition, in EVMOpSem.evm]
create_arguments [record, in EVMOpSem.evm]
create_account [definition, in EVMOpSem.block]
create_env [definition, in EVMOpSem.block]
cross [definition, in EVMOpSem.Lem.lem_set]
Csstore [definition, in EVMOpSem.evm]
Csuicide [definition, in EVMOpSem.evm]
curry [definition, in EVMOpSem.Lem.lem_function]
cut_natural_map [definition, in EVMOpSem.evm]
cut_data [definition, in EVMOpSem.evm]
cut_memory [definition, in EVMOpSem.evm]
cut_memory_aux_alt [definition, in EVMOpSem.evm]
cut_memory_aux [definition, in EVMOpSem.evm]
Cxfer [definition, in EVMOpSem.evm]
D
DAEMON [axiom, in EVMOpSem.Lem.coqharness]datasize [definition, in EVMOpSem.evm]
defaultAsr [definition, in EVMOpSem.Lem.lem_word]
defaultLand [definition, in EVMOpSem.Lem.lem_word]
defaultLnot [definition, in EVMOpSem.Lem.lem_word]
defaultLor [definition, in EVMOpSem.Lem.lem_word]
defaultLsl [definition, in EVMOpSem.Lem.lem_word]
defaultLsr [definition, in EVMOpSem.Lem.lem_word]
defaultLxor [definition, in EVMOpSem.Lem.lem_word]
delegatecall [definition, in EVMOpSem.evm]
DELEGATECALL [constructor, in EVMOpSem.evm]
deleteBy [definition, in EVMOpSem.Lem.lem_list]
deleteFirst [definition, in EVMOpSem.Lem.lem_list]
deletes [definition, in EVMOpSem.Lem.lem_list]
dest_init [definition, in EVMOpSem.Lem.lem_list]
dest_init_aux [definition, in EVMOpSem.Lem.lem_list]
de_r_b [definition, in EVMOpSem.rlplem]
DIFFICULTY [constructor, in EVMOpSem.evm]
DIV [constructor, in EVMOpSem.evm]
drop [definition, in EVMOpSem.Lem.lem_list]
dropWhile [definition, in EVMOpSem.Lem.lem_list]
Dup [constructor, in EVMOpSem.evm]
dup_inst_numbers [definition, in EVMOpSem.evm]
dup_inst_code [definition, in EVMOpSem.evm]
dup_inst_default [definition, in EVMOpSem.evm]
dup_inst [definition, in EVMOpSem.evm]
E
EIP150 [constructor, in EVMOpSem.evm]EIP158 [constructor, in EVMOpSem.evm]
either [definition, in EVMOpSem.Lem.lem_either]
eitherEqual [definition, in EVMOpSem.Lem.lem_either]
eitherEqualBy [definition, in EVMOpSem.Lem.lem_either]
either_setElemCompare [definition, in EVMOpSem.Lem.lem_either]
elem [definition, in EVMOpSem.Lem.lem_list]
elemBy [definition, in EVMOpSem.Lem.lem_list]
empty_memory [definition, in EVMOpSem.evm]
empty_account [definition, in EVMOpSem.evm]
empty_program [definition, in EVMOpSem.evm]
empty_storage [definition, in EVMOpSem.evm]
empty_state [definition, in EVMOpSem.block]
empty_account0 [definition, in EVMOpSem.block]
ENCODING_VALUE [section, in EVMOpSem.Zdigits]
end_transaction [definition, in EVMOpSem.block]
EnvironmentCall [constructor, in EVMOpSem.evm]
EnvironmentFail [constructor, in EVMOpSem.evm]
EnvironmentRet [constructor, in EVMOpSem.evm]
environment_action_default [definition, in EVMOpSem.evm]
environment_action_sind [definition, in EVMOpSem.evm]
environment_action_rec [definition, in EVMOpSem.evm]
environment_action_ind [definition, in EVMOpSem.evm]
environment_action_rect [definition, in EVMOpSem.evm]
environment_action [inductive, in EVMOpSem.evm]
Eq [record, in EVMOpSem.Lem.lem_basic_classes]
EQ [constructor, in EVMOpSem.Lem.coqharness]
evm [library]
evm_auxiliary [library]
exclusive_or [projection, in EVMOpSem.Lem.lem_word]
EXP [constructor, in EVMOpSem.evm]
extcodecopy [definition, in EVMOpSem.evm]
EXTCODECOPY [constructor, in EVMOpSem.evm]
EXTCODESIZE [constructor, in EVMOpSem.evm]
F
failure_reason_default [definition, in EVMOpSem.evm]failure_reason_sind [definition, in EVMOpSem.evm]
failure_reason_rec [definition, in EVMOpSem.evm]
failure_reason_ind [definition, in EVMOpSem.evm]
failure_reason_rect [definition, in EVMOpSem.evm]
failure_reason [inductive, in EVMOpSem.evm]
false_eq_true_P [lemma, in EVMOpSem.Lem.coqharness]
false_eq_true_False [lemma, in EVMOpSem.Lem.coqharness]
filter [definition, in EVMOpSem.Lem.lem_set]
filterI [definition, in EVMOpSem.keccak]
find [definition, in EVMOpSem.Lem.lem_list]
findIndex [definition, in EVMOpSem.Lem.lem_list]
findIndices [definition, in EVMOpSem.Lem.lem_list]
findIndices_aux [definition, in EVMOpSem.Lem.lem_list]
Finished [constructor, in EVMOpSem.block]
fix_push [definition, in EVMOpSem.block]
fmap [definition, in EVMOpSem.Lem.coqharness]
fmap_default [definition, in EVMOpSem.Lem.coqharness]
fmap_range_by [definition, in EVMOpSem.Lem.coqharness]
fmap_domain_by [definition, in EVMOpSem.Lem.coqharness]
fmap_map [definition, in EVMOpSem.Lem.coqharness]
fmap_delete_by [definition, in EVMOpSem.Lem.coqharness]
fmap_all [definition, in EVMOpSem.Lem.coqharness]
fmap_lookup_by [definition, in EVMOpSem.Lem.coqharness]
fmap_is_empty [definition, in EVMOpSem.Lem.coqharness]
fmap_add [definition, in EVMOpSem.Lem.coqharness]
fmap_empty [definition, in EVMOpSem.Lem.coqharness]
fmap_equal_by [definition, in EVMOpSem.Lem.coqharness]
for_inner [definition, in EVMOpSem.keccak]
fromList [definition, in EVMOpSem.Lem.lem_map]
fromMaybe [definition, in EVMOpSem.Lem.lem_maybe]
Frontier [constructor, in EVMOpSem.evm]
f_logs [projection, in EVMOpSem.block]
f_refund [projection, in EVMOpSem.block]
f_gas [projection, in EVMOpSem.block]
f_killed [projection, in EVMOpSem.block]
f_state [projection, in EVMOpSem.block]
G
gas [definition, in EVMOpSem.evm]GAS [constructor, in EVMOpSem.evm]
GASLIMIT [constructor, in EVMOpSem.evm]
GASPRICE [constructor, in EVMOpSem.evm]
Gbalance [definition, in EVMOpSem.evm]
Gbase [definition, in EVMOpSem.evm]
Gblockhash [definition, in EVMOpSem.evm]
Gcall [definition, in EVMOpSem.evm]
Gcallstipend [definition, in EVMOpSem.evm]
Gcallvalue [definition, in EVMOpSem.evm]
Gcodedeposit [definition, in EVMOpSem.evm]
Gcopy [definition, in EVMOpSem.evm]
Gcreate [definition, in EVMOpSem.evm]
general_dup [definition, in EVMOpSem.evm]
genericCompare [definition, in EVMOpSem.Lem.lem_basic_classes]
genlist [definition, in EVMOpSem.Lem.lem_list]
gen_pow_aux [definition, in EVMOpSem.Lem.coqharness]
gen_pow [definition, in EVMOpSem.Lem.lem_num]
get [definition, in EVMOpSem.keccak]
get_n [definition, in EVMOpSem.keccak]
get_byte [definition, in EVMOpSem.evm]
get_opt [definition, in EVMOpSem.block]
get_hint [definition, in EVMOpSem.block]
Gexp [definition, in EVMOpSem.evm]
Gexpbyte [definition, in EVMOpSem.evm]
Gextcode [definition, in EVMOpSem.evm]
Ghigh [definition, in EVMOpSem.evm]
Gjumpdest [definition, in EVMOpSem.evm]
global [record, in EVMOpSem.block]
global_state_default [definition, in EVMOpSem.block]
global_state_sind [definition, in EVMOpSem.block]
global_state_rec [definition, in EVMOpSem.block]
global_state_ind [definition, in EVMOpSem.block]
global_state_rect [definition, in EVMOpSem.block]
global_state [inductive, in EVMOpSem.block]
global_default [definition, in EVMOpSem.block]
Glog [definition, in EVMOpSem.evm]
Glogdata [definition, in EVMOpSem.evm]
Glogtopic [definition, in EVMOpSem.evm]
Glow [definition, in EVMOpSem.evm]
Gmemory [definition, in EVMOpSem.evm]
Gmid [definition, in EVMOpSem.evm]
Gnewaccount [definition, in EVMOpSem.evm]
Gsha3 [definition, in EVMOpSem.evm]
Gsha3word [definition, in EVMOpSem.evm]
Gsload [definition, in EVMOpSem.evm]
Gsreset [definition, in EVMOpSem.evm]
Gsset [definition, in EVMOpSem.evm]
Gsuicide [definition, in EVMOpSem.evm]
GT [constructor, in EVMOpSem.Lem.coqharness]
Gtransaction [definition, in EVMOpSem.evm]
Gtxcreate [definition, in EVMOpSem.evm]
Gtxdatanonzero [definition, in EVMOpSem.evm]
Gtxdatazero [definition, in EVMOpSem.evm]
Gverylow [definition, in EVMOpSem.evm]
Gzero [definition, in EVMOpSem.evm]
g_create [projection, in EVMOpSem.block]
g_vmstate [projection, in EVMOpSem.block]
g_killed [projection, in EVMOpSem.block]
g_cctx [projection, in EVMOpSem.block]
g_current [projection, in EVMOpSem.block]
g_stack [projection, in EVMOpSem.block]
g_orig [projection, in EVMOpSem.block]
H
helper [library]Homestead [constructor, in EVMOpSem.evm]
homestead_block [definition, in EVMOpSem.evm]
I
inclusive_or [projection, in EVMOpSem.Lem.lem_word]index [definition, in EVMOpSem.Lem.lem_list]
Info [constructor, in EVMOpSem.evm]
info_inst_numbers [definition, in EVMOpSem.evm]
info_inst_code [definition, in EVMOpSem.evm]
info_inst_default [definition, in EVMOpSem.evm]
info_inst_sind [definition, in EVMOpSem.evm]
info_inst_rec [definition, in EVMOpSem.evm]
info_inst_ind [definition, in EVMOpSem.evm]
info_inst_rect [definition, in EVMOpSem.evm]
info_inst [inductive, in EVMOpSem.evm]
initial_pos [definition, in EVMOpSem.keccak]
initial_st [definition, in EVMOpSem.keccak]
input_as_natural_map [definition, in EVMOpSem.evm]
insertBy [definition, in EVMOpSem.Lem.lem_sorting]
insertSortBy [definition, in EVMOpSem.Lem.lem_sorting]
inst [inductive, in EVMOpSem.evm]
InstructionContinue [constructor, in EVMOpSem.evm]
InstructionToEnvironment [constructor, in EVMOpSem.evm]
instruction_sem [definition, in EVMOpSem.evm]
instruction_return_result [definition, in EVMOpSem.evm]
instruction_failure_result [definition, in EVMOpSem.evm]
instruction_result_default [definition, in EVMOpSem.evm]
instruction_result_sind [definition, in EVMOpSem.evm]
instruction_result_rec [definition, in EVMOpSem.evm]
instruction_result_ind [definition, in EVMOpSem.evm]
instruction_result_rect [definition, in EVMOpSem.evm]
instruction_result [inductive, in EVMOpSem.evm]
inst_size [definition, in EVMOpSem.evm]
inst_stack_numbers [definition, in EVMOpSem.evm]
inst_code [definition, in EVMOpSem.evm]
inst_default [definition, in EVMOpSem.evm]
inst_sind [definition, in EVMOpSem.evm]
inst_rec [definition, in EVMOpSem.evm]
inst_ind [definition, in EVMOpSem.evm]
inst_rect [definition, in EVMOpSem.evm]
inst_LT [constructor, in EVMOpSem.evm]
inst_EQ [constructor, in EVMOpSem.evm]
inst_GT [constructor, in EVMOpSem.evm]
inst_NOT [constructor, in EVMOpSem.evm]
inst_XOR [constructor, in EVMOpSem.evm]
inst_OR [constructor, in EVMOpSem.evm]
inst_AND [constructor, in EVMOpSem.evm]
inst_to_byte [definition, in EVMOpSem.block]
intAsr [definition, in EVMOpSem.Lem.lem_word]
integerAsr [definition, in EVMOpSem.Lem.lem_word]
integerFromBitSeq [definition, in EVMOpSem.Lem.lem_word]
integerFromBoolList [definition, in EVMOpSem.Lem.lem_word]
integerFromBoolListAux [definition, in EVMOpSem.Lem.lem_word]
integerLand [definition, in EVMOpSem.Lem.lem_word]
integerLnot [definition, in EVMOpSem.Lem.lem_word]
integerLor [definition, in EVMOpSem.Lem.lem_word]
integerLsl [definition, in EVMOpSem.Lem.lem_word]
integerLxor [definition, in EVMOpSem.Lem.lem_word]
intFromBitSeq [definition, in EVMOpSem.Lem.lem_word]
intLand [definition, in EVMOpSem.Lem.lem_word]
intLnot [definition, in EVMOpSem.Lem.lem_word]
intLor [definition, in EVMOpSem.Lem.lem_word]
intLsl [definition, in EVMOpSem.Lem.lem_word]
intLxor [definition, in EVMOpSem.Lem.lem_word]
int_gteb [definition, in EVMOpSem.Lem.coqharness]
int_lteb [definition, in EVMOpSem.Lem.coqharness]
int_gtb [definition, in EVMOpSem.Lem.coqharness]
int_ltb [definition, in EVMOpSem.Lem.coqharness]
int32Abs [definition, in EVMOpSem.Lem.lem_num]
int32FromInt [definition, in EVMOpSem.Lem.lem_num]
int32FromInteger [definition, in EVMOpSem.Lem.lem_num]
int32FromInt64 [definition, in EVMOpSem.Lem.lem_num]
int64Abs [definition, in EVMOpSem.Lem.lem_num]
int64FromInt [definition, in EVMOpSem.Lem.lem_num]
int64FromInteger [definition, in EVMOpSem.Lem.lem_num]
int64FromInt32 [definition, in EVMOpSem.Lem.lem_num]
InvalidJumpDestination [constructor, in EVMOpSem.evm]
invert_endian [definition, in EVMOpSem.keccak]
iota [definition, in EVMOpSem.keccak]
iota0 [definition, in EVMOpSem.evm]
isAntisymmetric [definition, in EVMOpSem.Lem.lem_relation]
isAntisymmetricOn [definition, in EVMOpSem.Lem.lem_relation]
isEqual [projection, in EVMOpSem.Lem.lem_basic_classes]
isEquivalenceOn [definition, in EVMOpSem.Lem.lem_relation]
isGreater [projection, in EVMOpSem.Lem.lem_basic_classes]
isGreaterEqual [projection, in EVMOpSem.Lem.lem_basic_classes]
isInequal [projection, in EVMOpSem.Lem.lem_basic_classes]
isIrreflexive [definition, in EVMOpSem.Lem.lem_relation]
isIrreflexiveOn [definition, in EVMOpSem.Lem.lem_relation]
isJust [definition, in EVMOpSem.Lem.lem_maybe]
isLess [projection, in EVMOpSem.Lem.lem_basic_classes]
isLessEqual [projection, in EVMOpSem.Lem.lem_basic_classes]
isNothing [definition, in EVMOpSem.Lem.lem_maybe]
isPartialOrderOn [definition, in EVMOpSem.Lem.lem_relation]
isPermutationBy [definition, in EVMOpSem.Lem.lem_sorting]
isPrefixOf [definition, in EVMOpSem.Lem.lem_list]
isPreorderOn [definition, in EVMOpSem.Lem.lem_relation]
isReflexiveOn [definition, in EVMOpSem.Lem.lem_relation]
isSingleValued [definition, in EVMOpSem.Lem.lem_relation]
isSortedBy [definition, in EVMOpSem.Lem.lem_sorting]
isStrictPartialOrder [definition, in EVMOpSem.Lem.lem_relation]
isStrictPartialOrderOn [definition, in EVMOpSem.Lem.lem_relation]
isStrictTotalOrderOn [definition, in EVMOpSem.Lem.lem_relation]
isSymmetric [definition, in EVMOpSem.Lem.lem_relation]
isSymmetricOn [definition, in EVMOpSem.Lem.lem_relation]
isTotalOn [definition, in EVMOpSem.Lem.lem_relation]
isTotalOrderOn [definition, in EVMOpSem.Lem.lem_relation]
isTransitive [definition, in EVMOpSem.Lem.lem_relation]
isTransitiveOn [definition, in EVMOpSem.Lem.lem_relation]
isTrichotomousOn [definition, in EVMOpSem.Lem.lem_relation]
ISZERO [constructor, in EVMOpSem.evm]
is_call_like [definition, in EVMOpSem.evm]
J
jump [definition, in EVMOpSem.evm]JUMP [constructor, in EVMOpSem.evm]
JUMPDEST [constructor, in EVMOpSem.evm]
jumpi [definition, in EVMOpSem.evm]
JUMPI [constructor, in EVMOpSem.evm]
K
keccak [definition, in EVMOpSem.keccak]keccak [library]
keccakf [definition, in EVMOpSem.keccak]
keccakf_rounds [definition, in EVMOpSem.keccak]
keccakf_piln [definition, in EVMOpSem.keccak]
keccakf_rotc [definition, in EVMOpSem.keccak]
keccakf_randc [definition, in EVMOpSem.keccak]
keccak_final [definition, in EVMOpSem.keccak]
keccak_auxiliary [library]
keccak' [definition, in EVMOpSem.keccak]
kill_accounts [definition, in EVMOpSem.block]
L
L [definition, in EVMOpSem.evm]Leaf [constructor, in EVMOpSem.rlplem]
leastFixedPoint [definition, in EVMOpSem.Lem.lem_set]
left_shift [projection, in EVMOpSem.Lem.lem_word]
lem_word [library]
lem_sorting [library]
lem_basic_classes [library]
lem_show [library]
lem_tuple [library]
lem_bool [library]
lem_string [library]
lem_relation [library]
lem_map [library]
lem_num [library]
lem_set_helpers [library]
lem_maybe [library]
lem_set [library]
lem_function [library]
lem_list [library]
lem_pervasives [library]
lem_either [library]
lexicographicCompareBy [definition, in EVMOpSem.Lem.lem_list]
lexicographicLessBy [definition, in EVMOpSem.Lem.lem_list]
lexicographicLessEqBy [definition, in EVMOpSem.Lem.lem_list]
list_fill_left [definition, in EVMOpSem.keccak]
list_fill_right [definition, in EVMOpSem.keccak]
list_swap [definition, in EVMOpSem.evm]
list_default [definition, in EVMOpSem.Lem.coqharness]
list_tail [definition, in EVMOpSem.Lem.coqharness]
list_head [definition, in EVMOpSem.Lem.coqharness]
list_member_by [definition, in EVMOpSem.Lem.coqharness]
list_equal_by [definition, in EVMOpSem.Lem.coqharness]
lnot [projection, in EVMOpSem.Lem.lem_word]
log [definition, in EVMOpSem.evm]
Log [constructor, in EVMOpSem.evm]
logicial_right_shift [projection, in EVMOpSem.Lem.lem_word]
log_entry_default [definition, in EVMOpSem.evm]
log_data [projection, in EVMOpSem.evm]
log_topics [projection, in EVMOpSem.evm]
log_addr [projection, in EVMOpSem.evm]
log_entry [record, in EVMOpSem.evm]
log_inst_numbers [definition, in EVMOpSem.evm]
log_inst_code [definition, in EVMOpSem.evm]
log_inst_default [definition, in EVMOpSem.evm]
log_inst_sind [definition, in EVMOpSem.evm]
log_inst_rec [definition, in EVMOpSem.evm]
log_inst_ind [definition, in EVMOpSem.evm]
log_inst_rect [definition, in EVMOpSem.evm]
log_inst [inductive, in EVMOpSem.evm]
LOG0 [constructor, in EVMOpSem.evm]
LOG1 [constructor, in EVMOpSem.evm]
LOG2 [constructor, in EVMOpSem.evm]
log256floor [definition, in EVMOpSem.evm]
LOG3 [constructor, in EVMOpSem.evm]
LOG4 [constructor, in EVMOpSem.evm]
lookupBy [definition, in EVMOpSem.Lem.lem_list]
LT [constructor, in EVMOpSem.Lem.coqharness]
M
M [definition, in EVMOpSem.evm]make_program [definition, in EVMOpSem.block]
make_opt [definition, in EVMOpSem.block]
map [definition, in EVMOpSem.Lem.lem_set]
mapi [definition, in EVMOpSem.Lem.lem_list]
mapiAux [definition, in EVMOpSem.Lem.lem_list]
mapKeyCompare [projection, in EVMOpSem.Lem.lem_map]
MapKeyType [record, in EVMOpSem.Lem.lem_map]
mapMaybe [definition, in EVMOpSem.Lem.lem_list]
map_setElemCompare [definition, in EVMOpSem.Lem.lem_map]
map_tr [definition, in EVMOpSem.Lem.lem_list]
max [projection, in EVMOpSem.Lem.lem_basic_classes]
maxByLessEqual [definition, in EVMOpSem.Lem.lem_basic_classes]
maybe [definition, in EVMOpSem.Lem.lem_maybe]
maybeCompare [definition, in EVMOpSem.Lem.lem_maybe]
maybeEqualBy [definition, in EVMOpSem.Lem.lem_maybe]
maybe_to_list [definition, in EVMOpSem.evm]
maybe_default [definition, in EVMOpSem.Lem.coqharness]
mdlen [definition, in EVMOpSem.keccak]
Memory [constructor, in EVMOpSem.evm]
memory [definition, in EVMOpSem.evm]
memory_inst_numbers [definition, in EVMOpSem.evm]
memory_inst_code [definition, in EVMOpSem.evm]
memory_inst_default [definition, in EVMOpSem.evm]
memory_inst_sind [definition, in EVMOpSem.evm]
memory_inst_rec [definition, in EVMOpSem.evm]
memory_inst_ind [definition, in EVMOpSem.evm]
memory_inst_rect [definition, in EVMOpSem.evm]
memory_inst [inductive, in EVMOpSem.evm]
memory_default [definition, in EVMOpSem.evm]
meter_gas [definition, in EVMOpSem.evm]
Metropolis [constructor, in EVMOpSem.evm]
min [projection, in EVMOpSem.Lem.lem_basic_classes]
minByLessEqual [definition, in EVMOpSem.Lem.lem_basic_classes]
Misc [constructor, in EVMOpSem.evm]
misc_inst_numbers [definition, in EVMOpSem.evm]
misc_inst_code [definition, in EVMOpSem.evm]
misc_inst_default [definition, in EVMOpSem.evm]
misc_inst_sind [definition, in EVMOpSem.evm]
misc_inst_rec [definition, in EVMOpSem.evm]
misc_inst_ind [definition, in EVMOpSem.evm]
misc_inst_rect [definition, in EVMOpSem.evm]
misc_inst [inductive, in EVMOpSem.evm]
mload [definition, in EVMOpSem.evm]
MLOAD [constructor, in EVMOpSem.evm]
MOD [constructor, in EVMOpSem.evm]
MSIZE [constructor, in EVMOpSem.evm]
mstore [definition, in EVMOpSem.evm]
MSTORE [constructor, in EVMOpSem.evm]
mstore8 [definition, in EVMOpSem.evm]
MSTORE8 [constructor, in EVMOpSem.evm]
MUL [constructor, in EVMOpSem.evm]
MULMOD [constructor, in EVMOpSem.evm]
N
natAsr [definition, in EVMOpSem.Lem.lem_word]natFromBitSeq [definition, in EVMOpSem.Lem.lem_word]
natLand [definition, in EVMOpSem.Lem.lem_word]
natLor [definition, in EVMOpSem.Lem.lem_word]
natLsl [definition, in EVMOpSem.Lem.lem_word]
natLxor [definition, in EVMOpSem.Lem.lem_word]
naturalAsr [definition, in EVMOpSem.Lem.lem_word]
naturalFromBitSeq [definition, in EVMOpSem.Lem.lem_word]
naturalLand [definition, in EVMOpSem.Lem.lem_word]
naturalLor [definition, in EVMOpSem.Lem.lem_word]
naturalLsl [definition, in EVMOpSem.Lem.lem_word]
naturalLxor [definition, in EVMOpSem.Lem.lem_word]
nat_default [definition, in EVMOpSem.Lem.coqharness]
nat_gteb [definition, in EVMOpSem.Lem.coqharness]
nat_gtb [definition, in EVMOpSem.Lem.coqharness]
nat_lteb [definition, in EVMOpSem.Lem.coqharness]
nat_ltb [definition, in EVMOpSem.Lem.coqharness]
nat_max [definition, in EVMOpSem.Lem.coqharness]
nat_min [definition, in EVMOpSem.Lem.coqharness]
nat_mod [axiom, in EVMOpSem.Lem.coqharness]
nat_div [axiom, in EVMOpSem.Lem.coqharness]
nat_power [definition, in EVMOpSem.Lem.coqharness]
network [inductive, in EVMOpSem.evm]
network_of_block_number [definition, in EVMOpSem.evm]
network_default [definition, in EVMOpSem.evm]
network_sind [definition, in EVMOpSem.evm]
network_rec [definition, in EVMOpSem.evm]
network_ind [definition, in EVMOpSem.evm]
network_rect [definition, in EVMOpSem.evm]
new_memory_consumption [definition, in EVMOpSem.evm]
next_state [definition, in EVMOpSem.evm]
nibble [definition, in EVMOpSem.evm]
nibble_default [definition, in EVMOpSem.evm]
Node [constructor, in EVMOpSem.rlplem]
NoHint [constructor, in EVMOpSem.block]
nothing_happens [definition, in EVMOpSem.block]
null [definition, in EVMOpSem.Lem.lem_list]
NumAbs [record, in EVMOpSem.Lem.lem_num]
numAdd [projection, in EVMOpSem.Lem.lem_num]
NumAdd [record, in EVMOpSem.Lem.lem_num]
NUMBER [constructor, in EVMOpSem.evm]
numDivision [projection, in EVMOpSem.Lem.lem_num]
NumDivision [record, in EVMOpSem.Lem.lem_num]
numIntegerDivision [projection, in EVMOpSem.Lem.lem_num]
NumIntegerDivision [record, in EVMOpSem.Lem.lem_num]
numMinus [projection, in EVMOpSem.Lem.lem_num]
NumMinus [record, in EVMOpSem.Lem.lem_num]
numMult [projection, in EVMOpSem.Lem.lem_num]
NumMult [record, in EVMOpSem.Lem.lem_num]
numNegate [projection, in EVMOpSem.Lem.lem_num]
NumNegate [record, in EVMOpSem.Lem.lem_num]
numPow [projection, in EVMOpSem.Lem.lem_num]
NumPow [record, in EVMOpSem.Lem.lem_num]
NumPred [record, in EVMOpSem.Lem.lem_num]
numRemainder [projection, in EVMOpSem.Lem.lem_num]
NumRemainder [record, in EVMOpSem.Lem.lem_num]
NumSucc [record, in EVMOpSem.Lem.lem_num]
O
opt [definition, in EVMOpSem.block]opt_default [definition, in EVMOpSem.block]
Ord [record, in EVMOpSem.Lem.lem_basic_classes]
ordCompare [definition, in EVMOpSem.Lem.lem_basic_classes]
ordering [inductive, in EVMOpSem.Lem.coqharness]
orderingIsEqual [definition, in EVMOpSem.Lem.lem_basic_classes]
orderingIsGreater [definition, in EVMOpSem.Lem.lem_basic_classes]
orderingIsLess [definition, in EVMOpSem.Lem.lem_basic_classes]
ordering_cases [definition, in EVMOpSem.Lem.lem_basic_classes]
ordering_equal [definition, in EVMOpSem.Lem.coqharness]
ordering_sind [definition, in EVMOpSem.Lem.coqharness]
ordering_rec [definition, in EVMOpSem.Lem.coqharness]
ordering_ind [definition, in EVMOpSem.Lem.coqharness]
ordering_rect [definition, in EVMOpSem.Lem.coqharness]
OrdMaxMin [record, in EVMOpSem.Lem.lem_basic_classes]
ORIGIN [constructor, in EVMOpSem.evm]
OutOfGas [constructor, in EVMOpSem.evm]
P
pairCompare [definition, in EVMOpSem.Lem.lem_basic_classes]pairGreater [definition, in EVMOpSem.Lem.lem_basic_classes]
pairGreaterEq [definition, in EVMOpSem.Lem.lem_basic_classes]
pairLess [definition, in EVMOpSem.Lem.lem_basic_classes]
pairLessEq [definition, in EVMOpSem.Lem.lem_basic_classes]
partition [definition, in EVMOpSem.Lem.lem_list]
partitionEither [definition, in EVMOpSem.Lem.lem_either]
partition0 [definition, in EVMOpSem.Lem.lem_set]
pc [definition, in EVMOpSem.evm]
Pc [constructor, in EVMOpSem.evm]
PC [constructor, in EVMOpSem.evm]
pc_inst_numbers [definition, in EVMOpSem.evm]
pc_inst_code [definition, in EVMOpSem.evm]
pc_inst_default [definition, in EVMOpSem.evm]
pc_inst_sind [definition, in EVMOpSem.evm]
pc_inst_rec [definition, in EVMOpSem.evm]
pc_inst_ind [definition, in EVMOpSem.evm]
pc_inst_rect [definition, in EVMOpSem.evm]
pc_inst [inductive, in EVMOpSem.evm]
Pdiv2 [lemma, in EVMOpSem.Zdigits]
pop [definition, in EVMOpSem.evm]
POP [constructor, in EVMOpSem.evm]
pred [projection, in EVMOpSem.Lem.lem_num]
predicate_of_ord [definition, in EVMOpSem.Lem.lem_sorting]
program [record, in EVMOpSem.evm]
program_sem [definition, in EVMOpSem.evm]
program_as_natural_map [definition, in EVMOpSem.evm]
program_of_lst [definition, in EVMOpSem.evm]
program_default [definition, in EVMOpSem.evm]
program_length [projection, in EVMOpSem.evm]
program_content [projection, in EVMOpSem.evm]
Prop_of_bool [definition, in EVMOpSem.Lem.coqharness]
PUSH_N [constructor, in EVMOpSem.evm]
put_return_values [definition, in EVMOpSem.evm]
put_return_values_aux [definition, in EVMOpSem.evm]
Q
Qge_bool [definition, in EVMOpSem.Lem.coqharness]Qgt_bool [definition, in EVMOpSem.Lem.coqharness]
Qlt_bool [definition, in EVMOpSem.Lem.coqharness]
quadrupleCompare [definition, in EVMOpSem.Lem.lem_basic_classes]
quadrupleEqual [definition, in EVMOpSem.Lem.lem_basic_classes]
quadrupleGreater [definition, in EVMOpSem.Lem.lem_basic_classes]
quadrupleGreaterEq [definition, in EVMOpSem.Lem.lem_basic_classes]
quadrupleLess [definition, in EVMOpSem.Lem.lem_basic_classes]
quadrupleLessEq [definition, in EVMOpSem.Lem.lem_basic_classes]
quintupleCompare [definition, in EVMOpSem.Lem.lem_basic_classes]
quintupleEqual [definition, in EVMOpSem.Lem.lem_basic_classes]
quintupleGreater [definition, in EVMOpSem.Lem.lem_basic_classes]
quintupleGreaterEq [definition, in EVMOpSem.Lem.lem_basic_classes]
quintupleLess [definition, in EVMOpSem.Lem.lem_basic_classes]
quintupleLessEq [definition, in EVMOpSem.Lem.lem_basic_classes]
R
rationalFromFrac [definition, in EVMOpSem.Lem.lem_num]Rdown [definition, in EVMOpSem.Lem.coqharness]
read_word_from_bytes [definition, in EVMOpSem.evm]
read_n_bytes [definition, in EVMOpSem.rlplem]
realFromFrac [definition, in EVMOpSem.Lem.lem_num]
receipt [record, in EVMOpSem.block]
receipt_default [definition, in EVMOpSem.block]
receipt_logs [projection, in EVMOpSem.block]
receipt_bloom [projection, in EVMOpSem.block]
receipt_cumulative_gas [projection, in EVMOpSem.block]
receipt_state [projection, in EVMOpSem.block]
reflexiveTransitiveClosureOn [definition, in EVMOpSem.Lem.lem_relation]
refund_selfdestruct [definition, in EVMOpSem.block]
rel [definition, in EVMOpSem.Lem.lem_relation]
relApply [definition, in EVMOpSem.Lem.lem_relation]
relComp [definition, in EVMOpSem.Lem.lem_relation]
relConverse [definition, in EVMOpSem.Lem.lem_relation]
relDomain [definition, in EVMOpSem.Lem.lem_relation]
relEq [definition, in EVMOpSem.Lem.lem_relation]
relFromPred [definition, in EVMOpSem.Lem.lem_relation]
relIdOn [definition, in EVMOpSem.Lem.lem_relation]
relOver [definition, in EVMOpSem.Lem.lem_relation]
relRange [definition, in EVMOpSem.Lem.lem_relation]
relRestrict [definition, in EVMOpSem.Lem.lem_relation]
relToPred [definition, in EVMOpSem.Lem.lem_relation]
rel_default [definition, in EVMOpSem.Lem.lem_relation]
rel_set_default [definition, in EVMOpSem.Lem.lem_relation]
rel_set [definition, in EVMOpSem.Lem.lem_relation]
rel_pred_default [definition, in EVMOpSem.Lem.lem_relation]
rel_pred [definition, in EVMOpSem.Lem.lem_relation]
removeMaybe [definition, in EVMOpSem.Lem.lem_set]
replicate [definition, in EVMOpSem.Lem.lem_list]
resizeBitSeq [definition, in EVMOpSem.Lem.lem_word]
response_to_environment_default [definition, in EVMOpSem.evm]
response_to_environment [record, in EVMOpSem.evm]
ret [definition, in EVMOpSem.evm]
RETURN [constructor, in EVMOpSem.evm]
ReturnTo [constructor, in EVMOpSem.block]
return_result_default [definition, in EVMOpSem.evm]
return_balance [projection, in EVMOpSem.evm]
return_data [projection, in EVMOpSem.evm]
return_result [record, in EVMOpSem.evm]
reverseAppend [definition, in EVMOpSem.Lem.lem_list]
reversePartition [definition, in EVMOpSem.Lem.lem_list]
rev_apply [definition, in EVMOpSem.Lem.lem_function]
Rge_bool_ge [lemma, in EVMOpSem.Lem.coqharness]
Rge_bool [definition, in EVMOpSem.Lem.coqharness]
Rgt_bool_gt [lemma, in EVMOpSem.Lem.coqharness]
Rgt_iff_not_le [lemma, in EVMOpSem.Lem.coqharness]
Rgt_bool [definition, in EVMOpSem.Lem.coqharness]
rho_pi [definition, in EVMOpSem.keccak]
rho_pi_changes [definition, in EVMOpSem.keccak]
rho_pi_inner [definition, in EVMOpSem.keccak]
Rle_bool_le [lemma, in EVMOpSem.Lem.coqharness]
Rle_bool [definition, in EVMOpSem.Lem.coqharness]
RLP [definition, in EVMOpSem.rlplem]
rlplem [library]
RLP_address [definition, in EVMOpSem.rlplem]
RLP_w256 [definition, in EVMOpSem.rlplem]
RLP_nat [definition, in EVMOpSem.rlplem]
Rlt_bool_lt [lemma, in EVMOpSem.Lem.coqharness]
Rlt_Rgt_False [lemma, in EVMOpSem.Lem.coqharness]
Rlt_eq_False [lemma, in EVMOpSem.Lem.coqharness]
Rlt_bool [definition, in EVMOpSem.Lem.coqharness]
rotl64 [definition, in EVMOpSem.keccak]
Rsclear [definition, in EVMOpSem.evm]
rsiz [definition, in EVMOpSem.keccak]
Rsuicide [definition, in EVMOpSem.evm]
r_b [definition, in EVMOpSem.rlplem]
S
Sarith [constructor, in EVMOpSem.evm]sarith_inst_nums [definition, in EVMOpSem.evm]
sarith_inst_code [definition, in EVMOpSem.evm]
sarith_inst_default [definition, in EVMOpSem.evm]
sarith_inst_sind [definition, in EVMOpSem.evm]
sarith_inst_rec [definition, in EVMOpSem.evm]
sarith_inst_ind [definition, in EVMOpSem.evm]
sarith_inst_rect [definition, in EVMOpSem.evm]
sarith_inst [inductive, in EVMOpSem.evm]
SDIV [constructor, in EVMOpSem.evm]
set [definition, in EVMOpSem.Lem.coqharness]
setElemCompare [projection, in EVMOpSem.Lem.lem_basic_classes]
setf [definition, in EVMOpSem.keccak]
setMapMaybe [definition, in EVMOpSem.Lem.lem_set]
SetType [record, in EVMOpSem.Lem.lem_basic_classes]
set_account_code [definition, in EVMOpSem.block]
set_default [definition, in EVMOpSem.Lem.coqharness]
set_tc [axiom, in EVMOpSem.Lem.coqharness]
set_case_by [definition, in EVMOpSem.Lem.coqharness]
set_choose_dependent [definition, in EVMOpSem.Lem.coqharness]
set_sigma [definition, in EVMOpSem.Lem.coqharness]
set_to_list [definition, in EVMOpSem.Lem.coqharness]
set_from_list [definition, in EVMOpSem.Lem.coqharness]
set_proper_subset_by [definition, in EVMOpSem.Lem.coqharness]
set_subset_by [definition, in EVMOpSem.Lem.coqharness]
set_select_subset [definition, in EVMOpSem.Lem.coqharness]
set_fold [definition, in EVMOpSem.Lem.coqharness]
set_diff_by [definition, in EVMOpSem.Lem.coqharness]
set_union_by [definition, in EVMOpSem.Lem.coqharness]
set_inter_by [definition, in EVMOpSem.Lem.coqharness]
set_for_all [definition, in EVMOpSem.Lem.coqharness]
set_any [definition, in EVMOpSem.Lem.coqharness]
set_cardinal [definition, in EVMOpSem.Lem.coqharness]
set_choose [definition, in EVMOpSem.Lem.coqharness]
set_add [definition, in EVMOpSem.Lem.coqharness]
set_is_empty [definition, in EVMOpSem.Lem.coqharness]
set_singleton [definition, in EVMOpSem.Lem.coqharness]
set_empty [definition, in EVMOpSem.Lem.coqharness]
set_compare_by [axiom, in EVMOpSem.Lem.coqharness]
set_member_by [definition, in EVMOpSem.Lem.coqharness]
set_equal_by [definition, in EVMOpSem.Lem.coqharness]
sextupleCompare [definition, in EVMOpSem.Lem.lem_basic_classes]
sextupleEqual [definition, in EVMOpSem.Lem.lem_basic_classes]
sextupleGreater [definition, in EVMOpSem.Lem.lem_basic_classes]
sextupleGreaterEq [definition, in EVMOpSem.Lem.lem_basic_classes]
sextupleLess [definition, in EVMOpSem.Lem.lem_basic_classes]
sextupleLessEq [definition, in EVMOpSem.Lem.lem_basic_classes]
SGT [constructor, in EVMOpSem.evm]
sha3 [definition, in EVMOpSem.evm]
SHA3 [constructor, in EVMOpSem.evm]
sha3_update [definition, in EVMOpSem.keccak]
ShouldNotHappen [constructor, in EVMOpSem.evm]
show [projection, in EVMOpSem.Lem.lem_show]
Show [record, in EVMOpSem.Lem.lem_show]
signextend [definition, in EVMOpSem.evm]
SIGNEXTEND [constructor, in EVMOpSem.evm]
sintFromW256 [definition, in EVMOpSem.evm]
size160 [definition, in EVMOpSem.word160]
size256 [definition, in EVMOpSem.word256]
size32 [definition, in EVMOpSem.word32]
size64 [definition, in EVMOpSem.word64]
SLOAD [constructor, in EVMOpSem.evm]
SLT [constructor, in EVMOpSem.evm]
SMOD [constructor, in EVMOpSem.evm]
split [definition, in EVMOpSem.Lem.lem_set]
splitAt [definition, in EVMOpSem.Lem.lem_list]
splitAtAcc [definition, in EVMOpSem.Lem.lem_list]
splitMember [definition, in EVMOpSem.Lem.lem_set]
splitWhile [definition, in EVMOpSem.Lem.lem_list]
splitWhile_tr [definition, in EVMOpSem.Lem.lem_list]
sstore [definition, in EVMOpSem.evm]
SSTORE [constructor, in EVMOpSem.evm]
Stack [constructor, in EVMOpSem.evm]
stack_3_1_op [definition, in EVMOpSem.evm]
stack_2_1_op [definition, in EVMOpSem.evm]
stack_1_1_op [definition, in EVMOpSem.evm]
stack_0_1_op [definition, in EVMOpSem.evm]
stack_0_0_op [definition, in EVMOpSem.evm]
stack_inst_numbers [definition, in EVMOpSem.evm]
stack_inst_code [definition, in EVMOpSem.evm]
stack_inst_default [definition, in EVMOpSem.evm]
stack_inst_sind [definition, in EVMOpSem.evm]
stack_inst_rec [definition, in EVMOpSem.evm]
stack_inst_ind [definition, in EVMOpSem.evm]
stack_inst_rect [definition, in EVMOpSem.evm]
stack_inst [inductive, in EVMOpSem.evm]
stack_numbers_default [definition, in EVMOpSem.evm]
stack_numbers [definition, in EVMOpSem.evm]
stack_hint_default [definition, in EVMOpSem.block]
stack_hint_sind [definition, in EVMOpSem.block]
stack_hint_rec [definition, in EVMOpSem.block]
stack_hint_ind [definition, in EVMOpSem.block]
stack_hint_rect [definition, in EVMOpSem.block]
stack_hint [inductive, in EVMOpSem.block]
start_transaction [definition, in EVMOpSem.block]
start_env [definition, in EVMOpSem.block]
step [definition, in EVMOpSem.block]
stop [definition, in EVMOpSem.evm]
STOP [constructor, in EVMOpSem.evm]
Storage [constructor, in EVMOpSem.evm]
storage [definition, in EVMOpSem.evm]
storage_inst_numbers [definition, in EVMOpSem.evm]
storage_inst_code [definition, in EVMOpSem.evm]
storage_inst_default [definition, in EVMOpSem.evm]
storage_inst_sind [definition, in EVMOpSem.evm]
storage_inst_rec [definition, in EVMOpSem.evm]
storage_inst_ind [definition, in EVMOpSem.evm]
storage_inst_rect [definition, in EVMOpSem.evm]
storage_inst [inductive, in EVMOpSem.evm]
storage_default [definition, in EVMOpSem.evm]
store_word_memory [definition, in EVMOpSem.evm]
store_byte_list_memory [definition, in EVMOpSem.evm]
strict_if [definition, in EVMOpSem.evm]
stringFromList [definition, in EVMOpSem.Lem.lem_show]
stringFromListAux [definition, in EVMOpSem.Lem.lem_show]
stringFromMaybe [definition, in EVMOpSem.Lem.lem_show]
stringFromPair [definition, in EVMOpSem.Lem.lem_show]
string_case [definition, in EVMOpSem.Lem.lem_string]
string_default [definition, in EVMOpSem.Lem.coqharness]
string_make_string [definition, in EVMOpSem.Lem.coqharness]
string_from_char_list [definition, in EVMOpSem.Lem.coqharness]
string_to_char_list [definition, in EVMOpSem.Lem.coqharness]
string_equal [definition, in EVMOpSem.Lem.coqharness]
SUB [constructor, in EVMOpSem.evm]
subtract_gas [definition, in EVMOpSem.evm]
sub_balance [definition, in EVMOpSem.block]
succ [projection, in EVMOpSem.Lem.lem_num]
suicide [definition, in EVMOpSem.evm]
SUICIDE [constructor, in EVMOpSem.evm]
sum_default [definition, in EVMOpSem.Lem.coqharness]
swap [definition, in EVMOpSem.evm]
Swap [constructor, in EVMOpSem.evm]
swap_inst_numbers [definition, in EVMOpSem.evm]
swap_inst_code [definition, in EVMOpSem.evm]
swap_inst_default [definition, in EVMOpSem.evm]
swap_inst [definition, in EVMOpSem.evm]
T
take [definition, in EVMOpSem.Lem.lem_list]takeWhile [definition, in EVMOpSem.Lem.lem_list]
theta [definition, in EVMOpSem.keccak]
theta_t [definition, in EVMOpSem.keccak]
theta1 [definition, in EVMOpSem.keccak]
thirdComponentOfC [definition, in EVMOpSem.evm]
TIMESTAMP [constructor, in EVMOpSem.evm]
TooLongStack [constructor, in EVMOpSem.evm]
TooShortStack [constructor, in EVMOpSem.evm]
transaction [record, in EVMOpSem.block]
transaction_default [definition, in EVMOpSem.block]
transfer_balance [definition, in EVMOpSem.block]
transitiveClosureAdd [definition, in EVMOpSem.Lem.lem_relation]
tree [inductive, in EVMOpSem.rlplem]
tree_default [definition, in EVMOpSem.rlplem]
tree_sind [definition, in EVMOpSem.rlplem]
tree_rec [definition, in EVMOpSem.rlplem]
tree_ind [definition, in EVMOpSem.rlplem]
tree_rect [definition, in EVMOpSem.rlplem]
tripleCompare [definition, in EVMOpSem.Lem.lem_basic_classes]
tripleEqual [definition, in EVMOpSem.Lem.lem_basic_classes]
tripleGreater [definition, in EVMOpSem.Lem.lem_basic_classes]
tripleGreaterEq [definition, in EVMOpSem.Lem.lem_basic_classes]
tripleLess [definition, in EVMOpSem.Lem.lem_basic_classes]
tripleLessEq [definition, in EVMOpSem.Lem.lem_basic_classes]
tr_result_default [definition, in EVMOpSem.block]
tr_result [record, in EVMOpSem.block]
tr_data [projection, in EVMOpSem.block]
tr_nonce [projection, in EVMOpSem.block]
tr_value [projection, in EVMOpSem.block]
tr_gas_price [projection, in EVMOpSem.block]
tr_gas_limit [projection, in EVMOpSem.block]
tr_to [projection, in EVMOpSem.block]
tr_from [projection, in EVMOpSem.block]
tuple_equal_by [definition, in EVMOpSem.Lem.coqharness]
two_compl_to_Z_to_two_compl [lemma, in EVMOpSem.Zdigits]
two_compl_value_Sn [lemma, in EVMOpSem.Zdigits]
two_compl_value [lemma, in EVMOpSem.Zdigits]
two15 [definition, in EVMOpSem.keccak]
two31 [definition, in EVMOpSem.keccak]
txdatacost [definition, in EVMOpSem.block]
U
uint [definition, in EVMOpSem.evm]uncurry [definition, in EVMOpSem.Lem.lem_function]
Unimplemented [constructor, in EVMOpSem.block]
unit_default [definition, in EVMOpSem.Lem.coqharness]
Unknown [constructor, in EVMOpSem.evm]
unsafe_structural_inequality [definition, in EVMOpSem.Lem.lem_basic_classes]
unzip [definition, in EVMOpSem.Lem.lem_list]
update [definition, in EVMOpSem.Lem.lem_list]
update_byte [definition, in EVMOpSem.keccak]
update_account_state [definition, in EVMOpSem.evm]
update_balance [definition, in EVMOpSem.evm]
update_nonce [definition, in EVMOpSem.block]
update_call [definition, in EVMOpSem.block]
update_return [definition, in EVMOpSem.block]
update_world [definition, in EVMOpSem.block]
V
VALUE_OF_BOOLEAN_VECTORS [section, in EVMOpSem.Zdigits]variable_ctx_default [definition, in EVMOpSem.evm]
variable_ctx [record, in EVMOpSem.evm]
vctx_returned [constructor, in EVMOpSem.evm]
vctx_called [constructor, in EVMOpSem.evm]
vctx_returned_bytes [definition, in EVMOpSem.evm]
vctx_recipient [definition, in EVMOpSem.evm]
vctx_next_instruction_default [definition, in EVMOpSem.evm]
vctx_stack_default [definition, in EVMOpSem.evm]
vctx_advance_pc [definition, in EVMOpSem.evm]
vctx_next_instruction [definition, in EVMOpSem.evm]
vctx_update_storage [definition, in EVMOpSem.evm]
vctx_pop_stack [definition, in EVMOpSem.evm]
vctx_gasprice [projection, in EVMOpSem.evm]
vctx_refund [projection, in EVMOpSem.evm]
vctx_logs [projection, in EVMOpSem.evm]
vctx_touched_storage_index [projection, in EVMOpSem.evm]
vctx_account_existence [projection, in EVMOpSem.evm]
vctx_gas [projection, in EVMOpSem.evm]
vctx_block [projection, in EVMOpSem.evm]
vctx_ext_program [projection, in EVMOpSem.evm]
vctx_origin [projection, in EVMOpSem.evm]
vctx_balance_at_call [projection, in EVMOpSem.evm]
vctx_storage_at_call [projection, in EVMOpSem.evm]
vctx_data_sent [projection, in EVMOpSem.evm]
vctx_value_sent [projection, in EVMOpSem.evm]
vctx_caller [projection, in EVMOpSem.evm]
vctx_balance [projection, in EVMOpSem.evm]
vctx_pc [projection, in EVMOpSem.evm]
vctx_storage [projection, in EVMOpSem.evm]
vctx_memory_usage [projection, in EVMOpSem.evm]
vctx_memory [projection, in EVMOpSem.evm]
vctx_stack [projection, in EVMOpSem.evm]
vctx_update_from_world [definition, in EVMOpSem.block]
W
when_failed [projection, in EVMOpSem.evm]when_returned [projection, in EVMOpSem.evm]
when_called [projection, in EVMOpSem.evm]
withoutTransitiveEdges [definition, in EVMOpSem.Lem.lem_relation]
WordAnd [record, in EVMOpSem.Lem.lem_word]
WordAsr [record, in EVMOpSem.Lem.lem_word]
WordLsl [record, in EVMOpSem.Lem.lem_word]
WordLsr [record, in EVMOpSem.Lem.lem_word]
WordNot [record, in EVMOpSem.Lem.lem_word]
WordOr [record, in EVMOpSem.Lem.lem_word]
WordXor [record, in EVMOpSem.Lem.lem_word]
word_of_bytes [definition, in EVMOpSem.keccak]
word_rcat_k [definition, in EVMOpSem.keccak]
word_rsplit [definition, in EVMOpSem.keccak]
word_rsplit_aux [definition, in EVMOpSem.keccak]
word_exp [definition, in EVMOpSem.evm]
word_rsplit256 [definition, in EVMOpSem.evm]
word_rsplit160 [definition, in EVMOpSem.rlplem]
word160 [inductive, in EVMOpSem.word160]
word160 [library]
word160Add [definition, in EVMOpSem.word160]
word160Asr [definition, in EVMOpSem.word160]
word160BinOp [definition, in EVMOpSem.word160]
word160BinTest [definition, in EVMOpSem.word160]
word160Division [definition, in EVMOpSem.word160]
word160FromBoollist [definition, in EVMOpSem.word160]
word160FromInt [definition, in EVMOpSem.word160]
word160FromInteger [definition, in EVMOpSem.word160]
word160FromNatural [definition, in EVMOpSem.word160]
word160FromNumeral [definition, in EVMOpSem.word160]
word160IntegerDivision [definition, in EVMOpSem.word160]
word160Land [definition, in EVMOpSem.word160]
word160Lnot [definition, in EVMOpSem.word160]
word160Lor [definition, in EVMOpSem.word160]
word160Lsl [definition, in EVMOpSem.word160]
word160Lsr [definition, in EVMOpSem.word160]
word160Lxor [definition, in EVMOpSem.word160]
word160Max [definition, in EVMOpSem.word160]
word160Min [definition, in EVMOpSem.word160]
word160Minus [definition, in EVMOpSem.word160]
word160Mult [definition, in EVMOpSem.word160]
word160NatOp [definition, in EVMOpSem.word160]
word160Negate [definition, in EVMOpSem.word160]
word160Power [definition, in EVMOpSem.word160]
word160Pred [definition, in EVMOpSem.word160]
word160Remainder [definition, in EVMOpSem.word160]
word160Succ [definition, in EVMOpSem.word160]
word160ToInteger [definition, in EVMOpSem.word160]
word160ToNatural [definition, in EVMOpSem.word160]
word160UnaryOp [definition, in EVMOpSem.word160]
word160_default [definition, in EVMOpSem.word160]
word160_sind [definition, in EVMOpSem.word160]
word160_rec [definition, in EVMOpSem.word160]
word160_ind [definition, in EVMOpSem.word160]
word160_rect [definition, in EVMOpSem.word160]
word160_auxiliary [library]
word256 [library]
word256Add [definition, in EVMOpSem.word256]
word256Asr [definition, in EVMOpSem.word256]
word256BinOp [definition, in EVMOpSem.word256]
word256BinTest [definition, in EVMOpSem.word256]
word256Division [definition, in EVMOpSem.word256]
word256FromBoollist [definition, in EVMOpSem.word256]
word256FromInt [definition, in EVMOpSem.word256]
word256FromInteger [definition, in EVMOpSem.word256]
word256FromNat [definition, in EVMOpSem.word256]
word256FromNatural [definition, in EVMOpSem.word256]
word256FromNumeral [definition, in EVMOpSem.word256]
word256IntegerDivision [definition, in EVMOpSem.word256]
word256Land [definition, in EVMOpSem.word256]
word256Lnot [definition, in EVMOpSem.word256]
word256Lor [definition, in EVMOpSem.word256]
word256Lsl [definition, in EVMOpSem.word256]
word256Lsr [definition, in EVMOpSem.word256]
word256Lxor [definition, in EVMOpSem.word256]
word256Max [definition, in EVMOpSem.word256]
word256Min [definition, in EVMOpSem.word256]
word256Minus [definition, in EVMOpSem.word256]
word256Mult [definition, in EVMOpSem.word256]
word256NatOp [definition, in EVMOpSem.word256]
word256Negate [definition, in EVMOpSem.word256]
word256Power [definition, in EVMOpSem.word256]
word256Pred [definition, in EVMOpSem.word256]
word256Remainder [definition, in EVMOpSem.word256]
word256Succ [definition, in EVMOpSem.word256]
word256ToNatural [definition, in EVMOpSem.word256]
word256UGE [definition, in EVMOpSem.word256]
word256UGT [definition, in EVMOpSem.word256]
word256ULT [definition, in EVMOpSem.word256]
word256UnaryOp [definition, in EVMOpSem.word256]
word256_default [definition, in EVMOpSem.helper]
word32 [inductive, in EVMOpSem.word32]
word32 [library]
word32Add [definition, in EVMOpSem.word32]
word32Asr [definition, in EVMOpSem.word32]
word32BinOp [definition, in EVMOpSem.word32]
word32BinTest [definition, in EVMOpSem.word32]
word32Division [definition, in EVMOpSem.word32]
word32FromBoollist [definition, in EVMOpSem.word32]
word32FromInt [definition, in EVMOpSem.word32]
word32FromInteger [definition, in EVMOpSem.word32]
word32FromNat [definition, in EVMOpSem.word32]
word32FromNatural [definition, in EVMOpSem.word32]
word32FromNumeral [definition, in EVMOpSem.word32]
word32IntegerDivision [definition, in EVMOpSem.word32]
word32Land [definition, in EVMOpSem.word32]
word32Lnot [definition, in EVMOpSem.word32]
word32Lor [definition, in EVMOpSem.word32]
word32Lsl [definition, in EVMOpSem.word32]
word32Lsr [definition, in EVMOpSem.word32]
word32Lxor [definition, in EVMOpSem.word32]
word32Max [definition, in EVMOpSem.word32]
word32Min [definition, in EVMOpSem.word32]
word32Minus [definition, in EVMOpSem.word32]
word32Mult [definition, in EVMOpSem.word32]
word32NatOp [definition, in EVMOpSem.word32]
word32Negate [definition, in EVMOpSem.word32]
word32Power [definition, in EVMOpSem.word32]
word32Pred [definition, in EVMOpSem.word32]
word32Remainder [definition, in EVMOpSem.word32]
word32Succ [definition, in EVMOpSem.word32]
word32ToInteger [definition, in EVMOpSem.word32]
word32ToNatural [definition, in EVMOpSem.word32]
word32UGE [definition, in EVMOpSem.word32]
word32UGT [definition, in EVMOpSem.word32]
word32ULT [definition, in EVMOpSem.word32]
word32UnaryOp [definition, in EVMOpSem.word32]
word32_default [definition, in EVMOpSem.word32]
word32_sind [definition, in EVMOpSem.word32]
word32_rec [definition, in EVMOpSem.word32]
word32_ind [definition, in EVMOpSem.word32]
word32_rect [definition, in EVMOpSem.word32]
word32_auxiliary [library]
word4 [inductive, in EVMOpSem.word4]
word4 [library]
word4Add [definition, in EVMOpSem.word4]
word4Asr [definition, in EVMOpSem.word4]
word4BinOp [definition, in EVMOpSem.word4]
word4BinTest [definition, in EVMOpSem.word4]
word4Division [definition, in EVMOpSem.word4]
word4FromBoollist [definition, in EVMOpSem.word4]
word4FromInt [definition, in EVMOpSem.word4]
word4FromInteger [definition, in EVMOpSem.word4]
word4FromNat [definition, in EVMOpSem.word4]
word4FromNatural [definition, in EVMOpSem.word4]
word4FromNumeral [definition, in EVMOpSem.word4]
word4IntegerDivision [definition, in EVMOpSem.word4]
word4Land [definition, in EVMOpSem.word4]
word4Lnot [definition, in EVMOpSem.word4]
word4Lor [definition, in EVMOpSem.word4]
word4Lsl [definition, in EVMOpSem.word4]
word4Lsr [definition, in EVMOpSem.word4]
word4Lxor [definition, in EVMOpSem.word4]
word4Max [definition, in EVMOpSem.word4]
word4Min [definition, in EVMOpSem.word4]
word4Minus [definition, in EVMOpSem.word4]
word4Mult [definition, in EVMOpSem.word4]
word4NatOp [definition, in EVMOpSem.word4]
word4Negate [definition, in EVMOpSem.word4]
word4Power [definition, in EVMOpSem.word4]
word4Pred [definition, in EVMOpSem.word4]
word4Remainder [definition, in EVMOpSem.word4]
word4Succ [definition, in EVMOpSem.word4]
word4ToInt [definition, in EVMOpSem.word4]
word4ToNat [definition, in EVMOpSem.word4]
word4ToUInt [definition, in EVMOpSem.word4]
word4UGT [definition, in EVMOpSem.word4]
word4UnaryOp [definition, in EVMOpSem.word4]
word4_default [definition, in EVMOpSem.word4]
word4_sind [definition, in EVMOpSem.word4]
word4_rec [definition, in EVMOpSem.word4]
word4_ind [definition, in EVMOpSem.word4]
word4_rect [definition, in EVMOpSem.word4]
word4_auxiliary [library]
word64 [inductive, in EVMOpSem.word64]
word64 [library]
word64Add [definition, in EVMOpSem.word64]
word64Asr [definition, in EVMOpSem.word64]
word64BinOp [definition, in EVMOpSem.word64]
word64BinTest [definition, in EVMOpSem.word64]
word64Division [definition, in EVMOpSem.word64]
word64FromBoollist [definition, in EVMOpSem.word64]
word64FromInt [definition, in EVMOpSem.word64]
word64FromInteger [definition, in EVMOpSem.word64]
word64FromNat [definition, in EVMOpSem.word64]
word64FromNatural [definition, in EVMOpSem.word64]
word64FromNumeral [definition, in EVMOpSem.word64]
word64IntegerDivision [definition, in EVMOpSem.word64]
word64Land [definition, in EVMOpSem.word64]
word64Lnot [definition, in EVMOpSem.word64]
word64Lor [definition, in EVMOpSem.word64]
word64Lsl [definition, in EVMOpSem.word64]
word64Lsr [definition, in EVMOpSem.word64]
word64Lxor [definition, in EVMOpSem.word64]
word64Max [definition, in EVMOpSem.word64]
word64Min [definition, in EVMOpSem.word64]
word64Minus [definition, in EVMOpSem.word64]
word64Mult [definition, in EVMOpSem.word64]
word64NatOp [definition, in EVMOpSem.word64]
word64Negate [definition, in EVMOpSem.word64]
word64Power [definition, in EVMOpSem.word64]
word64Pred [definition, in EVMOpSem.word64]
word64Remainder [definition, in EVMOpSem.word64]
word64Succ [definition, in EVMOpSem.word64]
word64ToInteger [definition, in EVMOpSem.word64]
word64ToNatural [definition, in EVMOpSem.word64]
word64UGE [definition, in EVMOpSem.word64]
word64UGT [definition, in EVMOpSem.word64]
word64ULT [definition, in EVMOpSem.word64]
word64UnaryOp [definition, in EVMOpSem.word64]
word64_default [definition, in EVMOpSem.word64]
word64_sind [definition, in EVMOpSem.word64]
word64_rec [definition, in EVMOpSem.word64]
word64_ind [definition, in EVMOpSem.word64]
word64_rect [definition, in EVMOpSem.word64]
word64_auxiliary [library]
word8 [inductive, in EVMOpSem.word8]
word8 [library]
word8Add [definition, in EVMOpSem.word8]
word8Asr [definition, in EVMOpSem.word8]
word8BinOp [definition, in EVMOpSem.word8]
word8BinTest [definition, in EVMOpSem.word8]
word8Division [definition, in EVMOpSem.word8]
word8FromBoollist [definition, in EVMOpSem.word8]
word8FromInt [definition, in EVMOpSem.word8]
word8FromInteger [definition, in EVMOpSem.word8]
word8FromNat [definition, in EVMOpSem.word8]
word8FromNatural [definition, in EVMOpSem.word8]
word8FromNumeral [definition, in EVMOpSem.word8]
word8IntegerDivision [definition, in EVMOpSem.word8]
word8Land [definition, in EVMOpSem.word8]
word8Lnot [definition, in EVMOpSem.word8]
word8Lor [definition, in EVMOpSem.word8]
word8Lsl [definition, in EVMOpSem.word8]
word8Lsr [definition, in EVMOpSem.word8]
word8Lxor [definition, in EVMOpSem.word8]
word8Max [definition, in EVMOpSem.word8]
word8Min [definition, in EVMOpSem.word8]
word8Minus [definition, in EVMOpSem.word8]
word8Mult [definition, in EVMOpSem.word8]
word8NatOp [definition, in EVMOpSem.word8]
word8Negate [definition, in EVMOpSem.word8]
word8Power [definition, in EVMOpSem.word8]
word8Pred [definition, in EVMOpSem.word8]
word8Remainder [definition, in EVMOpSem.word8]
word8Succ [definition, in EVMOpSem.word8]
word8ToInt [definition, in EVMOpSem.word8]
word8ToNat [definition, in EVMOpSem.word8]
word8ToNatural [definition, in EVMOpSem.word8]
word8ToUInt [definition, in EVMOpSem.word8]
word8UGT [definition, in EVMOpSem.word8]
word8UnaryOp [definition, in EVMOpSem.word8]
word8_default [definition, in EVMOpSem.word8]
word8_sind [definition, in EVMOpSem.word8]
word8_rec [definition, in EVMOpSem.word8]
word8_ind [definition, in EVMOpSem.word8]
word8_rect [definition, in EVMOpSem.word8]
word8_to_word64 [definition, in EVMOpSem.keccak]
word8_auxiliary [library]
world_state_default [definition, in EVMOpSem.block]
world_state [definition, in EVMOpSem.block]
W160 [constructor, in EVMOpSem.word160]
w160Compare [definition, in EVMOpSem.word160]
w160Eq [definition, in EVMOpSem.word160]
w160Greater [definition, in EVMOpSem.word160]
w160GreaterEqual [definition, in EVMOpSem.word160]
w160Less [definition, in EVMOpSem.word160]
w160LessEqual [definition, in EVMOpSem.word160]
w160_to_bs [definition, in EVMOpSem.word160]
w256 [definition, in EVMOpSem.keccak]
w256Compare [definition, in EVMOpSem.word256]
w256Eq [definition, in EVMOpSem.word256]
w256Greater [definition, in EVMOpSem.word256]
w256GreaterEqual [definition, in EVMOpSem.word256]
w256Less [definition, in EVMOpSem.word256]
w256LessEqual [definition, in EVMOpSem.word256]
w256_default [definition, in EVMOpSem.keccak]
w256_to_byte [definition, in EVMOpSem.evm]
w256_to_address [definition, in EVMOpSem.evm]
w256_of_bl [definition, in EVMOpSem.evm]
W32 [constructor, in EVMOpSem.word32]
w32Compare [definition, in EVMOpSem.word32]
w32Eq [definition, in EVMOpSem.word32]
w32Greater [definition, in EVMOpSem.word32]
w32GreaterEqual [definition, in EVMOpSem.word32]
w32Less [definition, in EVMOpSem.word32]
w32LessEqual [definition, in EVMOpSem.word32]
w32_to_bs [definition, in EVMOpSem.word32]
W4 [constructor, in EVMOpSem.word4]
w4Compare [definition, in EVMOpSem.word4]
w4Eq [definition, in EVMOpSem.word4]
w4Greater [definition, in EVMOpSem.word4]
w4GreaterEqual [definition, in EVMOpSem.word4]
w4Less [definition, in EVMOpSem.word4]
w4LessEqual [definition, in EVMOpSem.word4]
w4_to_bs [definition, in EVMOpSem.word4]
W64 [constructor, in EVMOpSem.word64]
w64Compare [definition, in EVMOpSem.word64]
w64Eq [definition, in EVMOpSem.word64]
w64Greater [definition, in EVMOpSem.word64]
w64GreaterEqual [definition, in EVMOpSem.word64]
w64Less [definition, in EVMOpSem.word64]
w64LessEqual [definition, in EVMOpSem.word64]
w64_to_bs [definition, in EVMOpSem.word64]
W8 [constructor, in EVMOpSem.word8]
w8Compare [definition, in EVMOpSem.word8]
w8Eq [definition, in EVMOpSem.word8]
w8Greater [definition, in EVMOpSem.word8]
w8GreaterEqual [definition, in EVMOpSem.word8]
w8Less [definition, in EVMOpSem.word8]
w8LessEqual [definition, in EVMOpSem.word8]
w8_to_bs [definition, in EVMOpSem.word8]
X
x0_SetType [instance, in EVMOpSem.Lem.lem_basic_classes]x0_WordAsr [instance, in EVMOpSem.word256]
x1_Ord [instance, in EVMOpSem.Lem.lem_basic_classes]
x1_WordLsr [instance, in EVMOpSem.word256]
x10_Ord [instance, in EVMOpSem.Lem.lem_basic_classes]
x10_NumIntegerDivision [instance, in EVMOpSem.word256]
x100_NumAdd [instance, in EVMOpSem.word4]
x100_NumRemainder [instance, in EVMOpSem.Lem.lem_num]
x101_NumNegate [instance, in EVMOpSem.word4]
x101_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x102_SetType [instance, in EVMOpSem.word4]
x102_NumIntegerDivision [instance, in EVMOpSem.Lem.lem_num]
x103_Ord [instance, in EVMOpSem.word4]
x103_NumPow [instance, in EVMOpSem.Lem.lem_num]
x104_NumMult [instance, in EVMOpSem.Lem.lem_num]
x105_NumPred [instance, in EVMOpSem.Lem.lem_num]
x106_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x107_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x108_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x109_NumAbs [instance, in EVMOpSem.Lem.lem_num]
x11_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x11_NumPow [instance, in EVMOpSem.word256]
x110_NumNegate [instance, in EVMOpSem.Lem.lem_num]
x111_SetType [instance, in EVMOpSem.Lem.lem_num]
x112_Ord [instance, in EVMOpSem.Lem.lem_num]
x113_Eq [instance, in EVMOpSem.Lem.lem_num]
x115_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
x116_NumRemainder [instance, in EVMOpSem.Lem.lem_num]
x117_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x118_NumIntegerDivision [instance, in EVMOpSem.Lem.lem_num]
x119_NumPow [instance, in EVMOpSem.Lem.lem_num]
x12_SetType [instance, in EVMOpSem.Lem.lem_basic_classes]
x12_NumMult [instance, in EVMOpSem.word256]
x120_NumMult [instance, in EVMOpSem.Lem.lem_num]
x121_WordAsr [instance, in EVMOpSem.word32]
x121_NumPred [instance, in EVMOpSem.Lem.lem_num]
x122_WordLsr [instance, in EVMOpSem.word32]
x122_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x123_WordLsl [instance, in EVMOpSem.word32]
x123_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x124_WordXor [instance, in EVMOpSem.word32]
x124_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x125_WordOr [instance, in EVMOpSem.word32]
x125_SetType [instance, in EVMOpSem.Lem.lem_num]
x126_WordAnd [instance, in EVMOpSem.word32]
x126_Ord [instance, in EVMOpSem.Lem.lem_num]
x127_WordNot [instance, in EVMOpSem.word32]
x127_Eq [instance, in EVMOpSem.Lem.lem_num]
x128_OrdMaxMin [instance, in EVMOpSem.word32]
x129_NumRemainder [instance, in EVMOpSem.word32]
x129_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
x13_Ord [instance, in EVMOpSem.Lem.lem_basic_classes]
x13_NumPred [instance, in EVMOpSem.word256]
x130_NumDivision [instance, in EVMOpSem.word32]
x130_NumPow [instance, in EVMOpSem.Lem.lem_num]
x131_NumIntegerDivision [instance, in EVMOpSem.word32]
x131_NumRemainder [instance, in EVMOpSem.Lem.lem_num]
x132_NumPow [instance, in EVMOpSem.word32]
x132_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x133_NumMult [instance, in EVMOpSem.word32]
x133_NumIntegerDivision [instance, in EVMOpSem.Lem.lem_num]
x134_NumPred [instance, in EVMOpSem.word32]
x134_NumMult [instance, in EVMOpSem.Lem.lem_num]
x135_NumSucc [instance, in EVMOpSem.word32]
x135_NumPred [instance, in EVMOpSem.Lem.lem_num]
x136_NumMinus [instance, in EVMOpSem.word32]
x136_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x137_NumAdd [instance, in EVMOpSem.word32]
x137_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x138_NumNegate [instance, in EVMOpSem.word32]
x138_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x139_SetType [instance, in EVMOpSem.word32]
x139_SetType [instance, in EVMOpSem.Lem.lem_num]
x14_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x14_NumSucc [instance, in EVMOpSem.word256]
x140_Ord [instance, in EVMOpSem.word32]
x140_Ord [instance, in EVMOpSem.Lem.lem_num]
x141_Eq [instance, in EVMOpSem.Lem.lem_num]
x143_SetType [instance, in EVMOpSem.Lem.lem_list]
x144_Ord [instance, in EVMOpSem.Lem.lem_list]
x145_Eq [instance, in EVMOpSem.Lem.lem_list]
x146_SetType [instance, in EVMOpSem.Lem.lem_either]
x147_Eq [instance, in EVMOpSem.Lem.lem_either]
x148_Eq [instance, in EVMOpSem.Lem.lem_set]
x149_SetType [instance, in EVMOpSem.Lem.lem_map]
x15_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x15_NumMinus [instance, in EVMOpSem.word256]
x150_Eq [instance, in EVMOpSem.Lem.lem_map]
x155_WordAsr [instance, in EVMOpSem.Lem.lem_word]
x156_WordLsl [instance, in EVMOpSem.Lem.lem_word]
x157_WordAnd [instance, in EVMOpSem.Lem.lem_word]
x158_WordXor [instance, in EVMOpSem.Lem.lem_word]
x159_WordOr [instance, in EVMOpSem.Lem.lem_word]
x16_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x16_NumAdd [instance, in EVMOpSem.word256]
x160_WordAsr [instance, in EVMOpSem.Lem.lem_word]
x161_WordLsr [instance, in EVMOpSem.Lem.lem_word]
x162_WordLsl [instance, in EVMOpSem.Lem.lem_word]
x163_WordAnd [instance, in EVMOpSem.Lem.lem_word]
x164_WordXor [instance, in EVMOpSem.Lem.lem_word]
x165_WordOr [instance, in EVMOpSem.Lem.lem_word]
x166_WordAsr [instance, in EVMOpSem.Lem.lem_word]
x167_WordLsl [instance, in EVMOpSem.Lem.lem_word]
x168_WordAnd [instance, in EVMOpSem.Lem.lem_word]
x169_WordXor [instance, in EVMOpSem.Lem.lem_word]
x17_SetType [instance, in EVMOpSem.Lem.lem_basic_classes]
x17_NumNegate [instance, in EVMOpSem.word256]
x170_WordOr [instance, in EVMOpSem.Lem.lem_word]
x171_WordNot [instance, in EVMOpSem.Lem.lem_word]
x172_WordAsr [instance, in EVMOpSem.Lem.lem_word]
x173_WordLsr [instance, in EVMOpSem.Lem.lem_word]
x174_WordLsl [instance, in EVMOpSem.Lem.lem_word]
x175_WordAnd [instance, in EVMOpSem.Lem.lem_word]
x176_WordXor [instance, in EVMOpSem.Lem.lem_word]
x177_WordOr [instance, in EVMOpSem.Lem.lem_word]
x178_WordNot [instance, in EVMOpSem.Lem.lem_word]
x179_WordAsr [instance, in EVMOpSem.Lem.lem_word]
x18_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x18_SetType [instance, in EVMOpSem.word256]
x180_WordLsr [instance, in EVMOpSem.Lem.lem_word]
x181_WordLsl [instance, in EVMOpSem.Lem.lem_word]
x182_WordAnd [instance, in EVMOpSem.Lem.lem_word]
x183_WordXor [instance, in EVMOpSem.Lem.lem_word]
x184_WordOr [instance, in EVMOpSem.Lem.lem_word]
x185_WordNot [instance, in EVMOpSem.Lem.lem_word]
x186_WordAsr [instance, in EVMOpSem.Lem.lem_word]
x187_WordLsr [instance, in EVMOpSem.Lem.lem_word]
x188_WordLsl [instance, in EVMOpSem.Lem.lem_word]
x189_WordAnd [instance, in EVMOpSem.Lem.lem_word]
x19_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x19_Ord [instance, in EVMOpSem.word256]
x190_WordXor [instance, in EVMOpSem.Lem.lem_word]
x191_WordOr [instance, in EVMOpSem.Lem.lem_word]
x192_WordNot [instance, in EVMOpSem.Lem.lem_word]
x193_WordAsr [instance, in EVMOpSem.Lem.lem_word]
x194_WordLsr [instance, in EVMOpSem.Lem.lem_word]
x195_WordLsl [instance, in EVMOpSem.Lem.lem_word]
x196_WordXor [instance, in EVMOpSem.Lem.lem_word]
x197_WordOr [instance, in EVMOpSem.Lem.lem_word]
x198_WordAnd [instance, in EVMOpSem.Lem.lem_word]
x199_WordNot [instance, in EVMOpSem.Lem.lem_word]
x2_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x2_WordLsl [instance, in EVMOpSem.word256]
x20_Ord [instance, in EVMOpSem.Lem.lem_maybe]
x200_OrdMaxMin [instance, in EVMOpSem.Lem.lem_word]
x201_NumRemainder [instance, in EVMOpSem.Lem.lem_word]
x202_NumDivision [instance, in EVMOpSem.Lem.lem_word]
x203_NumIntegerDivision [instance, in EVMOpSem.Lem.lem_word]
x204_NumPow [instance, in EVMOpSem.Lem.lem_word]
x205_NumMult [instance, in EVMOpSem.Lem.lem_word]
x206_NumPred [instance, in EVMOpSem.Lem.lem_word]
x207_NumSucc [instance, in EVMOpSem.Lem.lem_word]
x208_NumMinus [instance, in EVMOpSem.Lem.lem_word]
x209_NumAdd [instance, in EVMOpSem.Lem.lem_word]
x21_WordAsr [instance, in EVMOpSem.word64]
x21_SetType [instance, in EVMOpSem.Lem.lem_maybe]
x210_NumNegate [instance, in EVMOpSem.Lem.lem_word]
x211_SetType [instance, in EVMOpSem.Lem.lem_word]
x212_Ord [instance, in EVMOpSem.Lem.lem_word]
x214_Eq [instance, in EVMOpSem.Lem.lem_word]
x215_Show [instance, in EVMOpSem.Lem.lem_show]
x216_Show [instance, in EVMOpSem.Lem.lem_show]
x217_Show [instance, in EVMOpSem.Lem.lem_show]
x218_Show [instance, in EVMOpSem.Lem.lem_show]
x219_Show [instance, in EVMOpSem.Lem.lem_show]
x22_WordLsr [instance, in EVMOpSem.word64]
x22_Eq [instance, in EVMOpSem.Lem.lem_maybe]
x23_WordLsl [instance, in EVMOpSem.word64]
x23_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
x24_WordXor [instance, in EVMOpSem.word64]
x24_NumPow [instance, in EVMOpSem.Lem.lem_num]
x25_WordOr [instance, in EVMOpSem.word64]
x25_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x26_WordAnd [instance, in EVMOpSem.word64]
x26_NumMult [instance, in EVMOpSem.Lem.lem_num]
x27_WordNot [instance, in EVMOpSem.word64]
x27_NumPred [instance, in EVMOpSem.Lem.lem_num]
x28_OrdMaxMin [instance, in EVMOpSem.word64]
x28_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x29_NumRemainder [instance, in EVMOpSem.word64]
x29_NumAbs [instance, in EVMOpSem.Lem.lem_num]
x3_SetType [instance, in EVMOpSem.Lem.lem_basic_classes]
x3_WordXor [instance, in EVMOpSem.word256]
x30_NumDivision [instance, in EVMOpSem.word64]
x30_NumNegate [instance, in EVMOpSem.Lem.lem_num]
x31_NumIntegerDivision [instance, in EVMOpSem.word64]
x31_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x32_NumPow [instance, in EVMOpSem.word64]
x32_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x33_NumMult [instance, in EVMOpSem.word64]
x33_SetType [instance, in EVMOpSem.Lem.lem_num]
x34_NumPred [instance, in EVMOpSem.word64]
x34_Ord [instance, in EVMOpSem.Lem.lem_num]
x35_NumSucc [instance, in EVMOpSem.word64]
x35_Eq [instance, in EVMOpSem.Lem.lem_num]
x36_NumMinus [instance, in EVMOpSem.word64]
x37_NumAdd [instance, in EVMOpSem.word64]
x37_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
x38_NumNegate [instance, in EVMOpSem.word64]
x38_NumPow [instance, in EVMOpSem.Lem.lem_num]
x39_SetType [instance, in EVMOpSem.word64]
x39_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x4_Ord [instance, in EVMOpSem.Lem.lem_basic_classes]
x4_WordOr [instance, in EVMOpSem.word256]
x40_Ord [instance, in EVMOpSem.word64]
x40_NumMult [instance, in EVMOpSem.Lem.lem_num]
x41_NumPred [instance, in EVMOpSem.Lem.lem_num]
x42_WordAsr [instance, in EVMOpSem.word8]
x42_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x43_WordLsr [instance, in EVMOpSem.word8]
x43_NumAbs [instance, in EVMOpSem.Lem.lem_num]
x44_WordLsl [instance, in EVMOpSem.word8]
x44_NumNegate [instance, in EVMOpSem.Lem.lem_num]
x45_WordXor [instance, in EVMOpSem.word8]
x45_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x46_WordOr [instance, in EVMOpSem.word8]
x46_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x47_WordAnd [instance, in EVMOpSem.word8]
x47_SetType [instance, in EVMOpSem.Lem.lem_num]
x48_WordNot [instance, in EVMOpSem.word8]
x48_Ord [instance, in EVMOpSem.Lem.lem_num]
x49_OrdMaxMin [instance, in EVMOpSem.word8]
x49_Eq [instance, in EVMOpSem.Lem.lem_num]
x5_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x5_WordAnd [instance, in EVMOpSem.word256]
x50_NumRemainder [instance, in EVMOpSem.word8]
x51_NumDivision [instance, in EVMOpSem.word8]
x51_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
x52_NumIntegerDivision [instance, in EVMOpSem.word8]
x52_NumRemainder [instance, in EVMOpSem.Lem.lem_num]
x53_NumPow [instance, in EVMOpSem.word8]
x53_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x54_NumMult [instance, in EVMOpSem.word8]
x54_NumIntegerDivision [instance, in EVMOpSem.Lem.lem_num]
x55_NumPred [instance, in EVMOpSem.word8]
x55_NumPow [instance, in EVMOpSem.Lem.lem_num]
x56_NumSucc [instance, in EVMOpSem.word8]
x56_NumMult [instance, in EVMOpSem.Lem.lem_num]
x57_NumMinus [instance, in EVMOpSem.word8]
x57_NumPred [instance, in EVMOpSem.Lem.lem_num]
x58_NumAdd [instance, in EVMOpSem.word8]
x58_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x59_NumNegate [instance, in EVMOpSem.word8]
x59_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x6_SetType [instance, in EVMOpSem.Lem.lem_basic_classes]
x6_WordNot [instance, in EVMOpSem.word256]
x60_SetType [instance, in EVMOpSem.word8]
x60_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x61_Ord [instance, in EVMOpSem.word8]
x61_NumAbs [instance, in EVMOpSem.Lem.lem_num]
x62_NumNegate [instance, in EVMOpSem.Lem.lem_num]
x63_WordAsr [instance, in EVMOpSem.word160]
x63_SetType [instance, in EVMOpSem.Lem.lem_num]
x64_WordLsr [instance, in EVMOpSem.word160]
x64_Ord [instance, in EVMOpSem.Lem.lem_num]
x65_WordLsl [instance, in EVMOpSem.word160]
x65_Eq [instance, in EVMOpSem.Lem.lem_num]
x66_WordXor [instance, in EVMOpSem.word160]
x67_WordOr [instance, in EVMOpSem.word160]
x67_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
x68_WordAnd [instance, in EVMOpSem.word160]
x68_NumRemainder [instance, in EVMOpSem.Lem.lem_num]
x69_WordNot [instance, in EVMOpSem.word160]
x69_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x7_Ord [instance, in EVMOpSem.Lem.lem_basic_classes]
x7_OrdMaxMin [instance, in EVMOpSem.word256]
x70_OrdMaxMin [instance, in EVMOpSem.word160]
x70_NumIntegerDivision [instance, in EVMOpSem.Lem.lem_num]
x71_NumRemainder [instance, in EVMOpSem.word160]
x71_NumPow [instance, in EVMOpSem.Lem.lem_num]
x72_NumDivision [instance, in EVMOpSem.word160]
x72_NumMult [instance, in EVMOpSem.Lem.lem_num]
x73_NumIntegerDivision [instance, in EVMOpSem.word160]
x73_NumPred [instance, in EVMOpSem.Lem.lem_num]
x74_NumPow [instance, in EVMOpSem.word160]
x74_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x75_NumMult [instance, in EVMOpSem.word160]
x75_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x76_NumPred [instance, in EVMOpSem.word160]
x76_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x77_NumSucc [instance, in EVMOpSem.word160]
x77_NumAbs [instance, in EVMOpSem.Lem.lem_num]
x78_NumMinus [instance, in EVMOpSem.word160]
x78_NumNegate [instance, in EVMOpSem.Lem.lem_num]
x79_NumAdd [instance, in EVMOpSem.word160]
x79_SetType [instance, in EVMOpSem.Lem.lem_num]
x8_Eq [instance, in EVMOpSem.Lem.lem_basic_classes]
x8_NumRemainder [instance, in EVMOpSem.word256]
x80_NumNegate [instance, in EVMOpSem.word160]
x80_Ord [instance, in EVMOpSem.Lem.lem_num]
x81_SetType [instance, in EVMOpSem.word160]
x81_Eq [instance, in EVMOpSem.Lem.lem_num]
x82_Ord [instance, in EVMOpSem.word160]
x83_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
x84_WordAsr [instance, in EVMOpSem.word4]
x84_NumRemainder [instance, in EVMOpSem.Lem.lem_num]
x85_WordLsr [instance, in EVMOpSem.word4]
x85_NumDivision [instance, in EVMOpSem.Lem.lem_num]
x86_WordLsl [instance, in EVMOpSem.word4]
x86_NumIntegerDivision [instance, in EVMOpSem.Lem.lem_num]
x87_WordXor [instance, in EVMOpSem.word4]
x87_NumPow [instance, in EVMOpSem.Lem.lem_num]
x88_WordOr [instance, in EVMOpSem.word4]
x88_NumMult [instance, in EVMOpSem.Lem.lem_num]
x89_WordAnd [instance, in EVMOpSem.word4]
x89_NumPred [instance, in EVMOpSem.Lem.lem_num]
x9_SetType [instance, in EVMOpSem.Lem.lem_basic_classes]
x9_NumDivision [instance, in EVMOpSem.word256]
x90_WordNot [instance, in EVMOpSem.word4]
x90_NumSucc [instance, in EVMOpSem.Lem.lem_num]
x91_OrdMaxMin [instance, in EVMOpSem.word4]
x91_NumMinus [instance, in EVMOpSem.Lem.lem_num]
x92_NumRemainder [instance, in EVMOpSem.word4]
x92_NumAdd [instance, in EVMOpSem.Lem.lem_num]
x93_NumDivision [instance, in EVMOpSem.word4]
x93_NumAbs [instance, in EVMOpSem.Lem.lem_num]
x94_NumIntegerDivision [instance, in EVMOpSem.word4]
x94_NumNegate [instance, in EVMOpSem.Lem.lem_num]
x95_NumPow [instance, in EVMOpSem.word4]
x95_SetType [instance, in EVMOpSem.Lem.lem_num]
x96_NumMult [instance, in EVMOpSem.word4]
x96_Ord [instance, in EVMOpSem.Lem.lem_num]
x97_NumPred [instance, in EVMOpSem.word4]
x97_Eq [instance, in EVMOpSem.Lem.lem_num]
x98_NumSucc [instance, in EVMOpSem.word4]
x99_NumMinus [instance, in EVMOpSem.word4]
x99_OrdMaxMin [instance, in EVMOpSem.Lem.lem_num]
Z
Zdigits [library]Zdiv2_two_power_nat [lemma, in EVMOpSem.Zdigits]
Zeven_bit_value [lemma, in EVMOpSem.Zdigits]
Zge_minus_two_power_nat_S [lemma, in EVMOpSem.Zdigits]
zip [definition, in EVMOpSem.Lem.lem_list]
Zlt_two_power_nat_S [lemma, in EVMOpSem.Zdigits]
Zmod2 [definition, in EVMOpSem.Zdigits]
Zmod2_twice [lemma, in EVMOpSem.Zdigits]
Zodd_bit_value [lemma, in EVMOpSem.Zdigits]
Z_to_two_compl_to_Z [lemma, in EVMOpSem.Zdigits]
Z_to_binary_to_Z [lemma, in EVMOpSem.Zdigits]
Z_to_two_compl_Sn_z [lemma, in EVMOpSem.Zdigits]
Z_div2_value [lemma, in EVMOpSem.Zdigits]
Z_to_binary_Sn_z [lemma, in EVMOpSem.Zdigits]
Z_to_two_compl_Sn [lemma, in EVMOpSem.Zdigits]
Z_to_binary_Sn [lemma, in EVMOpSem.Zdigits]
Z_BRIC_A_BRAC [section, in EVMOpSem.Zdigits]
Z_to_two_compl [lemma, in EVMOpSem.Zdigits]
Z_to_binary [lemma, in EVMOpSem.Zdigits]
Z_default [definition, in EVMOpSem.Lem.coqharness]
other
_ >= _ [notation, in EVMOpSem.Lem.lem_basic_classes]_ > _ [notation, in EVMOpSem.Lem.lem_basic_classes]
_ <= _ [notation, in EVMOpSem.Lem.lem_basic_classes]
_ < _ [notation, in EVMOpSem.Lem.lem_basic_classes]
_ <> _ [notation, in EVMOpSem.Lem.lem_basic_classes]
_ = _ [notation, in EVMOpSem.Lem.lem_basic_classes]
_ asr _ [notation, in EVMOpSem.Lem.lem_word]
_ lsr _ [notation, in EVMOpSem.Lem.lem_word]
_ lsl _ [notation, in EVMOpSem.Lem.lem_word]
_ lxor _ [notation, in EVMOpSem.Lem.lem_word]
_ lor _ [notation, in EVMOpSem.Lem.lem_word]
_ land _ [notation, in EVMOpSem.Lem.lem_word]
_ union _ [notation, in EVMOpSem.Lem.coqharness]
_ :: _ [notation, in EVMOpSem.Lem.coqharness]
_ mod _ [notation, in EVMOpSem.Lem.lem_num]
_ div _ [notation, in EVMOpSem.Lem.lem_num]
_ / _ [notation, in EVMOpSem.Lem.lem_num]
_ ** _ [notation, in EVMOpSem.Lem.lem_num]
_ * _ [notation, in EVMOpSem.Lem.lem_num]
_ - _ [notation, in EVMOpSem.Lem.lem_num]
_ + _ [notation, in EVMOpSem.Lem.lem_num]
_ ~ _ [notation, in EVMOpSem.Lem.lem_num]
[ _ ; .. ; _ ] [notation, in EVMOpSem.Lem.coqharness]
[ _ ] [notation, in EVMOpSem.Lem.coqharness]
[] [notation, in EVMOpSem.Lem.coqharness]
{[ _ with when_failed := _ ]} [notation, in EVMOpSem.evm]
{[ _ with when_returned := _ ]} [notation, in EVMOpSem.evm]
{[ _ with when_called := _ ]} [notation, in EVMOpSem.evm]
{[ _ with account_killed := _ ]} [notation, in EVMOpSem.evm]
{[ _ with account_ongoing_calls := _ ]} [notation, in EVMOpSem.evm]
{[ _ with account_balance := _ ]} [notation, in EVMOpSem.evm]
{[ _ with account_code := _ ]} [notation, in EVMOpSem.evm]
{[ _ with account_storage := _ ]} [notation, in EVMOpSem.evm]
{[ _ with account_address := _ ]} [notation, in EVMOpSem.evm]
{[ _ with cctx_hash_filter := _ ]} [notation, in EVMOpSem.evm]
{[ _ with cctx_this := _ ]} [notation, in EVMOpSem.evm]
{[ _ with cctx_program := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_gasprice := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_refund := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_logs := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_touched_storage_index := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_account_existence := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_gas := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_block := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_ext_program := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_origin := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_balance_at_call := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_storage_at_call := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_data_sent := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_value_sent := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_caller := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_balance := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_pc := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_storage := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_memory_usage := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_memory := _ ]} [notation, in EVMOpSem.evm]
{[ _ with vctx_stack := _ ]} [notation, in EVMOpSem.evm]
{[ _ with log_data := _ ]} [notation, in EVMOpSem.evm]
{[ _ with log_topics := _ ]} [notation, in EVMOpSem.evm]
{[ _ with log_addr := _ ]} [notation, in EVMOpSem.evm]
{[ _ with block_gaslimit := _ ]} [notation, in EVMOpSem.evm]
{[ _ with block_difficulty := _ ]} [notation, in EVMOpSem.evm]
{[ _ with block_number := _ ]} [notation, in EVMOpSem.evm]
{[ _ with block_timestamp := _ ]} [notation, in EVMOpSem.evm]
{[ _ with block_coinbase := _ ]} [notation, in EVMOpSem.evm]
{[ _ with block_blockhash := _ ]} [notation, in EVMOpSem.evm]
{[ _ with program_length := _ ]} [notation, in EVMOpSem.evm]
{[ _ with program_content := _ ]} [notation, in EVMOpSem.evm]
{[ _ with createarg_code := _ ]} [notation, in EVMOpSem.evm]
{[ _ with createarg_value := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callarg_output_size := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callarg_output_begin := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callarg_data := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callarg_value := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callarg_recipient := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callarg_code := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callarg_gas := _ ]} [notation, in EVMOpSem.evm]
{[ _ with return_balance := _ ]} [notation, in EVMOpSem.evm]
{[ _ with return_data := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callenv_balance := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callenv_blocknum := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callenv_timestamp := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callenv_caller := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callenv_data := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callenv_value := _ ]} [notation, in EVMOpSem.evm]
{[ _ with callenv_gaslimit := _ ]} [notation, in EVMOpSem.evm]
{[ _ with f_logs := _ ]} [notation, in EVMOpSem.block]
{[ _ with f_refund := _ ]} [notation, in EVMOpSem.block]
{[ _ with f_gas := _ ]} [notation, in EVMOpSem.block]
{[ _ with f_killed := _ ]} [notation, in EVMOpSem.block]
{[ _ with f_state := _ ]} [notation, in EVMOpSem.block]
{[ _ with g_create := _ ]} [notation, in EVMOpSem.block]
{[ _ with g_vmstate := _ ]} [notation, in EVMOpSem.block]
{[ _ with g_killed := _ ]} [notation, in EVMOpSem.block]
{[ _ with g_cctx := _ ]} [notation, in EVMOpSem.block]
{[ _ with g_current := _ ]} [notation, in EVMOpSem.block]
{[ _ with g_stack := _ ]} [notation, in EVMOpSem.block]
{[ _ with g_orig := _ ]} [notation, in EVMOpSem.block]
{[ _ with receipt_logs := _ ]} [notation, in EVMOpSem.block]
{[ _ with receipt_bloom := _ ]} [notation, in EVMOpSem.block]
{[ _ with receipt_cumulative_gas := _ ]} [notation, in EVMOpSem.block]
{[ _ with receipt_state := _ ]} [notation, in EVMOpSem.block]
{[ _ with block_account_hascode := _ ]} [notation, in EVMOpSem.block]
{[ _ with block_account_exists := _ ]} [notation, in EVMOpSem.block]
{[ _ with block_account_nonce := _ ]} [notation, in EVMOpSem.block]
{[ _ with block_account_balance := _ ]} [notation, in EVMOpSem.block]
{[ _ with block_account_code := _ ]} [notation, in EVMOpSem.block]
{[ _ with block_account_storage := _ ]} [notation, in EVMOpSem.block]
{[ _ with block_account_address := _ ]} [notation, in EVMOpSem.block]
{[ _ with tr_data := _ ]} [notation, in EVMOpSem.block]
{[ _ with tr_nonce := _ ]} [notation, in EVMOpSem.block]
{[ _ with tr_value := _ ]} [notation, in EVMOpSem.block]
{[ _ with tr_gas_price := _ ]} [notation, in EVMOpSem.block]
{[ _ with tr_gas_limit := _ ]} [notation, in EVMOpSem.block]
{[ _ with tr_to := _ ]} [notation, in EVMOpSem.block]
{[ _ with tr_from := _ ]} [notation, in EVMOpSem.block]
Notation Index
other
_ >= _ [in EVMOpSem.Lem.lem_basic_classes]_ > _ [in EVMOpSem.Lem.lem_basic_classes]
_ <= _ [in EVMOpSem.Lem.lem_basic_classes]
_ < _ [in EVMOpSem.Lem.lem_basic_classes]
_ <> _ [in EVMOpSem.Lem.lem_basic_classes]
_ = _ [in EVMOpSem.Lem.lem_basic_classes]
_ asr _ [in EVMOpSem.Lem.lem_word]
_ lsr _ [in EVMOpSem.Lem.lem_word]
_ lsl _ [in EVMOpSem.Lem.lem_word]
_ lxor _ [in EVMOpSem.Lem.lem_word]
_ lor _ [in EVMOpSem.Lem.lem_word]
_ land _ [in EVMOpSem.Lem.lem_word]
_ union _ [in EVMOpSem.Lem.coqharness]
_ :: _ [in EVMOpSem.Lem.coqharness]
_ mod _ [in EVMOpSem.Lem.lem_num]
_ div _ [in EVMOpSem.Lem.lem_num]
_ / _ [in EVMOpSem.Lem.lem_num]
_ ** _ [in EVMOpSem.Lem.lem_num]
_ * _ [in EVMOpSem.Lem.lem_num]
_ - _ [in EVMOpSem.Lem.lem_num]
_ + _ [in EVMOpSem.Lem.lem_num]
_ ~ _ [in EVMOpSem.Lem.lem_num]
[ _ ; .. ; _ ] [in EVMOpSem.Lem.coqharness]
[ _ ] [in EVMOpSem.Lem.coqharness]
[] [in EVMOpSem.Lem.coqharness]
{[ _ with when_failed := _ ]} [in EVMOpSem.evm]
{[ _ with when_returned := _ ]} [in EVMOpSem.evm]
{[ _ with when_called := _ ]} [in EVMOpSem.evm]
{[ _ with account_killed := _ ]} [in EVMOpSem.evm]
{[ _ with account_ongoing_calls := _ ]} [in EVMOpSem.evm]
{[ _ with account_balance := _ ]} [in EVMOpSem.evm]
{[ _ with account_code := _ ]} [in EVMOpSem.evm]
{[ _ with account_storage := _ ]} [in EVMOpSem.evm]
{[ _ with account_address := _ ]} [in EVMOpSem.evm]
{[ _ with cctx_hash_filter := _ ]} [in EVMOpSem.evm]
{[ _ with cctx_this := _ ]} [in EVMOpSem.evm]
{[ _ with cctx_program := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_gasprice := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_refund := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_logs := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_touched_storage_index := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_account_existence := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_gas := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_block := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_ext_program := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_origin := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_balance_at_call := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_storage_at_call := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_data_sent := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_value_sent := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_caller := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_balance := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_pc := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_storage := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_memory_usage := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_memory := _ ]} [in EVMOpSem.evm]
{[ _ with vctx_stack := _ ]} [in EVMOpSem.evm]
{[ _ with log_data := _ ]} [in EVMOpSem.evm]
{[ _ with log_topics := _ ]} [in EVMOpSem.evm]
{[ _ with log_addr := _ ]} [in EVMOpSem.evm]
{[ _ with block_gaslimit := _ ]} [in EVMOpSem.evm]
{[ _ with block_difficulty := _ ]} [in EVMOpSem.evm]
{[ _ with block_number := _ ]} [in EVMOpSem.evm]
{[ _ with block_timestamp := _ ]} [in EVMOpSem.evm]
{[ _ with block_coinbase := _ ]} [in EVMOpSem.evm]
{[ _ with block_blockhash := _ ]} [in EVMOpSem.evm]
{[ _ with program_length := _ ]} [in EVMOpSem.evm]
{[ _ with program_content := _ ]} [in EVMOpSem.evm]
{[ _ with createarg_code := _ ]} [in EVMOpSem.evm]
{[ _ with createarg_value := _ ]} [in EVMOpSem.evm]
{[ _ with callarg_output_size := _ ]} [in EVMOpSem.evm]
{[ _ with callarg_output_begin := _ ]} [in EVMOpSem.evm]
{[ _ with callarg_data := _ ]} [in EVMOpSem.evm]
{[ _ with callarg_value := _ ]} [in EVMOpSem.evm]
{[ _ with callarg_recipient := _ ]} [in EVMOpSem.evm]
{[ _ with callarg_code := _ ]} [in EVMOpSem.evm]
{[ _ with callarg_gas := _ ]} [in EVMOpSem.evm]
{[ _ with return_balance := _ ]} [in EVMOpSem.evm]
{[ _ with return_data := _ ]} [in EVMOpSem.evm]
{[ _ with callenv_balance := _ ]} [in EVMOpSem.evm]
{[ _ with callenv_blocknum := _ ]} [in EVMOpSem.evm]
{[ _ with callenv_timestamp := _ ]} [in EVMOpSem.evm]
{[ _ with callenv_caller := _ ]} [in EVMOpSem.evm]
{[ _ with callenv_data := _ ]} [in EVMOpSem.evm]
{[ _ with callenv_value := _ ]} [in EVMOpSem.evm]
{[ _ with callenv_gaslimit := _ ]} [in EVMOpSem.evm]
{[ _ with f_logs := _ ]} [in EVMOpSem.block]
{[ _ with f_refund := _ ]} [in EVMOpSem.block]
{[ _ with f_gas := _ ]} [in EVMOpSem.block]
{[ _ with f_killed := _ ]} [in EVMOpSem.block]
{[ _ with f_state := _ ]} [in EVMOpSem.block]
{[ _ with g_create := _ ]} [in EVMOpSem.block]
{[ _ with g_vmstate := _ ]} [in EVMOpSem.block]
{[ _ with g_killed := _ ]} [in EVMOpSem.block]
{[ _ with g_cctx := _ ]} [in EVMOpSem.block]
{[ _ with g_current := _ ]} [in EVMOpSem.block]
{[ _ with g_stack := _ ]} [in EVMOpSem.block]
{[ _ with g_orig := _ ]} [in EVMOpSem.block]
{[ _ with receipt_logs := _ ]} [in EVMOpSem.block]
{[ _ with receipt_bloom := _ ]} [in EVMOpSem.block]
{[ _ with receipt_cumulative_gas := _ ]} [in EVMOpSem.block]
{[ _ with receipt_state := _ ]} [in EVMOpSem.block]
{[ _ with block_account_hascode := _ ]} [in EVMOpSem.block]
{[ _ with block_account_exists := _ ]} [in EVMOpSem.block]
{[ _ with block_account_nonce := _ ]} [in EVMOpSem.block]
{[ _ with block_account_balance := _ ]} [in EVMOpSem.block]
{[ _ with block_account_code := _ ]} [in EVMOpSem.block]
{[ _ with block_account_storage := _ ]} [in EVMOpSem.block]
{[ _ with block_account_address := _ ]} [in EVMOpSem.block]
{[ _ with tr_data := _ ]} [in EVMOpSem.block]
{[ _ with tr_nonce := _ ]} [in EVMOpSem.block]
{[ _ with tr_value := _ ]} [in EVMOpSem.block]
{[ _ with tr_gas_price := _ ]} [in EVMOpSem.block]
{[ _ with tr_gas_limit := _ ]} [in EVMOpSem.block]
{[ _ with tr_to := _ ]} [in EVMOpSem.block]
{[ _ with tr_from := _ ]} [in EVMOpSem.block]
Library Index
B
blockblock_auxiliary
C
coqharnessE
evmevm_auxiliary
H
helperK
keccakkeccak_auxiliary
L
lem_wordlem_sorting
lem_basic_classes
lem_show
lem_tuple
lem_bool
lem_string
lem_relation
lem_map
lem_num
lem_set_helpers
lem_maybe
lem_set
lem_function
lem_list
lem_pervasives
lem_either
R
rlplemW
word160word160_auxiliary
word256
word32
word32_auxiliary
word4
word4_auxiliary
word64
word64_auxiliary
word8
word8_auxiliary
Z
ZdigitsConstructor Index
A
ADD [in EVMOpSem.evm]ADDMOD [in EVMOpSem.evm]
ADDRESS [in EVMOpSem.evm]
Arith [in EVMOpSem.evm]
B
BALANCE [in EVMOpSem.evm]Bits [in EVMOpSem.evm]
BitSeq [in EVMOpSem.Lem.lem_word]
BLOCKHASH [in EVMOpSem.evm]
BYTE [in EVMOpSem.evm]
C
CALL [in EVMOpSem.evm]CALLCODE [in EVMOpSem.evm]
CALLDATACOPY [in EVMOpSem.evm]
CALLDATALOAD [in EVMOpSem.evm]
CALLDATASIZE [in EVMOpSem.evm]
CALLER [in EVMOpSem.evm]
CALLVALUE [in EVMOpSem.evm]
CODECOPY [in EVMOpSem.evm]
CODESIZE [in EVMOpSem.evm]
COINBASE [in EVMOpSem.evm]
Continue [in EVMOpSem.block]
ContractCall [in EVMOpSem.evm]
ContractCreate [in EVMOpSem.evm]
ContractDelegateCall [in EVMOpSem.evm]
ContractFail [in EVMOpSem.evm]
ContractReturn [in EVMOpSem.evm]
ContractSuicide [in EVMOpSem.evm]
CREATE [in EVMOpSem.evm]
CreateAddress [in EVMOpSem.block]
D
DELEGATECALL [in EVMOpSem.evm]DIFFICULTY [in EVMOpSem.evm]
DIV [in EVMOpSem.evm]
Dup [in EVMOpSem.evm]
E
EIP150 [in EVMOpSem.evm]EIP158 [in EVMOpSem.evm]
EnvironmentCall [in EVMOpSem.evm]
EnvironmentFail [in EVMOpSem.evm]
EnvironmentRet [in EVMOpSem.evm]
EQ [in EVMOpSem.Lem.coqharness]
EXP [in EVMOpSem.evm]
EXTCODECOPY [in EVMOpSem.evm]
EXTCODESIZE [in EVMOpSem.evm]
F
Finished [in EVMOpSem.block]Frontier [in EVMOpSem.evm]
G
GAS [in EVMOpSem.evm]GASLIMIT [in EVMOpSem.evm]
GASPRICE [in EVMOpSem.evm]
GT [in EVMOpSem.Lem.coqharness]
H
Homestead [in EVMOpSem.evm]I
Info [in EVMOpSem.evm]InstructionContinue [in EVMOpSem.evm]
InstructionToEnvironment [in EVMOpSem.evm]
inst_LT [in EVMOpSem.evm]
inst_EQ [in EVMOpSem.evm]
inst_GT [in EVMOpSem.evm]
inst_NOT [in EVMOpSem.evm]
inst_XOR [in EVMOpSem.evm]
inst_OR [in EVMOpSem.evm]
inst_AND [in EVMOpSem.evm]
InvalidJumpDestination [in EVMOpSem.evm]
ISZERO [in EVMOpSem.evm]
J
JUMP [in EVMOpSem.evm]JUMPDEST [in EVMOpSem.evm]
JUMPI [in EVMOpSem.evm]
L
Leaf [in EVMOpSem.rlplem]Log [in EVMOpSem.evm]
LOG0 [in EVMOpSem.evm]
LOG1 [in EVMOpSem.evm]
LOG2 [in EVMOpSem.evm]
LOG3 [in EVMOpSem.evm]
LOG4 [in EVMOpSem.evm]
LT [in EVMOpSem.Lem.coqharness]
M
Memory [in EVMOpSem.evm]Metropolis [in EVMOpSem.evm]
Misc [in EVMOpSem.evm]
MLOAD [in EVMOpSem.evm]
MOD [in EVMOpSem.evm]
MSIZE [in EVMOpSem.evm]
MSTORE [in EVMOpSem.evm]
MSTORE8 [in EVMOpSem.evm]
MUL [in EVMOpSem.evm]
MULMOD [in EVMOpSem.evm]
N
Node [in EVMOpSem.rlplem]NoHint [in EVMOpSem.block]
NUMBER [in EVMOpSem.evm]
O
ORIGIN [in EVMOpSem.evm]OutOfGas [in EVMOpSem.evm]
P
Pc [in EVMOpSem.evm]PC [in EVMOpSem.evm]
POP [in EVMOpSem.evm]
PUSH_N [in EVMOpSem.evm]
R
RETURN [in EVMOpSem.evm]ReturnTo [in EVMOpSem.block]
S
Sarith [in EVMOpSem.evm]SDIV [in EVMOpSem.evm]
SGT [in EVMOpSem.evm]
SHA3 [in EVMOpSem.evm]
ShouldNotHappen [in EVMOpSem.evm]
SIGNEXTEND [in EVMOpSem.evm]
SLOAD [in EVMOpSem.evm]
SLT [in EVMOpSem.evm]
SMOD [in EVMOpSem.evm]
SSTORE [in EVMOpSem.evm]
Stack [in EVMOpSem.evm]
STOP [in EVMOpSem.evm]
Storage [in EVMOpSem.evm]
SUB [in EVMOpSem.evm]
SUICIDE [in EVMOpSem.evm]
Swap [in EVMOpSem.evm]
T
TIMESTAMP [in EVMOpSem.evm]TooLongStack [in EVMOpSem.evm]
TooShortStack [in EVMOpSem.evm]
U
Unimplemented [in EVMOpSem.block]Unknown [in EVMOpSem.evm]
V
vctx_returned [in EVMOpSem.evm]vctx_called [in EVMOpSem.evm]
W
W160 [in EVMOpSem.word160]W32 [in EVMOpSem.word32]
W4 [in EVMOpSem.word4]
W64 [in EVMOpSem.word64]
W8 [in EVMOpSem.word8]
Lemma Index
B
binary_to_Z_to_binary [in EVMOpSem.Zdigits]binary_value_pos [in EVMOpSem.Zdigits]
binary_value_Sn [in EVMOpSem.Zdigits]
binary_value [in EVMOpSem.Zdigits]
F
false_eq_true_P [in EVMOpSem.Lem.coqharness]false_eq_true_False [in EVMOpSem.Lem.coqharness]
P
Pdiv2 [in EVMOpSem.Zdigits]R
Rge_bool_ge [in EVMOpSem.Lem.coqharness]Rgt_bool_gt [in EVMOpSem.Lem.coqharness]
Rgt_iff_not_le [in EVMOpSem.Lem.coqharness]
Rle_bool_le [in EVMOpSem.Lem.coqharness]
Rlt_bool_lt [in EVMOpSem.Lem.coqharness]
Rlt_Rgt_False [in EVMOpSem.Lem.coqharness]
Rlt_eq_False [in EVMOpSem.Lem.coqharness]
T
two_compl_to_Z_to_two_compl [in EVMOpSem.Zdigits]two_compl_value_Sn [in EVMOpSem.Zdigits]
two_compl_value [in EVMOpSem.Zdigits]
Z
Zdiv2_two_power_nat [in EVMOpSem.Zdigits]Zeven_bit_value [in EVMOpSem.Zdigits]
Zge_minus_two_power_nat_S [in EVMOpSem.Zdigits]
Zlt_two_power_nat_S [in EVMOpSem.Zdigits]
Zmod2_twice [in EVMOpSem.Zdigits]
Zodd_bit_value [in EVMOpSem.Zdigits]
Z_to_two_compl_to_Z [in EVMOpSem.Zdigits]
Z_to_binary_to_Z [in EVMOpSem.Zdigits]
Z_to_two_compl_Sn_z [in EVMOpSem.Zdigits]
Z_div2_value [in EVMOpSem.Zdigits]
Z_to_binary_Sn_z [in EVMOpSem.Zdigits]
Z_to_two_compl_Sn [in EVMOpSem.Zdigits]
Z_to_binary_Sn [in EVMOpSem.Zdigits]
Z_to_two_compl [in EVMOpSem.Zdigits]
Z_to_binary [in EVMOpSem.Zdigits]
Axiom Index
D
DAEMON [in EVMOpSem.Lem.coqharness]N
nat_mod [in EVMOpSem.Lem.coqharness]nat_div [in EVMOpSem.Lem.coqharness]
S
set_tc [in EVMOpSem.Lem.coqharness]set_compare_by [in EVMOpSem.Lem.coqharness]
Projection Index
A
abs [in EVMOpSem.Lem.lem_num]account_killed [in EVMOpSem.evm]
account_ongoing_calls [in EVMOpSem.evm]
account_balance [in EVMOpSem.evm]
account_code [in EVMOpSem.evm]
account_storage [in EVMOpSem.evm]
account_address [in EVMOpSem.evm]
arithmetic_right_shift [in EVMOpSem.Lem.lem_word]
B
block_gaslimit [in EVMOpSem.evm]block_difficulty [in EVMOpSem.evm]
block_number [in EVMOpSem.evm]
block_timestamp [in EVMOpSem.evm]
block_coinbase [in EVMOpSem.evm]
block_blockhash [in EVMOpSem.evm]
block_account_hascode [in EVMOpSem.block]
block_account_exists [in EVMOpSem.block]
block_account_nonce [in EVMOpSem.block]
block_account_balance [in EVMOpSem.block]
block_account_code [in EVMOpSem.block]
block_account_storage [in EVMOpSem.block]
block_account_address [in EVMOpSem.block]
C
callarg_output_size [in EVMOpSem.evm]callarg_output_begin [in EVMOpSem.evm]
callarg_data [in EVMOpSem.evm]
callarg_value [in EVMOpSem.evm]
callarg_recipient [in EVMOpSem.evm]
callarg_code [in EVMOpSem.evm]
callarg_gas [in EVMOpSem.evm]
callenv_balance [in EVMOpSem.evm]
callenv_blocknum [in EVMOpSem.evm]
callenv_timestamp [in EVMOpSem.evm]
callenv_caller [in EVMOpSem.evm]
callenv_data [in EVMOpSem.evm]
callenv_value [in EVMOpSem.evm]
callenv_gaslimit [in EVMOpSem.evm]
cctx_hash_filter [in EVMOpSem.evm]
cctx_this [in EVMOpSem.evm]
cctx_program [in EVMOpSem.evm]
compare [in EVMOpSem.Lem.lem_basic_classes]
conjunction [in EVMOpSem.Lem.lem_word]
createarg_code [in EVMOpSem.evm]
createarg_value [in EVMOpSem.evm]
E
exclusive_or [in EVMOpSem.Lem.lem_word]F
f_logs [in EVMOpSem.block]f_refund [in EVMOpSem.block]
f_gas [in EVMOpSem.block]
f_killed [in EVMOpSem.block]
f_state [in EVMOpSem.block]
G
g_create [in EVMOpSem.block]g_vmstate [in EVMOpSem.block]
g_killed [in EVMOpSem.block]
g_cctx [in EVMOpSem.block]
g_current [in EVMOpSem.block]
g_stack [in EVMOpSem.block]
g_orig [in EVMOpSem.block]
I
inclusive_or [in EVMOpSem.Lem.lem_word]isEqual [in EVMOpSem.Lem.lem_basic_classes]
isGreater [in EVMOpSem.Lem.lem_basic_classes]
isGreaterEqual [in EVMOpSem.Lem.lem_basic_classes]
isInequal [in EVMOpSem.Lem.lem_basic_classes]
isLess [in EVMOpSem.Lem.lem_basic_classes]
isLessEqual [in EVMOpSem.Lem.lem_basic_classes]
L
left_shift [in EVMOpSem.Lem.lem_word]lnot [in EVMOpSem.Lem.lem_word]
logicial_right_shift [in EVMOpSem.Lem.lem_word]
log_data [in EVMOpSem.evm]
log_topics [in EVMOpSem.evm]
log_addr [in EVMOpSem.evm]
M
mapKeyCompare [in EVMOpSem.Lem.lem_map]max [in EVMOpSem.Lem.lem_basic_classes]
min [in EVMOpSem.Lem.lem_basic_classes]
N
numAdd [in EVMOpSem.Lem.lem_num]numDivision [in EVMOpSem.Lem.lem_num]
numIntegerDivision [in EVMOpSem.Lem.lem_num]
numMinus [in EVMOpSem.Lem.lem_num]
numMult [in EVMOpSem.Lem.lem_num]
numNegate [in EVMOpSem.Lem.lem_num]
numPow [in EVMOpSem.Lem.lem_num]
numRemainder [in EVMOpSem.Lem.lem_num]
P
pred [in EVMOpSem.Lem.lem_num]program_length [in EVMOpSem.evm]
program_content [in EVMOpSem.evm]
R
receipt_logs [in EVMOpSem.block]receipt_bloom [in EVMOpSem.block]
receipt_cumulative_gas [in EVMOpSem.block]
receipt_state [in EVMOpSem.block]
return_balance [in EVMOpSem.evm]
return_data [in EVMOpSem.evm]
S
setElemCompare [in EVMOpSem.Lem.lem_basic_classes]show [in EVMOpSem.Lem.lem_show]
succ [in EVMOpSem.Lem.lem_num]
T
tr_data [in EVMOpSem.block]tr_nonce [in EVMOpSem.block]
tr_value [in EVMOpSem.block]
tr_gas_price [in EVMOpSem.block]
tr_gas_limit [in EVMOpSem.block]
tr_to [in EVMOpSem.block]
tr_from [in EVMOpSem.block]
V
vctx_gasprice [in EVMOpSem.evm]vctx_refund [in EVMOpSem.evm]
vctx_logs [in EVMOpSem.evm]
vctx_touched_storage_index [in EVMOpSem.evm]
vctx_account_existence [in EVMOpSem.evm]
vctx_gas [in EVMOpSem.evm]
vctx_block [in EVMOpSem.evm]
vctx_ext_program [in EVMOpSem.evm]
vctx_origin [in EVMOpSem.evm]
vctx_balance_at_call [in EVMOpSem.evm]
vctx_storage_at_call [in EVMOpSem.evm]
vctx_data_sent [in EVMOpSem.evm]
vctx_value_sent [in EVMOpSem.evm]
vctx_caller [in EVMOpSem.evm]
vctx_balance [in EVMOpSem.evm]
vctx_pc [in EVMOpSem.evm]
vctx_storage [in EVMOpSem.evm]
vctx_memory_usage [in EVMOpSem.evm]
vctx_memory [in EVMOpSem.evm]
vctx_stack [in EVMOpSem.evm]
W
when_failed [in EVMOpSem.evm]when_returned [in EVMOpSem.evm]
when_called [in EVMOpSem.evm]
Inductive Index
A
arith_inst [in EVMOpSem.evm]B
bitSequence [in EVMOpSem.Lem.lem_word]bits_inst [in EVMOpSem.evm]
build_vctx_returned [in EVMOpSem.evm]
build_vctx_called [in EVMOpSem.evm]
C
contract_action [in EVMOpSem.evm]E
environment_action [in EVMOpSem.evm]F
failure_reason [in EVMOpSem.evm]G
global_state [in EVMOpSem.block]I
info_inst [in EVMOpSem.evm]inst [in EVMOpSem.evm]
instruction_result [in EVMOpSem.evm]
L
log_inst [in EVMOpSem.evm]M
memory_inst [in EVMOpSem.evm]misc_inst [in EVMOpSem.evm]
N
network [in EVMOpSem.evm]O
ordering [in EVMOpSem.Lem.coqharness]P
pc_inst [in EVMOpSem.evm]S
sarith_inst [in EVMOpSem.evm]stack_inst [in EVMOpSem.evm]
stack_hint [in EVMOpSem.block]
storage_inst [in EVMOpSem.evm]
T
tree [in EVMOpSem.rlplem]W
word160 [in EVMOpSem.word160]word32 [in EVMOpSem.word32]
word4 [in EVMOpSem.word4]
word64 [in EVMOpSem.word64]
word8 [in EVMOpSem.word8]
Instance Index
X
x0_SetType [in EVMOpSem.Lem.lem_basic_classes]x0_WordAsr [in EVMOpSem.word256]
x1_Ord [in EVMOpSem.Lem.lem_basic_classes]
x1_WordLsr [in EVMOpSem.word256]
x10_Ord [in EVMOpSem.Lem.lem_basic_classes]
x10_NumIntegerDivision [in EVMOpSem.word256]
x100_NumAdd [in EVMOpSem.word4]
x100_NumRemainder [in EVMOpSem.Lem.lem_num]
x101_NumNegate [in EVMOpSem.word4]
x101_NumDivision [in EVMOpSem.Lem.lem_num]
x102_SetType [in EVMOpSem.word4]
x102_NumIntegerDivision [in EVMOpSem.Lem.lem_num]
x103_Ord [in EVMOpSem.word4]
x103_NumPow [in EVMOpSem.Lem.lem_num]
x104_NumMult [in EVMOpSem.Lem.lem_num]
x105_NumPred [in EVMOpSem.Lem.lem_num]
x106_NumSucc [in EVMOpSem.Lem.lem_num]
x107_NumMinus [in EVMOpSem.Lem.lem_num]
x108_NumAdd [in EVMOpSem.Lem.lem_num]
x109_NumAbs [in EVMOpSem.Lem.lem_num]
x11_Eq [in EVMOpSem.Lem.lem_basic_classes]
x11_NumPow [in EVMOpSem.word256]
x110_NumNegate [in EVMOpSem.Lem.lem_num]
x111_SetType [in EVMOpSem.Lem.lem_num]
x112_Ord [in EVMOpSem.Lem.lem_num]
x113_Eq [in EVMOpSem.Lem.lem_num]
x115_OrdMaxMin [in EVMOpSem.Lem.lem_num]
x116_NumRemainder [in EVMOpSem.Lem.lem_num]
x117_NumDivision [in EVMOpSem.Lem.lem_num]
x118_NumIntegerDivision [in EVMOpSem.Lem.lem_num]
x119_NumPow [in EVMOpSem.Lem.lem_num]
x12_SetType [in EVMOpSem.Lem.lem_basic_classes]
x12_NumMult [in EVMOpSem.word256]
x120_NumMult [in EVMOpSem.Lem.lem_num]
x121_WordAsr [in EVMOpSem.word32]
x121_NumPred [in EVMOpSem.Lem.lem_num]
x122_WordLsr [in EVMOpSem.word32]
x122_NumSucc [in EVMOpSem.Lem.lem_num]
x123_WordLsl [in EVMOpSem.word32]
x123_NumMinus [in EVMOpSem.Lem.lem_num]
x124_WordXor [in EVMOpSem.word32]
x124_NumAdd [in EVMOpSem.Lem.lem_num]
x125_WordOr [in EVMOpSem.word32]
x125_SetType [in EVMOpSem.Lem.lem_num]
x126_WordAnd [in EVMOpSem.word32]
x126_Ord [in EVMOpSem.Lem.lem_num]
x127_WordNot [in EVMOpSem.word32]
x127_Eq [in EVMOpSem.Lem.lem_num]
x128_OrdMaxMin [in EVMOpSem.word32]
x129_NumRemainder [in EVMOpSem.word32]
x129_OrdMaxMin [in EVMOpSem.Lem.lem_num]
x13_Ord [in EVMOpSem.Lem.lem_basic_classes]
x13_NumPred [in EVMOpSem.word256]
x130_NumDivision [in EVMOpSem.word32]
x130_NumPow [in EVMOpSem.Lem.lem_num]
x131_NumIntegerDivision [in EVMOpSem.word32]
x131_NumRemainder [in EVMOpSem.Lem.lem_num]
x132_NumPow [in EVMOpSem.word32]
x132_NumDivision [in EVMOpSem.Lem.lem_num]
x133_NumMult [in EVMOpSem.word32]
x133_NumIntegerDivision [in EVMOpSem.Lem.lem_num]
x134_NumPred [in EVMOpSem.word32]
x134_NumMult [in EVMOpSem.Lem.lem_num]
x135_NumSucc [in EVMOpSem.word32]
x135_NumPred [in EVMOpSem.Lem.lem_num]
x136_NumMinus [in EVMOpSem.word32]
x136_NumSucc [in EVMOpSem.Lem.lem_num]
x137_NumAdd [in EVMOpSem.word32]
x137_NumMinus [in EVMOpSem.Lem.lem_num]
x138_NumNegate [in EVMOpSem.word32]
x138_NumAdd [in EVMOpSem.Lem.lem_num]
x139_SetType [in EVMOpSem.word32]
x139_SetType [in EVMOpSem.Lem.lem_num]
x14_Eq [in EVMOpSem.Lem.lem_basic_classes]
x14_NumSucc [in EVMOpSem.word256]
x140_Ord [in EVMOpSem.word32]
x140_Ord [in EVMOpSem.Lem.lem_num]
x141_Eq [in EVMOpSem.Lem.lem_num]
x143_SetType [in EVMOpSem.Lem.lem_list]
x144_Ord [in EVMOpSem.Lem.lem_list]
x145_Eq [in EVMOpSem.Lem.lem_list]
x146_SetType [in EVMOpSem.Lem.lem_either]
x147_Eq [in EVMOpSem.Lem.lem_either]
x148_Eq [in EVMOpSem.Lem.lem_set]
x149_SetType [in EVMOpSem.Lem.lem_map]
x15_Eq [in EVMOpSem.Lem.lem_basic_classes]
x15_NumMinus [in EVMOpSem.word256]
x150_Eq [in EVMOpSem.Lem.lem_map]
x155_WordAsr [in EVMOpSem.Lem.lem_word]
x156_WordLsl [in EVMOpSem.Lem.lem_word]
x157_WordAnd [in EVMOpSem.Lem.lem_word]
x158_WordXor [in EVMOpSem.Lem.lem_word]
x159_WordOr [in EVMOpSem.Lem.lem_word]
x16_Eq [in EVMOpSem.Lem.lem_basic_classes]
x16_NumAdd [in EVMOpSem.word256]
x160_WordAsr [in EVMOpSem.Lem.lem_word]
x161_WordLsr [in EVMOpSem.Lem.lem_word]
x162_WordLsl [in EVMOpSem.Lem.lem_word]
x163_WordAnd [in EVMOpSem.Lem.lem_word]
x164_WordXor [in EVMOpSem.Lem.lem_word]
x165_WordOr [in EVMOpSem.Lem.lem_word]
x166_WordAsr [in EVMOpSem.Lem.lem_word]
x167_WordLsl [in EVMOpSem.Lem.lem_word]
x168_WordAnd [in EVMOpSem.Lem.lem_word]
x169_WordXor [in EVMOpSem.Lem.lem_word]
x17_SetType [in EVMOpSem.Lem.lem_basic_classes]
x17_NumNegate [in EVMOpSem.word256]
x170_WordOr [in EVMOpSem.Lem.lem_word]
x171_WordNot [in EVMOpSem.Lem.lem_word]
x172_WordAsr [in EVMOpSem.Lem.lem_word]
x173_WordLsr [in EVMOpSem.Lem.lem_word]
x174_WordLsl [in EVMOpSem.Lem.lem_word]
x175_WordAnd [in EVMOpSem.Lem.lem_word]
x176_WordXor [in EVMOpSem.Lem.lem_word]
x177_WordOr [in EVMOpSem.Lem.lem_word]
x178_WordNot [in EVMOpSem.Lem.lem_word]
x179_WordAsr [in EVMOpSem.Lem.lem_word]
x18_Eq [in EVMOpSem.Lem.lem_basic_classes]
x18_SetType [in EVMOpSem.word256]
x180_WordLsr [in EVMOpSem.Lem.lem_word]
x181_WordLsl [in EVMOpSem.Lem.lem_word]
x182_WordAnd [in EVMOpSem.Lem.lem_word]
x183_WordXor [in EVMOpSem.Lem.lem_word]
x184_WordOr [in EVMOpSem.Lem.lem_word]
x185_WordNot [in EVMOpSem.Lem.lem_word]
x186_WordAsr [in EVMOpSem.Lem.lem_word]
x187_WordLsr [in EVMOpSem.Lem.lem_word]
x188_WordLsl [in EVMOpSem.Lem.lem_word]
x189_WordAnd [in EVMOpSem.Lem.lem_word]
x19_Eq [in EVMOpSem.Lem.lem_basic_classes]
x19_Ord [in EVMOpSem.word256]
x190_WordXor [in EVMOpSem.Lem.lem_word]
x191_WordOr [in EVMOpSem.Lem.lem_word]
x192_WordNot [in EVMOpSem.Lem.lem_word]
x193_WordAsr [in EVMOpSem.Lem.lem_word]
x194_WordLsr [in EVMOpSem.Lem.lem_word]
x195_WordLsl [in EVMOpSem.Lem.lem_word]
x196_WordXor [in EVMOpSem.Lem.lem_word]
x197_WordOr [in EVMOpSem.Lem.lem_word]
x198_WordAnd [in EVMOpSem.Lem.lem_word]
x199_WordNot [in EVMOpSem.Lem.lem_word]
x2_Eq [in EVMOpSem.Lem.lem_basic_classes]
x2_WordLsl [in EVMOpSem.word256]
x20_Ord [in EVMOpSem.Lem.lem_maybe]
x200_OrdMaxMin [in EVMOpSem.Lem.lem_word]
x201_NumRemainder [in EVMOpSem.Lem.lem_word]
x202_NumDivision [in EVMOpSem.Lem.lem_word]
x203_NumIntegerDivision [in EVMOpSem.Lem.lem_word]
x204_NumPow [in EVMOpSem.Lem.lem_word]
x205_NumMult [in EVMOpSem.Lem.lem_word]
x206_NumPred [in EVMOpSem.Lem.lem_word]
x207_NumSucc [in EVMOpSem.Lem.lem_word]
x208_NumMinus [in EVMOpSem.Lem.lem_word]
x209_NumAdd [in EVMOpSem.Lem.lem_word]
x21_WordAsr [in EVMOpSem.word64]
x21_SetType [in EVMOpSem.Lem.lem_maybe]
x210_NumNegate [in EVMOpSem.Lem.lem_word]
x211_SetType [in EVMOpSem.Lem.lem_word]
x212_Ord [in EVMOpSem.Lem.lem_word]
x214_Eq [in EVMOpSem.Lem.lem_word]
x215_Show [in EVMOpSem.Lem.lem_show]
x216_Show [in EVMOpSem.Lem.lem_show]
x217_Show [in EVMOpSem.Lem.lem_show]
x218_Show [in EVMOpSem.Lem.lem_show]
x219_Show [in EVMOpSem.Lem.lem_show]
x22_WordLsr [in EVMOpSem.word64]
x22_Eq [in EVMOpSem.Lem.lem_maybe]
x23_WordLsl [in EVMOpSem.word64]
x23_OrdMaxMin [in EVMOpSem.Lem.lem_num]
x24_WordXor [in EVMOpSem.word64]
x24_NumPow [in EVMOpSem.Lem.lem_num]
x25_WordOr [in EVMOpSem.word64]
x25_NumDivision [in EVMOpSem.Lem.lem_num]
x26_WordAnd [in EVMOpSem.word64]
x26_NumMult [in EVMOpSem.Lem.lem_num]
x27_WordNot [in EVMOpSem.word64]
x27_NumPred [in EVMOpSem.Lem.lem_num]
x28_OrdMaxMin [in EVMOpSem.word64]
x28_NumSucc [in EVMOpSem.Lem.lem_num]
x29_NumRemainder [in EVMOpSem.word64]
x29_NumAbs [in EVMOpSem.Lem.lem_num]
x3_SetType [in EVMOpSem.Lem.lem_basic_classes]
x3_WordXor [in EVMOpSem.word256]
x30_NumDivision [in EVMOpSem.word64]
x30_NumNegate [in EVMOpSem.Lem.lem_num]
x31_NumIntegerDivision [in EVMOpSem.word64]
x31_NumMinus [in EVMOpSem.Lem.lem_num]
x32_NumPow [in EVMOpSem.word64]
x32_NumAdd [in EVMOpSem.Lem.lem_num]
x33_NumMult [in EVMOpSem.word64]
x33_SetType [in EVMOpSem.Lem.lem_num]
x34_NumPred [in EVMOpSem.word64]
x34_Ord [in EVMOpSem.Lem.lem_num]
x35_NumSucc [in EVMOpSem.word64]
x35_Eq [in EVMOpSem.Lem.lem_num]
x36_NumMinus [in EVMOpSem.word64]
x37_NumAdd [in EVMOpSem.word64]
x37_OrdMaxMin [in EVMOpSem.Lem.lem_num]
x38_NumNegate [in EVMOpSem.word64]
x38_NumPow [in EVMOpSem.Lem.lem_num]
x39_SetType [in EVMOpSem.word64]
x39_NumDivision [in EVMOpSem.Lem.lem_num]
x4_Ord [in EVMOpSem.Lem.lem_basic_classes]
x4_WordOr [in EVMOpSem.word256]
x40_Ord [in EVMOpSem.word64]
x40_NumMult [in EVMOpSem.Lem.lem_num]
x41_NumPred [in EVMOpSem.Lem.lem_num]
x42_WordAsr [in EVMOpSem.word8]
x42_NumSucc [in EVMOpSem.Lem.lem_num]
x43_WordLsr [in EVMOpSem.word8]
x43_NumAbs [in EVMOpSem.Lem.lem_num]
x44_WordLsl [in EVMOpSem.word8]
x44_NumNegate [in EVMOpSem.Lem.lem_num]
x45_WordXor [in EVMOpSem.word8]
x45_NumMinus [in EVMOpSem.Lem.lem_num]
x46_WordOr [in EVMOpSem.word8]
x46_NumAdd [in EVMOpSem.Lem.lem_num]
x47_WordAnd [in EVMOpSem.word8]
x47_SetType [in EVMOpSem.Lem.lem_num]
x48_WordNot [in EVMOpSem.word8]
x48_Ord [in EVMOpSem.Lem.lem_num]
x49_OrdMaxMin [in EVMOpSem.word8]
x49_Eq [in EVMOpSem.Lem.lem_num]
x5_Eq [in EVMOpSem.Lem.lem_basic_classes]
x5_WordAnd [in EVMOpSem.word256]
x50_NumRemainder [in EVMOpSem.word8]
x51_NumDivision [in EVMOpSem.word8]
x51_OrdMaxMin [in EVMOpSem.Lem.lem_num]
x52_NumIntegerDivision [in EVMOpSem.word8]
x52_NumRemainder [in EVMOpSem.Lem.lem_num]
x53_NumPow [in EVMOpSem.word8]
x53_NumDivision [in EVMOpSem.Lem.lem_num]
x54_NumMult [in EVMOpSem.word8]
x54_NumIntegerDivision [in EVMOpSem.Lem.lem_num]
x55_NumPred [in EVMOpSem.word8]
x55_NumPow [in EVMOpSem.Lem.lem_num]
x56_NumSucc [in EVMOpSem.word8]
x56_NumMult [in EVMOpSem.Lem.lem_num]
x57_NumMinus [in EVMOpSem.word8]
x57_NumPred [in EVMOpSem.Lem.lem_num]
x58_NumAdd [in EVMOpSem.word8]
x58_NumSucc [in EVMOpSem.Lem.lem_num]
x59_NumNegate [in EVMOpSem.word8]
x59_NumMinus [in EVMOpSem.Lem.lem_num]
x6_SetType [in EVMOpSem.Lem.lem_basic_classes]
x6_WordNot [in EVMOpSem.word256]
x60_SetType [in EVMOpSem.word8]
x60_NumAdd [in EVMOpSem.Lem.lem_num]
x61_Ord [in EVMOpSem.word8]
x61_NumAbs [in EVMOpSem.Lem.lem_num]
x62_NumNegate [in EVMOpSem.Lem.lem_num]
x63_WordAsr [in EVMOpSem.word160]
x63_SetType [in EVMOpSem.Lem.lem_num]
x64_WordLsr [in EVMOpSem.word160]
x64_Ord [in EVMOpSem.Lem.lem_num]
x65_WordLsl [in EVMOpSem.word160]
x65_Eq [in EVMOpSem.Lem.lem_num]
x66_WordXor [in EVMOpSem.word160]
x67_WordOr [in EVMOpSem.word160]
x67_OrdMaxMin [in EVMOpSem.Lem.lem_num]
x68_WordAnd [in EVMOpSem.word160]
x68_NumRemainder [in EVMOpSem.Lem.lem_num]
x69_WordNot [in EVMOpSem.word160]
x69_NumDivision [in EVMOpSem.Lem.lem_num]
x7_Ord [in EVMOpSem.Lem.lem_basic_classes]
x7_OrdMaxMin [in EVMOpSem.word256]
x70_OrdMaxMin [in EVMOpSem.word160]
x70_NumIntegerDivision [in EVMOpSem.Lem.lem_num]
x71_NumRemainder [in EVMOpSem.word160]
x71_NumPow [in EVMOpSem.Lem.lem_num]
x72_NumDivision [in EVMOpSem.word160]
x72_NumMult [in EVMOpSem.Lem.lem_num]
x73_NumIntegerDivision [in EVMOpSem.word160]
x73_NumPred [in EVMOpSem.Lem.lem_num]
x74_NumPow [in EVMOpSem.word160]
x74_NumSucc [in EVMOpSem.Lem.lem_num]
x75_NumMult [in EVMOpSem.word160]
x75_NumMinus [in EVMOpSem.Lem.lem_num]
x76_NumPred [in EVMOpSem.word160]
x76_NumAdd [in EVMOpSem.Lem.lem_num]
x77_NumSucc [in EVMOpSem.word160]
x77_NumAbs [in EVMOpSem.Lem.lem_num]
x78_NumMinus [in EVMOpSem.word160]
x78_NumNegate [in EVMOpSem.Lem.lem_num]
x79_NumAdd [in EVMOpSem.word160]
x79_SetType [in EVMOpSem.Lem.lem_num]
x8_Eq [in EVMOpSem.Lem.lem_basic_classes]
x8_NumRemainder [in EVMOpSem.word256]
x80_NumNegate [in EVMOpSem.word160]
x80_Ord [in EVMOpSem.Lem.lem_num]
x81_SetType [in EVMOpSem.word160]
x81_Eq [in EVMOpSem.Lem.lem_num]
x82_Ord [in EVMOpSem.word160]
x83_OrdMaxMin [in EVMOpSem.Lem.lem_num]
x84_WordAsr [in EVMOpSem.word4]
x84_NumRemainder [in EVMOpSem.Lem.lem_num]
x85_WordLsr [in EVMOpSem.word4]
x85_NumDivision [in EVMOpSem.Lem.lem_num]
x86_WordLsl [in EVMOpSem.word4]
x86_NumIntegerDivision [in EVMOpSem.Lem.lem_num]
x87_WordXor [in EVMOpSem.word4]
x87_NumPow [in EVMOpSem.Lem.lem_num]
x88_WordOr [in EVMOpSem.word4]
x88_NumMult [in EVMOpSem.Lem.lem_num]
x89_WordAnd [in EVMOpSem.word4]
x89_NumPred [in EVMOpSem.Lem.lem_num]
x9_SetType [in EVMOpSem.Lem.lem_basic_classes]
x9_NumDivision [in EVMOpSem.word256]
x90_WordNot [in EVMOpSem.word4]
x90_NumSucc [in EVMOpSem.Lem.lem_num]
x91_OrdMaxMin [in EVMOpSem.word4]
x91_NumMinus [in EVMOpSem.Lem.lem_num]
x92_NumRemainder [in EVMOpSem.word4]
x92_NumAdd [in EVMOpSem.Lem.lem_num]
x93_NumDivision [in EVMOpSem.word4]
x93_NumAbs [in EVMOpSem.Lem.lem_num]
x94_NumIntegerDivision [in EVMOpSem.word4]
x94_NumNegate [in EVMOpSem.Lem.lem_num]
x95_NumPow [in EVMOpSem.word4]
x95_SetType [in EVMOpSem.Lem.lem_num]
x96_NumMult [in EVMOpSem.word4]
x96_Ord [in EVMOpSem.Lem.lem_num]
x97_NumPred [in EVMOpSem.word4]
x97_Eq [in EVMOpSem.Lem.lem_num]
x98_NumSucc [in EVMOpSem.word4]
x99_NumMinus [in EVMOpSem.word4]
x99_OrdMaxMin [in EVMOpSem.Lem.lem_num]
Section Index
C
COHERENT_VALUE [in EVMOpSem.Zdigits]E
ENCODING_VALUE [in EVMOpSem.Zdigits]V
VALUE_OF_BOOLEAN_VECTORS [in EVMOpSem.Zdigits]Z
Z_BRIC_A_BRAC [in EVMOpSem.Zdigits]Definition Index
A
absnat [in EVMOpSem.evm]account_state_pop_ongoing_call [in EVMOpSem.evm]
account_state_default [in EVMOpSem.evm]
address [in EVMOpSem.evm]
address_to_w256 [in EVMOpSem.evm]
address_default [in EVMOpSem.evm]
add_balance [in EVMOpSem.block]
allDistinct [in EVMOpSem.Lem.lem_list]
arith_inst_numbers [in EVMOpSem.evm]
arith_inst_code [in EVMOpSem.evm]
arith_inst_default [in EVMOpSem.evm]
arith_inst_sind [in EVMOpSem.evm]
arith_inst_rec [in EVMOpSem.evm]
arith_inst_ind [in EVMOpSem.evm]
arith_inst_rect [in EVMOpSem.evm]
at_least_eip150 [in EVMOpSem.evm]
B
BD [in EVMOpSem.rlplem]BD_rev [in EVMOpSem.rlplem]
BE [in EVMOpSem.rlplem]
before_homestead [in EVMOpSem.evm]
beq_nat [in EVMOpSem.Lem.lem_num]
BE_nat [in EVMOpSem.rlplem]
BE_rev_prim [in EVMOpSem.rlplem]
big [in EVMOpSem.keccak]
bigintersection [in EVMOpSem.Lem.lem_set]
bigunion [in EVMOpSem.Lem.lem_set]
bind [in EVMOpSem.Lem.lem_maybe]
bitSeqAdd [in EVMOpSem.Lem.lem_word]
bitSeqAnd [in EVMOpSem.Lem.lem_word]
bitSeqArithBinOp [in EVMOpSem.Lem.lem_word]
bitSeqArithBinTest [in EVMOpSem.Lem.lem_word]
bitSeqArithmeticShiftRight [in EVMOpSem.Lem.lem_word]
bitSeqArithUnaryOp [in EVMOpSem.Lem.lem_word]
bitSeqBinop [in EVMOpSem.Lem.lem_word]
bitSeqBinopAux [in EVMOpSem.Lem.coqharness]
bitSeqCompare [in EVMOpSem.Lem.lem_word]
bitSeqDiv [in EVMOpSem.Lem.lem_word]
bitSeqFromBoolList [in EVMOpSem.Lem.lem_word]
bitSeqFromInt [in EVMOpSem.Lem.lem_word]
bitSeqFromInteger [in EVMOpSem.Lem.lem_word]
bitSeqFromNat [in EVMOpSem.Lem.lem_word]
bitSeqFromNatural [in EVMOpSem.Lem.lem_word]
bitSeqGreater [in EVMOpSem.Lem.lem_word]
bitSeqGreaterEqual [in EVMOpSem.Lem.lem_word]
bitSeqLess [in EVMOpSem.Lem.lem_word]
bitSeqLessEqual [in EVMOpSem.Lem.lem_word]
bitSeqLogicalShiftRight [in EVMOpSem.Lem.lem_word]
bitSeqMax [in EVMOpSem.Lem.lem_word]
bitSeqMin [in EVMOpSem.Lem.lem_word]
bitSeqMinus [in EVMOpSem.Lem.lem_word]
bitSeqMod [in EVMOpSem.Lem.lem_word]
bitSeqMult [in EVMOpSem.Lem.lem_word]
bitSeqNegate [in EVMOpSem.Lem.lem_word]
bitSeqNot [in EVMOpSem.Lem.lem_word]
bitSeqOr [in EVMOpSem.Lem.lem_word]
bitSeqPow [in EVMOpSem.Lem.lem_word]
bitSeqPred [in EVMOpSem.Lem.lem_word]
bitSeqSetBit [in EVMOpSem.Lem.lem_word]
bitSeqShiftLeft [in EVMOpSem.Lem.lem_word]
bitSeqSucc [in EVMOpSem.Lem.lem_word]
bitSeqTestBit [in EVMOpSem.Lem.lem_word]
bitSequence_default [in EVMOpSem.Lem.lem_word]
bitSequence_sind [in EVMOpSem.Lem.lem_word]
bitSequence_rec [in EVMOpSem.Lem.lem_word]
bitSequence_ind [in EVMOpSem.Lem.lem_word]
bitSequence_rect [in EVMOpSem.Lem.lem_word]
bitSeqXor [in EVMOpSem.Lem.lem_word]
bits_stack_nums [in EVMOpSem.evm]
bits_inst_code [in EVMOpSem.evm]
bits_inst_default [in EVMOpSem.evm]
bits_inst_sind [in EVMOpSem.evm]
bits_inst_rec [in EVMOpSem.evm]
bits_inst_ind [in EVMOpSem.evm]
bits_inst_rect [in EVMOpSem.evm]
bit_value [in EVMOpSem.Zdigits]
blockedInstructionContinue [in EVMOpSem.evm]
blocked_jump [in EVMOpSem.evm]
block_info_default [in EVMOpSem.evm]
block_account_default [in EVMOpSem.block]
boolCompare [in EVMOpSem.Lem.lem_basic_classes]
boolListFrombitSeq [in EVMOpSem.Lem.lem_word]
boolListFrombitSeqAux [in EVMOpSem.Lem.lem_word]
boolListFromInteger [in EVMOpSem.Lem.lem_word]
boolListFromNatural [in EVMOpSem.Lem.coqharness]
boolListFromWord160 [in EVMOpSem.word160]
boolListFromWord256 [in EVMOpSem.word256]
boolListFromWord32 [in EVMOpSem.word32]
boolListFromWord4 [in EVMOpSem.word4]
boolListFromWord64 [in EVMOpSem.word64]
boolListFromWord8 [in EVMOpSem.word8]
bool_default [in EVMOpSem.Lem.coqharness]
bool_of_Prop [in EVMOpSem.Lem.coqharness]
bs_to_w160 [in EVMOpSem.word160]
bs_to_w8 [in EVMOpSem.word8]
bs_to_w4 [in EVMOpSem.word4]
bs_to_w64 [in EVMOpSem.word64]
bs_to_w32 [in EVMOpSem.word32]
build_vctx_returned_sind [in EVMOpSem.evm]
build_vctx_returned_ind [in EVMOpSem.evm]
build_vctx_called_sind [in EVMOpSem.evm]
build_vctx_called_ind [in EVMOpSem.evm]
build_vctx_failed [in EVMOpSem.evm]
build_cctx [in EVMOpSem.evm]
build_cctx0 [in EVMOpSem.block]
byte [in EVMOpSem.keccak]
byteFromNat [in EVMOpSem.evm]
bytelist_to_instlist [in EVMOpSem.block]
byte_default [in EVMOpSem.keccak]
byte_list_fill_right [in EVMOpSem.evm]
byte_to_w256 [in EVMOpSem.evm]
byte_to_inst [in EVMOpSem.block]
byte0 [in EVMOpSem.rlplem]
byte0_default [in EVMOpSem.rlplem]
C
C [in EVMOpSem.evm]calc_memu_extra2 [in EVMOpSem.evm]
calc_memu_extra [in EVMOpSem.evm]
calc_igas [in EVMOpSem.block]
calc_address [in EVMOpSem.block]
call [in EVMOpSem.evm]
callcode [in EVMOpSem.evm]
calldatacopy [in EVMOpSem.evm]
call_arguments_default [in EVMOpSem.evm]
call_env_default [in EVMOpSem.evm]
catMaybes [in EVMOpSem.Lem.lem_list]
Ccall [in EVMOpSem.evm]
Ccallgas [in EVMOpSem.evm]
Cextra [in EVMOpSem.evm]
Cgascap [in EVMOpSem.evm]
char_equal [in EVMOpSem.Lem.coqharness]
check_resources [in EVMOpSem.evm]
check_refund [in EVMOpSem.evm]
chi [in EVMOpSem.keccak]
chi_for_j [in EVMOpSem.keccak]
classical_boolean_equivalence [in EVMOpSem.Lem.coqharness]
cleanBitSeq [in EVMOpSem.Lem.lem_word]
Cmem [in EVMOpSem.evm]
Cnew [in EVMOpSem.evm]
codecopy [in EVMOpSem.evm]
codemap [in EVMOpSem.block]
concat [in EVMOpSem.Lem.lem_list]
concat0 [in EVMOpSem.Lem.lem_string]
constant_mark [in EVMOpSem.evm]
constant_ctx_default [in EVMOpSem.evm]
contract_behavior_default [in EVMOpSem.evm]
contract_behavior [in EVMOpSem.evm]
contract_action_default [in EVMOpSem.evm]
contract_action_sind [in EVMOpSem.evm]
contract_action_rec [in EVMOpSem.evm]
contract_action_ind [in EVMOpSem.evm]
contract_action_rect [in EVMOpSem.evm]
count_map [in EVMOpSem.Lem.lem_list]
create [in EVMOpSem.evm]
create_log_entry [in EVMOpSem.evm]
create_arguments_default [in EVMOpSem.evm]
create_account [in EVMOpSem.block]
create_env [in EVMOpSem.block]
cross [in EVMOpSem.Lem.lem_set]
Csstore [in EVMOpSem.evm]
Csuicide [in EVMOpSem.evm]
curry [in EVMOpSem.Lem.lem_function]
cut_natural_map [in EVMOpSem.evm]
cut_data [in EVMOpSem.evm]
cut_memory [in EVMOpSem.evm]
cut_memory_aux_alt [in EVMOpSem.evm]
cut_memory_aux [in EVMOpSem.evm]
Cxfer [in EVMOpSem.evm]
D
datasize [in EVMOpSem.evm]defaultAsr [in EVMOpSem.Lem.lem_word]
defaultLand [in EVMOpSem.Lem.lem_word]
defaultLnot [in EVMOpSem.Lem.lem_word]
defaultLor [in EVMOpSem.Lem.lem_word]
defaultLsl [in EVMOpSem.Lem.lem_word]
defaultLsr [in EVMOpSem.Lem.lem_word]
defaultLxor [in EVMOpSem.Lem.lem_word]
delegatecall [in EVMOpSem.evm]
deleteBy [in EVMOpSem.Lem.lem_list]
deleteFirst [in EVMOpSem.Lem.lem_list]
deletes [in EVMOpSem.Lem.lem_list]
dest_init [in EVMOpSem.Lem.lem_list]
dest_init_aux [in EVMOpSem.Lem.lem_list]
de_r_b [in EVMOpSem.rlplem]
drop [in EVMOpSem.Lem.lem_list]
dropWhile [in EVMOpSem.Lem.lem_list]
dup_inst_numbers [in EVMOpSem.evm]
dup_inst_code [in EVMOpSem.evm]
dup_inst_default [in EVMOpSem.evm]
dup_inst [in EVMOpSem.evm]
E
either [in EVMOpSem.Lem.lem_either]eitherEqual [in EVMOpSem.Lem.lem_either]
eitherEqualBy [in EVMOpSem.Lem.lem_either]
either_setElemCompare [in EVMOpSem.Lem.lem_either]
elem [in EVMOpSem.Lem.lem_list]
elemBy [in EVMOpSem.Lem.lem_list]
empty_memory [in EVMOpSem.evm]
empty_account [in EVMOpSem.evm]
empty_program [in EVMOpSem.evm]
empty_storage [in EVMOpSem.evm]
empty_state [in EVMOpSem.block]
empty_account0 [in EVMOpSem.block]
end_transaction [in EVMOpSem.block]
environment_action_default [in EVMOpSem.evm]
environment_action_sind [in EVMOpSem.evm]
environment_action_rec [in EVMOpSem.evm]
environment_action_ind [in EVMOpSem.evm]
environment_action_rect [in EVMOpSem.evm]
extcodecopy [in EVMOpSem.evm]
F
failure_reason_default [in EVMOpSem.evm]failure_reason_sind [in EVMOpSem.evm]
failure_reason_rec [in EVMOpSem.evm]
failure_reason_ind [in EVMOpSem.evm]
failure_reason_rect [in EVMOpSem.evm]
filter [in EVMOpSem.Lem.lem_set]
filterI [in EVMOpSem.keccak]
find [in EVMOpSem.Lem.lem_list]
findIndex [in EVMOpSem.Lem.lem_list]
findIndices [in EVMOpSem.Lem.lem_list]
findIndices_aux [in EVMOpSem.Lem.lem_list]
fix_push [in EVMOpSem.block]
fmap [in EVMOpSem.Lem.coqharness]
fmap_default [in EVMOpSem.Lem.coqharness]
fmap_range_by [in EVMOpSem.Lem.coqharness]
fmap_domain_by [in EVMOpSem.Lem.coqharness]
fmap_map [in EVMOpSem.Lem.coqharness]
fmap_delete_by [in EVMOpSem.Lem.coqharness]
fmap_all [in EVMOpSem.Lem.coqharness]
fmap_lookup_by [in EVMOpSem.Lem.coqharness]
fmap_is_empty [in EVMOpSem.Lem.coqharness]
fmap_add [in EVMOpSem.Lem.coqharness]
fmap_empty [in EVMOpSem.Lem.coqharness]
fmap_equal_by [in EVMOpSem.Lem.coqharness]
for_inner [in EVMOpSem.keccak]
fromList [in EVMOpSem.Lem.lem_map]
fromMaybe [in EVMOpSem.Lem.lem_maybe]
G
gas [in EVMOpSem.evm]Gbalance [in EVMOpSem.evm]
Gbase [in EVMOpSem.evm]
Gblockhash [in EVMOpSem.evm]
Gcall [in EVMOpSem.evm]
Gcallstipend [in EVMOpSem.evm]
Gcallvalue [in EVMOpSem.evm]
Gcodedeposit [in EVMOpSem.evm]
Gcopy [in EVMOpSem.evm]
Gcreate [in EVMOpSem.evm]
general_dup [in EVMOpSem.evm]
genericCompare [in EVMOpSem.Lem.lem_basic_classes]
genlist [in EVMOpSem.Lem.lem_list]
gen_pow_aux [in EVMOpSem.Lem.coqharness]
gen_pow [in EVMOpSem.Lem.lem_num]
get [in EVMOpSem.keccak]
get_n [in EVMOpSem.keccak]
get_byte [in EVMOpSem.evm]
get_opt [in EVMOpSem.block]
get_hint [in EVMOpSem.block]
Gexp [in EVMOpSem.evm]
Gexpbyte [in EVMOpSem.evm]
Gextcode [in EVMOpSem.evm]
Ghigh [in EVMOpSem.evm]
Gjumpdest [in EVMOpSem.evm]
global_state_default [in EVMOpSem.block]
global_state_sind [in EVMOpSem.block]
global_state_rec [in EVMOpSem.block]
global_state_ind [in EVMOpSem.block]
global_state_rect [in EVMOpSem.block]
global_default [in EVMOpSem.block]
Glog [in EVMOpSem.evm]
Glogdata [in EVMOpSem.evm]
Glogtopic [in EVMOpSem.evm]
Glow [in EVMOpSem.evm]
Gmemory [in EVMOpSem.evm]
Gmid [in EVMOpSem.evm]
Gnewaccount [in EVMOpSem.evm]
Gsha3 [in EVMOpSem.evm]
Gsha3word [in EVMOpSem.evm]
Gsload [in EVMOpSem.evm]
Gsreset [in EVMOpSem.evm]
Gsset [in EVMOpSem.evm]
Gsuicide [in EVMOpSem.evm]
Gtransaction [in EVMOpSem.evm]
Gtxcreate [in EVMOpSem.evm]
Gtxdatanonzero [in EVMOpSem.evm]
Gtxdatazero [in EVMOpSem.evm]
Gverylow [in EVMOpSem.evm]
Gzero [in EVMOpSem.evm]
H
homestead_block [in EVMOpSem.evm]I
index [in EVMOpSem.Lem.lem_list]info_inst_numbers [in EVMOpSem.evm]
info_inst_code [in EVMOpSem.evm]
info_inst_default [in EVMOpSem.evm]
info_inst_sind [in EVMOpSem.evm]
info_inst_rec [in EVMOpSem.evm]
info_inst_ind [in EVMOpSem.evm]
info_inst_rect [in EVMOpSem.evm]
initial_pos [in EVMOpSem.keccak]
initial_st [in EVMOpSem.keccak]
input_as_natural_map [in EVMOpSem.evm]
insertBy [in EVMOpSem.Lem.lem_sorting]
insertSortBy [in EVMOpSem.Lem.lem_sorting]
instruction_sem [in EVMOpSem.evm]
instruction_return_result [in EVMOpSem.evm]
instruction_failure_result [in EVMOpSem.evm]
instruction_result_default [in EVMOpSem.evm]
instruction_result_sind [in EVMOpSem.evm]
instruction_result_rec [in EVMOpSem.evm]
instruction_result_ind [in EVMOpSem.evm]
instruction_result_rect [in EVMOpSem.evm]
inst_size [in EVMOpSem.evm]
inst_stack_numbers [in EVMOpSem.evm]
inst_code [in EVMOpSem.evm]
inst_default [in EVMOpSem.evm]
inst_sind [in EVMOpSem.evm]
inst_rec [in EVMOpSem.evm]
inst_ind [in EVMOpSem.evm]
inst_rect [in EVMOpSem.evm]
inst_to_byte [in EVMOpSem.block]
intAsr [in EVMOpSem.Lem.lem_word]
integerAsr [in EVMOpSem.Lem.lem_word]
integerFromBitSeq [in EVMOpSem.Lem.lem_word]
integerFromBoolList [in EVMOpSem.Lem.lem_word]
integerFromBoolListAux [in EVMOpSem.Lem.lem_word]
integerLand [in EVMOpSem.Lem.lem_word]
integerLnot [in EVMOpSem.Lem.lem_word]
integerLor [in EVMOpSem.Lem.lem_word]
integerLsl [in EVMOpSem.Lem.lem_word]
integerLxor [in EVMOpSem.Lem.lem_word]
intFromBitSeq [in EVMOpSem.Lem.lem_word]
intLand [in EVMOpSem.Lem.lem_word]
intLnot [in EVMOpSem.Lem.lem_word]
intLor [in EVMOpSem.Lem.lem_word]
intLsl [in EVMOpSem.Lem.lem_word]
intLxor [in EVMOpSem.Lem.lem_word]
int_gteb [in EVMOpSem.Lem.coqharness]
int_lteb [in EVMOpSem.Lem.coqharness]
int_gtb [in EVMOpSem.Lem.coqharness]
int_ltb [in EVMOpSem.Lem.coqharness]
int32Abs [in EVMOpSem.Lem.lem_num]
int32FromInt [in EVMOpSem.Lem.lem_num]
int32FromInteger [in EVMOpSem.Lem.lem_num]
int32FromInt64 [in EVMOpSem.Lem.lem_num]
int64Abs [in EVMOpSem.Lem.lem_num]
int64FromInt [in EVMOpSem.Lem.lem_num]
int64FromInteger [in EVMOpSem.Lem.lem_num]
int64FromInt32 [in EVMOpSem.Lem.lem_num]
invert_endian [in EVMOpSem.keccak]
iota [in EVMOpSem.keccak]
iota0 [in EVMOpSem.evm]
isAntisymmetric [in EVMOpSem.Lem.lem_relation]
isAntisymmetricOn [in EVMOpSem.Lem.lem_relation]
isEquivalenceOn [in EVMOpSem.Lem.lem_relation]
isIrreflexive [in EVMOpSem.Lem.lem_relation]
isIrreflexiveOn [in EVMOpSem.Lem.lem_relation]
isJust [in EVMOpSem.Lem.lem_maybe]
isNothing [in EVMOpSem.Lem.lem_maybe]
isPartialOrderOn [in EVMOpSem.Lem.lem_relation]
isPermutationBy [in EVMOpSem.Lem.lem_sorting]
isPrefixOf [in EVMOpSem.Lem.lem_list]
isPreorderOn [in EVMOpSem.Lem.lem_relation]
isReflexiveOn [in EVMOpSem.Lem.lem_relation]
isSingleValued [in EVMOpSem.Lem.lem_relation]
isSortedBy [in EVMOpSem.Lem.lem_sorting]
isStrictPartialOrder [in EVMOpSem.Lem.lem_relation]
isStrictPartialOrderOn [in EVMOpSem.Lem.lem_relation]
isStrictTotalOrderOn [in EVMOpSem.Lem.lem_relation]
isSymmetric [in EVMOpSem.Lem.lem_relation]
isSymmetricOn [in EVMOpSem.Lem.lem_relation]
isTotalOn [in EVMOpSem.Lem.lem_relation]
isTotalOrderOn [in EVMOpSem.Lem.lem_relation]
isTransitive [in EVMOpSem.Lem.lem_relation]
isTransitiveOn [in EVMOpSem.Lem.lem_relation]
isTrichotomousOn [in EVMOpSem.Lem.lem_relation]
is_call_like [in EVMOpSem.evm]
J
jump [in EVMOpSem.evm]jumpi [in EVMOpSem.evm]
K
keccak [in EVMOpSem.keccak]keccakf [in EVMOpSem.keccak]
keccakf_rounds [in EVMOpSem.keccak]
keccakf_piln [in EVMOpSem.keccak]
keccakf_rotc [in EVMOpSem.keccak]
keccakf_randc [in EVMOpSem.keccak]
keccak_final [in EVMOpSem.keccak]
keccak' [in EVMOpSem.keccak]
kill_accounts [in EVMOpSem.block]
L
L [in EVMOpSem.evm]leastFixedPoint [in EVMOpSem.Lem.lem_set]
lexicographicCompareBy [in EVMOpSem.Lem.lem_list]
lexicographicLessBy [in EVMOpSem.Lem.lem_list]
lexicographicLessEqBy [in EVMOpSem.Lem.lem_list]
list_fill_left [in EVMOpSem.keccak]
list_fill_right [in EVMOpSem.keccak]
list_swap [in EVMOpSem.evm]
list_default [in EVMOpSem.Lem.coqharness]
list_tail [in EVMOpSem.Lem.coqharness]
list_head [in EVMOpSem.Lem.coqharness]
list_member_by [in EVMOpSem.Lem.coqharness]
list_equal_by [in EVMOpSem.Lem.coqharness]
log [in EVMOpSem.evm]
log_entry_default [in EVMOpSem.evm]
log_inst_numbers [in EVMOpSem.evm]
log_inst_code [in EVMOpSem.evm]
log_inst_default [in EVMOpSem.evm]
log_inst_sind [in EVMOpSem.evm]
log_inst_rec [in EVMOpSem.evm]
log_inst_ind [in EVMOpSem.evm]
log_inst_rect [in EVMOpSem.evm]
log256floor [in EVMOpSem.evm]
lookupBy [in EVMOpSem.Lem.lem_list]
M
M [in EVMOpSem.evm]make_program [in EVMOpSem.block]
make_opt [in EVMOpSem.block]
map [in EVMOpSem.Lem.lem_set]
mapi [in EVMOpSem.Lem.lem_list]
mapiAux [in EVMOpSem.Lem.lem_list]
mapMaybe [in EVMOpSem.Lem.lem_list]
map_setElemCompare [in EVMOpSem.Lem.lem_map]
map_tr [in EVMOpSem.Lem.lem_list]
maxByLessEqual [in EVMOpSem.Lem.lem_basic_classes]
maybe [in EVMOpSem.Lem.lem_maybe]
maybeCompare [in EVMOpSem.Lem.lem_maybe]
maybeEqualBy [in EVMOpSem.Lem.lem_maybe]
maybe_to_list [in EVMOpSem.evm]
maybe_default [in EVMOpSem.Lem.coqharness]
mdlen [in EVMOpSem.keccak]
memory [in EVMOpSem.evm]
memory_inst_numbers [in EVMOpSem.evm]
memory_inst_code [in EVMOpSem.evm]
memory_inst_default [in EVMOpSem.evm]
memory_inst_sind [in EVMOpSem.evm]
memory_inst_rec [in EVMOpSem.evm]
memory_inst_ind [in EVMOpSem.evm]
memory_inst_rect [in EVMOpSem.evm]
memory_default [in EVMOpSem.evm]
meter_gas [in EVMOpSem.evm]
minByLessEqual [in EVMOpSem.Lem.lem_basic_classes]
misc_inst_numbers [in EVMOpSem.evm]
misc_inst_code [in EVMOpSem.evm]
misc_inst_default [in EVMOpSem.evm]
misc_inst_sind [in EVMOpSem.evm]
misc_inst_rec [in EVMOpSem.evm]
misc_inst_ind [in EVMOpSem.evm]
misc_inst_rect [in EVMOpSem.evm]
mload [in EVMOpSem.evm]
mstore [in EVMOpSem.evm]
mstore8 [in EVMOpSem.evm]
N
natAsr [in EVMOpSem.Lem.lem_word]natFromBitSeq [in EVMOpSem.Lem.lem_word]
natLand [in EVMOpSem.Lem.lem_word]
natLor [in EVMOpSem.Lem.lem_word]
natLsl [in EVMOpSem.Lem.lem_word]
natLxor [in EVMOpSem.Lem.lem_word]
naturalAsr [in EVMOpSem.Lem.lem_word]
naturalFromBitSeq [in EVMOpSem.Lem.lem_word]
naturalLand [in EVMOpSem.Lem.lem_word]
naturalLor [in EVMOpSem.Lem.lem_word]
naturalLsl [in EVMOpSem.Lem.lem_word]
naturalLxor [in EVMOpSem.Lem.lem_word]
nat_default [in EVMOpSem.Lem.coqharness]
nat_gteb [in EVMOpSem.Lem.coqharness]
nat_gtb [in EVMOpSem.Lem.coqharness]
nat_lteb [in EVMOpSem.Lem.coqharness]
nat_ltb [in EVMOpSem.Lem.coqharness]
nat_max [in EVMOpSem.Lem.coqharness]
nat_min [in EVMOpSem.Lem.coqharness]
nat_power [in EVMOpSem.Lem.coqharness]
network_of_block_number [in EVMOpSem.evm]
network_default [in EVMOpSem.evm]
network_sind [in EVMOpSem.evm]
network_rec [in EVMOpSem.evm]
network_ind [in EVMOpSem.evm]
network_rect [in EVMOpSem.evm]
new_memory_consumption [in EVMOpSem.evm]
next_state [in EVMOpSem.evm]
nibble [in EVMOpSem.evm]
nibble_default [in EVMOpSem.evm]
nothing_happens [in EVMOpSem.block]
null [in EVMOpSem.Lem.lem_list]
O
opt [in EVMOpSem.block]opt_default [in EVMOpSem.block]
ordCompare [in EVMOpSem.Lem.lem_basic_classes]
orderingIsEqual [in EVMOpSem.Lem.lem_basic_classes]
orderingIsGreater [in EVMOpSem.Lem.lem_basic_classes]
orderingIsLess [in EVMOpSem.Lem.lem_basic_classes]
ordering_cases [in EVMOpSem.Lem.lem_basic_classes]
ordering_equal [in EVMOpSem.Lem.coqharness]
ordering_sind [in EVMOpSem.Lem.coqharness]
ordering_rec [in EVMOpSem.Lem.coqharness]
ordering_ind [in EVMOpSem.Lem.coqharness]
ordering_rect [in EVMOpSem.Lem.coqharness]
P
pairCompare [in EVMOpSem.Lem.lem_basic_classes]pairGreater [in EVMOpSem.Lem.lem_basic_classes]
pairGreaterEq [in EVMOpSem.Lem.lem_basic_classes]
pairLess [in EVMOpSem.Lem.lem_basic_classes]
pairLessEq [in EVMOpSem.Lem.lem_basic_classes]
partition [in EVMOpSem.Lem.lem_list]
partitionEither [in EVMOpSem.Lem.lem_either]
partition0 [in EVMOpSem.Lem.lem_set]
pc [in EVMOpSem.evm]
pc_inst_numbers [in EVMOpSem.evm]
pc_inst_code [in EVMOpSem.evm]
pc_inst_default [in EVMOpSem.evm]
pc_inst_sind [in EVMOpSem.evm]
pc_inst_rec [in EVMOpSem.evm]
pc_inst_ind [in EVMOpSem.evm]
pc_inst_rect [in EVMOpSem.evm]
pop [in EVMOpSem.evm]
predicate_of_ord [in EVMOpSem.Lem.lem_sorting]
program_sem [in EVMOpSem.evm]
program_as_natural_map [in EVMOpSem.evm]
program_of_lst [in EVMOpSem.evm]
program_default [in EVMOpSem.evm]
Prop_of_bool [in EVMOpSem.Lem.coqharness]
put_return_values [in EVMOpSem.evm]
put_return_values_aux [in EVMOpSem.evm]
Q
Qge_bool [in EVMOpSem.Lem.coqharness]Qgt_bool [in EVMOpSem.Lem.coqharness]
Qlt_bool [in EVMOpSem.Lem.coqharness]
quadrupleCompare [in EVMOpSem.Lem.lem_basic_classes]
quadrupleEqual [in EVMOpSem.Lem.lem_basic_classes]
quadrupleGreater [in EVMOpSem.Lem.lem_basic_classes]
quadrupleGreaterEq [in EVMOpSem.Lem.lem_basic_classes]
quadrupleLess [in EVMOpSem.Lem.lem_basic_classes]
quadrupleLessEq [in EVMOpSem.Lem.lem_basic_classes]
quintupleCompare [in EVMOpSem.Lem.lem_basic_classes]
quintupleEqual [in EVMOpSem.Lem.lem_basic_classes]
quintupleGreater [in EVMOpSem.Lem.lem_basic_classes]
quintupleGreaterEq [in EVMOpSem.Lem.lem_basic_classes]
quintupleLess [in EVMOpSem.Lem.lem_basic_classes]
quintupleLessEq [in EVMOpSem.Lem.lem_basic_classes]
R
rationalFromFrac [in EVMOpSem.Lem.lem_num]Rdown [in EVMOpSem.Lem.coqharness]
read_word_from_bytes [in EVMOpSem.evm]
read_n_bytes [in EVMOpSem.rlplem]
realFromFrac [in EVMOpSem.Lem.lem_num]
receipt_default [in EVMOpSem.block]
reflexiveTransitiveClosureOn [in EVMOpSem.Lem.lem_relation]
refund_selfdestruct [in EVMOpSem.block]
rel [in EVMOpSem.Lem.lem_relation]
relApply [in EVMOpSem.Lem.lem_relation]
relComp [in EVMOpSem.Lem.lem_relation]
relConverse [in EVMOpSem.Lem.lem_relation]
relDomain [in EVMOpSem.Lem.lem_relation]
relEq [in EVMOpSem.Lem.lem_relation]
relFromPred [in EVMOpSem.Lem.lem_relation]
relIdOn [in EVMOpSem.Lem.lem_relation]
relOver [in EVMOpSem.Lem.lem_relation]
relRange [in EVMOpSem.Lem.lem_relation]
relRestrict [in EVMOpSem.Lem.lem_relation]
relToPred [in EVMOpSem.Lem.lem_relation]
rel_default [in EVMOpSem.Lem.lem_relation]
rel_set_default [in EVMOpSem.Lem.lem_relation]
rel_set [in EVMOpSem.Lem.lem_relation]
rel_pred_default [in EVMOpSem.Lem.lem_relation]
rel_pred [in EVMOpSem.Lem.lem_relation]
removeMaybe [in EVMOpSem.Lem.lem_set]
replicate [in EVMOpSem.Lem.lem_list]
resizeBitSeq [in EVMOpSem.Lem.lem_word]
response_to_environment_default [in EVMOpSem.evm]
ret [in EVMOpSem.evm]
return_result_default [in EVMOpSem.evm]
reverseAppend [in EVMOpSem.Lem.lem_list]
reversePartition [in EVMOpSem.Lem.lem_list]
rev_apply [in EVMOpSem.Lem.lem_function]
Rge_bool [in EVMOpSem.Lem.coqharness]
Rgt_bool [in EVMOpSem.Lem.coqharness]
rho_pi [in EVMOpSem.keccak]
rho_pi_changes [in EVMOpSem.keccak]
rho_pi_inner [in EVMOpSem.keccak]
Rle_bool [in EVMOpSem.Lem.coqharness]
RLP [in EVMOpSem.rlplem]
RLP_address [in EVMOpSem.rlplem]
RLP_w256 [in EVMOpSem.rlplem]
RLP_nat [in EVMOpSem.rlplem]
Rlt_bool [in EVMOpSem.Lem.coqharness]
rotl64 [in EVMOpSem.keccak]
Rsclear [in EVMOpSem.evm]
rsiz [in EVMOpSem.keccak]
Rsuicide [in EVMOpSem.evm]
r_b [in EVMOpSem.rlplem]
S
sarith_inst_nums [in EVMOpSem.evm]sarith_inst_code [in EVMOpSem.evm]
sarith_inst_default [in EVMOpSem.evm]
sarith_inst_sind [in EVMOpSem.evm]
sarith_inst_rec [in EVMOpSem.evm]
sarith_inst_ind [in EVMOpSem.evm]
sarith_inst_rect [in EVMOpSem.evm]
set [in EVMOpSem.Lem.coqharness]
setf [in EVMOpSem.keccak]
setMapMaybe [in EVMOpSem.Lem.lem_set]
set_account_code [in EVMOpSem.block]
set_default [in EVMOpSem.Lem.coqharness]
set_case_by [in EVMOpSem.Lem.coqharness]
set_choose_dependent [in EVMOpSem.Lem.coqharness]
set_sigma [in EVMOpSem.Lem.coqharness]
set_to_list [in EVMOpSem.Lem.coqharness]
set_from_list [in EVMOpSem.Lem.coqharness]
set_proper_subset_by [in EVMOpSem.Lem.coqharness]
set_subset_by [in EVMOpSem.Lem.coqharness]
set_select_subset [in EVMOpSem.Lem.coqharness]
set_fold [in EVMOpSem.Lem.coqharness]
set_diff_by [in EVMOpSem.Lem.coqharness]
set_union_by [in EVMOpSem.Lem.coqharness]
set_inter_by [in EVMOpSem.Lem.coqharness]
set_for_all [in EVMOpSem.Lem.coqharness]
set_any [in EVMOpSem.Lem.coqharness]
set_cardinal [in EVMOpSem.Lem.coqharness]
set_choose [in EVMOpSem.Lem.coqharness]
set_add [in EVMOpSem.Lem.coqharness]
set_is_empty [in EVMOpSem.Lem.coqharness]
set_singleton [in EVMOpSem.Lem.coqharness]
set_empty [in EVMOpSem.Lem.coqharness]
set_member_by [in EVMOpSem.Lem.coqharness]
set_equal_by [in EVMOpSem.Lem.coqharness]
sextupleCompare [in EVMOpSem.Lem.lem_basic_classes]
sextupleEqual [in EVMOpSem.Lem.lem_basic_classes]
sextupleGreater [in EVMOpSem.Lem.lem_basic_classes]
sextupleGreaterEq [in EVMOpSem.Lem.lem_basic_classes]
sextupleLess [in EVMOpSem.Lem.lem_basic_classes]
sextupleLessEq [in EVMOpSem.Lem.lem_basic_classes]
sha3 [in EVMOpSem.evm]
sha3_update [in EVMOpSem.keccak]
signextend [in EVMOpSem.evm]
sintFromW256 [in EVMOpSem.evm]
size160 [in EVMOpSem.word160]
size256 [in EVMOpSem.word256]
size32 [in EVMOpSem.word32]
size64 [in EVMOpSem.word64]
split [in EVMOpSem.Lem.lem_set]
splitAt [in EVMOpSem.Lem.lem_list]
splitAtAcc [in EVMOpSem.Lem.lem_list]
splitMember [in EVMOpSem.Lem.lem_set]
splitWhile [in EVMOpSem.Lem.lem_list]
splitWhile_tr [in EVMOpSem.Lem.lem_list]
sstore [in EVMOpSem.evm]
stack_3_1_op [in EVMOpSem.evm]
stack_2_1_op [in EVMOpSem.evm]
stack_1_1_op [in EVMOpSem.evm]
stack_0_1_op [in EVMOpSem.evm]
stack_0_0_op [in EVMOpSem.evm]
stack_inst_numbers [in EVMOpSem.evm]
stack_inst_code [in EVMOpSem.evm]
stack_inst_default [in EVMOpSem.evm]
stack_inst_sind [in EVMOpSem.evm]
stack_inst_rec [in EVMOpSem.evm]
stack_inst_ind [in EVMOpSem.evm]
stack_inst_rect [in EVMOpSem.evm]
stack_numbers_default [in EVMOpSem.evm]
stack_numbers [in EVMOpSem.evm]
stack_hint_default [in EVMOpSem.block]
stack_hint_sind [in EVMOpSem.block]
stack_hint_rec [in EVMOpSem.block]
stack_hint_ind [in EVMOpSem.block]
stack_hint_rect [in EVMOpSem.block]
start_transaction [in EVMOpSem.block]
start_env [in EVMOpSem.block]
step [in EVMOpSem.block]
stop [in EVMOpSem.evm]
storage [in EVMOpSem.evm]
storage_inst_numbers [in EVMOpSem.evm]
storage_inst_code [in EVMOpSem.evm]
storage_inst_default [in EVMOpSem.evm]
storage_inst_sind [in EVMOpSem.evm]
storage_inst_rec [in EVMOpSem.evm]
storage_inst_ind [in EVMOpSem.evm]
storage_inst_rect [in EVMOpSem.evm]
storage_default [in EVMOpSem.evm]
store_word_memory [in EVMOpSem.evm]
store_byte_list_memory [in EVMOpSem.evm]
strict_if [in EVMOpSem.evm]
stringFromList [in EVMOpSem.Lem.lem_show]
stringFromListAux [in EVMOpSem.Lem.lem_show]
stringFromMaybe [in EVMOpSem.Lem.lem_show]
stringFromPair [in EVMOpSem.Lem.lem_show]
string_case [in EVMOpSem.Lem.lem_string]
string_default [in EVMOpSem.Lem.coqharness]
string_make_string [in EVMOpSem.Lem.coqharness]
string_from_char_list [in EVMOpSem.Lem.coqharness]
string_to_char_list [in EVMOpSem.Lem.coqharness]
string_equal [in EVMOpSem.Lem.coqharness]
subtract_gas [in EVMOpSem.evm]
sub_balance [in EVMOpSem.block]
suicide [in EVMOpSem.evm]
sum_default [in EVMOpSem.Lem.coqharness]
swap [in EVMOpSem.evm]
swap_inst_numbers [in EVMOpSem.evm]
swap_inst_code [in EVMOpSem.evm]
swap_inst_default [in EVMOpSem.evm]
swap_inst [in EVMOpSem.evm]
T
take [in EVMOpSem.Lem.lem_list]takeWhile [in EVMOpSem.Lem.lem_list]
theta [in EVMOpSem.keccak]
theta_t [in EVMOpSem.keccak]
theta1 [in EVMOpSem.keccak]
thirdComponentOfC [in EVMOpSem.evm]
transaction_default [in EVMOpSem.block]
transfer_balance [in EVMOpSem.block]
transitiveClosureAdd [in EVMOpSem.Lem.lem_relation]
tree_default [in EVMOpSem.rlplem]
tree_sind [in EVMOpSem.rlplem]
tree_rec [in EVMOpSem.rlplem]
tree_ind [in EVMOpSem.rlplem]
tree_rect [in EVMOpSem.rlplem]
tripleCompare [in EVMOpSem.Lem.lem_basic_classes]
tripleEqual [in EVMOpSem.Lem.lem_basic_classes]
tripleGreater [in EVMOpSem.Lem.lem_basic_classes]
tripleGreaterEq [in EVMOpSem.Lem.lem_basic_classes]
tripleLess [in EVMOpSem.Lem.lem_basic_classes]
tripleLessEq [in EVMOpSem.Lem.lem_basic_classes]
tr_result_default [in EVMOpSem.block]
tuple_equal_by [in EVMOpSem.Lem.coqharness]
two15 [in EVMOpSem.keccak]
two31 [in EVMOpSem.keccak]
txdatacost [in EVMOpSem.block]
U
uint [in EVMOpSem.evm]uncurry [in EVMOpSem.Lem.lem_function]
unit_default [in EVMOpSem.Lem.coqharness]
unsafe_structural_inequality [in EVMOpSem.Lem.lem_basic_classes]
unzip [in EVMOpSem.Lem.lem_list]
update [in EVMOpSem.Lem.lem_list]
update_byte [in EVMOpSem.keccak]
update_account_state [in EVMOpSem.evm]
update_balance [in EVMOpSem.evm]
update_nonce [in EVMOpSem.block]
update_call [in EVMOpSem.block]
update_return [in EVMOpSem.block]
update_world [in EVMOpSem.block]
V
variable_ctx_default [in EVMOpSem.evm]vctx_returned_bytes [in EVMOpSem.evm]
vctx_recipient [in EVMOpSem.evm]
vctx_next_instruction_default [in EVMOpSem.evm]
vctx_stack_default [in EVMOpSem.evm]
vctx_advance_pc [in EVMOpSem.evm]
vctx_next_instruction [in EVMOpSem.evm]
vctx_update_storage [in EVMOpSem.evm]
vctx_pop_stack [in EVMOpSem.evm]
vctx_update_from_world [in EVMOpSem.block]
W
withoutTransitiveEdges [in EVMOpSem.Lem.lem_relation]word_of_bytes [in EVMOpSem.keccak]
word_rcat_k [in EVMOpSem.keccak]
word_rsplit [in EVMOpSem.keccak]
word_rsplit_aux [in EVMOpSem.keccak]
word_exp [in EVMOpSem.evm]
word_rsplit256 [in EVMOpSem.evm]
word_rsplit160 [in EVMOpSem.rlplem]
word160Add [in EVMOpSem.word160]
word160Asr [in EVMOpSem.word160]
word160BinOp [in EVMOpSem.word160]
word160BinTest [in EVMOpSem.word160]
word160Division [in EVMOpSem.word160]
word160FromBoollist [in EVMOpSem.word160]
word160FromInt [in EVMOpSem.word160]
word160FromInteger [in EVMOpSem.word160]
word160FromNatural [in EVMOpSem.word160]
word160FromNumeral [in EVMOpSem.word160]
word160IntegerDivision [in EVMOpSem.word160]
word160Land [in EVMOpSem.word160]
word160Lnot [in EVMOpSem.word160]
word160Lor [in EVMOpSem.word160]
word160Lsl [in EVMOpSem.word160]
word160Lsr [in EVMOpSem.word160]
word160Lxor [in EVMOpSem.word160]
word160Max [in EVMOpSem.word160]
word160Min [in EVMOpSem.word160]
word160Minus [in EVMOpSem.word160]
word160Mult [in EVMOpSem.word160]
word160NatOp [in EVMOpSem.word160]
word160Negate [in EVMOpSem.word160]
word160Power [in EVMOpSem.word160]
word160Pred [in EVMOpSem.word160]
word160Remainder [in EVMOpSem.word160]
word160Succ [in EVMOpSem.word160]
word160ToInteger [in EVMOpSem.word160]
word160ToNatural [in EVMOpSem.word160]
word160UnaryOp [in EVMOpSem.word160]
word160_default [in EVMOpSem.word160]
word160_sind [in EVMOpSem.word160]
word160_rec [in EVMOpSem.word160]
word160_ind [in EVMOpSem.word160]
word160_rect [in EVMOpSem.word160]
word256Add [in EVMOpSem.word256]
word256Asr [in EVMOpSem.word256]
word256BinOp [in EVMOpSem.word256]
word256BinTest [in EVMOpSem.word256]
word256Division [in EVMOpSem.word256]
word256FromBoollist [in EVMOpSem.word256]
word256FromInt [in EVMOpSem.word256]
word256FromInteger [in EVMOpSem.word256]
word256FromNat [in EVMOpSem.word256]
word256FromNatural [in EVMOpSem.word256]
word256FromNumeral [in EVMOpSem.word256]
word256IntegerDivision [in EVMOpSem.word256]
word256Land [in EVMOpSem.word256]
word256Lnot [in EVMOpSem.word256]
word256Lor [in EVMOpSem.word256]
word256Lsl [in EVMOpSem.word256]
word256Lsr [in EVMOpSem.word256]
word256Lxor [in EVMOpSem.word256]
word256Max [in EVMOpSem.word256]
word256Min [in EVMOpSem.word256]
word256Minus [in EVMOpSem.word256]
word256Mult [in EVMOpSem.word256]
word256NatOp [in EVMOpSem.word256]
word256Negate [in EVMOpSem.word256]
word256Power [in EVMOpSem.word256]
word256Pred [in EVMOpSem.word256]
word256Remainder [in EVMOpSem.word256]
word256Succ [in EVMOpSem.word256]
word256ToNatural [in EVMOpSem.word256]
word256UGE [in EVMOpSem.word256]
word256UGT [in EVMOpSem.word256]
word256ULT [in EVMOpSem.word256]
word256UnaryOp [in EVMOpSem.word256]
word256_default [in EVMOpSem.helper]
word32Add [in EVMOpSem.word32]
word32Asr [in EVMOpSem.word32]
word32BinOp [in EVMOpSem.word32]
word32BinTest [in EVMOpSem.word32]
word32Division [in EVMOpSem.word32]
word32FromBoollist [in EVMOpSem.word32]
word32FromInt [in EVMOpSem.word32]
word32FromInteger [in EVMOpSem.word32]
word32FromNat [in EVMOpSem.word32]
word32FromNatural [in EVMOpSem.word32]
word32FromNumeral [in EVMOpSem.word32]
word32IntegerDivision [in EVMOpSem.word32]
word32Land [in EVMOpSem.word32]
word32Lnot [in EVMOpSem.word32]
word32Lor [in EVMOpSem.word32]
word32Lsl [in EVMOpSem.word32]
word32Lsr [in EVMOpSem.word32]
word32Lxor [in EVMOpSem.word32]
word32Max [in EVMOpSem.word32]
word32Min [in EVMOpSem.word32]
word32Minus [in EVMOpSem.word32]
word32Mult [in EVMOpSem.word32]
word32NatOp [in EVMOpSem.word32]
word32Negate [in EVMOpSem.word32]
word32Power [in EVMOpSem.word32]
word32Pred [in EVMOpSem.word32]
word32Remainder [in EVMOpSem.word32]
word32Succ [in EVMOpSem.word32]
word32ToInteger [in EVMOpSem.word32]
word32ToNatural [in EVMOpSem.word32]
word32UGE [in EVMOpSem.word32]
word32UGT [in EVMOpSem.word32]
word32ULT [in EVMOpSem.word32]
word32UnaryOp [in EVMOpSem.word32]
word32_default [in EVMOpSem.word32]
word32_sind [in EVMOpSem.word32]
word32_rec [in EVMOpSem.word32]
word32_ind [in EVMOpSem.word32]
word32_rect [in EVMOpSem.word32]
word4Add [in EVMOpSem.word4]
word4Asr [in EVMOpSem.word4]
word4BinOp [in EVMOpSem.word4]
word4BinTest [in EVMOpSem.word4]
word4Division [in EVMOpSem.word4]
word4FromBoollist [in EVMOpSem.word4]
word4FromInt [in EVMOpSem.word4]
word4FromInteger [in EVMOpSem.word4]
word4FromNat [in EVMOpSem.word4]
word4FromNatural [in EVMOpSem.word4]
word4FromNumeral [in EVMOpSem.word4]
word4IntegerDivision [in EVMOpSem.word4]
word4Land [in EVMOpSem.word4]
word4Lnot [in EVMOpSem.word4]
word4Lor [in EVMOpSem.word4]
word4Lsl [in EVMOpSem.word4]
word4Lsr [in EVMOpSem.word4]
word4Lxor [in EVMOpSem.word4]
word4Max [in EVMOpSem.word4]
word4Min [in EVMOpSem.word4]
word4Minus [in EVMOpSem.word4]
word4Mult [in EVMOpSem.word4]
word4NatOp [in EVMOpSem.word4]
word4Negate [in EVMOpSem.word4]
word4Power [in EVMOpSem.word4]
word4Pred [in EVMOpSem.word4]
word4Remainder [in EVMOpSem.word4]
word4Succ [in EVMOpSem.word4]
word4ToInt [in EVMOpSem.word4]
word4ToNat [in EVMOpSem.word4]
word4ToUInt [in EVMOpSem.word4]
word4UGT [in EVMOpSem.word4]
word4UnaryOp [in EVMOpSem.word4]
word4_default [in EVMOpSem.word4]
word4_sind [in EVMOpSem.word4]
word4_rec [in EVMOpSem.word4]
word4_ind [in EVMOpSem.word4]
word4_rect [in EVMOpSem.word4]
word64Add [in EVMOpSem.word64]
word64Asr [in EVMOpSem.word64]
word64BinOp [in EVMOpSem.word64]
word64BinTest [in EVMOpSem.word64]
word64Division [in EVMOpSem.word64]
word64FromBoollist [in EVMOpSem.word64]
word64FromInt [in EVMOpSem.word64]
word64FromInteger [in EVMOpSem.word64]
word64FromNat [in EVMOpSem.word64]
word64FromNatural [in EVMOpSem.word64]
word64FromNumeral [in EVMOpSem.word64]
word64IntegerDivision [in EVMOpSem.word64]
word64Land [in EVMOpSem.word64]
word64Lnot [in EVMOpSem.word64]
word64Lor [in EVMOpSem.word64]
word64Lsl [in EVMOpSem.word64]
word64Lsr [in EVMOpSem.word64]
word64Lxor [in EVMOpSem.word64]
word64Max [in EVMOpSem.word64]
word64Min [in EVMOpSem.word64]
word64Minus [in EVMOpSem.word64]
word64Mult [in EVMOpSem.word64]
word64NatOp [in EVMOpSem.word64]
word64Negate [in EVMOpSem.word64]
word64Power [in EVMOpSem.word64]
word64Pred [in EVMOpSem.word64]
word64Remainder [in EVMOpSem.word64]
word64Succ [in EVMOpSem.word64]
word64ToInteger [in EVMOpSem.word64]
word64ToNatural [in EVMOpSem.word64]
word64UGE [in EVMOpSem.word64]
word64UGT [in EVMOpSem.word64]
word64ULT [in EVMOpSem.word64]
word64UnaryOp [in EVMOpSem.word64]
word64_default [in EVMOpSem.word64]
word64_sind [in EVMOpSem.word64]
word64_rec [in EVMOpSem.word64]
word64_ind [in EVMOpSem.word64]
word64_rect [in EVMOpSem.word64]
word8Add [in EVMOpSem.word8]
word8Asr [in EVMOpSem.word8]
word8BinOp [in EVMOpSem.word8]
word8BinTest [in EVMOpSem.word8]
word8Division [in EVMOpSem.word8]
word8FromBoollist [in EVMOpSem.word8]
word8FromInt [in EVMOpSem.word8]
word8FromInteger [in EVMOpSem.word8]
word8FromNat [in EVMOpSem.word8]
word8FromNatural [in EVMOpSem.word8]
word8FromNumeral [in EVMOpSem.word8]
word8IntegerDivision [in EVMOpSem.word8]
word8Land [in EVMOpSem.word8]
word8Lnot [in EVMOpSem.word8]
word8Lor [in EVMOpSem.word8]
word8Lsl [in EVMOpSem.word8]
word8Lsr [in EVMOpSem.word8]
word8Lxor [in EVMOpSem.word8]
word8Max [in EVMOpSem.word8]
word8Min [in EVMOpSem.word8]
word8Minus [in EVMOpSem.word8]
word8Mult [in EVMOpSem.word8]
word8NatOp [in EVMOpSem.word8]
word8Negate [in EVMOpSem.word8]
word8Power [in EVMOpSem.word8]
word8Pred [in EVMOpSem.word8]
word8Remainder [in EVMOpSem.word8]
word8Succ [in EVMOpSem.word8]
word8ToInt [in EVMOpSem.word8]
word8ToNat [in EVMOpSem.word8]
word8ToNatural [in EVMOpSem.word8]
word8ToUInt [in EVMOpSem.word8]
word8UGT [in EVMOpSem.word8]
word8UnaryOp [in EVMOpSem.word8]
word8_default [in EVMOpSem.word8]
word8_sind [in EVMOpSem.word8]
word8_rec [in EVMOpSem.word8]
word8_ind [in EVMOpSem.word8]
word8_rect [in EVMOpSem.word8]
word8_to_word64 [in EVMOpSem.keccak]
world_state_default [in EVMOpSem.block]
world_state [in EVMOpSem.block]
w160Compare [in EVMOpSem.word160]
w160Eq [in EVMOpSem.word160]
w160Greater [in EVMOpSem.word160]
w160GreaterEqual [in EVMOpSem.word160]
w160Less [in EVMOpSem.word160]
w160LessEqual [in EVMOpSem.word160]
w160_to_bs [in EVMOpSem.word160]
w256 [in EVMOpSem.keccak]
w256Compare [in EVMOpSem.word256]
w256Eq [in EVMOpSem.word256]
w256Greater [in EVMOpSem.word256]
w256GreaterEqual [in EVMOpSem.word256]
w256Less [in EVMOpSem.word256]
w256LessEqual [in EVMOpSem.word256]
w256_default [in EVMOpSem.keccak]
w256_to_byte [in EVMOpSem.evm]
w256_to_address [in EVMOpSem.evm]
w256_of_bl [in EVMOpSem.evm]
w32Compare [in EVMOpSem.word32]
w32Eq [in EVMOpSem.word32]
w32Greater [in EVMOpSem.word32]
w32GreaterEqual [in EVMOpSem.word32]
w32Less [in EVMOpSem.word32]
w32LessEqual [in EVMOpSem.word32]
w32_to_bs [in EVMOpSem.word32]
w4Compare [in EVMOpSem.word4]
w4Eq [in EVMOpSem.word4]
w4Greater [in EVMOpSem.word4]
w4GreaterEqual [in EVMOpSem.word4]
w4Less [in EVMOpSem.word4]
w4LessEqual [in EVMOpSem.word4]
w4_to_bs [in EVMOpSem.word4]
w64Compare [in EVMOpSem.word64]
w64Eq [in EVMOpSem.word64]
w64Greater [in EVMOpSem.word64]
w64GreaterEqual [in EVMOpSem.word64]
w64Less [in EVMOpSem.word64]
w64LessEqual [in EVMOpSem.word64]
w64_to_bs [in EVMOpSem.word64]
w8Compare [in EVMOpSem.word8]
w8Eq [in EVMOpSem.word8]
w8Greater [in EVMOpSem.word8]
w8GreaterEqual [in EVMOpSem.word8]
w8Less [in EVMOpSem.word8]
w8LessEqual [in EVMOpSem.word8]
w8_to_bs [in EVMOpSem.word8]
Z
zip [in EVMOpSem.Lem.lem_list]Zmod2 [in EVMOpSem.Zdigits]
Z_default [in EVMOpSem.Lem.coqharness]
Record Index
A
account_state [in EVMOpSem.evm]B
block_info [in EVMOpSem.evm]block_account [in EVMOpSem.block]
C
call_arguments [in EVMOpSem.evm]call_env [in EVMOpSem.evm]
constant_ctx [in EVMOpSem.evm]
create_arguments [in EVMOpSem.evm]
E
Eq [in EVMOpSem.Lem.lem_basic_classes]G
global [in EVMOpSem.block]L
log_entry [in EVMOpSem.evm]M
MapKeyType [in EVMOpSem.Lem.lem_map]N
NumAbs [in EVMOpSem.Lem.lem_num]NumAdd [in EVMOpSem.Lem.lem_num]
NumDivision [in EVMOpSem.Lem.lem_num]
NumIntegerDivision [in EVMOpSem.Lem.lem_num]
NumMinus [in EVMOpSem.Lem.lem_num]
NumMult [in EVMOpSem.Lem.lem_num]
NumNegate [in EVMOpSem.Lem.lem_num]
NumPow [in EVMOpSem.Lem.lem_num]
NumPred [in EVMOpSem.Lem.lem_num]
NumRemainder [in EVMOpSem.Lem.lem_num]
NumSucc [in EVMOpSem.Lem.lem_num]
O
Ord [in EVMOpSem.Lem.lem_basic_classes]OrdMaxMin [in EVMOpSem.Lem.lem_basic_classes]
P
program [in EVMOpSem.evm]R
receipt [in EVMOpSem.block]response_to_environment [in EVMOpSem.evm]
return_result [in EVMOpSem.evm]
S
SetType [in EVMOpSem.Lem.lem_basic_classes]Show [in EVMOpSem.Lem.lem_show]
T
transaction [in EVMOpSem.block]tr_result [in EVMOpSem.block]
V
variable_ctx [in EVMOpSem.evm]W
WordAnd [in EVMOpSem.Lem.lem_word]WordAsr [in EVMOpSem.Lem.lem_word]
WordLsl [in EVMOpSem.Lem.lem_word]
WordLsr [in EVMOpSem.Lem.lem_word]
WordNot [in EVMOpSem.Lem.lem_word]
WordOr [in EVMOpSem.Lem.lem_word]
WordXor [in EVMOpSem.Lem.lem_word]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1848 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (116 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (120 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (121 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (327 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1017 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (40 entries) |
This page has been generated by coqdoc