Skip to content

Commit

Permalink
Recognise ==Int and ==K equations as substitutions when internalising (…
Browse files Browse the repository at this point in the history 
…#4061)

Booster now recognises predicates of shape `true #Equals (VAR ==Int
<expr>)` and `true #Equals (VAR ==K <expr>)` as substitutions (given the
global scope does not contradict that, i.e., no cycles or multiple
substitutions for the same VAR...).

Currently only matches ==Int and ==K.
We could also match notBool (_ =/=Int _) and notBool (_ =/=K _) (more
magic).

When internalising rules and equations, the substitution must be turned
back into predicates for the `requires` clause. Currently we also turn
back the ensures clause substitutions into predicates (might want to
change that).

Part of #4059
  • Loading branch information
@jberthold
jberthold authored Oct 16, 2024
1 parent 0bfbcff commit 4347105
Show file tree
Hide file tree
Showing 5 changed files with 173 additions and 227 deletions.
38 changes: 36 additions & 2 deletions booster/library/Booster/Syntax/Json/Internalise.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ module Booster.Syntax.Json.Internalise (
textToBS,
trm,
handleBS,
asEquations,
TermOrPredicates (..),
InternalisedPredicates (..),
PatternOrTopOrBottom (..),
Expand Down Expand Up @@ -481,6 +482,10 @@ mkEq x t = Internal.Predicate $ case sortOfTerm t of
Internal.SortBool -> Internal.EqualsBool (Internal.Var x) t
otherSort -> Internal.EqualsK (Internal.KSeq otherSort (Internal.Var x)) (Internal.KSeq otherSort t)

-- | turns a substitution into a list of equations
asEquations :: Map Internal.Variable Internal.Term -> [Internal.Predicate]
asEquations = map (uncurry mkEq) . Map.assocs

internalisePred ::
Flag "alias" ->
Flag "subsorts" ->
Expand Down Expand Up @@ -540,10 +545,12 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
ensureEqualSorts (sortOfTerm a) argS
ensureEqualSorts (sortOfTerm b) argS
case (argS, a, b) of
-- for "true" #Equals P, check whether P is in fact a substitution
(Internal.SortBool, Internal.TrueBool, x) ->
pure [BoolPred $ Internal.Predicate x]
mapM mbSubstitution [x]
(Internal.SortBool, x, Internal.TrueBool) ->
pure [BoolPred $ Internal.Predicate x]
mapM mbSubstitution [x]
-- we could also detect NotBool (NEquals _) in "false" #Equals P
(Internal.SortBool, Internal.FalseBool, x) ->
pure [BoolPred $ Internal.Predicate $ Internal.NotBool x]
(Internal.SortBool, x, Internal.FalseBool) ->
Expand Down Expand Up @@ -600,6 +607,33 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
throwE (IncompatibleSorts (map externaliseSort [s1, s2]))
zipWithM_ go args1 args2

mbSubstitution :: Internal.Term -> Except PatternError InternalisedPredicate
mbSubstitution = \case
eq@(Internal.EqualsInt (Internal.Var x) e)
| x `Set.member` freeVariables e -> pure $ boolPred eq
| otherwise -> pure $ SubstitutionPred x e
eq@(Internal.EqualsInt e (Internal.Var x))
| x `Set.member` freeVariables e -> pure $ boolPred eq
| otherwise -> pure $ SubstitutionPred x e
eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) ->
do
-- NB sorts do not have to agree! (could be subsorts)
pure $
if (x `Set.member` freeVariables e)
then boolPred eq
else SubstitutionPred x e
eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) ->
do
-- NB sorts do not have to agree! (could be subsorts)
pure $
if (x `Set.member` freeVariables e)
then boolPred eq
else SubstitutionPred x e
other ->
pure $ boolPred other

boolPred = BoolPred . Internal.Predicate

----------------------------------------

