{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Constrained.Preds.PParams (
  pParamsPreds,
  pParamsStage,
  extract,
  mainPParams,
  demoTest,
) where

import Cardano.Ledger.Alonzo.Scripts (ExUnits (..))
import qualified Cardano.Ledger.Alonzo.Scripts as Script (Prices (..))
import Cardano.Ledger.Api.Era
import Cardano.Ledger.BaseTypes (
  EpochInterval (..),
  NonNegativeInterval,
  boundRational,
 )
import Cardano.Ledger.Coin (Coin (..))
import Control.Monad (when)
import GHC.Num (Natural)
import Lens.Micro ((^.))
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (OrdCond (..))
import Test.Cardano.Ledger.Constrained.Env (Access (..), V (..), emptyEnv)
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Rewrite (standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Solver
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.Fields
import Test.Cardano.Ledger.Generic.Functions (protocolVersion)
import Test.Cardano.Ledger.Generic.Proof
import Test.Cardano.Ledger.Generic.Updaters (defaultCostModels, newPParams)
import Test.Tasty (TestTree, defaultMain)
import Test.Tasty.QuickCheck

extract :: Era era => Term era t -> Term era s -> Pred era
extract :: forall era t s. Era era => Term era t -> Term era s -> Pred era
extract term :: Term era t
term@(Var (V String
_ Rep era t
_ (Yes Rep era s
r1 Lens' s t
lens))) Term era s
record =
  case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era s
r1 (forall era t. Era era => Term era t -> Rep era t
termRep Term era s
record) of
    Just s :~: s
Refl -> Term era t
term forall era n r. Term era n -> RootTarget era r n -> Pred era
:<-: (forall n r era. String -> (n -> r) -> RootTarget era Void (n -> r)
Constr String
"lookup" (\s
x -> s
x forall s a. s -> Getting a s a -> a
^. Lens' s t
lens) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era s
record)
    Maybe (s :~: s)
Nothing -> forall a. HasCallStack => String -> a
error (String
"Term " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era t
term forall a. [a] -> [a] -> [a]
++ String
" with bad Access in extract2")
extract Term era t
term Term era s
_ = forall a. HasCallStack => String -> a
error (String
"Non Var term " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era t
term forall a. [a] -> [a] -> [a]
++ String
" in extract2")

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

nonNegativeInterval :: Rational -> NonNegativeInterval
nonNegativeInterval :: Rational -> NonNegativeInterval
nonNegativeInterval Rational
r = case (forall r. BoundedRational r => Rational -> Maybe r
boundRational @NonNegativeInterval Rational
r) of
  Just NonNegativeInterval
nn -> NonNegativeInterval
nn
  Maybe NonNegativeInterval
Nothing -> forall a. HasCallStack => String -> a
error (String
"Can't make NonNegativeInterval from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
r)

{- Preds we want to be True in pparams. This comment is meant as a statement of intent
   The actual code acheives this algorithmically, but we want this declaration of what should be true
  [ Sized (AtLeast 1) (maxBHSize proof)
  , Sized (AtLeast 1) (maxTxSize proof)
  , SumsTo (Right 1) (maxBBSize proof) LTE [One (maxBHSize proof), One (maxTxSize proof)]
  , Component
      (Right (pparams proof))
      [field pp (maxTxSize proof), field pp (maxBHSize proof), field pp (maxBBSize proof)]
  ]
-}

genPParams :: Reflect era => Proof era -> Natural -> Natural -> Natural -> Gen (PParamsF era)
genPParams :: forall era.
Reflect era =>
Proof era -> Natural -> Natural -> Natural -> Gen (PParamsF era)
genPParams Proof era
proof Natural
tx Natural
bb Natural
bh = do
  ExUnits
maxTxExUnits2 <-
    Natural -> Natural -> ExUnits
ExUnits
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Int
100 :: Int, Int
10000))
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Int
100 :: Int, Int
10000))
  Natural
maxCollateralInputs <- forall a. HasCallStack => [a] -> Gen a
elements [Natural
3 .. Natural
5]
  Natural
collateralPercentage2 <- forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
chooseInt (Int
1, Int
200)
  Coin
minfeeA <- Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
100)
  Coin
minfeeB <- Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
10)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall era. Proof era -> PParams era -> PParamsF era
PParamsF Proof era
proof forall a b. (a -> b) -> a -> b
$
        forall era.
EraPParams era =>
Proof era -> [PParamsField era] -> PParams era
newPParams
          Proof era
