Bump rustc to remove ShallowInitBox

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.197"
+let supported_charon_version = "0.1.198"

charon-ml/src/Print.ml

@@ -936,8 +936,6 @@ and rvalue_to_string (env : fmt_env) (rv : rvalue) : string =
       "[" ^ operand_to_string env v ^ ";"
       ^ constant_expr_to_string env len
       ^ "]"
-  | ShallowInitBox (op, _) ->
-      "shallow-init-box(" ^ operand_to_string env op ^ ")"
   | Aggregate (akind, ops) -> aggregate_to_string env akind ops
 
 let item_id_to_string (id : item_id) : string =

charon-ml/src/generated/Generated_Expressions.ml

@@ -310,11 +310,6 @@ and rvalue =
       (** [Repeat(x, n)] creates an array where [x] is copied [n] times.
 
           We translate this to a function call for LLBC. *)
-  | ShallowInitBox of operand * ty
-      (** Transmutes a [*mut u8] (obtained from [malloc]) into
-          shallow-initialized [Box<T>]. This only appears as part of lowering
-          [Box::new()] in some cases. We reconstruct the original [Box::new()]
-          call, but sometimes may fail to do so, leaking the expression. *)
 
 (** Unary operation *)
 and unop =

charon-ml/src/generated/Generated_OfJson.ml

@@ -1137,10 +1137,6 @@ and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
         let* x_1 = ty_of_json ctx x_1 in
         let* x_2 = box_of_json constant_expr_of_json ctx x_2 in
         Ok (Repeat (x_0, x_1, x_2))
