Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 802 deletions

diff --git a/source/Test/Unit/Identity.hs b/source/Test/Unit/Identity.hs
deleted file mode 100644
index 0cb46a5..0000000
--- a/source/Test/Unit/Identity.hs
+++ /dev/null
@@ -1,802 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-module Test.Unit.Identity (unitTests) where
-
-import Base
-import Checking.Authority qualified as Authority
-import Checking.Core qualified as Core
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Felix.Cache.Codec
-import Felix.Math.Codec
-import Felix.Module
-import Felix.Source
-
-import Control.Exception (bracket)
-import Data.ByteString qualified as ByteString
-import Data.Either (isLeft)
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Numeric.Natural (Natural)
-import System.Directory qualified as Directory
-import System.FilePath.Posix qualified as Posix
-import Test.Tasty
-import Test.Tasty.HUnit
-
-
-unitTests :: TestTree
-unitTests =
-    testGroup "Content identities"
-        [ testCase "uses the frozen mathematical hash framing"
-            hashesCanonicalFields
-        , testCase "orders exhaustive foundation rows by stable tags"
-            ordersFoundationManifestTags
-        , testCase "uses the frozen source path codecs"
-            encodesSourcePaths
-        , testCase "separates durable namespaces from mount labels"
-            separatesModuleOwnership
-        , testCase "rejects duplicate canonical collection encodings"
-            rejectsDuplicateCanonicalCollections
-        , testCase "matches every frozen mathematical identity vector"
-            matchesMathematicalIdentityVectors
-        , testCase "validates recursive transparent object content"
-            validatesTransparentObjectClosure
-        , testCase "rejects cyclic and mismatched object content"
-            rejectsInvalidObjectContent
-        , testCase "validates proposition content and theorem closure"
-            validatesPropositionAndTheorem
-        , testCase "round-trips deterministic epoch cache values"
-            roundTripsEpochCacheValues
-        , testCase "validates compact fact authority"
-            validatesCompactFactAuthority
-        , testCase "propagates candidate safety through local claims"
-            propagatesCandidateSafety
-        ]
-
-ordersFoundationManifestTags :: Assertion
-ordersFoundationManifestTags = do
-    let (intrinsics, rules, axioms) =
-            Identity.foundationManifestTags
-    assertEqual
-        "intrinsic stable-tag order"
-        [ Core.Member
-        , Core.Empty
-        , Core.PairSet
-        , Core.FamilyUnion
-        , Core.PowerSet
-        , Core.Sep
-        , Core.Repl
-        , Core.SetChoose
-        , Core.UnivOf
-        , Core.ISetLfp
-        ]
-        intrinsics
-    assertEqual
-        "kernel-rule stable-tag order"
-        [ Foundation.SetLfpBound
-        , Foundation.SetLfpLeast
-        , Foundation.SetLfpFixed
-        , Foundation.SetLfpInduct
-        ]
-        rules
-    assertEqual
-        "foundation-axiom stable-tag order"
-        [ Foundation.EmptyCharacteristic
-        , Foundation.PairSetCharacteristic
-        , Foundation.FamilyUnionCharacteristic
-        , Foundation.PowerSetCharacteristic
-        , Foundation.SeparationCharacteristic
-        , Foundation.ReplacementCharacteristic
-        , Foundation.SetChooseWitness
-        , Foundation.SetExtensionality
-        , Foundation.SetInduction
-        , Foundation.PropositionalExtensionality
-        , Foundation.DoubleNegationElim
-        , Foundation.UnivOfContains
-        , Foundation.UnivOfTransitive
-        , Foundation.UnivOfFamilyUnionClosed
-        , Foundation.UnivOfPowerSetClosed
-        , Foundation.UnivOfReplacementClosed
-        , Foundation.UnivOfMinimal
-        ]
-        axioms
-
-hashesCanonicalFields :: Assertion
-hashesCanonicalFields = do
-    let vectors =
-            [ ( []
-              , "09ace37213e33d80b79e5f21fd60d03f25855e528cc2f25da4762be81d34a8c2"
-              )
-            , ( [ByteString.empty]
-              , "cd166f5b566ebd02f00f202792699803df09e9a020afbaaa987f5001cb1d095e"
-              )
-            , (["a", "bc"]
-              , "70c43385ae5b28bb862bc461a3c8d85ab94fd616528e7d94a9e7a52217b5c657"
-              )
-            , (["ab", "c"]
-              , "d3588d1b26aac958d9f393d8528ad68ed34354aee41d7e405a156b3ffff20c90"
-              )
-            ]
-    traverse_
-        (\(fields, expected) -> do
-            digest <- expectRight
-                (hashCanonicalFields "felix-test-v1" fields)
-            assertEqual
-                ("fields " <> show fields)
-                expected
-                (mathematicalDigestHex digest))
-        vectors
-
-encodesSourcePaths :: Assertion
-encodesSourcePaths = do
-    let absoluteVectors =
-            [ ([]
-              , "000000000000002266656c69782d6162736f6c7574652d736f757263652d726f6f742d706174682d763100000000"
-              )
-            , (["a"]
-              , "000000000000002266656c69782d6162736f6c7574652d736f757263652d726f6f742d706174682d763100000001000000000000000161"
-              )
-            , (["a", "b"]
-              , "000000000000002266656c69782d6162736f6c7574652d736f757263652d726f6f742d706174682d763100000002000000000000000161000000000000000162"
-              )
-            ]
-        relativeVectors =
-            [ (["a"]
-              , "000000000000001b66656c69782d736166652d72656c61746976652d706174682d763100000001000000000000000161"
-              )
-            , (["a", "b"]
-              , "000000000000001b66656c69782d736166652d72656c61746976652d706174682d763100000002000000000000000161000000000000000162"
-              )
-            ]
-    traverse_
-        (\(components, expected) -> do
-            encoded <- expectRight
-                (encodeCanonicalPathRecord
-                    "felix-absolute-source-root-path-v1"
-                    components)
-            assertEqual
-                (show components)
-                expected
-                (hex encoded))
-        absoluteVectors
-    traverse_
-        (\(components, expected) -> do
-            encoded <- expectRight
-                (encodeCanonicalPathRecord
-                    "felix-safe-relative-path-v1"
-                    components)
-            assertEqual
-                (show components)
-                expected
-                (hex encoded))
-        relativeVectors
-
-separatesModuleOwnership :: Assertion
-separatesModuleOwnership =
-    withTemporaryDirectory "felix-module-owner" \root -> do
-        writeFile (root Posix.</> "b.tex") ""
-        mounts <- expectRight
-            =<< prepareSourceMounts
-                [(sourceMountId "display-only", root)]
-        request <- expectRight (searchedRoot "b.tex")
-        source <- expectRight =<< resolveRoot mounts request
-        mount <- case sourceMountList mounts of
-            [only] ->
-                pure only
-            _ ->
-                assertFailure "expected one prepared mount"
-                    >> fail "unreachable"
-        relative <- expectRight (safeRelativePath "b.tex")
-        let owner =
-                moduleName (resolvedSourceAddress source)
-        assertEqual
-            "relative owner"
-            relative
-            (moduleNameRelativePath owner)
-        assertEqual
-            "namespace derives from the canonical root"
-            (sourceNamespaceId (sourceMountRoot mount))
-            (moduleNameNamespace owner)
-
-rejectsDuplicateCanonicalCollections :: Assertion
-rejectsDuplicateCanonicalCollections = do
-    assertEqual
-        "set duplicate"
-        (Left (DuplicateCanonicalSetElement "a"))
-        (encodeCanonicalSet ["b", "a", "a"])
-    assertEqual
-        "map duplicate"
-        (Left (DuplicateCanonicalMapKey "a"))
-        (encodeCanonicalMap [("a", "first"), ("a", "second")])
-
-matchesMathematicalIdentityVectors :: Assertion
-matchesMathematicalIdentityVectors = do
-    fixture <- makeIdentityFixture
-    let vectors =
-            [ ( "theory"
-              , Identity.theoryIdDigest
-                    (fixtureTheory fixture)
-              , "46665f15f80ad52d319188de307471f34905ec3849b84b9d6d0d5a584a90eb62"
-              )
-            , ( "intrinsic Empty"
-              , Identity.objectIdDigest
-                    (fixtureIntrinsic fixture)
-              , "a11f641738714ac806f3c3b902841b3178d32fff38fea353aac409e3cc1a8efc"
-              )
-            , ( "transparent Empty"
-              , Identity.objectIdDigest
-                    (fixtureTransparent fixture)
-              , "49dfb3c96f0db2cc81703bbed82c08e9d2eda7d4a2274f0529d22c592003d4d1"
-              )
-            , ( "opaque signature"
-              , Identity.objectIdDigest
-                    (fixtureOpaque fixture)
-              , "8723488e60ed09ffad378bc6d9916d07c348d12d01548a7b482726e6e18b2c8d"
-              )
-            , ( "proposition"
-              , Identity.propositionIdDigest
-                    (Identity.checkedPropositionId
-                        (fixtureProposition fixture))
-              , "c40b403f0422f4125065d83b5eba64e4b0c4b24fb1559967ef986f5265829b65"
-              )
-            , ( "theorem"
-              , Identity.theoremIdDigest
-                    (fixtureTheorem fixture)
-              , "6a328a4142fde3c9851186ea00f54d8978d2640dcbe51421536c9726f4f717d2"
-              )
-            ]
-    traverse_
-        (\(description, digest, expected) ->
-            assertEqual
-                description
-                expected
-                (mathematicalDigestHex digest))
-        vectors
-    assertEqual
-        "opaque declaration seed"
-        "27697d641220b8bb63b32631492646277b28e70c8b7149206580337254ecc123"
-        (mathematicalDigestHex
-            (Identity.opaqueDeclarationSeedDigest
-                (fixtureOpaqueSeed fixture)))
-    assertEqual
-        "family domains remain distinct"
-        (length vectors)
-        (Set.size
-            (Set.fromList
-                [ digest
-                | (_description, digest, _expected) <- vectors
-                ]))
-
-validatesTransparentObjectClosure :: Assertion
-validatesTransparentObjectClosure = do
-    fixture <- makeIdentityFixture
-    let theory = fixtureTheory fixture
-        child = fixtureTransparent fixture
-        parentBody = Core.CGlobal child
-        parent =
-            Identity.transparentObjectId
-                theory
-                Core.TySet
-                parentBody
-        assertions =
-            [ Identity.assertedObject
-                parent
-                (Identity.TransparentObjectContent
-                    theory
-                    Core.TySet
-                    parentBody)
-            , Identity.assertedObject
-                child
-                (Identity.TransparentObjectContent
-                    theory
-                    Core.TySet
-                    (Core.CIntrinsic Core.Empty))
-            , Identity.assertedObject
-                (fixtureIntrinsic fixture)
-                (Identity.IntrinsicObjectContent
-                    theory
-                    Core.Empty
-                    Core.TySet)
-            ]
-    closure <- expectRight
-        (Identity.validateObjectClosure theory assertions)
-    assertEqual
-        "all recursively checked objects"
-        (Set.fromList
-            [ fixtureIntrinsic fixture
-            , child
-            , parent
-            ])
-        (Identity.checkedObjectIds closure)
-    assertEqual
-        "parent type"
-        (Just Core.TySet)
-        (Identity.lookupCheckedObjectType parent closure)
-
-rejectsInvalidObjectContent :: Assertion
-rejectsInvalidObjectContent = do
-    fixture <- makeIdentityFixture
-    firstDigest <- expectRight
-        (hashCanonicalFields "felix-invalid-object-a" [])
-    secondDigest <- expectRight
-        (hashCanonicalFields "felix-invalid-object-b" [])
-    mismatchDigest <- expectRight
-        (hashCanonicalFields "felix-invalid-object-mismatch" [])
-    let theory = fixtureTheory fixture
-        first =
-            Identity.objectId
-                Identity.TransparentObject
-                firstDigest
-        second =
-            Identity.objectId
-                Identity.TransparentObject
-                secondDigest
-        cycleAssertions =
-            [ Identity.assertedObject
-                first
-                (Identity.TransparentObjectContent
-                    theory
-                    Core.TySet
-                    (Core.CGlobal second))
-            , Identity.assertedObject
-                second
-                (Identity.TransparentObjectContent
-                    theory
-                    Core.TySet
-                    (Core.CGlobal first))
-            ]
-    case Identity.validateObjectClosure theory cycleAssertions of
-        Left (Identity.TransparentObjectCycle path) -> do
-            assertEqual
-                "cycle closes"
-                (NonEmpty.head path)
-                (NonEmpty.last path)
-            assertEqual
-                "cycle members"
-                (Set.fromList [first, second])
-                (Set.fromList (NonEmpty.toList path))
-        Left other ->
-            assertFailure
-                ("expected a transparent cycle, got " <> show other)
-        Right _ ->
-            assertFailure "expected a transparent cycle, got Right"
-    let mismatched =
-            Identity.objectId
-                Identity.TransparentObject
-                mismatchDigest
-        content =
-            Identity.TransparentObjectContent
-                theory
-                Core.TySet
-                (Core.CIntrinsic Core.Empty)
-    case
-        Identity.validateObjectClosure
-            theory
-            [Identity.assertedObject mismatched content] of
-        Left
-            (Identity.ObjectIdPayloadMismatch
-                supplied
-                computed) -> do
-                    assertEqual "supplied ID" mismatched supplied
-                    assertEqual
-                        "computed ID"
-                        (fixtureTransparent fixture)
-                        computed
-        Left other ->
-            assertFailure
-                ("expected object ID disagreement, got " <> show other)
-        Right _ ->
-            assertFailure "expected object ID disagreement, got Right"
-
-validatesPropositionAndTheorem :: Assertion
-validatesPropositionAndTheorem = do
-    fixture <- makeIdentityFixture
-    let proposition =
-            fixtureProposition fixture
-        reference =
-            fixtureTheoremRef fixture
-    assertEqual
-        "theorem retains its theory"
-        (fixtureTheory fixture)
-        (Identity.theoremRefTheory reference)
-    assertEqual
-        "theorem retains its proposition"
-        (Identity.checkedPropositionId proposition)
-        (Identity.theoremRefProposition reference)
-    falsum <- expectRight
-        (Identity.validatePropositionContent
-            (fixtureClosure fixture)
-            Core.CFalsum)
-    case
-        Identity.validateAssertedPropositionContent
-            (fixtureClosure fixture)
-            (Identity.checkedPropositionId falsum)
-            (Core.frozenCoreTerm
-                (Identity.checkedPropositionTerm proposition)) of
-        Left
-            (Identity.PropositionIdPayloadMismatch
-                supplied
-                computed) -> do
-                    assertEqual
-                        "supplied proposition ID"
-                        (Identity.checkedPropositionId falsum)
-                        supplied
-                    assertEqual
-                        "computed proposition ID"
-                        (Identity.checkedPropositionId proposition)
-                        computed
-        Left other ->
-            assertFailure
-                ("expected proposition ID disagreement, got "
-                    <> show other)
-        Right _ ->
-            assertFailure
-                "expected proposition ID disagreement, got Right"
-
-roundTripsEpochCacheValues :: Assertion
-roundTripsEpochCacheValues = do
-    fixture <- makeIdentityFixture
-    let theory = fixtureTheory fixture
-        contents =
-            [ Identity.IntrinsicObjectContent
-                theory
-                Core.Empty
-                Core.TySet
-            , Identity.TransparentObjectContent
-                theory
-                Core.TySet
-                (Core.CIntrinsic Core.Empty)
-            , Identity.OpaqueObjectContent
-                theory
-                (fixtureOpaqueSeed fixture)
-                Core.TySet
-            ]
-    traverse_
-        (\content ->
-            assertEqual
-                "object-content cache round trip"
-                (Right content)
-                (decodeCache
-                    Identity.getObjectContentCache
-                    (encodeCache
-                        (Identity.putObjectContentCache
-                            content))))
-        contents
-    assertEqual
-        "constructive theorem reference cache round trip"
-        (Right (fixtureTheoremRef fixture))
-        (decodeCache
-            Identity.getTheoremRefCache
-            (encodeCache
-                (Identity.putTheoremRefCache
-                    (fixtureTheoremRef fixture))))
-    assertBool
-        "cache bytes are not mathematical theorem-reference bytes"
-        ( encodeCache
-            (Identity.putTheoremRefCache
-                (fixtureTheoremRef fixture))
-            /= Identity.encodeTheoremRef
-                (fixtureTheoremRef fixture)
-        )
-    let ascending =
-            Map.fromList [("a", 1 :: Natural), ("b", 2)]
-        putMap =
-            putCanonicalCacheMap
-                putCacheText
-                putCacheNatural
-    assertEqual
-        "canonical cache map round trip"
-        (Right ascending)
-        (decodeCache
-            (getCanonicalCacheMap
-                getCacheText
-                getCacheNatural)
-            (encodeCache (putMap ascending)))
-
-validatesCompactFactAuthority :: Assertion
-validatesCompactFactAuthority = do
-    fixture <- makeIdentityFixture
-    let reference = fixtureTheoremRef fixture
-        sourceKinds =
-            Authority.singletonEscapeKind Authority.SourceAxiom
-        bothKinds =
-            Authority.escapeKinds
-                [Authority.Omitted, Authority.SourceAxiom]
-        sourceTarget =
-            Authority.factAuthority
-                reference
-                (Authority.authoritySafety sourceKinds)
-        bothTarget =
-            Authority.factAuthority
-                reference
-                (Authority.authoritySafety bothKinds)
-        requests =
-            [ Authority.preparedRequestId
-                Authority.PreparedRequestFof
-                Authority.PreparedRequestDirect
-                "first"
-            , Authority.preparedRequestId
-                Authority.PreparedRequestFof
-                Authority.PreparedRequestDirect
-                "first"
-            , Authority.preparedRequestId
-                Authority.PreparedRequestFof
-                Authority.PreparedRequestDirect
-                "second"
-            ]
-        directRequest =
-            Authority.preparedRequestId
-                Authority.PreparedRequestFof
-                Authority.PreparedRequestDirect
-                "same bytes"
-        indirectRequest =
-            Authority.preparedRequestId
-                Authority.PreparedRequestFof
-                Authority.PreparedRequestIndirect
-                "same bytes"
-        directAuthorizations =
-            [ Authority.CheckedKernelConstruction
-                (Authority.FoundationLeaf
-                    Foundation.EmptyCharacteristic)
-            , Authority.CheckedKernelConstruction
-                (Authority.GuardedFoundationRules
-                    (Authority.guardedRuleSet
-                        (Foundation.SetLfpBound :| [])))
-            , Authority.CheckedKernelConstruction
-                (Authority.CheckedDefinitionEquation
-                    (fixtureIntrinsic fixture))
-            , Authority.CheckedKernelConstruction
-                (Authority.CheckedSetConstructionExtensionality
-                    (fixtureIntrinsic fixture)
-                    (hashCacheFields
-                        "test-named-construction" ["checked"]))
-            , Authority.CheckedSourceProof requests
-            , Authority.TrustedCompilation
-                (Authority.DatatypeCompilation
-                    (Authority.datatypeCompilationDescriptor
-                        (fixtureIntrinsic fixture)
-                        (NonEmpty.singleton
-                            (fixtureIntrinsic fixture))
-                        [reference]))
-            , Authority.SourceAxiomAuthorization
-            , Authority.OmittedAuthorization
-            ]
-    sourceCertificate <- expectRight
-        (Authority.validationCertificate
-            sourceTarget
-            Authority.SourceAxiomAuthorization)
-    proofCertificate <- expectRight
-        (Authority.validationCertificate
-            bothTarget
-            (Authority.CheckedSourceProof requests))
-    assertEqual
-        "escape bits have canonical order"
-        [Authority.SourceAxiom, Authority.Omitted]
-        (Authority.escapeKindsToList bothKinds)
-    traverse_
-        (\direct ->
-            assertEqual
-                ("direct authorization round trip: " <> show direct)
-                (Right direct)
-                (decodeCache
-                    Authority.getDirectAuthorizationCache
-                    (encodeCache
-                        (Authority.putDirectAuthorizationCache
-                            direct))))
-        directAuthorizations
-    assertEqual
-        "certificate cache retains repeated ordered requests"
-        (Right proofCertificate)
-        (decodeCache
-            Authority.getValidationCertificateCache
-            (encodeCache
-                (Authority.putValidationCertificateCache
-                    proofCertificate)))
-    assertBool
-        "request mode participates in exact request identity"
-        (directRequest /= indirectRequest)
-    assertEqual
-        "prepared-request cache identity vector"
-        "1d72b851cb8b1704617becbf9f2cf492aed1c674d9e6ca759e244f169b15f278"
-        (hex
-            (encodeCache
-                (Authority.putPreparedRequestIdCache
-                    directRequest)))
-    assertEqual
-        "source certificate round trip"
-        (Right sourceCertificate)
-        (decodeCache
-            Authority.getValidationCertificateCache
-            (encodeCache
-                (Authority.putValidationCertificateCache
-                    sourceCertificate)))
-    assertBool
-        "source axiom requires its exact singleton safety"
-        (isLeft
-            (Authority.validationCertificate
-                bothTarget
-                Authority.SourceAxiomAuthorization))
-    assertBool
-        "omitted authorization requires its distinct bit"
-        (isLeft
-            (Authority.validationCertificate
-                sourceTarget
-                Authority.OmittedAuthorization))
-    assertBool
-        "cache rejects an empty escape-backed value"
-        (isLeft
-            (decodeCache
-                Authority.getAuthoritySafetyCache
-                (encodeCache do
-                    putCacheTag 0x01
-                    putCacheTag 0x00)))
-    let taintedCandidate =
-            Authority.addCandidateEscape
-                Authority.SourceAxiom
-                Authority.initialCandidateSafety
-    assertEqual
-        "candidate completion freezes accumulated safety"
-        sourceTarget
-        (Authority.candidateFactAuthority
-            reference
-            taintedCandidate)
-
-propagatesCandidateSafety :: Assertion
-propagatesCandidateSafety = do
-    fixture <- makeIdentityFixture
-    let reference = fixtureTheoremRef fixture
-        imported =
-            Authority.factAuthority
-                reference
-                (Authority.authoritySafety
-                    (Authority.singletonEscapeKind
-                        Authority.SourceAxiom))
-    afterImported <- expectRight
-        (Authority.accumulateFactSafety
-            reference
-            imported
-            Authority.initialCandidateSafety)
-    -- A local claim shares the enclosing candidate value; citing that claim
-    -- does not create a second support representation.
-    afterLocalClaim <- expectRight
-        (Authority.accumulateFactSafety
-            reference
-            (Authority.factAuthority
-                reference
-                Authority.cleanAuthoritySafety)
-            afterImported)
-    let finalSafety =
-            Authority.addCandidateEscape
-                Authority.Omitted
-                afterLocalClaim
-    assertEqual
-        "local claim retains prior safety and direct omission"
-        [Authority.SourceAxiom, Authority.Omitted]
-        (Authority.escapeKindsToList
-            (Authority.authoritySafetyEscapeKinds
-                (Authority.candidateSafetyAuthority finalSafety)))
-
-data IdentityFixture = IdentityFixture
-    { fixtureTheory :: !Identity.TheoryId
-    , fixtureIntrinsic :: !Identity.ObjectId
-    , fixtureTransparent :: !Identity.ObjectId
-    , fixtureOpaqueSeed :: !Identity.OpaqueDeclarationSeed
-    , fixtureOpaque :: !Identity.ObjectId
-    , fixtureClosure :: !Identity.CheckedObjectClosure
-    , fixtureProposition :: !Identity.CheckedPropositionContent
-    , fixtureTheoremRef :: !Identity.TheoremRef
-    , fixtureTheorem :: !Identity.TheoremId
-    }
-
-makeIdentityFixture :: IO IdentityFixture
-makeIdentityFixture = do
-    foundation <- expectRight Foundation.checkedFoundation
-    pathRecord <- expectRight
-        (encodeCanonicalPathRecord
-            "felix-absolute-source-root-path-v1"
-            ["a"])
-    namespaceDigest <- expectRight
-        (hashCanonicalFields
-            "felix-source-namespace-v1"
-            [pathRecord])
-    relative <- expectRight (safeRelativePath "b.tex")
-    let theory =
-            Identity.theoryId foundation
-        intrinsic =
-            Identity.intrinsicObjectId
-                theory
-                Core.Empty
-                Core.TySet
-        transparent =
-            Identity.transparentObjectId
-                theory
-                Core.TySet
-                (Core.CIntrinsic Core.Empty)
-        owner =
-            moduleNameFromParts
-                (sourceNamespaceIdFromDigest
-                    namespaceDigest)
-                relative
-        seed =
-            Identity.opaqueDeclarationSeed
-                owner
-                (localDeclarationOrdinal 2)
-                SignatureDeclaration
-                (generatedObjectSlot 0)
-        opaque =
-            Identity.opaqueObjectId
-                theory
-                seed
-                Core.TySet
-    closure <- expectRight
-        (Identity.validateObjectClosure
-            theory
-            [ Identity.assertedObject
-                intrinsic
-                (Identity.IntrinsicObjectContent
-                    theory
-                    Core.Empty
-                    Core.TySet)
-            ])
-    proposition <- expectRight
-        (Identity.validatePropositionContent
-            closure
-            (Core.CEq
-                Core.TySet
-                (Core.CGlobal intrinsic)
-                (Core.CGlobal intrinsic)))
-    let reference =
-            Identity.theoremRef
-                theory
-                (Identity.checkedPropositionId proposition)
-    pure
-        IdentityFixture
-            { fixtureTheory = theory
-            , fixtureIntrinsic = intrinsic
-            , fixtureTransparent = transparent
-            , fixtureOpaqueSeed = seed
-            , fixtureOpaque = opaque
-            , fixtureClosure = closure
-            , fixtureProposition = proposition
-            , fixtureTheoremRef = reference
-            , fixtureTheorem =
-                Identity.theoremId reference
-            }
-
-hex :: ByteString.ByteString -> Text
-hex =
-    Text.pack
-        . concatMap byteHex
-        . ByteString.unpack
-  where
-    byteHex byte =
-        let digits = "0123456789abcdef"
-            high = fromIntegral (byte `div` 16)
-            low = fromIntegral (byte `mod` 16)
-        in [digits `at` high, digits `at` low]
-
-    at characters index =
-        fromMaybe
-            (impossible "hex digit index")
-            (nth index characters)
-
-expectRight :: Show error => Either error value -> IO value
-expectRight = \case
-    Left err ->
-        assertFailure (show err) >> fail "unreachable"
-    Right value ->
-        pure value
-
-withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a
-withTemporaryDirectory template =
-    bracket create Directory.removePathForcibly
-  where
-    create = do
-        systemTemp <- Directory.getTemporaryDirectory
-        (path, handle) <- openTempFile systemTemp template
-        hClose handle
-        Directory.removeFile path
-        Directory.createDirectory path
-        pure path