Support unverified third party APIs in controllers (#180)

This PR allows developers to call any (unverified) third-party APIs
besides the Kubernetes client APIs when implementing the controller.

It adds `Lib` as a generic type to `Reconciler`. `Lib` also takes two
generic types `LibInputType` and `LibOutputType`. `Lib` wraps all
interactions with the third-party APIs, and it implements the trait
`ExternalLibrary<LibInputType, LibOutputType>`. `ExternalLibrary` has a
method `process` which calls the third-party API in a synchronous way:
it takes the input from `reconcile_core` (i.e., `LibInputType`) and
returns an output (`Option<LibOutputType>`).

During every reconcile loop, the reconciler will return an
`Option<Request>` (instead of the original `Option<KubeAPIRequest>`) to
the `shim_layer`. `Request` is an enum with two variants for the two
types of effects issued by the controller: invoking Kubernetes client
APIs or third-party APIs. The shim layer will do pattern matching to the
`Request` accordingly, which will either invoke the Kubernetes client
API as before, or invoke the third-party APIs by calling the
developer-provided `process`.

Correspondingly, the input to the reconciler, `Response`, is also an
enum that encodes the two types of responses from the Kubernetes client
APIs or third-party APIs.

---------

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

src/controller_examples/rabbitmq_controller/mod.rs

@@ -2,5 +2,5 @@
 // SPDX-License-Identifier: MIT
 pub mod common;
 pub mod exec;
-pub mod proof;
+// pub mod proof;
 pub mod spec;

src/controller_examples/rabbitmq_controller/proof/safety.rs

@@ -39,7 +39,7 @@ use crate::rabbitmq_controller::{
     proof::common::*,
     spec::{rabbitmqcluster::*, reconciler::*},
 };
-use crate::reconciler::spec::*;
+use crate::reconciler::spec::reconciler::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use vstd::{multiset::*, prelude::*, string::*};
 

src/controller_examples/rabbitmq_controller/proof/terminate.rs

@@ -31,7 +31,7 @@ use crate::rabbitmq_controller::{
     proof::{common::*, safety::*},
     spec::{rabbitmqcluster::*, reconciler::*},
 };
-use crate::reconciler::spec::*;
+use crate::reconciler::spec::reconciler::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;
 

src/controller_examples/simple_controller/exec/reconciler.rs

@@ -5,7 +5,8 @@ use crate::kubernetes_api_objects::{
     api_method::*, common::*, config_map::*, object_meta::*, resource::ResourceView,
 };
 use crate::pervasive_ext::string_map::StringMap;
-use crate::reconciler::exec::*;
+use crate::reconciler::exec::reconciler::*;
+use crate::reconciler::exec::{external::*, io::*};
 use crate::simple_controller::common::*;
 use crate::simple_controller::spec::custom_resource::*;
 use crate::simple_controller::spec::reconciler as simple_spec;
@@ -32,12 +33,12 @@ impl SimpleReconcileState {
 pub struct SimpleReconciler {}
 
 #[verifier(external)]
-impl Reconciler<CustomResource, SimpleReconcileState> for SimpleReconciler {
+impl Reconciler<CustomResource, SimpleReconcileState, EmptyMsg, EmptyMsg, EmptyLib> for SimpleReconciler {
     fn reconcile_init_state(&self) -> SimpleReconcileState {
         reconcile_init_state()
     }
 
-    fn reconcile_core(&self, cr: &CustomResource, resp_o: Option<KubeAPIResponse>, state: SimpleReconcileState) -> (SimpleReconcileState, Option<KubeAPIRequest>) {
+    fn reconcile_core(&self, cr: &CustomResource, resp_o: Option<Response<EmptyMsg>>, state: SimpleReconcileState) -> (SimpleReconcileState, Option<Request<EmptyMsg>>) {
         reconcile_core(cr, resp_o, state)
     }
 
@@ -93,12 +94,12 @@ pub fn reconcile_error(state: &SimpleReconcileState) -> (res: bool)
 // TODO: need to prove whether the object is valid; See an example:
 // ConfigMap "foo_cm" is invalid: metadata.name: Invalid value: "foo_cm": a lowercase RFC 1123 subdomain must consist of lower case alphanumeric characters, '-' or '.',
 // and must start and end with an alphanumeric character (e.g. 'example.com', regex used for validation is '[a-z0-9]([-a-z0-9]*[a-z0-9])?(\.[a-z0-9]([-a-z0-9]*[a-z0-9])?)*')
-pub fn reconcile_core(cr: &CustomResource, resp_o: Option<KubeAPIResponse>, state: SimpleReconcileState) -> (res: (SimpleReconcileState, Option<KubeAPIRequest>))
+pub fn reconcile_core(cr: &CustomResource, resp_o: Option<Response<EmptyMsg>>, state: SimpleReconcileState) -> (res: (SimpleReconcileState, Option<Request<EmptyMsg>>))
     requires
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        (res.0.to_view(), opt_req_to_view(&res.1)) == simple_spec::reconcile_core(cr@, opt_resp_to_view(&resp_o), state.to_view()),
+        (res.0.to_view(), opt_request_to_view(&res.1)) == simple_spec::reconcile_core(cr@, opt_response_to_view(&resp_o), state.to_view()),
 {
     let step = state.reconcile_step;
     match step {
@@ -108,22 +109,19 @@ pub fn reconcile_core(cr: &CustomResource, resp_o: Option<KubeAPIResponse>, stat
                 ..state
             };
             let config_map = make_configmap(cr);
-            let req_o = Option::Some(KubeAPIRequest::CreateRequest(
-                KubeCreateRequest {
-                    api_resource: ConfigMap::api_resource(),
-                    namespace: cr.metadata().namespace().unwrap(),
-                    obj: config_map.to_dynamic_object(),
-                }
-            ));
-            (state_prime, req_o)
+            let req_o = KubeAPIRequest::CreateRequest(KubeCreateRequest {
+                api_resource: ConfigMap::api_resource(),
+                namespace: cr.metadata().namespace().unwrap(),
+                obj: config_map.to_dynamic_object(),
+            });
+            (state_prime, Option::Some(Request::KRequest(req_o)))
         }
         _ => {
             let state_prime = SimpleReconcileState {
                 reconcile_step: step,
                 ..state
             };
-            let req_o = Option::None;
-            (state_prime, req_o)
+            (state_prime, Option::None)
         }
     }
 }

src/controller_examples/simple_controller/spec/reconciler.rs

@@ -6,7 +6,7 @@ use crate::kubernetes_api_objects::{
     resource::*,
 };
 use crate::kubernetes_cluster::spec::message::*;
-use crate::reconciler::spec::*;
+use crate::reconciler::spec::{io::*, reconciler::*};
 use crate::simple_controller::common::*;
 use crate::simple_controller::spec::custom_resource::*;
 use crate::state_machine::{action::*, state_machine::*};
@@ -28,13 +28,15 @@ pub struct SimpleReconcileState {
 pub struct SimpleReconciler {}
 
 impl Reconciler<CustomResourceView, SimpleReconcileState> for SimpleReconciler {
+    type LibInputType = ();
+    type LibOutputType = ();
     open spec fn reconcile_init_state() -> SimpleReconcileState {
         reconcile_init_state()
     }
 
     open spec fn reconcile_core(
-        cr: CustomResourceView, resp_o: Option<APIResponse>, state: SimpleReconcileState
-    ) -> (SimpleReconcileState, Option<APIRequest>) {
+        cr: CustomResourceView, resp_o: Option<ResponseView<()>>, state: SimpleReconcileState
+    ) -> (SimpleReconcileState, Option<RequestView<()>>) {
         reconcile_core(cr, resp_o, state)
     }
 
@@ -76,8 +78,8 @@ pub open spec fn reconcile_error(state: SimpleReconcileState) -> bool {
 /// it sends requests to create a configmap for the cr.
 /// TODO: make the reconcile_core create more resources such as a statefulset
 pub open spec fn reconcile_core(
-    cr: CustomResourceView, resp_o: Option<APIResponse>, state: SimpleReconcileState
-) -> (SimpleReconcileState, Option<APIRequest>)
+    cr: CustomResourceView, resp_o: Option<ResponseView<()>>, state: SimpleReconcileState
+) -> (SimpleReconcileState, Option<RequestView<()>>)
     recommends
         cr.metadata.name.is_Some(),
         cr.metadata.namespace.is_Some(),
@@ -89,7 +91,7 @@ pub open spec fn reconcile_core(
                 reconcile_step: SimpleReconcileStep::AfterCreateConfigMap,
                 ..state
             };
-            let req_o = Option::Some(create_cm_req(cr));
+            let req_o = Option::Some(RequestView::KRequest(create_cm_req(cr)));
             (state_prime, req_o)
         }
         _ => {

src/controller_examples/zookeeper_controller/common/mod.rs

@@ -1,7 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
-use vstd::prelude::*;
+use vstd::{prelude::*, string::*};
 
 verus! {
 
@@ -19,4 +19,8 @@ pub enum ZookeeperReconcileStep {
     Error,
 }
 
+pub enum Error {
+    ClusterSizeZKNodeCreationFailed,
+}
+
 }

src/controller_examples/zookeeper_controller/exec/common.rs

@@ -0,0 +1,40 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::pervasive_ext::string_view::*;
+use crate::zookeeper_controller::exec::zookeepercluster::*;
+use crate::zookeeper_controller::spec::reconciler as zk_spec;
+use vstd::{prelude::*, string::*};
+
+verus! {
+
+pub fn client_service_name(zk: &ZookeeperCluster) -> (name: String)
+    requires
+        [email protected]_Some(),
+        [email protected]_Some(),
+    ensures
+        name@ == zk_spec::make_client_service_name(zk@),
+{
+    zk.metadata().name().unwrap().concat(new_strlit("-client"))
+}
+
+pub fn zk_service_uri(zk: &ZookeeperCluster) -> String
+    requires
+        [email protected]_Some(),
+        [email protected]_Some(),
+{
+    client_service_name(zk)
+    .concat(new_strlit("."))
+    .concat(zk.metadata().namespace().unwrap().as_str())
+    .concat(new_strlit(".svc.cluster.local:2181"))
+}
+
+pub fn cluster_size_zk_node_path(zk: &ZookeeperCluster) -> String
+    requires
+        [email protected]_Some(),
+        [email protected]_Some(),
+{
+    new_strlit("/zookeeper-operator/").to_string()
+    .concat(zk.metadata().name().unwrap().as_str())
+}
+
+}

src/controller_examples/zookeeper_controller/exec/mod.rs

@@ -1,4 +1,6 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
+pub mod common;
 pub mod reconciler;
+pub mod zookeeper_lib;
 pub mod zookeepercluster;