ENACT conformance done

eras/alonzo/impl/CHANGELOG.md

@@ -3,6 +3,7 @@
 ## 1.8.1.0
 
 * Add `AllegraEraScript` and `ShelleyEraScript` instances for `AlonzoEra`
+* Add `Inject` instance for `AlonzoTx`
 
 ## testlib
 

eras/conway/impl/CHANGELOG.md

@@ -2,12 +2,27 @@
 
 ## 1.14.1.0
 
-* Add `NFData` instance for `RatifySignal`
+* Add `Inject` instances for:
+  * `EnactState`
+  * `RatifyState`
+  * `RatifySignal`
+  * `RatifyEnv`
+  * `GovProcedures`
+  * `Proposals`
+  * `CertEnv`
+  * `EnactSignal`
+  * `GovEnv`
+  * `ConwayTxCert`
+* Add `NFData` instances for:
+  * `RatifySignal`
+  * `EnactSignal`
 * Add `AllegraEraScript` and `ShelleyEraScript` instances for `ConwayEra`
 
 ### `testlib`
 
-* Add `ToExpr` instance for `RatifySignal`
+* Add `ToExpr` instances for:
+  * `RatifySignal`
+  * `EnactSignal`
 
 ## 1.14.0.0
 

eras/shelley/impl/CHANGELOG.md

@@ -12,6 +12,9 @@
 * Change signatures of `evalMultiSig` and `validateMultiSig`:
   * replace `Era` constraint with `ShelleyEraScript`
   * replace `MultiSig` with `NativeScript`
+* Add `Inject` instances for:
+  * `UTxOState`
+  * `UtxoEnv`
 
 ### testlib
 * Change signatures of `Arbitrary` instances for `MultiSig`:

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs

@@ -25,6 +25,7 @@ import Cardano.Ledger.Conway (Conway)
 import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParamsUpdate)
 import Cardano.Ledger.Conway.Governance (
   EnactState,
+  GovAction,
   GovActionId,
   GovActionState (..),
   GovProcedures (..),
@@ -38,7 +39,7 @@ import Cardano.Ledger.Conway.Governance (
   toPrevGovActionIds,
  )
 import Cardano.Ledger.Conway.PParams (THKD (..))
-import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, RatifyState)
+import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, EnactSignal, RatifyState)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
 import Cardano.Ledger.Credential (Credential)
@@ -221,21 +222,27 @@ agdaCompatiblePPU ppup =
         (branch $ const False)
         (branch $ const True)
 
