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

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

import Cardano.Ledger.BaseTypes (Network (..))
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Rules (CertsEnv (..))
import Cardano.Ledger.Core

-- import Cardano.Ledger.Shelley.LedgerState (AccountState (..))
import Cardano.Ledger.Shelley.TxBody (ShelleyTxBody (..))
import Cardano.Ledger.TxIn (TxIn (..))
import Cardano.Ledger.UTxO (UTxO (..), coinBalance)
import Cardano.Ledger.Val
import Constrained hiding (Value)
import Constrained.Base
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Word (Word64)

import Data.Sequence.Internal (Seq)
import Lens.Micro

-- , certStateSpec)

import Test.Cardano.Ledger.Constrained.Conway.Cert (
  EraSpecCert (..),
  certStateSpec,
  certStateSpecEx,
 )
import Test.Cardano.Ledger.Constrained.Conway.Certs (certsEnvSpec, projectEnv)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody (fromShelleyBody)
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (EraSpecLedger (..))

import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec
import Test.Cardano.Ledger.Generic.Proof (Reflect)
import qualified Test.Cardano.Ledger.Generic.Proof as Proof
import Test.QuickCheck hiding (forAll)
import Prelude hiding (seq)

import Cardano.Ledger.Address (Withdrawals (..))
import Cardano.Ledger.Allegra (Allegra)
import Cardano.Ledger.Alonzo (Alonzo)
import Cardano.Ledger.Babbage (Babbage)
import Cardano.Ledger.CertState (lookupDepositDState, lookupDepositVState)
import Cardano.Ledger.Mary (Mary)
import Cardano.Ledger.Shelley (Shelley)
import Cardano.Ledger.Shelley.AdaPots (Consumed (..), Produced (..), consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.LedgerState (CertState (..), PState (..))
import Data.Text (pack)
import Lens.Micro
import Prettyprinter (sep, vsep)
import Test.Cardano.Ledger.Generic.Fields (
  TxBodyField (..),
  abstractTxBody,
 )
import Test.Cardano.Ledger.Generic.PrettyCore (
  PDoc,
  PrettyA (..),
  pcTxBodyField,
  pcTxBodyWithUTxO,
  pcTxIn,
  pcTxOut,
  ppList,
  ppMap,
  ppRecord,
  ppString,
 )

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

subMap ::
  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
  Specification fn (Map k v, Map k v)
subMap :: forall k v (fn :: [*] -> * -> *).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Specification fn (Map k v, Map k v)
subMap = 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 (Map k v, Map k v)
[var|pair|] ->
  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 (Map k v, Map k v)
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Map k v)
[var|sub|] Term fn (Map k v)
[var|super|] ->
    [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map k v)
sub Term fn (Map k v)
super
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map k v)
super 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 (forall k a. Map k a
Map.empty)
    , 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 (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 k v)
sub) (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 k v)
super)
    , 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 (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term fn (k, v)
[var|kvpair|] ->
        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 (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term fn k
k Term fn v
v -> [forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn v
v Term fn k
k, forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn k
k Term fn (Map k v)
super) (\Term fn v
a -> Term fn v
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn v
a)]
    ]

subMapSubDependsOnSuper ::
  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
  Term fn (Map k v) ->
  Term fn (Map k v) ->
  Pred fn
subMapSubDependsOnSuper :: forall k v (fn :: [*] -> * -> *).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSubDependsOnSuper Term fn (Map k v)
sub Term fn (Map k v)
super =
  forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
    [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map k v)
sub Term fn (Map k v)
super
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map k v)
super 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 (forall k a. Map k a
Map.empty)
    , 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 (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 k v)
sub) (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 k v)
super)
    , 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 (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term fn (k, v)
[var|kvpair|] ->
        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 (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term fn k
k Term fn v
v -> [forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn v
v Term fn k
k, forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn k
k Term fn (Map k v)
super) (\Term fn v
a -> Term fn v
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn v
a)]
    ]

subMapSuperDependsOnSub ::
  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
  Term fn (Map k v) ->
  Term fn (Map k v) ->
  Pred fn
