Skip to content
/ forves2 Public

FORVES 2.0: FORmally VErified EVM optimizationS -- leveraging FORVES to inter-block optimizations

License

AGPL-3.0, GPL-3.0 licenses found

Licenses found

AGPL-3.0
LICENSE
GPL-3.0
COPYING
1 star 0 forks Branches Tags Activity
Star
Notifications You must be signed in to change notification settings

costa-group/forves2

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

109 Commits
ocaml_interface
ocaml_interface
 
 
optimizations
optimizations
 
 
.gitignore
.gitignore
 
 
COPYING
COPYING
 
 
LICENSE
LICENSE
 
 
README.md
README.md
 
 
_CoqProject
_CoqProject
 
 
block_equiv_checker.v
block_equiv_checker.v
 
 
block_equiv_checker_dbg.v
block_equiv_checker_dbg.v
 
 
block_equiv_checker_soundness.v
block_equiv_checker_soundness.v
 
 
concrete_interpreter.v
concrete_interpreter.v
 
 
constants.v
constants.v
 
 
constraints.v
constraints.v
 
 
context.v
context.v
 
 
context_facts.v
context_facts.v
 
 
eval_common.v
eval_common.v
 
 
execution_state.v
execution_state.v
 
 
execution_state_facts.v
execution_state_facts.v
 
 
extract_ocaml.v
extract_ocaml.v
 
 
memory_cmp_impl.v
memory_cmp_impl.v
 
 
memory_cmp_impl_soundness.v
memory_cmp_impl_soundness.v
 
 
memory_ops_solvers.v
memory_ops_solvers.v
 
 
memory_ops_solvers_impl.v
memory_ops_solvers_impl.v
 
 
memory_ops_solvers_impl_soundness.v
memory_ops_solvers_impl_soundness.v
 
 
memory_ops_solvers_impl_soundness_misc.v
memory_ops_solvers_impl_soundness_misc.v
 
 
misc.v
misc.v
 
 
octagon.v
octagon.v
 
 
opt_pipelines.v
opt_pipelines.v
 
 
optimizations_common.v
optimizations_common.v
 
 
optimizations_def.v
optimizations_def.v
 
 
parser.v
parser.v
 
 
program.v
program.v
 
 
sha3.v
sha3.v
 
 
sha3_cmp_impl.v
sha3_cmp_impl.v
 
 
sha3_cmp_impl_soundness.v
sha3_cmp_impl_soundness.v
 
 
sstack_val_cmp_impl.v
sstack_val_cmp_impl.v
 
 
sstack_val_cmp_impl_soundness.v
sstack_val_cmp_impl_soundness.v
 
 
stack_operation_instructions.v
stack_operation_instructions.v
 
 
storage_cmp_impl.v
storage_cmp_impl.v
 
 
storage_cmp_impl_soundness.v
storage_cmp_impl_soundness.v
 
 
storage_ops_solvers.v
storage_ops_solvers.v
 
 
storage_ops_solvers_impl.v
storage_ops_solvers_impl.v
 
 
storage_ops_solvers_impl_soundness.v
storage_ops_solvers_impl_soundness.v
 
 
symbolic_execution.v
symbolic_execution.v
 
 
symbolic_execution_soundness.v
symbolic_execution_soundness.v
 
 
symbolic_state.v
symbolic_state.v
 
 
symbolic_state_cmp.v
symbolic_state_cmp.v
 
 
symbolic_state_cmp_impl.v
symbolic_state_cmp_impl.v
 
 
symbolic_state_cmp_impl_soundness.v
symbolic_state_cmp_impl_soundness.v
 
 
symbolic_state_dec.v
symbolic_state_dec.v
 
 
symbolic_state_eval.v
symbolic_state_eval.v
 
 
symbolic_state_eval_facts.v
symbolic_state_eval_facts.v
 
 
tests.v
tests.v
 
 
tools_types.v
tools_types.v
 
 
valid_symbolic_state.v
valid_symbolic_state.v
 
 

Repository files navigation

forves2

FORVES 2.0: FORmally VErified EVM optimizationS -- leveraging FORVES to inter-block optimizations

Compilation

This project is developed using Coq 8.16.1 and requires the package coq-bbv version 1.4. It can be compiled with the following commands:

$ coq_makefile -f _CoqProject -o Makefile
$ make

License

The code is licensed under the GNU General Public License 3.0, also included in our repository in the COPYING file.

About

FORVES 2.0: FORmally VErified EVM optimizationS -- leveraging FORVES to inter-block optimizations

Resources

Readme

License

AGPL-3.0, GPL-3.0 licenses found

Licenses found

AGPL-3.0
LICENSE
GPL-3.0
COPYING
Activity
Custom properties

Stars

1 star

Watchers

3 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Contributors 3

  •  
  •  
  •  

Languages