Skip to content

Hash functions used in EVM implemented in Coq.

License

Notifications You must be signed in to change notification settings

formal-land/coq-evm

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

coq-evm

This might or might not become a full Ethereum Virtual Machine in Coq someday.

Right now you can have the hash functions:

- Keccak-256
- SHA256
- RIPEMD160
- BLAKE2b (F function only)

All those functions use native Coq integers for speed. All of them are tested against their Go implementations.

Checking

./configure    # just does coq_makefile
make

Testing

This needs Go.

cd test
./configure    # gives a warning but it's OK
make

About

Hash functions used in EVM implemented in Coq.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Coq 97.0%
  • Go 3.0%