IntersectMBO / IntersectMBO/formal-ledger-specifications

Check committee member on cold-key resignation in GOVCERT rule

Open
#634 4 comments 0 reactions 1 assignee Claimed by @williamdemeo View on GitHub
conformance era: conway
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.