diff --git a/src/program_proof/pav/merkle.v b/src/program_proof/pav/merkle.v
index ec08037ec..312ff7b2c 100644
--- a/src/program_proof/pav/merkle.v
+++ b/src/program_proof/pav/merkle.v
@@ -10,32 +10,22 @@ Context `{!heapGS Σ}.
 Inductive tree : Type :=
   (* Cut only exists for proof checking trees. *)
   | Cut : list w8 → tree
-  | Empty : tree
   | Leaf : list w8 → tree
-  | Interior : list tree → tree.
-
-Fixpoint has_entry (tr : tree) (id : list w8) (node : tree) : Prop :=
-  match tr with
-  | Cut _ => False
-  | Empty => id = [] ∧ tr = node
-  | Leaf val => id = [] ∧ tr = node
-  | Interior children =>
-    match id with
-    | [] => False
-    | pos :: rest =>
-      ∃ child, children !! Z.to_nat (word.unsigned pos) = Some child ∧ has_entry child rest node
-    end
-  end.
+  | Interior : list (option tree) → tree.
 
 (* The core invariant that defines the recursive hashing structure of merkle trees. *)
 Fixpoint is_node_hash (tr : tree) (hash : list w8) : iProp Σ :=
   match tr with
   | Cut hash' => ⌜hash = hash' ∧ length hash' = 32%nat⌝
-  | Empty => is_hash [W8 0] hash
   | Leaf val => is_hash (val ++ [W8 1]) hash
   | Interior children =>
     ∃ (child_hashes : list (list w8)),
-    let map_fn := (λ c h, is_node_hash c h) in
+    let map_fn := (λ c h,
+                     match c with
+                     | None => is_hash [W8 0] h
+                     | Some c => is_node_hash c h
+                     end
+                  ) in
     ([∗ list] child_fn;hash' ∈ (map_fn <$> children);child_hashes,
       child_fn hash') ∗
     is_hash (concat child_hashes ++ [W8 2]) hash
@@ -55,7 +45,7 @@ Proof.
   iIntros "Htree".
   destruct tr.
   { iDestruct "Htree" as "[%Heq %Hlen]". naive_solver. }
-  1-2: iDestruct (is_hash_len with "Htree") as "%Hlen"; naive_solver.
+  { iDestruct (is_hash_len with "Htree") as "%Hlen"; naive_solver. }
   {
     iDestruct "Htree" as (ch) "[_ Htree]".
     by iDestruct (is_hash_len with "Htree") as "%Hlen".
@@ -87,45 +77,12 @@ Proof.
   apply IHl1; eauto with lia.
 Qed.
 
-(* TODO: is this necessary? can we just apply node_hash_len when necessary? *)
-Lemma sep_node_hash_len ct ch :
-  ([∗ list] t;h ∈ ct;ch, is_node_hash t h) -∗
-  ⌜Forall (λ l, length l = 32%nat) ch⌝.
-Proof.
-  iIntros "Htree".
-  iDestruct (big_sepL2_impl _ (λ _ _ h, ⌜length h = 32%nat⌝%I) with "Htree []") as "Hlen_sepL2".
-  {
-    iIntros "!>" (???) "_ _ Hhash".
-    by iDestruct (node_hash_len with "Hhash") as "Hlen".
-  }
-  iDestruct (big_sepL2_const_sepL_r with "Hlen_sepL2") as "[_ %Hlen_sepL1]".
-  iPureIntro.
-  by apply Forall_lookup.
-Qed.
-
-Lemma disj_empty_leaf digest v :
-  is_node_hash Empty digest -∗
-  is_node_hash (Leaf v) digest -∗
-  False.
-Proof.
-  iIntros "Hempty Hleaf".
-  iDestruct (is_hash_inj with "Hempty Hleaf") as "%Heq".
-  iPureIntro.
-  destruct v as [|a]; [naive_solver|].
-  (* TODO: why doesn't list_simplifier or solve_length take care of this? *)
-  apply (f_equal length) in Heq.
-  rewrite length_app in Heq.
-  simpl in *.
-  lia.
-Qed.
-
 (* Ownership of a logical merkle tree. *)
 Definition own_node_except' (recur : option (list w8) -d> loc -d> tree -d> iPropO Σ) : option (list w8) -d> loc -d> tree -d> iPropO Σ :=
   (λ path ptr_tr tr,
     match tr with
     (* We should never have cuts in in-memory trees. *)
     | Cut _ => False
-    | Empty => True
     | Leaf val =>
       ∃ sl_val hash sl_hash,
       "Hval" ∷ own_slice_small sl_val byteT (DfracOwn 1) val ∗
@@ -144,11 +101,15 @@ Definition own_node_except' (recur : option (list w8) -d> loc -d> tree -d> iProp
       "Hptr_children" ∷ ptr_tr ↦[node :: "Children"] (slice_val sl_children) ∗
       "Hchildren" ∷
         ([∗ list] idx ↦ child;ptr_child ∈ children;ptr_children,
-           match path with
-           | Some (a :: path) => if decide (uint.nat a = idx) then ▷ recur (Some path) ptr_child child
-                               else ▷ recur None ptr_child child
-           | None => ▷ recur None ptr_child child
-           | Some [] => ▷ recur None ptr_child child
+           match child with
+           | None => True
+           | Some child =>
+               match path with
+               | Some (a :: path) => if decide (uint.nat a = idx) then ▷ recur (Some path) ptr_child child
+                                   else ▷ recur None ptr_child child
+               | None => ▷ recur None ptr_child child
+               | Some [] => ▷ recur None ptr_child child
+               end
            end
         ) ∗
       "#His_hash" ∷ match path with
@@ -168,22 +129,26 @@ Proof.
   apply (fixpoint_unfold own_node_except').
 Qed.
 
-Definition tree_to_map (tr : tree) : gmap (list w8) (list w8) :=
-  let fix traverse (tr : tree) (acc : gmap (list w8) (list w8)) (id : list w8) :=
-    match tr with
-    | Cut _ => acc
-    | Empty => acc
-    | Leaf val => <[id:=val]>acc
-    | Interior children =>
-      (* Grab all entries from the children, storing the ongoing id. *)
-      (foldr
-        (λ child (pIdxAcc:(Z * gmap (list w8) (list w8))),
-          let acc' := traverse child pIdxAcc.2 (id ++ [W8 pIdxAcc.1])
-          in (pIdxAcc.1 + 1, acc'))
-        (0, acc) children
-      ).2
-    end
-  in traverse tr ∅ [].
+Fixpoint is_tree_lookup (tr : tree) (k : list w8) (v : option (list w8)) : Prop :=
+  match tr with
+  | Cut _ => False
+  | Leaf v' => match k with
+             | [] => v = Some v'
+             | _ => v = None
+             end
+  | Interior children =>
+      match k with
+      | [] => v = None
+      | pos :: k => match (children !! (uint.nat pos)) with
+                  | Some (Some child) => is_tree_lookup child k v
+                  | Some None => v = None
+                  | None => False
+                  end
+      end
+  end.
+
+Definition eq_tree_map (tr : tree) (m : gmap (list w8) (list w8)) : Prop :=
+  ∀ k, is_tree_lookup tr k (m !! k).
 
 Lemma own_node_except_mono path2 path1 root tr :
   match path1, path2 with
@@ -204,14 +169,14 @@ Context `{!heapGS Σ}.
 (* own_merkle denotes ownership of a merkle tree containing some entries. *)
 Definition own_merkle ptr_tr entries : iProp Σ :=
   ∃ tr root,
