Add some proofs for the Lean backend (#255)

* Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan>
author: Son HO 2024-06-21 23:24:01 +0200
committer: GitHub 2024-06-21 23:24:01 +0200
commit: 4d30546c809cb2c512e0c3fd8ee540fff1330eab (patch)
tree: d83926c9aa30f7bfb2a1c6db0e776003bca63355
parent: f264b9dcc6331eb9149d951f308cdc61c8c02801 (diff)
18 files changed, 1163 insertions, 165 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index fb6b12e5..320b4b53 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -52,10 +52,6 @@ theorem int_pos_ind (p : Int → Prop) :
     rename_i m
     cases m <;> simp_all
 
--- We sometimes need this to make sure no natural numbers appear in the goals
--- TODO: there is probably something more general to do
-theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp
-
 -- This is mostly used in termination proofs
 theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) :
   ↑(x.toNat) < y := by
@@ -68,4 +64,8 @@ theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ)
   have : 0 ≤ x := by omega
   simp [Int.toNat_sub_of_le, *]
 
+-- WARNING: do not use this with `simp` as it might loop. The left-hand side indeed reduces to the
+-- righ-hand side, meaning the rewriting can be applied to `n` itself.
+theorem ofNat_instOfNatNat_eq (n : Nat) : @OfNat.ofNat Nat n (instOfNatNat n) = n := by rfl
+
 end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 068d6f2f..b1927cfd 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -3,6 +3,7 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
+import Mathlib.Tactic.Ring.RingNF
 import Base.Utils
 import Base.Arith.Base
 
@@ -111,7 +112,7 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
   let hs := HashSet.empty
   -- Explore the declarations
   let decls ← ctx.getDecls
-  let hs ← decls.foldlM (fun hs d => do 
+  let hs ← decls.foldlM (fun hs d => do
     -- Collect instances over all subexpressions in the context.
     -- Note that we explore the *type* of the local declarations: if we have
     -- for instance `h : A ∧ B` in the context, the expression itself is simply
@@ -154,7 +155,7 @@ def lookupHasIntPred (e : Expr) : MetaM (Option Expr) :=
   lookupProp "lookupHasIntPred" ``HasIntPred e (fun term => pure #[term]) (fun _ => pure #[])
 
 -- Collect the instances of `HasIntPred` for the subexpressions in the context
-def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do 
+def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
   collectInstancesFromMainCtx lookupHasIntPred
 
 -- Return an instance of `PropHasImp` for `e` if it has some
@@ -201,7 +202,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
     -- Add a declaration
     let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
-    Utils.simpAt true {} #[] [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
+    Utils.simpAt true {} [] [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
     -- Return the new value
     pure nval
 
@@ -214,7 +215,7 @@ def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
 elab "intro_has_int_prop_instances" : tactic => do
   let _ ← introHasIntPropInstances
 
-def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do 
+def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do
   trace[Arith] "Introducing the HasIntPred instances"
   introInstances ``HasIntPred.concl lookupHasIntPred
 
@@ -230,6 +231,8 @@ def introPropHasImpInstances : Tactic.TacticM (Array Expr) := do
 elab "intro_prop_has_imp_instances" : tactic => do
   let _ ← introPropHasImpInstances
 
+def intTacSimpRocs : List Name := [``Int.reduceNegSucc, ``Int.reduceNeg]
+
 /- Boosting a bit the `omega` tac.
  -/
 def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
@@ -244,7 +247,33 @@ def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM U
   extraPreprocess
   -- Reduce all the terms in the goal - note that the extra preprocessing step
   -- might have proven the goal, hence the `Tactic.allGoals`
-  Tactic.allGoals do tryTac (dsimpAt false {} #[] [] [] [] Tactic.Location.wildcard)
+  let dsimp :=
+    Tactic.allGoals do tryTac (
+      -- We set `simpOnly` at false on purpose
+      dsimpAt false {} intTacSimpRocs
+        -- Declarations to unfold
+        []
+        -- Theorems
+        []
+        [] Tactic.Location.wildcard)
+  dsimp
+  -- More preprocessing: apply norm_cast to the whole context
+  Tactic.allGoals (Utils.tryTac (Utils.normCastAtAll))
+  -- norm_cast does weird things with negative numbers so we reapply simp
+  dsimp
+  -- We also need this, in case the goal is: ¬ False
+  Tactic.allGoals do tryTac (
+    Utils.simpAt true {}
+               -- Simprocs
+               intTacSimpRocs
+               -- Unfoldings
+               []
+                -- Simp lemmas
+                [``not_false_eq_true]
+                -- Hypotheses
+                []
+                (.targets #[] true)
+  )
 
 elab "int_tac_preprocess" : tactic =>
   intTacPreprocess (do pure ())
@@ -260,8 +289,6 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess :  Tactic
   -- Preprocess - wondering if we should do this before or after splitting
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
-  -- More preprocessing
-  Tactic.allGoals (Utils.tryTac (Utils.simpAt true {} #[] [] [``nat_zero_eq_int_zero] [] .wildcard))
   -- Split the conjunctions in the goal
   if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call omega
@@ -298,4 +325,11 @@ example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) :
 example (a : Prop) (x : Int) (h0: 0 < x) (h1: x < 0) : a := by
   int_tac
 
+-- Intermediate cast through natural numbers
+example (a : Prop) (x : Int) (h0: (0 : Nat) < x) (h1: x < 0) : a := by
+  int_tac
+
+example (x : Int) (h : x ≤ -3) : x ≤ -2 := by
+  int_tac
+
 end Arith
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index ecc5acaf..31110b95 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -19,7 +19,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
   -- Reveal the concrete bounds, simplify calls to [ofInt]
   Utils.simpAt true {}
                -- Simprocs
-               #[]
+               intTacSimpRocs
                -- Unfoldings
                [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
                 ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
@@ -59,11 +59,11 @@ instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
   -- prop_ty is inferred
   prop := λ x => And.intro x.hmin x.hmax
 
-example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+example (x _y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   intro_has_int_prop_instances
   simp [*]
 
-example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+example (x _y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   scalar_tac
 
 -- Checking that we explore the goal *and* projectors correctly
@@ -92,4 +92,10 @@ example (x : U32) (h0 : ¬ x = U32.ofInt 0) : 0 < x.val := by
 example {u: U64} (h1: (u : Int) < 2): (u : Int) = 0 ∨ (u : Int) = 1 := by
   scalar_tac
 
+example (x : I32) : -100000000000 < x.val := by
+  scalar_tac
+
+example : (Usize.ofInt 2).val ≠ 0 := by
+  scalar_tac
+
 end Arith
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 96843f55..ab71daed 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -43,6 +43,9 @@ def index [Inhabited α] (ls : List α) (i : Int) : α :=
 
 @[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
 @[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
+@[simp] theorem index_zero_lt_cons [Inhabited α] (hne : 0 < i) : index ((x :: tl) : List α) i = index tl (i - 1) := by
+  have : i ≠ 0 := by scalar_tac
+  simp [*, index]
 
 theorem indexOpt_bounds (ls : List α) (i : Int) :
   ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i :=
@@ -453,16 +456,18 @@ theorem index_update_eq
         simp at *
         apply index_update_eq <;> scalar_tac
 
-theorem update_map_eq {α : Type u} {β : Type v} (ls : List α) (i : Int) (x : α) (f : α → β) :
+@[simp]
+theorem map_update_eq {α : Type u} {β : Type v} (ls : List α) (i : Int) (x : α) (f : α → β) :
   (ls.update i x).map f = (ls.map f).update i (f x) :=
   match ls with
   | [] => by simp
   | hd :: tl =>
     if h : i = 0 then by simp [*]
     else
-      have hi := update_map_eq tl (i - 1) x f
+      have hi := map_update_eq tl (i - 1) x f
       by simp [*]
 
+@[simp]
 theorem len_flatten_update_eq {α : Type u} (ls : List (List α)) (i : Int) (x : List α)
   (h0 : 0 ≤ i) (h1 : i < ls.len) :
   (ls.update i x).flatten.len = ls.flatten.len + x.len - (ls.index i).len :=
@@ -476,6 +481,20 @@ theorem len_flatten_update_eq {α : Type u} (ls : List (List α)) (i : Int) (x :
       simp [*]
       int_tac
 
+theorem len_index_le_len_flatten (ls : List (List α)) :
+  forall (i : Int), (ls.index i).len ≤ ls.flatten.len := by
+  induction ls <;> intro i <;> simp_all
+  . rw [List.index]
+    simp [default]
+  . rename ∀ _, _ => ih
+    if hi: i = 0 then
+      simp_all
+      int_tac
+    else
+      replace ih := ih (i - 1)
+      simp_all
+      int_tac
+
 @[simp]
 theorem index_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] (ls : List α) (i : Int) (f : α → β)
   (h0 : 0 ≤ i) (h1 : i < ls.len) :
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index be460987..899871af 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -129,7 +129,7 @@ example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
 def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
 
 -- TODO: very annoying that the α is an explicit parameter
-def Slice.len (α : Type u) (v : Slice α) : Usize :=
+abbrev Slice.len (α : Type u) (v : Slice α) : Usize :=
   Usize.ofIntCore v.val.len (by constructor <;> scalar_tac)
 
 @[simp]
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 9f809ead..31038e0d 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1301,22 +1301,25 @@ instance {ty} : LT (Scalar ty) where
 
 instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val
 
--- Not marking this one with @[simp] on purpose
+-- Not marking this one with @[simp] on purpose: if we have `x = y` somewhere in the context,
+-- we may want to use it to substitute `y` with `x` somewhere.
+-- TODO: mark it as simp anyway?
 theorem Scalar.eq_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x = y ↔ (↑x : Int) = ↑y := by
   cases x; cases y; simp_all
 
 -- This is sometimes useful when rewriting the goal with the local assumptions
+-- TODO: this doesn't get triggered
 @[simp] theorem Scalar.eq_imp {ty : ScalarTy} (x y : Scalar ty) :
   (↑x : Int) = ↑y → x = y := (eq_equiv x y).mpr
 
-theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
+@[simp] theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x < y ↔ (↑x : Int) < ↑y := by simp [LT.lt]
 
 @[simp] theorem Scalar.lt_imp {ty : ScalarTy} (x y : Scalar ty) :
   (↑x : Int) < (↑y) → x < y := (lt_equiv x y).mpr
 
-theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
+@[simp] theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x ≤ y ↔ (↑x : Int) ≤ ↑y := by simp [LE.le]
 
 @[simp] theorem Scalar.le_imp {ty : ScalarTy} (x y : Scalar ty) :
@@ -1377,8 +1380,6 @@ theorem coe_max {ty: ScalarTy} (a b: Scalar ty): ↑(Max.max a b) = (Max.max (�
   -- TODO: there should be a shorter way to prove this.
   rw [max_def, max_def]
   split_ifs <;> simp_all
-  refine' absurd _ (lt_irrefl a)
-  exact lt_of_le_of_lt (by assumption) ((Scalar.lt_equiv _ _).2 (by assumption))
 
 -- Max theory
 -- TODO: do the min theory later on.
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 0b010944..e584777a 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -33,14 +33,15 @@ abbrev Vec.v {α : Type u} (v : Vec α) : List α := v.val
 example {a: Type u} (v : Vec a) : v.length ≤ Scalar.max ScalarTy.Usize := by
   scalar_tac
 
-def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+abbrev Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
 
 instance (α : Type u) : Inhabited (Vec α) := by
   constructor
   apply Vec.new
 
 -- TODO: very annoying that the α is an explicit parameter
-def Vec.len (α : Type u) (v : Vec α) : Usize :=
+@[simp]
+abbrev Vec.len (α : Type u) (v : Vec α) : Usize :=
   Usize.ofIntCore v.val.len (by constructor <;> scalar_tac)
 
 @[simp]
@@ -63,6 +64,14 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
   else
     fail maximumSizeExceeded
 
+@[pspec]
+theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.len < Usize.max) :
+  ∃ v1, v.push α x = ok v1 ∧
+  v1.val = v.val ++ [x] := by
+  simp [push]
+  split <;> simp_all [List.len_eq_length]
+  scalar_tac
+
 -- This shouldn't be used
 def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
   if i.val < v.length then
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index da601b73..35cc8399 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -131,7 +131,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     Tactic.focus do
     let _ ←
       tryTac
-        (simpAt true {} #[] []
+        (simpAt true {} [] []
                [``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
                [hEq.fvarId!] (.targets #[] true))
     -- It may happen that at this point the goal is already solved (though this is rare)
@@ -140,7 +140,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     else
        trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
        -- TODO: remove this (some types get unfolded too much: we "fold" them back)
-       let _ ← tryTac (simpAt true {} #[] [] scalar_eqs [] .wildcard_dep)
+       let _ ← tryTac (simpAt true {} [] [] scalar_eqs [] .wildcard_dep)
        trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
        -- Clear the equality, unless the user requests not to do so
        let mgoal ← do
@@ -410,7 +410,7 @@ namespace Test
     -- This spec theorem is suboptimal, but it is good to check that it works
     progress with Scalar.add_spec as ⟨ z, h1 .. ⟩
     simp [*, h1]
- 
+
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
     ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 5954f048..b9de2fd1 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -664,21 +664,26 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
    Something very annoying is that there is no function which allows to
    initialize a simp context without doing an elaboration - as a consequence
    we write our own here. -/
-def mkSimpCtx (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
-  Tactic.TacticM Simp.Context := do
+def mkSimpCtx (simpOnly : Bool) (config : Simp.Config) (kind : SimpKind)
+  (simprocs : List Name) (declsToUnfold : List Name)
+  (thms : List Name) (hypsToUse : List FVarId) :
+  Tactic.TacticM (Simp.Context × Simp.SimprocsArray) := do
   -- Initialize either with the builtin simp theorems or with all the simp theorems
   let simpThms ←
     if simpOnly then Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
     else getSimpTheorems
   -- Add the equational theorem for the declarations to unfold
+  let addDeclToUnfold (thms : SimpTheorems) (decl : Name) : Tactic.TacticM SimpTheorems :=
+    if kind == .dsimp then pure (thms.addDeclToUnfoldCore decl)
+    else thms.addDeclToUnfold decl
   let simpThms ←
-    declsToUnfold.foldlM (fun thms decl => thms.addDeclToUnfold decl) simpThms
+    declsToUnfold.foldlM addDeclToUnfold simpThms
   -- Add the hypotheses and the rewriting theorems
   let simpThms ←
     hypsToUse.foldlM (fun thms fvarId =>
-      -- post: TODO: don't know what that is
+      -- post: TODO: don't know what that is. It seems to be true by default.
       -- inv: invert the equality
-      thms.add (.fvar fvarId) #[] (mkFVar fvarId) (post := false) (inv := false)
+      thms.add (.fvar fvarId) #[] (mkFVar fvarId) (post := true) (inv := false)
       -- thms.eraseCore (.fvar fvar)
       ) simpThms
   -- Add the rewriting theorems to use
@@ -693,7 +698,10 @@ def mkSimpCtx (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Nam
         throwError "Not a proposition: {thmName}"
       ) simpThms
   let congrTheorems ← getSimpCongrTheorems
-  pure { config, simpTheorems := #[simpThms], congrTheorems }
+  let defaultSimprocs ← if simpOnly then pure {} else Simp.getSimprocs
+  let simprocs ← simprocs.foldlM (fun simprocs name => simprocs.add name true) defaultSimprocs
+  let ctx := { config, simpTheorems := #[simpThms], congrTheorems }
+  pure (ctx, #[simprocs])
 
 inductive Location where
   /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/
@@ -725,30 +733,30 @@ def customSimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (dis
       simpLocation.go ctx simprocs discharge? tgts (simplifyTarget := true)
 
 /- Call the simp tactic. -/
-def simpAt (simpOnly : Bool) (config : Simp.Config) (simprocs : Simp.SimprocsArray)
+def simpAt (simpOnly : Bool) (config : Simp.Config) (simprocs : List Name)
   (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) (loc : Location) :
   Tactic.TacticM Unit := do
   -- Initialize the simp context
-  let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse
+  let (ctx, simprocs) ← mkSimpCtx simpOnly config .simp simprocs declsToUnfold thms hypsToUse
   -- Apply the simplifier
   let _ ← customSimpLocation ctx simprocs (discharge? := .none) loc
 
 /- Call the dsimp tactic. -/
-def dsimpAt (simpOnly : Bool) (config : Simp.Config) (simprocs : Simp.SimprocsArray)
+def dsimpAt (simpOnly : Bool) (config : Simp.Config) (simprocs : List Name)
   (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) (loc : Tactic.Location) :
   Tactic.TacticM Unit := do
   -- Initialize the simp context
-  let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse
+  let (ctx, simprocs) ← mkSimpCtx simpOnly config .dsimp simprocs declsToUnfold thms hypsToUse
   -- Apply the simplifier
   dsimpLocation ctx simprocs loc
 
 -- Call the simpAll tactic
-def simpAll (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
+def simpAll (config : Simp.Config) (simprocs : List Name) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
   Tactic.TacticM Unit := do
   -- Initialize the simp context
-  let ctx ← mkSimpCtx false config declsToUnfold thms hypsToUse
+  let (ctx, simprocs) ← mkSimpCtx false config .simpAll simprocs declsToUnfold thms hypsToUse
   -- Apply the simplifier
-  let _ ← Lean.Meta.simpAll (← getMainGoal) ctx
+  let _ ← Lean.Meta.simpAll (← getMainGoal) ctx simprocs
 
 /- Adapted from Elab.Tactic.Rewrite -/
 def rewriteTarget (eqThm : Expr) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
@@ -811,4 +819,12 @@ def rewriteAt (cfg : Rewrite.Config) (rpt : Bool)
   else
     evalRewriteSeqAux cfg thms loc
 
+/-- Apply norm_cast to the whole context -/
+def normCastAtAll : TacticM Unit := do
+  withMainContext do
+  let ctx ← Lean.MonadLCtx.getLCtx
+  let decls ← ctx.getDecls
+  NormCast.normCastTarget
+  decls.forM (fun d => NormCast.normCastHyp d.fvarId)
+
 end Utils
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 39bd5098..bd3b57cc 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -18,7 +18,7 @@ Definition hash_key (k : usize) : result usize :=
   Ok k.
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 61:4-67:5 *)
+    Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *)
 Fixpoint hashMap_allocate_slots_loop
   (T : Type) (n : nat) (slots : alloc_vec_Vec (AList_t T)) (n1 : usize) :
   result (alloc_vec_Vec (AList_t T))
@@ -36,7 +36,7 @@ Fixpoint hashMap_allocate_slots_loop
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
-    Source: 'tests/src/hashmap.rs', lines 61:4-61:78 *)
+    Source: 'tests/src/hashmap.rs', lines 63:4-63:78 *)
 Definition hashMap_allocate_slots
   (T : Type) (n : nat) (slots : alloc_vec_Vec (AList_t T)) (n1 : usize) :
   result (alloc_vec_Vec (AList_t T))
@@ -45,7 +45,7 @@ Definition hashMap_allocate_slots
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::new_with_capacity]:
-    Source: 'tests/src/hashmap.rs', lines 70:4-74:13 *)
+    Source: 'tests/src/hashmap.rs', lines 72:4-76:13 *)
 Definition hashMap_new_with_capacity
   (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
   (max_load_divisor : usize) :
@@ -59,18 +59,19 @@ Definition hashMap_new_with_capacity
       hashMap_num_entries := 0%usize;
       hashMap_max_load_factor := (max_load_dividend, max_load_divisor);
       hashMap_max_load := i1;
+      hashMap_saturated := false;
       hashMap_slots := slots
     |}
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::new]:
-    Source: 'tests/src/hashmap.rs', lines 86:4-86:24 *)
+    Source: 'tests/src/hashmap.rs', lines 89:4-89:24 *)
 Definition hashMap_new (T : Type) (n : nat) : result (HashMap_t T) :=
   hashMap_new_with_capacity T n 32%usize 4%usize 5%usize
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 94:8-99:5 *)
+    Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *)
 Fixpoint hashMap_clear_loop
   (T : Type) (n : nat) (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
   result (alloc_vec_Vec (AList_t T))
@@ -93,7 +94,7 @@ Fixpoint hashMap_clear_loop
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]:
-    Source: 'tests/src/hashmap.rs', lines 91:4-91:27 *)
+    Source: 'tests/src/hashmap.rs', lines 94:4-94:27 *)
 Definition hashMap_clear
   (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) :=
   hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
@@ -102,18 +103,19 @@ Definition hashMap_clear
       hashMap_num_entries := 0%usize;
       hashMap_max_load_factor := self.(hashMap_max_load_factor);
       hashMap_max_load := self.(hashMap_max_load);
+      hashMap_saturated := self.(hashMap_saturated);
       hashMap_slots := hm
     |}
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::len]:
-    Source: 'tests/src/hashmap.rs', lines 101:4-101:30 *)
+    Source: 'tests/src/hashmap.rs', lines 104:4-104:30 *)
 Definition hashMap_len (T : Type) (self : HashMap_t T) : result usize :=
   Ok self.(hashMap_num_entries)
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 108:4-125:5 *)
+    Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *)
 Fixpoint hashMap_insert_in_list_loop
   (T : Type) (n : nat) (key : usize) (value : T) (ls : AList_t T) :
   result (bool * (AList_t T))
@@ -135,7 +137,7 @@ Fixpoint hashMap_insert_in_list_loop
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
-    Source: 'tests/src/hashmap.rs', lines 108:4-108:72 *)
+    Source: 'tests/src/hashmap.rs', lines 111:4-111:72 *)
 Definition hashMap_insert_in_list
   (T : Type) (n : nat) (key : usize) (value : T) (ls : AList_t T) :
   result (bool * (AList_t T))
@@ -144,7 +146,7 @@ Definition hashMap_insert_in_list
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_no_resize]:
-    Source: 'tests/src/hashmap.rs', lines 128:4-128:54 *)
+    Source: 'tests/src/hashmap.rs', lines 131:4-131:54 *)
 Definition hashMap_insert_no_resize
   (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) :
   result (HashMap_t T)
