Skip to content

Commit

Permalink
Add a lemma about message, rename the transition_rule specs
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 27, 2023
1 parent c94a472 commit fe5bfa3
Show file tree
Hide file tree
Showing 5 changed files with 168 additions and 120 deletions.
7 changes: 7 additions & 0 deletions src/controller_examples/rabbitmq_controller/proof/common.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -385,6 +385,13 @@ pub open spec fn sts_update_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) ->
&& msg.content.get_update_request().obj.kind == Kind::StatefulSetKind
}

pub open spec fn sts_get_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool {
|msg: RMQMessage|
msg.dst.is_KubernetesAPI()
&& msg.content.is_get_request()
&& msg.content.get_get_request().key == make_stateful_set_key(key)
}

pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool {
|msg: RMQMessage|
msg.src.is_KubernetesAPI()
Expand Down
88 changes: 7 additions & 81 deletions src/controller_examples/rabbitmq_controller/proof/helper_invariants/invariants.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1107,7 +1107,7 @@ pub open spec fn response_at_after_get_stateful_set_step_is_sts_get_response(rab
|s: RMQCluster| {
at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s)
==> s.reconcile_state_of(key).pending_req_msg.is_Some()
&& is_get_stateful_set_request(s.pending_req_of(key).content.get_APIRequest_0(), rabbitmq)
&& sts_get_request_msg(key)(s.pending_req_of(key))
&& (
forall |msg: RMQMessage|
#[trigger] s.message_in_flight(msg)
Expand All @@ -1128,91 +1128,17 @@ pub proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_res
let key = rabbitmq.object_ref();
let next = |s, s_prime| {
&&& RMQCluster::next()(s, s_prime)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
&&& RMQCluster::every_in_flight_msg_has_lower_id_than_allocator()(s)
&&& RMQCluster::every_in_flight_or_pending_req_msg_has_unique_id()(s)
&&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
&&& RMQCluster::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key)(s_prime)
};
RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
RMQCluster::lemma_always_every_in_flight_msg_has_lower_id_than_allocator(spec);
RMQCluster::lemma_always_every_in_flight_or_pending_req_msg_has_unique_id(spec);
RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
RMQCluster::lemma_always_reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(spec, key);
always_to_always_later(spec, lift_state(RMQCluster::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key)));
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(RMQCluster::every_in_flight_msg_has_lower_id_than_allocator()),
lift_state(RMQCluster::every_in_flight_or_pending_req_msg_has_unique_id()),
lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata())
spec, lift_action(next), lift_action(RMQCluster::next()),
lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
later(lift_state(RMQCluster::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key)))
);
assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
if at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s_prime) {
if at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s) {
assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key));
assert(s_prime.reconcile_state_of(key).pending_req_msg.is_Some());
assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq));
} else {
assert(at_rabbitmq_step(key, RabbitmqReconcileStep::AfterCreateRoleBinding)(s));
assert(s_prime.reconcile_state_of(key).pending_req_msg.is_Some());
assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq));
}
assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Message::resp_msg_matches_req_msg(msg, s_prime.pending_req_of(key))
implies sts_get_response_msg(key)(msg) by {
let step = choose |step| RMQCluster::next_step(s, s_prime, step);
match step {
Step::ControllerStep(input) => {
assert(s.message_in_flight(msg));
let cr_key = input.1.get_Some_0();
if cr_key == key {
assert(s.message_in_flight(msg));
assert(false);
} else {
assert(s.pending_req_of(key) == s_prime.pending_req_of(key));
assert(sts_get_response_msg(key)(msg));
}
},
Step::KubernetesAPIStep(input) => {
assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key));
if !s.message_in_flight(msg) {
assert(RMQCluster::in_flight_or_pending_req_message(s, s.pending_req_of(key)));
assert(RMQCluster::in_flight_or_pending_req_message(s, input.get_Some_0()));
assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq));
assert(msg.content.is_get_response());
assert(msg == RMQCluster::handle_get_request(s.pending_req_of(key), s.kubernetes_api_state).1);
assert(msg.src.is_KubernetesAPI()
&& msg.content.is_get_response());
if msg.content.get_get_response().res.is_Ok() {
assert(s.resource_key_exists(make_stateful_set_key(key)));
assert(s.resource_obj_of(make_stateful_set_key(key)).object_ref() == make_stateful_set_key(key));
}
assert(sts_get_response_msg(key)(msg));
}
},
Step::KubernetesBusy(input) => {
assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key));
if !s.message_in_flight(msg) {
assert(RMQCluster::in_flight_or_pending_req_message(s, s.pending_req_of(key)));
assert(RMQCluster::in_flight_or_pending_req_message(s, input.get_Some_0()));
assert(msg.src.is_KubernetesAPI());
assert(msg.content.is_get_response());
assert(msg.content.get_get_response().res.is_Err());
}
assert(sts_get_response_msg(key)(msg));
},
Step::ClientStep() => {
assert(s.message_in_flight(msg));
assert(sts_get_response_msg(key)(msg));
},
Step::ExternalAPIStep(input) => {
assert(input.get_Some_0() != msg);
assert(s.message_in_flight(msg));
},
_ => {
assert(s.message_in_flight(msg));
assert(sts_get_response_msg(key)(msg));
}
}
}
}
}
init_invariant(spec, RMQCluster::init(), next, inv);
}

Expand Down
10 changes: 5 additions & 5 deletions src/controller_examples/rabbitmq_controller/proof/safety/safety.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -402,21 +402,21 @@ proof fn lemma_always_replicas_of_stateful_set_create_or_update_request_msg_sati
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
&&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime)
&&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
&&& RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s)
&&& RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)(s)
&&& object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(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()));
RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
RMQCluster::lemma_always_etcd_and_scheduled_and_triggering_cr_in_correct_order(spec, rabbitmq);
RMQCluster::lemma_always_transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(spec, rabbitmq);
lemma_always_object_in_every_create_or_update_request_msg_only_has_valid_owner_references(spec);
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(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
lift_state(RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)),
lift_state(RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)),
lift_state(object_in_every_create_or_update_request_msg_only_has_valid_owner_references())
);
assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
Expand All @@ -442,7 +442,7 @@ proof fn replicas_of_stateful_set_create_request_msg_satisfies_order_induction(
RMQCluster::each_object_in_etcd_is_well_formed()(s),
RMQCluster::each_object_in_etcd_is_well_formed()(s_prime),
RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s),
RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s),
RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)(s),
object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(s),
replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq)(s),
s_prime.message_in_flight(msg),
Expand Down Expand Up @@ -502,7 +502,7 @@ proof fn replicas_of_stateful_set_update_request_msg_satisfies_order_induction(
RMQCluster::each_object_in_etcd_is_well_formed()(s),
RMQCluster::each_object_in_etcd_is_well_formed()(s_prime),
RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s),
RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s),
RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)(s),
object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(s),
replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq)(s),
s_prime.message_in_flight(msg),
Expand Down
Loading

0 comments on commit fe5bfa3

Please sign in to comment.