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

{-# LANGUAGE NoImplicitPrelude #-}

module Test.Unit.Module (unitTests) where

import Base
import Api qualified
import Checking.Authority qualified as Authority
import Checking.Backend.Problem qualified as Backend
import Checking.Core qualified as Core
import Checking.Declaration qualified as Declaration
import Checking.Exact qualified as Exact
import Checking.Exact.Datatype qualified as ExactDatatype
import Checking.Exact.Inductive qualified as ExactInductive
import Checking.Exact.Proof qualified as ExactProof
import Checking.FinalPrelude qualified as FinalPrelude
import Checking.Foundation qualified as Foundation
import Checking.Identity qualified as Identity
import Checking.Module qualified as Module
import Checking.Semantic qualified as Semantic
import Checking.Typed.Inductive qualified as TypedInductive
import CommandLine qualified
import Felix.Module
import Felix.Math.Codec
import Felix.Parse qualified as Parse
import Felix.Prelude qualified as Prelude
import Felix.Source
import Felix.Source.Content qualified as Content
import Felix.Store qualified as Store
import Report.Location
import Provers qualified
import Paths_felix qualified as Paths
import Syntax.Abstract qualified as Raw
import Syntax.Internal qualified as Internal
import Syntax.Interface qualified as Syntax
import Syntax.Pragma qualified as Pragma

import Control.Concurrent (threadDelay)
import Control.Concurrent.STM
    ( atomically
    , check
    , newEmptyTMVarIO
    , newTQueueIO
    , newTVarIO
    , putTMVar
    , readTQueue
    , readTVar
    , takeTMVar
    , tryReadTMVar
    , tryReadTQueue
    , writeTQueue
    , writeTVar
    )
import Control.Exception (bracket)
import Control.Monad (foldM, when)
import Data.ByteString qualified as ByteString
import Data.Text qualified as StrictText
import Data.Text.Encoding qualified as Text
import Control.Monad.Logger (runNoLoggingT)
import Data.IORef
    ( IORef
    , atomicModifyIORef'
    , modifyIORef'
    , newIORef
    , readIORef
    )
import Data.List (sort)
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Vector qualified as Vector
import System.Directory
    ( createDirectoryIfMissing
    , doesFileExist
    , getCurrentDirectory
    , getPermissions
    , setOwnerExecutable
    , setPermissions
    )
import System.FilePath.Posix qualified as Posix
import System.IO.Temp qualified as Temp
import System.Timeout qualified as Timeout
import Test.Tasty
import Test.Tasty.HUnit
import UnliftIO.Async (withAsync, wait)


unitTests :: TestTree
unitTests =
    testGroup "Typed module inputs"
        [ testCase "constructs the empty bootstrap ordinarily"
            constructsEmptyBootstrap
        , testCase "identifies comment-only reserved input"
            identifiesCommentOnlyInput
        , testCase "loads and parses the packaged final prelude"
            parsesPackagedFinalPrelude
        , testCase "renders packaged final-prelude failures"
            rendersPackagedPreludeFailures
        , testCase "confines exact foundation-leaf completion"
            confinesFoundationLeafCompletion
        , testCase "builds the confined final prelude"
            buildsConfinedFinalPrelude
        , testCase "publishes the final prelude as an ordinary sealed root"
            publishesFinalPreludeRoot
        , testCase "retains exact omitted-proof locations"
            retainsExactOmittedProofLocation
        , testCase "coalesces syntax without collapsing semantic imports"
            coalescesSharedDirectSyntax
        , testCase "makes selected source errors terminal"
            rejectsUnsupportedTypedSource
        , testCase "compiles exact declarations across an import"
            compilesExactDeclarationGraph
        , testCase "compiles and imports exact structures"
            compilesExactStructures
        , testCase "compiles and caches contextual abbreviations"
            compilesContextualAbbreviations
        , testCase "rejects an unknown exact structure parent atomically"
            rejectsUnknownExactStructureParent
        , testCase "compiles exact relation expressions"
            compilesExactRelationExpressions
        , testCase "resolves source-owned set application"
            resolvesSourceOwnedApplication
        , testCase "confines quantified terms to exact statement subjects"
            confinesExactQuantifiedTerms
        , testCase "compiles exact ordinary proofs"
            compilesExactOrdinaryProofs
        , testCase "compiles and reuses proof-local set definitions"
            compilesAndReusesProofLocalSetDefinitions
        , testCase "compiles and reuses proof-local function graphs"
            compilesAndReusesProofLocalFunctionGraphs
        , testCase "confines terminal exact contradiction"
            confinesTerminalExactContradiction
        , testCase "compiles exact separation comprehensions"
            compilesExactSeparationComprehensions
        , testCase "compiles exact replacement comprehensions"
            compilesExactReplacementComprehensions
        , testCase "compiles and reuses exact finite sets"
            compilesAndReusesExactFiniteSets
        , testCase "prepares exact deterministic datatypes"
            preparesExactDatatypes
        , testCase "rejects nested exact datatype recursion"
            rejectsNestedExactDatatypeRecursion
        , testCase "compiles and reuses exact datatypes"
            compilesAndReusesExactDatatypes
        , testCase "prepares exact direct inductives"
            preparesExactDirectInductives
        , testCase "rejects nested exact inductive recursion"
            rejectsNestedExactInductiveRecursion
        , testCase "compiles and reuses exact inductives"
            compilesAndReusesExactInductives
        , testCase "authorizes recursive exact inductives"
            authorizesRecursiveExactInductives
        , testCase "reuses exact separation validation"
            reusesExactSeparationValidation
        , testCase "compiles exact source axioms"
            compilesExactSourceAxioms
        , testCase "does not treat marker-only nouns as the fixed set noun"
            doesNotTreatMarkerOnlyNounAsSet
        , testCase "rejects proof-local generalization"
            rejectsProofLocalGeneralization
        , testCase "rejects nested exact set induction"
            rejectsNestedExactSetInduction
        , testCase "compiles exact omitted proofs"
            compilesExactOmittedProofs
        , testCase "propagates and reuses exact escape authority"
            reusesExactEscapeAuthority
        , testCase "checks continuations after omitted subclaims"
            rejectsAfterExactOmittedSubclaim
        , testCase "reuses exact proof validation across module misses"
            reusesExactProofValidationAcrossModuleMisses
        , testCase "rejects declarations of fixed semantics"
            rejectsFixedSemanticDeclaration
        , testCase "rejects inductive carriers with fixed semantics"
            rejectsFixedSemanticInductive
        , testCase "keeps exact semantics independent of fixity"
            keepsExactSemanticsIndependentOfFixity
        , testCase "loads a cached exact producer for a fresh importer"
            loadsCachedExactProducerForFreshImporter
        , testCase "reports admitted source escapes on fresh, warm, and failure paths"
            reportsAdmittedSourceEscapes
        , testCase "selects concurrent module failures by source order"
            selectsConcurrentModuleFailureDeterministically
        , testCase "batches independent structure obligations atomically"
            batchesStructureObligationsAtomically
        , testCase "speculates dependent proof obligations without admitting ahead"
            speculatesDependentProofObligationsWithoutAdmittingAhead
        , testCase "starts diamond consumers after sealed acknowledgements"
            schedulesDiamondAfterSealedImports
        , testCase "classifies typed Vampire failures conservatively"
            classifiesTypedVampireFailures
        , testCase "retains the exact prefix before a later failure"
            retainsExactPrefixBeforeFailure
        , testCase "routes every production root through exact checking"
            routesProductionVerification
        , testCase "installs nonempty implicit prelude evidence"
            installsNonemptyImplicitPreludeEvidence
        ]

constructsEmptyBootstrap :: Assertion
constructsEmptyBootstrap = do
    foundation <- expectRight Foundation.checkedFoundation
    result <-
        Module.buildBootstrapPreludeFixture
            foundation
            unusedResolver
    session <- expectRight result
    let input = Module.bootstrapPreludeInput session
        parsed = Module.identifiedModuleParsed input
        sealed = Module.bootstrapPreludeModule session
        syntax = Module.sealedTypedModuleSyntax sealed
        semantic = Module.sealedTypedModuleSemantic sealed
    assertEqual "reserved owner"
        preludeModuleName
        (Module.identifiedModuleOwner input)
    case Module.identifiedModuleBinding input of
        Module.ReservedModuleBinding fileId label -> do
            assertEqual "diagnostic label"
                Prelude.preludeDiagnosticLabel
                label
            assertEqual "registered display label"
                (Just Prelude.preludeDiagnosticLabel)
                (lookupFilePath fileId)
            assertEqual "registered identity label"
                (Just Prelude.preludeDiagnosticLabel)
                (lookupFileIdentityPath fileId)
        Module.PhysicalModuleBinding source ->
            assertFailure
                ("bootstrap acquired a physical source: " <> show source)
    assertEqual "empty parsed blocks"
        []
        (Parse.identifiedParsedModuleBlocks parsed)
    assertEqual "exact empty source identity"
        (Content.sourceContentIdBytes ByteString.empty)
        (Parse.identifiedParsedModuleSourceContentId parsed)
    assertEqual "no syntax imports"
        []
        (Syntax.moduleSyntaxDirectInputs syntax)
    assertEqual "empty local syntax"
        []
        (Syntax.canonicalSyntaxDeltaEntries
            (Syntax.moduleSyntaxLocalDelta syntax))
    assertEqual "semantic owner"
        preludeModuleName
        (Semantic.semanticInterfaceOwner semantic)
    assertEqual "no semantic imports"
        []
        (Semantic.semanticInterfaceDirectInputs semantic)
    assertEqual "no semantic declarations"
        []
        (Semantic.semanticInterfaceDeclarations semantic)
    expectedPrefix <-
        expectRight
            (Semantic.initialPrefixContextId
                (Identity.theoryId foundation)
                preludeModuleName
                [])
    assertEqual "empty sealed prefix"
        expectedPrefix
        (Declaration.pendingModulePrefixCurrent
            (Module.sealedTypedModulePrefix sealed))

identifiesCommentOnlyInput :: Assertion
identifiesCommentOnlyInput = do
    emptySource <-
        expectRight
            =<< Prelude.parseReservedPreludeSource
                Prelude.emptyBootstrapSourceInput
    source <-
        expectRight
            (Prelude.reservedPreludeSourceInput
                (Text.encodeUtf8 "% an in-memory comment\n"))
    first <-
        expectRight
            =<< Prelude.parseReservedPreludeSource source
    second <-
        expectRight
            =<< Prelude.parseReservedPreludeSource source
    let emptyParsed = Prelude.reservedParsedPreludeModule emptySource
        firstParsed = Prelude.reservedParsedPreludeModule first
        secondParsed = Prelude.reservedParsedPreludeModule second
    assertEqual "reserved live source binding"
        Parse.FreshReservedSource
        (Parse.freshModuleInputBinding
            (Prelude.reservedParsedPreludeInput first))
    assertEqual "comment-only source has no blocks"
        []
        (Parse.identifiedParsedModuleBlocks firstParsed)
    assertBool "content changes parsed identity"
        (Parse.identifiedParsedModuleId emptyParsed
            /= Parse.identifiedParsedModuleId firstParsed)
    assertEqual "same input has stable parsed identity"
        (Parse.identifiedParsedModuleId firstParsed)
        (Parse.identifiedParsedModuleId secondParsed)
    assertEqual "comments do not change syntax"
        (Syntax.moduleSyntaxAssertedId
            (Parse.identifiedParsedModuleSyntaxInterface emptyParsed))
        (Syntax.moduleSyntaxAssertedId
            (Parse.identifiedParsedModuleSyntaxInterface firstParsed))

parsesPackagedFinalPrelude :: Assertion
parsesPackagedFinalPrelude = do
    path <- Paths.getDataFileName "data/felix-prelude.tex"
    expectedBytes <- ByteString.readFile path
    source <- expectRight =<< Prelude.loadReservedPreludeSourceInput
    assertEqual "exact packaged bytes"
        expectedBytes
        (Prelude.reservedPreludeSourceBytes source)
    assertEqual "reserved owner"
        preludeModuleName
        (Prelude.reservedPreludeSourceOwner source)
    assertEqual "diagnostic label"
        Prelude.preludeDiagnosticLabel
        (Prelude.reservedPreludeSourceLabel source)
    first <- expectRight =<< Prelude.parseReservedPreludeSource source
    second <- expectRight =<< Prelude.parseReservedPreludeSource source
    let firstInput = Prelude.reservedParsedPreludeInput first
        firstParsed = Prelude.reservedParsedPreludeModule first
        secondParsed = Prelude.reservedParsedPreludeModule second
    assertEqual "no textual imports"
        []
        (Parse.freshModuleInputImports firstInput)
    assertBool "declaration-bearing source"
        (not (null (Parse.identifiedParsedModuleBlocks firstParsed)))
    assertEqual "deterministic syntax interface"
        (Syntax.moduleSyntaxAssertedId
            (Parse.identifiedParsedModuleSyntaxInterface firstParsed))
        (Syntax.moduleSyntaxAssertedId
            (Parse.identifiedParsedModuleSyntaxInterface secondParsed))

rendersPackagedPreludeFailures :: Assertion
rendersPackagedPreludeFailures = do
    assertEqual "load failure"
        "/missing/felix-prelude.tex: unable to read packaged final prelude: not found"
        (Prelude.renderPreludeLoadError
            (Prelude.PreludeSourceReadFailed
                "/missing/felix-prelude.tex"
                "not found"))
    assertEqual "located syntax failure"
        "<felix-prelude>: syntax pragma location is out of range at 7:3"
        (Prelude.renderPreludeParseError parseFailure)
    assertEqual "authority-free API presentation"
        ("packaged final prelude parsing failed: "
            <> "<felix-prelude>: syntax pragma location is out of range at 7:3")
        (Api.renderAuthorityFreeParseError
            (Api.AuthorityFreePreludeParseFailed parseFailure))
  where
    parseFailure =
        Prelude.PreludeSyntaxPragmaFailed
            (Pragma.SyntaxPragmaLocationOutOfRange
                Prelude.preludeDiagnosticLabel
                7
                3)

confinesFoundationLeafCompletion :: Assertion
confinesFoundationLeafCompletion = do
    foundation <- expectRight Foundation.checkedFoundation
    packaged <- expectRight =<< Prelude.loadReservedPreludeSourceInput
    parsed <- expectRight =<< Prelude.parseReservedPreludeSource packaged
    matching <- sole "matching foundation claim"
        (take 1
            (Parse.identifiedParsedModuleBlocks
                (Prelude.reservedParsedPreludeModule parsed)))
    mismatchInput <-
        expectRight
            (Prelude.reservedPreludeSourceInput
                (Text.encodeUtf8
                    "\\begin{proposition}\\label{not_foundation}\n    $\\emptyset = \\emptyset$.\n\\end{proposition}\n"))
    mismatchParsed <-
        expectRight =<< Prelude.parseReservedPreludeSource mismatchInput
    mismatch <- sole "mismatching claim"
        (Parse.identifiedParsedModuleBlocks
            (Prelude.reservedParsedPreludeModule mismatchParsed))
    outcome <-
        Declaration.runModuleDriver
            foundation
            preludeModuleName
            []
            unusedResolver
            Declaration.FreshValidation do
                explicit <-
                    admitFoundationClaim
                        foundation
                        matching
                        (Just (Raw.Omitted (locate matching)))
                nonmatching <-
                    admitFoundationClaim
                        foundation
                        mismatch
                        Nothing
                committed <-
                    admitFoundationClaim
                        foundation
                        matching
                        Nothing
                pure (explicit, nonmatching, committed)
    case outcome of
        Right (Declaration.DriverSucceeded
                (explicit, nonmatching, committed)
                _semantic _prefix _closure) -> do
            case explicit of
                Left ExactProof.ExactProofFoundationLeafRequiresImplicitAuto{} ->
                    pure ()
                Left other ->
                    assertFailure
                        ("explicit foundation result: " <> show other)
                Right{} ->
                    assertFailure "explicit foundation proof was accepted"
            batch <- expectRight committed
            case nonmatching of
                Left ExactProof.ExactProofFoundationLeafTargetMismatch{} ->
                    pure ()
                Left other ->
                    assertFailure
                        ("mismatching foundation result: " <> show other)
                Right{} ->
                    assertFailure "mismatching foundation claim was accepted"
            assertEqual "foundation tag"
                Foundation.UnivOfContains
                (case Declaration.committedBatchProofValidations batch of
                    [record] ->
                        case Authority.validationDirectAuthorization
                                (Semantic.proofValidationRecordCertificate
                                    record) of
                            Authority.CheckedKernelConstruction
                                    (Authority.FoundationLeaf tag) ->
                                tag
                            authorization ->
                                error
                                    ("unexpected foundation authorization: "
                                        <> show authorization)
                    records ->
                        error
                            ("unexpected foundation validation count: "
                                <> show (length records)))
        Right Declaration.DriverFailed{} ->
            assertFailure "foundation driver failed"
        Right (Declaration.DriverSealFailed failure _prefix) ->
            assertFailure ("foundation driver did not seal: " <> show failure)
        Left failure ->
            assertFailure ("foundation driver did not open: " <> show failure)
  where
    admitFoundationClaim foundation block proof =
        Declaration.runProspectiveLoweringDriver
            (ExactProof.prepareFinalPreludeFoundationClaim
                foundation block proof) >>= \case
                Left failure -> pure (Left failure)
                Right prepared -> do
                    lowered <-
                        Declaration.runProspectiveLoweringDriver
                            (ExactProof.lowerPreparedFinalPreludeFoundationClaim
                                prepared)
                    checked <-
                        either Declaration.failDeclarationDriver pure lowered
                    batch <-
                        Declaration.admitCheckedDeclaration
                            checked
                            ExactProof.authorizeCheckedFinalPreludeFoundationClaim
                    pure (Right batch)

buildsConfinedFinalPrelude :: Assertion
buildsConfinedFinalPrelude = do
    foundation <- expectRight Foundation.checkedFoundation
    FinalPrelude.buildFinalPreludeCandidate
            foundation finalPreludeResolver >>= \case
        FinalPrelude.FinalPreludeBuilt candidate -> do
            assertEqual "confined semantic owner"
                preludeModuleName
                (Semantic.semanticInterfaceOwner
                    (FinalPrelude.finalPreludeSemantic candidate))
            assertEqual "confined semantic imports"
                []
                (Semantic.semanticInterfaceDirectInputs
                    (FinalPrelude.finalPreludeSemantic candidate))
            let baseDeltas =
                    [ delta
                    | delta <- Semantic.semanticInterfaceDeclarations
                        (FinalPrelude.finalPreludeSemantic candidate)
                    , not
                        (null
                            (Semantic.semanticEnvironmentStructures
                                (Semantic.declarationDeltaEnvironment delta)))
                    ]
            case baseDeltas of
                [delta] -> do
                    assertEqual "base structure has no facts"
                        []
                        (Semantic.declarationDeltaFacts delta)
                    assertEqual "base structure has no propositions"
                        []
                        (Semantic.declarationDeltaPropositions delta)
                    case Semantic.semanticEnvironmentStructures
                            (Semantic.declarationDeltaEnvironment delta) of
                        [descriptor] -> do
                            assertEqual "base structure is metadata-only"
                                Nothing
                                (Semantic.semanticStructureDescriptorPredicate
                                    descriptor)
                            case Semantic.semanticStructureDescriptorOperations
                                    descriptor of
                                [operation] ->
                                    case Identity.lookupCheckedObjectContent
                                            (Semantic.semanticStructureOperationObject
                                                operation)
                                            (FinalPrelude.finalPreludeObjects candidate) of
                                        Just Identity.OpaqueObjectContent{} -> pure ()
                                        content ->
                                            assertFailure
                                                ("expected opaque carrier, got "
                                                    <> show content)
                                operations ->
                                    assertFailure
                                        ("expected one base operation, got "
                                            <> show operations)
                        descriptors ->
                            assertFailure
                                ("expected one base descriptor, got "
                                    <> show descriptors)
                deltas ->
                    assertFailure
                        ("expected one base structure delta, got "
                            <> show (length deltas))
            let role roleName =
                    maybe
                        (assertFailure
                            ("missing final-prelude role "
                                <> show roleName))
                        pure
                        (FinalPrelude.finalPreludePublicRole
                            candidate roleName)
            omega <- role FinalPrelude.PreludeOmegaObject
            naturals <- role FinalPrelude.PreludeNaturalsAlias
            assertEqual "naturals expands to Omega"
                omega naturals
            traverse_
                (void . role)
                (Set.toList FinalPrelude.expectedFinalPreludePublicRoles)
            let foundationTags = Set.fromList
                    [ tag
                    | batch <-
                        Declaration.pendingModulePrefixBatches
                            (FinalPrelude.finalPreludePrefix candidate)
                    , record <-
                        Declaration.committedBatchProofValidations batch
                    , Authority.CheckedKernelConstruction
                        (Authority.FoundationLeaf tag) <-
                            [ Authority.validationDirectAuthorization
                                (Semantic.proofValidationRecordCertificate
                                    record)
                            ]
                    ]
            assertBool "protected foundation presentation"
                ( Set.fromList
                    [ Foundation.SetExtensionality
                    , Foundation.EmptyCharacteristic
                    , Foundation.PairSetCharacteristic
                    , Foundation.FamilyUnionCharacteristic
                    ]
                    `Set.isSubsetOf` foundationTags
                )
            assertFinalPreludeFoundationAlias
                candidate
                "pairset_iff"
                Foundation.PairSetCharacteristic
            assertFinalPreludeFoundationAlias
                candidate
                "pow_iff"
                Foundation.PowerSetCharacteristic
        FinalPrelude.FinalPreludeBuildFailed failure prefix ->
            assertFailure
                ("final prelude failed after "
                    <> show
                        (length
                            (Declaration.pendingModulePrefixBatches prefix))
                    <> " declarations: "
                    <> show failure)
        FinalPrelude.FinalPreludeBuildOpenFailed failure ->
            assertFailure ("final prelude did not open: " <> show failure)
        FinalPrelude.FinalPreludeSourceLoadFailed failure ->
            assertFailure ("final prelude did not load: " <> show failure)
        FinalPrelude.FinalPreludeSourceParseFailed failure ->
            assertFailure ("final prelude did not parse: " <> show failure)

publishesFinalPreludeRoot :: Assertion
publishesFinalPreludeRoot = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-final-prelude-root" \directory -> do
        let path = directory Posix.</> "store.sqlite"
            theory = Identity.theoryId foundation
            open = do
                (_startup, store) <-
                    Store.openStore path theory >>= expectRight
                pure store
        bracket open Store.closeStore \store -> do
            freshMemo <- Store.newStoreMemo store
            session <-
                expectRight
                    =<< Module.acquireFinalPreludeSession
                        freshMemo store foundation finalPreludeResolver
            let input = Module.finalPreludeInput session
                sealed = Module.finalPreludeModule session
                syntax = Module.sealedTypedModuleSyntax sealed
                semantic = Module.sealedTypedModuleSemantic sealed
            assertEqual "empty store constructs the final-prelude root"
                Module.ModuleRootMiss
                (Module.finalPreludeAcquisition session)
            assertEqual "final prelude owner"
                preludeModuleName
                (Module.identifiedModuleOwner input)
            assertEqual "final prelude has no semantic parents"
                []
                (Semantic.semanticInterfaceDirectInputs semantic)
            warmMemo <- Store.newStoreMemo store
            warmSession <- expectRight
                =<< Module.acquireFinalPreludeSession
                    warmMemo store foundation unusedResolver
            let cached = Module.finalPreludeModule warmSession
            assertEqual "persisted final-prelude root is a cache hit"
                Module.ModuleRootHit
                (Module.finalPreludeAcquisition warmSession)
            assertEqual "generic root syntax"
                syntax
                (Module.sealedTypedModuleSyntax cached)
            assertEqual "generic root semantics"
                semantic
                (Module.sealedTypedModuleSemantic cached)
            assertEqual "cached base structure descriptor"
                (semanticStructureDescriptors semantic)
                (semanticStructureDescriptors
                    (Module.sealedTypedModuleSemantic cached))
            assertEqual "generic root final prefix"
                (Declaration.pendingModulePrefixCurrent
                    (Module.sealedTypedModulePrefix sealed))
                (Declaration.pendingModulePrefixCurrent
                    (Module.sealedTypedModulePrefix cached))
            visits <- Store.storeMemoVisits warmMemo
            assertEqual "cached prelude validates one artifact root"
                1
                (Store.storeArtifactsValidated visits)

semanticStructureDescriptors
    :: Semantic.SemanticInterface
    -> [Semantic.SemanticStructureDescriptor]
semanticStructureDescriptors semantic =
    [ descriptor
    | delta <- Semantic.semanticInterfaceDeclarations semantic
    , descriptor <- Semantic.semanticEnvironmentStructures
        (Semantic.declarationDeltaEnvironment delta)
    ]

assertTransparentObjectAlias
    :: Module.SealedTypedModule
    -> Text
    -> Assertion
assertTransparentObjectAlias sealed name = do
    target <- localObjectAliasTarget sealed name
    assertEqual
        ("transparent object for " <> StrictText.unpack name)
        Identity.TransparentObject
        (Identity.objectIdFamily target)

localObjectKeyTarget
    :: Module.SealedTypedModule
    -> Semantic.SemanticGlobalKey
    -> IO Identity.ObjectId
localObjectKeyTarget sealed key = do
    binding <- sole
        ("semantic binding for " <> show key)
        [ candidate
        | delta <- localSemanticDeltas sealed
        , candidate <- Semantic.semanticEnvironmentBindings
            (Semantic.declarationDeltaEnvironment delta)
        , Semantic.semanticGlobalBindingKey candidate == key
        ]
    pure
        (Semantic.semanticGlobalTargetObject
            (Semantic.semanticGlobalBindingTarget binding))

localObjectAliasTarget
    :: Module.SealedTypedModule
    -> Text
    -> IO Identity.ObjectId
localObjectAliasTarget sealed name = do
    delta <- localDeltaByAlias sealed name
    binding <- sole
        ("semantic binding for " <> StrictText.unpack name)
        (Semantic.semanticEnvironmentBindings
            (Semantic.declarationDeltaEnvironment delta))
    pure
        (Semantic.semanticGlobalTargetObject
            (Semantic.semanticGlobalBindingTarget binding))

checkedPropositionTermByAlias
    :: Module.SealedTypedModule
    -> Text
    -> IO (Core.FrozenCheckedCore Identity.ObjectId)
checkedPropositionTermByAlias sealed name = do
    batch <- batchByAlias
        (Module.sealedTypedModulePrefix sealed)
        name
    alias <- sole
        ("semantic alias for " <> StrictText.unpack name)
        [ candidate
        | candidate <- Semantic.declarationDeltaAliases
            (Declaration.committedBatchDelta batch)
        , Semantic.semanticAliasName candidate
            == Semantic.semanticName name
        ]
    occurrence <- sole
        ("semantic fact for " <> StrictText.unpack name)
        [ candidate
        | candidate <- Semantic.declarationDeltaFacts
            (Declaration.committedBatchDelta batch)
        , Semantic.semanticFactFingerprint candidate
            == Semantic.semanticAliasTarget alias
        ]
    proposition <- sole
        ("checked proposition for " <> StrictText.unpack name)
        [ candidate
        | candidate <- Declaration.committedBatchPropositions batch
        , Identity.checkedPropositionId candidate
            == Semantic.semanticFactProposition occurrence
        ]
    pure (Identity.checkedPropositionTerm proposition)

assertCleanFactAlias
    :: Module.SealedTypedModule
    -> Text
    -> Assertion
assertCleanFactAlias sealed name = do
    delta <- localDeltaByAlias sealed name
    alias <- sole
        ("semantic alias " <> StrictText.unpack name)
        [ candidate
        | candidate <- Semantic.declarationDeltaAliases delta
        , Semantic.semanticAliasName candidate
            == Semantic.semanticName name
        ]
    fact <- sole
        ("semantic fact " <> StrictText.unpack name)
        [ candidate
        | candidate <- Semantic.declarationDeltaFacts delta
        , Semantic.semanticFactFingerprint candidate
            == Semantic.semanticAliasTarget alias
        ]
    assertEqual
        ("clean authority for " <> StrictText.unpack name)
        Authority.cleanAuthoritySafety
        (Authority.factAuthoritySafety
            (Semantic.semanticFactAuthority fact))

batchByAlias
    :: Declaration.PendingModulePrefix
    -> Text
    -> IO Declaration.CommittedDeclarationBatch
batchByAlias prefix name =
    sole
        ("declaration batch for " <> StrictText.unpack name)
        [ batch
        | batch <- Declaration.pendingModulePrefixBatches prefix
        , alias <- Semantic.declarationDeltaAliases
            (Declaration.committedBatchDelta batch)
        , Semantic.semanticAliasName alias
            == Semantic.semanticName name
        ]

assertFinalPreludeFoundationAlias
    :: FinalPrelude.FinalPreludeCandidate
    -> Text
    -> Foundation.FoundationAxiomTag
    -> Assertion
assertFinalPreludeFoundationAlias candidate name tag = do
    batch <- batchByAlias
        (FinalPrelude.finalPreludePrefix candidate)
        name
    fact <- sole
        ("foundation fact " <> StrictText.unpack name)
        (Semantic.declarationDeltaFacts
            (Declaration.committedBatchDelta batch))
    assertEqual
        ("foundation safety for " <> StrictText.unpack name)
        Authority.cleanAuthoritySafety
        (Authority.factAuthoritySafety
            (Semantic.semanticFactAuthority fact))
    validation <- sole
        ("foundation validation for " <> StrictText.unpack name)
        (Declaration.committedBatchProofValidations batch)
    assertEqual
        ("exact foundation authority for " <> StrictText.unpack name)
        (Authority.CheckedKernelConstruction
            (Authority.FoundationLeaf tag))
        (Authority.validationDirectAuthorization
            (Semantic.proofValidationRecordCertificate validation))

localDeltaByAlias
    :: Module.SealedTypedModule
    -> Text
    -> IO Semantic.DeclarationInterfaceDelta
localDeltaByAlias sealed name =
    sole
        ("declaration delta for " <> StrictText.unpack name)
        [ delta
        | delta <- localSemanticDeltas sealed
        , any
            ((== Semantic.semanticName name)
                . Semantic.semanticAliasName)
            (Semantic.declarationDeltaAliases delta)
        ]

localSemanticDeltas
    :: Module.SealedTypedModule
    -> [Semantic.DeclarationInterfaceDelta]
localSemanticDeltas =
    Semantic.semanticInterfaceDeclarations
        . Module.sealedTypedModuleSemantic

retainsExactOmittedProofLocation :: Assertion
retainsExactOmittedProofLocation = do
    foundation <- expectRight Foundation.checkedFoundation
    source <-
        expectRight
            (Prelude.reservedPreludeSourceInput
                (Text.encodeUtf8
                    (StrictText.unlines
                        [ "\\begin{proposition}\\label{omitted_location}"
                        , "    For all $x$ we have $x = x$."
                        , "\\end{proposition}"
                        , "\\begin{proof}"
                        , "    Omitted."
                        , "\\end{proof}"
                        ])))
    parsed <- expectRight =<< Prelude.parseReservedPreludeSource source
    let blocks =
            Parse.identifiedParsedModuleBlocks
                (Prelude.reservedParsedPreludeModule parsed)
    claim <- sole "omitted claim"
        [ block
        | block@Raw.BlockClaim{} <- blocks
        ]
    proof <- sole "omitted proof"
        [ sourceProof
        | Raw.BlockProof _location sourceProof _end <- blocks
        ]
    outcome <-
        Declaration.runModuleDriver
            foundation
            preludeModuleName
            []
            unusedResolver
            Declaration.FreshValidation do
                Declaration.runProspectiveLoweringDriver
                    (ExactProof.prepareExactProof claim (Just proof))
                    >>= either Declaration.failModuleDriver pure
    case outcome of
        Right (Declaration.DriverSucceeded
                prepared _semantic prefix _closure) -> do
            location <-
                maybe
                    (assertFailure "prepared omitted proof lost its location")
                    pure
                    (ExactProof.preparedExactProofFirstOmission prepared)
            assertEqual "omitted source line" 5 (locLine location)
            assertBool "preparation publishes no declaration"
                (null (Declaration.pendingModulePrefixBatches prefix))
        Right (Declaration.DriverFailed failure _prefix) ->
            assertFailure ("omitted preparation failed: " <> show failure)
        Right (Declaration.DriverSealFailed failure _prefix) ->
            assertFailure ("omitted preparation did not seal: " <> show failure)
        Left failure ->
            assertFailure ("omitted preparation did not open: " <> show failure)

coalescesSharedDirectSyntax :: Assertion
coalescesSharedDirectSyntax = do
    foundation <- expectRight Foundation.checkedFoundation
    session <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation
                unusedResolver
    root <- getCurrentDirectory
    mounts <-
        expectRight
            =<< prepareSourceMounts
                [ (sourceMountId "project", root)
                , (sourceMountId "library", root Posix.</> "library")
                , (sourceMountId "debug", root Posix.</> "debug")
                ]
    let bootstrapSyntax =
            Module.sealedTypedModuleSyntax
                (Module.bootstrapPreludeModule session)
        syntaxInputs _source = [bootstrapSyntax]
    request <-
        expectRight
            (searchedRoot "test/phase3/typed-shared-root.tex")
    (workspace, _measurements) <-
        expectRight
            =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs
                mounts
                request
                syntaxInputs
    case Parse.parsedWorkspaceModules workspace of
        [firstParsed, secondParsed, rootParsed] -> do
            first <- seal foundation session firstParsed []
            second <- seal foundation session secondParsed []
            assertEqual "distinct modules share one syntax interface"
                (Syntax.moduleSyntaxAssertedId
                    (Module.sealedTypedModuleSyntax first))
                (Syntax.moduleSyntaxAssertedId
                    (Module.sealedTypedModuleSyntax second))
            assertBool "semantic module owners remain distinct"
                (Module.sealedTypedModuleOwner first
                    /= Module.sealedTypedModuleOwner second)
            assertBool "semantic interfaces remain distinct"
                (Semantic.semanticInterfaceAssertedId
                    (Module.sealedTypedModuleSemantic first)
                    /= Semantic.semanticInterfaceAssertedId
                        (Module.sealedTypedModuleSemantic second))
            let rootSyntax = Parse.parsedModuleSyntaxInterface rootParsed
            assertEqual "root coalesces the shared direct syntax"
                [ Syntax.moduleSyntaxAssertedId bootstrapSyntax
                , Syntax.moduleSyntaxAssertedId
                    (Module.sealedTypedModuleSyntax first)
                ]
                (Syntax.moduleSyntaxDirectInputs rootSyntax)
            sealedRoot <-
                seal foundation session rootParsed [first, second]
            assertEqual "root retains both semantic imports"
                [ Semantic.semanticInterfaceAssertedId
                    (Module.sealedTypedModuleSemantic
                        (Module.bootstrapPreludeModule session))
                , Semantic.semanticInterfaceAssertedId
                    (Module.sealedTypedModuleSemantic first)
                , Semantic.semanticInterfaceAssertedId
                    (Module.sealedTypedModuleSemantic second)
                ]
                (Semantic.semanticInterfaceDirectInputs
                    (Module.sealedTypedModuleSemantic sealedRoot))
        modules ->
            assertFailure
                ("unexpected shared-syntax module count: "
                    <> show (length modules))
  where
    seal foundation session parsed direct = do
        input <-
            expectRight
                (Module.typedModuleInput
                    foundation
                    (Module.bootstrapPreludeReadiness session)
                    unusedResolver
                    Declaration.FreshValidation
                    parsed
                    direct)
        Module.runTypedModule input >>= \case
            Module.TypedModuleSucceeded sealed ->
                pure sealed
            Module.TypedModuleOpenFailed{} ->
                assertFailure "empty typed module did not open"
                    >> fail "unreachable"
            Module.TypedModuleFailed{} ->
                assertFailure "empty typed module did not seal"
                    >> fail "unreachable"

rejectsUnsupportedTypedSource :: Assertion
rejectsUnsupportedTypedSource = do
    result <-
        runNoLoggingT
            (Api.verifyMeasured
                (Provers.vampire
                    "vampire"
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit)
                "test/phase3/typed-unsupported.tex")
    case result of
        Right
            ( Api.VerificationCheckingFailure _report
                (failure@(Api.VerificationTypedModuleError
                source
                (Module.TypedActionFailed
                    (Module.TypedExactCompileFailed
                        (Exact.ExactUnsupportedDeclarationBody location)))
                prefix))
            , _measurements
            ) -> do
            assertEqual "failed source"
                "test/phase3/typed-unsupported.tex"
                (safeRelativePathFilePath
                    (resolvedSourceRelativePath source))
            assertEqual "unsupported source location line"
                1
                (locLine location)
            assertEqual "failure retains the initial module prefix"
                0
                (length
                    (Declaration.pendingModulePrefixBatches prefix))
            let diagnostic =
                    CommandLine.verificationDriverFailureMessage failure
            assertBool "diagnostic retains resolved source"
                ("project:test/phase3/typed-unsupported.tex"
                    `StrictText.isInfixOf` diagnostic)
            assertBool "diagnostic retains best location"
                ("typed-unsupported.tex 1:1"
                    `StrictText.isInfixOf` diagnostic)
            assertBool "diagnostic explains the typed failure"
                ("not yet supported by exact elaboration"
                    `StrictText.isInfixOf` diagnostic)
        Left err ->
            assertFailure ("unexpected verification driver error: " <> show err)
        Right{} ->
            assertFailure "unsupported typed source was admitted"

compilesExactDeclarationGraph :: Assertion
compilesExactDeclarationGraph = do
    (_foundation, _bootstrap, workspace, sealedModules) <-
        compileExactFixture "test/phase5/exact-importer.tex"
    assertEqual "dependency-closed module count" 2 (length sealedModules)
    assertEqual "imported-before-importer source order"
        [ "test/phase5/exact-producer.tex"
        , "test/phase5/exact-importer.tex"
        ]
        [ safeRelativePathFilePath
            (resolvedSourceRelativePath
                (Parse.parsedModuleResolved parsed))
        | parsed <- toList
            (Parse.parsedWorkspaceImportedBeforeImporter workspace)
        ]
    case sealedModules of
        [producer, importer] -> do
            let producerPrefix = Module.sealedTypedModulePrefix producer
                importerPrefix = Module.sealedTypedModulePrefix importer
                producerBatches =
                    Declaration.pendingModulePrefixBatches producerPrefix
                importerBatches =
                    Declaration.pendingModulePrefixBatches importerPrefix
            assertEqual "producer declaration batches" 3
                (length producerBatches)
            assertEqual "importer declaration batches" 1
                (length importerBatches)
            assertEqual "producer declaration order"
                [0, 1, 2]
                [ localDeclarationOrdinalValue
                    (Semantic.declarationSlotOrdinal
                        (Declaration.committedBatchSlot batch))
                | batch <- producerBatches
                ]

            let producerDeltas =
                    Semantic.semanticInterfaceDeclarations
                        (Module.sealedTypedModuleSemantic producer)
                importerDeltas =
                    Semantic.semanticInterfaceDeclarations
                        (Module.sealedTypedModuleSemantic importer)
            assertEqual "one exact binding per producer declaration"
                [1, 1, 1]
                (bindingCount <$> producerDeltas)
            assertEqual "one exact importer binding"
                [1]
                (bindingCount <$> importerDeltas)
            assertEqual "producer object families"
                ["opaque", "transparent"]
                [ objectFamilyName
                    (Identity.assertedObjectContent object)
                | batch <- producerBatches
                , object <- Declaration.committedBatchObjects batch
                ]

            definitionDelta <- sole "producer definition delta"
                (drop 2 producerDeltas)
            definitionBinding <- sole "producer definition binding"
                (bindings definitionDelta)
            definitionFact <- sole "producer definition fact"
                (Semantic.declarationDeltaFacts definitionDelta)
            definitionAlias <- sole "producer definition alias"
                (Semantic.declarationDeltaAliases definitionDelta)
            assertEqual "definition alias"
                (Semantic.semanticName "phase5_definition")
                (Semantic.semanticAliasName definitionAlias)
            assertEqual "definition is proof-search eligible"
                Semantic.SearchEligible
                (Semantic.semanticFactSearchEligibility definitionFact)
            assertEqual "definition authority is clean"
                Authority.cleanAuthoritySafety
                (Authority.factAuthoritySafety
                    (Semantic.semanticFactAuthority definitionFact))
            definitionBatch <- sole "producer definition batch"
                (drop 2 producerBatches)
            validation <-
                maybe
                    (assertFailure "definition declaration validation is absent"
                        >> fail "unreachable")
                    pure
                    (Declaration.committedBatchDeclarationValidation
                        definitionBatch)
            certificate <- sole "definition validation certificate"
                (Semantic.declarationValidationRecordCertificates validation)
            assertEqual "direct defining-equation authority"
                (Authority.CheckedKernelConstruction
                    (Authority.CheckedDefinitionEquation
                        (Semantic.semanticGlobalTargetObject
                            (Semantic.semanticGlobalBindingTarget
                                definitionBinding))))
                (Authority.validationDirectAuthorization
                    certificate)

            aliasDelta <- sole "producer abbreviation delta"
                (take 1 (drop 1 producerDeltas))
            aliasBinding <- sole "producer abbreviation binding"
                (bindings aliasDelta)
            seedDelta <- sole "producer signature delta"
                (take 1 producerDeltas)
            seedBinding <- sole "producer signature binding"
                (bindings seedDelta)
            let seedTarget =
                    Semantic.semanticGlobalTargetObject
                        (Semantic.semanticGlobalBindingTarget seedBinding)
                aliasTarget =
                    Semantic.semanticGlobalTargetObject
                        (Semantic.semanticGlobalBindingTarget aliasBinding)
                definitionTarget =
                    Semantic.semanticGlobalTargetObject
                        (Semantic.semanticGlobalBindingTarget
                            definitionBinding)
            assertEqual "abbreviation expands transparently"
                (Semantic.TransparentExpansion
                    aliasTarget)
                (Semantic.semanticGlobalBindingTarget aliasBinding)
            assertEqual "definition remains a named global"
                (Semantic.GlobalReference definitionTarget)
                (Semantic.semanticGlobalBindingTarget definitionBinding)
            assertEqual "definition content coalesces with its expansion"
                aliasTarget
                definitionTarget
            assertEqual "coalesced definition adds no object"
                []
                (Declaration.committedBatchObjects definitionBatch)
            aliasBatch <- sole "producer abbreviation batch"
                (take 1 (drop 1 producerBatches))
            aliasObject <- sole "producer abbreviation object"
                (Declaration.committedBatchObjects aliasBatch)
            case Identity.assertedObjectContent aliasObject of
                Identity.TransparentObjectContent _theory _coreType body ->
                    assertEqual
                        "expanded body retains only the opaque seed"
                        (Set.singleton seedTarget)
                        (Core.canonicalTermGlobals body)
                content ->
                    assertFailure
                        ("abbreviation object is not transparent: "
                            <> show content)
            importerBatch <- sole "importer declaration batch" importerBatches
            importerDelta <- sole "importer semantic delta" importerDeltas
            importerBinding <- sole "importer binding"
                (bindings importerDelta)
            assertEqual "equal transparent content reuses the producer object"
                (Semantic.semanticGlobalBindingTarget definitionBinding)
                (Semantic.semanticGlobalBindingTarget importerBinding)
            assertEqual "reused transparent content adds no object"
                []
                (Declaration.committedBatchObjects importerBatch)
        modules ->
            assertFailure
                ("unexpected exact module count: " <> show (length modules))
  where
    bindingCount = length . bindings

    bindings =
        Semantic.semanticEnvironmentBindings
            . Semantic.declarationDeltaEnvironment

    objectFamilyName :: Identity.ObjectContent -> String
    objectFamilyName = \case
        Identity.OpaqueObjectContent{} -> "opaque"
        Identity.TransparentObjectContent{} -> "transparent"
        Identity.IntrinsicObjectContent{} -> "intrinsic"

compilesExactStructures :: Assertion
compilesExactStructures = do
    foundation <- expectRight Foundation.checkedFoundation
    repository <- getCurrentDirectory
    Temp.withSystemTempDirectory "felix-exact-structures" \directory -> do
        let path = directory Posix.</> "store.sqlite"
            executable = directory Posix.</> "vampire"
        writeAcceptedFixtureVampire executable
        runs <- newIORef (0 :: Int)
        let resolver = countingAcceptedResolver executable runs
        (_startup, store) <-
            Store.openStore path (Identity.theoryId foundation)
                >>= expectRight
        bracket (pure store) Store.closeStore \opened -> do
            prelude <-
                expectRight
                    =<< acquireFinalPreludeSession
                        opened foundation resolver
            carrierOperation <- sole "base carrier operation"
                [ operation
                | descriptor <- semanticStructureDescriptors
                    (Module.sealedTypedModuleSemantic
                        (Module.finalPreludeModule prelude))
                , operation <-
                    Semantic.semanticStructureDescriptorOperations descriptor
                ]
            mounts <- exactFixtureMounts repository
            workspace <- parseFinalExactWorkspace
                prelude mounts "test/phase5/exact-structure-child.tex"
            sealed <- compileFinalParsedWorkspaceWithResolver
                foundation prelude resolver workspace
            freshRuns <- readIORef runs
            warm <- installAndLoadStructures
                opened foundation prelude workspace sealed
            warmRuns <- readIORef runs
            assertEqual "warm structures preserve descriptors"
                (structureDescriptors <$> sealed)
                (structureDescriptors <$> warm)
            assertEqual "warm structures make no prover calls"
                freshRuns warmRuns
            case sealed of
                [parent, child] -> do
                    let parentBatches =
                            Declaration.pendingModulePrefixBatches
                                (Module.sealedTypedModulePrefix parent)
                        parentDeltas =
                            Semantic.semanticInterfaceDeclarations
                                (Module.sealedTypedModuleSemantic parent)
                        childBatches =
                            Declaration.pendingModulePrefixBatches
                                (Module.sealedTypedModulePrefix child)
                        childDeltas =
                            Semantic.semanticInterfaceDeclarations
                                (Module.sealedTypedModuleSemantic child)
                    parentBatch <- sole "parent structure batch"
                        (take 1 parentBatches)
                    parentDelta <- sole "parent structure delta"
                        (take 1 parentDeltas)
                    parentDescriptor <- sole "parent structure descriptor"
                        (Semantic.semanticEnvironmentStructures
                            (Semantic.declarationDeltaEnvironment parentDelta))
                    parentOperation <- sole "parent structure operation"
                        (Semantic.semanticStructureDescriptorOperations
                            parentDescriptor)
                    parentPredicate <-
                        maybe
                            (assertFailure "parent structure has no predicate"
                                >> fail "unreachable")
                            pure
                            (Semantic.semanticStructureDescriptorPredicate
                                parentDescriptor)
                    assertEqual "structure object family order"
                        ["opaque", "transparent"]
                        [ objectFamilyName
                            (Identity.assertedObjectContent object)
                        | object <- Declaration.committedBatchObjects parentBatch
                        ]
                    assertEqual "structure fact aliases"
                        [ Semantic.semanticName "pointed_set"
                        , Semantic.semanticName "pointed_refl"
                        ]
                        (Semantic.semanticAliasName
                            <$> Semantic.declarationDeltaAliases parentDelta)
                    definitionFact <- sole "structure definition fact"
                        (take 1 (Semantic.declarationDeltaFacts parentDelta))
                    definitionTarget <-
                        targetForOccurrence parentBatch definitionFact
                    assertEqual "pointwise structure definition"
                        (Core.CForall Core.TySet
                            (Core.CEq Core.TyProp
                                (Core.CApp
                                    (Core.CGlobal parentPredicate)
                                    (Core.CBound 0))
                                (Core.CEq Core.TySet
                                    (Core.CBound 0)
                                    (Core.CBound 0))))
                        definitionTarget
                    validations <-
                        maybe
                            (assertFailure "structure validation is absent"
                                >> fail "unreachable")
                            (pure
                                . Semantic.declarationValidationRecordCertificates)
                            (Declaration.committedBatchDeclarationValidation
                                parentBatch)
                    case validations of
                        definitionValidation : projectionValidation : [] -> do
                            assertEqual "structure definition authority"
                                (Authority.CheckedKernelConstruction
                                    (Authority.CheckedDefinitionEquation
                                        parentPredicate))
                                (Authority.validationDirectAuthorization
                                    definitionValidation)
                            projectionFact <- sole
                                "structure projection fact"
                                (drop 1
                                    (Semantic.declarationDeltaFacts
                                        parentDelta))
                            assertEqual
                                "projection has independent authority"
                                (Semantic.semanticFactAuthority projectionFact)
                                (Authority.validationTarget
                                    projectionValidation)
                            assertEqual "projection authority is clean"
                                Authority.cleanAuthoritySafety
                                (Authority.factAuthoritySafety
                                    (Authority.validationTarget
                                        projectionValidation))
                        records ->
                            assertFailure
                                ("expected two structure validations, got "
                                    <> show records)
                    assertBool "all parent structure facts are clean"
                        (all
                            ((== Authority.cleanAuthoritySafety)
                                . Authority.factAuthoritySafety
                                . Semantic.semanticFactAuthority)
                            (Semantic.declarationDeltaFacts parentDelta))

                    let claimGlobals marker = do
                            batch <- batchWithAlias marker parentBatches
                            occurrence <- sole (marker <> " occurrence")
                                (Semantic.declarationDeltaFacts
                                    (Declaration.committedBatchDelta batch))
                            Core.canonicalTermGlobals
                                <$> targetForOccurrence batch occurrence
                    carrierGlobals <- claimGlobals "pointed_carrier"
                    operationGlobals <- claimGlobals "pointed_operation"
                    assertBool "membership uses inherited carrier"
                        (Semantic.semanticStructureOperationObject carrierOperation
                            `Set.member` carrierGlobals)
                    assertBool "implicit and explicit operation share one object"
                        (Semantic.semanticStructureOperationObject parentOperation
                            `Set.member` operationGlobals)

                    childBatch <- sole "child structure batch" childBatches
                    childDelta <- sole "child structure delta" childDeltas
                    childDescriptor <- sole "child structure descriptor"
                        (Semantic.semanticEnvironmentStructures
                            (Semantic.declarationDeltaEnvironment childDelta))
                    assertEqual "child allocates no replacement operation"
                        []
                        (Semantic.semanticStructureDescriptorOperations
                            childDescriptor)
                    assertEqual "child owns only its transparent predicate"
                        ["transparent"]
                        [ objectFamilyName
                            (Identity.assertedObjectContent object)
                        | object <- Declaration.committedBatchObjects childBatch
                        ]
                modules ->
                    assertFailure
                        ("expected parent and child structures, got "
                            <> show (length modules))
  where
    installAndLoadStructures store foundation prelude workspace sealed = do
        memo <- Store.newStoreMemo store
        case
            ( toList
                (Parse.parsedWorkspaceImportedBeforeImporter workspace)
            , sealed
            ) of
            ([parentParsed, childParsed], [parent, child]) -> do
                cachedParent <- persistAndLoad memo [] parentParsed parent
                cachedChild <- persistAndLoad
                    memo [cachedParent] childParsed child
                pure [cachedParent, cachedChild]
            (parsed, modules) ->
                assertFailure
                    ("expected two structure installations, got "
                        <> show (length parsed)
                        <> " parsed and "
                        <> show (length modules)
                        <> " checked modules")
                    >> fail "unreachable"
      where
        preludeModule = Module.finalPreludeModule prelude

        persistAndLoad memo parents parsed sealedModule = do
            let input = Module.identifiedPhysicalModule parsed
                syntax = Module.sealedTypedModuleSyntax sealedModule
                semantic = Module.sealedTypedModuleSemantic sealedModule
            key <- expectRight
                (Semantic.moduleArtifactKey
                    (Module.identifiedModuleOwner input)
                    (Parse.identifiedParsedModuleId
                        (Module.identifiedModuleParsed input))
                    (Semantic.semanticInterfaceDirectInputs semantic)
                    (Identity.theoryId foundation))
            let artifact = Semantic.moduleArtifactResult
                    key
                    (Syntax.moduleSyntaxAssertedId syntax)
                    (Semantic.semanticInterfaceAssertedId semantic)
            acknowledged <- expectRight
                =<< Store.writeSealedModule
                    store
                    (Module.sealedTypedModulePrefix sealedModule)
                    [syntax]
                    [semantic]
                    artifact
            assertEqual "cached structure artifact acknowledgement"
                artifact acknowledged
            loaded <- expectRight
                =<< Store.loadCachedModuleInstallation
                    memo
                    store
                    key
                    (Syntax.moduleSyntaxAssertedId
                        (Parse.parsedModuleSyntaxInterface parsed))
            installation <- maybe
                (assertFailure "cached structure installation is absent"
                    >> fail "unreachable")
                pure
                loaded
            expectRight
                (Module.cachedSealedTypedModule
                    foundation
                    (preludeModule : parents)
                    installation)

    structureDescriptors =
        semanticStructureDescriptors
            . Module.sealedTypedModuleSemantic

    objectFamilyName :: Identity.ObjectContent -> String
    objectFamilyName = \case
        Identity.OpaqueObjectContent{} -> "opaque"
        Identity.TransparentObjectContent{} -> "transparent"
        Identity.IntrinsicObjectContent{} -> "intrinsic"

    targetForOccurrence batch occurrence =
        maybe
            (assertFailure "structure proposition is absent"
                >> fail "unreachable")
            (pure . Core.frozenCoreTerm . Identity.checkedPropositionTerm)
            (find
                ((== Semantic.semanticFactProposition occurrence)
                    . Identity.checkedPropositionId)
                (Declaration.committedBatchPropositions batch))

    batchWithAlias marker batches =
        maybe
            (assertFailure ("missing batch alias " <> marker)
                >> fail "unreachable")
            pure
            (find
                (elem (Semantic.semanticName (StrictText.pack marker))
                    . fmap Semantic.semanticAliasName
                    . Semantic.declarationDeltaAliases
                    . Declaration.committedBatchDelta)
                batches)

compilesContextualAbbreviations :: Assertion
compilesContextualAbbreviations = do
    foundation <- expectRight Foundation.checkedFoundation
    repository <- getCurrentDirectory
    Temp.withSystemTempDirectory "felix-contextual-abbreviation" \directory -> do
        let storePath = directory Posix.</> "store.sqlite"
            executable = directory Posix.</> "vampire"
            relative = "test/phase5/exact-contextual-abbreviation.tex"
        writeAcceptedFixtureVampire executable
        runs <- newIORef (0 :: Int)
        let resolver = countingAcceptedResolver executable runs
        (_startup, store) <-
            Store.openStore storePath (Identity.theoryId foundation)
                >>= expectRight
        bracket (pure store) Store.closeStore \opened -> do
            prelude <-
                expectRight
                    =<< acquireFinalPreludeSession
                        opened foundation resolver
            mounts <- exactFixtureMounts repository
            workspace <- parseFinalExactWorkspace prelude mounts relative
            sealed <- sole "contextual abbreviation module"
                =<< compileFinalParsedWorkspaceWithResolver
                    foundation prelude resolver workspace
            let deltas =
                    Semantic.semanticInterfaceDeclarations
                        (Module.sealedTypedModuleSemantic sealed)
                contextualTargets =
                    [ (identity, requirements)
                    | delta <- deltas
                    , binding <- Semantic.semanticEnvironmentBindings
                        (Semantic.declarationDeltaEnvironment delta)
                    , Semantic.ContextualTransparentExpansion
                            identity requirements <-
                        [Semantic.semanticGlobalBindingTarget binding]
                    ]
            assertEqual "contextual target count" 2
                (length contextualTargets)
            requirements <-
                sole "canonical contextual requirement set"
                    (nubOrd (snd <$> contextualTargets))
            assertEqual "one structure operation requirement" 1
                (Map.size requirements)
            let batches =
                    Declaration.pendingModulePrefixBatches
                        (Module.sealedTypedModulePrefix sealed)
            traverse_
                (assertReflexiveFact batches)
                [ "phase5_context_dot_explicit"
                , "phase5_context_inherited"
                , "phase5_context_nested"
                , "phase5_context_explicit_unique"
                ]

            parsed <- pure (Parse.parsedWorkspaceRootModule workspace)
            let syntax = Module.sealedTypedModuleSyntax sealed
                semantic = Module.sealedTypedModuleSemantic sealed
            key <- expectRight
                (Semantic.moduleArtifactKey
                    (moduleName (Parse.parsedModuleAddress parsed))
                    (Parse.parsedModuleId parsed)
                    (Semantic.semanticInterfaceDirectInputs semantic)
                    (Identity.theoryId foundation))
            let artifact =
                    Semantic.moduleArtifactResult
                        key
                        (Syntax.moduleSyntaxAssertedId syntax)
                        (Semantic.semanticInterfaceAssertedId semantic)
            void
                (expectRight
                    =<< Store.writeSealedModule
                        opened
                        (Module.sealedTypedModulePrefix sealed)
                        [syntax]
                        [semantic]
                        artifact)
            memo <- Store.newStoreMemo opened
            loaded <- expectRight
                =<< Store.loadCachedModuleInstallation
                    memo opened key
                    (Syntax.moduleSyntaxAssertedId
                        (Parse.parsedModuleSyntaxInterface parsed))
            installation <- maybe
                (assertFailure "contextual cached installation is absent"
                    >> fail "unreachable")
                pure
                loaded
            cached <- expectRight
                (Module.cachedSealedTypedModule
                    foundation
                    [Module.finalPreludeModule prelude]
                    installation)
            assertEqual "cached contextual semantic target"
                semantic
                (Module.sealedTypedModuleSemantic cached)

            runsBeforeConsumer <- readIORef runs
            consumerWorkspace <-
                parseFinalExactWorkspace prelude mounts
                    "test/phase5/exact-contextual-abbreviation-consumer.tex"
            let consumerParsed =
                    Parse.parsedWorkspaceRootModule consumerWorkspace
            consumerInput <- expectRight
                (Module.typedModuleInput
                    foundation
                    (Module.finalPreludeReadiness prelude)
                    resolver
                    Declaration.FreshValidation
                    consumerParsed
                    [cached])
            consumer <- Module.runTypedModule consumerInput >>= \case
                Module.TypedModuleSucceeded sealedConsumer ->
                    pure sealedConsumer
                Module.TypedModuleOpenFailed failure ->
                    assertFailure
                        ("contextual consumer did not open: " <> show failure)
                        >> fail "unreachable"
                Module.TypedModuleFailed failure _prefix ->
                    assertFailure
                        ("contextual consumer did not seal: " <> show failure)
                        >> fail "unreachable"
            let consumerTargets =
                    [ Semantic.semanticGlobalTargetObject
                        (Semantic.semanticGlobalBindingTarget binding)
                    | delta <- localSemanticDeltas consumer
                    , binding <- Semantic.semanticEnvironmentBindings
                        (Semantic.declarationDeltaEnvironment delta)
                    ]
            assertEqual "two contextual consumer declarations" 2
                (length consumerTargets)
            void
                (sole
                    "quantified contextual binder matches its explicit parameter"
                    (nubOrd consumerTargets))
            runsAfterConsumer <- readIORef runs
            assertEqual "contextual abbreviations require no prover call"
                runsBeforeConsumer runsAfterConsumer

            verifyFailure foundation resolver prelude mounts sealed
                "test/phase5/exact-contextual-abbreviation-missing.tex"
                (\case
                    Exact.ExactContextualExpansionNotAvailable location _key ->
                        assertEqual "missing context line" 5 (locLine location)
                    failure ->
                        assertFailure
                            ("unexpected missing-context failure: "
                                <> show failure))
            verifyFailure foundation resolver prelude mounts sealed
                "test/phase5/exact-contextual-abbreviation-ambiguous.tex"
                (\case
                    Exact.ExactStructureOperationAmbiguous
                            location _symbol objects -> do
                        assertEqual "ambiguous operation line" 16
                            (locLine location)
                        assertEqual "two distinct operation objects" 2
                            (length objects)
                    failure ->
                        assertFailure
                            ("unexpected operation ambiguity failure: "
                                <> show failure))
  where
    assertReflexiveFact batches marker = do
        batch <- maybe
            (assertFailure ("missing contextual fact " <> marker)
                >> fail "unreachable")
            pure
            (find
                (elem (Semantic.semanticName (StrictText.pack marker))
                    . fmap Semantic.semanticAliasName
                    . Semantic.declarationDeltaAliases
                    . Declaration.committedBatchDelta)
                batches)
        proposition <- sole (marker <> " proposition")
            (Declaration.committedBatchPropositions batch)
        let body = stripClaimEnvelope
                (Core.frozenCoreTerm
                    (Identity.checkedPropositionTerm proposition))
        case body of
            Core.CEq _ left right ->
                assertEqual (marker <> " canonical sides") left right
            _ ->
                assertFailure
                    (marker <> " did not elaborate to reflexive equality: "
                        <> show body)

    stripClaimEnvelope = \case
        Core.CForall _ body -> stripClaimEnvelope body
        Core.CImp _ body -> stripClaimEnvelope body
        term -> term

    verifyFailure foundation resolver prelude mounts imported relative checkFailure = do
        workspace <- parseFinalExactWorkspace prelude mounts relative
        let parsed = Parse.parsedWorkspaceRootModule workspace
        input <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.finalPreludeReadiness prelude)
                resolver
                Declaration.FreshValidation
                parsed
                [imported])
        Module.runTypedModule input >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactCompileFailed failure))
                    _prefix ->
                checkFailure failure
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactProofFailed
                            (ExactProof.ExactProofElaborationFailed failure)))
                    _prefix ->
                checkFailure failure
            Module.TypedModuleSucceeded{} ->
                assertFailure (relative <> " was unexpectedly accepted")
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    (relative <> " did not open: " <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    (relative <> " failed unexpectedly: " <> show failure)

rejectsUnknownExactStructureParent :: Assertion
rejectsUnknownExactStructureParent =
    Temp.withSystemTempDirectory "felix-exact-structure-parent" \root -> do
        let relative = "entry.tex"
            path = root Posix.</> relative
            source =
                "\\begin{struct}\\label{known_structure}\n"
                    <> "    A known structure $X$ is a onesorted structure.\n"
                    <> "\\end{struct}\n\n"
                    <> "\\begin{struct}\\label{invalid_structure}\n"
                    <> "    An invalid structure $X$ is a future structure.\n"
                    <> "\\end{struct}\n\n"
                    <> "\\begin{struct}\\label{future_structure}\n"
                    <> "    A future structure $X$ is a onesorted structure.\n"
                    <> "\\end{struct}\n"
        ByteString.writeFile path
            (Text.encodeUtf8 (StrictText.pack source))
        foundation <- expectRight Foundation.checkedFoundation
        Temp.withSystemTempDirectory "felix-exact-structure-store" \directory -> do
            let storePath = directory Posix.</> "store.sqlite"
                executable = directory Posix.</> "vampire"
            writeAcceptedFixtureVampire executable
            runs <- newIORef (0 :: Int)
            let resolver = countingAcceptedResolver executable runs
            (_startup, store) <-
                Store.openStore storePath (Identity.theoryId foundation)
                    >>= expectRight
            bracket (pure store) Store.closeStore \opened -> do
                prelude <-
                    expectRight
                        =<< acquireFinalPreludeSession
                            opened foundation resolver
                mounts <- exactFixtureMounts root
                workspace <- parseFinalExactWorkspace prelude mounts relative
                let parsed = Parse.parsedWorkspaceRootModule workspace
                input <- expectRight
                    (Module.typedModuleInput
                        foundation
                        (Module.finalPreludeReadiness prelude)
                        resolver
                        Declaration.FreshValidation
                        parsed
                        [])
                Module.runTypedModule input >>= \case
                    Module.TypedModuleFailed
                            (Module.TypedActionFailed
                                (Module.TypedExactCompileFailed
                                    (Exact.ExactStructureNotVisible
                                        location _phrase)))
                            prefix -> do
                        assertEqual "unknown parent line" 5 (locLine location)
                        assertEqual "only the valid structure was published"
                            1
                            (length
                                (Declaration.pendingModulePrefixBatches prefix))
                    Module.TypedModuleSucceeded{} ->
                        assertFailure "unknown structure parent was accepted"
                    Module.TypedModuleOpenFailed failure ->
                        assertFailure
                            ("invalid structure module did not open: "
                                <> show failure)
                    Module.TypedModuleFailed failure _prefix ->
                        assertFailure
                            ("unexpected invalid structure failure: "
                                <> show failure)

compilesExactRelationExpressions :: Assertion
compilesExactRelationExpressions = do
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation unusedResolver
    repository <- getCurrentDirectory
    mounts <- exactFixtureMounts repository
    workspace <- parseExactWorkspace
        bootstrap mounts "test/phase5/exact-relation-expression.tex"
    observed <- newIORef []
    withAcceptedFixtureVampire "felix-exact-relation-expression" \prover -> do
        let resolver = Declaration.vampireResolver \prepared -> do
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                    claim = Backend.typedProblemClaim problem
                    locals = Backend.typedProblemLocalPremises problem
                modifyIORef' observed
                    (<> [ [ Backend.supportedPropositionTerm
                                (Backend.typedLocalPremiseProposition premise)
                            == Backend.supportedPropositionTerm claim
                           | premise <- Vector.toList locals
                           ]
                        ])
                runNoLoggingT
                    (Provers.runPreparedTypedProver prover prepared)
        void
            (compileParsedWorkspaceWithResolver
                foundation bootstrap resolver workspace)
    assertEqual
        "relation expression is ordered-pair membership"
        [[True]]
        =<< readIORef observed

    missingPair <-
        withAcceptedFixtureVampire "felix-exact-relation-expression-missing-pair" \prover ->
            runNoLoggingT
                (Api.verifyMeasured
                    prover
                    "test/phase5/exact-relation-expression-missing-pair.tex")
    case missingPair of
        Right
            ( Api.VerificationCheckingFailure _report
                (Api.VerificationTypedModuleError
                _source
                (Module.TypedActionFailed
                    (Module.TypedExactProofFailed
                        (ExactProof.ExactProofElaborationFailed
                            (Exact.ExactGlobalNotVisible location key))))
                prefix)
            , _measurements
            ) -> do
            assertEqual "missing ordered-pair provider line"
                2
                (locLine location)
            assertEqual "missing ordered-pair semantic key"
                (Semantic.SemanticExpressionFunction
                    (Raw.mixfixPattern Raw.PairSymbol))
                key
            assertEqual "missing provider publishes no declaration"
                0
                (length (Declaration.pendingModulePrefixBatches prefix))
        Left err ->
            assertFailure
                ("unexpected relation-expression failure: " <> show err)
        Right{} ->
            assertFailure "relation expression without ordered pairing was admitted"

resolvesSourceOwnedApplication :: Assertion
resolvesSourceOwnedApplication = do
    foundation <- expectRight Foundation.checkedFoundation
    repository <- getCurrentDirectory
    withAcceptedFixtureVampire "felix-exact-application" \prover ->
        Temp.withSystemTempDirectory "felix-exact-application" \directory -> do
            let storePath = directory Posix.</> "store.sqlite"
                resolver = Declaration.vampireResolver
                    (runNoLoggingT . Provers.runPreparedTypedProver prover)
            bracket
                (snd <$> (Store.openStore storePath
                    (Identity.theoryId foundation) >>= expectRight))
                Store.closeStore
                \store -> do
                    prelude <-
                        expectRight
                            =<< acquireFinalPreludeSession
                                store foundation resolver
                    mounts <- exactFixtureMounts repository
                    workspace <- parseFinalExactWorkspace
                        prelude mounts "test/phase5/exact-application.tex"
                    sealed <- compileFinalParsedWorkspaceWithResolver
                        foundation prelude resolver workspace
                    root <- case reverse sealed of
                        rootModule : _ -> pure rootModule
                        [] ->
                            assertFailure "application fixture root is absent"
                                >> fail "unreachable"
                    assertTransparentObjectAlias root "phase5_apply"
                    let applyKey = Semantic.SemanticExpressionFunction
                            (Raw.mixfixPattern Raw.ApplySymbol)
                    applyObject <- localObjectKeyTarget root applyKey
                    surface <- checkedPropositionTermByAlias
                        root "phase5_application_surface"
                    explicit <- checkedPropositionTermByAlias
                        root "phase5_application_explicit"
                    assertEqual
                        "surface and explicit application lower identically"
                        explicit
                        surface
                    assertBool
                        "surface application resolves through the declared object"
                        (applyObject `Set.member` Core.frozenCoreGlobals surface)

    missing <-
        withAcceptedFixtureVampire "felix-exact-application-missing"
            \prover ->
                runNoLoggingT
                    (Api.verifyMeasured
                        prover
                        "test/phase5/exact-application-missing.tex")
    case missing of
        Right
            ( Api.VerificationCheckingFailure _report
                (Api.VerificationTypedModuleError
                _source
                (Module.TypedActionFailed
                    (Module.TypedExactProofFailed
                        (ExactProof.ExactProofElaborationFailed
                            (Exact.ExactGlobalNotVisible location key))))
                prefix)
            , _measurements
            ) -> do
            assertEqual "unresolved application line" 2 (locLine location)
            assertEqual "unresolved application key"
                (Semantic.SemanticExpressionFunction
                    (Raw.mixfixPattern Raw.ApplySymbol))
                key
            assertEqual "unresolved application publishes no declaration"
                0
                (length (Declaration.pendingModulePrefixBatches prefix))
        Left failure ->
            assertFailure
                ("unexpected unresolved application failure: " <> show failure)
        Right{} ->
            assertFailure "application without its source binding was admitted"

confinesExactQuantifiedTerms :: Assertion
confinesExactQuantifiedTerms = do
    foundation <- expectRight Foundation.checkedFoundation
    repository <- getCurrentDirectory
    withAcceptedFixtureVampire "felix-exact-quantified-subject" \prover ->
        Temp.withSystemTempDirectory "felix-quantified-subject" \directory -> do
            let storePath = directory Posix.</> "store.sqlite"
                resolver = Declaration.vampireResolver
                    (runNoLoggingT . Provers.runPreparedTypedProver prover)
            bracket
                (snd <$> (Store.openStore storePath
                    (Identity.theoryId foundation) >>= expectRight))
                Store.closeStore
                \store -> do
                    prelude <-
                        expectRight
                            =<< acquireFinalPreludeSession
                                store foundation resolver
                    mounts <- exactFixtureMounts repository
                    workspace <- parseFinalExactWorkspace
                        prelude mounts
                        "test/phase5/exact-quantified-subject.tex"
                    sealed <- compileFinalParsedWorkspaceWithResolver
                        foundation prelude resolver workspace
                    root <- case reverse sealed of
                        rootModule : _ -> pure rootModule
                        [] ->
                            assertFailure "quantified-subject root is absent"
                                >> fail "unreachable"
                    quantified <- checkedPropositionTermByAlias root
                        "phase5_quantified_subject"
                    explicit <- checkedPropositionTermByAlias root
                        "phase5_explicit_quantifier"
                    assertEqual
                        "quantified noun subject retains its domain constraint"
                        explicit
                        quantified

    negative <-
        withAcceptedFixtureVampire "felix-exact-quantified-subject-nested"
            \prover ->
                runNoLoggingT
                    (Api.verifyMeasured
                        prover
                        "test/phase5/exact-quantified-subject-nested.tex")
    case negative of
        Right
            ( Api.VerificationCheckingFailure _report
                (Api.VerificationTypedModuleError
                _source
                (Module.TypedActionFailed
                    (Module.TypedExactProofFailed
                        (ExactProof.ExactProofElaborationFailed
                            (Exact.ExactQuantifiedTermRequiresStatementSubject
                                location))))
                prefix)
            , _measurements
            ) -> do
            assertEqual "nested quantified term line" 8 (locLine location)
            assertEqual "earlier exact definition remains committed"
                1
                (length (Declaration.pendingModulePrefixBatches prefix))
        Left failure ->
            assertFailure
                ("unexpected nested quantified-term failure: "
                    <> show failure)
        Right{} ->
            assertFailure "nested quantified exact term was admitted"
compilesExactOrdinaryProofs :: Assertion
compilesExactOrdinaryProofs =
    Temp.withSystemTempDirectory "felix-exact-proofs" \root -> do
        repository <- getCurrentDirectory
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation
                    unusedResolver
        mounts <- exactFixtureMounts repository
        workspace <- parseExactWorkspace
            bootstrap mounts "test/phase5/exact-proofs.tex"
        let executable = root Posix.</> "vampire"
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-proof'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        observations <- newIORef []
        let resolver = Declaration.vampireResolver \prepared -> do
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                    claim =
                        Backend.typedProblemClaim problem
                    locals =
                        Backend.typedProblemLocalPremises problem
                modifyIORef' observations
                    (<> [ ( Vector.length
                                (Backend.typedProblemGlobalPremises problem)
                           , Vector.length
                                locals
                           , [ Vector.length
                                (Backend.supportedPropositionSupport
                                    (Backend.typedLocalPremiseProposition premise))
                             | premise <- Vector.toList locals
                             ]
                           , [ Backend.supportedPropositionTerm
                                    (Backend.typedLocalPremiseProposition premise)
                                == Backend.supportedPropositionTerm claim
                             | premise <- Vector.toList locals
                             ]
                           )
                        ])
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        sealed <-
            compileParsedWorkspaceWithResolver
                foundation bootstrap resolver workspace
        rootModule <- sole "exact proof root" (drop 1 sealed)
        let batches =
                Declaration.pendingModulePrefixBatches
                    (Module.sealedTypedModulePrefix rootModule)
        assertEqual "one definition and five theorem declarations"
            6
            (length batches)
        let proofBatches = drop 1 batches
        assertEqual "only closed theorem facts are published"
            [1, 1, 1, 1, 1]
            [ length
                (Semantic.declarationDeltaFacts
                    (Declaration.committedBatchDelta batch))
            | batch <- proofBatches
            ]
        assertEqual "proof request aggregation follows source structure"
            [1, 2, 2, 1, 1]
            [ case Declaration.committedBatchProofValidations batch of
                [record] ->
                    case Authority.validationDirectAuthorization
                            (Semantic.proofValidationRecordCertificate
                                record) of
                        Authority.CheckedSourceProof requests ->
                            length requests
                        authorization ->
                            error
                                ("unexpected exact proof authority: "
                                    <> show authorization)
                records ->
                    error
                        ("unexpected exact proof validation count: "
                            <> show (length records))
            | batch <- proofBatches
            ]
        headerBatch <- sole "header-envelope proof batch"
            (take 1 (drop 3 proofBatches))
        headerProposition <- sole "header-envelope checked proposition"
            (Declaration.committedBatchPropositions headerBatch)
        assertEqual "header-envelope closed target"
            (Core.CForall Core.TySet
                (Core.CForall Core.TySet
                    (Core.CImp
                        (member
                            (Core.CBound 0)
                            (Core.CBound 1))
                        (member
                            (Core.CBound 0)
                            (Core.CBound 1)))))
            (Core.frozenCoreTerm
                (Identity.checkedPropositionTerm headerProposition))
        headerFact <- sole "header-envelope published fact"
            (Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta headerBatch))
        assertEqual "header-envelope proof remains clean"
            Authority.cleanAuthoritySafety
            (Authority.factAuthoritySafety
                (Semantic.semanticFactAuthority headerFact))
        observed <- readIORef observations
        case observed of
            (implicitGlobals, 0, [], [])
                : [ (0, 1, [1], _structuralMatches)
                  , (1, 2, [1, 1], _subclaimMatches)
                  , (0, 0, [], [])
                  , (0, 1, [1], _followingMatches)
                  , (0, 1, [2], [True])
                  , (generalizedGlobals, 0, [], [])
                  ] -> do
                    assertBool "implicit Auto selects visible FOF facts"
                        (implicitGlobals > 0)
                    assertBool "generalized Auto selects visible FOF facts"
                        (generalizedGlobals > 0)
            _ ->
                assertFailure
                    ("unexpected exact proof premise policies: "
                        <> show observed)
  where
    member element set =
        Core.CApp
            (Core.CApp
                (Core.CIntrinsic Core.Member)
                element)
            set

