Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Prove key invariants for VReplicaSet possibly involving PodEvent #549

Merged
merged 13 commits into from
Oct 2, 2024
Merged

Prove key invariants for VReplicaSet possibly involving PodEvent #549

merged 13 commits into from
Oct 2, 2024

Commits on Oct 1, 2024

  1. Get infrastructure set up to prove invariants 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    4f74701 View commit details
    Browse the repository at this point in the history

  2. Outline proof 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    0242e2a View commit details
    Browse the repository at this point in the history

  3. Finish lemma_eventually_always_no_pending_update_or_update_status_req… 

    …uest_on_pods

Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    729d2aa View commit details
    Browse the repository at this point in the history

  4. Actually get proof working 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    c2a41f0 View commit details
    Browse the repository at this point in the history

  5. Simplify proof 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    388479b View commit details
    Browse the repository at this point in the history

  6. Add partially-completed proofs about API requests on pods 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    b321b65 View commit details
    Browse the repository at this point in the history

  7. Proved 'create' modulo key == cr_key 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    995a6b5 View commit details
    Browse the repository at this point in the history

  8. Get a. e. create matching pod request lemma proved, modulo a definiti… 

    …on change

Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    e82d9d4 View commit details
    Browse the repository at this point in the history

  9. Fix broken VReplicaSet proofs 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    d34554e View commit details
    Browse the repository at this point in the history

  10. partial delete progress 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    33a3979 View commit details
    Browse the repository at this point in the history

  11. Mark unproven cases to prove later 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    ff86444 View commit details
    Browse the repository at this point in the history

  12. Finish another case

    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    d3b405d View commit details
    Browse the repository at this point in the history

  13. Small touchup 

    Signed-off-by: Cody Rivera <[email protected]>
    @codyjrivera
    codyjrivera committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    325cf8a View commit details
    Browse the repository at this point in the history