diff --git a/bench/cardano-recon-framework/CHANGELOG.md b/bench/cardano-recon-framework/CHANGELOG.md index 9d27d8aa8fc..4fc549f6e93 100644 --- a/bench/cardano-recon-framework/CHANGELOG.md +++ b/bench/cardano-recon-framework/CHANGELOG.md @@ -1,5 +1,15 @@ # Revision history for cardano-trace-ltl +## 1.2.0 -- May 2026 + +* Add `ContinuousFormula` — the temporal-operator-free fragment of `Formula`, with `retract` for + converting a `Formula` and `eval` for deciding it against a single event. +* Add `cardano-recon-grep` executable — filters a JSON array of `TraceMessage`s by a list of + continuous formulas, emitting only the messages that satisfy all of them. +* Add `--grep` flag to `cardano-recon` — on a negative formula outcome prints only the JSON array + of relevant events to stdout (bypassing trace-dispatcher); prints nothing on a positive outcome. +* Replace the raw context printout with a `ContextDump` trace message at `Debug` severity. + ## 1.1.1 -- April 2026 * Support atoms that refer to property keys at arbitrary depth * Replace the `crash-on-missing-key` build flag with a runtime CLI option `--on-missing-key ` (default: `bottom`) diff --git a/bench/cardano-recon-framework/README.md b/bench/cardano-recon-framework/README.md index 0705ba7772c..75661c27010 100644 --- a/bench/cardano-recon-framework/README.md +++ b/bench/cardano-recon-framework/README.md @@ -1,6 +1,8 @@ # Cardano Re(altime) Con(formance) Framework -## What it does +## Applications + +### `cardano-recon` — LTL conformance checker The application CLI takes as input: - A yaml list of strings, where each string is a parseable Linear Temporal Logic formula. @@ -14,14 +16,18 @@ The application CLI takes as input: The application traverses the events from the given log files and checks if each given formula is satisfied by them. If negative, reports as such and lists the events that have been relevant to the formula. -## CLI Syntax +Pass `--grep` for machine-readable output: on a negative outcome only the JSON array of relevant events is written +to stdout (bypassing trace-dispatcher), and nothing is printed on a positive outcome. This makes it straightforward +to pipe results directly into `cardano-recon-grep`. + +#### CLI Syntax ``` Usage: cardano-recon FILE --mode --duration INT FILES [--retention INT] [--trace-dispatcher-cfg FILE] [--context FILE] [--dump-metrics BOOL] [--seek-to-end BOOL] [--timeunit ] - [--on-missing-key ] + [--on-missing-key ] [--grep] Check formula satisfiability against a log of trace messages @@ -38,6 +44,44 @@ Available options: (default: True) --timeunit timeunit (default: second) + --on-missing-key + behaviour when a formula atom references a missing + event property key (default: bottom) + --grep on formula violation print only the JSON array of + relevant events; print nothing on satisfaction + -h,--help Show this help text +``` + +### `cardano-recon-grep` — Global Realisation Print + +A stateless utility that filters a JSON array of trace messages by interpreting a list of +_continuous_ (temporal-operator-free) formulas against each message individually. +Only messages that satisfy **all** given formulas are written to stdout as a pretty-printed +JSON array. + +Inputs: + - A YAML list of continuous formula strings (same syntax as `cardano-recon`, but temporal + operators such as `□`, `◇`, `○`, and `|` are not permitted). + For further details about the formula language, consult the [language overview](docs/formula-languages.txt). + - A JSON array of `TraceMessage` objects, read from a file (`--traces FILE`) or from stdin + if `--traces` is omitted (e.g. piped from `cardano-recon` on a negative formula outcome). + - An optional context variables YAML file for variable substitution in formulas. + - An `--on-missing-key` policy (default: `bottom`) controlling behaviour when a formula + references a property absent from a message. + +#### CLI Syntax + +``` +Usage: cardano-recon-grep --formulas FILE [--traces FILE] + [--context FILE] + [--on-missing-key ] + + Print log events that realise all given continuous formulas (Global Realisation Print) + +Available options: + --formulas FILE YAML file with a list of ContinuousFormulas + --traces FILE JSON array of TraceMessages to filter (default: stdin) + --context FILE context variables YAML file --on-missing-key behaviour when a formula atom references a missing event property key (default: bottom) diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon.hs b/bench/cardano-recon-framework/app/Cardano/ReCon.hs index 55e4355e41e..cf0df8e3bcd 100644 --- a/bench/cardano-recon-framework/app/Cardano/ReCon.hs +++ b/bench/cardano-recon-framework/app/Cardano/ReCon.hs @@ -34,6 +34,7 @@ import qualified Data.Map as Map import Data.Maybe (fromMaybe, listToMaybe) import Data.Text (Text) import qualified Data.Text as Text +import qualified Data.Text.IO as TIO import Data.Traversable (for) import GHC.IO.Encoding (setLocaleEncoding, utf8) import Network.HostName (HostName) @@ -45,18 +46,26 @@ import qualified System.Metrics as EKG import Streaming -check :: OnMissingKey -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO () -check omk idx {- Formula index -} tr phi events = +check :: OnMissingKey -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO () +check omk greppable idx {- Formula index -} tr phi events = let result = satisfies omk phi events in - traceWith tr $ formulaOutcome phi result idx - -checkS' :: OnMissingKey -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> Stream (Of TemporalEvent) IO () -> IO () -checkS' omk enableProgressDumps idx {- Formula index -} tr phi events = do + if greppable + then case result of + Satisfied -> pure () + Unsatisfied rel -> TIO.putStrLn (App.prettyRelevanceArray rel) + else traceWith tr $ formulaOutcome phi result idx + +checkS' :: OnMissingKey -> Bool -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> Stream (Of TemporalEvent) IO () -> IO () +checkS' omk greppable enableProgressDumps idx {- Formula index -} tr phi events = do let initial = SatisfyMetrics 0 phi 0 metrics <- newIORef initial withAsync (when enableProgressDumps $ runDisplayProgressDump initial metrics) $ \counterDisplayThread -> do r <- satisfiesS omk phi events metrics - traceWith tr $ formulaOutcome phi r idx + if greppable + then case r of + Satisfied -> pure () + Unsatisfied rel -> TIO.putStrLn (App.prettyRelevanceArray rel) + else traceWith tr $ formulaOutcome phi r idx cancel counterDisplayThread where runDisplayProgressDump :: SatisfyMetrics TemporalEvent Text -> IORef (SatisfyMetrics TemporalEvent Text) -> IO () @@ -69,6 +78,7 @@ checkS' omk enableProgressDumps idx {- Formula index -} tr phi events = do runDisplayProgressDump next counter checkOnline :: OnMissingKey + -> Bool -> Bool -> Trace IO App.TraceMessage -> TemporalEventDurationMicrosec @@ -78,23 +88,24 @@ checkOnline :: OnMissingKey -> [FilePath] -> [Formula TemporalEvent Text] -> IO () -checkOnline omk enableProgressDumps tr eventDuration retentionMs failureMode ingestMode files phis = do +checkOnline omk greppable enableProgressDumps tr eventDuration retentionMs failureMode ingestMode files phis = do ing <- mkIngestor (fromIntegral retentionMs) for_ files (ingestFileThreaded ing failureMode ingestMode) forConcurrently_ (zip [0..] phis) $ \(idx, phi) -> mkIngestorReader ing >>= \reader -> forever $ do traceWith tr $ FormulaStartCheck phi idx - checkS' omk enableProgressDumps idx tr phi (readS reader eventDuration) + checkS' omk greppable enableProgressDumps idx tr phi (readS reader eventDuration) checkOffline :: OnMissingKey + -> Bool -> Trace IO App.TraceMessage -> TemporalEventDurationMicrosec -> FilePath -> [Formula TemporalEvent Text] -> IO () -checkOffline omk tr eventDuration file phis = do +checkOffline omk greppable tr eventDuration file phis = do events <- read file eventDuration forConcurrently_ (zip [0..] phis) $ \(idx, phi) -> - check omk idx tr phi events + check omk greppable idx tr phi events threadDelay 200_000 -- Give the tracer a grace period to output the logs to whatever backend setupTraceDispatcher :: Maybe FilePath -> IO (Trace IO App.TraceMessage) @@ -139,8 +150,6 @@ main = do setLocaleEncoding utf8 options <- execParser opts ctx <- Map.toList . fromMaybe Map.empty <$> for options.context (readPropValues >=> dieOnYamlException) - putStrLn "Context:" - print ctx formulas <- readFormulas options.formulas (Context { interpDomain = ctx, varKinds = Map.empty }) Parser.name >>= dieOnYamlException for_ (fmap (\phi -> (phi, checkFormula mempty phi)) formulas) $ \case (phi, e : es) -> die $ @@ -152,15 +161,17 @@ main = do (_, []) -> pure () let formulas' = fmap (interpTimeunit (\u -> timeunitToMicrosecond options.timeunit u `div` fromIntegral options.duration)) formulas tr <- setupTraceDispatcher options.traceDispatcherCfg + traceWith tr $ ContextDump (map (second showT) ctx) case options.mode of Offline -> do file <- case options.traces of [x] -> pure x _ -> die "Only exactly one trace file is supported in 'offline' mode" - checkOffline options.onMissingKey tr options.duration file formulas' + checkOffline options.onMissingKey options.greppable tr options.duration file formulas' Online -> do checkOnline options.onMissingKey + options.greppable options.enableProgressDumps tr options.duration diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs index de1f58fded2..8917d1c5479 100644 --- a/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs +++ b/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs @@ -134,6 +134,11 @@ parseOnMissingKey = option readOnMissingKey $ <> value BottomOnMissingKey <> help "behaviour when a formula atom references a missing event property key" +parseGreppable :: Parser Bool +parseGreppable = switch $ + long "grep" + <> help "on formula violation print only the JSON array of relevant events; print nothing on satisfaction" + data CliOptions = CliOptions { formulas :: FilePath , mode :: Mode @@ -146,6 +151,7 @@ data CliOptions = CliOptions , enableSeekToEnd :: Bool , timeunit :: Timeunit , onMissingKey :: OnMissingKey + , greppable :: Bool } parseCliOptions :: Parser CliOptions @@ -161,6 +167,7 @@ parseCliOptions = CliOptions <*> parseSeekToEnd <*> parseTimeunit <*> parseOnMissingKey + <*> parseGreppable opts :: ParserInfo CliOptions opts = info (parseCliOptions <**> helper) diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs deleted file mode 100644 index 622051c7eca..00000000000 --- a/bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs +++ /dev/null @@ -1,16 +0,0 @@ -module Cardano.ReCon.Common where - -import Data.Aeson (Object, Value (..)) -import Data.Aeson.Key (toText) -import qualified Data.Aeson.KeyMap as KeyMap -import qualified Data.Map as Map -import Data.Map.Strict (Map) -import Data.Text (Text) - --- | Extract scalar properties from a JSON object as Aeson Values, for display. -extractJsonProps :: Object -> Map Text Value -extractJsonProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap - where - f v@(Number _) = Just v - f v@(String _) = Just v - f _ = Nothing diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs index 700e24a4be0..0fa2732843c 100644 --- a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs +++ b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs @@ -5,17 +5,15 @@ module Cardano.ReCon.TraceMessage where import Cardano.Logging import Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..)) import qualified Cardano.Logging.Types.TraceMessage as Envelop -import Cardano.ReCon.Common (extractJsonProps) import Cardano.ReCon.LTL.Formula (Formula, Relevance) import qualified Cardano.ReCon.LTL.Formula.Prec as Prec import Cardano.ReCon.LTL.Formula.Pretty (prettyFormula) import Cardano.ReCon.LTL.Satisfy (SatisfactionResult (..)) import Cardano.ReCon.Trace.Feed (TemporalEvent (..)) -import Data.Aeson (Value (..), (.=)) +import Data.Aeson ((.=)) import Data.Aeson.Encode.Pretty import Data.List (find) -import qualified Data.Map as Map import qualified Data.Set as Set import Data.Text (Text) import qualified Data.Text as Text @@ -44,13 +42,14 @@ data TraceMessage = FormulaStartCheck { | FormulaNegativeOutcome { formula :: Formula TemporalEvent Text, relevance :: Relevance TemporalEvent Text, - index :: Word + index :: Word } + | ContextDump { context :: [(Text, Text)] } -- | Smart constructor. formulaOutcome :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Word -> TraceMessage -formulaOutcome formula Satisfied idx = FormulaPositiveOutcome formula idx -formulaOutcome formula (Unsatisfied rel) idx = FormulaNegativeOutcome formula rel idx +formulaOutcome formula Satisfied idx = FormulaPositiveOutcome { formula, index = idx } +formulaOutcome formula (Unsatisfied rel) idx = FormulaNegativeOutcome { formula, relevance = rel, index = idx } green :: Text -> Text green text = "\x001b[32m" <> text <> "\x001b[0m" @@ -59,51 +58,49 @@ red :: Text -> Text red text = "\x001b[31m" <> text <> "\x001b[0m" prettyTraceMessage :: Envelop.TraceMessage -> Text -prettyTraceMessage Envelop.TraceMessage{..} = - toStrict $ toLazyText $ encodePrettyToTextBuilder $ - Map.insert "at" (String (showT tmsgAt)) $ - Map.insert "namespace" (String tmsgNS) $ - Map.insert "host" (String tmsgHost) $ - Map.insert "thread" (String tmsgThread) $ - extractJsonProps tmsgData +prettyTraceMessage = toStrict . toLazyText . encodePrettyToTextBuilder prettyTemporalEvent :: TemporalEvent -> Text -> Text prettyTemporalEvent (TemporalEvent _ msgs) ns = maybe ("< ns <> ">>") prettyTraceMessage (find (\ x -> x.tmsgNS == ns) msgs) +prettyRelevanceArray :: Relevance TemporalEvent Text -> Text +prettyRelevanceArray rel = + Text.unlines $ "[" : fmap (uncurry prettyTemporalEvent) (Set.toList rel) ++ ["]"] + prettySatisfactionResult :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Text prettySatisfactionResult initial Satisfied = prettyFormula initial Prec.Universe <> " " <> green "(✔)" prettySatisfactionResult initial (Unsatisfied rel) = prettyFormula initial Prec.Universe <> red " (✗)" <> "\n" - <> Text.intercalate - "\n----------------------------------------------\n" - (fmap (uncurry prettyTemporalEvent) (Set.toList rel)) + <> prettyRelevanceArray rel instance LogFormatting TraceMessage where forMachine _ FormulaStartCheck{..} = mconcat [ - "formula" .= String (prettyFormula formula Prec.Universe), + "formula" .= prettyFormula formula Prec.Universe, "index" .= index ] forMachine _ FormulaProgressDump{..} = mconcat [ - "events_per_second" .= Number (fromIntegral eventsPerSecond), - "catch_up_ratio" .= Number (realToFrac catchupRatio), + "eventsPerSecond" .= (fromIntegral eventsPerSecond :: Int), + "catchUpRatio" .= (realToFrac catchupRatio :: Double), "index" .= index ] forMachine _ FormulaPositiveOutcome{..} = mconcat [ - "formula" .= String (prettyFormula formula Prec.Universe), + "formula" .= prettyFormula formula Prec.Universe, "index" .= index ] forMachine _ FormulaNegativeOutcome{..} = mconcat [ - "formula" .= String (prettyFormula formula Prec.Universe) + "formula" .= prettyFormula formula Prec.Universe , - "relevance" .= String (showT relevance) + "relevance" .= showT relevance , "index" .= index ] + forMachine _ ContextDump{..} = mconcat + [ "context" .= context ] forHuman FormulaStartCheck{..} = "Starting satisfiability check on formula #" <> showT index <> ": " <> prettyFormula formula Prec.Universe @@ -119,16 +116,21 @@ instance LogFormatting TraceMessage where prettySatisfactionResult formula Satisfied forHuman FormulaNegativeOutcome{..} = prettySatisfactionResult formula (Unsatisfied relevance) + forHuman ContextDump{..} = + Text.unlines $ "Context:" : map (\(k, v) -> " " <> k <> " = " <> v) context asMetrics FormulaStartCheck{} = [] asMetrics (FormulaProgressDump {catchupRatio, index}) = [DoubleM ("catchup_ratio_" <> showT index) catchupRatio] asMetrics FormulaPositiveOutcome{} = [] asMetrics FormulaNegativeOutcome{} = [] + asMetrics ContextDump{} = [] instance MetaTrace TraceMessage where allNamespaces = [ + Namespace [] ["ContextDump"] + , Namespace [] ["FormulaStartCheck"] , Namespace [] ["FormulaProgressDump"] @@ -136,11 +138,13 @@ instance MetaTrace TraceMessage where Namespace [] ["FormulaOutcome"] ] + namespaceFor ContextDump{} = Namespace [] ["ContextDump"] namespaceFor FormulaStartCheck{} = Namespace [] ["FormulaStartCheck"] namespaceFor FormulaProgressDump{} = Namespace [] ["FormulaProgressDump"] namespaceFor FormulaPositiveOutcome{} = Namespace [] ["FormulaPositiveOutcome"] namespaceFor FormulaNegativeOutcome{} = Namespace [] ["FormulaNegativeOutcome"] + severityFor (Namespace [] ["ContextDump"]) _ = Just Debug severityFor (Namespace [] ["FormulaStartCheck"]) _ = Just Info severityFor (Namespace [] ["FormulaProgressDump"]) _ = Just Debug severityFor (Namespace [] ["FormulaPositiveOutcome"]) _ = Just Info @@ -149,6 +153,8 @@ instance MetaTrace TraceMessage where detailsFor _ _ = Just DNormal + documentFor (Namespace [] ["ContextDump"]) = + Just "Dump of the context variables supplied to the formula parser." documentFor (Namespace [] ["FormulaStartCheck"]) = Just "Formula satisfiability check has started." documentFor (Namespace [] ["FormulaProgressDump"]) = diff --git a/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs new file mode 100644 index 00000000000..78a33cecd4a --- /dev/null +++ b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs @@ -0,0 +1,109 @@ +module Main(main) where + +import Cardano.Logging.Types.TraceMessage (TraceMessage (..)) +import qualified Cardano.ReCon.LTL.ContinuousFormula as CF +import Cardano.ReCon.LTL.Formula (OnMissingKey (..)) +import Cardano.ReCon.LTL.Formula.Parser (Context (..)) +import qualified Cardano.ReCon.LTL.Formula.Parser as Parser +import Cardano.ReCon.LTL.Formula.Yaml (YamlReadError, readFormulas, readPropValues) +import Cardano.ReCon.Trace.Event () +import Cardano.ReCon.Trace.Feed (TemporalEvent (..)) + +import Control.Arrow ((>>>)) +import Control.Monad ((>=>)) +import Control.Monad.Reader (runReader) +import Data.Aeson (decodeStrict') +import Data.Aeson.Encode.Pretty (encodePrettyToTextBuilder) +import qualified Data.ByteString as BS +import qualified Data.ByteString.Char8 as BChar8 +import qualified Data.Text.IO as TIO +import Data.Text.Lazy (toStrict) +import Data.Text.Lazy.Builder (toLazyText) +import Data.Char (toLower) +import qualified Data.Map.Strict as Map +import Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds) +import Data.Text (Text) +import qualified Data.Text as Text +import Data.Traversable (for) +import GHC.IO.Encoding (setLocaleEncoding, utf8) +import Options.Applicative +import System.Exit (die) + +data CliOptions = CliOptions + { formulas :: FilePath + , traces :: Maybe FilePath + , context :: Maybe FilePath + , onMissingKey :: OnMissingKey + } + +readOnMissingKey :: ReadM OnMissingKey +readOnMissingKey = eitherReader $ fmap toLower >>> \case + "crash" -> Right CrashOnMissingKey + "bottom" -> Right BottomOnMissingKey + _ -> Left "Expected either of: 'crash' or 'bottom'" + +parseCliOptions :: Parser CliOptions +parseCliOptions = CliOptions + <$> option str + ( long "formulas" + <> metavar "FILE" + <> help "YAML file with a list of ContinuousFormulas") + <*> option (optional str) + ( long "traces" + <> value Nothing + <> metavar "FILE" + <> help "JSON array of TraceMessages to filter (default: stdin)") + <*> option (optional str) + ( long "context" + <> value Nothing + <> metavar "FILE" + <> help "context variables YAML file") + <*> option readOnMissingKey + ( long "on-missing-key" + <> metavar "" + <> showDefaultWith (\case BottomOnMissingKey -> "bottom"; CrashOnMissingKey -> "crash") + <> value BottomOnMissingKey + <> help "behaviour when a formula atom references a missing event property key") + +opts :: ParserInfo CliOptions +opts = info (parseCliOptions <**> helper) + (fullDesc <> progDesc "Print log events that realise all given continuous formulas (Global Realisation Print)") + +msgToEvent :: TraceMessage -> TemporalEvent +msgToEvent msg = TemporalEvent { beg = round (utcTimeToPOSIXSeconds msg.tmsgAt * 1_000_000), messages = [msg] } + +prettyMsg :: TraceMessage -> Text +prettyMsg = toStrict . toLazyText . encodePrettyToTextBuilder + +printArray :: [TraceMessage] -> IO () +printArray [] = TIO.putStrLn "[]" +printArray msgs = + TIO.putStr $ Text.unlines $ "[" : map prettyMsg msgs ++ ["]"] + +main :: IO () +main = do + setLocaleEncoding utf8 + options <- execParser opts + ctx <- maybe [] Map.toList <$> + for options.context (readPropValues >=> dieOnYamlError) + rawFormulas <- readFormulas options.formulas + (Context { interpDomain = ctx, varKinds = Map.empty }) + Parser.name + >>= dieOnYamlError + cformulas <- mapM retractOrDie rawFormulas + content <- maybe BS.getContents BChar8.readFile options.traces + msgs <- maybe (die "Failed to parse input as a JSON array of TraceMessages") pure + (decodeStrict' content :: Maybe [TraceMessage]) + let matching = [ msg | msg <- msgs + , let event = msgToEvent msg + , all (\phi -> runReader (CF.eval phi event) options.onMissingKey) cformulas ] + printArray matching + where + dieOnYamlError :: Either YamlReadError a -> IO a + dieOnYamlError (Left err) = die (Text.unpack err) + dieOnYamlError (Right ok) = pure ok + + retractOrDie phi = case CF.retract phi of + Just cf -> pure cf + Nothing -> die + "One of the formulas contains a temporal connective; filter mode only accepts continuous formulas" diff --git a/bench/cardano-recon-framework/cardano-recon-framework.cabal b/bench/cardano-recon-framework/cardano-recon-framework.cabal index be8a47c79f0..247a49efdf1 100644 --- a/bench/cardano-recon-framework/cardano-recon-framework.cabal +++ b/bench/cardano-recon-framework/cardano-recon-framework.cabal @@ -4,7 +4,7 @@ description: Cardano Re(altime) Con(formance) Framework based on Linear T category: Cardano Testing copyright: 2026 Intersect. -version: 1.1.1 +version: 1.2.0 license: Apache-2.0 license-files: LICENSE NOTICE @@ -72,6 +72,7 @@ library , Cardano.ReCon.Common.Parser , Cardano.ReCon.LTL.Check + , Cardano.ReCon.LTL.ContinuousFormula , Cardano.ReCon.LTL.Formula , Cardano.ReCon.LTL.Formula.Parser , Cardano.ReCon.LTL.Formula.Prec @@ -98,7 +99,6 @@ library , Cardano.ReCon.LTL.Internal.Subst , Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula , Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree - , Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree , Cardano.ReCon.Presburger.Internal.CooperQE , Cardano.ReCon.Presburger.Internal.IR.AffineDNF , Cardano.ReCon.Presburger.Internal.IR.CompNF @@ -143,7 +143,6 @@ executable cardano-recon other-modules: Cardano.ReCon.TraceMessage , Cardano.ReCon.Cli - , Cardano.ReCon.Common other-extensions: -- Other library packages from which modules are imported. @@ -167,6 +166,27 @@ executable cardano-recon -- Directories containing source files. hs-source-dirs: app +executable cardano-recon-grep + import: common + main-is: Cardano/ReConGrep.hs + + ghc-options: -O2 + + build-depends: + base + , text + , containers + , bytestring + , aeson + , aeson-pretty + , mtl + , time + , cardano-recon-framework + , trace-dispatcher + , optparse-applicative + + hs-source-dirs: app + test-suite cardano-recon-test import: common type: exitcode-stdio-1.0 diff --git a/bench/cardano-recon-framework/docs/formula-languages.txt b/bench/cardano-recon-framework/docs/formula-languages.txt new file mode 100644 index 00000000000..211dff71e85 --- /dev/null +++ b/bench/cardano-recon-framework/docs/formula-languages.txt @@ -0,0 +1,84 @@ +Formula Languages in Cardano ReCon +==================================== + +Languages are ordered from most to least expressive. +Each language is a strict subset of the language above it. + +┌─────────────────────────────────────────────────────────────────────────┐ +│ Formula event ty │ +│ src/Cardano/ReCon/LTL/Formula.hs │ +│ │ +│ temporal : ☐ᵏ φ ♢ᵏ φ ◯ φ ◯ᵏ φ φ |ᵏ ψ │ +│ atomic : Atom ty cs │ +│ boolean : ∧ ∨ ¬ ⇒ ⊤ ⊥ │ +│ FO : ∀x∈ℤ ∃x∈ℤ ∀x∈{v̄} ∃x∈{v̄} ∀x∈Text ∃x∈Text │ +│ ground : t rel t' (int) t = v (text) │ +└────────────┬─────────────────────────────────────────┬──────────────────┘ + │ │ + retract H.retract + (partial: fails (partial: fails on + on temporal ops) temporal ops or atoms) + │ │ + ▼ │ +┌────────────────────────────────┐ │ +│ ContinuousFormula ty │ │ +│ src/Cardano/ReCon/LTL/ │ │ +│ ContinuousFormula.hs │ │ +│ │ │ +│ atomic : Atom ty cs │ │ +│ boolean : ∧ ∨ ¬ ⇒ ⊤ ⊥ │ │ +│ FO : ∀x∈ℤ ∃x∈ℤ │ │ +│ ∀x∈{v̄} ∃x∈{v̄} │ │ +│ ∀x∈Text ∃x∈Text │ │ +│ ground : t rel t' t = v │ │ +└────────────┬───────────────────┘ │ + │ │ + interp(e) next(e) then rewrite + (resolve atoms ↺ repeated per event; + against event e) terminate at end of seq + │ │ + └─────────────────────┬───────────────────┘ + │ + ▼ +┌─────────────────────────────────────────────────────────────────────────┐ +│ HomogeneousFormula │ +│ src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs │ +│ │ +│ boolean : ∧ ∨ ¬ ⇒ ⊤ ⊥ │ +│ FO : ∀x∈ℤ ∃x∈ℤ ∀x∈{v̄} ∃x∈{v̄} ∀x∈Text ∃x∈Text │ +│ ground : t rel t' (int) t = v (text) │ +└──────────────────────────────────┬──────────────────────────────────────┘ + │ + lower + (unfold ∀x∈{v̄}, ∃x∈{v̄} + into ∧ / ∨) + │ + ▼ +┌─────────────────────────────────────────────────────────────────────────┐ +│ FinFree │ +│ src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs │ +│ │ +│ boolean : ∧ ∨ ¬ ⇒ ⊤ ⊥ │ +│ FO : ∀x∈ℤ ∃x∈ℤ ∀x∈Text ∃x∈Text │ +│ ground : t rel t' (int) t = v (text) │ +└──────────────────────────────────┬──────────────────────────────────────┘ + │ + lower + (decide ∀x∈Text, ∃x∈Text via + value accumulation + substitution) + │ + ▼ +┌─────────────────────────────────────────────────────────────────────────┐ +│ Presburger.Formula │ +│ src/Cardano/ReCon/Presburger/Formula.hs │ +│ │ +│ boolean : ∧ ∨ ¬ ⇒ ⊤ ⊥ │ +│ FO : ∀x∈ℤ ∃x∈ℤ │ +│ ground : t rel t' (int only) │ +└──────────────────────────────────┬──────────────────────────────────────┘ + │ + PD.eval + (Cooper quantifier elimination) + │ + ▼ + Bool diff --git a/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt b/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt index fcf10643a60..007efcd1226 100644 --- a/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt +++ b/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt @@ -37,6 +37,9 @@ c ::= name = t // property constraint, examples: // — slot = 1 // — "host" = "macbook-pro" // — slot = x + // Note: TraceMessage properties live inside the "data" JSON + // object. The "data" prefix is omitted when writing names; + // write `slot = 42`, not `data.slot = 42`. c̄ ::= {c, ..., c} // set of property constraints, examples: // — {slot = x} // — {slot = 42, blockHash = "xyz"} diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs new file mode 100644 index 00000000000..0ca1b9acb9d --- /dev/null +++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs @@ -0,0 +1,142 @@ +module Cardano.ReCon.LTL.ContinuousFormula ( + ContinuousFormula(..) + , retract + , interp + , eval) where + +import Cardano.ReCon.Common.Types (BinRel (..), IntValue, VariableIdentifier) +import Cardano.ReCon.Integer.Polynomial.Term (IntTerm (..)) +import Cardano.ReCon.LTL.Formula (Event (..), Formula, OnMissingKey (..), PropConstraint (..), + TextTerm, TextValue) +import qualified Cardano.ReCon.LTL.Formula as F +import Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula (HomogeneousFormula) +import qualified Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula as H + +import Control.Monad.Reader (Reader, asks) +import Data.Map.Strict (lookup) +import Data.Set (Set) +import qualified Data.Set as Set +import qualified Data.Text as Text +import Prelude hiding (lookup) + +-- | Default name: φ. +-- +-- The continuous counterpart of 'Formula': all temporal connectives are +-- absent. A 'ContinuousFormula' is evaluated against a /single/ event +-- (or time unit) rather than a sequence, making it a purely propositional / +-- first-order assertion about the present moment. +data ContinuousFormula ty = + + -------------- Atomic --------------- + -- | ty c̄ + Atom ty (Set PropConstraint) + ------------------------------------- + + ------------ Connective ------------- + -- | φ ∨ ψ + | Or (ContinuousFormula ty) (ContinuousFormula ty) + -- | φ ∧ ψ + | And (ContinuousFormula ty) (ContinuousFormula ty) + -- | ¬ φ + | Not (ContinuousFormula ty) + -- | φ ⇒ ψ + | Implies (ContinuousFormula ty) (ContinuousFormula ty) + -- | ⊤ + | Top + -- | ⊥ + | Bottom + ------------------------------------- + + ----------- Event property ---------- + -- | ∀x ∈ ℤ. φ — x ranges over all integers + | PropIntForall VariableIdentifier (ContinuousFormula ty) + -- | ∀x ∈ Text. φ — x ranges over all strings + | PropTextForall VariableIdentifier (ContinuousFormula ty) + -- | ∀x ∈ v̄. φ — x ranges over the given integers + | PropIntForallN VariableIdentifier (Set IntValue) (ContinuousFormula ty) + -- | ∀x ∈ v̄. φ — x ranges over the given strings + | PropTextForallN VariableIdentifier (Set TextValue) (ContinuousFormula ty) + -- | ∃x ∈ ℤ. φ — x ranges over all integers + | PropIntExists VariableIdentifier (ContinuousFormula ty) + -- | ∃x ∈ Text. φ — x ranges over all strings + | PropTextExists VariableIdentifier (ContinuousFormula ty) + -- | ∃x ∈ v̄. φ — x ranges over the given integers + | PropIntExistsN VariableIdentifier (Set IntValue) (ContinuousFormula ty) + -- | ∃x ∈ v̄. φ — x ranges over the given strings + | PropTextExistsN VariableIdentifier (Set TextValue) (ContinuousFormula ty) + -- | t rel t (integer) + | PropIntBinRel BinRel IntTerm IntTerm + -- | t = v (text) + | PropTextEq TextTerm TextValue + ------------------------------------- + deriving (Show, Eq, Ord) + +-- | Retract a 'Formula' into a 'ContinuousFormula', returning 'Nothing' if +-- the formula contains any temporal connective. +retract :: Formula event ty -> Maybe (ContinuousFormula ty) +retract (F.Forall {}) = Nothing +retract (F.ForallN {}) = Nothing +retract (F.ExistsN {}) = Nothing +retract (F.Next {}) = Nothing +retract (F.NextN {}) = Nothing +retract (F.UntilN {}) = Nothing +retract (F.Atom ty cs) = Just (Atom ty cs) +retract (F.Or phi psi) = Or <$> retract phi <*> retract psi +retract (F.And phi psi) = And <$> retract phi <*> retract psi +retract (F.Not phi) = Not <$> retract phi +retract (F.Implies phi psi) = Implies <$> retract phi <*> retract psi +retract F.Top = Just Top +retract F.Bottom = Just Bottom +retract (F.PropIntForall x phi) = PropIntForall x <$> retract phi +retract (F.PropTextForall x phi) = PropTextForall x <$> retract phi +retract (F.PropIntForallN x dom phi) = PropIntForallN x dom <$> retract phi +retract (F.PropTextForallN x dom phi) = PropTextForallN x dom <$> retract phi +retract (F.PropIntExists x phi) = PropIntExists x <$> retract phi +retract (F.PropTextExists x phi) = PropTextExists x <$> retract phi +retract (F.PropIntExistsN x dom phi) = PropIntExistsN x dom <$> retract phi +retract (F.PropTextExistsN x dom phi) = PropTextExistsN x dom <$> retract phi +retract (F.PropIntBinRel rel _ t1 t2) = Just (PropIntBinRel rel t1 t2) +retract (F.PropTextEq _ t v) = Just (PropTextEq t v) + +-- | Decide (e ⊧ φ). +eval :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey Bool +eval phi e = H.eval <$> interp phi e + +-- | Algorithm for (e ⊧ φ): checks each 'Atom' against the event type and +-- substitutes property constraints with the event's concrete values, +-- yielding a 'HomogeneousFormula' ready for decision. +interp :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey HomogeneousFormula +interp phi e = go phi + where + go (Atom ty cs) + | ofTy e ty = foldr H.And H.Top <$> traverse (evalConstraint ty) (Set.toList cs) + | otherwise = pure H.Bottom + go (Or phi' psi) = H.Or <$> go phi' <*> go psi + go (And phi' psi) = H.And <$> go phi' <*> go psi + go (Not phi') = H.Not <$> go phi' + go (Implies phi' psi) = H.Implies <$> go phi' <*> go psi + go Top = pure H.Top + go Bottom = pure H.Bottom + go (PropIntForall x phi') = H.PropIntForall x <$> go phi' + go (PropTextForall x phi') = H.PropTextForall x <$> go phi' + go (PropIntForallN x dom phi') = H.PropIntForallN x dom <$> go phi' + go (PropTextForallN x dom phi') = H.PropTextForallN x dom <$> go phi' + go (PropIntExists x phi') = H.PropIntExists x <$> go phi' + go (PropTextExists x phi') = H.PropTextExists x <$> go phi' + go (PropIntExistsN x dom phi') = H.PropIntExistsN x dom <$> go phi' + go (PropTextExistsN x dom phi') = H.PropTextExistsN x dom <$> go phi' + go (PropIntBinRel rel t1 t2) = pure $ H.PropIntBinRel rel t1 t2 + go (PropTextEq t v) = pure $ H.PropTextEq t v + + evalConstraint ty (IntPropConstraint key t) = + case lookup key (intProps e ty) of + Just v -> pure $ H.PropIntBinRel Eq t (IntConst v) + Nothing -> missingKey key + evalConstraint ty (TextPropConstraint key t) = + case lookup key (textProps e ty) of + Just v -> pure $ H.PropTextEq t v + Nothing -> missingKey key + + missingKey key = asks $ \case + BottomOnMissingKey -> H.Bottom + CrashOnMissingKey -> error $ "Missing key: " <> Text.unpack key diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs index 65fd24774f0..6851c415d3e 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs +++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs @@ -111,6 +111,9 @@ data Formula event ty = -- φ |¹⁺ᵏ ψ ≡ ψ ∨ ¬ ψ ∧ φ ∧ (φ |ᵏ ψ) -- φ until ψ in the n units of time from now | UntilN Word (Formula event ty) (Formula event ty) + ------------------------------------- + + -------------- Atomic --------------- -- | ty c̄ | Atom ty (Set PropConstraint) ------------------------------------- diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs index 594641d588c..a0084c83378 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs +++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs @@ -21,7 +21,7 @@ import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) --- | A `Formula` with no temporal operators. +-- | A `Formula` with no temporal operators and no atoms. -- Equivalence of two `HomogeneousFormula`s is decidable. data HomogeneousFormula = ------------ Connective ------------- diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs index b58f3dada69..06fade63350 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs +++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs @@ -9,15 +9,18 @@ module Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree ( import Cardano.ReCon.Common.Types (BinRel (..)) import Cardano.ReCon.LTL.Formula (IntTerm (..), IntValue, TextTerm (..), VariableIdentifier) -import Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree (Extended (..)) import Cardano.ReCon.LTL.Internal.Subst (substIntTerm) -import qualified Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree as TextFree +import qualified Cardano.ReCon.Presburger.Decide as PD +import qualified Cardano.ReCon.Presburger.Formula as P import Data.Functor ((<&>)) import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) +-- | An extended value: either a concrete value or a placeholder distinct from all concrete values. +data Extended a = Val a | Placeholder deriving (Show, Ord, Eq) + -- | `HomogeneousFormula` with all finite-domain quantifiers already eliminated. -- Only infinite-domain (unbounded) quantifiers remain. data FinFree = @@ -114,42 +117,42 @@ substText v x (PropTextExists x' phi) | x /= x' = PropTextExists x' (substText v substText _ _ (PropTextExists x' phi) = PropTextExists x' phi -- --------------------------------------------------------------------------- --- Lowering to TextFree +-- Lowering to Presburger.Formula -- --------------------------------------------------------------------------- --- | Lower a `FinFree` to `TextFree` by eliminating all text quantifiers and +-- | Lower a `FinFree` to 'P.Formula' by eliminating all text quantifiers and -- evaluating ground `PropTextEq` atoms. -- -- Text universals unfold to a conjunction (⊤ for empty domain); -- text existentials unfold to a disjunction (⊥ for empty domain). -- --- @'eval' = 'TextFree.eval' . 'lower'@ -lower :: FinFree -> TextFree.TextFree -lower (Or phi psi) = TextFree.Or (lower phi) (lower psi) -lower (And phi psi) = TextFree.And (lower phi) (lower psi) -lower (Not phi) = TextFree.Not (lower phi) -lower (Implies phi psi) = TextFree.Implies (lower phi) (lower psi) -lower Top = TextFree.Top -lower Bottom = TextFree.Bottom -lower (PropIntForall x phi) = TextFree.PropIntForall x (lower phi) -lower (PropIntExists x phi) = TextFree.PropIntExists x (lower phi) -lower (PropIntBinRel rel lhs rhs) = TextFree.PropIntBinRel rel lhs rhs +-- @'eval' = 'PD.eval' . 'lower'@ +lower :: FinFree -> P.Formula +lower (Or phi psi) = P.Or (lower phi) (lower psi) +lower (And phi psi) = P.And (lower phi) (lower psi) +lower (Not phi) = P.Not (lower phi) +lower (Implies phi psi) = P.Implies (lower phi) (lower psi) +lower Top = P.Top +lower Bottom = P.Bottom +lower (PropIntForall x phi) = P.IntForall x (lower phi) +lower (PropIntExists x phi) = P.IntExists x (lower phi) +lower (PropIntBinRel rel lhs rhs) = P.IntBinRel rel lhs rhs -- Ground text equations are folded directly to ⊤/⊥: lower (PropTextEq (TextConst lhs) rhs) - | lhs == rhs = TextFree.Top - | otherwise = TextFree.Bottom + | lhs == rhs = P.Top + | otherwise = P.Bottom lower (PropTextEq (TextVar x) _) = error $ "lower: free text variable " <> show x -- ⟦∀x ∈ Text. φ⟧ ≡ φ[☐/x] ∧ φ[v₁/x] ∧ ... (⊤ when dom is empty) lower (PropTextForall x phi) = let vals = Set.toList (textValues x phi) - in foldr TextFree.And TextFree.Top + in foldr P.And P.Top (lower (substText Placeholder x phi) : (vals <&> \v -> lower (substText (Val v) x phi))) -- ⟦∃x ∈ Text. φ⟧ ≡ φ[☐/x] ∨ φ[v₁/x] ∨ ... (⊥ when dom is empty) lower (PropTextExists x phi) = let vals = Set.toList (textValues x phi) - in foldr TextFree.Or TextFree.Bottom + in foldr P.Or P.Bottom (lower (substText Placeholder x phi) : (vals <&> \v -> lower (substText (Val v) x phi))) -- | Evaluate the `FinFree` onto `Bool`. eval :: FinFree -> Bool -eval = TextFree.eval . lower +eval = PD.eval . lower diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/TextFree.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/TextFree.hs deleted file mode 100644 index 97fed563e62..00000000000 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/TextFree.hs +++ /dev/null @@ -1,58 +0,0 @@ -module Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree ( - TextFree(..) - , Extended(..) - , eval - ) where - -import Cardano.ReCon.Common.Types (BinRel (..)) -import Cardano.ReCon.Integer.Polynomial.Term (IntTerm) -import Cardano.ReCon.LTL.Formula (VariableIdentifier) -import qualified Cardano.ReCon.Presburger.Decide as PD -import qualified Cardano.ReCon.Presburger.Formula as P - --- | An extended value: either a concrete value or a placeholder distinct from all concrete values. -data Extended a = Val a | Placeholder deriving (Show, Ord, Eq) - --- | `FinFree` with all text quantifiers and `PropTextEq` atoms eliminated. --- Only integer operations remain. -data TextFree = - ------------ Connective ------------- - Or TextFree TextFree - | And TextFree TextFree - | Not TextFree - | Implies TextFree TextFree - | Top - | Bottom - ------------------------------------- - - ----------- Event property ---------- - | PropIntForall VariableIdentifier TextFree - | PropIntExists VariableIdentifier TextFree - | PropIntBinRel BinRel IntTerm IntTerm - deriving (Show, Eq, Ord) - ------------------------------------- - --- --------------------------------------------------------------------------- --- Translation to Presburger arithmetic --- --------------------------------------------------------------------------- - -toPresburger :: TextFree -> P.Formula -toPresburger (Or phi psi) = P.Or (toPresburger phi) (toPresburger psi) -toPresburger (And phi psi) = P.And (toPresburger phi) (toPresburger psi) -toPresburger (Not phi) = P.Not (toPresburger phi) -toPresburger (Implies phi psi) = P.Implies (toPresburger phi) (toPresburger psi) -toPresburger Top = P.Top -toPresburger Bottom = P.Bottom -toPresburger (PropIntForall x phi) = P.IntForall x (toPresburger phi) -toPresburger (PropIntExists x phi) = P.IntExists x (toPresburger phi) -toPresburger (PropIntBinRel rel lhs rhs) = P.IntBinRel rel lhs rhs - - --- --------------------------------------------------------------------------- --- Evaluation --- --------------------------------------------------------------------------- - --- | Evaluate a `TextFree` formula by translating to Presburger arithmetic --- and deciding via quantifier elimination. -eval :: TextFree -> Bool -eval = PD.eval . toPresburger