Skip to content

Commit cc57262

Browse files
yunshengtwyunshengtw
committed
Internalize list for own_dbmap_in_slice
1 parent fd15d52 commit cc57262

File tree

11 files changed

+45
-52
lines changed

11 files changed

+45
-52
lines changed

‎src/program_proof/tulip/program/prelude.v

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -147,12 +147,13 @@ Proof. intros x y H. by destruct x, y. Defined.
147147
Section def.
148148
Context `{!heapGS Σ, !tulip_ghostG Σ}.
149149

150-
Definition own_dbmap_in_slice s (l : list dbmod) (m : dbmap) : iProp Σ :=
151-
own_slice s (struct.t WriteEntry) (DfracOwn 1) l ∗ ⌜map_to_list m ≡ₚ l⌝.
150+
Definition own_dbmap_in_slice s (m : dbmap) : iProp Σ :=
151+
∃ l : list dbmod,
152+
own_slice s (struct.t WriteEntry) (DfracOwn 1) l ∗ ⌜map_to_list m ≡ₚ l⌝.
152153

153154
Definition own_pwrs_slice (pwrsS : Slice.t) (c : ccommand) : iProp Σ :=
154155
match c with
155-
| CmdCommit _ pwrs => (∃ pwrsL : list dbmod, own_dbmap_in_slice pwrsS pwrsL pwrs)
156+
| CmdCommit _ pwrs => own_dbmap_in_slice pwrsS pwrs
156157
| _ => True
157158
end.
158159

‎src/program_proof/tulip/program/replica/replica_acquire.v

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,21 +6,22 @@ From Perennial.program_proof.tulip.program.replica Require Import
66
Section program.
77
Context `{!heapGS Σ, !tulip_ghostG Σ}.
88

9-
Theorem wp_Replica__acquire rp (tsW : u64) pwrsS pwrsL pwrs ptsm sptsm :
9+
Theorem wp_Replica__acquire rp (tsW : u64) pwrsS pwrs ptsm sptsm :
1010
valid_wrs pwrs ->
1111
let ts := uint.nat tsW in
12-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_ptsm_sptsm rp ptsm sptsm }}}
12+
{{{ own_dbmap_in_slice pwrsS pwrs ∗ own_replica_ptsm_sptsm rp ptsm sptsm }}}
1313
Replica__acquire #rp #tsW (to_val pwrsS)
1414
{{{ (acquired : bool), RET #acquired;
15-
own_dbmap_in_slice pwrsS pwrsL pwrs ∗
15+
own_dbmap_in_slice pwrsS pwrs ∗
1616
if acquired
1717
then own_replica_ptsm_sptsm rp (acquire ts pwrs ptsm) (acquire ts pwrs sptsm) ∗
1818
⌜validated_ptsm ptsm pwrs⌝ ∗
1919
⌜validated_sptsm sptsm ts pwrs⌝
2020
else own_replica_ptsm_sptsm rp ptsm sptsm
2121
}}}.
2222
Proof.
23-
iIntros (Hvw ts Φ) "[[HpwrsS %HpwrsL] Hrp] HΦ".
23+
iIntros (Hvw ts Φ) "[Hpwrs Hrp] HΦ".
24+
iDestruct "Hpwrs" as (pwrsL) "[HpwrsS %HpwrsL]".
2425
wp_rec.
2526
iDestruct (own_replica_ptsm_sptsm_dom with "Hrp") as %[Hdomptsm Hdomsptsm].
2627

