{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Cardano.Ledger.Allegra.Imp.UtxoSpec (spec) where

import Cardano.Ledger.Allegra.Rules
import Cardano.Ledger.Allegra.Scripts
import Cardano.Ledger.Allegra.TxBody
import Cardano.Ledger.Core
import Cardano.Slotting.Slot (SlotNo (..))
import Lens.Micro ((&), (.~))
import Test.Cardano.Ledger.Allegra.ImpTest
import Test.Cardano.Ledger.Imp.Common

spec ::
  forall era.
  AllegraEraImp era =>
  SpecWith (ImpInit (LedgerSpec era))
spec :: forall era.
AllegraEraImp era =>
SpecWith (ImpInit (LedgerSpec era))
spec =
  String
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"UTXO" (SpecWith (ImpInit (LedgerSpec era))
 -> SpecWith (ImpInit (LedgerSpec era)))
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
forall a b. (a -> b) -> a -> b
$ do
    String
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"validity interval" (SpecWith (ImpInit (LedgerSpec era))
 -> SpecWith (ImpInit (LedgerSpec era)))
-> SpecWith (ImpInit (LedgerSpec era))
-> SpecWith (ImpInit (LedgerSpec era))
forall a b. (a -> b) -> a -> b
$ do
      let situations :: a -> a -> [(StrictMaybe a, StrictMaybe a, Bool)]
situations a
x a
d =
            [ (StrictMaybe a
lo, StrictMaybe a
hi, Bool
loOk Bool -> Bool -> Bool
&& Bool
hiOk)
            | (StrictMaybe a
lo, Bool
loOk) <-
                [ (StrictMaybe a
forall a. StrictMaybe a
SNothing, Bool
True)
                , (a -> StrictMaybe a
forall a. a -> StrictMaybe a
SJust (a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
d), Bool
True)
                , (a -> StrictMaybe a
forall a. a -> StrictMaybe a
SJust a
x, Bool
True)
                , (a -> StrictMaybe a
forall a. a -> StrictMaybe a
SJust (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
d), Bool
False)
                ]
            , (StrictMaybe a
hi, Bool
hiOk) <-
                [ (StrictMaybe a
forall a. StrictMaybe a
SNothing, Bool
True)
                , (a -> StrictMaybe a
forall a. a -> StrictMaybe a
SJust (a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
d), Bool
False)
                , (a -> StrictMaybe a
forall a. a -> StrictMaybe a
SJust a
x, Bool
False)
                , (a -> StrictMaybe a
forall a. a -> StrictMaybe a
SJust (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
d), Bool
True)
                ]
            ]
          test :: SlotNo -> SlotNo -> ImpM (LedgerSpec era) ()
test SlotNo
currentSlot SlotNo
d =
            [(StrictMaybe SlotNo, StrictMaybe SlotNo, Bool)]
-> ((StrictMaybe SlotNo, StrictMaybe SlotNo, Bool)
    -> ImpM (LedgerSpec era) ())
-> ImpM (LedgerSpec era) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (SlotNo
-> SlotNo -> [(StrictMaybe SlotNo, StrictMaybe SlotNo, Bool)]
forall {a}.
Num a =>
a -> a -> [(StrictMaybe a, StrictMaybe a, Bool)]
situations SlotNo
currentSlot SlotNo
d) (((StrictMaybe SlotNo, StrictMaybe SlotNo, Bool)
  -> ImpM (LedgerSpec era) ())
 -> ImpM (LedgerSpec era) ())
-> ((StrictMaybe SlotNo, StrictMaybe SlotNo, Bool)
    -> ImpM (LedgerSpec era) ())
-> ImpM (LedgerSpec era) ()
forall a b. (a -> b) -> a -> b
$ \(StrictMaybe SlotNo
lo, StrictMaybe SlotNo
hi, Bool
expectedSuccess) -> do
              let validityInterval :: ValidityInterval
validityInterval = StrictMaybe SlotNo -> StrictMaybe SlotNo -> ValidityInterval
ValidityInterval StrictMaybe SlotNo
lo StrictMaybe SlotNo
hi
                  tx :: Tx TopTx era
tx = TxBody TopTx era -> Tx TopTx era
forall era (l :: TxLevel). EraTx era => TxBody l era -> Tx l era
forall (l :: TxLevel). TxBody l era -> Tx l era
mkBasicTx (TxBody TopTx era -> Tx TopTx era)
-> TxBody TopTx era -> Tx TopTx era
forall a b. (a -> b) -> a -> b
$ TxBody TopTx era
forall era (l :: TxLevel).
(EraTxBody era, Typeable l) =>
TxBody l era
forall (l :: TxLevel). Typeable l => TxBody l era
mkBasicTxBody TxBody TopTx era
-> (TxBody TopTx era -> TxBody TopTx era) -> TxBody TopTx era
forall a b. a -> (a -> b) -> b
& (ValidityInterval -> Identity ValidityInterval)
-> TxBody TopTx era -> Identity (TxBody TopTx era)
forall era (l :: TxLevel).
AllegraEraTxBody era =>
Lens' (TxBody l era) ValidityInterval
forall (l :: TxLevel). Lens' (TxBody l era) ValidityInterval
vldtTxBodyL ((ValidityInterval -> Identity ValidityInterval)
 -> TxBody TopTx era -> Identity (TxBody TopTx era))
-> ValidityInterval -> TxBody TopTx era -> TxBody TopTx era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ValidityInterval
validityInterval
              if Bool
expectedSuccess
                then
                  forall era.
(HasCallStack, ShelleyEraImp era) =>
Tx TopTx era -> ImpTestM era ()
submitTx_ @era Tx TopTx era
tx
                else
                  Tx TopTx era
-> NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> ImpM (LedgerSpec era) ()
forall era.
(HasCallStack, ShelleyEraImp era) =>
Tx TopTx era
-> NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> ImpTestM era ()
submitFailingTx
                    Tx TopTx era
tx
                    [AllegraUtxoPredFailure era -> EraRuleFailure "LEDGER" era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (AllegraUtxoPredFailure era -> EraRuleFailure "LEDGER" era)
-> AllegraUtxoPredFailure era -> EraRuleFailure "LEDGER" era
forall a b. (a -> b) -> a -> b
$ ValidityInterval -> SlotNo -> AllegraUtxoPredFailure era
forall era.
ValidityInterval -> SlotNo -> AllegraUtxoPredFailure era
OutsideValidityIntervalUTxO ValidityInterval
validityInterval SlotNo
currentSlot]
      String
-> ImpM (LedgerSpec era) ()
-> SpecWith (Arg (ImpM (LedgerSpec era) ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"corner cases around the current slot" (ImpM (LedgerSpec era) ()
 -> SpecWith (Arg (ImpM (LedgerSpec era) ())))
-> ImpM (LedgerSpec era) ()
-> SpecWith (Arg (ImpM (LedgerSpec era) ()))
forall a b. (a -> b) -> a -> b
$ do
        currentSlot <- ImpTestM era SlotNo
forall era. ImpTestM era SlotNo
getCurSlotNo
        test currentSlot 1

      String
-> ImpM (LedgerSpec era) ()
-> SpecWith (Arg (ImpM (LedgerSpec era) ()))
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"cases around the current slot" (ImpM (LedgerSpec era) ()
 -> SpecWith (Arg (ImpM (LedgerSpec era) ())))
-> ImpM (LedgerSpec era) ()
-> SpecWith (Arg (ImpM (LedgerSpec era) ()))
forall a b. (a -> b) -> a -> b
$ do
        currentSlot <- ImpTestM era SlotNo
forall era. ImpTestM era SlotNo
getCurSlotNo
        d <- SlotNo <$> choose (2, unSlotNo currentSlot)
        test currentSlot d