Prove timeless and countable instances

mit-pdos · Dec 4, 2024 · 5cc033a · 5cc033a
1 parent 61eea85
commit 5cc033a
Show file tree

Hide file tree

Showing 5 changed files with 170 additions and 7 deletions.
diff --git a/src/program_proof/tulip/inv.v b/src/program_proof/tulip/inv.v
@@ -64,6 +64,11 @@ Section def.
     Persistent (fast_or_slow_read γ rid key lts ts v slow).
   Proof. rewrite /fast_or_slow_read. apply _. Defined.
 
+  #[global]
+  Instance fast_or_slow_read_timeless γ rid key lts ts v slow :
+    Timeless (fast_or_slow_read γ rid key lts ts v slow).
+  Proof. rewrite /fast_or_slow_read. apply _. Defined.
+
   Definition validate_outcome γ gid rid ts res : iProp Σ :=
     match res with
     | ReplicaOK => is_replica_validated_ts γ gid rid ts
@@ -80,6 +85,11 @@ Section def.
     Persistent (validate_outcome γ gid rid ts res).
   Proof. destruct res; apply _. Defined.
 
+  #[global]
+  Instance validate_outcome_timeless γ gid rid ts res :
+    Timeless (validate_outcome γ gid rid ts res).
+  Proof. destruct res; apply _. Defined.
+
   Definition fast_prepare_outcome γ gid rid ts res : iProp Σ :=
     match res with
     | ReplicaOK => is_replica_validated_ts γ gid rid ts ∗
@@ -97,6 +107,11 @@ Section def.
     Persistent (fast_prepare_outcome γ gid rid ts res).
   Proof. destruct res; apply _. Defined.
 
+  #[global]
+  Instance fast_prepare_outcome_timeless γ gid rid ts res :
+    Timeless (fast_prepare_outcome γ gid rid ts res).
+  Proof. destruct res; apply _. Defined.
+
   Definition accept_outcome γ gid rid ts rank pdec res : iProp Σ :=
     match res with
     | ReplicaOK => is_replica_pdec_at_rank γ gid rid ts rank pdec
@@ -113,6 +128,11 @@ Section def.
     Persistent (accept_outcome γ gid rid ts rank pdec res).
   Proof. destruct res; apply _. Defined.
 
+  #[global]
+  Instance accept_outcome_timeless γ gid rid ts rank pdec res :
+    Timeless (accept_outcome γ gid rid ts rank pdec res).
+  Proof. destruct res; apply _. Defined.
+
   Definition query_outcome γ ts res : iProp Σ :=
     match res with
     | ReplicaOK => True
@@ -129,6 +149,11 @@ Section def.
     Persistent (query_outcome γ ts res).
   Proof. destruct res; apply _. Defined.
 
+  #[global]
+  Instance query_outcome_timeless γ ts res :
+    Timeless (query_outcome γ ts res).
+  Proof. destruct res; apply _. Defined.
+
 End def.
 
 Section inv_network.
@@ -162,6 +187,11 @@ Section inv_network.
     Persistent (safe_txnreq γ gid req).
   Proof. destruct req; apply _. Defined.
 
+  #[global]
+  Instance safe_txnreq_timeless γ gid req :
+    Timeless (safe_txnreq γ gid req).
+  Proof. destruct req; apply _. Defined.
+
   Definition safe_read_resp
     γ (ts rid : u64) (key : string) (ver : dbpver) (slow : bool) : iProp Σ :=
     "#Hsafe" ∷ fast_or_slow_read γ rid key (uint.nat ver.1) (uint.nat ts) ver.2 slow ∗
@@ -209,6 +239,11 @@ Section inv_network.
     Persistent (safe_txnresp γ gid resp).
   Proof. destruct resp; apply _. Defined.
 
+  #[global]
+  Instance safe_txnresp_timeless γ gid resp :
+    Timeless (safe_txnresp γ gid resp).
+  Proof. destruct resp; apply _. Defined.
+
   Definition listen_inv
     (addr : chan) (ms : gset message) gid γ : iProp Σ :=
     ∃ (reqs : gset txnreq),
@@ -236,7 +271,7 @@ Section inv_network.
   #[global]
   Instance tulip_network_inv_timeless γ gid addrm :
     Timeless (tulip_network_inv γ gid addrm).
-  Admitted.
+  Proof. apply _. Defined.
 
   Definition know_tulip_network_inv γ gid addrm : iProp Σ :=
     inv tulipnetNS (tulip_network_inv γ gid addrm).

diff --git a/src/program_proof/tulip/inv_txnlog.v b/src/program_proof/tulip/inv_txnlog.v
@@ -36,7 +36,7 @@ Section inv_txnlog.
   #[global]
   Instance tulip_txnlog_inv_timeless γ π gid :
     Timeless (tulip_txnlog_inv γ π gid).
