diff --git a/engine/backends/lean/dune b/engine/backends/lean/dune
new file mode 100644
index 000000000..0c5b33e6f
--- /dev/null
+++ b/engine/backends/lean/dune
@@ -0,0 +1,21 @@
+(library
+ (name lean_backend)
+ (package hax-engine)
+ (wrapped false)
+ (libraries hax_engine base)
+ (preprocess
+  (pps
+   ppx_yojson_conv
+   ppx_sexp_conv
+   ppx_compare
+   ppx_hash
+   ppx_deriving.show
+   ppx_deriving.eq
+   ppx_inline
+   ppx_functor_application
+   ppx_matches)))
+
+(env
+ (_
+  (flags
+   (:standard -w -A))))
diff --git a/engine/backends/lean/lean_backend.ml b/engine/backends/lean/lean_backend.ml
new file mode 100644
index 000000000..c838d95f1
--- /dev/null
+++ b/engine/backends/lean/lean_backend.ml
@@ -0,0 +1,132 @@
+open Hax_engine
+open Utils
+open Base
+
+include
+  Backend.Make
+    (struct
+      open Features
+      include Off
+      include On.Monadic_binding
+      include On.Slice
+      include On.Macro
+      include On.Construct_base
+      include On.Quote
+      include On.Dyn
+      include On.Unsafe
+    end)
+    (struct
+      let backend = Diagnostics.Backend.FStar
+    end)
+
+module SubtypeToInputLanguage
+    (FA :
+      Features.T
+        with type mutable_reference = Features.Off.mutable_reference
+         and type continue = Features.Off.continue
+         and type break = Features.Off.break
+         and type mutable_reference = Features.Off.mutable_reference
+         and type mutable_pointer = Features.Off.mutable_pointer
+         and type mutable_variable = Features.Off.mutable_variable
+         and type reference = Features.Off.reference
+         and type raw_pointer = Features.Off.raw_pointer
+         and type early_exit = Features.Off.early_exit
+         and type question_mark = Features.Off.question_mark
+         and type as_pattern = Features.Off.as_pattern
+         and type lifetime = Features.Off.lifetime
+         and type monadic_action = Features.Off.monadic_action
+         and type arbitrary_lhs = Features.Off.arbitrary_lhs
+         and type nontrivial_lhs = Features.Off.nontrivial_lhs
+         and type loop = Features.Off.loop
+         and type block = Features.Off.block
+         and type for_loop = Features.Off.for_loop
+         and type while_loop = Features.Off.while_loop
+         and type for_index_loop = Features.Off.for_index_loop
+         and type state_passing_loop = Features.Off.state_passing_loop
+         and type fold_like_loop = Features.Off.fold_like_loop
+         and type match_guard = Features.Off.match_guard
+         and type trait_item_default = Features.Off.trait_item_default) =
+struct
+  module FB = InputLanguage
+
+  include
+    Subtype.Make (FA) (FB)
+      (struct
+        module A = FA
+        module B = FB
+        include Features.SUBTYPE.Id
+        include Features.SUBTYPE.On.Monadic_binding
+        include Features.SUBTYPE.On.Construct_base
+        include Features.SUBTYPE.On.Slice
+        include Features.SUBTYPE.On.Macro
+        include Features.SUBTYPE.On.Quote
+        include Features.SUBTYPE.On.Dyn
+        include Features.SUBTYPE.On.Unsafe
+      end)
+
+  let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
+end
+
+module AST = Ast.Make (InputLanguage)
+
+module BackendOptions = struct
+  type t = Hax_engine.Types.f_star_options_for__null
+end
+
+open Ast
+module U = Ast_utils.Make (InputLanguage)
+module Visitors = Ast_visitors.Make (InputLanguage)
+open AST
+
+module Context = struct
+  type t = {
+    current_namespace : string list;
+    items : item list;
+    interface_mode : bool;
+    line_width : int;
+  }
+end
+
+open Phase_utils
+module DepGraphR = Dependencies.Make (Features.Rust)
+
+module TransformToInputLanguage =
+  [%functor_application
+    Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Transform_hax_lib_inline
+  |> Phases.Specialize
+  |> Phases.Drop_sized_trait
+  |> Phases.Simplify_question_marks
+  |> Phases.And_mut_defsite
+  |> Phases.Reconstruct_asserts
+  |> Phases.Reconstruct_for_loops
+  |> Phases.Reconstruct_while_loops
+  |> Phases.Direct_and_mut
+  |> Phases.Reject.Arbitrary_lhs
+  |> Phases.Drop_blocks
+  |> Phases.Drop_match_guards
+  |> Phases.Drop_references
+  |> Phases.Trivialize_assign_lhs
+  |> Side_effect_utils.Hoist
+  |> Phases.Hoist_disjunctive_patterns
+  |> Phases.Simplify_match_return
+  |> Phases.Local_mutation
+  |> Phases.Rewrite_control_flow
+  |> Phases.Drop_return_break_continue
+  |> Phases.Functionalize_loops
+  |> Phases.Reject.Question_mark
+  |> Phases.Reject.As_pattern
+  |> Phases.Traits_specs
+  |> Phases.Simplify_hoisting
+  |> Phases.Newtype_as_refinement
+  |> Phases.Reject.Trait_item_default
+  |> Phases.Bundle_cycles
+  |> Phases.Reorder_fields
+  |> Phases.Sort_items
+  |> SubtypeToInputLanguage
+  |> Identity
+  ]
+  [@ocamlformat "disable"]
+
+let apply_phases (items : Ast.Rust.item list) : AST.item list =
+  TransformToInputLanguage.ditems items
diff --git a/engine/bin/dune b/engine/bin/dune
index da07f5d3e..815872542 100644
--- a/engine/bin/dune
+++ b/engine/bin/dune
@@ -5,6 +5,7 @@
  (libraries
   hax_engine
   fstar_backend
+  lean_backend
   coq_backend
   ssprove_backend
   easycrypt_backend
diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
index d42843127..bc24e0bc0 100644
--- a/engine/bin/lib.ml
+++ b/engine/bin/lib.ml
@@ -257,7 +257,7 @@ let engine () =
       Printexc.raise_with_backtrace exn bt
 
 module ExportRustAst = Export_ast.Make (Features.Rust)
-module ExportFStarAst = Export_ast.Make (Fstar_backend.InputLanguage)
+module ExportLeanAst = Export_ast.Make (Lean_backend.InputLanguage)
 
 (** Entry point for interacting with the Rust hax engine *)
 let driver_for_rust_engine () : unit =
@@ -272,26 +272,16 @@ let driver_for_rust_engine () : unit =
   match query.kind with
   | Types.ImportThir { input; apply_phases } ->
       (* Note: `apply_phases` comes from the type `QueryKind` in
-      `ocaml_engine.rs`. This is a temporary flag that applies some phases while
-      importing THIR. In the future (when #1550 is merged), we will be able to
-      import THIR and then apply phases. *)
+       `ocaml_engine.rs`. This is a temporary flag that applies some phases while
+       importing THIR. In the future (when #1550 is merged), we will be able to
+       import THIR and then apply phases. *)
       let imported_items = import_thir_items [] input in
       let rust_ast_items =
         if apply_phases then
-          let imported_items =
-            (* TODO: this let binding is applying the phases from the F* backend *)
-            Fstar_backend.apply_phases
-              {
-                cli_extension = EmptyStructempty_args_extension;
-                fuel = Int64.zero;
-                ifuel = Int64.zero;
-                interfaces = [];
-                line_width = 80;
-                z3rlimit = Int64.zero;
-              }
-              imported_items
-          in
-          List.concat_map ~f:ExportFStarAst.ditem imported_items
+          let imported_items = Lean_backend.apply_phases imported_items in
+          List.concat_map
+            ~f:(fun item -> ExportLeanAst.ditem item)
+            imported_items
         else List.concat_map ~f:ExportRustAst.ditem imported_items
       in
       let response = Rust_engine_types.ImportThir { output = rust_ast_items } in
diff --git a/examples/barrett/proofs/lean/extraction/Lib.lean b/examples/barrett/proofs/lean/extraction/Lib.lean
deleted file mode 100644
index c71b38d20..000000000
--- a/examples/barrett/proofs/lean/extraction/Lib.lean
+++ /dev/null
@@ -1,83 +0,0 @@
-abbrev u8 := Nat
-abbrev u16 := Nat
-abbrev u32 := Nat
-abbrev u64 := Nat
-abbrev usize := Nat
-abbrev i8 := Nat
-abbrev i16 := Nat
-abbrev i32 := Nat
-abbrev i64 := Nat
-abbrev isize := Nat
-
--- Arithmetic
-def hax_machine_int_add (x y: Nat) := x + y
-def hax_machine_int_mul (x y: Nat) := x * y
-def hax_machine_int_bitxor (x y: Nat) : Nat := sorry
-
-def hax_machine_int_eq (x y: Nat) : Bool := x = y
-def hax_machine_int_ne (x y: Nat) : Bool := x != y
-def hax_machine_int_ge (x y: Nat) : Bool := x >= y
-def hax_machine_int_gt (x y: Nat) : Bool := x > y
-def hax_machine_int_le (x y: Nat) : Bool := x <= y
-def hax_machine_int_lt (x y: Nat) : Bool := x < y
-
-
--- Nums
-def num_impl_wrapping_add : Nat -> Nat -> Nat := sorry
-def num_impl_from_le_bytes {α} : (Array α) -> u32 := sorry
-
--- Results
-inductive result_Result α β
-| ok : α -> result_Result α β
-| err : β -> result_Result α β
-
-axiom array_TryFromSliceError : Type
-
--- Assert
-def assert : Bool -> Unit := fun _ => ()
-def assume : Prop -> Unit := fun _ => ()
-def prop_constructors_from_bool : Bool -> Prop := sorry
-
--- Hax
-def hax_folds_fold_range
-  (s: Nat)
-  (e: Nat) :
-  ((Array u32) -> Nat -> Bool) ->
-  (Array u32) ->
-  ((Array u32) -> Nat -> (Array u32)) ->
-  (Array u32) := sorry
-
-def hax_monomorphized_update_at_update_at_usize :
-  (Array u32) ->
-  Nat ->
-  u32 ->
-  (Array u32) := sorry
-
-abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize (_: Nat) (_: Nat) := Nat
-
-def result_impl_unwrap {α} : α -> Array β := sorry
-
--- Vectors
-def hax_repeat (x:Nat) (y:Nat) : Array u32 := sorry
-
--- Ranges
-
-structure ops_range_Range_arg (α: Type) where
-ops_range_Range_start : α
-ops_range_Range_end : α
-
-inductive ops_range_Range (α: Type)  where
-| constr_ops_range_Range : ops_range_Range_arg α -> ops_range_Range α
-
-
--- Arrays
-def ops_index_Index_index (a: Array u8) : α -> β := sorry
-def convert_TryInto_try_into {α} : Array α ->
-   result_Result (Array α) array_TryFromSliceError := sorry
-
-
--- Slices
-def slice_impl_len (a: Array u32) : Nat := sorry
-
--- Bytes
-def num_impl_to_le_bytes : u32 -> Array u8 := sorry
diff --git a/examples/default.nix b/examples/default.nix
index 29f68c404..392536e44 100644
--- a/examples/default.nix
+++ b/examples/default.nix
@@ -8,6 +8,7 @@
   hax-env,
   jq,
   proverif,
+  lean4,
 }: let
   commonArgs = import ./commonArgs.nix {inherit craneLib lib;};
   cargoArtifacts = craneLib.buildDepsOnly commonArgs;
@@ -29,7 +30,7 @@ in
         make
       '';
       buildInputs = [
-        hax hax-env fstar jq
+        hax hax-env fstar jq lean4
         (proverif.overrideDerivation (_: {
           patches = [ ./proverif-psk/pv_div_by_zero_fix.diff ];
         }))
diff --git a/hax-lib/build.rs b/hax-lib/build.rs
index eb4850605..90931618d 100644
--- a/hax-lib/build.rs
+++ b/hax-lib/build.rs
@@ -43,6 +43,7 @@ pub mod {backend} {{
             code("fstar", FSTAR_EXTRA),
             code("proverif", ""),
             code("coq", ""),
+            code("lean", ""),
         ]
         .join("\n"),
     )
diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs
index c89ce4e0a..57a5f4676 100644
--- a/hax-lib/macros/src/dummy.rs
+++ b/hax-lib/macros/src/dummy.rs
@@ -36,15 +36,19 @@ identity_proc_macro_attribute!(
     refinement_type,
     fstar_replace,
     coq_replace,
+    lean_replace,
     proverif_replace,
     fstar_replace_body,
     coq_replace_body,
+    lean_replace_body,
     proverif_replace_body,
     fstar_before,
     coq_before,
+    lean_before,
     proverif_before,
     fstar_after,
     coq_after,
+    lean_after,
     proverif_after,
     fstar_smt_pat,
     fstar_postprocess_with,
@@ -59,6 +63,10 @@ pub fn coq_expr(_payload: TokenStream) -> TokenStream {
     quote! { () }.into()
 }
 #[proc_macro]
+pub fn lean_expr(_payload: TokenStream) -> TokenStream {
+    quote! { () }.into()
+}
+#[proc_macro]
 pub fn proverif_expr(_payload: TokenStream) -> TokenStream {
     quote! { () }.into()
 }
@@ -84,6 +92,10 @@ pub fn coq_unsafe_expr(_payload: TokenStream) -> TokenStream {
     unsafe_expr()
 }
 #[proc_macro]
+pub fn lean_unsafe_expr(_payload: TokenStream) -> TokenStream {
+    unsafe_expr()
+}
+#[proc_macro]
 pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream {
     unsafe_expr()
 }
@@ -97,6 +109,10 @@ pub fn coq_prop_expr(_payload: TokenStream) -> TokenStream {
     quote! {::hax_lib::Prop::from_bool(true)}.into()
 }
 #[proc_macro]
+pub fn lean_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+#[proc_macro]
 pub fn proverif_prop_expr(_payload: TokenStream) -> TokenStream {
     quote! {::hax_lib::Prop::from_bool(true)}.into()
 }
diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs
index 2374db617..7a2040ffc 100644
--- a/hax-lib/macros/src/implementation.rs
+++ b/hax-lib/macros/src/implementation.rs
@@ -989,7 +989,7 @@ macro_rules! make_quoting_proc_macro {
     }
 }
 
-make_quoting_proc_macro!(fstar coq proverif);
+make_quoting_proc_macro!(fstar coq proverif lean);
 
 /// Marks a newtype `struct RefinedT(T);` as a refinement type. The
 /// struct should have exactly one unnamed private field.
diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs
index 1dbc003d8..237b669af 100644
--- a/hax-lib/macros/src/utils.rs
+++ b/hax-lib/macros/src/utils.rs
@@ -10,6 +10,7 @@ impl ToTokens for HaxQuantifiers {
         quote! {
             use ::hax_lib::fstar::prop as fstar;
             use ::hax_lib::coq::prop as coq;
+            use ::hax_lib::lean::prop as lean;
             use ::hax_lib::proverif::prop as proverif;
         }
         .to_tokens(tokens)
diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean
new file mode 100644
index 000000000..e82ea89f8
--- /dev/null
+++ b/hax-lib/proof-libs/lean/Lib.lean
@@ -0,0 +1,1110 @@
+/-
+Hax Lean Backend - Cryspen
+
+This library provides the Lean prelude for hax extracted rust-code. It contains
+the lean definition of rust (and hax) primitives and intrinsics.
+
+It borrows some definitions from the Aeneas project
+(https://github.com/AeneasVerif/aeneas/)
+-/
+
+import Std
+import Std.Do.Triple
+import Std.Tactic.Do
+import Std.Tactic.Do.Syntax
+
+open Std.Do
+open Std.Tactic
+
+set_option mvcgen.warning false
+set_option linter.unusedVariables false
+
+/-
+# Monadic encoding
+
+The encoding is based on the `Result` monad: all rust computations are wrapped
+in the monad, representing the fact that they are not total.
+
+-/
+
+/--
+  (Aeneas) Error cases
+-/
+inductive Error where
+   | assertionFailure: Error
+   | integerOverflow: Error
+   | divisionByZero: Error
+   | arrayOutOfBounds: Error
+   | maximumSizeExceeded: Error
+   | panic: Error
+   | undef: Error
+deriving Repr, BEq
+open Error
+
+/-- (Aeneas) Result monad, representing possible results of rust computations -/
+inductive Result.{u} (α : Type u) where
+  | ok (v: α): Result α
+  | fail (e: Error): Result α
+  | div
+deriving Repr, BEq
+
+namespace Result
+
+@[simp]
+instance instPure: Pure Result where
+  pure x := .ok x
+
+@[simp]
+def bind (x: Result α) (f: α -> Result β) := match x with
+  | .ok v => f v
+  | .fail e => .fail e
+  | .div => .div
+
+@[simp]
+def ofOption {α} (x:Option α) (e: Error) : Result α := match x with
+  | .some v => pure v
+  | .none => .fail e
+
+@[simp]
+instance instMonad : Monad Result where
+  pure := pure
+  bind := Result.bind
+
+@[simp]
+instance instLawfulMonad : LawfulMonad Result where
+  id_map x := by
+    dsimp [id, Functor.map]
+    cases x;
+    all_goals grind
+  map_const := by
+    intros α β
+    dsimp [Functor.map, Functor.mapConst]
+  seqLeft_eq x y := by
+    dsimp [Functor.map, SeqLeft.seqLeft, Seq.seq]
+    cases x ; all_goals cases y
+    all_goals try simp
+  seqRight_eq x y := by
+    dsimp [Functor.map, SeqRight.seqRight, Seq.seq]
+    cases x ; all_goals cases y
+    all_goals try simp
+  pure_seq g x := by
+    dsimp [Functor.map, Seq.seq, pure]
+  bind_pure_comp f x := by
+    dsimp [Functor.map]
+  bind_map f x := by
+    dsimp [Functor.map, bind, pure, Seq.seq]
+  pure_bind x f := by
+    dsimp [pure, bind, pure]
+  bind_assoc x f g := by
+    dsimp [pure, bind]
+    cases x; all_goals simp
+
+@[simp]
+instance instWP : WP Result (.except Error .pure) where
+  wp x := match x with
+  | .ok v => wp (Pure.pure v : Except Error _)
+  | .fail e => wp (throw e : Except Error _)
+  | .div => PredTrans.const ⌜False⌝
+
+@[simp]
+instance instWPMonad : WPMonad Result (.except Error .pure) where
+  wp_pure := by intros; ext Q; simp [wp, PredTrans.pure, Pure.pure, Except.pure, Id.run]
+  wp_bind x f := by
+    simp only [instWP]
+    ext Q
+    cases x <;> simp [PredTrans.bind, PredTrans.const, Bind.bind]
+
+@[default_instance]
+instance instCoe {α} : Coe α (Result α) where
+  coe x := pure x
+
+end Result
+
+
+/-
+  Logic predicates introduced by Hax (in pre/post conditions)
+-/
+section Logic
+
+@[simp, spec]
+abbrev hax_logical_op_and := (fun a b => a && b)
+@[simp, spec]
+abbrev hax_logical_op_or := (fun a b => a || b)
+
+abbrev assert (b:Bool) : Result Unit :=
+  if b then pure ()
+  else .fail (Error.assertionFailure)
+
+abbrev assume : Prop -> Result Unit := fun _ => pure ()
+
+abbrev prop_constructors_from_bool (b :Bool) : Prop := (b = true)
+
+end Logic
+
+/-
+  Integer types are represented as the corresponding type in Lean
+-/
+abbrev u8 := UInt8
+abbrev u16 := UInt16
+abbrev u32 := UInt32
+abbrev u64 := UInt64
+abbrev usize := USize
+abbrev i8 := Int8
+abbrev i16 := Int16
+abbrev i32 := Int32
+abbrev i64 := Int64
+abbrev isize := ISize
+
+/-- Class of objects that can be transformed into Nat -/
+class ToNat (α: Type) where
+  toNat : α -> Nat
+
+@[simp]
+instance : ToNat USize where
+  toNat x := x.toNat
+@[simp]
+instance : ToNat u64 where
+  toNat x := x.toNat
+@[simp]
+instance : ToNat u32 where
+  toNat x := x.toNat
+@[simp]
+instance : ToNat u16 where
+  toNat x := x.toNat
+@[simp]
+instance : ToNat Nat where
+  toNat x := x
+
+/-
+  Coercions between integer types
+-/
+-- TODO : make sure all are necessary, document their use-cases
+@[simp, spec]
+instance : Coe i32 (Result i64) where
+  coe x := pure (x.toInt64)
+
+@[simp]
+instance : Coe USize Nat where
+  coe x := x.toNat
+
+@[simp]
+instance : Coe u32 Nat where
+  coe x := x.toNat
+
+@[simp]
+instance : Coe Nat usize where
+  coe x := USize.ofNat x
+
+@[simp]
+instance : Coe Nat i32 where
+  coe x := Int32.ofNat x
+
+@[simp]
+instance : Coe USize UInt32 where
+  coe x := x.toUInt32
+
+@[simp]
+instance : Coe USize (Result u32) where
+  coe x := if x.toNat < UInt32.size then pure (x.toUInt32)
+           else Result.fail .integerOverflow
+
+@[simp]
+instance {β} : Coe (α -> usize -> β) (α -> Nat -> β) where
+  coe f a x := f a (USize.ofNat x)
+
+@[simp]
+instance {β} : Coe (α -> i32 -> β) (α -> Nat -> β) where
+  coe f a x := f a (Int32.ofNat x)
+
+@[simp]
+instance : OfNat (Result Nat) n where
+  ofNat := pure (n)
+
+
+/-
+
+# Arithmetic operations
+
+The Rust arithmetic operations have their own notations, using a `?`. They
+return a `Result`, that is `.fail` when arithmetic overflows occur.
+
+-/
+section Arithmetic
+
+/-- The notation typeclass for homogeneous addition that returns a Result.  This
+enables the notation `a +? b : α` where `a : α`, `b : α`. For now, there is no
+heterogeneous version -/
+class HaxAdd α where
+  /-- `a +? b` computes the panicking sum of `a` and `b`.  The meaning of this
+  notation is type-dependent. -/
+  add : α → α → Result α
+
+/-- The notation typeclass for homogeneous substraction that returns a Result.
+This enables the notation `a -? b : α` where `a : α`, `b : α`. For now, there is
+no heterogeneous version -/
+class HaxSub α where
+  /-- `a -? b` computes the panicking substraction of `a` and `b`.
+  The meaning of this notation is type-dependent. -/
+  sub : α → α → Result α
+
+/-- The notation typeclass for homogeneous multiplication that returns a Result.
+This enables the notation `a *? b : Result α` where `a b : α`. For now, there is
+no heterogeneous version -/
+class HaxMul α where
+  /-- `a -? b` computes the panicking multiplication of `a` and `b`.  The
+  meaning of this notation is type-dependent. -/
+  mul : α → α → Result α
+
+/-- The notation typeclass for homogeneous division that returns a Result.  This
+enables the notation `a /? b : Result α` where `a b : α`. For now, there is no
+heterogeneous version -/
+class HaxDiv α where
+  /-- `a -? b` computes the panicking multiplication of `a` and `b`.  The
+  meaning of this notation is type-dependent. -/
+  div : α → α → Result α
+
+/-- The typeclass behind the notation `a >>>? b : Result α` where `a b : α`. -/
+class HaxShiftRight α where
+  /-- `a >>>? b` computes the panicking right-shift of `a` by `b`.  The meaning
+  of this notation is type-dependent. It panics if `b` exceeds the size of `a`.
+  -/
+  shiftRight : α → α → Result α
+
+/-- The notation typeclass for remainder.  This enables the notation `a %? b :
+Result α` where `a b : α`.  -/
+class HaxRem α where
+  /-- `a %? b` computes the panicking remainder upon dividing `a` by `b`.  The
+  meaning of this notation is type-dependent. It panics if b is zero -/
+  rem : α → α → Result α
+
+@[inherit_doc] infixl:65 " +? " => HaxAdd.add
+@[inherit_doc] infixl:65 " -? " => HaxSub.sub
+@[inherit_doc] infixl:70 " *? " => HaxMul.mul
+@[inherit_doc] infixl:75 " >>>? " => HaxShiftRight.shiftRight
+@[inherit_doc] infixl:70 " %? "   => HaxRem.rem
+@[inherit_doc] infixl:70 " /? "   => HaxDiv.div
+
+/- Until notations are not introduced by the Lean backend, explicit hax-names
+  are also provided -/
+@[simp, spec]
+def hax_machine_int_add {α} [HaxAdd α] (x y: α) : Result α := x +? y
+@[simp, spec]
+def hax_machine_int_sub {α} [HaxSub α] (x y: α) : Result α := x -? y
+@[simp, spec]
+def hax_machine_int_mul {α} [HaxMul α] (x y: α) : Result α := x *? y
+@[simp, spec]
+def hax_machine_int_div {α} [HaxDiv α] (x y: α) : Result α := x /? y
+@[simp, spec]
+def hax_machine_int_rem {α} [HaxRem α] (x y: α) : Result α := x %? y
+@[simp, spec]
+def hax_machine_int_shr {α} [HaxShiftRight α] (a b: α) : Result α := a >>>? b
+@[simp]
+def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := pure (a ^^^ b)
+@[simp]
+def ops_arith_Neg_neg {α} [Neg α] (x:α) : Result α := pure (-x)
+
+@[simp]
+def hax_machine_int_eq {α} (x y: α) [BEq α] : Result Bool := pure (x == y)
+@[simp]
+def hax_machine_int_ne {α} (x y: α) [BEq α] : Result Bool := pure (x != y)
+@[simp]
+def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Result Bool :=
+  pure (x < y)
+@[simp]
+def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Result Bool :=
+  pure (x ≤ y)
+@[simp]
+def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Result Bool :=
+  pure (x ≥ y)
+@[simp]
+def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Result Bool :=
+  pure (x > y)
+
+
+/-
+
+# Properties
+
+For each integer types, instances of typeclasses for arithmetic operations are
+given, along with hoare-triple specifications (to be used by mvcgen)
+
+-/
+
+namespace USize
+
+/-- Partial addition on usize -/
+instance instHaxAdd : HaxAdd USize where
+  add x y :=
+    if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x + y)
+
+/-- Bitvec-based specification for rust addition on usize -/
+@[spec]
+theorem HaxAdd_spec_bv (x y: usize) :
+  ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄
+  (x +? y)
+  ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ]
+
+
+/-- Partial substraction on usize -/
+instance instHaxSub : HaxSub USize where
+  sub x y :=
+    if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x - y)
+
+/-- Bitvec-based specification for rust substraction on usize -/
+@[spec]
+theorem HaxSub_spec_bv (x y: usize) :
+  ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄
+  (x -? y)
+  ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub]
+
+
+/-- Partial multiplication on usize -/
+instance instHaxMul : HaxMul USize where
+  mul x y :=
+    if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x * y)
+
+/-- Bitvec-based specification for rust multiplication on usize -/
+@[spec]
+theorem HaxMul_spec_bv (x y: usize) :
+  ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄
+  (x *? y)
+  ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul]
+
+
+/-- Partial right shift on usize -/
+instance instHaxShiftRight : HaxShiftRight USize where
+  shiftRight x y :=
+    if (y ≤ USize.size) then pure (x >>> y)
+    else .fail .integerOverflow
+
+/-- Bitvec-based specification for rust right-shift on usize -/
+@[spec]
+theorem HaxShiftRight_spec_bv (x y: usize) :
+  ⦃ y ≤ USize.size ⦄
+  ( x >>>? y)
+  ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight]
+
+
+/-- Partial division on usize -/
+instance instHaxDiv : HaxDiv usize where
+  div x y :=
+    if y = 0 then .fail .divisionByZero
+    else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x / y)
+
+/-- Bitvec-based specification for rust division on usize -/
+@[spec]
+theorem HaxDiv_spec_bv (x y : usize) :
+  ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄
+  ( x /? y)
+  ⦃ ⇓ r => r = x / y ⦄ := by
+  mvcgen [instHaxDiv] <;> simp <;> try grind
+  have ⟨ _ , h ⟩ := h
+  apply h; assumption
+
+/-- Partial remainder on usize -/
+instance instHaxRem : HaxRem usize where
+  rem x y :=
+    if y = 0 then .fail .divisionByZero
+    else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x % y)
+
+/-- Bitvec-based specification for rust remainder on usize  -/
+@[spec]
+theorem HaxRem_spec_bv (x y : usize) :
+  ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄
+  ( x %? y)
+  ⦃ ⇓ r => r = x % y ⦄ := by
+  mvcgen [instHaxRem] <;> simp <;> try grind
+  have ⟨ _ , h ⟩ := h
+  apply h; assumption
+
+end USize
+
+
+namespace ISize
+
+instance instHaxAdd : HaxAdd ISize where
+  add x y :=
+    if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x + y)
+
+@[spec]
+theorem HaxAdd_spec_bv (x y: isize) :
+  ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄
+  (x +? y)
+  ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd]
+
+theorem HaxAdd_spec_bv_rw (x y: isize) :
+   ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) →
+   x +? y = Result.ok (x + y)
+:= by simp [instHaxAdd]
+
+
+instance instHaxSub : HaxSub ISize where
+  sub x y :=
+    if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x - y)
+
+@[spec]
+theorem HaxSub_spec_bv (x y: isize) :
+  ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄
+  (x -? y)
+  ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub]
+
+instance instHaxMul : HaxMul ISize where
+  mul x y :=
+    if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x * y)
+
+@[spec]
+theorem HaxMul_spec_bv (x y: isize) :
+  ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄
+  (x *? y)
+  ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul]
+
+instance instHaxShiftRight : HaxShiftRight ISize where
+  shiftRight x y :=
+    if (y ≤ ISize.size.toISize) then pure (x >>> y)
+    else .fail .integerOverflow
+
+@[spec]
+theorem HaxShiftRight_spec_bv (x y: isize) :
+  ⦃ y ≤ ISize.size.toISize ⦄
+  ( x >>>? y)
+  ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight]
+
+end ISize
+
+
+namespace Int64
+
+instance instHaxAdd : HaxAdd Int64 where
+  add x y :=
+    if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x + y)
+
+@[spec]
+theorem HaxAdd_spec_bv (x y: i64) :
+  ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄
+  (x +? y)
+  ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ]
+
+instance instHaxSub : HaxSub Int64 where
+  sub x y :=
+    if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x - y)
+
+@[spec]
+theorem HaxSub_spec_bv (x y: i64) :
+  ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄
+  (x -? y)
+  ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub]
+
+instance instHaxMul : HaxMul Int64 where
+  mul x y :=
+    if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x * y)
+
+@[spec]
+theorem HaxMul_spec_bv (x y: i64) :
+  ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄
+  (x *? y)
+  ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul]
+
+instance instHaxShiftRight : HaxShiftRight Int64 where
+  shiftRight x y :=
+    if (y ≤ 64) then pure (x >>> y)
+    else .fail .integerOverflow
+
+@[spec]
+theorem HaxShiftRight_spec_bv (x y: i64) :
+  ⦃ y ≤ 64 ⦄
+  ( x >>>? y)
+  ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight]
+
+end Int64
+
+
+namespace Int32
+
+instance instHaxAdd : HaxAdd Int32 where
+  add x y :=
+    if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x + y)
+
+@[spec]
+theorem HaxAdd_spec_bv (x y: i32) :
+  ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄
+  (x +? y)
+  ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ]
+
+instance instHaxSub : HaxSub Int32 where
+  sub x y :=
+    if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x - y)
+
+@[spec]
+theorem HaxSub_spec_bv (x y: i32) :
+  ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄
+  (x -? y : Result i32)
+  ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub]
+
+instance instHaxMul : HaxMul Int32 where
+  mul x y :=
+    if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x * y)
+
+@[spec]
+theorem HaxMul_spec_bv (x y: i32) :
+  ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄
+  (x *? y : Result i32)
+  ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul]
+
+instance instHaxRem : HaxRem i32 where
+  rem x y :=
+    if y = 0 then .fail .divisionByZero
+    else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
+    else pure (x % y)
+
+@[spec]
+theorem HaxRem_spec_bv (x y : i32) :
+  ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄
+  ( x %? y)
+  ⦃ ⇓ r => r = x % y ⦄ := by
+  mvcgen [instHaxRem] <;> simp <;> try grind
+  have ⟨ _ , h ⟩ := h
+  apply h; assumption
+
+end Int32
+
+/-
+
+# Wrapping operations
+
+Rust also has total arithmetic operations, renamed by hax (with disambiguator)
+for each implementation of typeclasses
+
+-/
+
+@[simp, spec]
+def num__8_impl_wrapping_add (x y: u32) : Result u32 := pure (x + y)
+
+@[simp, spec]
+def num__8_impl_rotate_left (x: u32) (n: Nat) : Result u32 :=
+  pure (UInt32.ofBitVec (BitVec.rotateLeft x.toBitVec n))
+
+
+/-- Hax-generated bounded integers -/
+abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize
+  (lo: USize) (hi: USize) := USize
+--  {u : usize // lo ≤ u ∧ u ≤ hi}
+-- Todo : make it into a proper subtype
+
+
+def num__8_impl_from_le_bytes (x: Vector u8 4) : u32 :=
+  x[0].toUInt32
+  + (x[1].toUInt32 <<< 8)
+  + (x[2].toUInt32 <<< 16)
+  + (x[3].toUInt32 <<< 24)
+
+def num__8_impl_to_le_bytes (x:u32) : Result (Vector u8 4) :=
+  #v[
+    (x % 256).toUInt8,
+    (x >>> 8 % 256).toUInt8,
+    (x >>> 16 % 256).toUInt8,
+    (x >>> 24 % 256).toUInt8,
+  ]
+
+
+end Arithmetic
+
+
+
+/-
+
+# Tuples
+
+-/
+section Tuples
+
+abbrev hax_Tuple0 : Type := Unit
+def constr_hax_Tuple0 : hax_Tuple0 := ()
+instance : CoeDep Type hax_Tuple0 (hax_Tuple0) where
+  coe := ()
+
+
+abbrev hax_Tuple1 (α: Type) : Type := α × Unit
+def constr_hax_Tuple1 {hax_Tuple1_Tuple0: α} : hax_Tuple1 α := (hax_Tuple1_Tuple0, ())
+
+abbrev hax_Tuple2 (α β: Type) : Type := α × β
+def constr_hax_Tuple2 {α β} {hax_Tuple2_Tuple0: α} {hax_Tuple2_Tuple1 : β} : hax_Tuple2 α β
+  := (hax_Tuple2_Tuple0, hax_Tuple2_Tuple1)
+
+end Tuples
+
+
+/-
+
+# Casts
+
+-/
+section Cast
+
+/-- Hax-introduced explicit cast. It is partial (returns a `Result`) -/
+@[simp, spec]
+def convert_From_from {α β} [Coe α (Result β)] (x:α) : (Result β) := x
+
+/-- Rust-supported casts on base types -/
+class Cast (α β: Type) where
+  cast : α → Result β
+
+/-- Wrapping cast, does not fail on overflow -/
+@[spec]
+instance : Cast i64 i32 where
+  cast x := pure (Int64.toInt32 x)
+
+@[spec]
+instance : Cast i64 (Result i32) where
+  cast x := pure (x.toInt32)
+
+@[spec]
+instance : Cast usize u32 where
+  cast x := pure (USize.toUInt32 x)
+
+@[simp, spec]
+def hax_cast_op {α β} [c: Cast α β] (x:α) : (Result β) := c.cast x
+
+end Cast
+
+
+/-
+
+# Results
+
+Not to be confused with the underlying `Result` monad of the Lean encoding, the
+`result_Result` type models the rust `Result`.
+
+-/
+section RustResult
+
+inductive result_Result α β
+| ok : α -> result_Result α β
+| err : β -> result_Result α β
+
+instance {β : Type} : Monad (fun α => result_Result α β) where
+  pure x := .ok x
+  bind {α α'} x (f: α -> result_Result α' β) := match x with
+  | .ok v => f v
+  | .err e => .err e
+
+/-- Rust unwrapping, panics if `x` is not `result_Result.ok _` -/
+def result_impl_unwrap (α: Type) (β:Type) (x: result_Result α β) : (Result α) :=
+  match x with
+  | .ok v => pure v
+  | .err _ => .fail .panic
+
+end RustResult
+
+
+/-
+
+# Folds
+
+Hax represents for-loops as folds over a range
+
+-/
+section Fold
+
+/--
+
+Hax-introduced function for for-loops, represented as a fold of the body of the
+loop `body` from index `e` to `s`. If the invariant is not checked at runtime,
+only passed around
+
+-/
+def hax_folds_fold_range {α}
+  (s e : Nat)
+  (inv : α -> Nat -> Result Bool)
+  (init: α)
+  (body : α -> Nat -> Result α) : Result α := do
+  if e ≤ s then pure init
+  else hax_folds_fold_range (s+1) e inv (← body init s) body
+
+-- Lemma for proof of hax_folds_fold_range property
+private
+theorem induction_decreasing {e} {P: Nat  → Prop}
+  (init: P e)
+  (rec: ∀ n, n < e → P (n+1) → P n) :
+  ∀ n, n ≤ e → P n
+:= by
+  intros n h
+  by_cases (n = 0)
+  . subst_vars
+    induction e <;> try grind
+  generalize h: (e - n) = d
+  have : n = e - d := by omega
+  have hlt : d < e := by omega
+  rw [this] ; clear h this
+  induction d with
+  | zero => simp ; grind
+  | succ d ih =>
+    apply rec <;> try omega
+    suffices e - (d + 1) + 1 = e - d by grind
+    omega
+
+-- Lemma for proof of hax_folds_fold_range property
+private
+def induction_decreasing_range {s e} {P: Nat → Nat → Prop} :
+  s ≤ e →
+  (init: P e e) →
+  (rec: ∀ (n : Nat), n < e → s ≤ n → P (n + 1) e → P n e) →
+  P s e
+:= by intros; apply induction_decreasing (P := fun n => (s ≤ n → P n e)) (e := e) <;> try grind
+
+/--
+
+Nat-based specification for hax_folds_fold_range. It requires that the invariant
+holds on the initial value, and that for any index `i` between the start and end
+values, executing body of the loop on a value that satisfies the invariant
+produces a result that also satisfies the invariant.
+
+-/
+@[spec]
+theorem hax_folds_fold_range_spec {α}
+  (s e : Nat)
+  (inv : α -> Nat -> Result Bool)
+  (init: α)
+  (body : α -> Nat -> Result α) :
+  ⦃ inv init s = pure true ∧
+    s ≤ e ∧
+    ∀ (acc:α) (i:Nat), s ≤ i → i < e →
+             ⦃ inv acc i = pure true ⦄
+             (body acc i)
+             ⦃ ⇓ res => inv res (i+1) = pure true ⦄
+  ⦄
+  (hax_folds_fold_range s e inv init body)
+  ⦃ ⇓ r => inv r e = pure true ⦄
+:= by
+  intro ⟨ h_inv_s, h_s_le_e , h_body ⟩
+  revert h_inv_s init
+  have :=  induction_decreasing_range (s := s) (e := e)
+    (P := fun s e =>
+      ∀ acc, inv acc s = pure true →
+      wp⟦hax_folds_fold_range s e inv acc body⟧ ⇓ r => inv r e = pure true)
+  apply this <;> clear this <;> try omega
+  . simp [hax_folds_fold_range]
+  . intros n _ _ ih acc h_acc
+    unfold hax_folds_fold_range
+    mvcgen <;> try grind
+    specialize h_body acc n (by omega) (by omega)
+    mspec h_body
+    intro h_r
+    apply (ih _ h_r)
+
+
+end Fold
+
+/-
+
+# Arrays
+
+Rust arrays, are represented as Lean `Vector` (Lean Arrays of known size)
+
+-/
+section Array
+
+inductive array_TryFromSliceError where
+  | array_TryFromSliceError
+
+def hax_monomorphized_update_at_update_at_usize {α n}
+  (a: Vector α n) (i:Nat) (v:α) : Result (Vector α n) :=
+  if h: i < a.size then
+    pure ( Vector.set a i v )
+  else
+    .fail (.arrayOutOfBounds)
+
+@[spec]
+def hax_update_at {α n} (m : Vector α n) (i : Nat) (v : α) : Result (Vector α n) :=
+  if i < n then
+    pure ( Vector.setIfInBounds m i v)
+  else
+    .fail (.arrayOutOfBounds)
+
+@[spec]
+def hax_repeat {α} (v:α) (n:Nat) : Result (Vector α n) :=
+  pure (Vector.replicate n v)
+
+def convert_TryInto_try_into {α n} (a: Array α) :
+   Result (result_Result (Vector α n) array_TryFromSliceError) :=
+   pure (
+     if h: a.size = n then
+       result_Result.ok (Eq.mp (congrArg _ h) a.toVector)
+     else
+       .err .array_TryFromSliceError
+     )
+
+end Array
+
+/-
+
+# Ranges
+
+-/
+
+/-- Type of ranges -/
+inductive ops_range_Range (α: Type)  where
+| range (r_start r_end : α) : ops_range_Range α
+
+@[simp, spec]
+def constr_ops_range_Range {α} (ops_range_Range_start : α) (ops_range_Range_end : α) :=
+  ops_range_Range.range ops_range_Range_start ops_range_Range_end
+
+
+/-
+
+# Polymorphic index access
+
+Hax introduces polymorphic index accesses, for any integer type (returning a
+single value) and for ranges (returning an array of values). A typeclass-based
+notation `a[i]_?` is introduced to support panicking lookups
+
+-/
+section Lookup
+
+/--
+The classes `GetElemResult` implement lookup notation `xs[i]_?`.
+-/
+class GetElemResult (coll : Type u) (idx : Type v) (elem : outParam (Type w)) where
+  /--
+  The syntax `arr[i]_?` gets the `i`'th element of the collection `arr`. It
+  can panic if the index is out of bounds.
+  -/
+  getElemResult (xs : coll) (i : idx) : Result elem
+
+export GetElemResult (getElemResult)
+
+@[inherit_doc getElemResult]
+syntax:max term noWs "[" withoutPosition(term) "]" noWs "_?": term
+macro_rules | `($x[$i]_?) => `(getElemResult $x $i)
+
+@[app_unexpander getElemResult] meta def unexpandGetElemResult : Lean.PrettyPrinter.Unexpander
+  | `($_ $array $index) => `($array[$index]_?)
+  | _ => throw ()
+
+/--
+
+Until the backend introduces notations, a definition for the explicit name
+`ops_index_index_index` is provided as a proxy
+
+-/
+@[simp, spec]
+def ops_index_Index_index {α β γ} (a: α) (i:β) [GetElemResult α β γ] : (Result γ) := a[i]_?
+
+
+instance Range.instGetElemResultArrayUSize :
+  GetElemResult
+    (Array α)
+    (ops_range_Range usize)
+    (Array α) where
+  getElemResult xs i := match i with
+  | ops_range_Range.range s e =>
+    let size := xs.size;
+    if s ≤ e && e ≤ size then
+      pure ( xs.extract s e )
+    else
+      Result.fail Error.arrayOutOfBounds
+
+instance Range.instGetElemResultVectorUSize :
+  GetElemResult
+    (Vector α n)
+    (ops_range_Range usize)
+    (Array α) where
+  getElemResult xs i := match i with
+  | ops_range_Range.range s e =>
+    if s ≤ e && e ≤ n then
+      pure (xs.extract s e).toArray
+    else
+      Result.fail Error.arrayOutOfBounds
+
+
+instance USize.instGetElemResultArray {α} : GetElemResult (Array α) usize α where
+  getElemResult xs i :=
+    if h: i.toNat < xs.size then pure (xs[i])
+    else .fail arrayOutOfBounds
+
+instance USize.instGetElemResultVector {α n} : GetElemResult (Vector α n) usize α where
+  getElemResult xs i :=
+    if h: i.toNat < n then pure (xs[i.toNat])
+    else .fail arrayOutOfBounds
+
+instance Nat.instGetElemResultArray {α} : GetElemResult (Array α) Nat α where
+  getElemResult xs i :=
+    if h: i < xs.size then pure (xs[i])
+    else .fail arrayOutOfBounds
+
+instance Nat.instGetElemResultVector {α n} : GetElemResult (Vector α n) Nat α where
+  getElemResult xs i :=
+    if h: i < n then pure (xs[i])
+    else .fail arrayOutOfBounds
+
+@[spec]
+theorem Nat.getElemArrayResult_spec
+  (α : Type) (a: Array α) (i: Nat):
+  ⦃ i < a.size ⦄
+  ( a[i]_? )
+  ⦃ ⇓ r => a[i]? = some r ⦄
+:= by
+  mvcgen [Result.ofOption, Nat.instGetElemResultArray]
+  simp
+
+@[spec]
+theorem Nat.getElemVectorResult_spec
+  (α : Type) (n:Nat) (a: Vector α n) (i: Nat):
+  ⦃ i < n ⦄
+  ( a[i]_? )
+  ⦃ ⇓ r => a[i]? = some r ⦄
+:= by
+  mvcgen [Nat.instGetElemResultVector]
+  simp
+
+@[spec]
+theorem USize.getElemArrayResult_spec
+  (α : Type) (a: Array α) (i: usize):
+  ⦃ i.toNat < a.size ⦄
+  ( a[i]_? )
+  ⦃ ⇓ r => a[i.toNat]? = some r ⦄
+:= by
+  mvcgen [USize.instGetElemResultArray]
+  simp
+
+@[spec]
+theorem USize.getElemVectorResult_spec
+  (α : Type) (n:Nat) (a: Vector α n) (i: usize):
+  ⦃ i.toNat < n ⦄
+  ( a[i]_? )
+  ⦃ ⇓ r => a[i.toNat]? = some r ⦄
+:= by
+  mvcgen [USize.instGetElemResultVector]
+  simp
+
+@[spec]
+theorem Range.getElemArrayUSize_spec
+  (α : Type) (a: Array α) (s e: usize) :
+  ⦃ s ≤ e ∧ e ≤ a.size ⦄
+  ( a[(ops_range_Range.range s e)]_? )
+  ⦃ ⇓ r => r = Array.extract a s e ⦄
+:= by
+  mvcgen [ops_index_Index_index, Range.instGetElemResultArrayUSize] <;> grind
+
+@[spec]
+theorem Range.getElemVectorUSize_spec
+  (α : Type) (n: Nat) (a: Vector α n) (s e: usize) :
+  ⦃ s ≤ e ∧ e ≤ n ⦄
+  ( a[(ops_range_Range.range s e)]_? )
+  ⦃ ⇓ r => r = (Vector.extract a s e).toArray ⦄
+:= by
+  mvcgen [ops_index_Index_index, Range.instGetElemResultVectorUSize] <;> grind
+
+
+end Lookup
+
+
+
+/-
+
+# Slices
+
+Rust slices are represented as Lean Arrays (variable size)
+
+-/
+
+
+@[spec]
+def unsize {α n} (a: Vector α n) : Result (Array α) :=
+  pure (a.toArray)
+
+def slice_impl_len α (a: Array α) : Result usize := pure a.size
+
+/-
+
+# Vectors
+
+Rust vectors are represented as Lean Arrays (variable size)
+
+-/
+section RustVectors
+
+def alloc_Global : Type := Unit
+def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α
+
+def vec_impl_new (α: Type) (Allocator:Type) : Result (vec_Vec α Allocator) :=
+  pure ((List.nil).toArray)
+
+def vec__1_impl_len (α: Type) (Allocator:Type) (x: vec_Vec α Allocator) : Result Nat :=
+  pure x.size
+
+def vec__2_impl_extend_from_slice (α Allocator) (x: vec_Vec α Allocator) (y: Array α)
+  : Result (vec_Vec α Allocator):=
+  pure (x.append y)
+
+def slice_impl_to_vec α (a:  Array α) : Result (vec_Vec α alloc_Global) :=
+  pure a
+
+-- For
+instance {α n} : Coe (Array α) (Result (Vector α n)) where
+  coe x :=
+    if h: x.size = n then by
+      rw [←h]
+      apply pure
+      apply (Array.toVector x)
+    else .fail (.arrayOutOfBounds)
+
+end RustVectors
+
+
+
+/-
+
+# Closures
+
+Rust closures are represented as regular Lean functions. Yet, Rust uses a
+typeclass `Fn` when calling a closure, which uncurrifies the arguments. This is
+taken care of by the `Fn` class
+
+-/
+
+class Fn α (β : outParam Type) γ where
+  call : α → β → γ
+
+instance {α β} : Fn (α → β) (hax_Tuple1 α) β where
+  call f x := f x.fst
+
+instance {α β γ} : Fn (α → β → γ) (hax_Tuple2 α β) γ where
+  call f x := f x.fst x.snd
+
+def ops_function_Fn_call {α β γ} [Fn α β γ] (f: α) (x: β) : γ := Fn.call f x
+
+
+-- Miscellaneous
+def ops_deref_Deref_deref {α Allocator} (v: vec_Vec α Allocator)
+  : Result (Array α)
+  := pure v
+
+
+-- Tactics
+macro "hax_bv_decide" : tactic => `(tactic| (
+  any_goals (injections <;> subst_vars)
+  all_goals try (
+    simp [Int32.eq_iff_toBitVec_eq,
+          Int32.lt_iff_toBitVec_slt,
+          Int32.le_iff_toBitVec_sle,
+          Int64.eq_iff_toBitVec_eq,
+          Int64.lt_iff_toBitVec_slt,
+          Int64.le_iff_toBitVec_sle] at * <;>
+    bv_decide;
+    done
+ )))
diff --git a/rust-engine/src/ast/identifiers.rs b/rust-engine/src/ast/identifiers.rs
index e8e04bc68..203169ed8 100644
--- a/rust-engine/src/ast/identifiers.rs
+++ b/rust-engine/src/ast/identifiers.rs
@@ -102,6 +102,12 @@ pub mod global_id {
             }
         }
 
+        /// Tests if the raw output is reduced to "_". Should be used only for
+        /// testing. See https://github.com/cryspen/hax/issues/1599
+        pub fn is_empty(&self) -> bool {
+            self.to_debug_string() == "_".to_string()
+        }
+
         /// Extract the raw `DefId` from a `GlobalId`.
         /// This should never be used for name printing.
         pub fn def_id(&self) -> DefId {
@@ -109,7 +115,8 @@ pub mod global_id {
             concrete_id.def_id.def_id.clone()
         }
 
-        /// Raw printing of identifier separated by underscore. Used for testing
+        /// Raw printing of identifier separated by underscore. Should be used
+        /// only for testing. See https://github.com/cryspen/hax/issues/1599
         pub fn to_debug_string(&self) -> String {
             match self {
                 GlobalId::Concrete(concrete_id) => concrete_id
@@ -118,12 +125,20 @@ pub mod global_id {
                     .clone()
                     .path
                     .into_iter()
-                    .map(|def| match def.clone().data {
-                        hax_frontend_exporter::DefPathItem::ValueNs(s)
-                        | hax_frontend_exporter::DefPathItem::MacroNs(s)
-                        | hax_frontend_exporter::DefPathItem::TypeNs(s) => s.clone(),
-                        hax_frontend_exporter::DefPathItem::Impl => "impl".to_string(),
-                        other => unimplemented!("{other:?}"),
+                    .map(|def| {
+                        let data = match def.clone().data {
+                            hax_frontend_exporter::DefPathItem::ValueNs(s)
+                            | hax_frontend_exporter::DefPathItem::MacroNs(s)
+                            | hax_frontend_exporter::DefPathItem::TypeNs(s) => s.clone(),
+                            hax_frontend_exporter::DefPathItem::Impl => "impl".to_string(),
+                            other => unimplemented!("{other:?}"),
+                        };
+                        if def.disambiguator != 0 && !data.is_empty() && data != "_" {
+                            // Don't print disambiguator of empty data
+                            format!("_{}_{}", def.disambiguator, data)
+                        } else {
+                            data
+                        }
                     })
                     .collect::<Vec<String>>()
                     .join("_"),
diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs
index a1ef7412d..2c6280e27 100644
--- a/rust-engine/src/lean.rs
+++ b/rust-engine/src/lean.rs
@@ -6,7 +6,6 @@
 
 use crate::ast::span::Span;
 use crate::printer::Allocator;
-use std::iter::once;
 
 use pretty::{DocAllocator, DocBuilder, Pretty, docs};
 
@@ -16,7 +15,12 @@ use crate::ast::*;
 
 macro_rules! print_todo {
     ($allocator:ident) => {
-        $allocator.text(format!("Todo at {}", line!())).parens()
+        $allocator
+            .text(format!(
+                "/- Unsupported by the Lean Backend (line {}) -/",
+                line!()
+            ))
+            .parens()
     };
 }
 
@@ -25,6 +29,35 @@ const INDENT: isize = 2;
 /// Placeholder structure for lean printer
 pub struct Lean;
 
+impl Lean {
+    /// A filter for items blacklisted by the Lean backend : returns false if
+    /// the item is definitely not printable, but might return true on
+    /// unsupported items
+    pub fn printable_item(item: &Item) -> bool {
+        match &item.kind {
+            // Anonymous consts
+            ItemKind::Fn {
+                name,
+                generics: _,
+                body: _,
+                params: _,
+                safety: _,
+            } if name.is_empty() => false,
+            // Other unprintable items
+            ItemKind::Error(_) | ItemKind::NotImplementedYet | ItemKind::Use { .. } => false,
+            // Printable items
+            ItemKind::Fn { .. }
+            | ItemKind::TyAlias { .. }
+            | ItemKind::Type { .. }
+            | ItemKind::Trait { .. }
+            | ItemKind::Impl { .. }
+            | ItemKind::Alias { .. }
+            | ItemKind::Resugared(_)
+            | ItemKind::Quote { .. } => true,
+        }
+    }
+}
+
 impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b Item {
     fn pretty(self, allocator: &'a Allocator<Lean>) -> DocBuilder<'a, Allocator<Lean>, Span> {
         self.kind.pretty(allocator)
@@ -36,28 +69,77 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ItemKind {
         match self {
             ItemKind::Fn {
                 name,
-                generics: _,
+                generics,
                 body,
                 params,
                 safety: _,
             } => {
-                // Generics are ignored for now
-                docs![
-                    allocator,
-                    "def ",
-                    name,
-                    allocator.softline(),
-                    allocator
-                        .intersperse(params, allocator.line())
-                        .align()
-                        .group(),
-                    docs![allocator, allocator.line(), ": ", &body.ty].group(),
-                    " :=",
-                    allocator.line(),
-                    docs![allocator, &*body.kind].group()
-                ]
-                .nest(INDENT)
-                .group()
+                match &*body.kind {
+                    ExprKind::Literal(l) => {
+                        // Literal consts, printed without monadic encoding
+                        // Todo: turn it into a proper refactor (see Hax issue #1542)
+                        docs![
+                            allocator,
+                            "def ",
+                            name,
+                            allocator.reflow(" : "),
+                            &body.ty,
+                            allocator.reflow(" :="),
+                            allocator.line(),
+                            l
+                        ]
+                        .group()
+                    }
+                    _ => {
+                        // Normal definition
+                        let generics = if generics.params.is_empty() {
+                            None
+                        } else {
+                            Some(
+                                docs![
+                                    allocator,
+                                    allocator.line(),
+                                    allocator
+                                        .intersperse(&generics.params, allocator.softline())
+                                        .braces()
+                                        .group()
+                                ]
+                                .group(),
+                            )
+                        };
+                        let args = if params.is_empty() {
+                            allocator.nil()
+                        } else {
+                            docs![
+                                allocator,
+                                allocator.line(),
+                                allocator.intersperse(params, allocator.softline()),
+                            ]
+                            .nest(INDENT)
+                            .group()
+                        };
+                        docs![
+                            allocator,
+                            "def ",
+                            name,
+                            generics,
+                            args,
+                            docs![
+                                allocator,
+                                allocator.line(),
+                                ": ",
+                                docs![allocator, "Result ", &body.ty].group()
+                            ]
+                            .group(),
+                            " := do",
+                            allocator.line(),
+                            docs![allocator, &*body.kind].group()
+                        ]
+                        .nest(INDENT)
+                        .group()
+                        .append(allocator.hardline())
+                    }
+                }
             }
             ItemKind::TyAlias {
                 name,
@@ -89,13 +171,10 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ItemKind {
                 is_external: _,
                 rename: _,
             } => allocator.nil(),
-            ItemKind::Quote {
-                quote: _,
-                origin: _,
-            } => print_todo!(allocator),
+            ItemKind::Quote { quote, origin: _ } => quote.pretty(allocator),
             ItemKind::Error(_diagnostic) => print_todo!(allocator),
             ItemKind::Resugared(_resugared_ty_kind) => print_todo!(allocator),
-            ItemKind::NotImplementedYet => allocator.text("-- unimplemented yet"),
+            ItemKind::NotImplementedYet => allocator.text("/- unsupported by Hax engine (yet) -/"),
         }
     }
 }
@@ -118,16 +197,21 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b TyKind {
                     head.pretty(allocator)
                         .append(allocator.softline())
                         .append(allocator.intersperse(args, allocator.softline()))
-                        .group()
                         .parens()
+                        .group()
                 }
             }
-            TyKind::Arrow { inputs, output } => allocator
-                .intersperse(
-                    inputs.into_iter().chain(once(output)),
-                    allocator.softline().append("-> "),
-                )
-                .parens(),
+            TyKind::Arrow { inputs, output } => docs![
+                allocator,
+                allocator.concat(inputs.into_iter().map(|input| docs![
+                    allocator,
+                    input,
+                    allocator.reflow(" -> ")
+                ])),
+                "Result ",
+                output
+            ]
+            .parens(),
             TyKind::Ref {
                 inner: _,
                 mutable: _,
@@ -176,7 +260,14 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b Expr {
 
 impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b Pat {
     fn pretty(self, allocator: &'a Allocator<Lean>) -> DocBuilder<'a, Allocator<Lean>, Span> {
-        (self.kind).pretty(allocator)
+        docs![
+            allocator,
+            self.kind.pretty(allocator),
+            allocator.reflow(" : "),
+            &self.ty
+        ]
+        .parens()
+        .group()
     }
 }
 
@@ -184,11 +275,7 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b PatKind {
     fn pretty(self, allocator: &'a Allocator<Lean>) -> DocBuilder<'a, Allocator<Lean>, Span> {
         match self {
             PatKind::Wild => allocator.text("_"),
-            PatKind::Ascription { pat, ty } => {
-                docs![allocator, pat, allocator.softline(), ": ", ty]
-                    .nest(INDENT)
-                    .group()
-            }
+            PatKind::Ascription { pat, ty: _ } => pat.kind.pretty(allocator),
             PatKind::Or { sub_pats: _ } => print_todo!(allocator),
             PatKind::Array { args: _ } => print_todo!(allocator),
             PatKind::Deref { sub_pat: _ } => print_todo!(allocator),
@@ -228,16 +315,29 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
                 then,
                 else_,
             } => match else_ {
-                Some(else_branch) => allocator
-                    .concat([
-                        allocator.text("if"),
-                        allocator.softline().append(condition).nest(INDENT),
-                        allocator.line().append("then"),
-                        allocator.softline().append(then).nest(INDENT),
-                        allocator.line().append("else"),
-                        allocator.softline().append(else_branch).nest(INDENT),
-                    ])
-                    .group(),
+                Some(else_branch) => docs![
+                    allocator,
+                    allocator
+                        .text("if")
+                        .append(allocator.line())
+                        .append(condition)
+                        .group(),
+                    allocator.line(),
+                    allocator
+                        .text("then")
+                        .append(allocator.line())
+                        .append(then)
+                        .group()
+                        .nest(INDENT),
+                    allocator.line(),
+                    allocator
+                        .text("else")
+                        .append(allocator.line())
+                        .append(else_branch)
+                        .group()
+                        .nest(INDENT),
+                ]
+                .group(),
                 None => print_todo!(allocator),
             },
             ExprKind::App {
@@ -246,18 +346,58 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
                 generic_args: _,
                 bounds_impls: _,
                 trait_: _,
+            } if match &*head.kind {
+                ExprKind::GlobalId(name) => {
+                    *name == crate::names::rust_primitives::hax::machine_int::add()
+                }
+                _ => false,
+            } && args.len() == 2 =>
+            {
+                docs![
+                    allocator,
+                    "← ",
+                    args.get(0),
+                    allocator.reflow(" +? "),
+                    args.get(1),
+                ]
+                .parens()
+                .group()
+            }
+            ExprKind::App {
+                head,
+                args,
+                generic_args,
+                bounds_impls: _,
+                trait_: _,
             } => {
-                let separator = allocator.line();
-                head.pretty(allocator)
-                    .append(allocator.softline())
-                    .append(allocator.intersperse(args, separator).nest(INDENT))
+                let generic_args = (!generic_args.is_empty()).then_some(
+                    allocator
+                        .line()
+                        .append(
+                            allocator
+                                .intersperse(generic_args, allocator.line())
+                                .nest(INDENT),
+                        )
+                        .group(),
+                );
+                let args = if args.is_empty() {
+                    None
+                } else {
+                    Some(
+                        allocator
+                            .line()
+                            .append(allocator.intersperse(args, allocator.line()).nest(INDENT))
+                            .group(),
+                    )
+                };
+                docs![allocator, "← ", head, generic_args, args]
                     .parens()
                     .group()
             }
             ExprKind::Literal(literal) => literal.pretty(allocator),
             ExprKind::Array(exprs) => docs![
                 allocator,
-                "#[",
+                "#v[",
                 allocator
                     .intersperse(exprs, allocator.text(",").append(allocator.line()))
                     .nest(INDENT),
@@ -272,31 +412,30 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
                 base: _,
             } => {
                 // Should be turned into a resugaring once https://github.com/cryspen/hax/pull/1528 have been merged
-                let record_args = if fields.len() > 0 {
-                    Some(
-                        allocator.softline().append(
+                let record_args = (fields.len() > 0).then_some(
+                    allocator
+                        .line()
+                        .append(
                             allocator
                                 .intersperse(
                                     fields.iter().map(|field: &(GlobalId, Expr)| {
                                         docs![
                                             allocator,
                                             &field.0,
-                                            " ",
-                                            allocator.reflow(":= "),
+                                            allocator.reflow(" := "),
                                             &field.1
                                         ]
+                                        .parens()
                                         .group()
                                     }),
-                                    allocator.reflow(", "),
+                                    allocator.line(),
                                 )
-                                .group()
-                                .braces(),
-                        ),
-                    )
-                } else {
-                    None
-                };
-                docs![allocator, ".constr_", constructor, record_args]
+                                .group(),
+                        )
+                        .group(),
+                );
+                docs![allocator, "constr_", constructor, record_args]
+                    .parens()
                     .group()
                     .nest(INDENT)
             }
@@ -314,25 +453,31 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
                 inner: _,
             } => print_todo!(allocator),
             ExprKind::Deref(_expr) => print_todo!(allocator),
-            ExprKind::Let { lhs, rhs, body } => {
-                docs![
-                    allocator,
-                    "let ",
-                    lhs,
-                    " :=",
-                    allocator.softline(),
-                    docs![allocator, rhs].group(),
-                    ";",
-                    allocator.line(),
-                    body,
-                ]
-            }
+            ExprKind::Let { lhs, rhs, body } => docs![
+                allocator,
+                "let ",
+                lhs,
+                " ←",
+                allocator.softline(),
+                docs![allocator, "pure", allocator.line(), rhs]
+                    .group()
+                    .nest(INDENT),
+                ";",
+                allocator.line(),
+                body,
+            ]
+            .group(),
             ExprKind::GlobalId(global_id) => global_id.pretty(allocator),
             ExprKind::LocalId(local_id) => local_id.pretty(allocator),
-            ExprKind::Ascription { e, ty } => docs![allocator, e, allocator.reflow(" : "), ty]
-                .nest(INDENT)
-                .parens()
-                .group(),
+            ExprKind::Ascription { e, ty } => {
+                let monadic_encoding = match *e.kind {
+                    ExprKind::Literal(_) | ExprKind::Construct { .. } => None,
+                    _ => Some("← "),
+                };
+                docs![allocator, monadic_encoding, e, allocator.reflow(" : "), ty]
+                    .parens()
+                    .group()
+            }
             ExprKind::Assign { lhs: _, value: _ } => print_todo!(allocator),
             ExprKind::Loop {
                 body: _,
@@ -351,19 +496,19 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
             } => docs![
                 allocator,
                 allocator.reflow("fun "),
-                allocator.intersperse(params, allocator.line()),
-                allocator.reflow(" =>"),
+                allocator.intersperse(params, allocator.softline()).group(),
+                allocator.reflow("=> do"),
                 allocator.line(),
                 body
             ]
-            .nest(INDENT)
+            .parens()
             .group()
-            .parens(),
+            .nest(INDENT),
             ExprKind::Block {
                 body: _,
                 safety_mode: _,
             } => print_todo!(allocator),
-            ExprKind::Quote { contents: _ } => print_todo!(allocator),
+            ExprKind::Quote { contents } => allocator.concat(&contents.0),
             ExprKind::Resugared(_resugared_expr_kind) => print_todo!(allocator),
             ExprKind::Error(_diagnostic) => print_todo!(allocator),
         }
@@ -450,9 +595,31 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b GlobalId {
 
 impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b Param {
     fn pretty(self, allocator: &'a Allocator<Lean>) -> DocBuilder<'a, Allocator<Lean>, Span> {
-        docs![allocator, &self.pat, allocator.softline(), ": ", &self.ty]
-            .nest(INDENT)
-            .parens()
-            .group()
+        self.pat.pretty(allocator)
+    }
+}
+
+impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b GenericParam {
+    fn pretty(self, allocator: &'a Allocator<Lean>) -> DocBuilder<'a, Allocator<Lean>, Span> {
+        self.ident.pretty(allocator)
+    }
+}
+
+impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b Quote {
+    fn pretty(self, allocator: &'a Allocator<Lean>) -> DocBuilder<'a, Allocator<Lean>, Span> {
+        allocator.concat(&self.0)
+    }
+}
+
+impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b QuoteContent {
+    fn pretty(self, allocator: &'a Allocator<Lean>) -> DocBuilder<'a, Allocator<Lean>, Span> {
+        match self {
+            QuoteContent::Verbatim(s) => {
+                allocator.intersperse(s.lines().map(|x| x.to_string()), allocator.hardline())
+            }
+            QuoteContent::Expr(expr) => expr.pretty(allocator),
+            QuoteContent::Pattern(pat) => pat.pretty(allocator),
+            QuoteContent::Ty(ty) => ty.pretty(allocator),
+        }
     }
 }
diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs
index b6acccc0c..a78611b16 100644
--- a/rust-engine/src/main.rs
+++ b/rust-engine/src/main.rs
@@ -6,7 +6,7 @@ use hax_rust_engine::{
 };
 use hax_types::{cli_options::Backend, engine_api::File};
 
-use pretty::{DocAllocator, DocBuilder};
+use pretty::{DocAllocator, DocBuilder, docs};
 
 fn krate_name(items: &Vec<Item>) -> String {
     let head_item = items.get(0).unwrap();
@@ -17,24 +17,35 @@ fn lean_backend(items: Vec<Item>) {
     let krate = krate_name(&items);
 
     // For now, the main function always calls the Lean backend
-    let allocator = Allocator::new(Lean);
+    let allocator = &Allocator::new(Lean);
 
-    let header = allocator
-        .intersperse(
-            vec![
-            "-- Experimental lean backend for Hax",
-            "-- Comment the following line to not import the prelude (requires the Lib.lean file) : ",
-            "import Lib",
-        ],
+    let header = docs![
+        allocator,
+        allocator.intersperse(
+            "
+-- Experimental lean backend for Hax
+-- Lib.lean can be found in hax/proof-libs/lean :
+import Lib
+import Std.Tactic.Do
+import Std.Do.Triple
+import Std.Tactic.Do.Syntax
+open Std.Do
+open Std.Tactic
+
+set_option mvcgen.warning false
+set_option linter.unusedVariables false"
+                .lines(),
             allocator.hardline(),
-        )
-        .append(allocator.hardline())
-        .append(allocator.hardline());
+        ),
+        allocator.hardline(),
+        allocator.hardline()
+    ];
 
-    let item_docs: DocBuilder<_, Span> = header.append(allocator.intersperse(
-        items.iter(),
-        allocator.hardline().append(allocator.hardline()),
-    ));
+    let items = items
+        .iter()
+        .filter(|item: &&hax_rust_engine::ast::Item| Lean::printable_item(*item));
+    let item_docs: DocBuilder<_, Span> =
+        header.append(allocator.intersperse(items, allocator.hardline()));
 
     hax_rust_engine::hax_io::write(&hax_types::engine_api::protocol::FromEngine::File(File {
         path: krate + ".lean",
diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap
index de38d8c02..870526afd 100644
--- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
+++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
@@ -28,30 +28,42 @@ diagnostics = []
 
 [stdout.files]
 "lean_tests.lean" = '''
+
 -- Experimental lean backend for Hax
--- Comment the following line to not import the prelude (requires the Lib.lean file) : 
+-- Lib.lean can be found in hax/proof-libs/lean :
 import Lib
+import Std.Tactic.Do
+import Std.Do.Triple
+import Std.Tactic.Do.Syntax
+open Std.Do
+open Std.Tactic
 
+set_option mvcgen.warning false
+set_option linter.unusedVariables false
 
+def FORTYTWO : usize := 42
+def returns42 (_ : hax_Tuple0) : Result usize := do FORTYTWO
 
--- unimplemented yet
-
-def FORTYTWO  : usize := 42
+def add_two_numbers (x : usize) (y : usize) : Result usize := do (← x +? y)
 
-def returns42 (_ : hax_Tuple0) : usize := FORTYTWO
+def letBinding (x : usize) (y : usize) : Result usize := do
+  let (useless : hax_Tuple0) ← pure (constr_hax_Tuple0);
+  let (result1 : usize) ← pure (← x +? y);
+  let (result2 : usize) ← pure (← result1 +? 2); (← result2 +? 1)
 
-def add_two_numbers (x : usize) (y : usize) : usize := (hax_machine_int_add x y)
+def closure (_ : hax_Tuple0) : Result i32 := do
+  let (x : i32) ← pure 41;
+  let (f1 : (i32 -> Result i32)) ← pure (fun (y : i32)=> do (← y +? x));
+  let (f2 : (i32 -> i32 -> Result i32)) ← pure
+    (fun (y : i32) (z : i32)=> do (← (← y +? x) +? z));
+  (← (← ops_function_Fn_call f1 (constr_hax_Tuple1 (hax_Tuple1_Tuple0 := 1))) +?
+  (← ops_function_Fn_call
+  f2
+    (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3))))
 
-def letBinding (x : usize) (y : usize) : usize :=
-  let useless := (.constr_hax_Tuple0 : hax_Tuple0);
-  let result1 := (hax_machine_int_add x y);
-  let result2 := (hax_machine_int_add result1 2);
-  (hax_machine_int_add result2 1)
+@[spec]
+def test_before_verbatime_single_line : u8 := 42
 
-def closure (_ : hax_Tuple0) : i32 :=
-  let x := 41;
-  let f := (fun y => (hax_machine_int_add y x));
-  (ops_function_Fn_call f
-    (.constr_hax_Tuple1 {hax_Tuple1_Tuple0 := 1} : (hax_Tuple1 i32)))
+def multiline : Unit := ()
 
-abbrev UsizeAlias := usize'''
+def test_before_verbatim_multi_line : u8 := 32'''
diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs
index 5cb31301e..f98bc471b 100644
--- a/tests/lean-tests/src/lib.rs
+++ b/tests/lean-tests/src/lib.rs
@@ -19,8 +19,16 @@ fn letBinding(x: usize, y: usize) -> usize {
 
 fn closure() -> i32 {
     let x = 41;
-    let f = |y| y + x;
-    f(1)
+    let f1 = |y| y + x ;
+    let f2 = |y, z| y + x + z;
+    f1(1) + f2(2,3)
 }
 
-type UsizeAlias = usize;
+#[hax_lib::lean::before("@[spec]")]
+fn test_before_verbatime_single_line(x: u8) -> u8 { 42 }
+
+#[hax_lib::lean::before("
+def multiline : Unit := ()
+
+")]
+fn test_before_verbatim_multi_line(x: u8) -> u8 { 32 }