Refactor and rename form_matched_resp_msg (#289)

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Sep 20, 2023 · 77b9e7f · 77b9e7f
1 parent adcedd4
commit 77b9e7f
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 10 deletions.
diff --git a/src/kubernetes_cluster/proof/controller_runtime_safety.rs b/src/kubernetes_cluster/proof/controller_runtime_safety.rs
@@ -362,7 +362,7 @@ pub proof fn lemma_always_pending_req_in_flight_or_resp_in_flight_at_reconcile_s
                 }
                 Step::KubernetesBusy(input) => {
                     if input == Some(s.ongoing_reconciles()[key].pending_req_msg.get_Some_0()) {
-                        let resp_msg = Message::form_matched_resp_msg(s.ongoing_reconciles()[key].pending_req_msg.get_Some_0(), Err(APIError::ServerTimeout));
+                        let resp_msg = Message::form_matched_err_resp_msg(s.ongoing_reconciles()[key].pending_req_msg.get_Some_0(), APIError::ServerTimeout);
                         assert(s_prime.in_flight().contains(resp_msg));
                     } else {
                         if !s.in_flight().contains(s.ongoing_reconciles()[key].pending_req_msg.get_Some_0()) {

diff --git a/src/kubernetes_cluster/proof/kubernetes_api_liveness.rs b/src/kubernetes_cluster/proof/kubernetes_api_liveness.rs
@@ -120,7 +120,7 @@ pub proof fn lemma_get_req_leads_to_some_resp
             },
             Step::KubernetesBusy(input) => {
                 if input.get_Some_0() == msg {
-                    let resp = Message::form_matched_resp_msg(msg, Err(APIError::ServerTimeout));
+                    let resp = Message::form_matched_err_resp_msg(msg, APIError::ServerTimeout);
                     assert(s_prime.in_flight().contains(resp));
                     assert(Message::resp_msg_matches_req_msg(resp, msg));
                     assert(post(s_prime));

diff --git a/src/kubernetes_cluster/spec/cluster_state_machine.rs b/src/kubernetes_cluster/spec/cluster_state_machine.rs
@@ -273,7 +273,7 @@ pub open spec fn disable_crash() -> Action<Self, (), ()> {
 pub open spec fn busy_kubernetes_api_rejects_request() -> Action<Self, Option<MsgType<E>>, ()> {
     let network_result = |input: Option<MsgType<E>>, s: Self| {
         let req_msg = input.get_Some_0();
-        let resp = Message::form_matched_resp_msg(req_msg, Err(APIError::ServerTimeout));
+        let resp = Message::form_matched_err_resp_msg(req_msg, APIError::ServerTimeout);
         let msg_ops = MessageOps {
             recv: input,
             send: Multiset::singleton(resp),

diff --git a/src/kubernetes_cluster/spec/message.rs b/src/kubernetes_cluster/spec/message.rs
@@ -252,16 +252,15 @@ pub open spec fn resp_msg_matches_req_msg(resp_msg: Message<I, O>, req_msg: Mess
     }
 }
 
-// TODO: handle list request
-pub open spec fn form_matched_resp_msg(req_msg: Message<I, O>, result: Result<DynamicObjectView, APIError>) -> Message<I, O>
+pub open spec fn form_matched_err_resp_msg(req_msg: Message<I, O>, err: APIError) -> Message<I, O>
     recommends req_msg.content.is_APIRequest(),
 {
     match req_msg.content.get_APIRequest_0() {
-        APIRequest::GetRequest(_) => Self::form_get_resp_msg(req_msg, result),
-        APIRequest::ListRequest(_) => Self::form_list_resp_msg(req_msg, Err(APIError::Invalid)),
-        APIRequest::CreateRequest(_) => Self::form_create_resp_msg(req_msg, result),
-        APIRequest::DeleteRequest(_) => Self::form_delete_resp_msg(req_msg, result),
-        APIRequest::UpdateRequest(_) => Self::form_update_resp_msg(req_msg, result),
+        APIRequest::GetRequest(_) => Self::form_get_resp_msg(req_msg, Err(err)),
+        APIRequest::ListRequest(_) => Self::form_list_resp_msg(req_msg, Err(err)),
+        APIRequest::CreateRequest(_) => Self::form_create_resp_msg(req_msg, Err(err)),
+        APIRequest::DeleteRequest(_) => Self::form_delete_resp_msg(req_msg, Err(err)),
+        APIRequest::UpdateRequest(_) => Self::form_update_resp_msg(req_msg, Err(err)),
     }
 }