View on GitHub
File Changes
                     StakePools (..), cwitness, decayKey, refund)
import           Delegation.PoolParams (poolSpec)

                      
-
import           BaseTypes (Nonce (..), UnitInterval, intervalValue, mkUnitInterval)
+
import           BaseTypes (UnitInterval, intervalValue, mkUnitInterval)

                      
import           Ledger.Core (dom, (∪), (∪+), (⋪), (▷), (◁))

                      
data NewEpochState hashAlgo dsignAlgo vrfAlgo =
  NewEpochState {
    nesEL    :: Epoch
-
  , nesEta0  :: Nonce
  , nesBprev :: BlocksMade hashAlgo dsignAlgo
  , nesBcur  :: BlocksMade hashAlgo dsignAlgo
  , nesEs    :: EpochState hashAlgo dsignAlgo vrfAlgo
  :: NewEpochState hashAlgo dsignAlgo vrfAlgo
  -> Set (GenKeyHash hashAlgo dsignAlgo)
getGKeys nes = Map.keysSet genDelegs
-
  where NewEpochState _ _ _ _ es _ _ _ = nes
+
  where NewEpochState _ _ _ es _ _ _ = nes
        EpochState _ _ ls _ = es
        LedgerState _ (DPState (DState _ _ _ _ _ (GenDelegs genDelegs) _) _) _ = ls

                      
data NewEpochEnv hashAlgo dsignAlgo =
  NewEpochEnv {
-
    neeEta1  :: Nonce
-
  , neeS     :: Slot
+
    neeS     :: Slot
  , neeGkeys :: Set (GenKeyHash hashAlgo dsignAlgo)
  } deriving (Show, Eq, Generic)

                      
overlaySchedule
  :: Epoch
  -> Set (GenKeyHash hashAlgo dsignAlgo)
-
  -> Nonce
  -> PParams
  -> Map Slot (Maybe (GenKeyHash hashAlgo dsignAlgo))
-
overlaySchedule e gkeys _ pp = Map.union active inactive
+
overlaySchedule e gkeys pp = Map.union active inactive
  where
    numActive = dval * fromIntegral slotsPerEpoch
    dval = intervalValue $ pp ^. d
  -> BlocksMade hashAlgo dsignAlgo
  -> LedgerState hashAlgo dsignAlgo vrfAlgo
  -> NewEpochState hashAlgo dsignAlgo vrfAlgo
-
updateNES (NewEpochState eL eta0 bprev _
+
updateNES (NewEpochState eL bprev _
           (EpochState acnt ss _ pp) ru pd osched) bcur ls =
-
  NewEpochState eL eta0 bprev bcur (EpochState acnt ss ls pp) ru pd osched
+
  NewEpochState eL bprev bcur (EpochState acnt ss ls pp) ru pd osched

                      
import           Data.Set (Set)

                      
-
import           BaseTypes
import           BlockChain
import           Keys
import           LedgerState
data BHEAD hashAlgo dsignAlgo kesAlgo vrfAlgo

                      
data BheadEnv hashAlgo dsignAlgo kesAlgo vrfAlgo
-
  = BheadEnv Nonce (Set (GenKeyHash hashAlgo dsignAlgo))
+
  = BheadEnv (Set (GenKeyHash hashAlgo dsignAlgo))

                      
instance
  ( HashAlgorithm hashAlgo
     )
  => TransitionRule (BHEAD hashAlgo dsignAlgo kesAlgo vrfAlgo)
bheadTransition = do
-
  TRC (BheadEnv etaC gkeys, [email protected](NewEpochState _ _ bprev _ es _ _ _), [email protected](BHeader bhb _)) <-
+
  TRC (BheadEnv gkeys, [email protected](NewEpochState _ bprev _ es _ _ _), [email protected](BHeader bhb _)) <-
    judgmentContext
  let slot                = bheaderSlot bhb
  let EpochState _ _ _ pp = es
  fromIntegral (hBbsize bhb) < _maxBBSize pp ?! BlockSizeTooLargeBHEAD

                      
  nes' <- trans @(NEWEPOCH hashAlgo dsignAlgo vrfAlgo)
-
    $ TRC (NewEpochEnv etaC slot gkeys, nes, epochFromSlot slot)
+
    $ TRC (NewEpochEnv slot gkeys, nes, epochFromSlot slot)

                      
  ru' <- trans @(RUPD hashAlgo dsignAlgo vrfAlgo) $ TRC (RupdEnv bprev es, nesRu nes', slot)
  let nes'' = nes' { nesRu = ru' }

                      
