Lower exact omitted proofs

3 files changed, 108 insertions, 5 deletions

diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index af5af96..3ed4739 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -686,6 +686,36 @@ aggregatesExactVampireObligations =
             Declaration.DriverSealFailed{} ->
                 assertFailure "mismatched request reached sealing"
 
+        unrecorded <- runDriver fixture do
+            Declaration.commitProofDeclaration
+                (Semantic.proofSyntaxId "unrecorded-omission") do
+                    candidate <- Declaration.reserveCandidate
+                        (factSpec fixture "unrecorded-omission")
+                    Declaration.authorizeOmittedCandidate candidate
+                        (pure ())
+        case unrecorded of
+            Declaration.DriverFailed
+                    (Declaration.DriverDeclarationFailed
+                        Declaration.OmittedProofDidNotRecordUse)
+                    prefix ->
+                assertEqual
+                    "unrecorded omission publishes no declaration"
+                    0
+                    (length
+                        (Declaration.pendingModulePrefixBatches prefix))
+            Declaration.DriverFailed
+                    (Declaration.DriverDeclarationFailed other) _prefix ->
+                assertFailure
+                    ("unexpected unrecorded-omission failure: "
+                        <> show other)
+            Declaration.DriverFailed
+                    (Declaration.DriverActionFailed _failure) _prefix ->
+                assertFailure "unexpected ordinary driver failure"
+            Declaration.DriverSucceeded{} ->
+                assertFailure "unrecorded omission was authorized"
+            Declaration.DriverSealFailed{} ->
+                assertFailure "unrecorded omission reached sealing"
+
         calls <- IORef.newIORef (0 :: Int)
         let countingResolver =
                 Declaration.vampireResolver \prepared -> do
@@ -699,6 +729,7 @@ aggregatesExactVampireObligations =
                     Declaration.authorizeOmittedCandidate candidate do
                         Declaration.acceptVampireObligation first
                         Declaration.acceptVampireObligation second
+                        Declaration.recordOmittedUse
             pure committed
         assertEqual
             "omitted proof still checks preceding obligations"
@@ -1395,7 +1426,8 @@ materializesSealedImport = do
             (Semantic.proofSyntaxId "sealed-import-producer") do
                 candidate <- Declaration.reserveCandidate
                     (factSpec fixture "producer-fact")
-                Declaration.authorizeOmittedCandidate candidate (pure ())
+                Declaration.authorizeOmittedCandidate candidate
+                    Declaration.recordOmittedUse
         pure batch
     (producerInterface, evidence, fingerprint) <-
         case producer of
@@ -1450,7 +1482,7 @@ materializesSealedImport = do
                         (factSpec fixture "consumer-fact")
                     Declaration.authorizeOmittedCandidate candidate do
                         _ <- Declaration.useAuthorizedFact fingerprint
-                        pure ()
+                        Declaration.recordOmittedUse
             pure committed
     case consumer of
         Declaration.DriverSucceeded committed _ _ _ -> do
@@ -2060,6 +2092,7 @@ foldsTransitiveAndDiamondEvidence = do
                         (factSpec fixture "local-after-import")
                     Declaration.authorizeOmittedCandidate candidate do
                         void (Declaration.useAuthorizedFact fingerprint)
+                        Declaration.recordOmittedUse
             pure committed
         pure batch
 
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 0a49b07..5e1a212 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -77,6 +77,8 @@ unitTests =
             compilesExactSourceAxioms
         , testCase "rejects source-axiom assumptions"
             rejectsExactSourceAxiomAssumptions
+        , testCase "compiles exact omitted proofs"
+            compilesExactOmittedProofs
         , testCase "reuses exact proof validation across module misses"
             reusesExactProofValidationAcrossModuleMisses
         , testCase "rejects declarations of fixed semantics"
@@ -754,6 +756,71 @@ rejectsExactSourceAxiomAssumptions = do
                 ("unexpected source-axiom assumption failure: "
                     <> show failure)
 
