From e7f4152c33e27357f1b2d93d053284330cfeba88 Mon Sep 17 00:00:00 2001
From: NGUYEN <ntson@amazon.com>
Date: Fri, 15 Nov 2024 08:36:11 -0800
Subject: [PATCH 1/4] add support for enum, struct, tuple in mod.rs, add some
 tests

---
 Cargo.lock                                    |  12 +
 charon                                        |   2 +-
 .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs   | 863 ++++++++++++++----
 ...TestRNvCshcvyQEKZjUj4test4main.symtab.lean |  24 +
 tests/expected/llbc/basic0/expected           |   2 +-
 tests/expected/llbc/basic0/test.rs            |   2 +-
 ...TestRNvCshcvyQEKZjUj4test4main.symtab.lean |  25 +
 ...TestRNvCshcvyQEKZjUj4test4main.symtab.lean |  31 +
 tests/expected/llbc/enum_test/expected        |  36 +
 tests/expected/llbc/enum_test/test.rs         |  27 +
 tests/expected/llbc/projection_test/expected  |  49 +
 tests/expected/llbc/projection_test/test.rs   |  32 +
 ...TestRNvCshcvyQEKZjUj4test4main.symtab.lean |  29 +
 tests/expected/llbc/struct_test/expected      |  27 +
 tests/expected/llbc/struct_test/test.rs       |  20 +
 ...TestRNvCshcvyQEKZjUj4test4main.symtab.lean |  24 +
 tests/expected/llbc/tuple_test/expected       |  28 +
 tests/expected/llbc/tuple_test/test.rs        |  14 +
 tests/perf/s2n-quic                           |   2 +-
 19 files changed, 1076 insertions(+), 173 deletions(-)
 create mode 100644 tests/expected/llbc/basic0/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
 create mode 100644 tests/expected/llbc/basic1/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
 create mode 100644 tests/expected/llbc/enum_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
 create mode 100644 tests/expected/llbc/enum_test/expected
 create mode 100644 tests/expected/llbc/enum_test/test.rs
 create mode 100644 tests/expected/llbc/projection_test/expected
 create mode 100644 tests/expected/llbc/projection_test/test.rs
 create mode 100644 tests/expected/llbc/struct_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
 create mode 100644 tests/expected/llbc/struct_test/expected
 create mode 100644 tests/expected/llbc/struct_test/test.rs
 create mode 100644 tests/expected/llbc/tuple_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
 create mode 100644 tests/expected/llbc/tuple_test/expected
 create mode 100644 tests/expected/llbc/tuple_test/test.rs

diff --git a/Cargo.lock b/Cargo.lock
index a8436fe8dea2..1c1d3b6458e0 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -253,6 +253,7 @@ dependencies = [
  "clap",
  "colored",
  "convert_case 0.6.0",
+ "derivative",
  "derive-visitor",
  "env_logger",
  "hashlink",
@@ -496,6 +497,17 @@ dependencies = [
  "powerfmt",
 ]
 
+[[package]]
+name = "derivative"
+version = "2.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
 [[package]]
 name = "derive-visitor"
 version = "0.4.0"
diff --git a/charon b/charon
index 454078ebdb4a..2193aa00fd89 160000
--- a/charon
+++ b/charon
@@ -1 +1 @@
-Subproject commit 454078ebdb4a607e2b21dc115e1ca99b516e436f
+Subproject commit 2193aa00fd89e991226ada10d8a8f66e0594f212
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 35e4d137229d..0d006456ea8a 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
@@ -7,56 +7,75 @@
 //! unstructured low-level borrow calculus (ULLBC)
 
 use core::panic;
+use std::any::Any;
+//use std::ascii::Char;
 use std::path::PathBuf;
 
+use charon_lib::ast::AggregateKind as CharonAggregateKind;
 use charon_lib::ast::CastKind as CharonCastKind;
+use charon_lib::ast::FieldId as CharonFieldId;
 use charon_lib::ast::Place as CharonPlace;
 use charon_lib::ast::ProjectionElem as CharonProjectionElem;
 use charon_lib::ast::Rvalue as CharonRvalue;
 use charon_lib::ast::Span as CharonSpan;
-use charon_lib::ast::meta::{AttrInfo, Loc, RawSpan};
+use charon_lib::ast::meta::{AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan};
 use charon_lib::ast::types::Ty as CharonTy;
+use charon_lib::ast::types::TypeDeclId as CharonTypeDeclId;
 use charon_lib::ast::types::TyKind as CharonTyKind;
-use charon_lib::ast::{AbortKind, Body as CharonBody, Var, VarId};
+use charon_lib::ast::TypeDecl as CharonTypeDecl;
+use charon_lib::ast::TypeDeclKind as CharonTypeDeclKind;
+use charon_lib::ast::Variant as CharonVariant;
+use charon_lib::ast::Field as CharonField;
+use charon_lib::ast::{AbortKind as CharonAbortKind, Body as CharonBody, Var as CharonVar, VarId as CharonVarId};
 use charon_lib::ast::{
-    AnyTransId, Assert, BodyId, BuiltinTy, Disambiguator, FileName, FunDecl, FunSig, GenericArgs,
-    GenericParams, IntegerTy, ItemKind, ItemMeta, ItemOpacity, Literal, LiteralTy, Name, Opaque,
-    PathElem, RawConstantExpr, RefKind, Region as CharonRegion, ScalarValue, TranslatedCrate,
-    TypeId,
+    AnyTransId as CharonAnyTransId, Assert as CharonAssert, BodyId as CharonBodyId, BuiltinTy as CharonBuiltinTy, 
+    Disambiguator as CharonDisambiguator, FileName as CharonFileName, FunDecl as CharonFunDecl, FunSig as CharonFunSig, GenericArgs as CharonGenericArgs,
+    GenericParams as CharonGenericParams, IntegerTy as CharonIntegerTy, 
+    ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, 
+    Literal as CharonLiteral, LiteralTy as CharonLiteralTy, Name as CharonName, Opaque as CharonOpaque,
+    PathElem as CharonPathElem, RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, ScalarValue as CharonScalarValue, 
+    TranslatedCrate as CharonTranslatedCrate, TypeId as CharonTypeId, RegionId as CharonRegionId, TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, ConstGeneric as CharonConstGeneric,
+    ConstGenericVarId as CharonConstGenericVarId, FieldProjKind as CharonFieldProjKind,
 };
 use charon_lib::ast::{
-    BinOp as CharonBinOp, Call, FnOperand, FnPtr, FunDeclId, FunId, FunIdOrTraitMethodRef,
-    VariantId,
+    BinOp as CharonBinOp, Call as CharonCall, FnOperand as CharonFnOperand, FnPtr as CharonFnPtr, 
+    FunDeclId as CharonFunDeclId, FunId as CharonFunId, FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, VariantId as CharonVariantId,
 };
 use charon_lib::ast::{
-    BorrowKind as CharonBorrowKind, ConstantExpr, Operand as CharonOperand, UnOp,
+    BorrowKind as CharonBorrowKind, ConstantExpr as CharonConstantExpr, Operand as CharonOperand, 
 };
-use charon_lib::errors::Error;
-use charon_lib::errors::ErrorCtx;
-use charon_lib::ids::Vector;
+use charon_lib::errors::Error as CharonError;
+use charon_lib::errors::ErrorCtx as CharonErrorCtx;
+use charon_lib::ids::Vector as CharonVector;
 use charon_lib::ullbc_ast::{
-    BlockData, BlockId, BodyContents, ExprBody, RawStatement, RawTerminator,
-    Statement as CharonStatement, SwitchTargets as CharonSwitchTargets,
+    BlockData as CharonBlockData, BlockId as CharonBlockId, BodyContents as CharonBodyContents, ExprBody as CharonExprBody, 
+    RawStatement as CharonRawStatement, RawTerminator as CharonRawTerminator, Statement as CharonStatement, SwitchTargets as CharonSwitchTargets,
     Terminator as CharonTerminator,
 };
 use charon_lib::{error_assert, error_or_panic};
 use rustc_data_structures::fx::FxHashMap;
+use rustc_data_structures::stable_hasher::HashStable;
+use rustc_middle::ty::AdtKind as MirAdtKind;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
+use stable_mir::ty::AdtDef;
+use stable_mir::ty::AdtKind;
 use stable_mir::abi::PassMode;
+use stable_mir::mir::AggregateKind;
 use stable_mir::mir::VarDebugInfoContents;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::mono::InstanceDef;
 use stable_mir::mir::{
-    BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability, Operand, Place,
+    BasicBlock, BinOp, UnOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability, Operand, Place,
     ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
 };
 use stable_mir::ty::{
     Allocation, ConstantKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span, Ty,
-    TyKind, UintTy,
+    TyKind, UintTy, TyConst, TyConstId, TraitDef, TyConstKind
 };
-
+use stable_mir::ty::{GenericArgs, GenericArgKind};
 use stable_mir::{CrateDef, DefId};
+use syn::token::Default;
 use tracing::{debug, trace};
 
 /// A context for translating a single MIR function to ULLBC.
@@ -64,9 +83,9 @@ use tracing::{debug, trace};
 pub struct Context<'a, 'tcx> {
     tcx: TyCtxt<'tcx>,
     instance: Instance,
-    translated: &'a mut TranslatedCrate,
-    id_map: &'a mut FxHashMap<DefId, AnyTransId>,
-    errors: &'a mut ErrorCtx<'tcx>,
+    translated: &'a mut CharonTranslatedCrate,
+    id_map: &'a mut FxHashMap<DefId, CharonAnyTransId>,
+    errors: &'a mut CharonErrorCtx<'tcx>,
     local_names: FxHashMap<Local, String>,
 }
 
@@ -76,9 +95,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     pub fn new(
         tcx: TyCtxt<'tcx>,
         instance: Instance,
-        translated: &'a mut TranslatedCrate,
-        id_map: &'a mut FxHashMap<DefId, AnyTransId>,
-        errors: &'a mut ErrorCtx<'tcx>,
+        translated: &'a mut CharonTranslatedCrate,
+        id_map: &'a mut FxHashMap<DefId, CharonAnyTransId>,
+        errors: &'a mut CharonErrorCtx<'tcx>,
     ) -> Self {
         let mut local_names = FxHashMap::default();
         // populate names of locals
@@ -128,21 +147,21 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         };
 
         let fun_decl =
-            FunDecl { def_id: fid, item_meta, signature, kind: ItemKind::Regular, body: Ok(body) };
+            CharonFunDecl { def_id: fid, item_meta, signature, kind: CharonItemKind::Regular, body: Ok(body) };
 
         self.translated.fun_decls.set_slot(fid, fun_decl);
 
         Ok(())
     }
 
-    /// Get or create a `FunDeclId` for the given function
-    fn register_fun_decl_id(&mut self, def_id: DefId) -> FunDeclId {
+    /// Get or create a `CharonFunDeclId` for the given function
+    fn register_fun_decl_id(&mut self, def_id: DefId) -> CharonFunDeclId {
         debug!("register_fun_decl_id: {:?}", def_id);
         let tid = match self.id_map.get(&def_id) {
             Some(tid) => *tid,
             None => {
                 debug!("***Not found!");
-                let tid = AnyTransId::Fun(self.translated.fun_decls.reserve_slot());
+                let tid = CharonAnyTransId::Fun(self.translated.fun_decls.reserve_slot());
                 self.id_map.insert(def_id, tid);
                 self.translated.all_ids.insert(tid);
                 tid
@@ -152,15 +171,154 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         tid.try_into().unwrap()
     }
 
+    fn find_fun_decl_id(&self, def_id: DefId) -> CharonFunDeclId {
+        debug!("register_fun_decl_id: {:?}", def_id);
+        let tid = *self.id_map.get(&def_id).unwrap(); 
+        debug!("register_fun_decl_id: {:?}", self.id_map);
+        tid.try_into().unwrap()
+    }
+
+    fn register_type_decl_id(&mut self, def_id: DefId) -> CharonTypeDeclId {
+        debug!("register_type_decl_id: {:?}", def_id);
+        let tid = match self.id_map.get(&def_id) {
+            Some(tid) => *tid,
+            None => {
+                debug!("***Not found!");
+                let tid = CharonAnyTransId::Type(self.translated.type_decls.reserve_slot());
+                self.id_map.insert(def_id, tid);
+                self.translated.all_ids.insert(tid);
+                tid
+            }
+        };
+        debug!("register_type_decl_id: {:?}", self.id_map);
+        tid.try_into().unwrap()
+    }    
+
+    fn find_type_decl_id(&self, def_id: DefId) -> CharonTypeDeclId {
+        debug!("register_type_decl_id: {:?}", def_id);
+        let tid = *self.id_map.get(&def_id).unwrap(); 
+        debug!("register_type_decl_id: {:?}", self.id_map);
+        tid.try_into().unwrap()
+    }
+
+    fn get_discriminant(&mut self, discr_val: u128, ty: Ty) -> CharonScalarValue {
+        let ty = self.translate_ty(ty);
+        let int_ty = *ty.kind().as_literal().unwrap().as_integer().unwrap();
+        CharonScalarValue::from_bits(int_ty, discr_val)
+    }
+
+
+    fn translate_adtdef(&mut self, adt_def: AdtDef) -> CharonTypeDeclId {
+        match adt_def.kind() {
+            AdtKind::Enum => {
+                let def_id  = adt_def.def_id();
+                let c_typedeclid = self.register_type_decl_id(def_id);
+                let mut c_variants: CharonVector<CharonVariantId, CharonVariant> = CharonVector::new();
+                for var_def in adt_def.variants_iter(){
+                    let mut c_fields: CharonVector<CharonFieldId, CharonField> = CharonVector::new();
+                    for field_def in var_def.fields(){
+                        let c_field_ty = self.translate_ty(field_def.ty());
+                        let c_field_name = Some(field_def.name);
+                        let c_span = self.translate_span(adt_def.span());
+                        let c_field = CharonField {
+                            span : c_span,
+                            attr_info : CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true },
+                            name: c_field_name,
+                            ty: c_field_ty,
+                        };
+                        c_fields.push(c_field);
+                    }
+                    let var_name = var_def.name();
+                    let span = self.translate_span(adt_def.span()); 
+
+                    let adtdef_internal = rustc_internal::internal(self.tcx, adt_def);
+                    let variant_index_internal = rustc_internal::internal(self.tcx, var_def.idx);
+                    let discr = adtdef_internal.discriminant_for_variant(self.tcx, variant_index_internal);
+                    let discr_val = discr.val;
+                    let discr_ty = rustc_internal::stable(discr.ty);
+                    let c_discr = self.get_discriminant(discr_val, discr_ty);
+
+                    let c_variant = CharonVariant{
+                        span : span,
+                        attr_info : CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true },
+                        name : var_name,
+                        fields : c_fields,
+                        discriminant : c_discr,
+                    };
+                    let c_varidx = c_variants.push(c_variant);
+                    assert_eq!(c_varidx.index(), var_def.idx.to_index());
+                }                        
+                let item_meta = self.translate_item_meta_adt(adt_def).unwrap();
+                let typedecl = CharonTypeDecl {
+                    def_id: c_typedeclid,
+                    generics: CharonGenericParams::empty(),
+                    kind: CharonTypeDeclKind::Enum(c_variants),
+                    item_meta : item_meta,
+                };
+                self.translated.type_decls.set_slot(c_typedeclid, typedecl);
+                c_typedeclid
+            }
+            AdtKind::Struct => {
+                let def_id  = adt_def.def_id();
+                let c_typedeclid = self.register_type_decl_id(def_id);
+                let mut c_fields: CharonVector<CharonFieldId, CharonField> = CharonVector::new();
+                let only_variant = *adt_def.variants().first().unwrap();
+                let fields = only_variant.fields();
+                for field_def in fields{
+                    let c_field_ty = self.translate_ty(field_def.ty());
+                    let c_field_name = Some(field_def.name);
+                    let c_span = self.translate_span(adt_def.span());
+                    let c_field = CharonField {
+                        span : c_span,
+                        attr_info : CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true },
+                        name: c_field_name,
+                        ty: c_field_ty,
+                    };
+                    c_fields.push(c_field);
+                }
+                let item_meta = self.translate_item_meta_adt(adt_def).unwrap();
+                let typedecl = CharonTypeDecl {
+                    def_id: c_typedeclid,
+                    generics: CharonGenericParams::empty(),
+                    kind: CharonTypeDeclKind::Struct(c_fields),
+                    item_meta : item_meta,
+                };
+                self.translated.type_decls.set_slot(c_typedeclid, typedecl);
+                c_typedeclid
+            }
+            _ => todo!(),             
+        }
+    }
+
     /// Compute the meta information for a Rust item identified by its id.
