Skip to content

Commit e327487

Browse files
yunshengtwyunshengtw
committed
Move to a relational approach to encode map
1 parent c45b857 commit e327487

File tree

9 files changed

+414
-95
lines changed

9 files changed

+414
-95
lines changed

‎external/Goose/github_com/mit_pdos/tulip/util.v

Lines changed: 12 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -51,39 +51,34 @@ Definition CountBoolMap: val :=
5151

5252
Definition EncodeString: val :=
5353
rec: "EncodeString" "bs" "str" :=
54-
let: "data" := ref_to (slice.T byteT) "bs" in
55-
"data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") (StringLength "str"));;
56-
"data" <-[slice.T byteT] (marshal.WriteBytes (![slice.T byteT] "data") (StringToBytes "str"));;
57-
![slice.T byteT] "data".
54+
let: "bs1" := marshal.WriteInt "bs" (StringLength "str") in
55+
let: "data" := marshal.WriteBytes "bs1" (StringToBytes "str") in
56+
"data".
5857

5958
Definition EncodeStrings: val :=
6059
rec: "EncodeStrings" "bs" "strs" :=
61-
let: "data" := ref_to (slice.T byteT) "bs" in
62-
"data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") (slice.len "strs"));;
60+
let: "data" := ref_to (slice.T byteT) (marshal.WriteInt "bs" (slice.len "strs")) in
6361
ForSlice stringT <> "s" "strs"
6462
("data" <-[slice.T byteT] (EncodeString (![slice.T byteT] "data") "s"));;
6563
![slice.T byteT] "data".
6664

6765
Definition DecodeString: val :=
6866
rec: "DecodeString" "bs" :=
69-
let: "data" := ref_to (slice.T byteT) "bs" in
70-
let: ("sz", "data") := marshal.ReadInt (![slice.T byteT] "data") in
71-
let: ("bsr", "data") := marshal.ReadBytes (![slice.T byteT] "data") "sz" in
72-
(StringFromBytes "bsr", ![slice.T byteT] "data").
67+
let: ("sz", "bs1") := marshal.ReadInt "bs" in
68+
let: ("bsr", "data") := marshal.ReadBytes "bs1" "sz" in
69+
(StringFromBytes "bsr", "data").
7370

