{-# 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 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 hiding (Value)
import Constrained.Base (Pred (..), addToErrorSpec, hasSize, rangeSize)
import Control.DeepSeq (NFData (..), deepseq)
import Control.Monad (replicateM)
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.Allegra.TreeDiff ()
import Test.Cardano.Ledger.Alonzo.TreeDiff ()
import Test.Cardano.Ledger.Babbage.TreeDiff ()
import Test.Cardano.Ledger.Common (ToExpr (..))
import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic (cSJust_)
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams ()
import Test.Cardano.Ledger.Constrained.Preds.Universes (genAddrPair)
import Test.Cardano.Ledger.Conway.TreeDiff ()
import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..), mkWitnessVKey)
import Test.Cardano.Ledger.Generic.PrettyCore
import Test.Cardano.Ledger.Generic.Proof (Reflect)
import qualified Test.Cardano.Ledger.Generic.Proof as Proof
import Test.QuickCheck hiding (forAll, witness)

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

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

instance (IsConwayUniv fn, Era era) => HasSpec fn (TxDats era)

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

instance
  ( IsConwayUniv fn
  , ShelleyEraScript era
  , NativeScript era ~ MultiSig era
  ) =>
  HasSpec fn (MultiSig era)
  where
  type TypeSpec fn (MultiSig era) = ()
  emptySpec :: TypeSpec fn (MultiSig era)
emptySpec = ()
  combineSpec :: TypeSpec fn (MultiSig era)
-> TypeSpec fn (MultiSig era) -> Specification fn (MultiSig era)
combineSpec TypeSpec fn (MultiSig era)
_ TypeSpec fn (MultiSig era)
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec fn (MultiSig era) -> GenT m (MultiSig era)
genFromTypeSpec TypeSpec fn (MultiSig era)
_ = forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$ forall era. ShelleyEraScript era => Int -> Gen (NativeScript era)
genNestedMultiSig Int
2
  cardinalTypeSpec :: TypeSpec fn (MultiSig era) -> Specification fn Integer
cardinalTypeSpec TypeSpec fn (MultiSig era)
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  shrinkWithTypeSpec :: TypeSpec fn (MultiSig era) -> MultiSig era -> [MultiSig era]
shrinkWithTypeSpec TypeSpec fn (MultiSig era)
_ = forall a. Arbitrary a => a -> [a]
shrink
  conformsTo :: HasCallStack => MultiSig era -> TypeSpec fn (MultiSig era) -> Bool
conformsTo MultiSig era
_ TypeSpec fn (MultiSig era)
_ = Bool
True
  toPreds :: Term fn (MultiSig era) -> TypeSpec fn (MultiSig era) -> Pred fn
toPreds Term fn (MultiSig era)
_ TypeSpec fn (MultiSig era)
_ = forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, PredLike p, UnivConstr p fn) =>
p -> Pred fn
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.

-- deriving instance Typeable r => Generic (KeyHash r c)

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 -> PDoc

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

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

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

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

-- | when we print a WitBlock, we are only interested in the hashes, not the witnesses
instance PrettyA (WitBlock t era) where
  prettyA :: WitBlock t era -> PDoc
prettyA (WitBlock Set t
hashset Map t (ProofType t era)
_) = forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet (forall hashtype era. HasWitness hashtype era => hashtype -> PDoc
prettyHash @t @era) Set t
hashset

instance Show (WitBlock t era) where
  show :: WitBlock t era -> String
show WitBlock t era
x = forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA WitBlock t era
x)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- Non deriveable instances for WitUniv

instance Proof.Reflect era => PrettyA (WitUniv era) where
  prettyA :: WitUniv era -> PDoc
