Fixed the certStateSpec

[TimSheard]

addresses Issue #4775

1. Embedded in the UMap of the DState, is the virtual DRep map with type
   Map (Credential Staking c) (DRep c)

2. There is a related map in the VState
   Map (Credential 'DRepRole c) (DRepState c)

Given the following two facts
A. every (Credential 'DRepRole c) corresponds to a unique DRep
B. Each DRepState contains a field drepDelegs:: DRepState -> Set (Credential Staking c)

There is a sort of inversse relation between the two maps
For every (Credential 'DRepRole c) in the Map in the VState, and every Set of Staking credentials associated with it, there is a corresponding entry in the DState Map, showing that each credential has delegated to the DRep uniquely identified by the (Credential 'DRepRole cere is a function that computes the invariant

-- | Compute the map of DReps, to those that delegate to them,
--   from the delegation map (Map (Credential 'Staking) Drep) which is stored in the DState
--   This ensures that every staking Credential, delegates to exactly one DRep.
aggregateDRep ::
  Map (Credential 'Staking c) (DRep c) ->
  Map (Credential 'DRepRole c) (Set (Credential 'Staking c))
aggregateDRep m = Map.foldlWithKey accum Map.empty m
  where
    accum ans cred (DRepKeyHash kh) = Map.insertWith Set.union (KeyHashObj kh) (Set.singleton cred) ans
    accum ans cred (DRepScriptHash sh) = Map.insertWith Set.union (ScriptHashObj sh) (Set.singleton cred) ans
    accum ans _ _ = ans

Maintaining this invariant is crucial. The problem was that in our attempt to state this invariant, we over-constrained the system, and the generators could not solve the over-constrained system,

This PR slightly restructures things so the invariant is maintained, and the system is no longer over constrained.

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• New tests are added if needed and existing tests are updated
• All visible changes are prepended to the latest section of a CHANGELOG.md for the affected packages.
  New section is never added with the code changes. (See RELEASING.md)
• When applicable, versions are updated in .cabal and CHANGELOG.md files according to the
  versioning process.
• The version bounds in .cabal files for all affected packages are updated.
  If you change the bounds in a cabal file, that package itself must have a version increase. (See RELEASING.md)
• Code is formatted with fourmolu (use scripts/fourmolize.sh)
• Cabal files are formatted (use scripts/cabal-format.sh)
• hie.yaml has been updated (use scripts/gen-hie.sh)
• Self-reviewed the diff

[teodanciu]

Thank you for the detailed explanation!
Looks good to me