{-# 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