From 24562abed6b669b0b899a4fc1bdd8858f88d6130 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Tue, 17 Sep 2024 11:28:31 -0500 Subject: [PATCH 1/4] Improve TLA lemma names Signed-off-by: Xudong Sun --- .../proof/helper_invariants/proof.rs | 2 +- .../proof/liveness/daemon_set_match.rs | 2 +- .../fluentbit/proof/liveness/proof.rs | 4 +- .../proof/liveness/resource_match.rs | 8 +- .../fluentbit/proof/liveness/spec.rs | 2 +- .../fluentbit/proof/liveness/terminate.rs | 2 +- .../fluentbit_config/proof/liveness/proof.rs | 4 +- .../proof/liveness/resource_match.rs | 4 +- .../proof/liveness/terminate.rs | 2 +- .../proof/liveness/proof.rs | 4 +- .../proof/liveness/resource_match.rs | 8 +- .../proof/liveness/stateful_set_match.rs | 2 +- .../proof/liveness/terminate.rs | 2 +- .../proof/liveness/proof.rs | 22 ++- .../proof/liveness/resource_match.rs | 145 +++++++++--------- .../proof/liveness/terminate.rs | 76 ++++----- .../proof/liveness/proof.rs | 4 +- .../proof/liveness/resource_match.rs | 8 +- .../proof/liveness/stateful_set_match.rs | 2 +- .../proof/liveness/terminate.rs | 2 +- .../proof/api_server_liveness.rs | 10 +- .../proof/controller_runtime_liveness.rs | 8 +- .../proof/daemon_set_controller.rs | 2 +- .../proof/external_api_liveness.rs | 2 +- .../proof/stateful_set_controller.rs | 2 +- src/temporal_logic/rules.rs | 52 ++----- .../proof/controller_runtime_liveness.rs | 4 +- .../proof/network_liveness.rs | 6 +- .../kubernetes_cluster/proof/wf1_helpers.rs | 8 +- 29 files changed, 183 insertions(+), 216 deletions(-) diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs index 6080fcfcd..9badd55f4 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs @@ -1012,7 +1012,7 @@ pub proof fn lemma_eventually_always_daemon_set_not_exists_or_matches_or_no_more lift_state(every_resource_create_request_implies_at_after_create_resource_step(SubResource::DaemonSet, fb)), lift_state(FBCluster::every_in_flight_create_req_msg_for_this_ds_matches(ds_key, make_fn)) ); - valid_implies_trans( + entails_trans( spec, always(lift_state(every_resource_create_request_implies_at_after_create_resource_step(SubResource::DaemonSet, fb))), always(lift_state(FBCluster::every_in_flight_create_req_msg_for_this_ds_matches(ds_key, make_fn))) diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs index 43fb69756..47ae27dd7 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs @@ -106,7 +106,7 @@ proof fn lemma_from_after_get_daemon_set_step_and_key_exists_to_daemon_set_match let post = lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb)); assert_by(spec.entails(daemon_set_matches.leads_to(post)), { - valid_implies_implies_leads_to(spec, daemon_set_matches, post); + entails_implies_leads_to(spec, daemon_set_matches, post); }); assert_by(spec.entails(daemon_set_not_matches.leads_to(post)), { diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs index 83c7d034d..3a5ec8272 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs @@ -64,7 +64,7 @@ proof fn liveness_proof(fb: FluentBitView) unpack_conditions_from_spec(invariants(fb), assumption, true_pred(), always(lift_state(current_state_matches::(fb)))); temp_pred_equality(true_pred().and(assumption), assumption); - valid_implies_trans( + entails_trans( cluster_spec().and(derived_invariants_since_beginning(fb)), invariants(fb), always(lift_state(desired_state_is(fb))).leads_to(always(lift_state(current_state_matches::(fb)))) ); @@ -208,7 +208,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, fb: F }; let input = fb.object_ref(); FBCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCluster::next(), desired_state_is(fb), pre, post); - valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post)); + entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCluster| {!s.ongoing_reconciles().contains_key(fb.object_ref())})); } diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs index 03437ef7c..842e217bc 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs @@ -176,7 +176,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fb)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb))); }); @@ -237,7 +237,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m } temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp); }); - valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); + entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state)); }); } @@ -339,7 +339,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches( }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fb)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb))); }); @@ -402,7 +402,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches( } temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp); }); - valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); + entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state)); }); } diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs index 20912a0a2..6371019e8 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs @@ -76,7 +76,7 @@ pub proof fn spec_of_previous_phases_entails_eventually_new_invariants(i: nat, f let spec = spec_before_phase_n(i, fb); reveal_with_fuel(spec_before_phase_n, 8); implies_preserved_by_always_temp(lift_state(desired_state_is(fb)), lift_state(FBCluster::desired_state_is(fb))); - valid_implies_trans(spec, always(lift_state(desired_state_is(fb))), always(lift_state(FBCluster::desired_state_is(fb)))); + entails_trans(spec, always(lift_state(desired_state_is(fb))), always(lift_state(FBCluster::desired_state_is(fb)))); if i == 1 { FBCluster::lemma_true_leads_to_crash_always_disabled(spec); FBCluster::lemma_true_leads_to_busy_always_disabled(spec); diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs index 40107251b..ed99f3ce1 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs @@ -56,7 +56,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, fb: Flue FBCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, fb.object_ref()); temp_pred_equality(lift_state(at_step_state_pred(fb, FluentBitReconcileStep::Done)), lift_state(FBCluster::reconciler_reconcile_done(fb.object_ref()))); temp_pred_equality(lift_state(at_step_state_pred(fb, FluentBitReconcileStep::Error)), lift_state(FBCluster::reconciler_reconcile_error(fb.object_ref()))); - valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); + entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); // Second, prove that the sub resource that every intermediate steps can lead to reconcile idle. lemma_from_after_get_resource_step_to_after_get_next_resource_step_to_reconcile_idle(spec, fb, SubResource::DaemonSet, FluentBitReconcileStep::Done); diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs index da94e3c0a..c537427b8 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs @@ -55,7 +55,7 @@ proof fn liveness_proof(fbc: FluentBitConfigView) unpack_conditions_from_spec(invariants(fbc), assumption, true_pred(), always(lift_state(current_state_matches::(fbc)))); temp_pred_equality(true_pred().and(assumption), assumption); - valid_implies_trans( + entails_trans( cluster_spec().and(derived_invariants_since_beginning(fbc)), invariants(fbc), always(lift_state(desired_state_is(fbc))).leads_to(always(lift_state(current_state_matches::(fbc)))) ); @@ -148,7 +148,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, fbc: }; let input = fbc.object_ref(); FBCCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCCluster::next(), desired_state_is(fbc), pre, post); - valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post)); + entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCCluster| {!s.ongoing_reconciles().contains_key(fbc.object_ref())})); } diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs index 95e443518..0500439a3 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs @@ -153,7 +153,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fbc)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc))); }); } @@ -242,7 +242,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches( }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fbc)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc))); }); } diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs index caa278238..75253f99a 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs @@ -55,7 +55,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, fbc: Fl FBCCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, fbc.object_ref()); temp_pred_equality(lift_state(at_step_state_pred(fbc, FluentBitConfigReconcileStep::Done)), lift_state(FBCCluster::reconciler_reconcile_done(fbc.object_ref()))); temp_pred_equality(lift_state(at_step_state_pred(fbc, FluentBitConfigReconcileStep::Error)), lift_state(FBCCluster::reconciler_reconcile_error(fbc.object_ref()))); - valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); + entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); // Second, prove that the sub resource that every intermediate steps can lead to reconcile idle. lemma_from_after_get_resource_step_to_after_get_next_resource_step_to_reconcile_idle(spec, fbc, SubResource::Secret, FluentBitConfigReconcileStep::Done); diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs index 0cf4fdf22..13c7e4d94 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs @@ -64,7 +64,7 @@ proof fn liveness_proof(rabbitmq: RabbitmqClusterView) unpack_conditions_from_spec(invariants(rabbitmq), assumption, true_pred(), always(lift_state(current_state_matches::(rabbitmq)))); temp_pred_equality(true_pred().and(assumption), assumption); - valid_implies_trans( + entails_trans( cluster_spec().and(derived_invariants_since_beginning(rabbitmq)), invariants(rabbitmq), always(lift_state(RMQCluster::desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches::(rabbitmq)))) ); @@ -303,7 +303,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, rabb }; let input = rabbitmq.object_ref(); RMQCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, RMQCluster::next(), RMQCluster::desired_state_is(rabbitmq), pre, post); - valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post)); + entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: RMQCluster| {!s.ongoing_reconciles().contains_key(rabbitmq.object_ref())})); } diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs index 50ab312b1..57c54e2b7 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs @@ -186,7 +186,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, rabbitmq)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); }); @@ -247,7 +247,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m } temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp); }); - valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); + entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state)); }); } @@ -349,7 +349,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches( }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, rabbitmq)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); }); @@ -412,7 +412,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches( } temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp); }); - valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); + entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state)); }); } diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs index f7c4fe7ad..9d5839f81 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs @@ -119,7 +119,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m let post = lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)); assert_by(spec.entails(stateful_set_matches.leads_to(post)), { - valid_implies_implies_leads_to(spec, stateful_set_matches, post); + entails_implies_leads_to(spec, stateful_set_matches, post); }); assert_by(spec.entails(stateful_set_not_matches.leads_to(post)), { diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs index 32dfcb945..95bedc71c 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs @@ -56,7 +56,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, rabbitm RMQCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, rabbitmq.object_ref()); temp_pred_equality(lift_state(at_step_state_pred(rabbitmq, RabbitmqReconcileStep::Done)), lift_state(RMQCluster::reconciler_reconcile_done(rabbitmq.object_ref()))); temp_pred_equality(lift_state(at_step_state_pred(rabbitmq, RabbitmqReconcileStep::Error)), lift_state(RMQCluster::reconciler_reconcile_error(rabbitmq.object_ref()))); - valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); + entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); // Second, prove that the sub resource that every intermediate steps can lead to reconcile idle. lemma_from_after_get_resource_step_to_after_get_next_resource_step_to_reconcile_idle(spec, rabbitmq, SubResource::StatefulSet, RabbitmqReconcileStep::Done); diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs index 5bfdeaecb..b3d3181dc 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs @@ -13,20 +13,16 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::temporal_logic::{defs::*, rules::*}; -use crate::vstd_ext::{map_lib::*, string_view::*}; use crate::v_replica_set_controller::{ - model::{reconciler::*}, + model::reconciler::*, proof::{ helper_invariants, - liveness::{ - spec::*, - resource_match::*, - terminate, - }, + liveness::{resource_match::*, spec::*, terminate}, predicate::*, }, trusted::{liveness_theorem::*, spec_types::*, step::*}, }; +use crate::vstd_ext::{map_lib::*, string_view::*}; use vstd::{prelude::*, string::*}; verus! { @@ -34,7 +30,7 @@ verus! { // We prove init /\ []next /\ []wf |= []VReplicaSet::desired_state_is(vrs) ~> []current_state_matches(vrs) holds for each vrs. proof fn liveness_proof_forall_vrs() ensures liveness_theorem(), -{ +{ assert forall |vrs: VReplicaSetView| #[trigger] cluster_spec().entails(liveness(vrs)) by { liveness_proof(vrs); }; @@ -59,7 +55,7 @@ proof fn liveness_proof(vrs: VReplicaSetView) unpack_conditions_from_spec(invariants(vrs), assumption, true_pred(), always(lift_state(current_state_matches(vrs)))); temp_pred_equality(true_pred().and(assumption), assumption); - valid_implies_trans( + entails_trans( cluster_spec().and(derived_invariants_since_beginning(vrs)), invariants(vrs), always(lift_state(VRSCluster::desired_state_is(vrs))).leads_to(always(lift_state(current_state_matches(vrs)))) ); @@ -94,7 +90,7 @@ proof fn lemma_true_leads_to_always_current_state_matches(vrs: VReplicaSetView) &&& num_diff_pods_is(vrs, diff)(s) } ); - + // The use of termination property ensures spec |= true ~> reconcile_idle. terminate::reconcile_eventually_terminates(spec, vrs); // Then we can continue to show that spec |= reconcile_idle ~> []current_state_matches(vrs). @@ -113,7 +109,7 @@ proof fn lemma_true_leads_to_always_current_state_matches(vrs: VReplicaSetView) let diff = pods.len() - vrs.spec.replicas.unwrap_or(0); // Instantiate exists statement. - assert((|diff| lift_state(num_diff_pods_is(vrs, diff)))(diff).satisfied_by(ex)); + assert((|diff| lift_state(num_diff_pods_is(vrs, diff)))(diff).satisfied_by(ex)); } assert(valid(true_pred::().implies(exists_num_diff_pods_is))); temp_pred_equality(true_pred::(), tla_exists(|diff| lift_state(num_diff_pods_is(vrs, diff)))); @@ -127,7 +123,7 @@ proof fn lemma_true_leads_to_always_current_state_matches(vrs: VReplicaSetView) let diff = choose |diff| lift_state(#[trigger] num_diff_pods_is(vrs, diff)).satisfied_by(ex); assert(diff_at_init(diff).satisfied_by(ex)); } - implies_to_leads_to(spec, at_init, tla_exists(diff_at_init)); + always_implies_to_leads_to(spec, at_init, tla_exists(diff_at_init)); }); // The following shows exists |diff| (num_diff_pods_is(diff) /\ init) ~> current_state_matches(vrs) @@ -173,7 +169,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, vrs: }; let input = vrs.object_ref(); VRSCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, VRSCluster::next(), VRSCluster::desired_state_is(vrs), pre, post); - valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post)); + entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: VRSCluster| {!s.ongoing_reconciles().contains_key(vrs.object_ref())})); } diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs index 4c3af685d..cca547470 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs @@ -14,16 +14,13 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::temporal_logic::{defs::*, rules::*}; -use crate::vstd_ext::{map_lib::*, seq_lib::*, set_lib::*, string_view::*}; use crate::v_replica_set_controller::{ - model::{reconciler::*}, - proof::{helper_invariants, predicate::*, liveness::api_actions::*}, - trusted::{spec_types::*, step::*, liveness_theorem::*}, -}; -use vstd::{ - prelude::*, seq::*, seq_lib::*, set_lib::*, - string::*, map::*, map_lib::*, math::abs + model::reconciler::*, + proof::{helper_invariants, liveness::api_actions::*, predicate::*}, + trusted::{liveness_theorem::*, spec_types::*, step::*}, }; +use crate::vstd_ext::{map_lib::*, seq_lib::*, set_lib::*, string_view::*}; +use vstd::{map::*, map_lib::*, math::abs, prelude::*, seq::*, seq_lib::*, set_lib::*, string::*}; verus! { @@ -107,24 +104,24 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( // Deal with transition from init to listing the pods. lemma_from_init_step_to_send_list_pods_req(spec, vrs, diff); - assert forall |req_msg: VRSMessage| + assert forall |req_msg: VRSMessage| invariants implies #[trigger] spec.entails(list_req_msg(req_msg, diff).leads_to(list_resp(diff))) by { lemma_from_after_send_list_pods_req_to_receive_list_pods_resp(spec, vrs, req_msg, diff); }; leads_to_exists_intro(spec, |req_msg| list_req_msg(req_msg, diff), list_resp(diff)); - + assert_by(spec.entails(list_req(diff).leads_to(tla_exists(|req_msg| list_req_msg(req_msg, diff)))), { - assert forall |ex| #[trigger] list_req(diff).satisfied_by(ex) + assert forall |ex| #[trigger] list_req(diff).satisfied_by(ex) implies tla_exists(|req_msg| list_req_msg(req_msg, diff)).satisfied_by(ex) by { let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); assert((|req_msg: VRSMessage| list_req_msg(req_msg, diff))(req_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, list_req(diff), tla_exists(|req_msg| list_req_msg(req_msg, diff))); + entails_implies_leads_to(spec, list_req(diff), tla_exists(|req_msg| list_req_msg(req_msg, diff))); }); leads_to_trans_n!( - spec, + spec, pre(diff), list_req(diff), tla_exists(|req_msg| list_req_msg(req_msg, diff)), @@ -152,10 +149,10 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( // Is this enough? if diff + 1 == 0 { // If so, pre(diff) ~> current_state_matches(vrs) trivially. - valid_implies_implies_leads_to(spec, create_resp(diff + 1), lift_state(current_state_matches(vrs))); + entails_implies_leads_to(spec, create_resp(diff + 1), lift_state(current_state_matches(vrs))); leads_to_trans_n!( - spec, - pre(diff), + spec, + pre(diff), create_resp(diff + 1), lift_state(current_state_matches(vrs)) ); @@ -169,16 +166,16 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( // Useful assertions to let us chain in and out of ranking_pred assert forall |n: nat| #![trigger create_resp(-n)] spec.entails(create_resp(-n).leads_to(ranking_pred(n))) by { - valid_implies_implies_leads_to(spec, create_resp(-n), ranking_pred(n)); + entails_implies_leads_to(spec, create_resp(-n), ranking_pred(n)); }; - + assert forall |n: nat| #![trigger create_resp(-n)] spec.entails(ranking_pred(n).leads_to(create_resp(-n))) by { - valid_implies_implies_leads_to(spec, ranking_pred(n), create_resp(-n)); + entails_implies_leads_to(spec, ranking_pred(n), create_resp(-n)); }; // Proving n > 0 => ranking_pred(n) ~> ranking_pred(n - 1) - assert forall |n: nat| #![trigger ranking_pred(n)] + assert forall |n: nat| #![trigger ranking_pred(n)] n > 0 implies spec.entails(ranking_pred(n).leads_to(ranking_pred((n - 1) as nat))) by { let diff = -n; lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp(spec, vrs, diff); @@ -191,15 +188,15 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( ranking_pred((n - 1) as nat) ); }; - + // Apply ranking function lemma leads_to_rank_step_one(spec, ranking_pred); // Chain everything - valid_implies_implies_leads_to(spec, create_resp(0), lift_state(current_state_matches(vrs))); + entails_implies_leads_to(spec, create_resp(0), lift_state(current_state_matches(vrs))); leads_to_trans_n!( - spec, - pre(diff), + spec, + pre(diff), create_resp(diff + 1), ranking_pred(-(diff + 1) as nat), ranking_pred(0), @@ -226,10 +223,10 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( // Is this enough? if diff - 1 == 0 { // If so, pre(diff) ~> current_state_matches(vrs) trivially. - valid_implies_implies_leads_to(spec, delete_resp(diff - 1), lift_state(current_state_matches(vrs))); + entails_implies_leads_to(spec, delete_resp(diff - 1), lift_state(current_state_matches(vrs))); leads_to_trans_n!( - spec, - pre(diff), + spec, + pre(diff), delete_resp(diff - 1), lift_state(current_state_matches(vrs)) ); @@ -241,16 +238,16 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( // Useful assertions to let us chain in and out of ranking_pred assert forall |n: nat| #![trigger ranking_pred(n)] spec.entails(delete_resp(n as int).leads_to(ranking_pred(n))) by { - valid_implies_implies_leads_to(spec, delete_resp(n as int), ranking_pred(n)); + entails_implies_leads_to(spec, delete_resp(n as int), ranking_pred(n)); }; - + assert forall |n: nat| #![trigger ranking_pred(n)] spec.entails(ranking_pred(n).leads_to(delete_resp(n as int))) by { - valid_implies_implies_leads_to(spec, ranking_pred(n), delete_resp(n as int)); + entails_implies_leads_to(spec, ranking_pred(n), delete_resp(n as int)); }; // Proving n > 0 => ranking_pred(n) ~> ranking_pred(n - 1) - assert forall |n: nat| #![trigger ranking_pred(n)] + assert forall |n: nat| #![trigger ranking_pred(n)] n > 0 implies spec.entails(ranking_pred(n).leads_to(ranking_pred((n - 1) as nat))) by { let diff = n as int; lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp(spec, vrs, diff); @@ -263,15 +260,15 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( ranking_pred((n - 1) as nat) ); }; - + // Apply ranking function lemma leads_to_rank_step_one(spec, ranking_pred); // Chain everything - valid_implies_implies_leads_to(spec, delete_resp(0), lift_state(current_state_matches(vrs))); + entails_implies_leads_to(spec, delete_resp(0), lift_state(current_state_matches(vrs))); leads_to_trans_n!( - spec, - pre(diff), + spec, + pre(diff), delete_resp(diff - 1), ranking_pred((diff - 1) as nat), ranking_pred(0), @@ -281,9 +278,9 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( } else { // diff = 0 // list_resp(diff) ~> current_state_matches(vrs) trivially. - valid_implies_implies_leads_to(spec, list_resp(diff), lift_state(current_state_matches(vrs))); + entails_implies_leads_to(spec, list_resp(diff), lift_state(current_state_matches(vrs))); leads_to_trans_n!( - spec, + spec, pre(diff), list_resp(diff), lift_state(current_state_matches(vrs)) @@ -458,7 +455,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( let resp_msg = VRSCluster::handle_list_request_msg(req_msg, s.kubernetes_api_state).1; let resp_objs = resp_msg.content.get_list_response().res.unwrap(); - assert forall |o: DynamicObjectView| #![auto] + assert forall |o: DynamicObjectView| #![auto] pre(s) && matching_pod_entries(vrs, s_prime.resources()).values().contains(o) implies resp_objs.to_set().contains(o) by { // Tricky reasoning about .to_seq @@ -472,7 +469,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( finite_set_to_seq_contains_all_set_elements(selected_elements); } - assert forall |o: DynamicObjectView| #![auto] + assert forall |o: DynamicObjectView| #![auto] pre(s) && resp_objs.contains(o) implies !PodView::unmarshal(o).is_err() by { // Tricky reasoning about .to_seq @@ -510,7 +507,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( let resp_msg = VRSCluster::handle_list_request_msg(req_msg, s.kubernetes_api_state).1; let resp_objs = resp_msg.content.get_list_response().res.unwrap(); - assert forall |o: DynamicObjectView| #![auto] + assert forall |o: DynamicObjectView| #![auto] pre(s) && matching_pod_entries(vrs, s_prime.resources()).values().contains(o) implies resp_objs.to_set().contains(o) by { // Tricky reasoning about .to_seq @@ -524,7 +521,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( finite_set_to_seq_contains_all_set_elements(selected_elements); } - assert forall |o: DynamicObjectView| #![auto] + assert forall |o: DynamicObjectView| #![auto] pre(s) && resp_objs.contains(o) implies !PodView::unmarshal(o).is_err() by { // Tricky reasoning about .to_seq @@ -563,7 +560,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp( spec: TempPred, vrs: VReplicaSetView, diff: int ) - requires + requires spec.entails(always(lift_action(VRSCluster::next()))), spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))), spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))), @@ -636,11 +633,11 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp( ); // Apply two lemmas relating to the first created pod. - assert forall |resp_msg: VRSMessage| + assert forall |resp_msg: VRSMessage| diff < 0 implies #[trigger] spec.entails(list_resp_msg(resp_msg, diff).leads_to(create_req(diff))) by { lemma_from_after_receive_list_pods_resp_to_send_create_pod_req(spec, vrs, resp_msg, diff); }; - assert forall |req_msg: VRSMessage| + assert forall |req_msg: VRSMessage| diff < 0 implies #[trigger] spec.entails(create_req_msg(req_msg, diff).leads_to(create_resp(diff + 1))) by { lemma_from_after_send_create_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff); }; @@ -651,7 +648,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp( assert_by( spec.entails(list_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)))), { - assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex) + assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex) implies tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)).satisfied_by(ex) by { let s = ex.head(); let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); @@ -668,24 +665,24 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp( }; assert((|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))); + entails_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))); } ); assert_by( spec.entails(create_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)))), { - assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex) + assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex) implies tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)).satisfied_by(ex) by { let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); assert((|req_msg: VRSMessage| create_req_msg(req_msg, diff))(req_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff))); + entails_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff))); } ); leads_to_trans_n!( spec, list_resp(diff), - tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)), + tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)), create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)), create_resp(diff + 1) @@ -754,11 +751,11 @@ pub proof fn lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp ); // Apply two lemmas relating to subsequent created pods. - assert forall |resp_msg: VRSMessage| + assert forall |resp_msg: VRSMessage| diff < 0 implies #[trigger] spec.entails(create_resp_msg(resp_msg, diff).leads_to(create_req(diff))) by { lemma_from_after_receive_ok_resp_to_send_create_pod_req(spec, vrs, resp_msg, diff); }; - assert forall |req_msg: VRSMessage| + assert forall |req_msg: VRSMessage| diff < 0 implies #[trigger] spec.entails(create_req_msg(req_msg, diff).leads_to(create_resp(diff + 1))) by { lemma_from_after_send_create_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff); }; @@ -769,18 +766,18 @@ pub proof fn lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp assert_by( spec.entails(create_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)))), { - assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex) + assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex) implies tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)).satisfied_by(ex) by { let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); assert((|req_msg: VRSMessage| create_req_msg(req_msg, diff))(req_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff))); + entails_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff))); } ); assert_by( spec.entails(create_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff)))), { - assert forall |ex| #[trigger] create_resp(diff).satisfied_by(ex) + assert forall |ex| #[trigger] create_resp(diff).satisfied_by(ex) implies tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff)).satisfied_by(ex) by { let s = ex.head(); let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); @@ -791,7 +788,7 @@ pub proof fn lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp }; assert((|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, create_resp(diff), tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff))); + entails_implies_leads_to(spec, create_resp(diff), tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff))); } ); @@ -932,7 +929,7 @@ pub proof fn lemma_filtered_pods_len_equals_matching_pods_len( pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( spec: TempPred, vrs: VReplicaSetView, req_msg: VRSMessage, diff: int ) - requires + requires spec.entails(always(lift_action(VRSCluster::next()))), spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))), spec.entails(always(lift_state(VRSCluster::crash_disabled()))), @@ -1109,7 +1106,7 @@ pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( spec: TempPred, vrs: VReplicaSetView, resp_msg: VRSMessage, diff: int ) - requires + requires spec.entails(always(lift_action(VRSCluster::next()))), spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))), spec.entails(always(lift_state(VRSCluster::crash_disabled()))), @@ -1205,7 +1202,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp( spec: TempPred, vrs: VReplicaSetView, diff: int ) - requires + requires spec.entails(always(lift_action(VRSCluster::next()))), spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))), spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))), @@ -1278,11 +1275,11 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp( ); // Apply two lemmas relating to the first deleted pod. - assert forall |resp_msg: VRSMessage| + assert forall |resp_msg: VRSMessage| diff > 0 implies #[trigger] spec.entails(list_resp_msg(resp_msg, diff).leads_to(delete_req(diff))) by { lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req(spec, vrs, resp_msg, diff); }; - assert forall |req_msg: VRSMessage| + assert forall |req_msg: VRSMessage| diff > 0 implies #[trigger] spec.entails(delete_req_msg(req_msg, diff).leads_to(delete_resp(diff - 1))) by { lemma_from_after_send_delete_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff); }; @@ -1293,7 +1290,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp( assert_by( spec.entails(list_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)))), { - assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex) + assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex) implies tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)).satisfied_by(ex) by { let s = ex.head(); let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); @@ -1310,24 +1307,24 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp( }; assert((|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))); + entails_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))); } ); assert_by( spec.entails(delete_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)))), { - assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex) + assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex) implies tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)).satisfied_by(ex) by { let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); assert((|req_msg: VRSMessage| delete_req_msg(req_msg, diff))(req_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff))); + entails_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff))); } ); leads_to_trans_n!( spec, list_resp(diff), - tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)), + tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)), delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)), delete_resp(diff - 1) @@ -1398,11 +1395,11 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp ); // Apply two lemmas relating to subsequent deleted pods. - assert forall |resp_msg: VRSMessage| + assert forall |resp_msg: VRSMessage| diff > 0 implies #[trigger] spec.entails(delete_resp_msg(resp_msg, diff).leads_to(delete_req(diff))) by { lemma_from_after_receive_ok_resp_to_send_delete_pod_req(spec, vrs, resp_msg, diff); }; - assert forall |req_msg: VRSMessage| + assert forall |req_msg: VRSMessage| diff > 0 implies #[trigger] spec.entails(delete_req_msg(req_msg, diff).leads_to(delete_resp(diff - 1))) by { lemma_from_after_send_delete_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff); }; @@ -1413,18 +1410,18 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp assert_by( spec.entails(delete_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)))), { - assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex) + assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex) implies tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)).satisfied_by(ex) by { let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); assert((|req_msg: VRSMessage| delete_req_msg(req_msg, diff))(req_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff))); + entails_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff))); } ); assert_by( spec.entails(delete_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff)))), { - assert forall |ex| #[trigger] delete_resp(diff).satisfied_by(ex) + assert forall |ex| #[trigger] delete_resp(diff).satisfied_by(ex) implies tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff)).satisfied_by(ex) by { let s = ex.head(); let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(); @@ -1435,7 +1432,7 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp }; assert((|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex)); }; - valid_implies_implies_leads_to(spec, delete_resp(diff), tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff))); + entails_implies_leads_to(spec, delete_resp(diff), tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff))); } ); @@ -1452,7 +1449,7 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req( spec: TempPred, vrs: VReplicaSetView, resp_msg: VRSMessage, diff: int ) - requires + requires spec.entails(always(lift_action(VRSCluster::next()))), spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))), spec.entails(always(lift_state(VRSCluster::crash_disabled()))), @@ -1581,7 +1578,7 @@ pub proof fn lemma_filtered_pods_set_equals_matching_pods( // filter_pods filters pods in a very similar way to matching_pods, but the former // works on a sequence of PodViews, while the latter works on the key-value store directly. // I need to do some manual effort to make the two representations work together. -// +// // Once proven, this will supplant the earlier lemma // lemma_filtered_pods_len_equals_matching_pods_len. // @@ -1716,7 +1713,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( spec: TempPred, vrs: VReplicaSetView, resp_msg: VRSMessage, diff: int ) - requires + requires spec.entails(always(lift_action(VRSCluster::next()))), spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))), spec.entails(always(lift_state(VRSCluster::crash_disabled()))), diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs index de3debd08..d2ecc8953 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs @@ -41,7 +41,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, vrs: VR spec.entails(always(tla_forall(|diff: usize| lift_state(VRSCluster::pending_req_in_flight_or_resp_in_flight_at_reconcile_state( vrs.object_ref(), at_step_closure(VReplicaSetReconcileStep::AfterDeletePod(diff)) ))))), - + ensures spec.entails(true_pred().leads_to(lift_state(|s: VRSCluster| !s.ongoing_reconciles().contains_key(vrs.object_ref())))), { assert forall |diff: usize| #![auto] @@ -73,7 +73,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, vrs: VR VRSCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, vrs.object_ref()); temp_pred_equality(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Done)), lift_state(VRSCluster::reconciler_reconcile_done(vrs.object_ref()))); temp_pred_equality(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), lift_state(VRSCluster::reconciler_reconcile_error(vrs.object_ref()))); - valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); + entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); // Second, prove that after_create_pod_rank(0) \/ after_delete_pod_rank(0) ~> reconcile_idle. lemma_from_after_create_or_delete_pod_rank_zero_to_reconcile_idle(spec, vrs); @@ -89,22 +89,22 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, vrs: VR } leads_to_rank_step_one_usize(spec, |n| lift_state(after_create_pod_rank(vrs, n))); - implies_to_leads_to( - spec, + always_implies_to_leads_to( + spec, lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))), lift_state(after_create_pod_rank(vrs, n)) ); assert(spec.entails((|n| lift_state(after_create_pod_rank(vrs, n)))(n) .leads_to((|n| lift_state(after_create_pod_rank(vrs, n)))(0)))); leads_to_trans_n!( - spec, + spec, lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))), - lift_state(after_create_pod_rank(vrs, n)), - lift_state(after_create_pod_rank(vrs, 0)), + lift_state(after_create_pod_rank(vrs, n)), + lift_state(after_create_pod_rank(vrs, 0)), lift_state(reconcile_idle) ); } - + // Similarly prove for all n that AfterDeletePod(n) ~> reconcile_idle. assert forall |n: usize| #![auto] spec.entails(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))) @@ -115,9 +115,9 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, vrs: VR lemma_from_after_delete_pod_rank_n_to_delete_pod_rank_n_minus_1(spec, vrs, n); } leads_to_rank_step_one_usize(spec, |n| lift_state(after_delete_pod_rank(vrs, n))); - - implies_to_leads_to( - spec, + + always_implies_to_leads_to( + spec, lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))), lift_state(after_delete_pod_rank(vrs, n)) ); @@ -138,15 +138,15 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, vrs: VR // Fifth, prove that reconcile init state can reach AfterListPods. VRSCluster::lemma_from_init_state_to_next_state_to_reconcile_idle( spec, vrs, at_step_closure(VReplicaSetReconcileStep::Init), at_step_closure(VReplicaSetReconcileStep::AfterListPods)); - + // Finally, combine all cases leads_to_exists_intro( - spec, + spec, |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))), lift_state(reconcile_idle) ); leads_to_exists_intro( - spec, + spec, |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))), lift_state(reconcile_idle) ); @@ -274,23 +274,23 @@ proof fn lemma_from_after_create_pod_rank_n_to_create_pod_rank_n_minus_1( || s.reconcile_step == VReplicaSetReconcileStep::Error }; - valid_implies_implies_leads_to( - spec, - lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), + entails_implies_leads_to( + spec, + lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), lift_state(after_create_pod_rank(vrs, (n - 1) as usize)) ); - + VRSCluster::lemma_from_some_state_to_arbitrary_next_state(spec, vrs, at_step_closure(VReplicaSetReconcileStep::AfterCreatePod(n)), state_after_create); - implies_to_leads_to( - spec, - lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)), + always_implies_to_leads_to( + spec, + lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)), lift_state(after_create_pod_rank(vrs, (n - 1) as usize)) ); leads_to_trans_n!( spec, lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))), - lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)), + lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)), lift_state(after_create_pod_rank(vrs, (n - 1) as usize)) ); @@ -327,23 +327,23 @@ proof fn lemma_from_after_delete_pod_rank_n_to_delete_pod_rank_n_minus_1( || s.reconcile_step == VReplicaSetReconcileStep::Error }; - valid_implies_implies_leads_to( - spec, - lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), + entails_implies_leads_to( + spec, + lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), lift_state(after_delete_pod_rank(vrs, (n - 1) as usize)) ); - + VRSCluster::lemma_from_some_state_to_arbitrary_next_state(spec, vrs, at_step_closure(VReplicaSetReconcileStep::AfterDeletePod(n)), state_after_delete); - implies_to_leads_to( - spec, - lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)), + always_implies_to_leads_to( + spec, + lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)), lift_state(after_delete_pod_rank(vrs, (n - 1) as usize)) ); leads_to_trans_n!( spec, lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))), - lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)), + lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)), lift_state(after_delete_pod_rank(vrs, (n - 1) as usize)) ); @@ -392,12 +392,12 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle( ||| s.reconcile_step == VReplicaSetReconcileStep::Error }; leads_to_exists_intro( - spec, + spec, |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))), lift_state(|s: VRSCluster| !s.ongoing_reconciles().contains_key(vrs.object_ref())) ); leads_to_exists_intro( - spec, + spec, |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))), lift_state(|s: VRSCluster| !s.ongoing_reconciles().contains_key(vrs.object_ref())) ); @@ -413,9 +413,9 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle( lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState| exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n))), { - assert forall |ex| #![auto] + assert forall |ex| #![auto] lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState| - exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n))).satisfied_by(ex) implies + exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n))).satisfied_by(ex) implies tla_exists(at_after_create_pod).satisfied_by(ex) by { let s = ex.head().ongoing_reconciles()[vrs.object_ref()].local_state; let witness_n = choose |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n); @@ -434,9 +434,9 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle( lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState| exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n))), { - assert forall |ex| #![auto] + assert forall |ex| #![auto] lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState| - exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n))).satisfied_by(ex) implies + exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n))).satisfied_by(ex) implies tla_exists(at_after_delete_pod).satisfied_by(ex) by { let s = ex.head().ongoing_reconciles()[vrs.object_ref()].local_state; let witness_n = choose |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n); @@ -461,7 +461,7 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle( VRSCluster::lemma_from_some_state_to_arbitrary_next_state(spec, vrs, at_step_closure(VReplicaSetReconcileStep::AfterListPods), state_after_list_pods); - + leads_to_trans_n!( spec, lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterListPods)), @@ -471,7 +471,7 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle( } proof fn lemma_true_equal_to_reconcile_idle_or_at_any_state(vrs: VReplicaSetView) - ensures true_pred::() + ensures true_pred::() == lift_state(|s: VRSCluster| { !s.ongoing_reconciles().contains_key(vrs.object_ref()) }) .or(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Init))) .or(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterListPods))) diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs index 700ef5b62..0414ac112 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs @@ -65,7 +65,7 @@ proof fn liveness_proof(zookeeper: ZookeeperClusterView) unpack_conditions_from_spec(invariants(zookeeper), assumption, true_pred(), always(lift_state(current_state_matches::(zookeeper)))); temp_pred_equality(true_pred().and(assumption), assumption); - valid_implies_trans( + entails_trans( cluster_spec().and(derived_invariants_since_beginning(zookeeper)), invariants(zookeeper), always(lift_state(ZKCluster::desired_state_is(zookeeper))).leads_to(always(lift_state(current_state_matches::(zookeeper)))) ); @@ -295,7 +295,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, zooke }; let input = zookeeper.object_ref(); ZKCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, ZKCluster::next(), ZKCluster::desired_state_is(zookeeper), pre, post); - valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post)); + entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: ZKCluster| {!s.ongoing_reconciles().contains_key(zookeeper.object_ref())})); } 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 53a57c2a3..2fd5b4705 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs @@ -201,7 +201,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, zookeeper)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); }); @@ -262,7 +262,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m } temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp); }); - valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); + entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state)); }); } @@ -375,7 +375,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches( }); assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, zookeeper)))), { - valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); + entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); }); @@ -433,7 +433,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches( } temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp); }); - valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); + entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp); leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state)); }); } 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 8e105a91d..2006a543c 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 @@ -117,7 +117,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m let post = lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)); assert_by(spec.entails(stateful_set_matches.leads_to(post)), { - valid_implies_implies_leads_to(spec, stateful_set_matches, post); + entails_implies_leads_to(spec, stateful_set_matches, post); }); assert_by(spec.entails(stateful_set_not_matches.leads_to(post)), { diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs b/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs index c08187ca2..c06d1b3e5 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs @@ -61,7 +61,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred, zookeepe ZKCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, zookeeper.object_ref()); temp_pred_equality(lift_state(at_step_state_pred(zookeeper, ZookeeperReconcileStep::Done)), lift_state(ZKCluster::reconciler_reconcile_done(zookeeper.object_ref()))); temp_pred_equality(lift_state(at_step_state_pred(zookeeper, ZookeeperReconcileStep::Error)), lift_state(ZKCluster::reconciler_reconcile_error(zookeeper.object_ref()))); - valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); + entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle)); or_leads_to_combine_and_equality!(spec, lift_state(at_step1_or_step2_state_pred(zookeeper, ZookeeperReconcileStep::Done, ZookeeperReconcileStep::Error)), diff --git a/src/kubernetes_cluster/proof/api_server_liveness.rs b/src/kubernetes_cluster/proof/api_server_liveness.rs index ef1423399..c92fad8f2 100644 --- a/src/kubernetes_cluster/proof/api_server_liveness.rs +++ b/src/kubernetes_cluster/proof/api_server_liveness.rs @@ -33,7 +33,7 @@ pub proof fn lemma_pre_leads_to_post_by_kubernetes_api( { use_tla_forall::>>(spec, |i| Self::kubernetes_api_next().weak_fairness(i), input); Self::kubernetes_api_action_pre_implies_next_pre(action, input); - valid_implies_trans::( + entails_trans::( lift_state(pre), lift_state(Self::kubernetes_api_action_pre(action, input)), lift_state(Self::kubernetes_api_next().pre(input)) @@ -55,7 +55,7 @@ pub proof fn lemma_pre_leads_to_post_by_builtin_controllers( { use_tla_forall::(spec, |i| Self::builtin_controllers_next().weak_fairness(i), input); Self::builtin_controllers_action_pre_implies_next_pre(action, input); - valid_implies_trans::( + entails_trans::( lift_state(pre), lift_state(Self::builtin_controllers_action_pre(action, input)), lift_state(Self::builtin_controllers_next().pre(input)) @@ -243,7 +243,7 @@ pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfie lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)) .implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) ); - valid_implies_trans( + entails_trans( spec_with_rest_id, always(lift_state(invariant)), always(lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)).implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))) ); @@ -262,7 +262,7 @@ pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfie always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) ); temp_pred_equality(true_pred().and(lift_state(Self::rest_id_counter_is(rest_id))), lift_state(Self::rest_id_counter_is(rest_id))); - valid_implies_trans(spec, stable_spec, lift_state(Self::rest_id_counter_is(rest_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))))); + entails_trans(spec, stable_spec, lift_state(Self::rest_id_counter_is(rest_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))))); } // All the APIRequest messages with a smaller id than rest_id will eventually leave the network. @@ -357,7 +357,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(spec: T } } }); - valid_implies_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests)); + entails_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests)); } else { // The induction step: // If we already have "there are msg_num-1 such requests" ~> "all such requests are gone" (the inductive hypothesis), diff --git a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs index 5c2d2af38..0685309e8 100644 --- a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs +++ b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs @@ -36,7 +36,7 @@ pub proof fn lemma_pre_leads_to_post_by_controller( ); Self::controller_action_pre_implies_next_pre(action, input); - valid_implies_trans::( + entails_trans::( lift_state(pre), lift_state(Self::controller_action_pre(action, input)), lift_state(Self::controller_next().pre(input)) @@ -261,7 +261,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state( }) }; temp_pred_equality::(lift_state(Self::pending_req_in_flight_or_resp_in_flight_at_reconcile_state(cr.object_ref(), state)), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)).implies(lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight))); - implies_to_leads_to::(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)); + always_implies_to_leads_to::(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)); let req_in_flight = Self::pending_req_in_flight_at_reconcile_state(cr.object_ref(), state); let resp_in_flight = Self::resp_in_flight_matches_pending_req_at_reconcile_state(cr.object_ref(), state); @@ -310,7 +310,7 @@ pub proof fn lemma_from_init_state_to_next_state_to_reconcile_idle( lift_state(Self::no_pending_req_msg_at_reconcile_state(cr.object_ref(), init_state)), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), init_state)).implies(lift_state(no_pending_req)) ); - implies_to_leads_to( + always_implies_to_leads_to( spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), init_state)), lift_state(no_pending_req) @@ -569,7 +569,7 @@ pub proof fn lemma_from_some_state_with_ext_resp_to_two_next_states_to_reconcile && Self::no_pending_req_msg(s, cr.object_ref()) }; temp_pred_equality(lift_state(Self::no_pending_req_msg_at_reconcile_state(cr.object_ref(), state)), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)).implies(lift_state(no_req_at_state))); - implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(no_req_at_state)); + always_implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(no_req_at_state)); let stronger_next = |s, s_prime: Self| { &&& Self::next()(s, s_prime) diff --git a/src/kubernetes_cluster/proof/daemon_set_controller.rs b/src/kubernetes_cluster/proof/daemon_set_controller.rs index f7e3afd52..17394de3d 100644 --- a/src/kubernetes_cluster/proof/daemon_set_controller.rs +++ b/src/kubernetes_cluster/proof/daemon_set_controller.rs @@ -225,7 +225,7 @@ proof fn lemma_pending_update_status_req_num_is_n_leads_to_daemon_set_not_exist_ } } }); - valid_implies_implies_leads_to(spec, lift_state(pre), lift_state(post)); + entails_implies_leads_to(spec, lift_state(pre), lift_state(post)); } else { let pre_concrete_msg = |msg: MsgType| lift_state(|s: Self| { &&& s.in_flight().filter(update_status_msg_from_bc_for(key)).len() == msg_num diff --git a/src/kubernetes_cluster/proof/external_api_liveness.rs b/src/kubernetes_cluster/proof/external_api_liveness.rs index 70bb9214c..72e19ec10 100644 --- a/src/kubernetes_cluster/proof/external_api_liveness.rs +++ b/src/kubernetes_cluster/proof/external_api_liveness.rs @@ -32,7 +32,7 @@ pub proof fn lemma_pre_leads_to_post_by_external_api( { use_tla_forall::>>(spec, |i| Self::external_api_next().weak_fairness(i), input); Self::external_api_action_pre_implies_next_pre(action, input); - valid_implies_trans::( + entails_trans::( lift_state(pre), lift_state(Self::external_api_action_pre(action, input)), lift_state(Self::external_api_next().pre(input)) diff --git a/src/kubernetes_cluster/proof/stateful_set_controller.rs b/src/kubernetes_cluster/proof/stateful_set_controller.rs index 30a9d5923..f608217cd 100644 --- a/src/kubernetes_cluster/proof/stateful_set_controller.rs +++ b/src/kubernetes_cluster/proof/stateful_set_controller.rs @@ -276,7 +276,7 @@ proof fn lemma_pending_update_status_req_num_is_n_leads_to_stateful_set_not_exis } } }); - valid_implies_implies_leads_to(spec, lift_state(pre), lift_state(post)); + entails_implies_leads_to(spec, lift_state(pre), lift_state(post)); } else { let pre_concrete_msg = |msg: MsgType| lift_state(|s: Self| { &&& s.in_flight().filter(update_status_msg_from_bc_for(key)).len() == msg_num diff --git a/src/temporal_logic/rules.rs b/src/temporal_logic/rules.rs index c96f6ba08..6e84b4346 100644 --- a/src/temporal_logic/rules.rs +++ b/src/temporal_logic/rules.rs @@ -202,20 +202,6 @@ spec fn eventually_choose_witness(ex: Execution, p: TempPred) -> nat witness } -proof fn equals_trans(ex: Execution, p: TempPred, q: TempPred, r: TempPred) - requires - p.equals(q).satisfied_by(ex), - q.equals(r).satisfied_by(ex), - ensures p.equals(r).satisfied_by(ex), -{} - -proof fn implies_trans(ex: Execution, p: TempPred, q: TempPred, r: TempPred) - requires - p.implies(q).satisfied_by(ex), - q.implies(r).satisfied_by(ex), - ensures p.implies(r).satisfied_by(ex), -{} - proof fn equals_to_implies(ex: Execution, p: TempPred, q: TempPred) requires p.equals(q).satisfied_by(ex), ensures @@ -261,18 +247,6 @@ proof fn valid_p_implies_always_p(p: TempPred) }; } -proof fn implies_and(p: TempPred, q: TempPred, r: TempPred) - requires - valid(p.implies(q)), - valid(p.implies(r)), - ensures valid(p.implies(q.and(r))), -{ - assert forall |ex| p.satisfied_by(ex) implies #[trigger] q.and(r).satisfied_by(ex) by { - implies_apply::(ex, p, q); - implies_apply::(ex, p, r); - }; -} - proof fn always_implies_current(p: TempPred) ensures valid(always(p).implies(p)), { @@ -448,7 +422,7 @@ proof fn instantiate_entailed_leads_to(ex: Execution, i: nat, spec: TempPr /// All the lemmas above are used internally for proving the lemmas below /// The following lemmas are used by developers to simplify liveness/safety proof -pub proof fn implies_to_leads_to(spec: TempPred, p: TempPred, q: TempPred) +pub proof fn always_implies_to_leads_to(spec: TempPred, p: TempPred, q: TempPred) requires spec.entails(always(p.implies(q))), ensures spec.entails(p.leads_to(q)), { @@ -496,7 +470,7 @@ pub proof fn always_to_always_later(spec: TempPred, p: TempPred) execution_equality(ex.suffix(i).suffix(1), ex.suffix(1).suffix(i)); } } - valid_implies_trans(spec, always(p), always(later(p))); + entails_trans(spec, always(p), always(later(p))); } proof fn always_double_equality(p: TempPred) @@ -680,7 +654,7 @@ pub proof fn always_tla_forall_apply(spec: TempPred, a_to_p: spec_fn(A) ensures spec.entails(always(a_to_p(a))), { implies_preserved_by_always_temp(tla_forall(a_to_p), a_to_p(a)); - valid_implies_trans(spec, always(tla_forall(a_to_p)), always(a_to_p(a))); + entails_trans(spec, always(tla_forall(a_to_p)), always(a_to_p(a))); } proof fn tla_forall_or_equality(a_to_p: spec_fn(A) -> TempPred, q: TempPred) @@ -874,7 +848,7 @@ proof fn stable_spec_entails_always_p(spec: TempPred, p: TempPred) } ); implies_preserved_by_always_temp(spec, p); - valid_implies_trans(spec, always(spec), always(p)); + entails_trans(spec, always(spec), always(p)); } /// Entails p and q if entails each of them. @@ -1039,7 +1013,7 @@ macro_rules! combine_spec_entails_always_n_internal { } ); implies_preserved_by_always_temp(combine_with_next!($($tail)*), $partial_spec); - valid_implies_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec)); + entails_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec)); }; } @@ -1075,9 +1049,9 @@ macro_rules! invariant_n_internal { } ); implies_preserved_by_always_temp(combine_with_next!($($tail)*), $partial_spec); - valid_implies_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec)); + entails_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec)); implies_preserved_by_always_temp($partial_spec, $inv); - valid_implies_trans($spec, always($partial_spec), always($inv)); + entails_trans($spec, always($partial_spec), always($inv)); }; } @@ -1421,7 +1395,7 @@ pub proof fn wf1(spec: TempPred, next: ActionPred, forward: ActionPred< /// q |= r /// post: /// p |= r -pub proof fn valid_implies_trans(p: TempPred, q: TempPred, r: TempPred) +pub proof fn entails_trans(p: TempPred, q: TempPred, r: TempPred) requires p.entails(q), q.entails(r), @@ -1439,12 +1413,12 @@ pub proof fn valid_implies_trans(p: TempPred, q: TempPred, r: TempPred< /// post: /// spec |= p ~> q /// Note: there is no constraint on spec, it can be true_pred(). -pub proof fn valid_implies_implies_leads_to(spec: TempPred, p: TempPred, q: TempPred) - requires valid(p.implies(q)), +pub proof fn entails_implies_leads_to(spec: TempPred, p: TempPred, q: TempPred) + requires p.entails(q), ensures spec.entails(p.leads_to(q)), { valid_p_implies_always_p(p.implies(q)); - implies_to_leads_to(spec, p, q); + always_implies_to_leads_to(spec, p, q); } /// Introduce always to both sides of implies. @@ -1620,8 +1594,8 @@ pub proof fn leads_to_weaken_temp(spec: TempPred, p1: TempPred, q1: Tem spec.entails(p1.leads_to(q1)), ensures spec.entails(p2.leads_to(q2)), { - implies_to_leads_to::(spec, p2, p1); - implies_to_leads_to::(spec, q1, q2); + always_implies_to_leads_to::(spec, p2, p1); + always_implies_to_leads_to::(spec, q1, q2); leads_to_trans_temp::(spec, p2, p1, q1); leads_to_trans_temp::(spec, p2, q1, q2); } diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs index 0395287c4..4632f1137 100644 --- a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs +++ b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs @@ -298,7 +298,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state(self, spec: TempPred< }) }; temp_pred_equality(lift_state(Self::pending_req_in_flight_or_resp_in_flight_at_reconcile_state(controller_id, cr.object_ref(), current_state)), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), current_state)).implies(lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight))); - implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), current_state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)); + always_implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), current_state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)); let req_in_flight = Self::pending_req_in_flight_at_reconcile_state(controller_id, cr.object_ref(), current_state); let resp_in_flight = Self::resp_in_flight_matches_pending_req_at_reconcile_state(controller_id, cr.object_ref(), current_state); @@ -336,7 +336,7 @@ pub proof fn lemma_from_init_state_to_next_state_to_reconcile_idle(self, spec: T &&& Self::no_pending_req_msg(controller_id, s, cr.object_ref()) }; temp_pred_equality(lift_state(Self::no_pending_req_msg_at_reconcile_state(controller_id, cr.object_ref(), init_state)), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), init_state)).implies(lift_state(no_pending_req))); - implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), init_state)), lift_state(no_pending_req)); + always_implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), init_state)), lift_state(no_pending_req)); let stronger_next = |s, s_prime| { &&& self.next()(s, s_prime) &&& Self::crash_disabled(controller_id)(s) diff --git a/src/v2/kubernetes_cluster/proof/network_liveness.rs b/src/v2/kubernetes_cluster/proof/network_liveness.rs index 87aad43ec..0f2566c4c 100644 --- a/src/v2/kubernetes_cluster/proof/network_liveness.rs +++ b/src/v2/kubernetes_cluster/proof/network_liveness.rs @@ -182,7 +182,7 @@ pub proof fn lemma_some_rpc_id_leads_to_always_every_in_flight_req_msg_satisfies lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)) .implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) ); - valid_implies_trans( + entails_trans( spec_with_rpc_id, always(lift_state(invariant)), always(lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)).implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))) ); @@ -201,7 +201,7 @@ pub proof fn lemma_some_rpc_id_leads_to_always_every_in_flight_req_msg_satisfies always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) ); temp_pred_equality(true_pred().and(lift_state(Self::rpc_id_counter_is(rpc_id))), lift_state(Self::rpc_id_counter_is(rpc_id))); - valid_implies_trans(spec, stable_spec, lift_state(Self::rpc_id_counter_is(rpc_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))))); + entails_trans(spec, stable_spec, lift_state(Self::rpc_id_counter_is(rpc_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))))); } // All the APIRequest messages with a smaller id than rpc_id will eventually leave the network. @@ -294,7 +294,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(self, s } } }); - valid_implies_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests)); + entails_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests)); } else { // The induction step: // If we already have "there are msg_num-1 such requests" ~> "all such requests are gone" (the inductive hypothesis), diff --git a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs index 1c837ae6a..b5b472be4 100644 --- a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs +++ b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs @@ -38,7 +38,7 @@ pub proof fn lemma_pre_leads_to_post_by_api_server( { use_tla_forall::>(spec, |i| self.api_server_next().weak_fairness(i), input); self.api_server_action_pre_implies_next_pre(step, input); - valid_implies_trans::( + entails_trans::( lift_state(pre), lift_state(self.api_server_action_pre(step, input)), lift_state(self.api_server_next().pre(input)) @@ -60,7 +60,7 @@ pub proof fn lemma_pre_leads_to_post_by_builtin_controllers( { use_tla_forall::(spec, |i| self.builtin_controllers_next().weak_fairness(i), input); self.builtin_controllers_action_pre_implies_next_pre(step, input); - valid_implies_trans::( + entails_trans::( lift_state(pre), lift_state(self.builtin_controllers_action_pre(step, input)), lift_state(self.builtin_controllers_next().pre(input)) @@ -82,7 +82,7 @@ pub proof fn lemma_pre_leads_to_post_by_controller( { use_tla_forall::, Option)>(spec, |i: (Option, Option)| self.controller_next().weak_fairness((controller_id, i.0, i.1)), input); self.controller_action_pre_implies_next_pre(step, (controller_id, input.0, input.1)); - valid_implies_trans( + entails_trans( lift_state(pre), lift_state(self.controller_action_pre(step, (controller_id, input.0, input.1))), lift_state(self.controller_next().pre((controller_id, input.0, input.1))) @@ -120,7 +120,7 @@ pub proof fn lemma_pre_leads_to_post_by_external( { use_tla_forall::>(spec, |i| self.external_next().weak_fairness((controller_id, i)), input); self.external_action_pre_implies_next_pre(step, (controller_id, input)); - valid_implies_trans::( + entails_trans::( lift_state(pre), lift_state(self.external_action_pre(step, (controller_id, input))), lift_state(self.external_next().pre((controller_id, input))) From aca00490f415085b3d8f83c4e8d1657bcd6fa711 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Tue, 17 Sep 2024 11:47:11 -0500 Subject: [PATCH 2/4] simplify Signed-off-by: Xudong Sun --- src/temporal_logic/defs.rs | 7 +- src/temporal_logic/rules.rs | 130 +++--------------------------------- 2 files changed, 10 insertions(+), 127 deletions(-) diff --git a/src/temporal_logic/defs.rs b/src/temporal_logic/defs.rs index ff8e9fdfe..dfbf7a2af 100644 --- a/src/temporal_logic/defs.rs +++ b/src/temporal_logic/defs.rs @@ -63,11 +63,6 @@ impl TempPred { TempPred::new(|ex: Execution| self.satisfied_by(ex) ==> other.satisfied_by(ex)) } - /// `<=>` for temporal predicates in TLA+ (i.e., `<==>` in Verus). - pub open spec fn equals(self, other: Self) -> Self { - TempPred::new(|ex: Execution| self.satisfied_by(ex) <==> other.satisfied_by(ex)) - } - /// `~>` for temporal predicates in TLA+. /// Returns a temporal predicate that is satisfied /// iff it is always the case that `self` getting satisfied implies `other` eventually getting satisfied. @@ -178,7 +173,7 @@ pub open spec fn true_pred() -> TempPred { } pub open spec fn false_pred() -> TempPred { - lift_state(|s: T| false) + not(true_pred()) } } diff --git a/src/temporal_logic/rules.rs b/src/temporal_logic/rules.rs index 6e84b4346..5bd773a85 100644 --- a/src/temporal_logic/rules.rs +++ b/src/temporal_logic/rules.rs @@ -97,13 +97,6 @@ proof fn implies_contraposition_apply(ex: Execution, p: TempPred, q: Te ensures not(p).satisfied_by(ex), {} -proof fn equals_apply(ex: Execution, p: TempPred, q: TempPred) - requires - p.equals(q).satisfied_by(ex), - p.satisfied_by(ex), - ensures q.satisfied_by(ex), -{} - proof fn implies_apply_with_always(ex: Execution, p: TempPred, q: TempPred) requires always(p.implies(q)).satisfied_by(ex), @@ -123,15 +116,6 @@ proof fn entails_apply(ex: Execution, p: TempPred, q: TempPred) implies_apply::(ex, p, q); } -proof fn entails_apply_auto() - ensures forall |ex: Execution, p: TempPred, q: TempPred| #[trigger] p.entails(q) && p.satisfied_by(ex) ==> #[trigger] q.satisfied_by(ex), -{ - assert forall |ex: Execution, p: TempPred, q: TempPred| - #[trigger] valid(p.implies(q)) && p.satisfied_by(ex) implies #[trigger] q.satisfied_by(ex) by { - entails_apply(ex, p, q); - }; -} - proof fn not_proved_by_contraposition(ex: Execution, p: TempPred, q: TempPred) requires p.implies(q).satisfied_by(ex), @@ -202,42 +186,6 @@ spec fn eventually_choose_witness(ex: Execution, p: TempPred) -> nat witness } -proof fn equals_to_implies(ex: Execution, p: TempPred, q: TempPred) - requires p.equals(q).satisfied_by(ex), - ensures - p.implies(q).satisfied_by(ex), - q.implies(p).satisfied_by(ex), -{} - -proof fn implies_to_equals(ex: Execution, p: TempPred, q: TempPred) - requires - p.implies(q).satisfied_by(ex), - q.implies(p).satisfied_by(ex), - ensures p.equals(q).satisfied_by(ex), -{} - -proof fn valid_equals_to_valid_implies(p: TempPred, q: TempPred) - requires valid(p.equals(q)), - ensures - valid(p.implies(q)), - valid(q.implies(p)), -{ - assert forall |ex| p.implies(q).satisfied_by(ex) && q.implies(p).satisfied_by(ex) by { - equals_to_implies::(ex, p, q); - }; -} - -proof fn valid_implies_to_valid_equals(p: TempPred, q: TempPred) - requires - valid(p.implies(q)), - valid(q.implies(p)), - ensures valid(p.equals(q)), -{ - assert forall |ex| p.equals(q).satisfied_by(ex) by { - implies_to_equals(ex, p, q); - }; -} - proof fn valid_p_implies_always_p(p: TempPred) requires valid(p), ensures valid(always(p)), @@ -247,15 +195,6 @@ proof fn valid_p_implies_always_p(p: TempPred) }; } -proof fn always_implies_current(p: TempPred) - ensures valid(always(p).implies(p)), -{ - assert forall |ex| always(p).satisfied_by(ex) implies #[trigger] p.satisfied_by(ex) by { - always_unfold(ex, p); - execution_equality::(ex, ex.suffix(0)); - }; -} - proof fn always_distributed_by_and(p: TempPred, q: TempPred) ensures valid(always(p.and(q)).implies(always(p).and(always(q)))), { @@ -346,59 +285,6 @@ proof fn next_preserves_inv_rec(ex: Execution, next: TempPred, inv: Tem } } -proof fn p_is_preserved_before_t(ex: Execution, next: TempPred, p: TempPred, q: TempPred, t: nat, i: nat) - requires - i <= t, - p.satisfied_by(ex), - forall |idx: nat| next.satisfied_by(#[trigger] ex.suffix(idx)), - forall |idx: nat| idx < t ==> !q.satisfied_by(#[trigger] ex.suffix(idx)), - forall |idx: nat| p.satisfied_by(ex.suffix(idx)) && !q.satisfied_by(ex.suffix(idx)) && next.satisfied_by(#[trigger] ex.suffix(idx)) - ==> p.satisfied_by(ex.suffix(idx + 1)), - ensures p.satisfied_by(ex.suffix(i)), - decreases i, -{ - if i == 0 { - execution_equality::(ex, ex.suffix(0)); - } else { - p_is_preserved_before_t::(ex, next, p, q, t, (i-1) as nat); - } -} - -proof fn confluence_at_some_point(ex: Execution, next: TempPred, p: TempPred, q: TempPred, i: nat) - requires - p.satisfied_by(ex), - q.satisfied_by(ex.suffix(i)), - always(p.and(not(q)).and(next).implies(later(p))).satisfied_by(ex), - always(next).satisfied_by(ex), - ensures exists |idx: nat| p.and(q).satisfied_by(#[trigger] ex.suffix(idx)), - decreases i, -{ - if i == 0 { - execution_equality::(ex, ex.suffix(0)); - assert(p.and(q).satisfied_by(ex.suffix(0))); - } else { - if exists |j: nat| { - &&& j < i - &&& q.satisfied_by(#[trigger] ex.suffix(j)) - } { - let t = choose |j: nat| { - &&& j < i - &&& q.satisfied_by(#[trigger] ex.suffix(j)) - }; - confluence_at_some_point::(ex, next, p, q, t); - } else { - assert forall |idx: nat| p.satisfied_by(ex.suffix(idx)) && !q.satisfied_by(ex.suffix(idx)) && next.satisfied_by(#[trigger] ex.suffix(idx)) - implies p.satisfied_by(ex.suffix(idx + 1)) by { - always_unfold::(ex, p.and(not(q)).and(next).implies(later(p))); - implies_apply::(ex.suffix(idx), p.and(not(q)).and(next), later(p)); - execution_equality::(ex.suffix(idx).suffix(1), ex.suffix(idx + 1)); - }; - p_is_preserved_before_t::(ex, next, p, q, i, i); - assert(p.and(q).satisfied_by(ex.suffix(i))); - } - } -} - proof fn instantiate_entailed_always(ex: Execution, i: nat, spec: TempPred, p: TempPred) requires spec.satisfied_by(ex), @@ -446,11 +332,12 @@ pub proof fn execution_equality(ex1: Execution, ex2: Execution) } pub proof fn temp_pred_equality(p: TempPred, q: TempPred) - requires valid(p.equals(q)), + requires + p.entails(q), + q.entails(p), ensures p == q, { assert forall |ex: Execution| #[trigger] (p.pred)(ex) == (q.pred)(ex) by { - valid_equals_to_valid_implies::(p, q); if (p.pred)(ex) { implies_apply::(ex, p, q); } else { @@ -538,7 +425,7 @@ proof fn p_and_always_p_equals_always_p(p: TempPred) } proof fn a_to_temp_pred_equality(p: spec_fn(A) -> TempPred, q: spec_fn(A) -> TempPred) - requires forall |a: A| #[trigger] valid(p(a).equals(q(a))), + requires forall |a: A| #[trigger] p(a).entails(q(a)) && q(a).entails(p(a)), ensures p == q, { assert forall |a: A| #[trigger] p(a) == q(a) by { @@ -598,7 +485,7 @@ pub proof fn tla_forall_always_equality(a_to_p: spec_fn(A) -> TempPred) } pub proof fn tla_forall_always_equality_variant(a_to_always: spec_fn(A) -> TempPred, a_to_p: spec_fn(A) -> TempPred) - requires forall |a: A| #![trigger a_to_always(a)] valid(a_to_always(a).equals((|a: A| always(a_to_p(a)))(a))), + requires forall |a: A| #![trigger a_to_always(a)] a_to_always(a).entails((|a: A| always(a_to_p(a)))(a)) && ((|a: A| always(a_to_p(a)))(a)).entails(a_to_always(a)), ensures tla_forall(a_to_always) == always(tla_forall(a_to_p)), { a_to_temp_pred_equality::(a_to_always, |a: A| always(a_to_p(a))); @@ -796,8 +683,8 @@ pub proof fn use_tla_forall(spec: TempPred, a_to_p: spec_fn(A) -> TempP requires spec.entails(tla_forall(a_to_p)), ensures spec.entails(a_to_p(a)), { - entails_apply_auto::(); - assert forall |ex: Execution| #[trigger] spec.implies(a_to_p(a)).satisfied_by(ex) by { + assert forall |ex: Execution| #[trigger] spec.satisfied_by(ex) implies (a_to_p(a)).satisfied_by(ex) by { + entails_apply(ex, spec, tla_forall(a_to_p)); assert(spec.implies(tla_forall(a_to_p)).satisfied_by(ex)); }; } @@ -1280,7 +1167,8 @@ pub proof fn strengthen_next(spec: TempPred, next: ActionPred, inv: Sta requires spec.entails(always(lift_action(next))), spec.entails(always(lift_state(inv))), - valid(lift_action(next_and_inv).equals(lift_action(next).and(lift_state(inv)))), + lift_action(next_and_inv).entails(lift_action(next).and(lift_state(inv))), + lift_action(next).and(lift_state(inv)).entails(lift_action(next_and_inv)), ensures spec.entails(always(lift_action(next_and_inv))), { entails_and_temp::(spec, always(lift_action(next)), always(lift_state(inv))); From 539a9237aa3de1620a7d750c3ae3b525a172912e Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Tue, 17 Sep 2024 12:01:12 -0500 Subject: [PATCH 3/4] Rename Signed-off-by: Xudong Sun --- .../proof/helper_invariants/proof.rs | 8 +-- .../proof/helper_invariants/unchangeable.rs | 2 +- .../proof/liveness/daemon_set_match.rs | 8 +-- .../fluentbit/proof/liveness/proof.rs | 8 +-- .../proof/liveness/resource_match.rs | 10 +-- .../fluentbit/proof/liveness/spec.rs | 2 +- .../proof/helper_invariants/proof.rs | 6 +- .../fluentbit_config/proof/liveness/proof.rs | 4 +- .../proof/liveness/resource_match.rs | 4 +- .../proof/helper_invariants/proof.rs | 22 +++--- .../proof/helper_invariants/unchangeable.rs | 2 +- .../proof/helper_invariants/validation.rs | 2 +- .../proof/liveness/proof.rs | 12 ++-- .../proof/liveness/resource_match.rs | 10 +-- .../proof/liveness/stateful_set_match.rs | 8 +-- .../proof/liveness/proof.rs | 2 +- .../proof/liveness/resource_match.rs | 2 +- .../proof/helper_invariants/proof.rs | 20 +++--- .../proof/helper_invariants/unchangeable.rs | 2 +- .../proof/liveness/proof.rs | 12 ++-- .../proof/liveness/resource_match.rs | 6 +- .../proof/liveness/stateful_set_match.rs | 6 +- .../proof/liveness/zookeeper_api.rs | 8 +-- .../proof/api_server_liveness.rs | 10 +-- .../proof/builtin_controllers.rs | 4 +- src/kubernetes_cluster/proof/cluster.rs | 4 +- .../controller_runtime_eventual_safety.rs | 8 +-- .../proof/controller_runtime_liveness.rs | 2 +- .../proof/daemon_set_controller.rs | 8 +-- .../proof/stateful_set_controller.rs | 8 +-- .../proof/validation_rule.rs | 4 +- src/state_machine/action.rs | 8 +-- src/temporal_logic/rules.rs | 71 ++++++++++--------- .../proof/controller_runtime_liveness.rs | 2 +- .../proof/failures_liveness.rs | 4 +- .../proof/garbage_collector.rs | 4 +- src/v2/kubernetes_cluster/proof/network.rs | 2 +- .../proof/network_liveness.rs | 10 +-- .../proof/objects_in_store.rs | 2 +- 39 files changed, 162 insertions(+), 155 deletions(-) diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs index 9badd55f4..861f0f8c5 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs @@ -961,9 +961,9 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po { let key = get_request(sub_resource, fb).key; let eventual_owner_ref = |owner_ref: Option>| {owner_ref == Some(seq![fb.controller_owner_ref()])}; - always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fb)), lift_state(FBCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb)), lift_state(FBCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fb)), lift_state(FBCluster::object_has_no_finalizers(key))); + always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fb)), lift_state(FBCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb)), lift_state(FBCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fb)), lift_state(FBCluster::object_has_no_finalizers(key))); let state = |s: FBCluster| { desired_state_is(fb)(s) @@ -1008,7 +1008,7 @@ pub proof fn lemma_eventually_always_daemon_set_not_exists_or_matches_or_no_more { let ds_key = get_request(SubResource::DaemonSet, fb).key; let make_fn = || make_daemon_set(fb); - implies_preserved_by_always_temp( + entails_preserved_by_always( lift_state(every_resource_create_request_implies_at_after_create_resource_step(SubResource::DaemonSet, fb)), lift_state(FBCluster::every_in_flight_create_req_msg_for_this_ds_matches(ds_key, make_fn)) ); diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs index 6a6c5a767..ddf06a4fb 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs @@ -151,7 +151,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred, fb: FluentBit } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } } diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs index 3a5ec8272..f427ff9d2 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs @@ -84,7 +84,7 @@ proof fn spec_before_phase_n_entails_true_leads_to_current_state_matches(i: nat, spec_of_previous_phases_entails_eventually_new_invariants(i, fb); unpack_conditions_from_spec(spec_before_phase_n(i, fb), invariants_since_phase_n(i, fb), true_pred(), always(lift_state(current_state_matches::(fb)))); temp_pred_equality(true_pred().and(invariants_since_phase_n(i, fb)), invariants_since_phase_n(i, fb)); - leads_to_trans_temp(spec_before_phase_n(i, fb), true_pred(), invariants_since_phase_n(i, fb), always(lift_state(current_state_matches::(fb)))); + leads_to_trans(spec_before_phase_n(i, fb), true_pred(), invariants_since_phase_n(i, fb), always(lift_state(current_state_matches::(fb)))); } proof fn lemma_true_leads_to_always_current_state_matches(fb: FluentBitView) @@ -160,13 +160,13 @@ proof fn lemma_true_leads_to_always_state_matches_for_all_resources(fb: FluentBi if sub_resource != SubResource::DaemonSet { let next_resource = next_resource_after(sub_resource).get_AfterKRequestStep_1(); lemma_from_after_get_resource_step_to_resource_matches(spec, fb, sub_resource, next_resource); - leads_to_trans_temp( + leads_to_trans( spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, fb)), lift_state(sub_resource_state_matches(sub_resource, fb)) ); } else { lemma_from_after_get_daemon_set_step_to_daemon_set_matches(spec, fb); - leads_to_trans_temp( + leads_to_trans( spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::DaemonSet, fb)), lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb)) ); @@ -209,7 +209,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, fb: F let input = fb.object_ref(); FBCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCluster::next(), desired_state_is(fb), pre, post); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); - or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); + or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCluster| {!s.ongoing_reconciles().contains_key(fb.object_ref())})); } diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs index 842e217bc..309851623 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs @@ -66,12 +66,12 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches( &&& s.resources().contains_key(get_request(sub_resource, fb).key) &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, fb)(s) }); - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fb))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fb))); temp_pred_equality( key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, fb)) ); if next_resource_after(sub_resource) == after_get_k_request_step(next_resource) { - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, fb))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, fb))); } } @@ -538,7 +538,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(spec: &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb)(s) &&& helper_invariants::no_create_resource_request_msg_without_name_in_flight(sub_resource, fb)(s) }; - always_weaken_temp(spec, lift_state(FBCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key)); + always_weaken(spec, lift_state(FBCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key)); combine_spec_entails_always_n!( spec, lift_action(stronger_next), lift_action(FBCluster::next()), @@ -854,7 +854,7 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(spec: &&& helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, fb)(s) &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fb)(s) }; - always_weaken_temp(spec, lift_state(FBCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); + always_weaken(spec, lift_state(FBCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); combine_spec_entails_always_n!( spec, lift_action(stronger_next), @@ -941,7 +941,7 @@ pub proof fn lemma_resource_object_is_stable(spec: TempPred, sub_reso } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } } diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs index 6371019e8..c69a93613 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs @@ -75,7 +75,7 @@ pub proof fn spec_of_previous_phases_entails_eventually_new_invariants(i: nat, f { let spec = spec_before_phase_n(i, fb); reveal_with_fuel(spec_before_phase_n, 8); - implies_preserved_by_always_temp(lift_state(desired_state_is(fb)), lift_state(FBCluster::desired_state_is(fb))); + entails_preserved_by_always(lift_state(desired_state_is(fb)), lift_state(FBCluster::desired_state_is(fb))); entails_trans(spec, always(lift_state(desired_state_is(fb))), always(lift_state(FBCluster::desired_state_is(fb)))); if i == 1 { FBCluster::lemma_true_leads_to_crash_always_disabled(spec); diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs index 999136ad0..d61b13ad4 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs @@ -842,9 +842,9 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po { let key = get_request(sub_resource, fbc).key; let eventual_owner_ref = |owner_ref: Option>| {owner_ref == Some(seq![fbc.controller_owner_ref()])}; - always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fbc)), lift_state(FBCCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fbc)), lift_state(FBCCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fbc)), lift_state(FBCCluster::object_has_no_finalizers(key))); + always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fbc)), lift_state(FBCCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fbc)), lift_state(FBCCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fbc)), lift_state(FBCCluster::object_has_no_finalizers(key))); let state = |s: FBCCluster| { desired_state_is(fbc)(s) diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs index c537427b8..16fc87a81 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs @@ -75,7 +75,7 @@ proof fn spec_before_phase_n_entails_true_leads_to_current_state_matches(i: nat, spec_of_previous_phases_entails_eventually_new_invariants(i, fbc); unpack_conditions_from_spec(spec_before_phase_n(i, fbc), invariants_since_phase_n(i, fbc), true_pred(), always(lift_state(current_state_matches::(fbc)))); temp_pred_equality(true_pred().and(invariants_since_phase_n(i, fbc)), invariants_since_phase_n(i, fbc)); - leads_to_trans_temp(spec_before_phase_n(i, fbc), true_pred(), invariants_since_phase_n(i, fbc), always(lift_state(current_state_matches::(fbc)))); + leads_to_trans(spec_before_phase_n(i, fbc), true_pred(), invariants_since_phase_n(i, fbc), always(lift_state(current_state_matches::(fbc)))); } proof fn lemma_true_leads_to_always_current_state_matches(fbc: FluentBitConfigView) @@ -149,7 +149,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, fbc: let input = fbc.object_ref(); FBCCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCCluster::next(), desired_state_is(fbc), pre, post); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); - or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); + or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCCluster| {!s.ongoing_reconciles().contains_key(fbc.object_ref())})); } diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs index 0500439a3..1c49a7f26 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs @@ -53,7 +53,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches(spec: TempPr &&& s.resources().contains_key(get_request(sub_resource, fbc).key) &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, fbc)(s) }); - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fbc))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fbc))); temp_pred_equality( key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, fbc)) ); @@ -712,7 +712,7 @@ pub proof fn lemma_resource_object_is_stable( } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } } diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs index e49947ef7..4ccc3d67f 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs +++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs @@ -144,7 +144,7 @@ proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updat &&& object_in_response_at_after_update_resource_step_is_same_as_etcd(SubResource::ServerConfigMap, rabbitmq)(s) &&& object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq)(s) }; - always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); + always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); always_to_always_later(spec, lift_state(resource_well_formed)); combine_spec_entails_always_n!( spec, lift_action(next), lift_action(RMQCluster::next()), @@ -155,7 +155,7 @@ proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updat lift_state(object_in_response_at_after_update_resource_step_is_same_as_etcd(SubResource::ServerConfigMap, rabbitmq)), lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq)) ); - leads_to_weaken_temp( + leads_to_weaken( spec, true_pred(), lift_state(|s: RMQCluster| !s.ongoing_reconciles().contains_key(rabbitmq.object_ref())), true_pred(), lift_state(inv) ); @@ -183,7 +183,7 @@ proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updat } } } - leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv)); + leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv)); } pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd_forall( @@ -257,7 +257,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_create_resource_ste lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq)), lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ServerConfigMap, rabbitmq)) ); - leads_to_weaken_temp( + leads_to_weaken( spec, true_pred(), lift_state(|s: RMQCluster| !s.ongoing_reconciles().contains_key(rabbitmq.object_ref())), true_pred(), lift_state(inv) ); @@ -295,7 +295,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_create_resource_ste } } } - leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv)); + leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv)); } #[verifier(spinoff_prover)] @@ -440,7 +440,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_update_resource_ste lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq)), lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ServerConfigMap, rabbitmq)) ); - leads_to_weaken_temp( + leads_to_weaken( spec, true_pred(), lift_state(|s: RMQCluster| !s.ongoing_reconciles().contains_key(rabbitmq.object_ref())), true_pred(), lift_state(inv) ); @@ -476,7 +476,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_update_resource_ste object_in_response_at_after_update_resource_step_is_same_as_etcd_helper(s, s_prime, rabbitmq); } } - leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv)); + leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv)); } #[verifier(spinoff_prover)] @@ -1555,7 +1555,7 @@ proof fn lemma_eventually_always_no_delete_resource_request_msg_in_flight(spec: &&& resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, rabbitmq)(s) &&& resource_well_formed(s) }; - always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); + always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); assert forall |s: RMQCluster, s_prime: RMQCluster| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { assert forall |msg: RMQMessage| (!s.in_flight().contains(msg) || requirements(msg, s)) && #[trigger] s_prime.in_flight().contains(msg) implies requirements(msg, s_prime) by { @@ -1648,9 +1648,9 @@ proof fn lemma_eventually_always_resource_object_only_has_owner_reference_pointi { let key = get_request(sub_resource, rabbitmq).key; let eventual_owner_ref = |owner_ref: Option>| {owner_ref == Some(seq![rabbitmq.controller_owner_ref()])}; - always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, rabbitmq)), lift_state(RMQCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, rabbitmq)), lift_state(RMQCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, rabbitmq)), lift_state(RMQCluster::object_has_no_finalizers(key))); + always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, rabbitmq)), lift_state(RMQCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, rabbitmq)), lift_state(RMQCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, rabbitmq)), lift_state(RMQCluster::object_has_no_finalizers(key))); let state = |s: RMQCluster| { RMQCluster::desired_state_is(rabbitmq)(s) diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs index 3018af5f8..4c7e38fe0 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs +++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs @@ -151,7 +151,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred(rabbitmq)))); temp_pred_equality(true_pred().and(invariants_since_phase_n(i, rabbitmq)), invariants_since_phase_n(i, rabbitmq)); - leads_to_trans_temp(spec_before_phase_n(i, rabbitmq), true_pred(), invariants_since_phase_n(i, rabbitmq), always(lift_state(current_state_matches::(rabbitmq)))); + leads_to_trans(spec_before_phase_n(i, rabbitmq), true_pred(), invariants_since_phase_n(i, rabbitmq), always(lift_state(current_state_matches::(rabbitmq)))); } proof fn lemma_true_leads_to_always_current_state_matches(rabbitmq: RabbitmqClusterView) @@ -178,7 +178,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_all_but_stateful_set(rabbi always_tla_forall_apply_for_sub_resource(spec, sub_resource, rabbitmq); let next_resource = next_resource_after(sub_resource).get_AfterKRequestStep_1(); lemma_from_after_get_resource_step_to_resource_matches(spec, rabbitmq, sub_resource, next_resource); - leads_to_trans_temp( + leads_to_trans( spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, rabbitmq)), lift_state(sub_resource_state_matches(sub_resource, rabbitmq)) ); @@ -259,7 +259,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(rabbitmq: Rab ); // We then prove pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq) ~> sub_resource_state_matches(SubResource::StatefulSet, rabbitmq) lemma_from_after_get_stateful_set_step_to_stateful_set_matches(spec, rabbitmq); - leads_to_trans_temp( + leads_to_trans( spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq)), lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)) ); @@ -271,13 +271,13 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(rabbitmq: Rab unpack_conditions_from_spec(spec2, always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)))); temp_pred_equality(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), true_pred().and(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))))); helper_invariants::lemma_eventually_always_stateful_set_not_exists_or_matches_or_no_more_status_update(spec2, rabbitmq); - leads_to_trans_temp(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)))); + leads_to_trans(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)))); }); assert_by(spec1.entails(true_pred().leads_to(always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))))), { unpack_conditions_from_spec(spec1, always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)))); temp_pred_equality(always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), true_pred().and(always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))))); - leads_to_trans_temp(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)))); + leads_to_trans(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)))); }); } @@ -304,7 +304,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, rabb let input = rabbitmq.object_ref(); RMQCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, RMQCluster::next(), RMQCluster::desired_state_is(rabbitmq), pre, post); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); - or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); + or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: RMQCluster| {!s.ongoing_reconciles().contains_key(rabbitmq.object_ref())})); } diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs index 57c54e2b7..77b2629eb 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs @@ -73,12 +73,12 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches( &&& s.resources().contains_key(get_request(sub_resource, rabbitmq).key) &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, rabbitmq)(s) }); - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, rabbitmq))); temp_pred_equality( key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, rabbitmq)) ); if next_resource_after(sub_resource) == after_get_k_request_step(next_resource) { - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, rabbitmq))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, rabbitmq))); } } @@ -562,7 +562,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step( &&& helper_invariants::no_create_resource_request_msg_without_name_in_flight(sub_resource, rabbitmq)(s) &&& helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(rabbitmq)(s) }; - always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key)); + always_weaken(spec, lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key)); combine_spec_entails_always_n!( spec, lift_action(stronger_next), lift_action(RMQCluster::next()), @@ -919,7 +919,7 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step( &&& helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, rabbitmq)(s) &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, rabbitmq)(s) }; - always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); + always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); combine_spec_entails_always_n!( spec, lift_action(stronger_next), @@ -1013,7 +1013,7 @@ pub proof fn lemma_resource_object_is_stable( } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } } diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs index 9d5839f81..76e4835a3 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs @@ -67,7 +67,7 @@ pub proof fn lemma_from_after_get_stateful_set_step_to_stateful_set_matches( &&& s.resources().contains_key(get_request(SubResource::StatefulSet, rabbitmq).key) &&& pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq)(s) }); - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))); temp_pred_equality( key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq)) ); @@ -190,7 +190,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m leads_to_trans_n!(spec, stateful_set_not_matches, post1, post2, post); }); - or_leads_to_combine_temp(spec, stateful_set_matches, stateful_set_not_matches, post); + or_leads_to_combine(spec, stateful_set_matches, stateful_set_not_matches, post); temp_pred_equality(stateful_set_matches.or(stateful_set_not_matches), pre); } @@ -438,7 +438,7 @@ proof fn lemma_stateful_set_state_matches_at_after_update_stateful_set_step(spec &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, rabbitmq)(s) &&& helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(rabbitmq)(s) }; - always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); + always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); combine_spec_entails_always_n!( spec, lift_action(stronger_next), lift_action(RMQCluster::next()), @@ -526,7 +526,7 @@ pub proof fn lemma_stateful_set_is_stable(spec: TempPred, rabbitmq: } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } } diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs index b3d3181dc..39b23fcbf 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs @@ -170,7 +170,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, vrs: let input = vrs.object_ref(); VRSCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, VRSCluster::next(), VRSCluster::desired_state_is(vrs), pre, post); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); - or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); + or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: VRSCluster| {!s.ongoing_reconciles().contains_key(vrs.object_ref())})); } diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs index cca547470..b369e4ed5 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs @@ -1860,7 +1860,7 @@ pub proof fn lemma_current_state_matches_is_stable( } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } // // TODO: Prove this. 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 e68e1f2dc..52ad3e2e0 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs @@ -158,7 +158,7 @@ pub proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_u lift_state(object_in_response_at_after_update_resource_step_is_same_as_etcd(SubResource::ConfigMap, zookeeper)), lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)) ); - leads_to_weaken_temp( + leads_to_weaken( spec, true_pred(), lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())), true_pred(), lift_state(inv) ); @@ -176,7 +176,7 @@ pub proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_u } } } - leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv)); + leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv)); } pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd_forall( @@ -254,7 +254,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource 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)) ); - leads_to_weaken_temp( + leads_to_weaken( spec, true_pred(), lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())), true_pred(), lift_state(inv) ); @@ -327,7 +327,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource } } } - leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv)); + leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv)); } pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource_step_is_same_as_etcd_forall( @@ -405,7 +405,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource 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)) ); - leads_to_weaken_temp( + leads_to_weaken( spec, true_pred(), lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())), true_pred(), lift_state(inv) ); @@ -479,7 +479,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource } } } - leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv)); + leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv)); } #[verifier(spinoff_prover)] @@ -1347,7 +1347,7 @@ pub proof fn lemma_eventually_always_no_delete_resource_request_msg_in_flight(sp &&& resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)(s) &&& resource_well_formed(s) }; - always_weaken_temp(spec, lift_state(ZKCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); + always_weaken(spec, lift_state(ZKCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed)); assert forall |s: ZKCluster, s_prime: ZKCluster| #[trigger] stronger_next(s, s_prime) implies ZKCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { assert forall |msg: ZKMessage| (!s.in_flight().contains(msg) || requirements(msg, s)) && #[trigger] s_prime.in_flight().contains(msg) implies requirements(msg, s_prime) by { @@ -1436,9 +1436,9 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po { let key = get_request(sub_resource, zookeeper).key; let eventual_owner_ref = |owner_ref: Option>| {owner_ref == Some(seq![zookeeper.controller_owner_ref()])}; - always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, zookeeper)), lift_state(ZKCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)), lift_state(ZKCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); - always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)), lift_state(ZKCluster::object_has_no_finalizers(key))); + always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, zookeeper)), lift_state(ZKCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)), lift_state(ZKCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref))); + always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)), lift_state(ZKCluster::object_has_no_finalizers(key))); let state = |s: ZKCluster| { ZKCluster::desired_state_is(zookeeper)(s) 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 be5e266e4..69c903808 100644 --- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs +++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs @@ -156,7 +156,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred(zookeeper)))); temp_pred_equality(true_pred().and(invariants_since_phase_n(i, zookeeper)), invariants_since_phase_n(i, zookeeper)); - leads_to_trans_temp(spec_before_phase_n(i, zookeeper), true_pred(), invariants_since_phase_n(i, zookeeper), always(lift_state(current_state_matches::(zookeeper)))); + leads_to_trans(spec_before_phase_n(i, zookeeper), true_pred(), invariants_since_phase_n(i, zookeeper), always(lift_state(current_state_matches::(zookeeper)))); } proof fn lemma_true_leads_to_always_current_state_matches(zookeeper: ZookeeperClusterView) @@ -173,7 +173,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_all_but_stateful_set(zooke ) by { always_tla_forall_apply_for_sub_resource(spec, sub_resource, zookeeper); lemma_from_after_get_resource_step_to_resource_matches(spec, zookeeper, sub_resource); - leads_to_trans_temp( + leads_to_trans( spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, zookeeper)), lift_state(sub_resource_state_matches(sub_resource, zookeeper)) ); @@ -251,7 +251,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(zookeeper: Zo // We then prove pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper) ~> sub_resource_state_matches(SubResource::StatefulSet, zookeeper) lemma_from_after_get_stateful_set_step_to_stateful_set_matches(spec, zookeeper); - leads_to_trans_temp( + leads_to_trans( spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper)), lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)) ); @@ -263,13 +263,13 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(zookeeper: Zo unpack_conditions_from_spec(spec2, always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)))); temp_pred_equality(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), true_pred().and(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))))); helper_invariants::lemma_eventually_always_stateful_set_not_exists_or_matches_or_no_more_status_update(spec2, zookeeper); - leads_to_trans_temp(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)))); + leads_to_trans(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)))); }); assert_by(spec1.entails(true_pred().leads_to(always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))))), { unpack_conditions_from_spec(spec1, always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)))); temp_pred_equality(always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), true_pred().and(always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))))); - leads_to_trans_temp(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)))); + leads_to_trans(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)))); }); } @@ -296,7 +296,7 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, zooke let input = zookeeper.object_ref(); ZKCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, ZKCluster::next(), ZKCluster::desired_state_is(zookeeper), pre, post); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); - or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post)); + or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: ZKCluster| {!s.ongoing_reconciles().contains_key(zookeeper.object_ref())})); } 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 2fd5b4705..9fbc73f70 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs @@ -72,7 +72,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches( &&& s.resources().contains_key(get_request(sub_resource, zookeeper).key) &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, zookeeper)(s) }); - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, zookeeper))); temp_pred_equality( key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, zookeeper)) ); @@ -82,7 +82,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches( } else { pending_req_in_flight_at_after_exists_stateful_set_step(zookeeper) // ConfigMap is a bit different since its next step is not a SubResource type }; - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(next_state)); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(next_state)); } pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_matches( @@ -1005,7 +1005,7 @@ pub proof fn lemma_resource_object_is_stable(spec: TempPred, sub_reso } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } } 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 2006a543c..d0a8897ee 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 @@ -62,7 +62,7 @@ pub proof fn lemma_from_after_get_stateful_set_step_to_stateful_set_matches( &&& s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key) &&& pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper)(s) }); - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))); temp_pred_equality( key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper)) ); @@ -188,7 +188,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m leads_to_trans_n!(spec, stateful_set_not_matches, post1, post2, post); }); - or_leads_to_combine_temp(spec, stateful_set_matches, stateful_set_not_matches, post); + or_leads_to_combine(spec, stateful_set_matches, stateful_set_not_matches, post); temp_pred_equality(stateful_set_matches.or(stateful_set_not_matches), pre); } @@ -526,7 +526,7 @@ pub proof fn lemma_stateful_set_is_stable( } } - leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post)); } } 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 8ac9c398f..8eb865521 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs @@ -65,7 +65,7 @@ pub proof fn lemma_from_after_exists_stateful_set_step_to_after_get_stateful_set &&& s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key) &&& pending_req_in_flight_at_after_exists_stateful_set_step(zookeeper)(s) }); - or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper))); + or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper))); temp_pred_equality(key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_exists_stateful_set_step(zookeeper))); } @@ -230,7 +230,7 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_exists_to_after_get_s temp_pred_equality(tla_exists(after_exists_stateful_set_step_resp_msg), after_exists_stateful_set_step_waiting); }); - leads_to_trans_temp(spec, pre, after_exists_stateful_set_step_waiting, after_exists_zk_node_step_pending); + leads_to_trans(spec, pre, after_exists_stateful_set_step_waiting, after_exists_zk_node_step_pending); }); assert_by(spec.entails(after_exists_zk_node_step_pending.leads_to(post)) , { @@ -483,10 +483,10 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_exists_to_after_get_s ); }); - or_leads_to_combine_temp(spec, addr_exists_and_after_exists_zk_node_step_pending, addr_not_exists_and_after_exists_zk_node_step_pending, post); + or_leads_to_combine(spec, addr_exists_and_after_exists_zk_node_step_pending, addr_not_exists_and_after_exists_zk_node_step_pending, post); temp_pred_equality(addr_exists_and_after_exists_zk_node_step_pending.or(addr_not_exists_and_after_exists_zk_node_step_pending), after_exists_zk_node_step_pending); }); - leads_to_trans_temp(spec, pre, after_exists_zk_node_step_pending, post); + leads_to_trans(spec, pre, after_exists_zk_node_step_pending, post); } proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_stateful_set_step(spec: TempPred, zookeeper: ZookeeperClusterView, req_msg: ZKMessage) diff --git a/src/kubernetes_cluster/proof/api_server_liveness.rs b/src/kubernetes_cluster/proof/api_server_liveness.rs index c92fad8f2..e8fcdd67a 100644 --- a/src/kubernetes_cluster/proof/api_server_liveness.rs +++ b/src/kubernetes_cluster/proof/api_server_liveness.rs @@ -238,7 +238,7 @@ pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfie Self::lemma_true_leads_to_always_no_req_before_rest_id_is_in_flight(spec_with_rest_id, rest_id); - implies_preserved_by_always_temp( + entails_preserved_by_always( lift_state(invariant), lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)) .implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) @@ -247,8 +247,8 @@ pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfie spec_with_rest_id, always(lift_state(invariant)), always(lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)).implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))) ); - always_implies_preserved_by_always_temp(spec_with_rest_id, lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements))); - leads_to_weaken_temp( + always_implies_preserved_by_always(spec_with_rest_id, lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements))); + leads_to_weaken( spec_with_rest_id, true_pred(), always(lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id))), true_pred(), always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) @@ -293,7 +293,7 @@ pub proof fn lemma_true_leads_to_always_no_req_before_rest_id_is_in_flight(spec: } } - leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id))); + leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id))); } pub proof fn lemma_eventually_no_req_before_rest_id_is_in_flight(spec: TempPred, rest_id: RestId) @@ -406,7 +406,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(spec: T Self::lemma_pending_requests_number_is_n_leads_to_no_pending_requests( spec, rest_id, (msg_num - 1) as nat ); - leads_to_trans_temp( + leads_to_trans( spec, pending_requests_num_is_msg_num, pending_requests_num_is_msg_num_minus_1, no_more_pending_requests ); } diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs index 220e43d5c..ac43ab471 100644 --- a/src/kubernetes_cluster/proof/builtin_controllers.rs +++ b/src/kubernetes_cluster/proof/builtin_controllers.rs @@ -208,7 +208,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies( leads_to_trans_n!(spec, lift_state(pre), lift_state(delete_msg_in_flight), lift_state(post)); temp_pred_equality(lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(Self::garbage_collector_deletion_enabled(key))), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(pre))); - leads_to_weaken_temp(spec, lift_state(pre), lift_state(post), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)), lift_state(post)); + leads_to_weaken(spec, lift_state(pre), lift_state(post), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)), lift_state(post)); } ); @@ -227,7 +227,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies( } } - leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(post)); } proof fn lemma_delete_msg_in_flight_leads_to_owner_references_satisfies( diff --git a/src/kubernetes_cluster/proof/cluster.rs b/src/kubernetes_cluster/proof/cluster.rs index 8c03ac966..69b33f388 100644 --- a/src/kubernetes_cluster/proof/cluster.rs +++ b/src/kubernetes_cluster/proof/cluster.rs @@ -59,7 +59,7 @@ pub proof fn lemma_true_leads_to_crash_always_disabled( { let true_state = |s: Self| true; Self::disable_crash().wf1((), spec, Self::next(), true_state, Self::crash_disabled()); - leads_to_stable_temp::(spec, lift_action(Self::next()), true_pred(), lift_state(Self::crash_disabled())); + leads_to_stable::(spec, lift_action(Self::next()), true_pred(), lift_state(Self::crash_disabled())); } pub proof fn lemma_true_leads_to_busy_always_disabled( @@ -72,7 +72,7 @@ pub proof fn lemma_true_leads_to_busy_always_disabled( { let true_state = |s: Self| true; Self::disable_transient_failure().wf1((), spec, Self::next(), true_state, Self::busy_disabled()); - leads_to_stable_temp::(spec, lift_action(Self::next()), true_pred(), lift_state(Self::busy_disabled())); + leads_to_stable::(spec, lift_action(Self::next()), true_pred(), lift_state(Self::busy_disabled())); } // This desired_state_is specifies the desired state (described in the cr object) diff --git a/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs b/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs index 273ae2a8f..12411ea75 100644 --- a/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs +++ b/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs @@ -49,7 +49,7 @@ pub proof fn lemma_true_leads_to_always_the_object_in_schedule_has_spec_and_uid_ Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec( spec, input, stronger_next, Self::desired_state_is(cr), pre, post ); - leads_to_stable_temp(spec, lift_action(stronger_next), lift_state(pre), lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), lift_state(pre), lift_state(post)); } pub open spec fn the_object_in_reconcile_has_spec_and_uid_as(cr: K) -> StatePred { @@ -107,7 +107,7 @@ pub proof fn lemma_true_leads_to_always_the_object_in_reconcile_has_spec_and_uid ); } ); - leads_to_trans_temp(spec, lift_state(not_scheduled_or_reconcile), lift_state(scheduled_and_not_reconcile), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr))); + leads_to_trans(spec, lift_state(not_scheduled_or_reconcile), lift_state(scheduled_and_not_reconcile), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr))); let not_reconcile = |s: Self| !s.ongoing_reconciles().contains_key(cr.object_ref()); or_leads_to_combine_and_equality!( @@ -115,11 +115,11 @@ pub proof fn lemma_true_leads_to_always_the_object_in_reconcile_has_spec_and_uid lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr)) ); - leads_to_trans_temp( + leads_to_trans( spec, true_pred(), lift_state(|s: Self| !s.ongoing_reconciles().contains_key(cr.object_ref())), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr)) ); - leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr))); + leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr))); } } diff --git a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs index 0685309e8..f2aedfef3 100644 --- a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs +++ b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs @@ -269,7 +269,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state( Self::lemma_from_in_flight_resp_matches_pending_req_at_some_state_to_next_state(spec, cr, state, next_state); Self::lemma_from_pending_req_in_flight_at_some_state_to_next_state(spec, cr, state, next_state); - or_leads_to_combine_temp(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), next_state))); + or_leads_to_combine(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), next_state))); temp_pred_equality::( lift_state(req_in_flight).or(lift_state(resp_in_flight)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight) diff --git a/src/kubernetes_cluster/proof/daemon_set_controller.rs b/src/kubernetes_cluster/proof/daemon_set_controller.rs index 17394de3d..ec75bee05 100644 --- a/src/kubernetes_cluster/proof/daemon_set_controller.rs +++ b/src/kubernetes_cluster/proof/daemon_set_controller.rs @@ -135,7 +135,7 @@ pub proof fn lemma_true_leads_to_always_daemon_set_not_exist_or_updated_or_no_mo } } - leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(post)); } proof fn lemma_true_leads_to_daemon_set_not_exist_or_updated_or_no_more_pending_req(spec: TempPred, key: ObjectRef, make_fn: spec_fn() -> DaemonSetView) @@ -186,12 +186,12 @@ proof fn lemma_true_leads_to_daemon_set_not_exist_or_updated_or_no_more_pending_ }); temp_pred_equality(lift_state(|s: Self| s.stable_resources().contains(key)).or(lift_state(key_not_exists)), lift_state(key_not_exists_or_stable)); temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post)); - sandwich_leads_to_by_or_temp(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists)); - leads_to_trans_temp(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post)); + leads_to_framed_by_or(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists)); + leads_to_trans(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post)); }); temp_pred_equality(lift_state(key_exists).or(lift_state(key_not_exists)), true_pred()); temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post)); - sandwich_leads_to_by_or_temp(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists)); + leads_to_framed_by_or(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists)); } proof fn lemma_pending_update_status_req_num_is_n_leads_to_daemon_set_not_exist_or_updated_or_no_more_pending_req(spec: TempPred, key: ObjectRef, make_fn: spec_fn() -> DaemonSetView, msg_num: nat) diff --git a/src/kubernetes_cluster/proof/stateful_set_controller.rs b/src/kubernetes_cluster/proof/stateful_set_controller.rs index f608217cd..a9e60055b 100644 --- a/src/kubernetes_cluster/proof/stateful_set_controller.rs +++ b/src/kubernetes_cluster/proof/stateful_set_controller.rs @@ -184,7 +184,7 @@ pub proof fn lemma_true_leads_to_always_stateful_set_not_exist_or_updated_or_no_ } } - leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(post)); + leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(post)); } proof fn lemma_true_leads_to_stateful_set_not_exist_or_updated_or_no_more_pending_req(spec: TempPred, key: ObjectRef, cm_key: ObjectRef, make_fn: spec_fn(rv: StringView) -> StatefulSetView) @@ -236,12 +236,12 @@ proof fn lemma_true_leads_to_stateful_set_not_exist_or_updated_or_no_more_pendin }); temp_pred_equality(lift_state(|s: Self| s.stable_resources().contains(key)).or(lift_state(key_not_exists)), lift_state(key_not_exists_or_stable)); temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post)); - sandwich_leads_to_by_or_temp(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists)); - leads_to_trans_temp(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post)); + leads_to_framed_by_or(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists)); + leads_to_trans(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post)); }); temp_pred_equality(lift_state(key_exists).or(lift_state(key_not_exists)), true_pred()); temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post)); - sandwich_leads_to_by_or_temp(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists)); + leads_to_framed_by_or(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists)); } proof fn lemma_pending_update_status_req_num_is_n_leads_to_stateful_set_not_exist_or_updated_or_no_more_pending_req( diff --git a/src/kubernetes_cluster/proof/validation_rule.rs b/src/kubernetes_cluster/proof/validation_rule.rs index 09ada659b..7c11fe834 100644 --- a/src/kubernetes_cluster/proof/validation_rule.rs +++ b/src/kubernetes_cluster/proof/validation_rule.rs @@ -269,8 +269,8 @@ proof fn lemma_always_triggering_cr_is_in_correct_order(spec: TempPred, cr } } init_invariant(spec, Self::init(), next, inv); - always_weaken_temp(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_etcd_and_triggering_cr(cr))); - always_weaken_temp(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr))); + always_weaken(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_etcd_and_triggering_cr(cr))); + always_weaken(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr))); } } diff --git a/src/state_machine/action.rs b/src/state_machine/action.rs index 5d14490a3..edb717bcd 100644 --- a/src/state_machine/action.rs +++ b/src/state_machine/action.rs @@ -46,8 +46,8 @@ impl Action { spec.entails(self.weak_fairness(input)), ensures spec.entails(lift_state(pre).leads_to(lift_state(post))), { - always_implies_preserved_by_always_temp::(spec, lift_state(pre), lift_state(self.pre(input))); - leads_to_weaken_temp::(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre)), lift_action(self.forward(input))); + always_implies_preserved_by_always::(spec, lift_state(pre), lift_state(self.pre(input))); + leads_to_weaken::(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre)), lift_action(self.forward(input))); wf1_variant_temp::(spec, lift_action(next), lift_action(self.forward(input)), lift_state(pre), lift_state(post)); } @@ -62,8 +62,8 @@ impl Action { spec.entails(always(lift_state(c))), ensures spec.entails(lift_state(pre).leads_to(lift_state(post))), { - always_implies_preserved_by_always_temp::(spec, lift_state(pre).and(lift_state(c)), lift_state(self.pre(input))); - leads_to_weaken_temp::(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre).and(lift_state(c))), lift_action(self.forward(input))); + always_implies_preserved_by_always::(spec, lift_state(pre).and(lift_state(c)), lift_state(self.pre(input))); + leads_to_weaken::(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre).and(lift_state(c))), lift_action(self.forward(input))); wf1_variant_borrow_from_spec_temp::(spec, lift_action(next), lift_action(self.forward(input)), lift_state(c), lift_state(pre), lift_state(post)); } } diff --git a/src/temporal_logic/rules.rs b/src/temporal_logic/rules.rs index 5bd773a85..6500b259a 100644 --- a/src/temporal_logic/rules.rs +++ b/src/temporal_logic/rules.rs @@ -540,7 +540,7 @@ pub proof fn always_tla_forall_apply(spec: TempPred, a_to_p: spec_fn(A) requires spec.entails(always(tla_forall(a_to_p))), ensures spec.entails(always(a_to_p(a))), { - implies_preserved_by_always_temp(tla_forall(a_to_p), a_to_p(a)); + entails_preserved_by_always(tla_forall(a_to_p), a_to_p(a)); entails_trans(spec, always(tla_forall(a_to_p)), always(a_to_p(a))); } @@ -734,7 +734,7 @@ proof fn stable_spec_entails_always_p(spec: TempPred, p: TempPred) } } ); - implies_preserved_by_always_temp(spec, p); + entails_preserved_by_always(spec, p); entails_trans(spec, always(spec), always(p)); } @@ -899,7 +899,7 @@ macro_rules! combine_spec_entails_always_n_internal { entails_always_and_n!($spec, $($tail)*); } ); - implies_preserved_by_always_temp(combine_with_next!($($tail)*), $partial_spec); + entails_preserved_by_always(combine_with_next!($($tail)*), $partial_spec); entails_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec)); }; } @@ -935,9 +935,9 @@ macro_rules! invariant_n_internal { entails_always_and_n!($spec, $($tail)*); } ); - implies_preserved_by_always_temp(combine_with_next!($($tail)*), $partial_spec); + entails_preserved_by_always(combine_with_next!($($tail)*), $partial_spec); entails_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec)); - implies_preserved_by_always_temp($partial_spec, $inv); + entails_preserved_by_always($partial_spec, $inv); entails_trans($spec, always($partial_spec), always($inv)); }; } @@ -1297,7 +1297,7 @@ pub proof fn entails_trans(p: TempPred, q: TempPred, r: TempPred) /// If p implies q for all executions, p will leads to q anyway. /// pre: -/// |= p => q +/// p |= q /// post: /// spec |= p ~> q /// Note: there is no constraint on spec, it can be true_pred(). @@ -1311,12 +1311,12 @@ pub proof fn entails_implies_leads_to(spec: TempPred, p: TempPred, q: T /// Introduce always to both sides of implies. /// pre: -/// |= p => q +/// p |= q /// post: -/// |= []p => []q -pub proof fn implies_preserved_by_always_temp(p: TempPred, q: TempPred) - requires valid(p.implies(q)), - ensures valid(always(p).implies(always(q))), +/// []p |= []q +pub proof fn entails_preserved_by_always(p: TempPred, q: TempPred) + requires p.entails(q), + ensures always(p).entails(always(q)), { assert forall |ex| always(p).satisfied_by(ex) implies always(q).satisfied_by(ex) by { assert forall |i:nat| q.satisfied_by(#[trigger] ex.suffix(i)) by { @@ -1332,13 +1332,13 @@ pub proof fn implies_preserved_by_always_temp(p: TempPred, q: TempPred) /// spec |= []p /// post: /// spec |= []q -pub proof fn always_weaken_temp(spec: TempPred, p: TempPred, q: TempPred) +pub proof fn always_weaken(spec: TempPred, p: TempPred, q: TempPred) requires valid(p.implies(q)), spec.entails(always(p)), ensures spec.entails(always(q)), { - implies_preserved_by_always_temp::(p, q); + entails_preserved_by_always::(p, q); assert forall |ex| #[trigger] spec.satisfied_by(ex) implies always(q).satisfied_by(ex) by { implies_apply::(ex, spec, always(p)); implies_apply::(ex, always(p), always(q)); @@ -1350,7 +1350,7 @@ pub proof fn always_weaken_temp(spec: TempPred, p: TempPred, q: TempPre /// spec |= [](p => q) /// post: /// spec |= []([]p => []q) -pub proof fn always_implies_preserved_by_always_temp(spec: TempPred, p: TempPred, q: TempPred) +pub proof fn always_implies_preserved_by_always(spec: TempPred, p: TempPred, q: TempPred) requires spec.entails(always(p.implies(q))), ensures spec.entails(always(always(p).implies(always(q)))), { @@ -1369,6 +1369,13 @@ pub proof fn always_implies_preserved_by_always_temp(spec: TempPred, p: Te }; } +/// Enhance the conclusion of leads to always using invariant. +/// pre: +/// spec |= []inv +/// spec |= p ~> []q1 +/// q1 /\ inv |= q2 +/// post: +/// spec |= p ~> []q2 pub proof fn leads_to_always_enhance(spec: TempPred, inv: TempPred, p: TempPred, q1: TempPred, q2: TempPred) requires spec.entails(always(inv)), @@ -1399,7 +1406,7 @@ pub proof fn leads_to_always_enhance(spec: TempPred, inv: TempPred, p: /// spec |= p ~> q /// post: /// spec |= <>q -pub proof fn leads_to_apply_temp(spec: TempPred, p: TempPred, q: TempPred) +pub proof fn leads_to_apply(spec: TempPred, p: TempPred, q: TempPred) requires spec.entails(p), spec.entails(p.leads_to(q)), @@ -1420,7 +1427,7 @@ pub proof fn leads_to_apply_temp(spec: TempPred, p: TempPred, q: TempPr /// spec |= q ~> r /// post: /// spec |= p ~> r -pub proof fn leads_to_trans_temp(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) +pub proof fn leads_to_trans(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(q)), spec.entails(q.leads_to(r)), @@ -1457,10 +1464,10 @@ macro_rules! leads_to_trans_n { #[macro_export] macro_rules! leads_to_trans_n_internal { ($spec:expr, $p1:expr, $p2:expr, $p3:expr) => { - leads_to_trans_temp($spec, $p1, $p2, $p3); + leads_to_trans($spec, $p1, $p2, $p3); }; ($spec:expr, $p1:expr, $p2:expr, $p3:expr, $($tail:tt)*) => { - leads_to_trans_temp($spec, $p1, $p2, $p3); + leads_to_trans($spec, $p1, $p2, $p3); leads_to_trans_n_internal!($spec, $p1, $p3, $($tail)*); }; } @@ -1475,7 +1482,7 @@ pub use leads_to_trans_n_internal; /// spec |= p1 ~> q1 /// post: /// spec |= p2 ~> q2 -pub proof fn leads_to_weaken_temp(spec: TempPred, p1: TempPred, q1: TempPred, p2: TempPred, q2: TempPred) +pub proof fn leads_to_weaken(spec: TempPred, p1: TempPred, q1: TempPred, p2: TempPred, q2: TempPred) requires spec.entails(always(p2.implies(p1))), spec.entails(always(q1.implies(q2))), @@ -1484,8 +1491,8 @@ pub proof fn leads_to_weaken_temp(spec: TempPred, p1: TempPred, q1: Tem { always_implies_to_leads_to::(spec, p2, p1); always_implies_to_leads_to::(spec, q1, q2); - leads_to_trans_temp::(spec, p2, p1, q1); - leads_to_trans_temp::(spec, p2, q1, q2); + leads_to_trans::(spec, p2, p1, q1); + leads_to_trans::(spec, p2, q1, q2); } /// Combine the premises of two leads_to using or. @@ -1494,7 +1501,7 @@ pub proof fn leads_to_weaken_temp(spec: TempPred, p1: TempPred, q1: Tem /// spec |= q ~> r /// post: /// spec |= (p \/ q) ~> r -pub proof fn or_leads_to_combine_temp(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) +pub proof fn or_leads_to_combine(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(r)), spec.entails(q.leads_to(r)), @@ -1530,10 +1537,10 @@ macro_rules! or_leads_to_combine_n { #[macro_export] macro_rules! or_leads_to_combine_n_internal { ($spec:expr, $p1:expr, $p2:expr; $q:expr) => { - or_leads_to_combine_temp($spec, $p1, $p2, $q); + or_leads_to_combine($spec, $p1, $p2, $q); }; ($spec:expr, $p1:expr, $p2:expr, $($rest:expr),+; $q:expr) => { - or_leads_to_combine_temp($spec, $p1, $p2, $q); + or_leads_to_combine($spec, $p1, $p2, $q); or_leads_to_combine_n_internal!($spec, $p1.or($p2), $($rest),+; $q); }; } @@ -1576,10 +1583,10 @@ macro_rules! leads_to_always_combine_n { #[macro_export] macro_rules! leads_to_always_combine_n_internal { ($spec:expr, $p:expr, $q1:expr, $q2:expr) => { - leads_to_always_combine_temp($spec, $p, $q1, $q2); + leads_to_always_combine($spec, $p, $q1, $q2); }; ($spec:expr, $p:expr, $q1:expr, $q2:expr, $($tail:tt)*) => { - leads_to_always_combine_temp($spec, $p, $q1, $q2); + leads_to_always_combine($spec, $p, $q1, $q2); always_and_equality($q1, $q2); leads_to_always_combine_n_internal!($spec, $p, $q1.and($q2), $($tail)*); }; @@ -1677,7 +1684,7 @@ pub proof fn leads_to_always_tla_forall(spec: TempPred, p: TempPred, /// spec |= p ~> []r /// post: /// spec |= p ~> [](q /\ r) -pub proof fn leads_to_always_combine_temp(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) +pub proof fn leads_to_always_combine(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(always(q))), spec.entails(p.leads_to(always(r))), @@ -1710,14 +1717,14 @@ pub proof fn leads_to_always_combine_temp(spec: TempPred, p: TempPred, always_and_equality(q, r); } -/// Get leads_to always. +/// Prove p leads_to always q by showing that q is preserved. /// pre: /// spec |= [](q /\ next => q') /// spec |= []next /// spec |= p ~> q /// post: /// spec |= p ~> []q -pub proof fn leads_to_stable_temp(spec: TempPred, next: TempPred, p: TempPred, q: TempPred) +pub proof fn leads_to_stable(spec: TempPred, next: TempPred, p: TempPred, q: TempPred) requires spec.entails(always(q.and(next).implies(later(q)))), spec.entails(always(next)), @@ -1759,7 +1766,7 @@ pub proof fn leads_to_stable_temp(spec: TempPred, next: TempPred, p: Te /// spec |= p ~> q /// post: /// spec |= p \/ r ~> q \/ r -pub proof fn sandwich_leads_to_by_or_temp(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) +pub proof fn leads_to_framed_by_or(spec: TempPred, p: TempPred, q: TempPred, r: TempPred) requires spec.entails(p.leads_to(q)), ensures spec.entails(p.or(r).leads_to(q.or(r))), { @@ -1792,9 +1799,9 @@ pub proof fn leads_to_shortcut_temp(spec: TempPred, p: TempPred, q: Tem spec.entails(q.leads_to(r.or(s))), ensures spec.entails(p.leads_to(r.or(s))), { - sandwich_leads_to_by_or_temp(spec, q, r.or(s), s); + leads_to_framed_by_or(spec, q, r.or(s), s); temp_pred_equality(r.or(s).or(s), r.or(s)); - leads_to_trans_temp(spec, p, q.or(s), r.or(s)); + leads_to_trans(spec, p, q.or(s), r.or(s)); } /// Concluding p(n) ~> p(0) using ranking functions, with a step of one. diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs index 4632f1137..6ce1432ca 100644 --- a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs +++ b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs @@ -306,7 +306,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state(self, spec: TempPred< self.lemma_from_in_flight_resp_matches_pending_req_at_some_state_to_next_state(spec, controller_id, cr, current_state, next_state); self.lemma_from_pending_req_in_flight_at_some_state_to_next_state(spec, controller_id, cr, current_state, next_state); - or_leads_to_combine_temp(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), next_state))); + or_leads_to_combine(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), next_state))); temp_pred_equality(lift_state(req_in_flight).or(lift_state(resp_in_flight)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)); leads_to_trans_n!( spec, diff --git a/src/v2/kubernetes_cluster/proof/failures_liveness.rs b/src/v2/kubernetes_cluster/proof/failures_liveness.rs index f8d76370f..2a2e846ad 100644 --- a/src/v2/kubernetes_cluster/proof/failures_liveness.rs +++ b/src/v2/kubernetes_cluster/proof/failures_liveness.rs @@ -33,7 +33,7 @@ pub proof fn lemma_true_leads_to_crash_always_disabled(self, spec: TempPred StatePred { @@ -48,7 +48,7 @@ pub proof fn lemma_true_leads_to_req_drop_always_disabled(self, spec: TempPred(spec, lift_state(Self::every_in_flight_msg_has_no_replicas_and_has_unique_id()), lift_state(Self::every_in_flight_msg_has_unique_id())); + always_weaken::(spec, lift_state(Self::every_in_flight_msg_has_no_replicas_and_has_unique_id()), lift_state(Self::every_in_flight_msg_has_unique_id())); } } diff --git a/src/v2/kubernetes_cluster/proof/network_liveness.rs b/src/v2/kubernetes_cluster/proof/network_liveness.rs index 0f2566c4c..1d1d4b5a2 100644 --- a/src/v2/kubernetes_cluster/proof/network_liveness.rs +++ b/src/v2/kubernetes_cluster/proof/network_liveness.rs @@ -177,7 +177,7 @@ pub proof fn lemma_some_rpc_id_leads_to_always_every_in_flight_req_msg_satisfies self.lemma_true_leads_to_always_no_req_before_rpc_id_is_in_flight(spec_with_rpc_id, rpc_id); - implies_preserved_by_always_temp( + entails_preserved_by_always( lift_state(invariant), lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)) .implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) @@ -186,8 +186,8 @@ pub proof fn lemma_some_rpc_id_leads_to_always_every_in_flight_req_msg_satisfies spec_with_rpc_id, always(lift_state(invariant)), always(lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)).implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))) ); - always_implies_preserved_by_always_temp(spec_with_rpc_id, lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements))); - leads_to_weaken_temp( + always_implies_preserved_by_always(spec_with_rpc_id, lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements))); + leads_to_weaken( spec_with_rpc_id, true_pred(), always(lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id))), true_pred(), always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))) @@ -231,7 +231,7 @@ pub proof fn lemma_true_leads_to_always_no_req_before_rpc_id_is_in_flight(self, } } - leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id))); + leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id))); } pub proof fn lemma_eventually_no_req_before_rpc_id_is_in_flight(self, spec: TempPred, rpc_id: RPCId) @@ -343,7 +343,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(self, s self.lemma_pending_requests_number_is_n_leads_to_no_pending_requests( spec, rpc_id, (msg_num - 1) as nat ); - leads_to_trans_temp( + leads_to_trans( spec, pending_requests_num_is_msg_num, pending_requests_num_is_msg_num_minus_1, no_more_pending_requests ); } diff --git a/src/v2/kubernetes_cluster/proof/objects_in_store.rs b/src/v2/kubernetes_cluster/proof/objects_in_store.rs index 5f32af86f..27c32fde6 100644 --- a/src/v2/kubernetes_cluster/proof/objects_in_store.rs +++ b/src/v2/kubernetes_cluster/proof/objects_in_store.rs @@ -238,7 +238,7 @@ pub proof fn lemma_always_each_object_in_etcd_is_well_formed(spec, lift_state(p), lift_state(invariant)); + always_weaken::(spec, lift_state(p), lift_state(invariant)); } } From 0f6fe73db301190f792565fb8576970ae875fe68 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Tue, 17 Sep 2024 14:00:40 -0500 Subject: [PATCH 4/4] cut Signed-off-by: Xudong Sun --- .../fluentbit/proof/liveness/proof.rs | 18 ++- .../fluentbit_config/proof/liveness/proof.rs | 18 ++- .../proof/liveness/proof.rs | 18 ++- .../proof/liveness/proof.rs | 18 ++- .../proof/liveness/proof.rs | 18 ++- .../controller_runtime_eventual_safety.rs | 47 ++++++-- .../proof/controller_runtime_liveness.rs | 18 --- src/state_machine/action.rs | 16 --- src/temporal_logic/rules.rs | 103 ++++++------------ 9 files changed, 156 insertions(+), 118 deletions(-) diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs index f427ff9d2..79af0a735 100644 --- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs @@ -207,7 +207,23 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, fb: F &&& s.scheduled_reconciles().contains_key(fb.object_ref()) }; let input = fb.object_ref(); - FBCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCluster::next(), desired_state_is(fb), pre, post); + let stronger_pre = |s| { + &&& pre(s) + &&& desired_state_is(fb)(s) + }; + let stronger_next = |s, s_prime| { + &&& FBCluster::next()(s, s_prime) + &&& desired_state_is(fb)(s_prime) + }; + always_to_always_later(spec, lift_state(desired_state_is(fb))); + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(FBCluster::next()), + later(lift_state(desired_state_is(fb))) + ); + FBCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post); + temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(fb))), lift_state(stronger_pre)); + leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(fb))); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCluster| {!s.ongoing_reconciles().contains_key(fb.object_ref())})); diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs index 16fc87a81..e65ec0f99 100644 --- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs +++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs @@ -147,7 +147,23 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, fbc: &&& s.scheduled_reconciles().contains_key(fbc.object_ref()) }; let input = fbc.object_ref(); - FBCCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCCluster::next(), desired_state_is(fbc), pre, post); + let stronger_pre = |s| { + &&& pre(s) + &&& desired_state_is(fbc)(s) + }; + let stronger_next = |s, s_prime| { + &&& FBCCluster::next()(s, s_prime) + &&& desired_state_is(fbc)(s_prime) + }; + always_to_always_later(spec, lift_state(desired_state_is(fbc))); + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(FBCCluster::next()), + later(lift_state(desired_state_is(fbc))) + ); + FBCCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post); + temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(fbc))), lift_state(stronger_pre)); + leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(fbc))); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCCluster| {!s.ongoing_reconciles().contains_key(fbc.object_ref())})); diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs index 64e18e6e3..39acf2d36 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs @@ -302,7 +302,23 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, rabb &&& s.scheduled_reconciles().contains_key(rabbitmq.object_ref()) }; let input = rabbitmq.object_ref(); - RMQCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, RMQCluster::next(), RMQCluster::desired_state_is(rabbitmq), pre, post); + let stronger_pre = |s| { + &&& pre(s) + &&& desired_state_is(rabbitmq)(s) + }; + let stronger_next = |s, s_prime| { + &&& RMQCluster::next()(s, s_prime) + &&& desired_state_is(rabbitmq)(s_prime) + }; + always_to_always_later(spec, lift_state(desired_state_is(rabbitmq))); + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(RMQCluster::next()), + later(lift_state(desired_state_is(rabbitmq))) + ); + RMQCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post); + temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(rabbitmq))), lift_state(stronger_pre)); + leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(rabbitmq))); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: RMQCluster| {!s.ongoing_reconciles().contains_key(rabbitmq.object_ref())})); diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs index 39b23fcbf..21f27a5cb 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs @@ -168,7 +168,23 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, vrs: &&& s.scheduled_reconciles().contains_key(vrs.object_ref()) }; let input = vrs.object_ref(); - VRSCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, VRSCluster::next(), VRSCluster::desired_state_is(vrs), pre, post); + let stronger_pre = |s| { + &&& pre(s) + &&& desired_state_is(vrs)(s) + }; + let stronger_next = |s, s_prime| { + &&& VRSCluster::next()(s, s_prime) + &&& desired_state_is(vrs)(s_prime) + }; + always_to_always_later(spec, lift_state(desired_state_is(vrs))); + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(VRSCluster::next()), + later(lift_state(desired_state_is(vrs))) + ); + VRSCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post); + temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(vrs))), lift_state(stronger_pre)); + leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(vrs))); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: VRSCluster| {!s.ongoing_reconciles().contains_key(vrs.object_ref())})); diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs index 81489ffdd..a47214055 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs @@ -294,7 +294,23 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred, zooke &&& s.scheduled_reconciles().contains_key(zookeeper.object_ref()) }; let input = zookeeper.object_ref(); - ZKCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, ZKCluster::next(), ZKCluster::desired_state_is(zookeeper), pre, post); + let stronger_pre = |s| { + &&& pre(s) + &&& desired_state_is(zookeeper)(s) + }; + let stronger_next = |s, s_prime| { + &&& ZKCluster::next()(s, s_prime) + &&& desired_state_is(zookeeper)(s_prime) + }; + always_to_always_later(spec, lift_state(desired_state_is(zookeeper))); + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(ZKCluster::next()), + later(lift_state(desired_state_is(zookeeper))) + ); + ZKCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post); + temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(zookeeper))), lift_state(stronger_pre)); + leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(zookeeper))); entails_implies_leads_to(spec, lift_state(post), lift_state(post)); or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post)); temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: ZKCluster| {!s.ongoing_reconciles().contains_key(zookeeper.object_ref())})); diff --git a/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs b/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs index 12411ea75..a66c739df 100644 --- a/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs +++ b/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs @@ -39,16 +39,27 @@ pub proof fn lemma_true_leads_to_always_the_object_in_schedule_has_spec_and_uid_ let pre = |s: Self| true; let post = Self::the_object_in_schedule_has_spec_and_uid_as(cr); let input = cr.object_ref(); - let stronger_next = |s, s_prime: Self| { - &&& Self::next()(s, s_prime) - &&& Self::desired_state_is(cr)(s) - }; - combine_spec_entails_always_n!(spec, lift_action(stronger_next), lift_action(Self::next()), lift_state(Self::desired_state_is(cr))); K::object_ref_is_well_formed(); - Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec( - spec, input, stronger_next, Self::desired_state_is(cr), pre, post + + let stronger_pre = |s| { + &&& pre(s) + &&& Self::desired_state_is(cr)(s) + }; + let stronger_next = |s, s_prime| { + &&& Self::next()(s, s_prime) + &&& Self::desired_state_is(cr)(s_prime) + }; + always_to_always_later(spec, lift_state(Self::desired_state_is(cr))); + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(Self::next()), + later(lift_state(Self::desired_state_is(cr))) ); + Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post); + temp_pred_equality(lift_state(pre).and(lift_state(Self::desired_state_is(cr))), lift_state(stronger_pre)); + leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(Self::desired_state_is(cr))); + leads_to_stable(spec, lift_action(stronger_next), lift_state(pre), lift_state(post)); } @@ -91,9 +102,27 @@ pub proof fn lemma_true_leads_to_always_the_object_in_reconcile_has_spec_and_uid { let input = cr.object_ref(); K::object_ref_is_well_formed(); - Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec( - spec, input, stronger_next, Self::desired_state_is(cr), not_scheduled_or_reconcile, scheduled_and_not_reconcile + + let pre = not_scheduled_or_reconcile; + let post = scheduled_and_not_reconcile; + let stronger_pre = |s| { + &&& pre(s) + &&& Self::desired_state_is(cr)(s) + }; + let even_stronger_next = |s, s_prime| { + &&& stronger_next(s, s_prime) + &&& Self::desired_state_is(cr)(s_prime) + }; + always_to_always_later(spec, lift_state(Self::desired_state_is(cr))); + combine_spec_entails_always_n!( + spec, lift_action(even_stronger_next), + lift_action(stronger_next), + later(lift_state(Self::desired_state_is(cr))) ); + Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, even_stronger_next, stronger_pre, post); + temp_pred_equality(lift_state(pre).and(lift_state(Self::desired_state_is(cr))), lift_state(stronger_pre)); + leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(Self::desired_state_is(cr))); + } ); assert_by( diff --git a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs index f2aedfef3..b06d60c8b 100644 --- a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs +++ b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs @@ -63,24 +63,6 @@ pub proof fn lemma_pre_leads_to_post_by_schedule_controller_reconcile( Self::schedule_controller_reconcile().wf1(input, spec, next, pre, post); } -pub proof fn lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec( - spec: TempPred, input: ObjectRef, next: ActionPred, c: StatePred, pre: StatePred, post: StatePred -) - requires - forall |s, s_prime: Self| pre(s) && c(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime), - forall |s, s_prime: Self| pre(s) && c(s) && #[trigger] next(s, s_prime) && Self::schedule_controller_reconcile().forward(input)(s, s_prime) ==> post(s_prime), - forall |s: Self| #[trigger] pre(s) && c(s) ==> Self::schedule_controller_reconcile().pre(input)(s), - spec.entails(always(lift_action(next))), - spec.entails(tla_forall(|i| Self::schedule_controller_reconcile().weak_fairness(i))), - spec.entails(always(lift_state(c))), - ensures spec.entails(lift_state(pre).leads_to(lift_state(post))), -{ - use_tla_forall::( - spec, |i| Self::schedule_controller_reconcile().weak_fairness(i), input - ); - Self::schedule_controller_reconcile().wf1_borrow_from_spec(input, spec, next, c, pre, post); -} - pub proof fn lemma_reconcile_done_leads_to_reconcile_idle(spec: TempPred, cr_key: ObjectRef) requires K::kind().is_CustomResourceKind(), diff --git a/src/state_machine/action.rs b/src/state_machine/action.rs index edb717bcd..1a67b380d 100644 --- a/src/state_machine/action.rs +++ b/src/state_machine/action.rs @@ -50,22 +50,6 @@ impl Action { leads_to_weaken::(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre)), lift_action(self.forward(input))); wf1_variant_temp::(spec, lift_action(next), lift_action(self.forward(input)), lift_state(pre), lift_state(post)); } - - /// `wf1_borrow_from_spec` is a specialized version of temporal_logic_rules::wf1 for Action - pub proof fn wf1_borrow_from_spec(self, input: Input, spec: TempPred, next: ActionPred, c: StatePred, pre: StatePred, post: StatePred) - requires - forall |s, s_prime: State| pre(s) && c(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime), - forall |s, s_prime: State| pre(s) && c(s) && #[trigger] next(s, s_prime) && self.forward(input)(s, s_prime) ==> post(s_prime), - spec.entails(always(lift_action(next))), - spec.entails(always((lift_state(pre).and(lift_state(c))).implies(lift_state(self.pre(input))))), - spec.entails(self.weak_fairness(input)), - spec.entails(always(lift_state(c))), - ensures spec.entails(lift_state(pre).leads_to(lift_state(post))), - { - always_implies_preserved_by_always::(spec, lift_state(pre).and(lift_state(c)), lift_state(self.pre(input))); - leads_to_weaken::(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre).and(lift_state(c))), lift_action(self.forward(input))); - wf1_variant_borrow_from_spec_temp::(spec, lift_action(next), lift_action(self.forward(input)), lift_state(c), lift_state(pre), lift_state(post)); - } } #[is_variant] diff --git a/src/temporal_logic/rules.rs b/src/temporal_logic/rules.rs index 6500b259a..26eb160b2 100644 --- a/src/temporal_logic/rules.rs +++ b/src/temporal_logic/rules.rs @@ -654,7 +654,7 @@ pub proof fn spec_entails_tla_forall(spec: TempPred, a_to_p: spec_fn(A) }; } -proof fn always_implies_forall_intro(spec: TempPred, p: TempPred, a_to_q: spec_fn(A) -> TempPred) +pub proof fn always_implies_forall_intro(spec: TempPred, p: TempPred, a_to_q: spec_fn(A) -> TempPred) requires forall |a: A| #[trigger] spec.entails(always(p.implies(a_to_q(a)))), ensures spec.entails(always(p.implies(tla_forall(a_to_q)))), { @@ -718,26 +718,6 @@ pub proof fn eliminate_always(spec: TempPred, p: TempPred) } } -proof fn stable_spec_entails_always_p(spec: TempPred, p: TempPred) - requires - valid(stable(spec)), - spec.entails(p), - ensures spec.entails(always(p)), -{ - assert_by( - spec.entails(always(spec)), - { - assert forall |ex| #[trigger] spec.implies(always(spec)).satisfied_by(ex) by { - assert(valid(stable(spec))); - assert(stable(spec).satisfied_by(ex)); - stable_unfold::(ex, spec); - } - } - ); - entails_preserved_by_always(spec, p); - entails_trans(spec, always(spec), always(p)); -} - /// Entails p and q if entails each of them. /// pre: /// spec |= p @@ -1082,21 +1062,6 @@ pub proof fn unpack_conditions_from_spec(spec: TempPred, c: TempPred, p }; } -proof fn borrow_conditions_from_spec(spec: TempPred, c: TempPred, p: TempPred, q: TempPred) - requires - spec.entails(p.and(c).leads_to(q)), - spec.entails(always(c)), - ensures spec.entails(p.leads_to(q)), -{ - assert forall |ex| #[trigger] spec.satisfied_by(ex) implies p.leads_to(q).satisfied_by(ex) by { - assert forall |i| #[trigger] p.satisfied_by(ex.suffix(i)) implies eventually(q).satisfied_by(ex.suffix(i)) by { - implies_apply(ex, spec, always(c)); - implies_apply(ex, spec, p.and(c).leads_to(q)); - implies_apply(ex.suffix(i), p.and(c), eventually(q)); - } - } -} - /// Pack the conditions from the right to the left side of |= /// pre: /// spec |= p /\ c ~> q @@ -1119,15 +1084,19 @@ proof fn pack_conditions_to_spec(spec: TempPred, c: TempPred, p: TempPr /// This lemma is used to make the predicate as concise as possible. /// Similar to the first-order logic where p equals p /\ q when p -> q is satisfied, /// we can reduce the size of predicate when some part of it implies the rest. -pub proof fn simplify_predicate(simpler: TempPred, redundant: TempPred) - requires simpler.entails(redundant), - ensures simpler == simpler.and(redundant), +/// pre: +/// p |= q +/// post: +/// p == p /\ q +pub proof fn simplify_predicate(p: TempPred, q: TempPred) + requires p.entails(q), + ensures p == p.and(q), { - assert forall |ex| #[trigger] simpler.satisfied_by(ex) implies simpler.and(redundant).satisfied_by(ex) by { - entails_and_temp::(simpler, simpler, redundant); - entails_apply::(ex, simpler, simpler.and(redundant)); + assert forall |ex| #[trigger] p.satisfied_by(ex) implies p.and(q).satisfied_by(ex) by { + entails_and_temp::(p, p, q); + entails_apply::(ex, p, p.and(q)); }; - temp_pred_equality::(simpler, simpler.and(redundant)); + temp_pred_equality::(p, p.and(q)); } /// Prove safety by induction. @@ -1218,33 +1187,6 @@ pub proof fn wf1_variant_temp(spec: TempPred, next: TempPred, forward: } } -pub proof fn wf1_variant_borrow_from_spec_temp(spec: TempPred, next: TempPred, forward: TempPred, c: TempPred, p: TempPred, q: TempPred) - requires - spec.entails(always(p.and(c).and(next).implies(later(p).or(later(q))))), - spec.entails(always(p.and(c).and(next).and(forward).implies(later(q)))), - spec.entails(always(next)), - spec.entails(always(p.and(c)).leads_to(forward)), - spec.entails(always(c)), - ensures spec.entails(p.leads_to(q)), -{ - assert forall |ex| #[trigger] spec.satisfied_by(ex) - implies always(p.and(c).and(next).implies(later(p.and(c)).or(later(q)))).satisfied_by(ex) by { - implies_apply::(ex, spec, always(p.and(c).and(next).implies(later(p).or(later(q))))); - implies_apply::(ex, spec, always(c)); - always_unfold(ex, p.and(c).and(next).implies(later(p).or(later(q)))); - always_unfold(ex, c); - assert forall |i| #[trigger] p.and(c).and(next).satisfied_by(ex.suffix(i)) - implies later(p.and(c)).or(later(q)).satisfied_by(ex.suffix(i)) by { - implies_apply(ex.suffix(i), p.and(c).and(next), later(p).or(later(q))); - execution_equality(ex.suffix(i).suffix(1), ex.suffix(i + 1)); - temp_pred_equality(later(p.and(c)), later(p).and(later(c))); - } - } - - wf1_variant_temp(spec, next, forward, p.and(c), q); - borrow_conditions_from_spec(spec, c, p, q); -} - /// Get the initial leads_to with a stronger wf assumption than wf1_variant. /// pre: /// |= p /\ next => p' \/ q' @@ -1901,4 +1843,25 @@ pub proof fn vacuous_leads_to(spec: TempPred, p: TempPred, q: TempPred< } } +/// Proving p leads to q by borrowing the inv. +/// pre: +/// spec |= p /\ inv ~> q +/// spec |= []inv +/// post: +/// spec |= p ~> q +pub proof fn leads_to_by_borrowing_inv(spec: TempPred, p: TempPred, q: TempPred, inv: TempPred) + requires + spec.entails(p.and(inv).leads_to(q)), + spec.entails(always(inv)), + ensures + spec.entails(p.leads_to(q)), +{ + assert forall |ex| #[trigger] spec.satisfied_by(ex) implies p.leads_to(q).satisfied_by(ex) by { + assert forall |i| #[trigger] p.satisfied_by(ex.suffix(i)) implies eventually(q).satisfied_by(ex.suffix(i)) by { + instantiate_entailed_always(ex, i, spec, inv); + instantiate_entailed_leads_to(ex, i, spec, p.and(inv), q); + } + } +} + }