Add ports field to FluentBitSpec (anvil-verifier#435)

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

Author: euclidgame

deploy/fluent/crd.yaml

@@ -1560,6 +1560,32 @@ spec:
                     type: string
                   default: {}
                   type: object
+                ports:
+                  items:
+                    description: ContainerPort represents a network port in a single container.
+                    properties:
+                      containerPort:
+                        description: "Number of port to expose on the pod's IP address. This must be a valid port number, 0 < x < 65536."
+                        format: int32
+                        type: integer
+                      hostIP:
+                        description: What host IP to bind the external port to.
+                        type: string
+                      hostPort:
+                        description: "Number of port to expose on the host. If specified, this must be a valid port number, 0 < x < 65536. If HostNetwork is specified, this must match ContainerPort. Most containers do not need this."
+                        format: int32
+                        type: integer
+                      name:
+                        description: "If specified, this must be an IANA_SVC_NAME and unique within the pod. Each named port in a pod must have a unique name. Name for the port that can be referred to by services."
+                        type: string
+                      protocol:
+                        description: "Protocol for port. Must be UDP, TCP, or SCTP. Defaults to \"TCP\".\n\n"
+                        type: string
+                    required:
+                      - containerPort
+                    type: object
+                  nullable: true
+                  type: array
                 positionDB:
                   description: Represents a host path mapped into a pod. Host path volumes do not support ownership management or SELinux relabeling.
                   nullable: true

e2e/src/fluent_e2e.rs

@@ -35,6 +35,12 @@ pub fn fluent_bit() -> String {
         image: kubesphere/fluent-bit:v2.1.7
         tolerations:
             - operator: Exists
+        ports:
+            - name: forward
+              containerPort: 24224
+              protocol: TCP
+            - containerPort: 8443
+              name: https
     "
     .to_string()
 }

src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs

@@ -249,7 +249,11 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
                 volume_mounts
             });
             fb_container.set_ports({
-                let mut ports = Vec::new();
+                let mut ports = if fb.spec().ports().is_some() {
+                        fb.spec().ports().unwrap()
+                    } else {
+                        Vec::new()
+                    };
                 let metrics_port = if fb.spec().metrics_port().is_some() { fb.spec().metrics_port().unwrap() } else { 2020 };
                 ports.push(ContainerPort::new_with(new_strlit("metrics").to_string(), metrics_port));
                 proof {
@@ -340,7 +344,7 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
                 volume
             });
         }
-        
+
         proof {
             assert_seqs_equal!(
                 volumes@.map_values(|vol: Volume| vol@),
@@ -389,5 +393,4 @@ fn make_env(fb: &FluentBit) -> (env_vars: Vec<EnvVar>)
     env_vars
 }
 
-
 }

src/controller_examples/fluent_controller/fluentbit/exec/resource/service.rs

