Progress with seq hash interface

theories/coneris/examples/hash/hash_view_impl.v

@@ -0,0 +1,118 @@
+From iris.algebra Require Import gset_bij.
+From clutch.coneris Require Export coneris hash_view_interface.
+
+Set Default Proof Using "Type*".
+
+Section hash_view_impl.
+  Context `{Hcon:conerisGS Σ, 
+              HinG: inG Σ (gset_bijR nat nat)}.
+
+  Definition hash_view_auth m γ := (own γ (gset_bij_auth (DfracOwn 1) (map_to_set pair m)))%I.
+  Definition hash_view_frag k v γ := (own γ (gset_bij_elem k v)).
+
+  Lemma hash_view_auth_coll_free m γ2:
+    hash_view_auth m γ2 -∗ ⌜coll_free m⌝.
+  Proof.
+    rewrite /hash_view_auth.
+    iIntros "H".
+    iDestruct (own_valid with "[$]") as "%H".
+    rewrite gset_bij_auth_valid in H.
+    iPureIntro.
+    intros k1 k2 H1 H2 H3.
+    destruct H1 as [v1 K1].
+    destruct H2 as [v2 H2].
+    assert (v1 = v2) as ->; first by erewrite !lookup_total_correct in H3.
+    unshelve epose proof (H k1 v2 _) as [_ H']; first by rewrite elem_of_map_to_set_pair.
+    unshelve epose proof (H' k2 _) as ->; last done.
+    by rewrite elem_of_map_to_set_pair.
+  Qed.
+
+  Lemma hash_view_auth_duplicate_frag m n b γ2:
+    m!!n=Some b -> hash_view_auth m γ2 ==∗ hash_view_auth m γ2 ∗ hash_view_frag n b γ2.
+  Proof.
+    iIntros (Hsome) "Hauth".
+    rewrite /hash_view_auth/hash_view_frag.
+    rewrite -own_op.
+    iApply own_update; last done.
+    rewrite -core_id_extract; first done.
+    apply bij_view_included.
+    rewrite elem_of_map_to_set.
+    naive_solver.
+  Qed.
+
+  Lemma hash_view_auth_frag_agree m γ2 k v:
+    hash_view_auth m γ2  ∗ hash_view_frag k v γ2 -∗
+    ⌜m!!k=Some v⌝.
+  Proof.
+    rewrite /hash_view_auth/hash_view_frag.
+    rewrite -own_op.
+    iIntros "H".
+    iDestruct (own_valid with "[$]") as "%H".
+    rewrite bij_both_valid in H.
+    destruct H as [? H].
+    rewrite elem_of_map_to_set in H.
+    iPureIntro.
+    destruct H as (?&?&?&?).
+    by simplify_eq.
+  Qed.
+
+  Lemma hash_view_auth_insert m n x γ:
+    m!!n=None ->
+    Forall (λ m : nat, x ≠ m) (map (λ p : nat * nat, p.2) (map_to_list m)) ->
+    hash_view_auth m γ ==∗
+    hash_view_auth (<[n:=x]> m) γ ∗ hash_view_frag n x γ.
+  Proof.
+    iIntros (H1 H2) "H".
+    rewrite /hash_view_auth/hash_view_frag.
+    rewrite -own_op.
+    iApply own_update; last done.
+    rewrite -core_id_extract; last first.
+    { apply bij_view_included. rewrite elem_of_map_to_set.
+      eexists _, _; split; last done.
+      apply lookup_insert.
+    }
+    etrans; first apply gset_bij_auth_extend; last by rewrite map_to_set_insert_L.
+    - intros b. rewrite elem_of_map_to_set; intros (?&?&?&?).
+      simplify_eq.
+    - intros a. rewrite elem_of_map_to_set; intros (?&?&?&?).
+      simplify_eq.
+      rewrite Forall_map in H2.
+      rewrite Forall_forall in H2.
+      unfold not in H2.
+      eapply H2; [by erewrite elem_of_map_to_list|done].
+  Qed.
+End hash_view_impl.
+
+
+
+Class hvG1 Σ := {hvG1_gsetbijR :: inG Σ (gset_bijR nat nat)}. 
+Program Definition hv_impl `{!conerisGS Σ} : hash_view :=
+  {|
+    hvG := hvG1;
+    hv_name := gname;
+    hv_auth _ m γ := hash_view_auth m γ;
+    hv_frag _ k v γ := hash_view_frag k v γ
+  |}.
+Next Obligation.
+  rewrite /hash_view_auth.
+  iIntros. iApply own_alloc.
+  by rewrite gset_bij_auth_valid.
+Qed.
+Next Obligation.
+  simpl.
+  iIntros.
+  by iApply hash_view_auth_coll_free.
+Qed.
+Next Obligation.
+  simpl. iIntros.
+  by iApply hash_view_auth_duplicate_frag.
+Qed.
+Next Obligation.
+  simpl. iIntros.
+  by iApply hash_view_auth_frag_agree.
+Qed.
+Next Obligation.
+  simpl.
+  iIntros.
+  by iApply hash_view_auth_insert.
+Qed.

