{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}

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

import qualified Cardano.Chain.Common as Byron
import Cardano.Crypto (SigningKey)
import Cardano.Crypto.Signing (toVerification)
import qualified Cardano.Crypto.Signing as Byron
import qualified Cardano.Crypto.Wallet as Byron (generate)
import Cardano.Ledger.Address (BootstrapAddress (..), RewardAccount (..))
import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Allegra.Scripts (
  AllegraEraScript (..),
  pattern RequireTimeExpire,
  pattern RequireTimeStart,
 )
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Alonzo.Scripts (AlonzoEraScript (..), AsIx (..), PlutusPurpose)
import Cardano.Ledger.Alonzo.TxWits (AlonzoEraTxWits (..), Redeemers (..), TxDats (..))
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.BaseTypes (Network (..), SlotNo (..))
import Cardano.Ledger.Binary (EncCBOR (encCBOR))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Core
import Cardano.Ledger.Credential
import Cardano.Ledger.DRep (DRep (..))
import Cardano.Ledger.Keys (
  BootstrapWitness,
  GenDelegPair (..),
  KeyHash (..),
  KeyRole (..),
  VKey,
  WitVKey,
  hashKey,
  makeBootstrapWitness,
 )
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.Mary.Value ()
import Cardano.Ledger.Plutus.Data (Data (..), hashData)
import Cardano.Ledger.Plutus.ExUnits (ExUnits (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.Scripts
import Cardano.Ledger.Shelley.TxCert
import Constrained.API
import Constrained.Base (toPred)
import Constrained.GenT (pureGen)
import Constrained.TheKnot (hasSize, rangeSize)
import Control.DeepSeq (NFData (..), deepseq)
import Control.Monad (replicateM)
import Data.ByteString (ByteString)
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import qualified Data.Sequence.Strict as Seq
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (pack)
import qualified Data.TreeDiff as Tree (Expr (..))
import Data.Typeable
import GHC.Generics
import Lens.Micro
import System.IO.Unsafe (unsafePerformIO)
import Test.Cardano.Ledger.Binary.Arbitrary (genByteString)
import Test.Cardano.Ledger.Common (ToExpr (..))
import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic (cSJust_, prettyE)
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams ()
import Test.Cardano.Ledger.Conway.TreeDiff ()
import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..), mkWitnessVKey)
import Test.QuickCheck hiding (forAll, witness)
import Text.PrettyPrint.HughesPJ (Doc)

-- ======================================================
-- BootstrapAddress are specific to the Byron Era.

-- | Turn a random bytestring into a SigningKey
genSigningKey :: Gen SigningKey
genSigningKey :: Gen SigningKey
genSigningKey = do
  ByteString
seed <- Int -> Gen ByteString
genByteString Int
32
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (XPrv -> SigningKey
Byron.SigningKey forall a b. (a -> b) -> a -> b
$ forall passPhrase seed.
(ByteArrayAccess passPhrase, ByteArrayAccess seed) =>
seed -> passPhrase -> XPrv
Byron.generate ByteString
seed (forall a. Monoid a => a
mempty :: ByteString))

-- | Generate a pair, A Byron address, and the key that can sign it.
genAddrPair :: Network -> Gen (BootstrapAddress, Byron.SigningKey)
genAddrPair :: Network -> Gen (BootstrapAddress, SigningKey)
genAddrPair Network
netwrk = do
  SigningKey
signkey <- Gen SigningKey
genSigningKey
  let verificationKey :: VerificationKey
verificationKey = SigningKey -> VerificationKey
Byron.toVerification SigningKey
signkey
      asd :: AddrSpendingData
asd = VerificationKey -> AddrSpendingData
Byron.VerKeyASD VerificationKey
verificationKey
      byronNetwork :: NetworkMagic
byronNetwork = case Network
netwrk of
        Network
Mainnet -> NetworkMagic
Byron.NetworkMainOrStage
        Network
Testnet -> Word32 -> NetworkMagic
Byron.NetworkTestnet Word32
0
      attrs :: AddrAttributes
attrs =
        Maybe HDAddressPayload -> NetworkMagic -> AddrAttributes
Byron.AddrAttributes
          (forall a. a -> Maybe a
Just (ByteString -> HDAddressPayload
Byron.HDAddressPayload ByteString
"a compressed lenna.png"))
          NetworkMagic
byronNetwork
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Address -> BootstrapAddress
BootstrapAddress (AddrSpendingData -> AddrAttributes -> Address
Byron.makeAddress AddrSpendingData
asd AddrAttributes
attrs), SigningKey
signkey)

-- ===============================================
-- Move these somewhere else

instance Era era => HasSimpleRep (TxDats era) where
  type SimpleRep (TxDats era) = Map DataHash (Data era)
  toSimpleRep :: TxDats era -> SimpleRep (TxDats era)
toSimpleRep (TxDats Map DataHash (Data era)
m) = Map DataHash (Data era)
m
  fromSimpleRep :: SimpleRep (TxDats era) -> TxDats era
fromSimpleRep SimpleRep (TxDats era)
m = forall era. Era era => Map DataHash (Data era) -> TxDats era
TxDats SimpleRep (TxDats era)
m

instance Era era => HasSpec (TxDats era)

instance AlonzoEraScript era => HasSimpleRep (Redeemers era) where
  type SimpleRep (Redeemers era) = Map (PlutusPurpose AsIx era) (Data era, ExUnits)
  toSimpleRep :: Redeemers era -> SimpleRep (Redeemers era)
toSimpleRep (Redeemers Map (PlutusPurpose AsIx era) (Data era, ExUnits)
m) = Map (PlutusPurpose AsIx era) (Data era, ExUnits)
m
  fromSimpleRep :: SimpleRep (Redeemers era) -> Redeemers era
fromSimpleRep SimpleRep (Redeemers era)
m = forall era.
AlonzoEraScript era =>
Map (PlutusPurpose AsIx era) (Data era, ExUnits) -> Redeemers era
Redeemers SimpleRep (Redeemers era)
m

instance
  ( ShelleyEraScript era
  , NativeScript era ~ MultiSig era
  ) =>
  HasSpec (MultiSig era)
  where
  type TypeSpec (MultiSig era) = ()
  emptySpec :: TypeSpec (MultiSig era)
emptySpec = ()
  combineSpec :: TypeSpec (MultiSig era)
-> TypeSpec (MultiSig era) -> Specification (MultiSig era)
combineSpec TypeSpec (MultiSig era)
_ TypeSpec (MultiSig era)
_ = forall deps a. SpecificationD deps a
TrueSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (MultiSig era) -> GenT m (MultiSig era)
genFromTypeSpec TypeSpec (MultiSig era)
_ = forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$ forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig Int
2
  cardinalTypeSpec :: TypeSpec (MultiSig era) -> Specification Integer
cardinalTypeSpec TypeSpec (MultiSig era)
_ = forall deps a. SpecificationD deps a
TrueSpec
  shrinkWithTypeSpec :: TypeSpec (MultiSig era) -> MultiSig era -> [MultiSig era]
shrinkWithTypeSpec TypeSpec (MultiSig era)
_ = forall a. Arbitrary a => a -> [a]
shrink
  conformsTo :: HasCallStack => MultiSig era -> TypeSpec (MultiSig era) -> Bool
conformsTo MultiSig era
_ TypeSpec (MultiSig era)
_ = Bool
True
  toPreds :: Term (MultiSig era) -> TypeSpec (MultiSig era) -> Pred
toPreds Term (MultiSig era)
_ TypeSpec (MultiSig era)
_ = forall p. IsPred p => p -> Pred
toPred Bool
True

-- ========================================================================
-- We need witnesses when the Tx has values of type 'hashtype' inside, because
-- the witnesses allows one to recover proof (ProofType hashtype era) that
-- the Tx author both knows, and controls, the thing that was Hashed,
-- i.e. (TypeHashed hashtype era). The witness (WitnessType hashtype era)
-- is NOT ALWAYS the same as the (ProofType hashtype era), since it can depend on
-- the Tx. All the strange class preconditions are required by conformance testing.

class
  ( Eq (ProofType hashtype era)
  , EncCBOR (ProofType hashtype era)
  , ToExpr (ProofType hashtype era)
  , NFData (ProofType hashtype era)
  , NFData hashtype
  , Eq hashtype
  ) =>
  HasWitness hashtype era
  where
  type ProofType hashtype era
  type WitnessType hashtype era
  type TypeHashed hashtype era
  hash :: TypeHashed hashtype era -> hashtype
  mkWitness :: ProofType hashtype era -> WitnessType hashtype era
  getTypeHashed :: ProofType hashtype era -> TypeHashed hashtype era
  prettyHash :: hashtype -> Doc

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