@@ -168,6 +170,7 @@ Definition hashMap_insert_no_resize
         hashMap_num_entries := i1;
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
         hashMap_max_load := self.(hashMap_max_load);
+        hashMap_saturated := self.(hashMap_saturated);
         hashMap_slots := v
       |})
   else (
@@ -177,6 +180,7 @@ Definition hashMap_insert_no_resize
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
         hashMap_max_load := self.(hashMap_max_load);
+        hashMap_saturated := self.(hashMap_saturated);
         hashMap_slots := v
       |})
 .
@@ -209,7 +213,7 @@ Definition hashMap_move_elements_from_list
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 182:4-191:5 *)
+    Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *)
 Fixpoint hashMap_move_elements_loop
   (T : Type) (n : nat) (ntable : HashMap_t T)
   (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
@@ -235,35 +239,35 @@ Fixpoint hashMap_move_elements_loop
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]:
-    Source: 'tests/src/hashmap.rs', lines 182:4-182:96 *)
+    Source: 'tests/src/hashmap.rs', lines 181:4-181:82 *)
 Definition hashMap_move_elements
   (T : Type) (n : nat) (ntable : HashMap_t T)
-  (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
+  (slots : alloc_vec_Vec (AList_t T)) :
   result ((HashMap_t T) * (alloc_vec_Vec (AList_t T)))
   :=
-  hashMap_move_elements_loop T n ntable slots i
+  hashMap_move_elements_loop T n ntable slots 0%usize
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::try_resize]:
-    Source: 'tests/src/hashmap.rs', lines 151:4-151:28 *)
+    Source: 'tests/src/hashmap.rs', lines 154:4-154:28 *)
 Definition hashMap_try_resize
   (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) :=
-  max_usize <- scalar_cast U32 Usize core_u32_max;
   let capacity := alloc_vec_Vec_len (AList_t T) self.(hashMap_slots) in
-  n1 <- usize_div max_usize 2%usize;
+  n1 <- usize_div core_usize_max 2%usize;
   let (i, i1) := self.(hashMap_max_load_factor) in
   i2 <- usize_div n1 i;
   if capacity s<= i2
   then (
     i3 <- usize_mul capacity 2%usize;
     ntable <- hashMap_new_with_capacity T n i3 i i1;
-    p <- hashMap_move_elements T n ntable self.(hashMap_slots) 0%usize;
+    p <- hashMap_move_elements T n ntable self.(hashMap_slots);
     let (ntable1, _) := p in
     Ok
       {|
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := (i, i1);
         hashMap_max_load := ntable1.(hashMap_max_load);
+        hashMap_saturated := self.(hashMap_saturated);
         hashMap_slots := ntable1.(hashMap_slots)
       |})
   else
