Prove VReplicaSet WF1 Lemmas for Create Path #571
Conversation
Signed-off-by: Cody Rivera <[email protected]>
Signed-off-by: Cody Rivera <[email protected]>
Signed-off-by: Cody Rivera <[email protected]>
Signed-off-by: Cody Rivera <[email protected]>
Signed-off-by: Cody Rivera <[email protected]>
codyjrivera
changed the title
src/vstd_ext/seq_lib.rs
Outdated
| requires forall |e: A| #![auto] s.contains(e) ==> !pred(e), | ||
| ensures s.filter(pred).len() == 0; | ||
| pub proof fn seq_pred_false_on_all_elements_is_equivalent_to_empty_filter<A>(s: Seq<A>, pred: spec_fn(A) -> bool) | ||
| ensures (forall |e: A| #![auto] s.contains(e) ==> !pred(e)) <==> s.filter(pred).len() == 0; |
There was a problem hiding this comment.
nit: let's set a trigger instead of using auto, which makes it even harder to predict the behavior of the solver
| // TODO: Prove this lemma. | ||
| // Annoying sequence reasoning. | ||
| #[verifier(external_body)] | ||
| pub proof fn lemma_filtered_pods_set_equals_matching_pods( |
There was a problem hiding this comment.
@codyjrivera could you write more descriptive comments for this lemma?
There was a problem hiding this comment.
Yes -- I can write better comments.
There was a problem hiding this comment.
Is this one already proved or not? Coz I still see the external_body annotation.
There was a problem hiding this comment.
It's not proven yet -- I had proved the first of the conjuncts but not the other two -- I've outlined roughly what we need to do in the body.
I can try to prove it today --- Fridays are generally terrible for me schedule-wise though.
There was a problem hiding this comment.
OK feel free to merge this one when you are ready. I've done my review
Signed-off-by: Cody Rivera <[email protected]>
Signed-off-by: Cody Rivera <[email protected]>
Modulo some auxiliary lemmas, this PR provides proofs for WF1 lemmas on the Create path of the ReplicaSet controller.