Support generate_name in the API server model

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

@@ -131,14 +131,26 @@ pub proof fn lemma_always_every_owner_ref_of_every_object_in_etcd_has_different_
     let next = |s, s_prime| {
         &&& FBCluster::next()(s, s_prime)
         &&& object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, fb)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb)(s)
     };
     lemma_always_object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(spec, sub_resource, fb);
-    combine_spec_entails_always_n!(spec, lift_action(next), lift_action(FBCluster::next()), lift_state(object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, fb)));
+    lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, fb);
+    combine_spec_entails_always_n!(spec, lift_action(next), lift_action(FBCluster::next()),
+        lift_state(object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, fb)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb))
+    );
     let resource_key = get_request(sub_resource, fb).key;
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         if s_prime.resources().contains_key(resource_key) {
             assert(s.kubernetes_api_state.uid_counter <= s_prime.kubernetes_api_state.uid_counter);
-            if !s.resources().contains_key(resource_key) || s.resources()[resource_key].metadata.owner_references != s_prime.resources()[resource_key].metadata.owner_references {} else {}
+            let step = choose |step| FBCluster::next_step(s, s_prime, step);
+            match step {
+                Step::ApiServerStep(input) => {
+                    assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0()));
+                    if !s.resources().contains_key(resource_key) || s.resources()[resource_key].metadata.owner_references != s_prime.resources()[resource_key].metadata.owner_references {} else {}
+                },
+                _ => {}
+            }
         }
     }
     init_invariant(spec, FBCluster::init(), next, inv);

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

@@ -193,6 +193,11 @@ pub open spec fn resource_object_only_has_owner_reference_pointing_to_current_cr
     }
 }
 
+pub open spec fn no_create_resource_request_msg_with_empty_name_in_flight(sub_resource: SubResource, fb: FluentBitView) -> StatePred<FBCluster> {
+    let resource_key = get_request(sub_resource, fb).key;
+    FBCluster::no_create_msg_that_uses_generate_name(resource_key.kind, resource_key.namespace)
+}
+
 pub open spec fn no_delete_resource_request_msg_in_flight(sub_resource: SubResource, fb: FluentBitView) -> StatePred<FBCluster> {
     |s: FBCluster| {
         forall |msg: FBMessage| !{

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

@@ -620,15 +620,29 @@ pub proof fn lemma_always_resource_object_has_no_finalizers_or_timestamp_and_onl
 {
     let inv = resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fb);
     lemma_always_resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(spec, sub_resource, fb);
+    lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, fb);
     let stronger_next = |s, s_prime| {
         &&& FBCluster::next()(s, s_prime)
         &&& resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, fb)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb)(s)
     };
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
         lift_action(FBCluster::next()),
-        lift_state(resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, fb))
+        lift_state(resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, fb)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb))
     );
+    let resource_key = get_request(sub_resource, fb).key;
+    assert forall |s, s_prime| inv(s) && #[trigger] stronger_next(s, s_prime) implies inv(s_prime) by {
+        let step = choose |step| FBCluster::next_step(s, s_prime, step);
+        match step {
+            Step::ApiServerStep(input) => {
+                let req_msg = input.get_Some_0();
+                assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req_msg));
+            }
+            _ => {}
+        }
+    }
     init_invariant(spec, FBCluster::init(), stronger_next, inv);
 }
 
@@ -912,12 +926,14 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
         spec.entails(always(tla_forall(|sub_resource: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fb))))),
         spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb))))),
         spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fb))))),
+        spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb))))),
     ensures spec.entails(true_pred().leads_to(always(tla_forall(|sub_resource: SubResource| (lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fb))))))),
 {
     assert forall |sub_resource: SubResource| spec.entails(true_pred().leads_to(always(lift_state(#[trigger] resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fb))))) by {
         always_tla_forall_apply(spec, |res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, fb)), sub_resource);
         always_tla_forall_apply(spec, |res: SubResource|lift_state(every_resource_create_request_implies_at_after_create_resource_step(res, fb)), sub_resource);
         always_tla_forall_apply(spec, |res: SubResource|lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, fb)), sub_resource);
+        always_tla_forall_apply(spec, |res: SubResource|lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, fb)), sub_resource);
         lemma_eventually_always_resource_object_only_has_owner_reference_pointing_to_current_cr(spec, sub_resource, fb);
     }
     leads_to_always_tla_forall_subresource(spec, true_pred(), |sub_resource: SubResource| lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fb)));
