Keep validation records inert

4 files changed, 124 insertions, 448 deletions

diff --git a/source/Checking/Authority.hs b/source/Checking/Authority.hs
index b932bc4..05216f6 100644
--- a/source/Checking/Authority.hs
+++ b/source/Checking/Authority.hs
@@ -35,6 +35,7 @@ module Checking.Authority
     , CandidateSafety
     , initialCandidateSafety
     , candidateSafetyAuthority
+    , candidateFactAuthority
     , consumeFactAuthority
     , addCandidateEscape
     , FactConsumptionError(..)
@@ -275,6 +276,17 @@ candidateSafetyAuthority :: CandidateSafety -> AuthoritySafety
 candidateSafetyAuthority (CandidateSafety safety) =
     safety
 
+-- | Freeze the final safety of one completed candidate into public authority.
+--
+-- Phase 2's trusted completion boundary must use 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 FactConsumptionError
     = ConsumedFactTheoremMismatch !TheoremRef !TheoremRef
     deriving stock (Show, Eq)
diff --git a/source/Checking/Materialization.hs b/source/Checking/Materialization.hs
index ac16105..1ddb1e6 100644
--- a/source/Checking/Materialization.hs
+++ b/source/Checking/Materialization.hs
@@ -1,26 +1,16 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 
--- | Pure validation and nonserializable builder-local fact capabilities.
+-- | Pure applicability checks for later trusted materialization.
+--
+-- Successful checks are inert. Phase 2 fresh completion and Phase 4 validated
+-- loading or sealing own the runtime authority that may publish a fact.
 module Checking.Materialization