@@ -272,12 +276,13 @@ Definition hashMap_try_resize
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := (i, i1);
         hashMap_max_load := self.(hashMap_max_load);
+        hashMap_saturated := true;
         hashMap_slots := self.(hashMap_slots)
       |}
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::insert]:
-    Source: 'tests/src/hashmap.rs', lines 140:4-140:48 *)
+    Source: 'tests/src/hashmap.rs', lines 143:4-143:48 *)
 Definition hashMap_insert
   (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) :
   result (HashMap_t T)
@@ -285,7 +290,26 @@ Definition hashMap_insert
   self1 <- hashMap_insert_no_resize T n self key value;
   i <- hashMap_len T self1;
   if i s> self1.(hashMap_max_load)
-  then hashMap_try_resize T n self1
+  then
+    if self1.(hashMap_saturated)
+    then
+      Ok
+        {|
+          hashMap_num_entries := self1.(hashMap_num_entries);
+          hashMap_max_load_factor := self1.(hashMap_max_load_factor);
+          hashMap_max_load := self1.(hashMap_max_load);
+          hashMap_saturated := true;
+          hashMap_slots := self1.(hashMap_slots)
+        |}
+    else
+      hashMap_try_resize T n
+        {|
+          hashMap_num_entries := self1.(hashMap_num_entries);
+          hashMap_max_load_factor := self1.(hashMap_max_load_factor);
+          hashMap_max_load := self1.(hashMap_max_load);
+          hashMap_saturated := false;
+          hashMap_slots := self1.(hashMap_slots)
+        |}
   else Ok self1
 .
 
@@ -423,6 +447,7 @@ Definition hashMap_get_mut
           hashMap_num_entries := self.(hashMap_num_entries);
           hashMap_max_load_factor := self.(hashMap_max_load_factor);
           hashMap_max_load := self.(hashMap_max_load);
+          hashMap_saturated := self.(hashMap_saturated);
           hashMap_slots := v
         |} in
   Ok (t, back)
@@ -489,6 +514,7 @@ Definition hashMap_remove
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
         hashMap_max_load := self.(hashMap_max_load);
+        hashMap_saturated := self.(hashMap_saturated);
         hashMap_slots := v
       |})
   | Some x1 =>
@@ -499,6 +525,7 @@ Definition hashMap_remove
         hashMap_num_entries := i1;
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
         hashMap_max_load := self.(hashMap_max_load);
+        hashMap_saturated := self.(hashMap_saturated);
         hashMap_slots := v
       |})
   end
diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v
index 070d6dfb..bd582254 100644
--- a/tests/coq/hashmap/Hashmap_Types.v
+++ b/tests/coq/hashmap/Hashmap_Types.v
@@ -27,6 +27,7 @@ mkHashMap_t {
   hashMap_num_entries : usize;
   hashMap_max_load_factor : (usize * usize);
   hashMap_max_load : usize;
+  hashMap_saturated : bool;
   hashMap_slots : alloc_vec_Vec (AList_t T);
 }
 .
@@ -35,6 +36,7 @@ Arguments mkHashMap_t { _ }.
 Arguments hashMap_num_entries { _ }.
 Arguments hashMap_max_load_factor { _ }.
 Arguments hashMap_max_load { _ }.
+Arguments hashMap_saturated { _ }.
 Arguments hashMap_slots { _ }.
 
 End Hashmap_Types.
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index d6ba503e..21789c69 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -7,21 +7,21 @@ open Hashmap.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 61:4-67:5 *)
+    Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *)
 unfold
 let hashMap_allocate_slots_loop_decreases (t : Type0)
   (slots : alloc_vec_Vec (aList_t t)) (n : usize) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 94:8-99:5 *)
+    Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *)
 unfold
 let hashMap_clear_loop_decreases (t : Type0)
   (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 108:4-125:5 *)
+    Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *)
 unfold
 let hashMap_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t)
   (ls : aList_t t) : nat =
@@ -35,7 +35,7 @@ let hashMap_move_elements_from_list_loop_decreases (t : Type0)
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 182:4-191:5 *)
+    Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *)
 unfold
 let hashMap_move_elements_loop_decreases (t : Type0) (ntable : hashMap_t t)
   (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat =
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 40362176..223bde57 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -14,7 +14,7 @@ let hash_key (k : usize) : result usize =
   Ok k
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 61:4-67:5 *)
+    Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *)
 let rec hashMap_allocate_slots_loop
   (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) :
   Tot (result (alloc_vec_Vec (aList_t t)))
@@ -28,7 +28,7 @@ let rec hashMap_allocate_slots_loop
   else Ok slots
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
-    Source: 'tests/src/hashmap.rs', lines 61:4-61:78 *)
+    Source: 'tests/src/hashmap.rs', lines 63:4-63:78 *)
 let hashMap_allocate_slots
   (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) :
   result (alloc_vec_Vec (aList_t t))
@@ -36,7 +36,7 @@ let hashMap_allocate_slots
   hashMap_allocate_slots_loop t slots n
 
 (** [hashmap::{hashmap::HashMap<T>}::new_with_capacity]:
-    Source: 'tests/src/hashmap.rs', lines 70:4-74:13 *)
+    Source: 'tests/src/hashmap.rs', lines 72:4-76:13 *)
 let hashMap_new_with_capacity
   (t : Type0) (capacity : usize) (max_load_dividend : usize)
   (max_load_divisor : usize) :
@@ -51,16 +51,17 @@ let hashMap_new_with_capacity
       num_entries = 0;
       max_load_factor = (max_load_dividend, max_load_divisor);
       max_load = i1;
+      saturated = false;
       slots = slots
     }
 
 (** [hashmap::{hashmap::HashMap<T>}::new]:
-    Source: 'tests/src/hashmap.rs', lines 86:4-86:24 *)
+    Source: 'tests/src/hashmap.rs', lines 89:4-89:24 *)
 let hashMap_new (t : Type0) : result (hashMap_t t) =
   hashMap_new_with_capacity t 32 4 5
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 94:8-99:5 *)
+    Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *)
 let rec hashMap_clear_loop
   (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (i : usize) :
   Tot (result (alloc_vec_Vec (aList_t t)))
@@ -78,18 +79,18 @@ let rec hashMap_clear_loop
   else Ok slots
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]:
-    Source: 'tests/src/hashmap.rs', lines 91:4-91:27 *)
+    Source: 'tests/src/hashmap.rs', lines 94:4-94:27 *)
 let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) =
   let* hm = hashMap_clear_loop t self.slots 0 in
   Ok { self with num_entries = 0; slots = hm }
 
 (** [hashmap::{hashmap::HashMap<T>}::len]:
-    Source: 'tests/src/hashmap.rs', lines 101:4-101:30 *)
+    Source: 'tests/src/hashmap.rs', lines 104:4-104:30 *)
 let hashMap_len (t : Type0) (self : hashMap_t t) : result usize =
   Ok self.num_entries
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 108:4-125:5 *)
+    Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *)
 let rec hashMap_insert_in_list_loop
   (t : Type0) (key : usize) (value : t) (ls : aList_t t) :
   Tot (result (bool & (aList_t t)))
@@ -106,7 +107,7 @@ let rec hashMap_insert_in_list_loop
   end
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
-    Source: 'tests/src/hashmap.rs', lines 108:4-108:72 *)
+    Source: 'tests/src/hashmap.rs', lines 111:4-111:72 *)
 let hashMap_insert_in_list
   (t : Type0) (key : usize) (value : t) (ls : aList_t t) :
   result (bool & (aList_t t))
@@ -114,7 +115,7 @@ let hashMap_insert_in_list
   hashMap_insert_in_list_loop t key value ls
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_no_resize]:
-    Source: 'tests/src/hashmap.rs', lines 128:4-128:54 *)
+    Source: 'tests/src/hashmap.rs', lines 131:4-131:54 *)
 let hashMap_insert_no_resize
   (t : Type0) (self : hashMap_t t) (key : usize) (value : t) :
   result (hashMap_t t)
@@ -155,7 +156,7 @@ let hashMap_move_elements_from_list
   hashMap_move_elements_from_list_loop t ntable ls
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 182:4-191:5 *)
+    Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *)
 let rec hashMap_move_elements_loop
   (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t))
   (i : usize) :
@@ -176,43 +177,51 @@ let rec hashMap_move_elements_loop
   else Ok (ntable, slots)
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]:
-    Source: 'tests/src/hashmap.rs', lines 182:4-182:96 *)
+    Source: 'tests/src/hashmap.rs', lines 181:4-181:82 *)
 let hashMap_move_elements
-  (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t))
-  (i : usize) :
+  (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t)) :
   result ((hashMap_t t) & (alloc_vec_Vec (aList_t t)))
   =
-  hashMap_move_elements_loop t ntable slots i
+  hashMap_move_elements_loop t ntable slots 0
 
 (** [hashmap::{hashmap::HashMap<T>}::try_resize]:
-    Source: 'tests/src/hashmap.rs', lines 151:4-151:28 *)
+    Source: 'tests/src/hashmap.rs', lines 154:4-154:28 *)
 let hashMap_try_resize
   (t : Type0) (self : hashMap_t t) : result (hashMap_t t) =
-  let* max_usize = scalar_cast U32 Usize core_u32_max in
   let capacity = alloc_vec_Vec_len (aList_t t) self.slots in
-  let* n1 = usize_div max_usize 2 in
+  let* n1 = usize_div core_usize_max 2 in
   let (i, i1) = self.max_load_factor in
   let* i2 = usize_div n1 i in
   if capacity <= i2
   then
     let* i3 = usize_mul capacity 2 in
     let* ntable = hashMap_new_with_capacity t i3 i i1 in
-    let* p = hashMap_move_elements t ntable self.slots 0 in
+    let* p = hashMap_move_elements t ntable self.slots in
     let (ntable1, _) = p in
     Ok
-      { ntable1 with num_entries = self.num_entries; max_load_factor = (i, i1)
+      {
+        self
+          with
+          max_load_factor = (i, i1);
+          max_load = ntable1.max_load;
+          slots = ntable1.slots
       }
-  else Ok { self with max_load_factor = (i, i1) }
+  else Ok { self with max_load_factor = (i, i1); saturated = true }
 
 (** [hashmap::{hashmap::HashMap<T>}::insert]:
-    Source: 'tests/src/hashmap.rs', lines 140:4-140:48 *)
+    Source: 'tests/src/hashmap.rs', lines 143:4-143:48 *)
 let hashMap_insert
   (t : Type0) (self : hashMap_t t) (key : usize) (value : t) :
   result (hashMap_t t)
   =
   let* self1 = hashMap_insert_no_resize t self key value in
   let* i = hashMap_len t self1 in
-  if i > self1.max_load then hashMap_try_resize t self1 else Ok self1
+  if i > self1.max_load
+  then
+    if self1.saturated
+    then Ok { self1 with saturated = true }
+    else hashMap_try_resize t { self1 with saturated = false }
+  else Ok self1
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
     Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *)
diff --git a/tests/fstar/hashmap/Hashmap.Types.fst b/tests/fstar/hashmap/Hashmap.Types.fst
index a10bd16c..accc5e21 100644
--- a/tests/fstar/hashmap/Hashmap.Types.fst
+++ b/tests/fstar/hashmap/Hashmap.Types.fst
@@ -19,6 +19,7 @@ type hashMap_t (t : Type0) =
   num_entries : usize;
   max_load_factor : (usize & usize);
   max_load : usize;
+  saturated : bool;
   slots : alloc_vec_Vec (aList_t t);
 }
 
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 76ec5041..f01f1c4f 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -16,7 +16,7 @@ def hash_key (k : Usize) : Result Usize :=
   Result.ok k
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 61:4-67:5 -/
+   Source: 'tests/src/hashmap.rs', lines 63:4-69:5 -/
 divergent def HashMap.allocate_slots_loop
   (T : Type) (slots : alloc.vec.Vec (AList T)) (n : Usize) :
   Result (alloc.vec.Vec (AList T))
