Merge remote-tracking branch 'origin/main' into son/clean

40 files changed, 310 insertions, 130 deletions

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index a57f8bb1..5a85dff0 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -3,7 +3,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 -- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
 --import Mathlib.Tactic.Omega
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index c9a2eec2..92ffd3cd 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.Diverge.Base
 import Base.Diverge.Elab
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 717a3e64..0f20125f 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
 import Base.Arith.Base
@@ -39,8 +38,7 @@ namespace Lemmas
     case zero =>
       simp_all
       intro m h1 h2
-      have h: n = m := by
-        linarith
+      have h: n = m := by omega
       unfold for_all_fin_aux; simp_all
       simp_all
       -- There is no i s.t. m ≤ i
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index d2dc3922..5db8ffed 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Base.Utils
 import Base.Diverge.Base
 import Base.Diverge.ElabBase
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index ef658e1b..91ca7284 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
@@ -269,7 +268,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
       . scalar_tac
       . scalar_tac
     let na := s_beg.append (s.val.append s_end)
-    have : na.len = a.val.len := by simp [*]
+    have : na.len = a.val.len := by simp [na, *]
     ok ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
@@ -343,7 +342,7 @@ def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : S
       . scalar_tac
       . scalar_tac
     let ns := s_beg.append (ss.val.append s_end)
-    have : ns.len = s.val.len := by simp [*]
+    have : ns.len = s.val.len := by simp [ns, *]
     ok ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean
index a268bcba..416cd201 100644
--- a/backends/lean/Base/Primitives/Range.lean
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index c298ba92..98d695a4 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -265,6 +265,14 @@ theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty
   have := Scalar.cMax_bound ty
   linarith
 
+/-- The scalar type.
+
+    We could use a subtype, but it using a custom structure type allows us
+    to have more control over the coercions and the simplifications (we tried
+    using a subtype and it caused issues especially as we had to make the Scalar
+    type non-reducible, so that we could have more control, but leading to
+    some natural equalities not being obvious to the simplifier anymore).
+ -/
 structure Scalar (ty : ScalarTy) where
   val : Int
   hmin : Scalar.min ty ≤ val
@@ -274,6 +282,9 @@ deriving Repr
 instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
   coe := λ v => v.val
 
+/- Activate the ↑ notation -/
+attribute [coe] Scalar.val
+
 theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty ->
   Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
@@ -1117,19 +1128,19 @@ theorem Scalar.eq_equiv {ty : ScalarTy} (x y : Scalar ty) :
 
 -- This is sometimes useful when rewriting the goal with the local assumptions
 @[simp] theorem Scalar.eq_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x = y → (↑x : Int) = ↑y := (eq_equiv x y).mp
+  (↑x : Int) = ↑y → x = y := (eq_equiv x y).mpr
 
 theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x < y ↔ (↑x : Int) < ↑y := by simp [LT.lt]
 
 @[simp] theorem Scalar.lt_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x < y → (↑x : Int) < ↑y := (lt_equiv x y).mp
+  (↑x : Int) < (↑y) → x < y := (lt_equiv x y).mpr
 
 theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x ≤ y ↔ (↑x : Int) ≤ ↑y := by simp [LE.le]
 
 @[simp] theorem Scalar.le_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x ≤ y → (↑x : Int) ≤ ↑y := (le_equiv x y).mp
+  (↑x : Int) ≤ ↑y → x ≤ y := (le_equiv x y).mpr
 
 instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt ..
 instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe ..
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index dbe5c8dd..8e2d65a8 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 3a18466f..99ec856e 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.27",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "056cc4b21e25e8d1daaeef3a6e3416872c9fc12c",
+   "rev": "3e99b48baf21ffdd202d5c2e39990fc23f4c6d32",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index f96d662e..9ad30404 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0
diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 53e56c44..30887593 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,6 +1,7 @@
 let log = Logging.errors_log
 
-let meta_to_string (span : Meta.span) =
+let meta_to_string (meta : Meta.meta) =
+  let span = meta.span in
   let file = match span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -10,7 +11,7 @@ let meta_to_string (span : Meta.span) =
 
 let format_error_message (meta : Meta.meta option) (msg : string) =
   let meta =
-    match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta.span
+    match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta
   in
   msg ^ meta
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 27e9a62c..6eeef772 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
           ^ string_of_int (List.length types)
           ^ " type arguments"
         in
