Skip to content

Commit 86820f7

Browse files
RussoulRussoul
committed
bench: Implement a decision procedure for Presburger Arithmetic (as per Cooper)
1 parent b5ef5d6 commit 86820f7

66 files changed

Lines changed: 3468 additions & 1429 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎bench/cardano-recon-framework/CHANGELOG.md‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
# Revision history for cardano-trace-ltl
22

3-
## 1.1.0 -- March 2026
3+
## 1.1.0 -- April 2026
44

55
* Support configurable timeunits in formulas via a CLI option.
66
* Support existential quantification over properties (both finite and infinite domain)
7+
* Support Presburger arithmetic (over ℤ)
78

89
## 1.0.0 -- Feb 2026
910

‎bench/cardano-recon-framework/app/Cardano/ReCon.hs‎

Lines changed: 11 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,20 @@
1-
{-# OPTIONS_GHC -Wno-orphans #-}
21
{-# LANGUAGE PackageImports #-}
32

43
module Main(main) where
54

65
import Cardano.Logging
76
import Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..),
87
runPrometheusSimple)
9-
import Cardano.Logging.Types.TraceMessage (TraceMessage (..))
8+
import Cardano.Logging.Types.TraceMessage ()
109
import Cardano.ReCon.Cli (CliOptions (..), Mode (..), opts, timeunitToMicrosecond)
11-
import Cardano.ReCon.Common (extractProps)
10+
import Cardano.ReCon.Trace.Event ()
1211
import Cardano.ReCon.LTL.Check (checkFormula, prettyError)
13-
import Cardano.ReCon.LTL.Lang.Formula
14-
import Cardano.ReCon.LTL.Lang.Formula.Parser (Context (..))
15-
import qualified Cardano.ReCon.LTL.Lang.Formula.Parser as Parser
16-
import Cardano.ReCon.LTL.Lang.Formula.Yaml
17-
import Cardano.ReCon.LTL.Pretty (prettyFormula)
18-
import qualified Cardano.ReCon.LTL.Pretty as Prec
12+
import Cardano.ReCon.LTL.Formula
13+
import Cardano.ReCon.LTL.Formula.Parser (Context (..))
14+
import qualified Cardano.ReCon.LTL.Formula.Parser as Parser
15+
import Cardano.ReCon.LTL.Formula.Yaml
16+
import Cardano.ReCon.LTL.Formula.Pretty (prettyFormula)
17+
import qualified Cardano.ReCon.LTL.Formula.Pretty as Prec
1918
import Cardano.ReCon.LTL.Satisfy
2019
import Cardano.ReCon.Trace.Feed (TemporalEvent (..), TemporalEventDurationMicrosec, read,
2120
readS)
@@ -31,10 +30,9 @@ import Control.Monad (forever, when, (>=>))
3130
import "contra-tracer" Control.Tracer (Tracer (..))
3231
import Data.Foldable (for_)
3332
import Data.IORef (IORef, newIORef, readIORef)
34-
import Data.List (find)
3533
import qualified Data.Map as Map
36-
import Data.Maybe (fromMaybe, isJust, listToMaybe)
37-
import Data.Text (Text, unpack)
34+
import Data.Maybe (fromMaybe, listToMaybe)
35+
import Data.Text (Text)
3836
import qualified Data.Text as Text
3937
import Data.Traversable (for)
4038
import GHC.IO.Encoding (setLocaleEncoding, utf8)
@@ -47,16 +45,6 @@ import qualified System.Metrics as EKG
4745
import Streaming
4846

4947

50-
instance Event TemporalEvent Text where
51-
ofTy (TemporalEvent _ msgs) c = isJust $ find (\msg -> msg.tmsgNS == c) msgs
52-
props (TemporalEvent _ msgs) c =
53-
case find (\msg -> msg.tmsgNS == c) msgs of
54-
Just x -> Map.insert "host" (TextValue x.tmsgHost) $
55-
Map.insert "thread" (TextValue x.tmsgThread) $
56-
extractProps x.tmsgData
57-
Nothing -> error ("Not an event of type " <> unpack c)
58-
beg (TemporalEvent t _) = t
59-
6048
check :: Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO ()
6149
check idx {- Formula index -} tr phi events =
6250
let result = satisfies phi events in
@@ -151,7 +139,7 @@ main = do
151139
ctx <- Map.toList . fromMaybe Map.empty <$> for options.context (readPropValues >=> dieOnYamlException)
152140
putStrLn "Context:"
153141
print ctx
154-
formulas <- readFormulas options.formulas (Context ctx) Parser.text >>= dieOnYamlException
142+
formulas <- readFormulas options.formulas (Context { interpDomain = ctx, varKinds = Map.empty }) Parser.name >>= dieOnYamlException
155143
for_ (fmap (\phi -> (phi, checkFormula mempty phi)) formulas) $ \case
156144
(phi, e : es) -> die $
157145
Text.unpack $