-- | A WitBlock is designed to have five purposes
--   1) To efficiently constrain objects to be witnessed when using constraint generators
--      the (Set hashtype) allows efficient constraints like :: (member_ t) (lit (wbHash witblock))
--   2) To efficiently compute witnesses from a 'hashtype'
--      the (Map hashtype (ProofType hashtype era)) can be used like this
--      case Map.lookup hash (wbMap witblock) of
--        Just base -> mkWitness base
--        Nothing -> error "Missing hash. perhaps generator did not constrain the hash to be witnessed?"
--   3) When (HasWitness hashtype era) holds, the WitBlock can be computed from only [ProofType hashtype era]
--      using 'getTypeHashed'. This makes Gen and CBOR instances, especially easy. We compute only with
--      [ProofType hashtype era] and then reconstruct the rest
--   4) WitBlock is a Monoid, so we can combine them easily
--   5) We can easily make (Gen (WitBlock t era)), so we can make them for testing.
data WitBlock t era where
  WitBlock :: (Era era, HasWitness t era) => Set t -> Map t (ProofType t era) -> WitBlock t era

instance ToExpr t => ToExpr (WitBlock t era) where
  toExpr :: WitBlock t era -> Expr
toExpr (WitBlock Set t
x Map t (ProofType t era)
y) = String -> [Expr] -> Expr
Tree.App String
"WitBlock" [forall a. ToExpr a => a -> Expr
toExpr Set t
x, forall a. ToExpr a => a -> Expr
toExpr Map t (ProofType t era)
y]

wbHash :: WitBlock t era -> Set t
wbHash :: forall t era. WitBlock t era -> Set t
wbHash (WitBlock Set t
x Map t (ProofType t era)
_) = Set t
x
wbMap :: WitBlock t era -> Map t (ProofType t era)
wbMap :: forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (WitBlock Set t
_ Map t (ProofType t era)
y) = Map t (ProofType t era)
y

-- | when we print a WitBlock, we are only interested in the hashes, not the witnesses
instance ToExpr t => Show (WitBlock t era) where
  show :: WitBlock t era -> String
show (WitBlock Set t
hashset Map t (ProofType t era)
_) = forall a. Show a => a -> String
show (forall x. ToExpr x => x -> Doc
prettyE Set t
hashset)

instance NFData (WitBlock t era) where
  rnf :: WitBlock t era -> ()
rnf (WitBlock Set t
x Map t (ProofType t era)
y) = forall a b. NFData a => a -> b -> b
deepseq (forall a. NFData a => a -> ()
rnf Set t
x) (forall a b. NFData a => a -> b -> b
deepseq (forall a. NFData a => a -> ()
rnf Map t (ProofType t era)
y) ())

instance Eq (WitBlock t era) where
  (WitBlock Set t
x Map t (ProofType t era)
y) == :: WitBlock t era -> WitBlock t era -> Bool
== (WitBlock Set t
a Map t (ProofType t era)
b) = Set t
x forall a. Eq a => a -> a -> Bool
== Set t
a Bool -> Bool -> Bool
&& Map t (ProofType t era)
y forall a. Eq a => a -> a -> Bool
== Map t (ProofType t era)
b

-- ==========================================================================
-- (HasWitness t era) Instances for several different types of hash and hashed types

-- A short descriptive name for a long complicated thing
type BodyHash = SafeHash EraIndependentTxBody

-- ========
-- KeyHash and VKey
-- KeyPair seems to be missing a lot of instances, so we define them here