@@ -934,6 +950,7 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
         spec.entails(always(lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fb)))),
         spec.entails(always(lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb)))),
         spec.entails(always(lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fb)))),
+        spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb)))),
     ensures spec.entails(true_pred().leads_to(always(lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fb))))),
 {
     let key = get_request(sub_resource, fb).key;
@@ -979,6 +996,7 @@ pub proof fn lemma_eventually_always_daemon_set_not_exists_or_matches_or_no_more
         spec.entails(always(lift_state(every_resource_update_request_implies_at_after_update_resource_step(SubResource::DaemonSet, fb)))),
         spec.entails(always(lift_state(daemon_set_in_etcd_satisfies_unchangeable(fb)))),
         spec.entails(always(lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::DaemonSet, fb)))),
+        spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::DaemonSet, fb)))),
         spec.entails(always(lift_state(no_update_status_request_msg_not_from_bc_in_flight_of_daemon_set(fb)))),
     ensures spec.entails(true_pred().leads_to(always(lift_state(daemon_set_not_exists_or_matches_or_no_more_status_update(fb))))),
 {
@@ -1044,4 +1062,45 @@ pub proof fn lemma_eventually_always_daemon_set_not_exists_or_matches_or_no_more
     );
 }
 
+// We can probably hide a lof of spec functions to make this lemma faster
+pub proof fn lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec: TempPred<FBCluster>, sub_resource: SubResource, fb: FluentBitView)
+    requires
+        spec.entails(lift_state(FBCluster::init())),
+        spec.entails(always(lift_action(FBCluster::next()))),
+    ensures spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb)))),
+{
+    let key = fb.object_ref();
+    let resource_key = get_request(sub_resource, fb).key;
+    let inv = no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb);
+
+    assert forall |s: FBCluster| #[trigger] FBCluster::init()(s) implies inv(s) by {}
+
+    assert forall |s: FBCluster, s_prime: FBCluster| #[trigger] FBCluster::next()(s, s_prime) && inv(s) implies inv(s_prime) by {
+        assert forall |msg: FBMessage|
+            !(s_prime.in_flight().contains(msg) && #[trigger] resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(msg))
+        by {
+            let step = choose |step| FBCluster::next_step(s, s_prime, step);
+            match step {
+                Step::ApiServerStep(_) => {
+                    if !s.in_flight().contains(msg) && s_prime.in_flight().contains(msg) {
+                        assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(msg));
+                    }
+                },
+                Step::ControllerStep(_) => {
+                    if !s.in_flight().contains(msg) && s_prime.in_flight().contains(msg) {
+                        assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(msg));
+                    }
+                },
+                _ => {
+                    if !s.in_flight().contains(msg) && s_prime.in_flight().contains(msg) {
+                        assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(msg));
+                    }
+                },
+            }
+        }
+    }
+    init_invariant(spec, FBCluster::init(), FBCluster::next(), inv);
+}
+
+
 }

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

@@ -125,6 +125,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<F
         &&& object_in_resource_update_request_msg_has_smaller_rv_than_etcd(sub_resource, fb)(s)
         &&& object_in_every_create_request_msg_satisfies_unchangeable(sub_resource, fb)(s)
         &&& response_at_after_get_resource_step_is_resource_get_response(sub_resource, fb)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb)(s)
     };
     FBCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
     FBCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
@@ -133,6 +134,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<F
     lemma_always_object_in_resource_update_request_msg_has_smaller_rv_than_etcd(spec, sub_resource, fb);
     lemma_always_object_in_every_create_request_msg_satisfies_unchangeable(spec, sub_resource, fb);
     lemma_always_response_at_after_get_resource_step_is_resource_get_response(spec, sub_resource, fb);
