Does not verify syntactic equality

[andreagilot-da]

Stainless timeouts when verifying that bar is actually equal to its body.

import stainless.lang._
import stainless.collection._

object Bug {
  def bar(l: List[(BigInt, Option[BigInt])]): List[Option[BigInt]] = {
    l.map{ case (left, right) => None()}
  }

  def barEqualsItsBody(l: List[(BigInt, Option[BigInt])]): Unit = {
  }.ensuring(bar(l) == (l.map{ case (left, right) => None()}))

}

Moreover if we add assertions in the body of the theorem, we have two body assertions timeouts, one for the Cons case and one for the global case, which should not happen.

  def barEqualsItsBody(l: List[(BigInt, Option[BigInt])]): Unit = {

    val a = bar(l)
    val b = l.map{ case (left, right) => None()}


    l match {
      case Nil() => assert(a == b)
      case Cons((key, keyMapping), t) => assert(a == b)
      case _ => assert(false)
    }

    assert(a == b)

  }.ensuring(bar(l) == (l.map{ case (left, right) => None()}))

In Scala 3, the first snippet verifies but there is still the same problem for the second one.

[mario-bucev]

In this particular case, it is due to underspecifying the type of None whose type is inferred differently depending on the Scala version.
This underspecification triggers type-encoding, generating hard VCs.
In this particular case, replacing None() to None[BigInt]() make the verification go for both frontend.
Still, it is an interesting issue to look at.

[andreagilot-da]

The same problem arises when changing the None by something else:

def foo(key: Boolean): Boolean = false
  
def bar(l: List[(Boolean, Unit)]): List[(Boolean, Boolean)] = l.map { case (key, keyMapping) => key -> foo(key)}

def barEqualsItsBody(l: List[(Boolean, Unit)]): Unit = {
}.ensuring(bar(l) == (l.map { case (key, keyMapping) => key -> foo(key)}))

This time even with an @extern annotation, the verification times out. Also, this time, the verification does not succeed in Scala 3 either.

Things I tried while keeping the @extern annotation:

• Replacing foo(key) by false inside bar, and this makes the verification work.
• Removing the (unused) key argument from the function foo either by replacing it with foo or foo() and both make verification work.
• Changing the tuple argument of the list by only BigInt either for the argument or result type of bar and both make the verification work.
• Changing Unit (in the list) by any other type, including a generic type does not change anything.
• Similarly, changing the type of the argument key of foo does not seem to change anything.

[mario-bucev]

Mostly commenting my findings so that I do not forget :p
It seems that this stems from the lambda being simplified when the function bar is unfolded while the original in barEqualsItsBody is not.
When unfolded, the lambda for bar is:

x => (x._1, foo(x._1))

For barEqualsItsBody, the lambda is instead:

x => {
  val y: Boolean = x._1
  (y, foo(y))
}

