Prove encoding/decoding of transaction response

external/Goose/github_com/mit_pdos/tulip/message.v

@@ -207,8 +207,8 @@ Definition EncodeTxnPrepareResponse: val :=
 Definition DecodeTxnPrepareResponse: val :=
   rec: "DecodeTxnPrepareResponse" "bs" :=
     let: ("ts", "bs1") := marshal.ReadInt "bs" in
-    let: ("rid", "bs2") := marshal.ReadInt "bs1" in
-    let: ("rank", "bs3") := marshal.ReadInt "bs2" in
+    let: ("rank", "bs2") := marshal.ReadInt "bs1" in
+    let: ("rid", "bs3") := marshal.ReadInt "bs2" in
     let: ("res", <>) := marshal.ReadInt "bs3" in
     struct.mk TxnResponse [
       "Kind" ::= MSG_TXN_PREPARE;
@@ -249,8 +249,8 @@ Definition EncodeTxnUnprepareResponse: val :=
 Definition DecodeTxnUnprepareResponse: val :=
   rec: "DecodeTxnUnprepareResponse" "bs" :=
     let: ("ts", "bs1") := marshal.ReadInt "bs" in
-    let: ("rid", "bs2") := marshal.ReadInt "bs1" in
-    let: ("rank", "bs3") := marshal.ReadInt "bs2" in
+    let: ("rank", "bs2") := marshal.ReadInt "bs1" in
+    let: ("rid", "bs3") := marshal.ReadInt "bs2" in
     let: ("res", <>) := marshal.ReadInt "bs3" in
     struct.mk TxnResponse [
       "Kind" ::= MSG_TXN_UNPREPARE;

src/program_proof/tulip/encode.v

@@ -136,3 +136,6 @@ Qed.
 
 Definition encode_dbmap (m : dbmap) (data : list u8) :=
   ∃ xs, data = encode_dbmods xs ∧ xs ≡ₚ map_to_list m.
+
+Definition encode_dbpver (x : dbpver) : list u8 :=
+  u64_le x.1 ++ encode_dbval x.2.

src/program_proof/tulip/msg.v

@@ -40,10 +40,10 @@ Definition encode_validate_req_xkind (ts rank : u64) (m : dbmap) (data : list u8
 Definition encode_validate_req (ts rank : u64) (m : dbmap) (data : list u8) :=
   ∃ reqdata, data = u64_le (U64 202) ++ reqdata ∧ encode_validate_req_xkind ts rank m reqdata.
 
-Definition encode_req_of_ts_rank_xkind (ts rank : u64) := u64_le ts ++ u64_le rank.
+Definition encode_ts_rank (ts rank : u64) := u64_le ts ++ u64_le rank.
 
-Definition encode_req_of_ts_rank (kind : u64) (ts rank : u64) (data : list u8) :=
-  data = u64_le kind ++ encode_req_of_ts_rank_xkind ts rank.
+Definition encode_txnreq_of_ts_rank (kind : u64) (ts rank : u64) (data : list u8) :=
+  data = u64_le kind ++ encode_ts_rank ts rank.
 
 Definition encode_commit_req_xkind (ts : u64) (m : dbmap) (data : list u8) :=
   ∃ mdata, data = u64_le ts ++ mdata ∧ encode_dbmap m mdata.
@@ -61,10 +61,10 @@ Definition encode_txnreq (req : txnreq) (data : list u8) :=
   | ReadReq ts key => encode_read_req ts key data
   | FastPrepareReq ts pwrs => encode_fast_prepare_req ts pwrs data
   | ValidateReq ts rank pwrs => encode_validate_req ts rank pwrs data
-  | PrepareReq ts rank => encode_req_of_ts_rank (U64 203) ts rank data
-  | UnprepareReq ts rank => encode_req_of_ts_rank (U64 204) ts rank data
-  | QueryReq ts rank => encode_req_of_ts_rank (U64 205) ts rank data
-  | RefreshReq ts rank => encode_req_of_ts_rank (U64 210) ts rank data
+  | PrepareReq ts rank => encode_txnreq_of_ts_rank (U64 203) ts rank data
+  | UnprepareReq ts rank => encode_txnreq_of_ts_rank (U64 204) ts rank data
+  | QueryReq ts rank => encode_txnreq_of_ts_rank (U64 205) ts rank data
+  | RefreshReq ts rank => encode_txnreq_of_ts_rank (U64 210) ts rank data
   | CommitReq ts pwrs => encode_commit_req ts pwrs data
   | AbortReq ts => encode_abort_req ts data
   end.
@@ -83,6 +83,22 @@ Instance rpres_eq_decision :
   EqDecision rpres.
 Proof. solve_decision. Qed.
 
+Definition rpres_to_u64 (r : rpres) :=
+  match r with
+  | ReplicaOK => (U64 0)
+  | ReplicaCommittedTxn => (U64 1)
+  | ReplicaAbortedTxn => (U64 2)
+  | ReplicaStaleCoordinator => (U64 3)
+  | ReplicaFailedValidation => (U64 4)
+  | ReplicaInvalidRank => (U64 5)
+  | ReplicaWrongLeader => (U64 6)
+  end.
+
+#[global]
+Instance rpres_to_u64_inj :
+  Inj eq eq rpres_to_u64.
+Proof. intros x y H. by destruct x, y. Defined.
+
 Inductive txnresp :=
 | ReadResp        (ts : u64) (rid : u64) (key : string) (ver : dbpver) (slow : bool)
 | FastPrepareResp (ts : u64) (rid : u64) (res : rpres)
@@ -103,5 +119,53 @@ Instance txnresp_countable :
   Countable txnresp.
 Admitted.
 
-Definition encode_txnresp (resp : txnresp) : list u8.
-Admitted.
+Definition encode_read_resp_xkind
+  (ts rid : u64) (key : string) (ver : dbpver) (slow : bool) :=
+  u64_le ts ++ u64_le rid ++ encode_string key ++
+    encode_dbpver ver ++ [if slow then U8 1 else U8 0].
+
+Definition encode_read_resp
+  (ts rid : u64) (key : string) (ver : dbpver) (slow : bool) :=
+  u64_le (U64 100) ++ encode_read_resp_xkind ts rid key ver slow.
+
+Definition encode_ts_rid_res (ts rid : u64) (res : rpres) :=
+  u64_le ts ++ u64_le rid ++ u64_le (rpres_to_u64 res).
+
+Definition encode_fast_prepare_resp (ts rid : u64) (res : rpres) :=
+  u64_le (U64 201) ++ encode_ts_rid_res ts rid res.
+
+Definition encode_validate_resp (ts rid : u64) (res : rpres) :=
+  u64_le (U64 202) ++ encode_ts_rid_res ts rid res.
+
+Definition encode_ts_rank_rid_res (ts rank rid : u64) (res : rpres) :=
+  u64_le ts ++ u64_le rank ++ u64_le rid ++ u64_le (rpres_to_u64 res).
+
+Definition encode_prepare_resp (ts rank rid : u64) (res : rpres) :=
+  u64_le (U64 203) ++ encode_ts_rank_rid_res ts rank rid res.
+
+Definition encode_unprepare_resp (ts rank rid : u64) (res : rpres) :=
+  u64_le (U64 204) ++ encode_ts_rank_rid_res ts rank rid res.
+
+Definition encode_ts_res (ts : u64) (res : rpres) :=
+  u64_le ts ++ u64_le (rpres_to_u64 res).
+
+Definition encode_query_resp (ts : u64) (res : rpres) :=
+  u64_le (U64 205) ++ encode_ts_res ts res.
+
+Definition encode_commit_resp (ts : u64) (res : rpres) :=
+  u64_le (U64 300) ++ encode_ts_res ts res.
+
+Definition encode_abort_resp (ts : u64) (res : rpres) :=
+  u64_le (U64 301) ++ encode_ts_res ts res.
+
+Definition encode_txnresp (resp : txnresp) : list u8 :=
+  match resp with
+  | ReadResp ts rid key ver slow => encode_read_resp ts rid key ver slow
+  | FastPrepareResp ts rid res => encode_fast_prepare_resp ts rid res
+  | ValidateResp ts rid res => encode_validate_resp ts rid res
+  | PrepareResp ts rank rid res => encode_prepare_resp ts rank rid res
+  | UnprepareResp ts rank rid res => encode_unprepare_resp ts rank rid res
+  | QueryResp ts res => encode_query_resp ts res
+  | CommitResp ts res => encode_commit_resp ts res
+  | AbortResp ts res => encode_abort_resp ts res
+  end.