‎src/program_proof/tulip/program/replica/replica_apply_commit.v

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,19 @@ Section program.
66
Context `{!heapGS Σ, !tulip_ghostG Σ}.
77

88
Theorem wp_Replica__applyCommit
9-
rp (tsW : u64) pwrsS pwrsL pwrs cloga gid rid γ α :
9+
rp (tsW : u64) pwrsS pwrs cloga gid rid γ α :
1010
let ts := uint.nat tsW in
1111
let cloga' := cloga ++ [CmdCommit ts pwrs] in
1212
valid_pwrs gid pwrs ->
1313
group_histm_lbs_from_log γ gid cloga' -∗
1414
is_txn_log_lb γ gid cloga' -∗
1515
is_replica_idx rp γ α -∗
16-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗
16+
{{{ own_dbmap_in_slice pwrsS pwrs ∗
1717
own_replica_with_cloga_no_lsna rp cloga gid rid γ α
1818
}}}
1919
Replica__applyCommit #rp #tsW (to_val pwrsS)
2020
{{{ RET #();
21-
own_dbmap_in_slice pwrsS pwrsL pwrs ∗
21+
own_dbmap_in_slice pwrsS pwrs ∗
2222
own_replica_with_cloga_no_lsna rp cloga' gid rid γ α
2323
}}}.
2424
Proof.

‎src/program_proof/tulip/program/replica/replica_commit.v

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Section program.
1212
let ts := uint.nat tsW in
1313
safe_commit γ gid ts pwrs -∗
1414
is_replica rp gid rid γ -∗
15-
{{{ ∃ l, own_dbmap_in_slice pwrsS l pwrs }}}
15+
{{{ own_dbmap_in_slice pwrsS pwrs }}}
1616
Replica__Commit #rp #tsW (to_val pwrsS)
1717
{{{ (ok : bool), RET #ok; True }}}.
1818
Proof.
@@ -43,7 +43,6 @@ Section program.
4343
(*@ @*)
4444
iNamed "Hrp". iNamed "Htxnlog".
4545
wp_loadField.
46-
iDestruct "Hpwrs" as (l) "Hpwrs".
4746
wp_apply (wp_TxnLog__SubmitCommit with "Htxnlog Hpwrs").
4847
iInv "Hinv" as "> HinvO" "HinvC".
4948
iNamed "HinvO".

‎src/program_proof/tulip/program/replica/replica_fast_prepare.v

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,13 @@ Section program.
88
Context `{!heapGS Σ, !tulip_ghostG Σ}.
99

