From 9a90faf314aea49511590db7dc17676317a1c468 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Mon, 15 Jul 2024 19:44:57 -0500 Subject: [PATCH] Fix zk controller proof Signed-off-by: Xudong Sun --- .../proof/helper_invariants/owner_ref.rs | 17 ++++++- .../proof/helper_invariants/predicate.rs | 8 +-- .../proof/helper_invariants/proof.rs | 45 +++++++++++++++-- .../proof/helper_invariants/unchangeable.rs | 8 ++- .../proof/helper_invariants/validation.rs | 4 ++ .../proof/liveness/proof.rs | 3 ++ .../proof/liveness/resource_match.rs | 50 +++++++++++++------ .../proof/liveness/spec.rs | 15 +++++- .../proof/liveness/stateful_set_match.rs | 6 +++ .../proof/liveness/zookeeper_api.rs | 31 ++++++++++-- .../proof/builtin_controllers.rs | 7 +-- 11 files changed, 156 insertions(+), 38 deletions(-) diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs index 794c7f36b..7951a4ae0 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs @@ -7,6 +7,7 @@ use crate::kubernetes_api_objects::spec::{ stateful_set::*, }; use crate::kubernetes_cluster::spec::{ + api_server::state_machine::generated_name_is_unique, builtin_controllers::types::BuiltinControllerChoice, cluster::*, cluster_state_machine::Step, @@ -131,14 +132,26 @@ pub proof fn lemma_always_every_owner_ref_of_every_object_in_etcd_has_different_ let next = |s, s_prime| { &&& ZKCluster::next()(s, s_prime) &&& object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, zookeeper)(s) + &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s) }; lemma_always_object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(spec, sub_resource, zookeeper); - combine_spec_entails_always_n!(spec, lift_action(next), lift_action(ZKCluster::next()), lift_state(object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, zookeeper))); + lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, zookeeper); + combine_spec_entails_always_n!(spec, lift_action(next), lift_action(ZKCluster::next()), + lift_state(object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, zookeeper)), + lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)) + ); let resource_key = get_request(sub_resource, zookeeper).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| ZKCluster::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, ZKCluster::init(), next, inv); diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs index c5368c0ab..a9f6df120 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs @@ -229,12 +229,8 @@ 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, zookeeper: ZookeeperClusterView) -> StatePred { - |s: ZKCluster| { - forall |msg: ZKMessage| !{ - &&& s.in_flight().contains(msg) - &&& #[trigger] resource_create_request_msg_with_empty_name(get_request(sub_resource, zookeeper).key.kind, get_request(sub_resource, zookeeper).key.namespace)(msg) - } - } + let resource_key = get_request(sub_resource, zookeeper).key; + ZKCluster::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, zookeeper: ZookeeperClusterView) -> StatePred { diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs index bbbe9dc13..7cec0d302 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs @@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{ api_method::*, common::*, owner_reference::*, prelude::*, resource::*, }; use crate::kubernetes_cluster::spec::{ + api_server::state_machine::generated_name_is_unique, cluster::*, cluster_state_machine::Step, controller::types::{ControllerActionInput, ControllerStep}, @@ -168,9 +169,10 @@ pub proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_u match step { Step::ApiServerStep(input) => { let req = input.get_Some_0(); - assert(!resource_delete_request_msg(get_request(SubResource::ConfigMap, zookeeper).key)(req)); - assert(!resource_update_status_request_msg(get_request(SubResource::ConfigMap, zookeeper).key)(req)); - if resource_update_request_msg(get_request(SubResource::ConfigMap, zookeeper).key)(req) {} else {} + assert(!resource_delete_request_msg(cm_key)(req)); + assert(!resource_update_status_request_msg(cm_key)(req)); + generated_name_is_unique(s.kubernetes_api_state); + if resource_update_request_msg(cm_key)(req) {} else {} }, _ => {}, } @@ -191,6 +193,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))), spec.entails(always(tla_forall(|res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper))))), spec.entails(always(tla_forall(|res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper))))), + spec.entails(always(tla_forall(|res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper))))), spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))), spec.entails(always(tla_forall(|res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper))))), spec.entails(always(tla_forall(|res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper))))), @@ -198,6 +201,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource { always_tla_forall_apply(spec, |res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper)), SubResource::ConfigMap); always_tla_forall_apply(spec, |res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper)), SubResource::ConfigMap); + always_tla_forall_apply(spec, |res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), SubResource::ConfigMap); always_tla_forall_apply(spec, |res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper)), SubResource::ConfigMap); always_tla_forall_apply(spec, |res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), SubResource::ConfigMap); lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd(spec, zookeeper); @@ -216,6 +220,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))), spec.entails(always(lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)))), spec.entails(always(lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)))), + spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)))), spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))), spec.entails(always(lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)))), spec.entails(always(lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)))), @@ -232,6 +237,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource &&& ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(key)(s_prime) &&& no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)(s) &&& no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)(s) + &&& no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)(s) &&& object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)(s) &&& resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)(s) }; @@ -246,6 +252,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource later(lift_state(ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(key))), lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)), lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)), + lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)), lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)), lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)) ); @@ -293,6 +300,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource assert(!resource_delete_request_msg(resource_key)(req_msg)); assert(!resource_update_request_msg(resource_key)(req_msg)); assert(!resource_update_status_request_msg(resource_key)(req_msg)); + assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req_msg)); match req_msg.content.get_APIRequest_0() { APIRequest::CreateRequest(_) => { if !s.in_flight().contains(msg) { @@ -336,6 +344,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))), spec.entails(always(tla_forall(|res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper))))), spec.entails(always(tla_forall(|res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper))))), + spec.entails(always(tla_forall(|res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper))))), spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))), spec.entails(always(tla_forall(|res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper))))), spec.entails(always(tla_forall(|res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper))))), @@ -343,6 +352,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource { always_tla_forall_apply(spec, |res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper)), SubResource::ConfigMap); always_tla_forall_apply(spec, |res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper)), SubResource::ConfigMap); + always_tla_forall_apply(spec, |res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), SubResource::ConfigMap); always_tla_forall_apply(spec, |res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper)), SubResource::ConfigMap); always_tla_forall_apply(spec, |res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), SubResource::ConfigMap); lemma_eventually_always_object_in_response_at_after_update_resource_step_is_same_as_etcd(spec, zookeeper); @@ -361,6 +371,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))), spec.entails(always(lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)))), spec.entails(always(lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)))), + spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)))), spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))), spec.entails(always(lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)))), spec.entails(always(lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)))), @@ -377,6 +388,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource &&& ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(key)(s_prime) &&& no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)(s) &&& no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)(s) + &&& no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)(s) &&& object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)(s) &&& resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)(s) }; @@ -391,6 +403,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource later(lift_state(ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(key))), lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)), lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)), + lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)), lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)), lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)) ); @@ -438,6 +451,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource let req_msg = input.get_Some_0(); assert(!resource_delete_request_msg(resource_key)(req_msg)); assert(!resource_update_status_request_msg(resource_key)(req_msg)); + assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req_msg)); match req_msg.content.get_APIRequest_0() { APIRequest::UpdateRequest(_) => { if !s.in_flight().contains(msg) { @@ -999,15 +1013,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, zookeeper); lemma_always_resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(spec, sub_resource, zookeeper); + lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, zookeeper); let stronger_next = |s, s_prime| { &&& ZKCluster::next()(s, s_prime) &&& resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, zookeeper)(s) + &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s) }; combine_spec_entails_always_n!( spec, lift_action(stronger_next), lift_action(ZKCluster::next()), - lift_state(resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, zookeeper)) + lift_state(resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, zookeeper)), + lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)) ); + let resource_key = get_request(sub_resource, zookeeper).key; + assert forall |s, s_prime| inv(s) && #[trigger] stronger_next(s, s_prime) implies inv(s_prime) by { + let step = choose |step| ZKCluster::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, ZKCluster::init(), stronger_next, inv); } @@ -1405,12 +1433,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, zookeeper))))), spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper))))), 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, zookeeper))))), + spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))))), 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, zookeeper))))))), { 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, zookeeper))))) by { always_tla_forall_apply(spec, |res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), sub_resource); always_tla_forall_apply(spec, |res: SubResource|lift_state(every_resource_create_request_implies_at_after_create_resource_step(res, zookeeper)), 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, zookeeper)), sub_resource); + always_tla_forall_apply(spec, |res: SubResource|lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), sub_resource); lemma_eventually_always_resource_object_only_has_owner_reference_pointing_to_current_cr(spec, sub_resource, zookeeper); } 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, zookeeper))); @@ -1427,6 +1457,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, zookeeper)))), spec.entails(always(lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))), spec.entails(always(lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, zookeeper)))), + spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))), ensures spec.entails(true_pred().leads_to(always(lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper))))), { let key = get_request(sub_resource, zookeeper).key; @@ -1438,11 +1469,13 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po let state = |s: ZKCluster| { ZKCluster::desired_state_is(zookeeper)(s) && resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)(s) + && no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s) }; invariant_n!( spec, lift_state(state), lift_state(ZKCluster::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(ZKCluster::garbage_collector_deletion_enabled(key))), lift_state(ZKCluster::desired_state_is(zookeeper)), - lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)) + lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)), + lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)) ); ZKCluster::lemma_eventually_objects_owner_references_satisfies(spec, key, eventual_owner_ref); temp_pred_equality( @@ -1481,6 +1514,7 @@ pub proof fn lemma_eventually_always_stateful_set_not_exists_or_matches_or_no_mo spec.entails(always(lift_state(cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))), spec.entails(always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper)))), spec.entails(always(lift_state(no_update_status_request_msg_not_from_bc_in_flight_of_stateful_set(zookeeper)))), + spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_action(cm_rv_stays_unchanged(zookeeper)))), ensures spec.entails(true_pred().leads_to(always(lift_state(stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))))), { @@ -1591,6 +1625,7 @@ pub proof fn lemma_always_cm_rv_stays_unchanged(spec: TempPred, zooke let req = input.get_Some_0(); assert(!resource_delete_request_msg(cm_key)(req)); assert(!resource_update_status_request_msg(cm_key)(req)); + generated_name_is_unique(s.kubernetes_api_state); if resource_update_request_msg(cm_key)(req) {} else {} }, _ => {}, diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs index 987a453aa..64f847810 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs @@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{ api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*, }; use crate::kubernetes_cluster::spec::{ + api_server::state_machine::generated_name_is_unique, cluster::*, cluster_state_machine::Step, controller::types::{ControllerActionInput, ControllerStep}, @@ -128,6 +129,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred {} } diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs index ff2645f8d..dd2b70e63 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs @@ -7,6 +7,7 @@ use crate::kubernetes_api_objects::spec::{ stateful_set::*, }; use crate::kubernetes_cluster::spec::{ + api_server::state_machine::generated_name_is_unique, cluster::*, cluster_state_machine::Step, controller::types::{ControllerActionInput, ControllerStep}, @@ -101,6 +102,7 @@ pub proof fn lemma_always_stateful_set_in_etcd_satisfies_unchangeable(spec: Temp assert(owner_refs.get_Some_0()[0] != ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0().controller_owner_ref()); } } else if s.resources()[key] != s_prime.resources()[key] { + generated_name_is_unique(s.kubernetes_api_state); assert(s.resources()[key].metadata.uid == s_prime.resources()[key].metadata.uid); assert(ZookeeperClusterView::unmarshal(s.resources()[key]).get_Ok_0().controller_owner_ref() == ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0().controller_owner_ref()); assert(ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0() @@ -114,6 +116,7 @@ pub proof fn lemma_always_stateful_set_in_etcd_satisfies_unchangeable(spec: Temp let req = input.get_Some_0(); if resource_create_request_msg(sts_key)(req) {} else {} if resource_update_request_msg(sts_key)(req) {} else {} + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -305,6 +308,7 @@ proof fn lemma_always_stateful_set_in_create_request_msg_satisfies_unchangeable( assert(s.controller_state == s_prime.controller_state); assert(s.in_flight().contains(msg)); if s.resources().contains_key(key) { + generated_name_is_unique(s.kubernetes_api_state); assert(ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0() .transition_validation(ZookeeperClusterView::unmarshal(s.resources()[key]).get_Ok_0())); } else { diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs index c5d57af70..377d7766f 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs @@ -380,6 +380,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred, sub spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper))))), spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(res, zookeeper))))), spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(res, zookeeper))))), + spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper))))), ensures spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))), @@ -388,6 +389,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred, sub spec.entails(always(lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))), { always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(res, zookeeper)), sub_resource); always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(res, zookeeper)), sub_resource); @@ -396,6 +398,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred, sub always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), sub_resource); always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(res, zookeeper)), sub_resource); always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(res, zookeeper)), sub_resource); + always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), sub_resource); } } diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs index fd9ae2625..63ae78bd2 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs @@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{ api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*, }; use crate::kubernetes_cluster::spec::{ + api_server::state_machine::generated_name_is_unique, builtin_controllers::types::BuiltinControllerChoice, cluster::*, cluster_state_machine::Step, @@ -43,6 +44,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches( spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::no_update_status_request_msg_in_flight_of_except_stateful_set(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(sub_resource, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))), spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)))), @@ -99,6 +101,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))), spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))), ensures spec.entails( @@ -445,6 +448,7 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou spec.entails(always(lift_state(ZKCluster::crash_disabled()))), spec.entails(always(lift_state(ZKCluster::busy_disabled()))), spec.entails(always(lift_state(ZKCluster::every_in_flight_msg_has_unique_id()))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))), ensures spec.entails( @@ -461,12 +465,13 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou )) ), { + let resource_key = get_request(sub_resource, zookeeper).key; let pre = |s: ZKCluster| { - &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key) + &&& !s.resources().contains_key(resource_key) &&& req_msg_is_the_in_flight_pending_req_at_after_get_resource_step(sub_resource, zookeeper, req_msg)(s) }; let post = |s: ZKCluster| { - &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key) + &&& !s.resources().contains_key(resource_key) &&& at_after_get_resource_step_and_exists_not_found_resp_in_flight(sub_resource, zookeeper)(s) }; let input = Some(req_msg); @@ -475,6 +480,7 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou &&& ZKCluster::crash_disabled()(s) &&& ZKCluster::busy_disabled()(s) &&& ZKCluster::every_in_flight_msg_has_unique_id()(s) + &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s) &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)(s) }; combine_spec_entails_always_n!( @@ -483,6 +489,7 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou lift_state(ZKCluster::crash_disabled()), lift_state(ZKCluster::busy_disabled()), lift_state(ZKCluster::every_in_flight_msg_has_unique_id()), + lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)), lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)) ); @@ -490,7 +497,8 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou let step = choose |step| ZKCluster::next_step(s, s_prime, step); match step { Step::ApiServerStep(input) => { - assert(!resource_create_request_msg(get_request(sub_resource, zookeeper).key)(input.get_Some_0())); + assert(!resource_create_request_msg(resource_key)(input.get_Some_0())); + assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0())); if input.get_Some_0() == req_msg { let resp_msg = ZKCluster::handle_get_request_msg(req_msg, s.kubernetes_api_state).1; assert({ @@ -532,6 +540,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step( spec.entails(always(lift_state(ZKCluster::each_object_in_etcd_is_well_formed()))), spec.entails(always(lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))), spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))), ensures @@ -547,14 +556,15 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step( })) ), { + let resource_key = get_request(sub_resource, zookeeper).key; let pre = |s: ZKCluster| { - &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key) + &&& !s.resources().contains_key(resource_key) &&& resp_msg_is_the_in_flight_resp_at_after_get_resource_step(sub_resource, zookeeper, resp_msg)(s) &&& resp_msg.content.get_get_response().res.is_Err() &&& resp_msg.content.get_get_response().res.get_Err_0().is_ObjectNotFound() }; let post = |s: ZKCluster| { - &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key) + &&& !s.resources().contains_key(resource_key) &&& pending_req_in_flight_at_after_create_resource_step(sub_resource, zookeeper)(s) }; let input = (Some(resp_msg), Some(zookeeper.object_ref())); @@ -565,6 +575,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step( &&& ZKCluster::each_object_in_etcd_is_well_formed()(s) &&& ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) &&& ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())(s) + &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s) &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)(s) &&& helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)(s) }; @@ -577,6 +588,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step( lift_state(ZKCluster::each_object_in_etcd_is_well_formed()), lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())), + lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)), lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)), lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)) ); @@ -585,7 +597,8 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step( let step = choose |step| ZKCluster::next_step(s, s_prime, step); match step { Step::ApiServerStep(input) => { - assert(!resource_create_request_msg(get_request(sub_resource, zookeeper).key)(input.get_Some_0())); + assert(!resource_create_request_msg(resource_key)(input.get_Some_0())); + assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0())); }, _ => {} } @@ -608,6 +621,7 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step( spec.entails(always(lift_state(ZKCluster::each_object_in_etcd_is_well_formed()))), spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))), spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))), ensures spec.entails( @@ -622,8 +636,9 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step( ) ), { + let resource_key = get_request(sub_resource, zookeeper).key; let pre = |s: ZKCluster| { - &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key) + &&& !s.resources().contains_key(resource_key) &&& req_msg_is_the_in_flight_pending_req_at_after_create_resource_step(sub_resource, zookeeper, req_msg)(s) }; let input = Some(req_msg); @@ -635,6 +650,7 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step( &&& ZKCluster::each_object_in_etcd_is_well_formed()(s) &&& helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())(s) &&& helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)(s) + &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s) &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)(s) }; combine_spec_entails_always_n!( @@ -646,6 +662,7 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step( lift_state(ZKCluster::each_object_in_etcd_is_well_formed()), lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())), lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)), + lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)), lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)) ); @@ -671,7 +688,8 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step( let step = choose |step| ZKCluster::next_step(s, s_prime, step); match step { Step::ApiServerStep(input) => { - if resource_create_request_msg(get_request(sub_resource, zookeeper).key)(input.get_Some_0()) {} else {} + if resource_create_request_msg(resource_key)(input.get_Some_0()) {} else {} + if resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0()) {} else {} }, _ => {}, } @@ -847,6 +865,7 @@ proof fn lemma_resource_state_matches_at_after_update_resource_step(spec: TempPr assert(!resource_delete_request_msg(resource_key)(input.get_Some_0())); assert(!resource_update_status_request_msg(resource_key)(input.get_Some_0())); if resource_update_request_msg(resource_key)(input.get_Some_0()) {} else {} + generated_name_is_unique(s.kubernetes_api_state); }, _ => {}, } @@ -881,6 +900,7 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(spec: let pre = resp_msg_is_the_in_flight_ok_resp_at_after_get_resource_step(sub_resource, zookeeper, resp_msg); let post = pending_req_in_flight_at_after_update_resource_step(sub_resource, zookeeper); let input = (Some(resp_msg), Some(zookeeper.object_ref())); + let resource_key = get_request(sub_resource, zookeeper).key; let stronger_next = |s, s_prime: ZKCluster| { &&& ZKCluster::next()(s, s_prime) &&& ZKCluster::crash_disabled()(s) @@ -917,9 +937,10 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(spec: match step { Step::ApiServerStep(input) => { let req = input.get_Some_0(); - assert(!resource_update_status_request_msg(get_request(sub_resource, zookeeper).key)(req)); - assert(!resource_delete_request_msg(get_request(sub_resource, zookeeper).key)(req)); - if resource_update_request_msg(get_request(sub_resource, zookeeper).key)(req) {} else {} + assert(!resource_update_status_request_msg(resource_key)(req)); + assert(!resource_delete_request_msg(resource_key)(req)); + if resource_update_request_msg(resource_key)(req) {} else {} + generated_name_is_unique(s.kubernetes_api_state); }, _ => {}, } @@ -968,9 +989,10 @@ pub proof fn lemma_resource_object_is_stable(spec: TempPred, sub_reso match step { Step::ApiServerStep(input) => { let req = input.get_Some_0(); - assert(!resource_delete_request_msg(get_request(sub_resource, zookeeper).key)(req)); - assert(!resource_update_status_request_msg(get_request(sub_resource, zookeeper).key)(req)); - if resource_update_request_msg(get_request(sub_resource, zookeeper).key)(req) {} else {} + assert(!resource_delete_request_msg(resource_key)(req)); + assert(!resource_update_status_request_msg(resource_key)(req)); + if resource_update_request_msg(resource_key)(req) {} else {} + generated_name_is_unique(s.kubernetes_api_state); }, _ => {}, } diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs b/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs index 35fe922d2..8299ee76e 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs @@ -230,6 +230,7 @@ pub open spec fn derived_invariants_since_beginning(zookeeper: ZookeeperClusterV .and(always(tla_forall(|res: SubResource| lift_state(ZKCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(get_request(res, zookeeper).key))))) .and(always(lift_state(helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(zookeeper)))) .and(always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper))))) + .and(always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))))) } pub proof fn derived_invariants_since_beginning_is_stable(zookeeper: ZookeeperClusterView) @@ -241,6 +242,7 @@ pub proof fn derived_invariants_since_beginning_is_stable(zookeeper: ZookeeperCl let a_to_p_4 = |res: SubResource| lift_state(helper_invariants::response_at_after_get_resource_step_is_resource_get_response(res, zookeeper)); let a_to_p_5 = |res: SubResource| lift_state(ZKCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(get_request(res, zookeeper).key)); let a_to_p_6 = |sub_resource: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)); + let a_to_p_7 = |sub_resource: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)); stable_and_always_n!( lift_state(ZKCluster::every_in_flight_msg_has_unique_id()), lift_state(ZKCluster::object_in_ok_get_response_has_smaller_rv_than_etcd()), @@ -268,7 +270,8 @@ pub proof fn derived_invariants_since_beginning_is_stable(zookeeper: ZookeeperCl tla_forall(a_to_p_4), tla_forall(a_to_p_5), lift_state(helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(zookeeper)), - tla_forall(a_to_p_6) + tla_forall(a_to_p_6), + tla_forall(a_to_p_7) ); } @@ -535,6 +538,13 @@ pub proof fn sm_spec_entails_all_invariants(zookeeper: ZookeeperClusterView) } spec_entails_always_tla_forall(spec, a_to_p_6); }); + let a_to_p_7 = |sub_resource: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)); + assert_by(spec.entails(always(tla_forall(a_to_p_7))), { + assert forall |sub_resource: SubResource| spec.entails(always(#[trigger] a_to_p_7(sub_resource))) by { + helper_invariants::lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, zookeeper); + } + spec_entails_always_tla_forall(spec, a_to_p_7); + }); entails_always_and_n!( spec, @@ -564,7 +574,8 @@ pub proof fn sm_spec_entails_all_invariants(zookeeper: ZookeeperClusterView) tla_forall(a_to_p_4), tla_forall(a_to_p_5), lift_state(helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(zookeeper)), - tla_forall(a_to_p_6) + tla_forall(a_to_p_6), + tla_forall(a_to_p_7) ); } diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs b/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs index 37b008d32..389c8b070 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs @@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{ api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*, }; use crate::kubernetes_cluster::spec::{ + api_server::state_machine::generated_name_is_unique, builtin_controllers::types::BuiltinControllerChoice, cluster::*, cluster_state_machine::Step, @@ -41,6 +42,7 @@ pub proof fn lemma_from_after_get_stateful_set_step_to_stateful_set_matches( spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper)))), spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(SubResource::StatefulSet, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))), spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(SubResource::StatefulSet, zookeeper)))), @@ -256,6 +258,7 @@ proof fn lemma_from_key_exists_to_receives_ok_resp_at_after_get_stateful_set_ste assert(!resource_delete_request_msg(resource_key)(req)); assert(!resource_update_request_msg(resource_key)(req)); assert(!resource_update_status_request_msg(resource_key)(req)); + generated_name_is_unique(s.kubernetes_api_state); if input.get_Some_0() == req_msg { let resp_msg = ZKCluster::handle_get_request_msg(req_msg, s.kubernetes_api_state).1; assert({ @@ -374,6 +377,7 @@ proof fn lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_ste assert(!resource_delete_request_msg(resource_key)(req)); assert(!resource_update_request_msg(resource_key)(req)); assert(!resource_update_status_request_msg(resource_key)(req)); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -471,6 +475,7 @@ proof fn lemma_stateful_set_state_matches_at_after_update_stateful_set_step(spec assert(!resource_delete_request_msg(resource_key)(req)); assert(!resource_update_status_request_msg(resource_key)(req)); if resource_update_request_msg(resource_key)(req) {} else {} + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -520,6 +525,7 @@ pub proof fn lemma_stateful_set_is_stable( let req = input.get_Some_0(); assert(!resource_delete_request_msg(resource_key)(req)); if resource_update_request_msg(resource_key)(req) {} else {} + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs b/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs index a93a2fd3b..1a1a11f9c 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs @@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{ api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*, }; use crate::kubernetes_cluster::spec::{ + api_server::state_machine::generated_name_is_unique, builtin_controllers::types::BuiltinControllerChoice, cluster::*, cluster_state_machine::Step, @@ -41,6 +42,7 @@ pub proof fn lemma_from_after_exists_stateful_set_step_to_after_get_stateful_set spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(SubResource::StatefulSet, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::StatefulSet, zookeeper)))), @@ -82,6 +84,7 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_not_exists_to_after_g spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))), spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))), ensures spec.entails( lift_state(|s: ZKCluster| { @@ -160,6 +163,7 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_exists_to_after_get_s spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))), spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(SubResource::StatefulSet, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(SubResource::StatefulSet, zookeeper)))), spec.entails(always(lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::StatefulSet, zookeeper)))), @@ -494,6 +498,7 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state spec.entails(always(lift_state(ZKCluster::busy_disabled()))), spec.entails(always(lift_state(ZKCluster::every_in_flight_msg_has_unique_id()))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))), ensures spec.entails( lift_state(|s: ZKCluster| { @@ -506,12 +511,13 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state })) ), { + let key = get_request(SubResource::StatefulSet, zookeeper).key; let pre = |s: ZKCluster| { - &&& !s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key) + &&& !s.resources().contains_key(key) &&& req_msg_is_the_in_flight_pending_req_at_after_exists_stateful_set_step(zookeeper, req_msg)(s) }; let post = |s: ZKCluster| { - &&& !s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key) + &&& !s.resources().contains_key(key) &&& at_after_exists_stateful_set_step_and_exists_not_found_resp_in_flight(zookeeper)(s) }; let input = Some(req_msg); @@ -521,6 +527,7 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state &&& ZKCluster::busy_disabled()(s) &&& ZKCluster::every_in_flight_msg_has_unique_id()(s) &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)(s) + &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)(s) }; combine_spec_entails_always_n!( spec, lift_action(stronger_next), @@ -528,14 +535,16 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state lift_state(ZKCluster::crash_disabled()), lift_state(ZKCluster::busy_disabled()), lift_state(ZKCluster::every_in_flight_msg_has_unique_id()), - lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)) + lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)), + lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)) ); assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by { let step = choose |step| ZKCluster::next_step(s, s_prime, step); match step { Step::ApiServerStep(input) => { - assert(!resource_create_request_msg(get_request(SubResource::StatefulSet, zookeeper).key)(input.get_Some_0())); + assert(!resource_create_request_msg(key)(input.get_Some_0())); + assert(!resource_create_request_msg_with_empty_name(key.kind, key.namespace)(input.get_Some_0())); if input.get_Some_0() == req_msg { let resp_msg = ZKCluster::handle_get_request_msg(req_msg, s.kubernetes_api_state).1; assert({ @@ -574,6 +583,7 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_ spec.entails(always(lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))), spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))), spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))), + spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))), ensures spec.entails( lift_state(|s: ZKCluster| { @@ -602,6 +612,7 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_ &&& ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) &&& ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())(s) &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)(s) + &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)(s) }; combine_spec_entails_always_n!( @@ -613,7 +624,8 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_ lift_state(ZKCluster::every_in_flight_req_msg_has_different_id_from_pending_req_msg_of(zookeeper.object_ref())), lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())), - lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)) + lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)), + lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)) ); assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by { @@ -622,6 +634,7 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_ Step::ApiServerStep(input) => { let sts_key = get_request(SubResource::StatefulSet, zookeeper).key; assert(!resource_create_request_msg(sts_key)(input.get_Some_0())); + assert(!resource_create_request_msg_with_empty_name(sts_key.kind, sts_key.namespace)(input.get_Some_0())); }, _ => {} } @@ -868,6 +881,7 @@ proof fn lemma_from_pending_req_to_receives_ok_resp_at_after_exists_zk_node_step Step::ApiServerStep(input) => { assert(!resource_delete_request_msg(resource_key)(input.get_Some_0())); assert(!resource_update_request_msg(resource_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -960,6 +974,7 @@ proof fn lemma_from_after_exists_zk_node_step_to_after_update_zk_node_step(spec: Step::ApiServerStep(input) => { assert(!resource_delete_request_msg(sts_key)(input.get_Some_0())); assert(!resource_update_request_msg(sts_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -1045,6 +1060,7 @@ proof fn lemma_from_pending_req_to_receives_ok_resp_at_after_update_zk_node_step Step::ApiServerStep(input) => { assert(!resource_delete_request_msg(sts_key)(input.get_Some_0())); assert(!resource_update_request_msg(sts_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -1199,6 +1215,7 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_zk_no Step::ApiServerStep(input) => { assert(!resource_delete_request_msg(sts_key)(input.get_Some_0())); assert(!resource_update_request_msg(sts_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -1291,6 +1308,7 @@ proof fn lemma_from_after_exists_zk_node_step_to_after_create_zk_parent_node_ste let sts_key = get_request(SubResource::StatefulSet, zookeeper).key; assert(!resource_delete_request_msg(sts_key)(input.get_Some_0())); assert(!resource_update_request_msg(sts_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -1386,6 +1404,7 @@ proof fn lemma_from_pending_req_to_receives_ok_or_already_exists_resp_at_after_c let sts_key = get_request(SubResource::StatefulSet, zookeeper).key; assert(!resource_delete_request_msg(sts_key)(input.get_Some_0())); assert(!resource_update_request_msg(sts_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); } _ => {} } @@ -1482,6 +1501,7 @@ proof fn lemma_from_after_create_zk_parent_node_step_to_after_create_zk_node_ste Step::ApiServerStep(input) => { assert(!resource_delete_request_msg(sts_key)(input.get_Some_0())); assert(!resource_update_request_msg(sts_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } @@ -1567,6 +1587,7 @@ proof fn lemma_from_pending_req_to_receives_ok_resp_at_after_create_zk_node_step Step::ApiServerStep(input) => { assert(!resource_delete_request_msg(sts_key)(input.get_Some_0())); assert(!resource_update_request_msg(sts_key)(input.get_Some_0())); + generated_name_is_unique(s.kubernetes_api_state); }, _ => {} } diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs index bb61334f3..b17403aaf 100644 --- a/src/kubernetes_cluster/proof/builtin_controllers.rs +++ b/src/kubernetes_cluster/proof/builtin_controllers.rs @@ -51,9 +51,10 @@ pub open spec fn no_create_msg_that_uses_generate_name( kind: Kind, namespace: StringView ) -> StatePred { |s: Self| { - forall |msg: MsgType| - #[trigger] resource_create_request_msg_with_empty_name(kind, namespace)(msg) - ==> !s.in_flight().contains(msg) + forall |msg: MsgType| !{ + &&& s.in_flight().contains(msg) + &&& #[trigger] resource_create_request_msg_with_empty_name(kind, namespace)(msg) + } } }