Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1159 deletions

diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs
deleted file mode 100644
index 0d0cf1b..0000000
--- a/source/Test/Unit/Provers.hs
+++ /dev/null
@@ -1,1159 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Test.Unit.Provers (unitTests) where
-
-import Base hiding (Empty)
-import Checking.Backend.Problem
-import 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 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