{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}

module Test.Cardano.Ledger.Constrained.Preds.TxOut where

import Cardano.Crypto.Hash.Class (Hash, HashAlgorithm, castHash, hashWith)
import Cardano.Ledger.Address (Addr (..))
import Cardano.Ledger.Alonzo.TxOut (AlonzoEraTxOut (..), AlonzoTxOut (..))
import Cardano.Ledger.Babbage.TxOut (BabbageEraTxOut (..), BabbageTxOut (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core (
  Era (EraCrypto),
  EraScript (..),
  EraTxOut (..),
  Script,
  TxOut,
  addrTxOutL,
  coinTxOutL,
  hashScript,
  valueTxOutL,
 )
import Cardano.Ledger.Hashes (DataHash, ScriptHash (..))
import Cardano.Ledger.Mary.Value (
  AssetName (..),
  MaryValue (..),
  MultiAsset (..),
  PolicyID (..),
  multiAssetFromList,
 )
import Cardano.Ledger.Plutus.Data (Data (..), Datum (..), dataToBinaryData, hashData)
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Control.Monad (when)
import Data.Default (Default (def))
import Data.Int (Int64)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..), maybeToStrictMaybe, strictMaybeToMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (IsString (..))
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes
import Test.Cardano.Ledger.Constrained.Combinators (genFromMap, itemFromSet)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.Repl
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Universes hiding (demo, demoTest, main)
import Test.Cardano.Ledger.Constrained.Rewrite (rewriteGen, standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Size
import Test.Cardano.Ledger.Constrained.Solver (toolChain, toolChainSub)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.Fields (TxBodyField (..), TxOutField (..))
import Test.Cardano.Ledger.Generic.PrettyCore (
  pcData,
  pcDataHash,
  pcScript,
  pcScriptHash,
  pcTxOut,
  ppList,
  ppMap,
 )
import Test.Cardano.Ledger.Generic.Proof
import Test.Cardano.Ledger.Generic.Updaters (newTxBody, newTxOut)
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain)

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

scriptFL :: Reflect era => Lens' (Script era) (ScriptF era)
scriptFL :: forall era. Reflect era => Lens' (Script era) (ScriptF era)
scriptFL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (forall era. Proof era -> Script era -> ScriptF era
ScriptF forall era. Reflect era => Proof era
reify) (\Script era
_ (ScriptF Proof era
_ Script era
u) -> Script era
u)

strictMaybeMaybeL :: Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL :: forall a. Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (forall a b. a -> b -> a
const forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe)

txoutRefScriptL :: (Reflect era, BabbageEraTxOut era) => Lens' (TxOutF era) (Maybe (ScriptF era))
txoutRefScriptL :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Lens' (TxOutF era) (Maybe (ScriptF era))
txoutRefScriptL = forall era. Lens' (TxOutF era) (TxOut era)
txOutFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
BabbageEraTxOut era =>
Lens' (TxOut era) (StrictMaybe (Script era))
referenceScriptTxOutL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Lens' a b -> Lens' (Maybe a) (Maybe b)
liftMaybeL forall era. Reflect era => Lens' (Script era) (ScriptF era)
scriptFL

liftMaybeL :: Lens' a b -> Lens' (Maybe a) (Maybe b)
liftMaybeL :: forall a b. Lens' a b -> Lens' (Maybe a) (Maybe b)
liftMaybeL Lens' a b
l = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Maybe a -> Maybe b
getter Maybe a -> Maybe b -> Maybe a
setter
  where
    getter :: Maybe a -> Maybe b
getter (Just a
x) = forall a. a -> Maybe a
Just (a
x forall s a. s -> Getting a s a -> a
^. Lens' a b
l)
    getter Maybe a
Nothing = forall a. Maybe a
Nothing
    setter :: Maybe a -> Maybe b -> Maybe a
setter (Just a
a) (Just b
b) = forall a. a -> Maybe a
Just (a
a forall a b. a -> (a -> b) -> b
& Lens' a b
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ b
b)
    setter (Just a
_a) Maybe b
Nothing = forall a. Maybe a
Nothing -- Type wise this Nothing could be (Just a), but that is wrong
    setter Maybe a
Nothing Maybe b
_ = forall a. Maybe a
Nothing

txoutScriptF :: (Reflect era, BabbageEraTxOut era) => Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF = forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field String
"txoutScript" (forall era a. Rep era a -> Rep era (Maybe a)
MaybeR (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR forall era. Reflect era => Proof era
reify)) (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR forall era. Reflect era => Proof era
reify) forall era.
(Reflect era, BabbageEraTxOut era) =>
Lens' (TxOutF era) (Maybe (ScriptF era))
txoutRefScriptL

txoutScript :: (Reflect era, BabbageEraTxOut era) => Term era (Maybe (ScriptF era))
txoutScript :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Maybe (ScriptF era))
txoutScript = forall era rec field. Field era rec field -> Term era field
fieldToTerm forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF

