From 9c7f1e0341c90dc89321d2c8e97b0b40a4b40c43 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Fri, 27 Mar 2026 02:39:57 +0700
Subject: [PATCH 1/2] feat: update to lean4:v4.29.0-rc8

---
 Makefile                |   9 +-
 Tutorial.lean           | 375 ---------------------
 Tutorial/Exercises.lean | 727 ++++++++++++++++++++++++----------------
 Tutorial/Solutions.lean | 169 +++++-----
 Tutorial/Tutorial.lean  | 534 ++++++++++++++++-------------
 lake-manifest.json      |  93 ++---
 lakefile.lean           |   8 +-
 lean-toolchain          |   2 +-
 source/Cargo.toml       |   2 +-
 source/src/lib.rs       |  44 ++-
 10 files changed, 925 insertions(+), 1038 deletions(-)
 delete mode 100644 Tutorial.lean

diff --git a/Makefile b/Makefile
index f9f785e..81e9957 100644
--- a/Makefile
+++ b/Makefile
@@ -1,9 +1,10 @@
 .PHONY: all
-all: Tutorial.lean
+all: Tutorial/Tutorial.lean
 
+# run inside of `nix develop` to fix error "install rustup or execute in nix develop"
 .PHONY: tutorial.llbc
 tutorial.llbc:
-	cd source && ../charon/bin/charon --hide-marker-traits --dest ../
+	cd source && nix develop ../../charon --command bash -c "../../charon/bin/charon cargo --preset=aeneas --hide-marker-traits --dest ../"
 
-Tutorial.lean: tutorial.llbc
-	aeneas/bin/aeneas -backend lean tutorial.llbc
+Tutorial/Tutorial.lean: tutorial.llbc
+	../aeneas/bin/aeneas -backend lean tutorial.llbc -dest ./Tutorial
diff --git a/Tutorial.lean b/Tutorial.lean
deleted file mode 100644
index 0c75089..0000000
--- a/Tutorial.lean
+++ /dev/null
@@ -1,375 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [tutorial]
-import Base
-open Primitives
-set_option linter.dupNamespace false
-set_option linter.hashCommand false
-set_option linter.unusedVariables false
-
-namespace tutorial
-
-/- [tutorial::choose]:
-   Source: 'src/lib.rs', lines 1:0-7:1 -/
-def choose
-  {T : Type} (b : Bool) (x : T) (y : T) : Result (T × (T → (T × T))) :=
-  if b
-  then let back := fun ret => (ret, y)
-       Result.ok (x, back)
-  else let back := fun ret => (x, ret)
-       Result.ok (y, back)
-
-/- [tutorial::mul2_add1]:
-   Source: 'src/lib.rs', lines 9:0-11:1 -/
-def mul2_add1 (x : U32) : Result U32 :=
-  do
-  let i ← x + x
-  i + 1#u32
-
-/- [tutorial::mul2_add1_add]:
-   Source: 'src/lib.rs', lines 13:0-15:1 -/
-def mul2_add1_add (x : U32) (y : U32) : Result U32 :=
-  do
-  let i ← mul2_add1 x
-  i + y
-
-/- [tutorial::incr]:
-   Source: 'src/lib.rs', lines 17:0-19:1 -/
-def incr (x : U32) : Result U32 :=
-  x + 1#u32
-
-/- [tutorial::use_incr]:
-   Source: 'src/lib.rs', lines 21:0-26:1 -/
-def use_incr : Result Unit :=
-  do
-  let x ← incr 0#u32
-  let x1 ← incr x
-  let _ ← incr x1
-  Result.ok ()
-
-/- [tutorial::CList]
-   Source: 'src/lib.rs', lines 30:0-33:1 -/
-inductive CList (T : Type) :=
-| CCons : T → CList T → CList T
-| CNil : CList T
-
-/- [tutorial::list_nth]:
-   Source: 'src/lib.rs', lines 35:0-48:1 -/
-divergent def list_nth {T : Type} (l : CList T) (i : U32) : Result T :=
-  match l with
-  | CList.CCons x tl =>
-    if i = 0#u32
-    then Result.ok x
-    else do
-         let i1 ← i - 1#u32
-         list_nth tl i1
-  | CList.CNil => Result.fail .panic
-
-/- [tutorial::list_nth_mut]:
-   Source: 'src/lib.rs', lines 50:0-63:1 -/
-divergent def list_nth_mut
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
-  match l with
-  | CList.CCons x tl =>
-    if i = 0#u32
-    then let back := fun ret => CList.CCons ret tl
-         Result.ok (x, back)
-    else
-      do
-      let i1 ← i - 1#u32
-      let (t, list_nth_mut_back) ← list_nth_mut tl i1
-      let back := fun ret => let tl1 := list_nth_mut_back ret
-                             CList.CCons x tl1
-      Result.ok (t, back)
-  | CList.CNil => Result.fail .panic
-
-/- [tutorial::list_nth1]: loop 0:
-   Source: 'src/lib.rs', lines 66:4-74:1 -/
-divergent def list_nth1_loop {T : Type} (l : CList T) (i : U32) : Result T :=
-  match l with
-  | CList.CCons x tl =>
-    if i = 0#u32
-    then Result.ok x
-    else do
-         let i1 ← i - 1#u32
-         list_nth1_loop tl i1
-  | CList.CNil => Result.fail .panic
-
-/- [tutorial::list_nth1]:
-   Source: 'src/lib.rs', lines 65:0-74:1 -/
-@[reducible]
-def list_nth1 {T : Type} (l : CList T) (i : U32) : Result T :=
-  list_nth1_loop l i
-
-/- [tutorial::i32_id]:
-   Source: 'src/lib.rs', lines 76:0-83:1 -/
-divergent def i32_id (i : I32) : Result I32 :=
-  if i = 0#i32
-  then Result.ok 0#i32
-  else do
-       let i1 ← i - 1#i32
-       let i2 ← i32_id i1
-       i2 + 1#i32
-
-/- [tutorial::even]:
-   Source: 'src/lib.rs', lines 85:0-92:1 -/
-mutual divergent def even (i : U32) : Result Bool :=
-  if i = 0#u32
-  then Result.ok true
-  else do
-       let i1 ← i - 1#u32
-       odd i1
-
-/- [tutorial::odd]:
-   Source: 'src/lib.rs', lines 94:0-101:1 -/
-divergent def odd (i : U32) : Result Bool :=
-  if i = 0#u32
-  then Result.ok false
-  else do
-       let i1 ← i - 1#u32
-       even i1
-
-end
-
-/- Trait declaration: [tutorial::Counter]
-   Source: 'src/lib.rs', lines 105:0-107:1 -/
-structure Counter (Self : Type) where
-  incr : Self → Result (Usize × Self)
-
-/- [tutorial::{tutorial::Counter for usize}::incr]:
-   Source: 'src/lib.rs', lines 110:4-114:5 -/
-def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
-  do
-  let self1 ← self + 1#usize
-  Result.ok (self, self1)
-
-/- Trait implementation: [tutorial::{tutorial::Counter for usize}]
-   Source: 'src/lib.rs', lines 109:0-115:1 -/
-@[reducible]
-def CounterUsize : Counter Usize := {
-  incr := CounterUsize.incr
-}
-
-/- [tutorial::use_counter]:
-   Source: 'src/lib.rs', lines 117:0-119:1 -/
-def use_counter
-  {T : Type} (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
-  CounterInst.incr cnt
-
-/- [tutorial::list_nth_mut1]: loop 0:
-   Source: 'src/lib.rs', lines 124:4-132:1 -/
-divergent def list_nth_mut1_loop
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
-  match l with
-  | CList.CCons x tl =>
-    if i = 0#u32
-    then let back := fun ret => CList.CCons ret tl
-         Result.ok (x, back)
-    else
-      do
-      let i1 ← i - 1#u32
-      let (t, back) ← list_nth_mut1_loop tl i1
-      let back1 := fun ret => let tl1 := back ret
-                              CList.CCons x tl1
-      Result.ok (t, back1)
-  | CList.CNil => Result.fail .panic
-
-/- [tutorial::list_nth_mut1]:
-   Source: 'src/lib.rs', lines 123:0-132:1 -/
-@[reducible]
-def list_nth_mut1
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
-  list_nth_mut1_loop l i
-
-/- [tutorial::list_tail]: loop 0:
-   Source: 'src/lib.rs', lines 135:4-137:5 -/
-divergent def list_tail_loop
-  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) :=
-  match l with
-  | CList.CCons t tl =>
-    do
-    let (c, back) ← list_tail_loop tl
-    let back1 := fun ret => let tl1 := back ret
-                            CList.CCons t tl1
-    Result.ok (c, back1)
-  | CList.CNil => let back := fun ret => ret
-                  Result.ok (CList.CNil, back)
-
-/- [tutorial::list_tail]:
-   Source: 'src/lib.rs', lines 134:0-139:1 -/
-@[reducible]
-def list_tail
-  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) :=
-  list_tail_loop l
-
-/- [tutorial::append_in_place]:
-   Source: 'src/lib.rs', lines 141:0-144:1 -/
-def append_in_place
-  {T : Type} (l0 : CList T) (l1 : CList T) : Result (CList T) :=
-  do
-  let (_, list_tail_back) ← list_tail l0
-  Result.ok (list_tail_back l1)
-
-/- [tutorial::reverse]: loop 0:
-   Source: 'src/lib.rs', lines 148:4-152:5 -/
-divergent def reverse_loop
-  {T : Type} (l : CList T) (out : CList T) : Result (CList T) :=
-  match l with
-  | CList.CCons hd tl => reverse_loop tl (CList.CCons hd out)
-  | CList.CNil => Result.ok out
-
-/- [tutorial::reverse]:
-   Source: 'src/lib.rs', lines 146:0-154:1 -/
-def reverse {T : Type} (l : CList T) : Result (CList T) :=
-  reverse_loop l CList.CNil
-
-/- [tutorial::zero]: loop 0:
-   Source: 'src/lib.rs', lines 164:4-167:5 -/
-divergent def zero_loop
-  (x : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
-  let i1 := alloc.vec.Vec.len x
-  if i < i1
-  then
-    do
-    let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
-    let i2 ← i + 1#usize
-    let x1 := index_mut_back 0#u32
-    zero_loop x1 i2
-  else Result.ok x
-
-/- [tutorial::zero]:
-   Source: 'src/lib.rs', lines 162:0-168:1 -/
-def zero (x : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
-  zero_loop x 0#usize
-
-/- [tutorial::add_no_overflow]: loop 0:
-   Source: 'src/lib.rs', lines 177:4-180:5 -/
-divergent def add_no_overflow_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize) :
-  Result (alloc.vec.Vec U32)
-  :=
-  let i1 := alloc.vec.Vec.len x
-  if i < i1
-  then
-    do
-    let i2 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
-    let (i3, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
-    let i4 ← i3 + i2
-    let i5 ← i + 1#usize
-    let x1 := index_mut_back i4
-    add_no_overflow_loop x1 y i5
-  else Result.ok x
-
-/- [tutorial::add_no_overflow]:
-   Source: 'src/lib.rs', lines 175:0-181:1 -/
-def add_no_overflow
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (alloc.vec.Vec U32)
-  :=
-  add_no_overflow_loop x y 0#usize
-
-/- [tutorial::add_with_carry]: loop 0:
-   Source: 'src/lib.rs', lines 190:4-197:5 -/
-divergent def add_with_carry_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (c0 : U8) (i : Usize) :
-  Result (U8 × (alloc.vec.Vec U32))
-  :=
-  let i1 := alloc.vec.Vec.len x
-  if i < i1
-  then
-    do
-    let i2 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) x i
-    let i3 ← Scalar.cast .U32 c0
-    let p ← core.num.U32.overflowing_add i2 i3
-    let (sum, c1) := p
-    let i4 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
-    let p1 ← core.num.U32.overflowing_add sum i4
-    let (sum1, c2) := p1
-    let i5 ← Scalar.cast_bool .U8 c1
-    let i6 ← Scalar.cast_bool .U8 c2
-    let c01 ← i5 + i6
-    let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
-    let i7 ← i + 1#usize
-    let x1 := index_mut_back sum1
-    add_with_carry_loop x1 y c01 i7
-  else Result.ok (c0, x)
-
-/- [tutorial::add_with_carry]:
-   Source: 'src/lib.rs', lines 186:0-199:1 -/
-def add_with_carry
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (U8 × (alloc.vec.Vec U32))
-  :=
-  add_with_carry_loop x y 0#u8 0#usize
-
-/- [tutorial::max]:
-   Source: 'src/lib.rs', lines 201:0-203:1 -/
-def max (x : Usize) (y : Usize) : Result Usize :=
-  if x > y
-  then Result.ok x
-  else Result.ok y
-
-/- [tutorial::get_or_zero]:
-   Source: 'src/lib.rs', lines 205:0-207:1 -/
-def get_or_zero (y : alloc.vec.Vec U32) (i : Usize) : Result U32 :=
-  let i1 := alloc.vec.Vec.len y
-  if i < i1
-  then alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
-  else Result.ok 0#u32
-
-/- [tutorial::add]: loop 0:
-   Source: 'src/lib.rs', lines 221:4-229:5 -/
-divergent def add_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (max1 : Usize) (c0 : U8)
-  (i : Usize) :
-  Result (alloc.vec.Vec U32)
-  :=
-  if i < max1
-  then
-    do
-    let yi ← get_or_zero y i
-    let i1 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) x i
-    let i2 ← Scalar.cast .U32 c0
-    let p ← core.num.U32.overflowing_add i1 i2
-    let (sum, c1) := p
-    let p1 ← core.num.U32.overflowing_add sum yi
-    let (sum1, c2) := p1
-    let i3 ← Scalar.cast_bool .U8 c1
-    let i4 ← Scalar.cast_bool .U8 c2
-    let c01 ← i3 + i4
-    let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
-    let i5 ← i + 1#usize
-    let x1 := index_mut_back sum1
-    add_loop x1 y max1 c01 i5
-  else
-    if c0 != 0#u8
-    then do
-         let i1 ← Scalar.cast .U32 c0
-         alloc.vec.Vec.push x i1
-    else Result.ok x
-
-/- [tutorial::add]:
-   Source: 'src/lib.rs', lines 214:0-235:1 -/
-def add
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (alloc.vec.Vec U32)
-  :=
-  do
-  let i := alloc.vec.Vec.len x
-  let i1 := alloc.vec.Vec.len y
-  let max1 ← max i i1
-  let x1 ← alloc.vec.Vec.resize core.clone.CloneU32 x max1 0#u32
-  add_loop x1 y max1 0#u8 0#usize
-
-end tutorial
diff --git a/Tutorial/Exercises.lean b/Tutorial/Exercises.lean
index c638f1a..d2557f8 100644
--- a/Tutorial/Exercises.lean
+++ b/Tutorial/Exercises.lean
@@ -1,5 +1,7 @@
-import Base
-open Primitives Result
+import Aeneas
+import Aeneas.Data.List
+import Aesop
+open Aeneas Aeneas.Std Result ControlFlow Error List
 
 set_option maxHeartbeats 1000000
 
