{-# 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 hiding (inject)
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.Constrained.Conway.Instances (ConwayFn)
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 fn s e.
  ( ExecSpecRule fn s e
  , ExecState fn s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Proxy fn ->
  Int ->
  Gen (Either [String] [Signal (EraRule s e)])
minitraceEither :: forall (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy fn -> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
minitraceEither WitRule s e
witrule Proxy fn
Proxy Int
n0 = do
  ExecContext fn s e
ctxt <- forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Gen (ExecContext fn rule era)
genExecContext @fn @s @e
  ExecEnvironment fn s e
env <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn @(ExecEnvironment fn s e) (forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> Specification fn (ExecEnvironment fn rule era)
environmentSpec @fn @s @e ExecContext fn 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 fn s e
env
  !State (EraRule s e)
state0 <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn @(ExecState fn s e) (forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> Specification fn (ExecState fn rule era)
stateSpec @fn @s @e ExecContext fn s e
ctxt ExecEnvironment fn 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 fn s e
signal <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn @(ExecSignal fn s e) (forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> Specification fn (ExecSignal fn rule era)
signalSpec @fn @s @e ExecContext fn s e
ctxt ExecEnvironment fn 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 fn 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 fn 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 fn s e.
  ( ExecSpecRule fn s e
  , ExecState fn s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Proxy fn ->
  Int ->
  Gen [Signal (EraRule s e)]
minitrace :: forall (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e -> Proxy fn -> Int -> Gen [Signal (EraRule s e)]
minitrace WitRule s e
witrule Proxy fn
Proxy Int
n0 = do
  Either [[Char]] [Signal (EraRule s e)]
ans <- forall (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy fn -> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
minitraceEither @fn @s @e WitRule s e
witrule forall {k} (t :: k). Proxy t
Proxy 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 ConwayFn s e
  , ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy fn -> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
minitraceEither @ConwayFn @s @e WitRule s e
witrule (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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 ConwayFn s e,
 ExecState ConwayFn 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))