Make creusot-contracts build on stable toolchain

.github/workflows/rust.yml

@@ -29,8 +29,21 @@ jobs:
           ~/.cargo/git
           target
         key: ${{ runner.os }}-contracts-${{ hashFiles('creusot-contracts/Cargo.lock') }}
-    - name: Build creusot-contracts with rustc
-      run: cargo build -p creusot-contracts
+    - name: Build creusot-contracts with nightly rustc
+      run: cargo build -p creusot-contracts -F nightly
+  contracts-build-stable:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: actions/cache@v4
+      with:
+        path: |
+          ~/.cargo/registry
+          ~/.cargo/git
+          target
+        key: ${{ runner.os }}-contracts-stable-${{ hashFiles('creusot-contracts/Cargo.lock') }}
+    - name: Build creusot-contracts with stable rustc
+      run: cargo +stable build -p creusot-contracts
   build:
     runs-on: ubuntu-latest
     steps:

cargo-creusot/src/main.rs

@@ -161,6 +161,7 @@ fn invoke_cargo(args: &CreusotArgs, creusot_rustc: Option<PathBuf>, cargo_flags:
     cmd.arg(format!("+{toolchain}"))
         .arg(cargo_cmd)
         .args(cargo_flags)
+        .args(["-F", "creusot-contracts/nightly"])
         .env("RUSTC", creusot_rustc_path)
         .env("CARGO_CREUSOT", "1");
     // Incremental compilation causes Creusot to not see all of a crate's code

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]
@@ -111,3 +117,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/Cargo.toml

