{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Conformance.Spec.Conway.Ratify (spec) where

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (
  EnactState,
  GovActionState (..),
  RatifyEnv (..),
  RatifyState (..),
  rsEnactStateL,
 )
import Cardano.Ledger.Conway.Rules qualified as Conway
import Constrained.Generation
import Data.Either (fromRight)
import Lens.Micro
import MAlonzo.Code.Ledger.Conway.Foreign.API qualified as Agda
import Prettyprinter as Pretty
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway ()
import Test.Cardano.Ledger.Conformance.Spec.Core
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Constrained.Conway.MiniTrace (
  ConstrainedGeneratorBundle (..),
  constrainedRatify,
 )
import Test.Cardano.Ledger.Conway.TreeDiff (tableDoc)
import Test.Cardano.Ledger.Imp.Common

conformsToImplAccepted ::
  (RatifyEnv ConwayEra -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool) ->
  ( SpecRep ConwayEra (RatifyEnv ConwayEra) ->
    SpecRep ConwayEra (EnactState ConwayEra) ->
    SpecRep ConwayEra (GovActionState ConwayEra) ->
    Bool
  ) ->
  Property
conformsToImplAccepted :: (RatifyEnv ConwayEra
 -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool)
-> (SpecRep ConwayEra (RatifyEnv ConwayEra)
    -> SpecRep ConwayEra (EnactState ConwayEra)
    -> SpecRep ConwayEra (GovActionState ConwayEra)
    -> Bool)
-> Property
conformsToImplAccepted RatifyEnv ConwayEra
-> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool
impl SpecRep ConwayEra (RatifyEnv ConwayEra)
-> SpecRep ConwayEra (EnactState ConwayEra)
-> SpecRep ConwayEra (GovActionState ConwayEra)
-> Bool
agda = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  let ConstrainedGeneratorBundle {Gen [GovActionState ConwayEra]
[GovActionState ConwayEra]
-> Specification (Environment (EraRule "RATIFY" ConwayEra))
[GovActionState ConwayEra]
-> Environment (EraRule "RATIFY" ConwayEra)
-> Specification (State (EraRule "RATIFY" ConwayEra))
[GovActionState ConwayEra]
-> Environment (EraRule "RATIFY" ConwayEra)
-> State (EraRule "RATIFY" ConwayEra)
-> Gen (Signal (EraRule "RATIFY" ConwayEra))
cgbContextGen :: Gen [GovActionState ConwayEra]
cgbEnvironmentSpec :: [GovActionState ConwayEra]
-> Specification (Environment (EraRule "RATIFY" ConwayEra))
cgbStateSpec :: [GovActionState ConwayEra]
-> Environment (EraRule "RATIFY" ConwayEra)
-> Specification (State (EraRule "RATIFY" ConwayEra))
cgbSignalGen :: [GovActionState ConwayEra]
-> Environment (EraRule "RATIFY" ConwayEra)
-> State (EraRule "RATIFY" ConwayEra)
-> Gen (Signal (EraRule "RATIFY" ConwayEra))
cgbSignalGen :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Gen (Signal (EraRule rule era))
cgbStateSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbEnvironmentSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx -> Specification (Environment (EraRule rule era))
cgbContextGen :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era -> Gen ctx
..} = ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
constrainedRatify
      fromSpecTransM :: Either a b -> b
fromSpecTransM = b -> Either a b -> b
forall b a. b -> Either a b -> b
fromRight (b -> Either a b -> b) -> b -> Either a b -> b
forall a b. (a -> b) -> a -> b
$ String -> b
forall a. HasCallStack => String -> a
error String
"conformsToImplAccepted: translation error"
  govActions <- Gen [GovActionState ConwayEra]
cgbContextGen
  ratifyEnv <- genFromSpec $ cgbEnvironmentSpec govActions
  ratifySt <- genFromSpec $ cgbStateSpec govActions ratifyEnv
  let specEnv = Either Text RatifyEnv -> RatifyEnv
forall {a} {b}. Either a b -> b
fromSpecTransM (Either Text RatifyEnv -> RatifyEnv)
-> Either Text RatifyEnv -> RatifyEnv
forall a b. (a -> b) -> a -> b
$ Coin
-> SpecTransM ConwayEra Coin RatifyEnv -> Either Text RatifyEnv
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM Coin
0 (SpecTransM ConwayEra Coin RatifyEnv -> Either Text RatifyEnv)
-> SpecTransM ConwayEra Coin RatifyEnv -> Either Text RatifyEnv
forall a b. (a -> b) -> a -> b
$ forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep @ConwayEra RatifyEnv ConwayEra
ratifyEnv
      specSt =
        Either Text EnactState -> EnactState
forall {a} {b}. Either a b -> b
fromSpecTransM (Either Text EnactState -> EnactState)
-> Either Text EnactState -> EnactState
forall a b. (a -> b) -> a -> b
$
          () -> SpecTransM ConwayEra () EnactState -> Either Text EnactState
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM () (SpecTransM ConwayEra () EnactState -> Either Text EnactState)
-> SpecTransM ConwayEra () EnactState -> Either Text EnactState
forall a b. (a -> b) -> a -> b
$
            forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep @ConwayEra (RatifyState ConwayEra
ratifySt RatifyState ConwayEra
-> Getting
     (EnactState ConwayEra)
     (RatifyState ConwayEra)
     (EnactState ConwayEra)
-> EnactState ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (EnactState ConwayEra)
  (RatifyState ConwayEra)
  (EnactState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(EnactState era -> f (EnactState era))
-> RatifyState era -> f (RatifyState era)
rsEnactStateL)
      specGovActions = Either Text [GovActionState] -> [GovActionState]
forall {a} {b}. Either a b -> b
fromSpecTransM (Either Text [GovActionState] -> [GovActionState])
-> Either Text [GovActionState] -> [GovActionState]
forall a b. (a -> b) -> a -> b
$ ()
-> SpecTransM ConwayEra () [GovActionState]
-> Either Text [GovActionState]
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM () (SpecTransM ConwayEra () [GovActionState]
 -> Either Text [GovActionState])
-> SpecTransM ConwayEra () [GovActionState]
-> Either Text [GovActionState]
forall a b. (a -> b) -> a -> b
$ forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep @ConwayEra [GovActionState ConwayEra]
govActions
  return $
    conjoin $
      zipWith
        ( \GovActionState ConwayEra
ga GovActionState
sga ->
            let implRes :: Bool
implRes = RatifyEnv ConwayEra
-> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool
impl RatifyEnv ConwayEra
ratifyEnv RatifyState ConwayEra
ratifySt GovActionState ConwayEra
ga
                agdaRes :: Bool
agdaRes = SpecRep ConwayEra (RatifyEnv ConwayEra)
-> SpecRep ConwayEra (EnactState ConwayEra)
-> SpecRep ConwayEra (GovActionState ConwayEra)
-> Bool
agda SpecRep ConwayEra (RatifyEnv ConwayEra)
RatifyEnv
specEnv SpecRep ConwayEra (EnactState ConwayEra)
EnactState
specSt SpecRep ConwayEra (GovActionState ConwayEra)
GovActionState
sga
             in String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (RatifyEnv ConwayEra
-> RatifyState ConwayEra
-> GovActionState ConwayEra
-> Bool
-> Bool
-> String
forall {a} {a} {a}.
(ToExpr a, ToExpr a, ToExpr a) =>
a -> a -> a -> Bool -> Bool -> String
prettify RatifyEnv ConwayEra
ratifyEnv RatifyState ConwayEra
ratifySt GovActionState ConwayEra
ga Bool
implRes Bool
agdaRes) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
                  Bool
implRes Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
agdaRes
        )
        govActions
        specGovActions
  where
    prettify :: a -> a -> a -> Bool -> Bool -> String
prettify a
ratifyEnv a
ratifySt a
ga Bool
implRes Bool
agdaRes =
      Doc AnsiStyle -> String
ansiDocToString (Doc AnsiStyle -> String) -> Doc AnsiStyle -> String
forall a b. (a -> b) -> a -> b
$
        [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
Pretty.vsep ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle] -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$
          Maybe (Doc AnsiStyle) -> [(String, Doc AnsiStyle)] -> Doc AnsiStyle
tableDoc Maybe (Doc AnsiStyle)
forall a. Maybe a
Nothing [(String
"Impl:", Bool -> Doc AnsiStyle
forall {ann}. Bool -> Doc ann
showAccepted Bool
implRes), (String
"Spec:", Bool -> Doc AnsiStyle
forall {ann}. Bool -> Doc ann
showAccepted Bool
agdaRes)]
            Doc AnsiStyle -> [Doc AnsiStyle] -> [Doc AnsiStyle]
forall a. a -> [a] -> [a]
: [a -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr a
ratifyEnv, a -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr a
ratifySt, a -> Doc AnsiStyle
forall a. ToExpr a => a -> Doc AnsiStyle
ansiExpr a
ga]

    showAccepted :: Bool -> Doc ann
showAccepted Bool
True = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
Pretty.brackets Doc ann
"✓"
    showAccepted Bool
False = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
Pretty.brackets Doc ann
"×"

spec :: Spec
spec :: Spec
spec = String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"RATIFY" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"STS" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
-> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
constrainedRatify
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Accepted" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    [(String,
  (RatifyEnv ConwayEra
   -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool,
   RatifyEnv -> EnactState -> GovActionState -> Bool))]
