Open exact claim envelopes in proofs

1 files changed, 43 insertions, 8 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 420a964..8210d24 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -612,6 +612,12 @@ compilesExactOrdinaryProofs =
                                 (Backend.typedProblemGlobalPremises problem)
                            , Vector.length
                                 (Backend.typedProblemLocalPremises problem)
+                           , [ Vector.length
+                                (Backend.supportedPropositionSupport
+                                    (Backend.typedLocalPremiseProposition premise))
+                             | premise <- Vector.toList
+                                (Backend.typedProblemLocalPremises problem)
+                             ]
                            )
                         ])
                 runNoLoggingT
@@ -628,19 +634,19 @@ compilesExactOrdinaryProofs =
         let batches =
                 Declaration.pendingModulePrefixBatches
                     (Module.sealedTypedModulePrefix rootModule)
-        assertEqual "one definition and three theorem declarations"
-            4
+        assertEqual "one definition and five theorem declarations"
+            6
             (length batches)
         let proofBatches = drop 1 batches
         assertEqual "only closed theorem facts are published"
-            [1, 1, 1]
+            [1, 1, 1, 1, 1]
             [ length
                 (Semantic.declarationDeltaFacts
                     (Declaration.committedBatchDelta batch))
             | batch <- proofBatches
             ]
         assertEqual "proof request aggregation follows source structure"
-            [1, 2, 2]
+            [1, 2, 2, 1, 1]
             [ case Declaration.committedBatchProofValidations batch of
                 [record] ->
                     case Authority.validationDirectAuthorization
@@ -658,13 +664,42 @@ compilesExactOrdinaryProofs =
                             <> show (length records))
             | batch <- proofBatches
             ]
+        headerBatch <- sole "header-envelope proof batch"
+            (take 1 (drop 3 proofBatches))
+        headerProposition <- sole "header-envelope checked proposition"
+            (Declaration.committedBatchPropositions headerBatch)
+        assertEqual "header-envelope closed target"
+            (Core.CForall Core.TySet
+                (Core.CImp
+                    (Core.CEq Core.TySet
+                        (Core.CBound 0)
+                        (Core.CBound 0))
+                    (Core.CEq Core.TySet
+                        (Core.CBound 0)
+                        (Core.CBound 0))))
+            (Core.frozenCoreTerm
+                (Identity.checkedPropositionTerm headerProposition))
+        headerFact <- sole "header-envelope published fact"
+            (Semantic.declarationDeltaFacts
+                (Declaration.committedBatchDelta headerBatch))
+        assertEqual "header-envelope proof remains clean"
+            Authority.cleanAuthoritySafety
+            (Authority.factAuthoritySafety
+                (Semantic.semanticFactAuthority headerFact))
         observed <- readIORef observations
         case observed of
-            (implicitGlobals, 0)
-                : [(0, 1), (1, 2), (0, 0), (0, 1)] ->
-                    assertBool
-                        "implicit Auto selects visible FOF facts"
+            (implicitGlobals, 0, [])
+                : [ (0, 1, [1])
+                  , (1, 2, [1, 1])
+                  , (0, 0, [])
+                  , (0, 1, [1])
+                  , (0, 1, [1])
+                  , (generalizedGlobals, 0, [])
+                  ] -> do
+                    assertBool "implicit Auto selects visible FOF facts"
                         (implicitGlobals > 0)
+                    assertBool "generalized Auto selects visible FOF facts"
+                        (generalizedGlobals > 0)
             _ ->
                 assertFailure
                     ("unexpected exact proof premise policies: "