-  Admitted.
+  Proof. apply _. Defined.
 
   Definition know_tulip_txnlog_inv γ π gid : iProp Σ :=
     inv txnlogNS (tulip_txnlog_inv γ π gid).

diff --git a/src/program_proof/tulip/msg.v b/src/program_proof/tulip/msg.v
@@ -20,7 +20,42 @@ Proof. solve_decision. Qed.
 #[global]
 Instance txnreq_countable :
   Countable txnreq.
-Admitted.
+Proof.
+  refine (inj_countable'
+            (λ x, match x with
+                  | ReadReq ts key => inl (ts, key)
+                  | FastPrepareReq ts pwrs => inr (inl (ts, pwrs))
+                  | ValidateReq ts rank pwrs => inr (inr (inl (ts, rank, pwrs)))
+                  | PrepareReq ts rank => inr (inr (inr (inl (ts, rank))))
+                  | UnprepareReq ts rank =>
+                      inr (inr (inr (inr (inl (ts, rank)))))
+                  | QueryReq ts rank =>
+                      inr (inr (inr (inr (inr (inl (ts, rank))))))
+                  | RefreshReq ts rank =>
+                      inr (inr (inr (inr (inr (inr (inl (ts, rank)))))))
+                  | CommitReq ts pwrs =>
+                      inr (inr (inr (inr (inr (inr (inr (inl (ts, pwrs))))))))
+                  | AbortReq ts =>
+                      inr (inr (inr (inr (inr (inr (inr (inr ts)))))))
+                  end)
+            (λ x, match x with
+                  | inl (ts, key) => ReadReq ts key
+                  | inr (inl (ts, pwrs)) => FastPrepareReq ts pwrs
+                  | inr (inr (inl (ts, rank, pwrs))) => ValidateReq ts rank pwrs
+                  | inr (inr (inr (inl (ts, rank)))) => PrepareReq ts rank
+                  | inr (inr (inr (inr (inl (ts, rank))))) => UnprepareReq ts rank
+                  | inr (inr (inr (inr (inr (inl (ts, rank)))))) =>
+                      QueryReq ts rank
+                  | inr (inr (inr (inr (inr (inr (inl (ts, rank))))))) =>
+                      RefreshReq ts rank
+                  | inr (inr (inr (inr (inr (inr (inr (inl (ts, pwrs)))))))) =>
+                      CommitReq ts pwrs
+                  | inr (inr (inr (inr (inr (inr (inr (inr ts))))))) =>
+                      AbortReq ts
+                  end)
+            _).
+  intros [| | | | | | | |] => //=.
+Qed.
 
 Definition encode_read_req_xkind (ts : u64) (key : string) :=
   u64_le ts ++ encode_string key.
@@ -83,6 +118,33 @@ Instance rpres_eq_decision :
   EqDecision rpres.
 Proof. solve_decision. Qed.
 
+#[global]
+Instance rpres_countable :
+  Countable rpres.
+Proof.
+  refine (inj_countable'
+            (λ x, match x with
+                  | ReplicaOK => 0
+                  | ReplicaCommittedTxn => 1
+                  | ReplicaAbortedTxn => 2
+                  | ReplicaStaleCoordinator => 3
+                  | ReplicaFailedValidation => 4
+                  | ReplicaInvalidRank => 5
+                  | ReplicaWrongLeader => 6
+                  end)
+            (λ x, match x with
+                  | 0 => _
+                  | 1 => _
+                  | 2 => _
+                  | 3 => _
+                  | 4 => _
+                  | 5 => _
+                  | _ => ReplicaWrongLeader
+                  end)
+            _).
+  intros [| | | | | |] => //=.
+Qed.
+
 Definition rpres_to_u64 (r : rpres) :=
   match r with
   | ReplicaOK => (U64 0)
@@ -117,7 +179,39 @@ Proof. solve_decision. Qed.
 #[global]
 Instance txnresp_countable :
   Countable txnresp.
