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#577}{\htmlId{883}{\htmlClass{Generalizable}{\text{mark}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#582}{\htmlId{890}{\htmlClass{Generalizable}{\text{set}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#586}{\htmlId{896}{\htmlClass{Generalizable}{\text{go}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#602}{\htmlId{901}{\htmlClass{Generalizable}{\text{feeSS}}}}\, \end{pmatrix}$ ⇀⦇ tt ,SNAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Rewards.html#803}{\htmlId{924}{\htmlClass{Bound}{\text{stake}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#577}{\htmlId{932}{\htmlClass{Generalizable}{\text{mark}}}}\, \\ \,\href{Ledger.Conway.Conformance.Rewards.html#582}{\htmlId{939}{\htmlClass{Generalizable}{\text{set}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{945}{\htmlClass{Function}{\text{fees}}}}\, \end{pmatrix}$