Make sure trait spec function axioms are guarded by trait bounds

(first step for #1094 )

source/rust_verify_test/tests/assoc_type_impls.rs

@@ -321,6 +321,188 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    #[test] trait_typ_equality1 verus_code! {
+        trait T {
+            type X;
+            type Y: Copy;
+            spec fn f(x: &Self::X, y: &Self::Y) -> Self::X {
+                *x
+            }
+            fn g(x: &Self::X, y: &Self::Y) -> Self::Y {
+                *y
+            }
+        }
+
+        impl T for bool {
+            type X = u8;
+            type Y = u16;
+            spec fn f(x: &Self::X, y: &Self::Y) -> Self::X {
+                (*x + *y) as u8
+            }
+            fn g(x: &Self::X, y: &Self::Y) -> (r: Self::Y)
+                ensures r == *x as u16 + *y / 2
+            {
+                *x as u16 + *y / 2
+            }
+        }
+
+        spec fn s1<A: T<X = u8>>(y: A::Y) -> u8 {
+            A::f(&3u8, &y)
+        }
+
+        spec fn s2<A: T<X = u8>>(y: A::Y) -> u8 {
+            A::f(&3u8, &y) / 2
+        }
+
+        proof fn test1<A: T<X = u8>>(y: A::Y) {
+            assert(s1::<A>(y) == A::f(&3u8, &y));
+        }
+
+        fn test2() {
+            assert(s1::<bool>(7u16) == <bool as T>::f(&3u8, &7u16));
+            assert(s1::<bool>(7u16) == 10u8);
+            assert(s2::<bool>(7u16) == 5u8);
+            let r = <bool as T>::g(&3u8, &7u16);
+            assert(r == 6u8);
+            assert(r == 7u8); // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] trait_typ_equality_struct verus_code! {
+        trait T {
+            type X;
+            type Y;
+        }
+
+        struct S<A: T<X = u8>> {
+            x: A::X,
+        }
+        impl T for bool {
+            type X = u8;
+            type Y = u16;
+        }
+        proof fn test() {
+            let s: S<bool> = S { x: 10u8 };
+            assert(s.x == 10);
+            assert(s.x == 11); // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] trait_typ_equality_broadcast verus_code! {
+        trait T {
+            type X;
+            type Y;
+        }
+
+        spec fn p<A>(a: A) -> bool;
+        spec fn q<A, B>(a: A, b: B) -> bool { true }
+
+        #[verifier::external_body]
+        proof fn p_u8(u: u8)
+            ensures p(u)
+        {
+        }
+
+        broadcast proof fn b<A: T<X = u8>>(x: A::X, a: A)
+            ensures #[trigger] q(a, x) && p(x)
+        {
+            p_u8(x);
+        }
+
+        impl T for u16 {
+            type X = u8;
+            type Y = i8;
+        }
+
+        impl T for u32 {
+            type X = u64;
+            type Y = i64;
+        }
+
+        proof fn test() {
+            broadcast use b;
+            assert(q(5u16, 10u8));
+            assert(p(10u8));
+            assert(q(5u32, 11u8));
+            assert(p(11u8)); // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] trait_typ_equality_dispatch_spec verus_code! {
+        trait U { type X; }
+        impl U for char { type X = u8; }
+        impl U for bool { type X = u16; }
+
+        trait T { spec fn f() -> int; }
+        impl<A: U<X = u8>> T for A { spec fn f() -> int { 100 } }
+        impl T for bool { spec fn f() -> int { 200 } }
+
+        proof fn test() {
+            assert(<char as T>::f() == 100);
+            assert(<bool as T>::f() == 200);
+            assert(<char as T>::f() == 200); // FAILS
+            assert(<bool as T>::f() == 100);
+            assert(false);
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] trait_typ_equality_dispatch_proof verus_code! {
+        trait U { type X; }
+        impl U for char { type X = u8; }
+        impl U for bool { type X = u16; }
+
+        trait T { proof fn f() -> int; }
+        impl<A: U<X = u8>> T for A { proof fn f() -> (r: int) ensures r == 100 { 100 } }
+        impl T for bool { proof fn f() -> (r: int) ensures r == 200 { 200 } }
+
+        proof fn test() {
+            let x = <char as T>::f();
+            assert(x == 100);
+            let x = <bool as T>::f();
+            assert(x == 200);
+            let x = <char as T>::f();
+            assert(x == 200); // FAILS
+            let x = <bool as T>::f();
+            assert(x == 100);
+            assert(false);
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] trait_typ_bound_no_dispatch verus_code! {
+        trait R {}
+        impl R for u8 {}
+        trait T {
+            spec fn f() -> int;
+        }
+        trait U {
+            type X;
+        }
+        impl<A: U> T for A where A::X: R { spec fn f() -> int { 100 } }
+        impl U for char { type X = u8; }
+        impl U for bool { type X = u16; }
+        impl T for bool { spec fn f() -> int { 200 } }
+
+        proof fn test() {
+            assert(<char as T>::f() == 100);
+            assert(<bool as T>::f() == 200);
+            assert(<char as T>::f() == 200);
+            assert(<bool as T>::f() == 100);
+            assert(false);
+        }
+    } => Err(err) => assert_rust_error_msg(err, "conflicting implementations")
+}
+
 test_verify_one_file! {
     #[test] trait_assoc_type_bound_mutual_bounds_0 verus_code! {
         trait A: B {

source/rust_verify_test/tests/traits.rs

@@ -2402,6 +2402,23 @@ test_verify_one_file! {
     } => Err(err) => assert_one_fails(err)
 }
 
+test_verify_one_file! {
+    #[test] test_specialize_dispatch_by_bound verus_code! {
+        struct S;
+        trait U {}
+
+        trait T { spec fn f() -> int; }
+        impl T for S { spec fn f() -> int { 100 } }
+        impl<A: U> T for A { spec fn f() -> int { 200 } }
+
+        proof fn test() {
+            assert(<S as T>::f() == 100);
+            assert(<S as T>::f() == 200); // FAILS
+            assert(false);
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
 test_verify_one_file! {
     #[test] test_trait_inline verus_code! {
         pub trait T<A> { spec fn f(&self) -> int; }
@@ -3040,119 +3057,6 @@ test_verify_one_file! {
     } => Ok(())
 }
 
-test_verify_one_file! {
-    #[test] trait_typ_equality1 verus_code! {
-        trait T {
-            type X;
-            type Y: Copy;
-            spec fn f(x: &Self::X, y: &Self::Y) -> Self::X {
-                *x
-            }
-            fn g(x: &Self::X, y: &Self::Y) -> Self::Y {
-                *y
-            }
-        }
-
-        impl T for bool {
-            type X = u8;
-            type Y = u16;
-            spec fn f(x: &Self::X, y: &Self::Y) -> Self::X {
-                (*x + *y) as u8
-            }
-            fn g(x: &Self::X, y: &Self::Y) -> (r: Self::Y)
-                ensures r == *x as u16 + *y / 2
-            {
-                *x as u16 + *y / 2
-            }
-        }
-
-        spec fn s1<A: T<X = u8>>(y: A::Y) -> u8 {
-            A::f(&3u8, &y)
-        }
-
-        spec fn s2<A: T<X = u8>>(y: A::Y) -> u8 {
-            A::f(&3u8, &y) / 2
-        }
-
-        proof fn test1<A: T<X = u8>>(y: A::Y) {
-            assert(s1::<A>(y) == A::f(&3u8, &y));
-        }
-
-        fn test2() {
-            assert(s1::<bool>(7u16) == <bool as T>::f(&3u8, &7u16));
-            assert(s1::<bool>(7u16) == 10u8);
-            assert(s2::<bool>(7u16) == 5u8);
-            let r = <bool as T>::g(&3u8, &7u16);
-            assert(r == 6u8);
-            assert(r == 7u8); // FAILS
-        }
-    } => Err(err) => assert_one_fails(err)
-}
-
-test_verify_one_file! {
-    #[test] trait_typ_equality_struct verus_code! {
-        trait T {
-            type X;
-            type Y;
-        }
-
-        struct S<A: T<X = u8>> {
-            x: A::X,
-        }
-        impl T for bool {
-            type X = u8;
-            type Y = u16;
-        }
-        proof fn test() {
-            let s: S<bool> = S { x: 10u8 };
-            assert(s.x == 10);
-            assert(s.x == 11); // FAILS
-        }
-    } => Err(err) => assert_one_fails(err)
-}
-
-test_verify_one_file! {
-    #[test] trait_typ_equality_broadcast verus_code! {
-        trait T {
-            type X;
-            type Y;
-        }
-
-        spec fn p<A>(a: A) -> bool;
-        spec fn q<A, B>(a: A, b: B) -> bool { true }
-
-        #[verifier::external_body]
-        proof fn p_u8(u: u8)
-            ensures p(u)
-        {
-        }
-
-        broadcast proof fn b<A: T<X = u8>>(x: A::X, a: A)
-            ensures #[trigger] q(a, x) && p(x)
-        {
-            p_u8(x);
-        }
-
-        impl T for u16 {
-            type X = u8;
-            type Y = i8;
-        }
-
-        impl T for u32 {
-            type X = u64;
-            type Y = i64;
-        }
-
-        proof fn test() {
-            broadcast use b;
-            assert(q(5u16, 10u8));
-            assert(p(10u8));
-            assert(q(5u32, 11u8));
-            assert(p(11u8)); // FAILS
-        }
-    } => Err(err) => assert_one_fails(err)
-}
-
 test_verify_one_file! {
     #[test] test_default1 verus_code! {
         trait T {

source/vir/src/func_to_air.rs

@@ -243,10 +243,13 @@ fn func_body_to_air(
     // Recursive function definitions, on the other hand, only hold conditionally for
     // type arguments and value arguments for which termination can be proved.
     // Collect the conditions on type arguments and value arguments in def_reqs.
-    if function.x.decrease.len() > 0 {
+    if function.x.decrease.len() > 0 || !matches!(function.x.kind, FunctionKind::Static) {
         // conditions on type arguments:
+        // (*always* needed in trait dispatch to make sure different implementations of the same
+        // trait don't conflict and contradict each other)
         def_reqs.extend(crate::traits::trait_bounds_to_air(ctx, &function.x.typ_bounds));
-
+    }
+    if function.x.decrease.len() > 0 {
         for param in function.x.params.iter() {
             let arg = ident_var(&param.x.name.lower());
             if let Some(pre) = typ_invariant(ctx, &param.x.typ, &arg) {