-Admitted.
+Proof.
+  refine (inj_countable'
+            (λ x, match x with
+                  | ReadResp ts rid key ver slow => inl (ts, rid, key, ver, slow)
+                  | FastPrepareResp ts rid res => inr (inl (ts, rid, res))
+                  | ValidateResp ts rid res => inr (inr (inl (ts, rid, res)))
+                  | PrepareResp ts rank rid res => inr (inr (inr (inl (ts, rank, rid, res))))
+                  | UnprepareResp ts rank rid res =>
+                      inr (inr (inr (inr (inl (ts, rank, rid, res)))))
+                  | QueryResp ts res =>
+                      inr (inr (inr (inr (inr (inl (ts, res))))))
+                  | CommitResp ts res =>
+                      inr (inr (inr (inr (inr (inr (inl (ts, res)))))))
+                  | AbortResp ts res =>
+                      inr (inr (inr (inr (inr (inr (inr (ts, res)))))))
+                  end)
+            (λ x, match x with
+                  | inl (ts, rid, key, ver, slow) => ReadResp ts rid key ver slow
+                  | inr (inl (ts, rid, res)) => FastPrepareResp ts rid res
+                  | inr (inr (inl (ts, rid, res))) => ValidateResp ts rid res
+                  | inr (inr (inr (inl (ts, rank, rid, res)))) => PrepareResp ts rank rid res
+                  | inr (inr (inr (inr (inl (ts, rank, rid, res))))) =>
+                      UnprepareResp ts rank rid res
+                  | inr (inr (inr (inr (inr (inl (ts, res)))))) =>
+                      QueryResp ts res
+                  | inr (inr (inr (inr (inr (inr (inl (ts, res))))))) =>
+                      CommitResp ts res
+                  | inr (inr (inr (inr (inr (inr (inr (ts, res))))))) =>
+                      AbortResp ts res
+                  end)
+            _).
+  intros [| | | | | | |] => //=.
+Qed.
 
 Definition encode_read_resp_xkind
   (ts rid : u64) (key : string) (ver : dbpver) (slow : bool) :=

diff --git a/src/program_proof/tulip/paxos/inv.v b/src/program_proof/tulip/paxos/inv.v
@@ -569,6 +569,11 @@ Section inv_network.
     Persistent (safe_pxreq γ nids req).
   Proof. destruct req; apply _. Defined.
 
+  #[global]
+  Instance safe_pxreq_timeless γ nids req :
+    Timeless (safe_pxreq γ nids req).
+  Proof. destruct req; apply _. Defined.
+
   Definition safe_request_vote_resp
     γ (nids : gset u64) (nid term terme : u64) (ents : list string) : iProp Σ :=
     ∃ (logpeer : list string) (lsne : u64),
@@ -598,6 +603,11 @@ Section inv_network.
     Persistent (safe_pxresp γ nids resp).
   Proof. destruct resp; apply _. Defined.
 
+  #[global]
+  Instance safe_pxresp_timeless γ nids resp :
+    Timeless (safe_pxresp γ nids resp).
+  Proof. destruct resp; apply _. Defined.
+
   Definition listen_inv
     (addr : chan) (ms : gset message) nids γ : iProp Σ :=
     ∃ (reqs : gset pxreq),
@@ -624,7 +634,7 @@ Section inv_network.
   #[global]
   Instance paxos_network_inv_timeless γ addrm :
     Timeless (paxos_network_inv γ addrm).
-  Admitted.
+  Proof. apply _. Defined.
 
   Definition know_paxos_network_inv γ addrm : iProp Σ :=
     inv paxosnetNS (paxos_network_inv γ addrm).

diff --git a/src/program_proof/tulip/paxos/msg.v b/src/program_proof/tulip/paxos/msg.v
@@ -14,7 +14,19 @@ Proof. solve_decision. Qed.
 #[global]
 Instance pxreq_countable :
   Countable pxreq.
-Admitted.
+Proof.
+  refine (inj_countable'
+            (λ x, match x with
+                  | RequestVoteReq term lsnlc => inl (term, lsnlc)
+                  | AppendEntriesReq term lsnlc lsne ents => inr (term, lsnlc, lsne, ents)
+                  end)
+            (λ x, match x with
+                  | inl (term, lsnlc) => RequestVoteReq term lsnlc
+                  | inr (term, lsnlc, lsne, ents) => AppendEntriesReq term lsnlc lsne ents
+                  end)
+            _).
+  intros [|] => //=.
+Qed.
 
 Definition encode_request_vote_req_xkind (term lsnlc : u64) :=
   u64_le term ++ u64_le lsnlc.
@@ -50,7 +62,19 @@ Proof. solve_decision. Qed.
 #[global]
 Instance pxresp_countable :
   Countable pxresp.
-Admitted.
+Proof.
+  refine (inj_countable'
+            (λ x, match x with
+                  | RequestVoteResp nid term terme ents => inl (nid, term, terme, ents)
+                  | AppendEntriesResp nid term lsneq => inr (nid, term, lsneq)
+                  end)
+            (λ x, match x with
+                  | inl (nid, term, terme, ents) => RequestVoteResp nid term terme ents
+                  | inr (nid, term, lsneq) => AppendEntriesResp nid term lsneq
+                  end)
+            _).
+  intros [|] => //=.
+Qed.
 
 Definition encode_request_vote_resp_xkind
   (nid term terme : u64) (ents : list string) :=