runtimeverification · geo2a · Jun 19, 2023 · Jun 26, 2023 · Jun 26, 2023 · Jun 26, 2023
diff --git a/cabal.project b/cabal.project
@@ -1,3 +1,5 @@
+optimization: False
+jobs: 4
 packages: .
 
 index-state: 2023-06-29T00:00:00Z
@@ -7,17 +9,16 @@ allow-newer:
   ghc-trace-events:base,
   ghc-bignum:base
 
-source-repository-package
-    type: git
-    location: https://github.com/co-log/co-log.git
-    tag: v0.5.0.0
-    --sha256: sha256-zs+cQf2bIQEaN10eEg8VJkCp0pQcTuXpUovCev5C6dc=
+-- source-repository-package
+--     type: git
+--     location: https://github.com/co-log/co-log.git
+--     tag: v0.5.0.0
+--     --sha256: sha256-zs+cQf2bIQEaN10eEg8VJkCp0pQcTuXpUovCev5C6dc=
 
 -- Do not move the order of `location`, `tag` and `--sha256` fields below as this will break the update script
 source-repository-package
     type: git
     location: https://github.com/runtimeverification/haskell-backend.git
-    tag: 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
-    --sha256: sha256-0icYpR6j++NkTlu7MDwR5yZRuOaqYwJCRwb2BnRU+8A=
+    tag: 3f22ee19cc591ce88cb8130c5442e9b344498729
+    --sha256: sha256-FKzHAugImqYFQDnF5MbCw8YDC7JoXAnORiJFNZxU7mI=
     subdir: kore kore-rpc-types
-
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -62,7 +62,7 @@
               cabal = "latest";
               haskell-language-server = "latest";
               fourmolu = {
-                inherit index-state;
+                index-state = "2023-05-17T00:00:00Z";
                 version = "0.12.0.0";
               };
               hlint = "latest";

diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -29,20 +29,28 @@ import Data.Text qualified as Text
 import Data.Text.Encoding qualified as Text
 import GHC.Records
 import Numeric.Natural
+import Prettyprinter (pretty)
 
 import Booster.Definition.Attributes.Base (getUniqueId, uniqueId)
 import Booster.Definition.Base (KoreDefinition (..))
 import Booster.Definition.Base qualified as Definition (RewriteRule (..))
 import Booster.LLVM.Internal qualified as LLVM
 import Booster.Pattern.ApplyEquations qualified as ApplyEquations
-import Booster.Pattern.Base (Pattern (..), TermOrPredicate (..))
+import Booster.Pattern.Base (Pattern (..), Predicate (..), TermOrPredicate (..))
+import Booster.Pattern.Implication (
+    ImplicationInvalidReason (..),
+    ImplicationResult (..),
+    ImplicationUnknownReason (..),
+    simplifyImplication,
+ )
 import Booster.Pattern.Rewrite (
     RewriteFailed (..),
     RewriteResult (..),
     RewriteTrace (..),
     performRewrite,
  )
-import Booster.Pattern.Util (sortOfPattern)
+import Booster.Pattern.Util (sortOfPattern, substitutionAsPredicate)
+import Booster.Prettyprinter (renderOneLineText)
 import Booster.Syntax.Json (KoreJson (..), addHeader, sortOfJson)
 import Booster.Syntax.Json.Externalise
 import Booster.Syntax.Json.Internalise (internalisePattern, internaliseTermOrPredicate)
@@ -180,8 +188,52 @@ respond stateVar =
                                     }
                         (Left something, _traces) ->
                             pure . Left . RpcError.backendError RpcError.Aborted $ show something -- FIXME