instance Era era => HasWitness (KeyHash 'Witness) era where
  type ProofType (KeyHash 'Witness) era = KeyPair 'Witness
  type WitnessType (KeyHash 'Witness) era = (BodyHash -> WitVKey 'Witness)
  type TypeHashed (KeyHash 'Witness) era = VKey 'Witness
  hash :: TypeHashed (KeyHash 'Witness) era -> KeyHash 'Witness
hash TypeHashed (KeyHash 'Witness) era
x = forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey TypeHashed (KeyHash 'Witness) era
x
  mkWitness :: ProofType (KeyHash 'Witness) era
-> WitnessType (KeyHash 'Witness) era
mkWitness ProofType (KeyHash 'Witness) era
keypair SafeHash EraIndependentTxBody
safehash = forall (kr :: KeyRole).
SafeHash EraIndependentTxBody -> KeyPair kr -> WitVKey 'Witness
mkWitnessVKey SafeHash EraIndependentTxBody
safehash ProofType (KeyHash 'Witness) era
keypair
  getTypeHashed :: ProofType (KeyHash 'Witness) era
-> TypeHashed (KeyHash 'Witness) era
getTypeHashed (KeyPair VKey 'Witness
x SignKeyDSIGN DSIGN
_) = VKey 'Witness
x
  prettyHash :: KeyHash 'Witness -> Doc
prettyHash KeyHash 'Witness
x = forall x. ToExpr x => x -> Doc
prettyE KeyHash 'Witness
x

-- ========
-- ScriptHash and Scripts

instance
  GenScript era =>
  HasWitness ScriptHash era
  where
  -- type ProofType ScriptHash era = NewScript era
  type ProofType ScriptHash era = Script era
  type WitnessType ScriptHash era = Script era
  type TypeHashed ScriptHash era = ProofType ScriptHash era
  hash :: TypeHashed ScriptHash era -> ScriptHash
hash (TypeHashed ScriptHash era
x) = forall era. EraScript era => Script era -> ScriptHash
hashScript TypeHashed ScriptHash era
x
  mkWitness :: ProofType ScriptHash era -> WitnessType ScriptHash era
mkWitness (ProofType ScriptHash era
script) = ProofType ScriptHash era
script
  getTypeHashed :: ProofType ScriptHash era -> TypeHashed ScriptHash era
getTypeHashed ProofType ScriptHash era
x = ProofType ScriptHash era
x
  prettyHash :: ScriptHash -> Doc
prettyHash ScriptHash
x = forall x. ToExpr x => x -> Doc
prettyE ScriptHash
x

-- ========
-- BootstrapAddress and SigningKey
-- BootstrapAddress is a convoluted hash of the SigningKey,
-- understood only by the Byron programmers (don't ask)

instance ToExpr SigningKey where toExpr :: SigningKey -> Expr
toExpr SigningKey
sk = String -> [Expr] -> Expr
Tree.App (forall a. Show a => a -> String
show SigningKey
sk) []

instance Era era => HasWitness BootstrapAddress era where
  type ProofType BootstrapAddress era = SigningKey
  type WitnessType BootstrapAddress era = (BodyHash -> BootstrapWitness)
  type TypeHashed BootstrapAddress era = SigningKey

  -- \| Don't ask about this, its related to the magic genAddrPair, which, like
  --   all things Byron, I don't understand. It generates a Byron address and
  --   its signing key for test purposes, and the signing key, uniquely determines
  --   the Byron address (for Testnet) as defined in method 'hash' below. I am certain, this
  --   is not how Byron address work in real life, but it works for test purposes.
  hash :: TypeHashed BootstrapAddress era -> BootstrapAddress
hash TypeHashed BootstrapAddress era
signkey =
    let verificationKey :: VerificationKey
verificationKey = SigningKey -> VerificationKey
toVerification TypeHashed BootstrapAddress era
signkey
        asd :: AddrSpendingData
asd = VerificationKey -> AddrSpendingData
Byron.VerKeyASD VerificationKey
verificationKey
        attrs :: AddrAttributes
attrs =
          Maybe HDAddressPayload -> NetworkMagic -> AddrAttributes
Byron.AddrAttributes
            (forall a. a -> Maybe a
Just (ByteString -> HDAddressPayload
Byron.HDAddressPayload ByteString
"a compressed lenna.png"))
            (Word32 -> NetworkMagic
Byron.NetworkTestnet Word32
0)
     in Address -> BootstrapAddress
BootstrapAddress (AddrSpendingData -> AddrAttributes -> Address
Byron.makeAddress AddrSpendingData
asd AddrAttributes
attrs)
  mkWitness :: ProofType BootstrapAddress era -> WitnessType BootstrapAddress era
mkWitness ProofType BootstrapAddress era
signkey SafeHash EraIndependentTxBody
bodyhash =
    let bootAddr :: BootstrapAddress
bootAddr = forall hashtype era.
HasWitness hashtype era =>
TypeHashed hashtype era -> hashtype
hash @BootstrapAddress @era ProofType BootstrapAddress era
signkey
     in Hash HASH EraIndependentTxBody
-> SigningKey -> Attributes AddrAttributes -> BootstrapWitness
makeBootstrapWitness
          (forall i. SafeHash i -> Hash HASH i
extractHash SafeHash EraIndependentTxBody
bodyhash)
          ProofType BootstrapAddress era
signkey
          (Address -> Attributes AddrAttributes
Byron.addrAttributes (BootstrapAddress -> Address
unBootstrapAddress BootstrapAddress
bootAddr))
  getTypeHashed :: ProofType BootstrapAddress era -> TypeHashed BootstrapAddress era
getTypeHashed ProofType BootstrapAddress era
signkey = ProofType BootstrapAddress era
signkey
  prettyHash :: BootstrapAddress -> Doc
prettyHash BootstrapAddress
x = forall x. ToExpr x => x -> Doc
prettyE BootstrapAddress
x

-- ========
-- DataHash and Data
-- note the type synonym
-- type DataHash = SafeHash c EraIndependentData

instance EraScript era => HasWitness DataHash era where
  type ProofType DataHash era = Data era
  type WitnessType DataHash era = Data era
  type TypeHashed DataHash era = Data era
  hash :: TypeHashed DataHash era -> DataHash
hash TypeHashed DataHash era
x = forall era. Data era -> DataHash
hashData TypeHashed DataHash era
x
  mkWitness :: ProofType DataHash era -> WitnessType DataHash era
mkWitness ProofType DataHash era
script = ProofType DataHash era
script
  getTypeHashed :: ProofType DataHash era -> TypeHashed DataHash era
getTypeHashed ProofType DataHash era
x = ProofType DataHash era
x
  prettyHash :: DataHash -> Doc
prettyHash DataHash
x = forall x. ToExpr x => x -> Doc
prettyE DataHash
x

-- ==============================================
-- The WitUniv type is 4 WitBlocks, there are some missing instances

data WitUniv era
  = WitUniv
  { forall era. WitUniv era -> Int
wvSize :: Int
  , forall era. WitUniv era -> WitBlock (KeyHash 'Witness) era
wvVKey :: WitBlock (KeyHash 'Witness) era
  , forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot :: WitBlock (BootstrapAddress) era
  , forall era. WitUniv era -> WitBlock ScriptHash era
wvScript :: WitBlock (ScriptHash) era
  , forall era. WitUniv era -> WitBlock DataHash era
wvDats :: WitBlock (DataHash) era
  }
  deriving (WitUniv era -> WitUniv era -> Bool
forall era. WitUniv era -> WitUniv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WitUniv era -> WitUniv era -> Bool
$c/= :: forall era. WitUniv era -> WitUniv era -> Bool
== :: WitUniv era -> WitUniv era -> Bool
$c== :: forall era. WitUniv era -> WitUniv era -> Bool
Eq, forall era. WitUniv era -> ()
forall a. (a -> ()) -> NFData a
rnf :: WitUniv era -> ()
$crnf :: forall era. WitUniv era -> ()
NFData, forall era. [WitUniv era] -> Expr
forall era. WitUniv era -> Expr
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
listToExpr :: [WitUniv era] -> Expr
$clistToExpr :: forall era. [WitUniv era] -> Expr
toExpr :: WitUniv era -> Expr
$ctoExpr :: forall era. WitUniv era -> Expr
ToExpr, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (WitUniv era) x -> WitUniv era
forall era x. WitUniv era -> Rep (WitUniv era) x
$cto :: forall era x. Rep (WitUniv era) x -> WitUniv era
$cfrom :: forall era x. WitUniv era -> Rep (WitUniv era) x
Generic)

instance Show (WitUniv era) where show :: WitUniv era -> String
show WitUniv era
x = forall a. Show a => a -> String
show (forall x. ToExpr x => x -> Doc
prettyE WitUniv era
x)

instance Era era => EncCBOR (WitUniv era) where
  encCBOR :: WitUniv era -> Encoding
encCBOR (WitUniv Int
n WitBlock (KeyHash 'Witness) era
w WitBlock BootstrapAddress era
x WitBlock ScriptHash era
y WitBlock DataHash era
z) = forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$ forall t. t -> Encode ('Closed 'Dense) t
Rec forall era.
Int
-> WitBlock (KeyHash 'Witness) era
-> WitBlock BootstrapAddress era
-> WitBlock ScriptHash era
-> WitBlock DataHash era
-> WitUniv era
WitUniv forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Int
n forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To WitBlock (KeyHash 'Witness) era
w forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To WitBlock BootstrapAddress era
x forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To WitBlock ScriptHash era
y forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To WitBlock DataHash era
z

-- ====================================================================
-- Purpose 1) To efficiently constrain objects to be witnessed when using constraint generators
-- the (Set hashtype) allows efficient constraints like :: (member_ t) (lit (wbHash witblock))

explainWit :: String -> WitUniv era -> Specification t -> Specification t
explainWit :: forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
str (WitUniv Int
n WitBlock (KeyHash 'Witness) era
_ WitBlock BootstrapAddress era
_ WitBlock ScriptHash era
_ WitBlock DataHash era
_) Specification t
spec =
  forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec
    [String
"While witnessing " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" with WitUniv of size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n]
    Specification t
spec

witKeyHashSpec ::
  forall era krole.
  Typeable krole =>
  WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec :: forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"keyhash :: (KeyHash r c)" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$
      \ Term (KeyHash krole)
[var|keyhash|] ->
        forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"witnessing " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (KeyHash krole)
keyhash)) forall a b. (a -> b) -> a -> b
$
          forall deps. TermD deps Bool -> PredD deps
Assert forall a b. (a -> b) -> a -> b
$
            forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ (forall a b.
(HasSpec a, HasSpec b, CoercibleLike a b) =>
Term a -> Term b
coerce_ Term (KeyHash krole)
keyhash) (forall a. HasSpec a => a -> Term a
lit (forall t era. WitBlock t era -> Set t
wbHash (forall era. WitUniv era -> WitBlock (KeyHash 'Witness) era
wvVKey WitUniv era
univ)))

witScriptHashSpec ::
  forall era.
  WitUniv era -> Specification (ScriptHash)
witScriptHashSpec :: forall era. WitUniv era -> Specification ScriptHash
witScriptHashSpec WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"scripthash :: ScriptHash" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$
      \ Term ScriptHash
[var|scripthash|] -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term ScriptHash
scripthash (forall a. HasSpec a => a -> Term a
lit (forall t era. WitBlock t era -> Set t
wbHash (forall era. WitUniv era -> WitBlock ScriptHash era
wvScript WitUniv era
univ)))

witBootstrapAddress ::
  forall era.
  WitUniv era -> Specification (BootstrapAddress)
witBootstrapAddress :: forall era. WitUniv era -> Specification BootstrapAddress
witBootstrapAddress WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"bootAddr :: BootstrapAddress" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$
      \ Term BootstrapAddress
[var|bootAddr|] -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term BootstrapAddress
bootAddr (forall a. HasSpec a => a -> Term a
lit (forall t era. WitBlock t era -> Set t
wbHash (forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
univ)))

witCredSpec ::
  forall era krole.
  Typeable krole =>
  WitUniv era -> Specification (Credential krole)
witCredSpec :: forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"cred :: (Credential c)" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (Credential krole)
[var|cred|] ->
      [ (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Credential krole)
cred)
          -- ScriptHash c -> Credential
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term ScriptHash
[var|scripthash|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ScriptHash
scripthash (forall era. WitUniv era -> Specification ScriptHash
witScriptHashSpec WitUniv era
univ))
          -- KeyHash kr c -> Credential
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash krole)
[var|keyhash|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash krole)
keyhash (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
      ]

witDRepSpec ::
  forall era.
  WitUniv era -> Specification (DRep)
witDRepSpec :: forall era. WitUniv era -> Specification DRep
witDRepSpec WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"drep :: (DRep c)" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term DRep
[var|drep|] ->
      [ (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term DRep
drep)
          -- KeyHash kr c -> Drep
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'DRepRole)
[var|keyhash|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'DRepRole)
keyhash (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
          -- ScriptHash c -> DRep
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \ Term ScriptHash
[var|scripthash|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ScriptHash
scripthash (forall era. WitUniv era -> Specification ScriptHash
witScriptHashSpec WitUniv era
univ))
          -- DRepAlwaysObstain
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> forall p. IsPred p => p -> Pred
assert Bool
True)
          -- DRepAlwaysNoConfidence
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> forall p. IsPred p => p -> Pred
assert Bool
True)
      ]

-- | Used only in Withdrawals, other RewardAccounts, not being withdrawn do not need witnessing
witRewardAccountSpec ::
  forall era.
  WitUniv era -> Specification (RewardAccount)
witRewardAccountSpec :: forall era. WitUniv era -> Specification RewardAccount
witRewardAccountSpec WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"rewaccount :: (RewardAccount c)" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term RewardAccount
[var|rewaccount|] ->
      forall p a.
(IsProductType a, IsPred p, GenericRequires a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewaccount forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] Term (Credential 'Staking)
[var|raCred|] ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Network
network forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit (Network
Testnet)
        , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
raCred (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec @era WitUniv era
univ)
        ]

owners_ ::
  Term PoolParams -> Term (Set (KeyHash 'Staking))
owners_ :: Term PoolParams -> Term (Set (KeyHash 'Staking))
owners_ = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @6

witPoolParamsSpec ::
  forall era.
  WitUniv era -> Specification PoolParams
witPoolParamsSpec :: forall era. WitUniv era -> Specification PoolParams
witPoolParamsSpec WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"poolparams :: (PoolParams c)" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term PoolParams
[var|poolparams|] ->
      [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term PoolParams -> Term (Set (KeyHash 'Staking))
owners_ Term PoolParams
poolparams) forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'Staking)
[var|ownerKeyHash|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'Staking)
ownerKeyHash (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ)
      , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term PoolParams -> Term (Set (KeyHash 'Staking))
owners_ Term PoolParams
poolparams) (forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
1 Integer
3))
      ]

witGenDelegPairSpec ::
  forall era.
  WitUniv era -> Specification (GenDelegPair)
witGenDelegPairSpec :: forall era. WitUniv era -> Specification GenDelegPair
witGenDelegPairSpec WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"gdpair :: (GenDelegPair  c)" WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term GenDelegPair
[var|gdpair|] ->
      forall p a.
(IsProductType a, IsPred p, GenericRequires a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegPair
gdpair forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'GenesisDelegate)
[var|keyhash|] Term (VRFVerKeyHash 'GenDelegVRF)
[var|_hash|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'GenesisDelegate)
keyhash (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ)

-- | Constrains all the Certificate Authors. Sometimes thay are keyHashes, and sometimes Credentials
witShelleyTxCert ::
  forall era.
  Era era =>
  WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert :: forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit (String
"txcert :: (ShelleyTxCert " forall a. [a] -> [a] -> [a]
++ String
"typeRep (Proxy @era)" forall a. [a] -> [a] -> [a]
++ String
")") WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (ShelleyTxCert era)
[var|txcert|] ->
      (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (ShelleyTxCert era)
txcert)
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
5 forall a b. (a -> b) -> a -> b
$ \Term ShelleyDelegCert
delegcert ->
            (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term ShelleyDelegCert
delegcert)
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
_register -> forall deps. PredD deps
TruePred :: Pred)
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
unregisterAuthor -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
unregisterAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
delegateAuthor TermD Deps (KeyHash 'StakePool)
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
delegateAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
        )
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term PoolCert
poolcert ->
            (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term PoolCert
poolcert)
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term PoolParams
registerPoolParams -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolParams
registerPoolParams (forall era. WitUniv era -> Specification PoolParams
witPoolParamsSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps (KeyHash 'StakePool)
retirePoolAuthor TermD Deps EpochNo
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies TermD Deps (KeyHash 'StakePool)
retirePoolAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
        )
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term GenesisDelegCert
genesiscert -> forall p a.
(IsProductType a, IsPred p, GenericRequires a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenesisDelegCert
genesiscert forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'Genesis)
authorkey Term (KeyHash 'GenesisDelegate)
_ Term (VRFVerKeyHash 'GenDelegVRF)
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'Genesis)
authorkey (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ)
        )
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \TermD Deps MIRCert
_mircert -> forall deps. NonEmpty String -> PredD deps
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"NO MIR") :: Pred)

-- | Constrains all the Certificate Authors. Sometimes thay are keyHashes, and sometimes Credentials
witConwayTxCert ::
  forall era.
  Era era =>
  WitUniv era -> Specification (ConwayTxCert era)
witConwayTxCert :: forall era.
Era era =>
WitUniv era -> Specification (ConwayTxCert era)
witConwayTxCert WitUniv era
univ =
  forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit (String
"txcert :: (ConwayTxCert " forall a. [a] -> [a] -> [a]
++ String
"typeRep (Proxy @era)" forall a. [a] -> [a] -> [a]
++ String
")") WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (ConwayTxCert era)
[var|txcert|] ->
      (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (ConwayTxCert era)
txcert)
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ConwayDelegCert
delegcert ->
            (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term ConwayDelegCert
delegcert)
              ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
registerAuthor Term (StrictMaybe Coin)
deposit ->
                  (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (StrictMaybe Coin)
deposit)
                    (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> forall deps. PredD deps
TruePred :: Pred)
                    (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps Coin
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
registerAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              )
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
unregisterAuthor Term (StrictMaybe Coin)
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
unregisterAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
delegateAuthor TermD Deps Delegatee
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
delegateAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
registerdelegateAuthor TermD Deps Delegatee
_ TermD Deps Coin
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
registerdelegateAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
        )
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term PoolCert
poolcert ->
            (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term PoolCert
poolcert)
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term PoolParams
registerPoolParams -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolParams
registerPoolParams (forall era. WitUniv era -> Specification PoolParams
witPoolParamsSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps (KeyHash 'StakePool)
retirePoolAuthor TermD Deps EpochNo
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies TermD Deps (KeyHash 'StakePool)
retirePoolAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
        )
        ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ConwayGovCert
govcert ->
            (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term ConwayGovCert
govcert)
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
regdrepAuthor TermD Deps Coin
_ TermD Deps (StrictMaybe Anchor)
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
regdrepAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
unregdrepAuthor TermD Deps Coin
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
unregdrepAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
updatedrepAuthor TermD Deps (StrictMaybe Anchor)
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
updatedrepAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'ColdCommitteeRole)
authorizeAuthor TermD Deps (Credential 'HotCommitteeRole)
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'ColdCommitteeRole)
authorizeAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Credential 'ColdCommitteeRole)
resignAuthor TermD Deps (StrictMaybe Anchor)
_ -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'ColdCommitteeRole)
resignAuthor (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
        )

-- =====================================================================
-- Purpose 2) To efficiently compute witnesses from a 'hashtype'
-- the (Map hashtype (ProofType hashtype era)) can be used like this
--     case Map.lookup hash (wbMap witblock) of
--        Just base -> mkWitness base
--        Nothing -> error "Missing hash. perhaps generator did not constrain the hash to be witnessed?"

witnessBootAddr ::
  forall era.
  EraTxWits era =>
  BodyHash -> BootstrapAddress -> WitUniv era -> TxWits era
witnessBootAddr :: forall era.
EraTxWits era =>
SafeHash EraIndependentTxBody
-> BootstrapAddress -> WitUniv era -> TxWits era
witnessBootAddr SafeHash EraIndependentTxBody
bodyhash BootstrapAddress
bootaddr WitUniv era
wu = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BootstrapAddress
bootaddr (forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
wu)) of
  Just SigningKey
x ->
    (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era)
      forall a b. a -> (a -> b) -> b
& forall era.
EraTxWits era =>
Lens' (TxWits era) (Set BootstrapWitness)
bootAddrTxWitsL
        forall s t a b. ASetter s t a b -> b -> s -> t
.~ (forall a. a -> Set a
Set.singleton (forall hashtype era.
HasWitness hashtype era =>
ProofType hashtype era -> WitnessType hashtype era
mkWitness @(BootstrapAddress) @era SigningKey
x SafeHash EraIndependentTxBody
bodyhash))
  Maybe SigningKey
Nothing -> forall a. HasCallStack => String -> a
error (String
"missing BootstrapAddress in WitUnv " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BootstrapAddress
bootaddr)

witnessKeyHash ::
  forall era.
  EraTxWits era =>
  BodyHash -> KeyHash 'Witness -> WitUniv era -> TxWits era
witnessKeyHash :: forall era.
EraTxWits era =>
SafeHash EraIndependentTxBody
-> KeyHash 'Witness -> WitUniv era -> TxWits era
witnessKeyHash SafeHash EraIndependentTxBody
bodyhash KeyHash 'Witness
keyhash WitUniv era
wu = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Witness
keyhash (forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (forall era. WitUniv era -> WitBlock (KeyHash 'Witness) era
wvVKey WitUniv era
wu)) of
  Just KeyPair 'Witness
x ->
    (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era)
      forall a b. a -> (a -> b) -> b
& forall era.
EraTxWits era =>
Lens' (TxWits era) (Set (WitVKey 'Witness))
addrTxWitsL
        forall s t a b. ASetter s t a b -> b -> s -> t
.~ (forall a. a -> Set a
Set.singleton (forall hashtype era.
HasWitness hashtype era =>
ProofType hashtype era -> WitnessType hashtype era
mkWitness @(KeyHash 'Witness) @era KeyPair 'Witness
x SafeHash EraIndependentTxBody
bodyhash))
  Maybe (KeyPair 'Witness)
Nothing -> forall a. HasCallStack => String -> a
error (String
"missing key hash in WitUnv " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show KeyHash 'Witness
keyhash)

witnessScriptHash ::
  forall era. EraTxWits era => ScriptHash -> WitUniv era -> TxWits era
witnessScriptHash :: forall era.
EraTxWits era =>
ScriptHash -> WitUniv era -> TxWits era
witnessScriptHash ScriptHash
scripthash WitUniv era
wu = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash
scripthash (forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (forall era. WitUniv era -> WitBlock ScriptHash era
wvScript WitUniv era
wu)) of
  Just Script era
script -> (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era) forall a b. a -> (a -> b) -> b
& forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL forall s t a b. ASetter s t a b -> b -> s -> t
.~ (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ScriptHash
scripthash Script era
script forall k a. Map k a
Map.empty)
  Maybe (Script era)
Nothing -> forall a. HasCallStack => String -> a
error (String
"missing script hash in WitUnv " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ScriptHash
scripthash)

witnessDataHash ::
  forall era. AlonzoEraTxWits era => DataHash -> WitUniv era -> TxWits era
witnessDataHash :: forall era.
AlonzoEraTxWits era =>
DataHash -> WitUniv era -> TxWits era
witnessDataHash DataHash
datahash WitUniv era
wu = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup DataHash
datahash (forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (forall era. WitUniv era -> WitBlock DataHash era
wvDats WitUniv era
wu)) of
  Just Data era
d -> (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era) forall a b. a -> (a -> b) -> b
& forall era. AlonzoEraTxWits era => Lens' (TxWits era) (TxDats era)
datsTxWitsL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall era. Era era => Map DataHash (Data era) -> TxDats era
TxDats (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert DataHash
datahash Data era
d forall k a. Map k a
Map.empty)
  Maybe (Data era)
Nothing -> forall a. HasCallStack => String -> a
error (String
"missing data hash in WitUnv " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DataHash
datahash)

-- =========================================================
-- Purpose 3) When (HasWitness hashtype era) holds, the WitBlock can be computed from
-- only [ProofType hashtype era] using 'getTypeHashed'. This makes Gen and CBOR instances,
-- especially easy. We compute only with [ProofType hashtype era] and then reconstruct the rest

-- | Reconstruct a (WitBlock t era) from only a [ProofType t era]
blockFromProofList ::
  forall t era. (Era era, Ord t, HasWitness t era) => [ProofType t era] -> WitBlock t era
blockFromProofList :: forall t era.
(Era era, Ord t, HasWitness t era) =>
[ProofType t era] -> WitBlock t era
blockFromProofList [ProofType t era]
baselist =
  forall era t.
(Era era, HasWitness t era) =>
Set t -> Map t (ProofType t era) -> WitBlock t era
WitBlock
    (forall a. Ord a => [a] -> Set a
Set.fromList [t]
hashlist)
    (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [t]
hashlist [ProofType t era]
baselist))
  where
    hashlist :: [t]
hashlist = forall a b. (a -> b) -> [a] -> [b]
map (forall hashtype era.
HasWitness hashtype era =>
TypeHashed hashtype era -> hashtype
hash @t @era forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall hashtype era.
HasWitness hashtype era =>
ProofType hashtype era -> TypeHashed hashtype era
getTypeHashed @t @era) [ProofType t era]
baselist

-- ===============================================================
-- Purpose 4) WitBlock is a Monoid, so we can combine them easily

instance Ord t => Semigroup (WitBlock t era) where
  (WitBlock Set t
x Map t (ProofType t era)
y) <> :: WitBlock t era -> WitBlock t era -> WitBlock t era
<> (WitBlock Set t
a Map t (ProofType t era)
b) = forall era t.
(Era era, HasWitness t era) =>
Set t -> Map t (ProofType t era) -> WitBlock t era
WitBlock (Set t
x forall a. Semigroup a => a -> a -> a
<> Set t
a) (Map t (ProofType t era)
y forall a. Semigroup a => a -> a -> a
<> Map t (ProofType t era)
b)

instance (Era era, Ord t, HasWitness t era) => Monoid (WitBlock t era) where
  mempty :: WitBlock t era
mempty = (forall era t.
(Era era, HasWitness t era) =>
Set t -> Map t (ProofType t era) -> WitBlock t era
WitBlock forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty)

-- | Easy to extend Monoid from WitBlock to WitUniv
instance Era era => Semigroup (WitUniv era) where
  WitUniv era
x <> :: WitUniv era -> WitUniv era -> WitUniv era
<> WitUniv era
y =
    WitUniv
      { wvSize :: Int
wvSize = forall a. Ord a => a -> a -> a
min (forall era. WitUniv era -> Int
wvSize WitUniv era
x) (forall era. WitUniv era -> Int
wvSize WitUniv era
y)
      , wvVKey :: WitBlock (KeyHash 'Witness) era
wvVKey = forall era. WitUniv era -> WitBlock (KeyHash 'Witness) era
wvVKey WitUniv era
x forall a. Semigroup a => a -> a -> a
<> forall era. WitUniv era -> WitBlock (KeyHash 'Witness) era
wvVKey WitUniv era
y
      , wvBoot :: WitBlock BootstrapAddress era
wvBoot = forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
x forall a. Semigroup a => a -> a -> a
<> forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
y
      , wvScript :: WitBlock ScriptHash era
wvScript = forall era. WitUniv era -> WitBlock ScriptHash era
wvScript WitUniv era
x forall a. Semigroup a => a -> a -> a
<> forall era. WitUniv era -> WitBlock ScriptHash era
wvScript WitUniv era
y
      , wvDats :: WitBlock DataHash era
wvDats = forall era. WitUniv era -> WitBlock DataHash era
wvDats WitUniv era
x forall a. Semigroup a => a -> a -> a
<> forall era. WitUniv era -> WitBlock DataHash era
wvDats WitUniv era
y
      }

instance (EraScript era, HasWitness (ScriptHash) era) => Monoid (WitUniv era) where
  mempty :: WitUniv era
mempty = WitUniv {wvSize :: Int
wvSize = Int
0, wvVKey :: WitBlock (KeyHash 'Witness) era
wvVKey = forall a. Monoid a => a
mempty, wvBoot :: WitBlock BootstrapAddress era
wvBoot = forall a. Monoid a => a
mempty, wvScript :: WitBlock ScriptHash era
wvScript = forall a. Monoid a => a
mempty, wvDats :: WitBlock DataHash era
wvDats = forall a. Monoid a => a
mempty}

-- =======================================================================
-- Purpose 5) We can easily to make (Gen (WitBlock t era)), so we can make them for testing.
-- this is facilitated by the methods of the (HasWitness t era) instances
-- and the special property that WitBlock can be computed from [ProofList]

genWitBlock ::
  forall t era.
  (Era era, Ord t, HasWitness t era) => Int -> Gen (ProofType t era) -> Gen (WitBlock t era)
genWitBlock :: forall t era.
(Era era, Ord t, HasWitness t era) =>
Int -> Gen (ProofType t era) -> Gen (WitBlock t era)
genWitBlock Int
n Gen (ProofType t era)
g = forall t era.
(Era era, Ord t, HasWitness t era) =>
[ProofType t era] -> WitBlock t era
blockFromProofList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen (ProofType t era)
g

instance (Era era, Typeable t) => EncCBOR (WitBlock t era) where
  encCBOR :: WitBlock t era -> Encoding
encCBOR (WitBlock Set t
_ Map t (ProofType t era)
m) = forall a. EncCBOR a => a -> Encoding
encCBOR (forall k a. Map k a -> [a]
Map.elems Map t (ProofType t era)
m)

genWitUniv ::
  forall era.
  (GenScript era, HasWitness (ScriptHash) era) =>
  Int -> Gen (WitUniv era)
genWitUniv :: forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
n =
  forall era.
Int
-> WitBlock (KeyHash 'Witness) era
-> WitBlock BootstrapAddress era
-> WitBlock ScriptHash era
-> WitBlock DataHash era
-> WitUniv era
WitUniv Int
n
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t era.
(Era era, Ord t, HasWitness t era) =>
Int -> Gen (ProofType t era) -> Gen (WitBlock t era)
genWitBlock Int
n (forall a. Arbitrary a => Gen a
arbitrary @(KeyPair 'Witness))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t era.
(Era era, Ord t, HasWitness t era) =>
Int -> Gen (ProofType t era) -> Gen (WitBlock t era)
genWitBlock Int
n (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network -> Gen (BootstrapAddress, SigningKey)
genAddrPair Network
Testnet)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t era.
(Era era, Ord t, HasWitness t era) =>
Int -> Gen (ProofType t era) -> Gen (WitBlock t era)
genWitBlock Int
n (forall era. GenScript era => Gen (Script era)
genScript @era)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t era.
(Era era, Ord t, HasWitness t era) =>
Int -> Gen (ProofType t era) -> Gen (WitBlock t era)
genWitBlock Int
n (forall a. Arbitrary a => Gen a
arbitrary @(Data era))

-- Use this for small tests only (otherwise increase from 100 to something larger)
-- or use (genWitUniv n) instead of arbitrary for some bigger 'n'
instance
  (HasWitness (ScriptHash) era, GenScript era) =>
  Arbitrary (WitUniv era)
  where
  arbitrary :: Gen (WitUniv era)
arbitrary = forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
100

-- ==================================================================================
-- Generating random native-scripts in every era. Needed to generate a random WitUniv)

genNestedMultiSig :: forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig :: forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig Int
depth
  | Int
depth forall a. Ord a => a -> a -> Bool
> Int
0 =
      forall a. HasCallStack => [Gen a] -> Gen a
oneof forall a b. (a -> b) -> a -> b
$
        [Gen (NativeScript era)]
nonRecTimelocks forall a. [a] -> [a] -> [a]
++ [Int -> Gen (NativeScript era)
requireAllOf Int
depth, Int -> Gen (NativeScript era)
requireAnyOf Int
depth, Int -> Gen (NativeScript era)
requireMOf Int
depth]
  | Bool
otherwise = forall a. HasCallStack => [Gen a] -> Gen a
oneof [Gen (NativeScript era)]
nonRecTimelocks
  where
    nonRecTimelocks :: [Gen (NativeScript era)]
nonRecTimelocks = [Gen (NativeScript era)
requireSignature]
    requireSignature :: Gen (NativeScript era)
requireSignature = forall era.
ShelleyEraScript era =>
KeyHash 'Witness -> NativeScript era
RequireSignature @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (KeyHash 'Witness)
genKeyHash
    requireAllOf :: Int -> Gen (NativeScript era)
requireAllOf Int
k = do
      Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
4)
      forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAllOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> StrictSeq a
Seq.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig @era (Int
k forall a. Num a => a -> a -> a
- Int
1))
    requireAnyOf :: Int -> Gen (NativeScript era)
requireAnyOf Int
k = do
      Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
4)
      forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAnyOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> StrictSeq a
Seq.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig @era (Int
k forall a. Num a => a -> a -> a
- Int
1))
    requireMOf :: Int -> Gen (NativeScript era)
requireMOf Int
k = do
      Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
4)
      Int
m <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
n)
      forall era.
ShelleyEraScript era =>
Int -> StrictSeq (NativeScript era) -> NativeScript era
RequireMOf Int
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> StrictSeq a
Seq.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig @era (Int
k forall a. Num a => a -> a -> a
- Int
1))
    genKeyHash :: Gen (KeyHash 'Witness)
    genKeyHash :: Gen (KeyHash 'Witness)
genKeyHash = forall a. Arbitrary a => Gen a
arbitrary

genNestedTimelock :: forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock :: forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock Int
depth
  | Int
depth forall a. Ord a => a -> a -> Bool
> Int
0 =
      forall a. HasCallStack => [Gen a] -> Gen a
oneof forall a b. (a -> b) -> a -> b
$
        [Gen (NativeScript era)]
nonRecTimelocks forall a. [a] -> [a] -> [a]
++ [Int -> Gen (NativeScript era)
requireAllOf Int
depth, Int -> Gen (NativeScript era)
requireAnyOf Int
depth, Int -> Gen (NativeScript era)
requireMOf Int
depth]
  | Bool
otherwise = forall a. HasCallStack => [Gen a] -> Gen a
oneof [Gen (NativeScript era)]
nonRecTimelocks
  where
    nonRecTimelocks :: [Gen (NativeScript era)]
nonRecTimelocks =
      [ Gen (NativeScript era)
requireSignature
      , forall {era}.
AllegraEraScript era =>
SlotNo -> Gen (NativeScript era)
requireTimeStart (Word64 -> SlotNo
SlotNo forall a. Bounded a => a
minBound)
      , forall {era}.
AllegraEraScript era =>
SlotNo -> Gen (NativeScript era)
requireTimeExpire (Word64 -> SlotNo
SlotNo forall a. Bounded a => a
maxBound)
      ]
    requireSignature :: Gen (NativeScript era)
requireSignature = forall era.
ShelleyEraScript era =>
KeyHash 'Witness -> NativeScript era
RequireSignature forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (KeyHash 'Witness)
genKeyHash
    requireAllOf :: Int -> Gen (NativeScript era)
requireAllOf Int
k = do
      Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
3) -- lift nonNegativeSingleDigitInt
      forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAllOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> StrictSeq a
Seq.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @era (Int
k forall a. Num a => a -> a -> a
- Int
1))
    requireAnyOf :: Int -> Gen (NativeScript era)
requireAnyOf Int
k = do
      Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
3) -- lift positiveSingleDigitInt
      forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAnyOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> StrictSeq a
Seq.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @era (Int
k forall a. Num a => a -> a -> a
- Int
1))
    requireMOf :: Int -> Gen (NativeScript era)
requireMOf Int
k = do
      Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
3) -- lift nonNegativeSingleDigitInt
      Int
m <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
n)
      forall era.
ShelleyEraScript era =>
Int -> StrictSeq (NativeScript era) -> NativeScript era
RequireMOf Int
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> StrictSeq a
Seq.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @era (Int
k forall a. Num a => a -> a -> a
- Int
1))
    requireTimeStart :: SlotNo -> Gen (NativeScript era)
requireTimeStart (SlotNo Word64
validFrom) = do
      Word64
minSlotNo <- forall a. Random a => (a, a) -> Gen a
choose (forall a. Bounded a => a
minBound, Word64
validFrom)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era. AllegraEraScript era => SlotNo -> NativeScript era
RequireTimeStart (Word64 -> SlotNo
SlotNo Word64
minSlotNo)
    requireTimeExpire :: SlotNo -> Gen (NativeScript era)
requireTimeExpire (SlotNo Word64
validTill) = do
      Word64
maxSlotNo <- forall a. Random a => (a, a) -> Gen a
choose (Word64
validTill, forall a. Bounded a => a
maxBound)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era. AllegraEraScript era => SlotNo -> NativeScript era
RequireTimeExpire (Word64 -> SlotNo
SlotNo Word64
maxSlotNo)
    genKeyHash :: Gen (KeyHash 'Witness)
    genKeyHash :: Gen (KeyHash 'Witness)
genKeyHash = forall a. Arbitrary a => Gen a
arbitrary

-- =======================================================================
-- Tools for Parametric Witnessing
-- ==============================================================

-- | The class of things we know how to witness. This way you don't
--   have to remember long complicated names.
class Witnessed era t where
  witness :: WitUniv era -> Term t -> Pred

instance (Era era, Typeable r) => Witnessed era (KeyHash r) where
  witness :: WitUniv era -> Term (KeyHash r) -> Pred
witness WitUniv era
univ Term (KeyHash r)
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash r)
t (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ)

instance Era era => Witnessed era ScriptHash where
  witness :: WitUniv era -> Term ScriptHash -> Pred
witness WitUniv era
univ Term ScriptHash
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ScriptHash
t (forall era. WitUniv era -> Specification ScriptHash
witScriptHashSpec WitUniv era
univ)

instance (Era era, Typeable r) => Witnessed era (Credential r) where
  witness :: WitUniv era -> Term (Credential r) -> Pred
witness WitUniv era
univ Term (Credential r)
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential r)
t (forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ)

instance Era era => Witnessed era BootstrapAddress where
  witness :: WitUniv era -> Term BootstrapAddress -> Pred
witness WitUniv era
univ Term BootstrapAddress
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term BootstrapAddress
t (forall era. WitUniv era -> Specification BootstrapAddress
witBootstrapAddress WitUniv era
univ)

instance Era era => Witnessed era DRep where
  witness :: WitUniv era -> Term DRep -> Pred
witness WitUniv era
univ Term DRep
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term DRep
t (forall era. WitUniv era -> Specification DRep
witDRepSpec WitUniv era
univ)

instance Era era => Witnessed era RewardAccount where
  witness :: WitUniv era -> Term RewardAccount -> Pred
witness WitUniv era
univ Term RewardAccount
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term RewardAccount
t (forall era. WitUniv era -> Specification RewardAccount
witRewardAccountSpec WitUniv era
univ)

instance Era era => Witnessed era PoolParams where
  witness :: WitUniv era -> Term PoolParams -> Pred
witness WitUniv era
univ Term PoolParams
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolParams
t (forall era. WitUniv era -> Specification PoolParams
witPoolParamsSpec WitUniv era
univ)

instance Era era => Witnessed era GenDelegPair where
  witness :: WitUniv era -> Term GenDelegPair -> Pred
witness WitUniv era
univ Term GenDelegPair
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term GenDelegPair
t (forall era. WitUniv era -> Specification GenDelegPair
witGenDelegPairSpec WitUniv era
univ)

instance Era era => Witnessed era (ShelleyTxCert era) where
  witness :: WitUniv era -> Term (ShelleyTxCert era) -> Pred
witness WitUniv era
univ Term (ShelleyTxCert era)
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (ShelleyTxCert era)
t (forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert WitUniv era
univ)

instance Era era => Witnessed era (ConwayTxCert era) where
  witness :: WitUniv era -> Term (ConwayTxCert era) -> Pred
witness WitUniv era
univ Term (ConwayTxCert era)
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (ConwayTxCert era)
t (forall era.
Era era =>
WitUniv era -> Specification (ConwayTxCert era)
witConwayTxCert WitUniv era
univ)

instance EraSpecPParams era => Witnessed era (Committee era) where
  witness :: WitUniv era -> Term (Committee era) -> Pred
witness WitUniv era
univ Term (Committee era)
t = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Committee era)
t (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (Committee era)
committeeWitness WitUniv era
univ)

instance (Era era, HasSpec t, Ord t, Witnessed era t) => Witnessed era (Set t) where
  witness :: WitUniv era -> Term (Set t) -> Pred
witness WitUniv era
univ Term (Set t)
t =
    forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll
      Term (Set t)
t
      ( \Term t
x ->
          forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @(Set t))) forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed")) forall a b. (a -> b) -> a -> b
$
            forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term t
x
      )

instance (Era era, HasSpec t, Witnessed era t, IsNormalType t) => Witnessed era (StrictMaybe t) where
  witness :: WitUniv era -> Term (StrictMaybe t) -> Pred
witness WitUniv era
univ Term (StrictMaybe t)
t =
    (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (StrictMaybe t)
t)
      -- SNothing
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
      -- SJust
      ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term t
x ->
          forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain
            (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @(StrictMaybe t))) forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed"))
            (forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term t
x)
      )

instance (Era era, HasSpec t, Witnessed era t, IsNormalType t) => Witnessed era (Maybe t) where
  witness :: WitUniv era -> Term (Maybe t) -> Pred
witness WitUniv era
univ Term (Maybe t)
t =
    (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (Maybe t)
t)
      -- Nothing
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
      -- Just
      ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term t
x ->
          forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain
            (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @(Maybe t))) forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed"))
            (forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term t
x)
      )

instance
  (Era era, HasSpec t, HasSpec v, IsNormalType t, IsNormalType v, Ord t, Witnessed era t) =>
  Witnessed era (Map t v)
  where
  witness :: WitUniv era -> Term (Map t v) -> Pred
witness WitUniv era
univ Term (Map t v)
t =
    forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @(Map t v))) forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed")) forall a b. (a -> b) -> a -> b
$
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (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 t v)
t) (forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ)

instance (Era era, HasSpec t, Witnessed era t) => Witnessed era [t] where
  witness :: WitUniv era -> Term [t] -> Pred
witness WitUniv era
univ Term [t]
t =
    forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @([t]))) forall a. [a] -> [a] -> [a]
++ String
" instance of Witnessed")) forall a b. (a -> b) -> a -> b
$
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [t]
t (forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ)

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

-- | Parametric TxCert
class (EraTxCert era, HasSpec (TxCert era)) => EraSpecTxCert era where
  witTxCert :: WitUniv era -> Specification (TxCert era)

instance EraSpecTxCert ShelleyEra where
  witTxCert :: WitUniv ShelleyEra -> Specification (TxCert ShelleyEra)
witTxCert = forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert
instance EraSpecTxCert AllegraEra where
  witTxCert :: WitUniv AllegraEra -> Specification (TxCert AllegraEra)
witTxCert = forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert
instance EraSpecTxCert MaryEra where
  witTxCert :: WitUniv MaryEra -> Specification (TxCert MaryEra)
witTxCert = forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert
instance EraSpecTxCert AlonzoEra where
  witTxCert :: WitUniv AlonzoEra -> Specification (TxCert AlonzoEra)
witTxCert = forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert
instance EraSpecTxCert BabbageEra where
  witTxCert :: WitUniv BabbageEra -> Specification (TxCert BabbageEra)
witTxCert = forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert
instance EraSpecTxCert ConwayEra where
  witTxCert :: WitUniv ConwayEra -> Specification (TxCert ConwayEra)
witTxCert = forall era.
Era era =>
WitUniv era -> Specification (ConwayTxCert era)
witConwayTxCert

-- | Parametric Script
class
  ( EraScript era
  , ToExpr (NativeScript era)
  , NFData (Script era)
  , ToExpr (Script era)
  ) =>
  GenScript era
  where
  genScript :: Gen (Script era)

instance GenScript ShelleyEra where genScript :: Gen (Script ShelleyEra)
genScript = forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig Int
2
instance GenScript AllegraEra where genScript :: Gen (Script AllegraEra)
genScript = forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @AllegraEra Int
2
instance GenScript MaryEra where genScript :: Gen (Script MaryEra)
genScript = forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @MaryEra Int
2
instance GenScript AlonzoEra where genScript :: Gen (Script AlonzoEra)
genScript = forall era. EraScript era => NativeScript era -> Script era
fromNativeScript forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @AlonzoEra Int
2
instance GenScript BabbageEra where genScript :: Gen (Script BabbageEra)
genScript = forall era. EraScript era => NativeScript era -> Script era
fromNativeScript forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @BabbageEra Int
2
instance GenScript ConwayEra where genScript :: Gen (Script ConwayEra)
genScript = forall era. EraScript era => NativeScript era -> Script era
fromNativeScript forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. AllegraEraScript era => Int -> Gen (NativeScript era)
genNestedTimelock @ConwayEra Int
2

-- ===============================================================
-- examples
spec1 :: WitUniv ShelleyEra -> Specification (Set ScriptHash)
spec1 :: WitUniv ShelleyEra -> Specification (Set ScriptHash)
spec1 WitUniv ShelleyEra
univ =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (Set ScriptHash)
[var|setHash|] -> [forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set ScriptHash)
setHash forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
11, forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv ShelleyEra
univ Term (Set ScriptHash)
setHash]

go1 :: IO ()
go1 :: IO ()
go1 = do
  WitUniv ShelleyEra
univ <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ShelleyEra Int
5
  Set ScriptHash
ans <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ShelleyEra -> Specification (Set ScriptHash)
spec1 WitUniv ShelleyEra
univ)
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall x. ToExpr x => x -> Doc
prettyE Set ScriptHash
ans))

spec2 ::
  WitUniv ShelleyEra ->
  Set ScriptHash ->
  Specification (Set ScriptHash)
spec2 :: WitUniv ShelleyEra
-> Set ScriptHash -> Specification (Set ScriptHash)
spec2 WitUniv ShelleyEra
univ Set ScriptHash
big =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (Set ScriptHash)
[var|setHash|] ->
    [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall a. HasSpec a => a -> Term a
lit Set ScriptHash
big) Term (Set ScriptHash)
setHash
    , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv ShelleyEra
univ Term (Set ScriptHash)
setHash
    ]
go2 :: IO ()
go2 :: IO ()
go2 = do
  WitUniv ShelleyEra
univ <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ShelleyEra Int
5
  Set ScriptHash
big <- forall a. Gen a -> IO a
generate forall a. Arbitrary a => Gen a
arbitrary
  Set ScriptHash
ans <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ShelleyEra
-> Set ScriptHash -> Specification (Set ScriptHash)
spec2 WitUniv ShelleyEra
univ Set ScriptHash
big)
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall x. ToExpr x => x -> Doc
prettyE Set ScriptHash
ans))

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

