diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v index c12163fad..5e58c5813 100644 --- a/theories/ub_logic/hash.v +++ b/theories/ub_logic/hash.v @@ -1,7 +1,9 @@ From clutch.ub_logic Require Export ub_clutch lib.map. +From stdpp Require Export fin_maps. +Import Hierarchy. Set Default Proof Using "Type*". -Module simple_bit_hash. +Section simple_bit_hash. Context `{!ub_clutchGS Σ}. @@ -39,7 +41,10 @@ Module 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). @@ -115,7 +120,7 @@ Module 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 "[$]"). @@ -125,7 +130,7 @@ Module 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⌝ }}} @@ -133,7 +138,7 @@ Module 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 "[$]"). @@ -154,11 +159,229 @@ Module 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. Qed. - + End simple_bit_hash. + + + +Section amortized_hash. + Context `{!ub_clutchGS Σ}. + Variable val_size:nat. + Variable max_hash_size : 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. + 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 ⌝ ∗ + ⌜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⌝ ∗ + € ε ∗ + 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 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_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)". 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)". + 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_new_amortized E f m (n : nat) : + 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 H0. 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|..]. + + 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. + * 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) : + (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' <= S $ size(m))%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/merkle/merkle_tree.v b/theories/ub_logic/merkle/merkle_tree.v new file mode 100644 index 000000000..06e5afde2 --- /dev/null +++ b/theories/ub_logic/merkle/merkle_tree.v @@ -0,0 +1,845 @@ +From clutch.ub_logic Require Export ub_clutch lib.map hash lib.list. +Import Hierarchy. +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. + Variables max_hash_size : nat. + Definition val_bit_size : nat := S val_bit_size'. + Definition val_size_for_hash:nat := (2^val_bit_size)-1. + Variable (Hineq: (max_hash_size <= val_size_for_hash)%nat). + Definition leaf_bit_size : nat := 2*val_bit_size. + (* Definition identifier : nat := 2^leaf_bit_size. *) + Definition num_of_leafs : nat := 2^height. + + Inductive merkle_tree := + | Leaf (hash_value : nat) (leaf_value:nat) + | Branch (hash_value : nat) (t1 t2:merkle_tree). + + Definition root_hash_value (t: merkle_tree) := + match t with + | Leaf h _ => h + | Branch h _ _ => h + end. + + + 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 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 (S n) (Branch h l r) m. + + + Definition map_valid (m:gmap nat Z) : Prop := coll_free m. + + + 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). + + (*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: + possible_proof ltree prooflist -> + hash < 2^val_bit_size -> + 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) [] + | 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). + + 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 := *) + (* λ: "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" := + 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: *) + (* {{{ ⌜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 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. + by eapply lookup_weaken. + - intros. inversion H; subst. constructor; try naive_solver. + 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. + + Lemma proof_correct_implies_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. + + 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 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. + + (*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 ∗ + ⌜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 (Φ) "(%Htvalid & H & %Hproof & %Hposs & %Hmvalid & %Hmsize &Herr) HΦ". + iInduction tree as [hash leaf|hash tree1 Htree1 tree2 Htree2] "IH" + 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 Htvalid; 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 [? 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. + - 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 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; 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. + * 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. + * 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. + + (* 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 ∗ + ⌜is_list proof lproof⌝ ∗ + ⌜correct_proof tree proof⌝ ∗ + ⌜tree_leaf_value_match tree v proof⌝ ∗ + ⌜map_valid m⌝ }}} + compute_hash_from_leaf f lproof (#v) @ E + {{{ (retv:Z), RET #retv; + hashfun_amortized (val_size_for_hash) max_hash_size f m ∗ + ⌜retv = root_hash_value tree⌝ + }}}. + Proof. + iIntros (Φ) "(%Htvalid & H & %Hlist & %Hcorrect & %Hvmatch & %Hmvalid) HΦ". + iInduction tree as [hash leaf|hash tree1 Htree1 tree2 Htree2] "IH" + 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_apply (wp_hashfun_prev_amortized with "[$]"). + + 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 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. + apply Z2Nat.inj_pow. + } + wp_apply (wp_hashfun_prev_amortized with "H"). + * done. + * iIntros "H". iApply "HΦ". + iFrame. 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. + { rewrite Nat2Z.inj_add. f_equal. rewrite Nat2Z.inj_mul. f_equal. + apply Z2Nat.inj_pow. + } + wp_apply (wp_hashfun_prev_amortized with "H"). + * done. + * iIntros "H". iApply "HΦ". + 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 ∗ + ⌜is_list proof lproof⌝ ∗ + ⌜possible_proof tree 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 + }}} + 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 (Φ) "(%Htvalid & H & %Hlist & %Hpossible & %Hvmatch & %Hneq & %Hmvalid & %Hmsize & Herr) HΦ". + iInduction tree as [|] "IH" + 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. + 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. + * 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 [? 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. + - 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 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. + { 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']"). + * 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 H22. + ++ 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 [? 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 (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']"). + * 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 H22. + ++ 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. + 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 ∗ + ⌜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 (Φ) "(%Htvalid & H & %Hlist & %Hposs & %Hincorrect & %Hvmatch & %Hmvalid & %Hmsize & Herr) HΦ". + iInduction tree as [|] "IH" + 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. + 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 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 Hposs; inversion Hvmatch; inversion Htvalid; inversion Hincorrect; subst; wp_pures; try done. + + (*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. + -- 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 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. + eapply lookup_weaken; first done. + etrans; exact. + } + epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit Hsplit']; subst. done. + Unshelve. + ** 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. + ++ 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. + * 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. + -- 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 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. + eapply lookup_weaken; first done. + etrans; exact. + } + epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. + lia. + Unshelve. + ** 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. + ++ 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 *) + 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. + -- 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 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. + eapply lookup_weaken; first done. + etrans; exact. + } + epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit Hsplit']; subst. done. + Unshelve. + ** 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. + 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. + * 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. + -- 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 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. + eapply lookup_weaken; first done. + etrans; exact. + } + epose proof (Nat.mul_split_l _ _ _ _ _ _ _ helper) as [Hsplit _]. + lia. + Unshelve. + ** 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. + 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. + 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 tree (m:gmap nat Z) f: + {{{ ⌜tree_valid height tree m⌝ ∗ + hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ + ⌜map_valid m⌝ + }}} merkle_tree_decider_program #(root_hash_value tree) f + {{{ + (checker:val), RET checker; + hashfun_amortized (val_size_for_hash)%nat max_hash_size f m ∗ + (∀ lproof proof v m', + {{{ + ⌜m⊆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 height) <= max_hash_size⌝ ∗ + € (nnreal_nat (S height) * amortized_error (val_size_for_hash)%nat max_hash_size)%NNR + + }}} + 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. + 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. 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. + + diff --git a/theories/ub_logic/merkle/unreliable.v b/theories/ub_logic/merkle/unreliable.v new file mode 100644 index 000000000..ad43d029c --- /dev/null +++ b/theories/ub_logic/merkle/unreliable.v @@ -0,0 +1,180 @@ +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 unreliable_alloc_program unreliable_write_program unreliable_read_program:val. + + Axiom unreliable_alloc_spec : + ∀ (m:nat), + m>0 -> + {{{ True }}} + unreliable_alloc_program #m + {{{ (x:nat), RET #x; True }}}. + + + Axiom unreliable_read_spec : + ∀ (l : nat), + {{{ True }}} + unreliable_read_program #l + {{{(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. + + Definition pow : val := + 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":= (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";; + 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 + 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 := + λ: "list" "height", + let: "lhmf" := init_hash val_size_for_hash #() in + (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. + + + + + + + + +End unreliable_storage. 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]]