Improve the propagation of explanations when a Spec fails. #4739

TimSheard · 2024-11-06T05:15:30Z

Improved the error messages when a Spec fails.
The function explainSpec no longer drops explanations.
Added guardTypeSpec, which catches errors earlier, so there is less noise.
Function symbols like subset_ and member_ print more compactly.

Description

Checklist

Commit sequence broadly makes sense and commits have useful messages
New tests are added if needed and existing tests are updated
All visible changes are prepended to the latest section of a CHANGELOG.md for the affected packages.
New section is never added with the code changes. (See RELEASING.md)
When applicable, versions are updated in .cabal and CHANGELOG.md files according to the
versioning process.
The version bounds in .cabal files for all affected packages are updated.
If you change the bounds in a cabal file, that package itself must have a version increase. (See RELEASING.md)
Code is formatted with fourmolu (use scripts/fourmolize.sh)
Cabal files are formatted (use scripts/cabal-format.sh)
hie.yaml has been updated (use scripts/gen-hie.sh)
Self-reviewed the diff

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

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

MaximilianAlgehed · 2024-11-06T08:36:36Z

libs/constrained-generators/src/Constrained/Univ.hs

+  Subset :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] Bool
+  Disjoint :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] Bool
+  Member :: (Ord a, Show a, Typeable a) => SetFn fn '[a, Set a] Bool
  Singleton :: Ord a => SetFn fn '[a] (Set a)
-  Union :: Ord a => SetFn fn '[Set a, Set a] (Set a)
-  Elem :: Eq a => SetFn fn '[a, [a]] Bool
+  Union :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] (Set a)
+  Elem :: (Eq a, Show a, Typeable a) => SetFn fn '[a, [a]] Bool


What's actually gained by introducing all these extra constraints?

Without them I cannot introduce the construtor form of the patterns.

I'm not sure I get why that's the case? Also, where are the patterns used?

So the patterns are used in the Pretty instance for Terms.
As we currently use the patterns to match, and not construct, we can get rid of some of the constraints.

libs/constrained-generators/src/Constrained/Base.hs

The function explainSpec no longer drops explanations on TypeSpec Added guardTypeSpec, which catches errors earlier, so there is less noise. function symbols like subset_ and member_ print a elided version of their set arguments when they are large literals. Improves readabilty as irrelevant information no longer overwhelms the user. Add the constructor ExplainSpec to Specification Assert now has type Assert :: Term fn Bool -> Pred fn

MaximilianAlgehed · 2024-11-13T14:10:05Z

libs/constrained-generators/src/Constrained/Base.hs

