A Reward-Deposit Pair Used to represent the reward and the deposit for a given (Credential 'Staking c)

A UMElem compactly represents the range of 4 Maps with the same domain as a single n-tuple.

This space-compacting datatype, and the pattern UMElem are equivalent to: data Elem c = Elem { rdPairT :: !(StrictMaybe RDPair), ptrT :: !(Set Ptr), sPoolT :: !(StrictMaybe (KeyHash 'StakePool c)), -- the stake pool identity dRepT :: !(StrictMaybe (DRep c)), } deriving (Show, Eq, Generic, NoThunks, NFData)

To name the constructors of UMElem we use the notation Txxx where each x is either F for full, i.e. the component is present, or E for empty, i.e. the component is not present.

There are four components: 1) the reward-deposit pair as an RDPair (CompactForm Coin) (CompactForm Coin) as a pair of Word64s, the first x, 2) the set of pointers, the second x, 3) the stake pool id (KeyHash 'StakePool c), the third x, and 4) the voting delegatee id (DRep c), the fourth x.

So, TEEEE means none of the components are present, TFEEE means only the reward-deposit pair is present, TEFEE means only the set of pointers is present, TEEFE means only the stake pool id is present. etc. TEEEF means only the voting delegatee id is present, and

The pattern UMElem will correctly use the optimal constructor.

Extract the reward-deposit pair if it is present. We can tell that the reward is present when Txxxx has an F in the first position

This is equivalent to the pattern (UMElem (SJust r) _ _ _) -> Just r

Extract a delegated reward-deposit pair if it is present. We can tell that the pair is present and active when Txxxx has an F in the 1st position (present) and 3rd position (delegated).

This is equivalent to the pattern (UMElem (SJust r) _ (SJust _) _) -> Just r

Extract a DRep delegated reward if it is present. We can tell that the pair is present and active when Txxxx has an F in the 1st position (present) and 4rd position (DRep delegated).

This is equivalent to the pattern (UMElem (SJust r) _ _ (SJust d)) -> Just (r, d)

Extract rewards that are either delegated to a DRep or an SPO (or both). We can tell that the pair is present and active when Txxxx has F's in the 1st and either 3rd or 4th or both positions. If there are no rewards or deposits but the delegations still exist, then we return zero coin as reward.

Extract the set of pointers if it is non-empty. We can tell that the reward is present when Txxxx has an F in the second position

This is equivalent to the pattern (UMElem _ p _ _) -> Just p

Extract the stake delegatee pool id, if present. We can tell that the pool id is present when Txxxx has an F in the third position

This is equivalent to the pattern (UMElem _ _ (SJust s) _) -> Just s

Extract the voting delegatee id, if present. We can tell that the delegatee is present when Txxxx has an F in the fourth position

This is equivalent to the pattern (UMElem _ _ _ (SJust d)) -> Just d

A n-Tuple view of the UMElem. We can view all of the constructors as an UMElem.

null for an UMElem

null Maybe for an UMElem

A unified map represents 4 Maps with domain (Credential 'Staking c)

1) Map (Credential 'Staking c) RDPair -- (RDPair rewardCoin depositCoin) 2) Map (Credential 'Staking c) (Set Ptr) 3) Map (Credential 'Staking c) (StrictMaybe (KeyHash 'StakePool c)) 4) Map (Credential 'Staking c) (StrictMaybe (DRep c)) and one more map in the inverse direction with Ptr for keys and (Credential 'Staking c) for values.

Construct an empty UMap

It is worthwhile stating the invariant that holds on a Unified Map. The umPtrs and the ptrT field of the umElems are inverses.

All maps unrolled. It is important to note that all fields are lazy, because conversion from UMap can be expensive, thus only fields that are forced will incur that conversion overhead.

A UView lets one view a UMap in n different ways, one for each of the elements in a Unified Element UMElem (4) A (UView c key value) can be used like a (Map key value). It acts like a map, supporting efficient insert, delete, and lookup operations.

Construct a RewDepUView from the two maps that make up a UMap

Construct a PtrUView from the two maps that make up a UMap

Construct a SPoolUView from the two maps that make up a UMap

Construct a DRepUView from the two maps that make up a UMap

Extract the underlying UMap from a UView

Materialize a real VMap (Vector Map) from a UView This is expensive, use it wisely (like maybe once per epoch boundary to make a SnapShot)

Extract a reward-deposit pairs Map from a UMap

Extract a rewards Map from a UMap

Extract a compact rewards Map from a UMap

Extract a deposits Map from a UMap

Extract a pointers Map from a UMap

Extract a pointers Map from a UMap

Extract a stake pool delegations Map from a UMap

Extract a delegated-representatives Map from a UMap

Extract a domain-restricted Map of a UMap. If `Set k` is small this should be efficient.

Create a UMap from 4 separate maps. NOTE: For use in tests only.

Materialize a real Map from a View This is expensive, use it wisely (like maybe once per epoch boundary to make a SnapShot) See also domRestrictedMap, which domain-restricts before computing a view.

null for a UView, just like null

Membership check for a UView, just like member

Spec: eval (k ∈ dom (rewards dState)) eval (k ∈ dom (rewards ds))) eval (hk ∈ dom (rewards ds)) eval (hk ∉ dom (rewards ds))

