Extract axioms from spec module and add to definition (#2938)

* Extract axioms from spec module and add to definition

* Move implementation at the very top level

* Format with fourmolu

* Implement for kore-repl as well

* Format with fourmolu

* Add documentation

* Format with fourmolu

* Retrigger build

* Materialize Nix expressions

* Review: add suggestion

Co-authored-by: github-actions <[email protected]>

Author: ana-pantilie

kore/app/exec/Main.hs

@@ -688,18 +688,19 @@ koreProve execOptions proveOptions = do
     mainModule <- loadModule mainModuleName definition
     let KoreProveOptions{specMainModule} = proveOptions
     specModule <- loadModule specMainModule definition
+    let mainModule' = addExtraAxioms mainModule specModule
     let KoreProveOptions{saveProofs} = proveOptions
     maybeAlreadyProvenModule <- loadProven definitionFileName saveProofs
     let KoreExecOptions{maxCounterexamples} = execOptions
-    proveResult <- execute execOptions mainModule $ do
+    proveResult <- execute execOptions mainModule' $ do
         let KoreExecOptions{breadthLimit, depthLimit} = execOptions
             KoreProveOptions{graphSearch} = proveOptions
         prove
             graphSearch
             breadthLimit
             depthLimit
             maxCounterexamples
-            mainModule
+            mainModule'
             specModule
             maybeAlreadyProvenModule
 

kore/app/repl/Main.hs

@@ -220,7 +220,9 @@ mainWithOptions
                                 indexedModule <- loadModule mainModuleName definition
                                 specDefIndexedModule <- loadModule specModule definition
 
-                                let smtConfig =
+                                let validatedDefinition =
+                                        addExtraAxioms indexedModule specDefIndexedModule
+                                    smtConfig =
                                         SMT.defaultConfig
                                             { SMT.timeOut = smtTimeOut
                                             , SMT.rLimit = smtRLimit
@@ -253,11 +255,11 @@ mainWithOptions
                                 SMT.runSMT
                                     smtConfig
                                     ( give
-                                        (MetadataTools.build indexedModule)
-                                        (declareSMTLemmas indexedModule)
+                                        (MetadataTools.build validatedDefinition)
+                                        (declareSMTLemmas validatedDefinition)
                                     )
                                     $ proveWithRepl
-                                        indexedModule
+                                        validatedDefinition
                                         specDefIndexedModule
                                         Nothing
                                         mvarLogAction

kore/app/share/GlobalMain.hs

@@ -24,16 +24,21 @@ module GlobalMain (
     loadModule,
     mainParseSearchPattern,
     mainPatternParseAndVerify,
+    addExtraAxioms,
 ) where
 
 import Control.Exception (
     evaluate,
  )
 import Control.Lens (
     (%~),
+    (<>~),
  )
 import qualified Control.Lens as Lens
 import qualified Control.Monad as Monad
+import Data.Generics.Product (
+    field,
+ )
 import Data.List (
     intercalate,
     nub,
@@ -68,6 +73,7 @@ import qualified Kore.Attribute.Symbol as Attribute (
  )
 import qualified Kore.Builtin as Builtin
 import Kore.IndexedModule.IndexedModule (
+    IndexedModule (indexedModuleAxioms),
     VerifiedModule,
  )
 import Kore.Internal.Conditional (Conditional (..))
@@ -560,3 +566,16 @@ mainPatternParseAndVerify indexedModule patternFileName =
 -}
 mainPatternParse :: String -> Main ParsedPattern
 mainPatternParse = mainParse parseKorePattern
+
+{- | Extract axioms from a module and add them to the main definition module.
+ This should be safe, as long as the axioms only depend on sorts/symbols
+ defined in the main module.
+-}
+addExtraAxioms ::
+    VerifiedModule StepperAttributes ->
+    VerifiedModule StepperAttributes ->
+    VerifiedModule StepperAttributes
+addExtraAxioms definitionModule moduleWithExtraAxioms =
+    definitionModule
+        & field @"indexedModuleAxioms"
+        <>~ indexedModuleAxioms moduleWithExtraAxioms

kore/kore.cabal

@@ -104,6 +104,7 @@ common global-main
   build-depends: clock >=0.8
   build-depends: containers >=0.5
   build-depends: filepath >=1.4
+  build-depends: generic-lens >=1.1
   build-depends: lens >=4.17
   build-depends: megaparsec >=7.0
   build-depends: optparse-applicative >=0.14

nix/kore.nix.d/kore.nix

@@ -473,6 +473,7 @@
             (hsPkgs."clock" or (errorHandler.buildDepError "clock"))
             (hsPkgs."containers" or (errorHandler.buildDepError "containers"))
             (hsPkgs."filepath" or (errorHandler.buildDepError "filepath"))
+            (hsPkgs."generic-lens" or (errorHandler.buildDepError "generic-lens"))
             (hsPkgs."lens" or (errorHandler.buildDepError "lens"))
             (hsPkgs."megaparsec" or (errorHandler.buildDepError "megaparsec"))
             (hsPkgs."optparse-applicative" or (errorHandler.buildDepError "optparse-applicative"))
@@ -481,7 +482,6 @@
             (hsPkgs."directory" or (errorHandler.buildDepError "directory"))
             (hsPkgs."exceptions" or (errorHandler.buildDepError "exceptions"))
             (hsPkgs."extra" or (errorHandler.buildDepError "extra"))
-            (hsPkgs."generic-lens" or (errorHandler.buildDepError "generic-lens"))
             (hsPkgs."reflection" or (errorHandler.buildDepError "reflection"))
             ];
           buildable = true;
@@ -500,6 +500,7 @@
             (hsPkgs."clock" or (errorHandler.buildDepError "clock"))
             (hsPkgs."containers" or (errorHandler.buildDepError "containers"))
             (hsPkgs."filepath" or (errorHandler.buildDepError "filepath"))
+            (hsPkgs."generic-lens" or (errorHandler.buildDepError "generic-lens"))
             (hsPkgs."lens" or (errorHandler.buildDepError "lens"))
             (hsPkgs."megaparsec" or (errorHandler.buildDepError "megaparsec"))
             (hsPkgs."optparse-applicative" or (errorHandler.buildDepError "optparse-applicative"))
@@ -521,6 +522,7 @@
             (hsPkgs."clock" or (errorHandler.buildDepError "clock"))
             (hsPkgs."containers" or (errorHandler.buildDepError "containers"))
             (hsPkgs."filepath" or (errorHandler.buildDepError "filepath"))
+            (hsPkgs."generic-lens" or (errorHandler.buildDepError "generic-lens"))
             (hsPkgs."lens" or (errorHandler.buildDepError "lens"))
             (hsPkgs."megaparsec" or (errorHandler.buildDepError "megaparsec"))
             (hsPkgs."optparse-applicative" or (errorHandler.buildDepError "optparse-applicative"))
@@ -557,6 +559,7 @@
             (hsPkgs."clock" or (errorHandler.buildDepError "clock"))
             (hsPkgs."containers" or (errorHandler.buildDepError "containers"))
             (hsPkgs."filepath" or (errorHandler.buildDepError "filepath"))
+            (hsPkgs."generic-lens" or (errorHandler.buildDepError "generic-lens"))
             (hsPkgs."lens" or (errorHandler.buildDepError "lens"))
             (hsPkgs."megaparsec" or (errorHandler.buildDepError "megaparsec"))
             (hsPkgs."optparse-applicative" or (errorHandler.buildDepError "optparse-applicative"))
@@ -580,6 +583,7 @@
             (hsPkgs."clock" or (errorHandler.buildDepError "clock"))
             (hsPkgs."containers" or (errorHandler.buildDepError "containers"))
             (hsPkgs."filepath" or (errorHandler.buildDepError "filepath"))
+            (hsPkgs."generic-lens" or (errorHandler.buildDepError "generic-lens"))
             (hsPkgs."lens" or (errorHandler.buildDepError "lens"))
             (hsPkgs."megaparsec" or (errorHandler.buildDepError "megaparsec"))
             (hsPkgs."optparse-applicative" or (errorHandler.buildDepError "optparse-applicative"))
@@ -602,6 +606,7 @@
             (hsPkgs."clock" or (errorHandler.buildDepError "clock"))
             (hsPkgs."containers" or (errorHandler.buildDepError "containers"))
             (hsPkgs."filepath" or (errorHandler.buildDepError "filepath"))
+            (hsPkgs."generic-lens" or (errorHandler.buildDepError "generic-lens"))
             (hsPkgs."lens" or (errorHandler.buildDepError "lens"))
             (hsPkgs."megaparsec" or (errorHandler.buildDepError "megaparsec"))
             (hsPkgs."optparse-applicative" or (errorHandler.buildDepError "optparse-applicative"))