@@ -9,46 +11,36 @@ end Primitives
 
 namespace Tutorial.Solutions
 
-/- [tutorial::mul2_add1]:
-   Source: 'src/lib.rs', lines 11:0-11:31 -/
-def mul2_add1 (x : U32) : Result U32 :=
-  do
+/-- [tutorial::mul2_add1]:
+    Source: 'src/lib.rs', lines 9:0-11:1 -/
+def mul2_add1 (x : Std.U32) : Result Std.U32 := do
   let i ← x + x
   i + 1#u32
 
-#check U32.add_spec
+/-- info: Aeneas.Std.U32.add_spec {x y : U32} (hmax : ↑x + ↑y ≤ U32.max) : x + y ⦃ z => ↑z = ↑x + ↑y ⦄ -/
+#guard_msgs in #check U32.add_spec
 
-/-- Theorem about `mul2_add1`: without the `progress` tactic -/
+/-- Theorem about `mul2_add1`: without the `step` tactic -/
 theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
-  : ∃ y, mul2_add1 x = ok y ∧
-  ↑y = 2 * ↑x + (1 : Int)
+  : mul2_add1 x ⦃ y => ↑y = 2 * ↑x + (1 : Int) ⦄
   := by
   sorry
 
-/-- Theorem about `mul2_add1`: with the `progress` tactic -/
--- @[pspec]
-theorem mul2_add1_spec' (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
-  : ∃ y, mul2_add1 x = ok y ∧
-  ↑y = 2 * ↑x + (1 : Int)
-  := by
-  sorry
-
-/- [tutorial::mul2_add1_add]:
-   Source: 'src/lib.rs', lines 15:0-15:43 -/
-def mul2_add1_add (x : U32) (y : U32) : Result U32 :=
-  do
+/-- [tutorial::mul2_add1_add]:
+    Source: 'src/lib.rs', lines 13:0-15:1 -/
+def mul2_add1_add (x : Std.U32) (y : Std.U32) : Result Std.U32 := do
   let i ← mul2_add1 x
   i + y
 
 /-- Theorem about `mul2_add1_add` -/
 theorem mul2_add1_add_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
-  ∃ z, mul2_add1_add x y = ok z ∧
-  ↑z = 2 * ↑x + (1 : Int) + ↑y := by
+  mul2_add1_add x y ⦃ z => ↑z = 2 * ↑x + (1 : Int) + ↑y ⦄ := by
   sorry
 
-/- [tutorial::CList]
-   Source: 'src/lib.rs', lines 32:0-32:17 -/
-inductive CList (T : Type) :=
+/-- [tutorial::CList]
+    Source: 'src/lib.rs', lines 30:0-33:1 -/
+@[discriminant isize]
+inductive CList (T : Type) where
 | CCons : T → CList T → CList T
 | CNil : CList T
 
@@ -66,79 +58,195 @@ open CList
 
 /- [tutorial::list_nth]:
    Source: 'src/lib.rs', lines 37:0-37:56 -/
-divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
+def list_nth {T : Type} (l : CList T) (i : Std.U32) : Result T := do
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then Result.ok x
-    else do
-         let i1 ← i - 1#u32
-         list_nth T tl i1
-  | CList.CNil => Result.fail .panic
+    then ok x
+    else let i1 ← i - 1#u32
+         list_nth tl i1
+  | CList.CNil => fail panic
+partial_fixpoint
 
 /-- Theorem about `list_nth` -/
 theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
   (h : i.val < l.toList.length) :
-  ∃ x, list_nth T l i = ok x ∧
-  x = l.toList.index i.toNat
+  list_nth l i ⦃ x => x = l.toList.get ⟨i.bv.toNat, by scalar_tac⟩ ⦄
   := by
-  rw [list_nth]
+  rw [list_nth.eq_def]
   split
-  . split
-    . simp_all
-    . simp_all
-      progress as ⟨ i1 ⟩
-      progress as ⟨ x ⟩
-      simp_all
-  . simp_all
-    scalar_tac
+  rename_i l hd tl
+  . -- Case CCons hd tl
+    split
+    . -- i = 0
+      simp_all only [toList, List.length_cons, U32.ofNat_bv, UScalarTy.U32_numBits_eq,
+        BitVec.toNat_ofNat, Nat.reducePow, Nat.zero_mod, Fin.zero_eta, List.get_eq_getElem,
+        Fin.coe_ofNat_eq_mod, List.getElem_cons_zero, WP.spec_ok]
+    . -- i > 0
+      simp_all only [UScalar.neq_to_neq_val, UScalar.ofNatCore_val_eq, toList, List.length_cons, U32.bv_toNat, List.get_eq_getElem]
+      step as ⟨ i1 ⟩
+      -- 2. Use step with an explicit precondition for the recursive call
+      step as ⟨ x ⟩
+      simp_all only [toList, List.length_cons, Order.lt_add_one_iff]
+      grind only
+      -- 3. Simplify list indexing: hd :: tl[i] = tl[i-1]
+      have hi : i.bv.toNat = i1.bv.toNat + 1 := by scalar_tac
+      simp_all only [U32.bv_toNat, Nat.sub_add_cancel]
+      rename_i __2
+      subst __2
+      simp_all only [List.get_eq_getElem]
+      grind only [= List.getElem_cons]
+  . -- Case CNil: i.val < [].length leads to contradiction
+    simp_all only [toList, List.length_nil, U32.bv_toNat, List.get_eq_getElem, WP.spec_fail]
+    contradiction
+
 
-/- [tutorial::i32_id]:
-   Source: 'src/lib.rs', lines 78:0-78:29 -/
-divergent def i32_id (i : I32) : Result I32 :=
+/-- Theorem about `list_nth` -/
+theorem list_nth_spec__manual {T : Type} [Inhabited T] (l : CList T) (i : U32)
+  (h : i.val < l.toList.length) :
+  ∃ x, list_nth l i = ok x ∧
+  x = l.toList.get ⟨i.bv.toNat, by scalar_tac⟩
+  := by
+  rw [list_nth.eq_def]
+  split
+  . -- Case CCons hd tl
+    rename_i hd tl
+    -- Pre-simplify the length hypothesis so scalar_tac can use it
+    have h_len : i.val < 1 + tl.toList.length := by
+      have h_cons : (CList.CCons hd tl).toList.length = 1 + tl.toList.length := by
+        simp_all [toList]; scalar_tac
+      rw [h_cons] at h
+      exact h
+
+    split
+    . -- i = 0
+      simp_all only [↓existsAndEq, toList, List.length_cons, U32.ofNat_bv, UScalarTy.U32_numBits_eq,
+        BitVec.toNat_ofNat, Nat.reducePow, Nat.zero_mod, Fin.zero_eta, List.get_eq_getElem,
+        Fin.coe_ofNat_eq_mod, List.getElem_cons_zero, and_self]
+    . -- i > 0
+      -- 1. Get the sub_spec, then manually 'cases' the subtraction to extract 'ok'
+      have hSub := @U32.sub_spec i 1#u32 (by scalar_tac)
+      cases hEq : i - 1#u32 with
+      | fail e => simp_all only [UScalar.neq_to_neq_val, UScalar.ofNatCore_val_eq, WP.spec_fail] -- Proved impossible by hSub
+      | div => simp_all only [UScalar.neq_to_neq_val, UScalar.ofNatCore_val_eq, WP.spec_div]    -- Proved impossible by hSub
+      | ok i1 =>
+        -- Now we are safely in the 'ok' case!
+        simp_all only [UScalar.neq_to_neq_val, UScalar.ofNatCore_val_eq, WP.spec_ok, ↓existsAndEq,
+          bind_tc_ok, toList, List.length_cons, U32.bv_toNat, List.get_eq_getElem, and_true]
+
+        -- 2. Manually apply the recursive call
+        obtain ⟨left, right⟩ := hSub
+
+        have ⟨x, h_rec, h_val⟩ := list_nth_spec__manual tl i1 (by scalar_tac)
+        rw [h_rec]
+
+        -- 3. Arithmetic to match the list index
+        have : i.bv.toNat = i1.bv.toNat + 1 := by scalar_tac
+        simp_all only [U32.bv_toNat, List.get_eq_getElem, UScalarTy.U32_numBits_eq,
+          Bvify.U32.UScalar_bv, Nat.sub_add_cancel, ok.injEq]
+
+        grind only [= List.getElem_cons]
+  . -- Case CNil: i.val < [].length leads to contradiction
+    simp_all only [↓existsAndEq, toList, List.length_nil, U32.bv_toNat, List.get_eq_getElem, reduceCtorEq, and_true]
+    contradiction
+
+
+/-- [tutorial::i32_id]:
+    Source: 'src/lib.rs', lines 76:0-83:1 -/
+def i32_id (i : Std.I32) : Result Std.I32 := do
   if i = 0#i32
-  then Result.ok 0#i32
-  else do
-       let i1 ← i - 1#i32
+  then ok 0#i32
+  else let i1 ← i - 1#i32
        let i2 ← i32_id i1
        i2 + 1#i32
+partial_fixpoint
 
 /-- Theorem about `i32_id` -/
 theorem i32_id_spec (n : I32) (h : 0 ≤ n.val) :
-  i32_id n = ok n := by
-  rw [i32_id]
+  i32_id n ⦃ res => res = n ⦄ := by
+  -- 1. Unfold the partial_fixpoint definition
+  rw [i32_id.eq_def]
   split
-  . simp [*]
-  . progress as ⟨ n1 ⟩
-    progress
-    progress as ⟨ n2 ⟩
+  . -- Case: n = 0
+    simp_all only [IScalar.ofInt_val_eq, Std.le_refl, WP.spec_ok]
+  . -- Case: n != 0
+    -- 2. Step through the subtraction (n - 1)
+    step as ⟨ n1 ⟩
+
+    -- 3. Step through the recursive call (i32_id n1)
+    -- Lean automatically uses the termination_by block to prove n1 < n is safe!
+    step as ⟨ n2 ⟩
+
+    -- 4. Step through the addition (n2 + 1)
+    step as ⟨ n3 ⟩
+
+    -- 5. Finish the arithmetic (proving n3 = n)
+    simp_all only [IScalar.neq_to_neq_val, IScalar.ofInt_val_eq, sub_add_cancel]
     scalar_tac
 termination_by n.toNat
