Encode trait bounds in AIR/SMT to enable broadcast_forall with trait bounds

[Chris-Hawblitzel]

Up to now, broadcast_forall was only allowed for proof functions with no trait bounds. This pull request adds AIR/SMT encodings of trait bounds so that we generate axioms for broadcast_forall that can include trait bounds as preconditions. This is also relevant to #744 , since axioms about spec function ensures may need preconditions for trait bounds.

Here is an example test:

trait T1<A, B> {}
trait T2<C, D> {}

struct S<E>(E);

impl<X> T1<X, bool> for S<X> {}
impl<Y, Z: T1<int, Y>> T2<Z, u16> for S<(Y, u8)> {}

spec fn f<A>(i: int) -> bool;

#[verifier::external_body]
#[verifier::broadcast_forall]
proof fn p<A: T2<S<int>, u16>>(i: int)
    ensures f::<A>(i)
{
}

proof fn test1() {
    assert(f::<S<(bool, u8)>>(3));
}

proof fn test2() {
    assert(f::<S<(u32, u8)>>(3)); // FAILS
}

proof fn test3() {
    assert(f::<S<(bool, u32)>>(3)); // FAILS
}

In this, only test1 succeeds, because p's trait bound A: T2<S<int>, u16> is satisfied by A = S<(bool, u8)> but not by A = S<(u32, u8)> or A = S<(bool, u32)>. For Z3 to see that the trait bound is satisfied, we need to encode the trait bounds as AIR/SMT predicates. This encoding looks like the following, where each relevant trait impl becomes an axiom:

(declare-fun tr_bound%!T1. (Dcr Type Dcr Type Dcr Type) Bool)
(declare-fun tr_bound%!T2. (Dcr Type Dcr Type Dcr Type) Bool)
(axiom (forall ((X&. Dcr) (X& Type)) (!
   (tr_bound%!T1. $ (TYPE%!S. X&. X&) X&. X& $ BOOL)
   :pattern ((tr_bound%!T1. $ (TYPE%!S. X&. X&) X&. X& $ BOOL))
)))
(axiom (forall ((Y&. Dcr) (Y& Type) (Z&. Dcr) (Z& Type)) (!
   (=>
    (tr_bound%!T1. Z&. Z& $ INT Y&. Y&)
    (tr_bound%!T2. $ (TYPE%!S. $ (TYPE%tuple%2. Y&. Y& $ (UINT 8))) Z&.
     Z& $ (UINT 16)
   ))
   :pattern ((tr_bound%!T2. $ (TYPE%!S. $ (TYPE%tuple%2. Y&. Y& $ (UINT 8)))
     Z&. Z& $ (UINT 16)
   ))
)))

With this, the axiom for p's broadcast_forall can use the trait bound tr_bound%!T2. as a precondition, so that it only applies to A that satisfy the proper T2 trait bound:

(axiom (forall ((A&. Dcr) (A& Type) (i~2$ Poly)) (!
   (=>
    (has_type i~2$ INT)
    (=>
     (tr_bound%!T2. A&. A& $ (TYPE%!S. $ INT) $ (UINT 16))
     (!f.? A&. A& i~2$)
   ))
   :pattern ((!f.? A&. A& i~2$))
)))

[utaal]

Let me check my understanding: in the example:

(declare-fun tr_bound%!T1. (Dcr Type Dcr Type Dcr Type) Bool)

The first Dcr Type is the type that conforms to the bound;
the other Dcr Types are the type arguments to T1.

Is that right?

[Chris-Hawblitzel]

Let me check my understanding: in the example:

(declare-fun tr_bound%!T1. (Dcr Type Dcr Type Dcr Type) Bool)

The first Dcr Type is the type that conforms to the bound; the other Dcr Types are the type arguments to T1.

Is that right?

Yes, internally T1 is viewed as having 3 type parameters, Self, A, and B, so the first Dcr Type is for Self. Internally, the bound Z: T1<int, Y> is viewed as being a predicate T1(Z, int, Y) instantiating Self = Z, A = int, B = Y.