conwayWitUniv :: Int -> WitUniv ConwayEra
conwayWitUniv :: Int -> WitUniv ConwayEra
conwayWitUniv Int
n = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
n

babbageWitUniv :: Int -> WitUniv BabbageEra
babbageWitUniv :: Int -> WitUniv BabbageEra
babbageWitUniv Int
n = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @BabbageEra Int
n

alonzoWitUniv :: Int -> WitUniv AlonzoEra
alonzoWitUniv :: Int -> WitUniv AlonzoEra
alonzoWitUniv Int
n = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @AlonzoEra Int
n

maryWitUniv :: Int -> WitUniv MaryEra
maryWitUniv :: Int -> WitUniv MaryEra
maryWitUniv Int
n = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @MaryEra Int
n

allegraWitUniv :: Int -> WitUniv AllegraEra
allegraWitUniv :: Int -> WitUniv AllegraEra
allegraWitUniv Int
n = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @AllegraEra Int
n

shelleyWitUniv :: Int -> WitUniv ShelleyEra
shelleyWitUniv :: Int -> WitUniv ShelleyEra
shelleyWitUniv Int
n = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ShelleyEra Int
n

class EraUniverse era where
  eraWitUniv :: Int -> WitUniv era

instance EraUniverse ConwayEra where eraWitUniv :: Int -> WitUniv ConwayEra
eraWitUniv = Int -> WitUniv ConwayEra
conwayWitUniv
instance EraUniverse BabbageEra where eraWitUniv :: Int -> WitUniv BabbageEra
eraWitUniv = Int -> WitUniv BabbageEra
babbageWitUniv
instance EraUniverse AlonzoEra where eraWitUniv :: Int -> WitUniv AlonzoEra
eraWitUniv = Int -> WitUniv AlonzoEra
alonzoWitUniv
instance EraUniverse MaryEra where eraWitUniv :: Int -> WitUniv MaryEra
eraWitUniv = Int -> WitUniv MaryEra
maryWitUniv
instance EraUniverse AllegraEra where eraWitUniv :: Int -> WitUniv AllegraEra
eraWitUniv = Int -> WitUniv AllegraEra
allegraWitUniv
instance EraUniverse ShelleyEra where eraWitUniv :: Int -> WitUniv ShelleyEra
eraWitUniv = Int -> WitUniv ShelleyEra
shelleyWitUniv

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

