Update the rustc pin

.envrc

@@ -1 +1,2 @@
+watch_file ./charon/rust-toolchain
 use flake

.github/workflows/ci.yml

@@ -68,3 +68,4 @@ jobs:
           nix flake update charon --override-input charon github:aeneasverif/charon/${{ github.sha }}
           nix flake update --refresh eurydice
           ./check.sh ml-kem-small
+          ./check.sh ml-dsa-small

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.73"
+let supported_charon_version = "0.1.74"

charon-ml/src/ExpressionsUtils.ml

@@ -2,7 +2,7 @@ open Expressions
 
 let unop_can_fail (unop : unop) : bool =
   match unop with
-  | Neg | Cast _ -> true
+  | Neg | Cast _ | PtrMetadata -> true
   | Not -> false
 
 let binop_can_fail (binop : binop) : bool =

charon-ml/src/PrintExpressions.ml

@@ -67,6 +67,7 @@ let unop_to_string (env : 'a fmt_env) (unop : unop) : string =
   match unop with
   | Not -> "¬"
   | Neg -> "-"
+  | PtrMetadata -> "ptr_metadata"
   | Cast cast_kind -> cast_kind_to_string env cast_kind
 
 let binop_to_string (binop : binop) : string =

charon-ml/src/generated/Generated_Expressions.ml

@@ -81,6 +81,8 @@ and unop =
           (in debug mode) to check that it is not equal to the minimum integer
           value (for the proper type).
        *)
