diff options
| -rw-r--r-- | backends/lean/Base/Arith/Base.lean | 8 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 48 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 12 | ||||
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 23 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 11 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 13 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 6 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 42 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 67 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Types.v | 2 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Clauses.Template.fst | 8 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 55 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Types.fst | 1 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 53 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 954 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Types.lean | 1 | ||||
| -rw-r--r-- | tests/src/hashmap.rs | 22 |
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); |