fix handling of bounds in conseq equiv phoare

[oskgo]

This fixes #834 and #836.

The fix is to modify the side condition requiring a memory satisfying the left precondition to imply the existence of a right memory satisfying the right precondition and jointly satisfying the two-sided precondition. Now we also require the bounds to be proven equal under these two memories.

In most existing uses this part of the side condition should just simplify away since the bounds should be equal and usually don't depend on memories.

As a side effect this PR also permits uses of this kind of conseq to use bounds that aren't trivially equal, requiring equality to be proven instead.

[Copilot]

Pull Request Overview

This PR fixes the handling of bounds in the conseq rule for equivalence judgments in phoare logic by adding a side condition that requires bounds to be equal under the appropriate memory substitutions.

Key Changes:

• Extended transitivity_side_cond to accept optional bound parameters and generate bound equality conditions
• Modified t_bdHoareF_conseq_equiv to accept and pass the second bound as a parameter
• Updated the documentation comment to reflect the new bound equality requirement

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[fdupress]

Decision from meeting: add a unit test and merge.

[mbbarbosa]

I was trying out this PR and I still get some issues with combining lossless with hoare to get phoare.
I don't know why, but this is the pattern that fails with invalid goal:

require import AllCore FMap.


module Foo = {
   proc foo(i :int, a : (int,int) fmap) = {
           a.[i] <- oget a.[i] + 1;
           return a;
   }
}.

lemma foo_ll : islossless Foo.foo by islossless.

lemma foo_h _i _a :
   hoare [ Foo.foo : i = _i /\ a = _a ==>
     forall j, j<>_i =>  _a.[j] = res.[j]] by proc;auto;smt(FMap.get_setE).

lemma foo_p _i _a : phoare [ Foo.foo : i = _i /\ a = _a ==>
     forall j, j<>_i =>  _a.[j] = res.[j]] = 1%r
   by conseq foo_ll (foo_h _i _a).

[fdupress]

Can you try introducing j and the premise, then also passing them to the proof term? (To note, this is to help debug and triage, not to dismiss the fact that this is clearly a bug.)

[mbbarbosa]

Ah, that works!

[fdupress]

Alright! Then the default and basic fix is "add an error message" (can be a separate PR). Then we think about tackling this in general.

[mbbarbosa]

I was hoping for a non breaking fix soonish. Ow this will impose a major refactoring on a large project.

[fdupress]

It might be quick, still, if it's just about reactivating an existing code path.

[fdupress]

#847 is the issue that would get closed if we also fix this new problem in this PR.

[fdupress]

I just noticed (weekend work is not my best work), that the j and premise are in the postcondition, so I now understand both why it's a major refactoring (which might not even be possible depending on how much you simplified), and why you might think it should Just Work.™

[oskgo]

I believe the issue in #847 is orthogonal. This uses the equiv phoare variant of conseq, while #847 uses phoare hoare. I'll get this merged and then have a look at the other issue.

I've added the tests I wanted to add now, so this is ready for merge.