Add proof_with() and declare_with() builtin functions for ghost/track…

source/builtin/src/lib.rs

@@ -23,6 +23,29 @@ pub fn admit() {
     unimplemented!();
 }
 
+/// Pass tracked or ghost values to the immediately following external function call.
+/// Used with `external_fn_specification` functions that have extra tracked/ghost parameters.
+/// Pass ghost/tracked arguments to a function call with proper borrow checking.
+/// `_a` is a tuple of `Tracked<T>` or `Ghost<T>` values.
+/// `_b` is the function call expression whose result is returned.
+/// Usage: `proof_with((Tracked(&mut x), Ghost(y)), f(a))`
+#[cfg(verus_keep_ghost)]
+#[rustc_diagnostic_item = "verus::verus_builtin::proof_with"]
+#[verifier::proof]
+pub fn proof_with<A, B>(_a: A, _b: B) -> B {
+    unimplemented!();
+}
+
+/// Zero-arg version of proof_with for output parameters.
+/// The type parameter indicates the output container type.
+
+#[cfg(verus_keep_ghost)]
+#[rustc_diagnostic_item = "verus::verus_builtin::declare_with"]
+#[verifier::proof]
+pub fn declare_with<A>() -> A {
+    unimplemented!();
+}
+
 // Can only appear at beginning of function body
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::verus_builtin::no_method_body"]

source/rust_verify/src/context.rs

@@ -8,14 +8,25 @@ use rustc_mir_build_verus::verus::BodyErasure;
 use rustc_span::SpanData;
 use rustc_span::def_id::DefId;
 use std::cell::RefCell;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::ops::DerefMut;
 use std::rc::Rc;
 use std::sync::Arc;
 use std::sync::atomic::AtomicU64;
 use vir::ast::{CrateId, Mode, Path, Pattern, VirErr};
 use vir::messages::AstId;
 
+/// A pending tracked/ghost argument from a `proof_with()` call, waiting to be
+/// appended to the next function call's argument list.
+pub(crate) struct PendingTrackedArg {
+    /// The VIR expression for the argument value
+    pub expr: vir::ast::Expr,
+    /// true for Tracked<T>, false for Ghost<T>
+    pub is_tracked: bool,
+    /// HirId of the proof_with argument expression (for type lookup)
+    pub arg_hir_id: HirId,
+}
+
 pub struct ErasureInfo {
     pub(crate) hir_vir_ids: Vec<(HirId, AstId)>,
     pub(crate) resolved_calls: Vec<(HirId, SpanData, ResolvedCall)>,
@@ -48,6 +59,10 @@ pub struct ContextX<'tcx> {
     pub(crate) crate_name: CrateId,
     pub(crate) name_def_id_map: Rc<RefCell<std::collections::HashMap<Path, DefId>>>,
     pub(crate) next_read_kind_id: AtomicU64,
+    /// For functions with extra ghost/tracked params (from declare_with() stmts):
+    /// maps the function's DefId to a Vec of (is_tracked, expected_ty) pairs
+    pub(crate) declare_with_params:
+        Rc<RefCell<std::collections::HashMap<DefId, Vec<(bool, rustc_middle::ty::Ty<'tcx>)>>>>,
 }
 
 /// The context in which a given header node might be interpretted
@@ -92,6 +107,11 @@ pub(crate) struct BodyCtxt<'tcx> {
     /// Assume specification defines a new opaque type for each opaque type in the external function.
     /// We use this map to resolve them later.
     pub(crate) external_opaque_type_map: Option<HashMap<Path, Path>>,
+    /// Pending tracked/ghost args from proof_with() calls, to be consumed by the next function call.
+    /// Set to Some(...) by ProofWith handler, taken (consumed) by fn_call_to_vir.
+    pub(crate) pending_tracked_args: Rc<RefCell<Option<Vec<PendingTrackedArg>>>>,
+    /// HirIds of declare_with() let-stmts to skip during body conversion
+    pub(crate) declare_with_hir_ids: Rc<HashSet<HirId>>,
 }
 
 impl<'tcx> ContextX<'tcx> {
@@ -117,6 +137,7 @@ impl<'tcx> ContextX<'tcx> {
             crate_name,
             name_def_id_map: Rc::new(RefCell::new(HashMap::new())),
             next_read_kind_id: AtomicU64::new(0),
+            declare_with_params: Rc::new(RefCell::new(HashMap::new())),
         }
     }
 

