{-# 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.Coin
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Core
import Cardano.Ledger.Val
import Constrained.API
import Data.Foldable
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.TreeDiff
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec
import Prelude hiding (seq)

-- =================================
-- 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 = (Term (Map k v, Map k v) -> Pred)
-> Specification (Map k v, Map k v)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map k v, Map k v) -> Pred)
 -> Specification (Map k v, Map k v))
-> (Term (Map k v, Map k v) -> Pred)
-> Specification (Map k v, Map k v)
forall a b. (a -> b) -> a -> b
$ \ Term (Map k v, Map k v)
[var|pair|] ->
  Term (Map k v, Map k v)
-> FunTy (MapList Term (ProductAsList (Map k v, Map k v))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Map k v, Map k v)
pair (FunTy (MapList Term (ProductAsList (Map k v, Map k v))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (Map k v, Map k v))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map k v)
[var|sub|] Term (Map k v)
[var|super|] ->
    [ Term (Map k v) -> Term (Map k v) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
sub Term (Map k v)
super
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super Term (Map k v) -> Term (Map k v) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Map k v -> Term (Map k v)
forall a. HasSpec a => a -> Term a
lit (Map k v
forall k a. Map k a
Map.empty)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set k) -> Term (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map k v) -> Term (Set k)
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) (Term (Map k v) -> Term (Set k)
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)
    , Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        Term (k, v)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair (FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [Term v -> Term k -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term v
v Term k
k, Term (Maybe v) -> (Term v -> Term Bool) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term k -> Term (Map k v) -> Term (Maybe v)
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 Term v -> Term v -> Term Bool
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
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
    [ Term (Map k v) -> Term (Map k v) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
sub Term (Map k v)
super
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super Term (Map k v) -> Term (Map k v) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Map k v -> Term (Map k v)
forall a. HasSpec a => a -> Term a
lit (Map k v
forall k a. Map k a
Map.empty)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set k) -> Term (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map k v) -> Term (Set k)
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) (Term (Map k v) -> Term (Set k)
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)
    , Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        Term (k, v)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair (FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [Term v -> Term k -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term v
v Term k
k, Term (Maybe v) -> (Term v -> Term Bool) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term k -> Term (Map k v) -> Term (Maybe v)
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 Term v -> Term v -> Term Bool
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
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
    [ Term (Map k v) -> Term (Map k v) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map k v)
super Term (Map k v)
sub
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map k v)
super Term (Map k v) -> Term (Map k v) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Map k v -> Term (Map k v)
forall a. HasSpec a => a -> Term a
lit (Map k v
forall k a. Map k a
Map.empty)
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set k) -> Term (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map k v) -> Term (Set k)
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) (Term (Map k v) -> Term (Set k)
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)
    , Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
sub ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (k, v)
[var|kvpair|] ->
        Term (k, v)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (k, v)
kvpair (FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (k, v))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k Term v
v -> [Term (Maybe v) -> (Term v -> Term Bool) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term k -> Term (Map k v) -> Term (Maybe v)
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 Term v -> Term v -> Term Bool
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 = (Term (TxOut era) -> Term Coin) -> Term [TxOut era] -> Term Coin
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 = (Term Coin -> Term Coin) -> Term [Coin] -> Term Coin
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term Coin -> Term Coin
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 TxOut era -> (TxOut era -> TxOut era) -> TxOut era
forall a b. a -> (a -> b) -> b
& (Coin -> Identity Coin) -> TxOut era -> Identity (TxOut era)
forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
Lens' (TxOut era) Coin
coinTxOutL ((Coin -> Identity Coin) -> TxOut era -> Identity (TxOut era))
-> Coin -> TxOut era -> TxOut era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ((TxOut era
x TxOut era -> Getting Coin (TxOut era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxOut era) Coin
forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
Lens' (TxOut era) Coin
coinTxOutL) Coin -> Coin -> Coin
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 (Coin -> DeltaCoin) -> Coin -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ PParams era -> (KeyHash 'StakePool -> Bool) -> [TxCert era] -> Coin
forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
forall (f :: * -> *).
Foldable f =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
getTotalDepositsTxCerts PParams era
pp (KeyHash 'StakePool -> Map (KeyHash 'StakePool) PoolParams -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
ps) [TxCert era]
certs
  , Coin -> DeltaCoin
delta (Coin -> DeltaCoin) -> Coin -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> [TxCert era]
-> Coin
forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
forall (f :: * -> *).
Foldable f =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
getTotalRefundsTxCerts PParams era
pp (DState era -> Credential 'Staking -> Maybe Coin
forall era. DState era -> Credential 'Staking -> Maybe Coin
lookupDepositDState DState era
ds) (VState era -> Credential 'DRepRole -> Maybe Coin
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 CertState era
-> Getting (VState era) (CertState era) (VState era) -> VState era
forall s a. s -> Getting a s a -> a
^. Getting (VState era) (CertState era) (VState era)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState era) (VState era)
certVStateL
    ps :: PState era
ps = CertState era
certState CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
    ds :: DState era
ds = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL

-- ==============================================================================
-- 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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (t -> Doc
forall x. ToExpr x => x -> Doc
prettyE t
x))