path: root/source/Provers.hs

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}

module Provers
    ( Vampire
    , vampire
    , VampireTaskMode(..)
    , VampireStatus(..)
    , CanonicalAtpOutcome(..)
    , CanonicalAtpRejection(..)
    , VampireProtocolError(..)
    , classifyVampireProtocol
    , vampireStatusParser
    , TimeLimit(..)
    , MemoryLimit(..)
    , defaultTimeLimit
    , defaultMemoryLimit
    , ProverAnswer
        ( CounterSatisfiable
        , ContradictoryAxioms
        , Uncertain
        , Error
        )
    , pattern Yes
    , ProverStream(..)
    , ProverOutputStream(..)
    , ProverProcessError(..)
    , VerificationDialect(..)
    , PreparedVerificationRequest
    , preparedVerificationDialect
    , preparedVerificationText
    , preparedVerificationBytes
    , preparedVerificationByteCount
    , preparedVerificationRequestId
    , PreparedTypedProverTask
    , prepareTypedProverTask
    , preparedTypedProverLogicalProblem
    , preparedTypedProverRequest
    , AcceptedVampireRun
    , acceptedVampireRequestId
    , provedVampireRun
    , runPreparedTypedProver
    , runPreparedTypedProverWithObserver
    , EffectiveJobs
    , effectiveJobs
    , effectiveJobsValue
    , JobsSelection(..)
    , selectEffectiveJobs
    , WorkPosition
    , workPosition
    , workPositionModuleOrdinal
    , workPositionLocalRequestOrdinal
    , VampireExecutor
    , VampireExecutorFault
    , VampireExecutorObservation(..)
    , VampireRequestOwner
    , VampireHandle
    , VampireTerminal(..)
    , renderVampireTerminalDiagnostic
    , VampireCompletion
    , vampireCompletionRequestId
    , vampireCompletionTerminal
    , withVampireExecutor
    , withVampireRequestOwner
    , submitVampireRequest
    , awaitVampireRequest
    , awaitPreparedVampireRequest
    , cancelVampireRequest
    , runPreparedTypedProverWithExecutor
    , vampireExecutorObservation
    ) where

import Base
import Checking.Authority qualified as Authority
import Checking.Backend.Problem
import Checking.Backend.Tptp

import Control.Concurrent.STM
    ( STM
    , TBQueue
    , TMVar
    , TVar
    , atomically
    , check
    , modifyTVar'
    , newEmptyTMVarIO
    , newTBQueueIO
    , newTVarIO
    , orElse
    , readTMVar
    , readTBQueue
    , readTVar
    , readTVarIO
    , throwSTM
    , tryPutTMVar
    , tryReadTMVar
    , writeTBQueue
    , writeTVar
    )
import Control.Exception
    ( AsyncException
    , IOException
    , SomeException
    , displayException
    , fromException
    )
import Control.Exception qualified as Exception
import Control.Monad (replicateM, unless, when)
import Control.Monad.Logger
import Data.ByteString qualified as ByteString
import Data.IntMap.Strict qualified as IntMap
import Data.IORef
    ( IORef
    , atomicModifyIORef'
    , newIORef
    , readIORef
    , writeIORef
    )
import Data.Set qualified as Set
import Data.Text qualified as Text
import Data.Text.Encoding qualified as TextEncoding
import Data.Text.Encoding.Error qualified as TextEncodingError
import Data.Time
import Numeric.Natural (Natural)
import System.Exit (ExitCode(..))
import System.Posix.Signals (sigKILL, signalProcessGroup)
import System.Posix.Types (ProcessGroupID)
import System.Process
    ( CreateProcess(..)
    , ProcessHandle
    , StdStream(CreatePipe)
    , getPid
    , proc
    , waitForProcess
    , withCreateProcess
    )
import System.Timeout qualified as Timeout
import Text.Megaparsec
import Text.Megaparsec.Char qualified as Char
import TextBuilder
import UnliftIO.Async
    ( async
    , cancel
    , concurrently
    , waitCatch
    , waitCatchSTM
    )

data Vampire = Vampire
    { vampireExecutable :: FilePath
    , vampireTimeLimit :: TimeLimit
    , vampireMemoryLimit :: MemoryLimit
    }
    deriving (Show, Eq)

newtype TimeLimit = Seconds Word64 deriving (Show, Eq, Num)
newtype MemoryLimit = Megabytes Word64 deriving (Show, Eq)

defaultTimeLimit :: TimeLimit
defaultTimeLimit = Seconds 10

defaultMemoryLimit :: MemoryLimit
defaultMemoryLimit = Megabytes 5000

vampire :: FilePath -> TimeLimit -> MemoryLimit -> Vampire
vampire = Vampire

vampireArguments :: Vampire -> [String]
vampireArguments Vampire{..} =
    [ "--input_syntax", "tptp"
    , "--mode", "casc"
    , "--time_limit", toSeconds vampireTimeLimit
    , "--memory_limit", toMegabytes vampireMemoryLimit
    , "--cores", "2"
    ]

-- | A strictly positive invocation-local bound for module pipelines and
-- top-level Vampire invocations.
newtype EffectiveJobs = EffectiveJobs Int
    deriving (Show, Eq, Ord)

effectiveJobs :: Int -> Maybe EffectiveJobs
effectiveJobs amount
    | amount > 0 = Just (EffectiveJobs amount)
    | otherwise = Nothing

effectiveJobsValue :: EffectiveJobs -> Int
effectiveJobsValue (EffectiveJobs amount) = amount

-- | The effective worker policy selected for one invocation.  Processor
-- discovery is operational evidence only and enters no durable identity.
data JobsSelection = JobsSelection
    { jobsSelectionDetectedProcessors :: !(Maybe Int)
    , jobsSelectionEffectiveJobs :: !EffectiveJobs
    , jobsSelectionWasOverridden :: !Bool
    }
    deriving (Show, Eq)

-- | Select the worker bound, with processor discovery injected for focused
-- testing.  Asynchronous cancellation is never mistaken for failed discovery.
selectEffectiveJobs
    :: Maybe EffectiveJobs
    -> IO Int
    -> IO JobsSelection
selectEffectiveJobs override detectProcessors =
    case override of
        Just selected ->
            pure
                JobsSelection
                    { jobsSelectionDetectedProcessors = Nothing
                    , jobsSelectionEffectiveJobs = selected
                    , jobsSelectionWasOverridden = True
                    }
        Nothing -> do
            detectedResult <- Exception.try detectProcessors
            case detectedResult of
                Left detectionFailure
                    | Just asynchronous <-
                        (fromException detectionFailure
                            :: Maybe AsyncException) ->
                            Exception.throwIO asynchronous
                    | otherwise ->
                        fallback
                Right detectedRaw ->
                    let detected = max 1 detectedRaw
                        -- Two portfolio workers plus one module pipeline
                        -- nominally consume about three logical CPUs.
                        automaticJobs = max 1 ((detected + 1) `div` 3)
                     in pure
                            JobsSelection
                                { jobsSelectionDetectedProcessors =
                                    Just detected
                                , jobsSelectionEffectiveJobs =
                                    EffectiveJobs automaticJobs
                                , jobsSelectionWasOverridden = False
                                }
  where
    fallback =
        pure
            JobsSelection
                { jobsSelectionDetectedProcessors = Nothing
                , jobsSelectionEffectiveJobs = EffectiveJobs 1
                , jobsSelectionWasOverridden = False
                }

-- | Stable runtime diagnostic position.  It is deliberately separate from
-- request, validation, cache, and mathematical identities.
data WorkPosition = WorkPosition !Natural !Natural
    deriving (Show, Eq, Ord)

workPosition :: Natural -> Natural -> WorkPosition
workPosition = WorkPosition

workPositionModuleOrdinal :: WorkPosition -> Natural
workPositionModuleOrdinal (WorkPosition moduleOrdinal _localOrdinal) =
    moduleOrdinal

