diff --git a/src/controller_examples/composition_example/consumer_controller/trusted/exec_types.rs b/src/controller_examples/composition_example/consumer_controller/trusted/exec_types.rs index e83a976e0..dc0bfc92e 100644 --- a/src/controller_examples/composition_example/consumer_controller/trusted/exec_types.rs +++ b/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, } diff --git a/src/controller_examples/composition_example/producer_controller/trusted/exec_types.rs b/src/controller_examples/composition_example/producer_controller/trusted/exec_types.rs index 45e719c68..bf4627be2 100644 --- a/src/controller_examples/composition_example/producer_controller/trusted/exec_types.rs +++ b/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, } diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/owner_ref.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/owner_ref.rs index a52aeee58..aaa2de059 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/owner_ref.rs +++ b/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(); diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/predicate.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/predicate.rs index 186de0e7a..0bb2612fb 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/predicate.rs +++ b/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 { diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs index 861f0f8c5..657b6a870 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs +++ b/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, sub_resource: SubResource, fb: FluentBitView) requires diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs index ddf06a4fb..a346f2a5f 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs +++ b/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 { 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 { let resource_key = get_request(sub_resource, fb).key; |s: FBCluster| { diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/validation.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/validation.rs index 14f3b24db..e211f7593 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/validation.rs +++ b/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(); diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs index 309851623..eb557a5f9 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs +++ b/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, fb: FluentBitView, sub_resource: SubResource, next_resource: SubResource ) diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs index c69a93613..f33dcacb5 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs +++ b/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 { 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 { 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 { 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 { 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 { always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(sub_resource, fb)))) } diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/owner_ref.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/owner_ref.rs index fff41ca33..2a2136c8f 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/owner_ref.rs +++ b/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(); diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs index d61b13ad4..42dcbd188 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs +++ b/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 diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/spec.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/spec.rs index 804542672..725344758 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/spec.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/spec.rs @@ -163,11 +163,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(fbc: FluentBitConfigView) -> TempPred { next_with_wf().and(derived_invariants_since_beginning(fbc)) } @@ -238,11 +238,11 @@ pub proof fn derived_invariants_since_beginning_is_stable(fbc: FluentBitConfigVi ); } -/// 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(fbc: FluentBitConfigView) -> TempPred { always(lift_state(FBCCluster::crash_disabled())) .and(always(lift_state(FBCCluster::busy_disabled()))) @@ -259,10 +259,10 @@ pub proof fn invariants_since_phase_i_is_stable(fbc: FluentBitConfigView) ); } -/// For now, phase II only contains one invariant, which is the object in reconcile has the same spec and uid as fbc. -/// -/// 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 fbc. +// +// 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(fbc: FluentBitConfigView) -> TempPred { always(lift_state(FBCCluster::the_object_in_reconcile_has_spec_and_uid_as(fbc))) } @@ -286,9 +286,9 @@ pub proof fn invariants_since_phase_iii_is_stable(fbc: FluentBitConfigView) 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(fbc: FluentBitConfigView) -> TempPred { always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fbc)))) } @@ -300,9 +300,9 @@ pub proof fn invariants_since_phase_iv_is_stable(fbc: FluentBitConfigView) 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(fbc: FluentBitConfigView) -> TempPred { always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(sub_resource, fbc)))) } diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/owner_ref.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/owner_ref.rs index 8ccea7810..fb3d40b36 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/owner_ref.rs +++ b/src/controller_examples/rabbitmq_controller/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: RMQCluster) -> bool { let owner_refs = obj.metadata.owner_references.get_Some_0(); diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs index 6e4e972e2..16842378d 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs +++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs @@ -112,12 +112,12 @@ pub open spec fn resource_create_response_msg(key: ObjectRef, s: RMQCluster) -> ) } -/// This spec tells that when the reconciler is at AfterGetStatefulSet, 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 -/// stateful_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 AfterGetStatefulSet, 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 +// stateful_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, rabbitmq: RabbitmqClusterView ) -> StatePred { @@ -283,7 +283,7 @@ pub open spec fn no_update_status_request_msg_not_from_bc_in_flight_of_stateful_ } } -/// We only need it for AfterGetStatefulSet, but keeping all the steps makes the invariant easier to prove. +// We only need it for AfterGetStatefulSet, but keeping all the steps makes the invariant easier to prove. pub open spec fn cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { let key = rabbitmq.object_ref(); diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs index 4ccc3d67f..ea3c6ff81 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs +++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs @@ -1222,12 +1222,12 @@ proof fn lemma_always_resource_object_create_or_update_request_msg_has_one_contr } -/// 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)] // TODO: broken by pod_event; Xudong will fix it later @@ -1509,25 +1509,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, rabbitmq))); } -/// 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 stateful 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 stateful set request messages in this lemma. Therefore, -/// we provide an invariant stateful_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_sts_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 stateful 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 stateful set request messages in this lemma. Therefore, +// we provide an invariant stateful_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_sts_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)] proof fn lemma_eventually_always_no_delete_resource_request_msg_in_flight(spec: TempPred, sub_resource: SubResource, rabbitmq: RabbitmqClusterView) requires diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs index 4c7e38fe0..d2a1e3862 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs +++ b/src/controller_examples/rabbitmq_controller/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, rabbitmq: RabbitmqClusterView) -> StatePred { let resource_key = get_request(sub_resource, rabbitmq).key; |s: RMQCluster| { @@ -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, rabbitmq: RabbitmqClusterView) -> StatePred { let resource_key = get_request(sub_resource, rabbitmq).key; |s: RMQCluster| { diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs index ecb10b8e8..0d318b901 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs +++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs @@ -28,13 +28,13 @@ use vstd::{multiset::*, prelude::*, string::*}; verus! { -/// We need such a spec for stateful 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 (rabbitmq) to show some fields of rabbitmq won't change -/// by the update request. Therefore, though updating stateful set won't update those fields, the stateful 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 rabbitmq -/// object (except the key of rabbitmq); and (2) these fields won't be updated during update. +// We need such a spec for stateful 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 (rabbitmq) to show some fields of rabbitmq won't change +// by the update request. Therefore, though updating stateful set won't update those fields, the stateful 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 rabbitmq +// object (except the key of rabbitmq); and (2) these fields won't be updated during update. pub open spec fn certain_fields_of_stateful_set_stay_unchanged(obj: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool { let made_spec = make_stateful_set(rabbitmq, ""@).spec.get_Some_0(); let sts = StatefulSetView::unmarshal(obj).get_Ok_0(); diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs index 77b2629eb..56d663a7e 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs @@ -26,11 +26,11 @@ use vstd::{prelude::*, string::*}; verus! { -/// Proves AtAfterKRequestStep(Get, sub_resource) ~> sub_resource_state_matches(sub_resource, rabbitmq) and AtAfterKRequestStep(Get, sub_resource) ~> -/// AtAfterKRequestStep(Get, next_resource). The second one is not applicable to StatefulSet 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, rabbitmq) and AtAfterKRequestStep(Get, sub_resource) ~> +// AtAfterKRequestStep(Get, next_resource). The second one is not applicable to StatefulSet 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, rabbitmq: RabbitmqClusterView, sub_resource: SubResource, next_resource: SubResource ) diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/spec.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/spec.rs index c86cfdef8..e0b900240 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/spec.rs +++ b/src/controller_examples/rabbitmq_controller/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(rabbitmq: RabbitmqClusterView) -> TempPred { next_with_wf().and(derived_invariants_since_beginning(rabbitmq)) } @@ -259,11 +259,11 @@ pub proof fn derived_invariants_since_beginning_is_stable(rabbitmq: RabbitmqClus ); } -/// 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(rabbitmq: RabbitmqClusterView) -> TempPred { always(lift_state(RMQCluster::crash_disabled())) .and(always(lift_state(RMQCluster::busy_disabled()))) @@ -280,10 +280,10 @@ pub proof fn invariants_since_phase_i_is_stable(rabbitmq: RabbitmqClusterView) ); } -/// For now, phase II only contains one invariant, which is the object in reconcile has the same spec and uid as rabbitmq. -/// -/// 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 rabbitmq. +// +// 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(rabbitmq: RabbitmqClusterView) -> TempPred { always(lift_state(RMQCluster::the_object_in_reconcile_has_spec_and_uid_as(rabbitmq))) } @@ -308,9 +308,9 @@ pub proof fn invariants_since_phase_iii_is_stable(rabbitmq: RabbitmqClusterView) 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(rabbitmq: RabbitmqClusterView) -> TempPred { always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, rabbitmq)))) } @@ -322,9 +322,9 @@ pub proof fn invariants_since_phase_iv_is_stable(rabbitmq: RabbitmqClusterView) 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(rabbitmq: RabbitmqClusterView) -> TempPred { always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(sub_resource, rabbitmq)))) } diff --git a/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs b/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs index 7c994f1fe..7f9cca219 100644 --- a/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs +++ b/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs @@ -36,11 +36,11 @@ proof fn safety_proof(rabbitmq: RabbitmqClusterView) lemma_stateful_set_never_scaled_down_for_rabbitmq(cluster_spec_without_wf(), rabbitmq); } -/// This invariant is exactly the high-level property. The proof of this invariant is where we talk about update Message. It requires another two invariants to hold all the time: -/// - replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd -/// - object_in_sts_update_request_has_smaller_rv_than_etcd -/// -/// Invariant 2 is to show that every stateful set update request must specify the resource version because stateful set is allowed to update unconditionally. If resource version can be none, we can't rule out invalid update request through resource version. Invariant 3 is quite obvious. +// This invariant is exactly the high-level property. The proof of this invariant is where we talk about update Message. It requires another two invariants to hold all the time: +// - replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd +// - object_in_sts_update_request_has_smaller_rv_than_etcd +// +// Invariant 2 is to show that every stateful set update request must specify the resource version because stateful set is allowed to update unconditionally. If resource version can be none, we can't rule out invalid update request through resource version. Invariant 3 is quite obvious. proof fn lemma_stateful_set_never_scaled_down_for_rabbitmq(spec: TempPred, rabbitmq: RabbitmqClusterView) requires spec.entails(lift_state(RMQCluster::init())), @@ -156,13 +156,13 @@ proof fn lemma_always_replicas_of_stateful_set_update_request_msg_is_no_smaller_ init_invariant(spec, RMQCluster::init(), next, inv); } -/// This function defined a replicas order for stateful set object. Here, obj can be the etcd statful set object, the object -/// in create/update stateful set object. We define this order because, the replicas in the update request is derived from -/// the triggering cr; so, in order to show the updated replicas is no smaller than the original one, we need to show that -/// the original one (the one stored in etcd)'s replicas is no larger than that of triggering cr. obj.metadata.owner_references_only_contains -/// (s.ongoing_reconciles()[key].triggering_cr.controller_owner_ref()) here is to ensure that the cr is still the one that creates the stateful -/// set object. The left two comparison is to assist the last one because when the state moves to the next state, the triggering_cr -/// may be assigned (inserted or updated). +// This function defined a replicas order for stateful set object. Here, obj can be the etcd statful set object, the object +// in create/update stateful set object. We define this order because, the replicas in the update request is derived from +// the triggering cr; so, in order to show the updated replicas is no smaller than the original one, we need to show that +// the original one (the one stored in etcd)'s replicas is no larger than that of triggering cr. obj.metadata.owner_references_only_contains +// (s.ongoing_reconciles()[key].triggering_cr.controller_owner_ref()) here is to ensure that the cr is still the one that creates the stateful +// set object. The left two comparison is to assist the last one because when the state moves to the next state, the triggering_cr +// may be assigned (inserted or updated). spec fn replicas_satisfies_order(obj: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> StatePred recommends obj.kind.is_StatefulSetKind(), diff --git a/src/controller_examples/rabbitmq_controller/trusted/exec_types.rs b/src/controller_examples/rabbitmq_controller/trusted/exec_types.rs index fb50f0faa..ca7cd907f 100644 --- a/src/controller_examples/rabbitmq_controller/trusted/exec_types.rs +++ b/src/controller_examples/rabbitmq_controller/trusted/exec_types.rs @@ -13,7 +13,7 @@ use vstd::prelude::*; verus! { -/// RabbitmqReconcileState describes the local state with which the reconcile functions makes decisions. +// RabbitmqReconcileState describes the local state with which the reconcile functions makes decisions. pub struct RabbitmqReconcileState { // reconcile_step, like a program counter, is used to track the progress of reconcile_core // since reconcile_core is frequently "trapped" into the controller_runtime spec. diff --git a/src/controller_examples/rabbitmq_controller/trusted/safety_theorem.rs b/src/controller_examples/rabbitmq_controller/trusted/safety_theorem.rs index 035a228ea..1178d3214 100644 --- a/src/controller_examples/rabbitmq_controller/trusted/safety_theorem.rs +++ b/src/controller_examples/rabbitmq_controller/trusted/safety_theorem.rs @@ -22,13 +22,13 @@ pub open spec fn safety(rabbitmq: RabbitmqClusterView) -> TempPred(rabbitmq))) } -/// To prove the safety property about stateful set, we need to first specify what the property is. -/// -/// Previously, we planned to use Message to describe the possible update/deletion/creation actions, and also specify the -/// relevant properties. However, it is better not to include Message in the description the high-level safety property -/// because Message is just a tool and a detail of the system. For update action, one way to circumvent using Message is -/// to talk about the previous and current state: an object being updated means that it exists in both states but changes -/// in current state. +// To prove the safety property about stateful set, we need to first specify what the property is. +// +// Previously, we planned to use Message to describe the possible update/deletion/creation actions, and also specify the +// relevant properties. However, it is better not to include Message in the description the high-level safety property +// because Message is just a tool and a detail of the system. For update action, one way to circumvent using Message is +// to talk about the previous and current state: an object being updated means that it exists in both states but changes +// in current state. pub open spec fn stateful_set_not_scaled_down(rabbitmq: RabbitmqClusterView) -> ActionPred { |s: RMQCluster, s_prime: RMQCluster| { let sts_key = M::make_stateful_set_key(rabbitmq); diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs index b78e33b67..4e0a86e49 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs @@ -128,11 +128,11 @@ pub open spec fn next_with_wf() -> TempPred { .and(VRSCluster::disable_pod_event().weak_fairness(())) } -/// 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(vrs: VReplicaSetView) -> TempPred { next_with_wf().and(derived_invariants_since_beginning(vrs)) } @@ -158,11 +158,11 @@ pub open spec fn derived_invariants_since_beginning(vrs: VReplicaSetView) -> Tem .and(always(lift_state(helper_invariants::every_create_request_is_well_formed()))) } -/// 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(vrs: VReplicaSetView) -> TempPred { always(lift_state(VRSCluster::crash_disabled())) .and(always(lift_state(VRSCluster::busy_disabled()))) diff --git a/src/controller_examples/v_replica_set_controller/trusted/exec_types.rs b/src/controller_examples/v_replica_set_controller/trusted/exec_types.rs index 037bad6fd..0d328646d 100644 --- a/src/controller_examples/v_replica_set_controller/trusted/exec_types.rs +++ b/src/controller_examples/v_replica_set_controller/trusted/exec_types.rs @@ -12,7 +12,7 @@ use vstd::prelude::*; verus! { -/// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions. +// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions. pub struct VReplicaSetReconcileState { pub reconcile_step: VReplicaSetReconcileStep, pub filtered_pods: Option>, diff --git a/src/controller_examples/zookeeper_controller/exec/resource/admin_server_service.rs b/src/controller_examples/zookeeper_controller/exec/resource/admin_server_service.rs index 8d9d57dbd..6cd8d2b57 100644 --- a/src/controller_examples/zookeeper_controller/exec/resource/admin_server_service.rs +++ b/src/controller_examples/zookeeper_controller/exec/resource/admin_server_service.rs @@ -109,7 +109,7 @@ pub fn update_admin_server_service(zk: &ZookeeperCluster, found_admin_server_ser admin_server_service } -/// Admin-server Service is used for client to connect to admin server +// Admin-server Service is used for client to connect to admin server pub fn make_admin_server_service(zk: &ZookeeperCluster) -> (service: Service) requires zk@.well_formed(), ensures service@ == model_resource::make_admin_server_service(zk@), diff --git a/src/controller_examples/zookeeper_controller/exec/resource/client_service.rs b/src/controller_examples/zookeeper_controller/exec/resource/client_service.rs index 16e5b95f0..001666831 100644 --- a/src/controller_examples/zookeeper_controller/exec/resource/client_service.rs +++ b/src/controller_examples/zookeeper_controller/exec/resource/client_service.rs @@ -111,7 +111,7 @@ pub fn update_client_service(zk: &ZookeeperCluster, found_client_service: &Servi client_service } -/// Client Service is used for any client to connect to the zookeeper server +// Client Service is used for any client to connect to the zookeeper server pub fn make_client_service(zk: &ZookeeperCluster) -> (service: Service) requires zk@.well_formed(), ensures service@ == model_resource::make_client_service(zk@), diff --git a/src/controller_examples/zookeeper_controller/exec/resource/common.rs b/src/controller_examples/zookeeper_controller/exec/resource/common.rs index c8a6bfd3f..f97bed357 100644 --- a/src/controller_examples/zookeeper_controller/exec/resource/common.rs +++ b/src/controller_examples/zookeeper_controller/exec/resource/common.rs @@ -51,7 +51,7 @@ pub fn make_owner_references(zk: &ZookeeperCluster) -> (owner_references: Vec, cluster_ip: bool) -> (service: Service) requires zk@.well_formed(), ensures service@ == model_resource::make_service(zk@, name@, ports@.map_values(|port: ServicePort| port@), cluster_ip), diff --git a/src/controller_examples/zookeeper_controller/exec/resource/config_map.rs b/src/controller_examples/zookeeper_controller/exec/resource/config_map.rs index 8f5df880b..2371db88a 100644 --- a/src/controller_examples/zookeeper_controller/exec/resource/config_map.rs +++ b/src/controller_examples/zookeeper_controller/exec/resource/config_map.rs @@ -100,7 +100,7 @@ pub fn update_config_map(zk: &ZookeeperCluster, found_config_map: &ConfigMap) -> config_map } -/// The ConfigMap stores the configuration data of zookeeper servers +// The ConfigMap stores the configuration data of zookeeper servers pub fn make_config_map(zk: &ZookeeperCluster) -> (config_map: ConfigMap) requires zk@.well_formed(), ensures config_map@ == model_resource::make_config_map(zk@), diff --git a/src/controller_examples/zookeeper_controller/exec/resource/headless_service.rs b/src/controller_examples/zookeeper_controller/exec/resource/headless_service.rs index 9923546d6..60ef21dad 100644 --- a/src/controller_examples/zookeeper_controller/exec/resource/headless_service.rs +++ b/src/controller_examples/zookeeper_controller/exec/resource/headless_service.rs @@ -111,7 +111,7 @@ pub fn update_headless_service(zk: &ZookeeperCluster, found_headless_service: &S headless_service } -/// Headless Service is used to assign DNS entry to each zookeeper server Pod +// Headless Service is used to assign DNS entry to each zookeeper server Pod pub fn make_headless_service(zk: &ZookeeperCluster) -> (service: Service) requires zk@.well_formed(), ensures service@ == model_resource::make_headless_service(zk@), diff --git a/src/controller_examples/zookeeper_controller/exec/resource/stateful_set.rs b/src/controller_examples/zookeeper_controller/exec/resource/stateful_set.rs index 28989e40a..3ff0d88a8 100644 --- a/src/controller_examples/zookeeper_controller/exec/resource/stateful_set.rs +++ b/src/controller_examples/zookeeper_controller/exec/resource/stateful_set.rs @@ -134,8 +134,8 @@ pub fn update_stateful_set(zk: &ZookeeperCluster, found_stateful_set: &StatefulS stateful_set } -/// The StatefulSet manages the zookeeper server containers (as Pods) -/// and the volumes attached to each server (as PersistentVolumeClaims) +// The StatefulSet manages the zookeeper server containers (as Pods) +// and the volumes attached to each server (as PersistentVolumeClaims) pub fn make_stateful_set(zk: &ZookeeperCluster, rv: &String) -> (stateful_set: StatefulSet) requires zk@.well_formed(), ensures stateful_set@ == model_resource::make_stateful_set(zk@, rv@), diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs index 35c9633e5..e1d216ad4 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs +++ b/src/controller_examples/zookeeper_controller/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: ZKCluster) -> bool { let owner_refs = obj.metadata.owner_references.get_Some_0(); diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs index 52ad3e2e0..4a47b7124 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs @@ -1133,12 +1133,12 @@ proof fn lemma_always_resource_object_create_or_update_request_msg_has_one_contr init_invariant(spec, ZKCluster::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, zookeeper: ZookeeperClusterView, s: ZKCluster, s_prime: ZKCluster, msg: ZKMessage, step: ZKStep) requires @@ -1301,25 +1301,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, zookeeper))); } -/// 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 stateful 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 stateful set request messages in this lemma. Therefore, -/// we provide an invariant stateful_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_sts_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 stateful 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 stateful set request messages in this lemma. Therefore, +// we provide an invariant stateful_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_sts_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, sub_resource: SubResource, zookeeper: ZookeeperClusterView) requires diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs index 69c903808..9d77e8c8d 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs @@ -36,8 +36,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, zookeeper: ZookeeperClusterView) -> StatePred { let resource_key = get_request(sub_resource, zookeeper).key; |s: ZKCluster| { @@ -48,7 +48,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, zookeeper: ZookeeperClusterView) -> StatePred { let resource_key = get_request(sub_resource, zookeeper).key; |s: ZKCluster| { diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs index d023a9ab7..9b70c1470 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs @@ -28,13 +28,13 @@ use vstd::{multiset::*, prelude::*, string::*}; verus! { -/// We need such a spec for stateful 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 (zookeeper) to show some fields of zookeeper won't change -/// by the update request. Therefore, though updating stateful set won't update those fields, the stateful 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 zookeeper -/// object (except the key of zookeeper); and (2) these fields won't be updated during update. +// We need such a spec for stateful 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 (zookeeper) to show some fields of zookeeper won't change +// by the update request. Therefore, though updating stateful set won't update those fields, the stateful 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 zookeeper +// object (except the key of zookeeper); and (2) these fields won't be updated during update. pub open spec fn certain_fields_of_stateful_set_stay_unchanged(obj: DynamicObjectView, zookeeper: ZookeeperClusterView) -> bool { let made_spec = make_stateful_set(zookeeper, ""@).spec.get_Some_0(); let sts = StatefulSetView::unmarshal(obj).get_Ok_0(); diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs b/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs index 92e7cd72d..a97f3f401 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs @@ -181,11 +181,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(zookeeper: ZookeeperClusterView) -> TempPred { next_with_wf().and(derived_invariants_since_beginning(zookeeper)) } @@ -275,11 +275,11 @@ pub proof fn derived_invariants_since_beginning_is_stable(zookeeper: ZookeeperCl ); } -/// 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(zookeeper: ZookeeperClusterView) -> TempPred { always(lift_state(ZKCluster::crash_disabled())) .and(always(lift_state(ZKCluster::busy_disabled()))) @@ -296,10 +296,10 @@ pub proof fn invariants_since_phase_i_is_stable(zookeeper: ZookeeperClusterView) ); } -/// For now, phase II only contains one invariant, which is the object in reconcile has the same spec and uid as zookeeper. -/// -/// 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 zookeeper. +// +// 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(zookeeper: ZookeeperClusterView) -> TempPred { always(lift_state(ZKCluster::the_object_in_reconcile_has_spec_and_uid_as(zookeeper))) } @@ -329,9 +329,9 @@ pub proof fn invariants_since_phase_iii_is_stable(zookeeper: ZookeeperClusterVie ); } -/// 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(zookeeper: ZookeeperClusterView) -> TempPred { always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)))) } @@ -343,9 +343,9 @@ pub proof fn invariants_since_phase_iv_is_stable(zookeeper: ZookeeperClusterView 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(zookeeper: ZookeeperClusterView) -> TempPred { always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(sub_resource, zookeeper)))) } diff --git a/src/controller_examples/zookeeper_controller/trusted/exec_types.rs b/src/controller_examples/zookeeper_controller/trusted/exec_types.rs index cd459c1d7..f13ecdf53 100644 --- a/src/controller_examples/zookeeper_controller/trusted/exec_types.rs +++ b/src/controller_examples/zookeeper_controller/trusted/exec_types.rs @@ -13,7 +13,7 @@ use vstd::{prelude::*, view::*}; verus! { -/// ZookeeperReconcileState describes the local state with which the reconcile functions makes decisions. +// ZookeeperReconcileState describes the local state with which the reconcile functions makes decisions. pub struct ZookeeperReconcileState { // reconcile_step, like a program counter, is used to track the progress of reconcile_core // since reconcile_core is frequently "trapped" into the controller_runtime spec. diff --git a/src/kubernetes_api_objects/exec/affinity.rs b/src/kubernetes_api_objects/exec/affinity.rs index e4b38fdbd..f8406c49e 100644 --- a/src/kubernetes_api_objects/exec/affinity.rs +++ b/src/kubernetes_api_objects/exec/affinity.rs @@ -10,13 +10,13 @@ use vstd::prelude::*; verus! { -/// Affinity is a group of affinity scheduling rules. -/// -/// This definition is a wrapper of Affinity defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/affinity.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/scheduling-eviction/assign-pod-node/#affinity-and-anti-affinity. +// Affinity is a group of affinity scheduling rules. +// +// This definition is a wrapper of Affinity defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/affinity.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/scheduling-eviction/assign-pod-node/#affinity-and-anti-affinity. #[verifier(external_body)] pub struct Affinity { diff --git a/src/kubernetes_api_objects/exec/api_method.rs b/src/kubernetes_api_objects/exec/api_method.rs index 9381beac4..d440a47f7 100644 --- a/src/kubernetes_api_objects/exec/api_method.rs +++ b/src/kubernetes_api_objects/exec/api_method.rs @@ -13,16 +13,16 @@ use vstd::pervasive::unreached; verus! { -/// KubeAPIRequest represents API requests used in executable. -/// -/// kube-rs uses a generic type kube::api::Api as an api handle to send -/// requests to the Kubernetes API. -/// So KubeAPIRequest wraps around the variables used to instantiate kube::api::Api -/// and to call its methods. -/// -/// Here we have one variant for each object kind because we need -/// the concrete object type to instantiate a kube::api::Api. -/// For example, to create a ConfigMap, we need to pass a ConfigMap object. +// KubeAPIRequest represents API requests used in executable. +// +// kube-rs uses a generic type kube::api::Api as an api handle to send +// requests to the Kubernetes API. +// So KubeAPIRequest wraps around the variables used to instantiate kube::api::Api +// and to call its methods. +// +// Here we have one variant for each object kind because we need +// the concrete object type to instantiate a kube::api::Api. +// For example, to create a ConfigMap, we need to pass a ConfigMap object. pub enum KubeAPIRequest { GetRequest(KubeGetRequest), @@ -33,7 +33,7 @@ pub enum KubeAPIRequest { UpdateStatusRequest(KubeUpdateStatusRequest), } -/// KubeGetRequest has the name as the parameter of Api.get(), and namespace to instantiate an Api. +// KubeGetRequest has the name as the parameter of Api.get(), and namespace to instantiate an Api. pub struct KubeGetRequest { pub api_resource: ApiResource, @@ -61,7 +61,7 @@ impl View for KubeGetRequest { } } -/// KubeListRequest has the namespace to instantiate an Api. +// KubeListRequest has the namespace to instantiate an Api. pub struct KubeListRequest { pub api_resource: ApiResource, @@ -85,7 +85,7 @@ impl View for KubeListRequest { } } -/// KubeCreateRequest has the obj as the parameter of Api.create(). +// KubeCreateRequest has the obj as the parameter of Api.create(). pub struct KubeCreateRequest { pub api_resource: ApiResource, @@ -110,7 +110,7 @@ impl View for KubeCreateRequest { } } -/// KubeDeleteRequest has the name as the parameter of Api.delete(), and namespace to instantiate an Api. +// KubeDeleteRequest has the name as the parameter of Api.delete(), and namespace to instantiate an Api. pub struct KubeDeleteRequest { pub api_resource: ApiResource, @@ -140,7 +140,7 @@ impl View for KubeDeleteRequest { } } -/// KubeUpdateRequest has the obj as the parameter of Api.replace(). +// KubeUpdateRequest has the obj as the parameter of Api.replace(). pub struct KubeUpdateRequest { pub api_resource: ApiResource, @@ -167,7 +167,7 @@ impl View for KubeUpdateRequest { } } -/// KubeUpdateRequest has the obj as the parameter of Api.replace_status(). +// KubeUpdateRequest has the obj as the parameter of Api.replace_status(). pub struct KubeUpdateStatusRequest { pub api_resource: ApiResource, @@ -217,9 +217,9 @@ pub open spec fn opt_req_to_view(req: &Option) -> Option, @@ -247,7 +247,7 @@ impl View for KubeGetResponse { } } -/// KubeListResponse has the sequence of objects returned by KubeListRequest. +// KubeListResponse has the sequence of objects returned by KubeListRequest. pub struct KubeListResponse { pub res: Result, APIError>, @@ -263,7 +263,7 @@ impl View for KubeListResponse { } } -/// KubeCreateResponse has the object created by KubeCreateRequest. +// KubeCreateResponse has the object created by KubeCreateRequest. pub struct KubeCreateResponse { pub res: Result, @@ -279,7 +279,7 @@ impl View for KubeCreateResponse { } } -/// DeleteResponse has (last version of) the object deleted by DeleteRequest. +// DeleteResponse has (last version of) the object deleted by DeleteRequest. pub struct KubeDeleteResponse { pub res: Result<(), APIError>, @@ -295,7 +295,7 @@ impl View for KubeDeleteResponse { } } -/// KubeUpdateResponse has the object updated by KubeUpdateRequest. +// KubeUpdateResponse has the object updated by KubeUpdateRequest. pub struct KubeUpdateResponse { pub res: Result, @@ -311,7 +311,7 @@ impl View for KubeUpdateResponse { } } -/// KubeUpdateStatusResponse has the object updated by KubeUpdateStatusRequest. +// KubeUpdateStatusResponse has the object updated by KubeUpdateStatusRequest. pub struct KubeUpdateStatusResponse { pub res: Result, diff --git a/src/kubernetes_api_objects/exec/api_resource.rs b/src/kubernetes_api_objects/exec/api_resource.rs index 4534d8012..7d4cda3c4 100644 --- a/src/kubernetes_api_objects/exec/api_resource.rs +++ b/src/kubernetes_api_objects/exec/api_resource.rs @@ -6,11 +6,11 @@ use vstd::prelude::*; verus! { -/// ApiResource is used for creating API handles for DynamicObject. -/// -/// This definition is a wrapper of ApiResource defined at -/// https://github.com/kube-rs/kube/blob/main/kube-core/src/discovery.rs. -/// It is supposed to be used in exec controller code. +// ApiResource is used for creating API handles for DynamicObject. +// +// This definition is a wrapper of ApiResource defined at +// https://github.com/kube-rs/kube/blob/main/kube-core/src/discovery.rs. +// It is supposed to be used in exec controller code. #[verifier(external_body)] pub struct ApiResource { diff --git a/src/kubernetes_api_objects/exec/config_map.rs b/src/kubernetes_api_objects/exec/config_map.rs index 49f835416..7cfdcd04f 100644 --- a/src/kubernetes_api_objects/exec/config_map.rs +++ b/src/kubernetes_api_objects/exec/config_map.rs @@ -10,15 +10,15 @@ use vstd::prelude::*; verus! { -/// ConfigMap is a type of API object used to store non-confidential data in key-value pairs. -/// A ConfigMap object can be used to set environment variables or configuration files -/// in a Volume mounted to a Pod. -/// -/// This definition is a wrapper of ConfigMap defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/config_map.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/configuration/configmap/. +// ConfigMap is a type of API object used to store non-confidential data in key-value pairs. +// A ConfigMap object can be used to set environment variables or configuration files +// in a Volume mounted to a Pod. +// +// This definition is a wrapper of ConfigMap defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/config_map.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/configuration/configmap/. #[verifier(external_body)] pub struct ConfigMap { diff --git a/src/kubernetes_api_objects/exec/daemon_set.rs b/src/kubernetes_api_objects/exec/daemon_set.rs index ff3b62b05..4f8972c02 100644 --- a/src/kubernetes_api_objects/exec/daemon_set.rs +++ b/src/kubernetes_api_objects/exec/daemon_set.rs @@ -11,17 +11,17 @@ use vstd::{prelude::*, seq_lib::*, string::*}; verus! { -/// DaemonSet is a type of API object used for managing daemon applications, -/// mainly a group of Pods and PersistentVolumeClaims attached to the Pods. -/// A DaemonSet object allows different types of Volumes attached to the pods, -/// including ConfigMaps, Secrets and PersistentVolumeClaims. -/// It also exposes the applications using a headless service. -/// -/// This definition is a wrapper of DaemonSet defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/apps/v1/daemon_set.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/workloads/controllers/daemonset/. +// DaemonSet is a type of API object used for managing daemon applications, +// mainly a group of Pods and PersistentVolumeClaims attached to the Pods. +// A DaemonSet object allows different types of Volumes attached to the pods, +// including ConfigMaps, Secrets and PersistentVolumeClaims. +// It also exposes the applications using a headless service. +// +// This definition is a wrapper of DaemonSet defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/apps/v1/daemon_set.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/workloads/controllers/daemonset/. #[verifier(external_body)] pub struct DaemonSet { @@ -90,7 +90,7 @@ impl DaemonSet { DynamicObject::from_kube(deps_hack::k8s_openapi::serde_json::from_str(&deps_hack::k8s_openapi::serde_json::to_string(&self.inner).unwrap()).unwrap()) } - /// Convert a DynamicObject to a DaemonSet + // Convert a DynamicObject to a DaemonSet #[verifier(external_body)] pub fn unmarshal(obj: DynamicObject) -> (res: Result) ensures diff --git a/src/kubernetes_api_objects/exec/dynamic.rs b/src/kubernetes_api_objects/exec/dynamic.rs index f274cde55..e8af445e3 100644 --- a/src/kubernetes_api_objects/exec/dynamic.rs +++ b/src/kubernetes_api_objects/exec/dynamic.rs @@ -8,9 +8,9 @@ use vstd::prelude::*; verus! { -/// DynamicObject is mainly used to pass requests/response between reconcile_core and the shim layer. -/// We use DynamicObject in KubeAPIRequest and KubeAPIResponse so that they can carry the requests and responses -/// for all kinds of Kubernetes resource objects without exhaustive pattern matching. +// DynamicObject is mainly used to pass requests/response between reconcile_core and the shim layer. +// We use DynamicObject in KubeAPIRequest and KubeAPIResponse so that they can carry the requests and responses +// for all kinds of Kubernetes resource objects without exhaustive pattern matching. #[verifier(external_body)] pub struct DynamicObject { diff --git a/src/kubernetes_api_objects/exec/label_selector.rs b/src/kubernetes_api_objects/exec/label_selector.rs index 5d8b2ba49..bdefedca1 100644 --- a/src/kubernetes_api_objects/exec/label_selector.rs +++ b/src/kubernetes_api_objects/exec/label_selector.rs @@ -8,14 +8,14 @@ use vstd::{prelude::*, string::*}; verus! { -/// LabelSelector is used to select objects that are relevant by matching the labels. -/// Labels are key/value pairs that are attached to objects such as Pods. -/// -/// This definition is a wrapper of LabelSelector defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/apimachinery/pkg/apis/meta/v1/label_selector.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/overview/working-with-objects/labels/#label-selectors. +// LabelSelector is used to select objects that are relevant by matching the labels. +// Labels are key/value pairs that are attached to objects such as Pods. +// +// This definition is a wrapper of LabelSelector defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/apimachinery/pkg/apis/meta/v1/label_selector.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/overview/working-with-objects/labels/#label-selectors. #[verifier(external_body)] pub struct LabelSelector { diff --git a/src/kubernetes_api_objects/exec/object_meta.rs b/src/kubernetes_api_objects/exec/object_meta.rs index cb3f17011..2fea18e83 100644 --- a/src/kubernetes_api_objects/exec/object_meta.rs +++ b/src/kubernetes_api_objects/exec/object_meta.rs @@ -8,14 +8,14 @@ use vstd::{prelude::*, string::*}; verus! { -/// ObjectMeta contains the metadata that all Kubernetes resource objects must have, -/// including name, namespace, uid, and so on. -/// -/// This definition is a wrapper of ObjectMeta defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/apimachinery/pkg/apis/meta/v1/object_meta.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/reference/kubernetes-api/common-definitions/object-meta/. +// ObjectMeta contains the metadata that all Kubernetes resource objects must have, +// including name, namespace, uid, and so on. +// +// This definition is a wrapper of ObjectMeta defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/apimachinery/pkg/apis/meta/v1/object_meta.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/reference/kubernetes-api/common-definitions/object-meta/. #[verifier(external_body)] pub struct ObjectMeta { diff --git a/src/kubernetes_api_objects/exec/owner_reference.rs b/src/kubernetes_api_objects/exec/owner_reference.rs index 6c19f3a1f..b1eaeec14 100644 --- a/src/kubernetes_api_objects/exec/owner_reference.rs +++ b/src/kubernetes_api_objects/exec/owner_reference.rs @@ -9,13 +9,13 @@ use vstd::{prelude::*, string::*}; verus! { -/// OwnerReference contains enough information to let you identify an owning object. -/// An owning object must be in the same namespace as the dependent, or be cluster-scoped, so there is no namespace field. -/// -/// This definition is a wrapper of OwnerReference defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/apimachinery/pkg/apis/meta/v1/owner_reference.rs. -/// It is supposed to be used in exec controller code. -/// +// OwnerReference contains enough information to let you identify an owning object. +// An owning object must be in the same namespace as the dependent, or be cluster-scoped, so there is no namespace field. +// +// This definition is a wrapper of OwnerReference defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/apimachinery/pkg/apis/meta/v1/owner_reference.rs. +// It is supposed to be used in exec controller code. +// #[verifier(external_body)] pub struct OwnerReference { diff --git a/src/kubernetes_api_objects/exec/persistent_volume_claim.rs b/src/kubernetes_api_objects/exec/persistent_volume_claim.rs index 292818aa0..cfe9928c9 100644 --- a/src/kubernetes_api_objects/exec/persistent_volume_claim.rs +++ b/src/kubernetes_api_objects/exec/persistent_volume_claim.rs @@ -11,14 +11,14 @@ use vstd::seq_lib::*; verus! { -/// PersistentVolumeClaim is a type of API object representing a request for storage (typically used by a Pod). -/// PersistentVolumeClaim objects are often defined in StatefulSet objects as the Volumes mounted to the Pods. -/// -/// This definition is a wrapper of PersistentVolumeClaim defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/persistent_volume_claim.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/storage/persistent-volumes/. +// PersistentVolumeClaim is a type of API object representing a request for storage (typically used by a Pod). +// PersistentVolumeClaim objects are often defined in StatefulSet objects as the Volumes mounted to the Pods. +// +// This definition is a wrapper of PersistentVolumeClaim defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/persistent_volume_claim.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/storage/persistent-volumes/. #[verifier(external_body)] pub struct PersistentVolumeClaim { diff --git a/src/kubernetes_api_objects/exec/pod.rs b/src/kubernetes_api_objects/exec/pod.rs index 8eb7cf33d..b4befe36d 100644 --- a/src/kubernetes_api_objects/exec/pod.rs +++ b/src/kubernetes_api_objects/exec/pod.rs @@ -13,17 +13,17 @@ use vstd::string::*; verus! { -/// Pod is a type of API object used for grouping one or more containers that share storage and network resources. -/// This is the smallest deployable unit in Kubernetes. -/// -/// You can specify the Container(s), including the images and commands, and the Volume(s), -/// such as a ConfigMap or a Secret, in the specification of a Pod (i.e., PodSpec). -/// -/// This definition is a wrapper of Pod defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/pod.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/workloads/pods/. +// Pod is a type of API object used for grouping one or more containers that share storage and network resources. +// This is the smallest deployable unit in Kubernetes. +// +// You can specify the Container(s), including the images and commands, and the Volume(s), +// such as a ConfigMap or a Secret, in the specification of a Pod (i.e., PodSpec). +// +// This definition is a wrapper of Pod defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/pod.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/workloads/pods/. #[verifier(external_body)] pub struct Pod { @@ -97,7 +97,7 @@ impl Pod { DynamicObject::from_kube(deps_hack::k8s_openapi::serde_json::from_str(&deps_hack::k8s_openapi::serde_json::to_string(&self.inner).unwrap()).unwrap()) } - /// Convert a DynamicObject to a Pod + // Convert a DynamicObject to a Pod #[verifier(external_body)] pub fn unmarshal(obj: DynamicObject) -> (res: Result) ensures diff --git a/src/kubernetes_api_objects/exec/resource.rs b/src/kubernetes_api_objects/exec/resource.rs index a67e36ab8..3e3e215b1 100644 --- a/src/kubernetes_api_objects/exec/resource.rs +++ b/src/kubernetes_api_objects/exec/resource.rs @@ -4,7 +4,7 @@ use vstd::prelude::*; verus! { -/// This trait defines the methods that each wrapper of Kubernetes resource object should implement +// This trait defines the methods that each wrapper of Kubernetes resource object should implement pub trait ResourceWrapper: Sized { fn from_kube(inner: T) -> Self; diff --git a/src/kubernetes_api_objects/exec/role.rs b/src/kubernetes_api_objects/exec/role.rs index 616925151..584e5495c 100644 --- a/src/kubernetes_api_objects/exec/role.rs +++ b/src/kubernetes_api_objects/exec/role.rs @@ -10,11 +10,11 @@ use vstd::{prelude::*, seq_lib::*}; verus! { -/// This definition is a wrapper of Role defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/rbac/v1/role.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/reference/access-authn-authz/rbac/. +// This definition is a wrapper of Role defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/rbac/v1/role.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/reference/access-authn-authz/rbac/. #[verifier(external_body)] pub struct Role { diff --git a/src/kubernetes_api_objects/exec/role_binding.rs b/src/kubernetes_api_objects/exec/role_binding.rs index 21719886e..b8716af00 100644 --- a/src/kubernetes_api_objects/exec/role_binding.rs +++ b/src/kubernetes_api_objects/exec/role_binding.rs @@ -14,11 +14,11 @@ use vstd::string::*; verus! { -/// This definition is a wrapper of RoleBinding defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/rbac/v1/role_binding.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/reference/access-authn-authz/rbac/. +// This definition is a wrapper of RoleBinding defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/rbac/v1/role_binding.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/reference/access-authn-authz/rbac/. #[verifier(external_body)] pub struct RoleBinding { diff --git a/src/kubernetes_api_objects/exec/secret.rs b/src/kubernetes_api_objects/exec/secret.rs index 7f9990391..86579c29b 100644 --- a/src/kubernetes_api_objects/exec/secret.rs +++ b/src/kubernetes_api_objects/exec/secret.rs @@ -11,15 +11,15 @@ use vstd::prelude::*; verus! { -/// Secret is a type of API object used to store confidential data in key-value pairs. -/// A Secret object can be used to set environment variables or configuration files -/// in a Volume mounted to a Pod. -/// -/// This definition is a wrapper of Secret defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/secret.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/configuration/secret/. +// Secret is a type of API object used to store confidential data in key-value pairs. +// A Secret object can be used to set environment variables or configuration files +// in a Volume mounted to a Pod. +// +// This definition is a wrapper of Secret defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/secret.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/configuration/secret/. #[verifier(external_body)] pub struct Secret { diff --git a/src/kubernetes_api_objects/exec/service.rs b/src/kubernetes_api_objects/exec/service.rs index 17c9be047..53b7ed4d0 100644 --- a/src/kubernetes_api_objects/exec/service.rs +++ b/src/kubernetes_api_objects/exec/service.rs @@ -12,15 +12,15 @@ use vstd::seq_lib::*; verus! { -/// Service is a type of API object used for exposing a network application -/// that is running as one or more Pods in your cluster. -/// A Service object can be used to assign stable IP addresses and DNS names to pods. -/// -/// This definition is a wrapper of Service defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/service.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/services-networking/service/. +// Service is a type of API object used for exposing a network application +// that is running as one or more Pods in your cluster. +// A Service object can be used to assign stable IP addresses and DNS names to pods. +// +// This definition is a wrapper of Service defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/service.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/services-networking/service/. #[verifier(external_body)] pub struct Service { diff --git a/src/kubernetes_api_objects/exec/service_account.rs b/src/kubernetes_api_objects/exec/service_account.rs index 186454003..40725704d 100644 --- a/src/kubernetes_api_objects/exec/service_account.rs +++ b/src/kubernetes_api_objects/exec/service_account.rs @@ -11,15 +11,15 @@ use vstd::prelude::*; verus! { -/// A service account is a type of non-human account that, in Kubernetes, provides a distinct identity in a Kubernetes cluster. -/// Application Pods, system components, and entities inside and outside the cluster can use a specific ServiceAccount's credentials to identify as that ServiceAccount. -/// This identity is useful in various situations, including authenticating to the API server or implementing identity-based security policies. -/// -/// This definition is a wrapper of ServiceAccount defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/service_account.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/security/service-accounts/. +// A service account is a type of non-human account that, in Kubernetes, provides a distinct identity in a Kubernetes cluster. +// Application Pods, system components, and entities inside and outside the cluster can use a specific ServiceAccount's credentials to identify as that ServiceAccount. +// This identity is useful in various situations, including authenticating to the API server or implementing identity-based security policies. +// +// This definition is a wrapper of ServiceAccount defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/service_account.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/security/service-accounts/. #[verifier(external_body)] pub struct ServiceAccount { diff --git a/src/kubernetes_api_objects/exec/stateful_set.rs b/src/kubernetes_api_objects/exec/stateful_set.rs index b7aa75360..4c791943f 100644 --- a/src/kubernetes_api_objects/exec/stateful_set.rs +++ b/src/kubernetes_api_objects/exec/stateful_set.rs @@ -14,17 +14,17 @@ use vstd::string::*; verus! { -/// StatefulSet is a type of API object used for managing stateful applications, -/// mainly a group of Pods and PersistentVolumeClaims attached to the Pods. -/// A StatefulSet object allows different types of Volumes attached to the pods, -/// including ConfigMaps, Secrets and PersistentVolumeClaims. -/// It also exposes the applications using a headless service. -/// -/// This definition is a wrapper of StatefulSet defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/apps/v1/stateful_set.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/workloads/controllers/statefulset/. +// StatefulSet is a type of API object used for managing stateful applications, +// mainly a group of Pods and PersistentVolumeClaims attached to the Pods. +// A StatefulSet object allows different types of Volumes attached to the pods, +// including ConfigMaps, Secrets and PersistentVolumeClaims. +// It also exposes the applications using a headless service. +// +// This definition is a wrapper of StatefulSet defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/apps/v1/stateful_set.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/workloads/controllers/statefulset/. #[verifier(external_body)] pub struct StatefulSet { @@ -116,7 +116,7 @@ impl StatefulSet { ) } - /// Convert a DynamicObject to a StatefulSet + // Convert a DynamicObject to a StatefulSet #[verifier(external_body)] pub fn unmarshal(obj: DynamicObject) -> (res: Result) ensures diff --git a/src/kubernetes_api_objects/exec/toleration.rs b/src/kubernetes_api_objects/exec/toleration.rs index c52add5c3..8d0ff2ff4 100644 --- a/src/kubernetes_api_objects/exec/toleration.rs +++ b/src/kubernetes_api_objects/exec/toleration.rs @@ -11,13 +11,13 @@ use vstd::prelude::*; verus! { -/// The pod this Toleration is attached to tolerates any taint that matches -/// -/// This definition is a wrapper of Toleration defined at -/// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/toleration.rs. -/// It is supposed to be used in exec controller code. -/// -/// More detailed information: https://kubernetes.io/docs/concepts/scheduling-eviction/taint-and-toleration/. +// The pod this Toleration is attached to tolerates any taint that matches +// +// This definition is a wrapper of Toleration defined at +// https://github.com/Arnavion/k8s-openapi/blob/v0.17.0/src/v1_26/api/core/v1/toleration.rs. +// It is supposed to be used in exec controller code. +// +// More detailed information: https://kubernetes.io/docs/concepts/scheduling-eviction/taint-and-toleration/. #[verifier(external_body)] pub struct Toleration { diff --git a/src/kubernetes_api_objects/exec/volume.rs b/src/kubernetes_api_objects/exec/volume.rs index becdc8a8d..33cc2cf51 100644 --- a/src/kubernetes_api_objects/exec/volume.rs +++ b/src/kubernetes_api_objects/exec/volume.rs @@ -82,7 +82,7 @@ impl Volume { #[verifier(external)] pub fn from_kube(inner: deps_hack::k8s_openapi::api::core::v1::Volume) -> Volume { Volume { inner } } - /// Methods for the fields that Anvil currently does not reason about + // Methods for the fields that Anvil currently does not reason about #[verifier(external_body)] pub fn set_empty_dir(&mut self, empty_dir: EmptyDirVolumeSource) diff --git a/src/kubernetes_api_objects/spec/affinity.rs b/src/kubernetes_api_objects/spec/affinity.rs index a4438e4c4..fd49b75df 100644 --- a/src/kubernetes_api_objects/spec/affinity.rs +++ b/src/kubernetes_api_objects/spec/affinity.rs @@ -4,8 +4,8 @@ use vstd::prelude::*; verus! { -/// AffinityView is the ghost type of Affinity. -/// It is supposed to be used in spec and proof code. +// AffinityView is the ghost type of Affinity. + pub struct AffinityView {} diff --git a/src/kubernetes_api_objects/spec/api_method.rs b/src/kubernetes_api_objects/spec/api_method.rs index 5d4ba897a..1b9bc9f2c 100644 --- a/src/kubernetes_api_objects/spec/api_method.rs +++ b/src/kubernetes_api_objects/spec/api_method.rs @@ -12,11 +12,11 @@ use vstd::{prelude::*, view::*}; verus! { -/// APIRequest represents API requests sent to the Kubernetes API for specifications. -/// -/// Kubernetes API accepts in general seven types requests: Get, List, Create, Delete, Update, Patch and Watch. -/// Each variant in APIRequest represents on type of request. -/// For now we do not consider Watch. +// APIRequest represents API requests sent to the Kubernetes API for specifications. +// +// Kubernetes API accepts in general seven types requests: Get, List, Create, Delete, Update, Patch and Watch. +// Each variant in APIRequest represents on type of request. +// For now we do not consider Watch. // TODO: implement Update and Patch request. #[is_variant] @@ -29,20 +29,20 @@ pub enum APIRequest { UpdateStatusRequest(UpdateStatusRequest), } -/// GetRequest gets an object with the key (kind, name and namespace). +// GetRequest gets an object with the key (kind, name and namespace). pub struct GetRequest { pub key: ObjectRef, } -/// ListRequest lists all the objects of kind in namespace. +// ListRequest lists all the objects of kind in namespace. pub struct ListRequest { pub kind: Kind, pub namespace: StringView, } -/// CreateRequest creates the obj. +// CreateRequest creates the obj. pub struct CreateRequest { pub namespace: StringView, @@ -59,14 +59,14 @@ impl CreateRequest { } } -/// DeleteRequest deletes the object with the key. +// DeleteRequest deletes the object with the key. pub struct DeleteRequest { pub key: ObjectRef, pub preconditions: Option, } -/// UpdateRequest replaces the existing obj with a new one. +// UpdateRequest replaces the existing obj with a new one. pub struct UpdateRequest { pub namespace: StringView, @@ -84,7 +84,7 @@ impl UpdateRequest { } } -/// UpdateStatusRequest replaces the status of the existing obj with a new one. +// UpdateStatusRequest replaces the status of the existing obj with a new one. pub struct UpdateStatusRequest { pub namespace: StringView, @@ -102,7 +102,7 @@ impl UpdateStatusRequest { } } -/// APIResponse represents API responses sent from the Kubernetes API for specifications. +// APIResponse represents API responses sent from the Kubernetes API for specifications. #[is_variant] pub enum APIResponse { @@ -114,37 +114,37 @@ pub enum APIResponse { UpdateStatusResponse(UpdateStatusResponse), } -/// GetResponse has the object returned by GetRequest. +// GetResponse has the object returned by GetRequest. pub struct GetResponse { pub res: Result, } -/// ListResponse has the sequence of objects returned by ListRequest. +// ListResponse has the sequence of objects returned by ListRequest. pub struct ListResponse { pub res: Result, APIError>, } -/// CreateResponse has the object created by CreateRequest. +// CreateResponse has the object created by CreateRequest. pub struct CreateResponse { pub res: Result, } -/// DeleteResponse does NOT contain the object that gets deleted. +// DeleteResponse does NOT contain the object that gets deleted. pub struct DeleteResponse { pub res: Result<(), APIError>, } -/// UpdateResponse has the object updated by UpdateRequest. +// UpdateResponse has the object updated by UpdateRequest. pub struct UpdateResponse { pub res: Result, } -/// UpdateStatusResponse has the object updated by UpdateStatusRequest. +// UpdateStatusResponse has the object updated by UpdateStatusRequest. pub struct UpdateStatusResponse { pub res: Result, diff --git a/src/kubernetes_api_objects/spec/api_resource.rs b/src/kubernetes_api_objects/spec/api_resource.rs index 78a10c0eb..1a94192a5 100644 --- a/src/kubernetes_api_objects/spec/api_resource.rs +++ b/src/kubernetes_api_objects/spec/api_resource.rs @@ -5,8 +5,8 @@ use vstd::prelude::*; verus! { -/// ApiResourceView is the ghost type of ApiResource. -/// It is supposed to be used in spec and proof code. +// ApiResourceView is the ghost type of ApiResource. + pub struct ApiResourceView { pub kind: Kind, diff --git a/src/kubernetes_api_objects/spec/config_map.rs b/src/kubernetes_api_objects/spec/config_map.rs index 6fd8a47a5..fa0127c03 100644 --- a/src/kubernetes_api_objects/spec/config_map.rs +++ b/src/kubernetes_api_objects/spec/config_map.rs @@ -7,22 +7,22 @@ use vstd::prelude::*; verus! { -/// ConfigMapView is the ghost type of ConfigMap. -/// It is supposed to be used in spec and proof code. +// ConfigMapView is the ghost type of ConfigMap. + pub struct ConfigMapView { pub metadata: ObjectMetaView, pub data: Option>, } -/// This ConfigMapSpecView is defined only to call marshal_spec and unmarshal_spec conveniently -/// Unlike most other Kubernetes objects, a ConfigMap does not have a spec field, -/// but its data, binary_data and immutable fields are treated similarly as spec of other objects. -/// Here we use a tuple to wrap around ConfigMap's fields (we will implement more fields like binary_data later) -/// instead of defining another struct. -/// -/// We use a unit type in the tuple because there has to be at least two members in a tuple. -/// The unit type will be replaced once we support other fields than data. +// This ConfigMapSpecView is defined only to call marshal_spec and unmarshal_spec conveniently +// Unlike most other Kubernetes objects, a ConfigMap does not have a spec field, +// but its data, binary_data and immutable fields are treated similarly as spec of other objects. +// Here we use a tuple to wrap around ConfigMap's fields (we will implement more fields like binary_data later) +// instead of defining another struct. +// +// We use a unit type in the tuple because there has to be at least two members in a tuple. +// The unit type will be replaced once we support other fields than data. type ConfigMapSpecView = Option>; impl ConfigMapView { diff --git a/src/kubernetes_api_objects/spec/daemon_set.rs b/src/kubernetes_api_objects/spec/daemon_set.rs index d0bbab2aa..55f5f6e54 100644 --- a/src/kubernetes_api_objects/spec/daemon_set.rs +++ b/src/kubernetes_api_objects/spec/daemon_set.rs @@ -12,8 +12,8 @@ use vstd::string::*; verus! { -/// DaemonSetView is the ghost type of DaemonSet. -/// It is supposed to be used in spec and proof code. +// DaemonSetView is the ghost type of DaemonSet. + pub struct DaemonSetView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/dynamic.rs b/src/kubernetes_api_objects/spec/dynamic.rs index 540b29119..24d3f87fd 100644 --- a/src/kubernetes_api_objects/spec/dynamic.rs +++ b/src/kubernetes_api_objects/spec/dynamic.rs @@ -8,8 +8,8 @@ use vstd::prelude::*; verus! { -/// DynamicObjectView is the ghost type of DynamicObject. -/// It is supposed to be used in spec and proof code. +// DynamicObjectView is the ghost type of DynamicObject. + pub struct DynamicObjectView { pub kind: Kind, diff --git a/src/kubernetes_api_objects/spec/label_selector.rs b/src/kubernetes_api_objects/spec/label_selector.rs index ef74bb274..55ce8c7de 100644 --- a/src/kubernetes_api_objects/spec/label_selector.rs +++ b/src/kubernetes_api_objects/spec/label_selector.rs @@ -9,8 +9,7 @@ use vstd::string::*; verus! { -/// LabelSelectorView is the ghost type of LabelSelector. -/// It is supposed to be used in spec and proof code. +// LabelSelectorView is the ghost type of LabelSelector. pub struct LabelSelectorView { pub match_labels: Option>, diff --git a/src/kubernetes_api_objects/spec/object_meta.rs b/src/kubernetes_api_objects/spec/object_meta.rs index 3e6a7b734..af448c086 100644 --- a/src/kubernetes_api_objects/spec/object_meta.rs +++ b/src/kubernetes_api_objects/spec/object_meta.rs @@ -9,8 +9,8 @@ use vstd::string::*; verus! { -/// ObjectMetaView is the ghost type of ObjectMeta. -/// It is supposed to be used in spec and proof code. +// ObjectMetaView is the ghost type of ObjectMeta. + pub struct ObjectMetaView { pub name: Option, diff --git a/src/kubernetes_api_objects/spec/owner_reference.rs b/src/kubernetes_api_objects/spec/owner_reference.rs index 68cade159..163ff93d0 100644 --- a/src/kubernetes_api_objects/spec/owner_reference.rs +++ b/src/kubernetes_api_objects/spec/owner_reference.rs @@ -9,8 +9,8 @@ use vstd::string::*; verus! { -/// OwnerReferenceView is the ghost type of OwnerReference. -/// It is supposed to be used in spec and proof code. +// OwnerReferenceView is the ghost type of OwnerReference. + pub struct OwnerReferenceView { pub block_owner_deletion: Option, diff --git a/src/kubernetes_api_objects/spec/persistent_volume_claim.rs b/src/kubernetes_api_objects/spec/persistent_volume_claim.rs index 384a61577..cdc954836 100644 --- a/src/kubernetes_api_objects/spec/persistent_volume_claim.rs +++ b/src/kubernetes_api_objects/spec/persistent_volume_claim.rs @@ -10,8 +10,8 @@ use vstd::seq_lib::*; verus! { -/// PersistentVolumeClaimView is the ghost type of PersistentVolumeClaim. -/// It is supposed to be used in spec and proof code. +// PersistentVolumeClaimView is the ghost type of PersistentVolumeClaim. + pub struct PersistentVolumeClaimView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/pod.rs b/src/kubernetes_api_objects/spec/pod.rs index cb2ef3052..e984960fc 100644 --- a/src/kubernetes_api_objects/spec/pod.rs +++ b/src/kubernetes_api_objects/spec/pod.rs @@ -12,8 +12,8 @@ use vstd::string::*; verus! { -/// PodView is the ghost type of Pod. -/// It is supposed to be used in spec and proof code. +// PodView is the ghost type of Pod. + pub struct PodView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/role.rs b/src/kubernetes_api_objects/spec/role.rs index 462b64ac4..18711328b 100644 --- a/src/kubernetes_api_objects/spec/role.rs +++ b/src/kubernetes_api_objects/spec/role.rs @@ -9,8 +9,8 @@ use vstd::seq_lib::*; verus! { -/// RoleView is the ghost type of Role. -/// It is supposed to be used in spec and proof code. +// RoleView is the ghost type of Role. + pub struct RoleView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/role_binding.rs b/src/kubernetes_api_objects/spec/role_binding.rs index 7fa24d22d..bec43a431 100644 --- a/src/kubernetes_api_objects/spec/role_binding.rs +++ b/src/kubernetes_api_objects/spec/role_binding.rs @@ -10,8 +10,8 @@ use vstd::string::*; verus! { -/// RoleBindingView is the ghost type of RoleBinding. -/// It is supposed to be used in spec and proof code. +// RoleBindingView is the ghost type of RoleBinding. + pub struct RoleBindingView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/service.rs b/src/kubernetes_api_objects/spec/service.rs index e7bcb24fb..8fb093cce 100644 --- a/src/kubernetes_api_objects/spec/service.rs +++ b/src/kubernetes_api_objects/spec/service.rs @@ -9,8 +9,8 @@ use vstd::seq_lib::*; verus! { -/// ServiceView is the ghost type of Service. -/// It is supposed to be used in spec and proof code. +// ServiceView is the ghost type of Service. + pub struct ServiceView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/service_account.rs b/src/kubernetes_api_objects/spec/service_account.rs index b766c490f..a7589a798 100644 --- a/src/kubernetes_api_objects/spec/service_account.rs +++ b/src/kubernetes_api_objects/spec/service_account.rs @@ -8,8 +8,8 @@ use vstd::prelude::*; verus! { -/// ServiceAccountView is the ghost type of ServiceAccount. -/// It is supposed to be used in spec and proof code. +// ServiceAccountView is the ghost type of ServiceAccount. + pub struct ServiceAccountView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/stateful_set.rs b/src/kubernetes_api_objects/spec/stateful_set.rs index ced2ce724..4f05da359 100644 --- a/src/kubernetes_api_objects/spec/stateful_set.rs +++ b/src/kubernetes_api_objects/spec/stateful_set.rs @@ -13,8 +13,8 @@ use vstd::string::*; verus! { -/// StatefulSetView is the ghost type of StatefulSet. -/// It is supposed to be used in spec and proof code. +// StatefulSetView is the ghost type of StatefulSet. + pub struct StatefulSetView { pub metadata: ObjectMetaView, diff --git a/src/kubernetes_api_objects/spec/toleration.rs b/src/kubernetes_api_objects/spec/toleration.rs index 91b34d9a1..081968780 100644 --- a/src/kubernetes_api_objects/spec/toleration.rs +++ b/src/kubernetes_api_objects/spec/toleration.rs @@ -8,8 +8,8 @@ use vstd::prelude::*; verus! { -/// TolerationView is the ghost type of Toleration. -/// It is supposed to be used in spec and proof code. +// TolerationView is the ghost type of Toleration. + pub struct TolerationView {} diff --git a/src/kubernetes_cluster/proof/api_server_liveness.rs b/src/kubernetes_cluster/proof/api_server_liveness.rs index e8fcdd67a..8f4d9ac4f 100644 --- a/src/kubernetes_cluster/proof/api_server_liveness.rs +++ b/src/kubernetes_cluster/proof/api_server_liveness.rs @@ -72,24 +72,24 @@ pub open spec fn no_req_before_rest_id_is_in_flight(rest_id: RestId) -> StatePre } } -/// To ensure that spec |= true ~> []every_in_fligh_message_satisfies(requirements), we only have to reason about the messages -/// created after some points. Here, "requirements" takes two parameters, the new message and the prime state. In many cases, -/// It's only related to the message. -/// -/// In detail, we have to show two things: -/// a. Newly created api request message satisfies requirements: s.in_flight(msg) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime). -/// b. The requirements, once satisfied, won't be violated as long as the message is still in flight: -/// s.in_flight(msg) /\ requirements(msg, s) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime). -/// -/// Previously, when "requirements" was irrelavant to the state, b will be sure to hold. Later, we find that "requirements" in some -/// case does need some information in the state. So we add state as another parameter and requires the caller of the lemma -/// lemma_true_leads_to_always_every_in_flight_req_msg_satisfies to prove b. is always satisfied. In order not to make those cases -/// where "requirements" has nothing to do with state more difficult, we combine a. and b. together. -/// -/// Therefore, we have the following predicate. As is easy to see, this is similar as: -/// (s.in_flight(msg) ==> requirements(msg, s)) ==> (s_prime.in_flight(msg) ==> requirements(msg, s_prime)) -/// If we think of s.in_flight(msg) ==> requirements(msg, s) as an invariant, it is the same as the proof of invariants in previous -/// proof strategy. +// To ensure that spec |= true ~> []every_in_fligh_message_satisfies(requirements), we only have to reason about the messages +// created after some points. Here, "requirements" takes two parameters, the new message and the prime state. In many cases, +// It's only related to the message. +// +// In detail, we have to show two things: +// a. Newly created api request message satisfies requirements: s.in_flight(msg) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime). +// b. The requirements, once satisfied, won't be violated as long as the message is still in flight: +// s.in_flight(msg) /\ requirements(msg, s) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime). +// +// Previously, when "requirements" was irrelavant to the state, b will be sure to hold. Later, we find that "requirements" in some +// case does need some information in the state. So we add state as another parameter and requires the caller of the lemma +// lemma_true_leads_to_always_every_in_flight_req_msg_satisfies to prove b. is always satisfied. In order not to make those cases +// where "requirements" has nothing to do with state more difficult, we combine a. and b. together. +// +// Therefore, we have the following predicate. As is easy to see, this is similar as: +// (s.in_flight(msg) ==> requirements(msg, s)) ==> (s_prime.in_flight(msg) ==> requirements(msg, s_prime)) +// If we think of s.in_flight(msg) ==> requirements(msg, s) as an invariant, it is the same as the proof of invariants in previous +// proof strategy. pub open spec fn every_new_req_msg_if_in_flight_then_satisfies(requirements: spec_fn(MsgType, Self) -> bool) -> ActionPred { |s: Self, s_prime: Self| { forall |msg: MsgType| @@ -117,13 +117,13 @@ pub open spec fn every_in_flight_req_msg_satisfies(requirements: spec_fn(MsgType } } -/// This lemma shows that if spec ensures every newly created Kubernetes api request message satisfies some requirements, -/// the system will eventually reaches a state where all Kubernetes api request messages satisfy those requirements. -/// -/// To require "every newly create Kubernetes api request message satisfies some requirements", we use a spec_fn (i.e., a closure) -/// as parameter which can be defined by callers and require spec |= [](every_new_req_msg_if_in_flight_then_satisfies(requirements)). -/// -/// The last parameter must be equivalent to every_in_flight_req_msg_satisfies(requirements) +// This lemma shows that if spec ensures every newly created Kubernetes api request message satisfies some requirements, +// the system will eventually reaches a state where all Kubernetes api request messages satisfy those requirements. +// +// To require "every newly create Kubernetes api request message satisfies some requirements", we use a spec_fn (i.e., a closure) +// as parameter which can be defined by callers and require spec |= [](every_new_req_msg_if_in_flight_then_satisfies(requirements)). +// +// The last parameter must be equivalent to every_in_flight_req_msg_satisfies(requirements) pub proof fn lemma_true_leads_to_always_every_in_flight_req_msg_satisfies(spec: TempPred, requirements: spec_fn(MsgType, Self) -> bool) requires spec.entails(always(lift_action(Self::every_new_req_msg_if_in_flight_then_satisfies(requirements)))), @@ -153,7 +153,7 @@ pub proof fn lemma_true_leads_to_always_every_in_flight_req_msg_satisfies(spec: ); } -/// This lemma is an assistant one for the previous one without rest_id. +// This lemma is an assistant one for the previous one without rest_id. pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfies_with_rest_id(spec: TempPred, requirements: spec_fn(MsgType, Self) -> bool, rest_id: nat) requires spec.entails(always(lift_action(Self::every_new_req_msg_if_in_flight_then_satisfies(requirements)))), diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs index 282a68ae7..fc2107cb4 100644 --- a/src/kubernetes_cluster/proof/builtin_controllers.rs +++ b/src/kubernetes_cluster/proof/builtin_controllers.rs @@ -19,11 +19,11 @@ verus! { impl > Cluster { -/// Everytime when we reason about update request message, we can only consider those valid ones (see validata_update_request). -/// However, listing all requirements makes spec looks cumbersome (consider using validate_create/update_request); we can only -/// list those that we need or that may appear according to the spec of system. -/// -/// For example, in some lemma we use msg.content.get_update_request().obj.kind == key.kind, so this requirement is added here. +// Everytime when we reason about update request message, we can only consider those valid ones (see validata_update_request). +// However, listing all requirements makes spec looks cumbersome (consider using validate_create/update_request); we can only +// list those that we need or that may appear according to the spec of system. +// +// For example, in some lemma we use msg.content.get_update_request().obj.kind == key.kind, so this requirement is added here. pub open spec fn every_update_msg_sets_owner_references_as( key: ObjectRef, requirements: spec_fn(Option>) -> bool ) -> StatePred { @@ -87,34 +87,34 @@ spec fn exists_delete_request_msg_in_flight_with_key(key: ObjectRef) -> StatePre } -/// This lemma is used to show that under some assumptions, the owner references of given object will eventually satisfy the -/// provided requirements (e.g., only points to the current cr's reference). We introduce this lemma because during reconciler -/// process, the reconciler only considers the object created from current cr and if so, it continues; otherwises, it returns. -/// With this lemma, we can prove that the reconciler will eventually continue the reconcile process. To use this lemma, please -/// read the explanations of all the preconditions and what each of them is for. -/// -/// This lemma requires the following preconditions: -/// 1. spec |= [](in_flight(update_msg_with(msg, key)) ==> satisfies(msg.obj.metadata.owner_references, eventual_owner_ref)). -/// 2. spec |= [](in_flight(create_msg_with(msg, key)) ==> satisfies(msg.obj.metadata.owner_references, eventual_owner_ref)). -/// 3. spec |= [](key_exists(key) ==> resource_obj_of(key) has no finalizers). -/// 4. spec |= [](!satisfies(eventual_owner_ref, key) => garbage_collector_deletion_enabled). -/// 1 is used to prove the stability; otherwise, even if the invalid object is deleted, the current system may also create an invalid -/// object or update the obejct into an invalid status. -/// In 3, no finalizers ensures the deletion will be done as long as the deleted request is received, used by -/// lemma_delete_msg_in_flight_leads_to_owner_references_satisfies. -/// 4 is quite intuitive. To reach the expected owner references state, we must ensure that if it's not expected, it satifies -/// the precondition of gc deleting it. Suppose eventual_owner_ref is owner_ref == Some(seq![o]), then the object of the given key -/// if with any other owner references, should be deleted. 4 basically limits the domain of "any other owner references". For example, -/// in rabbitmq controller, the universal set should be the set of any cr's controller owner ref that has once been in reconcile. -/// If we don't have this, suppose owner_ref == None, then the object won't be deleted. -/// -/// The proof of spec |= true ~> objects_owner_references_satisfies(eventual_owner_ref) consists of two parts: -/// 1. spec |= true ~> (object_has_invalid_owner_reference ==> delete message in flight). -/// 2. spec |= (object_has_invalid_owner_reference ==> delete message in flight) ~> all_objects_have_expected_owner_references. -/// The first is primarily obtained by the weak fairness of the builtin controllers action (specifially, the garbage collector); -/// and the second holds due to the weak fairness of kubernetes api. -/// -/// This lemma is enough for current proof, if later we introduce more complex case, we can try to strengthen it. +// This lemma is used to show that under some assumptions, the owner references of given object will eventually satisfy the +// provided requirements (e.g., only points to the current cr's reference). We introduce this lemma because during reconciler +// process, the reconciler only considers the object created from current cr and if so, it continues; otherwises, it returns. +// With this lemma, we can prove that the reconciler will eventually continue the reconcile process. To use this lemma, please +// read the explanations of all the preconditions and what each of them is for. +// +// This lemma requires the following preconditions: +// 1. spec |= [](in_flight(update_msg_with(msg, key)) ==> satisfies(msg.obj.metadata.owner_references, eventual_owner_ref)). +// 2. spec |= [](in_flight(create_msg_with(msg, key)) ==> satisfies(msg.obj.metadata.owner_references, eventual_owner_ref)). +// 3. spec |= [](key_exists(key) ==> resource_obj_of(key) has no finalizers). +// 4. spec |= [](!satisfies(eventual_owner_ref, key) => garbage_collector_deletion_enabled). +// 1 is used to prove the stability; otherwise, even if the invalid object is deleted, the current system may also create an invalid +// object or update the obejct into an invalid status. +// In 3, no finalizers ensures the deletion will be done as long as the deleted request is received, used by +// lemma_delete_msg_in_flight_leads_to_owner_references_satisfies. +// 4 is quite intuitive. To reach the expected owner references state, we must ensure that if it's not expected, it satifies +// the precondition of gc deleting it. Suppose eventual_owner_ref is owner_ref == Some(seq![o]), then the object of the given key +// if with any other owner references, should be deleted. 4 basically limits the domain of "any other owner references". For example, +// in rabbitmq controller, the universal set should be the set of any cr's controller owner ref that has once been in reconcile. +// If we don't have this, suppose owner_ref == None, then the object won't be deleted. +// +// The proof of spec |= true ~> objects_owner_references_satisfies(eventual_owner_ref) consists of two parts: +// 1. spec |= true ~> (object_has_invalid_owner_reference ==> delete message in flight). +// 2. spec |= (object_has_invalid_owner_reference ==> delete message in flight) ~> all_objects_have_expected_owner_references. +// The first is primarily obtained by the weak fairness of the builtin controllers action (specifially, the garbage collector); +// and the second holds due to the weak fairness of kubernetes api. +// +// This lemma is enough for current proof, if later we introduce more complex case, we can try to strengthen it. pub proof fn lemma_eventually_objects_owner_references_satisfies( spec: TempPred, key: ObjectRef, eventual_owner_ref: spec_fn(Option>) -> bool ) diff --git a/src/kubernetes_cluster/proof/cluster.rs b/src/kubernetes_cluster/proof/cluster.rs index 2283ba7e5..9036b859d 100644 --- a/src/kubernetes_cluster/proof/cluster.rs +++ b/src/kubernetes_cluster/proof/cluster.rs @@ -28,7 +28,7 @@ verus! { impl > Cluster { -/// Prove weak_fairness is stable. +// Prove weak_fairness is stable. pub proof fn action_weak_fairness_is_stable(action: Action) ensures valid(stable(action.weak_fairness(()))), @@ -37,7 +37,7 @@ pub proof fn action_weak_fairness_is_stable(action: Action(split_always); } -/// Prove weak_fairness for all input is stable. +// Prove weak_fairness for all input is stable. pub proof fn tla_forall_action_weak_fairness_is_stable( action: Action ) diff --git a/src/kubernetes_cluster/proof/daemon_set_controller.rs b/src/kubernetes_cluster/proof/daemon_set_controller.rs index ec75bee05..3302b18d2 100644 --- a/src/kubernetes_cluster/proof/daemon_set_controller.rs +++ b/src/kubernetes_cluster/proof/daemon_set_controller.rs @@ -79,8 +79,8 @@ pub open spec fn daemon_set_not_exist_or_updated_or_no_more_status_from_bc( } } -/// This lemma is very similar to lemma_true_leads_to_always_stateful_set_not_exist_or_updated_or_no_more_pending_req -/// but does not consider the dependency on a configmap('s rv) +// This lemma is very similar to lemma_true_leads_to_always_stateful_set_not_exist_or_updated_or_no_more_pending_req +// but does not consider the dependency on a configmap('s rv) pub proof fn lemma_true_leads_to_always_daemon_set_not_exist_or_updated_or_no_more_pending_req(spec: TempPred, key: ObjectRef, make_fn: spec_fn() -> DaemonSetView) requires diff --git a/src/kubernetes_cluster/proof/stateful_set_controller.rs b/src/kubernetes_cluster/proof/stateful_set_controller.rs index a9e60055b..ed50b2bee 100644 --- a/src/kubernetes_cluster/proof/stateful_set_controller.rs +++ b/src/kubernetes_cluster/proof/stateful_set_controller.rs @@ -102,29 +102,29 @@ pub open spec fn stateful_set_not_exist_or_updated_or_no_more_status_from_bc( } } -/// This lemma shows that for a given object (identified by the key) if -/// (1) all the create request for this object will create an object which is the same as make_fn -/// (2) all the update request for this object will update this object to match the result of make_fn, -/// then eventually it will reach a state where it is always true that -/// (1) the object does not exist, -/// (2) or the object exists and matches the result of make_fn, -/// (3) or there is no update-status request from the built-in controllers for this object in the network. -/// -/// This lemma is used to help prove that the custom controller eventually updates the object -/// to the desired state even with potential race from other built-in controllers, -/// such as the stateful set controller or daemon set controller. -/// -/// Such race condition makes the liveness proof harder because if the controller loses the race -/// and the built-in controller first updates the object, the controller's update will fail due -/// to the conflict error caused by resource version checking. -/// Note that liveness is still possible here since the built-in controller eventually stops -/// sending update-status request of an object (thanks to the stabilizer) before the next update to the same -/// object from the custom controller. -/// -/// This lemma basically shows us why liveness is still possible here: if the create/update from the custom -/// controller ever gets handled, then the object is already in the desired state; otherwise eventually -/// the object becomes stable and all update-status requests are gone, so later the request from the custom -/// controller can directly go through. +// This lemma shows that for a given object (identified by the key) if +// (1) all the create request for this object will create an object which is the same as make_fn +// (2) all the update request for this object will update this object to match the result of make_fn, +// then eventually it will reach a state where it is always true that +// (1) the object does not exist, +// (2) or the object exists and matches the result of make_fn, +// (3) or there is no update-status request from the built-in controllers for this object in the network. +// +// This lemma is used to help prove that the custom controller eventually updates the object +// to the desired state even with potential race from other built-in controllers, +// such as the stateful set controller or daemon set controller. +// +// Such race condition makes the liveness proof harder because if the controller loses the race +// and the built-in controller first updates the object, the controller's update will fail due +// to the conflict error caused by resource version checking. +// Note that liveness is still possible here since the built-in controller eventually stops +// sending update-status request of an object (thanks to the stabilizer) before the next update to the same +// object from the custom controller. +// +// This lemma basically shows us why liveness is still possible here: if the create/update from the custom +// controller ever gets handled, then the object is already in the desired state; otherwise eventually +// the object becomes stable and all update-status requests are gone, so later the request from the custom +// controller can directly go through. pub proof fn lemma_true_leads_to_always_stateful_set_not_exist_or_updated_or_no_more_pending_req( spec: TempPred, key: ObjectRef, cm_key: ObjectRef, make_fn: spec_fn(rv: StringView) -> StatefulSetView diff --git a/src/kubernetes_cluster/proof/validation_rule.rs b/src/kubernetes_cluster/proof/validation_rule.rs index 9c596a0c9..c30575500 100644 --- a/src/kubernetes_cluster/proof/validation_rule.rs +++ b/src/kubernetes_cluster/proof/validation_rule.rs @@ -29,18 +29,18 @@ pub open spec fn marshal_preserves_status() -> bool { ==> K::unmarshal_status(d.status).get_Ok_0() == K::unmarshal(d).get_Ok_0().status() } -/// The relexitivity allows the metadata to be different. +// The relexitivity allows the metadata to be different. pub open spec fn transition_validation_is_reflexive_and_transitive() -> bool { &&& forall |x: K, y: K| (x.spec() == y.spec() && x.status() == y.status()) ==> #[trigger] K::transition_validation(x, y) &&& forall |x: K, y: K, z: K| #![trigger K::transition_validation(x, y), K::transition_validation(y, z)] K::transition_validation(x, y) && K::transition_validation(y, z) ==> K::transition_validation(x, z) } -/// This spec and also this module are targeted at the relations of the three versions of custom resource object. We know that -/// if cr is updated, the old and new object are subject to the transition rule (if any). Since scheduled_cr and triggering_cr -/// are derived from the cr in etcd, they are either equal to or satisfy the transition rule with etcd cr. -/// -/// When the transition rule is transitive, we can determine a linear order of the three custom resource objects. +// This spec and also this module are targeted at the relations of the three versions of custom resource object. We know that +// if cr is updated, the old and new object are subject to the transition rule (if any). Since scheduled_cr and triggering_cr +// are derived from the cr in etcd, they are either equal to or satisfy the transition rule with etcd cr. +// +// When the transition rule is transitive, we can determine a linear order of the three custom resource objects. pub open spec fn transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(cr: K) -> StatePred { |s: Self| { Self::transition_rule_applies_to_etcd_and_scheduled_cr(cr)(s) diff --git a/src/kubernetes_cluster/spec/cluster.rs b/src/kubernetes_cluster/spec/cluster.rs index 3488e16dd..cfade6e2f 100644 --- a/src/kubernetes_cluster/spec/cluster.rs +++ b/src/kubernetes_cluster/spec/cluster.rs @@ -17,15 +17,15 @@ use vstd::{multiset::*, prelude::*}; verus! { -/// The Cluster struct is an abstraction of the compound state machine of the kubernetes cluster. It contains a number of -/// fields for describing the state of those components as well as all the methods of the specifications and lemmas of the -/// system. -/// -/// It takes three generics, which should be essentially one: R is the type of Reconciler and K and E are the two generics -/// fed to R. -/// -/// By using such a struct, we don't have to let all the functions carry the generics; and therefore we don't need to -/// specify the generics whenever calling those spec or proof functions. +// The Cluster struct is an abstraction of the compound state machine of the kubernetes cluster. It contains a number of +// fields for describing the state of those components as well as all the methods of the specifications and lemmas of the +// system. +// +// It takes three generics, which should be essentially one: R is the type of Reconciler and K and E are the two generics +// fed to R. +// +// By using such a struct, we don't have to let all the functions carry the generics; and therefore we don't need to +// specify the generics whenever calling those spec or proof functions. pub struct Cluster> { pub kubernetes_api_state: ApiServerState, pub controller_state: ControllerState, diff --git a/src/kubernetes_cluster/spec/cluster_state_machine.rs b/src/kubernetes_cluster/spec/cluster_state_machine.rs index e4c0613bd..9b9ada28c 100644 --- a/src/kubernetes_cluster/spec/cluster_state_machine.rs +++ b/src/kubernetes_cluster/spec/cluster_state_machine.rs @@ -15,8 +15,8 @@ use crate::kubernetes_cluster::spec::{ ControllerAction, ControllerActionInput, ControllerState, OngoingReconcile, }, external_api::types::{ExternalAPIAction, ExternalAPIActionInput}, - pod_event::types::{PodEventActionInput, PodEventState}, message::*, + pod_event::types::{PodEventActionInput, PodEventState}, }; use crate::reconciler::spec::reconciler::Reconciler; use crate::state_machine::{action::*, state_machine::*}; @@ -59,11 +59,11 @@ pub open spec fn init() -> StatePred { } } -/// kubernetes_api_next models the behavior that the Kubernetes API server (and its backend, a key-value store) -/// handles one request from some client or controller that gets/lists/creates/updates/deletes some object(s). -/// Handling each create/update/delete request will potentially change the objects stored in the key-value store -/// (etcd by default). -/// The persistent state stored in the key-value store is modeled as a Map. +// kubernetes_api_next models the behavior that the Kubernetes API server (and its backend, a key-value store) +// handles one request from some client or controller that gets/lists/creates/updates/deletes some object(s). +// Handling each create/update/delete request will potentially change the objects stored in the key-value store +// (etcd by default). +// The persistent state stored in the key-value store is modeled as a Map. pub open spec fn kubernetes_api_next() -> Action>, ()> { let result = |input: Option>, s: Self| { let host_result = Self::kubernetes_api().next_result( @@ -95,10 +95,10 @@ pub open spec fn kubernetes_api_next() -> Action>, ()> { } } -/// builtin_controllers_next models the behavior that one of the built-in controllers reconciles one object. -/// The cluster state machine chooses which built-in controller to run and which object to reconcile. -/// The behavior of each built-in controller is modeled as a function that takes the current cluster state -/// (objects stored in the key-value store) and returns request(s) to update the cluster state. +// builtin_controllers_next models the behavior that one of the built-in controllers reconciles one object. +// The cluster state machine chooses which built-in controller to run and which object to reconcile. +// The behavior of each built-in controller is modeled as a function that takes the current cluster state +// (objects stored in the key-value store) and returns request(s) to update the cluster state. pub open spec fn builtin_controllers_next() -> Action { let result = |input: (BuiltinControllerChoice, ObjectRef), s: Self| { let host_result = Self::builtin_controllers().next_result( @@ -134,10 +134,10 @@ pub open spec fn builtin_controllers_next() -> Action Action>, ()> { let result = |input: Option>, s: Self| { let host_result = Self::external_api().next_result( @@ -204,26 +204,26 @@ pub open spec fn controller_next() -> Action>, Option Action { Action { precondition: |input: ObjectRef, s: Self| { @@ -243,7 +243,7 @@ pub open spec fn schedule_controller_reconcile() -> Action } } -/// This action restarts the crashed controller. +// This action restarts the crashed controller. pub open spec fn restart_controller() -> Action { Action { precondition: |input: (), s: Self| { @@ -258,9 +258,9 @@ pub open spec fn restart_controller() -> Action { } } -/// This action disallows the controller to crash from this point. -/// This is used to constraint the crash behavior for liveness proof: -/// the controller eventually stops crashing. +// This action disallows the controller to crash from this point. +// This is used to constraint the crash behavior for liveness proof: +// the controller eventually stops crashing. pub open spec fn disable_crash() -> Action { Action { precondition: |input: (), s: Self| { @@ -275,8 +275,8 @@ pub open spec fn disable_crash() -> Action { } } -/// This action fails a request sent to the Kubernetes API in a transient way: -/// the request fails with timeout error or conflict error (caused by resource version conflicts). +// This action fails a request sent to the Kubernetes API in a transient way: +// the request fails with timeout error or conflict error (caused by resource version conflicts). pub open spec fn fail_request_transiently() -> Action, APIError), ()> { let result = |input: (MsgType, APIError), s: Self| { let req_msg = input.0; @@ -308,9 +308,9 @@ pub open spec fn fail_request_transiently() -> Action, APIErro } } -/// This action disallows the Kubernetes API to have transient failure from this point. -/// This is used to constraint the transient error of Kubernetes APIs for liveness proof: -/// the requests from the controller eventually stop being rejected by transient error. +// This action disallows the Kubernetes API to have transient failure from this point. +// This is used to constraint the transient error of Kubernetes APIs for liveness proof: +// the requests from the controller eventually stop being rejected by transient error. pub open spec fn disable_transient_failure() -> Action { Action { precondition: |input:(), s: Self| { @@ -431,9 +431,9 @@ pub open spec fn next_step(s: Self, s_prime: Self, step: Step>) -> bo } } -/// `next` chooses: -/// * which host to take the next action (`Step`) -/// * what input to feed to the chosen action +// `next` chooses: +// * which host to take the next action (`Step`) +// * what input to feed to the chosen action pub open spec fn next() -> ActionPred { |s: Self, s_prime: Self| exists |step: Step>| Self::next_step(s, s_prime, step) } diff --git a/src/reconciler/spec/reconciler.rs b/src/reconciler/spec/reconciler.rs index 8ae3d57bf..29d5b1e85 100644 --- a/src/reconciler/spec/reconciler.rs +++ b/src/reconciler/spec/reconciler.rs @@ -9,8 +9,8 @@ use vstd::prelude::*; verus! { -/// Reconciler is the key data structure we use to pack up all the custom controller-specific logic -/// and install it to the Kubernetes cluster state machine +// Reconciler is the key data structure we use to pack up all the custom controller-specific logic +// and install it to the Kubernetes cluster state machine #[verifier(reject_recursive_types(K))] #[verifier(reject_recursive_types(ExternalAPIType))] pub trait Reconciler: Sized { diff --git a/src/state_machine/action.rs b/src/state_machine/action.rs index 1a67b380d..c61830a51 100644 --- a/src/state_machine/action.rs +++ b/src/state_machine/action.rs @@ -11,10 +11,10 @@ verus! { #[verifier(reject_recursive_types(Input))] #[verifier(reject_recursive_types(Output))] pub struct Action { - /// The condition that enables the host action. + // The condition that enables the host action. pub precondition: spec_fn(Input, State) -> bool, - /// The new internal state and output made by the transition. + // The new internal state and output made by the transition. pub transition: spec_fn(Input, State) -> (State, Output), } @@ -30,13 +30,13 @@ impl Action { } } - /// `weak_fairness` assumption says that, - /// it is always true that, if `pre` is always true, `forward` eventually becomes true + // `weak_fairness` assumption says that, + // it is always true that, if `pre` is always true, `forward` eventually becomes true pub open spec fn weak_fairness(self, input: Input) -> TempPred { always(lift_state(self.pre(input))).leads_to(lift_action(self.forward(input))) } - /// `wf1` is a specialized version of temporal_logic_rules::wf1 for Action + // `wf1` is a specialized version of temporal_logic_rules::wf1 for Action pub proof fn wf1(self, input: Input, spec: TempPred, next: ActionPred, pre: StatePred, post: StatePred) requires forall |s, s_prime: State| pre(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime), diff --git a/src/state_machine/state_machine.rs b/src/state_machine/state_machine.rs index e4b4c8315..a21f5a267 100644 --- a/src/state_machine/state_machine.rs +++ b/src/state_machine/state_machine.rs @@ -7,39 +7,39 @@ use vstd::{multiset::*, prelude::*}; verus! { -/// `StateMachine` helps to write host state machines in a disciplined way -/// by explicitly writing `init`, `actions`, `step_to_action`, and `action_input`. -/// -/// It takes four generic types: -/// * `State`: The (internal) state of the host. -/// * `Input`: The input from the external world of the state machine. For example a message. -/// * `ActionInput`: The input to feed to the action. It might be a compound of `Input` and other types. -/// * `Output`: The output to send to the external world of the state machine. For example a set of messages. -/// * `Step`: The step binding variable that the state machine chooses to decide the action. +// `StateMachine` helps to write host state machines in a disciplined way +// by explicitly writing `init`, `actions`, `step_to_action`, and `action_input`. +// +// It takes four generic types: +// * `State`: The (internal) state of the host. +// * `Input`: The input from the external world of the state machine. For example a message. +// * `ActionInput`: The input to feed to the action. It might be a compound of `Input` and other types. +// * `Output`: The output to send to the external world of the state machine. For example a set of messages. +// * `Step`: The step binding variable that the state machine chooses to decide the action. #[verifier(reject_recursive_types(State))] #[verifier(reject_recursive_types(Input))] #[verifier(reject_recursive_types(ActionInput))] #[verifier(reject_recursive_types(Output))] #[verifier(reject_recursive_types(Step))] pub struct StateMachine { - /// Check if it is the initial internal state. + // Check if it is the initial internal state. pub init: spec_fn(State) -> bool, - /// The set of actions the state machine can take. + // The set of actions the state machine can take. pub actions: Set>, - /// Return the corresponding action of the binding step. + // Return the corresponding action of the binding step. pub step_to_action: spec_fn(Step) -> Action, - /// Return the input to the host action. + // Return the input to the host action. pub action_input: spec_fn(Step, Input) -> ActionInput, } impl StateMachine { - /// `next_result` is the interface that the host state machine exposes to the compound state machine. - /// It returns whether there exists an action that is enabled by input and s. - /// If exists, it also returns the new state and output generated by the action. + // `next_result` is the interface that the host state machine exposes to the compound state machine. + // It returns whether there exists an action that is enabled by input and s. + // If exists, it also returns the new state and output generated by the action. pub open spec fn next_result(self, input: Input, s: State) -> ActionResult { if exists |step| (#[trigger] (self.step_to_action)(step).precondition)((self.action_input)(step, input), s) { let witness_step = choose |step| (#[trigger] (self.step_to_action)(step).precondition)((self.action_input)(step, input), s); @@ -51,8 +51,8 @@ impl StateMachine, action_input: ActionInput, s: State) -> ActionResult { if (action.precondition)(action_input, s) { ActionResult::Enabled((action.transition)(action_input, s).0, (action.transition)(action_input, s).1) @@ -62,22 +62,22 @@ impl StateMachine { - /// Check if it is the initial internal state. + // Check if it is the initial internal state. pub init: spec_fn(State) -> bool, - /// The deliver action that (1) sends zero or one message to a host and (2) takes any number of messages from a host. + // The deliver action that (1) sends zero or one message to a host and (2) takes any number of messages from a host. pub deliver: Action, } impl NetworkStateMachine { - /// `next_result` is the interface that the network state machine exposes to the compound state machine. - /// It returns whether deliver is enabled or not, and the new internal state if deliver is enabled. + // `next_result` is the interface that the network state machine exposes to the compound state machine. + // It returns whether deliver is enabled or not, and the new internal state if deliver is enabled. pub open spec fn next_result(self, msg_ops: MessageOps, s: State) -> ActionResult { if (self.deliver.precondition)(msg_ops, s) { ActionResult::Enabled((self.deliver.transition)(msg_ops, s).0, (self.deliver.transition)(msg_ops, s).1) diff --git a/src/temporal_logic/defs.rs b/src/temporal_logic/defs.rs index dfbf7a2af..fb55cb465 100644 --- a/src/temporal_logic/defs.rs +++ b/src/temporal_logic/defs.rs @@ -46,33 +46,33 @@ impl TempPred { (self.pred)(execution) } - /// We specify all infix operators for temporal logic as TempPred methods to aid readability + // We specify all infix operators for temporal logic as TempPred methods to aid readability - /// `/\` for temporal predicates in TLA+ (i.e., `&&` in Verus). + // `/\` for temporal predicates in TLA+ (i.e., `&&` in Verus). pub open spec fn and(self, other: Self) -> Self { TempPred::new(|ex: Execution| self.satisfied_by(ex) && other.satisfied_by(ex)) } - /// `\/` for temporal predicates in TLA+ (i.e., `||` in Verus). + // `\/` for temporal predicates in TLA+ (i.e., `||` in Verus). pub open spec fn or(self, other: Self) -> Self { TempPred::new(|ex: Execution| self.satisfied_by(ex) || other.satisfied_by(ex)) } - /// `=>` for temporal predicates in TLA+ (i.e., `==>` in Verus). + // `=>` for temporal predicates in TLA+ (i.e., `==>` in Verus). pub open spec fn implies(self, other: Self) -> Self { TempPred::new(|ex: Execution| self.satisfied_by(ex) ==> other.satisfied_by(ex)) } - /// `~>` for temporal predicates in TLA+. - /// Returns a temporal predicate that is satisfied - /// iff it is always the case that `self` getting satisfied implies `other` eventually getting satisfied. - /// - /// Defined in 3.2.3. + // `~>` for temporal predicates in TLA+. + // Returns a temporal predicate that is satisfied + // iff it is always the case that `self` getting satisfied implies `other` eventually getting satisfied. + // + // Defined in 3.2.3. pub open spec fn leads_to(self, other: Self) -> Self { always(self.implies(eventually(other))) } - /// `|=` for temporal predicates in TLA+. + // `|=` for temporal predicates in TLA+. pub open spec fn entails(self, other: Self) -> bool { valid(self.implies(other)) } @@ -90,39 +90,39 @@ pub open spec fn lift_action(action_pred: ActionPred) -> TempPred { TempPred::new(|ex: Execution| action_pred(ex.head(), ex.head_next())) } -/// `[]` for temporal predicates in TLA+. -/// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on every suffix of the execution. -/// -/// Defined in 3.1. +// `[]` for temporal predicates in TLA+. +// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on every suffix of the execution. +// +// Defined in 3.1. pub open spec fn always(temp_pred: TempPred) -> TempPred { TempPred::new(|ex: Execution| forall |i: nat| #[trigger] temp_pred.satisfied_by(ex.suffix(i))) } -/// `<>` for temporal predicates in TLA+. -/// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on at least one suffix of the execution. -/// -/// Defined in 3.2.1. +// `<>` for temporal predicates in TLA+. +// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on at least one suffix of the execution. +// +// Defined in 3.2.1. pub open spec fn eventually(temp_pred: TempPred) -> TempPred { TempPred::new(|ex: Execution| exists |i: nat| #[trigger] temp_pred.satisfied_by(ex.suffix(i))) } -/// `'` (prime) for temporal predicates in TLA+. -/// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on the suffix execution starting from the next state. +// `'` (prime) for temporal predicates in TLA+. +// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on the suffix execution starting from the next state. pub open spec fn later(temp_pred: TempPred) -> TempPred { TempPred::new(|ex: Execution| temp_pred.satisfied_by(ex.suffix(1))) } -/// `~` for temporal predicates in TLA+ (i.e., `!` in Verus). +// `~` for temporal predicates in TLA+ (i.e., `!` in Verus). pub open spec fn not(temp_pred: TempPred) -> TempPred { TempPred::new(|ex: Execution| !temp_pred.satisfied_by(ex)) } -/// `\A` for temporal predicates in TLA+ (i.e., `forall` in Verus). +// `\A` for temporal predicates in TLA+ (i.e., `forall` in Verus). pub open spec fn tla_forall(a_to_temp_pred: spec_fn(A) -> TempPred) -> TempPred { TempPred::new(|ex: Execution| forall |a: A| #[trigger] a_to_temp_pred(a).satisfied_by(ex)) } -/// `\E` for temporal predicates in TLA+ (i.e., `exists` in Verus). +// `\E` for temporal predicates in TLA+ (i.e., `exists` in Verus). pub open spec fn tla_exists(a_to_temp_pred: spec_fn(A) -> TempPred) -> TempPred { TempPred::new(|ex: Execution| exists |a: A| #[trigger] a_to_temp_pred(a).satisfied_by(ex)) } @@ -131,39 +131,39 @@ pub open spec fn stable(temp_pred: TempPred) -> TempPred { TempPred::new(|ex: Execution| temp_pred.implies(always(temp_pred)).satisfied_by(ex)) } -/// Returns a state predicate that is satisfied -/// iff `action_pred` can be satisfied by any possible following state and the current state -/// -/// enabled() is used for checking whether a particular action is enabled at this **state** -/// -/// Note: it says whether the action *can possibly* happen, rather than whether the action *actually does* happen! +// Returns a state predicate that is satisfied +// iff `action_pred` can be satisfied by any possible following state and the current state +// +// enabled() is used for checking whether a particular action is enabled at this **state** +// +// Note: it says whether the action *can possibly* happen, rather than whether the action *actually does* happen! pub open spec fn enabled(action_pred: ActionPred) -> StatePred { |s: T| exists |s_prime: T| #[trigger] action_pred(s, s_prime) } -/// Returns a temporal predicate that is satisfied -/// iff `always(lift_state(enabled(action_pred)))` getting satisfied leads to `lift_action(action_pred)` getting satisfied. -/// -/// It says whether it is *always* the case that if the action is *always* enabled, the action *eventually* happens. -/// -/// Defined in 5.3 in a different form. -/// We can prove the two forms are the same: -/// []E(A) ~> A -/// == []([]E(A) => <>A) -/// == [](~[]E(A) \/ <>A) -/// == [](~~<>~E(A) \/ <>A) <--- apply always_to_eventually -/// == [](<>~E(A) \/ <>A) -/// == []<>(~E(A) \/ A) <--- apply eventually_or -/// == []<>~E(A) \/ []<>A <--- apply always_eventually_distrib -/// == []<>A \/ []<>~E(A) +// Returns a temporal predicate that is satisfied +// iff `always(lift_state(enabled(action_pred)))` getting satisfied leads to `lift_action(action_pred)` getting satisfied. +// +// It says whether it is *always* the case that if the action is *always* enabled, the action *eventually* happens. +// +// Defined in 5.3 in a different form. +// We can prove the two forms are the same: +// []E(A) ~> A +// == []([]E(A) => <>A) +// == [](~[]E(A) \/ <>A) +// == [](~~<>~E(A) \/ <>A) <--- apply always_to_eventually +// == [](<>~E(A) \/ <>A) +// == []<>(~E(A) \/ A) <--- apply eventually_or +// == []<>~E(A) \/ []<>A <--- apply always_eventually_distrib +// == []<>A \/ []<>~E(A) pub open spec fn weak_fairness(action_pred: ActionPred) -> TempPred { always(lift_state(enabled(action_pred))).leads_to(lift_action(action_pred)) } -/// `|=` for temporal predicates in TLA+. -/// Returns true iff `temp_pred` is satisfied by all possible executions (behaviors). -/// -/// Defined in 3.3. +// `|=` for temporal predicates in TLA+. +// Returns true iff `temp_pred` is satisfied by all possible executions (behaviors). +// +// Defined in 3.3. pub open spec fn valid(temp_pred: TempPred) -> bool { forall |ex: Execution| temp_pred.satisfied_by(ex) } diff --git a/src/temporal_logic/rules.rs b/src/temporal_logic/rules.rs index 07d26bb9c..9c156cab9 100644 --- a/src/temporal_logic/rules.rs +++ b/src/temporal_logic/rules.rs @@ -305,8 +305,8 @@ proof fn instantiate_entailed_leads_to(ex: Execution, i: nat, spec: TempPr leads_to_unfold::(ex, p, q); } -/// All the lemmas above are used internally for proving the lemmas below -/// The following lemmas are used by developers to simplify liveness/safety proof +// All the lemmas above are used internally for proving the lemmas below +// The following lemmas are used by developers to simplify liveness/safety proof pub proof fn always_implies_to_leads_to(spec: TempPred, p: TempPred, q: TempPred) requires spec.entails(always(p.implies(q))), @@ -452,9 +452,9 @@ proof fn tla_exists_equality(f: spec_fn(A, T) -> bool) temp_pred_equality::(p, q); } -/// Lift the "always" outside tla_forall if the function is previously wrapped by an "always" -/// Note: Verus may not able to infer that (|a| func(a))(a) equals func(a). -/// Please turn to lemma tla_forall_always_equality_variant for troubleshooting. +// Lift the "always" outside tla_forall if the function is previously wrapped by an "always" +// Note: Verus may not able to infer that (|a| func(a))(a) equals func(a). +// Please turn to lemma tla_forall_always_equality_variant for troubleshooting. pub proof fn tla_forall_always_equality(a_to_p: spec_fn(A) -> TempPred) ensures tla_forall(|a: A| always(a_to_p(a))) == always(tla_forall(a_to_p)), { @@ -678,7 +678,7 @@ pub proof fn leads_to_exists_intro(spec: TempPred, a_to_p: spec_fn(A) - }; } -/// This lemmas instantiates tla_forall for a. +// This lemmas instantiates tla_forall for a. pub proof fn use_tla_forall(spec: TempPred, a_to_p: spec_fn(A) -> TempPred, a: A) requires spec.entails(tla_forall(a_to_p)), ensures spec.entails(a_to_p(a)), @@ -689,9 +689,9 @@ pub proof fn use_tla_forall(spec: TempPred, a_to_p: spec_fn(A) -> TempP }; } -/// Obviously p ~> p is valid -/// post: -/// |= p ~> p +// Obviously p ~> p is valid +// post: +// |= p ~> p pub proof fn leads_to_self_temp(p: TempPred) ensures valid(p.leads_to(p)), { @@ -703,11 +703,11 @@ pub proof fn leads_to_self_temp(p: TempPred) }; } -/// Entails p if entails always p -/// pre: -/// spec |= []p -/// post: -/// spec |= p +// Entails p if entails always p +// pre: +// spec |= []p +// post: +// spec |= p pub proof fn eliminate_always(spec: TempPred, p: TempPred) requires spec.entails(always(p)), ensures spec.entails(p), @@ -718,12 +718,12 @@ pub proof fn eliminate_always(spec: TempPred, p: TempPred) } } -/// Entails p and q if entails each of them. -/// pre: -/// spec |= p -/// spec |= q -/// post: -/// spec |= p && q +// Entails p and q if entails each of them. +// pre: +// spec |= p +// spec |= q +// post: +// spec |= p && q pub proof fn entails_and_temp(spec: TempPred, p: TempPred, q: TempPred) requires spec.entails(p), @@ -736,16 +736,16 @@ pub proof fn entails_and_temp(spec: TempPred, p: TempPred, q: TempPred< }; } -/// Entails the conjunction of all the p if entails each of them. -/// pre: -/// spec |= p1 -/// spec |= p2 -/// ... -/// spec |= pn -/// post: -/// spec |= p1 /\ p2 /\ ... /\ pn -/// -/// Usage: entails_and_n!(spec, p1, p2, p3, p4) +// Entails the conjunction of all the p if entails each of them. +// pre: +// spec |= p1 +// spec |= p2 +// ... +// spec |= pn +// post: +// spec |= p1 /\ p2 /\ ... /\ pn +// +// Usage: entails_and_n!(spec, p1, p2, p3, p4) #[macro_export] macro_rules! entails_and_n { [$($tail:tt)*] => { @@ -767,16 +767,16 @@ macro_rules! entails_and_n_internal { pub use entails_and_n; pub use entails_and_n_internal; -/// Entails always the conjunction of all the p if entails each always p. -/// pre: -/// spec |= []p1 -/// spec |= []p2 -/// ... -/// spec |= []pn -/// post: -/// spec |= [](p1 /\ p2 /\ ... /\ pn) -/// -/// Usage: entails_always_and_n!(spec, p1, p2, p3, p4) +// Entails always the conjunction of all the p if entails each always p. +// pre: +// spec |= []p1 +// spec |= []p2 +// ... +// spec |= []pn +// post: +// spec |= [](p1 /\ p2 /\ ... /\ pn) +// +// Usage: entails_always_and_n!(spec, p1, p2, p3, p4) #[macro_export] macro_rules! entails_always_and_n { [$($tail:tt)*] => { @@ -801,12 +801,12 @@ macro_rules! entails_always_and_n_internal { pub use entails_always_and_n; pub use entails_always_and_n_internal; -/// Merge the next and other state predicates together into one action predicate. -/// Usage: -/// Given next, p1, p2, p3, ..., -/// returns |s, s_prime| next(s, s_prime) && p1(s) && p2(s) && p3(s) && ... -/// -/// Note: Verus reports strange errors saying the returned closure is not a spec_fn +// Merge the next and other state predicates together into one action predicate. +// Usage: +// Given next, p1, p2, p3, ..., +// returns |s, s_prime| next(s, s_prime) && p1(s) && p2(s) && p3(s) && ... +// +// Note: Verus reports strange errors saying the returned closure is not a spec_fn #[macro_export] macro_rules! merge_into_next { [$($tail:tt)*] => { @@ -830,10 +830,10 @@ macro_rules! merge_into_next_internal { pub use merge_into_next; pub use merge_into_next_internal; -/// Combine the temporal predicates together using and. -/// Usage: -/// Given next, p1, p2, p3, ..., -/// returns next.and(p1).and(p2).and(p3)... +// Combine the temporal predicates together using and. +// Usage: +// Given next, p1, p2, p3, ..., +// returns next.and(p1).and(p2).and(p3)... #[macro_export] macro_rules! combine_with_next { [$($tail:tt)*] => { @@ -856,17 +856,17 @@ macro_rules! combine_with_next_internal { pub use combine_with_next; pub use combine_with_next_internal; -/// Strengthen next with arbitrary number of predicates. -/// pre: -/// spec |= []p1 -/// spec |= []p2 -/// ... -/// spec |= []pn -/// p1 /\ p2 /\ ... /\ pn ==> partial_spec -/// post: -/// spec |= []all -/// -/// Usage: combine_spec_entails_always_n!(spec, partial_spec, p1, p2, p3, p4) +// Strengthen next with arbitrary number of predicates. +// pre: +// spec |= []p1 +// spec |= []p2 +// ... +// spec |= []pn +// p1 /\ p2 /\ ... /\ pn ==> partial_spec +// post: +// spec |= []all +// +// Usage: combine_spec_entails_always_n!(spec, partial_spec, p1, p2, p3, p4) #[macro_export] macro_rules! combine_spec_entails_always_n { [$($tail:tt)*] => { @@ -891,18 +891,18 @@ macro_rules! combine_spec_entails_always_n_internal { pub use combine_spec_entails_always_n; pub use combine_spec_entails_always_n_internal; -/// Show that an spec entails the invariant by a group of action/state predicates which are also invariants entailed by spec. -/// pre: -/// partial_spec |= inv -/// spec |= []p1 -/// spec |= []p2 -/// ... -/// spec |= []pn -/// p1 /\ p2 /\ ... /\ pn ==> partial_spec -/// post: -/// spec |= []inv -/// -/// Usage: invariant_n!(spec, partial_spec, inv, p1, p2, ..., pn) +// Show that an spec entails the invariant by a group of action/state predicates which are also invariants entailed by spec. +// pre: +// partial_spec |= inv +// spec |= []p1 +// spec |= []p2 +// ... +// spec |= []pn +// p1 /\ p2 /\ ... /\ pn ==> partial_spec +// post: +// spec |= []inv +// +// Usage: invariant_n!(spec, partial_spec, inv, p1, p2, ..., pn) #[macro_export] macro_rules! invariant_n { [$($tail:tt)*] => { @@ -929,12 +929,12 @@ macro_rules! invariant_n_internal { pub use invariant_n; pub use invariant_n_internal; -/// Combining two specs together entails p and q if each of them entails p, q respectively. -/// pre: -/// spec1 |= p -/// spec2 |= q -/// post: -/// spec1 /\ spec2 |= p /\ q +// Combining two specs together entails p and q if each of them entails p, q respectively. +// pre: +// spec1 |= p +// spec2 |= q +// post: +// spec1 /\ spec2 |= p /\ q pub proof fn entails_and_different_temp(spec1: TempPred, spec2: TempPred, p: TempPred, q: TempPred) requires spec1.entails(p), @@ -947,9 +947,9 @@ pub proof fn entails_and_different_temp(spec1: TempPred, spec2: TempPred(p: TempPred) ensures valid(stable(always(p))), { @@ -960,9 +960,9 @@ pub proof fn always_p_is_stable(p: TempPred) } } -/// A leads-to predicate is stable. -/// post: -/// |= stable(p ~> q) +// A leads-to predicate is stable. +// post: +// |= stable(p ~> q) pub proof fn p_leads_to_q_is_stable(p: TempPred, q: TempPred) ensures valid(stable(p.leads_to(q))), @@ -970,12 +970,12 @@ pub proof fn p_leads_to_q_is_stable(p: TempPred, q: TempPred) always_p_is_stable(p.implies(eventually(q))); } -/// p and q is stable if both p and q are stable. -/// pre: -/// |= stable(p) -/// |= stable(q) -/// post: -/// |= stable(p /\ q) +// p and q is stable if both p and q are stable. +// pre: +// |= stable(p) +// |= stable(q) +// post: +// |= stable(p /\ q) pub proof fn stable_and_temp(p: TempPred, q: TempPred) requires valid(stable(p)), @@ -988,16 +988,16 @@ pub proof fn stable_and_temp(p: TempPred, q: TempPred) } } -/// The conjunction of all the p is stable if each p is stable. -/// pre: -/// |= stable(p1) -/// |= stable(p2) -/// ... -/// |= stable(pn) -/// post: -/// |= stable(p1 /\ p2 /\ ... /\ pn) -/// -/// Usage: stable_and_n!(p1, p2, p3, p4) +// The conjunction of all the p is stable if each p is stable. +// pre: +// |= stable(p1) +// |= stable(p2) +// ... +// |= stable(pn) +// post: +// |= stable(p1 /\ p2 /\ ... /\ pn) +// +// Usage: stable_and_n!(p1, p2, p3, p4) #[macro_export] macro_rules! stable_and_n { [$($tail:tt)*] => { @@ -1019,11 +1019,11 @@ macro_rules! stable_and_n_internal { pub use stable_and_n; pub use stable_and_n_internal; -/// The conjunction of all the p is stable if each p is stable. -/// post: -/// |= stable(always(p1) /\ always(p2) /\ ... /\ always(pn)) -/// -/// Usage: stable_and_always_n!(p1, p2, p3, p4) +// The conjunction of all the p is stable if each p is stable. +// post: +// |= stable(always(p1) /\ always(p2) /\ ... /\ always(pn)) +// +// Usage: stable_and_always_n!(p1, p2, p3, p4) #[macro_export] macro_rules! stable_and_always_n { [$($tail:tt)*] => { @@ -1043,12 +1043,12 @@ macro_rules! stable_and_always_n_internal { pub use stable_and_always_n; pub use stable_and_always_n_internal; -/// Unpack the conditions from the left to the right side of |= -/// pre: -/// |= stable(spec) -/// spec /\ c |= p ~> q -/// post: -/// spec |= p /\ c ~> q +// Unpack the conditions from the left to the right side of |= +// pre: +// |= stable(spec) +// spec /\ c |= p ~> q +// post: +// spec |= p /\ c ~> q pub proof fn unpack_conditions_from_spec(spec: TempPred, c: TempPred, p: TempPred, q: TempPred) requires valid(stable(spec)), @@ -1066,11 +1066,11 @@ pub proof fn unpack_conditions_from_spec(spec: TempPred, c: TempPred, p }; } -/// Pack the conditions from the right to the left side of |= -/// pre: -/// spec |= p /\ c ~> q -/// post: -/// spec /\ []c |= p ~> q +// Pack the conditions from the right to the left side of |= +// pre: +// spec |= p /\ c ~> q +// post: +// spec /\ []c |= p ~> q proof fn pack_conditions_to_spec(spec: TempPred, c: TempPred, p: TempPred, q: TempPred) requires spec.entails(p.and(c).leads_to(q)), ensures spec.and(always(c)).entails(p.leads_to(q)), @@ -1085,13 +1085,13 @@ proof fn pack_conditions_to_spec(spec: TempPred, c: TempPred, p: TempPr } } -/// This lemma is used to make the predicate as concise as possible. -/// Similar to the first-order logic where p equals p /\ q when p -> q is satisfied, -/// we can reduce the size of predicate when some part of it implies the rest. -/// pre: -/// p |= q -/// post: -/// p == p /\ q +// This lemma is used to make the predicate as concise as possible. +// Similar to the first-order logic where p equals p /\ q when p -> q is satisfied, +// we can reduce the size of predicate when some part of it implies the rest. +// pre: +// p |= q +// post: +// p == p /\ q pub proof fn simplify_predicate(p: TempPred, q: TempPred) requires p.entails(q), ensures p == p.and(q), @@ -1103,13 +1103,13 @@ pub proof fn simplify_predicate(p: TempPred, q: TempPred) temp_pred_equality::(p, p.and(q)); } -/// Prove safety by induction. -/// pre: -/// |= init => inv -/// |= inv /\ next => inv' -/// spec |= init /\ []next -/// post: -/// spec |= []inv +// Prove safety by induction. +// pre: +// |= init => inv +// |= inv /\ next => inv' +// spec |= init /\ []next +// post: +// spec |= []inv pub proof fn init_invariant(spec: TempPred, init: StatePred, next: ActionPred, inv: StatePred) requires forall |s: T| #[trigger] init(s) ==> inv(s), @@ -1129,13 +1129,13 @@ pub proof fn init_invariant(spec: TempPred, init: StatePred, next: Acti }; } -/// Strengthen next with inv. -/// pre: -/// spec |= []next -/// spec |= []inv -/// |= next /\ inv <=> next_and_inv -/// post: -/// spec |= []next_and_inv +// Strengthen next with inv. +// pre: +// spec |= []next +// spec |= []inv +// |= next /\ inv <=> next_and_inv +// post: +// spec |= []next_and_inv pub proof fn strengthen_next(spec: TempPred, next: ActionPred, inv: StatePred, next_and_inv: ActionPred) requires spec.entails(always(lift_action(next))), @@ -1149,14 +1149,14 @@ pub proof fn strengthen_next(spec: TempPred, next: ActionPred, inv: Sta temp_pred_equality::(lift_action(next_and_inv), lift_action(next).and(lift_state(inv))); } -/// Get the initial leads_to. -/// pre: -/// spec |= [](p /\ next => p' \/ q') -/// spec |= [](p /\ next /\ forward => q') -/// spec |= []next -/// spec |= []p ~> forward -/// post: -/// spec |= p ~> q +// Get the initial leads_to. +// pre: +// spec |= [](p /\ next => p' \/ q') +// spec |= [](p /\ next /\ forward => q') +// spec |= []next +// spec |= []p ~> forward +// post: +// spec |= p ~> q pub proof fn wf1_variant_temp(spec: TempPred, next: TempPred, forward: TempPred, p: TempPred, q: TempPred) requires spec.entails(always(p.and(next).implies(later(p).or(later(q))))), @@ -1191,15 +1191,15 @@ pub proof fn wf1_variant_temp(spec: TempPred, next: TempPred, forward: } } -/// Get the initial leads_to with a stronger wf assumption than wf1_variant. -/// pre: -/// |= p /\ next => p' \/ q' -/// |= p /\ next /\ forward => q' -/// |= p => enabled(forward) -/// spec |= []next -/// spec |= wf(forward) -/// post: -/// spec |= p ~> q +// Get the initial leads_to with a stronger wf assumption than wf1_variant. +// pre: +// |= p /\ next => p' \/ q' +// |= p /\ next /\ forward => q' +// |= p => enabled(forward) +// spec |= []next +// spec |= wf(forward) +// post: +// spec |= p ~> q pub proof fn wf1(spec: TempPred, next: ActionPred, forward: ActionPred, p: StatePred, q: StatePred) requires forall |s, s_prime: T| p(s) && #[trigger] next(s, s_prime) ==> p(s_prime) || q(s_prime), @@ -1223,12 +1223,12 @@ pub proof fn wf1(spec: TempPred, next: ActionPred, forward: ActionPred< wf1_variant_temp::(spec, lift_action(next), lift_action(forward), lift_state(p), lift_state(q)); } -/// Connects two valid implies. -/// pre: -/// p |= q -/// q |= r -/// post: -/// p |= r +// Connects two valid implies. +// pre: +// p |= q +// q |= r +// post: +// p |= r pub proof fn entails_trans(p: TempPred, q: TempPred, r: TempPred) requires p.entails(q), @@ -1241,12 +1241,12 @@ pub proof fn entails_trans(p: TempPred, q: TempPred, r: TempPred) }; } -/// If p implies q for all executions, p will leads to q anyway. -/// pre: -/// p |= q -/// post: -/// spec |= p ~> q -/// Note: there is no constraint on spec, it can be true_pred(). +// If p implies q for all executions, p will leads to q anyway. +// pre: +// p |= q +// post: +// spec |= p ~> q +// Note: there is no constraint on spec, it can be true_pred(). pub proof fn entails_implies_leads_to(spec: TempPred, p: TempPred, q: TempPred) requires p.entails(q), ensures spec.entails(p.leads_to(q)), @@ -1255,11 +1255,11 @@ pub proof fn entails_implies_leads_to(spec: TempPred, p: TempPred, q: T always_implies_to_leads_to(spec, p, q); } -/// Introduce always to both sides of implies. -/// pre: -/// p |= q -/// post: -/// []p |= []q +// Introduce always to both sides of implies. +// pre: +// p |= q +// post: +// []p |= []q pub proof fn entails_preserved_by_always(p: TempPred, q: TempPred) requires p.entails(q), ensures always(p).entails(always(q)), @@ -1272,12 +1272,12 @@ pub proof fn entails_preserved_by_always(p: TempPred, q: TempPred) }; } -/// Weaken always by implies. -/// pre: -/// |= p => q -/// spec |= []p -/// post: -/// spec |= []q +// Weaken always by implies. +// pre: +// |= p => q +// spec |= []p +// post: +// spec |= []q pub proof fn always_weaken(spec: TempPred, p: TempPred, q: TempPred) requires valid(p.implies(q)), @@ -1291,11 +1291,11 @@ pub proof fn always_weaken(spec: TempPred, p: TempPred, q: TempPred) }; } -/// Introduce always to both sides of always implies. -/// pre: -/// spec |= [](p => q) -/// post: -/// spec |= []([]p => []q) +// Introduce always to both sides of always implies. +// pre: +// spec |= [](p => q) +// post: +// spec |= []([]p => []q) pub proof fn always_implies_preserved_by_always(spec: TempPred, p: TempPred, q: TempPred) requires spec.entails(always(p.implies(q))), ensures spec.entails(always(always(p).implies(always(q)))), @@ -1315,13 +1315,13 @@ pub proof fn always_implies_preserved_by_always(spec: TempPred, p: TempPre }; } -/// Enhance the conclusion of leads to always using invariant. -/// pre: -/// spec |= []inv -/// spec |= p ~> []q1 -/// q1 /\ inv |= q2 -/// post: -/// spec |= p ~> []q2 +// Enhance the conclusion of leads to always using invariant. +// pre: +// spec |= []inv +// spec |= p ~> []q1 +// q1 /\ inv |= q2 +// post: +// spec |= p ~> []q2 pub proof fn leads_to_always_enhance(spec: TempPred, inv: TempPred, p: TempPred, q1: TempPred, q2: TempPred) requires spec.entails(always(inv)), @@ -1346,12 +1346,12 @@ pub proof fn leads_to_always_enhance(spec: TempPred, inv: TempPred, p: } } -/// Get eventually from leads_to. -/// pre: -/// spec |= p -/// spec |= p ~> q -/// post: -/// spec |= <>q +// Get eventually from leads_to. +// pre: +// spec |= p +// spec |= p ~> q +// post: +// spec |= <>q pub proof fn leads_to_apply(spec: TempPred, p: TempPred, q: TempPred) requires spec.entails(p), @@ -1367,12 +1367,12 @@ pub proof fn leads_to_apply(spec: TempPred, p: TempPred, q: TempPred }; } -/// Connect two leads_to by transitivity. -/// pre: -/// spec |= p ~> q -/// spec |= q ~> r -/// post: -/// spec |= p ~> r +// Connect two leads_to by transitivity. +// pre: +// spec |= p ~> q +// spec |= q ~> r +// post: +// spec |= p ~> r pub proof fn leads_to_trans(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(q)), @@ -1421,13 +1421,13 @@ macro_rules! leads_to_trans_n_internal { pub use leads_to_trans_n; pub use leads_to_trans_n_internal; -/// Weaken leads_to by implies. -/// pre: -/// spec |= [](p2 => p1) -/// spec |= [](q1 => q2) -/// spec |= p1 ~> q1 -/// post: -/// spec |= p2 ~> q2 +// Weaken leads_to by implies. +// pre: +// spec |= [](p2 => p1) +// spec |= [](q1 => q2) +// spec |= p1 ~> q1 +// post: +// spec |= p2 ~> q2 pub proof fn leads_to_weaken(spec: TempPred, p1: TempPred, q1: TempPred, p2: TempPred, q2: TempPred) requires spec.entails(always(p2.implies(p1))), @@ -1441,12 +1441,12 @@ pub proof fn leads_to_weaken(spec: TempPred, p1: TempPred, q1: TempPred leads_to_trans::(spec, p2, q1, q2); } -/// Combine the premises of two leads_to using or. -/// pre: -/// spec |= p ~> r -/// spec |= q ~> r -/// post: -/// spec |= (p \/ q) ~> r +// Combine the premises of two leads_to using or. +// pre: +// spec |= p ~> r +// spec |= q ~> r +// post: +// spec |= (p \/ q) ~> r pub proof fn or_leads_to_combine(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(r)), @@ -1463,16 +1463,16 @@ pub proof fn or_leads_to_combine(spec: TempPred, p: TempPred, q: TempPr }; } -/// Combine the premises of all the leads_to using or. -/// pre: -/// spec |= p1 ~> q -/// spec |= p2 ~> q -/// ... -/// spec |= pn ~> q -/// post: -/// spec |= (p1 \/ p2 \/ ... \/ pn) ~> q -/// -/// Usage: or_leads_to_combine_n!(spec, p1, p2, p3, p4; q) +// Combine the premises of all the leads_to using or. +// pre: +// spec |= p1 ~> q +// spec |= p2 ~> q +// ... +// spec |= pn ~> q +// post: +// spec |= (p1 \/ p2 \/ ... \/ pn) ~> q +// +// Usage: or_leads_to_combine_n!(spec, p1, p2, p3, p4; q) #[macro_export] macro_rules! or_leads_to_combine_n { [$($tail:tt)*] => { @@ -1494,8 +1494,8 @@ macro_rules! or_leads_to_combine_n_internal { pub use or_leads_to_combine_n; pub use or_leads_to_combine_n_internal; -/// Combine or_leads_to_combine and temp_pred_equality. -/// The 'result' is the equivalent temporal predicate of joining all following predicates with \/. +// Combine or_leads_to_combine and temp_pred_equality. +// The 'result' is the equivalent temporal predicate of joining all following predicates with \/. #[macro_export] macro_rules! or_leads_to_combine_and_equality { ($spec:expr, $result:expr, $p1:expr, $($rest:expr),+; $q:expr) => { @@ -1509,16 +1509,16 @@ macro_rules! or_leads_to_combine_and_equality { pub use or_leads_to_combine_and_equality; -/// Leads to the conjunction of all the []q if leads to each of them. -/// pre: -/// spec |= p ~> []q1 -/// spec |= p ~> []q2 -/// ... -/// spec |= p ~> []qn -/// post: -/// spec |= p ~> [](q1 /\ q2 /\ ... /\ qn) -/// -/// Usage: leads_to_always_combine_n!(spec, p, q1, q2, q3, q4) +// Leads to the conjunction of all the []q if leads to each of them. +// pre: +// spec |= p ~> []q1 +// spec |= p ~> []q2 +// ... +// spec |= p ~> []qn +// post: +// spec |= p ~> [](q1 /\ q2 /\ ... /\ qn) +// +// Usage: leads_to_always_combine_n!(spec, p, q1, q2, q3, q4) #[macro_export] macro_rules! leads_to_always_combine_n { [$($tail:tt)*] => { @@ -1559,18 +1559,18 @@ macro_rules! leads_to_always_combine_n_with_equality_internal { pub use leads_to_always_combine_n_with_equality; pub use leads_to_always_combine_n_with_equality_internal; -/// Leads to []tla_forall(a_to_p) if forall a, it leads []a_to_p(a). -/// pre: -/// forall |a: A|, spec |= p ~> []a_to_p(a) -/// forall |a: A|, a \in domain -/// domain.is_finite() && domain.len() > 0 -/// post: -/// spec |= []tla_forall(a_to_p) -/// The domain set assist in showing type A contains finite elements. -/// -/// This lemma is actually similar to leads_to_always_combine_n when the n predicates are all a_to_p(a) for some a. -/// This is because tla_forall(a_to_p) == a_to_p(a1).and(a_to_p(a2))....and(a_to_p(an)), We only consider the case when -/// type A is finite here. +// Leads to []tla_forall(a_to_p) if forall a, it leads []a_to_p(a). +// pre: +// forall |a: A|, spec |= p ~> []a_to_p(a) +// forall |a: A|, a \in domain +// domain.is_finite() && domain.len() > 0 +// post: +// spec |= []tla_forall(a_to_p) +// The domain set assist in showing type A contains finite elements. +// +// This lemma is actually similar to leads_to_always_combine_n when the n predicates are all a_to_p(a) for some a. +// This is because tla_forall(a_to_p) == a_to_p(a1).and(a_to_p(a2))....and(a_to_p(an)), We only consider the case when +// type A is finite here. pub proof fn leads_to_always_tla_forall(spec: TempPred, p: TempPred, a_to_p: spec_fn(A)->TempPred, domain: Set) requires forall |a: A| spec.entails(p.leads_to(always(#[trigger] a_to_p(a)))), @@ -1624,12 +1624,12 @@ pub proof fn leads_to_always_tla_forall(spec: TempPred, p: TempPred, }; } -/// Combine the conclusions of two leads_to if the conclusions are stable. -/// pre: -/// spec |= p ~> []q -/// spec |= p ~> []r -/// post: -/// spec |= p ~> [](q /\ r) +// Combine the conclusions of two leads_to if the conclusions are stable. +// pre: +// spec |= p ~> []q +// spec |= p ~> []r +// post: +// spec |= p ~> [](q /\ r) pub proof fn leads_to_always_combine(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(always(q))), @@ -1663,13 +1663,13 @@ pub proof fn leads_to_always_combine(spec: TempPred, p: TempPred, q: Te always_and_equality(q, r); } -/// Prove p leads_to always q by showing that q is preserved. -/// pre: -/// spec |= [](q /\ next => q') -/// spec |= []next -/// spec |= p ~> q -/// post: -/// spec |= p ~> []q +// Prove p leads_to always q by showing that q is preserved. +// pre: +// spec |= [](q /\ next => q') +// spec |= []next +// spec |= p ~> q +// post: +// spec |= p ~> []q pub proof fn leads_to_stable(spec: TempPred, next: TempPred, p: TempPred, q: TempPred) requires spec.entails(always(q.and(next).implies(later(q)))), @@ -1707,11 +1707,11 @@ pub proof fn leads_to_stable(spec: TempPred, next: TempPred, p: TempPre }; } -/// Sandwich leads-to with or r. -/// pre: -/// spec |= p ~> q -/// post: -/// spec |= p \/ r ~> q \/ r +// Sandwich leads-to with or r. +// pre: +// spec |= p ~> q +// post: +// spec |= p \/ r ~> q \/ r pub proof fn leads_to_framed_by_or(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(q)), ensures spec.entails(p.or(r).leads_to(q.or(r))), @@ -1733,12 +1733,12 @@ pub proof fn leads_to_framed_by_or(spec: TempPred, p: TempPred, q: Temp } } -/// Combine two leads-to with a shortcut. -/// pre: -/// spec |= p ~> q \/ s -/// spec |= q ~> r \/ s -/// post: -/// spec |= p ~> r \/ s +// Combine two leads-to with a shortcut. +// pre: +// spec |= p ~> q \/ s +// spec |= q ~> r \/ s +// post: +// spec |= p ~> r \/ s pub proof fn leads_to_shortcut_temp(spec: TempPred, p: TempPred, q: TempPred, r: TempPred, s: TempPred) requires spec.entails(p.leads_to(q.or(s))), @@ -1750,11 +1750,11 @@ pub proof fn leads_to_shortcut_temp(spec: TempPred, p: TempPred, q: Tem leads_to_trans(spec, p, q.or(s), r.or(s)); } -/// Concluding p(n) ~> p(0) using ranking functions, with a step of one. -/// pre: -/// forall |n: nat|, n > 0 ==> spec |= p(n) ~> p(n - 1) -/// post: -/// forall |n: nat|, spec |= p(n) ~> p(0). +// Concluding p(n) ~> p(0) using ranking functions, with a step of one. +// pre: +// forall |n: nat|, n > 0 ==> spec |= p(n) ~> p(n - 1) +// post: +// forall |n: nat|, spec |= p(n) ~> p(0). pub proof fn leads_to_rank_step_one(spec: TempPred, p: spec_fn(nat) -> TempPred) requires forall |n: nat| #![trigger p(n)] (n > 0 ==> spec.entails(p(n).leads_to(p((n - 1) as nat)))), @@ -1820,12 +1820,12 @@ proof fn leads_to_rank_step_one_usize_help(spec: TempPred, p: spec_fn(usiz } } -/// Proving p leads to q vacuously. -/// pre: -/// spec |= []r -/// p /\ r == false -/// post: -/// spec |= p ~> q +// Proving p leads to q vacuously. +// pre: +// spec |= []r +// p /\ r == false +// post: +// spec |= p ~> q pub proof fn vacuous_leads_to(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(always(r)), @@ -1847,12 +1847,12 @@ pub proof fn vacuous_leads_to(spec: TempPred, p: TempPred, q: TempPred< } } -/// Proving p leads to q by borrowing the inv. -/// pre: -/// spec |= p /\ inv ~> q -/// spec |= []inv -/// post: -/// spec |= p ~> q +// Proving p leads to q by borrowing the inv. +// pre: +// spec |= p /\ inv ~> q +// spec |= []inv +// post: +// spec |= p ~> q pub proof fn leads_to_by_borrowing_inv(spec: TempPred, p: TempPred, q: TempPred, inv: TempPred) requires spec.entails(p.and(inv).leads_to(q)), diff --git a/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs b/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs index b5782206f..29e1a052f 100644 --- a/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs +++ b/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs @@ -12,7 +12,7 @@ use vstd::prelude::*; verus! { -/// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions. +// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions. pub struct VReplicaSetReconcileState { pub reconcile_step: VReplicaSetReconcileStep, pub filtered_pods: Option>,