import           STS.Bbody
import           STS.Bhead
-
import           STS.Overlay
import           STS.Prtcl

                      
data CHAIN hashAlgo dsignAlgo kesAlgo vrfAlgo
      (NewEpochState hashAlgo dsignAlgo vrfAlgo)
      Nonce
      Nonce
+
      Nonce
      (HashHeader hashAlgo dsignAlgo kesAlgo vrfAlgo)
      Slot
  deriving (Show, Eq)
     )
  => TransitionRule (CHAIN hashAlgo dsignAlgo kesAlgo vrfAlgo)
chainTransition = do
-
  TRC (sNow, ChainState nes etaV etaC h sL, [email protected](Block bh _)) <- judgmentContext
+
  TRC (sNow, ChainState nes eta0 etaV etaC h sL, [email protected](Block bh _)) <- judgmentContext

                      
  let gkeys = getGKeys nes
  nes' <-
-
    trans @(BHEAD hashAlgo dsignAlgo kesAlgo vrfAlgo) $ TRC (BheadEnv etaC gkeys, nes, bh)
+
    trans @(BHEAD hashAlgo dsignAlgo kesAlgo vrfAlgo) $ TRC (BheadEnv gkeys, nes, bh)

                      
-
  let NewEpochState _ eta0 _ bcur es _ _pd osched = nes'
+
  let NewEpochState e1 _ _ _ _ _ _ = nes
+
      NewEpochState e2 _ bcur es _ _pd osched = nes'
  let EpochState (AccountState _ _reserves) _ ls pp                         = es
  let LedgerState _ (DPState (DState _ _ _ _ _ _genDelegs _) (PState _ _ _ cs)) _ = ls

                      
-
  PrtclState cs' h' sL' etaV' etaC' <- trans @(PRTCL hashAlgo dsignAlgo kesAlgo vrfAlgo)
