Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 612 deletions

diff --git a/source/Checking/Authority.hs b/source/Checking/Authority.hs
deleted file mode 100644
index fb6cea0..0000000
--- a/source/Checking/Authority.hs
+++ /dev/null
@@ -1,612 +0,0 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Compact public fact authority and exact contextual authorization.
-module 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 Checking.Foundation
-import 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))