{-# 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 (ConwayEra)
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.State (UTxO (..), coinBalance)
import Cardano.Ledger.TxIn (TxIn (..))
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

import Test.Cardano.Ledger.Constrained.Conway.Cert (
  EraSpecCert (..),
  certStateSpec,
  delegateeSpec,
  shelleyTxCertSpec,
 )
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, witness)
import Prelude hiding (seq)

import Cardano.Ledger.Address (Withdrawals (..))
import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.AdaPots (Consumed (..), Produced (..), consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.LedgerState (CertState, PState (..))
import Cardano.Ledger.Shelley.State (ShelleyCertState)
import Cardano.Ledger.State (EraCertState (..), lookupDepositDState)
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,
 )

import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

-- =================================
-- 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 :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Specification fn (Map k v, Map k v)
subMap = forall a (fn :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall k a. Map k a
Map.empty)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ).
(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 :: Univ). [Pred fn] -> Pred fn
Block
    [ forall (fn :: Univ) 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 :: Univ) 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 :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall k a. Map k a
Map.empty)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ).
(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 :: Univ). [Pred fn] -> Pred fn
Block
    [ forall (fn :: Univ) 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 :: Univ) 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 :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall k a. Map k a
Map.empty)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) 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 :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumTxOut_ Term fn [TxOut era]
x = forall (fn :: Univ) a b.
(Foldy fn b, HasSpec fn a) =>
(Term fn a -> Term fn b) -> Term fn [a] -> Term fn b
foldMap_ (forall era (fn :: Univ).
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 :: Univ).
IsConwayUniv fn =>
Term fn [Coin] -> Term fn Coin
sumCoin_ Term fn [Coin]
x = forall (fn :: Univ) a b.
(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, ConwayEraCertState era) =>
  PParams era -> CertState era -> [TxCert era] -> (DeltaCoin, DeltaCoin)
getDepositRefund :: forall era.
(EraTxCert era, ConwayEraCertState era) =>
PParams era
-> CertState era -> [TxCert era] -> (DeltaCoin, DeltaCoin)
getDepositRefund PParams era
pp CertState era
certState [TxCert era]
certs =
  ( Coin -> DeltaCoin
delta forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (KeyHash 'StakePool -> 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) PoolParams
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 -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
getTotalRefundsTxCerts PParams era
pp (forall era. DState era -> Credential 'Staking -> Maybe Coin
lookupDepositDState DState era
ds) (forall era. VState era -> Credential 'DRepRole -> Maybe Coin
lookupDepositVState VState era
vs) [TxCert era]
certs
  )
  where
    delta :: Coin -> DeltaCoin
delta (Coin Integer
n) = Integer -> DeltaCoin
DeltaCoin Integer
n
    vs :: VState era
vs = CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
certVStateL
    ps :: PState era
ps = CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL
    ds :: DState era
ds = CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL

-- | 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 :: Univ) 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 :: Univ).
(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 :: Univ) 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 :: Univ).
(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
  , EraSpecTxCert fn era
  , ConwayEraCertState era
  ) =>
  WitUniv era ->
  CertsEnv era ->
  CertState era ->
  Specification
    fn
    ( ShelleyTxBody era
    , Map TxIn (TxOut era)
    , TxIn
    )
bodyspec :: forall era (fn :: Univ).
(EraSpecTxOut era fn, EraSpecCert era fn, EraSpecTxCert fn era,
 ConwayEraCertState era) =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification fn (ShelleyTxBody era, Map TxIn (TxOut era), TxIn)
bodyspec WitUniv era
univ CertsEnv era
certsenv CertState era
certstate =
  forall a (fn :: Univ) 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 (TxOut era))
[var|utxo|] Term fn TxIn
[var|feeInput|] ->
    forall (fn :: Univ) 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)
[var|inputs|] Term fn [TxOut era]
[var|outputs|] Term fn [TxCert era]
[var|certs|] Term fn (Map RewardAccount Coin)
[var|withdrawals|] Term fn Coin
[var|fee|] Term fn SlotNo
_ Term fn (Maybe (Update era))
[var|update|] Term fn (Maybe TxAuxDataHash)
_ ->
        forall a p (fn :: Univ).