-- | Constrains just the parts that need witnessing in GovActionState
govActionStateWitness ::
  forall era.
  EraSpecPParams era =>
  WitUniv era -> Specification (GovActionState era)
govActionStateWitness :: forall era.
EraSpecPParams era =>
WitUniv era -> Specification (GovActionState era)
govActionStateWitness WitUniv era
univ = forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"Witnessing GovActionState"] forall a b. (a -> b) -> a -> b
$
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState era)
[var|govactstate|] ->
    forall p a.
(IsProductType a, IsPred p, GenericRequires a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (GovActionState era)
govactstate forall a b. (a -> b) -> a -> b
$
      \TermD Deps GovActionId
_gaid Term (Map (Credential 'HotCommitteeRole) Vote)
[var|comVotemap|] Term (Map (Credential 'DRepRole) Vote)
[var|drepVotemap|] Term (Map (KeyHash 'StakePool) Vote)
[var|poolVotemap|] Term (ProposalProcedure era)
[var|proposalProc|] TermD Deps EpochNo
_proposed TermD Deps EpochNo
_expires ->
        [ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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 (Credential 'HotCommitteeRole) Vote)
comVotemap)
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 (Credential 'HotCommitteeRole) Vote)
comVotemap) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Integer
3
        , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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 (Credential 'DRepRole) Vote)
drepVotemap)
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 (Credential 'DRepRole) Vote)
drepVotemap) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Integer
2
        , forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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 (KeyHash 'StakePool) Vote)
poolVotemap)
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 (KeyHash 'StakePool) Vote)
poolVotemap) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Integer
2
        , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (ProposalProcedure era)
proposalProc (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (ProposalProcedure era)
proposalProcedureWitness WitUniv era
univ)
        ]

-- | Constrains just the parts that need witnessing in GovAction
govActionWitness ::
  forall era.
  EraSpecPParams era =>
  WitUniv era -> Specification (GovAction era)
govActionWitness :: forall era.
EraSpecPParams era =>
WitUniv era -> Specification (GovAction era)
govActionWitness WitUniv era
univ = forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"Witnessing GovAction"] forall a b. (a -> b) -> a -> b
$
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (GovAction era)
[var|govaction|] ->
    (forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (GovAction era)
govaction)
      -- ParameterChange
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose era))
_ TermD Deps (PParamsUpdate era)
_ Term (StrictMaybe ScriptHash)
mhash -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (StrictMaybe ScriptHash)
mhash)
      -- HardFork
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'HardForkPurpose era))
_ TermD Deps ProtVer
_ -> Bool
True)
      -- TreasuryWithdrawals
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
rewacctmap Term (StrictMaybe ScriptHash)
mhash -> [forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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 RewardAccount Coin)
rewacctmap), forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (StrictMaybe ScriptHash)
mhash])
      -- NoConfidence
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose era))
_ -> Bool
True)
      -- UpdateCommitee
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose era))
_ Term (Set (Credential 'ColdCommitteeRole))
credSet Term (Map (Credential 'ColdCommitteeRole) EpochNo)
credMap TermD Deps UnitInterval
_ -> [forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Set (Credential 'ColdCommitteeRole))
credSet, forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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 (Credential 'ColdCommitteeRole) EpochNo)
credMap)])
      -- NewConstituion
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose era))
_ TermD Deps (Constitution era)
_ -> Bool
True)
      -- InfoAction
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)

