Verus not instantiating deeply nested `forall`s in functions

[pratapsingh1729]

We are attempting to work with a recursive datatype where the branching is controlled by a FnSpec. We want to write our own extensional equality predicate on these datatypes, but we are unable to do any proofs with it, since it seems that Verus will not instantiate the forall quantifier that we need for the extensionality. As a minimal example:

#[is_variant]
pub enum T {
    Base(nat),
    F(FnSpec(nat) -> T)
}

pub open spec fn is_equal (x : T, y : T) -> bool 
    decreases x 
{ 
    match x {
        T::Base(b) => x == y,
        T::F(ff) => match y {
            T::F(gg) => forall|v| #[trigger] is_equal(ff(v), gg(v)),
            _ => false
        }
    }
}

pub proof fn test(ff : FnSpec(nat) -> T, gg : FnSpec(nat) -> T) {
    assert ((forall |v| #[trigger] is_equal(ff(v), gg(v))) ==> is_equal(T::F(ff), T::F(gg))); // 1
    assert (is_equal(T::F(ff), T::F(gg)) ==> (forall |v| #[trigger] is_equal(ff(v), gg(v)))); // 2
}

Both of the assertions in test fail. It seems like both assertions should follow directly from "reducing" the definition of is_equal, so we aren't sure why this isn't going through.

NB: This only works in the new is_smaller_than branch from #570.

[pratapsingh1729]

Looking at the generated smt, we have the following which I think maps to assertion 1:

      (=>
       (forall ((v~22$ Poly)) (!
         (=>
          (has_type v~22$ NAT)
          (equality!is_equal.? (%%apply%%0 ff~2@ v~22$) (%%apply%%0 gg~4@ v~22$))
         )
         :pattern ((equality!is_equal.? (%%apply%%0 ff~2@ v~22$) (%%apply%%0 gg~4@ v~22$)))
         :qid user_equality__test_5
         :skolemid skolem_user_equality__test_5
       ))
       (equality!is_equal.? (Poly%equality!T. (equality!T./F (%Poly%fun%1. (Poly%fun%1. ff~2@))))
        (Poly%equality!T. (equality!T./F (%Poly%fun%1. (Poly%fun%1. gg~4@))))
     ))

But the axiom for the recursive case of is_equal has a pattern that uses equality!rec%is_equal.?:

(assert
 (forall ((x~2@ Poly) (y~4@ Poly) (fuel%@ Fuel)) (!
   (= (equality!rec%is_equal.? x~2@ y~4@ (succ fuel%@)) (ite
     (is-equality!T./Base (%Poly%equality!T. x~2@))
     (let
      ((b~18$ (equality!T./Base/_0 (%Poly%equality!T. x~2@))))
      (= x~2@ y~4@)
     )
     (let
      ((ff~32$ (equality!T./F/_0 (%Poly%equality!T. x~2@))))
      (and
       (is-equality!T./F (%Poly%equality!T. y~4@))
       (let
        ((gg~40$ (equality!T./F/_0 (%Poly%equality!T. y~4@))))
        (forall ((v~50$ Poly)) (!
          (=>
           (has_type v~50$ NAT)
           (equality!rec%is_equal.? (%%apply%%0 ff~32$ v~50$) (%%apply%%0 gg~40$ v~50$) fuel%@)
          )
          :pattern ((equality!rec%is_equal.? (%%apply%%0 ff~32$ v~50$) (%%apply%%0 gg~40$ v~50$)
            fuel%@
          ))
          :qid user_equality__is_equal_1
          :skolemid skolem_user_equality__is_equal_1
   )))))))
   :pattern ((equality!rec%is_equal.? x~2@ y~4@ (succ fuel%@)))
   :qid internal_equality!is_equal._fuel_to_body_definition
   :skolemid skolem_internal_equality!is_equal._fuel_to_body_definition
)))

And this quantifier is nested within the outer forall which is also patterned on the rec% version. However, another axiom should separately translate the query about the non-rec% version into the rec% version:

(assert
 (=>
  (fuel_bool fuel%equality!is_equal.)
  (forall ((x~2@ Poly) (y~4@ Poly)) (!
    (= (equality!is_equal.? x~2@ y~4@) (equality!rec%is_equal.? x~2@ y~4@ (succ fuel_nat%equality!is_equal.)))
    :pattern ((equality!is_equal.? x~2@ y~4@))
    :qid internal_equality!is_equal.?_definition
    :skolemid skolem_internal_equality!is_equal.?_definition
))))

But we aren't sure whether Z3 is applying these quantifiers correctly.

[pratapsingh1729]

On the other hand, the following works:

#[is_variant]
pub enum T {
    Base(nat),
    F(FnSpec(()) -> T)
}

pub open spec fn is_equal (x : T, y : T) -> bool 
    decreases x 
{ 
    match x {
        T::Base(b) => x == y,
        T::F(ff) => match y {
            T::F(gg) => is_equal(ff(()), gg(())),
            _ => false
        }
    }
}

pub proof fn test(ff : FnSpec(()) -> T, gg : FnSpec(()) -> T) {
    assert ((is_equal(ff(()), gg(()))) ==> is_equal(T::F(ff), T::F(gg)));
    assert (is_equal(T::F(ff), T::F(gg)) ==> (is_equal(ff(()), gg(()))));
}

(the same, except with () instead of nat so there are no quantifiers.)

So there is something going wrong with the deeply nested forall in this case.

[Chris-Hawblitzel]

It looks like using a recursive function like is_equal as a trigger from inside the function's own definition isn't working because the trigger ends up being the recursive encoding of the function for a particular amount of fuel. I'll take a closer look, but in the meantime, here is a workaround that simply makes up a different trigger that is independent of the recursive function definition:

spec fn trig(x: int) -> bool { true }

spec fn is_equal(x: T, y: T) -> bool 
    decreases x 
{ 
    match (x, y) {
        (T::Base(_), T::Base(_)) => x == y,
        (T::F(ff), T::F(gg)) => forall|v| #[trigger] trig(v) ==> is_equal(ff(v), gg(v)),
        _ => false
    }
}

...
    assert((forall|v| #[trigger] trig(v) ==> is_equal(ff(v), gg(v))) ==> is_equal(T::F(ff), T::F(gg))); // 1
    assert(is_equal(T::F(ff), T::F(gg)) ==> (forall|v| #[trigger] trig(v) ==> is_equal(ff(v), gg(v)))); // 2

[pratapsingh1729]

@Chris-Hawblitzel Thanks for the workaround! This appears to work for some small examples I tried.

[Chris-Hawblitzel]

My first reaction was that Verus was simply emitting the wrong trigger, and that having Verus emit the right trigger would fix the problem. However, after looking at this more closely and experimenting with different possible solutions, I'm becoming more convinced that there is no right trigger for this, and that this combination of recursion and quantifiers is hard for SMT solvers to handle.

First, let me introduce a simplified example:

spec fn pred(i: int) -> int { i - 1 }

spec fn f(i: int, j: int) -> bool
    decreases i
{
    i > 0 ==> (forall|j: int| #[trigger] f(pred(i), j))
}

proof fn test(i: int, j: int) {
    assert(
        f(i, j)
        ==
        (i > 0 ==> (forall|j: int| #[trigger] f(pred(i), j)))
    );
}

The assertion fails in the current Verus implementation. However, the assertion also fails in Dafny and F*:

function pred(i: int): int { i - 1 }

ghost predicate f(i: int, j: int)
    decreases i
{
    i > 0 ==> (forall j: int :: f(pred(i), j))
}

lemma test(i: int, j: int)
{
    assert
        f(i, j)
        ==
        (i > 0 ==> (forall j: int :: f(pred(i), j)))
        ;
}

let pred (i:int) : int = i - 1

let rec f (i:int) (j:int) =
  i > 0 ==> (forall (j:int). (f (pred i) j))

let test (i:int) (j:int) =
  assert (
    f i j
    ==
    (i > 0 ==> (forall (j:int). (f (pred i) j)))
  )

(The Dafny and F* versions fail regardless of whether you explicitly make f(pred(i), j) the trigger. In fairness, you can get the assertion to work in Dafny by breaking it up into two assertions, one with ==> and one with <==, but nevertheless, this example shows that even in Dafny, f(i, j) is not seamlessly interchangeable with i > 0 ==> (forall j: int :: f(pred(i), j)).)

What's dismaying about the assertion failure is that the assertion appears at the source level to be a direct expansion of f's definition: we're simply asserting that f, applied to its arguments, equals its body. However, in the SMT encoding, the assertion is different from f's body, due to the fuel-based encoding of recursion (in Verus, Dafny, and F*). In the SMT encoding, the translation of f(pred(i), j) in the assertion is:

(f.? (I (pred.? (I i!))) j$)

whereas the translation of f(pred(i), j) in f's body is:

(rec%f.? (I (pred.? i!)) j$ fuel%)

The problem is that triggering is based on matching terms, and these two different terms, (f.? (I (pred.? (I i!))) j$) and (rec%f.? (I (pred.? i!)) j$ fuel%), don't match. Moreover, they don't match for an important reason: to stop the infinite matching loops that would be generated by f's definition axiom if f's body refered directly to (f.? (I (pred.? (I i!))) j$). This is the whole point of the fuel-based encoding used by Verus, Dafny, and F*. Furthermore, any attempt to make the different translations of f(pred(i), j) inside and outside of f match, or to make their triggers match, risks recreating the matching loop that we're trying to avoid.

For what it's worth, I committed what I originally thought would be a simple fix to a branch ( https://github.com/verus-lang/verus/tree/recursive-trigger-no-rename ), but it only half fixes the problem: it makes f(i, j) imply (i > 0 ==> (forall|j: int| #[trigger] f(pred(i), j))), but not the other way around. The difficulty is that if you assume (forall|j: int| #[trigger] f(pred(i), j)) outside of f's definition, you're making an assumption that triggers on (f.? (I (pred.? (I i!))) j$), and inside f's definition, there are no terms that match this (there is only (rec%f.? (I (pred.? i!)) j$ fuel%)), so the quantifier never gets triggered. You could imagine trying to get the quantifier outside f's definition to also trigger on (rec%f.? (I (pred.? i!)) j$ fuel%), but this risks matching loops.

So my feeling now is that allowing triggers on f's recursive calls inside f's own definition is going to lead to bad experiences for users, where obvious looking equalities fail to hold. Instead, I think it's safer to go with the workaround of introducing a separate artificial trigger that is defined outside the recursive definition. This is a fairly rare situation anyway; most recursive definitions don't contain quantifiers that trigger recursively on their own definition. So my plan is to disallow using f in a trigger inside f's own recursive definition, and print out a message suggesting the workaround. I've committed this to https://github.com/verus-lang/verus/compare/recursive-trigger-disallow . If there are no objections, I'll merge it into main.

[pratapsingh1729]

Thanks very much for the detailed explanation and investigation! Sorry I didn't get to this until now.

It does make sense, now that you have explained and shown the actual triggers, that allowing triggers on recursive calls to f inside of the definition of f would either generate matching loops or just fail to ever work due to the explicit introduction of fuel in the SMT query. I think the error message in the branch you posted explains the issue well, and would definitely be helpful for others who might end up wanting to do the same kind of thing I wanted to do. In my case the dummy trigger approach worked just fine.