Skip to content

Commit 352fe4d

Browse files
RussoulRussoul
committed
Support existential quantification over properties
1 parent 06fc91f commit 352fe4d

14 files changed

Lines changed: 195 additions & 4 deletions

File tree

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
## 1.1.0 -- March 2026
44

55
* Support configurable timeunits in formulas via a CLI option.
6+
* Support existential quantification over properties (both finite and infinite domain)
67

78
## 1.0.0 -- Feb 2026
89

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,8 @@ ns ::= s // namespace, examples:
3333
φ{and} ::= φ{>and} ∧ φ{≥and}
3434
φ{or} ::= φ{>or} ∨ φ{≥or}
3535
φ{implies} ::= φ{>implies} ⇒ φ{≥implies}
36-
φ{universe} ::= ∀(x ∈ v̄). φ{≥universe}
37-
| ∀x. φ{≥universe} | φ{≥implies} \|ᵏ φ{≥implies}
36+
φ{universe} ::= ∀(x ∈ v̄). φ{≥universe} | ∀x. φ{≥universe}
37+
| ∃(x ∈ v̄). φ{≥universe} | ∃x. φ{≥universe}
38+
| φ{≥implies} \|ᵏ φ{≥implies}
3839

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

‎bench/cardano-recon-framework/docs/satisfiability-semantics.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,8 @@
3535
t̄ ⊧ φ // connective & event property fragments
3636
(t̄ ⊧ ∀x. φ) ⇔ (∀x. (t̄ ⊧ φ))
3737
(t̄ ⊧ ∀(x ∈ v̄). φ) ⇔ (∀(x ∈ v̄). (t̄ ⊧ φ))
38+
(t̄ ⊧ ∃x. φ) ⇔ (∃x. (t̄ ⊧ φ))
39+
(t̄ ⊧ ∃(x ∈ v̄). φ) ⇔ (∃(x ∈ v̄). (t̄ ⊧ φ))
3840
(t̄ ⊧ φ ∨ ψ) ⇔ ((t̄ ⊧ φ) ∨ (t̄ ⊧ ψ))
3941
(t̄ ⊧ φ ∧ ψ) ⇔ ((t̄ ⊧ φ) ∧ (t̄ ⊧ ψ))
4042
(t̄ ⊧ φ ⇒ ψ) ⇔ ((t̄ ⊧ φ) ⇒ (t̄ ⊧ ψ))

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Check.hs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,5 +54,7 @@ checkFormula bound (Implies phi psi) = checkFormula bound phi ++ checkFormula bo
5454
checkFormula bound (UntilN _ phi psi) = checkFormula bound phi ++ checkFormula bound psi
5555
checkFormula bound (PropForall x phi) = checkFormula (insert x bound) phi
5656
checkFormula bound (PropForallN x _ phi) = checkFormula (insert x bound) phi
57+
checkFormula bound (PropExists x phi) = checkFormula (insert x bound) phi
58+
checkFormula bound (PropExistsN x _ phi) = checkFormula (insert x bound) phi
5759
checkFormula bound (PropEq _ t _) = checkParamTerm bound t
5860
checkFormula bound (Atom _ cs) = foldl' (++) [] (fmap (checkParamConstraint bound) (Set.toList cs))

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula.hs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,11 @@ data Formula event ty =
111111
-- | ∀(x ∈ v̄). φ
112112
-- `x` ranges over values in `v̄`
113113
| PropForallN PropVarIdentifier (Set PropValue) (Formula event ty)
114+
-- | ∃x. φ
115+
| PropExists PropVarIdentifier (Formula event ty)
116+
-- | ∃(x ∈ v̄). φ
117+
-- `x` ranges over values in `v̄`
118+
| PropExistsN PropVarIdentifier (Set PropValue) (Formula event ty)
114119
-- | i = v
115120
| PropEq (Relevance event ty) PropTerm PropValue deriving (Show, Eq, Ord)
116121
-------------------------------------
@@ -135,6 +140,8 @@ relevance = go mempty where
135140
go acc (Atom {}) = acc
136141
go acc (PropForall _ phi) = go acc phi
137142
go acc (PropForallN _ _ phi) = go acc phi
143+
go acc (PropExists _ phi) = go acc phi
144+
go acc (PropExistsN _ _ phi) = go acc phi
138145
go acc (PropEq rel _ _) = rel `union` acc
139146

