Preserve variable names in ProgramLogic proofs

[andres-erbsen]

• after function calls
• on loop entry
• ...

This will require careful thought about compat with current proofs.

[samuelgruetter]

A note on what I did in LiveVerif: I use a custom make_fresh tactic for this, because the previous values of variables still need names, so the old variables need to be renamed to not-too-confusing names. If the C source program contains variables named x0 and x1, and you use Rocq's builtin fresh tactic, you get a variable x1 that refers to an old value of x0, which can be confusing. So instead, I chose to use ' as a marker for old values, because that char cannot be part of C identifiers. So, if you have a program that assigns and reassigns a over and over again, its previous values will be named a', a'', a''', etc, and its most recent value is named a.