Preserve clause ordering of requires and ensures when internalisig rules in booster

booster/library/Booster/Definition/Base.hs

@@ -72,7 +72,7 @@ emptyKoreDefinition attributes =
 
 data RewriteRule (tag :: k) = RewriteRule
     { lhs, rhs :: Term
-    , requires, ensures :: Set Predicate
+    , requires, ensures :: [Predicate]
     , attributes :: AxiomAttributes
     , computedAttributes :: ComputedAxiomAttributes
     , existentials :: Set Variable
@@ -86,7 +86,7 @@ data Alias = Alias
     { name :: AliasName
     , params :: [Sort]
     , args :: [Variable]
-    , rhs :: Pattern
+    , rhs :: Term
     }
     deriving stock (Eq, Ord, Show, GHC.Generic)
     deriving anyclass (NFData)

booster/library/Booster/Definition/Ceil.hs

@@ -58,7 +58,7 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods ComputeCeilSumm
                         then []
                         else
                             [ "requires"
-                            , Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) $ Set.toList rule.requires
+                            , Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) rule.requires
                             ]
                    )
                 <> [ Pretty.line
@@ -105,7 +105,7 @@ computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attribut
         ns <- noSolver
         (res, _) <- runEquationT def mllvm ns mempty mempty $ do
             lhsCeils <- Set.fromList <$> computeCeil lhs
-            requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
+            requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) requires
             let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList
             rhsCeils <- simplifyCeils =<< (subtractLHSAndRequiresCeils <$> computeCeil rhs)
 

booster/library/Booster/JsonRpc.hs

@@ -58,6 +58,7 @@ import Booster.Pattern.Rewrite (
 import Booster.Pattern.Util (
     freeVariables,
     sortOfPattern,
+    sortOfTerm,
     substituteInPredicate,
     substituteInTerm,
  )
@@ -116,9 +117,9 @@ respond stateVar request =
                                     RpcError.CouldNotVerifyPattern
                                         [ patternErrorToRpcError patternError
                                         ]
-                    Right (pat, substitution, unsupported) -> do
+                    Right (term, preds, ceils, substitution, unsupported) -> do
                         unless (null unsupported) $ do
-                            withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $
+                            withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfTerm term) unsupported) $
                                 logMessage ("ignoring unsupported predicate parts" :: Text)
                         let cutPoints = fromMaybe [] req.cutPointRules
                             terminals = fromMaybe [] req.terminalRules
@@ -133,9 +134,9 @@ respond stateVar request =
                         -- apply the given substitution before doing anything else
                         let substPat =
                                 Pattern
-                                    { term = substituteInTerm substitution pat.term
-                                    , constraints = Set.map (substituteInPredicate substitution) pat.constraints
-                                    , ceilConditions = pat.ceilConditions
+                                    { term = substituteInTerm substitution term
+                                    , constraints = Set.fromList $ map (substituteInPredicate substitution) preds
+                                    , ceilConditions = ceils
                                     }
                             -- remember all variables used in the substitutions
                             substVars =
@@ -280,7 +281,7 @@ respond stateVar request =
                                 withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
                                     logMessage ("ignoring unsupported predicate parts" :: Text)
                             -- apply the given substitution before doing anything else
-                            let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
+                            let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
                             withContext CtxConstraint $
                                 ApplyEquations.simplifyConstraints
                                     def
@@ -295,7 +296,7 @@ respond stateVar request =
                                                         sortOfJson req.state.term
                                                 result =
                                                     map (externalisePredicate predicateSort) newPreds
-                                                        <> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates)
+                                                        <> map (externaliseCeil predicateSort) ps.ceilPredicates
                                                         <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
                                                         <> ps.unsupported
 
