Add lemma for incorrect proof but correct leaf

logsem · Feb 2, 2024 · 306d848 · 306d848
1 parent c57e605
commit 306d848
Showing 1 changed file with 210 additions and 3 deletions.
diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v
@@ -163,6 +163,131 @@ Section merkle_tree.
       + inversion H14; inversion H9; subst. done.
       + inversion H9; inversion H14; subst. eapply IHtree2; try done.
   Qed.
+
+  Lemma wp_compute_hash_from_leaf_size (n:nat) (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E:
+    {{{ ⌜tree_relate n ltree tree⌝ ∗
+        ⌜tree_valid tree m⌝ ∗
+        hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗
+        ⌜is_list proof lproof⌝ ∗
+        ⌜possible_proof tree proof⌝ ∗
+        ⌜map_valid m⌝ ∗
+        ⌜ size m + (S n) <= max_hash_size⌝ ∗
+        € (nnreal_nat (S n) * amortized_error (val_size_for_hash)%nat max_hash_size)%NNR 
+     }}}
+      compute_hash_from_leaf f lproof (#v) @ E
+      {{{ (retv:Z), RET #retv;
+          ∃ m', ⌜m ⊆ m'⌝ ∗
+                hashfun_amortized (val_size_for_hash) max_hash_size f m' ∗
+                ⌜map_valid m'⌝ ∗
+                ⌜size (m') <= size m + (S n)⌝ ∗
+                ⌜(0 <= retv < 2^val_bit_size)%Z⌝
+      }}}.
+  Proof.
+    iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hproof & %Hposs & %Hmvalid & %Hmsize &Herr) HΦ".
+    iInduction tree as [hash leaf|hash tree1 Htree1 tree2 Htree2] "IH"
+                         forall (n ltree v m proof lproof Φ
+                              Htrelate Htvalid Hproof Hposs Hmsize Hmvalid).
+    - rewrite /compute_hash_from_leaf. wp_pures. rewrite -/compute_hash_from_leaf.
+      wp_apply (wp_list_head); first done.
+      iIntros (?) "[[->->]|(%&%&%&%)]"; last first.
+      { inversion Hposs; subst. done. }
+      wp_pures. inversion Htrelate; subst.
+      wp_apply (wp_insert_amortized with "[$H Herr]"); try lia.
+      + iSplit; try done. iApply ec_spend_irrel; last done.
+        simpl. lra.
+      + iIntros (retv) "(%m' & H & %Hmvalid' & %Hfound & %Hmsize' & %Hmsubset)".
+        iApply ("HΦ" with "[H]").
+        iExists _; repeat iSplit; try done.
+        * iPureIntro; lia.
+        * rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+          iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done.
+          lia.
+        * rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+          iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. 
+          rewrite /val_size_for_hash in Hforall. destruct Hforall as [? H1].
+          apply Zle_lt_succ in H1.
+          eapply Z.lt_stepr; try done.
+          rewrite -Nat2Z.inj_succ. replace (2)%Z with (Z.of_nat 2) by lia.
+          rewrite -Nat2Z.inj_pow. f_equal.
+          assert (1<=2 ^val_bit_size); last lia. clear.
+          induction val_bit_size; simpl; lia.
+    - rewrite /compute_hash_from_leaf. wp_pures. rewrite -/compute_hash_from_leaf.
+      wp_apply wp_list_head; first done.
+      iIntros (?) "[[->->]|(%head & %lproof' & -> & ->)]".
+      { inversion Hposs. }
+      wp_pures. wp_apply wp_list_tail; first done.
+      iIntros (proof') "%Hproof'".
+      wp_pures. 
+      inversion Htrelate; subst.
+      iAssert (€ ((nnreal_nat (S n0) * amortized_error val_size_for_hash max_hash_size)%NNR) ∗
+               € (amortized_error val_size_for_hash max_hash_size)%NNR)%I with "[Herr]" as "[Herr Herr']".
+      { iApply ec_split. iApply (ec_spend_irrel with "[$]").
+        simpl. lra.
+      }
+      wp_pures.
+      inversion Hposs; inversion Htvalid; subst; wp_pures; try done.
+      + wp_apply ("IH" with "[][][][][][][$H][$Herr]"); try done.
+        { iPureIntro; lia. }
+        iIntros (lefthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashsize')".
+        wp_pures.
+        replace (_*_+_)%Z with (Z.of_nat (Z.to_nat lefthash' * 2 ^ val_bit_size + hash0)); last first.
+        { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul.
+          rewrite Z2Nat.id; last lia. f_equal.
+          rewrite Z2Nat.inj_pow. f_equal.
+        } 
+        wp_apply (wp_insert_amortized with "[$H $Herr']").
+        * lia.
+        * lia.
+        * by iPureIntro.
+        * iIntros (finalhash) "(%m'' & H & %Hmvalid'' & %Hmfound'' & %Hmsize'' & %Hmsubset')".
+          iApply "HΦ".
+          iExists m''. repeat iSplit.
+          -- iPureIntro; etrans; exact.
+          -- done.
+          -- by iPureIntro.
+          -- iPureIntro; lia.
+          -- rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+             iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. lia.
+          -- rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+             iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. 
+             rewrite /val_size_for_hash in Hforall. destruct Hforall as [? K].
+             apply Zle_lt_succ in K.
+             eapply Z.lt_stepr; try done.
+             rewrite -Nat2Z.inj_succ. replace (2)%Z with (Z.of_nat 2) by lia.
+             rewrite -Nat2Z.inj_pow. f_equal.
+             assert (1<=2 ^val_bit_size); last lia. clear.
+             induction val_bit_size; simpl; lia.        
+      + wp_apply ("IH1" with "[][][][][][][$H][$Herr]"); try done.
+        { iPureIntro; lia. }
+        iIntros (lefthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashsize')".
+        wp_pures.
+        replace (_*_+_)%Z with (Z.of_nat (hash0 * 2 ^ val_bit_size + Z.to_nat lefthash')); last first.
+        { rewrite Nat2Z.inj_add. f_equal; last lia. rewrite Nat2Z.inj_mul. f_equal.
+          apply Z2Nat.inj_pow.
+        }
+        wp_apply (wp_insert_amortized with "[$H $Herr']").
+        * lia.
+        * lia.
+        * by iPureIntro.
+        * iIntros (finalhash) "(%m'' & H & %Hmvalid'' & %Hmfound'' & %Hmsize'' & %Hmsubset')".
+          iApply "HΦ".
+          iExists m''. repeat iSplit.
+          -- iPureIntro; etrans; exact.
+          -- done.
+          -- by iPureIntro.
+          -- iPureIntro; lia.
+          -- rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+             iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. lia.
+          -- rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+             iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. 
+             rewrite /val_size_for_hash in Hforall. destruct Hforall as [? K].
+             apply Zle_lt_succ in K.
+             eapply Z.lt_stepr; try done.
+             rewrite -Nat2Z.inj_succ. replace (2)%Z with (Z.of_nat 2) by lia.
+             rewrite -Nat2Z.inj_pow. f_equal.
+             assert (1<=2 ^val_bit_size); last lia. clear.
+             induction val_bit_size; simpl; lia.        
+  Qed.
 
   (** Spec *)
   Lemma wp_compute_hash_from_leaf_correct (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E:
@@ -430,7 +555,47 @@ Section merkle_tree.
         simpl. lra.
       }
       inversion Hposs; inversion Hvmatch; inversion Htvalid; inversion Hincorrect; subst; wp_pures; try done.
-      + (*right neq guess right*) admit.
+      + (*right neq guess right*)
+        wp_apply (wp_compute_hash_from_leaf_size with "[$H $Herr]").
+        * repeat iSplit; last first; iPureIntro; try done. lia.
+        * iIntros (lefthash) "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashsize)".
+          wp_pures.
+          replace (_*_+_)%Z with (Z.of_nat (Z.to_nat lefthash * 2 ^ val_bit_size + hash)); last first.
+          { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul.
+            rewrite Z2Nat.id; last lia. f_equal.
+            rewrite Z2Nat.inj_pow. f_equal.
+          }
+          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.
+             ++ iPureIntro; etrans; exact.
+             ++ iPureIntro; lia.
+             ++ iPureIntro. simpl. intros ->. 
+                inversion H27; subst.
+                assert (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2 =
+                        Z.to_nat lefthash * 2 ^ val_bit_size + hash) as helper.
+                { eapply (coll_free_lemma m''); try done.
+                  eapply lookup_weaken; first done.
+                  etrans; exact.
+                }
+                epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit Hsplit']; subst. done.
+                Unshelve.
+                ** by inversion H19.
+                ** by inversion Hposs. 
+             ++ rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+                iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. lia.
+             ++  rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+                 iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. 
+                 rewrite /val_size_for_hash in Hforall. destruct Hforall as [? K].
+                 apply Zle_lt_succ in K.
+                 eapply Z.lt_stepr; try done.
+                 rewrite -Nat2Z.inj_succ. replace (2)%Z with (Z.of_nat 2) by lia.
+                 rewrite -Nat2Z.inj_pow. f_equal.
+                 assert (1<=2 ^val_bit_size); last lia. clear.
+                 induction val_bit_size; simpl; lia. 
       + (*incorrect happens above*)
         wp_apply ("IH" with "[][][][][][][][][$H][$Herr]"); try done.
         * iPureIntro; lia.
@@ -473,7 +638,49 @@ Section merkle_tree.
                  rewrite -Nat2Z.inj_pow. f_equal.
                  assert (1<=2 ^val_bit_size); last lia. clear.
                  induction val_bit_size; simpl; lia. 
-      + (*left neq guess left *) admit.
+      + (*left neq guess left *)
+        wp_apply (wp_compute_hash_from_leaf_size with "[$H $Herr]").
+        * repeat iSplit; last first; iPureIntro; try done. lia.
+        * iIntros (righthash) "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hrighthashsize)".
+          wp_pures.
+          replace (_*_+_)%Z with (Z.of_nat (hash * 2 ^ val_bit_size + Z.to_nat righthash )); last first.
+          { rewrite Nat2Z.inj_add. f_equal; last lia. rewrite Nat2Z.inj_mul. f_equal.
+            rewrite Z2Nat.inj_pow. f_equal.
+          }
+          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.
+             ++ iPureIntro; etrans; exact.
+             ++ iPureIntro; lia.
+             ++ iPureIntro. simpl. intros ->. 
+                inversion H27; subst.
+                assert (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2 =
+                        hash * 2 ^ val_bit_size + Z.to_nat righthash) as helper.
+                { eapply (coll_free_lemma m''); try done.
+                  eapply lookup_weaken; first done.
+                  etrans; exact.
+                }
+                epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit Hsplit']; subst. done.
+                Unshelve.
+                ** by inversion H19.
+                ** destruct Hrighthashsize as [Hrighthashsize Hrighthashsize'].
+                   rewrite Nat2Z.inj_lt. rewrite Z2Nat.inj_pow.
+                   replace (Z.of_nat 2) with 2%Z by lia.
+                   rewrite Z2Nat.id; lia.
+             ++ rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+                iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. lia.
+             ++  rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)".
+                 iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. 
+                 rewrite /val_size_for_hash in Hforall. destruct Hforall as [? K].
+                 apply Zle_lt_succ in K.
+                 eapply Z.lt_stepr; try done.
+                 rewrite -Nat2Z.inj_succ. replace (2)%Z with (Z.of_nat 2) by lia.
+                 rewrite -Nat2Z.inj_pow. f_equal.
+                 assert (1<=2 ^val_bit_size); last lia. clear.
+                 induction val_bit_size; simpl; lia. 
       + (*incorrect happens above *)
         wp_apply ("IH1" with "[][][][][][][][][$H][$Herr]"); try done.
         * iPureIntro; lia.
@@ -518,7 +725,7 @@ Section merkle_tree.
                  rewrite -Nat2Z.inj_pow. f_equal.
                  assert (1<=2 ^val_bit_size); last lia. clear.
                  induction val_bit_size; simpl; lia. 
-    Admitted.
+  Qed.
 
   (** checker*)
   Definition merkle_tree_decider_program : val :=