Add VDeployment type (#562)

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

.github/workflows/ci.yml

@@ -127,6 +127,29 @@ jobs:
           vargo build --release
       - name: Verify vreplicaset controller
         run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh v2_vreplicaset_controller.rs --time
+  v2-vdeployment-verification:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+      - name: Download Verus
+        uses: actions/checkout@v2
+        with:
+          repository: verus-lang/verus
+          path: verus
+          ref: 0d7b766446cd33521132cff03b6108705e83884f
+      - name: Move Verus
+        run: mv verus ../verus
+      - name: Install Rust toolchain
+        run: |
+          curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y
+      - name: Build Verus
+        run: |
+          cd ../verus/source
+          ./tools/get-z3.sh
+          source ../tools/activate
+          vargo build --release
+      - name: Verify vdeployment controller
+        run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh v2_vdeployment_controller.rs --time
   unit-tests:
     runs-on: ubuntu-20.04
     steps:

src/deps_hack/src/lib.rs

@@ -281,6 +281,17 @@ pub struct VReplicaSetSpec {
     pub template: Option<k8s_openapi::api::core::v1::PodTemplateSpec>,
 }
 
+#[derive(
+    kube::CustomResource, Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema,
+)]
+#[kube(group = "anvil.dev", version = "v1", kind = "VDeployment")]
+#[kube(shortname = "vrs", namespaced)]
+pub struct VDeploymentSpec {
+    pub replicas: Option<i32>,
+    pub selector: k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector,
+    pub template: Option<k8s_openapi::api::core::v1::PodTemplateSpec>,
+}
+
 #[derive(
     kube::CustomResource, Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema,
 )]
@@ -330,34 +341,3 @@ pub struct VStatefulSetStatus {
     #[serde(rename = "observedGeneration")]
     pub observed_generation: Option<i64>,
 }
-
-#[derive(
-    kube::CustomResource,
-    Debug,
-    Clone,
-    serde::Deserialize,
-    serde::Serialize,
-    schemars::JsonSchema,
-    Default,
-)]
-#[kube(namespaced, group = "anvil.dev", version = "v1", kind = "Producer")]
-pub struct ProducerSpec {
-    pub message: String,
-}
-
-impl Default for Producer {
-    fn default() -> Producer {
-        Producer {
-            metadata: k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta::default(),
-            spec: ProducerSpec::default(),
-        }
-    }
-}
-
-#[derive(
-    kube::CustomResource, Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema,
-)]
-#[kube(namespaced, group = "anvil.dev", version = "v1", kind = "Consumer")]
-pub struct ConsumerSpec {
-    pub message: String,
-}

src/v2/controllers/vdeployment_controller/mod.rs

@@ -0,0 +1,6 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+// pub mod exec;
+// pub mod model;
+// pub mod proof;
+pub mod trusted;

src/v2/controllers/vdeployment_controller/trusted/exec_types.rs