Membership check for a UView, just like member

Spec: eval (k ∈ dom (rewards dState)) eval (k ∈ dom (rewards ds))) eval (hk ∈ dom (rewards ds)) eval (hk ∉ dom (rewards ds))

Delete a key and its value from the map-like UView, returning a version of the same UView.

In the case of a PtrUView we maintain the umInvariant and delete the pairs from both umElems as well as umPtrs of the UMap.

Insert with combination

If k exists as a key in the (map-like) UView:

1. to keep the old value > insertWith' ( old new -> old) k v view
2. to replace the old value with the new value > insertWith' ( old new -> new) k v view
3. to combine the old and new values with summation > insertWith' ( old new -> old + new) k v view

If k does not exist as a key in the UView, the combining function is ignored, and the key k and the value v are inserted into the map-like UView > insertWith' ignoredCombiningFunction k v view

Adjust a UView, just like adjust. This is implemented only for reward-deposit pairs.

Lookup a UView, just like lookup.

Get the domain of the Map-like UView

Get the range of the Map-like UView

Union with left preference. So if k, already exists, do nothing, if it doesn't exist insert it.

Spec: evalUnified (RewDepUView u1 ∪ singleton hk mempty) evalUnified (Ptrs u2 ∪ singleton ptr hk)

Union with left preference. So if k, already exists, do nothing, if it doesn't exist insert it.

Spec: evalUnified (RewDepUView u1 ∪ singleton hk mempty) evalUnified (Ptrs u2 ∪ singleton ptr hk)

Union with right preference. So if k, already exists, then old v is overwritten with the new v.

Special rules apply for the RewDepUView, where only the rdReward field of the RDPair is overwritten, and the old rdDeposit value persists.

Note: In this case it is an invariant that the domain of the Map on the right side is a subset of the domain of the RewDepUView. See the single case in module Cardano.Ledger.Shelley.Rules.Delegs, in the dealing with Withdrawals's where it is used at this type.

Spec: evalUnified (delegations ds ⨃ singleton hk dpool) evalUnified (rewards' ⨃ wdrls_')

Union with right preference. So if k, already exists, then old v is overwritten with the new v.

Special rules apply for the RewDepUView, where only the rdReward field of the RDPair is overwritten, and the old rdDeposit value persists.

Note: In this case it is an invariant that the domain of the Map on the right side is a subset of the domain of the RewDepUView. See the single case in module Cardano.Ledger.Shelley.Rules.Delegs, in the dealing with Withdrawals's where it is used at this type.

Spec: evalUnified (delegations ds ⨃ singleton hk dpool) evalUnified (rewards' ⨃ wdrls_')

Add the reward from the Map on the right side to the reward in the UView on the left. This is only implemented and is applicable to RewDepUViews.

We presume that the domain of the Map on the right, is a subset of the domain of the UView on the left.

Spec: evalUnified (rewards dState ∪+ registeredAggregated) evalUnified (rewards' ∪+ update) evalUnified (RewDepUView u0 ∪+ refunds)

Add the reward from the Map on the right side to the reward in the UView on the left. This is only implemented and is applicable to RewDepUViews.

We presume that the domain of the Map on the right, is a subset of the domain of the UView on the left.

Spec: evalUnified (rewards dState ∪+ registeredAggregated) evalUnified (rewards' ∪+ update) evalUnified (RewDepUView u0 ∪+ refunds)

Add the deposit from the Map on the right side to the deposit in the UView on the left. This is only implemented and is applicable to RewDepUViews.

Delete all keys in the given Set from the domain of the given map-like UView.

Spec: evalUnified (setSingleton hk ⋪ RewDepUView u0) evalUnified (setSingleton hk ⋪ SPoolUView u1)

Delete all keys in the given Set from the domain of the given map-like UView.

Spec: evalUnified (setSingleton hk ⋪ RewDepUView u0) evalUnified (setSingleton hk ⋪ SPoolUView u1)

Delete all elements in the given Set from the range of the given map-like UView. This is slow for SPoolUView, RewDepUView, and DReps UViews, better hope the sets are small

Spec: evalUnified (Ptrs u2 ⋫ setSingleton hk) evalUnified (SPoolUView u1 ⋫ retired)

Delete all elements in the given Set from the range of the given map-like UView. This is slow for SPoolUView, RewDepUView, and DReps UViews, better hope the sets are small

Spec: evalUnified (Ptrs u2 ⋫ setSingleton hk) evalUnified (SPoolUView u1 ⋫ retired)

Domain restriction.

Spec: eval (dom rewards' ◁ iRReserves (_irwd ds) :: RewardAccounts (Crypto era)) eval (dom rewards' ◁ iRTreasury (_irwd ds) :: RewardAccounts (Crypto era))

Domain restriction.

Spec: eval (dom rewards' ◁ iRReserves (_irwd ds) :: RewardAccounts (Crypto era)) eval (dom rewards' ◁ iRTreasury (_irwd ds) :: RewardAccounts (Crypto era))

Find the value associated with a key from a UView, return the default if the key is not there.

A UView is a view, so the size of the view is NOT the same as the size of the underlying UMElem map.

Delete the stake credentials in the domain and all associated ranges from the UMap This can be expensive when there are many pointers associated with the credential.