Validate exact scoped Vampire obligations

2 files changed, 143 insertions, 0 deletions

diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs
index 493410a..0c4ff71 100644
--- a/source/Test/Unit/Backend.hs
+++ b/source/Test/Unit/Backend.hs
@@ -50,6 +50,9 @@ unitTests =
             "projects proposition equality as equivalence"
             classifiesPropositionEquality
         , testCase
+            "projects exact ambient support"
+            projectsExactAmbientSupport
+        , testCase
             "routes implicit, explicit, and local-only problems"
             routesCompleteProblems
         , testCase
@@ -81,6 +84,49 @@ classifiesPropositionEquality = do
                 ("proposition equality was not projected: "
                     <> show exclusions)
 
+projectsExactAmbientSupport :: Assertion
+projectsExactAmbientSupport = do
+    let term :: CanonicalTerm Void
+        term =
+            CForall TySet
+                (CEq TySet
+                    (CBound 1)
+                    (CBound 3))
+    scoped <-
+        either
+            (assertFailure . show)
+            pure
+            (checkScopedCanonicalCore
+                (const Nothing)
+                [TySet, TySet, TySet]
+                term)
+    projected <-
+        either
+            (assertFailure . show)
+            pure
+            (projectSupportedProposition
+                (const Nothing)
+                (Vector.fromList
+                    [ (0 :: Int, TySet)
+                    , (1, TySet)
+                    , (2, TySet)
+                    ])
+                scoped)
+    assertEqual
+        "unused middle support is removed"
+        (Vector.fromList
+            [ (0 :: Int, TySet)
+            , (2, TySet)
+            ])
+        (supportedPropositionSupport projected)
+    assertEqual
+        "indices are remapped below nested binders"
+        (CForall TySet
+            (CEq TySet
+                (CBound 1)
+                (CBound 2)))
+        (supportedPropositionTerm projected)
+
 routesCompleteProblems :: Assertion
 routesCompleteProblems = do
     fofFact <-
diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index 975965c..87261b0 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -48,6 +48,8 @@ unitTests =
             propagatesUnsafeAuthorityThroughLocalClaims
         , testCase "aggregates exact Vampire obligations"
             aggregatesExactVampireObligations
+        , testCase "accepts exact scoped Vampire obligations"
+            acceptsExactScopedVampireObligations
         , testCase "preserves source-axiom safety through Vampire validation"
             preservesSourceAxiomSafetyThroughVampireValidation
         , testCase "materializes a sealed import with fresh authority"
@@ -716,6 +718,101 @@ aggregatesExactVampireObligations =
                     ("unexpected omitted validation count: "
                         <> show (length records))
 
+acceptsExactScopedVampireObligations :: Assertion
+acceptsExactScopedVampireObligations =
+    withTemporaryDirectory "felix-declaration-scoped-vampire" \root -> do
+        fixture <- makeNamedFixture "scoped-vampire"
+        let executable = root Posix.</> "vampire"
+        writeAcceptedVampire executable
+        closure <- expectRight
+            (Identity.validateObjectClosure
+                (Identity.theoryId (fixtureFoundation fixture))
+                [])
+        proposition <- expectRight
+            (Identity.validatePropositionContent
+                closure
+                (Core.CForall Core.TySet
+                    (Core.CEq Core.TySet
+                        (Core.CBound 0)
+                        (Core.CBound 0))))
+        scoped <- expectRight
+            (Core.checkScopedCanonicalCore
+                (const Nothing)
+                [Core.TySet]
+                (Core.CEq Core.TySet
+                    (Core.CBound 0)
+                    (Core.CBound 0)))
+        claim <- expectRight
+            (Backend.projectSupportedProposition
+                (const Nothing)
+                (Vector.singleton (0 :: Int, Core.TySet))
+                scoped)
+        capturedText <- IORef.newIORef Nothing
+        let resolver = Declaration.vampireResolver \task -> do
+                IORef.writeIORef capturedText
+                    (Just
+                        (Provers.preparedVerificationText
+                            (Provers.preparedTypedProverRequest task)))
+                resolveAccepted executable task
+            scopedLocals =
+                [] :: [Backend.TypedLocalPremise
+                    Int
+                    ()
+                    Identity.ObjectId]
+            action
+                :: Declaration.ModuleDriver Text
+                    ((), Declaration.CommittedDeclarationBatch)
+            action = Declaration.commitProofDeclaration
+                (Semantic.proofSyntaxId "scoped-vampire") do
+                    candidate <- Declaration.reserveCandidate
+                        (Declaration.candidateSpec
+                            proposition
+                            Semantic.SearchEligible
+                            [Semantic.semanticName "scoped-vampire"])
+                    Declaration.authorizeVampireCandidate candidate do
+                        prepared <-
+                            Declaration.prepareVampireObligation
+                                claim
+                                scopedLocals
+                                []
+                                Declaration.VampireLocalPremises
+                                >>= either
+                                    (error . show)
+                                    pure
+                        Declaration.acceptPreparedVampireObligation
+                            prepared
+        result <- runDriverWithResolver fixture resolver action
+        case result of
+            Declaration.DriverSucceeded
+                    (_value, batch) _interface _prefix _closure -> do
+                assertEqual
+                    "one scoped request is retained"
+                    1
+                    (case Declaration.committedBatchProofValidations batch of
+                        [record] ->
+                            case Authority.validationDirectAuthorization
+                                    (Semantic.proofValidationRecordCertificate
+                                        record) of
+                                Authority.CheckedSourceProof requests ->
+                                    length requests
+                                _ -> 0
+                        _ -> 0)
+                problemText <-
+                    maybe
+                        (assertFailure "scoped request was not executed")
+                        pure
+                        =<< IORef.readIORef capturedText
+                assertBool
+                    "the scoped binder has a task-local backend name"
+                    ("zf_l0" `Text.isInfixOf` problemText)
+            Declaration.DriverFailed failure _prefix ->
+                assertFailure
+                    ("scoped Vampire declaration failed: " <> show failure)
+            Declaration.DriverSealFailed failure _prefix ->
+                assertFailure
+                    ("scoped Vampire declaration did not seal: "
+                        <> show failure)
+
 preservesSourceAxiomSafetyThroughVampireValidation :: Assertion
 preservesSourceAxiomSafetyThroughVampireValidation =
     withTemporaryDirectory "felix-declaration-source-axiom" \root -> do