Rewards

{-# OPTIONS --safe #-}

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

module Ledger.Conway.Conformance.Rewards
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs)
  where

open import Ledger.Prelude

open import Ledger.Conway.Conformance.Certs govStructure
open import Ledger.Conway.Conformance.Ledger txs abs
open import Ledger.Conway.Conformance.Utxo txs abs

open import Ledger.Conway.Specification.Rewards txs abs
  hiding (_⊢_⇀⦇_,SNAP⦈_) public

private variable
  lstate : LState
  mark set go : Snapshot
  feeSS : Coin

data _⊢_⇀⦇_,SNAP⦈_ : LState → Snapshots → ⊤ → Snapshots → Type where
  SNAP : let open LState lstate
             open UTxOState utxoSt
             open CertState certState
             stake = stakeDistr utxo (record { DState dState }) pState
    in
    lstate ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Rewards.html#664}{\htmlId{970}{\htmlClass{Generalizable}{\text{mark}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#669}{\htmlId{977}{\htmlClass{Generalizable}{\text{set}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#673}{\htmlId{983}{\htmlClass{Generalizable}{\text{go}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#689}{\htmlId{988}{\htmlClass{Generalizable}{\text{feeSS}}}}\, \end{pmatrix}$ ⇀⦇ tt ,SNAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Rewards.html#890}{\htmlId{1011}{\htmlClass{Bound}{\text{stake}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#664}{\htmlId{1019}{\htmlClass{Generalizable}{\text{mark}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#669}{\htmlId{1026}{\htmlClass{Generalizable}{\text{set}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{1032}{\htmlClass{Function}{\text{fees}}}}\, \end{pmatrix}$