-> ((String,
     (RatifyEnv ConwayEra
      -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool,
      RatifyEnv -> EnactState -> GovActionState -> Bool))
    -> Spec)
-> Spec
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_
      [ (String
"DRep", (RatifyEnv ConwayEra
-> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool
forall era.
ConwayEraPParams era =>
RatifyEnv era -> RatifyState era -> GovActionState era -> Bool
Conway.dRepAccepted, RatifyEnv -> EnactState -> GovActionState -> Bool
Agda.acceptedByDRep))
      , (String
"SPO", (RatifyEnv ConwayEra
-> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool
forall era.
(ConwayEraPParams era, ConwayEraAccounts era) =>
RatifyEnv era -> RatifyState era -> GovActionState era -> Bool
Conway.spoAccepted, RatifyEnv -> EnactState -> GovActionState -> Bool
Agda.acceptedBySPO))
      , (String
"CC", (RatifyEnv ConwayEra
-> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool
forall era.
ConwayEraPParams era =>
RatifyEnv era -> RatifyState era -> GovActionState era -> Bool
Conway.committeeAccepted, RatifyEnv -> EnactState -> GovActionState -> Bool
Agda.acceptedByCC))
      ]
      (((String,
   (RatifyEnv ConwayEra
    -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool,
    RatifyEnv -> EnactState -> GovActionState -> Bool))
  -> Spec)
 -> Spec)
-> ((String,
     (RatifyEnv ConwayEra
      -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool,
      RatifyEnv -> EnactState -> GovActionState -> Bool))
    -> Spec)
-> Spec
forall a b. (a -> b) -> a -> b
$ \(String
l, (RatifyEnv ConwayEra
-> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool
impl, RatifyEnv -> EnactState -> GovActionState -> Bool
agda)) ->
        String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
l (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ (RatifyEnv ConwayEra
 -> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool)
-> (SpecRep ConwayEra (RatifyEnv ConwayEra)
    -> SpecRep ConwayEra (EnactState ConwayEra)
    -> SpecRep ConwayEra (GovActionState ConwayEra)
    -> Bool)
-> Property
conformsToImplAccepted RatifyEnv ConwayEra
-> RatifyState ConwayEra -> GovActionState ConwayEra -> Bool
impl SpecRep ConwayEra (RatifyEnv ConwayEra)
-> SpecRep ConwayEra (EnactState ConwayEra)
-> SpecRep ConwayEra (GovActionState ConwayEra)
-> Bool
RatifyEnv -> EnactState -> GovActionState -> Bool
agda