{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}

module Test.Cardano.Ledger.Constrained.Conway.TxBodySpec where

import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Rules (CertsEnv (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Core
import Cardano.Ledger.Val
import Constrained.API
import Constrained.Base (IsPred (..))
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.TreeDiff
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway.Cert (
  delegateeSpec,
  shelleyTxCertSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.Certs (certsEnvSpec, projectEnv)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.QuickCheck hiding (forAll, witness)
import Prelude hiding (seq)

-- =================================
-- Move these to the MapSpec

subMap ::
  (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
  Specification (Map k v, Map k v)
subMap :: forall k v.
(Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
Specification (Map k v, Map k v)
subMap = (Term (Map k v, Map k v) -> Pred)
-> Specification (Map k v, Map k v)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map k v, Map k v) -> Pred)
 -> Specification (Map k v, Map k v))
-> (Term (Map k v, Map k v) -> Pred)
-> Specification (Map k v, Map k v)
forall a b. (a -> b) -> a -> b
$ \ Term (Map k v, Map k v)
[var|pair|] ->
  Term (Map k v, Map k v)
-> FunTy (MapList Term (ProductAsList (Map k v, Map k v))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Map k v, Map k v)
pair (FunTy (MapList Term (ProductAsList (Map k v, Map k v))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (Map k v, Map k v))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map k v)
[var|sub|] Term (Map k v)
[var|super|] ->
    [ Term (Map k v) -> Term (Map k v) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
sub Term (Map k v)
super
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super Term (Map k v) -> Term (Map k v) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Map k v -> Term (Map k v)
forall a. HasSpec a => a -> Term a
lit (Map k v
forall k a. Map k a
Map.empty)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set k) -> Term (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map k v) -> Term (Set k)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
sub) (Term (Map k v) -> Term (Set k)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
super)
    , Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        Term (k, v)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair (FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [Term v -> Term k -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term v
v Term k
k, Term (Maybe v) -> (Term v -> Term Bool) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term k -> Term (Map k v) -> Term (Maybe v)
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term k
k Term (Map k v)
super) (\Term v
a -> Term v
v Term v -> Term v -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term v
a)]
    ]