-    | `Assoc [ ("ShallowInitBox", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = operand_of_json ctx x_0 in
-        let* x_1 = ty_of_json ctx x_1 in
-        Ok (ShallowInitBox (x_0, x_1))
     | _ -> Error "")
 
 and scalar_value_of_json (ctx : of_json_ctx) (js : json) :

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -1048,10 +1048,6 @@ and rvalue_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
          let* x_1 = ty_of_postcard ctx st in
          let* x_2 = box_of_postcard constant_expr_of_postcard ctx st in
          Ok (Repeat (x_0, x_1, x_2))
-     | 10 ->
-         let* x_0 = operand_of_postcard ctx st in
-         let* x_1 = ty_of_postcard ctx st in
-         Ok (ShallowInitBox (x_0, x_1))
      | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag))
 
 and scalar_value_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :

charon/AGENTS.md

@@ -0,0 +1,62 @@
+# AGENTS.md
+
+Guidance for AI agents working on Charon.
+
+## Working Style
+
+- Charon is written with the following values in mind: correctness, robustness, maintainability, and
+  solving people's problems (also, finding joy in clean code and abstractions).
+- The codebase is built around carefully-crafted invariants, e.g. how we go from rustc to hax to
+  charon for `GenericArgs`, or how mono mode is transparent most of the time.
+- Read the surrounding code before editing. Most problems in this repository already have a nearby
+  pattern in another translation pass, AST utility, or normalization pass.
+- We are the owners of this codebase, we can make deep changes if that's the best way to solve
+  a problem.
+- Exercise judgment: sometimes the right fix is downstream (e.g. in aeneas) or upstream (e.g. in
+  rustc itself); I don't shy from fixing the bugs where they should be fixed (though well-placed
+  workarounds are often fine).
+- Correctness comes first. We should be very careful when modifying what we got from rustc. Even
+  tricky cases should be handled correctly; if in doubt, double-check and add tests.
+- Robustness comes second. Charon should be able to emit an llbc file even in the face of many
+  errors. Use panics appropriately, when they indicate a broken invariant within Charon. Use errors
+  when the invariant is less clear and/or there's high risk of it being broken in practice.
+- Maintainability comes third. Prefer small, principled changes over local cleverness. A change that
+  introduces a ton of code at once is suspicious; there's often a cleaner way. I'm the sole
+  maintainer so any unneeded complexity is a cost I'll have to bear in the future.
+- If in doubt, ask, and exercise judgment as a good OSS maintainer would.
+
+## Implementing Translation and Transformations
+
+- Avoid constructing generic arguments manually to avoid getting trait references wrong. Prefer
+  obtaining generics from an existing call, type, translated item, or Hax/rustc API.
+- Be careful about monomorphized mode: it can break some assumptions such as the fact that a given
+  item exists only once. If an approach relies on polymorphic item paths, function names, or
+  non-monomorphized generic structure, either make it work in mono deliberately or gate the pass off
+  in mono mode.
+- Prefer rustc and Hax APIs for item discovery and method resolution. Use `def_path_def_ids`/path
+  resolution for named standard items, and Hax `ItemRef`s when the result should flow through normal
+  Charon translation.
+- Be careful with `ctx.translated`: some bodies stored there may not have gone through later body
+  cleanup passes yet. If a pass reads from translated bodies while transformations are fused,
+  consider whether it is seeing pre-pass or post-pass state.
+- If a pass needs a declaration id, prefer an initializer (`Transform::new(ctx)`) that discovers it
+  once and stores it in the transform. Put prerequisites in `should_run`, including option gates and
+  whether required declarations were found.
+- Keep algorithmic complexity under control: generally avoid iterating over the whole crate or
+  a whole body too many times.
+
+## Testing
+
+- Every fix should ideally have a reproducer. The test suite is quite flexible, use it.
+- Changes to the generated output are to be double-checked: they can often indicate a bug.
+  Well-motivated changes are however totally fine.
+
+## OCaml vs Rust
+
+Charon is a hybrid codebase. A typical feature is mostly on the Rust side. However when the AST
+changes, this must be propagated. Use `make generate-ml` to regenerate the generated OCaml files.
+
+## Versioning
+
+Any change to the AST must come with a version bump to make the deserializers emit nice errors. Just
+bump the patch version in `Cargo.toml` then run `make test` at the root to propagate the changes.

charon/Cargo.toml

@@ -24,7 +24,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 
 [package]
 name = "charon"
-version = "0.1.197"
+version = "0.1.198"
 authors.workspace = true
 edition.workspace = true
 license.workspace = true

charon/rust-toolchain

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2026-02-07"
+channel = "nightly-2026-02-22"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-src", "miri" ]
 targets = [ "x86_64-unknown-linux-gnu", "x86_64-apple-darwin", "x86_64-pc-windows-msvc", "aarch64-apple-darwin", "i686-unknown-linux-gnu", "powerpc64-unknown-linux-gnu", "riscv64gc-unknown-none-elf" ]

charon/src/ast/builtins.rs

@@ -12,6 +12,15 @@ use crate::types::*;
 // We treat this one specially in the `inline_local_panic_functions` pass. See there for details.
 pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit"];
 
+pub static BOX_ASSUME_INIT_INTO_VEC_UNSAFE: &str = "box_assume_init_into_vec_unsafe";
+
+pub static BOX_WRITE: &str = "alloc::boxed::Box::write";
+
+// The translated Charon name contains an inherent impl path element where the Rust path contains
+// `Box`. `NamePattern` does not yet inspect inherent impl receiver types, so passes that match the
+// translated name need this wildcarded pattern.
+pub static BOX_WRITE_PATTERN: &str = "alloc::boxed::_::write";
+
 impl BuiltinTy {
     pub fn get_name(self) -> Name {
         let name: &[_] = match self {

charon/src/ast/expressions.rs

@@ -753,10 +753,6 @@ pub enum Rvalue {
     ///
     /// We translate this to a function call for LLBC.
     Repeat(Operand, Ty, Box<ConstantExpr>),
-    /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. This
-    /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original
-    /// `Box::new()` call, but sometimes may fail to do so, leaking the expression.
-    ShallowInitBox(Operand, Ty),
 }
 
 /// An aggregated ADT.

charon/src/ast/hash_cons.rs

@@ -77,7 +77,6 @@ mod intern_table {
         U: indexmap::Equivalent<Arc<T>>,
     {
         // Fast read-only check.
-        #[expect(irrefutable_let_patterns)] // https://github.com/rust-lang/rust/issues/139369
         let arc = if let read_guard = INTERNED.read().unwrap()
             && let Some(map) = read_guard.get::<T>()
             && let Some((arc, _id)) = map.get_key_value(&inner)

charon/src/ast/types_utils.rs

@@ -758,6 +758,10 @@ impl Ty {
         }
     }
 
+    pub fn as_adt_id(&self) -> Option<TypeDeclId> {
+        self.kind().as_adt().and_then(|a| a.id.as_adt().cloned())
+    }
+
     pub fn get_ptr_metadata(&self, translated: &TranslatedCrate) -> PtrMetadata {
         let ty_decls = &translated.type_decls;
         match self.kind() {

charon/src/ast/ullbc_ast_utils.rs

@@ -6,6 +6,33 @@ use crate::meta::Span;
 use crate::ullbc_ast::*;
 use std::collections::HashMap;
 use std::mem;
+use std::ops::{Index, IndexMut};
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct StmtLoc {
+    pub block: BlockId,
+    pub statement: usize,
+}
+
+impl StmtLoc {
+    pub fn new(block: BlockId, statement: usize) -> Self {
+        StmtLoc { block, statement }
+    }
+
+    pub fn block_start(block: BlockId) -> Self {
+        StmtLoc {
+            block,
+            statement: 0,
+        }
+    }
+
+    pub fn after(self) -> Self {
+        StmtLoc {
+            block: self.block,
+            statement: self.statement + 1,
+        }
+    }
+}
 
 impl SwitchTargets {
     pub fn targets(&self) -> SmallVec<[BlockId; 2]> {
@@ -118,6 +145,23 @@ impl Terminator {
             }
         }
     }
+
+    pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> {
+        match &self.kind {
+            TerminatorKind::Goto { target } => {
+                smallvec![*target]
+            }
+            TerminatorKind::Switch { targets, .. } => targets.targets(),
+            TerminatorKind::Call { target, .. }
+            | TerminatorKind::Drop { target, .. }
+            | TerminatorKind::Assert { target, .. } => {
+                smallvec![*target]
+            }
+            TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => {
+                smallvec![]
+            }
+        }
+    }
 }
 
 impl BlockData {
@@ -165,22 +209,8 @@ impl BlockData {
     pub fn targets(&self) -> SmallVec<[BlockId; 2]> {
         self.terminator.targets()
     }
-
     pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> {
-        match &self.terminator.kind {
-            TerminatorKind::Goto { target } => {
-                smallvec![*target]
-            }
-            TerminatorKind::Switch { targets, .. } => targets.targets(),
-            TerminatorKind::Call { target, .. }
-            | TerminatorKind::Drop { target, .. }
-            | TerminatorKind::Assert { target, .. } => {
-                smallvec![*target]
-            }
-            TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => {
-                smallvec![]
-            }
-        }
+        self.terminator.targets_ignoring_unwind()
     }
 
     /// Apply a transformer to all the statements.
@@ -304,6 +334,19 @@ impl ExprBody {
     }
 }
 
+impl Index<StmtLoc> for ExprBody {
+    type Output = Statement;
+    fn index(&self, loc: StmtLoc) -> &Self::Output {
+        &self.body[loc.block].statements[loc.statement]
+    }
+}
+
+impl IndexMut<StmtLoc> for ExprBody {
+    fn index_mut(&mut self, loc: StmtLoc) -> &mut Self::Output {
+        &mut self.body[loc.block].statements[loc.statement]
+    }
+}
+
 /// Helper to construct a small ullbc body.
 pub struct BodyBuilder {
     /// The span to use for everything.

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

@@ -11,7 +11,6 @@
 #![expect(incomplete_features)]
 #![feature(box_patterns)]
 #![feature(deref_patterns)]
-#![feature(if_let_guard)]
 #![feature(iter_array_chunks)]
 #![feature(iterator_try_collect)]
 #![feature(macro_metavar_expr)]