Add fields and methods to ServicePort and ContainerPort (anvil-verifier#434)

Add more fields, their setter and getter methods to `ServicePort` and
`ContainerPort`.

---------

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

Author: euclidgame

.github/workflows/ci.yml

@@ -34,7 +34,7 @@ jobs:
           source ../tools/activate
           vargo build --release
       - name: Verify fluent controller
-        run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh fluent_controller.rs --time
+        run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh fluent_controller.rs --time --rlimit 20
   rabbitmq-verification:
     runs-on: ubuntu-20.04
     steps:
@@ -57,7 +57,7 @@ jobs:
           source ../tools/activate
           vargo build --release
       - name: Verify rabbitmq controller
-        run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh rabbitmq_controller.rs --time
+        run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh rabbitmq_controller.rs --time --rlimit 20
   zookeeper-verification:
     runs-on: ubuntu-20.04
     steps:
@@ -80,7 +80,7 @@ jobs:
           source ../tools/activate
           vargo build --release
       - name: Verify zookeeper controller
-        run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh zookeeper_controller.rs --time
+        run: VERUS_DIR="$(dirname "${PWD}")/verus" ./build.sh zookeeper_controller.rs --time --rlimit 20
   unit-tests:
     runs-on: ubuntu-20.04
     steps:

src/kubernetes_api_objects/exec/container.rs

@@ -185,6 +185,33 @@ impl ContainerPort {
         self.inner.name = Some(name.into_rust_string());
     }
 
+    #[verifier(external_body)]
+    pub fn name(&self) -> (name: Option<String>)
+        ensures opt_string_to_view(&name) == self@.name,
+    {
+        match &self.inner.name {
+            Some(s) => Some(String::from_rust_string(s.clone())),
+            None => None,
+        }
+    }
+
+    #[verifier(external_body)]
+    pub fn container_port(&self) -> (container_port: i32)
+        ensures container_port == self@.container_port,
+    {
+        self.inner.container_port
+    }
+
+    #[verifier(external_body)]
+    pub fn protocol(&self) -> (protocol: Option<String>)
+        ensures opt_string_to_view(&protocol) == self@.protocol,
+    {
+        match &self.inner.protocol {
+            Some(s) => Some(String::from_rust_string(s.clone())),
+            None => None,
+        }
+    }
+
     #[verifier(external)]
     pub fn from_kube(inner: deps_hack::k8s_openapi::api::core::v1::ContainerPort) -> ContainerPort { ContainerPort { inner: inner } }
 

src/kubernetes_api_objects/exec/service.rs

@@ -266,6 +266,13 @@ impl ServicePort {
         self.inner.app_protocol = Some(app_protocol.into_rust_string());
     }
 
+    #[verifier(external_body)]
+    pub fn set_protocol(&mut self, protocol: String)
+        ensures self@ == old(self)@.set_protocol(protocol@),
+    {
+        self.inner.protocol = Some(protocol.into_rust_string());
+    }
+
     #[verifier(external)]
     pub fn from_kube(inner: deps_hack::k8s_openapi::api::core::v1::ServicePort) -> ServicePort { ServicePort { inner: inner } }
 

src/kubernetes_api_objects/spec/container.rs

@@ -183,13 +183,15 @@ impl LifecycleHandlerView {
 pub struct ContainerPortView {
     pub container_port: int,
     pub name: Option<StringView>,
+    pub protocol: Option<StringView>,
 }
 
 impl ContainerPortView {
     pub open spec fn default() -> ContainerPortView {
         ContainerPortView {
             container_port: 0, // TODO: is this the correct default value?
             name: None,
+            protocol: None,
         }
     }
 
@@ -206,6 +208,13 @@ impl ContainerPortView {
             ..self
         }
     }
+
+    pub open spec fn set_protocol(self, protocol: StringView) -> ContainerPortView {
+        ContainerPortView {
+            protocol: Some(protocol),
+            ..self
+        }
+    }
 }
 
 pub struct VolumeMountView {

src/kubernetes_api_objects/spec/service.rs

@@ -192,6 +192,7 @@ pub struct ServicePortView {
     pub name: Option<StringView>,
     pub port: int,
     pub app_protocol: Option<StringView>,
+    pub protocol: Option<StringView>,
 }
 
 impl ServicePortView {
@@ -200,6 +201,7 @@ impl ServicePortView {
             name: None,
             port: 0, // TODO: is this the correct default value?
             app_protocol: None,
+            protocol: None,
         }
     }
 
@@ -223,6 +225,13 @@ impl ServicePortView {
             ..self
         }
     }
+
+    pub open spec fn set_protocol(self, protocol: StringView) -> ServicePortView {
+        ServicePortView {
+            protocol: Some(protocol),
+            ..self
+        }
+    }
 }
 
 }