Warn when a claim is proven without taking any steps

kore/src/Kore/Exec.hs

@@ -102,6 +102,7 @@ import Kore.Log.InfoExecDepth
 import Kore.Log.KoreLogOptions
     ( KoreLogOptions (..)
     )
+import Kore.Log.WarnTrivialClaim
 import qualified Kore.ModelChecker.Bounded as Bounded
 import qualified Kore.Repl as Repl
 import qualified Kore.Repl.Data as Repl.Data
@@ -697,12 +698,13 @@ initializeProver definitionModule specModule maybeTrustedModule = do
         changedSpecClaims =
             expandClaim tools <$> Goal.extractClaims specModule
         simplifyToList
-            :: SimplifyRuleLHS rule
-            => rule
-            -> simplifier [rule]
+            :: ReachabilityRule
+            -> simplifier [ReachabilityRule]
         simplifyToList rule = do
             simplified <- simplifyRuleLhs rule
-            return (MultiAnd.extractPatterns simplified)
+            let result = MultiAnd.extractPatterns simplified
+            when (null result) $ warnTrivialClaimRemoved rule
+            return result
 
         trustedClaims :: [ReachabilityRule]
         trustedClaims =

kore/src/Kore/Log/Registry.hs

@@ -104,6 +104,9 @@ import Kore.Log.WarnStuckProofState
 import Kore.Log.WarnSymbolSMTRepresentation
     ( WarnSymbolSMTRepresentation
     )
+import Kore.Log.WarnTrivialClaim
+    ( WarnTrivialClaim
+    )
 import Log
     ( Entry (..)
     , LogMessage
@@ -152,6 +155,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @WarnSymbolSMTRepresentation
     , mk $ Proxy @WarnStuckProofState
     , mk $ Proxy @WarnIfLowProductivity
+    , mk $ Proxy @WarnTrivialClaim
     , mk $ Proxy @DebugEvaluateCondition
     , mk $ Proxy @ErrorException
     , mk $ Proxy @ErrorRewriteLoop

kore/src/Kore/Log/WarnTrivialClaim.hs

@@ -0,0 +1,64 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.WarnTrivialClaim
+    ( WarnTrivialClaim (..)
+    , warnProvenClaimZeroDepth
+    , warnTrivialClaimRemoved
+    ) where
+
+import Prelude.Kore
+
+import Kore.Attribute.SourceLocation
+import Kore.Log.InfoProofDepth
+import Kore.Step.RulePattern
+import Log
+import Pretty
+    ( Pretty
+    )
+import qualified Pretty
+
+data WarnTrivialClaim
+    = WarnProvenClaimZeroDepth ReachabilityRule
+    -- ^ Warning when a claim is proved without rewriting.
+    | WarnTrivialClaimRemoved ReachabilityRule
+    -- ^ Warning when a claim is proved during initialization.
+    deriving Show
+
+instance Pretty WarnTrivialClaim where
+    pretty (WarnProvenClaimZeroDepth rule) =
+        Pretty.hsep
+            [ "Claim proven without rewriting at:"
+            , Pretty.pretty (from rule :: SourceLocation)
+            ]
+    pretty (WarnTrivialClaimRemoved rule) =
+        Pretty.vsep
+            [ Pretty.hsep
+                [ "Claim proven during initialization:"
+                , Pretty.pretty (from rule :: SourceLocation)
+                ]
+            , "The left-hand side of the claim may be undefined."
+            ]
+
+
+instance Entry WarnTrivialClaim where
+    entrySeverity _ = Warning
+    helpDoc _ = "warn when a claim is proven without taking any steps"
+
+warnProvenClaimZeroDepth
+    :: MonadLog log
+    => ProofDepth
+    -> ReachabilityRule
+    -> log ()
+warnProvenClaimZeroDepth (ProofDepth depth) rule =
+    when (depth == 0) $ logEntry (WarnProvenClaimZeroDepth rule)
+
+warnTrivialClaimRemoved
+    :: MonadLog log
+    => ReachabilityRule
+    -> log ()
+warnTrivialClaimRemoved rule =
+    logEntry (WarnTrivialClaimRemoved rule)

kore/src/Kore/Strategies/Verification.hs

@@ -76,6 +76,7 @@ import qualified Kore.Internal.Pattern as Pattern
 import Kore.Log.DebugProofState
 import Kore.Log.InfoExecBreadth
 import Kore.Log.InfoProofDepth
+import Kore.Log.WarnTrivialClaim
 import Kore.Step.RulePattern
     ( leftPattern
     , toRulePattern
@@ -281,6 +282,7 @@ verifyClaim
             & handle handleLimitExceeded
     let maxProofDepth = sconcat (ProofDepth 0 :| proofDepths)
     infoProvenDepth maxProofDepth
+    warnProvenClaimZeroDepth maxProofDepth goal
   where
     discardStrategy = snd