support for deletion timestamp added, tests failed

[Catoverflow]

This PR implemented the model & executable part for
https://github.com/kubernetes/kubernetes/blob/master/pkg/controller/replicaset/replica_set.go#L721-L723

Test is still broken, working on fixing that

[marshtompsxd]

Can you move it to the Init step? If the VReplicaSet has deletion timestamp, then there is no need to list the pods whatsoever.

[Catoverflow]

The problem is I cannot align well the code block in k8s controller with the step in anvil. Take the line of code I want to model as an example, I'm not sure if we filter out the entire func (rsc *ReplicaSetController) syncReplicaSet(ctx context.Context, key string) where should I put the corresponding timestamp checking logic in anvil's model. In other words, I don't know if k8s itself put this part in init or afterlistpod step.

Do you have any suggestion?

[marshtompsxd]

So the conformance proof passes but the liveness proof breaks, right?

[tianyin]

@Catoverflow could you write some brief descriptions when you open PRs?

[Catoverflow]

So the conformance proof passes but the liveness proof breaks, right?

Yes, 2 failed tests are

error: assertion failed
   --> v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs:573:87
    |
573 |     assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by {
    |                                                                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ assertion failed

note: function body check: not all errors may have been reported; rerun with a higher value for --multiple-errors to find other potential errors in this function
   --> v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs:460:1
    |
460 | / pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req(
461 | |     vrs: VReplicaSetView, spec: TempPred<ClusterState>, cluster: Cluster, controller_id: int,
462 | |     resp_msg: Message, diff: int
463 | | )
    | |_^

error: assertion failed
    --> v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs:1071:87
     |
1071 |     assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by {
     |                                                                               

I'm trying to find a way to expand the pre and post wrappers to find the specific clauses

[Catoverflow]

@Catoverflow could you write some brief descriptions when you open PRs?

added

[marshtompsxd]

@Catoverflow You might need to revise the premise of the ESR property to focus on reasoning about VReplicaSet that has no deletion timestamp. You can work with @codyjrivera on that.