{-# 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#569}{\htmlId{875}{\htmlClass{Generalizable}{\text{mark}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#574}{\htmlId{882}{\htmlClass{Generalizable}{\text{set}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#578}{\htmlId{888}{\htmlClass{Generalizable}{\text{go}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#594}{\htmlId{893}{\htmlClass{Generalizable}{\text{feeSS}}}}\, \end{pmatrix}$ ⇀⦇ tt ,SNAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Rewards.html#795}{\htmlId{916}{\htmlClass{Bound}{\text{stake}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#569}{\htmlId{924}{\htmlClass{Generalizable}{\text{mark}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#574}{\htmlId{931}{\htmlClass{Generalizable}{\text{set}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#1316}{\htmlId{937}{\htmlClass{Function}{\text{fees}}}}\, \end{pmatrix}$