Merge remote-tracking branch 'upstream/main' into overflowing

source/builtin/src/lib.rs

@@ -370,6 +370,12 @@ pub struct Tracked<A> {
     phantom: PhantomData<A>,
 }
 
+impl<A> core::fmt::Debug for Tracked<A> {
+    fn fmt(&self, _: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
+        Ok(())
+    }
+}
+
 impl<A> Ghost<A> {
     #[cfg(verus_keep_ghost)]
     #[rustc_diagnostic_item = "verus::builtin::Ghost::view"]

source/rust_verify/src/attributes.rs

@@ -978,6 +978,21 @@ pub(crate) fn get_external_attrs(
 pub(crate) fn get_verifier_attrs(
     attrs: &[Attribute],
     diagnostics: Option<&mut Vec<VirErrAs>>,
+) -> Result<VerifierAttrs, VirErr> {
+    get_verifier_attrs_maybe_check(attrs, diagnostics, true)
+}
+
+pub(crate) fn get_verifier_attrs_no_check(
+    attrs: &[Attribute],
+    diagnostics: Option<&mut Vec<VirErrAs>>,
+) -> Result<VerifierAttrs, VirErr> {
+    get_verifier_attrs_maybe_check(attrs, diagnostics, false)
+}
+
+pub(crate) fn get_verifier_attrs_maybe_check(
+    attrs: &[Attribute],
+    diagnostics: Option<&mut Vec<VirErrAs>>,
+    do_check: bool,
 ) -> Result<VerifierAttrs, VirErr> {
     let mut vs = VerifierAttrs {
         verus_macro: false,
@@ -1096,8 +1111,10 @@ pub(crate) fn get_verifier_attrs(
             _ => {}
         }
     }
-    if let Some((rustc_attr, span)) = unsupported_rustc_attr {
-        return err_span(span, format!("The attribute `{rustc_attr:}` is not supported"));
+    if do_check {
+        if let Some((rustc_attr, span)) = unsupported_rustc_attr {
+            return err_span(span, format!("The attribute `{rustc_attr:}` is not supported"));
+        }
     }
     Ok(vs)
 }

source/rust_verify/src/context.rs

@@ -58,6 +58,16 @@ impl<'tcx> ContextX<'tcx> {
         crate::attributes::get_verifier_attrs(attrs, Some(&mut *self.diagnostics.borrow_mut()))
     }
 
+    pub(crate) fn get_verifier_attrs_no_check(
+        &self,
+        attrs: &[Attribute],
+    ) -> Result<crate::attributes::VerifierAttrs, vir::ast::VirErr> {
+        crate::attributes::get_verifier_attrs_no_check(
+            attrs,
+            Some(&mut *self.diagnostics.borrow_mut()),
+        )
+    }
+
     pub(crate) fn get_external_attrs(
         &self,
         attrs: &[Attribute],

source/rust_verify/src/rust_to_vir_global.rs

@@ -22,7 +22,7 @@ pub(crate) fn process_const_early<'tcx>(
     item: &Item<'tcx>,
 ) -> Result<(), VirErr> {
     let attrs = ctxt.tcx.hir().attrs(item.hir_id());
-    let vattrs = ctxt.get_verifier_attrs(attrs)?;
+    let vattrs = ctxt.get_verifier_attrs_no_check(attrs)?;
     if vattrs.size_of_global {
         let err = crate::util::err_span(item.span, "invalid global size_of");
         let ItemKind::Const(_ty, generics, body_id) = item.kind else {

source/rust_verify_test/tests/sets.rs

@@ -111,7 +111,7 @@ test_verify_one_file! {
 
         proof fn test() {
             let s: Set<nat> = set![9];
-            reveal_with_fuel(Set::fold, 10);
+            broadcast use fold::lemma_fold_insert, fold::lemma_fold_empty;
             assert(s.finite());
             assert(s.len() > 0);
             assert(s.fold(0, |p: nat, a: nat| p + a) == 9);

source/vir/src/ast.rs

@@ -10,7 +10,6 @@ use crate::messages::{Message, Span};
 pub use air::ast::{Binder, Binders};
 use num_bigint::BigInt;
 use serde::{Deserialize, Serialize};
-use std::fmt::Display;
 use std::sync::Arc;
 use vir_macros::{to_node_impl, ToDebugSNode};
 
@@ -585,12 +584,6 @@ pub struct SpannedTyped<X> {
     pub x: X,
 }
 
-impl<X: Display> Display for SpannedTyped<X> {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{}", self.x)
-    }
-}
-
 /// Patterns for match expressions
 pub type Pattern = Arc<SpannedTyped<PatternX>>;
 pub type Patterns = Arc<Vec<Pattern>>;
@@ -1280,21 +1273,6 @@ pub enum ArchWordBits {
     Exactly(u32),
 }
 
-impl ArchWordBits {
-    pub fn min_bits(&self) -> u32 {
-        match self {
-            ArchWordBits::Either32Or64 => 32,
-            ArchWordBits::Exactly(v) => *v,
-        }
-    }
-    pub fn num_bits(&self) -> Option<u32> {
-        match self {
-            ArchWordBits::Either32Or64 => None,
-            ArchWordBits::Exactly(v) => Some(*v),
-        }
-    }
-}
-
 #[derive(Clone, Debug, Serialize, Deserialize)]
 pub struct Arch {
     pub word_bits: ArchWordBits,
@@ -1327,16 +1305,3 @@ pub struct KrateX {
     /// Arch info
     pub arch: Arch,
 }
-
-impl FunctionKind {
-    pub(crate) fn inline_okay(&self) -> bool {
-        match self {
-            FunctionKind::Static | FunctionKind::TraitMethodImpl { .. } => true,
-            // We don't want to do inlining for MethodDecls. If a MethodDecl has a body,
-            // it's a *default* body, so we can't know for sure it hasn't been overridden.
-            FunctionKind::TraitMethodDecl { .. } | FunctionKind::ForeignTraitMethodImpl { .. } => {
-                false
-            }
-        }
-    }
-}

source/vir/src/ast_util.rs

@@ -75,6 +75,12 @@ impl fmt::Display for Mode {
     }
 }
 
+impl<X: fmt::Display> fmt::Display for SpannedTyped<X> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.x)
+    }
+}
+
 pub fn type_is_bool(typ: &Typ) -> bool {
     matches!(&**typ, TypX::Bool)
 }
@@ -908,6 +914,34 @@ impl<A: Clone> VarBinderX<A> {
     }
 }
 
+impl FunctionKind {
+    pub(crate) fn inline_okay(&self) -> bool {
+        match self {
+            FunctionKind::Static | FunctionKind::TraitMethodImpl { .. } => true,
+            // We don't want to do inlining for MethodDecls. If a MethodDecl has a body,
+            // it's a *default* body, so we can't know for sure it hasn't been overridden.
+            FunctionKind::TraitMethodDecl { .. } | FunctionKind::ForeignTraitMethodImpl { .. } => {
+                false
+            }
+        }
+    }
+}
+
+impl ArchWordBits {
+    pub fn min_bits(&self) -> u32 {
+        match self {
+            ArchWordBits::Either32Or64 => 32,
+            ArchWordBits::Exactly(v) => *v,
+        }
+    }
+    pub fn num_bits(&self) -> Option<u32> {
+        match self {
+            ArchWordBits::Either32Or64 => None,
+            ArchWordBits::Exactly(v) => Some(*v),
+        }
+    }
+}
+
 pub fn str_unique_var(s: &str, dis: crate::ast::VarIdentDisambiguate) -> VarIdent {
     VarIdent(Arc::new(s.to_string()), dis)
 }

source/vstd/map.rs

@@ -41,13 +41,13 @@ impl<K, V> Map<K, V> {
 
     /// Gives a `Map<K, V>` whose domain contains every key, and maps each key
     /// to the value given by `fv`.
-    pub open spec fn total(fv: impl Fn(K) -> V) -> Map<K, V> {
+    pub open spec fn total(fv: spec_fn(K) -> V) -> Map<K, V> {
         Set::full().mk_map(fv)
     }
 
     /// Gives a `Map<K, V>` whose domain is given by the boolean predicate on keys `fk`,
     /// and maps each key to the value given by `fv`.
-    pub open spec fn new(fk: impl Fn(K) -> bool, fv: impl Fn(K) -> V) -> Map<K, V> {
+    pub open spec fn new(fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V) -> Map<K, V> {
         Set::new(fk).mk_map(fv)
     }