{-# OPTIONS --safe #-}

open import Algebra              using (CommutativeMonoid)
open import Data.Nat.Properties  using (+-0-monoid)
import Data.Maybe as M
import Data.Sum.Relation.Unary.All as Sum

import Data.Integer as 
import Data.Rational as 


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

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

open import Ledger.Conway.Specification.Script.Validation txs abs
open import Ledger.Conway.Specification.Fees txs using (scriptsCost)
open import Ledger.Conway.Conformance.Certs govStructure

private
  module L where
    open import Ledger.Conway.Specification.Utxo txs abs public

open PParams

instance
  _ = +-0-monoid

open L public using (UTxOEnv; UTxOState; ⟦_,_,_,_⟧ᵘ; HasCast-UTxOState; updateDeposits
                    ; cbalance; balance; depositRefunds; consumed
                    ; produced; outs; newDeposits; refScriptsSize )

private variable
  Γ : UTxOEnv
  s s' : UTxOState
  tx : Tx

open PParams

data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv  UTxOState  Tx  UTxOState  Type where
  Scripts-Yes :
     {Γ} {s} {tx}
     let open Tx tx renaming (body to txb); open TxBody txb
          open UTxOEnv Γ renaming (pparams to pp)
          open UTxOState s
          p2Scripts = collectP2ScriptsWithContext pp tx utxo
      in
         evalP2Scripts p2Scripts  isValid
         isValid  true
          ────────────────────────────────
          Γ  s ⇀⦇ tx ,UTXOS⦈  $\begin{pmatrix} \,\htmlId{1617}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1294}{\htmlId{1618}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{1623}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3034}{\htmlId{1625}{\htmlClass{Function}{\text{txIns}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{1631}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{1632}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{1634}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\htmlId{1637}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#2296}{\htmlId{1638}{\htmlClass{Function}{\text{L.outs}}}}\, \,\href{Ledger.Conway.Conformance.Utxo.html#1303}{\htmlId{1645}{\htmlClass{Field}{\text{txb}}}}\,\,\htmlId{1648}{\htmlClass{Symbol}{\text{)}}}\,
                              \\ \,\href{Ledger.Conway.Specification.Utxo.html#1316}{\htmlId{1682}{\htmlClass{Function}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1687}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3256}{\htmlId{1689}{\htmlClass{Function}{\text{txFee}}}}\,
                              \\ \,\href{Ledger.Conway.Specification.Utxo.html#1338}{\htmlId{1727}{\htmlClass{Function}{\text{deposits}}}}\,
                              \\ \,\href{Ledger.Conway.Specification.Utxo.html#1364}{\htmlId{1768}{\htmlClass{Function}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1778}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3426}{\htmlId{1780}{\htmlClass{Function}{\text{txDonation}}}}\,
                              \end{pmatrix}$

  Scripts-No :
     {Γ} {s} {tx}
     let open Tx tx renaming (body to txb); open TxBody txb
          open UTxOEnv Γ renaming (pparams to pp)
          open UTxOState s
          p2Scripts = collectP2ScriptsWithContext pp tx utxo
      in
         evalP2Scripts p2Scripts  isValid
         isValid  false
          ────────────────────────────────
          Γ  s ⇀⦇ tx ,UTXOS⦈  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#1294}{\htmlId{2212}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2217}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3106}{\htmlId{2219}{\htmlClass{Function}{\text{collateralInputs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2236}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
                              \\ \,\href{Ledger.Conway.Specification.Utxo.html#1316}{\htmlId{2270}{\htmlClass{Function}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2275}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#2456}{\htmlId{2277}{\htmlClass{Function}{\text{L.cbalance}}}}\, \,\htmlId{2288}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1294}{\htmlId{2289}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{2294}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3106}{\htmlId{2296}{\htmlClass{Function}{\text{collateralInputs}}}}\,\,\htmlId{2312}{\htmlClass{Symbol}{\text{)}}}\,
                              \\ \,\href{Ledger.Conway.Specification.Utxo.html#1338}{\htmlId{2346}{\htmlClass{Function}{\text{deposits}}}}\,
                              \\ \,\href{Ledger.Conway.Specification.Utxo.html#1364}{\htmlId{2387}{\htmlClass{Function}{\text{donations}}}}\,
                              \end{pmatrix}$

unquoteDecl Scripts-Yes-premises = genPremises Scripts-Yes-premises (quote Scripts-Yes)
unquoteDecl Scripts-No-premises  = genPremises Scripts-No-premises  (quote Scripts-No)

data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv  UTxOState  Tx  UTxOState  Type where

  UTXO-inductive :
    let open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits
        open UTxOEnv Γ renaming (pparams to pp)
        open UTxOState s
        txOutsʰ = (mapValues txOutHash txOuts)
        overhead = 160
    in
     txIns                                 txIns  refInputs  dom utxo
     txIns  refInputs                     L.inInterval slot txVldt
     L.minfee pp utxo tx  txFee             (txrdmrs ˢ    L.collateralCheck pp tx utxo)
     consumed pp s txb  produced pp s txb   coin mint  0
     txsize  maxTxSize pp
     L.refScriptsSize utxo tx  pp .maxRefScriptSizePerTx

     ∀[ (_ , txout)   txOutsʰ  ]
        inject ((overhead + L.utxoEntrySize txout) * coinsPerUTxOByte pp) ≤ᵗ getValueʰ txout
     ∀[ (_ , txout)   txOutsʰ  ]
        serSize (getValueʰ txout)  maxValSize pp
     ∀[ (a , _)  range txOutsʰ ]
        Sum.All (const )  a  a .BootstrapAddr.attrsSize  64) a
     ∀[ (a , _)  range txOutsʰ ]  netId a          NetworkId
     ∀[ a  dom txWithdrawals ]    NetworkIdOf a    NetworkId
     txNetworkId ~ just NetworkId
     currentTreasury ~ just treasury
     Γ  s ⇀⦇ tx ,UTXOS⦈ s'
      ────────────────────────────────
      Γ  s ⇀⦇ tx ,UTXO⦈ s'

pattern UTXO-inductive⋯ tx Γ s x y z w k l m c v j n o p q r t u h
      = UTXO-inductive {tx}{Γ}{s} (x , y , z , w , k , l , m , c , v , j , n , o , p , q , r , t , u , h)
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)