-        log#serror err;
+        save_error __FILE__ __LINE__ None err;
         Result.Error (types, err))
       else
         let types = List.combine filter types in
@@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta)
     - application argument: [f (exp)]
     - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
  *)
+
+let extract_texpression_errors (fmt : F.formatter) =
+  match !Config.backend with
+  | FStar | Coq -> F.pp_print_string fmt "admit"
+  | Lean -> F.pp_print_string fmt "sorry"
+  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
 let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (e : texpression) : unit =
   match e.e with
@@ -323,6 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
   | Loop _ ->
       (* The loop nodes should have been eliminated in {!PureMicroPasses} *)
       craise __FILE__ __LINE__ meta "Unreachable"
+  | EError (_, _) -> extract_texpression_errors fmt
 
 (* Extract an application *or* a top-level qualif (function extraction has
  * to handle top-level qualifiers, so it seemed more natural to merge the
@@ -1871,7 +1879,7 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
     [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl}
     and {!extract_fun_decl}.
  *)
-let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
     (global : global_decl) (body : fun_decl) (interface : bool) : unit =
   let meta = body.meta in
   sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
@@ -1966,6 +1974,12 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
       (* Add a break to insert lines between declarations *)
       F.pp_print_break fmt 0 0
 
+let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+  match global with
+  | Some global -> extract_global_decl_aux ctx fmt global body interface
+  | None -> ()
+
 (** Similar to {!extract_trait_decl_register_names} *)
 let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8b17591e..656d2f27 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -259,7 +259,7 @@ let report_name_collision (id_to_string : id -> string)
   let meta_to_string (meta : Meta.meta option) =
     match meta with
     | None -> ""
-    | Some meta -> "\n  " ^ Errors.meta_to_string meta.span
+    | Some meta -> "\n  " ^ Errors.meta_to_string meta
   in
   let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
   let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
@@ -1719,7 +1719,8 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
       | TLiteral lty -> (
           match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
       | TArrow _ -> "f"
-      | TTraitType (_, name) -> name_from_type_ident name)
+      | TTraitType (_, name) -> name_from_type_ident name
+      | Error -> "x")
 
 (** Generates a type variable basename. *)
 let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 1f0abf8a..1c3657a3 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -433,6 +433,13 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
       End
     ]}
  *)
+
+let extract_ty_errors (fmt : F.formatter) : unit =
+  match !Config.backend with
+  | FStar | Coq -> F.pp_print_string fmt "admit"
+  | Lean -> F.pp_print_string fmt "sorry"
+  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
 let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
   let extract_rec = extract_ty meta ctx fmt no_params_tys in
@@ -566,6 +573,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
               "Trait types are not supported yet when generating code for HOL4";
             extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
+  | Error -> extract_ty_errors fmt
 
 and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index a65e1663..769e3144 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -191,6 +191,18 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
    * do it, and because it gives a bit of sanity.
    * *)
   let sg = fdef.signature in
+  (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+       (sg.output :: sg.inputs))
+    fdef.meta "Nested borrows are not supported yet";
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
+       (sg.output :: sg.inputs))
+    fdef.meta "ADTs containing borrows are not supported yet";
+
   (* Create the context *)
   let regions_hierarchy =
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
@@ -612,7 +624,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
   (* Evaluate the function *)
   let symbolic =
-    eval_function_body config (Option.get fdef.body).body cf_finish ctx
+    try eval_function_body config (Option.get fdef.body).body cf_finish ctx
+    with CFailure (meta, msg) -> Some (Error (meta, msg))
   in
 
   (* Return *)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e593ae75..a158ed9a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -303,13 +303,11 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
             if bid' = bid then (
               (* Sanity check *)
               let expected_ty = ty in
-              if nv.ty <> expected_ty then (
-                log#serror
-                  ("give_back_value: improper type:\n- expected: "
-                 ^ ty_to_string ctx ty ^ "\n- received: "
-                 ^ ty_to_string ctx nv.ty);
+              if nv.ty <> expected_ty then
                 craise __FILE__ __LINE__ meta
-                  "Value given back doesn't have the proper type");
+                  ("Value given back doesn't have the proper type:\n\
+                    - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
+                 ^ ty_to_string ctx nv.ty);
               (* Replace *)
               set_replaced ();
               nv.value)
@@ -540,13 +538,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                * see the comment at the level of the definition of
                * {!typed_avalue} *)
               let _, expected_ty, _ = ty_get_ref ty in
