Prove VSTS non-interference lemma

[Catoverflow]

This PR adds and proves VSTS non-interference lemma (lemma_no_interference) with a few assumptions to be proved in following PRs:

• vsts_guarantee
• no_interfering_request_between_vsts

Additional helper lemmas

And 2 helper lemmas needs to be proved in the future:

• generated_name_has_vsts_prefix_implies_generate_name_field_has_vsts_prefix
• vsts_name_non_eq_implies_no_pvc_name_match

Because of Verus' limited support for string they are not easy to prove.

Maybe @NikhilSDate can help on them and 2 assumptions above

These predicates are added and already proved for the shield lemma:

• cluster.no_pending_request_to_api_server_from_non_controllers
• seq_unequal_preserved_by_add_prefix

Change in VSTS rely conditions

Updated a few wrong and missing assimptions there

Change in VSTS spec

• Add requirements that PVC template should not contain - to fix Stricter checking/validation of statefulset pvcs kubernetes/kubernetes#41153

Change in cluster state machine

Cluster API Server state machine is updated to

• make it easier for Verus to learn the change made by UpdateStatus requests and Update requests
• add an additional check on req.owner_ref to make sure it's a controller owner for GetThenUpdate and GetThenDelete requests

Minor changes

• remove no_pending_mutation_request_not_from_controller_on_vrs_objects as it's replaced by cluster.no_pending_request_to_api_server_from_non_controllers
• rename generate_name to be generated_name

[marshtompsxd]

"Shield" is just a nickname. We should call it the non-interference lemma (you don't need to rename the file or lemma).

[Catoverflow]

We should call it the non-interference lemma (you don't need to rename the file or lemma).

Good catch, though I want a cooler name for it :3