diff --git a/lean/CoreModels.lean b/lean/CoreModels.lean
index 432c69d..5630275 100644
--- a/lean/CoreModels.lean
+++ b/lean/CoreModels.lean
@@ -3,3 +3,4 @@ import CoreModels.Core
 import CoreModels.Alloc
 import CoreModels.HaxLib
 import CoreModels.RustPrimitives
+import CoreModels.Spec
diff --git a/lean/CoreModels/Spec.lean b/lean/CoreModels/Spec.lean
new file mode 100644
index 0000000..4ecd61a
--- /dev/null
+++ b/lean/CoreModels/Spec.lean
@@ -0,0 +1,2 @@
+import CoreModels.Spec.Aeneas
+import CoreModels.Spec.Array
diff --git a/lean/CoreModels/Spec/Aeneas.lean b/lean/CoreModels/Spec/Aeneas.lean
new file mode 100644
index 0000000..ff9f28e
--- /dev/null
+++ b/lean/CoreModels/Spec/Aeneas.lean
@@ -0,0 +1,107 @@
+import CoreModels.Core.Funs
+
+namespace Aeneas.Std
+open Std.Do WP Std.Do Result
+
+set_option mvcgen.warning false
+
+@[spec]
+theorem Result.ok_spec {α : Type} {a : α} {Q} (hQ : (Q.1 a).down) :
+  ⦃ ⌜ True ⌝ ⦄ Result.ok a ⦃ Q ⦄ := by simpa [Triple]
+
+@[spec]
+theorem Result.fail_spec {α : Type} {e : Error} {Q} (hQ : (Q.2.1 e).down) :
+  ⦃ ⌜ True ⌝ ⦄ (Result.fail e : Result α) ⦃ Q ⦄ := by simpa [Triple]
+
+attribute [spec] Function.uncurry lift
+
+@[spec]
+theorem loop_spec
+  {α β γ : Type}
+  {P : PostCond β (PostShape.except Error (PostShape.except PUnit.{1} PostShape.pure))}
+  (body : α → Result (ControlFlow α β)) (init : α)
+  (inv : α → Prop)
+  (rel : γ → γ → Prop)
+  (termination : α → γ)
+  (hwf : WellFounded rel)
+  (h_inv_init : inv init)
+  (h_body : ∀ x, inv x → ⦃ ⌜ True ⌝ ⦄ body x ⦃ post⟨
+    fun cf => match cf with
+      | .cont r => ⌜ inv r ∧ (rel (termination r) (termination x) ∨ (P.2.2.1 ()).down) ⌝
+      | .done r => P.1 r,
+    P.2.1, P.2.2.1⟩ ⦄) :
+  ⦃ ⌜ True ⌝ ⦄ loop body init ⦃ P ⦄ := by
+  suffices h : ∀ x, inv x → (wp⟦loop body x⟧ P).down by
+    unfold Triple
+    intro _
+    exact h init h_inv_init
+  by_cases hdiv : (P.2.2.1 ()).down
+  · -- Divergence permitted: use partial-fixpoint induction.
+    intro x hinv
+    delta loop
+    refine Lean.Order.fix_induct (loop._proof_1 body)
+      (motive := fun g => ∀ x, inv x → (wp⟦g x⟧ P).down) ?_ ?_ x hinv
+    · apply Lean.Order.admissible_pi
+      intro y
+      apply Lean.Order.admissible_pi
+      intro _
+      apply Lean.Order.admissible_apply (β := fun _ => Result β)
+        (P := fun y r => (wp⟦r⟧ P).down) y
+      exact Lean.Order.admissible_flatOrder _ hdiv
+    · intro g IH y hinvy
+      have hb : (wp⟦body y⟧ _).down := h_body y hinvy trivial
+      cases hbe : body y with
+      | ok cf =>
+        rw [hbe] at hb
+        cases cf with
+        | cont r => exact IH r hb.1
+        | done r => exact hb
+      | fail e => rw [hbe] at hb; exact hb
+      | div => rw [hbe] at hb; exact hb
+  · -- Termination via WF induction on `rel`.
+    intro x hinv
+    induction hg : termination x using hwf.induction generalizing x
+    rename_i g IH
+    have hb : (wp⟦body x⟧ _).down := h_body x hinv trivial
+    rw [loop.eq_1]
+    cases hbe : body x with
+    | ok cf =>
+      rw [hbe] at hb
+      cases cf with
+      | cont r =>
+        obtain ⟨hinvr, hrel | hd⟩ := hb
+        · subst hg
+          exact IH (termination r) hrel r hinvr rfl
+        · exact absurd hd hdiv
+      | done r => exact hb
+    | fail e => rw [hbe] at hb; exact hb
+    | div => rw [hbe] at hb; exact hb
+
+open ScalarElab
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I8_spec (a : «%S») (b : I8) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I16_spec (a : «%S») (b : I16) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I32_spec (a : «%S») (b : I32) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I64_spec (a : «%S») (b : I64) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I128_spec (a : «%S») (b : I128) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+end Aeneas.Std
diff --git a/lean/CoreModels/Spec/Array.lean b/lean/CoreModels/Spec/Array.lean
new file mode 100644
index 0000000..1aa21d3
--- /dev/null
+++ b/lean/CoreModels/Spec/Array.lean
@@ -0,0 +1,144 @@
+import CoreModels.Core.Funs
+import CoreModels.Spec.Aeneas
+
+
+namespace CoreModels
+
+open Aeneas
+open Aeneas.Std hiding namespace core alloc
+open Std.Do WP Std.Do Result
+set_option mvcgen.warning false
+
+open ScalarElab
+
+uscalar @[spec] theorem «%S».Core_modelsCmpPartialEqArray.eq_spec {N : Std.Usize} {Q}
+  (a : Array «%S» N) (b : Array «%S» N) (h : (Q.1 (a.val == b.val)).down) :
+  ⦃ ⌜ True ⌝ ⦄
+  core.Array.Insts.CoreCmpPartialEqArray.eq core.«%S».Insts.CoreCmpPartialEq'S a b
+  ⦃ Q ⦄ := by
+  mvcgen -trivial [core.Array.Insts.CoreCmpPartialEqArray.eq,
+    core.Array.Insts.CoreCmpPartialEqArray.eq_loop,
+    core.Array.Insts.CoreCmpPartialEqArray.eq_loop.body, rust_primitives.slice.array_index,
+    core.«%S».Insts.CoreCmpPartialEq'S]
+  case vc1.γ => exact Nat
+  case vc4.termination => exact fun i => N.val - i.val
+  case vc3.rel => exact (· < ·)
+  case vc5.hwf => exact wellFounded_lt
+  case vc2.inv => exact fun i => a.val.take i.val = b.val.take i.val
+  case vc10 =>
+    constructor
+    · simp_all [@List.take_add, @List.take_one, -List.take_append_getElem]
+    · grind
+  · grind
+  · grind
+  · grind
+  · grind
+  · convert h; grind
+  · convert h; grind [List.take_eq_self_iff, List.Vector.length_val]
+
+@[spec]
+theorem core_models_Array_Insts_index_RangeUsize_spec
+      {T : Type} {N : Std.Usize} (arr : Std.Array T N)
+      (r : core.ops.range.Range Std.Usize)
+      (h0 : r.start.val < r.end.val) -- TODO: We should be able to allow "≤" here
+      (h1 : r.end.val ≤ N.val) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.Array.Insts.CoreOpsIndexIndexRangeUsizeSlice.index arr r
+    ⦃ ⇓ r' => ⌜ r'.val = arr.val.slice r.start.val r.end.val ∧
+                r'.val.length + r.start.val = r.end.val ⌝ ⦄ := by
+  mvcgen [core.Array.Insts.CoreOpsIndexIndexRangeUsizeSlice.index,
+    rust_primitives.slice.array_slice, -Array.subslice_spec.mvcgen_spec, Array.subslice]
+    <;> grind
+
+
+/-! ## A generic `from_fn` pure-closure spec.
+
+Analogous to `createi_pure_spec` (HacspecBridge.lean:663) but takes
+a `FnMut` instance directly (no `Fn` wrapper). Required because
+`sponge.xor_block_into_state` calls `CoreModels.core.array.from_fn` directly
+with the `FnMut` instance of its closure. -/
+
+private theorem from_fn_foldlM_pure_aux
+    {T F : Type}
+    (inst : CoreModels.core.ops.function.FnMut F Std.Usize T) (c : F) (f : Nat → T)
+    (l : List Nat) (acc : List T)
+    (hpure : ∀ k ∈ l,
+      inst.call_mut c ⟨BitVec.ofNat _ k⟩ = .ok (f k, c)) :
+    l.foldlM
+      (fun (s : List T × F) (i : Nat) => do
+        let (v, f') ← inst.call_mut s.2 ⟨BitVec.ofNat _ i⟩
+        Result.ok (s.1 ++ [v], f'))
+      (acc, c) = .ok (acc ++ l.map f, c) := by
+  induction l generalizing acc with
+  | nil =>
+      simp only [List.foldlM_nil, List.map_nil, List.append_nil]; rfl
+  | cons h t ih =>
+      have hh : inst.call_mut c ⟨BitVec.ofNat _ h⟩ = .ok (f h, c) :=
+        hpure h List.mem_cons_self
+      have ht : ∀ k ∈ t, inst.call_mut c ⟨BitVec.ofNat _ k⟩ = .ok (f k, c) :=
+        fun k hk => hpure k (List.mem_cons_of_mem _ hk)
+      have hih := ih (acc ++ [f h]) ht
+      simp only [List.foldlM_cons, hh, bind_tc_ok, List.map_cons]
+      rw [hih]
+      simp [List.append_assoc]
+
+/-- Lean-level equation for `from_fn` over pure closures. -/
+private theorem from_fn_pure_eq
+    {T F : Type} (N : Std.Usize)
+    (inst : CoreModels.core.ops.function.FnMut F Std.Usize T) (c : F) (f : Nat → T)
+    (hpure : ∀ k : Nat, k < N.val →
+      inst.call_mut c ⟨BitVec.ofNat _ k⟩ = .ok (f k, c)) :
+    CoreModels.core.array.from_fn N inst c =
+      .ok ⟨(List.range N.val).map f,
+           by simp [List.length_map, List.length_range]⟩ := by
+  have hf : ∀ k ∈ List.range N.val,
+      inst.call_mut c ⟨BitVec.ofNat _ k⟩ = .ok (f k, c) := by
+    intro k hk; exact hpure k (List.mem_range.mp hk)
+  have h_fold :=
+    from_fn_foldlM_pure_aux inst c f (List.range N.val) [] hf
+  simp only [List.nil_append] at h_fold
+  unfold CoreModels.core.array.from_fn CoreModels.rust_primitives.slice.array_from_fn
+  split
+  · rename_i e heq
+    rw [h_fold] at heq; exact absurd heq (by simp)
+  · rename_i heq
+    rw [h_fold] at heq; exact absurd heq (by simp)
+  · rename_i result heq
+    rw [h_fold] at heq
+    have hres : result = ((List.range N.val).map f, c) :=
+      (Result.ok.inj heq).symm
+    subst hres
+    rfl
+
+
+/-- **Generic pure-closure `[spec]` for `core_models.array.from_fn`.**
+
+For any closure whose `call_mut` is pure (doesn't mutate state),
+`from_fn N inst c` succeeds and its `i`-th cell is `f i`. `hpure` is a
+Triple over each `call_mut` so `hax_mvcgen` can recurse through it via
+per-closure `@[spec]` lemmas. -/
+@[spec]
+theorem from_fn_pure_spec
+    {T F : Type} [Inhabited T] (N : Std.Usize)
+    (inst : core.ops.function.FnMut F Std.Usize T) (c : F) (f : Nat → T)
+    (hpure : ∀ k : Nat, k < N.val →
+      ⦃ ⌜ True ⌝ ⦄
+      inst.call_mut c ⟨BitVec.ofNat _ k⟩
+      ⦃ ⇓ r => ⌜ r = (f k, c) ⌝ ⦄) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.array.from_fn N inst c
+    ⦃ ⇓ a => ⌜ ∀ i : Nat, i < N.val → a.val[i]! = f i ⌝ ⦄ := by
+  have hpure_eq : ∀ k : Nat, k < N.val →
+      inst.call_mut c ⟨BitVec.ofNat _ k⟩ = .ok (f k, c) :=
+    sorry -- fun k hk => result_eq_of_triple (hpure k hk)
+  have heq := from_fn_pure_eq N inst c f hpure_eq
+  rw [heq]
+  simp only [Triple, WP.wp]
+  apply SPred.pure_intro
+  intro i hi
+  show ((List.range N.val).map f)[i]! = f i
+  rw [List.getElem!_eq_getElem?_getD, List.getElem?_map,
+      List.getElem?_range hi]
+  rfl
+
+end CoreModels
diff --git a/lean/CoreModels/Spec/Iterator.lean b/lean/CoreModels/Spec/Iterator.lean
new file mode 100644
index 0000000..5c4ea2a
--- /dev/null
+++ b/lean/CoreModels/Spec/Iterator.lean
@@ -0,0 +1,29 @@
+import CoreModels.Core.Funs
+import CoreModels.Alloc.Funs
+import CoreModels.Spec.Aeneas
+
+namespace CoreModels
+
+open Aeneas
+open Aeneas.Std hiding namespace core alloc
+open Std.Do WP Std.Do Result
+
+set_option mvcgen.warning false
+
+@[spec]
+theorem IteratorRange_next_CoreIterRangeStep_spec (i e : Usize) {Q}
+      (h_lt : (h : i.val < e.val) →
+        ∀ (s : Usize), s.val = i.val + 1 → (Q.1 (some i, { start := s, «end» := e })).down)
+      (h_ge : i.val ≥ e.val → (Q.1 (none, { start := i, «end» := e })).down) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.IteratorRange.next core.Usize.Insts.CoreIterRangeStep
+      { start := i, «end» := e }
+    ⦃ Q ⦄ := by
+  unfold core.IteratorRange.next core.Usize.Insts.CoreIterRangeStep
+  simp only [core.Usize.Insts.CoreCmpPartialOrdUsize, core.mkUPartialOrd,
+    core.Usize.Insts.CoreCloneClone.clone, core.Usize.Insts.CoreIterRangeStep.forward_checked,
+    core.convert.TryFromUTInfallible.Blanket.try_from, core.convert.From.Blanket.from,
+    core.num.Usize.checked_add, core.num.Usize.overflowing_add,
+    rust_primitives.arithmetic.overflowing_add_usize]
+  mvcgen [uncurry]
+    <;> grind [UScalar.overflowing_add, BitVec.uaddOverflow, UScalar.overflowing_add_eq]
diff --git a/lean/CoreModels/Spec/Slice.lean b/lean/CoreModels/Spec/Slice.lean
new file mode 100644
index 0000000..87578fd
--- /dev/null
+++ b/lean/CoreModels/Spec/Slice.lean
@@ -0,0 +1,215 @@
+import CoreModels.Spec.Aeneas
+
+namespace CoreModels
+
+
+open Aeneas
+open Aeneas.Std hiding namespace core alloc
+open Std.Do WP Std.Do Result
+
+set_option mvcgen.warning false
+
+attribute [spec]
+  CoreModels.core.slice.Slice.len
+  massert
+  CoreModels.core.num.U8.from_le_bytes
+  CoreModels.core.num.U16.from_le_bytes
+  CoreModels.core.num.U32.from_le_bytes
+  CoreModels.core.num.U64.from_le_bytes
+  CoreModels.core.num.U128.from_le_bytes
+  CoreModels.core.num.Usize.from_le_bytes
+  CoreModels.core.num.U8.to_le_bytes
+  CoreModels.core.num.U16.to_le_bytes
+  CoreModels.core.num.U32.to_le_bytes
+  CoreModels.core.num.U64.to_le_bytes
+  CoreModels.core.num.U128.to_le_bytes
+  CoreModels.core.num.Usize.to_le_bytes
+  rust_primitives.arithmetic.from_le_bytes_u8
+  rust_primitives.arithmetic.from_le_bytes_u16
+  rust_primitives.arithmetic.from_le_bytes_u32
+  rust_primitives.arithmetic.from_le_bytes_u64
+  rust_primitives.arithmetic.from_le_bytes_u128
+  rust_primitives.arithmetic.from_le_bytes_usize
+  rust_primitives.arithmetic.to_le_bytes_u8
+  rust_primitives.arithmetic.to_le_bytes_u16
+  rust_primitives.arithmetic.to_le_bytes_u32
+  rust_primitives.arithmetic.to_le_bytes_u64
+  rust_primitives.arithmetic.to_le_bytes_u128
+  rust_primitives.arithmetic.to_le_bytes_usize
+
+@[spec]
+theorem CoreOpsIndexIndexRangeUsizeSlice_index_spec
+    {T : Type} (s : Slice T) (r : core.ops.range.Range Std.Usize)
+    (h0 : r.start.val < r.end.val) -- TODO: we should be able to allow "≤"
+    (h1 : r.end.val ≤ s.val.length) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice.index s r
+    ⦃ ⇓ r' => ⌜ r'.val = s.val.slice r.start.val r.end.val ∧
+                r.start.val + r'.val.length = r.end.val ⌝ ⦄ := by
+  mvcgen [core.Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice.index,
+    rust_primitives.slice.slice_slice, -Slice.subslice_spec.mvcgen_spec, Slice.subslice]
+    <;> grind
+
+
+/-! ### `CoreModels.core.Array.Insts.CoreConvertTryFromShared0SliceTryFromSliceError.try_from`
+
+The body invokes `CoreModels.rust_primitives.slice.array_from_fn` on the `try_from`
+closure (whose state is just the source `Slice T`). The proof has three
+parts:
+
+1. Closure step: `call_mut s i = .ok (s.val[i.val]!, s)` for `i.val <
+   s.length` — the closure reads the slice and preserves its state.
+2. `foldlM` invariant: induction on `k` shows that folding the closure
+   over `List.range' 0 k` (starting from `([], s)`) returns
+   `(s.val.take k, s)` when `k ≤ s.length`.
+3. Final assembly: `array_from_fn N closure s = .ok (Array.make N s.val)`
+   when `s.length = N.val`, hence `try_from N inst s = .ok (.Ok a)` with
+   `a.val = s.val`. -/
+
+/-- Closure step lemma. The `try_from` closure's state is the source
+    `Slice T`; `call_mut` reads the `i`-th element and preserves state.
+
+    We state this on the unfolded form `...call_mut.call_mut cpy s i`
+    because that's what the FnMut instance's `call_mut` field reduces to
+    after Lean unfolds the structure projection. -/
+private theorem try_from_closure_call_mut_eq
+    {T : Type} [Inhabited T] {N : Std.Usize} (cpy : CoreModels.core.marker.Copy T)
+    (s : Slice T) (i : Std.Usize) (h : i.val < s.val.length) :
+    CoreModels.core.convert.TryFromArrayShared0SliceTryFromSliceError.try_from.closure.Insts.CoreOpsFunctionFnMutTupleUsizeT.call_mut
+      (T := T) (N := N) cpy s i =
+      .ok (s.val[i.val]!, s) := by
+  -- Reduces to `do let t ← slice_index s i; ok (t, s)`.
+  unfold CoreModels.core.convert.TryFromArrayShared0SliceTryFromSliceError.try_from.closure.Insts.CoreOpsFunctionFnMutTupleUsizeT.call_mut
+  unfold CoreModels.rust_primitives.slice.slice_index Std.Slice.index_usize
+  -- Now `s[i]?` matches; for `i.val < s.length`, `s[i]? = some s.val[i.val]!`.
+  have hsome : s[i]? = some s.val[i.val]! := by
+    simp only [Std.Slice.getElem?_Usize_eq]
+    rw [List.getElem?_eq_getElem h, List.getElem!_eq_getElem?_getD,
+        List.getElem?_eq_getElem h]
+    rfl
+  rw [hsome]
+  rfl
+
+/-- The closure-fold accumulator at step `k` is `s.val.take k`. We prove
+    a slightly stronger invariant: starting from any accumulator `acc`
+    with the closure state `s`, folding over `List.range' acc.length k`
+    yields `(acc ++ s.val.slice acc.length (acc.length + k), s)` when
+    `acc.length + k ≤ s.length` and acc lines up with the slice prefix. -/
+private theorem foldlM_try_from_closure_invariant
+    {T : Type} [Inhabited T] {N : Std.Usize} (cpy : CoreModels.core.marker.Copy T)
+    (s : Slice T)
+    (_hN : s.val.length ≤ Std.Usize.max) :
+    ∀ (k start : Nat) (acc : List T),
+      acc = s.val.take start →
+      start + k ≤ s.val.length →
+      start + k ≤ Std.Usize.max →
+      (List.range' start k).foldlM
+        (fun (p : List T × Slice T) (i : Nat) => do
+          let (v, f') ←
+            CoreModels.core.convert.TryFromArrayShared0SliceTryFromSliceError.try_from.closure.Insts.CoreOpsFunctionFnMutTupleUsizeT.call_mut
+              (T := T) (N := N) cpy p.2 ⟨BitVec.ofNat _ i⟩
+          ok (p.1 ++ [v], f'))
+        (acc, s)
+      = .ok (s.val.take (start + k), s) := by
+  intro k
+  induction k with
+  | zero =>
+    intro start acc hacc hk1 hk2
+    show List.foldlM _ (acc, s) (List.range' start 0) = _
+    rw [show List.range' start 0 = [] from rfl]
+    rw [List.foldlM_nil]
+    show Result.ok (acc, s) = Result.ok (s.val.take (start + 0), s)
+    rw [hacc, Nat.add_zero]
+  | succ k ih =>
+    intro start acc hacc hk1 hk2
+    -- `List.range' start (k+1) = start :: List.range' (start+1) k`
+    rw [show List.range' start (k + 1) = start :: List.range' (start + 1) k from rfl]
+    simp only [List.foldlM_cons]
+    -- The step at `start` calls `call_mut s ⟨BitVec.ofNat _ start⟩`.
+    have hstart_lt : start < s.val.length := by omega
+    have hstart_max : start ≤ Std.Usize.max := by omega
+    have hval : (⟨BitVec.ofNat Std.UScalarTy.Usize.numBits start⟩ : Std.Usize).val = start := by
+      grind [Nat.mod_eq_of_lt, Std.Usize.max_def, Std.Usize.numBits_def, UScalar.val]
+    have hcall := try_from_closure_call_mut_eq (T := T) (N := N) cpy s
+                    ⟨BitVec.ofNat _ start⟩ (by rw [hval]; exact hstart_lt)
+    -- Rewrite both the closure-call output's `.val` and the `i` arg uniformly.
+    rw [hval] at hcall
+    rw [hcall]
+    simp only [bind_tc_ok]
+    -- New accumulator is `acc ++ [s.val[start]!] = s.val.take (start + 1)`.
+    have hacc' : acc ++ [s.val[start]!] = s.val.take (start + 1) := by
+      rw [hacc]
+      have : start < s.val.length := hstart_lt
+      rw [List.take_add_one]
+      simp [List.getElem?_eq_getElem this, List.getElem!_eq_getElem?_getD]
+    -- Now apply IH at `start := start + 1`. Note `(start + 1) + k = start + (k + 1)`.
+    have ih' := ih (start + 1) (acc ++ [s.val[start]!]) hacc' (by omega) (by omega)
+    have h_assoc : (start + 1) + k = start + (k + 1) := by omega
+    rw [h_assoc] at ih'
+    exact ih'
+
+/-- `array_from_fn N (try_from closure) s = .ok (Array.make N s.val)`
+    when `s.length = N.val`. -/
+theorem array_from_fn_try_from_eq_ok
+    {T : Type} [Inhabited T] {N : Std.Usize} (cpy : CoreModels.core.marker.Copy T)
+    (s : Slice T) (hlen : s.val.length = N.val) :
+    CoreModels.rust_primitives.slice.array_from_fn N
+      (CoreModels.core.convert.TryFromArrayShared0SliceTryFromSliceError.try_from.closure.Insts.CoreOpsFunctionFnMutTupleUsizeT
+        (T := T) (N := N) cpy) s
+    = .ok (Std.Array.make N s.val (by simp [hlen])) := by
+  -- Foldl invariant at start=0, k=N.val, acc=[].
+  have hN_max : s.val.length ≤ Std.Usize.max := by
+    have := s.property; exact this
+  have hN_max' : N.val ≤ Std.Usize.max := by
+    rw [← hlen]; exact hN_max
+  have h_fold :=
+    foldlM_try_from_closure_invariant (T := T) (N := N) cpy s hN_max
+      N.val 0 [] (by simp) (by omega) (by omega)
+  -- Normalize `0 + N.val = N.val` and reduce `take N.val s.val = s.val`.
+  simp only [Nat.zero_add] at h_fold
+  have h_take : s.val.take N.val = s.val :=
+    List.take_of_length_le (by omega)
+  rw [h_take] at h_fold
+  -- Match `range N.val` with `range' 0 N.val` (`range` is defined as `range' 0 _`).
+  have hrange : (List.range N.val) = List.range' 0 N.val := List.range_eq_range'
+  -- The `array_from_fn` definition is a `match` on the foldlM result.
+  -- We can't `rw [hrange]` (dependent motive); instead transfer h_fold to the
+  -- `List.range` form first, then unfold and split.
+  rw [← hrange] at h_fold
+  unfold CoreModels.rust_primitives.slice.array_from_fn
+  -- Now transport the foldlM equation through the `split`.
+  split
+  · rename_i e heq
+    rw [h_fold] at heq; exact absurd heq (by simp)
+  · rename_i heq
+    rw [h_fold] at heq; exact absurd heq (by simp)
+  · rename_i result heq
+    rw [h_fold] at heq
+    have hres : result = (s.val, s) := (Result.ok.inj heq).symm
+    subst hres
+    rfl
+
+/-- The main Triple: `try_from N cpy s` succeeds with `Ok (Array.make N s.val _)`,
+    whenever `s.val.length = N.val`. -/
+@[spec]
+theorem core_models_array_try_from_slice_spec
+    {T : Type} [Inhabited T] {N : Std.Usize} (cpy : CoreModels.core.marker.Copy T)
+    (s : Slice T) (hlen : s.val.length = N.val) :
+    ⦃ ⌜ True ⌝ ⦄
+    CoreModels.core.Array.Insts.CoreConvertTryFromShared0SliceTryFromSliceError.try_from
+      N cpy s
+    ⦃ ⇓ r => ⌜ r = CoreModels.core.result.Result.Ok
+                    (Std.Array.make N s.val (by simp [hlen])) ⌝ ⦄ := by
+  -- Unfold try_from and reduce the `do` chain step-by-step.
+  unfold CoreModels.core.Array.Insts.CoreConvertTryFromShared0SliceTryFromSliceError.try_from
+  -- `CoreModels.core.slice.Slice.len x` is `pure (Slice.len x)`, returns `.ok (Slice.len s)`.
+  unfold CoreModels.core.slice.Slice.len
+  -- The if-decision: `Slice.len s = N` reduces to `s.val.length = N.val`.
+  have hi_eq : (Std.Slice.len s) = N := by
+    apply Std.UScalar.eq_of_val_eq
+    simp [hlen]
+  -- Reduce the array_from_fn call to .ok.
+  have h_afn := array_from_fn_try_from_eq_ok (T := T) (N := N) cpy s hlen
+  simp only [Triple, WP.wp, Pure.pure, bind_tc_ok, hi_eq, if_true, h_afn]
+  intro _
+  trivial