hence they are actually not the same from Inox' perspective.
Putting an @inline to bar seems to confirm this hypothesis.
Maybe adding a simplification step in normalizeStructure could resolve the issue (but if it hasn't been done before, there is surely a good reason for that?).
Edit: Apparently, there is already a simplification step before, but SimplifierWithPC does not inline projection of variable. Adding this rule should resolve this particular issue (without touching normalizeStructure).

[samarion]

Hmm, this is a bit surprising. I would expect to see the reverse :P (namely the lambda inside the body of bar still containing the let-binding).

We call simplifyLets on the VC (which does the projection inlining):

stainless/core/src/main/scala/stainless/verification/VerificationChecker.scala

Lines 140 to 142 in 33a990a

	(e: Expr) => latticeSimp.simplify(simplifyLets(removeAssertionsAndGhostAnnotations(e)))
	case Vanilla =>
	(e: Expr) => simplifyExpr(simplifyLets(removeAssertionsAndGhostAnnotations(e)))(using PurityOptions.assumeChecked)

But we don't perform projection inlining inside simplifyExpr which is called on function bodies:
https://github.com/epfl-lara/inox/blob/1499384f950d7b0202c1303c00e8cdd1bcb6ca45/src/main/scala/inox/transformers/SimplifierWithPC.scala#L220-L268

We can extend the SimplifierWithPC logic to do projection inlining, but I would also remove the simplifyLets call in the verification checker to make sure simplifications are consistent.

You can extend the let case here to cover simple expressions:

...
lazy val realPE = ...
lazy val isSimpleBinding = re match {
  case TupleSelect(_: Variable, _) | ADTSelector(_: Variable, _) | IsConstructor(_: Variable, _) |
       FiniteSet(Seq(), _) | FiniteMap(Seq(), _, _, _) | FiniteBag(Seq(), _) => true
  case _ => false
}

if (
    (((!inLambda && pe) || (inLambda && realPE && !containsLambda)) && insts <= 1) ||
    (!inLambda && immediateCall && insts == 1) ||
    (((!inLambda && pe) || (inLambda && realPE)) && isSimpleBinding)
      ) {
  ...
  (replaceFromSymbols(Map(vd -> re), rb), pe && pb)
  ...

---

Unrelated, but these lines look a bit suspicious:
https://github.com/epfl-lara/inox/blob/1499384f950d7b0202c1303c00e8cdd1bcb6ca45/src/main/scala/inox/transformers/SimplifierWithPC.scala#L225-L233

Doesn't this transformation just get undone by the one below anyway?

[mario-bucev]

The simplified VC is:

bar$0(l$38) == map$9[(Boolean, Unit), (Boolean, Boolean)](l$38, (x$1$8: (Boolean, Unit)) => {
  val key$13: Boolean = x$1$8._1
  (key$13, foo$0(key$13))
})

which now you mention simplifiedLets is surprising me!
For projection inlining, wouldn't we need to be a bit more aggressiveness? For example, we maybe would also like to inline a.f1.f2 with val a = x.f0? Although epfl-lara/inox#198 may be too aggressive.
Regarding the suspicious line, my understanding is that it binds fields and use these bindings instead. But I do not see what es.exists { case _: ADT => true case _ => false } is supposed to prevent!

[samarion]

which now you mention simplifiedLets is surprising me!

Yeah same here. Might be worth investigating a bit exactly where the simplifications take place.

For projection inlining, wouldn't we need to be a bit more aggressiveness? For example, we maybe would also like to inline a.f1.f2 with val a = x.f0? Although epfl-lara/inox#198 may be too aggressive.

The issue is that x.f0 is not always pure, e.g. consider val a = Nil(); a.head. That's why I'm suggesting adapting the existing let case to make sure we only simplify in the right places.

Regarding the suspicious line, my understanding is that it binds fields and use these bindings instead. But I do not see what es.exists { case _: ADT => true case _ => false } is supposed to prevent!

It seems to lift ADT nodes which appear inside an ADT constructor into a dedicated let-binding. However, that let-binding will only be used in one place so it will be immediately inlined right afterwards...

I think we used to have a simplification which rewrote things like val x = A(1, 2, 3); x.f0 into 1 but it seems to have disappeared. Maybe that's what the case is supposed to handle?

[mario-bucev]

Ah right, I've forgot about impure expressions! I'll make these changes, thanks :)
I'll also investigate the ADT lifting at the same time.

[mario-bucev]

Regarding isSimpleBinding, could we extend the definition to handle multiple projections such as v.f1.f2? In the (((!inLambda && pe) || (inLambda && realPE)) && isSimpleBinding) condition, this should take care of the expression being pure?

---

For the suspicious line, it appears to worsen simplification in some cases.
For instance, in the following snippet:

object Simp {
  case class A(b: B, f2: BigInt)
  case class B(f1: BigInt, f2: BigInt)

  def test(f1: BigInt): Unit = {
    val a = A(B(f1, 1), 2)
    assert(a.b.f1 == f1)
  }
}

The original VC is:

val a: A = A(B(f1, BigInt("1")), BigInt("2"))
a.b.f1 == f1

With the suspicious line, we get:

B(f1, BigInt("1")).f1 == f1

Without it, the expression simplifies to true!
In https://github.com/epfl-lara/inox/blob/41ffe806b04769c0d6757ebfeb17a96c7d5efd8a/src/main/scala/inox/transformers/SimplifierWithPC.scala#L233-L235 we give the following expression to simplify:

val b: B = B(f1, BigInt("1"))
val a: A = A(b, BigInt("2"))
a.b.f1 == f1

The idea sounds good, though it may need some rules to be extended?

---

For the simplifyLets not inlining the binding, it's due to the original VC not having anything to inline:

val res: Unit = ()
bar(l) == map[(Boolean, Unit), (Boolean, Boolean)](l, (x: (Boolean, Unit)) => x match {
  case (key, keyMapping) =>
    (key, foo(key))
})

It's Stainless SimplifierWithPC that eliminates the pattern matching

[samarion]

Regarding isSimpleBinding, could we extend the definition to handle multiple projections such as v.f1.f2?

Yes, good idea!

In the (((!inLambda && pe) || (inLambda && realPE)) && isSimpleBinding) condition, this should take care of the expression being pure?

Right. IIRC the convoluted logic with inLambda is due to recursion under lambdas but I'm not too sure anymore. Let's just use that condition to be safe.

---

Without it, the expression simplifies to true!

Haha that's indeed significantly worse :)

The idea sounds good, though it may need some rules to be extended?

I'm not sure the expression we're giving to simplify is any easier to handle than the original one. It seems to me that we should just drop this case.

---

It's Stainless SimplifierWithPC that eliminates the pattern matching

Ahh, I see. I forgot we had a Stainless-specific version. Maybe these lines are the true culprit for the issue then:

stainless/core/src/main/scala/stainless/transformers/SimplifierWithPC.scala

Lines 15 to 19 in 73eb421

	case Let(vd, a @ Annotated(ADTSelector(v: Variable, _), flags), b) if flags.contains(DropVCs) =>
	simplify(exprOps.replaceFromSymbols(Map(vd -> a), b), path)
	case Let(vd, cs @ ADTSelector(v: Variable, _), b) =>
	simplify(exprOps.replaceFromSymbols(Map(vd -> cs), b), path)

We should probably drop them once you've added the simple-binding case to Inox.

[mario-bucev]

OP hasn't responded to me yet if these changes are still working for him. They do for the test cases I have.