Authorize exact defining equations

1 files changed, 75 insertions, 4 deletions

diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index d5bbfda..d83a22c 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -1501,6 +1501,7 @@ lowersExactOrdinaryDeclarations = do
         void (Exact.commitPreparedExactBinding preparedAbbreviation)
         (_afterDefinition, preparedDefinition) <-
             compile afterAbbreviation definition (entry definitionSymbol)
+        void (Exact.commitPreparedExactBinding preparedDefinition)
         pure
             ( preparedSignature
             , preparedAbbreviation
@@ -1510,11 +1511,11 @@ lowersExactOrdinaryDeclarations = do
         Declaration.DriverSucceeded
                 (preparedSignature, preparedAbbreviation, preparedDefinition)
                 interface prefix _closure -> do
-            assertEqual "two committed declarations"
-                2
+            assertEqual "three committed declarations"
+                3
                 (length (Semantic.semanticInterfaceDeclarations interface))
-            assertEqual "two committed batches"
-                2
+            assertEqual "three committed batches"
+                3
                 (length (Declaration.pendingModulePrefixBatches prefix))
             assertEqual "opaque signature family"
                 Identity.OpaqueObject
@@ -1549,11 +1550,81 @@ lowersExactOrdinaryDeclarations = do
                                 ("unexpected definition content: " <> show content)
                 Nothing ->
                     assertFailure "new definition object was not prepared"
+            case reverse (Declaration.pendingModulePrefixBatches prefix) of
+                definitionBatch : _ -> do
+                    case Declaration.committedBatchDeclarationValidation
+                            definitionBatch of
+                        Just record ->
+                            case Semantic.declarationValidationRecordCertificates
+                                    record of
+                                [certificate] -> do
+                                    assertEqual "definition authority"
+                                        (Authority.CheckedKernelConstruction
+                                            (Authority.CheckedDefinitionEquation
+                                                (Exact.preparedExactObjectId
+                                                    preparedDefinition)))
+                                        (Authority.validationDirectAuthorization
+                                            certificate)
+                                    assertEqual "definition authority is clean"
+                                        Authority.cleanAuthoritySafety
+                                        (Authority.factAuthoritySafety
+                                            (Authority.validationTarget
+                                                certificate))
+                                certificates ->
+                                    assertFailure
+                                        ("unexpected definition certificate count: "
+                                            <> show (length certificates))
+                        Nothing ->
+                            assertFailure "definition has no declaration validation"
+                [] -> assertFailure "definition batch is absent"
         Declaration.DriverFailed failure _prefix ->
             assertFailure ("exact lowering failed: " <> show failure)
         Declaration.DriverSealFailed failure _prefix ->
             assertFailure ("exact lowering did not seal: " <> show failure)
 
+    let theory = Identity.theoryId (fixtureFoundation fixture)
+        mismatchBody = Core.COpaqueInteger 0
+        mismatchType = Core.TySet
+        mismatchId =
+            Identity.transparentObjectId theory mismatchType mismatchBody
+        mismatchObject =
+            Identity.assertedObject
+                mismatchId
+                (Identity.TransparentObjectContent
+                    theory mismatchType mismatchBody)
+    let mismatchAction
+            :: Declaration.ModuleDriver Text
+                ((), Declaration.CommittedDeclarationBatch)
+        mismatchAction =
+            Declaration.commitCompiledDeclaration
+                (Semantic.declarationSyntaxId
+                    "mismatched-definition-equation") do
+                    Declaration.addDeclarationObject mismatchObject
+                    candidate <- Declaration.reserveCandidate
+                        (factSpec fixture "not-a-definition-equation")
+                    Declaration.authorizeCompiledDeclaration
+                        (Declaration.authorizeDefinitionEquationCandidate
+                            mismatchId
+                            candidate)
+    mismatch <- runDriver fixture mismatchAction
+    case mismatch of
+        Declaration.DriverFailed
+                (Declaration.DriverDeclarationFailed
+                    Declaration.DefinitionEquationCandidateMismatch)
+                prefix ->
+            assertEqual "mismatched equation publishes no batch"
+                0
+                (length (Declaration.pendingModulePrefixBatches prefix))
+        Declaration.DriverFailed failure _prefix ->
+            assertFailure
+                ("unexpected mismatched-equation failure: " <> show failure)
+        Declaration.DriverSucceeded{} ->
+            assertFailure "mismatched definition equation was authorized"
+        Declaration.DriverSealFailed failure _prefix ->
+            assertFailure
+                ("mismatched definition equation reached sealing: "
+                    <> show failure)
+
 reconstructsImportedGlobalBindings :: Assertion
 reconstructsImportedGlobalBindings = do
     producerFixture <- makeNamedFixture "global-producer"