-
    $ TRC ( PrtclEnv (OverlayEnv pp osched eta0 _pd _genDelegs) sNow
-
          , PrtclState cs h sL etaV etaC
+
  PrtclState cs' h' sL' eta0' etaV' etaC' <- trans @(PRTCL hashAlgo dsignAlgo kesAlgo vrfAlgo)
+
    $ TRC ( PrtclEnv pp osched _pd _genDelegs sNow (e1 /= e2)
+
          , PrtclState cs h sL eta0 etaV etaC
          , bh)

                      
  let ls' = setIssueNumbers ls cs'

                      
  let nes'' = updateNES nes' bcur' ls''

                      
-
  pure $ ChainState nes'' etaV' etaC' h' sL'
+
  pure $ ChainState nes'' eta0' etaV' etaC' h' sL'

                      
instance
  ( HashAlgorithm hashAlgo

                      
-- |Calculate the total ada in the chain state
totalAda :: ChainState hashAlgo dsignAlgo kesAlgo vrfAlgo -> Coin
-
totalAda (ChainState nes _ _ _ _) =
+
totalAda (ChainState nes _ _ _ _ _) =
  treasury_ + reserves_ + rewards_ + circulation + deposits + fees_
  where
    (EpochState (AccountState treasury_ reserves_) _ ls _) = nesEs nes
    [ pure $
      NewEpochState
        (Epoch 0)
-
        (mkNonce 0)
        (BlocksMade Map.empty)
        (BlocksMade Map.empty)
        emptyEpochState
  .  (HashAlgorithm hashAlgo, DSIGNAlgorithm dsignAlgo, VRFAlgorithm vrfAlgo)
  => TransitionRule (NEWEPOCH hashAlgo dsignAlgo vrfAlgo)
newEpochTransition = do
-
  TRC ( NewEpochEnv eta1 _s gkeys
-
      , [email protected](NewEpochState (Epoch eL) _ _ bcur es ru _pd _osched)
+
  TRC ( NewEpochEnv _s gkeys
+
      , [email protected](NewEpochState (Epoch eL) _ bcur es ru _pd _osched)
      , [email protected](Epoch e_)) <- judgmentContext
  if e_ /= eL + 1
    then pure src

                      
          pd' = Map.intersectionWith (,) sd (Map.map _poolVrf (_poolsSS ss))

                      
-
          osched' = overlaySchedule e gkeys eta1 pp
-

                      
-
          etaE = _extraEntropy pp
+
          osched' = overlaySchedule e gkeys pp

                      
          es'' = EpochState acnt ss ls (pp { _extraEntropy = NeutralNonce })

                      
      pure $ NewEpochState e
-
                           (eta1 ⭒ etaE)
                           bcur
                           (BlocksMade Map.empty)
                           es''

                      
import           BaseTypes
import           BlockChain
+
import           Delegation.Certificates
import           Keys
import           OCert
+
import           PParams
import           Slot

                      
import           STS.Overlay
      (Map (KeyHash hashAlgo dsignAlgo) Natural)
      (HashHeader hashAlgo dsignAlgo kesAlgo vrfAlgo)
      Slot
-
      Nonce
-
      Nonce
+
      Nonce -- ^ Current epoch nonce
+
      Nonce -- ^ Evolving nonce
+
      Nonce -- ^ Candidate nonce
  deriving (Generic, Show)

                      
instance NoUnexpectedThunks (PrtclState hashAlgo dsignAlgo kesAlgo vrfAlgo)

                      
data PrtclEnv hashAlgo dsignAlgo kesAlgo vrfAlgo
-
  = PrtclEnv (OverlayEnv hashAlgo dsignAlgo kesAlgo vrfAlgo) Slot
+
  = PrtclEnv
+
      PParams
+
      (Map Slot (Maybe (GenKeyHash hashAlgo dsignAlgo)))
+
      (PoolDistr hashAlgo dsignAlgo vrfAlgo)
+
      (GenDelegs hashAlgo dsignAlgo)
+
      Slot
+
      Bool -- ^ New epoch marker
  deriving (Generic)

                      
instance NoUnexpectedThunks (PrtclEnv hashAlgo dsignAlgo kesAlgo vrfAlgo)
     )
  => TransitionRule (PRTCL hashAlgo dsignAlgo kesAlgo vrfAlgo)
prtclTransition = do
-
  TRC (PrtclEnv oe sNow, PrtclState cs h sL etaV etaC, bh) <- judgmentContext
+
  TRC ( PrtclEnv pp osched pd dms sNow ne
+
      , PrtclState cs h sL eta0 etaV etaC
+
      , bh) <- judgmentContext
  let bhb  = bhbody bh
  let slot = bheaderSlot bhb
  let eta  = fromNatural . VRF.certifiedNatural $ bheaderEta bhb
  sL < slot && slot <= sNow ?! WrongSlotIntervalPRTCL
  h == bheaderPrev bhb ?! WrongBlockSequencePRTCL

                      
-
  cs'            <- trans @(OVERLAY hashAlgo dsignAlgo kesAlgo vrfAlgo) $ TRC (oe, cs, bh)
-
  UpdnState etaV' etaC' <- trans @UPDN $ TRC (eta, UpdnState etaV etaC, slot)
+
  UpdnState eta0' etaV' etaC'
+
    <- trans @UPDN $ TRC (UpdnEnv eta pp ne, UpdnState eta0 etaV etaC, slot)
+
  cs'
+
    <- trans @(OVERLAY hashAlgo dsignAlgo kesAlgo vrfAlgo)
+
        $ TRC (OverlayEnv pp osched eta0' pd dms, cs, bh)

                      
-
  pure $ PrtclState cs' (bhHash bh) slot etaV' etaC'
+
  pure $ PrtclState cs' (bhHash bh) slot eta0' etaV' etaC'

                      
instance
  ( HashAlgorithm hashAlgo

                      
module STS.Updn
  ( UPDN
+
  , UpdnEnv(..)
  , UpdnState(..)
  )
where

                      
import           BaseTypes
import           BlockChain
+
import           PParams
import           Slot

                      
import           Control.State.Transition

                      
data UPDN

                      
-
data UpdnState = UpdnState Nonce Nonce
+
data UpdnEnv = UpdnEnv Nonce PParams Bool
+
data UpdnState = UpdnState Nonce Nonce Nonce
  deriving (Show, Eq)

                      
instance STS UPDN where
  type State UPDN = UpdnState
  type Signal UPDN = Slot.Slot
-
  type Environment UPDN = Nonce
+
  type Environment UPDN = UpdnEnv
  data PredicateFailure UPDN = FailureUPDN
                               deriving (Show, Eq)
-
  initialRules = [pure (UpdnState (mkNonce 0) (mkNonce 0))]
+
  initialRules = [pure (UpdnState (mkNonce 0) (mkNonce 0) (mkNonce 0))]
  transitionRules = [updTransition]

                      
updTransition :: TransitionRule UPDN
updTransition = do
-
  TRC (eta, UpdnState eta_v eta_c, s) <- judgmentContext
+
  TRC (UpdnEnv eta pp ne, UpdnState eta_0 eta_v eta_c, s) <- judgmentContext
  let Epoch e = epochFromSlot s
-
  if s +* slotsPrior < firstSlot (Epoch (e + 1))
-
    then pure $ UpdnState (eta_v ⭒ eta) (eta_v ⭒ eta)
-
    else pure $ UpdnState (eta_v ⭒ eta) eta_c
+
  pure $ UpdnState
+
    (if ne then eta_c ⭒ _extraEntropy pp else eta_0)
+
    (eta_v ⭒ eta)
+
    (if s +* slotsPrior < firstSlot (Epoch (e + 1))
+
      then eta_v ⭒ eta
+
      else eta_c
+
    )
initStEx1 = ChainState
  (NewEpochState
     (Epoch 0)
-
     (mkNonce 0)
     (BlocksMade Map.empty)
     (BlocksMade Map.empty)
     esEx1
    -- The overlay schedule has one entry, setting Core Node 1 to slot 1.
  (mkNonce 0)
  (mkNonce 0)
+
  (mkNonce 0)
  lastByronHeaderHash
  (Slot 0)

                      
expectedStEx1 = ChainState
  (NewEpochState
     (Epoch 0)
-
     (mkNonce 0)
     (BlocksMade Map.empty)
     (BlocksMade Map.empty)
     -- Note that blocks in the overlay schedule do not add to this count.
     esEx1
     Nothing
     (PoolDistr Map.empty)
     (Map.singleton (Slot 1) (Just . hashKey $ coreNodeVKG 0)))
+
  (mkNonce 0)
  (mkNonce 0 ⭒ mkNonce 1)
  (mkNonce 0 ⭒ mkNonce 1)
  (bhHash (bheader blockEx1))
overlayEx2A = overlaySchedule
                    (Epoch 0)
                    (Map.keysSet genDelegs)
-
                    NeutralNonce
                    ppsEx1

                      
initStEx2A :: ChainState
initStEx2A = ChainState
  (NewEpochState
      (Epoch 0)
-
      (mkNonce 0)
      (BlocksMade Map.empty)
      (BlocksMade Map.empty)
      esEx2A
      overlayEx2A)
  (mkNonce 0)
  (mkNonce 0)
+
  (mkNonce 0)
  lastByronHeaderHash
  (Slot 0)

                      
expectedStEx2A = ChainState
  (NewEpochState
     (Epoch 0)
-
     (mkNonce 0)
     (BlocksMade Map.empty)
     (BlocksMade Map.empty)
     (EpochState acntEx2A emptySnapShots expectedLSEx2A ppsEx1)
     Nothing
     (PoolDistr Map.empty)
     overlayEx2A)
+
  (mkNonce 0)
  (mkNonce 0 ⭒ mkNonce 1)
  (mkNonce 0 ⭒ mkNonce 1)
  blockEx2AHash
expectedStEx2Bgeneric pp = ChainState
  (NewEpochState
     (Epoch 0)
-
     (mkNonce 0)
     (BlocksMade Map.empty)
     (BlocksMade Map.empty)
     (EpochState acntEx2A emptySnapShots expectedLSEx2B pp)
                        })
     (PoolDistr Map.empty)
     overlayEx2A)
+
  (mkNonce 0)
  (mkNonce 0 ⭒ mkNonce 1 ⭒ mkNonce 2)
  (mkNonce 0 ⭒ mkNonce 1)
  blockEx2BHash
epoch1OSchedEx2C = overlaySchedule
                    (Epoch 1)
                    (Map.keysSet genDelegs)
-
                    (mkNonce 0 ⭒ mkNonce 1)
                    ppsEx1

                      
snapEx2C :: (Stake, Map Credential KeyHash)
expectedStEx2Cgeneric ss ls pp = ChainState
  (NewEpochState
     (Epoch 1)
-
     (mkNonce 0 ⭒ mkNonce 1)
     (BlocksMade Map.empty)
     (BlocksMade Map.empty)
     (EpochState acntEx2A ss ls pp)
     Nothing
     (PoolDistr Map.empty)
     epoch1OSchedEx2C)
+
  (mkNonce 0 ⭒ mkNonce 1)
  (mkSeqNonce 3)
  (mkSeqNonce 3)
  blockEx2CHash
expectedStEx2D = ChainState
  (NewEpochState
     (Epoch 1)
-
     (mkNonce 0 ⭒ mkNonce 1)
     (BlocksMade Map.empty)
     (BlocksMade Map.empty)
     (EpochState acntEx2A snapsEx2C expectedLSEx2C ppsEx1)
                        })
     (PoolDistr Map.empty)
     epoch1OSchedEx2C)
+
  (mkNonce 0 ⭒ mkNonce 1)
  (mkSeqNonce 4)
  (mkSeqNonce 3)
  blockEx2DHash
epoch1OSchedEx2E = overlaySchedule
                    (Epoch 2)
                    (Map.keysSet genDelegs)
-
                    (mkSeqNonce 3)
                    ppsEx1

                      
snapsEx2E :: SnapShots
expectedStEx2E = ChainState
  (NewEpochState
     (Epoch 2)
-
     (mkSeqNonce 3)
     (BlocksMade Map.empty)
     (BlocksMade Map.empty)
     (EpochState acntEx2E snapsEx2E expectedLSEx2E ppsEx1)
          (hk alicePool)
          (1, hashKeyVRF (snd $ vrf alicePool))))
     epoch1OSchedEx2E)