compilesExactSeparationComprehensions :: Assertion
compilesExactSeparationComprehensions =
    Temp.withSystemTempDirectory "felix-exact-separation" \root -> do
        let relative = "test/phase5/exact-separation.tex"
            executable = root Posix.</> "vampire"
            failedSource = root Posix.</> relative
        repository <- getCurrentDirectory
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation
                    unusedResolver
        mounts <- exactFixtureMounts repository
        workspace <- parseExactWorkspace bootstrap mounts relative
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-separation'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        observations <- newIORef []
        let resolver = Declaration.vampireResolver \prepared -> do
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                modifyIORef' observations
                    (<> [ ( Backend.typedProblemRoute problem
                           , Backend.typedProblemAuxiliaryTag
                                <$> Vector.toList
                                    (Backend.typedProblemAuxiliaries problem)
                           )
                        ])
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        modules <- compileParsedWorkspaceWithResolver
            foundation bootstrap resolver workspace
        sealed <- sole "exact separation module" modules
        assertExactSeparationModule "fresh" sealed
        assertEqual
            "separation proof uses its checked characteristic on TH0"
            [( Backend.RouteTh0
             , [Foundation.SeparationCharacteristic]
             )]
            =<< readIORef observations

        createDirectoryIfMissing True (Posix.takeDirectory failedSource)
        original <- ByteString.readFile relative
        let invalid =
                Text.encodeUtf8
                    (StrictText.replace
                        "x \\in A \\mid x = x"
                        "x \\in x \\mid x = x"
                        (Text.decodeUtf8 original))
        ByteString.writeFile failedSource invalid
        failedMounts <- exactFixtureMounts root
        failedWorkspace <-
            parseExactWorkspace bootstrap failedMounts relative
        let parsed = Parse.parsedWorkspaceRootModule failedWorkspace
        input <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                unusedResolver
                Declaration.FreshValidation
                parsed
                [])
        Module.runTypedModule input >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactCompileFailed
                            (Exact.ExactFreeVariable location
                                (Raw.NamedVar "x"))))
                    prefix -> do
                assertEqual "invalid separation bound line"
                    2 (locLine location)
                assertEqual
                    "invalid separation publishes none of its declaration"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Module.TypedModuleSucceeded{} ->
                assertFailure "invalid separation was accepted"
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    ("invalid separation module did not open: "
                        <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    ("unexpected invalid separation failure: "
                        <> show failure)

compilesAndReusesProofLocalSetDefinitions :: Assertion
compilesAndReusesProofLocalSetDefinitions =
    Temp.withSystemTempDirectory "felix-exact-local-definition" \root -> do
        let relative = "test/phase5/exact-local-definition.tex"
            failedRelative =
                "test/phase5/exact-local-definition-failure.tex"
            sourcePath = root Posix.</> relative
            failedSourcePath = root Posix.</> failedRelative
            executable = root Posix.</> "vampire"
            storePath = root Posix.</> "store.sqlite"
        createDirectoryIfMissing True (Posix.takeDirectory sourcePath)
        ByteString.readFile relative >>= ByteString.writeFile sourcePath
        createDirectoryIfMissing True (Posix.takeDirectory failedSourcePath)
        ByteString.readFile failedRelative
            >>= ByteString.writeFile failedSourcePath
        writeAcceptedFixtureVampire executable
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation
                    unusedResolver
        mounts <- exactFixtureMounts root
        workspace <- parseExactWorkspace bootstrap mounts relative
        freshRuns <- newIORef (0 :: Int)
        observations <- newIORef []
        let freshResolver = Declaration.vampireResolver \prepared -> do
                modifyIORef' freshRuns (+ 1)
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                    premises =
                        Backend.typedProblemLocalPremises problem
                    definition =
                        Vector.find
                            ((== Backend.localPremiseOrdinal 0)
                                . Backend.typedLocalPremiseOrdinal)
                            premises
                modifyIORef' observations
                    (<> [ ( Backend.typedProblemRoute problem
                           , Vector.length premises
                           , fmap localDefinitionShape definition
                           )
                        ])
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        freshModules <-
            compileParsedWorkspaceWithValidation
                foundation
                bootstrap
                freshResolver
                Declaration.FreshValidation
                workspace
        assertEqual "fresh local-definition discharge count"
            2 =<< readIORef freshRuns
        assertEqual "local definitions remain on the FOF route"
            [ (Backend.RouteFof, 2, Just expectedLocalDefinitionShape)
            , (Backend.RouteFof, 2, Just expectedLocalDefinitionShape)
            ]
            =<< readIORef observations
        fresh <- sole "fresh local-definition module" freshModules
        localDefinitionBatch <- sole
            "proof-local definition publishes one declaration"
            (Declaration.pendingModulePrefixBatches
                (Module.sealedTypedModulePrefix fresh))
        assertEqual "proof-local definition publishes no object"
            []
            (Declaration.committedBatchObjects localDefinitionBatch)
        assertEqual "proof-local definition publishes only its theorem"
            1
            (length
                (Declaration.committedBatchPropositions
                    localDefinitionBatch))
        localDefinitionFact <- sole
            "proof-local definition theorem"
            (Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta
                    localDefinitionBatch))
        assertEqual "proof-local definition remains clean"
            Authority.cleanAuthoritySafety
            (Authority.factAuthoritySafety
                (Semantic.semanticFactAuthority localDefinitionFact))

        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                expectRightIO
                    (Store.writePendingModulePrefix store
                        (Module.sealedTypedModulePrefix fresh))
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmRuns <- newIORef (0 :: Int)
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation
                        bootstrap
                        (countingAcceptedResolver executable warmRuns)
                        validation
                        workspace
                assertEqual "warm local-definition proof skips Vampire"
                    0 =<< readIORef warmRuns
                warm <- sole "warm local-definition module" warmModules
                assertEqual "warm local-definition semantic interface"
                    (Module.sealedTypedModuleSemantic fresh)
                    (Module.sealedTypedModuleSemantic warm)
                assertEqual "warm local-definition prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix fresh))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warm))

        failedWorkspace <-
            parseExactWorkspace bootstrap mounts failedRelative
        let failedParsed =
                Parse.parsedWorkspaceRootModule failedWorkspace
        failedInput <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                unusedResolver
                Declaration.FreshValidation
                failedParsed
                [])
        Module.runTypedModule failedInput >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactProofFailed
                            (ExactProof.ExactProofElaborationFailed
                                (Exact.ExactFreeVariable location
                                    (Raw.NamedVar "B")))))
                    prefix -> do
                assertEqual "self-reference rejection line"
                    6 (locLine location)
                assertBool "failed local definition publishes no theorem"
                    (null
                        (Declaration.pendingModulePrefixBatches prefix))
            Module.TypedModuleSucceeded{} ->
                assertFailure "self-referential local definition was accepted"
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    ("local-definition failure fixture did not open: "
                        <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    ("unexpected local-definition failure: "
                        <> show failure)
  where
    localDefinitionShape premise =
        let proposition =
                Backend.typedLocalPremiseProposition premise
        in ( fmap
                snd
                (Vector.toList
                    (Backend.supportedPropositionSupport proposition))
           , Backend.supportedPropositionTerm proposition
           )

    expectedLocalDefinitionShape =
        ( [Core.TySet, Core.TySet]
        , Core.CForall Core.TySet
            (Core.CEq Core.TyProp
                (member (Core.CBound 0) (Core.CBound 1))
                (andP
                    (member (Core.CBound 0) (Core.CBound 2))
                    (Core.CEq Core.TySet
                        (Core.CBound 0)
                        (Core.CBound 0))))
        )

    member element set =
        Core.CApp
            (Core.CApp
                (Core.CIntrinsic Core.Member)
                element)
            set

    andP left right =
        Core.CImp
            (Core.CImp left (Core.CImp right Core.CFalsum))
            Core.CFalsum

compilesAndReusesProofLocalFunctionGraphs :: Assertion
compilesAndReusesProofLocalFunctionGraphs =
    Temp.withSystemTempDirectory "felix-exact-local-function" \root -> do
        let relative = "test/phase5/exact-local-function.tex"
            failedRelative =
                "test/phase5/exact-local-function-failure.tex"
            executable = root Posix.</> "vampire"
            storePath = root Posix.</> "store.sqlite"
        writeAcceptedFixtureVampire executable
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation unusedResolver
        mounts <- exactFixtureMounts =<< getCurrentDirectory
        workspace <- parseExactWorkspace bootstrap mounts relative
        observations <- newIORef []
        let resolver = Declaration.vampireResolver \prepared -> do
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                    premises =
                        [ ( Backend.typedProblemRoute problem
                          , fmap snd
                                (Vector.toList
                                    (Backend.supportedPropositionSupport
                                        proposition))
                          , Backend.supportedPropositionTerm proposition
                          )
                        | premise <-
                            Vector.toList
                                (Backend.typedProblemLocalPremises problem)
                        , let proposition =
                                Backend.typedLocalPremiseProposition premise
                        ]
                modifyIORef' observations (<> premises)
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        freshModules <-
            compileParsedWorkspaceWithValidation
                foundation bootstrap resolver
                Declaration.FreshValidation workspace
        allObserved <- readIORef observations
        let observed =
                [ (route, proposition)
                | (route, support, proposition) <- allObserved
                , support == [Core.TySet, Core.TySet]
                , isJust (localFunctionPair proposition)
                ]
        assertBool
            ("the local graph characteristic reaches a discharge: "
                <> show allObserved)
            (not (null observed))
        for_ observed \(route, proposition) -> do
            assertEqual "local function characteristic stays on FOF"
                Backend.RouteFof route
            assertExactLocalFunctionCharacteristic proposition
        freshRoot <- sole "fresh local-function root"
            (take 1 (reverse freshModules))
        rootBatch <- sole "local function publishes only its theorem"
            (drop 1
                (Declaration.pendingModulePrefixBatches
                    (Module.sealedTypedModulePrefix freshRoot)))
        assertEqual "local function publishes no object"
            [] (Declaration.committedBatchObjects rootBatch)
        assertEqual "local function publishes only its theorem"
            1
            (length
                (Declaration.committedBatchPropositions rootBatch))
        assertEqual "local function publishes no semantic binding"
            []
            (Semantic.semanticEnvironmentBindings
                (Semantic.declarationDeltaEnvironment
                    (Declaration.committedBatchDelta rootBatch)))
        rootFact <- sole "local-function theorem"
            (Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta rootBatch))
        assertEqual "local-function theorem remains clean"
            Authority.cleanAuthoritySafety
            (Authority.factAuthoritySafety
                (Semantic.semanticFactAuthority rootFact))

        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                traverse_
                    (expectRightIO
                        . Store.writePendingModulePrefix store
                        . Module.sealedTypedModulePrefix)
                    freshModules
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmRuns <- newIORef (0 :: Int)
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation bootstrap
                        (countingAcceptedResolver executable warmRuns)
                        validation workspace
                assertEqual "warm local-function graph skips Vampire"
                    0 =<< readIORef warmRuns
                warmRoot <- sole "warm local-function root"
                    (take 1 (reverse warmModules))
                assertEqual "warm local-function semantic interface"
                    (Module.sealedTypedModuleSemantic freshRoot)
                    (Module.sealedTypedModuleSemantic warmRoot)
                assertEqual "warm local-function prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix freshRoot))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warmRoot))

        failedWorkspace <-
            parseExactWorkspace bootstrap mounts failedRelative
        failedInput <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                unusedResolver
                Declaration.FreshValidation
                (Parse.parsedWorkspaceRootModule failedWorkspace)
                [])
        Module.runTypedModule failedInput >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactProofFailed
                            (ExactProof.ExactProofElaborationFailed
                                (Exact.ExactFreeVariable location
                                    (Raw.NamedVar "f")))))
                    prefix -> do
                assertEqual "self-reference rejection line"
                    6 (locLine location)
                assertBool "failed local function publishes no theorem"
                    (null
                        (Declaration.pendingModulePrefixBatches prefix))
            Module.TypedModuleSucceeded{} ->
                assertFailure "self-referential local function was accepted"
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    ("local-function failure fixture did not open: "
                        <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    ("unexpected local-function failure: "
                        <> show failure)
  where
    assertExactLocalFunctionCharacteristic proposition = do
        pair <-
            maybe
                (assertFailure "local function characteristic has wrong shape")
                pure
                (localFunctionPair proposition)
        assertEqual "local function uses the exact replacement characteristic"
            (expectedLocalFunctionCharacteristic pair)
            proposition

    localFunctionPair proposition =
        case Set.toList (Core.canonicalTermGlobals proposition) of
            [pair]
                | proposition == expectedLocalFunctionCharacteristic pair ->
                    Just pair
            _ ->
                Nothing

    expectedLocalFunctionCharacteristic pair =
        Core.CForall Core.TySet
            (Core.CEq Core.TyProp
                (member (Core.CBound 0) (Core.CBound 1))
                (existsP
                    (andP
                        (member (Core.CBound 0) (Core.CBound 3))
                        (Core.CEq Core.TySet
                            (Core.CBound 1)
                            (Core.CApp
                                (Core.CApp
                                    (Core.CGlobal pair)
                                    (Core.CBound 0))
                                (Core.CBound 0))))))

    member element set =
        Core.CApp
            (Core.CApp (Core.CIntrinsic Core.Member) element)
            set

    andP left right =
        notP (Core.CImp left (notP right))

    existsP proposition =
        notP (Core.CForall Core.TySet (notP proposition))

    notP proposition =
        Core.CImp proposition Core.CFalsum

confinesTerminalExactContradiction :: Assertion
confinesTerminalExactContradiction =
    Temp.withSystemTempDirectory "felix-exact-contradiction" \directory -> do
        let executable = directory Posix.</> "vampire"
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status ContradictoryAxioms for exact-contradiction'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation unusedResolver
        mounts <- exactFixtureMounts =<< getCurrentDirectory
        workspace <- parseExactWorkspace bootstrap mounts
            "test/phase5/exact-contradiction.tex"
        runs <- newIORef (0 :: Int)
        modules <-
            compileParsedWorkspaceWithResolver
                foundation
                bootstrap
                (countingAcceptedResolver executable runs)
                workspace
        accepted <- sole "terminal contradiction module" modules
        assertEqual "one indirect contradiction obligation"
            1 =<< readIORef runs
        assertCleanFactAlias accepted "phase5_contradiction"

        invalidWorkspace <- parseExactWorkspace bootstrap mounts
            "test/phase5/exact-contradiction-goal.tex"
        invalidParsed <-
            sole "invalid contradiction module"
                (toList
                    (Parse.parsedWorkspaceImportedBeforeImporter
                        invalidWorkspace))
        invalidInput <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                unusedResolver
                Declaration.FreshValidation
                invalidParsed
                [])
        Module.runTypedModule invalidInput >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactProofFailed
                            (ExactProof.ExactProofContradictionGoalMismatch
                                location)))
                    prefix -> do
                assertEqual "invalid contradiction line"
                    6 (locLine location)
                assertBool "invalid contradiction publishes no declaration"
                    (null
                        (Declaration.pendingModulePrefixBatches prefix))
            _result ->
                assertFailure "unexpected invalid contradiction result"