txoutDatumF :: (Reflect era, BabbageEraTxOut era) => Field era (TxOutF era) (Datum era)
txoutDatumF :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Datum era)
txoutDatumF = forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field String
"txoutDatumF" forall era. Era era => Rep era (Datum era)
DatumR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR forall era. Reflect era => Proof era
reify) (forall era. Lens' (TxOutF era) (TxOut era)
txOutFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. BabbageEraTxOut era => Lens' (TxOut era) (Datum era)
datumTxOutL)

txoutDatum :: (Reflect era, BabbageEraTxOut era) => Term era (Datum era)
txoutDatum :: forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Datum era)
txoutDatum = forall era rec field. Field era rec field -> Term era field
fieldToTerm forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Datum era)
txoutDatumF

txoutDataHashF ::
  (Reflect era, AlonzoEraTxOut era) => Field era (TxOutF era) (Maybe (DataHash (EraCrypto era)))
txoutDataHashF :: forall era.
(Reflect era, AlonzoEraTxOut era) =>
Field era (TxOutF era) (Maybe (DataHash (EraCrypto era)))
txoutDataHashF =
  forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field
    String
"txoutDataHashF"
    (forall era a. Rep era a -> Rep era (Maybe a)
MaybeR forall era. Era era => Rep era (DataHash (EraCrypto era))
DataHashR)
    (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR forall era. Reflect era => Proof era
reify)
    (forall era. Lens' (TxOutF era) (TxOut era)
txOutFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraTxOut era =>
Lens' (TxOut era) (StrictMaybe (DataHash (EraCrypto era)))
dataHashTxOutL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (StrictMaybe a) (Maybe a)
strictMaybeMaybeL)

txoutDataHash :: (Reflect era, AlonzoEraTxOut era) => Term era (Maybe (DataHash (EraCrypto era)))
txoutDataHash :: forall era.
(Reflect era, AlonzoEraTxOut era) =>
Term era (Maybe (DataHash (EraCrypto era)))
txoutDataHash = forall era rec field. Field era rec field -> Term era field
fieldToTerm forall era.
(Reflect era, AlonzoEraTxOut era) =>
Field era (TxOutF era) (Maybe (DataHash (EraCrypto era)))
txoutDataHashF

isBootstrapAddr :: Addr c -> Bool
isBootstrapAddr :: forall c. Addr c -> Bool
isBootstrapAddr (AddrBootstrap BootstrapAddress c
_) = Bool
True
isBootstrapAddr (Addr Network
_ PaymentCredential c
_ StakeReference c
_) = Bool
False

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

txOutPreds ::
  Reflect era => UnivSize -> Proof era -> Term era Coin -> Term era [TxOutF era] -> [Pred era]
