Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP Added the Data.Pulse module #2125

Closed
wants to merge 18 commits into from
Closed
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
107 changes: 99 additions & 8 deletions semantics/executable-spec/src/Data/Pulse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,12 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE StandaloneDeriving #-}


module Data.Pulse where

Expand All @@ -12,6 +18,10 @@ import Data.Map(Map)
import qualified Data.Map.Strict as Map
import Data.Map.Internal (Map (..))
import Control.Monad.Identity(Identity(..))
import Data.Coders
import Cardano.Binary(ToCBOR(..),FromCBOR(..))
import Data.Typeable


-- ====================================================

Expand Down Expand Up @@ -43,20 +53,25 @@ data PulseListM m ans where

instance Show ans => Show (PulseListM m ans) where
show(PulseList ass n _ t a) = "(Pulse "++assoc ass++show n++status t++show a++")"
where status [] = " Done "
status (_ : _) = " More "
assoc LeftA = "left "
where assoc LeftA = "left "
assoc RightA = "right "

isNil :: [a] -> Bool
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

isNil [] = True
isNil (_ : _) = False

status :: [a] -> String
status x = if isNil x then " Done " else " More "

-- =================================
-- Pulse structure for Map in an arbitray monad

data PulseMapM m ans where
PulseMap:: !Int -> !(ans -> k -> v -> m ans) -> !(Map k v) -> !ans -> PulseMapM m ans

instance Show ans => Show (PulseMapM m ans) where
show(PulseMap n _ t a) = "(Pulse "++show n++status t++show a++")"
where status x = if Map.null x then " Done " else " More "
show(PulseMap n _ t a) =
"(Pulse "++show n++(if Map.null t then " Done " else " More ")++show a++")"

-- ===============================================================
-- Pulse structures can be Specialize to the Identity Monad
Expand Down Expand Up @@ -89,8 +104,7 @@ complete p = runIdentity (completeM p)
-- Some instances

instance Pulsable PulseListM where
done (PulseList _ _ _ [] _) = True
done (PulseList _ _ _ (_: _) _) = False
done (PulseList _ _ _ zs _) = isNil zs
current (PulseList _ _ _ _ ans) = ans
pulseM (PulseList ass n accum balance ans) = do
let (steps, balance') = List.splitAt n balance
Expand Down Expand Up @@ -247,4 +261,81 @@ iosum = PulseList LeftA 2 (\ () k -> putStrLn (show k)) [(1::Int)..5] ()
*Pulse> pulseM it
5
(Pulse left 2 Done ())
-}
-}

{-
Need to serialize

-}

-- =========================================================
-- Every instance of MAccum, refers to exactly one function

class MAccum unique (m :: Type -> Type) free item ans | unique -> m free item ans where
maccum :: unique -> free -> ans -> item -> m ans

-- Here is an example instance

-- Make a Unique Unit type. (I.e. an enumeration with one constructor)
data XXX = XXX
deriving Show

instance ToCBOR XXX where toCBOR XXX = encode(Rec XXX)
instance FromCBOR XXX where fromCBOR = decode(RecD XXX)

-- | The unique 'maccum' function of the (MAccum XXX _ _ _ _) instance

fooAccum :: [a] -> Int -> Int -> Identity Int
fooAccum bs ans v = Identity (v+ans + length bs)

instance MAccum XXX Identity [Bool] Int Int where
maccum XXX = fooAccum

-- =========================================================
-- LL is a first order data type (no embedded functions)
-- that can be given a (Pulsable (LL name)) instance, We
-- can also make ToCBOR and FromCBOR instances for it.

data LL name (m :: Type -> Type) ans where
LL:: (MAccum name m free v ans, ToCBOR v, ToCBOR free) =>
name -> !Int -> !free -> ![v] -> !ans -> LL name m ans

instance (Show ans, Show name) => Show (LL name m ans) where
show (LL name n _ vs ans) = "(LL "++show name++" "++show n++status vs++" "++show ans++")"


-- There is a single ToCBOR instance for (LL name m ans)
-- But because of the uniqueness of the name, which implies
-- the hidden types (free and v for LL), We must supply
-- a unique FromCBOR instance for each name. See the XXX example below.

instance (Typeable m, ToCBOR name, ToCBOR ans) => ToCBOR (LL name m ans) where
toCBOR (LL name n free vs ans) = encode(Rec (LL name) !> To n !> To free !> To vs !> To ans)

instance Pulsable (LL name) where
done (LL _name _n _free zs _ans) = isNil zs
current (LL _ _ _ _ ans) = ans
pulseM (LL name n free balance ans) = do
let (steps, balance') = List.splitAt n balance
ans' <- foldlM' (maccum name free) ans steps
pure (LL name n free balance' ans')


-- =================================================
-- To make a serializable type that has a (Pulsable (LL name)) instance,
-- first, define a Unit type (an enumeration with 1 constructor).
-- This will have a unique MAccum instance, which
-- will refer to a unique function with no free variables.
-- If we follow the pattern below, then the Pulsable instance
-- will refer to that (MAccum) instance, but will store only
-- first order data.

-- We must supply a unique FromCBOR instance for each 'name'. The 'name'
-- fixes the monad 'm' and 'ans' type, as well as the 'maccum' function
-- for XXX at the value level.

instance FromCBOR (LL XXX Identity Int) where
fromCBOR = decode (RecD (LL XXX) <! From <! From <! From <! From)

foo :: LL XXX Identity Int
foo = LL XXX 3 [True] [1,2,3,5,6,7,8] 0
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,12 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}

