NOTE: This issue description is a draft, WIP

Introduction

Right now, the simplifier has reached a point where the old design clashes with newer features and it also no longer reflects the practical needs of the simplification expected to be done by the Haskell backend. Basically, the old design is too general and has acquired a lot of technical debt along the years.

What I mean by too general: initially, all Kore patterns were represented in the same way, and the simplifier strove to be able to simplify any arbitrary Kore pattern. It was also decided that each pattern connective has its own simplifier, which would attempt to simplify it as much as possible. These two approaches have introduced cyclic dependencies throughout the simplifier code, making it hard to understand and maintain. Newer features have broken many of the simplifier's initial assumptions, introducing even more brittle behavior into the code.

The following new design starts from the current design, together with additions which follow from previous refactorings and restructurings of parts of the simplifier code.

Representing Kore patterns

The simplifier simplifies configurations. A configuration is a Kore pattern which has the following structure: it is a conjunction between a term and a condition. I have noticed K users refer to the condition part as the side condition, because it usually comes from the side condition (the requires) of the claim which is being proven.

Recall that in Matching Logic, a predicate is a pattern which is semantically either \\top or \\bottom. We know that some connectives will necessarily construct predicates (\\ceil, \\equals etc.).

The backend distinguishes between arbitrary predicates and the more specialized kind of predicate, substitutions. Therefore, we consider conditions to be conjunctions of predicates and substitutions.

A term is a pattern which, in theory, can be any arbitrary Kore pattern. In practice, however, I believe this pattern can be constrained to a subset of Kore patterns. I am basing this on the observation that the code which does term simplification does not attempt to handle any cases where the term is constructed using predicate-making connectives (this is a fairly recent change). Therefore, it seems like these terms should be restricted as described in the following issue: https://github.com/kframework/kore/issues/2640.

TODO: change above will also result in issues with current Predicate representation, where there is a "predicate connective" over a Predicate (currently it only admits TermLike).

Some ideas about the simplifier:

Many small and simple passes which only do one thing (eg. "push #Or down" or "pull #And up")
Call many of these passes in a specific sequence to achieve a larger goal.
Take advantage of any term/problem structure you reasonably can (don't try to make general-case simplifiers).
Bottom up traversals are more general, but often less efficient for many simplification passes. For example, a pass which "pushes #And down" would be much slower on a bottom-up traversal than a top-down one. We should be using the correct traversal in each case.
Note that any existing passes which are non-looping (or can be broken into a looping and non-looping version) can be used directly.

One approach:

Implement new simplifier which has the properties above ^^^.
Call the new simplifier before calling the old simplifier (so we still get full simplification, but we exercise the new faster simplifier first).
Gradually make the new simplifier able to handle more of the cases that it was delegating to the old simplifier.
Remove the old simplifer when it's no longer needed.

Representing simplification:

Simple imperative description of the passes to be performed. There must be an inspectable and understandable presentation of the simplification procedure, because it's important for users of the Haskell backend to have a good mental model of the simplifier (because it's an automated prover).
Natural storage data-structure is some ADT like this (note this is still an imperative description):

data SimplifierPass = Seq SimplifierPass SimplifierPass | Repeat Int SimplifierPass | ....

I'm not up to date with the current Haskell backend architecture, but one interesting issue is that, in order to simplify terms, one needs to simplify predicates, and, in order to simplify predicates, one needs to simplify terms. That leads to natural ways of looping, e.g. if one does

rule f(X) => 0 requires f(X) == 1
rule f(X) => 2 [owise]

which is, I think, valid mathematically, one will get a loop. I'm not sure if the backend should be concerned about this or not.

Regardless, if the symbol application simplifier needs the the predicate simplifier and the predicate simplifier needs the application simplifier, it would be nice to have an architecture where those two are decoupled. I think that the idea below can be generalized to also handle that, but I'm not sure it's worth the trouble.

Anyway, let me add here what I also said on Slack, though with more details:

One approach is to keep the current simplifiers (split, perhaps, into predicate and term simplifiers) and the current term simplifier loop, let them work as they do right now, except for two things:

