{-# OPTIONS --safe #-}

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

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

open import Data.Rational using (0ℚ; ℚ; mkℚ+; _*_; floor)
open import Data.Rational.Literals using (number)
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ℕ)


scriptsCost : (pp : PParams) → ℕ → Coin
scriptsCost pp scriptSize


  with (PParams.refScriptCostStride pp)
... |  =   -- This case should never occur; refScriptCostStride should always be > 0.
... | suc m


  = scriptsCostAux 0ℚ minFeeRefScriptCoinsPerByte scriptSize


                  (<′-wellFounded scriptSize)


  where
    open PParams pp hiding (refScriptCostStride)
    refScriptCostStride = suc m


    scriptsCostAux : ℚ        -- accumulator
                   → ℚ        -- current tier price
                   → (n : ℕ)  -- remaining script size


                   → Acc _<′_ n


                   → Coin
    scriptsCostAux acl curTierPrice n


      (acc rs)


        = case n ≤? refScriptCostStride of λ where
            (yes _)  → ∣ floor (acl + (fromℕ n * curTierPrice)) ∣
            (no  p)  → scriptsCostAux (acl + (fromℕ refScriptCostStride * curTierPrice))
                                      (refScriptCostMultiplier * curTierPrice)
                                      (n - refScriptCostStride)


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


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