source/rust_verify/src/fn_call_to_vir.rs

@@ -42,6 +42,8 @@ use vir::ast_util::{
 };
 use vir::def::field_ident_from_rust;
 
+use crate::proof_with_lifetime::check_proof_with_lifetime;
+
 pub(crate) fn fn_call_to_vir<'tcx>(
     bctx: &BodyCtxt<'tcx>,
     expr: &Expr<'tcx>,
@@ -304,6 +306,95 @@ fn fn_call_or_assoc_const_to_vir<'tcx>(
 
     let vir_args = if let Some(args) = args { mk_vir_args(bctx, &args)? } else { vec![] };
 
+    // Consume pending tracked args from proof_with() if present.
+    // Only consume when callee expects extra params (has declare_with entries).
+    let vir_args = {
+        let mut args = vir_args;
+        let extra_params = bctx.ctxt.declare_with_params.borrow().get(&f).cloned();
+        if let Some(ref expected_params) = extra_params {
+            let extra_count = expected_params.len();
+            let mut pending_opt = bctx.pending_tracked_args.borrow_mut();
+            let pending = match pending_opt.take() {
+                Some(p) => p,
+                None => {
+                    return err_span(
+                        expr.span,
+                        format!(
+                            "this external function requires {} extra tracked/ghost argument(s) via proof_with()",
+                            extra_count
+                        ),
+                    );
+                }
+            };
+            if pending.len() != extra_count {
+                return err_span(
+                    expr.span,
+                    format!(
+                        "expected {} tracked/ghost argument(s) via proof_with(), got {}",
+                        extra_count,
+                        pending.len()
+                    ),
+                );
+            }
+            // Check mode and type for each pending arg
+            for (i, (pending_arg, (expected_is_tracked, expected_ty))) in
+                pending.iter().zip(expected_params.iter()).enumerate()
+            {
+                // Mode check
+                if pending_arg.is_tracked != *expected_is_tracked {
+                    let expected_mode = if *expected_is_tracked { "Tracked" } else { "Ghost" };
+                    let actual_mode = if pending_arg.is_tracked { "Tracked" } else { "Ghost" };
+                    return err_span(
+                        expr.span,
+                        format!(
+                            "proof_with argument {} has wrong mode: expected {}, got {}",
+                            i + 1,
+                            expected_mode,
+                            actual_mode,
+                        ),
+                    );
+                }
+                // Type check: compare rustc types with regions erased.
+                {
+                    let tcx = bctx.ctxt.tcx;
+                    let expected_ty_instantiated =
+                        rustc_middle::ty::EarlyBinder::bind(*expected_ty)
+                            .instantiate(tcx, node_substs);
+                    let actual_ty = bctx.types.node_type(pending_arg.arg_hir_id);
+                    use rustc_middle::ty::TypeFoldable;
+                    let expected_erased = expected_ty_instantiated.fold_with(
+                        &mut rustc_middle::ty::RegionFolder::new(tcx, &mut |_, _| {
+                            tcx.lifetimes.re_erased
+                        }),
+                    );
+                    if actual_ty != expected_erased {
+                        return err_span(
+                            expr.span,
+                            format!(
+                                "proof_with argument {} has wrong type: expected `{}`, got `{}`",
+                                i + 1,
+                                expected_ty_instantiated,
+                                actual_ty,
+                            ),
+                        );
+                    }
+                    check_proof_with_lifetime(
+                        bctx,
+                        f,
+                        expr.hir_id,
+                        pending_arg.arg_hir_id,
+                        *expected_ty,
+                        expr.span,
+                        i,
+                    )?;
+                }
+            }
+            let exprs: Vec<_> = pending.into_iter().map(|a| a.expr).collect();
+            args.extend(exprs);
+        }
+        args
+    };
+
     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 =
