WIP Syntactic simplifications

booster/library/Booster/Definition/Attributes/Base.hs

@@ -35,6 +35,7 @@ module Booster.Definition.Attributes.Base (
     Position (..),
     FileSource (..),
     Priority (..),
+    SyntacticClauses (..),
     pattern IsIdem,
     pattern IsNotIdem,
     pattern IsAssoc,
@@ -97,6 +98,7 @@ data AxiomAttributes = AxiomAttributes
     , preserving :: Flag "preservingDefinedness" -- this will override the computed attribute
     , concreteness :: Concreteness
     , smtLemma :: Flag "isSMTLemma"
+    , syntacticClauses :: SyntacticClauses -- indices of conjuncts in rule.requires to be checked syntactically
     }
     deriving stock (Eq, Ord, Show, Generic)
     deriving anyclass (NFData)
@@ -174,6 +176,10 @@ data SymbolType
     deriving stock (Eq, Ord, Show, Generic, Data, Lift)
     deriving anyclass (NFData, Hashable)
 
+newtype SyntacticClauses = SyntacticClauses [Word8]
+    deriving stock (Eq, Ord, Read, Show)
+    deriving newtype (NFData)
+
 pattern IsIdem, IsNotIdem :: Flag "isIdem"
 pattern IsIdem = Flag True
 pattern IsNotIdem = Flag False

booster/library/Booster/Definition/Attributes/Reader.hs

@@ -70,6 +70,7 @@ instance HasAttributes ParsedAxiom where
             <*> (attributes .! "preserves-definedness")
             <*> readConcreteness attributes
             <*> (attributes .! "smt-lemma")
+            <*> readSyntacticClauses attributes
       where
         -- Some rewrite rules are dynamically generated and injected into
         -- a running server using the RPC "add-module" endpoint.
@@ -153,6 +154,24 @@ readConcreteness attributes = do
         [name, sort] -> Right (Text.encodeUtf8 name, Text.encodeUtf8 sort)
         _ -> Left "Invalid variable"
 
+{- | Reads 'syntactic' attribute, returning the set of integer indices.
+     Reports an error if any of the integers are non-positive or there are duplicates.
+     Defaults to an empty set.
+-}
+readSyntacticClauses :: ParsedAttributes -> Except Text SyntacticClauses
+readSyntacticClauses attributes = do
+    syntacticClauses <-
+        maybe (pure Nothing) ((Just <$>) . mapM (except . readWord8)) $
+            getAttribute "syntactic" attributes
+    case syntacticClauses of
+        Nothing -> pure $ SyntacticClauses []
+        Just [] -> pure $ SyntacticClauses []
+        Just more -> pure $ SyntacticClauses more
+  where
+    readWord8 str
+        | all isDigit (Text.unpack str) = first Text.pack $ readEither (Text.unpack str)
+        | otherwise = Left $ "invalid syntactic clause" <> (Text.pack $ show str)
+
 instance HasAttributes ParsedSymbol where
     type Attributes ParsedSymbol = SymbolAttributes
 

booster/library/Booster/Pattern/Match.hs

@@ -10,6 +10,7 @@ module Booster.Pattern.Match (
     FailReason (..),
     Substitution,
     matchTerms,
+    matchTermsWithSubst,
     checkSubsort,
     SortError (..),
 ) where
@@ -121,6 +122,10 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) whe
 
 type Substitution = Map Variable Term
 
+-- | Specialisation of @matchTermsWithSubst@ to an empty initial substitution
+matchTerms :: MatchType -> KoreDefinition -> Term -> Term -> MatchResult
+matchTerms matchType def = matchTermsWithSubst matchType def mempty
+
 {- | Attempts to find a simple unifying substitution for the given
    terms.
 
@@ -131,8 +136,9 @@ type Substitution = Map Variable Term
    to ensure that we always produce a matching substitution without having to check
    after running the matcher
 -}
-matchTerms :: MatchType -> KoreDefinition -> Term -> Term -> MatchResult
-matchTerms matchType KoreDefinition{sorts} term1 term2 =
+matchTermsWithSubst ::
+    MatchType -> KoreDefinition -> Substitution -> Term -> Term -> MatchResult
+matchTermsWithSubst matchType KoreDefinition{sorts} knownSubst term1 term2 =
     let runMatch :: MatchState -> MatchResult
         runMatch =
             fromEither
@@ -153,7 +159,7 @@ matchTerms matchType KoreDefinition{sorts} term1 term2 =
             else
                 runMatch
                     State
