Mem2reg (Analysis + Transform plan)

[dc-mak]

This PR adds support for the analysis part of a Core-to-Core mem2reg pass. This would be useful to speed up execution of Core programs and also CN proof (and Fulminate?) substantially.

It was developed with Claude and so I've included the plans that fed into the code changes for documentation in this PR - the final PR can have these deleted (including a fresh branch so they don't even exist in the history).

For example, Claude seemed to think that an Ail/Ail+Core analysis would be more complicated than a simple Core-to-Core, so the reasoning for this is included in doc/history/2026-03-13_mem2reg-plan.md

It's already got a few commits and a fair amount of code, but the PR can and should be read one commit at a time.

The analysis pass is quite naive - it does multiple traversals for one thing at a time (instead of one complex one to collect all the info), but it's easy to understand and I figured it can be improved later once we have a working implementation that passes tests (or not, if it turns out to be fast enough), e.g. I assume perhaps the Core rewriter library does some sort of pass-fusion?

[dc-mak]

Pasting this discussion here for visiblity.

@cp526:
I suspect for Esave one wants to transform the label type. In the normal Core elaboration, for any in-scope C variable x, the Esave will take as an argument a pointer to the stack location of x. The mem2reg transformation should make it so the label instead takes the current value of x.

@neel-krishnaswami:
Operationally, save is basically just a let-binding, so it's easy.

It's only when you hit a run that anything weird happens. Its operational rule uses the "labelmap" which (annoyingly) shows up in the run operational rule and nowhere else in Kayvan's thesis. Conceptually it's pretty straightforward but there may be details which live only in the Cerberus codebase and/or Kayvan's brain.

@dc-mak:
Ok so it seems like for the analysis, the default parameter of save counts as a use, but a slightly unusual one. As Neel pointed out, it is basically a let-binding, so we need to consider the binder as an alias for analysing the body. But for the transformation/executing the save as straightline code (not from a run), we would want it to count the default value as a load.

AFAIR, elaboration ensures that saves are closed wrt C variables in scope (ie. only C local vars are bound in its binders). However, if this were not the case, any uses of a C local variable in the body (which were not bound by the save params), they would disqualify a local variable from promotion (since the save can be reached from straightline, forward run, and backward run, but any transformation would effectively lock-in the straightline case).

I think the fact that save parameters only bind the C local vars means that run should be easy. Unlike function calls, where passing the address of a local var would escape and disqualify it, passing the address of a local var to run would basically count as a load. I don't think labelmap will be much of a blocker, I remember understanding it once and I'll revisit it to be sure.

The transformation for save will be a little fiddly, like with if, since any mutated local vars will need to passed out the final expression, rebound with a let strong, and the environment updated.

@cp526 For what it's worth, there's two alternatives to doing this as a core-to-core rewrite: option (1), which Kayvan was considering, is to adjust the elaboration around the variables mem2reg would optimise; option(2) would be to make this a mucore-to-mucore rewrite. We want to merge the core and mucore expression grammars, but will want to keep mucore's separate handling of labels (with labels as function-local procedures rather than Esave), so then you wouldn't have to think about how mem2reg should work for Esave

[dc-mak]

@cp526:
For what it's worth, there's two alternatives to doing this as a core-to-core rewrite: option (1), which Kayvan was considering, is to adjust the elaboration around the variables mem2reg would optimise; option(2) would be to make this a mucore-to-mucore rewrite. We want to merge the core and mucore expression grammars, but will want to keep mucore's separate handling of labels (with labels as function-local procedures rather than Esave), so then you wouldn't have to think about how mem2reg should work for Esave

---

Other related points raised in discussion:

• Consider the impact on the code which supports reading local variables in at a program point within annotations (CN statements). We'd need to thread the environment of the transform through to that point.
• Consider that the promotable variables info could be useful to Fulminate; this may push towards an Ail-analysis at least, if not an Ail-transform too. IIRC, the symbols are the same in Ail and Core so this may not be a big concern.
• Another option is analysing at Ail/Core, but emulating the transform in the type system. This would make the type system more complicated.

[dc-mak]

I've been coding and thinking some more and I'm now less sure about doing a mem2reg transformation on Core.

1. It can affect source locations.
2. The eliminated and new symbols will need to be threaded through to any backends like anyways CN to support existing features to make sure that changes in mem2reg don't break specifications. The mem2reg pass would essentially need to preserve the environment used to support the ghost load in the middle of the function, or loop invariants.

   int main() {
       int x = 10;
       while (x > 0)
       /*@ inv 0i32 < x; x <= 10i32 @*/
      { x--; }
      /*@ assert (x == 0i32); @*/
      return x;
    }

I always found the treatment of local vars in CN to be confusing (and I was not alone in this #443).

Could it be possible to end up in a situation where updating a mem2reg pass would cause existing verified code to break? That would be bonkers, but I am confused right now.

These considerations push me towards favouring an analysis and then passing those locations to CN, so they can be treated specially/on a fast path in the checker itself. But I am not decided/am still unsure.