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

…bounds (#750)

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

* merge

source/rust_verify/src/rust_to_vir.rs

@@ -280,11 +280,24 @@ fn check_item<'tcx>(
                         false,
                     )?);
                 }
+                let types = Arc::new(types);
                 let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, path.res.def_id());
-                let trait_impl =
-                    vir::ast::TraitImplX { impl_path: impl_path.clone(), trait_path: path.clone() };
+                let (typ_params, typ_bounds) = crate::rust_to_vir_base::check_generics_bounds_fun(
+                    ctxt.tcx,
+                    &ctxt.verus_items,
+                    impll.generics,
+                    impl_def_id,
+                    Some(&mut *ctxt.diagnostics.borrow_mut()),
+                )?;
+                let trait_impl = vir::ast::TraitImplX {
+                    impl_path: impl_path.clone(),
+                    typ_params,
+                    typ_bounds,
+                    trait_path: path.clone(),
+                    trait_typ_args: types.clone(),
+                };
                 vir.trait_impls.push(ctxt.spanned_new(item.span, trait_impl));
-                Some((path, Arc::new(types)))
+                Some((path, types))
             } else {
                 None
             };
@@ -553,6 +566,7 @@ fn check_item<'tcx>(
             vir.functions.append(&mut methods);
             let traitx = vir::ast::TraitX {
                 name: trait_path,
+                visibility: visibility(),
                 methods: Arc::new(method_names),
                 assoc_typs: Arc::new(assoc_typs),
                 typ_params: generics_params,

source/rust_verify/src/verifier.rs

@@ -881,6 +881,15 @@ impl Verifier {
             &("Datatypes".to_string()),
         );
 
+        let trait_commands = vir::traits::traits_to_air(ctx, &krate);
+        self.run_commands(
+            module,
+            reporter,
+            &mut air_context,
+            &trait_commands,
+            &("Traits".to_string()),
+        );
+
         let assoc_type_impl_commands =
             vir::assoc_types_to_air::assoc_type_impls_to_air(ctx, &krate.assoc_type_impls);
         self.run_commands(
@@ -1311,14 +1320,15 @@ impl Verifier {
             reporter.report_now(&note_bare(format!("verifying {module_msg}{functions_msg}")));
         }
 
-        let (pruned_krate, mono_abstract_datatypes, lambda_types) =
+        let (pruned_krate, mono_abstract_datatypes, lambda_types, bound_traits) =
             vir::prune::prune_krate_for_module(&krate, &module, &self.vstd_crate_name);
         let mut ctx = vir::context::Ctx::new(
             &pruned_krate,
             global_ctx,
             module.clone(),
             mono_abstract_datatypes,
             lambda_types,
+            bound_traits,
             self.args.debug,
         )?;
         let poly_krate = vir::poly::poly_krate_for_module(&mut ctx, &pruned_krate);

source/rust_verify_test/tests/recursion.rs

@@ -797,7 +797,7 @@ test_verify_one_file! {
         //#[verifier(decreases_by)]
         proof fn check_arith_sum(i: int) {
         }
-    } => Err(err) => assert_vir_error_msg(err, "proof function must be marked #[verifier(decreases_by)] or #[verifier(recommends_by)] to be used as decreases_by/recommends_by")
+    } => Err(err) => assert_vir_error_msg(err, "proof function must be marked #[verifier::decreases_by] or #[verifier::recommends_by] to be used as decreases_by/recommends_by")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/traits.rs

@@ -74,30 +74,6 @@ test_verify_one_file! {
     } => Ok(())
 }
 
-test_verify_one_file! {
-    #[test] test_not_yet_supported_10 verus_code! {
-        trait T {
-            spec fn f(&self) -> bool;
-
-            proof fn p(&self)
-                ensures exists|x: &Self| self.f() != x.f();
-        }
-
-        #[verifier::external_body] /* vattr */
-        #[verifier::broadcast_forall] /* vattr */
-        proof fn f_not_g<A: T>()
-            ensures exists|x: &A, y: &A| x.f() != y.f()
-        {
-        }
-
-        struct S {}
-
-        fn test() {
-            assert(false);
-        }
-    } => Err(err) => assert_vir_error_msg(err, ": bounds on broadcast_forall function type parameters")
-}
-
 test_verify_one_file! {
     #[test] test_not_yet_supported_11 verus_code! {
         trait T {
@@ -1194,6 +1170,138 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    #[test] test_broadcast_forall1 verus_code! {
+        trait T {
+            spec fn f(&self) -> bool;
+
+            proof fn p(&self)
+                ensures exists|x: &Self| self.f() != x.f();
+        }
+
+        spec fn g<A: T>() -> bool {
+            exists|x: &A, y: &A| x.f() != y.f()
+        }
+        spec fn t<A>() -> bool { true }
+
+        #[verifier::external_body] /* vattr */
+        #[verifier::broadcast_forall] /* vattr */
+        proof fn f_not_g<A: T>()
+            ensures
+                #[trigger] t::<A>(),
+                g::<A>(),
+        {
+        }
+
+        struct S1 {}
+        impl T for S1 {
+            spec fn f(&self) -> bool {
+                true
+            }
+
+            proof fn p(&self) {
+                assert(exists|x: &Self| self.f() != x.f()); // FAILS
+            }
+        }
+
+        struct S2 {}
+
+        struct S3(bool);
+        impl T for S3 {
+            spec fn f(&self) -> bool {
+                self.0
+            }
+
+            proof fn p(&self) {
+                assert(self.f() != S3(!self.0).f())
+            }
+        }
+
+        fn test1() {
+            assert(t::<S1>());
+            assert(false);
+        }
+
+        fn test2() {
+            assert(t::<S2>());
+            assert(false); // FAILS
+        }
+
+        fn test3() {
+            assert(t::<S3>());
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 3)
+}
+
+test_verify_one_file! {
+    #[test] test_broadcast_forall2 verus_code! {
+        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
+        }
+    } => Err(err) => assert_fails(err, 2)
+}
+
+test_verify_one_file! {
+    #[test] test_decreases_trait_bound verus_code! {
+        trait T {
+            proof fn impossible()
+                ensures false;
+        }
+
+        spec fn f<A: T>(i: int) -> bool
+            decreases 0int when true via f_decreases::<A>
+        {
+            !f::<A>(i - 0)
+        }
+
+        #[verifier::decreases_by]
+        proof fn f_decreases<A: T>(i: int) {
+            A::impossible();
+        }
+
+        proof fn test1<A: T>(i: int) {
+            assert(f::<A>(i) == !f::<A>(i - 0));
+            assert(false);
+        }
+
+        proof fn test2() {
+            // We'd like to test that f's definition axiom only applies to A that implement T.
+            // Ideally, we'd test this by applying f to an A that doesn't implement T
+            // and seeing that the definition axiom doesn't apply.
+            // Unfortunately, it's hard to test this because Rust's type checker already (correctly)
+            // stops us from saying f::<ty>(x) for ty that doesn't implement T.
+            // So we have to manually check the AIR code for the axiom off line.
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 1)
+}
+
 test_verify_one_file! {
     #[test] test_synthetic_type_params verus_code!{
         spec fn global_type_id<A>() -> int;

source/rust_verify_test/tests/traits_modules.rs

@@ -68,38 +68,6 @@ test_verify_one_file! {
     } => Ok(())
 }
 
