MinSpend

{-# OPTIONS --safe #-}

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

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

open import Ledger.Conway.Certs govStructure
open import Ledger.Conway.Chain txs abs
open import Ledger.Conway.Enact govStructure
open import Ledger.Conway.Epoch txs abs
open import Ledger.Conway.Ledger txs abs
open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All)
open import Ledger.Conway.Properties txs abs using (validTxIn₂)
open import Ledger.Conway.Utxo txs abs

open import Data.List.Relation.Unary.All  using (All)
open import Data.Nat.Properties           hiding (_≟_)

isRefundCert : DCert → Bool
isRefundCert (dereg c _) = true
isRefundCert (deregdrep c _) = true
isRefundCert _ = false

noRefundCert : List DCert → Type _
noRefundCert l = All (λ cert → isRefundCert cert ≡ false) l

opaque
  unfolding List-Model
  unfolding finiteness
  fin∘list[] : {A : Type} → proj₁ (finiteness{A = A} ∅) ≡ []
  fin∘list[] = refl
  fin∘list∷[] : {A : Type} {a : A} → proj₁ (finiteness ❴ a ❵) ≡ [ a ]
  fin∘list∷[] = refl

coin∅ : getCoin{A = DepositPurpose ⇀ Coin} ∅ ≡ 
coin∅ = begin
  foldr (λ x → (proj₂ x) +_)  (deduplicate _≟_ (proj₁ (finiteness ∅)))
    ≡⟨ cong (λ u → (foldr (λ x → (proj₂ x) +_)  (deduplicate _≟_ u))) fin∘list[] ⟩
  foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_)  (deduplicate _≟_ [])
    ≡⟨ cong (λ u → (foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_)   u))
            {x = deduplicate _≟_ []} {y = []} refl ⟩
  foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_)  []
    ≡⟨ refl ⟩
   ∎
  where open ≡-Reasoning

getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c
getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _)