-              if nv.ty <> expected_ty then (
-                log#serror
-                  ("give_back_avalue_to_same_abstraction: improper type:\n\
+              if nv.ty <> expected_ty then
+                craise __FILE__ __LINE__ meta
+                  ("Value given back doesn't have the proper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                craise __FILE__ __LINE__ meta
-                  "Value given back doesn't have the proper type");
               (* This is the loan we are looking for: apply the projection to
                * the value we give back and replaced this mutable loan with
                * an ended loan *)
@@ -836,26 +832,26 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
       match lookup_borrow_opt ek_all l ctx with
       | None -> () (* Ok *)
       | Some _ ->
-          log#lerror
+          log#ltrace
             (lazy
               (fun_name ^ ": " ^ BorrowId.to_string l
              ^ ": borrow didn't disappear:\n- original context:\n"
               ^ eval_ctx_to_string ~meta:(Some meta) ctx0
               ^ "\n\n- new context:\n"
               ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-          craise __FILE__ __LINE__ meta "Borrow not eliminated"
+          internal_error __FILE__ __LINE__ meta
     in
     match lookup_loan_opt meta ek_all l ctx with
     | None -> () (* Ok *)
     | Some _ ->
-        log#lerror
+        log#ltrace
           (lazy
             (fun_name ^ ": " ^ BorrowId.to_string l
            ^ ": loan didn't disappear:\n- original context:\n"
             ^ eval_ctx_to_string ~meta:(Some meta) ctx0
             ^ "\n\n- new context:\n"
             ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-        craise __FILE__ __LINE__ meta "Loan not eliminated"
+        internal_error __FILE__ __LINE__ meta
   in
   unit_to_cm_fun check_disappeared
 
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 6e65b11d..a01be046 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -162,11 +162,11 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
       sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
       default
   | _ ->
-      log#lerror
+      log#ltrace
         (lazy
           ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1
          ^ "\n- ty2: " ^ show_ty ty2));
-      craise __FILE__ __LINE__ meta "Unreachable"
+      internal_error __FILE__ __LINE__ meta
 
 (** Check if two different projections intersect. This is necessary when
     giving a symbolic value to an abstraction: we need to check that
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 48a1cce6..5f849230 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -146,7 +146,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
             "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
           sanity_check __FILE__ __LINE__
-            (allow_adt_copy || ty_is_primitively_copyable ty)
+            (allow_adt_copy || ty_is_copyable ty)
             meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
@@ -157,9 +157,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               const_generics = [];
               trait_refs = [];
             } ) ->
-          exec_assert __FILE__ __LINE__
-            (ty_is_primitively_copyable ty)
-            meta "The type is not primitively copyable"
+          exec_assert __FILE__ __LINE__ (ty_is_copyable ty) meta
+            "The type is not primitively copyable"
       | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
@@ -195,7 +194,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
       cassert __FILE__ __LINE__
-        (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty))
+        (ty_is_copyable (Substitute.erase_regions sp.sv_ty))
         meta "Not primitively copyable";
       (* If the type is copyable, we simply return the current value. Side
        * remark: what is important to look at when copying symbolic values
@@ -528,9 +527,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
     exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta
       "The arguments given to the binop don't have the same type";
     (* Equality/inequality check is primitive only for a subset of types *)
-    exec_assert __FILE__ __LINE__
-      (ty_is_primitively_copyable v1.ty)
-      meta "Type is not primitively copyable";
+    exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
+      "Type is not primitively copyable";
     let b = v1 = v2 in
     Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
   else
@@ -621,9 +619,8 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
         (* Equality operations *)
         sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
         (* Equality/inequality check is primitive only for a subset of types *)
-        exec_assert __FILE__ __LINE__
-          (ty_is_primitively_copyable v1.ty)
-          meta "The type is not primitively copyable";
+        exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
+          "The type is not primitively copyable";
         TLiteral TBool)
       else
         (* Other operations: input types are integers *)
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index f2c0bcb1..ab3daa72 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -83,7 +83,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
       let nv = update v in
       (* Type checking *)
       if nv.ty <> v.ty then (
-        log#lerror
+        log#ltrace
           (lazy
             ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
            ^ show_ety v.ty));
@@ -252,8 +252,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
           let pe = "- pe: " ^ show_projection_elem pe in
           let v = "- v:\n" ^ show_value v in
           let ty = "- ty:\n" ^ show_ety ty in
-          log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
-          craise __FILE__ __LINE__ meta "Inconsistent projection")
+          craise __FILE__ __LINE__ meta
+            ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
 
 (** Generic function to access (read/write) the value at a given place.
 
@@ -319,14 +319,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
-      if !Config.sanity_checks then
-        if ctx1 <> ctx then (
-          let msg =
-            "Unexpected environment update:\nNew environment:\n"
-            ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
-          in
-          log#serror msg;
-          craise __FILE__ __LINE__ meta "Unexpected environment update");
+      (if !Config.sanity_checks then
+         if ctx1 <> ctx then
+           let msg =
+             "Unexpected environment update:\nNew environment:\n"
+             ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
+           in
+           craise __FILE__ __LINE__ meta msg);
       Ok read_value
 
 let read_place (meta : Meta.meta) (access : access_kind) (p : place)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 6e86e6a4..3993d845 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -217,12 +217,12 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
               meta);
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
-          log#lerror
+          log#ltrace
             (lazy
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
               ^ typed_value_to_string ~meta:(Some meta) ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
-          craise __FILE__ __LINE__ meta "Unreachable"
+          internal_error __FILE__ __LINE__ meta
     in
     { value; ty }
 
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 1cf1c5ef..de89f316 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1365,10 +1365,21 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
   let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg =
     eval_transparent_function_call_symbolic_inst meta call ctx
   in
-  (* Sanity check *)
+  (* Sanity check: same number of inputs *)
   sanity_check __FILE__ __LINE__
     (List.length call.args = List.length def.signature.inputs)
     def.meta;
+  (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+       (inst_sg.output :: inst_sg.inputs))
+    meta "Nested borrows are not supported yet";
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
+       (inst_sg.output :: inst_sg.inputs))
+    meta "ADTs containing borrows are not supported yet";
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config def.meta func def.signature
     regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 642d7a37..689db0c4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
           "find_info: could not find the representant of borrow "
           ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
         in
-        log#serror err;
         craise __FILE__ __LINE__ meta err
   in
 
@@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
         | AIgnored, _ -> ()
         | _ ->
-            log#lerror
+            log#ltrace
               (lazy
                 ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
                ^ "\n- value: "
                 ^ typed_avalue_to_string ~meta:(Some meta) ctx atv
                 ^ "\n- type: " ^ ty_to_string ctx atv.ty));
-            craise __FILE__ __LINE__ meta "Erroneous typing");
+            internal_error __FILE__ __LINE__ meta);
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
     end
