CredDepsEqualDomRwds

{-# OPTIONS --safe #-}

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

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

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

- *Informally*. This property concerns two quantities associated with a given `ChainState`{.AgdaRecord} , - the credential deposits of the `UTxOState`{.AgdaRecord} of and - the credential deposits of the rewards in the ledger state of . The predicate `credDeposits≡dom-rwds`{.AgdaFunction} asserts that these quantities are equal for . Formally,

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

The property `credDeposits≡dom-rwds-inv`{.AgdaFunction} asserts that `credDeposits≡dom-rwds`{.AgdaFunction} is a chain invariant. That is, if and are two `ChainState`{.AgdaRecord}s such that `⇀⦇`{.AgdaDatatype} `,CHAIN⦈`{.AgdaDatatype} , then `credDeposits≡dom-rwds`{.AgdaFunction} only if `credDeposits≡dom-rwds`{.AgdaFunction} . - *Formally*.

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

- *Proof*. *To appear* (in the module of the [formal ledger repository](\repourl)).