workPositionLocalRequestOrdinal :: WorkPosition -> Natural
workPositionLocalRequestOrdinal (WorkPosition _moduleOrdinal localOrdinal) =
    localOrdinal

toSeconds :: TimeLimit -> String
toSeconds (Seconds secs) = show secs

toMegabytes :: MemoryLimit -> String
toMegabytes (Megabytes mbs) = show mbs

data VampireTaskMode
    = DirectTask
    | IndirectTask
    deriving (Show, Eq)

data VampireStatus
    = StatusTheorem
    | StatusCounterSatisfiable
    | StatusContradictoryAxioms
    | StatusTimeout
    | StatusResourceOut
    | StatusGaveUp
    | StatusUnknown
    | UnsupportedStatus Text
    deriving (Show, Eq)

data CanonicalAtpOutcome
    = Proved
    | Counterexample
    | ContradictoryInput
    | Indeterminate
    deriving (Show, Eq, Ord)

-- | The closed non-accepting subset of canonical ATP outcomes.  Protocol
-- disagreement is represented separately from a semantic non-proof, while an
-- accepting result is unrepresentable here.
data CanonicalAtpRejection
    = RejectedCounterexample
    | RejectedContradictoryInput
    | RejectedIndeterminate
    deriving (Show, Eq)

data VampireProtocolError
    = UnsuccessfulVampireExit ExitCode
    | UnsupportedVampireStatuses (Set Text)
    | MalformedVampireStatusLines (Set Text)
    | MissingVampireOutcome
    | ConflictingTerminalOutcomes (Set CanonicalAtpOutcome)
    deriving (Show, Eq)

data CompleteCapturedStreams = CompleteCapturedStreams
    { completedStdout :: !Text
    , completedStderr :: !Text
    }
    deriving (Show, Eq)

data CompletedTranscript = CompletedTranscript
    { completedExitCode :: !ExitCode
    , completedStreams :: !CompleteCapturedStreams
    }
    deriving (Show, Eq)

data PartialCapturedStreams = PartialCapturedStreams
    { partialStdout :: !ByteString.ByteString
    , partialStderr :: !ByteString.ByteString
    }
    deriving (Eq)

instance Show PartialCapturedStreams where
    showsPrec precedence PartialCapturedStreams{..} =
        showParen (precedence > applicationPrecedence)
            ( showString "PartialCapturedStreams "
                . shows
                    ( ByteString.length partialStdout
                    , ByteString.length partialStderr
                    )
            )

data BoundedBytes = BoundedBytes
    { boundedBytesOriginalCount :: !Int
    , boundedBytesRetained :: !ByteString.ByteString
    , boundedBytesTruncated :: !Bool
    }
    deriving (Eq)

instance Show BoundedBytes where
    showsPrec precedence BoundedBytes{..} =
        showParen (precedence > applicationPrecedence)
            ( showString "BoundedBytes "
                . shows
                    ( boundedBytesOriginalCount
                    , ByteString.length boundedBytesRetained
                    , boundedBytesTruncated
                    )
            )

data BoundedCapturedStreams = BoundedCapturedStreams
    { boundedStdout :: !BoundedBytes
    , boundedStderr :: !BoundedBytes
    }
    deriving (Show, Eq)

data BoundedDiagnostic = BoundedDiagnostic
    { boundedDiagnosticSummary :: !Text
    , boundedDiagnosticStdout :: !BoundedBytes
    , boundedDiagnosticStderr :: !BoundedBytes
    }
    deriving (Show, Eq)

-- | Classify parsed Vampire statuses without depending on stream or line order.
classifyVampireProtocol
    :: VampireTaskMode
    -> ExitCode
    -> [VampireStatus]
    -> Either VampireProtocolError CanonicalAtpOutcome
classifyVampireProtocol mode exitCode statuses =
    case exitCode of
        ExitFailure _ ->
            Left (UnsuccessfulVampireExit exitCode)
        ExitSuccess
            | not (Set.null unsupported) ->
                Left (UnsupportedVampireStatuses unsupported)
            | otherwise ->
                classifyOutcomes
                    (Set.fromList
                        [ outcome
                        | status <- statuses
                        , Just outcome <- [vampireStatusOutcome mode status]
                        ])
  where
    unsupported =
        Set.fromList
            [ status
            | UnsupportedStatus status <- statuses
            ]

classifyOutcomes
    :: Set CanonicalAtpOutcome
    -> Either VampireProtocolError CanonicalAtpOutcome
classifyOutcomes outcomes =
    case Set.toList terminalOutcomes of
        [] ->
            if Indeterminate `Set.member` outcomes
                then Right Indeterminate
                else Left MissingVampireOutcome
        [outcome] ->
            Right outcome
        _ ->
            Left (ConflictingTerminalOutcomes terminalOutcomes)
  where
    terminalOutcomes = Set.delete Indeterminate outcomes

vampireStatusOutcome
    :: VampireTaskMode
    -> VampireStatus
    -> Maybe CanonicalAtpOutcome
vampireStatusOutcome mode = \case
    StatusTheorem ->
        Just Proved
    StatusCounterSatisfiable ->
        Just Counterexample
    StatusContradictoryAxioms ->
        Just case mode of
            DirectTask -> ContradictoryInput
            IndirectTask -> Proved
    StatusTimeout ->
        Just Indeterminate
    StatusResourceOut ->
        Just Indeterminate
    StatusGaveUp ->
        Just Indeterminate
    StatusUnknown ->
        Just Indeterminate
    UnsupportedStatus{} ->
        Nothing

data VerificationDialect
    = VerificationFof
    | VerificationTh0
    deriving (Show, Eq)

data PreparedVerificationRequest = PreparedVerificationRequest
    { preparedVerificationDialect :: !VerificationDialect
    , preparedVerificationMode :: !VampireTaskMode
    , preparedVerificationInput :: !ByteString.ByteString
    , preparedVerificationIdentity :: !Authority.PreparedRequestId
    }
    deriving (Eq)

-- | Decode the one canonical serialized request only at a textual boundary.
-- Prepared requests deliberately do not retain an equivalent 'Text' copy.
preparedVerificationText :: PreparedVerificationRequest -> Text
preparedVerificationText request =
    let encoded = preparedVerificationInput request
        withoutFinalNewline =
            case ByteString.unsnoc encoded of
                Just (body, 10) -> body
                _ -> encoded
    in TextEncoding.decodeUtf8 withoutFinalNewline

preparedVerificationByteCount
    :: PreparedVerificationRequest
    -> Int
preparedVerificationByteCount =
    ByteString.length . preparedVerificationInput

preparedVerificationBytes
    :: PreparedVerificationRequest
    -> ByteString.ByteString
preparedVerificationBytes =
    preparedVerificationInput

preparedVerificationRequestId
    :: PreparedVerificationRequest
    -> Authority.PreparedRequestId
preparedVerificationRequestId =
    preparedVerificationIdentity

data PreparedTypedProverTask ref local origin global =
    PreparedTypedProverTask
        !(TypedProblem ref local origin global)
        !PreparedVerificationRequest
        !Text

prepareTypedProverTask
    :: (Ord local, Ord global)
    => VampireTaskMode
    -> TypedProblem ref local origin global
    -> Either
        (TypedTptpPreparationError local global)
        (PreparedTypedProverTask ref local origin global)
