{-# LANGUAGE NoImplicitPrelude #-}

module Felix.Test.Unit.Declaration (unitTests) where

import Base
import Felix.Checking.Authority qualified as Authority
import Felix.Checking.Backend.Problem qualified as Backend
import Felix.Checking.Core qualified as Core
import Felix.Checking.Declaration qualified as Declaration
import Felix.Checking.Foundation qualified as Foundation
import Felix.Checking.Exact qualified as Exact
import Felix.Checking.Exact.Vocabulary qualified as Vocabulary
import Felix.Checking.Identity qualified as Identity
import Felix.Checking.Kernel.Derivation qualified as Kernel
import Felix.Checking.SetConstruction qualified as SetConstruction
import Felix.Checking.Semantic qualified as Semantic
import Felix.Checking.Typed.Inductive qualified as Typed
import Felix.Math.Codec
import Felix.Module
import Felix.Source
import Felix.Store qualified as Store
import Felix.Meaning qualified as Meaning
import Felix.Provers qualified as Provers
import Felix.Report.Location
import Felix.Syntax.Abstract qualified as Raw
import Felix.Syntax.Interface qualified as Syntax
import Felix.Syntax.Internal qualified as Internal
import Felix.Syntax.Lexicon qualified as Lexicon

import Data.List.NonEmpty qualified as NonEmpty
import Data.IORef qualified as IORef
import Data.Set qualified as Set
import Data.Text qualified as Text
import Data.Text.Encoding qualified as TextEncoding
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)
import Control.Exception (bracket)
import Control.Exception qualified as Exception
import Control.Monad.Except (runExceptT)
import Control.Monad.State (evalState)
import System.Directory qualified as Directory
import System.FilePath.Posix qualified as Posix
import Test.Tasty
import Test.Tasty.HUnit


unitTests :: TestTree
unitTests =
    testGroup "Typed declaration seam"
        [ testCase "enforces staged candidate order"
            enforcesStagedCandidateOrder
        , testCase "retains only appended declaration prefixes"
            retainsOnlyAppendedPrefixes
        , testCase "makes declaration failures terminal"
            makesDeclarationFailuresTerminal
        , testCase "propagates unsafe authority through local claims"
            propagatesUnsafeAuthorityThroughLocalClaims
        , testCase "aggregates exact Vampire obligations"
            aggregatesExactVampireObligations
        , testCase "validates complete resolver batches before rejection"
            validatesCompleteResolverBatchesBeforeRejection
        , testCase "rejects retained-plan admission drift fatally"
            rejectsRetainedPlanAdmissionDrift
        , testCase "preserves source-axiom safety through Vampire validation"
            preservesSourceAxiomSafetyThroughVampireValidation
        , testCase "materializes a sealed import with fresh authority"
            materializesSealedImport
        , testCase "reconstructs exact imported global bindings"
            reconstructsImportedGlobalBindings
        , testCase "elaborates scoped exact propositions"
            elaboratesScopedExactPropositions
        , testCase "lowers fixed equality aliases without global support"
            lowersFixedEqualityAliases
        , testCase "scopes quantified proposition terms"
            scopesQuantifiedPropositionTerms
        , testCase "prepares exact claim envelopes"
            preparesExactClaimEnvelopes
        , testCase "lowers exact separation comprehensions"
            lowersExactSeparationComprehensions
        , testCase "lowers exact replacement telescopes"
            lowersExactReplacementTelescopes
        , testCase "lowers exact finite sets"
            lowersExactFiniteSets
        , testCase "lowers exact ordinary declarations"
            lowersExactOrdinaryDeclarations
        , testCase "folds transitive and diamond import evidence"
            foldsTransitiveAndDiamondEvidence
        , testCase "validates exact kernel construction descriptors"
            validatesExactKernelConstructionDescriptors
        , testCase "authorizes exact datatype compilation families"
            authorizesExactDatatypeCompilationFamilies
        , testCase "reuses exact compiled declaration validation"
            reusesExactCompiledDeclarationValidation
        , testCase "keeps fatal validation lookup failures out of declarations"
            keepsFatalValidationLookupFailuresOutOfDeclarations
        ]

data FatalValidationLookup = FatalValidationLookup
    deriving (Show)

instance Exception.Exception FatalValidationLookup

keepsFatalValidationLookupFailuresOutOfDeclarations :: Assertion
keepsFatalValidationLookupFailuresOutOfDeclarations = do
    fixture <- makeFixture
    prepared <- makePreparedObligation
        fixture
        Foundation.EmptyCharacteristic
    let lookup = proofOnlyValidationLookup
            (const (Exception.throwIO FatalValidationLookup))
        action = Declaration.commitProofDeclaration
            (Semantic.proofSyntaxId "fatal-validation-lookup") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "fatal-validation-lookup")
                Declaration.authorizeVampireCandidate candidate
                    (Declaration.acceptVampireObligation prepared)
    result <- Exception.try
        (runDriverWithValidation fixture lookup action)
        :: IO
            (Either
                FatalValidationLookup
                (Declaration.DriverResult
                    Void
                    ((), Declaration.CommittedDeclarationBatch)))
    case result of
        Left FatalValidationLookup -> pure ()
        Right _ ->
            assertFailure "fatal validation lookup became a driver result"

enforcesStagedCandidateOrder :: Assertion
enforcesStagedCandidateOrder = do
    fixture <- makeFixture
    accepted <- runSuccessful fixture do
        result <- Declaration.commitCompiledDeclaration
            (Semantic.declarationSyntaxId "staged-success") do
                first <- Declaration.reserveCandidate
                    (factSpec fixture "first")
                later <- Declaration.reserveCandidateBatch
                    ( factSpec fixture "later-a"
                    :| [factSpec fixture "later-b"]
                    )
                Declaration.authorizeCompiledDeclaration do
                    Declaration.authorizeSourceAxiomCandidate first
                    traverse_
                        (\candidate ->
                            Declaration.authorizeKernelProofCandidate
                                candidate do
                                    premise <-
                                        Declaration.useStagedCandidate first
                                    pure
                                        (Kernel.importedFactDerivation premise))
                        later
        pure result
    let (_value, batch) = accepted
    assertEqual
        "all source-ordered candidates appended"
        3
        (length
            (Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta batch)))

    provenance <- runDriver fixture (priorDeclarationUse fixture)
    case provenance of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    (Declaration.CandidateOutsideDeclaration slot))
                prefix -> do
            assertEqual
                "cross-declaration staged premise"
                (localFact fixture 0)
                slot
            assertSingleCompletedPrefix prefix
        _other ->
            assertFailure
                "cross-declaration staged provenance was not rejected"

    traverse_
        (\(label, action, expectedPremise, expectedCandidate) -> do
            result <- runDriver fixture action
            case result of
                Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                    (Declaration.StagedPremiseNotEarlier
                        premiseSlot premiseStage
                        candidateSlot candidateStage))
                    _prefix -> do
                    assertEqual (label <> " premise slot")
                        expectedPremise premiseSlot
                    assertEqual (label <> " candidate slot")
                        expectedCandidate candidateSlot
                    assertBool (label <> " rejected non-earlier stage")
                        (premiseStage >= candidateStage)
                Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed other)
                    _prefix ->
                    assertFailure
                        (label <> ": unexpected error " <> show other)
                Declaration.DriverFailed
                    (Declaration.DriverActionFailed _failure)
                    _prefix ->
                    assertFailure
                        (label <> ": unexpected ordinary driver failure")
                Declaration.DriverSucceeded{} ->
                    assertFailure (label <> ": invalid staged use succeeded")
                Declaration.DriverSealFailed{} ->
                    assertFailure (label <> ": invalid staged use reached sealing"))
        [ ( "self"
          , selfUse fixture
          , localFact fixture 0
          , localFact fixture 0
          )
        , ( "same stage"
          , sameStageUse fixture
          , localFact fixture 1
          , localFact fixture 0
          )
        , ( "forward"
          , forwardUse fixture
          , localFact fixture 1
          , localFact fixture 0
          )
        ]
  where
    localFact fixture ordinal =
        Semantic.factSlot
            (fixtureOwner fixture)
            (localFactOrdinal ordinal)

    selfUse fixture =
        Declaration.commitCompiledDeclaration
            (Semantic.declarationSyntaxId "self") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "self")
                Declaration.authorizeCompiledDeclaration
                    (Declaration.authorizeKernelProofCandidate candidate do
                        premise <- Declaration.useStagedCandidate candidate
                        pure (Kernel.importedFactDerivation premise))

    sameStageUse fixture =
        Declaration.commitCompiledDeclaration
            (Semantic.declarationSyntaxId "same-stage") do
                candidates <- Declaration.reserveCandidateBatch
                    ( factSpec fixture "same-a"
                    :| [factSpec fixture "same-b"]
                    )
                let first = NonEmpty.head candidates
                    second = NonEmpty.last candidates
                Declaration.authorizeCompiledDeclaration
                    (Declaration.authorizeKernelProofCandidate first do
                        premise <- Declaration.useStagedCandidate second
                        pure (Kernel.importedFactDerivation premise))

    forwardUse fixture =
        Declaration.commitCompiledDeclaration
            (Semantic.declarationSyntaxId "forward") do
                first <- Declaration.reserveCandidate
                    (factSpec fixture "forward-a")
                second <- Declaration.reserveCandidate
                    (factSpec fixture "forward-b")
                Declaration.authorizeCompiledDeclaration
                    (Declaration.authorizeKernelProofCandidate first do
                        premise <- Declaration.useStagedCandidate second
                        pure (Kernel.importedFactDerivation premise))

    priorDeclarationUse fixture = do
        (premise, _batch) <- Declaration.commitCompiledDeclaration
            (Semantic.declarationSyntaxId "prior-stage") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "prior-stage")
                Declaration.authorizeCompiledDeclaration
                    (Declaration.authorizeSourceAxiomCandidate candidate)
                pure candidate
        void
            (Declaration.commitCompiledDeclaration
                (Semantic.declarationSyntaxId "later-stage") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "later-stage")
                    Declaration.authorizeCompiledDeclaration
                        (Declaration.authorizeKernelProofCandidate candidate do
                            imported <-
                                Declaration.useStagedCandidate premise
                            pure (Kernel.importedFactDerivation imported)))

retainsOnlyAppendedPrefixes :: Assertion
retainsOnlyAppendedPrefixes = do
    fixture <- makeFixture
    outcome <- runDriver fixture do
        (_value, _firstBatch) <- Declaration.commitProofDeclaration
            (Semantic.proofSyntaxId "accepted") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "accepted")
                Declaration.authorizeSourceAxiomCandidate candidate
        Declaration.failModuleDriver
            ("later checker failure" :: Text)
    case outcome of
        Declaration.DriverFailed
                (Declaration.DriverActionFailed reason) prefix -> do
            assertEqual
                "driver reports the later ordinary failure"
                "later checker failure"
                reason
            assertSingleCompletedPrefix prefix
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed err) _prefix ->
            assertFailure
                ("unexpected declaration failure: " <> show err)
        Declaration.DriverSucceeded{} ->
            assertFailure "ordinary driver failure was lost"
        Declaration.DriverSealFailed{} ->
            assertFailure "ordinary driver failure became a seal failure"

makesDeclarationFailuresTerminal :: Assertion
makesDeclarationFailuresTerminal = do
    fixture <- makeFixture
    outcome <- runDriver fixture do
        void
            (Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "accepted-before-failure") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "accepted-before-failure")
                    Declaration.authorizeSourceAxiomCandidate candidate)
        void
            (Declaration.commitCompiledDeclaration
                (Semantic.declarationSyntaxId "rolled-back") do
                    void
                        (Declaration.reserveCandidate
                            (factSpec fixture "uncommitted")))
        -- This declaration must be unreachable after the terminal failure.
        void
            (Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "must-not-publish") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "must-not-publish")
                    Declaration.authorizeSourceAxiomCandidate candidate)
    case outcome of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    Declaration.DeclarationHasUnauthorizedCandidates)
                prefix ->
            assertSingleCompletedPrefix prefix
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed other) _prefix ->
            assertFailure
                ("unexpected declaration failure: " <> show other)
        Declaration.DriverFailed
                (Declaration.DriverActionFailed _failure) _prefix ->
            assertFailure "unexpected ordinary driver failure"
        Declaration.DriverSucceeded{} ->
            assertFailure "failed declaration was skipped"
        Declaration.DriverSealFailed{} ->
            assertFailure "failed declaration reached sealing"

assertSingleCompletedPrefix
    :: Declaration.PendingModulePrefix
    -> Assertion
assertSingleCompletedPrefix prefix = do
    let batches =
            Declaration.pendingModulePrefixBatches prefix
    assertEqual "one completed envelope survives" 1 (length batches)
    case batches of
        [batch] -> do
            let expected =
                    Declaration.committedBatchNextPrefix batch
            assertEqual
                "failed declaration did not advance the prefix"
                expected
                (Declaration.pendingModulePrefixCurrent prefix)
            assertEqual
                "retained envelope ends at the exposed prefix"
                expected
                (Declaration.committedBatchNextPrefix batch)
        _ -> pure ()

propagatesUnsafeAuthorityThroughLocalClaims :: Assertion
propagatesUnsafeAuthorityThroughLocalClaims = do
    fixture <- makeFixture
    result <- runSuccessful fixture do
        (_sourceValue, sourceBatch) <- Declaration.commitProofDeclaration
            (Semantic.proofSyntaxId "source-axiom") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "source")
                Declaration.authorizeSourceAxiomCandidate candidate
        sourceOccurrence <- requireSingleOccurrence sourceBatch
        let
            sourceFingerprint =
                Semantic.semanticFactFingerprint sourceOccurrence
        (_derivedValue, derivedBatch) <- Declaration.commitProofDeclaration
            (Semantic.proofSyntaxId "local-claim") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "derived")
                Declaration.authorizeKernelProofCandidate candidate do
                    sourcePremise <-
                        Declaration.useAuthorizedFact sourceFingerprint
                    claim <- Declaration.proveLocalKernelClaim
                        (fixtureProposition fixture)
                        (Kernel.importedFactDerivation sourcePremise)
                    claimPremise <- Declaration.useLocalClaim claim
                    pure (Kernel.importedFactDerivation claimPremise)
        pure derivedBatch
    occurrence <-
        case Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta result) of
            [single] -> pure single
            facts ->
                assertFailure
                    ("unexpected fact count: " <> show (length facts))
                    >> fail "unreachable"
    let authority = Semantic.semanticFactAuthority occurrence
    assertEqual
        "local claim cannot erase source-axiom safety"
        (Authority.authoritySafety
            (Authority.singletonEscapeKind Authority.SourceAxiom))
        (Authority.factAuthoritySafety authority)
    case Declaration.committedBatchProofValidations result of
        [record] ->
            assertEqual
                "local support is absent from the compact direct authorization"
                (Authority.CheckedSourceProof [])
                (Authority.validationDirectAuthorization
                    (Semantic.proofValidationRecordCertificate record))
        records ->
            assertFailure
                ("unexpected proof validation count: "
                    <> show (length records))

