Amortized hash non resizing

theories/ub_logic/hash.v

@@ -1,7 +1,9 @@
 From clutch.ub_logic Require Export ub_clutch lib.map.
+From stdpp Require Export fin_maps.
+Import Hierarchy.
 Set Default Proof Using "Type*".
 
-Module simple_bit_hash.
+Section simple_bit_hash.
 
   Context `{!ub_clutchGS Σ}.
 
@@ -39,7 +41,10 @@ Module simple_bit_hash.
       compute_hash "hm".
 
   Definition hashfun f m : iProp Σ :=
-    ∃ (hm : loc), ⌜ f = compute_hash_specialized #hm ⌝ ∗ map_list hm ((λ b, LitV (LitInt b)) <$> m).
+    ∃ (hm : loc), ⌜ f = compute_hash_specialized #hm ⌝ ∗
+                  map_list hm ((λ b, LitV (LitInt b)) <$> m) ∗
+                  ⌜map_Forall (λ ind i, (0<= i <=val_size)%Z) m⌝
+  .
 
   #[global] Instance timeless_hashfun f m :
     Timeless (hashfun f m).
@@ -115,7 +120,7 @@ Module simple_bit_hash.
     {{{ RET #b; hashfun f m }}}.
   Proof.
     iIntros (Hlookup Φ) "Hhash HΦ".
-    iDestruct "Hhash" as (hm ->) "H".
+    iDestruct "Hhash" as (hm ->) "[H Hbound]".
     rewrite /compute_hash_specialized.
     wp_pures.
     wp_apply (wp_get with "[$]").
@@ -125,15 +130,15 @@ Module simple_bit_hash.
   Qed.
 
 
-  Lemma wp_insert_no_coll E f m (n : nat) (z : Z) :
+  Lemma wp_insert_no_coll E f m (n : nat) :
     m !! n = None →
     {{{ hashfun f m ∗ € (nnreal_div (nnreal_nat (length (gmap_to_list m))) (nnreal_nat(val_size+1))) ∗
           ⌜coll_free m⌝ }}}
       f #n @ E
     {{{ (v : Z), RET #v; hashfun f (<[ n := v ]>m) ∗ ⌜coll_free (<[ n := v ]>m)⌝ }}}.
   Proof.
     iIntros (Hlookup Φ) "(Hhash & Herr & %Hcoll) HΦ".
-    iDestruct "Hhash" as (hm ->) "H".
+    iDestruct "Hhash" as (hm ->) "[H %Hbound]".
     rewrite /compute_hash_specialized.
     wp_pures.
     wp_apply (wp_get with "[$]").
@@ -154,11 +159,229 @@ Module simple_bit_hash.
     - rewrite /hashfun.
       iExists _.
       iSplit; first auto.
-      rewrite fmap_insert //.
+      iSplitL.
+      + rewrite fmap_insert //.
+      + iPureIntro.
+        apply map_Forall_insert_2; last done.
+        split.
+        * lia.
+        * pose proof (fin_to_nat_lt x).
+          lia. 
     - iPureIntro.
       apply coll_free_insert; auto.
       apply (Forall_map (λ p : nat * Z, p.2)) in HForall; auto.
   Qed.
 
-
+  
 End simple_bit_hash.
+
+
+
+Section amortized_hash.
+  Context `{!ub_clutchGS Σ}.
+  Variable val_size:nat.
+  Variable max_hash_size : nat.
+  (* Variable Hineq : (max_hash_size <= (val_size+1))%nat. *)
+  Program Definition amortized_error : nonnegreal :=
+    mknonnegreal ((max_hash_size + 1)/(2*(val_size + 1)))%R _.
+  Next Obligation.
+    pose proof (pos_INR val_size) as H.
+    pose proof (pos_INR max_hash_size) as H'.
+    apply Rcomplements.Rdiv_le_0_compat; lra.
+  Qed.
+
+  Definition hashfun_amortized f m : iProp Σ :=
+    ∃ (hm : loc) (k : nat) (ε : nonnegreal),
+      ⌜ f = compute_hash_specialized val_size #hm ⌝ ∗
+      ⌜map_Forall (λ ind i, (0<= i <=val_size)%Z) m⌝ ∗
+      ⌜k = size m⌝ ∗
+      ⌜ (ε.(nonneg) = (((max_hash_size + 1) * k)/2 - sum_n_m (λ x, INR x) 0%nat (k-1)) / (val_size + 1))%R⌝ ∗
+      € ε ∗
+      map_list hm ((λ b, LitV (LitInt b)) <$> m) 
+  .
+
+  #[global] Instance timeless_hashfun_amortized f m :
+    Timeless (hashfun_amortized f m).
+  Proof. apply _. Qed.
+
+  Lemma wp_init_hash_amortized E :
+    {{{ True }}}
+      init_hash val_size #() @ E
+      {{{ f, RET f; hashfun_amortized f ∅ }}}.
+  Proof.
+    rewrite /init_hash.
+    iIntros (Φ) "_ HΦ".
+    wp_pures. rewrite /init_hash_state.
+    wp_apply (wp_init_map with "[//]").
+    iIntros (?) "Hm". wp_pures.
+    rewrite /compute_hash. wp_pures.
+    iApply "HΦ". iExists _. rewrite fmap_empty. iFrame.
+    iMod ec_zero.
+    iModIntro. iExists 0%nat, nnreal_zero.
+    repeat (iSplit; [done|]). iFrame.
+    iPureIntro.
+    simpl.
+    replace (sum_n_m _ _ _) with 0; first lra.
+    rewrite sum_n_n. by simpl. 
+  Qed.
+
+  Lemma wp_hashfun_prev_amortized E f m (n : nat) (b : Z) :
+    m !! n = Some b →
+    {{{ hashfun_amortized f m }}}
+      f #n @ E
+      {{{ RET #b; hashfun_amortized f m }}}.
+  Proof.
+    iIntros (Hlookup Φ) "Hhash HΦ".
+    iDestruct "Hhash" as (hm k ε ->) "[%[-> [% [Hε H]]]]".
+    wp_apply (wp_hashfun_prev with "[H]"); first done.
+    - iExists _. by iFrame.
+    - iIntros "(%&%&H)". inversion H1; subst. iApply "HΦ".
+      iExists _,_,_. iFrame. repeat iSplit; try done.
+      by iDestruct "H" as "[??]".
+  Qed.
+
+  Lemma hashfun_amortized_hashfun f m: ⊢ hashfun_amortized f m -∗ hashfun val_size f m.
+  Proof.
+    iIntros "(%&%&%&->&%&->&%&He&H)".
+    iExists _; by iFrame.
+  Qed.
+
+  Lemma amortized_inequality (k : nat):
+    (k <= max_hash_size)%nat ->
+    0 <= ((max_hash_size + 1) * k / 2 - sum_n_m (λ x : nat, INR x) 0 (k - 1)) / (val_size + 1).
+  Proof.
+    intros H.
+    pose proof (pos_INR max_hash_size) as H1.
+    pose proof (pos_INR val_size) as H2.    
+    pose proof (pos_INR k) as H3.    
+    apply Rcomplements.Rdiv_le_0_compat; last lra.
+    assert (sum_n_m (λ x : nat, INR x) 0 (k - 1) = (k-1)*k/2) as ->.
+    - clear.
+      induction k.
+      + simpl. rewrite sum_n_n.
+        rewrite Rmult_0_r. by assert (0/2 = 0) as -> by lra.
+      + clear. induction k.
+        * simpl. rewrite sum_n_n.
+          replace (_-_) with 0 by lra.
+          rewrite Rmult_0_l. by assert (0/2 = 0) as -> by lra.
+        * assert (S (S k) - 1 = S (S k - 1))%nat as -> by lia.
+          rewrite sum_n_Sm; last lia.
+          rewrite IHk.
+          replace (plus _ _) with (((S k - 1) * S k / 2) + (S (S k - 1))) by done.
+          assert (∀ k, (INR (S k) - 1) = (INR k)) as H'.
+          { intros. simpl. case_match; first replace (1 - 1) with 0 by lra.
+            - done.
+            - by replace (_+1-1) with (INR (S n)) by lra.
+          }
+          rewrite !H'.
+          replace (S k - 1)%nat with (k)%nat by lia.
+          assert (k * (S k) + S k + S k = S k * S (S k)); last lra.
+          assert (k * S k + S k + S k = S k * (k+1+1)) as ->; try lra.
+          assert (k+1+1 = S (S k)).
+          -- rewrite !S_INR. lra.
+          -- by rewrite H. 
+    - rewrite -!Rmult_minus_distr_r.
+      apply Rcomplements.Rdiv_le_0_compat; try lra.
+      apply Rmult_le_pos; try lra.
+      assert (INR k <= INR max_hash_size); try lra.
+      by apply le_INR.
+  Qed.
+
+
+  Lemma wp_insert_new_amortized E f m (n : nat) :
+    m !! n = None →
+    (size m < max_hash_size)%nat ->
+    {{{ hashfun_amortized f m ∗ € amortized_error ∗
+        ⌜coll_free m⌝ }}}
+      f #n @ E
+      {{{ (v : Z), RET #v; hashfun_amortized f (<[ n := v ]>m) ∗ ⌜coll_free (<[ n := v ]>m)⌝ }}}.
+  Proof.
+    iIntros (Hlookup Hsize Φ) "(Hhash & Herr & %Hcoll) HΦ".
+    iDestruct "Hhash" as (hm k ε -> ) "[%[->[% [Hε H]]]]".
+    iAssert (€ (nnreal_div (nnreal_nat (size m)) (nnreal_nat (val_size + 1))) ∗
+             € (mknonnegreal (((max_hash_size + 1) * size (<[n:=0%Z]> m) / 2 - sum_n_m (λ x, INR x) 0%nat (size (<[n:=0%Z]> m) - 1)) / (val_size + 1)) _ )
+            )%I with "[Hε Herr]" as "[Hε Herr]".
+    - iApply ec_split.
+      iCombine "Hε Herr" as "H".
+      iApply (ec_spend_irrel with "[$]").
+      simpl. rewrite H0. rewrite map_size_insert_None; [|done].
+      remember (size m) as k.
+      remember (val_size + 1) as v.
+      remember (max_hash_size) as h.
+      assert (∀ x y, x/y = x*/y) as Hdiv.
+      { intros. lra. }
+      destruct k.
+      + simpl. rewrite sum_n_n. rewrite Rmult_0_l Rmult_0_r.
+        replace (INR 0%nat) with 0; last done.
+        rewrite !Rminus_0_r.
+        replace (0/_/_) with 0; last lra.
+        rewrite !Rplus_0_l.
+        rewrite Rmult_1_r.
+        rewrite !Hdiv.
+        rewrite Rinv_mult.
+        lra. 
+      + assert (forall k, S k - 1 = k)%nat as H' by lia.
+        rewrite !H'.
+        clear H'.
+        rewrite sum_n_Sm; last lia.
+        replace (plus _ (INR (S k))) with ((sum_n_m (λ x : nat, INR x) 0 k) + (S k)) by done.
+        rewrite !Hdiv.
+        rewrite !Rmult_minus_distr_r.
+        rewrite (Rmult_plus_distr_r (sum_n_m _ _ _)).
+        rewrite -!Rplus_assoc.
+        rewrite Ropp_plus_distr.
+        rewrite -!Rplus_assoc.
+        assert ((h + 1) * S k * / 2 * / v+ (h + 1) * / (2 * v) = S k * / (val_size + 1)%nat + (h + 1) * S (S k) * / 2 * / v  + - (S k * / v)); try lra.
+        replace (INR((_+_)%nat)) with v; last first.
+        { rewrite Heqv. rewrite -S_INR. f_equal. lia. }
+        assert ( (h + 1) * S k * / 2 * / v + (h + 1) * / (2 * v) = (h + 1) * S (S k) * / 2 * / v); try lra.
+        replace (_*_*_*_) with ((h+1) * (S k) * /(2*v)); last first.
+        { rewrite Rinv_mult. lra. }
+        replace (_*_*_*_) with ((h+1) * (S(S k)) * /(2*v)); last first.
+        { rewrite Rinv_mult. lra. }
+        rewrite -Rdiv_plus_distr.
+        rewrite Hdiv.
+        f_equal.
+        rewrite -{2}(Rmult_1_r (h+1)).
+        rewrite -Rmult_plus_distr_l.
+        f_equal.
+    - wp_apply (wp_insert_no_coll with "[H Hε]"); [done|..].
+      + iFrame. iSplitL; try done.
+        iExists _. by iFrame.
+      + iIntros (v) "[H %]".
+        iApply "HΦ".
+        iSplitL; last done.
+        iExists _, _, _. iFrame.
+        iDestruct "H" as "(%&%&H&%)".
+        repeat (iSplitR); try done.
+        * iPureIntro. simpl. do 3 f_equal.
+          all: by repeat rewrite map_size_insert.
+        * inversion H2; by subst.
+          Unshelve.
+          apply amortized_inequality.
+          rewrite map_size_insert.
+          case_match => /=; lia.
+  Qed.
+
+  Lemma wp_insert_amortized E f m (n : nat) :
+    (size m < max_hash_size)%nat ->
+    {{{ hashfun_amortized f m ∗ € amortized_error ∗
+        ⌜coll_free m⌝ }}}
+      f #n @ E
+      {{{ (v : Z), RET #v; ∃ m', hashfun_amortized f m' ∗ ⌜coll_free m'⌝ ∗ ⌜m'!!n = Some v⌝ ∗ ⌜(size m' <= S $ size(m))%nat⌝ ∗ ⌜m⊆m'⌝ }}}.
+  Proof.
+    iIntros (Hsize Φ) "[Hh[Herr %Hc]] HΦ".
+    destruct (m!!n) eqn:Heq.
+    - wp_apply (wp_hashfun_prev_amortized with "[$]"); first done.
+      iIntros. iApply "HΦ".
+      iExists _; iFrame.
+      repeat iSplit; try done. iPureIntro; lia.
+    - wp_apply (wp_insert_new_amortized with "[$Hh $Herr]"); try done.
+      iIntros (?) "[??]"; iApply "HΦ".
+      iExists _; iFrame. iPureIntro. repeat split.
+      + rewrite lookup_insert_Some. naive_solver.
+      + rewrite map_size_insert. case_match; try (simpl; lia).
+      + by apply insert_subseteq.
+  Qed.
+
+End amortized_hash.