{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Constrained.Preds.UTxO where

import Control.Monad (when)
import Data.Default (Default (def))
import qualified Data.Map.Strict as Map
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Universes (UnivSize (..), universeStage)
import Test.Cardano.Ledger.Constrained.Rewrite (standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Size (Size (..))
import Test.Cardano.Ledger.Constrained.Solver (toolChainSub)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.PrettyCore (pcUTxO)
import Test.Cardano.Ledger.Generic.Proof
import Test.QuickCheck

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

utxoPreds :: forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
utxoPreds :: forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
utxoPreds UnivSize
usize Proof era
p =
  [ Size -> Term era Size -> Pred era
forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Size
SzExact (UnivSize -> Int
usNumPreUtxo UnivSize
usize)) Term era Size
utxoSize -- must be bigger than sum of (maxsize inputs 10) and (maxsize collateral 3)
  , Term era Size -> Term era (Map TxIn (TxOutF era)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
utxoSize Term era (Map TxIn (TxOutF era))
preUtxo
  , Term era Size -> Term era (Map TxIn (TxOutF era)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
6) Term era (Map TxIn (TxOutF era))
colUtxo
  , Term era TxIn
-> Term era (TxOutF era)
-> Direct (Term era (Map TxIn (TxOutF era)))
-> Pred era
forall k v era.
(Ord k, Eq v, Ord v) =>
Term era k -> Term era v -> Direct (Term era (Map k v)) -> Pred era
MapMember Term era TxIn
forall era. Era era => Term era TxIn
feeTxIn Term era (TxOutF era)
forall era. Reflect era => Term era (TxOutF era)
feeTxOut (Term era (Map TxIn (TxOutF era))
-> Direct (Term era (Map TxIn (TxOutF era)))
forall a b. b -> Either a b
Right Term era (Map TxIn (TxOutF era))
preUtxo)
  , Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
preUtxo) Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
txinUniv
  , Term era (Set (TxOutF era))
-> Term era (Set (TxOutF era)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map TxIn (TxOutF era)) -> Term era (Set (TxOutF era))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map TxIn (TxOutF era))
preUtxo) (Proof era -> Term era (Set (TxOutF era))
forall era. Era era => Proof era -> Term era (Set (TxOutF era))
txoutUniv Proof era
p)
  , Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p Term era (Map TxIn (TxOutF era))
-> RootTarget era Void (Map TxIn (TxOutF era)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (String
-> (Map TxIn (TxOutF era)
    -> Map TxIn (TxOutF era) -> Map TxIn (TxOutF era))
-> RootTarget
     era
     Void
     (Map TxIn (TxOutF era)
      -> Map TxIn (TxOutF era) -> Map TxIn (TxOutF era))
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"mapunion" Map TxIn (TxOutF era)
-> Map TxIn (TxOutF era) -> Map TxIn (TxOutF era)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RootTarget
  era
  Void
  (Map TxIn (TxOutF era)
   -> Map TxIn (TxOutF era) -> Map TxIn (TxOutF era))
-> Term era (Map TxIn (TxOutF era))
-> Target era (Map TxIn (TxOutF era) -> Map TxIn (TxOutF era))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
preUtxo Target era (Map TxIn (TxOutF era) -> Map TxIn (TxOutF era))
-> Term era (Map TxIn (TxOutF era))
-> RootTarget era Void (Map TxIn (TxOutF era))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
colUtxo)
  , Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
preUtxo) (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo)
  , Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo) Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
txinUniv
  , Term era (Set (TxOutF era))
-> Term era (Set (TxOutF era)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map TxIn (TxOutF era)) -> Term era (Set (TxOutF era))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map TxIn (TxOutF era))
colUtxo) (Proof era -> Term era (Set (TxOutF era))
forall era. Era era => Proof era -> Term era (Set (TxOutF era))
colTxoutUniv Proof era
p)
  , Term era TxIn -> Term era (Set TxIn) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era TxIn
forall era. Era era => Term era TxIn
feeTxIn (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo)
  , Term era (TxOutF era) -> Term era (Set (TxOutF era)) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era (TxOutF era)
