Use set variables for \ceil simplification rules?

[ttuegel]

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) 
    [anywhere]

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?

[traiansf]

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]

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.

[ttuegel]

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.

[ttuegel]

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

• ADDMOD
• BYTE
• LOG
• MLOAD
• MOD
• MSTORE
• MSTORE8
• MULMOD
• SIGNEXTEND
• SMOD