{-# LANGUAGE OverloadedStrings #-} module Felix.Test.Unit.Provers (unitTests) where import Base hiding (Empty) import Felix.Checking.Backend.Problem import Felix.Checking.Core import Felix.Provers import Control.Concurrent ( newEmptyMVar , putMVar , takeMVar , threadDelay ) import Control.Exception (bracket) import Control.Exception qualified as Exception import Control.Monad (when) import Data.IORef ( atomicModifyIORef' , newIORef , readIORef , writeIORef ) import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.IO qualified as Text import Data.Vector qualified as Vector import Felix.Report.Location (Location(..)) import System.Directory qualified as Directory import System.Exit (ExitCode(..)) import System.FilePath.Posix (()) import System.Posix.Signals ( nullSignal , sigTERM , signalProcess ) import System.Posix.Types (ProcessID) import System.Timeout qualified as Timeout import Test.Tasty import Test.Tasty.HUnit import Text.Read (readMaybe) import Text.Megaparsec (parseMaybe) import UnliftIO.Async (cancel, mapConcurrently, withAsync) import UnliftIO.Async qualified as Async unitTests :: TestTree unitTests = testGroup "Provers" [ vampireStatusParserTests , vampireClassifierTests , jobsSelectionTests , slowAtpReportTests , vampireExecutorTests , vampireProcessTests ] jobsSelectionTests :: TestTree jobsSelectionTests = testGroup "effective jobs" [ testCase "uses a positive override exactly" do detectorCalled <- newIORef False selected <- selectEffectiveJobs (effectiveJobs 3) (writeIORef detectorCalled True >> pure 99) selected `shouldBe` positiveJobs 3 readIORef detectorCalled >>= (`shouldBe` False) , testCase "rounds automatic jobs to one third of detected processors" do for_ [(8, 3), (16, 5), (24, 8), (32, 11)] \(detected, expected) -> do selected <- selectEffectiveJobs Nothing (pure detected) selected `shouldBe` positiveJobs expected , testCase "falls back to one after bad detection" do nonPositive <- selectEffectiveJobs Nothing (pure 0) nonPositive `shouldBe` positiveJobs 1 failed <- selectEffectiveJobs Nothing (Exception.throwIO (userError "processor detection failed")) failed `shouldBe` positiveJobs 1 ] slowAtpReportTests :: TestTree slowAtpReportTests = testGroup "slow ATP report" [ testCase "applies the threshold and retains the twelve slowest" do prepared <- preparedTypedTask 0 let requestId = preparedVerificationRequestId (preparedTypedProverRequest prepared) task nanoseconds position = SlowAtpTask { slowAtpDuration = atpDurationFromNanoseconds nanoseconds , slowAtpOutcome = SlowAtpAccepted , slowAtpPosition = workPosition 1 position , slowAtpLocation = testLocation , slowAtpRequestId = requestId } report = slowAtpReportFromTasks ( task 4999999999 0 : [ task (5000000000 + fromIntegral position) position | position <- [0..13] ] ) slowAtpQualifyingTaskCount report `shouldBe` 14 length (slowAtpTasks report) `shouldBe` 12 slowAtpOmittedTaskCount report `shouldBe` 2 atpDurationNanoseconds (slowAtpDuration (fromMaybe (error "slow report unexpectedly empty") (listToMaybe (slowAtpTasks report)))) `shouldBe` 5000000013 , testCase "keeps earlier source positions on equal durations" do prepared <- preparedTypedTask 0 let requestId = preparedVerificationRequestId (preparedTypedProverRequest prepared) task position = SlowAtpTask { slowAtpDuration = atpDurationFromNanoseconds 5000000000 , slowAtpOutcome = SlowAtpAccepted , slowAtpPosition = workPosition 1 position , slowAtpLocation = testLocation , slowAtpRequestId = requestId } report = slowAtpReportFromTasks (task <$> [1..13]) (workPositionLocalRequestOrdinal . slowAtpPosition <$> slowAtpTasks report) `shouldBe` [1..12] ] vampireExecutorTests :: TestTree vampireExecutorTests = testGroup "bounded Vampire executor" [ testCase "records completed qualifying tasks with runtime context" do prepared <- preparedTypedTask 0 clock <- scriptedClock [10, 5000000010] let position = workPosition 2 3 withFakeVampire [ "cat >/dev/null" , "printf '%s\n' '% SZS status Theorem for fake'" ] \vampireCommand -> withVampireExecutorUsingClock clock (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do handle <- submitVampireRequest owner position testLocation (preparedTypedProverRequest prepared) awaitVampireRequest handle >>= assertAcceptedRequest prepared report <- vampireExecutorSlowAtpReport executor slowAtpQualifyingTaskCount report `shouldBe` 1 case slowAtpTasks report of [task] -> do atpDurationNanoseconds (slowAtpDuration task) `shouldBe` 5000000000 slowAtpOutcome task `shouldBe` SlowAtpAccepted slowAtpPosition task `shouldBe` position slowAtpLocation task `shouldBe` testLocation slowAtpRequestId task `shouldBe` preparedVerificationRequestId (preparedTypedProverRequest prepared) tasks -> assertFailure ("unexpected slow-task report: " <> show tasks) , testCase "does not report a cancelled partial task" do prepared <- preparedTypedTask 0 clock <- scriptedClock [0, 6000000000] withProcessGroupFake defaultTimeLimit [] \pidFile vampireCommand -> withVampireExecutorUsingClock clock (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do handle <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) processIds <- waitForProcessIds pidFile cancelVampireRequest handle report <- vampireExecutorSlowAtpReport executor slowAtpQualifyingTaskCount report `shouldBe` 0 assertBool "cancelled report is empty" (null (slowAtpTasks report)) assertProcessesGone processIds , testCase "opaque handles complete out of submission order" do prepared <- preparedTypedTask 0 firstStarted <- newEmptyMVar releaseFirst <- newEmptyMVar withFakeVampire [ "cat >/dev/null" , "printf '%s\n' '% SZS status Theorem for fake'" ] \vampireCommand -> withVampireExecutor (positiveJobs 2) vampireCommand (\position _request -> when (workPositionLocalRequestOrdinal position == 1) (putMVar firstStarted () >> takeMVar releaseFirst)) \executor -> withVampireRequestOwner executor \owner -> do first <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) takeMVar firstStarted second <- submitVampireRequest owner (workPosition 1 2) testLocation (preparedTypedProverRequest prepared) secondCompletion <- awaitVampireRequest second assertAcceptedRequest prepared secondCompletion putMVar releaseFirst () firstCompletion <- awaitVampireRequest first assertAcceptedRequest prepared firstCompletion , testCase "validates request identity before a rejection" do submitted <- preparedTypedTask 0 mismatched <- preparedTypedTask 1 withFakeVampire [ "cat >/dev/null" , "printf '%s\n' '% SZS status CounterSatisfiable for fake'" ] \vampireCommand -> withVampireExecutor (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do handle <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest submitted) outcome <- Exception.try (awaitPreparedVampireRequest (preparedTypedProverRequest mismatched) handle) case outcome of Left (failure :: VampireExecutorFault) -> assertBool "request mismatch is an integrity fault" ("wrong request id" `Text.isInfixOf` Text.pack (show failure)) Right answer -> assertFailure ("mismatched rejection was accepted: " <> show answer) , testCase "runs requests through the bounded worker pool" do prepared <- preparedTypedTask 0 withFakeVampire [ "previous=''" , "found=0" , "for argument in \"$@\"; do" , " if [ \"$previous\" = '--cores' ]; then" , " [ \"$argument\" = '2' ] || exit 17" , " found=1" , " fi" , " previous=$argument" , "done" , "[ \"$found\" = '1' ] || exit 18" , "cat >/dev/null" , "sleep 0.2" , "printf '%s\n' '% SZS status Theorem for fake'" ] \vampireCommand -> withVampireExecutor (positiveJobs 2) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do answers <- mapConcurrently (\ordinal -> runPreparedTypedProverWithExecutor owner (workPosition 1 ordinal) testLocation prepared) [1..4] traverse_ assertProved answers , testCase "propagates observer failure to the submitter" do prepared <- preparedTypedTask 0 withFakeVampire [ "cat >/dev/null" , "printf '%s\n' '% SZS status Theorem for fake'" ] \vampireCommand -> withVampireExecutor (positiveJobs 1) vampireCommand (\_position _request -> Exception.throwIO (userError "observer failed")) \executor -> withVampireRequestOwner executor \owner -> do result <- Exception.try (runPreparedTypedProverWithExecutor owner (workPosition 1 1) testLocation prepared) case result of Left (failure :: VampireExecutorFault) -> assertBool "global executor fault" ("observer failed" `Text.isInfixOf` Text.pack (show failure)) Right answer -> assertFailure ("observer failure was lost: " <> show answer) , testCase "cancels queued and running jobs independently" do prepared <- preparedTypedTask 0 withProcessGroupFake defaultTimeLimit [] \pidFile vampireCommand -> withVampireExecutor (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> withAsync (runPreparedTypedProverWithExecutor owner (workPosition 1 1) testLocation prepared) \running -> do processIds <- waitForProcessIds pidFile queuedSubmitted <- newEmptyMVar withAsync (do handle <- submitVampireRequest owner (workPosition 2 1) testLocation (preparedTypedProverRequest prepared) putMVar queuedSubmitted () awaitPreparedVampireRequest (preparedTypedProverRequest prepared) handle) \queued -> do takeMVar queuedSubmitted cancel queued cancel running assertProcessesGone processIds , testCase "explicit cancellation completes queued and running handles" do prepared <- preparedTypedTask 0 withProcessGroupFake defaultTimeLimit [] \pidFile vampireCommand -> withVampireExecutor (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do running <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) processIds <- waitForProcessIds pidFile queued <- submitVampireRequest owner (workPosition 1 2) testLocation (preparedTypedProverRequest prepared) cancelVampireRequest queued awaitVampireRequest queued >>= assertCancelled prepared cancelVampireRequest running awaitVampireRequest running >>= assertCancelled prepared assertProcessesGone processIds , testCase "structured shutdown wakes waiter and full-queue submitter" do prepared <- preparedTypedTask 0 withProcessGroupFake defaultTimeLimit [] \pidFile vampireCommand -> do (waiter, blockedSubmit, processIds) <- withVampireExecutor (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do running <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) processIds <- waitForProcessIds pidFile _queuedOne <- submitVampireRequest owner (workPosition 1 2) testLocation (preparedTypedProverRequest prepared) _queuedTwo <- submitVampireRequest owner (workPosition 1 3) testLocation (preparedTypedProverRequest prepared) waiter <- Async.async (awaitVampireRequest running) submitStarted <- newEmptyMVar blockedSubmit <- Async.async do putMVar submitStarted () submitVampireRequest owner (workPosition 1 4) testLocation (preparedTypedProverRequest prepared) takeMVar submitStarted pure (waiter, blockedSubmit, processIds) Async.waitCatch waiter >>= \case Right completion -> assertCancelled prepared completion Left failure -> assertFailure ("shutdown waiter failed: " <> show failure) Async.waitCatch blockedSubmit >>= \case Left failure -> assertBool "backpressured submit observes owner shutdown" ("VampireRequestOwnerClosed" `Text.isInfixOf` Text.pack (show failure)) Right _handle -> assertFailure "backpressured submit survived structured shutdown" assertProcessesGone processIds , testCase "worker fault wakes a waiter and a full-queue submitter" do prepared <- preparedTypedTask 0 observerEntered <- newEmptyMVar failObserver <- newEmptyMVar withFakeVampire [ "cat >/dev/null" , "printf '%s\n' '% SZS status Theorem for fake'" ] \vampireCommand -> withVampireExecutor (positiveJobs 1) vampireCommand (\position _request -> when (workPositionLocalRequestOrdinal position == 1) (putMVar observerEntered () >> takeMVar failObserver >> Exception.throwIO (userError "fatal observer fault"))) \executor -> withVampireRequestOwner executor \owner -> do first <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) takeMVar observerEntered _second <- submitVampireRequest owner (workPosition 1 2) testLocation (preparedTypedProverRequest prepared) _third <- submitVampireRequest owner (workPosition 1 3) testLocation (preparedTypedProverRequest prepared) withAsync (submitVampireRequest owner (workPosition 1 4) testLocation (preparedTypedProverRequest prepared)) \blockedSubmit -> do putMVar failObserver () awaitFault (awaitVampireRequest first) Async.waitCatch blockedSubmit >>= \case Left failure -> assertExecutorFault failure Right _handle -> assertFailure "full-queue submission survived executor fault" , testCase "declared launch failure remains request-local" do prepared <- preparedTypedTask 0 let missing = vampire "/definitely/missing/felix-vampire" defaultTimeLimit defaultMemoryLimit withVampireExecutor (positiveJobs 1) missing (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do handle <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) completion <- awaitVampireRequest handle assertCompletionRequest prepared completion case vampireCompletionTerminal completion of VampireProcessFailed ProverLaunchFailed{} -> pure () terminal -> assertFailure ("expected a local launch failure, got " <> show terminal) , testCase "protocol failure is distinct from ATP rejection" do prepared <- preparedTypedTask 0 withFakeVampire [ "cat >/dev/null" , "printf '%s\n' 'completed without an SZS status'" ] \vampireCommand -> withVampireExecutor (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do handle <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) completion <- awaitVampireRequest handle assertCompletionRequest prepared completion case vampireCompletionTerminal completion of VampireProtocolFailed{} -> pure () terminal -> assertFailure ("expected a protocol terminal, got " <> show terminal) , testCase "completed rejection diagnostics are compact" do prepared <- preparedTypedTask 0 let headMarker :: Text headMarker = "HEAD-MARKER" tailMarker :: Text tailMarker = "TAIL-MARKER" status :: Text status = "% SZS status CounterSatisfiable for fake" originalByteCount = Text.length headMarker + 1048576 + Text.length tailMarker + 1 + Text.length status + 1 withFakeVampire [ "printf '%s' 'HEAD-MARKER'" , "head -c 1048576 /dev/zero" , "printf '%s\n' 'TAIL-MARKER'" , "printf '%s\n' '% SZS status CounterSatisfiable for fake'" ] \vampireCommand -> withVampireExecutor (positiveJobs 1) vampireCommand (\_position _request -> pure ()) \executor -> withVampireRequestOwner executor \owner -> do handle <- submitVampireRequest owner (workPosition 1 1) testLocation (preparedTypedProverRequest prepared) completion <- awaitVampireRequest handle case renderVampireTerminalDiagnostic (vampireCompletionTerminal completion) of Just diagnostic -> do assertBool "retained diagnostic is bounded" (Text.length diagnostic < 70000) assertBool "truncation is reported" ("retained first and last 16 KiB" `Text.isInfixOf` diagnostic) assertBool "original byte count is reported" (("of " <> Text.pack (show originalByteCount) <> " bytes)") `Text.isInfixOf` diagnostic) assertBool "diagnostic head is retained" (headMarker `Text.isInfixOf` diagnostic) assertBool "diagnostic tail is retained" (tailMarker `Text.isInfixOf` diagnostic) Nothing -> assertFailure "expected a rejected terminal" ] positiveJobs :: Int -> EffectiveJobs positiveJobs amount = fromMaybe (error "test requested a non-positive job count") (effectiveJobs amount) scriptedClock :: [Word64] -> IO (IO Word64) scriptedClock ticks = do remaining <- newIORef ticks pure (atomicModifyIORef' remaining \case next : rest -> (rest, next) [] -> error "test monotonic clock exhausted") testLocation :: Location testLocation = Location maxBound vampireStatusParserTests :: TestTree vampireStatusParserTests = testGroup "Vampire status parser" [ testCase "parses canonical status lines" do parseMaybe vampireStatusParser "% SZS status ContradictoryAxioms for 2260" `shouldBe` Just StatusContradictoryAxioms , testCase "parses worker-prefixed status lines" do parseMaybe vampireStatusParser "% (2581105)SZS status Timeout for " `shouldBe` Just StatusTimeout , testCase "parses ResourceOut status" do parseMaybe vampireStatusParser "% SZS status ResourceOut for 2260" `shouldBe` Just StatusResourceOut , testCase "retains unsupported status values" do parseMaybe vampireStatusParser "% SZS status AlienResult for 2260" `shouldBe` Just (UnsupportedStatus "AlienResult") ] vampireClassifierTests :: TestTree vampireClassifierTests = testGroup "Vampire completed transcript classifier" [ testCase "maps each terminal status in both task modes" do classify DirectTask [StatusTheorem] `shouldBe` Right Proved classify DirectTask [StatusCounterSatisfiable] `shouldBe` Right Counterexample classify DirectTask [StatusContradictoryAxioms] `shouldBe` Right ContradictoryInput classify IndirectTask [StatusContradictoryAxioms] `shouldBe` Right Proved , testCase "maps every resource status to indeterminate" do for_ indeterminateStatuses \status -> classify DirectTask [status] `shouldBe` Right Indeterminate , testCase "lets a unique terminal outcome override resource statuses" do for_ indeterminateStatuses \status -> classify DirectTask [status, StatusTheorem] `shouldBe` Right Proved , testCase "accepts duplicate and equivalent terminal statuses" do classify DirectTask [StatusTheorem, StatusTheorem] `shouldBe` Right Proved classify IndirectTask [StatusTheorem, StatusContradictoryAxioms] `shouldBe` Right Proved , testCase "rejects every pair of different terminal outcomes" do for_ conflictingTerminalCases \(mode, statuses, outcomes) -> classify mode statuses `shouldBe` Left (ConflictingTerminalOutcomes outcomes) , testCase "is independent of status order" do for_ orderCases \(mode, statuses) -> classify mode statuses `shouldBe` classify mode (reverse statuses) , testCase "rejects unsupported status values" do classify DirectTask [StatusTheorem, UnsupportedStatus "AlienResult"] `shouldBe` Left (UnsupportedVampireStatuses (Set.singleton "AlienResult")) , testCase "rejects a successful exit without an outcome" do classify DirectTask [] `shouldBe` Left MissingVampireOutcome , testCase "rejects every status after a nonzero exit" do classifyVampireProtocol DirectTask (ExitFailure 7) [StatusTheorem] `shouldBe` Left (UnsuccessfulVampireExit (ExitFailure 7)) ] vampireProcessTests :: TestTree vampireProcessTests = testGroup "Vampire process boundary" [ testCase "classifies statuses from both completed streams" do answer <- runFakeVampire [ "printf '%s\\n' '% SZS status Timeout for fake'" , "printf '%s\\n' '% SZS status Theorem for fake' >&2" , "exit 0" ] assertProved answer , testCase "rejects a split-stream terminal conflict" do answer <- runFakeVampire [ "printf '%s\\n' '% SZS status Theorem for fake'" , "printf '%s\\n' '% SZS status CounterSatisfiable for fake' >&2" , "exit 0" ] assertProtocolError "ConflictingTerminalOutcomes" answer , testCase "rejects a theorem from a nonzero exit" do answer <- runFakeVampire [ "printf '%s\\n' '% SZS status Theorem for fake'" , "exit 7" ] assertProtocolError "ExitFailure 7" answer , testCase "rejects malformed UTF-8 output" do answer <- runFakeVampire [ "printf '\\377'" , "exit 0" ] case answer of Left (ProverOutputMalformedUtf8 _ ProverOutputStdout _) -> pure () result -> assertFailure ("expected malformed stdout, got " <> show result) , testCase "returns a broken stdin pipe" do prepared <- preparedTypedTask 20000 result <- withFakeVampire [ "exec 0<&-" , "sleep 1" ] \vampireCommand -> runPreparedTypedProver vampireCommand prepared case result of Left (ProverCommunicationFailed _ ProverStdin _) -> pure () processResult -> assertFailure ("expected a communication failure, got " <> show processResult) , testCase "drains output while feeding prover input" do prepared <- preparedTypedTask 20000 guardedAnswer <- Timeout.timeout 30000000 (withFakeVampire [ "head -c 1048576 /dev/zero &" , "head -c 1048576 /dev/zero >&2 &" , "wait" , "printf '\\n'" , "printf '\\n' >&2" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for fake'" , "exit 0" ] \vampireCommand -> do runPreparedTypedProver vampireCommand prepared) case guardedAnswer of Nothing -> assertFailure "prover communication did not finish" Just answer -> assertProved answer , testCase "reports signal termination separately" do prepared <- preparedTypedTask 0 result <- withFakeVampire [ "kill -TERM $$" ] \vampireCommand -> runPreparedTypedProver vampireCommand prepared case result of Left (ProverTerminatedBySignal _ signalNumber _) -> assertEqual "termination signal" (fromIntegral sigTERM) signalNumber processResult -> assertFailure ("expected signal termination, got " <> show processResult) , testCase "deadline terminates and reaps the process group" do prepared <- preparedTypedTask 0 withProcessGroupFake (Seconds 0) [] \pidFile vampireCommand -> do result <- runPreparedTypedProver vampireCommand prepared assertTimedOut result processIds <- readProcessIds pidFile assertProcessesGone processIds , testCase "output exhaustion terminates the process group" do prepared <- preparedTypedTask 0 withProcessGroupFake defaultTimeLimit [ "head -c 33554432 /dev/zero" ] \pidFile vampireCommand -> do result <- runPreparedTypedProver vampireCommand prepared case result of Left (ProverOutputLimitExceeded _ ProverOutputStdout _) -> pure () processResult -> assertFailure ("expected stdout limit exhaustion, got " <> show processResult) processIds <- readProcessIds pidFile assertProcessesGone processIds , testCase "cancellation terminates and reaps the process group" do prepared <- preparedTypedTask 0 withProcessGroupFake defaultTimeLimit [] \pidFile vampireCommand -> withAsync (runPreparedTypedProver vampireCommand prepared) \worker -> do processIds <- waitForProcessIds pidFile cancel worker assertProcessesGone processIds ] classify :: VampireTaskMode -> [VampireStatus] -> Either VampireProtocolError CanonicalAtpOutcome classify mode = classifyVampireProtocol mode ExitSuccess indeterminateStatuses :: [VampireStatus] indeterminateStatuses = [ StatusTimeout , StatusResourceOut , StatusGaveUp , StatusUnknown ] conflictingTerminalCases :: [(VampireTaskMode, [VampireStatus], Set CanonicalAtpOutcome)] conflictingTerminalCases = [ ( DirectTask , [StatusTheorem, StatusCounterSatisfiable] , Set.fromList [Proved, Counterexample] ) , ( DirectTask , [StatusTheorem, StatusContradictoryAxioms] , Set.fromList [Proved, ContradictoryInput] ) , ( DirectTask , [StatusCounterSatisfiable, StatusContradictoryAxioms] , Set.fromList [Counterexample, ContradictoryInput] ) , ( IndirectTask , [StatusTheorem, StatusCounterSatisfiable] , Set.fromList [Proved, Counterexample] ) , ( IndirectTask , [StatusCounterSatisfiable, StatusContradictoryAxioms] , Set.fromList [Proved, Counterexample] ) ] orderCases :: [(VampireTaskMode, [VampireStatus])] orderCases = [ (DirectTask, StatusTheorem : indeterminateStatuses) , (DirectTask, [StatusTheorem, StatusCounterSatisfiable]) , (IndirectTask, [StatusTheorem, StatusContradictoryAxioms]) , (DirectTask, [UnsupportedStatus "B", UnsupportedStatus "A"]) ] assertProved :: Either ProverProcessError ProverAnswer -> Assertion assertProved = \case Right Yes -> pure () answer -> assertFailure ("expected a proof, got " <> show answer) assertAcceptedRequest :: PreparedTypedProverTask ref local origin global -> VampireCompletion -> Assertion assertAcceptedRequest prepared completion = do assertCompletionRequest prepared completion case vampireCompletionTerminal completion of VampireAccepted -> pure () terminal -> assertFailure ("expected an accepted terminal, got " <> show terminal) assertCompletionRequest :: PreparedTypedProverTask ref local origin global -> VampireCompletion -> Assertion assertCompletionRequest prepared completion = vampireCompletionRequestId completion `shouldBe` preparedVerificationRequestId (preparedTypedProverRequest prepared) assertCancelled :: PreparedTypedProverTask ref local origin global -> VampireCompletion -> Assertion assertCancelled prepared completion = do assertCompletionRequest prepared completion vampireCompletionTerminal completion `shouldBe` VampireCancelled awaitFault :: IO value -> Assertion awaitFault action = do result <- Exception.try action case result of Left failure -> assertExecutorFault failure Right _value -> assertFailure "expected a global executor fault" assertExecutorFault :: Exception.SomeException -> Assertion assertExecutorFault failure = case Exception.fromException failure :: Maybe VampireExecutorFault of Just _fault -> pure () Nothing -> assertFailure ("expected VampireExecutorFault, got " <> show failure) assertProtocolError :: Text -> Either ProverProcessError ProverAnswer -> Assertion assertProtocolError expected = \case Right (Error _label diagnostic) -> assertBool ( "expected protocol error containing " <> show expected <> ", got " <> show diagnostic ) (expected `Text.isInfixOf` diagnostic) answer -> assertFailure ("expected a protocol error, got " <> show answer) assertTimedOut :: Either ProverProcessError a -> Assertion assertTimedOut = \case Left ProverTimedOut{} -> pure () result -> assertFailure ("expected prover timeout, got " <> showResult result) where showResult = \case Left err -> show err Right _ -> "successful process result" withProcessGroupFake :: TimeLimit -> [String] -> (FilePath -> Vampire -> IO a) -> IO a withProcessGroupFake timeLimit body action = withFakeVampireIn (\temp -> let pidFile = temp "process-ids" in [ "trap '' TERM" , "sleep 60 &" , "printf '%s %s\\n' \"$$\" \"$!\" > " <> pidFile ] <> body <> ["wait"]) timeLimit \temp -> action (temp "process-ids") readProcessIds :: FilePath -> IO [ProcessID] readProcessIds path = do contents <- Text.readFile path case traverse (readMaybe . Text.unpack) (Text.words contents) of Just processIds@[_leader, _descendant] -> pure processIds _ -> assertFailure ("expected leader and descendant process ids, got " <> show contents) waitForProcessIds :: FilePath -> IO [ProcessID] waitForProcessIds path = do guarded <- Timeout.timeout 10000000 loop case guarded of Just processIds -> pure processIds Nothing -> assertFailure "fake prover did not publish its process ids" where loop = do exists <- Directory.doesFileExist path if exists then readProcessIds path else do threadDelay 10000 loop assertProcessesGone :: [ProcessID] -> Assertion assertProcessesGone processIds = do guarded <- Timeout.timeout 10000000 loop case guarded of Just () -> pure () Nothing -> assertFailure ("supervisor left processes running: " <> show processIds) where loop = do alive <- traverse processIsAlive processIds if or alive then do threadDelay 10000 loop else pure () processIsAlive :: ProcessID -> IO Bool processIsAlive processId = (signalProcess nullSignal processId >> pure True) `Exception.catch` \(err :: Exception.IOException) -> if isDoesNotExistError err then pure False else throwIO err runFakeVampire :: [String] -> IO (Either ProverProcessError ProverAnswer) runFakeVampire scriptLines = withFakeVampire (["cat >/dev/null"] <> scriptLines) \vampireCommand -> do prepared <- preparedTypedTask 0 runPreparedTypedProver vampireCommand prepared withFakeVampire :: [String] -> (Vampire -> IO a) -> IO a withFakeVampire scriptLines action = withFakeVampireIn (const scriptLines) defaultTimeLimit (const action) withFakeVampireIn :: (FilePath -> [String]) -> TimeLimit -> (FilePath -> Vampire -> IO a) -> IO a withFakeVampireIn makeScript timeLimit action = withTemporaryDirectory "felix-fake-vampire" \temp -> do let executablePath = temp "vampire" writeFile executablePath (unlines ( [ "#!/bin/sh" ] <> makeScript temp )) permissions <- Directory.getPermissions executablePath Directory.setPermissions executablePath (Directory.setOwnerExecutable True permissions) action temp (vampire executablePath timeLimit defaultMemoryLimit) withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a withTemporaryDirectory template = bracket create Directory.removePathForcibly where create = do systemTemp <- Directory.getTemporaryDirectory (path, handle) <- openTempFile systemTemp template hClose handle Directory.removeFile path Directory.createDirectory path pure path shouldBe :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion shouldBe = flip (assertEqual "") preparedTypedTask :: Int -> IO (PreparedTypedProverTask Int Void Void Void) preparedTypedTask factCount = do checked <- expectRight (checkScopedCanonicalCore (const Nothing) [] propositionTerm) proposition <- expectRight (supportedProposition Vector.empty checked) capability <- expectRight (classifySupportedProposition (const Nothing) proposition) let facts = Vector.generate factCount (\reference -> typedBackendFact reference proposition capability) problem <- expectRight (planTypedProblem (const Nothing) facts proposition [] [] FirstOrderLocals ExplicitHigherOrderJustification) expectRight (prepareTypedProverTask DirectTask problem) where propositionTerm = CEq TySet (CIntrinsic Empty) (CIntrinsic Empty) expectRight :: Show error => Either error value -> IO value expectRight = \case Left failure -> assertFailure (show failure) >> fail "unreachable" Right value -> pure value