@@ -826,9 +825,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
      * it must be expanded first *)
     if ty_has_borrows ctx.type_ctx.type_infos info.ty then
       sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
-    (* A duplicated symbolic value is necessarily primitively copyable *)
+    (* A duplicated symbolic value is necessarily copyable *)
     sanity_check __FILE__ __LINE__
-      (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
+      (info.env_count <= 1 || ty_is_copyable info.ty)
       meta;
 
     sanity_check __FILE__ __LINE__
diff --git a/compiler/Main.ml b/compiler/Main.ml
index db200f37..6161f2f2 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -274,12 +274,19 @@ let () =
 
          (* Translate the functions *)
          Aeneas.Translate.translate_crate filename dest_dir m
-       with Errors.CFailure (meta, msg) ->
+       with Errors.CFailure (_, _) ->
          (* In theory it shouldn't happen, but there may be uncaught errors -
             note that we let the [Failure] exceptions go through (they are
             send if we use the option [-abort-on-error] *)
-         log#serror (Errors.format_error_message meta msg);
-         exit 1);
+         ());
+
+      if !Errors.error_list <> [] then (
+        List.iter
+          (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg))
+          (* Reverse the list of error messages so that we print them from the
+             earliest to the latest. *)
+          (List.rev !Errors.error_list);
+        exit 1);
 
       (* Print total elapsed time *)
       log#linfo
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 0b39f64a..a46ef79c 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -238,9 +238,9 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
       method! visit_Sequence env st1 st2 =
         match st1.content with
         | Loop _ ->
-            sanity_check __FILE__ __LINE__
+            cassert __FILE__ __LINE__
               (statement_has_no_loop_break_continue st2)
-              st2.meta;
+              st2.meta "Sequences of loops are not supported yet";
             (replace_breaks_with st1 st2).content
         | _ -> super#visit_Sequence env st1 st2
     end
@@ -437,9 +437,22 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
 
 let apply_passes (crate : crate) : crate =
   let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
