Enable compilation with stable rust: macros ensures and requires remo…

…ve loop invariants

cargo-creusot/src/new.rs

@@ -55,17 +55,11 @@ unexpected_cfgs = {{ level = "warn", check-cfg = ['cfg(creusot)'] }}
 fn bin_template(name: &str) -> String {
     let name = name.replace("-", "_");
     format!(
-        r#"#![cfg_attr(
-    not(creusot),
-    feature(stmt_expr_attributes, proc_macro_hygiene, register_tool)
-)]
-#![cfg_attr(not(creusot), register_tool(creusot))]
-
-#[allow(unused_imports)]
+        r#"#[allow(unused_imports)]
 use creusot_contracts::*;
 use {name}::*;
 
-#[allow(creusot::experimental)]
+#[cfg_attr(creusot, allow(creusot::experimental))]
 fn main() {{
     assert!(add_one(2) == 3);
     println!("Hello, world!");
@@ -74,7 +68,7 @@ fn main() {{
     )
 }
 
-const TEST_TEMPLATE: &str = r#"#![cfg_attr(not(creusot), feature(stmt_expr_attributes, proc_macro_hygiene))]
+const TEST_TEMPLATE: &str = r#"#[allow(unused_imports)]
 use creusot_contracts::*;
 
 #[test]
@@ -83,8 +77,7 @@ fn it_works() {
 }
 "#;
 
-const LIB_TEMPLATE: &str = r#"#![cfg_attr(not(creusot), feature(stmt_expr_attributes, proc_macro_hygiene))]
-use creusot_contracts::*;
+const LIB_TEMPLATE: &str = r#"use creusot_contracts::*;
 
 #[requires(a@ < i64::MAX@)]
 #[ensures(result@ == a@ + 1)]
@@ -93,11 +86,6 @@ pub fn add_one(a: i64) -> i64 {
 }
 "#;
 
-const RUST_TOOLCHAIN: &str = r#"[toolchain]
-channel = "nightly-2024-07-25"
-components = [ "rustfmt" ]
-"#;
-
 pub fn new(args: NewArgs) -> Result<()> {
     validate_name(&args.name)?;
     fs::create_dir(&args.name).map_err(|e| {
@@ -134,7 +122,6 @@ pub fn create_project(name: String, args: NewInitArgs) -> Result<()> {
         None => r#""*""#.to_string(),
     };
     write("Cargo.toml", &cargo_template(&name, &contract_dep));
-    write("rust-toolchain", RUST_TOOLCHAIN);
     if args.tests {
         fs::create_dir_all("tests")?;
         write("tests/test.rs", TEST_TEMPLATE);

creusot-contracts-dummy/Cargo.toml

@@ -14,4 +14,4 @@ proc-macro = true
 [dependencies]
 quote = "1.0"
 proc-macro2 = "1.0"
-
+syn = { version = "2", features = ["full", "visit-mut"] }

creusot-contracts-dummy/src/lib.rs

@@ -4,15 +4,21 @@ extern crate proc_macro;
 mod ghost;
 
 use proc_macro::TokenStream as TS1;
+use quote::ToTokens as _;
+use syn::visit_mut::VisitMut;
 
 #[proc_macro_attribute]
 pub fn requires(_: TS1, tokens: TS1) -> TS1 {
-    tokens
+    let mut item = syn::parse_macro_input!(tokens as syn::ImplItemFn);
+    delete_invariants(&mut item);
+    TS1::from(item.into_token_stream())
 }
 
 #[proc_macro_attribute]
 pub fn ensures(_: TS1, tokens: TS1) -> TS1 {
-    tokens
+    let mut item = syn::parse_macro_input!(tokens as syn::ImplItemFn);
+    delete_invariants(&mut item);
+    TS1::from(item.into_token_stream())
 }
 
 #[proc_macro_attribute]
@@ -106,3 +112,52 @@ pub fn derive_deep_model(_: TS1) -> TS1 {
 pub fn derive_resolve(_: TS1) -> TS1 {
     TS1::new()
 }
+
+/// Visitor to delete all `#[invariant]` and `#[creusot_contracts::invariant]`
+/// attributes on loops.
+struct DeleteInvariants;
+
+impl VisitMut for DeleteInvariants {
+    fn visit_expr_for_loop_mut(&mut self, i: &mut syn::ExprForLoop) {
+        delete_invariants_attrs(&mut i.attrs);
+        syn::visit_mut::visit_expr_for_loop_mut(self, i)
+    }
+
+    fn visit_expr_while_mut(&mut self, i: &mut syn::ExprWhile) {
+        delete_invariants_attrs(&mut i.attrs);
+        syn::visit_mut::visit_expr_while_mut(self, i)
+    }
+
+    fn visit_expr_loop_mut(&mut self, i: &mut syn::ExprLoop) {
+        delete_invariants_attrs(&mut i.attrs);
+        syn::visit_mut::visit_expr_loop_mut(self, i)
+    }
+}
+
+// `invariant` or `creusot_contracts::invariant` or `::creusot_contracts::invariant`
+fn is_invariant(path: &syn::Path) -> bool {
+    if path.is_ident("invariant") {
+        return true;
+    }
+    let mut segments = path.segments.iter();
+    if let Some(first) = segments.next() {
+        if let Some(second) = segments.next() {
+            return first.ident == "creusot_contracts" && second.ident == "invariant";
+        }
+    }
+    false
+}
+
+fn delete_invariants_attrs(attrs: &mut Vec<syn::Attribute>) {
+    attrs.retain(|attr| {
+        if let syn::Meta::List(meta) = &attr.meta {
+            !is_invariant(&meta.path)
+        } else {
+            true
+        }
+    });
+}
+
+fn delete_invariants(item: &mut syn::ImplItemFn) {
+    DeleteInvariants.visit_impl_item_fn_mut(item);
+}

creusot-contracts/tests/compile_test.rs

@@ -0,0 +1,16 @@
+// Test that we can build verified code without enabling unstable features
+
+use creusot_contracts::*;
+
+// Test that `ensures` removes loop invariants
+#[ensures(true)]
+pub fn f() {
+    #[invariant(true)]
+    for _ in 0..1 {
+        #[creusot_contracts::invariant(true)]
+        while false {
+            #[::creusot_contracts::invariant(true)]
+            loop {}
+        }
+    }
+}

guide/src/basic_concepts/invariants.md

@@ -42,3 +42,21 @@ An `invariant` generates two verification conditions in Why3:
 
 - First, that the invariants holds before the loop (initialization).
 - Second, that if the invariant holds at the beginning of a loop iteration, then it holds at the end of it.
+
+## Compiling with `rustc`
+
+Make sure that functions that contain `#[invariant(...)]` attributes also have
+an `#[ensures(...)]` or `#[requires(...)]` attribute.
+You can always add `#[ensures(true)]` as a trivial contract.
+
+That enables compilation (`cargo build`) with a stable Rust compiler,
+preventing the following error:
+
+```
+error[E0658]: attributes on expressions are experimental
+```
+
+Indeed, the `#[invariant(...)]` attribute on loops is only allowed by unstable features
+(`stmt_expr_attributes`, `proc_macro_hygiene`). For compatibility with stable Rust,
+the `requires` and `ensures` macros remove `#[invariant(...)]`
+attributes during normal compilation.