Simplify injections in prelude, and move to Rust edition 2024 (#1381)

.github/workflows/rust.yml

@@ -29,7 +29,7 @@ jobs:
           ~/.cargo/registry
           ~/.cargo/git
           target
-        key: ${{ runner.os }}-contracts-${{ hashFiles('creusot-contracts/Cargo.lock') }}
+        key: ${{ runner.os }}-contracts-${{ hashFiles('**/Cargo.lock') }}
     - name: Build creusot-contracts with nightly rustc
       run: cargo build -p creusot-contracts -F nightly
   contracts-build-stable:
@@ -43,7 +43,7 @@ jobs:
           ~/.cargo/registry
           ~/.cargo/git
           target
-        key: ${{ runner.os }}-contracts-stable-${{ hashFiles('creusot-contracts/Cargo.lock') }}
+        key: ${{ runner.os }}-contracts-stable-${{ hashFiles('**/Cargo.lock') }}
     - name: Build creusot-contracts with stable rustc
       run: cargo +stable build -p creusot-contracts
   build:

cargo-creusot/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "cargo-creusot"
 version = "0.3.0"
-edition = "2021"
+edition = "2024"
 publish = false
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

cargo-creusot/src/main.rs

@@ -1,11 +1,11 @@
 use clap::*;
-use creusot_args::{options::*, CREUSOT_RUSTC_ARGS};
+use creusot_args::{CREUSOT_RUSTC_ARGS, options::*};
 use creusot_setup as setup;
 use std::{
     env,
     io::Write,
     path::{Display, PathBuf},
-    process::{exit, Command},
+    process::{Command, exit},
 };
 use tempdir::TempDir;
 
@@ -124,7 +124,9 @@ fn invoke_cargo(args: &CreusotArgs, creusot_rustc: Option<PathBuf>, cargo_flags:
     };
     // creusot_rustc binary exists
     if !creusot_rustc_path.exists() {
-        eprintln!("creusot-rustc not found (expected at {creusot_rustc_path:?}). You should reinstall Creusot.");
+        eprintln!(
+            "creusot-rustc not found (expected at {creusot_rustc_path:?}). You should reinstall Creusot."
+        );
         exit(1);
     }
     let mut cmd = Command::new(cargo_path);
@@ -353,9 +355,5 @@ fn find_dangling_rec(dir: &PathBuf) -> Result<Option<Vec<FileOrDirectory>>> {
             all_dangling = false;
         }
     }
-    if all_dangling {
-        Ok(None)
-    } else {
-        Ok(Some(dangling))
-    }
+    if all_dangling { Ok(None) } else { Ok(Some(dangling)) }
 }

cargo-creusot/src/new.rs

@@ -41,7 +41,7 @@ fn cargo_template(name: &str, dep: &str) -> String {
         r#"[package]
 name = "{name}"
 version = "0.1.0"
-edition = "2021"
+edition = "2024"
 
 [dependencies]
 creusot-contracts = {dep}

cargo-creusot/src/why3_launcher.rs

@@ -4,7 +4,7 @@ use std::{
 };
 
 use super::helpers::Result;
-use include_dir::{include_dir, Dir};
+use include_dir::{Dir, include_dir};
 
 static PRELUDE: Dir<'static> = include_dir!("$CARGO_MANIFEST_DIR/../prelude");
 

cargo-creusot/src/why3find_wrapper.rs

@@ -1,6 +1,6 @@
-use anyhow::{anyhow, Result};
+use anyhow::{Result, anyhow};
 use clap::*;
-use creusot_setup::{creusot_paths, Paths, PROVERS};
+use creusot_setup::{PROVERS, Paths, creusot_paths};
 use std::{
     path::{Path, PathBuf},
     process::Command,
@@ -48,11 +48,7 @@ fn raw_config(args: &Vec<String>, paths: &Paths) -> Result<()> {
         .map_err(|e| anyhow::Error::new(e).context("'why3find config' failed to launch"))
         .and_then(
             |status| {
-                if status.success() {
-                    Ok(())
-                } else {
-                    Err(anyhow!("'why3find config' failed"))
-                }
+                if status.success() { Ok(()) } else { Err(anyhow!("'why3find config' failed")) }
             },
         )
 }
@@ -81,11 +77,7 @@ fn raw_prove(args: ProveArgs, paths: &Paths) -> Result<()> {
         .map_err(|e| anyhow::Error::new(e).context("'why3find prove' failed to launch"))
         .and_then(
             |status| {
-                if status.success() {
-                    Ok(())
-                } else {
-                    Err(anyhow!("'why3find prove' failed"))
-                }
+                if status.success() { Ok(()) } else { Err(anyhow!("'why3find prove' failed")) }
             },
         )
 }
@@ -98,7 +90,9 @@ pub fn why3find_config(args: ConfigArgs) -> Result<()> {
 pub fn why3find_prove(args: ProveArgs) -> Result<()> {
     let paths = creusot_paths()?;
     if !why3find_json_exists() {
-        return Err(anyhow::anyhow!("why3find.json not found. Perhaps you are in the wrong directory, or you need to run `cargo creusot config`."));
+        return Err(anyhow::anyhow!(
+            "why3find.json not found. Perhaps you are in the wrong directory, or you need to run `cargo creusot config`."
+        ));
     }
     raw_prove(args, &paths)
 }

creusot-args/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "creusot-args"
 version = "0.3.0"
-edition = "2021"
+edition = "2024"
 publish = false
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

creusot-contracts-dummy/src/lib.rs

@@ -154,11 +154,7 @@ fn is_invariant(path: &syn::Path) -> bool {
 
 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
-        }
+        if let syn::Meta::List(meta) = &attr.meta { !is_invariant(&meta.path) } else { true }
     });
 }
 

