{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Trace.Pipeline where

import Cardano.Ledger.BaseTypes (Globals)
import Cardano.Ledger.Core (Era, EraRule, Tx)
import Cardano.Ledger.Shelley.LedgerState (LedgerState)
import Cardano.Ledger.Shelley.Rules
import Control.Monad.Reader (Reader, runReader)
import Control.State.Transition.Extended (
  BaseM,
  RuleType (Transition),
  STS (..),
  TRC (..),
  applySTS,
 )
import Data.Default (Default (def))
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.List.NonEmpty (NonEmpty)
import qualified Data.Map.Strict as Map
import Data.Pulse (foldlM')
import GHC.TypeLits (Symbol)
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (TxF (..))
import Test.Cardano.Ledger.Constrained.Env (Env, Name, emptyEnv, findVar)
import Test.Cardano.Ledger.Constrained.Monad (errorTyped, monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.Repl (goRepl)
import Test.Cardano.Ledger.Constrained.Preds.Tx (adjustColInput, adjustFeeInput, txBodyPreds)
import Test.Cardano.Ledger.Constrained.Rewrite (
  DependGraph (..),
  initialOrder,
  mkDependGraph,
  notBefore,
  rewriteGen,
  standardOrderInfo,
 )
import Test.Cardano.Ledger.Constrained.Solver (solveOneVar)
import Test.Cardano.Ledger.Constrained.Stage (Pipeline, Stage (..), ledgerPipeline, solvePipeline)
import Test.Cardano.Ledger.Constrained.Trace.TraceMonad
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.Proof hiding (WitRule (..), lift)
import Test.Cardano.Ledger.Shelley.Utils (testGlobals)
import Test.QuickCheck

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

data Rule (i :: Symbol) where
  DELEG :: Rule "DELEG"
  DELEGS :: Rule "DELEGS"
  DELPL :: Rule "DELPL"
  EPOCH :: Rule "EPOCH"
  LEDGER :: Rule "LEDGER"
  LEDGERS :: Rule "LEDGERS"
  MIR :: Rule "MIR"
  NEWEPOCH :: Rule "NEWSPOCH"
  NEWPP :: Rule "NEWPP"
  POOL :: Rule "POOL"
  POOLREAP :: Rule "POOLREAP"
  PPUP :: Rule "PPUP"
  RUPD :: Rule "RUPD"
  SNAP :: Rule "SNAP"
  TICK :: Rule "TICK"
  TICKF :: Rule "TICKF"
  UPEC :: Rule "UPEC"
  UTXO :: Rule "UTXO"
  UTXOW :: Rule "UTXOW"
  GOVCERT :: Rule "GOVCERT"
  GOV :: Rule "GOV"

trc ::
  Proof era ->
  Rule tag ->
  Environment (EraRule tag era) ->
  State (EraRule tag era) ->
  Signal (EraRule tag era) ->
  TRC (EraRule tag era)
trc :: forall era (tag :: Symbol).
Proof era
-> Rule tag
-> Environment (EraRule tag era)
-> State (EraRule tag era)
-> Signal (EraRule tag era)
-> TRC (EraRule tag era)
trc Proof era
_proof Rule tag
_rule Environment (EraRule tag era)
env State (EraRule tag era)
state Signal (EraRule tag era)
sig = forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule tag era)
env, State (EraRule tag era)
state, Signal (EraRule tag era)
sig)

sts ::
  forall era tag.
  ( BaseM (EraRule tag era) ~ Reader Globals
  , STS (EraRule tag era)
  ) =>
  Proof era ->
  Rule tag ->
  Environment (EraRule tag era) ->
  State (EraRule tag era) ->
  Signal (EraRule tag era) ->
  Either (NonEmpty (PredicateFailure (EraRule tag era))) (State (EraRule tag era))
sts :: forall era (tag :: Symbol).
(BaseM (EraRule tag era) ~ Reader Globals,
 STS (EraRule tag era)) =>
Proof era
-> Rule tag
-> Environment (EraRule tag era)
-> State (EraRule tag era)
-> Signal (EraRule tag era)
-> Either
     (NonEmpty (PredicateFailure (EraRule tag era)))
     (State (EraRule tag era))
sts Proof era
proof Rule tag
rule Environment (EraRule tag era)
env State (EraRule tag era)
state Signal (EraRule tag era)
sig =
  forall r a. Reader r a -> r -> a
runReader
    ( forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTS @(EraRule tag era) @(Reader _) @'Transition
        (forall era (tag :: Symbol).
Proof era
-> Rule tag
-> Environment (EraRule tag era)
-> State (EraRule tag era)
-> Signal (EraRule tag era)
-> TRC (EraRule tag era)
trc Proof era
proof Rule tag
rule Environment (EraRule tag era)
env State (EraRule tag era)
state Signal (EraRule tag era)
sig)
    )
    Globals
testGlobals

stsWithContinuations ::
  forall era tag ans.
  ( BaseM (EraRule tag era) ~ Reader Globals
  , STS (EraRule tag era)
  ) =>
  Proof era ->
  Rule tag ->
  (NonEmpty (PredicateFailure (EraRule tag era)) -> ans) ->
  (State (EraRule tag era) -> ans) ->
  Environment (EraRule tag era) ->
  State (EraRule tag era) ->
  Signal (EraRule tag era) ->
  ans
stsWithContinuations :: forall era (tag :: Symbol) ans.
(BaseM (EraRule tag era) ~ Reader Globals,
 STS (EraRule tag era)) =>
Proof era
-> Rule tag
-> (NonEmpty (PredicateFailure (EraRule tag era)) -> ans)
-> (State (EraRule tag era) -> ans)
-> Environment (EraRule tag era)
-> State (EraRule tag era)
-> Signal (EraRule tag era)
-> ans
stsWithContinuations Proof era
proof Rule tag
rule NonEmpty (PredicateFailure (EraRule tag era)) -> ans
fails State (EraRule tag era) -> ans
succeeds Environment (EraRule tag era)
env State (EraRule tag era)
state Signal (EraRule tag era)
sig =
  case forall era (tag :: Symbol).
(BaseM (EraRule tag era) ~ Reader Globals,
 STS (EraRule tag era)) =>
Proof era
-> Rule tag
-> Environment (EraRule tag era)
-> State (EraRule tag era)
-> Signal (EraRule tag era)
-> Either
     (NonEmpty (PredicateFailure (EraRule tag era)))
     (State (EraRule tag era))
sts Proof era
proof Rule tag
rule Environment (EraRule tag era)
env State (EraRule tag era)
state Signal (EraRule tag era)
sig of
    Left NonEmpty (PredicateFailure (EraRule tag era))
xs -> NonEmpty (PredicateFailure (EraRule tag era)) -> ans
fails NonEmpty (PredicateFailure (EraRule tag era))
xs
    Right State (EraRule tag era)
x -> State (EraRule tag era) -> ans
succeeds State (EraRule tag era)
x

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

-- | Translate a Pipe into a DependGraph, given the set
--   of variables that have aready been solved for.
pipeToGraph :: Era era => Stage era -> HashSet (Name era) -> TraceM era (DependGraph era)
pipeToGraph :: forall era.
Era era =>
Stage era -> HashSet (Name era) -> TraceM era (DependGraph era)
pipeToGraph (Stage OrderInfo
info [Pred era]
ps) HashSet (Name era)
alreadyDefined = do
  [Pred era]
simple <- forall a b era. ((Int, a) -> Gen (Int, b)) -> a -> TraceM era b
liftCounter forall era. Era era => (Int, [Pred era]) -> Gen (Int, [Pred era])
rewriteGen [Pred era]
ps
  [Name era]
orderedNames <- forall a era. Typed a -> TraceM era a
liftTyped forall a b. (a -> b) -> a -> b
$ forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder OrderInfo
info [Pred era]
simple
  forall a era. Typed a -> TraceM era a
liftTyped forall a b. (a -> b) -> a -> b
$
    forall era.
Era era =>
Int
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph
      (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
orderedNames)
      []
      HashSet (Name era)
alreadyDefined
      [Name era]
orderedNames
      []
      (forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter forall era. Pred era -> Bool
notBefore [Pred era]
simple)

-- | Merge a Pipeline into an existing DependGraph, given the set of variables
--   that have aready been solved for, to get a larger DependGraph
mergePipeline ::
  Era era => Pipeline era -> HashSet (Name era) -> DependGraph era -> TraceM era (DependGraph era)
mergePipeline :: forall era.
Era era =>
Pipeline era
-> HashSet (Name era)
-> DependGraph era
-> TraceM era (DependGraph era)
mergePipeline [] HashSet (Name era)
_ DependGraph era
graph = forall (f :: * -> *) a. Applicative f => a -> f a
pure DependGraph era
graph
mergePipeline (Stage era
pipe : [Stage era]
more) HashSet (Name era)
defined (DependGraph [([Name era], [Pred era])]
xs) = do
  DependGraph [([Name era], [Pred era])]
ys <- forall era.
Era era =>
Stage era -> HashSet (Name era) -> TraceM era (DependGraph era)
pipeToGraph Stage era
pipe HashSet (Name era)
defined
  let names :: [Name era]
names = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> a
fst [([Name era], [Pred era])]
ys
  forall era.
Era era =>
Pipeline era
-> HashSet (Name era)
-> DependGraph era
-> TraceM era (DependGraph era)
mergePipeline [Stage era]
more (forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union (forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList [Name era]
names) HashSet (Name era)
defined) (forall era. [([Name era], [Pred era])] -> DependGraph era
DependGraph ([([Name era], [Pred era])]
xs forall a. [a] -> [a] -> [a]
++ [([Name era], [Pred era])]
ys))

-- | Solve a Pipeline to get both an Env and a DependGraph
solvePipeline2 :: Reflect era => Pipeline era -> TraceM era (Env era, DependGraph era)
solvePipeline2 :: forall era.
Reflect era =>
Pipeline era -> TraceM era (Env era, DependGraph era)
solvePipeline2 Pipeline era
pipes = do
  gr :: DependGraph era
gr@(DependGraph [([Name era], [Pred era])]
pairs) <- forall era.
Era era =>
Pipeline era
-> HashSet (Name era)
-> DependGraph era
-> TraceM era (DependGraph era)
mergePipeline Pipeline era
pipes forall a. HashSet a
HashSet.empty (forall era. [([Name era], [Pred era])] -> DependGraph era
DependGraph [])
  Subst Map String (SubstElem era)
subst <- forall a era. Gen a -> TraceM era a
liftGen (forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' forall era.
Era era =>
Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar forall era. Subst era
emptySubst [([Name era], [Pred era])]
pairs)
  let isTempV :: t Char -> Bool
isTempV t Char
k = forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Char
'.' t Char
k
  let sub :: Subst era
sub = forall era. Map String (SubstElem era) -> Subst era
Subst (forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
k SubstElem era
_ -> forall {t :: * -> *}. Foldable t => t Char -> Bool
isTempV String
k) Map String (SubstElem era)
subst)
  Env era