-decreasing_by
-  -- We always need to start termination proofs with this tactic (it massages the goal)
-  simp_wf
-  -- It is an arithmetic goal:
-  scalar_tac
-  -- Remark: as the pattern above is quite common (`simp_wf; scalar_tac`),
-  -- we introduced the tactic `scalar_decr_tac` (it does the same)
-
-/- [tutorial::even]:
-   Source: 'src/lib.rs', lines 87:0-87:28 -/
-mutual divergent def even (i : U32) : Result Bool :=
+decreasing_by scalar_decr_tac
+
+/-- Theorem about `i32_id` -/
+theorem i32_id_spec_manual (n : I32) (h : 0 ≤ n.val) :
+  i32_id n = ok n := by
+  rw [i32_id.eq_def]
+  split
+  . -- Case n = 0
+    simp [*]
+  . -- Case n != 0
+
+    -- 1. Subtraction (n - 1)
+    have hSub := @I32.sub_spec n 1#i32 (by scalar_tac)
+    cases hEq1 : n - 1#i32 with
+    | fail e => simp_all only [IScalar.neq_to_neq_val, IScalar.ofInt_val_eq, tsub_le_iff_right, WP.spec_fail, imp_false, not_le, bind_tc_fail, reduceCtorEq]; grind only [usr ScalarTac.IScalar.bounds, = I32.max_eq, = IScalar.max_IScalarTy_I32_eq]
+    | div => rw [hEq1] at hSub; simp_all only [IScalar.neq_to_neq_val, IScalar.ofInt_val_eq, tsub_le_iff_right, WP.spec_div, imp_false, not_le, bind_tc_div, reduceCtorEq]; grind only [usr ScalarTac.IScalar.bounds, = I32.max_eq, = IScalar.max_IScalarTy_I32_eq]
+    | ok n1 =>
+      rw [hEq1] at hSub
+      -- Extract the arithmetic property from hSub: ↑n1 = ↑n - 1
+      have ⟨_y, _h_ok, h_arith1⟩ := (Aeneas.Std.WP.spec_equiv_exists _ _).mp (hSub (by scalar_tac))
+      simp only [bind_tc_ok]
+
+      -- 2. Recursive call
+      have hRec := i32_id_spec n1 (by grind only [usr ScalarTac.IScalar.bounds,
+        !IScalar.ofInt_val_eq, = I32.max_eq, = WP.spec_ok, = IScalar.max_IScalarTy_I32_eq, #ba93])
+      simp_all only [IScalar.neq_to_neq_val, IScalar.ofInt_val_eq, tsub_le_iff_right, WP.spec_ok]
+
+      -- 3. Addition
+      have hAdd := I32.add_spec (x := n1) (y := 1#i32) (by scalar_tac)
+      cases hEq2 : n1 + 1#i32 with
+      | fail e => rw [hEq2] at hAdd; grind only [usr ScalarTac.IScalar.bounds, = I32.max_eq,
+        !IScalar.ofInt_val_eq, = WP.spec_fail, = IScalar.max_IScalarTy_I32_eq]
+      | div => rw [hEq2] at hAdd; grind only [usr ScalarTac.IScalar.bounds, = I32.max_eq,
+        !IScalar.ofInt_val_eq, = WP.spec_div, = IScalar.max_IScalarTy_I32_eq]
+      | ok n2 =>
+        rw [hEq2] at hAdd
+        simp_all only [IScalar.ofInt_val_eq, WP.spec_ok, implies_true, ok.injEq, sub_add_cancel]
+        subst _h_ok
+        have ⟨i2, hi2, hi2val⟩ := (Aeneas.Std.WP.spec_equiv_exists _ _).mp hRec
+        simp only [hi2, hi2val]
+        subst hi2val
+        simp_all only [WP.spec_ok, bind_tc_ok, ok.injEq]
+        scalar_tac
+
+mutual
+
+/-- [tutorial::even]:
+    Source: 'src/lib.rs', lines 85:0-92:1 -/
+def even (i : Std.U32) : Result Bool := do
   if i = 0#u32
-  then Result.ok true
-  else do
-       let i1 ← i - 1#u32
+  then ok true
+  else let i1 ← i - 1#u32
        odd i1
+partial_fixpoint
 
-/- [tutorial::odd]:
-   Source: 'src/lib.rs', lines 96:0-96:27 -/
-divergent def odd (i : U32) : Result Bool :=
+/-- [tutorial::odd]:
+    Source: 'src/lib.rs', lines 94:0-101:1 -/
+def odd (i : Std.U32) : Result Bool := do
   if i = 0#u32
-  then Result.ok false
-  else do
-       let i1 ← i - 1#u32
+  then ok false
+  else let i1 ← i - 1#u32
        even i1
+partial_fixpoint
 
 end
 
@@ -146,55 +254,59 @@ mutual
 
 /-- The proof about `even` -/
 theorem even_spec (n : U32) :
-  ∃ b, even n = ok b ∧ (b ↔ Even n.val) := by
-  rw [even]
+  even n ⦃ b => b ↔ Even n.val ⦄ := by
+  rw [even.eq_def]
   split
   . simp [*]
-  . progress as ⟨ n' ⟩
-    progress as ⟨ b ⟩
+  . step with U32.sub_spec as ⟨ n' ⟩
+    step as ⟨ b ⟩
     simp [*]
-    simp [Int.odd_sub]
-termination_by n.toNat
+    apply iff_of_eq
+    simp_all only [UScalar.neq_to_neq_val, UScalar.ofNatCore_val_eq, eq_iff_iff]
+    grind only [= Nat.odd_iff, = Nat.even_iff, #c46a]
+termination_by n.val
 decreasing_by scalar_decr_tac
 
 /-- The proof about `odd` -/
 theorem odd_spec (n : U32) :
-  ∃ b, odd n = ok b ∧ (b ↔ Odd n.val) := by
-  rw [odd]
+  odd n ⦃ b => b ↔ Odd n.val ⦄ := by
+  rw [odd.eq_def]
   split
   . simp [*]
-  . progress as ⟨ n' ⟩
-    progress as ⟨ b ⟩
+  . step with U32.sub_spec as ⟨ n' ⟩
+    step as ⟨ b ⟩
     simp [*]
-    simp [Int.even_sub]
-termination_by n.toNat
+    apply iff_of_eq
+    simp_all only [UScalar.neq_to_neq_val, UScalar.ofNatCore_val_eq, eq_iff_iff]
+    grind only [= Nat.even_iff, = Nat.not_odd_iff_even, = Nat.odd_iff, #e573]
+termination_by n.val
 decreasing_by scalar_decr_tac
 
 end
 
-/- [tutorial::list_nth_mut1]: loop 0:
-   Source: 'src/lib.rs', lines 124:4-132:1 -/
-divergent def list_nth_mut1_loop
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
+/-- [tutorial::list_nth_mut1]: loop 0:
+    Source: 'src/lib.rs', lines 124:4-132:1 -/
+@[rust_loop]
+def list_nth_mut1_loop
+  {T : Type} (l : CList T) (i : Std.U32) : Result (T × (T → CList T)) := do
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then let back := fun ret => CList.CCons ret tl
-         Result.ok (x, back)
+    then ok (x, fun t => CList.CCons t tl)
     else
-      do
       let i1 ← i - 1#u32
       let (t, back) ← list_nth_mut1_loop tl i1
-      let back1 := fun ret => let tl1 := back ret
-                              CList.CCons x tl1
-      Result.ok (t, back1)
-  | CList.CNil => Result.fail .panic
-
-/- [tutorial::list_nth_mut1]:
-   Source: 'src/lib.rs', lines 123:0-132:1 -/
+      let back1 := fun t1 => let c := back t1
+                             CList.CCons x c
+      ok (t, back1)
+  | CList.CNil => fail panic
+partial_fixpoint
+
+/-- [tutorial::list_nth_mut1]:
+    Source: 'src/lib.rs', lines 123:0-132:1 -/
 @[reducible]
 def list_nth_mut1
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
+  {T : Type} (l : CList T) (i : Std.U32) : Result (T × (T → CList T)) := do
   list_nth_mut1_loop l i
 
 /-
@@ -223,10 +335,11 @@ def list_nth_mut1
 /- `simp` simplifies the goal by applying rewriting lemmas and simplifying definitions
    marked as `@[simp]`. For instance, the lemma `List.length_cons` which states that
    `(hd :: tl).length = tl.length + 1` has been marked as `simp`: -/
-#check List.length_cons
+/-- info: List.length_cons.{u} {α : Type u} {a : α} {«as» : List α} : (a :: «as»).length = «as».length + 1 -/
+#guard_msgs in #check List.length_cons
 example α (hd : α) (tl : List α) : (hd :: tl).length = tl.length + 1 := by
   -- This proves the goal automatically, by using `List.length_cons` above
-  simp
+  simp only [List.length_cons]
 
 /- You can see which lemmas are applied by `simp` by using `simp?`.
    This is often useful to build the intuition of what `simp` does, especially when
@@ -242,10 +355,10 @@ example α (hd : α) (tl : List α) : (hd :: tl).length = tl.length + 1 := by
    tactic, but you will not need to understand those for this tutorial.
 
    Just be aware that `rw` doesn't apply simplification lemmas recursively, while
-   `simp` repeatedly simplifies the goal until it can't make progress anymore.
+   `simp` repeatedly simplifies the goal until it can't make step anymore.
  -/
 example α (hd : α) (tl : List α) : (hd :: tl).length = tl.length + 1 := by
-  simp? -- This prints: `simp only [List.length_cons]`
+  simp? -- This prints: `simp only [List.length_cons, Nat.add_left_cancel_iff]`
 
 /- Your turn!
 
@@ -363,26 +476,28 @@ set_option pp.coercions true
 
    You can use the following two lemmas.
  -/
-#check List.index_zero_cons
-#check List.index_nzero_cons
+#check List.getElem_cons_zero
+#check List.getElem_cons_succ
 
 /- Example 1: indexing the first element of the list -/
 example [Inhabited α] (i : U32) (hd : α) (tl : CList α)
   (hEq : i = 0#u32) :
-  (hd :: tl.toList).index i.toNat = hd := by
-  have hi : i.toNat = 0 := by scalar_tac
+  (hd :: tl.toList)[i.val]'(by scalar_tac) = hd := by
+  have hi : i.val = 0 := by scalar_tac
   simp only [hi]
-  --
-  have hIndex := List.index_zero_cons hd tl.toList
-  simp only [hIndex]
+  simp only [getElem_cons_zero]
 
 /- Example 2: indexing in the tail -/
 example [Inhabited α] (i : U32) (hd : α) (tl : CList α)
-  (hEq : i ≠ 0#u32) :
-  (hd :: tl.toList).index i.toNat = tl.toList.index (i.toNat - 1) := by
+  (hEq : i ≠ 0#u32)  (hI : ↑i < (hd :: tl.toList).length) :
+  (hd :: tl.toList)[i.val]'(by simp_all only [ne_eq, UScalar.neq_to_neq_val, UScalar.ofNatCore_val_eq, length_cons,
+    Order.lt_add_one_iff]) = tl.toList[i.val - 1]'(by grind only [= UScalar.ofNatCore_val_eq,
+      = length_cons, #6b46]) := by
   -- Note that `scalar_tac` is aware of `Arith.Nat.not_eq`
-  have hIndex := List.index_nzero_cons hd tl.toList i.toNat (by scalar_tac)
-  simp only [hIndex]
+  -- have hIndex := List.getElem_cons_succ hd tl.toList i.val (by scalar_tac)
+  -- simp only [hIndex]
+  grind only [= UScalar.ofNatCore_val_eq, = getElem_cons]
+
 
 /- Note that `List.index_zero_cons` and `List.index_nzero_cons` have been
    marked as `@[simp]` and are thus automatically applied. Also note
@@ -393,15 +508,15 @@ example [Inhabited α] (i : U32) (hd : α) (tl : CList α)
    you expect. -/
 example [Inhabited α] (i : U32) (hd : α) (tl : CList α)
   (hEq : i = 0#u32) :
-  (hd :: tl.toList).index i.toNat = hd := by
+  (hd :: tl.toList)[i.val]'(by scalar_tac) = hd := by
   simp [hEq]
 
 /- Note that `simp_all` manages to automatically apply `List.index_nzero_cons` below,
    by using the fact that `i ≠ 0#u32`. -/
 example [Inhabited α] (i : U32) (hd : α) (tl : CList α)
-  (hEq : i ≠ 0#u32) :
-  (hd :: tl.toList).index i.toNat = tl.toList.index (i.toNat - 1) := by
-  simp_all
+  (hEq : i ≠ 0#u32) (hI : ↑i < (hd :: tl.toList).length) :
+  (hd :: tl.toList)[i.val]'(by scalar_tac) = tl.toList[i.val - 1]'(by scalar_tac) := by
+  grind only [= UScalar.ofNatCore_val_eq, = getElem_cons]
 
 /- Below, you will need to reason about `List.update`.
    You can use the following lemmas.
@@ -409,20 +524,20 @@ example [Inhabited α] (i : U32) (hd : α) (tl : CList α)
    Those lemmas have been marked as `@[simp]`, meaning that if `simp` is properly used,
    it will manage to apply them automatically.
  -/
-#check List.update_zero_cons
-#check List.update_nzero_cons
+#check List.set_cons_zero
+#check List.set_cons_succ
 
 /- # Some proofs of programs -/
 
 /-- Theorem about `list_nth_mut1`.
 
     **Hints**:
-    - you can use `progress` to automatically apply a lemma, then refine it into
-      `progress as ⟨ ... ⟩` to name the variables and the post-conditions(s) it introduces.
+    - you can use `step` to automatically apply a lemma, then refine it into
+      `step as ⟨ ... ⟩` to name the variables and the post-conditions(s) it introduces.
     - if there is a disjunction or branching (like an `if then else`) in the goal, use `split`
     - if the goal is a conjunction, you can use `split_conjs` to introduce one subgoal
       per disjunct
-    - you should use `progress` for as long as you see a monadic `do` block, unless you
+    - you should use `step` for as long as you see a monadic `do` block, unless you
       see a branching, in which case you should use `split`.
 
     **Remark**: we wrote two versions of the solution in `Solutions.lean`:
@@ -435,77 +550,76 @@ example [Inhabited α] (i : U32) (hd : α) (tl : CList α)
 theorem list_nth_mut1_spec {T: Type} [Inhabited T] (l : CList T) (i : U32)
   (h : i.val < l.toList.length) :
   ∃ x back, list_nth_mut1 l i = ok (x, back) ∧
-  x = l.toList.index i.toNat ∧
+  x = l.toList[i.val]'(by scalar_tac) ∧
   -- Specification of the backward function
-  ∀ x', (back x').toList = l.toList.update i.toNat x' := by
-  rw [list_nth_mut1, list_nth_mut1_loop]
+  ∀ x', (back x').toList = l.toList.set i.val x' := by
+  rw [list_nth_mut1, list_nth_mut1_loop.eq_def]
   sorry
 
-/- [tutorial::list_tail]: loop 0:
-   Source: 'src/lib.rs', lines 135:4-137:5 -/
-divergent def list_tail_loop
-  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) :=
+/-- [tutorial::list_tail]: loop 0:
+    Source: 'src/lib.rs', lines 135:4-137:5 -/
+@[rust_loop]
+def list_tail_loop
+  {T : Type} (l : CList T) : Result (CList T → CList T) := do
   match l with
   | CList.CCons t tl =>
-    do
-    let (c, back) ← list_tail_loop tl
-    let back1 := fun ret => let tl1 := back ret
-                            CList.CCons t tl1
-    Result.ok (c, back1)
-  | CList.CNil => let back := fun ret => ret
-                  Result.ok (CList.CNil, back)
-
-/- [tutorial::list_tail]:
-   Source: 'src/lib.rs', lines 134:0-139:1 -/
-@[reducible]
+    let back ← list_tail_loop tl
+    ok (fun c => let c1 := back c
+                 CList.CCons t c1)
+  | CList.CNil => ok (fun c => c)
+partial_fixpoint
+
+/-- [tutorial::list_tail]:
+    Source: 'src/lib.rs', lines 134:0-139:1 -/
 def list_tail
-  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) :=
-  list_tail_loop l
+  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) := do
+  let back ← list_tail_loop l
+  ok (CList.CNil, back)
 
-
-/- [tutorial::append_in_place]:
-   Source: 'src/lib.rs', lines 141:0-144:1 -/
+/-- [tutorial::append_in_place]:
+    Source: 'src/lib.rs', lines 141:0-144:1 -/
 def append_in_place
-  {T : Type} (l0 : CList T) (l1 : CList T) : Result (CList T) :=
-  do
+  {T : Type} (l0 : CList T) (l1 : CList T) : Result (CList T) := do
   let (_, list_tail_back) ← list_tail l0
-  Result.ok (list_tail_back l1)
+  ok (list_tail_back l1)
 
 /-- Theorem about `list_tail`: exercise -/
-@[pspec]
 theorem list_tail_spec {T : Type} (l : CList T) :
   ∃ back, list_tail l = ok (CList.CNil, back) ∧
   ∀ tl', (back tl').toList = l.toList ++ tl'.toList := by
-  rw [list_tail, list_tail_loop]
+  rw [list_tail, list_tail_loop.eq_def]
   sorry
 
 /-- Theorem about `append_in_place`: exercise -/
-@[pspec]
+
 theorem append_in_place_spec {T : Type} (l0 l1 : CList T) :
   ∃ l2, append_in_place l0 l1 = ok l2 ∧
   l2.toList = l0.toList ++ l1.toList := by
   rw [append_in_place]
   sorry
 
-/- [tutorial::reverse]: loop 0:
-   Source: 'src/lib.rs', lines 148:4-152:5 -/
-divergent def reverse_loop
-  {T : Type} (l : CList T) (out : CList T) : Result (CList T) :=
+/-- [tutorial::reverse]: loop 0:
+    Source: 'src/lib.rs', lines 148:4-152:5 -/
+@[rust_loop]
+def reverse_loop
+  {T : Type} (l : CList T) (out : CList T) : Result (CList T) := do
   match l with
   | CList.CCons hd tl => reverse_loop tl (CList.CCons hd out)
-  | CList.CNil => Result.ok out
+  | CList.CNil => ok out
+partial_fixpoint
+
 
-@[pspec]
 theorem reverse_loop_spec {T : Type} (l : CList T) (out : CList T) :
   ∃ l', reverse_loop l out = ok l' ∧
   True -- Leaving the post-condition as an exercise
   := by
-  rw [reverse_loop]
+  rw [reverse_loop.eq_def]
   sorry
 
-/- [tutorial::reverse]:
-   Source: 'src/lib.rs', lines 146:0-154:1 -/
-def reverse {T : Type} (l : CList T) : Result (CList T) :=
+/-- [tutorial::reverse]:
+    Source: 'src/lib.rs', lines 146:0-154:1 -/
+@[reducible]
+def reverse {T : Type} (l : CList T) : Result (CList T) := do
   reverse_loop l CList.CNil
 
 theorem reverse_spec {T : Type} (l : CList T) :
@@ -528,21 +642,35 @@ theorem reverse_spec {T : Type} (l : CList T) :
  -/
 attribute [-simp] Int.reducePow Nat.reducePow
 
-/- [tutorial::zero]: loop 0:
-   Source: 'src/lib.rs', lines 164:4-167:5 -/
-divergent def zero_loop
-  (x : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
+/-- [tutorial::zero]: loop body 0:
+    Source: 'src/lib.rs', lines 165:4-168:5 -/
+@[rust_loop_body]
+def zero_loop.body
+  (x : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.Usize) (alloc.vec.Vec
+    Std.U32))
+  := do
   let i1 := alloc.vec.Vec.len x
   if i < i1
   then
-    do
     let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i2 ← i + 1#usize
     let x1 := index_mut_back 0#u32
-    zero_loop x1 i2
-  else Result.ok x
+    ok (cont (x1, i2))
+  else ok (done x)
+
+/-- [tutorial::zero]: loop 0:
+    Source: 'src/lib.rs', lines 165:4-168:5 -/
+@[rust_loop]
+def zero_loop
+  (x : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
+  loop
+    (fun (x1, i1) => zero_loop.body x1 i1)
+    (x, i)
 
 
 /-- Auxiliary definitions to interpret a vector of u32 as a mathematical integer -/
@@ -567,21 +695,22 @@ def toInt (x : alloc.vec.Vec U32) : ℤ := toInt_aux x.val
       Ex.: `dcases x = y` will introduce two goals, one with the assumption `x = y` and the
       other with the assumption `x ≠ y`. You can name this assumption by writing: `dcases h : x = y`
  -/
-@[pspec]
+
 theorem zero_loop_spec
   (x : alloc.vec.Vec U32) (i : Usize) (h : i.val ≤ x.length) :
   ∃ x',
     zero_loop x i = ok x' ∧
     x'.length = x.length ∧
-    (∀ j, j < i.toNat → x'.val.index j = x.val.index j) ∧
-    (∀ j, i.toNat ≤ j → j < x.length → x'.val.index j = 0#u32) := by
-  rw [zero_loop]
+    (∀ j, j < i.val → x'.val[j]'(by sorry) = x.val[j]'(by sorry)) ∧
+    (∀ j, i.val ≤ j → j < x.length → x'.val[j]'(by sorry) = 0#u32) := by
+  rw [zero_loop.eq_def]
   simp
   sorry
 
-/- [tutorial::zero]:
-   Source: 'src/lib.rs', lines 162:0-168:1 -/
-def zero (x : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
+/-- [tutorial::zero]:
+    Source: 'src/lib.rs', lines 162:0-169:1 -/
+@[reducible]
+def zero (x : alloc.vec.Vec Std.U32) : Result (alloc.vec.Vec Std.U32) := do
   zero_loop x 0#usize
 
 /-- You will need this lemma for the proof of `zero_spec`
@@ -589,7 +718,7 @@ def zero (x : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
     Advice: do the proof of `zero_spec` first, then come back to prove this lemma.
 -/
 theorem all_nil_impl_toInt_eq_zero
-  (l : List U32) (h : ∀ (j : ℕ), j < l.length → l.index j = 0#u32) :
+  (l : List U32) (h : ∀ (j : ℕ), j < l.length → l[j]'(by sorry) = 0#u32) :
   toInt_aux l = 0 := by
   /- There are two ways of proving this theorem.
 
@@ -622,26 +751,38 @@ theorem zero_spec (x : alloc.vec.Vec U32) :
   rw [zero]
   sorry
 
-/- [tutorial::add_no_overflow]: loop 0:
-   Source: 'src/lib.rs', lines 177:4-180:5 -/
-divergent def add_no_overflow_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize) :
-  Result (alloc.vec.Vec U32)
-  :=
+/-- [tutorial::add_no_overflow]: loop body 0:
+    Source: 'src/lib.rs', lines 182:4-185:5 -/
+@[rust_loop_body]
+def add_no_overflow_loop.body
+  (y : alloc.vec.Vec Std.U32) (x : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.Usize) (alloc.vec.Vec
+    Std.U32))
+  := do
   let i1 := alloc.vec.Vec.len x
   if i < i1
   then
-    do
     let i2 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) y i
     let (i3, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i4 ← i3 + i2
     let i5 ← i + 1#usize
     let x1 := index_mut_back i4
-    add_no_overflow_loop x1 y i5
-  else Result.ok x
+    ok (cont (x1, i5))
+  else ok (done x)
+
+/-- [tutorial::add_no_overflow]: loop 0:
+    Source: 'src/lib.rs', lines 182:4-185:5 -/
+@[rust_loop]
+def add_no_overflow_loop
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
+  loop
+    (fun (x1, i1) => add_no_overflow_loop.body y x1 i1)
+    (x, i)
 
 /-- You will need this lemma for the proof of `add_no_overflow_loop_spec`.
 
@@ -655,7 +796,7 @@ divergent def add_no_overflow_loop
  -/
 @[simp]
 theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) :
-  toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by
+  toInt_aux (l.drop i) = l[i]'(by scalar_tac) + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by
   sorry
 
 /-- You will need this lemma for the proof of `add_no_overflow_loop_spec`.
@@ -673,7 +814,7 @@ theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) :
  -/
 @[simp]
 theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length) :
-  toInt_aux (l.update i x) = toInt_aux l + 2 ^ (32 * i) * (x - l.index i) := by
+  toInt_aux (l.set i x) = toInt_aux l + 2 ^ (32 * i) * (x - l[i]'(by scalar_tac)) := by
   sorry
 
 /-- The proof about `add_no_overflow_loop`.
@@ -681,70 +822,83 @@ theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length)
     Hint: you will need to reason about non-linear arithmetic with `scalar_nf` and
     `scalar_eq_nf` (see above).
  -/
-@[pspec]
+
 theorem add_no_overflow_loop_spec
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize)
   (hLength : x.length = y.length)
   -- No overflow occurs when we add the individual thunks
-  (hNoOverflow : ∀ (j : Nat), i.toNat ≤ j → j < x.length → (x.val.index j).val + (y.val.index j).val ≤ U32.max)
+  (hNoOverflow : ∀ (j : Nat), i.val ≤ j → j < x.length → (x.val[j]'(by sorry)).val + (y.val[j]'(by sorry)).val ≤ U32.max)
   (hi : i.val ≤ x.length) :
   ∃ x', add_no_overflow_loop x y i = ok x' ∧
   x'.length = x.length ∧
-  toInt x' = toInt x + 2 ^ (32 * i.toNat) * toInt_aux (y.val.drop i.toNat) := by
-  rw [add_no_overflow_loop]
+  toInt x' = toInt x + 2 ^ (32 * i.val) * toInt_aux (y.val.drop i.val) := by
+  rw [add_no_overflow_loop.eq_def]
   simp
   sorry
 
-/- [tutorial::add_no_overflow]:
-   Source: 'src/lib.rs', lines 175:0-181:1 -/
+/-- [tutorial::add_no_overflow]:
+    Source: 'src/lib.rs', lines 176:0-186:1 -/
+@[reducible]
 def add_no_overflow
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (alloc.vec.Vec U32)
-  :=
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
   add_no_overflow_loop x y 0#usize
 
 /-- The proof about `add_no_overflow` -/
 theorem add_no_overflow_spec (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32)
   (hLength : x.length = y.length)
-  (hNoOverflow : ∀ (j : Nat), j < x.length → (x.val.index j).val + (y.val.index j).val ≤ U32.max) :
+  (hNoOverflow : ∀ (j : Nat), j < x.length → (x.val[j]'(by sorry)).val + (y.val[j]'(by sorry)).val ≤ U32.max) :
   ∃ x', add_no_overflow x y = ok x' ∧
   x'.length = y.length ∧
   toInt x' = toInt x + toInt y := by
   rw [add_no_overflow]
   sorry
 
-/- [tutorial::add_with_carry]: loop 0:
-   Source: 'src/lib.rs', lines 190:4-197:5 -/
-divergent def add_with_carry_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (c0 : U8) (i : Usize) :
-  Result (U8 × (alloc.vec.Vec U32))
-  :=
+/-- [tutorial::add_with_carry]: loop body 0:
+    Source: 'src/lib.rs', lines 203:4-210:5 -/
+@[rust_loop_body]
+def add_with_carry_loop.body
+  (y : alloc.vec.Vec Std.U32) (x : alloc.vec.Vec Std.U32) (c0 : Std.U8)
+  (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.U8 × Std.Usize) (Std.U8
+    × (alloc.vec.Vec Std.U32)))
+  := do
   let i1 := alloc.vec.Vec.len x
   if i < i1
   then
-    do
     let i2 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) x i
-    let i3 ← Scalar.cast .U32 c0
-    let p ← core.num.U32.overflowing_add i2 i3
-    let (sum, c1) := p
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) x i
+    let i3 ← lift (UScalar.cast .U32 c0)
+    let (sum, c1) ← lift (core.num.U32.overflowing_add i2 i3)
     let i4 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
-    let p1 ← core.num.U32.overflowing_add sum i4
-    let (sum1, c2) := p1
-    let i5 ← Scalar.cast_bool .U8 c1
-    let i6 ← Scalar.cast_bool .U8 c2
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) y i
+    let (sum1, c2) ← lift (core.num.U32.overflowing_add sum i4)
+    let i5 ← lift (UScalar.cast_fromBool .U8 c1)
+    let i6 ← lift (UScalar.cast_fromBool .U8 c2)
     let c01 ← i5 + i6
     let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i7 ← i + 1#usize
     let x1 := index_mut_back sum1
-    add_with_carry_loop x1 y c01 i7
-  else Result.ok (c0, x)
+    ok (cont (x1, c01, i7))
+  else ok (done (c0, x))
+
+/-- [tutorial::add_with_carry]: loop 0:
+    Source: 'src/lib.rs', lines 203:4-210:5 -/
+@[rust_loop]
+def add_with_carry_loop
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) (c0 : Std.U8)
+  (i : Std.Usize) :
+  Result (Std.U8 × (alloc.vec.Vec Std.U32))
+  := do
+  loop
+    (fun (x1, c01, i1) => add_with_carry_loop.body y x1 c01 i1)
+    (x, c0, i)
 
 /-- The proof about `add_with_carry_loop` -/
-@[pspec]
+
 theorem add_with_carry_loop_spec
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (c0 : U8) (i : Usize)
   (hLength : x.length = y.length)
@@ -754,21 +908,22 @@ theorem add_with_carry_loop_spec
   x'.length = x.length ∧
   c1.val ≤ 1 ∧
   toInt x' + c1.val * 2 ^ (32 * x'.length) =
