Every critical-behavior ID in the scope inventory maps below to its specification, proof, executing implementation, contracts, supporting evidence and remaining gap. This is an inventory of the present boundary. It does not discharge the outstanding implementation, functional or platform requirements.
Formal verification, proof documentation and the exact proof/dependency manifest define the admitted models and extraction boundary. Links to tests identify inspectable repository evidence, not an executed check for a particular revision. Execution requires a separate exact-SHA receipt and verdict. Guarded DAO skips establish no native compatibility. The validation matrix and compact evidence retain the producing-engine, fixture and operation scope of existing native observations. Synthetic round trips cannot expand that scope.
Executable means production invokes generated Dafny decisions for the named operation; the containing C# method is not thereby verified. Abstract means the theorem holds for its model transition relation. Manual/tested means source review and finite conformance or independent regression controls support correspondence without a machine-checked C# refinement. Unspecified means no admitted machine-checked specification exists for that behavior; design, safety and compatibility requirements still apply. Qualification requires independent native-engine or actual runtime/OS/filesystem/device evidence. No entry has a complete power-loss qualification receipt.
| Contract | Explicit dependency, not a proved conclusion |
|---|---|
| A1 acquisition/identity | Reported reads return their exact bytes; framing, checksum/hash and path/generation construction bind admitted records and images. Generated ranges/cursors do not prove handwritten map construction or cryptographic identity. |
| A2 effects/persistence | Successful effects have their named bytes/length result; modeled successful flushes fence exact bytes and length. Failed/partial effects grant no successful transition. Namespace discovery, directory ordering, stale-I/O quiescence and device persistence need storage qualification. |
| A3 authority/coordination | Canonical identity, fresh object/generation/ticket identities, validated receipts and exclusive cooperating acquisition remain held through cleanup. Actual composite .NET/OS exclusion and deadlock prevention require refinement; valid record bytes alone grant no lease. |
| A4 native representation | Page/tag/token/row/field/key/collation meanings match supported native forms. Microsoft fixtures, independent byte inspection and successful named DAO operations are separate evidence. |
| A5 resources/ownership | Borrowed bytes stay stable until release; locator/pool/destination ownership and admitted aggregate work/storage bounds hold. CLR overhead, shared pools and caller resources need separate scope. Logical snapshot/allocation effects do not prove C# bookkeeping. |
| A6 compilation/runtime | Reviewed Dafny/Z3, projection including the three exact-signature controller inlining annotations, C# compiler and .NET JIT/AOT preserve generated semantics. The trust policy binds reviewed content; hashes attest freshness, not reviewer judgment, tool soundness or specification adequacy. |
Row-read admission and trailer geometry execute through RecoveryKernel in
scans, counts, POCO and index paths. OverflowRowTests and
RowReadAdmissionKernelTests supply independent strict refusal, explicit lenient
warning/accounting and native-width geometry controls. Linked omission accounting
shares the root reader’s counter. Row acquisition, C# call-site composition and
physical map completeness retain their separate parser/ownership obligations.
PageDigestKernel adds executable digest-slot admission and failure-atomic byte
replacement to the J1/J5 framing boundary. FilePageDigests and
StreamPageStore retain raw digest metadata under one exclusive writer and
invalidate reuse after uncertain effects, sparse gaps or length extensions. JournalDigestReuseTests
compares commitments with independently framed physical images through overwrite,
sparse append, shrink, live rollback and a torn-write failure. Complete ledger
correspondence, SHA-256, returned I/O effects and namespace/storage qualification
remain separate obligations; recovery independently acquires physical content.
| ID | Specification/proof and executing implementation | Evidence, dependent contracts and remaining gap |
|---|---|---|
| C1 | Unspecified; manual/tested. DatabaseCreationPublication privately initializes staging before publication; file/stream creation have separate lifecycles. No creation controller is in the proof manifest. | CreationCrashRecoveryTests terminates initialization/publication, including competing destinations. A2/A3/A4/A5. Specify/refine cancellation, failed publication, competition and cleanup; extend caller-stream creation fault sweeps (I5/V6/V12). Process kills do not qualify namespace persistence (E4/I15/V7). |
| J1 | Abstract + executable framing; manual full preparation. UndoJournal BufferedTracePreserves/SuccessfulFlushFencesPendingEffects; RecoveryKernel JournalManifestIsExactBoundedPageRounding/JournalFramingSelectsExactCompletePrefix. PersistentRollbackJournal Create/preparation promotion and PhysicalRollback BeginWrite use bounded framing. |
PersistentRollbackJournalTests, SelectiveRollbackJournalTests, RecoveryKernelTests. A1/A2/A3/A6. Bind actual manifest/tag/hash acquisition, creation/flush/promotion outcomes and retained preparation evidence to constructed payloads (V3/V6). Discovery after namespace loss remains unqualified (I15/V7). |
| J2 | Abstract preparation + executable selectors; manual full path. UndoJournal CaptureAlignedPageRange, PreparePageWrite, PreparePageTruncate, PrepareContentWrite, PrepareContentTruncation; RecoveryKernel TruncateCoverageAdmissionRefinesSaved/original-page slices. StreamPageStore observers call journal RecordBeforeWrite/RecordBeforeTruncate before effects. |
SelectiveRollbackJournalTests, BufferedJournalConformanceTests, ShrinkCrashRecoveryTests: missing/late captures, partial pages, sparse gaps and torn tails. A1/A2/A4/A6. Compose serialized acquisition/map/hash identity with coverage and content admission. PreparedReorderingCounterexample retains a safe-refusal survivor: exact undo alone does not prove zero-gap admission (V3/V6/V7). |
| J3 | Executable admission-state controller, framing/classification/authorization; manual acquisition/effects. RecoveryKernel JournalRecordClassificationIsExact, ReplayStateRefusesFurtherMutations, JournalRecordCursorMakesBoundedProgress, ByteAuthorizationRefinesUndo; UndoJournal RecordedAdmissionIsAuthorization, ContentBufferedTracePreserves, SerializedInventoryPreflightEstablishesEquality. Journal ValidateCurrentContent executes generated original/replay-zero, after-image, final-admission and zero-extension array scans. ValidateJournal executes AdvanceJournalAdmission/CompleteJournalAdmission for the scalar admission fold under exact capture/hash/tail outcomes. Record acquisition/hashing, dictionary effects and ValidateReplayInventory retain handwritten composition. |
JournalAdmissionKernelTests, JournalContentKernelTests, JournalReplayInventoryTests, SelectiveRollbackJournalTests, BufferedJournalConformanceTests: altered maps, checksum-valid changed originals, omitted evidence and no-write refusal. A1/A2/A3/A6. Prove raw acquisition constructs admitted tag/hash/inventory premises through complete-invalid, truncated, conflicting, duplicate, partial-read and cancellation paths (V3/V6/V8). Internal-map controls are not external exploit evidence. |
| J4 | Executable replay decisions + abstract effects; manual complete recovery. RecoveryKernel JournalReplayActionRefinesProductionOrder/ReplaySelectionRefinesExactInventoryPayload; UndoJournal CompletePageReplayControl, SerializedPageSelectionConsumesInventory, CompleteSerializedPageReplay, AcknowledgedBufferedImageSurvivesMixedTrace, FailedCommitCannotRollbackInPlace. Journal Recover, RestoreAsync, conditional recovery marker, Complete and CleanupCompleted execute the effectful schedule. |
RecoveryReplayCrashTests, TransactionCrashRecoveryTests, BufferedJournalConformanceTests, CommitFaultSweepTests. A1/A2/A3/A6. Compose J1–J3, effect outcomes, marker retries, acknowledgement and exact cleanup authority (V3/V6/V10). Rank counts successful abstract actions, not all syscalls or infinite failures; physical ordering/quiescence remains I15/V7. |
| J5 | Abstract lifecycle effects; manual physical implementation. WriterLifecycle assumes complete snapshots/restoration; the undo model separately covers its persistent-file protocol. PhysicalRollback, PagerTransaction, WriteScope own memory/spill captures, journal attachment, commit/restoration and detachment. | FileRollbackTests, StatementSpillTests, PageStoreTests. A1/A2/A5 and caller-owned stream exclusion. Refine capture/spill ownership, partial effects, failed restore and disposal (I5/V6/V10). Persistent stream identity/discovery/reopen/fence/quiescence/lease capabilities remain unimplemented I15 requirements, not consequences of live rollback. |
The directory-order refinements in GenerationOwnership and
ReplacementProtocol gate preparation authority and copy/native/receipt/intent
retirement on named acknowledgements. DirectoryPersistence supplies the narrow
Windows adapter in the net11.0 asset; unsupported assets/platforms grant no
acknowledgement. DirectoryPersistenceTests, publication and cleanup conformance
controls bind the source ordering and suppressed-error refusal. Actual C# effect
composition, lost names and filesystem/device power-cut qualification remain
separate A2/A3/E4/F6/I15/V7 obligations.
| ID | Specification/proof and executing implementation | Evidence, dependent contracts and remaining gap |
|---|---|---|
| R1 | Executable field scans/admission + abstract evidence composition. RecoveryKernel CheckReplacementHeader, CheckReplacementDecision, bounded length/read controls and refinement lemmas; ReplacementProtocol BytesRefineEvidenceAdmission, PartialDecisionCannotCommit, CompleteDecisionRequiresEveryCheckedField. EncryptionReplacementIntent ReadState invokes these before bootstrap. |
ReplacementKernelTests, ReplacementFieldConformanceTests, ReplacementIntentTests. A1/A2/A3/A6. Compose actual bytes, digest/path/GUID identity, immutable-copy admission and lease authority through the complete controller; valid prefixes/records cannot independently authorize ownership (V5/V6/V10). |
| R2 | Abstract copy/refinement; manual production effects. ReplacementProtocol CopyTracePreserves, CompleteCopySchedule, FencedCopyPublicationRefines, CompleteSelectedCopyRecovery, FiniteCopyFailuresAllowSelectedRecovery assume image and staging-persistence contracts. Intent Copy, CopyReplacement and old/new/publication staging consume conversion from EncryptionConverter. |
ReplacementCopyConformanceTests, ReplacementPublicationConformanceTests. A1/A2/A3/A4/A5/A6. Refine copy/hash identity, complete preparation/retry and failed/partial native syscalls; before/after callback exceptions do not determine physical survivors (V5/V6/V7/I5). Native encryption variants/providers remain F3 and matrix-scoped evidence. |
| R3 | Abstract selection/publication/cleanup refinement; manual complete flow. ReplacementProtocol ReturnedCommitSurvivesRecovery, InterruptedRecoveryKeepsDecision, PublicationFenceTracePreserves, FailedDestinationFlushRetainsEvidence, ProductionCleanupTracePreserves, ProductionDeletionRequiresSelectedLease, CompleteFencedSelectedProductionRecovery. Intent Commit, ValidateState, ValidatePublication, Publish, Recover, Cleanup; AccessDatabaseEncryption calls replacement. |
ReplacementPublicationConformanceTests, ReplacementCleanupConformanceTests, ReplacementCrashRecoveryTests, ReplacementNamespaceModelTests. A1/A2/A3/A4/A6. Compose R1/R2/O1/O2, failed bootstrap, commit uncertainty and every effect outcome (V5/V6/V10). Selected-copy/lease/flush remain premises; missing-name metadata and physical namespace durability remain F6/E4/V7. |
| O1 | Abstract staged authority; manual C#. GenerationOwnership CompletedBootstrapEstablishesAuthority, IncompleteBootstrapRefusesAuthority, FailedBootstrapRetainsEvidence, StaleOwnerCannotDelete, RepeatedDisposePreservesSuccessor, CompleteGenerationCleanup; MultiProcessOwnership adds tickets. RecoverableWriterLock AcquireRecovery, receipt/native checks and recovery/ordinary disposal implement distinct schedules. |
RecoverableWriterLockTests, RecoveryLockFileTests, ReplacementCleanupConformanceTests. A1/A2/A3/A6. Refine receipt codec, identity, acquisition failure/reconstruction and cleanup. Partial acquisition may require refusal; GUID freshness/canonical identity are contracts, not theorems about real names (V5/V10). Namespace qualification remains E4/F6/I15/V7. |
| O2 | Abstract multi-client exclusion; manual composite locks. MultiProcessOwnership TracePreserves, AtMostOneCoordinatedClient, MissingNamesDoNotAuthorizeSuccessor, StaleTicketCannotAct, fresh/recorded acquisition and successful-cleanup lemmas assume atomic canonical Coordinate. Intent/ownership composite acquisition, LockFileCoordinator teardown and JetByteRangeLock supply effects. |
CrossProcessLockTests checks child-process ranges on supported hosts and explicitly disabled macOS BCL ranges. Cleanup conformance separately checks competing handles while names disappear. A2/A3/A5/A6. Refine missing/existing-destination intent/native/source leases and ordinary post-database-close disposal; prove deadlock/rank and fairness separately. Same-process competing handles do not qualify whole composite cross-process/macOS exclusion or arbitrary namespace attacks (V10/V7/E4). |
| ID | Specification/proof and executing implementation | Evidence, dependent contracts and remaining gap |
|---|---|---|
| P1 | Executable shared primitives; unspecified/manual containing parsers. RecoveryKernel ByteRangeIsExactAndOverflowSafe, NestedByteSlicesCompose, BufferReadMakesExactProgress, ExactReadTraceAcquiresRequestedPrefix. BinaryBuffer, StreamRead, StreamPageStore and header/page/pointer callers use them. |
SharedParsingKernelTests: wide arithmetic, pointer overflow, short-read partitions, EOF/cancellation/errors/invalid counts; PageStoreTests: capabilities. A1/A4/A5/A6. Compose bounds before acquisition/allocation, format admission, failures/cancellation and aggregate resources across public sources. Real unsupported generations must not alias supported profiles (S1/E1/V8). |
| P2 | Unspecified containing metadata parsers; executable shared bounds where called. Definition metadata, catalog design, compact recovery state contracts. TableDefReader, LogicalTDefChain, catalog readers, CompactCatalogRecovery, CompactActiveCatalogRows remain handwritten. | CatalogTraversalCorruptionTests, CatalogSchemaBudgetTests, ColumnPropertyBlockTests, CompactCatalogRecoveryTests. A1/A4/A5/A6. Prove complete bounded traversal/count consistency, lossless authoritative identity admission and aggregate resources. Physical/Id/ParentIdName corroboration does not establish completeness after all evidence is damaged; populated pool binding still lacks native-accepted evidence (S1/S4/I17/V8). |
| P3 | Executable bounded slot acquisition and Jet3 jump controls; unspecified public row/overflow/scalar controller. Row-format notes define representation; shared bounds/LVAL decisions apply only where invoked. DataPageRows.TryGetSlotBound invokes generated ReadDataRowSlot: complete bounded header/directory acquisition and exact least greater masked offset, including deleted/duplicate slots. Jet3 span adapters execute generated sizing, dummy and monotone boundary decisions; their loads/stores and complete row acquisition remain explicit contracts. Other directory builders, TableReader, RowDecoder and typed/string/POCO controllers remain handwritten. Jet3JumpTableKernelTests pins sizing, boundary/dummy behavior and the dense 255-offset native-capacity specimen. DataRowSlotKernelTests supplies independent success/refusal and interval controls. |
OverflowRowTests, OverflowPayloadAliasTests, FixedSlotBoundsDecodePolicyTests, VariableSlotBoundsDecodePolicyTests, MalformedRowTraversalWriteBackTests, RowValueDecodePolicyTests, CalculatedLongValueDecodePolicyTests: complete calculated-envelope overhead, payload/trailer separation, public fault policy and no-loss write refusal. CalculatedColumnPayloadTests and CalculatedNumericDecodePolicyTests pin the covered Microsoft-authored envelope controls. CalculatedByteErrorReadTests constructs the measured native Byte error layout and checks distinct error values across public typed/string/DataTable reads, incompatible scalar POCO conversion, ordinary Null/Byte controls, malformed framing and repair updates. NativeCalculatedErrorTests adds independently authored source/compacted status fixtures, native recalculation and exact scalar error widths. CalculatedNumericNativeLayoutTests qualifies fixed-offset Decimal words, reserved leading words, zero-fill and Null framing. NativeDateSerialTests preserves exact raw Date serials through write-back. A1/A4/A5/A6. Specify/compose every surface’s slot/overflow/type/envelope/error admission, strict context, lenient representation/diagnostic, raw write-back preservation and actual I/O propagation. Remaining controller/resource/native-format composition remains S1/S3/F8/R4/V8 work. |
| P4 | Executable full descriptor codec/admission/pointer packing and visited-set count/growth orchestration; array-backed controller-connected chain schedule/manual public effect composition. LongValueKernel ReadDescriptor, WriteDescriptor, CompleteDescriptorRoundTrip, DescriptorAdmissionIsExact, DescriptorRefusalPriority, RowPointerRoundTrip, ChainPayloadMakesBoundedProgress, ContainsVisited, AddVisited, RehashVisited, PrepareVisitedAdd, CompleteVisitedGrowth, EncodeAbstractVisitedDecision, ValidVisitedDecisionHasExactClassification and the TrackedVisited invariant; LongValueTraversal Traverse and circular-probe/resource contracts. LongValueDescriptor, LongValueStore, LongValueVisitedSet invoke generated decisions. |
LongValueDescriptorKernelTests, LongValueTraversalTests, LongValueStreamingTests, LongValueStoreTests: codec, collision/growth/cycles/no-progress/cancellation/partial-output/release controls. CalculatedLongValueDecodePolicyTests also checks envelope framing and no-loss refusal for inline, single-row and chained Memo/Binary/OLE values. CalculatedBinaryResultTests qualifies calculated Binary/OLE storage selected by hydrated result type, native scalar bytes, per-column allocation/reclamation, rollback and native error repair/compact. A1/A4/A5/A6. Compose generated visited-set orchestration with actual allocation/adapter effects, retained matching array/count state and the containing public parser, locator/cache/pool/destination resources and native token/ownership meaning. Aggregate adversarial probe work and cancellation latency remain open. Array-payload bounds exclude CLR overhead/independent resources. Inline/single-page and large native values have separate gaps (S1/S3/F8/V8). |
| P5 | Generated full-key and bookmark mutation admission is scoped in value/resource/mutation admission, with InPlaceRowUpdateTests as production conformance. Executable index boundary/child-selection/emission controls and usage-bit access/enumeration; unspecified containing traversal. Index/relationship notes, usage design, complex design. IndexPageCodec invokes generated FindIndexEntryStart and CheckIndexLeafBitmap for exact bounded next-entry/sentinel scans, plus generated intermediate-entry admission, child selection and canonical pointer controls around the existing vectorized lexicographic comparison. UsageMap invokes generated inline/reference admission and exact array bit reads/updates, with preservation outside the selected bit and atomic refusal. IndexChildSelectionKernelTests covers compressed bookmark/pointer prefixes, vector-width boundaries, unequal key lengths, zero/full-width child identities and zero allocation. IndexEntryBoundaryKernelTests and UsageMapBitmapKernelTests cover independent bit/boundary oracles and malformed input. UsageMapKernel executes the ordered bitmap scan for INLINE and REFERENCE maps with exact byte-mask membership, ordered progress and strict in-byte prefix refusal contracts; UsageMapEnumerationKernelTests supplies independent scan and reference-effect controls. IndexCursor, complete key/node decoding, reference-pointer acquisition/return, complex readers and compact audits retain handwritten composition. |
IntermediateIndexCycleTests, IndexLeafChainConsistencyTests, UsageMapBitmapEnumerationTests, ComplexColumnCatalogValidationTests, AttachmentResourceLimitTests. A1/A4/A5/A6. PublicTextCollationTests checks public encoder-family choices, raw metadata, preallocation refusal and schema preservation; PublicTextCollationDaoTests covers native seek/uniqueness/mutation/compact for Jet3 General97 and Jet4 General Legacy via DAO3.6 and all four public Jet4/ACE choices plus compacted header-default rebuilding via DAO120. These tests do not expand key algorithms or establish broader locale/native coverage. Specify/prove complete roots/directories/nodes/key/row traversal, counts, cycles, ownership, native collation and aggregate resources through public scans (S1/S3/F9/V8/V9). |
| P6 | Unspecified compound/OLE/external-source parsers and capability policy. CompoundFileReader, encrypted-package/OLE paths and linked-file/ODBC/text capability resolution are handwritten; bounded internal slice calls do not verify their surrounding protocols. | CompoundFileHeaderTests, AttachmentCorruptionTests, LinkedSourceSecurityTests, LinkedSourceCapabilityTests, LinkedTextSourceStreamTests. A1/A3/A4/A5/A6. Specify/prove compound directory/FAT/stream bounds, real provider contracts, OLE/envelope policy, external path/capability isolation, delimited parsing/resources and cancellation (S1/S3/F3/F8/E1/V8/V12). |
| ID | Specification/proof and executing implementation | Evidence, dependent contracts and remaining gap |
|---|---|---|
| B1 | Executable complete-entry completion with an explicit vectorized key adapter, leaf-chain/neighbor and relationship admission, and page emission; unspecified containing structural edits. IndexMutationKernel executes prefix, capacity, header, bookmark/child, boundary and sentinel/free-space emission; IndexPageEmissionKernelTests compares complete independent byte images. Exact key-suffix bulk copies and list/layout inputs remain contracts. Index/relationship design states native forms; no B-tree edit module is admitted. IndexTreeInventory acquires captured physical membership and invokes generated leaf-chain admission before effects. IndexBTreeEditor, IndexEntrySplicer, IndexBTreeBuilder, IndexMaintainer choose incremental/splice/rebuild/fallback paths. | IndexSurgicalRootSplitTests, IndexSurgicalRecursiveIntermediateSplitTests, IndexSurgicalLeafMergeTests, IndexIncrementalMaintenanceTests, IndexBTreeStructuralFixtureTests, IndexEntryOrderingTests: native bookmark ties, ordered/unordered splice runs, untouched inputs and one-buffer allocation controls. IndexNeighborOwnershipTests checks foreign-table and same-table-other-index refusal before staged writes plus exact statement rollback. DuplicateBookmarkOrderingTests, RelationshipIndexAdmissionTests and ForeignKeyIncrementalEvidenceTests exercise native duplicate ordering, exact-map refusal and the admitted Int32 relationship subset. A2/A4/A5 and L1/J5 rollback. Specify/prove ordered multisets, separators, encoding, row identity, occupancy, ownership, all root/edit/fallback paths and allocator/codec composition. Retain rebuilds outside the admitted fixed Int32 relationship subset; complete tree/map acquisition and O(n log n) sorting/membership remain and do not prove full tree topology or native collation (I2/F9/V9). |
| B2 | Executable row-compaction admission/directory rewrite; unspecified allocation/page reclamation. DataPageKernel and DataPageReclaimKernelTests cover row-space bounds, exact directory updates and modeled byte preservation under explicit overlapping copy/clear effects. Stable page/layout identity and statement rollback remain contracts; row-space compaction grants no page-release authority. Global allocation and compact contract require conservative ownership. PageAllocator, UsageMapOwnership, UsageMapEditor, tree reclamation/shrink paths have no admitted ownership proof. | IndexTreeReclamationTests, UsageMapOwnershipTests, UsageMapNonliveAliasTests, PageAllocatorStateTests, SurgicalReservationFailureTests. A2/A4/A5 and J/L rollback. Prove freed pages disjoint from reachable and potentially referenced pages, including opaque references, all maps/index owners and cross-TDEF references; incomplete enumeration cannot establish exclusive ownership. Compose allocator rollback/descriptor renumbering (I2/I5/I17/V9). |
| B3 | Generated ordinary value-width admission and matching-only mutation snapshots are scoped in value/resource/mutation admission, with VariableValueWidthTests and snapshot diagnostics. Unspecified mutation semantics; abstract lifecycle assumes complete statements. WriterLifecycle does not verify validation/cascade/schema/relationship/complex algorithms. Calculated, complex, index/relationship design contracts apply. TableSchemaEditor, schema/TDEF writers and relationship/complex coordinators run under TransactionLifecycle. Logical row effects share MutationPlan and MutationExecutor, with whole-plan row-encoding preflight and explicit native index policies; their algorithms and rollback correspondence remain handwritten. | MutationPipelineTests covers composed self-cascade and complex changes, byte/identity rollback and whole-plan preflight refusal. SchemaRewritePropertyPreservationTests covers exact display and lookup property preservation through column edits and table deletion, including repeated and opaque source entries; NativeLookupPropertyTests checks raw lookup properties and native QueryDef type/SQL through native/writer column edits, referenced-table deletion, reopen and compact. Pinned DAO3.6 specimens compare complete query rows, exact query catalog values and query-specific permissions after managed edits in every writer mode. Direct/chained sources, parameterized SELECT, UNION, crosstab and stored append/update/delete/make-table definitions remain unexecuted (Jet3/Jet4 DAO3.6 and the selected fresh ACE DAO120 controls are recorded in the native validation matrix). NativeSqlSpecificQueryPreservationTests adds pinned Jet3/Jet4 stored DDL and row-returning/action pass-through forms, exact query/catalog/permission membership, long properties, connection flags, native/writer edit and compact controls and a deliberate DSN-change negative control. Stored definitions and connections remain unexecuted; ACE/UI variants remain separate; NativeDisplayPropertyTests compares Jet3/Jet4 DAO3.6 and ACE DAO120 controls and writer subjects through reopen and compact, RelationshipSchemaRewriteTests, ForeignKeyCascadeUpdateTests, ComplexItemMutationTests, NativeSchemaDaoTests, ComplexItemMutationDaoTests. A2/A4/A5/L1. TableRenamedQualifiedExpressionTests and QualifiedExpressionReferenceTests cover declaration refusal and unchanged bare binding. CalculatedStaleCacheTests independently compares retained old caches, absent new slots, dependency status -5617 and Required/field/table-rule outcomes. Absent cache markers have no invented native status or encoded error frame; ordinary calculated Null emits a complete 23-byte envelope. CalculatedExpressionBindingTests and CalculatedDeclarationAdmissionTests qualify dependency/type/cycle prebinding and native declaration refusals before mutation. CalculatedColumnWriteTests covers recomputed caller-supplied caches, completed-row validation and direct/transactional writes. Native Date, Numeric and Text storage projection retain exact row values; calculated Binary/OLE use native Variant bytes and existing long-value codecs. CalculatedMathDomainTests, CalculatedNumericComparisonTests, CalculatedLogicalOperandTests, CalculatedExpressionCurrencyTests, CalculatedExpressionRoundTests and CalculatedNativeDateExpressionDaoTests compare independent native values, subtypes, cached statuses, writer/native updates and compact. CalculatedExpressionFloatingSubtypeTests, CalculatedExpressionNumericLiteralTests, CalculatedExpressionDecimalCoercionTests and CalculatedExpressionDecimalPromotionTests retain separate shared/default/query controls and explicit OLE coefficient/scale conversion. Their native function/literal/storage evidence does not prove whole-expression or whole-statement refinement. CalculatedRegionalProfileTests and CalculatedCultureIsolationTests compare independent native Windows user profiles, complete retained caches, regional snapshots and concurrent writers. CalculatedOperatorStatusTests pins native unary subtype/error and membership coercion/order controls. CalculatedBooleanComparisonTests and CalculatedBooleanTextTests independently distinguish Boolean comparison/Asc projection from Str and other string conversions. Native membership provenance controls cover selected IIf branches and signed-literal syntax. These remain tested handwritten semantics; general shared expression contexts and broader caller-field/storage qualification retain their R4/E2 obligations. FixedNullScalarTests covers full fixed-slot reservation and unchanged oversized-row refusal before LVAL allocation; NativeFixedNullScalarTests compares DAO3.6 Jet3/Jet4 and DAO120 Jet4/ACE scalar geometry through managed/native mutations and compact. NativeDroppedNullSlotTests pins four DAO3.6-authored Jet3/Jet4 source/compacted fixtures and runs fresh DAO3.6 Jet3/Jet4 and DAO120 Jet4/ACE controls with dropped leading/middle/trailing fixed fields and a dropped variable field beside Null Double/GUID values. Independent native old/new/compacted geometry and public typed/string/POCO reads, insert/update and DAO reopen/update/compact qualify those shapes. Numeric/Large Number/DateTime Extended and remaining dropped-slot variants remain F8/E2 gaps. NativeMemoCompressionTests compares the bounded compression-enabled leading-marker escape with frozen DAO120 payloads and fresh DAO3.6 Jet4 and DAO120 Jet4/ACE read/update/compact controls; other short forms refuse. NativeCompressedTextMarkerTests pins descriptor/raw native-row evidence and tests the bounded ordinary compressed Text escape with an optional contiguous nonsurrogate wide prefix (nonzero low bytes), minimum Latin-1 tail, whole-value limits and contextual no-allocation refusal. Fresh DAO3.6 Jet4 and DAO120 Jet4/ACE authoring matches complete payloads before/after compact at prefix/tail boundaries, followed by writer read/update/compact; remaining ordinary character forms remain separate. NativeApplicationObjectPreservationTests checks both pinned inert ACE fixtures through public row/column/table edits in every write mode, complete unedited catalog/storage values, all original MSysACEs row values, selected owning TDEF/data/index pages, stable-object LVAL descriptors and exact reachable external LVAL rows with native framing and chain termination. The native validation matrix owns current DAO120 public-mutation/compact evidence; physical shared ACL pages and broader LVAL/security variants retain their separate scope. Specify/prove preflight/apply/index composition, raw unassigned preservation, counters/hints/catalog/cache rollback and unknown dependency preservation/refusal (R4/S3/S4/S9/F8/I5/I6/V9/V10/V12). |
| B4 | Unspecified compact/repair; manual/tested private assembly. Managed Compact & Repair defines bounded private copy and independent validation, not a completed public API. CompactDiscoverySession, CompactPinnedDatabaseBuilder, CompactPinnedDatabaseValidator, CompactEncodedDatabaseCopy, raw builders/validators and ledger I/O remain handwritten; generated monotone relocation admission/search is specified separately below. | CompactPinnedDatabaseCompositionTests, CompactPinnedDatabaseValidatorTests, CompactEncodedDatabaseCopyTests, CompactRawDataLongValueValidatorTests, CompactIndexRowAuditTests, CompactEncodedDatabaseNativeTests. A1–A5; publication also R/O. Prove complete inventory/reference/key-row/relocation/preservation/destination/reclamation composition. Pinned assembly/allocation coverage is not compact/repair. Complete healthy/damaged native comparisons and recovery diagnostics before authorized source replacement (I17/V8/V9/V12 and its named dependencies). |
| L1 | Abstract serialized lifecycle; manual C#. WriterLifecycle StepPreserves, TracePreserves, ResolutionRequiresInnermostToken, DepthLimitsRefuseWithoutResolution, SurvivingScopeSnapshotIsImmutable, RollbackRestoresExactScopeSnapshot, FailedStatementPreservesScopeAndSnapshot, FaultedResolutionEndsScope, CompleteWriterDisposal. Transaction lifecycle, JetTransaction, PagerTransaction, LockFileCoordinator implement serialized begin/resolve/savepoint/restore/detach/disposal. |
WriterLifecycleConformanceTests, NestedTransactionTests, TransactionRollbackStateTests, StatementAtomicityTests, shared statement fault sweep through Jet3, Jet4 and ACE partitions, JetTransactionTests; lifecycle design maps exact outcomes. A2/A3/A5/A6. Refine semaphore/reentry/cancellation, identities and async teardown; compose actual recovery/snapshot outcomes. Proof begins after serialized acquisition and assumes counter headroom; arbitrary concurrent C#/infinite generation availability remain unproved (I5/V6/V10). |
| L2 | Generated bounded count reservation and the abstract aggregate frame bound are scoped in the frame contract, with ReaderPageCacheAdmissionTests, Include budget controls and weak type-lifetime controls. Abstract frame ownership and generation retention; manual C# correspondence. PageFrameOwnership StepPreserves, TracePreserves, live-pin/final-return, idempotence, overflow/generation refusal and producer-handoff lemmas specify the bounded immutable frame ledger. Retained/unretained success witnesses supplement refusal. WriterLifecycle InvalidatedReadCannotRetain excludes stale cache publication. PageFrame, PageLease, Pager, ReaderPageCache and scan/seek/overflow/LVAL ownership remain handwritten; see the ownership boundary. |
PageLeaseTests, AccessReaderLeaseTests, PagerFrameCacheTests, AccessReaderCacheTests, PagerTransactionSavepointTests, RepeatedReadCacheTests, SchemaCacheCoherenceTests and LongValueStreamingTests retain the lifetime and snapshot evidence. QueryLambdaCompilerTests, QueryOperandEvaluationTests and QueryPipelineParityTests cover bounded templates, live captures, operand timing and shared ordering; complete query semantics remain tested; scalar seek/order admission has the separate proofs below. A3/A5/A6. Refine actual CAS/cache locks, frame/array identity, producer transfer, pool/decoder discipline and complete public lifecycle composition; complete aggregate accounting and restored-cache correspondence (I7/S1/V8/V10). Performance acceptance separately requires paired hosted benchmarks. |
OrderStage executes IndexMutationKernel.AdmitIntegerOrdering using the actual
native and mapped integer domains, and AccessQueryProvider.TryExecuteExtremeRowAsync
reuses that single-column admission for unfiltered root MinAsync and MaxAsync
selectors (reading the first row or the terminal leaf entry via IndexRowReader.TryReadLastIndexRowAsync).
AdmittedIntegerMappingPreservesOrder proves
exact value, equality and strict-order preservation across admitted identity and
widening conversions; checked counterexamples expose narrowing order reversal.
The ordering parity tests
and index streaming tests
exercise casts, overflow, mapped Text, mapper effects, integral endpoints, paging
and bounded-byte MinAsync/MaxAsync reads across ascending and descending unique
required indexes.
The containing C# guard requires exact or admitted widening conversions for every
bound ordinary scalar property, retaining coercion failures through the sorting or
full-scan folding path.
Complete unique nonnull index admission and the mapping/type/accessor checks remain
handwritten adapters under A4/A6; full query planning and native index correspondence
retain I9 and the existing independent native evidence requirements.
Pure query planning retains priority 2 and I9. IndexSeekFilter executes
RecoveryKernel.IsOutwardSeekBound and IsFloatingZeroSeekBound; quantified
order/rank lemmas retain every original match for their admitted comparisons.
IndexSeekRoundingTests
checks independent encoded-key results for supported orders and both Decimal forms;
TypedMappingCoercionTests
compares public indexed reads with full scans, including both signed zeros.
CLR conversion/comparison, native order, complete predicate/planner semantics
and endpoint-rewriting optimizations remain explicit A4/A6 and I9 boundaries.
B4 includes generated monotone relocation admission and exact binary-search
controls in CompactRowRelocationMap, backed by IndexMutationKernel’s
injectivity/order, preserved-search-interval, halving and exact-found lemmas.
CompactRowRelocationMapTests
checks native bookmark endpoints, an independent sparse dictionary, logarithmic
record reads, alias/order refusal and immutable-key preservation. The stream’s
exact reads/exclusive immutability remain A1/A5 contracts. Neither these local
decisions nor complete ledger membership establishes complete rooted references,
native row/key correspondence, reclaim authority or compact publication.
R3’s ProductionCleanupAuthorityTrace and
InterruptedProductionCleanupAllowsCompletion connect finite actual-order
cleanup interruptions to a constructive successful continuation, retaining the
selected image and decision through recorded/fresh generation reacquisition.
The repeated-restart cleanup regression checks surviving receipts, absent-name
reconstruction, live exclusion and successor admission. Complete C# flow and
bootstrap/I/O/OS/persistence contracts retain R1/R2/O1/O2 and A1–A4/A6.
Journal closure requires C1/J1–J5 with O1/O2 and L1/L2 through actual acquisition, admission, effect outcomes and acknowledgement. Replacement requires R1–R3 with O1/O2 and real copy/crypto/flush/name effects. Parsing requires P1–P6 through complete public entry points, resources and native forms. Structural edits and compact/repair require B1–B4 with complete source/reference evidence, mutation rollback and validated publication.
No testing-only critical behavior is silently excluded. V3/V5/V6/V8/V9/V10 retain implementation obligations; V7/E4/F6/I15 retain environmental qualification; V12 retains specification adequacy, full composition and architecture/trust review. Independent native/functional requirements remain open. The continuing review policy governs map/contract/evidence changes. The additional surfaces classified in the scope inventory retain their stated priority and functional acceptance requirements even where no dedicated proof project is scheduled.