Ceil simplifier in booster

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.

Start by reading runtimeverification/haskell-backend#3772 and the partially static definedness analysis in runtimeverification/hs-backend-booster#402. The issue provides no file or test entry point, so first identify the booster rewriting and RPC components involved. Done means ceil checking is a separate rewriting pass with the intended definedness behavior and suitable errors instead of exposing #Ceil predicates.