@@ -30,7 +30,7 @@ divergent def HashMap.allocate_slots_loop
   else Result.ok slots
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
-   Source: 'tests/src/hashmap.rs', lines 61:4-61:78 -/
+   Source: 'tests/src/hashmap.rs', lines 63:4-63:78 -/
 @[reducible]
 def HashMap.allocate_slots
   (T : Type) (slots : alloc.vec.Vec (AList T)) (n : Usize) :
@@ -39,7 +39,7 @@ def HashMap.allocate_slots
   HashMap.allocate_slots_loop T slots n
 
 /- [hashmap::{hashmap::HashMap<T>}::new_with_capacity]:
-   Source: 'tests/src/hashmap.rs', lines 70:4-74:13 -/
+   Source: 'tests/src/hashmap.rs', lines 72:4-76:13 -/
 def HashMap.new_with_capacity
   (T : Type) (capacity : Usize) (max_load_dividend : Usize)
   (max_load_divisor : Usize) :
@@ -54,16 +54,17 @@ def HashMap.new_with_capacity
       num_entries := 0#usize,
       max_load_factor := (max_load_dividend, max_load_divisor),
       max_load := i1,
+      saturated := false,
       slots := slots
     }
 
 /- [hashmap::{hashmap::HashMap<T>}::new]:
-   Source: 'tests/src/hashmap.rs', lines 86:4-86:24 -/
+   Source: 'tests/src/hashmap.rs', lines 89:4-89:24 -/
 def HashMap.new (T : Type) : Result (HashMap T) :=
   HashMap.new_with_capacity T 32#usize 4#usize 5#usize
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 94:8-99:5 -/
+   Source: 'tests/src/hashmap.rs', lines 97:8-102:5 -/
 divergent def HashMap.clear_loop
   (T : Type) (slots : alloc.vec.Vec (AList T)) (i : Usize) :
   Result (alloc.vec.Vec (AList T))
@@ -81,19 +82,19 @@ divergent def HashMap.clear_loop
   else Result.ok slots
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]:
-   Source: 'tests/src/hashmap.rs', lines 91:4-91:27 -/
+   Source: 'tests/src/hashmap.rs', lines 94:4-94:27 -/
 def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
   let hm ← HashMap.clear_loop T self.slots 0#usize
   Result.ok { self with num_entries := 0#usize, slots := hm }
 
 /- [hashmap::{hashmap::HashMap<T>}::len]:
-   Source: 'tests/src/hashmap.rs', lines 101:4-101:30 -/
+   Source: 'tests/src/hashmap.rs', lines 104:4-104:30 -/
 def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
   Result.ok self.num_entries
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 108:4-125:5 -/
+   Source: 'tests/src/hashmap.rs', lines 111:4-128:5 -/
 divergent def HashMap.insert_in_list_loop
   (T : Type) (key : Usize) (value : T) (ls : AList T) :
   Result (Bool × (AList T))
@@ -109,7 +110,7 @@ divergent def HashMap.insert_in_list_loop
   | AList.Nil => Result.ok (true, AList.Cons key value AList.Nil)
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 108:4-108:72 -/
+   Source: 'tests/src/hashmap.rs', lines 111:4-111:72 -/
 @[reducible]
 def HashMap.insert_in_list
   (T : Type) (key : Usize) (value : T) (ls : AList T) :
@@ -118,7 +119,7 @@ def HashMap.insert_in_list
   HashMap.insert_in_list_loop T key value ls
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_no_resize]:
-   Source: 'tests/src/hashmap.rs', lines 128:4-128:54 -/
+   Source: 'tests/src/hashmap.rs', lines 131:4-131:54 -/
 def HashMap.insert_no_resize
   (T : Type) (self : HashMap T) (key : Usize) (value : T) :
   Result (HashMap T)
@@ -161,7 +162,7 @@ def HashMap.move_elements_from_list
   HashMap.move_elements_from_list_loop T ntable ls
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 182:4-191:5 -/
+   Source: 'tests/src/hashmap.rs', lines 182:8-191:5 -/
 divergent def HashMap.move_elements_loop
   (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Usize)
   :
@@ -182,22 +183,19 @@ divergent def HashMap.move_elements_loop
   else Result.ok (ntable, slots)
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]:
-   Source: 'tests/src/hashmap.rs', lines 182:4-182:96 -/
-@[reducible]
+   Source: 'tests/src/hashmap.rs', lines 181:4-181:82 -/
 def HashMap.move_elements
-  (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Usize)
-  :
+  (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) :
   Result ((HashMap T) × (alloc.vec.Vec (AList T)))
   :=
-  HashMap.move_elements_loop T ntable slots i
+  HashMap.move_elements_loop T ntable slots 0#usize
 
 /- [hashmap::{hashmap::HashMap<T>}::try_resize]:
-   Source: 'tests/src/hashmap.rs', lines 151:4-151:28 -/
+   Source: 'tests/src/hashmap.rs', lines 154:4-154:28 -/
 def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
-  let max_usize ← Scalar.cast .Usize core_u32_max
   let capacity := alloc.vec.Vec.len (AList T) self.slots
-  let n1 ← max_usize / 2#usize
+  let n1 ← core_usize_max / 2#usize
   let (i, i1) := self.max_load_factor
   let i2 ← n1 / i
   if capacity <= i2
@@ -205,18 +203,20 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
     do
     let i3 ← capacity * 2#usize
     let ntable ← HashMap.new_with_capacity T i3 i i1
-    let p ← HashMap.move_elements T ntable self.slots 0#usize
+    let p ← HashMap.move_elements T ntable self.slots
     let (ntable1, _) := p
     Result.ok
       {
-        ntable1
+        self
           with
-          num_entries := self.num_entries, max_load_factor := (i, i1)
+          max_load_factor := (i, i1),
+          max_load := ntable1.max_load,
+          slots := ntable1.slots
       }
-  else Result.ok { self with max_load_factor := (i, i1) }
+  else Result.ok { self with max_load_factor := (i, i1), saturated := true }
 
 /- [hashmap::{hashmap::HashMap<T>}::insert]:
-   Source: 'tests/src/hashmap.rs', lines 140:4-140:48 -/
+   Source: 'tests/src/hashmap.rs', lines 143:4-143:48 -/
 def HashMap.insert
   (T : Type) (self : HashMap T) (key : Usize) (value : T) :
   Result (HashMap T)
@@ -225,7 +225,10 @@ def HashMap.insert
   let self1 ← HashMap.insert_no_resize T self key value
   let i ← HashMap.len T self1
   if i > self1.max_load
-  then HashMap.try_resize T self1
+  then
+    if self1.saturated
+    then Result.ok { self1 with saturated := true }
+    else HashMap.try_resize T { self1 with saturated := false }
   else Result.ok self1
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 29b5834b..246041f4 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -67,13 +67,31 @@ theorem hash_mod_key_eq : hash_mod_key k l = k.val % l := by
 def slot_s_inv_hash (l i : Int) (ls : List (Usize × α)) : Prop :=
   ls.allP (λ (k, _) => hash_mod_key k l = i)
 
-@[simp]
 def slot_s_inv (l i : Int) (ls : List (Usize × α)) : Prop :=
   distinct_keys ls ∧
   slot_s_inv_hash l i ls
 
 def slot_t_inv (l i : Int) (s : AList α) : Prop := slot_s_inv l i s.v
 
