Use associated types for the Reconciler trait

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

src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs

@@ -17,7 +17,11 @@ verus! {
 
 pub struct FluentBitReconciler {}
 
-impl Reconciler<FluentBit, FluentBitReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for FluentBitReconciler {
+impl Reconciler for FluentBitReconciler {
+    type R = FluentBit;
+    type T = FluentBitReconcileState;
+    type ExternalAPIType = EmptyAPIShimLayer;
+
     open spec fn well_formed(fb: &FluentBit) -> bool { [email protected]_formed() }
 
     fn reconcile_init_state() -> FluentBitReconcileState {

src/controller_examples/fluent_controller/fluentbit_config/exec/reconciler.rs

@@ -17,7 +17,11 @@ verus! {
 
 pub struct FluentBitConfigReconciler {}
 
-impl Reconciler<FluentBitConfig, FluentBitConfigReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for FluentBitConfigReconciler {
+impl Reconciler for FluentBitConfigReconciler {
+    type R = FluentBitConfig;
+    type T = FluentBitConfigReconcileState;
+    type ExternalAPIType = EmptyAPIShimLayer;
+
     open spec fn well_formed(fbc: &FluentBitConfig) -> bool { [email protected]_formed() }
 
     fn reconcile_init_state() -> FluentBitConfigReconcileState {

src/controller_examples/rabbitmq_controller/exec/reconciler.rs

@@ -24,7 +24,11 @@ verus! {
 
 pub struct RabbitmqReconciler {}
 
-impl Reconciler<RabbitmqCluster, RabbitmqReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for RabbitmqReconciler {
+impl Reconciler for RabbitmqReconciler {
+    type R = RabbitmqCluster;
+    type T = RabbitmqReconcileState;
+    type ExternalAPIType = EmptyAPIShimLayer;
+
     open spec fn well_formed(rabbitmq: &RabbitmqCluster) -> bool { [email protected]_formed() }
 
     fn reconcile_init_state() -> RabbitmqReconcileState {

src/controller_examples/zookeeper_controller/exec/reconciler.rs

@@ -25,7 +25,11 @@ verus! {
 
 pub struct ZookeeperReconciler {}
 
-impl Reconciler<ZookeeperCluster, ZookeeperReconcileState, ZKAPIInput, ZKAPIOutput, ZKAPIShimLayer> for ZookeeperReconciler {
+impl Reconciler for ZookeeperReconciler {
+    type R = ZookeeperCluster;
+    type T = ZookeeperReconcileState;
+    type ExternalAPIType = ZKAPIShimLayer;
+
     open spec fn well_formed(zk: &ZookeeperCluster) -> bool { [email protected]_formed() }
 
     fn reconcile_init_state() -> ZookeeperReconcileState {

src/controller_examples/zookeeper_controller/trusted/zookeeper_api_exec.rs

@@ -93,7 +93,9 @@ impl View for ZKAPIOutput {
 pub struct ZKAPIShimLayer {}
 
 #[verifier(external)]
-impl ExternalAPIShimLayer<ZKAPIInput, ZKAPIOutput> for ZKAPIShimLayer {
+impl ExternalAPIShimLayer for ZKAPIShimLayer {
+    type Input = ZKAPIInput;
+    type Output = ZKAPIOutput;
     fn call_external_api(input: ZKAPIInput) -> ZKAPIOutput {
         match input {
             ZKAPIInput::ExistsRequest(zk_name, zk_namespace, port, path)

src/external_api/exec.rs

@@ -11,16 +11,20 @@ verus! {
 // request type of a reconciler.
 // Similarly, Output is the output type of the external api, which composes the Response<?> type of a reconciler.
 // Note that we can encapsulate all the required libraries here, so each reconciler only has one ExternalAPI type.
-pub trait ExternalAPIShimLayer<Input: View, Output: View> {
-    fn call_external_api(input: Input) -> Output;
+pub trait ExternalAPIShimLayer {
+    type Input: View;
+    type Output: View;
+    fn call_external_api(input: Self::Input) -> Self::Output;
 }
 
 // An empty library that implements External Library.
 // This can be used by those controllers that don't rely on a third-party library.
 // Users can define a reconciler as Reconciler<xx, xx, EmptyType, EmptyType, EmptyAPI>.
 pub struct EmptyAPIShimLayer {}
 
-impl ExternalAPIShimLayer<EmptyType, EmptyType> for EmptyAPIShimLayer {
+impl ExternalAPIShimLayer for EmptyAPIShimLayer {
+    type Input = EmptyType;
+    type Output = EmptyType;
     fn call_external_api(_input: EmptyType) -> EmptyType {
         EmptyType {}
     }

src/fluent_controller.rs

@@ -49,14 +49,14 @@ async fn main() -> Result<()> {
         println!("{}", serde_yaml::to_string(&deps_hack::FluentBitConfig::crd())?);
     } else if cmd == String::from("run") {
         println!("running fluent-controller");
-        let fluentbit_controller_fut = run_controller::<deps_hack::FluentBit, FluentBit, FluentBitReconciler, FluentBitReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer>(false);
-        let fluentbit_config_controller_fut = run_controller::<deps_hack::FluentBitConfig, FluentBitConfig, FluentBitConfigReconciler, FluentBitConfigReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer>(false);
+        let fluentbit_controller_fut = run_controller::<deps_hack::FluentBit, FluentBitReconciler>(false);
+        let fluentbit_config_controller_fut = run_controller::<deps_hack::FluentBitConfig, FluentBitConfigReconciler>(false);
         futures::try_join!(fluentbit_controller_fut, fluentbit_config_controller_fut)?;
         println!("controller terminated");
     } else if cmd == String::from("crash") {
         println!("running fluent-controller in crash-testing mode");
-        let fluentbit_controller_fut = run_controller::<deps_hack::FluentBit, FluentBit, FluentBitReconciler, FluentBitReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer>(true);
-        let fluentbit_config_controller_fut = run_controller::<deps_hack::FluentBitConfig, FluentBitConfig, FluentBitConfigReconciler, FluentBitConfigReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer>(true);
+        let fluentbit_controller_fut = run_controller::<deps_hack::FluentBit, FluentBitReconciler>(true);
+        let fluentbit_config_controller_fut = run_controller::<deps_hack::FluentBitConfig, FluentBitConfigReconciler>(true);
         futures::try_join!(fluentbit_controller_fut, fluentbit_config_controller_fut)?;
         println!("controller terminated");
     } else {

src/rabbitmq_controller.rs

@@ -39,11 +39,11 @@ async fn main() -> Result<()> {
         println!("{}", serde_yaml::to_string(&deps_hack::RabbitmqCluster::crd())?);
     } else if cmd == String::from("run") {
         println!("running rabbitmq-controller");
-        run_controller::<deps_hack::RabbitmqCluster, RabbitmqCluster, RabbitmqReconciler, RabbitmqReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer>(false).await?;
+        run_controller::<deps_hack::RabbitmqCluster, RabbitmqReconciler>(false).await?;
         println!("controller terminated");
     } else if cmd == String::from("crash") {
         println!("running rabbitmq-controller in crash-testing mode");
-        run_controller::<deps_hack::RabbitmqCluster, RabbitmqCluster, RabbitmqReconciler, RabbitmqReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer>(true).await?;
+        run_controller::<deps_hack::RabbitmqCluster, RabbitmqReconciler>(true).await?;
         println!("controller terminated");
     } else {
         println!("wrong command; please use \"export\", \"run\" or \"crash\"");

src/reconciler/exec/reconciler.rs

@@ -9,34 +9,35 @@ use vstd::prelude::*;
 
 verus! {
 
-pub trait Reconciler<R, T, ExternalAPIInput, ExternalAPIOutput, ExternalAPIType>
-    where ExternalAPIInput: View, ExternalAPIOutput: View, ExternalAPIType: ExternalAPIShimLayer<ExternalAPIInput, ExternalAPIOutput>
-{
-    spec fn well_formed(cr: &R) -> bool;
-    fn reconcile_init_state() -> T;
-    fn reconcile_core(cr: &R, resp_o: Option<Response<ExternalAPIOutput>>, state: T) -> (T, Option<Request<ExternalAPIInput>>)
+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<Response<<Self::ExternalAPIType as ExternalAPIShimLayer>::Output>>, state: Self::T) -> (Self::T, Option<Request<<Self::ExternalAPIType as ExternalAPIShimLayer>::Input>>)
         requires Self::well_formed(cr);
-    fn reconcile_done(state: &T) -> bool;
-    fn reconcile_error(state: &T) -> bool;
+    fn reconcile_done(state: &Self::T) -> bool;
+    fn reconcile_error(state: &Self::T) -> bool;
 }
 
-pub open spec fn resource_version_check<I, O>(prev_resp_opt: Option<ResponseView<O>>, cur_req_opt: Option<RequestView<I>>) -> bool {
-    cur_req_opt.is_Some() && cur_req_opt.get_Some_0().is_k_update_request()
-    ==> prev_resp_opt.is_Some() && resource_version_check_helper(prev_resp_opt.get_Some_0(), cur_req_opt.get_Some_0())
-}
+// pub open spec fn resource_version_check<I, O>(prev_resp_opt: Option<ResponseView<O>>, cur_req_opt: Option<RequestView<I>>) -> bool {
+//     cur_req_opt.is_Some() && cur_req_opt.get_Some_0().is_k_update_request()
+//     ==> prev_resp_opt.is_Some() && resource_version_check_helper(prev_resp_opt.get_Some_0(), cur_req_opt.get_Some_0())
+// }
 
-pub open spec fn resource_version_check_helper<I, O>(prev_resp: ResponseView<O>, cur_req: RequestView<I>) -> bool {
-    let prev_get_resp = prev_resp.get_k_get_response();
-    let found_obj = prev_get_resp.res.get_Ok_0();
-    let cur_update_req = cur_req.get_k_update_request();
-    let obj_to_update = cur_update_req.obj;
-    cur_req.is_k_update_request()
-    ==> prev_resp.is_k_get_response()
-        && prev_get_resp.res.is_Ok()
-        && found_obj.kind == obj_to_update.kind
-        && found_obj.metadata.name == obj_to_update.metadata.name
-        && found_obj.metadata.namespace == obj_to_update.metadata.namespace
-        && found_obj.metadata.resource_version == obj_to_update.metadata.resource_version
-}
+// pub open spec fn resource_version_check_helper<I, O>(prev_resp: ResponseView<O>, cur_req: RequestView<I>) -> bool {
+//     let prev_get_resp = prev_resp.get_k_get_response();
+//     let found_obj = prev_get_resp.res.get_Ok_0();
+//     let cur_update_req = cur_req.get_k_update_request();
+//     let obj_to_update = cur_update_req.obj;
+//     cur_req.is_k_update_request()
+//     ==> prev_resp.is_k_get_response()
+//         && prev_get_resp.res.is_Ok()
+//         && found_obj.kind == obj_to_update.kind
+//         && found_obj.metadata.name == obj_to_update.metadata.name
+//         && found_obj.metadata.namespace == obj_to_update.metadata.namespace
+//         && found_obj.metadata.resource_version == obj_to_update.metadata.resource_version
+// }
 
 }

src/shim_layer/controller_runtime.rs

@@ -36,27 +36,24 @@ verus! {
 
 // run_controller prepares and runs the controller. It requires:
 // K: the custom resource type
-// ResourceWrapperType: the resource wrapper type
 // ReconcilerType: the reconciler type
-// ReconcileStateType: the local state of the reconciler
 #[verifier(external)]
-pub async fn run_controller<K, ResourceWrapperType, ReconcilerType, ReconcileStateType, ExternalAPIInputType, ExternalAPIOutputType, ExternalAPIShimLayerType>(fault_injection: bool) -> Result<()>
+pub async fn run_controller<K, ReconcilerType>(fault_injection: bool) -> Result<()>
 where
     K: Clone + Resource<Scope = NamespaceResourceScope> + CustomResourceExt + DeserializeOwned + Debug + Send + Serialize + Sync + 'static,
     K::DynamicType: Default + Eq + Hash + Clone + Debug + Unpin,
-    ResourceWrapperType: ResourceWrapper<K> + Send,
-    ReconcilerType: Reconciler<ResourceWrapperType, ReconcileStateType, ExternalAPIInputType, ExternalAPIOutputType, ExternalAPIShimLayerType> + Send + Sync + Default,
-    ReconcileStateType: Send,
-    ExternalAPIInputType: Send + View,
-    ExternalAPIOutputType: Send + View,
-    ExternalAPIShimLayerType: ExternalAPIShimLayer<ExternalAPIInputType, ExternalAPIOutputType>,
+    ReconcilerType: Reconciler + Send + Sync + Default,
+    ReconcilerType::R: ResourceWrapper<K> + Send,
+    ReconcilerType::T: Send,
+    <ReconcilerType::ExternalAPIType as ExternalAPIShimLayer>::Input: Send,
+    <ReconcilerType::ExternalAPIType as ExternalAPIShimLayer>::Output: Send,
 {
     let client = Client::try_default().await?;
     let crs = Api::<K>::all(client.clone());
 
     // Build the async closure on top of reconcile_with
     let reconcile = |cr: Arc<K>, ctx: Arc<Data>| async move {
-        return reconcile_with::<K, ResourceWrapperType, ReconcilerType, ReconcileStateType, ExternalAPIInputType, ExternalAPIOutputType, ExternalAPIShimLayerType>(
+        return reconcile_with::<K, ReconcilerType>(
             cr, ctx, fault_injection
         ).await;
     };
@@ -86,17 +83,12 @@ where
 // It ends the loop when the ReconcilerType reports the reconcile is done (ReconcilerType::reconcile_done)
 // or encounters error (ReconcilerType::reconcile_error).
 #[verifier(external)]
-pub async fn reconcile_with<K, ResourceWrapperType, ReconcilerType, ReconcileStateType, ExternalAPIInputType, ExternalAPIOutputType, ExternalAPIShimLayerType>(
-    cr: Arc<K>, ctx: Arc<Data>, fault_injection: bool
-) -> Result<Action, Error>
+pub async fn reconcile_with<K, ReconcilerType>(cr: Arc<K>, ctx: Arc<Data>, fault_injection: bool) -> Result<Action, Error>
 where
     K: Clone + Resource<Scope = NamespaceResourceScope> + CustomResourceExt + DeserializeOwned + Debug + Serialize,
     K::DynamicType: Default + Clone + Debug,
-    ResourceWrapperType: ResourceWrapper<K>,
-    ReconcilerType: Reconciler<ResourceWrapperType, ReconcileStateType, ExternalAPIInputType, ExternalAPIOutputType, ExternalAPIShimLayerType>,
-    ExternalAPIInputType: View,
-    ExternalAPIOutputType: View,
-    ExternalAPIShimLayerType: ExternalAPIShimLayer<ExternalAPIInputType, ExternalAPIOutputType>,
+    ReconcilerType: Reconciler,
+    ReconcilerType::R: ResourceWrapper<K>,
 {
     let client = &ctx.client;
 
@@ -125,9 +117,9 @@ where
     let cr = get_cr_resp.unwrap();
     println!("{} Get cr {}", log_header, deps_hack::k8s_openapi::serde_json::to_string(&cr).unwrap());
 
-    let cr_wrapper = ResourceWrapperType::from_kube(cr);
+    let cr_wrapper = ReconcilerType::R::from_kube(cr);
     let mut state = ReconcilerType::reconcile_init_state();
-    let mut resp_option: Option<Response<ExternalAPIOutputType>> = None;
+    let mut resp_option: Option<Response<<ReconcilerType::ExternalAPIType as ExternalAPIShimLayer>::Output>> = None;
     // check_fault_timing is only set to true right after the controller issues any create, update or delete request,
     // or external request
     let mut check_fault_timing: bool;
@@ -290,7 +282,7 @@ where
                 },
                 Request::ExternalRequest(req) => {
                     check_fault_timing = true;
-                    let external_resp = ExternalAPIShimLayerType::call_external_api(req);
+                    let external_resp = ReconcilerType::ExternalAPIType::call_external_api(req);
                     resp_option = Some(Response::ExternalResponse(external_resp));
                 },
             },

src/zookeeper_controller.rs

@@ -39,11 +39,11 @@ async fn main() -> Result<()> {
         println!("{}", serde_yaml::to_string(&deps_hack::ZookeeperCluster::crd())?);
     } else if cmd == String::from("run") {
         println!("running zookeeper-controller");
-        run_controller::<deps_hack::ZookeeperCluster, ZookeeperCluster, ZookeeperReconciler, ZookeeperReconcileState, ZKAPIInput, ZKAPIOutput, ZKAPIShimLayer>(false).await?;
+        run_controller::<deps_hack::ZookeeperCluster, ZookeeperReconciler>(false).await?;
         println!("controller terminated");
     } else if cmd == String::from("crash") {
         println!("running zookeeper-controller in crash-testing mode");
-        run_controller::<deps_hack::ZookeeperCluster, ZookeeperCluster, ZookeeperReconciler, ZookeeperReconcileState, ZKAPIInput, ZKAPIOutput, ZKAPIShimLayer>(true).await?;
+        run_controller::<deps_hack::ZookeeperCluster, ZookeeperReconciler>(true).await?;
         println!("controller terminated");
     } else {
         println!("wrong command; please use \"export\", \"run\" or \"crash\"");