update ltac of total

logsem · Feb 6, 2024 · 8bbe5ea · 8bbe5ea
1 parent ecf0a28
commit 8bbe5ea
Show file tree

Hide file tree

Showing 4 changed files with 115 additions and 18 deletions.
diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v
@@ -181,7 +181,7 @@ Section amortized_hash.
   Context `{!ub_clutchGS Σ}.
   Variable val_size:nat.
   Variable max_hash_size : nat.
-  Variable Hineq : (max_hash_size <= (val_size+1))%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.

diff --git a/theories/ub_logic/merkle/merkle_tree.v b/theories/ub_logic/merkle/merkle_tree.v
@@ -276,7 +276,6 @@ Section merkle_tree.
         } 
         wp_apply (wp_insert_amortized with "[$H $Herr']").
         * lia.
-        * lia.
         * by iPureIntro.
         * iIntros (finalhash) "(%m'' & H & %Hmvalid'' & %Hmfound'' & %Hmsize'' & %Hmsubset')".
           iApply "HΦ".
@@ -306,7 +305,6 @@ Section merkle_tree.
         }
         wp_apply (wp_insert_amortized with "[$H $Herr']").
         * lia.
-        * lia.
         * by iPureIntro.
         * iIntros (finalhash) "(%m'' & H & %Hmvalid'' & %Hmfound'' & %Hmsize'' & %Hmsubset')".
           iApply "HΦ".
@@ -353,7 +351,6 @@ Section merkle_tree.
         inversion H. }
       wp_pures. inversion Htvalid; inversion Hvmatch; subst.
       wp_apply (wp_hashfun_prev_amortized with "[$]").
-      + lia.
       + done.
       + iIntros "H". iApply "HΦ"; iFrame.
         done.
@@ -374,7 +371,6 @@ Section merkle_tree.
           apply Z2Nat.inj_pow.
         }
         wp_apply (wp_hashfun_prev_amortized with "H").
-        * lia.
         * done.
         * iIntros "H". iApply "HΦ".
           iFrame. done.
@@ -387,7 +383,6 @@ Section merkle_tree.
           apply Z2Nat.inj_pow.
         }
         wp_apply (wp_hashfun_prev_amortized with "H").
-        * lia.
         * done.
         * iIntros "H". iApply "HΦ".
           iFrame. done.
@@ -472,7 +467,6 @@ Section merkle_tree.
         } 
         wp_apply (wp_insert_amortized with "[$H $Herr']").
         * lia.
-        * lia.
         * by iPureIntro.
         * iIntros (finalhash) "(%m'' & H & %Hmvalid'' & %Hmfound'' & %Hmsize'' & %Hmsubset')".
           iApply "HΦ".
@@ -515,7 +509,6 @@ Section merkle_tree.
         } 
         wp_apply (wp_insert_amortized with "[$H $Herr']").
         * lia.
-        * lia.
         * by iPureIntro.
         * iIntros (finalhash) "(%m'' & H & %Hmvalid'' & %Hmfound'' & %Hmsize'' & %Hmsubset')".
           iApply "HΦ".
@@ -605,7 +598,6 @@ Section merkle_tree.
           }
           wp_apply (wp_insert_amortized with "[$H $Herr']"); try done.
           -- lia.
-          -- lia.
           -- iIntros (retv) "(%m'' & H & %Hmvalid'' & %Hmfound & %Hsize'' & %Hmsubset')".
              iApply "HΦ".
              iExists m''. repeat iSplit; try done.
@@ -646,7 +638,6 @@ Section merkle_tree.
           }
           wp_apply (wp_insert_amortized with "[$H $Herr']"); try done.
           -- lia.
-          -- lia.
           -- iIntros (retv) "(%m'' & H & %Hmvalid'' & %Hmfound & %Hsize'' & %Hmsubset')".
              iApply "HΦ".
              iExists m''. repeat iSplit; try done.
@@ -687,7 +678,6 @@ Section merkle_tree.
           }
           wp_apply (wp_insert_amortized with "[$H $Herr']"); try done.
           -- lia.
-          -- lia.
           -- iIntros (retv) "(%m'' & H & %Hmvalid'' & %Hmfound & %Hsize'' & %Hmsubset')".
              iApply "HΦ".
              iExists m''. repeat iSplit; try done.
@@ -730,7 +720,6 @@ Section merkle_tree.
           } 
           wp_apply (wp_insert_amortized with "[$H $Herr']"); try done.
           -- lia.
-          -- lia.
           -- iIntros (retv) "(%m'' & H & %Hmvalid'' & %Hmfound & %Hsize'' & %Hmsubset')".
              iApply "HΦ".
              iExists m''. repeat iSplit; try done.

diff --git a/theories/ub_logic/merkle/unreliable.v b/theories/ub_logic/merkle/unreliable.v
@@ -37,11 +37,41 @@ Section unreliable_storage.
     rec: "pow" "x":=
       if: "x"=#0 then #1 else #2 * ("pow" ("x"-#1)).
 
+  Lemma pow_spec (n:nat):
+    {{{ True }}}
+      pow #n
+      {{{(x:nat), RET (#x); ⌜x = 2^n⌝ }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ".
+    iLöb as "IH" forall (Φ n).
+    rewrite /pow.
+    wp_pures. rewrite -/pow.
+    case_bool_decide; wp_pures.
+    - iModIntro. replace (1%Z) with (Z.of_nat 1) by lia. iApply "HΦ".
+      iPureIntro. inversion H. assert (n=0) by lia. subst. by simpl.
+    - replace (Z.of_nat n - 1)%Z with (Z.of_nat (n-1)); last first.
+      + rewrite Nat2Z.inj_sub; first lia.
+        destruct n; last lia. done.
+      + wp_apply ("IH"). 
+        iIntros (x) "%".
+        wp_pures.
+        iModIntro.
+        replace (2*_)%Z with (Z.of_nat (2*x)); last first.
+        * rewrite Nat2Z.inj_mul. f_equal.
+        * iApply "HΦ". iPureIntro. subst.
+          rewrite -PeanoNat.Nat.pow_succ_r'. f_equal.
+          destruct n; try done. lia.
+  Qed.
+
+  (* Building the tree*)
   Definition tree_builder_helper : val:=
     rec: "helper" "lhmf" "n" "list":=
       if: "n" = #0
       then
-        let: "head":= list_head "list" in 
+        let: "head":= (match: (list_head "list") with
+                       | SOME "a" => "a"
+                       |NONE => #()
+                       end ) in 
         let: "hash" := "lhmf" "head" in
         let: "l" := unreliable_alloc_program #2 in
         unreliable_write_program "l" "hash";;
@@ -62,8 +92,86 @@ Section unreliable_storage.
   Definition tree_builder : val :=
     λ: "list" "height",
       let: "lhmf" := init_hash val_size_for_hash #() in
-      tree_builder_helper "lhmf" "height" "list"
+      (tree_builder_helper "lhmf" "height" "list", "lhmf")
   .
+
+  Inductive tree_leaf_list: merkle_tree -> list nat -> Prop :=
+  | tree_leaf_list_lf h lf: tree_leaf_list (Leaf h lf) (lf::[])
+  | tree_leaf_list_br a alist b blist h: tree_leaf_list a alist ->
+                       tree_leaf_list b blist ->
+                       tree_leaf_list (Branch h a b) (alist ++ blist).
+
+  Lemma tree_builder_helper_spec (list:list nat) (vlist: val) (height:nat) (m:gmap nat Z) (f:val):
+    size (m) + 2^(S height) - 1 <= max_hash_size ->
+    length list = 2^height ->
+    is_list list vlist ->
+    {{{ hashfun_amortized val_size_for_hash max_hash_size f m ∗
+        ⌜coll_free m⌝ ∗
+        € (nnreal_nat (2^(S height)-1) * amortized_error val_size_for_hash max_hash_size)%NNR
+    }}}
+      tree_builder_helper f #height vlist 
+      {{{ (hash:nat) (l:nat), RET (#hash, #l);
+          ∃ (m':gmap nat Z) (tree:merkle_tree),
+            ⌜m ⊆ m'⌝ ∗
+            ⌜size (m') <= size (m) + 2^(S height) - 1⌝ ∗
+            hashfun_amortized val_size_for_hash max_hash_size f m' ∗
+            ⌜coll_free m'⌝ ∗
+            ⌜tree_leaf_list tree list⌝ ∗
+            ⌜tree_valid val_bit_size height tree m'⌝ ∗
+            ⌜root_hash_value tree = hash ⌝
+      }}}.
+  Proof.
+    iIntros (Hmsize Hlength Hislist Φ) "(H&%Hcollfree&Herr) HΦ".
+    iInduction height as [|] "IH" forall (list vlist m Hmsize Hlength Hislist Φ Hcollfree).
+    - rewrite /tree_builder_helper. wp_pures.
+      assert (∃ x:nat, list = x::[]) as [x ->].
+      { destruct list as [_| x [|]]; first done.
+        - naive_solver.
+        - done.
+      }
+      wp_apply (wp_list_head); first done.
+      iIntros (?) "[[%?]|(%&%&%K&->)]"; first done.
+      inversion K; subst.
+      wp_pures.
+      admit.
+    - admit.
+    Admitted.
+
+  Lemma tree_builder_spec (list:list nat) (vlist: val) (height:nat):
+    2^(S height) - 1  <= max_hash_size ->
+    length list = 2^height ->
+    is_list list vlist ->
+    {{{ 
+          € (nnreal_nat (2^(S height)-1) * amortized_error val_size_for_hash max_hash_size)%NNR
+    }}}
+      tree_builder vlist #height
+      {{{ (hash:nat) (l:nat) (f:val), RET ((#hash, #l), f);
+          ∃ (m:gmap nat Z) (tree:merkle_tree),
+            hashfun_amortized val_size_for_hash max_hash_size f m ∗
+            ⌜tree_valid val_bit_size height tree m⌝ ∗
+            ⌜coll_free m⌝ ∗
+            ⌜size (m) <= 2^(S height) - 1⌝ ∗
+            ⌜tree_leaf_list tree list⌝ ∗
+            ⌜root_hash_value tree = hash ⌝
+      }}}.
+  Proof.
+    iIntros (Hmsize Hlistsize Hislist Φ) "Herr HΦ".
+    rewrite /tree_builder.
+    wp_pures.
+    wp_apply (wp_init_hash_amortized _ max_hash_size); first done.
+    iIntros (f) "H".
+    wp_pures.
+    wp_apply (tree_builder_helper_spec with "[$H $Herr]"); [done|done|done|..].
+    { iPureIntro. intros ???H??. exfalso. destruct H. set_solver. }
+    iIntros (hash l) "(%m'&%tree&%&%&H&%&%&%&%)".
+    wp_pures. iModIntro.
+    iApply "HΦ".
+    iExists m', tree. iFrame.
+    repeat iSplit; done.
+  Qed.
+
+
+
 
 
 

diff --git a/theories/ub_logic/proofmode.v b/theories/ub_logic/proofmode.v
@@ -136,7 +136,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     let e := eval simpl in e in
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
-      (* eapply (tac_twp_pure _ _ _ K e'); *)
+       eapply (tac_twp_pure _ _ K e'); 
       [iSolveTC                       (* PureExec *)
       |try solve_vals_compare_safe    (* The pure condition for PureExec *)
       |wp_finish                      (* new goal *)
@@ -447,7 +447,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     let process_single _ :=
         first
-          [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
+          [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ Htmp K))
           |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
         finish ()
     in process_single ()
@@ -472,7 +472,7 @@ Tactic Notation "wp_load" :=
     |wp_finish]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ _ K))
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
     [solve_mapsto ()
     |wp_finish]
@@ -494,7 +494,7 @@ Tactic Notation "wp_store" :=
     |pm_reduce; first [wp_seq|wp_finish]]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ K))
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ K))
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [solve_mapsto ()
     |pm_reduce; first [wp_seq|wp_finish]]