diff options
Diffstat (limited to 'source/Felix/Checking/Authority.hs')
| -rw-r--r-- | source/Felix/Checking/Authority.hs | 612 |
1 files changed, 612 insertions, 0 deletions
diff --git a/source/Felix/Checking/Authority.hs b/source/Felix/Checking/Authority.hs new file mode 100644 index 0000000..58c123f --- /dev/null +++ b/source/Felix/Checking/Authority.hs @@ -0,0 +1,612 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Compact public fact authority and exact contextual authorization. +module Felix.Checking.Authority + ( EscapeKind(..) + , EscapeKinds + , emptyEscapeKinds + , singletonEscapeKind + , escapeKinds + , escapeKindsToList + , unionEscapeKinds + , AuthoritySafety + , cleanAuthoritySafety + , authoritySafety + , authoritySafetyEscapeKinds + , unionAuthoritySafety + , FactAuthority + , factAuthority + , factAuthorityTheorem + , factAuthoritySafety + , PreparedRequestDialect(..) + , PreparedRequestMode(..) + , PreparedRequestId + , preparedRequestId + , GuardedRuleSet + , guardedRuleSet + , guardedRuleTags + , KernelConstructionDescriptor(..) + , DatatypeCompilationDescriptor + , datatypeCompilationDescriptor + , CompilationDescriptor(..) + , DirectAuthorization(..) + , ValidationCertificate + , validationCertificate + , validationTarget + , validationDirectAuthorization + , ValidationCertificateError(..) + , CandidateSafety + , initialCandidateSafety + , candidateSafetyAuthority + , candidateFactAuthority + , accumulateFactSafety + , addCandidateEscape + , FactSafetyError(..) + , putEscapeKindsCache + , getEscapeKindsCache + , putAuthoritySafetyCache + , getAuthoritySafetyCache + , putFactAuthorityCache + , getFactAuthorityCache + , putPreparedRequestIdCache + , getPreparedRequestIdCache + , putDirectAuthorizationCache + , getDirectAuthorizationCache + , putValidationCertificateCache + , getValidationCertificateCache + ) where + +import Base +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Cache.Codec + +import Control.DeepSeq (NFData) +import Control.Monad (unless, when) +import Data.Bits ((.&.), (.|.), bit, complement) +import Data.ByteString (ByteString) +import Data.ByteString qualified as ByteString +import Data.List (filter) +import Data.List.NonEmpty qualified as NonEmpty +import Data.Set qualified as Set +import Data.Word (Word8) + + +data EscapeKind + = SourceAxiom + | Omitted + deriving stock (Show, Eq, Ord, Enum, Bounded, Generic) + deriving anyclass (NFData) + +-- | Canonical bounded set. The bit positions are stable cache tags. +newtype EscapeKinds = + EscapeKinds Word8 + deriving stock (Show, Eq, Ord, Generic) + deriving newtype (NFData) + +emptyEscapeKinds :: EscapeKinds +emptyEscapeKinds = + EscapeKinds 0 + +singletonEscapeKind :: EscapeKind -> EscapeKinds +singletonEscapeKind = + EscapeKinds . escapeKindBit + +escapeKinds :: Foldable collection => collection EscapeKind -> EscapeKinds +escapeKinds = + foldl' + (\acc kind -> + unionEscapeKinds acc (singletonEscapeKind kind)) + emptyEscapeKinds + +escapeKindsToList :: EscapeKinds -> [EscapeKind] +escapeKindsToList kinds = + filter + (\kind -> + let EscapeKinds bits = kinds + in bits .&. escapeKindBit kind /= 0) + [SourceAxiom, Omitted] + +unionEscapeKinds :: EscapeKinds -> EscapeKinds -> EscapeKinds +unionEscapeKinds (EscapeKinds left) (EscapeKinds right) = + EscapeKinds (left .|. right) + +escapeKindBit :: EscapeKind -> Word8 +escapeKindBit = \case + SourceAxiom -> bit 0 + Omitted -> bit 1 + +allEscapeBits :: Word8 +allEscapeBits = + escapeKindBit SourceAxiom .|. escapeKindBit Omitted + + +data AuthoritySafety + = Clean + | EscapeHatchBacked !EscapeKinds + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +cleanAuthoritySafety :: AuthoritySafety +cleanAuthoritySafety = + Clean + +authoritySafety :: EscapeKinds -> AuthoritySafety +authoritySafety kinds + | kinds == emptyEscapeKinds = Clean + | otherwise = EscapeHatchBacked kinds + +authoritySafetyEscapeKinds :: AuthoritySafety -> EscapeKinds +authoritySafetyEscapeKinds = \case + Clean -> emptyEscapeKinds + EscapeHatchBacked kinds -> kinds + +unionAuthoritySafety + :: AuthoritySafety + -> AuthoritySafety + -> AuthoritySafety +unionAuthoritySafety left right = + authoritySafety + (unionEscapeKinds + (authoritySafetyEscapeKinds left) + (authoritySafetyEscapeKinds right)) + + +data FactAuthority = FactAuthority + !TheoremRef + !AuthoritySafety + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +factAuthority :: TheoremRef -> AuthoritySafety -> FactAuthority +factAuthority = + FactAuthority + +factAuthorityTheorem :: FactAuthority -> TheoremRef +factAuthorityTheorem (FactAuthority reference _) = + reference + +factAuthoritySafety :: FactAuthority -> AuthoritySafety +factAuthoritySafety (FactAuthority _ safety) = + safety + + +data PreparedRequestDialect + = PreparedRequestFof + | PreparedRequestTh0 + deriving stock (Show, Eq, Ord, Generic) + +data PreparedRequestMode + = PreparedRequestDirect + | PreparedRequestIndirect + deriving stock (Show, Eq, Ord, Generic) + +newtype PreparedRequestId = + PreparedRequestId CacheDigest + deriving stock (Show, Eq, Ord, Generic) + deriving newtype (Hashable, NFData) + +preparedRequestId + :: PreparedRequestDialect + -> PreparedRequestMode + -> ByteString + -> PreparedRequestId +preparedRequestId dialect mode bytes = + PreparedRequestId + (hashCacheFields + "felix-prepared-request-v2" + [ ByteString.singleton (preparedRequestDialectTag dialect) + , ByteString.singleton (preparedRequestModeTag mode) + , bytes + ]) + +preparedRequestDialectTag :: PreparedRequestDialect -> Word8 +preparedRequestDialectTag = \case + PreparedRequestFof -> 0x00 + PreparedRequestTh0 -> 0x01 + +preparedRequestModeTag :: PreparedRequestMode -> Word8 +preparedRequestModeTag = \case + PreparedRequestDirect -> 0x00 + PreparedRequestIndirect -> 0x01 + + +-- | A nonempty canonical set of guarded kernel rules. +newtype GuardedRuleSet = + GuardedRuleSet (Set KernelRuleTag) + deriving stock (Show, Eq, Ord, Generic) + +guardedRuleSet :: NonEmpty KernelRuleTag -> GuardedRuleSet +guardedRuleSet = + GuardedRuleSet . Set.fromList . NonEmpty.toList + +guardedRuleTags :: GuardedRuleSet -> Set KernelRuleTag +guardedRuleTags (GuardedRuleSet rules) = + rules + +data KernelConstructionDescriptor + = FoundationLeaf !FoundationAxiomTag + | GuardedFoundationRules !GuardedRuleSet + | CheckedDefinitionEquation !ObjectId + | CheckedSetConstructionExtensionality !ObjectId !CacheDigest + deriving stock (Show, Eq, Ord, Generic) + +-- | Exact semantic members of one trusted datatype compilation. +data DatatypeCompilationDescriptor = + DatatypeCompilationDescriptor + !ObjectId + !(NonEmpty ObjectId) + ![TheoremRef] + deriving stock (Show, Eq, Ord, Generic) + +datatypeCompilationDescriptor + :: ObjectId + -> NonEmpty ObjectId + -> [TheoremRef] + -> DatatypeCompilationDescriptor +datatypeCompilationDescriptor = + DatatypeCompilationDescriptor + +data CompilationDescriptor + = DatatypeCompilation !DatatypeCompilationDescriptor + deriving stock (Show, Eq, Ord, Generic) + +data DirectAuthorization + = CheckedKernelConstruction !KernelConstructionDescriptor + | CheckedSourceProof ![PreparedRequestId] + | TrustedCompilation !CompilationDescriptor + | SourceAxiomAuthorization + | OmittedAuthorization + deriving stock (Show, Eq, Ord, Generic) + + +data ValidationCertificate = ValidationCertificate + !FactAuthority + !DirectAuthorization + deriving stock (Show, Eq, Ord, Generic) + +data ValidationCertificateError + = SourceAxiomSafetyMismatch !AuthoritySafety + | OmittedSafetyMissing !AuthoritySafety + deriving stock (Show, Eq) + +validationCertificate + :: FactAuthority + -> DirectAuthorization + -> Either ValidationCertificateError ValidationCertificate +validationCertificate target direct = do + case direct of + SourceAxiomAuthorization -> + unless + (factAuthoritySafety target + == authoritySafety + (singletonEscapeKind SourceAxiom)) + (Left + (SourceAxiomSafetyMismatch + (factAuthoritySafety target))) + OmittedAuthorization -> + unless + (Omitted + `elem` escapeKindsToList + (authoritySafetyEscapeKinds + (factAuthoritySafety target))) + (Left + (OmittedSafetyMissing + (factAuthoritySafety target))) + CheckedKernelConstruction{} -> pure () + CheckedSourceProof{} -> pure () + TrustedCompilation{} -> pure () + pure (ValidationCertificate target direct) + +validationTarget :: ValidationCertificate -> FactAuthority +validationTarget (ValidationCertificate target _) = + target + +validationDirectAuthorization + :: ValidationCertificate + -> DirectAuthorization +validationDirectAuthorization (ValidationCertificate _ direct) = + direct + + +newtype CandidateSafety = + CandidateSafety AuthoritySafety + deriving stock (Show, Eq, Ord, Generic) + deriving newtype (NFData) + +initialCandidateSafety :: CandidateSafety +initialCandidateSafety = + CandidateSafety Clean + +candidateSafetyAuthority :: CandidateSafety -> AuthoritySafety +candidateSafetyAuthority (CandidateSafety safety) = + safety + +-- | Freeze the final safety of one completed candidate into public authority. +-- +-- The trusted completion boundary uses this projection for both the inert +-- validation certificate and its runtime pending authorization. +candidateFactAuthority + :: TheoremRef + -> CandidateSafety + -> FactAuthority +candidateFactAuthority reference (CandidateSafety safety) = + FactAuthority reference safety + +data FactSafetyError + = FactSafetyTheoremMismatch !TheoremRef !TheoremRef + deriving stock (Show, Eq) + +-- | Check theorem agreement and accumulate already-authorized public safety. +-- +-- This operation does not authorize a freely constructed 'FactAuthority'. +-- Callers may use it only after checking opaque global, imported, or staged +-- builder authorization at the boundary that owns that authority. +accumulateFactSafety + :: TheoremRef + -> FactAuthority + -> CandidateSafety + -> Either FactSafetyError CandidateSafety +accumulateFactSafety expected supplied (CandidateSafety current) = do + unless + (factAuthorityTheorem supplied == expected) + (Left + (FactSafetyTheoremMismatch + expected + (factAuthorityTheorem supplied))) + pure + (CandidateSafety + (unionAuthoritySafety + current + (factAuthoritySafety supplied))) + +addCandidateEscape + :: EscapeKind + -> CandidateSafety + -> CandidateSafety +addCandidateEscape kind (CandidateSafety current) = + CandidateSafety + (unionAuthoritySafety + current + (authoritySafety (singletonEscapeKind kind))) + + +putEscapeKindsCache :: EscapeKinds -> CachePut +putEscapeKindsCache (EscapeKinds bits) = + putCacheTag bits + +getEscapeKindsCache :: CacheGet EscapeKinds +getEscapeKindsCache = do + bits <- getCacheTag + unless + (bits .&. complement allEscapeBits == 0) + (fail "unknown cache escape-kind bit") + pure (EscapeKinds bits) + +putAuthoritySafetyCache :: AuthoritySafety -> CachePut +putAuthoritySafetyCache = \case + Clean -> + putCacheTag 0x00 + EscapeHatchBacked kinds -> do + putCacheTag 0x01 + putEscapeKindsCache kinds + +getAuthoritySafetyCache :: CacheGet AuthoritySafety +getAuthoritySafetyCache = + getCacheTag >>= \case + 0x00 -> + pure Clean + 0x01 -> do + kinds <- getEscapeKindsCache + when + (kinds == emptyEscapeKinds) + (fail "empty escape-hatch-backed safety") + pure (EscapeHatchBacked kinds) + tag -> + fail ("unknown cache authority-safety tag " <> show tag) + +putFactAuthorityCache :: FactAuthority -> CachePut +putFactAuthorityCache (FactAuthority reference safety) = do + putTheoremRefCache reference + putAuthoritySafetyCache safety + +getFactAuthorityCache :: CacheGet FactAuthority +getFactAuthorityCache = + FactAuthority + <$> getTheoremRefCache + <*> getAuthoritySafetyCache + +putPreparedRequestIdCache :: PreparedRequestId -> CachePut +putPreparedRequestIdCache (PreparedRequestId digest) = + putCacheDigest digest + +getPreparedRequestIdCache :: CacheGet PreparedRequestId +getPreparedRequestIdCache = + PreparedRequestId <$> getCacheDigest + +putDirectAuthorizationCache :: DirectAuthorization -> CachePut +putDirectAuthorizationCache = \case + CheckedKernelConstruction descriptor -> do + putCacheTag 0x00 + putKernelDescriptor descriptor + CheckedSourceProof requests -> do + putCacheTag 0x01 + putCacheList putPreparedRequestIdCache requests + TrustedCompilation descriptor -> do + putCacheTag 0x02 + putCompilationDescriptor descriptor + SourceAxiomAuthorization -> + putCacheTag 0x03 + OmittedAuthorization -> + putCacheTag 0x04 + +getDirectAuthorizationCache :: CacheGet DirectAuthorization +getDirectAuthorizationCache = + getCacheTag >>= \case + 0x00 -> + CheckedKernelConstruction <$> getKernelDescriptor + 0x01 -> + CheckedSourceProof + <$> getCacheList getPreparedRequestIdCache + 0x02 -> + TrustedCompilation <$> getCompilationDescriptor + 0x03 -> + pure SourceAxiomAuthorization + 0x04 -> + pure OmittedAuthorization + tag -> + fail ("unknown cache direct-authorization tag " <> show tag) + +putValidationCertificateCache :: ValidationCertificate -> CachePut +putValidationCertificateCache + (ValidationCertificate target direct) = do + putFactAuthorityCache target + putDirectAuthorizationCache direct + +getValidationCertificateCache :: CacheGet ValidationCertificate +getValidationCertificateCache = do + target <- getFactAuthorityCache + direct <- getDirectAuthorizationCache + case validationCertificate target direct of + Left err -> + fail ("invalid cache validation certificate: " <> show err) + Right certificate -> + pure certificate + + +putKernelDescriptor :: KernelConstructionDescriptor -> CachePut +putKernelDescriptor = \case + FoundationLeaf tag -> do + putCacheTag 0x00 + putFoundationTag tag + GuardedFoundationRules rules -> do + putCacheTag 0x01 + putCacheList putRuleTag + (Set.toAscList (guardedRuleTags rules)) + CheckedDefinitionEquation identity -> do + putCacheTag 0x02 + putObjectIdCache identity + CheckedSetConstructionExtensionality identity construction -> do + putCacheTag 0x03 + putObjectIdCache identity + putCacheDigest construction + +getKernelDescriptor :: CacheGet KernelConstructionDescriptor +getKernelDescriptor = + getCacheTag >>= \case + 0x00 -> FoundationLeaf <$> getFoundationTag + 0x01 -> do + tags <- getCacheList getRuleTag + rules <- + maybe + (fail "cache guarded-rule set is empty") + pure + (NonEmpty.nonEmpty tags) + unless (strictlyIncreasing tags) + (fail "cache guarded-rule tags are not in canonical order") + pure (GuardedFoundationRules (guardedRuleSet rules)) + 0x02 -> CheckedDefinitionEquation <$> getObjectIdCache + 0x03 -> + CheckedSetConstructionExtensionality + <$> getObjectIdCache + <*> getCacheDigest + tag -> + fail ("unknown cache kernel-construction tag " <> show tag) + +putCompilationDescriptor :: CompilationDescriptor -> CachePut +putCompilationDescriptor + (DatatypeCompilation + (DatatypeCompilationDescriptor + carrier constructors facts)) = do + putCacheTag 0x00 + putObjectIdCache carrier + putCacheList putObjectIdCache (NonEmpty.toList constructors) + putCacheList putTheoremRefCache facts + +getCompilationDescriptor :: CacheGet CompilationDescriptor +getCompilationDescriptor = + getCacheTag >>= \case + 0x00 -> do + carrier <- getObjectIdCache + rawConstructors <- + getCacheList getObjectIdCache + constructors <- + maybe + (fail "cache datatype compilation has no constructors") + pure + (NonEmpty.nonEmpty rawConstructors) + facts <- getCacheList getTheoremRefCache + pure + (DatatypeCompilation + (DatatypeCompilationDescriptor + carrier constructors facts)) + tag -> + fail ("unknown cache compilation tag " <> show tag) + +putFoundationTag :: FoundationAxiomTag -> CachePut +putFoundationTag = + putCacheTag . \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 + +getFoundationTag :: CacheGet FoundationAxiomTag +getFoundationTag = + getCacheTag >>= \case + 0x00 -> pure EmptyCharacteristic + 0x01 -> pure PairSetCharacteristic + 0x02 -> pure FamilyUnionCharacteristic + 0x03 -> pure PowerSetCharacteristic + 0x04 -> pure SeparationCharacteristic + 0x05 -> pure ReplacementCharacteristic + 0x06 -> pure SetChooseWitness + 0x07 -> pure SetExtensionality + 0x08 -> pure SetInduction + 0x09 -> pure PropositionalExtensionality + 0x0a -> pure DoubleNegationElim + 0x0b -> pure UnivOfContains + 0x0c -> pure UnivOfTransitive + 0x0d -> pure UnivOfFamilyUnionClosed + 0x0e -> pure UnivOfPowerSetClosed + 0x0f -> pure UnivOfReplacementClosed + 0x10 -> pure UnivOfMinimal + tag -> + fail ("unknown cache foundation-axiom tag " <> show tag) + +putRuleTag :: KernelRuleTag -> CachePut +putRuleTag = + putCacheTag . \case + SetLfpBound -> 0x00 + SetLfpLeast -> 0x01 + SetLfpFixed -> 0x02 + SetLfpInduct -> 0x03 + +getRuleTag :: CacheGet KernelRuleTag +getRuleTag = + getCacheTag >>= \case + 0x00 -> pure SetLfpBound + 0x01 -> pure SetLfpLeast + 0x02 -> pure SetLfpFixed + 0x03 -> pure SetLfpInduct + tag -> + fail ("unknown cache kernel-rule tag " <> show tag) + +strictlyIncreasing :: Ord value => [value] -> Bool +strictlyIncreasing values = + and (zipWith (<) values (drop 1 values)) |