Entities

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction using (TransactionStructure)

module Ledger.Dijkstra.Specification.Entities
  (txs : TransactionStructure) (open TransactionStructure txs) where

open import Ledger.Prelude renaming (filterˢ to filter)
open import Ledger.Prelude.Numeric.UnitInterval
open import Ledger.Dijkstra.Specification.Certs govStructure
open RewardAddress
open PParams

Auxiliary Types and Functions

record EntitiesEnv : Type where
  field
    epoch                   : Epoch
    pp                      : PParams
    coldCredentials         : ℙ Credential
    legacyMode              : Bool
    rewards₀                : Rewards

record SubEntitiesEnv : Type where
  field
    epoch                   : Epoch
    pp                      : PParams
    coldCredentials         : ℙ Credential
    rewards₀                : Rewards

unquoteDecl HasCast-EntitiesEnv HasCast-SubEntitiesEnv = derive-HasCast
  ( (quote SubEntitiesEnv , HasCast-SubEntitiesEnv) ∷
  [ (quote EntitiesEnv , HasCast-EntitiesEnv) ])

instance
  EntitiesEnv-HasEpoch : HasEpoch EntitiesEnv
  EntitiesEnv-HasEpoch .EpochOf = EntitiesEnv.epoch

  EntitiesEnv-HasColdCredentials : HasColdCredentials EntitiesEnv
  EntitiesEnv-HasColdCredentials .ColdCredentialsOf = EntitiesEnv.coldCredentials

  EntitiesEnv-HasPParams : HasPParams EntitiesEnv
  EntitiesEnv-HasPParams .PParamsOf = EntitiesEnv.pp

Since it underpins both applyDirectDeposits and applyWithdrawals, the applyToRewards function bears explaining. Given three arguments — a binary function f (e.g., addition or subtraction), a map m from RewardAddress to Coin (e.g., direct deposits or withdrawals), and a Rewards map (of account balances) — for each (addr , amt), the applyToRewards function does the following:

