bugfix: external_body on default method impl, fixes #1307

previously, we used body.is_some() to check if a method decl has a default;
this was wrong in the case of external_body. This commit adds an explicit
`has_default` flag to the VIR FunctionKind.

source/rust_verify/src/rust_to_vir_trait.rs

@@ -244,23 +244,25 @@ pub(crate) fn translate_trait<'tcx>(
 
         match kind {
             TraitItemKind::Fn(sig, fun) => {
-                let body_id = match fun {
+                let (body_id, has_default) = match fun {
                     TraitFn::Provided(_) if ex_trait_id_for.is_some() && !is_verus_spec => {
                         return err_span(
                             *span,
                             format!("`external_trait_specification` functions cannot have bodies"),
                         );
                     }
-                    TraitFn::Provided(body_id) => CheckItemFnEither::BodyId(body_id),
-                    TraitFn::Required(param_names) => CheckItemFnEither::ParamNames(*param_names),
+                    TraitFn::Provided(body_id) => (CheckItemFnEither::BodyId(body_id), true),
+                    TraitFn::Required(param_names) => {
+                        (CheckItemFnEither::ParamNames(*param_names), false)
+                    }
                 };
                 let attrs = tcx.hir().attrs(trait_item.hir_id());
                 let fun = check_item_fn(
                     ctxt,
                     &mut methods,
                     None,
                     owner_id.to_def_id(),
-                    FunctionKind::TraitMethodDecl { trait_path: trait_path.clone() },
+                    FunctionKind::TraitMethodDecl { trait_path: trait_path.clone(), has_default },
                     visibility.clone(),
                     module_path,
                     attrs,

source/rust_verify_test/tests/external_traits.rs

@@ -423,3 +423,29 @@ test_verify_one_file! {
         }
     } => Err(e) => assert_one_fails(e)
 }
+
+test_verify_one_file! {
+    #[test] test_trait_default_external_body_issue1307 verus_code! {
+        #[verifier::external]
+        fn some_external_fn() { }
+
+        trait T {
+            #[verifier(external_body)]
+            fn f1() -> (ret: bool)
+                ensures
+                    !ret
+            {
+                some_external_fn();
+                false
+            }
+
+            fn f2() -> bool {
+                Self::f1()
+            }
+        }
+
+        struct S;
+
+        impl T for S { }
+    } => Ok(())
+}

source/vir/src/ast.rs

@@ -994,6 +994,7 @@ pub enum FunctionKind {
     /// Method declaration inside a trait
     TraitMethodDecl {
         trait_path: Path,
+        has_default: bool,
     },
     /// Method implementation inside an impl, implementing a trait method for a trait for a type
     TraitMethodImpl {

source/vir/src/ast_visitor.rs

@@ -1226,7 +1226,9 @@ where
     let name = name.clone();
     let proxy = proxy.clone();
     let kind = match kind {
-        FunctionKind::Static | FunctionKind::TraitMethodDecl { trait_path: _ } => kind.clone(),
+        FunctionKind::Static | FunctionKind::TraitMethodDecl { trait_path: _, has_default: _ } => {
+            kind.clone()
+        }
         FunctionKind::TraitMethodImpl {
             method,
             impl_path,

source/vir/src/recursion.rs

@@ -398,7 +398,7 @@ pub(crate) fn expand_call_graph(
     let f_node = Node::Fun(function.x.name.clone());
 
     // Add T --> f if T declares method f
-    if let FunctionKind::TraitMethodDecl { trait_path } = &function.x.kind {
+    if let FunctionKind::TraitMethodDecl { trait_path, has_default: _ } = &function.x.kind {
         // T --> f
         call_graph.add_edge(Node::Trait(trait_path.clone()), f_node.clone());
     }
@@ -429,7 +429,7 @@ pub(crate) fn expand_call_graph(
 
     // Add f --> T for any function f with "where ...: T(...)"
     for bound in function.x.typ_bounds.iter() {
-        if let FunctionKind::TraitMethodDecl { trait_path } = &function.x.kind {
+        if let FunctionKind::TraitMethodDecl { trait_path, has_default: _ } = &function.x.kind {
             if crate::recursive_types::suppress_bound_in_trait_decl(
                 &trait_path,
                 &function.x.typ_params,

source/vir/src/traits.rs

@@ -329,10 +329,8 @@ pub fn inherit_default_bodies(krate: &Krate) -> Result<Krate, VirErr> {
         default_methods.insert(tr.x.name.clone(), Vec::new());
     }
     for f in &krate.functions {
-        if let FunctionKind::TraitMethodDecl { trait_path } = &f.x.kind {
-            if f.x.body.is_some() {
-                default_methods.get_mut(trait_path).expect("trait_path").push(f);
-            }
+        if let FunctionKind::TraitMethodDecl { trait_path, has_default: true } = &f.x.kind {
+            default_methods.get_mut(trait_path).expect("trait_path").push(f);
         }
         if let FunctionKind::TraitMethodImpl { impl_path, method, .. } = &f.x.kind {
             let p = (impl_path, method);