kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

bn128 elliptic curve builtins in k #2350

Closed dwightguth closed 6 years ago

dwightguth commented 6 years ago

For the EVM semantics of Byzantium.

daejunpark commented 6 years ago

I'm ok to merge this. I haven't carefully read the actual implementation of the fields and curves, but it should be ok to add it for now as a builtin, since we're not going to symbolically reason about the crypto algorithms in the near future.

daejunpark commented 6 years ago

@bmmoore Are you reviewing (or will you review) this? Otherwise, I'd like to merge this.