+
  (mkSeqNonce 3)
  (mkSeqNonce 5)
  (mkSeqNonce 5)
  blockEx2EHash
expectedStEx2F = ChainState
  (NewEpochState
     (Epoch 2)
-
     (mkSeqNonce 3)
     (BlocksMade Map.empty)
     (BlocksMade $ Map.singleton (hk alicePool) 1)
     (EpochState acntEx2E snapsEx2E expectedLSEx2E ppsEx1)
                        })
     pdEx2F
     epoch1OSchedEx2E)
+
  (mkSeqNonce 3)
  (mkSeqNonce 6)
  (mkSeqNonce 5)
  blockEx2FHash
epoch1OSchedEx2G = overlaySchedule
                    (Epoch 3)
                    (Map.keysSet genDelegs)
-
                    (mkSeqNonce 5)
                    ppsEx1

                      
snapsEx2G :: SnapShots
expectedStEx2G = ChainState
  (NewEpochState
     (Epoch 3)
-
     (mkSeqNonce 5)
     (BlocksMade $ Map.singleton (hk alicePool) 1)
     (BlocksMade Map.empty)
     (EpochState (acntEx2E { _treasury = 33}) snapsEx2G expectedLSEx2G ppsEx1)
     Nothing
     pdEx2F
     epoch1OSchedEx2G)
