Replace Sums constraints with Lenses for specs (Aniket Deshpande)

Added type family witness added to Proof.hs. computing fees.
Added support for Conway DCert in Preds/Certs.hs
Added TxOuts to Universes

libs/cardano-ledger-test/cardano-ledger-test.cabal

@@ -30,6 +30,8 @@ library
         Test.Cardano.Ledger.Constrained.Preds.TxOut
         Test.Cardano.Ledger.Constrained.Preds.TxBody
         Test.Cardano.Ledger.Constrained.Preds.DPState
+        Test.Cardano.Ledger.Constrained.Preds.Repl
+        Test.Cardano.Ledger.Constrained.Preds.Certs
         Test.Cardano.Ledger.Constrained.Spec
         Test.Cardano.Ledger.Constrained.SpecClass
         Test.Cardano.Ledger.Constrained.Tests

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Ast.hs

@@ -30,7 +30,6 @@ import Test.Cardano.Ledger.Constrained.Classes (
   Count (..),
   ScriptF (..),
   Sizeable (..),
-  Sums (..),
  )
 import Test.Cardano.Ledger.Constrained.Env (
   Access (..),
@@ -47,7 +46,7 @@ import Test.Cardano.Ledger.Constrained.Monad (HasConstraint (With), Typed (..),
 import Test.Cardano.Ledger.Constrained.Size (OrdCond (..), Size (..), runOrdCond, runSize, seps)
 import Test.Cardano.Ledger.Constrained.TypeRep (Rep (..), hasEq, synopsis, testEql, (:~:) (Refl))
 import Test.Cardano.Ledger.Generic.Proof (Reflect)
-import Test.QuickCheck (Gen)
+import Test.QuickCheck (Gen, oneof)
 
 -- =========================================================
 -- class FromList cannot be defined in Classes.hs because
@@ -138,7 +137,7 @@ data Sum era c where
   SumList :: Adds c => Term era [c] -> Sum era c
   One :: Term era c -> Sum era c
   ProjOne :: forall x c era. Lens' x c -> Rep era c -> Term era x -> Sum era c
-  Project :: forall x c a era. Sums x c => Rep era c -> Term era (Map a x) -> Sum era c -- TODO uses lenses here
+  ProjMap :: forall x c a era. Adds c => Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
 
 -- ====================================================================
 -- Special patterns for building literal Terms of type Size and Word64
@@ -214,6 +213,25 @@ infixl 0 ^$
 constTarget :: t -> Target era t
 constTarget t = Constr "constTarget" (const t) ^$ (Lit UnitR ())
 
+emptyTarget :: Target era ()
+emptyTarget = (Simple (Lit UnitR ()))
+
+justTarget :: Term era t -> Target era (Maybe t)
+justTarget x = Constr "Just" Just ^$ x
+
+idTarget :: Term era t -> Target era t
+idTarget x = Constr "id" id ^$ x
+
+-- | Usefull when using the Pred 'FromGen'
+--   E.g. (FromGen termMaybeT (maybeTarget ^$ termT))
+maybeTarget :: Target era (t -> Gen (Maybe t))
+maybeTarget = Constr "maybeTarget" genMaybe
+  where
+    genMaybe x = oneof [pure Nothing, pure (Just x)]
+
+listToSetTarget :: Ord x => Term era [x] -> Target era (Set.Set x)
+listToSetTarget x = Constr "FromList" Set.fromList ^$ x
+
 -- ===================================
 
 showL :: (t -> String) -> [Char] -> [t] -> [Char]
@@ -242,7 +260,7 @@ instance Show (Sum era c) where
   show (SumList t) = "sum " ++ show t
   show (One t) = show t
   show (ProjOne _ c t) = seps ["ProjOne", show c, show t]
-  show (Project crep t) = "Project " ++ show crep ++ " " ++ show t
+  show (ProjMap crep _lens t) = "ProjMap " ++ show crep ++ " " ++ show t
 
 instance Show (Pred era) where
   show (MetaSize n t) = "MetaSize " ++ show n ++ " " ++ show t
@@ -405,7 +423,7 @@ varsOfSum ans (SumMap y) = varsOfTerm ans y
 varsOfSum ans (SumList y) = varsOfTerm ans y
 varsOfSum ans (One y) = varsOfTerm ans y
 varsOfSum ans (ProjOne _ _ y) = varsOfTerm ans y
-varsOfSum ans (Project _ x) = varsOfTerm ans x
+varsOfSum ans (ProjMap _ _ x) = varsOfTerm ans x
 
 -- =====================================================
 -- Subtitution of (V era t) inside of (Spec era t)
@@ -540,7 +558,7 @@ substSum sub (SumMap x) = SumMap (substTerm sub x)
 substSum sub (SumList x) = SumList (substTerm sub x)
 substSum sub (One x) = One (substTerm sub x)
 substSum sub (ProjOne l r x) = ProjOne l r (substTerm sub x)
-substSum sub (Project crep x) = Project crep (substTerm sub x)
+substSum sub (ProjMap crep l x) = ProjMap crep l (substTerm sub x)
 
 substTarget :: Subst era -> Target era t -> Target era t
 substTarget sub (Simple e) = Simple (substTerm sub e)
@@ -590,7 +608,7 @@ simplifySum (One (Negate (Lit DeltaCoinR (DeltaCoin n)))) = pure (DeltaCoin (-n)
 simplifySum (ProjOne l _ (Lit _ x)) = pure (x ^. l)
 simplifySum (SumMap (Lit _ m)) = pure (Map.foldl' add zero m)
 simplifySum (SumList (Lit _ m)) = pure (List.foldl' add zero m)
-simplifySum (Project _ (Lit _ m)) = pure (List.foldl' (\ans x -> add ans (getSum x)) zero m)
+simplifySum (ProjMap _ l (Lit _ m)) = pure (List.foldl' (\ans x -> add ans (x ^. l)) zero m)
 simplifySum x = failT ["Can't simplify Sum: " ++ show x ++ ", to a value."]
 
 simplifyTarget :: Target era t -> Typed t
@@ -776,9 +794,9 @@ runSum env (One t) = runTerm env t
 runSum env (ProjOne l _ t) = do
   x <- runTerm env t
   pure (x ^. l)
-runSum env (Project _ t) = Map.foldl' accum zero <$> runTerm env t
+runSum env (ProjMap _ l t) = Map.foldl' accum zero <$> runTerm env t
   where
-    accum ans x = add ans (getSum x)
+    accum ans x = add ans (x ^. l)
 
 makeTest :: Env era -> Pred era -> Typed (String, Bool, Pred era)
 makeTest env c = do
@@ -807,6 +825,10 @@ data Arg era t where
   ArgPs :: !(Field era t s) -> ![Pat era s] -> Arg era t
   Arg :: !(Field era t s) -> Arg era t
 
+-- | Succeds if 'term' is a variable with an embedded (Lens' t2 t1)
+patt :: Rep era t1 -> Term era t2 -> Pat era t1
+patt rep term = Pat rep [arg rep term]
+
 instance Show (Pat era t) where
   show (Pat r xs) = "Pat " ++ show r ++ " " ++ showL show ", " xs
 instance Show (Arg era t) where

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Classes.hs

@@ -44,7 +44,7 @@ import Test.Cardano.Ledger.Constrained.Scripts (genCoreScript)
 import Test.Cardano.Ledger.Constrained.Size (AddsSpec (..), Size (..), genFromIntRange, genFromNonNegIntRange)
 import Test.Cardano.Ledger.Conway.Arbitrary ()
 import Test.Cardano.Ledger.Core.Arbitrary ()
-import Test.Cardano.Ledger.Generic.PrettyCore (pcDCert, pcScript, pcTxOut, pcVal)
+import Test.Cardano.Ledger.Generic.PrettyCore (pcScript, pcTxCert, pcTxOut, pcVal)
 import Test.Cardano.Ledger.Generic.Proof (
   AllegraEra,
   GoodCrypto,
@@ -122,7 +122,12 @@ sumAdds xs = List.foldl' add zero xs
 projAdds :: (Foldable t, Sums a b) => t a -> b
 projAdds xs = List.foldl' accum zero xs
   where
-    accum ans x = add ans (getSum x)
+    accum ans x = add ans (getSum x) -- TODO: Remove after removing Sums constraint over ElemSpec
+
+lensAdds :: (Foldable t, Adds b) => Lens' a b -> t a -> b
+lensAdds l xs = List.foldl' accum zero xs
+  where
+    accum ans x = add ans (x ^. l)
 
 genFromAddsSpec :: [String] -> AddsSpec c -> Gen Int
 genFromAddsSpec _ AddsSpecAny = genFromIntRange SzAny
@@ -344,18 +349,18 @@ instance Count SlotNo where
 -- ============================================================================
 -- Special accomodation for Type Families
 -- ============================================================================
-data DCertF era where
-  DCertF :: Proof era -> DCert era -> DCertF era
+data TxCertF era where
+  TxCertF :: Proof era -> TxCert era -> TxCertF era
 
-unDCertF :: DCertF era -> DCert era
-unDCertF (DCertF _ x) = x
+unTxCertF :: TxCertF era -> TxCert era
+unTxCertF (TxCertF _ x) = x
 
-instance Show (DCertF era) where
-  show (DCertF p x) = show (pcDCert p x)
+instance Show (TxCertF era) where
+  show (TxCertF p x) = show (pcTxCert p x)
 
 {-
-instance Ord (DCertF era) where
-  compare (DCertF p x) (DCertF q y) =
+instance Ord (TxCertF era) where
+  compare (TxCertF p x) (TxCertF q y) =
     case testEql p q of
       Just Refl -> case p of
          Shelley _ -> compare x y
@@ -367,13 +372,13 @@ instance Ord (DCertF era) where
       Nothing -> cmpIndex p q
 -}
 
-instance Eq (DCertF era) where
-  (DCertF (Shelley _) x) == (DCertF (Shelley _) y) = x == y
-  (DCertF (Allegra _) x) == (DCertF (Allegra _) y) = x == y
-  (DCertF (Mary _) x) == (DCertF (Mary _) y) = x == y
-  (DCertF (Alonzo _) x) == (DCertF (Alonzo _) y) = x == y
-  (DCertF (Babbage _) x) == (DCertF (Babbage _) y) = x == y
-  (DCertF (Conway _) x) == (DCertF (Conway _) y) = x == y
+instance Eq (TxCertF era) where
+  (TxCertF (Shelley _) x) == (TxCertF (Shelley _) y) = x == y
+  (TxCertF (Allegra _) x) == (TxCertF (Allegra _) y) = x == y
+  (TxCertF (Mary _) x) == (TxCertF (Mary _) y) = x == y
+  (TxCertF (Alonzo _) x) == (TxCertF (Alonzo _) y) = x == y
+  (TxCertF (Babbage _) x) == (TxCertF (Babbage _) y) = x == y
+  (TxCertF (Conway _) x) == (TxCertF (Conway _) y) = x == y
 
 -- =========
 data TxOutF era where

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Examples.hs

@@ -356,8 +356,8 @@ sumPreds proof =
   , fees :=: (Lit CoinR (Coin 400))
   , deposits :=: (Lit CoinR (Coin 200))
   , SumsTo (Right (Coin 1)) totalAda LTE [One fees, One deposits, One utxoAmt]
-  , SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [Project RationalR poolDistr]
-  , SumsTo (Right (Coin 1)) utxoAmt GTH [Project CoinR (utxo proof)]
+  , SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [ProjMap RationalR individualPoolStakeL poolDistr]
+  , SumsTo (Right (Coin 1)) utxoAmt GTH [ProjMap CoinR outputCoinL (utxo proof)]
   , Sized (AtLeast 1) (utxo proof) -- Any map that is summed, to a nonzero amount, can't be empty.
   , Sized (AtLeast 1) poolDistr
   ]
@@ -512,12 +512,12 @@ test15 =
 
 -- ============================================================
 
-preds16 :: Reflect era => Proof era -> [Pred era]
+preds16 :: Proof era -> [Pred era]
 preds16 _proof =
   [ Sized (ExactSize 6) poolHashUniv
   , Sized (Range 1 3) (Dom poolDistr) -- At least 1 but smaller than the poolHashUniv
   , Dom poolDistr :⊆: poolHashUniv
-  , SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [Project RationalR poolDistr]
+  , SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [ProjMap RationalR individualPoolStakeL poolDistr]
   , Sized (Range 1 4) (Dom foox) -- At least 1 but smaller than the poolHashUniv
   , Dom foox :⊆: poolHashUniv
   , SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [SumMap foox]
@@ -617,15 +617,15 @@ accountstatePreds _p = [] -- Constraints on reserves and treasury appear in dsta
 
 utxostatePreds :: Reflect era => Proof era -> [Pred era]
 utxostatePreds proof =
-  [ SumsTo (Right (Coin 1)) utxoCoin EQL [Project CoinR (utxo proof)]
+  [ SumsTo (Right (Coin 1)) utxoCoin EQL [ProjMap CoinR outputCoinL (utxo proof)]
   , SumsTo (Right (Coin 1)) deposits EQL [SumMap stakeDeposits, SumMap poolDeposits]
   , SumsTo (Right (Coin 1)) totalAda EQL [One utxoCoin, One treasury, One reserves, One fees, One deposits, SumMap rewards]
   , Random fees
   , Random (proposalsT proof)
   , Random (futureProposalsT proof)
   ]
 
-epochstatePreds :: Reflect era => Proof era -> [Pred era]
+epochstatePreds :: Proof era -> [Pred era]
 epochstatePreds proof =
   [ Random markStake
   , Random markDelegs
@@ -642,7 +642,7 @@ epochstatePreds proof =
   , Sized (AtLeast 1) (maxBHSize proof)
   , Sized (AtLeast 1) (maxTxSize proof)
   , -- , Random (maxBBSize proof) -- This will cause underflow on Natural
-    SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [Project RationalR markPoolDistr]
+    SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [ProjMap RationalR individualPoolStakeL markPoolDistr]
   , SumsTo (Right 1) (maxBBSize proof) LTE [One (maxBHSize proof), One (maxTxSize proof)]
   , Component
       (Right (pparams proof))
@@ -651,12 +651,12 @@ epochstatePreds proof =
   where
     pp = PParamsR proof
 
-newepochstatePreds :: Reflect era => Proof era -> [Pred era]
+newepochstatePreds :: Proof era -> [Pred era]
 newepochstatePreds _proof =
-  [ Random epochNo
+  [ Random currentEpoch
   , Sized (ExactSize 8) (Dom prevBlocksMade) -- Both prevBlocksMade and prevBlocksMadeDom will have size 8
   , Sized (ExactSize 8) (Dom currBlocksMade)
-  , SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [Project RationalR poolDistr]
+  , SumsTo (Right (1 % 1000)) (Lit RationalR 1) EQL [ProjMap RationalR individualPoolStakeL poolDistr]
   ]
 
 newepochConstraints :: Reflect era => Proof era -> [Pred era]