+agdaCompatibleGovAction ::
+  IsConwayUniv fn =>
+  Term fn (GovAction Conway) ->
+  Pred fn
+agdaCompatibleGovAction govAction =
+  caseOn
+    govAction
+    (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
+    (branch $ \_ _ -> True)
+    (branch $ \_ _ -> True)
+    (branch $ const True)
+    (branch $ \_ _ _ _ -> True)
+    (branch $ \_ _ -> True)
+    (branch $ const True)
+
 agdaCompatibleProposal ::
   IsConwayUniv fn =>
   Term fn (ProposalProcedure Conway) ->
   Pred fn
 agdaCompatibleProposal prop =
-  match prop $ \_ _ govAction _ ->
-    caseOn
-      govAction
-      (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
-      (branch $ \_ _ -> True)
-      (branch $ \_ _ -> True)
-      (branch $ const True)
-      (branch $ \_ _ _ _ -> True)
-      (branch $ \_ _ -> True)
-      (branch $ const True)
+  match prop $ \_ _ govAction _ -> agdaCompatibleGovAction govAction
 
 agdaCompatibleGAS ::
   IsConwayUniv fn =>
@@ -536,11 +543,15 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
       $ Agda.ratifyStep env st sig
 
 instance IsConwayUniv fn => ExecSpecRule fn "ENACT" Conway where
-  type ExecEnvironment fn "ENACT" Conway = ConwayExecEnactEnv
+  type ExecEnvironment fn "ENACT" Conway = ConwayExecEnactEnv Conway
 
   environmentSpec _ = TrueSpec
   stateSpec _ _ = TrueSpec
-  signalSpec _ _ _ = TrueSpec
+  signalSpec _ _ _ = onlyMinFeeAUpdates
+    where
+      onlyMinFeeAUpdates :: Specification fn (EnactSignal Conway)
+      onlyMinFeeAUpdates = constrained $ \sig ->
+        match sig $ \_ ga -> agdaCompatibleGovAction ga
   runAgdaRule env st sig =
     first (error "ENACT failed")
       . computationResultToEither

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs

@@ -55,6 +55,12 @@ type ForAllExecTypes (c :: Type -> Constraint) fn rule era =
   , c (ExecSignal fn rule era)
   )
 
+type ForAllExecSpecRep (c :: Type -> Constraint) fn rule era =
+  ( c (SpecRep (ExecEnvironment fn rule era))
+  , c (SpecRep (ExecState fn rule era))
+  , c (SpecRep (ExecSignal fn rule era))
+  )
+
 class
   ( ForAllExecTypes (CV2.HasSpec fn) fn rule era
   , ForAllExecTypes ToExpr fn rule era
@@ -123,9 +129,7 @@ class
       )
   default translateInputs ::
     ( ForAllExecTypes (SpecTranslate (ExecContext fn rule era)) fn rule era
-    , ToExpr (SpecRep (ExecEnvironment fn rule era))
-    , ToExpr (SpecRep (ExecState fn rule era))
-    , ToExpr (SpecRep (ExecSignal fn rule era))
+    , ForAllExecSpecRep ToExpr fn rule era
     ) =>
     ExecEnvironment fn rule era ->
     ExecState fn rule era ->
@@ -152,32 +156,21 @@ class
   testConformance ::
     ( ShelleyEraImp era
     , SpecTranslate (ExecContext fn rule era) (State (EraRule rule era))
+    , ForAllExecSpecRep NFData fn rule era
+    , ForAllExecSpecRep ToExpr fn rule era
+    , ForAllExecSpecRep FixupSpecRep fn rule era
     , NFData (SpecRep (PredicateFailure (EraRule rule era)))
-    , NFData (SpecRep (ExecEnvironment fn rule era))
-    , NFData (SpecRep (ExecState fn rule era))
-    , NFData (SpecRep (ExecSignal fn rule era))
     , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
-    , ToExpr (SpecRep (ExecEnvironment fn rule era))
-    , ToExpr (SpecRep (ExecState fn rule era))
-    , ToExpr (SpecRep (ExecSignal fn rule era))
-    , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
-    , FixupSpecRep (SpecRep (State (EraRule rule era)))
-    , FixupSpecRep (SpecRep (ExecState fn rule era))
     , Eq (SpecRep (PredicateFailure (EraRule rule era)))
     , Eq (SpecRep (ExecState fn rule era))
-    , Inject
-        (SpecRep (ExecEnvironment fn rule era))
-        (SpecRep (ExecEnvironment fn rule era))
-    , Inject
-        (SpecRep (ExecState fn rule era))
-        (SpecRep (ExecState fn rule era))
-    , Inject
-        (SpecRep (ExecSignal fn rule era))
-        (SpecRep (ExecSignal fn rule era))
     , Inject
         (State (EraRule rule era))
         (ExecState fn rule era)
     , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
+    , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
+    , Inject (SpecRep (ExecEnvironment fn rule era)) (SpecRep (ExecEnvironment fn rule era))
+    , Inject (SpecRep (ExecState fn rule era)) (SpecRep (ExecState fn rule era))
+    , Inject (SpecRep (ExecSignal fn rule era)) (SpecRep (ExecSignal fn rule era))
     ) =>
     ExecContext fn rule era ->
     ExecEnvironment fn rule era ->
@@ -216,24 +209,20 @@ checkConformance implResTest agdaResTest = do
 defaultTestConformance ::
   forall fn era rule.
   ( ShelleyEraImp era
+  , ExecSpecRule fn rule era
+  , ForAllExecSpecRep NFData fn rule era
+  , ForAllExecSpecRep ToExpr fn rule era
   , NFData (SpecRep (PredicateFailure (EraRule rule era)))
-  , NFData (SpecRep (ExecEnvironment fn rule era))
-  , NFData (SpecRep (ExecState fn rule era))
-  , NFData (SpecRep (ExecSignal fn rule era))
   , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
-  , ToExpr (SpecRep (ExecEnvironment fn rule era))
-  , ToExpr (SpecRep (ExecState fn rule era))
-  , ToExpr (SpecRep (ExecSignal fn rule era))
-  , ExecSpecRule fn rule era
-  , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
   , Eq (SpecRep (PredicateFailure (EraRule rule era)))
   , Eq (SpecRep (ExecState fn rule era))
+  , Inject (State (EraRule rule era)) (ExecState fn rule era)
+  , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
+  , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
+  , FixupSpecRep (SpecRep (ExecState fn rule era))
   , Inject (SpecRep (ExecEnvironment fn rule era)) (SpecRep (ExecEnvironment fn rule era))
   , Inject (SpecRep (ExecState fn rule era)) (SpecRep (ExecState fn rule era))
   , Inject (SpecRep (ExecSignal fn rule era)) (SpecRep (ExecSignal fn rule era))
-  , FixupSpecRep (SpecRep (ExecState fn rule era))
-  , Inject (State (EraRule rule era)) (ExecState fn rule era)
-  , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
   ) =>
   ExecContext fn rule era ->
   ExecEnvironment fn rule era ->
@@ -248,19 +237,15 @@ runConformance ::
   forall (rule :: Symbol) (fn :: [Type] -> Type -> Type) era.
   ( ExecSpecRule fn rule era
   , NFData (SpecRep (PredicateFailure (EraRule rule era)))
-  , NFData (SpecRep (ExecEnvironment fn rule era))
-  , NFData (SpecRep (ExecState fn rule era))
-  , NFData (SpecRep (ExecSignal fn rule era))
-  , ToExpr (SpecRep (ExecEnvironment fn rule era))
-  , ToExpr (SpecRep (ExecState fn rule era))
-  , ToExpr (SpecRep (ExecSignal fn rule era))
+  , ForAllExecSpecRep NFData fn rule era
+  , ForAllExecSpecRep ToExpr fn rule era
   , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
   , FixupSpecRep (SpecRep (ExecState fn rule era))
+  , Inject (State (EraRule rule era)) (ExecState fn rule era)
+  , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
   , Inject (SpecRep (ExecEnvironment fn rule era)) (SpecRep (ExecEnvironment fn rule era))
   , Inject (SpecRep (ExecState fn rule era)) (SpecRep (ExecState fn rule era))
   , Inject (SpecRep (ExecSignal fn rule era)) (SpecRep (ExecSignal fn rule era))
-  , Inject (State (EraRule rule era)) (ExecState fn rule era)
-  , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
   ) =>
   ExecContext fn rule era ->
   ExecEnvironment fn rule era ->
@@ -298,26 +283,21 @@ conformsToImpl ::
   forall (rule :: Symbol) fn era.
   ( ShelleyEraImp era
   , ExecSpecRule fn rule era
+  , ForAllExecSpecRep NFData fn rule era
+  , ForAllExecSpecRep ToExpr fn rule era
+  , ForAllExecSpecRep FixupSpecRep fn rule era
   , NFData (SpecRep (PredicateFailure (EraRule rule era)))
-  , NFData (SpecRep (ExecEnvironment fn rule era))
-  , NFData (SpecRep (ExecState fn rule era))
-  , NFData (SpecRep (ExecSignal fn rule era))
   , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
   , ToExpr (ExecContext fn rule era)
   , SpecTranslate (ExecContext fn rule era) (State (EraRule rule era))
-  , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
-  , FixupSpecRep (SpecRep (State (EraRule rule era)))
   , Eq (SpecRep (PredicateFailure (EraRule rule era)))
-  , ToExpr (SpecRep (ExecEnvironment fn rule era))
-  , ToExpr (SpecRep (ExecState fn rule era))
-  , ToExpr (SpecRep (ExecSignal fn rule era))
-  , FixupSpecRep (SpecRep (ExecState fn rule era))
   , Inject (SpecRep (ExecEnvironment fn rule era)) (SpecRep (ExecEnvironment fn rule era))
   , Inject (SpecRep (ExecState fn rule era)) (SpecRep (ExecState fn rule era))
   , Inject (SpecRep (ExecSignal fn rule era)) (SpecRep (ExecSignal fn rule era))
   , Inject (State (EraRule rule era)) (ExecState fn rule era)
   , Eq (SpecRep (ExecState fn rule era))
   , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)
+  , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era)))
   ) =>
   Property
 conformsToImpl =

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs

