Add comments

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

src/v2/controllers/vreplicaset_controller/exec/reconciler.rs

@@ -46,17 +46,14 @@ impl Reconciler for VReplicaSetReconciler {
     type K = VReplicaSet;
     type EReq = VoidEReq;
     type EResp = VoidEResp;
-
-    open spec fn well_formed(v_replica_set: &Self::K) -> bool {
-        [email protected]_formed()
-    }
+    type M = model_reconciler::VReplicaSetReconciler;
 
     fn reconcile_init_state() -> Self::S {
         reconcile_init_state()
     }
 
-    fn reconcile_core(v_replica_set: &Self::K, resp_o: Option<Response<Self::EResp>>, state: Self::S) -> (Self::S, Option<Request<Self::EReq>>) {
-        reconcile_core(v_replica_set, resp_o, state)
+    fn reconcile_core(vrs: &Self::K, resp_o: Option<Response<Self::EResp>>, state: Self::S) -> (Self::S, Option<Request<Self::EReq>>) {
+        reconcile_core(vrs, resp_o, state)
     }
 
     fn reconcile_done(state: &Self::S) -> bool {

src/v2/controllers/vreplicaset_controller/model/install.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::{error::*, spec::prelude::*};
 use crate::kubernetes_cluster::spec::cluster::{Cluster, ControllerModel};
+use crate::reconciler::spec::io::{VoidEReqView, VoidERespView};
 use crate::vreplicaset_controller::model::reconciler::*;
 use crate::vreplicaset_controller::trusted::spec_types::*;
 use vstd::prelude::*;
@@ -21,7 +22,7 @@ impl Marshallable for VReplicaSetReconcileState {
 
 pub open spec fn vrs_controller_model() -> ControllerModel {
     ControllerModel {
-        reconcile_model: Cluster::installed_reconcile_model::<VReplicaSetReconciler>(),
+        reconcile_model: Cluster::installed_reconcile_model::<VReplicaSetReconciler, VReplicaSetReconcileState, VReplicaSetView, VoidEReqView, VoidERespView>(),
         external_model: None,
     }
 }

src/v2/controllers/vreplicaset_controller/model/reconciler.rs

@@ -15,25 +15,25 @@ pub struct VReplicaSetReconcileState {
     pub filtered_pods: Option<Seq<PodView>>,
 }
 
-impl Reconciler for VReplicaSetReconciler {
-    type S = VReplicaSetReconcileState;
-    type K = VReplicaSetView;
-    type EReq = VoidEReqView;
-    type EResp = VoidERespView;
+impl Reconciler<VReplicaSetReconcileState, VReplicaSetView, VoidEReqView, VoidERespView> for VReplicaSetReconciler {
+    // type S = VReplicaSetReconcileState;
+    // type K = VReplicaSetView;
+    // type EReq = VoidEReqView;
+    // type EResp = VoidERespView;
 
-    open spec fn reconcile_init_state() -> Self::S {
+    open spec fn reconcile_init_state() -> VReplicaSetReconcileState {
         reconcile_init_state()
     }
 
-    open spec fn reconcile_core(fb: Self::K, resp_o: Option<ResponseView<Self::EResp>>, state: Self::S) -> (Self::S, Option<RequestView<Self::EReq>>) {
-        reconcile_core(fb, resp_o, state)
+    open spec fn reconcile_core(vrs: VReplicaSetView, resp_o: Option<ResponseView<VoidERespView>>, state: VReplicaSetReconcileState) -> (VReplicaSetReconcileState, Option<RequestView<VoidEReqView>>) {
+        reconcile_core(vrs, resp_o, state)
     }
 
-    open spec fn reconcile_done(state: Self::S) -> bool {
+    open spec fn reconcile_done(state: VReplicaSetReconcileState) -> bool {
         reconcile_done(state)
     }
 
-    open spec fn reconcile_error(state: Self::S) -> bool {
+    open spec fn reconcile_error(state: VReplicaSetReconcileState) -> bool {
         reconcile_error(state)
     }
 }

src/v2/kubernetes_cluster/spec/install_helpers.rs

@@ -27,36 +27,38 @@ pub open spec fn type_is_installed_in_cluster<T: CustomResourceView>(self) -> bo
     &&& self.installed_types[string] == Self::installed_type::<T>()
 }
 
-pub open spec fn installed_reconcile_model<R: Reconciler>() -> ReconcileModel
+pub open spec fn installed_reconcile_model<R, S, K, EReq, EResp>() -> ReconcileModel
     where
-        R::S: Marshallable,
-        R::EReq: Marshallable,
-        R::EResp: Marshallable,
+        R: Reconciler<S, K, EReq, EResp>,
+        K: CustomResourceView,
+        S: Marshallable,
+        EReq: Marshallable,
+        EResp: Marshallable,
 {
     ReconcileModel {
-        kind: R::K::kind(),
+        kind: K::kind(),
         init: || R::reconcile_init_state().marshal(),
         transition: |obj, resp_o, s| {
-            let obj_um = R::K::unmarshal(obj).get_Ok_0();
+            let obj_um = 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::<R::EResp>::KResponse(api_resp),
-                    ResponseContent::ExternalResponse(ext_resp) => ResponseView::<R::EResp>::ExternalResponse(R::EResp::unmarshal(ext_resp).get_Ok_0()),
+                    ResponseContent::KubernetesResponse(api_resp) => ResponseView::<EResp>::KResponse(api_resp),
+                    ResponseContent::ExternalResponse(ext_resp) => ResponseView::<EResp>::ExternalResponse(EResp::unmarshal(ext_resp).get_Ok_0()),
                 })
             };
-            let s_um = R::S::unmarshal(s).get_Ok_0();
+            let s_um = 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::<R::EReq>::KRequest(api_req) => RequestContent::KubernetesRequest(api_req),
-                    RequestView::<R::EReq>::ExternalRequest(ext_req) => RequestContent::ExternalRequest(ext_req.marshal()),
+                    RequestView::<EReq>::KRequest(api_req) => RequestContent::KubernetesRequest(api_req),
+                    RequestView::<EReq>::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()),
+        done: |s| R::reconcile_done(S::unmarshal(s).get_Ok_0()),
+        error: |s| R::reconcile_error(S::unmarshal(s).get_Ok_0()),
     }
 }
 

src/v2/reconciler/exec/reconciler.rs

@@ -1,24 +1,63 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
-use crate::kubernetes_api_objects::exec::api_method::*;
+use crate::kubernetes_api_objects::spec::resource::{CustomResourceView, ResourceView};
 use crate::reconciler::exec::io::*;
-use crate::reconciler::spec::io::*;
+use crate::reconciler::spec::{io::*, reconciler::Reconciler as ModelReconciler};
+use crate::vstd_ext::option_lib::*;
 use vstd::prelude::*;
 
 verus! {
 
-pub trait Reconciler {
+// Reconciler is used to implement the custom controller as a state machine
+// that interacts with Kubernetes API server via the shim_layer::controller_runtime.
+pub trait Reconciler
+where
+    Self::S: View,
+    Self::K: View,
+    <Self::K as View>::V: CustomResourceView,
+    Self::EReq: View,
+    Self::EResp: View,
+    // The ModelReconciler is built using the view of S, K, EReq and EResp.
+    // This is a workaround of missing type equality constraint in Rust.
+    Self::M: ModelReconciler<<Self::S as View>::V, <Self::K as View>::V, <Self::EReq as View>::V, <Self::EResp as View>::V>,
+{
+    // S: type of the reconciler state of the reconciler.
     type S;
+    // K: type of the custom resource.
     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<Response<Self::EResp>>, state: Self::S) -> (Self::S, Option<Request<Self::EReq>>)
-        requires Self::well_formed(cr);
-    fn reconcile_done(state: &Self::S) -> bool;
-    fn reconcile_error(state: &Self::S) -> bool;
+    // 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;
+    // M: type of the ModelReconciler that this implementation should conform to.
+    type M;
+
+    // reconcile_init_state returns the initial local state that the reconciler starts
+    // its reconcile function with.
+    // It conforms to the model's reconcile_init_state.
+    fn reconcile_init_state() -> (state: Self::S)
+        ensures state@ == Self::M::reconcile_init_state();
+
+    // 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 API server (if any).
+    // It conforms to the model's reconcile_core.
+    fn reconcile_core(cr: &Self::K, resp_o: Option<Response<Self::EResp>>, state: Self::S) -> (res: (Self::S, Option<Request<Self::EReq>>))
+        requires [email protected]().well_formed() && [email protected]_validation(),
+        ensures (res.0@, option_view(res.1)) == Self::M::reconcile_core(cr@, option_view(resp_o), state@);
+
+    // 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.
+    // It conforms to the model's reconcile_done.
+    fn reconcile_done(state: &Self::S) -> (res: bool)
+        ensures res == Self::M::reconcile_done(state@);
+
+    // 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 typically shorter waiting time.
+    // It conforms to the model's reconciler_error.
+    fn reconcile_error(state: &Self::S) -> (res: bool)
+        ensures res == Self::M::reconcile_error(state@);
 }
 
 }

src/v2/reconciler/spec/reconciler.rs

@@ -8,34 +8,38 @@ use vstd::prelude::*;
 
 verus! {
 
-// Reconciler is used to specify the custom controller as a state machine
+// Reconciler is used to model the custom controller as a state machine
 // and install it to the Kubernetes cluster state machine.
-pub trait Reconciler {
-    // S: type of the reconciler state of the reconciler.
-    type S;
-    // K: type of the custom resource.
-    type K: CustomResourceView;
-    // 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;
-
+//
+// S: type of the reconciler state of the reconciler.
+// K: type of the custom resource.
+// EReq: type of request the controller sends to the external systems (if any).
+// EResp: type of response the controller receives from the external systems (if any).
+//
+// The only reason that we don't make the types above as associated types is that
+// we need to connect this spec Reconciler to the exec Reconciler to pose the proof obligation
+// on the reconciler implementation. To do so, the exec Reconciler needs to pose a constraint
+// on its S, K, EReq and EResp that their views are the same type as the spec Reconciler's S, K, EReq and EResp
+// correspondingly. Since Rust doesn't support type equality constraint (see https://github.com/rust-lang/rust/issues/20041),
+// instead of stating the equality constraint, we state that the spec Reconciler is built
+// using the views of the exec Reconciler's S, K, EReq and EResp.
+pub trait Reconciler<S, K, EReq, EResp> {
     // reconcile_init_state returns the initial local state that the reconciler starts
     // its reconcile function with.
-    spec fn reconcile_init_state() -> Self::S;
+    spec fn reconcile_init_state() -> 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<ResponseView<Self::EResp>>, state: Self::S) -> (Self::S, Option<RequestView<Self::EReq>>);
+    // and outputs the next local state and the request to send to API server (if any).
+    spec fn reconcile_core(cr: K, resp_o: Option<ResponseView<EResp>>, state: S) -> (S, Option<RequestView<EReq>>);
 
     // 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::S) -> bool;
+    spec fn reconcile_done(state: 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::S) -> bool;
+    // If it is true, controller_runtime will requeue the reconcile with a typically shorter waiting time.
+    spec fn reconcile_error(state: S) -> bool;
 }
 
 }

src/v2/shim_layer/controller_runtime.rs

@@ -4,6 +4,7 @@
 use crate::external_shim_layer::*;
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::exec::{api_method::*, dynamic::*, resource::*};
+use crate::kubernetes_api_objects::spec::resource::*;
 use crate::reconciler::exec::{io::*, reconciler::*};
 use crate::shim_layer::fault_injection::*;
 use builtin::*;
@@ -50,6 +51,7 @@ where
     K::DynamicType: Default + Eq + Hash + Clone + Debug + Unpin,
     R: Reconciler + Send + Sync,
     R::K: ResourceWrapper<K> + Send,
+    <R::K as View>::V: CustomResourceView,
     R::S: Send,
     R::EReq: Send,
     R::EResp: Send,
@@ -102,6 +104,7 @@ where
     K::DynamicType: Default + Clone + Debug,
     R: Reconciler,
     R::K: ResourceWrapper<K>,
+    <R::K as View>::V: CustomResourceView,
     E: ExternalShimLayer<R::EReq, R::EResp>,
 {
     let client = &ctx.client;