Skip to content

Commit

Permalink
Spec for writing a tree into unreliable memory
Browse files Browse the repository at this point in the history
  • Loading branch information
@hei411
hei411 committed Feb 6, 2024
1 parent 8bbe5ea commit 00a7704
Show file tree
Hide file tree
Showing 2 changed files with 195 additions and 13 deletions.
32 changes: 32 additions & 0 deletions theories/ub_logic/lib/list.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -949,6 +949,37 @@ Section list_specs.
+ iApply "HΦ"; iPureIntro.
simpl. rewrite HP. done.
Qed.


Lemma wp_list_split E (n:nat) (lv:val) l:
{{{ ⌜is_list l lv⌝ ∗ ⌜n<=length l⌝ }}}
list_split #n lv @ E
{{{ a b, RET (a, b)%V;
∃ l1 l2, ⌜is_list l1 a⌝ ∗ ⌜is_list l2 b⌝ ∗ ⌜l=l1++l2⌝ ∗ ⌜length (l1) = n⌝
}}}.
Proof.
revert lv l.
induction n;
iIntros (lv l Φ) "[%Hlist %Hlength] HΦ".
- rewrite /list_split. wp_pures. iModIntro. iApply "HΦ".
iExists [], l.
repeat iSplit; by iPureIntro.
- rewrite /list_split. wp_pures. rewrite -/list_split.
destruct l.
{ simpl in Hlength. lia. }
destruct Hlist as [?[-> Hlist]].
wp_pures. replace (Z.of_nat (S n) - 1)%Z with (Z.of_nat n) by lia.
wp_apply IHn.
+ iSplit; iPureIntro; try done. simpl in Hlength. lia.
+ iIntros (??) "(%l1 & %l2 &%&%&%&%)".
wp_pures.
wp_apply wp_list_cons; first done.
iIntros. wp_pures. iApply "HΦ".
iExists (_::l1), l2.
iModIntro; repeat iSplit; iPureIntro; try done.
* set_solver.
* set_solver.
Qed.
End list_specs.

Global Arguments wp_list_nil : clear implicits.
Expand Down Expand Up @@ -1268,4 +1299,5 @@ Section list_specs_extra.
Qed.



End list_specs_extra.
176 changes: 163 additions & 13 deletions theories/ub_logic/merkle/unreliable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,8 @@ Section unreliable_storage.
destruct n; try done. lia.
Qed.