aggregatesExactVampireObligations :: Assertion
aggregatesExactVampireObligations =
    withTemporaryDirectory "felix-declaration-vampire" \root -> do
        fixture <- makeFixture
        let executable = root Posix.</> "vampire"
        writeAcceptedVampire executable
        first <- makePreparedObligation
            fixture
            Foundation.EmptyCharacteristic
        second <- makePreparedObligation
            fixture
            Foundation.PairSetCharacteristic
        let exactResolver = acceptedResolver executable
        freshOutcome <-
            (runDriverWithResolver fixture exactResolver do
                (_value, committed) <- Declaration.commitProofDeclaration
                    (Semantic.proofSyntaxId "two-vampire-obligations") do
                        candidate <- Declaration.reserveCandidate
                            (factSpec fixture "two-vampire-obligations")
                        Declaration.authorizeVampireCandidate candidate do
                            Declaration.acceptVampireObligation first
                            Declaration.acceptVampireObligation second
                pure committed
                :: IO
                    (Declaration.DriverResult Text
                        Declaration.CommittedDeclarationBatch))
        (batch, freshPrefix) <-
            case freshOutcome of
                Declaration.DriverSucceeded value _ prefix _closure ->
                    pure (value, prefix)
                Declaration.DriverFailed failure _ ->
                    assertFailure
                        ("fresh Vampire fixture failed: " <> show failure)
                        >> fail "unreachable"
                Declaration.DriverSealFailed failure _ ->
                    assertFailure
                        ("fresh Vampire fixture did not seal: "
                            <> show failure)
                        >> fail "unreachable"
        let expectedRequests =
                Provers.preparedVerificationRequestId
                    (Provers.preparedTypedProverRequest first)
                : [Provers.preparedVerificationRequestId
                    (Provers.preparedTypedProverRequest second)]
        case Declaration.committedBatchProofValidations batch of
            [record] ->
                assertEqual
                    "accepted requests retain source order"
                    (Authority.CheckedSourceProof expectedRequests)
                    (Authority.validationDirectAuthorization
                        (Semantic.proofValidationRecordCertificate record))
            records ->
                assertFailure
                    ("unexpected proof validation count: "
                        <> show (length records))

        cachedRecord <-
            case Declaration.committedBatchProofValidations batch of
                [record] -> pure record
                records ->
                    assertFailure
                        ("unexpected cached proof records: "
                            <> show (length records))
                    >> fail "unreachable"
        cachedLookupKey <- IORef.newIORef Nothing
        cached <- runSuccessfulWithValidation fixture
            (proofOnlyValidationLookup
                (\key -> do
                    IORef.writeIORef cachedLookupKey (Just key)
                    pure (Just cachedRecord))) do
            (_value, committed) <- Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "two-vampire-obligations") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "two-vampire-obligations")
                    Declaration.authorizeVampireCandidate candidate do
                        Declaration.acceptVampireObligation first
                        Declaration.acceptVampireObligation second
            pure committed
        publishedRecord <-
            case Declaration.committedBatchProofValidations cached of
                [record] -> pure record
                records ->
                    assertFailure
                        ("unexpected cached validation records: "
                            <> show (length records))
                        >> fail "unreachable"
        assertEqual
            "cached authorization preserves the exact direct proof"
            (Authority.CheckedSourceProof expectedRequests)
            (Authority.validationDirectAuthorization
                (Semantic.proofValidationRecordCertificate publishedRecord))
        assertEqual
            "lookup and publication retain the same validation key"
            (Semantic.proofValidationRecordKey cachedRecord)
            (Semantic.proofValidationRecordKey publishedRecord)
        assertEqual
            "one proof syntax key governs lookup and publication"
            (Just
                (Semantic.proofValidationRecordKey cachedRecord))
            =<< IORef.readIORef cachedLookupKey

        missLookups <- IORef.newIORef (0 :: Int)
        missRuns <- IORef.newIORef (0 :: Int)
        let missLookup = proofOnlyValidationLookup \_key -> do
                IORef.modifyIORef' missLookups (+ 1)
                pure Nothing
            missResolver = Declaration.vampireResolver \prepared -> do
                IORef.modifyIORef' missRuns (+ 1)
                resolveAccepted executable prepared
        miss <- runDriverWithValidationAndResolver
            fixture
            missLookup
            missResolver
            do
                (_value, committed) <- Declaration.commitProofDeclaration
                    (Semantic.proofSyntaxId "two-vampire-obligations") do
                        candidate <- Declaration.reserveCandidate
                            (factSpec fixture "two-vampire-obligations")
                        Declaration.authorizeVampireCandidate candidate do
                            Declaration.acceptVampireObligation first
                            Declaration.acceptVampireObligation second
                pure committed
        case miss of
            Declaration.DriverSucceeded{} -> pure ()
            _ ->
                assertFailure "warm miss failed"
        assertEqual "warm miss performs one exact lookup"
            1
            =<< IORef.readIORef missLookups
        assertEqual "warm miss runs every reached Vampire request"
            2
            =<< IORef.readIORef missRuns

        mismatchRuns <- IORef.newIORef (0 :: Int)
        let editedSyntax =
                Semantic.proofSyntaxId "edited-proof-syntax"
            cachedCertificate =
                Semantic.proofValidationRecordCertificate cachedRecord
            corruptedKey =
                Semantic.proofValidationKey
                    (Identity.theoremId
                        (Authority.factAuthorityTheorem
                            (Authority.validationTarget
                                cachedCertificate)))
                    editedSyntax
                    (Declaration.committedBatchPreviousPrefix batch)
            corruptedRecord =
                Semantic.proofValidationRecord
                    corruptedKey
                    cachedCertificate
            mismatchResolver = Declaration.vampireResolver \prepared -> do
                IORef.modifyIORef' mismatchRuns (+ 1)
                resolveAccepted executable prepared
            mismatchingLookup = proofOnlyValidationLookup
                (const (pure (Just corruptedRecord)))
        mismatching <- Exception.try
            (runDriverWithValidationAndResolver
                fixture
                mismatchingLookup
                mismatchResolver
                do
                    Declaration.commitProofDeclaration editedSyntax do
                        candidate <- Declaration.reserveCandidate
                            (factSpec fixture "two-vampire-obligations")
                        Declaration.authorizeVampireCandidate candidate
                            (Declaration.acceptVampireObligation first))
            :: IO
                (Either
                    Declaration.ValidationIntegrityError
                    (Declaration.DriverResult
                        Text
                        ((), Declaration.CommittedDeclarationBatch)))
        case mismatching of
            Left Declaration.CachedValidationIntegrityError{} ->
                pure ()
            Right _ ->
                assertFailure "mismatching hit did not abort as corruption"
        assertEqual "mismatching hit does not fall back to Vampire"
            0
            =<< IORef.readIORef mismatchRuns

        withOpenedStore fixture root \store -> do
            expectRightIO
                (Store.writePendingModulePrefix store freshPrefix)
            warmCalls <- IORef.newIORef (0 :: Int)
            let storeLookup = proofOnlyValidationLookup \key -> do
                    IORef.modifyIORef' warmCalls (+ 1)
                    Store.loadProofValidation store key >>= expectRight
            warm <- runSuccessfulWithValidation fixture
                storeLookup
                do
                    (_value, committed) <- Declaration.commitProofDeclaration
                        (Semantic.proofSyntaxId "two-vampire-obligations") do
                            candidate <- Declaration.reserveCandidate
                                (factSpec fixture "two-vampire-obligations")
                            Declaration.authorizeVampireCandidate candidate do
                                Declaration.acceptVampireObligation first
                                Declaration.acceptVampireObligation second
                    pure committed
            assertEqual "warm lookup executes once through the store"
                1
                =<< IORef.readIORef warmCalls
            assertEqual "warm path retains cached request IDs"
                (Authority.CheckedSourceProof expectedRequests)
                (case Declaration.committedBatchProofValidations warm of
                    [record] ->
                        Authority.validationDirectAuthorization
                            (Semantic.proofValidationRecordCertificate record)
                    records ->
                        error
                            ("unexpected warm validation records: "
                                <> show (length records)))

        emptyProof <- runDriver fixture do
            Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "empty-vampire-proof") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "empty-vampire-proof")
                    Declaration.authorizeVampireCandidate candidate
                        (pure ())
        case emptyProof of
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                        Declaration.VampireProofHasNoAcceptedObligations)
                    prefix ->
                assertEqual
                    "empty Vampire proof publishes no declaration"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed other) _prefix ->
                assertFailure
                    ("unexpected empty-proof failure: " <> show other)
            Declaration.DriverFailed
                    (Declaration.DriverActionFailed _failure) _prefix ->
                assertFailure "unexpected ordinary driver failure"
            Declaration.DriverSucceeded{} ->
                assertFailure "empty Vampire proof was authorized"
            Declaration.DriverSealFailed{} ->
                assertFailure "empty Vampire proof reached sealing"

        invalidClosure <- expectRight
            (Identity.validateObjectClosure
                (Identity.theoryId (fixtureFoundation fixture))
                [])
        invalidTarget <- expectRight
            (Identity.validatePropositionContent
                invalidClosure
                (Core.CImp Core.CFalsum Core.CFalsum))
        invalidCalls <- IORef.newIORef (0 :: Int)
        let invalidResolver =
                Declaration.vampireResolver \prepared -> do
                    IORef.modifyIORef' invalidCalls (+ 1)
                    resolveAccepted executable prepared
        invalid <- runDriverWithResolver fixture invalidResolver do
            Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "invalid-vampire-target") do
                    candidate <- Declaration.reserveCandidate
                        (Declaration.candidateSpec
                            invalidTarget
                            Semantic.SearchEligible
                            [Semantic.semanticName
                                "invalid-vampire-target"])
                    Declaration.authorizeVampireCandidate candidate
                        (Declaration.acceptVampireObligation first)
        assertEqual
            "invalid prepared problem does not invoke Vampire"
            0
            =<< IORef.readIORef invalidCalls
        case invalid of
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                        Declaration.VampireTargetMismatch)
                    prefix ->
                assertEqual
                    "invalid prepared problem publishes no declaration"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed other) _prefix ->
                assertFailure
                    ("unexpected prepared-problem failure: " <> show other)
            Declaration.DriverFailed
                    (Declaration.DriverActionFailed _failure) _prefix ->
                assertFailure "unexpected ordinary driver failure"
            Declaration.DriverSucceeded{} ->
                assertFailure "invalid prepared problem was authorized"
            Declaration.DriverSealFailed{} ->
                assertFailure "invalid prepared problem reached sealing"

        let mismatchedResolver =
                Declaration.vampireResolver \_prepared ->
                    resolveAccepted executable second
        mismatch <- runDriverWithResolver fixture mismatchedResolver do
            Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "mismatched-vampire-request") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "mismatched-vampire-request")
                    Declaration.authorizeVampireCandidate candidate
                        (Declaration.acceptVampireObligation first)
        case mismatch of
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                        Declaration.VampireRequestMismatch)
                    prefix ->
                assertEqual
                    "mismatch publishes no declaration"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed other) _prefix ->
                assertFailure
                    ("unexpected mismatch failure: " <> show other)
            Declaration.DriverFailed
                    (Declaration.DriverActionFailed _failure) _prefix ->
                assertFailure "unexpected ordinary driver failure"
            Declaration.DriverSucceeded{} ->
                assertFailure "mismatched request was authorized"
            Declaration.DriverSealFailed{} ->
                assertFailure "mismatched request reached sealing"

        unrecorded <- runDriver fixture do
            Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "unrecorded-omission") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "unrecorded-omission")
                    Declaration.authorizeOmittedCandidate candidate
                        (pure ())
        case unrecorded of
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                        Declaration.OmittedProofDidNotRecordUse)
                    prefix ->
                assertEqual
                    "unrecorded omission publishes no declaration"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed other) _prefix ->
                assertFailure
                    ("unexpected unrecorded-omission failure: "
                        <> show other)
            Declaration.DriverFailed
                    (Declaration.DriverActionFailed _failure) _prefix ->
                assertFailure "unexpected ordinary driver failure"
            Declaration.DriverSucceeded{} ->
                assertFailure "unrecorded omission was authorized"
            Declaration.DriverSealFailed{} ->
                assertFailure "unrecorded omission reached sealing"

        calls <- IORef.newIORef (0 :: Int)
        let countingResolver =
                Declaration.vampireResolver \prepared -> do
                    IORef.modifyIORef' calls (+ 1)
                    resolveAccepted executable prepared
        omittedBatch <- runSuccessfulWithResolver fixture countingResolver do
            (_value, committed) <- Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "omitted-after-obligations") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "omitted-after-obligations")
                    Declaration.authorizeOmittedCandidate candidate do
                        Declaration.acceptVampireObligation first
                        Declaration.acceptVampireObligation second
                        Declaration.recordOmittedUse
            pure committed
        assertEqual
            "omitted proof still checks preceding obligations"
            2
            =<< IORef.readIORef calls
        case Declaration.committedBatchProofValidations omittedBatch of
            [record] ->
                assertEqual
                    "omitted direct authorization discards request IDs"
                    Authority.OmittedAuthorization
                    (Authority.validationDirectAuthorization
                        (Semantic.proofValidationRecordCertificate record))
            records ->
                assertFailure
                    ("unexpected omitted validation count: "
                        <> show (length records))

validatesCompleteResolverBatchesBeforeRejection :: Assertion
validatesCompleteResolverBatchesBeforeRejection =
    withTemporaryDirectory "felix-declaration-batch-integrity" \root -> do
        fixture <- makeFixture
        let executable = root Posix.</> "vampire"
            firstLocation = mkLocation (FileId 76) 1 1
            secondLocation = mkLocation (FileId 76) 2 1
        writeAcceptedVampire executable
        mismatchedTask <-
            makePreparedObligation
                fixture
                Foundation.EmptyCharacteristic
        let integrityResolver =
                Declaration.vampireBatchResolver \_tasks -> do
                    mismatched <- resolveAccepted executable mismatchedTask
                    pure
                        ( Right (Provers.CounterSatisfiable "earlier")
                        :| [mismatched]
                        )
        integrityOutcome <-
            (runDriverWithResolver fixture integrityResolver do
                Declaration.commitProofDeclaration
                    (Semantic.proofSyntaxId "batch-integrity-priority") do
                        candidates <- Declaration.reserveCandidateBatch
                            ( factSpec fixture "batch-integrity-first"
                            :| [factSpec fixture "batch-integrity-second"]
                            )
                        Declaration.authorizeVampireCandidateBatch
                            ( ( firstLocation
                              , NonEmpty.head candidates
                              , Declaration.prepareCurrentCandidateVampire
                              )
                            :| [ ( secondLocation
                                 , NonEmpty.last candidates
                                 , Declaration.prepareCurrentCandidateVampire
                                 )
                               ]
                            )
                :: IO
                    (Declaration.DriverResult Text
                        ((), Declaration.CommittedDeclarationBatch)))
        case integrityOutcome of
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                        (Declaration.ProofObligationFailedAt
                            location
                            Declaration.VampireRequestMismatch))
                    prefix -> do
                assertEqual
                    "later request mismatch retains its location"
                    secondLocation
                    location
                assertEqual
                    "integrity failure rolls back the complete declaration"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Declaration.DriverFailed failure _prefix ->
                assertFailure
                    ("unexpected batch-integrity failure: " <> show failure)
            Declaration.DriverSucceeded{} ->
                assertFailure
                    "earlier ordinary rejection concealed no integrity failure"
            Declaration.DriverSealFailed{} ->
                assertFailure "invalid batch reached module sealing"

        prepared <-
            makePreparedObligation
                fixture
                Foundation.EmptyCharacteristic
        let excessResolver =
                Declaration.vampireBatchResolver \_tasks ->
                    pure
                        ( Right (Provers.CounterSatisfiable "first")
                        :| [Right (Provers.CounterSatisfiable "excess")]
                        )
        excessOutcome <-
            (runDriverWithResolver fixture excessResolver do
                Declaration.commitProofDeclaration
                    (Semantic.proofSyntaxId "singleton-excess-result") do
                        candidate <- Declaration.reserveCandidate
                            (factSpec fixture "singleton-excess-result")
                        Declaration.authorizeVampireCandidate candidate
                            (Declaration.acceptVampireObligation prepared)
                :: IO
                    (Declaration.DriverResult Text
                        ((), Declaration.CommittedDeclarationBatch)))
        case excessOutcome of
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                        (Declaration.VampireResolverBatchSizeMismatch 1 2))
                    prefix ->
                assertEqual
                    "malformed singleton response publishes no declaration"
                    0
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Declaration.DriverFailed failure _prefix ->
                assertFailure
                    ("unexpected singleton-cardinality failure: "
                        <> show failure)
            Declaration.DriverSucceeded{} ->
                assertFailure "singleton resolver ignored an excess result"
            Declaration.DriverSealFailed{} ->
                assertFailure "malformed singleton reached module sealing"

