Simplify TLA lib

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<Seq<OwnerReferenceView>>| {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,11 +1008,11 @@ 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))
     );
-    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)))

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<F
         object_in_every_update_request_msg_satisfies_unchangeable_induction(sub_resource, fb, s, s_prime);
     }
     init_invariant(spec, FBCluster::init(), next, inv);
-    always_weaken_temp(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, fb)));
+    always_weaken(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, fb)));
 }
 
 pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubResource, fb: FluentBitView, s: FBCluster, s_prime: FBCluster)

src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs

@@ -58,7 +58,7 @@ pub proof fn lemma_from_after_get_daemon_set_step_to_daemon_set_matches(spec: Te
         &&& s.resources().contains_key(get_request(SubResource::DaemonSet, fb).key)
         &&& pending_req_in_flight_at_after_get_resource_step(SubResource::DaemonSet, fb)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::DaemonSet, fb))
     );
@@ -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)), {
@@ -177,7 +177,7 @@ proof fn lemma_from_after_get_daemon_set_step_and_key_exists_to_daemon_set_match
         leads_to_trans_n!(spec, daemon_set_not_matches, post1, post2, post);
     });
 
-    or_leads_to_combine_temp(spec, daemon_set_matches, daemon_set_not_matches, post);
+    or_leads_to_combine(spec, daemon_set_matches, daemon_set_not_matches, post);
     temp_pred_equality(daemon_set_matches.or(daemon_set_not_matches), pre);
 }
 
@@ -402,7 +402,7 @@ proof fn lemma_daemon_set_state_matches_at_after_update_daemon_set_step(spec: Te
         &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::DaemonSet, fb)(s)
         &&& helper_invariants::daemon_set_in_etcd_satisfies_unchangeable(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),
         lift_action(FBCluster::next()),
@@ -483,7 +483,7 @@ pub proof fn lemma_daemon_set_is_stable(spec: TempPred<FBCluster>, 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));
 }
 
 }

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::<FluentBitMaker>(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::<FluentBitMaker>(fb))))
     );
@@ -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::<FluentBitMaker>(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::<FluentBitMaker>(fb))));
+    leads_to_trans(spec_before_phase_n(i, fb), true_pred(), invariants_since_phase_n(i, fb), always(lift_state(current_state_matches::<FluentBitMaker>(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))
             );
@@ -207,9 +207,25 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred<FBCluster>, 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);
-    valid_implies_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));
+    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())}));
 }
 

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)));
     }
 }
 
@@ -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));
         });
     }
@@ -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<FBCluster>, 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));
 }
 
 }

src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs

@@ -75,8 +75,8 @@ 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_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);
         FBCluster::lemma_true_leads_to_busy_always_disabled(spec);

src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs

@@ -56,7 +56,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<FBCluster>, 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);

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<Seq<OwnerReferenceView>>| {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)