@@ -2109,6 +2200,65 @@ fn verus_item_to_vir<'tcx, 'a>(
             let p = crate::rust_to_vir_expr::simplify_place_by_cancelling(&p);
             mk_expr(ExprX::BorrowMutTracked(p))
         }
+        VerusItem::ProofWith => {
+            // proof_with(ghost_args, call) — ghost args and call in one expression.
+            // First arg: single Tracked/Ghost or tuple of them.
+            // Second arg: the actual function call, whose result is returned.
+            unsupported_err_unless!(
+                args_len == 2,
+                expr.span,
+                "expected proof_with(ghost_args, call)",
+                &args
+            );
+
+            // Extract individual ghost/tracked items from the first arg.
+            let ghost_arg = &args[0];
+            let ghost_items: Vec<&rustc_hir::Expr> = match &ghost_arg.kind {
+                rustc_hir::ExprKind::Tup(elems) => elems.iter().collect(),
+                _ => vec![ghost_arg],
+            };
+
+            let bctx_ghost = &BodyCtxt { in_ghost: true, ..bctx.clone() };
+            let mut pending_args = Vec::new();
+            for item in &ghost_items {
+                let arg_typ = typ_of_expr_adjusted(bctx, item.span, &item.hir_id)?;
+                let is_tracked = match &*arg_typ {
+                    TypX::Decorate(TypDecoration::Tracked, _, _) => true,
+                    TypX::Decorate(TypDecoration::Ghost, _, _) => false,
+                    _ => {
+                        return err_span(
+                            item.span,
+                            "proof_with expects arguments of type Tracked<T> or Ghost<T>",
+                        );
+                    }
+                };
+                let arg_expr = expr_to_vir_consume(bctx_ghost, item)?;
+                pending_args.push(crate::context::PendingTrackedArg {
+                    expr: arg_expr,
+                    is_tracked,
+                    arg_hir_id: item.hir_id,
+                });
+            }
+
+            // Set pending args for consumption by the inner fn_call_to_vir
+            *bctx.pending_tracked_args.borrow_mut() = Some(pending_args);
+
+            // Record erasure: replace proof_with(A, B) with just B (arg index 1)
+            record_call(bctx, expr, ResolvedCall::SpecAllowProofArgs);
+
+            // Process second arg (the function call) — this will consume pending args
+            let call_expr = expr_to_vir_consume(bctx, &args[1])?;
+
+            // Assert pending args were consumed
+            if bctx.pending_tracked_args.borrow().is_some() {
+                return err_span(
+                    expr.span,
+                    "proof_with second argument must be a function call that accepts extra tracked/ghost arguments",
+                );
+            }
+
+            Ok(call_expr)
+        }
         VerusItem::BuiltinDeref(d) => {
             // This would be easy to support (similar to handling borrow_mut etc.) but their usage
             // would be very rare so I'm skipping for now
@@ -2126,6 +2276,11 @@ fn verus_item_to_vir<'tcx, 'a>(
             )
             .help("you can implicitly dereference this type using `*`"));
         }
+        VerusItem::DeclareWith => {
+            // declare_with() is handled at let-stmt level
+            // in rust_to_vir_expr.rs. If we reach here, it's used outside a let-stmt.
+            return err_span(expr.span, "declare_with() must be used as a let initializer");
+        }
         VerusItem::Vstd(_, _)
         | VerusItem::Marker(_)
         | VerusItem::BuiltinType(_)

source/rust_verify/src/lib.rs

@@ -53,6 +53,7 @@ mod fn_call_to_vir;
 mod hir_hide_reveal_rewrite;
 mod import_export;
 pub mod profiler;
+mod proof_with_lifetime;
 mod resolve_traits;
 pub mod reveal_hide;
 mod rust_intrinsics_to_vir;