rejectsRetainedPlanAdmissionDrift :: Assertion
rejectsRetainedPlanAdmissionDrift = do
    fixture <- makeFixture
    let checked =
            Declaration.checkedProofDeclaration
                (Semantic.proofSyntaxId "planned-admission-drift")
                []
                []
                []
                []
                [ Declaration.checkedCandidate
                    (factSpec fixture "planned-admission-drift")
                    Declaration.checkedSourceAxiomPlanning
                    :| []
                ]
                ()
        action = do
            planned <-
                Declaration.runProspectiveLoweringDriver
                    (Declaration.planCheckedDeclaration checked)
                    >>= either Declaration.failDeclarationDriver pure
            Declaration.admitPlannedCheckedDeclaration planned
                (\() stages ->
                    case concatMap toList stages of
                        [candidate] ->
                            Declaration.authorizeOmittedCandidate candidate
                                Declaration.recordOmittedUse
                        _ -> error "planned drift fixture candidate shape")
    outcome <-
        Exception.try (runDriver fixture action)
            :: IO
                (Either
                    Declaration.PlanningIntegrityError
                    (Declaration.DriverResult
                        Void
                        Declaration.CommittedDeclarationBatch))
    case outcome of
        Left (Declaration.PlanningIntegrityError diagnostic) ->
            assertBool "fatal mismatch identifies prospective contract drift"
                ("prospective contract" `Text.isInfixOf` diagnostic)
        Right _ ->
            assertFailure
                "a changed admitted authority was accepted against its plan"

preservesSourceAxiomSafetyThroughVampireValidation :: Assertion
preservesSourceAxiomSafetyThroughVampireValidation =
    withTemporaryDirectory "felix-declaration-source-axiom" \root -> do
        fixture <- makeFixture
        let executable = root Posix.</> "vampire"
        writeAcceptedVampire executable
        prepared <-
            makePreparedObligationWithPremise
                fixture
                (fixtureSourceAxiomFingerprint fixture)
        freshCalls <- IORef.newIORef (0 :: Int)
        let freshResolver = Declaration.vampireResolver \task -> do
                IORef.modifyIORef' freshCalls (+ 1)
                resolveAccepted executable task
        freshOutcome <-
            (runDriverWithResolver fixture freshResolver
                (sourceAxiomThenVampire fixture prepared)
                :: IO
                    (Declaration.DriverResult Text
                        Declaration.CommittedDeclarationBatch))
        assertEqual
            "fresh source-axiom theorem invokes Vampire once"
            1
            =<< IORef.readIORef freshCalls
        freshBatch <-
            case freshOutcome of
                Declaration.DriverSucceeded batch _ _ _closure ->
                    pure batch
                Declaration.DriverFailed failure _ ->
                    assertFailure
                        ("fresh source-axiom driver failed: "
                            <> show failure)
                        >> fail "unreachable"
                Declaration.DriverSealFailed failure _ ->
                    assertFailure
                        ("fresh source-axiom driver did not seal: "
                            <> show failure)
                        >> fail "unreachable"
        let freshRecord = singleProofValidation freshBatch
        assertEqual
            "fresh theorem retains source-axiom safety"
            sourceAxiomSafety
            (Authority.factAuthoritySafety
                (Authority.validationTarget
                    (Semantic.proofValidationRecordCertificate freshRecord)))
        separationCalls <- IORef.newIORef (0 :: Int)
        let separationResolver = Declaration.vampireResolver \task -> do
                IORef.modifyIORef' separationCalls (+ 1)
                resolveAccepted executable task
        separated <-
            (runDriverWithResolver fixture separationResolver do
                void
                    (Declaration.commitProofDeclaration
                        (Semantic.proofSyntaxId "source-axiom") do
                            candidate <- Declaration.reserveCandidate
                                (factSpec fixture "source-axiom")
                            Declaration.authorizeSourceAxiomCandidate candidate)
                Declaration.commitProofDeclaration
                    (Semantic.proofSyntaxId "atp-does-not-import") do
                        candidate <- Declaration.reserveCandidate
                            (factSpec fixture "atp-does-not-import")
                        Declaration.authorizeKernelProofCandidate candidate do
                            Declaration.acceptVampireObligation prepared
                            pure
                                (Kernel.importedFactDerivation
                                    (Kernel.importIx 0))
                :: IO
                    (Declaration.DriverResult Text
                        ((), Declaration.CommittedDeclarationBatch)))
        assertEqual "mixed proof executes its ATP obligation"
            1
            =<< IORef.readIORef separationCalls
        case separated of
            Declaration.DriverFailed
                    (Declaration.DriverDeclarationFailed
                        (Declaration.KernelCompletionFailed
                            (Kernel.KernelReplayImportOutOfBounds index)))
                    prefix -> do
                assertEqual "ATP premise is absent from kernel imports"
                    (Kernel.importIx 0)
                    index
                assertEqual "failed mixed proof retains only its prefix"
                    1
                    (length
                        (Declaration.pendingModulePrefixBatches prefix))
            Declaration.DriverFailed failure _prefix ->
                assertFailure
                    ("unexpected mixed-proof failure: " <> show failure)
            Declaration.DriverSucceeded{} ->
                assertFailure "ATP premise entered the kernel import inventory"
            Declaration.DriverSealFailed{} ->
                assertFailure "mixed proof unexpectedly reached sealing"
        withOpenedStore fixture root \store -> do
            freshPrefix <-
                case freshOutcome of
                    Declaration.DriverSucceeded _ _ prefix _closure ->
                        pure prefix
                    Declaration.DriverFailed failure _ ->
                        assertFailure
                            ("fresh source-axiom driver failed: "
                                <> show failure)
                            >> fail "unreachable"
                    Declaration.DriverSealFailed failure _ ->
                        assertFailure
                            ("fresh source-axiom driver did not seal: "
                                <> show failure)
                            >> fail "unreachable"
            expectRightIO
                (Store.writePendingModulePrefix store freshPrefix)
            warmCalls <- IORef.newIORef (0 :: Int)
            let storeLookup = proofOnlyValidationLookup \key -> do
                    IORef.modifyIORef' warmCalls (+ 1)
                    Store.loadProofValidation store key >>= expectRight
            warmBatch <- runSuccessfulWithValidation fixture
                storeLookup
                (sourceAxiomThenVampire fixture prepared)
            assertEqual
                "warm source-axiom theorem performs one store lookup"
                1
                =<< IORef.readIORef warmCalls
            assertEqual
                "warm theorem retains source-axiom safety"
                sourceAxiomSafety
                (Authority.factAuthoritySafety
                    (Authority.validationTarget
                        (Semantic.proofValidationRecordCertificate
                            (singleProofValidation warmBatch))))
  where
    sourceAxiomSafety =
        Authority.authoritySafety
            (Authority.singletonEscapeKind Authority.SourceAxiom)

    singleProofValidation batch =
        case Declaration.committedBatchProofValidations batch of
            [record] -> record
            records ->
                error
                    ("unexpected proof validation count: "
                        <> show (length records))

sourceAxiomThenVampire
    :: Fixture
    -> Provers.PreparedTypedProverTask
        Semantic.SemanticFactOccurrenceFingerprint
        Void
        ()
        Identity.ObjectId
    -> Declaration.ModuleDriver failure
        Declaration.CommittedDeclarationBatch
sourceAxiomThenVampire fixture prepared = do
    void
        (Declaration.commitProofDeclaration
            (Semantic.proofSyntaxId "source-axiom") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "source-axiom")
                Declaration.authorizeSourceAxiomCandidate candidate)
    (_value, batch) <- Declaration.commitProofDeclaration
        (Semantic.proofSyntaxId "source-axiom-vampire") do
            candidate <- Declaration.reserveCandidate
                (factSpec fixture "source-axiom-vampire")
            Declaration.authorizeVampireCandidate candidate
                (Declaration.acceptVampireObligation prepared)
    pure batch

fixtureSourceAxiomFingerprint
    :: Fixture
    -> Semantic.SemanticFactOccurrenceFingerprint
fixtureSourceAxiomFingerprint fixture =
    Semantic.semanticFactOccurrenceFingerprint
        (Semantic.factSlot
            (fixtureOwner fixture)
            (localFactOrdinal 0))
        (Authority.factAuthority
            (Identity.theoremRef
                (Identity.theoryId (fixtureFoundation fixture))
                (Identity.checkedPropositionId
                    (fixtureProposition fixture)))
            (Authority.authoritySafety
                (Authority.singletonEscapeKind Authority.SourceAxiom)))

makePreparedObligationWithPremise
    :: Fixture
    -> Semantic.SemanticFactOccurrenceFingerprint
    -> IO
        (Provers.PreparedTypedProverTask
            Semantic.SemanticFactOccurrenceFingerprint
            Void
            ()
            Identity.ObjectId)
makePreparedObligationWithPremise fixture fingerprint = do
    claim <- expectRight
        (Backend.supportedProposition
            (Vector.empty :: Vector.Vector (Void, Core.CoreType))
            (Core.embedClosedCore
                []
                (Identity.checkedPropositionTerm
                    (fixtureProposition fixture))))
    factProposition <- expectRight
        (Backend.supportedProposition
            (Vector.empty :: Vector.Vector (Void, Core.CoreType))
            (Core.embedClosedCore
                []
                (Identity.checkedPropositionTerm
                    (fixtureProposition fixture))))
    capability <- expectRight
        (Backend.classifySupportedProposition
            (const Nothing)
            factProposition)
    problem <- expectRight
        (Backend.planTypedProblem
            (const Nothing)
            (Vector.singleton
                (Backend.typedBackendFact
                    fingerprint
                    factProposition
                    capability))
            claim
            []
            []
            Backend.FirstOrderLocals
            Backend.ExplicitHigherOrderJustification)
    expectRight
        (Provers.prepareTypedProverTask
            Provers.DirectTask
            problem)

makePreparedObligation
    :: Fixture
    -> Foundation.FoundationAxiomTag
    -> IO
        (Provers.PreparedTypedProverTask
            Semantic.SemanticFactOccurrenceFingerprint
            Void
            ()
            Identity.ObjectId)
makePreparedObligation fixture tag = do
    claim <- expectRight
        (Backend.supportedProposition
            (Vector.empty :: Vector.Vector (Void, Core.CoreType))
            (Core.embedClosedCore
                []
                (Identity.checkedPropositionTerm
                    (fixtureProposition fixture))))
    problem <- expectRight
        (Backend.planTypedProblem
            (const Nothing)
            Vector.empty
            claim
            []
            [Backend.typedFoundationAuxiliaryInput
                (fixtureFoundation fixture)
                tag]
            Backend.CompleteLocals
            Backend.ExplicitHigherOrderJustification)
    expectRight
        (Provers.prepareTypedProverTask
            Provers.DirectTask
            problem)

acceptedResolver :: FilePath -> Declaration.VampireResolver
acceptedResolver executable =
    Declaration.vampireResolver (resolveAccepted executable)

resolveAccepted
    :: FilePath
    -> Provers.PreparedTypedProverTask
        ref local origin global
    -> IO
        (Either
            Provers.ProverProcessError
            Provers.ProverAnswer)
resolveAccepted executable prepared =
    Provers.runPreparedTypedProver
        (Provers.vampire
            executable
            Provers.defaultTimeLimit
            Provers.defaultMemoryLimit)
        prepared

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

validatesExactKernelConstructionDescriptors :: Assertion
validatesExactKernelConstructionDescriptors = do
    fixture <- makeFixture
    proposition <- foundationProposition
        fixture
        Foundation.EmptyCharacteristic
    let declaredObject = opaqueFixtureObject fixture
        run descriptor =
            runDriver fixture
                (Declaration.commitCompiledDeclaration
                    (Semantic.declarationSyntaxId
                        "kernel-construction-descriptor") do
                        Declaration.addDeclarationObject declaredObject
                        candidate <- Declaration.reserveCandidate
                            (Declaration.candidateSpec
                                proposition
                                Semantic.SearchEligible
                                [Semantic.semanticName "kernel-construction"])
                        Declaration.authorizeCompiledDeclaration
                            (Declaration.authorizeKernelConstructionCandidate
                                descriptor
                                candidate
                                (pure
                                    (Kernel.foundationFactDerivation
                                        Foundation.EmptyCharacteristic))))
    success <- run
        (Authority.FoundationLeaf
            Foundation.EmptyCharacteristic)
    case success of
        Declaration.DriverSucceeded (_value, batch) _interface _prefix _closure -> do
            assertEqual
                "new object is included in the checked declaration batch"
                1
                (length (Declaration.committedBatchObjects batch))
            case Declaration.committedBatchDeclarationValidation batch of
                Just record ->
                    case Semantic.declarationValidationRecordCertificates
                            record of
                        [certificate] ->
                            assertEqual
                                "exact kernel descriptor is retained"
                                (Authority.CheckedKernelConstruction
                                    (Authority.FoundationLeaf
                                        Foundation.EmptyCharacteristic))
                                (Authority.validationDirectAuthorization
                                    certificate)
                        certificates ->
                            assertFailure
                                ("unexpected kernel certificate count: "
                                    <> show (length certificates))
                Nothing ->
                    assertFailure "missing declaration validation"
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed failure) _prefix ->
            assertFailure
                ("valid kernel descriptor failed: " <> show failure)
        Declaration.DriverFailed
                (Declaration.DriverActionFailed _failure) _prefix ->
            assertFailure "unexpected ordinary driver failure"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure (show failure)

    traverse_
        (\(label, descriptor) -> do
            outcome <- run descriptor
            case outcome of
                Declaration.DriverFailed
                        (Declaration.DriverDeclarationFailed
                            Declaration.KernelConstructionDescriptorMismatch)
                        prefix ->
                    assertEqual
                        (label <> " publishes no declaration")
                        0
                        (length
                            (Declaration.pendingModulePrefixBatches prefix))
                Declaration.DriverFailed
                        (Declaration.DriverDeclarationFailed other)
                        _prefix ->
                    assertFailure
                        (label <> ": unexpected error " <> show other)
                Declaration.DriverFailed
                        (Declaration.DriverActionFailed _failure)
                        _prefix ->
                    assertFailure (label <> ": ordinary driver failure")
                Declaration.DriverSucceeded{} ->
                    assertFailure (label <> ": mismatch was accepted")
                Declaration.DriverSealFailed{} ->
                    assertFailure (label <> ": mismatch reached sealing"))
        [ ( "wrong foundation leaf"
          , Authority.FoundationLeaf
                Foundation.PairSetCharacteristic
          )
        , ( "wrong construction family"
          , Authority.GuardedFoundationRules
                (Authority.guardedRuleSet
                    (Foundation.SetLfpBound :| []))
          )
        ]

