1 files changed, 108 insertions, 0 deletions
diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index c03c21c..78ad27e 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -50,6 +50,8 @@ unitTests =
             propagatesUnsafeAuthorityThroughLocalClaims
         , testCase "aggregates exact Vampire obligations"
             aggregatesExactVampireObligations
+        , testCase "validates complete resolver batches before rejection"
+            validatesCompleteResolverBatchesBeforeRejection
         , testCase "preserves source-axiom safety through Vampire validation"
             preservesSourceAxiomSafetyThroughVampireValidation
         , testCase "materializes a sealed import with fresh authority"
@@ -759,6 +761,112 @@ aggregatesExactVampireObligations =
                     ("unexpected omitted validation count: "
                         <> show (length records))
 
+validatesCompleteResolverBatchesBeforeRejection :: Assertion
+validatesCompleteResolverBatchesBeforeRejection =
+    withTemporaryDirectory "felix-declaration-batch-integrity" \root -> do
+        fixture <- makeFixture
+        let executable = root Posix.</> "vampire"
+            firstLocation = mkLocation (FileId 76) 1 1
+            secondLocation = mkLocation (FileId 76) 2 1
+        writeAcceptedVampire executable
+        mismatchedTask <-
+            makePreparedObligation
+                fixture
+                Foundation.EmptyCharacteristic
+        let integrityResolver =
+                Declaration.vampireBatchResolver \_tasks -> do
+                    mismatched <- resolveAccepted executable mismatchedTask
+                    pure
+                        ( Right (Provers.CounterSatisfiable "earlier")
+                        :| [mismatched]
+                        )
+        integrityOutcome <-
+            (runDriverWithResolver fixture integrityResolver do
+                Declaration.commitProofDeclaration
+                    (Semantic.proofSyntaxId "batch-integrity-priority") do
+                        candidates <- Declaration.reserveCandidateBatch
+                            ( factSpec fixture "batch-integrity-first"
+                            :| [factSpec fixture "batch-integrity-second"]
+                            )
+                        Declaration.authorizeVampireCandidateBatch
+                            ( ( firstLocation
+                              , NonEmpty.head candidates
+                              , Declaration.prepareCurrentCandidateVampire
+                              )
+                            :| [ ( secondLocation
+                                 , NonEmpty.last candidates
+                                 , Declaration.prepareCurrentCandidateVampire
+                                 )
+                               ]
+                            )
+                :: IO
+                    (Declaration.DriverResult Text
+                        ((), Declaration.CommittedDeclarationBatch)))
+        case integrityOutcome of
+            Declaration.DriverFailed
+                    (Declaration.DriverDeclarationFailed
+                        (Declaration.ProofObligationFailedAt
+                            location
+                            Declaration.VampireRequestMismatch))
+                    prefix -> do
+                assertEqual
+                    "later request mismatch retains its location"
+                    secondLocation
+                    location
+                assertEqual
+                    "integrity failure rolls back the complete declaration"
+                    0
+                    (length
+                        (Declaration.pendingModulePrefixBatches prefix))
+            Declaration.DriverFailed failure _prefix ->
+                assertFailure
+                    ("unexpected batch-integrity failure: " <> show failure)
+            Declaration.DriverSucceeded{} ->
+                assertFailure
+                    "earlier ordinary rejection concealed no integrity failure"
+            Declaration.DriverSealFailed{} ->
+                assertFailure "invalid batch reached module sealing"
+
+        prepared <-
+            makePreparedObligation
+                fixture
+                Foundation.EmptyCharacteristic
+        let excessResolver =
+                Declaration.vampireBatchResolver \_tasks ->
+                    pure
+                        ( Right (Provers.CounterSatisfiable "first")
+                        :| [Right (Provers.CounterSatisfiable "excess")]
+                        )
+        excessOutcome <-
+            (runDriverWithResolver fixture excessResolver do
+                Declaration.commitProofDeclaration
+                    (Semantic.proofSyntaxId "singleton-excess-result") do
+                        candidate <- Declaration.reserveCandidate
+                            (factSpec fixture "singleton-excess-result")
+                        Declaration.authorizeVampireCandidate candidate
+                            (Declaration.acceptVampireObligation prepared)
+                :: IO
+                    (Declaration.DriverResult Text
+                        ((), Declaration.CommittedDeclarationBatch)))
+        case excessOutcome of
+            Declaration.DriverFailed
+                    (Declaration.DriverDeclarationFailed
+                        (Declaration.VampireResolverBatchSizeMismatch 1 2))
+                    prefix ->
+                assertEqual
+                    "malformed singleton response publishes no declaration"
+                    0
+                    (length
+                        (Declaration.pendingModulePrefixBatches prefix))
+            Declaration.DriverFailed failure _prefix ->
+                assertFailure
+                    ("unexpected singleton-cardinality failure: "
+                        <> show failure)
+            Declaration.DriverSucceeded{} ->
+                assertFailure "singleton resolver ignored an excess result"
+            Declaration.DriverSealFailed{} ->
+                assertFailure "malformed singleton reached module sealing"
+
 preservesSourceAxiomSafetyThroughVampireValidation :: Assertion
 preservesSourceAxiomSafetyThroughVampireValidation =
     withTemporaryDirectory "felix-declaration-source-axiom" \root -> do