env <- forall a era. Typed a -> TraceM era a
liftTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
sub forall era. Env era
emptyEnv)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era
env, DependGraph era
gr)

main :: IO ()
main :: IO ()
main = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
  ((Env BabbageEra
env, DependGraph [([Name BabbageEra], [Pred BabbageEra])]
zs), Int
_, Env BabbageEra
_) <-
    forall a. Gen a -> IO a
generate (forall era a.
Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
runTraceM Int
0 forall era. Env era
emptyEnv (forall era.
Reflect era =>
Pipeline era -> TraceM era (Env era, DependGraph era)
solvePipeline2 (forall era. Reflect era => UnivSize -> Proof era -> Pipeline era
ledgerPipeline forall a. Default a => a
def Proof BabbageEra
proof)))
  let vs :: HashSet (Name BabbageEra)
vs = forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty forall era. Era era => RootTarget era (DState era) (DState era)
dstateT
      ok :: ([Name BabbageEra], [Pred BabbageEra]) -> Bool
ok = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet (Name BabbageEra)
vs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall era. [([Name era], [Pred era])] -> DependGraph era
DependGraph (forall a. (a -> Bool) -> [a] -> [a]
filter ([Name BabbageEra], [Pred BabbageEra]) -> Bool
ok [([Name BabbageEra], [Pred BabbageEra])]
zs)))
  forall era. Proof era -> Env era -> String -> IO ()
