Skip to content

Commit

Permalink
Fix zk controller proof
Browse files Browse the repository at this point in the history 
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
@marshtompsxd
marshtompsxd committed Jul 16, 2024
1 parent e258faf commit 9a90faf
Show file tree
Hide file tree
Showing 11 changed files with 156 additions and 38 deletions.
17 changes: 15 additions & 2 deletions src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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);
Expand Down
8 changes: 2 additions & 6 deletions src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<ZKCluster> {
|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<ZKCluster> {
Expand Down
45 changes: 40 additions & 5 deletions src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
View file

Large diffs are not rendered by default.

8 changes: 7 additions & 1 deletion src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand Down Expand Up @@ -128,6 +129,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<Z
&&& object_in_every_create_request_msg_satisfies_unchangeable(sub_resource, zookeeper)(s)
&&& response_at_after_get_resource_step_is_resource_get_response(sub_resource, zookeeper)(s)
&&& the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())(s)
&&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
};
ZKCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
ZKCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
Expand All @@ -137,6 +139,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<Z
lemma_always_object_in_every_create_request_msg_satisfies_unchangeable(spec, sub_resource, zookeeper);
lemma_always_response_at_after_get_resource_step_is_resource_get_response(spec, sub_resource, zookeeper);
lemma_always_the_object_in_reconcile_satisfies_state_validation(spec, zookeeper.object_ref());
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(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
Expand All @@ -146,7 +149,8 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<Z
lift_state(object_in_resource_update_request_msg_has_smaller_rv_than_etcd(sub_resource, zookeeper)),
lift_state(object_in_every_create_request_msg_satisfies_unchangeable(sub_resource, zookeeper)),
lift_state(response_at_after_get_resource_step_is_resource_get_response(sub_resource, zookeeper)),
lift_state(the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref()))
lift_state(the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())),
lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))
);
assert forall |s: ZKCluster, s_prime: ZKCluster| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
object_in_etcd_satisfies_unchangeable_induction(sub_resource, zookeeper, s, s_prime);
Expand All @@ -166,6 +170,7 @@ pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubRe
ZKCluster::each_object_in_etcd_is_well_formed()(s_prime),
object_in_resource_update_request_msg_has_smaller_rv_than_etcd(sub_resource, zookeeper)(s),
object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)(s),
no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s),
ensures object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)(s_prime),
{
let resource_key = get_request(sub_resource, zookeeper).key;
Expand All @@ -187,6 +192,7 @@ pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubRe
let req = input.get_Some_0();
if resource_create_request_msg(resource_key)(req) {} else {}
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 {}
},
_ => {}
}
Expand Down
4 changes: 4 additions & 0 deletions src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand Down Expand Up @@ -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()
Expand All @@ -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);
},
_ => {}
}
Expand Down Expand Up @@ -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 {
Expand Down
3 changes: 3 additions & 0 deletions src/controller_examples/zookeeper_controller/proof/liveness/proof.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -380,6 +380,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred<ZKCluster>, 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)))),
Expand All @@ -388,6 +389,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred<ZKCluster>, 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);
Expand All @@ -396,6 +398,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred<ZKCluster>, 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);
}

}
Loading

0 comments on commit 9a90faf

Please sign in to comment.