_CoqProject

-R . FORVES2

octagon.v
context.v
context_facts.v
constraints.v

constants.v
program.v
stack_operation_instructions.v
sha3.v
execution_state.v
execution_state_facts.v
concrete_interpreter.v

symbolic_state.v
symbolic_state_dec.v
valid_symbolic_state.v
misc.v
eval_common.v
symbolic_state_eval.v
symbolic_state_eval_facts.v

storage_ops_solvers.v
storage_ops_solvers_impl.v
storage_ops_solvers_impl_soundness.v

memory_ops_solvers.v
memory_ops_solvers_impl.v
memory_ops_solvers_impl_soundness_misc.v
memory_ops_solvers_impl_soundness.v

symbolic_execution.v
symbolic_execution_soundness.v

symbolic_state_cmp.v
symbolic_state_cmp_impl.v
symbolic_state_cmp_impl_soundness.v

sstack_val_cmp_impl.v
sstack_val_cmp_impl_soundness.v

memory_cmp_impl.v
memory_cmp_impl_soundness.v

storage_cmp_impl.v
storage_cmp_impl_soundness.v

sha3_cmp_impl.v
sha3_cmp_impl_soundness.v

optimizations_common.v
optimizations_def.v

optimizations/add_zero.v
optimizations/eval.v
optimizations/not_not.v
optimizations/and_and.v
optimizations/and_origin.v
optimizations/mul_shl.v
optimizations/div_shl.v
optimizations/shr_zero_x.v
optimizations/shr_x_zero.v
optimizations/eq_zero.v
optimizations/sub_x_x.v
optimizations/and_zero.v
optimizations/div_one.v
optimizations/lt_x_one.v
optimizations/gt_one_x.v
optimizations/and_address.v
optimizations/mul_one.v
optimizations/iszero_gt.v
optimizations/eq_iszero.v
optimizations/and_caller.v
optimizations/iszero3.v
optimizations/add_sub.v
optimizations/shl_zero_x.v
optimizations/sub_zero.v
optimizations/shl_x_zero.v
optimizations/mul_zero.v
optimizations/div_x_x.v
optimizations/div_zero.v
optimizations/mod_one.v
optimizations/mod_zero.v
optimizations/mod_x_x.v
optimizations/exp_x_zero.v
optimizations/exp_x_one.v
optimizations/exp_one_x.v
optimizations/exp_zero_x.v
optimizations/exp_two_x.v
optimizations/gt_zero_x.v
optimizations/gt_x_x.v
optimizations/lt_x_zero.v
optimizations/lt_x_x.v
optimizations/eq_x_x.v
optimizations/iszero_sub.v
optimizations/iszero_lt.v
optimizations/iszero_xor.v
optimizations/iszero2_gt.v
optimizations/iszero2_lt.v
optimizations/iszero2_eq.v
optimizations/xor_x_x.v
optimizations/xor_zero.v
optimizations/xor_xor.v
optimizations/or_or.v
optimizations/or_and.v
optimizations/and_or.v
optimizations/and_not.v
optimizations/or_not.v
optimizations/or_x_x.v
optimizations/and_x_x.v
optimizations/or_zero.v
optimizations/or_ffff.v
optimizations/and_ffff.v
optimizations/and_coinbase.v
optimizations/balance_address.v
optimizations/slt_x_x.v
optimizations/sgt_x_x.v
optimizations/mem_solver.v
optimizations/strg_solver.v
optimizations/jumpi_neq.v
optimizations/lt_ctx.v
optimizations/gt_ctx.v
optimizations/eq_ctx.v

opt_pipelines.v

tools_types.v
block_equiv_checker.v
block_equiv_checker_dbg.v
block_equiv_checker_soundness.v

parser.v
extract_ocaml.v