-    ( BuilderIdentity
-    , builderIdentity
-    , DeclarationInvocationId
-    , declarationInvocationId
-    , AuthorizationBuilder
-    , authorizationBuilder
-    , authorizationBuilderPrefix
-    , DeclarationAuthorizationScope
-    , beginDeclarationAuthorization
-    , CandidateValidation(..)
+    ( CandidateValidation(..)
     , candidateProofValidation
     , candidateDeclarationValidation
-    , PendingFactAuthorization
-    , materializeCandidateFact
-    , BuilderFactAuthorization
-    , builderFactAuthority
-    , appendAuthorizedDeclaration
-    , materializeImportedFact
+    , checkCandidateValidation
+    , checkImportedMembership
     , MaterializationError(..)
     ) where
 
@@ -28,81 +18,12 @@ import Base
 import Checking.Authority
 import Checking.Identity
 import Checking.Semantic
-import Felix.Module
 
 import Control.Monad (unless)
 import Data.List (filter)
-import Data.Set qualified as Set
 import Numeric.Natural (Natural)
 
 
-newtype BuilderIdentity =
-    BuilderIdentity Natural
-    deriving stock (Show, Eq, Ord)
-
-builderIdentity :: Natural -> BuilderIdentity
-builderIdentity =
-    BuilderIdentity
-
-newtype DeclarationInvocationId =
-    DeclarationInvocationId Natural
-    deriving stock (Show, Eq, Ord)
-
-declarationInvocationId
-    :: Natural
-    -> DeclarationInvocationId
-declarationInvocationId =
-    DeclarationInvocationId
-
--- The constructor remains private. Phase 2 owns and threads this state.
-data AuthorizationBuilder = AuthorizationBuilder
-    !BuilderIdentity
-    !ModuleName
-    !PrefixContextId
-
-authorizationBuilder
-    :: BuilderIdentity
-    -> ModuleName
-    -> PrefixContextId
-    -> AuthorizationBuilder
-authorizationBuilder =
-    AuthorizationBuilder
-
-authorizationBuilderPrefix
-    :: AuthorizationBuilder
-    -> PrefixContextId
-authorizationBuilderPrefix
-        (AuthorizationBuilder _ _ prefix) =
-    prefix
-
-data DeclarationAuthorizationScope =
-    DeclarationAuthorizationScope
-        !BuilderIdentity
-        !ModuleName
-        !PrefixContextId
-        !DeclarationInvocationId
-        !DeclarationSlot
-
-beginDeclarationAuthorization
-    :: AuthorizationBuilder
-    -> DeclarationInvocationId
-    -> DeclarationSlot
-    -> Either MaterializationError DeclarationAuthorizationScope
-beginDeclarationAuthorization
-        (AuthorizationBuilder identity owner prefix)
-        invocation
-        slot = do
-    unless
-        (declarationSlotModule slot == owner)
-        (Left
-            (DeclarationScopeOwnerMismatch
-                owner
-                (declarationSlotModule slot)))
-    pure
-        (DeclarationAuthorizationScope
-            identity owner prefix invocation slot)
-
-
 data CandidateValidation
     = CandidateProofValidation
         !ProofValidationRecord
@@ -132,41 +53,8 @@ candidateDeclarationValidation
 candidateDeclarationValidation =
     CandidateDeclarationValidation
 
--- Deliberately no Show, Eq, NFData, or codec instance.
-data PendingFactAuthorization =
-    PendingFactAuthorization
-        !BuilderIdentity
-        !PrefixContextId
-        !DeclarationInvocationId
-        !DeclarationSlot
-        !FactSlot
-        !Natural
-        !(Maybe Natural)
-        !PropositionId
-        !FactAuthority
-
--- Deliberately nonserializable. The builder identity grants only session-local
--- use after the declaration append has consumed its pending authorization.
-data BuilderFactAuthorization =
-    BuilderFactAuthorization
-        !BuilderIdentity
-        !PropositionId
-        !FactAuthority
-
-builderFactAuthority
-    :: BuilderFactAuthorization
-    -> FactAuthority
-builderFactAuthority
-        (BuilderFactAuthorization _ _ authority) =
-    authority
-
 data MaterializationError
-    = DeclarationScopeOwnerMismatch !ModuleName !ModuleName
-    | BuilderIdentityMismatch
-    | BuilderPrefixMismatch !PrefixContextId !PrefixContextId
-    | DeclarationScopeMismatch
-    | CandidateOwnerMismatch !ModuleName !ModuleName
-    | CandidateFrontierNotEarlier !Natural !Natural
+    = CandidateFrontierNotEarlier !Natural !Natural
     | CandidateValidationIndexMissing !Natural
     | ProofValidationKeyMismatch
         !ProofValidationKey
@@ -187,10 +75,6 @@ data MaterializationError
     | CandidatePropositionMismatch
         !PropositionId
         !PropositionId
-    | PendingAuthorizationCountMismatch !Int !Int
-    | DuplicatePendingCandidate !FactSlot
-    | NonIncreasingCandidateStages
-    | PendingAuthorizationMismatch !FactSlot
     | ImportedOccurrenceMissing
         !SemanticFactOccurrenceFingerprint
     | ImportedOccurrenceAmbiguous
@@ -205,29 +89,24 @@ data MaterializationError
     deriving stock (Show, Eq)
 
 
-materializeCandidateFact
+-- | Check whether inert validation data applies to one exact candidate.
+--
+-- Success deliberately returns no builder authorization. A fresh trusted
+-- completion or compatible validated-store hit must perform this check before
+-- its owning phase mints runtime authority.
+checkCandidateValidation
     :: TheoryId
-    -> DeclarationAuthorizationScope
-    -> FactSlot
+    -> PrefixContextId
     -> Natural
     -> Maybe Natural
     -> CheckedPropositionContent
     -> FactAuthority
     -> DirectAuthorization
     -> CandidateValidation
-    -> Either MaterializationError PendingFactAuthorization
-materializeCandidateFact
-        theory
-        (DeclarationAuthorizationScope
-            identity owner prefix invocation declaration)
-        slot stage frontier proposition expectedAuthority expectedDirect
-        validation = do
-    unless
-        (factSlotModule slot == owner)
-        (Left
-            (CandidateOwnerMismatch
-                owner
-                (factSlotModule slot)))
+    -> Either MaterializationError ()
+checkCandidateValidation
+        theory prefix stage frontier proposition expectedAuthority
+        expectedDirect validation = do
     traverse_
         (\earlier ->
             unless
@@ -241,11 +120,6 @@ materializeCandidateFact
             prefix expectedAuthority validation
     validateCertificateTarget
         theory proposition expectedAuthority expectedDirect certificate
-    pure
-        (PendingFactAuthorization
-            identity prefix invocation declaration slot stage frontier
-            (checkedPropositionId proposition)
-            expectedAuthority)
 
 candidateCertificate
     :: PrefixContextId
@@ -258,7 +132,7 @@ candidateCertificate prefix authority = \case
                 proofValidationRecordKey record
             certificate =
                 proofValidationRecordCertificate record
-        let expectedKey =
+            expectedKey =
                 proofValidationKey
                     (theoremId
                         (factAuthorityTheorem authority))
@@ -276,7 +150,7 @@ candidateCertificate prefix authority = \case
                 declarationValidationRecordKey record
             certificates =
                 declarationValidationRecordCertificates record
-        let expectedKey =
+            expectedKey =
                 declarationValidationKey
                     syntax prefix objects theorems
         unless
@@ -340,103 +214,19 @@ validateCertificateTarget
                 (theoremRefProposition reference)))
 
 
