MinSpend

{-# OPTIONS --safe #-}

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

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

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

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

module _
  where

Theorem (general spend lower bound).

Informally.

Let tx : Tx be a valid transaction and let txCerts be its list of DCerts. Denote by noRefundCert txCerts the assertion that no element in txCerts is one of the two refund types (i.e., an element of l is neither a dereg nor a deregdrep). Let s, s' : UTxOState be two UTxO states. If s ⇀⦇ tx ,UTXO⦈ s' and if noRefundCert txCerts, then the coin consumed by tx is at least the sum of the governance action deposits of the proposals in tx.

Formally.

module _
  -- ASSUMPTION --
  (gc-hom : (d₁ d₂ : DepositPurpose ⇀ Coin) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂)
  {Γ : UTxOEnv}
  where
    open module Γ = UTxOEnv Γ
    govActionDeps : Coin
    govActionDeps = PParams.govActionDeposit Γ.pparams

    utxoMinSpend : {tx : Tx} {s s' : UTxOState}
      → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
      → noRefundCert (DCertsOf tx)
      → coin (consumed _ s (TxBodyOf tx)) ≥ length (GovProposalsOf tx) * govActionDeps

Proof.

    utxoMinSpend step@(UTXO-inductive⋯ tx Γ utxoSt _ _ _ _ _ _ c≡p cmint≡0 _ _ _ _ _ _ _ _ _ _) nrf =
      begin
      length txGovProposals * govActionDeps
        ≡˘⟨ updatePropDeps≡ gc-hom txGovProposals ⟩
      getCoin (updateProposalDeposits txGovProposals txId (govActionDeps) deposits) ∸ getCoin deposits
        ≤⟨ ∸-monoˡ-≤ (getCoin deposits) (≤updateCertDeps gc-hom 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 (WithdrawalsOf tx)

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

Theorem (spend lower bound for proposals).

Preliminary remarks.

1. Define noRefundCert l and pp as in the "min spend" theorem above.

2. Given a ledger state ls and a transaction tx, denote by validTxIn₂ tx the assertion that there exists ledger state ls' such that ls ⇀⦇ tx ,LEDGER⦈ ls'.

3. Assume the following additive property of the ∪⁺ 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

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

Informally.

Let tx : Tx be a valid transaction and let cs : ChainState be a chain state. If the condition validTxIn₂ tx (described above) holds, then the coin consumed by tx is at least the sum of the governance action deposits of the proposals in tx.

Formally.

  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 txGovProposals * pp .govActionDeposit

Proof.

  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