Use regular comment style (#550)

We are not using the comments as doc yet.

---------

Signed-off-by: Xudong Sun <[email protected]>

src/controller_examples/composition_example/consumer_controller/trusted/exec_types.rs

@@ -12,7 +12,7 @@ use vstd::prelude::*;
 
 verus! {
 
-/// ConsumerReconcileState describes the local state with which the reconcile functions makes decisions.
+// ConsumerReconcileState describes the local state with which the reconcile functions makes decisions.
 pub struct ConsumerReconcileState {
     pub reconcile_step: ConsumerReconcileStep,
 }

src/controller_examples/composition_example/producer_controller/trusted/exec_types.rs

@@ -12,7 +12,7 @@ use vstd::prelude::*;
 
 verus! {
 
-/// ProducerReconcileState describes the local state with which the reconcile functions makes decisions.
+// ProducerReconcileState describes the local state with which the reconcile functions makes decisions.
 pub struct ProducerReconcileState {
     pub reconcile_step: ProducerReconcileStep,
 }

src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/owner_ref.rs

@@ -27,8 +27,8 @@ use vstd::prelude::*;
 
 verus! {
 
-/// Valid owner_references field satisfies that every owner reference in it valid uid, i.e., it points to some existing objects.
-/// We don't test custom resource object here because we don't care about whether it's owner_references is valid.
+// Valid owner_references field satisfies that every owner reference in it valid uid, i.e., it points to some existing objects.
+// We don't test custom resource object here because we don't care about whether it's owner_references is valid.
 pub open spec fn owner_references_is_valid(obj: DynamicObjectView, s: FBCluster) -> bool {
     let owner_refs = obj.metadata.owner_references.get_Some_0();
 

src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/predicate.rs

@@ -111,12 +111,12 @@ pub open spec fn resource_create_response_msg(key: ObjectRef, s: FBCluster) -> s
         )
 }
 
-/// This spec tells that when the reconciler is at AfterGetDaemonSet, and there is a matched response, the reponse must be
-/// sts_get_response_msg. This lemma is used to show that the response message, if is ok, has an object whose reference is
-/// daemon_set_key. resp_msg_matches_req_msg doesn't talk about the object in response should match the key in request
-/// so we need this extra spec and lemma.
-///
-/// If we don't have this, we have no idea of what is inside the response message.
+// This spec tells that when the reconciler is at AfterGetDaemonSet, and there is a matched response, the reponse must be
+// sts_get_response_msg. This lemma is used to show that the response message, if is ok, has an object whose reference is
+// daemon_set_key. resp_msg_matches_req_msg doesn't talk about the object in response should match the key in request
+// so we need this extra spec and lemma.
+//
+// If we don't have this, we have no idea of what is inside the response message.
 pub open spec fn response_at_after_get_resource_step_is_resource_get_response(
     sub_resource: SubResource, fb: FluentBitView
 ) -> StatePred<FBCluster> {

src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs

@@ -746,12 +746,12 @@ proof fn lemma_always_resource_object_create_or_update_request_msg_has_one_contr
     init_invariant(spec, FBCluster::init(), stronger_next, inv);
 }
 
-/// This lemma is used to show that if an action (which transfers the state from s to s_prime) creates a sub resource object
-/// create/update request message (with key as key), it must be a controller action, and the triggering cr is s.ongoing_reconciles()[key].triggering_cr.
-///
-/// After the action, the controller stays at After(Create/Update, SubResource) step.
-///
-/// Tips: Talking about both s and s_prime give more information to those using this lemma and also makes the verification faster.
+// This lemma is used to show that if an action (which transfers the state from s to s_prime) creates a sub resource object
+// create/update request message (with key as key), it must be a controller action, and the triggering cr is s.ongoing_reconciles()[key].triggering_cr.
+//
+// After the action, the controller stays at After(Create/Update, SubResource) step.
+//
+// Tips: Talking about both s and s_prime give more information to those using this lemma and also makes the verification faster.
 #[verifier(spinoff_prover)]
 pub proof fn lemma_resource_create_or_update_request_msg_implies_key_in_reconcile_equals(sub_resource: SubResource, fb: FluentBitView, s: FBCluster, s_prime: FBCluster, msg: FBMessage, step: FBStep)
     requires
@@ -828,25 +828,25 @@ pub proof fn lemma_eventually_always_no_delete_resource_request_msg_in_flight_fo
     leads_to_always_tla_forall_subresource(spec, true_pred(), |sub_resource: SubResource| lift_state(no_delete_resource_request_msg_in_flight(sub_resource, fb)));
 }
 
-/// This lemma demonstrates how to use kubernetes_cluster::proof::api_server_liveness::lemma_true_leads_to_always_every_in_flight_req_msg_satisfies
-/// (referred to as lemma_X) to prove that the system will eventually enter a state where delete daemon set request messages
-/// will never appear in flight.
-///
-/// As an example, we can look at how this lemma is proved.
-/// - Precondition: The preconditions should include all precondtions used by lemma_X and other predicates which show that
-///     the newly generated messages are as expected. ("expected" means not delete daemon set request messages in this lemma. Therefore,
-///     we provide an invariant daemon_set_has_owner_reference_pointing_to_current_cr so that the grabage collector won't try
-///     to send a delete request to delete the messsage.)
-/// - Postcondition: spec |= true ~> [](forall |msg| as_expected(msg))
-/// - Proof body: The proof consists of three parts.
-///   + Come up with "requirements" for those newly created api request messages. Usually, just move the forall |msg| and
-///     s.in_flight().contains(msg) in the statepred of final state (no_delete_ds_req_is_in_flight in this lemma, so we can
-///     get the requirements in this lemma).
-///   + Show that spec |= every_new_req_msg_if_in_flight_then_satisfies. Basically, use two assert forall to show that forall state and
-///     its next state and forall messages, if the messages are newly generated, they must satisfy the "requirements" and always satisfies it
-///     as long as it is in flight.
-///   + Call lemma_X. If a correct "requirements" are provided, we can easily prove the equivalence of every_in_flight_req_msg_satisfies(requirements)
-///     and the original statepred.
+// This lemma demonstrates how to use kubernetes_cluster::proof::api_server_liveness::lemma_true_leads_to_always_every_in_flight_req_msg_satisfies
+// (referred to as lemma_X) to prove that the system will eventually enter a state where delete daemon set request messages
+// will never appear in flight.
+//
+// As an example, we can look at how this lemma is proved.
+// - Precondition: The preconditions should include all precondtions used by lemma_X and other predicates which show that
+//     the newly generated messages are as expected. ("expected" means not delete daemon set request messages in this lemma. Therefore,
+//     we provide an invariant daemon_set_has_owner_reference_pointing_to_current_cr so that the grabage collector won't try
+//     to send a delete request to delete the messsage.)
+// - Postcondition: spec |= true ~> [](forall |msg| as_expected(msg))
+// - Proof body: The proof consists of three parts.
+//   + Come up with "requirements" for those newly created api request messages. Usually, just move the forall |msg| and
+//     s.in_flight().contains(msg) in the statepred of final state (no_delete_ds_req_is_in_flight in this lemma, so we can
+//     get the requirements in this lemma).
+//   + Show that spec |= every_new_req_msg_if_in_flight_then_satisfies. Basically, use two assert forall to show that forall state and
+//     its next state and forall messages, if the messages are newly generated, they must satisfy the "requirements" and always satisfies it
+//     as long as it is in flight.
+//   + Call lemma_X. If a correct "requirements" are provided, we can easily prove the equivalence of every_in_flight_req_msg_satisfies(requirements)
+//     and the original statepred.
 #[verifier(spinoff_prover)]
 pub proof fn lemma_eventually_always_no_delete_resource_request_msg_in_flight(spec: TempPred<FBCluster>, sub_resource: SubResource, fb: FluentBitView)
     requires

src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs

@@ -34,8 +34,8 @@ verus! {
 // And the following lemmas are more powerful because it considers the cases when the objects in update request messages
 // and etcd rely on each other to show they satisfy those properties.
 
-/// Objects in create request messages satisfying the properties can be proved along because it doesn't have to do with
-/// how the objects in etcd look like now.
+// Objects in create request messages satisfying the properties can be proved along because it doesn't have to do with
+// how the objects in etcd look like now.
 pub open spec fn object_in_every_create_request_msg_satisfies_unchangeable(sub_resource: SubResource, fb: FluentBitView) -> StatePred<FBCluster> {
     let resource_key = get_request(sub_resource, fb).key;
     |s: FBCluster| {
@@ -46,7 +46,7 @@ pub open spec fn object_in_every_create_request_msg_satisfies_unchangeable(sub_r
     }
 }
 
-/// On the contrary, we should combine the proof of update request message and etcd because they rely on each other.
+// On the contrary, we should combine the proof of update request message and etcd because they rely on each other.
 pub open spec fn object_in_every_update_request_msg_satisfies_unchangeable(sub_resource: SubResource, fb: FluentBitView) -> StatePred<FBCluster> {
     let resource_key = get_request(sub_resource, fb).key;
     |s: FBCluster| {

src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/validation.rs

@@ -28,13 +28,13 @@ use vstd::{multiset::*, prelude::*, string::*};
 
 verus! {
 
-/// We need such a spec for daemon set because certain fields are determined by the spec of custom resource object and won't
-/// be updated. So we need the transition validation of custom resource (fb) to show some fields of fb won't change
-/// by the update request. Therefore, though updating daemon set won't update those fields, the daemon set will still match
-/// the desired state.
-///
-/// We don't need this for other subresources because they don't have such fields: (1) those fields are determined by the fb
-/// object (except the key of fb); and (2) these fields won't be updated during update.
+// We need such a spec for daemon set because certain fields are determined by the spec of custom resource object and won't
+// be updated. So we need the transition validation of custom resource (fb) to show some fields of fb won't change
+// by the update request. Therefore, though updating daemon set won't update those fields, the daemon set will still match
+// the desired state.
+//
+// We don't need this for other subresources because they don't have such fields: (1) those fields are determined by the fb
+// object (except the key of fb); and (2) these fields won't be updated during update.
 pub open spec fn certain_fields_of_daemon_set_stay_unchanged(obj: DynamicObjectView, fb: FluentBitView) -> bool {
     let made_spec = make_daemon_set(fb).spec.get_Some_0();
     let ds = DaemonSetView::unmarshal(obj).get_Ok_0();

src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs

@@ -23,11 +23,11 @@ use vstd::{prelude::*, string::*};
 
 verus! {
 
-/// Proves AtAfterKRequestStep(Get, sub_resource) ~> sub_resource_state_matches(sub_resource, fb) and AtAfterKRequestStep(Get, sub_resource) ~>
-/// AtAfterKRequestStep(Get, next_resource). The second one is not applicable to DaemonSet which doesn't have a next resource.
-///
-/// The proof contains two part: resource_key exists or does not exist at first. The proof of both parts contains several times of applying
-/// wf1, handle_get_request => continue_reconcile => handle_create/update_request => continue_reconcile.
+// Proves AtAfterKRequestStep(Get, sub_resource) ~> sub_resource_state_matches(sub_resource, fb) and AtAfterKRequestStep(Get, sub_resource) ~>
+// AtAfterKRequestStep(Get, next_resource). The second one is not applicable to DaemonSet which doesn't have a next resource.
+//
+// The proof contains two part: resource_key exists or does not exist at first. The proof of both parts contains several times of applying
+// wf1, handle_get_request => continue_reconcile => handle_create/update_request => continue_reconcile.
 pub proof fn lemma_from_after_get_resource_step_to_resource_matches(
     spec: TempPred<FBCluster>, fb: FluentBitView, sub_resource: SubResource, next_resource: SubResource
 )

src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs

@@ -177,11 +177,11 @@ pub proof fn next_with_wf_is_stable()
     );
 }
 
-/// This predicate combines all the possible actions (next), weak fairness and invariants that hold throughout the execution.
-/// We name it invariants here because these predicates are never violated, thus they can all be seen as some kind of invariants.
-///
-/// The final goal of our proof is to show init /\ invariants |= []desired_state_is(cr) ~> []current_state_matches(cr).
-/// init /\ invariants is equivalent to init /\ next /\ weak_fairness, so we get cluster_spec() |= []desired_state_is(cr) ~> []current_state_matches(cr).
+// This predicate combines all the possible actions (next), weak fairness and invariants that hold throughout the execution.
+// We name it invariants here because these predicates are never violated, thus they can all be seen as some kind of invariants.
+//
+// The final goal of our proof is to show init /\ invariants |= []desired_state_is(cr) ~> []current_state_matches(cr).
+// init /\ invariants is equivalent to init /\ next /\ weak_fairness, so we get cluster_spec() |= []desired_state_is(cr) ~> []current_state_matches(cr).
 pub open spec fn invariants(fb: FluentBitView) -> TempPred<FBCluster> {
     next_with_wf().and(derived_invariants_since_beginning(fb))
 }
@@ -261,11 +261,11 @@ pub proof fn derived_invariants_since_beginning_is_stable(fb: FluentBitView)
     );
 }
 
-/// The first notable phase comes when crash and k8s busy are always disabled and the object in schedule always has the same
-/// spec and uid as the cr we provide.
-///
-/// Note that don't try to find any connections between those invariants -- they are put together because they don't have to
-/// wait for another of them to first be satisfied.
+// The first notable phase comes when crash and k8s busy are always disabled and the object in schedule always has the same
+// spec and uid as the cr we provide.
+//
+// Note that don't try to find any connections between those invariants -- they are put together because they don't have to
+// wait for another of them to first be satisfied.
 pub open spec fn invariants_since_phase_i(fb: FluentBitView) -> TempPred<FBCluster> {
     always(lift_state(FBCluster::crash_disabled()))
     .and(always(lift_state(FBCluster::busy_disabled())))
@@ -282,10 +282,10 @@ pub proof fn invariants_since_phase_i_is_stable(fb: FluentBitView)
     );
 }
 
-/// For now, phase II only contains one invariant, which is the object in reconcile has the same spec and uid as fb.
-///
-/// It is alone because it relies on the invariant the_object_in_schedule_has_spec_and_uid_as (in phase I) and every invariant
-/// in phase III relies on it.
+// For now, phase II only contains one invariant, which is the object in reconcile has the same spec and uid as fb.
+//
+// It is alone because it relies on the invariant the_object_in_schedule_has_spec_and_uid_as (in phase I) and every invariant
+// in phase III relies on it.
 pub open spec fn invariants_since_phase_ii(fb: FluentBitView) -> TempPred<FBCluster> {
     always(lift_state(FBCluster::the_object_in_reconcile_has_spec_and_uid_as(fb)))
 }
@@ -309,9 +309,9 @@ pub proof fn invariants_since_phase_iii_is_stable(fb: FluentBitView)
     stable_and_always_n!(tla_forall(a_to_p_1), tla_forall(a_to_p_2));
 }
 
-/// Invariants since this phase ensure that certain objects only have owner references that point to current cr.
-/// To have these invariants, we first need the invariant that evert create/update request make/change the object in the
-/// expected way.
+// Invariants since this phase ensure that certain objects only have owner references that point to current cr.
+// To have these invariants, we first need the invariant that evert create/update request make/change the object in the
+// expected way.
 pub open spec fn invariants_since_phase_iv(fb: FluentBitView) -> TempPred<FBCluster> {
     always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fb))))
 }