compilesExactReplacementComprehensions :: Assertion
compilesExactReplacementComprehensions =
    Temp.withSystemTempDirectory "felix-exact-replacement" \root -> do
        let relative = "test/phase5/exact-replacement.tex"
            executable = root Posix.</> "vampire"
        repository <- getCurrentDirectory
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation
                    unusedResolver
        mounts <- exactFixtureMounts repository
        workspace <- parseExactWorkspace bootstrap mounts relative
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-replacement'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        observations <- newIORef []
        let resolver = Declaration.vampireResolver \prepared -> do
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                modifyIORef' observations
                    (<> [ ( Backend.typedProblemRoute problem
                           , Backend.typedProblemAuxiliaryTag
                                <$> Vector.toList
                                    (Backend.typedProblemAuxiliaries problem)
                           )
                        ])
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        modules <- compileParsedWorkspaceWithResolver
            foundation bootstrap resolver workspace
        sealed <- sole "exact replacement module" modules
        assertExactReplacementModule sealed
        assertEqual
            "replacement proof uses its checked characteristic on TH0"
            [( Backend.RouteTh0
             , [Foundation.ReplacementCharacteristic]
             )]
            =<< readIORef observations

assertExactReplacementModule
    :: Module.SealedTypedModule
    -> Assertion
