-
Notifications
You must be signed in to change notification settings - Fork 9
Build and verify admission controller for vstatefulset #610
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.
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
Conversation
Added/fix some specs for statefulset to make complete These specs are also commented out so that it passes ci
@hank95179 I think we are still missing specs for: DeploymentSet
StatefulSet
|
|
||
|
||
// updateStrategy.rollingUpdate.partition is non-negative | ||
&&& self.spec.update_strategy.get_Some_0().rolling_update.get_Some_0().partition.is_Some() ==> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@agrama64 I think we should still check for rolling_update.is_Some() before using get_Some_0()
refactor: use match to condense logic
Deployment spec
comment out for ci to work
@hank95179 @fredred375 could you submit two PRs, one for stateful set and one for deployment set? You can keep this PR for stateful set. Also, could you change the first comment to describe what this PR does? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is the code commented out now?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I commented out the new specs for both deployment and statefulset so that it doesnt mess up ci. Primarily for deployment, but also commented out statefulset just to be safe.
But yes, that probably isnt needed for statefulset and everything should still work
Found various mistakes in the proposed spec: 1. serviceName is not required and can even be empty 2. Missing ")" 3. revisionHistoryLimit can be any integer 4. Minor fix and comments on volume_claim_templates 5. is_some get_some logic for persistentVolumeClaim... and ordinals.start
@marshtompsxd I have create another PR for deployment and this one PR will only for statefulset. |
@hank95179 Can you uncomment the code and see whether Verus reports any error? |
There should be an entry file just like https://github.com/anvil-verifier/anvil/blob/main/src/v2_vdeployment_controller.rs that imports the statefulset files simply to check whether everything compiles and passes Verus' check |
* add: temporary statefulsetview definitions for verfication * add: ci for statefulset verification
@marshtompsxd
|
@hank95179 could you address this conflict with |
Should we close this PR? |
@hank95179 we can go on and close this |
This PR defines the
state_validation
spec function for a StatefulSet object.Rules include the following fields. The fields selector, template, and replicas are omitted below since they are identical to ReplicaSet and Deployment
state_validation
is implemented forPersistentVolumeClaim
for now.