Allow substitutions of locals using the same memory as that used by a Pr

[oskgo]

Before, the following would fail:

require import Real.

module M = {var x: bool proc p()={}}.

lemma L (&m: {b:bool}): b{m}= true => Pr[M.p()@&m:true] = 1%r. 
proof. move => ->>.

We still prevent it in the case where the substitution uses a global, because in that case we'd be erasing information:

lemma L (&m: {b:bool}): M.x{m}= true => Pr[M.p()@&m:true] = 1%r. 
proof. move => ->>. (* This fails to substitute *)

This makes progress and /> more aggressive, which makes it a breaking change. It also fixes some bugs when nesting Pr formulas inside other program logic formulas:

lemma L: phoare[M.p{&m}: true ==> Pr[M.p()@&m:true] = 1%r] = 1%r.
proof.
proc. (* This line used to cause a memory clash anomaly *)

[strub]

@fdupress How do we handle external projects breakage?

[fdupress]

Badly. You ping the maintainer (me) and give a reasonable timeframe to fix so it doesn't hold up the merge.

I am not working today (at least not on this), but will take a look tomorrow. If you prefer, you can remove the failing project from external CI and task me with adding it back in once I've fixed the proof.

(We could set up a secondary list that gets checked but doesn't fail the whole CI for this purpose.)

[strub]

Removing the project from the CI is the first step of a two-step permanent removal.

Let's wait. I suspect that the fix is easy and I can have a look.

[fdupress]

Quick and dirty fix applied. Pipeline running again.

This is a breaking change. Can it wait for the next window?

The naive fix does not yield a valid proof in the last version of EC. It is likely that for all proofs that are broken by this, there is a proof that is valid in both the old and new versions. (Just avoid substitutions on Pr expressions.)

[alleystoughton]

It seems this PR doesn't have the eager logic changes, which makes it hard to check developments that use eager.