assertExactReplacementModule sealed =
    case Declaration.pendingModulePrefixBatches
            (Module.sealedTypedModulePrefix sealed) of
        [definitionBatch, theoremBatch] -> do
            definitionObject <- sole
                "replacement definition object"
                (Declaration.committedBatchObjects definitionBatch)
            case Identity.assertedObjectContent definitionObject of
                Identity.TransparentObjectContent
                        _theory coreType body -> do
                    assertEqual "replacement definition type"
                        (Core.TyArrow Core.TySet Core.TySet)
                        coreType
                    assertEqual "replacement definition body"
                        expectedBody
                        body
                content ->
                    assertFailure
                        ("unexpected replacement object " <> show content)
            assertEqual "replacement definition fact count"
                1
                (length
                    (Semantic.declarationDeltaFacts
                        (Declaration.committedBatchDelta definitionBatch)))
            assertEqual "replacement definition proposition count"
                1
                (length
                    (Declaration.committedBatchPropositions definitionBatch))
            assertEqual "replacement definition proof validations"
                []
                (Declaration.committedBatchProofValidations definitionBatch)

            assertEqual "replacement theorem adds no object"
                []
                (Declaration.committedBatchObjects theoremBatch)
            assertEqual "replacement theorem fact count"
                1
                (length
                    (Semantic.declarationDeltaFacts
                        (Declaration.committedBatchDelta theoremBatch)))
            assertEqual "replacement theorem proposition count"
                1
                (length
                    (Declaration.committedBatchPropositions theoremBatch))
            theoremValidation <- sole
                "replacement theorem validation"
                (Declaration.committedBatchProofValidations theoremBatch)
            case Authority.validationDirectAuthorization
                    (Semantic.proofValidationRecordCertificate
                        theoremValidation) of
                Authority.CheckedSourceProof [_request] ->
                    pure ()
                authorization ->
                    assertFailure
                        ("unexpected replacement theorem authority "
                            <> show authorization)
        batches ->
            assertFailure
                ("expected replacement definition and theorem, found "
                    <> show (length batches))
  where
    app1 intrinsic argument =
        Core.CApp (Core.CIntrinsic intrinsic) argument
    app2 intrinsic first second =
        Core.CApp (app1 intrinsic first) second
    expectedBody =
        Core.CLam Core.TySet $
            app1 Core.FamilyUnion $
                app2 Core.Repl (Core.CBound 0) $
                    Core.CLam Core.TySet $
                        app2 Core.Repl
                            (app2 Core.Sep
                                (Core.CBound 0)
                                (Core.CLam Core.TySet $
                                    Core.CEq Core.TySet
                                        (Core.CBound 1)
                                        (Core.CBound 0)))
                            (Core.CLam Core.TySet
                                (Core.CBound 0))

compilesAndReusesExactFiniteSets :: Assertion
compilesAndReusesExactFiniteSets =
    Temp.withSystemTempDirectory "felix-exact-finite-set" \root -> do
        let relative = "test/phase5/exact-finite-set.tex"
            sourcePath = root Posix.</> relative
            executable = root Posix.</> "vampire"
            storePath = root Posix.</> "store.sqlite"
        createDirectoryIfMissing True (Posix.takeDirectory sourcePath)
        ByteString.readFile relative >>= ByteString.writeFile sourcePath
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-finite-set'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation
                    unusedResolver
        mounts <- exactFixtureMounts root
        workspace <- parseExactWorkspace bootstrap mounts relative
        observations <- newIORef []
        let resolver = Declaration.vampireResolver \prepared -> do
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                modifyIORef' observations
                    (<> [ ( Backend.typedProblemRoute problem
                           , Backend.typedProblemAuxiliaryTag
                                <$> Vector.toList
                                    (Backend.typedProblemAuxiliaries problem)
                           )
                        ])
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        freshModules <-
            compileParsedWorkspaceWithValidation
                foundation bootstrap resolver
                Declaration.FreshValidation
                workspace
        fresh <- sole "fresh finite-set module" freshModules
        assertExactFiniteSetModule "fresh" fresh
        assertEqual
            "finite-set proof uses exactly its FOF characteristics"
            [( Backend.RouteFof
             , [ Foundation.EmptyCharacteristic
               , Foundation.PairSetCharacteristic
               , Foundation.FamilyUnionCharacteristic
               ]
             )]
            =<< readIORef observations

        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                expectRightIO
                    (Store.writePendingModulePrefix store
                        (Module.sealedTypedModulePrefix fresh))
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmRuns <- newIORef (0 :: Int)
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation bootstrap
                        (countingAcceptedResolver executable warmRuns)
                        validation
                        workspace
                assertEqual "warm finite-set proof skips Vampire"
                    0
                    =<< readIORef warmRuns
                warm <- sole "warm finite-set module" warmModules
                assertExactFiniteSetModule "warm" warm
                assertEqual "warm finite-set semantic interface"
                    (Module.sealedTypedModuleSemantic fresh)
                    (Module.sealedTypedModuleSemantic warm)
                assertEqual "warm finite-set final prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix fresh))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warm))

preparesExactDirectInductives :: Assertion
preparesExactDirectInductives = do
    prepared <-
        expectRight
            =<< prepareExactInductiveFixture
                "test/phase5/exact-inductive.tex"
    assertEqual "exact inductive carrier type"
        (Core.TyArrow Core.TySet Core.TySet)
        (ExactInductive.preparedExactInductiveCarrierType prepared)
    assertEqual "exact inductive carrier body"
        expectedCarrier
        (Core.frozenCoreTerm
            (ExactInductive.preparedExactInductiveCarrierBody prepared))
    assertEqual "foundation guard needs no imported fact"
        []
        (Vector.toList
            (ExactInductive.preparedExactInductiveGuardTargets prepared))
    let facts =
            toList
                (ExactInductive.preparedExactInductiveFacts prepared)
    assertEqual "generated fact order"
        [ Raw.Marker "phase5_fin_intro_1"
        , Raw.Marker "phase5_fin_dom_subset"
        , Raw.Marker "phase5_fin_cases"
        , Raw.Marker "phase5_fin_induct"
        ]
        (TypedInductive.typedInductiveFactMarker <$> facts)
    assertEqual "generated guarded-rule descriptors"
        [ Set.singleton Foundation.SetLfpFixed
        , Set.singleton Foundation.SetLfpBound
        , Set.singleton Foundation.SetLfpFixed
        , Set.singleton Foundation.SetLfpInduct
        ]
        ( Set.fromList
            . toList
            . TypedInductive.typedInductiveFactRules
            <$> facts
        )
    assertBool "generated targets are closed propositions"
        (all
            (\fact ->
                let target = TypedInductive.typedInductiveFactTarget fact
                in Core.frozenCoreType target == Core.TyProp
                    && Set.null (Core.frozenCoreGlobals target))
            facts)
  where
    apply1 intrinsic argument =
        Core.CApp (Core.CIntrinsic intrinsic) argument
    expectedCarrier =
        Core.CLam Core.TySet
            (Core.CApp
                (Core.CApp
                    (Core.CIntrinsic Core.ISetLfp)
                    (apply1 Core.UnivOf (Core.CBound 0)))
                (Core.CLam Core.TySet
                    (Core.CApp
                        (Core.CApp
                            (Core.CIntrinsic Core.Sep)
                            (apply1 Core.UnivOf (Core.CBound 1)))
                        (Core.CLam Core.TySet
                            (Core.CEq Core.TySet
                                (Core.CBound 0)
                                (Core.CBound 2))))))

preparesExactDatatypes :: Assertion
preparesExactDatatypes = do
    (foundation, owner, prepared) <-
        expectRight
            =<< prepareExactDatatypeFixture
                "test/phase5/exact-datatype.tex"
    let objects =
            toList
                (ExactDatatype.preparedExactDatatypeObjects prepared)
        objectIds = fst <$> objects
        objectTypes = snd <$> objects
        expectedTypes =
            [ Core.TySet
            , Core.TySet
            , Core.TyArrow Core.TySet Core.TySet
            , Core.TyArrow Core.TySet
                (Core.TyArrow Core.TySet Core.TySet)
            ]
        theory = Identity.theoryId foundation
        expectedIds =
            [ Identity.opaqueObjectId theory
                (Identity.opaqueDeclarationSeed
                    owner
                    (localDeclarationOrdinal 0)
                    DatatypeDeclaration
                    (generatedObjectSlot index))
                coreType
            | (index, coreType) <- zip [0 ..] expectedTypes
            ]
    assertEqual "datatype opaque object types"
        expectedTypes objectTypes
    assertEqual "datatype opaque object slots"
        expectedIds objectIds
    assertBool "datatype objects are opaque"
        (all ((== Identity.OpaqueObject) . Identity.objectIdFamily) objectIds)
    (carrierId, zeroId, atomId, joinId, constructorIds) <-
        case expectedIds of
            [carrier, zero, atom, join] ->
                pure
                    ( carrier
                    , zero
                    , atom
                    , join
                    , zero :| [atom, join]
                    )
            _ ->
                assertFailure "datatype object inventory is incomplete"
                    >> fail "unreachable"
    let facts =
            toList
                (ExactDatatype.preparedExactDatatypeFacts prepared)
        markers =
            ExactDatatype.preparedExactDatatypeFactMarker <$> facts
    assertEqual "datatype generated fact order"
        [ Internal.Marker "phase5_data_phasefivezero_intro"
        , Internal.Marker "phase5_data_phasefiveatom_intro"
        , Internal.Marker "phase5_data_phasefivejoin_intro"
        , Internal.Marker
            "phase5_data_phasefivezero_phasefiveatom_distinct"
        , Internal.Marker
            "phase5_data_phasefivezero_phasefivejoin_distinct"
        , Internal.Marker
            "phase5_data_phasefiveatom_phasefivejoin_distinct"
        , Internal.Marker "phase5_data_phasefiveatom_injective"
        , Internal.Marker "phase5_data_phasefivejoin_injective"
        , Internal.Marker "phase5_data_cases"
        , Internal.Marker "phase5_data_induct"
        ]
        markers
    assertBool "datatype generated targets are checked propositions"
        (all
            (\fact ->
                Core.frozenCoreType
                    (ExactDatatype.preparedExactDatatypeFactTarget fact)
                    == Core.TyProp)
            facts)
    atomIntroduction <-
        sole "domain-bearing datatype introduction"
            [ fact
            | fact <- facts
            , ExactDatatype.preparedExactDatatypeFactMarker fact
                == Internal.Marker "phase5_data_phasefiveatom_intro"
            ]
    assertEqual "domain-bearing datatype introduction target"
        (Core.CForall Core.TySet
            (Core.CImp
                (member
                    (Core.CBound 0)
                    (apply1 Core.FamilyUnion
                        (Core.CIntrinsic Core.Empty)))
                (member
                    (Core.CApp
                        (Core.CGlobal atomId)
                        (Core.CBound 0))
                    (Core.CGlobal carrierId))))
        (Core.frozenCoreTerm
            (ExactDatatype.preparedExactDatatypeFactTarget
                atomIntroduction))
    induction <-
        sole "datatype induction law"
            [ fact
            | fact <- facts
            , ExactDatatype.preparedExactDatatypeFactMarker fact
                == Internal.Marker "phase5_data_induct"
            ]
    assertEqual "datatype induction target"
        (Core.CForall Core.TySet
            (Core.CImp
                (conjunctions
                    [ member
                        (Core.CGlobal zeroId)
                        (Core.CBound 0)
                    , Core.CForall Core.TySet
                        (Core.CImp
                            (member
                                (Core.CBound 0)
                                (apply1 Core.FamilyUnion
                                    (Core.CIntrinsic Core.Empty)))
                            (member
                                (Core.CApp
                                    (Core.CGlobal atomId)
                                    (Core.CBound 0))
                                (Core.CBound 1)))
                    , Core.CForall Core.TySet
                        (Core.CForall Core.TySet
                            (Core.CImp
                                (conjunction
                                    (member
                                        (Core.CBound 1)
                                        (Core.CBound 2))
                                    (member
                                        (Core.CBound 0)
                                        (Core.CBound 2)))
                                (member
                                    (Core.CApp
                                        (Core.CApp
                                            (Core.CGlobal joinId)
                                            (Core.CBound 1))
                                        (Core.CBound 0))
                                    (Core.CBound 2))))
                    ])
                (Core.CForall Core.TySet
                    (Core.CImp
                        (member
                            (Core.CBound 0)
                            (Core.CGlobal carrierId))
                        (member
                            (Core.CBound 0)
                            (Core.CBound 1))))))
        (Core.frozenCoreTerm
            (ExactDatatype.preparedExactDatatypeFactTarget induction))
    assertEqual "datatype descriptor membership"
        (Authority.datatypeCompilationDescriptor
            carrierId
            constructorIds
            (ExactDatatype.preparedExactDatatypeFactReference <$> facts))
        (ExactDatatype.preparedExactDatatypeDescriptor prepared)
  where
    apply1 intrinsic argument =
        Core.CApp (Core.CIntrinsic intrinsic) argument

    member element set =
        Core.CApp
            (Core.CApp
                (Core.CIntrinsic Core.Member)
                element)
            set

    conjunction left right =
        Core.CImp
            (Core.CImp left (Core.CImp right Core.CFalsum))
            Core.CFalsum

    conjunctions = \case
        [] -> Core.CImp Core.CFalsum Core.CFalsum
        first : remaining -> foldl' conjunction first remaining

rejectsNestedExactDatatypeRecursion :: Assertion
rejectsNestedExactDatatypeRecursion = do
    result <-
        prepareExactDatatypeFixture
            "test/phase5/exact-datatype-nested.tex"
    case result of
        Left ExactDatatype.ExactDatatypeInvalid{} -> pure ()
        Left failure ->
            assertFailure
                ("unexpected nested datatype failure: " <> show failure)
        Right _prepared ->
            assertFailure "nested exact datatype recursion was accepted"

compilesAndReusesExactDatatypes :: Assertion
compilesAndReusesExactDatatypes =
    Temp.withSystemTempDirectory "felix-exact-datatype" \directory -> do
        let relative = "test/phase5/exact-datatype.tex"
            storePath = directory Posix.</> "store.sqlite"
        (foundation, bootstrap, workspace, freshModules) <-
            compileExactFixture relative
        fresh <- sole "fresh exact datatype module" freshModules
        assertExactDatatypeModule "fresh" fresh
        parsed <-
            sole "exact datatype parsed module"
                (toList
                    (Parse.parsedWorkspaceImportedBeforeImporter workspace))
        let artifact sealed = do
                key <- expectRight
                    (Semantic.moduleArtifactKey
                        (moduleName (Parse.parsedModuleAddress parsed))
                        (Parse.parsedModuleId parsed)
                        [ Semantic.semanticInterfaceAssertedId
                            (Module.sealedTypedModuleSemantic
                                (Module.bootstrapPreludeModule bootstrap))
                        ]
                        (Identity.theoryId foundation))
                pure
                    (Semantic.moduleArtifactResult
                        key
                        (Syntax.moduleSyntaxAssertedId
                            (Module.sealedTypedModuleSyntax sealed))
                        (Semantic.semanticInterfaceAssertedId
                            (Module.sealedTypedModuleSemantic sealed)))
        freshArtifact <- artifact fresh
        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                expectRightIO
                    (Store.writePendingModulePrefix store
                        (Module.sealedTypedModulePrefix fresh))
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation
                        bootstrap
                        unusedResolver
                        validation
                        workspace
                warm <- sole "warm exact datatype module" warmModules
                assertExactDatatypeModule "warm" warm
                assertEqual "warm exact datatype semantic interface"
                    (Module.sealedTypedModuleSemantic fresh)
                    (Module.sealedTypedModuleSemantic warm)
                assertEqual "warm exact datatype final prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix fresh))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warm))
                assertEqual "warm exact datatype module artifact"
                    freshArtifact
                    =<< artifact warm

        mounts <- exactFixtureMounts =<< getCurrentDirectory
        nestedWorkspace <-
            parseExactWorkspace bootstrap mounts
                "test/phase5/exact-datatype-nested.tex"
        nestedParsed <-
            sole "nested exact datatype module"
                (toList
                    (Parse.parsedWorkspaceImportedBeforeImporter
                        nestedWorkspace))
        nestedInput <-
            expectRight
                (Module.typedModuleInput
                    foundation
                    (Module.bootstrapPreludeReadiness bootstrap)
                    unusedResolver
                    Declaration.FreshValidation
                    nestedParsed
                    [])
        Module.runTypedModule nestedInput >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactDatatypeFailed
                            (ExactDatatype.ExactDatatypeInvalid
                                location _message)))
                    prefix -> do
                assertEqual "nested datatype failure line"
                    4
                    (locLine location)
                assertBool "nested datatype publishes no prefix"
                    (null
                        (Declaration.pendingModulePrefixBatches prefix))
            _result ->
                assertFailure "unexpected nested datatype result"

rejectsNestedExactInductiveRecursion :: Assertion
rejectsNestedExactInductiveRecursion = do
    result <-
        prepareExactInductiveFixture
            "test/phase5/exact-inductive-nested.tex"
    case result of
        Left (ExactInductive.ExactInductiveNestedRecursion location) ->
            assertEqual "nested recursive occurrence line"
                6
                (locLine location)
        Left failure ->
            assertFailure
                ("unexpected exact inductive failure: " <> show failure)
        Right{} ->
            assertFailure "nested inductive recursion was accepted"