1010
Theorem wp_Replica__fastPrepare
11-
rp (tsW : u64) pwrsS pwrsL pwrs gid rid γ α :
11+
rp (tsW : u64) pwrsS pwrs gid rid γ α :
1212
let ts := uint.nat tsW in
1313
gid ∈ gids_all ->
1414
rid ∈ rids_all ->
1515
safe_txn_pwrs γ gid ts pwrs -∗
1616
know_tulip_inv γ -∗
17-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica rp gid rid γ α }}}
17+
{{{ own_dbmap_in_slice pwrsS pwrs ∗ own_replica rp gid rid γ α }}}
1818
Replica__fastPrepare #rp #tsW (to_val pwrsS) slice.nil
1919
{{{ (res : rpres), RET #(rpres_to_u64 res);
2020
own_replica rp gid rid γ α ∗ fast_prepare_outcome γ gid rid ts res
@@ -274,11 +274,11 @@ Section program.
274274
Qed.
275275

276276
Theorem wp_Replica__FastPrepare
277-
rp (tsW : u64) pwrsS pwrsL pwrs gid rid γ :
277+
rp (tsW : u64) pwrsS pwrs gid rid γ :
278278
let ts := uint.nat tsW in
279279
safe_txn_pwrs γ gid ts pwrs -∗
280280
is_replica rp gid rid γ -∗
281-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs }}}
281+
{{{ own_dbmap_in_slice pwrsS pwrs }}}
282282
Replica__FastPrepare #rp #tsW (to_val pwrsS) slice.nil
283283
{{{ (res : rpres), RET #(rpres_to_u64 res);
284284
fast_prepare_outcome γ gid rid ts res

‎src/program_proof/tulip/program/replica/replica_multiwrite.v

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,22 +6,23 @@ From Perennial.program_proof.tulip.program.index Require Import index.
66
Section program.
77
Context `{!heapGS Σ, !tulip_ghostG Σ}.
88

9-
Theorem wp_Replica__multiwrite rp (tsW : u64) pwrsS pwrsL pwrs histm gid γ α :
9+
Theorem wp_Replica__multiwrite rp (tsW : u64) pwrsS pwrs histm gid γ α :
1010
let ts := uint.nat tsW in
1111
let histm' := multiwrite ts pwrs histm in
1212
valid_pwrs gid pwrs ->
1313
dom histm = keys_all ->
1414
safe_extension ts pwrs histm ->
1515
([∗ map] k ↦ h ∈ filter_group gid histm', is_repl_hist_lb γ k h) -∗
1616
is_replica_idx rp γ α -∗
17-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_histm rp histm α }}}
17+
{{{ own_dbmap_in_slice pwrsS pwrs ∗ own_replica_histm rp histm α }}}
1818
Replica__multiwrite #rp #tsW (to_val pwrsS)
1919
{{{ RET #();
20-
own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_histm rp histm' α
20+
own_dbmap_in_slice pwrsS pwrs ∗ own_replica_histm rp histm' α
2121
}}}.
2222
Proof.
2323
iIntros (ts histm' Hvw Hdomhistm Hlenhistm) "#Hrlbs #Hidx".
24-
iIntros (Φ) "!> [[HpwrsS %Hpwrs] Hhistm] HΦ".
24+
iIntros (Φ) "!> [Hpwrs Hhistm] HΦ".
25+
iDestruct "Hpwrs" as (pwrsL) "[HpwrsS %HpwrsL]".
2526
wp_rec.
2627

2728
(*@ func (rp *Replica) multiwrite(ts uint64, pwrs []tulip.WriteEntry) { @*)
@@ -56,15 +57,15 @@ Section program.
5657
wp_loadField.
5758
(* Prove [k] in the domain of [pwrs] and in [keys_all]. *)
5859
apply elem_of_list_lookup_2 in Hi as Hpwrsv.
59-
rewrite -Hpwrs elem_of_map_to_list in Hpwrsv.
60+
rewrite -HpwrsL elem_of_map_to_list in Hpwrsv.
6061
apply elem_of_dom_2 in Hpwrsv as Hdompwrs.
6162
assert (Hvk : k ∈ keys_all).
6263
{ clear -Hvw Hdompwrs. set_solver. }
6364
wp_apply (wp_Index__GetTuple with "Hidx"); first apply Hvk.
6465
iIntros (tpl) "#Htpl".
6566
(* Obtain proof that the current key [k] has not been written. *)
6667
pose proof (NoDup_fst_map_to_list pwrs) as Hnd.
67-
rewrite Hpwrs in Hnd.
68+
rewrite HpwrsL in Hnd.
6869
pose proof (list_lookup_fmap fst pwrsL (uint.nat i)) as Hk.
6970
rewrite Hi /= in Hk.
7071
pose proof (not_elem_of_take _ _ _ Hnd Hk) as Htake.
@@ -120,7 +121,7 @@ Section program.
120121
iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS".
121122
wp_pures.
122123
iApply "HΦ".
123-
pose proof (list_to_map_flip _ _ Hpwrs) as Hltm.
124+
pose proof (list_to_map_flip _ _ HpwrsL) as Hltm.
124125
rewrite -Hlenpwrs firstn_all -Hltm.
125126
by iFrame.
126127
Qed.

‎src/program_proof/tulip/program/replica/replica_release.v

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,16 +5,17 @@ From Perennial.program_proof.tulip.program.replica Require Import
55
Section program.
66
Context `{!heapGS Σ, !tulip_ghostG Σ}.
77

8-
Theorem wp_Replica__release rp pwrsS pwrsL pwrs ptsm sptsm :
8+
Theorem wp_Replica__release rp pwrsS pwrs ptsm sptsm :
99
valid_wrs pwrs ->
10-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_ptsm_sptsm rp ptsm sptsm }}}
10+
{{{ own_dbmap_in_slice pwrsS pwrs ∗ own_replica_ptsm_sptsm rp ptsm sptsm }}}
1111
Replica__release #rp (to_val pwrsS)
1212
{{{ RET #();
13-
own_dbmap_in_slice pwrsS pwrsL pwrs ∗
13+
own_dbmap_in_slice pwrsS pwrs ∗
1414
own_replica_ptsm_sptsm rp (release pwrs ptsm) sptsm
1515
}}}.
1616
Proof.
17-
iIntros (Hvw Φ) "[[HpwrsS %Hpwrs] Hrp] HΦ".
17+
iIntros (Hvw Φ) "[Hpwrs Hrp] HΦ".
18+
iDestruct "Hpwrs" as (pwrsL) "[HpwrsS %HpwrsL]".
1819
wp_rec.
1920
iDestruct (own_replica_ptsm_sptsm_dom with "Hrp") as %[Hdomptsm Hdomsptsm].
2021

