diff options
Diffstat (limited to 'tests/lean/Hashmap/Properties.lean')
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 954 |
1 files changed, 912 insertions, 42 deletions
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 |