authorizesExactDatatypeCompilationFamilies :: Assertion
authorizesExactDatatypeCompilationFamilies = do
    fixture <- makeFixture
    firstProposition <- foundationProposition
        fixture
        Foundation.EmptyCharacteristic
    secondProposition <- foundationProposition
        fixture
        Foundation.PairSetCharacteristic
    let carrier = datatypeFixtureObject fixture 0
        constructor = datatypeFixtureObject fixture 1
        carrierId = Identity.assertedObjectId carrier
        constructorId = Identity.assertedObjectId constructor
        references =
            fmap
                (Identity.theoremRef
                    (Identity.theoryId
                        (fixtureFoundation fixture))
                    . Identity.checkedPropositionId)
                [firstProposition, secondProposition]
        descriptor =
            Authority.datatypeCompilationDescriptor
                carrierId
                (constructorId :| [])
                references
        action
            :: Authority.DatatypeCompilationDescriptor
            -> Declaration.ModuleDriver Text
                ((), Declaration.CommittedDeclarationBatch)
        action suppliedDescriptor =
            Declaration.commitCompiledDeclaration
                (Semantic.declarationSyntaxId "datatype-compilation") do
                traverse_ Declaration.addDeclarationObject
                    [carrier, constructor]
                candidates <-
                    Declaration.reserveCandidateBatch
                        ( Declaration.candidateSpec
                            firstProposition
                            Semantic.SearchEligible
                            [Semantic.semanticName "datatype-first"]
                        :| [ Declaration.candidateSpec
                                secondProposition
                                Semantic.SearchEligible
                                [Semantic.semanticName "datatype-second"]
                           ]
                        )
                Declaration.authorizeCompiledDeclaration
                    (Declaration.authorizeDatatypeCompilationCandidates
                        suppliedDescriptor
                        carrierId
                        (constructorId :| [])
                        candidates)

    (_value, batch) <- runSuccessful fixture (action descriptor)
    assertEqual "complete object family was published"
        [carrier, constructor]
        (Declaration.committedBatchObjects batch)
    case Declaration.committedBatchDeclarationValidation batch of
        Just record -> do
            let certificates =
                    Semantic.declarationValidationRecordCertificates record
            assertEqual "complete fact family was authorized" 2
                (length certificates)
            traverse_
                (\certificate -> do
                    assertEqual "datatype authority is clean"
                        Authority.cleanAuthoritySafety
                        (Authority.factAuthoritySafety
                            (Authority.validationTarget certificate))
                    assertEqual "one descriptor protects every member"
                        (Authority.TrustedCompilation
                            (Authority.DatatypeCompilation descriptor))
                        (Authority.validationDirectAuthorization certificate))
                certificates
        Nothing ->
            assertFailure "datatype compilation omitted validation"

    let mismatched =
            Authority.datatypeCompilationDescriptor
                carrierId
                (constructorId :| [])
                (reverse references)
    rejected <- runDriver fixture (action mismatched)
    case rejected of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    Declaration.DatatypeCompilationDescriptorMismatch)
                prefix ->
            assertEqual "mismatched family publishes no declaration"
                0
                (length
                    (Declaration.pendingModulePrefixBatches prefix))
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("unexpected datatype-family failure: " <> show failure)
        Declaration.DriverSucceeded{} ->
            assertFailure "mismatched datatype family was authorized"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("mismatched datatype family reached sealing: "
                    <> show failure)

reusesExactCompiledDeclarationValidation :: Assertion
reusesExactCompiledDeclarationValidation = do
    fixture <- makeFixture
    proposition <- foundationProposition
        fixture
        Foundation.EmptyCharacteristic
    let declaredObject = opaqueFixtureObject fixture
        syntax =
            Semantic.declarationSyntaxId
                "cached-kernel-construction"
        action derivationTag =
            Declaration.commitCompiledDeclaration syntax do
                Declaration.addDeclarationObject declaredObject
                candidate <- Declaration.reserveCandidate
                    (Declaration.candidateSpec
                        proposition
                        Semantic.SearchEligible
                        [Semantic.semanticName
                            "cached-kernel-construction"])
                Declaration.authorizeCompiledDeclaration
                    (Declaration.authorizeKernelConstructionCandidate
                        (Authority.FoundationLeaf
                            Foundation.EmptyCharacteristic)
                        candidate
                        (pure
                            (Kernel.foundationFactDerivation
                                derivationTag)))
    freshBatch <- runSuccessful fixture
        (snd <$> action Foundation.EmptyCharacteristic)
    freshRecord <-
        case Declaration.committedBatchDeclarationValidation freshBatch of
            Just record -> pure record
            Nothing ->
                assertFailure "fresh compiled declaration omitted validation"
                    >> fail "unreachable"

    missLookups <- IORef.newIORef (0 :: Int)
    missBatch <- runSuccessfulWithValidation fixture
        (compiledOnlyValidationLookup \_key -> do
            IORef.modifyIORef' missLookups (+ 1)
            pure Nothing)
        (snd <$> action Foundation.EmptyCharacteristic)
    assertEqual "compiled warm miss performs one exact lookup"
        1
        =<< IORef.readIORef missLookups
    assertBool "compiled miss publishes fresh validation"
        (isJust
            (Declaration.committedBatchDeclarationValidation missBatch))

    hitLookups <- IORef.newIORef []
    hitBatch <- runSuccessfulWithValidation fixture
        (compiledOnlyValidationLookup \key -> do
            IORef.modifyIORef' hitLookups (key :)
            pure (Just freshRecord))
        (snd <$> action Foundation.PairSetCharacteristic)
    assertEqual "compiled warm hit performs one exact lookup"
        [Semantic.declarationValidationRecordKey freshRecord]
        . reverse
        =<< IORef.readIORef hitLookups
    case Declaration.committedBatchDeclarationValidation hitBatch of
        Just record ->
            assertEqual
                "compiled hit republishes the exact validation"
                freshRecord
                record
        Nothing ->
            assertFailure "compiled hit omitted validation"

foundationProposition
    :: Fixture
    -> Foundation.FoundationAxiomTag
    -> IO Identity.CheckedPropositionContent
foundationProposition fixture tag = do
    closure <- expectRight
        (Identity.validateObjectClosure
            (Identity.theoryId (fixtureFoundation fixture))
            [])
    expectRight
        (Identity.validatePropositionContent
            closure
            (Core.frozenCoreTerm
                (Core.mapFrozenGlobals
                    absurd
                    (Foundation.foundationAxiomFrozen
                        (fixtureFoundation fixture)
                        tag))))

opaqueFixtureObject :: Fixture -> Identity.AssertedObject
opaqueFixtureObject fixture =
    let theory = Identity.theoryId (fixtureFoundation fixture)
        seed =
            Identity.opaqueDeclarationSeed
                (fixtureOwner fixture)
                (localDeclarationOrdinal 0)
                SignatureDeclaration
                (generatedObjectSlot 0)
        identity =
            Identity.opaqueObjectId
                theory
                seed
                Core.TySet
    in Identity.assertedObject
        identity
        (Identity.OpaqueObjectContent
            theory
            seed
            Core.TySet)

datatypeFixtureObject
    :: Fixture
    -> Natural
    -> Identity.AssertedObject
datatypeFixtureObject fixture slot =
    let theory = Identity.theoryId (fixtureFoundation fixture)
        seed =
            Identity.opaqueDeclarationSeed
                (fixtureOwner fixture)
                (localDeclarationOrdinal 0)
                DatatypeDeclaration
                (generatedObjectSlot slot)
        identity =
            Identity.opaqueObjectId theory seed Core.TySet
    in Identity.assertedObject
        identity
        (Identity.OpaqueObjectContent theory seed Core.TySet)


data Fixture = Fixture
    { fixtureFoundation :: !Foundation.CheckedFoundation
    , fixtureOwner :: !ModuleName
    , fixtureProposition :: !Identity.CheckedPropositionContent
    }

makeFixture :: IO Fixture
makeFixture =
    makeNamedFixture "root"

makeNamedFixture :: Text -> IO Fixture
makeNamedFixture name = do
    foundation <- expectRight Foundation.checkedFoundation
    namespaceDigest <- expectRight
        (hashCanonicalFields
            "declaration-test-namespace"
            [TextEncoding.encodeUtf8 name])
    relative <- expectRight
        (safeRelativePath
            (Text.unpack name <> ".tex"))
    let theory = Identity.theoryId foundation
        owner =
            moduleNameFromParts
                (sourceNamespaceIdFromDigest namespaceDigest)
                relative
    closure <- expectRight
        (Identity.validateObjectClosure theory [])
    proposition <- expectRight
        (Identity.validatePropositionContent closure Core.CFalsum)
    pure
        Fixture
            { fixtureFoundation = foundation
            , fixtureOwner = owner
            , fixtureProposition = proposition
            }

factSpec :: Fixture -> Text -> Declaration.CandidateSpec
factSpec fixture alias =
    Declaration.candidateSpec
        (fixtureProposition fixture)
        Semantic.SearchEligible
        [Semantic.semanticName alias]

runDriver
    :: Fixture
    -> Declaration.ModuleDriver failure value
    -> IO (Declaration.DriverResult failure value)
runDriver fixture =
    runDriverWithResolver fixture unavailableVampireResolver

runDriverWithResolver
    :: Fixture
    -> Declaration.VampireResolver
    -> Declaration.ModuleDriver failure value
    -> IO (Declaration.DriverResult failure value)
runDriverWithResolver fixture resolver action = do
    result <- Declaration.runModuleDriver
        (fixtureFoundation fixture)
        (fixtureOwner fixture)
        []
        resolver
        Declaration.FreshValidation
        action
    expectRight result

runDriverWithValidation
    :: Fixture
    -> Declaration.ValidationLookup
    -> Declaration.ModuleDriver failure value
    -> IO (Declaration.DriverResult failure value)
runDriverWithValidation fixture lookup action = do
    runDriverWithValidationAndResolver
        fixture
        lookup
        unavailableVampireResolver
        action

runDriverWithValidationAndResolver
    :: Fixture
    -> Declaration.ValidationLookup
    -> Declaration.VampireResolver
    -> Declaration.ModuleDriver failure value
    -> IO (Declaration.DriverResult failure value)
runDriverWithValidationAndResolver fixture lookup resolver action = do
    result <- Declaration.runModuleDriver
        (fixtureFoundation fixture)
        (fixtureOwner fixture)
        []
        resolver
        (Declaration.WarmValidation lookup)
        action
    expectRight result

proofOnlyValidationLookup
    :: (Semantic.ProofValidationKey
        -> IO (Maybe Semantic.ProofValidationRecord))
    -> Declaration.ValidationLookup
proofOnlyValidationLookup lookupProof =
    Declaration.validationLookup
        lookupProof
        (const (pure Nothing))

compiledOnlyValidationLookup
    :: (Semantic.DeclarationValidationKey
        -> IO (Maybe Semantic.DeclarationValidationRecord))
    -> Declaration.ValidationLookup
compiledOnlyValidationLookup lookupDeclaration =
    Declaration.validationLookup
        (const (pure Nothing))
        lookupDeclaration

runDriverWithDirect
    :: Fixture
    -> [Semantic.SemanticInterfaceId]
    -> Declaration.ModuleDriver failure value
    -> IO (Declaration.DriverResult failure value)
runDriverWithDirect fixture direct action = do
    result <- Declaration.runModuleDriver
        (fixtureFoundation fixture)
        (fixtureOwner fixture)
        direct
        unavailableVampireResolver
        Declaration.FreshValidation
        action
    expectRight result

unavailableVampireResolver :: Declaration.VampireResolver
unavailableVampireResolver =
    Declaration.vampireResolver \_prepared ->
        pure
            (Left
                (Provers.ProverLaunchFailed
                    "unused"
                    "Vampire resolver was not expected"))

runSuccessful
    :: Fixture
    -> Declaration.ModuleDriver failure value
    -> IO value
runSuccessful fixture =
    runSuccessfulWithResolver fixture unavailableVampireResolver

runSuccessfulWithResolver
    :: Fixture
    -> Declaration.VampireResolver
    -> Declaration.ModuleDriver failure value
    -> IO value
runSuccessfulWithResolver fixture resolver action = do
    outcome <- runDriverWithResolver fixture resolver action
    case outcome of
        Declaration.DriverSucceeded value _interface _prefix _closure ->
            pure value
        Declaration.DriverFailed _failure _prefix ->
            assertFailure "unexpected driver failure" >> fail "unreachable"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure (show failure) >> fail "unreachable"

runSuccessfulWithValidation
    :: Fixture
    -> Declaration.ValidationLookup
    -> Declaration.ModuleDriver failure value
    -> IO value
runSuccessfulWithValidation fixture lookup action = do
    outcome <- runDriverWithValidation fixture lookup action
    case outcome of
        Declaration.DriverSucceeded value _interface _prefix _closure ->
            pure value
        Declaration.DriverFailed _failure _prefix ->
            assertFailure "unexpected driver failure" >> fail "unreachable"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure (show failure) >> fail "unreachable"

