Roadmaps and to-do lists

[marshtompsxd]

Must-to-have

• Have a Zookeeper controller implementation that supports creation and update (e.g., scaling, reconfiguration) and verify its liveness by 08/01/2023
• Have a Rabbitmq controller implementation that supports creation and update and verify its liveness by 09/01/2023
• Support non-k8s API calls in controller implementations by 9/01/2023
• Implement scale-down operation (which requires non-k8s API) for the Zookeeper controller 9/01/2023
• Prove liveness with non-k8s API for the Zookeeper controller 9/15/2023
• Specify the k8s garbage collector (a built-in controller) 9/01/2023
• Have a Fluent verified controller implementation by 9/01/2023
• Support multiple reconcile loops by 10/01/2023
• Implement multiple reconcile loops for the Fluent controller 10/15/2023
• API and experience sharing for gradual verification 10/15/2023

Nice-to-have

• Specify and prove isolation-related safety properties
• Verify deletion operations for one controller
• Test verified controllers using SOTA testing tools
• A study on the prevalent bugs in controllers
• A study on the common features in controllers
• Specify more built-in controllers (e.g., stateful set, deployment)

Concrete to-dos

• Make from_dynamic_object return Result and handle error cases (Major)
• Make to_dynamic_object return Result and handle error cases (Medium)
• Implement update operations for the Zookeepr controller (Major)
• Refactor DynamicObjectView to split spec and status data (Major)
• Try out StatefulSetPersistentVolumeClaimRetentionPolicy (Major)
• Refactor update handling logic to avoid increasing rv if the object remains unchanged (Medium)
• Make the spec reconciler a trait with safety and liveness proof obligations (Medium)
• Support owner_reference (Major)
• Support uid (Major)
• Split the tla rules into multiple files (Medium)
• Merge the schedule_controller_reconcile action and the run_scheduled_reconcile action (Medium)
• Remove overly designed abbreviation methods in the top-level state machine and proof (Medium)
• Refactor Anvil built-in lemmas to parameterize them with spec (Medium)
• Support cluster-scoped resources (Medium)
• Merge e2e tests into CI (Medium)
• Update the docs (Minor)

... and many more