forall era. Reflect era => Term era (TxOutF era)
feeTxOut (Term era (Map TxIn (TxOutF era)) -> Term era (Set (TxOutF era))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map TxIn (TxOutF era))
colUtxo)
  , Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instantStakeTerm Term era (Map (Credential 'Staking) Coin)
-> RootTarget era Void (Map (Credential 'Staking) Coin) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Proof era -> RootTarget era Void (Map (Credential 'Staking) Coin)
forall era.
Reflect era =>
Proof era -> Target era (Map (Credential 'Staking) Coin)
instantStakeTarget Proof era
p -- Computes instantStake from the Term 'utxo' and the proof 'p'
  ]
  where
    colUtxo :: Term era (Map TxIn (TxOutF era))
colUtxo = V era (Map TxIn (TxOutF era)) -> Term era (Map TxIn (TxOutF era))
forall era t. V era t -> Term era t
Var (String
-> Rep era (Map TxIn (TxOutF era))
-> Access era Any (Map TxIn (TxOutF era))
-> V era (Map TxIn (TxOutF era))
forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"colUtxo" (Rep era TxIn
-> Rep era (TxOutF era) -> Rep era (Map TxIn (TxOutF era))
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era TxIn
forall era. Era era => Rep era TxIn
TxInR (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) Access era Any (Map TxIn (TxOutF era))
forall era s t. Access era s t
No)
    utxoSize :: Term era Size
utxoSize = V era Size -> Term era Size
forall era t. V era t -> Term era t
Var (String -> Rep era Size -> Access era Any Size -> V era Size
forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"utxoSize" Rep era Size
forall era. Rep era Size
SizeR Access era Any Size
forall era s t. Access era s t
No)
    preUtxo :: Term era (Map TxIn (TxOutF era))
preUtxo = V era (Map TxIn (TxOutF era)) -> Term era (Map TxIn (TxOutF era))
forall era t. V era t -> Term era t
Var (String
-> Rep era (Map TxIn (TxOutF era))
-> Access era Any (Map TxIn (TxOutF era))
-> V era (Map TxIn (TxOutF era))
forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preUtxo" (Rep era TxIn
-> Rep era (TxOutF era) -> Rep era (Map TxIn (TxOutF era))
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era TxIn
forall era. Era era => Rep era TxIn
TxInR (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) Access era Any (Map TxIn (TxOutF era))
forall era s t. Access era s t
No)

utxoStage ::
  Reflect era =>
  UnivSize ->
  Proof era ->
  Subst era ->
  Gen (Subst era)
utxoStage :: forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
usize Proof era
proof Subst era
subst0 = do
  let preds :: [Pred era]
preds = UnivSize -> Proof era -> [Pred era]
forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
utxoPreds UnivSize
usize Proof era
proof
  Subst era
subst <- Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo [Pred era]
preds Subst era
subst0
  (Any
_env, Maybe String
status) <- (Any, Maybe String) -> Gen (Any, Maybe String)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Any
forall a. HasCallStack => String -> a
error String
"not used in utxoStage", Maybe String
forall a. Maybe a
Nothing) -- monadTyped $ checkForSoundness preds subst
  case Maybe String
status of
    Maybe String
Nothing -> Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
subst
    Just String
msg -> String -> Gen (Subst era)
forall a. HasCallStack => String -> a
error String
msg

demoUTxO :: Reflect era => Proof era -> ReplMode -> IO ()
demoUTxO :: forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoUTxO Proof era
proof ReplMode
mode = do
  Env era
env <-
    Gen (Env era) -> IO (Env era)
forall a. Gen a -> IO a
generate
      ( Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof era
proof
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
forall a. Default a => a
def Proof era
proof
          Gen (Subst era) -> (Subst era -> Gen (Env era)) -> Gen (Env era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv)
      )
  Map TxIn (TxOutF era)
utx <- Typed (Map TxIn (TxOutF era)) -> IO (Map TxIn (TxOutF era))
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Map TxIn (TxOutF era)) -> IO (Map TxIn (TxOutF era)))
-> Typed (Map TxIn (TxOutF era)) -> IO (Map TxIn (TxOutF era))
forall a b. (a -> b) -> a -> b
$ Env era
-> Term era (Map TxIn (TxOutF era))
-> Typed (Map TxIn (TxOutF era))
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
proof)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (PDoc -> String
forall a. Show a => a -> String
show (Proof era -> UTxO era -> PDoc
forall era. Proof era -> UTxO era -> PDoc
pcUTxO Proof era
proof (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
utx)))
  ReplMode -> Proof era -> Env era -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env String
""