{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.MiniTrace where

import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..))
import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Governance (
  RatifySignal (..),
  VotingProcedures (..),
 )
import Cardano.Ledger.Conway.Rules (GovSignal (..))
import Cardano.Ledger.Core
import Constrained.API
import Control.State.Transition.Extended (STS (..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import qualified Data.OSet.Strict as OSet
import Data.Proxy
import Test.Cardano.Ledger.Common
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (..))
import Test.Cardano.Ledger.Generic.Proof (Proof (..), WitRule (..), goSTS)
import qualified Test.Cardano.Ledger.Generic.Proof as Proof

-- \| This is where most of the ExecSpecRule instances are defined
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
  nameCerts,
  nameDelegCert,
  nameEnact,
  nameEpoch,
  nameGovCert,
  namePoolCert,
  nameTxCert,
 )

-- ====================================================================

-- | Generate either a list of signals, or a list of error messages
minitraceEither ::
  forall s e.
  ( ExecSpecRule s e
  , ExecState s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Int ->
  Gen (Either [String] [Signal (EraRule s e)])
minitraceEither :: forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e -> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
minitraceEither WitRule s e
witrule Int
n0 = do
  ExecContext s e
ctxt <- forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Gen (ExecContext rule era)
genExecContext @s @e
  ExecEnvironment s e
env <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ExecEnvironment s e) (forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era -> Specification (ExecEnvironment rule era)
environmentSpec @s @e ExecContext s e
ctxt)
  let env2 :: Environment (EraRule s e)
      env2 :: Environment (EraRule s e)
env2 = forall t s. Inject t s => t -> s
inject ExecEnvironment s e
env
  !State (EraRule s e)
state0 <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ExecState s e) (forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> ExecEnvironment rule era -> Specification (ExecState rule era)
stateSpec @s @e ExecContext s e
ctxt ExecEnvironment s e
env)
  let go :: State (EraRule s e) -> Int -> Gen (Either [String] [Signal (EraRule s e)])
      go :: State (EraRule s e)
-> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
go State (EraRule s e)
_ Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right [])
      go State (EraRule s e)
state Int
n = do
        ExecSignal s e
signal <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ExecSignal s e) (forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
ExecContext rule era
-> ExecEnvironment rule era
-> ExecState rule era
-> Specification (ExecSignal rule era)
signalSpec @s @e ExecContext s e
ctxt ExecEnvironment s e
env State (EraRule s e)
state)
        let signal2 :: Signal (EraRule s e)
            signal2 :: Signal (EraRule s e)
signal2 = forall t s. Inject t s => t -> s
inject ExecSignal s e
signal
        forall (s :: Symbol) e ans env state sig.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e),
 env ~ Environment (EraRule s e), state ~ State (EraRule s e),
 sig ~ Signal (EraRule s e)) =>
WitRule s e
-> env
-> state
-> sig
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
goSTS @s @e @(Gen (Either [String] [Signal (EraRule s e)]))
          WitRule s e
witrule
          Environment (EraRule s e)
env2
          State (EraRule s e)
state
          Signal (EraRule s e)
signal2
          ( \Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
x -> case Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
x of
              Left NonEmpty (PredicateFailure (EraRule s e))
ps ->
                forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  ( forall a b. a -> Either a b
Left
                      ( [ [Char]
"\nSIGNAL = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA Signal (EraRule s e)
signal2)
                        , [Char]
"\nSTATE = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA State (EraRule s e)
state)
                        , [Char]
"\nPredicateFailures"
                        ]
                          forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty (PredicateFailure (EraRule s e))
ps)
                      )
                  )
              Right !State (EraRule s e)
state2 -> do
                Either [[Char]] [Signal (EraRule s e)]
ans <- State (EraRule s e)
-> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
go State (EraRule s e)
state2 (Int
n forall a. Num a => a -> a -> a
- Int
1)
                case Either [[Char]] [Signal (EraRule s e)]
ans of
                  Left [[Char]]
xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left [[Char]]
xs)
                  Right [Signal (EraRule s e)]
more -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall t s. Inject t s => t -> s
inject ExecSignal s e
signal forall a. a -> [a] -> [a]
: [Signal (EraRule s e)]
more))
          )
  State (EraRule s e)
-> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
go State (EraRule s e)
state0 Int
n0

minitrace ::
  forall s e.
  ( ExecSpecRule s e
  , ExecState s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Int ->
  Gen [Signal (EraRule s e)]
minitrace :: forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e -> Int -> Gen [Signal (EraRule s e)]
minitrace WitRule s e
witrule Int
n0 = do
  Either [[Char]] [Signal (EraRule s e)]
ans <- forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e -> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
minitraceEither @s @e WitRule s e
witrule Int
n0
  case Either [[Char]] [Signal (EraRule s e)]
ans of
    Left [[Char]]
zs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => [Char] -> a
error ([[Char]] -> [Char]
unlines [[Char]]
zs)
    Right [Signal (EraRule s e)]
zs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Signal (EraRule s e)]
zs