materializesSealedImport :: Assertion
materializesSealedImport = do
    fixture <- makeFixture
    producer <- runDriver fixture do
        (_value, batch) <- Declaration.commitProofDeclaration
            (Semantic.proofSyntaxId "sealed-import-producer") do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture "producer-fact")
                Declaration.authorizeOmittedCandidate candidate
                    Declaration.recordOmittedUse
        pure batch
    (producerInterface, evidence, fingerprint) <-
        case producer of
            Declaration.DriverSucceeded _ interface prefix _closure ->
                let imported =
                        Declaration.freshImportedModuleEvidence
                            [] interface prefix
                in case concatMap
                        Semantic.declarationDeltaFacts
                        (Semantic.semanticInterfaceDeclarations interface) of
                    [occurrence] ->
                        pure
                            ( interface
                            , imported
                            , Semantic.semanticFactFingerprint occurrence
                            )
                    occurrences ->
                        assertFailure
                            ("unexpected producer facts: "
                                <> show (length occurrences))
                            >> fail "unreachable"
            Declaration.DriverFailed failure _prefix ->
                assertFailure
                    ("producer failed: "
                        <> show
                            (failure
                                :: Declaration.DriverFailure
                                    Declaration.DeclarationError))
                    >> fail "unreachable"
            Declaration.DriverSealFailed failure _prefix ->
                assertFailure ("producer did not seal: " <> show failure)
                    >> fail "unreachable"
    consumerNamespace <- expectRight
        (hashCanonicalFields
            "declaration-import-consumer"
            ["consumer"])
    consumerPath <- expectRight (safeRelativePath "consumer.tex")
    let consumerFixture =
            fixture
                { fixtureOwner =
                    moduleNameFromParts
                        (sourceNamespaceIdFromDigest consumerNamespace)
                        consumerPath
                }
    consumer <- runDriverWithDirect consumerFixture
        [Semantic.semanticInterfaceAssertedId producerInterface]
        do
            (_value, committed) <- Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "sealed-import-consumer") do
                    Declaration.importSealedModule evidence
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "consumer-fact")
                    Declaration.authorizeOmittedCandidate candidate do
                        _ <- Declaration.useAuthorizedFact fingerprint
                        Declaration.recordOmittedUse
            pure committed
    case consumer of
        Declaration.DriverSucceeded committed _ _ _ -> do
            case Semantic.declarationDeltaFacts
                    (Declaration.committedBatchDelta committed) of
                [localOccurrence] -> do
                    assertEqual
                        "the first local fact keeps ordinal zero"
                        (localFactOrdinal 0)
                        (Semantic.factSlotOrdinal
                            (Semantic.semanticFactSlot localOccurrence))
                    assertEqual
                        "the local fact belongs to the consumer"
                        (fixtureOwner consumerFixture)
                        (Semantic.factSlotModule
                            (Semantic.semanticFactSlot localOccurrence))
                facts ->
                    assertFailure
                        ("unexpected consumer fact count: "
                            <> show (length facts))
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("consumer failed: "
                    <> show
                        (failure
                            :: Declaration.DriverFailure
                                Declaration.DeclarationError))
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure ("consumer did not seal: " <> show failure)