-  "%Htree" ∷ ⌜tree_to_map tr = entries⌝ ∗
+  "%Htree" ∷ ⌜ eq_tree_map tr entries ⌝ ∗
   "Hnode" ∷ own_node_except None root tr ∗
   "Hroot" ∷ ptr_tr ↦[Tree :: "root"] #root.
 
 (* is_dig says that the tree with these entries has this digest. *)
 Definition is_dig entries dig : iProp Σ :=
   ∃ tr,
-  "%Htree" ∷ ⌜tree_to_map tr = entries⌝ ∗
+  "%Htree" ∷ ⌜ eq_tree_map tr entries ⌝ ∗
   "#Hdig" ∷ is_node_hash tr dig.
 
 Global Instance is_dig_func : Func is_dig.
@@ -223,13 +188,7 @@ Proof. Admitted.
 we use (val : option string) instead of (val : tree) bc there are really
 only two types of nodes we want to allow. *)
 Definition is_merkle_entry id val digest : iProp Σ :=
-  ∃ tr,
-  is_node_hash tr digest ∧
-  ⌜has_entry tr id
-    match val with
-    | None => Empty
-    | Some val' => Leaf val'
-    end⌝.
+  ∃ tr, is_node_hash tr digest ∧ ⌜ is_tree_lookup tr id val ⌝.
 
 (* is_merkle_entry_with_map says that if you know an entry as well
 as the underlying map, you can combine those to get a pure map fact. *)