-    fn translate_item_meta_from_rid(&mut self, instance: Instance) -> Result<ItemMeta, Error> {
+    fn translate_item_meta_from_rid(&mut self, instance: Instance) -> Result<CharonItemMeta, CharonError> {
         let span = self.translate_instance_span(instance);
         let name = self.def_to_name(instance.def)?;
         // TODO: populate the source text
         let source_text = None;
         // TODO: populate the attribute info
         let attr_info =
-            AttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true };
+            CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true };
+
+        // Aeneas only translates items that are local to the top-level crate
+        // Since we want all reachable items (including those in external
+        // crates) to be translated, always set `is_local` to true
+        let is_local = true;
+
+        // For now, assume all items are transparent
+        let opacity = CharonItemOpacity::Transparent;
+
+        Ok(CharonItemMeta { span, source_text, attr_info, name, is_local, opacity })
+    }
+
+    fn translate_item_meta_adt(&mut self, adt: AdtDef) -> Result<CharonItemMeta, CharonError> {
+        let span = self.translate_span(adt.span());
+        let name = self.adtdef_to_name(adt)?;
+        // TODO: populate the source text
+        let source_text = None;
+        // TODO: populate the attribute info
+        let attr_info =
+            CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true };
 
         // Aeneas only translates items that are local to the top-level crate
         // Since we want all reachable items (including those in external
@@ -168,15 +326,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let is_local = true;
 
         // For now, assume all items are transparent
-        let opacity = ItemOpacity::Transparent;
+        let opacity = CharonItemOpacity::Transparent;
 
-        Ok(ItemMeta { span, source_text, attr_info, name, is_local, opacity })
+        Ok(CharonItemMeta { span, source_text, attr_info, name, is_local, opacity })
     }
 
+
     /// Retrieve an item name from a [DefId].
     /// This function is adapted from Charon:
     /// https://github.com/AeneasVerif/charon/blob/53530427db2941ce784201e64086766504bc5642/charon/src/bin/charon-driver/translate/translate_ctx.rs#L344
