{-# 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 #-}

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

import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.BaseTypes (Network (..))
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Rules (CertsEnv (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)

import Cardano.Ledger.Shelley.TxBody (ShelleyTxBody (..))
import Cardano.Ledger.TxIn (TxIn (..))
import Cardano.Ledger.Val
import Constrained.API
import Constrained.Base (IsPred (..))
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.TreeDiff
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway.Cert (
  delegateeSpec,
  shelleyTxCertSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.Certs (certsEnvSpec, projectEnv)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.QuickCheck hiding (forAll, witness)
import Prelude hiding (seq)

import Cardano.Ledger.Conway.State

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

subMap ::
  (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
  Specification (Map k v, Map k v)
subMap :: forall k v.
(Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
Specification (Map k v, Map k v)
subMap = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (Map k v, Map k v)
[var|pair|] ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Map k v, Map k v)
pair forall a b. (a -> b) -> a -> b
$ \ Term (Map k v)
[var|sub|] Term (Map k v)
[var|super|] ->
    [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
sub Term (Map k v)
super
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall k a. Map k a
Map.empty)
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
sub) (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
super)
    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term v
v Term k
k, forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term k
k Term (Map k v)
super) (\Term v
a -> Term v
v forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term v
a)]
    ]

subMapSubDependsOnSuper ::
  (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
  Term (Map k v) ->
  Term (Map k v) ->
  Pred
subMapSubDependsOnSuper :: forall k v.
(Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
Term (Map k v) -> Term (Map k v) -> Pred
subMapSubDependsOnSuper Term (Map k v)
sub Term (Map k v)
super =
  [Pred] -> Pred
And
    [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
sub Term (Map k v)
super
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall k a. Map k a
Map.empty)
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
sub) (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
super)
    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term v
v Term k
k, forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term k
k Term (Map k v)
super) (\Term v
a -> Term v
v forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term v
a)]
    ]

subMapSuperDependsOnSub ::
  (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
  Term (Map k v) ->
  Term (Map k v) ->
  Pred
subMapSuperDependsOnSub :: forall k v.
(Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
Term (Map k v) -> Term (Map k v) -> Pred
subMapSuperDependsOnSub Term (Map k v)
sub Term (Map k v)
super =
  [Pred] -> Pred
And
    [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
super Term (Map k v)
sub
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall k a. Map k a
Map.empty)
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
sub) (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
super)
    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term k
k Term (Map k v)
super) (\Term v
a -> Term v
v forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term v
a)]
    ]

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

sumCoin_ :: Term [Coin] -> Term Coin
sumCoin_ :: Term [Coin] -> Term Coin
sumCoin_ Term [Coin]
x = forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ forall a. a -> a
id Term [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 a
  , HasSpec b
  , IsPred p
  ) =>
  Term a ->
  (a -> b) ->
  (Term b -> p) ->
  Pred
reifyX :: forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reifyX Term a
t a -> b
f Term b -> p
body =
  forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term 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 b -> b
eval Term a
t)) forall a b. (a -> b) -> a -> b
$ \ Term b
[var|reifyvar|] ->
    -- NOTE we name the existenital variable 'reifyvar'
    [ forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies Term b
reifyvar Term a
t a -> b
f
    , NonEmpty String -> Pred -> Pred
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"reifies " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term b
reifyvar)) forall a b. (a -> b) -> a -> b
$ forall p. IsPred p => p -> Pred
toPred forall a b. (a -> b) -> a -> b
$ Term b -> p
body Term 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_ @era outputs) ==. inputS + with + refund - deposit - f
bodyspec ::
  forall era.
  ( EraSpecTxOut era
  , EraSpecCert era
  , EraSpecTxCert era
  , ConwayEraCertState era
  ) =>
  WitUniv era ->
  CertsEnv era ->
  CertState era ->
  Specification
    ( ShelleyTxBody era
    , Map TxIn (TxOut era)
    , TxIn
    )
bodyspec :: forall era.
(EraSpecTxOut era, EraSpecCert era, EraSpecTxCert era,
 ConwayEraCertState era) =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification (ShelleyTxBody era, Map TxIn (TxOut era), TxIn)
bodyspec WitUniv era
univ CertsEnv era
certsenv CertState era
certstate =
  forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term (ShelleyTxBody era)