@@ -320,11 +320,6 @@ instance Inject RatifyEnv RatifyEnv
 
 instance Inject CertEnv CertEnv
 
-instance
-  Inject
-    (GovActionID, GovActionState)
-    (GovActionID, GovActionState)
-
 instance Inject EnactEnv EnactEnv
 
 instance Inject RatifyState RatifyState
@@ -344,3 +339,8 @@ instance Inject GovSignal GovSignal
 instance Inject Tx Tx
 
 instance Inject GovAction GovAction
+
+-- GovState
+instance Inject [(GovActionID, GovActionState)] [(GovActionID, GovActionState)]
+
+instance Inject [GovSignal] [GovSignal]

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway.hs

@@ -1114,16 +1114,24 @@ instance EraPParams era => SpecTranslate ctx (EnactSignal era) where
 
   toSpecRep (EnactSignal _ ga) = toSpecRep ga
 
-data ConwayExecEnactEnv = ConwayExecEnactEnv
+data ConwayExecEnactEnv era = ConwayExecEnactEnv
+  { ceeeGid :: GovActionId (EraCrypto era)
+  , ceeeTreasury :: Coin
+  , ceeeEpoch :: EpochNo
+  }
   deriving (Generic, Eq, Show)
 
-instance ToExpr ConwayExecEnactEnv
-instance NFData ConwayExecEnactEnv
+instance ToExpr (ConwayExecEnactEnv era)
+instance Era era => NFData (ConwayExecEnactEnv era)
 