subMapSuperDependsOnSub :: forall k v (fn :: [*] -> * -> *).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSuperDependsOnSub Term fn (Map k v)
sub Term fn (Map k v)
super =
  forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
    [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map k v)
super Term fn (Map k v)
sub
    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map k v)
super 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 (forall k a. Map k a
Map.empty)
    , 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 (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 k v)
sub) (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 k v)
super)
    , 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 (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term fn (k, v)
[var|kvpair|] ->
        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 (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term fn k
k Term fn v
v -> [forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn k
k Term fn (Map k v)
super) (\Term fn v
a -> Term fn v
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn v
a)]
    ]

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

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

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

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

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

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

-- | This is the first step to generating balanced TxBodies. It illustrates several techniques
--   1) Generate a tuple of related types. Previously we relied on generating one type and then
--      passing the actual generated value as the input of the next generator. This is an alternative to that.
--      But note we still rely partly on the old technique because we take CertsEnv and CertState values as input.
--   2) Carefully using dependsOn, to make explicit the order the code writer thinks the the variables
--      should be solved in. This makes failures less mysterious. Because variable ordering failures
--      are mysterious and hard to solve
--   3) The use of nested reify (here reifyX which just makes error messages better). This supports
--      using complicated Haskell functions to extract one random value, from a previous solved variable
--      using a pure function. Examples of this are 'getDepositRefund' and 'adjustTxOutCoin'
--   4) How complicated balancing constraints can be solved declaratively, rather than algorithmically
--      i.e.  toDelta_ (sumTxOut_ @fn @era outputs) ==. inputS + with + refund - deposit - f
bodyspec ::
  forall era fn.
  ( EraSpecTxOut era fn
  , EraSpecCert era fn
  ) =>
  CertsEnv era ->
  CertState era ->
  Specification
    fn
    ( ShelleyTxBody era
    , Map (TxIn (EraCrypto era)) (TxOut era)
    , TxIn (EraCrypto era)
    )
bodyspec :: forall era (fn :: [*] -> * -> *).
(EraSpecTxOut era fn, EraSpecCert era fn) =>
CertsEnv era
-> CertState era
-> Specification
     fn
     (ShelleyTxBody era, Map (TxIn (EraCrypto era)) (TxOut era),
      TxIn (EraCrypto era))
bodyspec CertsEnv era
certsenv CertState era
certstate =
  forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term fn (ShelleyTxBody era)
[var|shelleyBody|] Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|utxo|] Term fn (TxIn StandardCrypto)
[var|feeInput|] ->
    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 (ShelleyTxBody era)
shelleyBody forall a b. (a -> b) -> a -> b
$
      \ Term fn (Set (TxIn StandardCrypto))
[var|inputs|] Term fn [TxOut era]
[var|outputs|] Term fn [TxCert era]
[var|certs|] Term fn (Map (RewardAccount StandardCrypto) Coin)
[var|withdrawals|] Term fn Coin
[var|fee|] Term fn SlotNo
_ Term fn (Maybe (Update era))
[var|update|] Term fn (Maybe (AuxiliaryDataHash StandardCrypto))
_ ->
        forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys (forall b. Term fn b -> b
eval Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo) (forall b. Term fn b -> b
eval Term fn (Set (TxIn StandardCrypto))
inputs)) forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|utxosubset|] ->
          forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (forall era. EraTxOut era => DeltaCoin -> TxOut era -> TxOut era
adjustTxOutCoin (Integer -> DeltaCoin
DeltaCoin Integer
0)) (forall b. Term fn b -> b
eval Term fn (TxIn StandardCrypto)
feeInput) (forall b. Term fn b -> b
eval Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo)) forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|tempUtxo|] ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Maybe (Update era))
update 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 forall a. Maybe a
Nothing
            , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
3 Integer
4))
            , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset forall a b. (a -> b) -> a -> b
$ \Term fn (TxIn StandardCrypto)
_ Term fn (TxOut era)
[var|out|] -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
out forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (TxIn StandardCrypto)
feeInput Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
            , 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, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (TxIn StandardCrypto)