[var|shelleyBody|] Term (Map TxIn (TxOut era))
[var|utxo|] Term TxIn
[var|feeInput|] ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ShelleyTxBody era)
shelleyBody forall a b. (a -> b) -> a -> b
$
      \ Term (Set TxIn)
[var|inputs|] Term [TxOut era]
[var|outputs|] Term [TxCert era]
[var|certs|] Term (Map RewardAccount Coin)
[var|withdrawals|] Term Coin
[var|fee|] Term SlotNo
_ Term (Maybe (Update era))
[var|update|] Term (Maybe TxAuxDataHash)
_ ->
        forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term 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 b -> b
eval Term (Map TxIn (TxOut era))
utxo) (forall b. Term b -> b
eval Term (Set TxIn)
inputs)) forall a b. (a -> b) -> a -> b
$ \ Term (Map TxIn (TxOut era))
[var|utxosubset|] ->
          forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term 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 b -> b
eval Term TxIn
feeInput) (forall b. Term b -> b
eval Term (Map TxIn (TxOut era))
utxo)) forall a b. (a -> b) -> a -> b
$ \ Term (Map TxIn (TxOut era))
[var|tempUtxo|] ->
            [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Maybe (Update era))
update forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Maybe a
Nothing
            , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map TxIn (TxOut era))
utxosubset (forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
3 Integer
4))
            , forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map TxIn (TxOut era))
utxosubset forall a b. (a -> b) -> a -> b
$ \Term TxIn
_ Term (TxOut era)
[var|out|] -> forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era Term (TxOut era)
out forall a. OrdLike a => Term a -> Term a -> Term Bool
>. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term TxIn
feeInput Term (Map TxIn (TxOut era))
utxosubset
            , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term TxIn
feeInput (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map TxIn (TxOut era))
utxosubset)
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term Coin
fee Term TxIn
feeInput
            , forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term TxIn
feeInput Term (Map TxIn (TxOut era))
utxosubset) (\ Term (TxOut era)
[var|feeTxout|] -> Term Coin
fee forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era Term (TxOut era)
feeTxout)
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Set TxIn)
inputs Term (Map TxIn (TxOut era))
utxosubset
            , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set TxIn)
inputs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map TxIn (TxOut era))
utxosubset
            , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term TxIn
feeInput Term (Set TxIn)
inputs
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map TxIn (TxOut era))
tempUtxo Term (Map TxIn (TxOut era))
utxosubset
            , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map TxIn (TxOut era))
tempUtxo) (forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize (Integer -> Integer -> NumSpec Integer
rangeSize Integer
8 Integer
10))
            , forall k v.
(Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) =>
Term (Map k v) -> Term (Map k v) -> Pred
subMapSuperDependsOnSub Term (Map TxIn (TxOut era))
utxosubset Term (Map TxIn (TxOut era))
tempUtxo
            , forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map TxIn (TxOut era))
tempUtxo forall a b. (a -> b) -> a -> b
$ \Term TxIn
_ Term (TxOut era)
[var|out|] -> forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era Term (TxOut era)
out forall a. OrdLike a => Term a -> Term a -> Term Bool
>. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
            , -- Certs has no dependencies
              forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [TxCert era]
certs forall a b. (a -> b) -> a -> b
$ \ Term (TxCert era)
[var|oneCert|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (TxCert era)
oneCert (forall era.
EraSpecTxCert era =>
WitUniv era -> Specification (TxCert era)
witTxCert WitUniv era
univ)
            , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [TxCert era]
certs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
4
            , -- withdrawals hs no dependencies
              forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map RewardAccount Coin)
withdrawals forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Integer
2
            , forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map RewardAccount Coin)
withdrawals forall a b. (a -> b) -> a -> b
$ \ Term RewardAccount
[var|acct|] Term Coin
[var|val|] ->
                [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin
val forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
10)
                , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin
val forall a. OrdLike a => Term a -> Term a -> Term Bool
>. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
                , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
acct forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] Term (Credential 'Staking)
_ -> forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Network
network forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Network
Testnet
                ]
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term [TxOut era]
outputs Term [TxCert era]
certs
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term [TxOut era]
outputs Term Coin
fee
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term [TxOut era]
outputs Term (Map RewardAccount Coin)
withdrawals
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term [TxOut era]
outputs Term (Map TxIn (TxOut era))
utxosubset
            , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [TxOut era]