@@ -45,22 +46,22 @@ Section program.
4546
iIntros "Hrp".
4647
iApply "HΦ".
4748
(* Obtain proof that the current key [k] has not been written. *)
48-
pose proof (map_to_list_not_elem_of_take_key _ _ _ _ Hpwrs Hi) as Htake.
49+
pose proof (map_to_list_not_elem_of_take_key _ _ _ _ HpwrsL Hi) as Htake.
4950
(* Adjust the goal. *)
5051
rewrite uint_nat_word_add_S; last by word.
5152
rewrite (take_S_r _ _ _ Hi) list_to_map_snoc; last apply Htake.
5253
set pwrs' := list_to_map _.
5354
rewrite /release setts_insert; last first.
5455
{ apply elem_of_list_lookup_2 in Hi.
55-
rewrite -Hpwrs in Hi.
56+
rewrite -HpwrsL in Hi.
5657
apply elem_of_map_to_list, elem_of_dom_2 in Hi.
5758
clear -Hvw Hi Hdomptsm. set_solver.
5859
}
5960
done.
6061
}
6162
iIntros "[Hrp HpwrsS]".
6263
subst P. simpl.
63-
pose proof (list_to_map_flip _ _ Hpwrs) as Hltm.
64+
pose proof (list_to_map_flip _ _ HpwrsL) as Hltm.
6465
rewrite -Hlenpwrs firstn_all Hltm.
6566
iDestruct ("HpwrsC" with "HpwrsS") as "HpwrsS".
6667
wp_pures.

‎src/program_proof/tulip/program/replica/replica_repr.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ Section repr.
5252
∃ (prepmP : loc) (prepmS : gmap u64 Slice.t) (prepm : gmap u64 dbmap),
5353
"HprepmP" ∷ rp ↦[Replica :: "prepm"] #prepmP ∗
5454
"HprepmS" ∷ own_map prepmP (DfracOwn 1) prepmS ∗
55-
"Hprepm" ∷ ([∗ map] s; m ∈ prepmS; prepm, ∃ l, own_dbmap_in_slice s l m) ∗
55+
"Hprepm" ∷ ([∗ map] s; m ∈ prepmS; prepm, own_dbmap_in_slice s m) ∗
5656
"%Hcpmabs" ∷ ⌜(kmap Z.of_nat cpm : gmap Z dbmap) = kmap uint.Z prepm⌝.
5757

5858
Definition absrel_ptsm (ptsm : gmap dbkey nat) (ptsmM : gmap dbkey u64) :=

‎src/program_proof/tulip/program/replica/replica_request_session.v

Lines changed: 5 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,9 @@ Section decode.
4444
DecodeTxnRequest (to_val dataP)
4545
{{{ (pwrsP : Slice.t), RET (txnreq_to_val req pwrsP);
4646
match req with
47-
| FastPrepareReq _ pwrs => (∃ pwrsL, own_dbmap_in_slice pwrsP pwrsL pwrs)
48-
| ValidateReq _ _ pwrs => (∃ pwrsL, own_dbmap_in_slice pwrsP pwrsL pwrs)
49-
| CommitReq _ pwrs => (∃ pwrsL, own_dbmap_in_slice pwrsP pwrsL pwrs)
47+
| FastPrepareReq _ pwrs => own_dbmap_in_slice pwrsP pwrs
48+
| ValidateReq _ _ pwrs => own_dbmap_in_slice pwrsP pwrs
49+
| CommitReq _ pwrs => own_dbmap_in_slice pwrsP pwrs
5050
| _ => True
5151
end
5252
}}}.
@@ -211,20 +211,14 @@ Section program.
211211
iDestruct "Herr" as "%Hmsg".
212212
apply Henc in Hmsg as Hreq.
213213
destruct Hreq as (req & Hinreqs & Hreq). simpl in Hreq.
214-
(* assert (∃ req, retdata = encode_txnreq req ∧ req ∈ reqs) as (req & Hreq & Hinreqs). *)
215-
(* { specialize (Henc retdata). *)
216-
(* apply (elem_of_map_2 msg_data (D := gset (list u8))) in Hmsg. *)
217-
(* specialize (Henc Hmsg). *)
218-
(* by rewrite elem_of_map in Henc. *)
219-
(* } *)
220214