140147
unfoldForall :: Word -> Formula event ty -> Formula event ty
@@ -189,6 +196,8 @@ interpTimeunit _ phi@Atom{} = phi
189196
interpTimeunit _ phi@PropEq{} = phi
190197
interpTimeunit f (PropForall x phi) = PropForall x (interpTimeunit f phi)
191198
interpTimeunit f (PropForallN x dom phi) = PropForallN x dom (interpTimeunit f phi)
199+
interpTimeunit f (PropExists x phi) = PropExists x (interpTimeunit f phi)
200+
interpTimeunit f (PropExistsN x dom phi) = PropExistsN x dom (interpTimeunit f phi)
192201

193202
-- | A constraint signifying that `a` is an `Event` over base `ty`:
194203
-- — Given an element of `ty`, `ofTy` shall name whether the event is of the given type.

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula/Parser.hs‎

Lines changed: 35 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -196,6 +196,20 @@ formulaPropForall ctx ty = do
196196
phi <- formulaUniverse ctx ty
197197
pure (maybe (PropForall x phi) (\dom -> PropForallN x dom phi) optDom)
198198

199+
formulaPropExists :: Context -> Parser ty -> Parser (Formula event ty)
200+
formulaPropExists ctx ty = do
201+
void $ string "∃"
202+
space
203+
x <- variableIdentifier
204+
space
205+
optDom <- optional $ do
206+
void $ string "∈"
207+
space *> setPropValue ctx <* space
208+
void $ string "."
209+
space
210+
phi <- formulaUniverse ctx ty
211+
pure (maybe (PropExists x phi) (\dom -> PropExistsN x dom phi) optDom)
212+
199213
formulaPropForallN :: Context -> Parser ty -> Parser (Formula event ty)
200214
formulaPropForallN ctx ty = do
201215
void $ try (string "∀" *> space *> string "(" *> space)
@@ -212,6 +226,22 @@ formulaPropForallN ctx ty = do
212226
phi <- formulaUniverse ctx ty
213227
pure (PropForallN x vs phi)
214228

