From ca05f14b7957fec9f2a5ab3444cae01c5a76f12f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 20 Dec 2023 10:07:38 +0100 Subject: [PATCH] Revert "Concurrent `kore-rpc` server (#3704)" (#3707) Reverts https://github.com/runtimeverification/haskell-backend/pull/3704. We would like to update the `haskell-backend` version used in [hs-backend-booster](https://github.com/runtimeverification/hs-backend-booster/) in order to merge https://github.com/runtimeverification/hs-backend-booster/pull/421. We cannot have https://github.com/runtimeverification/haskell-backend/pull/3704 (concurrent `kore-rpc`), because we will need to merge https://github.com/runtimeverification/hs-backend-booster/pull/427 (concurrent `kore-rpc-booster`). We do not want to merge the concurrent `kore-rpc-booster` PR before the Holiday break, since it is a braking change for `pyk`. The reverted PR will need to be reopened. I think it is best to merge it in sync with https://github.com/runtimeverification/hs-backend-booster/pull/427, preparing a relevant change to `pyk` in advance. --- cabal.project.freeze | 2 +- kore-rpc-types/src/Kore/JsonRpc/Error.hs | 1 - kore-rpc-types/src/Kore/JsonRpc/Types.hs | 3 +- kore/src/Kore/JsonRpc.hs | 133 +- .../rpc-server/add-module/add-again/README.md | 32 - .../add-module/add-again/definition.kore | 1425 ----------------- .../add-module/add-again/params.json | 4 - .../add-module/add-again/response.golden | 1 - test/rpc-server/add-module/add/params.json | 3 +- .../rpc-server/add-module/add/response.golden | 2 +- 10 files changed, 53 insertions(+), 1553 deletions(-) delete mode 100644 test/rpc-server/add-module/add-again/README.md delete mode 100644 test/rpc-server/add-module/add-again/definition.kore delete mode 100644 test/rpc-server/add-module/add-again/params.json delete mode 100644 test/rpc-server/add-module/add-again/response.golden diff --git a/cabal.project.freeze b/cabal.project.freeze index a451ab6bcd..2fccf97608 100644 --- a/cabal.project.freeze +++ b/cabal.project.freeze @@ -131,7 +131,7 @@ constraints: any.Cabal ==3.6.3.0, any.json-rpc ==1.0.4, any.junit-xml ==0.1.0.2, any.kan-extensions ==5.2.5, - kore +threaded, + kore -threaded, any.lens ==5.1.1, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, any.libyaml ==0.1.2, diff --git a/kore-rpc-types/src/Kore/JsonRpc/Error.hs b/kore-rpc-types/src/Kore/JsonRpc/Error.hs index 2911eb7856..7b52fb6f11 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Error.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Error.hs @@ -41,7 +41,6 @@ data JsonRpcBackendError | SmtSolverError | Aborted | MultipleStates - | DuplicateModule deriving stock (Enum, Show) backendError :: ToJSON a => JsonRpcBackendError -> a -> ErrorObj diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 0dfbe8243c..fca0b16617 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -76,12 +76,11 @@ data SimplifyRequest = SimplifyRequest data AddModuleRequest = AddModuleRequest { _module :: Text - , nameAsId :: !(Maybe Bool) } deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] AddModuleRequest + via CustomJSON '[FieldLabelModifier '[StripPrefix "_"]] AddModuleRequest data GetModelRequest = GetModelRequest { state :: KoreJson diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index b84d3a55ae..bcff4478d9 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -9,10 +9,8 @@ module Kore.JsonRpc ( ) where import Control.Concurrent.MVar qualified as MVar -import Control.Monad.Except (MonadError (throwError), liftEither, runExceptT, withExceptT) +import Control.Monad.Except (runExceptT) import Control.Monad.Logger (runLoggingT) -import Control.Monad.Trans.Except (catchE) -import Crypto.Hash (SHA256 (..), hashWith) import Data.Aeson.Types (ToJSON (..)) import Data.Coerce (coerce) import Data.Conduit.Network (serverSettings) @@ -25,9 +23,7 @@ import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map import Data.Sequence as Seq (Seq, empty) import Data.Set qualified as Set -import Data.String (fromString) import Data.Text (Text) -import Data.Text.Encoding (encodeUtf8) import GlobalMain ( LoadedDefinition (..), SerializedDefinition (..), @@ -465,85 +461,54 @@ respond serverState moduleName runSMT = OrPattern.toTermLike sort result , logs = allLogs } - AddModule AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do - let nameAsId = fromMaybe False nameAsId' - parsedModule@Module{moduleName = name} <- - withExceptT (backendError CouldNotParsePattern) $ - liftEither $ - parseKoreModule "" _module - st@ServerState - { serializedModules - , loadedDefinition = LoadedDefinition{indexedModules, definedNames, kFileLocations} - } <- - liftIO $ MVar.takeMVar serverState - let moduleHash = ModuleName . fromString . ('m' :) . show . hashWith SHA256 $ encodeUtf8 _module - - -- put the original state back if we fail at any point - flip catchE (\e -> liftIO (MVar.putMVar serverState st) >> throwError e) $ do - when - ( nameAsId - && isJust (Map.lookup (coerce name) indexedModules) - && isNothing (Map.lookup (coerce moduleHash) indexedModules) - ) - $ - -- if a module with the same name already exists, but it's contents are different to the current module, throw an error - throwError - $ backendError DuplicateModule name - - case Map.lookup (coerce moduleHash) indexedModules of - Just{} -> do - -- the module already exists so we don't need to add it again - liftIO $ MVar.putMVar serverState st - pure . AddModule $ AddModuleResult (getModuleName moduleHash) - Nothing -> do - (newIndexedModules, newDefinedNames) <- - withExceptT (backendError CouldNotVerifyPattern) $ - liftEither $ - verifyAndIndexDefinitionWithBase - (indexedModules, definedNames) - Builtin.koreVerifiers - (Definition (def @Attributes) [parsedModule{moduleName = moduleHash}]) - - newModule <- - liftEither $ - maybe (Left $ backendError CouldNotFindModule moduleHash) Right $ - Map.lookup (coerce moduleHash) newIndexedModules - - let metadataTools = MetadataTools.build newModule - lemmas = getSMTLemmas newModule - serializedModule <- - liftIO - . runSMT metadataTools lemmas - $ Exec.makeSerializedModule newModule - internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache - - let serializedDefinition = - SerializedDefinition - { serializedModule = serializedModule - , locations = kFileLocations - , internedTextCache = internedTextCacheHash - , lemmas = lemmas - } - newSerializedModules = - Map.fromList $ - if nameAsId - then [(coerce moduleHash, serializedDefinition), (coerce name, serializedDefinition)] - else [(coerce moduleHash, serializedDefinition)] - loadedDefinition = - LoadedDefinition - { indexedModules = (if nameAsId then Map.insert (coerce name) newModule else id) newIndexedModules - , definedNames = newDefinedNames - , kFileLocations - } - - liftIO . MVar.putMVar serverState $ - ServerState - { serializedModules = - serializedModules `Map.union` newSerializedModules - , loadedDefinition - } - - pure . AddModule $ AddModuleResult (getModuleName moduleHash) + AddModule AddModuleRequest{_module} -> + case parseKoreModule "" _module of + Left err -> pure $ Left $ backendError CouldNotParsePattern err + Right parsedModule@Module{moduleName = name} -> do + LoadedDefinition{indexedModules, definedNames, kFileLocations} <- + liftIO $ loadedDefinition <$> MVar.readMVar serverState + let verified = + verifyAndIndexDefinitionWithBase + (indexedModules, definedNames) + Builtin.koreVerifiers + (Definition (def @Attributes) [parsedModule]) + case verified of + Left err -> pure $ Left $ backendError CouldNotVerifyPattern err + Right (indexedModules', definedNames') -> + case Map.lookup (coerce name) indexedModules' of + Nothing -> pure $ Left $ backendError CouldNotFindModule name + Just mainModule -> do + let metadataTools = MetadataTools.build mainModule + lemmas = getSMTLemmas mainModule + serializedModule' <- + liftIO + . runSMT metadataTools lemmas + $ Exec.makeSerializedModule mainModule + internedTextCache <- liftIO $ readIORef globalInternedTextCache + + liftIO . MVar.modifyMVar_ serverState $ + \ServerState{serializedModules} -> do + let serializedDefinition = + SerializedDefinition + { serializedModule = serializedModule' + , locations = kFileLocations + , internedTextCache + , lemmas + } + loadedDefinition = + LoadedDefinition + { indexedModules = indexedModules' + , definedNames = definedNames' + , kFileLocations + } + pure + ServerState + { serializedModules = + Map.insert (coerce name) serializedDefinition serializedModules + , loadedDefinition + } + + pure . Right . AddModule $ AddModuleResult (getModuleName name) GetModel GetModelRequest{state, _module} -> withMainModule (coerce _module) $ \serializedModule lemmas -> case verifyIn serializedModule state of diff --git a/test/rpc-server/add-module/add-again/README.md b/test/rpc-server/add-module/add-again/README.md deleted file mode 100644 index 90f28de5f7..0000000000 --- a/test/rpc-server/add-module/add-again/README.md +++ /dev/null @@ -1,32 +0,0 @@ -# Add module with `add-module` endpoint again - -This test uses [a-to-f](../../resources/a-to-f/) [definition](../../resources/a-to-f/definition.kore) split into two parts: - -When the server starts, a `TEST` module is loaded which contains the following transitions: - -``` - a - / \ - V V - b c - | - V - d -``` - -Then a `NEW` module is added using the `add-module` endpoint [parameters](./params.json), -adding the following transitions: - - -``` - d - | - V - e - | - V - f -``` - -Expected: -* Module successfully added even though it has been added already, because the content is exactly the same. diff --git a/test/rpc-server/add-module/add-again/definition.kore b/test/rpc-server/add-module/add-again/definition.kore deleted file mode 100644 index 3ae9d4f3ce..0000000000 --- a/test/rpc-server/add-module/add-again/definition.kore +++ /dev/null @@ -1,1425 +0,0 @@ -[topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)")] - -module BASIC-K - sort SortK{} [] - sort SortKItem{} [] -endmodule -[] -module KSEQ - import BASIC-K [] - symbol kseq{}(SortKItem{}, SortK{}) : SortK{} [constructor{}(), functional{}()] - symbol dotk{}() : SortK{} [constructor{}(), functional{}()] - symbol append{}(SortK{}, SortK{}) : SortK{} [function{}(), functional{}()] - axiom {R} \implies{R}( - \and{R}( - \top{R}(), - \and{R}( - \in{SortK{}, R}(X0:SortK{}, dotk{}()), - \and{R}( - \in{SortK{}, R}(X1:SortK{}, TAIL:SortK{}), - \top{R}() - )) - ), - \equals{SortK{}, R}( - append{}(X0:SortK{}, X1:SortK{}), - \and{SortK{}}( - TAIL:SortK{}, - \top{SortK{}}() - ) - ) - ) [] - axiom {R} \implies{R}( - \and{R}( - \top{R}(), - \and{R}( - \in{SortK{}, R}(X0:SortK{}, kseq{}(K:SortKItem{}, KS:SortK{})), - \and{R}( - \in{SortK{}, R}(X1:SortK{}, TAIL:SortK{}), - \top{R}() - )) - ), - \equals{SortK{}, R}( - append{}(X0:SortK{}, X1:SortK{}), - \and{SortK{}}( - kseq{}(K:SortKItem{}, append{}(KS:SortK{}, TAIL:SortK{})), - \top{SortK{}}() - ) - ) - ) [] -endmodule -[] -module INJ - symbol inj{From, To}(From) : To [sortInjection{}()] - axiom {S1, S2, S3, R} \equals{S3, R}(inj{S2, S3}(inj{S1, S2}(T:S1)), inj{S1, S3}(T:S1)) [simplification{}()] -endmodule -[] -module K - import KSEQ [] - import INJ [] - alias weakExistsFinally{A}(A) : A where weakExistsFinally{A}(@X:A) := @X:A [] - alias weakAlwaysFinally{A}(A) : A where weakAlwaysFinally{A}(@X:A) := @X:A [] - alias allPathGlobally{A}(A) : A where allPathGlobally{A}(@X:A) := @X:A [] -endmodule -[] - -module TEST - -// imports - import K [] - -// sorts - sort SortKCellOpt{} [] - sort SortGeneratedTopCellFragment{} [] - hooked-sort SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), element{}(LblListItem{}()), concat{}(Lbl'Unds'List'Unds'{}()), unit{}(Lbl'Stop'List{}()), hook{}("LIST.List"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(723,3,723,32)")] - sort SortKCell{} [] - sort SortGeneratedTopCell{} [] - sort SortGeneratedCounterCell{} [] - hooked-sort SortMap{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), concat{}(Lbl'Unds'Map'Unds'{}()), unit{}(Lbl'Stop'Map{}()), hook{}("MAP.Map"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(218,3,218,29)")] - sort SortGeneratedCounterCellOpt{} [] - sort SortKConfigVar{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/kast.md)"), token{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(40,3,40,28)"), hasDomainValues{}()] - hooked-sort SortInt{} [hook{}("INT.Int"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(999,3,999,29)"), hasDomainValues{}()] - hooked-sort SortSet{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), element{}(LblSetItem{}()), concat{}(Lbl'Unds'Set'Unds'{}()), unit{}(Lbl'Stop'Set{}()), hook{}("SET.Set"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(510,3,510,29)")] - sort SortState{} [hasDomainValues{}()] - hooked-sort SortBool{} [hook{}("BOOL.Bool"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(878,3,878,32)"), hasDomainValues{}()] - -// symbols - hooked-symbol Lbl'Stop'List{}() : SortList{} [latex{}("\\dotCt{List}"), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), smtlib{}("smt_seq_nil"), terminals{}("1"), klabel{}(".List"), hook{}("LIST.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(747,19,747,142)"), left{}(), format{}("%c.List%r"), function{}()] - hooked-symbol Lbl'Stop'Map{}() : SortMap{} [latex{}("\\dotCt{Map}"), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("1"), klabel{}(".Map"), hook{}("MAP.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(248,18,248,124)"), left{}(), format{}("%c.Map%r"), function{}()] - hooked-symbol Lbl'Stop'Set{}() : SortSet{} [latex{}("\\dotCt{Set}"), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("1"), klabel{}(".Set"), hook{}("SET.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(539,18,539,118)"), left{}(), format{}("%c.Set%r"), function{}()] - symbol Lbl'-LT-'generatedCounter'-GT-'{}(SortInt{}) : SortGeneratedCounterCell{} [functional{}(), constructor{}(), cellName{}("generatedCounter"), priorities{}(), right{}(), terminals{}("101"), left{}(), format{}("%c%r%i%n%1%d%n%c%r"), injective{}(), cell{}()] - symbol Lbl'-LT-'generatedTop'-GT-'{}(SortKCell{}, SortGeneratedCounterCell{}) : SortGeneratedTopCell{} [functional{}(), constructor{}(), cellName{}("generatedTop"), priorities{}(), right{}(), terminals{}("1001"), left{}(), format{}("%1"), injective{}(), cell{}(), topcell{}()] - symbol Lbl'-LT-'generatedTop'-GT-'-fragment{}(SortKCellOpt{}, SortGeneratedCounterCellOpt{}) : SortGeneratedTopCellFragment{} [functional{}(), constructor{}(), cellFragment{}("GeneratedTopCell"), priorities{}(), right{}(), terminals{}("1001"), left{}(), format{}("%c-fragment%r %1 %2 %c-fragment%r"), injective{}()] - symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)"), cellName{}("k"), maincell{}(), priorities{}(), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), right{}(), terminals{}("101"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(9,17,9,42)"), left{}(), format{}("%c%r%i%n%1%d%n%c%r"), injective{}(), cell{}(), topcell{}()] - hooked-symbol LblList'Coln'get{}(SortList{}, SortInt{}) : SortKItem{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("0101"), klabel{}("List:get"), hook{}("LIST.get"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(766,20,766,99)"), left{}(), format{}("%1 %c[%r %2 %c]%r"), function{}()] - hooked-symbol LblList'Coln'range{}(SortList{}, SortInt{}, SortInt{}) : SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("11010101"), klabel{}("List:range"), hook{}("LIST.range"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(813,19,813,120)"), left{}(), format{}("%crange%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}()] - hooked-symbol LblListItem{}(SortKItem{}) : SortList{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), smtlib{}("smt_seq_elem"), terminals{}("1101"), klabel{}("ListItem"), hook{}("LIST.element"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(755,19,755,132)"), left{}(), format{}("%cListItem%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol LblMap'Coln'lookup{}(SortMap{}, SortKItem{}) : SortKItem{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("0101"), klabel{}("Map:lookup"), hook{}("MAP.lookup"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(271,20,271,113)"), left{}(), format{}("%1 %c[%r %2 %c]%r"), function{}()] - hooked-symbol LblMap'Coln'update{}(SortMap{}, SortKItem{}, SortKItem{}) : SortMap{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), prefer{}(), right{}(), terminals{}("010101"), klabel{}("Map:update"), hook{}("MAP.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(290,18,290,140)"), left{}(), format{}("%1 %c[%r %2 %c<-%r %3 %c]%r"), function{}()] - hooked-symbol LblSet'Coln'difference{}(SortSet{}, SortSet{}) : SortSet{} [latex{}("{#1}-_{\\it Set}{#2}"), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("010"), klabel{}("Set:difference"), hook{}("SET.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(579,18,579,142)"), left{}(), format{}("%1 %c-Set%r %2"), function{}()] - hooked-symbol LblSet'Coln'in{}(SortKItem{}, SortSet{}) : SortBool{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("010"), klabel{}("Set:in"), hook{}("SET.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(587,19,587,102)"), left{}(), format{}("%1 %cin%r %2"), function{}()] - hooked-symbol LblSetItem{}(SortKItem{}) : SortSet{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("1101"), klabel{}("SetItem"), hook{}("SET.element"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(547,18,547,119)"), left{}(), format{}("%cSetItem%r %c(%r %1 %c)%r"), injective{}(), function{}()] - hooked-symbol Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [latex{}("{#1}-_{\\it Map}{#2}"), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("010"), hook{}("MAP.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(311,18,311,116)"), left{}(), format{}("%1 %c-Map%r %2"), function{}()] - hooked-symbol Lbl'Unds-LT-Eqls'Map'UndsUnds'MAP'Unds'Bool'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortBool{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("010"), hook{}("MAP.inclusion"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(383,19,383,87)"), left{}(), format{}("%1 %c<=Map%r %2"), function{}()] - hooked-symbol Lbl'Unds-LT-Eqls'Set'UndsUnds'SET'Unds'Bool'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortBool{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("010"), hook{}("SET.inclusion"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(596,19,596,81)"), left{}(), format{}("%1 %c<=Set%r %2"), function{}()] - hooked-symbol Lbl'Unds'List'Unds'{}(SortList{}, SortList{}) : SortList{} [unit{}(Lbl'Stop'List{}()), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), element{}(LblListItem{}()), symbol'Kywd'{}(), priorities{}(), right{}(), assoc{}(), smtlib{}("smt_seq_concat"), terminals{}("00"), klabel{}("_List_"), hook{}("LIST.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(739,19,739,188)"), left{}(Lbl'Unds'List'Unds'{}()), format{}("%1%n%2"), function{}()] - hooked-symbol Lbl'Unds'Map'Unds'{}(SortMap{}, SortMap{}) : SortMap{} [unit{}(Lbl'Stop'Map{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), symbol'Kywd'{}(), comm{}(), priorities{}(), right{}(), assoc{}(), terminals{}("00"), index{}("0"), klabel{}("_Map_"), hook{}("MAP.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(240,18,240,173)"), left{}(Lbl'Unds'Map'Unds'{}()), format{}("%1%n%2"), function{}()] - hooked-symbol Lbl'Unds'Set'Unds'{}(SortSet{}, SortSet{}) : SortSet{} [unit{}(Lbl'Stop'Set{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), element{}(LblSetItem{}()), symbol'Kywd'{}(), idem{}(), comm{}(), priorities{}(), right{}(), assoc{}(), terminals{}("00"), klabel{}("_Set_"), hook{}("SET.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(531,18,531,165)"), left{}(Lbl'Unds'Set'Unds'{}()), format{}("%1%n%2"), function{}()] - hooked-symbol Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortKItem{}) : SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010101"), klabel{}("List:set"), hook{}("LIST.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(775,19,775,108)"), left{}(), format{}("%1 %c[%r %2 %c<-%r %3 %c]%r"), function{}()] - hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(SortMap{}, SortKItem{}) : SortMap{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("010111"), klabel{}("_[_<-undef]"), hook{}("MAP.remove"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(299,18,299,117)"), left{}(), format{}("%1 %c[%r %2 %c<-%r %cundef%r %c]%r"), function{}()] - hooked-symbol Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem{}(SortMap{}, SortKItem{}, SortKItem{}) : SortKItem{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("010110"), klabel{}("Map:lookupOrDefault"), hook{}("MAP.lookupOrDefault"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(281,20,281,134)"), left{}(), format{}("%1 %c[%r %2 %c]%r %corDefault%r %3"), function{}()] - hooked-symbol Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List{}(SortKItem{}, SortList{}) : SortBool{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("010"), klabel{}("_inList_"), hook{}("LIST.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(822,19,822,97)"), left{}(), format{}("%1 %cin%r %2"), function{}()] - hooked-symbol Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(SortKItem{}, SortMap{}) : SortBool{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("01101"), hook{}("MAP.in_keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(357,19,357,89)"), left{}(), format{}("%1 %cin_keys%r %c(%r %2 %c)%r"), function{}()] - hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(SortKItem{}, SortKItem{}) : SortMap{} [latex{}("{#1}\\mapsto{#2}"), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), symbol'Kywd'{}(), priorities{}(Lbl'Stop'Map{}(),Lbl'Unds'Map'Unds'{}()), right{}(Lbl'UndsPipe'-'-GT-Unds'{}()), terminals{}("010"), klabel{}("_|->_"), hook{}("MAP.element"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(257,18,257,151)"), left{}(Lbl'UndsPipe'-'-GT-Unds'{}()), format{}("%1 %c|->%r %2"), injective{}(), function{}()] - hooked-symbol Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), comm{}(), priorities{}(), right{}(), terminals{}("010"), hook{}("SET.union"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(558,18,558,92)"), left{}(Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}()), format{}("%1 %c|Set%r %2"), function{}()] - hooked-symbol Lblchoice'LParUndsRParUnds'MAP'Unds'KItem'Unds'Map{}(SortMap{}) : SortKItem{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("Map:choice"), hook{}("MAP.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(393,20,393,101)"), left{}(), format{}("%cchoice%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol Lblchoice'LParUndsRParUnds'SET'Unds'KItem'Unds'Set{}(SortSet{}) : SortKItem{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("Set:choice"), hook{}("SET.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(614,20,614,95)"), left{}(), format{}("%cchoice%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol LblfillList'LParUndsCommUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortInt{}, SortKItem{}) : SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101010101"), klabel{}("fillList"), hook{}("LIST.fill"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(803,19,803,100)"), left{}(), format{}("%cfillList%r %c(%r %1 %c,%r %2 %c,%r %3 %c,%r %4 %c)%r"), function{}()] - symbol LblgetGeneratedCounterCell{}(SortGeneratedTopCell{}) : SortGeneratedCounterCell{} [priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cgetGeneratedCounterCell%r %c(%r %1 %c)%r"), function{}()] - symbol LblinitGeneratedCounterCell{}() : SortGeneratedCounterCell{} [noThread{}(), priorities{}(), right{}(), terminals{}("1"), left{}(), initializer{}(), format{}("%cinitGeneratedCounterCell%r"), function{}()] - symbol LblinitGeneratedTopCell{}(SortMap{}) : SortGeneratedTopCell{} [noThread{}(), priorities{}(), right{}(), terminals{}("1101"), left{}(), initializer{}(), format{}("%cinitGeneratedTopCell%r %c(%r %1 %c)%r"), function{}()] - symbol LblinitKCell{}(SortMap{}) : SortKCell{} [noThread{}(), priorities{}(), right{}(), terminals{}("1101"), left{}(), initializer{}(), format{}("%cinitKCell%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), comm{}(), priorities{}(), right{}(), terminals{}("110101"), klabel{}("intersectSet"), hook{}("SET.intersection"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(569,18,569,90)"), left{}(), format{}("%cintersectSet%r %c(%r %1 %c,%r %2 %c)%r"), function{}()] - symbol LblisBool{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("Bool"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisBool%r %c(%r %1 %c)%r"), function{}()] - symbol LblisGeneratedCounterCell{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("GeneratedCounterCell"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisGeneratedCounterCell%r %c(%r %1 %c)%r"), function{}()] - symbol LblisGeneratedCounterCellOpt{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("GeneratedCounterCellOpt"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisGeneratedCounterCellOpt%r %c(%r %1 %c)%r"), function{}()] - symbol LblisGeneratedTopCell{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("GeneratedTopCell"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisGeneratedTopCell%r %c(%r %1 %c)%r"), function{}()] - symbol LblisGeneratedTopCellFragment{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("GeneratedTopCellFragment"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisGeneratedTopCellFragment%r %c(%r %1 %c)%r"), function{}()] - symbol LblisInt{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("Int"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisInt%r %c(%r %1 %c)%r"), function{}()] - symbol LblisK{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("K"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisK%r %c(%r %1 %c)%r"), function{}()] - symbol LblisKCell{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("KCell"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisKCell%r %c(%r %1 %c)%r"), function{}()] - symbol LblisKCellOpt{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("KCellOpt"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisKCellOpt%r %c(%r %1 %c)%r"), function{}()] - symbol LblisKConfigVar{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("KConfigVar"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisKConfigVar%r %c(%r %1 %c)%r"), function{}()] - symbol LblisKItem{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("KItem"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisKItem%r %c(%r %1 %c)%r"), function{}()] - symbol LblisList{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("List"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisList%r %c(%r %1 %c)%r"), function{}()] - symbol LblisMap{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("Map"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisMap%r %c(%r %1 %c)%r"), function{}()] - symbol LblisSet{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("Set"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisSet%r %c(%r %1 %c)%r"), function{}()] - symbol LblisState{}(SortK{}) : SortBool{} [functional{}(), total{}(), predicate{}("State"), priorities{}(), right{}(), terminals{}("1101"), left{}(), format{}("%cisState%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(SortMap{}) : SortSet{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("1101"), klabel{}("keys"), hook{}("MAP.keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(341,18,341,82)"), left{}(), format{}("%ckeys%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol Lblkeys'Unds'list'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), hook{}("MAP.keys_list"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(349,19,349,80)"), left{}(), format{}("%ckeys_list%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol LblmakeList'LParUndsCommUndsRParUnds'LIST'Unds'List'Unds'Int'Unds'KItem{}(SortInt{}, SortKItem{}) : SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), klabel{}("makeList"), hook{}("LIST.make"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(784,19,784,82)"), left{}(), format{}("%cmakeList%r %c(%r %1 %c,%r %2 %c)%r"), function{}()] - symbol LblnoGeneratedCounterCell{}() : SortGeneratedCounterCellOpt{} [functional{}(), constructor{}(), cellOptAbsent{}("GeneratedCounterCell"), priorities{}(), right{}(), terminals{}("1"), left{}(), format{}("%cnoGeneratedCounterCell%r"), injective{}()] - symbol LblnoKCell{}() : SortKCellOpt{} [functional{}(), constructor{}(), cellOptAbsent{}("KCell"), priorities{}(), right{}(), terminals{}("1"), left{}(), format{}("%cnoKCell%r"), injective{}()] - symbol Lblproject'Coln'Bool{}(SortK{}) : SortBool{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:Bool%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'GeneratedCounterCell{}(SortK{}) : SortGeneratedCounterCell{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:GeneratedCounterCell%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'GeneratedCounterCellOpt{}(SortK{}) : SortGeneratedCounterCellOpt{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:GeneratedCounterCellOpt%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'GeneratedTopCell{}(SortK{}) : SortGeneratedTopCell{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:GeneratedTopCell%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'GeneratedTopCellFragment{}(SortK{}) : SortGeneratedTopCellFragment{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:GeneratedTopCellFragment%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'Int{}(SortK{}) : SortInt{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:Int%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'K{}(SortK{}) : SortK{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:K%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'KCell{}(SortK{}) : SortKCell{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:KCell%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'KCellOpt{}(SortK{}) : SortKCellOpt{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:KCellOpt%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'KItem{}(SortK{}) : SortKItem{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:KItem%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'List{}(SortK{}) : SortList{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:List%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'Map{}(SortK{}) : SortMap{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:Map%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'Set{}(SortK{}) : SortSet{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:Set%r %c(%r %1 %c)%r"), function{}()] - symbol Lblproject'Coln'State{}(SortK{}) : SortState{} [priorities{}(), right{}(), terminals{}("1101"), projection{}(), left{}(), format{}("%cproject:State%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(SortMap{}, SortSet{}) : SortMap{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("110101"), klabel{}("removeAll"), hook{}("MAP.removeAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(333,18,333,87)"), left{}(), format{}("%cremoveAll%r %c(%r %1 %c,%r %2 %c)%r"), function{}()] - hooked-symbol Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}(SortList{}) : SortInt{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), smtlib{}("smt_seq_len"), terminals{}("1101"), klabel{}("sizeList"), hook{}("LIST.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(830,18,830,117)"), left{}(), format{}("%csize%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map{}(SortMap{}) : SortInt{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("1101"), klabel{}("sizeMap"), hook{}("MAP.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(373,18,373,99)"), left{}(), format{}("%csize%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(SortSet{}) : SortInt{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("1101"), klabel{}("size"), hook{}("SET.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(604,18,604,76)"), left{}(), format{}("%csize%r %c(%r %1 %c)%r"), function{}()] - hooked-symbol LblupdateList'LParUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'List{}(SortList{}, SortInt{}, SortList{}) : SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("11010101"), klabel{}("updateList"), hook{}("LIST.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(794,19,794,97)"), left{}(), format{}("%cupdateList%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}()] - hooked-symbol LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("110101"), klabel{}("updateMap"), hook{}("MAP.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(324,18,324,87)"), left{}(), format{}("%cupdateMap%r %c(%r %1 %c,%r %2 %c)%r"), function{}()] - hooked-symbol Lblvalues'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("values"), hook{}("MAP.values"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(365,19,365,77)"), left{}(), format{}("%cvalues%r %c(%r %1 %c)%r"), function{}()] - -// generated axioms - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKCellOpt{}, SortKItem{}} (From:SortKCellOpt{}))) [subsort{SortKCellOpt{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedCounterCellOpt{}, SortKItem{}} (From:SortGeneratedCounterCellOpt{}))) [subsort{SortGeneratedCounterCellOpt{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortGeneratedCounterCellOpt{}, \equals{SortGeneratedCounterCellOpt{}, R} (Val:SortGeneratedCounterCellOpt{}, inj{SortGeneratedCounterCell{}, SortGeneratedCounterCellOpt{}} (From:SortGeneratedCounterCell{}))) [subsort{SortGeneratedCounterCell{}, SortGeneratedCounterCellOpt{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKCell{}, SortKItem{}} (From:SortKCell{}))) [subsort{SortKCell{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKCellOpt{}, \equals{SortKCellOpt{}, R} (Val:SortKCellOpt{}, inj{SortKCell{}, SortKCellOpt{}} (From:SortKCell{}))) [subsort{SortKCell{}, SortKCellOpt{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortSet{}, SortKItem{}} (From:SortSet{}))) [subsort{SortSet{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (From:SortGeneratedCounterCell{}))) [subsort{SortGeneratedCounterCell{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortState{}, SortKItem{}} (From:SortState{}))) [subsort{SortState{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedTopCell{}, SortKItem{}} (From:SortGeneratedTopCell{}))) [subsort{SortGeneratedTopCell{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortList{}, SortKItem{}} (From:SortList{}))) [subsort{SortList{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKConfigVar{}, SortKItem{}} (From:SortKConfigVar{}))) [subsort{SortKConfigVar{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortBool{}, SortKItem{}} (From:SortBool{}))) [subsort{SortBool{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortInt{}, SortKItem{}} (From:SortInt{}))) [subsort{SortInt{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (From:SortGeneratedTopCellFragment{}))) [subsort{SortGeneratedTopCellFragment{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortMap{}, SortKItem{}} (From:SortMap{}))) [subsort{SortMap{}, SortKItem{}}()] // subsort - axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, Lbl'Stop'List{}())) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'Stop'Map{}())) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, Lbl'Stop'Set{}())) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortGeneratedCounterCell{}, \equals{SortGeneratedCounterCell{}, R} (Val:SortGeneratedCounterCell{}, Lbl'-LT-'generatedCounter'-GT-'{}(K0:SortInt{}))) [functional{}()] // functional - axiom{}\implies{SortGeneratedCounterCell{}} (\and{SortGeneratedCounterCell{}} (Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{}), Lbl'-LT-'generatedCounter'-GT-'{}(Y0:SortInt{})), Lbl'-LT-'generatedCounter'-GT-'{}(\and{SortInt{}} (X0:SortInt{}, Y0:SortInt{}))) [constructor{}()] // no confusion same constructor - axiom{R} \exists{R} (Val:SortGeneratedTopCell{}, \equals{SortGeneratedTopCell{}, R} (Val:SortGeneratedTopCell{}, Lbl'-LT-'generatedTop'-GT-'{}(K0:SortKCell{}, K1:SortGeneratedCounterCell{}))) [functional{}()] // functional - axiom{}\implies{SortGeneratedTopCell{}} (\and{SortGeneratedTopCell{}} (Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortGeneratedCounterCell{}), Lbl'-LT-'generatedTop'-GT-'{}(Y0:SortKCell{}, Y1:SortGeneratedCounterCell{})), Lbl'-LT-'generatedTop'-GT-'{}(\and{SortKCell{}} (X0:SortKCell{}, Y0:SortKCell{}), \and{SortGeneratedCounterCell{}} (X1:SortGeneratedCounterCell{}, Y1:SortGeneratedCounterCell{}))) [constructor{}()] // no confusion same constructor - axiom{R} \exists{R} (Val:SortGeneratedTopCellFragment{}, \equals{SortGeneratedTopCellFragment{}, R} (Val:SortGeneratedTopCellFragment{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(K0:SortKCellOpt{}, K1:SortGeneratedCounterCellOpt{}))) [functional{}()] // functional - axiom{}\implies{SortGeneratedTopCellFragment{}} (\and{SortGeneratedTopCellFragment{}} (Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortGeneratedCounterCellOpt{}), Lbl'-LT-'generatedTop'-GT-'-fragment{}(Y0:SortKCellOpt{}, Y1:SortGeneratedCounterCellOpt{})), Lbl'-LT-'generatedTop'-GT-'-fragment{}(\and{SortKCellOpt{}} (X0:SortKCellOpt{}, Y0:SortKCellOpt{}), \and{SortGeneratedCounterCellOpt{}} (X1:SortGeneratedCounterCellOpt{}, Y1:SortGeneratedCounterCellOpt{}))) [constructor{}()] // no confusion same constructor - axiom{R} \exists{R} (Val:SortKCell{}, \equals{SortKCell{}, R} (Val:SortKCell{}, Lbl'-LT-'k'-GT-'{}(K0:SortK{}))) [functional{}()] // functional - axiom{}\implies{SortKCell{}} (\and{SortKCell{}} (Lbl'-LT-'k'-GT-'{}(X0:SortK{}), Lbl'-LT-'k'-GT-'{}(Y0:SortK{})), Lbl'-LT-'k'-GT-'{}(\and{SortK{}} (X0:SortK{}, Y0:SortK{}))) [constructor{}()] // no confusion same constructor - axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, LblListItem{}(K0:SortKItem{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblMap'Coln'update{}(K0:SortMap{}, K1:SortKItem{}, K2:SortKItem{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, LblSet'Coln'difference{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblSet'Coln'in{}(K0:SortKItem{}, K1:SortSet{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, LblSetItem{}(K0:SortKItem{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-LT-Eqls'Map'UndsUnds'MAP'Unds'Bool'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-LT-Eqls'Set'UndsUnds'SET'Unds'Bool'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional - axiom{R} \equals{SortList{}, R} (Lbl'Unds'List'Unds'{}(Lbl'Unds'List'Unds'{}(K1:SortList{},K2:SortList{}),K3:SortList{}),Lbl'Unds'List'Unds'{}(K1:SortList{},Lbl'Unds'List'Unds'{}(K2:SortList{},K3:SortList{}))) [assoc{}()] // associativity - axiom{R}\equals{SortList{}, R} (Lbl'Unds'List'Unds'{}(K:SortList{},Lbl'Stop'List{}()),K:SortList{}) [unit{}()] // right unit - axiom{R}\equals{SortList{}, R} (Lbl'Unds'List'Unds'{}(Lbl'Stop'List{}(),K:SortList{}),K:SortList{}) [unit{}()] // left unit - axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, Lbl'Unds'List'Unds'{}(K0:SortList{}, K1:SortList{}))) [functional{}()] // functional - axiom{R} \equals{SortMap{}, R} (Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(K1:SortMap{},K2:SortMap{}),K3:SortMap{}),Lbl'Unds'Map'Unds'{}(K1:SortMap{},Lbl'Unds'Map'Unds'{}(K2:SortMap{},K3:SortMap{}))) [assoc{}()] // associativity - axiom{R} \equals{SortMap{}, R} (Lbl'Unds'Map'Unds'{}(K1:SortMap{},K2:SortMap{}),Lbl'Unds'Map'Unds'{}(K2:SortMap{},K1:SortMap{})) [comm{}()] // commutativity - axiom{R}\equals{SortMap{}, R} (Lbl'Unds'Map'Unds'{}(K:SortMap{},Lbl'Stop'Map{}()),K:SortMap{}) [unit{}()] // right unit - axiom{R}\equals{SortMap{}, R} (Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),K:SortMap{}),K:SortMap{}) [unit{}()] // left unit - axiom{R} \equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(Lbl'Unds'Set'Unds'{}(K1:SortSet{},K2:SortSet{}),K3:SortSet{}),Lbl'Unds'Set'Unds'{}(K1:SortSet{},Lbl'Unds'Set'Unds'{}(K2:SortSet{},K3:SortSet{}))) [assoc{}()] // associativity - axiom{R} \equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(K1:SortSet{},K2:SortSet{}),Lbl'Unds'Set'Unds'{}(K2:SortSet{},K1:SortSet{})) [comm{}()] // commutativity - axiom{R} \equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(K:SortSet{},K:SortSet{}),K:SortSet{}) [idem{}()] // idempotency - axiom{R}\equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(K:SortSet{},Lbl'Stop'Set{}()),K:SortSet{}) [unit{}()] // right unit - axiom{R}\equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(Lbl'Stop'Set{}(),K:SortSet{}),K:SortSet{}) [unit{}()] // left unit - axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(K0:SortMap{}, K1:SortKItem{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem{}(K0:SortMap{}, K1:SortKItem{}, K2:SortKItem{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List{}(K0:SortKItem{}, K1:SortList{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(K0:SortKItem{}, K1:SortMap{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'UndsPipe'-'-GT-Unds'{}(K0:SortKItem{}, K1:SortKItem{}))) [functional{}()] // functional - axiom{R} \equals{SortSet{}, R} (Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K1:SortSet{},K2:SortSet{}),Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K2:SortSet{},K1:SortSet{})) [comm{}()] // commutativity - axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional - axiom{R} \equals{SortSet{}, R} (LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K1:SortSet{},K2:SortSet{}),LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K2:SortSet{},K1:SortSet{})) [comm{}()] // commutativity - axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisBool{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisGeneratedCounterCell{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisGeneratedCounterCellOpt{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisGeneratedTopCell{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisGeneratedTopCellFragment{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisInt{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisK{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKCell{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKCellOpt{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKConfigVar{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKItem{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisList{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisMap{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisSet{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisState{}(K0:SortK{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(K0:SortMap{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortGeneratedCounterCellOpt{}, \equals{SortGeneratedCounterCellOpt{}, R} (Val:SortGeneratedCounterCellOpt{}, LblnoGeneratedCounterCell{}())) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortKCellOpt{}, \equals{SortKCellOpt{}, R} (Val:SortKCellOpt{}, LblnoKCell{}())) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(K0:SortMap{}, K1:SortSet{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}(K0:SortList{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map{}(K0:SortMap{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(K0:SortSet{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional - axiom{} \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortGeneratedCounterCellOpt{}, inj{SortGeneratedCounterCellOpt{}, SortKItem{}} (Val:SortGeneratedCounterCellOpt{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}()))))))))))))) [constructor{}()] // no junk - axiom{} \bottom{SortList{}}() [constructor{}()] // no junk - axiom{} \or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \or{SortGeneratedCounterCellOpt{}} (LblnoGeneratedCounterCell{}(), \or{SortGeneratedCounterCellOpt{}} (\exists{SortGeneratedCounterCellOpt{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortGeneratedCounterCellOpt{}} (Val:SortGeneratedCounterCell{})), \bottom{SortGeneratedCounterCellOpt{}}())) [constructor{}()] // no junk - axiom{} \or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}()) [constructor{}()] // no junk - axiom{} \or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}()) [constructor{}()] // no junk - axiom{} \bottom{SortK{}}() [constructor{}()] // no junk - axiom{} \bottom{SortMap{}}() [constructor{}()] // no junk - axiom{} \or{SortKCellOpt{}} (LblnoKCell{}(), \or{SortKCellOpt{}} (\exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}())) [constructor{}()] // no junk - axiom{} \or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortGeneratedCounterCell{}))), \bottom{SortGeneratedTopCell{}}()) [constructor{}()] // no junk - axiom{} \bottom{SortSet{}}() [constructor{}()] // no junk - axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortGeneratedCounterCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortGeneratedCounterCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk - axiom{} \or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) - -// rules -// rule ``(``(inj{State,KItem}(#token("a","State"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token("b","State"))~>_DotVar1),_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(aba8479fef763c749fa1a1837f2591f85d8541ca8837c738cf586de790c6f8b8), label(TEST.AB), org.kframework.attributes.Location(Location(11,14,11,33)), org.kframework.attributes.Source(Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] - alias rule0LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{} - where rule0LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) := - \and{SortGeneratedTopCell{}} ( - \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) [] - - axiom{} \rewrites{SortGeneratedTopCell{}} ( - rule0LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}), - \and{SortGeneratedTopCell{}} ( - \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("b")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}))) - [label{}("TEST.AB"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(11,14,11,33)"), UNIQUE'Unds'ID{}("aba8479fef763c749fa1a1837f2591f85d8541ca8837c738cf586de790c6f8b8")] - -// rule ``(``(inj{State,KItem}(#token("a","State"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token("c","State"))~>_DotVar1),_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(3cfae148c63f879628626da1753b07d517f6ac9b414543f7dd8f7b3e8e19329e), label(TEST.AC), org.kframework.attributes.Location(Location(12,14,12,33)), org.kframework.attributes.Source(Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] - alias rule1LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{} - where rule1LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) := - \and{SortGeneratedTopCell{}} ( - \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) [] - - axiom{} \rewrites{SortGeneratedTopCell{}} ( - rule1LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}), - \and{SortGeneratedTopCell{}} ( - \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("c")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}))) - [label{}("TEST.AC"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(12,14,12,33)"), UNIQUE'Unds'ID{}("3cfae148c63f879628626da1753b07d517f6ac9b414543f7dd8f7b3e8e19329e")] - -// rule ``(``(inj{State,KItem}(#token("c","State"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token("d","State"))~>_DotVar1),_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(3b659856414a0b25778a01d888792269de4c0d88279f07da7b0d1f236c226bad), label(TEST.CD), org.kframework.attributes.Location(Location(13,14,13,33)), org.kframework.attributes.Source(Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] - alias rule2LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{} - where rule2LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) := - \and{SortGeneratedTopCell{}} ( - \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("c")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) [] - - axiom{} \rewrites{SortGeneratedTopCell{}} ( - rule2LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}), - \and{SortGeneratedTopCell{}} ( - \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("d")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}))) - [label{}("TEST.CD"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(13,14,13,33)"), UNIQUE'Unds'ID{}("3b659856414a0b25778a01d888792269de4c0d88279f07da7b0d1f236c226bad")] - -// rule `_|Set__SET_Set_Set_Set`(S1,S2)=>`_Set_`(S1,`Set:difference`(S2,S1)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e9a710d8d1ca5c799420161879cbbff926de45a5bddd820d646f51d43eb67e62), concrete, org.kframework.attributes.Location(Location(559,8,559,45)), org.kframework.attributes.Source(Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortSet{}, R} ( - X0:SortSet{}, - VarS1:SortSet{} - ),\and{R} ( - \in{SortSet{}, R} ( - X1:SortSet{}, - VarS2:SortSet{} - ), - \top{R} () - ))), - \equals{SortSet{},R} ( - Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(X0:SortSet{},X1:SortSet{}), - \and{SortSet{}} ( - Lbl'Unds'Set'Unds'{}(VarS1:SortSet{},LblSet'Coln'difference{}(VarS2:SortSet{},VarS1:SortSet{})), - \top{SortSet{}}()))) - [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/sxlm4w731fhxy1cihwbv2flwd6xb90im-k-5.5.86-e25a8597d787d6b22eae989c85d9d0262b0539fd-maven/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(559,8,559,45)"), UNIQUE'Unds'ID{}("e9a710d8d1ca5c799420161879cbbff926de45a5bddd820d646f51d43eb67e62")] - -// rule getGeneratedCounterCell(``(_DotVar0,Cell))=>Cell requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortGeneratedTopCell{}, R} ( - X0:SortGeneratedTopCell{}, - Lbl'-LT-'generatedTop'-GT-'{}(Var'Unds'DotVar0:SortKCell{},VarCell:SortGeneratedCounterCell{}) - ), - \top{R} () - )), - \equals{SortGeneratedCounterCell{},R} ( - LblgetGeneratedCounterCell{}(X0:SortGeneratedTopCell{}), - \and{SortGeneratedCounterCell{}} ( - VarCell:SortGeneratedCounterCell{}, - \top{SortGeneratedCounterCell{}}()))) - [] - -// rule initGeneratedCounterCell(.KList)=>``(#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [initializer] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - - \top{R} () - ), - \equals{SortGeneratedCounterCell{},R} ( - LblinitGeneratedCounterCell{}(), - \and{SortGeneratedCounterCell{}} ( - Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")), - \top{SortGeneratedCounterCell{}}()))) - [initializer{}()] - -// rule initGeneratedTopCell(Init)=>``(initKCell(Init),initGeneratedCounterCell(.KList)) requires #token("true","Bool") ensures #token("true","Bool") [initializer] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortMap{}, R} ( - X0:SortMap{}, - VarInit:SortMap{} - ), - \top{R} () - )), - \equals{SortGeneratedTopCell{},R} ( - LblinitGeneratedTopCell{}(X0:SortMap{}), - \and{SortGeneratedTopCell{}} ( - Lbl'-LT-'generatedTop'-GT-'{}(LblinitKCell{}(VarInit:SortMap{}),LblinitGeneratedCounterCell{}()), - \top{SortGeneratedTopCell{}}()))) - [initializer{}()] - -// rule initKCell(Init)=>``(inj{State,KItem}(`project:State`(`Map:lookup`(Init,inj{KConfigVar,KItem}(#token("$PGM","KConfigVar")))))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(64786fd44ad73c13ddf8b9aaecebe5256c7a4102003fdf068a91202656965b95), initializer] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortMap{}, R} ( - X0:SortMap{}, - VarInit:SortMap{} - ), - \top{R} () - )), - \equals{SortKCell{},R} ( - LblinitKCell{}(X0:SortMap{}), - \and{SortKCell{}} ( - Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(Lblproject'Coln'State{}(kseq{}(LblMap'Coln'lookup{}(VarInit:SortMap{},inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM"))),dotk{}()))),dotk{}())), - \top{SortKCell{}}()))) - [initializer{}(), UNIQUE'Unds'ID{}("64786fd44ad73c13ddf8b9aaecebe5256c7a4102003fdf068a91202656965b95")] - -// rule isBool(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen0:SortBool{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortBool{}, SortKItem{}}(Var'Unds'Gen0:SortBool{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisBool{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isBool(inj{Bool,KItem}(Bool))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortBool{}, SortKItem{}}(VarBool:SortBool{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisBool{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isGeneratedCounterCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortGeneratedCounterCell{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(Var'Unds'Gen1:SortGeneratedCounterCell{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisGeneratedCounterCell{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isGeneratedCounterCell(inj{GeneratedCounterCell,KItem}(GeneratedCounterCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(VarGeneratedCounterCell:SortGeneratedCounterCell{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisGeneratedCounterCell{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isGeneratedCounterCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortGeneratedCounterCellOpt{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCellOpt{}, SortKItem{}}(Var'Unds'Gen1:SortGeneratedCounterCellOpt{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisGeneratedCounterCellOpt{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isGeneratedCounterCellOpt(inj{GeneratedCounterCellOpt,KItem}(GeneratedCounterCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCellOpt{}, SortKItem{}}(VarGeneratedCounterCellOpt:SortGeneratedCounterCellOpt{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisGeneratedCounterCellOpt{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isGeneratedTopCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortGeneratedTopCell{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(Var'Unds'Gen1:SortGeneratedTopCell{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisGeneratedTopCell{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isGeneratedTopCell(inj{GeneratedTopCell,KItem}(GeneratedTopCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(VarGeneratedTopCell:SortGeneratedTopCell{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisGeneratedTopCell{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isGeneratedTopCellFragment(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen0:SortGeneratedTopCellFragment{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedTopCellFragment{}, SortKItem{}}(Var'Unds'Gen0:SortGeneratedTopCellFragment{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisGeneratedTopCellFragment{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isGeneratedTopCellFragment(inj{GeneratedTopCellFragment,KItem}(GeneratedTopCellFragment))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedTopCellFragment{}, SortKItem{}}(VarGeneratedTopCellFragment:SortGeneratedTopCellFragment{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisGeneratedTopCellFragment{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isInt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortInt{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortInt{}, SortKItem{}}(Var'Unds'Gen1:SortInt{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisInt{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isInt(inj{Int,KItem}(Int))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortInt{}, SortKItem{}}(VarInt:SortInt{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisInt{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isK(K)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisK{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isKCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortKCell{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKCell{}, SortKItem{}}(Var'Unds'Gen1:SortKCell{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisKCell{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isKCell(inj{KCell,KItem}(KCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKCell{}, SortKItem{}}(VarKCell:SortKCell{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisKCell{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isKCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen0:SortKCellOpt{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKCellOpt{}, SortKItem{}}(Var'Unds'Gen0:SortKCellOpt{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisKCellOpt{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isKCellOpt(inj{KCellOpt,KItem}(KCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKCellOpt{}, SortKItem{}}(VarKCellOpt:SortKCellOpt{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisKCellOpt{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isKConfigVar(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortKConfigVar{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKConfigVar{}, SortKItem{}}(Var'Unds'Gen1:SortKConfigVar{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisKConfigVar{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isKConfigVar(inj{KConfigVar,KItem}(KConfigVar))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKConfigVar{}, SortKItem{}}(VarKConfigVar:SortKConfigVar{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisKConfigVar{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isKItem(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortKItem{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(Var'Unds'Gen1:SortKItem{},dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisKItem{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isKItem(KItem)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(VarKItem:SortKItem{},dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisKItem{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isList(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen0:SortList{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortList{}, SortKItem{}}(Var'Unds'Gen0:SortList{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisList{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isList(inj{List,KItem}(List))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortList{}, SortKItem{}}(VarList:SortList{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisList{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isMap(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen1:SortMap{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortMap{}, SortKItem{}}(Var'Unds'Gen1:SortMap{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisMap{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isMap(inj{Map,KItem}(Map))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortMap{}, SortKItem{}}(VarMap:SortMap{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisMap{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isSet(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen0:SortSet{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortSet{}, SortKItem{}}(Var'Unds'Gen0:SortSet{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisSet{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isSet(inj{Set,KItem}(Set))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortSet{}, SortKItem{}}(VarSet:SortSet{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisSet{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule isState(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise] - axiom{R} \implies{R} ( - \and{R} ( - \not{R} ( - \or{R} ( - \exists{R} (Var'Unds'Gen0:SortState{}, - \and{R} ( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortState{}, SortKItem{}}(Var'Unds'Gen0:SortState{}),dotk{}()) - ), - \top{R} () - ) - )), - \bottom{R}() - ) - ), - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - ) - )), - \equals{SortBool{},R} ( - LblisState{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("false"), - \top{SortBool{}}()))) - [owise{}()] - -// rule isState(inj{State,KItem}(State))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortState{}, SortKItem{}}(VarState:SortState{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - LblisState{}(X0:SortK{}), - \and{SortBool{}} ( - \dv{SortBool{}}("true"), - \top{SortBool{}}()))) - [] - -// rule `project:Bool`(inj{Bool,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortBool{}, SortKItem{}}(VarK:SortBool{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortBool{},R} ( - Lblproject'Coln'Bool{}(X0:SortK{}), - \and{SortBool{}} ( - VarK:SortBool{}, - \top{SortBool{}}()))) - [projection{}()] - -// rule `project:GeneratedCounterCell`(inj{GeneratedCounterCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(VarK:SortGeneratedCounterCell{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortGeneratedCounterCell{},R} ( - Lblproject'Coln'GeneratedCounterCell{}(X0:SortK{}), - \and{SortGeneratedCounterCell{}} ( - VarK:SortGeneratedCounterCell{}, - \top{SortGeneratedCounterCell{}}()))) - [projection{}()] - -// rule `project:GeneratedCounterCellOpt`(inj{GeneratedCounterCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCellOpt{}, SortKItem{}}(VarK:SortGeneratedCounterCellOpt{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortGeneratedCounterCellOpt{},R} ( - Lblproject'Coln'GeneratedCounterCellOpt{}(X0:SortK{}), - \and{SortGeneratedCounterCellOpt{}} ( - VarK:SortGeneratedCounterCellOpt{}, - \top{SortGeneratedCounterCellOpt{}}()))) - [projection{}()] - -// rule `project:GeneratedTopCell`(inj{GeneratedTopCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(VarK:SortGeneratedTopCell{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortGeneratedTopCell{},R} ( - Lblproject'Coln'GeneratedTopCell{}(X0:SortK{}), - \and{SortGeneratedTopCell{}} ( - VarK:SortGeneratedTopCell{}, - \top{SortGeneratedTopCell{}}()))) - [projection{}()] - -// rule `project:GeneratedTopCellFragment`(inj{GeneratedTopCellFragment,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortGeneratedTopCellFragment{}, SortKItem{}}(VarK:SortGeneratedTopCellFragment{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortGeneratedTopCellFragment{},R} ( - Lblproject'Coln'GeneratedTopCellFragment{}(X0:SortK{}), - \and{SortGeneratedTopCellFragment{}} ( - VarK:SortGeneratedTopCellFragment{}, - \top{SortGeneratedTopCellFragment{}}()))) - [projection{}()] - -// rule `project:Int`(inj{Int,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortInt{}, SortKItem{}}(VarK:SortInt{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortInt{},R} ( - Lblproject'Coln'Int{}(X0:SortK{}), - \and{SortInt{}} ( - VarK:SortInt{}, - \top{SortInt{}}()))) - [projection{}()] - -// rule `project:K`(K)=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - VarK:SortK{} - ), - \top{R} () - )), - \equals{SortK{},R} ( - Lblproject'Coln'K{}(X0:SortK{}), - \and{SortK{}} ( - VarK:SortK{}, - \top{SortK{}}()))) - [projection{}()] - -// rule `project:KCell`(inj{KCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKCell{}, SortKItem{}}(VarK:SortKCell{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortKCell{},R} ( - Lblproject'Coln'KCell{}(X0:SortK{}), - \and{SortKCell{}} ( - VarK:SortKCell{}, - \top{SortKCell{}}()))) - [projection{}()] - -// rule `project:KCellOpt`(inj{KCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortKCellOpt{}, SortKItem{}}(VarK:SortKCellOpt{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortKCellOpt{},R} ( - Lblproject'Coln'KCellOpt{}(X0:SortK{}), - \and{SortKCellOpt{}} ( - VarK:SortKCellOpt{}, - \top{SortKCellOpt{}}()))) - [projection{}()] - -// rule `project:KItem`(K)=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(VarK:SortKItem{},dotk{}()) - ), - \top{R} () - )), - \equals{SortKItem{},R} ( - Lblproject'Coln'KItem{}(X0:SortK{}), - \and{SortKItem{}} ( - VarK:SortKItem{}, - \top{SortKItem{}}()))) - [projection{}()] - -// rule `project:List`(inj{List,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortList{}, SortKItem{}}(VarK:SortList{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortList{},R} ( - Lblproject'Coln'List{}(X0:SortK{}), - \and{SortList{}} ( - VarK:SortList{}, - \top{SortList{}}()))) - [projection{}()] - -// rule `project:Map`(inj{Map,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortMap{}, SortKItem{}}(VarK:SortMap{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortMap{},R} ( - Lblproject'Coln'Map{}(X0:SortK{}), - \and{SortMap{}} ( - VarK:SortMap{}, - \top{SortMap{}}()))) - [projection{}()] - -// rule `project:Set`(inj{Set,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortSet{}, SortKItem{}}(VarK:SortSet{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortSet{},R} ( - Lblproject'Coln'Set{}(X0:SortK{}), - \and{SortSet{}} ( - VarK:SortSet{}, - \top{SortSet{}}()))) - [projection{}()] - -// rule `project:State`(inj{State,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [projection] - axiom{R} \implies{R} ( - \and{R}( - \top{R}(), - \and{R} ( - \in{SortK{}, R} ( - X0:SortK{}, - kseq{}(inj{SortState{}, SortKItem{}}(VarK:SortState{}),dotk{}()) - ), - \top{R} () - )), - \equals{SortState{},R} ( - Lblproject'Coln'State{}(X0:SortK{}), - \and{SortState{}} ( - VarK:SortState{}, - \top{SortState{}}()))) - [projection{}()] - -// rule #Ceil{Map,#SortParam}(`_Map_`(`_|->_`(@K0,@K1),@Rest))=>#And{#SortParam}(#Equals{Bool,#SortParam}(`_in_keys(_)_MAP_Bool_KItem_Map`(@K0,@Rest),#token("false","Bool")),#And{#SortParam}(#Top{#SortParam}(.KList),#Ceil{KItem,#SortParam}(@K1))) requires #token("true","Bool") ensures #token("true","Bool") [simplification, sortParams({Q0})] - axiom{R,Q0} \implies{R} ( - \top{R}(), - \equals{Q0,R} ( - \ceil{SortMap{}, Q0}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(@VarK0:SortKItem{},@VarK1:SortKItem{}),@VarRest:SortMap{})), - \and{Q0} ( - \and{Q0}(\equals{SortBool{}, Q0}(Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(@VarK0:SortKItem{},@VarRest:SortMap{}),\dv{SortBool{}}("false")),\and{Q0}(\top{Q0}(),\ceil{SortKItem{}, Q0}(@VarK1:SortKItem{}))), - \top{Q0}()))) - [simplification{}(), sortParams{}()] - - -// priority groups -endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1,1,18,10)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/hs-backend-booster/test/rpc-integration/resources/module-addition/test.k)")] diff --git a/test/rpc-server/add-module/add-again/params.json b/test/rpc-server/add-module/add-again/params.json deleted file mode 100644 index fc7794705a..0000000000 --- a/test/rpc-server/add-module/add-again/params.json +++ /dev/null @@ -1,4 +0,0 @@ -{ - "module" : "module NEW\n import TEST []\n\n// rule ``(``(inj{State,KItem}(#token(\"d\",\"State\"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859), label(NEW.DE), org.kframework.attributes.Location(Location(10,14,10,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule3LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"d\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.DE\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(10,14,10,33)\")]\n\n// rule ``(``(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token(\"f\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(326083bfd90582092d450c8db2c16552b080ed66344a5d424a189caab7fe33ef), label(NEW.EF), org.kframework.attributes.Location(Location(11,14,11,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule4LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"f\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.EF\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(11,14,11,33)\")]\n\n\nendmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(3,1,13,10)\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\")]\n", - "name-as-id": true -} diff --git a/test/rpc-server/add-module/add-again/response.golden b/test/rpc-server/add-module/add-again/response.golden deleted file mode 100644 index e59aae8743..0000000000 --- a/test/rpc-server/add-module/add-again/response.golden +++ /dev/null @@ -1 +0,0 @@ -{"jsonrpc":"2.0","id":1,"result":{"module":"m8e723e34b156f187e7cce8658dbb513244788a1ab81c1f496b909b1a2d1cc0c3"}} diff --git a/test/rpc-server/add-module/add/params.json b/test/rpc-server/add-module/add/params.json index fc7794705a..ac1cd567c3 100644 --- a/test/rpc-server/add-module/add/params.json +++ b/test/rpc-server/add-module/add/params.json @@ -1,4 +1,3 @@ { - "module" : "module NEW\n import TEST []\n\n// rule ``(``(inj{State,KItem}(#token(\"d\",\"State\"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859), label(NEW.DE), org.kframework.attributes.Location(Location(10,14,10,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule3LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"d\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.DE\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(10,14,10,33)\")]\n\n// rule ``(``(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token(\"f\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(326083bfd90582092d450c8db2c16552b080ed66344a5d424a189caab7fe33ef), label(NEW.EF), org.kframework.attributes.Location(Location(11,14,11,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule4LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"f\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.EF\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(11,14,11,33)\")]\n\n\nendmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(3,1,13,10)\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\")]\n", - "name-as-id": true + "module" : "module NEW\n import TEST []\n\n// rule ``(``(inj{State,KItem}(#token(\"d\",\"State\"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859), label(NEW.DE), org.kframework.attributes.Location(Location(10,14,10,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule3LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"d\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule3LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.DE\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(10,14,10,33)\")]\n\n// rule ``(``(inj{State,KItem}(#token(\"e\",\"State\"))~>_DotVar1),_DotVar0)=>``(``(inj{State,KItem}(#token(\"f\",\"State\"))~>_DotVar1),_DotVar0) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [UNIQUE_ID(326083bfd90582092d450c8db2c16552b080ed66344a5d424a189caab7fe33ef), label(NEW.EF), org.kframework.attributes.Location(Location(11,14,11,33)), org.kframework.attributes.Source(rpc-request), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]\n alias rule4LHS{}(SortGeneratedCounterCell{},SortK{}) : SortGeneratedTopCell{}\n where rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}) :=\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"e\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})) []\n\n axiom{} \\rewrites{SortGeneratedTopCell{}} (\n rule4LHS{}(Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'DotVar1:SortK{}),\n \\and{SortGeneratedTopCell{}} (\n \\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\\dv{SortState{}}(\"f\")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})))\n [label{}(\"NEW.EF\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\"), org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(11,14,11,33)\")]\n\n\nendmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(\"Location(3,1,13,10)\"), org'Stop'kframework'Stop'attributes'Stop'Source{}(\"rpc-request\")]\n" } diff --git a/test/rpc-server/add-module/add/response.golden b/test/rpc-server/add-module/add/response.golden index e59aae8743..026d7878bd 100644 --- a/test/rpc-server/add-module/add/response.golden +++ b/test/rpc-server/add-module/add/response.golden @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"result":{"module":"m8e723e34b156f187e7cce8658dbb513244788a1ab81c1f496b909b1a2d1cc0c3"}} +{"jsonrpc":"2.0","id":1,"result":{"module":"NEW"}}