+
  (mkSeqNonce 5)
  (mkSeqNonce 7)
  (mkSeqNonce 7)
  blockEx2GHash
expectedStEx2H = ChainState
  (NewEpochState
     (Epoch 3)
-
     (mkSeqNonce 5)
     (BlocksMade $ Map.singleton (hk alicePool) 1)
     (BlocksMade Map.empty)
     (EpochState (acntEx2E { _treasury = Coin 33 }) snapsEx2G expectedLSEx2G ppsEx1)
                        })
     pdEx2F
     epoch1OSchedEx2G)
import           Control.State.Transition.Trace (checkTrace, (.-), (.->))
import           Slot (Slot (..))
import           STS.Chain (totalAda)
-
import           STS.Updn (UPDN, UpdnState (..))
+
import           STS.Updn (UPDN, UpdnEnv(..), UpdnState (..))
import           STS.Utxow (PredicateFailure (..))
import           Tx (hashScript)
import           TxData (pattern RewardAcnt, pattern ScriptHashObj)
testUPNEarly :: Assertion
testUPNEarly =
  let
-
    st = applySTS @UPDN (TRC (mkNonce 1, UpdnState (mkNonce 2) (mkNonce 3), Slot.Slot 5))
+
    st = applySTS @UPDN
+
        ( TRC ( UpdnEnv (mkNonce 1) (error "Not needed now") False
+
              , UpdnState (mkNonce 0) (mkNonce 2) (mkNonce 3)
+
              , Slot.Slot 5
+
              )
+
        )
  in
