Migrate to `Felix` namespaceHEADhotg

1 files changed, 802 insertions, 0 deletions

diff --git a/source/Felix/Test/Unit/Identity.hs b/source/Felix/Test/Unit/Identity.hs
new file mode 100644
index 0000000..7e1e73f
--- /dev/null
+++ b/source/Felix/Test/Unit/Identity.hs
@@ -0,0 +1,802 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Felix.Test.Unit.Identity (unitTests) where
+
+import Base
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.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