{-# LANGUAGE OverloadedStrings #-}

module Main (
  main,
)
where

import Test.Byron.Spec.Ledger.AbstractSize.Properties (testProperty, testTxHasTypeReps)
import qualified Test.Byron.Spec.Ledger.Core.Generators.Properties as CoreGen
import Test.Byron.Spec.Ledger.Delegation.Examples (deleg)
import qualified Test.Byron.Spec.Ledger.Delegation.Properties as DELEG
import Test.Byron.Spec.Ledger.Relation.Properties (testRelation)
import Test.Byron.Spec.Ledger.UTxO.Properties (moneyIsConstant)
import qualified Test.Byron.Spec.Ledger.UTxO.Properties as UTxO
import Test.Byron.Spec.Ledger.Update.Examples (upiendExamples)
import qualified Test.Byron.Spec.Ledger.Update.Properties as UPDATE
import Test.Tasty (TestTree, defaultMain, localOption, testGroup)
import Test.Tasty.Ingredients.ConsoleReporter (UseColor (Auto))

main :: IO ()
IO ()
main = TestTree -> IO ()
defaultMain TestTree
tests
  where
    tests :: TestTree
    tests :: TestTree
tests =
      forall v. IsOption v => v -> TestTree -> TestTree
localOption UseColor
Auto forall a b. (a -> b) -> a -> b
$
        TestName -> [TestTree] -> TestTree
testGroup
          TestName
"Test.Byron.Spec.Ledger"
          [ TestName -> [TestTree] -> TestTree
testGroup
              TestName
"Core generators properties"
              [TestName -> Property -> TestTree
testProperty TestName
"Relevant k values are generated" Property
CoreGen.relevantKValuesAreGenerated]
          , TestName -> [TestTree] -> TestTree
testGroup TestName
"Delegation Examples" [TestTree]
deleg
          , TestName -> [TestTree] -> TestTree
testGroup
              TestName
"Delegation properties"
              [ TestName -> Property -> TestTree
testProperty TestName
"Certificates are triggered" Property
DELEG.dcertsAreTriggered
              , TestName -> Property -> TestTree
testProperty TestName
"DBLOCK Traces are classified" Property
DELEG.dblockTracesAreClassified
              , TestName -> Property -> TestTree
testProperty TestName
"Relevant DBLOCK traces covered" Property
DELEG.relevantCasesAreCovered
              , TestName -> Property -> TestTree
testProperty TestName
"Duplicated certificates are rejected" Property
DELEG.rejectDupSchedDelegs
              , TestName -> Property -> TestTree
testProperty TestName
"Traces are classified" Property
DELEG.tracesAreClassified
              , TestName -> Property -> TestTree
testProperty TestName
"Only valid DBLOCK signals are generated" Property
DELEG.onlyValidSignalsAreGenerated
              ]
          , TestName -> [TestTree] -> TestTree
testGroup
              TestName
"UTxO properties"
              [ TestName -> Property -> TestTree
testProperty TestName
"Money is constant" Property
moneyIsConstant
              , TestName -> Property -> TestTree
testProperty TestName
"Relevant UTxO traces are generated" Property
UTxO.relevantCasesAreCovered
              , TestName -> Property -> TestTree
testProperty TestName
"No double spending" Property
UTxO.noDoubleSpending
              , TestName -> Property -> TestTree
testProperty TestName
"UTxO is outputs minus inputs" Property
UTxO.utxoDiff
              , TestName -> Property -> TestTree
testProperty TestName
"UTxO and txouts are disjoint" Property
UTxO.utxoAndTxoutsMustBeDisjoint
              ]
          , TestTree
testTxHasTypeReps
          , TestName -> [TestTree] -> TestTree
testGroup TestName
"Update examples" [TestTree]
upiendExamples
          , TestName -> [TestTree] -> TestTree
testGroup
              TestName
"Update properties"
              [ TestName -> Property -> TestTree
testProperty TestName
"UPIREG traces are classified" Property
UPDATE.upiregTracesAreClassified
              , TestName -> Property -> TestTree
testProperty TestName
"UBLOCK traces are classified" Property
UPDATE.ublockTraceLengthsAreClassified
              , TestName -> Property -> TestTree
testProperty TestName
"Relevant UPIREG traces are covered" Property
UPDATE.upiregRelevantTracesAreCovered
              , TestName -> Property -> TestTree
testProperty TestName
"Only valid UPIREG signals are generated" Property
UPDATE.onlyValidSignalsAreGenerated
              , TestName -> Property -> TestTree
testProperty TestName
"Only valid UBLOCK signals are generated" HasCallStack => Property
UPDATE.ublockOnlyValidSignalsAreGenerated
              , TestName -> Property -> TestTree
testProperty TestName
"Relevant UBLOCK traces are covered" Property
UPDATE.ublockRelevantTracesAreCovered
              ]
          , -- TODO move this out of here (these are not properties of the transition
            -- systems) and also move the Relation class and instances out of Byron.Spec.Ledger.Core
            TestTree
testRelation
          ]