Skip to content

Commit

Permalink
Move some lemmas
Browse files Browse the repository at this point in the history 
Signed-off-by: Wenjie Ma <[email protected]>
  • Loading branch information
@euclidgame
euclidgame committed Aug 25, 2023
1 parent aec117e commit b4c5bf2
Show file tree
Hide file tree
Showing 2 changed files with 151 additions and 103 deletions.
139 changes: 36 additions & 103 deletions src/controller_examples/rabbitmq_controller/proof/safety.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,12 +54,12 @@ proof fn lemma_stateful_set_never_scaled_down_for_rabbitmq(spec: TempPred<RMQClu
let next = |s, s_prime| {
&&& RMQCluster::next()(s, s_prime)
&&& replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)(s)
&&& stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)(s)
&&& object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)(s)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime)
};
lemma_always_replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(spec, rabbitmq);
lemma_always_stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(spec, rabbitmq);
lemma_always_object_in_sts_update_request_has_smaller_rv_than_etcd(spec, rabbitmq);
RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
always_to_always_later(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()));
assert forall |s, s_prime| #[trigger] next(s, s_prime) implies stateful_set_not_scaled_down(rabbitmq)(s, s_prime) by {
Expand All @@ -76,13 +76,13 @@ proof fn lemma_stateful_set_never_scaled_down_for_rabbitmq(spec: TempPred<RMQClu
assert(replicas_of_stateful_set(s_prime.resource_obj_of(sts_key)) == replicas_of_stateful_set(input.content.get_update_request().obj));
assert(replicas_of_stateful_set(s_prime.resource_obj_of(sts_key)) >= replicas_of_stateful_set(s.resource_obj_of(sts_key)));
}
}
}
}
}
invariant_n!(
spec, lift_action(next), lift_action(inv),
lift_action(RMQCluster::next()), lift_state(replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)),
lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)),
lift_state(object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)),
lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed()))
);
}
Expand Down Expand Up @@ -373,32 +373,26 @@ proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_respons
init_invariant(spec, RMQCluster::init(), next, inv);
}

spec fn stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
spec fn object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
|s: RMQCluster| {
let sts_key = make_stateful_set_key(rabbitmq.object_ref());
let etcd_rv = s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0();
forall |msg: RMQMessage|
#[trigger] s.message_in_flight(msg)
==> (
sts_update_request_msg(rabbitmq.object_ref())(msg)
==> msg.content.get_update_request().obj.metadata.resource_version.is_Some()
&& msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter
) && (
ok_sts_get_response_msg(rabbitmq.object_ref())(msg)
==> msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.is_Some()
&& msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter
)
&& sts_update_request_msg(rabbitmq.object_ref())(msg)
==> msg.content.get_update_request().obj.metadata.resource_version.is_Some()
&& msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter
}
}

proof fn lemma_always_stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(
proof fn lemma_always_object_in_sts_update_request_has_smaller_rv_than_etcd(
spec: TempPred<RMQCluster>, rabbitmq: RabbitmqClusterView
)
requires
spec.entails(lift_state(RMQCluster::init())),
spec.entails(always(lift_action(RMQCluster::next()))),
ensures
spec.entails(always(lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)))),
spec.entails(always(lift_state(object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)))),
{
let key = rabbitmq.object_ref();
let sts_key = make_stateful_set_key(rabbitmq.object_ref());
Expand All @@ -407,46 +401,40 @@ proof fn lemma_always_stateful_set_in_get_response_and_update_request_have_no_la
==> msg.content.get_update_request().obj.metadata.resource_version.is_Some()
&& msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter
};
let get_rv_leq = |msg: RMQMessage, s: RMQCluster| {
ok_sts_get_response_msg(rabbitmq.object_ref())(msg)
==> msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.is_Some()
&& msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter
};
let inv = stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq);
let inv = object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq);
let next = |s, s_prime| {
&&& RMQCluster::next()(s, s_prime)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime)
&&& response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)(s)
&&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
&&& RMQCluster::object_in_ok_get_response_has_lower_rv_than_etcd(sts_key)(s)
};
RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
lemma_always_response_at_after_get_stateful_set_step_is_sts_get_response(spec, rabbitmq);
always_to_always_later(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()));
RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
RMQCluster::lemma_always_object_in_ok_get_response_has_lower_rv_than_etcd(spec, sts_key);
combine_spec_entails_always_n!(
spec, lift_action(next), lift_action(RMQCluster::next()),
lift_state(RMQCluster::each_object_in_etcd_is_well_formed()),
later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed())),
lift_state(response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)),
lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata())
lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
lift_state(RMQCluster::object_in_ok_get_response_has_lower_rv_than_etcd(sts_key))
);
assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
let etcd_rv = s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0();
assert forall |msg| #[trigger] s_prime.message_in_flight(msg) implies upd_rv_leq(msg, s_prime) && get_rv_leq(msg, s_prime) by {
assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && sts_update_request_msg(rabbitmq.object_ref())(msg) implies
msg.content.get_update_request().obj.metadata.resource_version.is_Some()
&& msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s_prime.kubernetes_api_state.resource_version_counter by {
let step = choose |step| RMQCluster::next_step(s, s_prime, step);
if s.message_in_flight(msg) {
assert(s.kubernetes_api_state.resource_version_counter <= s_prime.kubernetes_api_state.resource_version_counter);
} else if sts_update_request_msg(rabbitmq.object_ref())(msg) {
lemma_stateful_set_update_request_msg_implies_key_in_reconcile_equals(key, s, s_prime, msg, step);
assert(at_rabbitmq_step(key, RabbitmqReconcileStep::AfterUpdateStatefulSet)(s_prime));
} else if ok_sts_get_response_msg(rabbitmq.object_ref())(msg) {
let input = step.get_KubernetesAPIStep_0().get_Some_0();
assert(s.resource_key_exists(input.content.get_get_request().key));
assert(input.content.get_get_request().key == sts_key);
assert(msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() == s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0());
assert(s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter);
}
}
}
}
init_invariant(spec, RMQCluster::init(), next, inv);
Expand Down Expand Up @@ -494,63 +482,6 @@ spec fn replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabb
}
}