@@ -237,71 +196,120 @@ Lemma is_merkle_entry_with_map id val dig m :
   is_merkle_entry id val dig -∗ is_dig m dig -∗ ⌜ m !! id = val ⌝.
 Proof. Admitted.
 
-Lemma is_merkle_entry_inj' pos rest val1 val2 digest :
-  is_merkle_entry (pos :: rest) val1 digest -∗
-  is_merkle_entry (pos :: rest) val2 digest -∗
-  ∃ digest',
-  is_merkle_entry rest val1 digest' ∗
-  is_merkle_entry rest val2 digest'.
-Proof.
-  iIntros "Hval1 Hval2".
-  rewrite /is_merkle_entry.
-  iDestruct "Hval1" as (tr1) "[Htree1 %Hcont1]".
-  iDestruct "Hval2" as (tr2) "[Htree2 %Hcont2]".
-  destruct tr1 as [| | |ct1], tr2 as [| | |ct2]; try naive_solver.
-
-  (* Get contains pred and is_node_hash for children. *)
-  destruct Hcont1 as [child1 [Hlist1 Hcont1]].
-  destruct Hcont2 as [child2 [Hlist2 Hcont2]].
-  iDestruct "Htree1" as (ch1) "[Htree1 Hdig1]".
-  iDestruct "Htree2" as (ch2) "[Htree2 Hdig2]".
-  iDestruct (big_sepL2_fmap_l (λ c h, is_node_hash c h) with "Htree1") as "Htree1".
-  iDestruct (big_sepL2_fmap_l (λ c h, is_node_hash c h) with "Htree2") as "Htree2".
-
-  (* Use is_hash ch1/ch2 digest to prove that child hashes are same. *)
-  iDestruct (sep_node_hash_len with "Htree1") as "%Hlen_ch1".
-  iDestruct (sep_node_hash_len with "Htree2") as "%Hlen_ch2".
-
-  iDestruct (is_hash_inj with "Hdig1 Hdig2") as "%Heq".
-  apply app_inv_tail in Heq.
-  assert (ch1 = ch2) as Hch.
-  { apply (concat_len_eq 32); eauto with lia. }
-  subst ch1.
-
-  (* Finish up. *)
-  iDestruct (big_sepL2_lookup_1_some with "Htree1") as (h1) "%Hlook1"; [done|].
-  iDestruct (big_sepL2_lookup_1_some with "Htree2") as (h2) "%Hlook2"; [done|].
-  iDestruct (big_sepL2_lookup with "Htree1") as "Hhash1"; [done..|].
-  iDestruct (big_sepL2_lookup with "Htree2") as "Hhash2"; [done..|].
-  clear Hlook1 Hlook2.
-
-  iFrame "%∗".
-Qed.
-
 Lemma is_merkle_entry_inj id val1 val2 digest :
   is_merkle_entry id val1 digest -∗
   is_merkle_entry id val2 digest -∗
   ⌜val1 = val2⌝.
 Proof.