feeInput (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 (TxIn StandardCrypto) (TxOut era))
utxosubset)
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
fee Term fn (TxIn StandardCrypto)
feeInput
            , forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn (TxIn StandardCrypto)
feeInput Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset) (\ Term fn (TxOut era)
[var|feeTxout|] -> Term fn Coin
fee forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
feeTxout)
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Set (TxIn StandardCrypto))
inputs Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
            , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set (TxIn StandardCrypto))
inputs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. 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 (TxIn StandardCrypto) (TxOut era))
utxosubset
            , 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, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (TxIn StandardCrypto)
feeInput Term fn (Set (TxIn StandardCrypto))
inputs
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
            , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (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 (TxIn StandardCrypto) (TxOut era))
tempUtxo) (forall (fn :: [*] -> * -> *) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: [*] -> * -> *). Integer -> Integer -> SizeSpec fn
rangeSize Integer
8 Integer
10))
            , forall k v (fn :: [*] -> * -> *).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSuperDependsOnSub Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo
            , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo forall a b. (a -> b) -> a -> b
$ \Term fn (TxIn StandardCrypto)
_ Term fn (TxOut era)
[var|out|] -> forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
out forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
            , -- Certs has no dependencies
              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 [TxCert era]
certs forall a b. (a -> b) -> a -> b
$ \ Term fn (TxCert era)
[var|oneCert|] -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (TxCert era)
oneCert (forall era (fn :: [*] -> * -> *).
EraSpecCert era fn =>
CertEnv era -> CertState era -> Specification fn (TxCert era)
txCertSpec (forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv era
certsenv) CertState era
certstate)
            , 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 a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxCert era]
certs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
4
            , -- withdrawals hs no dependencies
              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 a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map (RewardAccount StandardCrypto) Coin)
withdrawals 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 :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Map (RewardAccount StandardCrypto) Coin)
withdrawals forall a b. (a -> b) -> a -> b
$ \ Term fn (RewardAccount StandardCrypto)
[var|acct|] Term fn Coin
[var|val|] ->
                [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
val forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
10)
                , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
val forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
                , 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 StandardCrypto)
acct forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Staking StandardCrypto)
_ -> 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 b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn [TxCert era]
certs
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn Coin
fee
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn (Map (RewardAccount StandardCrypto) Coin)
withdrawals
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
            , 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 a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxOut era]
outputs forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
4
            , 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 [TxOut era]
outputs forall a b. (a -> b) -> a -> b
$ \ Term fn (TxOut era)
[var|oneoutput|] -> forall era (fn :: [*] -> * -> *).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
oneoutput forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
            , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reifyX (forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ Term fn Coin
fee) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn DeltaCoin
[var|f|] ->
                forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reifyX (forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: [*] -> * -> *) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumTxOut_ @fn @era (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset))) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn DeltaCoin
[var|inputS|] ->
                  forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reifyX (forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn [Coin] -> Term fn Coin
sumCoin_ @fn (forall (fn :: [*] -> * -> *) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (RewardAccount StandardCrypto) Coin)
withdrawals))) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn DeltaCoin
[var|with|] ->
                    forall (fn :: [*] -> * -> *) a b p.
(Cases (SimpleRep b) ~ '[SimpleRep b],
 TypeSpec fn b ~ TypeSpec fn (SimpleRep b),
 HasSpec fn (SimpleRep b), HasSimpleRep b,
 All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b),
 HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a
-> (a -> b)
-> FunTy (MapList (Term fn) (Args (SimpleRep b))) p
-> Pred fn
reify' Term fn [TxCert era]
certs (forall era.
EraTxCert era =>
PParams era
-> CertState era -> [TxCert era] -> (DeltaCoin, DeltaCoin)
getDepositRefund @era (forall era. CertsEnv era -> PParams era
certsPParams CertsEnv era
certsenv) CertState era
certstate) forall a b. (a -> b) -> a -> b
$
                      \ Term fn DeltaCoin
[var|deposit|] Term fn DeltaCoin
[var|refund|] ->
                        forall (fn :: [*] -> * -> *).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: [*] -> * -> *) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumTxOut_ @fn @era Term fn [TxOut era]