theories/coneris/examples/hash/hash_view_interface.v

@@ -0,0 +1,41 @@
+From clutch.coneris Require Import coneris.
+
+Set Default Proof Using "Type*".
+
+(* A hash function is collision free if the partial map it
+     implements is an injective function *)
+Definition coll_free (m : gmap nat nat) :=
+  forall k1 k2,
+  is_Some (m !! k1) ->
+  is_Some (m !! k2) ->
+  m !!! k1 = m !!! k2 ->
+  k1 = k2.
+
+Class hash_view `{!conerisGS Σ} := Hash_View
+{
+  hvG : gFunctors -> Type;
+  hv_name : Type; 
+  hv_auth {L:hvG Σ} : gmap nat nat ->  hv_name -> iProp Σ;
+  hv_frag {L:hvG Σ} : nat -> nat -> hv_name -> iProp Σ;
+
+  hv_auth_timeless {L:hvG Σ} m γ::
+  Timeless (hv_auth (L:=L) m γ);
+  hv_frag_timeless {L:hvG Σ} k v γ::
+  Timeless (hv_frag (L:=L) k v γ);
+  hv_frag_persistent {L:hvG Σ} k v γ::
+  Persistent (hv_frag (L:=L) k v γ);
+
+  hv_auth_init {L:hvG Σ}:
+  (⊢|==> (∃ γ, hv_auth (L:=L) ∅ γ))%I;
+  hv_auth_coll_free {L:hvG Σ} m γ: hv_auth (L:=L) m γ -∗ ⌜coll_free m⌝;
+  hv_auth_duplicate_frag {L:hvG Σ} m n b γ:
+    m!!n=Some b -> hv_auth (L:=L) m γ ==∗ hv_auth (L:=L) m γ ∗ hv_frag (L:=L) n b γ;
+  hv_auth_frag_agree {L:hvG Σ} m γ k v:
+    hv_auth (L:=L) m γ  ∗ hv_frag (L:=L) k v γ -∗
+    ⌜m!!k=Some v⌝;
+  hv_auth_insert {L:hvG Σ} m n x γ:
+    m!!n=None ->
+    Forall (λ m : nat, x ≠ m) (map (λ p : nat * nat, p.2) (map_to_list m)) ->
+    hv_auth (L:=L) m γ ==∗
+    hv_auth (L:=L) (<[n:=x]> m) γ ∗ hv_frag (L:=L) n x γ             
+}.

theories/coneris/examples/hash/seq_hash.v

@@ -1,122 +1,8 @@
 From stdpp Require Export fin_maps.
 From iris.algebra Require Import excl_auth numbers gset_bij.
-From clutch.coneris Require Export coneris lib.map hocap_rand abstract_tape seq_hash_interface.
+From clutch.coneris Require Export coneris lib.map hocap_rand abstract_tape hash_view_interface seq_hash_interface.
 Set Default Proof Using "Type*".
 
-Section hash_view_impl.
-  Context `{Hcon:conerisGS Σ, 
-              HinG: inG Σ (gset_bijR nat nat)}.
-
-  Definition hash_view_auth m γ := (own γ (gset_bij_auth (DfracOwn 1) (map_to_set pair m)))%I.
-  Definition hash_view_frag k v γ := (own γ (gset_bij_elem k v)).
-
-  Lemma hash_view_auth_coll_free m γ2:
-    hash_view_auth m γ2 -∗ ⌜coll_free m⌝.
-  Proof.
-    rewrite /hash_view_auth.
-    iIntros "H".
-    iDestruct (own_valid with "[$]") as "%H".
-    rewrite gset_bij_auth_valid in H.
-    iPureIntro.
-    intros k1 k2 H1 H2 H3.
-    destruct H1 as [v1 K1].
-    destruct H2 as [v2 H2].
-    assert (v1 = v2) as ->; first by erewrite !lookup_total_correct in H3.
-    unshelve epose proof (H k1 v2 _) as [_ H']; first by rewrite elem_of_map_to_set_pair.
-    unshelve epose proof (H' k2 _) as ->; last done.
-    by rewrite elem_of_map_to_set_pair.
-  Qed.
-
-  Lemma hash_view_auth_duplicate_frag m n b γ2:
-    m!!n=Some b -> hash_view_auth m γ2 ==∗ hash_view_auth m γ2 ∗ hash_view_frag n b γ2.
-  Proof.
-    iIntros (Hsome) "Hauth".
-    rewrite /hash_view_auth/hash_view_frag.
-    rewrite -own_op.
-    iApply own_update; last done.
-    rewrite -core_id_extract; first done.
-    apply bij_view_included.
-    rewrite elem_of_map_to_set.
-    naive_solver.
-  Qed.
-
-  Lemma hash_view_auth_frag_agree m γ2 k v:
-    hash_view_auth m γ2  ∗ hash_view_frag k v γ2 -∗
-    ⌜m!!k=Some v⌝.
-  Proof.
-    rewrite /hash_view_auth/hash_view_frag.
-    rewrite -own_op.
-    iIntros "H".
-    iDestruct (own_valid with "[$]") as "%H".
-    rewrite bij_both_valid in H.
-    destruct H as [? H].
-    rewrite elem_of_map_to_set in H.
-    iPureIntro.
-    destruct H as (?&?&?&?).
-    by simplify_eq.
-  Qed.
-
-  Lemma hash_view_auth_insert m n x γ:
-    m!!n=None ->
-    Forall (λ m : nat, x ≠ m) (map (λ p : nat * nat, p.2) (map_to_list m)) ->
-    hash_view_auth m γ ==∗
-    hash_view_auth (<[n:=x]> m) γ ∗ hash_view_frag n x γ.
-  Proof.
-    iIntros (H1 H2) "H".
-    rewrite /hash_view_auth/hash_view_frag.
-    rewrite -own_op.
-    iApply own_update; last done.
-    rewrite -core_id_extract; last first.
-    { apply bij_view_included. rewrite elem_of_map_to_set.
-      eexists _, _; split; last done.
-      apply lookup_insert.
-    }
-    etrans; first apply gset_bij_auth_extend; last by rewrite map_to_set_insert_L.
-    - intros b. rewrite elem_of_map_to_set; intros (?&?&?&?).
-      simplify_eq.
-    - intros a. rewrite elem_of_map_to_set; intros (?&?&?&?).
-      simplify_eq.
-      rewrite Forall_map in H2.
-      rewrite Forall_forall in H2.
-      unfold not in H2.
-      eapply H2; [by erewrite elem_of_map_to_list|done].
-  Qed.
-End hash_view_impl.
-
-
-
-Class hvG1 Σ := {hvG1_gsetbijR :: inG Σ (gset_bijR nat nat)}. 
-Program Definition hv_impl `{!conerisGS Σ} : hash_view :=
-  {|
-    hvG := hvG1;
-    hv_name := gname;
-    hv_auth _ m γ := hash_view_auth m γ;
-    hv_frag _ k v γ := hash_view_frag k v γ
-  |}.
-Next Obligation.
-  rewrite /hash_view_auth.
-  iIntros. iApply own_alloc.
-  by rewrite gset_bij_auth_valid.
-Qed.
-Next Obligation.
-  simpl.
-  iIntros.
-  by iApply hash_view_auth_coll_free.
-Qed.
-Next Obligation.
-  simpl. iIntros.
-  by iApply hash_view_auth_duplicate_frag.
-Qed.
-Next Obligation.
-  simpl. iIntros.
-  by iApply hash_view_auth_frag_agree.
-Qed.
-Next Obligation.
-  simpl.
-  iIntros.
-  by iApply hash_view_auth_insert.
-Qed.
-
 Section seq_hash_impl.
 
   Context `{Hcon:conerisGS Σ, r1:!@rand_spec Σ Hcon, L:!randG Σ,
@@ -169,8 +55,6 @@ Section seq_hash_impl.
                   [∗ map] α ↦ t ∈ tape_m,  rand_tapes (L:=L) α (val_size, t)
   .
 
-  Definition tape_m_elements (tape_m : gmap val (list nat)) :=
-    concat (map_to_list tape_m).*2.
 
   Definition hash_tape α ns γ:=
     (α ◯↪N (val_size; ns) @ γ)%I .