Ledger

{-# OPTIONS --safe #-}

import Data.List as L

open import Ledger.Prelude
open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)

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

open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Conformance.Gov txs abs
open import Ledger.Conway.Conformance.Utxo txs abs
open import Ledger.Conway.Conformance.Utxow txs abs
open import Ledger.Conway.Conformance.Certs govStructure

open import Ledger.Conway.Specification.Ledger txs abs public
  using (LEnv; HasCast-LEnv; allColdCreds; rmOrphanDRepVotes; txgov)

open Tx

record LState : Type where
  constructor ⟦_,_,_⟧ˡ
  field
    utxoSt     : UTxOState
    govSt      : GovState
    certState  : CertState

instance
  unquoteDecl HasCast-LState = derive-HasCast
    [ (quote LState , HasCast-LState) ]

private variable
  Γ : LEnv
  s s' s'' : LState
  utxoSt' : UTxOState
  govSt' : GovState
  certState' : CertState
  tx : Tx

open UTxOState

data

  _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type

  where

  LEDGER-V :
    let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ
        open CertState certState; open DState dState
        utxoSt'' = record utxoSt' { deposits = updateDeposits pparams txb (deposits utxoSt') }
     in
    ∙  isValid tx ≡ true
    ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
    ∙  $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{1644}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1064}{\htmlId{1650}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1122}{\htmlId{1657}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#5247}{\htmlId{1667}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#5072}{\htmlId{1680}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#3680}{\htmlId{1696}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Conway.Conformance.Ledger.html#958}{\htmlId{1709}{\htmlClass{Function}{\text{govSt}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1148}{\htmlId{1715}{\htmlClass{Function}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
    ∙  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Transaction.html#4964}{\htmlId{1779}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{1786}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1064}{\htmlId{1792}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1122}{\htmlId{1799}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1087}{\htmlId{1809}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#1148}{\htmlId{1819}{\htmlClass{Function}{\text{enactState}}}}\, \\  \,\href{Ledger.Conway.Conformance.Ledger.html#1196}{\htmlId{1833}{\htmlClass{Generalizable}{\text{certState'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{1846}{\htmlClass{Function}{\text{dom}}}}\,
    \,\href{Ledger.Conway.Conformance.Certs.html#811}{\htmlId{1854}{\htmlClass{Function}{\text{rewards}}}}\, \end{pmatrix}$ ⊢ govSt ⇀⦇ txgov txb ,GOVS⦈ govSt'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Ledger.html#1459}{\htmlId{1969}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#1176}{\htmlId{1980}{\htmlClass{Generalizable}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#1196}{\htmlId{1989}{\htmlClass{Generalizable}{\text{certState'}}}}\, \end{pmatrix}$


  LEDGER-I : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in
    ∙  isValid tx ≡ false
    ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Ledger.html#1154}{\htmlId{2236}{\htmlClass{Generalizable}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#958}{\htmlId{2246}{\htmlClass{Function}{\text{govSt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#984}{\htmlId{2254}{\htmlClass{Function}{\text{certState}}}}\, \end{pmatrix}$

pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
pattern LEDGER-I⋯ y z     = LEDGER-I (y , z)

_⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}