GovDepsMatch

{-# OPTIONS --safe #-}

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

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

open import Ledger.Conway.Certs govStructure
open import Ledger.Conway.Chain txs abs
open import Ledger.Conway.Enact govStructure
open import Ledger.Conway.Epoch txs abs
open import Ledger.Conway.Epoch.Properties.GovDepsMatch txs abs
open import Ledger.Conway.Ledger txs abs
open import Ledger.Conway.Ledger.Properties txs abs
open import Ledger.Conway.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)

  - *Informally*. Fix a `Block`{.AgdaRecord} , a `ChainState`{.AgdaRecord} , and a `NewEpochState`{.AgdaRecord} . Let `csLState`{.AgdaFunction} be the ledger state of . Recall, a `ChainState`{.AgdaRecord} has just one field, `newEpochState`{.AgdaField} : `NewEpochState`{.AgdaRecord}. Consider the chain state `cs’`{.AgdaFunction} defined as follows:

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

That is `cs’`{.AgdaFunction} is essentially , but the `EpochState`{.AgdaRecord} field is set to the `epochState`{.AgdaField} of with the exception of the `LState`{.AgdaRecord} field, which is set to that of .  Let and be the respective `UTxOState`{.AgdaRecord}s of the ledger states of and `cs’`{.AgdaFunction}, respectively, and let and be their respective `GovState`{.AgdaFunction}s.  Assume the following conditions hold: - let `removed’`{.AgdaFunction} : `ℙ`{.AgdaFunction}(`GovActionID`{.AgdaDatatype} × `GovActionState`{.AgdaDatatype}) be the union of - the governance actions in the `removed`{.AgdaField} field of the ratify state of , and - the orphaned governance actions in the `GovState`{.AgdaFunction} of . Let $\mathcal{G}$ be the set $\{\mbox{\texttt{@@AgdaTerm@@basename=GovActionDeposit@@class=AgdaInductiveConstructor@@} \ab{id}} : \mbox{\ab{id}} ∈ \mbox{proj}₁ \mbox{\texttt{@@AgdaTerm@@basename=removed'@@class=AgdaFunction@@}}\}$. $\mathcal{G}$ is a subset of the set of deposits of the chain state ; that is, `map`{.AgdaFunction} (`GovActionDeposit`{.AgdaInductiveConstructor} $∘$ `proj₁`{.AgdaField}) `removed’`{.AgdaFunction} `@@AgdaTerm@@basename=`$⊆$`@@class=AgdaField@@` `dom`{.AgdaFunction} (`DepositsOf`{.AgdaField} ); - the total reference script size of `csLState`{.AgdaFunction} is not greater than the maximum allowed size per block (as specified in `PParams`{.AgdaRecord}); - `⇀⦇`{.AgdaDatatype} `,CHAIN⦈`{.AgdaDatatype} `cs’`{.AgdaFunction}. Under these conditions, if the governance action deposits of equal those of , then the same holds for and . In other terms, `govDepsMatch`{.AgdaFunction} `csLState`{.AgdaFunction} implies `govDepsMatch`{.AgdaFunction} `nesState`{.AgdaFunction}. - *Formally*.

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

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

  -- 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₂