summaryrefslogtreecommitdiff
path: root/tests/lean/Hashmap
diff options
context:
space:
mode:
authorSon HO2024-06-21 23:24:01 +0200
committerGitHub2024-06-21 23:24:01 +0200
commit4d30546c809cb2c512e0c3fd8ee540fff1330eab (patch)
treed83926c9aa30f7bfb2a1c6db0e776003bca63355 /tests/lean/Hashmap
parentf264b9dcc6331eb9149d951f308cdc61c8c02801 (diff)
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>
Diffstat (limited to 'tests/lean/Hashmap')
-rw-r--r--tests/lean/Hashmap/Funs.lean53
-rw-r--r--tests/lean/Hashmap/Properties.lean954
-rw-r--r--tests/lean/Hashmap/Types.lean1
3 files changed, 941 insertions, 67 deletions
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