creusot-contracts-proc/src/derive/clone.rs

@@ -1,8 +1,8 @@
 use proc_macro2::{Ident, TokenStream};
 use quote::{format_ident, quote, quote_spanned};
 use syn::{
-    parse_macro_input, parse_quote, spanned::Spanned, Data, DeriveInput, Fields, GenericParam,
-    Generics, Index,
+    Data, DeriveInput, Fields, GenericParam, Generics, Index, parse_macro_input, parse_quote,
+    spanned::Spanned,
 };
 
 pub fn derive_clone(input: proc_macro::TokenStream) -> proc_macro::TokenStream {

creusot-contracts-proc/src/derive/deep_model.rs

@@ -1,8 +1,8 @@
 use proc_macro2::{Ident, TokenStream};
 use quote::{format_ident, quote, quote_spanned};
 use syn::{
-    parse_macro_input, parse_quote, spanned::Spanned, Data, DeriveInput, Error, Expr, ExprLit,
-    Fields, GenericParam, Generics, Index, Lit, Meta, MetaNameValue, Path,
+    Data, DeriveInput, Error, Expr, ExprLit, Fields, GenericParam, Generics, Index, Lit, Meta,
+    MetaNameValue, Path, parse_macro_input, parse_quote, spanned::Spanned,
 };
 
 pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
@@ -80,7 +80,7 @@ fn add_trait_bounds(mut generics: Generics) -> Generics {
 
 fn deep_model_ty_fields(fields: &Fields) -> TokenStream {
     match fields {
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             let recurse = fields.named.iter().map(|f| {
                 let name = &f.ident;
                 let ty = &f.ty;
@@ -93,7 +93,7 @@ fn deep_model_ty_fields(fields: &Fields) -> TokenStream {
                  { #(#recurse),*}
             }
         }
-        Fields::Unnamed(ref fields) => {
+        Fields::Unnamed(fields) => {
             let recurse = fields.unnamed.iter().map(|f| {
                 let ty = &f.ty;
                 let vis = &f.vis;
@@ -111,12 +111,12 @@ fn deep_model_ty_fields(fields: &Fields) -> TokenStream {
 
 fn deep_model_ty(base_ident: &Ident, generics: &Generics, data: &Data) -> TokenStream {
     match data {
-        Data::Struct(ref data) => {
+        Data::Struct(data) => {
             let semi_colon = data.semi_token;
             let data = deep_model_ty_fields(&data.fields);
             quote! { struct #base_ident #generics #data #semi_colon }
         }
-        Data::Enum(ref data) => {
+        Data::Enum(data) => {
             let arms = data.variants.iter().map(|v| {
                 let ident = &v.ident;
                 let fields = deep_model_ty_fields(&v.fields);

creusot-contracts-proc/src/derive/default.rs

@@ -1,8 +1,8 @@
 use proc_macro2::{Span, TokenStream};
 use quote::{quote, quote_spanned};
 use syn::{
-    parse_macro_input, parse_quote, spanned::Spanned, Data, DeriveInput, Fields, GenericParam,
-    Generics, Ident,
+    Data, DeriveInput, Fields, GenericParam, Generics, Ident, parse_macro_input, parse_quote,
+    spanned::Spanned,
 };
 
 /// Derive `Default` and `creusot_contracts::Default` on the given type.

creusot-contracts-proc/src/derive/partial_eq.rs

@@ -1,8 +1,8 @@
 use proc_macro2::{Ident, TokenStream};
 use quote::{format_ident, quote, quote_spanned};
 use syn::{
-    parse_macro_input, parse_quote, spanned::Spanned, Data, DeriveInput, Fields, GenericParam,
-    Generics, Index,
+    Data, DeriveInput, Fields, GenericParam, Generics, Index, parse_macro_input, parse_quote,
+    spanned::Spanned,
 };
 
 pub fn derive_partial_eq(input: proc_macro::TokenStream) -> proc_macro::TokenStream {

creusot-contracts-proc/src/derive/resolve.rs

@@ -1,6 +1,6 @@
 use proc_macro2::{Ident, TokenStream};
 use quote::{format_ident, quote, quote_spanned};
-use syn::{parse_macro_input, spanned::Spanned, Data, DeriveInput, Fields, Index};
+use syn::{Data, DeriveInput, Fields, Index, parse_macro_input, spanned::Spanned};
 
 pub fn derive_resolve(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let input = parse_macro_input!(input as DeriveInput);

creusot-contracts-proc/src/doc.rs

@@ -30,7 +30,9 @@ pub(crate) fn document_spec(spec_name: &str, spec_body: LogicBody) -> TokenStrea
         LogicBody::Some(s) if !s.is_empty() => s,
         _ => {
             let spec = if matches!(spec_body, LogicBody::Trusted) {
-                format!("{styled_spec_name} <span class=\"tooltip\" style=\"color:Red; white-space:nowrap;\" data-title=\"this function is trusted\"><sup>&#9888;</sup></span>")
+                format!(
+                    "{styled_spec_name} <span class=\"tooltip\" style=\"color:Red; white-space:nowrap;\" data-title=\"this function is trusted\"><sup>&#9888;</sup></span>"
+                )
             } else {
                 styled_spec_name
             };

creusot-contracts-proc/src/extern_spec.rs

@@ -1,7 +1,7 @@
 use crate::{doc::DocItemName, generate_unique_ident};
 use pearlite_syn::term::*;
 use proc_macro2::TokenStream;
-use quote::{quote, ToTokens};
+use quote::{ToTokens, quote};
 use syn::{
     parse::Parse,
     punctuated::{Pair, Punctuated},

creusot-contracts-proc/src/invariant.rs

@@ -1,9 +1,9 @@
 use crate::pretyping;
 use proc_macro2::{Span, TokenStream};
-use quote::{quote, quote_spanned, ToTokens};
+use quote::{ToTokens, quote, quote_spanned};
 use syn::{
-    parse_quote_spanned, spanned::Spanned, token::Brace, AttrStyle, Attribute, Block, Error, Expr,
-    ExprForLoop, ExprLoop, ExprWhile, Ident, ItemFn, Meta, Result, Stmt, Token,
+    AttrStyle, Attribute, Block, Error, Expr, ExprForLoop, ExprLoop, ExprWhile, Ident, ItemFn,
+    Meta, Result, Stmt, Token, parse_quote_spanned, spanned::Spanned, token::Brace,
 };
 
 #[derive(Debug, Clone, Copy)]
@@ -73,7 +73,7 @@ fn desugar(tag: Tag, invariant0: TokenStream, expr: TokenStream) -> Result<Token
             return Err(Error::new_spanned(
                 expr,
                 "invariants must be attached to either a `for`, `loop` or `while`",
-            ))
+            ));
         }
     }
 }
@@ -180,22 +180,17 @@ fn desugar_for(mut invariants: Vec<Invariant>, f: ExprForLoop) -> TokenStream {
         },
     );
 
-    invariants.insert(
-        0,
-        Invariant {
-            tag: Tag::Invariant(ForInvariant),
-            span: for_span,
-            term: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(#it) },
-        },
-    );
+    invariants.insert(0, Invariant {
+        tag: Tag::Invariant(ForInvariant),
+        span: for_span,
+        term: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(#it) },
+    });
 
-    invariants.insert(0,
-        Invariant {
-            tag: Tag::Invariant(ForInvariant),
-            span: for_span,
-            term: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(*#produced) },
-        },
-    );
+    invariants.insert(0, Invariant {
+        tag: Tag::Invariant(ForInvariant),
+        span: for_span,
+        term: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(*#produced) },
+    });
 
     let elem = Ident::new("__creusot_proc_iter_elem", proc_macro::Span::def_site().into());
 

creusot-contracts-proc/src/lib.rs

@@ -5,7 +5,7 @@ extern crate proc_macro;
 use pearlite_syn::*;
 use proc_macro::TokenStream as TS1;
 use proc_macro2::{Span, TokenStream};
-use quote::{quote, quote_spanned, ToTokens, TokenStreamExt};
+use quote::{ToTokens, TokenStreamExt, quote, quote_spanned};
 use std::iter;
 use syn::{
     parse::{Parse, Result},
@@ -609,11 +609,7 @@ pub fn predicate(prophetic: TS1, tokens: TS1) -> TS1 {
         None
     } else {
         let t = parse_macro_input!(prophetic as Ident);
-        if t == "prophetic" {
-            Some(quote!(#[creusot::decl::logic::prophetic]))
-        } else {
-            None
-        }
+        if t == "prophetic" { Some(quote!(#[creusot::decl::logic::prophetic])) } else { None }
     };
 
     let pred = parse_macro_input!(tokens as LogicInput);

creusot-contracts-proc/src/pretyping.rs

@@ -1,9 +1,9 @@
 use pearlite_syn::Term as RT;
 use proc_macro2::{Delimiter, Group, Span, TokenStream, TokenTree};
-use syn::{spanned::Spanned, ExprMacro, Pat, UnOp};
+use syn::{ExprMacro, Pat, UnOp, spanned::Spanned};
 
 use pearlite_syn::term::*;
-use quote::{quote, quote_spanned, ToTokens};
+use quote::{ToTokens, quote, quote_spanned};
 use syn::Lit;
 
 #[derive(Debug)]
@@ -165,17 +165,15 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
             })
         }
         RT::Let(_) => Err(EncodeError::Unsupported(term.span(), "Let".into())),
-        RT::Lit(TermLit { ref lit }) => match lit {
+        RT::Lit(TermLit { lit: lit @ Lit::Int(int) }) if int.suffix() == "" => {
             // FIXME: allow unbounded integers
-            Lit::Int(int) if int.suffix() == "" => {
-                Ok(quote_spanned! {sp=> ::creusot_contracts::model::View::view(#lit as i128) })
-            }
-            Lit::Int(int) if int.suffix() == "int" => {
-                let lit = syn::LitInt::new(int.base10_digits(), int.span());
-                Ok(quote_spanned! {sp=> ::creusot_contracts::model::View::view(#lit as i128) })
-            }
-            _ => Ok(quote_spanned! {sp=> #lit }),
-        },
+            Ok(quote_spanned! {sp=> ::creusot_contracts::model::View::view(#lit as i128) })
+        }
+        RT::Lit(TermLit { lit: Lit::Int(int) }) if int.suffix() == "int" => {
+            let lit = syn::LitInt::new(int.base10_digits(), int.span());
+            Ok(quote_spanned! {sp=> ::creusot_contracts::model::View::view(#lit as i128) })
+        }
+        RT::Lit(TermLit { lit }) => Ok(quote_spanned! {sp=> #lit }),
         RT::Match(TermMatch { expr, arms, .. }) => {
             let arms: Vec<_> = arms.iter().map(encode_arm).collect::<Result<_, _>>()?;
             let expr = encode_term(expr)?;

creusot-contracts/src/lib.rs

@@ -400,7 +400,7 @@ pub mod well_founded;
 mod base_prelude {
     pub use crate::{
         ghost::GhostBox,
-        logic::{ops::IndexLogic as _, Int, OrdLogic, Seq},
+        logic::{Int, OrdLogic, Seq, ops::IndexLogic as _},
         model::{DeepModel, View},
         resolve::*,
         snapshot::Snapshot,