spec fn helper_3_spec_ok_get_resp(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
|s: RMQCluster| {
let key = rabbitmq.object_ref();
let sts_key = make_stateful_set_key(key);
forall |msg|
#[trigger] s.message_in_flight(msg)
&& ok_sts_get_response_msg(key)(msg)
&& s.resource_key_exists(sts_key)
&& s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() == msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0()
==> s.resource_obj_of(sts_key) == msg.content.get_get_response().res.get_Ok_0()
}
}

proof fn lemma_always_helper_3_spec(spec: TempPred<RMQCluster>, rabbitmq: RabbitmqClusterView)
requires
spec.entails(lift_state(RMQCluster::init())),
spec.entails(always(lift_action(RMQCluster::next()))),
ensures
spec.entails(always(lift_state(helper_3_spec_ok_get_resp(rabbitmq)))),
{
let key = rabbitmq.object_ref();
let sts_key = make_stateful_set_key(key);
let inv = helper_3_spec_ok_get_resp(rabbitmq);
let next = |s, s_prime| {
&&& RMQCluster::next()(s, s_prime)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
&&& stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)(s)
};
RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
lemma_always_stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(spec, rabbitmq);
combine_spec_entails_always_n!(
spec, lift_action(next), lift_action(RMQCluster::next()), lift_state(RMQCluster::each_object_in_etcd_is_well_formed()),
lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq))
);
assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && ok_sts_get_response_msg(key)(msg) && s_prime.resource_key_exists(sts_key)
&& s_prime.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() == msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() implies s_prime.resource_obj_of(sts_key) == msg.content.get_get_response().res.get_Ok_0() by {
if s.message_in_flight(msg) {
if !s.resource_key_exists(sts_key) || s.resource_obj_of(sts_key) != s_prime.resource_obj_of(sts_key) {
assert(s_prime.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() != msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0())
}
} else {
let step = choose |step| RMQCluster::next_step(s, s_prime, step);
assert(step.is_KubernetesAPIStep());
let req = step.get_KubernetesAPIStep_0().get_Some_0();
assert(msg == RMQCluster::handle_get_request(req, s.kubernetes_api_state).1);
assert(s.resource_key_exists(req.content.get_get_request().key));
assert(msg.content.get_get_response().res.get_Ok_0() == s.resource_obj_of(req.content.get_get_request().key));
assert(req.content.get_get_request().key == msg.content.get_get_response().res.get_Ok_0().object_ref());
assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
assert(s_prime.resource_obj_of(sts_key) == msg.content.get_get_response().res.get_Ok_0());
}
}
}
init_invariant(spec, RMQCluster::init(), next, inv);
}