-    toInt x + 2 ^ (32 * i.toNat) * toInt_aux (y.val.drop i.toNat) + c0.val * 2 ^ (32 * i.toNat) := by
-  rw [add_with_carry_loop]
+    toInt x + 2 ^ (32 * i.val) * toInt_aux (y.val.drop i.val) + c0.val * 2 ^ (32 * i.val) := by
+  rw [add_with_carry_loop.eq_def]
   simp
   sorry
 
-/- [tutorial::add_with_carry]:
-   Source: 'src/lib.rs', lines 186:0-199:1 -/
+/-- [tutorial::add_with_carry]:
+    Source: 'src/lib.rs', lines 191:0-212:1 -/
+@[reducible]
 def add_with_carry
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (U8 × (alloc.vec.Vec U32))
-  :=
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) :
+  Result (Std.U8 × (alloc.vec.Vec Std.U32))
+  := do
   add_with_carry_loop x y 0#u8 0#usize
 
 /-- The proof about `add_with_carry` -/
-@[pspec]
+
 theorem add_with_carry_spec
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32)
   (hLength : x.length = y.length) :
@@ -780,68 +935,78 @@ theorem add_with_carry_spec
   sorry
 
 /- Bonus exercises -/
-/-- We leave it to you to state the theorems for the functions below -/
+/- We leave it to you to state the theorems for the functions below -/
 