prettyA (WitUniv Int
n WitBlock (KeyHash 'Witness) era
keys WitBlock BootstrapAddress era
boot WitBlock ScriptHash era
script WitBlock DataHash era
dats) =
    Text -> [(Text, PDoc)] -> PDoc
ppRecord
      (Text
"WitnessUniverse " forall a. Semigroup a => a -> a -> a
<> String -> Text
pack (forall a. Show a => a -> String
show Int
n))
      [ (Text
"keys", forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet forall (discriminator :: KeyRole). KeyHash discriminator -> PDoc
pcKeyHash (forall t era. WitBlock t era -> Set t
wbHash WitBlock (KeyHash 'Witness) era
keys))
      , (Text
"boot", forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet BootstrapAddress -> PDoc
pcByronAddress (forall t era. WitBlock t era -> Set t
wbHash WitBlock BootstrapAddress era
boot))
      , (Text
"scripts", forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet ScriptHash -> PDoc
pcScriptHash (forall t era. WitBlock t era -> Set t
wbHash WitBlock ScriptHash era
script))
      , (Text
"dats", forall x ann. (x -> Doc ann) -> Set x -> Doc ann
ppSet forall index. SafeHash index -> PDoc
ppSafeHash (forall t era. WitBlock t era -> Set t
wbHash WitBlock DataHash era
dats))
      ]

instance Proof.Reflect era => Show (WitUniv era) where show :: WitUniv era -> String
show WitUniv era
x = forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA WitUniv era
x)

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Constrains all the Certificate Authors. Sometimes thay are keyHashes, and sometimes Credentials
witConwayTxCert ::
  forall fn era.
  (Era era, IsConwayUniv fn) =>
  WitUniv era -> Specification fn (ConwayTxCert era)
witConwayTxCert :: forall (fn :: [*] -> * -> *) era.
(Era era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (ConwayTxCert era)
witConwayTxCert WitUniv era
univ =
  forall era (fn :: [*] -> * -> *) t.
String -> WitUniv era -> Specification fn t -> Specification fn t
explainWit (String
"txcert :: (ConwayTxCert " forall a. [a] -> [a] -> [a]
++ String
"typeRep (Proxy @era)" forall a. [a] -> [a] -> [a]
++ String
")") WitUniv era
univ forall a b. (a -> b) -> a -> b
$
    forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (ConwayTxCert era)
[var|txcert|] ->
      (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (ConwayTxCert era)
txcert)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ConwayDelegCert
delegcert ->
            (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn ConwayDelegCert
delegcert)
              ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
registerAuthor Term fn (StrictMaybe Coin)
deposit ->
                  (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (StrictMaybe Coin)
deposit)
                    (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> forall (fn :: [*] -> * -> *). Pred fn
TruePred)
                    (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn Coin
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'Staking)
registerAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
              )
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
unregisterAuthor Term fn (StrictMaybe Coin)
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'Staking)
unregisterAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
delegateAuthor Term fn Delegatee
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'Staking)
delegateAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'Staking)
registerdelegateAuthor Term fn Delegatee
_ Term fn Coin
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'Staking)
registerdelegateAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
        )
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn PoolCert
poolcert ->
            (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn PoolCert
poolcert)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn PoolParams
registerPoolParams -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn PoolParams
registerPoolParams (forall (fn :: [*] -> * -> *) era.
IsConwayUniv fn =>
WitUniv era -> Specification fn PoolParams
witPoolParamsSpec WitUniv era
univ))
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (KeyHash 'StakePool)
retirePoolAuthor Term fn EpochNo
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (KeyHash 'StakePool)
retirePoolAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (KeyHash krole)
witKeyHashSpec WitUniv era
univ))
        )
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ConwayGovCert
govcert ->
            (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn ConwayGovCert
govcert)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'DRepRole)
regdrepAuthor Term fn Coin
_ Term fn (StrictMaybe Anchor)
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'DRepRole)
regdrepAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'DRepRole)
unregdrepAuthor Term fn Coin
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'DRepRole)
unregdrepAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'DRepRole)
updatedrepAuthor Term fn (StrictMaybe Anchor)
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'DRepRole)
updatedrepAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'ColdCommitteeRole)
authorizeAuthor Term fn (Credential 'HotCommitteeRole)
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'ColdCommitteeRole)
authorizeAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (Credential krole)
witCredSpec WitUniv era
univ))
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Credential 'ColdCommitteeRole)
resignAuthor Term fn (StrictMaybe Anchor)
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Credential 'ColdCommitteeRole)
resignAuthor (forall (fn :: [*] -> * -> *) era (krole :: KeyRole).
(IsConwayUniv fn, Typeable krole) =>
WitUniv era -> Specification fn (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.
  Proof.Reflect era =>
  BodyHash -> BootstrapAddress -> WitUniv era -> TxWits era
witnessBootAddr :: forall era.
Reflect era =>
SafeHash EraIndependentTxBody
-> BootstrapAddress -> WitUniv era -> TxWits era
witnessBootAddr SafeHash EraIndependentTxBody
bodyhash BootstrapAddress
bootaddr WitUniv era
wu = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BootstrapAddress
bootaddr (forall t era. WitBlock t era -> Map t (ProofType t era)
wbMap (forall era. WitUniv era -> WitBlock BootstrapAddress era
wvBoot WitUniv era
wu)) of
  Just SigningKey
x ->
    (forall era. EraTxWits era => TxWits era
mkBasicTxWits @era)
      forall a b. a -> (a -> b) -> b
& forall era.
EraTxWits era =>
Lens' (TxWits era) (Set BootstrapWitness)
bootAddrTxWitsL
        forall s t a b. ASetter s t a b -> b -> s -> t
.~ (forall a. a -> Set a
Set.singleton (forall hashtype era.
HasWitness hashtype era =>
ProofType hashtype era -> WitnessType hashtype era
mkWitness @(BootstrapAddress) @era SigningKey
x SafeHash EraIndependentTxBody
bodyhash))
  Maybe SigningKey
Nothing -> forall a. HasCallStack => String -> a
error (String
"missing BootstrapAddress in WitUnv " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BootstrapAddress
bootaddr)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- ===============================================================
-- examples
spec1 :: WitUniv ShelleyEra -> Specification ConwayFn (Set ScriptHash)
spec1 :: WitUniv ShelleyEra -> Specification ConwayFn (Set ScriptHash)
spec1 WitUniv ShelleyEra
univ =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term ConwayFn (Set ScriptHash)
[var|setHash|] -> [forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Set ScriptHash)
setHash forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  Integer
11, forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv ShelleyEra
univ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Set ScriptHash)
setHash]

