{-# 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
  SigningKey -> Gen SigningKey
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (XPrv -> SigningKey
Byron.SigningKey (XPrv -> SigningKey) -> XPrv -> SigningKey
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString -> XPrv
forall passPhrase seed.
(ByteArrayAccess passPhrase, ByteArrayAccess seed) =>
seed -> passPhrase -> XPrv
Byron.generate ByteString
seed (ByteString
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
          (HDAddressPayload -> Maybe HDAddressPayload
forall a. a -> Maybe a
Just (ByteString -> HDAddressPayload
Byron.HDAddressPayload ByteString
"a compressed lenna.png"))
          NetworkMagic
byronNetwork
  (BootstrapAddress, SigningKey)
-> Gen (BootstrapAddress, SigningKey)
forall a. a -> Gen a
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)
SimpleRep (TxDats era)
m
  fromSimpleRep :: SimpleRep (TxDats era) -> TxDats era
fromSimpleRep SimpleRep (TxDats era)
m = Map DataHash (Data era) -> TxDats era
forall era. Era era => Map DataHash (Data era) -> TxDats era
TxDats Map DataHash (Data era)
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)
SimpleRep (Redeemers era)
m
  fromSimpleRep :: SimpleRep (Redeemers era) -> Redeemers era
fromSimpleRep SimpleRep (Redeemers era)
m = Map (PlutusPurpose AsIx era) (Data era, ExUnits) -> Redeemers era
forall era.
AlonzoEraScript era =>
Map (PlutusPurpose AsIx era) (Data era, ExUnits) -> Redeemers era
Redeemers Map (PlutusPurpose AsIx era) (Data era, ExUnits)
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)
_ = Specification (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)
_ = Gen (MultiSig era) -> GenT m (MultiSig era)
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen (MultiSig era) -> GenT m (MultiSig era))
-> Gen (MultiSig era) -> GenT m (MultiSig era)
forall a b. (a -> b) -> a -> b
$ Int -> Gen (NativeScript era)
forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig Int
2
  cardinalTypeSpec :: TypeSpec (MultiSig era) -> Specification Integer
cardinalTypeSpec TypeSpec (MultiSig era)
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
  shrinkWithTypeSpec :: TypeSpec (MultiSig era) -> MultiSig era -> [MultiSig era]