-/- [tutorial::max]:
-   Source: 'src/lib.rs', lines 26:0-26:37 -/
-def max (x : Usize) (y : Usize) : Result Usize :=
+/-- [tutorial::max]:
+    Source: 'src/lib.rs', lines 214:0-216:1 -/
+def max (x : Std.Usize) (y : Std.Usize) : Result Std.Usize := do
   if x > y
-  then Result.ok x
-  else Result.ok y
+  then ok x
+  else ok y
 
-/- [tutorial::get_or_zero]:
-   Source: 'src/lib.rs', lines 205:0-207:1 -/
-def get_or_zero (y : alloc.vec.Vec U32) (i : Usize) : Result U32 :=
+/-- [tutorial::get_or_zero]:
+    Source: 'src/lib.rs', lines 218:0-220:1 -/
+def get_or_zero
+  (y : alloc.vec.Vec Std.U32) (i : Std.Usize) : Result Std.U32 := do
   let i1 := alloc.vec.Vec.len y
   if i < i1
-  then alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
-  else Result.ok 0#u32
-
-/- [tutorial::add]: loop 0:
-   Source: 'src/lib.rs', lines 221:4-229:5 -/
-divergent def add_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (max1 : Usize) (c0 : U8)
-  (i : Usize) :
-  Result (alloc.vec.Vec U32)
-  :=
+  then alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) y i
+  else ok 0#u32
+
+/-- [tutorial::add]: loop body 0:
+    Source: 'src/lib.rs', lines 235:4-244:5 -/
+@[rust_loop_body]
+def add_loop.body
+  (y : alloc.vec.Vec Std.U32) (max1 : Std.Usize) (x : alloc.vec.Vec Std.U32)
+  (c0 : Std.U8) (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.U8 × Std.Usize)
+    ((alloc.vec.Vec Std.U32) × Std.U8))
+  := do
   if i < max1
   then
-    do
     let yi ← get_or_zero y i
     let i1 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) x i
-    let i2 ← Scalar.cast .U32 c0
-    let p ← core.num.U32.overflowing_add i1 i2
-    let (sum, c1) := p
-    let p1 ← core.num.U32.overflowing_add sum yi
-    let (sum1, c2) := p1
-    let i3 ← Scalar.cast_bool .U8 c1
-    let i4 ← Scalar.cast_bool .U8 c2
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) x i
+    let i2 ← lift (UScalar.cast .U32 c0)
+    let (sum, c1) ← lift (core.num.U32.overflowing_add i1 i2)
+    let (sum1, c2) ← lift (core.num.U32.overflowing_add sum yi)
+    let i3 ← lift (UScalar.cast_fromBool .U8 c1)
+    let i4 ← lift (UScalar.cast_fromBool .U8 c2)
     let c01 ← i3 + i4
     let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i5 ← i + 1#usize
     let x1 := index_mut_back sum1
-    add_loop x1 y max1 c01 i5
-  else
-    if c0 != 0#u8
-    then do
-         let i1 ← Scalar.cast .U32 c0
-         alloc.vec.Vec.push x i1
-    else Result.ok x
-
-/- [tutorial::add]:
-   Source: 'src/lib.rs', lines 214:0-235:1 -/
+    ok (cont (x1, c01, i5))
+  else ok (done (x, c0))
+
+/-- [tutorial::add]: loop 0:
+    Source: 'src/lib.rs', lines 235:4-244:5 -/
+@[rust_loop]
+def add_loop
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) (max1 : Std.Usize)
+  (c0 : Std.U8) (i : Std.Usize) :
+  Result ((alloc.vec.Vec Std.U32) × Std.U8)
+  := do
+  loop
+    (fun (x1, c01, i1) => add_loop.body y max1 x1 c01 i1)
+    (x, c0, i)
+
+/-- [tutorial::add]:
+    Source: 'src/lib.rs', lines 227:0-250:1 -/
 def add
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (alloc.vec.Vec U32)
-  :=
-  do
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
   let i := alloc.vec.Vec.len x
   let i1 := alloc.vec.Vec.len y
   let max1 ← max i i1
   let x1 ← alloc.vec.Vec.resize core.clone.CloneU32 x max1 0#u32
-  add_loop x1 y max1 0#u8 0#usize
+  let (x2, c0) ← add_loop x1 y max1 0#u8 0#usize
+  if c0 != 0#u8
+  then let i2 ← lift (UScalar.cast .U32 c0)
+       alloc.vec.Vec.push x2 i2
+  else ok x2
 
 end Tutorial.Solutions
diff --git a/Tutorial/Solutions.lean b/Tutorial/Solutions.lean
index 1503e4e..d6c35f2 100644
--- a/Tutorial/Solutions.lean
+++ b/Tutorial/Solutions.lean
@@ -1,6 +1,6 @@
-import Base
+import Aeneas
 import Tutorial.Tutorial
-open Primitives Result
+open Aeneas Aeneas.Std Result ControlFlow Error
 
 set_option maxHeartbeats 1000000
 
@@ -8,10 +8,11 @@ namespace tutorial
 
 /- # Demo -/
 
-/-- Theorem about `mul2_add1`: without the `progress` tactic -/
+/-- Theorem about `mul2_add1`: without the `step` tactic -/
 theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
-  : ∃ y, mul2_add1 x = ok y ∧
-  ↑y = 2 * ↑x + (1 : Int)
+  : mul2_add1 x ⦃ y => ↑y = 2 * ↑x + (1 : Int) ⦄
+  -- : ∃ y, mul2_add1 x = ok y ∧
+  -- ↑y = 2 * ↑x + (1 : Int)
   := by
   rw [mul2_add1]
   have ⟨ x1, hEq1, hPost1 ⟩ := @U32.add_spec x x (by scalar_tac)
@@ -20,23 +21,22 @@ theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
   simp [hEq2]
   scalar_tac
 
-/-- Theorem about `mul2_add1`: with the `progress` tactic -/
-@[pspec]
+/-- Theorem about `mul2_add1`: with the `step` tactic -/
 theorem mul2_add1_spec' (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
   : ∃ y, mul2_add1 x = ok y ∧
   ↑y = 2 * ↑x + (1 : Int)
   := by
   rw [mul2_add1]
-  progress with U32.add_spec as ⟨ x1 ⟩
-  progress as ⟨ x2 ⟩
+  step with U32.add_spec as ⟨ x1 ⟩
+  step as ⟨ x2 ⟩
   scalar_tac
 
 theorem mul2_add1_add_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
   ∃ z, mul2_add1_add x y = ok z ∧
   ↑z = 2 * ↑x + (1 : Int) + ↑y := by
   rw [mul2_add1_add]
-  progress as ⟨ x1 ⟩
-  progress as ⟨ x2 ⟩
+  step as ⟨ x1 ⟩
+  step as ⟨ x2 ⟩
   scalar_tac
 
 /- # Basic tactics -/
@@ -81,8 +81,8 @@ open CList
 theorem list_nth_mut1_spec {T: Type} [Inhabited T] (l : CList T) (i : U32)
   (h : i.val < l.toList.length) :
   ∃ x back, list_nth_mut1 l i = ok (x, back) ∧
-  x = l.toList.index i.toNat ∧
-  ∀ x', (back x').toList = l.toList.update i.toNat x' := by
+  x = l.toList[i.val]! ∧
+  ∀ x', (back x').toList = l.toList.set i.val x' := by
   rw [list_nth_mut1, list_nth_mut1_loop]
   split
   . rename_i hd tl
@@ -91,32 +91,32 @@ theorem list_nth_mut1_spec {T: Type} [Inhabited T] (l : CList T) (i : U32)
       simp
       split_conjs
       . -- Reasoning about `List.index`:
-        have hi : i.toNat = 0 := by scalar_tac
+        have hi : i.val = 0 := by scalar_tac
         simp only [hi] -- Without the `only`, this actually finished the goal
         have hIndex := List.index_zero_cons hd tl.toList
         simp only [hIndex]
       . intro x
         -- Reasoning about `List.update`:
-        have hi : i.toNat = 0 := by scalar_tac
+        have hi : i.val = 0 := by scalar_tac
         simp only [hi] -- Without the `only`, this actually finished the goal
         have hUpdate := List.update_zero_cons hd tl.toList x
         simp only [hUpdate]
     . simp at *
-      progress as ⟨ i1, hi1 ⟩
-      progress as ⟨ tl1, back, htl1, ih ⟩
+      step as ⟨ i1, hi1 ⟩
+      step as ⟨ tl1, back, htl1, ih ⟩
       simp
       split_conjs
-      . have hIndex := List.index_nzero_cons hd tl.toList i.toNat (by scalar_tac)
+      . have hIndex := List.index_nzero_cons hd tl.toList i.val (by scalar_tac)
         simp only [hIndex]
         simp only [htl1]
-        have hiEq : i1.toNat = i.toNat - 1 := by scalar_tac
+        have hiEq : i1.val = i.val - 1 := by scalar_tac
         simp only [hiEq]
       . -- Backward function
         intro x'
-        have hUpdate := List.update_nzero_cons hd tl.toList i.toNat x' (by scalar_tac)
+        have hUpdate := List.update_nzero_cons hd tl.toList i.val x' (by scalar_tac)
         simp only [hUpdate]
         -- simp at ih
-        have hiEq : i.toNat - 1 = (i1: ℤ).toNat := by scalar_tac
+        have hiEq : i.val - 1 = (i1: ℤ).val := by scalar_tac
         simp only [hiEq, ih]
   . simp_all
     scalar_tac
@@ -131,8 +131,8 @@ theorem list_nth_mut1_spec {T: Type} [Inhabited T] (l : CList T) (i : U32)
 theorem list_nth_mut1_spec' {T: Type} [Inhabited T] (l : CList T) (i : U32)
   (h : i.val < l.toList.length) :
   ∃ x back, list_nth_mut1 l i = ok (x, back) ∧
-  x = l.toList.index i.toNat ∧
-  ∀ x', (back x').toList = l.toList.update i.toNat x' := by
+  x = l.toList[i.val]! ∧
+  ∀ x', (back x').toList = l.toList.set i.val x' := by
   rw [list_nth_mut1, list_nth_mut1_loop]
   split
   . split
@@ -142,8 +142,8 @@ theorem list_nth_mut1_spec' {T: Type} [Inhabited T] (l : CList T) (i : U32)
       . intro x
         simp_all
     . simp at *
-      progress as ⟨ i1 ⟩
-      progress as ⟨ tl1, back ⟩
+      step as ⟨ i1 ⟩
+      step as ⟨ tl1, back ⟩
       simp
       split_conjs
       . simp [*]
@@ -154,7 +154,6 @@ theorem list_nth_mut1_spec' {T: Type} [Inhabited T] (l : CList T) (i : U32)
     scalar_tac
 
 /-- Theorem about `list_tail`: verbose version -/
-@[pspec]
 theorem list_tail_spec {T : Type} (l : CList T) :
   ∃ back, list_tail l = ok (CList.CNil, back) ∧
   ∀ tl', (back tl').toList = l.toList ++ tl'.toList := by
@@ -162,7 +161,7 @@ theorem list_tail_spec {T : Type} (l : CList T) :
   split
   . rename_i hd tl
     simp
-    progress as ⟨ back, hBack ⟩
+    step as ⟨ back, hBack ⟩
     -- This call to `simp` simplifies the `∃ ...`
     simp
     -- Proving the post-condition about the backward function
