{-# 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
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))
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
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|] ->
[ 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
]
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)
,
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
,
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)
(\ 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)
]
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)
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
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)
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))