Booster Description

[geo2a]

This PR adds prose documentation for Booster --- a fast symbolic rewrite engine for K.

Some of the prose and the rewriting diagram have been contributed earlier by Sam Balco.

[jberthold]

Good that you point out unevaluated functions. I think we should add some concrete examples here.

[jberthold]

Suggested change

	The requires clause check is encapsulated by the [checkRequires](https://github.com/runtimeverification/haskell-backend/blob/master/booster/library/Booster/Pattern/Rewrite.hs#L496) function defined in the `where`-clause of `applyRul`e. It will:
	1. substitute the rule's requires clause with the matching substitution
	2. check if we already have any of the conjuncts verbatim in the pattern's constrains. If so, we filter them out as known truth
	3. simplify every conjunct individually by applying equations. This is morally equivalent to sending every conjunct as to the `"simplify"` endpoint and will use the same code path, bypassing internalisation.
	4. filter again, as the simplified conjuncts may not be present verbatim in the known truth
	5. if any clauses remain, it's time to fire-up Z3 and check them for validity.
	- some rule will be rejected at that point, as their pre-condition P (the `requires` clause) is invalid, which means that the rule is applicable statically, but the dynamic conditions makes it inapplicable.
	- some rules may have an indeterminate pre-condition P, which means that both P and its negation are satisfiable, i.e. the solver said (SAT, SAT) for (P, not P).
	- in this case we can apply this rule conditionally, but add P into the path condition We will call `not P` the _remainder condition_ of this rule and keep track of it too
	The requires clause check is encapsulated by the [checkRequires](https://github.com/runtimeverification/haskell-backend/blob/master/booster/library/Booster/Pattern/Rewrite.hs#L496) function defined in the `where`-clause of `applyRule`. It will:
	1. substitute the rule's requires clause with the matching substitution
	2. check if we already have any of the conjuncts verbatim in the pattern's path condition (`PC`). If so, we filter them out as known truth
	3. simplify every conjunct individually by applying equations. This is morally equivalent to sending every conjunct as to the `"simplify"` endpoint and will use the same code path, bypassing internalisation.
	4. check again whether any of the, now simplified, conjuncts is present verbatim in the path condition
	5. if any clauses remain, check all conjuncts together with Z3 for validity given the path condition.
	- some rule will be rejected at that point, as their pre-condition `P` (the `requires` clause) is false given `PC`, which means that the rule is applicable statically, but the dynamic conditions makes it inapplicable.
	- some rules may have an indeterminate pre-condition `P`, which means that both `PC /\ P` and `PC /\ not P` are `SAT` in the solver, i.e., neither `P` nor `not P` are implied by `PC`
	- in this case we can apply this rule conditionally, but add `P` into the path condition We will call `not P` the _remainder condition_ of this rule and keep track of it too

[jberthold]

Suggested change

	- some rules will have a valid requires clause, which means they definitely do apply and we do need to add anything else into the path condition as an assumption.
	- some rules will have a valid requires clause, i.e., `PC => P`, which means they definitely apply and we do not need to add anything else into the path condition as an assumption.

[jberthold]

Suggested change

	- if `requires` is UNSAT, we do not apply the rule, just if it didn't even match;
	- if `requires` is found to be false, we do not apply the rule, just as if it didn't even match;

[jberthold]

Suggested change

A priority group of rules gives raise to a group **coverage condition**, which is defined as a disjunction of the requires clauses of the rules in the group. If the coverage condition is valid, it means that no other rules can possibly apply. The negation of the coverage condition is called the group's coverage condition is called the **remainder condition**. The the remainder condition is unsatisfiable, then the coverage condition is valid, and the group is complete.

A priority group of rules gives rise to a group **coverage condition**, which is defined as a disjunction of the requires clauses of the rules in the group. If the coverage condition is valid, it means that no other rules can possibly apply. The negation of the coverage condition is called the group's **remainder condition**. If the remainder condition is unsatisfiable, then the coverage condition is valid, and the group is complete.

[jberthold]

Suggested change

	Successful rule application does not trigger pattern-wide simplification, i.e. very far and make many steps without simplifying the pattern even ones.
	Successful rule application does not trigger pattern-wide simplification, i.e. rewriting can proceed very far and make many steps without simplifying the pattern even once.