+  | PtrMetadata
+      (** Retreive the metadata part of a fat pointer. For slices, this retreives their length. *)
   | Cast of cast_kind
       (** Casts are rvalues in MIR, but we treat them as unops. *)
 

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -91,6 +91,7 @@ and unop_of_json (ctx : of_json_ctx) (js : json) : (unop, string) result =
     (match js with
     | `String "Not" -> Ok Not
     | `String "Neg" -> Ok Neg
+    | `String "PtrMetadata" -> Ok PtrMetadata
     | `Assoc [ ("Cast", cast) ] ->
         let* cast = cast_kind_of_json ctx cast in
         Ok (Cast cast)

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.73"
+version = "0.1.74"
 authors = ["Son Ho <hosonmarc@gmail.com>", "Guillaume Boisseau <nadrieril+git@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"

charon/rust-toolchain

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2024-11-23"
+channel = "nightly-2025-03-29"
 components = [ "rustc-dev", "llvm-tools-preview" ]

charon/src/ast/expressions.rs

@@ -158,6 +158,8 @@ pub enum UnOp {
     /// (in debug mode) to check that it is not equal to the minimum integer
     /// value (for the proper type).
     Neg,
+    /// Retreive the metadata part of a fat pointer. For slices, this retreives their length.
+    PtrMetadata,
     /// Casts are rvalues in MIR, but we treat them as unops.
     Cast(CastKind),
     /// Coercion from array (i.e., [T; N]) to slice.

charon/src/ast/llbc_ast_utils.rs

@@ -118,7 +118,7 @@ impl Block {
 
     /// Apply a function to all the statements, in a top-down manner.
     pub fn visit_statements<F: FnMut(&mut Statement)>(&mut self, f: F) {
-        BlockVisitor::new(|_| {}, f).visit(self);
+        let _ = BlockVisitor::new(|_| {}, f).visit(self);
     }
 
     /// Apply a transformer to all the statements, in a bottom-up manner.
@@ -169,7 +169,7 @@ impl Block {
 
     /// Visit `self` and its sub-blocks in a bottom-up (post-order) traversal.
     pub fn visit_blocks_bwd<F: FnMut(&mut Block)>(&mut self, f: F) {
-        BlockVisitor::new(f, |_| {}).visit(self);
+        let _ = BlockVisitor::new(f, |_| {}).visit(self);
     }
 }
 

charon/src/ast/types_utils.rs

@@ -199,15 +199,15 @@ impl<T: AstVisitable> Binder<Binder<T>> {
         // - at binder level 0 we shift all variable ids to match the concatenated params;
         // - at binder level > 0 we decrease binding level because there's one fewer binder.
         let mut bound_value = self.skip_binder.skip_binder;
-        bound_value.drive_mut(&mut FlattenVisitor {
+        let _ = bound_value.drive_mut(&mut FlattenVisitor {
             shift_by: &outer_params,
             binder_depth: Default::default(),
         });
 
         // The inner params must also be updated, as they can refer to themselves and the outer
         // one.
         let mut inner_params = self.skip_binder.params;
-        inner_params.drive_mut(&mut FlattenVisitor {
+        let _ = inner_params.drive_mut(&mut FlattenVisitor {
             shift_by: &outer_params,
             binder_depth: Default::default(),
         });
@@ -837,7 +837,7 @@ pub trait TyVisitable: Sized + AstVisitable {
     }
 
     fn substitute_with_self(mut self, generics: &GenericArgs, self_ref: &TraitRefKind) -> Self {
-        self.drive_mut(&mut SubstVisitor::new(generics, self_ref));
+        let _ = self.drive_mut(&mut SubstVisitor::new(generics, self_ref));
         self
     }
 

charon/src/ast/visitor.rs

@@ -82,11 +82,11 @@ pub trait AstVisitable: Any {
     }
     /// Visit all occurrences of that type inside `self`, in pre-order traversal.
     fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T)) {
-        self.drive(&mut DynVisitor::new_shared::<T>(f));
+        let _ = self.drive(&mut DynVisitor::new_shared::<T>(f));
     }
     /// Visit all occurrences of that type inside `self`, in pre-order traversal.
     fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T)) {
-        self.drive_mut(&mut DynVisitor::new_mut::<T>(f));
+        let _ = self.drive_mut(&mut DynVisitor::new_mut::<T>(f));
     }
 }
 
@@ -173,12 +173,12 @@ impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
 pub trait BodyVisitable: Any {
     /// Visit all occurrences of that type inside `self`, in pre-order traversal.
     fn dyn_visit_in_body<T: BodyVisitable>(&self, f: impl FnMut(&T)) {
-        self.drive_body(&mut DynVisitor::new_shared::<T>(f));
+        let _ = self.drive_body(&mut DynVisitor::new_shared::<T>(f));
     }
 
     /// Visit all occurrences of that type inside `self`, in pre-order traversal.
     fn dyn_visit_in_body_mut<T: BodyVisitable>(&mut self, f: impl FnMut(&mut T)) {
-        self.drive_body_mut(&mut DynVisitor::new_mut::<T>(f));
+        let _ = self.drive_body_mut(&mut DynVisitor::new_mut::<T>(f));
     }
 }
 

charon/src/bin/charon-driver/driver.rs

@@ -4,8 +4,9 @@ use crate::CharonFailure;
 use charon_lib::options::CliOpts;
 use charon_lib::transform::TransformCtx;
 use rustc_driver::{Callbacks, Compilation};
+use rustc_interface::interface::Compiler;
 use rustc_interface::Config;
-use rustc_interface::{interface::Compiler, Queries};
+use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
 use rustc_session::config::{OutputType, OutputTypes, Polonius};
 use std::ops::Deref;
@@ -17,10 +18,8 @@ fn run_compiler_with_callbacks(
     args: Vec<String>,
     callbacks: &mut (dyn Callbacks + Send),
 ) -> Result<(), CharonFailure> {
-    rustc_driver::catch_fatal_errors(|| rustc_driver::RunCompiler::new(&args, callbacks).run())
-        .map_err(|_| CharonFailure::RustcError)?
-        .map_err(|_| CharonFailure::RustcError)?;
-    Ok(())
+    rustc_driver::catch_fatal_errors(|| rustc_driver::run_compiler(&args, callbacks))
+        .map_err(|_| CharonFailure::RustcError)
 }
 
 /// Tweak options to get usable MIR even for foreign crates.
@@ -170,26 +169,17 @@ impl<'a> Callbacks for CharonCallbacks<'a> {
     /// "built" MIR (which results from the conversion to HIR to MIR) to become unaccessible.
     /// Because we require built MIR at the moment, we hook ourselves before MIR-based analysis
     /// passes.
-    fn after_expansion<'tcx>(
-        &mut self,
-        compiler: &Compiler,
-        queries: &'tcx Queries<'tcx>,
-    ) -> Compilation {
+    fn after_expansion<'tcx>(&mut self, compiler: &Compiler, tcx: TyCtxt<'tcx>) -> Compilation {
         // Set up our own `DefId` debug routine.
         rustc_hir::def_id::DEF_ID_DEBUG
             .swap(&(def_id_debug as fn(_, &mut fmt::Formatter<'_>) -> _));
 
-        let transform_ctx = queries.global_ctxt().unwrap().get_mut().enter(|tcx| {
-            translate_crate_to_ullbc::translate(&self.options, tcx, compiler.sess.sysroot.clone())
-        });
+        let transform_ctx =
+            translate_crate_to_ullbc::translate(&self.options, tcx, compiler.sess.sysroot.clone());
         self.transform_ctx = Some(transform_ctx);
         Compilation::Continue
     }
-    fn after_analysis<'tcx>(
-        &mut self,
-        _: &rustc_interface::interface::Compiler,
-        _: &'tcx Queries<'tcx>,
-    ) -> Compilation {
+    fn after_analysis<'tcx>(&mut self, _: &Compiler, _: TyCtxt<'tcx>) -> Compilation {
         // Don't continue to codegen etc.
         Compilation::Stop
     }

charon/src/bin/charon-driver/main.rs

@@ -11,7 +11,6 @@
 
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;
-extern crate rustc_attr;
 extern crate rustc_driver;
 extern crate rustc_error_messages;
 extern crate rustc_errors;

charon/src/bin/charon-driver/translate/get_mir.rs

@@ -83,7 +83,7 @@ fn get_mir_for_def_id_and_level(
     let body = if tcx.is_mir_available(def_id) {
         if let Some(local_def_id) = def_id.as_local()
             && !matches!(
-                tcx.hir().body_const_context(local_def_id),
+                tcx.hir_body_const_context(local_def_id),
                 None | Some(rustc_hir::ConstContext::ConstFn)
             )
         {

charon/src/bin/charon-driver/translate/translate_ctx.rs

@@ -331,7 +331,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             }
             // We map the three namespaces onto a single one. We can always disambiguate by looking
             // at the definition.
-            DefPathItem::TypeNs(symbol)
+            DefPathItem::TypeNs(None) => None,
+            DefPathItem::TypeNs(Some(symbol))
             | DefPathItem::ValueNs(symbol)
             | DefPathItem::MacroNs(symbol) => Some(PathElem::Ident(symbol, disambiguator)),
             DefPathItem::Impl => {
@@ -602,18 +603,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     }
                 }
             }
-            hax::FileName::QuoteExpansion(_)
-            | hax::FileName::Anon(_)
-            | hax::FileName::MacroExpansion(_)
-            | hax::FileName::ProcMacroSourceCode(_)
-            | hax::FileName::CliCrateAttr(_)
-            | hax::FileName::Custom(_)
-            | hax::FileName::DocTest(..)
-            | hax::FileName::InlineAsm(_) => {
-                // We use the debug formatter to generate a filename.
-                // This is not ideal, but filenames are for debugging anyway.
-                FileName::NotReal(format!("{name:?}"))
-            }
+            // We use the debug formatter to generate a filename.
+            // This is not ideal, but filenames are for debugging anyway.
+            _ => FileName::NotReal(format!("{name:?}")),
         }
     }
 
@@ -690,20 +682,25 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
     /// encodes them as attributes). For now we use `String`s for `Attributes`.
     pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
-        match &attr.kind {
-            hax::AttrKind::Normal(normal_attr) => {
+        use hax::Attribute as Haxttribute;
+        use hax::AttributeKind as HaxttributeKind;
+        match attr {
+            Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
+                Some(Attribute::DocComment(comment.to_string()))
+            }
+            Haxttribute::Parsed(_) => None,
+            Haxttribute::Unparsed(attr) => {
                 let raw_attr = RawAttribute {
-                    path: normal_attr.item.path.clone(),
-                    args: match &normal_attr.item.args {
+                    path: attr.path.clone(),
+                    args: match &attr.args {
                         hax::AttrArgs::Empty => None,
                         hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
-                        hax::AttrArgs::Eq(_, hax::AttrArgsEq::Hir(lit)) => self
+                        hax::AttrArgs::Eq { expr, .. } => self
                             .tcx
                             .sess
                             .source_map()
-                            .span_to_snippet(lit.span.rust_span_data.unwrap().span())
+                            .span_to_snippet(expr.span.rust_span_data.unwrap().span())
                             .ok(),
-                        hax::AttrArgs::Eq(..) => None,
                     },
                 };
                 match Attribute::parse_from_raw(raw_attr) {
@@ -715,9 +712,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     }
                 }
             }
-            hax::AttrKind::DocComment(_kind, comment) => {
-                Some(Attribute::DocComment(comment.to_string()))
-            }
         }
     }
 
@@ -729,6 +723,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     hax::InlineAttr::Hint => Some(InlineAttr::Hint),
                     hax::InlineAttr::Never => Some(InlineAttr::Never),
                     hax::InlineAttr::Always => Some(InlineAttr::Always),
+                    hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
                 }
             }
             _ => None,