txOutPreds :: forall era.
Reflect era =>
UnivSize
-> Proof era
-> Term era Coin
-> Term era [TxOutF era]
-> [Pred era]
txOutPreds size :: UnivSize
size@UnivSize {Int
usDatumFreq :: UnivSize -> Int
usDatumFreq :: Int
usDatumFreq} Proof era
p Term era Coin
balanceCoin Term era [TxOutF era]
outputS =
  [ forall era a.
(Era era, Eq a) =>
Term era Size
-> Term era [a] -> [(Int, Target era a, [Pred era])] -> Pred era
Choose
      (forall era. Era era => Int -> Int -> Term era Size
Range Int
6 Int
6)
      Term era [Datum era]
datums
      [ (Int
1, forall era t. Term era t -> RootTarget era Void t
Simple (forall era t. Rep era t -> t -> Term era t
Lit forall era. Era era => Rep era (Datum era)
DatumR forall era. Datum era
NoDatum), [])
      , (Int
1, forall a t era. String -> (a -> t) -> RootTarget era Void (a -> t)
Constr String
"DatumHash" forall era. DataHash (EraCrypto era) -> Datum era
DatumHash forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (DataHash (EraCrypto era))
hash, [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (DataHash (EraCrypto era))
hash) (forall a era t. Ord a => Term era (Map a t) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataUniv)])
      ,
        ( Int
usDatumFreq
        , forall a t era. String -> (a -> t) -> RootTarget era Void (a -> t)
Constr String
"Datum" (forall era. BinaryData era -> Datum era
Datum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Era era => Data era -> BinaryData era
dataToBinaryData)
            forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Data era)
dat
        , [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left (forall era.
Era era =>
Term era (Data era) -> Term era (DataHash (EraCrypto era))
HashD Term era (Data era)
dat)) (forall a era t. Ord a => Term era (Map a t) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataUniv)]
        )
      ]
  , Term era (Set (Datum era))
datumsSet forall era a t. Term era a -> RootTarget era t a -> Pred era
:<-: forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [Datum era]
datums
  , case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
p of
      TxOutWit era
TxOutShelleyToMary ->
        forall era a t.
(Era era, FromList a t, Eq t) =>
Term era Size -> Term era a -> Pat era t -> [Pred era] -> Pred era
ForEach
          (forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat
              Rep era (TxOutF era)
outR
              [ forall era t a. Field era t a -> Arg era t
Arg forall era.
Reflect era =>
Field era (TxOutF era) (Addr (EraCrypto era))
txoutAddressF
              , forall era t a. Field era t a -> [Pat era a] -> Arg era t
ArgPs forall era. Reflect era => Field era (TxOutF era) (ValueF era)
txoutAmountF [forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t a. Field era t a -> Arg era t
Arg forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t a. Field era t a -> Arg era t
Arg forall era.
Reflect era =>
Field era (ValueF era) (MultiAsset (EraCrypto era))
valueFMultiAssetF]]
              ]
          )
          [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Reflect era => Term era (Addr (EraCrypto era))
txoutAddress) forall era. Era era => Term era (Set (Addr (EraCrypto era)))
addrUniv
          , forall era a. Direct (Term era a) -> [AnyF era a] -> Pred era
Component (forall a b. b -> Either a b
Right forall era. Reflect era => Term era (ValueF era)
txoutAmount) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin, forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. Reflect era => Term era (MultiAsset (EraCrypto era))
valueFMultiAsset]
          , -- , SumsTo (Left (Coin 1)) balanceCoin EQL [One valCoin]
            forall era a.