outputs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
4
            , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [TxOut era]
outputs forall a b. (a -> b) -> a -> b
$ \ Term (TxOut era)
[var|oneoutput|] -> forall era. EraSpecTxOut era => Term (TxOut era) -> Term Coin
txOutCoin_ @era Term (TxOut era)
oneoutput forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
            , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reifyX (Term Coin -> Term DeltaCoin
toDelta_ Term Coin
fee) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term DeltaCoin
[var|f|] ->
                forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reifyX (Term Coin -> Term DeltaCoin
toDelta_ (forall era. EraSpecTxOut era => Term [TxOut era] -> Term Coin
sumTxOut_ @era (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map TxIn (TxOut era))
utxosubset))) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term DeltaCoin
[var|inputS|] ->
                  forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reifyX (Term Coin -> Term DeltaCoin
toDelta_ (Term [Coin] -> Term Coin
sumCoin_ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map RewardAccount Coin)
withdrawals))) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term DeltaCoin
[var|with|] ->
                    forall a b p.
(Cases (SimpleRep b) ~ '[SimpleRep b],
 TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b),
 HasSimpleRep b, All HasSpec (Args (SimpleRep b)),
 IsProd (SimpleRep b), HasSpec a, HasSpec b, IsPred p) =>
Term a
-> (a -> b) -> FunTy (MapList Term (Args (SimpleRep b))) p -> Pred
reify' Term [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 DeltaCoin
[var|deposit|] Term DeltaCoin
[var|refund|] ->
                        Term Coin -> Term DeltaCoin
toDelta_ (forall era. EraSpecTxOut era => Term [TxOut era] -> Term Coin
sumTxOut_ @era Term [TxOut era]
outputs) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term DeltaCoin
inputS forall a. Num a => a -> a -> a
+ Term DeltaCoin
with forall a. Num a => a -> a -> a
+ Term DeltaCoin
refund forall a. Num a => a -> a -> a
- Term DeltaCoin
deposit forall a. Num a => a -> a -> a
- Term DeltaCoin
f
            , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map TxIn (TxOut era))
utxo Term (Map TxIn (TxOut era))
tempUtxo
            , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reifyX
                (forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term (Map TxIn (TxOut era))
tempUtxo Term 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 (Map TxIn (TxOut era))
[var|u|] -> Term (Map TxIn (TxOut era))
utxo forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Map TxIn (TxOut era))
u)
            ]

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

putPretty :: ToExpr t => [Char] -> t -> IO ()
putPretty :: forall t. ToExpr 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 x. ToExpr x => x -> Doc
prettyE t
x))

go2 ::
  forall era.
  ( ToExpr (TxOut era)
  , EraSpecTxOut era
  , EraSpecCert era
  , EraSpecTxCert era
  , HasSpec (Tx era)
  , HasSpec (CertState era)
  , ConwayEraCertState era
  ) =>
  IO ()
go2 :: forall era.
(ToExpr (TxOut era), EraSpecTxOut era, EraSpecCert era,
 EraSpecTxCert era, HasSpec (Tx era), HasSpec (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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Specification (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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertState era)
        (forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec @era 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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertsEnv era) forall era.
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
(EraSpecTxOut era, EraSpecCert era, EraSpecTxCert era,
 ConwayEraCertState era) =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification (ShelleyTxBody era, Map TxIn (TxOut era), TxIn)
bodyspec @era 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. ToExpr t => String -> t -> IO ()
putPretty String
"UTxO" UTxO era
utxo
  forall t. ToExpr t => String -> t -> IO ()
putPretty String
"\nfeeInput" TxIn
feeinput
  -- TODO add code to show the inputs, as the TxOuts they UTxO resolves to so that one can inspect
  -- that the TxBody balances. Tghis used to be done with pcTxBodyWithUTxO, which no longer exists.
  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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv AllegraEra
univ Term (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Specification (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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertsEnv AllegraEra) forall era.
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (CertsEnv era)
certsEnvSpec
  ShelleyCertState AllegraEra
certState <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertState AllegraEra)
        (forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec @AllegraEra 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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(TxCert AllegraEra) forall a b. (a -> b) -> a -> b
$
        (forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec @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 era.
Era era =>
WitUniv era -> Specification (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 x. ToExpr x => x -> Doc
prettyE ShelleyTxCert AllegraEra
cert))