Whenever a simplifier calls another simplifier (it's easier to provide an example for predicates, e.g. the #Equals simplifier may call the #Ceil one), or when it calls itself for something that's different enough from the start expression (e.g. when f(x) is evaluated to g(x) and now we want to evaluate g(x)), use instead an unsimplified expression, return that, and let the term simplifier loop on it. As an example, the Equals simplifier would take a == (b or c) and would return (not ceil(a) and not ceil(b) and not ceil(c)) or (ceil(a) and (ceil(b) or ceil(c)) and (ceil(b) => a == b) and (ceil(c) => a == c)) as an unsimplified term
When marking things as simplified, either let the main simplifier loop do that (i.e. when the simplified term is the same as the starting term), or take into account the previous bullet in the list.

There are at least two possible issues with this approach:

Performance loss due to going through the main loop instead of directly calling simplifiers
New reasons for looping, e.g. when something can be simplified as a -> b -> a -> b ..., a simplifier receiving a may decide that b is simplified enough and return that, while the main simplifier loop might not have enough information to know that it should stop at b.

By listing the issues above (which were, IIRC, true in the past, but may not be so with the current code) I did not mean that one should not try this approach, I just meant that one should keep them in mind if one is trying it.

Thanks @virgil-serbanuta, you're right about the function application loop, which I had forgotten about. The term simplifier, when encountering applications, will attempt to apply equations, and that procedure has to call the condition simplifier when checking requirements (concretely, this is the current implementation).

That's a good example where I think looping is inevitable. My issue with the current implementation is that, it's looping there in an opaque way. You have to really know the simplifier code in order to quickly find and mentally visualize this loop. I think we need to find a way to make these necessary loops explicit and obvious at the top level.

How are simplifiers implemented for other automatic provers? I know the underlying logic will be different, but there must be common problems with well-researched algorithmic solutions.

I am only slightly familiar with Maude, but I remember it has conditional equations which are probably pretty similar to the ones in K, maybe they have some literature on the algorithm used to apply them.

I do not think that looping is inevitable. We can do a loop like:

while changed:
    callTermSimplifier()
    callPredicateSimplifier()

instead. And then build callTermSimplifier() and callPredicateSimplifier() so that they can do their own independent work without calling each other. We should really avoid having simplifier call each other. For example, if the #And simplifier needs the #Not simplifier, then we should just call the #Not simplificatino ahead of time (so that its work is done), then call the #And simplifier. So each pass is valid on its own, but then putting them together you still get valid passes and each one only needs to traverse the term once.

What we definitely want to avoid is "we're doing a traversal to do #And simplification, and then we discover we need #Not simplification, so we re-traverse the term with the #Not simplifier in the middle of the #And simplification loop." This is very expensive, anything where we're enabling re-traversing a term inside another term traversal will necessarily be asymptotically expensive.

Better to have a bunch of individual passes which are guaranteed to only traverse the term once, and then call those in the needed cycle to achieve the overall goal. That way the performance characteristics of each individual pass (and thus the whole algorithm) is well-understood and simple.

I think that will avoid the loop but it won't avoid the dependency term simplifier -> predicate simplifier. Basically, to evaluate terms, you must evaluate predicates. Virgil's example illustrates this: the term simplifier must evaluate f(X) by attempting to apply one of its function definition rules. In order to check if it can apply a rule, it must call the predicate simplifier to evaluate the requires condition.

The reverse dependency can be unpacked as you said: remove the calls to the term simplifier from the predicate simplifier, add a separate "simplify only predicate's subterms" procedure which is called beforehand. I assume it makes most sense to first evaluate the terms inside a predicate, and then attempt to simplify the predicate, but maybe I'm wrong.

I'm getting tired, that won't avoid the loop because of the first dependency 🤦 , the second needs to be "packed together" in order for the first to do actual work. So, yeah, I'm pretty sure the looping is inevitable here. I'll have to revisit this discussion tomorrow after some rest.

I think we should write down these ideas more algorithmically, because it's hard to understand what's going on for me. I think I'm understanding the issue with the term simplifier needing to call the predicate simplifier.

Here's my attempt at a psuedo-code algorithm for "simplifying the constrained term after a rewrite step":

// rules map is from: RULE_LHS_TOP_SYMBOL -> [ RULE ]
// So we can lookup the list of applicable rules for a given symbol.
// functionalRules :: RULE_LHS_TOP_SYMBOL -> [RULE]
functionalRules     = functionRuleMap(semantics)
simplificationRules = simplificationRuleMap(semantics)

// Given a term and ruleMap, returns the term with at most one of the rMap rules applied to it
def rewriteAtTopWithRules(term, rMap, matching = False):
     applications = []
     for rule in rMap[term.topSymbol]:
         newTerm = applyRule(rule, term, matching = matching)    //  <-----      can trigger a call to predicate simplifier
         if newTerm is not None:
             applications.append(newTerm)
     if len(applications) != 1:
         return term
     else:
         return applications[0]

// Given a term and a rule map, return the term with the rules in the rule map applied _anywhere_ they can in the term.
def rewriteWithRules(term, rMap, matching = False):
    // traverseBottomUp visits every node in a term (bottom up) and applies the given function to it
    return traverseBottomUp(term, lambda t: rewriteAtTopWithRules(t, rMap, matching = matching))

def simplifyConstrainedTerm(constrainedTerm):
    (config, constraint)      = splitConfigAndConstraint(constrainedTerm)
    constraint                = simplifyPredicate(constraint)
    simplifiedConstrainedTerm = joinConfigAndConstraint(config, constraint)
    while true:
       newConstrainedTerm = simplifiedConstrainedTerm
       newConstrainedTerm = rewriteWithRules(newConstrainedTerm, functionalRules)
       newConstrainedTerm = rewriteWithRules(newConstrainedTerm, simplificationRules, matching = True)
       if newConstrainedTerm == simplifiedConstrainedTerm:
           break
       simplifiedConstrainedTerm = newConstrainedTerm
    return simplifiedConstrainedTerm

This algorithm doesn't take into account priorities, but I guess we can think about that later for the moment (by just having separate rulemap buckets for each priority level).

Can we have the actual algorithm (as it's implemented in the code now) also translated into psuedo-code like this (or however you like) so we can inspect it @ana-pantilie ? Then we can suggest more concrete changes to it. I also think it would help us all better understand how the current simplifier works.

I think that none of the approaches listed above would really avoid loops, though one could probably stop after a number of iterations or something (which just moves the problem somewhere else; arguably, that somewhere else is easier to debug).

I'll just mention an idea that is not that practical, but it's too interesting to not say anything about it. Also, maybe it's more practical than it seems to me.

We could implement any bottom-up simplification (see a suggestion below) and we could model the algorithm in K, proving that it does not have infinite loops.

A basic algorithm may look something like this (heating and cooling have the same meaning as in K): simplify(pattern, side-condition):

  evaluation_stack = [pattern]
  while the evaluation stack contains more than one element, or it contains exactly element, and that element is not fully simplified:
    if the thing at the top is unsimplified:
      if the thing at the top is a pattern:
        if its predicate is not simplified:
          heat the predicate
        elif its term is not simplified:
          heat the term
      elif the thing at the top is a predicate:
        if it's an `#And`:
          heat one of its unsimplified `#And` terms with the other terms
                as the side condition
        elif it has unsimplified subterms:
          heat an unsimplified subterm
        else:
          apply a one-step simplifier to the thing at the top
      elif the thing at the top is a term:
        if it has unsimplified subterms:
          heat an unsimplified subterm
        else:
          apply a one-step simplifier to the thing at the top
    else:
      cool the thing at the top

If anything requires special evaluation (e.g. #And, or function evaluation), it gets a separate case in the if statements above. The algorithm already contains a special case for #And. A special case for function application could be implemented by, say, adding a new term type, FunctionChoice, which is a list of patterns. A function application term would be evaluated to a set of unsimplified patterns that would be used to construct a FunctionChoice term, then the algorithm would heat+evaluate all predicates in the FunctionChoice thing, after which it would check that at most one of the predicates is non-bottom (or something like that), after which it would replace the FunctionChoice with the remaining pattern.

If pattern simplification is implemented in this way, then it should be easy to model the algorithm in K. In order to prove termination, we would have to put the evaluation stack in correspondence with a well-founded relation (https://en.wikipedia.org/wiki/Well-founded_relation ). I'm guessing that, if we assume that the user only defines functions whose evaluation can be put in correspondence with a well-founded relation (and the same for #Ceil and other user-controlled stuff), then we can probably find some well-founded relation that works for the entire simplification algorithm.

Then, in K, we can probably prove something like this:

  claim singleSimplifyStep(StartEvaluationStack) => EndEvaluationStack
    ensures wellOrderLessThan(toWellOrderElement(EndEvaluationStack), toWellOrderElement(StartEvaluationStack))

where toWellOrderElement is the function which transforms an evaluation stack into a member of the set on which we defined the well-ordering relation (most N^k or something based on that) and wellOrderLessThan is the actual well-ordering relation.

Some obvious drawbacks are:

Proving this will likely take a long time (months?).
For each change to the simplifiers, one would need to also update the proof. It would be nice to have a way to translate the K semantics automatically into reasonable Haskell code.
The resulting algorithm will likely be slower than the current one.

Benefits:

All future loops would be caused by the user, not by the backend.
Future correctness proofs would be easier to do.

Alternately, you could hire RV to review the simplification code ;)

Well, we don't need to prove that the whole algorithm is complete or anything, we just need to improve the situation from "sometimes it loops" to "it doesn't loop on reasonable inputs". I think it's also pretty reasonable to require that it never loops unless a user puts in looping K rules, and even that case should be detectable (though not without performance overhead).

In my algorithm above, I think you can make a reasonable argument that it does not loop, because applyRule is always called on a smaller term (some subterm) of the overall term (something smaller than the first input).

I still want a nice psuedo-code description of the current simplification algorithm, so we can talk about re-designing it by suggesting changes to that psuedo-code algorithm. This also serves as excellent documentation for how the simplifier works.

@ehildenb I sort of agree with what you're saying, but I'm not sure about this:

The RHS of a function rule can be fairly complex, and can include ML connectives (i.e. it's not a pure term + predicate thing). E.g. you can currently define rule f(X:Int) => (0 #And {X #Equals 0}) #Or (1 #And #Not({X #Equals 0})). This kind of thing is currently used for #Ceil rules, but I have been experimenting with it for refactoring Map usage in the current elrond-multisig semantics, and it seems to be fairly nice so far (though it may take a while until the refactoring is finished, if it is ever finished). But this means that, in principle, one may use even more interesting mixes of logical connectors and terms. If the new algorithm will still support this, then it can't be as simple as you mentioned above. Do you intend to stop supporting this in the simplifier?

It's true that Grigore once said that we could probably implement all simplifiers as rules in the semantics, and this would make the algorithm above work for almost any function rule, and I kind of like that idea, but I'm guessing you didn't mean that.

If you also include handling the various ML connectors in the algorithm above, is it really different from what is currently implemented? This is not a rhetorical question, I don't know the answer, though my guess is that it's the same or fairly close. Also, if you do not include ML connectors, is it really dofferent from the current algorithm if it stops handling ML connectors?

@ana-pantilie Should things like rule f(X:Int) => (0 #And {X #Equals 0}) #Or (1 #And #Not({X #Equals 0})) still work in the new simplifier?

@virgil-serbanuta Thanks for pointing that out. I spent a bit investigating how we parse these kinds of equations, and indeed the RHS is parsed as an internal term structure. Since the internal term structure (the TermLike type) is very general right now, any kinds of ML terms can go there. I would be, however, a bit surprised if this works right now for any term because the current TermLike simplifier will not attempt to simplify any predicates inside it. What I guess is happening for #Ceil rules right now is that the RHS term gets identified as a predicate along the way and simplified accordingly.

That being the case, for rules like this, we could continue to accept them as long as the RHS is a predicate. If we want something more general, then we need to re-think our representation of terms and predicates as well.

I'm not 100% sure what you meant, but this works with the Haskell backend at commit f5bed2d571628241f68c37e22d0bacb15094b6ee (Nov 24, I think)

tmp.k

module TMP
  imports INT

  syntax A ::= a(Int)
  syntax Int ::= f(Int)  [function, functional]

  rule a(X) => f(X)

  rule f(X:Int) => (0 #And {X #Equals 0}) #Or (1 #And #Not({X #Equals 0}))

endmodule

proof-tmp.k

module PROOF-TMP
  imports BOOL
  imports TMP

  claim a(_X) => ?Y:Int ensures ?Y ==Int 1 orBool ?Y ==Int 0

  claim a(X) => 0 requires X ==Int 0

  claim a(X) => 1 requires notBool X ==Int 0
endmodule

bash

$ kompile tmp.k --backend haskell && kprove proof-tmp.k
[Warning] Compiler: Could not find main syntax module with name TMP-SYNTAX in
definition.  Use --syntax-module to specify one. Using TMP as default.
#Top

That rule doesn't look like a correct function definition to me, I don't think we want to support this. Maybe we can continue to support this style of equations in simplification rules.

Anyway, it's very surprising to me that this works right now. What I mean is that 0 #And {X #Equals 0}) #Or (1 #And #Not({X #Equals 0}) is not a predicate, but it contains predicates (those #Equals inside the conjunctions). I would expect it to not be able to simplify those #Equals, probably throw some "not simplified" errors as well. I'm thinking that maybe because it's a disjunction it's able to split it up into patt1 #Or patt2, where patt is a (term, condition) conjunction we know how to simplify.

We could alter simplification rules to allow disjunctions of patterns in their RHSs. I'm afraid anything more general than that would also require the simplifier to be more general.

Maybe we should create a list of similar examples: features the backend currently has which might be broken by a less general simplifier. For some, we can find different solutions, like the above, others will serve as reminders of how general the simplifier needs to be exactly.

To summarize, we need to better define the required completeness of the simplifier before we can start thinking about the algorithm itself.

That kind of rule is only useful when doing proofs so, indeed, it makes more sense as a simplification rule.

On first glance, that rule does look malformed to me, even for a simplification rule. The LHS is exactly single-valued, and the RHS is exactly dual-valued on the term f(Y:Int). But then I see that the extra _#And_ of each part of the disjunct restricts us to be single-valued on the RHS in all cases. So I'm not sure, but I guess I would say that this particular rule should instead be expressed as:

rule f(X) => 0 requires         X ==Int 0
rule f(X) => 1 requires notBool X ==Int 0

or if you want the haskell backend to actually evaluate it (in case it can't do the case splitting), then:

rule f(X) => #if X ==Int 0 #then 0 #else 1 #fi

I guess if we want to disallow this example, it should be caught by kore-check-functions tool. But I'm not sure it should be disallowed, I would just say it's not "idiomatic K".

I think we should restrict what cases we consider for the first cut of the simplifier rewrite to ones that are common in practice and fast to simplify, then broaden it. It would be nice to handle arbitrary functional ML patterns on the RHS, but the reality is that having general simplification procedures directly conflicts with having performance in many cases. We agreed (in the last planning meeting) that our goals for the rewrite are (in order):

soundness (never do an invalid simplification),
simplicity (maintainability of the code long term),
performance, then
completeness (able to handle arbitrary ML cases).

That is in contrast with our previous project goals here, which put completeness as number 1 priority.

This is part of the reason I suggested this architecture for the new simplifier:

def doSimplify(constrainedTerm):
      newConstrainedTerm = newSimplifier(constrainedTerm)
      if not args['--no-run-old-simplifier']:
          newConstrainedTerm = oldSimplifier(constrainedTerm)

def newSimplifier(constrainedTerm):
      # new simplifier designed to be simple, fast, and incremental.

So by default we would still always call the old simplifier on terms after calling the new simplifier, and we'll retain existing completeness. But we can gradually have the new simplifier able to handle broader classes of terms until the old one doesn't do any real work anymore.

We can also build in timers for "how much time spent in new simplifier" and "how much time spent in old simplifier". As we add more functionality to the new simplifier, it will increase how much time it's taking, but ideally that would reduce how much work the old simplifier is doing and it would decrease time spent there. So we can be very careful about merging changes that increase the amount of time spent in the new simplifier by more than the decrease in time spent in the old simplifier. Eventually, the old simplifier should be doing basically no work.

Also, as the new simplifier is able to handle more cases, those cases can be removed from the old simplifier. This will further decrease time spent there.

An example of how extreme we could make this. The first cut of the new simplifier could just gather up all the function symbols that only have unconditional rules, and apply those until completion using some efficient traversal over the current pattern. Then we call the old simplifier, but perhaps tell it not to consider those function symbols for evaluation anymore? This is just an idea.

The point is, we could build the new simplifier incrementally by first just identifying all the simplification cases we already know simple and fast algorithms for, and have it perform those. Then we fall back to the slow complete algorithm to finish the job.

@ehildenb I'm attempting to use rules like that because Map handling in K and the Haskell backend is far form optimal.

To be more specific with one of the issues (certainly not the only one):

rewrite rules can't access term structure (e.g. can't differentiate between a map variable M:Map and a concatenation K |->V N:Map).
Equations can't introduce new variables and can split the configuration only with rules like the one above.
The Haskell backend can't properly unify, say, K1 |-> V1 M1:Map with K2 |-> V2 M2:Map with K1 =/= K2 (it could, most likely, introduce a new variable X:Map and resolve the unification to M1 === K2 |-> V2 X and M2 === K1 |-> V1 X, but it doesn't do that)

These, together, make it significantly harder or awkward to implement certain things in K. A simple example is this: a proof needs to take a map as an input, and that map can be anything, so it should be an unconstrained variable. Inside the proof, the executed program branches on whether a certain key is in the map, and, if it's there, it tries to take the value with a specific type (say, unsigned int). One can prove a lemma saying that if K in_keys(M) then M ==K K |-> ?V ?M, so then the program can use either matching or unification or M[K] to get ?V, which can then be casted (which is awkward in itself, I think it's currently impossible to prove a lemma that if isUint(V:KItem) then V ==K ?U:Uint because the Haskell backend can't send sort injections to z3). Anyway, let's ignore casting for now. However, next, the program checks that another key K2 is in the map, and, if it is, then it tries to access it. We can't apply the same lemma, because we would get K |-> ?V ?M ==K K2 |-> ?V2 ?M2, the first equality term would get replaced by the second, after which we would not be able to evaluate M[K].

Using functions ([], [] orDefault, [<-] and so on) solves some of these problems, while introducing others.

Also cells of type Map have types for keys and values, but using them except in very constrained ways opens another can of worms, and triggers "Too many iterations simplifying the predicate" warnings.

Anyway, I asked for support from the Haskell backend for map unification (see e.g. https://github.com/kframework/kore/issues/2642 ) and got nowhere with that, so I started to figure out ways of using the current backend as-is, working around its limitations. Functions like the one above are part of one of the plans for doing this (to be specific, it is part of an attempt to make it less awkward to use functions on maps instead of solutions based on unification).

Please post specific examples of what you need @virgil-serbanuta , so that I can either suggest work-arounds/more idiomatic K, or can understand better the issue. I get the generic problem you stated above about lacking unification algorithms, but we've been able to work around that pretty successfully in KEVM using what I call an "abstract-pre concrete-post" storage model, combined with wrapper function #lookup which makes the sort Map look like sort Map{Int,Int}. Not sure if this will solve your problems too. https://github.com/kframework/evm-semantics/blob/master/evm-types.md#storagememory-lookup

If what you need is proper AC unification for maps, then we will have to discuss implementing that separately I think.

Either way, I want to emphasize again, that the new simplification algorithm should focus on being simple and fast. If it can't do something simply and quickly, it should err on the side of not doing it at all until we find a simple and fast way to express the same simplification. Using the sketch I provided above, we can maintain existing completeness levels of the existing simplifier while developing the a simpler and faster simplifier (which perhaps would be less complete). So your rule should continue to work while we develop it, but I would like us to focus on "what can we do very fast simplification-wise up-front, before going to the slow simplification algorithm".

General overview of the current simplification algorithm

The current simplification algorithm is, generally, about evaluating functions, pushing disjunctions to the top to create branches and pruning any infeasible ones. This is a very simplified description, of course, and it's probably the way we could quickly describe the future algorithm as well.

Internal datatypes

In order to give a more detailed description of the algorithm, I should first present a (very) simplified version of the internal types of data the algorithm uses:

-- A sum type for all ML connectives and internalized types like Maps, Sets, other builtins etc.
-- To note is that each node contains attributes which are applicable to the whole subtree.
-- The simplification algorithm depends a lot on the simplified attribute which indicates if the term
-- is fully/partially simplified, and with what SideCondition.
data TermLike

-- A sum type for _only_ predicate types.
-- The constructors for predicate-constructing connectives (like \\equals, or \\in)
-- require TermLikes as arguments.
data Predicate

-- A type which represents conjunctions of \\equals(Var, TermLike).
data Substitution

type Condition = (Predicate, Substitution)

type Pattern = (TermLike, Condition)

-- A disjunction of patterns.
type OrPattern = [Pattern]

-- This, essentially, is a type which contains information used to either prune branches
-- or to optimize the simplification process, like:
--     - conjunction of Predicates known to be \\top at a particular moment in simplification
--     - a TermLike replacement table which is built from the aforementioned conjunction
--     - a Predicate replacement table which is built from the aforementioned conjunction
--     - terms known to be defined at a particular moment in simplification
--     - function applications which are known to have been already attempted at a particular
--     moment in simplification.
data SideCondition

I decided to give a bit more detail on the SideCondition type since it encompasses most of the optimizations the simplifier currently does, and we shouldn't forget about how to transpose these into the new algorithm. There's also the issue that the addition of these optimizations the past year or so has proven to be incompatible with the rest of the simplification algorithm.

The simplification algorithm

Since the beginning, the simplification algorithm was based on simplifiers for each internal type/ML connective. I believe that initially, each one of these simplifiers tried to simplify its input fully, instead of delegating this work to a top-level loop. Work on improving separating concerns has been already done, but there are still many cases where the inter-dependencies of, especially, the smaller connective-simplifiers aren't yet fixed.

I will try to present the algorithm in a top-down fashion, I hope to present it in enough detail so that it doesn't miss the point (it has just enough information to allow constructing a new algorithm based on the old, without going down the rabbit hole that is the current implementation).

The top-most level of the simplification algorithm deals with simplifying Patterns because it is also our internal representation of Kore program configurations: a term with a condition. Therefore, we call this the Pattern simplifier.

The `Pattern` simplifier

Since one main feature of the simplification algorithm is "pushing disjunctions to the top", all simplifiers return a disjunction of some internal representation of a Kore pattern. This simplifier can also assume that the Pattern it receives as input is defined, or it can assume some a priori conditions, which adds information to its SideCondition, but the rest of the algorithm is the same:

simplifyPattern :: SideCondition -> Pattern -> OrPattern
simplifyPattern sideCondition =
    -- loop worker until the input to the loop == output;
    where
      worker pattern = do
          (term, simplifiedCondition) <- simplifyCondition sideCondition pattern
          let substitutedTerm = substitute (substitutionFrom simplifiedCondition) term
               newSideCondition = addConditionWithReplacements sideCondition simplifiedCondition
          simplifiedTerm <- simplifyTermLike newSideCondition substitutedTerm
          let simplifiedPattern = (simplifiedTerm, simplifiedCondition)
          return simplifiedPattern

Remark: of course, this computation happens inside a monadic context which I've omitted for brevity, and I will omit it for all other simplifiers as well. I just want to note that this top-level loop is fairly new code, before this loop used to happen in the TermLike simplifier, causing multiple issues with looping that were fixed.

The `TermLike` simplifier

Next, I believe it's easier to present the TermLike simplifier, since the Condition simplifier is a bit more complicated at the top level. The TermLike simplifier, similar to the Pattern simplifier, also returns a disjunction of Patterns (represented as OrPattern). I believe this is because simplifying certain terms may produce new conditions, and any \\ors need to be pushed to the top as well.

simplifyTermLike :: SideCondition -> TermLike -> OrPattern
simplifyTermLike sideCondition =
    -- loop worker until the input to the loop == output;
    where
      worker termLike
          -- This is one of the optimizations stored in the SideCondition (*).
          | Just replacementForTermLike <- lookForReplacement sideCondition termLike =
              worker replacementForTermLike
          | isTermLikeAttributeSimplified sideCondition termLike =
              return termLike
          | otherwise =
              -- Treat each TermLike case as the following: simplify the TermLike bottom-up,
              -- so basically call worker on the children, and feed that output to the respective
              -- simplifier for each case, i.e. the Application simplifier, the Not simplifier, the And simplifier ...
              -- Very important: no simplification will happen in the predicate cases (\\equals, \\ceil, \\in etc.).

(*) The SideCondition keeps a table of terms with function applications at the top -> constructor-like terms which it built from the predicates assumed to be true.

This seems simple enough, but the complexity lies inside the connective-simplifiers themselves. I think the most complex ones here are the Application, And and the internal Map/Set simplifiers: the Application one essentially does function evaluation, the And one eventually calls unification and the Map/Set ones do AC normalization.

One other thing to add is that some of these simplifiers call eachother, a good example would be the Not simplifier: it calls the And simplifier, while the And simplifier also depends on a Not simplifier which it receives as an argument. I won't enter into details about these connective simplifiers here because I think this comment should just be a general overview of the current algorithm. I can add more details in follow-up comments.

The `Condition` simplifier

The result of this simplifier is, in practice, again an OrPattern, even though it does not modify the input TermLike in any way.

simplifyCondition :: SideCondition -> Pattern -> OrPattern
simplifyCondition sideCondition =
    -- normalize the input, then loop worker until the input to the loop == output;
    where
       worker (term, (predicate, substitution)) = do
           let substitutedPredicate = substitute substitution predicate
           simplifiedPredicate <- simplifyPredicate sideCondition substitutedPredicate
           fullySimplifiedPredicate <- simplifyPredicates sideCondition simplifiedPredicate
           let newCondition = fullySimplifiedPredicate <> toCondition substitution
           normalizedNewCondition <- normalize newCondition
           fullySimplifiedCondition <- simplifyConjunctions normalizedNewCondition
           -- if the fullySimplifiedCondition has not changed, and it doesn't contain any variables from the substitution
           -- then return fullySimplifiedCondition, otherwise call worker again on it

There are two loops and four main procedure calls here. We probably should merge the two loops into one, just note that the two termination conditions, although seem similar from this pseudocode, are actually different conditions. But that doesn't mean we couldn't combine them. The four main procedures are: normalize, simplifyPredicate, simplifyPredicates and simplifyConjunctions. I will try to succinctly describe each of them.

The `Substitution` simplifier

normalize will effectively call the Substitution simplifier. This is another simplifier which creates some inter-dependencies between the Condition simplifier itself, the And simplifier and possibly more. It's possible it gets passed in to other simplifiers as an argument as well, but I haven't had the chance to investigate this very much. I just want to notify everyone that there's a lot of hidden complexity here.

simplifyPredicate is essentially the Predicate simplifier, so the next section will be about that.

The `Predicate` simplifier

Very similar to the TermLike simplifier, it traverses the Predicate bottom-up and applies simplifiers. The difference is, that most of these simplifiers are much more well-behaved. The main idea is that we want to end up with a normalized disjunction of conjunction of predicates, therefore most of the simplifiers are constructed to just do their part of the job for attaining this.

The main problem makers here are the Equals, Ceil and In simplifiers, which just call the old simplifiers.

Another thing to note here is that this simplifier is required to call the TermLike simplifier, because the children of predicate-constructing connectives are TermLikes.

`simplifyPredicates`

This procedure splits the Predicate on the top conjunction and simplifies each smaller Predicate with the others contained in the SideCondition. For example, P1 /\ P2 /\ P3 gets split up into [P1, P2, P3], and the procedure calls simplifyPredicate for each predicate in the list with the SideCondition containing the rest of the predicates in the list.

What this means is that all of the Predicates inside the conjunction will essentially get simplified with a different SideCondition, invalidating some initial assumptions of the Simplified attribute.

`simplifyConjunctions`

This is a procedure which also gets called when constructing SideConditions. It essentially creates the TermLike and Predicate replacement tables which can be used to optimize simplification. Inside the Condition simplifier, this function will also apply any possible replacements to the Predicate, hereby simplifying it further.

Closing remarks

I hope this does a good-enough job of describing the top level of the current simplification algorithm. In my opinion, the current implementation is fairly clean, and the bigger issues are inside the "smaller" simplifiers. Let me know if you'd like more details for any of the sections.

We could probably optimize it further to allow top-down simplification as well. One case where this would be useful I think is for Ceil simplification: you don't need to always evaluate everything inside a term to figure out if it's defined or not. There are also probably other cases where this approach would be faster. @dopamane suggested, that since we're already using Cofree to represent our term/predicate types we could use recursion schemes for combining top-down and bottom-up traversals.

Experiments:

And simplifier: split between Unification and And normalization, make a list with places which use And simplification, do they actually want And normalizing or And unification? Is And unification
Function application simplifier (which just applies equations)
Investigate Ceil simplifier

Concretely:

add --simplifierx flag which switches on calling new simplifiers in particular places, in order to test with downstream projects; needs test duplication

@ana-pantilie

Sorry to ask only now: Could you list the goals of this overhauling? The original message lists seems to imply that the goal is to make the simplifier easier to understand and maintain. Is that the only goal? How about avoiding loops, or performance gains, or other things? Are those explicit goals, or they are things that might benefit from the redesign, without being actual goals?

I'm asking because one could, e.g., make the simplifier easier to understand and maintain, without directly addressing the looping issue. Of course, simplifying the simplifier would probably make it easier to debug/fix/avoid loops simply because the code is better.

@virgil-serbanuta Everett and I have been discussing this, and I agree with his philosophy: correctness is first place with simplicity being a close second. The main difference is that the old algorithm was designed with completeness in mind, which we realized is not in line with our practical purposes.

simplifying the simplifier would probably make it easier to debug/fix/avoid loops simply because the code is better.

I agree, a simpler design should have as a consequence less implicit looping, and it should be easier to make it faster as well.

@ehildenb suggested a good method for making incremental changes. I am currently implementing the architecture to allow us to do this, and then we will start to do some experiments.

runtimeverification / haskell-backend

Discussion: overhaul the simplifier #2923

NOTE: This issue description is a draft, WIP

Introduction

Representing Kore patterns

General overview of the current simplification algorithm

Internal datatypes

The simplification algorithm

The `Pattern` simplifier

The `TermLike` simplifier

The `Condition` simplifier

The `Substitution` simplifier

The `Predicate` simplifier

`simplifyPredicates`

`simplifyConjunctions`

Closing remarks

runtimeverification / haskell-backend

Discussion: overhaul the simplifier #2923

NOTE: This issue description is a draft, WIP

Introduction

Representing Kore patterns

General overview of the current simplification algorithm

Internal datatypes

The simplification algorithm

The Pattern simplifier

The TermLike simplifier

The Condition simplifier

The Substitution simplifier

The Predicate simplifier

simplifyPredicates

simplifyConjunctions

Closing remarks

The `Pattern` simplifier

The `TermLike` simplifier

The `Condition` simplifier

The `Substitution` simplifier

The `Predicate` simplifier

`simplifyPredicates`

`simplifyConjunctions`