@@ -173,14 +172,13 @@ theorem list_tail_spec {T : Type} (l : CList T) :
     simp
 
 /-- Theorem about `list_tail: simple version -/
-@[pspec]
 theorem list_tail_spec' {T : Type} (l : CList T) :
   ∃ back, list_tail l = ok (CList.CNil, back) ∧
   ∀ tl', (back tl').toList = l.toList ++ tl'.toList := by
   rw [list_tail, list_tail_loop]
   split
   . simp
-    progress as ⟨ back ⟩
+    step as ⟨ back ⟩
     simp
     -- Proving the post-condition about the backward function
     intro tl'
@@ -188,22 +186,20 @@ theorem list_tail_spec' {T : Type} (l : CList T) :
   . simp
 
 /-- Theorem about `append_in_place` -/
-@[pspec]
 theorem append_in_place_spec {T : Type} (l0 l1 : CList T) :
   ∃ l2, append_in_place l0 l1 = ok l2 ∧
   l2.toList = l0.toList ++ l1.toList := by
   rw [append_in_place]
-  progress as ⟨ tl ⟩
+  step as ⟨ tl ⟩
   -- Nothing much to do here
   simp [*]
 
-@[pspec]
 theorem reverse_loop_spec {T : Type} (l : CList T) (out : CList T) :
   ∃ l', reverse_loop l out = ok l' ∧
   l'.toList = l.toList.reverse ++ out.toList := by
-  rw [reverse_loop]
+  rw [reverse_loop.eq_def]
   split
-  . progress as ⟨ l1, hl1 ⟩
+  . step as ⟨ l1, hl1 ⟩
     simp at *
     simp [hl1]
   . simp
@@ -212,7 +208,7 @@ theorem reverse_spec {T : Type} (l : CList T) :
   ∃ l', reverse l = ok l' ∧
   l'.toList = l.toList.reverse := by
   rw [reverse]
-  progress as ⟨ l', hl' ⟩
+  step as ⟨ l', hl' ⟩
   simp at hl'
   simp [hl']
 
@@ -234,36 +230,35 @@ def toInt_aux (l : List U32) : ℤ :=
 def toInt (x : alloc.vec.Vec U32) : ℤ := toInt_aux x.val
 
 /-- The theorem about `zero_loop` -/
-@[pspec]
 theorem zero_loop_spec
   (x : alloc.vec.Vec U32) (i : Usize) (h : i.val ≤ x.length) :
   ∃ x',
     zero_loop x i = ok x' ∧
     x'.length = x.length ∧
-    (∀ j, j < i.toNat → x'.val.index j = x.val.index j) ∧
-    (∀ j, i.toNat ≤ j → j < x.length → x'.val.index j = 0#u32) := by
-  rw [zero_loop]
+    (∀ j, j < i.val → x'.val[j]! = x.val[j]!) ∧
+    (∀ j, i.val ≤ j → j < x.length → x'.val[j]! = 0#u32) := by
+  rw [zero_loop.eq_def]
   simp
   split
-  . progress as ⟨ _ ⟩
-    progress as ⟨ i1 ⟩
-    progress as ⟨ x1, _, hSame, hZero ⟩
-    progress
+  . step as ⟨ _ ⟩
+    step as ⟨ i1 ⟩
+    step as ⟨ x1, _, hSame, hZero ⟩
+    step
     simp_all
     split_conjs
     . intro j h0
       replace hSame := hSame j (by scalar_tac)
       simp_all
     . intro j h0 h1
-      dcases j = i.toNat <;> simp_all
+      dcases j = i.val <;> simp_all
       have := hZero j (by scalar_tac)
       simp_all
   . simp; scalar_tac
-termination_by (x.length - i.val).toNat
+termination_by (x.length - i.val).val
 decreasing_by scalar_decr_tac
 
 theorem all_nil_impl_toInt_eq_zero
-  (l : List U32) (h : ∀ (j : ℕ), j < l.length → l.index j = 0#u32) :
+  (l : List U32) (h : ∀ (j : ℕ), j < l.length → l[j]! = 0#u32) :
   toInt_aux l = 0 := by
   match l with
   | [] => simp
@@ -284,7 +279,7 @@ theorem zero_spec (x : alloc.vec.Vec U32) :
     x'.length = x.length ∧
     toInt x' = 0 := by
   rw [zero]
-  progress as ⟨ x', hLength, hSame, hZero ⟩
+  step as ⟨ x', hLength, hSame, hZero ⟩
   simp_all
   apply all_nil_impl_toInt_eq_zero
   simp_all
@@ -295,7 +290,7 @@ theorem zero_spec (x : alloc.vec.Vec U32) :
  -/
 @[simp]
 theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) :
-  toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by
+  toInt_aux (l.drop i) = l[i]! + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by
   cases l with
   | nil => simp at *
   | cons hd tl =>
@@ -309,7 +304,7 @@ theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) :
 
 @[simp]
 theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length) :
-  toInt_aux (l.update i x) = toInt_aux l + 2 ^ (32 * i) * (x - l.index i) := by
+  toInt_aux (l[i]! x) = toInt_aux l + 2 ^ (32 * i) * (x - l[i]!) := by
   cases l with
   | nil => simp at *
   | cons hd tl =>
@@ -344,68 +339,67 @@ theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length)
       scalar_eq_nf
 
 /-- The proof about `add_no_overflow_loop` -/
-@[pspec]
 theorem add_no_overflow_loop_spec
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize)
   (hLength : x.length = y.length)
   -- No overflow occurs when we add the individual thunks
-  (hNoOverflow : ∀ (j : Nat), i.toNat ≤ j → j < x.length → (x.val.index j).val + (y.val.index j).val ≤ U32.max)
+  (hNoOverflow : ∀ (j : Nat), i.val ≤ j → j < x.length → (x.val[j]!).val + (y.val[j]!).val ≤ U32.max)
   (hi : i.val ≤ x.length) :
   ∃ x', add_no_overflow_loop x y i = ok x' ∧
   x'.length = x.length ∧
-  toInt x' = toInt x + 2 ^ (32 * i.toNat) * toInt_aux (y.val.drop i.toNat) := by
-  rw [add_no_overflow_loop]
+  toInt x' = toInt x + 2 ^ (32 * i.val) * toInt_aux (y.val.drop i.val) := by
+  rw [add_no_overflow_loop.eq_def]
   simp
   split
-  . progress as ⟨ yv ⟩
-    progress as ⟨ xv ⟩
-    progress as ⟨ sum ⟩
+  . step as ⟨ yv ⟩
+    step as ⟨ xv ⟩
+    step as ⟨ sum ⟩
     . -- This precondition is not proven automatically
-      have := hNoOverflow i.toNat (by scalar_tac) (by scalar_tac)
+      have := hNoOverflow i.val (by scalar_tac) (by scalar_tac)
       scalar_tac
-    progress as ⟨ i' ⟩
-    progress as ⟨ x1 ⟩
+    step as ⟨ i' ⟩
+    step as ⟨ x1 ⟩
     . -- This precondition is not proven automatically
       intro j h0 h1
       simp_all
-      -- Simplifying (x.update ...).index:
-      have := List.index_update_neq x.val i.toNat j sum (by scalar_tac)
+      -- Simplifying (x[]!...).index:
+      have := List.index_update_neq x.val i.val j sum (by scalar_tac)
       simp [*]
       apply hNoOverflow j (by scalar_tac) (by scalar_tac)
     -- Postcondition
     /- Note that you don't have to manually call the lemmas `toInt_aux_update`
         and `toInt_aux_drop` below if you first do:
         ```