+compilesExactOmittedProofs :: Assertion
+compilesExactOmittedProofs =
+    Temp.withSystemTempDirectory "felix-exact-omitted" \root -> do
+        repository <- getCurrentDirectory
+        foundation <- expectRight Foundation.checkedFoundation
+        bootstrap <-
+            expectRight
+                =<< Module.buildBootstrapPreludeSession
+                    foundation unusedResolver
+        mounts <- exactFixtureMounts repository
+        workspace <- parseExactWorkspace
+            bootstrap mounts "test/phase5/exact-omitted.tex"
+        let executable = root Posix.</> "vampire"
+        writeFile executable
+            (unlines
+                [ "#!/bin/sh"
+                , "cat >/dev/null"
+                , "printf '%s\\n' '% SZS status Theorem for exact-omitted'"
+                ])
+        permissions <- getPermissions executable
+        setPermissions executable
+            (setOwnerExecutable True permissions)
+        calls <- newIORef (0 :: Int)
+        let resolver = Declaration.vampireResolver \prepared -> do
+                modifyIORef' calls (+ 1)
+                runNoLoggingT
+                    (Provers.runPreparedTypedProver
+                        (Provers.vampire
+                            executable
+                            Provers.defaultTimeLimit
+                            Provers.defaultMemoryLimit)
+                        prepared)
+        modules <-
+            compileParsedWorkspaceWithResolver
+                foundation bootstrap resolver workspace
+        sealed <- sole "exact omitted module" modules
+        assertEqual "only the non-omitted continuation invokes Vampire"
+            1
+            =<< readIORef calls
+        let batches =
+                Declaration.pendingModulePrefixBatches
+                    (Module.sealedTypedModulePrefix sealed)
+        assertEqual "top-level and nested omitted declarations"
+            2 (length batches)
+        for_ (zip ["top-level", "nested"] batches) \(label, batch) -> do
+            fact <- sole (label <> " omitted fact")
+                (Semantic.declarationDeltaFacts
+                    (Declaration.committedBatchDelta batch))
+            assertEqual (label <> " omitted safety")
+                (Authority.authoritySafety
+                    (Authority.singletonEscapeKind Authority.Omitted))
+                (Authority.factAuthoritySafety
+                    (Semantic.semanticFactAuthority fact))
+            record <- sole (label <> " omitted validation")
+                (Declaration.committedBatchProofValidations batch)
+            assertEqual (label <> " omitted direct authority")
+                Authority.OmittedAuthorization
+                (Authority.validationDirectAuthorization
+                    (Semantic.proofValidationRecordCertificate record))
+            assertEqual (label <> " publishes only its final theorem")
+                1
+                (length
+                    (Semantic.declarationDeltaFacts
+                        (Declaration.committedBatchDelta batch)))
+
 reusesExactProofValidationAcrossModuleMisses :: Assertion
 reusesExactProofValidationAcrossModuleMisses =
     Temp.withSystemTempDirectory "felix-exact-proof-cache" \root -> do
@@ -1475,6 +1542,7 @@ installsNonemptyImplicitPreludeEvidence = do
                         void
                             (Declaration.useAuthorizedFact
                                 preludeFingerprint)
+                        Declaration.recordOmittedUse
     consumedResult <- expectRight consumed
     case consumedResult of
         Declaration.DriverSucceeded{} -> pure ()
diff --git a/source/Test/Unit/Store.hs b/source/Test/Unit/Store.hs
index 916f56f..9f25a3b 100644
--- a/source/Test/Unit/Store.hs
+++ b/source/Test/Unit/Store.hs
@@ -397,7 +397,7 @@ installsSealedProducerForCachedImporter =
                                     [])
                             Declaration.authorizeOmittedCandidate candidate do
                                 _ <- Declaration.useAuthorizedFact fingerprint
-                                pure ()
+                                Declaration.recordOmittedUse
                     pure batch
                 :: IO
                     (Either
@@ -1092,7 +1092,8 @@ makeCommittedModule theory fixture = do
                             proposition
                             Semantic.SearchIneligible
                             [])
-                    Declaration.authorizeOmittedCandidate candidate (pure ())
+                    Declaration.authorizeOmittedCandidate candidate
+                        Declaration.recordOmittedUse
             pure ()
     (_value, prefix, semantic) <-
         case driver of
@@ -1169,7 +1170,8 @@ makePendingPrefix fixture objects = do
                             proposition
                             Semantic.SearchIneligible
                             [])
-                    Declaration.authorizeOmittedCandidate candidate (pure ())
+                    Declaration.authorizeOmittedCandidate candidate
+                        Declaration.recordOmittedUse
             pure ()
     case driver of
         Right (Declaration.DriverSucceeded _value _interface prefix _closure) ->