diff options
Diffstat (limited to 'source/Test/Unit/Declaration.hs')
| -rw-r--r-- | source/Test/Unit/Declaration.hs | 2978 |
1 files changed, 0 insertions, 2978 deletions
diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs deleted file mode 100644 index 26261f3..0000000 --- a/source/Test/Unit/Declaration.hs +++ /dev/null @@ -1,2978 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - -module Test.Unit.Declaration (unitTests) where - -import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Core qualified as Core -import Checking.Declaration qualified as Declaration -import Checking.Foundation qualified as Foundation -import Checking.Exact qualified as Exact -import Checking.Identity qualified as Identity -import Checking.Kernel.Derivation qualified as Kernel -import Checking.Semantic qualified as Semantic -import Felix.Math.Codec -import Felix.Module -import Felix.Source -import Felix.Store qualified as Store -import Provers qualified -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface qualified as Syntax -import Syntax.Lexicon qualified as Lexicon - -import Data.List.NonEmpty qualified as NonEmpty -import Data.IORef qualified as IORef -import Data.Text qualified as Text -import Data.Text.Encoding qualified as TextEncoding -import Data.Vector qualified as Vector -import Numeric.Natural (Natural) -import Control.Exception (bracket) -import Control.Exception qualified as Exception -import Control.Monad.Logger (runNoLoggingT) -import System.Directory qualified as Directory -import System.FilePath.Posix qualified as Posix -import Test.Tasty -import Test.Tasty.HUnit - - -unitTests :: TestTree -unitTests = - testGroup "Typed declaration seam" - [ testCase "enforces staged candidate order" - enforcesStagedCandidateOrder - , testCase "retains only appended declaration prefixes" - retainsOnlyAppendedPrefixes - , testCase "makes declaration failures terminal" - makesDeclarationFailuresTerminal - , testCase "propagates unsafe authority through local claims" - propagatesUnsafeAuthorityThroughLocalClaims - , testCase "aggregates exact Vampire obligations" - aggregatesExactVampireObligations - , testCase "validates complete resolver batches before rejection" - validatesCompleteResolverBatchesBeforeRejection - , testCase "rejects retained-plan admission drift fatally" - rejectsRetainedPlanAdmissionDrift - , testCase "preserves source-axiom safety through Vampire validation" - preservesSourceAxiomSafetyThroughVampireValidation - , testCase "materializes a sealed import with fresh authority" - materializesSealedImport - , testCase "reconstructs exact imported global bindings" - reconstructsImportedGlobalBindings - , testCase "elaborates scoped exact propositions" - elaboratesScopedExactPropositions - , testCase "prepares exact claim envelopes" - preparesExactClaimEnvelopes - , testCase "lowers exact separation comprehensions" - lowersExactSeparationComprehensions - , testCase "lowers exact replacement telescopes" - lowersExactReplacementTelescopes - , testCase "lowers exact finite sets" - lowersExactFiniteSets - , testCase "lowers exact ordinary declarations" - lowersExactOrdinaryDeclarations - , testCase "folds transitive and diamond import evidence" - foldsTransitiveAndDiamondEvidence - , testCase "validates exact kernel construction descriptors" - validatesExactKernelConstructionDescriptors - , testCase "authorizes exact datatype compilation families" - authorizesExactDatatypeCompilationFamilies - , testCase "reuses exact compiled declaration validation" - reusesExactCompiledDeclarationValidation - , testCase "keeps fatal validation lookup failures out of declarations" - keepsFatalValidationLookupFailuresOutOfDeclarations - ] - -data FatalValidationLookup = FatalValidationLookup - deriving (Show) - -instance Exception.Exception FatalValidationLookup - -keepsFatalValidationLookupFailuresOutOfDeclarations :: Assertion -keepsFatalValidationLookupFailuresOutOfDeclarations = do - fixture <- makeFixture - prepared <- makePreparedObligation - fixture - Foundation.EmptyCharacteristic - let lookup = proofOnlyValidationLookup - (const (Exception.throwIO FatalValidationLookup)) - action = Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "fatal-validation-lookup") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "fatal-validation-lookup") - Declaration.authorizeVampireCandidate candidate - (Declaration.acceptVampireObligation prepared) - result <- Exception.try - (runDriverWithValidation fixture lookup action) - :: IO - (Either - FatalValidationLookup - (Declaration.DriverResult - Void - ((), Declaration.CommittedDeclarationBatch))) - case result of - Left FatalValidationLookup -> pure () - Right _ -> - assertFailure "fatal validation lookup became a driver result" - -enforcesStagedCandidateOrder :: Assertion -enforcesStagedCandidateOrder = do - fixture <- makeFixture - accepted <- runSuccessful fixture do - result <- Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "staged-success") do - first <- Declaration.reserveCandidate - (factSpec fixture "first") - later <- Declaration.reserveCandidateBatch - ( factSpec fixture "later-a" - :| [factSpec fixture "later-b"] - ) - Declaration.authorizeCompiledDeclaration do - Declaration.authorizeSourceAxiomCandidate first - traverse_ - (\candidate -> - Declaration.authorizeKernelProofCandidate - candidate do - premise <- - Declaration.useStagedCandidate first - pure - (Kernel.importedFactDerivation premise)) - later - pure result - let (_value, batch) = accepted - assertEqual - "all source-ordered candidates appended" - 3 - (length - (Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta batch))) - - provenance <- runDriver fixture (priorDeclarationUse fixture) - case provenance of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - (Declaration.CandidateOutsideDeclaration slot)) - prefix -> do - assertEqual - "cross-declaration staged premise" - (localFact fixture 0) - slot - assertSingleCompletedPrefix prefix - _other -> - assertFailure - "cross-declaration staged provenance was not rejected" - - traverse_ - (\(label, action, expectedPremise, expectedCandidate) -> do - result <- runDriver fixture action - case result of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - (Declaration.StagedPremiseNotEarlier - premiseSlot premiseStage - candidateSlot candidateStage)) - _prefix -> do - assertEqual (label <> " premise slot") - expectedPremise premiseSlot - assertEqual (label <> " candidate slot") - expectedCandidate candidateSlot - assertBool (label <> " rejected non-earlier stage") - (premiseStage >= candidateStage) - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed other) - _prefix -> - assertFailure - (label <> ": unexpected error " <> show other) - Declaration.DriverFailed - (Declaration.DriverActionFailed _failure) - _prefix -> - assertFailure - (label <> ": unexpected ordinary driver failure") - Declaration.DriverSucceeded{} -> - assertFailure (label <> ": invalid staged use succeeded") - Declaration.DriverSealFailed{} -> - assertFailure (label <> ": invalid staged use reached sealing")) - [ ( "self" - , selfUse fixture - , localFact fixture 0 - , localFact fixture 0 - ) - , ( "same stage" - , sameStageUse fixture - , localFact fixture 1 - , localFact fixture 0 - ) - , ( "forward" - , forwardUse fixture - , localFact fixture 1 - , localFact fixture 0 - ) - ] - where - localFact fixture ordinal = - Semantic.factSlot - (fixtureOwner fixture) - (localFactOrdinal ordinal) - - selfUse fixture = - Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "self") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "self") - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeKernelProofCandidate candidate do - premise <- Declaration.useStagedCandidate candidate - pure (Kernel.importedFactDerivation premise)) - - sameStageUse fixture = - Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "same-stage") do - candidates <- Declaration.reserveCandidateBatch - ( factSpec fixture "same-a" - :| [factSpec fixture "same-b"] - ) - let first = NonEmpty.head candidates - second = NonEmpty.last candidates - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeKernelProofCandidate first do - premise <- Declaration.useStagedCandidate second - pure (Kernel.importedFactDerivation premise)) - - forwardUse fixture = - Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "forward") do - first <- Declaration.reserveCandidate - (factSpec fixture "forward-a") - second <- Declaration.reserveCandidate - (factSpec fixture "forward-b") - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeKernelProofCandidate first do - premise <- Declaration.useStagedCandidate second - pure (Kernel.importedFactDerivation premise)) - - priorDeclarationUse fixture = do - (premise, _batch) <- Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "prior-stage") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "prior-stage") - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeSourceAxiomCandidate candidate) - pure candidate - void - (Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "later-stage") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "later-stage") - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeKernelProofCandidate candidate do - imported <- - Declaration.useStagedCandidate premise - pure (Kernel.importedFactDerivation imported))) - -retainsOnlyAppendedPrefixes :: Assertion -retainsOnlyAppendedPrefixes = do - fixture <- makeFixture - outcome <- runDriver fixture do - (_value, _firstBatch) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "accepted") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "accepted") - Declaration.authorizeSourceAxiomCandidate candidate - Declaration.failModuleDriver - ("later checker failure" :: Text) - case outcome of - Declaration.DriverFailed - (Declaration.DriverActionFailed reason) prefix -> do - assertEqual - "driver reports the later ordinary failure" - "later checker failure" - reason - assertSingleCompletedPrefix prefix - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed err) _prefix -> - assertFailure - ("unexpected declaration failure: " <> show err) - Declaration.DriverSucceeded{} -> - assertFailure "ordinary driver failure was lost" - Declaration.DriverSealFailed{} -> - assertFailure "ordinary driver failure became a seal failure" - -makesDeclarationFailuresTerminal :: Assertion -makesDeclarationFailuresTerminal = do - fixture <- makeFixture - outcome <- runDriver fixture do - void - (Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "accepted-before-failure") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "accepted-before-failure") - Declaration.authorizeSourceAxiomCandidate candidate) - void - (Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "rolled-back") do - void - (Declaration.reserveCandidate - (factSpec fixture "uncommitted"))) - -- This declaration must be unreachable after the terminal failure. - void - (Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "must-not-publish") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "must-not-publish") - Declaration.authorizeSourceAxiomCandidate candidate) - case outcome of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - Declaration.DeclarationHasUnauthorizedCandidates) - prefix -> - assertSingleCompletedPrefix prefix - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed other) _prefix -> - assertFailure - ("unexpected declaration failure: " <> show other) - Declaration.DriverFailed - (Declaration.DriverActionFailed _failure) _prefix -> - assertFailure "unexpected ordinary driver failure" - Declaration.DriverSucceeded{} -> - assertFailure "failed declaration was skipped" - Declaration.DriverSealFailed{} -> - assertFailure "failed declaration reached sealing" - -assertSingleCompletedPrefix - :: Declaration.PendingModulePrefix - -> Assertion -assertSingleCompletedPrefix prefix = do - let batches = - Declaration.pendingModulePrefixBatches prefix - assertEqual "one completed envelope survives" 1 (length batches) - case batches of - [batch] -> do - let expected = - Declaration.committedBatchNextPrefix batch - assertEqual - "failed declaration did not advance the prefix" - expected - (Declaration.pendingModulePrefixCurrent prefix) - assertEqual - "retained envelope ends at the exposed prefix" - expected - (Declaration.committedBatchNextPrefix batch) - _ -> pure () - -propagatesUnsafeAuthorityThroughLocalClaims :: Assertion -propagatesUnsafeAuthorityThroughLocalClaims = do - fixture <- makeFixture - result <- runSuccessful fixture do - (_sourceValue, sourceBatch) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "source-axiom") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "source") - Declaration.authorizeSourceAxiomCandidate candidate - sourceOccurrence <- requireSingleOccurrence sourceBatch - let - sourceFingerprint = - Semantic.semanticFactFingerprint sourceOccurrence - (_derivedValue, derivedBatch) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "local-claim") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "derived") - Declaration.authorizeKernelProofCandidate candidate do - sourcePremise <- - Declaration.useAuthorizedFact sourceFingerprint - claim <- Declaration.proveLocalKernelClaim - (fixtureProposition fixture) - (Kernel.importedFactDerivation sourcePremise) - claimPremise <- Declaration.useLocalClaim claim - pure (Kernel.importedFactDerivation claimPremise) - pure derivedBatch - occurrence <- - case Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta result) of - [single] -> pure single - facts -> - assertFailure - ("unexpected fact count: " <> show (length facts)) - >> fail "unreachable" - let authority = Semantic.semanticFactAuthority occurrence - assertEqual - "local claim cannot erase source-axiom safety" - (Authority.authoritySafety - (Authority.singletonEscapeKind Authority.SourceAxiom)) - (Authority.factAuthoritySafety authority) - case Declaration.committedBatchProofValidations result of - [record] -> - assertEqual - "local support is absent from the compact direct authorization" - (Authority.CheckedSourceProof []) - (Authority.validationDirectAuthorization - (Semantic.proofValidationRecordCertificate record)) - records -> - assertFailure - ("unexpected proof validation count: " - <> show (length records)) - -aggregatesExactVampireObligations :: Assertion -aggregatesExactVampireObligations = - withTemporaryDirectory "felix-declaration-vampire" \root -> do - fixture <- makeFixture - let executable = root Posix.</> "vampire" - writeAcceptedVampire executable - first <- makePreparedObligation - fixture - Foundation.EmptyCharacteristic - second <- makePreparedObligation - fixture - Foundation.PairSetCharacteristic - let exactResolver = acceptedResolver executable - freshOutcome <- - (runDriverWithResolver fixture exactResolver do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "two-vampire-obligations") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "two-vampire-obligations") - Declaration.authorizeVampireCandidate candidate do - Declaration.acceptVampireObligation first - Declaration.acceptVampireObligation second - pure committed - :: IO - (Declaration.DriverResult Text - Declaration.CommittedDeclarationBatch)) - (batch, freshPrefix) <- - case freshOutcome of - Declaration.DriverSucceeded value _ prefix _closure -> - pure (value, prefix) - Declaration.DriverFailed failure _ -> - assertFailure - ("fresh Vampire fixture failed: " <> show failure) - >> fail "unreachable" - Declaration.DriverSealFailed failure _ -> - assertFailure - ("fresh Vampire fixture did not seal: " - <> show failure) - >> fail "unreachable" - let expectedRequests = - Provers.preparedVerificationRequestId - (Provers.preparedTypedProverRequest first) - : [Provers.preparedVerificationRequestId - (Provers.preparedTypedProverRequest second)] - case Declaration.committedBatchProofValidations batch of - [record] -> - assertEqual - "accepted requests retain source order" - (Authority.CheckedSourceProof expectedRequests) - (Authority.validationDirectAuthorization - (Semantic.proofValidationRecordCertificate record)) - records -> - assertFailure - ("unexpected proof validation count: " - <> show (length records)) - - cachedRecord <- - case Declaration.committedBatchProofValidations batch of - [record] -> pure record - records -> - assertFailure - ("unexpected cached proof records: " - <> show (length records)) - >> fail "unreachable" - cachedLookupKey <- IORef.newIORef Nothing - cached <- runSuccessfulWithValidation fixture - (proofOnlyValidationLookup - (\key -> do - IORef.writeIORef cachedLookupKey (Just key) - pure (Just cachedRecord))) do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "two-vampire-obligations") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "two-vampire-obligations") - Declaration.authorizeVampireCandidate candidate do - Declaration.acceptVampireObligation first - Declaration.acceptVampireObligation second - pure committed - publishedRecord <- - case Declaration.committedBatchProofValidations cached of - [record] -> pure record - records -> - assertFailure - ("unexpected cached validation records: " - <> show (length records)) - >> fail "unreachable" - assertEqual - "cached authorization preserves the exact direct proof" - (Authority.CheckedSourceProof expectedRequests) - (Authority.validationDirectAuthorization - (Semantic.proofValidationRecordCertificate publishedRecord)) - assertEqual - "lookup and publication retain the same validation key" - (Semantic.proofValidationRecordKey cachedRecord) - (Semantic.proofValidationRecordKey publishedRecord) - assertEqual - "one proof syntax key governs lookup and publication" - (Just - (Semantic.proofValidationRecordKey cachedRecord)) - =<< IORef.readIORef cachedLookupKey - - missLookups <- IORef.newIORef (0 :: Int) - missRuns <- IORef.newIORef (0 :: Int) - let missLookup = proofOnlyValidationLookup \_key -> do - IORef.modifyIORef' missLookups (+ 1) - pure Nothing - missResolver = Declaration.vampireResolver \prepared -> do - IORef.modifyIORef' missRuns (+ 1) - resolveAccepted executable prepared - miss <- runDriverWithValidationAndResolver - fixture - missLookup - missResolver - do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "two-vampire-obligations") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "two-vampire-obligations") - Declaration.authorizeVampireCandidate candidate do - Declaration.acceptVampireObligation first - Declaration.acceptVampireObligation second - pure committed - case miss of - Declaration.DriverSucceeded{} -> pure () - _ -> - assertFailure "warm miss failed" - assertEqual "warm miss performs one exact lookup" - 1 - =<< IORef.readIORef missLookups - assertEqual "warm miss runs every reached Vampire request" - 2 - =<< IORef.readIORef missRuns - - mismatchRuns <- IORef.newIORef (0 :: Int) - let editedSyntax = - Semantic.proofSyntaxId "edited-proof-syntax" - cachedCertificate = - Semantic.proofValidationRecordCertificate cachedRecord - corruptedKey = - Semantic.proofValidationKey - (Identity.theoremId - (Authority.factAuthorityTheorem - (Authority.validationTarget - cachedCertificate))) - editedSyntax - (Declaration.committedBatchPreviousPrefix batch) - corruptedRecord = - Semantic.proofValidationRecord - corruptedKey - cachedCertificate - mismatchResolver = Declaration.vampireResolver \prepared -> do - IORef.modifyIORef' mismatchRuns (+ 1) - resolveAccepted executable prepared - mismatchingLookup = proofOnlyValidationLookup - (const (pure (Just corruptedRecord))) - mismatching <- Exception.try - (runDriverWithValidationAndResolver - fixture - mismatchingLookup - mismatchResolver - do - Declaration.commitProofDeclaration editedSyntax do - candidate <- Declaration.reserveCandidate - (factSpec fixture "two-vampire-obligations") - Declaration.authorizeVampireCandidate candidate - (Declaration.acceptVampireObligation first)) - :: IO - (Either - Declaration.ValidationIntegrityError - (Declaration.DriverResult - Text - ((), Declaration.CommittedDeclarationBatch))) - case mismatching of - Left Declaration.CachedValidationIntegrityError{} -> - pure () - Right _ -> - assertFailure "mismatching hit did not abort as corruption" - assertEqual "mismatching hit does not fall back to Vampire" - 0 - =<< IORef.readIORef mismatchRuns - - withOpenedStore fixture root \store -> do - expectRightIO - (Store.writePendingModulePrefix store freshPrefix) - warmCalls <- IORef.newIORef (0 :: Int) - let storeLookup = proofOnlyValidationLookup \key -> do - IORef.modifyIORef' warmCalls (+ 1) - Store.loadProofValidation store key >>= expectRight - warm <- runSuccessfulWithValidation fixture - storeLookup - do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "two-vampire-obligations") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "two-vampire-obligations") - Declaration.authorizeVampireCandidate candidate do - Declaration.acceptVampireObligation first - Declaration.acceptVampireObligation second - pure committed - assertEqual "warm lookup executes once through the store" - 1 - =<< IORef.readIORef warmCalls - assertEqual "warm path retains cached request IDs" - (Authority.CheckedSourceProof expectedRequests) - (case Declaration.committedBatchProofValidations warm of - [record] -> - Authority.validationDirectAuthorization - (Semantic.proofValidationRecordCertificate record) - records -> - error - ("unexpected warm validation records: " - <> show (length records))) - - emptyProof <- runDriver fixture do - Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "empty-vampire-proof") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "empty-vampire-proof") - Declaration.authorizeVampireCandidate candidate - (pure ()) - case emptyProof of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - Declaration.VampireProofHasNoAcceptedObligations) - prefix -> - assertEqual - "empty Vampire proof publishes no declaration" - 0 - (length - (Declaration.pendingModulePrefixBatches prefix)) - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed other) _prefix -> - assertFailure - ("unexpected empty-proof failure: " <> show other) - Declaration.DriverFailed - (Declaration.DriverActionFailed _failure) _prefix -> - assertFailure "unexpected ordinary driver failure" - Declaration.DriverSucceeded{} -> - assertFailure "empty Vampire proof was authorized" - Declaration.DriverSealFailed{} -> - assertFailure "empty Vampire proof reached sealing" - - invalidClosure <- expectRight - (Identity.validateObjectClosure - (Identity.theoryId (fixtureFoundation fixture)) - []) - invalidTarget <- expectRight - (Identity.validatePropositionContent - invalidClosure - (Core.CImp Core.CFalsum Core.CFalsum)) - invalidCalls <- IORef.newIORef (0 :: Int) - let invalidResolver = - Declaration.vampireResolver \prepared -> do - IORef.modifyIORef' invalidCalls (+ 1) - resolveAccepted executable prepared - invalid <- runDriverWithResolver fixture invalidResolver do - Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "invalid-vampire-target") do - candidate <- Declaration.reserveCandidate - (Declaration.candidateSpec - invalidTarget - Semantic.SearchEligible - [Semantic.semanticName - "invalid-vampire-target"]) - Declaration.authorizeVampireCandidate candidate - (Declaration.acceptVampireObligation first) - assertEqual - "invalid prepared problem does not invoke Vampire" - 0 - =<< IORef.readIORef invalidCalls - case invalid of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - Declaration.VampireTargetMismatch) - prefix -> - assertEqual - "invalid prepared problem publishes no declaration" - 0 - (length - (Declaration.pendingModulePrefixBatches prefix)) - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed other) _prefix -> - assertFailure - ("unexpected prepared-problem failure: " <> show other) - Declaration.DriverFailed - (Declaration.DriverActionFailed _failure) _prefix -> - assertFailure "unexpected ordinary driver failure" - Declaration.DriverSucceeded{} -> - assertFailure "invalid prepared problem was authorized" - Declaration.DriverSealFailed{} -> - assertFailure "invalid prepared problem reached sealing" - - let mismatchedResolver = - Declaration.vampireResolver \_prepared -> - resolveAccepted executable second - mismatch <- runDriverWithResolver fixture mismatchedResolver do - Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "mismatched-vampire-request") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "mismatched-vampire-request") - Declaration.authorizeVampireCandidate candidate - (Declaration.acceptVampireObligation first) - case mismatch of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - Declaration.VampireRequestMismatch) - prefix -> - assertEqual - "mismatch publishes no declaration" - 0 - (length - (Declaration.pendingModulePrefixBatches prefix)) - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed other) _prefix -> - assertFailure - ("unexpected mismatch failure: " <> show other) - Declaration.DriverFailed - (Declaration.DriverActionFailed _failure) _prefix -> - assertFailure "unexpected ordinary driver failure" - Declaration.DriverSucceeded{} -> - assertFailure "mismatched request was authorized" - 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 - IORef.modifyIORef' calls (+ 1) - resolveAccepted executable prepared - omittedBatch <- runSuccessfulWithResolver fixture countingResolver do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "omitted-after-obligations") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "omitted-after-obligations") - Declaration.authorizeOmittedCandidate candidate do - Declaration.acceptVampireObligation first - Declaration.acceptVampireObligation second - Declaration.recordOmittedUse - pure committed - assertEqual - "omitted proof still checks preceding obligations" - 2 - =<< IORef.readIORef calls - case Declaration.committedBatchProofValidations omittedBatch of - [record] -> - assertEqual - "omitted direct authorization discards request IDs" - Authority.OmittedAuthorization - (Authority.validationDirectAuthorization - (Semantic.proofValidationRecordCertificate record)) - records -> - assertFailure - ("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" - -rejectsRetainedPlanAdmissionDrift :: Assertion -rejectsRetainedPlanAdmissionDrift = do - fixture <- makeFixture - let checked = - Declaration.checkedProofDeclaration - (Semantic.proofSyntaxId "planned-admission-drift") - [] - [] - [] - [] - [ Declaration.checkedCandidate - (factSpec fixture "planned-admission-drift") - Declaration.checkedSourceAxiomPlanning - :| [] - ] - () - action = do - planned <- - Declaration.runProspectiveLoweringDriver - (Declaration.planCheckedDeclaration checked) - >>= either Declaration.failDeclarationDriver pure - Declaration.admitPlannedCheckedDeclaration planned - (\() stages -> - case concatMap toList stages of - [candidate] -> - Declaration.authorizeOmittedCandidate candidate - Declaration.recordOmittedUse - _ -> error "planned drift fixture candidate shape") - outcome <- - Exception.try (runDriver fixture action) - :: IO - (Either - Declaration.PlanningIntegrityError - (Declaration.DriverResult - Void - Declaration.CommittedDeclarationBatch)) - case outcome of - Left (Declaration.PlanningIntegrityError diagnostic) -> - assertBool "fatal mismatch identifies prospective contract drift" - ("prospective contract" `Text.isInfixOf` diagnostic) - Right _ -> - assertFailure - "a changed admitted authority was accepted against its plan" - -preservesSourceAxiomSafetyThroughVampireValidation :: Assertion -preservesSourceAxiomSafetyThroughVampireValidation = - withTemporaryDirectory "felix-declaration-source-axiom" \root -> do - fixture <- makeFixture - let executable = root Posix.</> "vampire" - writeAcceptedVampire executable - prepared <- - makePreparedObligationWithPremise - fixture - (fixtureSourceAxiomFingerprint fixture) - freshCalls <- IORef.newIORef (0 :: Int) - let freshResolver = Declaration.vampireResolver \task -> do - IORef.modifyIORef' freshCalls (+ 1) - resolveAccepted executable task - freshOutcome <- - (runDriverWithResolver fixture freshResolver - (sourceAxiomThenVampire fixture prepared) - :: IO - (Declaration.DriverResult Text - Declaration.CommittedDeclarationBatch)) - assertEqual - "fresh source-axiom theorem invokes Vampire once" - 1 - =<< IORef.readIORef freshCalls - freshBatch <- - case freshOutcome of - Declaration.DriverSucceeded batch _ _ _closure -> - pure batch - Declaration.DriverFailed failure _ -> - assertFailure - ("fresh source-axiom driver failed: " - <> show failure) - >> fail "unreachable" - Declaration.DriverSealFailed failure _ -> - assertFailure - ("fresh source-axiom driver did not seal: " - <> show failure) - >> fail "unreachable" - let freshRecord = singleProofValidation freshBatch - assertEqual - "fresh theorem retains source-axiom safety" - sourceAxiomSafety - (Authority.factAuthoritySafety - (Authority.validationTarget - (Semantic.proofValidationRecordCertificate freshRecord))) - separationCalls <- IORef.newIORef (0 :: Int) - let separationResolver = Declaration.vampireResolver \task -> do - IORef.modifyIORef' separationCalls (+ 1) - resolveAccepted executable task - separated <- - (runDriverWithResolver fixture separationResolver do - void - (Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "source-axiom") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "source-axiom") - Declaration.authorizeSourceAxiomCandidate candidate) - Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "atp-does-not-import") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "atp-does-not-import") - Declaration.authorizeKernelProofCandidate candidate do - Declaration.acceptVampireObligation prepared - pure - (Kernel.importedFactDerivation - (Kernel.importIx 0)) - :: IO - (Declaration.DriverResult Text - ((), Declaration.CommittedDeclarationBatch))) - assertEqual "mixed proof executes its ATP obligation" - 1 - =<< IORef.readIORef separationCalls - case separated of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - (Declaration.KernelCompletionFailed - (Kernel.KernelReplayImportOutOfBounds index))) - prefix -> do - assertEqual "ATP premise is absent from kernel imports" - (Kernel.importIx 0) - index - assertEqual "failed mixed proof retains only its prefix" - 1 - (length - (Declaration.pendingModulePrefixBatches prefix)) - Declaration.DriverFailed failure _prefix -> - assertFailure - ("unexpected mixed-proof failure: " <> show failure) - Declaration.DriverSucceeded{} -> - assertFailure "ATP premise entered the kernel import inventory" - Declaration.DriverSealFailed{} -> - assertFailure "mixed proof unexpectedly reached sealing" - withOpenedStore fixture root \store -> do - freshPrefix <- - case freshOutcome of - Declaration.DriverSucceeded _ _ prefix _closure -> - pure prefix - Declaration.DriverFailed failure _ -> - assertFailure - ("fresh source-axiom driver failed: " - <> show failure) - >> fail "unreachable" - Declaration.DriverSealFailed failure _ -> - assertFailure - ("fresh source-axiom driver did not seal: " - <> show failure) - >> fail "unreachable" - expectRightIO - (Store.writePendingModulePrefix store freshPrefix) - warmCalls <- IORef.newIORef (0 :: Int) - let storeLookup = proofOnlyValidationLookup \key -> do - IORef.modifyIORef' warmCalls (+ 1) - Store.loadProofValidation store key >>= expectRight - warmBatch <- runSuccessfulWithValidation fixture - storeLookup - (sourceAxiomThenVampire fixture prepared) - assertEqual - "warm source-axiom theorem performs one store lookup" - 1 - =<< IORef.readIORef warmCalls - assertEqual - "warm theorem retains source-axiom safety" - sourceAxiomSafety - (Authority.factAuthoritySafety - (Authority.validationTarget - (Semantic.proofValidationRecordCertificate - (singleProofValidation warmBatch)))) - where - sourceAxiomSafety = - Authority.authoritySafety - (Authority.singletonEscapeKind Authority.SourceAxiom) - - singleProofValidation batch = - case Declaration.committedBatchProofValidations batch of - [record] -> record - records -> - error - ("unexpected proof validation count: " - <> show (length records)) - -sourceAxiomThenVampire - :: Fixture - -> Provers.PreparedTypedProverTask - Semantic.SemanticFactOccurrenceFingerprint - Void - () - Identity.ObjectId - -> Declaration.ModuleDriver failure - Declaration.CommittedDeclarationBatch -sourceAxiomThenVampire fixture prepared = do - void - (Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "source-axiom") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "source-axiom") - Declaration.authorizeSourceAxiomCandidate candidate) - (_value, batch) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "source-axiom-vampire") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "source-axiom-vampire") - Declaration.authorizeVampireCandidate candidate - (Declaration.acceptVampireObligation prepared) - pure batch - -fixtureSourceAxiomFingerprint - :: Fixture - -> Semantic.SemanticFactOccurrenceFingerprint -fixtureSourceAxiomFingerprint fixture = - Semantic.semanticFactOccurrenceFingerprint - (Semantic.factSlot - (fixtureOwner fixture) - (localFactOrdinal 0)) - (Authority.factAuthority - (Identity.theoremRef - (Identity.theoryId (fixtureFoundation fixture)) - (Identity.checkedPropositionId - (fixtureProposition fixture))) - (Authority.authoritySafety - (Authority.singletonEscapeKind Authority.SourceAxiom))) - -makePreparedObligationWithPremise - :: Fixture - -> Semantic.SemanticFactOccurrenceFingerprint - -> IO - (Provers.PreparedTypedProverTask - Semantic.SemanticFactOccurrenceFingerprint - Void - () - Identity.ObjectId) -makePreparedObligationWithPremise fixture fingerprint = do - claim <- expectRight - (Backend.supportedProposition - (Vector.empty :: Vector.Vector (Void, Core.CoreType)) - (Core.embedClosedCore - [] - (Identity.checkedPropositionTerm - (fixtureProposition fixture)))) - factProposition <- expectRight - (Backend.supportedProposition - (Vector.empty :: Vector.Vector (Void, Core.CoreType)) - (Core.embedClosedCore - [] - (Identity.checkedPropositionTerm - (fixtureProposition fixture)))) - capability <- expectRight - (Backend.classifySupportedProposition - (const Nothing) - factProposition) - problem <- expectRight - (Backend.planTypedProblem - (const Nothing) - (Vector.singleton - (Backend.typedBackendFact - fingerprint - factProposition - capability)) - claim - [] - [] - Backend.ExplicitGlobalPremises - Backend.FirstOrderLocals) - expectRight - (Provers.prepareTypedProverTask - Provers.DirectTask - problem) - -makePreparedObligation - :: Fixture - -> Foundation.FoundationAxiomTag - -> IO - (Provers.PreparedTypedProverTask - Semantic.SemanticFactOccurrenceFingerprint - Void - () - Identity.ObjectId) -makePreparedObligation fixture tag = do - claim <- expectRight - (Backend.supportedProposition - (Vector.empty :: Vector.Vector (Void, Core.CoreType)) - (Core.embedClosedCore - [] - (Identity.checkedPropositionTerm - (fixtureProposition fixture)))) - problem <- expectRight - (Backend.planTypedProblem - (const Nothing) - Vector.empty - claim - [] - [Backend.typedFoundationAuxiliaryInput - (fixtureFoundation fixture) - tag] - Backend.NoGlobalPremises - Backend.AllLocals) - expectRight - (Provers.prepareTypedProverTask - Provers.DirectTask - problem) - -acceptedResolver :: FilePath -> Declaration.VampireResolver -acceptedResolver executable = - Declaration.vampireResolver (resolveAccepted executable) - -resolveAccepted - :: FilePath - -> Provers.PreparedTypedProverTask - ref local origin global - -> IO - (Either - Provers.ProverProcessError - Provers.ProverAnswer) -resolveAccepted executable prepared = - runNoLoggingT - (Provers.runPreparedTypedProver - (Provers.vampire - executable - Provers.defaultTimeLimit - Provers.defaultMemoryLimit) - prepared) - -writeAcceptedVampire :: FilePath -> IO () -writeAcceptedVampire executable = do - writeFile executable - (unlines - [ "#!/bin/sh" - , "cat >/dev/null" - , "printf '%s\\n' '% SZS status Theorem for typed'" - ]) - permissions <- Directory.getPermissions executable - Directory.setPermissions executable - (Directory.setOwnerExecutable True permissions) - -validatesExactKernelConstructionDescriptors :: Assertion -validatesExactKernelConstructionDescriptors = do - fixture <- makeFixture - proposition <- foundationProposition - fixture - Foundation.EmptyCharacteristic - let declaredObject = opaqueFixtureObject fixture - run descriptor = - runDriver fixture - (Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId - "kernel-construction-descriptor") do - Declaration.addDeclarationObject declaredObject - candidate <- Declaration.reserveCandidate - (Declaration.candidateSpec - proposition - Semantic.SearchEligible - [Semantic.semanticName "kernel-construction"]) - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeKernelConstructionCandidate - descriptor - candidate - (pure - (Kernel.foundationFactDerivation - Foundation.EmptyCharacteristic)))) - success <- run - (Authority.FoundationLeaf - Foundation.EmptyCharacteristic) - case success of - Declaration.DriverSucceeded (_value, batch) _interface _prefix _closure -> do - assertEqual - "new object is included in the checked declaration batch" - 1 - (length (Declaration.committedBatchObjects batch)) - case Declaration.committedBatchDeclarationValidation batch of - Just record -> - case Semantic.declarationValidationRecordCertificates - record of - [certificate] -> - assertEqual - "exact kernel descriptor is retained" - (Authority.CheckedKernelConstruction - (Authority.FoundationLeaf - Foundation.EmptyCharacteristic)) - (Authority.validationDirectAuthorization - certificate) - certificates -> - assertFailure - ("unexpected kernel certificate count: " - <> show (length certificates)) - Nothing -> - assertFailure "missing declaration validation" - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed failure) _prefix -> - assertFailure - ("valid kernel descriptor failed: " <> show failure) - Declaration.DriverFailed - (Declaration.DriverActionFailed _failure) _prefix -> - assertFailure "unexpected ordinary driver failure" - Declaration.DriverSealFailed failure _prefix -> - assertFailure (show failure) - - traverse_ - (\(label, descriptor) -> do - outcome <- run descriptor - case outcome of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - Declaration.KernelConstructionDescriptorMismatch) - prefix -> - assertEqual - (label <> " publishes no declaration") - 0 - (length - (Declaration.pendingModulePrefixBatches prefix)) - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed other) - _prefix -> - assertFailure - (label <> ": unexpected error " <> show other) - Declaration.DriverFailed - (Declaration.DriverActionFailed _failure) - _prefix -> - assertFailure (label <> ": ordinary driver failure") - Declaration.DriverSucceeded{} -> - assertFailure (label <> ": mismatch was accepted") - Declaration.DriverSealFailed{} -> - assertFailure (label <> ": mismatch reached sealing")) - [ ( "wrong foundation leaf" - , Authority.FoundationLeaf - Foundation.PairSetCharacteristic - ) - , ( "wrong construction family" - , Authority.GuardedFoundationRules - (Authority.guardedRuleSet - (Foundation.SetLfpBound :| [])) - ) - ] - -authorizesExactDatatypeCompilationFamilies :: Assertion -authorizesExactDatatypeCompilationFamilies = do - fixture <- makeFixture - firstProposition <- foundationProposition - fixture - Foundation.EmptyCharacteristic - secondProposition <- foundationProposition - fixture - Foundation.PairSetCharacteristic - let carrier = datatypeFixtureObject fixture 0 - constructor = datatypeFixtureObject fixture 1 - carrierId = Identity.assertedObjectId carrier - constructorId = Identity.assertedObjectId constructor - references = - fmap - (Identity.theoremRef - (Identity.theoryId - (fixtureFoundation fixture)) - . Identity.checkedPropositionId) - [firstProposition, secondProposition] - descriptor = - Authority.datatypeCompilationDescriptor - carrierId - (constructorId :| []) - references - action - :: Authority.DatatypeCompilationDescriptor - -> Declaration.ModuleDriver Text - ((), Declaration.CommittedDeclarationBatch) - action suppliedDescriptor = - Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "datatype-compilation") do - traverse_ Declaration.addDeclarationObject - [carrier, constructor] - candidates <- - Declaration.reserveCandidateBatch - ( Declaration.candidateSpec - firstProposition - Semantic.SearchEligible - [Semantic.semanticName "datatype-first"] - :| [ Declaration.candidateSpec - secondProposition - Semantic.SearchEligible - [Semantic.semanticName "datatype-second"] - ] - ) - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeDatatypeCompilationCandidates - suppliedDescriptor - carrierId - (constructorId :| []) - candidates) - - (_value, batch) <- runSuccessful fixture (action descriptor) - assertEqual "complete object family was published" - [carrier, constructor] - (Declaration.committedBatchObjects batch) - case Declaration.committedBatchDeclarationValidation batch of - Just record -> do - let certificates = - Semantic.declarationValidationRecordCertificates record - assertEqual "complete fact family was authorized" 2 - (length certificates) - traverse_ - (\certificate -> do - assertEqual "datatype authority is clean" - Authority.cleanAuthoritySafety - (Authority.factAuthoritySafety - (Authority.validationTarget certificate)) - assertEqual "one descriptor protects every member" - (Authority.TrustedCompilation - (Authority.DatatypeCompilation descriptor)) - (Authority.validationDirectAuthorization certificate)) - certificates - Nothing -> - assertFailure "datatype compilation omitted validation" - - let mismatched = - Authority.datatypeCompilationDescriptor - carrierId - (constructorId :| []) - (reverse references) - rejected <- runDriver fixture (action mismatched) - case rejected of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - Declaration.DatatypeCompilationDescriptorMismatch) - prefix -> - assertEqual "mismatched family publishes no declaration" - 0 - (length - (Declaration.pendingModulePrefixBatches prefix)) - Declaration.DriverFailed failure _prefix -> - assertFailure - ("unexpected datatype-family failure: " <> show failure) - Declaration.DriverSucceeded{} -> - assertFailure "mismatched datatype family was authorized" - Declaration.DriverSealFailed failure _prefix -> - assertFailure - ("mismatched datatype family reached sealing: " - <> show failure) - -reusesExactCompiledDeclarationValidation :: Assertion -reusesExactCompiledDeclarationValidation = do - fixture <- makeFixture - proposition <- foundationProposition - fixture - Foundation.EmptyCharacteristic - let declaredObject = opaqueFixtureObject fixture - syntax = - Semantic.declarationSyntaxId - "cached-kernel-construction" - action derivationTag = - Declaration.commitCompiledDeclaration syntax do - Declaration.addDeclarationObject declaredObject - candidate <- Declaration.reserveCandidate - (Declaration.candidateSpec - proposition - Semantic.SearchEligible - [Semantic.semanticName - "cached-kernel-construction"]) - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeKernelConstructionCandidate - (Authority.FoundationLeaf - Foundation.EmptyCharacteristic) - candidate - (pure - (Kernel.foundationFactDerivation - derivationTag))) - freshBatch <- runSuccessful fixture - (snd <$> action Foundation.EmptyCharacteristic) - freshRecord <- - case Declaration.committedBatchDeclarationValidation freshBatch of - Just record -> pure record - Nothing -> - assertFailure "fresh compiled declaration omitted validation" - >> fail "unreachable" - - missLookups <- IORef.newIORef (0 :: Int) - missBatch <- runSuccessfulWithValidation fixture - (compiledOnlyValidationLookup \_key -> do - IORef.modifyIORef' missLookups (+ 1) - pure Nothing) - (snd <$> action Foundation.EmptyCharacteristic) - assertEqual "compiled warm miss performs one exact lookup" - 1 - =<< IORef.readIORef missLookups - assertBool "compiled miss publishes fresh validation" - (isJust - (Declaration.committedBatchDeclarationValidation missBatch)) - - hitLookups <- IORef.newIORef [] - hitBatch <- runSuccessfulWithValidation fixture - (compiledOnlyValidationLookup \key -> do - IORef.modifyIORef' hitLookups (key :) - pure (Just freshRecord)) - (snd <$> action Foundation.PairSetCharacteristic) - assertEqual "compiled warm hit performs one exact lookup" - [Semantic.declarationValidationRecordKey freshRecord] - . reverse - =<< IORef.readIORef hitLookups - case Declaration.committedBatchDeclarationValidation hitBatch of - Just record -> - assertEqual - "compiled hit republishes the exact validation" - freshRecord - record - Nothing -> - assertFailure "compiled hit omitted validation" - -foundationProposition - :: Fixture - -> Foundation.FoundationAxiomTag - -> IO Identity.CheckedPropositionContent -foundationProposition fixture tag = do - closure <- expectRight - (Identity.validateObjectClosure - (Identity.theoryId (fixtureFoundation fixture)) - []) - expectRight - (Identity.validatePropositionContent - closure - (Core.frozenCoreTerm - (Core.mapFrozenGlobals - absurd - (Foundation.foundationAxiomFrozen - (fixtureFoundation fixture) - tag)))) - -opaqueFixtureObject :: Fixture -> Identity.AssertedObject -opaqueFixtureObject fixture = - let theory = Identity.theoryId (fixtureFoundation fixture) - seed = - Identity.opaqueDeclarationSeed - (fixtureOwner fixture) - (localDeclarationOrdinal 0) - SignatureDeclaration - (generatedObjectSlot 0) - identity = - Identity.opaqueObjectId - theory - seed - Core.TySet - in Identity.assertedObject - identity - (Identity.OpaqueObjectContent - theory - seed - Core.TySet) - -datatypeFixtureObject - :: Fixture - -> Natural - -> Identity.AssertedObject -datatypeFixtureObject fixture slot = - let theory = Identity.theoryId (fixtureFoundation fixture) - seed = - Identity.opaqueDeclarationSeed - (fixtureOwner fixture) - (localDeclarationOrdinal 0) - DatatypeDeclaration - (generatedObjectSlot slot) - identity = - Identity.opaqueObjectId theory seed Core.TySet - in Identity.assertedObject - identity - (Identity.OpaqueObjectContent theory seed Core.TySet) - - -data Fixture = Fixture - { fixtureFoundation :: !Foundation.CheckedFoundation - , fixtureOwner :: !ModuleName - , fixtureProposition :: !Identity.CheckedPropositionContent - } - -makeFixture :: IO Fixture -makeFixture = - makeNamedFixture "root" - -makeNamedFixture :: Text -> IO Fixture -makeNamedFixture name = do - foundation <- expectRight Foundation.checkedFoundation - namespaceDigest <- expectRight - (hashCanonicalFields - "declaration-test-namespace" - [TextEncoding.encodeUtf8 name]) - relative <- expectRight - (safeRelativePath - (Text.unpack name <> ".tex")) - let theory = Identity.theoryId foundation - owner = - moduleNameFromParts - (sourceNamespaceIdFromDigest namespaceDigest) - relative - closure <- expectRight - (Identity.validateObjectClosure theory []) - proposition <- expectRight - (Identity.validatePropositionContent closure Core.CFalsum) - pure - Fixture - { fixtureFoundation = foundation - , fixtureOwner = owner - , fixtureProposition = proposition - } - -factSpec :: Fixture -> Text -> Declaration.CandidateSpec -factSpec fixture alias = - Declaration.candidateSpec - (fixtureProposition fixture) - Semantic.SearchEligible - [Semantic.semanticName alias] - -runDriver - :: Fixture - -> Declaration.ModuleDriver failure value - -> IO (Declaration.DriverResult failure value) -runDriver fixture = - runDriverWithResolver fixture unavailableVampireResolver - -runDriverWithResolver - :: Fixture - -> Declaration.VampireResolver - -> Declaration.ModuleDriver failure value - -> IO (Declaration.DriverResult failure value) -runDriverWithResolver fixture resolver action = do - result <- Declaration.runModuleDriver - (fixtureFoundation fixture) - (fixtureOwner fixture) - [] - resolver - Declaration.FreshValidation - action - expectRight result - -runDriverWithValidation - :: Fixture - -> Declaration.ValidationLookup - -> Declaration.ModuleDriver failure value - -> IO (Declaration.DriverResult failure value) -runDriverWithValidation fixture lookup action = do - runDriverWithValidationAndResolver - fixture - lookup - unavailableVampireResolver - action - -runDriverWithValidationAndResolver - :: Fixture - -> Declaration.ValidationLookup - -> Declaration.VampireResolver - -> Declaration.ModuleDriver failure value - -> IO (Declaration.DriverResult failure value) -runDriverWithValidationAndResolver fixture lookup resolver action = do - result <- Declaration.runModuleDriver - (fixtureFoundation fixture) - (fixtureOwner fixture) - [] - resolver - (Declaration.WarmValidation lookup) - action - expectRight result - -proofOnlyValidationLookup - :: (Semantic.ProofValidationKey - -> IO (Maybe Semantic.ProofValidationRecord)) - -> Declaration.ValidationLookup -proofOnlyValidationLookup lookupProof = - Declaration.validationLookup - lookupProof - (const (pure Nothing)) - -compiledOnlyValidationLookup - :: (Semantic.DeclarationValidationKey - -> IO (Maybe Semantic.DeclarationValidationRecord)) - -> Declaration.ValidationLookup -compiledOnlyValidationLookup lookupDeclaration = - Declaration.validationLookup - (const (pure Nothing)) - lookupDeclaration - -runDriverWithDirect - :: Fixture - -> [Semantic.SemanticInterfaceId] - -> Declaration.ModuleDriver failure value - -> IO (Declaration.DriverResult failure value) -runDriverWithDirect fixture direct action = do - result <- Declaration.runModuleDriver - (fixtureFoundation fixture) - (fixtureOwner fixture) - direct - unavailableVampireResolver - Declaration.FreshValidation - action - expectRight result - -unavailableVampireResolver :: Declaration.VampireResolver -unavailableVampireResolver = - Declaration.vampireResolver \_prepared -> - pure - (Left - (Provers.ProverLaunchFailed - "unused" - "Vampire resolver was not expected")) - -runSuccessful - :: Fixture - -> Declaration.ModuleDriver failure value - -> IO value -runSuccessful fixture = - runSuccessfulWithResolver fixture unavailableVampireResolver - -runSuccessfulWithResolver - :: Fixture - -> Declaration.VampireResolver - -> Declaration.ModuleDriver failure value - -> IO value -runSuccessfulWithResolver fixture resolver action = do - outcome <- runDriverWithResolver fixture resolver action - case outcome of - Declaration.DriverSucceeded value _interface _prefix _closure -> - pure value - Declaration.DriverFailed _failure _prefix -> - assertFailure "unexpected driver failure" >> fail "unreachable" - Declaration.DriverSealFailed failure _prefix -> - assertFailure (show failure) >> fail "unreachable" - -runSuccessfulWithValidation - :: Fixture - -> Declaration.ValidationLookup - -> Declaration.ModuleDriver failure value - -> IO value -runSuccessfulWithValidation fixture lookup action = do - outcome <- runDriverWithValidation fixture lookup action - case outcome of - Declaration.DriverSucceeded value _interface _prefix _closure -> - pure value - Declaration.DriverFailed _failure _prefix -> - assertFailure "unexpected driver failure" >> fail "unreachable" - Declaration.DriverSealFailed failure _prefix -> - assertFailure (show failure) >> fail "unreachable" - -materializesSealedImport :: Assertion -materializesSealedImport = do - fixture <- makeFixture - producer <- runDriver fixture do - (_value, batch) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "sealed-import-producer") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "producer-fact") - Declaration.authorizeOmittedCandidate candidate - Declaration.recordOmittedUse - pure batch - (producerInterface, evidence, fingerprint) <- - case producer of - Declaration.DriverSucceeded _ interface prefix _closure -> - let imported = - Declaration.freshImportedModuleEvidence - [] interface prefix - in case concatMap - Semantic.declarationDeltaFacts - (Semantic.semanticInterfaceDeclarations interface) of - [occurrence] -> - pure - ( interface - , imported - , Semantic.semanticFactFingerprint occurrence - ) - occurrences -> - assertFailure - ("unexpected producer facts: " - <> show (length occurrences)) - >> fail "unreachable" - Declaration.DriverFailed failure _prefix -> - assertFailure - ("producer failed: " - <> show - (failure - :: Declaration.DriverFailure - Declaration.DeclarationError)) - >> fail "unreachable" - Declaration.DriverSealFailed failure _prefix -> - assertFailure ("producer did not seal: " <> show failure) - >> fail "unreachable" - consumerNamespace <- expectRight - (hashCanonicalFields - "declaration-import-consumer" - ["consumer"]) - consumerPath <- expectRight (safeRelativePath "consumer.tex") - let consumerFixture = - fixture - { fixtureOwner = - moduleNameFromParts - (sourceNamespaceIdFromDigest consumerNamespace) - consumerPath - } - consumer <- runDriverWithDirect consumerFixture - [Semantic.semanticInterfaceAssertedId producerInterface] - do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "sealed-import-consumer") do - Declaration.importSealedModule evidence - candidate <- Declaration.reserveCandidate - (factSpec fixture "consumer-fact") - Declaration.authorizeOmittedCandidate candidate do - _ <- Declaration.useAuthorizedFact fingerprint - Declaration.recordOmittedUse - pure committed - case consumer of - Declaration.DriverSucceeded committed _ _ _ -> do - case Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta committed) of - [localOccurrence] -> do - assertEqual - "the first local fact keeps ordinal zero" - (localFactOrdinal 0) - (Semantic.factSlotOrdinal - (Semantic.semanticFactSlot localOccurrence)) - assertEqual - "the local fact belongs to the consumer" - (fixtureOwner consumerFixture) - (Semantic.factSlotModule - (Semantic.semanticFactSlot localOccurrence)) - facts -> - assertFailure - ("unexpected consumer fact count: " - <> show (length facts)) - Declaration.DriverFailed failure _prefix -> - assertFailure - ("consumer failed: " - <> show - (failure - :: Declaration.DriverFailure - Declaration.DeclarationError)) - Declaration.DriverSealFailed failure _prefix -> - assertFailure ("consumer did not seal: " <> show failure) - -elaboratesScopedExactPropositions :: Assertion -elaboratesScopedExactPropositions = do - fixture <- makeNamedFixture "exact-scoped-proposition" - let x = Raw.NamedVar "x" - y = Raw.NamedVar "y" - statement = - Raw.SymbolicQuantified - Nowhere - Raw.Universally - (x :| [y]) - Raw.Unbounded - Nothing - (Raw.StmtFormula - (Raw.FormulaChain - (Raw.ChainBase - (Raw.ExprVar x :| []) - Raw.Positive - (Raw.Relation - Nowhere - Raw.EqSymbol - []) - (Raw.ExprVar y :| [])))) - action - :: Declaration.ModuleDriver Text - (Either - Exact.ExactCompileError - Exact.PreparedExactProposition) - action = - Declaration.runProspectiveLoweringDriver - (Exact.prepareExactProposition - Exact.emptyExactBinderContext - statement) - outcome <- runDriver fixture action - case outcome of - Declaration.DriverSucceeded (Right prepared) _interface _prefix _closure -> - assertEqual - "source-order universal binders" - (Core.CForall Core.TySet - (Core.CForall Core.TySet - (Core.CEq Core.TySet - (Core.CBound 1) - (Core.CBound 0)))) - (Core.scopedCoreTerm - (Exact.preparedExactPropositionCore prepared)) - Declaration.DriverSucceeded (Left failure) _interface _prefix _closure -> - assertFailure - ("scoped exact elaboration failed: " - <> Text.unpack (Exact.renderExactCompileError failure)) - Declaration.DriverFailed failure _prefix -> - assertFailure ("scoped exact driver failed: " <> show failure) - Declaration.DriverSealFailed failure _prefix -> - assertFailure ("scoped exact driver did not seal: " <> show failure) - -preparesExactClaimEnvelopes :: Assertion -preparesExactClaimEnvelopes = do - fixture <- makeNamedFixture "exact-claim-envelope" - let bLocation = mkLocation (FileId 78) 2 11 - aLocation = mkLocation (FileId 78) 2 15 - xLocation = mkLocation (FileId 78) 3 9 - b = Raw.NamedVarAt bLocation "b" - a = Raw.NamedVarAt aLocation "a" - x = Raw.NamedVarAt xLocation "x" - c = Raw.NamedVarAt Nowhere "c" - d = Raw.NamedVarAt Nowhere "d" - z = Raw.NamedVarAt Nowhere "z" - equality left right = - Raw.StmtFormula - (Raw.FormulaChain - (Raw.ChainBase - (Raw.ExprVar left :| []) - Raw.Positive - (Raw.Relation Nowhere Raw.EqSymbol []) - (Raw.ExprVar right :| []))) - quantified variable body = - Raw.SymbolicQuantified - (locate variable) - Raw.Universally - (variable :| []) - Raw.Unbounded - Nothing - body - sourceAssumptions = [Raw.AsmSuppose (equality b a)] - sourceConclusion = quantified x (equality x b) - alphaAssumptions = [Raw.AsmSuppose (equality c d)] - alphaConclusion = quantified z (equality z c) - action - :: Declaration.ModuleDriver Text - ( Either - Exact.ExactCompileError - Exact.PreparedExactClaimEnvelope - , Either - Exact.ExactCompileError - Exact.PreparedExactClaimEnvelope - ) - action = - Declaration.runProspectiveLoweringDriver do - source <- Exact.prepareExactClaimEnvelope - sourceAssumptions sourceConclusion - alpha <- Exact.prepareExactClaimEnvelope - alphaAssumptions alphaConclusion - pure (source, alpha) - expected = - Core.CForall Core.TySet - (Core.CForall Core.TySet - (Core.CImp - (Core.CEq Core.TySet - (Core.CBound 1) - (Core.CBound 0)) - (Core.CForall Core.TySet - (Core.CEq Core.TySet - (Core.CBound 0) - (Core.CBound 2))))) - runDriver fixture action >>= \case - Declaration.DriverSucceeded - (Right source, Right alpha) - _interface _prefix _closure -> do - let sourceTarget = Exact.preparedExactClaimTarget source - alphaTarget = Exact.preparedExactClaimTarget alpha - assertEqual "closed claim envelope core" - expected - (Core.scopedCoreTerm sourceTarget) - assertEqual "claim envelope is closed" - [] - (Core.scopedCoreContext sourceTarget) - assertEqual "first semantic occurrence binder order" - [bLocation, aLocation] - (locate <$> Exact.preparedExactClaimVariables source) - assertEqual "explicit binders are not generalized" - 2 - (length (Exact.preparedExactClaimVariables source)) - assertEqual "header antecedent count" - 1 - (Exact.preparedExactClaimAntecedentCount source) - assertEqual "alpha-renaming preserves the checked target" - sourceTarget alphaTarget - assertEqual "alpha-renaming preserves proposition identity" - (Identity.propositionIdOf - (Core.scopedCoreTerm sourceTarget)) - (Identity.propositionIdOf - (Core.scopedCoreTerm alphaTarget)) - Declaration.DriverSucceeded result _interface _prefix _closure -> - assertFailure - ("exact claim envelope preparation failed: " - <> case result of - (Left failure, _) -> - Text.unpack - (Exact.renderExactCompileError failure) - (_, Left failure) -> - Text.unpack - (Exact.renderExactCompileError failure)) - Declaration.DriverFailed failure _prefix -> - assertFailure ("claim envelope driver failed: " <> show failure) - Declaration.DriverSealFailed failure _prefix -> - assertFailure - ("claim envelope driver did not seal: " <> show failure) - -lowersExactSeparationComprehensions :: Assertion -lowersExactSeparationComprehensions = do - fixture <- makeNamedFixture "exact-separation-comprehension" - let binderLocation = mkLocation (FileId 73) 2 7 - ambientLocation = mkLocation (FileId 73) 2 18 - boundOccurrenceLocation = mkLocation (FileId 73) 3 14 - x = Raw.NamedVarAt binderLocation "x" - a = Raw.NamedVarAt ambientLocation "A" - equality left right = - Raw.StmtFormula - (Raw.FormulaChain - (Raw.ChainBase - (left :| []) - Raw.Positive - (Raw.Relation Nowhere Raw.EqSymbol []) - (right :| []))) - separation bound = - Raw.ExprSep - binderLocation - x - bound - (equality (Raw.ExprVar x) (Raw.ExprVar a)) - validStatement = - Raw.SymbolicQuantified - Nowhere - Raw.Universally - (a :| []) - Raw.Unbounded - Nothing - (equality - (separation (Raw.ExprVar a)) - (Raw.ExprVar a)) - boundOccurrence = - Raw.NamedVarAt boundOccurrenceLocation "x" - invalidStatement = - equality - (separation (Raw.ExprVar boundOccurrence)) - (Raw.ExprVar a) - action - :: Declaration.ModuleDriver Text - ( Either - Exact.ExactCompileError - Exact.PreparedExactProposition - , Either - Exact.ExactCompileError - Exact.PreparedExactProposition - ) - action = - Declaration.runProspectiveLoweringDriver do - valid <- Exact.prepareExactProposition - Exact.emptyExactBinderContext - validStatement - invalid <- Exact.prepareExactProposition - Exact.emptyExactBinderContext - invalidStatement - pure (valid, invalid) - outcome <- runDriver fixture action - case outcome of - Declaration.DriverSucceeded - (Right prepared, Left failure) _interface _prefix _closure -> do - assertEqual - "separation comprehension core" - (Core.CForall Core.TySet - (Core.CEq Core.TySet - (Core.CApp - (Core.CApp - (Core.CIntrinsic Core.Sep) - (Core.CBound 0)) - (Core.CLam Core.TySet - (Core.CEq Core.TySet - (Core.CBound 0) - (Core.CBound 1)))) - (Core.CBound 0))) - (Core.scopedCoreTerm - (Exact.preparedExactPropositionCore prepared)) - assertEqual - "separation proposition type" - Core.TyProp - (Core.scopedCoreType - (Exact.preparedExactPropositionCore prepared)) - assertEqual - "the separation binder is unavailable in its bound" - (Exact.ExactFreeVariable - boundOccurrenceLocation - boundOccurrence) - failure - Declaration.DriverSucceeded result _interface _prefix _closure -> - case result of - (Left validFailure, _) -> - assertFailure - ("valid separation failed: " - <> Text.unpack - (Exact.renderExactCompileError validFailure)) - (_, Right{}) -> - assertFailure "invalid separation was accepted" - Declaration.DriverFailed failure _prefix -> - assertFailure ("separation exact driver failed: " <> show failure) - Declaration.DriverSealFailed failure _prefix -> - assertFailure ("separation exact driver did not seal: " <> show failure) - -lowersExactReplacementTelescopes :: Assertion -lowersExactReplacementTelescopes = do - fixture <- makeNamedFixture "exact-replacement-telescope" - let location = mkLocation (FileId 74) 2 1 - futureOccurrenceLocation = mkLocation (FileId 74) 7 19 - a = Raw.NamedVarAt location "A" - x = Raw.NamedVarAt location "x" - y = Raw.NamedVarAt location "y" - futureY = Raw.NamedVarAt futureOccurrenceLocation "y" - equality left right = - Raw.StmtFormula - (Raw.FormulaChain - (Raw.ChainBase - (left :| []) - Raw.Positive - (Raw.Relation Nowhere Raw.EqSymbol []) - (right :| []))) - replacement firstDomain = - Raw.ExprReplace - location - (Raw.ExprVar y) - ( (x, firstDomain) :| - [(y, Raw.ExprVar x)] - ) - (Just (equality (Raw.ExprVar x) (Raw.ExprVar y))) - validStatement = - Raw.SymbolicQuantified - Nowhere - Raw.Universally - (a :| []) - Raw.Unbounded - Nothing - (equality - (replacement (Raw.ExprVar a)) - (Raw.ExprVar a)) - invalidStatement = - equality - (replacement (Raw.ExprVar futureY)) - (Raw.ExprInteger Nowhere 0) - predicateReplacementLocation = mkLocation (FileId 74) 9 3 - predicateReplacementStatement = - equality - (Raw.ExprReplacePred - predicateReplacementLocation - y - x - (Raw.ExprInteger Nowhere 0) - (equality (Raw.ExprVar x) (Raw.ExprVar y))) - (Raw.ExprInteger Nowhere 0) - app1 intrinsic argument = - Core.CApp (Core.CIntrinsic intrinsic) argument - app2 intrinsic first second = - Core.CApp (app1 intrinsic first) second - expected = - Core.CForall Core.TySet $ - Core.CEq Core.TySet - (app1 Core.FamilyUnion $ - app2 Core.Repl (Core.CBound 0) $ - Core.CLam Core.TySet $ - app2 Core.Repl - (app2 Core.Sep - (Core.CBound 0) - (Core.CLam Core.TySet $ - Core.CEq Core.TySet - (Core.CBound 1) - (Core.CBound 0))) - (Core.CLam Core.TySet - (Core.CBound 0))) - (Core.CBound 0) - action - :: Declaration.ModuleDriver Text - ( Either - Exact.ExactCompileError - Exact.PreparedExactProposition - , Either - Exact.ExactCompileError - Exact.PreparedExactProposition - , Either - Exact.ExactCompileError - Exact.PreparedExactProposition - ) - action = - Declaration.runProspectiveLoweringDriver do - valid <- Exact.prepareExactProposition - Exact.emptyExactBinderContext - validStatement - invalid <- Exact.prepareExactProposition - Exact.emptyExactBinderContext - invalidStatement - predicateReplacement <- Exact.prepareExactProposition - Exact.emptyExactBinderContext - predicateReplacementStatement - pure (valid, invalid, predicateReplacement) - runDriver fixture action >>= \case - Declaration.DriverSucceeded - ( Right prepared - , Left failure - , Left predicateReplacementFailure - ) _interface _prefix _closure -> do - assertEqual - "dependent replacement core" - expected - (Core.scopedCoreTerm - (Exact.preparedExactPropositionCore prepared)) - assertEqual - "future replacement binder location" - (Exact.ExactFreeVariable futureOccurrenceLocation futureY) - failure - assertEqual - "predicate replacement remains unsupported at its location" - (Exact.ExactUnsupportedDeclarationBody - predicateReplacementLocation) - predicateReplacementFailure - Declaration.DriverSucceeded - (Left validFailure, _, _) _interface _prefix _closure -> - assertFailure - ("valid replacement failed: " - <> Text.unpack - (Exact.renderExactCompileError validFailure)) - Declaration.DriverSucceeded - (_, Right{}, _) _interface _prefix _closure -> - assertFailure "invalid replacement was accepted" - Declaration.DriverSucceeded - (_, _, Right{}) _interface _prefix _closure -> - assertFailure "predicate replacement was accepted" - Declaration.DriverFailed failure _prefix -> - assertFailure - ("replacement driver failed: " <> show failure) - Declaration.DriverSealFailed failure _prefix -> - assertFailure - ("replacement driver did not seal: " <> show failure) - -lowersExactFiniteSets :: Assertion -lowersExactFiniteSets = do - fixture <- makeNamedFixture "exact-finite-set" - let location = mkLocation (FileId 75) 2 1 - a = Raw.NamedVarAt location "a" - b = Raw.NamedVarAt location "b" - equality left right = - Raw.StmtFormula - (Raw.FormulaChain - (Raw.ChainBase - (left :| []) - Raw.Positive - (Raw.Relation Nowhere Raw.EqSymbol []) - (right :| []))) - statement = - Raw.SymbolicQuantified - Nowhere - Raw.Universally - (a :| [b]) - Raw.Unbounded - Nothing - (equality - (Raw.ExprFiniteSet - location - (Raw.ExprVar a :| [Raw.ExprVar b])) - (Raw.ExprVar a)) - app1 intrinsic argument = - Core.CApp (Core.CIntrinsic intrinsic) argument - app2 intrinsic first second = - Core.CApp (app1 intrinsic first) second - insert element rest = - app1 Core.FamilyUnion - (app2 Core.PairSet - (app2 Core.PairSet element element) - rest) - expected = - Core.CForall Core.TySet - (Core.CForall Core.TySet - (Core.CEq Core.TySet - (insert - (Core.CBound 1) - (insert - (Core.CBound 0) - (Core.CIntrinsic Core.Empty))) - (Core.CBound 1))) - action - :: Declaration.ModuleDriver Text - (Either - Exact.ExactCompileError - Exact.PreparedExactProposition) - action = - Declaration.runProspectiveLoweringDriver - (Exact.prepareExactProposition - Exact.emptyExactBinderContext - statement) - runDriver fixture action >>= \case - Declaration.DriverSucceeded - (Right prepared) _interface _prefix _closure -> - assertEqual - "source-order finite-set core" - expected - (Core.scopedCoreTerm - (Exact.preparedExactPropositionCore prepared)) - Declaration.DriverSucceeded - (Left failure) _interface _prefix _closure -> - assertFailure - ("valid finite set failed: " - <> Text.unpack - (Exact.renderExactCompileError failure)) - Declaration.DriverFailed failure _prefix -> - assertFailure - ("finite-set driver failed: " <> show failure) - Declaration.DriverSealFailed failure _prefix -> - assertFailure - ("finite-set driver did not seal: " <> show failure) - -lowersExactOrdinaryDeclarations :: Assertion -lowersExactOrdinaryDeclarations = do - fixture <- makeNamedFixture "exact-lowering" - level <- expectRight (Syntax.mixfixLevel 2) - let makeSymbol command marker = - Raw.mkMixfixItem - [ Just (Raw.Command command) - , Just Raw.InvisibleBraceL - , Nothing - , Just Raw.InvisibleBraceR - ] - (Raw.Marker marker) - Raw.NonAssoc - opaqueSymbol = makeSymbol "phasefiveopaque" "opaque-label" - aliasSymbol = makeSymbol "phasefivealias" "alias-label" - definitionSymbol = makeSymbol "phasefivedef" "definition-label" - entry symbol = - Syntax.CanonicalExpressionFunction - (Raw.mixfixPattern symbol) - (Raw.mixfixMarker symbol) - (Syntax.Fixity Raw.NonAssoc level) - parameter = Raw.NamedVar "x" - exactSet = - Raw.NounPhrase - [] - (Raw.Noun Nowhere Lexicon.builtinSetNoun []) - Nothing - [] - Nothing - signature = - Raw.BlockSig - Nowhere Nothing (Raw.Marker "opaque-declaration") [] - (Raw.SignatureSymbolic - (Raw.SymbolPattern opaqueSymbol [parameter]) - exactSet) - application symbol = - Raw.ExprOp Nowhere symbol [Raw.ExprVar parameter] - abbreviation = - Raw.BlockAbbr - Nowhere Nothing (Raw.Marker "alias-declaration") - (Raw.AbbreviationEq - (Raw.SymbolPattern aliasSymbol [parameter]) - (application opaqueSymbol)) - definition = - Raw.BlockDefn - Nowhere Nothing (Raw.Marker "definition-declaration") - (Raw.DefnOp - (Raw.SymbolPattern definitionSymbol [parameter]) - (application aliasSymbol)) - compile block lexicalEntry = do - Declaration.runProspectiveLoweringDriver - (Exact.prepareExactDeclaration block [lexicalEntry]) >>= \case - Left failure -> - Declaration.failModuleDriver - (Exact.renderExactCompileError failure) - Right prepared -> pure prepared - admit prepared = do - lowered <- - Declaration.runProspectiveLoweringDriver - (Exact.lowerPreparedExactBinding prepared) - checked <- - either Declaration.failDeclarationDriver pure lowered - void - (Declaration.admitCheckedDeclaration - checked - Exact.authorizeCheckedExactBinding) - outcome <- runFixtureDriver fixture [] do - preparedSignature <- - compile signature (entry opaqueSymbol) - admit preparedSignature - preparedAbbreviation <- - compile abbreviation (entry aliasSymbol) - admit preparedAbbreviation - preparedDefinition <- - compile definition (entry definitionSymbol) - admit preparedDefinition - pure - ( preparedSignature - , preparedAbbreviation - , preparedDefinition - ) - case outcome of - Declaration.DriverSucceeded - (preparedSignature, preparedAbbreviation, preparedDefinition) - interface prefix _closure -> do - assertEqual "three committed declarations" - 3 - (length (Semantic.semanticInterfaceDeclarations interface)) - assertEqual "three committed batches" - 3 - (length (Declaration.pendingModulePrefixBatches prefix)) - assertEqual "opaque signature family" - Identity.OpaqueObject - (Identity.objectIdFamily - (Exact.preparedExactObjectId preparedSignature)) - assertEqual "transparent abbreviation family" - Identity.TransparentObject - (Identity.objectIdFamily - (Exact.preparedExactObjectId preparedAbbreviation)) - assertEqual "transparent definition family" - Identity.TransparentObject - (Identity.objectIdFamily - (Exact.preparedExactObjectId preparedDefinition)) - assertEqual "expanded definition coalesces with abbreviation" - (Exact.preparedExactObjectId preparedAbbreviation) - (Exact.preparedExactObjectId preparedDefinition) - case Exact.preparedExactObject preparedAbbreviation of - Just object -> - case Identity.assertedObjectContent object of - Identity.TransparentObjectContent - _theory coreType body -> do - assertEqual "definition type" - (Core.TyArrow Core.TySet Core.TySet) - coreType - assertEqual "expanded body retains opaque seed" - (Core.CLam Core.TySet - (Core.CApp - (Core.CGlobal - (Exact.preparedExactObjectId - preparedSignature)) - (Core.CBound 0))) - body - content -> - assertFailure - ("unexpected definition content: " <> show content) - Nothing -> - assertFailure "new abbreviation object was not prepared" - assertEqual "coalesced definition adds no object" - Nothing - (Exact.preparedExactObject preparedDefinition) - case reverse (Declaration.pendingModulePrefixBatches prefix) of - definitionBatch : _ -> do - case Declaration.committedBatchDeclarationValidation - definitionBatch of - Just record -> - case Semantic.declarationValidationRecordCertificates - record of - [certificate] -> do - assertEqual "definition authority" - (Authority.CheckedKernelConstruction - (Authority.CheckedDefinitionEquation - (Exact.preparedExactObjectId - preparedDefinition))) - (Authority.validationDirectAuthorization - certificate) - assertEqual "definition authority is clean" - Authority.cleanAuthoritySafety - (Authority.factAuthoritySafety - (Authority.validationTarget - certificate)) - certificates -> - assertFailure - ("unexpected definition certificate count: " - <> show (length certificates)) - Nothing -> - assertFailure "definition has no declaration validation" - [] -> assertFailure "definition batch is absent" - Declaration.DriverFailed failure _prefix -> - assertFailure ("exact lowering failed: " <> show failure) - Declaration.DriverSealFailed failure _prefix -> - assertFailure ("exact lowering did not seal: " <> show failure) - - let theory = Identity.theoryId (fixtureFoundation fixture) - mismatchBody = Core.COpaqueInteger 0 - mismatchType = Core.TySet - mismatchId = - Identity.transparentObjectId theory mismatchType mismatchBody - mismatchObject = - Identity.assertedObject - mismatchId - (Identity.TransparentObjectContent - theory mismatchType mismatchBody) - let mismatchAction - :: Declaration.ModuleDriver Text - ((), Declaration.CommittedDeclarationBatch) - mismatchAction = - Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId - "mismatched-definition-equation") do - Declaration.addDeclarationObject mismatchObject - candidate <- Declaration.reserveCandidate - (factSpec fixture "not-a-definition-equation") - Declaration.authorizeCompiledDeclaration - (Declaration.authorizeDefinitionEquationCandidate - mismatchId - candidate) - mismatch <- runDriver fixture mismatchAction - case mismatch of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - Declaration.DefinitionEquationCandidateMismatch) - prefix -> - assertEqual "mismatched equation publishes no batch" - 0 - (length (Declaration.pendingModulePrefixBatches prefix)) - Declaration.DriverFailed failure _prefix -> - assertFailure - ("unexpected mismatched-equation failure: " <> show failure) - Declaration.DriverSucceeded{} -> - assertFailure "mismatched definition equation was authorized" - Declaration.DriverSealFailed failure _prefix -> - assertFailure - ("mismatched definition equation reached sealing: " - <> show failure) - -reconstructsImportedGlobalBindings :: Assertion -reconstructsImportedGlobalBindings = do - producerFixture <- makeNamedFixture "global-producer" - consumerFixture <- makeNamedFixture "global-consumer" - conflictFixture <- makeNamedFixture "global-conflict" - rootFixture <- makeNamedFixture "global-root" - let key = - Semantic.SemanticExpressionFunction - (Raw.TokenCons (Raw.Command "phasefive") Raw.End) - asserted = opaqueFixtureObject producerFixture - target = Identity.assertedObjectId asserted - publishWith targetMode fixture object = do - (batch, sealed) <- sealFixture fixture [] do - (_value, committed) <- - Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "global-binding") do - Declaration.addDeclarationObject object - Declaration.stageSemanticGlobalBinding - key - (targetMode - (Identity.assertedObjectId object)) - Declaration.authorizeCompiledDeclaration (pure ()) - pure committed - pure (batch, sealed) - (producerBatch, freshProducer) <- - publishWith Semantic.GlobalReference producerFixture asserted - let FixtureSealed producerInterface _freshEvidence = freshProducer - objects = Declaration.committedBatchObjects producerBatch - cachedEvidence <- expectRight - (Declaration.validateImportedModuleEvidence - (Identity.theoryId - (fixtureFoundation producerFixture)) - [] - producerInterface - objects - []) - let cachedProducer = FixtureSealed producerInterface cachedEvidence - resolveThrough label parent = do - outcome <- runFixtureDriver consumerFixture [parent] do - fst <$> Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId - (TextEncoding.encodeUtf8 (Text.pack label))) do - found <- Declaration.resolveVisibleGlobal key - Declaration.authorizeCompiledDeclaration (pure ()) - pure found - case outcome of - Declaration.DriverSucceeded found _interface _prefix _closure -> - assertEqual label - (Just - ( Semantic.GlobalReference target - , Core.TySet - )) - found - Declaration.DriverFailed failure _prefix -> - assertFailure - ("global binding consumer failed: " <> show failure) - Declaration.DriverSealFailed failure _prefix -> - assertFailure - ("global binding consumer did not seal: " <> show failure) - resolveThrough "fresh-global-binding" freshProducer - resolveThrough "cached-global-binding" cachedProducer - - missingEnvironment <- expectRight - (Semantic.semanticEnvironmentDelta - [Semantic.semanticGlobalBinding - key - (Semantic.GlobalReference target)]) - missingDelta <- expectRight - (Semantic.declarationInterfaceDelta - (Semantic.declarationSlot - (fixtureOwner producerFixture) - (localDeclarationOrdinal 0)) - [] - [] - [] - [] - missingEnvironment) - missingInterface <- expectRight - (Semantic.semanticInterface - (fixtureOwner producerFixture) - [] - [missingDelta]) - case Declaration.validateImportedModuleEvidence - (Identity.theoryId - (fixtureFoundation producerFixture)) - [] - missingInterface - [] - [] of - Left (Declaration.ImportedGlobalTargetInvalid - actualKey actualTarget - (Semantic.SemanticGlobalTargetMissing missingTarget)) -> do - assertEqual "missing target key" key actualKey - assertEqual "missing target mode" - (Semantic.GlobalReference target) - actualTarget - assertEqual "missing target object" target missingTarget - Left failure -> - assertFailure - ("unexpected missing-target failure: " <> show failure) - Right _evidence -> - assertFailure "cached evidence accepted a missing target object" - - expansionEnvironment <- expectRight - (Semantic.semanticEnvironmentDelta - [Semantic.semanticGlobalBinding - key - (Semantic.TransparentExpansion target)]) - expansionDelta <- expectRight - (Semantic.declarationInterfaceDelta - (Semantic.declarationSlot - (fixtureOwner producerFixture) - (localDeclarationOrdinal 0)) - [] [] [target] [] expansionEnvironment) - expansionInterface <- expectRight - (Semantic.semanticInterface - (fixtureOwner producerFixture) [] [expansionDelta]) - case Declaration.validateImportedModuleEvidence - (Identity.theoryId - (fixtureFoundation producerFixture)) - [] - expansionInterface - [asserted] - [] of - Left (Declaration.ImportedGlobalTargetInvalid - actualKey actualTarget - (Semantic.SemanticGlobalExpansionNotTransparent - invalidTarget)) -> do - assertEqual "nontransparent target key" key actualKey - assertEqual "nontransparent target mode" - (Semantic.TransparentExpansion target) - actualTarget - assertEqual "nontransparent target object" target invalidTarget - Left failure -> - assertFailure - ("unexpected nontransparent-target failure: " - <> show failure) - Right _evidence -> - assertFailure "cached evidence accepted a nontransparent expansion" - - let intrinsicTarget = - Identity.intrinsicObjectId - (Identity.theoryId - (fixtureFoundation producerFixture)) - Core.Empty - Core.TySet - intrinsicObject = - Identity.assertedObject - intrinsicTarget - (Identity.IntrinsicObjectContent - (Identity.theoryId - (fixtureFoundation producerFixture)) - Core.Empty - Core.TySet) - intrinsicFailure <- runFixtureDriver producerFixture [] do - Declaration.commitCompiledDeclaration - (Semantic.declarationSyntaxId "intrinsic-global-binding") do - Declaration.addDeclarationObject intrinsicObject - Declaration.stageSemanticGlobalBinding - key - (Semantic.GlobalReference intrinsicTarget) - Declaration.authorizeCompiledDeclaration (pure ()) - case intrinsicFailure of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - (Declaration.DeclarationGlobalTargetInvalid - actualKey actualTarget - (Semantic.SemanticGlobalTargetIsIntrinsic - invalidTarget))) - _prefix -> do - assertEqual "intrinsic target key" key actualKey - assertEqual "intrinsic target mode" - (Semantic.GlobalReference intrinsicTarget) - actualTarget - assertEqual "intrinsic target object" - intrinsicTarget invalidTarget - other -> - assertFailure - (case other of - Declaration.DriverSucceeded{} -> - "ordinary binding accepted an intrinsic target" - Declaration.DriverFailed failure _prefix -> - "unexpected intrinsic-target failure: " <> show failure - Declaration.DriverSealFailed failure _prefix -> - "intrinsic target reached sealing: " <> show failure) - - conflictObject <- pure (opaqueFixtureObject conflictFixture) - (_conflictBatch, conflicting) <- - publishWith Semantic.GlobalReference conflictFixture conflictObject - collision <- runFixtureDriver rootFixture - [freshProducer, conflicting] - (pure ()) - case collision of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - (Declaration.ImportedGlobalCollision - actualKey firstTarget secondTarget)) - _prefix -> do - assertEqual "colliding global key" key actualKey - assertEqual "first imported target" - (Semantic.GlobalReference target) - firstTarget - assertEqual "second imported target" - (Semantic.GlobalReference - (Identity.assertedObjectId conflictObject)) - secondTarget - Declaration.DriverFailed failure _prefix -> - assertFailure - ("unexpected imported collision: " <> show failure) - Declaration.DriverSucceeded{} -> - assertFailure "unequal imported bindings did not collide" - Declaration.DriverSealFailed failure _prefix -> - assertFailure - ("global collision reached sealing: " <> show failure) - - let theory = Identity.theoryId (fixtureFoundation producerFixture) - transparentBody = Core.COpaqueInteger 0 - transparentTarget = - Identity.transparentObjectId - theory Core.TySet transparentBody - transparentObject = - Identity.assertedObject - transparentTarget - (Identity.TransparentObjectContent - theory Core.TySet transparentBody) - (_referenceBatch, referenceProducer) <- - publishWith - Semantic.GlobalReference - producerFixture - transparentObject - (_expansionBatch, expansionProducer) <- - publishWith - Semantic.TransparentExpansion - conflictFixture - transparentObject - modeCollision <- runFixtureDriver rootFixture - [referenceProducer, expansionProducer] - (pure ()) - case modeCollision of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - (Declaration.ImportedGlobalCollision - actualKey firstTarget secondTarget)) - _prefix -> do - assertEqual "mode collision key" key actualKey - assertEqual "reference target" - (Semantic.GlobalReference transparentTarget) - firstTarget - assertEqual "expansion target" - (Semantic.TransparentExpansion transparentTarget) - secondTarget - other -> - assertFailure - (case other of - Declaration.DriverSucceeded{} -> - "different global target modes did not collide" - Declaration.DriverFailed failure _prefix -> - "unexpected mode-collision failure: " <> show failure - Declaration.DriverSealFailed failure _prefix -> - "mode collision reached sealing: " <> show failure) - -data FixtureSealed = FixtureSealed - !Semantic.SemanticInterface - !Declaration.ImportedModuleEvidence - -foldsTransitiveAndDiamondEvidence :: Assertion -foldsTransitiveAndDiamondEvidence = do - baseFixture <- makeNamedFixture "base" - middleFixture <- makeNamedFixture "middle" - transitiveFixture <- makeNamedFixture "transitive" - leftFixture <- makeNamedFixture "left" - rightFixture <- makeNamedFixture "right" - diamondFixture <- makeNamedFixture "diamond" - conflictLeftFixture <- makeNamedFixture "conflict-left" - conflictRightFixture <- makeNamedFixture "conflict-right" - conflictRootFixture <- makeNamedFixture "conflict-root" - - (base, baseFingerprint) <- - sealFactFixture baseFixture [] "transitive-shared" - middle <- snd <$> sealFixture middleFixture [base] (pure ()) - transitive <- sealUsingImportedFact - transitiveFixture [middle] baseFingerprint - assertLocalFactOrdinalZero "transitive importer" transitive - - left <- snd <$> sealFixture leftFixture [base] (pure ()) - right <- snd <$> sealFixture rightFixture [base] (pure ()) - diamond <- sealUsingImportedFact - diamondFixture [left, right] baseFingerprint - assertLocalFactOrdinalZero "diamond importer" diamond - - (conflictLeft, leftFingerprint) <- - sealFactFixture conflictLeftFixture [] "diamond-conflict" - (conflictRight, rightFingerprint) <- - sealFactFixture conflictRightFixture [] "diamond-conflict" - conflict <- runFixtureDriver - conflictRootFixture - [conflictLeft, conflictRight] - (pure ()) - case conflict of - Declaration.DriverFailed - (Declaration.DriverDeclarationFailed - (Declaration.ImportedAliasCollision - alias - (Declaration.ImportedAliasOrigin - _leftSlot firstTarget) - (Declaration.ImportedAliasOrigin - _rightSlot secondTarget))) - _prefix -> do - assertEqual "conflicting alias" - (Semantic.semanticName "diamond-conflict") - alias - assertEqual "first alias origin" - leftFingerprint - firstTarget - assertEqual "second alias origin" - rightFingerprint - secondTarget - _ -> - assertFailure "conflicting diamond alias was not rejected" - where - sealUsingImportedFact fixture parents fingerprint = do - (batch, _sealed) <- sealFixture fixture parents do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId "use-transitive-import") do - candidate <- Declaration.reserveCandidate - (factSpec fixture "local-after-import") - Declaration.authorizeOmittedCandidate candidate do - void (Declaration.useAuthorizedFact fingerprint) - Declaration.recordOmittedUse - pure committed - pure batch - - assertLocalFactOrdinalZero label batch = - case Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta batch) of - [occurrence] -> - assertEqual label - (localFactOrdinal 0) - (Semantic.factSlotOrdinal - (Semantic.semanticFactSlot occurrence)) - facts -> - assertFailure - (label <> ": unexpected fact count " - <> show (length facts)) - -sealFactFixture - :: Fixture - -> [FixtureSealed] - -> Text - -> IO - ( FixtureSealed - , Semantic.SemanticFactOccurrenceFingerprint - ) -sealFactFixture fixture parents alias = do - (batch, sealed) <- sealFixture fixture parents do - (_value, committed) <- Declaration.commitProofDeclaration - (Semantic.proofSyntaxId - (TextEncoding.encodeUtf8 alias)) do - candidate <- Declaration.reserveCandidate - (factSpec fixture alias) - Declaration.authorizeSourceAxiomCandidate candidate - pure committed - case Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta batch) of - [occurrence] -> - pure - ( sealed - , Semantic.semanticFactFingerprint occurrence - ) - facts -> - assertFailure - ("unexpected sealed fact count: " <> show (length facts)) - >> fail "unreachable" - -sealFixture - :: Fixture - -> [FixtureSealed] - -> Declaration.ModuleDriver Text value - -> IO (value, FixtureSealed) -sealFixture fixture parents action = do - outcome <- runFixtureDriver fixture parents action - case outcome of - Declaration.DriverSucceeded value interface prefix _closure -> - pure - ( value - , FixtureSealed - interface - (Declaration.freshImportedModuleEvidence - [ evidence - | FixtureSealed _interface evidence <- parents - ] - interface - prefix) - ) - Declaration.DriverFailed failure _prefix -> - assertFailure ("fixture failed: " <> show failure) - >> fail "unreachable" - Declaration.DriverSealFailed failure _prefix -> - assertFailure ("fixture did not seal: " <> show failure) - >> fail "unreachable" - -runFixtureDriver - :: Fixture - -> [FixtureSealed] - -> Declaration.ModuleDriver Text value - -> IO (Declaration.DriverResult Text value) -runFixtureDriver fixture parents action = do - result <- Declaration.runModuleDriver - (fixtureFoundation fixture) - (fixtureOwner fixture) - [ Semantic.semanticInterfaceAssertedId interface - | FixtureSealed interface _evidence <- parents - ] - unavailableVampireResolver - Declaration.FreshValidation - do - traverse_ - (\(FixtureSealed _interface evidence) -> - Declaration.importSealedModuleDriver evidence) - parents - action - expectRight result - -requireSingleOccurrence - :: Declaration.CommittedDeclarationBatch - -> Declaration.ModuleDriver - Declaration.DeclarationError - Semantic.SemanticFactOccurrence -requireSingleOccurrence batch = - case Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta batch) of - [occurrence] -> - pure occurrence - _ -> - Declaration.failModuleDriver - Declaration.ProofDeclarationMustProduceOneFact - -expectRight :: Show error => Either error value -> IO value -expectRight = \case - Left err -> - assertFailure (show err) >> fail "unreachable" - Right value -> - pure value - -expectRightIO :: Show error => IO (Either error value) -> IO value -expectRightIO action = - action >>= expectRight - -withOpenedStore - :: Fixture - -> FilePath - -> (Store.Store -> IO value) - -> IO value -withOpenedStore fixture root action = - bracket - (expectRightIO - (Store.openStore - (root Posix.</> "store.sqlite") - (Identity.theoryId (fixtureFoundation fixture)))) - (Store.closeStore . snd) - (action . snd) - -withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a -withTemporaryDirectory template = - bracket create Directory.removePathForcibly - where - create = do - root <- Directory.getTemporaryDirectory - (path, handle) <- openTempFile root template - hClose handle - Directory.removeFile path - Directory.createDirectory path - pure path |