7471
Definition DecodeStrings: val :=
7572
rec: "DecodeStrings" "bs" :=
76-
let: "data" := ref_to (slice.T byteT) "bs" in
77-
let: ("n", "data") := marshal.ReadInt (![slice.T byteT] "data") in
73+
let: ("n", "bs1") := marshal.ReadInt "bs" in
74+
let: "data" := ref_to (slice.T byteT) "bs1" in
7875
let: "ents" := ref_to (slice.T stringT) (NewSliceWithCap stringT #0 "n") in
7976
let: "i" := ref_to uint64T #0 in
80-
let: "s" := ref (zero_val stringT) in
8177
Skip;;
8278
(for: (λ: <>, (![uint64T] "i") < "n"); (λ: <>, Skip) := λ: <>,
83-
let: ("0_ret", "1_ret") := DecodeString (![slice.T byteT] "data") in
84-
"s" <-[stringT] "0_ret";;
85-
"data" <-[slice.T byteT] "1_ret";;
86-
"ents" <-[slice.T stringT] (SliceAppend stringT (![slice.T stringT] "ents") (![stringT] "s"));;
79+
let: ("s", "bsloop") := DecodeString (![slice.T byteT] "data") in
80+
"ents" <-[slice.T stringT] (SliceAppend stringT (![slice.T stringT] "ents") "s");;
81+
"data" <-[slice.T byteT] "bsloop";;
8782
"i" <-[uint64T] ((![uint64T] "i") + #1);;
8883
Continue);;
8984
(![slice.T stringT] "ents", ![slice.T byteT] "data").

‎src/program_proof/tulip/base.v

Lines changed: 0 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -251,68 +251,3 @@ Class tulip_ghostG (Σ : gFunctors).
251251

252252
Record tulip_names := {}.
253253
Record replica_names := {}.
254-
255-
Section msg.
256-
257-
Inductive txnreq :=
258-
| ReadReq (ts : u64) (key : string)
259-
| FastPrepareReq (ts : u64) (pwrs : dbmap)
260-
| ValidateReq (ts : u64) (rank : u64) (pwrs : dbmap)
261-
| PrepareReq (ts : u64) (rank : u64)
262-
| UnprepareReq (ts : u64) (rank : u64)
263-
| QueryReq (ts : u64) (rank : u64)
264-
| RefreshReq (ts : u64) (rank : u64)
265-
| CommitReq (ts : u64) (pwrs : dbmap)
266-
| AbortReq (ts : u64).
267-
268-
#[global]
269-
Instance txnreq_eq_decision :
270-
EqDecision txnreq.
271-
Proof. solve_decision. Qed.
272-
273-
#[global]
274-
Instance txnreq_countable :
275-
Countable txnreq.
276-
Admitted.
277-
278-
Definition encode_txnreq (req : txnreq) : list u8.
279-
Admitted.
280-
281-
Inductive rpres :=
282-
| ReplicaOK
283-
| ReplicaCommittedTxn
284-
| ReplicaAbortedTxn
285-
| ReplicaStaleCoordinator
286-
| ReplicaFailedValidation
287-
| ReplicaInvalidRank
288-
| ReplicaWrongLeader.
289-
290-
#[global]
291-
Instance rpres_eq_decision :
292-
EqDecision rpres.
293-
Proof. solve_decision. Qed.
294-
295-
Inductive txnresp :=
296-
| ReadResp (ts : u64) (rid : u64) (key : string) (ver : dbpver) (slow : bool)
297-
| FastPrepareResp (ts : u64) (rid : u64) (res : rpres)
298-
| ValidateResp (ts : u64) (rid : u64) (res : rpres)
299-
| PrepareResp (ts : u64) (rank : u64) (rid : u64) (res : rpres)
300-
| UnprepareResp (ts : u64) (rank : u64) (rid : u64) (res : rpres)
301-
| QueryResp (ts : u64) (res : rpres)
302-
| CommitResp (ts : u64) (res : rpres)
303-
| AbortResp (ts : u64) (res : rpres).
304-
305-
#[global]
306-
Instance txnresp_eq_decision :
307-
EqDecision txnresp.
308-
Proof. solve_decision. Qed.
309-
310-
#[global]
311-
Instance txnresp_countable :
312-
Countable txnresp.
313-
Admitted.
314-
315-
Definition encode_txnresp (resp : txnresp) : list u8.
316-
Admitted.
317-
318-
End msg.

‎src/program_proof/tulip/encode.v

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
From Perennial.program_proof Require Import grove_prelude.
2+
From Perennial.program_proof.tulip Require Import base.
3+
4+
Definition encode_string (x : string) : list u8 :=
5+
let bs := string_to_bytes x in
6+
u64_le (U64 (length bs)) ++ bs.
7+
8+
Opaque encode_string.
9+
10+
Definition encode_strings_step (bs : list u8) (x : string) : list u8 :=
11+
bs ++ encode_string x.
12+
13+
Definition encode_strings_xlen (xs : list string) : list u8 :=
14+
foldl encode_strings_step [] xs.
15+
16+
Definition encode_strings (xs : list string) : list u8 :=
17+
u64_le (U64 (length xs)) ++ encode_strings_xlen xs.
18+
19+
Lemma encode_strings_xlen_snoc xs x :
20+
encode_strings_xlen (xs ++ [x]) = encode_strings_xlen xs ++ encode_string x.
21+
Proof.
22+
by rewrite /encode_strings_xlen foldl_snoc /encode_strings_step.
23+
Qed.
24+
25+
Lemma foldl_encode_strings_step_app (bs : list u8) (xs : list string) :
26+
foldl encode_strings_step bs xs = bs ++ foldl encode_strings_step [] xs.
27+
Proof.
28+
generalize dependent bs.
29+
induction xs as [| x xs IH]; intros bs.
30+
{ by rewrite /= app_nil_r. }
31+
rewrite /= (IH (encode_strings_step bs x)) (IH (encode_strings_step [] x)).
32+
rewrite {1 3}/encode_strings_step.
33+
by rewrite app_nil_l app_assoc.
34+
Qed.
35+
36+
Lemma encode_strings_xlen_cons xs x :
37+
encode_strings_xlen (x :: xs) = encode_string x ++ encode_strings_xlen xs.
38+
Proof.
39+
rewrite /encode_strings_xlen /= foldl_encode_strings_step_app.
40+
by rewrite {1}/encode_strings_step app_nil_l.
41+
Qed.
42+
43+
Lemma encode_strings_xlen_length_inv xs n :
44+
(length (encode_strings_xlen xs) ≤ n)%nat ->
45+
(length xs ≤ n)%nat.
46+
Proof.
47+
generalize dependent n.
48+
induction xs as [| x xs IH]; intros n; first done.
49+
rewrite encode_strings_xlen_cons length_app /=.
50+
assert (length (encode_string x) ≠ O).
51+
{ by destruct (nil_or_length_pos (encode_string x)). }
52+
intros Hlen.
53+
assert (Hlenxs : (length xs ≤ pred n)%nat).
54+
{ apply IH. lia. }
55+
lia.
56+
Qed.
57+
58+
Lemma encode_strings_length_inv xs n :
59+
(length (encode_strings xs) ≤ n)%nat ->
60+
(length xs ≤ n)%nat.
61+
Proof.
62+
rewrite /encode_strings length_app.
63+
intros Hn.
64+
pose proof (encode_strings_xlen_length_inv xs n) as Hlen.
65+
lia.
66+
Qed.
67+
68+
Definition encode_dbval (x : dbval) : list u8 :=
69+
match x with
70+
| Some v => [U8 0] ++ encode_string v
71+
| None => [U8 1]
72+
end.
73+
74+
Definition encode_dbmod (x : dbmod) : list u8 :=
75+
encode_string x.1 ++ encode_dbval x.2.
76+
77+
Fixpoint encode_dbmods (xs : list dbmod) : list u8 :=
78+
match xs with
79+
| x :: tail => encode_dbmod x ++ encode_dbmods tail
80+
| _ => []
81+
end.
82+
83+
Definition encode_dbmap (m : dbmap) (data : list u8) :=
84+
∃ xs, data = u64_le (size m) ++ encode_dbmods xs ∧ xs ≡ₚ map_to_list m.

‎src/program_proof/tulip/inv.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
From Perennial.program_proof Require Import grove_prelude.
22
From Perennial.program_proof.rsm Require Import big_sep.
33
From Perennial.program_proof.rsm.pure Require Import vslice extend quorum fin_maps.
4-
From Perennial.program_proof.tulip Require Import base res cmd.
4+
From Perennial.program_proof.tulip Require Import base res cmd msg.
55
From Perennial.program_proof.tulip Require Export inv_txnsys inv_key inv_group inv_replica.
66

77
Section inv.
@@ -222,7 +222,7 @@ Section inv_network.
222222
(* senders are always reachable *)
223223
"#Hsender" ∷ ([∗ set] trml ∈ set_map msg_sender ms, is_terminal γ gid trml) ∗
224224
"#Hreqs" ∷ ([∗ set] req ∈ reqs, safe_txnreq γ gid req) ∗
225-
"%Henc" ∷ ⌜(set_map msg_data ms : gset (list u8)) ⊆ set_map encode_txnreq reqs⌝.
225+
"%Henc" ∷ ⌜set_Forall (λ x, ∃ req, req ∈ reqs ∧ encode_txnreq req (msg_data x)) ms⌝.
226226

227227
Definition connect_inv (trml : chan) (ms : gset message) gid γ : iProp Σ :=
228228
∃ (resps : gset txnresp),

‎src/program_proof/tulip/msg.v

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
From Perennial.program_proof Require Import grove_prelude.
2+
From Perennial.program_proof.tulip Require Import base encode.
3+
4+
Inductive txnreq :=
5+
| ReadReq (ts : u64) (key : string)
6+
| FastPrepareReq (ts : u64) (pwrs : dbmap)
7+
| ValidateReq (ts : u64) (rank : u64) (pwrs : dbmap)
8+
| PrepareReq (ts : u64) (rank : u64)
9+
| UnprepareReq (ts : u64) (rank : u64)
10+
| QueryReq (ts : u64) (rank : u64)
11+
| RefreshReq (ts : u64) (rank : u64)
12+
| CommitReq (ts : u64) (pwrs : dbmap)
13+
| AbortReq (ts : u64).
14+
15+
#[global]
16+
Instance txnreq_eq_decision :
17+
EqDecision txnreq.
18+
Proof. solve_decision. Qed.
19+
20+
#[global]
21+
Instance txnreq_countable :
22+
Countable txnreq.
23+
Admitted.
24+
25+
Definition encode_fast_prepare_req (ts : u64) (pwrs : dbmap) (data : list u8) :=
26+
∃ datapwrs, data = u64_le (U64 201) ++ u64_le ts ++ datapwrs ∧ encode_dbmap pwrs datapwrs.
27+
28+
Definition encode_txnreq (req : txnreq) (data : list u8) :=
29+
match req with
30+
| FastPrepareReq ts pwrs => encode_fast_prepare_req ts pwrs data
31+
| _ => True
32+
end.
33+
34+
Inductive rpres :=
35+
| ReplicaOK
36+
| ReplicaCommittedTxn
37+
| ReplicaAbortedTxn
38+
| ReplicaStaleCoordinator
39+
| ReplicaFailedValidation
40+
| ReplicaInvalidRank
41+
| ReplicaWrongLeader.
42+
43+
#[global]
44+
Instance rpres_eq_decision :
45+
EqDecision rpres.
46+
Proof. solve_decision. Qed.
47+
48+
Inductive txnresp :=
49+
| ReadResp (ts : u64) (rid : u64) (key : string) (ver : dbpver) (slow : bool)
50+
| FastPrepareResp (ts : u64) (rid : u64) (res : rpres)
51+
| ValidateResp (ts : u64) (rid : u64) (res : rpres)
52+
| PrepareResp (ts : u64) (rank : u64) (rid : u64) (res : rpres)
53+
| UnprepareResp (ts : u64) (rank : u64) (rid : u64) (res : rpres)
54+
| QueryResp (ts : u64) (res : rpres)
55+
| CommitResp (ts : u64) (res : rpres)
56+
| AbortResp (ts : u64) (res : rpres).
57+
58+
#[global]
59+
Instance txnresp_eq_decision :
60+
EqDecision txnresp.
61+
Proof. solve_decision. Qed.
62+
63+
#[global]
64+
Instance txnresp_countable :
65+
Countable txnresp.
66+
Admitted.
67+
68+
Definition encode_txnresp (resp : txnresp) : list u8.
69+
Admitted.

‎src/program_proof/tulip/prelude.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,4 @@ From Perennial.program_proof.rsm.pure Require Export
55
dual_lookup extend fin_maps fin_maps_list fin_sets largest_before list misc nat
66
nonexpanding_merge sets vslice word quorum.
77
From Perennial.program_proof.tulip Require Export
8-
action base cmd res inv stability.
8+
action base cmd encode res msg inv stability.

‎src/program_proof/tulip/program/gcoord/gcoord_send.v

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Section encode.
1010
EncodeTxnReadRequest #ts #(LitString key)
1111
{{{ (dataP : Slice.t) (data : list u8), RET (to_val dataP);
1212
own_slice dataP byteT (DfracOwn 1) data ∗
13-
⌜data = encode_txnreq (ReadReq ts key)⌝
13+
⌜encode_txnreq (ReadReq ts key) data⌝
1414
}}}.
1515
Proof.
1616
Admitted.
@@ -146,8 +146,12 @@ Section program.
146146
iSplit.
147147
{ iApply big_sepS_insert_2; [done | done]. }
148148
iPureIntro.
149-
rewrite 2!set_map_union_L 2!set_map_singleton_L /= -Hdataenc.
150-
set_solver.
149+
apply set_Forall_union; last first.
150+
{ apply (set_Forall_impl _ _ _ Henc). intros m Hm. clear -Hm. set_solver. }
151+
rewrite set_Forall_singleton.
152+
exists req.
153+
split; first set_solver.
154+
done.
151155
}
152156
rewrite insert_delete_insert.
153157
iMod "Hmask" as "_".

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

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ Section decode.
3939
Context `{!heapGS Σ, !tulip_ghostG Σ}.
4040

4141
Theorem wp_DecodeTxnRequest (dataP : Slice.t) (data : list u8) (req : txnreq) :
42-
data = encode_txnreq req ->
42+
encode_txnreq req data ->
4343
{{{ own_slice dataP byteT (DfracOwn 1) data }}}
4444
DecodeTxnRequest (to_val dataP)
4545
{{{ (pwrsP : Slice.t), RET (txnreq_to_val req pwrsP);
@@ -209,12 +209,14 @@ Section program.
209209
destruct err; wp_pures.
210210
{ by iApply "HΦ". }
211211
iDestruct "Herr" as "%Hmsg".
212-
assert (∃ req, retdata = encode_txnreq req ∧ req ∈ reqs) as (req & Hreq & Hinreqs).
213-
{ specialize (Henc retdata).
214-
apply (elem_of_map_2 msg_data (D := gset (list u8))) in Hmsg.
215-
specialize (Henc Hmsg).
216-
by rewrite elem_of_map in Henc.
217-
}
212+
apply Henc in Hmsg as Hreq.
213+
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+
(* } *)
218220

219221
(*@ req := message.DecodeTxnRequest(ret.Data) @*)
220222
(*@ kind := req.Kind @*)

0 commit comments

Comments
 (0)