-        have : i.toNat < x.length := by scalar_tac
+        have : i.val < x.length := by scalar_tac
         ```
         (simp_all will automatically apply the lemmas and prove the
         the precondition sby using the context)
       -/
     simp_all [toInt]
     scalar_eq_nf
-    -- Simplifying: toInt_aux ((↑x).update (↑i).toNat sum)
-    have := toInt_aux_update x.val i.toNat sum (by scalar_tac)
+    -- Simplifying: toInt_aux ((↑x)[]!(↑i).val sum)
+    have := toInt_aux_update x.val i.val sum (by scalar_tac)
     simp [*]; scalar_eq_nf
-    -- Simplifying: toInt_aux (List.drop (1 + (↑i).toNat) ↑y
-    have := toInt_aux_drop y.val i.toNat (by scalar_tac)
+    -- Simplifying: toInt_aux (List.drop (1 + (↑i).val) ↑y
+    have := toInt_aux_drop y.val i.val (by scalar_tac)
     simp [*]; scalar_eq_nf
   . simp_all
-termination_by (x.length - i.val).toNat
+termination_by (x.length - i.val).val
 decreasing_by scalar_decr_tac
 
 /-- The proof about `add_no_overflow` -/
 theorem add_no_overflow_spec (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32)
   (hLength : x.length = y.length)
-  (hNoOverflow : ∀ (j : Nat), j < x.length → (x.val.index j).val + (y.val.index j).val ≤ U32.max) :
+  (hNoOverflow : ∀ (j : Nat), j < x.length → (x.val[j]!).val + (y.val[j]!).val ≤ U32.max) :
   ∃ x', add_no_overflow x y = ok x' ∧
   x'.length = y.length ∧
   toInt x' = toInt x + toInt y := by
   rw [add_no_overflow]
-  progress as ⟨ x' ⟩ <;>
+  step as ⟨ x' ⟩ <;>
   simp_all [toInt]
 
 /-- The proof about `add_with_carry_loop` -/
-@[pspec]
+
 theorem add_with_carry_loop_spec
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (c0 : U8) (i : Usize)
   (hLength : x.length = y.length)
@@ -415,26 +409,26 @@ theorem add_with_carry_loop_spec
   x'.length = x.length ∧
   c1.val ≤ 1 ∧
   toInt x' + c1.val * 2 ^ (32 * x'.length) =
-    toInt x + 2 ^ (32 * i.toNat) * toInt_aux (y.val.drop i.toNat) + c0.val * 2 ^ (32 * i.toNat) := by
-  rw [add_with_carry_loop]
+    toInt x + 2 ^ (32 * i.val) * toInt_aux (y.val.drop i.val) + c0.val * 2 ^ (32 * i.val) := by
+  rw [add_with_carry_loop.eq_def]
   simp
   split
-  . progress as ⟨ xi ⟩
-    progress as ⟨ c0u ⟩
-    . progress as ⟨ s1, c1, hConv1 ⟩
-      progress as ⟨ yi ⟩
-      progress as ⟨ s2, c2, hConv2 ⟩
-      progress as ⟨ c1u ⟩
-      progress as ⟨ c2u ⟩
-      progress as ⟨ c3 ⟩
-      progress as ⟨ _ ⟩
-      progress as ⟨ i1 ⟩
-      progress as ⟨ x1 ⟩
+  . step as ⟨ xi ⟩
+    step as ⟨ c0u ⟩
+    . step as ⟨ s1, c1, hConv1 ⟩
+      step as ⟨ yi ⟩
+      step as ⟨ s2, c2, hConv2 ⟩
+      step as ⟨ c1u ⟩
+      step as ⟨ c2u ⟩
+      step as ⟨ c3 ⟩
+      step as ⟨ _ ⟩
+      step as ⟨ i1 ⟩
+      step as ⟨ x1 ⟩
       -- Proving the post-condition
       simp_all [toInt]
-      have hxUpdate := toInt_aux_update x.val i.toNat s2 (by scalar_tac)
+      have hxUpdate := toInt_aux_update x.val i.val s2 (by scalar_tac)
       simp [hxUpdate]; clear hxUpdate
-      have hyDrop := toInt_aux_drop y.val i.toNat (by scalar_tac)
+      have hyDrop := toInt_aux_drop y.val i.val (by scalar_tac)
       simp [hyDrop]; clear hyDrop
       scalar_eq_nf
       split at hConv1 <;>
@@ -442,11 +436,10 @@ theorem add_with_carry_loop_spec
       simp_all <;>
       scalar_eq_nf <;> simp [U32.max] <;> scalar_eq_nf
   . simp_all
-termination_by (x.length - i.val).toNat
+termination_by (x.length - i.val).val
 decreasing_by scalar_decr_tac
 
 /-- The proof about `add_with_carry` -/
-@[pspec]
 theorem add_with_carry_spec
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32)
   (hLength : x.length = y.length) :
@@ -455,7 +448,7 @@ theorem add_with_carry_spec
   c.val ≤ 1 ∧
   toInt x' + c.val * 2 ^ (32 * x'.length) = toInt x + toInt y := by
   rw [add_with_carry]
-  progress as ⟨ c, x' ⟩
+  step as ⟨ c, x' ⟩
   simp_all
 
 end tutorial
diff --git a/Tutorial/Tutorial.lean b/Tutorial/Tutorial.lean
index 0c75089..0ade22c 100644
--- a/Tutorial/Tutorial.lean
+++ b/Tutorial/Tutorial.lean
@@ -1,375 +1,433 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [tutorial]
-import Base
-open Primitives
+import Aeneas
+open Aeneas Aeneas.Std Result ControlFlow Error
 set_option linter.dupNamespace false
 set_option linter.hashCommand false
 set_option linter.unusedVariables false
 
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
 namespace tutorial
 
-/- [tutorial::choose]:
-   Source: 'src/lib.rs', lines 1:0-7:1 -/
+/-- [tutorial::choose]:
+    Source: 'src/lib.rs', lines 1:0-7:1 -/
 def choose
-  {T : Type} (b : Bool) (x : T) (y : T) : Result (T × (T → (T × T))) :=
+  {T : Type} (b : Bool) (x : T) (y : T) : Result (T × (T → (T × T))) := do
   if b
-  then let back := fun ret => (ret, y)
-       Result.ok (x, back)
-  else let back := fun ret => (x, ret)
-       Result.ok (y, back)
-
-/- [tutorial::mul2_add1]:
-   Source: 'src/lib.rs', lines 9:0-11:1 -/
-def mul2_add1 (x : U32) : Result U32 :=
-  do
+  then let back := fun x1 => (x1, y)
+       ok (x, back)
+  else let back := fun y1 => (x, y1)
+       ok (y, back)
+
+/-- [tutorial::mul2_add1]:
+    Source: 'src/lib.rs', lines 9:0-11:1 -/
+def mul2_add1 (x : Std.U32) : Result Std.U32 := do
   let i ← x + x
   i + 1#u32
 
-/- [tutorial::mul2_add1_add]:
-   Source: 'src/lib.rs', lines 13:0-15:1 -/
-def mul2_add1_add (x : U32) (y : U32) : Result U32 :=
-  do
+/-- [tutorial::mul2_add1_add]:
+    Source: 'src/lib.rs', lines 13:0-15:1 -/
+def mul2_add1_add (x : Std.U32) (y : Std.U32) : Result Std.U32 := do
   let i ← mul2_add1 x
   i + y
 
-/- [tutorial::incr]:
-   Source: 'src/lib.rs', lines 17:0-19:1 -/
-def incr (x : U32) : Result U32 :=
+/-- [tutorial::incr]:
+    Source: 'src/lib.rs', lines 17:0-19:1 -/
+def incr (x : Std.U32) : Result Std.U32 := do
   x + 1#u32
 
-/- [tutorial::use_incr]:
-   Source: 'src/lib.rs', lines 21:0-26:1 -/
-def use_incr : Result Unit :=
-  do
+/-- [tutorial::use_incr]:
+    Source: 'src/lib.rs', lines 21:0-26:1 -/
+def use_incr : Result Unit := do
   let x ← incr 0#u32
   let x1 ← incr x
   let _ ← incr x1
-  Result.ok ()
+  ok ()
 
-/- [tutorial::CList]
-   Source: 'src/lib.rs', lines 30:0-33:1 -/
-inductive CList (T : Type) :=
+/-- [tutorial::CList]
+    Source: 'src/lib.rs', lines 30:0-33:1 -/
+@[discriminant isize]
+inductive CList (T : Type) where
 | CCons : T → CList T → CList T
 | CNil : CList T
 
-/- [tutorial::list_nth]:
-   Source: 'src/lib.rs', lines 35:0-48:1 -/
-divergent def list_nth {T : Type} (l : CList T) (i : U32) : Result T :=
+/-- [tutorial::list_nth]:
+    Source: 'src/lib.rs', lines 35:0-48:1 -/
+def list_nth {T : Type} (l : CList T) (i : Std.U32) : Result T := do
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then Result.ok x
-    else do
-         let i1 ← i - 1#u32
+    then ok x
+    else let i1 ← i - 1#u32
          list_nth tl i1
-  | CList.CNil => Result.fail .panic
+  | CList.CNil => fail panic
+partial_fixpoint
 
-/- [tutorial::list_nth_mut]:
-   Source: 'src/lib.rs', lines 50:0-63:1 -/
-divergent def list_nth_mut
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
+/-- [tutorial::list_nth_mut]:
+    Source: 'src/lib.rs', lines 50:0-63:1 -/
+def list_nth_mut
+  {T : Type} (l : CList T) (i : Std.U32) : Result (T × (T → CList T)) := do
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then let back := fun ret => CList.CCons ret tl
-         Result.ok (x, back)
+    then let back := fun t => CList.CCons t tl
+         ok (x, back)
     else
-      do
       let i1 ← i - 1#u32
-      let (t, list_nth_mut_back) ← list_nth_mut tl i1
-      let back := fun ret => let tl1 := list_nth_mut_back ret
-                             CList.CCons x tl1
-      Result.ok (t, back)
-  | CList.CNil => Result.fail .panic
-
-/- [tutorial::list_nth1]: loop 0:
-   Source: 'src/lib.rs', lines 66:4-74:1 -/
-divergent def list_nth1_loop {T : Type} (l : CList T) (i : U32) : Result T :=
+      let (x1, list_nth_mut_back) ← list_nth_mut tl i1
+      let back := fun t => let tl1 := list_nth_mut_back t
+                           CList.CCons x tl1
+      ok (x1, back)
+  | CList.CNil => fail panic
+partial_fixpoint
+
+/-- [tutorial::list_nth1]: loop 0:
+    Source: 'src/lib.rs', lines 66:4-74:1 -/
+@[rust_loop]
+def list_nth1_loop {T : Type} (l : CList T) (i : Std.U32) : Result T := do
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then Result.ok x
-    else do
-         let i1 ← i - 1#u32
+    then ok x
+    else let i1 ← i - 1#u32
          list_nth1_loop tl i1
-  | CList.CNil => Result.fail .panic
+  | CList.CNil => fail panic
+partial_fixpoint
 
-/- [tutorial::list_nth1]:
-   Source: 'src/lib.rs', lines 65:0-74:1 -/
+/-- [tutorial::list_nth1]:
+    Source: 'src/lib.rs', lines 65:0-74:1 -/
 @[reducible]
-def list_nth1 {T : Type} (l : CList T) (i : U32) : Result T :=
+def list_nth1 {T : Type} (l : CList T) (i : Std.U32) : Result T := do
   list_nth1_loop l i
 
-/- [tutorial::i32_id]:
-   Source: 'src/lib.rs', lines 76:0-83:1 -/
-divergent def i32_id (i : I32) : Result I32 :=
+/-- [tutorial::i32_id]:
+    Source: 'src/lib.rs', lines 76:0-83:1 -/
+def i32_id (i : Std.I32) : Result Std.I32 := do
   if i = 0#i32
-  then Result.ok 0#i32
-  else do
-       let i1 ← i - 1#i32
+  then ok 0#i32
+  else let i1 ← i - 1#i32
        let i2 ← i32_id i1
        i2 + 1#i32
+partial_fixpoint
+
+mutual
 
-/- [tutorial::even]:
-   Source: 'src/lib.rs', lines 85:0-92:1 -/
-mutual divergent def even (i : U32) : Result Bool :=
+/-- [tutorial::even]:
+    Source: 'src/lib.rs', lines 85:0-92:1 -/
+def even (i : Std.U32) : Result Bool := do
   if i = 0#u32
-  then Result.ok true
-  else do
-       let i1 ← i - 1#u32
+  then ok true
+  else let i1 ← i - 1#u32
        odd i1
+partial_fixpoint
 
-/- [tutorial::odd]:
-   Source: 'src/lib.rs', lines 94:0-101:1 -/
-divergent def odd (i : U32) : Result Bool :=
+/-- [tutorial::odd]:
+    Source: 'src/lib.rs', lines 94:0-101:1 -/
+def odd (i : Std.U32) : Result Bool := do
   if i = 0#u32
-  then Result.ok false
-  else do
-       let i1 ← i - 1#u32
+  then ok false
+  else let i1 ← i - 1#u32
        even i1
+partial_fixpoint
 
 end
 
-/- Trait declaration: [tutorial::Counter]
-   Source: 'src/lib.rs', lines 105:0-107:1 -/
+/-- Trait declaration: [tutorial::Counter]
+    Source: 'src/lib.rs', lines 105:0-107:1 -/
 structure Counter (Self : Type) where
-  incr : Self → Result (Usize × Self)
+  incr : Self → Result (Std.Usize × Self)
 
-/- [tutorial::{tutorial::Counter for usize}::incr]:
-   Source: 'src/lib.rs', lines 110:4-114:5 -/
-def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
-  do
+/-- [tutorial::{tutorial::Counter for usize}::incr]:
+    Source: 'src/lib.rs', lines 110:4-114:5 -/
+def Usize.Insts.TutorialCounter.incr
+  (self : Std.Usize) : Result (Std.Usize × Std.Usize) := do
   let self1 ← self + 1#usize
-  Result.ok (self, self1)
+  ok (self, self1)
 
-/- Trait implementation: [tutorial::{tutorial::Counter for usize}]
-   Source: 'src/lib.rs', lines 109:0-115:1 -/
+/-- Trait implementation: [tutorial::{tutorial::Counter for usize}]
+    Source: 'src/lib.rs', lines 109:0-115:1 -/
 @[reducible]
-def CounterUsize : Counter Usize := {
-  incr := CounterUsize.incr
+def Usize.Insts.TutorialCounter : Counter Std.Usize := {
+  incr := Usize.Insts.TutorialCounter.incr
 }
 
-/- [tutorial::use_counter]:
-   Source: 'src/lib.rs', lines 117:0-119:1 -/
+/-- [tutorial::use_counter]:
+    Source: 'src/lib.rs', lines 117:0-119:1 -/
 def use_counter
-  {T : Type} (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
+  {T : Type} (CounterInst : Counter T) (cnt : T) :
+  Result (Std.Usize × T)
+  := do
   CounterInst.incr cnt
 
-/- [tutorial::list_nth_mut1]: loop 0:
-   Source: 'src/lib.rs', lines 124:4-132:1 -/
-divergent def list_nth_mut1_loop
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
+/-- [tutorial::list_nth_mut1]: loop 0:
+    Source: 'src/lib.rs', lines 124:4-132:1 -/
+@[rust_loop]
+def list_nth_mut1_loop
+  {T : Type} (l : CList T) (i : Std.U32) : Result (T × (T → CList T)) := do
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then let back := fun ret => CList.CCons ret tl
-         Result.ok (x, back)
+    then ok (x, fun t => CList.CCons t tl)
     else
-      do
       let i1 ← i - 1#u32
       let (t, back) ← list_nth_mut1_loop tl i1
-      let back1 := fun ret => let tl1 := back ret
-                              CList.CCons x tl1
-      Result.ok (t, back1)
-  | CList.CNil => Result.fail .panic
-
-/- [tutorial::list_nth_mut1]:
-   Source: 'src/lib.rs', lines 123:0-132:1 -/
+      let back1 := fun t1 => let c := back t1
+                             CList.CCons x c
+      ok (t, back1)
+  | CList.CNil => fail panic
+partial_fixpoint
+
+/-- [tutorial::list_nth_mut1]:
+    Source: 'src/lib.rs', lines 123:0-132:1 -/
 @[reducible]
 def list_nth_mut1
-  {T : Type} (l : CList T) (i : U32) : Result (T × (T → CList T)) :=
+  {T : Type} (l : CList T) (i : Std.U32) : Result (T × (T → CList T)) := do
   list_nth_mut1_loop l i
 
-/- [tutorial::list_tail]: loop 0:
-   Source: 'src/lib.rs', lines 135:4-137:5 -/
-divergent def list_tail_loop
-  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) :=
+/-- [tutorial::list_tail]: loop 0:
+    Source: 'src/lib.rs', lines 135:4-137:5 -/
+@[rust_loop]
+def list_tail_loop
+  {T : Type} (l : CList T) : Result (CList T → CList T) := do
   match l with
   | CList.CCons t tl =>
-    do
-    let (c, back) ← list_tail_loop tl
-    let back1 := fun ret => let tl1 := back ret
-                            CList.CCons t tl1
-    Result.ok (c, back1)
-  | CList.CNil => let back := fun ret => ret
-                  Result.ok (CList.CNil, back)
-
-/- [tutorial::list_tail]:
-   Source: 'src/lib.rs', lines 134:0-139:1 -/
-@[reducible]
+    let back ← list_tail_loop tl
+    ok (fun c => let c1 := back c
+                 CList.CCons t c1)
+  | CList.CNil => ok (fun c => c)
+partial_fixpoint
+
+/-- [tutorial::list_tail]:
+    Source: 'src/lib.rs', lines 134:0-139:1 -/
 def list_tail
-  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) :=
-  list_tail_loop l
+  {T : Type} (l : CList T) : Result ((CList T) × (CList T → CList T)) := do
+  let back ← list_tail_loop l
+  ok (CList.CNil, back)
 
-/- [tutorial::append_in_place]:
-   Source: 'src/lib.rs', lines 141:0-144:1 -/
+/-- [tutorial::append_in_place]:
+    Source: 'src/lib.rs', lines 141:0-144:1 -/
 def append_in_place
-  {T : Type} (l0 : CList T) (l1 : CList T) : Result (CList T) :=
-  do
+  {T : Type} (l0 : CList T) (l1 : CList T) : Result (CList T) := do
   let (_, list_tail_back) ← list_tail l0
-  Result.ok (list_tail_back l1)
+  ok (list_tail_back l1)
 
-/- [tutorial::reverse]: loop 0:
-   Source: 'src/lib.rs', lines 148:4-152:5 -/
-divergent def reverse_loop
-  {T : Type} (l : CList T) (out : CList T) : Result (CList T) :=
+/-- [tutorial::reverse]: loop 0:
+    Source: 'src/lib.rs', lines 148:4-152:5 -/
+@[rust_loop]
+def reverse_loop
+  {T : Type} (l : CList T) (out : CList T) : Result (CList T) := do
   match l with
   | CList.CCons hd tl => reverse_loop tl (CList.CCons hd out)
-  | CList.CNil => Result.ok out
+  | CList.CNil => ok out
+partial_fixpoint
 
-/- [tutorial::reverse]:
-   Source: 'src/lib.rs', lines 146:0-154:1 -/
-def reverse {T : Type} (l : CList T) : Result (CList T) :=
+/-- [tutorial::reverse]:
+    Source: 'src/lib.rs', lines 146:0-154:1 -/
+@[reducible]
+def reverse {T : Type} (l : CList T) : Result (CList T) := do
   reverse_loop l CList.CNil
 
-/- [tutorial::zero]: loop 0:
-   Source: 'src/lib.rs', lines 164:4-167:5 -/
-divergent def zero_loop
-  (x : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
+/-- [tutorial::zero]: loop body 0:
+    Source: 'src/lib.rs', lines 165:4-168:5 -/
+@[rust_loop_body]
+def zero_loop.body
+  (x : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.Usize) (alloc.vec.Vec
+    Std.U32))
+  := do
   let i1 := alloc.vec.Vec.len x
   if i < i1
   then
-    do
     let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i2 ← i + 1#usize
     let x1 := index_mut_back 0#u32
-    zero_loop x1 i2
-  else Result.ok x
-
-/- [tutorial::zero]:
-   Source: 'src/lib.rs', lines 162:0-168:1 -/
-def zero (x : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
+    ok (cont (x1, i2))
+  else ok (done x)
+
+/-- [tutorial::zero]: loop 0:
+    Source: 'src/lib.rs', lines 165:4-168:5 -/
+@[rust_loop]
+def zero_loop
+  (x : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
+  loop
+    (fun (x1, i1) => zero_loop.body x1 i1)
+    (x, i)
+
+/-- [tutorial::zero]:
+    Source: 'src/lib.rs', lines 162:0-169:1 -/
+@[reducible]
+def zero (x : alloc.vec.Vec Std.U32) : Result (alloc.vec.Vec Std.U32) := do
   zero_loop x 0#usize
 
-/- [tutorial::add_no_overflow]: loop 0:
-   Source: 'src/lib.rs', lines 177:4-180:5 -/
-divergent def add_no_overflow_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize) :
-  Result (alloc.vec.Vec U32)
-  :=
+/-- [tutorial::add_no_overflow]: loop body 0:
+    Source: 'src/lib.rs', lines 182:4-185:5 -/
+@[rust_loop_body]
+def add_no_overflow_loop.body
+  (y : alloc.vec.Vec Std.U32) (x : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.Usize) (alloc.vec.Vec
+    Std.U32))
+  := do
   let i1 := alloc.vec.Vec.len x
   if i < i1
   then
-    do
     let i2 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) y i
     let (i3, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i4 ← i3 + i2
     let i5 ← i + 1#usize
     let x1 := index_mut_back i4
-    add_no_overflow_loop x1 y i5
-  else Result.ok x
-
-/- [tutorial::add_no_overflow]:
-   Source: 'src/lib.rs', lines 175:0-181:1 -/
+    ok (cont (x1, i5))
+  else ok (done x)
+
+/-- [tutorial::add_no_overflow]: loop 0:
+    Source: 'src/lib.rs', lines 182:4-185:5 -/
+@[rust_loop]
+def add_no_overflow_loop
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) (i : Std.Usize) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
+  loop
+    (fun (x1, i1) => add_no_overflow_loop.body y x1 i1)
+    (x, i)
+
+/-- [tutorial::add_no_overflow]:
+    Source: 'src/lib.rs', lines 176:0-186:1 -/
+@[reducible]
 def add_no_overflow
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (alloc.vec.Vec U32)
-  :=
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
   add_no_overflow_loop x y 0#usize
 
-/- [tutorial::add_with_carry]: loop 0:
-   Source: 'src/lib.rs', lines 190:4-197:5 -/
-divergent def add_with_carry_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (c0 : U8) (i : Usize) :
-  Result (U8 × (alloc.vec.Vec U32))
-  :=
+/-- [tutorial::add_with_carry]: loop body 0:
+    Source: 'src/lib.rs', lines 203:4-210:5 -/
+@[rust_loop_body]
+def add_with_carry_loop.body
+  (y : alloc.vec.Vec Std.U32) (x : alloc.vec.Vec Std.U32) (c0 : Std.U8)
+  (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.U8 × Std.Usize) (Std.U8
+    × (alloc.vec.Vec Std.U32)))
+  := do
   let i1 := alloc.vec.Vec.len x
   if i < i1
   then
-    do
     let i2 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) x i
-    let i3 ← Scalar.cast .U32 c0
-    let p ← core.num.U32.overflowing_add i2 i3
-    let (sum, c1) := p
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) x i
+    let i3 ← lift (UScalar.cast .U32 c0)
+    let (sum, c1) ← lift (core.num.U32.overflowing_add i2 i3)
     let i4 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
-    let p1 ← core.num.U32.overflowing_add sum i4
-    let (sum1, c2) := p1
-    let i5 ← Scalar.cast_bool .U8 c1
-    let i6 ← Scalar.cast_bool .U8 c2
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) y i
+    let (sum1, c2) ← lift (core.num.U32.overflowing_add sum i4)
+    let i5 ← lift (UScalar.cast_fromBool .U8 c1)
+    let i6 ← lift (UScalar.cast_fromBool .U8 c2)
     let c01 ← i5 + i6
     let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i7 ← i + 1#usize
     let x1 := index_mut_back sum1
-    add_with_carry_loop x1 y c01 i7
-  else Result.ok (c0, x)
-
-/- [tutorial::add_with_carry]:
-   Source: 'src/lib.rs', lines 186:0-199:1 -/
+    ok (cont (x1, c01, i7))
+  else ok (done (c0, x))
+
+/-- [tutorial::add_with_carry]: loop 0:
+    Source: 'src/lib.rs', lines 203:4-210:5 -/
+@[rust_loop]
+def add_with_carry_loop
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) (c0 : Std.U8)
+  (i : Std.Usize) :
+  Result (Std.U8 × (alloc.vec.Vec Std.U32))
+  := do
+  loop
+    (fun (x1, c01, i1) => add_with_carry_loop.body y x1 c01 i1)
+    (x, c0, i)
+
+/-- [tutorial::add_with_carry]:
+    Source: 'src/lib.rs', lines 191:0-212:1 -/
+@[reducible]
 def add_with_carry
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (U8 × (alloc.vec.Vec U32))
-  :=
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) :
+  Result (Std.U8 × (alloc.vec.Vec Std.U32))
+  := do
   add_with_carry_loop x y 0#u8 0#usize
 
-/- [tutorial::max]:
-   Source: 'src/lib.rs', lines 201:0-203:1 -/
-def max (x : Usize) (y : Usize) : Result Usize :=
+/-- [tutorial::max]:
+    Source: 'src/lib.rs', lines 214:0-216:1 -/
+def max (x : Std.Usize) (y : Std.Usize) : Result Std.Usize := do
   if x > y
-  then Result.ok x
-  else Result.ok y
+  then ok x
+  else ok y
 
-/- [tutorial::get_or_zero]:
-   Source: 'src/lib.rs', lines 205:0-207:1 -/
-def get_or_zero (y : alloc.vec.Vec U32) (i : Usize) : Result U32 :=
+/-- [tutorial::get_or_zero]:
+    Source: 'src/lib.rs', lines 218:0-220:1 -/
+def get_or_zero
+  (y : alloc.vec.Vec Std.U32) (i : Std.Usize) : Result Std.U32 := do
   let i1 := alloc.vec.Vec.len y
   if i < i1
-  then alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) y i
-  else Result.ok 0#u32
-
-/- [tutorial::add]: loop 0:
-   Source: 'src/lib.rs', lines 221:4-229:5 -/
-divergent def add_loop
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (max1 : Usize) (c0 : U8)
-  (i : Usize) :
-  Result (alloc.vec.Vec U32)
-  :=
+  then alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) y i
+  else ok 0#u32
+
+/-- [tutorial::add]: loop body 0:
+    Source: 'src/lib.rs', lines 235:4-244:5 -/
+@[rust_loop_body]
+def add_loop.body
+  (y : alloc.vec.Vec Std.U32) (max1 : Std.Usize) (x : alloc.vec.Vec Std.U32)
+  (c0 : Std.U8) (i : Std.Usize) :
+  Result (ControlFlow ((alloc.vec.Vec Std.U32) × Std.U8 × Std.Usize)
+    ((alloc.vec.Vec Std.U32) × Std.U8))
+  := do
   if i < max1
   then
-    do
     let yi ← get_or_zero y i
     let i1 ←
-      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSliceTInst U32) x i
-    let i2 ← Scalar.cast .U32 c0
-    let p ← core.num.U32.overflowing_add i1 i2
-    let (sum, c1) := p
-    let p1 ← core.num.U32.overflowing_add sum yi
-    let (sum1, c2) := p1
-    let i3 ← Scalar.cast_bool .U8 c1
-    let i4 ← Scalar.cast_bool .U8 c2
+      alloc.vec.Vec.index (core.slice.index.SliceIndexUsizeSlice Std.U32) x i
+    let i2 ← lift (UScalar.cast .U32 c0)
+    let (sum, c1) ← lift (core.num.U32.overflowing_add i1 i2)
+    let (sum1, c2) ← lift (core.num.U32.overflowing_add sum yi)
+    let i3 ← lift (UScalar.cast_fromBool .U8 c1)
+    let i4 ← lift (UScalar.cast_fromBool .U8 c2)
     let c01 ← i3 + i4
     let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst U32)
-        x i
+      alloc.vec.Vec.index_mut (core.slice.index.SliceIndexUsizeSlice Std.U32) x
+        i
     let i5 ← i + 1#usize
     let x1 := index_mut_back sum1
-    add_loop x1 y max1 c01 i5
-  else
-    if c0 != 0#u8
-    then do
-         let i1 ← Scalar.cast .U32 c0
-         alloc.vec.Vec.push x i1
-    else Result.ok x
-
-/- [tutorial::add]:
-   Source: 'src/lib.rs', lines 214:0-235:1 -/
+    ok (cont (x1, c01, i5))
+  else ok (done (x, c0))
+
+/-- [tutorial::add]: loop 0:
+    Source: 'src/lib.rs', lines 235:4-244:5 -/
+@[rust_loop]
+def add_loop
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) (max1 : Std.Usize)
+  (c0 : Std.U8) (i : Std.Usize) :
+  Result ((alloc.vec.Vec Std.U32) × Std.U8)
+  := do
+  loop
+    (fun (x1, c01, i1) => add_loop.body y max1 x1 c01 i1)
+    (x, c0, i)
+
+/-- [tutorial::add]:
+    Source: 'src/lib.rs', lines 227:0-250:1 -/
 def add
-  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) :
-  Result (alloc.vec.Vec U32)
-  :=
-  do
+  (x : alloc.vec.Vec Std.U32) (y : alloc.vec.Vec Std.U32) :
+  Result (alloc.vec.Vec Std.U32)
+  := do
   let i := alloc.vec.Vec.len x
   let i1 := alloc.vec.Vec.len y
   let max1 ← max i i1
   let x1 ← alloc.vec.Vec.resize core.clone.CloneU32 x max1 0#u32
-  add_loop x1 y max1 0#u8 0#usize
+  let (x2, c0) ← add_loop x1 y max1 0#u8 0#usize
+  if c0 != 0#u8
+  then let i2 ← lift (UScalar.cast .U32 c0)
+       alloc.vec.Vec.push x2 i2
+  else ok x2
 
 end tutorial
diff --git a/lake-manifest.json b/lake-manifest.json
index 7be5955..e199408 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,85 +1,102 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"type": "path",
+   "scope": "",
+   "name": "base",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../aeneas/backends/lean",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "698d2b68b870f1712040ab0c233d34372d4b56df",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0-rc8",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53",
-   "name": "batteries",
+   "rev": "22a0afa903bcf65285152eea298a3d319badc78d",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
-   "name": "Qq",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
-   "name": "aesop",
+   "rev": "db22912cdd820b2a2bd84bd25273cb322ff09ead",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "136730b5a40dc633967f5433cb7668df5c3bf9a3",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.94",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "3426969888a264d3f69b6f30ab50aa11f28eb38d",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
-   "name": "importGraph",
+   "rev": "3a9fde028258300f1cbb003d457d47c8d8e16b1c",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71",
-   "name": "mathlib",
+   "scope": "leanprover-community",
+   "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/AeneasVerif/aeneas.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
-   "subDir": "backends/lean",
-   "scope": "",
-   "rev": "ee2f13b3451b79083082682a4acfed2db3cdd936",
-   "name": "base",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "v4.29.0-rc8",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "tutorial",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 7a912e2..8294e97 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,8 +1,14 @@
 import Lake
 open Lake DSL
 
+-- require base from "../aeneas/backends/lean"
 require base from git
   "https://github.com/AeneasVerif/aeneas.git" @ "main" / "backends/lean"
 
 package «tutorial» {}
-@[default_target] lean_lib Tutorial
+@[default_target] lean_lib Tutorial where
+  roots := #[
+    `Tutorial.Exercises,
+    `Tutorial.Tutorial,
+    -- `Tutorial.Solutions -- TODO: fix and reenable
+  ]
diff --git a/lean-toolchain b/lean-toolchain
index e7a4f40..b58ff4f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc2
+leanprover/lean4:v4.29.0-rc8
\ No newline at end of file
diff --git a/source/Cargo.toml b/source/Cargo.toml
index 7a5a488..3068e74 100644
--- a/source/Cargo.toml
+++ b/source/Cargo.toml
@@ -1,7 +1,7 @@
 [package]
 name = "tutorial"
 version = "0.1.0"
