Action Plan (Jan 16 - Jan 23)

[codyjrivera]

• Finish non-trivial invariant proofs (Jan 17)
• Adapt pre-existing proof skeleton in the V2 state machine (Jan 21)

[Catoverflow]

• Prove DS lemmas in src/vstd_ext
• Prove lemma_filtered_pods_set_equals_matching_pods

[codyjrivera]

Cluster lemmas (don't require knowledge of VReplicaSet):

(DONE) cr_objects_in_schedule_satisfy_state_validation (Cody, possibly Cathy for one if this is easy)
(DONE) cr_objects_in_reconcile_satisfy_state_validation
each_object_in_etcd_has_at_most_one_controller_owner (Cathy)

VRS invariants:

(DONE) every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter (Cody)
each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs (harder) (Cody)
at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries (harder) (Cody)

Random lemmas:

lemma_filtered_pods_set_equals_matching_pods (Cathy)