@@ -350,10 +351,10 @@ respond stateVar request =
                                                         ( Text.unlines $
                                                             map
                                                                 (renderText . ("#Ceil:" <>) . pretty' @mods)
-                                                                (Set.toList ps.ceilPredicates)
+                                                                ps.ceilPredicates
                                                                 <> map prettyPattern ps.unsupported
                                                         )
-                                        pure (Set.toList ps.boolPredicates, ps.substitution)
+                                        pure (ps.boolPredicates, ps.substitution)
 
                             smtResult <-
                                 if null boolPs && Map.null suppliedSubst

booster/library/Booster/JsonRpc/Utils.hs

@@ -39,7 +39,6 @@ import Booster.Syntax.Json.Internalise
 import Data.Binary.Builder (fromLazyByteString, toLazyByteString)
 import Data.List (intersperse)
 import Data.Map qualified as Map
-import Data.Set qualified as Set
 import Data.Text.Encoding qualified as Text
 import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Types
@@ -252,11 +251,11 @@ diffBy def pat1 pat2 =
                 [ "Conditions:"
                     : fmap
                         (Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated])
-                        (Set.toList ps.boolPredicates)
+                        ps.boolPredicates
                 , "Ceil conditions:"
                     : map
                         (Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated])
-                        (Set.toList ps.ceilPredicates)
+                        ps.ceilPredicates
                 , "Substitutions:"
                     : fmap
                         (Pretty.indent 4)

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -1014,7 +1014,7 @@ applyEquation term rule =
         let ensured =
                 concatMap
                     (splitBoolPredicates . substituteInPredicate matchingSubst)
-                    (Set.toList rule.ensures)
+                    rule.ensures
         ensuredConditions <-
             -- throws if an ensured condition found to be false
             catMaybes

booster/library/Booster/Pattern/Implies.hs

@@ -204,8 +204,8 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                 (Right IsTop{}, _) ->
                     pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly $
                         "The check implication step expects the antecedent term to be function-like."
-                ( Right (IsPattern (existsL, (patL, substitutionL, unsupportedL)))
-                    , Right (IsPattern (existsR, (patR, substitutionR, unsupportedR)))
+                ( Right (IsPattern (existsL, patL, substitutionL, unsupportedL))
+                    , Right (IsPattern (existsR, patR, substitutionR, unsupportedR))
                     ) ->
                         checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR
                 (Right IsPattern{}, Right (IsTop sort)) ->

booster/library/Booster/Pattern/Rewrite.hs

@@ -461,8 +461,7 @@ applyRule pat@Pattern{ceilConditions} rule =
     checkEnsures matchingSubst = do
         -- apply substitution to rule requires
         let ruleEnsures =
-                concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) $
-                    Set.toList rule.ensures
+                concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
         newConstraints <-
             catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures
 

booster/library/Booster/Pattern/Util.hs

@@ -10,6 +10,7 @@ module Booster.Pattern.Util (
     substituteInPredicate,
     modifyVariables,
     modifyVariablesInT,
+    modifyVariablesInP,
     modifyVarName,
     modifyVarNameConcreteness,
     freeVariables,
@@ -107,7 +108,7 @@ modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern
 modifyVariables f p =
     Pattern
         { term = modifyVariablesInT f p.term
-        , constraints = Set.map (coerce $ modifyVariablesInT f) p.constraints
+        , constraints = Set.map (modifyVariablesInP f) p.constraints
         , ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions
         }
 
@@ -116,6 +117,9 @@ modifyVariablesInT f = cata $ \case
     VarF v -> Var (f v)
     other -> embed other
 
+modifyVariablesInP :: (Variable -> Variable) -> Predicate -> Predicate
+modifyVariablesInP = coerce modifyVariablesInT
+
 modifyVarName :: (VarName -> VarName) -> Variable -> Variable
 modifyVarName f v = v{variableName = f v.variableName}
 

booster/library/Booster/SMT/Translate.hs

@@ -188,12 +188,12 @@ equationToSMTLemma equation
         -- if requires empty: just (= (lhs) (rhs))
         -- if requires not empty: (=> (requires) (= (lhs) (rhs)))
         lemmaRaw <-
-            if Set.null equation.requires
+            if null equation.requires
                 then pure equationRaw
                 else do
                     smtPremise <-
                         foldl1 SMT.and
-                            <$> mapM (translateTerm . \(Predicate t) -> t) (Set.toList equation.requires)
+                            <$> mapM (translateTerm . \(Predicate t) -> t) equation.requires
                     pure $ SMT.implies smtPremise equationRaw
         -- NB ensures has no SMT implications (single shot sat-check)
 
@@ -247,13 +247,13 @@ equationToSMTLemma equation
                     ( pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.lhs)
                         <> " == "
                         <> pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.rhs)