229+
formulaPropExistsN :: Context -> Parser ty -> Parser (Formula event ty)
230+
formulaPropExistsN ctx ty = do
231+
void $ try (string "∃" *> space *> string "(" *> space)
232+
x <- variableIdentifier
233+
space
234+
void $ string "∈"
235+
space
236+
vs <- setPropValue ctx
237+
space
238+
void $ string ")"
239+
space
240+
void $ string "."
241+
space
242+
phi <- formulaUniverse ctx ty
243+
pure (PropExistsN x vs phi)
244+
215245
formulaUntilN :: Context -> Parser ty -> Parser (Formula event ty)
216246
formulaUntilN ctx ty = apply <$> (formulaImplies ctx ty <* space) <*> optional (do
217247
void $ string "|"
@@ -224,7 +254,11 @@ formulaUntilN ctx ty = apply <$> (formulaImplies ctx ty <* space) <*> optional (
224254
apply phi (Just (!k, !psi)) = UntilN k phi psi
225255

226256
formulaUniverse :: Context -> Parser ty -> Parser (Formula event ty)
227-
formulaUniverse ctx ty = formulaPropForallN ctx ty <|> formulaPropForall ctx ty <|> formulaUntilN ctx ty
257+
formulaUniverse ctx ty = formulaPropForallN ctx ty
258+
<|> formulaPropForall ctx ty
259+
<|> formulaPropExistsN ctx ty
260+
<|> formulaPropExists ctx ty
261+
<|> formulaUntilN ctx ty
228262

229263
formula :: Context -> Parser ty -> Parser (Formula event ty)
230264
formula = formulaUniverse

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Fragment.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,9 @@ retract abs (F.Not a) = F0.Not <$> retract abs a
2828
retract _ F.Top = Just F0.Top
2929
retract _ F.Bottom = Just F0.Bottom
3030
retract _ (F.PropForall {}) = Nothing
31+
retract _ (F.PropExists {}) = Nothing
3132
retract _ (F.PropForallN {}) = Nothing
33+
retract _ (F.PropExistsN {}) = Nothing
3234
retract (!x, !v) (F.PropEq rel (Var x') v') | x == x' && v == v'
3335
= Just (F0.Atom rel)
3436
retract _ (F.PropEq {}) = Nothing
@@ -77,7 +79,9 @@ findAtoms F.Top set = set
7779
findAtoms (F.PropEq _ (Var x) v) set = Set.insert (x, v) set
7880
findAtoms (F.PropEq {}) set = set
7981
findAtoms (F.PropForall _ phi) set = findAtoms phi set
82+
findAtoms (F.PropExists _ phi) set = findAtoms phi set
8083
findAtoms (F.PropForallN _ _ phi) set = findAtoms phi set
84+
findAtoms (F.PropExistsN _ _ phi) set = findAtoms phi set
8185

8286
-- | Given a set of propositional equalities {xᵢ = vᵢ}ᵢ and a formula, if the formula can be retracted into
8387
-- `Fragment0` where the atom is taken to be one of the equalities (xᵢ = vᵢ), computes normal form in `Fragment0` and

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/HomogeneousFormula.hs‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
{- HLINT ignore "Use all" -}
2+
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
3+
{-# HLINT ignore "Use any" #-}
24
module Cardano.ReCon.LTL.Lang.HomogeneousFormula (
35
HomogeneousFormula(..)
46
, toFormula
@@ -37,6 +39,8 @@ data HomogeneousFormula event ty =
3739
----------- Event property ----------
3840
| PropForall PropVarIdentifier (HomogeneousFormula event ty)
3941
| PropForallN PropVarIdentifier (Set PropValue) (HomogeneousFormula event ty)
42+
| PropExists PropVarIdentifier (HomogeneousFormula event ty)
43+
| PropExistsN PropVarIdentifier (Set PropValue) (HomogeneousFormula event ty)
4044
| PropEq (Relevance event ty) PropTerm PropValue deriving (Show, Eq, Ord)
4145
-------------------------------------
4246

@@ -50,6 +54,8 @@ toFormula Top = F.Top
5054
toFormula (PropEq e a b) = F.PropEq e a b
5155
toFormula (PropForall x phi) = F.PropForall x (toFormula phi)
5256
toFormula (PropForallN x dom phi) = F.PropForallN x dom (toFormula phi)
57+
toFormula (PropExists x phi) = F.PropExists x (toFormula phi)
58+
toFormula (PropExistsN x dom phi) = F.PropExistsN x dom (toFormula phi)
5359

5460
valuesAccum :: Set PropValue -> PropVarIdentifier -> HomogeneousFormula event ty -> Set PropValue
5561
valuesAccum acc x (Or phi psi) = valuesAccum (valuesAccum acc x phi) x psi
@@ -65,6 +71,10 @@ valuesAccum acc x (PropForall x' phi) | x /= x' = valuesAccum acc x phi
6571
valuesAccum acc _ (PropForall _ _) = acc
6672
valuesAccum acc x (PropForallN x' _ phi) | x /= x' = valuesAccum acc x phi
6773
valuesAccum acc _ (PropForallN {}) = acc
74+
valuesAccum acc x (PropExists x' phi) | x /= x' = valuesAccum acc x phi
75+
valuesAccum acc _ (PropExists _ _) = acc
76+
valuesAccum acc x (PropExistsN x' _ phi) | x /= x' = valuesAccum acc x phi
77+
valuesAccum acc _ (PropExistsN {}) = acc
6878

6979
-- | Set of values the given prop var can take in the formula.
7080
values :: PropVarIdentifier -> HomogeneousFormula event ty -> Set PropValue
@@ -88,6 +98,10 @@ substHomogeneousFormula v x (PropForall x' phi) | x /= x' = PropForall x' (subst
8898
substHomogeneousFormula _ _ (PropForall x' phi) = PropForall x' phi
8999
substHomogeneousFormula v x (PropForallN x' dom phi) | x /= x' = PropForallN x' dom (substHomogeneousFormula v x phi)
90100
substHomogeneousFormula _ _ (PropForallN x' dom phi) = PropForallN x' dom phi
101+
substHomogeneousFormula v x (PropExists x' phi) | x /= x' = PropExists x' (substHomogeneousFormula v x phi)
102+
substHomogeneousFormula _ _ (PropExists x' phi) = PropExists x' phi
103+
substHomogeneousFormula v x (PropExistsN x' dom phi) | x /= x' = PropExistsN x' dom (substHomogeneousFormula v x phi)
104+
substHomogeneousFormula _ _ (PropExistsN x' dom phi) = PropExistsN x' dom phi
91105

92106
-- | Evaluate the `HomogeneousFormula` onto `Bool`.
93107
-- This is the "interesting" part of the iso: `HomogeneousFormula` ≅ `Bool`
@@ -112,6 +126,18 @@ eval (PropForallN x dom phi) =
112126
Set.toList dom <&> \v ->
113127
eval (substHomogeneousFormula (Val v) x phi)
114128
)
129+
-- ⟦∃x. φ⟧ <=> φ[☐/x] ∨ φ[v₁ / x] ∨ ... ∨ φ[vₖ / x] where v₁...vₖ is the set of values in φ which x can take.
130+
eval (PropExists x phi) = eval (substHomogeneousFormula Placeholder x phi) ||
131+
Prelude.or (
132+
Set.toList (values x phi) <&> \v ->
133+
eval (substHomogeneousFormula (Val v) x phi)
134+
)
135+
-- ⟦∃(x ∈ v₁...vₖ). φ⟧ <=> φ[v₁ / x] ∨ ... ∨ φ[vₖ / x]
136+
eval (PropExistsN x dom phi) =
137+
Prelude.or (
138+
Set.toList dom <&> \v ->
139+
eval (substHomogeneousFormula (Val v) x phi)
140+
)
115141

116142
-- | This is the "easy" part of the iso: `HomogeneousFormula` ≅ `Bool`
117143
quote :: Bool -> HomogeneousFormula event ty
@@ -144,6 +170,8 @@ retract = go Set.empty where
144170
go _ (F.PropEq _ (Var _) _) = Nothing
145171
go bound (F.PropForall x phi) = PropForall x <$> go (Set.insert x bound) phi
146172
go bound (F.PropForallN x dom phi) = PropForallN x dom <$> go (Set.insert x bound) phi
173+
go bound (F.PropExists x phi) = PropExists x <$> go (Set.insert x bound) phi
174+
go bound (F.PropExistsN x dom phi) = PropExistsN x dom <$> go (Set.insert x bound) phi
147175

148176
normaliseHomogeneous :: Formula event ty -> Maybe (Formula event ty)
149177
normaliseHomogeneous phi =

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Occurs.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,5 +39,9 @@ occursFormula x (PropForall x' _) | x == x' = False
3939
occursFormula x (PropForall _ phi) = occursFormula x phi
4040
occursFormula x (PropForallN x' _ _) | x == x' = False
4141
occursFormula x (PropForallN _ _ phi) = occursFormula x phi
42+
occursFormula x (PropExists x' _) | x == x' = False
43+
occursFormula x (PropExists _ phi) = occursFormula x phi
44+
occursFormula x (PropExistsN x' _ _) | x == x' = False
45+
occursFormula x (PropExistsN _ _ phi) = occursFormula x phi
4246
occursFormula x (Atom _ is) = foldl' (\acc phi -> acc || occursPropConstraint x phi) False is
4347
occursFormula x (PropEq _ t _) = occursPropTerm x t

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Pretty.hs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,12 @@ prettyFormula (PropForallN x dom phi) lvl = surround lvl Prec.Universe $
114114
"∀" <> "(" <> x <> " ∈ "
115115
<> "{" <> intercalate ", " (fmap prettyPropValue (Set.toList dom)) <> "}"
116116
<> ")" <> ". " <> prettyFormula phi Prec.Universe
117+
prettyFormula (PropExistsN x dom phi) lvl = surround lvl Prec.Universe $
118+
"∃" <> "(" <> x <> " ∈ "
119+
<> "{" <> intercalate ", " (fmap prettyPropValue (Set.toList dom)) <> "}"
120+
<> ")" <> ". " <> prettyFormula phi Prec.Universe
121+
prettyFormula (PropExists x phi) lvl = surround lvl Prec.Universe $
122+
"∃" <> x <> ". " <> prettyFormula phi Prec.Universe
117123
prettyFormula (Atom c is) lvl = surround lvl Prec.Atom $
118124
showT c <> "(" <> prettyPropConstraints (Set.toList is) <> ")"
119125
prettyFormula (PropEq _ t v) lvl = surround lvl Prec.Eq $

0 commit comments

Comments
 (0)