module Shelley.Spec.Ledger.Rewards
( desirability,
Expand All @@ -32,6 +38,7 @@ module Shelley.Spec.Ledger.Rewards
memberRew,
aggregateRewards,
sumRewards,
rewardLL,
)
where

Expand All @@ -45,7 +52,7 @@ import Cardano.Binary
encodeWord,
)
import qualified Cardano.Ledger.Crypto as CC (Crypto)
import Cardano.Ledger.Era (Crypto)
import Cardano.Ledger.Era (Era,Crypto)
import Cardano.Ledger.Val ((<->))
import Cardano.Slotting.Slot (EpochSize)
import Control.DeepSeq (NFData)
Expand Down Expand Up @@ -98,6 +105,9 @@ import Shelley.Spec.Ledger.Serialization
encodeFoldable,
)
import Shelley.Spec.Ledger.TxBody (PoolParams (..), getRwdCred)
import Data.Pulse(LL(..),MAccum(..))
import Data.Kind(Type)
import Data.Typeable

newtype LogWeight = LogWeight {unLogWeight :: Float}
deriving (Eq, Generic, Ord, Num, NFData, NoThunks, ToCBOR, FromCBOR)
Expand Down Expand Up @@ -661,3 +671,84 @@ nonMyopicMemberRew
f = maxPool pp rPot (unStakeShare nm) (unStakeShare s)
fHat = floor (p * (fromRational . coinToRational) f)
in memberRew (Coin fHat) pool t nm


-- ==========================================


data FreeVars era =
FreeVars{ b:: Map (KeyHash 'StakePool (Crypto era)) Natural,
delegs:: Map (Credential 'Staking (Crypto era)) (KeyHash 'StakePool (Crypto era)),
stake:: Stake (Crypto era),
addrsRew :: Set (Credential 'Staking (Crypto era)),
totalStake :: Integer,
activeStake :: Integer,
asc :: ActiveSlotCoeff,
totalBlocks :: Natural, --
r :: Coin,
pp :: PParams era,
slotsPerEpoch :: EpochSize }


actionFree
:: (Monad m) =>
FreeVars era
-> ( Map (Credential 'Staking (Crypto era)) (Set (Reward (Crypto era)))
, Map (KeyHash 'StakePool (Crypto era)) Likelihood)
-> (KeyHash 'StakePool (Crypto era), PoolParams (Crypto era))
-> ProvM
(Map
(KeyHash 'StakePool (Crypto era))
(RewardProvenancePool (Crypto era)))
m
( Map (Credential 'Staking (Crypto era)) (Set (Reward (Crypto era)))
, Map (KeyHash 'StakePool (Crypto era)) Likelihood)
actionFree (FreeVars{b,delegs,stake,addrsRew,totalStake,activeStake,asc,totalBlocks,r,pp,slotsPerEpoch})
(m1, m2) (hk, pparams) = do
let blocksProduced = Map.lookup hk b
actgr@(Stake s) = poolStake hk delegs stake
Coin pstake = fold s
sigma = if totalStake == 0 then 0 else fromIntegral pstake % fromIntegral totalStake
sigmaA = if activeStake == 0 then 0 else fromIntegral pstake % fromIntegral activeStake
ls =
likelihood
(fromMaybe 0 blocksProduced)
(leaderProbability asc sigma (_d pp))
slotsPerEpoch
case blocksProduced of
Nothing -> pure (m1, Map.insert hk ls m2)
Just n -> do
m <- rewardOnePool pp r n totalBlocks pparams actgr sigma sigmaA (Coin totalStake) addrsRew
pure (Map.unionWith Set.union m m1, Map.insert hk ls m2)

data RewardCalc (m:: Type -> Type) era c = RewardCalc

instance (Monad m, c ~ Crypto era) =>
MAccum (RewardCalc m era c)
(ProvM (Map (KeyHash 'StakePool c) (RewardProvenancePool c)) m)
(FreeVars era)
(KeyHash 'StakePool c, PoolParams c)
( Map (Credential 'Staking c) (Set (Reward c)),
Map (KeyHash 'StakePool c) Likelihood )
where maccum RewardCalc = actionFree

-- Make an example LL

instance Typeable era => ToCBOR (FreeVars era) where
toCBOR _x = undefined

freevars :: FreeVars era
freevars = undefined

rewardLL :: (Monad m, Era era) =>
LL
(RewardCalc m era (Crypto era))
(ProvM
(Map
(KeyHash 'StakePool (Crypto era))
(RewardProvenancePool (Crypto era)))
m)
(Map
(Credential 'Staking (Crypto era)) (Set (Reward (Crypto era))),
Map (KeyHash 'StakePool (Crypto era)) Likelihood)
rewardLL = LL RewardCalc 10 freevars [] (Map.empty, Map.empty)