+  (* Attempt to apply a pass: if it fails we replace the body by [None] *)
+  let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
+    try pass f
+    with CFailure (_, _) ->
+      (* The error was already registered, we don't need to register it twice.
+         However, we replace the body of the function, and save an error to
+         report to the user the fact that we will ignore the function body *)
+      let fmt = Print.Crate.crate_to_fmt_env crate in
+      let name = Print.name_to_string fmt f.name in
+      save_error __FILE__ __LINE__ (Some f.meta)
+        ("Ignoring the body of '" ^ name ^ "' because of previous error");
+      { f with body = None }
+  in
   let fun_decls =
     List.fold_left
-      (fun fl pass -> FunDeclId.Map.map pass fl)
+      (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl)
       crate.fun_decls passes
   in
   let crate = { crate with fun_decls } in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dad1aea3..51286553 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,4 +1,5 @@
 include Charon.PrintUtils
+include Charon.PrintTypes
 include Charon.PrintLlbcAst
 open Charon.PrintTypes
 open Charon.PrintExpressions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 43ec083e..db9c583d 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -164,6 +164,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
       let trait_ref = trait_ref_to_string env false trait_ref in
       let s = trait_ref ^ "::" ^ type_name in
       if inside then "(" ^ s ^ ")" else s
+  | Error -> "@Error"
 
 and generic_args_to_strings (env : fmt_env) (inside : bool)
     (generics : generic_args) : string list =
@@ -615,6 +616,7 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None)
           let e = meta_s ^ "\n" ^ indent ^ e in
           if inside then "(" ^ e ^ ")" else e
       | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
+  | EError (_, _) -> "@Error"
 
 and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
     (inside : bool) (indent : string) (indent_incr : string) (app : texpression)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index daf213cf..451767f8 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -285,6 +285,7 @@ type ty =
   | TArrow of ty * ty
   | TTraitType of trait_ref * string
       (** The string is for the name of the associated type *)
