fix(engine) Avoid wrapping return in a tuple.

[maximebuyse]

Fixes #1044.

This fixes phase LocalMutation that was wrapping return expressions inside a tuple (to pass a state) but the state is lost in case of a return so we should not try to pass the state (otherwise it is not caught by DropReturnBreakContinue).

[W95Psp]

Ah, that makes sense, thanks, looks great!

[W95Psp]

The test failure looks suspicious though, do you have an idea why we have this change @maximebuyse?

[maximebuyse]

The test failure looks suspicious though, do you have an idea why we have this change @maximebuyse?

I just pushed a fix. It was just a dumb mistake. Tests are passing now.

[maximebuyse]

@W95Psp I fixed the issue with the typing of returns and the bug introduced for the proverif backend is now gone. Should we merge now?

[W95Psp]

Fantastic!
Let me try on bertie

[W95Psp]

Nothing changed in the generation of PV, but the verification doesn't work any longer.
The proverif TC is not under CI and relies on patches, so we can't say what broke it.
Let's go ahead and merge, it will be hard to diagnostic what broke bertie PV.
We need to (1) remove the patches and then (2) add CI there

[karthikbhargavan]

@jschneider-bensch may want to look at why PV verification fails