-edition = "2021"
+edition = "2024"
 
 [lib]
 name = "tutorial"
diff --git a/source/src/lib.rs b/source/src/lib.rs
index f826062..0be92e8 100644
--- a/source/src/lib.rs
+++ b/source/src/lib.rs
@@ -160,6 +160,7 @@ pub type Bignum = Vec<u32>;
 
 /// Zero out a bignum
 pub fn zero(x : &mut Bignum) {
+    // x.fill(0)
     let mut i = 0;
     while i < x.len() {
         x[i] = 0;
@@ -173,6 +174,10 @@ pub fn zero(x : &mut Bignum) {
 /// - they have the same length
 /// - there is no overflow when suming the individual thunks
 pub fn add_no_overflow(x: &mut Bignum, y: &Bignum) {
+    // .zip() pairs up elements from x and y safely
+    // for (a, &b) in x.iter_mut().zip(y.iter()) {
+    //     *a += b;
+    // }
     let mut i = 0;
     while i < x.len() {
         x[i] += y[i]; // We assume this doesn't overflow
@@ -184,6 +189,14 @@ pub fn add_no_overflow(x: &mut Bignum, y: &Bignum) {
 ///
 /// We assume the bignums have the same length
 pub fn add_with_carry(x: &mut Bignum, y: &Bignum) -> u8 {
+    // let mut carry = 0u8;
+    // for (a, &b) in x.iter_mut().zip(y.iter()) {
+    //     let (sum, c1) = a.overflowing_add(carry as u32);
+    //     let (sum, c2) = sum.overflowing_add(b);
+    //     carry = c1 as u8 + c2 as u8;
+    //     *a = sum;
+    // }
+    // carry
     let mut c0 = 0u8;
     let mut i = 0;
     // Remark: we have (and need) the invariant that: c0 <= 1
@@ -213,6 +226,7 @@ fn get_or_zero(y : &Bignum, i : usize) -> u32 {
 /// numbers have a fixed size, but is interesting as an exercise.
 pub fn add(x: &mut Bignum, y: &Bignum) {
     let max = max(x.len(), y.len());
+    // let max = std::cmp::max(x.len(), y.len());
     x.resize(max, 0u32);
     // now: length x >= length y
     let mut c0 = 0u8;
@@ -220,6 +234,7 @@ pub fn add(x: &mut Bignum, y: &Bignum) {
     // Remark: we have (and need) the invariant that: c0 <= 1
     while i < max {
         let yi = get_or_zero(y, i);
+        // let yi = y.get(i).copied().unwrap_or(0);
         let (sum, c1) = x[i].overflowing_add(c0 as u32);
         let (sum, c2) = sum.overflowing_add(yi);
         // We have: c1 as u8 + c2 as u8 <= 1
@@ -234,15 +249,22 @@ pub fn add(x: &mut Bignum, y: &Bignum) {
     }
 }
 
-#[test]
-fn test() {
-    // TODO:
-    // let mut x = vec![0xffffffffu32];
-    // let mut y = vec![0xffffffffu32];
-    let mut x = Vec::from([0xffffffffu32]);
-    let mut y = Vec::from([0xffffffffu32]);
-    let carry = add_with_carry(&mut x, &mut y);
-    assert!(carry == 1);
-    assert!(x.len() == 1);
-    assert!(x[0] == 0xfffffffe);
+#[cfg(test)] // This ensures tests are only compiled when running `cargo test`
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test() {
+        // TODO:
+        let mut x = vec![0xffffffffu32];
+        let mut y = vec![0xffffffffu32];
+        // let mut x = Vec::from([0xffffffffu32]);
+        // let mut y = Vec::from([0xffffffffu32]);
+        let carry = add_with_carry(&mut x, &mut y);
+        assert_eq!(carry, 1);
+        assert_eq!(x.len(), 1);
+        assert_eq!(x[0], 0xfffffffe);
+
+        // assert_eq!(even(10_000_000), true) // NOTE: this will crash with stack overflow because written using recursion
+    }
 }

From a7f10aced96df9c89633036e2093929302d5cc4d Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Fri, 22 May 2026 12:14:34 +0700
Subject: [PATCH 2/2] feat: update latest lean

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index b58ff4f..6c7e31f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc8
\ No newline at end of file
+leanprover/lean4:v4.30.0-rc2