+    lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, fb);
     combine_spec_entails_always_n!(
         spec, lift_action(next), lift_action(FBCluster::next()),
         lift_state(FBCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
@@ -141,7 +143,8 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<F
         lift_state(FBCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(resource_key)),
         lift_state(object_in_resource_update_request_msg_has_smaller_rv_than_etcd(sub_resource, fb)),
         lift_state(object_in_every_create_request_msg_satisfies_unchangeable(sub_resource, fb)),
-        lift_state(response_at_after_get_resource_step_is_resource_get_response(sub_resource, fb))
+        lift_state(response_at_after_get_resource_step_is_resource_get_response(sub_resource, fb)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb))
     );
     assert forall |s: FBCluster, s_prime: FBCluster| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         object_in_etcd_satisfies_unchangeable_induction(sub_resource, fb, s, s_prime);
@@ -161,6 +164,7 @@ pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubRe
         FBCluster::each_object_in_etcd_is_well_formed()(s_prime),
         object_in_resource_update_request_msg_has_smaller_rv_than_etcd(sub_resource, fb)(s),
         object_in_etcd_satisfies_unchangeable(sub_resource, fb)(s),
+        no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, fb)(s),
     ensures object_in_etcd_satisfies_unchangeable(sub_resource, fb)(s_prime),
 {
     let resource_key = get_request(sub_resource, fb).key;
@@ -189,6 +193,7 @@ pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubRe
             Step::ApiServerStep(input) => {
                 let req = input.get_Some_0();
                 if resource_update_request_msg(resource_key)(req) {} else {}
+                if resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req) {} else {}
             },
             _ => {}
         }

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

@@ -72,20 +72,23 @@ pub proof fn lemma_always_daemon_set_in_etcd_satisfies_unchangeable(spec: TempPr
         &&& daemon_set_in_create_request_msg_satisfies_unchangeable(fb)(s)
         &&& daemon_set_update_request_msg_does_not_change_owner_reference(fb)(s)
         &&& object_in_resource_update_request_msg_has_smaller_rv_than_etcd(SubResource::DaemonSet, fb)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(SubResource::DaemonSet, fb)(s)
     };
     FBCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
     always_to_always_later(spec, lift_state(FBCluster::each_object_in_etcd_is_well_formed()));
     lemma_always_every_owner_ref_of_every_object_in_etcd_has_different_uid_from_uid_counter(spec, ds_res, fb);
     lemma_always_daemon_set_in_create_request_msg_satisfies_unchangeable(spec, fb);
     lemma_always_daemon_set_update_request_msg_does_not_change_owner_reference(spec, fb);
     lemma_always_object_in_resource_update_request_msg_has_smaller_rv_than_etcd(spec, ds_res, fb);
+    lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, ds_res, fb);
     combine_spec_entails_always_n!(
         spec, lift_action(next), lift_action(FBCluster::next()), lift_state(FBCluster::each_object_in_etcd_is_well_formed()),
         later(lift_state(FBCluster::each_object_in_etcd_is_well_formed())),
         lift_state(every_owner_ref_of_every_object_in_etcd_has_different_uid_from_uid_counter(ds_res, fb)),
         lift_state(daemon_set_in_create_request_msg_satisfies_unchangeable(fb)),
         lift_state(daemon_set_update_request_msg_does_not_change_owner_reference(fb)),
-        lift_state(object_in_resource_update_request_msg_has_smaller_rv_than_etcd(SubResource::DaemonSet, fb))
+        lift_state(object_in_resource_update_request_msg_has_smaller_rv_than_etcd(SubResource::DaemonSet, fb)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::DaemonSet, fb))
     );
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         let key = fb.object_ref();
@@ -113,6 +116,7 @@ pub proof fn lemma_always_daemon_set_in_etcd_satisfies_unchangeable(spec: TempPr
                         let req = input.get_Some_0();
                         if resource_create_request_msg(ds_key)(req) {} else {}
                         if resource_update_request_msg(ds_key)(req) {} else {}
+                        if resource_create_request_msg_with_empty_name(ds_key.kind, ds_key.namespace)(req) {} else {}
                     },
                     _ => {}
                 }

src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs

@@ -42,6 +42,7 @@ pub proof fn lemma_from_after_get_daemon_set_step_to_daemon_set_matches(spec: Te
         spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::DaemonSet, fb)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::DaemonSet, fb)))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::DaemonSet, fb)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::DaemonSet, fb)))),
         spec.entails(always(lift_state(helper_invariants::daemon_set_in_etcd_satisfies_unchangeable(fb)))),
     ensures
         spec.entails(lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::DaemonSet, fb)).leads_to(lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb)))),