Check Associate-Pred signatures

[ranjitjhala]

We should try making the following definition work without trusting it:

#[flux::sig(fn<T as base>(&{T[@x] | <T as MyTrait>::f(x)}))]
pub fn bob<T: MyTrait>(x: &T) {
    x.method();
}

We just need to encode the associated predicate as an uninterpreted function. We could generalize refine_tree::NodeKind::Guard to contain a Pred and then do something similar to FixpointCtxt::collect_sorts to collect the abstract refinements needed to encode the constraint.

Originally posted by @nilehmann in https://github.com/flux-rs/flux/pull/597#pullrequestreview-1816072205

[ranjitjhala]

Hmm, I think this is a bit trickier, as ultimately, to do the sort checking (and determine the sort of the uninterpreted function in the fixpoint encoding) you want to "normalize" to determine that

1. In the specification of MyTrait, we know f : Self -> bool and
2. In this instance <T as MyTrait> tells you that the Self is T and so
3. The <T as MyTrait>::f is of type T -> bool.

A more lassez-faire approach would be to recover the type from the arguments, from x but that can get messy e.g. if we use the <T as MyTrait>::f at two different sorted index/arguments in the same signature.

Am I missing something? [RJ: edit -- see #599]

[ranjitjhala]

Actually, now that I've written it all out, it doesn't seem so bad so I'll just do it! :-)

[nilehmann]

I'm talking specifically about the cases where the associated predicate cannot be normalized away. In those cases both the predicate and the sort remain abstract.

[nilehmann]

More concretely, given something like

#[flux::generics(Self as base)]
#[flux::predicate(f: (Self) -> bool)]
trait MyTrait {
    #[flux::sig(fn(self: &Self{v: <Self as MyTrait>::f(v)}) -> Self{v: <Self as MyTrait>::f(v)}]
    fn method(&self) -> Self;
}

#[flux::sig(fn<T as base>(&T{v: <T as MyTrait>::f(x)}) -> T{v: <T as MyTrait>::f(x)})]
pub fn bob<T: MyTrait>(x: &T) ->  T {
    x.method()
}

we should generate a constraint that looks like this (in pseudo fixpoint)

(declare-sort MyTrait)
(declare-fun f (MyTrait) Bool)

(constraint
  (forall ((a1 MyTrait) (f a1))
      (and
        (f a1)
        (forall ((a2 MyTrait) (f a2))
          (f a2)
        )
      )
    )
)

I believe the fixpoint horn syntax doesn't support declaring sorts, but we can encode Sort::Param as int, which I think we are already doing.

[ranjitjhala]

I believe this is already implemented, see this