define predicates for con hash

theories/coneris/examples/hash/con_hash_impl.v

@@ -1,5 +1,5 @@
 From iris.algebra Require Import excl_auth gmap.
-From clutch.coneris Require Import coneris hash_view_interface seq_hash_interface lock.
+From clutch.coneris Require Import coneris hocap_rand lib.map abstract_tape hash_view_interface lock.
 
 Set Default Proof Using "Type*".
 (* Concurrent hash impl*)
@@ -64,30 +64,93 @@ Section lemmas'.
 End lemmas'.
 
 
+Class con_hashG (Σ:gFunctors) := ConhashG {
+                                     conhashG_tapesG::inG Σ (excl_authR (gmapO nat natO));
+                                     conhashG_sizeG::inG Σ (excl_authR natO);
+                                     conhashG_conerisG::conerisGS Σ;
+                                     conhashG_rand::@rand_spec Σ conhashG_conerisG;
+                                     conhashG_randG:randG Σ;
+                                     conhashG_hv::@hash_view Σ conhashG_conerisG;
+                                     conhashG_hvG: hvG Σ;
+                                     conhashG_abstract_tapesG::abstract_tapesGS Σ;
+                                     conhashG_lock::lock;
+                                     conhashG_lockG:lockG Σ
+
+}.
 Section con_hash_impl.
-
-  Context `{Hcon:conerisGS Σ, sh:@seq_hash Σ Hcon h hvG0 val_size, shG:seq_hashG Σ, l:lock, lockG Σ}.
-  Context `{inG Σ (excl_authR (gmapO nat natO)), inG Σ (excl_authR natO)}.
+  Context `{con_hashG Σ}.
+  Variable val_size:nat.
 
-  Definition init_con_hash := init_hash.
-  Definition allocate_tape:= seq_hash_interface.allocate_tape.
+  (* A hash function's internal state is a map from previously queried keys to their hash value *)
+  Definition init_hash_state : val := init_map.
+
+  (* To hash a value v, we check whether it is in the map (i.e. it has been previously hashed).
+     If it has we return the saved hash value, otherwise we draw a hash value and save it in the map *)
+  (* Definition compute_hash_specialized hm : val := *)
+  (*   λ: "v" "α", *)
+  (*     match: get hm "v" with *)
+  (*     | SOME "b" => "b" *)
+  (*     | NONE => *)
+  (*         let: "b" := (rand_tape "α" #val_size) in *)
+  (*         set hm "v" "b";; *)
+  (*         "b" *)
+  (*     end. *)
+  Definition compute_hash : val :=
+    λ: "hm" "v" "α",
+      match: get "hm" "v" with
+      | SOME "b" => "b"
+      | NONE =>
+          let: "b" := (rand_tape "α" #val_size) in
+          set "hm" "v" "b";;
+          "b"
+      end.
+
+  (* init_hash returns a hash as a function, basically wrapping the internal state
+     in the returned function *)
+  Definition init_hash : val :=
+    λ: "_",
+      let: "hm" := init_hash_state #() in
+      let: "l" := newlock #() in
+      ("l", compute_hash "hm").
 
-  Definition compute_con_hash (h l:val):val:=
+  Definition allocate_tape : val :=
     λ: "_",
-      acquire l;;
-      let: "output" := compute_hash "input" in
-      release l;;
+      rand_allocate_tape #val_size.
+
+  Definition compute_con_hash :val:=
+    λ: "lhm" "v" "α",
+      let, ("l", "hm") := "lhm" in
+      acquire "l";;
+      let: "output" := compute_hash "hm" "v" "α" in
+      release "l";;
       "output".
 
-  Definition abstract_con_hash (f:val) (γ1:seq_hash_tape_gname) (γ2:hv_name) γ3 γ4 : iProp Σ :=
-    ∃ m tape_m,
-      abstract_seq_hash (L:=shG) f m tape_m γ1 γ2 ∗
+  Definition compute_con_hash_specialized (lhm:val):val:=
+    λ: "v" "α",
+      let, ("l", "hm") := lhm in
+      acquire "l";;
+      let: "output" := (compute_hash "hm") "v" "α" in
+      release "l";;
+      "output".
+
+  Definition tape_m_elements (tape_m : gmap val (list nat)) :=
+    concat (map_to_list tape_m).*2.
+
+  Definition abstract_con_hash (f:val) (l:val) (hm:loc) γ1 γ2 γ3 γ4 : iProp Σ :=
+    ∃ m tape_m ,
+      ⌜f=compute_con_hash_specialized (l, #hm)%V⌝ ∗
+      ⌜map_Forall (λ ind i, (0<= i <=val_size)%nat) m⌝ ∗
+      (* the tapes*)
+      ● ((λ x, (val_size, x))<$>tape_m) @ γ1 ∗
+      ([∗ map] α ↦ t ∈ tape_m,  rand_tapes (L:=conhashG_randG) α (val_size, t)) ∗
+      hv_auth (L:=conhashG_hvG) m γ2 ∗
+      ⌜NoDup (tape_m_elements tape_m ++ (map_to_list m).*2)⌝ ∗
       own γ3 (●E m) ∗
       own γ4 (●E (length (map_to_list m) + length (tape_m_elements tape_m)))
   .
 
-  Definition concrete_con_hash (f:val) (m:gmap nat nat) γ : iProp Σ:=
-    concrete_seq_hash (L:=shG) f m ∗
+  Definition concrete_con_hash (hm:loc) (m:gmap nat nat) γ : iProp Σ:=
+    map_list hm ((λ b, LitV (LitInt (Z.of_nat b))) <$> m) ∗
     own γ (◯E m).
 
 End con_hash_impl.

theories/coneris/examples/hash/seq_hash_impl.v

@@ -1,6 +1,6 @@
 From stdpp Require Export fin_maps.
 From iris.algebra Require Import excl_auth numbers gset_bij.
-From clutch.coneris Require Import coneris lib.map hocap_rand abstract_tape seq_hash_interface hash_view_interface.
+From clutch.coneris Require Import coneris lib.map hocap_rand abstract_tape hash_view_interface.
 Set Default Proof Using "Type*".
 
 Section seq_hash_impl.
@@ -60,7 +60,7 @@ Section seq_hash_impl.
 
   Definition hash_tape α ns γ:=
     (α ◯↪N (val_size; ns) @ γ)%I .
-
+  
   Definition coll_free_hashfun f m tape_m γ1 γ2: iProp Σ :=
     hashfun f m tape_m γ1 ∗ hv_auth (L:=L') m γ2 ∗
     ⌜NoDup (tape_m_elements tape_m ++ (map_to_list m).*2)⌝.

theories/coneris/examples/hash/seq_hash_interface.v

@@ -1,9 +1,7 @@
 From clutch.coneris Require Import coneris hash_view_interface.
 
 Set Default Proof Using "Type*".
-
-(** * TODO *)
-(** * For the hash with lock, the lock protects the hash table plus the authoritative part of the maps*)
+(** * Not that useful *)
 
 Definition tape_m_elements (tape_m : gmap val (list nat)) :=
     concat (map_to_list tape_m).*2.