diff --git a/external/Goose/github_com/mit_pdos/tulip/paxos.v b/external/Goose/github_com/mit_pdos/tulip/paxos.v index dcf04df37..ed7b3795a 100644 --- a/external/Goose/github_com/mit_pdos/tulip/paxos.v +++ b/external/Goose/github_com/mit_pdos/tulip/paxos.v @@ -352,13 +352,13 @@ Definition MSG_ACCEPT : expr := #1. Definition EncodeAcceptRequest: val := rec: "EncodeAcceptRequest" "term" "lsnc" "lsne" "ents" := - let: "data" := ref_to (slice.T byteT) (NewSliceWithCap byteT #0 #64) in - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") MSG_ACCEPT);; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "term");; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "lsnc");; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "lsne");; - "data" <-[slice.T byteT] (util.EncodeStrings (![slice.T byteT] "data") "ents");; - ![slice.T byteT] "data". + let: "bs" := NewSliceWithCap byteT #0 #64 in + let: "bs1" := marshal.WriteInt "bs" MSG_ACCEPT in + let: "bs2" := marshal.WriteInt "bs1" "term" in + let: "bs3" := marshal.WriteInt "bs2" "lsnc" in + let: "bs4" := marshal.WriteInt "bs3" "lsne" in + let: "data" := util.EncodeStrings "bs4" "ents" in + "data". Definition Paxos__GetConnection: val := rec: "Paxos__GetConnection" "px" "nid" := @@ -419,11 +419,11 @@ Definition Paxos__LeaderSession: val := Definition EncodePrepareRequest: val := rec: "EncodePrepareRequest" "term" "lsnc" := - let: "data" := ref_to (slice.T byteT) (NewSliceWithCap byteT #0 #24) in - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") MSG_PREPARE);; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "term");; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "lsnc");; - ![slice.T byteT] "data". + let: "bs" := NewSliceWithCap byteT #0 #24 in + let: "bs1" := marshal.WriteInt "bs" MSG_PREPARE in + let: "bs2" := marshal.WriteInt "bs1" "term" in + let: "data" := marshal.WriteInt "bs2" "lsnc" in + "data". Definition Paxos__ElectionSession: val := rec: "Paxos__ElectionSession" "px" := @@ -488,11 +488,11 @@ Definition PaxosResponse := struct.decl [ ]. Definition DecodePrepareResponse: val := - rec: "DecodePrepareResponse" "data" := - let: ("nid", "data") := marshal.ReadInt "data" in - let: ("term", "data") := marshal.ReadInt "data" in - let: ("terma", "data") := marshal.ReadInt "data" in - let: ("ents", "data") := util.DecodeStrings "data" in + rec: "DecodePrepareResponse" "bs" := + let: ("nid", "bs1") := marshal.ReadInt "bs" in + let: ("term", "bs2") := marshal.ReadInt "bs1" in + let: ("terma", "bs3") := marshal.ReadInt "bs2" in + let: ("ents", <>) := util.DecodeStrings "bs3" in struct.mk PaxosResponse [ "Kind" ::= MSG_PREPARE; "NodeID" ::= "nid"; @@ -502,10 +502,10 @@ Definition DecodePrepareResponse: val := ]. Definition DecodeAcceptResponse: val := - rec: "DecodeAcceptResponse" "data" := - let: ("nid", "data") := marshal.ReadInt "data" in - let: ("term", "data") := marshal.ReadInt "data" in - let: ("lsn", "data") := marshal.ReadInt "data" in + rec: "DecodeAcceptResponse" "bs" := + let: ("nid", "bs1") := marshal.ReadInt "bs" in + let: ("term", "bs2") := marshal.ReadInt "bs1" in + let: ("lsn", <>) := marshal.ReadInt "bs2" in struct.mk PaxosResponse [ "Kind" ::= MSG_ACCEPT; "NodeID" ::= "nid"; @@ -514,16 +514,20 @@ Definition DecodeAcceptResponse: val := ]. Definition DecodeResponse: val := - rec: "DecodeResponse" "data" := - let: ("kind", "data") := marshal.ReadInt "data" in - let: "resp" := ref (zero_val (struct.t PaxosResponse)) in + rec: "DecodeResponse" "bs" := + let: ("kind", "data") := marshal.ReadInt "bs" in (if: "kind" = MSG_PREPARE - then "resp" <-[struct.t PaxosResponse] (DecodePrepareResponse "data") + then + let: "resp" := DecodePrepareResponse "data" in + "resp" else (if: "kind" = MSG_ACCEPT - then "resp" <-[struct.t PaxosResponse] (DecodeAcceptResponse "data") - else #()));; - ![struct.t PaxosResponse] "resp". + then + let: "resp" := DecodeAcceptResponse "data" in + "resp" + else + struct.mk PaxosResponse [ + ])). Definition Paxos__ResponseSession: val := rec: "Paxos__ResponseSession" "px" "nid" := @@ -602,9 +606,9 @@ Definition PaxosRequest := struct.decl [ ]. Definition DecodePrepareRequest: val := - rec: "DecodePrepareRequest" "data" := - let: ("term", "data") := marshal.ReadInt "data" in - let: ("lsnc", "data") := marshal.ReadInt "data" in + rec: "DecodePrepareRequest" "bs" := + let: ("term", "bs1") := marshal.ReadInt "bs" in + let: ("lsnc", <>) := marshal.ReadInt "bs1" in struct.mk PaxosRequest [ "Kind" ::= MSG_PREPARE; "Term" ::= "term"; @@ -612,11 +616,11 @@ Definition DecodePrepareRequest: val := ]. Definition DecodeAcceptRequest: val := - rec: "DecodeAcceptRequest" "data" := - let: ("term", "data") := marshal.ReadInt "data" in - let: ("lsnc", "data") := marshal.ReadInt "data" in - let: ("lsne", "data") := marshal.ReadInt "data" in - let: ("ents", "data") := util.DecodeStrings "data" in + rec: "DecodeAcceptRequest" "bs" := + let: ("term", "bs1") := marshal.ReadInt "bs" in + let: ("lsnc", "bs2") := marshal.ReadInt "bs1" in + let: ("lsne", "bs3") := marshal.ReadInt "bs2" in + let: ("ents", <>) := util.DecodeStrings "bs3" in struct.mk PaxosRequest [ "Kind" ::= MSG_ACCEPT; "Term" ::= "term"; @@ -626,35 +630,39 @@ Definition DecodeAcceptRequest: val := ]. Definition DecodeRequest: val := - rec: "DecodeRequest" "data" := - let: ("kind", "data") := marshal.ReadInt "data" in - let: "req" := ref (zero_val (struct.t PaxosRequest)) in + rec: "DecodeRequest" "bs" := + let: ("kind", "data") := marshal.ReadInt "bs" in (if: "kind" = MSG_PREPARE - then "req" <-[struct.t PaxosRequest] (DecodePrepareRequest "data") + then + let: "req" := DecodePrepareRequest "data" in + "req" else (if: "kind" = MSG_ACCEPT - then "req" <-[struct.t PaxosRequest] (DecodeAcceptRequest "data") - else #()));; - ![struct.t PaxosRequest] "req". + then + let: "req" := DecodeAcceptRequest "data" in + "req" + else + struct.mk PaxosRequest [ + ])). Definition EncodePrepareResponse: val := rec: "EncodePrepareResponse" "nid" "term" "terma" "ents" := - let: "data" := ref_to (slice.T byteT) (NewSliceWithCap byteT #0 #64) in - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") MSG_PREPARE);; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "nid");; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "term");; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "terma");; - "data" <-[slice.T byteT] (util.EncodeStrings (![slice.T byteT] "data") "ents");; - ![slice.T byteT] "data". + let: "bs" := NewSliceWithCap byteT #0 #64 in + let: "bs1" := marshal.WriteInt "bs" MSG_PREPARE in + let: "bs2" := marshal.WriteInt "bs1" "nid" in + let: "bs3" := marshal.WriteInt "bs2" "term" in + let: "bs4" := marshal.WriteInt "bs3" "terma" in + let: "data" := util.EncodeStrings "bs4" "ents" in + "data". Definition EncodeAcceptResponse: val := rec: "EncodeAcceptResponse" "nid" "term" "lsn" := - let: "data" := ref_to (slice.T byteT) (NewSliceWithCap byteT #0 #32) in - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") MSG_ACCEPT);; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "nid");; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "term");; - "data" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "data") "lsn");; - ![slice.T byteT] "data". + let: "bs" := NewSliceWithCap byteT #0 #32 in + let: "bs1" := marshal.WriteInt "bs" MSG_ACCEPT in + let: "bs2" := marshal.WriteInt "bs1" "nid" in + let: "bs3" := marshal.WriteInt "bs2" "term" in + let: "data" := marshal.WriteInt "bs3" "lsn" in + "data". Definition Paxos__RequestSession: val := rec: "Paxos__RequestSession" "px" "conn" := diff --git a/src/program_proof/tulip/paxos/base.v b/src/program_proof/tulip/paxos/base.v index e10cb5093..9ff973543 100644 --- a/src/program_proof/tulip/paxos/base.v +++ b/src/program_proof/tulip/paxos/base.v @@ -329,44 +329,6 @@ Section def. End def. -Section msg. - - Inductive pxreq := - | RequestVoteReq (term : u64) (lsnlc : u64) - | AppendEntriesReq (term : u64) (lsnlc : u64) (lsne : u64) (ents : list string). - - #[global] - Instance pxreq_eq_decision : - EqDecision pxreq. - Proof. solve_decision. Qed. - - #[global] - Instance pxreq_countable : - Countable pxreq. - Admitted. - - Definition encode_pxreq (req : pxreq) : list u8. - Admitted. - - Inductive pxresp := - | RequestVoteResp (nid term terme : u64) (ents : list string) - | AppendEntriesResp (nid term lsneq : u64). - - #[global] - Instance pxresp_eq_decision : - EqDecision pxresp. - Proof. solve_decision. Qed. - - #[global] - Instance pxresp_countable : - Countable pxresp. - Admitted. - - Definition encode_pxresp (resp : pxresp) : list u8. - Admitted. - -End msg. - Definition max_nodes : Z := 16. Definition is_term_of_node (x : u64) (t : nat) := diff --git a/src/program_proof/tulip/paxos/inv.v b/src/program_proof/tulip/paxos/inv.v index cdc122936..1bfeec42c 100644 --- a/src/program_proof/tulip/paxos/inv.v +++ b/src/program_proof/tulip/paxos/inv.v @@ -1,7 +1,7 @@ From Perennial.program_proof Require Import grove_prelude. From Perennial.program_proof.rsm Require Import big_sep. From Perennial.program_proof.rsm.pure Require Import quorum list extend. -From Perennial.program_proof.tulip.paxos Require Import base consistency res recovery. +From Perennial.program_proof.tulip.paxos Require Import base consistency msg res recovery. Section inv. Context `{!heapGS Σ, !paxos_ghostG Σ}. diff --git a/src/program_proof/tulip/paxos/msg.v b/src/program_proof/tulip/paxos/msg.v new file mode 100644 index 000000000..2c455785d --- /dev/null +++ b/src/program_proof/tulip/paxos/msg.v @@ -0,0 +1,75 @@ +From Perennial.program_proof Require Import grove_prelude. +From Perennial.program_proof.tulip Require Import encode. + + +Inductive pxreq := +| RequestVoteReq (term : u64) (lsnlc : u64) +| AppendEntriesReq (term : u64) (lsnlc : u64) (lsne : u64) (ents : list string). + +#[global] +Instance pxreq_eq_decision : + EqDecision pxreq. +Proof. solve_decision. Qed. + +#[global] +Instance pxreq_countable : + Countable pxreq. +Admitted. + +Definition encode_request_vote_req_xkind (term lsnlc : u64) := + u64_le term ++ u64_le lsnlc. + +Definition encode_request_vote_req (term lsnlc : u64) := + u64_le (U64 0) ++ encode_request_vote_req_xkind term lsnlc. + +Definition encode_append_entries_req_xkind + (term lsnlc lsne : u64) (ents : list string) := + u64_le term ++ u64_le lsnlc ++ u64_le lsne ++ encode_strings ents. + +Definition encode_append_entries_req + (term lsnlc lsne : u64) (ents : list string) := + u64_le (U64 1) ++ encode_append_entries_req_xkind term lsnlc lsne ents. + +Definition encode_pxreq (req : pxreq) : list u8 := + match req with + | RequestVoteReq term lsnlc => + encode_request_vote_req term lsnlc + | AppendEntriesReq term lsnlc lsne ents => + encode_append_entries_req term lsnlc lsne ents + end. + +Inductive pxresp := +| RequestVoteResp (nid term terme : u64) (ents : list string) +| AppendEntriesResp (nid term lsneq : u64). + +#[global] +Instance pxresp_eq_decision : + EqDecision pxresp. +Proof. solve_decision. Qed. + +#[global] +Instance pxresp_countable : + Countable pxresp. +Admitted. + +Definition encode_request_vote_resp_xkind + (nid term terme : u64) (ents : list string) := + u64_le nid ++ u64_le term ++ u64_le terme ++ encode_strings ents. + +Definition encode_request_vote_resp + (nid term terme : u64) (ents : list string) := + u64_le (U64 0) ++ encode_request_vote_resp_xkind nid term terme ents. + +Definition encode_append_entries_resp_xkind (nid term lsneq : u64) := + u64_le nid ++ u64_le term ++ u64_le lsneq. + +Definition encode_append_entries_resp (nid term lsneq : u64) := + u64_le (U64 1) ++ encode_append_entries_resp_xkind nid term lsneq. + +Definition encode_pxresp (resp : pxresp) : list u8 := + match resp with + | RequestVoteResp nid term terme ents => + encode_request_vote_resp nid term terme ents + | AppendEntriesResp nid term lsneq => + encode_append_entries_resp nid term lsneq + end. diff --git a/src/program_proof/tulip/paxos/prelude.v b/src/program_proof/tulip/paxos/prelude.v index ca0befb65..7fabddf1e 100644 --- a/src/program_proof/tulip/paxos/prelude.v +++ b/src/program_proof/tulip/paxos/prelude.v @@ -4,4 +4,4 @@ From Perennial.program_proof.rsm Require Export big_sep. From Perennial.program_proof.rsm.pure Require Export extend fin_maps fin_sets list misc nat sets word quorum. From Perennial.program_proof.tulip.paxos Require Export - base consistency inv res recovery. + base consistency msg inv res recovery. diff --git a/src/program_proof/tulip/paxos/program/decode_request.v b/src/program_proof/tulip/paxos/program/decode_request.v index dae3fca49..aee0a0db6 100644 --- a/src/program_proof/tulip/paxos/program/decode_request.v +++ b/src/program_proof/tulip/paxos/program/decode_request.v @@ -1,4 +1,7 @@ +From Perennial.program_proof Require Import marshal_stateless_proof. +From Perennial.program_proof.tulip Require Import encode. From Perennial.program_proof.tulip.paxos Require Import prelude. +From Perennial.program_proof.tulip.program.util Require Import decode_strings. From Goose.github_com.mit_pdos.tulip Require Import paxos. Definition pxreq_to_val (req : pxreq) (entsP : Slice.t) : val := @@ -17,9 +20,74 @@ Definition pxreq_to_val (req : pxreq) (entsP : Slice.t) : val := Section decode_request. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Theorem wp_DecodeRequest (dataP : Slice.t) (data : list u8) (req : pxreq) : - data = encode_pxreq req -> - {{{ own_slice dataP byteT (DfracOwn 1) data }}} + Theorem wp_DecodePrepareRequest (bsP : Slice.t) term lsnlc : + let bs := encode_request_vote_req_xkind term lsnlc in + {{{ own_slice_small bsP byteT (DfracOwn 1) bs }}} + DecodePrepareRequest (to_val bsP) + {{{ RET (pxreq_to_val (RequestVoteReq term lsnlc) Slice.nil); True }}}. + Proof. + iIntros (bs Φ) "Hbs HΦ". + wp_rec. + + (*@ func DecodePrepareRequest(bs []byte) PaxosRequest { @*) + (*@ term, bs1 := marshal.ReadInt(bs) @*) + (*@ lsnc, _ := marshal.ReadInt(bs1) @*) + (*@ @*) + (*@ return PaxosRequest{ @*) + (*@ Kind : MSG_PREPARE, @*) + (*@ Term : term, @*) + (*@ CommittedLSN : lsnc, @*) + (*@ } @*) + (*@ } @*) + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p2) "Hbs". + wp_pures. + by iApply "HΦ". + Qed. + + Theorem wp_DecodeAcceptRequest (bsP : Slice.t) term lsnc lsne ents : + let bs := encode_append_entries_req_xkind term lsnc lsne ents in + {{{ own_slice_small bsP byteT (DfracOwn 1) bs }}} + DecodeAcceptRequest (to_val bsP) + {{{ (entsP : Slice.t), RET (pxreq_to_val (AppendEntriesReq term lsnc lsne ents) entsP); + own_slice entsP stringT (DfracOwn 1) ents + }}}. + Proof. + iIntros (Henc Φ) "Hbs HΦ". + wp_rec. + + (*@ func DecodeAcceptRequest(bs []byte) PaxosRequest { @*) + (*@ term, bs1 := marshal.ReadInt(bs) @*) + (*@ lsnc, bs2 := marshal.ReadInt(bs1) @*) + (*@ lsne, bs3 := marshal.ReadInt(bs2) @*) + (*@ ents, _ := util.DecodeStrings(bs3) @*) + (*@ @*) + (*@ return PaxosRequest{ @*) + (*@ Kind : MSG_ACCEPT, @*) + (*@ Term : term, @*) + (*@ CommittedLSN : lsnc, @*) + (*@ EntriesLSN : lsne, @*) + (*@ Entries : ents, @*) + (*@ } @*) + (*@ } @*) + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p2) "Hbs". + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p3) "Hbs". + rewrite -(app_nil_r (encode_strings ents)). + wp_apply (wp_DecodeStrings with "Hbs"). + iIntros (entsP dataP) "[Hents Hdata]". + wp_pures. + by iApply "HΦ". + Qed. + + Theorem wp_DecodeRequest (dataP : Slice.t) (req : pxreq) : + let data := encode_pxreq req in + {{{ own_slice_small dataP byteT (DfracOwn 1) data }}} DecodeRequest (to_val dataP) {{{ (entsP : Slice.t), RET (pxreq_to_val req entsP); match req with @@ -28,12 +96,41 @@ Section decode_request. end }}}. Proof. - iIntros (Hdataenc Φ) "Hdata HΦ". + iIntros (bs Φ) "Hbs HΦ". wp_rec. - (*@ func DecodeRequest(data []byte) PaxosRequest { @*) + (*@ func DecodeRequest(bs []byte) PaxosRequest { @*) + (*@ kind, data := marshal.ReadInt(bs) @*) + (*@ @*) + (*@ if kind == MSG_PREPARE { @*) + (*@ req := DecodePrepareRequest(data) @*) + (*@ return req @*) + (*@ } @*) + (*@ if kind == MSG_ACCEPT { @*) + (*@ req := DecodeAcceptRequest(data) @*) + (*@ return req @*) + (*@ } @*) + (*@ @*) + destruct req; wp_pures. + { wp_apply (wp_ReadInt with "Hbs"). + iIntros (p) "Hbs". + wp_pures. + wp_apply (wp_DecodePrepareRequest with "Hbs"). + wp_pures. + (* TODO: figure why need this application here while not required in [gcoord/decode.v]. *) + by iApply ("HΦ" $! Slice.nil). + } + { wp_apply (wp_ReadInt with "Hbs"). + iIntros (p) "Hbs". + wp_pures. + wp_apply (wp_DecodeAcceptRequest with "Hbs"). + iIntros (entsP) "Hents". + wp_pures. + by iApply "HΦ". + } + (*@ return PaxosRequest{} @*) (*@ } @*) - Admitted. + Qed. End decode_request. diff --git a/src/program_proof/tulip/paxos/program/decode_response.v b/src/program_proof/tulip/paxos/program/decode_response.v index c230cfa16..37e376a41 100644 --- a/src/program_proof/tulip/paxos/program/decode_response.v +++ b/src/program_proof/tulip/paxos/program/decode_response.v @@ -1,4 +1,7 @@ +From Perennial.program_proof Require Import marshal_stateless_proof. +From Perennial.program_proof.tulip Require Import encode. From Perennial.program_proof.tulip.paxos Require Import prelude. +From Perennial.program_proof.tulip.program.util Require Import decode_strings. From Goose.github_com.mit_pdos.tulip Require Import paxos. Definition pxresp_to_val (resp : pxresp) (entsP : Slice.t) : val := @@ -18,10 +21,78 @@ Definition pxresp_to_val (resp : pxresp) (entsP : Slice.t) : val := Section decode_response. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Theorem wp_DecodeResponse (dataP : Slice.t) (data : list u8) (resp : pxresp) : - data = encode_pxresp resp -> - (* FIXME: this should take ownership of data. *) - {{{ True }}} + Theorem wp_DecodePrepareResponse (bsP : Slice.t) nid term terme ents : + let bs := encode_request_vote_resp_xkind nid term terme ents in + {{{ own_slice_small bsP byteT (DfracOwn 1) bs }}} + DecodePrepareResponse (to_val bsP) + {{{ (entsP : Slice.t), RET (pxresp_to_val (RequestVoteResp nid term terme ents) entsP); + own_slice entsP stringT (DfracOwn 1) ents + }}}. + Proof. + iIntros (bs Φ) "Hbs HΦ". + wp_rec. + + (*@ func DecodePrepareResponse(bs []byte) PaxosResponse { @*) + (*@ nid, bs1 := marshal.ReadInt(bs) @*) + (*@ term, bs2 := marshal.ReadInt(bs1) @*) + (*@ terma, bs3 := marshal.ReadInt(bs2) @*) + (*@ ents, _ := util.DecodeStrings(bs3) @*) + (*@ @*) + (*@ return PaxosResponse{ @*) + (*@ Kind : MSG_PREPARE, @*) + (*@ NodeID : nid, @*) + (*@ Term : term, @*) + (*@ EntriesTerm : terma, @*) + (*@ Entries : ents, @*) + (*@ } @*) + (*@ } @*) + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p2) "Hbs". + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p3) "Hbs". + rewrite -(app_nil_r (encode_strings ents)). + wp_apply (wp_DecodeStrings with "Hbs"). + iIntros (entsP dataP) "[Hents Hdata]". + wp_pures. + by iApply "HΦ". + Qed. + + Theorem wp_DecodeAcceptResponse (bsP : Slice.t) nid term lsneq : + let bs := encode_append_entries_resp_xkind nid term lsneq in + {{{ own_slice_small bsP byteT (DfracOwn 1) bs }}} + DecodeAcceptResponse (to_val bsP) + {{{ RET (pxresp_to_val (AppendEntriesResp nid term lsneq) Slice.nil); True }}}. + Proof. + iIntros (bs Φ) "Hbs HΦ". + wp_rec. + + (*@ func DecodeAcceptResponse(bs []byte) PaxosResponse { @*) + (*@ nid, bs1 := marshal.ReadInt(bs) @*) + (*@ term, bs2 := marshal.ReadInt(bs1) @*) + (*@ lsn, _ := marshal.ReadInt(bs2) @*) + (*@ @*) + (*@ return PaxosResponse{ @*) + (*@ Kind : MSG_ACCEPT, @*) + (*@ NodeID : nid, @*) + (*@ Term : term, @*) + (*@ MatchedLSN : lsn, @*) + (*@ } @*) + (*@ } @*) + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p2) "Hbs". + wp_apply (wp_ReadInt with "Hbs"). + iIntros (p3) "Hbs". + wp_pures. + by iApply "HΦ". + Qed. + + Theorem wp_DecodeResponse (dataP : Slice.t) (resp : pxresp) : + let data := encode_pxresp resp in + {{{ own_slice_small dataP byteT (DfracOwn 1) data }}} DecodeResponse (to_val dataP) {{{ (entsP : Slice.t), RET (pxresp_to_val resp entsP); match resp with @@ -30,9 +101,39 @@ Section decode_response. end }}}. Proof. - (*@ func DecodeResponse(data []byte) PaxosResponse { @*) + iIntros (bs Φ) "Hbs HΦ". + wp_rec. + + (*@ func DecodeResponse(bs []byte) PaxosResponse { @*) + (*@ kind, data := marshal.ReadInt(bs) @*) + (*@ @*) + (*@ if kind == MSG_PREPARE { @*) + (*@ resp := DecodePrepareResponse(data) @*) + (*@ return resp @*) + (*@ } @*) + (*@ if kind == MSG_ACCEPT { @*) + (*@ resp := DecodeAcceptResponse(data) @*) + (*@ return resp @*) + (*@ } @*) + (*@ @*) (*@ return PaxosResponse{} @*) (*@ } @*) - Admitted. + destruct resp; wp_pures. + { wp_apply (wp_ReadInt with "Hbs"). + iIntros (p) "Hbs". + wp_pures. + wp_apply (wp_DecodePrepareResponse with "Hbs"). + iIntros (entsP) "Hents". + wp_pures. + by iApply "HΦ". + } + { wp_apply (wp_ReadInt with "Hbs"). + iIntros (p) "Hbs". + wp_pures. + wp_apply (wp_DecodeAcceptResponse with "Hbs"). + wp_pures. + by iApply ("HΦ" $! Slice.nil). + } + Qed. End decode_response. diff --git a/src/program_proof/tulip/paxos/program/encode_accept_request.v b/src/program_proof/tulip/paxos/program/encode_accept_request.v index defe07e72..1fcf76c67 100644 --- a/src/program_proof/tulip/paxos/program/encode_accept_request.v +++ b/src/program_proof/tulip/paxos/program/encode_accept_request.v @@ -1,4 +1,7 @@ +From Perennial.program_proof Require Import marshal_stateless_proof. From Perennial.program_proof.tulip.paxos Require Import prelude. +From Perennial.program_proof.tulip Require Import encode. +From Perennial.program_proof.tulip.program.util Require Import encode_strings. From Goose.github_com.mit_pdos.tulip Require Import paxos. Section encode_accept_request. @@ -13,9 +16,37 @@ Section encode_accept_request. ⌜data = encode_pxreq (AppendEntriesReq term lsnc lsne ents)⌝ }}}. Proof. - (*@ func EncodeAcceptRequest(term uint64, lsnc, lsne uint64, ents []string) []byte { @*) - (*@ return nil @*) + iIntros (Φ) "Hents HΦ". + wp_rec. + + (*@ func EncodeAcceptRequest(term, lsnc, lsne uint64, ents []string) []byte { @*) + (*@ bs := make([]byte, 0, 64) @*) + (*@ @*) + (*@ bs1 := marshal.WriteInt(bs, MSG_ACCEPT) @*) + (*@ bs2 := marshal.WriteInt(bs1, term) @*) + (*@ bs3 := marshal.WriteInt(bs2, lsnc) @*) + (*@ bs4 := marshal.WriteInt(bs3, lsne) @*) + (*@ data := util.EncodeStrings(bs4, ents) @*) + (*@ @*) + (*@ return data @*) (*@ } @*) - Admitted. + wp_apply wp_NewSliceWithCap; first word. + iIntros (p) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p2) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p3) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p4) "Hbs". + iDestruct (own_slice_to_small with "Hents") as "Hents". + wp_apply (wp_EncodeStrings with "[$Hbs $Hents]"). + iIntros (dataP) "[Hdata Hents]". + wp_pures. + rewrite uint_nat_W64_0 replicate_0 app_nil_l -!app_assoc. + iApply "HΦ". + by iFrame. + Qed. End encode_accept_request. diff --git a/src/program_proof/tulip/paxos/program/encode_accept_response.v b/src/program_proof/tulip/paxos/program/encode_accept_response.v index 2a212d9fc..e2c0dc66d 100644 --- a/src/program_proof/tulip/paxos/program/encode_accept_response.v +++ b/src/program_proof/tulip/paxos/program/encode_accept_response.v @@ -1,4 +1,7 @@ +From Perennial.program_proof Require Import marshal_stateless_proof. From Perennial.program_proof.tulip.paxos Require Import prelude. +From Perennial.program_proof.tulip Require Import encode. +From Perennial.program_proof.tulip.program.util Require Import encode_strings. From Goose.github_com.mit_pdos.tulip Require Import paxos. Section encode_accept_request. @@ -12,9 +15,33 @@ Section encode_accept_request. ⌜data = encode_pxresp (AppendEntriesResp nid term lsn)⌝ }}}. Proof. - (*@ func EncodeAcceptResponse(nid, term uint64, lsn uint64) []byte { @*) - (*@ return nil @*) + iIntros (Φ) "_ HΦ". + wp_rec. + + (*@ func EncodeAcceptResponse(nid, term, lsn uint64) []byte { @*) + (*@ bs := make([]byte, 0, 32) @*) + (*@ @*) + (*@ bs1 := marshal.WriteInt(bs, MSG_ACCEPT) @*) + (*@ bs2 := marshal.WriteInt(bs1, nid) @*) + (*@ bs3 := marshal.WriteInt(bs2, term) @*) + (*@ data := marshal.WriteInt(bs3, lsn) @*) + (*@ @*) + (*@ return data @*) (*@ } @*) - Admitted. + wp_apply wp_NewSliceWithCap; first word. + iIntros (p) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p2) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p3) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p4) "Hbs". + wp_pures. + rewrite uint_nat_W64_0 replicate_0 app_nil_l -!app_assoc. + iApply "HΦ". + by iFrame. + Qed. End encode_accept_request. diff --git a/src/program_proof/tulip/paxos/program/encode_prepare_request.v b/src/program_proof/tulip/paxos/program/encode_prepare_request.v index 532755711..4e4d1be3b 100644 --- a/src/program_proof/tulip/paxos/program/encode_prepare_request.v +++ b/src/program_proof/tulip/paxos/program/encode_prepare_request.v @@ -1,4 +1,7 @@ +From Perennial.program_proof Require Import marshal_stateless_proof. From Perennial.program_proof.tulip.paxos Require Import prelude. +From Perennial.program_proof.tulip Require Import encode. +From Perennial.program_proof.tulip.program.util Require Import encode_strings. From Goose.github_com.mit_pdos.tulip Require Import paxos. Section encode_prepare_request. @@ -12,9 +15,30 @@ Section encode_prepare_request. ⌜data = encode_pxreq (RequestVoteReq term lsnc)⌝ }}}. Proof. - (*@ func EncodePrepareRequest(term uint64, lsnc uint64) []byte { @*) - (*@ return nil @*) + iIntros (Φ) "_ HΦ". + wp_rec. + + (*@ func EncodePrepareRequest(term, lsnc uint64) []byte { @*) + (*@ bs := make([]byte, 0, 24) @*) + (*@ @*) + (*@ bs1 := marshal.WriteInt(bs, MSG_PREPARE) @*) + (*@ bs2 := marshal.WriteInt(bs1, term) @*) + (*@ data := marshal.WriteInt(bs2, lsnc) @*) + (*@ @*) + (*@ return data @*) (*@ } @*) - Admitted. + wp_apply wp_NewSliceWithCap; first word. + iIntros (p) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p2) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p3) "Hbs". + wp_pures. + rewrite uint_nat_W64_0 replicate_0 app_nil_l -!app_assoc. + iApply "HΦ". + by iFrame. + Qed. End encode_prepare_request. diff --git a/src/program_proof/tulip/paxos/program/encode_prepare_response.v b/src/program_proof/tulip/paxos/program/encode_prepare_response.v index 3ad365a71..ec266cee6 100644 --- a/src/program_proof/tulip/paxos/program/encode_prepare_response.v +++ b/src/program_proof/tulip/paxos/program/encode_prepare_response.v @@ -1,4 +1,7 @@ +From Perennial.program_proof Require Import marshal_stateless_proof. From Perennial.program_proof.tulip.paxos Require Import prelude. +From Perennial.program_proof.tulip Require Import encode. +From Perennial.program_proof.tulip.program.util Require Import encode_strings. From Goose.github_com.mit_pdos.tulip Require Import paxos. Section encode_prepare_response. @@ -17,8 +20,33 @@ Section encode_prepare_response. wp_rec. (*@ func EncodePrepareResponse(nid, term, terma uint64, ents []string) []byte { @*) - (*@ return nil @*) + (*@ bs := make([]byte, 0, 64) @*) + (*@ @*) + (*@ bs1 := marshal.WriteInt(bs, MSG_PREPARE) @*) + (*@ bs2 := marshal.WriteInt(bs1, nid) @*) + (*@ bs3 := marshal.WriteInt(bs2, term) @*) + (*@ bs4 := marshal.WriteInt(bs3, terma) @*) + (*@ data := util.EncodeStrings(bs4, ents) @*) + (*@ @*) + (*@ return data @*) (*@ } @*) - Admitted. + wp_apply wp_NewSliceWithCap; first word. + iIntros (p) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p1) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p2) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p3) "Hbs". + wp_apply (wp_WriteInt with "Hbs"). + iIntros (p4) "Hbs". + iDestruct (own_slice_to_small with "Hents") as "Hents". + wp_apply (wp_EncodeStrings with "[$Hbs $Hents]"). + iIntros (dataP) "[Hdata Hents]". + wp_pures. + rewrite uint_nat_W64_0 replicate_0 app_nil_l -!app_assoc. + iApply "HΦ". + by iFrame. + Qed. End encode_prepare_response. diff --git a/src/program_proof/tulip/paxos/program/paxos_election_session.v b/src/program_proof/tulip/paxos/program/paxos_election_session.v index 98dcfa10f..5ce9da029 100644 --- a/src/program_proof/tulip/paxos/program/paxos_election_session.v +++ b/src/program_proof/tulip/paxos/program/paxos_election_session.v @@ -197,7 +197,7 @@ Section election_session. iFrame "Hlsnprc". } iPureIntro. - rewrite 2!set_map_union_L 2!set_map_singleton_L /= -Hdataenc. + rewrite 2!set_map_union_L 2!set_map_singleton_L. set_solver. } rewrite insert_delete_insert. diff --git a/src/program_proof/tulip/paxos/program/paxos_leader_session.v b/src/program_proof/tulip/paxos/program/paxos_leader_session.v index 67047fc50..2a75f8254 100644 --- a/src/program_proof/tulip/paxos/program/paxos_leader_session.v +++ b/src/program_proof/tulip/paxos/program/paxos_leader_session.v @@ -131,7 +131,7 @@ Section leader_session. iSplit. { iApply big_sepS_insert_2; [iFrame "# %" | done]. } iPureIntro. - rewrite 2!set_map_union_L 2!set_map_singleton_L /= -Hdataenc. + rewrite 2!set_map_union_L 2!set_map_singleton_L. set_solver. } rewrite insert_delete_insert. diff --git a/src/program_proof/tulip/paxos/program/paxos_request_session.v b/src/program_proof/tulip/paxos/program/paxos_request_session.v index 8987a86e8..354982ea8 100644 --- a/src/program_proof/tulip/paxos/program/paxos_request_session.v +++ b/src/program_proof/tulip/paxos/program/paxos_request_session.v @@ -62,8 +62,9 @@ Section request_session. (*@ req := message.DecodePaxosRequest(ret.Data) @*) (*@ kind := req.Kind @*) (*@ @*) + iDestruct (own_slice_to_small with "Hretdata") as "Hretdata". + rewrite Hreq. wp_apply (wp_DecodeRequest with "Hretdata"). - { apply Hreq. } iIntros (entsaP) "Hentsa". destruct req as [term lsnc |]; wp_pures. { (* Case: RequestVote. *) @@ -185,6 +186,7 @@ Section request_session. { iApply big_sepS_insert_2; [iFrame "# %" | done]. } iPureIntro. clear -Henc Hdata. + rewrite 2!set_map_union_L 2!set_map_singleton. set_solver. } iCombine "Hconn Hconnects" as "Hconnects". @@ -307,6 +309,7 @@ Section request_session. { iApply big_sepS_insert_2; [iFrame "# %" | done]. } iPureIntro. clear -Henc Hdata. + rewrite 2!set_map_union_L 2!set_map_singleton. set_solver. } iCombine "Hconn Hconnects" as "Hconnects". diff --git a/src/program_proof/tulip/paxos/program/paxos_response_session.v b/src/program_proof/tulip/paxos/program/paxos_response_session.v index c4d9cea70..b304046b3 100644 --- a/src/program_proof/tulip/paxos/program/paxos_response_session.v +++ b/src/program_proof/tulip/paxos/program/paxos_response_session.v @@ -50,8 +50,9 @@ Section response_sesion. (*@ resp := message.DecodePaxosResponse(data) @*) (*@ kind := resp.Kind @*) (*@ @*) - wp_apply wp_DecodeResponse. - { apply Hdataenc. } + iDestruct (own_slice_to_small with "Hdata") as "Hdata". + rewrite Hdataenc. + wp_apply (wp_DecodeResponse with "Hdata"). iIntros (entsP) "Hents". destruct resp as [nid' term terme ents | nid' term lsneq]; wp_pures. { (* Case: RequestVote. *)