(* Building the tree*)
Definition tree_builder_helper : val:=
rec: "helper" "lhmf" "n" "list":=
Expand All @@ -79,9 +81,9 @@ Section unreliable_storage.
("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, ("lhash", "ltree") := "helper" "lhmf" ("n"-#1) "list1" in
let, ("rhash", "rtree") := "helper" "lhmf" ("n"-#1) "list2" in
let: "hash" := "lhmf" (pow #val_bit_size * "lhash" + "rhash") in
let: "l" := unreliable_alloc_program #3 in
unreliable_write_program "l" "hash";;
unreliable_write_program ("l"+#1) "ltree";;
Expand All @@ -104,6 +106,7 @@ Section unreliable_storage.
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 ->
Forall (λ x, x < 2^(2*val_bit_size)) list ->
is_list list vlist ->
{{{ hashfun_amortized val_size_for_hash max_hash_size f m ∗
⌜coll_free m⌝ ∗
Expand All @@ -117,29 +120,176 @@ Section unreliable_storage.
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'⌝ ∗
⌜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).
iIntros (Hmsize Hlength Hforall Hislist Φ) "(H&%Hcollfree&Herr) HΦ".
iInduction height as [|height] "IH" forall (list vlist m Hmsize Hlength Hforall Hislist Φ Hcollfree).
- rewrite /tree_builder_helper. wp_pures.
assert (∃ x:nat, list = x::[]) as [x ->].
{ destruct list as [_| x [|]]; first done.
{ destruct list as [| ? [|]]; first done.
- naive_solver.
- done.
}
wp_apply (wp_list_head); first done.
iIntros (?) "[[%?]|(%&%&%K&->)]"; first done.
inversion K; subst.
wp_pures.
admit.
- admit.
Admitted.
wp_apply (wp_insert_amortized with "[$H Herr]").
+ simpl in Hmsize. lia.
+ iSplitL; last done.
iApply ec_spend_irrel; last done.
simpl. lra.
+ iIntros (hash) "(%m' & H&%&%&%&%)".
wp_pures. replace 2%Z with (Z.of_nat 2) by lia.
wp_apply unreliable_alloc_spec; [lia|done|].
iIntros (l) "_".
wp_pures.
iAssert (⌜(0<=hash<2^val_bit_size)%Z⌝)%I as "[%Ha %Hb]".
{ iDestruct "H" as "(%&%&%&%&%K' &H)".
iPureIntro.
eapply map_Forall_lookup_1 in K' as [? K']; last done.
split; try lia.
rewrite /val_size_for_hash in K'. rewrite Z.lt_le_pred.
eapply Z.le_stepr; first done.
rewrite Nat2Z.inj_sub; last first.
- clear. induction val_bit_size; simpl; lia.
- rewrite Nat2Z.inj_pow. lia.
}
replace (hash) with (Z.of_nat $ Z.to_nat hash); last lia.
wp_apply unreliable_write_spec; first done.
iIntros "_".
wp_pures.
replace (_+_)%Z with (Z.of_nat (l+1)%nat); last lia.
wp_apply unreliable_write_spec; first done.
iIntros "_"; wp_pures.
iModIntro.
iApply "HΦ".
iExists m', _.
repeat iSplit; try done.
* iPureIntro. simpl; lia.
* iPureIntro; constructor.
* iPureIntro; constructor.
-- instantiate (1 := Z.to_nat hash).
rewrite /merkle_tree.val_bit_size.
rewrite Z2Nat.inj_lt in Hb; try lia.
rewrite Znat.Z2Nat.inj_pow in Hb; try lia.
eapply Nat.lt_stepr; first done. f_equal.
rewrite Nat2Z.id. done.
-- apply Forall_inv in Hforall. done.
-- rewrite Z2Nat.id; last lia. done.
* done.
- rewrite /tree_builder_helper. wp_pures. rewrite -/tree_builder_helper.
replace (_-_)%Z with (Z.of_nat (height)); last lia.
wp_apply pow_spec; first done.
iIntros (?) "->".
wp_apply wp_list_split; first (iSplit; iPureIntro; try done; rewrite Hlength).
{ apply PeanoNat.Nat.pow_le_mono_r; lia. }
iIntros (a b) "(%l1 & %l2 &%&%&%&%)"; wp_pures.
iAssert (€ ((nnreal_nat (2 ^ S height - 1) * amortized_error val_size_for_hash max_hash_size)%NNR) ∗
€ ((nnreal_nat (2 ^ S height - 1) * amortized_error val_size_for_hash max_hash_size)%NNR) ∗
€ ((nnreal_nat (1) * amortized_error val_size_for_hash max_hash_size)%NNR)

)%I with "[Herr]" as "[Herr [Herr' Herr'']]".
{ repeat rewrite -ec_split. iApply ec_spend_irrel; last done.
remember (amortized_error val_size_for_hash max_hash_size) as x.
clear.
assert (forall x y z, (nnreal_nat x * z + nnreal_nat y * z)%NNR = (nnreal_nat (x+y) * z)%NNR) as Hr; last rewrite !Hr.
- clear. intros. destruct z. apply nnreal_ext. simpl. rewrite plus_INR. lra.
- repeat f_equal. remember (S height) as h.
simpl. assert (1<=2^h).
+ clear. induction h; simpl; lia.
+ lia.
}
subst.
replace (Z.of_nat (S height) - 1)%Z with (Z.of_nat height); last lia.
wp_apply ("IH" with "[][][][][][$H][$Herr]"); try iPureIntro; try done.
+ assert (2^S height <= 2^ S (S height)); try lia.
simpl. lia.
+ by apply Forall_app in Hforall as [Hforall1 Hforall2].
+ iIntros (hasha la) "(%m' & %treea & %&%&H&%&%&%&%)".
wp_pures.
replace (Z.of_nat (S height) - 1)%Z with (Z.of_nat height); last lia.
wp_apply ("IH"$! l2 with "[][][][][][$H][$Herr']"); try iPureIntro; try done.
* trans (size m + 2^ S height - 1 + 2 ^ S height - 1); try lia.
etrans; last exact. simpl. lia.
* replace (2^ S height) with (2^height + 2 ^ height) in Hlength; last first.
{ simpl. lia. }
rewrite app_length in Hlength. lia.
* rewrite Forall_app in Hforall. set_solver.
* iIntros (hashb lb) "(%m'' & %treeb & %&%&H&%&%&%&%)".
wp_pures.
wp_apply pow_spec; first done.
iIntros (?) "->".
wp_pures. rewrite <-Nat2Z.inj_mul. rewrite <-Nat2Z.inj_add.
replace (_+(_+0)) with (2^S val_bit_size'); last (simpl; lia).
wp_apply (wp_insert_amortized with "[$H Herr'']").
-- eapply PeanoNat.Nat.le_lt_trans; first exact.
eapply PeanoNat.Nat.lt_le_trans; last exact.
apply (PeanoNat.Nat.le_lt_trans _ (size m + 2 ^ S height - 1 + 2^S height - 1)); try lia.
clear. simpl. assert (0<2^height); try lia.
induction height; simpl; lia.
-- iSplit; last done. iApply ec_spend_irrel; last done.
simpl. lra.
-- iIntros (hash) "(%m''' & H&%&%Hfound&%&%)".
wp_pures.
replace 3%Z with (Z.of_nat 3) by lia.
wp_apply unreliable_alloc_spec; [lia|done|].
iIntros (?) "_".
wp_pures.
iAssert (⌜(0<=hash<2^val_bit_size)%Z⌝)%I as "[%Ha %Hb]".
{ iDestruct "H" as "(%&%&%&%&%K' &H)".
iPureIntro.
eapply map_Forall_lookup_1 in K' as [? K']; last done.
split; try lia.
rewrite /val_size_for_hash in K'. rewrite Z.lt_le_pred.
eapply Z.le_stepr; first done.
rewrite Nat2Z.inj_sub; last first.
- clear. induction val_bit_size; simpl; lia.
- rewrite Nat2Z.inj_pow. lia.
}
replace (hash) with (Z.of_nat (Z.to_nat hash)); last lia.
wp_apply unreliable_write_spec; first done.
iIntros "_".
wp_pures.
replace (_+1)%Z with (Z.of_nat (x+1)) by lia.
wp_apply unreliable_write_spec; first done.
iIntros "_".
wp_pures.
replace (_+2)%Z with (Z.of_nat (x+2)) by lia.
wp_apply unreliable_write_spec; first done.
iIntros "_".
wp_pures.
iModIntro. iApply "HΦ".
iExists m''', (Branch (Z.to_nat hash) treea treeb).
repeat iSplit; try done.
++ iPureIntro. by do 3 (etrans; last exact).
++ iPureIntro. replace (_+_-_) with (size m + 2 ^ S height + 2^ S height - 1); last by (simpl;lia).
trans (size m' + 2^S height); last lia.
etrans; first exact.
assert (0<2^S height); try lia.
clear.
remember (S height) as x; clear.
induction x; simpl; lia.
++ iPureIntro. by constructor.
++ iPureIntro. constructor.
--- eapply tree_valid_superset; [done|done|].
by do 2 (etrans; last exact).
--- eapply tree_valid_superset; [done|done|].
by etrans; last exact.
--- rewrite Z2Nat.inj_lt in Hb; try lia.
eapply Nat.lt_stepr; first exact.
rewrite Znat.Z2Nat.inj_pow; try lia. rewrite Nat2Z.id.
f_equal.
--- rewrite Z2Nat.id; last lia.
rewrite -Hfound. f_equal. subst. simpl. lia.
Qed.

Lemma tree_builder_spec (list:list nat) (vlist: val) (height:nat):
2^(S height) - 1 <= max_hash_size ->
length list = 2^height ->
Forall (λ x, x < 2^(2*val_bit_size)) list ->
is_list list vlist ->
{{{
€ (nnreal_nat (2^(S height)-1) * amortized_error val_size_for_hash max_hash_size)%NNR
Expand All @@ -148,20 +298,20 @@ Section unreliable_storage.
{{{ (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⌝ ∗
⌜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Φ".
iIntros (Hmsize Hlistsize Hforall 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|..].
wp_apply (tree_builder_helper_spec with "[$H $Herr]"); [done|done|done|done|..].
{ iPureIntro. intros ???H??. exfalso. destruct H. set_solver. }
iIntros (hash l) "(%m'&%tree&%&%&H&%&%&%&%)".
wp_pures. iModIntro.
Expand Down

0 comments on commit 00a7704

Please sign in to comment.