{-# 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)



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


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