compilesAndReusesExactInductives :: Assertion
compilesAndReusesExactInductives =
    Temp.withSystemTempDirectory "felix-exact-inductive" \directory -> do
        let relative = "test/phase5/exact-inductive.tex"
            storePath = directory Posix.</> "store.sqlite"
        (foundation, bootstrap, workspace, freshModules) <-
            compileExactFixture relative
        fresh <- sole "fresh exact inductive module" freshModules
        assertExactInductiveModule foundation "fresh" fresh
        parsed <-
            sole "exact inductive parsed module"
                (toList
                    (Parse.parsedWorkspaceImportedBeforeImporter workspace))
        let artifact sealed = do
                key <- expectRight
                    (Semantic.moduleArtifactKey
                        (moduleName (Parse.parsedModuleAddress parsed))
                        (Parse.parsedModuleId parsed)
                        [ Semantic.semanticInterfaceAssertedId
                            (Module.sealedTypedModuleSemantic
                                (Module.bootstrapPreludeModule bootstrap))
                        ]
                        (Identity.theoryId foundation))
                pure
                    (Semantic.moduleArtifactResult
                        key
                        (Syntax.moduleSyntaxAssertedId
                            (Module.sealedTypedModuleSyntax sealed))
                        (Semantic.semanticInterfaceAssertedId
                            (Module.sealedTypedModuleSemantic sealed)))
        freshArtifact <- artifact fresh
        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                expectRightIO
                    (Store.writePendingModulePrefix store
                        (Module.sealedTypedModulePrefix fresh))
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation
                        bootstrap
                        unusedResolver
                        validation
                        workspace
                warm <- sole "warm exact inductive module" warmModules
                assertExactInductiveModule foundation "warm" warm
                assertEqual "warm exact inductive semantic interface"
                    (Module.sealedTypedModuleSemantic fresh)
                    (Module.sealedTypedModuleSemantic warm)
                assertEqual "warm exact inductive final prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix fresh))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warm))
                assertEqual "warm exact inductive module artifact"
                    freshArtifact
                    =<< artifact warm

        mounts <- exactFixtureMounts =<< getCurrentDirectory
        nestedWorkspace <-
            parseExactWorkspace bootstrap mounts
                "test/phase5/exact-inductive-nested.tex"
        nestedParsed <-
            sole "nested exact inductive module"
                (toList
                    (Parse.parsedWorkspaceImportedBeforeImporter
                        nestedWorkspace))
        nestedInput <-
            expectRight
                (Module.typedModuleInput
                    foundation
                    (Module.bootstrapPreludeReadiness bootstrap)
                    unusedResolver
                    Declaration.FreshValidation
                    nestedParsed
                    [])
        Module.runTypedModule nestedInput >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactInductiveFailed
                            (ExactInductive.ExactInductiveNestedRecursion
                                location)))
                    prefix -> do
                assertEqual "nested failure line" 6 (locLine location)
                assertBool "nested declaration publishes no prefix"
                    (null (Declaration.pendingModulePrefixBatches prefix))
            _result ->
                assertFailure "unexpected nested inductive result"

authorizesRecursiveExactInductives :: Assertion
authorizesRecursiveExactInductives =
    Temp.withSystemTempDirectory "felix-recursive-inductive" \directory -> do
        let relative = "test/phase5/exact-inductive-recursive.tex"
            storePath = directory Posix.</> "store.sqlite"
        (foundation, bootstrap, workspace, freshModules) <-
            compileExactFixture relative
        fresh <- sole "fresh recursive inductive module" freshModules
        assertRecursiveExactInductiveModule "fresh" fresh
        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                expectRightIO
                    (Store.writePendingModulePrefix store
                        (Module.sealedTypedModulePrefix fresh))
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation
                        bootstrap
                        unusedResolver
                        validation
                        workspace
                warm <- sole "warm recursive inductive module" warmModules
                assertRecursiveExactInductiveModule "warm" warm
                assertEqual "warm recursive inductive semantic interface"
                    (Module.sealedTypedModuleSemantic fresh)
                    (Module.sealedTypedModuleSemantic warm)
                assertEqual "warm recursive inductive final prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix fresh))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warm))

assertRecursiveExactInductiveModule
    :: String
    -> Module.SealedTypedModule
    -> Assertion
assertRecursiveExactInductiveModule label sealed =
    case Declaration.pendingModulePrefixBatches
            (Module.sealedTypedModulePrefix sealed) of
        [_axiomBatch, inductiveBatch] -> do
            object <-
                sole (label <> " recursive inductive carrier")
                    (Declaration.committedBatchObjects inductiveBatch)
            let facts =
                    Semantic.declarationDeltaFacts
                        (Declaration.committedBatchDelta inductiveBatch)
                sourceSafety =
                    Authority.authoritySafety
                        (Authority.singletonEscapeKind
                            Authority.SourceAxiom)
            assertEqual (label <> " recursive inductive safety")
                (Authority.cleanAuthoritySafety : replicate 4 sourceSafety)
                ( Authority.factAuthoritySafety
                    . Semantic.semanticFactAuthority
                    <$> facts
                )
            validation <-
                maybe
                    (assertFailure
                        (label <> ": recursive validation is absent")
                        >> fail "unreachable")
                    pure
                    (Declaration.committedBatchDeclarationValidation
                        inductiveBatch)
            assertEqual (label <> " recursive inductive descriptors")
                [ Authority.CheckedKernelConstruction
                    (Authority.CheckedDefinitionEquation
                        (Identity.assertedObjectId object))
                , guardedRules
                    (Foundation.SetLfpBound :| [Foundation.SetLfpFixed])
                , guardedRules (Foundation.SetLfpBound :| [])
                , guardedRules (Foundation.SetLfpFixed :| [])
                , guardedRules (Foundation.SetLfpInduct :| [])
                ]
                ( Authority.validationDirectAuthorization
                    <$> Semantic.declarationValidationRecordCertificates
                        validation
                )
        batches ->
            assertFailure
                (label <> ": expected axiom and inductive batches, found "
                    <> show (length batches))
  where
    guardedRules rules =
        Authority.CheckedKernelConstruction
            (Authority.GuardedFoundationRules
                (Authority.guardedRuleSet rules))

assertExactDatatypeModule
    :: String
    -> Module.SealedTypedModule
    -> Assertion
assertExactDatatypeModule label sealed = do
    assertEqual (label <> " datatype semantic declaration count")
        1
        (length
            (Semantic.semanticInterfaceDeclarations
                (Module.sealedTypedModuleSemantic sealed)))
    batch <-
        sole (label <> " datatype declaration batch")
            (Declaration.pendingModulePrefixBatches
                (Module.sealedTypedModulePrefix sealed))
    let objects = Declaration.committedBatchObjects batch
        objectIds = Identity.assertedObjectId <$> objects
        delta = Declaration.committedBatchDelta batch
        facts = Semantic.declarationDeltaFacts delta
        aliases = Semantic.declarationDeltaAliases delta
        bindings =
            Semantic.semanticEnvironmentBindings
                (Semantic.declarationDeltaEnvironment delta)
        boundIds =
            Semantic.semanticGlobalTargetObject
                . Semantic.semanticGlobalBindingTarget
                <$> bindings
    assertEqual (label <> " datatype object count") 4 (length objects)
    assertBool (label <> " datatype objects are opaque")
        (all
            ((== Identity.OpaqueObject)
                . Identity.objectIdFamily
                . Identity.assertedObjectId)
            objects)
    assertEqual (label <> " datatype global binding count")
        4
        (length bindings)
    assertBool (label <> " datatype globals are references")
        (all
            (\binding ->
                case Semantic.semanticGlobalBindingTarget binding of
                    Semantic.GlobalReference{} -> True
                    Semantic.TransparentExpansion{} -> False
                    Semantic.ContextualTransparentExpansion{} -> False)
            bindings)
    assertEqual (label <> " datatype global targets")
        (Set.fromList objectIds)
        (Set.fromList boundIds)
    assertEqual (label <> " datatype fact count") 10 (length facts)
    assertEqual (label <> " datatype aliases")
        (Semantic.semanticName <$>
            [ "phase5_data_phasefivezero_intro"
            , "phase5_data_phasefiveatom_intro"
            , "phase5_data_phasefivejoin_intro"
            , "phase5_data_phasefivezero_phasefiveatom_distinct"
            , "phase5_data_phasefivezero_phasefivejoin_distinct"
            , "phase5_data_phasefiveatom_phasefivejoin_distinct"
            , "phase5_data_phasefiveatom_injective"
            , "phase5_data_phasefivejoin_injective"
            , "phase5_data_cases"
            , "phase5_data_induct"
            ])
        (Semantic.semanticAliasName <$> aliases)
    assertBool (label <> " datatype facts are clean")
        (all
            ((== Authority.cleanAuthoritySafety)
                . Authority.factAuthoritySafety
                . Semantic.semanticFactAuthority)
            facts)
    assertEqual (label <> " datatype proof validations")
        []
        (Declaration.committedBatchProofValidations batch)
    validation <-
        maybe
            (assertFailure (label <> ": datatype validation is absent")
                >> fail "unreachable")
            pure
            (Declaration.committedBatchDeclarationValidation batch)
    descriptor <-
        case objectIds of
            carrier : firstConstructor : remainingConstructors ->
                pure
                    (Authority.datatypeCompilationDescriptor
                        carrier
                        (firstConstructor :| remainingConstructors)
                        ( Authority.factAuthorityTheorem
                            . Semantic.semanticFactAuthority
                            <$> facts
                        ))
            _ ->
                assertFailure (label <> ": datatype object family is absent")
                    >> fail "unreachable"
    assertEqual (label <> " datatype validation descriptors")
        (replicate 10
            (Authority.TrustedCompilation
                (Authority.DatatypeCompilation descriptor)))
        ( Authority.validationDirectAuthorization
            <$> Semantic.declarationValidationRecordCertificates validation
        )

assertExactInductiveModule
    :: Foundation.CheckedFoundation
    -> String
    -> Module.SealedTypedModule
    -> Assertion
assertExactInductiveModule foundation label sealed =
    case Declaration.pendingModulePrefixBatches
            (Module.sealedTypedModulePrefix sealed) of
        [batch] -> do
            object <-
                sole (label <> " inductive carrier")
                    (Declaration.committedBatchObjects batch)
            case Identity.assertedObjectContent object of
                Identity.TransparentObjectContent
                        _theory coreType body -> do
                    assertEqual (label <> " inductive carrier type")
                        (Core.TyArrow Core.TySet Core.TySet)
                        coreType
                    assertEqual (label <> " inductive carrier identity")
                        (Identity.transparentObjectId
                            (Identity.theoryId foundation)
                            coreType
                            body)
                        (Identity.assertedObjectId object)
                content ->
                    assertFailure
                        (label <> ": unexpected inductive carrier "
                            <> show content)
            let delta = Declaration.committedBatchDelta batch
                facts = Semantic.declarationDeltaFacts delta
                aliases = Semantic.declarationDeltaAliases delta
            assertEqual (label <> " inductive fact count")
                5
                (length facts)
            assertEqual (label <> " inductive aliases")
                (Semantic.semanticName <$>
                    [ "phase5_fin"
                    , "phase5_fin_intro_1"
                    , "phase5_fin_dom_subset"
                    , "phase5_fin_cases"
                    , "phase5_fin_induct"
                    ])
                (Semantic.semanticAliasName <$> aliases)
            assertBool (label <> " inductive facts are clean")
                (all
                    ((== Authority.cleanAuthoritySafety)
                        . Authority.factAuthoritySafety
                        . Semantic.semanticFactAuthority)
                    facts)
            assertEqual (label <> " inductive proof validations")
                []
                (Declaration.committedBatchProofValidations batch)
            validation <-
                maybe
                    (assertFailure
                        (label <> ": inductive validation is absent")
                        >> fail "unreachable")
                    pure
                    (Declaration.committedBatchDeclarationValidation batch)
            assertEqual (label <> " inductive validation descriptors")
                [ Authority.CheckedKernelConstruction
                    (Authority.CheckedDefinitionEquation
                        (Identity.assertedObjectId object))
                , guardedRules (Foundation.SetLfpFixed :| [])
                , guardedRules (Foundation.SetLfpBound :| [])
                , guardedRules (Foundation.SetLfpFixed :| [])
                , guardedRules (Foundation.SetLfpInduct :| [])
                ]
                ( Authority.validationDirectAuthorization
                    <$> Semantic.declarationValidationRecordCertificates
                        validation
                )
        batches ->
            assertFailure
                (label <> ": expected one inductive batch, found "
                    <> show (length batches))
  where
    guardedRules rules =
        Authority.CheckedKernelConstruction
            (Authority.GuardedFoundationRules
                (Authority.guardedRuleSet rules))

assertExactFiniteSetModule
    :: String
    -> Module.SealedTypedModule
    -> Assertion
assertExactFiniteSetModule label sealed = do
    assertEqual (label <> " finite-set semantic declarations")
        2
        (length
            (Semantic.semanticInterfaceDeclarations
                (Module.sealedTypedModuleSemantic sealed)))
    case Declaration.pendingModulePrefixBatches
            (Module.sealedTypedModulePrefix sealed) of
        [definitionBatch, theoremBatch] -> do
            definitionObject <- sole
                (label <> " finite-set definition object")
                (Declaration.committedBatchObjects definitionBatch)
            case Identity.assertedObjectContent definitionObject of
                Identity.TransparentObjectContent
                        _theory coreType body -> do
                    assertEqual (label <> " finite-set definition type")
                        (Core.TyArrow Core.TySet
                            (Core.TyArrow Core.TySet Core.TySet))
                        coreType
                    assertEqual (label <> " finite-set definition body")
                        expectedBody
                        body
                content ->
                    assertFailure
                        (label <> ": unexpected finite-set object "
                            <> show content)
            assertEqual (label <> " finite-set definition fact count")
                1
                (length
                    (Semantic.declarationDeltaFacts
                        (Declaration.committedBatchDelta definitionBatch)))
            assertEqual (label <> " finite-set definition proof validations")
                []
                (Declaration.committedBatchProofValidations definitionBatch)

            assertEqual (label <> " finite-set theorem adds no object")
                []
                (Declaration.committedBatchObjects theoremBatch)
            theoremFact <- sole
                (label <> " finite-set theorem fact")
                (Semantic.declarationDeltaFacts
                    (Declaration.committedBatchDelta theoremBatch))
            assertEqual (label <> " finite-set theorem safety")
                Authority.cleanAuthoritySafety
                (Authority.factAuthoritySafety
                    (Semantic.semanticFactAuthority theoremFact))
            theoremValidation <- sole
                (label <> " finite-set theorem validation")
                (Declaration.committedBatchProofValidations theoremBatch)
            case Authority.validationDirectAuthorization
                    (Semantic.proofValidationRecordCertificate
                        theoremValidation) of
                Authority.CheckedSourceProof [_request] ->
                    pure ()
                authorization ->
                    assertFailure
                        (label <> ": unexpected finite-set theorem authority "
                            <> show authorization)
        batches ->
            assertFailure
                (label <> ": expected finite-set definition and theorem, found "
                    <> show (length batches))
  where
    expectedBody =
        Core.CLam Core.TySet
            (Core.CLam Core.TySet
                (Core.canonicalSetInsert
                    (Core.CBound 1)
                    (Core.canonicalSetInsert
                        (Core.CBound 0)
                        (Core.CIntrinsic Core.Empty))))

assertExactSeparationModule
    :: String
    -> Module.SealedTypedModule
    -> Assertion
assertExactSeparationModule label sealed = do
    case Declaration.pendingModulePrefixBatches
            (Module.sealedTypedModulePrefix sealed) of
        [definitionBatch, theoremBatch] -> do
            assertEqual (label <> " separation definition object count")
                1
                (length
                    (Declaration.committedBatchObjects definitionBatch))
            definitionObject <- sole
                (label <> " separation definition object")
                (Declaration.committedBatchObjects definitionBatch)
            case Identity.assertedObjectContent definitionObject of
                Identity.TransparentObjectContent
                        _theory coreType body -> do
                    assertEqual (label <> " separation definition type")
                        (Core.TyArrow Core.TySet Core.TySet)
                        coreType
                    assertEqual (label <> " separation definition body")
                        (Core.CLam Core.TySet
                            (Core.CApp
                                (Core.CApp
                                    (Core.CIntrinsic Core.Sep)
                                    (Core.CBound 0))
                                (Core.CLam Core.TySet
                                    (Core.CEq Core.TySet
                                        (Core.CBound 0)
                                        (Core.CBound 0)))))
                        body
                content ->
                    assertFailure
                        (label <> ": unexpected separation object "
                            <> show content)
            assertEqual (label <> " definition fact count")
                1
                (length
                    (Semantic.declarationDeltaFacts
                        (Declaration.committedBatchDelta definitionBatch)))
            assertEqual (label <> " definition proposition count")
                1
                (length
                    (Declaration.committedBatchPropositions definitionBatch))
            assertEqual (label <> " definition proof validations")
                []
                (Declaration.committedBatchProofValidations definitionBatch)
            definitionValidation <-
                maybe
                    (assertFailure
                        (label <> ": definition validation is absent")
                        >> fail "unreachable")
                    pure
                    (Declaration.committedBatchDeclarationValidation
                        definitionBatch)
            definitionCertificate <- sole
                (label <> " definition certificate")
                (Semantic.declarationValidationRecordCertificates
                    definitionValidation)
            case Authority.validationDirectAuthorization
                    definitionCertificate of
                Authority.CheckedKernelConstruction
                        (Authority.CheckedDefinitionEquation _target) ->
                    pure ()
                authorization ->
                    assertFailure
                        (label <> ": unexpected definition authority "
                            <> show authorization)

            assertEqual (label <> " theorem adds no object")
                []
                (Declaration.committedBatchObjects theoremBatch)
            theoremFact <- sole
                (label <> " separation theorem fact")
                (Semantic.declarationDeltaFacts
                    (Declaration.committedBatchDelta theoremBatch))
            assertEqual (label <> " theorem safety")
                Authority.cleanAuthoritySafety
                (Authority.factAuthoritySafety
                    (Semantic.semanticFactAuthority theoremFact))
            theoremValidation <- sole
                (label <> " separation theorem validation")
                (Declaration.committedBatchProofValidations theoremBatch)
            case Authority.validationDirectAuthorization
                    (Semantic.proofValidationRecordCertificate
                        theoremValidation) of
                Authority.CheckedSourceProof [_request] ->
                    pure ()
                authorization ->
                    assertFailure
                        (label <> ": unexpected theorem authority "
                            <> show authorization)
        batches ->
            assertFailure
                (label <> ": expected definition and theorem, found "
                    <> show (length batches))

reusesExactSeparationValidation :: Assertion
reusesExactSeparationValidation =
    Temp.withSystemTempDirectory "felix-exact-separation-cache" \root -> do
        let relative = "test/phase5/exact-separation.tex"
            sourcePath = root Posix.</> relative
            executable = root Posix.</> "vampire"
            storePath = root Posix.</> "store.sqlite"
        createDirectoryIfMissing True (Posix.takeDirectory sourcePath)
        ByteString.readFile relative >>= ByteString.writeFile sourcePath
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-separation-cache'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation
                    unusedResolver
        mounts <- exactFixtureMounts root
        workspace <- parseExactWorkspace bootstrap mounts relative
        freshRuns <- newIORef (0 :: Int)
        freshModules <-
            compileParsedWorkspaceWithValidation
                foundation
                bootstrap
                (countingAcceptedResolver executable freshRuns)
                Declaration.FreshValidation
                workspace
        assertEqual "fresh separation proof runs Vampire once"
            1
            =<< readIORef freshRuns
        fresh <- sole "fresh exact separation module" freshModules
        assertExactSeparationModule "fresh cached" fresh
        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                expectRightIO
                    (Store.writePendingModulePrefix store
                        (Module.sealedTypedModulePrefix fresh))
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmRuns <- newIORef (0 :: Int)
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation
                        bootstrap
                        (countingAcceptedResolver executable warmRuns)
                        validation
                        workspace
                assertEqual "warm separation proof skips Vampire"
                    0
                    =<< readIORef warmRuns
                warm <- sole "warm exact separation module" warmModules
                assertExactSeparationModule "warm cached" warm
                assertEqual "warm separation semantic interface"
                    (Module.sealedTypedModuleSemantic fresh)
                    (Module.sealedTypedModuleSemantic warm)
                assertEqual "warm separation final prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix fresh))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warm))
                let components sealed =
                        let batches =
                                Declaration.pendingModulePrefixBatches
                                    (Module.sealedTypedModulePrefix sealed)
                        in ( concatMap
                                Declaration.committedBatchObjects
                                batches
                           , concatMap
                                (fmap Identity.checkedPropositionId
                                    . Declaration.committedBatchPropositions)
                                batches
                           , concatMap
                                Declaration.committedBatchProofValidations
                                batches
                           , Declaration.committedBatchDeclarationValidation
                                <$> batches
                           )
                assertEqual "warm separation checked artifacts"
                    (components fresh)
                    (components warm)

compilesExactSourceAxioms :: Assertion
compilesExactSourceAxioms =
    Temp.withSystemTempDirectory "felix-exact-source-axiom" \root -> do
        let storePath = root Posix.</> "store.sqlite"
        (foundation, bootstrap, workspace, freshModules) <-
            compileExactFixture
                "test/phase5/exact-source-axiom-assumptions.tex"
        fresh <- sole "fresh source-axiom module" freshModules
        assertSourceAxiom "fresh" fresh
        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                expectRightIO
                    (Store.writePendingModulePrefix store
                        (Module.sealedTypedModulePrefix fresh))
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                warmModules <-
                    compileParsedWorkspaceWithValidation
                        foundation bootstrap unusedResolver validation workspace
                warm <- sole "warm source-axiom module" warmModules
                assertSourceAxiom "warm" warm
                assertEqual "warm source axiom preserves semantics"
                    (Module.sealedTypedModuleSemantic fresh)
                    (Module.sealedTypedModuleSemantic warm)
                assertEqual "warm source axiom preserves prefix"
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix fresh))
                    (Declaration.pendingModulePrefixCurrent
                        (Module.sealedTypedModulePrefix warm))
  where
    assertSourceAxiom label sealed = do
        batch <- sole (label <> " source-axiom batch")
            (Declaration.pendingModulePrefixBatches
                (Module.sealedTypedModulePrefix sealed))
        fact <- sole (label <> " source-axiom fact")
            (Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta batch))
        alias <- sole (label <> " source-axiom alias")
            (Semantic.declarationDeltaAliases
                (Declaration.committedBatchDelta batch))
        assertEqual (label <> " source-axiom search eligibility")
            Semantic.SearchEligible
            (Semantic.semanticFactSearchEligibility fact)
        assertEqual (label <> " source-axiom marker alias")
            (Semantic.semanticName "phase5_exact_source_axiom_assumptions")
            (Semantic.semanticAliasName alias)
        proposition <- sole (label <> " source-axiom proposition")
            (Declaration.committedBatchPropositions batch)
        assertEqual (label <> " source-axiom closed target")
            (Core.CForall Core.TySet
                (Core.CForall Core.TySet
                    (Core.CImp
                        (member (Core.CBound 0) (Core.CBound 1))
                        (Core.CImp
                            (Core.CEq Core.TySet
                                (Core.CBound 0)
                                (Core.CBound 0))
                            (member
                                (Core.CBound 0)
                                (Core.CBound 1))))))
            (Core.frozenCoreTerm
                (Identity.checkedPropositionTerm proposition))
        assertEqual (label <> " source-axiom safety")
            (Authority.authoritySafety
                (Authority.singletonEscapeKind Authority.SourceAxiom))
            (Authority.factAuthoritySafety
                (Semantic.semanticFactAuthority fact))
        validation <-
            maybe
                (assertFailure (label <> " source-axiom validation is absent")
                    >> fail "unreachable")
                pure
                (Declaration.committedBatchDeclarationValidation batch)
        certificate <- sole (label <> " source-axiom certificate")
            (Semantic.declarationValidationRecordCertificates validation)
        assertEqual (label <> " source-axiom direct authority")
            Authority.SourceAxiomAuthorization
            (Authority.validationDirectAuthorization certificate)
        assertEqual (label <> " source axiom has no proof validations")
            []
            (Declaration.committedBatchProofValidations batch)

    member element set =
        Core.CApp
            (Core.CApp
                (Core.CIntrinsic Core.Member)
                element)
            set

rejectsProofLocalGeneralization :: Assertion
rejectsProofLocalGeneralization = do
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation unusedResolver
    repository <- getCurrentDirectory
    mounts <- exactFixtureMounts repository
    workspace <- parseExactWorkspace
        bootstrap mounts
        "test/phase5/exact-proof-local-free.tex"
    input <- expectRight
        (Module.typedModuleInput
            foundation
            (Module.bootstrapPreludeReadiness bootstrap)
            unusedResolver
            Declaration.FreshValidation
            (Parse.parsedWorkspaceRootModule workspace)
            [])
    Module.runTypedModule input >>= \case
        Module.TypedModuleFailed
                (Module.TypedActionFailed
                    (Module.TypedExactProofFailed
                        (ExactProof.ExactProofElaborationFailed
                            (Exact.ExactFreeVariable location
                                (Raw.NamedVar "y")))))
                prefix -> do
            assertEqual "proof-local free variable line"
                6 (locLine location)
            assertEqual "proof-local failure commits nothing"
                0
                (length
                    (Declaration.pendingModulePrefixBatches prefix))
        Module.TypedModuleSucceeded{} ->
            assertFailure "proof-local variable was generalized"
        Module.TypedModuleOpenFailed failure ->
            assertFailure
                ("proof-local generalization module did not open: "
                    <> show failure)
        Module.TypedModuleFailed failure _prefix ->
            assertFailure
                ("unexpected proof-local generalization failure: "
                    <> show failure)

