From 6befb118850061cdb404865a49336dd0d7b63de0 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Wed, 20 Sep 2023 15:31:53 -0500 Subject: [PATCH] Refactor and rename form_matched_resp_msg Signed-off-by: Xudong Sun --- .../proof/controller_runtime_safety.rs | 2 +- .../proof/kubernetes_api_liveness.rs | 2 +- .../spec/cluster_state_machine.rs | 2 +- src/kubernetes_cluster/spec/message.rs | 13 ++++++------- 4 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/kubernetes_cluster/proof/controller_runtime_safety.rs b/src/kubernetes_cluster/proof/controller_runtime_safety.rs index b217e039d..3b4e9506c 100644 --- 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 index 3c86ba435..b2e11fe7c 100644 --- 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 index eb044a9ce..bfb6cf5bc 100644 --- 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 { pub open spec fn busy_kubernetes_api_rejects_request() -> Action>, ()> { let network_result = |input: Option>, 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 index 14ba967b4..b1d3b8d56 100644 --- 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, req_msg: Mess } } -// TODO: handle list request -pub open spec fn form_matched_resp_msg(req_msg: Message, result: Result) -> Message +pub open spec fn form_matched_err_resp_msg(req_msg: Message, err: APIError) -> Message 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)), } }