@@ -0,0 +1,125 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::error::UnmarshalError;
+use crate::kubernetes_api_objects::exec::{
+    api_resource::*, label_selector::*, pod_template_spec::*, prelude::*,
+};
+use crate::kubernetes_api_objects::spec::resource::*;
+use crate::vdeployment_controller::trusted::{spec_types, step::*};
+use crate::vstd_ext::{string_map::*, string_view::*};
+use deps_hack::kube::Resource;
+use vstd::prelude::*;
+
+verus! {
+
+#[verifier(external_body)]
+pub struct VDeployment {
+    inner: deps_hack::VDeployment
+}
+
+impl View for VDeployment {
+    type V = spec_types::VDeploymentView;
+
+    spec fn view(&self) -> spec_types::VDeploymentView;
+}
+
+impl VDeployment {
+    #[verifier(external_body)]
+    pub fn metadata(&self) -> (metadata: ObjectMeta)
+        ensures metadata@ == self@.metadata,
+    {
+        ObjectMeta::from_kube(self.inner.metadata.clone())
+    }
+
+    #[verifier(external_body)]
+    pub fn spec(&self) -> (spec: VDeploymentSpec)
+        ensures spec@ == self@.spec,
+    {
+        VDeploymentSpec { inner: self.inner.spec.clone() }
+    }
+
+    #[verifier(external_body)]
+    pub fn api_resource() -> (res: ApiResource)
+        ensures [email protected] == spec_types::VDeploymentView::kind(),
+    {
+        ApiResource::from_kube(deps_hack::kube::api::ApiResource::erase::<deps_hack::VDeployment>(&()))
+    }
+
+    #[verifier(external_body)]
+    pub fn controller_owner_ref(&self) -> (owner_reference: OwnerReference)
+        ensures owner_reference@ == self@.controller_owner_ref(),
+    {
+        // We can safely unwrap here because the trait method implementation always returns a Some(...)
+        OwnerReference::from_kube(self.inner.controller_owner_ref(&()).unwrap())
+    }
+
+    // NOTE: This function assumes serde_json::to_string won't fail!
+    #[verifier(external_body)]
+    pub fn marshal(self) -> (obj: DynamicObject)
+        ensures obj@ == self@.marshal(),
+    {
+        // TODO: this might be unnecessarily slow
+        DynamicObject::from_kube(deps_hack::k8s_openapi::serde_json::from_str(&deps_hack::k8s_openapi::serde_json::to_string(&self.inner).unwrap()).unwrap())
+    }
+
+    #[verifier(external_body)]
+    pub fn unmarshal(obj: DynamicObject) -> (res: Result<VDeployment, UnmarshalError>)
+        ensures
+            res.is_Ok() == spec_types::VDeploymentView::unmarshal(obj@).is_Ok(),
+            res.is_Ok() ==> res.get_Ok_0()@ == spec_types::VDeploymentView::unmarshal(obj@).get_Ok_0(),
+    {
+        let parse_result = obj.into_kube().try_parse::<deps_hack::VDeployment>();
+        if parse_result.is_ok() {
+            let res = VDeployment { inner: parse_result.unwrap() };
+            Ok(res)
+        } else {
+            Err(())
+        }
+    }
+}
+
+#[verifier(external)]
+impl ResourceWrapper<deps_hack::VDeployment> for VDeployment {
+    fn from_kube(inner: deps_hack::VDeployment) -> VDeployment { VDeployment { inner: inner } }
+
+    fn into_kube(self) -> deps_hack::VDeployment { self.inner }
+}
+
+#[verifier(external_body)]
+pub struct VDeploymentSpec {
+    inner: deps_hack::VDeploymentSpec,
+}
+
+impl VDeploymentSpec {
+    pub spec fn view(&self) -> spec_types::VDeploymentSpecView;
+
+    #[verifier(external_body)]
+    pub fn replicas(&self) -> (replicas: Option<i32>)
+        ensures
+            replicas.is_Some() == self@.replicas.is_Some(),
+            replicas.is_Some() ==> replicas.get_Some_0() as int == self@.replicas.get_Some_0(),
+    {
+        self.inner.replicas
+    }
+
+    #[verifier(external_body)]
+    pub fn selector(&self) -> (selector: LabelSelector)
+        ensures selector@ == self@.selector
+    {
+        LabelSelector::from_kube(self.inner.selector.clone())
+    }
+
+    #[verifier(external_body)]
+    pub fn template(&self) -> (template: Option<PodTemplateSpec>)
+        ensures
+            template.is_Some() == self@.template.is_Some(),
+            template.is_Some() ==> template.get_Some_0()@ == self@.template.get_Some_0(),
+    {
+        match &self.inner.template {
+            Some(t) => Some(PodTemplateSpec::from_kube(t.clone())),
+            None => None
+        }
+    }
+}
+
+}

src/v2/controllers/vdeployment_controller/trusted/mod.rs

@@ -0,0 +1,5 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+pub mod exec_types;
+pub mod spec_types;
+pub mod step;

src/v2/controllers/vdeployment_controller/trusted/spec_types.rs