prepareTypedProverTask mode problem = do
    prepared <-
        prepareTypedTptpProblem problem
    let dialect =
            case preparedTypedTptpRoute prepared of
                RouteFof -> VerificationFof
                RouteTh0 -> VerificationTh0
        bytes =
            TextEncoding.encodeUtf8
                (preparedTypedTptpTextNewline prepared)
        identity =
            Authority.preparedRequestId
                (case dialect of
                    VerificationFof -> Authority.PreparedRequestFof
                    VerificationTh0 -> Authority.PreparedRequestTh0)
                (case mode of
                    DirectTask -> Authority.PreparedRequestDirect
                    IndirectTask -> Authority.PreparedRequestIndirect)
                bytes
        preparedRequest =
            PreparedVerificationRequest
                { preparedVerificationDialect = dialect
                , preparedVerificationMode = mode
                , preparedVerificationInput = bytes
                , preparedVerificationIdentity = identity
                }
    pure
        (PreparedTypedProverTask
            problem
            preparedRequest
            (preparedTypedTptpConjectureText prepared))

preparedTypedProverLogicalProblem
    :: PreparedTypedProverTask ref local origin global
    -> TypedProblem ref local origin global
preparedTypedProverLogicalProblem
        (PreparedTypedProverTask
            problem
            _request
            _conjecture) =
    problem

preparedTypedProverRequest
    :: PreparedTypedProverTask ref local origin global
    -> PreparedVerificationRequest
preparedTypedProverRequest
        (PreparedTypedProverTask
            _problem
            request
            _conjecture) =
    request

data AcceptedVampireRun = AcceptedVampireRun
    { acceptedVampireRequestId :: !Authority.PreparedRequestId }
    deriving (Eq)

data ProverAnswer
    = ProvedAnswer AcceptedVampireRun
    | CounterSatisfiable Text
    | ContradictoryAxioms Text
    | Uncertain Text
    | Error Text Text
    deriving (Eq)

pattern Yes :: ProverAnswer
pattern Yes <- ProvedAnswer _