doesNotTreatMarkerOnlyNounAsSet :: Assertion
doesNotTreatMarkerOnlyNounAsSet = do
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation unusedResolver
    repository <- getCurrentDirectory
    mounts <- exactFixtureMounts repository
    workspace <- parseExactWorkspace
        bootstrap mounts
        "test/phase5/exact-set-marker.tex"
    Temp.withSystemTempDirectory "felix-exact-set-marker" \root -> do
        let executable = root Posix.</> "vampire"
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for set-marker'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        observed <- newIORef []
        let resolver = Declaration.vampireResolver \prepared -> do
                let problem =
                        Provers.preparedTypedProverLogicalProblem prepared
                    claim = Backend.typedProblemClaim problem
                    locals = Backend.typedProblemLocalPremises problem
                modifyIORef' observed
                    (<> [ [ Backend.supportedPropositionTerm
                                (Backend.typedLocalPremiseProposition premise)
                            == Backend.supportedPropositionTerm claim
                           | premise <- Vector.toList locals
                           ]
                        ])
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        input <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                resolver
                Declaration.FreshValidation
                (Parse.parsedWorkspaceRootModule workspace)
                [])
        Module.runTypedModule input >>= \case
            Module.TypedModuleSucceeded{} ->
                assertEqual
                    "the source noun supplies the local proof premise"
                    [[True]]
                    =<< readIORef observed
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    ("marker-only set noun module did not open: "
                        <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    ("unexpected marker-only set noun failure: "
                        <> show failure)

compilesExactOmittedProofs :: Assertion
compilesExactOmittedProofs =
    Temp.withSystemTempDirectory "felix-exact-omitted" \root -> do
        repository <- getCurrentDirectory
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation unusedResolver
        mounts <- exactFixtureMounts repository
        workspace <- parseExactWorkspace
            bootstrap mounts "test/phase5/exact-omitted.tex"
        let executable = root Posix.</> "vampire"
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-omitted'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        calls <- newIORef (0 :: Int)
        let resolver = Declaration.vampireResolver \prepared -> do
                modifyIORef' calls (+ 1)
                runNoLoggingT
                    (Provers.runPreparedTypedProver
                        (Provers.vampire
                            executable
                            Provers.defaultTimeLimit
                            Provers.defaultMemoryLimit)
                        prepared)
        modules <-
            compileParsedWorkspaceWithResolver
                foundation bootstrap resolver workspace
        sealed <- sole "exact omitted module" modules
        assertEqual "only the non-omitted continuation invokes Vampire"
            1
            =<< readIORef calls
        let batches =
                Declaration.pendingModulePrefixBatches
                    (Module.sealedTypedModulePrefix sealed)
        assertEqual "top-level and nested omitted declarations"
            2 (length batches)
        for_ (zip ["top-level", "nested"] batches) \(label, batch) -> do
            fact <- sole (label <> " omitted fact")
                (Semantic.declarationDeltaFacts
                    (Declaration.committedBatchDelta batch))
            assertEqual (label <> " omitted safety")
                (Authority.authoritySafety
                    (Authority.singletonEscapeKind Authority.Omitted))
                (Authority.factAuthoritySafety
                    (Semantic.semanticFactAuthority fact))
            record <- sole (label <> " omitted validation")
                (Declaration.committedBatchProofValidations batch)
            assertEqual (label <> " omitted direct authority")
                Authority.OmittedAuthorization
                (Authority.validationDirectAuthorization
                    (Semantic.proofValidationRecordCertificate record))
            assertEqual (label <> " publishes only its final theorem")
                1
                (length
                    (Semantic.declarationDeltaFacts
                        (Declaration.committedBatchDelta batch)))

reusesExactEscapeAuthority :: Assertion
reusesExactEscapeAuthority =
    Temp.withSystemTempDirectory "felix-exact-escape-cache" \root -> do
        let consumerRelative = "test/phase5/exact-escape-consumer.tex"
            producerRelative = "test/phase5/exact-escape-producer.tex"
            consumerPath = root Posix.</> consumerRelative
            producerPath = root Posix.</> producerRelative
            executable = root Posix.</> "vampire"
            storePath = root Posix.</> "store.sqlite"
        createDirectoryIfMissing True (Posix.takeDirectory consumerPath)
        consumerSource <- ByteString.readFile consumerRelative
        producerSource <- ByteString.readFile producerRelative
        ByteString.writeFile consumerPath consumerSource
        ByteString.writeFile producerPath producerSource
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-escape'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation unusedResolver
        mounts <- exactFixtureMounts root
        freshWorkspace <-
            parseExactWorkspace bootstrap mounts consumerRelative
        freshRuns <- newIORef (0 :: Int)
        freshModules <-
            compileParsedWorkspaceWithValidation
                foundation bootstrap
                (acceptedResolver executable freshRuns)
                Declaration.FreshValidation
                freshWorkspace
        assertEqual "fresh escape graph Vampire requests"
            5
            =<< readIORef freshRuns
        assertEscapeGraph "fresh" freshModules
        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                traverse_
                    (expectRightIO
                        . Store.writePendingModulePrefix store
                        . Module.sealedTypedModulePrefix)
                    freshModules
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                    compileWarm workspace = do
                        runs <- newIORef (0 :: Int)
                        modules <-
                            compileParsedWorkspaceWithValidation
                                foundation bootstrap
                                (acceptedResolver executable runs)
                                validation
                                workspace
                        runCount <- readIORef runs
                        pure (modules, runCount)
                (warmModules, warmRuns) <- compileWarm freshWorkspace
                assertEqual "exact escape warm hit skips Vampire"
                    0 warmRuns
                assertEscapeGraph "warm" warmModules
                assertEqual "warm escape graph preserves module semantics"
                    (moduleSemantics freshModules)
                    (moduleSemantics warmModules)
                assertEqual "warm escape graph preserves module prefixes"
                    (modulePrefixes freshModules)
                    (modulePrefixes warmModules)

                let formattingOnly =
                        Text.encodeUtf8
                            ("% shifted exact escape source\n"
                                <> Text.decodeUtf8 consumerSource)
                ByteString.writeFile consumerPath formattingOnly
                formattedWorkspace <-
                    parseExactWorkspace bootstrap mounts consumerRelative
                assertBool "formatting changes the escape parsed identity"
                    (Parse.parsedModuleId
                        (Parse.parsedWorkspaceRootModule freshWorkspace)
                        /= Parse.parsedModuleId
                            (Parse.parsedWorkspaceRootModule
                                formattedWorkspace))
                (formattedModules, formattedRuns) <-
                    compileWarm formattedWorkspace
                assertEqual "formatting-only escape edit reuses validation"
                    0 formattedRuns
                assertEqual "formatting-only escape edit preserves semantics"
                    (moduleSemantics freshModules)
                    (moduleSemantics formattedModules)

                let omittedGoalEdit =
                        Text.encodeUtf8
                            (StrictText.replace
                                "    Show $x = x$."
                                "    Show if $x = x$, then $x = x$."
                                (Text.decodeUtf8 consumerSource))
                ByteString.writeFile consumerPath omittedGoalEdit
                editedWorkspace <-
                    parseExactWorkspace bootstrap mounts consumerRelative
                (editedModules, editedRuns) <-
                    compileWarm editedWorkspace
                assertEqual "changed omitted goal misses its proof validation"
                    1 editedRuns
                assertEqual "changed omitted goal preserves public semantics"
                    (moduleSemantics freshModules)
                    (moduleSemantics editedModules)
  where
    acceptedResolver executable runs =
        Declaration.vampireResolver \prepared -> do
            modifyIORef' runs (+ 1)
            runNoLoggingT
                (Provers.runPreparedTypedProver
                    (Provers.vampire
                        executable
                        Provers.defaultTimeLimit
                        Provers.defaultMemoryLimit)
                    prepared)

    moduleSemantics = fmap Module.sealedTypedModuleSemantic
    modulePrefixes =
        fmap
            (Declaration.pendingModulePrefixCurrent
                . Module.sealedTypedModulePrefix)

    assertEscapeGraph label = \case
        [producer, consumer] -> do
            let producerBatches =
                    Declaration.pendingModulePrefixBatches
                        (Module.sealedTypedModulePrefix producer)
                consumerBatches =
                    Declaration.pendingModulePrefixBatches
                        (Module.sealedTypedModulePrefix consumer)
            case producerBatches of
                [sourceAxiom, omitted] -> do
                    assertEscapeSafety
                        (label <> " source axiom")
                        [Authority.SourceAxiom]
                        sourceAxiom
                    assertDeclarationDirect
                        (label <> " source axiom")
                        Authority.SourceAxiomAuthorization
                        sourceAxiom
                    assertEscapeSafety
                        (label <> " omitted theorem")
                        [Authority.Omitted]
                        omitted
                    assertProofDirectOmitted
                        (label <> " omitted theorem")
                        omitted
                batches ->
                    assertFailure
                        (label <> " producer batch count: "
                            <> show (length batches))
            case consumerBatches of
                [fromAxiom, fromOmitted, throughLocal, ownOmission] -> do
                    assertEscapeSafety
                        (label <> " source-axiom consumer")
                        [Authority.SourceAxiom]
                        fromAxiom
                    assertProofDirectChecked
                        (label <> " source-axiom consumer") 1 fromAxiom
                    assertEscapeSafety
                        (label <> " omitted consumer")
                        [Authority.Omitted]
                        fromOmitted
                    assertProofDirectChecked
                        (label <> " omitted consumer") 1 fromOmitted
                    assertEscapeSafety
                        (label <> " local source-axiom consumer")
                        [Authority.SourceAxiom]
                        throughLocal
                    assertProofDirectChecked
                        (label <> " local source-axiom consumer")
                        2 throughLocal
                    assertEscapeSafety
                        (label <> " own omission")
                        [Authority.SourceAxiom, Authority.Omitted]
                        ownOmission
                    assertProofDirectOmitted
                        (label <> " own omission") ownOmission
                batches ->
                    assertFailure
                        (label <> " consumer batch count: "
                            <> show (length batches))
        modules ->
            assertFailure
                (label <> " escape module count: "
                    <> show (length modules))

    assertEscapeSafety label expected batch = do
        fact <- sole (label <> " fact")
            (Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta batch))
        assertEqual (label <> " public escape kinds")
            expected
            (Authority.escapeKindsToList
                (Authority.authoritySafetyEscapeKinds
                    (Authority.factAuthoritySafety
                        (Semantic.semanticFactAuthority fact))))

    assertDeclarationDirect label expected batch = do
        validation <-
            maybe
                (assertFailure (label <> " declaration validation is absent")
                    >> fail "unreachable")
                pure
                (Declaration.committedBatchDeclarationValidation batch)
        certificate <- sole (label <> " declaration certificate")
            (Semantic.declarationValidationRecordCertificates validation)
        assertEqual (label <> " direct authorization")
            expected
            (Authority.validationDirectAuthorization certificate)

    assertProofDirectChecked label expectedCount batch = do
        authorization <- proofDirect label batch
        case authorization of
            Authority.CheckedSourceProof requests ->
                assertEqual (label <> " accepted request count")
                    expectedCount (length requests)
            direct ->
                assertFailure
                    (label <> " has unexpected direct authority: "
                        <> show direct)

    assertProofDirectOmitted label batch = do
        authorization <- proofDirect label batch
        assertEqual (label <> " direct authorization")
            Authority.OmittedAuthorization authorization

    proofDirect label batch = do
        record <- sole (label <> " proof validation")
            (Declaration.committedBatchProofValidations batch)
        pure
            (Authority.validationDirectAuthorization
                (Semantic.proofValidationRecordCertificate record))

rejectsAfterExactOmittedSubclaim :: Assertion
rejectsAfterExactOmittedSubclaim =
    Temp.withSystemTempDirectory "felix-exact-omitted-rollback" \root -> do
        repository <- getCurrentDirectory
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation unusedResolver
        mounts <- exactFixtureMounts repository
        workspace <- parseExactWorkspace
            bootstrap mounts "test/phase5/exact-escape-consumer.tex"
        parsedModules <-
            pure
                (toList
                    (Parse.parsedWorkspaceImportedBeforeImporter workspace))
        (producerParsed, consumerParsed) <-
            case parsedModules of
                [producer, consumer] -> pure (producer, consumer)
                modules ->
                    assertFailure
                        ("unexpected rollback graph size: "
                            <> show (length modules))
                        >> fail "unreachable"
        producerInput <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                unusedResolver
                Declaration.FreshValidation
                producerParsed
                [])
        producer <- Module.runTypedModule producerInput >>= \case
            Module.TypedModuleSucceeded sealed -> pure sealed
            _ ->
                assertFailure "escape producer did not seal"
                    >> fail "unreachable"
        let executable = root Posix.</> "vampire"
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for omitted-rollback'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        calls <- newIORef (0 :: Int)
        let resolver = Declaration.vampireResolver \prepared -> do
                runCount <- readIORef calls
                modifyIORef' calls (+ 1)
                if runCount < 4
                    then
                        runNoLoggingT
                            (Provers.runPreparedTypedProver
                                (Provers.vampire
                                    executable
                                    Provers.defaultTimeLimit
                                    Provers.defaultMemoryLimit)
                                prepared)
                    else
                        pure
                            (Right
                                (Provers.CounterSatisfiable
                                    "rejected continuation"))
        consumerInput <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                resolver
                Declaration.FreshValidation
                consumerParsed
                [producer])
        Module.runTypedModule consumerInput >>= \case
            Module.TypedModuleFailed
                    (Module.TypedDeclarationFailed
                        (Declaration.ProofObligationFailedAt
                            location
                            Declaration.VampireObligationRejected{}))
                    prefix -> do
                assertEqual "the continuation is the fifth request"
                    5
                    =<< readIORef calls
                assertEqual "rejected continuation location"
                    37 (locLine location)
                assertEqual "omitted declaration rolls back atomically"
                    3
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Module.TypedModuleSucceeded{} ->
                assertFailure "rejected omitted continuation was accepted"
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    ("omitted rollback module did not open: "
                        <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    ("unexpected omitted rollback failure: "
                        <> show failure)

reusesExactProofValidationAcrossModuleMisses :: Assertion
reusesExactProofValidationAcrossModuleMisses =
    Temp.withSystemTempDirectory "felix-exact-proof-cache" \root -> do
        let relative = "test/phase5/exact-proofs.tex"
            producerRelative = "test/phase5/exact-producer.tex"
            sourcePath = root Posix.</> relative
            producerPath = root Posix.</> producerRelative
            executable = root Posix.</> "vampire"
            storePath = root Posix.</> "store.sqlite"
        createDirectoryIfMissing True (Posix.takeDirectory sourcePath)
        original <- ByteString.readFile relative
        producer <- ByteString.readFile producerRelative
        ByteString.writeFile sourcePath original
        ByteString.writeFile producerPath producer
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for exact-cache'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation
                    unusedResolver
        mounts <- exactFixtureMounts root
        freshWorkspace <- parseExactWorkspace bootstrap mounts relative
        freshRuns <- newIORef (0 :: Int)
        freshModules <-
            compileParsedWorkspaceWithValidation
                foundation bootstrap
                (countingAcceptedResolver executable freshRuns)
                Declaration.FreshValidation
                freshWorkspace
        assertEqual "fresh proof obligations run Vampire"
            7
            =<< readIORef freshRuns
        freshRoot <- sole "fresh exact proof root" (drop 1 freshModules)
        bracket
            (snd <$> (Store.openStore storePath
                (Identity.theoryId foundation) >>= expectRight))
            Store.closeStore
            \store -> do
                traverse_
                    (expectRightIO
                        . Store.writePendingModulePrefix store
                        . Module.sealedTypedModulePrefix)
                    freshModules
                let validation =
                        Declaration.WarmValidation
                            (Declaration.validationLookup
                                (expectRightIO
                                    . Store.loadProofValidation store)
                                (expectRightIO
                                    . Store.loadDeclarationValidation store))
                    compileWarm workspace = do
                        runs <- newIORef (0 :: Int)
                        modules <-
                            compileParsedWorkspaceWithValidation
                                foundation bootstrap
                                (countingAcceptedResolver executable runs)
                                validation
                                workspace
                        rootModule <- sole "warm exact proof root" (drop 1 modules)
                        runCount <- readIORef runs
                        pure (rootModule, runCount)
                (unchangedRoot, unchangedRuns) <-
                    compileWarm freshWorkspace
                assertEqual "exact warm hit skips Vampire"
                    0 unchangedRuns
                assertEqual "exact warm hit preserves public semantics"
                    (Module.sealedTypedModuleSemantic freshRoot)
                    (Module.sealedTypedModuleSemantic unchangedRoot)

                let formattingOnly =
                        Text.encodeUtf8
                            (StrictText.replace
                                "\\begin{proposition}\\label{phase5_structural_proof}"
                                ("% shifted source location\n"
                                    <> "\\begin{proposition}\\label{phase5_structural_proof}")
                                (Text.decodeUtf8 original))
                ByteString.writeFile sourcePath formattingOnly
                formattedWorkspace <-
                    parseExactWorkspace bootstrap mounts relative
                assertBool "formatting changes parsed module identity"
                    (Parse.parsedModuleId
                        (Parse.parsedWorkspaceRootModule freshWorkspace)
                        /= Parse.parsedModuleId
                            (Parse.parsedWorkspaceRootModule formattedWorkspace))
                (formattedRoot, formattedRuns) <-
                    compileWarm formattedWorkspace
                assertEqual "formatting-only module miss reuses proof validation"
                    0 formattedRuns
                assertEqual "formatting-only miss preserves public semantics"
                    (Module.sealedTypedModuleSemantic freshRoot)
                    (Module.sealedTypedModuleSemantic formattedRoot)

                let semanticEdit =
                        Text.encodeUtf8
                            (StrictText.replace
                                "    We have $x = x$ by assumption."
                                (StrictText.intercalate "\n"
                                    [ "    Show $x = x$."
                                    , "    \\begin{subproof}"
                                    , "        Follows by assumption."
                                    , "    \\end{subproof}"
                                    ])
                                (Text.decodeUtf8 original))
                ByteString.writeFile sourcePath semanticEdit
                editedWorkspace <-
                    parseExactWorkspace bootstrap mounts relative
                (editedRoot, editedRuns) <-
                    compileWarm editedWorkspace
                assertEqual "semantic proof edit reruns its obligations"
                    2 editedRuns
                assertEqual "request-equivalent proof preserves public semantics"
                    (Module.sealedTypedModuleSemantic freshRoot)
                    (Module.sealedTypedModuleSemantic editedRoot)
rejectsFixedSemanticDeclaration :: Assertion
rejectsFixedSemanticDeclaration =
    Temp.withSystemTempDirectory "felix-fixed-semantic" \root -> do
        let relative = "entry.tex"
            path = root Posix.</> relative
            source =
                "\\begin{signature}\\label{source_unions}\n"
                    <> "    $\\unions{X}$ is a set.\n"
                    <> "\\end{signature}\n"
        ByteString.writeFile path
            (Text.encodeUtf8 (StrictText.pack source))
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation unusedResolver
        mounts <- exactFixtureMounts root
        workspace <- parseExactWorkspace bootstrap mounts relative
        let parsed = Parse.parsedWorkspaceRootModule workspace
        input <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                unusedResolver
                Declaration.FreshValidation
                parsed
                [])
        Module.runTypedModule input >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactCompileFailed
                            (Exact.ExactFixedSemanticCollision
                                location key)))
                    prefix -> do
                assertEqual "fixed collision line" 1 (locLine location)
                assertEqual "fixed collision key"
                    (Semantic.SemanticExpressionFunction
                        (Raw.TokenCons (Raw.Command "unions")
                            (Raw.TokenCons Raw.InvisibleBraceL
                                (Raw.HoleCons
                                    (Raw.TokenCons
                                        Raw.InvisibleBraceR Raw.End)))))
                    key
                assertEqual "fixed collision commits no prefix"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Module.TypedModuleSucceeded{} ->
                assertFailure "fixed semantic declaration was accepted"
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    ("fixed semantic module did not open: "
                        <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    ("unexpected fixed semantic failure: "
                        <> show failure)

rejectsFixedSemanticInductive :: Assertion
rejectsFixedSemanticInductive =
    Temp.withSystemTempDirectory "felix-fixed-inductive" \root -> do
        let relative = "entry.tex"
            path = root Posix.</> relative
            source =
                "\\begin{inductive}\\label{source_pow}\n"
                    <> "    Define $\\pow{A}\\subseteq\\cumul{A}$ inductively as follows.\n"
                    <> "    \\begin{enumerate}\n"
                    <> "        \\item $A\\in\\pow{A}$.\n"
                    <> "    \\end{enumerate}\n"
                    <> "\\end{inductive}\n"
        ByteString.writeFile path
            (Text.encodeUtf8 (StrictText.pack source))
        foundation <- expectRight Foundation.checkedFoundation
        bootstrap <-
            expectRight
                =<< Module.buildBootstrapPreludeFixture
                    foundation unusedResolver
        mounts <- exactFixtureMounts root
        workspace <- parseExactWorkspace bootstrap mounts relative
        let parsed = Parse.parsedWorkspaceRootModule workspace
        input <- expectRight
            (Module.typedModuleInput
                foundation
                (Module.bootstrapPreludeReadiness bootstrap)
                unusedResolver
                Declaration.FreshValidation
                parsed
                [])
        Module.runTypedModule input >>= \case
            Module.TypedModuleFailed
                    (Module.TypedActionFailed
                        (Module.TypedExactInductiveFailed
                            (ExactInductive.ExactInductiveFixedSemanticCollision
                                location key)))
                    prefix -> do
                assertEqual "fixed inductive collision line"
                    1
                    (locLine location)
                assertEqual "fixed inductive collision key"
                    (Semantic.SemanticExpressionFunction
                        (Raw.TokenCons (Raw.Command "pow")
                            (Raw.TokenCons Raw.InvisibleBraceL
                                (Raw.HoleCons
                                    (Raw.TokenCons
                                        Raw.InvisibleBraceR Raw.End)))))
                    key
                assertEqual "fixed inductive collision commits no prefix"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Module.TypedModuleSucceeded{} ->
                assertFailure "fixed semantic inductive was accepted"
            Module.TypedModuleOpenFailed failure ->
                assertFailure
                    ("fixed semantic inductive did not open: "
                        <> show failure)
            Module.TypedModuleFailed failure _prefix ->
                assertFailure
                    ("unexpected fixed inductive failure: "
                        <> show failure)

keepsExactSemanticsIndependentOfFixity :: Assertion
keepsExactSemanticsIndependentOfFixity =
    Temp.withSystemTempDirectory "felix-exact-fixity" \root -> do
        let relative = "test/phase5/exact-producer.tex"
            path = root Posix.</> relative
        createDirectoryIfMissing True (Posix.takeDirectory path)
        original <- ByteString.readFile relative
        let changed =
                Text.encodeUtf8
                    (StrictText.replace
                        "infixl 2"
                        "infixr 6"
                        (Text.decodeUtf8 original))
        ByteString.writeFile path original
        first <- compileExactRootAt root relative
        ByteString.writeFile path changed
        second <- compileExactRootAt root relative
        let firstParsed = Parse.parsedWorkspaceRootModule (fst first)
            secondParsed = Parse.parsedWorkspaceRootModule (fst second)
            firstSealed = snd first
            secondSealed = snd second
        assertBool "fixity changes syntax identity"
            (Syntax.moduleSyntaxAssertedId
                (Parse.parsedModuleSyntaxInterface firstParsed)
                /= Syntax.moduleSyntaxAssertedId
                    (Parse.parsedModuleSyntaxInterface secondParsed))
        assertBool "fixity changes parsed identity"
            (Parse.parsedModuleId firstParsed
                /= Parse.parsedModuleId secondParsed)
        assertEqual "fixity preserves semantic interface"
            (Module.sealedTypedModuleSemantic firstSealed)
            (Module.sealedTypedModuleSemantic secondSealed)
        assertEqual "fixity preserves semantic prefix"
            (Declaration.pendingModulePrefixCurrent
                (Module.sealedTypedModulePrefix firstSealed))
            (Declaration.pendingModulePrefixCurrent
                (Module.sealedTypedModulePrefix secondSealed))

loadsCachedExactProducerForFreshImporter :: Assertion
loadsCachedExactProducerForFreshImporter = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-exact-cache" \root -> do
        let path = root Posix.</> "store.sqlite"
            executable = root Posix.</> "vampire"
        writeAcceptedFixtureVampire executable
        (_startup, store) <-
            Store.openStore path (Identity.theoryId foundation)
                >>= expectRight
        let observer = Api.verificationRequestObserver \_ordinal _request ->
                pure ()
            prover =
                Provers.vampire
                    executable
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit
            verify mode source =
                runNoLoggingT
                    (Api.verifyWithObserverAndStoreMode
                        store mode observer prover source)
                    >>= expectRight
        producer <-
            verify Api.FreshStoreValidation
                "test/phase5/exact-producer.tex"
        importer <-
            verify Api.WarmStoreValidation
                "test/phase5/exact-importer.tex"
        assertTypedSuccess "fresh producer" producer
        assertTypedSuccess "warm producer/fresh importer" importer
        memo <- Store.newStoreMemo store
        prelude <-
            expectRight
                =<< Module.acquireFinalPreludeSession
                    memo store foundation unusedResolver
        preludeVisits <- Store.storeMemoVisits memo
        repository <- getCurrentDirectory
        mounts <- exactFixtureMounts repository
        workspace <- parseFinalExactWorkspace
            prelude mounts "test/phase5/exact-importer.tex"
        let parsedModules =
                toList
                    (Parse.parsedWorkspaceImportedBeforeImporter workspace)
            preludeSemantic =
                Module.sealedTypedModuleSemantic
                    (Module.finalPreludeModule prelude)
            preludeId =
                Semantic.semanticInterfaceAssertedId preludeSemantic
            theory = Identity.theoryId foundation
            loadInstallation parsed direct = do
                key <- expectRight
                    (Semantic.moduleArtifactKey
                        (moduleName (Parse.parsedModuleAddress parsed))
                        (Parse.parsedModuleId parsed)
                        direct
                        theory)
                loaded <- expectRight
                    =<< Store.loadCachedModuleInstallation
                        memo
                        store
                        key
                        (Syntax.moduleSyntaxAssertedId
                            (Parse.parsedModuleSyntaxInterface parsed))
                maybe
                    (assertFailure "exact cached installation is absent"
                        >> fail "unreachable")
                    pure
                    loaded
            environmentBindings installation =
                [ binding
                | delta <- Semantic.semanticInterfaceDeclarations
                    (Store.cachedInstallationSemantic installation)
                , binding <- Semantic.semanticEnvironmentBindings
                    (Semantic.declarationDeltaEnvironment delta)
                ]
        case parsedModules of
            [producerParsed, importerParsed] -> do
                producerInstallation <-
                    loadInstallation producerParsed [preludeId]
                producerVisits <- Store.storeMemoVisits memo
                assertEqual "ordinary root adds one artifact validation"
                    (Store.storeArtifactsValidated preludeVisits + 1)
                    (Store.storeArtifactsValidated producerVisits)
                assertEqual "ordinary root reuses prelude syntax validation"
                    (Store.storeSyntaxRowsValidated preludeVisits + 1)
                    (Store.storeSyntaxRowsValidated producerVisits)
                assertEqual "ordinary root reuses prelude semantic validation"
                    (Store.storeSemanticRowsValidated preludeVisits + 1)
                    (Store.storeSemanticRowsValidated producerVisits)
                let producerSemanticId =
                        Semantic.semanticInterfaceAssertedId
                            (Store.cachedInstallationSemantic
                                producerInstallation)
                importerInstallation <-
                    loadInstallation
                        importerParsed [preludeId, producerSemanticId]
                case ( environmentBindings producerInstallation
                     , environmentBindings importerInstallation
                     ) of
                    (seedBinding : aliasBinding : _definitionBinding : [],
                     [importerBinding]) -> do
                        let seedTarget =
                                Semantic.semanticGlobalTargetObject
                                    (Semantic.semanticGlobalBindingTarget
                                        seedBinding)
                            aliasTarget =
                                Semantic.semanticGlobalTargetObject
                                    (Semantic.semanticGlobalBindingTarget
                                        aliasBinding)
                            importerTarget =
                                Semantic.semanticGlobalTargetObject
                                    (Semantic.semanticGlobalBindingTarget
                                        importerBinding)
                        assertEqual "cached importer reuses expanded content"
                            aliasTarget importerTarget
                        assertEqual "cached importer adds no object"
                            []
                            (Store.cachedInstallationObjects
                                importerInstallation)
                        expandedObject <-
                            maybe
                                (assertFailure
                                    "cached expanded object is absent"
                                    >> fail "unreachable")
                                pure
                                (find
                                    ((== aliasTarget)
                                        . Identity.assertedObjectId)
                                    (Store.cachedInstallationObjects
                                        producerInstallation))
                        case Identity.assertedObjectContent expandedObject of
                            Identity.TransparentObjectContent
                                    _identity _coreType body ->
                                assertEqual
                                    "cached expansion retains the opaque seed"
                                    (Set.singleton seedTarget)
                                    (Core.canonicalTermGlobals body)
                            content ->
                                assertFailure
                                    ("cached expansion is not transparent: "
                                        <> show content)
                    (producerBindings, importerBindings) ->
                        assertFailure
                            ("unexpected cached exact bindings: "
                                <> show
                                    ( length producerBindings
                                    , length importerBindings
                                    ))
            modules ->
                assertFailure
                    ("unexpected cached exact module count: "
                        <> show (length modules))
        Store.closeStore store

selectsConcurrentModuleFailureDeterministically :: Assertion
selectsConcurrentModuleFailureDeterministically = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-concurrent-module-failure" \root -> do
        let executable = root Posix.</> "vampire"
            source = "test/phase7/concurrent-failure-root.tex"
            prover =
                Provers.vampire
                    executable
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit
            ignored =
                Api.verificationRequestObserver
                    (\_position _request -> pure ())
            select amount =
                Provers.selectEffectiveJobs
                    (Provers.effectiveJobs amount)
                    (fail "explicit jobs unexpectedly detected processors")
            reportEntry escape =
                ( Api.reportedEscapeKind escape
                , locFile (Api.reportedEscapeLocation escape)
                , locLine (Api.reportedEscapeLocation escape)
                )
            inspect label expectedPositions
                    (result, measurements, positions) = do
                case result of
                    Api.VerificationFailure report failed -> do
                        assertEqual (label <> " selected earlier failure")
                            "test/phase7/concurrent-earlier.tex"
                            (locFile (Api.failedVerificationLocation failed))
                        assertEqual (label <> " admitted source prefix")
                            [ ( Api.ReportedSourceAxiom
                              , "test/phase7/concurrent-earlier.tex"
                              , 1
                              )
                            ]
                            (reportEntry
                                <$> Api.verificationDirectEscapes report)
                    other ->
                        assertFailure
                            (label <> " did not reject deterministically: "
                                <> show other)
                assertEqual (label <> " executed only sibling obligations")
                    expectedPositions
                    (sort
                        [ ( Provers.workPositionModuleOrdinal position
                          , Provers.workPositionLocalRequestOrdinal position
                          )
                        | position <- positions
                        ])
                pure measurements
            runCase label jobsAmount = do
                let storePath = root Posix.</> (label <> ".sqlite")
                    processLock = root Posix.</> (label <> ".process-lock")
                    processStarted =
                        root Posix.</> (label <> ".process-started")
                writeAcceptedFixtureVampire executable
                (_startup, store) <-
                    Store.openStore storePath (Identity.theoryId foundation)
                        >>= expectRight
                bracket (pure store) Store.closeStore \openStore -> do
                    -- Seed only the final prelude.  The unsupported ordinary
                    -- module cannot publish a root.
                    void
                        (runNoLoggingT
                            (Api.verifyMeasuredWithObserverAndStoreMode
                                openStore
                                Api.WarmStoreValidation
                                ignored
                                prover
                                "test/phase3/typed-unsupported.tex")
                            >>= expectRight)
                    writeFile executable
                        (unlines
                            [ "#!/bin/sh"
                            , "while ! mkdir \"" <> processLock
                                <> "\" 2>/dev/null; do sleep 0.01; done"
                            , "trap 'rmdir \"" <> processLock
                                <> "\"' EXIT"
                            , ": > \"" <> processStarted <> "\""
                            , "cat >/dev/null"
                            , "printf '%s\\n' '% SZS status CounterSatisfiable for concurrent-fixture'"
                            ])
                    permissions <- getPermissions executable
                    setPermissions executable
                        (setOwnerExecutable True permissions)
                    positionsRef <- newIORef []
                    let observer =
                            Api.verificationRequestObserver
                                (\position _request -> do
                                    atomicModifyIORef' positionsRef
                                        (\positions ->
                                            (position : positions, ()))
                                    when
                                        (jobsAmount > 1
                                            && Provers.workPositionModuleOrdinal
                                                position == 1)
                                        (waitForFileSignal
                                            "later module process"
                                            processStarted))
                    jobs <- select jobsAmount
                    (result, measurements) <-
                        runNoLoggingT
                            (Api.verifyMeasuredWithObserverAndStoreModeAndJobs
                                openStore
                                Api.WarmStoreValidation
                                jobs
                                observer
                                prover
                                source)
                            >>= expectRight
                    positions <- readIORef positionsRef
                    pure (result, measurements, positions)
        parallel <-
            runCase "parallel" 2
                >>= inspect "parallel" [(1, 1), (2, 1)]
        sequential <-
            runCase "sequential" 1
                >>= inspect "sequential" [(1, 1)]
        assertEqual "parallel module checker bound"
            2
            (Api.verificationMaximumLiveModuleCheckers parallel)
        assertEqual "parallel Vampire bound"
            2
            (Api.verificationMaximumLiveVampireProcesses parallel)
        assertEqual "sequential module checker reference"
            1
            (Api.verificationMaximumLiveModuleCheckers sequential)
        assertEqual "sequential Vampire reference"
            1
            (Api.verificationMaximumLiveVampireProcesses sequential)

waitForFileSignal :: String -> FilePath -> Assertion
waitForFileSignal label path = do
    guarded <- Timeout.timeout 10000000 loop
    case guarded of
        Just () ->
            pure ()
        Nothing ->
            assertFailure (label <> " was not observed")
  where
    loop = do
        exists <- doesFileExist path
        if exists
            then pure ()
            else do
                threadDelay 10000
                loop

batchesStructureObligationsAtomically :: Assertion
batchesStructureObligationsAtomically = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-structure-obligation-batch" \root -> do
        let storePath = root Posix.</> "store.sqlite"
            executable = root Posix.</> "vampire"
            unavailable = root Posix.</> "must-not-run-vampire"
            source = "test/phase7/structure-obligation-batch.tex"
            prover path =
                Provers.vampire
                    path
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit
            select amount =
                Provers.selectEffectiveJobs
                    (Provers.effectiveJobs amount)
                    (fail "explicit jobs unexpectedly detected processors")
            run openStore jobs observer vampireCommand =
                runNoLoggingT
                    (Api.verifyMeasuredWithObserverAndStoreModeAndJobs
                        openStore
                        Api.WarmStoreValidation
                        jobs
                        observer
                        vampireCommand
                        source)
                    >>= expectRight
            inspectFailure label positions (result, measurements) = do
                case result of
                    Api.VerificationFailure report failed -> do
                        assertEqual (label <> " selects first consequence")
                            (source, 12)
                            ( locFile (Api.failedVerificationLocation failed)
                            , locLine (Api.failedVerificationLocation failed)
                            )
                        assertEqual (label <> " retains preceding prefix")
                            [(Api.ReportedSourceAxiom, source, 1)]
                            [ ( Api.reportedEscapeKind escape
                              , locFile (Api.reportedEscapeLocation escape)
                              , locLine (Api.reportedEscapeLocation escape)
                              )
                            | escape <- Api.verificationDirectEscapes report
                            ]
                    other ->
                        assertFailure
                            (label <> " did not reject its structure batch: "
                                <> show other)
                assertEqual (label <> " assigns consecutive positions")
                    [(1, 1), (1, 2)]
                    (sort positions)
                assertEqual (label <> " observes one two-member batch")
                    (1, 2, 2)
                    ( Api.verificationObligationBatchCount measurements
                    , Api.verificationPreparedObligationCount measurements
                    , Api.verificationMaximumObligationBatchSize measurements
                    )
                pure measurements
        writeAcceptedFixtureVampire executable
        (_startup, store) <-
            Store.openStore storePath (Identity.theoryId foundation)
                >>= expectRight
        bracket (pure store) Store.closeStore \openStore -> do
            let ignored =
                    Api.verificationRequestObserver
                        (\_position _request -> pure ())
            -- Seed only the confined prelude so this fixture observes exactly
            -- the ordinary structure module's ready batch.
            void
                (runNoLoggingT
                    (Api.verifyMeasuredWithObserverAndStoreMode
                        openStore
                        Api.WarmStoreValidation
                        ignored
                        (prover executable)
                        "test/phase3/typed-unsupported.tex")
                    >>= expectRight)
            parallelJobs <- select 2
            parallelPositions <- newIORef []
            firstStarted <- newEmptyTMVarIO
            secondStarted <- newEmptyTMVarIO
            releaseFirst <- newEmptyTMVarIO
            let laterCompleted = root Posix.</> "later-completed"
            writeLaterAcceptingVampire executable laterCompleted
            let parallelObserver =
                    Api.verificationRequestObserver \position _request -> do
                        let ordinal =
                                Provers.workPositionLocalRequestOrdinal position
                        atomicModifyIORef' parallelPositions
                            (\positions ->
                                ( ( Provers.workPositionModuleOrdinal position
                                  , ordinal
                                  ) : positions
                                , ()
                                ))
                        case ordinal of
                            1 -> do
                                atomically (putTMVar firstStarted ())
                                atomically (takeTMVar releaseFirst)
                            2 ->
                                atomically (putTMVar secondStarted ())
                            _ ->
                                assertFailure
                                    ("unexpected structure request ordinal: "
                                        <> show ordinal)
            withAsync
                (run openStore parallelJobs parallelObserver
                    (prover executable))
                \verification -> do
                    void
                        (awaitSignal "first structure request"
                            (atomically (takeTMVar firstStarted)))
                    void
                        (awaitSignal "second structure request"
                            (atomically (takeTMVar secondStarted)))
                    -- Only the later member can reach the subprocess while
                    -- the first observer is gated.  Its completed signal
                    -- therefore establishes reversed wall-clock completion.
                    waitForFileSignal
                        "later structure consequence"
                        laterCompleted
                    atomically (putTMVar releaseFirst ())
                    parallelResult <- wait verification
                    positions <- readIORef parallelPositions
                    parallelMeasurements <-
                        inspectFailure "parallel"
                            positions parallelResult
                    assertEqual "parallel obligations overlap"
                        2
                        (Api.verificationMaximumLiveVampireProcesses
                            parallelMeasurements)

            sequentialJobs <- select 1
            sequentialPositions <- newIORef []
            let sequentialCompleted = root Posix.</> "sequential-completed"
            writeRejectingVampire executable sequentialCompleted
            let sequentialObserver =
                    Api.verificationRequestObserver \position _request ->
                        atomicModifyIORef' sequentialPositions
                            (\positions ->
                                ( ( Provers.workPositionModuleOrdinal position
                                  , Provers.workPositionLocalRequestOrdinal
                                        position
                                  ) : positions
                                , ()
                                ))
            sequentialResult <-
                run openStore sequentialJobs sequentialObserver
                    (prover executable)
            sequentialObserved <- readIORef sequentialPositions
            sequentialMeasurements <-
                inspectFailure "sequential"
                    sequentialObserved sequentialResult
            assertEqual "sequential batch is the semantic reference"
                1
                (Api.verificationMaximumLiveVampireProcesses
                    sequentialMeasurements)

            -- A rejected sibling wrote neither validation nor a module root:
            -- the complete batch executes again, while the earlier source
            -- axiom remains the admitted prefix.  A subsequent hit executes
            -- no request at all.
            writeAcceptedFixtureVampire executable
            acceptedPositions <- newIORef []
            let acceptedObserver =
                    Api.verificationRequestObserver \position _request ->
                        modifyIORef' acceptedPositions
                            (position :)
            (accepted, acceptedMeasurements) <-
                run openStore parallelJobs acceptedObserver
                    (prover executable)
            case accepted of
                Api.VerificationCompleted report _presentation ->
                    assertEqual "successful retry retains only source axiom"
                        [Api.ReportedSourceAxiom]
                        (Api.reportedEscapeKind
                            <$> Api.verificationDirectEscapes report)
                other ->
                    assertFailure
                        ("successful structure retry failed: " <> show other)
            acceptedObserved <- readIORef acceptedPositions
            assertEqual "successful retry executes the complete batch"
                2
                (length acceptedObserved)
            assertEqual "failed declaration published no root"
                (1, 1)
                ( Api.verificationModuleRootHitCount acceptedMeasurements
                , Api.verificationModuleRootMissCount acceptedMeasurements
                )
            let forbiddenObserver =
                    Api.verificationRequestObserver \position _request ->
                        assertFailure
                            ("warm structure batch invoked Vampire at "
                                <> show position)
            (warm, warmMeasurements) <-
                run openStore parallelJobs forbiddenObserver
                    (prover unavailable)
            case warm of
                Api.VerificationCompleted{} -> pure ()
                other ->
                    assertFailure
                        ("warm structure batch did not install: " <> show other)
            assertEqual "warm module hit executes no batch"
                (2, 0, 0)
                ( Api.verificationModuleRootHitCount warmMeasurements
                , Api.verificationModuleRootMissCount warmMeasurements
                , Api.verificationVampireRunCount warmMeasurements
                )
  where
    awaitSignal label action = do
        result <- Timeout.timeout 10000000 action
        maybe
            (assertFailure (label <> " was not observed")
                >> fail "unreachable")
            pure
            result

    writeRejectingVampire executable completed = do
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , ": > \"" <> completed <> "\""
                , "printf '%s\\n' '% SZS status CounterSatisfiable for structure-batch-fixture'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)

    writeLaterAcceptingVampire executable completed = do
        let firstProcess = completed <> ".first-process"
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , ": > \"" <> completed <> "\""
                , "if mkdir \"" <> firstProcess <> "\" 2>/dev/null; then"
                , "  printf '%s\\n' '% SZS status Theorem for structure-batch-fixture'"
                , "else"
                , "  printf '%s\\n' '% SZS status CounterSatisfiable for structure-batch-fixture'"
                , "fi"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)