1. Look up stake addr in the accumulator.
2. If found with current balance bal, replace the entry with (stake addr, f bal amt). Note. since ∪ˡ is left-biased, the fresh singleton wins at stake addr and all other entries of acc are preserved; no explicit complement restriction is needed.
3. If not found (defensive; the caller's precondition will rule this out), return acc unchanged; this keeps applyToRewards total.

applyToRewards : (Coin → Coin → Coin) → (RewardAddress ⇀ Coin) → Rewards → Rewards
applyToRewards f m rwds =
  foldl (λ acc (addr , amt) → maybe (λ bal → ❴ stake addr , f bal amt ❵ ∪ˡ acc) acc (lookupᵐ? acc (stake addr)))
        rwds
        (setToList (m ˢ))

applyDirectDeposits : DirectDeposits → Rewards → Rewards
applyDirectDeposits = applyToRewards _+_

applyWithdrawals : Withdrawals → Rewards → Rewards
applyWithdrawals = applyToRewards _∸_

ENTITIES Transition System

In Dijkstra, the new ENTITIES rule subsumes the pre-Dijkstra CERTS rule. This rule in addition to processing certificates via CERTS, processes withdrawals, direct deposits, and account balance intervals.

CIP-159 introduces two new fields to transactions: directDeposits and balanceIntervals. Direct deposits represent value that flows from the transaction into account addresses. Balance intervals enable CIP-159 introduces three new transaction fields: txDirectDeposits, txBalanceIntervals and, at the top level only, txStartingBalanceIntervals. Direct deposits represent value that flows from the transaction into account addresses. The two interval fields let a transaction assert bounds on account balances: txBalanceIntervals against the balances this rule sees, and txStartingBalanceIntervals against the balances at the start of the whole batch (rewards₀).

Withdrawals

The ENTITIES rule applies withdrawals, via applyWithdrawals before certificate evaluation. In the Dijkstra era, withdrawals can be partial, unless in legacy mode. Whether legacy mode applies is decided in the LEDGER rule (via isLegacyMode, defined in the Utxow module) and provided here through the legacyMode field of EntitiesEnv.

Direct Deposits

The ENTITIES rule applies direct deposits to the CertState after CERTS.

open GovVote using (voter)

private variable
  txTop : TopLevelTx
  txSub : SubLevelTx
  rewards rewards' : Rewards
  dReps : DReps
  stakeDelegs stakeDelegs' : StakeDelegs
  ccHotKeys : CCHotKeys
  voteDelegs voteDelegs' : VoteDelegs
  rewards₀ : Rewards
  depositsᵍ depositsᵈ depositsᵈ' : Credential ⇀ Coin
  legacyMode : Bool

  e : Epoch
  pp : PParams
  cc : ℙ Credential

  gState' : GState
  pState pState' : PState

data _⊢_⇀⦇_,SUBENTITIES⦈_ : SubEntitiesEnv → CertState → SubLevelTx → CertState → Type where

  SUBENTITIES :
    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txSub))
        refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh

        withdrawals               = WithdrawalsOf txSub
        withdrawalsCredentials    = mapˢ stake (dom withdrawals)
        accountBalanceIntervals   = BalanceIntervalsOf txSub
        directDeposits            = DirectDepositsOf txSub
        directDepositsCredentials = mapˢ stake (dom directDeposits)
    in
    ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
    ∙ withdrawalsCredentials ⊆ dom rewards₀
    ∙ withdrawalsCredentials ⊆ dom rewards

    ∙ dom accountBalanceIntervals ⊆ dom rewards
    ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
        (InBalanceInterval (maybe id  (lookupᵐ? rewards c)) interval)

    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#5013}{\htmlId{6063}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5025}{\htmlId{6067}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5040}{\htmlId{6072}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4880}{\htmlId{6083}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4815}{\htmlId{6096}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#2912}{\htmlId{6110}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#5428}{\htmlId{6127}{\htmlClass{Bound}{\text{withdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4770}{\htmlId{6139}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4949}{\htmlId{6149}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5080}{\htmlId{6163}{\htmlClass{Generalizable}{\text{pState}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#5337}{\htmlId{6174}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4856}{\htmlId{6191}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4939}{\htmlId{6203}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ DCertsOf txSub  ,CERTS⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4891}{\htmlId{6248}{\htmlClass{Generalizable}{\text{voteDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4827}{\htmlId{6262}{\htmlClass{Generalizable}{\text{stakeDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4778}{\htmlId{6277}{\htmlClass{Generalizable}{\text{rewards'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4959}{\htmlId{6288}{\htmlClass{Generalizable}{\text{depositsᵈ'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5087}{\htmlId{6303}{\htmlClass{Generalizable}{\text{pState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5061}{\htmlId{6313}{\htmlClass{Generalizable}{\text{gState'}}}}\, \end{pmatrix}$

    ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
    ∙ directDepositsCredentials ⊆ dom rewards'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#5013}{\htmlId{6478}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5025}{\htmlId{6482}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5040}{\htmlId{6487}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4918}{\htmlId{6492}{\htmlClass{Generalizable}{\text{rewards₀}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4880}{\htmlId{6509}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4815}{\htmlId{6522}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4770}{\htmlId{6536}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4949}{\htmlId{6546}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5080}{\htmlId{6560}{\htmlClass{Generalizable}{\text{pState}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4799}{\htmlId{6571}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4856}{\htmlId{6579}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4939}{\htmlId{6591}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ txSub ,SUBENTITIES⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4891}{\htmlId{6632}{\htmlClass{Generalizable}{\text{voteDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4827}{\htmlId{6646}{\htmlClass{Generalizable}{\text{stakeDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#2813}{\htmlId{6661}{\htmlClass{Function}{\text{applyDirectDeposits}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#5610}{\htmlId{6681}{\htmlClass{Bound}{\text{directDeposits}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4778}{\htmlId{6696}{\htmlClass{Generalizable}{\text{rewards'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4959}{\htmlId{6707}{\htmlClass{Generalizable}{\text{depositsᵈ'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5087}{\htmlId{6722}{\htmlClass{Generalizable}{\text{pState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5061}{\htmlId{6732}{\htmlClass{Generalizable}{\text{gState'}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → CertState → Type where

  ENTITIES :
    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop))
        refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh

        withdrawalsSubTxs               = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop)
        withdrawals                     = WithdrawalsOf txTop
        withdrawalsCredentials          = mapˢ stake (dom withdrawals)
        accountBalanceIntervals         = BalanceIntervalsOf txTop
        startingAccountBalanceIntervals = StartingBalanceIntervalsOf txTop
        directDeposits                  = DirectDepositsOf txTop
        directDepositsCredentials       = mapˢ stake (dom directDeposits)
    in

    ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
    ∙ withdrawalsCredentials ⊆ dom rewards

    ∙ (legacyMode ≡ true →
        ∙ ∀[ (addr , amt) ∈ withdrawals ˢ ] amt ≡ maybe id  (lookupᵐ? rewards (stake addr))
        ∙ ∀[ (addr , amt) ∈ withdrawalsSubTxs ˢ ] amt ≤ maybe id  (lookupᵐ? rewards₀ (stake addr)))

    ∙ (legacyMode ≡ false →
        ∙ withdrawalsCredentials ⊆ dom rewards₀
        ∙ ∀[ (addr , amt) ∈ (withdrawalsSubTxs ∪⁺ withdrawals) ˢ ] amt ≤ maybe id  (lookupᵐ? rewards₀ (stake addr)))

    ∙ dom accountBalanceIntervals ⊆ dom rewards
    ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
        (InBalanceInterval (maybe id  (lookupᵐ? rewards c)) interval)

    ∙ dom startingAccountBalanceIntervals ⊆ dom rewards₀
    ∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ]
        (InBalanceInterval (maybe id  (lookupᵐ? rewards₀ c)) interval)

    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#5013}{\htmlId{8466}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5025}{\htmlId{8470}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5040}{\htmlId{8475}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4880}{\htmlId{8486}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4815}{\htmlId{8499}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#2912}{\htmlId{8513}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#7160}{\htmlId{8530}{\htmlClass{Bound}{\text{withdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4770}{\htmlId{8542}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4949}{\htmlId{8552}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5080}{\htmlId{8566}{\htmlClass{Generalizable}{\text{pState}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#6950}{\htmlId{8577}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4856}{\htmlId{8594}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4939}{\htmlId{8606}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ DCertsOf txTop  ,CERTS⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4891}{\htmlId{8651}{\htmlClass{Generalizable}{\text{voteDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4827}{\htmlId{8665}{\htmlClass{Generalizable}{\text{stakeDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4778}{\htmlId{8680}{\htmlClass{Generalizable}{\text{rewards'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4959}{\htmlId{8691}{\htmlClass{Generalizable}{\text{depositsᵈ'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5087}{\htmlId{8706}{\htmlClass{Generalizable}{\text{pState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5061}{\htmlId{8716}{\htmlClass{Generalizable}{\text{gState'}}}}\, \end{pmatrix}$

    ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
    ∙ directDepositsCredentials ⊆ dom rewards'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#5013}{\htmlId{8881}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5025}{\htmlId{8885}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5040}{\htmlId{8890}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4992}{\htmlId{8895}{\htmlClass{Generalizable}{\text{legacyMode}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4918}{\htmlId{8908}{\htmlClass{Generalizable}{\text{rewards₀}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4880}{\htmlId{8925}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4815}{\htmlId{8938}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4770}{\htmlId{8952}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4949}{\htmlId{8962}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5080}{\htmlId{8976}{\htmlClass{Generalizable}{\text{pState}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4799}{\htmlId{8987}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4856}{\htmlId{8995}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4939}{\htmlId{9007}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ txTop ,ENTITIES⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4891}{\htmlId{9045}{\htmlClass{Generalizable}{\text{voteDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4827}{\htmlId{9059}{\htmlClass{Generalizable}{\text{stakeDelegs'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#2813}{\htmlId{9074}{\htmlClass{Function}{\text{applyDirectDeposits}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#7435}{\htmlId{9094}{\htmlClass{Bound}{\text{directDeposits}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4778}{\htmlId{9109}{\htmlClass{Generalizable}{\text{rewards'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4959}{\htmlId{9120}{\htmlClass{Generalizable}{\text{depositsᵈ'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5087}{\htmlId{9135}{\htmlClass{Generalizable}{\text{pState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#5061}{\htmlId{9145}{\htmlClass{Generalizable}{\text{gState'}}}}\, \end{pmatrix}$