@@ -17,10 +17,10 @@ creusot-contracts-proc = { path = "../creusot-contracts-proc", version = "0.3.0"
 creusot-contracts-dummy = { path = "../creusot-contracts-dummy", version = "0.3.0" }
 
 [features]
-default = []
-typechecker = []
-contracts = []
-
+# Enabled by creusot.
+# Must be disabled to build with stable Rust.
+# May be enabled to build with nightly Rust.
+nightly = []
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(creusot)'] }

creusot-contracts/src/ghost.rs

@@ -63,7 +63,7 @@ impl<T: ?Sized> Deref for GhostBox<T> {
     type Target = T;
 
     /// This function can only be called in `ghost!` context
-    #[rustc_diagnostic_item = "ghost_box_deref"]
+    #[cfg_attr(creusot, rustc_diagnostic_item = "ghost_box_deref")]
     #[pure]
     #[ensures(*(*self).0 == *result)]
     fn deref(&self) -> &Self::Target {
@@ -79,7 +79,7 @@ impl<T: ?Sized> Deref for GhostBox<T> {
 }
 impl<T: ?Sized> DerefMut for GhostBox<T> {
     /// This function can only be called in `ghost!` context
-    #[rustc_diagnostic_item = "ghost_box_deref_mut"]
+    #[cfg_attr(creusot, rustc_diagnostic_item = "ghost_box_deref_mut")]
     #[pure]
     #[ensures(result == &mut *self.0)]
     fn deref_mut(&mut self) -> &mut Self::Target {
@@ -181,7 +181,7 @@ impl<T> GhostBox<T> {
     /// This function can only be called in `ghost!` code.
     #[pure]
     #[ensures(*result.0 == x)]
-    #[rustc_diagnostic_item = "ghost_box_new"]
+    #[cfg_attr(creusot, rustc_diagnostic_item = "ghost_box_new")]
     pub fn new(x: T) -> Self {
         #[cfg(creusot)]
         {
@@ -206,7 +206,7 @@ impl<T> GhostBox<T> {
     /// This function can only be called in `ghost!` context.
     #[pure]
     #[ensures(result == *self.0)]
-    #[rustc_diagnostic_item = "ghost_box_into_inner"]
+    #[cfg_attr(creusot, rustc_diagnostic_item = "ghost_box_into_inner")]
     pub fn into_inner(self) -> T {
         #[cfg(creusot)]
         {

creusot-contracts/src/invariant.rs

@@ -6,6 +6,7 @@ pub trait Invariant {
     fn invariant(self) -> bool;
 }
 
+#[cfg(feature = "nightly")]
 impl Invariant for ! {
     #[predicate(prophetic)]
     #[open]

creusot-contracts/src/lib.rs

@@ -22,28 +22,27 @@
 //! ```
 //!
 //! For a more detailed explanation, see the [guide](https://creusot-rs.github.io/creusot/guide).
-
 #![cfg_attr(
-    creusot,
-    feature(unsized_locals, fn_traits),
-    allow(incomplete_features),
-    feature(slice_take),
-    feature(print_internals, fmt_internals, fmt_helpers_for_derive)
-)]
-#![cfg_attr(feature = "typechecker", feature(rustc_private), feature(box_patterns))]
-#![feature(
-    step_trait,
-    allocator_api,
-    unboxed_closures,
-    tuple_trait,
-    panic_internals,
-    libstd_sys_internals,
-    rt,
-    never_type,
-    ptr_metadata
+    feature = "nightly",
+    allow(incomplete_features, internal_features),
+    feature(
+        unsized_locals,
+        fn_traits,
+        slice_take,
+        print_internals,
+        fmt_internals,
+        fmt_helpers_for_derive,
+        step_trait,
+        allocator_api,
+        unboxed_closures,
+        tuple_trait,
+        panic_internals,
+        libstd_sys_internals,
+        rt,
+        never_type,
+        ptr_metadata
+    )
 )]
-#![cfg_attr(not(creusot), feature(rustc_attrs))]
-#![cfg_attr(not(creusot), allow(internal_features))]
 
 extern crate self as creusot_contracts;
 

creusot-contracts/src/logic/ops/index.rs

@@ -1,6 +1,7 @@
 //! Definition of [`IndexLogic`]
 
 use crate::*;
+#[cfg(feature = "nightly")]
 use ::std::alloc::Allocator;
 
 /// Used for indexing operations (`container[index]`) in pearlite.
@@ -17,6 +18,7 @@ pub trait IndexLogic<I: ?Sized> {
     fn index_logic(self, idx: I) -> Self::Item;
 }
 
+#[cfg(feature = "nightly")]
 impl<T, A: Allocator> IndexLogic<Int> for Vec<T, A> {
     type Item = T;
 
@@ -28,6 +30,7 @@ impl<T, A: Allocator> IndexLogic<Int> for Vec<T, A> {
     }
 }
 
+#[cfg(feature = "nightly")]
 impl<T, A: Allocator> IndexLogic<usize> for Vec<T, A> {
     type Item = T;
 
@@ -93,3 +96,14 @@ impl<T> IndexLogic<Int> for Snapshot<Seq<T>> {
         pearlite! { (*self)[ix] }
     }
 }
+
+/// Dummy impls that don't use the unstable trait Allocator
+#[cfg(not(feature = "nightly"))]
+impl<T> IndexLogic<Int> for Vec<T> {
+    type Item = T;
+}
+
+#[cfg(not(feature = "nightly"))]
+impl<T> IndexLogic<usize> for Vec<T> {
+    type Item = T;
+}

creusot-contracts/src/snapshot.rs

@@ -26,8 +26,11 @@ use crate::std::ops::Deref;
 /// let m: Snapshot<Mapping<Int, Int>> = snapshot!(|x| x + 1);
 /// ```
 #[trusted]
-#[rustc_diagnostic_item = "snapshot_ty"]
-#[cfg_attr(creusot, creusot::builtins = "prelude.prelude.Snapshot.snap_ty")]
+#[cfg_attr(
+    creusot,
+    rustc_diagnostic_item = "snapshot_ty",
+    creusot::builtins = "prelude.prelude.Snapshot.snap_ty"
+)]
 pub struct Snapshot<T: ?Sized>(pub(crate) std::marker::PhantomData<T>);
 
 #[cfg(creusot)]

creusot-contracts/src/std/boxed.rs

@@ -1,6 +1,9 @@
-use crate::{invariant::*, std::alloc::Allocator, *};
+use crate::{invariant::*, *};
+#[cfg(feature = "nightly")]
+use ::std::alloc::Allocator;
 pub use ::std::boxed::*;
 
+#[cfg(feature = "nightly")]
 impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A> {
     type DeepModelTy = Box<T::DeepModelTy>;
     #[logic]
@@ -10,6 +13,7 @@ impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A> {
     }
 }
 
+#[cfg(feature = "nightly")]
 impl<T: View + ?Sized, A: Allocator> View for Box<T, A> {
     type ViewTy = T::ViewTy;
     #[logic]
@@ -19,6 +23,7 @@ impl<T: View + ?Sized, A: Allocator> View for Box<T, A> {
     }
 }
 
+#[cfg(feature = "nightly")]
 impl<T: ?Sized, A: Allocator> Invariant for Box<T, A> {
     #[predicate(prophetic)]
     #[open]
@@ -51,3 +56,17 @@ extern_spec! {
         }
     }
 }
+
+/// Dummy impls that don't use the unstable trait Allocator
+#[cfg(not(feature = "nightly"))]
+impl<T: DeepModel + ?Sized> DeepModel for Box<T> {
+    type DeepModelTy = Box<T::DeepModelTy>;
+}
+
+#[cfg(not(feature = "nightly"))]
+impl<T: View + ?Sized> View for Box<T> {
+    type ViewTy = T::ViewTy;
+}
+
+#[cfg(not(feature = "nightly"))]
+impl<T: ?Sized> Invariant for Box<T> {}