-appendAuthorizedDeclaration
-    :: AuthorizationBuilder
-    -> DeclarationAuthorizationScope
-    -> DeclarationInterfaceDelta
-    -> [PendingFactAuthorization]
-    -> Either
-        MaterializationError
-        (AuthorizationBuilder, [BuilderFactAuthorization])
-appendAuthorizedDeclaration
-        (AuthorizationBuilder
-            builderIdentity' owner currentPrefix)
-        (DeclarationAuthorizationScope
-            scopeIdentity scopeOwner predecessor invocation declaration)
-        delta pending = do
-    unless
-        (builderIdentity' == scopeIdentity)
-        (Left BuilderIdentityMismatch)
-    unless
-        (owner == scopeOwner
-            && declaration == declarationDeltaSlot delta)
-        (Left DeclarationScopeMismatch)
-    unless
-        (currentPrefix == predecessor)
-        (Left
-            (BuilderPrefixMismatch
-                predecessor currentPrefix))
-    let occurrences =
-            declarationDeltaFacts delta
-    unless
-        (length pending == length occurrences)
-        (Left
-            (PendingAuthorizationCountMismatch
-                (length occurrences)
-                (length pending)))
-    case firstDuplicate
-            (pendingSlot <$> pending) of
-        Just duplicate ->
-            Left (DuplicatePendingCandidate duplicate)
-        Nothing ->
-            pure ()
-    unless
-        (strictlyIncreasing (pendingStage <$> pending))
-        (Left NonIncreasingCandidateStages)
-    traverse_
-        (uncurry
-            (validatePending
-                scopeIdentity predecessor invocation declaration))
-        (zip pending occurrences)
-    let next =
-            nextPrefixContextId predecessor delta
-        authorizations =
-            zipWith
-                (\pendingAuthorization occurrence ->
-                    BuilderFactAuthorization
-                        builderIdentity'
-                        (pendingProposition pendingAuthorization)
-                        (semanticFactAuthority occurrence))
-                pending
-                occurrences
-    pure
-        ( AuthorizationBuilder builderIdentity' owner next
-        , authorizations
-        )
-  where
-    validatePending identity prefix expectedInvocation expectedDeclaration
-            pendingAuthorization occurrence =
-        unless
-            ( pendingIdentity pendingAuthorization == identity
-                && pendingPrefix pendingAuthorization == prefix
-                && pendingInvocation pendingAuthorization
-                    == expectedInvocation
-                && pendingDeclaration pendingAuthorization
-                    == expectedDeclaration
-                && pendingSlot pendingAuthorization
-                    == semanticFactSlot occurrence
-                && pendingProposition pendingAuthorization
-                    == semanticFactProposition occurrence
-                && pendingAuthority pendingAuthorization
-                    == semanticFactAuthority occurrence
-            )
-            (Left
-                (PendingAuthorizationMismatch
-                    (pendingSlot pendingAuthorization)))
-
-
-materializeImportedFact
+-- | Validate exact membership in inert canonical interface data.
+--
+-- Logical sealing or atomic cached installation must additionally supply the
+-- opaque runtime evidence before an importer receives builder authority.
+checkImportedMembership
     :: TheoryId
-    -> AuthorizationBuilder
     -> SemanticInterface
     -> SemanticFactOccurrenceFingerprint
     -> CheckedPropositionContent
     -> FactAuthority
-    -> Either MaterializationError BuilderFactAuthorization
-materializeImportedFact
-        theory
-        (AuthorizationBuilder identity _owner _prefix)
-        interface fingerprint proposition expectedAuthority = do
+    -> Either MaterializationError SemanticFactOccurrence
+checkImportedMembership
+        theory interface fingerprint proposition expectedAuthority = do
     occurrence <-
         case filter
                 ((== fingerprint) . semanticFactFingerprint)
@@ -474,60 +264,8 @@ materializeImportedFact
             (ImportedPropositionMismatch
                 (checkedPropositionId proposition)
                 (semanticFactProposition occurrence)))
-    pure
-        (BuilderFactAuthorization
-            identity
-            (checkedPropositionId proposition)
-            actualAuthority)
-
+    pure occurrence
 
-pendingIdentity :: PendingFactAuthorization -> BuilderIdentity
-pendingIdentity
-        (PendingFactAuthorization identity _ _ _ _ _ _ _ _) =
-    identity
-
-pendingPrefix :: PendingFactAuthorization -> PrefixContextId
-pendingPrefix
-        (PendingFactAuthorization _ prefix _ _ _ _ _ _ _) =
-    prefix
-
-pendingInvocation
-    :: PendingFactAuthorization
-    -> DeclarationInvocationId
-pendingInvocation
-        (PendingFactAuthorization _ _ invocation _ _ _ _ _ _) =
-    invocation
-
-pendingDeclaration
-    :: PendingFactAuthorization
-    -> DeclarationSlot
-pendingDeclaration
-        (PendingFactAuthorization _ _ _ declaration _ _ _ _ _) =
-    declaration
-
-pendingSlot :: PendingFactAuthorization -> FactSlot
-pendingSlot
-        (PendingFactAuthorization _ _ _ _ slot _ _ _ _) =
-    slot
-
-pendingStage :: PendingFactAuthorization -> Natural
-pendingStage
-        (PendingFactAuthorization _ _ _ _ _ stage _ _ _) =
-    stage
-
-pendingProposition
-    :: PendingFactAuthorization
-    -> PropositionId
-pendingProposition
-        (PendingFactAuthorization _ _ _ _ _ _ _ proposition _) =
-    proposition
-
-pendingAuthority
-    :: PendingFactAuthorization
-    -> FactAuthority
-pendingAuthority
-        (PendingFactAuthorization _ _ _ _ _ _ _ _ authority) =
-    authority
 
 nthNatural :: Natural -> [value] -> Maybe value
 nthNatural ordinal =
@@ -539,19 +277,3 @@ nthNatural ordinal =
         Just value
     go remaining (_ : rest) =
         go (remaining - 1) rest
-
-firstDuplicate :: Ord value => [value] -> Maybe value
-firstDuplicate =
-    go Set.empty
-  where
-    go _ [] =
-        Nothing
-    go seen (value : rest)
-        | value `Set.member` seen =
-            Just value
-        | otherwise =
-            go (Set.insert value seen) rest
-
-strictlyIncreasing :: Ord value => [value] -> Bool
-strictlyIncreasing values =
-    and (zipWith (<) values (drop 1 values))
diff --git a/source/Test/Unit/Identity.hs b/source/Test/Unit/Identity.hs
index 6642679..45cdfdf 100644
--- a/source/Test/Unit/Identity.hs
+++ b/source/Test/Unit/Identity.hs
@@ -517,6 +517,27 @@ validatesCompactFactAuthority = do
             , Authority.preparedRequestId "first"
             , Authority.preparedRequestId "second"
             ]