-instance HasSimpleRep ConwayExecEnactEnv
-instance IsConwayUniv fn => HasSpec fn ConwayExecEnactEnv
+instance HasSimpleRep (ConwayExecEnactEnv era)
+instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayExecEnactEnv era)
 
-instance SpecTranslate ctx ConwayExecEnactEnv where
-  type SpecRep ConwayExecEnactEnv = Agda.EnactEnv
+instance SpecTranslate ctx (ConwayExecEnactEnv era) where
+  type SpecRep (ConwayExecEnactEnv era) = Agda.EnactEnv
 
-  toSpecRep _ = undefined
+  toSpecRep ConwayExecEnactEnv {..} =
+    Agda.MkEnactEnv
+      <$> toSpecRep ceeeGid
+      <*> toSpecRep ceeeTreasury
+      <*> toSpecRep ceeeEpoch

libs/cardano-ledger-core/CHANGELOG.md

@@ -1,8 +1,8 @@
 # Version history for `cardano-ledger-core`
 
-## 1.12.0.1
+## 1.12.1.0
 
-*
+* Add `Inject` instance for `CertState`
 
 ## 1.12.0.0
 

libs/cardano-ledger-core/src/Cardano/Ledger/BaseTypes.hs

@@ -855,9 +855,6 @@ instance Inject t () where
 instance Inject Void s where
   inject = absurd
 
-instance Inject a b => Inject [a] [b] where
-  inject = fmap inject
-
 -- | Helper function for a common pattern of creating objects
 kindObject :: Text -> [Pair] -> Value
 kindObject name obj = object $ ("kind" .= name) : obj