Prove claims in fixed order (#2199)

* Prove claims in fixed order

* Remove test draft

* Unit test

* Adressed comments

* Hlint

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: andreiburdusa

kore/app/share/GlobalMain.hs

@@ -31,7 +31,14 @@ import Prelude.Kore
 import Control.Exception
     ( evaluate
     )
+import Control.Lens
+    ( (%~)
+    )
+import qualified Control.Lens as Lens
 import qualified Control.Monad as Monad
+import Data.Functor
+    ( (<&>)
+    )
 import Data.List
     ( intercalate
     )
@@ -106,7 +113,8 @@ import System.Clock
 import qualified System.Environment as Env
 
 import Kore.ASTVerifier.DefinitionVerifier
-    ( verifyAndIndexDefinitionWithBase
+    ( sortModuleClaims
+    , verifyAndIndexDefinitionWithBase
     )
 import Kore.ASTVerifier.PatternVerifier as PatternVerifier
 import qualified Kore.Attribute.Symbol as Attribute
@@ -518,8 +526,14 @@ type LoadedDefinition = (Map ModuleName LoadedModule, Map Text AstLocation)
 
 loadDefinitions :: [FilePath] -> Main LoadedDefinition
 loadDefinitions filePaths =
-    Monad.foldM verifyDefinitionWithBase mempty
-    =<< traverse parseDefinition filePaths
+    loadedDefinitions <&> sortClaims
+  where
+    loadedDefinitions =
+        Monad.foldM verifyDefinitionWithBase mempty
+        =<< traverse parseDefinition filePaths
+
+    sortClaims :: LoadedDefinition -> LoadedDefinition
+    sortClaims = Lens._1 . Lens.traversed %~ sortModuleClaims
 
 loadModule :: ModuleName -> LoadedDefinition -> Main LoadedModule
 loadModule moduleName = lookupMainModule moduleName . fst

kore/src/Kore/ASTVerifier/DefinitionVerifier.hs

@@ -11,14 +11,24 @@ module Kore.ASTVerifier.DefinitionVerifier
     ( verifyDefinition
     , verifyAndIndexDefinition
     , verifyAndIndexDefinitionWithBase
+    , sortModuleClaims
     ) where
 
 import Prelude.Kore
 
+import Control.Lens
+    ( (%~)
+    )
 import Control.Monad
     ( foldM
     )
 import qualified Data.Foldable as Foldable
+import Data.Generics.Product
+    ( field
+    )
+import Data.List
+    ( sortOn
+    )
 import Data.Map.Strict
     ( Map
     )
@@ -138,3 +148,11 @@ verifyAndIndexDefinitionWithBase
     return (index, names)
   where
     modulesByName = Map.fromList . map (\m -> (moduleName m, m))
+
+sortModuleClaims
+    :: VerifiedModule declAtts
+    -> VerifiedModule declAtts
+sortModuleClaims verifiedModule =
+    verifiedModule
+    & field @"indexedModuleClaims"
+        %~ sortOn (Attribute.sourceLocation . fst)

kore/test/Test/Kore.hs

@@ -28,6 +28,8 @@ module Test.Kore
     , couple
     , symbolOrAliasGen
     , addVariable
+    , sentenceAxiomGen
+    , korePatternUnifiedGen
       -- * Re-exports
     , ParsedPattern
     , asParsedPattern

kore/test/Test/Kore/Builtin.hs

@@ -1,5 +1,6 @@
 module Test.Kore.Builtin
     ( test_internalize
+    , test_sortModuleClaims
     ) where
 
 import Prelude.Kore hiding
@@ -9,14 +10,36 @@ import Prelude.Kore hiding
 import Test.Tasty
 import Test.Tasty.HUnit
 
+import Control.Lens
+    ( ix
+    , (%~)
+    , (.~)
+    )
+import qualified Control.Lens as Lens
+import Data.Generics.Product
+    ( field
+    )
 import qualified Data.Set
 
+import Kore.ASTVerifier.DefinitionVerifier
+    ( sortModuleClaims
+    )
+import Kore.Attribute.Axiom
+    ( SourceLocation
+    )
 import qualified Kore.Attribute.Symbol as Attribute
 import qualified Kore.Builtin as Kore
+import Kore.IndexedModule.IndexedModule
+    ( IndexedModule (..)
+    , VerifiedModule
+    )
 import Kore.IndexedModule.MetadataTools
     ( SmtMetadataTools
     )
 import Kore.Internal.TermLike
+import Test.Kore.Step.SMT.Builders
+    ( indexModule
+    )
 
 import qualified Test.Kore.Builtin.Builtin as Builtin
 import qualified Test.Kore.Builtin.Definition as Builtin
@@ -151,3 +174,25 @@ notInternalizes name origin =
 
 metadata :: SmtMetadataTools Attribute.Symbol
 metadata = Builtin.testMetadataTools
+
+test_sortModuleClaims :: TestTree
+test_sortModuleClaims =
+    testCase "sort claims" $ do
+        let verifiedModule =
+                indexModule Builtin.testModuleWithTwoClaims
+                & ixSetLocation 0 (from $ FileLocation "file" 5 3)
+                & ixSetLocation 1 (from $ FileLocation "file" 1 1)
+            withSortedClaims = sortModuleClaims verifiedModule
+        assertEqual ""
+            (indexedModuleClaims withSortedClaims)
+            (indexedModuleClaims verifiedModule & reverse)
+  where
+    ixSetLocation
+        :: Int
+        -> SourceLocation
+        -> VerifiedModule declAtts
+        -> VerifiedModule declAtts
+    ixSetLocation index sourceLocation verifiedModule =
+        verifiedModule
+        & field @"indexedModuleClaims"
+            %~ (ix index . Lens._1 . field @"sourceLocation" .~ sourceLocation)

kore/test/Test/Kore/Builtin/Definition.hs

@@ -55,7 +55,11 @@ import Kore.Internal.TermLike hiding
     ( Symbol
     , bytesSort
     )
+import Kore.Syntax
+    ( Const (..)
+    )
 import Kore.Syntax.Definition as Syntax
+import qualified Kore.Syntax.PatternF as PatternF
 
 import Test.Kore
 import qualified Test.Kore.Step.MockSymbols as Mock
@@ -1747,6 +1751,42 @@ testModule =
             ]
         }
 
+testModuleWithTwoClaims :: ParsedModule
+testModuleWithTwoClaims =
+    Module
+        { moduleName = testModuleName
+        , moduleAttributes = Attributes []
+        , moduleSentences =
+            [ SentenceClaimSentence . SentenceClaim $
+                (SentenceAxiom
+                    { sentenceAxiomParameters = [SortVariable (testId "sv1")]
+                    , sentenceAxiomPattern =
+                        Builtin.externalize (mkStringLiteral "a")
+                    , sentenceAxiomAttributes =
+                        Attributes
+                            [ asParsedPattern
+                                $ PatternF.StringLiteralF
+                                $ Const (StringLiteral "b")
+                            ]
+                    }
+                :: ParsedSentenceAxiom)
+            , SentenceClaimSentence . SentenceClaim $
+                (SentenceAxiom
+                    { sentenceAxiomParameters = [SortVariable (testId "sv2")]
+                    , sentenceAxiomPattern =
+                        Builtin.externalize (mkStringLiteral "c")
+                    , sentenceAxiomAttributes =
+                        Attributes
+                            [ asParsedPattern
+                                $ PatternF.StringLiteralF
+                                $ Const (StringLiteral "b")
+                            ]
+                    }
+                :: ParsedSentenceAxiom)
+            ]
+        }
+
+
 -- -------------------------------------------------------------
 -- * Definition