{-# OPTIONS --safe #-}

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

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

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


scriptsCost : (pp : PParams) → ℕ → Coin
scriptsCost pp scriptSize
  = scriptsCostAux 0ℚ minFeeRefScriptCoinsPerByte scriptSize (<′-wellFounded scriptSize)
    where
    minFeeRefScriptCoinsPerByte refScriptCostMultiplier : ℚ
    minFeeRefScriptCoinsPerByte = PParams.minFeeRefScriptCoinsPerByte pp
    refScriptCostMultiplier = PParams.refScriptCostMultiplier pp

    refScriptCostStride : ℕ⁺
    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 >  → 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))