Skip to content
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.

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

Use set variables for \ceil simplification rules? #729

ttuegel opened this issue Jun 11, 2019 · 4 comments

Use set variables for \ceil simplification rules? #729

ttuegel opened this issue Jun 11, 2019 · 4 comments


Copy link

ttuegel commented Jun 11, 2019

In the frontend's domains.k, we define simplification rules such as:

   * Definability conditions for _/Int_ and _%Int_

  rule #Ceil(I1:Int /Int I2:Int) => {(I2 =/=Int 0) #Equals true} [anywhere]
  rule #Ceil(I1:Int %Int I2:Int) => {(I2 =/=Int 0) #Equals true} [anywhere]

This causes an error in the backend in contexts where one of the arguments of /Int or %Int may, itself, be undefined, for example in the expression (X /Int Y) /Int Z. Applying one of these simplification rules generates a remainder because we cannot unconditionally unify I1:Int with X /Int Y, which may not be defined. The backend throws an error when simplification rules produce a remainder (and rightly so).

I would propose that we express these simplification rules using set variables,

  rule #Ceil(#I1:Int /Int #I2:Int) =>
    {(#I2 =/=Int 0) #Equals true} #And #Ceil(#I1) #And #Ceil(#I2) 

which is more verbose, but does not create any remainders. @traiansf, you have worked on our set variables support in the past; can the frontend support something like this? Or, can you suggest another way to handle this problem?

Copy link

I think the frontend doesn't currently support a variable name to start with #.
Until that restriction is relaxed, we might be able to work around it using an attribute, say setVariables which has as argument the list of variables which should be marked as set variables (or, if no variable is specified, then we could default to all vars being set variables. Then the frontend could prefix them with # when generating KORE.

@dwightguth what do you think? does this seem reasonable? would it be easier to add support for set variables directly in the K Frontend parser?

@ttuegel ttuegel added this to To do in Iteration via automation Jun 20, 2019
Copy link
Contributor Author

ttuegel commented Jun 20, 2019

This is one of only a few issues blocking our progress on the KEVM single-opcode proofs, and it seems relatively simple, so I would like to prioritize it for the next iteration.

Copy link
Contributor Author

ttuegel commented Jun 21, 2019

There is another way we could handle this in the backend which I want to consider. If we have a symbol f(x₁, …), that symbol is only defined if its arguments are defined, i.e.

⌈f(φ₁, …)⌉ = ⌈f(φ₁, …)⌉ ∧ ⌈φ₁⌉ ∧ …

The backend could produce the defined-argument conditions ⌈φ₁⌉ ∧ … itself before applying any simplification rules. This would prevent the formation of the remainders which are causing the error.

Copy link
Contributor Author

ttuegel commented Jun 21, 2019

@ehildenb The EVM opcode proofs which are affected by this are:

  • BYTE
  • LOG
  • MOD
  • SMOD

@eviefp eviefp moved this from To do to In progress in Iteration Jun 25, 2019
@ttuegel ttuegel added next and removed next labels Jul 30, 2019
@ttuegel ttuegel closed this as completed Aug 12, 2019
Iteration automation moved this from In progress to Done Aug 12, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
None yet
No open projects

No branches or pull requests

2 participants