-                        : if Set.null equation.requires
+                        : if null equation.requires
                             then []
                             else
                                 "  requires"
                                     : map
                                         ((Pretty.indent 4 . pretty) . (PrettyWithModifiers @['Decoded, 'Truncated]))
-                                        (Set.toList equation.requires)
+                                        equation.requires
                     )
             lemmaComment = BS.pack (Pretty.renderDefault prettyLemma)
 

booster/library/Booster/Syntax/Json/Internalise.hs

@@ -107,8 +107,8 @@ data InternalisedPredicate
     deriving stock (Eq, Show)
 
 data InternalisedPredicates = InternalisedPredicates
-    { boolPredicates :: Set Internal.Predicate
-    , ceilPredicates :: Set Internal.Ceil
+    { boolPredicates :: [Internal.Predicate]
+    , ceilPredicates :: [Internal.Ceil]
     , substitution :: Map Internal.Variable Internal.Term
     , unsupported :: [Syntax.KorePattern]
     }
@@ -117,8 +117,8 @@ data InternalisedPredicates = InternalisedPredicates
 instance FromModifiersT mods => Pretty (PrettyWithModifiers mods InternalisedPredicates) where
     pretty (PrettyWithModifiers ps) =
         Pretty.vsep $
-            ("Bool predicates: " : map (pretty' @mods) (Set.toList ps.boolPredicates))
-                <> ("Ceil predicates: " : map (pretty' @mods) (Set.toList ps.ceilPredicates))
+            ("Bool predicates: " : map (pretty' @mods) ps.boolPredicates)
+                <> ("Ceil predicates: " : map (pretty' @mods) ps.ceilPredicates)
                 <> ( "Substitution: "
                         : map
                             (\(v, t) -> pretty' @mods v Pretty.<+> "->" Pretty.<+> pretty' @mods t)
@@ -145,7 +145,14 @@ internalisePattern ::
     Maybe [Syntax.Id] ->
     KoreDefinition ->
     Syntax.KorePattern ->
-    Except PatternError (Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
+    Except
+        PatternError
+        ( Internal.Term
+        , [Internal.Predicate]
+        , [Internal.Ceil]
+        , Map Internal.Variable Internal.Term
+        , [Syntax.KorePattern]
+        )
 internalisePattern allowAlias checkSubsorts sortVars definition p = do
     (terms, predicates) <- partitionM isTermM $ explodeAnd p
 
@@ -157,11 +164,9 @@ internalisePattern allowAlias checkSubsorts sortVars definition p = do
     internalPs <-
         internalisePredicates allowAlias checkSubsorts sortVars definition predicates
     pure
-        ( Internal.Pattern
-            { term
-            , constraints = internalPs.boolPredicates
-            , ceilConditions = Set.toList internalPs.ceilPredicates
-            }
+        ( term
+        , internalPs.boolPredicates
+        , internalPs.ceilPredicates
         , internalPs.substitution
         , internalPs.unsupported
         )
@@ -196,7 +201,7 @@ internalisePatternOrTopOrBottom ::
     Except
         PatternError
         ( PatternOrTopOrBottom
-            ([Internal.Variable], (Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern]))
+            ([Internal.Variable], Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
         )
 internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition existentials p = do
     let exploded = explodeAnd p
@@ -210,7 +215,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
                     variableSort <- lookupInternalSort sortVars definition.sorts p sort
                     let variableName = textToBS var.getId
                     pure $ Internal.Variable{variableSort, variableName}
-                IsPattern . (existentialVars,) <$> internalisePattern allowAlias checkSubsorts sortVars definition p
+                (term, preds, ceilConditions, subst, unknown) <-
+                    internalisePattern allowAlias checkSubsorts sortVars definition p
+                pure $
+                    IsPattern
+                        ( existentialVars
+                        , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions}
+                        , subst
+                        , unknown
+                        )
   where
     isTop = \case
         [Syntax.KJTop{sort}] -> Just $ IsTop sort
@@ -234,9 +247,13 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa
         internalisePredicates allowAlias checkSubsorts sortVars definition [syntaxPatt]
     )
         <|> ( withExcept (: []) $ do
-                (pat, substitution, unsupported) <-
+                (term, constrs, ceilConditions, substitution, unsupported) <-
                     internalisePattern allowAlias checkSubsorts sortVars definition syntaxPatt
-                pure $ TermAndPredicates pat substitution unsupported
+                pure $
+                    TermAndPredicates
+                        Internal.Pattern{term, constraints = Set.fromList constrs, ceilConditions}
+                        substitution
+                        unsupported
             )
 
 lookupInternalSort ::
@@ -412,8 +429,8 @@ internalisePredicates allowAlias checkSubsorts sortVars definition ps = do
 
     pure
         InternalisedPredicates
-            { boolPredicates = Set.fromList $ [p | BoolPred p <- internalised] <> moreEquations
-            , ceilPredicates = Set.fromList $ [p | CeilPred p <- internalised]
+            { boolPredicates = [p | BoolPred p <- internalised] <> moreEquations
+            , ceilPredicates = [p | CeilPred p <- internalised]
             , substitution
             , unsupported = [p | UnsupportedPred p <- internalised]
             }
@@ -682,6 +699,8 @@ data PatternError
     | UnknownSymbol Syntax.Id Syntax.KorePattern
     | MacroOrAliasSymbolNotAllowed Syntax.Id Syntax.KorePattern
     | SubstitutionNotAllowed
+    | PredicateNotAllowed
+    | CeilNotAllowed
     | IncorrectSymbolArity Syntax.KorePattern Syntax.Id Int Int
     deriving stock (Eq, Show)
 
@@ -715,6 +734,8 @@ patternErrorToRpcError = \case
     MacroOrAliasSymbolNotAllowed sym p ->
         wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p
     SubstitutionNotAllowed -> RpcError.ErrorOnly "Substitution predicates are not allowed here"
+    PredicateNotAllowed -> RpcError.ErrorOnly "Predicates are not allowed here"
+    CeilNotAllowed -> RpcError.ErrorOnly "Ceil predicates are not allowed here"
     IncorrectSymbolArity p s expected got ->
         wrap
             ( "Inconsistent pattern. Symbol '"
@@ -740,6 +761,8 @@ logPatternError = \case
     UnknownSymbol sym p -> withKorePatternContext p $ logMessage $ "Unknown symbol '" <> Syntax.getId sym <> "'"
     MacroOrAliasSymbolNotAllowed sym p -> withKorePatternContext p $ logMessage $ "Symbol '" <> Syntax.getId sym <> "' is a macro/alias"
     SubstitutionNotAllowed -> logMessage ("Substitution predicates are not allowed here" :: Text)
+    PredicateNotAllowed -> logMessage ("Predicates are not allowed here" :: Text)
+    CeilNotAllowed -> logMessage ("Ceil predicates are not allowed here" :: Text)
     IncorrectSymbolArity p s expected got ->
         withKorePatternContext p $
             logMessage $