From 4b05c4e0294b988d4fcdb9da8ca4be799f378319 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 29 Jan 2024 13:48:07 +0100 Subject: [PATCH 01/21] Amortized hash non resizing --- theories/ub_logic/hash.v | 188 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v index c12163fad..cd98d6d60 100644 --- a/theories/ub_logic/hash.v +++ b/theories/ub_logic/hash.v @@ -1,4 +1,5 @@ From clutch.ub_logic Require Export ub_clutch lib.map. +Import Hierarchy. Set Default Proof Using "Type*". Module simple_bit_hash. @@ -160,5 +161,192 @@ Module simple_bit_hash. apply (Forall_map (λ p : nat * Z, p.2)) in HForall; auto. Qed. + Section amortized. + Variable max_hash_size : nat. + Variable Hineq : max_hash_size <= (val_size+1). + Program Definition amortized_error : nonnegreal := + mknonnegreal ((max_hash_size + 1)/(2*(val_size + 1)))%R _. + Next Obligation. + pose proof (pos_INR val_size) as H. + pose proof (pos_INR max_hash_size) as H'. + apply Rcomplements.Rdiv_le_0_compat; lra. + Qed. + Definition hashfun_amortized f m : iProp Σ := + ∃ (hm : loc) (k : nat) (ε : nonnegreal), + ⌜ f = compute_hash_specialized #hm ⌝ ∗ + ⌜k = size m⌝ ∗ + ⌜ (ε.(nonneg) = (((max_hash_size + 1) * k)/2 - sum_n_m (λ x, INR x) 0%nat (k-1)) / (val_size + 1))%R⌝ ∗ + € ε ∗ + map_list hm ((λ b, LitV (LitInt b)) <$> m) + . + + #[global] Instance timeless_hashfun_amortized f m : + Timeless (hashfun_amortized f m). + Proof. apply _. Qed. + + Lemma wp_init_hash_amortized E : + {{{ True }}} + init_hash #() @ E + {{{ f, RET f; hashfun_amortized f ∅ }}}. + Proof. + rewrite /init_hash. + iIntros (Φ) "_ HΦ". + wp_pures. rewrite /init_hash_state. + wp_apply (wp_init_map with "[//]"). + iIntros (?) "Hm". wp_pures. + rewrite /compute_hash. wp_pures. + iApply "HΦ". iExists _. rewrite fmap_empty. iFrame. + iMod ec_zero. + iModIntro. iExists 0%nat, nnreal_zero. + repeat (iSplit; [done|]). iFrame. + iPureIntro. + simpl. + replace (sum_n_m _ _ _) with 0; first lra. + rewrite sum_n_n. by simpl. + Qed. + + Lemma wp_hashfun_prev_amortized E f m (n : nat) (b : Z) : + m !! n = Some b → + {{{ hashfun_amortized f m }}} + f #n @ E + {{{ RET #b; hashfun_amortized f m }}}. + Proof. + iIntros (Hlookup Φ) "Hhash HΦ". + iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". + wp_apply (wp_hashfun_prev with "[H]"); first done. + - iExists _. by iFrame. + - iIntros "(%&%&H)". iApply "HΦ". + iExists _,_,_. by iFrame. + Qed. + + Lemma hashfun_amortized_hashfun f m: ⊢ hashfun_amortized f m -∗ hashfun f m. + Proof. + iIntros "(%&%&%&->&->&%&He&H)". + iExists _; by iFrame. + Qed. + + Lemma amortized_inequality (k : nat): + (k <= max_hash_size)%nat -> + 0 <= ((max_hash_size + 1) * k / 2 - sum_n_m (λ x : nat, INR x) 0 (k - 1)) / (val_size + 1). + Proof. + intros H. + pose proof (pos_INR max_hash_size) as H1. + pose proof (pos_INR val_size) as H2. + pose proof (pos_INR k) as H3. + apply Rcomplements.Rdiv_le_0_compat; last lra. + assert (sum_n_m (λ x : nat, INR x) 0 (k - 1) = (k-1)*k/2) as ->. + - clear. + induction k. + + simpl. rewrite sum_n_n. + rewrite Rmult_0_r. by assert (0/2 = 0) as -> by lra. + + clear. induction k. + * simpl. rewrite sum_n_n. + replace (_-_) with 0 by lra. + rewrite Rmult_0_l. by assert (0/2 = 0) as -> by lra. + * assert (S (S k) - 1 = S (S k - 1))%nat as -> by lia. + rewrite sum_n_Sm; last lia. + rewrite IHk. + replace (plus _ _) with (((S k - 1) * S k / 2) + (S (S k - 1))) by done. + assert (∀ k, (INR (S k) - 1) = (INR k)) as H'. + { intros. simpl. case_match; first replace (1 - 1) with 0 by lra. + - done. + - by replace (_+1-1) with (INR (S n)) by lra. + } + rewrite !H'. + replace (S k - 1)%nat with (k)%nat by lia. + assert (k * (S k) + S k + S k = S k * S (S k)); last lra. + assert (k * S k + S k + S k = S k * (k+1+1)) as ->; try lra. + assert (k+1+1 = S (S k)). + -- rewrite !S_INR. lra. + -- by rewrite H. + - rewrite -!Rmult_minus_distr_r. + apply Rcomplements.Rdiv_le_0_compat; try lra. + apply Rmult_le_pos; try lra. + assert (INR k <= INR max_hash_size); try lra. + by apply le_INR. + Qed. + + + Lemma wp_insert_no_coll_amortized E f m (n : nat) (z : Z) : + m !! n = None → + (size m < max_hash_size)%nat -> + {{{ hashfun_amortized f m ∗ € amortized_error ∗ + ⌜coll_free m⌝ }}} + f #n @ E + {{{ (v : Z), RET #v; hashfun_amortized f (<[ n := v ]>m) ∗ ⌜coll_free (<[ n := v ]>m)⌝ }}}. + Proof. + iIntros (Hlookup Hsize Φ) "(Hhash & Herr & %Hcoll) HΦ". + iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". + iAssert (€ (nnreal_div (nnreal_nat (size m)) (nnreal_nat (val_size + 1))) ∗ + € (mknonnegreal (((max_hash_size + 1) * size (<[n:=0%Z]> m) / 2 - sum_n_m (λ x, INR x) 0%nat (size (<[n:=0%Z]> m) - 1)) / (val_size + 1)) _ ) + )%I with "[Hε Herr]" as "[Hε Herr]". + - iApply ec_split. + iCombine "Hε Herr" as "H". + iApply (ec_spend_irrel with "[$]"). + simpl. rewrite H. rewrite map_size_insert_None; [|done]. + remember (size m) as k. + remember (val_size + 1) as v. + remember (max_hash_size) as h. + assert (∀ x y, x/y = x*/y) as Hdiv. + { intros. lra. } + destruct k. + + simpl. rewrite sum_n_n. rewrite Rmult_0_l Rmult_0_r. + replace (INR 0%nat) with 0; last done. + rewrite !Rminus_0_r. + replace (0/_/_) with 0; last lra. + rewrite !Rplus_0_l. + rewrite Rmult_1_r. + rewrite !Hdiv. + rewrite Rinv_mult. + lra. + + assert (forall k, S k - 1 = k)%nat as H' by lia. + rewrite !H'. + clear H'. + rewrite sum_n_Sm; last lia. + replace (plus _ (INR (S k))) with ((sum_n_m (λ x : nat, INR x) 0 k) + (S k)) by done. + rewrite !Hdiv. + rewrite !Rmult_minus_distr_r. + rewrite (Rmult_plus_distr_r (sum_n_m _ _ _)). + rewrite -!Rplus_assoc. + rewrite Ropp_plus_distr. + rewrite -!Rplus_assoc. + assert ((h + 1) * S k * / 2 * / v+ (h + 1) * / (2 * v) = S k * / (val_size + 1)%nat + (h + 1) * S (S k) * / 2 * / v + - (S k * / v)); try lra. + replace (INR((_+_)%nat)) with v; last first. + { rewrite Heqv. rewrite -S_INR. f_equal. lia. } + assert ( (h + 1) * S k * / 2 * / v + (h + 1) * / (2 * v) = (h + 1) * S (S k) * / 2 * / v); try lra. + replace (_*_*_*_) with ((h+1) * (S k) * /(2*v)); last first. + { rewrite Rinv_mult. lra. } + replace (_*_*_*_) with ((h+1) * (S(S k)) * /(2*v)); last first. + { rewrite Rinv_mult. lra. } + rewrite -Rdiv_plus_distr. + rewrite Hdiv. + f_equal. + rewrite -{2}(Rmult_1_r (h+1)). + rewrite -Rmult_plus_distr_l. + f_equal. + - wp_apply (wp_insert_no_coll with "[H Hε]"); [done|done|..]. + + iFrame. iSplitL; try done. + iExists _. by iFrame. + + iIntros (v) "[H %]". + iApply "HΦ". + iSplitL; last done. + iExists _, _, _. iFrame. + repeat (iSplitR); try done. + * iPureIntro. simpl. do 3 f_equal. + all: by repeat rewrite map_size_insert. + * iDestruct "H" as "[% [% H]]". + inversion H1; subst. + iFrame. + Unshelve. + apply amortized_inequality. + rewrite map_size_insert. + case_match => /=; lia. + Qed. + + End amortized. + + End simple_bit_hash. + + From 25bdb1e378515dca5d73d3881062231face248d4 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 30 Jan 2024 10:42:27 +0100 Subject: [PATCH 02/21] amortized hash spec now uses spec of non-amortized --- theories/ub_logic/hash.v | 360 ++++++++++++++++++++------------------- 1 file changed, 181 insertions(+), 179 deletions(-) diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v index cd98d6d60..f64e9ed2e 100644 --- a/theories/ub_logic/hash.v +++ b/theories/ub_logic/hash.v @@ -2,7 +2,7 @@ From clutch.ub_logic Require Export ub_clutch lib.map. Import Hierarchy. Set Default Proof Using "Type*". -Module simple_bit_hash. +Section simple_bit_hash. Context `{!ub_clutchGS Σ}. @@ -161,192 +161,194 @@ Module simple_bit_hash. apply (Forall_map (λ p : nat * Z, p.2)) in HForall; auto. Qed. - Section amortized. - Variable max_hash_size : nat. - Variable Hineq : max_hash_size <= (val_size+1). - Program Definition amortized_error : nonnegreal := - mknonnegreal ((max_hash_size + 1)/(2*(val_size + 1)))%R _. - Next Obligation. - pose proof (pos_INR val_size) as H. - pose proof (pos_INR max_hash_size) as H'. - apply Rcomplements.Rdiv_le_0_compat; lra. - Qed. - - Definition hashfun_amortized f m : iProp Σ := - ∃ (hm : loc) (k : nat) (ε : nonnegreal), - ⌜ f = compute_hash_specialized #hm ⌝ ∗ - ⌜k = size m⌝ ∗ - ⌜ (ε.(nonneg) = (((max_hash_size + 1) * k)/2 - sum_n_m (λ x, INR x) 0%nat (k-1)) / (val_size + 1))%R⌝ ∗ - € ε ∗ - map_list hm ((λ b, LitV (LitInt b)) <$> m) - . + +End simple_bit_hash. - #[global] Instance timeless_hashfun_amortized f m : - Timeless (hashfun_amortized f m). - Proof. apply _. Qed. - Lemma wp_init_hash_amortized E : - {{{ True }}} - init_hash #() @ E - {{{ f, RET f; hashfun_amortized f ∅ }}}. - Proof. - rewrite /init_hash. - iIntros (Φ) "_ HΦ". - wp_pures. rewrite /init_hash_state. - wp_apply (wp_init_map with "[//]"). - iIntros (?) "Hm". wp_pures. - rewrite /compute_hash. wp_pures. - iApply "HΦ". iExists _. rewrite fmap_empty. iFrame. - iMod ec_zero. - iModIntro. iExists 0%nat, nnreal_zero. - repeat (iSplit; [done|]). iFrame. - iPureIntro. - simpl. - replace (sum_n_m _ _ _) with 0; first lra. - rewrite sum_n_n. by simpl. - Qed. - Lemma wp_hashfun_prev_amortized E f m (n : nat) (b : Z) : - m !! n = Some b → - {{{ hashfun_amortized f m }}} - f #n @ E - {{{ RET #b; hashfun_amortized f m }}}. - Proof. - iIntros (Hlookup Φ) "Hhash HΦ". - iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". - wp_apply (wp_hashfun_prev with "[H]"); first done. - - iExists _. by iFrame. - - iIntros "(%&%&H)". iApply "HΦ". - iExists _,_,_. by iFrame. - Qed. +Section amortized_hash. + Context `{!ub_clutchGS Σ}. + Variable val_size:nat. + Variable max_hash_size : nat. + Variable Hineq : max_hash_size <= (val_size+1). + Program Definition amortized_error : nonnegreal := + mknonnegreal ((max_hash_size + 1)/(2*(val_size + 1)))%R _. + Next Obligation. + pose proof (pos_INR val_size) as H. + pose proof (pos_INR max_hash_size) as H'. + apply Rcomplements.Rdiv_le_0_compat; lra. + Qed. + + Definition hashfun_amortized f m : iProp Σ := + ∃ (hm : loc) (k : nat) (ε : nonnegreal), + ⌜ f = compute_hash_specialized val_size #hm ⌝ ∗ + ⌜k = size m⌝ ∗ + ⌜ (ε.(nonneg) = (((max_hash_size + 1) * k)/2 - sum_n_m (λ x, INR x) 0%nat (k-1)) / (val_size + 1))%R⌝ ∗ + € ε ∗ + map_list hm ((λ b, LitV (LitInt b)) <$> m) + . - Lemma hashfun_amortized_hashfun f m: ⊢ hashfun_amortized f m -∗ hashfun f m. - Proof. - iIntros "(%&%&%&->&->&%&He&H)". - iExists _; by iFrame. - Qed. + #[global] Instance timeless_hashfun_amortized f m : + Timeless (hashfun_amortized f m). + Proof. apply _. Qed. - Lemma amortized_inequality (k : nat): - (k <= max_hash_size)%nat -> - 0 <= ((max_hash_size + 1) * k / 2 - sum_n_m (λ x : nat, INR x) 0 (k - 1)) / (val_size + 1). - Proof. - intros H. - pose proof (pos_INR max_hash_size) as H1. - pose proof (pos_INR val_size) as H2. - pose proof (pos_INR k) as H3. - apply Rcomplements.Rdiv_le_0_compat; last lra. - assert (sum_n_m (λ x : nat, INR x) 0 (k - 1) = (k-1)*k/2) as ->. - - clear. - induction k. - + simpl. rewrite sum_n_n. - rewrite Rmult_0_r. by assert (0/2 = 0) as -> by lra. - + clear. induction k. - * simpl. rewrite sum_n_n. - replace (_-_) with 0 by lra. - rewrite Rmult_0_l. by assert (0/2 = 0) as -> by lra. - * assert (S (S k) - 1 = S (S k - 1))%nat as -> by lia. - rewrite sum_n_Sm; last lia. - rewrite IHk. - replace (plus _ _) with (((S k - 1) * S k / 2) + (S (S k - 1))) by done. - assert (∀ k, (INR (S k) - 1) = (INR k)) as H'. - { intros. simpl. case_match; first replace (1 - 1) with 0 by lra. - - done. - - by replace (_+1-1) with (INR (S n)) by lra. - } - rewrite !H'. - replace (S k - 1)%nat with (k)%nat by lia. - assert (k * (S k) + S k + S k = S k * S (S k)); last lra. - assert (k * S k + S k + S k = S k * (k+1+1)) as ->; try lra. - assert (k+1+1 = S (S k)). - -- rewrite !S_INR. lra. - -- by rewrite H. - - rewrite -!Rmult_minus_distr_r. - apply Rcomplements.Rdiv_le_0_compat; try lra. - apply Rmult_le_pos; try lra. - assert (INR k <= INR max_hash_size); try lra. - by apply le_INR. - Qed. - + Lemma wp_init_hash_amortized E : + {{{ True }}} + init_hash val_size #() @ E + {{{ f, RET f; hashfun_amortized f ∅ }}}. + Proof. + rewrite /init_hash. + iIntros (Φ) "_ HΦ". + wp_pures. rewrite /init_hash_state. + wp_apply (wp_init_map with "[//]"). + iIntros (?) "Hm". wp_pures. + rewrite /compute_hash. wp_pures. + iApply "HΦ". iExists _. rewrite fmap_empty. iFrame. + iMod ec_zero. + iModIntro. iExists 0%nat, nnreal_zero. + repeat (iSplit; [done|]). iFrame. + iPureIntro. + simpl. + replace (sum_n_m _ _ _) with 0; first lra. + rewrite sum_n_n. by simpl. + Qed. - Lemma wp_insert_no_coll_amortized E f m (n : nat) (z : Z) : - m !! n = None → - (size m < max_hash_size)%nat -> - {{{ hashfun_amortized f m ∗ € amortized_error ∗ - ⌜coll_free m⌝ }}} - f #n @ E - {{{ (v : Z), RET #v; hashfun_amortized f (<[ n := v ]>m) ∗ ⌜coll_free (<[ n := v ]>m)⌝ }}}. - Proof. - iIntros (Hlookup Hsize Φ) "(Hhash & Herr & %Hcoll) HΦ". - iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". - iAssert (€ (nnreal_div (nnreal_nat (size m)) (nnreal_nat (val_size + 1))) ∗ - € (mknonnegreal (((max_hash_size + 1) * size (<[n:=0%Z]> m) / 2 - sum_n_m (λ x, INR x) 0%nat (size (<[n:=0%Z]> m) - 1)) / (val_size + 1)) _ ) - )%I with "[Hε Herr]" as "[Hε Herr]". - - iApply ec_split. - iCombine "Hε Herr" as "H". - iApply (ec_spend_irrel with "[$]"). - simpl. rewrite H. rewrite map_size_insert_None; [|done]. - remember (size m) as k. - remember (val_size + 1) as v. - remember (max_hash_size) as h. - assert (∀ x y, x/y = x*/y) as Hdiv. - { intros. lra. } - destruct k. - + simpl. rewrite sum_n_n. rewrite Rmult_0_l Rmult_0_r. - replace (INR 0%nat) with 0; last done. - rewrite !Rminus_0_r. - replace (0/_/_) with 0; last lra. - rewrite !Rplus_0_l. - rewrite Rmult_1_r. - rewrite !Hdiv. - rewrite Rinv_mult. - lra. - + assert (forall k, S k - 1 = k)%nat as H' by lia. - rewrite !H'. - clear H'. - rewrite sum_n_Sm; last lia. - replace (plus _ (INR (S k))) with ((sum_n_m (λ x : nat, INR x) 0 k) + (S k)) by done. - rewrite !Hdiv. - rewrite !Rmult_minus_distr_r. - rewrite (Rmult_plus_distr_r (sum_n_m _ _ _)). - rewrite -!Rplus_assoc. - rewrite Ropp_plus_distr. - rewrite -!Rplus_assoc. - assert ((h + 1) * S k * / 2 * / v+ (h + 1) * / (2 * v) = S k * / (val_size + 1)%nat + (h + 1) * S (S k) * / 2 * / v + - (S k * / v)); try lra. - replace (INR((_+_)%nat)) with v; last first. - { rewrite Heqv. rewrite -S_INR. f_equal. lia. } - assert ( (h + 1) * S k * / 2 * / v + (h + 1) * / (2 * v) = (h + 1) * S (S k) * / 2 * / v); try lra. - replace (_*_*_*_) with ((h+1) * (S k) * /(2*v)); last first. - { rewrite Rinv_mult. lra. } - replace (_*_*_*_) with ((h+1) * (S(S k)) * /(2*v)); last first. - { rewrite Rinv_mult. lra. } - rewrite -Rdiv_plus_distr. - rewrite Hdiv. - f_equal. - rewrite -{2}(Rmult_1_r (h+1)). - rewrite -Rmult_plus_distr_l. - f_equal. - - wp_apply (wp_insert_no_coll with "[H Hε]"); [done|done|..]. - + iFrame. iSplitL; try done. - iExists _. by iFrame. - + iIntros (v) "[H %]". - iApply "HΦ". - iSplitL; last done. - iExists _, _, _. iFrame. - repeat (iSplitR); try done. - * iPureIntro. simpl. do 3 f_equal. - all: by repeat rewrite map_size_insert. - * iDestruct "H" as "[% [% H]]". - inversion H1; subst. - iFrame. - Unshelve. - apply amortized_inequality. - rewrite map_size_insert. - case_match => /=; lia. - Qed. + Lemma wp_hashfun_prev_amortized E f m (n : nat) (b : Z) : + m !! n = Some b → + {{{ hashfun_amortized f m }}} + f #n @ E + {{{ RET #b; hashfun_amortized f m }}}. + Proof. + iIntros (Hlookup Φ) "Hhash HΦ". + iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". + wp_apply (wp_hashfun_prev with "[H]"); first done. + - iExists _. by iFrame. + - iIntros "(%&%&H)". iApply "HΦ". + iExists _,_,_. by iFrame. + Qed. - End amortized. + Lemma hashfun_amortized_hashfun f m: ⊢ hashfun_amortized f m -∗ hashfun val_size f m. + Proof. + iIntros "(%&%&%&->&->&%&He&H)". + iExists _; by iFrame. + Qed. + Lemma amortized_inequality (k : nat): + (k <= max_hash_size)%nat -> + 0 <= ((max_hash_size + 1) * k / 2 - sum_n_m (λ x : nat, INR x) 0 (k - 1)) / (val_size + 1). + Proof. + intros H. + pose proof (pos_INR max_hash_size) as H1. + pose proof (pos_INR val_size) as H2. + pose proof (pos_INR k) as H3. + apply Rcomplements.Rdiv_le_0_compat; last lra. + assert (sum_n_m (λ x : nat, INR x) 0 (k - 1) = (k-1)*k/2) as ->. + - clear. + induction k. + + simpl. rewrite sum_n_n. + rewrite Rmult_0_r. by assert (0/2 = 0) as -> by lra. + + clear. induction k. + * simpl. rewrite sum_n_n. + replace (_-_) with 0 by lra. + rewrite Rmult_0_l. by assert (0/2 = 0) as -> by lra. + * assert (S (S k) - 1 = S (S k - 1))%nat as -> by lia. + rewrite sum_n_Sm; last lia. + rewrite IHk. + replace (plus _ _) with (((S k - 1) * S k / 2) + (S (S k - 1))) by done. + assert (∀ k, (INR (S k) - 1) = (INR k)) as H'. + { intros. simpl. case_match; first replace (1 - 1) with 0 by lra. + - done. + - by replace (_+1-1) with (INR (S n)) by lra. + } + rewrite !H'. + replace (S k - 1)%nat with (k)%nat by lia. + assert (k * (S k) + S k + S k = S k * S (S k)); last lra. + assert (k * S k + S k + S k = S k * (k+1+1)) as ->; try lra. + assert (k+1+1 = S (S k)). + -- rewrite !S_INR. lra. + -- by rewrite H. + - rewrite -!Rmult_minus_distr_r. + apply Rcomplements.Rdiv_le_0_compat; try lra. + apply Rmult_le_pos; try lra. + assert (INR k <= INR max_hash_size); try lra. + by apply le_INR. + Qed. -End simple_bit_hash. + Lemma wp_insert_no_coll_amortized E f m (n : nat) (z : Z) : + m !! n = None → + (size m < max_hash_size)%nat -> + {{{ hashfun_amortized f m ∗ € amortized_error ∗ + ⌜coll_free m⌝ }}} + f #n @ E + {{{ (v : Z), RET #v; hashfun_amortized f (<[ n := v ]>m) ∗ ⌜coll_free (<[ n := v ]>m)⌝ }}}. + Proof. + iIntros (Hlookup Hsize Φ) "(Hhash & Herr & %Hcoll) HΦ". + iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". + iAssert (€ (nnreal_div (nnreal_nat (size m)) (nnreal_nat (val_size + 1))) ∗ + € (mknonnegreal (((max_hash_size + 1) * size (<[n:=0%Z]> m) / 2 - sum_n_m (λ x, INR x) 0%nat (size (<[n:=0%Z]> m) - 1)) / (val_size + 1)) _ ) + )%I with "[Hε Herr]" as "[Hε Herr]". + - iApply ec_split. + iCombine "Hε Herr" as "H". + iApply (ec_spend_irrel with "[$]"). + simpl. rewrite H. rewrite map_size_insert_None; [|done]. + remember (size m) as k. + remember (val_size + 1) as v. + remember (max_hash_size) as h. + assert (∀ x y, x/y = x*/y) as Hdiv. + { intros. lra. } + destruct k. + + simpl. rewrite sum_n_n. rewrite Rmult_0_l Rmult_0_r. + replace (INR 0%nat) with 0; last done. + rewrite !Rminus_0_r. + replace (0/_/_) with 0; last lra. + rewrite !Rplus_0_l. + rewrite Rmult_1_r. + rewrite !Hdiv. + rewrite Rinv_mult. + lra. + + assert (forall k, S k - 1 = k)%nat as H' by lia. + rewrite !H'. + clear H'. + rewrite sum_n_Sm; last lia. + replace (plus _ (INR (S k))) with ((sum_n_m (λ x : nat, INR x) 0 k) + (S k)) by done. + rewrite !Hdiv. + rewrite !Rmult_minus_distr_r. + rewrite (Rmult_plus_distr_r (sum_n_m _ _ _)). + rewrite -!Rplus_assoc. + rewrite Ropp_plus_distr. + rewrite -!Rplus_assoc. + assert ((h + 1) * S k * / 2 * / v+ (h + 1) * / (2 * v) = S k * / (val_size + 1)%nat + (h + 1) * S (S k) * / 2 * / v + - (S k * / v)); try lra. + replace (INR((_+_)%nat)) with v; last first. + { rewrite Heqv. rewrite -S_INR. f_equal. lia. } + assert ( (h + 1) * S k * / 2 * / v + (h + 1) * / (2 * v) = (h + 1) * S (S k) * / 2 * / v); try lra. + replace (_*_*_*_) with ((h+1) * (S k) * /(2*v)); last first. + { rewrite Rinv_mult. lra. } + replace (_*_*_*_) with ((h+1) * (S(S k)) * /(2*v)); last first. + { rewrite Rinv_mult. lra. } + rewrite -Rdiv_plus_distr. + rewrite Hdiv. + f_equal. + rewrite -{2}(Rmult_1_r (h+1)). + rewrite -Rmult_plus_distr_l. + f_equal. + - wp_apply (wp_insert_no_coll with "[H Hε]"); [done|done|..]. + + iFrame. iSplitL; try done. + iExists _. by iFrame. + + iIntros (v) "[H %]". + iApply "HΦ". + iSplitL; last done. + iExists _, _, _. iFrame. + repeat (iSplitR); try done. + * iPureIntro. simpl. do 3 f_equal. + all: by repeat rewrite map_size_insert. + * iDestruct "H" as "[% [% H]]". + inversion H1; subst. + iFrame. + Unshelve. + apply amortized_inequality. + rewrite map_size_insert. + case_match => /=; lia. + Qed. +End amortized_hash. From 9f3b3d498e535016bbefb787b1421e5bdede82fa Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 30 Jan 2024 10:59:39 +0100 Subject: [PATCH 03/21] Second try, not sure why check failed --- theories/ub_logic/merkel_tree.v | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 theories/ub_logic/merkel_tree.v diff --git a/theories/ub_logic/merkel_tree.v b/theories/ub_logic/merkel_tree.v new file mode 100644 index 000000000..f9d5ab35d --- /dev/null +++ b/theories/ub_logic/merkel_tree.v @@ -0,0 +1,3 @@ +From clutch.ub_logic Require Export ub_clutch lib.map hash. +Import Hierarchy. +Set Default Proof Using "Type*". From 6491bf356bcd91e69359bb1f61a53d7b688d8ef8 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 30 Jan 2024 16:34:04 +0100 Subject: [PATCH 04/21] progress with merkel tree --- theories/ub_logic/hash.v | 26 +++++++- theories/ub_logic/merkel_tree.v | 109 +++++++++++++++++++++++++++++++- 2 files changed, 132 insertions(+), 3 deletions(-) diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v index f64e9ed2e..f983d92e7 100644 --- a/theories/ub_logic/hash.v +++ b/theories/ub_logic/hash.v @@ -1,4 +1,5 @@ From clutch.ub_logic Require Export ub_clutch lib.map. +From stdpp Require Export fin_maps. Import Hierarchy. Set Default Proof Using "Type*". @@ -170,7 +171,7 @@ Section amortized_hash. Context `{!ub_clutchGS Σ}. Variable val_size:nat. Variable max_hash_size : nat. - Variable Hineq : max_hash_size <= (val_size+1). + 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. @@ -275,7 +276,7 @@ Section amortized_hash. Qed. - Lemma wp_insert_no_coll_amortized E f m (n : nat) (z : Z) : + Lemma wp_insert_new_amortized E f m (n : nat) (z : Z) : m !! n = None → (size m < max_hash_size)%nat -> {{{ hashfun_amortized f m ∗ € amortized_error ∗ @@ -351,4 +352,25 @@ Section amortized_hash. case_match => /=; lia. Qed. + Lemma wp_insert_amortized E f m (n : nat) (z : Z) : + (size m < max_hash_size)%nat -> + {{{ hashfun_amortized f m ∗ € amortized_error ∗ + ⌜coll_free m⌝ }}} + f #n @ E + {{{ (v : Z), RET #v; ∃ m', hashfun_amortized f m' ∗ ⌜coll_free m'⌝ ∗ ⌜m'!!n = Some v⌝ ∗ ⌜(size m' <= max_hash_size)%nat⌝ ∗ ⌜m⊆m'⌝ }}}. + Proof. + iIntros (Hsize Φ) "[Hh[Herr %Hc]] HΦ". + destruct (m!!n) eqn:Heq. + - wp_apply (wp_hashfun_prev_amortized with "[$]"); first done. + iIntros. iApply "HΦ". + iExists _; iFrame. + repeat iSplit; try done. iPureIntro; lia. + - wp_apply (wp_insert_new_amortized with "[$Hh $Herr]"); try done. + iIntros (?) "[??]"; iApply "HΦ". + iExists _; iFrame. iPureIntro. repeat split. + + rewrite lookup_insert_Some. naive_solver. + + rewrite map_size_insert. case_match; try (simpl; lia). + + by apply insert_subseteq. + Qed. + End amortized_hash. diff --git a/theories/ub_logic/merkel_tree.v b/theories/ub_logic/merkel_tree.v index f9d5ab35d..fd490d113 100644 --- a/theories/ub_logic/merkel_tree.v +++ b/theories/ub_logic/merkel_tree.v @@ -1,3 +1,110 @@ -From clutch.ub_logic Require Export ub_clutch lib.map hash. +From clutch.ub_logic Require Export ub_clutch lib.map hash lib.list. Import Hierarchy. Set Default Proof Using "Type*". + +Section merkel_tree. + Context `{!ub_clutchGS Σ}. + Variables height:nat. + Variables val_bit_size':nat. + Variables max_hash_size : nat. + Definition val_bit_size : nat := S val_bit_size'. + Definition val_size:nat := (2^val_bit_size)-1. + Variable (Hineq: (max_hash_size <= val_size)%nat). + Definition leaf_bit_size : nat := 2*val_bit_size. + (* Definition identifier : nat := 2^leaf_bit_size. *) + Definition num_of_leafs : nat := 2^height. + + Inductive merkel_tree := + | Leaf (hash_value : nat) (leaf_value:nat) + | Branch (hash_value : nat) (t1 t2:merkel_tree). + + Definition root_hash_value (t: merkel_tree) := + match t with + | Leaf h _ => h + | Branch h _ _ => h + end. + + Fixpoint tree_relate (h:nat) (lt : val) (t:merkel_tree) : Prop:= + match h with + |0 => (∃ (hv v:nat), lt = InjLV (#hv, #v) /\ t = Leaf hv v) + |S h' => ∃ (hv:nat) (ll lr:val) (l r:merkel_tree), lt = InjRV (#hv, ll, lr) /\ t = Branch hv l r /\ + tree_relate h' ll l /\ tree_relate h' lr r + end. + + Fixpoint tree_valid (t:merkel_tree) (m:gmap nat Z) : Prop := + match t with + | Leaf h l => h < 2^val_bit_size /\ l < 2^leaf_bit_size /\ m!!l%nat = Some (Z.of_nat h) + | Branch h l r => h < 2^val_bit_size /\ m!!((root_hash_value l)*2^val_bit_size + root_hash_value r)%nat=Some (Z.of_nat h) /\ tree_valid l m /\ tree_valid r m + end. + + Definition map_valid (m:gmap nat Z) : Prop := coll_free m. + + Definition compute_hash_from_leaf : val := + rec: "compute_hash_from_leaf" "ltree" "lhmf" "ll" "lf" := + match: "ltree" with + | InjL "x" => "lhmf" "lf" + | InjR "x" => let: "b" := (match: list_head "ll" with + | SOME "a" => "a" + | NONE => #() + end + ) in + let: "ll'" := (match: list_tail "ll" with + | SOME "a" => "a" + | NONE => #() + end + ) in + let, ("l", "r") := Snd "x" in + if: "b" + then "lhmf" + (("compute_hash_from_leaf" "l" "lhmf" "ll'" "lleaf")*#(2^val_bit_size)+"r") + else "lhmf" + ("l"*#(2^val_bit_size)+("compute_hash_from_leaf" "r" "lhmf" "ll'" "lleaf")) + end + + . + + Fixpoint tree_value_match (tree:merkel_tree) (v:nat) (path:list bool) := + match (tree, path) with + | (Leaf h lf, []) => lf=v + | (Branch h l r, x::xs) => if x then tree_value_match l v xs else tree_value_match r v xs + | _ => False + end. + + (** Lemmas *) + Lemma tree_relate_leaf h ltree a b : + tree_relate h ltree (Leaf a b) -> h = 0%nat /\ ltree = InjLV (#a, #b). + Proof. + Admitted. + + + (** Spec *) + Lemma wp_correct_check (ltree:val) (tree:merkel_tree) (m:gmap nat Z) (v:nat) (path:list bool) llist f E: + {{{ ⌜tree_relate height ltree tree⌝ ∗ + ⌜tree_valid tree m⌝ ∗ + hashfun_amortized (val_size-1)%nat max_hash_size f m ∗ + ⌜is_list path llist⌝ ∗ + ⌜tree_value_match tree v path⌝ ∗ + ⌜map_valid m⌝ }}} + compute_hash_from_leaf ltree f llist (#v) @ E + {{{ (retv:Z), RET #retv; + hashfun_amortized (val_size-1) max_hash_size f m ∗ + ⌜retv = root_hash_value tree⌝ + }}}. + Proof. + iIntros (Φ) "(%Htrelate&%Htvalid&H&%Hlsit&%Hvmatch&%Hmvalid) HΦ". + revert Htrelate Htvalid Hlsit Hvmatch Hmvalid. + revert height ltree v path llist f. + induction tree. + - intros. + rewrite /compute_hash_from_leaf. + wp_pures. apply tree_relate_leaf in Htrelate as [-> ->]. + wp_match. + wp_apply (wp_hashfun_prev_amortized with "[$]"). + + lia. + + admit. + + admit. + + - admit. + Admitted. + +End merkel_tree. From 8e7cc92de0f29a186181de00ebdffcf0aa33578a Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 30 Jan 2024 16:57:29 +0100 Subject: [PATCH 05/21] Change merkel to merkle. Also change many proposition to inductive --- .../ub_logic/{merkel_tree.v => merkle_tree.v} | 66 +++++++++++-------- 1 file changed, 37 insertions(+), 29 deletions(-) rename theories/ub_logic/{merkel_tree.v => merkle_tree.v} (65%) diff --git a/theories/ub_logic/merkel_tree.v b/theories/ub_logic/merkle_tree.v similarity index 65% rename from theories/ub_logic/merkel_tree.v rename to theories/ub_logic/merkle_tree.v index fd490d113..795f14b79 100644 --- a/theories/ub_logic/merkel_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -1,8 +1,9 @@ From clutch.ub_logic Require Export ub_clutch lib.map hash lib.list. Import Hierarchy. Set Default Proof Using "Type*". +Open Scope nat. -Section merkel_tree. +Section merkle_tree. Context `{!ub_clutchGS Σ}. Variables height:nat. Variables val_bit_size':nat. @@ -14,28 +15,37 @@ Section merkel_tree. (* Definition identifier : nat := 2^leaf_bit_size. *) Definition num_of_leafs : nat := 2^height. - Inductive merkel_tree := + Inductive merkle_tree := | Leaf (hash_value : nat) (leaf_value:nat) - | Branch (hash_value : nat) (t1 t2:merkel_tree). + | Branch (hash_value : nat) (t1 t2:merkle_tree). - Definition root_hash_value (t: merkel_tree) := + Definition root_hash_value (t: merkle_tree) := match t with | Leaf h _ => h | Branch h _ _ => h end. - - Fixpoint tree_relate (h:nat) (lt : val) (t:merkel_tree) : Prop:= - match h with - |0 => (∃ (hv v:nat), lt = InjLV (#hv, #v) /\ t = Leaf hv v) - |S h' => ∃ (hv:nat) (ll lr:val) (l r:merkel_tree), lt = InjRV (#hv, ll, lr) /\ t = Branch hv l r /\ - tree_relate h' ll l /\ tree_relate h' lr r - end. - Fixpoint tree_valid (t:merkel_tree) (m:gmap nat Z) : Prop := - match t with - | Leaf h l => h < 2^val_bit_size /\ l < 2^leaf_bit_size /\ m!!l%nat = Some (Z.of_nat h) - | Branch h l r => h < 2^val_bit_size /\ m!!((root_hash_value l)*2^val_bit_size + root_hash_value r)%nat=Some (Z.of_nat h) /\ tree_valid l m /\ tree_valid r m - end. + Inductive tree_relate: nat -> val -> merkle_tree -> Prop:= + | tree_relate_lf (hv v:nat): tree_relate 0 (InjLV (#hv, #v)) (Leaf hv v) + | tree_relate_br n (hv:nat) ll l lr r: + tree_relate n ll l -> + tree_relate n lr r -> + tree_relate (S n) (InjRV (#hv, ll, lr)) (Branch hv l r) + . + + Inductive tree_valid: merkle_tree -> gmap nat Z -> Prop := + |tree_valid_lf (h l:nat) m: + h < 2^val_bit_size -> + l < 2^leaf_bit_size -> + m!!l%nat = Some (Z.of_nat h) -> + tree_valid (Leaf h l) m + |tree_valid_br (h:nat) l r m: + tree_valid l m -> + tree_valid r m -> + h < 2^val_bit_size -> + m!!((root_hash_value l)*2^val_bit_size + root_hash_value r)%nat=Some (Z.of_nat h) -> + tree_valid (Branch h l r) m. + Definition map_valid (m:gmap nat Z) : Prop := coll_free m. @@ -63,22 +73,20 @@ Section merkel_tree. . - Fixpoint tree_value_match (tree:merkel_tree) (v:nat) (path:list bool) := - match (tree, path) with - | (Leaf h lf, []) => lf=v - | (Branch h l r, x::xs) => if x then tree_value_match l v xs else tree_value_match r v xs - | _ => False - end. + Inductive tree_value_match: merkle_tree -> nat -> list bool -> Prop:= + | tree_value_match_lf h lf: tree_value_match (Leaf h lf) lf [] + | tree_value_match_left h l r xs v: + tree_value_match l v xs -> + tree_value_match (Branch h l r) v (true::xs) + | tree_value_match_right h l r xs v: + tree_value_match r v xs -> + tree_value_match (Branch h l r) v (false::xs). (** Lemmas *) - Lemma tree_relate_leaf h ltree a b : - tree_relate h ltree (Leaf a b) -> h = 0%nat /\ ltree = InjLV (#a, #b). - Proof. - Admitted. (** Spec *) - Lemma wp_correct_check (ltree:val) (tree:merkel_tree) (m:gmap nat Z) (v:nat) (path:list bool) llist f E: + Lemma wp_correct_check (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (path:list bool) llist f E: {{{ ⌜tree_relate height ltree tree⌝ ∗ ⌜tree_valid tree m⌝ ∗ hashfun_amortized (val_size-1)%nat max_hash_size f m ∗ @@ -97,7 +105,7 @@ Section merkel_tree. induction tree. - intros. rewrite /compute_hash_from_leaf. - wp_pures. apply tree_relate_leaf in Htrelate as [-> ->]. + wp_pures. inversion Htrelate; subst. wp_match. wp_apply (wp_hashfun_prev_amortized with "[$]"). + lia. @@ -107,4 +115,4 @@ Section merkel_tree. - admit. Admitted. -End merkel_tree. +End merkle_tree. From d7e26728707b44847016f28531e5df64db8c8ea0 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 1 Feb 2024 10:46:02 +0100 Subject: [PATCH 06/21] merkle tree example when hash is correct --- theories/ub_logic/merkle_tree.v | 93 +++++++++++++++++++++++++-------- 1 file changed, 71 insertions(+), 22 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 795f14b79..61d82b855 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -49,26 +49,30 @@ Section merkle_tree. Definition map_valid (m:gmap nat Z) : Prop := coll_free m. + Definition root_hash_value_program : val := + λ: "ltree", + match: "ltree" with + | InjL "x" => Fst "x" + | InjR "x" => let, ("a", "b", "c") := "x" in "a" + end. + Definition compute_hash_from_leaf : val := - rec: "compute_hash_from_leaf" "ltree" "lhmf" "ll" "lf" := + rec: "compute_hash_from_leaf" "ltree" "lhmf" "ll" "lleaf" := match: "ltree" with - | InjL "x" => "lhmf" "lf" + | InjL "x" => "lhmf" "lleaf" | InjR "x" => let: "b" := (match: list_head "ll" with | SOME "a" => "a" | NONE => #() end ) in - let: "ll'" := (match: list_tail "ll" with - | SOME "a" => "a" - | NONE => #() - end - ) in - let, ("l", "r") := Snd "x" in + let: "ll'" := list_tail "ll" in + let, ("notneeded", "l", "r") := "x" in if: "b" then "lhmf" - (("compute_hash_from_leaf" "l" "lhmf" "ll'" "lleaf")*#(2^val_bit_size)+"r") + (("compute_hash_from_leaf" "l" "lhmf" "ll'" "lleaf")*#(2^val_bit_size)+ + root_hash_value_program "r") else "lhmf" - ("l"*#(2^val_bit_size)+("compute_hash_from_leaf" "r" "lhmf" "ll'" "lleaf")) + ((root_hash_value_program "l")*#(2^val_bit_size)+("compute_hash_from_leaf" "r" "lhmf" "ll'" "lleaf")) end . @@ -83,10 +87,20 @@ Section merkle_tree. tree_value_match (Branch h l r) v (false::xs). (** Lemmas *) - + Lemma wp_root_hash_value_program n lt tree E: + {{{ ⌜tree_relate n lt tree⌝ }}} + root_hash_value_program lt @ E + {{{ (retv:Z), RET #retv; ⌜retv = root_hash_value tree⌝}}}. + Proof. + iIntros (Φ) "%H HΦ". + rewrite /root_hash_value_program. wp_pures. + inversion H. + - wp_pures. iApply "HΦ". by iPureIntro. + - wp_pures. iApply "HΦ". by iPureIntro. + Qed. (** Spec *) - Lemma wp_correct_check (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (path:list bool) llist f E: + Lemma wp_compute_hash_from_leaf_correct (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (path:list bool) llist f E: {{{ ⌜tree_relate height ltree tree⌝ ∗ ⌜tree_valid tree m⌝ ∗ hashfun_amortized (val_size-1)%nat max_hash_size f m ∗ @@ -100,19 +114,54 @@ Section merkle_tree. }}}. Proof. iIntros (Φ) "(%Htrelate&%Htvalid&H&%Hlsit&%Hvmatch&%Hmvalid) HΦ". - revert Htrelate Htvalid Hlsit Hvmatch Hmvalid. - revert height ltree v path llist f. - induction tree. - - intros. - rewrite /compute_hash_from_leaf. + iInduction tree as [|] "IH" + forall (height ltree v path llist f Htrelate Htvalid Hlsit Hvmatch Hmvalid Φ). + - rewrite /compute_hash_from_leaf. wp_pures. inversion Htrelate; subst. wp_match. + inversion Htrelate. inversion Htvalid. inversion Hvmatch. subst. wp_apply (wp_hashfun_prev_amortized with "[$]"). + lia. - + admit. - + admit. - - - admit. - Admitted. + + done. + + iIntros. iApply "HΦ". iFrame. by iPureIntro. + - rewrite /compute_hash_from_leaf. + inversion Htrelate. inversion Htvalid. inversion Hvmatch; subst. + + wp_pures. wp_apply wp_list_head; first done. iIntros (v') "[[%%]|(%&%&%&%)]"; first done. + subst. inversion H; subst. wp_pures. rewrite -/compute_hash_from_leaf. + wp_apply wp_list_tail; first done. iIntros (v') "%". wp_pures. + wp_apply wp_root_hash_value_program; try done. + iIntros (x) "->". + wp_apply ("IH" with "[][][][][][H][HΦ]"); try done. + iModIntro. iIntros (?) "[H ->]". + wp_pures. + replace (_*_+_)%Z with (Z.of_nat (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2)); last first. + { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul. f_equal. + apply Z2Nat.inj_pow. + } + wp_apply (wp_hashfun_prev_amortized with "H"). + * lia. + * done. + * iIntros "H". iApply "HΦ". iFrame. + done. + + wp_pures. wp_apply wp_list_head; first done. iIntros (v') "[[%%]|(%&%&%&%)]"; first done. + subst. inversion H; subst. wp_pures. rewrite -/compute_hash_from_leaf. + wp_apply wp_list_tail; first done. iIntros (v') "%". wp_pures. + wp_apply ("IH1" with "[][][][][][H][HΦ]"); try done. + iModIntro. iIntros (?) "[H ->]". + wp_apply wp_root_hash_value_program; try done. + iIntros (x) "->". + wp_pures. + replace (_*_+_)%Z with (Z.of_nat (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2)); last first. + { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul. f_equal. + apply Z2Nat.inj_pow. + } + wp_apply (wp_hashfun_prev_amortized with "H"). + * lia. + * done. + * iIntros "H". iApply "HΦ". iFrame. + done. + Qed. + + End merkle_tree. From bb51d1e0c850ec7ef967f78d2e9ec2eac72cdd88 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 1 Feb 2024 15:22:54 +0100 Subject: [PATCH 07/21] merkle tree done, but wrong implementation :) --- theories/ub_logic/hash.v | 47 +++++---- theories/ub_logic/merkle_tree.v | 163 +++++++++++++++++++++++++++++++- 2 files changed, 191 insertions(+), 19 deletions(-) diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v index f983d92e7..a0f044cd0 100644 --- a/theories/ub_logic/hash.v +++ b/theories/ub_logic/hash.v @@ -41,7 +41,10 @@ Section simple_bit_hash. compute_hash "hm". Definition hashfun f m : iProp Σ := - ∃ (hm : loc), ⌜ f = compute_hash_specialized #hm ⌝ ∗ map_list hm ((λ b, LitV (LitInt b)) <$> m). + ∃ (hm : loc), ⌜ f = compute_hash_specialized #hm ⌝ ∗ + map_list hm ((λ b, LitV (LitInt b)) <$> m) ∗ + ⌜map_Forall (λ ind i, (0<= i <=val_size)%Z) m⌝ + . #[global] Instance timeless_hashfun f m : Timeless (hashfun f m). @@ -117,7 +120,7 @@ Section simple_bit_hash. {{{ RET #b; hashfun f m }}}. Proof. iIntros (Hlookup Φ) "Hhash HΦ". - iDestruct "Hhash" as (hm ->) "H". + iDestruct "Hhash" as (hm ->) "[H Hbound]". rewrite /compute_hash_specialized. wp_pures. wp_apply (wp_get with "[$]"). @@ -127,7 +130,7 @@ Section simple_bit_hash. Qed. - Lemma wp_insert_no_coll E f m (n : nat) (z : Z) : + Lemma wp_insert_no_coll E f m (n : nat) : m !! n = None → {{{ hashfun f m ∗ € (nnreal_div (nnreal_nat (length (gmap_to_list m))) (nnreal_nat(val_size+1))) ∗ ⌜coll_free m⌝ }}} @@ -135,7 +138,7 @@ Section simple_bit_hash. {{{ (v : Z), RET #v; hashfun f (<[ n := v ]>m) ∗ ⌜coll_free (<[ n := v ]>m)⌝ }}}. Proof. iIntros (Hlookup Φ) "(Hhash & Herr & %Hcoll) HΦ". - iDestruct "Hhash" as (hm ->) "H". + iDestruct "Hhash" as (hm ->) "[H %Hbound]". rewrite /compute_hash_specialized. wp_pures. wp_apply (wp_get with "[$]"). @@ -156,7 +159,14 @@ Section simple_bit_hash. - rewrite /hashfun. iExists _. iSplit; first auto. - rewrite fmap_insert //. + iSplitL. + + rewrite fmap_insert //. + + iPureIntro. + apply map_Forall_insert_2; last done. + split. + * lia. + * pose proof (fin_to_nat_lt x). + lia. - iPureIntro. apply coll_free_insert; auto. apply (Forall_map (λ p : nat * Z, p.2)) in HForall; auto. @@ -183,6 +193,7 @@ Section amortized_hash. Definition hashfun_amortized f m : iProp Σ := ∃ (hm : loc) (k : nat) (ε : nonnegreal), ⌜ f = compute_hash_specialized val_size #hm ⌝ ∗ + ⌜map_Forall (λ ind i, (0<= i <=val_size)%Z) m⌝ ∗ ⌜k = size m⌝ ∗ ⌜ (ε.(nonneg) = (((max_hash_size + 1) * k)/2 - sum_n_m (λ x, INR x) 0%nat (k-1)) / (val_size + 1))%R⌝ ∗ € ε ∗ @@ -221,16 +232,17 @@ Section amortized_hash. {{{ RET #b; hashfun_amortized f m }}}. Proof. iIntros (Hlookup Φ) "Hhash HΦ". - iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". + iDestruct "Hhash" as (hm k ε ->) "[%[-> [% [Hε H]]]]". wp_apply (wp_hashfun_prev with "[H]"); first done. - iExists _. by iFrame. - - iIntros "(%&%&H)". iApply "HΦ". - iExists _,_,_. by iFrame. + - iIntros "(%&%&H)". inversion H1; subst. iApply "HΦ". + iExists _,_,_. iFrame. repeat iSplit; try done. + by iDestruct "H" as "[??]". Qed. Lemma hashfun_amortized_hashfun f m: ⊢ hashfun_amortized f m -∗ hashfun val_size f m. Proof. - iIntros "(%&%&%&->&->&%&He&H)". + iIntros "(%&%&%&->&%&->&%&He&H)". iExists _; by iFrame. Qed. @@ -276,7 +288,7 @@ Section amortized_hash. Qed. - Lemma wp_insert_new_amortized E f m (n : nat) (z : Z) : + Lemma wp_insert_new_amortized E f m (n : nat) : m !! n = None → (size m < max_hash_size)%nat -> {{{ hashfun_amortized f m ∗ € amortized_error ∗ @@ -285,14 +297,14 @@ Section amortized_hash. {{{ (v : Z), RET #v; hashfun_amortized f (<[ n := v ]>m) ∗ ⌜coll_free (<[ n := v ]>m)⌝ }}}. Proof. iIntros (Hlookup Hsize Φ) "(Hhash & Herr & %Hcoll) HΦ". - iDestruct "Hhash" as (hm k ε -> ->) "[% [Hε H]]". + iDestruct "Hhash" as (hm k ε -> ) "[%[->[% [Hε H]]]]". iAssert (€ (nnreal_div (nnreal_nat (size m)) (nnreal_nat (val_size + 1))) ∗ € (mknonnegreal (((max_hash_size + 1) * size (<[n:=0%Z]> m) / 2 - sum_n_m (λ x, INR x) 0%nat (size (<[n:=0%Z]> m) - 1)) / (val_size + 1)) _ ) )%I with "[Hε Herr]" as "[Hε Herr]". - iApply ec_split. iCombine "Hε Herr" as "H". iApply (ec_spend_irrel with "[$]"). - simpl. rewrite H. rewrite map_size_insert_None; [|done]. + simpl. rewrite H0. rewrite map_size_insert_None; [|done]. remember (size m) as k. remember (val_size + 1) as v. remember (max_hash_size) as h. @@ -333,31 +345,30 @@ Section amortized_hash. rewrite -{2}(Rmult_1_r (h+1)). rewrite -Rmult_plus_distr_l. f_equal. - - wp_apply (wp_insert_no_coll with "[H Hε]"); [done|done|..]. + - wp_apply (wp_insert_no_coll with "[H Hε]"); [done|..]. + iFrame. iSplitL; try done. iExists _. by iFrame. + iIntros (v) "[H %]". iApply "HΦ". iSplitL; last done. iExists _, _, _. iFrame. + iDestruct "H" as "(%&%&H&%)". repeat (iSplitR); try done. * iPureIntro. simpl. do 3 f_equal. all: by repeat rewrite map_size_insert. - * iDestruct "H" as "[% [% H]]". - inversion H1; subst. - iFrame. + * inversion H2; by subst. Unshelve. apply amortized_inequality. rewrite map_size_insert. case_match => /=; lia. Qed. - Lemma wp_insert_amortized E f m (n : nat) (z : Z) : + Lemma wp_insert_amortized E f m (n : nat) : (size m < max_hash_size)%nat -> {{{ hashfun_amortized f m ∗ € amortized_error ∗ ⌜coll_free m⌝ }}} f #n @ E - {{{ (v : Z), RET #v; ∃ m', hashfun_amortized f m' ∗ ⌜coll_free m'⌝ ∗ ⌜m'!!n = Some v⌝ ∗ ⌜(size m' <= max_hash_size)%nat⌝ ∗ ⌜m⊆m'⌝ }}}. + {{{ (v : Z), RET #v; ∃ m', hashfun_amortized f m' ∗ ⌜coll_free m'⌝ ∗ ⌜m'!!n = Some v⌝ ∗ ⌜(size m' <= S $ size(m))%nat⌝ ∗ ⌜m⊆m'⌝ }}}. Proof. iIntros (Hsize Φ) "[Hh[Herr %Hc]] HΦ". destruct (m!!n) eqn:Heq. diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 61d82b855..0ddc9da48 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -99,6 +99,17 @@ Section merkle_tree. - wp_pures. iApply "HΦ". by iPureIntro. Qed. + Lemma tree_valid_superset m m' tree: + tree_valid tree m -> m ⊆ m' -> tree_valid tree m'. + Proof. + induction tree. + - intros. inversion H; subst. + constructor; try done. + by eapply lookup_weaken. + - intros. inversion H; subst. constructor; try naive_solver. + by eapply lookup_weaken. + Qed. + (** Spec *) Lemma wp_compute_hash_from_leaf_correct (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (path:list bool) llist f E: {{{ ⌜tree_relate height ltree tree⌝ ∗ @@ -161,7 +172,157 @@ Section merkle_tree. * iIntros "H". iApply "HΦ". iFrame. done. Qed. + + + Lemma wp_compute_hash_from_leaf_incorrect (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v v':nat) (path:list bool) llist f E: + {{{ ⌜tree_relate height ltree tree⌝ ∗ + ⌜tree_valid tree m⌝ ∗ + hashfun_amortized (val_size-1)%nat max_hash_size f m ∗ + ⌜is_list path llist⌝ ∗ + ⌜tree_value_match tree v path⌝ ∗ + ⌜map_valid m⌝ ∗ + ⌜ size m + (S height) <= max_hash_size⌝ ∗ + ⌜v ≠ v'⌝ ∗ + € (nnreal_nat (S height) * amortized_error (val_size-1)%nat max_hash_size)%NNR + }}} + compute_hash_from_leaf ltree f llist (#v') @ E + {{{ (retv:Z), RET #retv; + ∃ m', ⌜m ⊆ m'⌝ ∗ + hashfun_amortized (val_size-1) max_hash_size f m' ∗ + ⌜map_valid m'⌝ ∗ + ⌜size (m') <= size m + (S height)⌝ ∗ + ⌜retv ≠ root_hash_value tree⌝ ∗ + ⌜(0 <= retv)%Z⌝ + }}}. + Proof. + iIntros (Φ) "(%Htrelate&%Htvalid&H&%Hlsit&%Hvmatch&%Hmvalid&%Hmsize&%Hneq&Herr) HΦ". + iInduction tree as [|] "IH" + forall (height ltree m path llist Φ Htrelate Htvalid Hlsit Hvmatch Hmvalid Hmsize Hneq). + - rewrite /compute_hash_from_leaf. + wp_pures. inversion Htrelate; subst. + wp_match. + inversion Htrelate. inversion Htvalid. inversion Hvmatch. subst. + wp_apply (wp_insert_amortized with "[$H Herr]"). + + lia. + + lia. + + iSplitL. + * assert (∀ x, (nnreal_nat 1 * x)%NNR = x) as ->; last iFrame. + intros. apply nnreal_ext. simpl. lra. + * done. + + iIntros (v2) "(%m' & Hm & %Hmvalid' & %Hmv' & %Hmsize' & %Hmsubset)". + iApply "HΦ". iExists m'. + repeat iSplit; try done. + * iPureIntro. lia. + * iPureIntro. simpl. intro Hfalse; subst. + apply Hneq. apply Hmvalid'; try done. + -- by eapply lookup_weaken_is_Some. + -- erewrite lookup_total_correct; last eapply lookup_weaken; try done. + by erewrite lookup_total_correct. + * iDestruct "Hm" as "(%&%&%&%&%&H)". iPureIntro. + eapply map_Forall_lookup_1 in H2; last done. + lia. + - rewrite /compute_hash_from_leaf. + wp_pures. rewrite -/compute_hash_from_leaf. + inversion Htrelate; subst. + wp_pures. inversion Htvalid; subst. + inversion Hvmatch; subst. + + wp_apply wp_list_head; try done. iIntros (?) "[%|%Hl]". + { naive_solver. } + destruct Hl as (?&?&?&?); subst. inversion H; subst. + wp_pures. + wp_apply wp_list_tail; try done. + iIntros (l') "%". + wp_pures. + wp_apply wp_root_hash_value_program; try done. + iIntros (?) "->". + iAssert (€ ((nnreal_nat (S n) * amortized_error (val_size - 1) max_hash_size)%NNR) ∗ + € (amortized_error (val_size - 1) max_hash_size)%NNR)%I with "[Herr]" as "[Herr Herr']". + { iApply ec_split. iApply (ec_spend_irrel with "[$]"). + simpl. lra. + } + wp_apply ("IH" with "[][][][][][][][$H][$Herr]"); try done. + * iPureIntro. lia. + * iIntros (retv) "(%m' & %Htvalid' & H & %Hmvalid' & %Hmsize' & %Hneq' & %Hnonneg)". + wp_pures. + replace (_*_+_)%Z with (Z.of_nat (Z.to_nat retv * 2 ^ val_bit_size + root_hash_value tree2)); last first. + { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul. f_equal; first lia. + apply Z2Nat.inj_pow. + } + wp_apply (wp_insert_amortized with "[$H $Herr']"). + -- lia. + -- lia. + -- iPureIntro. done. + -- iIntros (hv) "(%m''&Hm'' & %Hcoll_free' & %Hmsome'' & %Hsize'' & %Hsubset'')". + iApply "HΦ". + iExists m''. + repeat iSplit; try done. + ++ iPureIntro. etrans; exact. + ++ iPureIntro. lia. + ++ simpl. iPureIntro. + intro; subst. apply Hneq'. + assert (Z.to_nat retv * 2 ^ val_bit_size + root_hash_value tree2 = + root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2); last first. + { assert (Z.to_nat retv = + root_hash_value tree1 ); try lia. + assert (Z.to_nat retv * 2 ^ val_bit_size = + root_hash_value tree1 * 2 ^ val_bit_size); try lia. + rewrite <- Nat.mul_cancel_r; try done. + lia. + } + apply Hcoll_free'; try done. + ** eapply lookup_weaken_is_Some; try done. + etrans; exact. + ** erewrite lookup_total_correct; last done. + erewrite lookup_total_correct; last eapply lookup_weaken; try done. + etrans; exact. + ++ iDestruct "Hm''" as "(%&%&%&%&%&%&H)". + iPureIntro. eapply map_Forall_lookup_1 in H6; last done. lia. + + wp_apply wp_list_head; try done. iIntros (?) "[%|%Hl]". + { naive_solver. } + destruct Hl as (?&?&?&?); subst. inversion H; subst. + wp_pures. + wp_apply wp_list_tail; try done. + iIntros (l') "%". + wp_pures. + iAssert (€ ((nnreal_nat (S n) * amortized_error (val_size - 1) max_hash_size)%NNR) ∗ + € (amortized_error (val_size - 1) max_hash_size)%NNR)%I with "[Herr]" as "[Herr Herr']". + { iApply ec_split. iApply (ec_spend_irrel with "[$]"). + simpl. lra. + } + wp_apply ("IH1" with "[][][][][][][][$H][$Herr]"); try done. + * iPureIntro. lia. + * iIntros (retv) "(%m' & %Htvalid' & H & %Hmvalid' & %Hmsize' & %Hneq' & %Hnonneg)". + wp_pures. + wp_apply wp_root_hash_value_program; try done. + iIntros (?) "->". + wp_pures. + replace (_*_+_)%Z with (Z.of_nat ((root_hash_value tree1) * 2 ^ val_bit_size + Z.to_nat retv)); last first. + { rewrite Nat2Z.inj_add. f_equal; try lia. rewrite Nat2Z.inj_mul. f_equal. + apply Z2Nat.inj_pow. + } + wp_apply (wp_insert_amortized with "[$H $Herr']"). + -- lia. + -- lia. + -- iPureIntro. done. + -- iIntros (hv) "(%m''&Hm'' & %Hcoll_free' & %Hmsome'' & %Hsize'' & %Hsubset'')". + iApply "HΦ". + iExists m''. + repeat iSplit; try done. + ++ iPureIntro. etrans; exact. + ++ iPureIntro. lia. + ++ simpl. iPureIntro. + intro; subst. apply Hneq'. + assert (root_hash_value tree1 * 2 ^ val_bit_size + Z.to_nat retv = + root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2); try lia. + apply Hcoll_free'; try done. + ** eapply lookup_weaken_is_Some; try done. + etrans; exact. + ** erewrite lookup_total_correct; last done. + erewrite lookup_total_correct; last eapply lookup_weaken; try done. + etrans; exact. + ++ iDestruct "Hm''" as "(%&%&%&%&%&%&H)". + iPureIntro. eapply map_Forall_lookup_1 in H6; last done. lia. + Qed. - End merkle_tree. From e9815b87a06c79d905d9b866b33549866014025b Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 1 Feb 2024 16:17:30 +0100 Subject: [PATCH 08/21] Start writing 2nd version of the code --- theories/ub_logic/merkle_tree.v | 36 ++++++++++++++++++++++++--------- 1 file changed, 27 insertions(+), 9 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 0ddc9da48..9957392b2 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -48,6 +48,33 @@ Section merkle_tree. Definition map_valid (m:gmap nat Z) : Prop := coll_free m. + + + Inductive tree_value_match: merkle_tree -> nat -> list bool -> Prop:= + | tree_value_match_lf h lf: tree_value_match (Leaf h lf) lf [] + | tree_value_match_left h l r xs v: + tree_value_match l v xs -> + tree_value_match (Branch h l r) v (true::xs) + | tree_value_match_right h l r xs v: + tree_value_match r v xs -> + tree_value_match (Branch h l r) v (false::xs). + + Inductive possible_proof: list bool -> list nat -> Prop:= + | possible_proof_lf: possible_proof [] [] + | possible_proof_br b path hashlist hash: + possible_proof path hashlist -> + hash < 2^val_bit_size -> + possible_proof (b::path) (hash::hashlist). + + Inductive correct_proof: merkle_tree -> list bool -> list nat -> Prop := + | correct_proof_lf h l: correct_proof (Leaf h l) [] [] + | correct_proof_left ltree rtree h path hashlist: + correct_proof (ltree) path hashlist -> + correct_proof (Branch h ltree rtree) (true::path) (root_hash_value rtree::hashlist) + | correct_proof_right ltree rtree h path hashlist: + correct_proof (rtree) path hashlist -> + correct_proof (Branch h ltree rtree) (false::path) (root_hash_value ltree::hashlist). + Definition root_hash_value_program : val := λ: "ltree", @@ -77,15 +104,6 @@ Section merkle_tree. . - Inductive tree_value_match: merkle_tree -> nat -> list bool -> Prop:= - | tree_value_match_lf h lf: tree_value_match (Leaf h lf) lf [] - | tree_value_match_left h l r xs v: - tree_value_match l v xs -> - tree_value_match (Branch h l r) v (true::xs) - | tree_value_match_right h l r xs v: - tree_value_match r v xs -> - tree_value_match (Branch h l r) v (false::xs). - (** Lemmas *) Lemma wp_root_hash_value_program n lt tree E: {{{ ⌜tree_relate n lt tree⌝ }}} From 17c0c8c3378a7d2adbdc1460710bfd9a5da010c2 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 2 Feb 2024 13:23:41 +0100 Subject: [PATCH 09/21] merkle tree done --- theories/ub_logic/merkle_tree.v | 435 +++++++++++++++++--------------- 1 file changed, 226 insertions(+), 209 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 9957392b2..27f13c15e 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -9,8 +9,8 @@ Section merkle_tree. Variables val_bit_size':nat. Variables max_hash_size : nat. Definition val_bit_size : nat := S val_bit_size'. - Definition val_size:nat := (2^val_bit_size)-1. - Variable (Hineq: (max_hash_size <= val_size)%nat). + Definition val_size_for_hash:nat := (2^val_bit_size)-1. + 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. @@ -50,30 +50,31 @@ Section merkle_tree. Definition map_valid (m:gmap nat Z) : Prop := coll_free m. - Inductive tree_value_match: merkle_tree -> nat -> list bool -> Prop:= - | tree_value_match_lf h lf: tree_value_match (Leaf h lf) lf [] - | tree_value_match_left h l r xs v: - tree_value_match l v xs -> - tree_value_match (Branch h l r) v (true::xs) - | tree_value_match_right h l r xs v: - tree_value_match r v xs -> - tree_value_match (Branch h l r) v (false::xs). + Inductive tree_leaf_value_match: merkle_tree -> nat -> list (bool*nat) -> Prop:= + | tree_value_match_lf h lf: tree_leaf_value_match (Leaf h lf) lf [] + | tree_leaf_value_match_left h l r xs v rhash: + tree_leaf_value_match l v xs-> + tree_leaf_value_match (Branch h l r) v ((true,rhash)::xs) + | tree_value_match_right h l r xs v lhash: + tree_leaf_value_match r v xs -> + tree_leaf_value_match (Branch h l r) v ((false,lhash)::xs). - Inductive possible_proof: list bool -> list nat -> Prop:= - | possible_proof_lf: possible_proof [] [] - | possible_proof_br b path hashlist hash: - possible_proof path hashlist -> + (*This ensures all numbers in the proof are smaller than 2^val_bit_size*) + Inductive possible_proof: list (bool*nat) -> Prop:= + | possible_proof_lf: possible_proof [] + | possible_proof_br b hash prooflist: + possible_proof prooflist -> hash < 2^val_bit_size -> - possible_proof (b::path) (hash::hashlist). + possible_proof ((b,hash)::prooflist). - Inductive correct_proof: merkle_tree -> list bool -> list nat -> Prop := - | correct_proof_lf h l: correct_proof (Leaf h l) [] [] - | correct_proof_left ltree rtree h path hashlist: - correct_proof (ltree) path hashlist -> - correct_proof (Branch h ltree rtree) (true::path) (root_hash_value rtree::hashlist) - | correct_proof_right ltree rtree h path hashlist: - correct_proof (rtree) path hashlist -> - correct_proof (Branch h ltree rtree) (false::path) (root_hash_value ltree::hashlist). + Inductive correct_proof: merkle_tree -> list (bool*nat) -> Prop := + | correct_proof_lf h l: correct_proof (Leaf h l) [] + | correct_proof_left ltree rtree h prooflist: + correct_proof (ltree) prooflist -> + correct_proof (Branch h ltree rtree) ((true, root_hash_value rtree)::prooflist) + | correct_proof_right ltree rtree h prooflist: + correct_proof (rtree) prooflist -> + correct_proof (Branch h ltree rtree) ((false, root_hash_value ltree)::prooflist). Definition root_hash_value_program : val := @@ -84,25 +85,20 @@ Section merkle_tree. end. Definition compute_hash_from_leaf : val := - rec: "compute_hash_from_leaf" "ltree" "lhmf" "ll" "lleaf" := - match: "ltree" with - | InjL "x" => "lhmf" "lleaf" - | InjR "x" => let: "b" := (match: list_head "ll" with - | SOME "a" => "a" - | NONE => #() - end - ) in - let: "ll'" := list_tail "ll" in - let, ("notneeded", "l", "r") := "x" in - if: "b" - then "lhmf" - (("compute_hash_from_leaf" "l" "lhmf" "ll'" "lleaf")*#(2^val_bit_size)+ - root_hash_value_program "r") - else "lhmf" - ((root_hash_value_program "l")*#(2^val_bit_size)+("compute_hash_from_leaf" "r" "lhmf" "ll'" "lleaf")) - end - - . + rec: "compute_hash_from_leaf" "lhmf" "lproof" "lleaf" := + match: list_head "lproof" with + | SOME "head" => + let: "lproof'" := list_tail "lproof" in + let, ("b", "hash") := "head" in + if: "b" + then "lhmf" + (("compute_hash_from_leaf" "lhmf" "lproof'" "lleaf")*#(2^val_bit_size)+ + "hash") + else "lhmf" + ("hash"*#(2^val_bit_size)+("compute_hash_from_leaf" "lhmf" "lproof'" "lleaf")) + + | NONE => "lhmf" "lleaf" + end. (** Lemmas *) Lemma wp_root_hash_value_program n lt tree E: @@ -128,40 +124,55 @@ Section merkle_tree. by eapply lookup_weaken. Qed. + Lemma coll_free_lemma m v v' k: + coll_free m -> m!!v=Some k -> m!! v' = Some k -> v= v'. + Proof. + intros H ? ?. + apply H; try done. + repeat erewrite lookup_total_correct; try done. + Qed. + (** Spec *) - Lemma wp_compute_hash_from_leaf_correct (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (path:list bool) llist f E: + 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: {{{ ⌜tree_relate height ltree tree⌝ ∗ ⌜tree_valid tree m⌝ ∗ - hashfun_amortized (val_size-1)%nat max_hash_size f m ∗ - ⌜is_list path llist⌝ ∗ - ⌜tree_value_match tree v path⌝ ∗ + hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ + ⌜is_list proof lproof⌝ ∗ + ⌜correct_proof tree proof⌝ ∗ + ⌜tree_leaf_value_match tree v proof⌝ ∗ ⌜map_valid m⌝ }}} - compute_hash_from_leaf ltree f llist (#v) @ E + compute_hash_from_leaf f lproof (#v) @ E {{{ (retv:Z), RET #retv; - hashfun_amortized (val_size-1) max_hash_size f m ∗ + hashfun_amortized (val_size_for_hash) max_hash_size f m ∗ ⌜retv = root_hash_value tree⌝ }}}. Proof. - iIntros (Φ) "(%Htrelate&%Htvalid&H&%Hlsit&%Hvmatch&%Hmvalid) HΦ". - iInduction tree as [|] "IH" - forall (height ltree v path llist f Htrelate Htvalid Hlsit Hvmatch Hmvalid Φ). - - rewrite /compute_hash_from_leaf. - wp_pures. inversion Htrelate; subst. - wp_match. - inversion Htrelate. inversion Htvalid. inversion Hvmatch. subst. + iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hlist & %Hcorrect & %Hvmatch & %Hmvalid) HΦ". + iInduction tree as [hash leaf|hash tree1 Htree1 tree2 Htree2] "IH" + forall (height ltree m proof lproof Φ + Htrelate Htvalid Hlist Hcorrect Hvmatch Hmvalid). + - rewrite /compute_hash_from_leaf. wp_pures. rewrite -/compute_hash_from_leaf. + wp_apply wp_list_head; first done. + iIntros (?) "[[-> ->]|%]"; last first. + { inversion Hcorrect; subst. destruct H as [?[?[??]]]. + inversion H. } + wp_pures. inversion Htvalid; inversion Hvmatch. subst. wp_apply (wp_hashfun_prev_amortized with "[$]"). + lia. - + done. - + iIntros. iApply "HΦ". iFrame. by iPureIntro. - - rewrite /compute_hash_from_leaf. - inversion Htrelate. inversion Htvalid. inversion Hvmatch; subst. - + wp_pures. wp_apply wp_list_head; first done. iIntros (v') "[[%%]|(%&%&%&%)]"; first done. - subst. inversion H; subst. wp_pures. rewrite -/compute_hash_from_leaf. - wp_apply wp_list_tail; first done. iIntros (v') "%". wp_pures. - wp_apply wp_root_hash_value_program; try done. - iIntros (x) "->". - wp_apply ("IH" with "[][][][][][H][HΦ]"); try done. - iModIntro. iIntros (?) "[H ->]". + + done. + + iIntros "H". iApply "HΦ"; iFrame. + done. + - rewrite /compute_hash_from_leaf. wp_pures. + rewrite -/compute_hash_from_leaf. + wp_apply wp_list_head; first done. + iIntros (head) "[[->->]|(%&%&->&->)]". + { inversion Hcorrect. } + wp_pures. wp_apply wp_list_tail; first done. + iIntros (tail) "%Htail". + inversion Hcorrect; wp_pures. + + inversion Htrelate. inversion Htvalid. inversion Hvmatch; subst; last done. + wp_apply ("IH" with "[][][][][][][$]"); try done. + iIntros (lhash) "[H ->]". wp_pures. replace (_*_+_)%Z with (Z.of_nat (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2)); last first. { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul. f_equal. @@ -170,15 +181,11 @@ Section merkle_tree. wp_apply (wp_hashfun_prev_amortized with "H"). * lia. * done. - * iIntros "H". iApply "HΦ". iFrame. - done. - + wp_pures. wp_apply wp_list_head; first done. iIntros (v') "[[%%]|(%&%&%&%)]"; first done. - subst. inversion H; subst. wp_pures. rewrite -/compute_hash_from_leaf. - wp_apply wp_list_tail; first done. iIntros (v') "%". wp_pures. - wp_apply ("IH1" with "[][][][][][H][HΦ]"); try done. - iModIntro. iIntros (?) "[H ->]". - wp_apply wp_root_hash_value_program; try done. - iIntros (x) "->". + * iIntros "H". iApply "HΦ". + iFrame. done. + + inversion Htrelate. inversion Htvalid. inversion Hvmatch; subst; first done. + wp_apply ("IH1" with "[][][][][][][$]"); try done. + iIntros (rhash) "[H ->]". wp_pures. replace (_*_+_)%Z with (Z.of_nat (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2)); last first. { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul. f_equal. @@ -187,159 +194,169 @@ Section merkle_tree. wp_apply (wp_hashfun_prev_amortized with "H"). * lia. * done. - * iIntros "H". iApply "HΦ". iFrame. - done. + * iIntros "H". iApply "HΦ". + iFrame. done. Qed. - - Lemma wp_compute_hash_from_leaf_incorrect (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v v':nat) (path:list bool) llist f E: + Lemma wp_compute_hash_from_leaf_incorrect (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v v':nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_relate height ltree tree⌝ ∗ ⌜tree_valid tree m⌝ ∗ - hashfun_amortized (val_size-1)%nat max_hash_size f m ∗ - ⌜is_list path llist⌝ ∗ - ⌜tree_value_match tree v path⌝ ∗ + hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ + ⌜is_list proof lproof⌝ ∗ + ⌜possible_proof proof⌝ ∗ + ⌜tree_leaf_value_match tree v proof⌝ ∗ + ⌜v ≠ v'⌝ ∗ ⌜map_valid m⌝ ∗ ⌜ size m + (S height) <= max_hash_size⌝ ∗ - ⌜v ≠ v'⌝ ∗ - € (nnreal_nat (S height) * amortized_error (val_size-1)%nat max_hash_size)%NNR + € (nnreal_nat (S height) * amortized_error (val_size_for_hash)%nat max_hash_size)%NNR }}} - compute_hash_from_leaf ltree f llist (#v') @ E + compute_hash_from_leaf f lproof (#v') @ E {{{ (retv:Z), RET #retv; ∃ m', ⌜m ⊆ m'⌝ ∗ - hashfun_amortized (val_size-1) max_hash_size f m' ∗ + hashfun_amortized (val_size_for_hash) max_hash_size f m' ∗ ⌜map_valid m'⌝ ∗ ⌜size (m') <= size m + (S height)⌝ ∗ ⌜retv ≠ root_hash_value tree⌝ ∗ - ⌜(0 <= retv)%Z⌝ + ⌜(0 <= retv < 2^val_bit_size)%Z⌝ }}}. Proof. - iIntros (Φ) "(%Htrelate&%Htvalid&H&%Hlsit&%Hvmatch&%Hmvalid&%Hmsize&%Hneq&Herr) HΦ". + iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hlist & %Hpossible & %Hvmatch & %Hneq & %Hmvalid & %Hmsize & Herr) HΦ". iInduction tree as [|] "IH" - forall (height ltree m path llist Φ Htrelate Htvalid Hlsit Hvmatch Hmvalid Hmsize Hneq). - - rewrite /compute_hash_from_leaf. - wp_pures. inversion Htrelate; subst. - wp_match. - inversion Htrelate. inversion Htvalid. inversion Hvmatch. subst. - wp_apply (wp_insert_amortized with "[$H Herr]"). - + lia. - + lia. - + iSplitL. - * assert (∀ x, (nnreal_nat 1 * x)%NNR = x) as ->; last iFrame. - intros. apply nnreal_ext. simpl. lra. - * done. - + iIntros (v2) "(%m' & Hm & %Hmvalid' & %Hmv' & %Hmsize' & %Hmsubset)". - iApply "HΦ". iExists m'. + forall (height ltree m proof lproof Φ Htrelate Htvalid Hlist Hpossible Hvmatch Hmvalid Hmsize). + - inversion Htrelate; subst. rewrite /compute_hash_from_leaf. wp_pures. + rewrite -/compute_hash_from_leaf. inversion Hvmatch; subst. + wp_apply wp_list_head; first done. + iIntros (?) "[[_ ->]|(%&%&%&%)]"; last done. + wp_pures. + wp_apply (wp_insert_amortized with "[$H Herr]"); try lia. + + iSplit; try done. iApply ec_spend_irrel; last done. + simpl. lra. + + iIntros (hash_value') "(%m' & H & %Hvalid' & %Hmfound & %Hmsize' & %Hmsubset)". + iApply "HΦ". + iExists _. repeat iSplit; try done. - * iPureIntro. lia. - * iPureIntro. simpl. intro Hfalse; subst. - apply Hneq. apply Hmvalid'; try done. - -- by eapply lookup_weaken_is_Some. - -- erewrite lookup_total_correct; last eapply lookup_weaken; try done. - by erewrite lookup_total_correct. - * iDestruct "Hm" as "(%&%&%&%&%&H)". iPureIntro. - eapply map_Forall_lookup_1 in H2; last done. - lia. - - rewrite /compute_hash_from_leaf. - wp_pures. rewrite -/compute_hash_from_leaf. + * iPureIntro; lia. + * simpl. + inversion Htvalid; subst. + iPureIntro. intro; subst. apply Hneq. eapply coll_free_lemma; try done. + by erewrite lookup_weaken. + * 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 Hvmatch. } + wp_pures. wp_apply wp_list_tail; first done. + iIntros (proof') "%Hproof'". + wp_pures. inversion Hpossible; subst. + wp_pures. inversion Htrelate; subst. - wp_pures. inversion Htvalid; subst. - inversion Hvmatch; subst. - + wp_apply wp_list_head; try done. iIntros (?) "[%|%Hl]". - { naive_solver. } - destruct Hl as (?&?&?&?); subst. inversion H; subst. - wp_pures. - wp_apply wp_list_tail; try done. - iIntros (l') "%". + iAssert (€ ((nnreal_nat (S n) * 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. + } + inversion Hvmatch; inversion Htvalid; subst; wp_pures. + + wp_apply ("IH" with "[][][][][][][][$H][$Herr]"); try done. + { iPureIntro; lia. } + iIntros (lefthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashneq & %Hlefthashsize')". wp_pures. - wp_apply wp_root_hash_value_program; try done. - iIntros (?) "->". - iAssert (€ ((nnreal_nat (S n) * amortized_error (val_size - 1) max_hash_size)%NNR) ∗ - € (amortized_error (val_size - 1) max_hash_size)%NNR)%I with "[Herr]" as "[Herr Herr']". - { iApply ec_split. iApply (ec_spend_irrel with "[$]"). - simpl. lra. - } - wp_apply ("IH" with "[][][][][][][][$H][$Herr]"); try done. - * iPureIntro. lia. - * iIntros (retv) "(%m' & %Htvalid' & H & %Hmvalid' & %Hmsize' & %Hneq' & %Hnonneg)". - wp_pures. - replace (_*_+_)%Z with (Z.of_nat (Z.to_nat retv * 2 ^ val_bit_size + root_hash_value tree2)); last first. - { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul. f_equal; first lia. - apply Z2Nat.inj_pow. - } - wp_apply (wp_insert_amortized with "[$H $Herr']"). - -- lia. - -- lia. - -- iPureIntro. done. - -- iIntros (hv) "(%m''&Hm'' & %Hcoll_free' & %Hmsome'' & %Hsize'' & %Hsubset'')". - iApply "HΦ". - iExists m''. - repeat iSplit; try done. - ++ iPureIntro. etrans; exact. - ++ iPureIntro. lia. - ++ simpl. iPureIntro. - intro; subst. apply Hneq'. - assert (Z.to_nat retv * 2 ^ val_bit_size + root_hash_value tree2 = - root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2); last first. - { assert (Z.to_nat retv = - root_hash_value tree1 ); try lia. - assert (Z.to_nat retv * 2 ^ val_bit_size = - root_hash_value tree1 * 2 ^ val_bit_size); try lia. - rewrite <- Nat.mul_cancel_r; try done. - lia. - } - apply Hcoll_free'; try done. - ** eapply lookup_weaken_is_Some; try done. - etrans; exact. - ** erewrite lookup_total_correct; last done. - erewrite lookup_total_correct; last eapply lookup_weaken; try done. - etrans; exact. - ++ iDestruct "Hm''" as "(%&%&%&%&%&%&H)". - iPureIntro. eapply map_Forall_lookup_1 in H6; last done. lia. - + wp_apply wp_list_head; try done. iIntros (?) "[%|%Hl]". - { naive_solver. } - destruct Hl as (?&?&?&?); subst. inversion H; subst. - wp_pures. - wp_apply wp_list_tail; try done. - iIntros (l') "%". + 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']"). + * 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. + -- iPureIntro. simpl. + intro; subst. apply Hlefthashneq. + 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 _]. + lia. + Unshelve. + ++ by inversion H15. + ++ by inversion Hpossible. + -- 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 [? H3]. + apply Zle_lt_succ in H3. + 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 (righthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hrighthashneq & %Hrighthashsize')". wp_pures. - iAssert (€ ((nnreal_nat (S n) * amortized_error (val_size - 1) max_hash_size)%NNR) ∗ - € (amortized_error (val_size - 1) max_hash_size)%NNR)%I with "[Herr]" as "[Herr Herr']". - { iApply ec_split. iApply (ec_spend_irrel with "[$]"). - simpl. lra. - } - wp_apply ("IH1" with "[][][][][][][][$H][$Herr]"); try done. - * iPureIntro. lia. - * iIntros (retv) "(%m' & %Htvalid' & H & %Hmvalid' & %Hmsize' & %Hneq' & %Hnonneg)". - wp_pures. - wp_apply wp_root_hash_value_program; try done. - iIntros (?) "->". - wp_pures. - replace (_*_+_)%Z with (Z.of_nat ((root_hash_value tree1) * 2 ^ val_bit_size + Z.to_nat retv)); last first. - { rewrite Nat2Z.inj_add. f_equal; try lia. rewrite Nat2Z.inj_mul. f_equal. - apply Z2Nat.inj_pow. - } - wp_apply (wp_insert_amortized with "[$H $Herr']"). - -- lia. - -- lia. - -- iPureIntro. done. - -- iIntros (hv) "(%m''&Hm'' & %Hcoll_free' & %Hmsome'' & %Hsize'' & %Hsubset'')". - iApply "HΦ". - iExists m''. - repeat iSplit; try done. - ++ iPureIntro. etrans; exact. - ++ iPureIntro. lia. - ++ simpl. iPureIntro. - intro; subst. apply Hneq'. - assert (root_hash_value tree1 * 2 ^ val_bit_size + Z.to_nat retv = - root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2); try lia. - apply Hcoll_free'; try done. - ** eapply lookup_weaken_is_Some; try done. - etrans; exact. - ** erewrite lookup_total_correct; last done. - erewrite lookup_total_correct; last eapply lookup_weaken; try done. - etrans; exact. - ++ iDestruct "Hm''" as "(%&%&%&%&%&%&H)". - iPureIntro. eapply map_Forall_lookup_1 in H6; last done. lia. + 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']"). + * 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. + -- iPureIntro. simpl. + intro; subst. apply Hrighthashneq. + 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 _]. + lia. + Unshelve. + ++ by inversion H15. + ++ 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 [? H3]. + apply Zle_lt_succ in H3. + 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. From 3a452cae7481e47c2c36d332fa16e34fb5f14396 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 2 Feb 2024 14:01:29 +0100 Subject: [PATCH 10/21] Added a helper function --- theories/ub_logic/merkle_tree.v | 83 ++++++++++++++++++++++++++++++++- 1 file changed, 82 insertions(+), 1 deletion(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 27f13c15e..224d667fb 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -358,6 +358,87 @@ Section merkle_tree. assert (1<=2 ^val_bit_size); last lia. clear. induction val_bit_size; simpl; lia. Qed. - + + (** checker*) + Definition merkle_tree_decider_program : val := + λ: "correct_root_hash" "lhmf", + (λ: "lproof" "lleaf", + "correct_root_hash" = compute_hash_from_leaf "lhmf" "lproof" "lleaf" + ). + + Lemma merkle_tree_decider_program_spec ltree tree (m:gmap nat Z) f: + {{{ ⌜tree_relate height ltree tree⌝ ∗ + ⌜tree_valid 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 ∗ + (** correct*) + (∀ lproof proof v m', + {{{ + ⌜m⊆m'⌝ ∗ + hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' ∗ + ⌜is_list proof lproof⌝ ∗ + ⌜correct_proof tree proof⌝ ∗ + ⌜tree_leaf_value_match tree v proof⌝∗ + ⌜map_valid m'⌝ + + }}} + checker lproof (#v) + {{{ RET #true; + hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' + }}}) ∗ + (** incorrect*) + (∀ lproof proof v v' m', + {{{ ⌜m⊆m'⌝ ∗ + hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' ∗ + ⌜is_list proof lproof⌝ ∗ + ⌜possible_proof proof⌝ ∗ + ⌜tree_leaf_value_match tree v proof⌝ ∗ + ⌜v ≠ v'⌝ ∗ + ⌜map_valid m'⌝ ∗ + ⌜ size m' + (S height) <= max_hash_size⌝ ∗ + € (nnreal_nat (S height) * amortized_error (val_size_for_hash)%nat max_hash_size)%NNR + + }}} + checker lproof (#v') + {{{ RET #false; + ∃ m'', ⌜m' ⊆ m''⌝ ∗ + hashfun_amortized (val_size_for_hash) max_hash_size f m'' ∗ + ⌜map_valid m''⌝ ∗ + ⌜size (m'') <= size m' + (S height)⌝ + }}}) + }}}. + Proof. + iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hmvalid) IH". + rewrite /merkle_tree_decider_program. + wp_pures. iModIntro. + iApply "IH". iFrame. + iSplit. + - iIntros (?????). iModIntro. + iIntros "(%&H&%&%&%&%)IH". + wp_pures. + wp_apply (wp_compute_hash_from_leaf_correct with "[$H]"). + + repeat iSplit; iPureIntro; try done. + by eapply tree_valid_superset. + + iIntros (?) "[H ->]". wp_pures. + iModIntro. case_bool_decide; last done. + iApply "IH"; iFrame. + - iIntros (??????). + iModIntro. + iIntros "(%&H&%&%&%&%&%&%&Herr) IH". + wp_pures. + wp_apply (wp_compute_hash_from_leaf_incorrect with "[$H $Herr]"). + + repeat iSplit; iPureIntro; try done. + by eapply tree_valid_superset. + + iIntros (?) "(%&%&H&%&%&%&%)". + wp_pures. iModIntro. + case_bool_decide as K; first by inversion K. + iApply "IH". + iExists _; iFrame. + repeat iSplit; try done. + Qed. End merkle_tree. From 39cd2dcf6730bb73ebd99a00a693192e8693601a Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 2 Feb 2024 15:47:24 +0100 Subject: [PATCH 11/21] add lemma for incorrect proof --- theories/ub_logic/merkle_tree.v | 63 ++++++++++++++++++++++++--------- 1 file changed, 47 insertions(+), 16 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 224d667fb..b9a721ff2 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -60,12 +60,17 @@ Section merkle_tree. tree_leaf_value_match (Branch h l r) v ((false,lhash)::xs). (*This ensures all numbers in the proof are smaller than 2^val_bit_size*) - Inductive possible_proof: list (bool*nat) -> Prop:= - | possible_proof_lf: possible_proof [] - | possible_proof_br b hash prooflist: - possible_proof prooflist -> + Inductive possible_proof: merkle_tree -> list (bool*nat) -> Prop:= + | possible_proof_lf h v: possible_proof (Leaf h v) [] + | possible_proof_br_left h ltree rtree hash prooflist: + possible_proof ltree prooflist -> hash < 2^val_bit_size -> - possible_proof ((b,hash)::prooflist). + possible_proof (Branch h ltree rtree) ((true,hash)::prooflist) + | possible_proof_br_right h ltree rtree hash prooflist: + possible_proof rtree prooflist -> + hash < 2^val_bit_size -> + possible_proof (Branch h ltree rtree) ((false,hash)::prooflist). + Inductive correct_proof: merkle_tree -> list (bool*nat) -> Prop := | correct_proof_lf h l: correct_proof (Leaf h l) [] @@ -75,6 +80,20 @@ Section merkle_tree. | correct_proof_right ltree rtree h prooflist: correct_proof (rtree) prooflist -> correct_proof (Branch h ltree rtree) ((false, root_hash_value ltree)::prooflist). + + Inductive incorrect_proof : merkle_tree -> list (bool*nat) -> Prop := + | incorrect_proof_base_left ltree rtree h v prooflist: + v ≠ root_hash_value rtree -> + incorrect_proof (Branch h ltree rtree) ((true, v)::prooflist) + | incorrect_proof_next_left ltree rtree h prooflist: + incorrect_proof ltree prooflist -> + incorrect_proof (Branch h ltree rtree) ((true, root_hash_value rtree)::prooflist) + | incorrect_proof_base_right ltree rtree h v prooflist: + v ≠ root_hash_value ltree -> + incorrect_proof (Branch h ltree rtree) ((false, v)::prooflist) + | incorrect_proof_next_right ltree rtree h prooflist: + incorrect_proof rtree prooflist -> + incorrect_proof (Branch h ltree rtree) ((false, root_hash_value ltree)::prooflist). Definition root_hash_value_program : val := @@ -132,6 +151,19 @@ Section merkle_tree. repeat erewrite lookup_total_correct; try done. Qed. + Lemma proof_correct_iff_not_incorrect tree proof: + possible_proof tree proof -> correct_proof tree proof -> incorrect_proof tree proof -> False. + Proof. + revert proof. + induction tree; intros proof H1 H2 H3 . + - inversion H3. + - inversion H1; inversion H2; inversion H3; subst; try done. + + inversion H14; subst. inversion H9; subst. done. + + inversion H9; inversion H14; subst. eapply IHtree1; try done. + + inversion H14; inversion H9; subst. done. + + inversion H9; inversion H14; subst. eapply IHtree2; try done. + 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: {{{ ⌜tree_relate height ltree tree⌝ ∗ @@ -203,7 +235,7 @@ Section merkle_tree. ⌜tree_valid tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ ⌜is_list proof lproof⌝ ∗ - ⌜possible_proof proof⌝ ∗ + ⌜possible_proof tree proof⌝ ∗ ⌜tree_leaf_value_match tree v proof⌝ ∗ ⌜v ≠ v'⌝ ∗ ⌜map_valid m⌝ ∗ @@ -258,15 +290,14 @@ Section merkle_tree. { inversion Hvmatch. } wp_pures. wp_apply wp_list_tail; first done. iIntros (proof') "%Hproof'". - wp_pures. inversion Hpossible; subst. - wp_pures. + wp_pures. inversion Htrelate; subst. iAssert (€ ((nnreal_nat (S n) * 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. } - inversion Hvmatch; inversion Htvalid; subst; wp_pures. + inversion Hpossible; inversion Hvmatch; inversion Htvalid; subst; wp_pures; try done. + wp_apply ("IH" with "[][][][][][][][$H][$Herr]"); try done. { iPureIntro; lia. } iIntros (lefthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashneq & %Hlefthashsize')". @@ -298,14 +329,14 @@ Section merkle_tree. epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. lia. Unshelve. - ++ by inversion H15. + ++ by inversion H19. ++ by inversion Hpossible. -- 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 [? H3]. - apply Zle_lt_succ in H3. + 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. @@ -341,7 +372,7 @@ Section merkle_tree. epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. lia. Unshelve. - ++ by inversion H15. + ++ 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. @@ -350,8 +381,8 @@ Section merkle_tree. 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 [? H3]. - apply Zle_lt_succ in H3. + 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. @@ -395,7 +426,7 @@ Section merkle_tree. {{{ ⌜m⊆m'⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' ∗ ⌜is_list proof lproof⌝ ∗ - ⌜possible_proof proof⌝ ∗ + ⌜possible_proof tree proof⌝ ∗ ⌜tree_leaf_value_match tree v proof⌝ ∗ ⌜v ≠ v'⌝ ∗ ⌜map_valid m'⌝ ∗ From c57e605ddfb26ef3f10b40108f0c24dd07f32d32 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 2 Feb 2024 16:23:25 +0100 Subject: [PATCH 12/21] Prove 2 out of four cases of the incorrect proof lemma --- theories/ub_logic/merkle_tree.v | 130 ++++++++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index b9a721ff2..282e4a133 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -390,6 +390,136 @@ Section merkle_tree. induction val_bit_size; simpl; lia. Qed. + Lemma wp_compute_hash_from_leaf_incorrect_proof (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: + {{{ ⌜tree_relate height 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⌝ ∗ + ⌜incorrect_proof tree proof ⌝ ∗ + ⌜tree_leaf_value_match tree v proof⌝ ∗ + ⌜map_valid m⌝ ∗ + ⌜ size m + (S height) <= max_hash_size⌝ ∗ + € (nnreal_nat (S height) * 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 height)⌝ ∗ + ⌜retv ≠ root_hash_value tree⌝ ∗ + ⌜(0 <= retv < 2^val_bit_size)%Z⌝ + }}}. + Proof. + iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hlist & %Hposs & %Hincorrect & %Hvmatch & %Hmvalid & %Hmsize & Herr) HΦ". + iInduction tree as [|] "IH" + forall (height ltree m proof lproof Φ Htrelate Htvalid Hlist Hposs Hincorrect Hvmatch Hmvalid Hmsize). + - inversion Hincorrect. + - rewrite /compute_hash_from_leaf. wp_pures. + rewrite -/compute_hash_from_leaf. + wp_apply wp_list_head; first done. + iIntros (?) "[[->->]|(%head & %lproof' & -> & ->)]". + { inversion Hvmatch. } + wp_pures. wp_apply wp_list_tail; first done. + iIntros (proof') "%Hproof'". + wp_pures. inversion Htrelate; subst. + iAssert (€ ((nnreal_nat (S n) * 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. + } + inversion Hposs; inversion Hvmatch; inversion Htvalid; inversion Hincorrect; subst; wp_pures; try done. + + (*right neq guess right*) admit. + + (*incorrect happens above*) + wp_apply ("IH" with "[][][][][][][][][$H][$Herr]"); try done. + * iPureIntro; lia. + * iIntros (lefthash) "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashneq & %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 ->. apply Hlefthashneq. + inversion H27; subst. + assert (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2 = + Z.to_nat lefthash * 2 ^ val_bit_size + root_hash_value tree2) 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 _]. + lia. + 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. + + (*left neq guess left *) admit. + + (*incorrect happens above *) + wp_apply ("IH1" with "[][][][][][][][][$H][$Herr]"); try done. + * iPureIntro; lia. + * iIntros (righthash) "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hrighthashneq & %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 ->. apply Hrighthashneq. + inversion H27; subst. + assert (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2 = + root_hash_value tree1 * 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 _]. + lia. + 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. + Admitted. + (** checker*) Definition merkle_tree_decider_program : val := λ: "correct_root_hash" "lhmf", From 306d8485d852eb424437e60790d3efa45f0be789 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 2 Feb 2024 17:11:52 +0100 Subject: [PATCH 13/21] 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 282e4a133..ec564d703 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 := From 7c8e2b4ae5089e2a35ba365262a138c681443b89 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 5 Feb 2024 11:17:44 +0100 Subject: [PATCH 14/21] Improve spec of wp lemmas + prove converse of incorrect correct proof proposition --- theories/ub_logic/merkle_tree.v | 183 +++++++++++++++++--------------- 1 file changed, 99 insertions(+), 84 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index ec564d703..bca20d85c 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -25,26 +25,26 @@ Section merkle_tree. | Branch h _ _ => h end. - Inductive tree_relate: nat -> val -> merkle_tree -> Prop:= - | tree_relate_lf (hv v:nat): tree_relate 0 (InjLV (#hv, #v)) (Leaf hv v) - | tree_relate_br n (hv:nat) ll l lr r: - tree_relate n ll l -> - tree_relate n lr r -> - tree_relate (S n) (InjRV (#hv, ll, lr)) (Branch hv l r) - . + (* Inductive tree_relate: nat -> val -> merkle_tree -> Prop:= *) + (* | tree_relate_lf (hv v:nat): tree_relate 0 (InjLV (#hv, #v)) (Leaf hv v) *) + (* | tree_relate_br n (hv:nat) ll l lr r: *) + (* tree_relate n ll l -> *) + (* tree_relate n lr r -> *) + (* tree_relate (S n) (InjRV (#hv, ll, lr)) (Branch hv l r) *) + (* . *) - Inductive tree_valid: merkle_tree -> gmap nat Z -> Prop := + Inductive tree_valid: nat -> merkle_tree -> gmap nat Z -> Prop := |tree_valid_lf (h l:nat) m: h < 2^val_bit_size -> l < 2^leaf_bit_size -> m!!l%nat = Some (Z.of_nat h) -> - tree_valid (Leaf h l) m - |tree_valid_br (h:nat) l r m: - tree_valid l m -> - tree_valid r m -> + tree_valid 0 (Leaf h l) m + |tree_valid_br n (h:nat) l r m: + tree_valid n l m -> + tree_valid n r m -> h < 2^val_bit_size -> m!!((root_hash_value l)*2^val_bit_size + root_hash_value r)%nat=Some (Z.of_nat h) -> - tree_valid (Branch h l r) m. + tree_valid (S n) (Branch h l r) m. Definition map_valid (m:gmap nat Z) : Prop := coll_free m. @@ -96,12 +96,12 @@ Section merkle_tree. incorrect_proof (Branch h ltree rtree) ((false, root_hash_value ltree)::prooflist). - Definition root_hash_value_program : val := - λ: "ltree", - match: "ltree" with - | InjL "x" => Fst "x" - | InjR "x" => let, ("a", "b", "c") := "x" in "a" - end. + (* Definition root_hash_value_program : val := *) + (* λ: "ltree", *) + (* match: "ltree" with *) + (* | InjL "x" => Fst "x" *) + (* | InjR "x" => let, ("a", "b", "c") := "x" in "a" *) + (* end. *) Definition compute_hash_from_leaf : val := rec: "compute_hash_from_leaf" "lhmf" "lproof" "lleaf" := @@ -120,21 +120,22 @@ Section merkle_tree. end. (** Lemmas *) - Lemma wp_root_hash_value_program n lt tree E: - {{{ ⌜tree_relate n lt tree⌝ }}} - root_hash_value_program lt @ E - {{{ (retv:Z), RET #retv; ⌜retv = root_hash_value tree⌝}}}. - Proof. - iIntros (Φ) "%H HΦ". - rewrite /root_hash_value_program. wp_pures. - inversion H. - - wp_pures. iApply "HΦ". by iPureIntro. - - wp_pures. iApply "HΦ". by iPureIntro. - Qed. + (* Lemma wp_root_hash_value_program n lt tree E: *) + (* {{{ ⌜tree_relate n lt tree⌝ }}} *) + (* root_hash_value_program lt @ E *) + (* {{{ (retv:Z), RET #retv; ⌜retv = root_hash_value tree⌝}}}. *) + (* Proof. *) + (* iIntros (Φ) "%H HΦ". *) + (* rewrite /root_hash_value_program. wp_pures. *) + (* inversion H. *) + (* - wp_pures. iApply "HΦ". by iPureIntro. *) + (* - wp_pures. iApply "HΦ". by iPureIntro. *) + (* Qed. *) - Lemma tree_valid_superset m m' tree: - tree_valid tree m -> m ⊆ m' -> tree_valid tree m'. + Lemma tree_valid_superset n m m' tree: + tree_valid n tree m -> m ⊆ m' -> tree_valid n tree m'. Proof. + revert n. induction tree. - intros. inversion H; subst. constructor; try done. @@ -151,7 +152,7 @@ Section merkle_tree. repeat erewrite lookup_total_correct; try done. Qed. - Lemma proof_correct_iff_not_incorrect tree proof: + Lemma proof_correct_implies_not_incorrect tree proof: possible_proof tree proof -> correct_proof tree proof -> incorrect_proof tree proof -> False. Proof. revert proof. @@ -164,9 +165,25 @@ Section merkle_tree. + 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⌝ ∗ + Lemma proof_not_correct_implies_incorrect tree proof: + possible_proof tree proof -> (¬ correct_proof tree proof) -> incorrect_proof tree proof. + Proof. + revert proof. + induction tree; intros proof H1 H2. + - inversion H1; subst. exfalso. apply H2. constructor. + - inversion H1; subst. + + destruct (decide(hash = root_hash_value tree2)). + * subst. apply incorrect_proof_next_left. apply IHtree1; first done. + intro; apply H2. by constructor. + * by apply incorrect_proof_base_left. + + destruct (decide(hash = root_hash_value tree1)). + * subst. apply incorrect_proof_next_right. apply IHtree2; first done. + intro; apply H2. by constructor. + * by apply incorrect_proof_base_right. + Qed. + + Lemma wp_compute_hash_from_leaf_size (n:nat) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: + {{{ ⌜tree_valid n tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ ⌜is_list proof lproof⌝ ∗ ⌜possible_proof tree proof⌝ ∗ @@ -183,15 +200,16 @@ Section merkle_tree. ⌜(0 <= retv < 2^val_bit_size)%Z⌝ }}}. Proof. - iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hproof & %Hposs & %Hmvalid & %Hmsize &Herr) HΦ". + iIntros (Φ) "(%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). + forall (n v m proof lproof Φ + 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_pures. + inversion Htvalid; subst. wp_apply (wp_insert_amortized with "[$H Herr]"); try lia. + iSplit; try done. iApply ec_spend_irrel; last done. simpl. lra. @@ -204,8 +222,8 @@ Section merkle_tree. 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. + 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. @@ -218,15 +236,15 @@ Section merkle_tree. wp_pures. wp_apply wp_list_tail; first done. iIntros (proof') "%Hproof'". wp_pures. - inversion Htrelate; subst. + inversion Htvalid; 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. + inversion Hposs; 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. @@ -257,7 +275,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. - + wp_apply ("IH1" with "[][][][][][][$H][$Herr]"); try done. + + wp_apply ("IH1" with "[][][][][][$H][$Herr]"); try done. { iPureIntro; lia. } iIntros (lefthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashsize')". wp_pures. @@ -291,8 +309,7 @@ Section merkle_tree. (** 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: - {{{ ⌜tree_relate height ltree tree⌝ ∗ - ⌜tree_valid tree m⌝ ∗ + {{{ ⌜tree_valid height tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ ⌜is_list proof lproof⌝ ∗ ⌜correct_proof tree proof⌝ ∗ @@ -304,16 +321,16 @@ Section merkle_tree. ⌜retv = root_hash_value tree⌝ }}}. Proof. - iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hlist & %Hcorrect & %Hvmatch & %Hmvalid) HΦ". + iIntros (Φ) "(%Htvalid & H & %Hlist & %Hcorrect & %Hvmatch & %Hmvalid) HΦ". iInduction tree as [hash leaf|hash tree1 Htree1 tree2 Htree2] "IH" - forall (height ltree m proof lproof Φ - Htrelate Htvalid Hlist Hcorrect Hvmatch Hmvalid). + forall (height m proof lproof Φ + Htvalid Hlist Hcorrect Hvmatch Hmvalid). - rewrite /compute_hash_from_leaf. wp_pures. rewrite -/compute_hash_from_leaf. wp_apply wp_list_head; first done. iIntros (?) "[[-> ->]|%]"; last first. { inversion Hcorrect; subst. destruct H as [?[?[??]]]. inversion H. } - wp_pures. inversion Htvalid; inversion Hvmatch. subst. + wp_pures. inversion Htvalid; inversion Hvmatch; subst. wp_apply (wp_hashfun_prev_amortized with "[$]"). + lia. + done. @@ -327,8 +344,8 @@ Section merkle_tree. wp_pures. wp_apply wp_list_tail; first done. iIntros (tail) "%Htail". inversion Hcorrect; wp_pures. - + inversion Htrelate. inversion Htvalid. inversion Hvmatch; subst; last done. - wp_apply ("IH" with "[][][][][][][$]"); try done. + + inversion Htvalid. inversion Hvmatch; subst; last done. + wp_apply ("IH" with "[][][][][][$]"); try done. iIntros (lhash) "[H ->]". wp_pures. replace (_*_+_)%Z with (Z.of_nat (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2)); last first. @@ -340,8 +357,8 @@ Section merkle_tree. * done. * iIntros "H". iApply "HΦ". iFrame. done. - + inversion Htrelate. inversion Htvalid. inversion Hvmatch; subst; first done. - wp_apply ("IH1" with "[][][][][][][$]"); try done. + + inversion Htvalid. inversion Hvmatch; subst; first done. + wp_apply ("IH1" with "[][][][][][$]"); try done. iIntros (rhash) "[H ->]". wp_pures. replace (_*_+_)%Z with (Z.of_nat (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2)); last first. @@ -355,9 +372,8 @@ Section merkle_tree. iFrame. done. Qed. - Lemma wp_compute_hash_from_leaf_incorrect (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v v':nat) (proof:list (bool*nat)) lproof f E: - {{{ ⌜tree_relate height ltree tree⌝ ∗ - ⌜tree_valid tree m⌝ ∗ + Lemma wp_compute_hash_from_leaf_incorrect (tree:merkle_tree) (m:gmap nat Z) (v v':nat) (proof:list (bool*nat)) lproof f E: + {{{ ⌜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⌝ ∗ @@ -377,10 +393,10 @@ Section merkle_tree. ⌜(0 <= retv < 2^val_bit_size)%Z⌝ }}}. Proof. - iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hlist & %Hpossible & %Hvmatch & %Hneq & %Hmvalid & %Hmsize & Herr) HΦ". + iIntros (Φ) "(%Htvalid & H & %Hlist & %Hpossible & %Hvmatch & %Hneq & %Hmvalid & %Hmsize & Herr) HΦ". iInduction tree as [|] "IH" - forall (height ltree m proof lproof Φ Htrelate Htvalid Hlist Hpossible Hvmatch Hmvalid Hmsize). - - inversion Htrelate; subst. rewrite /compute_hash_from_leaf. wp_pures. + forall (height m proof lproof Φ Htvalid Hlist Hpossible Hvmatch Hmvalid Hmsize). + - inversion Htvalid; subst. rewrite /compute_hash_from_leaf. wp_pures. rewrite -/compute_hash_from_leaf. inversion Hvmatch; subst. wp_apply wp_list_head; first done. iIntros (?) "[[_ ->]|(%&%&%&%)]"; last done. @@ -402,8 +418,8 @@ Section merkle_tree. 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. + 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. @@ -416,14 +432,14 @@ Section merkle_tree. wp_pures. wp_apply wp_list_tail; first done. iIntros (proof') "%Hproof'". wp_pures. - inversion Htrelate; subst. + inversion Htvalid; subst. iAssert (€ ((nnreal_nat (S n) * 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. } inversion Hpossible; inversion Hvmatch; inversion Htvalid; subst; wp_pures; try done. - + wp_apply ("IH" with "[][][][][][][][$H][$Herr]"); try done. + + wp_apply ("IH" with "[][][][][][][$H][$Herr]"); try done. { iPureIntro; lia. } iIntros (lefthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashneq & %Hlefthashsize')". wp_pures. @@ -454,7 +470,7 @@ Section merkle_tree. epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. lia. Unshelve. - ++ by inversion H19. + ++ by inversion H22. ++ by inversion Hpossible. -- rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)". iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. lia. @@ -467,7 +483,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. - + wp_apply ("IH1" with "[][][][][][][][$H][$Herr]"); try done. + + wp_apply ("IH1" with "[][][][][][][$H][$Herr]"); try done. { iPureIntro; lia. } iIntros (righthash') "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hrighthashneq & %Hrighthashsize')". wp_pures. @@ -497,7 +513,7 @@ Section merkle_tree. epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. lia. Unshelve. - ++ by inversion H19. + ++ by inversion H22. ++ destruct Hrighthashsize' as [Hrighthashsize Hrighthashsize']. rewrite Nat2Z.inj_lt. rewrite Z2Nat.inj_pow. replace (Z.of_nat 2) with 2%Z by lia. @@ -516,8 +532,7 @@ Section merkle_tree. Qed. Lemma wp_compute_hash_from_leaf_incorrect_proof (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: - {{{ ⌜tree_relate height ltree tree⌝ ∗ - ⌜tree_valid tree 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⌝ ∗ @@ -537,9 +552,9 @@ Section merkle_tree. ⌜(0 <= retv < 2^val_bit_size)%Z⌝ }}}. Proof. - iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hlist & %Hposs & %Hincorrect & %Hvmatch & %Hmvalid & %Hmsize & Herr) HΦ". + iIntros (Φ) "(%Htvalid & H & %Hlist & %Hposs & %Hincorrect & %Hvmatch & %Hmvalid & %Hmsize & Herr) HΦ". iInduction tree as [|] "IH" - forall (height ltree m proof lproof Φ Htrelate Htvalid Hlist Hposs Hincorrect Hvmatch Hmvalid Hmsize). + forall (height m proof lproof Φ Htvalid Hlist Hposs Hincorrect Hvmatch Hmvalid Hmsize). - inversion Hincorrect. - rewrite /compute_hash_from_leaf. wp_pures. rewrite -/compute_hash_from_leaf. @@ -548,7 +563,7 @@ Section merkle_tree. { inversion Hvmatch. } wp_pures. wp_apply wp_list_tail; first done. iIntros (proof') "%Hproof'". - wp_pures. inversion Htrelate; subst. + wp_pures. inversion Htvalid; subst. iAssert (€ ((nnreal_nat (S n) * 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 "[$]"). @@ -574,7 +589,7 @@ Section merkle_tree. ++ iPureIntro; etrans; exact. ++ iPureIntro; lia. ++ iPureIntro. simpl. intros ->. - inversion H27; subst. + inversion H30; 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. @@ -583,7 +598,7 @@ Section merkle_tree. } epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit Hsplit']; subst. done. Unshelve. - ** by inversion H19. + ** by inversion H22. ** by inversion Hposs. ++ rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)". iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. lia. @@ -597,7 +612,7 @@ Section merkle_tree. 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. + wp_apply ("IH" with "[][][][][][][][$H][$Herr]"); try done. * iPureIntro; lia. * iIntros (lefthash) "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hlefthashneq & %Hlefthashsize)". wp_pures. @@ -615,7 +630,7 @@ Section merkle_tree. ++ iPureIntro; etrans; exact. ++ iPureIntro; lia. ++ iPureIntro. simpl. intros ->. apply Hlefthashneq. - inversion H27; subst. + inversion H30; subst. assert (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2 = Z.to_nat lefthash * 2 ^ val_bit_size + root_hash_value tree2) as helper. { eapply (coll_free_lemma m''); try done. @@ -625,7 +640,7 @@ Section merkle_tree. epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. lia. Unshelve. - ** by inversion H19. + ** by inversion H22. ** by inversion Hposs. ++ rewrite /hashfun_amortized. iDestruct "H" as "(%&%&%&%&%Hforall&H)". iPureIntro. eapply map_Forall_lookup_1 in Hforall; last done. lia. @@ -656,7 +671,7 @@ Section merkle_tree. ++ iPureIntro; etrans; exact. ++ iPureIntro; lia. ++ iPureIntro. simpl. intros ->. - inversion H27; subst. + inversion H30; 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. @@ -665,7 +680,7 @@ Section merkle_tree. } epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit Hsplit']; subst. done. Unshelve. - ** by inversion H19. + ** by inversion H22. ** destruct Hrighthashsize as [Hrighthashsize Hrighthashsize']. rewrite Nat2Z.inj_lt. rewrite Z2Nat.inj_pow. replace (Z.of_nat 2) with 2%Z by lia. @@ -682,7 +697,7 @@ Section merkle_tree. 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. + wp_apply ("IH1" with "[][][][][][][][$H][$Herr]"); try done. * iPureIntro; lia. * iIntros (righthash) "(%m' & %Hmsubset & H & %Hmvalid' & %Hmsize' & %Hrighthashneq & %Hrighthashsize)". wp_pures. @@ -699,7 +714,7 @@ Section merkle_tree. ++ iPureIntro; etrans; exact. ++ iPureIntro; lia. ++ iPureIntro. simpl. intros ->. apply Hrighthashneq. - inversion H27; subst. + inversion H30; subst. assert (root_hash_value tree1 * 2 ^ val_bit_size + root_hash_value tree2 = root_hash_value tree1 * 2 ^ val_bit_size + Z.to_nat righthash) as helper. { eapply (coll_free_lemma m''); try done. @@ -709,7 +724,7 @@ Section merkle_tree. epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. lia. Unshelve. - ** by inversion H19. + ** by inversion H22. ** destruct Hrighthashsize as [Hrighthashsize Hrighthashsize']. rewrite Nat2Z.inj_lt. rewrite Z2Nat.inj_pow. replace (Z.of_nat 2) with 2%Z by lia. From 35ad5079fe091e8dc0c488b596312ae86065f3b1 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 5 Feb 2024 11:22:31 +0100 Subject: [PATCH 15/21] small fix --- theories/ub_logic/merkle_tree.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index bca20d85c..11bfe4081 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -308,7 +308,7 @@ Section merkle_tree. 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: + Lemma wp_compute_hash_from_leaf_correct (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_valid height tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ ⌜is_list proof lproof⌝ ∗ @@ -531,7 +531,7 @@ Section merkle_tree. induction val_bit_size; simpl; lia. Qed. - Lemma wp_compute_hash_from_leaf_incorrect_proof (ltree:val) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: + Lemma wp_compute_hash_from_leaf_incorrect_proof (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_valid height tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ ⌜is_list proof lproof⌝ ∗ @@ -749,9 +749,8 @@ Section merkle_tree. "correct_root_hash" = compute_hash_from_leaf "lhmf" "lproof" "lleaf" ). - Lemma merkle_tree_decider_program_spec ltree tree (m:gmap nat Z) f: - {{{ ⌜tree_relate height ltree tree⌝ ∗ - ⌜tree_valid tree m⌝ ∗ + 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 @@ -795,7 +794,7 @@ Section merkle_tree. }}}) }}}. Proof. - iIntros (Φ) "(%Htrelate & %Htvalid & H & %Hmvalid) IH". + iIntros (Φ) "(%Htvalid & H & %Hmvalid) IH". rewrite /merkle_tree_decider_program. wp_pures. iModIntro. iApply "IH". iFrame. From 1f1696c869e3fedb3b890de266e35fd34e5c4c33 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 5 Feb 2024 12:47:08 +0100 Subject: [PATCH 16/21] General spec --- theories/ub_logic/merkle_tree.v | 106 ++++++++++++++++++-------------- 1 file changed, 61 insertions(+), 45 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index 11bfe4081..c170bca45 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -182,6 +182,17 @@ Section merkle_tree. * by apply incorrect_proof_base_right. Qed. + Lemma possible_proof_implies_exists_leaf tree proof: + possible_proof tree proof -> ∃ v, tree_leaf_value_match tree v proof. + Proof. + revert proof. + induction tree; intros proof H; inversion H; subst. + - eexists _. constructor. + - destruct (IHtree1 _ H4). eexists _. constructor. naive_solver. + - destruct (IHtree2 _ H4). eexists _. constructor. naive_solver. + Qed. + + Lemma wp_compute_hash_from_leaf_size (n:nat) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_valid n tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ @@ -757,70 +768,75 @@ Section merkle_tree. {{{ (checker:val), RET checker; hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ - (** correct*) (∀ lproof proof v m', {{{ ⌜m⊆m'⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' ∗ ⌜is_list proof lproof⌝ ∗ - ⌜correct_proof tree proof⌝ ∗ - ⌜tree_leaf_value_match tree v proof⌝∗ - ⌜map_valid m'⌝ - - }}} - checker lproof (#v) - {{{ RET #true; - hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' - }}}) ∗ - (** incorrect*) - (∀ lproof proof v v' m', - {{{ ⌜m⊆m'⌝ ∗ - hashfun_amortized (val_size_for_hash)%nat max_hash_size f m' ∗ - ⌜is_list proof lproof⌝ ∗ - ⌜possible_proof tree proof⌝ ∗ - ⌜tree_leaf_value_match tree v proof⌝ ∗ - ⌜v ≠ v'⌝ ∗ + ⌜possible_proof tree proof ⌝∗ ⌜map_valid m'⌝ ∗ ⌜ size m' + (S height) <= max_hash_size⌝ ∗ - € (nnreal_nat (S height) * amortized_error (val_size_for_hash)%nat max_hash_size)%NNR + € (nnreal_nat (S height) * amortized_error (val_size_for_hash)%nat max_hash_size)%NNR }}} - checker lproof (#v') - {{{ RET #false; - ∃ m'', ⌜m' ⊆ m''⌝ ∗ + checker lproof (#v) + {{{ (b:bool), RET #b; + if b then + ⌜correct_proof tree proof⌝ ∗ + ⌜tree_leaf_value_match tree v proof⌝ ∗ + hashfun_amortized (val_size_for_hash) max_hash_size f m' ∗ + € (nnreal_nat (S height) * amortized_error (val_size_for_hash)%nat max_hash_size)%NNR + else + ⌜incorrect_proof tree proof \/ + (∃ v', tree_leaf_value_match tree v' proof /\ v ≠ v')⌝ ∗ + ∃ m'', ⌜m' ⊆ m''⌝ ∗ hashfun_amortized (val_size_for_hash) max_hash_size f m'' ∗ ⌜map_valid m''⌝ ∗ ⌜size (m'') <= size m' + (S height)⌝ - }}}) + }}} ) }}}. Proof. iIntros (Φ) "(%Htvalid & H & %Hmvalid) IH". rewrite /merkle_tree_decider_program. wp_pures. iModIntro. iApply "IH". iFrame. - iSplit. - - iIntros (?????). iModIntro. - iIntros "(%&H&%&%&%&%)IH". - wp_pures. - wp_apply (wp_compute_hash_from_leaf_correct with "[$H]"). - + repeat iSplit; iPureIntro; try done. - by eapply tree_valid_superset. - + iIntros (?) "[H ->]". wp_pures. - iModIntro. case_bool_decide; last done. - iApply "IH"; iFrame. - - iIntros (??????). - iModIntro. - iIntros "(%&H&%&%&%&%&%&%&Herr) IH". - wp_pures. - wp_apply (wp_compute_hash_from_leaf_incorrect with "[$H $Herr]"). - + repeat iSplit; iPureIntro; try done. - by eapply tree_valid_superset. + iIntros (?????) "!> (%&H&%&%&%&%&Herr) HΦ". + wp_pures. + epose proof (possible_proof_implies_exists_leaf tree proof _) as [v' ?]. + destruct (decide (v=v')). + - 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. + iModIntro. iApply "HΦ". iFrame. + by iSplit. + + 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. + rewrite bool_decide_eq_false_2; last first. + { intros K'; inversion K'; by subst. } + iModIntro; iApply "HΦ". + repeat iSplit. + -- 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. + iIntros (?) "(%&%&H&%&%&%&%)". - wp_pures. iModIntro. - case_bool_decide as K; first by inversion K. - iApply "IH". - iExists _; iFrame. - repeat iSplit; try done. + wp_pures. rewrite bool_decide_eq_false_2; last first. + { intros K. inversion K. by subst. } + iModIntro. iApply "HΦ". + repeat iSplit. + * iPureIntro. right. eexists _; naive_solver. + * iExists _; by repeat iSplit. + Unshelve. + all: done. Qed. End merkle_tree. From 2d4751502361d1580c01fe97650a159c99d2dfcd Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 5 Feb 2024 13:06:02 +0100 Subject: [PATCH 17/21] added comments --- theories/ub_logic/merkle_tree.v | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle_tree.v index c170bca45..8a30c3999 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle_tree.v @@ -4,6 +4,18 @@ Set Default Proof Using "Type*". 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 + 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. + For each branch, the concatentation of the left and right hash are provided as input. + + In other words, input bit size = 2 * 2 ^ val_bit_size + and output bit size = 2 ^ val_bit_size + + *) Context `{!ub_clutchGS Σ}. Variables height:nat. Variables val_bit_size':nat. @@ -59,7 +71,10 @@ Section merkle_tree. tree_leaf_value_match r v xs -> tree_leaf_value_match (Branch h l r) v ((false,lhash)::xs). - (*This ensures all numbers in the proof are smaller than 2^val_bit_size*) + (*This ensures all numbers in the proof are smaller than 2^val_bit_size + If the numbers are larger or equal to 2^val_bit_size + One knows immediately that the proof is invalid and should not be considered. + *) Inductive possible_proof: merkle_tree -> list (bool*nat) -> Prop:= | possible_proof_lf h v: possible_proof (Leaf h v) [] | possible_proof_br_left h ltree rtree hash prooflist: @@ -192,7 +207,9 @@ Section merkle_tree. - destruct (IHtree2 _ H4). eexists _. constructor. naive_solver. Qed. - + (*This lemma is here to ensure that the return value lies within a bound + This lemma is eventually used in the case where the proof is incorrect. + *) Lemma wp_compute_hash_from_leaf_size (n:nat) (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_valid n tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ @@ -318,7 +335,7 @@ Section merkle_tree. induction val_bit_size; simpl; lia. Qed. - (** Spec *) + (* The case where everything is correct *) Lemma wp_compute_hash_from_leaf_correct (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_valid height tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ @@ -383,6 +400,7 @@ Section merkle_tree. iFrame. done. Qed. + (*The case where the leaf is incorrect*) Lemma wp_compute_hash_from_leaf_incorrect (tree:merkle_tree) (m:gmap nat Z) (v v':nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_valid height tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ @@ -542,6 +560,7 @@ Section merkle_tree. induction val_bit_size; simpl; lia. Qed. + (*The case where the leaf is correct but the proof is not *) Lemma wp_compute_hash_from_leaf_incorrect_proof (tree:merkle_tree) (m:gmap nat Z) (v:nat) (proof:list (bool*nat)) lproof f E: {{{ ⌜tree_valid height tree m⌝ ∗ hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ From b3be3ba749217c3497773ae46e9bb2501eb0bedf Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 5 Feb 2024 15:39:16 +0100 Subject: [PATCH 18/21] Wrote program for unreliable storage --- theories/ub_logic/{ => merkle}/merkle_tree.v | 9 +-- theories/ub_logic/merkle/unreliable.v | 66 ++++++++++++++++++++ 2 files changed, 68 insertions(+), 7 deletions(-) rename theories/ub_logic/{ => merkle}/merkle_tree.v (99%) create mode 100644 theories/ub_logic/merkle/unreliable.v diff --git a/theories/ub_logic/merkle_tree.v b/theories/ub_logic/merkle/merkle_tree.v similarity index 99% rename from theories/ub_logic/merkle_tree.v rename to theories/ub_logic/merkle/merkle_tree.v index 8a30c3999..ed5a684ee 100644 --- a/theories/ub_logic/merkle_tree.v +++ b/theories/ub_logic/merkle/merkle_tree.v @@ -37,13 +37,6 @@ Section merkle_tree. | Branch h _ _ => h end. - (* Inductive tree_relate: nat -> val -> merkle_tree -> Prop:= *) - (* | tree_relate_lf (hv v:nat): tree_relate 0 (InjLV (#hv, #v)) (Leaf hv v) *) - (* | tree_relate_br n (hv:nat) ll l lr r: *) - (* tree_relate n ll l -> *) - (* tree_relate n lr r -> *) - (* tree_relate (S n) (InjRV (#hv, ll, lr)) (Branch hv l r) *) - (* . *) Inductive tree_valid: nat -> merkle_tree -> gmap nat Z -> Prop := |tree_valid_lf (h l:nat) m: @@ -859,3 +852,5 @@ Section merkle_tree. Qed. End merkle_tree. + + diff --git a/theories/ub_logic/merkle/unreliable.v b/theories/ub_logic/merkle/unreliable.v new file mode 100644 index 000000000..173ba3e57 --- /dev/null +++ b/theories/ub_logic/merkle/unreliable.v @@ -0,0 +1,66 @@ +From clutch.ub_logic Require Export ub_clutch lib.map hash lib.list merkle.merkle_tree. +Import Hierarchy. +Set Default Proof Using "Type*". +Open Scope nat. + +Section unreliable_storage. + Context `{!ub_clutchGS Σ}. + Variables ε_write ε_read: nonnegreal. + Variables unreliable_write_program unreliable_read_program:val. + + Axiom unreliable_write_spec : + ∀ l (n:nat), + {{{€ ε_write ∗ ∃ v, l ↦ v }}} + unreliable_write_program #l #n + {{{ RET #(); l ↦ #n}}}. + Axiom unreliable_read_spec : + ∀ l (n:nat), + {{{€ ε_read ∗ l ↦ #n }}} + unreliable_read_program #l + {{{ RET #n; l ↦ #n}}}. + + Variables val_bit_size':nat. + Variables max_hash_size : nat. + Definition val_bit_size : nat := S val_bit_size'. + Definition val_size_for_hash := 2^val_bit_size -1. + + Fixpoint tree_relate (n:nat) (l:loc) (t:merkle_tree) :iProp Σ := + match n with + | O => (∃ (hv v:nat), l ↦ (#hv, #v)%V ∗ ⌜t= (Leaf hv v)⌝) + | S n' => ∃ (hv:nat) (leftbrl rightbrl:loc) leftbr rightbr, + l ↦ (#hv, #leftbrl, #rightbrl)%V ∗ + ⌜t=(Branch hv leftbr rightbr)⌝ ∗ + tree_relate n' leftbrl leftbr ∗ + tree_relate n' rightbrl rightbr + end. + + Definition pow : val := + rec: "pow" "x":= + if: "x"=#0 then #1 else #2 * ("pow" ("x"-#1)). + + Definition tree_builder_helper : val:= + rec: "helper" "lhmf" "n" "list":= + if: "n" = #0 + then + let: "head":= list_head "list" in + let: "hash" := "lhmf" "head" in + ("hash", Alloc ("hash", "head")) + else + let, ("list1", "list2") := list_split (pow ("n"-#1)) "list" in + let, ("lhash", "ltree") := "helper" ("n"-#1) "list1" in + let, ("rhash", "rtree") := "helper" ("n"-#1) "list2" in + let: "hash" := "lhmf" (pow "n" * "lhash" + "rhash") in + ("hash", Alloc ("hash", "ltree", "rtree")) + . + + Definition tree_builder : val := + λ: "list" "height", + let: "lhmf" := init_hash val_size_for_hash #() in + tree_builder_helper "lhmf" "height" "list" + . + + + + + +End unreliable_storage. From fd5bdf89b2c76ceb3d0ac748753c3b45d092e13b Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 5 Feb 2024 15:42:07 +0100 Subject: [PATCH 19/21] small fix, using unreliable alloc --- theories/ub_logic/merkle/unreliable.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/ub_logic/merkle/unreliable.v b/theories/ub_logic/merkle/unreliable.v index 173ba3e57..8f27a54f9 100644 --- a/theories/ub_logic/merkle/unreliable.v +++ b/theories/ub_logic/merkle/unreliable.v @@ -6,13 +6,13 @@ Open Scope nat. Section unreliable_storage. Context `{!ub_clutchGS Σ}. Variables ε_write ε_read: nonnegreal. - Variables unreliable_write_program unreliable_read_program:val. + Variables unreliable_alloc_program unreliable_read_program:val. - Axiom unreliable_write_spec : - ∀ l (n:nat), - {{{€ ε_write ∗ ∃ v, l ↦ v }}} - unreliable_write_program #l #n - {{{ RET #(); l ↦ #n}}}. + Axiom unreliable_alloc_spec : + ∀ (n:nat), + {{{€ ε_write }}} + unreliable_alloc_program #n + {{{ RET #(); ∃ l, l ↦ #n}}}. Axiom unreliable_read_spec : ∀ l (n:nat), {{{€ ε_read ∗ l ↦ #n }}} @@ -44,13 +44,13 @@ Section unreliable_storage. then let: "head":= list_head "list" in let: "hash" := "lhmf" "head" in - ("hash", Alloc ("hash", "head")) + ("hash", unreliable_alloc_program ("hash", "head")) else let, ("list1", "list2") := list_split (pow ("n"-#1)) "list" in let, ("lhash", "ltree") := "helper" ("n"-#1) "list1" in let, ("rhash", "rtree") := "helper" ("n"-#1) "list2" in let: "hash" := "lhmf" (pow "n" * "lhash" + "rhash") in - ("hash", Alloc ("hash", "ltree", "rtree")) + ("hash", unreliable_alloc_program ("hash", "ltree", "rtree")) . Definition tree_builder : val := From ecf0a287bf27bfd53d331dd99b0a5e6462e53516 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 5 Feb 2024 16:27:00 +0100 Subject: [PATCH 20/21] Using new axioms to implement program --- theories/ub_logic/merkle/unreliable.v | 48 +++++++++++++++------------ 1 file changed, 27 insertions(+), 21 deletions(-) diff --git a/theories/ub_logic/merkle/unreliable.v b/theories/ub_logic/merkle/unreliable.v index 8f27a54f9..912f51c59 100644 --- a/theories/ub_logic/merkle/unreliable.v +++ b/theories/ub_logic/merkle/unreliable.v @@ -5,34 +5,33 @@ Open Scope nat. Section unreliable_storage. Context `{!ub_clutchGS Σ}. - Variables ε_write ε_read: nonnegreal. - Variables unreliable_alloc_program unreliable_read_program:val. + Variables unreliable_alloc_program unreliable_write_program unreliable_read_program:val. Axiom unreliable_alloc_spec : - ∀ (n:nat), - {{{€ ε_write }}} - unreliable_alloc_program #n - {{{ RET #(); ∃ l, l ↦ #n}}}. + ∀ (m:nat), + m>0 -> + {{{ True }}} + unreliable_alloc_program #m + {{{ (x:nat), RET #x; True }}}. + + Axiom unreliable_read_spec : - ∀ l (n:nat), - {{{€ ε_read ∗ l ↦ #n }}} + ∀ (l : nat), + {{{ True }}} unreliable_read_program #l - {{{ RET #n; l ↦ #n}}}. + {{{(n:nat), RET #n; True}}}. + + + Axiom unreliable_write_spec : + ∀ (n l: nat), + {{{ True }}} + unreliable_write_program #l #n + {{{ RET #(); True}}}. Variables val_bit_size':nat. Variables max_hash_size : nat. Definition val_bit_size : nat := S val_bit_size'. Definition val_size_for_hash := 2^val_bit_size -1. - - Fixpoint tree_relate (n:nat) (l:loc) (t:merkle_tree) :iProp Σ := - match n with - | O => (∃ (hv v:nat), l ↦ (#hv, #v)%V ∗ ⌜t= (Leaf hv v)⌝) - | S n' => ∃ (hv:nat) (leftbrl rightbrl:loc) leftbr rightbr, - l ↦ (#hv, #leftbrl, #rightbrl)%V ∗ - ⌜t=(Branch hv leftbr rightbr)⌝ ∗ - tree_relate n' leftbrl leftbr ∗ - tree_relate n' rightbrl rightbr - end. Definition pow : val := rec: "pow" "x":= @@ -44,13 +43,20 @@ Section unreliable_storage. then let: "head":= list_head "list" in let: "hash" := "lhmf" "head" in - ("hash", unreliable_alloc_program ("hash", "head")) + let: "l" := unreliable_alloc_program #2 in + unreliable_write_program "l" "hash";; + unreliable_write_program ("l"+#1) "head";; + ("hash", "l") else let, ("list1", "list2") := list_split (pow ("n"-#1)) "list" in let, ("lhash", "ltree") := "helper" ("n"-#1) "list1" in let, ("rhash", "rtree") := "helper" ("n"-#1) "list2" in let: "hash" := "lhmf" (pow "n" * "lhash" + "rhash") in - ("hash", unreliable_alloc_program ("hash", "ltree", "rtree")) + let: "l" := unreliable_alloc_program #3 in + unreliable_write_program "l" "hash";; + unreliable_write_program ("l"+#1) "ltree";; + unreliable_write_program ("l"+#2) "rtree";; + ("hash", "l") . Definition tree_builder : val := From 8bbe5eaed690082721a9aac1702e734eae87959f Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 6 Feb 2024 12:55:06 +0100 Subject: [PATCH 21/21] update ltac of total --- theories/ub_logic/hash.v | 2 +- theories/ub_logic/merkle/merkle_tree.v | 11 --- theories/ub_logic/merkle/unreliable.v | 112 ++++++++++++++++++++++++- theories/ub_logic/proofmode.v | 8 +- 4 files changed, 115 insertions(+), 18 deletions(-) diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v index a0f044cd0..5e58c5813 100644 --- 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 index ed5a684ee..06e5afde2 100644 --- 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 index 912f51c59..ad43d029c 100644 --- 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 index 57498a26f..522035d5f 100644 --- 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]]