-                        { mSubstitution = Map.empty
+                        { mSubstitution = knownSubst
                         , mQueue = Seq.singleton (term1, term2) -- PriorityQueue.singleton (term1, term2) RegularTerm ()
                         , mMapQueue = mempty
                         , mIndeterminate = []

booster/test/rpc-integration/resources/kompile-from-double-definition.sh

@@ -39,7 +39,7 @@ esac
 llvm-kompile ${NAME}.llvm.kore ./dt c -- \
              -fPIC -std=c++17 -o interpreter \
              $PLUGIN_LIBS $PLUGIN_INCLUDE $PLUGIN_CPP \
-             -lcrypto -lssl $LPROCPS -lsecp256k1
+             -lcrypto -lssl -lsecp256k1 $LPROCPS
 mv interpreter.* ${NAME}.dylib
 
 # remove temporary artefacts

booster/test/rpc-integration/resources/syntactic-simplification.k

@@ -0,0 +1,38 @@
+module SYNTACTIC-SIMPLIFICATION
+  imports INT
+  imports BOOL
+
+  syntax State ::= test1Init()
+                 | test1State1()
+                 | test1State2()
+
+  configuration <k> $PGM:State ~> .K </k>
+                <int-x> 0:Int        </int-x>
+                <int-y> 0:Int        </int-y>
+
+  ////////////////////////////////////////////////////////////////////////////////
+  //
+  ////////////////////////////////////////////////////////////////////////////////
+  rule [test1-init]: <k> test1Init() => test1State1() ... </k>
+                     <int-x> _         => ?X              </int-x>
+                     <int-y> _         => ?Y              </int-y>
+                     ensures  ?X <Int 100
+                      andBool ?Y <Int 50
+                      andBool ?X <Int ?Y
+
+  rule [test1-1-2]: <k> test1State1() => test1State2() ... </k>
+                    <int-x> X                              </int-x>
+                    requires X <Int 50
+
+  rule [test1-simplify]:
+    X <Int Y => true
+    requires X <Int Z
+     andBool Z <Int Y
+     // [simplification, syntactic(1)]
+     [simplification]
+
+// 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

booster/test/rpc-integration/resources/syntactic-simplification.kompile

@@ -0,0 +1,45 @@
+set -eux
+
+SCRIPT_DIR=$(dirname $0)
+PLUGIN_DIR=${PLUGIN_DIR:-""}
+
+if [ -z "$PLUGIN_DIR" ]; then
+    echo "PLUGIN_DIR required to link in a crypto plugin dependency"
+    exit 1
+else
+    for lib in libff libcryptopp blake2; do
+        LIBFILE=$(find ${PLUGIN_DIR} -name "${lib}.a" | head -1)
+        [ -z "$LIBFILE" ] && (echo "[Error] Unable to locate ${lib}.a"; exit 1)
+        PLUGIN_LIBS+="$LIBFILE "
+        PLUGIN_INCLUDE+="-I$(dirname $LIBFILE) -I$(dirname $LIBFILE)/../include "
+    done
+    #PLUGIN_CPP=$(find ${PLUGIN_DIR}/plugin-c -name "*.cpp")
+    PLUGIN_CPP="${PLUGIN_DIR}/include/plugin-c/crypto.cpp ${PLUGIN_DIR}/include/plugin-c/plugin_util.cpp"
+fi
+
+NAME=$(basename ${0%.kompile})
+NAMETGZ=$(basename ${0%.kompile})
+
+
+# provide haskell definition
+cp ${NAME}.haskell.kore ${NAME}.kore
+
+# Regenerate llvm backend decision tree
+mkdir -p ./dt
+llvm-kompile-matching ${NAME}.llvm.kore qbaL ./dt 0
+
+# kompile llvm-definition to interpreter
+
+case "$OSTYPE" in
+  linux*)   LPROCPS="-lprocps" ;;
+  *)        LPROCPS="" ;;
+esac
+
+llvm-kompile ${NAME}.llvm.kore ./dt c -- \
+             -fPIC -std=c++17 -o interpreter \
+             $PLUGIN_LIBS $PLUGIN_INCLUDE $PLUGIN_CPP \
+             -lcrypto -lssl -lsecp256k1 $LPROCPS
+mv interpreter.* ${NAME}.dylib
+
+# remove temporary artefacts
+rm -r dt

booster/test/rpc-integration/resources/syntactic-simplification.llvm.kore

@@ -0,0 +1 @@
+3934-smt.llvm.kore

booster/test/rpc-integration/test-syntactic-simplification/README.md

@@ -0,0 +1,7 @@
+# Test application of syntactic simplification rules
+
+See `../resourses/syntactic-simplification.k`.
+
+We have to keep `../resourses/syntactic-simplification.haskell.kore`, the K front-end does not yet support the `syntactic` attribute. The Kore encoding of the simplification rule `test1-simplify` is manually modified to contain the attribute `syntactic{}("1")`. `../resourses/syntactic-simplification.haskell.kore` should be removed from Git once the compiler supports this feature.
+
+We also need an LLVM definition, and we are re-using ``../resourses/3934-smt.llvm.kore` as it is checked-in, but any definition with `INT` and `BOOL` would work.