cardano-ledger icon indicating copy to clipboard operation
cardano-ledger copied to clipboard
verified publisher icon IntersectMBO

Constraints and properties for GOVCERT rule

Open lehins opened this issue 2 years ago • 3 comments

lehins avatar Oct 25 '23 18:10 lehins

Already exists here https://github.com/input-output-hk/cardano-ledger/blob/f4269490502fc928c13a86e71c059d88cb5ac995/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs#L439

MaximilianAlgehed avatar Oct 25 '23 19:10 MaximilianAlgehed

We need to implement as many properties that verify that the rules behaves as expected, which is still missing

lehins avatar Oct 25 '23 20:10 lehins

This ticket defines some properties that can be testes with property testing: https://github.com/input-output-hk/cardano-ledger/issues/3881

In particular utilizing GetCommitteeMembersState to check the state change after certificate submission:

  • Status is Active and authorized Hot credential is MemberNotAuthorized right after committee member was enacted
  • Status is Active and Authorized Hot credential in MemberAuthorized matches the one that was supplied in the authorization certificate, right after submission of such certificate
  • Status is Active and Hot credential status is MemberResigned right after submission of resigning certificate

lehins avatar Nov 17 '23 12:11 lehins