shrinkWithTypeSpec TypeSpec (MultiSig era)
_ = MultiSig era -> [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)
_ = Bool -> Pred
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" [Set t -> Expr
forall a. ToExpr a => a -> Expr
toExpr Set t
x, Map t (ProofType t era) -> Expr
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)
_) = Doc -> String
forall a. Show a => a -> String
show (Set t -> Doc
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 (Set t -> ()
forall a. NFData a => a -> ()
rnf Set t
x) (() -> () -> ()
forall a b. NFData a => a -> b -> b
deepseq (Map t (ProofType t era) -> ()
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 Set t -> Set t -> Bool
forall a. Eq a => a -> a -> Bool
== Set t
a Bool -> Bool -> Bool
&& Map t (ProofType t era)
y Map t (ProofType t era) -> Map t (ProofType t era) -> Bool
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 = VKey 'Witness -> KeyHash 'Witness
forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey VKey 'Witness
TypeHashed (KeyHash 'Witness) era
x
  mkWitness :: ProofType (KeyHash 'Witness) era
-> WitnessType (KeyHash 'Witness) era
mkWitness ProofType (KeyHash 'Witness) era
keypair SafeHash EraIndependentTxBody
safehash = SafeHash EraIndependentTxBody
-> KeyPair 'Witness -> WitVKey 'Witness
forall (kr :: KeyRole).
SafeHash EraIndependentTxBody -> KeyPair kr -> WitVKey 'Witness
mkWitnessVKey SafeHash EraIndependentTxBody
safehash KeyPair 'Witness
ProofType (KeyHash 'Witness) era
keypair
  getTypeHashed :: ProofType (KeyHash 'Witness) era
-> TypeHashed (KeyHash 'Witness) era
getTypeHashed (KeyPair VKey 'Witness
x SignKeyDSIGN DSIGN
_) = VKey 'Witness
TypeHashed (KeyHash 'Witness) era
x
  prettyHash :: KeyHash 'Witness -> Doc
prettyHash KeyHash 'Witness
x = KeyHash 'Witness -> Doc
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) = Script era -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript Script era
TypeHashed ScriptHash era
x
  mkWitness :: ProofType ScriptHash era -> WitnessType ScriptHash era
mkWitness (ProofType ScriptHash era
script) = ProofType ScriptHash era
WitnessType ScriptHash era
script
  getTypeHashed :: ProofType ScriptHash era -> TypeHashed ScriptHash era
getTypeHashed ProofType ScriptHash era
x = ProofType ScriptHash era
TypeHashed ScriptHash era
x
  prettyHash :: ScriptHash -> Doc
prettyHash ScriptHash
x = ScriptHash -> Doc
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 (SigningKey -> String
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 SigningKey
TypeHashed BootstrapAddress era
signkey
        asd :: AddrSpendingData
asd = VerificationKey -> AddrSpendingData
Byron.VerKeyASD VerificationKey
verificationKey
        attrs :: AddrAttributes
attrs =
          Maybe HDAddressPayload -> NetworkMagic -> AddrAttributes
Byron.AddrAttributes
            (HDAddressPayload -> Maybe HDAddressPayload
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
TypeHashed BootstrapAddress era
signkey
     in Hash HASH EraIndependentTxBody
-> SigningKey -> Attributes AddrAttributes -> BootstrapWitness
makeBootstrapWitness
          (SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash SafeHash EraIndependentTxBody
bodyhash)
          SigningKey
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
TypeHashed BootstrapAddress era
signkey
  prettyHash :: BootstrapAddress -> Doc
prettyHash BootstrapAddress
x = BootstrapAddress -> Doc
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 = Data era -> DataHash
forall era. Data era -> DataHash
hashData Data era
TypeHashed DataHash era
x
  mkWitness :: ProofType DataHash era -> WitnessType DataHash era
mkWitness ProofType DataHash era
script = ProofType DataHash era
WitnessType DataHash era
script
  getTypeHashed :: ProofType DataHash era -> TypeHashed DataHash era
getTypeHashed ProofType DataHash era
x = ProofType DataHash era
TypeHashed DataHash era
x
  prettyHash :: DataHash -> Doc
prettyHash DataHash
x = DataHash -> Doc
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
(WitUniv era -> WitUniv era -> Bool)
-> (WitUniv era -> WitUniv era -> Bool) -> Eq (WitUniv era)
forall era. WitUniv era -> WitUniv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era. WitUniv era -> WitUniv era -> Bool
== :: WitUniv era -> WitUniv era -> Bool
$c/= :: forall era. WitUniv era -> WitUniv era -> Bool
/= :: WitUniv era -> WitUniv era -> Bool
Eq, WitUniv era -> ()
(WitUniv era -> ()) -> NFData (WitUniv era)
forall era. WitUniv era -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall era. WitUniv era -> ()
rnf :: WitUniv era -> ()
NFData, [WitUniv era] -> Expr
WitUniv era -> Expr
(WitUniv era -> Expr)
-> ([WitUniv era] -> Expr) -> ToExpr (WitUniv era)
forall era. [WitUniv era] -> Expr
forall era. WitUniv era -> Expr
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: forall era. WitUniv era -> Expr
toExpr :: WitUniv era -> Expr
$clistToExpr :: forall era. [WitUniv era] -> Expr
listToExpr :: [WitUniv era] -> Expr
ToExpr, (forall x. WitUniv era -> Rep (WitUniv era) x)
-> (forall x. Rep (WitUniv era) x -> WitUniv era)
-> Generic (WitUniv era)
forall x. Rep (WitUniv era) x -> WitUniv era
forall x. WitUniv era -> Rep (WitUniv era) x
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
$cfrom :: forall era x. WitUniv era -> Rep (WitUniv era) x
from :: forall x. WitUniv era -> Rep (WitUniv era) x
$cto :: forall era x. Rep (WitUniv era) x -> WitUniv era
to :: forall x. Rep (WitUniv era) x -> WitUniv era
Generic)

instance Show (WitUniv era) where show :: WitUniv era -> String
show WitUniv era
x = Doc -> String
forall a. Show a => a -> String
show (WitUniv era -> Doc
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) = Encode ('Closed 'Dense) (WitUniv era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode ('Closed 'Dense) (WitUniv era) -> Encoding)
-> Encode ('Closed 'Dense) (WitUniv era) -> Encoding
forall a b. (a -> b) -> a -> b
$ (Int
 -> WitBlock (KeyHash 'Witness) era
 -> WitBlock BootstrapAddress era
 -> WitBlock ScriptHash era
 -> WitBlock DataHash era
 -> WitUniv era)
-> Encode
     ('Closed 'Dense)
     (Int
      -> WitBlock (KeyHash 'Witness) era
      -> WitBlock BootstrapAddress era
      -> WitBlock ScriptHash era
      -> WitBlock DataHash era
      -> WitUniv era)
forall t. t -> Encode ('Closed 'Dense) t
Rec Int
-> WitBlock (KeyHash 'Witness) era
-> WitBlock BootstrapAddress era
-> WitBlock ScriptHash era
-> WitBlock DataHash era
-> WitUniv era
forall era.
Int
-> WitBlock (KeyHash 'Witness) era
-> WitBlock BootstrapAddress era
-> WitBlock ScriptHash era
-> WitBlock DataHash era
-> WitUniv era
WitUniv Encode
  ('Closed 'Dense)
  (Int
   -> WitBlock (KeyHash 'Witness) era
   -> WitBlock BootstrapAddress era
   -> WitBlock ScriptHash era
   -> WitBlock DataHash era
   -> WitUniv era)
-> Encode ('Closed 'Dense) Int
-> Encode
     ('Closed 'Dense)
     (WitBlock (KeyHash 'Witness) era
      -> WitBlock BootstrapAddress era
      -> WitBlock ScriptHash era
      -> WitBlock DataHash era
      -> WitUniv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Int -> Encode ('Closed 'Dense) Int
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Int
n Encode
  ('Closed 'Dense)
  (WitBlock (KeyHash 'Witness) era
   -> WitBlock BootstrapAddress era
   -> WitBlock ScriptHash era
   -> WitBlock DataHash era
   -> WitUniv era)
-> Encode ('Closed 'Dense) (WitBlock (KeyHash 'Witness) era)
-> Encode
     ('Closed 'Dense)
     (WitBlock BootstrapAddress era
      -> WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> WitBlock (KeyHash 'Witness) era
-> Encode ('Closed 'Dense) (WitBlock (KeyHash 'Witness) era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To WitBlock (KeyHash 'Witness) era
w Encode
  ('Closed 'Dense)
  (WitBlock BootstrapAddress era
   -> WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
-> Encode ('Closed 'Dense) (WitBlock BootstrapAddress era)
-> Encode
     ('Closed 'Dense)
     (WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> WitBlock BootstrapAddress era
-> Encode ('Closed 'Dense) (WitBlock BootstrapAddress era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To WitBlock BootstrapAddress era
x Encode
  ('Closed 'Dense)
  (WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
-> Encode ('Closed 'Dense) (WitBlock ScriptHash era)
-> Encode ('Closed 'Dense) (WitBlock DataHash era -> WitUniv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> WitBlock ScriptHash era
-> Encode ('Closed 'Dense) (WitBlock ScriptHash era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To WitBlock ScriptHash era
y Encode ('Closed 'Dense) (WitBlock DataHash era -> WitUniv era)
-> Encode ('Closed 'Dense) (WitBlock DataHash era)
-> Encode ('Closed 'Dense) (WitUniv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> WitBlock DataHash era
-> Encode ('Closed 'Dense) (WitBlock DataHash era)
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 =
  [String] -> Specification t -> Specification t
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec
    [String
"While witnessing " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with WitUniv of size " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
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 =
  String
-> WitUniv era
-> Specification (KeyHash krole)
-> Specification (KeyHash krole)
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"keyhash :: (KeyHash r c)" WitUniv era
univ (Specification (KeyHash krole) -> Specification (KeyHash krole))
-> Specification (KeyHash krole) -> Specification (KeyHash krole)
forall a b. (a -> b) -> a -> b
$
    (Term (KeyHash krole) -> Pred) -> Specification (KeyHash krole)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (KeyHash krole) -> Pred) -> Specification (KeyHash krole))
-> (Term (KeyHash krole) -> Pred) -> Specification (KeyHash krole)
forall a b. (a -> b) -> a -> b
$
      \ Term (KeyHash krole)
[var|keyhash|] ->
        NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"witnessing " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term (KeyHash krole) -> String
forall a. Show a => a -> String
show Term (KeyHash krole)
keyhash)) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
          Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$
            Term (KeyHash 'Witness)
-> Term (Set (KeyHash 'Witness)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ (Term (KeyHash krole) -> Term (KeyHash 'Witness)
forall a b.
(HasSpec a, HasSpec b, CoercibleLike a b) =>
Term a -> Term b
coerce_ Term (KeyHash krole)
keyhash) (Set (KeyHash 'Witness) -> Term (Set (KeyHash 'Witness))
forall a. HasSpec a => a -> Term a
lit (WitBlock (KeyHash 'Witness) era -> Set (KeyHash 'Witness)
forall t era. WitBlock t era -> Set t
wbHash (WitUniv era -> WitBlock (KeyHash 'Witness) era
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 =
  String
-> WitUniv era
-> Specification ScriptHash
-> Specification ScriptHash
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"scripthash :: ScriptHash" WitUniv era
univ (Specification ScriptHash -> Specification ScriptHash)
-> Specification ScriptHash -> Specification ScriptHash
forall a b. (a -> b) -> a -> b
$
    (Term ScriptHash -> Term Bool) -> Specification ScriptHash
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term ScriptHash -> Term Bool) -> Specification ScriptHash)
-> (Term ScriptHash -> Term Bool) -> Specification ScriptHash
forall a b. (a -> b) -> a -> b
$
      \ Term ScriptHash
[var|scripthash|] -> Term ScriptHash -> Term (Set ScriptHash) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term ScriptHash
scripthash (Set ScriptHash -> Term (Set ScriptHash)
forall a. HasSpec a => a -> Term a
lit (WitBlock ScriptHash era -> Set ScriptHash
forall t era. WitBlock t era -> Set t
wbHash (WitUniv era -> WitBlock ScriptHash era
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 =
  String
-> WitUniv era
-> Specification BootstrapAddress
-> Specification BootstrapAddress
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"bootAddr :: BootstrapAddress" WitUniv era
univ (Specification BootstrapAddress -> Specification BootstrapAddress)
-> Specification BootstrapAddress -> Specification BootstrapAddress
forall a b. (a -> b) -> a -> b
$
    (Term BootstrapAddress -> Term Bool)
-> Specification BootstrapAddress
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term BootstrapAddress -> Term Bool)
 -> Specification BootstrapAddress)
-> (Term BootstrapAddress -> Term Bool)
-> Specification BootstrapAddress
forall a b. (a -> b) -> a -> b
$
      \ Term BootstrapAddress
[var|bootAddr|] -> Term BootstrapAddress -> Term (Set BootstrapAddress) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term BootstrapAddress
bootAddr (Set BootstrapAddress -> Term (Set BootstrapAddress)
forall a. HasSpec a => a -> Term a
lit (WitBlock BootstrapAddress era -> Set BootstrapAddress
forall t era. WitBlock t era -> Set t
wbHash (WitUniv era -> WitBlock BootstrapAddress era
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 =
  String
-> WitUniv era
-> Specification (Credential krole)
-> Specification (Credential krole)
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"cred :: (Credential c)" WitUniv era
univ (Specification (Credential krole)
 -> Specification (Credential krole))
-> Specification (Credential krole)
-> Specification (Credential krole)
forall a b. (a -> b) -> a -> b
$
    (Term (Credential krole) -> [Pred])
-> Specification (Credential krole)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Credential krole) -> [Pred])
 -> Specification (Credential krole))
-> (Term (Credential krole) -> [Pred])
-> Specification (Credential krole)
forall a b. (a -> b) -> a -> b
$ \ Term (Credential krole)
[var|cred|] ->
      [ (Term (Credential krole)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (Credential krole))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Credential krole)
cred)
          -- ScriptHash c -> Credential
          (Int
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args ScriptHash)) Pred
 -> Weighted (BinderD Deps) ScriptHash)
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall a b. (a -> b) -> a -> b
$ \ Term ScriptHash
[var|scripthash|] -> Term ScriptHash -> Specification ScriptHash -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ScriptHash
scripthash (WitUniv era -> Specification ScriptHash
forall era. WitUniv era -> Specification ScriptHash
witScriptHashSpec WitUniv era
univ))
          -- KeyHash kr c -> Credential
          (Int
-> FunTy (MapList Term (Args (KeyHash krole))) Pred
-> Weighted (BinderD Deps) (KeyHash krole)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args (KeyHash krole))) Pred
 -> Weighted (BinderD Deps) (KeyHash krole))
-> FunTy (MapList Term (Args (KeyHash krole))) Pred
-> Weighted (BinderD Deps) (KeyHash krole)
forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash krole)
[var|keyhash|] -> Term (KeyHash krole) -> Specification (KeyHash krole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash krole)
keyhash (WitUniv era -> Specification (KeyHash krole)
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 =
  String -> WitUniv era -> Specification DRep -> Specification DRep
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"drep :: (DRep c)" WitUniv era
univ (Specification DRep -> Specification DRep)
-> Specification DRep -> Specification DRep
forall a b. (a -> b) -> a -> b
$
    (Term DRep -> [Pred]) -> Specification DRep
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term DRep -> [Pred]) -> Specification DRep)
-> (Term DRep -> [Pred]) -> Specification DRep
forall a b. (a -> b) -> a -> b
$ \ Term DRep
[var|drep|] ->
      [ (Term DRep
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep DRep))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term DRep
drep)
          -- KeyHash kr c -> Drep
          (Int
-> FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
 -> Weighted (BinderD Deps) (KeyHash 'DRepRole))
-> FunTy (MapList Term (Args (KeyHash 'DRepRole))) Pred
-> Weighted (BinderD Deps) (KeyHash 'DRepRole)
forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'DRepRole)
[var|keyhash|] -> Term (KeyHash 'DRepRole)
-> Specification (KeyHash 'DRepRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'DRepRole)
keyhash (WitUniv era -> Specification (KeyHash 'DRepRole)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
          -- ScriptHash c -> DRep
          (Int
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args ScriptHash)) Pred
 -> Weighted (BinderD Deps) ScriptHash)
-> FunTy (MapList Term (Args ScriptHash)) Pred
-> Weighted (BinderD Deps) ScriptHash
forall a b. (a -> b) -> a -> b
$ \ Term ScriptHash
[var|scripthash|] -> Term ScriptHash -> Specification ScriptHash -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ScriptHash
scripthash (WitUniv era -> Specification ScriptHash
forall era. WitUniv era -> Specification ScriptHash
witScriptHashSpec WitUniv era
univ))
          -- DRepAlwaysObstain
          (Int
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool -> Pred
forall p. IsPred p => p -> Pred
assert Bool
True)
          -- DRepAlwaysNoConfidence
          (Int
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool -> Pred
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 =
  String
-> WitUniv era
-> Specification RewardAccount
-> Specification RewardAccount
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"rewaccount :: (RewardAccount c)" WitUniv era
univ (Specification RewardAccount -> Specification RewardAccount)
-> Specification RewardAccount -> Specification RewardAccount
forall a b. (a -> b) -> a -> b
$
    (Term RewardAccount -> Pred) -> Specification RewardAccount
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term RewardAccount -> Pred) -> Specification RewardAccount)
-> (Term RewardAccount -> Pred) -> Specification RewardAccount
forall a b. (a -> b) -> a -> b
$ \ Term RewardAccount
[var|rewaccount|] ->
      Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewaccount (FunTy (MapList Term (ProductAsList RewardAccount)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] Term (Credential 'Staking)
[var|raCred|] ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Network
network Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit (Network
Testnet)
        , Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
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 =
  String
-> WitUniv era
-> Specification PoolParams
-> Specification PoolParams
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"poolparams :: (PoolParams c)" WitUniv era
univ (Specification PoolParams -> Specification PoolParams)
-> Specification PoolParams -> Specification PoolParams
forall a b. (a -> b) -> a -> b
$
    (Term PoolParams -> [Pred]) -> Specification PoolParams
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term PoolParams -> [Pred]) -> Specification PoolParams)
-> (Term PoolParams -> [Pred]) -> Specification PoolParams
forall a b. (a -> b) -> a -> b
$ \ Term PoolParams
[var|poolparams|] ->
      [ Term (Set (KeyHash 'Staking))
-> (Term (KeyHash 'Staking) -> Pred) -> Pred
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) ((Term (KeyHash 'Staking) -> Pred) -> Pred)
-> (Term (KeyHash 'Staking) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'Staking)
[var|ownerKeyHash|] -> Term (KeyHash 'Staking) -> Specification (KeyHash 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'Staking)
ownerKeyHash (WitUniv era -> Specification (KeyHash 'Staking)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ)
      , Term (Set (KeyHash 'Staking))
-> Specification (Set (KeyHash 'Staking)) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term PoolParams -> Term (Set (KeyHash 'Staking))
owners_ Term PoolParams
poolparams) (NumSpec Integer -> Specification (Set (KeyHash 'Staking))
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 =
  String
-> WitUniv era
-> Specification GenDelegPair
-> Specification GenDelegPair
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit String
"gdpair :: (GenDelegPair  c)" WitUniv era
univ (Specification GenDelegPair -> Specification GenDelegPair)
-> Specification GenDelegPair -> Specification GenDelegPair
forall a b. (a -> b) -> a -> b
$
    (Term GenDelegPair -> Pred) -> Specification GenDelegPair
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term GenDelegPair -> Pred) -> Specification GenDelegPair)
-> (Term GenDelegPair -> Pred) -> Specification GenDelegPair
forall a b. (a -> b) -> a -> b
$ \ Term GenDelegPair
[var|gdpair|] ->
      Term GenDelegPair
-> FunTy (MapList Term (ProductAsList GenDelegPair)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegPair
gdpair (FunTy (MapList Term (ProductAsList GenDelegPair)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList GenDelegPair)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'GenesisDelegate)
[var|keyhash|] Term (VRFVerKeyHash 'GenDelegVRF)
[var|_hash|] -> Term (KeyHash 'GenesisDelegate)
-> Specification (KeyHash 'GenesisDelegate) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'GenesisDelegate)
keyhash (WitUniv era -> Specification (KeyHash 'GenesisDelegate)
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 =
  String
-> WitUniv era
-> Specification (ShelleyTxCert era)
-> Specification (ShelleyTxCert era)
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit (String
"txcert :: (ShelleyTxCert " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"typeRep (Proxy @era)" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")") WitUniv era
univ (Specification (ShelleyTxCert era)
 -> Specification (ShelleyTxCert era))
-> Specification (ShelleyTxCert era)
-> Specification (ShelleyTxCert era)
forall a b. (a -> b) -> a -> b
$
    (Term (ShelleyTxCert era) -> Pred)
-> Specification (ShelleyTxCert era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ShelleyTxCert era) -> Pred)
 -> Specification (ShelleyTxCert era))
-> (Term (ShelleyTxCert era) -> Pred)
-> Specification (ShelleyTxCert era)
forall a b. (a -> b) -> a -> b
$ \ Term (ShelleyTxCert era)
[var|txcert|] ->
      (Term (ShelleyTxCert era)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (ShelleyTxCert era))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (ShelleyTxCert era)
txcert)
        ( Int
-> FunTy (MapList Term (Args ShelleyDelegCert)) Pred
-> Weighted (BinderD Deps) ShelleyDelegCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
5 (FunTy (MapList Term (Args ShelleyDelegCert)) Pred
 -> Weighted (BinderD Deps) ShelleyDelegCert)
-> FunTy (MapList Term (Args ShelleyDelegCert)) Pred
-> Weighted (BinderD Deps) ShelleyDelegCert
forall a b. (a -> b) -> a -> b
$ \Term ShelleyDelegCert
delegcert ->
            (Term ShelleyDelegCert
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep ShelleyDelegCert)))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term ShelleyDelegCert
delegcert)
              (FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Credential 'Staking))) Pred
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
_register -> Pred
forall deps. PredD deps
TruePred :: Pred)
              (FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Credential 'Staking))) Pred
 -> Weighted (BinderD Deps) (Credential 'Staking))
-> FunTy (MapList Term (Args (Credential 'Staking))) Pred
-> Weighted (BinderD Deps) (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
unregisterAuthor -> Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
unregisterAuthor (WitUniv era -> Specification (Credential 'Staking)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (FunTy
  (MapList
     Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
  Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
   Pred
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (KeyHash 'StakePool))))
     Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (KeyHash 'StakePool))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
delegateAuthor TermD Deps (KeyHash 'StakePool)
_ -> Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
delegateAuthor (WitUniv era -> Specification (Credential 'Staking)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
        )
        ( Int
-> FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args PoolCert)) Pred
 -> Weighted (BinderD Deps) PoolCert)
-> FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall a b. (a -> b) -> a -> b
$ \Term PoolCert
poolcert ->
            (Term PoolCert
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep PoolCert)))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term PoolCert
poolcert)
              (FunTy (MapList Term (Args PoolParams)) Pred
-> Weighted (BinderD Deps) PoolParams
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args PoolParams)) Pred
 -> Weighted (BinderD Deps) PoolParams)
-> FunTy (MapList Term (Args PoolParams)) Pred
-> Weighted (BinderD Deps) PoolParams
forall a b. (a -> b) -> a -> b
$ \Term PoolParams
registerPoolParams -> Term PoolParams -> Specification PoolParams -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolParams
registerPoolParams (WitUniv era -> Specification PoolParams
forall era. WitUniv era -> Specification PoolParams
witPoolParamsSpec WitUniv era
univ))
              (FunTy
  (MapList Term (Args (Prod (KeyHash 'StakePool) EpochNo))) Pred
-> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) EpochNo)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList Term (Args (Prod (KeyHash 'StakePool) EpochNo))) Pred
 -> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) EpochNo))
-> FunTy
     (MapList Term (Args (Prod (KeyHash 'StakePool) EpochNo))) Pred
-> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) EpochNo)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (KeyHash 'StakePool)
retirePoolAuthor TermD Deps EpochNo
_ -> TermD Deps (KeyHash 'StakePool)
-> Specification (KeyHash 'StakePool) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies TermD Deps (KeyHash 'StakePool)
retirePoolAuthor (WitUniv era -> Specification (KeyHash 'StakePool)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
        )
        ( Int
-> FunTy (MapList Term (Args GenesisDelegCert)) Pred
-> Weighted (BinderD Deps) GenesisDelegCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args GenesisDelegCert)) Pred
 -> Weighted (BinderD Deps) GenesisDelegCert)
-> FunTy (MapList Term (Args GenesisDelegCert)) Pred
-> Weighted (BinderD Deps) GenesisDelegCert
forall a b. (a -> b) -> a -> b
$ \Term GenesisDelegCert
genesiscert -> Term GenesisDelegCert
-> FunTy (MapList Term (ProductAsList GenesisDelegCert)) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenesisDelegCert
genesiscert (FunTy (MapList Term (ProductAsList GenesisDelegCert)) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList GenesisDelegCert)) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'Genesis)
authorkey Term (KeyHash 'GenesisDelegate)
_ Term (VRFVerKeyHash 'GenDelegVRF)
_ -> Term (KeyHash 'Genesis) -> Specification (KeyHash 'Genesis) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash 'Genesis)
authorkey (WitUniv era -> Specification (KeyHash 'Genesis)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ)
        )
        (Int
-> FunTy (MapList Term (Args MIRCert)) Pred
-> Weighted (BinderD Deps) MIRCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args MIRCert)) Pred
 -> Weighted (BinderD Deps) MIRCert)
-> FunTy (MapList Term (Args MIRCert)) Pred
-> Weighted (BinderD Deps) MIRCert
forall a b. (a -> b) -> a -> b
$ \TermD Deps MIRCert
_mircert -> NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred (String -> NonEmpty String
forall a. a -> NonEmpty a
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 =
  String
-> WitUniv era
-> Specification (ConwayTxCert era)
-> Specification (ConwayTxCert era)
forall era t.
String -> WitUniv era -> Specification t -> Specification t
explainWit (String
"txcert :: (ConwayTxCert " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"typeRep (Proxy @era)" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")") WitUniv era
univ (Specification (ConwayTxCert era)
 -> Specification (ConwayTxCert era))
-> Specification (ConwayTxCert era)
-> Specification (ConwayTxCert era)
forall a b. (a -> b) -> a -> b
$
    (Term (ConwayTxCert era) -> Pred)
-> Specification (ConwayTxCert era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayTxCert era) -> Pred)
 -> Specification (ConwayTxCert era))
-> (Term (ConwayTxCert era) -> Pred)
-> Specification (ConwayTxCert era)
forall a b. (a -> b) -> a -> b
$ \ Term (ConwayTxCert era)
[var|txcert|] ->
      (Term (ConwayTxCert era)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (ConwayTxCert era))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (ConwayTxCert era)
txcert)
        ( FunTy (MapList Term (Args ConwayDelegCert)) Pred
-> Weighted (BinderD Deps) ConwayDelegCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ConwayDelegCert)) Pred
 -> Weighted (BinderD Deps) ConwayDelegCert)
-> FunTy (MapList Term (Args ConwayDelegCert)) Pred
-> Weighted (BinderD Deps) ConwayDelegCert
forall a b. (a -> b) -> a -> b
$ \Term ConwayDelegCert
delegcert ->
            (Term ConwayDelegCert
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep ConwayDelegCert)))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term ConwayDelegCert
delegcert)
              ( FunTy
  (MapList
     Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
  Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
   Pred
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
registerAuthor Term (StrictMaybe Coin)
deposit ->
                  (Term (StrictMaybe Coin)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (StrictMaybe Coin))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (StrictMaybe Coin)
deposit)
                    (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Pred
forall deps. PredD deps
TruePred :: Pred)
                    (FunTy (MapList Term (Args Coin)) Pred
-> Weighted (BinderD Deps) Coin
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Coin)) Pred
 -> Weighted (BinderD Deps) Coin)
-> FunTy (MapList Term (Args Coin)) Pred
-> Weighted (BinderD Deps) Coin
forall a b. (a -> b) -> a -> b
$ \TermD Deps Coin
_ -> Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
registerAuthor (WitUniv era -> Specification (Credential 'Staking)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              )
              (FunTy
  (MapList
     Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
  Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
   Pred
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (StrictMaybe Coin))))
     Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (StrictMaybe Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
unregisterAuthor Term (StrictMaybe Coin)
_ -> Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
unregisterAuthor (WitUniv era -> Specification (Credential 'Staking)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (FunTy
  (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) Pred
-> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) Pred
 -> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee))
-> FunTy
     (MapList Term (Args (Prod (Credential 'Staking) Delegatee))) Pred
-> Weighted (BinderD Deps) (Prod (Credential 'Staking) Delegatee)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
delegateAuthor TermD Deps Delegatee
_ -> Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
delegateAuthor (WitUniv era -> Specification (Credential 'Staking)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (FunTy
  (MapList
     Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
  Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
   Pred
 -> Weighted
      (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'Staking) (Prod Delegatee Coin))))
     Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'Staking) (Prod Delegatee Coin))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
registerdelegateAuthor TermD Deps Delegatee
_ TermD Deps Coin
_ -> Term (Credential 'Staking)
-> Specification (Credential 'Staking) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'Staking)
registerdelegateAuthor (WitUniv era -> Specification (Credential 'Staking)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
        )
        ( FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args PoolCert)) Pred
 -> Weighted (BinderD Deps) PoolCert)
-> FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall a b. (a -> b) -> a -> b
$ \Term PoolCert
poolcert ->
            (Term PoolCert
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep PoolCert)))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term PoolCert
poolcert)
              (FunTy (MapList Term (Args PoolParams)) Pred
-> Weighted (BinderD Deps) PoolParams
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args PoolParams)) Pred
 -> Weighted (BinderD Deps) PoolParams)
-> FunTy (MapList Term (Args PoolParams)) Pred
-> Weighted (BinderD Deps) PoolParams
forall a b. (a -> b) -> a -> b
$ \Term PoolParams
registerPoolParams -> Term PoolParams -> Specification PoolParams -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolParams
registerPoolParams (WitUniv era -> Specification PoolParams
forall era. WitUniv era -> Specification PoolParams
witPoolParamsSpec WitUniv era
univ))
              (FunTy
  (MapList Term (Args (Prod (KeyHash 'StakePool) EpochNo))) Pred
-> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) EpochNo)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList Term (Args (Prod (KeyHash 'StakePool) EpochNo))) Pred
 -> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) EpochNo))
-> FunTy
     (MapList Term (Args (Prod (KeyHash 'StakePool) EpochNo))) Pred
-> Weighted (BinderD Deps) (Prod (KeyHash 'StakePool) EpochNo)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (KeyHash 'StakePool)
retirePoolAuthor TermD Deps EpochNo
_ -> TermD Deps (KeyHash 'StakePool)
-> Specification (KeyHash 'StakePool) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies TermD Deps (KeyHash 'StakePool)
retirePoolAuthor (WitUniv era -> Specification (KeyHash 'StakePool)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
        )
        ( FunTy (MapList Term (Args ConwayGovCert)) Pred
-> Weighted (BinderD Deps) ConwayGovCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ConwayGovCert)) Pred
 -> Weighted (BinderD Deps) ConwayGovCert)
-> FunTy (MapList Term (Args ConwayGovCert)) Pred
-> Weighted (BinderD Deps) ConwayGovCert
forall a b. (a -> b) -> a -> b
$ \Term ConwayGovCert
govcert ->
            (Term ConwayGovCert
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep ConwayGovCert)))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term ConwayGovCert
govcert)
              (FunTy
  (MapList
     Term
     (Args
        (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'DRepRole) (Prod Coin (StrictMaybe Anchor)))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
regdrepAuthor TermD Deps Coin
_ TermD Deps (StrictMaybe Anchor)
_ -> Term (Credential 'DRepRole)
-> Specification (Credential 'DRepRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
regdrepAuthor (WitUniv era -> Specification (Credential 'DRepRole)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (FunTy (MapList Term (Args (Prod (Credential 'DRepRole) Coin))) Pred
-> Weighted (BinderD Deps) (Prod (Credential 'DRepRole) Coin)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList Term (Args (Prod (Credential 'DRepRole) Coin))) Pred
 -> Weighted (BinderD Deps) (Prod (Credential 'DRepRole) Coin))
-> FunTy
     (MapList Term (Args (Prod (Credential 'DRepRole) Coin))) Pred
-> Weighted (BinderD Deps) (Prod (Credential 'DRepRole) Coin)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
unregdrepAuthor TermD Deps Coin
_ -> Term (Credential 'DRepRole)
-> Specification (Credential 'DRepRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
unregdrepAuthor (WitUniv era -> Specification (Credential 'DRepRole)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (FunTy
  (MapList
     Term (Args (Prod (Credential 'DRepRole) (StrictMaybe Anchor))))
  Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'DRepRole) (StrictMaybe Anchor))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term (Args (Prod (Credential 'DRepRole) (StrictMaybe Anchor))))
   Pred
 -> Weighted
      (BinderD Deps) (Prod (Credential 'DRepRole) (StrictMaybe Anchor)))
-> FunTy
     (MapList
        Term (Args (Prod (Credential 'DRepRole) (StrictMaybe Anchor))))
     Pred
-> Weighted
     (BinderD Deps) (Prod (Credential 'DRepRole) (StrictMaybe Anchor))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
updatedrepAuthor TermD Deps (StrictMaybe Anchor)
_ -> Term (Credential 'DRepRole)
-> Specification (Credential 'DRepRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'DRepRole)
updatedrepAuthor (WitUniv era -> Specification (Credential 'DRepRole)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (FunTy
  (MapList
     Term
     (Args
        (Prod
           (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (Credential 'ColdCommitteeRole) (Credential 'HotCommitteeRole))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'ColdCommitteeRole)
authorizeAuthor TermD Deps (Credential 'HotCommitteeRole)
_ -> Term (Credential 'ColdCommitteeRole)
-> Specification (Credential 'ColdCommitteeRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'ColdCommitteeRole)
authorizeAuthor (WitUniv era -> Specification (Credential 'ColdCommitteeRole)
forall era (krole :: KeyRole).
Typeable krole =>
WitUniv era -> Specification (Credential krole)
witCredSpec WitUniv era
univ))
              (FunTy
  (MapList
     Term
     (Args (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod (Credential 'ColdCommitteeRole) (StrictMaybe Anchor))
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'ColdCommitteeRole)
resignAuthor TermD Deps (StrictMaybe Anchor)
_ -> Term (Credential 'ColdCommitteeRole)
-> Specification (Credential 'ColdCommitteeRole) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential 'ColdCommitteeRole)
resignAuthor (WitUniv era -> Specification (Credential 'ColdCommitteeRole)
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 BootstrapAddress
-> Map BootstrapAddress SigningKey -> Maybe SigningKey
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BootstrapAddress
bootaddr (WitBlock BootstrapAddress era
-> Map BootstrapAddress (ProofType BootstrapAddress era)
forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (WitUniv era -> WitBlock BootstrapAddress era
forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
wu)) of
  Just SigningKey
x ->
    (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era)
      TxWits era -> (TxWits era -> TxWits era) -> TxWits era
forall a b. a -> (a -> b) -> b
& (Set BootstrapWitness -> Identity (Set BootstrapWitness))
-> TxWits era -> Identity (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Set BootstrapWitness)
Lens' (TxWits era) (Set BootstrapWitness)
bootAddrTxWitsL
        ((Set BootstrapWitness -> Identity (Set BootstrapWitness))
 -> TxWits era -> Identity (TxWits era))
-> Set BootstrapWitness -> TxWits era -> TxWits era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (BootstrapWitness -> Set BootstrapWitness
forall a. a -> Set a
Set.singleton (forall hashtype era.
HasWitness hashtype era =>
ProofType hashtype era -> WitnessType hashtype era
mkWitness @(BootstrapAddress) @era SigningKey
ProofType BootstrapAddress era
x SafeHash EraIndependentTxBody
bodyhash))
  Maybe SigningKey
Nothing -> String -> TxWits era
forall a. HasCallStack => String -> a
error (String
"missing BootstrapAddress in WitUnv " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BootstrapAddress -> String
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 KeyHash 'Witness
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> Maybe (KeyPair 'Witness)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Witness
keyhash (WitBlock (KeyHash 'Witness) era
-> Map (KeyHash 'Witness) (ProofType (KeyHash 'Witness) era)
forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (WitUniv era -> WitBlock (KeyHash 'Witness) era
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)
      TxWits era -> (TxWits era -> TxWits era) -> TxWits era
forall a b. a -> (a -> b) -> b
& (Set (WitVKey 'Witness) -> Identity (Set (WitVKey 'Witness)))
-> TxWits era -> Identity (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Set (WitVKey 'Witness))
Lens' (TxWits era) (Set (WitVKey 'Witness))
addrTxWitsL
        ((Set (WitVKey 'Witness) -> Identity (Set (WitVKey 'Witness)))
 -> TxWits era -> Identity (TxWits era))
-> Set (WitVKey 'Witness) -> TxWits era -> TxWits era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (WitVKey 'Witness -> Set (WitVKey 'Witness)
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
ProofType (KeyHash 'Witness) era
x SafeHash EraIndependentTxBody
bodyhash))
  Maybe (KeyPair 'Witness)
Nothing -> String -> TxWits era
forall a. HasCallStack => String -> a
error (String
"missing key hash in WitUnv " String -> ShowS
forall a. [a] -> [a] -> [a]
++ KeyHash 'Witness -> String
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 ScriptHash -> Map ScriptHash (Script era) -> Maybe (Script era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash
scripthash (WitBlock ScriptHash era
-> Map ScriptHash (ProofType ScriptHash era)
forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (WitUniv era -> WitBlock ScriptHash era
forall era. WitUniv era -> WitBlock ScriptHash era
wvScript WitUniv era
wu)) of
  Just Script era
script -> (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era) TxWits era -> (TxWits era -> TxWits era) -> TxWits era
forall a b. a -> (a -> b) -> b
& (Map ScriptHash (Script era)
 -> Identity (Map ScriptHash (Script era)))
-> TxWits era -> Identity (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL ((Map ScriptHash (Script era)
  -> Identity (Map ScriptHash (Script era)))
 -> TxWits era -> Identity (TxWits era))
-> Map ScriptHash (Script era) -> TxWits era -> TxWits era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (ScriptHash
-> Script era
-> Map ScriptHash (Script era)
-> Map ScriptHash (Script era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ScriptHash
scripthash Script era
script Map ScriptHash (Script era)
forall k a. Map k a
Map.empty)
  Maybe (Script era)
Nothing -> String -> TxWits era
forall a. HasCallStack => String -> a
error (String
"missing script hash in WitUnv " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScriptHash -> String
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 DataHash -> Map DataHash (Data era) -> Maybe (Data era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup DataHash
datahash (WitBlock DataHash era -> Map DataHash (ProofType DataHash era)
forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (WitUniv era -> WitBlock DataHash era
forall era. WitUniv era -> WitBlock DataHash era
wvDats WitUniv era
wu)) of
  Just Data era
d -> (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era) TxWits era -> (TxWits era -> TxWits era) -> TxWits era
forall a b. a -> (a -> b) -> b
& (TxDats era -> Identity (TxDats era))
-> TxWits era -> Identity (TxWits era)
forall era. AlonzoEraTxWits era => Lens' (TxWits era) (TxDats era)
Lens' (TxWits era) (TxDats era)
datsTxWitsL ((TxDats era -> Identity (TxDats era))
 -> TxWits era -> Identity (TxWits era))
-> TxDats era -> TxWits era -> TxWits era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map DataHash (Data era) -> TxDats era
forall era. Era era => Map DataHash (Data era) -> TxDats era
TxDats (DataHash
-> Data era -> Map DataHash (Data era) -> Map DataHash (Data era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert DataHash
datahash Data era
d Map DataHash (Data era)
forall k a. Map k a
Map.empty)
  Maybe (Data era)
Nothing -> String -> TxWits era
forall a. HasCallStack => String -> a
error (String
"missing data hash in WitUnv " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DataHash -> String
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 =
  Set t -> Map t (ProofType t era) -> WitBlock t era
forall era t.
(Era era, HasWitness t era) =>
Set t -> Map t (ProofType t era) -> WitBlock t era
WitBlock
    ([t] -> Set t
forall a. Ord a => [a] -> Set a
Set.fromList [t]
hashlist)
    ([(t, ProofType t era)] -> Map t (ProofType t era)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([t] -> [ProofType t era] -> [(t, ProofType t era)]
forall a b. [a] -> [b] -> [(a, b)]
zip [t]
hashlist [ProofType t era]
baselist))
  where
    hashlist :: [t]
hashlist = (ProofType t era -> t) -> [ProofType t era] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map (forall hashtype era.
HasWitness hashtype era =>
TypeHashed hashtype era -> hashtype
hash @t @era (TypeHashed t era -> t)
-> (ProofType t era -> TypeHashed t era) -> ProofType t era -> t
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) = Set t -> Map t (ProofType t era) -> WitBlock t era
forall era t.
(Era era, HasWitness t era) =>
Set t -> Map t (ProofType t era) -> WitBlock t era
WitBlock (Set t
x Set t -> Set t -> Set t
forall a. Semigroup a => a -> a -> a
<> Set t
a) (Map t (ProofType t era)
y Map t (ProofType t era)
-> Map t (ProofType t era) -> Map t (ProofType t era)
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 = (Set t -> Map t (ProofType t era) -> WitBlock t era
forall era t.
(Era era, HasWitness t era) =>
Set t -> Map t (ProofType t era) -> WitBlock t era
WitBlock Set t
forall a. Monoid a => a
mempty Map t (ProofType t era)
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 = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (WitUniv era -> Int
forall era. WitUniv era -> Int
wvSize WitUniv era
x) (WitUniv era -> Int
forall era. WitUniv era -> Int
wvSize WitUniv era
y)
      , wvVKey :: WitBlock (KeyHash 'Witness) era
wvVKey = WitUniv era -> WitBlock (KeyHash 'Witness) era
forall era. WitUniv era -> WitBlock (KeyHash 'Witness) era
wvVKey WitUniv era
x WitBlock (KeyHash 'Witness) era
-> WitBlock (KeyHash 'Witness) era
-> WitBlock (KeyHash 'Witness) era
forall a. Semigroup a => a -> a -> a
<> WitUniv era -> WitBlock (KeyHash 'Witness) era
forall era. WitUniv era -> WitBlock (KeyHash 'Witness) era
wvVKey WitUniv era
y
      , wvBoot :: WitBlock BootstrapAddress era
wvBoot = WitUniv era -> WitBlock BootstrapAddress era
forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
x WitBlock BootstrapAddress era
-> WitBlock BootstrapAddress era -> WitBlock BootstrapAddress era
forall a. Semigroup a => a -> a -> a
<> WitUniv era -> WitBlock BootstrapAddress era
forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
y
      , wvScript :: WitBlock ScriptHash era
wvScript = WitUniv era -> WitBlock ScriptHash era
forall era. WitUniv era -> WitBlock ScriptHash era
wvScript WitUniv era
x WitBlock ScriptHash era
-> WitBlock ScriptHash era -> WitBlock ScriptHash era
forall a. Semigroup a => a -> a -> a
<> WitUniv era -> WitBlock ScriptHash era
forall era. WitUniv era -> WitBlock ScriptHash era
wvScript WitUniv era
y
      , wvDats :: WitBlock DataHash era
wvDats = WitUniv era -> WitBlock DataHash era
forall era. WitUniv era -> WitBlock DataHash era
wvDats WitUniv era
x WitBlock DataHash era
-> WitBlock DataHash era -> WitBlock DataHash era
forall a. Semigroup a => a -> a -> a
<> WitUniv era -> WitBlock DataHash era
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 = WitBlock (KeyHash 'Witness) era
forall a. Monoid a => a
mempty, wvBoot :: WitBlock BootstrapAddress era
wvBoot = WitBlock BootstrapAddress era
forall a. Monoid a => a
mempty, wvScript :: WitBlock ScriptHash era
wvScript = WitBlock ScriptHash era
forall a. Monoid a => a
mempty, wvDats :: WitBlock DataHash era
wvDats = WitBlock DataHash era
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 = [ProofType t era] -> WitBlock t era
forall t era.
(Era era, Ord t, HasWitness t era) =>
[ProofType t era] -> WitBlock t era
blockFromProofList ([ProofType t era] -> WitBlock t era)
-> Gen [ProofType t era] -> Gen (WitBlock t era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (ProofType t era) -> Gen [ProofType t era]
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) = [ProofType t era] -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Map t (ProofType t era) -> [ProofType t era]
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 =
  Int
-> WitBlock (KeyHash 'Witness) era
-> WitBlock BootstrapAddress era
-> WitBlock ScriptHash era
-> WitBlock DataHash era
-> WitUniv era
forall era.
Int
-> WitBlock (KeyHash 'Witness) era
-> WitBlock BootstrapAddress era
-> WitBlock ScriptHash era
-> WitBlock DataHash era
-> WitUniv era
WitUniv Int
n
    (WitBlock (KeyHash 'Witness) era
 -> WitBlock BootstrapAddress era
 -> WitBlock ScriptHash era
 -> WitBlock DataHash era
 -> WitUniv era)
-> Gen (WitBlock (KeyHash 'Witness) era)
-> Gen
     (WitBlock BootstrapAddress era
      -> WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Gen (ProofType (KeyHash 'Witness) era)
-> Gen (WitBlock (KeyHash 'Witness) era)
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))
    Gen
  (WitBlock BootstrapAddress era
   -> WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
-> Gen (WitBlock BootstrapAddress era)
-> Gen
     (WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int
-> Gen (ProofType BootstrapAddress era)
-> Gen (WitBlock BootstrapAddress era)
forall t era.
(Era era, Ord t, HasWitness t era) =>
Int -> Gen (ProofType t era) -> Gen (WitBlock t era)
genWitBlock Int
n ((BootstrapAddress, SigningKey) -> SigningKey
forall a b. (a, b) -> b
snd ((BootstrapAddress, SigningKey) -> SigningKey)
-> Gen (BootstrapAddress, SigningKey) -> Gen SigningKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network -> Gen (BootstrapAddress, SigningKey)
genAddrPair Network
Testnet)
    Gen
  (WitBlock ScriptHash era -> WitBlock DataHash era -> WitUniv era)
-> Gen (WitBlock ScriptHash era)
-> Gen (WitBlock DataHash era -> WitUniv era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int
-> Gen (ProofType ScriptHash era) -> Gen (WitBlock ScriptHash era)
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)
    Gen (WitBlock DataHash era -> WitUniv era)
-> Gen (WitBlock DataHash era) -> Gen (WitUniv era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Gen (ProofType DataHash era) -> Gen (WitBlock DataHash era)
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 = Int -> Gen (WitUniv era)
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 =
      [Gen (NativeScript era)] -> Gen (NativeScript era)
forall a. HasCallStack => [Gen a] -> Gen a
oneof ([Gen (NativeScript era)] -> Gen (NativeScript era))
-> [Gen (NativeScript era)] -> Gen (NativeScript era)
forall a b. (a -> b) -> a -> b
$
        [Gen (NativeScript era)]
nonRecTimelocks [Gen (NativeScript era)]
-> [Gen (NativeScript era)] -> [Gen (NativeScript era)]
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 = [Gen (NativeScript era)] -> Gen (NativeScript era)
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 (KeyHash 'Witness -> NativeScript era)
-> Gen (KeyHash 'Witness) -> Gen (NativeScript 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 <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
4)
      StrictSeq (NativeScript era) -> NativeScript era
forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAllOf (StrictSeq (NativeScript era) -> NativeScript era)
-> ([NativeScript era] -> StrictSeq (NativeScript era))
-> [NativeScript era]
-> NativeScript era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NativeScript era] -> StrictSeq (NativeScript era)
forall a. [a] -> StrictSeq a
Seq.fromList ([NativeScript era] -> NativeScript era)
-> Gen [NativeScript era] -> Gen (NativeScript era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (NativeScript era) -> Gen [NativeScript era]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    requireAnyOf :: Int -> Gen (NativeScript era)
requireAnyOf Int
k = do
      Int
n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
4)
      StrictSeq (NativeScript era) -> NativeScript era
forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAnyOf (StrictSeq (NativeScript era) -> NativeScript era)
-> ([NativeScript era] -> StrictSeq (NativeScript era))
-> [NativeScript era]
-> NativeScript era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NativeScript era] -> StrictSeq (NativeScript era)
forall a. [a] -> StrictSeq a
Seq.fromList ([NativeScript era] -> NativeScript era)
-> Gen [NativeScript era] -> Gen (NativeScript era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (NativeScript era) -> Gen [NativeScript era]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    requireMOf :: Int -> Gen (NativeScript era)
requireMOf Int
k = do
      Int
n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
4)
      Int
m <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
n)
      Int -> StrictSeq (NativeScript era) -> NativeScript era
forall era.
ShelleyEraScript era =>
Int -> StrictSeq (NativeScript era) -> NativeScript era
RequireMOf Int
m (StrictSeq (NativeScript era) -> NativeScript era)
-> ([NativeScript era] -> StrictSeq (NativeScript era))
-> [NativeScript era]
-> NativeScript era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NativeScript era] -> StrictSeq (NativeScript era)
forall a. [a] -> StrictSeq a
Seq.fromList ([NativeScript era] -> NativeScript era)
-> Gen [NativeScript era] -> Gen (NativeScript era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (NativeScript era) -> Gen [NativeScript era]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    genKeyHash :: Gen (KeyHash 'Witness)
    genKeyHash :: Gen (KeyHash 'Witness)
genKeyHash = Gen (KeyHash 'Witness)
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 =
      [Gen (NativeScript era)] -> Gen (NativeScript era)
forall a. HasCallStack => [Gen a] -> Gen a
oneof ([Gen (NativeScript era)] -> Gen (NativeScript era))
-> [Gen (NativeScript era)] -> Gen (NativeScript era)
forall a b. (a -> b) -> a -> b
$
        [Gen (NativeScript era)]
nonRecTimelocks [Gen (NativeScript era)]
-> [Gen (NativeScript era)] -> [Gen (NativeScript era)]
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 = [Gen (NativeScript era)] -> Gen (NativeScript era)
forall a. HasCallStack => [Gen a] -> Gen a
oneof [Gen (NativeScript era)]
nonRecTimelocks
  where
    nonRecTimelocks :: [Gen (NativeScript era)]
nonRecTimelocks =
      [ Gen (NativeScript era)
requireSignature
      , SlotNo -> Gen (NativeScript era)
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 AllegraEraScript era) =>
SlotNo -> Gen (NativeScript era)
requireTimeStart (Word64 -> SlotNo
SlotNo Word64
forall a. Bounded a => a
minBound)
      , SlotNo -> Gen (NativeScript era)
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 AllegraEraScript era) =>
SlotNo -> Gen (NativeScript era)
requireTimeExpire (Word64 -> SlotNo
SlotNo Word64
forall a. Bounded a => a
maxBound)
      ]
    requireSignature :: Gen (NativeScript era)
requireSignature = KeyHash 'Witness -> NativeScript era
forall era.
ShelleyEraScript era =>
KeyHash 'Witness -> NativeScript era
RequireSignature (KeyHash 'Witness -> NativeScript era)
-> Gen (KeyHash 'Witness) -> Gen (NativeScript 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 <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
3) -- lift nonNegativeSingleDigitInt
      StrictSeq (NativeScript era) -> NativeScript era
forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAllOf (StrictSeq (NativeScript era) -> NativeScript era)
-> ([NativeScript era] -> StrictSeq (NativeScript era))
-> [NativeScript era]
-> NativeScript era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NativeScript era] -> StrictSeq (NativeScript era)
forall a. [a] -> StrictSeq a
Seq.fromList ([NativeScript era] -> NativeScript era)
-> Gen [NativeScript era] -> Gen (NativeScript era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (NativeScript era) -> Gen [NativeScript era]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    requireAnyOf :: Int -> Gen (NativeScript era)
requireAnyOf Int
k = do
      Int
n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
3) -- lift positiveSingleDigitInt
      StrictSeq (NativeScript era) -> NativeScript era
forall era.
ShelleyEraScript era =>
StrictSeq (NativeScript era) -> NativeScript era
RequireAnyOf (StrictSeq (NativeScript era) -> NativeScript era)
-> ([NativeScript era] -> StrictSeq (NativeScript era))
-> [NativeScript era]
-> NativeScript era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NativeScript era] -> StrictSeq (NativeScript era)
forall a. [a] -> StrictSeq a
Seq.fromList ([NativeScript era] -> NativeScript era)
-> Gen [NativeScript era] -> Gen (NativeScript era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (NativeScript era) -> Gen [NativeScript era]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    requireMOf :: Int -> Gen (NativeScript era)
requireMOf Int
k = do
      Int
n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
3) -- lift nonNegativeSingleDigitInt
      Int
m <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
n)
      Int -> StrictSeq (NativeScript era) -> NativeScript era
forall era.
ShelleyEraScript era =>
Int -> StrictSeq (NativeScript era) -> NativeScript era
RequireMOf Int
m (StrictSeq (NativeScript era) -> NativeScript era)
-> ([NativeScript era] -> StrictSeq (NativeScript era))
-> [NativeScript era]
-> NativeScript era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NativeScript era] -> StrictSeq (NativeScript era)
forall a. [a] -> StrictSeq a
Seq.fromList ([NativeScript era] -> NativeScript era)
-> Gen [NativeScript era] -> Gen (NativeScript era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (NativeScript era) -> Gen [NativeScript era]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    requireTimeStart :: SlotNo -> Gen (NativeScript era)
requireTimeStart (SlotNo Word64
validFrom) = do
      Word64
minSlotNo <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
forall a. Bounded a => a
minBound, Word64
validFrom)
      NativeScript era -> Gen (NativeScript era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NativeScript era -> Gen (NativeScript era))
-> NativeScript era -> Gen (NativeScript era)
forall a b. (a -> b) -> a -> b
$ SlotNo -> NativeScript era
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 <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
validTill, Word64
forall a. Bounded a => a
maxBound)
      NativeScript era -> Gen (NativeScript era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NativeScript era -> Gen (NativeScript era))
-> NativeScript era -> Gen (NativeScript era)
forall a b. (a -> b) -> a -> b
$ SlotNo -> NativeScript era
forall era. AllegraEraScript era => SlotNo -> NativeScript era
RequireTimeExpire (Word64 -> SlotNo
SlotNo Word64
maxSlotNo)
    genKeyHash :: Gen (KeyHash 'Witness)
    genKeyHash :: Gen (KeyHash 'Witness)
genKeyHash = Gen (KeyHash 'Witness)
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 = Term (KeyHash r) -> Specification (KeyHash r) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (KeyHash r)
t (WitUniv era -> Specification (KeyHash r)
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 = Term ScriptHash -> Specification ScriptHash -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ScriptHash
t (WitUniv era -> Specification ScriptHash
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 = Term (Credential r) -> Specification (Credential r) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Credential r)
t (WitUniv era -> Specification (Credential r)
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 = Term BootstrapAddress -> Specification BootstrapAddress -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term BootstrapAddress
t (WitUniv era -> Specification BootstrapAddress
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 = Term DRep -> Specification DRep -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term DRep
t (WitUniv era -> Specification DRep
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 = Term RewardAccount -> Specification RewardAccount -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term RewardAccount
t (WitUniv era -> Specification RewardAccount
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 = Term PoolParams -> Specification PoolParams -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolParams
t (WitUniv era -> Specification PoolParams
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 = Term GenDelegPair -> Specification GenDelegPair -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term GenDelegPair
t (WitUniv era -> Specification GenDelegPair
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 = Term (ShelleyTxCert era)
-> Specification (ShelleyTxCert era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (ShelleyTxCert era)
t (WitUniv era -> Specification (ShelleyTxCert era)
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 = Term (ConwayTxCert era) -> Specification (ConwayTxCert era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (ConwayTxCert era)
t (WitUniv era -> Specification (ConwayTxCert era)
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 = Term (Committee era) -> Specification (Committee era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Committee era)
t (WitUniv era -> Specification (Committee era)
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 =
    Term (Set t) -> (Term t -> Pred) -> Pred
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 ->
          NonEmpty String -> Pred -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Proxy (Set t) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Set t))) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed")) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
            WitUniv era -> Term t -> Pred
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 =
    (Term (StrictMaybe t)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (StrictMaybe t))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (StrictMaybe t)
t)
      -- SNothing
      (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
      -- SJust
      ( FunTy (MapList Term (Args t)) Pred -> Weighted (BinderD Deps) t
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args t)) Pred -> Weighted (BinderD Deps) t)
-> FunTy (MapList Term (Args t)) Pred -> Weighted (BinderD Deps) t
forall a b. (a -> b) -> a -> b
$ \Term t
x ->
          NonEmpty String -> Pred -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain
            (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Proxy (StrictMaybe t) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(StrictMaybe t))) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed"))
            (WitUniv era -> Term t -> Pred
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 =
    (Term (Maybe t)
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep (Maybe t))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (Maybe t)
t)
      -- Nothing
      (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
      -- Just
      ( FunTy (MapList Term (Args t)) Pred -> Weighted (BinderD Deps) t
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args t)) Pred -> Weighted (BinderD Deps) t)
-> FunTy (MapList Term (Args t)) Pred -> Weighted (BinderD Deps) t
forall a b. (a -> b) -> a -> b
$ \Term t
x ->
          NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain
            (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Proxy (Maybe t) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Maybe t))) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed"))
            (WitUniv era -> Term t -> Pred
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 =
    NonEmpty String -> Pred -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Proxy (Map t v) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Map t v))) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" instance of Witnesssed")) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
      Term (Set t) -> (Term t -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map t v) -> Term (Set t)
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) (WitUniv era -> Term t -> Pred
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 =
    NonEmpty String -> Pred -> Pred
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Proxy [t] -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @([t]))) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" instance of Witnessed")) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
      Term [t] -> (Term t -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [t]
t (WitUniv era -> Term t -> Pred
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 = WitUniv ShelleyEra -> Specification (TxCert ShelleyEra)
WitUniv ShelleyEra -> Specification (ShelleyTxCert ShelleyEra)
forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert

instance EraSpecTxCert AllegraEra where
  witTxCert :: WitUniv AllegraEra -> Specification (TxCert AllegraEra)
witTxCert = WitUniv AllegraEra -> Specification (TxCert AllegraEra)
WitUniv AllegraEra -> Specification (ShelleyTxCert AllegraEra)
forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert

instance EraSpecTxCert MaryEra where
  witTxCert :: WitUniv MaryEra -> Specification (TxCert MaryEra)
witTxCert = WitUniv MaryEra -> Specification (TxCert MaryEra)
WitUniv MaryEra -> Specification (ShelleyTxCert MaryEra)
forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert

instance EraSpecTxCert AlonzoEra where
  witTxCert :: WitUniv AlonzoEra -> Specification (TxCert AlonzoEra)
witTxCert = WitUniv AlonzoEra -> Specification (TxCert AlonzoEra)
WitUniv AlonzoEra -> Specification (ShelleyTxCert AlonzoEra)
forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert

instance EraSpecTxCert BabbageEra where
  witTxCert :: WitUniv BabbageEra -> Specification (TxCert BabbageEra)
witTxCert = WitUniv BabbageEra -> Specification (TxCert BabbageEra)
WitUniv BabbageEra -> Specification (ShelleyTxCert BabbageEra)
forall era.
Era era =>
WitUniv era -> Specification (ShelleyTxCert era)
witShelleyTxCert

instance EraSpecTxCert ConwayEra where
  witTxCert :: WitUniv ConwayEra -> Specification (TxCert ConwayEra)
witTxCert = WitUniv ConwayEra -> Specification (TxCert ConwayEra)
WitUniv ConwayEra -> Specification (ConwayTxCert ConwayEra)
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 = Int -> Gen (NativeScript ShelleyEra)
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 = NativeScript AlonzoEra -> Script AlonzoEra
NativeScript AlonzoEra -> AlonzoScript AlonzoEra
forall era. EraScript era => NativeScript era -> Script era
fromNativeScript (NativeScript AlonzoEra -> AlonzoScript AlonzoEra)
-> Gen (NativeScript AlonzoEra) -> Gen (AlonzoScript AlonzoEra)
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 = NativeScript BabbageEra -> Script BabbageEra
NativeScript BabbageEra -> AlonzoScript BabbageEra
forall era. EraScript era => NativeScript era -> Script era
fromNativeScript (NativeScript BabbageEra -> AlonzoScript BabbageEra)
-> Gen (NativeScript BabbageEra) -> Gen (AlonzoScript BabbageEra)
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 = NativeScript ConwayEra -> Script ConwayEra
NativeScript ConwayEra -> AlonzoScript ConwayEra
forall era. EraScript era => NativeScript era -> Script era
fromNativeScript (NativeScript ConwayEra -> AlonzoScript ConwayEra)
-> Gen (NativeScript ConwayEra) -> Gen (AlonzoScript ConwayEra)
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 =
  (Term (Set ScriptHash) -> [Pred]) -> Specification (Set ScriptHash)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set ScriptHash) -> [Pred])
 -> Specification (Set ScriptHash))
-> (Term (Set ScriptHash) -> [Pred])
-> Specification (Set ScriptHash)
forall a b. (a -> b) -> a -> b
$ \ Term (Set ScriptHash)
[var|setHash|] -> [Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set ScriptHash) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set ScriptHash)
setHash Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
11, WitUniv ShelleyEra -> Term (Set ScriptHash) -> Pred
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 <- Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra))
-> Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra)
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 <- Gen (Set ScriptHash) -> IO (Set ScriptHash)
forall a. Gen a -> IO a
generate (Gen (Set ScriptHash) -> IO (Set ScriptHash))
-> Gen (Set ScriptHash) -> IO (Set ScriptHash)
forall a b. (a -> b) -> a -> b
$ Specification (Set ScriptHash) -> Gen (Set ScriptHash)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ShelleyEra -> Specification (Set ScriptHash)
spec1 WitUniv ShelleyEra
univ)
  String -> IO ()
putStrLn (Doc -> String
forall a. Show a => a -> String
show (Set ScriptHash -> Doc
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 =
  (Term (Set ScriptHash) -> [Pred]) -> Specification (Set ScriptHash)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set ScriptHash) -> [Pred])
 -> Specification (Set ScriptHash))
-> (Term (Set ScriptHash) -> [Pred])
-> Specification (Set ScriptHash)
forall a b. (a -> b) -> a -> b
$ \ Term (Set ScriptHash)
[var|setHash|] ->
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set ScriptHash) -> Term (Set ScriptHash) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Set ScriptHash -> Term (Set ScriptHash)
forall a. HasSpec a => a -> Term a
lit Set ScriptHash
big) Term (Set ScriptHash)
setHash
    , WitUniv ShelleyEra -> Term (Set ScriptHash) -> Pred
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 <- Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra))
-> Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra)
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 <- Gen (Set ScriptHash) -> IO (Set ScriptHash)
forall a. Gen a -> IO a
generate Gen (Set ScriptHash)
forall a. Arbitrary a => Gen a
arbitrary
  Set ScriptHash
ans <- Gen (Set ScriptHash) -> IO (Set ScriptHash)
forall a. Gen a -> IO a
generate (Gen (Set ScriptHash) -> IO (Set ScriptHash))
-> Gen (Set ScriptHash) -> IO (Set ScriptHash)
forall a b. (a -> b) -> a -> b
$ Specification (Set ScriptHash) -> Gen (Set ScriptHash)
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 (Doc -> String
forall a. Show a => a -> String
show (Set ScriptHash -> Doc
forall x. ToExpr x => x -> Doc
prettyE Set ScriptHash
ans))

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

conwayWitUniv :: Int -> WitUniv ConwayEra
conwayWitUniv :: Int -> WitUniv ConwayEra
conwayWitUniv Int
n = IO (WitUniv ConwayEra) -> WitUniv ConwayEra
forall a. IO a -> a
unsafePerformIO (IO (WitUniv ConwayEra) -> WitUniv ConwayEra)
-> IO (WitUniv ConwayEra) -> WitUniv ConwayEra
forall a b. (a -> b) -> a -> b
$ Gen (WitUniv ConwayEra) -> IO (WitUniv ConwayEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv ConwayEra) -> IO (WitUniv ConwayEra))
-> Gen (WitUniv ConwayEra) -> IO (WitUniv ConwayEra)
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 = IO (WitUniv BabbageEra) -> WitUniv BabbageEra
forall a. IO a -> a
unsafePerformIO (IO (WitUniv BabbageEra) -> WitUniv BabbageEra)
-> IO (WitUniv BabbageEra) -> WitUniv BabbageEra
forall a b. (a -> b) -> a -> b
$ Gen (WitUniv BabbageEra) -> IO (WitUniv BabbageEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv BabbageEra) -> IO (WitUniv BabbageEra))
-> Gen (WitUniv BabbageEra) -> IO (WitUniv BabbageEra)
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 = IO (WitUniv AlonzoEra) -> WitUniv AlonzoEra
forall a. IO a -> a
unsafePerformIO (IO (WitUniv AlonzoEra) -> WitUniv AlonzoEra)
-> IO (WitUniv AlonzoEra) -> WitUniv AlonzoEra
forall a b. (a -> b) -> a -> b
$ Gen (WitUniv AlonzoEra) -> IO (WitUniv AlonzoEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv AlonzoEra) -> IO (WitUniv AlonzoEra))
-> Gen (WitUniv AlonzoEra) -> IO (WitUniv AlonzoEra)
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 = IO (WitUniv MaryEra) -> WitUniv MaryEra
forall a. IO a -> a
unsafePerformIO (IO (WitUniv MaryEra) -> WitUniv MaryEra)
-> IO (WitUniv MaryEra) -> WitUniv MaryEra
forall a b. (a -> b) -> a -> b
$ Gen (WitUniv MaryEra) -> IO (WitUniv MaryEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv MaryEra) -> IO (WitUniv MaryEra))
-> Gen (WitUniv MaryEra) -> IO (WitUniv MaryEra)
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 = IO (WitUniv AllegraEra) -> WitUniv AllegraEra
forall a. IO a -> a
unsafePerformIO (IO (WitUniv AllegraEra) -> WitUniv AllegraEra)
-> IO (WitUniv AllegraEra) -> WitUniv AllegraEra
forall a b. (a -> b) -> a -> b
$ Gen (WitUniv AllegraEra) -> IO (WitUniv AllegraEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv AllegraEra) -> IO (WitUniv AllegraEra))
-> Gen (WitUniv AllegraEra) -> IO (WitUniv AllegraEra)
forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @AllegraEra Int
n

shelleyWitUniv :: Int -> WitUniv ShelleyEra
shelleyWitUniv :: Int -> WitUniv ShelleyEra
shelleyWitUniv Int
n = IO (WitUniv ShelleyEra) -> WitUniv ShelleyEra
forall a. IO a -> a
unsafePerformIO (IO (WitUniv ShelleyEra) -> WitUniv ShelleyEra)
-> IO (WitUniv ShelleyEra) -> WitUniv ShelleyEra
forall a b. (a -> b) -> a -> b
$ Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra))
-> Gen (WitUniv ShelleyEra) -> IO (WitUniv ShelleyEra)
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 = [String]
-> SpecificationD Deps (GovActionState era)
-> SpecificationD Deps (GovActionState era)
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"Witnessing GovActionState"] (SpecificationD Deps (GovActionState era)
 -> SpecificationD Deps (GovActionState era))
-> SpecificationD Deps (GovActionState era)
-> SpecificationD Deps (GovActionState era)
forall a b. (a -> b) -> a -> b
$
  (Term (GovActionState era) -> Pred)
-> SpecificationD Deps (GovActionState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (GovActionState era) -> Pred)
 -> SpecificationD Deps (GovActionState era))
-> (Term (GovActionState era) -> Pred)
-> SpecificationD Deps (GovActionState era)
forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState era)
[var|govactstate|] ->
    Term (GovActionState era)
-> FunTy (MapList Term (ProductAsList (GovActionState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (GovActionState era)
govactstate (FunTy (MapList Term (ProductAsList (GovActionState era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (GovActionState era))) [Pred]
-> Pred
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 ->
        [ WitUniv era -> Term (Set (Credential 'HotCommitteeRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'HotCommitteeRole) Vote)
-> Term (Set (Credential 'HotCommitteeRole))
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)
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'HotCommitteeRole)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (Credential 'HotCommitteeRole) Vote)
-> Term (Set (Credential 'HotCommitteeRole))
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) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
3
        , WitUniv era -> Term (Set (Credential 'DRepRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'DRepRole) Vote)
-> Term (Set (Credential 'DRepRole))
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)
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'DRepRole)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (Credential 'DRepRole) Vote)
-> Term (Set (Credential 'DRepRole))
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) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
2
        , WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) Vote)
-> Term (Set (KeyHash 'StakePool))
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)
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (KeyHash 'StakePool)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (KeyHash 'StakePool) Vote)
-> Term (Set (KeyHash 'StakePool))
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) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
2
        , Term (ProposalProcedure era)
-> Specification (ProposalProcedure era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (ProposalProcedure era)
proposalProc (WitUniv era -> Specification (ProposalProcedure era)
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 = [String]
-> SpecificationD Deps (GovAction era)
-> SpecificationD Deps (GovAction era)
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"Witnessing GovAction"] (SpecificationD Deps (GovAction era)
 -> SpecificationD Deps (GovAction era))
-> SpecificationD Deps (GovAction era)
-> SpecificationD Deps (GovAction era)
forall a b. (a -> b) -> a -> b
$
  (Term (GovAction era) -> Pred)
-> SpecificationD Deps (GovAction era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (GovAction era) -> Pred)
 -> SpecificationD Deps (GovAction era))
-> (Term (GovAction era) -> Pred)
-> SpecificationD Deps (GovAction era)
forall a b. (a -> b) -> a -> b
$ \ Term (GovAction era)
[var|govaction|] ->
    (Term (GovAction era)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (GovAction era))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (GovAction era)
govaction)
      -- ParameterChange
      (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
           (Prod (PParamsUpdate era) (StrictMaybe ScriptHash)))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
        (Prod (PParamsUpdate era) (StrictMaybe ScriptHash)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
            (Prod (PParamsUpdate era) (StrictMaybe ScriptHash)))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
         (Prod (PParamsUpdate era) (StrictMaybe ScriptHash))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
              (Prod (PParamsUpdate era) (StrictMaybe ScriptHash)))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
        (Prod (PParamsUpdate era) (StrictMaybe ScriptHash)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
_ TermD Deps (PParamsUpdate era)
_ Term (StrictMaybe ScriptHash)
mhash -> WitUniv era -> Term (StrictMaybe ScriptHash) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (StrictMaybe ScriptHash)
mhash)
      -- HardFork
      (FunTy
  (MapList
     Term
     (Args
        (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer))
-> FunTy
     (MapList
        Term
        (Args
           (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'HardForkPurpose))
_ TermD Deps ProtVer
_ -> Bool
True)
      -- TreasuryWithdrawals
      (FunTy
  (MapList
     Term
     (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
rewacctmap Term (StrictMaybe ScriptHash)
mhash -> [WitUniv era -> Term (Set RewardAccount) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map RewardAccount Coin) -> Term (Set RewardAccount)
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), WitUniv era -> Term (StrictMaybe ScriptHash) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (StrictMaybe ScriptHash)
mhash])
      -- NoConfidence
      (FunTy
  (MapList
     Term (Args (StrictMaybe (GovPurposeId 'CommitteePurpose))))
  Bool
-> Weighted
     (BinderD Deps) (StrictMaybe (GovPurposeId 'CommitteePurpose))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term (Args (StrictMaybe (GovPurposeId 'CommitteePurpose))))
   Bool
 -> Weighted
      (BinderD Deps) (StrictMaybe (GovPurposeId 'CommitteePurpose)))
-> FunTy
     (MapList
        Term (Args (StrictMaybe (GovPurposeId 'CommitteePurpose))))
     Bool
-> Weighted
     (BinderD Deps) (StrictMaybe (GovPurposeId 'CommitteePurpose))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose))
_ -> Bool
True)
      -- UpdateCommitee
      (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'CommitteePurpose))
           (Prod
              (Set (Credential 'ColdCommitteeRole))
              (Prod
                 (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'CommitteePurpose))
            (Prod
               (Set (Credential 'ColdCommitteeRole))
               (Prod
                  (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'CommitteePurpose))
         (Prod
            (Set (Credential 'ColdCommitteeRole))
            (Prod
               (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'CommitteePurpose))
              (Prod
                 (Set (Credential 'ColdCommitteeRole))
                 (Prod
                    (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose))
_ Term (Set (Credential 'ColdCommitteeRole))
credSet Term (Map (Credential 'ColdCommitteeRole) EpochNo)
credMap TermD Deps UnitInterval
_ -> [WitUniv era -> Term (Set (Credential 'ColdCommitteeRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Set (Credential 'ColdCommitteeRole))
credSet, WitUniv era -> Term (Set (Credential 'ColdCommitteeRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'ColdCommitteeRole) EpochNo)
-> Term (Set (Credential 'ColdCommitteeRole))
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
      (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
           (Constitution era))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
        (Constitution era))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
            (Constitution era))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
         (Constitution era)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
              (Constitution era))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
        (Constitution era))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
_ TermD Deps (Constitution era)
_ -> Bool
True)
      -- InfoAction
      (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
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 =
  (Term (ProposalProcedure era) -> Pred)
-> Specification (ProposalProcedure era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ProposalProcedure era) -> Pred)
 -> Specification (ProposalProcedure era))
-> (Term (ProposalProcedure era) -> Pred)
-> Specification (ProposalProcedure era)
forall a b. (a -> b) -> a -> b
$ \ Term (ProposalProcedure era)
[var|proposalProc|] ->
    Term (ProposalProcedure era)
-> FunTy
     (MapList Term (ProductAsList (ProposalProcedure era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposalProcedure era)
proposalProc (FunTy
   (MapList Term (ProductAsList (ProposalProcedure era))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ProposalProcedure era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps Coin
_dep Term RewardAccount
[var|returnAddr|] Term (GovAction era)
[var|govAction|] TermD Deps Anchor
_anchor ->
      [WitUniv era -> Term RewardAccount -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term RewardAccount
returnAddr, Term (GovAction era) -> Specification (GovAction era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (GovAction era)
govAction (WitUniv era -> Specification (GovAction era)
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 =
  (Term (Committee era) -> Pred) -> Specification (Committee era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Committee era) -> Pred) -> Specification (Committee era))
-> (Term (Committee era) -> Pred) -> Specification (Committee era)
forall a b. (a -> b) -> a -> b
$ \ Term (Committee era)
[var|committee|] ->
    Term (Committee era)
-> FunTy (MapList Term (ProductAsList (Committee era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Committee era)
committee (FunTy (MapList Term (ProductAsList (Committee era))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (Committee era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
[var|epochMap|] TermD Deps UnitInterval
_threshold ->
      [WitUniv era -> Term (Set (Credential 'ColdCommitteeRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (Credential 'ColdCommitteeRole) EpochNo)
-> Term (Set (Credential 'ColdCommitteeRole))
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), Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential 'ColdCommitteeRole)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (Credential 'ColdCommitteeRole) EpochNo)
-> Term (Set (Credential 'ColdCommitteeRole))
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) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
3]

go9 :: IO ()
go9 :: IO ()
go9 = do
  WitUniv ConwayEra
univ <- Gen (WitUniv ConwayEra) -> IO (WitUniv ConwayEra)
forall a. Gen a -> IO a
generate (Gen (WitUniv ConwayEra) -> IO (WitUniv ConwayEra))
-> Gen (WitUniv ConwayEra) -> IO (WitUniv ConwayEra)
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 <- Gen (Committee ConwayEra) -> IO (Committee ConwayEra)
forall a. Gen a -> IO a
generate (Gen (Committee ConwayEra) -> IO (Committee ConwayEra))
-> Gen (Committee ConwayEra) -> IO (Committee ConwayEra)
forall a b. (a -> b) -> a -> b
$ Specification (Committee ConwayEra) -> Gen (Committee ConwayEra)
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 (Doc -> String
forall a. Show a => a -> String
show (Committee ConwayEra -> Doc
forall x. ToExpr x => x -> Doc
prettyE Committee ConwayEra
ans))
  String -> IO ()
putStrLn (Doc -> String
forall a. Show a => a -> String
show (WitUniv ConwayEra -> Doc
forall x. ToExpr x => x -> Doc
prettyE WitUniv ConwayEra
univ))