‎bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,16 @@
11
module Cardano.ReCon.Common where
2-
import Cardano.ReCon.LTL.Lang.Formula
32

4-
import Data.Aeson
3+
import Data.Aeson (Object, Value (..))
54
import Data.Aeson.Key (toText)
65
import qualified Data.Aeson.KeyMap as KeyMap
76
import qualified Data.Map as Map
87
import Data.Map.Strict (Map)
8+
import Data.Text (Text)
99

10-
-- | Extract all accessible properties (fields) from the json object, non-recursively.
11-
-- Accessible fields are all fields of one of the following types: number, string.
12-
extractProps :: Object -> Map PropVarIdentifier PropValue
13-
extractProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
10+
-- | Extract scalar properties from a JSON object as Aeson Values, for display.
11+
extractJsonProps :: Object -> Map Text Value
12+
extractJsonProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
1413
where
15-
f (Number v) = Just $ IntValue (truncate v)
16-
f (String v) = Just $ TextValue v
17-
f _ = Nothing
14+
f v@(Number _) = Just v
15+
f v@(String _) = Just v
16+
f _ = Nothing

‎bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@ module Cardano.ReCon.TraceMessage where
55
import Cardano.Logging
66
import Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..))
77
import qualified Cardano.Logging.Types.TraceMessage as Envelop
8-
import Cardano.ReCon.Common (extractProps)
9-
import Cardano.ReCon.LTL.Lang.Formula (Formula, PropValue (..), Relevance)
10-
import qualified Cardano.ReCon.LTL.Lang.Formula.Prec as Prec
11-
import Cardano.ReCon.LTL.Pretty (prettyFormula)
8+
import Cardano.ReCon.Common (extractJsonProps)
9+
import Cardano.ReCon.LTL.Formula (Formula, Relevance)
10+
import qualified Cardano.ReCon.LTL.Formula.Prec as Prec
11+
import Cardano.ReCon.LTL.Formula.Pretty (prettyFormula)
1212
import Cardano.ReCon.LTL.Satisfy (SatisfactionResult (..))
1313
import Cardano.ReCon.Trace.Feed (TemporalEvent (..))
1414

@@ -61,11 +61,11 @@ red text = "\x001b[31m" <> text <> "\x001b[0m"
6161
prettyTraceMessage :: Envelop.TraceMessage -> Text
6262
prettyTraceMessage Envelop.TraceMessage{..} =
6363
toStrict $ toLazyText $ encodePrettyToTextBuilder $
64-
Map.insert "at" (TextValue (showT tmsgAt)) $
65-
Map.insert "namespace" (TextValue tmsgNS) $
66-
Map.insert "host" (TextValue tmsgHost) $
67-
Map.insert "thread" (TextValue tmsgThread) $
68-
extractProps tmsgData
64+
Map.insert "at" (String (showT tmsgAt)) $
65+
Map.insert "namespace" (String tmsgNS) $
66+
Map.insert "host" (String tmsgHost) $
67+
Map.insert "thread" (String tmsgThread) $
68+
extractJsonProps tmsgData
6969

7070
prettyTemporalEvent :: TemporalEvent -> Text -> Text
7171
prettyTemporalEvent (TemporalEvent _ msgs) ns =

‎bench/cardano-recon-framework/cardano-recon-framework.cabal‎