-    fn def_to_name(&mut self, def: InstanceDef) -> Result<Name, Error> {
+    fn def_to_name(&mut self, def: InstanceDef) -> Result<CharonName, CharonError> {
         let def_id = def.def_id();
         trace!("{:?}", def_id);
         let tcx = self.tcx();
@@ -231,10 +390,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         // ```
         //
         // The names we will generate for `foo` and `bar` are:
-        // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(0), Ident("foo")]`
-        // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(1), Ident("bar")]`
+        // `[Ident("test"), Ident("bla"), Ident("Foo"), CharonDisambiguator(0), Ident("foo")]`
+        // `[Ident("test"), Ident("bla"), Ident("Foo"), CharonDisambiguator(1), Ident("bar")]`
         let mut found_crate_name = false;
-        let mut name: Vec<PathElem> = Vec::new();
+        let mut name: Vec<CharonPathElem> = Vec::new();
 
         let def_path = tcx.def_path(def_id);
         let crate_name = tcx.crate_name(def_path.krate).to_string();
@@ -256,17 +415,17 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         for cur_id in parents {
             let data = tcx.def_key(cur_id).disambiguated_data;
             // Match over the key data
-            let disambiguator = Disambiguator::new(data.disambiguator as usize);
+            let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
             use rustc_hir::definitions::DefPathData;
             match &data.data {
                 DefPathData::TypeNs(symbol) => {
                     error_assert!(self, span, data.disambiguator == 0); // Sanity check
-                    name.push(PathElem::Ident(symbol.to_string(), disambiguator));
+                    name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }
                 DefPathData::ValueNs(symbol) => {
                     // I think `disambiguator != 0` only with names introduced by macros (though
                     // not sure).
-                    name.push(PathElem::Ident(symbol.to_string(), disambiguator));
+                    name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }
                 DefPathData::CrateRoot => {
                     // Sanity check
@@ -275,7 +434,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     // This should be the beginning of the path
                     error_assert!(self, span, name.is_empty());
                     found_crate_name = true;
-                    name.push(PathElem::Ident(crate_name.clone(), disambiguator));
+                    name.push(CharonPathElem::Ident(crate_name.clone(), disambiguator));
                 }
                 DefPathData::Impl => todo!(),
                 DefPathData::OpaqueTy => {
@@ -289,13 +448,13 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     // of an issue here, because for now we don't expose macros
                     // in the AST, and only use macro names in [register], for
                     // instance to filter opaque modules.
-                    name.push(PathElem::Ident(symbol.to_string(), disambiguator));
+                    name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }
                 DefPathData::Closure => {
                     // TODO: this is not very satisfactory, but on the other hand
                     // we should be able to extract closures in local let-bindings
                     // (i.e., we shouldn't have to introduce top-level let-bindings).
-                    name.push(PathElem::Ident("closure".to_string(), disambiguator))
+                    name.push(CharonPathElem::Ident("closure".to_string(), disambiguator))
                 }
                 DefPathData::ForeignMod => {
                     // Do nothing, functions in `extern` blocks are in the same namespace as the
@@ -309,13 +468,103 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
 
         // We always add the crate name
         if !found_crate_name {
-            name.push(PathElem::Ident(crate_name, Disambiguator::new(0)));
+            name.push(CharonPathElem::Ident(crate_name, CharonDisambiguator::new(0)));
         }
 
         trace!("{:?}", name);
-        Ok(Name { name })
+        Ok(CharonName { name })
     }
 
+    fn adtdef_to_name(&mut self, def: AdtDef) -> Result<CharonName, CharonError> {
+        let def_id = def.def_id();
+        trace!("{:?}", def_id);
+        let tcx = self.tcx();
+        let span: CharonSpan = self.translate_span(def.span());
+        let def_id = rustc_internal::internal(self.tcx(), def_id);
+        let mut found_crate_name = false;
+        let mut name: Vec<CharonPathElem> = Vec::new();
+
+        let def_path = tcx.def_path(def_id);
+        let crate_name = tcx.crate_name(def_path.krate).to_string();
+
+        let parents: Vec<_> = {
+            let mut parents = vec![def_id];
+            let mut cur_id = def_id;
+            while let Some(parent) = tcx.opt_parent(cur_id) {
+                parents.push(parent);
+                cur_id = parent;
+            }
+            parents.into_iter().rev().collect()
+        };
+
+        // Rk.: below we try to be as tight as possible with regards to sanity
+        // checks, to make sure we understand what happens with def paths, and
+        // fail whenever we get something which is even slightly outside what
+        // we expect.
+        for cur_id in parents {
+            let data = tcx.def_key(cur_id).disambiguated_data;
+            // Match over the key data
+            let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
+            use rustc_hir::definitions::DefPathData;
+            match &data.data {
+                DefPathData::TypeNs(symbol) => {
+                    error_assert!(self, span, data.disambiguator == 0); // Sanity check
+                    name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
+                }
+                DefPathData::ValueNs(symbol) => {
+                    // I think `disambiguator != 0` only with names introduced by macros (though
+                    // not sure).
+                    name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
+                }
+                DefPathData::CrateRoot => {
+                    // Sanity check
+                    error_assert!(self, span, data.disambiguator == 0);
+
+                    // This should be the beginning of the path
+                    error_assert!(self, span, name.is_empty());
+                    found_crate_name = true;
+                    name.push(CharonPathElem::Ident(crate_name.clone(), disambiguator));
+                }
+                DefPathData::Impl => todo!(),
+                DefPathData::OpaqueTy => {
+                    // TODO: do nothing for now
+                }
+                DefPathData::MacroNs(symbol) => {
+                    error_assert!(self, span, data.disambiguator == 0); // Sanity check
+
+                    // There may be namespace collisions between, say, function
+                    // names and macros (not sure). However, this isn't much
+                    // of an issue here, because for now we don't expose macros
+                    // in the AST, and only use macro names in [register], for
+                    // instance to filter opaque modules.
+                    name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
+                }
+                DefPathData::Closure => {
+                    // TODO: this is not very satisfactory, but on the other hand
+                    // we should be able to extract closures in local let-bindings
+                    // (i.e., we shouldn't have to introduce top-level let-bindings).
+                    name.push(CharonPathElem::Ident("closure".to_string(), disambiguator))
+                }
+                DefPathData::ForeignMod => {
+                    // Do nothing, functions in `extern` blocks are in the same namespace as the
+                    // block.
+                }
+                _ => {
+                    error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
+                }
+            }
+        }
+
+        // We always add the crate name
+        if !found_crate_name {
+            name.push(CharonPathElem::Ident(crate_name, CharonDisambiguator::new(0)));
+        }
+
+        trace!("{:?}", name);
+        Ok(CharonName { name })
+    }
+
+
     /// Compute the span information for the given instance
     fn translate_instance_span(&mut self, instance: Instance) -> CharonSpan {
         self.translate_span(instance.def.span())
@@ -323,7 +572,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
 
     /// Compute the span information for MIR span
     fn translate_span(&mut self, span: Span) -> CharonSpan {
-        let filename = FileName::Local(PathBuf::from(span.get_filename()));
+        let filename = CharonFileName::Local(PathBuf::from(span.get_filename()));
         let file_id = match self.translated.file_to_id.get(&filename) {
             Some(file_id) => *file_id,
             None => {
@@ -333,17 +582,32 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             }
         };
         let lineinfo = span.get_lines();
-        let rspan = RawSpan {
+        let rspan = CharonRawSpan {
+            file_id,
+            beg: CharonLoc { line: lineinfo.start_line, col: lineinfo.start_col },
+            end: CharonLoc { line: lineinfo.end_line, col: lineinfo.end_col },
+        };
+
+        // TODO: populate `generated_from_span` info
+        CharonSpan { span: rspan, generated_from_span: None }
+    }
+
+    fn translate_span_immut(&self, span: Span) -> CharonSpan {
+        let filename = CharonFileName::Local(PathBuf::from(span.get_filename()));
+        let file_id = *self.translated.file_to_id.get(&filename).unwrap();
+        let lineinfo = span.get_lines();
+        let rspan = CharonRawSpan {
             file_id,
-            beg: Loc { line: lineinfo.start_line, col: lineinfo.start_col },
-            end: Loc { line: lineinfo.end_line, col: lineinfo.end_col },
+            beg: CharonLoc { line: lineinfo.start_line, col: lineinfo.start_col },
+            end: CharonLoc { line: lineinfo.end_line, col: lineinfo.end_col },
         };
 
         // TODO: populate `generated_from_span` info
         CharonSpan { span: rspan, generated_from_span: None }
     }
+        
 
-    fn translate_function_signature(&mut self) -> FunSig {
+    fn translate_function_signature(&mut self) -> CharonFunSig {
         let instance = self.instance;
         let fn_abi = instance.fn_abi().unwrap();
         let requires_caller_location = self.requires_caller_location(instance);
@@ -373,18 +637,18 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let ret_type = self.translate_ty(fn_abi.ret.ty);
 
         // TODO: populate the rest of the information (`is_unsafe`, `is_closure`, etc.)
-        FunSig {
+        CharonFunSig {
             is_unsafe: false,
             is_closure: false,
             closure_info: None,
-            generics: GenericParams::default(),
+            generics: CharonGenericParams::default(),
             parent_params_info: None,
             inputs: args,
             output: ret_type,
         }
     }
 
-    fn translate_function_body(&mut self) -> Result<BodyId, Opaque> {
+    fn translate_function_body(&mut self) -> Result<CharonBodyId, CharonOpaque> {
         let instance = self.instance;
         let mir_body = instance.body().unwrap();
         let body_id = self.translated.bodies.reserve_slot();
@@ -397,10 +661,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let span = self.translate_span(mir_body.span);
         let arg_count = self.instance.fn_abi().unwrap().args.len();
         let locals = self.translate_body_locals(&mir_body);
-        let body: BodyContents =
+        let body: CharonBodyContents =
             mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect();
 
-        let body_expr = ExprBody { span, arg_count, locals, body, comments: Vec::new() };
+        let body_expr = CharonExprBody { span, arg_count, locals, body, comments: Vec::new() };
         CharonBody::Unstructured(body_expr)
     }
 
@@ -409,54 +673,148 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         instance_internal.def.requires_caller_location(self.tcx())
     }
 
-    fn translate_ty(&self, ty: Ty) -> CharonTy {
+/* 
+    fn generic_args_to_generic_params (&self, ga: GenericArgs) -> CharonGenericParams{
+        let genvec = ga.0;
+        let mut c_regions: CharonVector<CharonRegionId, CharonRegion> = CharonVector::new();
+        let mut c_types: CharonVector<CharonTypeVarId, CharonTy> = CharonVector::new();
+        let mut c_const_generics: CharonVector<CharonConstGenericVarId, CharonConstGeneric> =CharonVector::new();
+        //let mut  trait_refs: CharonVector<CharonTraitClauseId, CharonTraitRef> = CharonVector::new();
+        for genkind in genvec.iter(){
+            match *genkind{
+                GenericArgKind::Lifetime(region) => {
+                    let c_region = self.translate_region(region);
+                    c_regions.push(c_region);
+                }
+                GenericArgKind::Type(ty) => {
+                    let c_ty = self.translate_ty(ty);
+                    c_types.push(c_ty);
+                }
+                GenericArgKind::Const(tc ) => {
+                    let c_const_generic = self.tyconst_to_constgeneric(tc); 
+                    c_const_generics.push(c_const_generic);
+                }
+            }
+        }
+        CharonGenericParams{
+            regions : c_regions,
+            types : c_types,
+            const_generics : c_const_generics,
+            trait_clauses : CharonVector::new(),
+            regions_outlive : Vec::new(),
+            types_outlive : Vec::new(),
+            trait_type_constraints : Vec::new(),
+        }
+        }
+*/ 
+        
+    fn translate_generic_args (&mut self, ga: GenericArgs) -> CharonGenericArgs{
+            let genvec = ga.0;
+            let mut c_regions: CharonVector<CharonRegionId, CharonRegion> = CharonVector::new();
+            let mut c_types: CharonVector<CharonTypeVarId, CharonTy> = CharonVector::new();
+            let mut c_const_generics: CharonVector<CharonConstGenericVarId, CharonConstGeneric> =CharonVector::new();
+            //let mut  trait_refs: CharonVector<CharonTraitClauseId, CharonTraitRef> = CharonVector::new();
+            for genkind in genvec.iter(){
+                let gk = genkind.clone();
+                match gk{
+                    GenericArgKind::Lifetime(region) => {
+                        let c_region = self.translate_region(region);
+                        c_regions.push(c_region);
+                    },
+                    GenericArgKind::Type(ty) => {
+                        let c_ty = self.translate_ty(ty);
+                        c_types.push(c_ty);
+                    },
+                    GenericArgKind::Const(tc ) => {
+                        let c_const_generic = self.tyconst_to_constgeneric(tc); 
+                        c_const_generics.push(c_const_generic);
+                    }
+                }
+            }
+            CharonGenericArgs{
+                regions : c_regions,
+                types : c_types,
+                const_generics : c_const_generics,
+                trait_refs : CharonVector::new(),
+            }
+        }
+
+    fn translate_ty(&mut self, ty: Ty) -> CharonTy {
         match ty.kind() {
             TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty),
             _ => todo!(),
         }
     }
 
-    fn translate_rigid_ty(&self, rigid_ty: RigidTy) -> CharonTy {
+    fn tyconst_to_constgeneric(&self, tyconst: TyConst) -> CharonConstGeneric {
+        match tyconst.kind() {
+            TyConstKind::Value(ty, alloc) => {
+                let c_raw_constexpr = self.translate_allocation(alloc, *ty);
+                let c_const_generic = translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap();
+                c_const_generic
+            }
+            _ => todo!(),
+        }
+    }
+
+    fn translate_rigid_ty(&mut self, rigid_ty: RigidTy) -> CharonTy {
         debug!("translate_rigid_ty: {rigid_ty:?}");
         match rigid_ty {
-            RigidTy::Bool => CharonTy::new(CharonTyKind::Literal(LiteralTy::Bool)),
-            RigidTy::Char => CharonTy::new(CharonTyKind::Literal(LiteralTy::Char)),
+            RigidTy::Bool => CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Bool)),
+            RigidTy::Char => CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Char)),
             RigidTy::Int(it) => {
-                CharonTy::new(CharonTyKind::Literal(LiteralTy::Integer(translate_int_ty(it))))
+                CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Integer(translate_int_ty(it))))
             }
             RigidTy::Uint(uit) => {
-                CharonTy::new(CharonTyKind::Literal(LiteralTy::Integer(translate_uint_ty(uit))))
+                CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Integer(translate_uint_ty(uit))))
             }
             RigidTy::Never => CharonTy::new(CharonTyKind::Never),
             RigidTy::Str => CharonTy::new(CharonTyKind::Adt(
-                TypeId::Builtin(BuiltinTy::Str),
+                CharonTypeId::Builtin(CharonBuiltinTy::Str),
                 // TODO: find out whether any of the information below should be
                 // populated for strings
-                GenericArgs {
-                    regions: Vector::new(),
-                    types: Vector::new(),
-                    const_generics: Vector::new(),
-                    trait_refs: Vector::new(),
+                CharonGenericArgs {
+                    regions: CharonVector::new(),
+                    types: CharonVector::new(),
+                    const_generics: CharonVector::new(),
+                    trait_refs: CharonVector::new(),
                 },
             )),
+            RigidTy::Array(ty, tyconst) => {
+                let c_ty = self.translate_ty(ty);
+                let c_const_generic = self.tyconst_to_constgeneric(tyconst);
+                let mut c_types = CharonVector::new();
+                let mut c_const_generics = CharonVector::new();
+                c_types.push(c_ty);
+                c_const_generics.push(c_const_generic);
+                CharonTy::new(CharonTyKind::Adt(
+                    CharonTypeId::Builtin(CharonBuiltinTy::Array),
+                    CharonGenericArgs {
+                        regions: CharonVector::new(),
+                        types: c_types,
+                        const_generics: c_const_generics,
+                        trait_refs: CharonVector::new(),
+                    }
+                ))
+            }
             RigidTy::Ref(region, ty, mutability) => CharonTy::new(CharonTyKind::Ref(
                 self.translate_region(region),
                 self.translate_ty(ty),
                 match mutability {
-                    Mutability::Mut => RefKind::Mut,
-                    Mutability::Not => RefKind::Shared,
+                    Mutability::Mut => CharonRefKind::Mut,
+                    Mutability::Not => CharonRefKind::Shared,
                 },
             )),
             RigidTy::Tuple(ty) => {
                 let types = ty.iter().map(|ty| self.translate_ty(*ty)).collect();
                 // TODO: find out if any of the information below is needed
-                let generic_args = GenericArgs {
-                    regions: Vector::new(),
+                let generic_args = CharonGenericArgs {
+                    regions: CharonVector::new(),
                     types,
-                    const_generics: Vector::new(),
-                    trait_refs: Vector::new(),
+                    const_generics: CharonVector::new(),
+                    trait_refs: CharonVector::new(),
                 };
-                CharonTy::new(CharonTyKind::Adt(TypeId::Tuple, generic_args))
+                CharonTy::new(CharonTyKind::Adt(CharonTypeId::Tuple, generic_args))
             }
             RigidTy::FnDef(def_id, args) => {
                 if !args.0.is_empty() {
@@ -466,51 +824,60 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect();
                 let output = self.translate_ty(sig.output());
                 // TODO: populate regions?
-                CharonTy::new(CharonTyKind::Arrow(Vector::new(), inputs, output))
+                CharonTy::new(CharonTyKind::Arrow(CharonVector::new(), inputs, output))
             }
+            RigidTy::Adt(adt_def, genarg ) => {
+                let def_id  = adt_def.def_id();
+                let c_typedeclid = self.register_type_decl_id(def_id);
+                if self.translated.type_decls.get(c_typedeclid).is_none() {
+                    self.translate_adtdef(adt_def);
+                }
+                let c_generic_args = self.translate_generic_args(genarg);
+                CharonTy::new(CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), c_generic_args))
+                },
             _ => todo!(),
         }
     }
 
-    fn translate_body_locals(&mut self, mir_body: &Body) -> Vector<VarId, Var> {
+    fn translate_body_locals(&mut self, mir_body: &Body) -> CharonVector<CharonVarId, CharonVar> {
         // Charon expects the locals in the following order:
         // - the local used for the return value (index 0)
         // - the input arguments
         // - the remaining locals, used for the intermediate computations
-        let mut locals = Vector::new();
+        let mut locals = CharonVector::new();
         mir_body.local_decls().for_each(|(local, local_decl)| {
             let ty = self.translate_ty(local_decl.ty);
             let name = self.local_names.get(&local);
-            locals.push_with(|index| Var { index, name: name.cloned(), ty });
+            locals.push_with(|index| CharonVar { index, name: name.cloned(), ty });
         });
         locals
     }
 
-    fn translate_block(&mut self, bb: &BasicBlock) -> BlockData {
+    fn translate_block(&mut self, bb: &BasicBlock) -> CharonBlockData {
         let mut statements: Vec<CharonStatement> =
             bb.statements.iter().filter_map(|stmt| self.translate_statement(stmt)).collect();
         let (statement, terminator) = self.translate_terminator(&bb.terminator);
         if let Some(statement) = statement {
             statements.push(statement);
         }
-        BlockData { statements, terminator }
+        CharonBlockData { statements, terminator }
     }
 
     fn translate_statement(&mut self, stmt: &Statement) -> Option<CharonStatement> {
         let content = match &stmt.kind {
-            StatementKind::Assign(place, rhs) => Some(RawStatement::Assign(
+            StatementKind::Assign(place, rhs) => Some(CharonRawStatement::Assign(
                 self.translate_place(&place),
                 self.translate_rvalue(&rhs),
             )),
             StatementKind::SetDiscriminant { place, variant_index } => {
-                Some(RawStatement::SetDiscriminant(
+                Some(CharonRawStatement::SetDiscriminant(
                     self.translate_place(&place),
-                    VariantId::from_usize(variant_index.to_index()),
+                    CharonVariantId::from_usize(variant_index.to_index()),
                 ))
             }
             StatementKind::StorageLive(_) => None,
             StatementKind::StorageDead(local) => {
-                Some(RawStatement::StorageDead(VarId::from_usize(*local)))
+                Some(CharonRawStatement::StorageDead(CharonVarId::from_usize(*local)))
             }
             StatementKind::Nop => None,
             _ => todo!(),
@@ -528,21 +895,21 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     ) -> (Option<CharonStatement>, CharonTerminator) {
         let span = self.translate_span(terminator.span);
         let (statement, terminator) = match &terminator.kind {
-            TerminatorKind::Return => (None, RawTerminator::Return),
+            TerminatorKind::Return => (None, CharonRawTerminator::Return),
             TerminatorKind::Goto { target } => {
-                (None, RawTerminator::Goto { target: BlockId::from_usize(*target) })
+                (None, CharonRawTerminator::Goto { target: CharonBlockId::from_usize(*target) })
             }
             TerminatorKind::Unreachable => {
-                (None, RawTerminator::Abort(AbortKind::UndefinedBehavior))
+                (None, CharonRawTerminator::Abort(CharonAbortKind::UndefinedBehavior))
             }
             TerminatorKind::Drop { place, target, .. } => {
-                (Some(RawStatement::Drop(self.translate_place(&place))), RawTerminator::Goto {
-                    target: BlockId::from_usize(*target),
+                (Some(CharonRawStatement::Drop(self.translate_place(&place))), CharonRawTerminator::Goto {
+                    target: CharonBlockId::from_usize(*target),
                 })
             }
             TerminatorKind::SwitchInt { discr, targets } => {
                 let (discr, targets) = self.translate_switch_targets(discr, targets);
-                (None, RawTerminator::Switch { discr, targets })
+                (None, CharonRawTerminator::Switch { discr, targets })
             }
             TerminatorKind::Call { func, args, destination, target, .. } => {
                 debug!("translate_call: {func:?} {args:?} {destination:?} {target:?}");
@@ -552,14 +919,14 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                         let instance = Instance::resolve(def, &args).unwrap();
                         let def_id = instance.def.def_id();
                         let fid = self.register_fun_decl_id(def_id);
-                        FnPtr {
-                            func: FunIdOrTraitMethodRef::Fun(FunId::Regular(fid)),
+                        CharonFnPtr {
+                            func: CharonFunIdOrTraitMethodRef::Fun(CharonFunId::Regular(fid)),
                             // TODO: populate generics?
-                            generics: GenericArgs {
-                                regions: Vector::new(),
-                                types: Vector::new(),
-                                const_generics: Vector::new(),
-                                trait_refs: Vector::new(),
+                            generics: CharonGenericArgs {
+                                regions: CharonVector::new(),
+                                types: CharonVector::new(),
+                                const_generics: CharonVector::new(),
+                                trait_refs: CharonVector::new(),
                             },
                         }
                     }
@@ -569,22 +936,22 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                         x
                     ),
                 };
-                let func = FnOperand::Regular(fn_ptr);
-                let call = Call {
+                let func = CharonFnOperand::Regular(fn_ptr);
+                let call = CharonCall {
                     func,
                     args: args.iter().map(|arg| self.translate_operand(arg)).collect(),
                     dest: self.translate_place(destination),
                 };
-                (Some(RawStatement::Call(call)), RawTerminator::Goto {
-                    target: BlockId::from_usize(target.unwrap()),
+                (Some(CharonRawStatement::Call(call)), CharonRawTerminator::Goto {
+                    target: CharonBlockId::from_usize(target.unwrap()),
                 })
             }
             TerminatorKind::Assert { cond, expected, msg: _, target, .. } => (
-                Some(RawStatement::Assert(Assert {
+                Some(CharonRawStatement::Assert(CharonAssert {
                     cond: self.translate_operand(cond),
                     expected: *expected,
                 })),
-                RawTerminator::Goto { target: BlockId::from_usize(*target) },
+                CharonRawTerminator::Goto { target: CharonBlockId::from_usize(*target) },
             ),
             _ => todo!(),
         };
@@ -594,14 +961,20 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         )
     }
 
-    fn translate_place(&self, place: &Place) -> CharonPlace {
-        let projection = self.translate_projection(&place.projection);
+    fn translate_place(&mut self, place: &Place) -> CharonPlace {
+        let projection = self.translate_projection(place, &place.projection);
         let local = place.local;
-        let var_id = VarId::from_usize(local);
+        let var_id = CharonVarId::from_usize(local);
         CharonPlace { var_id, projection }
     }
 
-    fn translate_rvalue(&self, rvalue: &Rvalue) -> CharonRvalue {
+    fn place_ty (&self, place: &Place) -> Ty {
+        let body = self.instance.body().unwrap();
+        let ty = body.local_decl(place.local).unwrap().ty;
+        ty
+    }
+
+    fn translate_rvalue(&mut self, rvalue: &Rvalue) -> CharonRvalue {
         trace!("translate_rvalue: {rvalue:?}");
         match rvalue {
             Rvalue::Use(operand) => CharonRvalue::Use(self.translate_operand(operand)),
@@ -616,7 +989,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 None,
             ),
             Rvalue::Cast(kind, operand, ty) => CharonRvalue::UnaryOp(
-                UnOp::Cast(self.translate_cast(*kind, operand, *ty)),
+                CharonUnOp::Cast(self.translate_cast(*kind, operand, *ty)),
                 self.translate_operand(operand),
             ),
             Rvalue::BinaryOp(bin_op, lhs, rhs) => CharonRvalue::BinaryOp(
@@ -624,10 +997,67 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 self.translate_operand(lhs),
                 self.translate_operand(rhs),
             ),
-            Rvalue::CheckedBinaryOp(_, _, _) => todo!(),
-            Rvalue::UnaryOp(_, _) => todo!(),
-            Rvalue::Discriminant(_) => todo!(),
-            Rvalue::Aggregate(_, _) => todo!(),
+            //TODO: recheck
+            Rvalue::CheckedBinaryOp(bin_op, lhs, rhs) => CharonRvalue::BinaryOp(
+                translate_bin_op(*bin_op),
+                self.translate_operand(lhs),
+                self.translate_operand(rhs),
+            ),
+            Rvalue::UnaryOp(op, operand) => CharonRvalue::UnaryOp(translate_un_op(*op), self.translate_operand(operand)),
+            Rvalue::Discriminant(place) => {
+                let c_place = self.translate_place(place);
+                let ty = self.place_ty(place);
+                let c_ty = self.translate_ty(ty);
+                match c_ty.kind() {
+                    CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), _) => CharonRvalue::Discriminant(c_place, *c_typedeclid),
+                    _ => todo!()
+                }           
+            },
+
+            Rvalue::Aggregate(agg_kind, operands) => {
+                let c_operands = (*operands).iter().map(|operand| self.translate_operand(operand)).collect();
+                let akind = agg_kind.clone();
+                match akind {
+                    AggregateKind::Adt(adt_def, variant_id , gen_args , user_anot , field_id ) => {
+                        let adt_kind = adt_def.kind();
+                        match adt_kind {
+                            AdtKind::Enum => {
+                                let def_id = adt_def.def_id();                      
+                                let c_typedeclid: CharonTypeDeclId = self.find_type_decl_id(def_id);
+                                let c_type_id = CharonTypeId::Adt(c_typedeclid);
+                                let c_variant_id  = Some(CharonVariantId::from_usize(variant_id.to_index()));
+                                let c_field_id = match field_id {
+                                    Some(fid) => Some (CharonFieldId::from_usize(fid)),
+                                    None => None,
+                                };      
+                                let c_generic_args = CharonGenericArgs::empty();
+                                let c_agg_kind = CharonAggregateKind::Adt(c_type_id, c_variant_id, c_field_id, c_generic_args);
+                                CharonRvalue::Aggregate(c_agg_kind, c_operands)
+                            },
+                            AdtKind::Struct => {
+                                let def_id = adt_def.def_id();
+                                let c_typedeclid: CharonTypeDeclId = self.find_type_decl_id(def_id);
+                                let c_type_id = CharonTypeId::Adt(c_typedeclid);
+                                let c_variant_id  = None;
+                                let c_field_id = None;
+                                let c_generic_args = CharonGenericArgs::empty();
+                                let c_agg_kind = CharonAggregateKind::Adt(c_type_id, c_variant_id, c_field_id, c_generic_args);
+                                CharonRvalue::Aggregate(c_agg_kind, c_operands)
+                            },
+                            _ =>todo!()
+                        }
+                    },
+                    AggregateKind::Tuple => CharonRvalue::Aggregate(CharonAggregateKind::Adt(CharonTypeId::Tuple, None, None, CharonGenericArgs::empty()), c_operands),
+                    AggregateKind::Array(ty)=> {
+                        let c_ty = self.translate_ty(ty);
+                        let cg = CharonConstGeneric::Value(CharonLiteral::Scalar(CharonScalarValue::Usize(c_operands.len() as u64,)));
+                        CharonRvalue::Aggregate(CharonAggregateKind::Array(c_ty, cg), c_operands)
+                    }
+                    _ => todo!(),
+                    }
+                },
+
+            
             Rvalue::ShallowInitBox(_, _) => todo!(),
             Rvalue::CopyForDeref(_) => todo!(),
             Rvalue::ThreadLocalRef(_) => todo!(),
@@ -635,7 +1065,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         }
     }
 
-    fn translate_operand(&self, operand: &Operand) -> CharonOperand {
+    fn translate_operand(&mut self, operand: &Operand) -> CharonOperand {
         trace!("translate_operand: {operand:?}");
         match operand {
             Operand::Constant(constant) => CharonOperand::Const(self.translate_constant(constant)),
@@ -644,13 +1074,13 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         }
     }
 
-    fn translate_constant(&self, constant: &ConstOperand) -> ConstantExpr {
+    fn translate_constant(&mut self, constant: &ConstOperand) -> CharonConstantExpr {
         trace!("translate_constant: {constant:?}");
         let value = self.translate_constant_value(&constant.const_);
-        ConstantExpr { value, ty: self.translate_ty(constant.ty()) }
+        CharonConstantExpr { value, ty: self.translate_ty(constant.ty()) }
     }
 
-    fn translate_constant_value(&self, constant: &MirConst) -> RawConstantExpr {
+    fn translate_constant_value(&self, constant: &MirConst) -> CharonRawConstantExpr {
         trace!("translate_constant_value: {constant:?}");
         match constant.kind() {
             ConstantKind::Allocated(alloc) => self.translate_allocation(alloc, constant.ty()),
@@ -661,39 +1091,39 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         }
     }
 
-    fn translate_allocation(&self, alloc: &Allocation, ty: Ty) -> RawConstantExpr {
+    fn translate_allocation(&self, alloc: &Allocation, ty: Ty) -> CharonRawConstantExpr {
         match ty.kind() {
             TyKind::RigidTy(RigidTy::Int(it)) => {
                 let value = alloc.read_int().unwrap();
                 let scalar_value = match it {
-                    IntTy::I8 => ScalarValue::I8(value as i8),
-                    IntTy::I16 => ScalarValue::I16(value as i16),
-                    IntTy::I32 => ScalarValue::I32(value as i32),
-                    IntTy::I64 => ScalarValue::I64(value as i64),
-                    IntTy::I128 => ScalarValue::I128(value),
-                    IntTy::Isize => ScalarValue::Isize(value as i64),
+                    IntTy::I8 => CharonScalarValue::I8(value as i8),
+                    IntTy::I16 => CharonScalarValue::I16(value as i16),
+                    IntTy::I32 => CharonScalarValue::I32(value as i32),
+                    IntTy::I64 => CharonScalarValue::I64(value as i64),
+                    IntTy::I128 => CharonScalarValue::I128(value),
+                    IntTy::Isize => CharonScalarValue::Isize(value as i64),
                 };
-                RawConstantExpr::Literal(Literal::Scalar(scalar_value))
+                CharonRawConstantExpr::Literal(CharonLiteral::Scalar(scalar_value))
             }
             TyKind::RigidTy(RigidTy::Uint(uit)) => {
                 let value = alloc.read_uint().unwrap();
                 let scalar_value = match uit {
-                    UintTy::U8 => ScalarValue::U8(value as u8),
-                    UintTy::U16 => ScalarValue::U16(value as u16),
-                    UintTy::U32 => ScalarValue::U32(value as u32),
-                    UintTy::U64 => ScalarValue::U64(value as u64),
-                    UintTy::U128 => ScalarValue::U128(value),
-                    UintTy::Usize => ScalarValue::Usize(value as u64),
+                    UintTy::U8 => CharonScalarValue::U8(value as u8),
+                    UintTy::U16 => CharonScalarValue::U16(value as u16),
+                    UintTy::U32 => CharonScalarValue::U32(value as u32),
+                    UintTy::U64 => CharonScalarValue::U64(value as u64),
+                    UintTy::U128 => CharonScalarValue::U128(value),
+                    UintTy::Usize => CharonScalarValue::Usize(value as u64),
                 };
-                RawConstantExpr::Literal(Literal::Scalar(scalar_value))
+                CharonRawConstantExpr::Literal(CharonLiteral::Scalar(scalar_value))
             }
             TyKind::RigidTy(RigidTy::Bool) => {
                 let value = alloc.read_bool().unwrap();
-                RawConstantExpr::Literal(Literal::Bool(value))
+                CharonRawConstantExpr::Literal(CharonLiteral::Bool(value))
             }
             TyKind::RigidTy(RigidTy::Char) => {
                 let value = char::from_u32(alloc.read_uint().unwrap() as u32);
-                RawConstantExpr::Literal(Literal::Char(value.unwrap()))
+                CharonRawConstantExpr::Literal(CharonLiteral::Char(value.unwrap()))
             }
             _ => todo!(),
         }
@@ -704,7 +1134,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     }
 
     fn translate_switch_targets(
-        &self,
+        &mut self,
         discr: &Operand,
         targets: &SwitchTargets,
     ) -> (CharonOperand, CharonSwitchTargets) {
@@ -719,47 +1149,116 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let (value, bb) = targets.branches().last().unwrap();
             let (then_bb, else_bb) =
                 if value == 0 { (targets.otherwise(), bb) } else { (bb, targets.otherwise()) };
-            CharonSwitchTargets::If(BlockId::from_usize(then_bb), BlockId::from_usize(else_bb))
+            CharonSwitchTargets::If(CharonBlockId::from_usize(then_bb), CharonBlockId::from_usize(else_bb))
         } else {
-            let CharonTyKind::Literal(LiteralTy::Integer(int_ty)) = charon_ty.kind() else {
+            let CharonTyKind::Literal(CharonLiteralTy::Integer(int_ty)) = charon_ty.kind() else {
                 panic!("Expected integer type for switch discriminant");
             };
             let branches = targets
                 .branches()
                 .map(|(value, bb)| {
                     let scalar_val = match int_ty {
-                        IntegerTy::I8 => ScalarValue::I8(value as i8),
-                        IntegerTy::I16 => ScalarValue::I16(value as i16),
-                        IntegerTy::I32 => ScalarValue::I32(value as i32),
-                        IntegerTy::I64 => ScalarValue::I64(value as i64),
-                        IntegerTy::I128 => ScalarValue::I128(value as i128),
-                        IntegerTy::Isize => ScalarValue::Isize(value as i64),
-                        IntegerTy::U8 => ScalarValue::U8(value as u8),
-                        IntegerTy::U16 => ScalarValue::U16(value as u16),
-                        IntegerTy::U32 => ScalarValue::U32(value as u32),
-                        IntegerTy::U64 => ScalarValue::U64(value as u64),
-                        IntegerTy::U128 => ScalarValue::U128(value),
-                        IntegerTy::Usize => ScalarValue::Usize(value as u64),
+                        CharonIntegerTy::I8 => CharonScalarValue::I8(value as i8),
+                        CharonIntegerTy::I16 => CharonScalarValue::I16(value as i16),
+                        CharonIntegerTy::I32 => CharonScalarValue::I32(value as i32),
+                        CharonIntegerTy::I64 => CharonScalarValue::I64(value as i64),
+                        CharonIntegerTy::I128 => CharonScalarValue::I128(value as i128),
+                        CharonIntegerTy::Isize => CharonScalarValue::Isize(value as i64),
+                        CharonIntegerTy::U8 => CharonScalarValue::U8(value as u8),
+                        CharonIntegerTy::U16 => CharonScalarValue::U16(value as u16),
+                        CharonIntegerTy::U32 => CharonScalarValue::U32(value as u32),
+                        CharonIntegerTy::U64 => CharonScalarValue::U64(value as u64),
+                        CharonIntegerTy::U128 => CharonScalarValue::U128(value),
+                        CharonIntegerTy::Usize => CharonScalarValue::Usize(value as u64),
                     };
-                    (scalar_val, BlockId::from_usize(bb))
+                    (scalar_val, CharonBlockId::from_usize(bb))
                 })
                 .collect();
-            let otherwise = BlockId::from_usize(targets.otherwise());
+            let otherwise = CharonBlockId::from_usize(targets.otherwise());
             CharonSwitchTargets::SwitchInt(*int_ty, branches, otherwise)
         };
         (discr, switch_targets)
     }
 
-    fn translate_projection(&self, projection: &[ProjectionElem]) -> Vec<CharonProjectionElem> {
-        projection.iter().map(|elem| self.translate_projection_elem(elem)).collect()
+    fn translate_projection(&mut self, place: &Place, projection: &[ProjectionElem]) -> Vec<CharonProjectionElem> {
+        let c_place_ty = self.translate_ty(self.place_ty(place));
+        let mut c_provec = Vec::new();
+        let mut current_ty = c_place_ty.clone();
+        let mut current_var: usize = 0;
+        for prj in projection.iter() {            
+            match prj {
+                ProjectionElem::Deref => c_provec.push(CharonProjectionElem::Deref),
+                ProjectionElem::Field(fid, ty) => {
+                    let c_fieldid = CharonFieldId::from_usize(*fid);
+                    let c_variantid = CharonVariantId::from_usize(current_var);
+                    match current_ty.kind() {
+                        CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => 
+                        {
+                            let adttype = self.translated.type_decls.get(*tdid).unwrap();
+                            match adttype.kind {
+                                CharonTypeDeclKind::Struct(_) => 
+                                    {
+                                        let c_fprj = CharonFieldProjKind::Adt(*tdid, None);
+                                        c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
+                                        let current_ty = ty.clone();
+                                    }                         
+                                CharonTypeDeclKind::Enum(_) => 
+                                    {
+                                        let c_fprj = CharonFieldProjKind::Adt(*tdid, Some(c_variantid));
+                                        c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
+                                        let current_ty = ty.clone();
+                                    }
+                                _ => (),}
+                        }                       
+                        CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => 
+                            {
+                                let c_fprj = CharonFieldProjKind::Tuple((*genargs).types.len());
+                                c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
+                                let current_ty = ty.clone();
+                            }
+                        _ => ()
+                        }
+                }
+                ProjectionElem::Downcast(varid) => 
+                    {
+                        let current_var = varid.to_index();
+                    }
+                
+                _ => continue,
+                }
+        }
+        c_provec
     }
-
-    fn translate_projection_elem(&self, projection_elem: &ProjectionElem) -> CharonProjectionElem {
+/* 
+    fn translate_projection_elem(&mut self, place: &Place, projection_elem: &ProjectionElem) -> CharonProjectionElem {
         match projection_elem {
             ProjectionElem::Deref => CharonProjectionElem::Deref,
+            /* 
+            ProjectionElem::Downcast(varid) => {
+                let c_varid = CharonVariantId::from_usize((*varid).to_index());
+                let c_place_ty = self.translate_ty(self.place_ty(place));
+                let c_typedeclid =  *match c_place_ty.kind() {
+                    CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => tdid,
+                    _ => todo!()
+                };   
+                let c_fprj = CharonFieldProjKind::Adt(c_typedeclid, Some(c_varid));
+                let c_fieldid = CharonFieldId::from_usize(0);
+                CharonProjectionElem::Field(c_fprj,c_fieldid)
+            },*/
+            ProjectionElem::Field(fid, ty, ) =>{
+                let c_fieldid = CharonFieldId::from_usize(*fid);
+                let c_place_ty = self.translate_ty(self.place_ty(place));
+                let c_fprj = match c_place_ty.kind() {
+                    CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => CharonFieldProjKind::Adt(*tdid, None),
+                    CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => CharonFieldProjKind::Tuple((*genargs).types.len()),
+                    _ => todo!()
+                };
+                CharonProjectionElem::Field(c_fprj, c_fieldid)
+            }
             _ => todo!(),
         }
     }
+*/
 
     fn translate_region(&self, region: Region) -> CharonRegion {
         match region.kind {
@@ -772,35 +1271,38 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     }
 }
 
-fn translate_int_ty(int_ty: IntTy) -> IntegerTy {
+fn translate_int_ty(int_ty: IntTy) -> CharonIntegerTy {
     match int_ty {
-        IntTy::I8 => IntegerTy::I8,
-        IntTy::I16 => IntegerTy::I16,
-        IntTy::I32 => IntegerTy::I32,
-        IntTy::I64 => IntegerTy::I64,
-        IntTy::I128 => IntegerTy::I128,
+        IntTy::I8 => CharonIntegerTy::I8,
+        IntTy::I16 => CharonIntegerTy::I16,
+        IntTy::I32 => CharonIntegerTy::I32,
+        IntTy::I64 => CharonIntegerTy::I64,
+        IntTy::I128 => CharonIntegerTy::I128,
         // TODO: assumes 64-bit platform
-        IntTy::Isize => IntegerTy::I64,
+        IntTy::Isize => CharonIntegerTy::I64,
     }
 }
 
-fn translate_uint_ty(uint_ty: UintTy) -> IntegerTy {
+fn translate_uint_ty(uint_ty: UintTy) -> CharonIntegerTy {
     match uint_ty {
-        UintTy::U8 => IntegerTy::U8,
-        UintTy::U16 => IntegerTy::U16,
-        UintTy::U32 => IntegerTy::U32,
-        UintTy::U64 => IntegerTy::U64,
-        UintTy::U128 => IntegerTy::U128,
+        UintTy::U8 => CharonIntegerTy::U8,
+        UintTy::U16 => CharonIntegerTy::U16,
+        UintTy::U32 => CharonIntegerTy::U32,
+        UintTy::U64 => CharonIntegerTy::U64,
+        UintTy::U128 => CharonIntegerTy::U128,
         // TODO: assumes 64-bit platform
-        UintTy::Usize => IntegerTy::U64,
+        UintTy::Usize => CharonIntegerTy::U64,
     }
 }
 
 fn translate_bin_op(bin_op: BinOp) -> CharonBinOp {
     match bin_op {
-        BinOp::Add | BinOp::AddUnchecked => CharonBinOp::Add,
-        BinOp::Sub | BinOp::SubUnchecked => CharonBinOp::Sub,
-        BinOp::Mul | BinOp::MulUnchecked => CharonBinOp::Mul,
+        BinOp::AddUnchecked => CharonBinOp::Add,
+        BinOp::Add => CharonBinOp::CheckedAdd,
+        BinOp::SubUnchecked => CharonBinOp::Sub,
+        BinOp::Sub => CharonBinOp::CheckedSub,
+        BinOp::MulUnchecked => CharonBinOp::Mul,
+        BinOp::Mul => CharonBinOp::CheckedMul,
         BinOp::Div => CharonBinOp::Div,
         BinOp::Rem => CharonBinOp::Rem,
         BinOp::BitXor => CharonBinOp::BitXor,
@@ -819,6 +1321,18 @@ fn translate_bin_op(bin_op: BinOp) -> CharonBinOp {
     }
 }
 
+
+
+fn translate_un_op(un_op: UnOp) -> CharonUnOp {
+    match un_op {
+        UnOp::Not => CharonUnOp::Not,
+        UnOp::Neg => CharonUnOp::Neg,
+        UnOp::PtrMetadata => todo!()
+    }
+
+}
+
+
 fn translate_borrow_kind(kind: &BorrowKind) -> CharonBorrowKind {
     match kind {
         BorrowKind::Shared => CharonBorrowKind::Shared,
@@ -826,3 +1340,14 @@ fn translate_borrow_kind(kind: &BorrowKind) -> CharonBorrowKind {
         BorrowKind::Fake(_kind) => todo!(),
     }
 }
+
+fn translate_constant_expr_to_const_generic(
+    value: CharonRawConstantExpr,
+) -> Result<CharonConstGeneric, CharonError> {
+    match value {
+        CharonRawConstantExpr::Literal(v) => Ok(CharonConstGeneric::Value(v)),
+        CharonRawConstantExpr::Var(v) => Ok(CharonConstGeneric::Var(v)),
+        _ => todo!()
+        }    
+    }
+
diff --git a/tests/expected/llbc/basic0/TestRNvCshcvyQEKZjUj4test4main.symtab.lean b/tests/expected/llbc/basic0/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
new file mode 100644
index 000000000000..bcb9aabce301
--- /dev/null
+++ b/tests/expected/llbc/basic0/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
@@ -0,0 +1,24 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::tuple_fn]:
+   Source: 'test.rs', lines 38:1-38:33 -/
+def tuple_fn (t : (I32 × I32)) : Result I32 :=
+  let (i, i1) := t
+  i + i1
+
+/- [test::main]:
+   Source: 'test.rs', lines 43:1-43:10 -/
+def main : Result Unit :=
+  do
+  let _ ← tuple_fn (1#i32, 2#i32)
+  Result.ok ()
+
+end test
diff --git a/tests/expected/llbc/basic0/expected b/tests/expected/llbc/basic0/expected
index 45d073737f3b..bc35dff45272 100644
--- a/tests/expected/llbc/basic0/expected
+++ b/tests/expected/llbc/basic0/expected
@@ -5,4 +5,4 @@ fn test::is_zero(@1: i32) -> bool\
 
     @0 := copy (i@1) == const (0 : i32)\
     return\
-}
+}
\ No newline at end of file
diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs
index 410cf1848d44..cbd1e0a3a253 100644
--- a/tests/expected/llbc/basic0/test.rs
+++ b/tests/expected/llbc/basic0/test.rs
@@ -12,4 +12,4 @@ fn is_zero(i: i32) -> bool {
 #[kani::proof]
 fn main() {
     let _ = is_zero(0);
-}
+}
\ No newline at end of file
diff --git a/tests/expected/llbc/basic1/TestRNvCshcvyQEKZjUj4test4main.symtab.lean b/tests/expected/llbc/basic1/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
new file mode 100644
index 000000000000..e9731570d6b4
--- /dev/null
+++ b/tests/expected/llbc/basic1/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
@@ -0,0 +1,25 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::select]:
+   Source: 'test.rs', lines 8:1-8:42 -/
+def select (s : Bool) (x : I32) (y : I32) : Result I32 :=
+  if s
+  then Result.ok x
+  else Result.ok y
+
+/- [test::main]:
+   Source: 'test.rs', lines 13:1-13:10 -/
+def main : Result Unit :=
+  do
+  let _ ← select true 3#i32 7#i32
+  Result.ok ()
+
+end test
diff --git a/tests/expected/llbc/enum_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean b/tests/expected/llbc/enum_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
new file mode 100644
index 000000000000..9460d45ece3b
--- /dev/null
+++ b/tests/expected/llbc/enum_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
@@ -0,0 +1,31 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::MyEnum]
+   Source: 'test.rs', lines 8:1-8:12 -/
+inductive MyEnum :=
+| A : I32 → MyEnum
+| B : MyEnum
+
+/- [test::enum_match]:
+   Source: 'test.rs', lines 14:1-14:32 -/
+def enum_match (e : MyEnum) : Result I32 :=
+  match e with
+  | MyEnum.A i => Result.ok i
+  | MyEnum.B => Result.ok 0#i32
+
+/- [test::main]:
+   Source: 'test.rs', lines 24:1-24:10 -/
+def main : Result Unit :=
+  do
+  let _ ← enum_match (MyEnum.A 1#i32)
+  Result.ok ()
+
+end test
diff --git a/tests/expected/llbc/enum_test/expected b/tests/expected/llbc/enum_test/expected
new file mode 100644
index 000000000000..7b61e8d75ef4
--- /dev/null
+++ b/tests/expected/llbc/enum_test/expected
@@ -0,0 +1,36 @@
+enum test::MyEnum =
+|  A(0: i32)
+|  B()
+
+
+fn test::enum_match(@1: @Adt0) -> i32
+{
+    let @0: i32; // return
+    let e@1: @Adt0; // arg #1
+    let i@2: i32; // local
+
+    match e@1 {
+        0 => {
+            i@2 := copy ((e@1 as variant @0).0)
+            @0 := copy (i@2)
+            drop i@2
+        },
+        1 => {
+            @0 := const (0 : i32)
+        },
+    }
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let e@1: @Adt0; // local
+    let i@2: i32; // local
+
+    e@1 := test::MyEnum::A { 0: const (1 : i32) }
+    i@2 := @Fun0(move (e@1))
+    drop i@2
+    @0 := ()
+    return
+}
\ No newline at end of file
diff --git a/tests/expected/llbc/enum_test/test.rs b/tests/expected/llbc/enum_test/test.rs
new file mode 100644
index 000000000000..c271275fa9c0
--- /dev/null
+++ b/tests/expected/llbc/enum_test/test.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zlean --print-llbc
+
+//! This test checks that Kani's LLBC backend handles simple enum
+
+
+enum MyEnum {
+    A(i32),
+    B,
+}
+
+
+fn enum_match(e: MyEnum) -> i32 {
+    match e {
+        MyEnum::A(i) => i ,
+        MyEnum::B => 0 ,
+    }
+}
+
+
+
+#[kani::proof]
+fn main() {
+    let e = MyEnum::A(1);
+    let i = enum_match(e);
+}
diff --git a/tests/expected/llbc/projection_test/expected b/tests/expected/llbc/projection_test/expected
new file mode 100644
index 000000000000..3ce8819a8b21
--- /dev/null
+++ b/tests/expected/llbc/projection_test/expected
@@ -0,0 +1,49 @@
+struct test::MyStruct =
+{
+  a: i32,
+  b: i32,
+}
+
+enum test::MyEnum =
+|  A(0: @Adt1, 1: i32)
+|  B()
+
+
+fn test::enum_match(@1: @Adt0) -> i32
+{
+    let @0: i32; // return
+    let e@1: @Adt0; // arg #1
+    let s@2: @Adt1; // local
+    let i@3: i32; // local
+    let @4: i32; // anonymous local
+
+    match e@1 {
+        0 => {
+            s@2 := move ((e@1 as variant @0).0)
+            i@3 := copy ((e@1 as variant @0).1)
+            @4 := copy ((s@2).a)
+            @0 := copy (@4) + copy (i@3)
+            drop @4
+            drop s@2
+        },
+        1 => {
+            @0 := const (0 : i32)
+        },
+    }
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let s@1: @Adt1; // local
+    let e@2: @Adt0; // local
+    let i@3: i32; // local
+
+    s@1 := @Adt1 { a: const (1 : i32), b: const (2 : i32) }
+    e@2 := test::MyEnum::A { 0: move (s@1), 1: const (1 : i32) }
+    i@3 := @Fun0(move (e@2))
+    drop i@3
+    @0 := ()
+    return
+}
\ No newline at end of file
diff --git a/tests/expected/llbc/projection_test/test.rs b/tests/expected/llbc/projection_test/test.rs
new file mode 100644
index 000000000000..22440d7a9986
--- /dev/null
+++ b/tests/expected/llbc/projection_test/test.rs
@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zlean --print-llbc
+
+//! This test checks that Kani's LLBC backend handles simple projection
+
+struct MyStruct {
+    a: i32,
+    b: i32,
+}
+
+enum MyEnum {
+    A(MyStruct, i32),
+    B,
+}
+
+
+fn enum_match(e: MyEnum) -> i32 {
+    match e {
+        MyEnum::A(s, i) => s.a + i,
+        MyEnum::B => 0 ,
+    }
+}
+
+
+
+#[kani::proof]
+fn main() {
+    let s = MyStruct { a: 1, b: 2 };
+    let e = MyEnum::A(s,1);
+    let i = enum_match(e);
+}
diff --git a/tests/expected/llbc/struct_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean b/tests/expected/llbc/struct_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
new file mode 100644
index 000000000000..3be8da62cf28
--- /dev/null
+++ b/tests/expected/llbc/struct_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
@@ -0,0 +1,29 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::MyStruct]
+   Source: 'test.rs', lines 7:1-7:16 -/
+structure MyStruct where
+  a : I32
+  b : Bool
+
+/- [test::struct_project]:
+   Source: 'test.rs', lines 12:1-12:38 -/
+def struct_project (s : MyStruct) : Result I32 :=
+  Result.ok s.a
+
+/- [test::main]:
+   Source: 'test.rs', lines 17:1-17:10 -/
+def main : Result Unit :=
+  do
+  let _ ← struct_project { a := 1#i32, b := true }
+  Result.ok ()
+
+end test
diff --git a/tests/expected/llbc/struct_test/expected b/tests/expected/llbc/struct_test/expected
new file mode 100644
index 000000000000..58c90867c732
--- /dev/null
+++ b/tests/expected/llbc/struct_test/expected
@@ -0,0 +1,27 @@
+struct test::MyStruct =
+{
+  a: i32,
+  b: bool,
+}
+
+fn test::struct_project(@1: @Adt0) -> i32
+{
+    let @0: i32; // return
+    let s@1: @Adt0; // arg #1
+
+    @0 := copy ((s@1).a)
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let s@1: @Adt0; // local
+    let a@2: i32; // local
+
+    s@1 := @Adt0 { a: const (1 : i32), b: const (true) }
+    a@2 := @Fun0(move (s@1))
+    drop a@2
+    @0 := ()
+    return
+}
\ No newline at end of file
diff --git a/tests/expected/llbc/struct_test/test.rs b/tests/expected/llbc/struct_test/test.rs
new file mode 100644
index 000000000000..14c9bac45258
--- /dev/null
+++ b/tests/expected/llbc/struct_test/test.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zlean --print-llbc
+
+//! This test checks that Kani's LLBC backend handles simple struct
+
+struct MyStruct{
+    a: i32,
+    b: bool,
+}
+
+fn struct_project(s: MyStruct) -> i32 {
+    s.a
+}
+
+#[kani::proof]
+fn main() {
+    let s = MyStruct { a: 1, b: true };
+    let a = struct_project(s);
+}
diff --git a/tests/expected/llbc/tuple_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean b/tests/expected/llbc/tuple_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
new file mode 100644
index 000000000000..0c1c30720a6e
--- /dev/null
+++ b/tests/expected/llbc/tuple_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean
@@ -0,0 +1,24 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::tuple_add]:
+   Source: 'test.rs', lines 7:1-7:36 -/
+def tuple_add (t : (I32 × I32)) : Result I32 :=
+  let (i, i1) := t
+  i + i1
+
+/- [test::main]:
+   Source: 'test.rs', lines 12:1-12:10 -/
+def main : Result Unit :=
+  do
+  let _ ← tuple_add (1#i32, 2#i32)
+  Result.ok ()
+
+end test
diff --git a/tests/expected/llbc/tuple_test/expected b/tests/expected/llbc/tuple_test/expected
new file mode 100644
index 000000000000..2459a98f7021
--- /dev/null
+++ b/tests/expected/llbc/tuple_test/expected
@@ -0,0 +1,28 @@
+fn test::tuple_add(@1: (i32, i32)) -> i32
+{
+    let @0: i32; // return
+    let t@1: (i32, i32); // arg #1
+    let @2: i32; // anonymous local
+    let @3: i32; // anonymous local
+
+    @2 := copy ((t@1).0)
+    @3 := copy ((t@1).1)
+    @0 := copy (@2) + copy (@3)
+    drop @3
+    drop @2
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let s@1: i32; // local
+    let @2: (i32, i32); // anonymous local
+
+    @2 := (const (1 : i32), const (2 : i32))
+    s@1 := @Fun0(move (@2))
+    drop @2
+    drop s@1
+    @0 := ()
+    return
+}
\ No newline at end of file
diff --git a/tests/expected/llbc/tuple_test/test.rs b/tests/expected/llbc/tuple_test/test.rs
new file mode 100644
index 000000000000..4a2a2cc87141
--- /dev/null
+++ b/tests/expected/llbc/tuple_test/test.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zlean --print-llbc
+
+//! This test checks that Kani's LLBC backend handles simple tuple
+
+fn tuple_add (t: (i32, i32)) -> i32 {
+    t.0 + t.1
+}
+
+#[kani::proof]
+fn main() {
+    let s = tuple_add((1, 2));
+}
diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
index cb41b35a9bc0..65d55a48ae49 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit cb41b35a9bc0412435b70b5038df0681a881e414
+Subproject commit 65d55a48ae4916c2a0c4ab9a90631668ba8ea23f

From 0937022931484f8e7a5740db7bfdccb13b354572 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Fri, 15 Nov 2024 11:08:09 -0800
Subject: [PATCH 2/4] revert changes

---
 Cargo.lock          | 12 ------------
 charon              |  2 +-
 tests/perf/s2n-quic |  2 +-
 3 files changed, 2 insertions(+), 14 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 1c1d3b6458e0..a8436fe8dea2 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -253,7 +253,6 @@ dependencies = [
  "clap",
  "colored",
  "convert_case 0.6.0",
- "derivative",
  "derive-visitor",
  "env_logger",
  "hashlink",
@@ -497,17 +496,6 @@ dependencies = [
  "powerfmt",
 ]
 
-[[package]]
-name = "derivative"
-version = "2.2.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "derive-visitor"
 version = "0.4.0"
diff --git a/charon b/charon
index 2193aa00fd89..454078ebdb4a 160000
--- a/charon
+++ b/charon
@@ -1 +1 @@
-Subproject commit 2193aa00fd89e991226ada10d8a8f66e0594f212
+Subproject commit 454078ebdb4a607e2b21dc115e1ca99b516e436f
diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
index 65d55a48ae49..cb41b35a9bc0 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit 65d55a48ae4916c2a0c4ab9a90631668ba8ea23f
+Subproject commit cb41b35a9bc0412435b70b5038df0681a881e414

From bb789a784e47c5817146c32f8ba9d60a8c1e70aa Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Fri, 15 Nov 2024 11:10:25 -0800
Subject: [PATCH 3/4] format code

---
 .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs   | 471 ++++++++++--------
 tests/expected/llbc/basic0/test.rs            |   2 +-
 tests/expected/llbc/enum_test/test.rs         |   8 +-
 tests/expected/llbc/projection_test/test.rs   |   7 +-
 tests/expected/llbc/struct_test/test.rs       |   2 +-
 tests/expected/llbc/tuple_test/test.rs        |   2 +-
 6 files changed, 271 insertions(+), 221 deletions(-)

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 0d006456ea8a..021cea6444eb 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
@@ -13,44 +13,54 @@ use std::path::PathBuf;
 
 use charon_lib::ast::AggregateKind as CharonAggregateKind;
 use charon_lib::ast::CastKind as CharonCastKind;
+use charon_lib::ast::Field as CharonField;
 use charon_lib::ast::FieldId as CharonFieldId;
 use charon_lib::ast::Place as CharonPlace;
 use charon_lib::ast::ProjectionElem as CharonProjectionElem;
 use charon_lib::ast::Rvalue as CharonRvalue;
 use charon_lib::ast::Span as CharonSpan;
-use charon_lib::ast::meta::{AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan};
-use charon_lib::ast::types::Ty as CharonTy;
-use charon_lib::ast::types::TypeDeclId as CharonTypeDeclId;
-use charon_lib::ast::types::TyKind as CharonTyKind;
 use charon_lib::ast::TypeDecl as CharonTypeDecl;
 use charon_lib::ast::TypeDeclKind as CharonTypeDeclKind;
 use charon_lib::ast::Variant as CharonVariant;
-use charon_lib::ast::Field as CharonField;
-use charon_lib::ast::{AbortKind as CharonAbortKind, Body as CharonBody, Var as CharonVar, VarId as CharonVarId};
+use charon_lib::ast::meta::{
+    AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan,
+};
+use charon_lib::ast::types::Ty as CharonTy;
+use charon_lib::ast::types::TyKind as CharonTyKind;
+use charon_lib::ast::types::TypeDeclId as CharonTypeDeclId;
+use charon_lib::ast::{
+    AbortKind as CharonAbortKind, Body as CharonBody, Var as CharonVar, VarId as CharonVarId,
+};
 use charon_lib::ast::{
-    AnyTransId as CharonAnyTransId, Assert as CharonAssert, BodyId as CharonBodyId, BuiltinTy as CharonBuiltinTy, 
-    Disambiguator as CharonDisambiguator, FileName as CharonFileName, FunDecl as CharonFunDecl, FunSig as CharonFunSig, GenericArgs as CharonGenericArgs,
-    GenericParams as CharonGenericParams, IntegerTy as CharonIntegerTy, 
-    ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, 
-    Literal as CharonLiteral, LiteralTy as CharonLiteralTy, Name as CharonName, Opaque as CharonOpaque,
-    PathElem as CharonPathElem, RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, ScalarValue as CharonScalarValue, 
-    TranslatedCrate as CharonTranslatedCrate, TypeId as CharonTypeId, RegionId as CharonRegionId, TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, ConstGeneric as CharonConstGeneric,
-    ConstGenericVarId as CharonConstGenericVarId, FieldProjKind as CharonFieldProjKind,
+    AnyTransId as CharonAnyTransId, Assert as CharonAssert, BodyId as CharonBodyId,
+    BuiltinTy as CharonBuiltinTy, ConstGeneric as CharonConstGeneric,
+    ConstGenericVarId as CharonConstGenericVarId, Disambiguator as CharonDisambiguator,
+    FieldProjKind as CharonFieldProjKind, FileName as CharonFileName, FunDecl as CharonFunDecl,
+    FunSig as CharonFunSig, GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams,
+    IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta,
+    ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy,
+    Name as CharonName, Opaque as CharonOpaque, PathElem as CharonPathElem,
+    RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion,
+    RegionId as CharonRegionId, ScalarValue as CharonScalarValue,
+    TranslatedCrate as CharonTranslatedCrate, TypeId as CharonTypeId, TypeVarId as CharonTypeVarId,
+    UnOp as CharonUnOp,
 };
 use charon_lib::ast::{
-    BinOp as CharonBinOp, Call as CharonCall, FnOperand as CharonFnOperand, FnPtr as CharonFnPtr, 
-    FunDeclId as CharonFunDeclId, FunId as CharonFunId, FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, VariantId as CharonVariantId,
+    BinOp as CharonBinOp, Call as CharonCall, FnOperand as CharonFnOperand, FnPtr as CharonFnPtr,
+    FunDeclId as CharonFunDeclId, FunId as CharonFunId,
+    FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, VariantId as CharonVariantId,
 };
 use charon_lib::ast::{
-    BorrowKind as CharonBorrowKind, ConstantExpr as CharonConstantExpr, Operand as CharonOperand, 
+    BorrowKind as CharonBorrowKind, ConstantExpr as CharonConstantExpr, Operand as CharonOperand,
 };
 use charon_lib::errors::Error as CharonError;
 use charon_lib::errors::ErrorCtx as CharonErrorCtx;
 use charon_lib::ids::Vector as CharonVector;
 use charon_lib::ullbc_ast::{
-    BlockData as CharonBlockData, BlockId as CharonBlockId, BodyContents as CharonBodyContents, ExprBody as CharonExprBody, 
-    RawStatement as CharonRawStatement, RawTerminator as CharonRawTerminator, Statement as CharonStatement, SwitchTargets as CharonSwitchTargets,
-    Terminator as CharonTerminator,
+    BlockData as CharonBlockData, BlockId as CharonBlockId, BodyContents as CharonBodyContents,
+    ExprBody as CharonExprBody, RawStatement as CharonRawStatement,
+    RawTerminator as CharonRawTerminator, Statement as CharonStatement,
+    SwitchTargets as CharonSwitchTargets, Terminator as CharonTerminator,
 };
 use charon_lib::{error_assert, error_or_panic};
 use rustc_data_structures::fx::FxHashMap;
@@ -58,22 +68,23 @@ use rustc_data_structures::stable_hasher::HashStable;
 use rustc_middle::ty::AdtKind as MirAdtKind;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
-use stable_mir::ty::AdtDef;
-use stable_mir::ty::AdtKind;
 use stable_mir::abi::PassMode;
 use stable_mir::mir::AggregateKind;
 use stable_mir::mir::VarDebugInfoContents;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::mono::InstanceDef;
 use stable_mir::mir::{
-    BasicBlock, BinOp, UnOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability, Operand, Place,
+    BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability, Operand, Place,
     ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
+    UnOp,
 };
+use stable_mir::ty::AdtDef;
+use stable_mir::ty::AdtKind;
 use stable_mir::ty::{
-    Allocation, ConstantKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span, Ty,
-    TyKind, UintTy, TyConst, TyConstId, TraitDef, TyConstKind
+    Allocation, ConstantKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span,
+    TraitDef, Ty, TyConst, TyConstId, TyConstKind, TyKind, UintTy,
 };
-use stable_mir::ty::{GenericArgs, GenericArgKind};
+use stable_mir::ty::{GenericArgKind, GenericArgs};
 use stable_mir::{CrateDef, DefId};
 use syn::token::Default;
 use tracing::{debug, trace};
@@ -146,8 +157,13 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             }
         };
 
-        let fun_decl =
-            CharonFunDecl { def_id: fid, item_meta, signature, kind: CharonItemKind::Regular, body: Ok(body) };
+        let fun_decl = CharonFunDecl {
+            def_id: fid,
+            item_meta,
+            signature,
+            kind: CharonItemKind::Regular,
+            body: Ok(body),
+        };
 
         self.translated.fun_decls.set_slot(fid, fun_decl);
 
@@ -173,7 +189,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
 
     fn find_fun_decl_id(&self, def_id: DefId) -> CharonFunDeclId {
         debug!("register_fun_decl_id: {:?}", def_id);
-        let tid = *self.id_map.get(&def_id).unwrap(); 
+        let tid = *self.id_map.get(&def_id).unwrap();
         debug!("register_fun_decl_id: {:?}", self.id_map);
         tid.try_into().unwrap()
     }
@@ -192,11 +208,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         };
         debug!("register_type_decl_id: {:?}", self.id_map);
         tid.try_into().unwrap()
-    }    
+    }
 
     fn find_type_decl_id(&self, def_id: DefId) -> CharonTypeDeclId {
         debug!("register_type_decl_id: {:?}", def_id);
-        let tid = *self.id_map.get(&def_id).unwrap(); 
+        let tid = *self.id_map.get(&def_id).unwrap();
         debug!("register_type_decl_id: {:?}", self.id_map);
         tid.try_into().unwrap()
     }
@@ -207,70 +223,87 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         CharonScalarValue::from_bits(int_ty, discr_val)
     }
 
-
     fn translate_adtdef(&mut self, adt_def: AdtDef) -> CharonTypeDeclId {
         match adt_def.kind() {
             AdtKind::Enum => {
-                let def_id  = adt_def.def_id();
+                let def_id = adt_def.def_id();
                 let c_typedeclid = self.register_type_decl_id(def_id);
-                let mut c_variants: CharonVector<CharonVariantId, CharonVariant> = CharonVector::new();
-                for var_def in adt_def.variants_iter(){
-                    let mut c_fields: CharonVector<CharonFieldId, CharonField> = CharonVector::new();
-                    for field_def in var_def.fields(){
+                let mut c_variants: CharonVector<CharonVariantId, CharonVariant> =
+                    CharonVector::new();
+                for var_def in adt_def.variants_iter() {
+                    let mut c_fields: CharonVector<CharonFieldId, CharonField> =
+                        CharonVector::new();
+                    for field_def in var_def.fields() {
                         let c_field_ty = self.translate_ty(field_def.ty());
                         let c_field_name = Some(field_def.name);
                         let c_span = self.translate_span(adt_def.span());
                         let c_field = CharonField {
-                            span : c_span,
-                            attr_info : CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true },
+                            span: c_span,
+                            attr_info: CharonAttrInfo {
+                                attributes: Vec::new(),
+                                inline: None,
+                                rename: None,
+                                public: true,
+                            },
                             name: c_field_name,
                             ty: c_field_ty,
                         };
                         c_fields.push(c_field);
                     }
                     let var_name = var_def.name();
-                    let span = self.translate_span(adt_def.span()); 
+                    let span = self.translate_span(adt_def.span());
 
                     let adtdef_internal = rustc_internal::internal(self.tcx, adt_def);
                     let variant_index_internal = rustc_internal::internal(self.tcx, var_def.idx);
-                    let discr = adtdef_internal.discriminant_for_variant(self.tcx, variant_index_internal);
+                    let discr =
+                        adtdef_internal.discriminant_for_variant(self.tcx, variant_index_internal);
                     let discr_val = discr.val;
                     let discr_ty = rustc_internal::stable(discr.ty);
                     let c_discr = self.get_discriminant(discr_val, discr_ty);
 
-                    let c_variant = CharonVariant{
-                        span : span,
-                        attr_info : CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true },
-                        name : var_name,
-                        fields : c_fields,
-                        discriminant : c_discr,
+                    let c_variant = CharonVariant {
+                        span: span,
+                        attr_info: CharonAttrInfo {
+                            attributes: Vec::new(),
+                            inline: None,
+                            rename: None,
+                            public: true,
+                        },
+                        name: var_name,
+                        fields: c_fields,
+                        discriminant: c_discr,
                     };
                     let c_varidx = c_variants.push(c_variant);
                     assert_eq!(c_varidx.index(), var_def.idx.to_index());
-                }                        
+                }
                 let item_meta = self.translate_item_meta_adt(adt_def).unwrap();
                 let typedecl = CharonTypeDecl {
                     def_id: c_typedeclid,
                     generics: CharonGenericParams::empty(),
                     kind: CharonTypeDeclKind::Enum(c_variants),
-                    item_meta : item_meta,
+                    item_meta: item_meta,
                 };
                 self.translated.type_decls.set_slot(c_typedeclid, typedecl);
                 c_typedeclid
             }
             AdtKind::Struct => {
-                let def_id  = adt_def.def_id();
+                let def_id = adt_def.def_id();
                 let c_typedeclid = self.register_type_decl_id(def_id);
                 let mut c_fields: CharonVector<CharonFieldId, CharonField> = CharonVector::new();
                 let only_variant = *adt_def.variants().first().unwrap();
                 let fields = only_variant.fields();
-                for field_def in fields{
+                for field_def in fields {
                     let c_field_ty = self.translate_ty(field_def.ty());
                     let c_field_name = Some(field_def.name);
                     let c_span = self.translate_span(adt_def.span());
                     let c_field = CharonField {
-                        span : c_span,
-                        attr_info : CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true },
+                        span: c_span,
+                        attr_info: CharonAttrInfo {
+                            attributes: Vec::new(),
+                            inline: None,
+                            rename: None,
+                            public: true,
+                        },
                         name: c_field_name,
                         ty: c_field_ty,
                     };
@@ -281,17 +314,20 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     def_id: c_typedeclid,
                     generics: CharonGenericParams::empty(),
                     kind: CharonTypeDeclKind::Struct(c_fields),
-                    item_meta : item_meta,
+                    item_meta: item_meta,
                 };
                 self.translated.type_decls.set_slot(c_typedeclid, typedecl);
                 c_typedeclid
             }
-            _ => todo!(),             
+            _ => todo!(),
         }
     }
 
     /// Compute the meta information for a Rust item identified by its id.
-    fn translate_item_meta_from_rid(&mut self, instance: Instance) -> Result<CharonItemMeta, CharonError> {
+    fn translate_item_meta_from_rid(
+        &mut self,
+        instance: Instance,
+    ) -> Result<CharonItemMeta, CharonError> {
         let span = self.translate_instance_span(instance);
         let name = self.def_to_name(instance.def)?;
         // TODO: populate the source text
@@ -331,7 +367,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         Ok(CharonItemMeta { span, source_text, attr_info, name, is_local, opacity })
     }
 
-
     /// Retrieve an item name from a [DefId].
     /// This function is adapted from Charon:
     /// https://github.com/AeneasVerif/charon/blob/53530427db2941ce784201e64086766504bc5642/charon/src/bin/charon-driver/translate/translate_ctx.rs#L344
@@ -564,7 +599,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         Ok(CharonName { name })
     }
 
-
     /// Compute the span information for the given instance
     fn translate_instance_span(&mut self, instance: Instance) -> CharonSpan {
         self.translate_span(instance.def.span())
@@ -605,7 +639,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         // TODO: populate `generated_from_span` info
         CharonSpan { span: rspan, generated_from_span: None }
     }
-        
 
     fn translate_function_signature(&mut self) -> CharonFunSig {
         let instance = self.instance;
@@ -673,71 +706,72 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         instance_internal.def.requires_caller_location(self.tcx())
     }
 
-/* 
-    fn generic_args_to_generic_params (&self, ga: GenericArgs) -> CharonGenericParams{
-        let genvec = ga.0;
-        let mut c_regions: CharonVector<CharonRegionId, CharonRegion> = CharonVector::new();
-        let mut c_types: CharonVector<CharonTypeVarId, CharonTy> = CharonVector::new();
-        let mut c_const_generics: CharonVector<CharonConstGenericVarId, CharonConstGeneric> =CharonVector::new();
-        //let mut  trait_refs: CharonVector<CharonTraitClauseId, CharonTraitRef> = CharonVector::new();
-        for genkind in genvec.iter(){
-            match *genkind{
-                GenericArgKind::Lifetime(region) => {
-                    let c_region = self.translate_region(region);
-                    c_regions.push(c_region);
-                }
-                GenericArgKind::Type(ty) => {
-                    let c_ty = self.translate_ty(ty);
-                    c_types.push(c_ty);
-                }
-                GenericArgKind::Const(tc ) => {
-                    let c_const_generic = self.tyconst_to_constgeneric(tc); 
-                    c_const_generics.push(c_const_generic);
-                }
-            }
-        }
-        CharonGenericParams{
-            regions : c_regions,
-            types : c_types,
-            const_generics : c_const_generics,
-            trait_clauses : CharonVector::new(),
-            regions_outlive : Vec::new(),
-            types_outlive : Vec::new(),
-            trait_type_constraints : Vec::new(),
-        }
-        }
-*/ 
-        
-    fn translate_generic_args (&mut self, ga: GenericArgs) -> CharonGenericArgs{
+    /*
+        fn generic_args_to_generic_params (&self, ga: GenericArgs) -> CharonGenericParams{
             let genvec = ga.0;
             let mut c_regions: CharonVector<CharonRegionId, CharonRegion> = CharonVector::new();
             let mut c_types: CharonVector<CharonTypeVarId, CharonTy> = CharonVector::new();
             let mut c_const_generics: CharonVector<CharonConstGenericVarId, CharonConstGeneric> =CharonVector::new();
             //let mut  trait_refs: CharonVector<CharonTraitClauseId, CharonTraitRef> = CharonVector::new();
             for genkind in genvec.iter(){
-                let gk = genkind.clone();
-                match gk{
+                match *genkind{
                     GenericArgKind::Lifetime(region) => {
                         let c_region = self.translate_region(region);
                         c_regions.push(c_region);
-                    },
+                    }
                     GenericArgKind::Type(ty) => {
                         let c_ty = self.translate_ty(ty);
                         c_types.push(c_ty);
-                    },
+                    }
                     GenericArgKind::Const(tc ) => {
-                        let c_const_generic = self.tyconst_to_constgeneric(tc); 
+                        let c_const_generic = self.tyconst_to_constgeneric(tc);
                         c_const_generics.push(c_const_generic);
                     }
                 }
             }
-            CharonGenericArgs{
+            CharonGenericParams{
                 regions : c_regions,
                 types : c_types,
                 const_generics : c_const_generics,
-                trait_refs : CharonVector::new(),
+                trait_clauses : CharonVector::new(),
+                regions_outlive : Vec::new(),
+                types_outlive : Vec::new(),
+                trait_type_constraints : Vec::new(),
+            }
+            }
+    */
+
+    fn translate_generic_args(&mut self, ga: GenericArgs) -> CharonGenericArgs {
+        let genvec = ga.0;
+        let mut c_regions: CharonVector<CharonRegionId, CharonRegion> = CharonVector::new();
+        let mut c_types: CharonVector<CharonTypeVarId, CharonTy> = CharonVector::new();
+        let mut c_const_generics: CharonVector<CharonConstGenericVarId, CharonConstGeneric> =
+            CharonVector::new();
+        //let mut  trait_refs: CharonVector<CharonTraitClauseId, CharonTraitRef> = CharonVector::new();
+        for genkind in genvec.iter() {
+            let gk = genkind.clone();
+            match gk {
+                GenericArgKind::Lifetime(region) => {
+                    let c_region = self.translate_region(region);
+                    c_regions.push(c_region);
+                }
+                GenericArgKind::Type(ty) => {
+                    let c_ty = self.translate_ty(ty);
+                    c_types.push(c_ty);
+                }
+                GenericArgKind::Const(tc) => {
+                    let c_const_generic = self.tyconst_to_constgeneric(tc);
+                    c_const_generics.push(c_const_generic);
+                }
             }
         }
+        CharonGenericArgs {
+            regions: c_regions,
+            types: c_types,
+            const_generics: c_const_generics,
+            trait_refs: CharonVector::new(),
+        }
+    }
 
     fn translate_ty(&mut self, ty: Ty) -> CharonTy {
         match ty.kind() {
@@ -750,7 +784,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         match tyconst.kind() {
             TyConstKind::Value(ty, alloc) => {
                 let c_raw_constexpr = self.translate_allocation(alloc, *ty);
-                let c_const_generic = translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap();
+                let c_const_generic =
+                    translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap();
                 c_const_generic
             }
             _ => todo!(),
@@ -765,9 +800,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             RigidTy::Int(it) => {
                 CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Integer(translate_int_ty(it))))
             }
-            RigidTy::Uint(uit) => {
-                CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Integer(translate_uint_ty(uit))))
-            }
+            RigidTy::Uint(uit) => CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Integer(
+                translate_uint_ty(uit),
+            ))),
             RigidTy::Never => CharonTy::new(CharonTyKind::Never),
             RigidTy::Str => CharonTy::new(CharonTyKind::Adt(
                 CharonTypeId::Builtin(CharonBuiltinTy::Str),
@@ -794,7 +829,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                         types: c_types,
                         const_generics: c_const_generics,
                         trait_refs: CharonVector::new(),
-                    }
+                    },
                 ))
             }
             RigidTy::Ref(region, ty, mutability) => CharonTy::new(CharonTyKind::Ref(
@@ -826,15 +861,15 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 // TODO: populate regions?
                 CharonTy::new(CharonTyKind::Arrow(CharonVector::new(), inputs, output))
             }
-            RigidTy::Adt(adt_def, genarg ) => {
-                let def_id  = adt_def.def_id();
+            RigidTy::Adt(adt_def, genarg) => {
+                let def_id = adt_def.def_id();
                 let c_typedeclid = self.register_type_decl_id(def_id);
                 if self.translated.type_decls.get(c_typedeclid).is_none() {
                     self.translate_adtdef(adt_def);
                 }
                 let c_generic_args = self.translate_generic_args(genarg);
                 CharonTy::new(CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), c_generic_args))
-                },
+            }
             _ => todo!(),
         }
     }
@@ -902,11 +937,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             TerminatorKind::Unreachable => {
                 (None, CharonRawTerminator::Abort(CharonAbortKind::UndefinedBehavior))
             }
-            TerminatorKind::Drop { place, target, .. } => {
-                (Some(CharonRawStatement::Drop(self.translate_place(&place))), CharonRawTerminator::Goto {
-                    target: CharonBlockId::from_usize(*target),
-                })
-            }
+            TerminatorKind::Drop { place, target, .. } => (
+                Some(CharonRawStatement::Drop(self.translate_place(&place))),
+                CharonRawTerminator::Goto { target: CharonBlockId::from_usize(*target) },
+            ),
             TerminatorKind::SwitchInt { discr, targets } => {
                 let (discr, targets) = self.translate_switch_targets(discr, targets);
                 (None, CharonRawTerminator::Switch { discr, targets })
@@ -968,7 +1002,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         CharonPlace { var_id, projection }
     }
 
-    fn place_ty (&self, place: &Place) -> Ty {
+    fn place_ty(&self, place: &Place) -> Ty {
         let body = self.instance.body().unwrap();
         let ty = body.local_decl(place.local).unwrap().ty;
         ty
@@ -1003,61 +1037,86 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 self.translate_operand(lhs),
                 self.translate_operand(rhs),
             ),
-            Rvalue::UnaryOp(op, operand) => CharonRvalue::UnaryOp(translate_un_op(*op), self.translate_operand(operand)),
+            Rvalue::UnaryOp(op, operand) => {
+                CharonRvalue::UnaryOp(translate_un_op(*op), self.translate_operand(operand))
+            }
             Rvalue::Discriminant(place) => {
                 let c_place = self.translate_place(place);
                 let ty = self.place_ty(place);
                 let c_ty = self.translate_ty(ty);
                 match c_ty.kind() {
-                    CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), _) => CharonRvalue::Discriminant(c_place, *c_typedeclid),
-                    _ => todo!()
-                }           
-            },
+                    CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), _) => {
+                        CharonRvalue::Discriminant(c_place, *c_typedeclid)
+                    }
+                    _ => todo!(),
+                }
+            }
 
             Rvalue::Aggregate(agg_kind, operands) => {
-                let c_operands = (*operands).iter().map(|operand| self.translate_operand(operand)).collect();
+                let c_operands =
+                    (*operands).iter().map(|operand| self.translate_operand(operand)).collect();
                 let akind = agg_kind.clone();
                 match akind {
-                    AggregateKind::Adt(adt_def, variant_id , gen_args , user_anot , field_id ) => {
+                    AggregateKind::Adt(adt_def, variant_id, gen_args, user_anot, field_id) => {
                         let adt_kind = adt_def.kind();
                         match adt_kind {
                             AdtKind::Enum => {
-                                let def_id = adt_def.def_id();                      
+                                let def_id = adt_def.def_id();
                                 let c_typedeclid: CharonTypeDeclId = self.find_type_decl_id(def_id);
                                 let c_type_id = CharonTypeId::Adt(c_typedeclid);
-                                let c_variant_id  = Some(CharonVariantId::from_usize(variant_id.to_index()));
+                                let c_variant_id =
+                                    Some(CharonVariantId::from_usize(variant_id.to_index()));
                                 let c_field_id = match field_id {
-                                    Some(fid) => Some (CharonFieldId::from_usize(fid)),
+                                    Some(fid) => Some(CharonFieldId::from_usize(fid)),
                                     None => None,
-                                };      
+                                };
                                 let c_generic_args = CharonGenericArgs::empty();
-                                let c_agg_kind = CharonAggregateKind::Adt(c_type_id, c_variant_id, c_field_id, c_generic_args);
+                                let c_agg_kind = CharonAggregateKind::Adt(
+                                    c_type_id,
+                                    c_variant_id,
+                                    c_field_id,
+                                    c_generic_args,
+                                );
                                 CharonRvalue::Aggregate(c_agg_kind, c_operands)
-                            },
+                            }
                             AdtKind::Struct => {
                                 let def_id = adt_def.def_id();
                                 let c_typedeclid: CharonTypeDeclId = self.find_type_decl_id(def_id);
                                 let c_type_id = CharonTypeId::Adt(c_typedeclid);
-                                let c_variant_id  = None;
+                                let c_variant_id = None;
                                 let c_field_id = None;
                                 let c_generic_args = CharonGenericArgs::empty();
-                                let c_agg_kind = CharonAggregateKind::Adt(c_type_id, c_variant_id, c_field_id, c_generic_args);
+                                let c_agg_kind = CharonAggregateKind::Adt(
+                                    c_type_id,
+                                    c_variant_id,
+                                    c_field_id,
+                                    c_generic_args,
+                                );
                                 CharonRvalue::Aggregate(c_agg_kind, c_operands)
-                            },
-                            _ =>todo!()
+                            }
+                            _ => todo!(),
                         }
-                    },
-                    AggregateKind::Tuple => CharonRvalue::Aggregate(CharonAggregateKind::Adt(CharonTypeId::Tuple, None, None, CharonGenericArgs::empty()), c_operands),
-                    AggregateKind::Array(ty)=> {
+                    }
+                    AggregateKind::Tuple => CharonRvalue::Aggregate(
+                        CharonAggregateKind::Adt(
+                            CharonTypeId::Tuple,
+                            None,
+                            None,
+                            CharonGenericArgs::empty(),
+                        ),
+                        c_operands,
+                    ),
+                    AggregateKind::Array(ty) => {
                         let c_ty = self.translate_ty(ty);
-                        let cg = CharonConstGeneric::Value(CharonLiteral::Scalar(CharonScalarValue::Usize(c_operands.len() as u64,)));
+                        let cg = CharonConstGeneric::Value(CharonLiteral::Scalar(
+                            CharonScalarValue::Usize(c_operands.len() as u64),
+                        ));
                         CharonRvalue::Aggregate(CharonAggregateKind::Array(c_ty, cg), c_operands)
                     }
                     _ => todo!(),
-                    }
-                },
+                }
+            }
 