minitraceProp ::
  forall s e.
  ( ExecSpecRule s e
  , ExecState s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Int ->
  (Signal (EraRule s e) -> String) ->
  Gen Property
minitraceProp :: forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp WitRule s e
witrule Int
n0 Signal (EraRule s e) -> [Char]
namef = do
  Either [[Char]] [Signal (EraRule s e)]
ans <- forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e -> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
minitraceEither @s @e WitRule s e
witrule Int
n0
  case Either [[Char]] [Signal (EraRule s e)]
ans of
    Left [[Char]]
zs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([[Char]] -> [Char]
unlines [[Char]]
zs) (forall prop. Testable prop => prop -> Property
property Bool
False)
    Right [Signal (EraRule s e)]
sigs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x. (x -> [Char]) -> [x] -> Property -> Property
classifyFirst Signal (EraRule s e) -> [Char]
namef [Signal (EraRule s e)]
sigs forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True

-- =======================================================
-- Classifying what is in a trace requires a function that
-- lifts a Signal to a String
-- =======================================================

classifyMany :: (x -> String) -> [x] -> Property -> Property
classifyMany :: forall x. (x -> [Char]) -> [x] -> Property -> Property
classifyMany x -> [Char]
_ [] Property
p = Property
p
classifyMany x -> [Char]
f (x
x : [x]
xs) Property
p = forall x. (x -> [Char]) -> [x] -> Property -> Property
classifyMany x -> [Char]
f [x]
xs (forall prop. Testable prop => Bool -> [Char] -> prop -> Property
classify Bool
True (x -> [Char]
f x
x) Property
p)

classifyFirst :: (x -> String) -> [x] -> Property -> Property
classifyFirst :: forall x. (x -> [Char]) -> [x] -> Property -> Property
classifyFirst x -> [Char]
_ [] Property
p = Property
p
classifyFirst x -> [Char]
f (x
x : [x]
_) Property
p = forall prop. Testable prop => Bool -> [Char] -> prop -> Property
classify Bool
True (x -> [Char]
f x
x) Property
p

classifyFirst' :: (x -> Maybe String) -> [x] -> Property -> Property
classifyFirst' :: forall x. (x -> Maybe [Char]) -> [x] -> Property -> Property
classifyFirst' x -> Maybe [Char]
_ [] Property
p = Property
p
classifyFirst' x -> Maybe [Char]
f (x
x : [x]
_) Property
p = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Property
p (\[Char]
s -> forall prop. Testable prop => Bool -> [Char] -> prop -> Property
classify Bool
True [Char]
s Property
p) (x -> Maybe [Char]
f x
x)

nameRatify :: RatifySignal era -> String
nameRatify :: forall era. RatifySignal era -> [Char]
nameRatify (RatifySignal StrictSeq (GovActionState era)
xs) = forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length StrictSeq (GovActionState era)
xs) forall a. [a] -> [a] -> [a]
++ [Char]
" GovActionStates"

nameGovSignal :: GovSignal Proof.ConwayEra -> String
nameGovSignal :: GovSignal ConwayEra -> [Char]
nameGovSignal (GovSignal (VotingProcedures Map Voter (Map GovActionId (VotingProcedure ConwayEra))
m) OSet (ProposalProcedure ConwayEra)
os StrictSeq (TxCert ConwayEra)
cs) = forall a. Show a => a -> [Char]
show (forall k a. Map k a -> Int
Map.size Map Voter (Map GovActionId (VotingProcedure ConwayEra))
m) forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. OSet a -> Int
OSet.size OSet (ProposalProcedure ConwayEra)
os) forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length StrictSeq (TxCert ConwayEra)
cs)

nameAlonzoTx :: AlonzoTx era -> String
nameAlonzoTx :: forall era. AlonzoTx era -> [Char]
nameAlonzoTx (AlonzoTx TxBody era
_body TxWits era
_wits IsValid
isV StrictMaybe (TxAuxData era)
_auxdata) = forall a. Show a => a -> [Char]
show IsValid
isV

-- | Run a minitrace for every instance of ExecRuleSpec
spec :: Spec
spec :: Spec
spec = do
  forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe [Char]
"50 MiniTrace tests with trace length of 50" forall a b. (a -> b) -> a -> b
$ do
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
prop
      [Char]
"POOL"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "POOL" e
POOL Proof ConwayEra
Conway) Int
50 PoolCert -> [Char]
namePoolCert))
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
prop
      [Char]
"DELEG"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "DELEG" e
DELEG Proof ConwayEra
Conway) Int
50 ConwayDelegCert -> [Char]
nameDelegCert))
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
prop
      [Char]
"GOVCERT"
      ( forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess
          Int
50
          (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "GOVCERT" e
GOVCERT Proof ConwayEra
Conway) Int
50 ConwayGovCert -> [Char]
nameGovCert)
      )
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
prop
      [Char]
"CERT"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "CERT" e
CERT Proof ConwayEra
Conway) Int
50 ConwayTxCert ConwayEra -> [Char]
nameTxCert))
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
prop
      [Char]
"CERTS"
      ( forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess
          Int
50
          (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "CERTS" e
CERTS Proof ConwayEra
Conway) Int
50 Seq (ConwayTxCert ConwayEra) -> [Char]
nameCerts)
      )
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
prop
      [Char]
"RATIFY"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "RATIFY" e
RATIFY Proof ConwayEra
Conway) Int
50 forall era. RatifySignal era -> [Char]
nameRatify))
    -- prop "ENACT" (withMaxSuccess 50 (minitraceProp (ENACT Conway) (Proxy @ConwayFn) 50 nameEnact))
    -- These properties do not have working 'signalSpec' Specifications yet.
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
xprop
      [Char]
"GOV"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "GOV" e
GOV Proof ConwayEra
Conway) Int
50 GovSignal ConwayEra -> [Char]
nameGovSignal))
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
xprop
      [Char]
"UTXO"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "UTXO" e
UTXO Proof ConwayEra
Conway) Int
50 forall era. AlonzoTx era -> [Char]
nameAlonzoTx))
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
xprop
      [Char]
"EPOCH"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "EPOCH" e
EPOCH Proof ConwayEra
Conway) Int
50 EpochNo -> [Char]
nameEpoch))
    forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
xprop
      [Char]
"NEWEPOCH"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp (forall e. Proof e -> WitRule "NEWEPOCH" e
NEWEPOCH Proof ConwayEra
Conway) Int
50 EpochNo -> [Char]
nameEpoch))