+  | Error
 
 and trait_ref = {
   trait_id : trait_instance_id;
@@ -621,6 +622,7 @@ class ['self] iter_expression_base =
     method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
     method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> ()
     method visit_field_id : 'env -> field_id -> unit = fun _ _ -> ()
+    method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for {!map_expression} visitor *)
@@ -632,6 +634,7 @@ class ['self] map_expression_base =
     method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
     method visit_loop_id : 'env -> loop_id -> loop_id = fun _ x -> x
     method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x
+    method visit_meta : 'env -> Meta.meta -> Meta.meta = fun _ x -> x
   end
 
 (** Ancestor for {!reduce_expression} visitor *)
@@ -643,6 +646,7 @@ class virtual ['self] reduce_expression_base =
     method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
     method visit_loop_id : 'env -> loop_id -> 'a = fun _ _ -> self#zero
     method visit_field_id : 'env -> field_id -> 'a = fun _ _ -> self#zero
+    method visit_meta : 'env -> Meta.meta -> 'a = fun _ _ -> self#zero
   end
 
 (** Ancestor for {!mapreduce_expression} visitor *)
@@ -662,6 +666,9 @@ class virtual ['self] mapreduce_expression_base =
 
     method visit_field_id : 'env -> field_id -> field_id * 'a =
       fun _ x -> (x, self#zero)
+
+    method visit_meta : 'env -> Meta.meta -> Meta.meta * 'a =
+      fun _ x -> (x, self#zero)
   end
 
 (** **Rk.:** here, {!expression} is not at all equivalent to the expressions
@@ -726,6 +733,7 @@ type expression =
   | Loop of loop  (** See the comments for {!loop} *)
   | StructUpdate of struct_update  (** See the comments for {!struct_update} *)
   | Meta of (emeta[@opaque]) * texpression  (** Meta-information *)
+  | EError of Meta.meta option * string
 
 and switch_body = If of texpression * texpression | Match of match_branch list
 and match_branch = { pat : typed_pattern; branch : texpression }
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b1c85d61..004ecfef 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -416,6 +416,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | StructUpdate supd -> update_struct_update supd ctx
       | Lambda (lb, e) -> update_lambda lb e ctx
       | Meta (meta, e) -> update_emeta meta e ctx
+      | EError (meta, msg) -> (ctx, EError (meta, msg))
     in
     (ctx, { e; ty })
   (* *)
@@ -1006,7 +1007,8 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
         match e with
         | Var _ | CVar _ | Const _ | App _ | Qualif _
         | Meta (_, _)
-        | StructUpdate _ | Lambda _ ->
+        | StructUpdate _ | Lambda _
+        | EError (_, _) ->
             super#visit_expression env e
         | Switch (scrut, switch) -> (
             match switch with
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 9eed76b2..c1da4019 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -93,12 +93,11 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx)
         get_adt_field_types meta ctx.type_decls type_id av.variant_id generics
       in
       let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
-        if ty <> v.ty then (
+        if ty <> v.ty then
           (* TODO: we need to normalize the types *)
-          log#serror
-            ("check_typed_pattern: not the same types:" ^ "\n- ty: "
-           ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
-          craise __FILE__ __LINE__ meta "Inconsistent types");
+          craise __FILE__ __LINE__ meta
+            ("Inconsistent types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: "
+           ^ show_ty v.ty);
         check_typed_pattern meta ctx v
       in
       (* Check the field types: check that the field patterns have the expected
@@ -238,3 +237,4 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
   | Meta (_, e_next) ->
       sanity_check __FILE__ __LINE__ (e_next.ty = e.ty) meta;
       check_texpression meta ctx e_next
+  | EError (meta, msg) -> craise_opt_meta __FILE__ __LINE__ meta msg
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index e8f2d95e..fdd14eba 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -233,6 +233,9 @@ let rec let_group_requires_parentheses (meta : Meta.meta) (e : texpression) :
   | Loop _ ->
       (* Should have been eliminated *)
       craise __FILE__ __LINE__ meta "Unreachable"
+  | EError (meta, msg) ->
+      craise_opt_meta __FILE__ __LINE__ meta
+        msg (* TODO : check if true should'nt be returned instead ? *)
 
 let texpression_requires_parentheses meta e =
   match !Config.backend with
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index e164fd49..f15a2c23 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -212,6 +212,7 @@ type expression =
           TODO: merge this with Return.
        *)
   | Meta of emeta * expression  (** Meta information *)
+  | Error of Meta.meta option * string
 
 and loop = {
   loop_id : loop_id;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 482ebf3a..cf03fddf 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1997,6 +1997,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
   (* Return the computed information *)
   !info
 
+let translate_error (meta : Meta.meta option) (msg : string) : texpression =
+  { e = EError (meta, msg); ty = Error }
+
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   match e with
   | S.Return (ectx, opt_v) ->
@@ -2023,6 +2026,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       *)
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
+  | Error (meta, msg) -> translate_error meta msg
 
 and translate_panic (ctx : bs_ctx) : texpression = Option.get ctx.mk_panic
 
@@ -3916,7 +3920,16 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   def
 
 let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
-  List.map (translate_type_decl ctx)
+  List.filter_map
+    (fun a ->
+      try Some (translate_type_decl ctx a)
+      with CFailure (meta, _) ->
+        let env = PrintPure.decls_ctx_to_fmt_env ctx in
+        let name = PrintPure.name_to_string env a.name in
+        save_error __FILE__ __LINE__ meta
+          ("Could not translate type decl '" ^ name
+         ^ "' because of previous error");
+        None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
 let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 22288fe2..9460c5f4 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
     of backward functions, we also provide names for the outputs.
     TODO: maybe we should introduce a record for this.
 *)
-let translate_function_to_pure (trans_ctx : trans_ctx)
+let translate_function_to_pure_aux (trans_ctx : trans_ctx)
     (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
     (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
     pure_fun_translation_no_loops =
@@ -197,6 +197,20 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   | None -> SymbolicToPure.translate_fun_decl ctx None
   | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast)
 
+let translate_function_to_pure (trans_ctx : trans_ctx)
+    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
+    (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
+    pure_fun_translation_no_loops option =
+  try
+    Some
+      (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
+  with CFailure (meta, _) ->
+    let name = name_to_string trans_ctx fdef.name in
+    save_error __FILE__ __LINE__ meta
+      ("Could not translate the function '" ^ name
+     ^ "' because of previous error");
+    None
+
 (* TODO: factor out the return type *)
 let translate_crate_to_pure (crate : crate) :
     trans_ctx
@@ -222,32 +236,54 @@ let translate_crate_to_pure (crate : crate) :
   (* Compute the decomposed fun sigs for the whole crate *)
   let fun_dsigs =
     FunDeclId.Map.of_list
-      (List.map
+      (List.filter_map
          (fun (fdef : LlbcAst.fun_decl) ->
-           ( fdef.def_id,
-             SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx
-               fdef ))
+           try
+             Some
+               ( fdef.def_id,
+                 SymbolicToPure.translate_fun_sig_from_decl_to_decomposed
+                   trans_ctx fdef )
+           with CFailure (meta, _) ->
+             let name = name_to_string trans_ctx fdef.name in
+             save_error __FILE__ __LINE__ meta
+               ("Could not translate the function signature of '" ^ name
+              ^ "' because of previous error");
+             None)
          (FunDeclId.Map.values crate.fun_decls))
   in
 
   (* Translate all the *transparent* functions *)
   let pure_translations =
-    List.map
+    List.filter_map
       (translate_function_to_pure trans_ctx type_decls_map fun_dsigs)
       (FunDeclId.Map.values crate.fun_decls)
   in
 
   (* Translate the trait declarations *)
   let trait_decls =
-    List.map
-      (SymbolicToPure.translate_trait_decl trans_ctx)
+    List.filter_map
+      (fun a ->
+        try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
+        with CFailure (meta, _) ->
+          let name = name_to_string trans_ctx a.name in
+          save_error __FILE__ __LINE__ meta
+            ("Could not translate the trait declaration '" ^ name
+           ^ "' because of previous error");
+          None)
       (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
   in
 
   (* Translate the trait implementations *)
   let trait_impls =
-    List.map
-      (SymbolicToPure.translate_trait_impl trans_ctx)
+    List.filter_map
+      (fun a ->
+        try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
+        with CFailure (meta, _) ->
+          let name = name_to_string trans_ctx a.name in
+          save_error __FILE__ __LINE__ meta
+            ("Could not translate the trait instance '" ^ name
+           ^ "' because of previous error");
+          None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
 
@@ -473,7 +509,15 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
        groups are always singletons, so the [extract_global_decl] function
        takes care of generating the delimiters.
     *)
-    let global = SymbolicToPure.translate_global ctx.trans_ctx global in
+    let global =
+      try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
+      with CFailure (meta, _) ->
+        let name = name_to_string ctx.trans_ctx global.name in
+        save_error __FILE__ __LINE__ meta
+          ("Could not translate the global declaration '" ^ name
+         ^ "' because of previous error");
+        None
+    in
     Extract.extract_global_decl ctx fmt global body config.interface
 
 (** Utility.
@@ -728,22 +772,28 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     | TypeGroup (RecGroup ids) ->
         if config.extract_types then export_types_group true ids
     | FunGroup (NonRecGroup id) -> (
-        (* Lookup *)
-        let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+        (* Lookup - the translated function may not be in the map if we had
+           to ignore it because of errors *)
+        let pure_fun = FunDeclId.Map.find_opt id ctx.trans_funs in
         (* Special case: we skip trait method *declarations* (we will
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
-        match pure_fun.f.Pure.kind with
-        | TraitItemDecl _ -> ()
-        | _ ->
-            (* Translate *)
-            export_functions_group [ pure_fun ])
+        match pure_fun with
+        | Some pure_fun -> (
+            match pure_fun.f.Pure.kind with
+            | TraitItemDecl _ -> ()
+            | _ ->
+                (* Translate *)
+                export_functions_group [ pure_fun ])
+        | None -> ())
     | FunGroup (RecGroup ids) ->
         (* General case of mutually recursive functions *)
         (* Lookup *)
         let pure_funs =
-          List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
+          List.filter_map
+            (fun id -> FunDeclId.Map.find_opt id ctx.trans_funs)
+            ids
         in
         (* Translate *)
         export_functions_group pure_funs
@@ -901,7 +951,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
 
   (* Some logging *)
-  log#linfo (lazy ("Generated: " ^ fi.filename));
+  if !Errors.error_list <> [] then
+    log#linfo
+      (lazy ("Generated the partial file (because of errors): " ^ fi.filename))
+  else log#linfo (lazy ("Generated: " ^ fi.filename));
 
   (* Flush and close the file *)
   close_out out
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index f5dd7df4..b2c60cc6 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -12,6 +12,26 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
   let info = TypesAnalysis.analyze_ty infos ty in
   info.TypesAnalysis.contains_borrow
 
+let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool
+    =
+  let visitor =
+    object
+      inherit [_] iter_ty as super
+
+      method! visit_ty env ty =
+        match ty with
+        | TAdt (type_id, _) when type_id <> TTuple ->
+            let info = TypesAnalysis.analyze_ty infos ty in
+            if info.TypesAnalysis.contains_borrow then raise Found
+            else super#visit_ty env ty
+        | _ -> super#visit_ty env ty
+    end
+  in
+  try
+    visitor#visit_ty () ty;
+    false
+  with Found -> true
+
 (** Retuns true if the type contains nested borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 91010e07..b6ee66f5 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -160,7 +160,7 @@ let find_first_primitively_copyable_sv_with_borrows
 
       method! visit_VSymbolic _ sv =
         let ty = sv.sv_ty in
-        if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
+        if ty_is_copyable ty && ty_has_borrows type_infos ty then
           raise (FoundSymbolicValue sv)
         else ()
     end
diff --git a/flake.lock b/flake.lock
index 27a555ad..1eaf1375 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1712233083,
-        "narHash": "sha256-KR4UwlgUzLWObSzQ1LIKITjRrYe4AuZXdvCK78qrip8=",
+        "lastModified": 1712825631,
+        "narHash": "sha256-YC0QArtso4Z9iBgd63FXHsSopMtWof0kC7ZrYpE6yzg=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "6e31313fdfd4830aa0fc795f6ab8b27600fcbbfb",
+        "rev": "657de2521c285401d706ec69d588bb5778b18109",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 72c4fd99..36910f45 100644
--- a/flake.nix
+++ b/flake.nix
@@ -153,7 +153,14 @@
           default = aeneas;
         };
         devShells.default = pkgs.mkShell {
+          # By default, tests run some sanity checks which are pretty slow.
+          # This disables these checks when developping locally.
+          OPTIONS = "";
+
           packages = [
+            pkgs.ocamlPackages.ocaml
+            pkgs.ocamlPackages.ocamlformat
+            pkgs.ocamlPackages.menhir
             pkgs.ocamlPackages.odoc
           ];
 
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 7215e286..4e0ca509 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -113,6 +113,10 @@ def inv (hm : HashMap α) : Prop :=
 -- This rewriting lemma is problematic below
 attribute [-simp] Bool.exists_bool
 
+-- The proof below is a bit expensive, so we need to increase the maximum number
+-- of heart beats
+set_option maxHeartbeats 1000000
+
 theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
   (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
   (hdk : distinct_keys l0.v) :
@@ -232,7 +236,7 @@ set_option pp.coercions false -- do not print coercions with ↑ (this doesn't p
 
 -- The proof below is a bit expensive, so we need to increase the maximum number
 -- of heart beats
-set_option maxHeartbeats 1000000
+set_option maxHeartbeats 2000000
 
 theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
   (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
@@ -318,17 +322,21 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
       simp_all
     have _ : 0 ≤ k_hash_mod := by
       -- TODO: we want to automate this
-      simp
+      simp only [k_hash_mod]
       apply Int.emod_nonneg k.val hvnz
     have _ : k_hash_mod < alloc.vec.Vec.length hm.slots := by
       -- TODO: we want to automate this
-      simp
+      simp only [k_hash_mod]
       have h := Int.emod_lt_of_pos k.val hvpos
-      simp_all
+      simp_all only [ret.injEq, exists_eq_left', List.len_update, gt_iff_lt,
+                     List.index_update_eq, ne_eq, not_false_eq_true, neq_imp]
     if h_hm : k_hash_mod = hash_mod.val then
-      simp_all
+      simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
+                     ne_eq, not_false_eq_true, neq_imp, alloc.vec.Vec.length]
     else
-      simp_all
+      simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
+                     ne_eq, not_false_eq_true, neq_imp, ge_iff_le,
+                     alloc.vec.Vec.length, List.index_update_ne]
   have _ :
     match hm.lookup key with
     | none => nhm.len_s = hm.len_s + 1
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index e167e841..404d3dab 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.27",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "d04f8d39c0e47a0d73450b49f6c0665897cdcaf7",
+   "rev": "d9c412b8103b5098bf8b66cbb981b81a57375925",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -70,5 +70,5 @@
    "inherited": false,
    "dir": "./../../backends/lean",
    "configFile": "lakefile.lean"}],
- "name": "Tests",
+ "name": "tests",
  "lakeDir": ".lake"}
diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
index f96d662e..9ad30404 100644
--- a/tests/lean/lean-toolchain
+++ b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0