(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 (TxOut era))
utxo) (forall b. Term fn b -> b
eval Term fn (Set TxIn)
inputs)) forall a b. (a -> b) -> a -> b
$ \ Term fn (Map TxIn (TxOut era))
[var|utxosubset|] ->
          forall a p (fn :: Univ).
(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
feeInput) (forall b. Term fn b -> b
eval Term fn (Map TxIn (TxOut era))
utxo)) forall a b. (a -> b) -> a -> b
$ \ Term fn (Map TxIn (TxOut era))
[var|tempUtxo|] ->
            [ forall (fn :: Univ) 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 :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit forall a. Maybe a
Nothing
            , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map TxIn (TxOut era))
utxosubset (forall (fn :: Univ) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
3 Integer
4))
            , forall (fn :: Univ) 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 (TxOut era))
utxosubset forall a b. (a -> b) -> a -> b
$ \Term fn TxIn
_ Term fn (TxOut era)
[var|out|] -> forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
out forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>. forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
            , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn TxIn
feeInput Term fn (Map TxIn (TxOut era))
utxosubset
            , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn TxIn
feeInput (forall (fn :: Univ) 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 (TxOut era))
utxosubset)
            , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
fee Term fn TxIn
feeInput
            , forall (fn :: Univ) 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 :: Univ) 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
feeInput Term fn (Map TxIn (TxOut era))
utxosubset) (\ Term fn (TxOut era)
[var|feeTxout|] -> Term fn Coin
fee forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
feeTxout)
            , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Set TxIn)
inputs Term fn (Map TxIn (TxOut era))
utxosubset
            , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set TxIn)
inputs forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) 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 (TxOut era))
utxosubset
            , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn TxIn
feeInput Term fn (Set TxIn)
inputs
            , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map TxIn (TxOut era))
tempUtxo Term fn (Map TxIn (TxOut era))
utxosubset
            , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: Univ) 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 (TxOut era))
tempUtxo) (forall (fn :: Univ) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
8 Integer
10))
            , forall k v (fn :: Univ).
(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 (TxOut era))
utxosubset Term fn (Map TxIn (TxOut era))
tempUtxo
            , forall (fn :: Univ) 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 (TxOut era))
tempUtxo forall a b. (a -> b) -> a -> b
$ \Term fn TxIn
_ Term fn (TxOut era)
[var|out|] -> forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
out forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>. forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
            , -- Certs has no dependencies
              forall t a (fn :: Univ) 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 :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (TxCert era)
oneCert (forall (fn :: Univ) era.
EraSpecTxCert fn era =>
WitUniv era -> Specification fn (TxCert era)
witTxCert WitUniv era
univ)
            , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxCert era]
certs forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
4
            , -- withdrawals hs no dependencies
              forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn (Map RewardAccount Coin)
withdrawals forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit Integer
2
            , forall (fn :: Univ) 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 Coin)
withdrawals forall a b. (a -> b) -> a -> b
$ \ Term fn RewardAccount
[var|acct|] Term fn Coin
[var|val|] ->
                [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
val forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
10)
                , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Coin
val forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>. forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
                , forall (fn :: Univ) 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
acct forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Staking)
_ -> forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Network
network forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit Network
Testnet
                ]
            , forall (fn :: Univ) 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 :: Univ) 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 :: Univ) 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 Coin)
withdrawals
            , forall (fn :: Univ) 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 (TxOut era))
utxosubset
            , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized fn a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxOut era]
outputs forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
4
            , forall t a (fn :: Univ) 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 :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
oneoutput forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
            , forall (fn :: Univ) 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 :: Univ).
(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 :: Univ) 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 :: Univ).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumTxOut_ @fn @era (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map TxIn (TxOut era))
utxosubset))) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn DeltaCoin
[var|inputS|] ->
                  forall (fn :: Univ) 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 :: Univ).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: Univ).
IsConwayUniv fn =>
Term fn [Coin] -> Term fn Coin
sumCoin_ @fn (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map RewardAccount Coin)
withdrawals))) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term fn DeltaCoin
[var|with|] ->
                    forall (fn :: Univ) 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, ConwayEraCertState 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 :: Univ).
