From 29b4b1a8f5b0df29c41d8b72f6b2ccac5129236e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 11 Nov 2025 10:58:55 +0000
Subject: [PATCH] Update charon submodule by 15 commits
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This increment advances the charon submodule from 0c4617c9 to 30cab882
(15 commits).

API Changes Required:

- TraitDecl.const_defaults: HashMap → IndexMap
- TraitDecl.type_defaults: HashMap → IndexMap

Progress: 15 of ~1008 commits (1.5%)
---
 Cargo.lock                                               | 3 ++-
 charon                                                   | 2 +-
 kani-compiler/Cargo.toml                                 | 1 +
 .../src/codegen_aeneas_llbc/compiler_interface.rs        | 1 -
 .../src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs          | 9 +++------
 scripts/charon-patch.diff                                | 2 +-
 6 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 786f6056a36..34aa59db806 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -248,7 +248,7 @@ checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
 
 [[package]]
 name = "charon"
-version = "0.1.65"
+version = "0.1.67"
 dependencies = [
  "annotate-snippets",
  "anstream",
@@ -940,6 +940,7 @@ dependencies = [
  "charon",
  "clap",
  "cprover_bindings",
+ "indexmap",
  "itertools 0.14.0",
  "kani_metadata",
  "lazy_static",
diff --git a/charon b/charon
index 0c4617c91b3..30cab882652 160000
--- a/charon
+++ b/charon
@@ -1 +1 @@
-Subproject commit 0c4617c91b30e7770a3d2ea3914e220a80d92257
+Subproject commit 30cab88265206f4fa849736e704983e39a404d96
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index ec22f80066f..9d6d0a3e066 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -12,6 +12,7 @@ publish = false
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 charon = { path = "../charon/charon", optional = true, default-features = false } 
 clap = { version = "4.4.11", features = ["derive", "cargo"] }
+indexmap = { version = "2.7.1", features = ["serde"] }
 itertools = "0.14"
 kani_metadata = { path = "../kani_metadata" }
 lazy_static = "1.5.0"
diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
index 6d6b8bebdeb..d146c5bfa97 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
@@ -40,7 +40,6 @@ use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 use std::any::Any;
-use std::cell::RefCell;
 use std::fs::File;
 use std::path::Path;
 use std::sync::{Arc, Mutex};
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
index a83bd58d6cc..22800b2e3b6 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -54,6 +54,7 @@ use charon_lib::ullbc_ast::{
 };
 use charon_lib::{error_assert, raise_error, register_error};
 use core::panic;
+use indexmap::IndexMap;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::{TyCtxt, TypingEnv};
 use rustc_public::mir::mono::{Instance, InstanceDef};
@@ -118,10 +119,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         self.errors.span_err(self.translated, span, msg)
     }
 
-    fn continue_on_failure(&self) -> bool {
-        self.errors.continue_on_failure()
-    }
-
     fn translate_traitdecl(&mut self, trait_def: TraitDef) -> CharonTraitDeclId {
         let trait_def_id = trait_def.def_id();
         let trait_decl_id = self.register_trait_decl_id(trait_def_id);
@@ -129,10 +126,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             None => {
                 let trait_decl = TraitDef::declaration(&trait_def);
                 let consts = Vec::new();
-                let const_defaults = HashMap::new();
+                let const_defaults = IndexMap::new();
                 let types = Vec::new();
                 let type_clauses = Vec::new();
-                let type_defaults = HashMap::new();
+                let type_defaults = IndexMap::new();
                 let required_methods = Vec::new();
                 let provided_methods = Vec::new();
                 let parent_clauses = CharonVector::new();
diff --git a/scripts/charon-patch.diff b/scripts/charon-patch.diff
index ec9120dcf28..7ea1d700a9b 100644
--- a/scripts/charon-patch.diff
+++ b/scripts/charon-patch.diff
@@ -4,7 +4,7 @@ index 20f8a9df..a1bf1ee6 100644
 +++ b/charon/Cargo.toml
 @@ -2,7 +2,7 @@
  name = "charon"
- version = "0.1.65"
+ version = "0.1.67"
  authors = ["Son Ho <hosonmarc@gmail.com>"]
 -edition = "2021"
 +edition = "2024"