goRepl Proof BabbageEra
proof Env BabbageEra
env String
""

-- =================================================
-- Staging and STS rules

sts0 ::
  (Show ctx, Show state, Show sig, Testable prop) =>
  Gen ctx ->
  (ctx -> Gen state) ->
  (ctx -> state -> Gen sig) ->
  (ctx -> state -> sig -> state) ->
  (state -> state -> prop) ->
  Property
sts0 :: forall ctx state sig prop.
(Show ctx, Show state, Show sig, Testable prop) =>
Gen ctx
-> (ctx -> Gen state)
-> (ctx -> state -> Gen sig)
-> (ctx -> state -> sig -> state)
-> (state -> state -> prop)
-> Property
sts0 Gen ctx
ctx ctx -> Gen state
state ctx -> state -> Gen sig
sig ctx -> state -> sig -> state
apply state -> state -> prop
test =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
    Gen ctx
ctx
    ( \ctx
c ->
        forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
          (ctx -> Gen state
state ctx
c)
          ( \state
s ->
              forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess
                Int
100
                (forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (ctx -> state -> Gen sig
sig ctx
c state
s) (\sig
tx -> state -> state -> prop
test state
s (ctx -> state -> sig -> state
apply ctx
c state
s sig
tx)))
          )
    )

-- | When we run a STS rule, the context (env) is a subset of the state, so
--   it makes sense to generate state, and then extract the context.
sts1 ::
  (Show ctx, Show state, Show sig, Testable prop) =>
  Gen state ->
  (state -> Gen ctx) ->
  (state -> ctx -> Gen sig) ->
  ((ctx, state, sig) -> state) ->
  (state -> state -> prop) ->
  Property