go1 :: IO ()
go1 :: IO ()
go1 = do
  WitUniv ShelleyEra
univ <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ShelleyEra Int
5
  Set ScriptHash
ans <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (WitUniv ShelleyEra -> Specification ConwayFn (Set ScriptHash)
spec1 WitUniv ShelleyEra
univ)
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA Set ScriptHash
ans))

spec2 ::
  WitUniv ShelleyEra ->
  Set ScriptHash ->
  Specification ConwayFn (Set ScriptHash)
spec2 :: WitUniv ShelleyEra
-> Set ScriptHash -> Specification ConwayFn (Set ScriptHash)
spec2 WitUniv ShelleyEra
univ Set ScriptHash
big =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term ConwayFn (Set ScriptHash)
[var|setHash|] ->
    [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn (Set a), Ord a, Show a, Typeable a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set ScriptHash
big) Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Set ScriptHash)
setHash
    , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv ShelleyEra
univ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (Set ScriptHash)
setHash
    ]
go2 :: IO ()
go2 :: IO ()
go2 = do
  WitUniv ShelleyEra
univ <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ShelleyEra Int
5
  Set ScriptHash
big <- forall a. Gen a -> IO a
generate forall a. Arbitrary a => Gen a
arbitrary
  Set ScriptHash
ans <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (WitUniv ShelleyEra
-> Set ScriptHash -> Specification ConwayFn (Set ScriptHash)
spec2 WitUniv ShelleyEra
univ Set ScriptHash
big)
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA Set ScriptHash
ans))

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

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

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

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

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

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

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

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

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

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

-- | Constrains just the parts that need witnessing in GovActionState
govActionStateWitness ::
  forall fn era.
  (IsConwayUniv fn, EraSpecPParams era) =>
  WitUniv era -> Specification fn (GovActionState era)
govActionStateWitness :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecPParams era) =>
WitUniv era -> Specification fn (GovActionState era)
govActionStateWitness WitUniv era
univ = forall (fn :: [*] -> * -> *) a.
[String] -> Specification fn a -> Specification fn a
ExplainSpec [String
"Witnessing GovActionState"] forall a b. (a -> b) -> a -> b
$
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (GovActionState era)
[var|govactstate|] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (GovActionState era)
govactstate forall a b. (a -> b) -> a -> b
$
      \Term fn GovActionId
_gaid Term fn (Map (Credential 'HotCommitteeRole) Vote)
[var|comVotemap|] Term fn (Map (Credential 'DRepRole) Vote)
[var|drepVotemap|] Term fn (Map (KeyHash 'StakePool) Vote)
[var|poolVotemap|] Term fn (ProposalProcedure era)
[var|proposalProc|] Term fn EpochNo
_proposed Term fn EpochNo
_expires ->
        [ forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'HotCommitteeRole) Vote)
comVotemap)
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'HotCommitteeRole) Vote)
comVotemap) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
3
        , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'DRepRole) Vote)
drepVotemap)
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'DRepRole) Vote)
drepVotemap) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
2
        , forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool) Vote)
poolVotemap)
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (KeyHash 'StakePool) Vote)
poolVotemap) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
2
        , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (ProposalProcedure era)
proposalProc (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecPParams era) =>
WitUniv era -> Specification fn (ProposalProcedure era)
proposalProcedureWitness WitUniv era
univ)
        ]

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

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

-- | Constrains just the parts that need witnessing in Committee
committeeWitness ::
  (IsConwayUniv fn, EraSpecPParams era) =>
  WitUniv era -> Specification fn (Committee era)
committeeWitness :: forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecPParams era) =>
WitUniv era -> Specification fn (Committee era)
committeeWitness WitUniv era
univ =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (Committee era)
[var|committee|] ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (Committee era)
committee forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
[var|epochMap|] Term fn UnitInterval
_threshold ->
      [forall (fn :: [*] -> * -> *) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
epochMap), forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
epochMap) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Integer
3]

go9 :: IO ()
go9 :: IO ()
go9 = do
  WitUniv ConwayEra
univ <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
5
  Committee ConwayEra
ans <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecPParams era) =>
WitUniv era -> Specification fn (Committee era)
committeeWitness @ConwayFn @ConwayEra WitUniv ConwayEra
univ)
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA Committee ConwayEra
ans))
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA WitUniv ConwayEra
univ))