elaboratesScopedExactPropositions :: Assertion
elaboratesScopedExactPropositions = do
    fixture <- makeNamedFixture "exact-scoped-proposition"
    let x = Raw.NamedVar "x"
        y = Raw.NamedVar "y"
        statement =
            Raw.SymbolicQuantified
                Nowhere
                Raw.Universally
                (x :| [y])
                Raw.Unbounded
                Nothing
                (Raw.StmtFormula
                    (Raw.FormulaChain
                        (Raw.ChainBase
                            (Raw.ExprVar x :| [])
                            Raw.Positive
                            (Raw.Relation
                                Nowhere
                                Raw.EqSymbol
                                [])
                            (Raw.ExprVar y :| []))))
        action
            :: Declaration.ModuleDriver Text
                (Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition)
        action =
            Declaration.runProspectiveLoweringDriver
                (Exact.prepareExactProposition
                    Exact.emptyExactBinderContext
                    statement)
    outcome <- runDriver fixture action
    case outcome of
        Declaration.DriverSucceeded (Right prepared) _interface _prefix _closure ->
            assertEqual
                "source-order universal binders"
                (Core.CForall Core.TySet
                    (Core.CForall Core.TySet
                        (Core.CEq Core.TySet
                            (Core.CBound 1)
                            (Core.CBound 0))))
                (Core.scopedCoreTerm
                    (Exact.preparedExactPropositionCore prepared))
        Declaration.DriverSucceeded (Left failure) _interface _prefix _closure ->
            assertFailure
                ("scoped exact elaboration failed: "
                    <> Text.unpack (Exact.renderExactCompileError failure))
        Declaration.DriverFailed failure _prefix ->
            assertFailure ("scoped exact driver failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure ("scoped exact driver did not seal: " <> show failure)

lowersFixedEqualityAliases :: Assertion
lowersFixedEqualityAliases = do
    fixture <- makeNamedFixture "fixed-equality-aliases"
    let x = Raw.NamedVar "x"
        y = Raw.NamedVar "y"
        z = Raw.NamedVar "z"
        term variable = Raw.TermExpr (Raw.ExprVar variable)
        equality left right =
            Raw.StmtFormula
                (Raw.FormulaChain
                    (Raw.ChainBase
                        (Raw.ExprVar left :| [])
                        Raw.Positive
                        (Raw.Relation Nowhere Raw.EqSymbol [])
                        (Raw.ExprVar right :| [])))
        quantified variables statement =
            Raw.SymbolicQuantified
                Nowhere
                Raw.Universally
                variables
                Raw.Unbounded
                Nothing
                statement
        adjective =
            Raw.Adj
                Nowhere
                Lexicon.builtinEqualityRightAdjective
                [term y]
        copular =
            Raw.StmtVerbPhrase
                (term x :| [])
                (Raw.VPAdj (adjective :| []))
        rightAttribute =
            Raw.StmtNoun
                (term x :| [])
                (Raw.NounPhrase
                    []
                    (Raw.Noun Nowhere Lexicon.builtinSetNoun [])
                    Nothing
                    [ Raw.AdjR
                        Nowhere
                        Lexicon.builtinEqualityRightAdjective
                        [term y]
                    ]
                    Nothing)
        rightAttributeExpected =
            Raw.StmtNoun
                (term x :| [])
                (Raw.NounPhrase
                    []
                    (Raw.Noun Nowhere Lexicon.builtinSetNoun [])
                    Nothing
                    []
                    (Just (equality x y)))
        verb argument =
            Raw.Verb
                Nowhere
                Lexicon.builtinEqualityVerb
                [term argument]
        singular =
            Raw.StmtVerbPhrase
                (term x :| [])
                (Raw.VPVerb (verb y))
        negated =
            Raw.StmtVerbPhrase
                (term x :| [])
                (Raw.VPVerbNot (verb y))
        coordinated =
            Raw.StmtVerbPhrase
                (term x :| [term y])
                (Raw.VPVerb (verb z))
        coordinatedExpected =
            Raw.StmtConnected
                Raw.Conjunction
                Nothing
                (equality x z)
                (equality y z)
        comparisons =
            [ ( "copular adjective"
              , quantified (x :| [y]) copular
              , quantified (x :| [y]) (equality x y)
              )
            , ( "right adjective"
              , quantified (x :| [y]) rightAttribute
              , quantified (x :| [y]) rightAttributeExpected
              )
            , ( "singular verb"
              , quantified (x :| [y]) singular
              , quantified (x :| [y]) (equality x y)
              )
            , ( "negated verb"
              , quantified (x :| [y]) negated
              , quantified
                    (x :| [y])
                    (Raw.StmtNeg Nowhere (equality x y))
              )
            , ( "quantified coordinated verb"
              , quantified (x :| [y, z]) coordinated
              , quantified (x :| [y, z]) coordinatedExpected
              )
            ]
        action
            :: Declaration.ModuleDriver Text
                [ ( Either
                        Exact.ExactCompileError
                        Exact.PreparedExactProposition
                  , Either
                        Exact.ExactCompileError
                        Exact.PreparedExactProposition
                  )
                ]
        action =
            Declaration.runProspectiveLoweringDriver
                (traverse
                    (\(_label, alias, symbolic) ->
                        (,)
                            <$> Exact.prepareExactProposition
                                Exact.emptyExactBinderContext alias
                            <*> Exact.prepareExactProposition
                                Exact.emptyExactBinderContext symbolic)
                    comparisons)
    runDriver fixture action >>= \case
        Declaration.DriverSucceeded results _interface _prefix _closure ->
            for_ (zip comparisons results) \((label, _alias, _symbolic), result) ->
                case result of
                    (Right alias, Right symbolic) -> do
                        let aliasTerm =
                                Core.scopedCoreTerm
                                    (Exact.preparedExactPropositionCore alias)
                            symbolicTerm =
                                Core.scopedCoreTerm
                                    (Exact.preparedExactPropositionCore symbolic)
                        assertEqual
                            (label <> " checked core")
                            symbolicTerm
                            aliasTerm
                        assertEqual
                            (label <> " global support")
                            Set.empty
                            (Core.canonicalTermGlobals aliasTerm)
                        assertEqual
                            (label <> " foundation support")
                            Set.empty
                            (Foundation.foundationAxiomDependencies aliasTerm)
                    (Left failure, _) ->
                        assertFailure
                            (label <> " alias failed: "
                                <> Text.unpack
                                    (Exact.renderExactCompileError failure))
                    (_, Left failure) ->
                        assertFailure
                            (label <> " symbolic comparison failed: "
                                <> Text.unpack
                                    (Exact.renderExactCompileError failure))
        Declaration.DriverFailed failure _prefix ->
            assertFailure ("fixed equality driver failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure ("fixed equality driver did not seal: " <> show failure)

    let internalEquality =
            Internal.FormulaVerb
                Nowhere
                (Internal.EmptySet Nowhere)
                Lexicon.builtinEqualityVerb
                [Internal.EmptySet Nowhere]
        internalResult
            :: Either
                Typed.TypedInductiveError
                (Core.FrozenCheckedCore Void)
        internalResult =
            Typed.prepareTypedClosedFormula
                absurd
                (const Nothing)
                internalEquality
    case internalResult of
        Right checked -> do
            assertEqual
                "internal fixed verb core"
                (Core.CEq
                    Core.TySet
                    (Core.CIntrinsic Core.Empty)
                    (Core.CIntrinsic Core.Empty))
                (Core.frozenCoreTerm checked)
            assertEqual
                "internal fixed verb global support"
                Set.empty
                (Core.frozenCoreGlobals checked)
        Left failure ->
            assertFailure
                ("internal fixed verb failed: " <> show failure)

scopesQuantifiedPropositionTerms :: Assertion
scopesQuantifiedPropositionTerms = do
    fixture <- makeNamedFixture "quantified-proposition-terms"
    let x = Raw.NamedVar "x"
        y = Raw.NamedVar "y"
        term variable = Raw.TermExpr (Raw.ExprVar variable)
        zero = Raw.TermExpr (Raw.ExprInteger Nowhere 0)
        setNoun = Raw.Noun Nowhere Lexicon.builtinSetNoun []
        setPhrase named = Raw.NounPhrase [] setNoun named [] Nothing
        quantified quantifier variable =
            Raw.TermQuantified
                quantifier Nowhere (setPhrase (Just variable))
        equalityVerb argument =
            Raw.Verb Nowhere Lexicon.builtinEqualityVerb [argument]
        equalityAdjective argument =
            Raw.Adj
                Nowhere Lexicon.builtinEqualityRightAdjective [argument]
        equality left right = Core.CEq Core.TySet left right
        notP proposition = Core.CImp proposition Core.CFalsum
        andP left right = notP (Core.CImp left (notP right))
        existsP body = notP (Core.CForall Core.TySet (notP body))
        truth = Core.CImp Core.CFalsum Core.CFalsum
        member left right =
            Core.CApp
                (Core.CApp (Core.CIntrinsic Core.Member) left)
                right
        soleSubject =
            Raw.StmtNoun
                (quantified Raw.Universally x :| [])
                (setPhrase Nothing)
        explicitSubject =
            Raw.SymbolicQuantified
                Nowhere Raw.Universally (x :| []) Raw.Unbounded Nothing
                (Raw.StmtNoun (term x :| []) (setPhrase Nothing))
        multipleSubjects =
            Raw.StmtVerbPhrase
                ( quantified Raw.Universally x
                    :| [quantified Raw.Existentially y]
                )
                (Raw.VPVerb (equalityVerb zero))
        adjectiveArgument =
            Raw.StmtVerbPhrase
                (zero :| [])
                (Raw.VPAdj
                    (equalityAdjective
                        (quantified Raw.Universally x) :| []))
        nounArgument =
            Raw.StmtNoun
                (zero :| [])
                (Raw.NounPhrase
                    []
                    (Raw.Noun
                        Nowhere Lexicon.builtinElementNoun
                        [quantified Raw.Universally x])
                    Nothing [] Nothing)
        negatedSubject =
            Raw.StmtVerbPhrase
                (quantified Raw.Universally x :| [])
                (Raw.VPVerbNot (equalityVerb zero))
        negatedArgument =
            Raw.StmtVerbPhrase
                (zero :| [])
                (Raw.VPVerbNot
                    (equalityVerb (quantified Raw.Universally x)))
        nonexistentialArgument =
            Raw.StmtVerbPhrase
                (zero :| [])
                (Raw.VPVerb
                    (equalityVerb (quantified Raw.Nonexistentially x)))
        negatedStatement =
            Raw.StmtNeg Nowhere soleSubject
        siblingConstraints =
            Raw.StmtNoun
                (zero :| [])
                (Raw.NounPhrase
                    []
                    (Raw.Noun
                        Nowhere Lexicon.builtinElementNoun
                        [quantified Raw.Universally x])
                    Nothing
                    [Raw.AdjR
                        Nowhere Lexicon.builtinEqualityRightAdjective
                        [quantified Raw.Universally y]]
                    Nothing)
        constrainedSubject =
            Raw.TermQuantified Raw.Universally Nowhere
                (Raw.NounPhrase
                    []
                    (Raw.Noun
                        Nowhere Lexicon.builtinElementNoun [term x])
                    (Just x)
                    [Raw.AdjR
                        Nowhere Lexicon.builtinEqualityRightAdjective [term x]]
                    (Just
                        (Raw.StmtVerbPhrase
                            (term x :| [])
                            (Raw.VPVerb (equalityVerb (term x))))))
        constrainedStatement =
            Raw.StmtVerbPhrase
                (constrainedSubject :| [])
                (Raw.VPVerb (equalityVerb (term x)))
        xEqualsX = equality (Core.CBound 0) (Core.CBound 0)
        cases =
            [ ( "sole quantified subject"
              , soleSubject
              , Core.CForall Core.TySet truth
              )
            , ( "explicit sole quantified subject"
              , explicitSubject
              , Core.CForall Core.TySet truth
              )
            , ( "multiple quantified subjects"
              , multipleSubjects
              , Core.CForall Core.TySet
                    (existsP
                        (andP
                            (equality
                                (Core.CBound 1) (Core.COpaqueInteger 0))
                            (equality
                                (Core.CBound 0) (Core.COpaqueInteger 0))))
              )
            , ( "quantified adjective argument"
              , adjectiveArgument
              , Core.CForall Core.TySet
                    (equality (Core.COpaqueInteger 0) (Core.CBound 0))
              )
            , ( "quantified noun argument"
              , nounArgument
              , Core.CForall Core.TySet
                    (member (Core.COpaqueInteger 0) (Core.CBound 0))
              )
            , ( "quantified subject outside negation"
              , negatedSubject
              , Core.CForall Core.TySet
                    (notP
                        (equality
                            (Core.CBound 0) (Core.COpaqueInteger 0)))
              )
            , ( "quantified argument inside negation"
              , negatedArgument
              , notP
                    (Core.CForall Core.TySet
                        (equality
                            (Core.COpaqueInteger 0) (Core.CBound 0)))
              )
            , ( "nonexistential quantified verb argument"
              , nonexistentialArgument
              , notP
                    (existsP
                        (equality
                            (Core.COpaqueInteger 0)
                            (Core.CBound 0)))
              )
            , ( "statement recursion bounds a quantified subject"
              , negatedStatement
              , notP (Core.CForall Core.TySet truth)
              )
            , ( "sibling constraints own their argument quantifiers"
              , siblingConstraints
              , andP
                    (Core.CForall Core.TySet
                        (member
                            (Core.COpaqueInteger 0)
                            (Core.CBound 0)))
                    (Core.CForall Core.TySet
                        (equality
                            (Core.COpaqueInteger 0)
                            (Core.CBound 0)))
              )
            , ( "quantified noun constraints share their binder"
              , constrainedStatement
              , Core.CForall Core.TySet
                    (Core.CImp
                        (andP
                            (member (Core.CBound 0) (Core.CBound 0))
                            (andP xEqualsX xEqualsX))
                        xEqualsX)
              )
            ]
        prepare context statement =
            Exact.prepareExactProposition context statement
    activeContext <- expectRight
        (Exact.extendExactBinderContext
            ((Exact.exactLocalId 0, x) :| [])
            Exact.emptyExactBinderContext)
    let action
            :: Declaration.ModuleDriver Text
                ( [ Either
                        Exact.ExactCompileError
                        Exact.PreparedExactProposition
                  ]
                , Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition
                )
        action =
            Declaration.runProspectiveLoweringDriver do
                compiled <- traverse
                    (\(_label, statement, _expected) ->
                        prepare Exact.emptyExactBinderContext statement)
                    cases
                collision <- prepare activeContext soleSubject
                pure (compiled, collision)
    runDriver fixture action >>= \case
        Declaration.DriverSucceeded
                (compiled, collision) _interface _prefix _closure -> do
            for_ (zip cases compiled) \
                    ((label, _statement, expected), result) ->
                case result of
                    Right prepared ->
                        assertEqual label expected
                            (Core.scopedCoreTerm
                                (Exact.preparedExactPropositionCore prepared))
                    Left failure ->
                        assertFailure
                            (label <> " failed: "
                                <> Text.unpack
                                    (Exact.renderExactCompileError failure))
            case collision of
                Left (Exact.ExactDuplicateLocalBinder _location variable) ->
                    assertEqual "quantified binder collision" x variable
                Left failure ->
                    assertFailure
                        ("unexpected quantified-binder collision: "
                            <> Text.unpack
                                (Exact.renderExactCompileError failure))
                Right{} ->
                    assertFailure "an active quantified binder was shadowed"
            case compiled of
                Right sole : Right explicit : _ ->
                    assertEqual
                        "sole-subject lowering remains byte-for-byte identical"
                        (Exact.preparedExactPropositionCore sole)
                        (Exact.preparedExactPropositionCore explicit)
                _ ->
                    assertFailure
                        "sole-subject equality comparison did not compile"
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("quantified proposition-term driver failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("quantified proposition-term driver did not seal: "
                    <> show failure)

preparesExactClaimEnvelopes :: Assertion
preparesExactClaimEnvelopes = do
    fixture <- makeNamedFixture "exact-claim-envelope"
    let bLocation = mkLocation (FileId 78) 2 11
        aLocation = mkLocation (FileId 78) 2 15
        xLocation = mkLocation (FileId 78) 3 9
        b = Raw.NamedVarAt bLocation "b"
        a = Raw.NamedVarAt aLocation "a"
        x = Raw.NamedVarAt xLocation "x"
        c = Raw.NamedVarAt Nowhere "c"
        d = Raw.NamedVarAt Nowhere "d"
        z = Raw.NamedVarAt Nowhere "z"
        equality left right =
            Raw.StmtFormula
                (Raw.FormulaChain
                    (Raw.ChainBase
                        (Raw.ExprVar left :| [])
                        Raw.Positive
                        (Raw.Relation Nowhere Raw.EqSymbol [])
                        (Raw.ExprVar right :| [])))
        quantified variable body =
            Raw.SymbolicQuantified
                (locate variable)
                Raw.Universally
                (variable :| [])
                Raw.Unbounded
                Nothing
                body
        sourceAssumptions = [Raw.AsmSuppose (equality b a)]
        sourceConclusion = quantified x (equality x b)
        alphaAssumptions = [Raw.AsmSuppose (equality c d)]
        alphaConclusion = quantified z (equality z c)
        action
            :: Declaration.ModuleDriver Text
                ( Either
                    Exact.ExactCompileError
                    Exact.PreparedExactClaimEnvelope
                , Either
                    Exact.ExactCompileError
                    Exact.PreparedExactClaimEnvelope
                )
        action =
            Declaration.runProspectiveLoweringDriver do
                source <- Exact.prepareExactClaimEnvelope
                    sourceAssumptions sourceConclusion
                alpha <- Exact.prepareExactClaimEnvelope
                    alphaAssumptions alphaConclusion
                pure (source, alpha)
        expected =
            Core.CForall Core.TySet
                (Core.CForall Core.TySet
                    (Core.CImp
                        (Core.CEq Core.TySet
                            (Core.CBound 1)
                            (Core.CBound 0))
                        (Core.CForall Core.TySet
                            (Core.CEq Core.TySet
                                (Core.CBound 0)
                                (Core.CBound 2)))))
    runDriver fixture action >>= \case
        Declaration.DriverSucceeded
                (Right source, Right alpha)
                _interface _prefix _closure -> do
            let sourceTarget = Exact.preparedExactClaimTarget source
                alphaTarget = Exact.preparedExactClaimTarget alpha
            assertEqual "closed claim envelope core"
                expected
                (Core.scopedCoreTerm sourceTarget)
            assertEqual "claim envelope is closed"
                []
                (Core.scopedCoreContext sourceTarget)
            assertEqual "first semantic occurrence binder order"
                [bLocation, aLocation]
                (locate <$> Exact.preparedExactClaimVariables source)
            assertEqual "explicit binders are not generalized"
                2
                (length (Exact.preparedExactClaimVariables source))
            assertEqual "header antecedent count"
                1
                (Exact.preparedExactClaimAntecedentCount source)
            assertEqual "alpha-renaming preserves the checked target"
                sourceTarget alphaTarget
            assertEqual "alpha-renaming preserves proposition identity"
                (Identity.propositionIdOf
                    (Core.scopedCoreTerm sourceTarget))
                (Identity.propositionIdOf
                    (Core.scopedCoreTerm alphaTarget))
        Declaration.DriverSucceeded result _interface _prefix _closure ->
            assertFailure
                ("exact claim envelope preparation failed: "
                    <> case result of
                        (Left failure, _) ->
                            Text.unpack
                                (Exact.renderExactCompileError failure)
                        (_, Left failure) ->
                            Text.unpack
                                (Exact.renderExactCompileError failure))
        Declaration.DriverFailed failure _prefix ->
            assertFailure ("claim envelope driver failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("claim envelope driver did not seal: " <> show failure)

lowersExactSeparationComprehensions :: Assertion
lowersExactSeparationComprehensions = do
    fixture <- makeNamedFixture "exact-separation-comprehension"
    let binderLocation = mkLocation (FileId 73) 2 7
        ambientLocation = mkLocation (FileId 73) 2 18
        boundOccurrenceLocation = mkLocation (FileId 73) 3 14
        x = Raw.NamedVarAt binderLocation "x"
        a = Raw.NamedVarAt ambientLocation "A"
        equality left right =
            Raw.StmtFormula
                (Raw.FormulaChain
                    (Raw.ChainBase
                        (left :| [])
                        Raw.Positive
                        (Raw.Relation Nowhere Raw.EqSymbol [])
                        (right :| [])))
        separation bound =
            Raw.ExprSep
                binderLocation
                x
                bound
                (equality (Raw.ExprVar x) (Raw.ExprVar a))
        validStatement =
            Raw.SymbolicQuantified
                Nowhere
                Raw.Universally
                (a :| [])
                Raw.Unbounded
                Nothing
                (equality
                    (separation (Raw.ExprVar a))
                    (Raw.ExprVar a))
        boundOccurrence =
            Raw.NamedVarAt boundOccurrenceLocation "x"
        invalidStatement =
            equality
                (separation (Raw.ExprVar boundOccurrence))
                (Raw.ExprVar a)
        action
            :: Declaration.ModuleDriver Text
                ( Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition
                , Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition
                )
        action =
            Declaration.runProspectiveLoweringDriver do
                valid <- Exact.prepareExactProposition
                    Exact.emptyExactBinderContext
                    validStatement
                invalid <- Exact.prepareExactProposition
                    Exact.emptyExactBinderContext
                    invalidStatement
                pure (valid, invalid)
    outcome <- runDriver fixture action
    case outcome of
        Declaration.DriverSucceeded
                (Right prepared, Left failure) _interface _prefix _closure -> do
            assertEqual
                "separation comprehension core"
                (Core.CForall Core.TySet
                    (Core.CEq 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 1))))
                        (Core.CBound 0)))
                (Core.scopedCoreTerm
                    (Exact.preparedExactPropositionCore prepared))
            assertEqual
                "separation proposition type"
                Core.TyProp
                (Core.scopedCoreType
                    (Exact.preparedExactPropositionCore prepared))
            assertEqual
                "the separation binder is unavailable in its bound"
                (Exact.ExactFreeVariable
                    boundOccurrenceLocation
                    boundOccurrence)
                failure
        Declaration.DriverSucceeded result _interface _prefix _closure ->
            case result of
                (Left validFailure, _) ->
                    assertFailure
                        ("valid separation failed: "
                            <> Text.unpack
                                (Exact.renderExactCompileError validFailure))
                (_, Right{}) ->
                    assertFailure "invalid separation was accepted"
        Declaration.DriverFailed failure _prefix ->
            assertFailure ("separation exact driver failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure ("separation exact driver did not seal: " <> show failure)

lowersExactReplacementTelescopes :: Assertion
lowersExactReplacementTelescopes = do
    fixture <- makeNamedFixture "exact-replacement-telescope"
    let location = mkLocation (FileId 74) 2 1
        futureOccurrenceLocation = mkLocation (FileId 74) 7 19
        a = Raw.NamedVarAt location "A"
        x = Raw.NamedVarAt location "x"
        y = Raw.NamedVarAt location "y"
        futureY = Raw.NamedVarAt futureOccurrenceLocation "y"
        equality left right =
            Raw.StmtFormula
                (Raw.FormulaChain
                    (Raw.ChainBase
                        (left :| [])
                        Raw.Positive
                        (Raw.Relation Nowhere Raw.EqSymbol [])
                        (right :| [])))
        replacement firstDomain =
            Raw.ExprReplace
                location
                (Raw.ExprVar y)
                ( (x, firstDomain) :|
                    [(y, Raw.ExprVar x)]
                )
                (Just (equality (Raw.ExprVar x) (Raw.ExprVar y)))
        validStatement =
            Raw.SymbolicQuantified
                Nowhere
                Raw.Universally
                (a :| [])
                Raw.Unbounded
                Nothing
                (equality
                    (replacement (Raw.ExprVar a))
                    (Raw.ExprVar a))
        invalidStatement =
            equality
                (replacement (Raw.ExprVar futureY))
                (Raw.ExprInteger Nowhere 0)
        predicateReplacementLocation = mkLocation (FileId 74) 9 3
        predicateReplacementStatement =
            equality
                (Raw.ExprReplacePred
                    predicateReplacementLocation
                    y
                    x
                    (Raw.ExprInteger Nowhere 0)
                    (equality (Raw.ExprVar x) (Raw.ExprVar y)))
                (Raw.ExprInteger Nowhere 0)
        namedPredicateReplacement =
            Raw.ExprReplacePred
                predicateReplacementLocation
                y
                x
                (Raw.ExprVar a)
                (equality (Raw.ExprVar x) (Raw.ExprVar y))
        app1 intrinsic argument =
            Core.CApp (Core.CIntrinsic intrinsic) argument
        app2 intrinsic first second =
            Core.CApp (app1 intrinsic first) second
        expected =
            Core.CForall Core.TySet $
                Core.CEq 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)))
                    (Core.CBound 0)
        action
            :: Declaration.ModuleDriver Text
                ( Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition
                , Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition
                , Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition
                , Either
                    Exact.ExactCompileError
                    Exact.PreparedExactSetExpression
                )
        action =
            Declaration.runProspectiveLoweringDriver do
                valid <- Exact.prepareExactProposition
                    Exact.emptyExactBinderContext
                    validStatement
                invalid <- Exact.prepareExactProposition
                    Exact.emptyExactBinderContext
                    invalidStatement
                predicateReplacement <- Exact.prepareExactProposition
                    Exact.emptyExactBinderContext
                    predicateReplacementStatement
                namedContext <-
                    either
                        (impossible
                            . Text.unpack
                            . Exact.renderExactCompileError)
                        pure
                        (Exact.extendExactBinderContext
                            ((Exact.exactLocalId 0, a) :| [])
                            Exact.emptyExactBinderContext)
                named <- Exact.prepareExactSetExpression
                    namedContext namedPredicateReplacement
                pure (valid, invalid, predicateReplacement, named)
    runDriver fixture action >>= \case
        Declaration.DriverSucceeded
                ( Right prepared
                    , Left failure
                    , Left predicateReplacementFailure
                    , Right named
                    ) _interface _prefix _closure -> do
            assertEqual
                "dependent replacement core"
                expected
                (Core.scopedCoreTerm
                    (Exact.preparedExactPropositionCore prepared))
            assertEqual
                "future replacement binder location"
                (Exact.ExactFreeVariable futureOccurrenceLocation futureY)
                failure
            assertEqual
                "predicate replacement remains unsupported at its location"
                (Exact.ExactRelationalReplacementRequiresNamedDefinition
                    predicateReplacementLocation)
                predicateReplacementFailure
            case Exact.preparedExactSetExpressionConstruction named of
                Just (Exact.PreparedRelationalSetConstruction construction) -> do
                    assertEqual "relational replacement canonical term"
                        expectedRelationalTerm
                        (Core.scopedCoreTerm
                            (SetConstruction.relationalSetConstructionTerm
                                construction))
                    assertEqual "relational replacement functionality"
                        expectedFunctionality
                        (Core.scopedCoreTerm
                            (SetConstruction.relationalSetConstructionFunctionality
                                construction))
                    let relationalObject =
                            Identity.assertedObjectId
                                (opaqueFixtureObject fixture)
                        closedFunctionality =
                            SetConstruction.relationalSetConstructionClosedFunctionality
                                construction
                    relationalFact <-
                        maybe
                            (assertFailure
                                "exact functionality did not unlock relational extensionality"
                                >> fail "unreachable")
                            pure
                            (SetConstruction.relationalSetConstructionObjectFact
                                (SetConstruction.checkedFoundationSetConstruction
                                    (fixtureFoundation fixture))
                                relationalObject
                                construction
                                closedFunctionality)
                    assertEqual
                        "relational replacement flattened extensional proposition"
                        (expectedRelationalExtensional relationalObject)
                        (Core.frozenCoreTerm
                            (SetConstruction.relationalSetConstructionFactProposition
                                relationalFact))
                    assertEqual
                        "unrelated functionality cannot unlock the relational view"
                        Nothing
                        (SetConstruction.relationalSetConstructionLocalViews
                            (SetConstruction.checkedFoundationSetConstruction
                                (fixtureFoundation fixture))
                            construction
                            (Core.falsumScopedCore [Core.TySet]))
                    wrongClosed <- expectRight
                        (Core.checkCanonicalCore
                            (const Nothing)
                            Core.CFalsum)
                    assertBool
                        "malformed relational authority is rejected"
                        (isNothing
                            (SetConstruction.relationalSetConstructionObjectFact
                                (SetConstruction.checkedFoundationSetConstruction
                                    (fixtureFoundation fixture))
                                relationalObject
                                construction
                                wrongClosed))
                _ ->
                    assertFailure
                        "named predicate replacement lost its relational construction"
        Declaration.DriverSucceeded
                (Left validFailure, _, _, _) _interface _prefix _closure ->
            assertFailure
                ("valid replacement failed: "
                    <> Text.unpack
                        (Exact.renderExactCompileError validFailure))
        Declaration.DriverSucceeded
                (_, Right{}, _, _) _interface _prefix _closure ->
            assertFailure "invalid replacement was accepted"
        Declaration.DriverSucceeded
                (_, _, Right{}, _) _interface _prefix _closure ->
            assertFailure "predicate replacement was accepted"
        Declaration.DriverSucceeded
                (_, _, _, Left failure) _interface _prefix _closure ->
            assertFailure
                ("named predicate replacement failed: "
                    <> Text.unpack (Exact.renderExactCompileError failure))
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("replacement driver failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("replacement driver did not seal: " <> show failure)
  where
    relApp1 intrinsic argument =
        Core.CApp (Core.CIntrinsic intrinsic) argument
    relApp2 intrinsic first second =
        Core.CApp (relApp1 intrinsic first) second
    notP proposition = Core.CImp proposition Core.CFalsum
    andP left right = notP (Core.CImp left (notP right))
    existsP body = notP (Core.CForall Core.TySet (notP body))
    relation = Core.CEq Core.TySet (Core.CBound 1) (Core.CBound 0)
    restricted =
        relApp2 Core.Sep (Core.CBound 0)
            (Core.CLam Core.TySet (existsP relation))
    expectedRelationalTerm =
        relApp2 Core.Repl restricted
            (Core.CLam Core.TySet
                (relApp1 Core.SetChoose (Core.CLam Core.TySet relation)))
    expectedFunctionality =
        Core.CForall Core.TySet
            (Core.CImp
                (relApp2 Core.Member (Core.CBound 0) (Core.CBound 1))
                (Core.CForall Core.TySet
                    (Core.CForall Core.TySet
                        (Core.CImp
                            (andP
                                (Core.CEq Core.TySet
                                    (Core.CBound 2) (Core.CBound 1))
                                (Core.CEq Core.TySet
                                    (Core.CBound 2) (Core.CBound 0)))
                            (Core.CEq Core.TySet
                                (Core.CBound 1) (Core.CBound 0))))))
    expectedRelationalExtensional object =
        Core.CForall Core.TySet
            (Core.CForall Core.TySet
                (Core.CEq Core.TyProp
                    (relApp2 Core.Member
                        (Core.CBound 0)
                        (Core.CApp
                            (Core.CGlobal object)
                            (Core.CBound 1)))
                    (existsP
                        (andP
                            (relApp2 Core.Member
                                (Core.CBound 0)
                                (Core.CBound 2))
                            (Core.CEq Core.TySet
                                (Core.CBound 0)
                                (Core.CBound 1))))))

lowersExactFiniteSets :: Assertion
lowersExactFiniteSets = do
    fixture <- makeNamedFixture "exact-finite-set"
    let location = mkLocation (FileId 75) 2 1
        a = Raw.NamedVarAt location "a"
        b = Raw.NamedVarAt location "b"
        equality left right =
            Raw.StmtFormula
                (Raw.FormulaChain
                    (Raw.ChainBase
                        (left :| [])
                        Raw.Positive
                        (Raw.Relation Nowhere Raw.EqSymbol [])
                        (right :| [])))
        statement =
            Raw.SymbolicQuantified
                Nowhere
                Raw.Universally
                (a :| [b])
                Raw.Unbounded
                Nothing
                (equality
                    (Raw.ExprFiniteSet
                        location
                        (Raw.ExprVar a :| [Raw.ExprVar b]))
                    (Raw.ExprVar a))
        app1 intrinsic argument =
            Core.CApp (Core.CIntrinsic intrinsic) argument
        app2 intrinsic first second =
            Core.CApp (app1 intrinsic first) second
        insert element rest =
            app1 Core.FamilyUnion
                (app2 Core.PairSet
                    (app2 Core.PairSet element element)
                    rest)
        expected =
            Core.CForall Core.TySet
                (Core.CForall Core.TySet
                    (Core.CEq Core.TySet
                        (insert
                            (Core.CBound 1)
                            (insert
                                (Core.CBound 0)
                                (Core.CIntrinsic Core.Empty)))
                        (Core.CBound 1)))
        action
            :: Declaration.ModuleDriver Text
                (Either
                    Exact.ExactCompileError
                    Exact.PreparedExactProposition)
        action =
            Declaration.runProspectiveLoweringDriver
                (Exact.prepareExactProposition
                    Exact.emptyExactBinderContext
                    statement)
    internal <-
        expectRight
            (evalState
                (runExceptT (Meaning.glossStmt statement))
                Meaning.initialGlossState)
    reusable <-
        expectRight
            (Typed.prepareTypedClosedFormula
                absurd
                (const Nothing)
                internal
                :: Either
                    Typed.TypedInductiveError
                    (Core.FrozenCheckedCore Void))
    assertEqual
        "raw and reusable finite-set lowering"
        expected
        (Core.frozenCoreTerm reusable)
    let internalSymbols = Internal.mentionedSymbols internal
    assertBool
        "finite-set meaning has no source-owned cons dependency"
        (Internal.SymbolMixfix Raw.ConsSymbol
            `Set.notMember` internalSymbols)
    assertBool
        "finite-set meaning retains fixed adjunction operations"
        ( Set.fromList
            [ Internal.SymbolMixfix Raw.UnionsSymbol
            , Internal.SymbolMixfix Raw.UpairSymbol
            ]
            `Set.isSubsetOf` internalSymbols
        )
    case Vocabulary.classifyExactSymbol
            (Internal.SymbolMixfix Raw.ConsSymbol) of
        Vocabulary.ExactSourceGlobal{} -> pure ()
        classification ->
            assertFailure
                ("explicit cons did not retain source ownership: "
                    <> show classification)
    runDriver fixture action >>= \case
        Declaration.DriverSucceeded
                (Right prepared) _interface _prefix _closure ->
            assertEqual
                "source-order finite-set core"
                expected
                (Core.scopedCoreTerm
                    (Exact.preparedExactPropositionCore prepared))
        Declaration.DriverSucceeded
                (Left failure) _interface _prefix _closure ->
            assertFailure
                ("valid finite set failed: "
                    <> Text.unpack
                        (Exact.renderExactCompileError failure))
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("finite-set driver failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("finite-set driver did not seal: " <> show failure)

lowersExactOrdinaryDeclarations :: Assertion
lowersExactOrdinaryDeclarations = do
    fixture <- makeNamedFixture "exact-lowering"
    level <- expectRight (Syntax.mixfixLevel 2)
    let makeSymbol command marker =
            Raw.mkMixfixItem
                [ Just (Raw.Command command)
                , Just Raw.InvisibleBraceL
                , Nothing
                , Just Raw.InvisibleBraceR
                ]
                (Raw.Marker marker)
                Raw.NonAssoc
        opaqueSymbol = makeSymbol "phasefiveopaque" "opaque-label"
        aliasSymbol = makeSymbol "phasefivealias" "alias-label"
        definitionSymbol = makeSymbol "phasefivedef" "definition-label"
        entry symbol =
            Syntax.CanonicalExpressionFunction
                (Raw.mixfixPattern symbol)
                (Raw.mixfixMarker symbol)
                (Syntax.Fixity Raw.NonAssoc level)
        parameter = Raw.NamedVar "x"
        exactSet =
            Raw.NounPhrase
                []
                (Raw.Noun Nowhere Lexicon.builtinSetNoun [])
                Nothing
                []
                Nothing
        signature =
            Raw.BlockSig
                Nowhere Nothing (Raw.Marker "opaque-declaration") []
                (Raw.SignatureSymbolic
                    (Raw.SymbolPattern opaqueSymbol [parameter])
                    exactSet)
        application symbol =
            Raw.ExprOp Nowhere symbol [Raw.ExprVar parameter]
        abbreviation =
            Raw.BlockAbbr
                Nowhere Nothing (Raw.Marker "alias-declaration")
                (Raw.AbbreviationEq
                    (Raw.SymbolPattern aliasSymbol [parameter])
                    (application opaqueSymbol))
        definition =
            Raw.BlockDefn
                Nowhere Nothing (Raw.Marker "definition-declaration")
                (Raw.DefnOp
                    (Raw.SymbolPattern definitionSymbol [parameter])
                    (application aliasSymbol))
        compile block lexicalEntry = do
            Declaration.runProspectiveLoweringDriver
                (Exact.prepareExactDeclaration block [lexicalEntry]) >>= \case
                Left failure ->
                    Declaration.failModuleDriver
                        (Exact.renderExactCompileError failure)
                Right prepared -> pure prepared
        admit prepared = do
            lowered <-
                Declaration.runProspectiveLoweringDriver
                    (Exact.lowerPreparedExactBinding prepared)
            checked <-
                either Declaration.failDeclarationDriver pure lowered
            void
                (Declaration.admitCheckedDeclaration
                    checked
                    Exact.authorizeCheckedExactBinding)
    outcome <- runFixtureDriver fixture [] do
        preparedSignature <-
            compile signature (entry opaqueSymbol)
        admit preparedSignature
        preparedAbbreviation <-
            compile abbreviation (entry aliasSymbol)
        admit preparedAbbreviation
        preparedDefinition <-
            compile definition (entry definitionSymbol)
        admit preparedDefinition
        pure
            ( preparedSignature
            , preparedAbbreviation
            , preparedDefinition
            )
    case outcome of
        Declaration.DriverSucceeded
                (preparedSignature, preparedAbbreviation, preparedDefinition)
                interface prefix _closure -> do
            assertEqual "three committed declarations"
                3
                (length (Semantic.semanticInterfaceDeclarations interface))
            assertEqual "three committed batches"
                3
                (length (Declaration.pendingModulePrefixBatches prefix))
            assertEqual "opaque signature family"
                Identity.OpaqueObject
                (Identity.objectIdFamily
                    (Exact.preparedExactObjectId preparedSignature))
            assertEqual "transparent abbreviation family"
                Identity.TransparentObject
                (Identity.objectIdFamily
                    (Exact.preparedExactObjectId preparedAbbreviation))
            assertEqual "transparent definition family"
                Identity.TransparentObject
                (Identity.objectIdFamily
                    (Exact.preparedExactObjectId preparedDefinition))
            assertEqual "expanded definition coalesces with abbreviation"
                (Exact.preparedExactObjectId preparedAbbreviation)
                (Exact.preparedExactObjectId preparedDefinition)
            case Exact.preparedExactObject preparedAbbreviation of
                Just object ->
                    case Identity.assertedObjectContent object of
                        Identity.TransparentObjectContent
                                _theory coreType body -> do
                            assertEqual "definition type"
                                (Core.TyArrow Core.TySet Core.TySet)
                                coreType
                            assertEqual "expanded body retains opaque seed"
                                (Core.CLam Core.TySet
                                    (Core.CApp
                                        (Core.CGlobal
                                            (Exact.preparedExactObjectId
                                                preparedSignature))
                                        (Core.CBound 0)))
                                body
                        content ->
                            assertFailure
                                ("unexpected definition content: " <> show content)
                Nothing ->
                    assertFailure "new abbreviation object was not prepared"
            assertEqual "coalesced definition adds no object"
                Nothing
                (Exact.preparedExactObject preparedDefinition)
            case reverse (Declaration.pendingModulePrefixBatches prefix) of
                definitionBatch : _ -> do
                    case Declaration.committedBatchDeclarationValidation
                            definitionBatch of
                        Just record ->
                            case Semantic.declarationValidationRecordCertificates
                                    record of
                                [certificate] -> do
                                    assertEqual "definition authority"
                                        (Authority.CheckedKernelConstruction
                                            (Authority.CheckedDefinitionEquation
                                                (Exact.preparedExactObjectId
                                                    preparedDefinition)))
                                        (Authority.validationDirectAuthorization
                                            certificate)
                                    assertEqual "definition authority is clean"
                                        Authority.cleanAuthoritySafety
                                        (Authority.factAuthoritySafety
                                            (Authority.validationTarget
                                                certificate))
                                certificates ->
                                    assertFailure
                                        ("unexpected definition certificate count: "
                                            <> show (length certificates))
                        Nothing ->
                            assertFailure "definition has no declaration validation"
                [] -> assertFailure "definition batch is absent"
        Declaration.DriverFailed failure _prefix ->
            assertFailure ("exact lowering failed: " <> show failure)
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure ("exact lowering did not seal: " <> show failure)

    let theory = Identity.theoryId (fixtureFoundation fixture)
        mismatchBody = Core.COpaqueInteger 0
        mismatchType = Core.TySet
        mismatchId =
            Identity.transparentObjectId theory mismatchType mismatchBody
        mismatchObject =
            Identity.assertedObject
                mismatchId
                (Identity.TransparentObjectContent
                    theory mismatchType mismatchBody)
    let mismatchAction
            :: Declaration.ModuleDriver Text
                ((), Declaration.CommittedDeclarationBatch)
        mismatchAction =
            Declaration.commitCompiledDeclaration
                (Semantic.declarationSyntaxId
                    "mismatched-definition-equation") do
                    Declaration.addDeclarationObject mismatchObject
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "not-a-definition-equation")
                    Declaration.authorizeCompiledDeclaration
                        (Declaration.authorizeDefinitionEquationCandidate
                            mismatchId
                            candidate)
    mismatch <- runDriver fixture mismatchAction
    case mismatch of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    Declaration.DefinitionEquationCandidateMismatch)
                prefix ->
            assertEqual "mismatched equation publishes no batch"
                0
                (length (Declaration.pendingModulePrefixBatches prefix))
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("unexpected mismatched-equation failure: " <> show failure)
        Declaration.DriverSucceeded{} ->
            assertFailure "mismatched definition equation was authorized"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("mismatched definition equation reached sealing: "
                    <> show failure)

