Sync executable with formal spec - NEWEPOCH STS

[uroboros]

The exec. spec effectively does

floor (activeSlotCoeeff pp * (floor ((d pp) * SlotsPerEpoch))) - 1

instead of the formal spec's

floor (activeSlotCoeeff pp * ((d pp) * SlotsPerEpoch)))

• the exec spec considers the two cases

  e_l + 1 /= e
  e_l + 1 == e

and the formal spec uses two different cases althogether

e  = e_l + 1
e_l /= e + 1

• the sd and pd' definitions in the formal spec are hard to recognise in the exec spec

[mgudemann]

I see if eL' + 1 /= e' then pure src else do in the exec spec

[mgudemann]

I agree that aggregate+ should be translated more clearly, maybe using Relation could be of help here?

[uroboros]

I see if eL' + 1 /= e' then pure src else do in the exec spec

thanks, fixed that in the above (but the mismatch remains)