{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -- | Content-addressed identities for checked mathematical content. module Felix.Checking.Identity ( TheoryId , theoryId , theoryIdDigest , encodeFoundationManifest , foundationManifestTags , encodeKernelRuleTag , ObjectFamily(..) , ObjectId , objectId , objectIdFamily , objectIdDigest , encodeObjectId , OpaqueDeclarationSeed , opaqueDeclarationSeed , opaqueDeclarationSeedDigest , ObjectContent(..) , objectContentTheory , objectContentType , intrinsicObjectId , transparentObjectId , opaqueObjectId , AssertedObject , assertedObject , assertedObjectId , assertedObjectContent , CheckedObjectClosure , checkedObjectClosureTheory , checkedObjectIds , lookupCheckedObjectType , lookupCheckedObjectContent , validateObjectClosure , extendObjectClosure , ObjectValidationError(..) , PropositionId , propositionIdDigest , CheckedPropositionContent , checkedPropositionId , checkedPropositionTerm , validatePropositionContent , validateAssertedPropositionContent , propositionIdOf , PropositionValidationError(..) , TheoremRef , theoremRef , theoremRefTheory , theoremRefProposition , encodeTheoremRef , TheoremId , theoremId , theoremIdDigest , putTheoryIdCache , getTheoryIdCache , putObjectIdCache , getObjectIdCache , putObjectContentCache , getObjectContentCache , putPropositionIdCache , getPropositionIdCache , putTheoremRefCache , getTheoremRefCache ) where import Base import Felix.Checking.Core import Felix.Checking.Foundation import Felix.Cache.Codec import Felix.Math.Codec import Felix.Module import Control.DeepSeq (NFData) import Control.Monad.State.Strict import Data.Bifunctor (first) import Data.ByteString (ByteString) import Data.ByteString qualified as ByteString import Data.List qualified as List import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Word (Word8) newtype TheoryId = TheoryId MathematicalDigest deriving stock (Show, Eq, Ord, Generic) deriving newtype (Hashable, NFData) theoryId :: CheckedFoundation -> TheoryId theoryId foundation = TheoryId (codecInvariant (hashCanonicalFields "felix-theory" [encodeFoundationManifest foundation])) theoryIdDigest :: TheoryId -> MathematicalDigest theoryIdDigest (TheoryId digest) = digest -- | Canonical ordered intrinsic/rule/axiom manifest. Backend classification is -- intentionally absent. encodeFoundationManifest :: CheckedFoundation -> ByteString encodeFoundationManifest foundation = codecInvariant (encodeSequence [ codecInvariant (encodeSequence intrinsicRows) , codecInvariant (encodeSequence ruleRows) , codecInvariant (encodeSequence axiomRows) ]) where (intrinsicTags, ruleTags, axiomTags) = foundationManifestTags intrinsicRows = [ encodeCoreIntrinsicTag tag <> encodeFrame (encodeCoreType (coreIntrinsicType tag)) | tag <- intrinsicTags ] ruleRows = [ encodeKernelRuleTag tag <> encodeFrame (codecInvariant (encodeSequence (encodeCoreType <$> inputTypes))) <> encodeFrame (encodeNatural binderCount) | tag <- ruleTags , let KernelRuleSignature inputTypes binderCount = foundationRuleSignature foundation tag ] axiomRows = [ encodeFoundationAxiomTag tag <> encodeFrame (encodeCanonicalTerm absurd (frozenCoreTerm (foundationAxiomFrozen foundation tag))) | tag <- axiomTags ] -- | Exhaustive foundation inventories in their stable encoded-tag order. foundationManifestTags :: ( [CoreIntrinsicTag] , [KernelRuleTag] , [FoundationAxiomTag] ) foundationManifestTags = ( stableTagOrder "core intrinsic" encodeCoreIntrinsicTag allCoreIntrinsicTags , stableTagOrder "kernel rule" encodeKernelRuleTag allKernelRuleTags , stableTagOrder "foundation axiom" encodeFoundationAxiomTag allFoundationAxiomTags ) data ObjectFamily = IntrinsicObject | TransparentObject | OpaqueObject deriving stock (Show, Eq, Ord, Enum, Bounded, Generic) deriving anyclass (NFData) data ObjectId = ObjectId !ObjectFamily !MathematicalDigest deriving stock (Show, Eq, Ord, Generic) deriving anyclass (NFData) objectId :: ObjectFamily -> MathematicalDigest -> ObjectId objectId = ObjectId objectIdFamily :: ObjectId -> ObjectFamily objectIdFamily (ObjectId family _digest) = family objectIdDigest :: ObjectId -> MathematicalDigest objectIdDigest (ObjectId _family digest) = digest encodeObjectId :: ObjectId -> ByteString encodeObjectId (ObjectId family digest) = ByteString.singleton (objectFamilyTag family) <> mathematicalDigestBytes digest newtype OpaqueDeclarationSeed = OpaqueDeclarationSeed MathematicalDigest deriving stock (Show, Eq, Ord, Generic) deriving newtype (Hashable, NFData) opaqueDeclarationSeed :: ModuleName -> LocalDeclarationOrdinal -> DeclarationFamilyTag -> GeneratedObjectSlot -> OpaqueDeclarationSeed opaqueDeclarationSeed owner declarationOrdinal family generatedSlot = OpaqueDeclarationSeed (codecInvariant (hashCanonicalFields "felix-opaque-declaration-v1" [ encodeModuleName owner , encodeNatural (localDeclarationOrdinalValue declarationOrdinal) , encodeDeclarationFamilyTag family , encodeNatural (generatedObjectSlotValue generatedSlot) ])) opaqueDeclarationSeedDigest :: OpaqueDeclarationSeed -> MathematicalDigest opaqueDeclarationSeedDigest (OpaqueDeclarationSeed digest) = digest data ObjectContent = IntrinsicObjectContent !TheoryId !CoreIntrinsicTag !CoreType | TransparentObjectContent !TheoryId !CoreType !(CanonicalTerm ObjectId) | OpaqueObjectContent !TheoryId !OpaqueDeclarationSeed !CoreType deriving stock (Show, Eq, Ord, Generic) deriving anyclass (NFData) objectContentTheory :: ObjectContent -> TheoryId objectContentTheory = \case IntrinsicObjectContent identity _tag _coreType -> identity TransparentObjectContent identity _coreType _body -> identity OpaqueObjectContent identity _seed _coreType -> identity objectContentType :: ObjectContent -> CoreType objectContentType = \case IntrinsicObjectContent _identity _tag coreType -> coreType TransparentObjectContent _identity coreType _body -> coreType OpaqueObjectContent _identity _seed coreType -> coreType intrinsicObjectId :: TheoryId -> CoreIntrinsicTag -> CoreType -> ObjectId intrinsicObjectId identity tag coreType = ObjectId IntrinsicObject (codecInvariant (hashCanonicalFields "felix-intrinsic-object-v1" [ mathematicalDigestBytes (theoryIdDigest identity) , encodeCoreIntrinsicTag tag , encodeCoreType coreType ])) transparentObjectId :: TheoryId -> CoreType -> CanonicalTerm ObjectId -> ObjectId transparentObjectId identity coreType body = ObjectId TransparentObject (codecInvariant (hashCanonicalFields "felix-transparent-object-v1" [ mathematicalDigestBytes (theoryIdDigest identity) , encodeCoreType coreType , encodeCanonicalTerm encodeObjectId body ])) opaqueObjectId :: TheoryId -> OpaqueDeclarationSeed -> CoreType -> ObjectId opaqueObjectId identity seed coreType = ObjectId OpaqueObject (codecInvariant (hashCanonicalFields "felix-opaque-object-v1" [ mathematicalDigestBytes (theoryIdDigest identity) , mathematicalDigestBytes (opaqueDeclarationSeedDigest seed) , encodeCoreType coreType ])) data AssertedObject = AssertedObject !ObjectId !ObjectContent deriving stock (Show, Eq, Ord, Generic) deriving anyclass (NFData) assertedObject :: ObjectId -> ObjectContent -> AssertedObject assertedObject = AssertedObject assertedObjectId :: AssertedObject -> ObjectId assertedObjectId (AssertedObject identity _content) = identity assertedObjectContent :: AssertedObject -> ObjectContent assertedObjectContent (AssertedObject _identity content) = content data CheckedObject = CheckedObject !ObjectContent !CoreType data CheckedObjectClosure = CheckedObjectClosure !TheoryId !(Map ObjectId CheckedObject) checkedObjectClosureTheory :: CheckedObjectClosure -> TheoryId checkedObjectClosureTheory (CheckedObjectClosure identity _objects) = identity checkedObjectIds :: CheckedObjectClosure -> Set ObjectId checkedObjectIds (CheckedObjectClosure _identity objects) = Map.keysSet objects lookupCheckedObjectType :: ObjectId -> CheckedObjectClosure -> Maybe CoreType lookupCheckedObjectType identity (CheckedObjectClosure _theory objects) = checkedObjectType <$> Map.lookup identity objects lookupCheckedObjectContent :: ObjectId -> CheckedObjectClosure -> Maybe ObjectContent lookupCheckedObjectContent identity (CheckedObjectClosure _theory objects) = checkedObjectContent <$> Map.lookup identity objects checkedObjectType :: CheckedObject -> CoreType checkedObjectType (CheckedObject _content coreType) = coreType checkedObjectContent :: CheckedObject -> ObjectContent checkedObjectContent (CheckedObject content _coreType) = content data ObjectValidationError = DuplicateAssertedObjectId !ObjectId | ObjectContentTheoryMismatch !ObjectId !TheoryId !TheoryId | ObjectContentFamilyMismatch !ObjectId !ObjectFamily !ObjectFamily | IntrinsicObjectTypeMismatch !ObjectId !CoreIntrinsicTag !CoreType !CoreType | TransparentObjectReferenceMissing !ObjectId !ObjectId | TransparentObjectCycle !(NonEmpty ObjectId) | TransparentObjectCoreCheckError !ObjectId !CoreCheckError | TransparentObjectTypeMismatch !ObjectId !CoreType !CoreType | ObjectIdPayloadMismatch !ObjectId !ObjectId deriving stock (Show, Eq) data ObjectValidationState = ObjectValidationState { validationStack :: ![ObjectId] , validatedObjects :: !(Map ObjectId CheckedObject) } validateObjectClosure :: TheoryId -> [AssertedObject] -> Either ObjectValidationError CheckedObjectClosure validateObjectClosure expectedTheory asserted = do inventory <- buildObjectInventory asserted finalState <- execStateT (traverse_ (validateOneObject expectedTheory inventory) (Map.keys inventory)) (ObjectValidationState [] Map.empty) pure (CheckedObjectClosure expectedTheory (validatedObjects finalState)) -- | Validate one declaration's new objects against an already checked -- closure. The existing closure is returned unchanged for an empty batch. extendObjectClosure :: CheckedObjectClosure -> [AssertedObject] -> Either ObjectValidationError CheckedObjectClosure extendObjectClosure closure [] = Right closure extendObjectClosure (CheckedObjectClosure expectedTheory existing) asserted = do additions <- buildObjectInventory asserted traverse_ (\identity -> when (Map.member identity existing) (Left (DuplicateAssertedObjectId identity))) (Map.keys additions) let existingInventory = checkedObjectContent <$> existing inventory = Map.union additions existingInventory finalState <- execStateT (traverse_ (validateOneObject expectedTheory inventory) (Map.keys additions)) (ObjectValidationState [] existing) pure (CheckedObjectClosure expectedTheory (validatedObjects finalState)) buildObjectInventory :: [AssertedObject] -> Either ObjectValidationError (Map ObjectId ObjectContent) buildObjectInventory = foldM insertOne Map.empty where insertOne inventory (AssertedObject identity content) | Map.member identity inventory = Left (DuplicateAssertedObjectId identity) | otherwise = Right (Map.insert identity content inventory) validateOneObject :: TheoryId -> Map ObjectId ObjectContent -> ObjectId -> StateT ObjectValidationState (Either ObjectValidationError) () validateOneObject expectedTheory inventory identity = do alreadyValidated <- gets (Map.member identity . validatedObjects) unless alreadyValidated do stack <- gets validationStack when (identity `elem` stack) do lift (Left (TransparentObjectCycle (cyclePath identity stack))) content <- case Map.lookup identity inventory of Nothing -> impossible "object validation root is absent from its inventory" Just found -> pure found unless (objectContentTheory content == expectedTheory) (lift (Left (ObjectContentTheoryMismatch identity expectedTheory (objectContentTheory content)))) let expectedFamily = objectContentFamily content suppliedFamily = objectIdFamily identity unless (suppliedFamily == expectedFamily) (lift (Left (ObjectContentFamilyMismatch identity expectedFamily suppliedFamily))) modify' (\validationState -> validationState { validationStack = identity : validationStack validationState }) checked <- case content of IntrinsicObjectContent theory tag suppliedType -> do let expectedType = coreIntrinsicType tag unless (suppliedType == expectedType) (lift (Left (IntrinsicObjectTypeMismatch identity tag expectedType suppliedType))) verifyObjectId identity (intrinsicObjectId theory tag suppliedType) pure (CheckedObject content suppliedType) TransparentObjectContent theory suppliedType body -> do traverse_ (validateDependency expectedTheory inventory identity) (Set.toAscList (canonicalTermGlobals body)) resolvedObjects <- gets validatedObjects checkedBody <- lift (first (TransparentObjectCoreCheckError identity) (checkCanonicalCore (\reference -> checkedObjectType <$> Map.lookup reference resolvedObjects) body)) let inferredType = frozenCoreType checkedBody unless (inferredType == suppliedType) (lift (Left (TransparentObjectTypeMismatch identity suppliedType inferredType))) verifyObjectId identity (transparentObjectId theory suppliedType body) pure (CheckedObject content suppliedType) OpaqueObjectContent theory seed suppliedType -> do verifyObjectId identity (opaqueObjectId theory seed suppliedType) pure (CheckedObject content suppliedType) modify' (\validationState -> validationState { validationStack = dropCurrent identity (validationStack validationState) , validatedObjects = Map.insert identity checked (validatedObjects validationState) }) where verifyObjectId supplied computed = unless (supplied == computed) (lift (Left (ObjectIdPayloadMismatch supplied computed))) validateDependency :: TheoryId -> Map ObjectId ObjectContent -> ObjectId -> ObjectId -> StateT ObjectValidationState (Either ObjectValidationError) () validateDependency expectedTheory inventory parent dependency = case Map.lookup dependency inventory of Nothing -> lift (Left (TransparentObjectReferenceMissing parent dependency)) Just _ -> validateOneObject expectedTheory inventory dependency cyclePath :: ObjectId -> [ObjectId] -> NonEmpty ObjectId cyclePath repeated stack = case break (== repeated) stack of (between, _repeated : _outer) -> repeated :| (reverse between <> [repeated]) _ -> impossible "repeated object is absent from validation stack" dropCurrent :: ObjectId -> [ObjectId] -> [ObjectId] dropCurrent expected = \case current : rest | current == expected -> rest _ -> impossible "object validation stack is inconsistent" objectContentFamily :: ObjectContent -> ObjectFamily objectContentFamily = \case IntrinsicObjectContent{} -> IntrinsicObject TransparentObjectContent{} -> TransparentObject OpaqueObjectContent{} -> OpaqueObject newtype PropositionId = PropositionId MathematicalDigest deriving stock (Show, Eq, Ord, Generic) deriving newtype (Hashable, NFData) propositionIdDigest :: PropositionId -> MathematicalDigest propositionIdDigest (PropositionId digest) = digest data CheckedPropositionContent = CheckedPropositionContent !PropositionId !(FrozenCheckedCore ObjectId) deriving stock (Generic) deriving anyclass (NFData) checkedPropositionId :: CheckedPropositionContent -> PropositionId checkedPropositionId (CheckedPropositionContent identity _term) = identity checkedPropositionTerm :: CheckedPropositionContent -> FrozenCheckedCore ObjectId checkedPropositionTerm (CheckedPropositionContent _identity term) = term data PropositionValidationError = PropositionObjectMissing !ObjectId | PropositionCoreCheckError !CoreCheckError | PropositionIsNotProp !CoreType | PropositionIdPayloadMismatch !PropositionId !PropositionId deriving stock (Show, Eq) validatePropositionContent :: CheckedObjectClosure -> CanonicalTerm ObjectId -> Either PropositionValidationError CheckedPropositionContent validatePropositionContent closure term = do traverse_ (\identity -> unless (isJust (lookupCheckedObjectType identity closure)) (Left (PropositionObjectMissing identity))) (Set.toAscList (canonicalTermGlobals term)) checked <- first PropositionCoreCheckError (checkCanonicalCore (\identity -> lookupCheckedObjectType identity closure) term) unless (frozenCoreType checked == TyProp) (Left (PropositionIsNotProp (frozenCoreType checked))) let identity = propositionIdOf term pure (CheckedPropositionContent identity checked) validateAssertedPropositionContent :: CheckedObjectClosure -> PropositionId -> CanonicalTerm ObjectId -> Either PropositionValidationError CheckedPropositionContent validateAssertedPropositionContent closure supplied term = do checked <- validatePropositionContent closure term let computed = checkedPropositionId checked unless (supplied == computed) (Left (PropositionIdPayloadMismatch supplied computed)) pure checked propositionIdOf :: CanonicalTerm ObjectId -> PropositionId propositionIdOf term = PropositionId (codecInvariant (hashCanonicalFields "felix-proposition-v1" [encodeCanonicalTerm encodeObjectId term])) data TheoremRef = TheoremRef !TheoryId !PropositionId deriving stock (Show, Eq, Ord, Generic) deriving anyclass (NFData) theoremRef :: TheoryId -> PropositionId -> TheoremRef theoremRef = TheoremRef theoremRefTheory :: TheoremRef -> TheoryId theoremRefTheory (TheoremRef identity _proposition) = identity theoremRefProposition :: TheoremRef -> PropositionId theoremRefProposition (TheoremRef _identity proposition) = proposition encodeTheoremRef :: TheoremRef -> ByteString encodeTheoremRef (TheoremRef identity proposition) = encodeFrame (mathematicalDigestBytes (theoryIdDigest identity)) <> encodeFrame (mathematicalDigestBytes (propositionIdDigest proposition)) newtype TheoremId = TheoremId MathematicalDigest deriving stock (Show, Eq, Ord, Generic) deriving newtype (Hashable, NFData) theoremId :: TheoremRef -> TheoremId theoremId reference = TheoremId (codecInvariant (hashCanonicalFields "felix-theorem" [encodeTheoremRef reference])) theoremIdDigest :: TheoremId -> MathematicalDigest theoremIdDigest (TheoremId digest) = digest putTheoryIdCache :: TheoryId -> CachePut putTheoryIdCache = putMathematicalDigestCache . theoryIdDigest getTheoryIdCache :: CacheGet TheoryId getTheoryIdCache = TheoryId <$> getMathematicalDigestCache putObjectIdCache :: ObjectId -> CachePut putObjectIdCache (ObjectId family digest) = do putCacheTag (objectFamilyTag family) putMathematicalDigestCache digest getObjectIdCache :: CacheGet ObjectId getObjectIdCache = do family <- getCacheTag >>= \case 0x00 -> pure IntrinsicObject 0x01 -> pure TransparentObject 0x02 -> pure OpaqueObject tag -> fail ("unknown cache object-family tag " <> show tag) ObjectId family <$> getMathematicalDigestCache putOpaqueDeclarationSeedCache :: OpaqueDeclarationSeed -> CachePut putOpaqueDeclarationSeedCache = putMathematicalDigestCache . opaqueDeclarationSeedDigest getOpaqueDeclarationSeedCache :: CacheGet OpaqueDeclarationSeed getOpaqueDeclarationSeedCache = OpaqueDeclarationSeed <$> getMathematicalDigestCache putObjectContentCache :: ObjectContent -> CachePut putObjectContentCache = \case IntrinsicObjectContent identity tag coreType -> do putCacheTag 0x00 putTheoryIdCache identity putCoreIntrinsicTagCache tag putCoreTypeCache coreType TransparentObjectContent identity coreType body -> do putCacheTag 0x01 putTheoryIdCache identity putCoreTypeCache coreType putCanonicalTermCache putObjectIdCache body OpaqueObjectContent identity seed coreType -> do putCacheTag 0x02 putTheoryIdCache identity putOpaqueDeclarationSeedCache seed putCoreTypeCache coreType getObjectContentCache :: CacheGet ObjectContent getObjectContentCache = getCacheTag >>= \case 0x00 -> IntrinsicObjectContent <$> getTheoryIdCache <*> getCoreIntrinsicTagCache <*> getCoreTypeCache 0x01 -> TransparentObjectContent <$> getTheoryIdCache <*> getCoreTypeCache <*> getCanonicalTermCache getObjectIdCache 0x02 -> OpaqueObjectContent <$> getTheoryIdCache <*> getOpaqueDeclarationSeedCache <*> getCoreTypeCache tag -> fail ("unknown cache object-content tag " <> show tag) putPropositionIdCache :: PropositionId -> CachePut putPropositionIdCache = putMathematicalDigestCache . propositionIdDigest getPropositionIdCache :: CacheGet PropositionId getPropositionIdCache = PropositionId <$> getMathematicalDigestCache putTheoremRefCache :: TheoremRef -> CachePut putTheoremRefCache (TheoremRef identity proposition) = do putTheoryIdCache identity putPropositionIdCache proposition getTheoremRefCache :: CacheGet TheoremRef getTheoremRefCache = TheoremRef <$> getTheoryIdCache <*> getPropositionIdCache objectFamilyTag :: ObjectFamily -> Word8 objectFamilyTag = \case IntrinsicObject -> 0x00 TransparentObject -> 0x01 OpaqueObject -> 0x02 encodeKernelRuleTag :: KernelRuleTag -> ByteString encodeKernelRuleTag = ByteString.singleton . \case SetLfpBound -> 0x00 SetLfpLeast -> 0x01 SetLfpFixed -> 0x02 SetLfpInduct -> 0x03 encodeFoundationAxiomTag :: FoundationAxiomTag -> ByteString encodeFoundationAxiomTag = ByteString.singleton . \case EmptyCharacteristic -> 0x00 PairSetCharacteristic -> 0x01 FamilyUnionCharacteristic -> 0x02 PowerSetCharacteristic -> 0x03 SeparationCharacteristic -> 0x04 ReplacementCharacteristic -> 0x05 SetChooseWitness -> 0x06 SetExtensionality -> 0x07 SetInduction -> 0x08 PropositionalExtensionality -> 0x09 DoubleNegationElim -> 0x0a UnivOfContains -> 0x0b UnivOfTransitive -> 0x0c UnivOfFamilyUnionClosed -> 0x0d UnivOfPowerSetClosed -> 0x0e UnivOfReplacementClosed -> 0x0f UnivOfMinimal -> 0x10 allCoreIntrinsicTags :: [CoreIntrinsicTag] allCoreIntrinsicTags = [minBound .. maxBound] allKernelRuleTags :: [KernelRuleTag] allKernelRuleTags = [minBound .. maxBound] allFoundationAxiomTags :: [FoundationAxiomTag] allFoundationAxiomTags = [minBound .. maxBound] stableTagOrder :: Show tag => String -> (tag -> ByteString) -> [tag] -> [tag] stableTagOrder description encodeTag tags | Set.size encodedTags == length tags = List.sortOn encodeTag tags | otherwise = impossible ("duplicate stable " <> description <> " tag in " <> show tags) where encodedTags = Set.fromList (encodeTag <$> tags) codecInvariant :: Either MathematicalCodecError value -> value codecInvariant = either (impossible . ("canonical codec invariant: " <>) . show) id