Lib

{-# OPTIONS --safe #-}

open import Ledger.Prelude hiding (fromList; ε; _/_)
open import Test.LedgerImplementation using (SVTransactionStructure)
import Ledger.Conway.Specification.Script.ScriptPurpose as SP

module Test.Lib
  {T D : Set}{{DecEq-Data : DecEq D}}{{Show-Data : Show D}}
  (open SP (SVTransactionStructure T D) using (TxInfo; ScriptPurpose))
  (valContext' : TxInfo → ScriptPurpose → D)
  where

open import Test.AbstractImplementation valContext'
open import Test.LedgerImplementation T D
  renaming (SVTransactionStructure to SVTransactionStructure')
open import Ledger.Conway.Specification.Utxo SVTransactionStructure' SVAbstractFunctions
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)
open TransactionStructure SVTransactionStructure'
open import Ledger.Prelude.Numeric using (mkUnitInterval; mkℕ⁺)
open import Data.Integer using (ℤ; +_)
open import Data.Rational using (½; 1ℚ ; mkℚ+ ; _/_)
open import Data.Nat.Coprimality using (Coprime; gcd≡1⇒coprime)

createEnv : ℕ → UTxOEnv
createEnv s = record { slot = s ; treasury =  ;
                   pparams = record
                               { maxBlockSize = 
                               ; maxTxSize = 
                               ; maxHeaderSize = 
                               ; maxValSize = 
                               ; maxCollateralInputs = 
                               ; pv =  , 
                               ; maxTxExUnits =  , 
                               ; maxBlockExUnits =  , 
                               ; a = 
                               ; b = 
                               ; minUTxOValue = 
                               ; poolDeposit =  -- lovelace
                               ; keyDeposit =  -- lovelace
                               ; monetaryExpansion = mkUnitInterval (+  / )
                               ; treasuryCut = mkUnitInterval (+  / )
                               ; coinsPerUTxOByte =   --lovelace
                               -- ^^^ was 4310, but that value resulted in failed tests once
                               -- we replaced `minUTxOValue` with `coinsPerUTxOByte`; see `HelloWorld.agda`
                               -- line 153: `isSuccess succeedExample ≡ true`
                               ; minFeeRefScriptCoinsPerByte = mkℚ+   (gcd≡1⇒coprime refl) -- see [1]
                               ; prices = tt -- fix this
                               ; maxRefScriptSizePerTx =  *  -- 200KiB
                               ; maxRefScriptSizePerBlock =  *  -- 1MiB
                               ; refScriptCostStride  = mkℕ⁺ 
                               ; refScriptCostMultiplier = mkℚ+   (gcd≡1⇒coprime refl) -- see [1]
                               ; a0 = 1ℚ -- don't know
                               ; Emax = 
                               ; nopt =  -- don't know
                               ; collateralPercentage = 
                               ; costmdls = tt -- fix this
                               ; drepThresholds = record -- unknown so setting all to 50%
                                                    { P1 = ½
                                                    ; P2a = ½
                                                    ; P2b = ½
                                                    ; P3 = ½
                                                    ; P4 = ½
                                                    ; P5a = ½
                                                    ; P5b = ½
                                                    ; P5c = ½
                                                    ; P5d = ½
                                                    ; P6 = ½
                                                    }
                               ; poolThresholds = record
                                                    { Q1 = ½
                                                    ; Q2a = ½
                                                    ; Q2b = ½
                                                    ; Q4 = ½
                                                    ; Q5 = ½
                                                    }
                               ; govActionLifetime =  -- unknown
                               ; govActionDeposit =  -- unknown (set to 1 ada)
                               ; drepDeposit =  -- unknown (set to 1 ada)
                               ; drepActivity =  -- unknown
                               ; ccMinSize =  -- unknown
                               ; ccMaxTermLength =  -- unknown set to 1 year (73 epochs)
                               } }

createUTxO : (index : ℕ)
           → (wallet : ℕ)
           → (value : Value)
           → Maybe (D ⊎ DataHash)
           → TxIn × TxOut
createUTxO index wallet value d = (index , index)
                                , (inj₁ (record { net =  ; pay = KeyHashObj wallet ; stake = just (KeyHashObj wallet) })
                                  , value , d , nothing)

createInitUtxoState : (wallets : ℕ)
                    → (value : Value)
                    → List (TxIn × TxOut)
createInitUtxoState zero value = []
createInitUtxoState (suc wallet) value = createUTxO (suc wallet) (suc wallet) value nothing
                                         ∷ createInitUtxoState wallet value

fromList' : List (TxIn × TxOut) → UTxO
fromList' = fromListᵐ

fromListIx : List (Implementation.Ix × TxOut) → Implementation.Ix ⇀ TxOut
fromListIx = fromListᵐ

applyScript : (Maybe D → Maybe D → Bool) → List D → Bool
applyScript f [] = f nothing nothing
applyScript f (_ ∷ []) = f nothing nothing
applyScript f (redeemer ∷ valcontext ∷ []) = f nothing (just redeemer)
applyScript f (datum ∷ redeemer ∷ valcontext ∷ _) = f (just datum) (just redeemer)

notEmpty : ∀ {A : Type} → List A → Type
notEmpty [] = ⊥
notEmpty (x ∷ xs) = ⊤

isSuccess : ComputationResult String UTxOState → Bool
isSuccess (success x) = true
isSuccess (failure x) = false

applyScriptWithContext : (Maybe D → Maybe D → List D → Bool) → List D → Bool
applyScriptWithContext f [] = f nothing nothing []
applyScriptWithContext f (_ ∷ []) = f nothing nothing []
applyScriptWithContext f (redeemer ∷ valcontext ∷ []) = f nothing (just redeemer) []
applyScriptWithContext f (datum ∷ redeemer ∷ valcontext ∷ vs) = f (just datum) (just redeemer) (valcontext ∷ vs)

-- [1] https://github.com/IntersectMBO/cardano-ledger/blob/master/docs/adr/2024-08-14_009-refscripts-fee-change.md