{-# 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 =
  [ 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)
  , 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
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
6) Term era (Map TxIn (TxOutF era))
colUtxo
  , 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 forall era. Era era => Term era TxIn
feeTxIn forall era. Reflect era => Term era (TxOutF era)
feeTxOut (forall a b. b -> Either a b
Right Term era (Map TxIn (TxOutF era))
preUtxo)
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
preUtxo) forall era. Era era => Term era (Set TxIn)
txinUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (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) (forall era. Era era => Proof era -> Term era (Set (TxOutF era))
txoutUniv Proof era
p)
  , forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"mapunion" forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
preUtxo forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
colUtxo)
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
preUtxo) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo)
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo) forall era. Era era => Term era (Set TxIn)
txinUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (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) (forall era. Era era => Proof era -> Term era (Set (TxOutF era))
colTxoutUniv Proof era
p)
  , forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember forall era. Era era => Term era TxIn
feeTxIn (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo)
  , forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember forall era. Reflect era => Term era (TxOutF era)
feeTxOut (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)
  , forall era. Era era => Term era (Map (Credential 'Staking) Coin)
incrementalStake forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Proof era -> Target era (Map (Credential 'Staking) Coin)
incrementalStakeT Proof era
p -- Computes incrementalStake from the Term 'utxo' and the proof 'p'
  ]
  where
    colUtxo :: Term era (Map TxIn (TxOutF era))
colUtxo = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"colUtxo" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era TxIn
TxInR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) forall era s t. Access era s t
No)
    utxoSize :: Term era Size
utxoSize = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"utxoSize" forall era. Rep era Size
SizeR forall era s t. Access era s t
No)
    preUtxo :: Term era (Map TxIn (TxOutF era))
preUtxo = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"preUtxo" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era TxIn
TxInR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) 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 = forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
utxoPreds UnivSize
usize Proof era
proof
  Subst era
subst <- 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) <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. HasCallStack => String -> a
error String
"not used in utxoStage", forall a. Maybe a
Nothing) -- monadTyped $ checkForSoundness preds subst
  case Maybe String
status of
    Maybe String
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
subst
    Just String
msg -> 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 <-
    forall a. Gen a -> IO a
generate
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof era
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage forall a. Default a => a
def Proof era
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv)
      )
  Map TxIn (TxOutF era)
utx <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
proof)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall era. Proof era -> UTxO era -> PDoc
pcUTxO Proof era
proof (forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
utx)))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env String
""