Add verifier::assume(externals_available_without_declaration) (verus-lang#1988)

Author: Chris-Hawblitzel

source/rust_verify/src/attributes.rs

@@ -345,6 +345,8 @@ pub(crate) enum Attr {
     OpenVisibilityQualifier,
     // Allow the function to not have decreases clauses
     ExecAllowNoDecreasesClause,
+    // Assume that external items can be used without a Verus declaration (unsound)
+    ExternalsAvailableWithoutDeclaration(bool),
     // Assume that the function terminates
     AssumeTermination,
     // Proxy containing unerased code
@@ -677,6 +679,16 @@ pub(crate) fn parse_attrs(
                 AttrTree::Fun(_, arg, None) if arg == "exec_allows_no_decreases_clause" => {
                     v.push(Attr::ExecAllowNoDecreasesClause);
                 }
+                AttrTree::Fun(_, arg, Some(box [AttrTree::Fun(_, r, None)]))
+                    if arg == "assume" && r == "externals_available_without_declaration" =>
+                {
+                    v.push(Attr::ExternalsAvailableWithoutDeclaration(true))
+                }
+                AttrTree::Fun(_, arg, Some(box [AttrTree::Fun(_, r, None)]))
+                    if arg == "deny" && r == "externals_available_without_declaration" =>
+                {
+                    v.push(Attr::ExternalsAvailableWithoutDeclaration(false))
+                }
                 AttrTree::Fun(_, arg, None) if arg == "tracked_swap_primitive" => {
                     v.push(Attr::TrackedSwap)
                 }
@@ -942,6 +954,18 @@ pub(crate) fn get_allow_exec_allows_no_decreases_clause_walk_parents<'tcx>(
     false
 }
 
+pub(crate) fn get_externals_available_without_declaration_walk_parents<'tcx>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    def_id: rustc_span::def_id::DefId,
+) -> bool {
+    for attr in parse_attrs_walk_parents(tcx, def_id) {
+        if let Attr::ExternalsAvailableWithoutDeclaration(flag) = attr {
+            return flag;
+        }
+    }
+    false
+}
+
 pub(crate) fn get_ghost_block_opt(attrs: &[Attribute]) -> Option<GhostBlockAttr> {
     for attr in parse_attrs_opt(attrs, None) {
         match attr {
@@ -1126,6 +1150,7 @@ pub(crate) struct VerifierAttrs {
     pub(crate) open_visibility_qualifier: bool,
     pub(crate) assume_termination: bool,
     pub(crate) exec_allows_no_decreases_clause: bool,
+    pub(crate) externals_available_without_declaration: Option<bool>,
     pub(crate) unerased_proxy: bool,
     pub(crate) encoded_const: bool,
     pub(crate) encoded_static: bool,
@@ -1300,6 +1325,7 @@ pub(crate) fn get_verifier_attrs_maybe_check(
         open_visibility_qualifier: false,
         assume_termination: false,
         exec_allows_no_decreases_clause: false,
+        externals_available_without_declaration: None,
         unerased_proxy: false,
         encoded_const: false,
         encoded_static: false,
@@ -1380,6 +1406,9 @@ pub(crate) fn get_verifier_attrs_maybe_check(
             Attr::OpenVisibilityQualifier => vs.open_visibility_qualifier = true,
             Attr::AssumeTermination => vs.assume_termination = true,
             Attr::ExecAllowNoDecreasesClause => vs.exec_allows_no_decreases_clause = true,
+            Attr::ExternalsAvailableWithoutDeclaration(flag) => {
+                vs.externals_available_without_declaration = Some(flag)
+            }
             Attr::UnerasedProxy => vs.unerased_proxy = true,
             Attr::EncodedConst => vs.encoded_const = true,
             Attr::EncodedStatic => vs.encoded_static = true,

source/rust_verify/src/erase.rs

@@ -50,9 +50,9 @@ pub enum ResolvedCall {
     /// The call is to an operator like == or + that should be compiled.
     CompilableOperator(CompilableOperator),
     /// The call is to a function, and we record the name of the function here
-    /// (both unresolved and resolved), as well as an in_ghost flag.
+    /// (both unresolved and resolved), as well as (in_ghost, assume_external) flags.
     /// This is replaced by CallModes as soon as the modes are available.
-    Call(Fun, Fun, bool),
+    Call(Fun, Fun, bool, bool),
     /// Path and variant of datatype constructor
     Ctor(Path, vir::ast::Ident),
     /// Path and variant of datatype constructor. Used for ExprKind::Struct nodes.
@@ -168,11 +168,15 @@ fn resolved_call_to_call_erase(
     Ok(match resolved_call {
         ResolvedCall::SpecPure => CallErasure::EraseTree(TreeErase::IncludeBasicChecks),
         ResolvedCall::SpecAllowProofArgs => CallErasure::Call(NodeErase::Erase),
-        ResolvedCall::Call(ufun, rfun, in_ghost) => {
+        ResolvedCall::Call(ufun, rfun, in_ghost, assume_external) => {
             // Note: in principle, the unresolved function ufun should always be present,
             // but we currently allow external declarations of resolved trait functions
             // without a corresponding external trait declaration.
             let Some(f) = functions.get(ufun).or_else(|| functions.get(rfun)) else {
+                if *assume_external {
+                    let erase = CallErasure::Call(NodeErase::Keep);
+                    return Ok(erase);
+                }
                 dbg!(ufun, rfun);
                 panic!("internal Verus error: could not find mode declarations for function")
             };

source/rust_verify/src/fn_call_to_vir.rs

@@ -300,14 +300,23 @@ fn fn_call_or_assoc_const_to_vir<'tcx>(
         }
     };
 
-    record_call(bctx, expr, ResolvedCall::Call(name.clone(), record_name, bctx.in_ghost));
+    let assume_external_allowed =
+        crate::attributes::get_externals_available_without_declaration_walk_parents(
+            bctx.ctxt.tcx,
+            bctx.fun_id,
+        );
+
+    let resolved_call =
+        ResolvedCall::Call(name.clone(), record_name, bctx.in_ghost, assume_external_allowed);
+    record_call(bctx, expr, resolved_call);
 
     let vir_args = if let Some(args) = args { mk_vir_args(bctx, &args)? } else { vec![] };
 
     let typ_args = mk_typ_args(bctx, node_substs, f, expr.span)?;
     let impl_paths = get_impl_paths(bctx, f, node_substs, None, const_var, expr.span)?;
-    let target =
-        CallTarget::Fun(target_kind, name, typ_args, impl_paths, autospec_usage, const_var);
+    let call_target_attrs =
+        vir::ast::CallTargetAttrs { autospec: autospec_usage, assume_external_allowed, const_var };
+    let target = CallTarget::Fun(target_kind, name, typ_args, impl_paths, call_target_attrs);
     Ok(bctx.spanned_typed_new(
         expr.span,
         &expr_typ()?,
@@ -379,8 +388,13 @@ pub(crate) fn deref_to_vir<'tcx>(
 
     let typ_args = mk_typ_args(bctx, node_substs, trait_fun_id, span)?;
     let impl_paths = get_impl_paths(bctx, trait_fun_id, node_substs, None, false, span)?;
+    let call_target_attrs = vir::ast::CallTargetAttrs {
+        autospec: autospec_usage,
+        assume_external_allowed: false,
+        const_var: false,
+    };
     let call_target =
-        CallTarget::Fun(target_kind, trait_fun, typ_args, impl_paths, autospec_usage, false);
+        CallTarget::Fun(target_kind, trait_fun, typ_args, impl_paths, call_target_attrs);
     let args = Arc::new(vec![arg.clone()]);
     let x = ExprX::Call(call_target, args, None);
 
@@ -2815,12 +2829,12 @@ fn record_loop_spec<'tcx>(
 
 pub(crate) fn record_call<'tcx>(bctx: &BodyCtxt<'tcx>, expr: &Expr, resolved_call: ResolvedCall) {
     let resolved_call = match (resolved_call, &bctx.external_trait_from_to) {
-        (ResolvedCall::Call(ufun, rfun, in_ghost), Some(paths)) if paths.2.is_some() => {
+        (ResolvedCall::Call(ufun, rfun, in_ghost, ae), Some(paths)) if paths.2.is_some() => {
             let (from_path, _to_path, to_spec_path) = &**paths;
             use vir::traits::rewrite_fun;
             let ufun = rewrite_fun(from_path, to_spec_path.as_ref().unwrap(), &ufun);
             let rfun = rewrite_fun(from_path, to_spec_path.as_ref().unwrap(), &rfun);
-            ResolvedCall::Call(ufun, rfun, in_ghost)
+            ResolvedCall::Call(ufun, rfun, in_ghost, ae)
         }
         (resolved_call, _) => resolved_call,
     };

source/rust_verify/src/rust_to_vir_expr.rs

@@ -1462,13 +1462,17 @@ pub(crate) fn expr_to_vir_with_adjustments<'tcx>(
             if let Some((fun, typ_args)) = f {
                 let autospec_usage =
                     if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final };
+                let call_target_attrs = vir::ast::CallTargetAttrs {
+                    autospec: autospec_usage,
+                    const_var: false,
+                    assume_external_allowed: false,
+                };
                 let call_target = CallTarget::Fun(
                     vir::ast::CallTargetKind::Static,
                     fun,
                     typ_args,
                     Arc::new(vec![]),
-                    autospec_usage,
-                    false,
+                    call_target_attrs,
                 );
                 let arg = arg.consume(bctx, get_inner_ty());
                 let args = Arc::new(vec![arg.clone()]);
@@ -2071,14 +2075,18 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                         )?;
 
                         let typ_args = Arc::new(vec![tup_typ, ret_typ, fun_typ]);
+                        let call_target_attrs = vir::ast::CallTargetAttrs {
+                            autospec: AutospecUsage::Final,
+                            const_var: false,
+                            assume_external_allowed: false,
+                        };
                         (
                             CallTarget::Fun(
                                 kind,
                                 helper_fun,
                                 typ_args,
                                 impl_paths,
-                                AutospecUsage::Final,
-                                false,
+                                call_target_attrs,
                             ),
                             vec![vir_fun, tup],
                             rcall,
@@ -2134,13 +2142,17 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                 };
                 let autospec_usage =
                     if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final };
+                let call_target_attrs = vir::ast::CallTargetAttrs {
+                    autospec: autospec_usage,
+                    const_var: false,
+                    assume_external_allowed: false,
+                };
                 let call_target = CallTarget::Fun(
                     vir::ast::CallTargetKind::Static,
                     fun,
                     typ_args,
                     Arc::new(vec![]),
-                    autospec_usage,
-                    false,
+                    call_target_attrs,
                 );
                 let args = Arc::new(vec![arg_vir.clone()]);
                 mk_expr(ExprX::Call(call_target, args, None))
@@ -2231,13 +2243,17 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                     let typ_args = Arc::new(vec![from_typ, to_typ]);
                     let autospec_usage =
                         if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final };
+                    let call_target_attrs = vir::ast::CallTargetAttrs {
+                        autospec: autospec_usage,
+                        const_var: false,
+                        assume_external_allowed: false,
+                    };
                     let call_target = CallTarget::Fun(
                         vir::ast::CallTargetKind::Static,
                         fun,
                         typ_args,
                         Arc::new(vec![]),
-                        autospec_usage,
-                        false,
+                        call_target_attrs,
                     );
                     let args = Arc::new(vec![source_vir_expr.clone()]);
                     mk_expr(ExprX::Call(call_target, args, None))
@@ -2992,6 +3008,11 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                     None
                 };
 
+                let call_target_attrs = vir::ast::CallTargetAttrs {
+                    autospec: AutospecUsage::Final,
+                    const_var: false,
+                    assume_external_allowed: false,
+                };
                 let call_target = if let Some((fun, typ_args)) = fun_typ_args {
                     // special fast path
                     CallTarget::Fun(
@@ -3001,8 +3022,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                         // arbitrary impl_path
                         // REVIEW: why is this needed?
                         Arc::new(vec![ImplPath::TraitImplPath(vir::def::prefix_spec_fn_type(0))]),
-                        AutospecUsage::Final,
-                        false,
+                        call_target_attrs,
                     )
                 } else {
                     // general Index trait case
@@ -3011,14 +3031,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                     let typ_args =
                         Arc::new(vec![undecorate_typ(&tgt_vir.typ), idx_vir.typ.clone()]);
                     let fun = vir::fun!(CrateId::Core => "ops", "index", "Index", "index");
-                    CallTarget::Fun(
-                        target_kind,
-                        fun,
-                        typ_args,
-                        impl_paths,
-                        AutospecUsage::Final,
-                        false,
-                    )
+                    CallTarget::Fun(target_kind, fun, typ_args, impl_paths, call_target_attrs)
                 };
 
                 // tgt[idx] is equivalent to either *index(tgt, idx) or *index_mut(tgt, idx)
@@ -3842,13 +3855,17 @@ pub(crate) fn maybe_do_ptr_cast<'tcx>(
         Some(PtrCastKind::Complex(fun, typ_args, clip)) => {
             let autospec_usage =
                 if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final };
+            let call_target_attrs = vir::ast::CallTargetAttrs {
+                autospec: autospec_usage,
+                const_var: false,
+                assume_external_allowed: false,
+            };
             let call_target = CallTarget::Fun(
                 vir::ast::CallTargetKind::Static,
                 fun,
                 typ_args,
                 Arc::new(vec![]),
-                autospec_usage,
-                false,
+                call_target_attrs,
             );
             let args = Arc::new(vec![src_vir.clone()]);
             let x = ExprX::Call(call_target, args, None);

source/rust_verify_test/tests/verifier_assume_allow.rs

@@ -0,0 +1,81 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+test_verify_one_file! {
+    #[test] test_externals_available_without_declaration1 verus_code! {
+        #[verifier::external]
+        fn f0() {}
+
+        #[verifier::external]
+        fn f1() -> u8 { 3 }
+
+        #[verifier::external]
+        fn f2(u: &mut u8) -> u8 { 3 }
+
+        #[verifier::external]
+        fn f3(u: u8) {}
+
+        assume_specification[ f3 ](u: u8)
+            requires
+                u > 10,
+        ;
+
+        #[verifier::assume(externals_available_without_declaration)]
+        fn g0() {
+            f0();
+            f3(5); // FAILS
+        }
+
+        #[verifier::assume(externals_available_without_declaration)]
+        mod m {
+            fn g0() {
+                super::f0();
+            }
+        }
+
+        #[verifier::exec_allows_no_decreases_clause]
+        #[verifier::assume(externals_available_without_declaration)]
+        fn g1() {
+            let mut x = 3;
+            x = f1();
+            assert(x >= 0);
+            assert(x == 3); // FAILS
+            loop {
+                assert(x >= 0);
+                break;
+            }
+        }
+
+        #[verifier::exec_allows_no_decreases_clause]
+        #[verifier::assume(externals_available_without_declaration)]
+        fn g2() {
+            let mut x = 3;
+            let u = f2(&mut x);
+            assert(x >= 0);
+            assert(u >= 0);
+            assert(x == 3); // FAILS
+            loop {
+                assert(x >= 0);
+                assert(u >= 0);
+                break;
+            }
+        }
+    } => Err(err) => assert_fails(err, 3)
+}
+
+test_verify_one_file! {
+    #[test] test_externals_available_without_declaration2 verus_code! {
+        #[verifier::external]
+        fn f0() {}
+
+        #[verifier::assume(externals_available_without_declaration)]
+        mod m {
+            #[verifier::deny(externals_available_without_declaration)]
+            fn g0() {
+                super::f0();
+            }
+        }
+    } => Err(err) => assert_vir_error_msg(err, "cannot use function")
+}