@@ -323,9 +323,9 @@ pub proof fn invariants_since_phase_iv_is_stable(fb: FluentBitView)
     always_p_is_stable(tla_forall(a_to_p_1));
 }
 
-/// Invariants since phase V rely on the invariants since phase IV. When the objects starts to always have owner reference
-/// pointing to current cr, it will never be recycled by the garbage collector. Plus, the reconciler itself never tries to
-/// delete this object, so we can have the invariants saying that no delete request messages will be in flight.
+// Invariants since phase V rely on the invariants since phase IV. When the objects starts to always have owner reference
+// pointing to current cr, it will never be recycled by the garbage collector. Plus, the reconciler itself never tries to
+// delete this object, so we can have the invariants saying that no delete request messages will be in flight.
 pub open spec fn invariants_since_phase_v(fb: FluentBitView) -> TempPred<FBCluster> {
     always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(sub_resource, fb))))
 }

src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/owner_ref.rs

@@ -27,8 +27,8 @@ use vstd::prelude::*;
 
 verus! {
 
-/// Valid owner_references field satisfies that every owner reference in it valid uid, i.e., it points to some existing objects.
-/// We don't test custom resource object here because we don't care about whether it's owner_references is valid.
+// Valid owner_references field satisfies that every owner reference in it valid uid, i.e., it points to some existing objects.
+// We don't test custom resource object here because we don't care about whether it's owner_references is valid.
 pub open spec fn owner_references_is_valid(obj: DynamicObjectView, s: FBCCluster) -> bool {
     let owner_refs = obj.metadata.owner_references.get_Some_0();
 

src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs

@@ -652,12 +652,12 @@ proof fn lemma_always_resource_object_create_or_update_request_msg_has_one_contr
     init_invariant(spec, FBCCluster::init(), stronger_next, inv);
 }
 
-/// This lemma is used to show that if an action (which transfers the state from s to s_prime) creates a sub resource object
-/// create/update request message (with key as key), it must be a controller action, and the triggering cr is s.ongoing_reconciles()[key].triggering_cr.
-///
-/// After the action, the controller stays at After(Create/Update, SubResource) step.
-///
-/// Tips: Talking about both s and s_prime give more information to those using this lemma and also makes the verification faster.
+// This lemma is used to show that if an action (which transfers the state from s to s_prime) creates a sub resource object
+// create/update request message (with key as key), it must be a controller action, and the triggering cr is s.ongoing_reconciles()[key].triggering_cr.
+//
+// After the action, the controller stays at After(Create/Update, SubResource) step.
+//
+// Tips: Talking about both s and s_prime give more information to those using this lemma and also makes the verification faster.
 #[verifier(spinoff_prover)]
 pub proof fn lemma_resource_create_or_update_request_msg_implies_key_in_reconcile_equals(sub_resource: SubResource, fbc: FluentBitConfigView, s: FBCCluster, s_prime: FBCCluster, msg: FBCMessage, step: FBCStep)
     requires