Lines changed: 56 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -62,27 +62,45 @@ common common
6262
library
6363
import: common
6464
exposed-modules:
65-
Cardano.ReCon.LTL.Check
66-
, Cardano.ReCon.LTL.Lang.Formula
67-
, Cardano.ReCon.LTL.Lang.Formula.Parser
68-
, Cardano.ReCon.LTL.Lang.Formula.Prec
69-
, Cardano.ReCon.LTL.Lang.Formula.Yaml
70-
, Cardano.ReCon.LTL.Lang.Fragment
71-
, Cardano.ReCon.LTL.Lang.Fragment.Fragment0
72-
, Cardano.ReCon.LTL.Lang.Fragment.Fragment1
73-
, Cardano.ReCon.LTL.Lang.Fragment.Fragment2
74-
, Cardano.ReCon.LTL.Lang.HomogeneousFormula
75-
, Cardano.ReCon.LTL.Occurs
76-
, Cardano.ReCon.LTL.Pretty
77-
, Cardano.ReCon.LTL.Progress
78-
, Cardano.ReCon.LTL.Rewrite
65+
Cardano.ReCon.Common.Types
66+
, Cardano.ReCon.Common.Parser
67+
68+
, Cardano.ReCon.LTL.Check
69+
, Cardano.ReCon.LTL.Formula
70+
, Cardano.ReCon.LTL.Formula.Parser
71+
, Cardano.ReCon.LTL.Formula.Prec
72+
, Cardano.ReCon.LTL.Formula.Yaml
73+
, Cardano.ReCon.LTL.Formula.Pretty
7974
, Cardano.ReCon.LTL.Satisfy
80-
, Cardano.ReCon.LTL.Subst
8175

76+
, Cardano.ReCon.Integer.Polynomial.Parser
77+
, Cardano.ReCon.Integer.Polynomial.Term
78+
, Cardano.ReCon.Integer.Polynomial.Value
79+
80+
, Cardano.ReCon.Presburger.Decide
81+
, Cardano.ReCon.Presburger.Formula
82+
, Cardano.ReCon.Presburger.Parser
83+
84+
, Cardano.ReCon.Trace.Event
8285
, Cardano.ReCon.Trace.Feed
8386
, Cardano.ReCon.Trace.Ingest
8487

8588
other-modules:
89+
Cardano.ReCon.LTL.Internal.Occurs
90+
, Cardano.ReCon.LTL.Internal.Progress
91+
, Cardano.ReCon.LTL.Internal.Rewrite
92+
, Cardano.ReCon.LTL.Internal.Subst
93+
, Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula
94+
, Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree
95+
, Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree
96+
, Cardano.ReCon.Presburger.Internal.CooperQE
97+
, Cardano.ReCon.Presburger.Internal.IR.AffineDNF
98+
, Cardano.ReCon.Presburger.Internal.IR.CompNF
99+
, Cardano.ReCon.Presburger.Internal.IR.DNF
100+
, Cardano.ReCon.Presburger.Internal.IR.ForallFree
101+
, Cardano.ReCon.Presburger.Internal.IR.NegNF
102+
, Cardano.ReCon.Presburger.Internal.IR.NormAffineDNF
103+
, Cardano.ReCon.Presburger.Internal.IR.QuantifierFree
86104
other-extensions:
87105

88106
build-depends: base
@@ -147,6 +165,13 @@ test-suite cardano-recon-test
147165
type: exitcode-stdio-1.0
148166
hs-source-dirs: test
149167
main-is: Cardano/ReCon/Unit.hs
168+
other-modules:
169+
Cardano.ReCon.Integer.Polynomial.Semantics.Suite
170+
, Cardano.ReCon.Integer.Polynomial.Syntax.Suite
171+
, Cardano.ReCon.LTL.Semantics.Suite
172+
, Cardano.ReCon.LTL.Syntax.Suite
173+
, Cardano.ReCon.Presburger.Semantics.Suite
174+
, Cardano.ReCon.Presburger.Syntax.Suite
150175
build-depends:
151176
base
152177
, cardano-recon-framework
@@ -155,3 +180,19 @@ test-suite cardano-recon-test
155180
, tasty-hunit
156181
, text
157182
, megaparsec
183+
184+
test-suite cardano-recon-integration-test
185+
import: common
186+
type: exitcode-stdio-1.0
187+
hs-source-dirs: test
188+
main-is: Cardano/ReCon/Integration.hs
189+
other-modules:
190+
Cardano.ReCon.Integration.Suite
191+
build-depends:
192+
base
193+
, cardano-recon-framework
194+
, containers
195+
, filepath
196+
, tasty
197+
, tasty-hunit
198+
, text

‎bench/cardano-recon-framework/docs/ltl-formula-syntax.txt‎