-
    st @?= Right (UpdnState (mkNonce 2 ⭒ mkNonce 1) (mkNonce 2 ⭒ mkNonce 1))
+
    st @?= Right (UpdnState (mkNonce 0) (mkNonce 2 ⭒ mkNonce 1) (mkNonce 2 ⭒ mkNonce 1))

                      
-- | The UPDN transition should update only the evolving nonce
-- in the last thirds of the epoch.
-- Note that the number of slots per epoch is hard-coded in the Slot module.
testUPNLate :: Assertion
testUPNLate =
  let
-
    st = applySTS @UPDN (TRC (mkNonce 1, UpdnState (mkNonce 2) (mkNonce 3), Slot.Slot 85))
+
    st = applySTS @UPDN
+
          ( TRC ( UpdnEnv (mkNonce 1) (error "Not needed now") False
+
                , UpdnState (mkNonce 0) (mkNonce 2) (mkNonce 3)
+
                , Slot.Slot 85
+
                )
+
          )
  in
-
    st @?= Right (UpdnState ((mkNonce 2) ⭒ (mkNonce 1)) (mkNonce 3))
+
    st @?= Right (UpdnState (mkNonce 0) ((mkNonce 2) ⭒ (mkNonce 1)) (mkNonce 3))

                      
testCHAINExample :: CHAINExample -> Assertion
testCHAINExample (CHAINExample slotNow initSt block expectedSt) = do
        \var{pd} & \PoolDistr & \text{pool stake distribution} \\
        \var{dms} & \KeyHashGen\mapsto\KeyHash & \text{genesis key delegations} \\
        \var{s_{now}} & \Slot & \text{current slot} \\
+
        \var{ne} & \Bool & \text{new epoch marker} \\
      \end{array}
    \right)
  \end{equation*}