proof
          [ forall era. Coin -> PParamsField era
MinfeeA Coin
minfeeA
          , forall era. Coin -> PParamsField era
MinfeeB Coin
minfeeB
          , forall era. Prices -> PParamsField era
Prices (NonNegativeInterval -> NonNegativeInterval -> Prices
Script.Prices (Rational -> NonNegativeInterval
nonNegativeInterval Rational
1.0) (Rational -> NonNegativeInterval
nonNegativeInterval Rational
1.0))
          , forall era. Proof era -> PParamsField era
defaultCostModels Proof era
proof
          , forall era. Natural -> PParamsField era
MaxValSize Natural
1000
          , forall era. Word32 -> PParamsField era
MaxTxSize (forall a b.
(HasCallStack, Integral a, Show a, Integral b, Bounded b,
 Show b) =>
String -> a -> b
fromIntegralBounded String
"TxSize" Natural
tx) -- In the Model these are Natural
          , forall era. Word32 -> PParamsField era
MaxBBSize (forall a b.
(HasCallStack, Integral a, Show a, Integral b, Bounded b,
 Show b) =>
String -> a -> b
fromIntegralBounded String
"BlockBodySize" Natural
bb) -- But in the PParams, they are
          , forall era. Word16 -> PParamsField era
MaxBHSize (forall a b.
(HasCallStack, Integral a, Show a, Integral b, Bounded b,
 Show b) =>
String -> a -> b
fromIntegralBounded String
"BlockHeaderSize" Natural
bh) -- Word32, Word32, and Word16
          , forall era. ExUnits -> PParamsField era
MaxTxExUnits ExUnits
maxTxExUnits2
          , forall era. Natural -> PParamsField era
MaxCollateralInputs Natural
maxCollateralInputs
          , forall era. Natural -> PParamsField era
CollateralPercentage Natural
collateralPercentage2
          , forall era. ProtVer -> PParamsField era
ProtocolVersion forall a b. (a -> b) -> a -> b
$ forall era. Proof era -> ProtVer
protocolVersion Proof era
proof
          , forall era. Coin -> PParamsField era
PoolDeposit forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
5
          , forall era. Coin -> PParamsField era
KeyDeposit forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
2
          , forall era. Coin -> PParamsField era
DRepDeposit forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
7
          , forall era. Coin -> PParamsField era
GovActionDeposit forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
13
          , forall era. EpochInterval -> PParamsField era
DRepActivity forall a b. (a -> b) -> a -> b
$ Word32 -> EpochInterval
EpochInterval Word32
8
          , forall era. EpochInterval -> PParamsField era
EMax forall a b. (a -> b) -> a -> b
$ Word32 -> EpochInterval
EpochInterval Word32
100
          ]
    )

pParamsPreds :: Reflect era => Proof era -> [Pred era]
pParamsPreds :: forall era. Reflect era => Proof era -> [Pred era]
pParamsPreds Proof era
p =
  [ forall era n r. Term era n -> RootTarget era r (Gen n) -> Pred era
GenFrom
      (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
      ( forall n r era. String -> (n -> r) -> RootTarget era Void (n -> r)
Constr String
"genPParams" (forall era.
Reflect era =>
Proof era -> Natural -> Natural -> Natural -> Gen (PParamsF era)
genPParams Proof era
p)
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
p)
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
p)
          forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
p)
      )
  , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. Era era => Proof era -> Term era Coin
minFeeB Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. Era era => Proof era -> Term era Coin
keyDepAmt Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. Era era => Proof era -> Term era Coin
poolDepAmt Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. Era era => Proof era -> Term era EpochInterval
maxEpoch Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
  , forall n era. Sizeable n => Term era Size -> Term era n -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
100) (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
p)
  , forall n era. Sizeable n => Term era Size -> Term era n -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
40000) (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
p)
  , forall era n.
(Era era, Adds n) =>
Direct n -> Term era n -> OrdCond -> [Sum era n] -> Pred era
SumsTo (forall a b. b -> Either a b
Right Natural
1) (forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
p) OrdCond
LTE [forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
p), forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
p)]
  , (forall era. Era era => Proof era -> Term era ProtVer
protVer Proof era
p) forall n era. Count n => Term era n -> Term era n -> Pred era
`CanFollow` (forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof era
p)
  ]
    forall a. [a] -> [a] -> [a]
++ ( case forall era. Proof era -> PParamsWit era
whichPParams Proof era
p of
          PParamsWit era
PParamsShelleyToMary -> []
          PParamsWit era
PParamsAlonzoToAlonzo ->
            [ forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. AlonzoEraPParams era => Proof era -> Term era Natural
collateralPercentage Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            ]
          PParamsWit era
PParamsBabbageToBabbage ->
            [ forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. AlonzoEraPParams era => Proof era -> Term era Natural
collateralPercentage Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            ]
          PParamsWit era
PParamsConwayToConway ->
            [ forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. AlonzoEraPParams era => Proof era -> Term era Natural
collateralPercentage Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era.
ConwayEraPParams era =>
Proof era -> Term era EpochInterval
drepActivity Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. ConwayEraPParams era => Proof era -> Term era Coin
drepDeposit Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            , forall era t s. Era era => Term era t -> Term era s -> Pred era
extract (forall era. ConwayEraPParams era => Proof era -> Term era Coin
proposalDeposit Proof era
p) (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p)
            ]
       )

pParamsStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
pParamsStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof = forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (forall era. Reflect era => Proof era -> [Pred era]
pParamsPreds Proof era
proof)

demo :: ReplMode -> IO ()
demo :: ReplMode -> IO ()
demo ReplMode
mode = do
  let proof :: Proof (BabbageEra StandardCrypto)
proof = Proof (BabbageEra StandardCrypto)
Babbage
  Subst (BabbageEra StandardCrypto)
subst <- forall a. Gen a -> IO a
generate (forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof (BabbageEra StandardCrypto)
proof forall era. Subst era
emptySubst)
  Env (BabbageEra StandardCrypto)
env <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst (BabbageEra StandardCrypto)
subst forall era. Env era
emptyEnv)
  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 String
"\n" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn (forall a. Show a => a -> String
show Subst (BabbageEra StandardCrypto)
subst)
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof (BabbageEra StandardCrypto)
proof Env (BabbageEra StandardCrypto)
env String
""

demoTest :: TestTree
demoTest :: TestTree
demoTest = forall a. String -> IO a -> TestTree
testIO String
"Testing TxOut Stage" (ReplMode -> IO ()
demo ReplMode
CI)

mainPParams :: IO ()
mainPParams :: IO ()
mainPParams = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing TxOut Stage" (ReplMode -> IO ()
demo ReplMode
Interactive)