Skip to content

Fee Calculation

This section is part of the Ledger.Conway.Fees module of the formal ledger specification, where we define the functions used to compute the fees associated with reference scripts.

The function scriptsCost (Section 'Calculation of fees for reference scripts') calculates the fee for reference scripts in a transaction. It takes as input the total size of the reference scripts in bytes—which can be calculated using refScriptsSize (Section 'Functions used in UTxO rules, continued')—and uses a function (scriptsCostAux) that is piece-wise linear in the size, where the linear constant multiple grows with each refScriptCostStride bytes. In addition, scriptsCost depends on the following constants (which are bundled with the protocol parameters; see Section 'Protocol parameter definitions'):

  • refScriptCostMultiplier, a rational number, the growth factor or step multiplier that determines how much the price per byte increases after each increment;

  • refScriptCostStride, an integer, the size in bytes at which the price per byte grows linearly;

  • minFeeRefScriptCoinsPerByte, a rational number, the base fee or initial price per byte.

For background on this particular choice of fee calculation, see Kuleshevich24.

{-# OPTIONS --safe #-}

open import Ledger.Prelude hiding (_%_; _*_; ≤-trans; ∣_∣)
open import Ledger.Conway.Abstract
open import Ledger.Conway.Transaction

module Ledger.Conway.Fees
  (txs : _) (open TransactionStructure txs)
  where

open import Data.Rational using (0ℚ; ℚ; mkℚ+; _*_; floor)
open import Data.Rational.Literals using (number)
open import Ledger.Conway.Types.Numeric
open import Data.Nat.Induction using (<′-wellFounded)
open import Data.Nat.Properties using (<⇒<′; ≰⇒>; ∸-monoʳ-≤; +-monoʳ-≤; n≤1+n; m+[n∸m]≡n; ≤-reflexive; ≤-trans)
open import Data.Integer using (∣_∣)
open import Induction.WellFounded using (Acc; acc)
open import Agda.Builtin.FromNat using (Number)

open Number number renaming (fromNat to fromℕ)

Calculation of fees for reference scripts

scriptsCost : (pp : PParams) → ℕ → Coin
scriptsCost pp scriptSize
  = scriptsCostAux 0ℚ minFeeRefScriptCoinsPerByte scriptSize

                  (<′-wellFounded scriptSize)

  where
    minFeeRefScriptCoinsPerByte = PParams.minFeeRefScriptCoinsPerByte pp
    refScriptCostMultiplier = PParams.refScriptCostMultiplier pp
    refScriptCostStride = PParams.refScriptCostStride pp
    scriptsCostAux : ℚ        -- accumulator
                   → ℚ        -- current tier price
                   → (n : ℕ)  -- remaining script size

                   → Acc _<′_ n

                   → Coin
    scriptsCostAux acl curTierPrice n

       (acc rs)

       = case  n ≤? fromℕ⁺ refScriptCostStride of

                λ where

                (yes _)  → ∣ floor (acl + (fromℕ n * curTierPrice)) ∣
                (no  p)  → scriptsCostAux
                             (acl + (fromℕ (fromℕ⁺ refScriptCostStride) * curTierPrice))
                             (refScriptCostMultiplier * curTierPrice)
                             (n - fromℕ⁺ refScriptCostStride)

                             (rs $ <⇒<′ (suc∸≤ (≤-trans (s<s z≤n) (≰⇒> p)) (ℕ⁺->0 refScriptCostStride)))

      where
        suc∸≤ : ∀ {n m : ℕ} → n > 0 → m > 0 → n ∸ m < n
        suc∸≤ {n} {.suc m} p (s≤s q) = ≤-trans (+-monoʳ-≤ 1 (∸-monoʳ-≤ n (s<s q)))
                                               (≤-reflexive (m+[n∸m]≡n p))

References

[Kuleshevich24] Alexey Kuleshevich. Changes to the fee calculation due to Reference Scripts. 2024.