(HasSpec fn Coin, HasSpec fn DeltaCoin, Member (CoinFn fn) fn) =>
Term fn Coin -> Term fn DeltaCoin
toDelta_ (forall (fn :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumTxOut_ @fn @era Term fn [TxOut era]
outputs) forall (fn :: Univ) 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 :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map TxIn (TxOut era))
utxo Term fn (Map TxIn (TxOut era))
tempUtxo
            , forall (fn :: Univ) 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 :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term fn (Map TxIn (TxOut era))
tempUtxo Term fn TxIn
feeInput)
                (\(Map TxIn (TxOut era)
m, TxIn
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
i Map TxIn (TxOut era)
m) -- mimics how we will adjust fee
                (\ Term fn (Map TxIn (TxOut era))
[var|u|] -> Term fn (Map TxIn (TxOut era))
utxo forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (Map TxIn (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
  , EraSpecTxCert ConwayFn era
  , HasSpec ConwayFn (Tx era)
  , HasSpec ConwayFn (CertState era)
  , ConwayEraCertState era
  ) =>
  IO ()
go2 :: forall era.
(EraSpecTxOut era ConwayFn, EraSpecCert era ConwayFn,
 EraSpecTxCert ConwayFn era, HasSpec ConwayFn (Tx era),
 HasSpec ConwayFn (CertState era), ConwayEraCertState era) =>
IO ()
go2 = do
  WitUniv era
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 Int
25
  Map RewardAccount Coin
wdrls <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map RewardAccount Coin)
x -> forall (fn :: Univ) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term ConwayFn (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Specification fn (Set (Credential 'DRepRole))
delegateeSpec WitUniv era
univ)
  CertState era
certState <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertState era)
        (forall era (fn :: Univ).
EraSpecCert era fn =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec @era @ConwayFn WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls) -- (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 :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertsEnv era) forall era (fn :: Univ).
(EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
Specification fn (CertsEnv era)
certsEnvSpec

  (ShelleyTxBody era
body, Map TxIn (TxOut era)
utxomap, TxIn
feeinput) <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (forall era (fn :: Univ).
(EraSpecTxOut era fn, EraSpecCert era fn, EraSpecTxCert fn era,
 ConwayEraCertState era) =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification fn (ShelleyTxBody era, Map TxIn (TxOut era), TxIn)
bodyspec @era @ConwayFn WitUniv era
univ CertsEnv era
certsEnv CertState era
certState)
  let utxo :: UTxO era
utxo = forall era. Map TxIn (TxOut era) -> UTxO era
UTxO Map TxIn (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 (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
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, EraCertState 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, EraCertState 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)

testBody :: IO ()
testBody :: IO ()
testBody = do
  WitUniv AllegraEra
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 @AllegraEra Int
5
  Map RewardAccount Coin
wdrls <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map RewardAccount Coin)
x -> forall (fn :: Univ) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv AllegraEra
univ Term ConwayFn (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Specification fn (Set (Credential 'DRepRole))
delegateeSpec WitUniv AllegraEra
univ)
  CertsEnv AllegraEra
certsEnv <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertsEnv AllegraEra) forall era (fn :: Univ).
(EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
Specification fn (CertsEnv era)
certsEnvSpec
  ShelleyCertState AllegraEra
certState <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertState AllegraEra)
        (forall era (fn :: Univ).
EraSpecCert era fn =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec @AllegraEra @ConwayFn WitUniv AllegraEra
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls)

  ShelleyTxCert AllegraEra
cert <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(TxCert AllegraEra) forall a b. (a -> b) -> a -> b
$
        (forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec @ConwayFn @AllegraEra WitUniv AllegraEra
univ (forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv AllegraEra
certsEnv) ShelleyCertState AllegraEra
certState)
          forall a. Semigroup a => a -> a -> a
<> (forall (fn :: Univ) era.
(Era era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (ShelleyTxCert era)
witShelleyTxCert WitUniv AllegraEra
univ)
  -- The problem with this is that the CertState does not have any
  -- thing from the universe, so any Cert that requires a member_ of someting
  -- in the CertState, will never succeed,  because the Hashes are disjoint
  -- between the CertState and the Universe. So those certs with member_
  -- always fail, so the only ones that are ever generated are RegCert and RegPool
  forall a. Show a => a -> IO ()
print WitUniv AllegraEra
univ
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA ShelleyTxCert AllegraEra
cert))