-- | Constrains just the parts that need witnessing in ProposalProcedure
proposalProcedureWitness ::
  forall era.
  EraSpecPParams era =>
  WitUniv era -> Specification (ProposalProcedure era)
proposalProcedureWitness :: forall era.
EraSpecPParams era =>
WitUniv era -> Specification (ProposalProcedure era)
proposalProcedureWitness WitUniv era
univ =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (ProposalProcedure era)
[var|proposalProc|] ->
    forall p a.
(IsProductType a, IsPred p, GenericRequires a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposalProcedure era)
proposalProc forall a b. (a -> b) -> a -> b
$ \TermD Deps Coin
_dep Term RewardAccount
[var|returnAddr|] Term (GovAction era)
[var|govAction|] TermD Deps Anchor
_anchor ->
      [forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term RewardAccount
returnAddr, forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (GovAction era)
govAction (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (GovAction era)
govActionWitness WitUniv era
univ)]

-- | Constrains just the parts that need witnessing in Committee
committeeWitness ::
  EraSpecPParams era =>
  WitUniv era -> Specification (Committee era)
committeeWitness :: forall era.
EraSpecPParams era =>
WitUniv era -> Specification (Committee era)
committeeWitness WitUniv era
univ =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (Committee era)
[var|committee|] ->
    forall p a.
(IsProductType a, IsPred p, GenericRequires a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Committee era)
committee forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
[var|epochMap|] TermD Deps UnitInterval
_threshold ->
      [forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (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 (Credential 'ColdCommitteeRole) EpochNo)
epochMap), forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 (Credential 'ColdCommitteeRole) EpochNo)
epochMap) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Integer
3]

go9 :: IO ()
go9 :: IO ()
go9 = do
  WitUniv ConwayEra
univ <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
5
  Committee ConwayEra
ans <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (Committee era)
committeeWitness @ConwayEra WitUniv ConwayEra
univ)
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall x. ToExpr x => x -> Doc
prettyE Committee ConwayEra
ans))
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall x. ToExpr x => x -> Doc
prettyE WitUniv ConwayEra
univ))