diff options
Diffstat (limited to 'source/Felix/Test/Unit/Declaration.hs')
| -rw-r--r-- | source/Felix/Test/Unit/Declaration.hs | 3596 |
1 files changed, 3596 insertions, 0 deletions
diff --git a/source/Felix/Test/Unit/Declaration.hs b/source/Felix/Test/Unit/Declaration.hs new file mode 100644 index 0000000..f3d9be7 --- /dev/null +++ b/source/Felix/Test/Unit/Declaration.hs @@ -0,0 +1,3596 @@ +{-# LANGUAGE NoImplicitPrelude #-} + +module Felix.Test.Unit.Declaration (unitTests) where + +import Base +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Backend.Problem qualified as Backend +import Felix.Checking.Core qualified as Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Exact qualified as Exact +import Felix.Checking.Exact.Vocabulary qualified as Vocabulary +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Kernel.Derivation qualified as Kernel +import Felix.Checking.SetConstruction qualified as SetConstruction +import Felix.Checking.Semantic qualified as Semantic +import Felix.Checking.Typed.Inductive qualified as Typed +import Felix.Math.Codec +import Felix.Module +import Felix.Source +import Felix.Store qualified as Store +import Felix.Meaning qualified as Meaning +import Felix.Provers qualified as Provers +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface qualified as Syntax +import Felix.Syntax.Internal qualified as Internal +import Felix.Syntax.Lexicon qualified as Lexicon + +import Data.List.NonEmpty qualified as NonEmpty +import Data.IORef qualified as IORef +import Data.Set qualified as Set +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.Except (runExceptT) +import Control.Monad.State (evalState) +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 "lowers fixed equality aliases without global support" + lowersFixedEqualityAliases + , testCase "scopes quantified proposition terms" + scopesQuantifiedPropositionTerms + , 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.FirstOrderLocals + Backend.ExplicitHigherOrderJustification) + 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.CompleteLocals + Backend.ExplicitHigherOrderJustification) + 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 = + 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) + +lowersFixedEqualityAliases :: Assertion +lowersFixedEqualityAliases = do + fixture <- makeNamedFixture "fixed-equality-aliases" + let x = Raw.NamedVar "x" + y = Raw.NamedVar "y" + z = Raw.NamedVar "z" + term variable = Raw.TermExpr (Raw.ExprVar variable) + equality left right = + Raw.StmtFormula + (Raw.FormulaChain + (Raw.ChainBase + (Raw.ExprVar left :| []) + Raw.Positive + (Raw.Relation Nowhere Raw.EqSymbol []) + (Raw.ExprVar right :| []))) + quantified variables statement = + Raw.SymbolicQuantified + Nowhere + Raw.Universally + variables + Raw.Unbounded + Nothing + statement + adjective = + Raw.Adj + Nowhere + Lexicon.builtinEqualityRightAdjective + [term y] + copular = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPAdj (adjective :| [])) + rightAttribute = + Raw.StmtNoun + (term x :| []) + (Raw.NounPhrase + [] + (Raw.Noun Nowhere Lexicon.builtinSetNoun []) + Nothing + [ Raw.AdjR + Nowhere + Lexicon.builtinEqualityRightAdjective + [term y] + ] + Nothing) + rightAttributeExpected = + Raw.StmtNoun + (term x :| []) + (Raw.NounPhrase + [] + (Raw.Noun Nowhere Lexicon.builtinSetNoun []) + Nothing + [] + (Just (equality x y))) + verb argument = + Raw.Verb + Nowhere + Lexicon.builtinEqualityVerb + [term argument] + singular = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerb (verb y)) + negated = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerbNot (verb y)) + coordinated = + Raw.StmtVerbPhrase + (term x :| [term y]) + (Raw.VPVerb (verb z)) + coordinatedExpected = + Raw.StmtConnected + Raw.Conjunction + Nothing + (equality x z) + (equality y z) + comparisons = + [ ( "copular adjective" + , quantified (x :| [y]) copular + , quantified (x :| [y]) (equality x y) + ) + , ( "right adjective" + , quantified (x :| [y]) rightAttribute + , quantified (x :| [y]) rightAttributeExpected + ) + , ( "singular verb" + , quantified (x :| [y]) singular + , quantified (x :| [y]) (equality x y) + ) + , ( "negated verb" + , quantified (x :| [y]) negated + , quantified + (x :| [y]) + (Raw.StmtNeg Nowhere (equality x y)) + ) + , ( "quantified coordinated verb" + , quantified (x :| [y, z]) coordinated + , quantified (x :| [y, z]) coordinatedExpected + ) + ] + action + :: Declaration.ModuleDriver Text + [ ( Either + Exact.ExactCompileError + Exact.PreparedExactProposition + , Either + Exact.ExactCompileError + Exact.PreparedExactProposition + ) + ] + action = + Declaration.runProspectiveLoweringDriver + (traverse + (\(_label, alias, symbolic) -> + (,) + <$> Exact.prepareExactProposition + Exact.emptyExactBinderContext alias + <*> Exact.prepareExactProposition + Exact.emptyExactBinderContext symbolic) + comparisons) + runDriver fixture action >>= \case + Declaration.DriverSucceeded results _interface _prefix _closure -> + for_ (zip comparisons results) \((label, _alias, _symbolic), result) -> + case result of + (Right alias, Right symbolic) -> do + let aliasTerm = + Core.scopedCoreTerm + (Exact.preparedExactPropositionCore alias) + symbolicTerm = + Core.scopedCoreTerm + (Exact.preparedExactPropositionCore symbolic) + assertEqual + (label <> " checked core") + symbolicTerm + aliasTerm + assertEqual + (label <> " global support") + Set.empty + (Core.canonicalTermGlobals aliasTerm) + assertEqual + (label <> " foundation support") + Set.empty + (Foundation.foundationAxiomDependencies aliasTerm) + (Left failure, _) -> + assertFailure + (label <> " alias failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + (_, Left failure) -> + assertFailure + (label <> " symbolic comparison failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + Declaration.DriverFailed failure _prefix -> + assertFailure ("fixed equality driver failed: " <> show failure) + Declaration.DriverSealFailed failure _prefix -> + assertFailure ("fixed equality driver did not seal: " <> show failure) + + let internalEquality = + Internal.FormulaVerb + Nowhere + (Internal.EmptySet Nowhere) + Lexicon.builtinEqualityVerb + [Internal.EmptySet Nowhere] + internalResult + :: Either + Typed.TypedInductiveError + (Core.FrozenCheckedCore Void) + internalResult = + Typed.prepareTypedClosedFormula + absurd + (const Nothing) + internalEquality + case internalResult of + Right checked -> do + assertEqual + "internal fixed verb core" + (Core.CEq + Core.TySet + (Core.CIntrinsic Core.Empty) + (Core.CIntrinsic Core.Empty)) + (Core.frozenCoreTerm checked) + assertEqual + "internal fixed verb global support" + Set.empty + (Core.frozenCoreGlobals checked) + Left failure -> + assertFailure + ("internal fixed verb failed: " <> show failure) + +scopesQuantifiedPropositionTerms :: Assertion +scopesQuantifiedPropositionTerms = do + fixture <- makeNamedFixture "quantified-proposition-terms" + let x = Raw.NamedVar "x" + y = Raw.NamedVar "y" + term variable = Raw.TermExpr (Raw.ExprVar variable) + zero = Raw.TermExpr (Raw.ExprInteger Nowhere 0) + setNoun = Raw.Noun Nowhere Lexicon.builtinSetNoun [] + setPhrase named = Raw.NounPhrase [] setNoun named [] Nothing + quantified quantifier variable = + Raw.TermQuantified + quantifier Nowhere (setPhrase (Just variable)) + equalityVerb argument = + Raw.Verb Nowhere Lexicon.builtinEqualityVerb [argument] + equalityAdjective argument = + Raw.Adj + Nowhere Lexicon.builtinEqualityRightAdjective [argument] + equality left right = Core.CEq Core.TySet left right + notP proposition = Core.CImp proposition Core.CFalsum + andP left right = notP (Core.CImp left (notP right)) + existsP body = notP (Core.CForall Core.TySet (notP body)) + truth = Core.CImp Core.CFalsum Core.CFalsum + member left right = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) left) + right + soleSubject = + Raw.StmtNoun + (quantified Raw.Universally x :| []) + (setPhrase Nothing) + explicitSubject = + Raw.SymbolicQuantified + Nowhere Raw.Universally (x :| []) Raw.Unbounded Nothing + (Raw.StmtNoun (term x :| []) (setPhrase Nothing)) + multipleSubjects = + Raw.StmtVerbPhrase + ( quantified Raw.Universally x + :| [quantified Raw.Existentially y] + ) + (Raw.VPVerb (equalityVerb zero)) + adjectiveArgument = + Raw.StmtVerbPhrase + (zero :| []) + (Raw.VPAdj + (equalityAdjective + (quantified Raw.Universally x) :| [])) + nounArgument = + Raw.StmtNoun + (zero :| []) + (Raw.NounPhrase + [] + (Raw.Noun + Nowhere Lexicon.builtinElementNoun + [quantified Raw.Universally x]) + Nothing [] Nothing) + negatedSubject = + Raw.StmtVerbPhrase + (quantified Raw.Universally x :| []) + (Raw.VPVerbNot (equalityVerb zero)) + negatedArgument = + Raw.StmtVerbPhrase + (zero :| []) + (Raw.VPVerbNot + (equalityVerb (quantified Raw.Universally x))) + nonexistentialArgument = + Raw.StmtVerbPhrase + (zero :| []) + (Raw.VPVerb + (equalityVerb (quantified Raw.Nonexistentially x))) + negatedStatement = + Raw.StmtNeg Nowhere soleSubject + siblingConstraints = + Raw.StmtNoun + (zero :| []) + (Raw.NounPhrase + [] + (Raw.Noun + Nowhere Lexicon.builtinElementNoun + [quantified Raw.Universally x]) + Nothing + [Raw.AdjR + Nowhere Lexicon.builtinEqualityRightAdjective + [quantified Raw.Universally y]] + Nothing) + constrainedSubject = + Raw.TermQuantified Raw.Universally Nowhere + (Raw.NounPhrase + [] + (Raw.Noun + Nowhere Lexicon.builtinElementNoun [term x]) + (Just x) + [Raw.AdjR + Nowhere Lexicon.builtinEqualityRightAdjective [term x]] + (Just + (Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerb (equalityVerb (term x)))))) + constrainedStatement = + Raw.StmtVerbPhrase + (constrainedSubject :| []) + (Raw.VPVerb (equalityVerb (term x))) + xEqualsX = equality (Core.CBound 0) (Core.CBound 0) + cases = + [ ( "sole quantified subject" + , soleSubject + , Core.CForall Core.TySet truth + ) + , ( "explicit sole quantified subject" + , explicitSubject + , Core.CForall Core.TySet truth + ) + , ( "multiple quantified subjects" + , multipleSubjects + , Core.CForall Core.TySet + (existsP + (andP + (equality + (Core.CBound 1) (Core.COpaqueInteger 0)) + (equality + (Core.CBound 0) (Core.COpaqueInteger 0)))) + ) + , ( "quantified adjective argument" + , adjectiveArgument + , Core.CForall Core.TySet + (equality (Core.COpaqueInteger 0) (Core.CBound 0)) + ) + , ( "quantified noun argument" + , nounArgument + , Core.CForall Core.TySet + (member (Core.COpaqueInteger 0) (Core.CBound 0)) + ) + , ( "quantified subject outside negation" + , negatedSubject + , Core.CForall Core.TySet + (notP + (equality + (Core.CBound 0) (Core.COpaqueInteger 0))) + ) + , ( "quantified argument inside negation" + , negatedArgument + , notP + (Core.CForall Core.TySet + (equality + (Core.COpaqueInteger 0) (Core.CBound 0))) + ) + , ( "nonexistential quantified verb argument" + , nonexistentialArgument + , notP + (existsP + (equality + (Core.COpaqueInteger 0) + (Core.CBound 0))) + ) + , ( "statement recursion bounds a quantified subject" + , negatedStatement + , notP (Core.CForall Core.TySet truth) + ) + , ( "sibling constraints own their argument quantifiers" + , siblingConstraints + , andP + (Core.CForall Core.TySet + (member + (Core.COpaqueInteger 0) + (Core.CBound 0))) + (Core.CForall Core.TySet + (equality + (Core.COpaqueInteger 0) + (Core.CBound 0))) + ) + , ( "quantified noun constraints share their binder" + , constrainedStatement + , Core.CForall Core.TySet + (Core.CImp + (andP + (member (Core.CBound 0) (Core.CBound 0)) + (andP xEqualsX xEqualsX)) + xEqualsX) + ) + ] + prepare context statement = + Exact.prepareExactProposition context statement + activeContext <- expectRight + (Exact.extendExactBinderContext + ((Exact.exactLocalId 0, x) :| []) + Exact.emptyExactBinderContext) + let action + :: Declaration.ModuleDriver Text + ( [ Either + Exact.ExactCompileError + Exact.PreparedExactProposition + ] + , Either + Exact.ExactCompileError + Exact.PreparedExactProposition + ) + action = + Declaration.runProspectiveLoweringDriver do + compiled <- traverse + (\(_label, statement, _expected) -> + prepare Exact.emptyExactBinderContext statement) + cases + collision <- prepare activeContext soleSubject + pure (compiled, collision) + runDriver fixture action >>= \case + Declaration.DriverSucceeded + (compiled, collision) _interface _prefix _closure -> do + for_ (zip cases compiled) \ + ((label, _statement, expected), result) -> + case result of + Right prepared -> + assertEqual label expected + (Core.scopedCoreTerm + (Exact.preparedExactPropositionCore prepared)) + Left failure -> + assertFailure + (label <> " failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + case collision of + Left (Exact.ExactDuplicateLocalBinder _location variable) -> + assertEqual "quantified binder collision" x variable + Left failure -> + assertFailure + ("unexpected quantified-binder collision: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + Right{} -> + assertFailure "an active quantified binder was shadowed" + case compiled of + Right sole : Right explicit : _ -> + assertEqual + "sole-subject lowering remains byte-for-byte identical" + (Exact.preparedExactPropositionCore sole) + (Exact.preparedExactPropositionCore explicit) + _ -> + assertFailure + "sole-subject equality comparison did not compile" + Declaration.DriverFailed failure _prefix -> + assertFailure + ("quantified proposition-term driver failed: " <> show failure) + Declaration.DriverSealFailed failure _prefix -> + assertFailure + ("quantified proposition-term 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) + namedPredicateReplacement = + Raw.ExprReplacePred + predicateReplacementLocation + y + x + (Raw.ExprVar a) + (equality (Raw.ExprVar x) (Raw.ExprVar y)) + 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 + , Either + Exact.ExactCompileError + Exact.PreparedExactSetExpression + ) + action = + Declaration.runProspectiveLoweringDriver do + valid <- Exact.prepareExactProposition + Exact.emptyExactBinderContext + validStatement + invalid <- Exact.prepareExactProposition + Exact.emptyExactBinderContext + invalidStatement + predicateReplacement <- Exact.prepareExactProposition + Exact.emptyExactBinderContext + predicateReplacementStatement + namedContext <- + either + (impossible + . Text.unpack + . Exact.renderExactCompileError) + pure + (Exact.extendExactBinderContext + ((Exact.exactLocalId 0, a) :| []) + Exact.emptyExactBinderContext) + named <- Exact.prepareExactSetExpression + namedContext namedPredicateReplacement + pure (valid, invalid, predicateReplacement, named) + runDriver fixture action >>= \case + Declaration.DriverSucceeded + ( Right prepared + , Left failure + , Left predicateReplacementFailure + , Right named + ) _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.ExactRelationalReplacementRequiresNamedDefinition + predicateReplacementLocation) + predicateReplacementFailure + case Exact.preparedExactSetExpressionConstruction named of + Just (Exact.PreparedRelationalSetConstruction construction) -> do + assertEqual "relational replacement canonical term" + expectedRelationalTerm + (Core.scopedCoreTerm + (SetConstruction.relationalSetConstructionTerm + construction)) + assertEqual "relational replacement functionality" + expectedFunctionality + (Core.scopedCoreTerm + (SetConstruction.relationalSetConstructionFunctionality + construction)) + let relationalObject = + Identity.assertedObjectId + (opaqueFixtureObject fixture) + closedFunctionality = + SetConstruction.relationalSetConstructionClosedFunctionality + construction + relationalFact <- + maybe + (assertFailure + "exact functionality did not unlock relational extensionality" + >> fail "unreachable") + pure + (SetConstruction.relationalSetConstructionObjectFact + (SetConstruction.checkedFoundationSetConstruction + (fixtureFoundation fixture)) + relationalObject + construction + closedFunctionality) + assertEqual + "relational replacement flattened extensional proposition" + (expectedRelationalExtensional relationalObject) + (Core.frozenCoreTerm + (SetConstruction.relationalSetConstructionFactProposition + relationalFact)) + assertEqual + "unrelated functionality cannot unlock the relational view" + Nothing + (SetConstruction.relationalSetConstructionLocalViews + (SetConstruction.checkedFoundationSetConstruction + (fixtureFoundation fixture)) + construction + (Core.falsumScopedCore [Core.TySet])) + wrongClosed <- expectRight + (Core.checkCanonicalCore + (const Nothing) + Core.CFalsum) + assertBool + "malformed relational authority is rejected" + (isNothing + (SetConstruction.relationalSetConstructionObjectFact + (SetConstruction.checkedFoundationSetConstruction + (fixtureFoundation fixture)) + relationalObject + construction + wrongClosed)) + _ -> + assertFailure + "named predicate replacement lost its relational construction" + 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.DriverSucceeded + (_, _, _, Left failure) _interface _prefix _closure -> + assertFailure + ("named predicate replacement failed: " + <> Text.unpack (Exact.renderExactCompileError failure)) + Declaration.DriverFailed failure _prefix -> + assertFailure + ("replacement driver failed: " <> show failure) + Declaration.DriverSealFailed failure _prefix -> + assertFailure + ("replacement driver did not seal: " <> show failure) + where + relApp1 intrinsic argument = + Core.CApp (Core.CIntrinsic intrinsic) argument + relApp2 intrinsic first second = + Core.CApp (relApp1 intrinsic first) second + notP proposition = Core.CImp proposition Core.CFalsum + andP left right = notP (Core.CImp left (notP right)) + existsP body = notP (Core.CForall Core.TySet (notP body)) + relation = Core.CEq Core.TySet (Core.CBound 1) (Core.CBound 0) + restricted = + relApp2 Core.Sep (Core.CBound 0) + (Core.CLam Core.TySet (existsP relation)) + expectedRelationalTerm = + relApp2 Core.Repl restricted + (Core.CLam Core.TySet + (relApp1 Core.SetChoose (Core.CLam Core.TySet relation))) + expectedFunctionality = + Core.CForall Core.TySet + (Core.CImp + (relApp2 Core.Member (Core.CBound 0) (Core.CBound 1)) + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CImp + (andP + (Core.CEq Core.TySet + (Core.CBound 2) (Core.CBound 1)) + (Core.CEq Core.TySet + (Core.CBound 2) (Core.CBound 0))) + (Core.CEq Core.TySet + (Core.CBound 1) (Core.CBound 0)))))) + expectedRelationalExtensional object = + Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CEq Core.TyProp + (relApp2 Core.Member + (Core.CBound 0) + (Core.CApp + (Core.CGlobal object) + (Core.CBound 1))) + (existsP + (andP + (relApp2 Core.Member + (Core.CBound 0) + (Core.CBound 2)) + (Core.CEq Core.TySet + (Core.CBound 0) + (Core.CBound 1)))))) + +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) + internal <- + expectRight + (evalState + (runExceptT (Meaning.glossStmt statement)) + Meaning.initialGlossState) + reusable <- + expectRight + (Typed.prepareTypedClosedFormula + absurd + (const Nothing) + internal + :: Either + Typed.TypedInductiveError + (Core.FrozenCheckedCore Void)) + assertEqual + "raw and reusable finite-set lowering" + expected + (Core.frozenCoreTerm reusable) + let internalSymbols = Internal.mentionedSymbols internal + assertBool + "finite-set meaning has no source-owned cons dependency" + (Internal.SymbolMixfix Raw.ConsSymbol + `Set.notMember` internalSymbols) + assertBool + "finite-set meaning retains fixed adjunction operations" + ( Set.fromList + [ Internal.SymbolMixfix Raw.UnionsSymbol + , Internal.SymbolMixfix Raw.UpairSymbol + ] + `Set.isSubsetOf` internalSymbols + ) + case Vocabulary.classifyExactSymbol + (Internal.SymbolMixfix Raw.ConsSymbol) of + Vocabulary.ExactSourceGlobal{} -> pure () + classification -> + assertFailure + ("explicit cons did not retain source ownership: " + <> show classification) + 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 |