@@ -131,17 +131,25 @@ pub fn make_service(fb: &FluentBit) -> (service: Service)
     service.set_spec({
         let mut service_spec = ServiceSpec::default();
         service_spec.set_ports({
-            let mut ports = Vec::new();
-            ports.push({
-                let mut port = ServicePort::default();
-                port.set_name(new_strlit("metrics").to_string());
-                if fb.spec().metrics_port().is_some() {
-                    port.set_port(fb.spec().metrics_port().unwrap());
+            let mut ports = if fb.spec().ports().is_some() {
+                    make_new_ports(fb.spec().ports().unwrap())
                 } else {
-                    port.set_port(2020);
-                }
-                port
-            });
+                    Vec::new()
+                };
+            let mut port = ServicePort::default();
+            port.set_name(new_strlit("metrics").to_string());
+            if fb.spec().metrics_port().is_some() {
+                port.set_port(fb.spec().metrics_port().unwrap());
+            } else {
+                port.set_port(2020);
+            }
+            proof {
+                assert_seqs_equal!(
+                    ports@.map_values(|port: ServicePort| port@).push(port@),
+                    model_resource::make_service(fb@).spec.get_Some_0().ports.get_Some_0()
+                );
+            }
+            ports.push(port);
             proof {
                 assert_seqs_equal!(
                     ports@.map_values(|port: ServicePort| port@),
@@ -156,4 +164,55 @@ pub fn make_service(fb: &FluentBit) -> (service: Service)
     service
 }
 
+fn make_new_ports(ports: Vec<ContainerPort>) -> (service_ports: Vec<ServicePort>)
+    ensures service_ports@.map_values(|p: ServicePort| p@) == ports@.map_values(|p: ContainerPort| model_resource::make_service_port(p@)),
+{
+    let mut service_ports = Vec::new();
+    let mut i = 0;
+    proof {
+        assert_seqs_equal!(
+            service_ports@.map_values(|p: ServicePort| p@),
+            Seq::new(i as nat, |k: int| model_resource::make_service_port(ports[k]@))
+        );
+    }
+    while i < ports.len()
+        invariant
+            i <= ports@.len(),
+            service_ports@.map_values(|p: ServicePort| p@) == Seq::new(i as nat, |k: int| model_resource::make_service_port(ports[k]@)),
+        ensures
+            service_ports@.map_values(|p: ServicePort| p@) == Seq::new(ports@.len(), |k: int| model_resource::make_service_port(ports[k]@)),
+    {
+        let port = &ports[i];
+        let mut service_port = ServicePort::default();
+        service_port.set_port(port.container_port());
+        if port.name().is_some() {
+            service_port.set_name(port.name().unwrap());
+        }
+        if port.protocol().is_some() {
+            service_port.set_protocol(port.protocol().unwrap());
+        }
+        service_ports.push(service_port);
+        proof {
+            assert(service_port@ == model_resource::make_service_port(port@));
+            assert_seqs_equal!(
+                service_ports@.map_values(|p: ServicePort| p@),
+                Seq::new(i as nat, |k: int| model_resource::make_service_port(ports[k]@)).push(service_port@)
+            );
+            assert_seqs_equal!(
+                Seq::new(i as nat, |k: int| model_resource::make_service_port(ports[k]@)).push(service_port@),
+                Seq::new((i + 1) as nat, |k: int| model_resource::make_service_port(ports[k]@))
+            );
+        }
+        i = i + 1;
+    }
+    proof {
+        assert_seqs_equal!(
+            ports@.map_values(|p: ContainerPort| model_resource::make_service_port(p@)),
+            Seq::new(ports@.len(), |k: int| model_resource::make_service_port(ports[k]@))
+        );
+    }
+    
+    service_ports
+}
+
 }

src/controller_examples/fluent_controller/fluentbit/model/resource/daemon_set.rs

@@ -238,14 +238,19 @@ pub open spec fn make_fluentbit_pod_spec(fb: FluentBitView) -> PodSpecView {
                         }
                     }
                 }),
-                ports: Some(seq![
-                    ContainerPortView::default()
+                ports: {
+                    let metrics_port = ContainerPortView::default()
                         .set_name(new_strlit("metrics")@)
                         .set_container_port({
                             let port = if fb.spec.metrics_port.is_Some() { fb.spec.metrics_port.get_Some_0() } else { 2020 };
                             port
-                        }),
-                ]),
+                        });
+                    if fb.spec.ports.is_Some() {
+                        Some(fb.spec.ports.get_Some_0().push(metrics_port))
+                    } else {
+                        Some(seq![metrics_port])
+                    }
+                },
                 resources: fb.spec.resources,
                 args: if fb.spec.args.is_Some() {
                         fb.spec.args

src/controller_examples/fluent_controller/fluentbit/model/resource/service.rs

@@ -101,22 +101,36 @@ pub open spec fn make_service(fb: FluentBitView) -> ServiceView {
             ..ObjectMetaView::default()
         },
         spec: Some(ServiceSpecView {
-            ports: Some(seq![
-                ServicePortView {
+            ports: {
+                let metrics_port = ServicePortView {
                     name: Some(new_strlit("metrics")@),
                     port: if fb.spec.metrics_port.is_Some() {
                         fb.spec.metrics_port.get_Some_0()
                     } else {
                         2020
                     },
                     ..ServicePortView::default()
+                };
+                if fb.spec.ports.is_Some() {
+                    Some(fb.spec.ports.get_Some_0().map_values(|p: ContainerPortView| make_service_port(p)).push(metrics_port))
+                } else {
+                    Some(seq![metrics_port])
                 }
-            ]),
+            },
             selector: Some(make_base_labels(fb)),
             ..ServiceSpecView::default()
         }),
         ..ServiceView::default()
     }
 }
 
+pub open spec fn make_service_port(port: ContainerPortView) -> ServicePortView {
+    ServicePortView {
+        port: port.container_port,
+        name: if port.name.is_Some() { port.name } else { ServicePortView::default().name },
+        protocol: if port.protocol.is_Some() { port.protocol } else { ServicePortView::default().protocol },
+        ..ServicePortView::default()
+    }
+}
+
 }

src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs

@@ -175,6 +175,7 @@ pub proof fn lemma_eventually_always_every_resource_update_request_implies_at_af
     leads_to_always_tla_forall_subresource(spec, true_pred(), |sub_resource: SubResource| lift_state(every_resource_update_request_implies_at_after_update_resource_step(sub_resource, fb)));
 }
 
+#[verifier(spinoff_prover)]
 pub proof fn make_fluentbit_pod_spec_determined_by_spec_and_name(fb1: FluentBitView, fb2: FluentBitView)
     requires 
         fb1.metadata.name.get_Some_0() == fb2.metadata.name.get_Some_0(),

src/controller_examples/fluent_controller/fluentbit/trusted/exec_types.rs

@@ -448,6 +448,18 @@ impl FluentBitSpec {
             None => None,
         }
     }
+
+    #[verifier(external_body)]
+    pub fn ports(&self) -> (ports: Option<Vec<ContainerPort>>)
+        ensures
+            self@.ports.is_Some() == ports.is_Some(),
+            ports.is_Some() ==> ports.get_Some_0()@.map_values(|c: ContainerPort| c@) == self@.ports.get_Some_0(),
+    {
+        match &self.inner.ports {
+            Some(ports) => Some(ports.clone().into_iter().map(|c: deps_hack::k8s_openapi::api::core::v1::ContainerPort| ContainerPort::from_kube(c)).collect()),
+            None => None,
+        }
+    }
 }
 
 }

src/controller_examples/fluent_controller/fluentbit/trusted/spec_types.rs

@@ -171,6 +171,7 @@ pub struct FluentBitSpecView {
     pub liveness_probe: Option<ProbeView>,
     pub readiness_probe: Option<ProbeView>,
     pub init_containers: Option<Seq<ContainerView>>,
+    pub ports: Option<Seq<ContainerPortView>>,
 }
 
 }

src/deps_hack/src/lib.rs

@@ -251,6 +251,7 @@ pub struct FluentBitSpec {
     pub readiness_probe: Option<k8s_openapi::api::core::v1::Probe>,
     #[serde(rename = "initContainers")]
     pub init_containers: Option<Vec<k8s_openapi::api::core::v1::Container>>,
+    pub ports: Option<Vec<k8s_openapi::api::core::v1::ContainerPort>>,
 }
 
 #[derive(