+@[simp] theorem distinct_keys_nil : @distinct_keys α [] := by simp [distinct_keys]
+@[simp] theorem slot_s_inv_hash_nil : @slot_s_inv_hash l i α [] := by simp [slot_s_inv_hash]
+@[simp] theorem slot_s_inv_nil : @slot_s_inv α l i [] := by simp [slot_s_inv]
+@[simp] theorem slot_t_inv_nil : @slot_t_inv α l i .Nil := by simp [slot_t_inv]
+
+@[simp] theorem distinct_keys_cons (kv : Usize × α) (tl : List (Usize × α)) :
+  distinct_keys (kv :: tl) ↔ ((tl.allP fun (k', _) => ¬↑kv.1 = ↑k') ∧ distinct_keys tl) := by simp [distinct_keys]
+
+@[simp] theorem slot_s_inv_hash_cons (kv : Usize × α) (tl : List (Usize × α)) :
+  slot_s_inv_hash l i (kv :: tl) ↔
+    (hash_mod_key kv.1 l = i ∧ tl.allP (λ (k, _) => hash_mod_key k l = i) ∧ slot_s_inv_hash l i tl) :=
+  by simp [slot_s_inv_hash]
+
+@[simp] theorem slot_s_inv_cons (kv : Usize × α) (tl : List (Usize × α)) :
+  slot_s_inv l i (kv :: tl) ↔
+    ((tl.allP fun (k', _) => ¬↑kv.1 = ↑k') ∧ distinct_keys tl ∧
+     hash_mod_key kv.1 l = i ∧ tl.allP (λ (k, _) => hash_mod_key k l = i) ∧ slot_s_inv l i tl) := by
+    simp [slot_s_inv]; tauto
+
 -- Interpret the hashmap as a list of lists
 def v (hm : HashMap α) : List (List (Usize × α)) :=
   hm.slots.val.map AList.v
@@ -94,26 +112,175 @@ def slots_t_inv (s : alloc.vec.Vec (AList α)) : Prop :=
   slots_s_inv s.v
 
 @[simp]
-def base_inv (hm : HashMap α) : Prop :=
+def slots_s_lookup (s : List (AList α)) (k : Usize) : Option α :=
+  let i := hash_mod_key k s.len
+  let slot := s.index i
+  slot.lookup k
+
+abbrev Slots α := alloc.vec.Vec (AList α)
+
+abbrev Slots.lookup (s : Slots α) (k : Usize) := slots_s_lookup s.val k
+
+abbrev Slots.al_v (s : Slots α) := (s.val.map AList.v).flatten
+
+def lookup (hm : HashMap α) (k : Usize) : Option α :=
+  slots_s_lookup hm.slots.val k
+
+@[simp]
+abbrev len_s (hm : HashMap α) : Int := hm.al_v.len
+
+instance : Membership Usize (HashMap α) where
+  mem k hm := hm.lookup k ≠ none
+
+/- Activate the ↑ notation -/
+attribute [coe] HashMap.v
+
+abbrev inv_load (hm : HashMap α) : Prop :=
+  let capacity := hm.slots.val.len
+  -- TODO: let (dividend, divisor) := hm.max_load_factor introduces field notation .2, etc.
+  let dividend := hm.max_load_factor.1
+  let divisor := hm.max_load_factor.2
+  0 < dividend.val ∧ dividend < divisor ∧
+  capacity * dividend >= divisor ∧
+  hm.max_load = (capacity * dividend) / divisor
+
+@[simp]
+def inv_base (hm : HashMap α) : Prop :=
   -- [num_entries] correctly tracks the number of entries
   hm.num_entries.val = hm.al_v.len ∧
   -- Slots invariant
   slots_t_inv hm.slots ∧
   -- The capacity must be > 0 (otherwise we can't resize)
-  0 < hm.slots.length
-  -- TODO: load computation
+  0 < hm.slots.length ∧ -- TODO: normalization lemmas for comparison
+  -- Load computation
+  inv_load hm
 
 def inv (hm : HashMap α) : Prop :=
   -- Base invariant
-  base_inv hm
+  inv_base hm
   -- TODO: either the hashmap is not overloaded, or we can't resize it
 
+def frame_load (hm nhm : HashMap α) : Prop :=
+  nhm.max_load_factor = hm.max_load_factor ∧
+  nhm.max_load = hm.max_load ∧
+  nhm.saturated = hm.saturated
+
 -- This rewriting lemma is problematic below
 attribute [-simp] Bool.exists_bool
 
 -- The proof below is a bit expensive, so we need to increase the maximum number
 -- of heart beats
 set_option maxHeartbeats 1000000
+open AList
+
+@[pspec]
+theorem allocate_slots_spec {α : Type} (slots : alloc.vec.Vec (AList α)) (n : Usize)
+  (Hslots : ∀ (i : Int), 0 ≤ i → i < slots.len → slots.val.index i = Nil)
+  (Hlen : slots.len + n.val ≤ Usize.max) :
+  ∃ slots1, allocate_slots α slots n = ok slots1 ∧
+  (∀ (i : Int), 0 ≤ i → i < slots1.len → slots1.val.index i = Nil) ∧
+  slots1.len = slots.len + n.val := by
+  rw [allocate_slots]
+  rw [allocate_slots_loop]
+  if h: 0 < n.val then
+    simp [h]
+    -- TODO: progress fails here (maximum recursion depth reached)
+    -- progress as ⟨ slots1 .. ⟩
+    have ⟨ slots1, hEq, _ ⟩ := alloc.vec.Vec.push_spec slots Nil (by scalar_tac)
+    simp [hEq]; clear hEq
+    progress as ⟨ n1 ⟩
+    have Hslots1Nil :
+      ∀ (i : ℤ), 0 ≤ i → i < ↑(alloc.vec.Vec.len (AList α) slots1) → slots1.val.index i = Nil := by
+      intro i h0 h1
+      simp [*]
+      if hi : i < slots.val.len then
+        simp [*]
+      else
+        simp_all
+        have : i - slots.val.len = 0 := by scalar_tac
+        simp [*]
+    have Hslots1Len : alloc.vec.Vec.len (AList α) slots1 + n1.val ≤ Usize.max := by
+      simp_all
+    -- TODO: progress fails here (maximum recursion depth reached)
+    -- This probably comes from the fact that allocate_slots is reducible and applied an infinite number
+    -- of times
+    -- progress as ⟨ slots2 .. ⟩
+    -- TODO: bug here as well
+    stop
+    have ⟨ slots2, hEq, _, _ ⟩ := allocate_slots_spec slots1 n1 (by assumption) (by assumption)
+    stop
+    rw [allocate_slots] at hEq; rw [hEq]; clear hEq
+    simp
+    constructor
+    . intro i h0 h1
+      simp_all
+    . simp_all
+  else
+    simp [h]
+    simp_all
+    scalar_tac
+
+theorem forall_nil_imp_flatten_len_zero (slots : List (List α))
+  (Hnil : ∀ i, 0 ≤ i → i < slots.len → slots.index i = []) :
+  slots.flatten = [] := by
+  induction slots <;> simp_all
+  have Hhead := Hnil 0 (by simp) (by scalar_tac)
+  simp_all; clear Hhead
+  rename _ → _ => Hind
+  apply Hind
+  intros i h0 h1
+  have := Hnil (i + 1) (by scalar_tac) (by scalar_tac)
+  have : 0 < i + 1 := by scalar_tac
+  simp_all
+
+@[pspec]
+theorem new_with_capacity_spec
+  (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize)
+  (Hcapa : 0 < capacity.val)
+  (Hfactor : 0 < max_load_dividend.val ∧ max_load_dividend.val < max_load_divisor.val ∧
+             capacity.val * max_load_dividend.val ≤ Usize.max ∧
+             capacity.val * max_load_dividend.val ≥ max_load_divisor)
+  (Hdivid : 0 < max_load_divisor.val) :
+  ∃ hm, new_with_capacity α capacity max_load_dividend max_load_divisor = ok hm ∧
+  hm.inv ∧ hm.len_s = 0 ∧ ∀ k, hm.lookup k = none := by
+  rw [new_with_capacity]
+  progress as ⟨ slots, Hnil .. ⟩
+  . intros; simp [alloc.vec.Vec.new] at *; scalar_tac
+  . simp [alloc.vec.Vec.new]; scalar_tac
+  . progress as ⟨ i1 .. ⟩
+    progress as ⟨ i2 .. ⟩
+    simp [inv, inv_load]
+    have : (Slots.al_v slots).len = 0 := by
+      have := forall_nil_imp_flatten_len_zero (slots.val.map AList.v)
+        (by intro i h0 h1; simp_all)
+      simp_all
+    have : 0 < slots.val.len := by simp_all [alloc.vec.Vec.len, alloc.vec.Vec.new]
+    have : slots_t_inv slots := by
+      simp [slots_t_inv, slot_t_inv]
+      intro i h0 h1
+      simp_all
+    split_conjs
+    . simp_all [al_v, Slots.al_v, v]
+    . assumption
+    . scalar_tac
+    . simp_all [alloc.vec.Vec.len, alloc.vec.Vec.new]
+    . simp_all
+    . simp_all [alloc.vec.Vec.len, alloc.vec.Vec.new]
+    . simp_all [alloc.vec.Vec.len, alloc.vec.Vec.new]
+    . simp_all [al_v, Slots.al_v, v]
+    . simp [lookup]
+      intro k
+      have : 0 ≤ k.val % slots.val.len := by apply Int.emod_nonneg; scalar_tac
+      have : k.val % slots.val.len < slots.val.len := by apply Int.emod_lt_of_pos; scalar_tac
+      simp [*]
+
+@[pspec]
+theorem new_spec (α : Type) :
+  ∃ hm, new α = ok hm ∧
+  hm.inv ∧ hm.len_s = 0 ∧ ∀ k, hm.lookup k = none := by
+  rw [new]
+  progress as ⟨ hm ⟩
+  simp_all
 
 theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: AList α)
   (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
@@ -141,21 +308,19 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (
     exists true -- TODO: why do we need to do this?
     simp [insert_in_list]
     rw [insert_in_list_loop]
-    simp (config := {contextual := true})
-      [AList.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel]
+    simp (config := {contextual := true}) [AList.v]
   | Cons k v tl0 =>
      if h: k = key then
        rw [insert_in_list]
        rw [insert_in_list_loop]
        simp [h]
-       exists false; simp -- TODO: why do we need to do this?
+       exists false; simp only [true_and, exists_eq_left', List.lookup', ↓reduceIte, AList.v_cons] -- TODO: why do we need to do this?
        split_conjs
        . intros; simp [*]
-       . simp [AList.v, slot_s_inv_hash] at *
-         simp [*]
-       . simp [*, distinct_keys] at *
-         apply hdk
-       . tauto
+       . simp_all [slot_s_inv_hash]
+       . simp at hinv; tauto
+       . simp_all [slot_s_inv_hash]
+       . simp_all
      else
        rw [insert_in_list]
        rw [insert_in_list_loop]
@@ -199,18 +364,6 @@ theorem insert_in_list_spec {α : Type} (l : Int) (key: Usize) (value: α) (l0:
   exists b
   exists l1
 
-@[simp]
-def slots_t_lookup (s : List (AList α)) (k : Usize) : Option α :=
-  let i := hash_mod_key k s.len
-  let slot := s.index i
-  slot.lookup k
-
-def lookup (hm : HashMap α) (k : Usize) : Option α :=
-  slots_t_lookup hm.slots.val k
-
-@[simp]
-abbrev len_s (hm : HashMap α) : Int := hm.al_v.len
-
 -- Remark: α and β must live in the same universe, otherwise the
 -- bind doesn't work
 theorem if_update_eq
@@ -235,6 +388,7 @@ set_option pp.coercions false -- do not print coercions with ↑ (this doesn't p
 -- of heart beats
 set_option maxHeartbeats 2000000
 
+@[pspec]
 theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
   (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
   ∃ nhm, hm.insert_no_resize α key value = ok nhm  ∧
@@ -271,7 +425,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     simp [slot_t_inv, hhm] at h
     simp [h, hhm, h_leq]
   have hd : distinct_keys l.v := by
-    simp [inv, slots_t_inv, slot_t_inv] at hinv
+    simp [inv, slots_t_inv, slot_t_inv, slot_s_inv] at hinv
     have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
     simp [h, h_leq]
   progress as ⟨ inserted, l0, _, _, _, _, hlen .. ⟩
@@ -300,7 +454,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   -- TODO: update progress to automate that
   -- TODO: later I don't want to inline nhm - we need to control simp: deactivate
   -- zeta reduction? For now I have to do this peculiar manipulation
-  have ⟨ nhm, nhm_eq ⟩ := @mk_opaque (HashMap α) { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v }
+  have ⟨ nhm, nhm_eq ⟩ := @mk_opaque (HashMap α) {
+      num_entries := i0,
+      max_load_factor := hm.max_load_factor,
+      max_load := hm.max_load,
+      saturated := hm.saturated,
+      slots := v }
   exists nhm
   have hupdt : lookup nhm key = some value := by
     simp [lookup, List.lookup] at *
@@ -338,14 +497,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     match hm.lookup key with
     | none => nhm.len_s = hm.len_s + 1
     | some _ => nhm.len_s = hm.len_s := by
-    simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at *
+    simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_s_lookup] at *
     -- We have to do a case disjunction
-    simp_all
-    simp [List.update_map_eq]
+    simp_all [List.map_update_eq]
     -- TODO: dependent rewrites
     have _ : key.val % hm.slots.val.len < (List.map AList.v hm.slots.val).len := by
       simp [*]
-    simp [List.len_flatten_update_eq, *]
     split <;>
     rename_i heq <;>
     simp [heq] at hlen <;>
@@ -366,21 +523,734 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     . simp [slots_t_inv, slot_t_inv] at *
       intro i hipos _
       have _ := hinv.right.left i hipos (by simp_all)
-      simp [hhm, h_veq, nhm_eq] at * -- TODO: annoying, we do that because simp_all fails below
       -- We need a case disjunction
-      if h_ieq : i = key.val % List.len hm.slots.val then
-        -- TODO: simp_all fails: "(deterministic) timeout at 'whnf'"
-        -- Also, it is annoying to do this kind
-        -- of rewritings by hand. We could have a different simp
-        -- which safely substitutes variables when we have an
-        -- equality `x = ...` and `x` doesn't appear in the rhs
-        simp [h_ieq] at *
-        simp [*]
-      else
-        simp [*]
+      cases h_ieq : i == key.val % List.len hm.slots.val <;> simp_all [slot_s_inv]
     . simp [hinv, h_veq, nhm_eq]
+    . simp_all [frame_load, inv_base, inv_load]
   simp_all
 
+theorem slot_allP_not_key_lookup (slot : AList T) (h : slot.v.allP fun (k', _) => ¬k = k') :
+  slot.lookup k = none := by
+  induction slot <;> simp_all
+
+@[pspec]
+theorem move_elements_from_list_spec
+  {T : Type} (ntable : HashMap T) (slot : AList T)
+  (hinv : ntable.inv)
+  {l i : Int} (hSlotInv : slot_t_inv l i slot)
+  (hDisjoint1 : ∀ key v, ntable.lookup key = some v → slot.lookup key = none)
+  (hDisjoint2 : ∀ key v, slot.lookup key = some v → ntable.lookup key = none)
+  (hLen : ntable.al_v.len + slot.v.len ≤ Usize.max)
+  :
+  ∃ ntable1, ntable.move_elements_from_list T slot = ok ntable1 ∧
+  ntable1.inv ∧
+  (∀ key v, ntable1.lookup key = some v → ntable.lookup key = some v ∨ slot.lookup key = some v) ∧
+  (∀ key v, ntable.lookup key = some v → ntable1.lookup key = some v) ∧
+  (∀ key v, slot.lookup key = some v → ntable1.lookup key = some v) ∧
+  ntable1.al_v.len = ntable.al_v.len + slot.v.len
+  := by
+  rw [move_elements_from_list]; rw [move_elements_from_list_loop]
+  cases slot with
+  | Nil =>
+    simp [hinv]
+  | Cons key value slot1 =>
+    simp
+    have hLookupKey : ntable.lookup key = none := by
+      by_contra
+      cases h: ntable.lookup key <;> simp_all
+      have h := hDisjoint1 _ _ h
+      simp_all
+    have : ntable.lookup key = none → ntable.len_s < Usize.max := by simp_all; scalar_tac
+    progress as ⟨ ntable1, _, hLookup11, hLookup12, hLength1 ⟩
+    simp [hLookupKey] at hLength1
+    have hTable1LookupImp : ∀ (key : Usize) (v : T), ntable1.lookup key = some v → slot1.lookup key = none := by
+      intro key' v hLookup
+      if h: key = key' then
+        simp_all [slot_t_inv]
+        apply slot_allP_not_key_lookup
+        simp_all
+      else
+        simp_all
+        cases h: ntable.lookup key' <;> simp_all
+        have := hDisjoint1 _ _ h
+        simp_all
+    have hSlot1LookupImp : ∀ (key : Usize) (v : T), slot1.lookup key = some v → ntable1.lookup key = none := by
+      intro key' v hLookup
+      if h: key' = key then
+        by_contra
+        rename _ => hNtable1NotNone
+        cases h: ntable1.lookup key' <;> simp [h] at hNtable1NotNone
+        have := hTable1LookupImp _ _ h
+        simp_all
+      else
+        have := hLookup12 key' h
+        have := hDisjoint2 key' v
+        simp_all
+    have : ntable1.al_v.len + slot1.v.len ≤ Usize.max := by simp_all; scalar_tac
+    have : slot_t_inv l i slot1 := by
+      simp [slot_t_inv] at hSlotInv
+      simp [slot_t_inv, hSlotInv]
+    -- TODO: progress leads to: slot_t_inv i i slot1
+    -- progress as ⟨ ntable2 ⟩
+
+    have  ⟨ ntable2, hEq, hInv2, hLookup21, hLookup22, hLookup23, hLen1 ⟩ :=
+      move_elements_from_list_spec ntable1 slot1 (by assumption) (by assumption)
+          hTable1LookupImp hSlot1LookupImp (by assumption)
+    simp [hEq]; clear hEq
+    -- The conclusion
+    -- TODO: use aesop here
+    split_conjs
+    . simp [*]
+    . intro key' v hLookup
+      have := hLookup21 key' v
+      if h: key = key' then
+        have := hLookup22 key' v
+        have := hLookup23 key' v
+        have := hDisjoint1 key' v
+        have := hDisjoint2 key' v
+        have := hTable1LookupImp key' v
+        have := hSlot1LookupImp key' v
+        simp_all [Slots.lookup]
+      else have := hLookup12 key'; simp_all
+    . intro key' v hLookup1
+      if h: key' = key then
+        simp_all
+      else
+        have := hLookup12 key' h
+        have := hLookup22 key' v
+        simp_all
+    . intro key' v hLookup1
+      if h: key' = key then
+        have := hLookup22 key' v
+        simp_all
+      else
+        have := hLookup23 key' v
+        simp_all
+    . scalar_tac
+
+theorem slots_forall_nil_imp_lookup_none (slots : Slots T) (hLen : slots.val.len ≠ 0)
+  (hEmpty : ∀ j, 0 ≤ j → j < slots.val.len → slots.val.index j = AList.Nil) :
+  ∀ key, slots.lookup key = none := by
+  intro key
+  simp [Slots.lookup]
+  have : 0 ≤ key.val % slots.val.len := by
+    exact Int.emod_nonneg key.val hLen -- TODO: automate that
+  have : key.val % slots.val.len < slots.val.len := by
+    apply Int.emod_lt_of_pos
+    scalar_tac
+  have := hEmpty (key.val % slots.val.len) (by assumption) (by assumption)
+  simp [*]
+
+theorem slots_index_len_le_flatten_len (slots : List (AList α)) (i : Int) (h : 0 ≤ i ∧ i < slots.len) :
+  (slots.index i).len ≤ (List.map AList.v slots).flatten.len := by
+  match slots with
+  | [] =>
+    simp at *; scalar_tac
+  | slot :: slots' =>
+    simp at *
+    if hi : i = 0 then
+      simp_all; scalar_tac
+    else
+      have := slots_index_len_le_flatten_len slots' (i - 1) (by scalar_tac)
+      simp [*]
+      scalar_tac
+
+/- If we successfully lookup a key from a slot, the hash of the key modulo the number of slots must
+   be equal to the slot index.
+   TODO: remove?
+ -/
+theorem slots_inv_lookup_imp_eq (slots : Slots α) (hInv : slots_t_inv slots)
+  (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) (key : Usize) :
+  (slots.val.index i).lookup key ≠ none → i = key.val % slots.val.len := by
+  suffices hSlot : ∀ (slot : List (Usize × α)),
+           slot_s_inv slots.val.len i slot →
+           slot.lookup' key ≠ none →
+           i = key.val % slots.val.len
+  from by
+    rw [slots_t_inv, slots_s_inv] at hInv
+    replace hInv := hInv i hi.left hi.right
+    simp [slot_t_inv] at hInv
+    exact hSlot _ hInv
+  intro slot
+  induction slot <;> simp_all
+  intros; simp_all
+  split at * <;> simp_all
+
+-- TODO: remove?
+theorem slots_update_lookup_equiv (slots : Slots α) (hInv : slots_t_inv slots)
+  (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) (key : Usize) :
+  let slot := slots.val.index i
+  slot.lookup key ≠ none ∨ slots_s_lookup (slots.val.update i .Nil) key ≠ none ↔
+  slots.lookup key ≠ none := by
+  -- We need the following lemma to derive a contradiction
+  have := slots_inv_lookup_imp_eq slots hInv i hi key
+  cases hi : (key.val % slots.val.len) == i <;>
+  simp_all [Slots.lookup]
+
+/-theorem slots_update_lookup_imp
+  (slots slots1 : Slots α) (slot : AList α) (hInv : slots_t_inv slots) (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len)
+  (hSlotsEq : slots.val = slots.val.update i slot) :
+  ∀ key v, slots1.lookup key = some v → slots.lookup key = some v ∨ slot.lookup key = some v-/
+
+theorem move_slots_updated_table_lookup_imp
+  (ntable ntable1 ntable2 : HashMap α) (slots slots1 : Slots α) (slot : AList α)
+  (hi : 0 ≤ i ∧ i < slots.val.len)
+  (hSlotsInv : slots_t_inv slots)
+  (hSlotEq : slot = slots.val.index i)
+  (hSlotsEq : slots1.val = slots.val.update i .Nil)
+  (hTableLookup : ∀ (key : Usize) (v : α), ntable1.lookup key = some v →
+                    ntable.lookup key = some v ∨ slot.lookup key = some v)
+  (hTable1Lookup : ∀ (key : Usize) (v : α), ntable2.lookup key = some v →
+                    ntable1.lookup key = some v ∨ Slots.lookup slots1 key = some v)
+  :
+  ∀ key v, ntable2.lookup key = some v → ntable.lookup key = some v ∨ slots.lookup key = some v := by
+  intro key v hLookup
+  replace hTableLookup := hTableLookup key v
+  replace hTable1Lookup := hTable1Lookup key v hLookup
+  cases hTable1Lookup with
+  | inl hTable1Lookup =>
+    replace hTableLookup := hTableLookup hTable1Lookup
+    cases hTableLookup <;> try simp [*]
+    right
+    have := slots_inv_lookup_imp_eq slots hSlotsInv i hi key (by simp_all)
+    simp_all [Slots.lookup]
+  | inr hTable1Lookup =>
+    right
+    -- The key can't be for the slot we replaced
+    if heq : key.val % slots.val.len = i then
+      simp_all [Slots.lookup]
+    else
+      simp_all [Slots.lookup]
+
+theorem move_one_slot_lookup_equiv {α : Type} (ntable ntable1 ntable2 : HashMap α)
+  (slot : AList α)
+  (slots slots1 : Slots α)
+  (i : Int) (h1 : i < slots.len)
+  (hSlotEq : slot = slots.val.index i)
+  (hSlots1Eq : slots1.val = slots.val.update i .Nil)
+  (hLookup1 : ∀ (key : Usize) (v : α), ntable.lookup key = some v → ntable1.lookup key = some v)
+  (hLookup2 : ∀ (key : Usize) (v : α), slot.lookup key = some v → ntable1.lookup key = some v)
+  (hLookup3 : ∀ (key : Usize) (v : α), ntable1.lookup key = some v → ntable2.lookup key = some v)
+  (hLookup4 : ∀ (key : Usize) (v : α), slots1.lookup key = some v → ntable2.lookup key = some v) :
+  (∀ key v, slots.lookup key = some v → ntable2.lookup key = some v) ∧
+  (∀ key v, ntable.lookup key = some v → ntable2.lookup key = some v) := by
+  constructor <;> intro key v hLookup
+  . if hi: key.val % slots.val.len = i then
+      -- We lookup in slot
+      have := hLookup2 key v
+      simp_all [Slots.lookup]
+      have := hLookup3 key v
+      simp_all
+    else
+      -- We lookup in slots
+      have := hLookup4 key v
+      simp_all [Slots.lookup]
+  . have := hLookup1 key v
+    have := hLookup3 key v
+    simp_all
+
+theorem slots_lookup_none_imp_slot_lookup_none
+  (slots : Slots α) (hInv : slots_t_inv slots) (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) :
+  ∀ (key : Usize), slots.lookup key = none → (slots.val.index i).lookup key = none := by
+  intro key hLookup
+  if heq : i = key.val % slots.val.len then
+    simp_all [Slots.lookup]
+  else
+    have := slots_inv_lookup_imp_eq slots hInv i (by scalar_tac) key
+    by_contra
+    simp_all
+
+theorem slot_lookup_not_none_imp_slots_lookup_not_none
+  (slots : Slots α) (hInv : slots_t_inv slots) (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) :
+  ∀ (key : Usize), (slots.val.index i).lookup key ≠ none → slots.lookup key ≠ none := by
+  intro key hLookup hNone
+  have := slots_lookup_none_imp_slot_lookup_none slots hInv i hi key hNone
+  apply hLookup this
+
+theorem slots_forall_nil_imp_al_v_nil (slots : Slots α)
+  (hEmpty : ∀ i, 0 ≤ i → i < slots.val.len → slots.val.index i = AList.Nil) :
+  slots.al_v = [] := by
+  suffices h :
+    ∀ (slots : List (AList α)),
+      (∀ (i : ℤ), 0 ≤ i → i < slots.len → slots.index i = Nil) →
+      (slots.map AList.v).flatten = [] from by
+      replace h := h slots.val (by intro i h0 h1; exact hEmpty i h0 h1)
+      simp_all
+  clear slots hEmpty
+  intro slots hEmpty
+  induction slots <;> simp_all
+  have hHead := hEmpty 0 (by simp) (by scalar_tac)
+  simp at hHead
+  simp [hHead]
+  rename (_ → _) => ih
+  apply ih; intro i h0 h1
+  replace hEmpty := hEmpty (i + 1) (by omega) (by omega)
+  -- TODO: simp at hEmpty
+  have : 0 < i + 1 := by omega
+  simp_all
+
+theorem move_elements_loop_spec
+  (n : Nat) -- We need this, otherwise we can't prove termination (the termination_by clauses can be expensive)
+  {α : Type} (ntable : HashMap α) (slots : Slots α)
+  (i : Usize)
+  (hn : n = slots.val.len - i.val) -- Condition for termination
+  (hi : i ≤ alloc.vec.Vec.len (AList α) slots)
+  (hinv : ntable.inv)
+  (hSlotsNonZero : slots.val.len ≠ 0)
+  (hSlotsInv : slots_t_inv slots)
+  (hEmpty : ∀ j, 0 ≤ j → j < i.val → slots.val.index j = AList.Nil)
+  (hDisjoint1 : ∀ key v, ntable.lookup key = some v → slots.lookup key = none)
+  (hDisjoint2 : ∀ key v, slots.lookup key = some v → ntable.lookup key = none)
+  (hLen : ntable.al_v.len + slots.al_v.len ≤ Usize.max)
+  :
+  ∃ ntable1 slots1, ntable.move_elements_loop α slots i = ok (ntable1, slots1) ∧
+  ntable1.inv ∧
+  ntable1.al_v.len = ntable.al_v.len + slots.al_v.len ∧
+  (∀ key v, ntable1.lookup key = some v → ntable.lookup key = some v ∨ slots.lookup key = some v) ∧
+  (∀ key v, slots.lookup key = some v → ntable1.lookup key = some v) ∧
+  (∀ key v, ntable.lookup key = some v → ntable1.lookup key = some v) ∧
+  (∀ (j : Int), 0 ≤ j → j < slots1.len → slots1.val.index j = AList.Nil)
+  := by
+  rw [move_elements_loop]
+  simp
+  if hi: i.val < slots.val.len then
+    -- Proof of termination: eliminate the case: n = 0
+    cases n; scalar_tac
+    rename ℕ => n
+    -- Continue the proof
+    have hIneq : 0 ≤ i.val ∧ i.val < slots.val.len := by scalar_tac
+    simp [hi]
+    progress as ⟨ slot, index_back, hSlotEq, hIndexBack ⟩
+    rw [hIndexBack]; clear hIndexBack
+    have hInvSlot : slot_t_inv slots.val.len i.val slot := by
+      simp [slots_t_inv] at hSlotsInv
+      simp [*]
+    have ntableLookupImpSlot :
+      ∀ (key : Usize) (v : α), ntable.lookup key = some v → slot.lookup key = none := by
+      intro key v hLookup
+      by_contra
+      have : i.val = key.val % slots.val.len := by
+        apply slots_inv_lookup_imp_eq slots hSlotsInv i.val (by scalar_tac)
+        simp_all
+      cases h: slot.lookup key <;> simp_all
+      have := hDisjoint2 _ _ h
+      simp_all
+    have slotLookupImpNtable :
+      ∀ (key : Usize) (v : α), slot.lookup key = some v → ntable.lookup key = none := by
+      intro key v hLookup
+      by_contra
+      cases h : ntable.lookup key <;> simp_all
+      have := ntableLookupImpSlot _ _ h
+      simp_all
+
+    have : ntable.al_v.len + slot.v.len ≤ Usize.max := by
+      have := slots_index_len_le_flatten_len slots.val i.val (by scalar_tac)
+      simp_all [Slots.al_v]; scalar_tac
+    progress as ⟨ ntable1, _, hDisjointNtable1, hLookup11, hLookup12, hLen1 ⟩ -- TODO: decompose post-condition by default
+    progress as ⟨ i' .. ⟩
+    progress as ⟨ slots1, hSlots1Eq .. ⟩
+    have : i' ≤ alloc.vec.Vec.len (AList α) slots1 := by simp_all [alloc.vec.Vec.len]; scalar_tac
+    have : slots_t_inv slots1 := by
+      simp [slots_t_inv] at *
+      intro j h0 h1
+      cases h: j == i.val <;> simp_all
+
+    have ntable1LookupImpSlots1 : ∀ (key : Usize) (v : α), ntable1.lookup key = some v → Slots.lookup slots1 key = none := by
+      intro key v hLookup
+      cases hDisjointNtable1 _ _ hLookup with
+      | inl h =>
+        have := ntableLookupImpSlot _ _ h
+        have := hDisjoint1 _ _ h
+        cases heq : i == key.val % slots.val.len <;> simp_all [Slots.lookup]
+      | inr h =>
+        --have h1 := hLookup12 _ _ h
+        have heq : i = key.val % slots.val.len := by
+          exact slots_inv_lookup_imp_eq slots hSlotsInv i.val hIneq key (by simp_all [Slots.lookup])
+        simp_all [Slots.lookup]
+
+    have : ∀ (key : Usize) (v : α), Slots.lookup slots1 key = some v → ntable1.lookup key = none := by
+      intro key v hLookup
+      by_contra h
+      cases h : ntable1.lookup key <;> simp_all
+      have := ntable1LookupImpSlots1 _ _ h
+      simp_all
+
+    have : ∀ (j : ℤ), OfNat.ofNat 0 ≤ j → j < i'.val → slots1.val.index j = AList.Nil := by
+      intro j h0 h1
+      if h : j = i.val then
+        simp_all
+      else
+        have := hEmpty j h0 (by scalar_tac)
+        simp_all
+
+    have : ntable1.al_v.len + (Slots.al_v slots1).len ≤ Usize.max := by
+      have : i.val < (List.map AList.v slots.val).len := by simp; scalar_tac
+      simp_all [Slots.al_v, List.len_flatten_update_eq, List.map_update_eq]
+
+    have : n = slots1.val.len - i'.val := by simp_all; scalar_tac
+
+    progress as ⟨ ntable2, slots2, _, _, hLookup2Rev, hLookup21, hLookup22, hIndexNil ⟩
+
+    simp [and_assoc]
+    have : ∀ (j : ℤ), OfNat.ofNat 0 ≤ j → j < slots2.val.len → slots2.val.index j = AList.Nil := by
+      intro j h0 h1
+      apply hIndexNil j h0 h1
+    have : ntable2.al_v.len = ntable.al_v.len + slots.al_v.len := by simp_all [Slots.al_v]
+    have : ∀ key v, ntable2.lookup key = some v →
+           ntable.lookup key = some v ∨ slots.lookup key = some v := by
+      intro key v hLookup
+      apply move_slots_updated_table_lookup_imp ntable ntable1 ntable2 slots slots1 slot hIneq <;>
+      try assumption
+    have hLookupPreserve :
+      (∀ key v, slots.lookup key = some v → ntable2.lookup key = some v) ∧
+      (∀ key v, ntable.lookup key = some v → ntable2.lookup key = some v) := by
+      exact move_one_slot_lookup_equiv ntable ntable1 ntable2 slot slots slots1 i.val
+        (by assumption) (by assumption) (by assumption)
+        (by assumption) (by assumption) (by assumption) (by assumption)
+    simp_all [alloc.vec.Vec.len, or_assoc]
+    apply hLookupPreserve
+  else
+    simp [hi, and_assoc, *]
+    simp_all
+    have hi : i = alloc.vec.Vec.len (AList α) slots := by scalar_tac
+    have hEmpty : ∀ j, 0 ≤ j → j < slots.val.len → slots.val.index j = AList.Nil := by
+      simp [hi] at hEmpty
+      exact hEmpty
+    have hNil : slots.al_v = [] := slots_forall_nil_imp_al_v_nil slots hEmpty
+    have hLenNonZero : slots.val.len ≠ 0 := by simp [*]
+    have hLookupEmpty := slots_forall_nil_imp_lookup_none slots hLenNonZero hEmpty
+    simp [hNil, hLookupEmpty]
+    apply hEmpty
+
+@[pspec]
+theorem move_elements_spec
+  {α : Type} (ntable : HashMap α) (slots : Slots α)
+  (hinv : ntable.inv)
+  (hslotsNempty : 0 < slots.val.len)
+  (hSlotsInv : slots_t_inv slots)
+  -- The initial table is empty
+  (hEmpty : ∀ key, ntable.lookup key = none)
+  (hTableLen : ntable.al_v.len = 0)
+  (hSlotsLen : slots.al_v.len ≤ Usize.max)
+  :
+  ∃ ntable1 slots1, ntable.move_elements α slots = ok (ntable1, slots1) ∧
+  ntable1.inv ∧
+  ntable1.al_v.len = ntable.al_v.len + slots.al_v.len ∧
+  (∀ key v, ntable1.lookup key = some v ↔ slots.lookup key = some v)
+  := by
+  rw [move_elements]
+  let n := (slots.val.len - 0).toNat
+  have hn : n = slots.val.len - 0 := by
+    -- TODO: scalar_tac should succeed here
+    scalar_tac_preprocess
+    simp [n] at *
+    norm_cast at *
+    have := @Int.le_toNat n (slots.val.len - OfNat.ofNat 0) (by simp; scalar_tac)
+    simp_all
+  have ⟨ ntable1, slots1, hEq, _, _, ntable1Lookup, slotsLookup, _, _ ⟩ :=
+    move_elements_loop_spec (slots.val.len - 0).toNat ntable slots 0#usize hn (by scalar_tac) hinv
+    (by scalar_tac)
+    hSlotsInv
+    (by intro j h0 h1; scalar_tac)
+    (by simp [*])
+    (by simp [*])
+    (by scalar_tac)
+  simp [hEq]; clear hEq
+  split_conjs <;> try assumption
+  intro key v
+  have := ntable1Lookup key v
+  have := slotsLookup key v
+  constructor <;> simp_all
+
+@[pspec]
+theorem try_resize_spec {α : Type} (hm : HashMap α) (hInv : hm.inv):
+  ∃ hm', hm.try_resize α = ok hm' ∧
+  (∀ key, hm'.lookup key = hm.lookup key) ∧
+  hm'.al_v.len = hm.al_v.len := by
+  rw [try_resize]
+  simp
+  progress as ⟨ n1 ⟩ -- TODO: simplify (Usize.ofInt (OfNat.ofNat 2) try_resize.proof_1).val
+  have : hm.2.1.val ≠ 0 := by
+    simp [inv, inv_load] at hInv
+    -- TODO: why does hm.max_load_factor appears as hm.2??
+    -- Can we deactivate field notations?
+    omega
+  progress as ⟨ n2 ⟩
+  if hSmaller : hm.slots.val.len ≤ n2.val then
+    simp [hSmaller]
+    have : (alloc.vec.Vec.len (AList α) hm.slots).val * 2 ≤ Usize.max := by
+          simp [alloc.vec.Vec.len, inv, inv_load] at *
+          -- TODO: this should be automated
+          have hIneq1 : n1.val ≤ Usize.max / 2 := by simp [*]
+          simp [Int.le_ediv_iff_mul_le] at hIneq1
+          -- TODO: this should be automated
+          have hIneq2 : n2.val ≤ n1.val / hm.2.1.val := by simp [*]
+          rw [Int.le_ediv_iff_mul_le] at hIneq2 <;> try simp [*]
+          have : n2.val * 1 ≤ n2.val * hm.max_load_factor.1.val := by
+            apply Int.mul_le_mul <;> scalar_tac
+          scalar_tac
+    progress as ⟨ newLength ⟩
+    have : 0 < newLength.val := by
+      simp_all [inv, inv_load]
+    progress as ⟨ ntable1 .. ⟩ -- TODO: introduce nice notation to take care of preconditions
+    . -- Pre 1
+      simp_all [inv, inv_load]
+      split_conjs at hInv
+      --
+      apply Int.mul_le_of_le_ediv at hSmaller <;> try simp [*]
+      apply Int.mul_le_of_le_ediv at hSmaller <;> try simp
+      --
+      have : (hm.slots.val.len * hm.2.1.val) * 1 ≤ (hm.slots.val.len * hm.2.1.val) * 2 := by
+        apply Int.mul_le_mul <;> (try simp [*]); scalar_tac
+      --
+      ring_nf at *
+      simp [*]
+      unfold max_load max_load_factor at *
+      omega
+    . -- Pre 2
+      simp_all [inv, inv_load]
+      unfold max_load_factor at * -- TODO: this is really annoying
+      omega
+    . -- End of the proof
+      have : slots_t_inv hm.slots := by simp_all [inv] -- TODO
+      have : (Slots.al_v hm.slots).len ≤ Usize.max := by simp_all [inv, al_v, v, Slots.al_v]; scalar_tac
+      progress as ⟨ ntable2, slots1, _, _, hLookup .. ⟩ -- TODO: assumption is not powerful enough
+      simp_all [lookup, al_v, v, alloc.vec.Vec.len]
+      intro key
+      replace hLookup := hLookup key
+      cases h1: (ntable2.slots.val.index (key.val % ntable2.slots.val.len)).v.lookup' key <;>
+      cases h2: (hm.slots.val.index (key.val % hm.slots.val.len)).v.lookup' key <;>
+      simp_all [Slots.lookup]
+  else
+    simp [hSmaller]
+    tauto
+
+@[pspec]
+theorem insert_spec {α} (hm : HashMap α) (key : Usize) (value : α)
+  (hInv : hm.inv)
+  (hNotSat : hm.lookup key = none → hm.len_s < Usize.max) :
+  ∃ hm1, insert α hm key value = ok hm1 ∧
+  --
+  hm1.lookup key = value ∧
+  (∀ key', key' ≠ key → hm1.lookup key' = hm.lookup key') ∧
+  --
+  match hm.lookup key with
+  | none => hm1.len_s = hm.len_s + 1
+  | some _ => hm1.len_s = hm.len_s
+  := by
+  rw [insert]
+  progress as ⟨ hm1 .. ⟩
+  simp [len]
+  split
+  . split
+    . simp [*]
+      intros; tauto
+    . progress as ⟨ hm2 .. ⟩
+      simp [*]
+      intros; tauto
+  . simp [*]; tauto
+
+@[pspec]
+theorem get_in_list_spec {α} (key : Usize) (slot : AList α) (hLookup : slot.lookup key ≠ none) :
+  ∃ v, get_in_list α key slot = ok v ∧ slot.lookup key = some v := by
+  induction slot <;>
+  rw [get_in_list, get_in_list_loop] <;>
+  simp_all [AList.lookup]
+  split <;> simp_all
+
+@[pspec]
+theorem get_spec {α} (hm : HashMap α) (key : Usize) (hInv : hm.inv) (hLookup : hm.lookup key ≠ none) :
+  ∃ v, get α hm key = ok v ∧ hm.lookup key = some v := by
+  rw [get]
+  simp [hash_key, alloc.vec.Vec.len]
+  have : 0 < hm.slots.val.len := by simp_all [inv]
+  progress as ⟨ hash_mod .. ⟩ -- TODO: decompose post by default
+  simp at *
+  have : 0 ≤ hash_mod.val := by -- TODO: automate
+    simp [*]
+    apply Int.emod_nonneg; simp [inv] at hInv; scalar_tac
+  have : hash_mod < hm.slots.val.len := by -- TODO: automate
+    simp [*]
+    apply Int.emod_lt_of_pos; scalar_tac
+  progress as ⟨ slot ⟩
+  progress as ⟨ v .. ⟩ <;> simp_all [lookup]
+
+@[pspec]
+theorem get_mut_in_list_spec {α} (key : Usize) (slot : AList α)
+  {l i : Int}
+  (hInv : slot_t_inv l i slot)
+  (hLookup : slot.lookup key ≠ none) :
+  ∃ v back, get_mut_in_list α slot key = ok (v, back) ∧
+  slot.lookup key = some v ∧
+  ∀ v', ∃ slot', back v' = ok slot' ∧
+    slot_t_inv l i slot' ∧
+    slot'.lookup key = v' ∧
+    (∀ key', key' ≠ key → slot'.lookup key' = slot.lookup key') ∧
+    -- We need this strong post-condition for the recursive case
+    (∀ key', slot.v.allP (fun x => key' ≠ x.1) → slot'.v.allP (fun x => key' ≠ x.1))
+   := by
+  induction slot <;>
+  rw [get_mut_in_list, get_mut_in_list_loop] <;>
+  simp_all [AList.lookup]
+  split
+  . -- Non-recursive case
+    simp_all [and_assoc, slot_t_inv]
+  . -- Recursive case
+    -- TODO: progress doesn't instantiate l correctly
+    rename _ → _ → _ => ih
+    rename AList α => tl
+    replace ih := ih (by simp_all [slot_t_inv]) (by simp_all)
+    -- progress also fails here
+    -- TODO: progress? notation to have some feedback
+    have ⟨ v, back, hEq, _, hBack ⟩ := ih; clear ih
+    simp [hEq]; clear hEq
+    simp [and_assoc, *]
+    -- Proving the post-condition about back
+    intro v
+    progress as ⟨ slot', _, _, _, hForAll ⟩; clear hBack
+    simp [and_assoc, *]
+    constructor
+    . simp_all [slot_t_inv, slot_s_inv, slot_s_inv_hash]
+    . simp_all
+
+@[pspec]
+theorem get_mut_spec {α} (hm : HashMap α) (key : Usize) (hInv : hm.inv) (hLookup : hm.lookup key ≠ none) :
+  ∃ v back, get_mut α hm key = ok (v, back) ∧
+  hm.lookup key = some v ∧
+  ∀ v', ∃ hm', back v' = ok hm' ∧
+    hm'.lookup key = v' ∧
+    ∀ key', key' ≠ key → hm'.lookup key' = hm.lookup key'
+   := by
+  rw [get_mut]
+  simp [hash_key, alloc.vec.Vec.len]
+  have : 0 < hm.slots.val.len := by simp_all [inv]
+  progress as ⟨ hash_mod .. ⟩ -- TODO: decompose post by default
+  simp at *
+  have : 0 ≤ hash_mod.val := by -- TODO: automate
+    simp [*]
+    apply Int.emod_nonneg; simp [inv] at hInv; scalar_tac
+  have : hash_mod < hm.slots.val.len := by -- TODO: automate
+    simp [*]
+    apply Int.emod_lt_of_pos; scalar_tac
+  progress as ⟨ slot, index_back .. ⟩
+  have : slot_t_inv hm.slots.val.len hash_mod slot := by
+    simp_all [inv, slots_t_inv]
+  have : slot.lookup key ≠ none := by
+    simp_all [lookup]
+  progress as ⟨ v, back .. ⟩
+  simp [and_assoc, lookup, *]
+  constructor
+  . simp_all
+  . -- Backward function
+    intro v'
+    progress as ⟨ slot' .. ⟩
+    progress as ⟨ slots' ⟩
+    simp_all
+    -- Last postcondition
+    intro key' hNotEq
+    have : 0 ≤ key'.val % hm.slots.val.len := by -- TODO: automate
+      apply Int.emod_nonneg; simp [inv] at hInv; scalar_tac
+    have : key'.val % hm.slots.val.len < hm.slots.val.len := by -- TODO: automate
+      apply Int.emod_lt_of_pos; scalar_tac
+    -- We need to do a case disjunction
+    cases h: (key.val % hm.slots.val.len == key'.val % hm.slots.val.len) <;>
+    simp_all
+
+@[pspec]
+theorem remove_from_list_spec {α} (key : Usize) (slot : AList α) {l i} (hInv : slot_t_inv l i slot) :
+  ∃ v slot', remove_from_list α key slot = ok (v, slot') ∧
+  slot.lookup key = v ∧
+  slot'.lookup key = none ∧
+  (∀ key', key' ≠ key → slot'.lookup key' = slot.lookup key') ∧
+  match v with
+  | none => slot'.v.len = slot.v.len
+  | some _ => slot'.v.len = slot.v.len - 1 := by
+  rw [remove_from_list, remove_from_list_loop]
+  match hEq : slot with
+  | .Nil =>
+    simp [and_assoc]
+  | .Cons k v0 tl =>
+    simp
+    if hKey : k = key then
+      simp [hKey, and_assoc]
+      simp_all [slot_t_inv, slot_s_inv]
+      apply slot_allP_not_key_lookup
+      simp [*]
+    else
+      simp [hKey]
+      -- TODO: progress doesn't instantiate l properly
+      have hInv' : slot_t_inv l i tl := by simp_all [slot_t_inv]
+      have ⟨ v1, tl1, hRemove, _, _, hLookupTl1, _ ⟩ := remove_from_list_spec key tl hInv'
+      simp [and_assoc, *]; clear hRemove
+      constructor
+      . intro key' hNotEq1
+        simp_all
+      . cases v1 <;> simp_all
+
+theorem lookup'_not_none_imp_len_pos (l : List (Usize × α)) (key : Usize) (hLookup : l.lookup' key ≠ none) :
+  0 < l.len := by
+  induction l <;> simp_all
+  scalar_tac
+
+theorem lookup_not_none_imp_len_s_pos (hm : HashMap α) (key : Usize) (hLookup : hm.lookup key ≠ none)
+  (hNotEmpty : 0 < hm.slots.val.len) :
+  0 < hm.len_s := by
+  have : 0 ≤ key.val % hm.slots.val.len := by -- TODO: automate
+    apply Int.emod_nonneg; scalar_tac
+  have : key.val % hm.slots.val.len < hm.slots.val.len := by -- TODO: automate
+    apply Int.emod_lt_of_pos; scalar_tac
+  have := List.len_index_le_len_flatten hm.v (key.val % hm.slots.val.len)
+  have := lookup'_not_none_imp_len_pos (hm.slots.val.index (key.val % hm.slots.val.len)).v key
+  simp_all [lookup, len_s, al_v, v]
+  scalar_tac
+
+@[pspec]
+theorem remove_spec {α} (hm : HashMap α) (key : Usize) (hInv : hm.inv) :
+  ∃ v hm', remove α hm key = ok (v, hm') ∧
+  hm.lookup key = v ∧
+  hm'.lookup key = none ∧
+  (∀ key', key' ≠ key → hm'.lookup key' = hm.lookup key') ∧
+  match v with
+  | none => hm'.len_s = hm.len_s
+  | some _ => hm'.len_s = hm.len_s - 1 := by
+  rw [remove]
+  simp [hash_key, alloc.vec.Vec.len]
+  have : 0 < hm.slots.val.len := by simp_all [inv]
+  progress as ⟨ hash_mod .. ⟩ -- TODO: decompose post by default
+  simp at *
+  have : 0 ≤ hash_mod.val := by -- TODO: automate
+    simp [*]
+    apply Int.emod_nonneg; simp [inv] at hInv; scalar_tac
+  have : hash_mod < hm.slots.val.len := by -- TODO: automate
+    simp [*]
+    apply Int.emod_lt_of_pos; scalar_tac
+  progress as ⟨ slot, index_back .. ⟩
+  have : slot_t_inv hm.slots.val.len hash_mod slot := by simp_all [inv, slots_t_inv]
+  progress as ⟨ vOpt, slot' .. ⟩
+  match hOpt : vOpt with
+  | none =>
+    simp [*]
+    progress as ⟨ slot'' ⟩
+    simp [and_assoc, lookup, *]
+    simp_all [al_v, v]
+    intro key' hNotEq
+    -- We need to make a case disjunction
+    cases h: (key.val % hm.slots.val.len) == (key'.val % hm.slots.val.len) <;>
+    simp_all
+  | some v =>
+    simp [*]
+    have : 0 < hm.num_entries.val := by
+      have := lookup_not_none_imp_len_s_pos hm key (by simp_all [lookup]) (by simp_all [inv])
+      simp_all [inv]
+    progress as ⟨ newSize .. ⟩
+    progress as ⟨ slots1 .. ⟩
+    simp_all [and_assoc, lookup, al_v, HashMap.v]
+    constructor
+    . intro key' hNotEq
+      cases h: (key.val % hm.slots.val.len) == (key'.val % hm.slots.val.len) <;>
+      simp_all
+    . scalar_tac
+
 end HashMap
 
 end hashmap
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index 6f5d99a5..90d352c1 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -21,6 +21,7 @@ structure HashMap (T : Type) where
   num_entries : Usize
   max_load_factor : (Usize × Usize)
   max_load : Usize
+  saturated : Bool
   slots : alloc.vec.Vec (AList T)
 
 end hashmap
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 12a95d0f..6d7702c1 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -51,6 +51,8 @@ pub struct HashMap<T> {
     /// The max load factor applied to the current table length:
     /// gives the threshold at which to resize the table.
     max_load: usize,
+    /// [true] if we can't increase the size anymore.
+    saturated: bool,
     /// The table itself
     slots: Vec<AList<T>>,
 }
@@ -79,6 +81,7 @@ impl<T> HashMap<T> {
             num_entries: 0,
             max_load_factor: (max_load_dividend, max_load_divisor),
             max_load: (capacity * max_load_dividend) / max_load_divisor,
+            saturated: false,
             slots,
         }
     }
@@ -140,8 +143,8 @@ impl<T> HashMap<T> {
     pub fn insert(&mut self, key: Key, value: T) {
         // Insert
         self.insert_no_resize(key, value);
-        // Resize if necessary
-        if self.len() > self.max_load {
+        // Resize if necessary and if we're not saturated
+        if self.len() > self.max_load && !self.saturated {
             self.try_resize()
         }
     }
@@ -149,13 +152,7 @@ impl<T> HashMap<T> {
     /// The resize function, called if we need to resize the table after
     /// an insertion.
     fn try_resize(&mut self) {
-        // Check that we can resize: we need to check that there are no overflows.
-        // Note that we are conservative about the usize::MAX.
-        // Also note that `as usize` is a trait, but we apply it to a constant
-        // here, which gets compiled by the MIR interpreter (so we don't see
-        // the conversion, actually).
-        // Rk.: this is a hit heavy...
-        let max_usize = u32::MAX as usize;
+        let max_usize = usize::MAX;
         let capacity = self.slots.len();
         // Checking that there won't be overflows by using the fact that, if m > 0:
         // n * m <= p <==> n <= p / m
@@ -169,17 +166,20 @@ impl<T> HashMap<T> {
             );
 
             // Move the elements to the new table
-            HashMap::move_elements(&mut ntable, &mut self.slots, 0);
+            HashMap::move_elements(&mut ntable, &mut self.slots);
 
             // Replace the current table with the new table
             self.slots = ntable.slots;
             self.max_load = ntable.max_load;
+        } else {
+            self.saturated = true;
         }
     }
 
     /// Auxiliary function called by [try_resize] to move all the elements
     /// from the table to a new table
-    fn move_elements<'a>(ntable: &'a mut HashMap<T>, slots: &'a mut Vec<AList<T>>, mut i: usize) {
+    fn move_elements<'a>(ntable: &'a mut HashMap<T>, slots: &'a mut Vec<AList<T>>) {
+        let mut i = 0;
         while i < slots.len() {
             // Move the elements out of the slot i
             let ls = std::mem::replace(&mut slots[i], AList::Nil);
author	Son HO	2024-06-21 23:24:01 +0200
committer	GitHub	2024-06-21 23:24:01 +0200
commit	4d30546c809cb2c512e0c3fd8ee540fff1330eab (patch)
tree	d83926c9aa30f7bfb2a1c6db0e776003bca63355
parent	f264b9dcc6331eb9149d951f308cdc61c8c02801 (diff)