Check exact declarations in typed modules

1 files changed, 399 insertions, 1 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index bc634ac..9d36641 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -4,6 +4,7 @@ module Test.Unit.Module (unitTests) where
 
 import Base
 import Api qualified
+import Checking.Authority qualified as Authority
 import Checking.Core qualified as Core
 import Checking.Declaration qualified as Declaration
 import Checking.Foundation qualified as Foundation
@@ -26,11 +27,14 @@ import Syntax.Interface qualified as Syntax
 
 import Bound.Scope (fromScope)
 import Bound.Var (Var(..))
+import Control.Monad (foldM)
 import Data.ByteString qualified as ByteString
 import Data.Text qualified as StrictText
 import Data.Text.Encoding qualified as Text
 import Control.Monad.Logger (runNoLoggingT)
-import System.Directory (getCurrentDirectory)
+import Data.IORef (modifyIORef', newIORef, readIORef)
+import Data.Map.Strict qualified as Map
+import System.Directory (createDirectoryIfMissing, getCurrentDirectory)
 import System.FilePath.Posix qualified as Posix
 import System.IO.Temp qualified as Temp
 import Test.Tasty
@@ -52,6 +56,14 @@ unitTests =
             resetsGlossStatePerModule
         , testCase "makes selected unsupported syntax terminal"
             rejectsUnsupportedTypedSource
+        , testCase "compiles exact declarations across an import"
+            compilesExactDeclarationGraph
+        , testCase "keeps exact semantics independent of fixity"
+            keepsExactSemanticsIndependentOfFixity
+        , testCase "loads a cached exact producer for a fresh importer"
+            loadsCachedExactProducerForFreshImporter
+        , testCase "retains the exact prefix before a later failure"
+            retainsExactPrefixBeforeFailure
         , testCase "routes production verification by complete graph"
             routesProductionVerification
         , testCase "installs nonempty implicit prelude evidence"
@@ -346,6 +358,241 @@ rejectsUnsupportedTypedSource = do
         Right{} ->
             assertFailure "unsupported typed source was admitted"
 
+compilesExactDeclarationGraph :: Assertion
+compilesExactDeclarationGraph = do
+    (_foundation, _bootstrap, workspace, sealedModules) <-
+        compileExactFixture "test/phase5/exact-importer.tex"
+    assertEqual "dependency-closed module count" 2 (length sealedModules)
+    assertEqual "imported-before-importer source order"
+        [ "test/phase5/exact-producer.tex"
+        , "test/phase5/exact-importer.tex"
+        ]
+        [ safeRelativePathFilePath
+            (resolvedSourceRelativePath
+                (Parse.parsedModuleResolved parsed))
+        | parsed <- toList
+            (Parse.parsedWorkspaceImportedBeforeImporter workspace)
+        ]
+    case sealedModules of
+        [producer, importer] -> do
+            let producerPrefix = Module.sealedTypedModulePrefix producer
+                importerPrefix = Module.sealedTypedModulePrefix importer
+                producerBatches =
+                    Declaration.pendingModulePrefixBatches producerPrefix
+                importerBatches =
+                    Declaration.pendingModulePrefixBatches importerPrefix
+            assertEqual "producer declaration batches" 3
+                (length producerBatches)
+            assertEqual "importer declaration batches" 1
+                (length importerBatches)
+            assertEqual "producer declaration order"
+                [0, 1, 2]
+                [ localDeclarationOrdinalValue
+                    (Semantic.declarationSlotOrdinal
+                        (Declaration.committedBatchSlot batch))
+                | batch <- producerBatches
+                ]
+
+            let producerDeltas =
+                    Semantic.semanticInterfaceDeclarations
+                        (Module.sealedTypedModuleSemantic producer)
+                importerDeltas =
+                    Semantic.semanticInterfaceDeclarations
+                        (Module.sealedTypedModuleSemantic importer)
+            assertEqual "one exact binding per producer declaration"
+                [1, 1, 1]
+                (bindingCount <$> producerDeltas)
+            assertEqual "one exact importer binding"
+                [1]
+                (bindingCount <$> importerDeltas)
+            assertEqual "producer object families"
+                ["opaque", "transparent", "transparent"]
+                [ objectFamilyName
+                    (Identity.assertedObjectContent object)
+                | batch <- producerBatches
+                , object <- Declaration.committedBatchObjects batch
+                ]
+
+            definitionDelta <- sole "producer definition delta"
+                (drop 2 producerDeltas)
+            definitionBinding <- sole "producer definition binding"
+                (bindings definitionDelta)
+            definitionFact <- sole "producer definition fact"
+                (Semantic.declarationDeltaFacts definitionDelta)
+            definitionAlias <- sole "producer definition alias"
+                (Semantic.declarationDeltaAliases definitionDelta)
+            assertEqual "definition alias"
+                (Semantic.semanticName "phase5_definition")
+                (Semantic.semanticAliasName definitionAlias)
+            assertEqual "definition is proof-search eligible"
+                Semantic.SearchEligible
+                (Semantic.semanticFactSearchEligibility definitionFact)
+            assertEqual "definition authority is clean"
+                Authority.cleanAuthoritySafety
+                (Authority.factAuthoritySafety
+                    (Semantic.semanticFactAuthority definitionFact))
+            definitionBatch <- sole "producer definition batch"
+                (drop 2 producerBatches)
+            validation <-
+                maybe
+                    (assertFailure "definition declaration validation is absent"
+                        >> fail "unreachable")
+                    pure
+                    (Declaration.committedBatchDeclarationValidation
+                        definitionBatch)
+            certificate <- sole "definition validation certificate"
+                (Semantic.declarationValidationRecordCertificates validation)
+            assertEqual "direct defining-equation authority"
+                (Authority.CheckedKernelConstruction
+                    (Authority.CheckedDefinitionEquation
+                        (Semantic.semanticGlobalBindingTarget
+                            definitionBinding)))
+                (Authority.validationDirectAuthorization
+                    certificate)
+
+            aliasDelta <- sole "producer abbreviation delta"
+                (take 1 (drop 1 producerDeltas))
+            aliasBinding <- sole "producer abbreviation binding"
+                (bindings aliasDelta)
+            definitionObject <- sole "producer definition object"
+                (Declaration.committedBatchObjects definitionBatch)
+            case Identity.assertedObjectContent definitionObject of
+                Identity.TransparentObjectContent _theory _coreType body ->
+                    assertBool "definition resolves the producer alias"
+                        (Semantic.semanticGlobalBindingTarget aliasBinding
+                            `elem` canonicalGlobals body)
+                content ->
+                    assertFailure
+                        ("definition object is not transparent: "
+                            <> show content)
+            importerBatch <- sole "importer declaration batch" importerBatches
+            importerDelta <- sole "importer semantic delta" importerDeltas
+            importerBinding <- sole "importer binding"
+                (bindings importerDelta)
+            assertEqual "equal transparent content reuses the producer object"
+                (Semantic.semanticGlobalBindingTarget definitionBinding)
+                (Semantic.semanticGlobalBindingTarget importerBinding)
+            assertEqual "reused transparent content adds no object"
+                []
+                (Declaration.committedBatchObjects importerBatch)
+        modules ->
+            assertFailure
+                ("unexpected exact module count: " <> show (length modules))
+  where
+    bindingCount = length . bindings
+
+    bindings =
+        Semantic.semanticEnvironmentBindings
+            . Semantic.declarationDeltaEnvironment
+
+    objectFamilyName :: Identity.ObjectContent -> String
+    objectFamilyName = \case
+        Identity.OpaqueObjectContent{} -> "opaque"
+        Identity.TransparentObjectContent{} -> "transparent"
+        Identity.IntrinsicObjectContent{} -> "intrinsic"
+
+keepsExactSemanticsIndependentOfFixity :: Assertion
+keepsExactSemanticsIndependentOfFixity =
+    Temp.withSystemTempDirectory "felix-exact-fixity" \root -> do
+        let relative = "test/phase5/exact-producer.tex"
+            path = root Posix.</> relative
+        createDirectoryIfMissing True (Posix.takeDirectory path)
+        original <- ByteString.readFile relative
+        let changed =
+                Text.encodeUtf8
+                    (StrictText.replace
+                        "infixl 2"
+                        "infixr 6"
+                        (Text.decodeUtf8 original))
+        ByteString.writeFile path original
+        first <- compileExactRootAt root relative
+        ByteString.writeFile path changed
+        second <- compileExactRootAt root relative
+        let firstParsed = Parse.parsedWorkspaceRootModule (fst first)
+            secondParsed = Parse.parsedWorkspaceRootModule (fst second)
+            firstSealed = snd first
+            secondSealed = snd second
+        assertBool "fixity changes syntax identity"
+            (Syntax.moduleSyntaxAssertedId
+                (Parse.parsedModuleSyntaxInterface firstParsed)
+                /= Syntax.moduleSyntaxAssertedId
+                    (Parse.parsedModuleSyntaxInterface secondParsed))
+        assertBool "fixity changes parsed identity"
+            (Parse.parsedModuleId firstParsed
+                /= Parse.parsedModuleId secondParsed)
+        assertEqual "fixity preserves semantic interface"
+            (Module.sealedTypedModuleSemantic firstSealed)
+            (Module.sealedTypedModuleSemantic secondSealed)
+        assertEqual "fixity preserves semantic prefix"
+            (Declaration.pendingModulePrefixCurrent
+                (Module.sealedTypedModulePrefix firstSealed))
+            (Declaration.pendingModulePrefixCurrent
+                (Module.sealedTypedModulePrefix secondSealed))
+
+loadsCachedExactProducerForFreshImporter :: Assertion
+loadsCachedExactProducerForFreshImporter = do
+    foundation <- expectRight Foundation.checkedFoundation
+    Temp.withSystemTempDirectory "felix-exact-cache" \root -> do
+        let path = root Posix.</> "store.sqlite"
+        (_startup, store) <-
+            Store.openStore path (Identity.theoryId foundation)
+                >>= expectRight
+        observed <- newIORef (0 :: Int)
+        let observer = Api.verificationRequestObserver \_ordinal _request ->
+                modifyIORef' observed (+ 1)
+            prover =
+                Provers.vampire
+                    "phase5-fixture-must-not-run-vampire"
+                    Provers.defaultTimeLimit
+                    Provers.defaultMemoryLimit
+            verify mode source =
+                runNoLoggingT
+                    (Api.verifyWithObserverAndStoreMode
+                        store mode observer prover source)
+                    >>= expectRight
+        producer <-
+            verify Api.FreshStoreValidation
+                "test/phase5/exact-producer.tex"
+        importer <-
+            verify Api.WarmStoreValidation
+                "test/phase5/exact-importer.tex"
+        assertTypedSuccess "fresh producer" producer
+        assertTypedSuccess "warm producer/fresh importer" importer
+        assertEqual "exact declarations issue no Vampire requests"
+            0
+            =<< readIORef observed
+        Store.closeStore store
+
+retainsExactPrefixBeforeFailure :: Assertion
+retainsExactPrefixBeforeFailure = do
+    result <-
+        runNoLoggingT
+            (Api.verifyMeasured
+                (Provers.vampire
+                    "phase5-fixture-must-not-run-vampire"
+                    Provers.defaultTimeLimit
+                    Provers.defaultMemoryLimit)
+                "test/phase5/exact-failure.tex")
+    case result of
+        Left
+            (Api.VerificationTypedModuleError
+                source
+                (Module.TypedActionFailed
+                    (Module.TypedUnsupportedBlock location))
+                prefix) -> do
+            assertEqual "failed exact source"
+                "test/phase5/exact-failure.tex"
+                (safeRelativePathFilePath
+                    (resolvedSourceRelativePath source))
+            assertEqual "unsupported declaration line" 5 (locLine location)
+            assertEqual "earlier exact declaration remains committed"
+                1
+                (length (Declaration.pendingModulePrefixBatches prefix))
+        Left err ->
+            assertFailure ("unexpected exact failure: " <> show err)
+        Right{} ->
+            assertFailure "unsupported declaration was admitted"
+
 routesProductionVerification :: Assertion
 routesProductionVerification = do
     producer <- verifyFixture "test/phase3/typed-producer.tex"
@@ -551,6 +798,157 @@ unusedResolver =
     Declaration.vampireResolver \_prepared ->
         fail "empty bootstrap invoked Vampire"
 
+compileExactFixture
+    :: FilePath
+    -> IO
+        ( Foundation.CheckedFoundation
+        , Module.MigrationPreludeSession
+        , Parse.ParsedSourceWorkspace
+        , [Module.SealedTypedModule]
+        )
+compileExactFixture relative = do
+    root <- getCurrentDirectory
+    foundation <- expectRight Foundation.checkedFoundation
+    bootstrap <-
+        expectRight
+            =<< Module.buildBootstrapPreludeSession
+                foundation
+                unusedResolver
+    mounts <- exactFixtureMounts root
+    workspace <- parseExactWorkspace bootstrap mounts relative
+    sealed <- compileParsedWorkspace foundation bootstrap workspace
+    pure (foundation, bootstrap, workspace, sealed)
+
+compileExactRootAt
+    :: FilePath
+    -> FilePath
+    -> IO (Parse.ParsedSourceWorkspace, Module.SealedTypedModule)
+compileExactRootAt projectRoot relative = do
+    foundation <- expectRight Foundation.checkedFoundation
+    bootstrap <-
+        expectRight
+            =<< Module.buildBootstrapPreludeSession
+                foundation
+                unusedResolver
+    mounts <- exactFixtureMounts projectRoot
+    workspace <- parseExactWorkspace bootstrap mounts relative
+    sealed <- compileParsedWorkspace foundation bootstrap workspace
+    rootModule <- sole "exact root module" (reverse sealed)
+    pure (workspace, rootModule)
+
+exactFixtureMounts :: FilePath -> IO SourceMounts
+exactFixtureMounts projectRoot = do
+    repository <- getCurrentDirectory
+    expectRight
+        =<< prepareSourceMounts
+            [ (sourceMountId "project", projectRoot)
+            , (sourceMountId "library", repository Posix.</> "library")
+            , (sourceMountId "debug", repository Posix.</> "debug")
+            ]
+
+parseExactWorkspace
+    :: Module.MigrationPreludeSession
+    -> SourceMounts
+    -> FilePath
+    -> IO Parse.ParsedSourceWorkspace
+parseExactWorkspace bootstrap mounts relative = do
+    request <- expectRight (searchedRoot relative)
+    let preludeSyntax =
+            Module.sealedTypedModuleSyntax
+                (Module.migrationPreludeModule bootstrap)
+    fst
+        <$> (expectRight
+            =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs
+                mounts
+                request
+                (const [preludeSyntax]))
+
+compileParsedWorkspace
+    :: Foundation.CheckedFoundation
+    -> Module.MigrationPreludeSession
+    -> Parse.ParsedSourceWorkspace
+    -> IO [Module.SealedTypedModule]
+compileParsedWorkspace foundation bootstrap workspace =
+    snd
+        <$> foldM
+            compileOne
+            (Map.empty, [])
+            (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace))
+  where
+    compileOne (admitted, ordered) parsed = do
+        direct <-
+            traverse
+                (\address ->
+                    maybe
+                        (assertFailure
+                            ("missing exact direct module: " <> show address)
+                            >> fail "unreachable")
+                        pure
+                        (Map.lookup address admitted))
+                (nubOrd
+                    (Parse.parsedImportedAddress
+                        <$> Parse.parsedModuleImports parsed))
+        input <-
+            expectRight
+                (Module.typedModuleInput
+                    foundation
+                    (Module.bootstrapWalkingReadiness bootstrap)
+                    unusedResolver
+                    Declaration.FreshValidation
+                    parsed
+                    direct)
+        sealed <-
+            Module.runTypedModule input >>= \case
+                Module.TypedModuleSucceeded module' -> pure module'
+                Module.TypedModuleOpenFailed failure ->
+                    assertFailure
+                        ("exact module did not open: " <> show failure)
+                        >> fail "unreachable"
+                Module.TypedModuleFailed failure _prefix ->
+                    assertFailure
+                        ("exact module did not seal: " <> show failure)
+                        >> fail "unreachable"
+        pure
+            ( Map.insert (Parse.parsedModuleAddress parsed) sealed admitted
+            , ordered <> [sealed]
+            )
+
+canonicalGlobals :: Core.CanonicalTerm Identity.ObjectId -> [Identity.ObjectId]
+canonicalGlobals = \case
+    Core.CBound{} -> []
+    Core.CGlobal identity -> [identity]
+    Core.CIntrinsic{} -> []
+    Core.COpaqueInteger{} -> []
+    Core.CApp function argument ->
+        canonicalGlobals function <> canonicalGlobals argument
+    Core.CLam _type body -> canonicalGlobals body
+    Core.CFalsum -> []
+    Core.CImp premise conclusion ->
+        canonicalGlobals premise <> canonicalGlobals conclusion
+    Core.CEq _type left right ->
+        canonicalGlobals left <> canonicalGlobals right
+    Core.CForall _type body -> canonicalGlobals body
+
+assertTypedSuccess :: String -> Api.VerificationResult -> Assertion
+assertTypedSuccess label = \case
+    Api.VerifiedWithTrustedVampire report ->
+        assertEqual label Api.TypedVerificationRoute
+            (Api.verificationRoute report)
+    Api.CompletedWithExplicitGaps report ->
+        assertFailure
+            (label <> " completed with gaps via "
+                <> show (Api.verificationRoute report))
+    Api.VerificationFailure failure ->
+        assertFailure (label <> " failed: " <> show failure)
+
+sole :: String -> [value] -> IO value
+sole label = \case
+    [value] -> pure value
+    values ->
+        assertFailure
+            (label <> ": expected one value, found " <> show (length values))
+            >> fail "unreachable"
+
 expectRight :: Show error => Either error value -> IO value
 expectRight = \case
     Left err -> assertFailure (show err) >> fail "unreachable"