Support default trait associated consts

Author: Chris-Hawblitzel

source/rust_verify/src/rust_to_vir_trait.rs

@@ -345,8 +345,23 @@ pub(crate) fn translate_trait<'tcx>(
                     method_names.push(fun);
                 }
             }
-            TraitItemKind::Const(_ty, None) => {
-                let has_default = false;
+            TraitItemKind::Const(_ty, body_opt) => {
+                let param_names = vec![];
+                let (body_id, has_default) = match body_opt {
+                    Some(_) if ex_trait_id_for.is_some() && !is_verus_spec => {
+                        return err_span(
+                            *span,
+                            format!("`external_trait_specification` functions cannot have bodies"),
+                        );
+                    }
+                    Some(rustc_hir::ConstItemRhs::Body(body_id)) => {
+                        (CheckItemFnEither::BodyId(body_id), true)
+                    }
+                    Some(_) => {
+                        crate::unsupported_err!(trait_span, "non-expression trait const default")
+                    }
+                    None => (CheckItemFnEither::ParamNames(param_names.as_slice()), false),
+                };
                 let mid_ty = ctxt.tcx.type_of(owner_id.to_def_id()).skip_binder();
                 let typ = ctxt.mid_ty_to_vir(owner_id.to_def_id(), *span, &mid_ty, false, None)?;
                 let fun = crate::rust_to_vir_func::check_item_fn(
@@ -361,7 +376,7 @@ pub(crate) fn translate_trait<'tcx>(
                     crate::rust_to_vir_func::FnOrConstSig::const_var(*span, typ),
                     Some((trait_generics, trait_def_id)),
                     item_generics,
-                    crate::rust_to_vir_func::CheckItemFnEither::ParamNames(&[]),
+                    body_id,
                     ex_trait_id_for.map(|d| (d, trait_extension_in_spec)),
                     ex_item_id_for,
                     external_info,
@@ -372,12 +387,6 @@ pub(crate) fn translate_trait<'tcx>(
                     method_names.push(fun);
                 }
             }
-            TraitItemKind::Const(_ty, Some(_body_id)) => {
-                return err_span(
-                    trait_span,
-                    "Verus does not yet support associated constants with default values",
-                );
-            }
             TraitItemKind::Type(_, Some(_)) => {
                 return err_span(
                     trait_span,

source/rust_verify_test/tests/traits.rs

@@ -4573,3 +4573,77 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "cannot read const with mode exec")
 }
+
+test_verify_one_file! {
+    #[test] trait_assoc_const1_default verus_code! {
+        trait U {}
+
+        trait T<A, B> {
+            const C: usize = 10;
+            const S: &str = "no";
+            const E: usize = 20;
+        }
+
+        impl U for u16 {}
+
+        const Q: u8 = 10;
+
+        impl<Z: U> T<u8, Z> for bool {
+            const C: usize = 13 - Q as usize;
+            const S: &str = "ha";
+
+            #[verifier::external_body]
+            const E: usize = 4;
+        }
+
+        impl<Z: U> T<u16, Z> for bool {
+        }
+
+        fn test1() {
+            assert(<bool as T<u8, u16>>::C == 3);
+            assert(<bool as T<u16, u16>>::C == 10);
+            let c = <bool as T<u8, u16>>::C;
+            assert(c == 3);
+            let c2 = <bool as T<u16, u16>>::C;
+            assert(c2 == 3); // FAILS
+        }
+
+        fn test2<A: T<u8, u16>>() {
+            assert(A::C == 3); // FAILS
+        }
+
+        fn test3<A: T<u8, u16>>() {
+            assert(A::C == 10); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 3)
+}
+
+test_verify_one_file! {
+    #[test] trait_assoc_const2_default verus_code! {
+        const fn f() -> u8 { 3 }
+        trait T {
+            // implicitly dual exec-spec mode:
+            const C: u8 = f();
+        }
+    } => Err(err) => assert_vir_error_msg(err, "with mode exec")
+}
+
+test_verify_one_file! {
+    #[test] trait_assoc_const3_default verus_code! {
+        spec const Q: u8 = 3;
+        trait T {
+            // implicitly dual exec-spec mode:
+            const C: u8 = Q;
+        }
+    } => Err(err) => assert_vir_error_msg(err, "expected mode")
+}
+
+test_verify_one_file! {
+    #[test] trait_assoc_const4_default verus_code! {
+        exec const Q: u8 = 3;
+        trait T {
+            // implicitly dual exec-spec mode:
+            const C: u8 = Q;
+        }
+    } => Err(err) => assert_vir_error_msg(err, "cannot read const with mode exec")
+}