Triggers silently ignored/replaced

[fpoli]

For some reason, the following program verifies even if the apply_on tigger is not used in test. Removing the precondition of apply_on makes the program fail as expected. Both versions of the program don't verify in Carbon.

function apply_on(a: Int): Bool
  requires 0 <= a && a <= 18446744073709551615

function opaque_property(a: Int, k: Int): Int

method test() {
  var a: Int
  assume forall k: Int :: { apply_on(k) } opaque_property(a, k) == 100

  assert opaque_property(a, 123) == 100
}

[mschwerhoff]

That's due to how Silicon handles triggers. In your example, the trigger { apply_on(k) } is silently (good design choice) ignored because 1. it is a program function (heap-dependent function) and 2. does not occur in the quantifier body. If you use a domain function instead, the trigger makes it to the SMT solver and the final assertion cannot be verified.

To understand the root problem, here's a bit of context. Imagine the following program (concrete types irrelevant):

function foo(x)
  requires A

method main() {
  ...
  inhale forall y :: {foo(x)} A1 && (A2 ==> A3) && A4
}

Symbolically evaluating foo(x) entails computing foo's heap footprint, which (in current Silicon) entails temporarily exhaling A. However, it is not clear when A is supposed to hold: before inhaling A1? After A1 and A2? Etc. Silicon sidesteps the problem by recording the symbolic terms corresponding to function application while going over the quantifier body, and reusing them to translate triggers. If a trigger doesn't occur in the body, however, it is silently ignored.

[marcoeilers]

Couldn't we trigger on the stateless version of the function in that case?

[mschwerhoff]

Yes, that should work. We should get rid of heap-dependent triggers anyway ... :-)

[fpoli]

Thanks! So far I thought that Viper functions are heap-dependent only when they require predicates or permissions in their precondition.

That's due to how Silicon handles triggers. In your example, the trigger { apply_on(k) } is silently (good design choice) ignored because 1. it is a program function (heap-dependent function) and 2. does not occur in the quantifier body. If you use a domain function instead, the trigger makes it to the SMT solver and the final assertion cannot be verified.

Wouldn't a warning or error message be better than silently ignoring explicit triggers? Especially if ignoring the triggers makes Silicon/Z3 choose triggers on its own, which can introduce matching loops.

[mschwerhoff]

We don't have a good term for non-domain functions, and simply called them heap-dependent so far. If they don't access the heap, their footprint is empty, but they nonetheless have one.

Yes, emitting a warning would be better. I don't think these are shown in the IDE, though.

[marcoeilers]

Warnings, at least some kinds (see for example this

silicon/src/main/scala/verifier/DefaultMainVerifier.scala

Line 160 in 228387a

reporter.report(WarningsDuringTypechecking(Seq(TypecheckerWarning("No triggers provided or inferred for quantifier.", res.pos))))

) are shown in the IDE.

[Aurel300]

(Tangential:) For front-ends it might make sense to have a mode like -Werror for C compilers, which would turn any warning into an error that we must handle as part of the verification result…