Separate declaration semantics from evidence

1 files changed, 34 insertions, 0 deletions

diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index 78ad27e..56a6c6b 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -146,6 +146,21 @@ enforcesStagedCandidateOrder = do
             (Semantic.declarationDeltaFacts
                 (Declaration.committedBatchDelta batch)))
 
+    provenance <- runDriver fixture (priorDeclarationUse fixture)
+    case provenance of
+        Declaration.DriverFailed
+                (Declaration.DriverDeclarationFailed
+                    (Declaration.CandidateOutsideDeclaration slot))
+                prefix -> do
+            assertEqual
+                "cross-declaration staged premise"
+                (localFact fixture 0)
+                slot
+            assertSingleCompletedPrefix prefix
+        _other ->
+            assertFailure
+                "cross-declaration staged provenance was not rejected"
+
     traverse_
         (\(label, action, expectedPremise, expectedCandidate) -> do
             result <- runDriver fixture action
@@ -234,6 +249,25 @@ enforcesStagedCandidateOrder = do
                         premise <- Declaration.useStagedCandidate second
                         pure (Kernel.importedFactDerivation premise))
 
+    priorDeclarationUse fixture = do
+        (premise, _batch) <- Declaration.commitCompiledDeclaration
+            (Semantic.declarationSyntaxId "prior-stage") do
+                candidate <- Declaration.reserveCandidate
+                    (factSpec fixture "prior-stage")
+                Declaration.authorizeCompiledDeclaration
+                    (Declaration.authorizeSourceAxiomCandidate candidate)
+                pure candidate
+        void
+            (Declaration.commitCompiledDeclaration
+                (Semantic.declarationSyntaxId "later-stage") do
+                    candidate <- Declaration.reserveCandidate
+                        (factSpec fixture "later-stage")
+                    Declaration.authorizeCompiledDeclaration
+                        (Declaration.authorizeKernelProofCandidate candidate do
+                            imported <-
+                                Declaration.useStagedCandidate premise
+                            pure (Kernel.importedFactDerivation imported)))
+
 retainsOnlyAppendedPrefixes :: Assertion
 retainsOnlyAppendedPrefixes = do
     fixture <- makeFixture