Make termination checks for exec functions, add support for mutable references in parameters, and emit a warning that the check doesn't account for loops

[utaal]

I do not believe this opens to any potential unsoundness, especially because it's already possible to write a non-terminating recursive exec function with a loop.

Reported by @matthias-brun.

[utaal]

I am not confident this is okay.

[Chris-Hawblitzel]

Can you say what the motivation for this change is? I could imagine having an option that either disables termination checks for both exec recursive functions and exec loops, or enables termination checks for both exec recursive functions and exec loops.

[tjhance]

I was already under the impression we didn't support termination checking for exec functions, seeing as, exec functions support while loops, which don't support termination checking. As far as I can tell, Verus never complains about the existence of loops and there isn't support for opting in to exec-mode termination checking (at the moment) so permitting decreases on an exec function would be misleading.

[Chris-Hawblitzel]

Won't some people want termination checking for exec loops in the future, though? It's not implemented yet, but I think that's just because it wasn't a high priority to implement. And the syntax for decreases on loops is implemented, even if the check isn't yet. I don't think exec checking would have to be turned on by default, but in cases where people explicitly want the checking, it seems harmless to allow it. Let me propose a way to allow it when requested:

• if some writes decreases on a loop or exec function, it is checked
• if the command-line option --check-exec-termination is provided, then exec recursive functions and exec loops must have decreases clauses

[tjhance]

well, i don't object to supporting it in the future. I'm just saying Andrea's change makes sense now and until such support does exist.

[Chris-Hawblitzel]

I think in the design I'm proposing, though, we wouldn't be disallowing and removing the decreases clauses that already exist.

[Chris-Hawblitzel]

We would, however, remove by default the requirement that exec functions have decreases clauses. I support that part of the change.

[utaal]

The initial impetus was due to the fact that the support was incomplete: decreases did not work for functions with mutable references as arguments. That turned out to be a simple fix, so those are now supported.

The need to check termination and the guarantees provided by the check were unclear to me. From the discussion:

• termination checks for exec functions aren't necessary for soundness,
• the current check does not take into account loops,
• we'd like to support optional full termination checks for exec functions in the future.

So, this PR, now:

• makes the termination check for exec functions optional (only enabled when there's a decreases clause),
• warns the user that a termination check on an exec passing doesn't guarantee that the function terminates if there are loops.

[tjhance]

can you add a warning or error if the user tries to use decreases on a loop? It looks like that's still missing, I think.