Reuse exact separation validation

1 files changed, 114 insertions, 13 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index d819692..fee5aa4 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -37,7 +37,7 @@ import Data.ByteString qualified as ByteString
 import Data.Text qualified as StrictText
 import Data.Text.Encoding qualified as Text
 import Control.Monad.Logger (runNoLoggingT)
-import Data.IORef (modifyIORef', newIORef, readIORef)
+import Data.IORef (IORef, modifyIORef', newIORef, readIORef)
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Vector qualified as Vector
@@ -75,6 +75,8 @@ unitTests =
             compilesExactOrdinaryProofs
         , testCase "compiles exact separation comprehensions"
             compilesExactSeparationComprehensions
+        , testCase "reuses exact separation validation"
+            reusesExactSeparationValidation
         , testCase "compiles exact source axioms"
             compilesExactSourceAxioms
         , testCase "rejects source-axiom assumptions"
@@ -842,6 +844,102 @@ assertExactSeparationModule label sealed = do
                 (label <> ": expected definition and theorem, found "
                     <> show (length batches))
 
+reusesExactSeparationValidation :: Assertion
+reusesExactSeparationValidation =
+    Temp.withSystemTempDirectory "felix-exact-separation-cache" \root -> do
+        let relative = "test/phase5/exact-separation.tex"
+            sourcePath = root Posix.</> relative
+            executable = root Posix.</> "vampire"
+            storePath = root Posix.</> "store.sqlite"
+        createDirectoryIfMissing True (Posix.takeDirectory sourcePath)
+        ByteString.readFile relative >>= ByteString.writeFile sourcePath
+        writeFile executable
+            (unlines
+                [ "#!/bin/sh"
+                , "cat >/dev/null"
+                , "printf '%s\\n' '% SZS status Theorem for exact-separation-cache'"
+                ])
+        permissions <- getPermissions executable
+        setPermissions executable
+            (setOwnerExecutable True permissions)
+        foundation <- expectRight Foundation.checkedFoundation
+        bootstrap <-
+            expectRight
+                =<< Module.buildBootstrapPreludeSession
+                    foundation
+                    unusedResolver
+        mounts <- exactFixtureMounts root
+        workspace <- parseExactWorkspace bootstrap mounts relative
+        freshRuns <- newIORef (0 :: Int)
+        freshModules <-
+            compileParsedWorkspaceWithValidation
+                foundation
+                bootstrap
+                (countingAcceptedResolver executable freshRuns)
+                Declaration.FreshValidation
+                workspace
+        assertEqual "fresh separation proof runs Vampire once"
+            1
+            =<< readIORef freshRuns
+        fresh <- sole "fresh exact separation module" freshModules
+        assertExactSeparationModule "fresh cached" fresh
+        bracket
+            (snd <$> (Store.openStore storePath
+                (Identity.theoryId foundation) >>= expectRight))
+            Store.closeStore
+            \store -> do
+                expectRightIO
+                    (Store.writePendingModulePrefix store
+                        (Module.sealedTypedModulePrefix fresh))
+                let validation =
+                        Declaration.WarmValidation
+                            (Declaration.validationLookup
+                                (expectRightIO
+                                    . Store.loadProofValidation store)
+                                (expectRightIO
+                                    . Store.loadDeclarationValidation store))
+                warmRuns <- newIORef (0 :: Int)
+                warmModules <-
+                    compileParsedWorkspaceWithValidation
+                        foundation
+                        bootstrap
+                        (countingAcceptedResolver executable warmRuns)
+                        validation
+                        workspace
+                assertEqual "warm separation proof skips Vampire"
+                    0
+                    =<< readIORef warmRuns
+                warm <- sole "warm exact separation module" warmModules
+                assertExactSeparationModule "warm cached" warm
+                assertEqual "warm separation semantic interface"
+                    (Module.sealedTypedModuleSemantic fresh)
+                    (Module.sealedTypedModuleSemantic warm)
+                assertEqual "warm separation final prefix"
+                    (Declaration.pendingModulePrefixCurrent
+                        (Module.sealedTypedModulePrefix fresh))
+                    (Declaration.pendingModulePrefixCurrent
+                        (Module.sealedTypedModulePrefix warm))
+                let components sealed =
+                        let batches =
+                                Declaration.pendingModulePrefixBatches
+                                    (Module.sealedTypedModulePrefix sealed)
+                        in ( concatMap
+                                Declaration.committedBatchObjects
+                                batches
+                           , concatMap
+                                (fmap Identity.checkedPropositionId
+                                    . Declaration.committedBatchPropositions)
+                                batches
+                           , concatMap
+                                Declaration.committedBatchProofValidations
+                                batches
+                           , Declaration.committedBatchDeclarationValidation
+                                <$> batches
+                           )
+                assertEqual "warm separation checked artifacts"
+                    (components fresh)
+                    (components warm)
+
 compilesExactSourceAxioms :: Assertion
 compilesExactSourceAxioms =
     Temp.withSystemTempDirectory "felix-exact-source-axiom" \root -> do
@@ -1493,18 +1591,6 @@ reusesExactProofValidationAcrossModuleMisses =
                 assertEqual "request-equivalent proof preserves public semantics"
                     (Module.sealedTypedModuleSemantic freshRoot)
                     (Module.sealedTypedModuleSemantic editedRoot)
-  where
-    countingAcceptedResolver executable runs =
-        Declaration.vampireResolver \prepared -> do
-            modifyIORef' runs (+ 1)
-            runNoLoggingT
-                (Provers.runPreparedTypedProver
-                    (Provers.vampire
-                        executable
-                        Provers.defaultTimeLimit
-                        Provers.defaultMemoryLimit)
-                    prepared)
-
 rejectsFixedSemanticDeclaration :: Assertion
 rejectsFixedSemanticDeclaration =
     Temp.withSystemTempDirectory "felix-fixed-semantic" \root -> do
@@ -2105,6 +2191,21 @@ unusedResolver =
     Declaration.vampireResolver \_prepared ->
         fail "empty bootstrap invoked Vampire"
 
+countingAcceptedResolver
+    :: FilePath
+    -> IORef Int
+    -> Declaration.VampireResolver
+countingAcceptedResolver executable runs =
+    Declaration.vampireResolver \prepared -> do
+        modifyIORef' runs (+ 1)
+        runNoLoggingT
+            (Provers.runPreparedTypedProver
+                (Provers.vampire
+                    executable
+                    Provers.defaultTimeLimit
+                    Provers.defaultMemoryLimit)
+                prepared)
+
 compileExactFixture
     :: FilePath
     -> IO