-
-        -- this case is only reachable if the cancel appeared as part of a batch request
+        RpcTypes.SimplifyImplication req -> withContext req._module $ \(def, mLlvmLibrary) -> do
+            let internalisedAntecedent =
+                    runExcept $ internalisePattern False Nothing def req.antecedent.term
+                internalisedConsequent =
+                    runExcept $ internalisePattern False Nothing def req.consequent.term
+                doTracing =
+                    any
+                        (fromMaybe False)
+                        [ req.logSuccessfulSimplifications
+                        , req.logFailedSimplifications
+                        ]
+            case (internalisedAntecedent, internalisedConsequent) of
+                (Left patternErrorsAntecedent, _) -> do
+                    Log.logError $ "Error internalising antecedent cterm: " <> Text.pack (show patternErrorsAntecedent)
+                    pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrorsAntecedent
+                (_, Left patternErrorsConsequent) -> do
+                    Log.logError $ "Error internalising consequent cterm: " <> Text.pack (show patternErrorsConsequent)
+                    pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrorsConsequent
+                (Right antecedentPattern, Right consequentPattern) -> do
+                    Log.logInfoNS "booster" "Checking implication by simplification"
+                    let predicateSort = externaliseSort (sortOfPattern consequentPattern)
+                    case simplifyImplication doTracing def mLlvmLibrary antecedentPattern consequentPattern of
+                        ImplicationValid subst -> do
+                            let koreJsonSubstitution = addHeader . externalisePredicate predicateSort . substitutionAsPredicate $ subst
+                            pure . Right . RpcTypes.SimplifyImplication $
+                                RpcTypes.SimplifyImplicationResult
+                                    { validity = RpcTypes.ImplicationValid
+                                    , substitution = Just koreJsonSubstitution
+                                    , logs = mempty
+                                    }
+                        ImplicationInvalid subst reason -> do
+                            let koreJsonSubstitution = addHeader . externalisePredicate predicateSort . substitutionAsPredicate <$> subst
+                            pure . Right . RpcTypes.SimplifyImplication $
+                                RpcTypes.SimplifyImplicationResult
+                                    { validity = RpcTypes.ImplicationInvalid (externaliseImplicationInvalidReason predicateSort reason)
+                                    , substitution = koreJsonSubstitution
+                                    , logs = mempty
+                                    }
+                        ImplicationUnknown subst reason -> do
+                            let koreJsonSubstitution = addHeader . externalisePredicate predicateSort . substitutionAsPredicate <$> subst
+                            pure . Right . RpcTypes.SimplifyImplication $
+                                RpcTypes.SimplifyImplicationResult
+                                    { validity = RpcTypes.ImplicationUnknown (externaliseImplicationUnknownReason predicateSort reason)
+                                    , substitution = koreJsonSubstitution
+                                    , logs = mempty
+                                    }
         RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode
         -- using "Method does not exist" error code
         _ -> pure $ Left RpcError.notImplemented
@@ -338,6 +390,24 @@ toExecState pat =
   where
     (t, p) = externalisePattern pat
 
+externaliseImplicationInvalidReason ::
+    KoreJson.Sort -> ImplicationInvalidReason -> RpcTypes.ImplicationInvalidReason
+externaliseImplicationInvalidReason externalisedSort = \case
+    MatchingFailed reason -> RpcTypes.MatchingFailed (renderOneLineText . pretty $ reason)
+    ConstraintSubsumptionFailed constraints ->
+        let conjunction = foldl AndPredicate Top constraints
+         in RpcTypes.ConstraintSubsumptionFailed $ addHeader $ externalisePredicate externalisedSort conjunction
+
+externaliseImplicationUnknownReason ::
+    KoreJson.Sort -> ImplicationUnknownReason -> RpcTypes.ImplicationUnknownReason
+externaliseImplicationUnknownReason externalisedSort = \case
+    MatchingUnknown term1 term2 -> RpcTypes.MatchingUnknown (addHeader $ externaliseTerm term1) (addHeader $ externaliseTerm term2)
+    ConstraintSubsumptionUnknown constraints ->
+        let conjunction = foldl AndPredicate Top constraints
+         in RpcTypes.ConstraintSubsumptionUnknown $
+                addHeader $
+                    externalisePredicate externalisedSort conjunction
+
 mkLogEquationTrace :: (Maybe Bool, Maybe Bool) -> ApplyEquations.EquationTrace -> Maybe LogEntry
 mkLogEquationTrace
     (logSuccessfulSimplifications, logFailedSimplifications)

diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs
@@ -135,6 +135,7 @@ instance ToJSON KoreRpcJson where
                 Execute r -> toJSON r
                 Implies r -> toJSON r
                 Simplify r -> toJSON r
+                SimplifyImplication r -> toJSON r
                 AddModule r -> toJSON r
                 GetModel r -> toJSON r
                 Cancel -> toJSON ()
@@ -179,6 +180,7 @@ rpcTypeOf = \case
         Execute _ -> ExecuteM
         Implies _ -> ImpliesM
         Simplify _ -> SimplifyM
