Update Ledger Spec to reflect the implementation

[ashisherc]

Update Ledger Spec to reflect the implementation

[disassembler]

The spec doesn't implement the pulser because there is no consensus layer in the spec. The way the pulser works is every tick a calculation is done that increments the pulser state until it completes or it reaches the 6k/f slots before the end of the epoch, at which point it forces the pulser to complete. However; the result is exactly the same if you do the entire calculation at the end of the epoch during ratification or if you pulse through it during the epoch. This is the difference between a spec and implementation. You want to keep the spec as simple as possible to be closest to the math itself, whereas in a real world where you need to propagate blocks, you have a lot more work to do to not slow down the system to a halt.

[disassembler]

More details around how pulser works (this applies to both stake rewards calculation and the governance pulser:

The pulser is initialized on the last block of the previous Epoch. After that all 3 of these have exactly the same answer.
in any block in the current era before the 6k/f point the pulser can be completed.
2. The pulser can be pulsed pulsed on some blocks and is completed at the 6k/f point
3. nothing is done at all, until the 6k/f point, at which time the pulser is completed

This is the state within the governance pulser. The vote scome from psProposals snapshot. Calculation can be forced with forceDRepPulsingState

-- | A snapshot of information from the previous epoch stored inside the Pulser.
--   After the pulser completes, but before the epoch turns, this information
--   is store in the 'DRComplete' constructor of the 'DRepPulsingState'
--   These are the values at the start of the current epoch. This allows the API
--   To access these "previous" values, both during and after pulsing.
data PulsingSnapshot era = PulsingSnapshot
  { psProposals :: !(StrictSeq (GovActionState era))
  , psDRepDistr :: !(Map (DRep (EraCrypto era)) (CompactForm Coin))
  , psDRepState :: !(Map (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
  , psPoolDistr :: Map (KeyHash 'StakePool (EraCrypto era)) (CompactForm Coin)
  }
  deriving (Generic)

[WhatisRT]

The point is that the pulser doesn't need to be in the spec since it's fully optional. An implementation doesn't have to do this and could instead choose to do exactly what is described in the spec. It would be perfectly able to participate in block validation and production, the only issue would be that it would have to do a large amount of work at the epoch boundary which is an issue in practice, but not in theory. Any implementation is free to solve that issue in whatever way they choose (or ignore it entirely).

In general, the issue of 'how do I compute a necessary value fast' is out of scope of the spec. What the spec does do is wait one epoch before it uses the result of ratification in any way. This is to enable solutions like the pulser that the Haskell implementation uses, but that's all.

[ashisherc]

I understand the need for a pulser, I would request to detail this exact process mentioned by @disassembler regarding the gov state snapshot in the spec as these details are missing and some wordings suggest that there is no pulse or gov state at all (I have ref relevant sections in the issue description). I'm in no way suggesting adding details regarding the pulser but the gov state snapshot.

I will create a different issue to suggest adding a query to be able to query the gov state snapshot, i.e it doesn't have to be part of the pulser state, similar to how Mark/Set/Go states are maintained, this gov state snapshot can be made available as part of the dump (outside of the pulser).

[disassembler]

I understand the need for a pulser, I would request to detail this exact process mentioned by @disassembler regarding the gov state snapshot in the spec as these details are missing and some wordings suggest that there is no pulse or gov state at all (I have ref relevant sections in the issue description). I'm in no way suggesting adding details regarding the pulser but the gov state snapshot.

See Figure 38 of the spec. The spec clearly shows gov state for RATIFY uses a snapshot.

[lehins]

this gov state snapshot can be made available as part of the dump (outside of the pulser).

We can't reliably create a query that will dump the pulser state, because queries are meant to be stable, while pulser is subject to change in the future. However, that doesn't mean we can't expose relevant parts of the pulser state as stable ledger state queries. For example, governance related stake distributions for SPOs and DReps that live in the pulser have already been exposed as ledger state queries. We can do the same for the RatifyState and Proposals, see #4511

I am not quite sure what the actual ask here in this ticket, but if I understand it correctly, then this ticket can be closed, since there is no reason to change the spec. As @WhatisRT's explanation points out, pulsing and snapshotting is an implementation detail that was done for performance reasons. In other words in the spec ratification and enactment happens in the beginning of the epoch, but the result isn't applied until the beginning of the next epoch, so there is never a need for creation of any snapshots. While in the implementation we do create a snapshot and spread out expensive computation throughout the first portion of the epoch. The most important part is that in the end we do get the same outcome.

Considering that there is no need to change the specification I will close this issue in favor of #4511. @ashisherc please add a comment on the aforementioned ticket if you feel like it does not capture everything that you are looking for. Also if you believe that I misunderstood the request of this issue, feel free to reopen it with some further elaboration. Side note for the future, any spec related issues normally should go into the formal-ledger-specification repository, however, since this case in particular is not relevant to the spec, this was a good place to create it.

The spec doesn't implement the pulser because there is no consensus layer in the spec.

@disassembler This isn't 100% accurate. A more correct way to say would be that we postpone the enactment for the whole epoch, because of consensus requirements of predicting future for HFC, but the fact that we use pulser to do the work is not relevant to consensus either. So, if we were to implement the same thing in Haskell as it is implemented in the Agda spec, it would all still work correctly even in presence of consensus layer, we would just have pretty bad slow downs on the epoch boundary.

The way the pulser works is every tick a calculation is done that increments the pulser state until it completes or it reaches the 6k/f slots before the end of the epoch, at which point it forces the pulser to complete.

This is 100% accurate. Here is a short document ADR-008-PParamsUpdate that goes into some more detail on how PParams updating works, which is the reason for the delay of enactment of PParams.