reconstructsImportedGlobalBindings :: Assertion
reconstructsImportedGlobalBindings = do
    producerFixture <- makeNamedFixture "global-producer"
    consumerFixture <- makeNamedFixture "global-consumer"
    conflictFixture <- makeNamedFixture "global-conflict"
    rootFixture <- makeNamedFixture "global-root"
    let key =
            Semantic.SemanticExpressionFunction
                (Raw.TokenCons (Raw.Command "phasefive") Raw.End)
        asserted = opaqueFixtureObject producerFixture
        target = Identity.assertedObjectId asserted
        publishWith targetMode fixture object = do
            (batch, sealed) <- sealFixture fixture [] do
                (_value, committed) <-
                    Declaration.commitCompiledDeclaration
                        (Semantic.declarationSyntaxId "global-binding") do
                            Declaration.addDeclarationObject object
                            Declaration.stageSemanticGlobalBinding
                                key
                                (targetMode
                                    (Identity.assertedObjectId object))
                            Declaration.authorizeCompiledDeclaration (pure ())
                pure committed
            pure (batch, sealed)
    (producerBatch, freshProducer) <-
        publishWith Semantic.GlobalReference producerFixture asserted
    let FixtureSealed producerInterface _freshEvidence = freshProducer
        objects = Declaration.committedBatchObjects producerBatch
    cachedEvidence <- expectRight
        (Declaration.validateImportedModuleEvidence
            (Identity.theoryId
                (fixtureFoundation producerFixture))
            []
            producerInterface
            objects
            [])
    let cachedProducer = FixtureSealed producerInterface cachedEvidence
        resolveThrough label parent = do
            outcome <- runFixtureDriver consumerFixture [parent] do
                fst <$> Declaration.commitCompiledDeclaration
                    (Semantic.declarationSyntaxId
                        (TextEncoding.encodeUtf8 (Text.pack label))) do
                        found <- Declaration.resolveVisibleGlobal key
                        Declaration.authorizeCompiledDeclaration (pure ())
                        pure found
            case outcome of
                Declaration.DriverSucceeded found _interface _prefix _closure ->
                    assertEqual label
                        (Just
                            ( Semantic.GlobalReference target
                            , Core.TySet
                            ))
                        found
                Declaration.DriverFailed failure _prefix ->
                    assertFailure
                        ("global binding consumer failed: " <> show failure)
                Declaration.DriverSealFailed failure _prefix ->
                    assertFailure
                        ("global binding consumer did not seal: " <> show failure)
    resolveThrough "fresh-global-binding" freshProducer
    resolveThrough "cached-global-binding" cachedProducer

    missingEnvironment <- expectRight
        (Semantic.semanticEnvironmentDelta
            [Semantic.semanticGlobalBinding
                key
                (Semantic.GlobalReference target)])
    missingDelta <- expectRight
        (Semantic.declarationInterfaceDelta
            (Semantic.declarationSlot
                (fixtureOwner producerFixture)
                (localDeclarationOrdinal 0))
            []
            []
            []
            []
            missingEnvironment)
    missingInterface <- expectRight
        (Semantic.semanticInterface
            (fixtureOwner producerFixture)
            []
            [missingDelta])
    case Declaration.validateImportedModuleEvidence
            (Identity.theoryId
                (fixtureFoundation producerFixture))
            []
            missingInterface
            []
            [] of
        Left (Declaration.ImportedGlobalTargetInvalid
                actualKey actualTarget
                (Semantic.SemanticGlobalTargetMissing missingTarget)) -> do
            assertEqual "missing target key" key actualKey
            assertEqual "missing target mode"
                (Semantic.GlobalReference target)
                actualTarget
            assertEqual "missing target object" target missingTarget
        Left failure ->
            assertFailure
                ("unexpected missing-target failure: " <> show failure)
        Right _evidence ->
            assertFailure "cached evidence accepted a missing target object"

    expansionEnvironment <- expectRight
        (Semantic.semanticEnvironmentDelta
            [Semantic.semanticGlobalBinding
                key
                (Semantic.TransparentExpansion target)])
    expansionDelta <- expectRight
        (Semantic.declarationInterfaceDelta
            (Semantic.declarationSlot
                (fixtureOwner producerFixture)
                (localDeclarationOrdinal 0))
            [] [] [target] [] expansionEnvironment)
    expansionInterface <- expectRight
        (Semantic.semanticInterface
            (fixtureOwner producerFixture) [] [expansionDelta])
    case Declaration.validateImportedModuleEvidence
            (Identity.theoryId
                (fixtureFoundation producerFixture))
            []
            expansionInterface
            [asserted]
            [] of
        Left (Declaration.ImportedGlobalTargetInvalid
                actualKey actualTarget
                (Semantic.SemanticGlobalExpansionNotTransparent
                    invalidTarget)) -> do
            assertEqual "nontransparent target key" key actualKey
            assertEqual "nontransparent target mode"
                (Semantic.TransparentExpansion target)
                actualTarget
            assertEqual "nontransparent target object" target invalidTarget
        Left failure ->
            assertFailure
                ("unexpected nontransparent-target failure: "
                    <> show failure)
        Right _evidence ->
            assertFailure "cached evidence accepted a nontransparent expansion"

    let intrinsicTarget =
            Identity.intrinsicObjectId
                (Identity.theoryId
                    (fixtureFoundation producerFixture))
                Core.Empty
                Core.TySet
        intrinsicObject =
            Identity.assertedObject
                intrinsicTarget
                (Identity.IntrinsicObjectContent
                    (Identity.theoryId
                        (fixtureFoundation producerFixture))
                    Core.Empty
                    Core.TySet)
    intrinsicFailure <- runFixtureDriver producerFixture [] do
        Declaration.commitCompiledDeclaration
            (Semantic.declarationSyntaxId "intrinsic-global-binding") do
                Declaration.addDeclarationObject intrinsicObject
                Declaration.stageSemanticGlobalBinding
                    key
                    (Semantic.GlobalReference intrinsicTarget)
                Declaration.authorizeCompiledDeclaration (pure ())
    case intrinsicFailure of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    (Declaration.DeclarationGlobalTargetInvalid
                        actualKey actualTarget
                        (Semantic.SemanticGlobalTargetIsIntrinsic
                            invalidTarget)))
                _prefix -> do
            assertEqual "intrinsic target key" key actualKey
            assertEqual "intrinsic target mode"
                (Semantic.GlobalReference intrinsicTarget)
                actualTarget
            assertEqual "intrinsic target object"
                intrinsicTarget invalidTarget
        other ->
            assertFailure
                (case other of
                    Declaration.DriverSucceeded{} ->
                        "ordinary binding accepted an intrinsic target"
                    Declaration.DriverFailed failure _prefix ->
                        "unexpected intrinsic-target failure: " <> show failure
                    Declaration.DriverSealFailed failure _prefix ->
                        "intrinsic target reached sealing: " <> show failure)

    conflictObject <- pure (opaqueFixtureObject conflictFixture)
    (_conflictBatch, conflicting) <-
        publishWith Semantic.GlobalReference conflictFixture conflictObject
    collision <- runFixtureDriver rootFixture
        [freshProducer, conflicting]
        (pure ())
    case collision of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    (Declaration.ImportedGlobalCollision
                        actualKey firstTarget secondTarget))
                _prefix -> do
            assertEqual "colliding global key" key actualKey
            assertEqual "first imported target"
                (Semantic.GlobalReference target)
                firstTarget
            assertEqual "second imported target"
                (Semantic.GlobalReference
                    (Identity.assertedObjectId conflictObject))
                secondTarget
        Declaration.DriverFailed failure _prefix ->
            assertFailure
                ("unexpected imported collision: " <> show failure)
        Declaration.DriverSucceeded{} ->
            assertFailure "unequal imported bindings did not collide"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure
                ("global collision reached sealing: " <> show failure)

    let theory = Identity.theoryId (fixtureFoundation producerFixture)
        transparentBody = Core.COpaqueInteger 0
        transparentTarget =
            Identity.transparentObjectId
                theory Core.TySet transparentBody
        transparentObject =
            Identity.assertedObject
                transparentTarget
                (Identity.TransparentObjectContent
                    theory Core.TySet transparentBody)
    (_referenceBatch, referenceProducer) <-
        publishWith
            Semantic.GlobalReference
            producerFixture
            transparentObject
    (_expansionBatch, expansionProducer) <-
        publishWith
            Semantic.TransparentExpansion
            conflictFixture
            transparentObject
    modeCollision <- runFixtureDriver rootFixture
        [referenceProducer, expansionProducer]
        (pure ())
    case modeCollision of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    (Declaration.ImportedGlobalCollision
                        actualKey firstTarget secondTarget))
                _prefix -> do
            assertEqual "mode collision key" key actualKey
            assertEqual "reference target"
                (Semantic.GlobalReference transparentTarget)
                firstTarget
            assertEqual "expansion target"
                (Semantic.TransparentExpansion transparentTarget)
                secondTarget
        other ->
            assertFailure
                (case other of
                    Declaration.DriverSucceeded{} ->
                        "different global target modes did not collide"
                    Declaration.DriverFailed failure _prefix ->
                        "unexpected mode-collision failure: " <> show failure
                    Declaration.DriverSealFailed failure _prefix ->
                        "mode collision reached sealing: " <> show failure)

