Update charon submodule by 15 commits (model-checking#4464)

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%)

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

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",

charon

@@ -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"

kani-compiler/Cargo.toml

@@ -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};

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.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,21 +119,17 @@ 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);
         match self.translated.trait_decls.get(trait_decl_id) {
             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();

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -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 <[email protected]>"]
 -edition = "2021"
 +edition = "2024"