kframework / k-legacy

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

add power-modulo operator to UIUC K #2372

Closed dwightguth closed 6 years ago

dwightguth commented 6 years ago

This is needed to execute the power-modulo operation in the modexp precompiled contract in the EVM semantics.

dwightguth commented 6 years ago

when we need it we can just represent it with a macro in the prelude that does power and modulo directly. but until we verify contracts that call precompiled contracts it won't be an issue.