(Era era, Adds a) =>
a -> Term era a -> OrdCond -> [Sum era a] -> Pred era
SumSplit (Integer -> Coin
Coin Integer
1) Term era Coin
balanceCoin OrdCond
EQL [forall era c. Term era c -> Sum era c
One forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall era a t. Term era a -> RootTarget era t (Gen a) -> Pred era
GenFrom forall era. Reflect era => Term era (MultiAsset (EraCrypto era))
valueFMultiAsset (forall a t era. String -> (a -> t) -> RootTarget era Void (a -> t)
Constr String
"multiAsset" (forall era.
UnivSize
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (MultiAsset (EraCrypto era))
multiAsset UnivSize
size) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
      TxOutWit era
TxOutAlonzoToAlonzo ->
        forall era a t.
(Era era, FromList a t, Eq t) =>
Term era Size -> Term era a -> Pat era t -> [Pred era] -> Pred era
ForEach
          (forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat -- analog to Haskell pattern (TxOut{txoutAddress, txoutAmount{valCoin}, txoutDataHash})
              (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)
              [ forall era t a. Field era t a -> Arg era t
Arg forall era.
Reflect era =>
Field era (TxOutF era) (Addr (EraCrypto era))
txoutAddressF
              , forall era t a. Field era t a -> [Pat era a] -> Arg era t
ArgPs forall era. Reflect era => Field era (TxOutF era) (ValueF era)
txoutAmountF [forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era (ValueF era)
valueR [forall era t a. Field era t a -> Arg era t
Arg forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t a. Field era t a -> Arg era t
Arg forall era.
Reflect era =>
Field era (ValueF era) (MultiAsset (EraCrypto era))
valueFMultiAssetF]]
              , forall era t a. Field era t a -> Arg era t
Arg forall era.
(Reflect era, AlonzoEraTxOut era) =>
Field era (TxOutF era) (Maybe (DataHash (EraCrypto era)))
txoutDataHashF
              ]
          )
          [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Reflect era => Term era (Addr (EraCrypto era))
txoutAddress) forall era. Era era => Term era (Set (Addr (EraCrypto era)))
addrUniv
          , forall era a. Direct (Term era a) -> [AnyF era a] -> Pred era
Component (forall a b. b -> Either a b
Right forall era. Reflect era => Term era (ValueF era)
txoutAmount) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall a era t.
(Era era, Typeable a) =>
Term era (Maybe t) -> RootTarget era a t -> [Pred era] -> Pred era
Maybe forall era.
(Reflect era, AlonzoEraTxOut era) =>
Term era (Maybe (DataHash (EraCrypto era)))
txoutDataHash (forall era t. Term era t -> RootTarget era Void t
Simple Term era (DataHash (EraCrypto era))
hash) [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left Term era (DataHash (EraCrypto era))
hash) (forall a era t. Ord a => Term era (Map a t) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataUniv)]
          , forall era a.
(Era era, Adds a) =>
a -> Term era a -> OrdCond -> [Sum era a] -> Pred era
SumSplit (Integer -> Coin
Coin Integer
2) Term era Coin
balanceCoin OrdCond
EQL [forall era c. Term era c -> Sum era c
One forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall era a t. Term era a -> RootTarget era t (Gen a) -> Pred era
GenFrom forall era. Reflect era => Term era (MultiAsset (EraCrypto era))
valueFMultiAsset (forall a t era. String -> (a -> t) -> RootTarget era Void (a -> t)
Constr String
"multiAsset" (forall era.
UnivSize
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (MultiAsset (EraCrypto era))
multiAsset UnivSize
size) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
      TxOutWit era
TxOutBabbageToConway ->
        forall era a t.
(Era era, FromList a t, Eq t) =>
Term era Size -> Term era a -> Pat era t -> [Pred era] -> Pred era
ForEach
          (forall era. Era era => Int -> Int -> Term era Size
Range Int
3 Int
5)
          Term era [TxOutF era]
outputS
          ( forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat
              (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)
              [ forall era t a. Field era t a -> Arg era t
Arg forall era.
Reflect era =>
Field era (TxOutF era) (Addr (EraCrypto era))
txoutAddressF
              , forall era s t. Rep era s -> Term era t -> [Pat era t] -> Arg era s
argP Rep era (TxOutF era)
outR forall era. Reflect era => Term era (ValueF era)
txoutAmount [forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t a. Field era t a -> Arg era t
Arg forall era.
(HasCallStack, Reflect era) =>
Field era (ValueF era) Coin
valCoinF], forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) [forall era t a. Field era t a -> Arg era t
Arg forall era.
Reflect era =>
Field era (ValueF era) (MultiAsset (EraCrypto era))
valueFMultiAssetF]]
              , forall era t a. Field era t a -> Arg era t
Arg forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Maybe (ScriptF era))
txoutScriptF
              , forall era t a. Field era t a -> Arg era t
Arg forall era.
(Reflect era, BabbageEraTxOut era) =>
Field era (TxOutF era) (Datum era)
txoutDatumF
              ]
          )
          [ forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Reflect era => Term era (Addr (EraCrypto era))
txoutAddress) forall era. Era era => Term era (Set (Addr (EraCrypto era)))
addrUniv
          , forall era a. Direct (Term era a) -> [AnyF era a] -> Pred era