@@ -0,0 +1,160 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::error::*;
+use crate::kubernetes_api_objects::spec::{
+    api_resource::*, label_selector::*, pod_template_spec::*, prelude::*,
+};
+use crate::kubernetes_cluster::spec::{cluster::*, message::*};
+use crate::vdeployment_controller::trusted::step::*;
+use crate::vstd_ext::string_view::*;
+use vstd::prelude::*;
+
+verus! {
+
+pub struct VDeploymentView {
+    pub metadata: ObjectMetaView,
+    pub spec: VDeploymentSpecView,
+    pub status: Option<VDeploymentStatusView>,
+}
+
+pub type VDeploymentStatusView = EmptyStatusView;
+
+impl VDeploymentView {
+    pub open spec fn well_formed(self) -> bool {
+        &&& self.metadata.well_formed()
+        &&& self.state_validation()
+    }
+
+    pub open spec fn controller_owner_ref(self) -> OwnerReferenceView {
+        OwnerReferenceView {
+            block_owner_deletion: Some(true),
+            controller: Some(true),
+            kind: Self::kind(),
+            name: self.metadata.name.get_Some_0(),
+            uid: self.metadata.uid.get_Some_0(),
+        }
+    }
+}
+
+impl ResourceView for VDeploymentView {
+    type Spec = VDeploymentSpecView;
+    type Status = Option<VDeploymentStatusView>;
+
+    open spec fn default() -> VDeploymentView {
+        VDeploymentView {
+            metadata: ObjectMetaView::default(),
+            spec: arbitrary(), // TODO: specify the default value for spec
+            status: None,
+        }
+    }
+
+    open spec fn metadata(self) -> ObjectMetaView { self.metadata }
+
+    open spec fn kind() -> Kind { Kind::CustomResourceKind("vdeployment"@) }
+
+    open spec fn object_ref(self) -> ObjectRef {
+        ObjectRef {
+            kind: Self::kind(),
+            name: self.metadata.name.get_Some_0(),
+            namespace: self.metadata.namespace.get_Some_0(),
+        }
+    }
+
+    proof fn object_ref_is_well_formed() {}
+
+    open spec fn spec(self) -> VDeploymentSpecView { self.spec }
+
+    open spec fn status(self) -> Option<VDeploymentStatusView> { self.status }
+
+    open spec fn marshal(self) -> DynamicObjectView {
+        DynamicObjectView {
+            kind: Self::kind(),
+            metadata: self.metadata,
+            spec: VDeploymentView::marshal_spec(self.spec),
+            status: VDeploymentView::marshal_status(self.status),
+        }
+    }
+
+    open spec fn unmarshal(obj: DynamicObjectView) -> Result<VDeploymentView, UnmarshalError> {
+        if obj.kind != Self::kind() {
+            Err(())
+        } else if !VDeploymentView::unmarshal_spec(obj.spec).is_Ok() {
+            Err(())
+        } else if !VDeploymentView::unmarshal_status(obj.status).is_Ok() {
+            Err(())
+        } else {
+            Ok(VDeploymentView {
+                metadata: obj.metadata,
+                spec: VDeploymentView::unmarshal_spec(obj.spec).get_Ok_0(),
+                status: VDeploymentView::unmarshal_status(obj.status).get_Ok_0(),
+            })
+        }
+    }
+
+    proof fn marshal_preserves_integrity() {
+        VDeploymentView::marshal_spec_preserves_integrity();
+        VDeploymentView::marshal_status_preserves_integrity();
+    }
+
+    proof fn marshal_preserves_metadata() {}
+
+    proof fn marshal_preserves_kind() {}
+
+    closed spec fn marshal_spec(s: VDeploymentSpecView) -> Value;
+
+    closed spec fn unmarshal_spec(v: Value) -> Result<VDeploymentSpecView, UnmarshalError>;
+
+    closed spec fn marshal_status(s: Option<VDeploymentStatusView>) -> Value;
+
+    closed spec fn unmarshal_status(v: Value) -> Result<Option<VDeploymentStatusView>, UnmarshalError>;
+
+    #[verifier(external_body)]
+    proof fn marshal_spec_preserves_integrity() {}
+
+    #[verifier(external_body)]
+    proof fn marshal_status_preserves_integrity() {}
+
+    proof fn unmarshal_result_determined_by_unmarshal_spec_and_status() {}
+
+    // TODO: keep it consistent with k8s's Deployment
+    open spec fn state_validation(self) -> bool {
+        // replicas is non-negative
+        &&& self.spec.replicas.is_Some() ==> self.spec.replicas.get_Some_0() >= 0
+        // selector exists, and its match_labels is not empty
+        // TODO: revise it after supporting selector.match_expressions
+        &&& self.spec.selector.match_labels.is_Some()
+        &&& self.spec.selector.match_labels.get_Some_0().len() > 0
+        // template and its metadata ane spec exists
+        &&& self.spec.template.is_Some()
+        &&& self.spec.template.get_Some_0().metadata.is_Some()
+        &&& self.spec.template.get_Some_0().spec.is_Some()
+        // selector matches template's metadata's labels
+        &&& self.spec.selector.matches(self.spec.template.get_Some_0().metadata.get_Some_0().labels.unwrap_or(Map::empty()))
+    }
+
+    open spec fn transition_validation(self, old_obj: VDeploymentView) -> bool {
+        true
+    }
+}
+
+impl CustomResourceView for VDeploymentView {
+    proof fn kind_is_custom_resource() {}
+
+    open spec fn spec_status_validation(obj_spec: Self::Spec, obj_status: Self::Status) -> bool {
+        VDeploymentView {
+            metadata: arbitrary(),
+            spec: obj_spec,
+            status: obj_status,
+        }.state_validation()
+    }
+
+    proof fn validation_result_determined_by_spec_and_status() {}
+}
+
+pub struct VDeploymentSpecView {
+    pub replicas: Option<int>,
+    pub selector: LabelSelectorView,
+    pub template: Option<PodTemplateSpecView>,
+}
+
+}