Reword some comments

Signed-off-by: Wenjie Ma <[email protected]>

src/external_api/exec.rs

@@ -6,10 +6,11 @@ use vstd::{prelude::*, view::*};
 
 verus! {
 
-// A trait for the external library of a reconciler.
-// Its core is a process method, and the developer should wrap all possible operations they may need in the function.
-// Input is the ? of Request<?> of the reconciler, i.e., it completes the request type of a reconciler.
-// Similarly, Output composes the Response<?> type of a reconciler.
+// A trait for the external api of a reconciler, whose core is a transition method, and the developer should wrap all 
+// possible operations they may need in the function.
+// Input is the input type of the external api and also the ? of Request<?> of the reconciler, i.e., it completes the 
+// request type of a reconciler.
+// Similarly, Output is the output type of the external api, which composes the Response<?> type of a reconciler.
 // Note that we can encapsulate all the required libraries here, so each reconciler only has one ExternalAPI type.
 pub trait ExternalAPI<Input: ToView, Output: ToView> {
     fn transition(input: Input) -> Option<Output>;

src/kubernetes_cluster/spec/cluster.rs

@@ -157,7 +157,7 @@ pub open spec fn kubernetes_api_next<K: ResourceView, E: ExternalAPI, R: Reconci
 pub open spec fn external_api_next<K: ResourceView, E: ExternalAPI, R: Reconciler<K, E>>() -> Action<State<K, E, R>, ExternalComm<E::Input, E::Output>, ()> {
     Action {
         precondition: |input: ExternalComm<E::Input, E::Output>, s: State<K, E, R>| {
-            // For the external api action, a valid input must be contained by the in_flight field of the external_api_state.
+            // For the external api action, a valid input must exist in the in_flight set of the external_api_state.
             &&& input.is_Input()
             &&& s.external_api_state.in_flight.contains(input)
         },

src/kubernetes_cluster/spec/controller/controller_runtime.rs

@@ -57,8 +57,8 @@ pub open spec fn continue_reconcile<K: ResourceView, E: ExternalAPI, R: Reconcil
                 &&& !R::reconcile_error(s.ongoing_reconciles[cr_key].local_state)
                 // Split cases:
                 // (1) there is a pending request which is destined for kubernetes api;
-                // (2) there is a pending external api request (so that we should send a message to the external api) and an external api output
-                // (3) there is no pending request;
+                // (2) there is a pending external api input (so that we should feed the input to the external api) and an external api output
+                // (3) there is no pending request or external api input;
                 // The three cases don't overlap each other, and we must make them mutually exclusive in the
                 // precondition, i.e., there should not be a state which satifies the precondition but fits for more
                 // than one case of the three.

src/kubernetes_cluster/spec/external_api.rs

@@ -10,8 +10,12 @@ use vstd::{multiset::*, prelude::*};
 
 verus! {
 
-// This enum is a wrapper for attaching rest id to the input and output of the external api.
-// By doing this, we are able to check whether the output matches the input when conducting continue_reconcile.
+// ExternalComm is used to represent communication between the external api and controller. 
+// It has two variants: Input is computed by controller and sent to and consumed by external api; Output is generated by
+// external api after handling the input. 
+// Each variant also carries a nat which represents the rest_id of the state when the input is generated or the call id of
+// the corresponding input when the output is created.
+// With call id, we are able to check whether the output matches the input when conducting continue_reconcile.
 #[is_variant]
 pub enum ExternalComm<Input, Output> {
     Input(Input, nat),