summaryrefslogtreecommitdiff
path: root/source/Felix/Test/Unit/Identity.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Felix/Test/Unit/Identity.hs')
-rw-r--r--source/Felix/Test/Unit/Identity.hs802
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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:58:54 +0000