+        SimplifyImplication _ -> SimplifyImplicationM
         AddModule _ -> AddModuleM
         GetModel _ -> GetModelM
         Cancel -> error "Cancel"

diff --git a/library/Booster/Pattern/Implication.hs b/library/Booster/Pattern/Implication.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2023
+License     : BSD-3-Clause
+-}
+module Booster.Pattern.Implication (
+    simplifyImplication,
+    ImplicationResult (..),
+    ImplicationInvalidReason (..),
+    ImplicationUnknownReason (..),
+) where
+
+import Booster.Definition.Base (KoreDefinition)
+import Booster.LLVM.Internal qualified as LLVM
+import Booster.Pattern.Base (Pattern (..), Predicate, Term)
+import Booster.Pattern.Match qualified as Match
+import Booster.Pattern.Unify (Substitution)
+
+data ImplicationResult
+    = ImplicationValid Substitution
+    | ImplicationInvalid (Maybe Substitution) ImplicationInvalidReason
+    | ImplicationUnknown (Maybe Substitution) ImplicationUnknownReason
+    deriving stock (Eq, Show)
+
+data ImplicationInvalidReason
+    = MatchingFailed Match.MatchFailReason
+    | ConstraintSubsumptionFailed [Predicate]
+    deriving stock (Eq, Show)
+
+data ImplicationUnknownReason
+    = MatchingUnknown Term Term
+    | ConstraintSubsumptionUnknown [Predicate]
+    deriving stock (Eq, Show)
+
+-- | Check implication between two patterns using matching and simplification rules
+simplifyImplication ::
+    Bool ->
+    KoreDefinition ->
+    Maybe LLVM.API ->
+    Pattern ->
+    Pattern ->
+    ImplicationResult
+simplifyImplication _doTracing def _mLlvmLibrary antecedent consequent =
+    case Match.matchTerm def antecedent.term consequent.term of
+        Match.MatchSuccess subst ->
+            -- got substitution, let's now look at constraints
+            case (antecedent.constraints, consequent.constraints) of
+                -- successful matching
+                ([], []) -> ImplicationValid subst
+                (_, _) ->
+                    ImplicationUnknown (Just subst) $
+                        ConstraintSubsumptionUnknown (antecedent.constraints <> consequent.constraints)
+        Match.MatchFailed reason -> ImplicationInvalid Nothing $ MatchingFailed reason
+        Match.MatchIndeterminate antecedentSubterm consequentSubterm ->
+            ImplicationUnknown Nothing $ MatchingUnknown antecedentSubterm consequentSubterm
diff --git a/library/Booster/Pattern/Match.hs b/library/Booster/Pattern/Match.hs
@@ -31,6 +31,7 @@ import Booster.Pattern.Unify (FailReason (..), SortError, checkSubsort)
 import Booster.Pattern.Util (
     checkSymbolIsAc,
     freeVariables,
+    isConcrete,
     isConstructorSymbol,
     isFunctionSymbol,
     modifyVariablesInP,
@@ -269,7 +270,19 @@ match1
             -- and, domain values, injections, maps: fail
             _other ->
                 failWith $ DifferentSymbols app subj
--- matching on maps unsupported
+----- KMap
+-- empty maps match trivially with an empty substitution
+match1
+    (KMap _ [] Nothing)
+    (KMap _ [] Nothing) = pure mempty
+-- concrete maps with equal keys and values match trivially
+match1
+    t1@(KMap def1 keyVals1 Nothing)
+    t2@(KMap def2 keyVals2 Nothing) =
+        if def1 == def2 && isConcrete t1 && isConcrete t2 && keyVals1 == keyVals2
+            then pure mempty
+            else indeterminate t1 t2
+-- matching on non-empty symbolic maps is not supported
 match1
     t1@KMap{}
     t2 = indeterminate t1 t2

diff --git a/library/Booster/Pattern/Util.hs b/library/Booster/Pattern/Util.hs
@@ -10,6 +10,7 @@ module Booster.Pattern.Util (
     retractPattern,
     substituteInTerm,
     substituteInPredicate,
+    substitutionAsPredicate,
     modifyVariables,
     modifyVariablesInT,
     modifyVariablesInP,
@@ -73,6 +74,10 @@ retractPattern :: TermOrPredicate -> Maybe Pattern
 retractPattern (TermAndPredicate patt) = Just patt
 retractPattern _ = Nothing
 
+-- | Convert a substitution into a conjunction of equalities
+substitutionAsPredicate :: Map Variable Term -> Predicate
+substitutionAsPredicate = foldl AndPredicate Top . Map.foldMapWithKey (\var term -> [EqualsTerm (Var var) term])
+
 substituteInTerm :: Map Variable Term -> Term -> Term
 substituteInTerm substitution = goSubst
   where

diff --git a/stack.yaml b/stack.yaml
@@ -11,7 +11,7 @@ extra-deps:
   - typerep-map-0.5.0.0
   - monad-validate-1.2.0.1
   - git: https://github.com/runtimeverification/haskell-backend.git
-    commit: 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
+    commit: 3f22ee19cc591ce88cb8130c5442e9b344498729
     subdirs:
       - kore
       - kore-rpc-types

diff --git a/stack.yaml.lock b/stack.yaml.lock
@@ -40,29 +40,29 @@ packages:
   original:
     hackage: monad-validate-1.2.0.1
 - completed:
-    commit: 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
+    commit: 3f22ee19cc591ce88cb8130c5442e9b344498729
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore
     pantry-tree:
-      sha256: fa0760a1e027c82aac39bcd7b3720d7eede897c1ead49a68bc8b73c25146c9e3
+      sha256: 55f800064db0f4d4ec820cf96d60d0cd0c4cb2b702318be7fccbc5d7266d8047
       size: 44548
     subdir: kore
     version: 0.60.0.0
   original:
-    commit: 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
+    commit: 3f22ee19cc591ce88cb8130c5442e9b344498729
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore
 - completed:
-    commit: 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
+    commit: 3f22ee19cc591ce88cb8130c5442e9b344498729
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore-rpc-types
     pantry-tree:
-      sha256: dd3ceace4dc6a415ac97890808e12bb8d462a81e15f8a192dfeb920c978318fc
-      size: 404
+      sha256: d2fe34b42a7ebed6e53ef592954977a6a8cf5ae86e13517622bb781f6a023015
+      size: 405
     subdir: kore-rpc-types
     version: 0.60.0.0
   original:
-    commit: 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
+    commit: 3f22ee19cc591ce88cb8130c5442e9b344498729
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore-rpc-types
 snapshots:

diff --git a/test/rpc-integration/default.nix b/test/rpc-integration/default.nix
@@ -48,4 +48,5 @@ in {
   get-model = mkIntegrationTest { name = "get-model"; };
   issue212 = mkIntegrationTest { name = "issue212"; };
   foundry-bug-report.tar.gz = mkIntegrationTest { name = "foundry-bug-report.tar.gz"; nativeBuildInputs = [ k openssl procps ]; };
+  simplify-implication = mkIntegrationTest { name = "simplify-implication"; };
 }
diff --git a/test/rpc-integration/resources/micro-kevm.k b/test/rpc-integration/resources/micro-kevm.k
@@ -0,0 +1,30 @@
+module MICRO-KEVM-SYNTAX
+  imports INT
+  imports SET
+// Micro KEVM is a synthetic K definition that uses several K features important in KEVM:
+// * Map-cells
+// * Sets
+// * Lists of Bytes
+    syntax WordStack ::= ".WordStack"      [smtlib(_dotWS)]
+                       | Int ":" WordStack [klabel(_:_WS), smtlib(_WS_)]
+ // --------------------------------------------------------------------
+
+  syntax EthereumSimulation ::= ".EthereumSimulation"
+
+  configuration
+    <k> $PGM:EthereumSimulation </k>
+    <micro-kevm>
+      <wordStack> .WordStack </wordStack>
+      <touchedAccounts> .Set </touchedAccounts>
+      <accounts>
+        <account multiplicity="*" type="Map">
+          <acctID>      0                  </acctID>
+          <balance>     0                  </balance>
+        </account>
+      </accounts>
+    </micro-kevm>
+endmodule
+
+module MICRO-KEVM
+  imports MICRO-KEVM-SYNTAX
+endmodule
diff --git a/test/rpc-integration/resources/micro-kevm.kompile b/test/rpc-integration/resources/micro-kevm.kompile
@@ -0,0 +1,4 @@
+echo "kompiling micro-kevm.k"
+kompile --backend haskell micro-kevm.k
+cp micro-kevm-kompiled/definition.kore micro-kevm.kore
+rm -r micro-kevm-kompiled