Lines changed: 44 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,61 @@
1-
s ::= "..." where ... stands for a list of arbitrary unicode characters such that each is:
2-
— not a control
3-
— if whitespace, then simple ' '
4-
— not a double quote
5-
x ::= [_a-zA-Z][_a-zA-Z0-9]*
6-
v ::= <int> | s // property value, examples:
7-
// — 42
8-
// — "hello"
9-
v̄ ::= {v, ..., v} // set of property values, examples:
10-
// — {42, "hello"}
11-
// — {}
12-
// — {1, 2, 3, "bye"}
1+
<string> stands for a list of arbitrary unicode characters in double-quotes such that each is:
2+
— not a control
3+
— if whitespace, then simple ' '
4+
— not a double quote
5+
<int> stands for an integer // examples: 0, -1, 42
6+
<nat> stands for a natural number written in // examples: ⁰ ¹ ⁴² (superscript)
7+
superscript or subscript Unicode digits // ₀ ₁ ₄₂ (subscript)
8+
9+
x ::= [_a-zA-Z][_a-zA-Z0-9₀-₉]*
10+
11+
// integer (ℤ) terms
12+
i{atom} ::= <int> | <int> · x | x | (i{≥universe})
13+
i{universe} ::= i{≥atom} + i{≥universe}
14+
| i{≥atom} - i{≥universe}
15+
16+
// string terms
17+
s ::= <string>
18+
19+
// property value: integer or string
20+
v ::= <int> | s
21+
22+
// quantifier domain: a homogeneous set of integers or strings, or a context variable
23+
v̄ ::= {<int>, ..., <int>} // integer domain, examples: {}, {1, 2, 3}
24+
| {s, ..., s} // string domain, examples: {}, {"a", "b"}
25+
| $x // context-provided domain variable
26+
1327
t ::= <int> | s | x // property term, examples:
1428
// — 42
1529
// — "hello"
1630
// — x
1731
// — this_is_variable
18-
c ::= s = t // property constraint, examples:
19-
// — "slot" = 1
32+
name ::= [_a-zA-Z][_a-zA-Z0-9._]* | s // unquoted or quoted, examples:
33+
// — slot
34+
// — Forge.Loop.ForgedBlock
35+
// — "with spaces"
36+
c ::= name = t // property constraint, examples:
37+
// — slot = 1
2038
// — "host" = "macbook-pro"
21-
// — "slot" = x
39+
// — slot = x
2240
c̄ ::= {c, ..., c} // set of property constraints, examples:
23-
// — {"slot" = x}
24-
// — {"slot" = 42, "blockHash" = "xyz"}
41+
// — {slot = x}
42+
// — {slot = 42, blockHash = "xyz"}
2543
// — {}
26-
ns ::= s // namespace, examples:
27-
// — "Forge.Loop.ForgedBlock"
44+
ns ::= name // namespace, examples:
45+
// — Forge.Loop.ForgedBlock
2846
// — "Forge.Loop.NodeIsLeader"
2947

3048
φ{atom} ::= ⊤ | ⊥ | ns c̄ | (φ{≥universe})
31-
φ{eq} ::= t = v
49+
φ{eq} ::= i = i | i < i | i > i | i ≤ i | i ≥ i
50+
| x = s // text equality; only = is supported, not <, >, etc.
3251
φ{prefix} ::= ◯ φ{≥atom} | ◯ᵏ φ{≥atom} | ♢ᵏ φ{≥atom} | ☐ ᪲ₖ φ{≥atom} | ☐ᵏ φ{≥atom} | ¬ φ{≥atom}
3352
φ{and} ::= φ{>and} ∧ φ{≥and}
3453
φ{or} ::= φ{>or} ∨ φ{≥or}
3554
φ{implies} ::= φ{>implies} ⇒ φ{≥implies}
36-
φ{universe} ::= ∀(x ∈ v̄). φ{≥universe} | ∀x. φ{≥universe}
37-
| ∃(x ∈ v̄). φ{≥universe} | ∃x. φ{≥universe}
38-
| φ{≥implies} \|ᵏ φ{≥implies}
55+
φ{universe} ::= ∀x ∈ v̄. φ{≥universe} | ∀x ∈ ℤ. φ{≥universe} | ∀x ∈ Text. φ{≥universe}
56+
| ∃x ∈ v̄. φ{≥universe} | ∃x ∈ ℤ. φ{≥universe} | ∃x ∈ Text. φ{≥universe}
57+
| φ{≥implies} |ᵏ φ{≥implies} // until; | here is not BNF alternation
58+
59+
// k denotes a <nat> encoded as superscript (e.g. ◯⁴²) or subscript (e.g. ☐ ᪲₄₂)
3960

4061
atom < eq = prefix < and < or < implies < universe

0 commit comments

Comments
 (0)