From 07c7b7feff15339bd6af2fe1619e1a5c81c9847d Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Thu, 3 Oct 2024 12:19:40 -0500 Subject: [PATCH] Add install helper for reconcile model Signed-off-by: Xudong Sun --- .../vreplicaset_controller/exec/reconciler.rs | 59 +++++++++------ .../vreplicaset_controller/model/install.rs | 71 +------------------ .../model/reconciler.rs | 26 ++++--- .../trusted/exec_types.rs | 36 ---------- .../trusted/spec_types.rs | 9 +-- .../proof/objects_in_store.rs | 10 --- .../spec/install_helpers.rs | 68 +++++++++++++----- src/v2/reconciler/exec/io.rs | 14 ++++ src/v2/reconciler/exec/reconciler.rs | 20 +++--- src/v2/reconciler/spec/io.rs | 31 +++++++- src/v2/reconciler/spec/reconciler.rs | 21 +++--- src/v2_vreplicaset_controller.rs | 32 ++++----- 12 files changed, 184 insertions(+), 213 deletions(-) diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs index afb227b7c..001d181b4 100644 --- a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs +++ b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs @@ -1,48 +1,61 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT -use crate::external_api::exec::*; -use crate::kubernetes_api_objects::exec::resource::ResourceWrapper; -use crate::kubernetes_api_objects::exec::{ - container::*, label_selector::*, pod_template_spec::*, prelude::*, resource_requirements::*, - volume::*, -}; -use crate::kubernetes_api_objects::spec::prelude::DynamicObjectView; -use crate::kubernetes_api_objects::spec::prelude::PodView; -use crate::kubernetes_api_objects::spec::resource::ResourceView; -use crate::reconciler::exec::{io::*, reconciler::*, resource_builder::*}; +use crate::kubernetes_api_objects::exec::{label_selector::*, pod_template_spec::*, prelude::*}; +use crate::kubernetes_api_objects::spec::prelude::*; +use crate::reconciler::exec::{io::*, reconciler::*}; use crate::vreplicaset_controller::model::reconciler as model_reconciler; -use crate::vreplicaset_controller::trusted::exec_types::*; -use crate::vreplicaset_controller::trusted::spec_types; -use crate::vreplicaset_controller::trusted::step::*; +use crate::vreplicaset_controller::trusted::{exec_types::*, step::*}; use crate::vstd_ext::{string_map::StringMap, string_view::*}; use vstd::prelude::*; use vstd::seq_lib::*; -use vstd::string::*; verus! { +// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions. +pub struct VReplicaSetReconcileState { + pub reconcile_step: VReplicaSetReconcileStep, + pub filtered_pods: Option>, +} + +impl View for VReplicaSetReconcileState { + type V = model_reconciler::VReplicaSetReconcileState; + + open spec fn view(&self) -> model_reconciler::VReplicaSetReconcileState { + model_reconciler::VReplicaSetReconcileState { + reconcile_step: self.reconcile_step, + filtered_pods: match self.filtered_pods { + Some(fp) => Some(fp@.map_values(|p: Pod| p@)), + None => None, + }, + } + } +} + pub struct VReplicaSetReconciler {} impl Reconciler for VReplicaSetReconciler { - type R = VReplicaSet; - type T = VReplicaSetReconcileState; - type ExternalAPIType = EmptyAPIShimLayer; + type S = VReplicaSetReconcileState; + type K = VReplicaSet; + type EReq = VoidEReq; + type EResp = VoidEResp; - open spec fn well_formed(v_replica_set: &VReplicaSet) -> bool { v_replica_set@.well_formed() } + open spec fn well_formed(v_replica_set: &Self::K) -> bool { + v_replica_set@.well_formed() + } - fn reconcile_init_state() -> VReplicaSetReconcileState { + fn reconcile_init_state() -> Self::S { reconcile_init_state() } - fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option>, state: VReplicaSetReconcileState) -> (VReplicaSetReconcileState, Option>) { + fn reconcile_core(v_replica_set: &Self::K, resp_o: Option>, state: Self::S) -> (Self::S, Option>) { reconcile_core(v_replica_set, resp_o, state) } - fn reconcile_done(state: &VReplicaSetReconcileState) -> bool { + fn reconcile_done(state: &Self::S) -> bool { reconcile_done(state) } - fn reconcile_error(state: &VReplicaSetReconcileState) -> bool { + fn reconcile_error(state: &Self::S) -> bool { reconcile_error(state) } } @@ -74,7 +87,7 @@ pub fn reconcile_error(state: &VReplicaSetReconcileState) -> (res: bool) } } -pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option>, state: VReplicaSetReconcileState) -> (res: (VReplicaSetReconcileState, Option>)) +pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option>, state: VReplicaSetReconcileState) -> (res: (VReplicaSetReconcileState, Option>)) requires v_replica_set@.well_formed(), ensures (res.0@, opt_request_to_view(&res.1)) == model_reconciler::reconcile_core(v_replica_set@, opt_response_to_view(&resp_o), state@), { diff --git a/src/v2/controllers/vreplicaset_controller/model/install.rs b/src/v2/controllers/vreplicaset_controller/model/install.rs index a2131dee9..97e50962a 100644 --- a/src/v2/controllers/vreplicaset_controller/model/install.rs +++ b/src/v2/controllers/vreplicaset_controller/model/install.rs @@ -1,41 +1,13 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT -use crate::external_api::spec::EmptyTypeView; use crate::kubernetes_api_objects::{error::*, spec::prelude::*}; -use crate::kubernetes_cluster::spec::{ - api_server::types::InstalledType, - cluster::ControllerModel, - controller::types::{ReconcileModel, RequestContent, ResponseContent}, - install_helpers::*, -}; -use crate::reconciler::spec::io::{RequestView, ResponseView}; -use crate::reconciler::spec::reconciler::Reconciler; +use crate::kubernetes_cluster::spec::cluster::{Cluster, ControllerModel}; use crate::vreplicaset_controller::model::reconciler::*; use crate::vreplicaset_controller::trusted::spec_types::*; use vstd::prelude::*; verus! { -pub open spec fn vrs_installed_type() -> InstalledType { - InstalledType { - unmarshallable_spec: |v| { - InstallTypeHelper::::unmarshal_spec(v) - }, - unmarshallable_status: |v| { - InstallTypeHelper::::unmarshal_status(v) - }, - valid_object: |obj| { - InstallTypeHelper::::valid_object(obj) - }, - valid_transition: |obj, old_obj| { - InstallTypeHelper::::valid_transition(obj, old_obj) - }, - marshalled_default_status: || { - InstallTypeHelper::::marshalled_default_status() - } - } -} - impl Marshallable for VReplicaSetReconcileState { spec fn marshal(self) -> Value; @@ -47,48 +19,9 @@ impl Marshallable for VReplicaSetReconcileState { {} } -impl Marshallable for EmptyTypeView { - spec fn marshal(self) -> Value; - - spec fn unmarshal(v: Value) -> Result; - - #[verifier(external_body)] - proof fn marshal_preserves_integrity() - ensures forall |o: Self| Self::unmarshal(#[trigger] o.marshal()).is_Ok() && o == Self::unmarshal(o.marshal()).get_Ok_0() - {} -} - -pub open spec fn vrs_reconcile_model() -> ReconcileModel { - ReconcileModel { - kind: VReplicaSetView::kind(), - init: || VReplicaSetReconciler::reconcile_init_state().marshal(), - transition: |obj, resp_o, s| { - let obj_um = VReplicaSetView::unmarshal(obj).get_Ok_0(); - let resp_o_um = match resp_o { - None => None, - Some(resp) => Some(match resp { - ResponseContent::KubernetesResponse(api_resp) => ResponseView::::KResponse(api_resp), - ResponseContent::ExternalResponse(ext_resp) => ResponseView::::ExternalResponse(EmptyTypeView::unmarshal(ext_resp).get_Ok_0()), - }) - }; - let s_um = VReplicaSetReconcileState::unmarshal(s).get_Ok_0(); - let (s_prime_um, req_o_um) = VReplicaSetReconciler::reconcile_core(obj_um, resp_o_um, s_um); - (s_prime_um.marshal(), match req_o_um { - None => None, - Some(req) => Some(match req { - RequestView::::KRequest(api_req) => RequestContent::KubernetesRequest(api_req), - RequestView::::ExternalRequest(ext_req) => RequestContent::ExternalRequest(ext_req.marshal()), - }) - }) - }, - done: |s| VReplicaSetReconciler::reconcile_done(VReplicaSetReconcileState::unmarshal(s).get_Ok_0()), - error: |s| VReplicaSetReconciler::reconcile_error(VReplicaSetReconcileState::unmarshal(s).get_Ok_0()), - } -} - pub open spec fn vrs_controller_model() -> ControllerModel { ControllerModel { - reconcile_model: vrs_reconcile_model(), + reconcile_model: Cluster::installed_reconcile_model::(), external_model: None, } } diff --git a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs index 4a5e649b4..d71c47f68 100644 --- a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs +++ b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs @@ -1,7 +1,6 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT #![allow(unused_imports)] -use crate::external_api::spec::*; use crate::kubernetes_api_objects::spec::prelude::*; use crate::reconciler::spec::{io::*, reconciler::*}; use crate::vreplicaset_controller::trusted::{spec_types::*, step::*}; @@ -9,25 +8,32 @@ use vstd::{prelude::*, string::*}; verus! { +pub struct VReplicaSetReconciler {} + +pub struct VReplicaSetReconcileState { + pub reconcile_step: VReplicaSetReconcileStep, + pub filtered_pods: Option>, +} + impl Reconciler for VReplicaSetReconciler { - type T = VReplicaSetReconcileState; + type S = VReplicaSetReconcileState; type K = VReplicaSetView; - type E = EmptyAPI; + type EReq = VoidEReqView; + type EResp = VoidERespView; - open spec fn reconcile_init_state() -> VReplicaSetReconcileState { + open spec fn reconcile_init_state() -> Self::S { reconcile_init_state() } - open spec fn reconcile_core(fb: VReplicaSetView, resp_o: Option>, state: VReplicaSetReconcileState) - -> (VReplicaSetReconcileState, Option>) { + open spec fn reconcile_core(fb: Self::K, resp_o: Option>, state: Self::S) -> (Self::S, Option>) { reconcile_core(fb, resp_o, state) } - open spec fn reconcile_done(state: VReplicaSetReconcileState) -> bool { + open spec fn reconcile_done(state: Self::S) -> bool { reconcile_done(state) } - open spec fn reconcile_error(state: VReplicaSetReconcileState) -> bool { + open spec fn reconcile_error(state: Self::S) -> bool { reconcile_error(state) } } @@ -53,9 +59,7 @@ pub open spec fn reconcile_error(state: VReplicaSetReconcileState) -> bool { } } -pub open spec fn reconcile_core( - v_replica_set: VReplicaSetView, resp_o: Option>, state: VReplicaSetReconcileState -) -> (VReplicaSetReconcileState, Option>) { +pub open spec fn reconcile_core(v_replica_set: VReplicaSetView, resp_o: Option>, state: VReplicaSetReconcileState) -> (VReplicaSetReconcileState, Option>) { let namespace = v_replica_set.metadata.namespace.unwrap(); match &state.reconcile_step { VReplicaSetReconcileStep::Init => { diff --git a/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs b/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs index 29e1a052f..8aaf14a71 100644 --- a/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs +++ b/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs @@ -12,42 +12,6 @@ use vstd::prelude::*; verus! { -// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions. -pub struct VReplicaSetReconcileState { - pub reconcile_step: VReplicaSetReconcileStep, - pub filtered_pods: Option>, -} - -// impl std::clone::Clone for VReplicaSetReconcileState { - -// #[verifier(external_body)] -// fn clone(&self) -> (result: VReplicaSetReconcileState) -// ensures result == self -// { -// VReplicaSetReconcileState { -// reconcile_step: self.reconcile_step, -// filtered_pods: match self.filtered_pods { -// Some(fp) => Some(fp.clone()), -// None => None, -// }, -// } -// } -// } - -impl View for VReplicaSetReconcileState { - type V = spec_types::VReplicaSetReconcileState; - - open spec fn view(&self) -> spec_types::VReplicaSetReconcileState { - spec_types::VReplicaSetReconcileState { - reconcile_step: self.reconcile_step, - filtered_pods: match self.filtered_pods { - Some(fp) => Some(fp@.map_values(|p: Pod| p@)), - None => None, - }, - } - } -} - #[verifier(external_body)] pub struct VReplicaSet { inner: deps_hack::VReplicaSet diff --git a/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs b/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs index 55d905642..8e6a2e12e 100644 --- a/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs +++ b/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs @@ -1,6 +1,5 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT -use crate::external_api::spec::{EmptyAPI, EmptyTypeView}; use crate::kubernetes_api_objects::error::*; use crate::kubernetes_api_objects::spec::{ api_resource::*, label_selector::*, pod_template_spec::*, prelude::*, @@ -12,13 +11,6 @@ use vstd::prelude::*; verus! { -pub struct VReplicaSetReconciler {} - -pub struct VReplicaSetReconcileState { - pub reconcile_step: VReplicaSetReconcileStep, - pub filtered_pods: Option>, -} - pub struct VReplicaSetView { pub metadata: ObjectMetaView, pub spec: VReplicaSetSpecView, @@ -28,6 +20,7 @@ pub struct VReplicaSetView { pub type VReplicaSetStatusView = EmptyStatusView; impl VReplicaSetView { + // TODO: well_formed should just call state_validation pub open spec fn well_formed(self) -> bool { &&& self.metadata.name.is_Some() &&& self.metadata.namespace.is_Some() diff --git a/src/v2/kubernetes_cluster/proof/objects_in_store.rs b/src/v2/kubernetes_cluster/proof/objects_in_store.rs index 1a0fde1bb..7ff4f699c 100644 --- a/src/v2/kubernetes_cluster/proof/objects_in_store.rs +++ b/src/v2/kubernetes_cluster/proof/objects_in_store.rs @@ -140,16 +140,6 @@ pub open spec fn each_custom_object_in_etcd_is_well_formed(self) -> bool { - let string = T::kind().get_CustomResourceKind_0(); - &&& self.installed_types.contains_key(string) - &&& self.installed_types[string].unmarshallable_spec == |v: Value| InstallTypeHelper::::unmarshal_spec(v) - &&& self.installed_types[string].unmarshallable_status == |v: Value| InstallTypeHelper::::unmarshal_status(v) - &&& self.installed_types[string].valid_object == |obj: DynamicObjectView| InstallTypeHelper::::valid_object(obj) - &&& self.installed_types[string].valid_transition == |obj, old_obj: DynamicObjectView| InstallTypeHelper::::valid_transition(obj, old_obj) - &&& self.installed_types[string].marshalled_default_status == || InstallTypeHelper::::marshalled_default_status() -} - pub proof fn lemma_always_each_custom_object_in_etcd_is_well_formed(self, spec: TempPred) requires spec.entails(lift_state(self.init())), diff --git a/src/v2/kubernetes_cluster/spec/install_helpers.rs b/src/v2/kubernetes_cluster/spec/install_helpers.rs index 1b1076c3e..74e50e3f9 100644 --- a/src/v2/kubernetes_cluster/spec/install_helpers.rs +++ b/src/v2/kubernetes_cluster/spec/install_helpers.rs @@ -1,35 +1,65 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT use crate::kubernetes_api_objects::spec::prelude::*; -use crate::kubernetes_cluster::spec::{api_server::types::*, controller::types::*}; +use crate::kubernetes_cluster::spec::{ + api_server::types::*, cluster::Cluster, controller::types::*, +}; +use crate::reconciler::spec::{io::*, reconciler::*}; use vstd::prelude::*; verus! { -pub struct InstallTypeHelper { - dummy: core::marker::PhantomData, -} - -impl InstallTypeHelper { - pub open spec fn unmarshal_spec(v: Value) -> bool { - T::unmarshal_spec(v).is_Ok() - } +impl Cluster { - pub open spec fn unmarshal_status(v: Value) -> bool { - T::unmarshal_status(v).is_Ok() +pub open spec fn installed_type() -> InstalledType { + InstalledType { + unmarshallable_spec: |v: Value| T::unmarshal_spec(v).is_Ok(), + unmarshallable_status: |v: Value| T::unmarshal_status(v).is_Ok(), + valid_object: |obj: DynamicObjectView| T::unmarshal(obj).get_Ok_0().state_validation(), + valid_transition: |obj, old_obj: DynamicObjectView| T::unmarshal(obj).get_Ok_0().transition_validation(T::unmarshal(old_obj).get_Ok_0()), + marshalled_default_status: || T::marshal_status(T::default().status()), } +} - pub open spec fn valid_object(obj: DynamicObjectView) -> bool { - T::unmarshal(obj).get_Ok_0().state_validation() - } +pub open spec fn type_is_installed_in_cluster(self) -> bool { + let string = T::kind().get_CustomResourceKind_0(); + &&& self.installed_types.contains_key(string) + &&& self.installed_types[string] == Self::installed_type::() +} - pub open spec fn valid_transition(obj: DynamicObjectView, old_obj: DynamicObjectView) -> bool { - T::unmarshal(obj).get_Ok_0().transition_validation(T::unmarshal(old_obj).get_Ok_0()) +pub open spec fn installed_reconcile_model() -> ReconcileModel + where + R::S: Marshallable, + R::EReq: Marshallable, + R::EResp: Marshallable, +{ + ReconcileModel { + kind: R::K::kind(), + init: || R::reconcile_init_state().marshal(), + transition: |obj, resp_o, s| { + let obj_um = R::K::unmarshal(obj).get_Ok_0(); + let resp_o_um = match resp_o { + None => None, + Some(resp) => Some(match resp { + ResponseContent::KubernetesResponse(api_resp) => ResponseView::::KResponse(api_resp), + ResponseContent::ExternalResponse(ext_resp) => ResponseView::::ExternalResponse(R::EResp::unmarshal(ext_resp).get_Ok_0()), + }) + }; + let s_um = R::S::unmarshal(s).get_Ok_0(); + let (s_prime_um, req_o_um) = R::reconcile_core(obj_um, resp_o_um, s_um); + (s_prime_um.marshal(), match req_o_um { + None => None, + Some(req) => Some(match req { + RequestView::::KRequest(api_req) => RequestContent::KubernetesRequest(api_req), + RequestView::::ExternalRequest(ext_req) => RequestContent::ExternalRequest(ext_req.marshal()), + }) + }) + }, + done: |s| R::reconcile_done(R::S::unmarshal(s).get_Ok_0()), + error: |s| R::reconcile_error(R::S::unmarshal(s).get_Ok_0()), } +} - pub open spec fn marshalled_default_status() -> Value { - T::marshal_status(T::default().status()) - } } } diff --git a/src/v2/reconciler/exec/io.rs b/src/v2/reconciler/exec/io.rs index 9b1076481..c96abb54e 100644 --- a/src/v2/reconciler/exec/io.rs +++ b/src/v2/reconciler/exec/io.rs @@ -9,6 +9,20 @@ use vstd::pervasive::unreached; verus! { +pub struct VoidEReq {} + +impl View for VoidEReq { + type V = VoidEReqView; + spec fn view(&self) -> VoidEReqView; +} + +pub struct VoidEResp {} + +impl View for VoidEResp { + type V = VoidERespView; + spec fn view(&self) -> VoidERespView; +} + // Third-party libraries can also receive requests from reconciler. // T: The input type of the third-party library of the reconciler which should also be defined by the developer. // Typically, T can be an enum type, which lists all the possible supporting handlings the developer need support from the diff --git a/src/v2/reconciler/exec/reconciler.rs b/src/v2/reconciler/exec/reconciler.rs index ea9599552..0cf00a80b 100644 --- a/src/v2/reconciler/exec/reconciler.rs +++ b/src/v2/reconciler/exec/reconciler.rs @@ -1,7 +1,6 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT #![allow(unused_imports)] -use crate::external_api::exec::*; use crate::kubernetes_api_objects::exec::api_method::*; use crate::reconciler::exec::io::*; use crate::reconciler::spec::io::*; @@ -9,16 +8,17 @@ use vstd::prelude::*; verus! { -pub trait Reconciler{ - type R; - type T; - type ExternalAPIType: ExternalAPIShimLayer; - spec fn well_formed(cr: &Self::R) -> bool; - fn reconcile_init_state() -> Self::T; - fn reconcile_core(cr: &Self::R, resp_o: Option::Output>>, state: Self::T) -> (Self::T, Option::Input>>) +pub trait Reconciler { + type S; + type K; + type EReq: View; + type EResp: View; + spec fn well_formed(cr: &Self::K) -> bool; + fn reconcile_init_state() -> Self::S; + fn reconcile_core(cr: &Self::K, resp_o: Option>, state: Self::S) -> (Self::S, Option>) requires Self::well_formed(cr); - fn reconcile_done(state: &Self::T) -> bool; - fn reconcile_error(state: &Self::T) -> bool; + fn reconcile_done(state: &Self::S) -> bool; + fn reconcile_error(state: &Self::S) -> bool; } } diff --git a/src/v2/reconciler/spec/io.rs b/src/v2/reconciler/spec/io.rs index 2fc6cbb94..25c25b9b7 100644 --- a/src/v2/reconciler/spec/io.rs +++ b/src/v2/reconciler/spec/io.rs @@ -1,12 +1,41 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT #![allow(unused_imports)] -use crate::kubernetes_api_objects::spec::{api_method::*, common::*, resource::*}; +use crate::kubernetes_api_objects::{ + error::UnmarshalError, + spec::{api_method::*, common::*, resource::*}, +}; use crate::kubernetes_cluster::spec::message::*; use vstd::prelude::*; verus! { +pub struct VoidEReqView {} + +pub struct VoidERespView {} + +impl Marshallable for VoidEReqView { + spec fn marshal(self) -> Value; + + spec fn unmarshal(v: Value) -> Result; + + #[verifier(external_body)] + proof fn marshal_preserves_integrity() + ensures forall |o: Self| Self::unmarshal(#[trigger] o.marshal()).is_Ok() && o == Self::unmarshal(o.marshal()).get_Ok_0() + {} +} + +impl Marshallable for VoidERespView { + spec fn marshal(self) -> Value; + + spec fn unmarshal(v: Value) -> Result; + + #[verifier(external_body)] + proof fn marshal_preserves_integrity() + ensures forall |o: Self| Self::unmarshal(#[trigger] o.marshal()).is_Ok() && o == Self::unmarshal(o.marshal()).get_Ok_0() + {} +} + #[is_variant] pub enum RequestView { KRequest(APIRequest), diff --git a/src/v2/reconciler/spec/reconciler.rs b/src/v2/reconciler/spec/reconciler.rs index 41a70e044..1011f64b1 100644 --- a/src/v2/reconciler/spec/reconciler.rs +++ b/src/v2/reconciler/spec/reconciler.rs @@ -1,7 +1,6 @@ // Copyright 2022 VMware, Inc. -// SPDX-License-Identifier: MIT +// SPDX-License-Identifier: MIS #![allow(unused_imports)] -use crate::external_api::spec::*; use crate::kubernetes_api_objects::spec::{api_method::*, common::*, dynamic::*, resource::*}; use crate::kubernetes_cluster::spec::message::*; use crate::reconciler::spec::io::*; @@ -12,29 +11,31 @@ verus! { // Reconciler is used to specify the custom controller as a state machine // and install it to the Kubernetes cluster state machine. pub trait Reconciler { - // T: type of the reconciler state of the reconciler. - type T; + // S: type of the reconciler state of the reconciler. + type S; // K: type of the custom resource. type K: CustomResourceView; - // E: type of request and response via which the controller interacts with external systems (if any). - type E: ExternalAPI; + // EReq: type of request the controller sends to the external systems (if any). + type EReq; + // EResp: type of response the controller receives from the external systems (if any). + type EResp; // reconcile_init_state returns the initial local state that the reconciler starts // its reconcile function with. - spec fn reconcile_init_state() -> Self::T; + spec fn reconcile_init_state() -> Self::S; // reconcile_core describes the logic of reconcile function and is the key logic we want to verify. // Each reconcile_core should take the local state and a response of the previous request (if any) as input // and outputs the next local state and the request to send to Kubernetes API (if any). - spec fn reconcile_core(cr: Self::K, resp_o: Option::Output>>, state: Self::T) -> (Self::T, Option::Input>>); + spec fn reconcile_core(cr: Self::K, resp_o: Option>, state: Self::S) -> (Self::S, Option>); // reconcile_done is used to tell the controller_runtime whether this reconcile round is done. // If it is true, controller_runtime will requeue the reconcile. - spec fn reconcile_done(state: Self::T) -> bool; + spec fn reconcile_done(state: Self::S) -> bool; // reconcile_error is used to tell the controller_runtime whether this reconcile round returns with error. // If it is true, controller_runtime will requeue the reconcile with a shorter waiting time. - spec fn reconcile_error(state: Self::T) -> bool; + spec fn reconcile_error(state: Self::S) -> bool; } } diff --git a/src/v2_vreplicaset_controller.rs b/src/v2_vreplicaset_controller.rs index bcf654e57..3cdbfe434 100644 --- a/src/v2_vreplicaset_controller.rs +++ b/src/v2_vreplicaset_controller.rs @@ -8,7 +8,7 @@ pub mod kubernetes_api_objects; pub mod kubernetes_cluster; #[path = "v2/reconciler/mod.rs"] pub mod reconciler; -pub mod shim_layer; +// pub mod shim_layer; pub mod state_machine; pub mod temporal_logic; #[path = "v2/controllers/vreplicaset_controller/mod.rs"] @@ -22,25 +22,25 @@ use deps_hack::serde_yaml; use deps_hack::tokio; use deps_hack::tracing::{error, info}; use deps_hack::tracing_subscriber; -use shim_layer::controller_runtime::run_controller; +// use shim_layer::controller_runtime::run_controller; use std::env; #[tokio::main] async fn main() -> Result<()> { - tracing_subscriber::fmt::init(); - let args: Vec = env::args().collect(); - let cmd = args[1].clone(); + // tracing_subscriber::fmt::init(); + // let args: Vec = env::args().collect(); + // let cmd = args[1].clone(); - if cmd == String::from("export") { - println!("{}", serde_yaml::to_string(&deps_hack::VReplicaSet::crd())?); - } else if cmd == String::from("run") { - info!("running v-replica-set-controller"); - run_controller::(false).await?; - } else if cmd == String::from("crash") { - info!("running v-replica-set-controller in crash-testing mode"); - run_controller::(true).await?; - } else { - error!("wrong command; please use \"export\", \"run\" or \"crash\""); - } + // if cmd == String::from("export") { + // println!("{}", serde_yaml::to_string(&deps_hack::VReplicaSet::crd())?); + // } else if cmd == String::from("run") { + // info!("running v-replica-set-controller"); + // run_controller::(false).await?; + // } else if cmd == String::from("crash") { + // info!("running v-replica-set-controller in crash-testing mode"); + // run_controller::(true).await?; + // } else { + // error!("wrong command; please use \"export\", \"run\" or \"crash\""); + // } Ok(()) }