speculatesDependentProofObligationsWithoutAdmittingAhead :: Assertion
speculatesDependentProofObligationsWithoutAdmittingAhead = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-dependent-proof-chain" \root -> do
        let executable = root Posix.</> "vampire"
            unavailable = root Posix.</> "must-not-run-vampire"
            storePath = root Posix.</> "store.sqlite"
            source = "test/phase7/dependent-proof-chain.tex"
            prover path =
                Provers.vampire
                    path
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit
            ignored =
                Api.verificationRequestObserver
                    (\_position _request -> pure ())
        writeAcceptedFixtureVampire executable
        (_startup, store) <-
            Store.openStore storePath (Identity.theoryId foundation)
                >>= expectRight
        bracket (pure store) Store.closeStore \openStore -> do
            -- Seed only the final prelude so the observed work belongs to the
            -- ordinary proof module.
            void
                (runNoLoggingT
                    (Api.verifyMeasuredWithObserverAndStoreMode
                        openStore
                        Api.WarmStoreValidation
                        ignored
                        (prover executable)
                        "test/phase3/typed-unsupported.tex")
                    >>= expectRight)
            jobs <-
                Provers.selectEffectiveJobs
                    (Provers.effectiveJobs 2)
                    (fail "explicit jobs unexpectedly detected processors")
            firstStarted <- newEmptyTMVarIO
            secondStarted <- newEmptyTMVarIO
            releaseFirst <- newEmptyTMVarIO
            positionsRef <- newIORef []
            let observer =
                    Api.verificationRequestObserver \position _request -> do
                        let ordinal =
                                Provers.workPositionLocalRequestOrdinal position
                        atomicModifyIORef' positionsRef
                            (\positions ->
                                ( ( Provers.workPositionModuleOrdinal position
                                  , ordinal
                                  ) : positions
                                , ()
                                ))
                        case ordinal of
                            1 -> do
                                atomically (putTMVar firstStarted ())
                                atomically (takeTMVar releaseFirst)
                            2 -> atomically (putTMVar secondStarted ())
                            _ ->
                                assertFailure
                                    ("unexpected dependent proof request: "
                                        <> show ordinal)
            withAsync
                (runNoLoggingT
                    (Api.verifyMeasuredWithObserverAndStoreModeAndJobs
                        openStore
                        Api.WarmStoreValidation
                        jobs
                        observer
                        (prover executable)
                        source)
                    >>= expectRight)
                \checking -> do
                    void
                        (awaitSignal "local subclaim request"
                            (atomically (takeTMVar firstStarted)))
                    -- The continuation is semantically dependent, but its
                    -- already checked request may execute prospectively.  It
                    -- cannot be admitted until the local claim succeeds.
                    void
                        (awaitSignal "dependent continuation request"
                            (atomically (takeTMVar secondStarted)))
                    atomically (putTMVar releaseFirst ())
                    (result, measurements) <- wait checking
                    case result of
                        Api.VerificationCompleted report _presentation ->
                            assertEqual "only the preceding axiom is reported"
                                [Api.ReportedSourceAxiom]
                                (Api.reportedEscapeKind
                                    <$> Api.verificationDirectEscapes report)
                        other ->
                            assertFailure
                                ("dependent proof module did not seal: "
                                    <> show other)
                    assertEqual "dependent proof obligations overlap"
                        2
                        (Api.verificationMaximumLiveVampireProcesses
                            measurements)
            positions <- readIORef positionsRef
            assertEqual "dependent requests retain source positions"
                [(1, 1), (1, 2)]
                (sort positions)

            let forbiddenObserver =
                    Api.verificationRequestObserver \position _request ->
                        assertFailure
                            ("warm dependent proof invoked Vampire at "
                                <> show position)
            (warm, warmMeasurements) <-
                runNoLoggingT
                    (Api.verifyMeasuredWithObserverAndStoreModeAndJobs
                        openStore
                        Api.WarmStoreValidation
                        jobs
                        forbiddenObserver
                        (prover unavailable)
                        source)
                    >>= expectRight
            case warm of
                Api.VerificationCompleted{} -> pure ()
                other ->
                    assertFailure
                        ("warm dependent proof did not install: " <> show other)
            assertEqual "warm plan executes no live request"
                0
                (Api.verificationVampireRunCount warmMeasurements)
  where
    awaitSignal label action = do
        result <- Timeout.timeout 10000000 action
        maybe
            (assertFailure (label <> " was not observed")
                >> fail "unreachable")
            pure
            result

schedulesDiamondAfterSealedImports :: Assertion
schedulesDiamondAfterSealedImports = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-concurrent-diamond" \root -> do
        let storePath = root Posix.</> "store.sqlite"
            executable = root Posix.</> "vampire"
            unavailable = root Posix.</> "must-not-run-vampire"
            source = "test/phase7/diamond-root.tex"
            prover path =
                Provers.vampire
                    path
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit
            ignored =
                Api.verificationRequestObserver
                    (\_position _request -> pure ())
        writeAcceptedFixtureVampire executable
        (_startup, store) <-
            Store.openStore storePath (Identity.theoryId foundation)
                >>= expectRight
        bracket (pure store) Store.closeStore \openStore -> do
            -- Acquire the final prelude before introducing scheduler gates.
            void
                (runNoLoggingT
                    (Api.verifyMeasuredWithObserverAndStoreMode
                        openStore
                        Api.WarmStoreValidation
                        ignored
                        (prover executable)
                        "test/phase3/typed-unsupported.tex")
                    >>= expectRight)
            jobs <- Provers.selectEffectiveJobs
                (Provers.effectiveJobs 2)
                (fail "explicit jobs unexpectedly detected processors")
            baseStarted <- newEmptyTMVarIO
            branchStarted <- newTQueueIO
            rootStarted <- newEmptyTMVarIO
            releaseBase <- newTVarIO False
            releaseBranches <- newTVarIO False
            let awaitRelease released =
                    atomically (readTVar released >>= check)
                observer =
                    Api.verificationRequestObserver
                        (\position _request ->
                            case Provers.workPositionModuleOrdinal position of
                                1 -> do
                                    atomically (putTMVar baseStarted ())
                                    awaitRelease releaseBase
                                ordinal@2 -> do
                                    atomically
                                        (writeTQueue branchStarted ordinal)
                                    awaitRelease releaseBranches
                                ordinal@3 -> do
                                    atomically
                                        (writeTQueue branchStarted ordinal)
                                    awaitRelease releaseBranches
                                4 ->
                                    atomically (putTMVar rootStarted ())
                                _ ->
                                    pure ())
                verify vampireCommand requestObserver =
                    runNoLoggingT
                        (Api.verifyMeasuredWithObserverAndStoreModeAndJobs
                            openStore
                            Api.WarmStoreValidation
                            jobs
                            requestObserver
                            vampireCommand
                            source)
                        >>= expectRight
                await label action = do
                    result <- Timeout.timeout 10000000 action
                    maybe
                        (assertFailure (label <> " was not observed")
                            >> fail "unreachable")
                        pure
                        result
            withAsync (verify (prover executable) observer) \verification -> do
                void (await "base request" (atomically (takeTMVar baseStarted)))
                threadDelay 50000
                atomically (tryReadTQueue branchStarted) >>= \case
                    Nothing -> pure ()
                    Just ordinal ->
                        assertFailure
                            ("dependent module started before base seal: "
                                <> show ordinal)
                atomically (writeTVar releaseBase True)
                firstBranch <- await "first branch"
                    (atomically (readTQueue branchStarted))
                secondBranch <- await "second branch"
                    (atomically (readTQueue branchStarted))
                assertEqual "both diamond branches became ready together"
                    [2, 3]
                    (sort [firstBranch, secondBranch])
                atomically (tryReadTMVar rootStarted) >>= \case
                    Nothing -> pure ()
                    Just () ->
                        assertFailure
                            "diamond root started before both branch seals"
                atomically (writeTVar releaseBranches True)
                void (await "diamond root" (atomically (takeTMVar rootStarted)))
                (coldResult, coldMeasurements) <- wait verification
                case coldResult of
                    Api.VerificationCompleted{} -> pure ()
                    other ->
                        assertFailure
                            ("cold diamond did not complete: " <> show other)
                assertEqual "cold diamond module misses plus prelude hit"
                    (1, 4)
                    ( Api.verificationModuleRootHitCount coldMeasurements
                    , Api.verificationModuleRootMissCount coldMeasurements
                    )
            let forbiddenObserver =
                    Api.verificationRequestObserver
                        (\position _request ->
                            assertFailure
                                ("warm diamond invoked Vampire at "
                                    <> show position))
            (warmResult, warmMeasurements) <-
                verify (prover unavailable) forbiddenObserver
            case warmResult of
                Api.VerificationCompleted{} -> pure ()
                other ->
                    assertFailure
                        ("warm diamond did not install: " <> show other)
            assertEqual "warm diamond installs each distinct root"
                (5, 0)
                ( Api.verificationModuleRootHitCount warmMeasurements
                , Api.verificationModuleRootMissCount warmMeasurements
                )
            assertEqual "warm diamond runs no prover"
                0
                (Api.verificationVampireRunCount warmMeasurements)

reportsAdmittedSourceEscapes :: Assertion
reportsAdmittedSourceEscapes = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-admitted-source-report" \root -> do
        let storePath = root Posix.</> "store.sqlite"
            executable = root Posix.</> "vampire"
            unavailable = root Posix.</> "must-not-run-vampire"
            observer =
                Api.verificationRequestObserver \_ordinal _request -> pure ()
            prover path =
                Provers.vampire
                    path
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit
        writeAcceptedFixtureVampire executable
        (_startup, store) <-
            Store.openStore storePath (Identity.theoryId foundation)
                >>= expectRight
        bracket (pure store) Store.closeStore \openStore -> do
            let verify mode vampirePath source =
                    runNoLoggingT
                        (Api.verifyMeasuredWithObserverAndStoreMode
                            openStore
                            mode
                            observer
                            (prover vampirePath)
                            source)
                        >>= expectRight
                reportEntries =
                    fmap
                        (\escape ->
                            ( Api.reportedEscapeKind escape
                            , locFile (Api.reportedEscapeLocation escape)
                            , locLine (Api.reportedEscapeLocation escape)
                            ))
                        . Api.verificationDirectEscapes
                expectedConsumer =
                    [ ( Api.ReportedSourceAxiom
                      , "test/phase5/exact-escape-producer.tex"
                      , 1
                      )
                    , ( Api.ReportedOmitted
                      , "test/phase5/exact-escape-producer.tex"
                      , 9
                      )
                    , ( Api.ReportedOmitted
                      , "test/phase5/exact-escape-consumer.tex"
                      , 35
                      )
                    ]
            (freshResult, freshMeasurements) <-
                verify
                    Api.FreshStoreValidation
                    executable
                    "test/phase5/exact-escape-consumer.tex"
            freshReport <- case freshResult of
                Api.CompletedWithExplicitGaps report _presentation -> pure report
                other ->
                    assertFailure
                        ("fresh escape report did not complete with gaps: "
                            <> show other)
                        >> fail "unreachable"
            assertEqual "fresh direct escapes"
                expectedConsumer
                (reportEntries freshReport)
            assertEqual "cold acquisition includes prelude and two modules"
                (0, 3)
                ( Api.verificationModuleRootHitCount freshMeasurements
                , Api.verificationModuleRootMissCount freshMeasurements
                )

            (warmResult, warmMeasurements) <-
                verify
                    Api.WarmStoreValidation
                    unavailable
                    "test/phase5/exact-escape-consumer.tex"
            warmReport <- case warmResult of
                Api.CompletedWithExplicitGaps report _presentation -> pure report
                other ->
                    assertFailure
                        ("warm escape report did not complete with gaps: "
                            <> show other)
                        >> fail "unreachable"
            assertEqual "warm report uses rebound current locations"
                freshReport warmReport
            assertEqual "warm acquisition includes prelude and two modules"
                (3, 0)
                ( Api.verificationModuleRootHitCount warmMeasurements
                , Api.verificationModuleRootMissCount warmMeasurements
                )
            assertEqual "warm root hit invokes no Vampire process"
                0
                (Api.verificationVampireRunCount warmMeasurements)

            void
                (verify
                    Api.FreshStoreValidation
                    executable
                    "test/phase5/exact-source-axiom.tex")
            (failedResult, failedMeasurements) <-
                verify
                    Api.WarmStoreValidation
                    unavailable
                    "test/phase6/admitted-prefix-failure.tex"
            failedReport <- case failedResult of
                Api.VerificationCheckingFailure report _failure -> pure report
                other ->
                    assertFailure
                        ("typed suffix failure was not report-bearing: "
                            <> show other)
                        >> fail "unreachable"
            assertEqual "failure report retains only admitted source prefix"
                (take 2 expectedConsumer
                    <> [ ( Api.ReportedOmitted
                         , "test/phase6/admitted-prefix-failure.tex"
                         , 7
                         )
                       ])
                (reportEntries failedReport)
            assertEqual "failed root is not counted as acquired"
                (2, 0)
                ( Api.verificationModuleRootHitCount failedMeasurements
                , Api.verificationModuleRootMissCount failedMeasurements
                )
            assertEqual "cached prefix failure invokes no Vampire process"
                0
                (Api.verificationVampireRunCount failedMeasurements)