module _ -- ASSUMPTION --
         (gc-hom : (d₁ d₂ : DepositPurpose ⇀ Coin) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂)
  where

  ∪⁺singleton≡ : {deps : DepositPurpose ⇀ Coin} {(dp , c) : DepositPurpose × Coin}
                 → getCoin (deps ∪⁺ ❴ (dp , c) ❵ᵐ) ≡ getCoin deps + c
  ∪⁺singleton≡ {deps} {(dp , c)} = begin
    getCoin (deps ∪⁺ ❴ (dp , c) ❵)
      ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩
    getCoin deps + getCoin{A = DepositPurpose ⇀ Coin} ❴ (dp , c) ❵
      ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩
    getCoin deps + c
      ∎
    where open ≡-Reasoning

  module _ {deposits : DepositPurpose ⇀ Coin} {txid : TxId} {gaDep : Coin} where

    ≤updatePropDeps : (props : List GovProposal)
      → getCoin deposits ≤ getCoin (updateProposalDeposits props txid gaDep deposits)
    ≤updatePropDeps [] = ≤-reflexive refl
    ≤updatePropDeps (x ∷ props) = ≤-trans (≤updatePropDeps props)
                                          (≤-trans (m≤m+n _ _)
                                                   (≤-reflexive $ sym $ ∪⁺singleton≡))
    updatePropDeps≡ : (ps : List GovProposal)
      → getCoin (updateProposalDeposits ps txid gaDep deposits) - getCoin deposits ≡ (length ps) * gaDep
    updatePropDeps≡ [] = n∸n≡0 (getCoin deposits)
    updatePropDeps≡ (_ ∷ ps) = let
      upD = updateProposalDeposits ps txid gaDep deposits in
      begin
        getCoin (upD ∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵ᵐ) ∸ getCoin deposits
          ≡⟨ cong (_∸ getCoin deposits) ∪⁺singleton≡ ⟩
        getCoin upD + gaDep ∸ getCoin deposits
          ≡⟨ +-∸-comm _ (≤updatePropDeps ps) ⟩
        (getCoin upD ∸ getCoin deposits) + gaDep
          ≡⟨ cong (_+ gaDep) (updatePropDeps≡ ps) ⟩
        (length ps) * gaDep + gaDep
          ≡⟨ +-comm ((length ps) * gaDep) gaDep ⟩
        gaDep + (length ps) * gaDep
          ∎
        where open ≡-Reasoning

  ≤certDeps  :  {d : DepositPurpose ⇀ Coin} {(dp , c) : DepositPurpose × Coin}
             →  getCoin d ≤ getCoin (d ∪⁺ ❴ (dp , c) ❵)

  ≤certDeps {d} = begin
    getCoin d                      ≤⟨ m≤m+n (getCoin d) _ ⟩
    getCoin d + _                  ≡⟨ sym ∪⁺singleton≡ ⟩
    getCoin (d ∪⁺ ❴ _ ❵)           ∎
    where open ≤-Reasoning


  ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits :  DepositPurpose ⇀ Coin}
    → noRefundCert cs
    → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits)
  ≤updateCertDeps [] nrf = ≤-reflexive refl
  ≤updateCertDeps (reg c v ∷ cs) {pp} {deposits} (_ All.∷ nrf) =
    ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵} nrf)
  ≤updateCertDeps (delegate c _ _ v ∷ cs) {pp} {deposits} (_ All.∷ nrf) =
    ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , v ❵} nrf)
  ≤updateCertDeps (regpool _ _ ∷ cs)       (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf)
  ≤updateCertDeps (retirepool _ _ ∷ cs)    (_ All.∷ nrf) = ≤updateCertDeps cs nrf
  ≤updateCertDeps (regdrep _ _ _ ∷ cs)     (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf)
  ≤updateCertDeps (ccreghot _ _ ∷ cs)      (_ All.∷ nrf) = ≤updateCertDeps cs nrf

  - *Informally*. Let : `Tx`{.AgdaRecord} be a valid transaction and let `txcerts`{.AgdaFunction} be its list of `DCert`{.AgdaDatatype}s. Denote by `noRefundCert`{.AgdaFunction} `txcerts`{.AgdaFunction} the assertion that no element in `txcerts`{.AgdaFunction} is one of the two refund types (i.e., an element of is neither a `dereg`{.AgdaInductiveConstructor} nor a `deregdrep`{.AgdaInductiveConstructor}).  Let , : `UTxOState`{.AgdaRecord} be two UTxO states. If `⇀⦇`{.AgdaDatatype} `,UTXO⦈`{.AgdaDatatype} and if `noRefundCert`{.AgdaFunction} `txcerts`{.AgdaFunction}, then the coin consumed by is at least the sum of the governance action deposits of the proposals in . - *Formally*.

  utxoMinSpend : {Γ : UTxOEnv} {tx : Tx} {s s' : UTxOState}
    → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
    → noRefundCert (txcertsOf tx)
    → coin (consumed _ s (TxBodyOf tx)) ≥ length (txpropOf tx) * govActionDepositOf Γ

- *Proof*. See the module in the [formal ledger repository](\repourl).

  utxoMinSpend step@(UTXO-inductive⋯ tx Γ utxoSt _ _ _ _ _ _ c≡p cmint≡0 _ _ _ _ _ _ _ _ _ _) nrf =
    begin
    length txprop * govActionDepositOf Γ
      ≡˘⟨ updatePropDeps≡ txprop ⟩
    getCoin (updateProposalDeposits txprop txid (govActionDepositOf Γ) deposits) ∸ getCoin deposits
      ≤⟨ ∸-monoˡ-≤ (getCoin deposits) (≤updateCertDeps txcerts nrf) ⟩
    getCoin (updateDeposits (PParamsOf Γ) txb deposits) - getCoin deposits
      ≡⟨ ∸≡posPart⊖ {getCoin (updateDeposits (PParamsOf Γ) txb deposits)} {getCoin deposits} ⟩
    newDeps
      ≤⟨ m≤n+m newDeps (coin balOut + txfee + txdonation) ⟩
    coin balOut + txfee + txdonation + newDeps
      ≡⟨ +-assoc (coin balOut + txfee) txdonation newDeps ⟩
    coin balOut + txfee + (txdonation + newDeps)
      ≡⟨ cong (coin balOut + txfee +_) (+-comm txdonation newDeps) ⟩
    coin balOut + txfee + (newDeps + txdonation)
      ≡˘⟨ +-assoc (coin balOut + txfee) newDeps txdonation ⟩
    coin balOut + txfee + newDeps + txdonation
      ≡˘⟨ cong (λ x → x + newDeps + txdonation) coin-inject-lemma ⟩
    coin (balOut + inject txfee) + newDeps + txdonation
      ≡˘⟨ cong (_+ txdonation) coin-inject-lemma ⟩
    coin (balOut + inject txfee + inject newDeps) + txdonation
      ≡˘⟨ coin-inject-lemma ⟩
    coin (balOut + inject txfee + inject newDeps + inject txdonation)
      ≡˘⟨ cong coin c≡p ⟩
    coin (balIn + mint + inject refunds + inject wdrls) ∎
    where
    open ≤-Reasoning
    open Tx tx renaming (body to txb); open TxBody txb
    open UTxOState utxoSt

    newDeps refunds wdrls : Coin
    newDeps = newDeposits (PParamsOf Γ) utxoSt txb
    refunds = depositRefunds (PParamsOf Γ) utxoSt txb
    wdrls = getCoin (wdrlsOf tx)

    balIn balOut : Value
    balIn = balance (utxo ∣ txins)
    balOut = balance (outs txb)

  - *Preliminary remarks*. 1. Define `noRefundCert`{.AgdaFunction} and as in *'thm:minspend' (unresolved reference)*. 2. Given a ledger state and a transaction , denote by `validTxIn₂`{.AgdaFunction} the assertion that there exists ledger state such that `⇀⦇`{.AgdaDatatype} `,LEDGER⦈`{.AgdaDatatype} . 3. Assume the following additive property of the `∪⁺`{.AgdaFunction} operator holds:

module _
    ( indexedSum-∪⁺-hom :  {A V : Type}
                           ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq V ⦄
                           ⦃ _ : CommutativeMonoid 0ℓ 0ℓ V ⦄
                           (d₁ d₂ : A ⇀ V)
       →

                           ∑[ x ← d₁ ∪⁺ d₂ ] x ≡ ∑[ x ← d₁ ] x ◇ ∑[ x ← d₂ ] x

    )

- *Informally*. Let : `Tx`{.AgdaRecord} be a valid transaction and let : `ChainState`{.AgdaRecord} be a chain state. If the condition `validTxIn₂`{.AgdaFunction} (described above) holds, then the coin consumed by is at least the sum of the governance action deposits of the proposals in . - *Formally*.

  where
  open import Ledger.Conway.Utxow txs abs
  open ChainState; open NewEpochState; open EpochState
  open LState; open EnactState;  open PParams

  propose-minSpend :  {slot : Slot} {tx : Tx} {cs : ChainState}
                      ( let  pp      = PParamsOf cs
                             utxoSt  = UTxOStateOf cs )

    ( open Tx tx )
    ( open TxBody body )

    → noRefundCert txcerts
    → validTxIn₂ cs slot tx
    → coin (consumed pp utxoSt body) ≥ length txprop * pp .govActionDeposit

- *Proof*. See the module in the [formal ledger repository](\repourl).

  propose-minSpend noRef valid = case valid of λ where
    (_ , LEDGER-V (_ , UTXOW⇒UTXO x , _ , _)) → utxoMinSpend indexedSum-∪⁺-hom x noRef
    (_ , LEDGER-I (_ , UTXOW⇒UTXO x))         → utxoMinSpend indexedSum-∪⁺-hom x noRef