+        directAuthorizations =
+            [ Authority.CheckedKernelConstruction
+                (Authority.FoundationLeaf
+                    Foundation.EmptyCharacteristic)
+            , Authority.CheckedKernelConstruction
+                (Authority.GuardedFoundationRule
+                    Foundation.SetLfpBound)
+            , Authority.CheckedKernelConstruction
+                (Authority.CheckedDefinitionEquation
+                    (fixtureIntrinsic fixture))
+            , 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
@@ -529,6 +550,17 @@ validatesCompactFactAuthority = do
         "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)
@@ -565,6 +597,16 @@ validatesCompactFactAuthority = do
                 (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
diff --git a/source/Test/Unit/Materialization.hs b/source/Test/Unit/Materialization.hs
index 7c492d8..45b4a38 100644
--- a/source/Test/Unit/Materialization.hs
+++ b/source/Test/Unit/Materialization.hs
@@ -13,111 +13,51 @@ import Felix.Math.Codec
 import Felix.Module
 import Felix.Source
 
-import Numeric.Natural (Natural)
 import Test.Tasty
 import Test.Tasty.HUnit
 
 
 unitTests :: TestTree
 unitTests =
-    testGroup "Fact materialization"
-        [ testCase "consumes exact pending authorization once"
-            consumesPendingAuthorization
+    testGroup "Validation applicability"
+        [ testCase "keeps serializable candidate validation inert"
+            keepsCandidateValidationInert
         , testCase "rejects inexact candidate validation"
             rejectsInexactCandidateValidation
         , testCase "selects ordered declaration certificates"
             selectsDeclarationCertificate
-        , testCase "materializes exact sealed membership"
-            materializesImportedMembership
+        , testCase "keeps raw interface membership inert"
+            keepsImportedMembershipInert
         ]
 
-consumesPendingAuthorization :: Assertion
-consumesPendingAuthorization = do
+keepsCandidateValidationInert :: Assertion
+keepsCandidateValidationInert = do
     fixture <- makeFixture
-    pending <- materializeProof fixture 0 Nothing
-    (advanced, [authorization]) <- expectRight
-        (Materialization.appendAuthorizedDeclaration
-            (fixtureBuilder fixture)
-            (fixtureScope fixture)
-            (fixtureDelta fixture)
-            [pending])
+    let check =
+            Materialization.checkCandidateValidation
+                (fixtureTheory fixture)
+                (fixturePrefix fixture)
+                0
+                Nothing
+                (fixtureProposition fixture)
+                (fixtureAuthority fixture)
+                (fixtureDirect fixture)
+                (fixtureProofValidation fixture)
     assertEqual
-        "append advances the exact semantic prefix"
-        (Semantic.nextPrefixContextId
-            (fixturePrefix fixture)
-            (fixtureDelta fixture))
-        (Materialization.authorizationBuilderPrefix advanced)
+        "freely constructed records yield only inert applicability"
+        (Right ())
+        check
     assertEqual
-        "append exposes the validated public authority"
-        (fixtureAuthority fixture)
-        (Materialization.builderFactAuthority authorization)
-    case Materialization.appendAuthorizedDeclaration
-            advanced
-            (fixtureScope fixture)
-            (fixtureDelta fixture)
-            [pending] of
-        Left Materialization.BuilderPrefixMismatch{} ->
-            pure ()
-        Left other ->
-            assertFailure
-                ("unexpected reused-pending error: " <> show other)
-        Right _ ->
-            assertFailure "reused pending authorization succeeded"
-    firstOccurrence <-
-        case Semantic.declarationDeltaFacts
-                (fixtureDelta fixture) of
-            [only] ->
-                pure only
-            _ ->
-                assertFailure "expected one fixture occurrence"
-                    >> fail "unreachable"
-    let secondSlot =
-            Semantic.factSlot
-                (Semantic.factSlotModule
-                    (fixtureFactSlot fixture))
-                (localFactOrdinal 1)
-        secondOccurrence =
-            Semantic.semanticFactOccurrence
-                secondSlot
-                (Identity.checkedPropositionId
-                    (fixtureProposition fixture))
-                (fixtureAuthority fixture)
-                Semantic.SearchEligible
-    duplicateDelta <- expectRight
-        (Semantic.declarationInterfaceDelta
-            (Semantic.declarationDeltaSlot
-                (fixtureDelta fixture))
-            [firstOccurrence, secondOccurrence]
-            []
-            []
-            [Identity.checkedPropositionId
-                (fixtureProposition fixture)]
-            (Semantic.declarationDeltaEnvironment
-                (fixtureDelta fixture)))
-    case Materialization.appendAuthorizedDeclaration
-            (fixtureBuilder fixture)
-            (fixtureScope fixture)
-            duplicateDelta
-            [pending, pending] of
-        Left
-            (Materialization.DuplicatePendingCandidate slot) ->
-                assertEqual
-                    "duplicated candidate slot"
-                    (fixtureFactSlot fixture)
-                    slot
-        Left other ->
-            assertFailure
-                ("unexpected duplicate-pending error: " <> show other)
-        Right _ ->
-            assertFailure "duplicated pending authorization succeeded"
+        "inert applicability data is reusable"
+        (Right ())
+        check
 
 rejectsInexactCandidateValidation :: Assertion
 rejectsInexactCandidateValidation = do
     fixture <- makeFixture
-    case Materialization.materializeCandidateFact
+    case Materialization.checkCandidateValidation
             (fixtureTheory fixture)
-            (fixtureScope fixture)
-            (fixtureFactSlot fixture)
+            (fixturePrefix fixture)
             1
             (Just 1)
             (fixtureProposition fixture)
@@ -144,10 +84,9 @@ rejectsInexactCandidateValidation = do
                     wrongKey
                     (fixtureCertificate fixture))
                 (Semantic.proofSyntaxId "proof")
-    case Materialization.materializeCandidateFact
+    case Materialization.checkCandidateValidation
             (fixtureTheory fixture)
-            (fixtureScope fixture)
-            (fixtureFactSlot fixture)
+            (fixturePrefix fixture)
             0
             Nothing
             (fixtureProposition fixture)
@@ -197,43 +136,41 @@ selectsDeclarationCertificate = do
                 syntax []
                 producedTheorems
                 1
-    _ <- expectRight
-        (Materialization.materializeCandidateFact
+    assertEqual
+        "candidate ordinal selects the second certificate"
+        (Right ())
+        (Materialization.checkCandidateValidation
             (fixtureTheory fixture)
-            (fixtureScope fixture)
-            (fixtureFactSlot fixture)
+            (fixturePrefix fixture)
             0
             Nothing
             (fixtureProposition fixture)
             (fixtureAuthority fixture)
             (fixtureDirect fixture)
             validation)
-    pure ()
 
-materializesImportedMembership :: Assertion
-materializesImportedMembership = do
+keepsImportedMembershipInert :: Assertion
+keepsImportedMembershipInert = do
     fixture <- makeFixture
-    authorization <- expectRight
-        (Materialization.materializeImportedFact
+    occurrence <- expectRight
+        (Materialization.checkImportedMembership
             (fixtureTheory fixture)
-            (fixtureBuilder fixture)
             (fixtureInterface fixture)
             (fixtureFingerprint fixture)
             (fixtureProposition fixture)
             (fixtureAuthority fixture))
     assertEqual
-        "sealed member authority"
+        "raw interface yields only its inert occurrence"
         (fixtureAuthority fixture)
-        (Materialization.builderFactAuthority authorization)
+        (Semantic.semanticFactAuthority occurrence)
     let wrongAuthority =
             Authority.factAuthority
                 (fixtureReference fixture)
                 (Authority.authoritySafety
                     (Authority.singletonEscapeKind
                         Authority.Omitted))
-    case Materialization.materializeImportedFact
+    case Materialization.checkImportedMembership
             (fixtureTheory fixture)
-            (fixtureBuilder fixture)
             (fixtureInterface fixture)
             (fixtureFingerprint fixture)
             (fixtureProposition fixture)
@@ -254,15 +191,10 @@ data Fixture = Fixture
     , fixtureAuthority :: !Authority.FactAuthority
     , fixtureDirect :: !Authority.DirectAuthorization
     , fixtureCertificate :: !Authority.ValidationCertificate
-    , fixtureFactSlot :: !Semantic.FactSlot
     , fixtureFingerprint
         :: !Semantic.SemanticFactOccurrenceFingerprint
-    , fixtureDelta :: !Semantic.DeclarationInterfaceDelta
     , fixtureInterface :: !Semantic.SemanticInterface
     , fixturePrefix :: !Semantic.PrefixContextId
-    , fixtureBuilder :: !Materialization.AuthorizationBuilder
-    , fixtureScope
-        :: !Materialization.DeclarationAuthorizationScope
     , fixtureProofValidation
         :: !Materialization.CandidateValidation
     }
@@ -327,17 +259,7 @@ makeFixture = do
         (Semantic.semanticInterface owner [] [delta])
     let prefix =
             Semantic.initialPrefixContextId theory owner []
-        builder =
-            Materialization.authorizationBuilder
-                (Materialization.builderIdentity 0)
-                owner
-                prefix
-    scope <- expectRight
-        (Materialization.beginDeclarationAuthorization
-            builder
-            (Materialization.declarationInvocationId 0)
-            declaration)
-    let syntax =
+        syntax =
             Semantic.proofSyntaxId "proof"
         key =
             Semantic.proofValidationKey
@@ -351,13 +273,9 @@ makeFixture = do
             , fixtureAuthority = authority
             , fixtureDirect = direct
             , fixtureCertificate = certificate
-            , fixtureFactSlot = slot
             , fixtureFingerprint = fingerprint
-            , fixtureDelta = delta
             , fixtureInterface = interface
             , fixturePrefix = prefix
-            , fixtureBuilder = builder
-            , fixtureScope = scope
             , fixtureProofValidation =
                 Materialization.candidateProofValidation
                     (Semantic.proofValidationRecord
@@ -365,24 +283,6 @@ makeFixture = do
                     syntax
             }
 
-materializeProof
-    :: Fixture
-    -> Natural
-    -> Maybe Natural
-    -> IO Materialization.PendingFactAuthorization
-materializeProof fixture stage frontier =
-    expectRight
-        (Materialization.materializeCandidateFact
-            (fixtureTheory fixture)
-            (fixtureScope fixture)
-            (fixtureFactSlot fixture)
-            stage
-            frontier
-            (fixtureProposition fixture)
-            (fixtureAuthority fixture)
-            (fixtureDirect fixture)
-            (fixtureProofValidation fixture))
-
 expectRight :: Show error => Either error value -> IO value
 expectRight = \case
     Left err ->