Trigger inference infers invalid triggers

[vakaras]

If one tries to verify the following Viper program:

function offset(start: Ref, index: Int): Ref

method test(start: Ref, l: Int)
    ensures forall ii: Int :: 0 <= ii && ii < l ==> offset(start, 0 + ii) == old(offset(start, 1 + ii))
{
}

they will get the following error message:

Silicon found 1 error in 5,26s:
  [0] Postcondition of test might not hold. Assertion (forall __rw_ii1: Int, __rw_ii2: Int :: { offset(start, __rw_ii1) } { offset(start, __rw_ii2) } true && __rw_ii1 - 0 == __rw_ii2 - 1 ==> 0 <= __rw_ii1 - 0 && __rw_ii1 - 0 < l ==> offset(start, __rw_ii1) == old(offset(start, __rw_ii2))) might not hold. (dedup_by.vpr@5.13--5.104)

Potential incompleteness: Some((:reason-unknown "(incomplete quantifiers)"))

which shows that Viper inferred invalid triggers for the quantifier.

Z3 rejects this trigger, as witnessed by the following message in the log:

13:50:45.129 [ForkJoinPool-1-worker-3] WARN viper.silicon.decider.Z3ProverStdIO - Prover warning: WARNING: (642,21): pattern does not contain all quantified variables.

cc @marcoeilers

The credit for noticing this goes to Olivia.

[fpoli]

Why is a forall with a single quantified variable rewritten to a forall with two quantified variables? Does Silicon do it frequently?

[marcoeilers]

The trigger generation code (I think only in Silicon?) does it when all possible trigger expressions it finds in the quantifier body contain arithmetic, like in this example. offset(start, 0 + ii) would be the natural trigger expression, but that is invalid, because it contains an addition. So Silicon rewrites the quantifier to an equivalent one where it replaces the addition expression 0 + ii with a new quantified variable and constrains it accordingly. So it can trigger on offset(start, newVar) and rewrites the body s.t. newVar must be 0 + ii.

[fpoli]

I see, thanks! Just to be sure, the extra quantified variable can only be introduced when the user does not specify the triggers, right? Otherwise it'd be really hard to reason about the maximum number of QI of domain axioms.

[marcoeilers]

As far as I know that's correct, yes.