path: root/source/Test/Unit/Provers.hs

{-# LANGUAGE OverloadedStrings #-}

module Test.Unit.Provers (unitTests) where

import Base hiding (Empty)
import Checking.Backend.Problem
import Checking.Core
import Provers

import Control.Concurrent
    ( newEmptyMVar
    , putMVar
    , takeMVar
    , threadDelay
    )
import Control.Exception (bracket)
import Control.Exception qualified as Exception
import Control.Monad (when)
import Control.Monad.Logger (runNoLoggingT)
import Data.IORef
    ( 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 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
        , 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)
            jobsSelectionEffectiveJobs selected
                `shouldBe` positiveJobs 3
            jobsSelectionDetectedProcessors selected `shouldBe` Nothing
            jobsSelectionWasOverridden selected `shouldBe` True
            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)
                    jobsSelectionEffectiveJobs selected
                        `shouldBe` positiveJobs expected
                    jobsSelectionDetectedProcessors selected
                        `shouldBe` Just detected
                    jobsSelectionWasOverridden selected `shouldBe` False
        , testCase "falls back to one after bad detection" do
            nonPositive <- selectEffectiveJobs Nothing (pure 0)
            jobsSelectionEffectiveJobs nonPositive
                `shouldBe` positiveJobs 1
            jobsSelectionDetectedProcessors nonPositive `shouldBe` Just 1
            failed <- selectEffectiveJobs Nothing
                (Exception.throwIO (userError "processor detection failed"))
            jobsSelectionEffectiveJobs failed
                `shouldBe` positiveJobs 1
            jobsSelectionDetectedProcessors failed `shouldBe` Nothing
        ]

vampireExecutorTests :: TestTree
vampireExecutorTests =
    testGroup "bounded Vampire executor"
        [ 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)
                                (preparedTypedProverRequest prepared)
                            takeMVar firstStarted
                            second <- submitVampireRequest
                                owner
                                (workPosition 1 2)
                                (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)
                                (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 "bounds live two-worker Vampire invocations" 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 ->
                                    runNoLoggingT
                                        (runPreparedTypedProverWithExecutor
                                            owner
                                            (workPosition 1 ordinal)
                                            prepared))
                                [1..4]
                            traverse_ assertProved answers
                            observed <- vampireExecutorObservation executor
                            vampireExecutorRunCount observed `shouldBe` 4
                            vampireExecutorMaximumLiveCount observed
                                `shouldBe` 2
        , 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
                                (runNoLoggingT
                                    (runPreparedTypedProverWithExecutor
                                        owner
                                        (workPosition 1 1)
                                        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
                                (runNoLoggingT
                                    (runPreparedTypedProverWithExecutor
                                        owner
                                        (workPosition 1 1)
                                        prepared))
                                \running -> do
                                    processIds <- waitForProcessIds pidFile
                                    withAsync
                                        (runNoLoggingT
                                            (runPreparedTypedProverWithExecutor
                                                owner
                                                (workPosition 2 1)
                                                prepared))
                                        \queued -> do
                                            waitForSubmittedCount executor 2
                                            cancel queued
                                            cancel running
                                    observed <- vampireExecutorObservation
                                        executor
                                    vampireExecutorSubmittedCount observed
                                        `shouldBe` 2
                                    vampireExecutorRunCount observed
                                        `shouldBe` 1
                                    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)
                                (preparedTypedProverRequest prepared)
                            processIds <- waitForProcessIds pidFile
                            queued <- submitVampireRequest
                                owner
                                (workPosition 1 2)
                                (preparedTypedProverRequest prepared)
                            cancelVampireRequest queued
                            awaitVampireRequest queued
                                >>= assertCancelled prepared
                            afterQueued <- vampireExecutorObservation executor
                            assertBool
                                "queued terminal updates final completion"
                                (isJust
                                    (vampireExecutorFinalCompletionNanoseconds
                                        afterQueued))
                            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)
                                        (preparedTypedProverRequest prepared)
                                    processIds <- waitForProcessIds pidFile
                                    _queuedOne <- submitVampireRequest
                                        owner
                                        (workPosition 1 2)
                                        (preparedTypedProverRequest prepared)
                                    _queuedTwo <- submitVampireRequest
                                        owner
                                        (workPosition 1 3)
                                        (preparedTypedProverRequest prepared)
                                    waiter <- Async.async
                                        (awaitVampireRequest running)
                                    submitStarted <- newEmptyMVar
                                    blockedSubmit <- Async.async do
                                        putMVar submitStarted ()
                                        submitVampireRequest
                                            owner
                                            (workPosition 1 4)
                                            (preparedTypedProverRequest prepared)
                                    takeMVar submitStarted
                                    waitForSubmittedCount executor 3
                                    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)
                                (preparedTypedProverRequest prepared)
                            takeMVar observerEntered
                            _second <- submitVampireRequest
                                owner
                                (workPosition 1 2)
                                (preparedTypedProverRequest prepared)
                            _third <- submitVampireRequest
                                owner
                                (workPosition 1 3)
                                (preparedTypedProverRequest prepared)
                            withAsync
                                (submitVampireRequest
                                    owner
                                    (workPosition 1 4)
                                    (preparedTypedProverRequest prepared))
                                \blockedSubmit -> do
                                    waitForSubmittedCount executor 3
                                    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)
                        (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)
                                (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)
                                (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)

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 ->
                    runNoLoggingT
                        (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
                        runNoLoggingT
                            (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 ->
                    runNoLoggingT
                        (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 <-
                        runNoLoggingT
                            (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 <-
                        runNoLoggingT
                            (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
                        (runNoLoggingT
                            (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

waitForSubmittedCount :: VampireExecutor -> Int -> Assertion
waitForSubmittedCount executor expected = do
    guarded <- Timeout.timeout 10000000 loop
    case guarded of
        Just () ->
            pure ()
        Nothing ->
            assertFailure
                ("executor did not submit " <> show expected <> " requests")
  where
    loop = do
        observed <- vampireExecutorObservation executor
        if vampireExecutorSubmittedCount observed >= expected
            then pure ()
            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
            runNoLoggingT
                (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
            []
            []
            ExplicitGlobalPremiseSelection)
    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