-  iInduction (id) as [|a] "IH" forall (digest);
-    iIntros "Hpath1 Hpath2".
+  iInduction (id) as [|a] "IH" forall (digest).
   {
+    iIntros "Hval1 Hval2".
     rewrite /is_merkle_entry.
-    iDestruct "Hpath1" as (tr1) "[Htree1 %Hcont1]".
-    iDestruct "Hpath2" as (tr2) "[Htree2 %Hcont2]".
-    destruct tr1 as [| | |ct1], tr2 as [| | |ct2], val1, val2; try naive_solver.
-    { iExFalso. iApply (disj_empty_leaf with "[$] [$]"). }
-    { iExFalso. iApply (disj_empty_leaf with "[$] [$]"). }
-    destruct Hcont1 as [_ Hleaf1].
-    destruct Hcont2 as [_ Hleaf2].
-    inversion Hleaf1; subst l; clear Hleaf1.
-    inversion Hleaf2; subst l0; clear Hleaf2.
-    iDestruct (is_hash_inj with "[$Htree1] [$Htree2]") as "%Heq".
-    by list_simplifier.
+    iDestruct "Hval1" as (tr1) "[Htree1 %Hcont1]".
+    iDestruct "Hval2" as (tr2) "[Htree2 %Hcont2]".
+    simpl in *.
+    destruct tr1, tr2; try done; subst.
+    - iDestruct (is_hash_inj with "[$] [$]") as "%Heq".
+      iPureIntro. by list_simplifier.
+    - simpl. iDestruct "Htree2" as (?) "[? Htree2]".
+      iDestruct (is_hash_inj with "[$] [$]") as "%Heq".
+      exfalso. by list_simplifier.
+    - simpl. iDestruct "Htree1" as (?) "[? Htree1]".
+      iDestruct (is_hash_inj with "[$] [$]") as "%Heq".
+      exfalso. by list_simplifier.
+    - done.
   }
   {
-    iDestruct (is_merkle_entry_inj' with "[$Hpath1] [$Hpath2]") as (digest') "[Hval1 Hval2]".
-    by iSpecialize ("IH" $! digest' with "[$Hval1] [$Hval2]").
+    iIntros "Hval1 Hval2".
+    rewrite /is_merkle_entry.
+    iDestruct "Hval1" as (tr1) "[Htree1 %Hcont1]".
+    iDestruct "Hval2" as (tr2) "[Htree2 %Hcont2]".
+    simpl in *.
+    destruct tr1, tr2; subst; try done.
+    - simpl. iDestruct "Htree2" as (?) "[? Htree2]".
+      iDestruct (is_hash_inj with "[$] [$]") as "%Heq".
+      exfalso. by list_simplifier.
+    - simpl. iDestruct "Htree1" as (?) "[? Htree1]".
+      iDestruct (is_hash_inj with "[$] [$]") as "%Heq".
+      exfalso. by list_simplifier.
+    - simpl.
+      iDestruct "Htree1" as (?) "[Hchildren1 Htree1]".
+      iDestruct "Htree2" as (?) "[Hchildren2 Htree2]".
+      iDestruct (is_hash_inj with "[$] [$]") as "%Heq".
+      list_simplifier.
+      rename H into Heq.
+      iClear "Htree1 Htree2".
+
+      iAssert (⌜ child_hashes0 = child_hashes ⌝)%I with "[-]" as %->.
+      {
+        iApply pure_mono.
+        { by pose proof (and_ind (and_ind (concat_len_eq (32%nat) _ _ Heq))). }
+        iSplit.
+        2:{ word. }
+        iSplit.
+        - rewrite Forall_forall.
+          iIntros (hash Helem_of).
+          clear a Hcont1 Hcont2.
+          apply elem_of_list_lookup_1 in Helem_of as [a Hlookup].
+          iClear "Hchildren1".
+          iDestruct (big_sepL2_lookup_2_some _ _ _ a with "Hchildren2") as %[? Hlookup'].
+          { done. }
+          apply list_lookup_fmap_Some in Hlookup' as (? & Hlookup' & ->).
+          iDestruct (big_sepL2_lookup _ _ _ a with "Hchildren2") as "H".
+          { rewrite list_lookup_fmap Hlookup' //. }
+          { done. }
+          simpl.
+          destruct x0.
+          { by iApply node_hash_len. }
+          { by iApply is_hash_len. }
+        - rewrite Forall_forall.
+          iIntros (hash Helem_of).
+          clear a Hcont1 Hcont2.
+          apply elem_of_list_lookup_1 in Helem_of as [a Hlookup].
+          iClear "Hchildren2".
+          iDestruct (big_sepL2_lookup_2_some _ _ _ a with "Hchildren1") as %[? Hlookup'].
+          { done. }
+          apply list_lookup_fmap_Some in Hlookup' as (? & Hlookup' & ->).
+          iDestruct (big_sepL2_lookup _ _ _ a with "Hchildren1") as "H".
+          { rewrite list_lookup_fmap Hlookup' //. }
+          { done. }
+          simpl.
+          destruct x0.
+          { by iApply node_hash_len. }
+          { by iApply is_hash_len. }
+      }
+      destruct (l !! uint.nat a) eqn:Hlookup; [|done].
+      destruct (l0 !! uint.nat a) eqn:Hlookup0; [|done].
+      iDestruct (big_sepL2_lookup_1_some _ _ _ (uint.nat a) with "Hchildren1") as %[? Hlookup'].
+      { rewrite list_lookup_fmap Hlookup //. }
+      iDestruct (big_sepL2_lookup_1_some _ _ _ (uint.nat a) with "Hchildren2") as %[? Hlookup0'].
+      { rewrite list_lookup_fmap Hlookup0 //. }
+
+
+      iDestruct (big_sepL2_lookup _ _ _ (uint.nat a) with "Hchildren1") as "Hchild1".
+      { rewrite list_lookup_fmap Hlookup //. }
+      { done. }
+      iDestruct (big_sepL2_lookup _ _ _ (uint.nat a) with "Hchildren2") as "Hchild2".
+      { rewrite list_lookup_fmap Hlookup0 //. }
+      { done. }
+      simpl.
+      destruct o, o0; subst.
+      + iApply ("IH" with "[Hchild1] [Hchild2]").
+        { by iFrame. }
+        { by iFrame. }
+      + destruct t.
+        { simpl in *. destruct id; done. }
+        { simpl. iDestruct (is_hash_inj with "[$] [$]") as "%Hbad".
+          apply (f_equal last) in Hbad. rewrite last_snoc //= in Hbad. }
+        { simpl. iDestruct "Hchild1" as (?) "[? ?]". iDestruct (is_hash_inj with "[$] [$]") as "%Hbad".
+          apply (f_equal last) in Hbad. rewrite last_snoc //= in Hbad. }
+      + destruct t.
+        { simpl in *. destruct id; done. }
+        { simpl. iDestruct (is_hash_inj with "[$] [$]") as "%Hbad".
+          apply (f_equal last) in Hbad. rewrite last_snoc //= in Hbad. }
+        { simpl. iDestruct "Hchild2" as (?) "[? ?]". iDestruct (is_hash_inj with "[$] [$]") as "%Hbad".
+          apply (f_equal last) in Hbad. rewrite last_snoc //= in Hbad. }
+      + done.
   }
 Qed.
 
@@ -382,12 +390,13 @@ Lemma wp_Tree_Put ptr_tr entries sl_id id sl_val val d0 d1 :
   }}}
   Tree__Put #ptr_tr (slice_val sl_id) (slice_val sl_val)
   {{{
-    sl_dig dig sl_proof proof (err : bool),
+    sl_dig sl_proof (err : bool),
     RET ((slice_val sl_dig), (slice_val sl_proof), #err);
     "Hid" ∷ own_slice_small sl_id byteT d0 id ∗
     "%Hvalid_id" ∷ ⌜ length id = hash_len → err = false ⌝ ∗
     "Herr" ∷
       if negb err then
+        ∃ dig proof,
         "Htree" ∷ own_merkle ptr_tr (<[id:=val]>entries) ∗
         "Hdig" ∷ own_slice_small sl_dig byteT (DfracOwn 1) dig ∗
         "#HisDig" ∷ is_dig (<[id:=val]>entries) dig ∗
@@ -425,7 +434,7 @@ Proof.
                              ∃ (root : loc) tr,
                                "Hroot" ∷ ptr_tr ↦[Tree::"root"] #root ∗
                                "Hnode" ∷ own_node_except (Some id) root tr ∗
-                               "%Htree" ∷ ⌜ tree_to_map tr = entries ⌝
+                               "%Htree" ∷ ⌜ eq_tree_map tr entries ⌝
               )%I
              with "[Hnode Hroot]").
   {
@@ -445,18 +454,9 @@ Proof.
     2:{ iNamed "Hnode".
         by iDestruct (struct_field_pointsto_not_null with "Hptr_val") as %Hn.
     }
-    2:{ iNamed "Hnode".
-        by iDestruct (struct_field_pointsto_not_null with "Hptr_val") as %Hn.
+    { iNamed "Hnode".
+      by iDestruct (struct_field_pointsto_not_null with "Hptr_val") as %Hn.
     }
-    iClear "Hnode".
-    iIntros (?) "Hnode".
-    iDestruct (struct_fields_split with "Hnode") as "Hnode".
-    iNamed "Hnode".
-    wp_storeField.
-    iFrame.
-    iExists Empty.
-    iSplitL; last done.
-    by iApply own_node_except_unfold.
   }
   iIntros (?) "HifInv".
   wp_pures. clear v.
@@ -464,6 +464,7 @@ Proof.
   { done. }
   iIntros (nodePath_ptr) "HnodePath_ptr".
   wp_pures.
+  clear tr root Htree.
   iNamed "HifInv".
   wp_loadField.
   wp_load.
@@ -477,7 +478,55 @@ Proof.
   { val_ty. }
   iIntros (pathIdx_ptr) "HpathIdx".
   wp_pures.
-  wp_apply (wp_forUpto' with "[$HpathIdx]").
+  set (loopInv :=
+         (λ (i : w64),
+            ∃ (node_ptr : loc) sub_tree sub_map nodePath_sl (nodePath : list loc) currNode,
+              "Hid" ∷ own_slice_small sl_id byteT d0 id ∗
+              "HnodePath_ptr" ∷ nodePath_ptr ↦[slice.T ptrT] (slice_val nodePath_sl) ∗
+              "HnodePath" ∷ own_slice nodePath_sl ptrT (DfracOwn 1) nodePath ∗
+              "Hnode" ∷ own_node_except (Some (drop (uint.nat i) id)) node_ptr sub_tree ∗
+              "%HnodePath_last" ∷ ⌜ last nodePath = Some currNode ⌝ ∗
+              "%HnodePath_length" ∷ ⌜ length nodePath = S (uint.nat i) ⌝ ∗
+              "%Hsubmap" ∷ ⌜ eq_tree_map sub_tree sub_map ⌝ ∗
+              "Hrest" ∷ (∀ sub_tree' ,
+                           ⌜ eq_tree_map sub_tree' (<[id := val]> sub_map) ⌝ -∗
+                           own_node_except (Some (drop (uint.nat i) id)) node_ptr sub_tree' -∗
+                           ∃ tr', own_node_except (Some id) node_ptr tr' ∗
+                                  ⌜ eq_tree_map tr' (<[id := val]> entries) ⌝)
+         )%I).
+  wp_apply (wp_forUpto' loopInv with "[$HpathIdx Hid Hnode HnodePath_ptr HnodePath]").
+  {
+    iSplitR; first word.
+    iFrame. repeat iExists _. iSplitR; first done.
+    iSplitR; first done. iSplitR; first done.
+    iIntros (?). iIntros.
+    iExists _; iFrame. done.
+  }
+  { (* one loop iteration *)
+    clear Φ.
+    iIntros "!# * (H & HpathIdx & %Hlt) HΦ'".
+    iNamed "H".
+    wp_pures. wp_load. wp_load.
+    iDestruct (own_slice_split_1 with "HnodePath") as "[HnodePath HnodePath_cap]".
+    wp_apply (wp_SliceGet with "[$HnodePath]").
+    {
+      iPureIntro.
+      rewrite last_lookup in HnodePath_last.
+      rewrite HnodePath_length /= in HnodePath_last.
+      done.
+    }
+    iIntros "HnodePath".
+    wp_pures.
+    wp_load.
+    opose proof (list_lookup_lt id (uint.nat i) ltac:(word)) as [pos H].
+    wp_apply (wp_SliceGet with "[$Hid //]").
+    iIntros "Hid".
+    wp_pures.
+    iDestruct (own_node_except_unfold with "Hnode") as "Hnode".
+    iNamed "Hnode".
+    (* FIXME: always own node. *)
+    admit.
+  }
 Admitted.
 
 Lemma wp_Tree_Get ptr_tr entries sl_id id d0 :
@@ -512,31 +561,6 @@ Lemma wp_Tree_DeepCopy ptr_tr entries :
   }}}.
 Proof. Admitted.
 
-Lemma wp_node_getHash_null :
-  {{{ True }}}
-  node__getHash #null
-  {{{
-    sl_hash hash, RET (slice_val sl_hash);
-    "Hhash" ∷ own_slice_small sl_hash byteT (DfracOwn 1) hash ∗
-    "#His_hash" ∷ is_node_hash Empty hash
-  }}}.
-Proof.
-  iIntros (Φ) "_ HΦ".
-  rewrite /node__getHash.
-  wp_apply wp_SliceSingleton; [val_ty|];
-    iIntros (sl_data) "Hdata".
-  wp_apply (wp_Hash with "[Hdata]").
-  {
-    iDestruct (slice.own_slice_to_small with "Hdata") as "Hdata".
-    rewrite /own_slice_small.
-    instantiate (1:=[_]).
-    iFrame.
-  }
-  iIntros (??) "H"; iNamed "H".
-  iApply "HΦ".
-  iFrame "#∗".
-Qed.
-
 Lemma wp_isValidHashSl sl_data data :
   {{{
     "#Hdata" ∷ is_Slice2D sl_data data
@@ -550,6 +574,7 @@ Lemma wp_isValidHashSl sl_data data :
   }}}.
 Proof. Admitted.
 
+(*
 Lemma wp_pathProof_check ptr_proof proof val :
   {{{
     "Hproof" ∷ pathProof.own ptr_proof proof ∗
@@ -790,7 +815,7 @@ Proof.
     with (0%nat) by word) in "Hpath_val".
   iEval (rewrite drop_0 Heq_currHash) in "Hpath_val".
   by iApply "HΦ".
-Qed.
+Qed. *)
 
 (* is_merkle_proof says that the merkle proof gives rise to a cut tree
 that has digest dig. and is_merkle_entry id val dig.