Component (forall a b. b -> Either a b
Right forall era. Reflect era => Term era (ValueF era)
txoutAmount) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field (forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p) forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall a era t.
(Era era, Typeable a) =>
Term era (Maybe t) -> RootTarget era a t -> [Pred era] -> Pred era
Maybe forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Maybe (ScriptF era))
txoutScript (forall era t. Term era t -> RootTarget era Void t
Simple Term era (ScriptF era)
script) [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left (forall era.
Reflect era =>
Term era (ScriptF era) -> Term era (ScriptHash (EraCrypto era))
HashS Term era (ScriptF era)
script)) (forall a era t. Ord a => Term era (Map a t) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
spendscriptUniv Proof era
p))]
          , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era.
(Reflect era, BabbageEraTxOut era) =>
Term era (Datum era)
txoutDatum) Term era (Set (Datum era))
datumsSet
          , forall era a.
(Era era, Adds a) =>
a -> Term era a -> OrdCond -> [Sum era a] -> Pred era
SumSplit (Integer -> Coin
Coin Integer
2) Term era Coin
balanceCoin OrdCond
EQL [forall era c. Term era c -> Sum era c
One forall era. (HasCallStack, Reflect era) => Term era Coin
valCoin]
          , forall era a t. Term era a -> RootTarget era t (Gen a) -> Pred era
GenFrom forall era. Reflect era => Term era (MultiAsset (EraCrypto era))
valueFMultiAsset (forall a t era. String -> (a -> t) -> RootTarget era Void (a -> t)
Constr String
"multiAsset" (forall era.
UnivSize
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Gen (MultiAsset (EraCrypto era))
multiAsset UnivSize
size) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
nonSpendScriptUniv Proof era
p))
          ]
  ]
  where
    outR :: Rep era (TxOutF era)
outR = forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p
    valueR :: Rep era (ValueF era)
valueR = forall era. Era era => Proof era -> Rep era (ValueF era)
ValueR Proof era
p
    script :: Term era (ScriptF era)
script = (forall era t. Era era => String -> Rep era t -> Term era t
var String
"x" (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
p))
    datums :: Term era [Datum era]
datums = forall era t. Era era => String -> Rep era t -> Term era t
var String
"datums" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era (Datum era)
DatumR)
    datumsSet :: Term era (Set (Datum era))
datumsSet = forall era t. Era era => String -> Rep era t -> Term era t
var String
"datumsSet" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (Datum era)
DatumR)
    hash :: Term era (DataHash (EraCrypto era))
hash = forall era t. Era era => String -> Rep era t -> Term era t
var String
"hash" forall era. Era era => Rep era (DataHash (EraCrypto era))
DataHashR
    dat :: Term era (Data era)
dat = forall era t. Era era => String -> Rep era t -> Term era t
var String
"dat" forall era. Era era => Rep era (Data era)
DataR

demo :: ReplMode -> IO ()
demo :: ReplMode -> IO ()
demo ReplMode
mode = do
  let proof :: Proof (ConwayEra StandardCrypto)
proof = Proof (ConwayEra StandardCrypto)
Conway
  Env (ConwayEra StandardCrypto)
env <-
    forall a. Gen a -> IO a
generate
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof (ConwayEra StandardCrypto)
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Era era =>
Proof era -> OrderInfo -> [Pred era] -> Subst era -> Gen (Env era)
toolChain Proof (ConwayEra StandardCrypto)
proof OrderInfo
standardOrderInfo (forall era.
Reflect era =>
UnivSize
-> Proof era
-> Term era Coin
-> Term era [TxOutF era]
-> [Pred era]
txOutPreds forall a. Default a => a
def Proof (ConwayEra StandardCrypto)
proof (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
100)) (forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof (ConwayEra StandardCrypto)
proof))
      )
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (forall era a. Era era => Env era -> Term era a -> IO ()
displayTerm Env (ConwayEra StandardCrypto)
env (forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof (ConwayEra StandardCrypto)
proof))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof (ConwayEra StandardCrypto)
proof Env (ConwayEra StandardCrypto)
env String
""

demoTest :: TestTree
demoTest :: TestTree
demoTest = forall a. String -> IO a -> TestTree
testIO String
"Testing TxOut Stage" (ReplMode -> IO ()
demo ReplMode
CI)

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing TxOut Stage" (ReplMode -> IO ()
demo ReplMode
Interactive)