Draft: `kred`: A faster, somewhat compatible `cbn` alternative

[Janno]

This introduces kred (short for "kernel reduction", not to be confused with kernel reduction [no quotes]). The name needs some workshopping. But it is descriptive in the sense that kred is based on a modified copy of CClosure. The modifications are as follows:

• It does refolding of global fixpoints (by including #18672). Note that this is likely as unsound as the refolding in cbn and simpl for reasons of subtyping. (See also #5645 which is not directly related to subtyping but fits the general scheme of unsound refolding.)
• It respects Arguments and also the absence of Arguments. It tries to interpret the (lack of) Arguments the same way cbn does (AFAIK), i.e. no annotations introduces an implicit simpl nomatch, everything that is not simpl never is fair game to be unfolded (and generally will be) as long as the !s and / are satisified, and / restricts the unfolding to applications with no less than the specified number of arguments.

kred currently produces almost the same output as cbn except in some specific test cases (see output/simpl.v.out for examples where it differs).

The main feature of kred is that it is fast. The reason for this is mostly the delayed substitutions it inherits from CClosure. AFAICT kred's performance is usually within a factor of 2x to 3x of lazy. Said differently, it is algorithmically faster than cbn and the relative performance can be arbitrarily better. kred addresses known performance issues of cbn with primitive projections, (mutual) fixpoints, and many more. The examples in #18619 and #15720 have been incorporated into the test suite to showcase the performance.

TODO:

• [ ] Choose a good name. kred is very confusing.
• [x] See if the 4 TODOs in Arguments.v can be fixed. This is the case of a.(p) being reduced to {| p := .. |}.(p) when p : simpl never and a : simpl nomatch. I think the current behavior is faithful to these annotations but cbn refolds a, possibly because the overall term ends up being a projection. This could possibly be implemented with some stack shuffling but I don't know that it is necessary.
• [x] Make the performance tests actually test something. Right now neither the performance nor the resulting terms are being checked in any way.
• [ ] There is any issue with lifts/shifts, likely Zshift nodes being accumulated in the wrong order in the new stack nodes
• [ ] Refolding of Definition foo := let x := bla in fix blub := .. does not work yet and I do not understand how it is supposed to work. cbn does it but only in some specific circumstances.

Fixes / closes #????

• [ ] Added / updated test-suite.

• [ ] Added changelog.
• [ ] Added / updated documentation.
  • [ ] Documented any new / changed user messages.
  • [ ] Updated documented syntax by running make doc_gram_rsts.

• [ ] Opened overlay pull requests.