Revert some format changes (anvil-verifier#438)

Signed-off-by: Xudong Sun <[email protected]>
xlab-uiuc · Nov 29, 2023 · 88998b4 · 88998b4
1 parent f077082
commit 88998b4
Show file tree

Hide file tree

Showing 47 changed files with 340 additions and 114 deletions.
diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs
@@ -6,8 +6,8 @@ use crate::fluent_controller::fluentbit::exec::resource::*;
 use crate::fluent_controller::fluentbit::model::reconciler as model_reconciler;
 use crate::fluent_controller::fluentbit::model::resource as model_resource;
 use crate::fluent_controller::fluentbit::trusted::{exec_types::*, spec_types, step::*};
-use crate::kubernetes_api_objects::exec::resource::ResourceWrapper;
 use crate::kubernetes_api_objects::exec::prelude::*;
+use crate::kubernetes_api_objects::exec::resource::ResourceWrapper;
 use crate::reconciler::exec::{io::*, reconciler::*, resource_builder::*};
 use crate::reconciler::spec::resource_builder::ResourceBuilder as SpecResourceBuilder;
 use crate::vstd_ext::{string_map::StringMap, string_view::*};
@@ -20,14 +20,22 @@ pub struct FluentBitReconciler {}
 impl Reconciler<FluentBit, FluentBitReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for FluentBitReconciler {
     open spec fn well_formed(fb: &FluentBit) -> bool { fb@.well_formed() }
 
-    fn reconcile_init_state() -> FluentBitReconcileState { reconcile_init_state() }
+    fn reconcile_init_state() -> FluentBitReconcileState {
+        reconcile_init_state()
+    }
 
-    fn reconcile_core(fb: &FluentBit, resp_o: Option<Response<EmptyType>>, state: FluentBitReconcileState) 
-    -> (FluentBitReconcileState, Option<Request<EmptyType>>) { reconcile_core(fb, resp_o, state) }
+    fn reconcile_core(fb: &FluentBit, resp_o: Option<Response<EmptyType>>, state: FluentBitReconcileState)
+    -> (FluentBitReconcileState, Option<Request<EmptyType>>) {
+        reconcile_core(fb, resp_o, state)
+    }
 
-    fn reconcile_done(state: &FluentBitReconcileState) -> bool { reconcile_done(state) }
+    fn reconcile_done(state: &FluentBitReconcileState) -> bool {
+        reconcile_done(state)
+    }
 
-    fn reconcile_error(state: &FluentBitReconcileState) -> bool { reconcile_error(state) }
+    fn reconcile_error(state: &FluentBitReconcileState) -> bool {
+        reconcile_error(state)
+    }
 }
 
 impl Default for FluentBitReconciler {
@@ -190,7 +198,11 @@ pub fn reconcile_helper<
                         let next_state = Builder::state_after_create(fb, resp_o.unwrap().into_k_response().into_create_response().res.unwrap(), state.clone());
                         if next_state.is_ok() {
                             let (state_prime, req) = next_state.unwrap();
-                            let req_o = if req.is_some() { Some(Request::KRequest(req.unwrap())) } else { None };
+                            let req_o = if req.is_some() {
+                                Some(Request::KRequest(req.unwrap()))
+                            } else {
+                                None
+                            };
                             return (state_prime, req_o);
                         }
                     }
@@ -208,7 +220,11 @@ pub fn reconcile_helper<
                         let next_state = Builder::state_after_update(fb, resp_o.unwrap().into_k_response().into_update_response().res.unwrap(), state.clone());
                         if next_state.is_ok() {
                             let (state_prime, req) = next_state.unwrap();
-                            let req_o = if req.is_some() { Some(Request::KRequest(req.unwrap())) } else { None };
+                            let req_o = if req.is_some() {
+                                Some(Request::KRequest(req.unwrap()))
+                            } else {
+                                None
+                            };
                             return (state_prime, req_o);
                         }
                     }

diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs b/src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs
@@ -24,7 +24,9 @@ verus! {
 pub struct DaemonSetBuilder {}
 
 impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::DaemonSetBuilder> for DaemonSetBuilder {
-    open spec fn requirements(fb: FluentBitView) -> bool { fb.well_formed() }
+    open spec fn requirements(fb: FluentBitView) -> bool {
+        fb.well_formed()
+    }
 
     fn get_request(fb: &FluentBit) -> KubeGetRequest {
         KubeGetRequest {
@@ -34,7 +36,9 @@ impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::DaemonS
         }
     }
 
-    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> { Ok(make_daemon_set(fb).marshal()) }
+    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> {
+        Ok(make_daemon_set(fb).marshal())
+    }
 
     fn update(fb: &FluentBit, state: &FluentBitReconcileState, obj: DynamicObject) -> Result<DynamicObject, ()> {
         let ds = DaemonSet::unmarshal(obj);
@@ -254,7 +258,11 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
                     } else {
                         Vec::new()
                     };
-                let metrics_port = if fb.spec().metrics_port().is_some() { fb.spec().metrics_port().unwrap() } else { 2020 };
+                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 {
                     assert_seqs_equal!(

diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/resource/role.rs b/src/controller_examples/fluent_controller/fluentbit/exec/resource/role.rs
@@ -25,7 +25,9 @@ verus! {
 pub struct RoleBuilder {}
 
 impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::RoleBuilder> for RoleBuilder {
-    open spec fn requirements(fb: FluentBitView) -> bool { fb.well_formed() }
+    open spec fn requirements(fb: FluentBitView) -> bool {
+        fb.well_formed()
+    }
 
     fn get_request(fb: &FluentBit) -> KubeGetRequest {
         KubeGetRequest {
@@ -35,7 +37,9 @@ impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::RoleBui
         }
     }
 
-    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> { Ok(make_role(fb).marshal()) }
+    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> {
+        Ok(make_role(fb).marshal())
+    }
 
     fn update(fb: &FluentBit, state: &FluentBitReconcileState, obj: DynamicObject) -> Result<DynamicObject, ()> {
         let role = Role::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/resource/role_binding.rs b/src/controller_examples/fluent_controller/fluentbit/exec/resource/role_binding.rs
@@ -27,7 +27,9 @@ verus! {
 pub struct RoleBindingBuilder {}
 
 impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::RoleBindingBuilder> for RoleBindingBuilder {
-    open spec fn requirements(fb: FluentBitView) -> bool { fb.well_formed() }
+    open spec fn requirements(fb: FluentBitView) -> bool {
+        fb.well_formed()
+    }
 
     fn get_request(fb: &FluentBit) -> KubeGetRequest {
         KubeGetRequest {
@@ -37,7 +39,9 @@ impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::RoleBin
         }
     }
 
-    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> { Ok(make_role_binding(fb).marshal()) }
+    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> {
+        Ok(make_role_binding(fb).marshal())
+    }
 
     fn update(fb: &FluentBit, state: &FluentBitReconcileState, obj: DynamicObject) -> Result<DynamicObject, ()> {
         let rb = RoleBinding::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/resource/service.rs b/src/controller_examples/fluent_controller/fluentbit/exec/resource/service.rs
@@ -25,7 +25,9 @@ verus! {
 pub struct ServiceBuilder {}
 
 impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::ServiceBuilder> for ServiceBuilder {
-    open spec fn requirements(fb: FluentBitView) -> bool { fb.well_formed() }
+    open spec fn requirements(fb: FluentBitView) -> bool {
+        fb.well_formed()
+    }
 
     fn get_request(fb: &FluentBit) -> KubeGetRequest {
         KubeGetRequest {
@@ -35,7 +37,9 @@ impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::Service
         }
     }
 
-    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> { Ok(make_service(fb).marshal()) }
+    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> {
+        Ok(make_service(fb).marshal())
+    }
 
     fn update(fb: &FluentBit, state: &FluentBitReconcileState, obj: DynamicObject) -> Result<DynamicObject, ()> {
         let service = Service::unmarshal(obj);
@@ -122,7 +126,9 @@ pub fn make_service(fb: &FluentBit) -> (service: Service)
         metadata.set_labels({
             if fb.spec().service_labels().len() > 0 {
                 fb.spec().service_labels()
-            } else { make_labels(fb) }
+            } else {
+                make_labels(fb)
+            }
         });
         metadata.set_annotations(fb.spec().service_annotations());
 
@@ -217,7 +223,7 @@ fn make_new_ports(ports: Vec<ContainerPort>) -> (service_ports: Vec<ServicePort>
             Seq::new(ports@.len(), |k: int| model_resource::make_service_port(ports[k]@))
         );
     }
-    
+
     service_ports
 }
 

diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/resource/service_account.rs b/src/controller_examples/fluent_controller/fluentbit/exec/resource/service_account.rs
@@ -25,7 +25,9 @@ verus! {
 pub struct ServiceAccountBuilder {}
 
 impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::ServiceAccountBuilder> for ServiceAccountBuilder {
-    open spec fn requirements(fb: FluentBitView) -> bool { fb.well_formed() }
+    open spec fn requirements(fb: FluentBitView) -> bool {
+        fb.well_formed()
+    }
 
     fn get_request(fb: &FluentBit) -> KubeGetRequest {
         KubeGetRequest {
@@ -35,7 +37,9 @@ impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::Service
         }
     }
 
-    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> { Ok(make_service_account(fb).marshal()) }
+    fn make(fb: &FluentBit, state: &FluentBitReconcileState) -> Result<DynamicObject, ()> {
+        Ok(make_service_account(fb).marshal())
+    }
 
     fn update(fb: &FluentBit, state: &FluentBitReconcileState, obj: DynamicObject) -> Result<DynamicObject, ()> {
         let sa = ServiceAccount::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit/model/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit/model/reconciler.rs
@@ -15,14 +15,22 @@ verus! {
 impl Reconciler<FluentBitView, EmptyAPI> for FluentBitReconciler {
     type T = FluentBitReconcileState;
 
-    open spec fn reconcile_init_state() -> FluentBitReconcileState { reconcile_init_state() }
+    open spec fn reconcile_init_state() -> FluentBitReconcileState {
+        reconcile_init_state()
+    }
 
-    open spec fn reconcile_core(fb: FluentBitView, resp_o: Option<ResponseView<EmptyTypeView>>, state: FluentBitReconcileState) 
-    -> (FluentBitReconcileState, Option<RequestView<EmptyTypeView>>) { reconcile_core(fb, resp_o, state) }
+    open spec fn reconcile_core(fb: FluentBitView, resp_o: Option<ResponseView<EmptyTypeView>>, state: FluentBitReconcileState)
+    -> (FluentBitReconcileState, Option<RequestView<EmptyTypeView>>) {
+        reconcile_core(fb, resp_o, state)
+    }
 
-    open spec fn reconcile_done(state: FluentBitReconcileState) -> bool { reconcile_done(state) }
+    open spec fn reconcile_done(state: FluentBitReconcileState) -> bool {
+        reconcile_done(state)
+    }
 
-    open spec fn reconcile_error(state: FluentBitReconcileState) -> bool { reconcile_error(state) }
+    open spec fn reconcile_error(state: FluentBitReconcileState) -> bool {
+        reconcile_error(state)
+    }
 
     open spec fn expect_from_user(obj: DynamicObjectView) -> bool { obj.kind == SecretView::kind() /* expect the user might create some secret object */ }
 }

diff --git a/src/controller_examples/fluent_controller/fluentbit/model/resource/daemon_set.rs b/src/controller_examples/fluent_controller/fluentbit/model/resource/daemon_set.rs
@@ -20,9 +20,13 @@ verus! {
 pub struct DaemonSetBuilder {}
 
 impl ResourceBuilder<FluentBitView, FluentBitReconcileState> for DaemonSetBuilder {
-    open spec fn get_request(fb: FluentBitView) -> GetRequest { GetRequest { key: make_daemon_set_key(fb) } }
+    open spec fn get_request(fb: FluentBitView) -> GetRequest {
+        GetRequest { key: make_daemon_set_key(fb) }
+    }
 
-    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> { Ok(make_daemon_set(fb).marshal()) }
+    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> {
+        Ok(make_daemon_set(fb).marshal())
+    }
 
     open spec fn update(fb: FluentBitView, state: FluentBitReconcileState, obj: DynamicObjectView) -> Result<DynamicObjectView, ()> {
         let ds = DaemonSetView::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit/model/resource/role.rs b/src/controller_examples/fluent_controller/fluentbit/model/resource/role.rs
@@ -20,9 +20,13 @@ verus! {
 pub struct RoleBuilder {}
 
 impl ResourceBuilder<FluentBitView, FluentBitReconcileState> for RoleBuilder {
-    open spec fn get_request(fb: FluentBitView) -> GetRequest { GetRequest { key: make_role_key(fb) } }
+    open spec fn get_request(fb: FluentBitView) -> GetRequest {
+        GetRequest { key: make_role_key(fb) }
+    }
 
-    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> { Ok(make_role(fb).marshal()) }
+    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> {
+        Ok(make_role(fb).marshal())
+    }
 
     open spec fn update(fb: FluentBitView, state: FluentBitReconcileState, obj: DynamicObjectView) -> Result<DynamicObjectView, ()> {
         let role = RoleView::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit/model/resource/role_binding.rs b/src/controller_examples/fluent_controller/fluentbit/model/resource/role_binding.rs
@@ -21,9 +21,13 @@ verus! {
 pub struct RoleBindingBuilder {}
 
 impl ResourceBuilder<FluentBitView, FluentBitReconcileState> for RoleBindingBuilder {
-    open spec fn get_request(fb: FluentBitView) -> GetRequest { GetRequest { key: make_role_binding_key(fb) } }
+    open spec fn get_request(fb: FluentBitView) -> GetRequest {
+        GetRequest { key: make_role_binding_key(fb) }
+    }
 
-    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> { Ok(make_role_binding(fb).marshal()) }
+    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> {
+        Ok(make_role_binding(fb).marshal())
+    }
 
     open spec fn update(fb: FluentBitView, state: FluentBitReconcileState, obj: DynamicObjectView) -> Result<DynamicObjectView, ()> {
         let rb = RoleBindingView::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit/model/resource/service.rs b/src/controller_examples/fluent_controller/fluentbit/model/resource/service.rs
@@ -20,9 +20,13 @@ verus! {
 pub struct ServiceBuilder {}
 
 impl ResourceBuilder<FluentBitView, FluentBitReconcileState> for ServiceBuilder {
-    open spec fn get_request(fb: FluentBitView) -> GetRequest { GetRequest { key: make_service_key(fb) } }
+    open spec fn get_request(fb: FluentBitView) -> GetRequest {
+        GetRequest { key: make_service_key(fb) }
+    }
 
-    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> { Ok(make_service(fb).marshal()) }
+    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> {
+        Ok(make_service(fb).marshal())
+    }
 
     open spec fn update(fb: FluentBitView, state: FluentBitReconcileState, obj: DynamicObjectView) -> Result<DynamicObjectView, ()> {
         let service = ServiceView::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit/model/resource/service_account.rs b/src/controller_examples/fluent_controller/fluentbit/model/resource/service_account.rs
@@ -18,9 +18,13 @@ verus! {
 pub struct ServiceAccountBuilder {}
 
 impl ResourceBuilder<FluentBitView, FluentBitReconcileState> for ServiceAccountBuilder {
-    open spec fn get_request(fb: FluentBitView) -> GetRequest { GetRequest { key: make_service_account_key(fb) }  }
+    open spec fn get_request(fb: FluentBitView) -> GetRequest {
+        GetRequest { key: make_service_account_key(fb) }
+    }
 
-    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> { Ok(make_service_account(fb).marshal()) }
+    open spec fn make(fb: FluentBitView, state: FluentBitReconcileState) -> Result<DynamicObjectView, ()> {
+        Ok(make_service_account(fb).marshal())
+    }
 
     open spec fn update(fb: FluentBitView, state: FluentBitReconcileState, obj: DynamicObjectView) -> Result<DynamicObjectView, ()> {
         let sa = ServiceAccountView::unmarshal(obj);

diff --git a/src/controller_examples/fluent_controller/fluentbit_config/exec/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit_config/exec/reconciler.rs
@@ -6,8 +6,8 @@ use crate::fluent_controller::fluentbit_config::exec::resource::*;
 use crate::fluent_controller::fluentbit_config::model::reconciler as model_reconciler;
 use crate::fluent_controller::fluentbit_config::model::resource as model_resource;
 use crate::fluent_controller::fluentbit_config::trusted::{exec_types::*, spec_types, step::*};
-use crate::kubernetes_api_objects::exec::resource::ResourceWrapper;
 use crate::kubernetes_api_objects::exec::prelude::*;
+use crate::kubernetes_api_objects::exec::resource::ResourceWrapper;
 use crate::reconciler::exec::{io::*, reconciler::*, resource_builder::*};
 use crate::reconciler::spec::resource_builder::ResourceBuilder as SpecResourceBuilder;
 use crate::vstd_ext::{string_map::StringMap, string_view::*};
@@ -20,14 +20,22 @@ pub struct FluentBitConfigReconciler {}
 impl Reconciler<FluentBitConfig, FluentBitConfigReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for FluentBitConfigReconciler {
     open spec fn well_formed(fbc: &FluentBitConfig) -> bool { fbc@.well_formed() }
 
-    fn reconcile_init_state() -> FluentBitConfigReconcileState { reconcile_init_state() }
+    fn reconcile_init_state() -> FluentBitConfigReconcileState {
+        reconcile_init_state()
+    }
 
-    fn reconcile_core(fbc: &FluentBitConfig, resp_o: Option<Response<EmptyType>>, state: FluentBitConfigReconcileState) 
-    -> (FluentBitConfigReconcileState, Option<Request<EmptyType>>) { reconcile_core(fbc, resp_o, state) }
+    fn reconcile_core(fbc: &FluentBitConfig, resp_o: Option<Response<EmptyType>>, state: FluentBitConfigReconcileState)
+    -> (FluentBitConfigReconcileState, Option<Request<EmptyType>>) {
+        reconcile_core(fbc, resp_o, state)
+    }
 
-    fn reconcile_done(state: &FluentBitConfigReconcileState) -> bool { reconcile_done(state) }
+    fn reconcile_done(state: &FluentBitConfigReconcileState) -> bool {
+        reconcile_done(state)
+    }
 
-    fn reconcile_error(state: &FluentBitConfigReconcileState) -> bool { reconcile_error(state) }
+    fn reconcile_error(state: &FluentBitConfigReconcileState) -> bool {
+        reconcile_error(state)
+    }
 }
 
 impl Default for FluentBitConfigReconciler {
@@ -157,7 +165,11 @@ pub fn reconcile_helper<
                         let next_state = Builder::state_after_create(fbc, resp_o.unwrap().into_k_response().into_create_response().res.unwrap(), state.clone());
                         if next_state.is_ok() {
                             let (state_prime, req) = next_state.unwrap();
-                            let req_o = if req.is_some() { Some(Request::KRequest(req.unwrap())) } else { None };
+                            let req_o = if req.is_some() {
+                                Some(Request::KRequest(req.unwrap()))
+                            } else {
+                                None
+                            };
                             return (state_prime, req_o);
                         }
                     }
@@ -175,7 +187,11 @@ pub fn reconcile_helper<
                         let next_state = Builder::state_after_update(fbc, resp_o.unwrap().into_k_response().into_update_response().res.unwrap(), state.clone());
                         if next_state.is_ok() {
                             let (state_prime, req) = next_state.unwrap();
-                            let req_o = if req.is_some() { Some(Request::KRequest(req.unwrap())) } else { None };
+                            let req_o = if req.is_some() {
+                                Some(Request::KRequest(req.unwrap()))
+                            } else {
+                                None
+                            };
                             return (state_prime, req_o);
                         }
                     }

diff --git a/src/controller_examples/fluent_controller/fluentbit_config/exec/resource/secret.rs b/src/controller_examples/fluent_controller/fluentbit_config/exec/resource/secret.rs
@@ -34,7 +34,9 @@ impl ResourceBuilder<FluentBitConfig, FluentBitConfigReconcileState, model_resou
         }
     }
 
-    fn make(fbc: &FluentBitConfig, state: &FluentBitConfigReconcileState) -> Result<DynamicObject, ()> { Ok(make_secret(fbc).marshal()) }
+    fn make(fbc: &FluentBitConfig, state: &FluentBitConfigReconcileState) -> Result<DynamicObject, ()> {
+        Ok(make_secret(fbc).marshal())
+    }
 
     fn update(fbc: &FluentBitConfig, state: &FluentBitConfigReconcileState, obj: DynamicObject) -> Result<DynamicObject, ()> {
         let secret = Secret::unmarshal(obj);