subMapSubDependsOnSuper ::
  (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
  Term (Map k v) ->
  Term (Map k v) ->
  Pred
subMapSubDependsOnSuper :: forall k v.
(Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
Term (Map k v) -> Term (Map k v) -> Pred
subMapSubDependsOnSuper Term (Map k v)
sub Term (Map k v)
super =
  [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
    [ Term (Map k v) -> Term (Map k v) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
sub Term (Map k v)
super
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super Term (Map k v) -> Term (Map k v) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Map k v -> Term (Map k v)
forall a. HasSpec a => a -> Term a
lit (Map k v
forall k a. Map k a
Map.empty)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set k) -> Term (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map k v) -> Term (Set k)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
sub) (Term (Map k v) -> Term (Set k)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
super)
    , Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        Term (k, v)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair (FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [Term v -> Term k -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term v
v Term k
k, Term (Maybe v) -> (Term v -> Term Bool) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term k -> Term (Map k v) -> Term (Maybe v)
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term k
k Term (Map k v)
super) (\Term v
a -> Term v
v Term v -> Term v -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term v
a)]
    ]

subMapSuperDependsOnSub ::
  (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
  Term (Map k v) ->
  Term (Map k v) ->
  Pred
subMapSuperDependsOnSub :: forall k v.
(Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
Term (Map k v) -> Term (Map k v) -> Pred
subMapSuperDependsOnSub Term (Map k v)
sub Term (Map k v)
super =
  [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
    [ Term (Map k v) -> Term (Map k v) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
super Term (Map k v)
sub
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super Term (Map k v) -> Term (Map k v) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Map k v -> Term (Map k v)
forall a. HasSpec a => a -> Term a
lit (Map k v
forall k a. Map k a
Map.empty)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set k) -> Term (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map k v) -> Term (Set k)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
sub) (Term (Map k v) -> Term (Set k)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
super)
    , Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        Term (k, v)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair (FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [Term (Maybe v) -> (Term v -> Term Bool) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term k -> Term (Map k v) -> Term (Maybe v)
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term k
k Term (Map k v)
super) (\Term v
a -> Term v
v Term v -> Term v -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term v
a)]
    ]

sumTxOut_ :: forall era. EraSpecTxOut era => Term [TxOut era] -> Term Coin
sumTxOut_ :: forall era. EraSpecTxOut era => Term [TxOut era] -> Term Coin
sumTxOut_ Term [TxOut era]
x = (Term (TxOut era) -> Term Coin) -> Term [TxOut era] -> Term Coin
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ (forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era) Term [TxOut era]
x

sumCoin_ :: Term [Coin] -> Term Coin
sumCoin_ :: Term [Coin] -> Term Coin
sumCoin_ Term [Coin]
x = (Term Coin -> Term Coin) -> Term [Coin] -> Term Coin
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term Coin -> Term Coin
forall a. a -> a
id Term [Coin]
x

adjustTxOutCoin :: EraTxOut era => DeltaCoin -> TxOut era -> TxOut era
adjustTxOutCoin :: forall era. EraTxOut era => DeltaCoin -> TxOut era -> TxOut era
adjustTxOutCoin (DeltaCoin Integer
n) TxOut era
x = TxOut era
x TxOut era -> (TxOut era -> TxOut era) -> TxOut era
forall a b. a -> (a -> b) -> b
& (Coin -> Identity Coin) -> TxOut era -> Identity (TxOut era)
forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
Lens' (TxOut era) Coin
coinTxOutL ((Coin -> Identity Coin) -> TxOut era -> Identity (TxOut era))
-> Coin -> TxOut era -> TxOut era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ((TxOut era
x TxOut era -> Getting Coin (TxOut era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxOut era) Coin
forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
Lens' (TxOut era) Coin
coinTxOutL) Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> (Integer -> Coin
Coin Integer
n))

-- | Extract the total deposits and refunds from a list of TxCerts.
--   This a kind of AdaPot relative to the Certs in a Transaction body
--   It depends on the PParams (deposit ammounts for registering a staking key, a ppol, and registering a Drep)
--   and on the CertState (what deposits were made in the past)
getDepositRefund ::
  forall era.
  (EraTxCert era, ConwayEraCertState era) =>
  PParams era -> CertState era -> [TxCert era] -> (DeltaCoin, DeltaCoin)
getDepositRefund :: forall era.
(EraTxCert era, ConwayEraCertState era) =>
PParams era
-> CertState era -> [TxCert era] -> (DeltaCoin, DeltaCoin)
getDepositRefund PParams era
pp CertState era
certState [TxCert era]
certs =
  ( Coin -> DeltaCoin
delta (Coin -> DeltaCoin) -> Coin -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ PParams era -> (KeyHash 'StakePool -> Bool) -> [TxCert era] -> Coin
forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
forall (f :: * -> *).
Foldable f =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
getTotalDepositsTxCerts PParams era
pp (KeyHash 'StakePool -> Map (KeyHash 'StakePool) PoolParams -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
ps) [TxCert era]
certs
  , Coin -> DeltaCoin
delta (Coin -> DeltaCoin) -> Coin -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> [TxCert era]
-> Coin
forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
forall (f :: * -> *).
Foldable f =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
getTotalRefundsTxCerts PParams era
pp (DState era -> Credential 'Staking -> Maybe Coin
forall era. DState era -> Credential 'Staking -> Maybe Coin
lookupDepositDState DState era
ds) (VState era -> Credential 'DRepRole -> Maybe Coin
forall era. VState era -> Credential 'DRepRole -> Maybe Coin
lookupDepositVState VState era
vs) [TxCert era]
certs
  )
  where
    delta :: Coin -> DeltaCoin
delta (Coin Integer
n) = Integer -> DeltaCoin
DeltaCoin Integer
n
    vs :: VState era
vs = CertState era
certState CertState era
-> Getting (VState era) (CertState era) (VState era) -> VState era
forall s a. s -> Getting a s a -> a
^. Getting (VState era) (CertState era) (VState era)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState era) (VState era)
certVStateL
    ps :: PState era
ps = CertState era
certState CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
    ds :: DState era
ds = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL

-- | This is exactly the same as reify, except it names the existential varaible for better error messages
reifyX ::
  ( HasSpec a
  , HasSpec b
  , IsPred p
  ) =>
  Term a ->
  (a -> b) ->
  (Term b -> p) ->
  Pred
reifyX :: forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reifyX Term a
t a -> b
f Term b -> p
body =
  ((forall b. Term b -> b) -> GE b) -> (Term b -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> b -> GE b
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> GE b) -> b -> GE b
forall a b. (a -> b) -> a -> b
$ a -> b
f (Term a -> a
forall b. Term b -> b
eval Term a
t)) ((Term b -> [Pred]) -> Pred) -> (Term b -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term b
[var|reifyvar|] ->
    -- NOTE we name the existenital variable 'reifyvar'
    [ Term b -> Term a -> (a -> b) -> Pred
forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies Term b
reifyvar Term a
t a -> b
f
    , NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"reifies " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term b -> String
forall a. Show a => a -> String
show Term b
reifyvar)) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ p -> Pred
forall p. IsPred p => p -> Pred
toPred (p -> Pred) -> p -> Pred
forall a b. (a -> b) -> a -> b
$ Term b -> p
body Term b
reifyvar
    ]

-- ==============================================================================
-- Some code to visualize what is happening, this code will disappear eventually

putPretty :: ToExpr t => [Char] -> t -> IO ()
putPretty :: forall t. ToExpr t => String -> t -> IO ()
putPretty String
nm t
x = String -> IO ()
putStrLn (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (t -> Doc
forall x. ToExpr x => x -> Doc
prettyE t
x))