proof fn lemma_always_replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(spec: TempPred<RMQCluster>, rabbitmq: RabbitmqClusterView)
requires
spec.entails(lift_state(RMQCluster::init())),
Expand All @@ -559,50 +490,52 @@ proof fn lemma_always_replicas_of_stateful_set_update_request_msg_is_no_smaller_
spec.entails(always(lift_state(replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)))),
{
let inv = replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq);
let key = rabbitmq.object_ref();
let sts_key = make_stateful_set_key(key);
let next = |s, s_prime| {
&&& RMQCluster::next()(s, s_prime)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime)
&&& replicas_of_etcd_stateful_set_satisfies_order(rabbitmq)(s_prime)
&&& stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)(s)
&&& object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)(s)
&&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
&&& helper_3_spec_ok_get_resp(rabbitmq)(s)
&&& RMQCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(sts_key)(s)
&&& response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)(s)
};
RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
always_to_always_later(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()));
lemma_always_replicas_of_etcd_stateful_set_satisfies_order(spec, rabbitmq);
always_to_always_later(spec, lift_state(replicas_of_etcd_stateful_set_satisfies_order(rabbitmq)));
lemma_always_stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(spec, rabbitmq);
lemma_always_object_in_sts_update_request_has_smaller_rv_than_etcd(spec, rabbitmq);
RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
lemma_always_helper_3_spec(spec, rabbitmq);
RMQCluster::lemma_always_object_in_ok_get_resp_is_same_as_etcd_with_same_rv(spec, sts_key);
lemma_always_response_at_after_get_stateful_set_step_is_sts_get_response(spec, rabbitmq);
combine_spec_entails_always_n!(
spec, lift_action(next), lift_action(RMQCluster::next()),
lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed())),
later(lift_state(replicas_of_etcd_stateful_set_satisfies_order(rabbitmq))),
lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)),
lift_state(object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)),
lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
lift_state(helper_3_spec_ok_get_resp(rabbitmq)),
lift_state(RMQCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(sts_key)),
lift_state(response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq))
);
assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
helper_2(rabbitmq, s, s_prime);
replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd_induction(rabbitmq, s, s_prime);
}
init_invariant(spec, RMQCluster::init(), next, inv);
}


proof fn helper_2(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster)
proof fn replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd_induction(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster)
requires
RMQCluster::next()(s, s_prime),
RMQCluster::each_object_in_etcd_is_well_formed()(s),
RMQCluster::each_object_in_etcd_is_well_formed()(s_prime),
replicas_of_etcd_stateful_set_satisfies_order(rabbitmq)(s_prime),
replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)(s),
stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)(s),
object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)(s),
RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s),
helper_3_spec_ok_get_resp(rabbitmq)(s),
RMQCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(make_stateful_set_key(rabbitmq.object_ref()))(s),
response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)(s),
ensures
replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)(s_prime),
Expand Down Expand Up @@ -663,12 +596,12 @@ proof fn lemma_always_replicas_of_etcd_stateful_set_satisfies_order(spec: TempPr
lift_state(replicas_of_stateful_set_create_request_msg_satisfies_order(rabbitmq))
);
assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
helper_1(rabbitmq, s, s_prime);
replicas_of_etcd_stateful_set_satisfies_order_induction(rabbitmq, s, s_prime);
}
init_invariant(spec, RMQCluster::init(), next, inv);
}

proof fn helper_1(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster)
proof fn replicas_of_etcd_stateful_set_satisfies_order_induction(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster)
requires
RMQCluster::next()(s, s_prime),
replicas_of_etcd_stateful_set_satisfies_order(rabbitmq)(s),
Expand Down Expand Up @@ -729,7 +662,7 @@ spec fn owner_references_is_valid(obj: DynamicObjectView, s: RMQCluster) -> bool
#![auto] 0 <= i < owner_refs.len()
==> owner_refs[i].uid < s.kubernetes_api_state.uid_counter
}

}

spec fn object_in_every_create_or_update_request_msg_only_has_valid_owner_references() -> StatePred<RMQCluster> {
Expand Down Expand Up @@ -959,7 +892,7 @@ proof fn lemma_always_replicas_of_stateful_set_create_request_msg_satisfies_orde
assert(replicas_satisfies_order(msg.content.get_create_request().obj, rabbitmq)(s_prime));
}
}
}
}
}
init_invariant(spec, RMQCluster::init(), next, inv);
}
Expand Down Expand Up @@ -1065,7 +998,7 @@ proof fn lemma_always_replicas_of_stateful_set_update_request_msg_satisfies_orde
assert(replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime));
}
}
}
}
}
init_invariant(spec, RMQCluster::init(), next, inv);
}
Expand Down
Loading

0 comments on commit b4c5bf2

Please sign in to comment.