sts1 :: forall ctx state sig prop.
(Show ctx, Show state, Show sig, Testable prop) =>
Gen state
-> (state -> Gen ctx)
-> (state -> ctx -> Gen sig)
-> ((ctx, state, sig) -> state)
-> (state -> state -> prop)
-> Property
sts1 Gen state
state state -> Gen ctx
ctx state -> ctx -> Gen sig
sig (ctx, state, sig) -> state
apply state -> state -> prop
test =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
    Gen state
state
    ( \state
s ->
        forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
          (state -> Gen ctx
ctx state
s)
          ( \ctx
c ->
              forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess
                Int
100
                (forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (state -> ctx -> Gen sig
sig state
s ctx
c) (\sig
tx -> state -> state -> prop
test state
s ((ctx, state, sig) -> state
apply (ctx
c, state
s, sig
tx))))
          )
    )

proofx :: Proof BabbageEra
proofx :: Proof BabbageEra
proofx = Proof BabbageEra
Babbage

genLedgerState :: Gen (Env BabbageEra, Subst BabbageEra, LedgerState BabbageEra)
genLedgerState :: Gen (Env BabbageEra, Subst BabbageEra, LedgerState BabbageEra)
genLedgerState = do
  (Env BabbageEra
env, Subst BabbageEra
sub, DependGraph BabbageEra
_graph) <- forall era.
Reflect era =>
Pipeline era -> Gen (Env era, Subst era, DependGraph era)
solvePipeline (forall era. Reflect era => UnivSize -> Proof era -> Pipeline era
ledgerPipeline forall a. Default a => a
def Proof BabbageEra
proofx)
  LedgerState BabbageEra
ledgerstate <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env BabbageEra
env (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof BabbageEra
proofx)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env BabbageEra
env, Subst BabbageEra
sub, LedgerState BabbageEra
ledgerstate)

genSig :: Reflect era => Proof era -> (a, Subst era, b) -> p -> Gen (Tx era)
genSig :: forall era a b p.
Reflect era =>
Proof era -> (a, Subst era, b) -> p -> Gen (Tx era)
genSig Proof era
proof (a
_, Subst era
sub, b
_) p
_ledgerEnv = do
  let preds :: [Pred era]
preds = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub) (forall era.
(HasCallStack, Reflect era) =>
UnivSize -> Proof era -> [Pred era]
txBodyPreds forall a. Default a => a
def Proof era
proof)
  (Env era
env0, Subst era
_sub, DependGraph era
_graph) <- forall era.
Reflect era =>
Pipeline era -> Gen (Env era, Subst era, DependGraph era)
solvePipeline [forall era. OrderInfo -> [Pred era] -> Stage era
Stage OrderInfo
standardOrderInfo [Pred era]
preds]
  Env era
env1 <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env0
  Env era
env2 <- forall t. HasCallStack => Typed t -> t
errorTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env1
  (TxF Proof era
_ Tx era
tx) <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era t. V era t -> Env era -> Typed t
findVar (forall era t. Term era t -> V era t
unVar forall era. Reflect era => Term era (TxF era)
txterm) Env era
env2)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Tx era
tx