Reuse checked declaration object closures

1 files changed, 139 insertions, 0 deletions

diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index 067de08..0b3e67b 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -40,6 +40,8 @@ unitTests =
             propagatesUnsafeAuthorityThroughLocalClaims
         , testCase "aggregates exact Vampire obligations"
             aggregatesExactVampireObligations
+        , testCase "validates exact kernel construction descriptors"
+            validatesExactKernelConstructionDescriptors
         ]
 
 enforcesStagedCandidateOrder :: Assertion
@@ -546,6 +548,143 @@ writeAcceptedVampire executable = do
     Directory.setPermissions executable
         (Directory.setOwnerExecutable True permissions)
 
+validatesExactKernelConstructionDescriptors :: Assertion
+validatesExactKernelConstructionDescriptors = do
+    fixture <- makeFixture
+    proposition <- foundationProposition
+        fixture
+        Foundation.EmptyCharacteristic
+    let declaredObject = opaqueFixtureObject fixture
+        run descriptor =
+            runDriver fixture
+                (Declaration.commitCompiledDeclaration
+                    (Semantic.declarationSyntaxId
+                        "kernel-construction-descriptor") do
+                        Declaration.addDeclarationObject declaredObject
+                        candidate <- Declaration.reserveCandidate
+                            (Declaration.candidateSpec
+                                proposition
+                                Semantic.SearchEligible
+                                [Semantic.semanticName "kernel-construction"])
+                        Declaration.authorizeKernelConstructionCandidate
+                            descriptor
+                            candidate
+                            (pure
+                                (Kernel.foundationFactDerivation
+                                    Foundation.EmptyCharacteristic)))
+    success <- run
+        (Authority.FoundationLeaf
+            Foundation.EmptyCharacteristic)
+    case success of
+        Declaration.DriverSucceeded (_value, batch) _interface _prefix -> do
+            assertEqual
+                "new object is included in the checked declaration batch"
+                1
+                (length (Declaration.committedBatchObjects batch))
+            case Declaration.committedBatchDeclarationValidation batch of
+                Just record ->
+                    case Semantic.declarationValidationRecordCertificates
+                            record of
+                        [certificate] ->
+                            assertEqual
+                                "exact kernel descriptor is retained"
+                                (Authority.CheckedKernelConstruction
+                                    (Authority.FoundationLeaf
+                                        Foundation.EmptyCharacteristic))
+                                (Authority.validationDirectAuthorization
+                                    certificate)
+                        certificates ->
+                            assertFailure
+                                ("unexpected kernel certificate count: "
+                                    <> show (length certificates))
+                Nothing ->
+                    assertFailure "missing declaration validation"
+        Declaration.DriverFailed
+                (Declaration.DriverDeclarationFailed failure) _prefix ->
+            assertFailure
+                ("valid kernel descriptor failed: " <> show failure)
+        Declaration.DriverFailed
+                (Declaration.DriverActionFailed _failure) _prefix ->
+            assertFailure "unexpected ordinary driver failure"
+        Declaration.DriverSealFailed failure _prefix ->
+            assertFailure (show failure)
+
+    traverse_
+        (\(label, descriptor) -> do
+            outcome <- run descriptor
+            case outcome of
+                Declaration.DriverFailed
+                        (Declaration.DriverDeclarationFailed
+                            Declaration.KernelConstructionDescriptorMismatch)
+                        prefix ->
+                    assertEqual
+                        (label <> " publishes no declaration")
+                        0
+                        (length
+                            (Declaration.pendingModulePrefixBatches prefix))
+                Declaration.DriverFailed
+                        (Declaration.DriverDeclarationFailed other)
+                        _prefix ->
+                    assertFailure
+                        (label <> ": unexpected error " <> show other)
+                Declaration.DriverFailed
+                        (Declaration.DriverActionFailed _failure)
+                        _prefix ->
+                    assertFailure (label <> ": ordinary driver failure")
+                Declaration.DriverSucceeded{} ->
+                    assertFailure (label <> ": mismatch was accepted")
+                Declaration.DriverSealFailed{} ->
+                    assertFailure (label <> ": mismatch reached sealing"))
+        [ ( "wrong foundation leaf"
+          , Authority.FoundationLeaf
+                Foundation.PairSetCharacteristic
+          )
+        , ( "wrong construction family"
+          , Authority.GuardedFoundationRule
+                Foundation.SetLfpBound
+          )
+        ]
+
+foundationProposition
+    :: Fixture
+    -> Foundation.FoundationAxiomTag
+    -> IO Identity.CheckedPropositionContent
+foundationProposition fixture tag = do
+    closure <- expectRight
+        (Identity.validateObjectClosure
+            (Identity.theoryId (fixtureFoundation fixture))
+            [])
+    expectRight
+        (Identity.validatePropositionContent
+            closure
+            (Core.frozenCoreTerm
+                (Core.mapFrozenGlobals
+                    absurd
+                    (Foundation.foundationAxiomFrozen
+                        (fixtureFoundation fixture)
+                        tag))))
+
+opaqueFixtureObject :: Fixture -> Identity.AssertedObject
+opaqueFixtureObject fixture =
+    let theory = Identity.theoryId (fixtureFoundation fixture)
+        seed =
+            Identity.opaqueDeclarationSeed
+                (fixtureOwner fixture)
+                (localDeclarationOrdinal 0)
+                SignatureDeclaration
+                (generatedObjectSlot 0)
+        identity =
+            Identity.opaqueObjectId
+                theory
+                seed
+                Core.TySet
+    in Identity.assertedObject
+        identity
+        (Identity.OpaqueObjectContent
+            theory
+            seed
+            Core.TySet)
+
 
 data Fixture = Fixture
     { fixtureFoundation :: !Foundation.CheckedFoundation