Weekly Plans

[marshtompsxd]

Mar. 30 - Apr. 13

• Finish fixing the liveness proof for the simple controller @euclidgame Complete simple controller liveness proof #89
• Specify controller crash @marshtompsxd Specify controller crash behavior #91

Mar. 23 - Mar. 30

• Build simple controller exec code @marshtompsxd Implement executable simple controller and prove refinement #82
• Fix the lemma after_get_cr_pc ~> []cm_exists for simple controller @euclidgame Fix liveness proof: after_get_cr_pc ~> cm_always_exists #87
• Get familiar with the reference zookeeper controller @euclidgame

Mar. 16 - Mar. 23

• Use k8s openapi objects in Kubernetes cluster spec @marshtompsxd Use k8s openapi objects in spec and proof #78
• Simplify spec by assuming wf on triggering reconcile @marshtompsxd Assume the controller's reconcile is infinitely frequently triggered #79
• Prove []next /\ []fair /\ []exist |= true ~> reconcile_scheduled @marshtompsxd Prove true leads to reconcile scheduled under the assumption that cr always exists #81
• Fix the lemma after_create_cm_pc ~> []cm_exists for simple controller @euclidgame Fix simple controller liveness proof: Prove after_create_cm_pc ~> cm_always_exists #84

Mar. 2 - Mar. 9

• Specify the controller's list-then-watch behavior Specify the controller's list-then-watch pattern #71
• Layout the k8s openapi objects implementation in both exec and spec mode Implement exec and spec version of k8s openapi objects #74
• Prove the lemma for unpacking assumptions from spec Prove lemmas to unpack assumption #75

Feb. 23 - Mar. 2

• Revise the network model for at-most-once delivery At most once delivery #67
• Revise the network mode to use multiset to preserve duplicated messages At most once delivery #67

Feb. 16 - Feb. 23

• Assign unique id to request/response pairs Add unique id to request/response pair #65
• Investigate on the complexity of real-world controllers Kubernetes resource objects (and their fields) used by controllers #66

Feb. 9 - Feb. 16

• Build a simple controller using the Anvil style Implement simple controller based on the example from kube-rs #62
• Check how controllers use async/sync k8s API calls Async programming model in kube-rs and potential reordering between requests #61 Do controllers (in Rust) issue API requests asynchronously? #64
• Have a list of needed support for exec Map and trait cast from Verus

Dec. 7 - ... - Feb. 9

• Complete the simple controller spec (e.g., stream notification, send API request, receive API response) Prove liveness of simple controller #54
• Prove the liveness of the simple controller Prove liveness of simple controller #54
• Prove the stability of the simple controller Simple controller: prove stability #58
• Implement the generic type for reconciler Make ReconcileState a generic type RS #60
• Finish the D-F refactoring for the compound state machine liveness proof Refactor compound state machine liveness proof for LTL engine #53

Nov. 30 - Dec. 7

• Streamline the action abstraction using the generic Action type Use generic action type in spec #50
• Rewrite the weak fairness assumptions and enabled proof without the enabled operator Specialize wf1 and weak_fairness for Action #52
• Refactor compound state machine proof in the form friendly to LTL engine

Nov. 23 - Nov. 30

• Finish reworking the compound state machine Rework host state machines #49
• Write more complex controller spec

Nov. 16 - Nov. 23

• Implement the next_result interface of host/network state machine Rework host state machines #49

Nov. 9 - Nov. 16

• Rewrite the concurrent controller into a compound state machine Implement compound state machine #48
• Prove the safety and liveness property of the compound state machine Implement compound state machine #48
• Collect more real controller reconcile patterns Representative controller reconcile patterns #44

Nov. 2 - Nov. 9

• Fix the liveness property in Introduce deletion event to the concurrent controller state machine #45
• Implement variants of wf1 and leads_to_stable suitable for liveness proof
• Prove all the lemmas except execution_suffix_xxx ones Introduce deletion event to the concurrent controller state machine #45

Oct. 26 - Nov. 2

• Fix the liveness property and remove any wf assumption on user action Fix the liveness property of the concurrent controller #42
• Document TL lemmas Document temporal logic lemmas #43
• Introduce deletion event to the concurrent controller state machine Introduce deletion event to the concurrent controller state machine #45
• Collect real controller reconcile patterns Representative controller reconcile patterns #44

Oct. 19 - Oct. 26

• Reform StatePred/ActionPred from struct to FnSpec Reform StatePred/ActionPred from struct to FnSpec #38
• Clean up the state machine definition (e.g., remove redundant predicates/XXXPred) Clean up redundant StatePred/ActionPred #37
• Clean up the liveness proof (e.g., expose the closures in the proof to increase readability) Remove hardcoded string from concurrent controller #40 Fix the liveness property of the concurrent controller #42
• Make the concurrent controller more real (e.g., more string operation and less hardcoding) Remove hardcoded string from concurrent controller #40 Fix the liveness property of the concurrent controller #42

Oct. 12 - Oct. 19

• Specify the concurrent controller example Prove safety/liveness properties of the concurrent controller state machine #32
• Prove the liveness property of the concurrent controller Prove safety/liveness properties of the concurrent controller state machine #32
• Implement universal/existential quantifier for TLA Prove safety/liveness properties of the concurrent controller state machine #32

Oct. 5 - Oct. 12

• Address the comments on the temporal logic operator implementation from the meeting Fix bug in always(): change && to ==> so that the always() can be true #17 Implement enabled() for state predicates #18 Use FnSpec type for closure #19 Simplify liveness proof of the ABC state machine #20
• Specify the sequential controller Prove safety/liveness properties of the Coq controller example #23
• Prove the liveness property of the sequential controller Prove safety/liveness properties of the Coq controller example #23

Sep. 28 - Oct. 5

• Specify the ABC state machine Prove safety/liveness properties of the ABC state machine with temporal logic #11
• Prove the liveness property of the ABC state machine Prove safety/liveness properties of the ABC state machine with temporal logic #11

[marshtompsxd]

Close it since everyone knows what to do at this stage