-- for use with withAssoc
Expand Down
26 changes: 13 additions & 13 deletions booster/library/Booster/Syntax/ParsedKore/Internalise.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -765,6 +765,10 @@ internaliseAxiom (Partial partialDefinition) parsedAxiom =
sortVars
attribs

{- | internalises a pattern and turns its contained substitution into
equations (predicates). Errors if any ceil conditions or
unsupported predicates are found.
-}
internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported ::
KoreDefinition ->
SourceRef ->
Expand All @@ -776,16 +780,16 @@ internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref
(term, preds, ceilConditions, substitution, unsupported) <-
withExcept (DefinitionPatternError ref) $
internalisePattern AllowAlias IgnoreSubsorts maybeVars partialDefinition t
unless (null substitution) $
throwE $
DefinitionPatternError ref SubstitutionNotAllowed
unless (null ceilConditions) $
throwE $
DefinitionPatternError ref CeilNotAllowed
unless (null unsupported) $
throwE $
DefinitionPatternError ref (NotSupported (head unsupported))
pure (Util.modifyVariablesInT f term, map (Util.modifyVariablesInP f) preds)
pure
( Util.modifyVariablesInT f term
, map (Util.modifyVariablesInP f) (preds <> asEquations substitution)
)

internaliseRewriteRuleNoAlias ::
KoreDefinition ->
Expand Down Expand Up @@ -964,12 +968,10 @@ internaliseCeil partialDef left right sortVars attrs = do
internalPs <-
withExcept (DefinitionPatternError (sourceRef attrs)) $
internalisePredicates AllowAlias IgnoreSubsorts (Just sortVars) partialDef [p]
let constraints = internalPs.boolPredicates
substitutions = internalPs.substitution
let
-- turn substitution-like predicates back into equations
constraints = internalPs.boolPredicates <> asEquations internalPs.substitution
unsupported = internalPs.unsupported
unless (null substitutions) $
throwE $
DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed
unless (null unsupported) $
throwE $
DefinitionPatternError (sourceRef attrs) $
Expand Down Expand Up @@ -1005,9 +1007,6 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
withExcept (DefinitionPatternError (sourceRef attrs)) $
internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef $
Syntax.KJAnd leftTerm.sort [leftTerm, requires]
unless (null substitution) $
throwE $
DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed
unless (null ceils) $
throwE $
DefinitionPatternError (sourceRef attrs) CeilNotAllowed
Expand Down Expand Up @@ -1049,7 +1048,8 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
RewriteRule
{ lhs
, rhs
, requires = map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) preds
, requires =
map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) (preds <> asEquations substitution)
, ensures
, attributes
, computedAttributes
Expand Down
2 changes: 2 additions & 0 deletions booster/test/rpc-integration/test-vacuous/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ Rules `init` and `AC` introduce constraints on this variable:

_Expected:_
- The rewrite is stuck with `<k>d</k><int>N</int> \and...(contradiction)`
- The `N` is substituted by value `1` in the final result (booster).
- The result is simplified and discovered to be `vacuous` (with state `d`).
1) _vacuous-but-rewritten_

Expand All @@ -47,6 +48,7 @@ Rules `init` and `AC` introduce constraints on this variable:
_Expected:_
- Rewrite with `BD` (despite the contradiction)
- The rewrite is stuck with `<k>d</k><int>N</int> \and...(contradiction)`
- The `N` is substituted by value `1` in the final result (booster).
- The result is simplified and discovered to be `vacuous` (with state `d`).

With `kore-rpc-dev`, some contradictions will be discovered before or while
Expand Down
167 changes: 61 additions & 106 deletions booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,13 +66,13 @@
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"value": "0"
}
]
},
Expand All @@ -95,119 +95,74 @@
]
}
},
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "And",
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "LblnotBool'Unds'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
]
"value": "true"
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "false"
}
}
}
}
Expand Down
Loading

0 comments on commit 4347105

Please sign in to comment.