Entities¶

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)

module Ledger.Dijkstra.Specification.Entities
  (gs : GovStructure) (open GovStructure gs) where

open import Ledger.Prelude renaming (filterˢ to filter)
open import Ledger.Prelude.Numeric.UnitInterval
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
open import Ledger.Dijkstra.Specification.Account gs
open import Ledger.Dijkstra.Specification.Certs gs
open RewardAddress
open PParams

Auxiliary Functions¶

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:

Look up stake addr in the accumulator.
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.
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 ENTITIES rule replaces pre-Dijkstra CERTS rule. This rule processes withdrawals, certificates and direct deposits.

Withdrawal Processing¶

The ENTITIES rule applies withdrawals, via applyWithdrawals before certificate evaluation. In the Dijkstra era, CIP-159 extends the withdrawal semantics from an "all-or-nothing" model (where the withdrawn amount must equal the full account balance) to a "partial withdrawal" model (where any amount up to the full balance may be withdrawn).

Premise (1) ensures that each withdrawal targets a registered account and that the withdrawal amount does not exceed the account's current balance.

The phantom-asset prohibition of CIP-159 — that withdrawals in one sub-transaction may not draw from deposits made by an earlier sub-transaction in the same batch — is enforced separately in the Utxo (see Phantom Asset Prevention).

Direct Deposit Application (CIP-159)¶

The ENTITIES rule applies CIP-159 direct deposits to the CertState after all individual CERT steps for the transaction have run, alongside its existing voteDelegs filtering. Specifically:

voteDelegs is restricted to credentials that delegate to a currently-registered DRep (or to the abstain / no-confidence pseudo-DReps).
rewards is augmented by directDeposits via ∪⁺ (union with addition) — equivalently, applyDirectDeposits directDeposits is applied to the threaded DState.

Premise (2) ensures that applyDirectDeposits does not silently re-introduce a credential into rewards that was deregistered earlier in the same transaction's CERT steps (and is therefore no longer present in voteDelegs, stakeDelegs, or deposits), which would produce an inconsistent DState.

open GovVote using (voter)

private variable
  rewards₀ rewards₁ : Rewards
  dReps : DReps
  stakeDelegs stakeDelegs₀ stakeDelegs₁ : StakeDelegs
  ccHotKeys : CCHotKeys
  voteDelegs₀ voteDelegs₁ : VoteDelegs
  wdrls : Withdrawals
  dd : DirectDeposits
  depositsᵍ depositsᵈ₀ depositsᵈ₁ : Credential ⇀ Coin

  dCerts : List DCert
  e : Epoch
  vs : List GovVote
  pp : PParams
  cc : ℙ Credential

  gState₁ : GState
  pState₀ pState₁ : PState

data _⊢_⇀⦇_,ENTITIES⦈_ : CertEnv → CertState → List DCert → CertState → Type where

  ENTITIES :
    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
        refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
        wdrlCreds       = mapˢ stake (dom wdrls)
        ddCreds         = mapˢ stake (dom dd)
        activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState₁))
                               ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
    in
    ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs₀
    ∙ wdrlCreds ⊆ dom rewards₀
    ∙ ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rewards₀ (stake addr)) -- (1)
    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4623}{\htmlId{5454}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4655}{\htmlId{5458}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4635}{\htmlId{5463}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4502}{\htmlId{5468}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4670}{\htmlId{5476}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4524}{\htmlId{5481}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4463}{\htmlId{5492}{\htmlClass{Generalizable}{\text{voteDelegs₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4397}{\htmlId{5506}{\htmlClass{Generalizable}{\text{stakeDelegs₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#1989}{\htmlId{5521}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4502}{\htmlId{5538}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4339}{\htmlId{5544}{\htmlClass{Generalizable}{\text{rewards₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4556}{\htmlId{5555}{\htmlClass{Generalizable}{\text{depositsᵈ₀}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4710}{\htmlId{5570}{\htmlClass{Generalizable}{\text{pState₀}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4933}{\htmlId{5582}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4439}{\htmlId{5599}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4546}{\htmlId{5611}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ dCerts  ,CERTS⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4475}{\htmlId{5648}{\htmlClass{Generalizable}{\text{voteDelegs₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4410}{\htmlId{5662}{\htmlClass{Generalizable}{\text{stakeDelegs₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4348}{\htmlId{5677}{\htmlClass{Generalizable}{\text{rewards₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4567}{\htmlId{5688}{\htmlClass{Generalizable}{\text{depositsᵈ₁}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4718}{\htmlId{5703}{\htmlClass{Generalizable}{\text{pState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4691}{\htmlId{5713}{\htmlClass{Generalizable}{\text{gState₁}}}}\, \end{pmatrix}$
    ∙ ddCreds ⊆ dom rewards₁ -- (2)
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4623}{\htmlId{5806}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4655}{\htmlId{5810}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4635}{\htmlId{5815}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4502}{\htmlId{5820}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4670}{\htmlId{5828}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4524}{\htmlId{5833}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4463}{\htmlId{5844}{\htmlClass{Generalizable}{\text{voteDelegs₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4397}{\htmlId{5858}{\htmlClass{Generalizable}{\text{stakeDelegs₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4339}{\htmlId{5873}{\htmlClass{Generalizable}{\text{rewards₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4556}{\htmlId{5884}{\htmlClass{Generalizable}{\text{depositsᵈ₀}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4710}{\htmlId{5899}{\htmlClass{Generalizable}{\text{pState₀}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4369}{\htmlId{5911}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4439}{\htmlId{5919}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4546}{\htmlId{5931}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ dCerts ,ENTITIES⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#4475}{\htmlId{5970}{\htmlClass{Generalizable}{\text{voteDelegs₁}}}}\, \,\href{Axiom.Set.Map.html#17775}{\htmlId{5982}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#5118}{\htmlId{5985}{\htmlClass{Bound}{\text{activeVDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4410}{\htmlId{6001}{\htmlClass{Generalizable}{\text{stakeDelegs₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#1890}{\htmlId{6016}{\htmlClass{Function}{\text{applyDirectDeposits}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4524}{\htmlId{6036}{\htmlClass{Generalizable}{\text{dd}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.html#4348}{\htmlId{6039}{\htmlClass{Generalizable}{\text{rewards₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4567}{\htmlId{6050}{\htmlClass{Generalizable}{\text{depositsᵈ₁}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4718}{\htmlId{6065}{\htmlClass{Generalizable}{\text{pState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#4691}{\htmlId{6075}{\htmlClass{Generalizable}{\text{gState₁}}}}\, \end{pmatrix}$

Entities¶

Auxiliary Functions¶

ENTITIES Transition System¶

Withdrawal Processing¶

Direct Deposit Application (CIP-159)¶

`ENTITIES` Transition System¶