Ceil simplifier in booster

[goodlyrottenapple]

The use of #Ceil in the old backend stems from partial functions in the semantics. The three main issues with the design of partiality checking in the old backend are:

• fully dynamic checks which take a lot of time
• ceil computation is part of the general simplification engine which makes it difficult to debug and collect statistics on
• ceil terms are mixed in with predicates and configurations

As a result of the last two points especially, we want to implement the ceil/definedness checker to be a (somewhat) separate pass during rewriting, which should make it easier to scrutinise and maintain. We also want to shift to a partially static definedness analysis (already implemented for rewrite rules in runtimeverification/hs-backend-booster#402), with the hope that a semantics writer could eventually make the ceil checks fully static. What we mean by this is that instead of computing the definedness for every instance of a partial function call, we could instead insert the definedness conditions of partial functions at call sities in rewrite rules. For example, given the rule

rule foo(X) => 10 mod X

and given the definedness condition for A mod B being B > 0, the static checker would transform the above rule into

rule foo(X) => 10 mod X requires X > 0

The goal of making the dynamic ceil check a separate pass is more difficult, since the way we will compute #Ceil for a given partial function will either be to:

1. check for a ceil rule for the particular function, e.g. #Ceil(X mod Y) = Y > 0. If this rule exists, we continue checking whether the predicate Y > 0 holds.
2. if no user specified ceil rule exists, we will have to apply function evaluation/simplification to the partial function and then either
   1. fail, because we cannot apply any function rules (note: this might be tricky, especially with some inputs to the function being symbolic
   2. apply the function and check if the rewritten term contains any partial functions. If not, the original term under #Ceil is defined, otherwise, recursively check definedness of all new partial function calls.

See runtimeverification/haskell-backend#3772 for a discussion on how to refactor the different simplification/evaluation procedures in the booster in such a way as to avoid one giant mutually recursive ball of functions (as is the case in the old backend).

We already internalise and store ceil conditions separately from the configuration and the predicates, and once the old backend is removed, the user should never receive a #Ceil predicate as a response. Instead, we should augment the RPC types with a suitable set of errors, indicating that a partial function application could not be determined to be preserving definedness.

[ehildenb]

If we're adding boolean requires clauses by default, then we're changing the users transition system, which I don't think is a good idea. I think better is:

• Warn the user about the extra condition that must be checked for the given rule at kompile time, maybe they just forgot to add that extra condition?
• Store that particular condition separately than the requires clause when loading the rule, ideally store it as the original Ceil condition, which then can be discharged dynamically before attempting the side-condition evaluation. We would have to have yet another separate bunch of Ceil conditions associated with any potential non-defindeness in the requires clause as well.

[goodlyrottenapple]

I think storing the computed condition separately is probably the way to go. I'm not sure the user should be required to add this condition manually. This could result in rules which contain partial functions on the RHS to have huge custom written requires clauses which manually copy the ceil conditions for that partial symbol.

Computing these conditions at load time and then storing them separately would also produce better error messages, If the evaluation of such condition is indeterminate or false. I.e. rather than saying the rule did not apply, we return something along the lines of, the rule is applicable but we could not determine whether definiteness would be preserved or worse, this rule somehow leads to an undefined state.