IntersectMBO / IntersectMBO/formal-ledger-specifications
Check committee member on cold-key resignation in GOVCERT rule
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
In ledger, when we process a cold-key committee resignation certificate in GOVCERT, we are doing the following checks on the cold-key credential provided in the certificate:
1) the cold key has not already resigned (as per the `committeeState` stored in `VState`)
2) the cold key is either:
* part of the current committee (as per the committee members stored in `GovState`) or
* a candidate for a future committee (meaning: it appears in an existing `UpdateCommitee` proposal in the current `GovState`).
If any of the 1) , 2) checks fails, we are failing the rule. Our conformance test in ledger shows that in the spec, some of these checks are not implemented, because the rule is passing when we expect it to fail.
If we could implement this check in the (alternative) GOVCERT rule, we could enable the GOVCERT conformance test in ledger.
Contributor guide
Assessment
This issue has not been assessed yet.