CredDepsEqualDomRwds

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs)
  where

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Chain txs abs
open import Ledger.Prelude hiding (map) renaming (mapˢ to map; filterˢ to filter)
open import Ledger.Conway.Specification.Properties txs abs

Claim (Equality of credential depsoits is a CHAIN invariant).

Informally.

This property concerns two quantities associated with a given ChainState cs,

• the credential deposits of the UTxOState of cs and

• the credential deposits of the rewards in the ledger state of cs.

The predicate credDeposits≡dom-rwds cs asserts that these quantities are equal for cs.

The property credDeposits≡dom-rwds-inv asserts that credDeposits≡dom-rwds is a chain invariant. That is, if cs and cs' are two ChainStates such that cs ⇀⦇ tx ,CHAIN⦈ cs', then credDeposits≡dom-rwds cs only if credDeposits≡dom-rwds cs'.

Formally.

credDeposits≡dom-rwds : ChainState → Type
credDeposits≡dom-rwds cs =  filter isCredDeposit (dom (DepositsOf cs))
                            ≡ map CredentialDeposit (dom (RewardsOf cs))

credDeposits≡dom-rwds-inv : Type
credDeposits≡dom-rwds-inv = LedgerInvariant _⊢_⇀⦇_,CHAIN⦈_ credDeposits≡dom-rwds

Proof. (coming soon)