data FixtureSealed = FixtureSealed
    !Semantic.SemanticInterface
    !Declaration.ImportedModuleEvidence

foldsTransitiveAndDiamondEvidence :: Assertion
foldsTransitiveAndDiamondEvidence = do
    baseFixture <- makeNamedFixture "base"
    middleFixture <- makeNamedFixture "middle"
    transitiveFixture <- makeNamedFixture "transitive"
    leftFixture <- makeNamedFixture "left"
    rightFixture <- makeNamedFixture "right"
    diamondFixture <- makeNamedFixture "diamond"
    conflictLeftFixture <- makeNamedFixture "conflict-left"
    conflictRightFixture <- makeNamedFixture "conflict-right"
    conflictRootFixture <- makeNamedFixture "conflict-root"

    (base, baseFingerprint) <-
        sealFactFixture baseFixture [] "transitive-shared"
    middle <- snd <$> sealFixture middleFixture [base] (pure ())
    transitive <- sealUsingImportedFact
        transitiveFixture [middle] baseFingerprint
    assertLocalFactOrdinalZero "transitive importer" transitive

    left <- snd <$> sealFixture leftFixture [base] (pure ())
    right <- snd <$> sealFixture rightFixture [base] (pure ())
    diamond <- sealUsingImportedFact
        diamondFixture [left, right] baseFingerprint
    assertLocalFactOrdinalZero "diamond importer" diamond

    (conflictLeft, leftFingerprint) <-
        sealFactFixture conflictLeftFixture [] "diamond-conflict"
    (conflictRight, rightFingerprint) <-
        sealFactFixture conflictRightFixture [] "diamond-conflict"
    conflict <- runFixtureDriver
        conflictRootFixture
        [conflictLeft, conflictRight]
        (pure ())
    case conflict of
        Declaration.DriverFailed
                (Declaration.DriverDeclarationFailed
                    (Declaration.ImportedAliasCollision
                        alias
                        (Declaration.ImportedAliasOrigin
                            _leftSlot firstTarget)
                        (Declaration.ImportedAliasOrigin
                            _rightSlot secondTarget)))
                _prefix -> do
            assertEqual "conflicting alias"
                (Semantic.semanticName "diamond-conflict")
                alias
            assertEqual "first alias origin"
                leftFingerprint
                firstTarget
            assertEqual "second alias origin"
                rightFingerprint
                secondTarget
        _ ->
            assertFailure "conflicting diamond alias was not rejected"
  where
    sealUsingImportedFact fixture parents fingerprint = do
        (batch, _sealed) <- sealFixture fixture parents do
            (_value, committed) <- Declaration.commitProofDeclaration
                (Semantic.proofSyntaxId "use-transitive-import") do
                    candidate <- Declaration.reserveCandidate
                        (factSpec fixture "local-after-import")
                    Declaration.authorizeOmittedCandidate candidate do
                        void (Declaration.useAuthorizedFact fingerprint)
                        Declaration.recordOmittedUse
            pure committed
        pure batch

    assertLocalFactOrdinalZero label batch =
        case Semantic.declarationDeltaFacts
                (Declaration.committedBatchDelta batch) of
            [occurrence] ->
                assertEqual label
                    (localFactOrdinal 0)
                    (Semantic.factSlotOrdinal
                        (Semantic.semanticFactSlot occurrence))
            facts ->
                assertFailure
                    (label <> ": unexpected fact count "
                        <> show (length facts))

sealFactFixture
    :: Fixture
    -> [FixtureSealed]
    -> Text
    -> IO
        ( FixtureSealed
        , Semantic.SemanticFactOccurrenceFingerprint
        )
sealFactFixture fixture parents alias = do
    (batch, sealed) <- sealFixture fixture parents do
        (_value, committed) <- Declaration.commitProofDeclaration
            (Semantic.proofSyntaxId
                (TextEncoding.encodeUtf8 alias)) do
                candidate <- Declaration.reserveCandidate
                    (factSpec fixture alias)
                Declaration.authorizeSourceAxiomCandidate candidate
        pure committed
    case Semantic.declarationDeltaFacts
            (Declaration.committedBatchDelta batch) of
        [occurrence] ->
            pure
                ( sealed
                , Semantic.semanticFactFingerprint occurrence
                )
        facts ->
            assertFailure
                ("unexpected sealed fact count: " <> show (length facts))
                >> fail "unreachable"

sealFixture
    :: Fixture
    -> [FixtureSealed]
    -> Declaration.ModuleDriver Text value
    -> IO (value, FixtureSealed)
sealFixture fixture parents action = do
    outcome <- runFixtureDriver fixture parents action
    case outcome of
        Declaration.DriverSucceeded value interface prefix _closure ->
            pure
                ( value
                , FixtureSealed
                    interface
                    (Declaration.freshImportedModuleEvidence
                        [ evidence
                        | FixtureSealed _interface evidence <- parents
                        ]
                        interface
                        prefix)
                )
        Declaration.DriverFailed failure _prefix ->
            assertFailure ("fixture failed: " <> show failure)
                >> fail "unreachable"
        Declaration.DriverSealFailed failure _prefix ->
            assertFailure ("fixture did not seal: " <> show failure)
                >> fail "unreachable"

runFixtureDriver
    :: Fixture
    -> [FixtureSealed]
    -> Declaration.ModuleDriver Text value
    -> IO (Declaration.DriverResult Text value)
runFixtureDriver fixture parents action = do
    result <- Declaration.runModuleDriver
        (fixtureFoundation fixture)
        (fixtureOwner fixture)
        [ Semantic.semanticInterfaceAssertedId interface
        | FixtureSealed interface _evidence <- parents
        ]
        unavailableVampireResolver
        Declaration.FreshValidation
        do
            traverse_
                (\(FixtureSealed _interface evidence) ->
                    Declaration.importSealedModuleDriver evidence)
                parents
            action
    expectRight result

requireSingleOccurrence
    :: Declaration.CommittedDeclarationBatch
    -> Declaration.ModuleDriver
        Declaration.DeclarationError
        Semantic.SemanticFactOccurrence
requireSingleOccurrence batch =
    case Semantic.declarationDeltaFacts
            (Declaration.committedBatchDelta batch) of
        [occurrence] ->
            pure occurrence
        _ ->
            Declaration.failModuleDriver
                Declaration.ProofDeclarationMustProduceOneFact

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

withOpenedStore
    :: Fixture
    -> FilePath
    -> (Store.Store -> IO value)
    -> IO value
withOpenedStore fixture root action =
    bracket
        (expectRightIO
            (Store.openStore
                (root Posix.</> "store.sqlite")
                (Identity.theoryId (fixtureFoundation fixture))))
        (Store.closeStore . snd)
        (action . snd)

withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a
withTemporaryDirectory template =
    bracket create Directory.removePathForcibly
  where
    create = do
        root <- Directory.getTemporaryDirectory
        (path, handle) <- openTempFile root template
        hClose handle
        Directory.removeFile path
        Directory.createDirectory path
        pure path