-            
             Rvalue::ShallowInitBox(_, _) => todo!(),
             Rvalue::CopyForDeref(_) => todo!(),
             Rvalue::ThreadLocalRef(_) => todo!(),
@@ -1149,7 +1208,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let (value, bb) = targets.branches().last().unwrap();
             let (then_bb, else_bb) =
                 if value == 0 { (targets.otherwise(), bb) } else { (bb, targets.otherwise()) };
-            CharonSwitchTargets::If(CharonBlockId::from_usize(then_bb), CharonBlockId::from_usize(else_bb))
+            CharonSwitchTargets::If(
+                CharonBlockId::from_usize(then_bb),
+                CharonBlockId::from_usize(else_bb),
+            )
         } else {
             let CharonTyKind::Literal(CharonLiteralTy::Integer(int_ty)) = charon_ty.kind() else {
                 panic!("Expected integer type for switch discriminant");
@@ -1180,85 +1242,85 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         (discr, switch_targets)
     }
 
-    fn translate_projection(&mut self, place: &Place, projection: &[ProjectionElem]) -> Vec<CharonProjectionElem> {
+    fn translate_projection(
+        &mut self,
+        place: &Place,
+        projection: &[ProjectionElem],
+    ) -> Vec<CharonProjectionElem> {
         let c_place_ty = self.translate_ty(self.place_ty(place));
         let mut c_provec = Vec::new();
         let mut current_ty = c_place_ty.clone();
         let mut current_var: usize = 0;
-        for prj in projection.iter() {            
+        for prj in projection.iter() {
             match prj {
                 ProjectionElem::Deref => c_provec.push(CharonProjectionElem::Deref),
                 ProjectionElem::Field(fid, ty) => {
                     let c_fieldid = CharonFieldId::from_usize(*fid);
                     let c_variantid = CharonVariantId::from_usize(current_var);
                     match current_ty.kind() {
-                        CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => 
-                        {
+                        CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => {
                             let adttype = self.translated.type_decls.get(*tdid).unwrap();
                             match adttype.kind {
-                                CharonTypeDeclKind::Struct(_) => 
-                                    {
-                                        let c_fprj = CharonFieldProjKind::Adt(*tdid, None);
-                                        c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
-                                        let current_ty = ty.clone();
-                                    }                         
-                                CharonTypeDeclKind::Enum(_) => 
-                                    {
-                                        let c_fprj = CharonFieldProjKind::Adt(*tdid, Some(c_variantid));
-                                        c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
-                                        let current_ty = ty.clone();
-                                    }
-                                _ => (),}
-                        }                       
-                        CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => 
-                            {
-                                let c_fprj = CharonFieldProjKind::Tuple((*genargs).types.len());
-                                c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
-                                let current_ty = ty.clone();
+                                CharonTypeDeclKind::Struct(_) => {
+                                    let c_fprj = CharonFieldProjKind::Adt(*tdid, None);
+                                    c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
+                                    let current_ty = ty.clone();
+                                }
+                                CharonTypeDeclKind::Enum(_) => {
+                                    let c_fprj = CharonFieldProjKind::Adt(*tdid, Some(c_variantid));
+                                    c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
+                                    let current_ty = ty.clone();
+                                }
+                                _ => (),
                             }
-                        _ => ()
                         }
-                }
-                ProjectionElem::Downcast(varid) => 
-                    {
-                        let current_var = varid.to_index();
+                        CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => {
+                            let c_fprj = CharonFieldProjKind::Tuple((*genargs).types.len());
+                            c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
+                            let current_ty = ty.clone();
+                        }
+                        _ => (),
                     }
-                
-                _ => continue,
                 }
+                ProjectionElem::Downcast(varid) => {
+                    let current_var = varid.to_index();
+                }
+
+                _ => continue,
+            }
         }
         c_provec
     }
-/* 
-    fn translate_projection_elem(&mut self, place: &Place, projection_elem: &ProjectionElem) -> CharonProjectionElem {
-        match projection_elem {
-            ProjectionElem::Deref => CharonProjectionElem::Deref,
-            /* 
-            ProjectionElem::Downcast(varid) => {
-                let c_varid = CharonVariantId::from_usize((*varid).to_index());
-                let c_place_ty = self.translate_ty(self.place_ty(place));
-                let c_typedeclid =  *match c_place_ty.kind() {
-                    CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => tdid,
-                    _ => todo!()
-                };   
-                let c_fprj = CharonFieldProjKind::Adt(c_typedeclid, Some(c_varid));
-                let c_fieldid = CharonFieldId::from_usize(0);
-                CharonProjectionElem::Field(c_fprj,c_fieldid)
-            },*/
-            ProjectionElem::Field(fid, ty, ) =>{
-                let c_fieldid = CharonFieldId::from_usize(*fid);
-                let c_place_ty = self.translate_ty(self.place_ty(place));
-                let c_fprj = match c_place_ty.kind() {
-                    CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => CharonFieldProjKind::Adt(*tdid, None),
-                    CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => CharonFieldProjKind::Tuple((*genargs).types.len()),
-                    _ => todo!()
-                };
-                CharonProjectionElem::Field(c_fprj, c_fieldid)
+    /*
+        fn translate_projection_elem(&mut self, place: &Place, projection_elem: &ProjectionElem) -> CharonProjectionElem {
+            match projection_elem {
+                ProjectionElem::Deref => CharonProjectionElem::Deref,
+                /*
+                ProjectionElem::Downcast(varid) => {
+                    let c_varid = CharonVariantId::from_usize((*varid).to_index());
+                    let c_place_ty = self.translate_ty(self.place_ty(place));
+                    let c_typedeclid =  *match c_place_ty.kind() {
+                        CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => tdid,
+                        _ => todo!()
+                    };
+                    let c_fprj = CharonFieldProjKind::Adt(c_typedeclid, Some(c_varid));
+                    let c_fieldid = CharonFieldId::from_usize(0);
+                    CharonProjectionElem::Field(c_fprj,c_fieldid)
+                },*/
+                ProjectionElem::Field(fid, ty, ) =>{
+                    let c_fieldid = CharonFieldId::from_usize(*fid);
+                    let c_place_ty = self.translate_ty(self.place_ty(place));
+                    let c_fprj = match c_place_ty.kind() {
+                        CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => CharonFieldProjKind::Adt(*tdid, None),
+                        CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => CharonFieldProjKind::Tuple((*genargs).types.len()),
+                        _ => todo!()
+                    };
+                    CharonProjectionElem::Field(c_fprj, c_fieldid)
+                }
+                _ => todo!(),
             }
-            _ => todo!(),
         }
-    }
-*/
+    */
 
     fn translate_region(&self, region: Region) -> CharonRegion {
         match region.kind {
@@ -1321,18 +1383,14 @@ fn translate_bin_op(bin_op: BinOp) -> CharonBinOp {
     }
 }
 
-
-
 fn translate_un_op(un_op: UnOp) -> CharonUnOp {
     match un_op {
         UnOp::Not => CharonUnOp::Not,
         UnOp::Neg => CharonUnOp::Neg,
-        UnOp::PtrMetadata => todo!()
+        UnOp::PtrMetadata => todo!(),
     }
-
 }
 
-
 fn translate_borrow_kind(kind: &BorrowKind) -> CharonBorrowKind {
     match kind {
         BorrowKind::Shared => CharonBorrowKind::Shared,
@@ -1347,7 +1405,6 @@ fn translate_constant_expr_to_const_generic(
     match value {
         CharonRawConstantExpr::Literal(v) => Ok(CharonConstGeneric::Value(v)),
         CharonRawConstantExpr::Var(v) => Ok(CharonConstGeneric::Var(v)),
-        _ => todo!()
-        }    
+        _ => todo!(),
     }
-
+}
diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs
index cbd1e0a3a253..410cf1848d44 100644
--- a/tests/expected/llbc/basic0/test.rs
+++ b/tests/expected/llbc/basic0/test.rs
@@ -12,4 +12,4 @@ fn is_zero(i: i32) -> bool {
 #[kani::proof]
 fn main() {
     let _ = is_zero(0);
-}
\ No newline at end of file
+}
diff --git a/tests/expected/llbc/enum_test/test.rs b/tests/expected/llbc/enum_test/test.rs
index c271275fa9c0..ee5c75e4b780 100644
--- a/tests/expected/llbc/enum_test/test.rs
+++ b/tests/expected/llbc/enum_test/test.rs
@@ -4,22 +4,18 @@
 
 //! This test checks that Kani's LLBC backend handles simple enum
 
-
 enum MyEnum {
     A(i32),
     B,
 }
 
-
 fn enum_match(e: MyEnum) -> i32 {
     match e {
-        MyEnum::A(i) => i ,
-        MyEnum::B => 0 ,
+        MyEnum::A(i) => i,
+        MyEnum::B => 0,
     }
 }
 
-
-
 #[kani::proof]
 fn main() {
     let e = MyEnum::A(1);
diff --git a/tests/expected/llbc/projection_test/test.rs b/tests/expected/llbc/projection_test/test.rs
index 22440d7a9986..79b9382e34d2 100644
--- a/tests/expected/llbc/projection_test/test.rs
+++ b/tests/expected/llbc/projection_test/test.rs
@@ -14,19 +14,16 @@ enum MyEnum {
     B,
 }
 
-
 fn enum_match(e: MyEnum) -> i32 {
     match e {
         MyEnum::A(s, i) => s.a + i,
-        MyEnum::B => 0 ,
+        MyEnum::B => 0,
     }
 }
 
-
-
 #[kani::proof]
 fn main() {
     let s = MyStruct { a: 1, b: 2 };
-    let e = MyEnum::A(s,1);
+    let e = MyEnum::A(s, 1);
     let i = enum_match(e);
 }
diff --git a/tests/expected/llbc/struct_test/test.rs b/tests/expected/llbc/struct_test/test.rs
index 14c9bac45258..f9365de1888e 100644
--- a/tests/expected/llbc/struct_test/test.rs
+++ b/tests/expected/llbc/struct_test/test.rs
@@ -4,7 +4,7 @@
 
 //! This test checks that Kani's LLBC backend handles simple struct
 
-struct MyStruct{
+struct MyStruct {
     a: i32,
     b: bool,
 }
diff --git a/tests/expected/llbc/tuple_test/test.rs b/tests/expected/llbc/tuple_test/test.rs
index 4a2a2cc87141..16b054a02cc7 100644
--- a/tests/expected/llbc/tuple_test/test.rs
+++ b/tests/expected/llbc/tuple_test/test.rs
@@ -4,7 +4,7 @@
 
 //! This test checks that Kani's LLBC backend handles simple tuple
 
-fn tuple_add (t: (i32, i32)) -> i32 {
+fn tuple_add(t: (i32, i32)) -> i32 {
     t.0 + t.1
 }
 

From cebeff5f6175f7fd9d13acb20d4951da75eff3e7 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Fri, 15 Nov 2024 11:52:43 -0800
Subject: [PATCH 4/4] edit according to clippy suggestions

---
 .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs   | 47 ++++++++++---------
 1 file changed, 26 insertions(+), 21 deletions(-)

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 021cea6444eb..13e6eb4fbaf9 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
@@ -7,7 +7,7 @@
 //! unstructured low-level borrow calculus (ULLBC)
 
 use core::panic;
-use std::any::Any;
+//use std::any::Any;
 //use std::ascii::Char;
 use std::path::PathBuf;
 
@@ -64,8 +64,8 @@ use charon_lib::ullbc_ast::{
 };
 use charon_lib::{error_assert, error_or_panic};
 use rustc_data_structures::fx::FxHashMap;
-use rustc_data_structures::stable_hasher::HashStable;
-use rustc_middle::ty::AdtKind as MirAdtKind;
+//use rustc_data_structures::stable_hasher::HashStable;
+//use rustc_middle::ty::AdtKind as MirAdtKind;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::abi::PassMode;
@@ -82,11 +82,11 @@ use stable_mir::ty::AdtDef;
 use stable_mir::ty::AdtKind;
 use stable_mir::ty::{
     Allocation, ConstantKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span,
-    TraitDef, Ty, TyConst, TyConstId, TyConstKind, TyKind, UintTy,
+    Ty, TyConst, TyConstKind, TyKind, UintTy,
 };
 use stable_mir::ty::{GenericArgKind, GenericArgs};
 use stable_mir::{CrateDef, DefId};
-use syn::token::Default;
+//use syn::token::Default;
 use tracing::{debug, trace};
 
 /// A context for translating a single MIR function to ULLBC.
@@ -187,12 +187,14 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         tid.try_into().unwrap()
     }
 
+    /* 
     fn find_fun_decl_id(&self, def_id: DefId) -> CharonFunDeclId {
         debug!("register_fun_decl_id: {:?}", def_id);
         let tid = *self.id_map.get(&def_id).unwrap();
         debug!("register_fun_decl_id: {:?}", self.id_map);
         tid.try_into().unwrap()
     }
+    */
 
     fn register_type_decl_id(&mut self, def_id: DefId) -> CharonTypeDeclId {
         debug!("register_type_decl_id: {:?}", def_id);
@@ -262,7 +264,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     let c_discr = self.get_discriminant(discr_val, discr_ty);
 
                     let c_variant = CharonVariant {
-                        span: span,
+                        span,
                         attr_info: CharonAttrInfo {
                             attributes: Vec::new(),
                             inline: None,
@@ -281,7 +283,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     def_id: c_typedeclid,
                     generics: CharonGenericParams::empty(),
                     kind: CharonTypeDeclKind::Enum(c_variants),
-                    item_meta: item_meta,
+                    item_meta,
                 };
                 self.translated.type_decls.set_slot(c_typedeclid, typedecl);
                 c_typedeclid
@@ -314,7 +316,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     def_id: c_typedeclid,
                     generics: CharonGenericParams::empty(),
                     kind: CharonTypeDeclKind::Struct(c_fields),
-                    item_meta: item_meta,
+                    item_meta,
                 };
                 self.translated.type_decls.set_slot(c_typedeclid, typedecl);
                 c_typedeclid
@@ -626,6 +628,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         CharonSpan { span: rspan, generated_from_span: None }
     }
 
+/*    
     fn translate_span_immut(&self, span: Span) -> CharonSpan {
         let filename = CharonFileName::Local(PathBuf::from(span.get_filename()));
         let file_id = *self.translated.file_to_id.get(&filename).unwrap();
@@ -639,6 +642,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         // TODO: populate `generated_from_span` info
         CharonSpan { span: rspan, generated_from_span: None }
     }
+*/ 
 
     fn translate_function_signature(&mut self) -> CharonFunSig {
         let instance = self.instance;
@@ -784,9 +788,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         match tyconst.kind() {
             TyConstKind::Value(ty, alloc) => {
                 let c_raw_constexpr = self.translate_allocation(alloc, *ty);
-                let c_const_generic =
-                    translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap();
-                c_const_generic
+                //let c_const_generic =
+                    //translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap();
+                translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap()
             }
             _ => todo!(),
         }
@@ -1057,7 +1061,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     (*operands).iter().map(|operand| self.translate_operand(operand)).collect();
                 let akind = agg_kind.clone();
                 match akind {
-                    AggregateKind::Adt(adt_def, variant_id, gen_args, user_anot, field_id) => {
+                    AggregateKind::Adt(adt_def, variant_id, _gen_args, _user_anot, field_id) => {
                         let adt_kind = adt_def.kind();
                         match adt_kind {
                             AdtKind::Enum => {
@@ -1066,10 +1070,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                                 let c_type_id = CharonTypeId::Adt(c_typedeclid);
                                 let c_variant_id =
                                     Some(CharonVariantId::from_usize(variant_id.to_index()));
-                                let c_field_id = match field_id {
-                                    Some(fid) => Some(CharonFieldId::from_usize(fid)),
-                                    None => None,
-                                };
+                                //let c_field_id = match field_id {
+                                //    Some(fid) => Some(CharonFieldId::from_usize(fid)),
+                                //    None => None,
+                                //};
+                                let c_field_id = field_id.map(CharonFieldId::from_usize);
                                 let c_generic_args = CharonGenericArgs::empty();
                                 let c_agg_kind = CharonAggregateKind::Adt(
                                     c_type_id,
@@ -1264,26 +1269,26 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                                 CharonTypeDeclKind::Struct(_) => {
                                     let c_fprj = CharonFieldProjKind::Adt(*tdid, None);
                                     c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
-                                    let current_ty = ty.clone();
+                                    current_ty = self.translate_ty(*ty);
                                 }
                                 CharonTypeDeclKind::Enum(_) => {
                                     let c_fprj = CharonFieldProjKind::Adt(*tdid, Some(c_variantid));
                                     c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
-                                    let current_ty = ty.clone();
+                                    current_ty = self.translate_ty(*ty);
                                 }
                                 _ => (),
                             }
                         }
                         CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => {
-                            let c_fprj = CharonFieldProjKind::Tuple((*genargs).types.len());
+                            let c_fprj = CharonFieldProjKind::Tuple(genargs.types.len());
                             c_provec.push(CharonProjectionElem::Field(c_fprj, c_fieldid));
-                            let current_ty = ty.clone();
+                            current_ty = self.translate_ty(*ty);
                         }
                         _ => (),
                     }
                 }
                 ProjectionElem::Downcast(varid) => {
-                    let current_var = varid.to_index();
+                    current_var = varid.to_index();
                 }
 
                 _ => continue,