diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 85172ffbcc..48460a1c7b 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -47,7 +47,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..)) import Booster.LLVM as LLVM (API) import Booster.Log import Booster.Pattern.ApplyEquations qualified as ApplyEquations -import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable) +import Booster.Pattern.Base (Pattern (..), Predicate (..), Sort (SortApp), Term, Variable) import Booster.Pattern.Base qualified as Pattern import Booster.Pattern.Bool (pattern TrueBool) import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms) @@ -609,11 +609,14 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.Branching , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing , nextStates = - Just $ - map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $ - toList nexts + -- FIXME return _ruleSubst in the response, removing '#'s from the variable names to make pyk happy + Just + $ map + ( \(_, muid, p', mrulePred, _ruleSubst) -> toExecState p' originalSubstitution unsupported (Just muid) mrulePred Nothing + ) + $ toList nexts , rule = Nothing , unknownPredicate = Nothing } @@ -624,7 +627,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.Stuck , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -636,7 +639,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.Vacuous , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -648,8 +651,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.CutPointRule , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing - , nextStates = Just [toExecState next originalSubstitution unsupported Nothing] + , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing + , nextStates = Just [toExecState next originalSubstitution unsupported Nothing Nothing Nothing] , rule = Just lbl , unknownPredicate = Nothing } @@ -660,7 +663,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.TerminalRule , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing , nextStates = Nothing , rule = Just lbl , unknownPredicate = Nothing @@ -672,7 +675,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.DepthBound , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -689,7 +692,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of (logSuccessfulRewrites, logFailedRewrites) (RewriteStepFailed failure) in logs <|> abortRewriteLog - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -712,19 +715,32 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of xs@(_ : _) -> Just xs toExecState :: - Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState -toExecState pat sub unsupported muid = + Pattern -> + Map Variable Term -> + [Syntax.KorePattern] -> + Maybe UniqueId -> + Maybe Predicate -> + Maybe (Map Variable Term) -> + RpcTypes.ExecuteState +toExecState pat sub unsupported muid mrulePredicate mruleSubst = RpcTypes.ExecuteState { term = addHeader t , predicate = addHeader <$> addUnsupported p , substitution = addHeader <$> s - , ruleSubstitution = Nothing - , rulePredicate = Nothing + , ruleSubstitution = addHeader <$> mruleSubstExt + , rulePredicate = addHeader <$> mrulePredExt , ruleId = getUniqueId <$> muid } where + mrulePredExt = externalisePredicate termSort <$> mrulePredicate + mruleSubstExt = + Syntax.KJAnd predicateSort + . map (uncurry $ externaliseSubstitution predicateSort) + . Map.toList + <$> mruleSubst (t, p, s) = externalisePattern pat sub termSort = externaliseSort $ sortOfPattern pat + predicateSort = externaliseSort Pattern.SortBool allUnsupported = Syntax.KJAnd termSort unsupported addUnsupported | null unsupported = id diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs index 417a080f01..a14d36c5b1 100644 --- a/booster/library/Booster/JsonRpc/Utils.hs +++ b/booster/library/Booster/JsonRpc/Utils.hs @@ -70,15 +70,19 @@ diffJson file1 file2 = -- \| Branching execution results are considered equivalent if -- \* they both have two branches -- \* branches are syntactically the same, but may be in different order + -- \* the "rule-substitution" field is ignored sameModuloBranchOrder :: ExecuteResult -> ExecuteResult -> Bool sameModuloBranchOrder res1 res2 | res1.reason == Branching && res1.reason == res2.reason = - case (res1.nextStates, res2.nextStates) of + case (map ignoreRuleSubstituiton <$> res1.nextStates, map ignoreRuleSubstituiton <$> res2.nextStates) of (Just xs, Just ys) -> length xs == 2 && length ys == 2 && (xs == ys || xs == reverse ys) _ -> False | otherwise = False + ignoreRuleSubstituiton :: ExecuteState -> ExecuteState + ignoreRuleSubstituiton state = state{ruleSubstitution = Nothing} + data DiffResult = Identical KoreRpcType | DifferentType KoreRpcType KoreRpcType diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index ca5fee67b1..fcc926aa45 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -833,99 +833,14 @@ applyEquation term rule = map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $ Map.toList subst ) - - -- instantiate the requires clause with the obtained substitution - let required = - concatMap - (splitBoolPredicates . coerce . substituteInTerm subst . coerce) - rule.requires - -- If the required condition is _syntactically_ present in - -- the prior (known constraints), we don't check it. - knownPredicates <- (.predicates) <$> lift getState - toCheck <- lift $ filterOutKnownConstraints knownPredicates required - - -- check the filtered requires clause conditions - unclearConditions <- - catMaybes - <$> mapM - ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) - ) - toCheck - - -- unclear conditions may have been simplified and - -- could now be syntactically present in the path constraints, filter again - stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions - - solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig - - -- check any conditions that are still unclear with the SMT solver - -- (or abort if no solver is being used), abort if still unclear after - unless (null stillUnclear) $ - let checkWithSmt :: SMT.SMTContext -> EquationT io (Maybe Bool) - checkWithSmt smt = - SMT.checkPredicates smt knownPredicates mempty (Set.fromList stillUnclear) >>= \case - Left SMT.SMTSolverUnknown{} -> do - pure Nothing - Left other -> - liftIO $ Exception.throw other - Right result -> - pure result - in lift (checkWithSmt solver) >>= \case - Nothing -> do - -- no solver or still unclear: abort - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ - renderOneLineText - ( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear) - ) - , IndeterminateCondition stillUnclear - ) - Just False -> do - -- actually false given path condition: fail - let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ - renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP) - , ConditionFalse failedP - ) - Just True -> do - -- can proceed - pure () + -- check required constraints from lhs. + -- Reaction on false/indeterminate varies depending on the equation's type (function/simplification), + -- see @handleSimplificationEquation@ and @handleFunctionEquation@ + checkRequires subst -- check ensured conditions, filter any -- true ones, prune if any is false - let ensured = - concatMap - (splitBoolPredicates . substituteInPredicate subst) - (Set.toList rule.ensures) - ensuredConditions <- - -- throws if an ensured condition found to be false - catMaybes - <$> mapM - ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p) - ) - ensured - -- check all ensured conditions together with the path condition - lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case - Right (Just False) -> do - let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $ - renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures) - , EnsuresFalse falseEnsures - ) - Right _other -> - pure () - Left SMT.SMTSolverUnknown{} -> - pure () - Left other -> - liftIO $ Exception.throw other + ensuredConditions <- checkEnsures subst lift $ pushConstraints $ Set.fromList ensuredConditions -- when a new path condition is added, invalidate the equation cache unless (null ensuredConditions) $ do @@ -1021,6 +936,116 @@ applyEquation term rule = check $ Map.lookup Variable{variableSort = SortApp sortName [], variableName} subst + checkRequires :: + Substitution -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + () + checkRequires matchingSubst = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + -- instantiate the requires clause with the obtained substitution + let required = + concatMap + (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) + rule.requires + -- If the required condition is _syntactically_ present in + -- the prior (known constraints), we don't check it. + knownPredicates <- (.predicates) <$> lift getState + toCheck <- lift $ filterOutKnownConstraints knownPredicates required + + -- check the filtered requires clause conditions + unclearConditions <- + catMaybes + <$> mapM + ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) + ) + toCheck + + -- unclear conditions may have been simplified and + -- could now be syntactically present in the path constraints, filter again + stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions + + solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig + + -- check any conditions that are still unclear with the SMT solver + -- (or abort if no solver is being used), abort if still unclear after + unless (null stillUnclear) $ + let checkWithSmt :: SMT.SMTContext -> EquationT io (Maybe Bool) + checkWithSmt smt = + SMT.checkPredicates smt knownPredicates mempty (Set.fromList stillUnclear) >>= \case + Left SMT.SMTSolverUnknown{} -> do + pure Nothing + Left other -> + liftIO $ Exception.throw other + Right result -> + pure result + in lift (checkWithSmt solver) >>= \case + Nothing -> do + -- no solver or still unclear: abort + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ + renderOneLineText + ( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear) + ) + , IndeterminateCondition stillUnclear + ) + Just False -> do + -- actually false given path condition: fail + let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ + renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP) + , ConditionFalse failedP + ) + Just True -> do + -- can proceed + pure () + + checkEnsures :: + Substitution -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + [Predicate] + checkEnsures matchingSubst = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + let ensured = + concatMap + (splitBoolPredicates . substituteInPredicate matchingSubst) + (Set.toList rule.ensures) + ensuredConditions <- + -- throws if an ensured condition found to be false + catMaybes + <$> mapM + ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p) + ) + ensured + -- check all ensured conditions together with the path condition + knownPredicates <- (.predicates) <$> lift getState + solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig + lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case + Right (Just False) -> do + let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $ + renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures) + , EnsuresFalse falseEnsures + ) + Right _other -> + pure () + Left SMT.SMTSolverUnknown{} -> + pure () + Left other -> + liftIO $ Exception.throw other + pure ensuredConditions + -------------------------------------------------------------------- {- Simplification for boolean predicates diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index 39dd2cacc3..c1672f3671 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/booster/library/Booster/Pattern/Bool.hs @@ -7,9 +7,11 @@ License : BSD-3-Clause module Booster.Pattern.Bool ( foldAndBool, isBottom, + isFalse, negateBool, splitBoolPredicates, splitAndBools, + collapseAndBools, -- patterns pattern TrueBool, pattern FalseBool, @@ -189,6 +191,11 @@ foldAndBool (x : xs) = AndBool x $ foldAndBool xs isBottom :: Pattern -> Bool isBottom = (Predicate FalseBool `elem`) . constraints +isFalse :: Predicate -> Bool +isFalse = \case + (Predicate FalseBool) -> True + _ -> False + {- | We want to break apart predicates of type `Y1 andBool ... Yn` apart, in case some of the `Y`s are abstract which prevents the original expression from being fed to the LLVM simplifyBool function -} @@ -206,3 +213,7 @@ splitAndBools :: Predicate -> [Predicate] splitAndBools p@(Predicate t) | AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r] | otherwise = [p] + +-- | Inverse of splitAndBools +collapseAndBools :: [Predicate] -> Predicate +collapseAndBools = Predicate . foldAndBool . map (\(Predicate p) -> p) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 8e30383f97..4f00ce8a02 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -1,8 +1,10 @@ {-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Redundant <$>" #-} {- | Copyright : (c) Runtime Verification, 2022 @@ -13,6 +15,7 @@ module Booster.Pattern.Rewrite ( rewriteStep, RewriteConfig (..), RewriteFailed (..), + RewriteStepResult (..), RewriteResult (..), RewriteTrace (..), pattern CollectRewriteTraces, @@ -23,14 +26,13 @@ module Booster.Pattern.Rewrite ( import Control.Applicative ((<|>)) import Control.Exception qualified as Exception (throw) import Control.Monad -import Control.Monad.Extra (whenJust) import Control.Monad.IO.Class (MonadIO (..)) import Control.Monad.Trans.Class import Control.Monad.Trans.Except import Control.Monad.Trans.Reader (ReaderT (..), ask, asks, withReaderT) import Control.Monad.Trans.State.Strict (StateT (runStateT), get, modify) import Data.Aeson (object, (.=)) -import Data.Bifunctor (bimap) +import Data.Bifunctor (bimap, first) import Data.Coerce (coerce) import Data.Data (Proxy) import Data.Hashable qualified as Hashable @@ -38,12 +40,13 @@ import Data.List (intersperse, partition) import Data.List.NonEmpty (NonEmpty (..), toList) import Data.List.NonEmpty qualified as NE import Data.Map qualified as Map -import Data.Maybe (catMaybes, fromMaybe) +import Data.Maybe (catMaybes, fromMaybe, mapMaybe) import Data.Sequence (Seq, (|>)) import Data.Set qualified as Set -import Data.Text as Text (Text, pack) +import Data.Text as Text (Text, intercalate, pack) import Numeric.Natural import Prettyprinter +import Unsafe.Coerce (unsafeCoerce) import Booster.Definition.Attributes.Base import Booster.Definition.Base @@ -64,6 +67,7 @@ import Booster.Pattern.Match ( MatchResult (MatchFailed, MatchIndeterminate, MatchSuccess), MatchType (Rewrite), SortError, + Substitution, matchTerms, ) import Booster.Pattern.Pretty @@ -75,7 +79,10 @@ import Booster.Util (Flag (..)) newtype RewriteT io a = RewriteT { unRewriteT :: - ReaderT RewriteConfig (StateT SimplifierCache (ExceptT (RewriteFailed "Rewrite") io)) a + ReaderT + RewriteConfig + (StateT (SimplifierCache, Set.Set Predicate) (ExceptT (RewriteFailed "Rewrite") io)) + a } deriving newtype (Functor, Applicative, Monad, MonadIO) @@ -107,17 +114,36 @@ pattern NoCollectRewriteTraces = Flag False runRewriteT :: RewriteConfig -> SimplifierCache -> + Set.Set Predicate -> RewriteT io a -> - io (Either (RewriteFailed "Rewrite") (a, SimplifierCache)) -runRewriteT rewriteConfig cache = - runExceptT . flip runStateT cache . flip runReaderT rewriteConfig . unRewriteT + io (Either (RewriteFailed "Rewrite") (a, (SimplifierCache, Set.Set Predicate))) +runRewriteT rewriteConfig cache remainders m = do + runExceptT + . flip runStateT (cache, remainders) + . flip runReaderT rewriteConfig + . unRewriteT + $ m throw :: LoggerMIO io => RewriteFailed "Rewrite" -> RewriteT io a throw = RewriteT . lift . lift . throwE -getDefinition :: LoggerMIO io => RewriteT io KoreDefinition +getConfig :: Monad m => RewriteT m RewriteConfig +getConfig = RewriteT ask + +getDefinition :: Monad m => RewriteT m KoreDefinition getDefinition = RewriteT $ definition <$> ask +getSolver :: Monad m => RewriteT m SMT.SMTContext +getSolver = RewriteT $ (.smtSolver) <$> ask + +getRemainder :: Monad m => RewriteT m (Set.Set Predicate) +getRemainder = RewriteT $ snd <$> lift get + +setRemainder :: Monad m => Set.Set Predicate -> RewriteT m () +setRemainder r = RewriteT $ lift $ modify $ \(cache, _) -> (cache, r) + +data RewriteStepResult a = OnlyTrivial | AppliedRules a deriving (Eq, Show, Functor) + {- | Performs a rewrite step (using suitable rewrite rules from the definition). @@ -127,11 +153,9 @@ getDefinition = RewriteT $ definition <$> ask -} rewriteStep :: LoggerMIO io => - [Text] -> - [Text] -> Pattern -> - RewriteT io (RewriteResult Pattern) -rewriteStep cutLabels terminalLabels pat = do + RewriteT io (RewriteStepResult [(RewriteRule "Rewrite", Pattern, Substitution)]) +rewriteStep pat = do def <- getDefinition let getIndex = if null def.attributes.indexCells @@ -147,114 +171,97 @@ rewriteStep cutLabels terminalLabels pat = do -- process one priority group at a time (descending priority), -- until a result is obtained or the entire rewrite fails. - processGroups pat rules + filterOutTrivial <$> processGroups rules where + -- return `OnlyTrivial` if all elements of a list are `(r, Nothing)`. If the list is empty or contains at least one `(r, Just p)`, + -- return an `AppliedRules` list of `(r, p)` pairs. + filterOutTrivial :: + [(RewriteRule "Rewrite", Maybe (Pattern, Substitution))] -> + RewriteStepResult [(RewriteRule "Rewrite", Pattern, Substitution)] + filterOutTrivial = \case + [] -> AppliedRules [] + [(_, Nothing)] -> OnlyTrivial + (_, Nothing) : xs -> filterOutTrivial xs + (rule, Just (p, subst)) : xs -> AppliedRules $ (rule, p, subst) : mapMaybe (\(r, mp) -> (\(x, y) -> (r, x, y)) <$> mp) xs + processGroups :: LoggerMIO io => - Pattern -> [[RewriteRule "Rewrite"]] -> - RewriteT io (RewriteResult Pattern) - processGroups pattr [] = - pure $ RewriteStuck pattr - processGroups pattr (rules : rest) = do + RewriteT io [(RewriteRule "Rewrite", Maybe (Pattern, Substitution))] + processGroups [] = pure [] + processGroups (rules : lowerPriorityRules) = do + withContext CtxDetail $ logMessage ("Trying rules at priority " <> show (ruleGroupPriority rules)) -- try all rules of the priority group. This will immediately -- fail the rewrite if anything is uncertain (unification, -- definedness, rule conditions) - results <- filter (/= NotApplied) <$> mapM (applyRule pattr) rules - - -- simplify and filter out bottom states - - -- At the moment, there is no point in calling simplify on the conditions of the - -- resulting patterns again, since we already pruned any rule applications - -- which resulted in one of the conditions being bottom. - -- Also, our current simplifier cannot deduce bottom from a combination of conditions, - -- so unless the original pattern contained bottom, we won't gain anything from - -- calling the simplifier on the original conditions which came with the term. - - let labelOf = fromMaybe "" . (.ruleLabel) . (.attributes) - ruleLabelOrLocT = renderOneLineText . ruleLabelOrLoc - uniqueId = (.uniqueId) . (.attributes) - - case results of - -- no rules in this group were applicable - [] -> processGroups pattr rest - _ -> case concatMap (\case Applied x -> [x]; _ -> []) results of - [] -> - -- all remaining branches are trivial, i.e. rules which did apply had an ensures condition which evaluated to false - -- if, all the other groups only generate a not applicable or trivial rewrites, - -- then we return a `RewriteTrivial`. - processGroups pattr rest >>= \case - RewriteStuck{} -> pure $ RewriteTrivial pat - other -> pure other - -- all branches but one were either not applied or trivial - [(r, x)] - | labelOf r `elem` cutLabels -> - pure $ RewriteCutPoint (labelOf r) (uniqueId r) pat x - | labelOf r `elem` terminalLabels -> - pure $ RewriteTerminal (labelOf r) (uniqueId r) x - | otherwise -> - pure $ RewriteFinished (Just $ ruleLabelOrLocT r) (Just $ uniqueId r) x - -- at this point, there were some Applied rules and potentially some Trivial ones. - -- here, we just return all the applied rules in a `RewriteBranch` - rxs -> - pure $ - RewriteBranch pat $ - NE.fromList $ - map (\(r, p) -> (ruleLabelOrLocT r, uniqueId r, p)) rxs - -data RewriteRuleAppResult a - = Applied a - | NotApplied - | Trivial - deriving (Show, Eq, Functor) - -newtype RewriteRuleAppT m a = RewriteRuleAppT {runRewriteRuleAppT :: m (RewriteRuleAppResult a)} - deriving (Functor) - -instance Monad m => Applicative (RewriteRuleAppT m) where - pure = RewriteRuleAppT . return . Applied - {-# INLINE pure #-} - mf <*> mx = RewriteRuleAppT $ do - mb_f <- runRewriteRuleAppT mf - case mb_f of - NotApplied -> return NotApplied - Trivial -> return Trivial - Applied f -> do - mb_x <- runRewriteRuleAppT mx - case mb_x of - NotApplied -> return NotApplied - Trivial -> return Trivial - Applied x -> return (Applied (f x)) - {-# INLINE (<*>) #-} - m *> k = m >> k - {-# INLINE (*>) #-} - -instance Monad m => Monad (RewriteRuleAppT m) where - return = pure - {-# INLINE return #-} - x >>= f = RewriteRuleAppT $ do - v <- runRewriteRuleAppT x - case v of - Applied y -> runRewriteRuleAppT (f y) - NotApplied -> return NotApplied - Trivial -> return Trivial - {-# INLINE (>>=) #-} - -instance MonadTrans RewriteRuleAppT where - lift :: Monad m => m a -> RewriteRuleAppT m a - lift = RewriteRuleAppT . fmap Applied - {-# INLINE lift #-} - -instance Monad m => MonadFail (RewriteRuleAppT m) where - fail _ = RewriteRuleAppT (return NotApplied) - {-# INLINE fail #-} - -instance MonadIO m => MonadIO (RewriteRuleAppT m) where - liftIO = lift . liftIO - {-# INLINE liftIO #-} - -instance LoggerMIO m => LoggerMIO (RewriteRuleAppT m) where - withLogger l (RewriteRuleAppT m) = RewriteRuleAppT $ withLogger l m + currentRemainder <- getRemainder + results <- + catMaybes + <$> mapM + (\r -> (fmap (r,)) <$> applyRule pat{constraints = pat.constraints <> currentRemainder} r) + rules + + let nonTrivialResultsWithPartialRemainders = + foldr + ( \(rule, mRes) accRes -> case mRes of + Nothing -> accRes + Just res -> (rule, res) : accRes + ) + mempty + results + -- compute remainder condition here from @nonTrivialResults@ and the remainder up to now. + -- If the new remainder is bottom, then no lower priority rules apply + newRemainder = + currentRemainder + <> Set.fromList (mapMaybe ((\(_, r, _) -> r) . snd) nonTrivialResultsWithPartialRemainders) + resultsWithoutRemainders = map (fmap (fmap (\(p, _, s) -> (p, s)))) results + setRemainder newRemainder + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + withContext CtxRemainder $ logPretty' @mods (collapseAndBools . Set.toList $ newRemainder) + + case resultsWithoutRemainders of + [] -> do + -- proceed to lower priority rules if we have not applied any rules at this priority level + processGroups lowerPriorityRules + _xs -> do + if any isFalse newRemainder -- no need to call SMT if any of the conditions is trivially false + then do + setRemainder mempty + pure resultsWithoutRemainders + else do + solver <- getSolver + SMT.isSat solver (pat.constraints <> newRemainder) >>= \case + Right False -> do + -- the remainder condition is unsatisfiable: no need to consider the remainder branch. + setRemainder mempty + withContext CtxRemainder $ logMessage ("remainder is UNSAT" :: Text) + pure resultsWithoutRemainders + Right True -> do + withContext CtxRemainder $ logMessage ("remainder is SAT" :: Text) + -- the remainder condition is satisfiable. + -- Have to construct the remainder branch and consider it + -- To construct the "remainder pattern", + -- we add the remainder condition to the predicates of the @pattr@ + (resultsWithoutRemainders <>) <$> processGroups lowerPriorityRules + Left SMT.SMTSolverUnknown{} -> do + withContext CtxRemainder $ logMessage ("remainder is UNKNWON" :: Text) + -- solver cannot solve the remainder. Descend into the remainder branch anyway + (resultsWithoutRemainders <>) <$> processGroups lowerPriorityRules + Left other -> liftIO $ Exception.throw other -- fail hard on other SMT errors + +ruleGroupPriority :: [RewriteRule a] -> Maybe Priority +ruleGroupPriority = \case + [] -> Nothing + (rule : _) -> Just rule.attributes.priority + +type RewriteRuleAppT m a = ExceptT (Maybe ()) m a + +returnTrivial, returnNotApplied :: Monad m => RewriteRuleAppT m a +returnTrivial = throwE $ Just () +returnNotApplied = throwE Nothing + +runRewriteRuleAppT :: Monad m => RewriteRuleAppT m a -> m (Maybe (Maybe a)) +runRewriteRuleAppT = fmap (either (maybe Nothing (const $ Just Nothing)) (Just . Just)) . runExceptT {- | Tries to apply one rewrite rule: @@ -272,7 +279,7 @@ applyRule :: LoggerMIO io => Pattern -> RewriteRule "Rewrite" -> - RewriteT io (RewriteRuleAppResult (RewriteRule "Rewrite", Pattern)) + RewriteT io (Maybe (Maybe (Pattern, Maybe Predicate, Substitution))) applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRuleAppT $ @@ -285,23 +292,13 @@ applyRule pat@Pattern{ceilConditions} rule = withContext CtxError $ logPretty' @mods sortError failRewrite $ RewriteSortError rule pat.term sortError MatchFailed err@ArgLengthsDiffer{} -> do - withContext CtxError $ - logPretty' @mods err + withContext CtxError $ logPretty' @mods err failRewrite $ InternalMatchError $ renderText $ pretty' @mods err MatchFailed reason -> do withContext CtxFailure $ logPretty' @mods reason - fail "Rule matching failed" + returnNotApplied MatchIndeterminate remainder -> do - withContext CtxIndeterminate $ - logMessage $ - WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ - renderOneLineText $ - "Uncertain about match with rule. Remainder:" - <+> ( hsep $ - punctuate comma $ - map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ - NE.toList remainder - ) + withContext CtxIndeterminate $ logIndeterminateMatch remainder failRewrite $ RuleApplicationUnclear rule pat.term remainder MatchSuccess substitution -> do withContext CtxSuccess $ do @@ -335,78 +332,19 @@ applyRule pat@Pattern{ceilConditions} rule = pat rule.computedAttributes.notPreservesDefinednessReasons - -- apply substitution to rule requires constraints and simplify (one by one - -- in isolation). Stop if false, abort rewrite if indeterminate. - let ruleRequires = - concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) rule.requires - notAppliedIfBottom = RewriteRuleAppT $ pure NotApplied - -- filter out any predicates known to be _syntactically_ present in the known prior - let prior = pat.constraints - toCheck <- lift $ filterOutKnownConstraints prior ruleRequires - - unclearRequires <- - catMaybes <$> mapM (checkConstraint id notAppliedIfBottom prior) toCheck - - -- unclear conditions may have been simplified and - -- could now be syntactically present in the path constraints, filter again - stillUnclear <- lift $ filterOutKnownConstraints prior unclearRequires - - -- check unclear requires-clauses in the context of known constraints (prior) - solver <- lift $ RewriteT $ (.smtSolver) <$> ask - - let smtUnclear = do - withContext CtxConstraint . withContext CtxAbort . logMessage $ - WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $ - renderOneLineText $ - "Uncertain about condition(s) in a rule:" - <+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear) - failRewrite $ - RuleConditionUnclear rule . coerce . foldl1 AndTerm $ - map coerce stillUnclear - - checkAllRequires <- - SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear) - - case checkAllRequires of - Left SMT.SMTSolverUnknown{} -> - smtUnclear -- abort rewrite if a solver result was Unknown - Left other -> - liftIO $ Exception.throw other -- fail hard on other SMT errors - Right (Just False) -> do - -- requires is actually false given the prior - withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) - RewriteRuleAppT $ pure NotApplied - Right (Just True) -> - pure () -- can proceed - Right Nothing -> - smtUnclear -- no implication could be determined + -- check required constraints from lhs: Stop if any is false, + -- add as remainders if indeterminate. + unclearRequiresAfterSmt <- checkRequires subst -- check ensures constraints (new) from rhs: stop and return `Trivial` if -- any are false, remove all that are trivially true, return the rest - let ruleEnsures = - concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) $ - Set.toList rule.ensures - trivialIfBottom = RewriteRuleAppT $ pure Trivial - newConstraints <- - catMaybes <$> mapM (checkConstraint id trivialIfBottom prior) ruleEnsures - - -- check all new constraints together with the known side constraints - (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case - Right (Just False) -> do - withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) - RewriteRuleAppT $ pure Trivial - Right _other -> - pure () - Left SMT.SMTSolverUnknown{} -> - pure () - Left other -> - liftIO $ Exception.throw other + newConstraints <- checkEnsures subst -- if a new constraint is going to be added, the equation cache is invalid unless (null newConstraints) $ do withContextFor Equations . logMessage $ ("New path condition ensured, invalidating cache" :: Text) - lift . RewriteT . lift . modify $ \s -> s{equations = mempty} + lift . RewriteT . lift . modify $ first (\s -> s{equations = mempty}) -- existential variables may be present in rule.rhs and rule.ensures, -- need to strip prefixes and freshen their names with respect to variables already @@ -420,10 +358,10 @@ applyRule pat@Pattern{ceilConditions} rule = (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) rule.existentials - -- modify the substitution to include the existentials - let substWithExistentials = subst `Map.union` existentialSubst + -- modify the substitution to include the existentials + substWithExistentials = subst `Map.union` existentialSubst - let rewritten = + rewritten = Pattern (substituteInTerm substWithExistentials rule.rhs) -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables @@ -431,9 +369,14 @@ applyRule pat@Pattern{ceilConditions} rule = <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints) ) ceilConditions - withContext CtxSuccess $ - withPatternContext rewritten $ - return (rule, rewritten) + withContext CtxSuccess $ do + case unclearRequiresAfterSmt of + [] -> withPatternContext rewritten $ pure (rewritten, Just $ Predicate FalseBool, subst) + _ -> + let rewritten' = rewritten{constraints = rewritten.constraints <> Set.fromList unclearRequiresAfterSmt} + in withPatternContext rewritten' $ + pure + (rewritten', Just $ Predicate $ NotBool $ coerce $ collapseAndBools unclearRequiresAfterSmt, subst) where filterOutKnownConstraints :: Set.Set Predicate -> [Predicate] -> RewriteT io [Predicate] filterOutKnownConstraints priorKnowledge constraitns = do @@ -451,25 +394,94 @@ applyRule pat@Pattern{ceilConditions} rule = failRewrite = lift . (throw) checkConstraint :: - (Predicate -> a) -> - RewriteRuleAppT (RewriteT io) (Maybe a) -> + RewriteRuleAppT (RewriteT io) (Maybe Predicate) -> Set.Set Predicate -> Predicate -> - RewriteRuleAppT (RewriteT io) (Maybe a) - checkConstraint onUnclear onBottom knownPredicates p = do - RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask - oldCache <- lift . RewriteT . lift $ get + RewriteRuleAppT (RewriteT io) (Maybe Predicate) + checkConstraint onBottom knownPredicates p = do + RewriteConfig{definition, llvmApi, smtSolver} <- lift getConfig + (oldCache, _) <- lift . RewriteT . lift $ get (simplified, cache) <- withContext CtxConstraint $ simplifyConstraint definition llvmApi smtSolver oldCache knownPredicates p -- update cache - lift . RewriteT . lift . modify $ const cache + lift . RewriteT . lift . modify $ \(_, rems) -> (cache, rems) case simplified of Right (Predicate FalseBool) -> onBottom Right (Predicate TrueBool) -> pure Nothing - Right other -> pure $ Just $ onUnclear other + Right other -> pure $ Just other Left UndefinedTerm{} -> onBottom - Left _ -> pure $ Just $ onUnclear p + Left _ -> pure $ Just p + + checkRequires :: + Substitution -> RewriteRuleAppT (RewriteT io) [Predicate] + checkRequires matchingSubst = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + -- apply substitution to rule requires constraints and simplify (one by one + -- in isolation). Stop if false, abort rewrite if indeterminate. + let ruleRequires = + concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires + -- filter out any predicates known to be _syntactically_ present in the known prior + let prior = pat.constraints + toCheck <- lift $ filterOutKnownConstraints prior ruleRequires + + unclearRequires <- + catMaybes <$> mapM (checkConstraint returnNotApplied prior) toCheck + + -- unclear conditions may have been simplified and + -- could now be syntactically present in the path constraints, filter again + stillUnclear <- lift $ filterOutKnownConstraints prior unclearRequires + + -- check unclear requires-clauses in the context of known constraints (prior) + solver <- lift $ RewriteT $ (.smtSolver) <$> ask + + checkAllRequires <- + SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear) + + case checkAllRequires of + Left SMT.SMTSolverUnknown{} -> do + withContext CtxConstraint . logMessage . renderOneLineText $ + "Uncertain about condition(s) in a rule, SMT returned unknown, adding as remainder:" + <+> (hsep . punctuate comma . map (pretty' @mods) $ unclearRequires) + pure unclearRequires + Left other -> + liftIO $ Exception.throw other -- fail hard on other SMT errors + Right (Just False) -> do + -- requires is actually false given the prior + withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) + returnNotApplied + Right (Just True) -> + pure [] -- can proceed + Right Nothing -> do + withContext CtxConstraint . logMessage . renderOneLineText $ + "Uncertain about condition(s) in a rule, adding as remainder:" + <+> (hsep . punctuate comma . map (pretty' @mods) $ unclearRequires) + pure unclearRequires + + checkEnsures :: + Substitution -> RewriteRuleAppT (RewriteT io) [Predicate] + checkEnsures matchingSubst = do + let prior = pat.constraints + solver <- lift $ RewriteT $ (.smtSolver) <$> ask + let ruleEnsures = + concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) $ + Set.toList rule.ensures + newConstraints <- + catMaybes <$> mapM (checkConstraint returnTrivial prior) ruleEnsures + + -- check all new constraints together with the known side constraints + (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case + Right (Just False) -> do + withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) + -- it's probably still fine to return trivial here even if we assumed unclear required conditions + returnTrivial + Right _other -> + pure () + Left SMT.SMTSolverUnknown{} -> + pure () + Left other -> + liftIO $ Exception.throw other + pure newConstraints {- | Reason why a rewrite did not produce a result. Contains additional information for logging what happened during the rewrite. @@ -543,7 +555,7 @@ ruleLabelOrLoc rule = -- | Different rewrite results (returned from RPC execute endpoint) data RewriteResult pat = -- | branch point - RewriteBranch pat (NonEmpty (Text, UniqueId, pat)) + RewriteBranch pat (NonEmpty (Text, UniqueId, pat, Maybe Predicate, Substitution)) | -- | no rules could be applied, config is stuck RewriteStuck pat | -- | cut point rule, return current (lhs) and single next state @@ -630,6 +642,28 @@ mkDiffTerms = \case in (SymbolApplication s1 ss1 xs', SymbolApplication s2 ss2 ys') r -> r +data MaybeSimplified (isSimplified :: Bool) a where + Simplified :: a -> MaybeSimplified 'True a + Unsimplified :: a -> MaybeSimplified 'False a + Bottom :: a -> MaybeSimplified 'True a + +instance Functor (MaybeSimplified 'True) where + fmap f = \case + Simplified a -> Simplified $ f a + Bottom a -> Bottom $ f a + +unMaybeSimplified :: MaybeSimplified isSimplified a -> a +unMaybeSimplified = \case + Simplified a -> unsafeCoerce a + Unsimplified a -> unsafeCoerce a + Bottom a -> unsafeCoerce a + +catSimplified :: [MaybeSimplified 'True a] -> [a] +catSimplified = \case + [] -> [] + Bottom{} : xs -> catSimplified xs + (Simplified x) : xs -> x : catSimplified xs + {- | Interface for RPC execute: Rewrite given term as long as there is exactly one result in each step. @@ -706,9 +740,9 @@ performRewrite :: RewriteConfig -> Pattern -> io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) -performRewrite rewriteConfig pat = do +performRewrite rewriteConfig initialPattern = do (rr, RewriteStepsState{counter, traces}) <- - flip runStateT rewriteStart $ doSteps False pat + flip runStateT rewriteStart $ doSteps (Unsimplified initialPattern) pure (counter, traces, rr) where RewriteConfig @@ -740,179 +774,177 @@ performRewrite rewriteConfig pat = do updateCache simplifierCache = modify $ \rss -> rss{simplifierCache} - simplifyP :: Pattern -> StateT RewriteStepsState io (Maybe Pattern) - simplifyP p = withContext CtxSimplify $ do - st <- get - let cache = st.simplifierCache - evaluatePattern definition llvmApi smtSolver cache p >>= \(res, newCache) -> do - updateCache newCache - case res of - Right newPattern -> do - emitRewriteTrace $ RewriteSimplified Nothing - pure $ Just newPattern - Left r@SideConditionFalse{} -> do - emitRewriteTrace $ RewriteSimplified (Just r) - pure Nothing - Left r@UndefinedTerm{} -> do - emitRewriteTrace $ RewriteSimplified (Just r) - pure Nothing - Left other -> do - emitRewriteTrace $ RewriteSimplified (Just other) - pure $ Just p - - -- Results may change when simplification prunes a false side - -- condition, otherwise this would mainly be fmap simplifyP - simplifyResult :: - Pattern -> - RewriteResult Pattern -> - StateT RewriteStepsState io (RewriteResult Pattern) - simplifyResult orig = \case - RewriteBranch p nexts -> do - simplifyP p >>= \case - Nothing -> pure $ RewriteTrivial orig - Just p' -> do - let simplifyP3rd (a, b, c) = - fmap (a,b,) <$> simplifyP c - nexts' <- catMaybes <$> mapM simplifyP3rd (toList nexts) - pure $ case nexts' of - -- The `[]` case should be `Stuck` not `Trivial`, because `RewriteTrivial p'` - -- means the pattern `p'` is bottom, but we know that is not the case here. - [] -> RewriteStuck p' - [(lbl, uId, n)] -> RewriteFinished (Just lbl) (Just uId) n - ns -> RewriteBranch p' $ NE.fromList ns - r@RewriteStuck{} -> pure r - r@RewriteTrivial{} -> pure r - RewriteCutPoint lbl uId p next -> do - simplifyP p >>= \case - Nothing -> pure $ RewriteTrivial orig - Just p' -> do - next' <- simplifyP next - pure $ case next' of - Nothing -> RewriteTrivial next - Just n -> RewriteCutPoint lbl uId p' n - RewriteTerminal lbl uId p -> - maybe (RewriteTrivial orig) (RewriteTerminal lbl uId) <$> simplifyP p - RewriteFinished lbl uId p -> - maybe (RewriteTrivial orig) (RewriteFinished lbl uId) <$> simplifyP p - RewriteAborted reason p -> - maybe (RewriteTrivial orig) (RewriteAborted reason) <$> simplifyP p + simplify :: + MaybeSimplified flag Pattern -> StateT RewriteStepsState io (MaybeSimplified 'True Pattern) + simplify = \case + Simplified p -> pure $ Simplified p + Bottom p -> pure $ Bottom p + Unsimplified p -> withPatternContext p $ withContext CtxSimplify $ do + st <- get + let cache = st.simplifierCache + evaluatePattern definition llvmApi smtSolver cache p >>= \(res, newCache) -> do + updateCache newCache + case res of + Right newPattern -> do + emitRewriteTrace $ RewriteSimplified Nothing + pure $ Simplified newPattern + Left r@SideConditionFalse{} -> do + emitRewriteTrace $ RewriteSimplified (Just r) + pure $ Bottom p + Left r@UndefinedTerm{} -> do + emitRewriteTrace $ RewriteSimplified (Just r) + pure $ Bottom p + Left other -> do + emitRewriteTrace $ RewriteSimplified (Just other) + pure $ Simplified p + + labelOf = fromMaybe "" . (.ruleLabel) . (.attributes) + ruleLabelOrLocT = renderOneLineText . ruleLabelOrLoc + uniqueId = (.uniqueId) . (.attributes) doSteps :: - Bool -> Pattern -> StateT RewriteStepsState io (RewriteResult Pattern) - doSteps wasSimplified pat' = do + MaybeSimplified flag Pattern -> StateT RewriteStepsState io (RewriteResult Pattern) + doSteps pat | unWrappedPat <- unMaybeSimplified pat = do RewriteStepsState{counter, simplifierCache} <- get logDepth $ showCounter counter if | depthReached counter -> do logDepth $ "Reached maximum depth of " <> maybe "?" showCounter mbMaxDepth - (if wasSimplified then pure else simplifyResult pat') $ RewriteFinished Nothing Nothing pat' - | shouldSimplifyAt counter && not wasSimplified -> do + simplify pat >>= \case + Bottom pat' -> pure $ RewriteTrivial pat' + Simplified pat' -> pure $ RewriteFinished Nothing Nothing pat' + | shouldSimplifyAt counter -> do logDepth $ "Interim simplification after " <> maybe "??" showCounter mbSimplify - simplifyP pat' >>= \case - Nothing -> pure $ RewriteTrivial pat' - Just newPat -> doSteps True newPat + simplify pat >>= \case + Bottom pat' -> pure $ RewriteTrivial pat' + Simplified pat' -> pure $ RewriteFinished Nothing Nothing pat' | otherwise -> runRewriteT rewriteConfig simplifierCache - (withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat') + mempty + (withPatternContext unWrappedPat $ rewriteStep unWrappedPat) >>= \case - Right (RewriteFinished mlbl mUniqueId single, cache) -> do - whenJust mlbl $ \lbl -> - whenJust mUniqueId $ \uniqueId -> - emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single - updateCache cache - incrementCounter - doSteps False single - Right (terminal@(RewriteTerminal lbl uniqueId single), _cache) -> withPatternContext pat' $ do - emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single - incrementCounter - simplifyResult pat' terminal - Right (branching@RewriteBranch{}, cache) -> do - logMessage $ "Stopped due to branching after " <> showCounter counter - updateCache cache - simplified <- withPatternContext pat' $ simplifyResult pat' branching - case simplified of - RewriteStuck{} -> withPatternContext pat' $ do - logMessage ("Rewrite stuck after pruning branches" :: Text) - pure simplified - RewriteTrivial{} -> withPatternContext pat' $ do - logMessage $ "Simplified to bottom after " <> showCounter counter - pure simplified - RewriteFinished mlbl mUniqueId single -> do - logMessage ("All but one branch pruned, continuing" :: Text) - whenJust mlbl $ \lbl -> - whenJust mUniqueId $ \uniqueId -> - emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single - incrementCounter - doSteps False single - RewriteBranch pat'' branches -> withPatternContext pat' $ do - emitRewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _) -> (lbl, uid)) branches - pure simplified - _other -> withPatternContext pat' $ error "simplifyResult: Unexpected return value" - Right (cutPoint@(RewriteCutPoint lbl _ _ _), _) -> withPatternContext pat' $ do - simplified <- simplifyResult pat' cutPoint - case simplified of - RewriteCutPoint{} -> - logMessage $ "Cut point " <> lbl <> " after " <> showCounter counter - RewriteStuck{} -> - logMessage $ "Stuck after " <> showCounter counter - RewriteTrivial{} -> - logMessage $ "Simplified to bottom after " <> showCounter counter - _other -> error "simplifyResult: Unexpected return value" - pure simplified - Right (stuck@RewriteStuck{}, cache) -> do - logMessage $ "Stopped after " <> showCounter counter - updateCache cache - emitRewriteTrace $ RewriteStepFailed $ NoApplicableRules pat' - if wasSimplified - then pure stuck - else withSimplified pat' "Retrying with simplified pattern" (doSteps True) - Right (trivial@RewriteTrivial{}, _) -> withPatternContext pat' $ do - logMessage $ "Simplified to bottom after " <> showCounter counter - pure trivial - Right (aborted@RewriteAborted{}, _) -> withPatternContext pat' $ do - logMessage $ "Aborted after " <> showCounter counter - simplifyResult pat' aborted - -- if unification was unclear and the pattern was - -- unsimplified, simplify and retry rewriting once - Left failure@(RuleApplicationUnclear rule _ remainder) - | not wasSimplified -> do - emitRewriteTrace $ RewriteStepFailed failure - withSimplified pat' "Retrying with simplified pattern" (doSteps True) - | otherwise -> do - -- was already simplified, emit an abort log entry - withRuleContext rule . withContext CtxMatch . withContext CtxAbort $ - getPrettyModifiers >>= \case - ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> - logMessage $ - WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ - renderOneLineText $ - "Uncertain about match with rule. Remainder:" - <+> ( hsep $ - punctuate comma $ - map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ - NE.toList remainder - ) - emitRewriteTrace $ RewriteStepFailed failure - logMessage $ "Aborted after " <> showCounter counter - pure (RewriteAborted failure pat') + Left failure@(RuleApplicationUnclear rule _ remainder) -> + case pat of + Simplified pat' -> do + -- was already simplified, emit an abort log entry + withRuleContext rule . withContext CtxMatch . withContext CtxAbort $ logIndeterminateMatch remainder + logMessage ("Aborted after " <> showCounter counter) >> pure (RewriteAborted failure pat') + _ -> + simplify pat >>= \case + -- We are stuck here not trivial because we didn't apply a single rule + Bottom pat' -> logMessage ("Rewrite stuck after simplification." :: Text) >> pure (RewriteStuck pat') + pat'@Simplified{} -> logMessage ("Retrying with simplified pattern" :: Text) >> doSteps pat' Left failure -> do emitRewriteTrace $ RewriteStepFailed failure - let msg = "Aborted after " <> showCounter counter - if wasSimplified - then logMessage msg >> pure (RewriteAborted failure pat') - else withSimplified pat' msg (pure . RewriteAborted failure) - where - withSimplified p msg cont = do - (withPatternContext p $ simplifyP p) >>= \case - Nothing -> do - logMessage ("Rewrite stuck after simplification." :: Text) - pure $ RewriteStuck p - Just simplifiedPat -> do - logMessage msg - cont simplifiedPat + case pat of + Simplified pat' -> logMessage ("Aborted after " <> showCounter counter) >> pure (RewriteAborted failure pat') + _ -> + simplify pat >>= \case + -- We are stuck here not trivial because we didn't apply a single rule + Bottom pat' -> logMessage ("Rewrite stuck after simplification." :: Text) >> pure (RewriteStuck pat') + Simplified pat' -> logMessage ("Aborted after " <> showCounter counter) >> pure (RewriteAborted failure pat') + -- We may want to return the remainder as a new field in the execute response, as the remainder + -- may not be empty, which would indicate a "hole" in the semantics that the user should be aware of. + Right (appliedRules, (cache, remainderPredicates)) -> + updateCache cache >> case appliedRules of + OnlyTrivial -> do + -- all rule applications were trivial + -- by definition that means we couldn't have had any remainders, so we can just return trivial + logMessage $ "Simplified to bottom after " <> showCounter counter + pure $ RewriteTrivial unWrappedPat + AppliedRules [] -> do + -- no rules applied. + -- We return stuck if the term had already been simplified in a previous step + logMessage $ "Stopped after " <> showCounter counter + emitRewriteTrace $ RewriteStepFailed $ NoApplicableRules unWrappedPat + case pat of + Simplified pat' -> pure $ RewriteStuck pat' + _ -> + simplify pat >>= \case + Bottom pat' -> + -- We are stuck here not trivial because we didn't apply a single rule + logMessage ("Rewrite stuck after simplification." :: Text) >> pure (RewriteStuck pat') + pat'@Simplified{} -> logMessage ("Retrying with simplified pattern" :: Text) >> doSteps pat' + AppliedRules [(rule, nextPat, _subst)] -- applied single rule + -- cut-point rule, stop + | labelOf rule `elem` cutLabels -> do + simplify pat >>= \case + Bottom pat' -> do + logMessage $ "Previous state found to be bottom after " <> showCounter counter + pure $ RewriteTrivial pat' + Simplified pat' -> + simplify (Unsimplified nextPat) >>= \case + Bottom nextPat' -> do + logMessage $ "Simplified to bottom after " <> showCounter counter + pure $ RewriteTrivial nextPat' + Simplified nextPat' -> do + logMessage $ "Cut point " <> (labelOf rule) <> " after " <> showCounter counter + pure $ RewriteCutPoint (labelOf rule) (uniqueId rule) pat' nextPat' + | labelOf rule `elem` terminalLabels -> do + -- terminal rule, stop + emitRewriteTrace $ RewriteSingleStep (labelOf rule) (uniqueId rule) unWrappedPat nextPat + simplify (Unsimplified nextPat) >>= \case + Bottom nextPat' -> do + logMessage $ "Simplified to bottom after " <> showCounter counter + pure $ RewriteTrivial nextPat' + Simplified nextPat' -> do + logMessage $ "Terminal " <> (labelOf rule) <> " after " <> showCounter counter + incrementCounter + pure $ RewriteTerminal (labelOf rule) (uniqueId rule) nextPat' + | otherwise -> do + -- any other rule, go on + emitRewriteTrace $ RewriteSingleStep (labelOf rule) (uniqueId rule) unWrappedPat nextPat + incrementCounter + doSteps (Unsimplified nextPat) + AppliedRules nextPats -> do + -- applied multiple rules + logMessage $ "Stopped due to branching after " <> showCounter counter + simplify pat >>= \case + Bottom pat' -> do + logMessage $ "Previous state found to be bottom after " <> showCounter counter + pure $ RewriteTrivial pat' + Simplified pat' -> + ( catSimplified + <$> mapM (\(r, nextPat, subst) -> fmap (r,,subst) <$> simplify (Unsimplified nextPat)) nextPats + ) + >>= \case + [] -> withPatternContext pat' $ do + logMessage ("Rewrite trivial after pruning all branches" :: Text) + pure $ RewriteTrivial pat' + [(rule, nextPat', _subst)] -> withPatternContext pat' $ do + logMessage ("All but one branch pruned, continuing" :: Text) + emitRewriteTrace $ RewriteSingleStep (labelOf rule) (uniqueId rule) pat' nextPat' + incrementCounter + doSteps (Simplified nextPat') + nextPats' -> do + emitRewriteTrace $ + RewriteBranchingStep pat' $ + NE.fromList $ + map (\(rule, _, _subst) -> (ruleLabelOrLocT rule, uniqueId rule)) nextPats' + unless (Set.null remainderPredicates) $ do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + withContext CtxRemainder . withContext CtxDetail $ + logMessage + ( ("Uncovered remainder branch after rewriting with rules " :: Text) + <> ( Text.intercalate ", " $ map (\(r, _, _subst) -> getUniqueId $ uniqueId r) nextPats' + ) + ) + pure $ + RewriteBranch pat' $ + NE.fromList $ + map + ( \(r, n, subst) -> + ( ruleLabelOrLocT r + , uniqueId r + , n + , mkRulePredicate r subst + , subst + ) + ) + nextPats' data RewriteStepsState = RewriteStepsState { counter :: !Natural @@ -927,3 +959,28 @@ rewriteStart = , traces = mempty , simplifierCache = mempty } + +{- | Instantiate a rewrite rule's requires clause with a substitution. + Returns Nothing is the resulting @Predicate@ is trivially @True@. +-} +mkRulePredicate :: RewriteRule a -> Substitution -> Maybe Predicate +mkRulePredicate rule subst = + case concatMap + (splitBoolPredicates . coerce . substituteInTerm subst . coerce) + rule.requires of + [] -> Nothing + xs -> Just $ collapseAndBools xs + +logIndeterminateMatch :: forall io. LoggerMIO io => NonEmpty (Term, Term) -> io () +logIndeterminateMatch remainder = + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + logMessage $ + WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ + renderOneLineText $ + "Uncertain about match with rule. Remainder:" + <+> ( hsep $ + punctuate comma $ + map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ + NE.toList remainder + ) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index d88a8b06f5..8a79563f19 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -15,6 +15,7 @@ module Booster.SMT.Interface ( finaliseSolver, getModelFor, checkPredicates, + isSat, hardResetSolver, ) where @@ -493,3 +494,65 @@ checkPredicates ctxt givenPs givenSubst psToCheck "Given ∧ P and Given ∧ !P interpreted as " <> pack (show (positive', negative')) pure (positive', negative') + +isSat :: + forall io. + Log.LoggerMIO io => + SMT.SMTContext -> + Set Predicate -> + io (Either SMTError Bool) +isSat ctxt psToCheck + | null psToCheck = pure . Right $ True + | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do + Log.withContext Log.CtxAbort $ Log.logMessage $ "SMT translation error: " <> errMsg + pure . Left . SMTTranslationError $ errMsg + | Right (smtToCheck, transState) <- translated = Log.withContext Log.CtxSMT $ do + evalSMT ctxt . runExceptT $ solve smtToCheck transState + where + translated :: Either Text ([DeclareCommand], TranslationState) + translated = + SMT.runTranslator $ + mapM (\(Predicate p) -> Assert (mkComment p) <$> SMT.translateTerm p) $ + Set.toList psToCheck + + solve smtToCheck transState = solve' + where + solve' = do + lift $ hardResetSolver ctxt.options + Log.getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + Log.logMessage . Pretty.renderOneLineText $ + hsep ("Predicates to check for SAT:" : map (pretty' @mods) (Set.toList psToCheck)) + lift $ declareVariables transState + mapM_ smtRun smtToCheck + smtRun CheckSat >>= \case + Sat -> pure True + Unsat -> pure False + Unknown _ -> retry + other -> do + let msg = "Unexpected result while calling 'check-sat': " <> show other + Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg + throwSMT' msg + + retry = do + opts <- lift . SMT $ gets (.options) + case opts.retryLimit of + Just x | x > 0 -> do + let newOpts = opts{timeout = 2 * opts.timeout, retryLimit = Just $ x - 1} + lift $ hardResetSolver newOpts + Log.logMessage ("Retrying with higher timeout" :: Text) + solve' + _ -> failBecauseUnknown + + failBecauseUnknown :: ExceptT SMTError (SMT io) Bool + failBecauseUnknown = + smtRun GetReasonUnknown >>= \case + Unknown reason -> do + Log.withContext Log.CtxAbort $ + Log.logMessage $ + "Returned Unknown. Reason: " <> show reason + throwE $ SMTSolverUnknown reason mempty psToCheck + other -> do + let msg = "Unexpected result while calling ':reason-unknown': " <> show other + Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg + throwSMT' msg diff --git a/booster/test/rpc-integration/resources/remainder-predicates.k b/booster/test/rpc-integration/resources/remainder-predicates.k new file mode 100644 index 0000000000..c3ccd20256 --- /dev/null +++ b/booster/test/rpc-integration/resources/remainder-predicates.k @@ -0,0 +1,169 @@ +module REMAINDER-PREDICATES + imports INT + imports BOOL + + syntax State ::= test1Init() + | test1State1() + | test1State2() + | test1State3() + + | test2Init() + | test2State1() + | test2State2() + | test2State3() + + | test3Init() + | test3State1() + | test3State2() + | test3State3() + + | test4Init() + | test4State1() + | test4State2() + | test4State3() + | test4State4() + + | test5Init() + | test5State1() + | test5State2() + | test5State3() + | test5State4() + | test5State5() + + | test6Init() + | test6State1() + | test6State2() + | test6State3() + | test6State4() + | test6State5() + + configuration $PGM:State ~> .K + 0:Int + + //////////////////////////////////////////////////////////////////////////////// + /// two rules apply with UNSAT remainder predicate, no further rules apply. // + /// Results in 2 branches. // + //////////////////////////////////////////////////////////////////////////////// + rule [test1-init]: test1Init() => test1State1() ... + _ => ?_X + + rule [test1-1-2]: test1State1() => test1State2() ... + X + requires X >Int 0 + + rule [test1-1-3]: test1State1() => test1State3() ... + X + requires X <=Int 0 + + //////////////////////////////////////////////////////////////////////////////// + /// two rules apply with SAT remainder predicate, // + /// have to consider the remainder branch where X ==Int 0, // + /// no further rules apply. // + /// Results in 2 branches. // + //////////////////////////////////////////////////////////////////////////////// + rule [test2-init]: test2Init() => test2State1() ... + _ => ?_X + + rule [test2-1-2]: test2State1() => test2State2() ... + X + requires X >Int 0 + + rule [test2-1-3]: test2State1() => test2State3() ... + X + requires X test3Init() => test3State1() ... + _ => ?_X + + rule [test3-1-2]: test3State1() => test3State2() ... + X + requires X >Int 0 + + rule [test3-1-3]: test3State1() => test3State3() ... + X + requires X test4Init() => test4State1() ... + _ => ?_X + + rule [test4-1-2]: test4State1() => test4State2() ... + X + requires X >Int 0 + [priority(49)] + + rule [test4-1-3]: test4State1() => test4State3() ... + X + requires X test4State1() => test4State4() ... + X + requires X ==Int 0 + + + //////////////////////////////////////////////////////////////////////////////// + /// two hight-priorty rules apply with SAT remainder predicate, // + /// have to consider the remainder branch where X ==Int 0, // + /// one rule at a lower priority applies unconditionally, which means that // + /// that the remainder is False. Rule test5-1-5 is unreachable. // + /// Results in 3 branches. // + //////////////////////////////////////////////////////////////////////////////// + rule [test5-init]: test5Init() => test5State1() ... + _ => ?_X + + rule [test5-1-2]: test5State1() => test5State2() ... + X + requires X >Int 0 [priority(48)] + + rule [test5-1-3]: test5State1() => test5State3() ... + X + requires X test5State1() => test5State4() ... + [priority(49)] + + rule [test5-1-5]: test5State1() => test5State5() ... + X + requires X ==Int 0 + + //////////////////////////////////////////////////////////////////////////////// + /// two hight-priorty rules apply with SAT remainder predicate, // + /// have to consider the remainder branch where X ==Int 0, // + /// two rule at a lower priority applies unconditionally. // + /// Results in 4 branches. // + //////////////////////////////////////////////////////////////////////////////// + rule [test6-init]: test6Init() => test6State1() ... + _ => ?_X + + rule [test6-1-2]: test6State1() => test6State2() ... + X + requires X >Int 0 [priority(48)] + + rule [test6-1-3]: test6State1() => test6State3() ... + X + requires X test6State1() => test6State4() ... + [priority(49)] + + rule [test6-1-5]: test6State1() => test6State5() ... + [priority(49)] + +// to produce input state: +// krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json +// then edit state-test1Init.json to substitute test1State1() for test1Init() + +endmodule diff --git a/booster/test/rpc-integration/resources/remainder-predicates.kompile b/booster/test/rpc-integration/resources/remainder-predicates.kompile new file mode 100755 index 0000000000..9caac778f2 --- /dev/null +++ b/booster/test/rpc-integration/resources/remainder-predicates.kompile @@ -0,0 +1,4 @@ +echo "kompiling remainder-predicates.k" +kompile --backend haskell remainder-predicates.k +cp remainder-predicates-kompiled/definition.kore remainder-predicates.kore +rm -r remainder-predicates-kompiled \ No newline at end of file diff --git a/booster/test/rpc-integration/resources/use-path-condition-in-equations.k b/booster/test/rpc-integration/resources/use-path-condition-in-equations.k index c3b72a17bc..1236039912 100644 --- a/booster/test/rpc-integration/resources/use-path-condition-in-equations.k +++ b/booster/test/rpc-integration/resources/use-path-condition-in-equations.k @@ -10,17 +10,29 @@ module USE-PATH-CONDITION-IN-EQUATIONS | test2State1() | test2State2() + | test3Init() + | test3State1() + | test3State2() + + | test4Init() + | test4State1() + | test4State2() + | test4State3() + syntax Int ::= test1F ( Int ) [function, total, no-evaluators] | test2F ( Int ) [function, total, no-evaluators] + | test3F ( Int ) [function, total] + | test4F ( Int ) [function, total] configuration $PGM:State ~> .K 0:Int //////////////////////////////////////////////////////////////////////////////// // Here the simplification's side condition is syntactically present // - // in the path condition and is not checked. // - // Result: Stuck at depth 2 in state test1State2() // - // after applying rules test1-init,test1-1-2 // + // in the path condition and is not checked. // + // Result // + // Stuck at depth 2 in state test1State2() // + // after applying rules test1-init,test1-1-2 // //////////////////////////////////////////////////////////////////////////////// rule [test1-init]: test1Init() => test1State1() ... _ => ?X @@ -33,8 +45,7 @@ module USE-PATH-CONDITION-IN-EQUATIONS rule [test1F-simplify]: test1F(X:Int) => X requires X ==Int 42 [simplification] //////////////////////////////////////////////////////////////////////////////// - // Here the simplification's side condition is implied by the path condition, // - // but we need an SMT solver to establish that. // + // Here the simplification's side condition is implied by the path condition. // // Result: Stuck at depth 2 in state test2State2(), // // after applying rules test2-init, test2-1-2. // //////////////////////////////////////////////////////////////////////////////// @@ -48,6 +59,47 @@ module USE-PATH-CONDITION-IN-EQUATIONS rule [test2F-simplify]: test2F(X:Int) => X requires X >Int 0 [simplification] + ///////////////////////////////////////////////////////////////////////////////// + // Exactly like test2, but the function now has actual evaluators, rather than // + // a simplification-based semantics. Using the SMT solver Booster determines // + // that the condition of rule test3-1-2 is False. // + // Result kore-rpc-booster: // + // Stuck at depth in state test3State1() // + // after applying rules test3-init . // + ///////////////////////////////////////////////////////////////////////////////// + rule [test3-init]: test3Init() => test3State1() ... + _ => ?X + ensures ?X ==Int 42 + + rule [test3-1-2]: test3State1() => test3State2() ... + X + requires test3F(X) >Int 0 + + rule [test3F-zero-if-x-positive]: test3F(X:Int) => 0 requires X >Int 0 + rule [test3F-one-if-not-x-nonpositive]: test3F(X:Int) => 1 requires X <=Int 0 + + ///////////////////////////////////////////////////////////////////////////////// + // Similar to test3, but now there are two rules. Using the solver, Booster // + // determines that the condition of rule test4-1-2 is False. // + // Result: // + // Stuck at depth 2 in state test2State3() // + ///////////////////////////////////////////////////////////////////////////////// + rule [test4-init]: test4Init() => test4State1() ... + _ => ?X + ensures ?X ==Int 42 + + rule [test4-1-2]: test4State1() => test4State2() ... + X + requires test4F(X) >Int 0 + + rule [test4-1-3]: test4State1() => test4State3() ... + X + requires test4F(X) <=Int 0 + + + rule [test4F-zero-if-x-positive]: test4F(X:Int) => 0 requires X >Int 0 + rule [test4F-one-if-not-x-nonpositive]: test4F(X:Int) => 1 requires X <=Int 0 + // to produce input state: // krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json // then edit state-test1Init.json to substitute test1State1() for test1Init() diff --git a/booster/test/rpc-integration/test-3934-smt/response-008.json b/booster/test/rpc-integration/test-3934-smt/response-008.json index 98e9dca69e..1487dcd8ac 100644 --- a/booster/test/rpc-integration/test-3934-smt/response-008.json +++ b/booster/test/rpc-integration/test-3934-smt/response-008.json @@ -1910,64 +1910,30 @@ "args": [ { "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], + "name": "Lblend", + "sorts": [], "args": [ { "tag": "App", - "name": "Lbl'Hash'gas'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode", - "sorts": [], + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortExceptionalStatusCode", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortStatusCode", + "args": [] + } + ], "args": [ { "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortOpCode", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "64" - } - ] - } - ] + "name": "LblEVMC'Unds'OUT'Unds'OF'Unds'GAS'Unds'NETWORK'Unds'ExceptionalStatusCode", + "sorts": [], + "args": [] } ] } @@ -1996,33 +1962,9 @@ "args": [ { "tag": "App", - "name": "Lbl'Hash'access'LSqBUndsCommUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode'Unds'OpCode", + "name": "Lbl'Hash'gas'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode", "sorts": [], "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortUnStackOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortOpCode", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - } - ] - }, { "tag": "App", "name": "inj", @@ -2090,23 +2032,72 @@ "args": [ { "tag": "App", - "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", + "name": "Lbl'Hash'access'LSqBUndsCommUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode'Unds'OpCode", "sorts": [], "args": [ { "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortUnStackOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortOpCode", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", + "sorts": [], + "args": [] + } + ] }, { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "64" + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInternalOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortOpCode", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", + "sorts": [], + "args": [] + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "64" + } + ] + } + ] } ] } @@ -2135,32 +2126,23 @@ "args": [ { "tag": "App", - "name": "Lblpc", + "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", "sorts": [], "args": [ { "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortUnStackOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortOpCode", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - } - ] + "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", + "sorts": [], + "args": [] + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "64" } ] } @@ -2173,18 +2155,74 @@ "args": [ { "tag": "App", - "name": "Lblexecute", - "sorts": [], - "args": [] + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInternalOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblpc", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortUnStackOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortOpCode", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", + "sorts": [], + "args": [] + } + ] + } + ] + } + ] }, { - "tag": "EVar", - "name": "VarK'Unds'CELL'Unds'de090c3b", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lblexecute", + "sorts": [], + "args": [] + }, + { + "tag": "EVar", + "name": "VarK'Unds'CELL'Unds'de090c3b", + "sort": { + "tag": "SortApp", + "name": "SortK", + "args": [] + } + } + ] } ] } @@ -2551,96 +2589,13 @@ "sorts": [], "args": [ { - "tag": "App", - "name": "Lbl'Unds'-Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarGAS'Unds'AMT", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'Unds'-Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblCmem'LParUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblLONDON'Unds'EVM", - "sorts": [], - "args": [] - }, - { - "tag": "App", - "name": "Lbl'Hash'memoryUsageUpdate'LParUndsCommUndsCommUndsRParUnds'EVM'Unds'Int'Unds'Int'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarMEMORYUSED'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "64" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "32" - } - ] - } - ] - }, - { - "tag": "App", - "name": "LblCmem'LParUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblLONDON'Unds'EVM", - "sorts": [], - "args": [] - }, - { - "tag": "EVar", - "name": "VarMEMORYUSED'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - ] - } - ] + "tag": "EVar", + "name": "VarGAS'Unds'AMT", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } }, { "tag": "DV", @@ -3324,9 +3279,34 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "Lbl'Unds-LT-'Int'Unds'", "sorts": [], "args": [ + { + "tag": "App", + "name": "Lbl'UndsPlus'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarGAS'Unds'AMT", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "-23" + } + ] + }, { "tag": "App", "name": "Lbl'Unds'-Int'Unds'", @@ -3402,31 +3382,6 @@ ] } ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarGAS'Unds'AMT", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "-23" - } - ] } ] } @@ -3843,7 +3798,7 @@ ] } }, - "rule-id": "e80dae2349dc4cf016147f969cff262399d625e3e979474e412b3c14914c4e77", + "rule-id": "a0a224658695b9eeae4eecf43289c46f78c5b34020e5e6ef966eaaf80525eccf", "rule-predicate": { "format": "KORE", "version": 1, @@ -3870,80 +3825,47 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "Lbl'Unds-LT-'Gas'UndsUnds'GAS-SYNTAX'Unds'Bool'Unds'Gas'Unds'Gas", "sorts": [], "args": [ { "tag": "App", - "name": "Lbl'Unds'-Int'Unds'", - "sorts": [], - "args": [ + "name": "inj", + "sorts": [ { - "tag": "App", - "name": "LblCmem'LParUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblLONDON'Unds'EVM", - "sorts": [], - "args": [] - }, - { - "tag": "App", - "name": "Lbl'Hash'memoryUsageUpdate'LParUndsCommUndsCommUndsRParUnds'EVM'Unds'Int'Unds'Int'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarMEMORYUSED'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "64" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "32" - } - ] - } - ] + "tag": "SortApp", + "name": "SortInt", + "args": [] }, + { + "tag": "SortApp", + "name": "SortGas", + "args": [] + } + ], + "args": [ { "tag": "App", - "name": "LblCmem'LParUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int", + "name": "Lbl'UndsPlus'Int'Unds'", "sorts": [], "args": [ - { - "tag": "App", - "name": "LblLONDON'Unds'EVM", - "sorts": [], - "args": [] - }, { "tag": "EVar", - "name": "VarMEMORYUSED'Unds'CELL", + "name": "VarGAS'Unds'AMT", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "-23" } ] } @@ -3951,2678 +3873,876 @@ }, { "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarGAS'Unds'AMT", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, + "name": "inj", + "sorts": [ { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "-23" + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortGas", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbl'Unds'-Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "LblCmem'LParUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "LblLONDON'Unds'EVM", + "sorts": [], + "args": [] + }, + { + "tag": "App", + "name": "Lbl'Hash'memory'LParUndsCommUndsRParUnds'EVM'Unds'Int'Unds'OpCode'Unds'Int", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInternalOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortOpCode", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", + "sorts": [], + "args": [] + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "64" + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarMEMORYUSED'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + ] + }, + { + "tag": "App", + "name": "LblCmem'LParUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "LblLONDON'Unds'EVM", + "sorts": [], + "args": [] + }, + { + "tag": "EVar", + "name": "VarMEMORYUSED'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + ] } ] } ] } } - }, - "rule-substitution": { + } + }, + { + "term": { "format": "KORE", "version": 1, "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "App", + "name": "Lbl'-LT-'kevm'-GT-'", + "sorts": [], + "args": [ { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "App", + "name": "inj", + "sorts": [ { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "SortApp", + "name": "SortInternalOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbl'Hash'gas'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode", + "sorts": [], + "args": [ { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "App", + "name": "inj", + "sorts": [ { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ + "tag": "SortApp", + "name": "SortInternalOp", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortOpCode", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", + "sorts": [], + "args": [] + }, { - "tag": "And", + "tag": "DV", "sort": { "tag": "SortApp", - "name": "SortGeneratedTopCell", + "name": "SortInt", "args": [] }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar0", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarGENERATEDCOUNTER'Unds'CELL'Unds'c84b0b5f", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar2", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "Lbl'Hash'gas'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortOpCode", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "64" - } - ] - } - ] - } - ] - } - ] - }, - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "Lbl'Hash'access'LSqBUndsCommUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode'Unds'OpCode", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortUnStackOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortOpCode", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortOpCode", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "64" - } - ] - } - ] - } - ] - } - ] - }, - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "64" - } - ] - } - ] - }, - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortInternalOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "Lblpc", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortUnStackOp", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortOpCode", - "args": [] - } - ], - "args": [ - { - "tag": "App", - "name": "LblMLOAD'Unds'EVM'Unds'UnStackOp", - "sorts": [], - "args": [] - } - ] - } - ] - } - ] - }, - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblexecute", - "sorts": [], - "args": [] - }, - { - "tag": "EVar", - "name": "VarK'Unds'CELL'Unds'de090c3b", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - } - ] - } - ] - } - ] - } - ] - } - ] - } - } - ] - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortNetworkCell", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar3", - "sort": { - "tag": "SortApp", - "name": "SortNetworkCell", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'-LT-'network'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'chainID'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarCHAINID'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'accounts'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarACCOUNTS'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortAccountCellMap", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'txOrder'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarTXORDER'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortList", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'txPending'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarTXPENDING'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortList", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'messages'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarMESSAGES'Unds'CELL", - "sort": { - "tag": "SortApp", - "name": "SortMessageCellMap", - "args": [] - } - } - ] - } - ] - } - } - ] - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortProgramCell", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'Gen0", - "sort": { - "tag": "SortApp", - "name": "SortProgramCell", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'-LT-'program'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBytes", - "args": [] - }, - "value": "`€`@R4€\u0015a\u0000\u0010W`\u0000€ý[P`\u00046\u0010a\u0001,W`\u00005`à\u001c€c]â/\u0007\u0011a\u0000­W€c¡\u0018á\u0002\u0011a\u0000qW€c¡\u0018á\u0002\u0014a\u0002bW€cºAO¦\u0014a\u0002uW€cÓ\u0013”\r\u0014a\u0002W€cøÌ¿G\u0014a\u0002 W€cúv&Ô\u0014a\u0002³W`\u0000€ý[€c]â/\u0007\u0014a\u0002\u0003W€cm]9ß\u0014a\u0002\u0016W€c~Ž#Ð\u0014a\u0002)W€cˆ~OÛ\u0014a\u0002=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011 accumulatedLogs ) r{ExecuteRequest.state = execStateToKoreJson simplifiedBoosterState} - -- if we stop for a reason in fallbackReasons (default [Aborted, Stuck, Branching], + -- TODO this is an experimental code path. It needs to be guarded with an CLI option before merging + -- if we stop because of branching, simplify the next states to prune them and optionally + -- execute a fallback rewrite step from the pre-state in Kore con confirm the branch + | boosterResult.reason == Branching -> do + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage $ + "Booster " <> displayExecuteResultVerbose boosterResult + prunedBoosterResult <- simplifyExecResult logSettings r._module def boosterResult + case prunedBoosterResult of + Left (_prunedToOneNext, _logs) -> do + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage $ + "After simplification: Booster " + <> displayExecuteResultVerbose boosterResult{nextStates = take 1 <$> boosterResult.nextStates} + Right stillBranching -> + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage $ + "After simplification: Booster " <> displayExecuteResultVerbose stillBranching + + -- -- attempt to do one step in the old backend + -- Booster.Log.withContext CtxProxy $ + -- Booster.Log.logMessage ("Executing fall-back request" :: Text) + -- (koreResult, _kTime) <- + -- Stats.timed $ + -- kore + -- ( Execute + -- r + -- { state = execStateToKoreJson boosterResult.state + -- , maxDepth = Just $ Depth 1 + -- , assumeStateDefined = Just True + -- } + -- ) + -- case koreResult of + -- Right (Execute result) -> + -- Booster.Log.withContext CtxProxy $ + -- Booster.Log.logMessage $ + -- "Kore " <> displayExecuteResultVerbose result + -- _err -> + -- Booster.Log.withContext CtxProxy $ + -- Booster.Log.withContext CtxWarn $ + -- Booster.Log.logMessage ("Kore returned error" :: Text) + -- continue with the pruned Booster's result + case prunedBoosterResult of + Left (nextState, newLogs) -> do + let prunedBoosterBranchStep = 1 + executionLoop + logSettings + def + ( currentDepth + boosterResult.depth + prunedBoosterBranchStep + , time + bTime + , koreTime + , postProcessLogs <$> combineLogs (rpcLogs : boosterResult.logs : newLogs) + ) + r{ExecuteRequest.state = nextState} + Right result -> do + logStats ExecuteM (time + bTime, koreTime) + pure . Right $ + Execute + result + { depth = currentDepth + boosterResult.depth + , logs = postProcessLogs <$> combineLogs [rpcLogs, result.logs] + } + + -- if we stop for a reason in fallbackReasons (default [Aborted, Stuck]), -- revert to the old backend to re-confirm and possibly proceed | boosterResult.reason `elem` cfg.fallbackReasons -> do Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ - Text.pack $ - "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth + "Booster " <> displayExecuteResultVerbose boosterResult -- simplify Booster's state with Kore's simplifier Booster.Log.withContext CtxProxy $ Booster.Log.logMessage ("Simplifying booster state and falling back to Kore" :: Text) @@ -454,17 +516,18 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of -- we were successful with the booster, thus we -- return the booster result with the updated -- depth, in case we previously looped - Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ - "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth + Booster.Log.withContext CtxProxy . Booster.Log.logMessage $ + "Booster " <> displayExecuteResultVerbose boosterResult -- perform post-exec simplification postExecResult <- simplifyExecResult logSettings r._module def boosterResult case postExecResult of - Left (nextState, newLogs) -> + Left (nextState, newLogs) -> do + let prunedBoosterBranchStep = 0 executionLoop logSettings def - ( currentDepth + boosterResult.depth + ( currentDepth + boosterResult.depth + prunedBoosterBranchStep , time + bTime , koreTime , postProcessLogs <$> combineLogs (rpcLogs : boosterResult.logs : newLogs) @@ -520,7 +583,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of -- this ensures the information from next states in a branch reponse doesn't get lost pure $ Right - ( (Booster.toExecState p sub unsup Nothing) + ( (Booster.toExecState p sub unsup Nothing Nothing Nothing) { ruleId = s.ruleId , ruleSubstitution = s.ruleSubstitution , rulePredicate = s.rulePredicate @@ -652,3 +715,6 @@ makeVacuous newLogs execState = , rule = Nothing , logs = combineLogs [execState.logs, newLogs] } + +displayExecuteResultVerbose :: ExecuteResult -> Text +displayExecuteResultVerbose _ = "" diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index 32cbd99e93..7c1c47b5d3 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -454,7 +454,7 @@ clProxyOptionsParser = (eitherReader $ mapM reasonReader . splitOn ",") ( long "fallback-on" <> metavar "REASON1,REASON2..." - <> value [Branching, Stuck, Aborted] + <> value defaultFallbackReasons <> help "Halt reasons for which requests should be re-executed with kore-rpc" <> showDefaultWith (intercalate "," . map show) ) @@ -470,6 +470,8 @@ clProxyOptionsParser = ( long "no-fallback-simplify" <> help "disable simplification before fallback requests" ) + defaultFallbackReasons :: [HaltReason] + defaultFallbackReasons = [Stuck, Aborted] reasonReader :: String -> Either String HaltReason reasonReader = \case diff --git a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs index 3c295c7ebe..f3950287c2 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -223,9 +223,7 @@ errorCases = rewriteSuccess = testCase "con1 app rewrites to f1 app" $ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |] - `rewritesTo` ( "con1-f1" - , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |] - ) + `rewritesTo` [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |] unifyNotMatch = testCase "Stuck case when subject has variables" $ getsStuck @@ -252,35 +250,30 @@ rewriteStuck = rulePriority = testCase "con1 rewrites to a branch when higher priority does not apply" $ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("otherThing") ) ), ConfigVar:SortK{}) ) |] - `branchesTo` [ - ( "con1-f2" - , [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("otherThing"), \dv{SomeSort{}}("otherThing") ) ), ConfigVar:SortK{}) ) |] - ) - , - ( "con1-f1'" - , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("otherThing") ) ), ConfigVar:SortK{}) ) |] - ) + `branchesTo` [ [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("otherThing"), \dv{SomeSort{}}("otherThing") ) ), ConfigVar:SortK{}) ) |] + , [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("otherThing") ) ), ConfigVar:SortK{}) ) |] ] -runWith :: Term -> IO (Either (RewriteFailed "Rewrite") (RewriteResult Pattern)) +runWith :: Term -> IO (Either (RewriteFailed "Rewrite") (RewriteStepResult [Pattern])) runWith t = - second fst <$> do + second (fmap (fmap (\(_, p, _) -> p)) . fst) <$> do conf <- testConf - runNoLoggingT $ runRewriteT conf mempty (rewriteStep [] [] $ Pattern_ t) + runNoLoggingT $ + runRewriteT conf mempty mempty (rewriteStep $ Pattern_ t) -rewritesTo :: Term -> (Text, Term) -> IO () -t1 `rewritesTo` (lbl, t2) = - runWith t1 @?>>= Right (RewriteFinished (Just lbl) (Just mockUniqueId) $ Pattern_ t2) +rewritesTo :: Term -> Term -> IO () +t1 `rewritesTo` t2 = + runWith t1 @?>>= Right (AppliedRules [Pattern_ t2]) getsStuck :: Term -> IO () getsStuck t1 = - runWith t1 @?>>= Right (RewriteStuck $ Pattern_ t1) + runWith t1 @?>>= Right (AppliedRules []) -branchesTo :: Term -> [(Text, Term)] -> IO () +branchesTo :: Term -> [Term] -> IO () t `branchesTo` ts = runWith t @?>>= Right - (RewriteBranch (Pattern_ t) $ NE.fromList $ map (\(lbl, t') -> (lbl, mockUniqueId, Pattern_ t')) ts) + (AppliedRules $ map Pattern_ ts) failsWith :: Term -> RewriteFailed "Rewrite" -> IO () failsWith t err = @@ -304,8 +297,22 @@ aborts failure t = runRewrite t >>= (@?= (0, RewriteAborted failure t)) newtype Steps = Steps Natural rewrites :: Steps -> Term -> t -> (t -> RewriteResult Term) -> IO () -rewrites (Steps n) t t' f = - runRewrite t >>= (@?= (n, f t')) +rewrites (Steps n) t t' f = do + let expected = (n, f t') + actual <- runRewrite t + second withoutRuleSubst actual @?= expected + +mkRewriteBranch :: a -> NE.NonEmpty (Text, UniqueId, a) -> RewriteResult a +mkRewriteBranch pre branches = RewriteBranch pre (fmap withEmptyPredandSubst branches) + where + withEmptyPredandSubst (l, uid, post) = (l, uid, post, Nothing, Map.empty) + +withoutRuleSubst :: RewriteResult a -> RewriteResult a +withoutRuleSubst = \case + RewriteBranch pre branches -> RewriteBranch pre (fmap ignoreRuleSubst branches) + other -> other + where + ignoreRuleSubst (l, uid, post, rulePred, _) = (l, uid, post, rulePred, Map.empty) canRewrite :: TestTree canRewrite = @@ -337,7 +344,7 @@ canRewrite = (Steps 1) [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("otherThing"), \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - (`RewriteBranch` NE.fromList [branch1, branch2]) + (`mkRewriteBranch` NE.fromList [branch1, branch2]) , testCase "Returns stuck when no rules could be applied" $ do rewrites (Steps 0) @@ -431,7 +438,7 @@ supportsDepthControl = (Steps 1) [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("otherThing"), \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - (`RewriteBranch` NE.fromList [branch1, branch2]) + (`mkRewriteBranch` NE.fromList [branch1, branch2]) ] where rewritesToDepth :: MaxDepth -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO () @@ -439,7 +446,7 @@ supportsDepthControl = conf <- testConf (counter, _, res) <- runNoLoggingT $ performRewrite conf{mbMaxDepth = Just depth} $ Pattern_ t - (counter, fmap (.term) res) @?= (n, f t') + (counter, withoutRuleSubst $ fmap (.term) res) @?= (n, f t') supportsCutPoints :: TestTree supportsCutPoints = @@ -484,7 +491,7 @@ supportsCutPoints = (Steps 1) [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("otherThing"), \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |] [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("somethingElse") ) ), C:SortK{}) ) |] - (`RewriteBranch` NE.fromList [branch1, branch2]) + (`mkRewriteBranch` NE.fromList [branch1, branch2]) ] where rewritesToCutPoint :: Text -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO () @@ -494,7 +501,7 @@ supportsCutPoints = runNoLoggingT $ performRewrite conf{cutLabels = [lbl]} $ Pattern_ t - (counter, fmap (.term) res) @?= (n, f t') + (counter, withoutRuleSubst $ fmap (.term) res) @?= (n, f t') supportsTerminalRules :: TestTree supportsTerminalRules = diff --git a/scripts/booster-integration-tests.sh b/scripts/booster-integration-tests.sh index 3a24d3db64..29fc10914c 100755 --- a/scripts/booster-integration-tests.sh +++ b/scripts/booster-integration-tests.sh @@ -37,7 +37,7 @@ for dir in $(ls -d test-*); do SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; - "get-model" | "collectiontest" | "implies" | "implies2" | "implies-issue-3941") + "get-model" | "collectiontest" | "implies" | "implies2" | "implies-issue-3941" | "use-path-condition-in-equations") SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; @@ -49,7 +49,7 @@ for dir in $(ls -d test-*); do SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@ ;; - "use-path-condition-in-equations" | "compute-ceil" | "no-evaluator" | "non-linear-int-requires" | "get-model-subsorts" | "simplify") + "remainder-predicates"| "compute-ceil" | "no-evaluator" | "non-linear-int-requires" | "get-model-subsorts" | "simplify") SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ ;; "log-simplify-json")