classifiesTypedVampireFailures :: Assertion
classifiesTypedVampireFailures = do
    foundation <- expectRight Foundation.checkedFoundation
    Temp.withSystemTempDirectory "felix-typed-failure-classification" \root -> do
        let storePath = root Posix.</> "store.sqlite"
            executable = root Posix.</> "vampire"
            observer =
                Api.verificationRequestObserver \_ordinal _request -> pure ()
            prover =
                Provers.vampire
                    executable
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit
        writeAcceptedFixtureVampire executable
        (_startup, store) <-
            Store.openStore storePath (Identity.theoryId foundation)
                >>= expectRight
        bracket (pure store) Store.closeStore \openStore -> do
            let verify source =
                    runNoLoggingT
                        (Api.verifyMeasuredWithObserverAndStoreMode
                            openStore
                            Api.WarmStoreValidation
                            observer
                            prover
                            source)
                        >>= expectRight
                writeProtocol lines = do
                    writeFile executable
                        (unlines (["#!/bin/sh", "cat >/dev/null"] <> lines))
                    permissions <- getPermissions executable
                    setPermissions executable
                        (setOwnerExecutable True permissions)
                expectTypedFailure classify = do
                    (result, _measurements) <-
                        verify "test/phase5/exact-runtime-failure.tex"
                    case result of
                        Api.VerificationFailure report failed -> do
                            assertEqual "typed failure has no direct escapes"
                                []
                                (Api.verificationDirectEscapes report)
                            assertEqual "typed failure retains source location"
                                "test/phase5/exact-runtime-failure.tex"
                                (locFile
                                    (Api.failedVerificationLocation failed))
                            classify
                                (Api.failedVerificationReason failed)
                                (CommandLine.verificationCommandOutcome result)
                        other ->
                            assertFailure
                                ("typed prover outcome was misclassified: "
                                    <> show other)

            -- Populate only the confined prelude.  The selected ordinary
            -- module then remains a miss for each classified live failure.
            (_preludeResult, _preludeMeasurements) <-
                verify "test/phase3/typed-unsupported.tex"

            writeProtocol
                [ "printf '%s\\n' '% SZS status CounterSatisfiable for typed-failure'"
                , "exit 0"
                ]
            expectTypedFailure \reason outcome -> do
                case reason of
                    Api.CountermodelFailure{} -> pure ()
                    other -> assertFailure ("expected countermodel: " <> show other)
                case outcome of
                    CommandLine.VerificationRejected{} -> pure ()
                    other -> assertFailure ("expected rejection: " <> show other)

            writeProtocol
                [ "printf '%s\\n' '% SZS status Timeout for typed-failure'"
                , "exit 0"
                ]
            expectTypedFailure \reason outcome -> do
                case reason of
                    Api.IndeterminateFailure{} -> pure ()
                    other -> assertFailure ("expected indeterminate result: " <> show other)
                case outcome of
                    CommandLine.ProverFailed
                            _report _location CommandLine.ProverIndeterminate{} ->
                        pure ()
                    other -> assertFailure ("expected prover failure: " <> show other)

            writeProtocol
                [ "printf '%s\\n' '% SZS status Theorem for typed-failure'"
                , "exit 7"
                ]
            expectTypedFailure \reason outcome -> do
                case reason of
                    Api.ProtocolFailure{} -> pure ()
                    other -> assertFailure ("expected protocol failure: " <> show other)
                case outcome of
                    CommandLine.ProverFailed
                            _report _location CommandLine.ProverProtocolFailure{} ->
                        pure ()
                    other -> assertFailure ("expected prover failure: " <> show other)

            writeFile executable "not executable"
            permissions <- getPermissions executable
            setPermissions executable
                (setOwnerExecutable False permissions)
            expectTypedFailure \reason outcome -> do
                case reason of
                    Api.TransportFailure{} -> pure ()
                    other -> assertFailure ("expected transport failure: " <> show other)
                case outcome of
                    CommandLine.ProverFailed
                            _report _location CommandLine.ProverTransportFailure{} ->
                        pure ()
                    other -> assertFailure ("expected prover failure: " <> show other)

retainsExactPrefixBeforeFailure :: Assertion
retainsExactPrefixBeforeFailure = do
    result <-
        withAcceptedFixtureVampire "felix-exact-failure" \prover ->
            runNoLoggingT
                (Api.verifyMeasured
                    prover
                    "test/phase5/exact-failure.tex")
    case result of
        Right
            ( Api.VerificationCheckingFailure _report
                (Api.VerificationTypedModuleError
                source
                (Module.TypedActionFailed
                    (Module.TypedExactCompileFailed
                        (Exact.ExactUnsupportedDeclarationBody location)))
                prefix)
            , _measurements
            ) -> do
            assertEqual "failed exact source"
                "test/phase5/exact-failure.tex"
                (safeRelativePathFilePath
                    (resolvedSourceRelativePath source))
            assertEqual "unsupported declaration line" 5 (locLine location)
            assertEqual "earlier exact declaration remains committed"
                1
                (length (Declaration.pendingModulePrefixBatches prefix))
        Left err ->
            assertFailure ("unexpected exact failure: " <> show err)
        Right{} ->
            assertFailure "unsupported declaration was admitted"

    proofFailure <-
        withAcceptedFixtureVampire "felix-exact-proof-failure" \prover ->
            runNoLoggingT
                (Api.verifyMeasured
                    prover
                    "test/phase5/exact-proof-failure.tex")
    case proofFailure of
        Right
            ( Api.VerificationCheckingFailure _report
                (Api.VerificationTypedModuleError
                _source
                (Module.TypedActionFailed
                    (Module.TypedExactProofFailed
                        (ExactProof.ExactProofGoalStatementMismatch
                            location)))
                prefix)
            , _measurements
            ) -> do
            assertEqual "mismatched assumption line" 10 (locLine location)
            assertEqual "failed proof publishes no theorem"
                1
                (length (Declaration.pendingModulePrefixBatches prefix))
        Left err ->
            assertFailure
                ("unexpected exact proof failure: " <> show err)
        Right{} ->
            assertFailure "mismatched exact proof was admitted"

    unmatched <-
        withAcceptedFixtureVampire "felix-unmatched-proof" \prover ->
            runNoLoggingT
                (Api.verifyMeasured
                    prover
                    "test/phase5/unmatched-proof.tex")
    case unmatched of
        Right
            ( Api.VerificationCheckingFailure _report
                (Api.VerificationTypedModuleError
                _source
                (Module.TypedActionFailed
                    (Module.TypedUnmatchedProof location))
                prefix)
            , _measurements
            ) -> do
            assertEqual "unmatched proof line" 1 (locLine location)
            assertEqual "unmatched proof publishes no declaration"
                0
                (length (Declaration.pendingModulePrefixBatches prefix))
        Left err ->
            assertFailure
                ("unexpected unmatched-proof failure: " <> show err)
        Right{} ->
            assertFailure "unmatched proof was admitted"

    runtimeFailure <-
        Temp.withSystemTempDirectory "felix-runtime-proof-failure" \root -> do
            foundation <- expectRight Foundation.checkedFoundation
            bootstrap <-
                expectRight
                    =<< Module.buildBootstrapPreludeFixture
                        foundation
                        unusedResolver
            repository <- getCurrentDirectory
            mounts <- exactFixtureMounts repository
            workspace <- parseExactWorkspace
                bootstrap mounts "test/phase5/exact-runtime-failure.tex"
            let executable = root Posix.</> "vampire"
            writeFile executable
                (unlines
                    [ "#!/bin/sh"
                    , "cat >/dev/null"
                    , "printf '%s\\n' '% SZS status Theorem for located-proof'"
                    ])
            permissions <- getPermissions executable
            setPermissions executable
                (setOwnerExecutable True permissions)
            runs <- newIORef (0 :: Int)
            let resolver = Declaration.vampireResolver \prepared -> do
                    runNumber <- readIORef runs
                    modifyIORef' runs (+ 1)
                    if runNumber == 0
                        then
                            runNoLoggingT
                                (Provers.runPreparedTypedProver
                                    (Provers.vampire
                                        executable
                                        Provers.defaultTimeLimit
                                        Provers.defaultMemoryLimit)
                                    prepared)
                        else
                            pure
                                (Right
                                    (Provers.CounterSatisfiable
                                        "later exact obligation"))
                parsed = Parse.parsedWorkspaceRootModule workspace
            input <- expectRight
                (Module.typedModuleInput
                    foundation
                    (Module.bootstrapPreludeReadiness bootstrap)
                    resolver
                    Declaration.FreshValidation
                    parsed
                    [])
            Module.runTypedModule input
    case runtimeFailure of
        Module.TypedModuleFailed
                failure@(Module.TypedDeclarationFailed
                    (Declaration.ProofObligationFailedAt
                        location
                        Declaration.VampireObligationRejected{}))
                prefix -> do
            assertEqual "later rejected obligation line"
                11
                (locLine location)
            assertEqual "typed failure retains obligation location"
                (Just location)
                (Module.typedModuleFailureLocation failure)
            assertEqual "runtime proof failure publishes no theorem"
                1
                (length (Declaration.pendingModulePrefixBatches prefix))
        _result ->
            assertFailure "unexpected runtime proof failure"

rejectsNestedExactSetInduction :: Assertion
rejectsNestedExactSetInduction = do
    result <-
        withAcceptedFixtureVampire "felix-nested-set-induction" \prover ->
            runNoLoggingT
                (Api.verifyMeasured
                    prover
                    "test/phase5/exact-induction-nested.tex")
    case result of
        Right
            ( Api.VerificationCheckingFailure _report
                (Api.VerificationTypedModuleError
                _source
                (Module.TypedActionFailed
                    (Module.TypedExactProofFailed
                        (ExactProof.ExactProofSetInductionNotOutermost
                            location)))
                prefix)
            , _measurements
            ) -> do
            assertEqual "nested induction line" 7 (locLine location)
            assertBool "failed proof publishes no theorem"
                (null (Declaration.pendingModulePrefixBatches prefix))
        Left err ->
            assertFailure
                ("unexpected nested-induction failure: " <> show err)
        Right{} ->
            assertFailure "nested exact set induction was admitted"

routesProductionVerification :: Assertion
routesProductionVerification =
    Temp.withSystemTempDirectory "felix-production-route" \directory -> do
        let executable = directory Posix.</> "vampire"
            counter = directory Posix.</> "runs"
        writeFile executable
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' run >> " <> show counter
                , "printf '%s\\n' '% SZS status Theorem for production-route'"
                ])
        permissions <- getPermissions executable
        setPermissions executable
            (setOwnerExecutable True permissions)
        producer <- verifyFixture executable "test/phase3/typed-producer.tex"
        assertTypedSuccess "exact producer" producer
        selectedRuns <- runCount counter
        assertBool "ordinary roots construct the final prelude"
            (selectedRuns > 0)
        importer <- verifyFixture executable "test/phase3/typed-importer.tex"
        assertTypedSuccess "ordinary importer" importer
        assertBool "every root constructs the final prelude"
            . (> selectedRuns)
            =<< runCount counter
  where
    verifyFixture executable path =
        fst
            <$> (runNoLoggingT
                (Api.verifyMeasured
                    (Provers.vampire
                        executable
                        Provers.defaultTimeLimit
                        Provers.defaultMemoryLimit)
                    path)
                >>= expectRight)

    runCount path =
        length . StrictText.lines . StrictText.pack <$> readFile path

installsNonemptyImplicitPreludeEvidence :: Assertion
installsNonemptyImplicitPreludeEvidence = do
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation
                unusedResolver
    closure <- expectRight
        (Identity.validateObjectClosure
            (Identity.theoryId foundation)
            [])
    proposition <- expectRight
        (Identity.validatePropositionContent closure Core.CFalsum)
    preludeDriver <- Declaration.runModuleDriver
        foundation
        preludeModuleName
        []
        unusedResolver
        Declaration.FreshValidation
        do
            Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "nonempty-prelude") do
                    candidate <- Declaration.reserveCandidate
                        (Declaration.candidateSpec
                            proposition
                            Semantic.SearchEligible
                            [Semantic.semanticName "prelude-fact"])
                    Declaration.authorizeSourceAxiomCandidate candidate
    preludeResult <- expectRight preludeDriver
    (preludeSemantic, preludePrefix) <-
        case preludeResult of
            Declaration.DriverSucceeded _value semantic prefix _closure ->
                pure (semantic, prefix)
            _ ->
                assertFailure "nonempty prelude fixture did not seal"
                    >> fail "unreachable"
    preludeFingerprint <-
        case concatMap
                Semantic.declarationDeltaFacts
                (Semantic.semanticInterfaceDeclarations preludeSemantic) of
            [occurrence] ->
                pure (Semantic.semanticFactFingerprint occurrence)
            facts ->
                assertFailure
                    ("unexpected prelude fact count: "
                        <> show (length facts))
                    >> fail "unreachable"
    let preludeSyntax =
            Module.sealedTypedModuleSyntax
                (Module.bootstrapPreludeModule bootstrap)
    nonemptyPrelude <-
        Temp.withSystemTempDirectory "felix-nonempty-prelude" \directory -> do
            let path = directory Posix.</> "store.sqlite"
                theory = Identity.theoryId foundation
                parsed =
                    Module.identifiedModuleParsed
                        (Module.bootstrapPreludeInput bootstrap)
            (_startup, store) <-
                Store.openStore path theory >>= expectRight
            artifactKey <- expectRight
                (Semantic.moduleArtifactKey
                    preludeModuleName
                    (Parse.identifiedParsedModuleId parsed)
                    []
                    theory)
            let artifact =
                    Semantic.moduleArtifactResult
                        artifactKey
                        (Syntax.moduleSyntaxAssertedId preludeSyntax)
                        (Semantic.semanticInterfaceAssertedId
                            preludeSemantic)
            _ <- expectRight
                =<< Store.writeSealedModule
                    store
                    preludePrefix
                    [preludeSyntax]
                    [preludeSemantic]
                    artifact
            memo <- Store.newStoreMemo store
            loaded <- expectRight
                =<< Store.loadCachedModuleInstallation
                    memo
                    store
                    artifactKey
                    (Syntax.moduleSyntaxAssertedId preludeSyntax)
            installation <- maybe
                (assertFailure "nonempty prelude was not installed"
                    >> fail "unreachable")
                pure
                loaded
            sealed <- expectRight
                (Module.cachedSealedTypedModule
                    foundation
                    []
                    installation)
            Store.closeStore store
            pure sealed

    root <- getCurrentDirectory
    mounts <-
        expectRight
            =<< prepareSourceMounts
                [ (sourceMountId "project", root)
                , (sourceMountId "library", root Posix.</> "library")
                , (sourceMountId "debug", root Posix.</> "debug")
                ]
    request <- expectRight
        (searchedRoot "test/phase3/typed-producer.tex")
    workspace <-
        fst
            <$> (expectRight
                =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs
                    mounts
                    request
                    (const [preludeSyntax]))
    let parsed = Parse.parsedWorkspaceRootModule workspace
    input <- expectRight
        (Module.typedModuleInput
            foundation
            (Module.fixtureFinalPreludeReadinessFromSealed nonemptyPrelude)
            unusedResolver
            Declaration.FreshValidation
            parsed
            [])
    ordinary <- Module.runTypedModule input >>= \case
        Module.TypedModuleSucceeded sealed -> pure sealed
        _ ->
            assertFailure "ordinary module rejected the nonempty prelude"
                >> fail "unreachable"

    consumerDigest <- expectRight
        (hashCanonicalFields
            "implicit-prelude-consumer"
            ["consumer"])
    consumerPath <- expectRight (safeRelativePath "consumer.tex")
    let consumerOwner =
            moduleNameFromParts
                (sourceNamespaceIdFromDigest consumerDigest)
                consumerPath
    consumed <- Declaration.runModuleDriver
        foundation
        consumerOwner
        [Semantic.semanticInterfaceAssertedId
            (Module.sealedTypedModuleSemantic ordinary)]
        unusedResolver
        Declaration.FreshValidation
        do
            Declaration.importSealedModuleDriver
                (Module.sealedTypedModuleEvidence ordinary)
            Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "use-implicit-prelude") do
                    candidate <- Declaration.reserveCandidate
                        (Declaration.candidateSpec
                            proposition
                            Semantic.SearchIneligible
                            [])
                    Declaration.authorizeOmittedCandidate candidate do
                        void
                            (Declaration.useAuthorizedFact
                                preludeFingerprint)
                        Declaration.recordOmittedUse
    consumedResult <- expectRight consumed
    case consumedResult of
        Declaration.DriverSucceeded{} -> pure ()
        _ ->
            assertFailure
                "implicit prelude fact was not transitively visible"

unusedResolver :: Declaration.VampireResolver
unusedResolver =
    Declaration.vampireResolver \_prepared ->
        fail "empty bootstrap invoked Vampire"

writeAcceptedFixtureVampire :: FilePath -> IO ()
writeAcceptedFixtureVampire executable = do
    writeFile executable
        (unlines
            [ "#!/bin/sh"
            , "cat >/dev/null"
            , "printf '%s\\n' '% SZS status Theorem for typed-fixture'"
            ])
    permissions <- getPermissions executable
    setPermissions executable
        (setOwnerExecutable True permissions)

withAcceptedFixtureVampire
    :: String
    -> (Provers.Vampire -> IO value)
    -> IO value
withAcceptedFixtureVampire label action =
    Temp.withSystemTempDirectory label \directory -> do
        let executable = directory Posix.</> "vampire"
        writeAcceptedFixtureVampire executable
        action
            (Provers.vampire
                executable
                Provers.defaultTimeLimit
                Provers.defaultMemoryLimit)

finalPreludeResolver :: Declaration.VampireResolver
finalPreludeResolver =
    Declaration.vampireResolver \prepared ->
        runNoLoggingT
            (Provers.runPreparedTypedProver
                (Provers.vampire
                    "vampire"
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit)
                prepared)

countingAcceptedResolver
    :: FilePath
    -> IORef Int
    -> Declaration.VampireResolver
countingAcceptedResolver executable runs =
    Declaration.vampireResolver \prepared -> do
        modifyIORef' runs (+ 1)
        runNoLoggingT
            (Provers.runPreparedTypedProver
                (Provers.vampire
                    executable
                    Provers.defaultTimeLimit
                    Provers.defaultMemoryLimit)
                prepared)

prepareExactInductiveFixture
    :: FilePath
    -> IO
        (Either
            ExactInductive.ExactInductiveError
            ExactInductive.PreparedExactInductive)
prepareExactInductiveFixture relative = do
    root <- getCurrentDirectory
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation
                unusedResolver
    mounts <- exactFixtureMounts root
    workspace <- parseExactWorkspace bootstrap mounts relative
    parsed <-
        sole "exact inductive parsed module"
            (toList
                (Parse.parsedWorkspaceImportedBeforeImporter workspace))
    let identified = Module.identifiedPhysicalModule parsed
        owner = Module.identifiedModuleOwner identified
        parsedModule = Module.identifiedModuleParsed identified
    block <-
        sole "exact inductive block"
            (Parse.identifiedParsedModuleBlocks parsedModule)
    let entries =
            [ Parse.parsedSyntaxOccurrenceEntry occurrence
            | occurrence <-
                Parse.identifiedParsedModuleSyntaxOccurrences parsedModule
            , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == 0
            ]
        action
            :: Declaration.ModuleDriver Void
                (Either
                    ExactInductive.ExactInductiveError
                    ExactInductive.PreparedExactInductive)
        action =
            Declaration.runProspectiveLoweringDriver
                (ExactInductive.prepareExactInductive
                    foundation
                    block
                    entries)
    result <-
        Declaration.runModuleDriver
            foundation
            owner
            []
            unusedResolver
            Declaration.FreshValidation
            action
    driver <- expectRight result
    case driver of
        Declaration.DriverSucceeded prepared _semantic _prefix _closure ->
            pure prepared
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("exact inductive preparation driver failed: "
                    <> show failure)
                >> fail "unreachable"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("exact inductive preparation driver did not seal: "
                    <> show failure)
                >> fail "unreachable"

prepareExactDatatypeFixture
    :: FilePath
    -> IO
        (Either
            ExactDatatype.ExactDatatypeError
            ( Foundation.CheckedFoundation
            , ModuleName
            , ExactDatatype.PreparedExactDatatype
            ))
prepareExactDatatypeFixture relative = do
    root <- getCurrentDirectory
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation
                unusedResolver
    mounts <- exactFixtureMounts root
    workspace <- parseExactWorkspace bootstrap mounts relative
    parsed <-
        sole "exact datatype parsed module"
            (toList
                (Parse.parsedWorkspaceImportedBeforeImporter workspace))
    let identified = Module.identifiedPhysicalModule parsed
        owner = Module.identifiedModuleOwner identified
        parsedModule = Module.identifiedModuleParsed identified
    block <-
        sole "exact datatype block"
            (Parse.identifiedParsedModuleBlocks parsedModule)
    let occurrences =
            [ ( Parse.parsedSyntaxOccurrenceLocation occurrence
              , Parse.parsedSyntaxOccurrenceMarker occurrence
              , Parse.parsedSyntaxOccurrenceEntry occurrence
              )
            | occurrence <-
                Parse.identifiedParsedModuleSyntaxOccurrences parsedModule
            , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == 0
            ]
        action
            :: Declaration.ModuleDriver Void
                (Either
                    ExactDatatype.ExactDatatypeError
                    ExactDatatype.PreparedExactDatatype)
        action =
            Declaration.runProspectiveLoweringDriver
                (ExactDatatype.prepareExactDatatype block occurrences)
    result <-
        Declaration.runModuleDriver
            foundation
            owner
            []
            unusedResolver
            Declaration.FreshValidation
            action
    driver <- expectRight result
    case driver of
        Declaration.DriverSucceeded prepared _semantic _prefix _closure ->
            pure
                ((\datatype -> (foundation, owner, datatype))
                    <$> prepared)
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("exact datatype preparation driver failed: "
                    <> show failure)
                >> fail "unreachable"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("exact datatype preparation driver did not seal: "
                    <> show failure)
                >> fail "unreachable"

compileExactFixture
    :: FilePath
    -> IO
        ( Foundation.CheckedFoundation
        , Module.BootstrapPreludeFixture
        , Parse.ParsedSourceWorkspace
        , [Module.SealedTypedModule]
        )
compileExactFixture relative = do
    root <- getCurrentDirectory
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation
                unusedResolver
    mounts <- exactFixtureMounts root
    workspace <- parseExactWorkspace bootstrap mounts relative
    sealed <- compileParsedWorkspace foundation bootstrap workspace
    pure (foundation, bootstrap, workspace, sealed)

compileExactRootAt
    :: FilePath
    -> FilePath
    -> IO (Parse.ParsedSourceWorkspace, Module.SealedTypedModule)
compileExactRootAt projectRoot relative = do
    foundation <- expectRight Foundation.checkedFoundation
    bootstrap <-
        expectRight
            =<< Module.buildBootstrapPreludeFixture
                foundation
                unusedResolver
    mounts <- exactFixtureMounts projectRoot
    workspace <- parseExactWorkspace bootstrap mounts relative
    sealed <- compileParsedWorkspace foundation bootstrap workspace
    rootModule <- sole "exact root module" (reverse sealed)
    pure (workspace, rootModule)

exactFixtureMounts :: FilePath -> IO SourceMounts
exactFixtureMounts projectRoot = do
    repository <- getCurrentDirectory
    expectRight
        =<< prepareSourceMounts
            [ (sourceMountId "project", projectRoot)
            , (sourceMountId "library", repository Posix.</> "library")
            , (sourceMountId "debug", repository Posix.</> "debug")
            ]

parseExactWorkspace
    :: Module.BootstrapPreludeFixture
    -> SourceMounts
    -> FilePath
    -> IO Parse.ParsedSourceWorkspace
parseExactWorkspace bootstrap mounts relative =
    parseExactWorkspaceWithPrelude
        (Module.bootstrapPreludeModule bootstrap)
        mounts
        relative

parseFinalExactWorkspace
    :: Module.FinalPreludeSession
    -> SourceMounts
    -> FilePath
    -> IO Parse.ParsedSourceWorkspace
parseFinalExactWorkspace prelude mounts relative =
    parseExactWorkspaceWithPrelude
        (Module.finalPreludeModule prelude)
        mounts
        relative

parseExactWorkspaceWithPrelude
    :: Module.SealedTypedModule
    -> SourceMounts
    -> FilePath
    -> IO Parse.ParsedSourceWorkspace
parseExactWorkspaceWithPrelude prelude mounts relative = do
    request <- expectRight (searchedRoot relative)
    let preludeSyntax =
            Module.sealedTypedModuleSyntax
                prelude
    fst
        <$> (expectRight
            =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs
                mounts
                request
                (const [preludeSyntax]))

compileParsedWorkspace
    :: Foundation.CheckedFoundation
    -> Module.BootstrapPreludeFixture
    -> Parse.ParsedSourceWorkspace
    -> IO [Module.SealedTypedModule]
compileParsedWorkspace foundation bootstrap workspace =
    compileParsedWorkspaceWithResolver
        foundation
        bootstrap
        unusedResolver
        workspace

compileParsedWorkspaceWithResolver
    :: Foundation.CheckedFoundation
    -> Module.BootstrapPreludeFixture
    -> Declaration.VampireResolver
    -> Parse.ParsedSourceWorkspace
    -> IO [Module.SealedTypedModule]
compileParsedWorkspaceWithResolver foundation bootstrap resolver workspace =
    compileParsedWorkspaceWithValidation
        foundation
        bootstrap
        resolver
        Declaration.FreshValidation
        workspace

compileParsedWorkspaceWithValidation
    :: Foundation.CheckedFoundation
    -> Module.BootstrapPreludeFixture
    -> Declaration.VampireResolver
    -> Declaration.ValidationRun
    -> Parse.ParsedSourceWorkspace
    -> IO [Module.SealedTypedModule]
compileParsedWorkspaceWithValidation
        foundation bootstrap resolver validation workspace =
    compileParsedWorkspaceWithReadiness
        foundation
        (Module.bootstrapPreludeReadiness bootstrap)
        resolver
        validation
        workspace

compileFinalParsedWorkspaceWithResolver
    :: Foundation.CheckedFoundation
    -> Module.FinalPreludeSession
    -> Declaration.VampireResolver
    -> Parse.ParsedSourceWorkspace
    -> IO [Module.SealedTypedModule]
compileFinalParsedWorkspaceWithResolver foundation prelude resolver workspace =
    compileParsedWorkspaceWithReadiness
        foundation
        (Module.finalPreludeReadiness prelude)
        resolver
        Declaration.FreshValidation
        workspace

compileParsedWorkspaceWithReadiness
    :: Foundation.CheckedFoundation
    -> Module.FinalPreludeReadiness
    -> Declaration.VampireResolver
    -> Declaration.ValidationRun
    -> Parse.ParsedSourceWorkspace
    -> IO [Module.SealedTypedModule]
compileParsedWorkspaceWithReadiness
        foundation readiness resolver validation workspace =
    snd
        <$> foldM
            compileOne
            (Map.empty, [])
            (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace))
  where
    compileOne (admitted, ordered) parsed = do
        direct <-
            traverse
                (\address ->
                    maybe
                        (assertFailure
                            ("missing exact direct module: " <> show address)
                            >> fail "unreachable")
                        pure
                        (Map.lookup address admitted))
                (nubOrd
                    (Parse.parsedImportedAddress
                        <$> Parse.parsedModuleImports parsed))
        input <-
            expectRight
                (Module.typedModuleInput
                    foundation
                    readiness
                    resolver
                    validation
                    parsed
                    direct)
        sealed <-
            Module.runTypedModule input >>= \case
                Module.TypedModuleSucceeded module' -> pure module'
                Module.TypedModuleOpenFailed failure ->
                    assertFailure
                        ("exact module did not open: " <> show failure)
                        >> fail "unreachable"
                Module.TypedModuleFailed failure _prefix ->
                    assertFailure
                        ("exact module did not seal: " <> show failure)
                        >> fail "unreachable"
        pure
            ( Map.insert (Parse.parsedModuleAddress parsed) sealed admitted
            , ordered <> [sealed]
            )

assertTypedSuccess :: String -> Api.VerificationResult -> Assertion
assertTypedSuccess label = \case
    Api.VerificationCompleted _report _presentation ->
        pure ()
    Api.CompletedWithExplicitGaps _report _presentation ->
        assertFailure (label <> " completed with gaps")
    Api.VerificationFailure _report failure ->
        assertFailure (label <> " failed: " <> show failure)
    Api.VerificationCheckingFailure _report failure ->
        assertFailure (label <> " failed: " <> show failure)

sole :: String -> [value] -> IO value
sole label = \case
    [value] -> pure value
    values ->
        assertFailure
            (label <> ": expected one value, found " <> show (length values))
            >> fail "unreachable"

expectRight :: Show error => Either error value -> IO value
expectRight = \case
    Left err -> assertFailure (show err) >> fail "unreachable"
    Right value -> pure value

expectRightIO :: Show error => IO (Either error value) -> IO value
expectRightIO action =
    action >>= expectRight

acquireFinalPreludeSession
    :: Store.Store
    -> Foundation.CheckedFoundation
    -> Declaration.VampireResolver
    -> IO
        (Either
            Module.FinalPreludeReadinessError
            Module.FinalPreludeSession)
acquireFinalPreludeSession store foundation resolver = do
    memo <- Store.newStoreMemo store
    Module.acquireFinalPreludeSession
        memo store foundation resolver