{-# COMPLETE Yes, CounterSatisfiable, ContradictoryAxioms, Uncertain, Error #-}

instance Show ProverAnswer where
    showsPrec _ (ProvedAnswer _) =
        showString "Yes"
    showsPrec precedence (CounterSatisfiable task) =
        showParen (precedence > applicationPrecedence)
            (showString "CounterSatisfiable "
                . showsPrec (applicationPrecedence + 1) task)
    showsPrec precedence (ContradictoryAxioms task) =
        showParen (precedence > applicationPrecedence)
            (showString "ContradictoryAxioms "
                . showsPrec (applicationPrecedence + 1) task)
    showsPrec precedence (Uncertain task) =
        showParen (precedence > applicationPrecedence)
            (showString "Uncertain "
                . showsPrec (applicationPrecedence + 1) task)
    showsPrec precedence (Error errorLabel message) =
        showParen (precedence > applicationPrecedence)
            (showString "Error "
                . showsPrec (applicationPrecedence + 1) errorLabel
                . showChar ' '
                . showsPrec (applicationPrecedence + 1) message)

provedVampireRun :: ProverAnswer -> Maybe AcceptedVampireRun
provedVampireRun = \case
    ProvedAnswer accepted ->
        Just accepted
    CounterSatisfiable{} ->
        Nothing
    ContradictoryAxioms{} ->
        Nothing
    Uncertain{} ->
        Nothing
    Error{} ->
        Nothing

applicationPrecedence :: Int
applicationPrecedence = 10

data ProverStream
    = ProverStdin
    | ProverStdout
    | ProverStderr
    deriving (Show, Eq)

data ProverOutputStream
    = ProverOutputStdout
    | ProverOutputStderr
    deriving (Show, Eq)

data ProverProcessError
    = ProverLaunchFailed !FilePath !Text
    | ProverCommunicationFailed !FilePath !ProverStream !Text
    | ProverOutputMalformedUtf8 !FilePath !ProverOutputStream !Text
    | ProverTimedOut
        !FilePath
        !TimeLimit
        !BoundedCapturedStreams
    | ProverOutputLimitExceeded
        !FilePath
        !ProverOutputStream
        !BoundedCapturedStreams
    | ProverTerminatedBySignal
        !FilePath
        !Int
        !BoundedCapturedStreams
    | ProverLifecycleFailed !FilePath !Text
    deriving (Show, Eq)

data SupervisorAbort
    = SupervisorCommunicationFailed !ProverStream !Text
    | SupervisorOutputLimitExceeded !ProverOutputStream
    | SupervisorLifecycleFailed !Text
    deriving (Show)

instance Exception.Exception SupervisorAbort

data CaptureBuffer = CaptureBuffer
    { captureByteCount :: !Int
    , captureChunksReversed :: ![ByteString.ByteString]
    }

vampireOutputByteLimit :: Int
vampireOutputByteLimit =
    16 * 1024 * 1024

vampireWallGraceSeconds :: Integer
vampireWallGraceSeconds =
    2

captureChunkSize :: Int
captureChunkSize =
    32 * 1024

runPreparedTypedProver
    :: (MonadIO io, MonadLogger io)
    => Vampire
    -> PreparedTypedProverTask ref local origin global
    -> io (Either ProverProcessError ProverAnswer)
runPreparedTypedProver
        vampireCommand =
    runPreparedTypedProverWithObserver
        (\_request -> pure ())
        vampireCommand

runPreparedTypedProverWithObserver
    :: (MonadIO io, MonadLogger io)
    => (PreparedVerificationRequest -> IO ())
    -> Vampire
    -> PreparedTypedProverTask ref local origin global
    -> io (Either ProverProcessError ProverAnswer)
runPreparedTypedProverWithObserver
        observer
        vampireCommand
        (PreparedTypedProverTask
            _problem
            preparedRequest
            conjecture) = do
    startTime <- liftIO getCurrentTime
    terminal <- liftIO
        (runPreparedVerificationTerminal
            observer
            vampireCommand
            preparedRequest)
    answer <- liftIO
        (completionProverResult
            preparedRequest
            (VampireCompletion
                (preparedVerificationRequestId preparedRequest)
                terminal))
    endTime <- liftIO getCurrentTime
    let duration =
            timeDifferenceToText
                startTime
                endTime
        dialect =
            case preparedVerificationDialect preparedRequest of
                VerificationFof ->
                    "FOF"
                VerificationTh0 ->
                    "TH0"
    logInfoN
        (duration
            <> " "
            <> conjecture
            <> " [typed "
            <> dialect
            <> "]")
    pure answer

-- | Invocation-local bounded owner of Vampire subprocesses.  The finite queue
-- carries only immutable prepared bytes plus runtime diagnostic position;
-- checker builders and typed tasks never cross this boundary.
data VampireExecutor = VampireExecutor
    { executorQueue :: !(TBQueue ExecutorJob)
    , executorState :: !(TVar VampireExecutorState)
    , executorNextHandle :: !(TVar Int)
    , executorCommand :: !Vampire
    , executorRequestObserver
        :: !(WorkPosition -> PreparedVerificationRequest -> IO ())
    , executorRuntime :: !(TVar VampireExecutorRuntime)
    }

data ExecutorJob = ExecutorJob
    { executorJobPosition :: !WorkPosition
    , executorJobRequest :: !PreparedVerificationRequest
    , executorJobCancelled :: !(TVar Bool)
    , executorJobStarted :: !(TVar Bool)
    , executorJobCompletion
        :: !(TMVar VampireCompletion)
    }

data VampireExecutorState
    = ExecutorRunning
    | ExecutorClosing
    | ExecutorFaulted !VampireExecutorFault

-- | A global executor fault is distinct from one request's declared process
-- or protocol outcome.  Its bounded message carries no process transcript.
newtype VampireExecutorFault = VampireExecutorFault Text
    deriving (Show)

instance Exception.Exception VampireExecutorFault

data VampireRequestOwner = VampireRequestOwner
    { requestOwnerExecutor :: !VampireExecutor
    , requestOwnerState :: !(TVar VampireRequestOwnerState)
    }

data VampireRequestOwnerState
    = RequestOwnerOpen !(IntMap VampireHandle)
    | RequestOwnerClosed

-- | An opaque, owner-scoped completion handle.  It deliberately retains no
-- prepared request, command, transcript, builder, or parser state.
data VampireHandle = VampireHandle
    { vampireHandleOrdinal :: !Int
    , vampireHandleOwner :: !VampireRequestOwner
    , vampireHandleRequestId :: !Authority.PreparedRequestId
    , vampireHandleCancelled :: !(TVar Bool)
    , vampireHandleStarted :: !(TVar Bool)
    , vampireHandleCompletion :: !(TMVar VampireCompletion)
    }

data VampireTerminal
    = VampireAccepted
    | VampireRejected !CanonicalAtpRejection !BoundedDiagnostic
    | VampireProtocolFailed !BoundedDiagnostic
    | VampireProcessFailed !ProverProcessError
    | VampireCancelled
    deriving (Show, Eq)

data VampireCompletion = VampireCompletion
    { vampireCompletionRequestId :: !Authority.PreparedRequestId
    , vampireCompletionTerminal :: !VampireTerminal
    }
    deriving (Show, Eq)

renderVampireTerminalDiagnostic :: VampireTerminal -> Maybe Text
renderVampireTerminalDiagnostic = \case
    VampireAccepted -> Nothing
    VampireRejected _rejection diagnostic ->
        Just (renderBoundedDiagnostic diagnostic)
    VampireProtocolFailed diagnostic ->
        Just (renderBoundedDiagnostic diagnostic)
    VampireProcessFailed processFailure ->
        Just (Text.pack (show processFailure))
    VampireCancelled -> Nothing

data VampireExecutorRuntime = VampireExecutorRuntime
    { runtimeSubmittedCount :: !Int
    , runtimeRunCount :: !Int
    , runtimeLiveCount :: !Int
    , runtimeMaximumLiveCount :: !Int
    , runtimeFirstStartNanoseconds :: !(Maybe Word64)
    , runtimeFinalSubmissionNanoseconds :: !(Maybe Word64)
    , runtimeFinalCompletionNanoseconds :: !(Maybe Word64)
    , runtimeExecutionNanoseconds :: !Word64
    , runtimeLongestExecutionNanoseconds :: !Word64
    }

data VampireExecutorObservation = VampireExecutorObservation
    { vampireExecutorSubmittedCount :: !Int
    , vampireExecutorRunCount :: !Int
    , vampireExecutorMaximumLiveCount :: !Int
    , vampireExecutorFirstStartNanoseconds :: !(Maybe Word64)
    , vampireExecutorFinalSubmissionNanoseconds :: !(Maybe Word64)
    , vampireExecutorFinalCompletionNanoseconds :: !(Maybe Word64)
    , vampireExecutorExecutionNanoseconds :: !Word64
    , vampireExecutorLongestExecutionNanoseconds :: !Word64
    }
    deriving (Show, Eq)

data VampireExecutorClosed = VampireExecutorClosed
    deriving (Show)

instance Exception.Exception VampireExecutorClosed

data VampireRequestOwnerClosed = VampireRequestOwnerClosed
    deriving (Show)

instance Exception.Exception VampireRequestOwnerClosed

data RequestObserverFailure = RequestObserverFailure SomeException

instance Show RequestObserverFailure where
    show (RequestObserverFailure observerError) =
        "request observer failed: " <> displayException observerError

instance Exception.Exception RequestObserverFailure

initialVampireExecutorRuntime :: VampireExecutorRuntime
initialVampireExecutorRuntime =
    VampireExecutorRuntime
        { runtimeSubmittedCount = 0
        , runtimeRunCount = 0
        , runtimeLiveCount = 0
        , runtimeMaximumLiveCount = 0
        , runtimeFirstStartNanoseconds = Nothing
        , runtimeFinalSubmissionNanoseconds = Nothing
        , runtimeFinalCompletionNanoseconds = Nothing
        , runtimeExecutionNanoseconds = 0
        , runtimeLongestExecutionNanoseconds = 0
        }

-- | Bracket exactly the selected number of workers.  Cancelling the bracket
-- cancels each worker; a worker owning a subprocess in turn terminates and
-- reaps that process group through the ordinary supervisor boundary.
withVampireExecutor
    :: EffectiveJobs
    -> Vampire
    -> (WorkPosition -> PreparedVerificationRequest -> IO ())
    -> (VampireExecutor -> IO value)
    -> IO value
withVampireExecutor selected command observer action =
    Exception.bracket acquire release (action . fst)
  where
    workerCount = effectiveJobsValue selected

    acquire = do
        queue <- newTBQueueIO
            (fromIntegral workerCount * 2)
        state <- newTVarIO ExecutorRunning
        nextHandle <- newTVarIO 0
        runtime <- newTVarIO initialVampireExecutorRuntime
        let executor =
                VampireExecutor
                    { executorQueue = queue
                    , executorState = state
                    , executorNextHandle = nextHandle
                    , executorCommand = command
                    , executorRequestObserver = observer
                    , executorRuntime = runtime
                    }
        workers <- replicateM workerCount
            (async (superviseExecutorWorker executor))
        pure (executor, workers)

    release (executor, workers) = do
        atomically do
            state <- readTVar (executorState executor)
            case state of
                ExecutorRunning ->
                    writeTVar (executorState executor) ExecutorClosing
                ExecutorClosing ->
                    pure ()
                ExecutorFaulted{} ->
                    pure ()
        traverse_ cancel workers
        traverse_ waitCatch workers

-- | Bracket the complete set of handles submitted by one module pipeline.
-- Normal early return, failure, and asynchronous cancellation all cancel and
-- reap the remaining owned work before the scope is left.
withVampireRequestOwner
    :: VampireExecutor
    -> (VampireRequestOwner -> IO value)
    -> IO value
withVampireRequestOwner executor =
    Exception.bracket acquire release
  where
    acquire =
        VampireRequestOwner executor
            <$> newTVarIO (RequestOwnerOpen IntMap.empty)

    release owner = Exception.mask_ do
        handles <- atomically do
            state <- readTVar (requestOwnerState owner)
            case state of
                RequestOwnerClosed ->
                    pure []
                RequestOwnerOpen owned -> do
                    writeTVar (requestOwnerState owner) RequestOwnerClosed
                    pure (IntMap.elems owned)
        traverse_ signalVampireCancellation handles
        traverse_ awaitVampireCancellation handles
        traverse_ deregisterVampireHandle handles

runPreparedTypedProverWithExecutor
    :: (MonadIO io, MonadLogger io)
    => VampireRequestOwner
    -> WorkPosition
    -> PreparedTypedProverTask ref local origin global
    -> io (Either ProverProcessError ProverAnswer)
runPreparedTypedProverWithExecutor
        owner
        position
        (PreparedTypedProverTask
            _problem
            preparedRequest
            conjecture) = do
    startTime <- liftIO getCurrentTime
    answer <- liftIO do
        handle <- submitVampireRequest owner position preparedRequest
        awaitPreparedVampireRequest preparedRequest handle
            `Exception.onException` cancelVampireRequest handle
    endTime <- liftIO getCurrentTime
    let dialect =
            case preparedVerificationDialect preparedRequest of
                VerificationFof -> "FOF"
                VerificationTh0 -> "TH0"
    logInfoN
        (timeDifferenceToText startTime endTime
            <> " "
            <> conjecture
            <> " [typed "
            <> dialect
            <> "]")
    pure answer

vampireExecutorObservation
    :: VampireExecutor
    -> IO VampireExecutorObservation
vampireExecutorObservation executor = do
    runtime <- readTVarIO (executorRuntime executor)
    pure
        VampireExecutorObservation
            { vampireExecutorSubmittedCount = runtimeSubmittedCount runtime
            , vampireExecutorRunCount = runtimeRunCount runtime
            , vampireExecutorMaximumLiveCount =
                runtimeMaximumLiveCount runtime
            , vampireExecutorFirstStartNanoseconds =
                runtimeFirstStartNanoseconds runtime
            , vampireExecutorFinalSubmissionNanoseconds =
                runtimeFinalSubmissionNanoseconds runtime
            , vampireExecutorFinalCompletionNanoseconds =
                runtimeFinalCompletionNanoseconds runtime
            , vampireExecutorExecutionNanoseconds =
                runtimeExecutionNanoseconds runtime
            , vampireExecutorLongestExecutionNanoseconds =
                runtimeLongestExecutionNanoseconds runtime
            }

submitVampireRequest
    :: VampireRequestOwner
    -> WorkPosition
    -> PreparedVerificationRequest
    -> IO VampireHandle
submitVampireRequest owner position request = do
    -- Force the compact queue payload before masked ownership acquisition.
    _ <- Exception.evaluate (preparedVerificationByteCount request)
    _ <- Exception.evaluate (preparedVerificationRequestId request)
    Exception.mask_ do
        cancelled <- newTVarIO False
        started <- newTVarIO False
        completion <- newEmptyTMVarIO
        let executor = requestOwnerExecutor owner
        handle <- atomically do
            executorStatus <- readTVar (executorState executor)
            case executorStatus of
                ExecutorClosing -> throwSTM VampireExecutorClosed
                ExecutorFaulted fault -> throwSTM fault
                ExecutorRunning -> pure ()
            ownerStatus <- readTVar (requestOwnerState owner)
            owned <- case ownerStatus of
                RequestOwnerClosed -> throwSTM VampireRequestOwnerClosed
                RequestOwnerOpen current -> pure current
            ordinal <- readTVar (executorNextHandle executor)
            writeTVar (executorNextHandle executor) (ordinal + 1)
            let acquired =
                    VampireHandle
                        { vampireHandleOrdinal = ordinal
                        , vampireHandleOwner = owner
                        , vampireHandleRequestId =
                            preparedVerificationRequestId request
                        , vampireHandleCancelled = cancelled
                        , vampireHandleStarted = started
                        , vampireHandleCompletion = completion
                        }
                job =
                    ExecutorJob
                        { executorJobPosition = position
                        , executorJobRequest = request
                        , executorJobCancelled = cancelled
                        , executorJobStarted = started
                        , executorJobCompletion = completion
                        }
            writeTBQueue (executorQueue executor) job
            writeTVar
                (requestOwnerState owner)
                (RequestOwnerOpen (IntMap.insert ordinal acquired owned))
            modifyTVar'
                (executorRuntime executor)
                (\runtime ->
                    runtime
                        { runtimeSubmittedCount =
                            runtimeSubmittedCount runtime + 1
                        })
            pure acquired
        submitted <- getMonotonicTimeNSec
        atomically
            (modifyTVar'
                (executorRuntime executor)
                (\runtime ->
                    runtime
                        { runtimeFinalSubmissionNanoseconds =
                            Just
                                (maybe submitted
                                    (max submitted)
                                    (runtimeFinalSubmissionNanoseconds
                                        runtime))
                        }))
        pure handle

awaitVampireRequest :: VampireHandle -> IO VampireCompletion
awaitVampireRequest handle = Exception.mask \restore -> do
    let executor = requestOwnerExecutor (vampireHandleOwner handle)
    completion <- restore (atomically do
        executorStatus <- readTVar (executorState executor)
        case executorStatus of
            ExecutorFaulted fault -> throwSTM fault
            ExecutorRunning -> readTMVar (vampireHandleCompletion handle)
            ExecutorClosing ->
                (readTMVar (vampireHandleCompletion handle))
                    `orElse` throwSTM VampireExecutorClosed)
    deregisterVampireHandle handle
    pure completion

-- | Await one already submitted request and recover the ordinary typed
-- prover result.  The supplied immutable request is checked against every
-- completion before any caller may interpret its terminal outcome.
awaitPreparedVampireRequest
    :: PreparedVerificationRequest
    -> VampireHandle
    -> IO (Either ProverProcessError ProverAnswer)
awaitPreparedVampireRequest request handle =
    awaitVampireRequest handle >>= completionProverResult request

cancelVampireRequest :: VampireHandle -> IO ()
cancelVampireRequest handle = Exception.mask_ do
    signalVampireCancellation handle
    awaitVampireCancellation handle
    deregisterVampireHandle handle

signalVampireCancellation :: VampireHandle -> IO ()
signalVampireCancellation handle = do
    let executor = requestOwnerExecutor (vampireHandleOwner handle)
        completion =
            VampireCompletion
                (vampireHandleRequestId handle)
                VampireCancelled
    _ <- Exception.evaluate completion
    published <- getMonotonicTimeNSec
    atomically do
        writeTVar (vampireHandleCancelled handle) True
        started <- readTVar (vampireHandleStarted handle)
        unless started
            (void
                (publishVampireTerminalSTM
                    executor
                    (vampireHandleCompletion handle)
                    published
                    completion))

awaitVampireCancellation :: VampireHandle -> IO ()
awaitVampireCancellation handle =
    -- A running worker acknowledges ordinary cancellation only after
    -- terminating and reaping its owned process group.  After a global fault,
    -- the worker lifecycle flag is the acknowledgement because the terminal
    -- cell deliberately remains subordinate to that fault.
    atomically do
        executorStatus <- readTVar
            (executorState (requestOwnerExecutor (vampireHandleOwner handle)))
        case executorStatus of
            ExecutorFaulted{} -> do
                stillRunning <- readTVar (vampireHandleStarted handle)
                check (not stillRunning)
            _ -> void (readTMVar (vampireHandleCompletion handle))

deregisterVampireHandle :: VampireHandle -> IO ()
deregisterVampireHandle handle = atomically do
    let owner = vampireHandleOwner handle
    state <- readTVar (requestOwnerState owner)
    case state of
        RequestOwnerClosed -> pure ()
        RequestOwnerOpen owned ->
            writeTVar
                (requestOwnerState owner)
                (RequestOwnerOpen
                    (IntMap.delete (vampireHandleOrdinal handle) owned))

superviseExecutorWorker :: VampireExecutor -> IO ()
superviseExecutorWorker executor = do
    result <- Exception.try (executorWorker executor)
    case result of
        Right () -> pure ()
        Left workerFailure -> do
            state <- readTVarIO (executorState executor)
            case state of
                ExecutorRunning ->
                    recordExecutorFault executor workerFailure
                ExecutorClosing ->
                    pure ()
                ExecutorFaulted{} ->
                    pure ()

recordExecutorFault :: VampireExecutor -> SomeException -> IO ()
recordExecutorFault executor workerFailure = atomically do
    state <- readTVar (executorState executor)
    case state of
        ExecutorRunning ->
            writeTVar
                (executorState executor)
                (ExecutorFaulted
                    (VampireExecutorFault
                        (boundedText
                            (Text.pack (displayException workerFailure)))))
        ExecutorClosing -> pure ()
        ExecutorFaulted{} -> pure ()

executorWorker :: VampireExecutor -> IO ()
executorWorker executor = do
    next <- atomically do
        state <- readTVar (executorState executor)
        case state of
            ExecutorRunning -> Just <$> readTBQueue (executorQueue executor)
            ExecutorClosing -> pure Nothing
            ExecutorFaulted{} -> pure Nothing
    case next of
        Nothing -> pure ()
        Just job -> do
            shouldRun <- atomically do
                completed <- tryReadTMVar (executorJobCompletion job)
                case completed of
                    Just _ -> pure False
                    Nothing -> do
                        writeTVar (executorJobStarted job) True
                        pure True
            when shouldRun
                (executeJob executor job
                    `Exception.finally`
                        atomically (writeTVar (executorJobStarted job) False))
            executorWorker executor

data JobWait value
    = JobFinished !(Either SomeException value)
    | JobCancelled
    | JobExecutorStopped

executeJob :: VampireExecutor -> ExecutorJob -> IO ()
executeJob executor job =
    Exception.mask \restore -> do
        running <- async
            (restore
                (timedExecutorRun executor job))
        waited <- restore
            (atomically
                (do
                    state <- readTVar (executorState executor)
                    case state of
                        ExecutorRunning ->
                            (JobFinished <$> waitCatchSTM running)
                                `orElse`
                                (do
                                    cancelled <- readTVar
                                        (executorJobCancelled job)
                                    check cancelled
                                    pure JobCancelled)
                        ExecutorClosing -> pure JobExecutorStopped
                        ExecutorFaulted{} -> pure JobExecutorStopped))
            `Exception.onException`
                (cancel running >> void (waitCatch running))
        case waited of
            JobFinished result -> case result of
                Left workerFailure -> Exception.throwIO workerFailure
                Right terminal ->
                    publishVampireTerminal
                        executor
                        (preparedVerificationRequestId
                            (executorJobRequest job))
                        (executorJobCompletion job)
                        terminal
            JobCancelled -> do
                cancel running
                void (waitCatch running)
                publishVampireTerminal
                    executor
                    (preparedVerificationRequestId
                        (executorJobRequest job))
                    (executorJobCompletion job)
                    VampireCancelled
            JobExecutorStopped -> do
                cancel running
                void (waitCatch running)

timedExecutorRun
    :: VampireExecutor
    -> ExecutorJob
    -> IO VampireTerminal
timedExecutorRun executor job = Exception.mask \restore -> do
    started <- getMonotonicTimeNSec
    atomically
        (modifyTVar'
            (executorRuntime executor)
            (\runtime ->
                let live = runtimeLiveCount runtime + 1
                in runtime
                    { runtimeRunCount = runtimeRunCount runtime + 1
                    , runtimeLiveCount = live
                    , runtimeMaximumLiveCount =
                        max live (runtimeMaximumLiveCount runtime)
                    , runtimeFirstStartNanoseconds =
                        runtimeFirstStartNanoseconds runtime <|> Just started
                    }))
    terminal <- restore
        (runPreparedVerificationTerminal
            (executorRequestObserver executor (executorJobPosition job))
            (executorCommand executor)
            (executorJobRequest job))
        `Exception.onException` finishExecutorRun executor started
    finishExecutorRun executor started
    pure terminal

finishExecutorRun :: VampireExecutor -> Word64 -> IO ()
finishExecutorRun executor started = do
    finished <- getMonotonicTimeNSec
    let elapsed = finished - started
    atomically
        (modifyTVar'
            (executorRuntime executor)
            (\runtime ->
                runtime
                    { runtimeLiveCount = runtimeLiveCount runtime - 1
                    , runtimeExecutionNanoseconds =
                        runtimeExecutionNanoseconds runtime + elapsed
                    , runtimeLongestExecutionNanoseconds =
                        max elapsed (runtimeLongestExecutionNanoseconds runtime)
                    }))

publishVampireTerminal
    :: VampireExecutor
    -> Authority.PreparedRequestId
    -> TMVar VampireCompletion
    -> VampireTerminal
    -> IO ()
publishVampireTerminal executor requestId completionCell terminal = do
    let completion = VampireCompletion requestId terminal
    _ <- Exception.evaluate completion
    published <- getMonotonicTimeNSec
    void
        (atomically
            (publishVampireTerminalSTM
                executor completionCell published completion))

publishVampireTerminalSTM
    :: VampireExecutor
    -> TMVar VampireCompletion
    -> Word64
    -> VampireCompletion
    -> STM Bool
publishVampireTerminalSTM executor completionCell published completion = do
    inserted <- tryPutTMVar completionCell completion
    when inserted
        (modifyTVar'
            (executorRuntime executor)
            (\runtime ->
                runtime
                    { runtimeFinalCompletionNanoseconds =
                        Just
                            (maybe published
                                (max published)
                                (runtimeFinalCompletionNanoseconds runtime))
                    }))
    pure inserted

runPreparedVerificationTerminal
    :: (PreparedVerificationRequest -> IO ())
    -> Vampire
    -> PreparedVerificationRequest
    -> IO VampireTerminal
runPreparedVerificationTerminal observer command request = do
    transcriptResult <-
        runPreparedVampireProcessWithObserver observer command request
    pure case transcriptResult of
        Left processFailure ->
            VampireProcessFailed processFailure
        Right transcript ->
            case classifyVampireCompleted
                (preparedVerificationMode request)
                transcript of
                Left protocolFailure ->
                    VampireProtocolFailed
                        (boundedTranscriptDiagnostic
                            (Text.pack (show protocolFailure))
                            transcript)
                Right Proved ->
                    VampireAccepted
                Right Counterexample ->
                    VampireRejected
                        RejectedCounterexample
                        (boundedTranscriptDiagnostic
                            "Vampire found a countermodel"
                            transcript)
                Right ContradictoryInput ->
                    VampireRejected
                        RejectedContradictoryInput
                        (boundedTranscriptDiagnostic
                            "Vampire reported contradictory input"
                            transcript)
                Right Indeterminate ->
                    VampireRejected
                        RejectedIndeterminate
                        (boundedTranscriptDiagnostic
                            "Vampire did not establish the obligation"
                            transcript)

completionProverResult
    :: PreparedVerificationRequest
    -> VampireCompletion
    -> IO (Either ProverProcessError ProverAnswer)
completionProverResult request completion = do
    unless (actualId == expectedId)
        (Exception.throwIO
            (VampireExecutorFault
                "Vampire completion has the wrong request id"))
    case vampireCompletionTerminal completion of
        VampireAccepted ->
            pure
                (Right
                    (ProvedAnswer
                        (AcceptedVampireRun actualId)))
        VampireRejected rejection _diagnostic ->
            pure
                (Right
                    (case rejection of
                        RejectedCounterexample ->
                            CounterSatisfiable task
                        RejectedContradictoryInput ->
                            ContradictoryAxioms task
                        RejectedIndeterminate ->
                            Uncertain task))
        VampireProtocolFailed diagnostic ->
            pure
                (Right
                    (Error
                        "typed obligation"
                        (renderBoundedDiagnostic diagnostic)))
        VampireProcessFailed processFailure ->
            pure (Left processFailure)
        VampireCancelled ->
            Exception.throwIO
                (VampireExecutorFault
                    "active admission encountered a cancelled Vampire request")
  where
    expectedId = preparedVerificationRequestId request
    actualId = vampireCompletionRequestId completion
    task = preparedVerificationText request

runPreparedVampireProcessWithObserver
    :: (PreparedVerificationRequest -> IO ())
    -> Vampire
    -> PreparedVerificationRequest
    -> IO (Either ProverProcessError CompletedTranscript)
runPreparedVampireProcessWithObserver
    observer
    vampireCommand@Vampire{vampireExecutable = executable}
    preparedRequest = do
        callbackStarted <- newIORef False
        processResult <- Exception.try
            (withCreateProcess
                (proc executable (vampireArguments vampireCommand))
                    { std_in = CreatePipe
                    , std_out = CreatePipe
                    , std_err = CreatePipe
                    , create_group = True
                    }
                \mIn mOut mErr processHandle ->
                    Exception.mask \restore -> do
                    writeIORef callbackStarted True
                    case (mIn, mOut, mErr) of
                        (Just inputHandle, Just outputHandle, Just errorHandle) -> do
                            maybePid <- getPid processHandle
                            processGroup <- case maybePid of
                                Just pid ->
                                    pure (fromIntegral pid)
                                Nothing ->
                                    impossible
                                        "Vampire supervisor: missing process-group id"
                            restore
                                (do
                                    runRequestObserver
                                        observer
                                        preparedRequest
                                    superviseVampireProcess
                                        executable
                                        (vampireTimeLimit vampireCommand)
                                        preparedRequest
                                        inputHandle
                                        outputHandle
                                        errorHandle
                                        processGroup
                                        processHandle)
                                `Exception.onException`
                                    forceTerminateProcessGroup
                                        processGroup
                                        processHandle
                        _ ->
                            impossible
                                "Vampire supervisor: expected CreatePipe handles")
            :: IO
                (Either
                    SomeException
                    (Either ProverProcessError CompletedTranscript))
        case processResult of
            Right result ->
                pure result
            Left err
                | Just (RequestObserverFailure observerFailure) <-
                    fromException err ->
                        Exception.throwIO observerFailure
                | Just asynchronous <-
                    (fromException err :: Maybe AsyncException) ->
                        Exception.throwIO asynchronous
                | Just ioFailure <-
                    (fromException err :: Maybe IOException) -> do
                        started <- readIORef callbackStarted
                        pure
                            (Left
                                (if started
                                    then
                                        ProverLifecycleFailed
                                            executable
                                            (boundedText
                                                (exceptionText ioFailure))
                                    else
                                        ProverLaunchFailed
                                            executable
                                            (boundedText
                                                (exceptionText ioFailure))))
                | otherwise ->
                    Exception.throwIO err

runRequestObserver
    :: (PreparedVerificationRequest -> IO ())
    -> PreparedVerificationRequest
    -> IO ()
runRequestObserver observer request =
    observer request `Exception.catch` \observerError ->
        case fromException observerError :: Maybe AsyncException of
            Just asynchronous ->
                Exception.throwIO asynchronous
            Nothing ->
                Exception.throwIO
                    (RequestObserverFailure observerError)

superviseVampireProcess
    :: FilePath
    -> TimeLimit
    -> PreparedVerificationRequest
    -> Handle
    -> Handle
    -> Handle
    -> ProcessGroupID
    -> ProcessHandle
    -> IO (Either ProverProcessError CompletedTranscript)
superviseVampireProcess
    executable
    timeLimit
    preparedRequest
    inputHandle
    outputHandle
    errorHandle
    processGroup
    processHandle = do
        stdoutCapture <- newIORef emptyCaptureBuffer
        stderrCapture <- newIORef emptyCaptureBuffer
        let terminateOwnedProcess =
                forceTerminateProcessGroup
                    processGroup
                    processHandle
            communicate =
                communicateWithVampire
                    preparedRequest
                    inputHandle
                    outputHandle
                    errorHandle
                    stdoutCapture
                    stderrCapture
                    processHandle
        supervised <-
            Timeout.timeout
                (wallTimeoutMicroseconds timeLimit)
                (Exception.try communicate
                    :: IO (Either SupervisorAbort ExitCode))
        case supervised of
            Nothing -> do
                terminateOwnedProcess
                partial <-
                    capturedStreams
                        stdoutCapture
                        stderrCapture
                pure
                    (Left
                        (ProverTimedOut
                            executable
                            timeLimit
                            (boundedCapturedStreams partial)))
            Just (Left abort) -> do
                terminateOwnedProcess
                partial <-
                    capturedStreams
                        stdoutCapture
                        stderrCapture
                pure
                    (Left
                        (supervisorAbortError
                            executable
                            partial
                            abort))
            Just (Right exitCode) -> do
                terminateRemainingProcessGroup processGroup
                partial <-
                    capturedStreams
                        stdoutCapture
                        stderrCapture
                case exitCode of
                    ExitFailure signalCode
                        | signalCode < 0 ->
                            pure
                                (Left
                                    (ProverTerminatedBySignal
                                        executable
                                        (negate signalCode)
                                        (boundedCapturedStreams partial)))
                    _ ->
                        pure do
                            stdout <- decodeOutput
                                executable
                                ProverOutputStdout
                                (partialStdout partial)
                            stderr <- decodeOutput
                                executable
                                ProverOutputStderr
                                (partialStderr partial)
                            Right
                                CompletedTranscript
                                    { completedExitCode = exitCode
                                    , completedStreams =
                                        CompleteCapturedStreams
                                            { completedStdout = stdout
                                            , completedStderr = stderr
                                            }
                                    }

communicateWithVampire
    :: PreparedVerificationRequest
    -> Handle
    -> Handle
    -> Handle
    -> IORef CaptureBuffer
    -> IORef CaptureBuffer
    -> ProcessHandle
    -> IO ExitCode
communicateWithVampire
    preparedRequest
    inputHandle
    outputHandle
    errorHandle
    stdoutCapture
    stderrCapture
    processHandle = do
        _ <-
            concurrently
                (concurrently
                    (captureCommunication ProverStdin
                        (ByteString.hPut
                            inputHandle
                            (preparedVerificationInput preparedRequest)
                            `Exception.finally` hClose inputHandle))
                    (captureOutput
                        ProverOutputStdout
                        outputHandle
                        stdoutCapture))
                (captureOutput
                    ProverOutputStderr
                    errorHandle
                    stderrCapture)
        captureLifecycle (waitForProcess processHandle)

captureCommunication
    :: ProverStream
    -> IO a
    -> IO a
captureCommunication stream action =
    action `Exception.catch` \(err :: IOException) ->
        throwIO
            (SupervisorCommunicationFailed
                stream
                (exceptionText err))

captureOutput
    :: ProverOutputStream
    -> Handle
    -> IORef CaptureBuffer
    -> IO ()
captureOutput stream handle capture =
    captureCommunication (outputStream stream) go
  where
    go = do
        bytes <- ByteString.hGetSome handle captureChunkSize
        if ByteString.null bytes
            then pure ()
            else do
                exceeded <- appendCapturedChunk capture bytes
                if exceeded
                    then
                        throwIO
                            (SupervisorOutputLimitExceeded stream)
                    else go

outputStream :: ProverOutputStream -> ProverStream
outputStream = \case
    ProverOutputStdout ->
        ProverStdout
    ProverOutputStderr ->
        ProverStderr

captureLifecycle :: IO a -> IO a
captureLifecycle action =
    action `Exception.catch` \(err :: IOException) ->
        throwIO (SupervisorLifecycleFailed (exceptionText err))

emptyCaptureBuffer :: CaptureBuffer
emptyCaptureBuffer =
    CaptureBuffer
        { captureByteCount = 0
        , captureChunksReversed = []
        }

appendCapturedChunk
    :: IORef CaptureBuffer
    -> ByteString.ByteString
    -> IO Bool
appendCapturedChunk capture bytes =
    atomicModifyIORef' capture \buffer@CaptureBuffer{..} ->
        let remaining =
                vampireOutputByteLimit - captureByteCount
            retained =
                ByteString.take remaining bytes
            retainedLength =
                ByteString.length retained
            buffer' =
                buffer
                    { captureByteCount =
                        captureByteCount + retainedLength
                    , captureChunksReversed =
                        if ByteString.null retained
                            then captureChunksReversed
                            else retained : captureChunksReversed
                    }
        in (buffer', ByteString.length bytes > remaining)

capturedStreams
    :: IORef CaptureBuffer
    -> IORef CaptureBuffer
    -> IO PartialCapturedStreams
capturedStreams stdoutCapture stderrCapture =
    PartialCapturedStreams
        <$> capturedBytes stdoutCapture
        <*> capturedBytes stderrCapture

capturedBytes :: IORef CaptureBuffer -> IO ByteString.ByteString
capturedBytes capture =
    ByteString.concat
        . reverse
        . captureChunksReversed
        <$> readIORef capture

boundedTranscriptBytes :: Int
boundedTranscriptBytes = 32 * 1024

boundedTranscriptHalf :: Int
boundedTranscriptHalf = boundedTranscriptBytes `div` 2

boundedBytes :: ByteString.ByteString -> BoundedBytes
boundedBytes bytes =
    let original = ByteString.length bytes
    in if original <= boundedTranscriptBytes
        then
            BoundedBytes
                { boundedBytesOriginalCount = original
                , boundedBytesRetained = bytes
                , boundedBytesTruncated = False
                }
        else
            BoundedBytes
                { boundedBytesOriginalCount = original
                , boundedBytesRetained =
                    ByteString.take boundedTranscriptHalf bytes
                        <> ByteString.drop
                            (original - boundedTranscriptHalf)
                            bytes
                , boundedBytesTruncated = True
                }

boundedText :: Text -> Text
boundedText =
    decodeBoundedBytes . boundedBytes . TextEncoding.encodeUtf8

decodeBoundedBytes :: BoundedBytes -> Text
decodeBoundedBytes =
    TextEncoding.decodeUtf8With TextEncodingError.lenientDecode
        . boundedBytesRetained

boundedCapturedStreams
    :: PartialCapturedStreams
    -> BoundedCapturedStreams
boundedCapturedStreams PartialCapturedStreams{..} =
    BoundedCapturedStreams
        { boundedStdout = boundedBytes partialStdout
        , boundedStderr = boundedBytes partialStderr
        }

boundedTranscriptDiagnostic
    :: Text
    -> CompletedTranscript
    -> BoundedDiagnostic
boundedTranscriptDiagnostic summary CompletedTranscript{completedStreams = streams} =
    BoundedDiagnostic
        { boundedDiagnosticSummary = boundedText summary
        , boundedDiagnosticStdout =
            boundedBytes
                (TextEncoding.encodeUtf8 (completedStdout streams))
        , boundedDiagnosticStderr =
            boundedBytes
                (TextEncoding.encodeUtf8 (completedStderr streams))
        }

renderBoundedDiagnostic :: BoundedDiagnostic -> Text
renderBoundedDiagnostic BoundedDiagnostic{..} =
    Text.unlines
        [ boundedDiagnosticSummary
        , renderBoundedStream "stdout" boundedDiagnosticStdout
        , renderBoundedStream "stderr" boundedDiagnosticStderr
        ]

renderBoundedStream :: Text -> BoundedBytes -> Text
renderBoundedStream streamLabel bytes =
    streamLabel
        <> (if boundedBytesTruncated bytes
            then
                " (retained first and last 16 KiB of "
                    <> Text.pack (show (boundedBytesOriginalCount bytes))
                    <> " bytes)"
            else "")
        <> ":\n"
        <> decodeBoundedBytes bytes

supervisorAbortError
    :: FilePath
    -> PartialCapturedStreams
    -> SupervisorAbort
    -> ProverProcessError
supervisorAbortError executable partial = \case
    SupervisorCommunicationFailed stream message ->
        ProverCommunicationFailed executable stream (boundedText message)
    SupervisorOutputLimitExceeded stream ->
        ProverOutputLimitExceeded
            executable
            stream
            (boundedCapturedStreams partial)
    SupervisorLifecycleFailed message ->
        ProverLifecycleFailed executable (boundedText message)

wallTimeoutMicroseconds :: TimeLimit -> Int
wallTimeoutMicroseconds (Seconds seconds) =
    fromInteger
        (min
            (toInteger (maxBound :: Int))
            ((toInteger seconds + vampireWallGraceSeconds)
                * 1000000))

forceTerminateProcessGroup
    :: ProcessGroupID
    -> ProcessHandle
    -> IO ()
forceTerminateProcessGroup processGroup processHandle =
    Exception.uninterruptibleMask_ do
        terminateRemainingProcessGroup processGroup
        _ <- waitForProcess processHandle
        pure ()

terminateRemainingProcessGroup :: ProcessGroupID -> IO ()
terminateRemainingProcessGroup processGroup =
    ignoreMissingProcess
        (signalProcessGroup sigKILL processGroup)

ignoreMissingProcess :: IO () -> IO ()
ignoreMissingProcess action =
    action `Exception.catch` \(err :: IOException) ->
        if isDoesNotExistError err
            then pure ()
            else throwIO err

decodeOutput
    :: FilePath
    -> ProverOutputStream
    -> ByteString.ByteString
    -> Either ProverProcessError Text
decodeOutput executable stream bytes =
    case TextEncoding.decodeUtf8' bytes of
        Left err ->
            Left
                (ProverOutputMalformedUtf8
                    executable
                    stream
                    (boundedText (Text.pack (show err))))
        Right output ->
            Right output

exceptionText :: IOException -> Text
exceptionText =
    Text.pack . displayException

classifyVampireCompleted
    :: VampireTaskMode
    -> CompletedTranscript
    -> Either VampireProtocolError CanonicalAtpOutcome
classifyVampireCompleted mode CompletedTranscript{..} =
    case completedExitCode of
        ExitFailure _ ->
            classifyVampireProtocol mode completedExitCode []
        ExitSuccess -> do
            statuses <- statusesFromCompleteStreams completedStreams
            classifyVampireProtocol mode completedExitCode statuses

statusesFromCompleteStreams
    :: CompleteCapturedStreams
    -> Either VampireProtocolError [VampireStatus]
statusesFromCompleteStreams CompleteCapturedStreams{..}
    | Set.null malformed =
        Right statuses
    | otherwise =
        Left (MalformedVampireStatusLines malformed)
  where
    (malformed, statuses) =
        foldMap classifyLine
            (Text.lines completedStdout <> Text.lines completedStderr)

    classifyLine line =
        case parseMaybe vampireStatusParser line of
            Just status ->
                (mempty, [status])
            Nothing
                | "SZS status" `Text.isInfixOf` line ->
                    (Set.singleton line, [])
                | otherwise ->
                    mempty

vampireStatusFromText :: Text -> VampireStatus
vampireStatusFromText = \case
    "Theorem" -> StatusTheorem
    "CounterSatisfiable" -> StatusCounterSatisfiable
    "ContradictoryAxioms" -> StatusContradictoryAxioms
    "Timeout" -> StatusTimeout
    "ResourceOut" -> StatusResourceOut
    "GaveUp" -> StatusGaveUp
    "Unknown" -> StatusUnknown
    status -> UnsupportedStatus status

-- | Parse a Vampire SZS status line.
--
-- Recognizes both standard lines like:
--   % SZS status Timeout for 123
-- and lines prefixed by worker ids (seen with portfolio output), e.g.:
--   % (2581105)SZS status Timeout for
vampireStatusParser :: Parsec Void Text VampireStatus
vampireStatusParser = do
    _ <- Char.char '%'
    Char.hspace
    optional do
        _ <- Char.char '('
        _ <- some Char.digitChar
        _ <- Char.char ')'
        Char.hspace
    _ <- chunk "SZS"
    Char.hspace1
    _ <- chunk "status"
    Char.hspace1
    status <-
        takeWhile1P
            (Just "SZS status")
            (\character -> character /= ' ' && character /= '\t')
    _ <- takeRest
    pure (vampireStatusFromText status)

nominalDiffTimeToText :: NominalDiffTime -> Text
nominalDiffTimeToText delta =
    toText (nominalDiffTimeToTextBuilder delta)

nominalDiffTimeToTextBuilder :: NominalDiffTime -> TextBuilder
nominalDiffTimeToTextBuilder delta =
    case hours of
        0 ->
            padded minutes
                <> ":"
                <> padded restSeconds
                <> "."
                <> padded restCentis
        _ ->
            padded hours
                <> ":"
                <> padded restMinutes
                <> ":"
                <> padded restSeconds
  where
    padded n =
        if n < 10
            then char '0' <> decimal n
            else decimal n
    centiseconds =
        truncate (100 * nominalDiffTimeToSeconds delta) :: Int
    (seconds, restCentis) = divMod centiseconds 100
    (minutes, restSeconds) = divMod seconds 60
    (hours, restMinutes) = divMod minutes 60

timeDifferenceToText :: UTCTime -> UTCTime -> Text
timeDifferenceToText startTime endTime =
    nominalDiffTimeToText (diffUTCTime endTime startTime)