New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Get rid of duplicated lemmas for commutative operations #315

Open

hjorthjort opened this issue Apr 20, 2020 · 0 comments

Labels

enhancement good first issue

Contributor

hjorthjort commented Apr 20, 2020

KEVM uses the following lemmas to push symbolic values to the left in commutative-associative operations: https://github.com/kframework/evm-semantics/blob/master/tests/specs/lemmas.k#L290

We should add the same or similar lemmas, and go over our lemmas file and look for other cases where this can be simplified.

hjorthjort added enhancement good first issue labels

hjorthjort mentioned this issue

Wrc20 balance fixes #310

Merged

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment