sim less robust

[mbbarbosa]

Detected breaking change in matching lambda expressions.
(Also pretty printing declares match when programs are the same modulo simplification).

Here's a minimal example.

require import AllCore.

module Foo = {

        proc foo1() : (int -> int) = {
             var x;
              x <- fun i => 2*256;
              return x;
        }
        proc foo2() : (int -> int) = {
              var x;
              x <- fun i => 512;
              return x;
        }
        }.

equiv foo : Foo.foo1 ~ Foo.foo2 :
        true ==> ={res}.
        proc. sim.

[oskgo]

It reproduces on ba49ccd, so it's been around for a while now (At least it's not another consequence of #789, lucky me). Versions before that are more annoying for me to build due to changes in dependencies.

Do you know when this used to work?

I think that it's super weird that the pretty printer behaves differently than sim here. I'd expect sim to be more aggressive in normalisation than the pretty printer, not the other way around.

[mbbarbosa]

We are working on a branch that follows main (bdep_ecCircuitsRefactor).
Things were OK when we merged main here:
d0d639b

[oskgo]

That commit was merged from e9aec65, but the issue reproduces there as well. Maybe there's something fragile in bdep_ecCircuitsRefactor that fixed it temporarily?

[oskgo]

I've tried a bit more to find a commit where your example passes, without luck. I can't run the bdep_ecCircuitsRefactor branch due to architecture incompatibilities. I've checked with main branch commits that are over 2 years old and the bug is still there.

Are you sure that your example showcases the regression and not just the bug? Maybe there's something else in your original code that made it pass before?

I sure hope it's not a breaking change coming from a dependency that got updated, but that's also a possibility. If you can find a configuration without the bug we could test this by reinstalling the dependencies.

[mbbarbosa]

Ok, some more info.
The bug is manifesting itself in code that was unrolled using unroll for.
The original lambdas are of the form i => f (i * constant).
Maybe what happened is that at some point unroll for started simplifying?
This would explain what we both see.
In any case, I have fixed my proofs so that they now use a closer syntactic match, so they are accepted.