221215
(*@ req := message.DecodeTxnRequest(ret.Data) @*)
222216
(*@ kind := req.Kind @*)
223217
(*@ ts := req.Timestamp @*)
224218
(*@ @*)
225219
wp_apply (wp_DecodeTxnRequest with "Hretdata").
226220
{ apply Hreq. }
227-
iIntros (entsaP) "Hentsa".
221+
iIntros (pwrsP) "Hpwrs".
228222
assert (Hrid : rid ∈ rids_all).
229223
{ apply elem_of_dom_2 in Haddr. by rewrite Hdomaddrm in Haddr. }
230224
destruct req; wp_pures.
@@ -312,8 +306,6 @@ Section program.
312306
(*@ grove_ffi.Send(conn, data) @*)
313307
(*@ @*)
314308
iDestruct (big_sepS_elem_of with "Hreqs") as "Hsafe"; first apply Hinreqs.
315-
simpl.
316-
iDestruct "Hentsa" as (pwrsL) "Hpwrs".
317309
wp_apply (wp_Replica__FastPrepare with "Hsafe Hrp Hpwrs").
318310
iIntros (res) "#Houtcome".
319311
wp_loadField.
@@ -376,7 +368,6 @@ Section program.
376368
(*@ @*)
377369
iDestruct (big_sepS_elem_of with "Hreqs") as "Hsafe"; first apply Hinreqs.
378370
simpl.
379-
iDestruct "Hentsa" as (pwrsL) "Hpwrs".
380371
wp_apply (wp_Replica__Validate with "Hsafe Hrp Hpwrs").
381372
iIntros (res) "#Houtcome".
382373
wp_loadField.
@@ -627,7 +618,7 @@ Section program.
627618
(*@ } @*)
628619
(*@ @*)
629620
iDestruct (big_sepS_elem_of with "Hreqs") as "Hsafe"; first apply Hinreqs.
630-
wp_apply (wp_Replica__Commit with "Hsafe Hrp Hentsa").
621+
wp_apply (wp_Replica__Commit with "Hsafe Hrp Hpwrs").
631622
iIntros (ok) "_".
632623
wp_pures.
633624
destruct ok; wp_pures.

‎src/program_proof/tulip/program/replica/replica_validate.v

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,13 @@ Section program.
77
Context `{!heapGS Σ, !tulip_ghostG Σ}.
88

99
Theorem wp_Replica__validate
10-
rp (tsW : u64) pwrsS pwrsL pwrs gid rid γ α :
10+
rp (tsW : u64) pwrsS pwrs gid rid γ α :
1111
let ts := uint.nat tsW in
1212
gid ∈ gids_all ->
1313
rid ∈ rids_all ->
1414
safe_txn_pwrs γ gid ts pwrs -∗
1515
know_tulip_inv γ -∗
16-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica rp gid rid γ α }}}
16+
{{{ own_dbmap_in_slice pwrsS pwrs ∗ own_replica rp gid rid γ α }}}
1717
Replica__validate #rp #tsW (to_val pwrsS) slice.nil
1818
{{{ (res : rpres), RET #(rpres_to_u64 res);
1919
own_replica rp gid rid γ α ∗ validate_outcome γ gid rid ts res
@@ -156,11 +156,11 @@ Section program.
156156
Qed.
157157

158158
Theorem wp_Replica__Validate
159-
rp (tsW rankW : u64) pwrsS pwrsL pwrs gid rid γ :
159+
rp (tsW rankW : u64) pwrsS pwrs gid rid γ :
160160
let ts := uint.nat tsW in
161161
safe_txn_pwrs γ gid ts pwrs -∗
162162
is_replica rp gid rid γ -∗
163-
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs }}}
163+
{{{ own_dbmap_in_slice pwrsS pwrs }}}
164164
Replica__Validate #rp #tsW #rankW (to_val pwrsS) slice.nil
165165
{{{ (res : rpres), RET #(rpres_to_u64 res);
166166
validate_outcome γ gid rid ts res

0 commit comments

Comments
 (0)