GovDepsMatch

{-# OPTIONS --safe #-}

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

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

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

module _
  {b   : Block }
  {nes : NewEpochState}
  {cs  : ChainState}
  where
  open Block b; open ChainState cs
  open NewEpochState
  open EPOCH-Body (EpochStateOf cs) renaming (epsLState to csLState)
  open EnactState ens using (pparams)
  pp = pparams .proj₁
  open PParams pp using (maxRefScriptSizePerBlock)

Theorem (govDepsMatch is invariant of CHAIN rule).

Informally.

Fix a Block b, a ChainState cs, and a NewEpochState nes. Let csLState be the ledger state of cs. Recall, a ChainState has just one field, newEpochState : NewEpochState. Consider the chain state cs' defined as follows:

  cs' : ChainState
  cs' .newEpochState =
    record { lastEpoch   = nes .lastEpoch
           ; epochState  = record (EpochStateOf cs) {ls = LStateOf nes}
           ; ru          = nes .ru }

That is cs' is essentially nes, but the EpochState field is set to the epochState of cs with the exception of the LState field, which is set to that of nes. Let utxoSt and utxoSt' be the respective UTxOStates of the ledger states of cs and cs', respectively, and let govSt and govSt' be their respective GovStates. Assume the following conditions hold:

Let removed' : ℙ(GovActionID × GovActionState) be the union of
- the governance actions in the removed field of the ratify state of eps, and
- the orphaned governance actions in the GovState of eps.
Let \(\mathcal{G}\) be the set \(\{\)GovActionDeposit id : id ∈ proj₁ removed'\(\}\).

\(\mathcal{G}\) is a subset of the set of deposits of the chain state cs; that is,

map (GovActionDeposit \(∘\) proj₁) removed' ⊆ dom (DepositsOf cs).
The total reference script size of csLState is not greater than the maximum allowed size per block (as specified in PParams).
cs ⇀⦇ b ,CHAIN⦈ cs'.

Under these conditions, if the governance action deposits of utxoSt equal those of govSt, then the same holds for utxoSt' and govSt'. In other terms,

govDepsMatch csLState implies govDepsMatch nesState.

Formally.

  CHAIN-govDepsMatch :
    map (GovActionDeposit ∘ proj₁) removed' ⊆ dom (DepositsOf cs)
    →  totalRefScriptsSize csLState ts ≤ maxRefScriptSizePerBlock
    →  _ ⊢ cs ⇀⦇ b ,CHAIN⦈ cs'
    →  govDepsMatch csLState → govDepsMatch (LStateOf nes)

Proof.

  CHAIN-govDepsMatch rrm rss (CHAIN (x , NEWEPOCH-New (_ , eps₁→eps₂) , ledgers)) =
    RTC-preserves-inv LEDGER-govDepsMatch ledgers
     ∘ EPOCH-PROPS.EPOCH-govDepsMatch rrm eps₁→eps₂

  CHAIN-govDepsMatch rrm rss (CHAIN (x , NEWEPOCH-Not-New _ , ledgers)) =
    RTC-preserves-inv LEDGER-govDepsMatch ledgers

  CHAIN-govDepsMatch rrm rss (CHAIN (x , NEWEPOCH-No-Reward-Update (_ , eps₁→eps₂) , ledgers)) =
    RTC-preserves-inv LEDGER-govDepsMatch ledgers
     ∘ EPOCH-PROPS.EPOCH-govDepsMatch rrm eps₁→eps₂