-test_verify_one_file! {
-    #[test] test_not_yet_supported_10 verus_code! {
-        mod M1 {
-            pub trait T {
-                spec fn f(&self) -> bool;
-
-                proof fn p(&self)
-                    ensures exists|x: &Self| self.f() != x.f();
-            }
-        }
-
-        mod M2 {
-            #[verifier::external_body] /* vattr */
-            #[verifier::broadcast_forall] /* vattr */
-            proof fn f_not_g<A: crate::M1::T>()
-                ensures exists|x: &A, y: &A| x.f() != y.f()
-            {
-            }
-        }
-
-        mod M3 {
-            struct S {}
-        }
-
-        mod M4 {
-            fn test() {
-                assert(false);
-            }
-        }
-    } => Err(err) => assert_vir_error_msg(err, ": bounds on broadcast_forall function type parameters")
-}
-
 test_verify_one_file! {
     #[test] test_ill_formed_7 code! {
         mod M1 {

source/rust_verify_test/tests/traits_modules_pub_crate.rs

@@ -69,38 +69,6 @@ test_verify_one_file! {
     } => Ok(())
 }
 
-test_verify_one_file! {
-    #[test] test_not_yet_supported_10 verus_code! {
-        mod M1 {
-            pub(crate) trait T {
-                spec fn f(&self) -> bool;
-
-                proof fn p(&self)
-                    ensures exists|x: &Self| self.f() != x.f();
-            }
-        }
-
-        mod M2 {
-            #[verifier::external_body] /* vattr */
-            #[verifier::broadcast_forall] /* vattr */
-            proof fn f_not_g<A: crate::M1::T>()
-                ensures exists|x: &A, y: &A| x.f() != y.f()
-            {
-            }
-        }
-
-        mod M3 {
-            struct S {}
-        }
-
-        mod M4 {
-            fn test() {
-                assert(false);
-            }
-        }
-    } => Err(err) => assert_vir_error_msg(err, ": bounds on broadcast_forall function type parameters")
-}
-
 test_verify_one_file! {
     #[test] test_ill_formed_7 code! {
         mod M1 {

source/vir/src/ast.rs

@@ -224,6 +224,8 @@ pub enum ModeCoercion {
 pub enum NullaryOpr {
     /// convert a const generic into an expression, as in fn f<const N: usize>() -> usize { N }
     ConstGeneric(Typ),
+    /// predicate representing a satisfied trait bound T(t1, ..., tn) for trait T
+    TraitBound(Path, Typs),
 }
 
 /// Primitive unary operations
@@ -925,6 +927,7 @@ pub type Trait = Arc<Spanned<TraitX>>;
 #[derive(Clone, Debug, Serialize, Deserialize, ToDebugSNode)]
 pub struct TraitX {
     pub name: Path,
+    pub visibility: Visibility,
     // REVIEW: typ_params does not yet explicitly include Self (right now, Self is implicit)
     pub typ_params: TypPositives,
     pub typ_bounds: GenericBounds,
@@ -942,7 +945,7 @@ pub struct AssocTypeImplX {
     pub typ_params: Idents,
     pub typ_bounds: GenericBounds,
     pub trait_path: Path,
-    pub trait_typ_args: Arc<Vec<Typ>>,
+    pub trait_typ_args: Typs,
     pub typ: Typ,
 }
 
@@ -951,7 +954,11 @@ pub type TraitImpl = Arc<Spanned<TraitImplX>>;
 pub struct TraitImplX {
     /// Path of the impl (e.g. "impl2")
     pub impl_path: Path,
+    // typ_params of impl (unrelated to typ_params of trait)
+    pub typ_params: Idents,
+    pub typ_bounds: GenericBounds,
     pub trait_path: Path,
+    pub trait_typ_args: Typs,
 }
 
 #[derive(Clone, Debug, Hash, Serialize, Deserialize, ToDebugSNode, PartialEq, Eq)]