-shrinkFromPreds :: HasSpec fn a => Pred fn -> Var a -> a -> [a]
-shrinkFromPreds p
-  | Result _ plan <- prepareLinearization p = \x a -> listFromGE $ do
-      -- NOTE: we do this to e.g. guard against bad construction functions in Exists
-      xaGood <- checkPred (singletonEnv x a) p
-      unless xaGood $
-        fatalError1 "Trying to shrink a bad value, don't do that!"
-      -- Get an `env` for the original value
-      initialEnv <- envFromPred (singletonEnv x a) p
-      return
-        [ a'
-        | -- Shrink the initialEnv
-        env' <- shrinkEnvFromPlan initialEnv plan
-        , -- Get the value of the constrained variable `x` in the shrunk env
-        Just a' <- [lookupEnv env' x]
-        , -- NOTE: this is necessary because it's possible that changing
-        -- a particular value in the env during shrinking might not result
-        -- in the value of `x` changing and there is no better way to know than
-        -- to do this.
-        a' /= a
-        ]
-  | otherwise = error "Bad pred"
-
-- Start with a valid Env for the plan and try to shrink it
-shrinkEnvFromPlan :: Env -> SolverPlan fn -> [Env]
-shrinkEnvFromPlan initialEnv SolverPlan {..} = go mempty solverPlan
-  where
-    go _ [] = [] -- In this case we decided to keep every variable the same so nothing to return
-    go env ((substStage env -> SolverStage {..}) : plan) = do
-      Just a <- [lookupEnv initialEnv stageVar]
-      -- Two cases:
-      --  - either we shrink this value and try to fixup every value later on in the plan or
-      [ env' <> fixedEnv
-        | a' <- shrinkWithSpec stageSpec a
-        , let env' = extendEnv stageVar a' env
-        , Just fixedEnv <- [fixupPlan env' plan]
-        ]
-        --  - we keep this value the way it is and try to shrink some later value
-        ++ go (extendEnv stageVar a env) plan
-
-    -- Fix the rest of the plan given an environment `env` for the plan so far
-    fixupPlan env [] = pure env
-    fixupPlan env ((substStage env -> SolverStage {..}) : plan) =
-      case lookupEnv initialEnv stageVar >>= fixupWithSpec stageSpec of
-        Nothing -> Nothing
-        Just a -> fixupPlan (extendEnv stageVar a env) plan
-
-- Try to fix a value w.r.t a specification
-fixupWithSpec :: forall fn a. HasSpec fn a => Specification fn a -> a -> Maybe a
-fixupWithSpec spec a
-  | a `conformsToSpec` spec = Just a
-  | otherwise = case spec of
-      MemberSpec (a :| _) -> Just a
-      _ -> listToMaybe $ filter (`conformsToSpec` spec) (shrinkWithSpec @fn TrueSpec a)
-
-- Construct an environment for all variables that show up on the top level
-- (i.e. ones bound in `let` and `exists`) from an environment for all the free
-- variables in the pred. The environment you get out of this function is
-- _bigger_ than the environment you put in. From
-- ```
-- let y = x + 1 in let z = y + 1 in foo x y z
-- ```
-- and an environment with `{x -> 1}` you would get `{x -> 1, y -> 2, z -> 3}`
-- out.
-envFromPred :: Env -> Pred fn -> GE Env
-envFromPred env p = case p of
-  -- NOTE: these don't bind anything
-  Assert {} -> pure env
-  DependsOn {} -> pure env
-  Monitor {} -> pure env
-  TruePred {} -> pure env
-  FalsePred {} -> pure env
-  GenHint {} -> pure env
-  -- NOTE: this is ok because the variables either come from an `Exists`, a `Let`, or from
-  -- the top level
-  Reifies {} -> pure env
-  -- NOTE: variables in here shouldn't escape to the top level
-  ForAll {} -> pure env
-  Case {} -> pure env
-  -- These can introduce binders that show up in the plan
-  When _ p -> envFromPred env p
-  Subst x a p -> envFromPred env (substitutePred x a p)
-  Let t (x :-> p) -> do
-    v <- runTerm env t
-    envFromPred (extendEnv x v env) p
-  Explain _ p -> envFromPred env p
-  Exists c (x :-> p) -> do
-    v <- c (errorGE . explain1 "envFromPred: Exists" . runTerm env)
-    envFromPred (extendEnv x v env) p
-  Block [] -> pure env
-  Block (p : ps) -> do
-    env' <- envFromPred env p
-    envFromPred env' (Block ps)


Why is this being removed?

Maybe a merge conflict that I messed up?

MaximilianAlgehed · 2024-11-13T14:11:11Z

libs/constrained-generators/src/Constrained/GenT.hs

+-- | Temporarily extend the stack while executing 'm', and revert to the old stack if successful
+push :: forall m a. MonadGenError m => [String] -> GenT GE a -> GenT m a
+push [] m = dropGen m
+push (x : xs) m =
+  case explain (x NE.:| xs) m of
+    GenT f -> (GenT g)
+      where
+        g :: GenMode -> Gen (m a)
+        g mode = do
+          result <- f mode
+          case result of
+            Result (_ : ys) a -> pure $ runGE (Result ys a)
+            other -> pure $ runGE other
+
+pushGE :: forall a. [String] -> GE a -> GE a
+pushGE [] x = x
+pushGE (x : xs) m = do
+  case explain (x NE.:| xs) m of
+    Result (_ : ys) a -> Result ys a
+    other -> other


I don't get at all why this is necessary. This is what explain already does??

explain, adds an explanation, and it is never removed. This code adds a explanation for one computation, and then if it succeeds, it is rolled back to the state before.

Right, that's a bug in explain. It shouldn't do that for Result!

Soupstraw · 2024-11-13T16:56:43Z

libs/constrained-generators/test/Constrained/Test.hs

@@ -4,7 +4,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE ImportQualifiedPost #-}
+-- {-# LANGUAGE ImportQualifiedPost #-}


Suggested change

-- {-# LANGUAGE ImportQualifiedPost #-}

TimSheard requested review from MaximilianAlgehed, Soupstraw and lehins November 6, 2024 05:15

MaximilianAlgehed reviewed Nov 6, 2024

View reviewed changes

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/WitnessUniverse.hs Outdated Show resolved Hide resolved

MaximilianAlgehed reviewed Nov 6, 2024

View reviewed changes

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs Outdated Show resolved Hide resolved

MaximilianAlgehed requested changes Nov 6, 2024

View reviewed changes

Soupstraw reviewed Nov 6, 2024

View reviewed changes

libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved

TimSheard force-pushed the ts-better-explanations branch from f4a840b to aa9bbf2 Compare November 6, 2024 14:01

TimSheard marked this pull request as ready for review November 6, 2024 15:22

TimSheard requested a review from a team as a code owner November 6, 2024 15:22

TimSheard force-pushed the ts-better-explanations branch 4 times, most recently from 9ba2f7c to 19c01e0 Compare November 12, 2024 16:58

TimSheard force-pushed the ts-better-explanations branch from 19c01e0 to 9074791 Compare November 12, 2024 17:53

MaximilianAlgehed requested changes Nov 13, 2024

View reviewed changes

MaximilianAlgehed reviewed Nov 13, 2024

View reviewed changes

Soupstraw reviewed Nov 13, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve the propagation of explanations when a Spec fails. #4739

Improve the propagation of explanations when a Spec fails. #4739

TimSheard commented Nov 6, 2024 •

edited

Loading

MaximilianAlgehed Nov 6, 2024

TimSheard Nov 6, 2024

MaximilianAlgehed Nov 13, 2024

TimSheard Nov 13, 2024

MaximilianAlgehed Nov 13, 2024

TimSheard Nov 13, 2024

MaximilianAlgehed Nov 13, 2024

TimSheard Nov 13, 2024

MaximilianAlgehed Nov 13, 2024

Soupstraw Nov 13, 2024

Improve the propagation of explanations when a Spec fails. #4739

Are you sure you want to change the base?

Improve the propagation of explanations when a Spec fails. #4739

Conversation

TimSheard commented Nov 6, 2024 • edited Loading

Description

Checklist

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

TimSheard commented Nov 6, 2024 •

edited

Loading