Spec for writing a tree into unreliable memory

theories/ub_logic/lib/list.v

@@ -949,6 +949,37 @@ Section list_specs.
       + iApply "HΦ"; iPureIntro.
         simpl. rewrite HP. done.
   Qed.
+
+
+  Lemma wp_list_split E (n:nat) (lv:val) l:
+    {{{ ⌜is_list l lv⌝ ∗ ⌜n<=length l⌝ }}}
+      list_split #n lv @ E
+      {{{ a b, RET (a, b)%V;
+          ∃ l1 l2, ⌜is_list l1 a⌝ ∗ ⌜is_list l2 b⌝ ∗ ⌜l=l1++l2⌝ ∗ ⌜length (l1) = n⌝
+      }}}.
+  Proof.
+    revert lv l.
+    induction n;
+      iIntros (lv l Φ) "[%Hlist %Hlength] HΦ".
+    - rewrite /list_split. wp_pures. iModIntro. iApply "HΦ".
+      iExists [], l.
+      repeat iSplit; by iPureIntro.
+    - rewrite /list_split. wp_pures. rewrite -/list_split.
+      destruct l.
+      { simpl in Hlength. lia. }
+      destruct Hlist as [?[-> Hlist]].
+      wp_pures. replace (Z.of_nat (S n) - 1)%Z with (Z.of_nat n) by lia.
+      wp_apply IHn.
+      + iSplit; iPureIntro; try done. simpl in Hlength. lia.
+      + iIntros (??) "(%l1 & %l2 &%&%&%&%)".
+        wp_pures.
+        wp_apply wp_list_cons; first done.
+        iIntros. wp_pures. iApply "HΦ".
+        iExists (_::l1), l2.
+        iModIntro; repeat iSplit; iPureIntro; try done.
+        * set_solver.
+        * set_solver.
+  Qed.
 End list_specs.
 
 Global Arguments wp_list_nil : clear implicits.
@@ -1268,4 +1299,5 @@ Section list_specs_extra.
   Qed.
 
 
+
 End list_specs_extra.

theories/ub_logic/merkle/merkle_tree.v

@@ -6,7 +6,7 @@ Open Scope nat.
 Section merkle_tree.
   (*val_bit_size is a positive integer, 
     referring to the bit size of the return value of the hash function
-    Therefore all hashes are smalelr than 2 ^ val_bit_size
+    Therefore all hashes are smaller than 2 ^ val_bit_size
     val_bit_size_for_hash is one smaller than 2^val_bit_size since the spec for hash
     adds one to that value implicitly (to ensure positive codomain size)
     Leaf bit size is fixed to be twice of val_bit_size.
@@ -22,7 +22,7 @@ Section merkle_tree.
   Variables max_hash_size : nat.
   Definition val_bit_size : nat := S val_bit_size'.
   Definition val_size_for_hash:nat := (2^val_bit_size)-1.
-  Variable (Hineq: (max_hash_size <= val_size_for_hash)%nat).
+  (* Variable (Hineq: (max_hash_size <= val_size_for_hash)%nat). *)
   Definition leaf_bit_size : nat := 2*val_bit_size.
   (* Definition identifier : nat := 2^leaf_bit_size. *)
   Definition num_of_leafs : nat := 2^height.
@@ -761,17 +761,10 @@ Section merkle_tree.
          "correct_root_hash" = compute_hash_from_leaf "lhmf" "lproof" "lleaf"
       ).
 
-  Lemma merkle_tree_decider_program_spec tree (m:gmap nat Z) f:
-    {{{ ⌜tree_valid height tree m⌝ ∗
-        hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗
-        ⌜map_valid m⌝ 
-    }}} merkle_tree_decider_program #(root_hash_value tree) f
-    {{{
-          (checker:val), RET checker;
-          hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗
-          (∀ lproof proof v m',
+  Definition decider_program_helper_spec (checker:val) (tree:merkle_tree) (f:val) : iProp Σ:=
+    (∀ lproof proof v m',
              {{{
-                  ⌜m⊆m'⌝ ∗
+                  ⌜tree_valid height tree m'⌝ ∗
                   hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' ∗
                   ⌜is_list proof lproof⌝ ∗
                   ⌜possible_proof tree proof ⌝∗
@@ -794,7 +787,17 @@ Section merkle_tree.
                         hashfun_amortized (val_size_for_hash) max_hash_size f m'' ∗
                         ⌜map_valid m''⌝ ∗
                         ⌜size (m'') <= size m' + (S height)⌝ 
-          }}} )
+          }}} )%I.
+
+  Lemma merkle_tree_decider_program_spec tree (m:gmap nat Z) f:
+    {{{ ⌜tree_valid height tree m⌝ ∗
+        hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗
+        ⌜map_valid m⌝ 
+    }}} merkle_tree_decider_program #(root_hash_value tree) f
+    {{{
+          (checker:val), RET checker;
+          hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗
+          decider_program_helper_spec checker tree f
     }}}.
   Proof.
     iIntros (Φ) "(%Htvalid & H & %Hmvalid) IH".
@@ -808,7 +811,6 @@ Section merkle_tree.
     - destruct (@decide (correct_proof tree proof) (make_decision (correct_proof tree proof))) as [K|K].
       + wp_apply (wp_compute_hash_from_leaf_correct with "[$H]").
         * repeat iSplit; try done; iPureIntro.
-          -- by eapply tree_valid_superset.
           -- by subst.
         * iIntros (?) "(H&%)".
           wp_pures. subst. case_bool_decide; last done.
@@ -817,7 +819,6 @@ Section merkle_tree.
       + epose proof (proof_not_correct_implies_incorrect _ _ _ K).
         wp_apply (wp_compute_hash_from_leaf_incorrect_proof with "[$H $Herr]").
         * repeat iSplit; try done; iPureIntro.
-          -- by eapply tree_valid_superset.
           -- by subst.
         * iIntros (?) "(%&%&H&%&%&%&%)".
           wp_pures.
@@ -828,7 +829,7 @@ Section merkle_tree.
           -- iPureIntro. naive_solver.
           -- iExists _; by repeat iSplit.
     - wp_apply (wp_compute_hash_from_leaf_incorrect with "[$H $Herr]").
-      + repeat iSplit; try done. iPureIntro. by eapply tree_valid_superset.
+      + repeat iSplit; done. 
       + iIntros (?) "(%&%&H&%&%&%&%)".
         wp_pures. rewrite bool_decide_eq_false_2; last first.
         { intros K. inversion K. by subst. }