Migrate to `Felix` namespaceHEADhotg

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))