From 306d8485d852eb424437e60790d3efa45f0be789 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 2 Feb 2024 17:11:52 +0100 Subject: [PATCH] Add lemma for incorrect proof but correct leaf --- theories/ub_logic/merkle_tree.v | 213 +++++++++++++++++++++++++++++++- 1 file changed, 210 insertions(+), 3 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 282e4a13..ec564d70 100644 --- 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 :=