{-# 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.Base txs abs
open import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch txs abs
open import Ledger.Prelude hiding (map) renaming (mapˢ to map)
open import Ledger.Conway.Specification.RewardUpdate txs abs

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)


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


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


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

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

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