Closed andreagilot-da closed 1 year ago
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.
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:
foo(key)
by false
inside bar
, and this makes the verification work.key
argument from the function foo
either by replacing it with foo
or foo()
and both make verification work.BigInt
either for the argument or result type of bar
and both make the verification work.Unit
(in the list) by any other type, including a generic type does not change anything.key
of foo
does not seem to change anything.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
).
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):
https://github.com/epfl-lara/stainless/blob/33a990a7b69470bc7ea529b9e602162febd7987e/core/src/main/scala/stainless/verification/VerificationChecker.scala#L140-L142
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?
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 https://github.com/epfl-lara/inox/pull/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!
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 https://github.com/epfl-lara/inox/pull/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?
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.
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
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: https://github.com/epfl-lara/stainless/blob/73eb421de6a21ecb5d2812c686bf6a7eb1d1282a/core/src/main/scala/stainless/transformers/SimplifierWithPC.scala#L15-L19
We should probably drop them once you've added the simple-binding case to Inox.
OP hasn't responded to me yet if these changes are still working for him. They do for the test cases I have.
Stainless timeouts when verifying that
bar
is actually equal to its body.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.
In Scala 3, the first snippet verifies but there is still the same problem for the second one.