outputs) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn DeltaCoin
inputS forall a. Num a => a -> a -> a
+ Term fn DeltaCoin
with forall a. Num a => a -> a -> a
+ Term fn DeltaCoin
refund forall a. Num a => a -> a -> a
- Term fn DeltaCoin
deposit forall a. Num a => a -> a -> a
- Term fn DeltaCoin
f
            , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo
            , forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reifyX
                (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo Term fn (TxIn StandardCrypto)
feeInput)
                (\(Map (TxIn StandardCrypto) (TxOut era)
m, TxIn StandardCrypto
i) -> forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (forall era. EraTxOut era => DeltaCoin -> TxOut era -> TxOut era
adjustTxOutCoin (Integer -> DeltaCoin
DeltaCoin Integer
0)) TxIn StandardCrypto
i Map (TxIn StandardCrypto) (TxOut era)
m) -- mimics how we will adjust fee
                (\ Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|u|] -> Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (Map (TxIn StandardCrypto) (TxOut era))
u)
            ]

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

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

go2 ::
  forall era.
  ( EraSpecTxOut era ConwayFn
  , EraSpecCert era ConwayFn
  , HasSpec ConwayFn (Tx era)
  ) =>
  IO ()
go2 :: forall era.
(EraSpecTxOut era ConwayFn, EraSpecCert era ConwayFn,
 HasSpec ConwayFn (Tx era)) =>
IO ()
go2 = do
  CertState era
certState <-
    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 @ConwayFn @(CertState era)
        (forall (fn :: [*] -> * -> *) era.
(IsConwayUniv fn, EraSpecDeleg era) =>
Specification fn (CertState era)
certStateSpecEx @ConwayFn @era) -- (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100)))
        -- error "STOP"
  CertsEnv era
certsEnv <- 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 @ConwayFn @(CertsEnv era) forall era (fn :: [*] -> * -> *).
(EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
Specification fn (CertsEnv era)
certsEnvSpec

  (ShelleyTxBody era
body, Map (TxIn StandardCrypto) (TxOut era)
utxomap, TxIn StandardCrypto
feeinput) <-
    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 era (fn :: [*] -> * -> *).
(EraSpecTxOut era fn, EraSpecCert era fn) =>
CertsEnv era
-> CertState era
-> Specification
     fn
     (ShelleyTxBody era, Map (TxIn (EraCrypto era)) (TxOut era),
      TxIn (EraCrypto era))
bodyspec @era @ConwayFn CertsEnv era
certsEnv CertState era
certState)
  let utxo :: UTxO era
utxo = forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn StandardCrypto) (TxOut era)
utxomap
      txbody :: TxBody era
txbody = forall era. EraTxBody era => ShelleyTxBody era -> TxBody era
fromShelleyBody ShelleyTxBody era
body

  String -> IO ()
putStrLn
    (String
"Input UTxO, total " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era. EraTxOut era => UTxO era -> Coin
coinBalance @era UTxO era
utxo) forall a. [a] -> [a] -> [a]
++ String
", size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Int
Map.size Map (TxIn StandardCrypto) (TxOut era)
utxomap))
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"UTxO" UTxO era
utxo
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"\nfeeInput" TxIn StandardCrypto
feeinput
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall era. Reflect era => UTxO era -> TxBody era -> PDoc
pcTxBodyWithUTxO UTxO era
utxo TxBody era
txbody))
  forall a. Show a => a -> IO ()
print (forall era.
EraTxBody era =>
TxBody era -> PParams era -> CertState era -> UTxO era -> Consumed
consumedTxBody TxBody era
txbody (forall era. CertsEnv era -> PParams era
certsPParams CertsEnv era
certsEnv) CertState era
certState UTxO era
utxo)
  forall a. Show a => a -> IO ()
print (forall era.
EraTxBody era =>
TxBody era -> PParams era -> CertState era -> Produced
producedTxBody TxBody era
txbody (forall era. CertsEnv era -> PParams era
certsPParams CertsEnv era
certsEnv) CertState era
certState)