testBody :: IO ()
testBody :: IO ()
testBody = do
  WitUniv AllegraEra
univ <- Gen (WitUniv AllegraEra) -> IO (WitUniv AllegraEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv AllegraEra) -> IO (WitUniv AllegraEra))
-> Gen (WitUniv AllegraEra) -> IO (WitUniv AllegraEra)
forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @AllegraEra Int
5
  Map RewardAccount Coin
wdrls <- Gen (Map RewardAccount Coin) -> IO (Map RewardAccount Coin)
forall a. Gen a -> IO a
generate (Gen (Map RewardAccount Coin) -> IO (Map RewardAccount Coin))
-> Gen (Map RewardAccount Coin) -> IO (Map RewardAccount Coin)
forall a b. (a -> b) -> a -> b
$ Specification (Map RewardAccount Coin)
-> Gen (Map RewardAccount Coin)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec ((Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map RewardAccount Coin) -> Pred)
 -> Specification (Map RewardAccount Coin))
-> (Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> WitUniv AllegraEra -> Term (Map RewardAccount Coin) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv AllegraEra
univ Term (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- Gen (Set (Credential 'DRepRole)) -> IO (Set (Credential 'DRepRole))
forall a. Gen a -> IO a
generate (Gen (Set (Credential 'DRepRole))
 -> IO (Set (Credential 'DRepRole)))
-> Gen (Set (Credential 'DRepRole))
-> IO (Set (Credential 'DRepRole))
forall a b. (a -> b) -> a -> b
$ Specification (Set (Credential 'DRepRole))
-> Gen (Set (Credential 'DRepRole))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv AllegraEra -> Specification (Set (Credential 'DRepRole))
forall era.
Era era =>
WitUniv era -> Specification (Set (Credential 'DRepRole))
delegateeSpec WitUniv AllegraEra
univ)
  CertsEnv AllegraEra
certsEnv <- Gen (CertsEnv AllegraEra) -> IO (CertsEnv AllegraEra)
forall a. Gen a -> IO a
generate (Gen (CertsEnv AllegraEra) -> IO (CertsEnv AllegraEra))
-> Gen (CertsEnv AllegraEra) -> IO (CertsEnv AllegraEra)
forall a b. (a -> b) -> a -> b
$ forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertsEnv AllegraEra) Specification (CertsEnv AllegraEra)
forall era.
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (CertsEnv era)
certsEnvSpec
  ShelleyCertState AllegraEra
certState <-
    Gen (CertState AllegraEra) -> IO (CertState AllegraEra)
forall a. Gen a -> IO a
generate (Gen (CertState AllegraEra) -> IO (CertState AllegraEra))
-> Gen (CertState AllegraEra) -> IO (CertState AllegraEra)
forall a b. (a -> b) -> a -> b
$
      forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertState AllegraEra)
        (forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec @AllegraEra WitUniv AllegraEra
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls)

  ShelleyTxCert AllegraEra
cert <-
    Gen (ShelleyTxCert AllegraEra) -> IO (ShelleyTxCert AllegraEra)
forall a. Gen a -> IO a
generate (Gen (ShelleyTxCert AllegraEra) -> IO (ShelleyTxCert AllegraEra))
-> Gen (ShelleyTxCert AllegraEra) -> IO (ShelleyTxCert AllegraEra)
forall a b. (a -> b) -> a -> b
$
      forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(TxCert AllegraEra) (Specification (TxCert AllegraEra) -> Gen (TxCert AllegraEra))
-> Specification (TxCert AllegraEra) -> Gen (TxCert AllegraEra)
forall a b. (a -> b) -> a -> b
$
        (forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec @AllegraEra WitUniv AllegraEra
univ (CertsEnv AllegraEra -> CertEnv AllegraEra
forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv AllegraEra
certsEnv) ShelleyCertState AllegraEra
certState)
          Specification (ShelleyTxCert AllegraEra)
-> Specification (ShelleyTxCert AllegraEra)
-> Specification (ShelleyTxCert AllegraEra)
forall a. Semigroup a => a -> a -> a
<> (WitUniv AllegraEra -> Specification (ShelleyTxCert AllegraEra)
forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert WitUniv AllegraEra
univ)
  -- The problem with this is that the CertState does not have any
  -- thing from the universe, so any Cert that requires a member_ of someting
  -- in the CertState, will never succeed,  because the Hashes are disjoint
  -- between the CertState and the Universe. So those certs with member_
  -- always fail, so the only ones that are ever generated are RegCert and RegPool
  WitUniv AllegraEra -> IO ()
forall a. Show a => a -> IO ()
print WitUniv AllegraEra
univ
  String -> IO ()
putStrLn (Doc -> String
forall a. Show a => a -> String
show (ShelleyTxCert AllegraEra -> Doc
forall x. ToExpr x => x -> Doc
prettyE ShelleyTxCert AllegraEra
cert))