Using a call to a FnSpec as a trigger

[marshtompsxd]

Initially requested by @marshtompsxd.

The intent is to be able to write:

proof fn something(a: FnSpec(s)->bool, b: FnSpec(s)->bool)
  ensures forall|s: S| a(s) ==> b(s)
{ ... }

spec fn prop_1(s: S);
spec fn prop_2(s: S);

proof fn foo {
  something(|s| prop_1(s), |s| prop_2(s));
  assume(prop_1(s));
  assert(prop_2(s)); // this should pass
}

which is currently rejected because something's ensures doesn't have a valid trigger.

---

Original message by @marshtompsxd:

Hi Verus team,
I am writing a function that takes a closure as a parameter. The closure is later used in forall but Verus only allows "a function call, a field access, or a bitwise operator" to be a trigger. Is it possible to make a closure call be a trigger?

[marshtompsxd]

Just follow up.
I am using 6d90cb8
If I have closure inside forall, Verus sometimes reports an error that it cannot automatically find trigger.

And the problem of not being able to set closure as trigger still exists

[marshtompsxd]

Follow up:
We want to write something like

forall |t: T| p(t) ==> q(t)

and both p and q are FnSpec(T) -> bool. Such quantifiers appear in both ensures/requires and inside proof.

[utaal]

Supporting this may require synthesizing a trigger name for the FnSpec call, which may be possible, but I need to take another look at the encoding.

[utaal]

There's a draft PR for this here: #331

[utaal]

There is now support for this. Marking as resolved.