Erase ghost code by default

source/builtin/src/lib.rs

@@ -1,6 +1,7 @@
+#![no_std]
 #![feature(rustc_attrs)]
 #![feature(negative_impls)]
-#![no_std]
+#![feature(const_trait_impl)]
 #![feature(unboxed_closures)]
 #![feature(fn_traits)]
 #![feature(register_tool)]
@@ -637,48 +638,70 @@ impl<T> SyncSendIfSend<T> {
 // Marker for integer types (i8 ... u128, isize, usize, nat, int)
 // so that we get reasonable type error messages when someone uses a non-Integer type
 // in an arithmetic operation.
-pub trait Integer {}
-impl Integer for u8 {}
-impl Integer for u16 {}
-impl Integer for u32 {}
-impl Integer for u64 {}
-impl Integer for u128 {}
-impl Integer for usize {}
-impl Integer for i8 {}
-impl Integer for i16 {}
-impl Integer for i32 {}
-impl Integer for i64 {}
-impl Integer for i128 {}
-impl Integer for isize {}
-impl Integer for int {}
-impl Integer for nat {}
-impl Integer for char {}
+#[const_trait]
+pub trait Integer {
+    fn integer_default() -> Self;
+}
+
+macro_rules! impl_integer {
+    ([$($t:ty)*]) => {
+        $(
+            impl const Integer for $t {
+                fn integer_default() -> Self {
+                    0
+                }
+            }
+        )*
+    }
+}
+impl_integer!([
+    usize u8 u16 u32 u64 u128
+    isize i8 i16 i32 i64 i128
+]);
+impl const Integer for int {
+    fn integer_default() -> Self {
+        int {}
+    }
+}
+impl const Integer for nat {
+    fn integer_default() -> Self {
+        nat {}
+    }
+}
+impl const Integer for char {
+    fn integer_default() -> Self {
+        ' '
+    }
+}
 
 // spec literals of the form "33", which could have any Integer type
+// (this is a const fn to allow rustc to handle things like "spec const foo: int = 7")
 #[rustc_diagnostic_item = "verus::builtin::spec_literal_integer"]
 #[allow(non_camel_case_types)]
 #[verifier::spec]
-pub fn spec_literal_integer<
-    hint_please_add_suffix_on_literal_like_100u32_or_100int_or_100nat: Integer,
+pub const fn spec_literal_integer<
+    hint_please_add_suffix_on_literal_like_100u32_or_100int_or_100nat: ~const Integer,
 >(
     _s: &str,
 ) -> hint_please_add_suffix_on_literal_like_100u32_or_100int_or_100nat {
-    unimplemented!()
+    hint_please_add_suffix_on_literal_like_100u32_or_100int_or_100nat::integer_default()
 }
 
 // spec literals of the form "33int",
 // or spec literals in positions syntactically expected to be int (e.g. in "x + 33")
+// (this is a const fn to allow rustc to handle things like "spec const foo: int = 7int")
 #[rustc_diagnostic_item = "verus::builtin::spec_literal_int"]
 #[verifier::spec]
-pub fn spec_literal_int(_s: &str) -> int {
-    unimplemented!()
+pub const fn spec_literal_int(_s: &str) -> int {
+    int {}
 }
 
 // spec literals of the form "33nat"
+// (this is a const fn to allow rustc to handle things like "spec const foo: int = 7nat")
 #[rustc_diagnostic_item = "verus::builtin::spec_literal_nat"]
 #[verifier::spec]
-pub fn spec_literal_nat(_s: &str) -> nat {
-    unimplemented!()
+pub const fn spec_literal_nat(_s: &str) -> nat {
+    nat {}
 }
 
 // Fixed-width add

source/builtin_macros/src/fndecl.rs

@@ -4,6 +4,6 @@ use quote::quote;
 #[inline(always)]
 pub fn fndecl(input: TokenStream) -> TokenStream {
     quote! {
-        #[verifier::spec] #[verifier::external_body] /* vattr */ #input { unimplemented!() }
+        #[cfg_attr(verus_macro_keep_ghost, verifier::spec)] #[cfg_attr(verus_macro_keep_ghost, verifier::external_body)] /* vattr */ #input { unimplemented!() }
     }
 }

source/builtin_macros/src/lib.rs

@@ -60,8 +60,7 @@ pub fn verus_exec_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStrea
 }
 
 pub(crate) fn cfg_erase() -> bool {
-    let ts: proc_macro::TokenStream =
-        quote::quote! { ::core::cfg!(verus_macro_erase_ghost) }.into();
+    let ts: proc_macro::TokenStream = quote::quote! { ::core::cfg!(verus_macro_keep_ghost) }.into();
     let bool_ts = ts.expand_expr();
     let bool_ts = match bool_ts {
         Ok(name) => name,
@@ -71,7 +70,7 @@ pub(crate) fn cfg_erase() -> bool {
     };
     let bool_ts = bool_ts.to_string();
     assert!(bool_ts == "true" || bool_ts == "false");
-    bool_ts == "true"
+    bool_ts == "false"
 }
 
 /// verus_proof_macro_exprs!(f!(exprs)) applies verus syntax to transform exprs into exprs',

source/builtin_macros/src/syntax.rs

@@ -139,6 +139,17 @@ impl Visitor {
         if self.erase_ghost { Expr::Verbatim(quote_spanned!(span => {})) } else { e }
     }
 
+    fn filter_attrs(&mut self, attrs: &mut Vec<Attribute>) {
+        if self.erase_ghost {
+            // Remove verus:: and verifier:: attributes to make it easier for
+            // standard rustc to compile the code
+            attrs.retain(|attr| {
+                let prefix = attr.path.segments[0].ident.to_string();
+                prefix != "verus" && prefix != "verifier"
+            });
+        }
+    }
+
     fn visit_fn(
         &mut self,
         attrs: &mut Vec<Attribute>,
@@ -150,10 +161,14 @@ impl Visitor {
         let mut stmts: Vec<Stmt> = Vec::new();
         let mut unwrap_ghost_tracked: Vec<Stmt> = Vec::new();
 
-        attrs.push(mk_verus_attr(sig.fn_token.span, quote! { verus_macro }));
+        // attrs.push(mk_verus_attr(sig.fn_token.span, quote! { verus_macro }));
+        if !self.erase_ghost {
+            attrs.push(mk_verus_attr(sig.fn_token.span, quote! { verus_macro }));
+        }
 
         for arg in &mut sig.inputs {
             match (arg.tracked, &mut arg.kind) {
+                _ if self.erase_ghost => {}
                 (None, _) => {}
                 (Some(token), FnArgKind::Receiver(receiver)) => {
                     receiver.attrs.push(mk_verus_attr(token.span, quote! { proof }));
@@ -209,7 +224,9 @@ impl Visitor {
             ReturnType::Default => None,
             ReturnType::Type(_, ref mut tracked, ref mut ret_opt, ty) => {
                 if let Some(token) = tracked {
-                    attrs.push(mk_verus_attr(token.span, quote! { returns(proof) }));
+                    if !self.erase_ghost {
+                        attrs.push(mk_verus_attr(token.span, quote! { returns(proof) }));
+                    }
                     *tracked = None;
                 }
                 match std::mem::take(ret_opt) {
@@ -398,6 +415,7 @@ impl Visitor {
         attrs.extend(mode_attrs);
         attrs.extend(prover_attr.into_iter());
         attrs.extend(ext_attrs);
+        self.filter_attrs(attrs);
         // unwrap_ghost_tracked must go first so that unwrapped vars are in scope in other headers
         stmts.splice(0..0, unwrap_ghost_tracked);
         stmts.extend(unimpl);
@@ -412,7 +430,9 @@ impl Visitor {
         publish: &mut Publish,
         mode: &mut FnMode,
     ) {
-        attrs.push(mk_verus_attr(span, quote! { verus_macro }));
+        if !self.erase_ghost {
+            attrs.push(mk_verus_attr(span, quote! { verus_macro }));
+        }
 
         let publish_attrs = match (vis, &publish) {
             (Some(Visibility::Inherited), _) => vec![],
@@ -444,6 +464,7 @@ impl Visitor {
         *mode = FnMode::Default;
         attrs.extend(publish_attrs);
         attrs.extend(mode_attrs);
+        self.filter_attrs(attrs);
     }
 }
 
@@ -736,7 +757,7 @@ impl Visitor {
             };
             if let Some((name, vis)) = erase_fn {
                 *item = Item::Verbatim(quote_spanned! {
-                    span => #[allow(unused_imports)] #vis use bool as #name;
+                    span => #[allow(unused_imports)] #vis use core::primitive::bool as #name;
                 });
             }
         }
@@ -1900,6 +1921,11 @@ impl VisitMut for Visitor {
         visit_block_mut(self, block);
     }
 
+    fn visit_type_param_mut(&mut self, p: &mut syn_verus::TypeParam) {
+        self.filter_attrs(&mut p.attrs);
+        syn_verus::visit_mut::visit_type_param_mut(self, p);
+    }
+
     fn visit_item_fn_mut(&mut self, fun: &mut ItemFn) {
         // Process rustdoc before processing the ItemFn itself.
         // That way, the generated rustdoc gets the prettier syntax instead of the
@@ -1970,18 +1996,21 @@ impl VisitMut for Visitor {
         visit_field_mut(self, field);
         field.attrs.extend(data_mode_attrs(&field.mode));
         field.mode = DataMode::Default;
+        self.filter_attrs(&mut field.attrs);
     }
 
     fn visit_item_enum_mut(&mut self, item: &mut ItemEnum) {
         visit_item_enum_mut(self, item);
         item.attrs.extend(data_mode_attrs(&item.mode));
         item.mode = DataMode::Default;
+        self.filter_attrs(&mut item.attrs);
     }
 
     fn visit_item_struct_mut(&mut self, item: &mut ItemStruct) {
         visit_item_struct_mut(self, item);
         item.attrs.extend(data_mode_attrs(&item.mode));
         item.mode = DataMode::Default;
+        self.filter_attrs(&mut item.attrs);
     }
 
     fn visit_type_mut(&mut self, ty: &mut Type) {
@@ -2060,16 +2089,19 @@ impl VisitMut for Visitor {
         if let Some((_, items)) = &mut item.content {
             self.visit_items_prefilter(items);
         }
+        self.filter_attrs(&mut item.attrs);
         syn_verus::visit_mut::visit_item_mod_mut(self, item);
     }
 
     fn visit_item_impl_mut(&mut self, imp: &mut ItemImpl) {
         self.visit_impl_items_prefilter(&mut imp.items, imp.trait_.is_some());
+        self.filter_attrs(&mut imp.attrs);
         syn_verus::visit_mut::visit_item_impl_mut(self, imp);
     }
 
     fn visit_item_trait_mut(&mut self, tr: &mut ItemTrait) {
         self.visit_trait_items_prefilter(&mut tr.items);
+        self.filter_attrs(&mut tr.attrs);
         syn_verus::visit_mut::visit_item_trait_mut(self, tr);
     }
 }
@@ -2404,7 +2436,7 @@ fn rejoin_tokens(stream: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let adjacent = |s1: Span, s2: Span| {
         let l1 = s1.end();
         let l2 = s2.start();
-        s1.source_file() == s2.source_file() && l1 == l2
+        s1.source_file() == s2.source_file() && l1.eq(&l2)
     };
     for i in 0..(if tokens.len() >= 2 { tokens.len() - 2 } else { 0 }) {
         let t0 = pun(&tokens[i]);

source/pervasive/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "vstd"
+version = "0.1.0"
+edition = "2018"
+
+[lib]
+name = "vstd"
+path = "vstd.rs"
+
+[dependencies]
+builtin_macros = { path = "../builtin_macros" }
+builtin = { path = "../builtin" }

source/pervasive/invariant.rs

@@ -117,11 +117,11 @@ pub trait InvariantPredicate<K, V> {
 /// using the [`atomic_ghost` APIs](crate::atomic_ghost).
 
 
-#[verifier::proof]
-#[verifier::external_body] /* vattr */
-#[verifier::accept_recursive_types(K)]
-#[verifier::accept_recursive_types(V)]
-#[verifier::accept_recursive_types(Pred)]
+#[cfg_attr(verus_macro_keep_ghost, verifier::proof)]
+#[cfg_attr(verus_macro_keep_ghost, verifier::external_body)] /* vattr */
+#[cfg_attr(verus_macro_keep_ghost, verifier::accept_recursive_types(K))]
+#[cfg_attr(verus_macro_keep_ghost, verifier::accept_recursive_types(V))]
+#[cfg_attr(verus_macro_keep_ghost, verifier::accept_recursive_types(Pred))]
 pub struct AtomicInvariant<K, V, Pred> {
     dummy: builtin::SyncSendIfSend<V>,
     dummy1: core::marker::PhantomData<(K, Pred)>,
@@ -159,11 +159,11 @@ pub struct AtomicInvariant<K, V, Pred> {
 /// The `LocalInvariant` API is an instance of the ["invariant" method in Verus's general philosophy on interior mutability](https://verus-lang.github.io/verus/guide/interior_mutability.html).
 
 
-#[verifier::proof]
-#[verifier::external_body] /* vattr */
-#[verifier::accept_recursive_types(K)]
-#[verifier::accept_recursive_types(V)]
-#[verifier::accept_recursive_types(Pred)]
+#[cfg_attr(verus_macro_keep_ghost, verifier::proof)]
+#[cfg_attr(verus_macro_keep_ghost, verifier::external_body)] /* vattr */
+#[cfg_attr(verus_macro_keep_ghost, verifier::accept_recursive_types(K))]
+#[cfg_attr(verus_macro_keep_ghost, verifier::accept_recursive_types(V))]
+#[cfg_attr(verus_macro_keep_ghost, verifier::accept_recursive_types(Pred))]
 pub struct LocalInvariant<K, V, Pred> {
     dummy: builtin::SendIfSend<V>,
     dummy1: core::marker::PhantomData<(K, Pred)>, // TODO ignore Send/Sync here
@@ -217,7 +217,7 @@ macro_rules! declare_invariant_impl {
             ///`, returning the tracked value contained within.
 
             #[verifier::external_body]
-            pub proof fn into_inner(#[verifier::proof] self) -> (tracked v: V)
+            pub proof fn into_inner(tracked self) -> (tracked v: V)
                 ensures self.inv(v),
             {
                 unimplemented!();
@@ -232,7 +232,7 @@ declare_invariant_impl!(AtomicInvariant);
 declare_invariant_impl!(LocalInvariant);
 
 #[doc(hidden)]
-#[verifier::proof]
+#[cfg_attr(verus_macro_keep_ghost, verifier::proof)]
 pub struct InvariantBlockGuard;
 
 // NOTE: These 3 methods are removed in the conversion to VIR; they are only used
@@ -256,21 +256,21 @@ pub struct InvariantBlockGuard;
 
 #[rustc_diagnostic_item = "verus::pervasive::invariant::open_atomic_invariant_begin"]
 #[doc(hidden)]
-#[verifier::external] /* vattr */
+#[cfg_attr(verus_macro_keep_ghost, verifier::external)] /* vattr */
 pub fn open_atomic_invariant_begin<'a, K, V, Pred: InvariantPredicate<K, V>>(_inv: &'a AtomicInvariant<K, V, Pred>) -> (&'a InvariantBlockGuard, V) {
     unimplemented!();
 }
 
 #[rustc_diagnostic_item = "verus::pervasive::invariant::open_local_invariant_begin"]
 #[doc(hidden)]
-#[verifier::external] /* vattr */
+#[cfg_attr(verus_macro_keep_ghost, verifier::external)] /* vattr */
 pub fn open_local_invariant_begin<'a, K, V, Pred: InvariantPredicate<K, V>>(_inv: &'a LocalInvariant<K, V, Pred>) -> (&'a InvariantBlockGuard, V) {
     unimplemented!();
 }
 
 #[rustc_diagnostic_item = "verus::pervasive::invariant::open_invariant_end"]
 #[doc(hidden)]
-#[verifier::external] /* vattr */
+#[cfg_attr(verus_macro_keep_ghost, verifier::external)] /* vattr */
 pub fn open_invariant_end<V>(_guard: &InvariantBlockGuard, _v: V) {
     unimplemented!();
 }
@@ -329,11 +329,11 @@ macro_rules! open_atomic_invariant {
 #[macro_export]
 macro_rules! open_atomic_invariant_internal {
     ($eexpr:expr => $iident:ident => $bblock:block) => {
-        #[verifier::invariant_block] /* vattr */ {
-            #[cfg(not(verus_macro_erase_ghost))]
+        #[cfg_attr(verus_macro_keep_ghost, verifier::invariant_block)] /* vattr */ {
+            #[cfg(verus_macro_keep_ghost)]
             #[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_atomic_invariant_begin($eexpr);
             $bblock
-            #[cfg(not(verus_macro_erase_ghost))]
+            #[cfg(verus_macro_keep_ghost)]
             $crate::invariant::open_invariant_end(guard, $iident);
         }
     }
@@ -446,11 +446,11 @@ macro_rules! open_local_invariant {
 #[macro_export]
 macro_rules! open_local_invariant_internal {
     ($eexpr:expr => $iident:ident => $bblock:block) => {
-        #[verifier::invariant_block] /* vattr */ {
-            #[cfg(not(verus_macro_erase_ghost))]
+        #[cfg_attr(verus_macro_keep_ghost, verifier::invariant_block)] /* vattr */ {
+            #[cfg(verus_macro_keep_ghost)]
             #[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_local_invariant_begin($eexpr);
             $bblock
-            #[cfg(not(verus_macro_erase_ghost))]
+            #[cfg(verus_macro_keep_ghost)]
             $crate::invariant::open_invariant_end(guard, $iident);
         }
     }