diff options
Diffstat (limited to 'source/Test/Unit/Identity.hs')
| -rw-r--r-- | source/Test/Unit/Identity.hs | 797 |
1 files changed, 0 insertions, 797 deletions
diff --git a/source/Test/Unit/Identity.hs b/source/Test/Unit/Identity.hs deleted file mode 100644 index b91d2b3..0000000 --- a/source/Test/Unit/Identity.hs +++ /dev/null @@ -1,797 +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.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 |