Replace req/resp_id with rest_id

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Aug 23, 2023 · 2f87796 · 2f87796
1 parent f35cf64
commit 2f87796
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 23 deletions.
diff --git a/src/controller_examples/simple_controller/proof/liveness.rs b/src/controller_examples/simple_controller/proof/liveness.rs
@@ -692,7 +692,7 @@ pub proof fn next_and_not_crash_preserves_init_pc_or_reconciler_at_after_get_cr_
         let input = next_step.get_ControllerStep_0();
         let req_msg = controller_req_msg(APIRequest::GetRequest(GetRequest{key: cr.object_ref()}), s.rest_id_allocator.allocate().1);
         assert(is_controller_get_cr_request_msg(req_msg, cr));
-        assert(req_msg.content.get_req_id() == s.rest_id_allocator.rest_id_counter);
+        assert(req_msg.content.get_rest_id() == s.rest_id_allocator.rest_id_counter);
         if (exists |resp_msg: Message<E::Input, E::Output>| {
             &&& #[trigger] s_prime.message_in_flight(resp_msg)
             &&& Message::resp_msg_matches_req_msg(resp_msg, req_msg)

diff --git a/src/kubernetes_cluster/proof/message.rs b/src/kubernetes_cluster/proof/message.rs
@@ -64,12 +64,12 @@ proof fn next_preserves_every_in_flight_msg_has_lower_id_than_allocator(
                         Step::KubernetesAPIStep(input) => {
                             let req_msg = input.get_Some_0();
                             assert(s.message_in_flight(req_msg));
-                            assert(id == req_msg.content.get_req_id());
+                            assert(id == req_msg.content.get_rest_id());
                         }
                         Step::KubernetesBusy(input) => {
                             let req_msg = input.get_Some_0();
                             assert(s.message_in_flight(req_msg));
-                            assert(id == req_msg.content.get_req_id());
+                            assert(id == req_msg.content.get_rest_id());
                         }
                         _ => assert(false),
                     }
@@ -261,7 +261,7 @@ pub open spec fn pending_req_has_lower_req_id_than_allocator() -> StatePred<Self
         forall |cr_key: ObjectRef|
             #[trigger] s.reconcile_state_contains(cr_key)
             && Self::pending_k8s_api_req_msg(s, cr_key)
-            ==> s.reconcile_state_of(cr_key).pending_req_msg.get_Some_0().content.get_req_id() < s.rest_id_allocator.rest_id_counter
+            ==> s.reconcile_state_of(cr_key).pending_req_msg.get_Some_0().content.get_rest_id() < s.rest_id_allocator.rest_id_counter
     }
 }
 

diff --git a/src/kubernetes_cluster/spec/message.rs b/src/kubernetes_cluster/spec/message.rs
@@ -139,13 +139,6 @@ impl<I, O> MessageContent<I, O> {
         self.get_APIRequest_0().get_UpdateRequest_0()
     }
 
-    pub open spec fn get_req_id(self) -> RestId
-        recommends
-            self.is_APIRequest()
-    {
-        self.get_APIRequest_1()
-    }
-
     pub open spec fn is_get_response(self) -> bool {
         &&& self.is_APIResponse()
         &&& self.get_APIResponse_0().is_GetResponse()
@@ -194,13 +187,6 @@ impl<I, O> MessageContent<I, O> {
         self.get_APIResponse_0().get_ListResponse_0()
     }
 
-    pub open spec fn get_resp_id(self) -> RestId
-        recommends
-            self.is_APIResponse()
-    {
-        self.get_APIResponse_1()
-    }
-
     pub open spec fn get_rest_id(self) -> RestId
     {
         match self {
@@ -288,31 +274,31 @@ pub open spec fn form_msg(src: HostId, dst: HostId, msg_content: MessageContent<
 pub open spec fn form_get_resp_msg(req_msg: Message<I, O>, result: Result<DynamicObjectView, APIError>) -> Message<I, O>
     recommends req_msg.content.is_get_request(),
 {
-    Self::form_msg(req_msg.dst, req_msg.src, Self::get_resp_msg_content(result, req_msg.content.get_req_id()))
+    Self::form_msg(req_msg.dst, req_msg.src, Self::get_resp_msg_content(result, req_msg.content.get_rest_id()))
 }
 
 pub open spec fn form_list_resp_msg(req_msg: Message<I, O>, result: Result<Seq<DynamicObjectView>, APIError>) -> Message<I, O>
     recommends req_msg.content.is_list_request(),
 {
-    Self::form_msg(req_msg.dst, req_msg.src, Self::list_resp_msg_content(result, req_msg.content.get_req_id()))
+    Self::form_msg(req_msg.dst, req_msg.src, Self::list_resp_msg_content(result, req_msg.content.get_rest_id()))
 }
 
 pub open spec fn form_create_resp_msg(req_msg: Message<I, O>, result: Result<DynamicObjectView, APIError>) -> Message<I, O>
     recommends req_msg.content.is_create_request(),
 {
-    Self::form_msg(req_msg.dst, req_msg.src, Self::create_resp_msg_content(result, req_msg.content.get_req_id()))
+    Self::form_msg(req_msg.dst, req_msg.src, Self::create_resp_msg_content(result, req_msg.content.get_rest_id()))
 }
 
 pub open spec fn form_delete_resp_msg(req_msg: Message<I, O>, result: Result<DynamicObjectView, APIError>) -> Message<I, O>
     recommends req_msg.content.is_delete_request(),
 {
-    Self::form_msg(req_msg.dst, req_msg.src, Self::delete_resp_msg_content(result, req_msg.content.get_req_id()))
+    Self::form_msg(req_msg.dst, req_msg.src, Self::delete_resp_msg_content(result, req_msg.content.get_rest_id()))
 }
 
 pub open spec fn form_update_resp_msg(req_msg: Message<I, O>, result: Result<DynamicObjectView, APIError>) -> Message<I, O>
     recommends req_msg.content.is_update_request(),
 {
-    Self::form_msg(req_msg.dst, req_msg.src, Self::update_resp_msg_content(result, req_msg.content.get_req_id()))
+    Self::form_msg(req_msg.dst, req_msg.src, Self::update_resp_msg_content(result, req_msg.content.get_rest_id()))
 }
 
 pub open spec fn form_external_resp_msg(req_msg: Message<I, O>, resp: O) -> Message<I, O>