Rename lower_rv => smaller_rv

Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Aug 26, 2023 · 3363833 · 3363833
1 parent 922ae12
commit 3363833
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs
@@ -136,20 +136,20 @@ proof fn lemma_always_object_in_sts_update_request_has_smaller_rv_than_etcd(
         &&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime)
         &&& response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)(s)
         &&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
-        &&& RMQCluster::object_in_ok_get_response_has_lower_rv_than_etcd(sts_key)(s)
+        &&& RMQCluster::object_in_ok_get_response_has_smaller_rv_than_etcd(sts_key)(s)
     };
     RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
     lemma_always_response_at_after_get_stateful_set_step_is_sts_get_response(spec, rabbitmq);
     always_to_always_later(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()));
     RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
-    RMQCluster::lemma_always_object_in_ok_get_response_has_lower_rv_than_etcd(spec, sts_key);
+    RMQCluster::lemma_always_object_in_ok_get_response_has_smaller_rv_than_etcd(spec, sts_key);
     combine_spec_entails_always_n!(
         spec, lift_action(next), lift_action(RMQCluster::next()),
         lift_state(RMQCluster::each_object_in_etcd_is_well_formed()),
         later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed())),
         lift_state(response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)),
         lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
-        lift_state(RMQCluster::object_in_ok_get_response_has_lower_rv_than_etcd(sts_key))
+        lift_state(RMQCluster::object_in_ok_get_response_has_smaller_rv_than_etcd(sts_key))
     );
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         let etcd_rv = s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0();

diff --git a/src/kubernetes_cluster/proof/message.rs b/src/kubernetes_cluster/proof/message.rs
@@ -354,7 +354,7 @@ pub open spec fn ok_get_response_msg(key: ObjectRef) -> FnSpec(MsgType<E>) -> bo
         && msg.content.get_get_response().res.get_Ok_0().object_ref() == key
 }
 
-pub open spec fn object_in_ok_get_response_has_lower_rv_than_etcd(key: ObjectRef) -> StatePred<Self> {
+pub open spec fn object_in_ok_get_response_has_smaller_rv_than_etcd(key: ObjectRef) -> StatePred<Self> {
     |s: Self| {
         let etcd_rv = s.resource_obj_of(key).metadata.resource_version.get_Some_0();
         forall |msg: MsgType<E>|
@@ -365,14 +365,14 @@ pub open spec fn object_in_ok_get_response_has_lower_rv_than_etcd(key: ObjectRef
     }
 }
 
-pub proof fn lemma_always_object_in_ok_get_response_has_lower_rv_than_etcd(spec: TempPred<Self>, key: ObjectRef)
+pub proof fn lemma_always_object_in_ok_get_response_has_smaller_rv_than_etcd(spec: TempPred<Self>, key: ObjectRef)
     requires
         spec.entails(lift_state(Self::init())),
         spec.entails(always(lift_action(Self::next()))),
     ensures
-        spec.entails(always(lift_state(Self::object_in_ok_get_response_has_lower_rv_than_etcd(key)))),
+        spec.entails(always(lift_state(Self::object_in_ok_get_response_has_smaller_rv_than_etcd(key)))),
 {
-    let inv = Self::object_in_ok_get_response_has_lower_rv_than_etcd(key);
+    let inv = Self::object_in_ok_get_response_has_smaller_rv_than_etcd(key);
     let next = |s, s_prime| {
         &&& Self::next()(s, s_prime)
         &&& Self::each_object_in_etcd_is_well_formed()(s)
@@ -430,13 +430,13 @@ pub proof fn lemma_always_object_in_ok_get_resp_is_same_as_etcd_with_same_rv(spe
     let next = |s, s_prime| {
         &&& Self::next()(s, s_prime)
         &&& Self::each_object_in_etcd_is_well_formed()(s)
-        &&& Self::object_in_ok_get_response_has_lower_rv_than_etcd(key)(s)
+        &&& Self::object_in_ok_get_response_has_smaller_rv_than_etcd(key)(s)
     };
     Self::lemma_always_each_object_in_etcd_is_well_formed(spec);
-    Self::lemma_always_object_in_ok_get_response_has_lower_rv_than_etcd(spec, key);
+    Self::lemma_always_object_in_ok_get_response_has_smaller_rv_than_etcd(spec, key);
     combine_spec_entails_always_n!(
         spec, lift_action(next), lift_action(Self::next()), lift_state(Self::each_object_in_etcd_is_well_formed()),
-        lift_state(Self::object_in_ok_get_response_has_lower_rv_than_etcd(key))
+        lift_state(Self::object_in_ok_get_response_has_smaller_rv_than_etcd(key))
     );
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Self::ok_get_response_msg(key)(msg) && s_prime.resource_key_exists(key)