This inventory defines the production scope of the formal-verification workstream. Each ID includes its alternate, refusal, failure and retry paths. Listing a behavior does not establish its proof, native-format completeness or platform qualification. The evidence map records those separate evidence levels against the same IDs. The formal boundary describes existing theorems; PLAN.md retains unfinished implementation and acceptance work.
Priorities order work rather than exclude requirements. A shared-helper proof does not close its callers, and a successful path does not close a fallback. Newly discovered paths must join this inventory before a coverage claim expands. Review this scope with the source-domain classification below and the continuing review policy.
Each behavior requires bounds before allocation/slicing/narrowing, exact identity and ownership checks, unrelated-content preservation, honest error/cancellation reporting and correct resource release. Mutations must prepare and validate before effects, retain evidence on uncertain outcomes and avoid reclaiming reachable or potentially referenced storage. Refusal must preserve the promised source/evidence state; it cannot replace support for valid input.
Progress is separate: finite valid supported inputs within explicit budgets must complete under eventually successful I/O, exclusive access where required and fair cooperating-client scheduling. Reads terminate or observe cancellation. Mutations and recovery need reachable successful completion paths. Infinite interruptions, permanent I/O failures or clients that never release locks do not imply eventual success. Current abstract progress proofs do not prove every handwritten production loop or deadlock freedom.
Native scope includes recognized Jet3 .mdb (2,048-byte pages), Jet4 .mdb and ACE .accdb (4,096-byte pages), with the variants implemented by the named paths. Recognition does not imply complete feature coverage. Pre-Jet3, unknown descriptors/collations/providers and opaque references retain E1/E2/F3/F8/F9/S1/S3/S9 requirements: safe refusal/preservation is in scope even when interpretation/writing is unsupported. Microsoft-authored/native-accepted observations, synthetic malformed inputs and library round trips are distinct evidence.
Recovery formats are library sidecars, not native Access logs. Recovery operates on raw bytes, including encrypted images; page codecs and format semantics have separate contracts. Native Jet3/Jet4 RC4 and implemented ACE Standard/Agile forms do not establish third-party provider or Office package support. Native Access does not replay this library’s sidecars.
Execution scope covers shipped netstandard2.1 and net11.0 assets, CI’s .NET 10/.NET 11 execution and Windows/Linux/macOS paths. The following remain explicitly qualified contracts:
| Boundary | Alternatives and required qualification |
|---|---|
| Storage effects | Short reads, EOF, throwing reads, full/partial failed writes, length changes, successful/failed flushes, disposal and older queued I/O. Exact bytes-and-length fencing and crash quiescence are assumptions. Pre-marker buffered zero exposure remains V3/V7. |
| Interruption | Process failure/repeated replay differs from power loss, media corruption or adversarial namespace edits. Content flush does not persist directory entries. E4/F6/I15/V7 retain OS/filesystem/device and physical interruption qualification. |
| Coordination | Canonical paths, native/receipt/intent/source leases and exclusive cooperating clients. macOS disables BCL byte-range locking. Windows/Linux evidence does not qualify macOS, SMB, alias paths, noncooperating Access or hostile namespace changes. |
| Caller streams | Production selects persistent recovery for supported FileStream paths. Other seekable streams/memory stores/temporary undo spill provide live rollback, without persistent-adapter guarantees (I15). Caller-owned outputs/callbacks require separate ownership/resource contracts. |
| Memory | Bound arrays, sets/dictionaries, fixed headers/scratch, caches and private output assembly together. Distinguish shared-pool capacity, runtime/GC overhead and caller-owned output. A per-page/value limit does not bound a complete public scan. |
| Cancellation/failure | Honor documented read/preparation cancellation. Mandatory commit/replay must finish or retain its decision rather than perform unsafe partial rollback. Preserve both primary and undo/cleanup failures. |
See the storage contract, caller-stream contract, lock ordering and multi-process ownership.
| ID and production entry points | Native forms and complete path scope | Required safety and progress; remaining boundary |
|---|---|---|
C1 — Creation. AccessWriter.CreateDatabaseAsync path/stream; DatabaseCreationPublication.PublishAsync; header initialization. |
Jet3/Jet4/ACE bootstrap and selected encryption; private adjacent file initialization/flush/no-overwrite move/reopen; caller-stream initialization. Include cancellation, hot evidence, competing destination creation, pre/post-publication errors and owned-temporary cleanup. | Publish only complete output without overwriting another file; retain it if reopen fails. Valid supported creation must succeed. Caller-stream write/flush/truncate sweeps and namespace/metadata qualification remain I5/E4/F6/I15. |
| J1 — Provision/discover. PersistentRollbackJournal.Create, RejectHotJournal, Recover; PhysicalRollback.BeginWrite; writer file open. | Bounded header/raw page-hash manifest, partial original final page, path identity; .preparing create/flush/promote/reopen; final-only/preparing-only/both-name discovery; matching/contradictory copies, directory collisions and preparation failures before/after promotion. |
Establish authority before mutation and retain valid discoverable evidence. Clean files must prepare; valid survivors must reach recovery. Loss of every name is an I15/V7 bootstrap gap, not proof of an empty journal. |
J2 — Prepare writes/truncation. RecordBeforeWrite, RecordBeforeTruncate, CaptureOriginalPage, AppendRecord in PersistentRollbackJournal; StreamPageStore interception. |
First/repeated page capture; original/appended bytes, zero-padded partial final page, aligned writes, multi-page removed-tail coverage, capacity/offset overflow, actual record tags/hashes and failed append/fence. | Serialized durable records must establish exact undo coverage, after-image and length authority before effects. Valid finite preparation must succeed within limits. Logical page schedules do not prove actual serialization/hash identity or zero-exposure admission (V3/V6). |
J3 — Admit/build maps. ValidateJournal, ReadRecord, ValidatePreparationCopy, ValidateCurrentContent, framing/iteration in PersistentRollbackJournal. |
Short/exact/failed reads; header/path/manifest, tags/payloads, torn suffix versus invalid complete records, duplicate/conflicting evidence, minimum-length/replay controls, original/after-image mixtures and removed-tail coverage. | Every admitted map corresponds to exactly acquired records; refusal precedes writes and retains evidence. Valid pre-marker/marked survivors need reachable admission cases. Reordered truncate/older-write zero gaps remain V3/V6/V7 availability gaps even with exact undo coverage. |
J4 — Replay/decide/clean. Recover, RestoreBeforeImages, ValidateReplayInventory, RestoreAsync, RecordRecoveryStart, Complete in PersistentRollbackJournal; PhysicalRollback.CommitAsync. |
Committed cleanup/undecided restore; conditional removed-tail replay marker, exact inventory/source positions, resize/re-extension, ranked page replay, repeated torn replay, database fence, uncertain commit append/fence and cleanup callback/name deletion. | Acknowledgement selects committed output; uncertain decisions retain authority without contradictory rollback. Valid survivors eventually restore exact original or retain committed image under successful exclusive effects. Full production-loop/exception/namespace composition remains V6/V7. |
J5 — Live rollback/spill. PhysicalRollback; Pager.CommitAsync, SpillStatementAsync, RollbackStatementAsync, RestoreAfterFailureAsync in Pager. |
File journal versus other-stream raw undo, in-memory/temporary spill, private statements, physical page encryption, cancellation before first effect, mandatory replay, write/flush/truncate failure, aggregate undo errors, faulted writer and disposal/invalidation. | Restore promised image or fault/retain evidence; successful rollback restores counters/caches too. Commit/live restore must succeed for every supported store capability. Temporary spill is not persistent recovery; complete composition remains I5/I15/V6. |
| ID and production entry points | Complete path scope | Required safety and progress; remaining boundary |
|---|---|---|
R1 — Replacement admission. ReadState, ReadEvidence, field checks/length decode in EncryptionReplacementIntent. |
256-byte header, partial/complete 96-byte decision suffix, reserved fields, magic/version/generation/path, old/new length/hash, recomputed-checksum semantic corruption, short reads/EOF/I/O failure and admission before bootstrap. | Partial valid decisions select Prepared; complete valid decisions select Committed; complete invalid evidence refuses without authority. Generated scans cover named byte decisions; hash/path/GUID/I/O remain V5/V6 contracts. |
R2 — Immutable copy/prepare. Begin, CreateReplacement, CopyReplacement, Copy, Hash, ReadImage, IsPrefix/disposal in EncryptionReplacementIntent; EncryptionFileReplacement. |
Borrowed/acquired source handles, empty/multibuffer input, source-position restore, bounded/short reads, partial failed writes, digest/length identity, flushes, valid/conflicting staging prefixes, unprepared owned cleanup, prepared copy retention and retry. | Immutable selected copy and retired prior effects permit eventual exact bounded preparation. Prefix persistence, cryptography, failed syscall survivors, metadata and directory durability remain V5/V7. |
R3 — Publish/recover/clean. Commit, Recover, ValidateState, ValidatePublication, Publish, Cleanup in EncryptionReplacementIntent; EncryptionReplacementCommit; AccessDatabaseEncryption. |
Prepared/Committed; existing/missing destination; empty selected image; source/copy validation, publication/rename/replacement, source/destination fences, uncertain decisions, before/after callbacks, repeated retries, retained-path reporting and caller temporary cleanup. | Eventually publish the authorized selected image; cleanup follows successful validation/fence with leases retained. Bytes alone do not grant authority. Missing-name ACL/streams/timestamps/power-loss policy remains F6/V5/V6/V7. |
| O1 — Generation ownership. RecoverableWriterLock.Acquire, AcquireRecovery, Recover, Dispose and RecoveryLease. | Native lock evidence/receipt, fresh/existing/missing names, complete/partial/mismatched receipt, exact-authority reconstruction, failed bootstrap read/write/fence, stale attempts, owned-handle identity, retained-database cleanup and ordinary disposal after database closure. | Ready authority needs exact complete generation evidence; incomplete acquisition refuses/retains. Valid acquisition/reconstruction must succeed. Fresh tokens/canonical identity are contracts; complete composite refinement and namespace/exclusion qualification remain V10/V7/E4. |
| O2 — Composite coordination. LockFileCoordinator, LockFileSlotWriter, JetByteRangeLock, reader/writer open/dispose and R3/O1 leases. | Reader slots, strict writer/re-encryption, disabled/pathless/respect-existing options, intent/native/source/receipt handles, bootstrap before database open, page/commit locks, timeout/cancellation, partial acquisition, operation-drain/disposal order and cooperating clients. | No stale cleanup or recovery/write overlap; establish lock-order/deadlock prevention and separate fair eventual acquisition. Abstract atomic coordination does not refine the physical composite, aliases, SMB or macOS (V10/V7/E4). |
| ID and production entry points | Native forms and complete path scope | Required safety and progress; remaining boundary |
|---|---|---|
| P1 — File/header/page acquisition. Public path/stream open/detection; DatabaseFile, JetFormat, EncryptionManager, PageFile, StreamPageStore, StreamRead, BinaryBuffer. | Masked headers/generations, lengths/page counts, unaligned/truncated inputs, long offsets/checked narrowing, positional/gated seek I/O, read-ahead/disabled modes, pooled buffers, short reads/EOF/errors, codec/password/work budgets, cancellation and partial-open disposal/leaveOpen. |
Bounds before acquisition/allocation; actual I/O errors cannot become optional missing data. Valid reads must succeed in each mode. Shared kernels do not prove containing headers/parsers, pool accounting or physical effects (S1/V8). |
| P2 — TDEF/properties/catalog. TableDefReader, LogicalTDefChain, TDefCodec, ColumnPropertyReader, ColumnPropertyBlock, CatalogRowReader, TableCatalog. | Jet3/Jet4/ACE chains; cycles/count/slot contradictions, logical/aggregate schema budgets, opaque bytes, single/repeated/empty/populated pools, equivalent/conflicting targets, full catalog IDs/low-bit collisions, user/system/linked identities, physical ownership and independent Id/ParentIdName evidence, missing/damaged authoritative metadata. | Complete supported membership/identity, preserve unknown bytes or refuse edits; pinned positive observations do not prove completeness. Valid metadata must enumerate successfully. Native populated-pool binding, identity gaps and complete parser proof remain S1/S4/I17/V8. |
| P3 — Rows/scalars/public decode. OwnedDataPages, DataPageRows, RowDecoder, RowDecodePlan, ScalarColumnReader, RowValueDecodePolicy, TableReader. | Live/deleted/overflow rows, directory/fixed/null/variable slots, Jet3 jump tables, cycles/foreign owner, calculated envelopes, numeric/Boolean/date/complex-ID validation, string/typed/POCO/direct/hybrid/projected surfaces. | Contextual strict corruption; explicit lenient diagnostics/missing representation; preserve unreadable unassigned raw fields and refuse assigned erasure. Valid finite rows must yield consistent public results or cancellation without disappearing. Semantic/resource composition remains S1/S3/R4/V8. |
| P4 — LVAL codec/traversal. LongValueDescriptor, LongValueStore.ValidatePayload, LocateRow, CopyPayloadAsync, LongValueDecoder, LongValueVisitedSet. | 30-bit lengths; inline/single/chained/reserved modes/tokens; 24-bit page/8-bit row pointers; exact ownership, payload/declared mismatch, duplicates/cycles, end packing, Unicode/compression markers, calculated Memo/OLE/attachment envelopes, per-value/chain/aggregate budgets and large values, cancellation/short reads, locator/cache/pool/destination ownership. | Valid chains decrease to the exact declared payload. Codec and selected chain proofs do not establish native token semantics, complete public parser or all resources. Remaining forms/composition stay F8/S1/S3/V8. |
| P5 — Maps/index/complex traversal. UsageMap, OwnedDataPages, IndexCatalogReader, IndexPageCodec, IndexCursor, ComplexColumnReader, ComplexItemReader. | Inline/reference bitmaps; root/count/size consistency; key prefix/compression/sibling/child links, scalar/text/Memo/complex-reference keys, collations/code pages, positive complex IDs, attachment/multivalue/history catalogs/payloads, empty maps/trees, cycles/duplicates, scan/seek/range/last-entry, cancellation/resources. | Bounds/order compose with complete membership/ownership; opaque pages grant no reclamation authority. Valid supported scans must complete and agree with native forms. Complete forms/traversal/resource proofs remain S1/F9/I2/V8/V9. |
| P6 — External/container parsing. LinkedTableReader, LinkedSourcePolicy, LinkedSourceTraversal, DelimitedTextReader, CompoundFileReader, OleObjectDecoder, PageCodecFactory. | Permitted/denied linked paths/aliases, nested/cyclic links, aggregate reads/password work, missing-source/ODBC refusal, quoted field/record budgets, CFB FAT/miniFAT/directory chains, OLE wrappers and bounded encryption descriptors/XML. Office package recognition/refusal differs from native Access support. | Never execute database code/providers/macros/commands. Valid explicitly permitted sources must complete within limits; unknown forms require contextual refusal. No complete containing proof; external capability/security/resource risks remain S1/S3/F3/E1/V8. |
| ID and production entry points | Complete path scope | Required safety and progress; remaining boundary |
|---|---|---|
| B1 — B-tree edits/fallbacks. IndexMaintainer, IndexBTreeEditor, IndexTreeInventory, IndexBTreeBuilder, IndexEntrySplicer, IndexRewriteTopology, IndexKeyEncoder. | Ordinary/system/catalog incremental edits, tail append, surgical leaf/multilevel edits, split/merge/root changes, row/root relocation, key/Null/duplicate changes, opaque pages, system-table refusal where bulk fallback is disabled, retained rebuild/splice and FK fallback, descriptor/cross-TDEF renumbering. | Preserve ordered multiset/separators/row identity/counts and potential ownership atomically under L1/J5. Valid supported growth/shrink/edit paths must succeed. Native keys/forms and composed edit/reclamation proof remain I2/F9/V9. |
| B2 — Allocate/reclaim. PageAllocator, UsageMapEditor, UsageMapOwnership, LongValueReleaseScope, LongValueUsageMapMaintainer and deletion/rewrite callers. | Reuse/append/contiguous reservation, failed reservation cleanup, inline/reference map growth/shared rows, LVAL/tree/FK deallocation, empty pages, secure scrub/free-tail shrink/truncate, allocator hints and rollback. | Free only storage disjoint from reachable and potential references, including unknown metadata. Valid allocation must succeed within limits without reusing pinned/transaction-owned pages. Complete incoming-reference evidence and proofs remain I2/I5/I7/I17/V9. |
| B3 — Data/schema/constraint mutation. TableDataWriter, MutationPlan, MutationExecutor, TableRowStore, TableSchemaEditor, IndexSchemaEditor, TableRewritePlanner, TableStorageEditor, ConstraintRegistry, catalog/relationship/cascade/complex/history writers. | Insert/batch/update/delete; raw field/LVAL preservation/overflow; key swaps/index maintenance; defaults/validation/calculation/Null/uniqueness; self/cyclic cascades; complex/history IDs; add/drop/rename/private rewrites; logical index-name/target edits preserving tree and partner identities; security/catalog/dependency/application metadata; direct/auto/explicit/nested modes and all prepare/apply/failure paths. | Supported writes must succeed and preserve data/native-readable constraints; refusal/rollback must not lose unreadable data, partial cascades or state. Bounded interpretation never executes embedded code. Semantic/native gaps R4/S3/S9/F8/F9 and composition gaps I2/I5/I6/V6/V9/V10 remain. |
| B4 — Compact/repair. CompactDiscoverySession, CompactCatalogRecovery, CompactPinnedDatabaseBuilder, CompactPinnedDatabaseValidator, raw builders/validators, CompactEncodedDatabaseCopy; full design. | Healthy/damaged catalog; active/corroborated versus physical/pinned candidates; contradictory/duplicate evidence; source-index and incoming-reference audits; bounded workspaces; table/database raw/logical/encrypted assembly; independent destination inventory; refusal before source replacement. | Pinned assembly is not reclaiming compaction. Complete object/reference evidence must precede reclamation. Recover independently readable content/IDs/unknown metadata, report decisions and validate before R3 publication. No completed public compact or full proof is claimed; I17/V8/V9/V12 remain. |
| L1 — Writer/transaction lifecycle. TransactionLifecycle, PagerTransaction, JetTransaction, AsyncReentrantOperationGate, writer mutation/disposal. | Direct/auto/explicit/nested/savepoint, callback re-entry, page/depth budgets, terminal identities, preparation cancellation, uncertain commit, replay/undo failure, spill, snapshots/counters/catalog/constraint/allocator restore, gate drain/disposal errors. | No terminal transaction reuse or post-fault/dispose mutation; refusal restores state and uncertainty retains authority. Valid commit/rollback/dispose must be reachable under fair successful effects. Full lifecycle/controller/effect composition remains I5/V6/V10. |
| L2 — Cache/pool/snapshot ownership. Pager, PageFile, PageBuffers, ReaderPageCache, TDefImageCache, TableCatalog, MaterializerCache, TableSnapshotReader. | Cached/disabled/read-ahead, reader immutable buffers/writer dirty frames, savepoint copies, CLOCK eviction with retained consumers, exact pool returns, generations after write/rollback/truncate/failure, schema/catalog/materializer caches, concurrent/abandoned scans/seeks/LVAL/cancellation/dispose. | Do not recycle live references. Immutable pooled frames, scoped leases and replacement writes preserve borrowed images across eviction/invalidation; the abstract reference ledger is specified separately. Supported reads complete with stable values and released pins. Complete C# correspondence, aggregate bounds and containing lifecycle composition remain S1/I7/V8/V10; paired performance qualification remains separate. |
This table accounts for root APIs and every first-level library source directory. Mapped critical domains remain in scope even without a proof. Priority 0 denotes recovery authority/durable-decision risk, priority 1 denotes malicious-input/data-loss/ownership/concurrency risk, and priority 2 denotes pure semantic/API correctness without independent storage authority. Priorities are not coverage statuses.
| Surface | Classification/priority and reason |
|---|---|
Root APIs, DatabaseFile, JetFormat*, options, diagnostics, transaction |
Critical C1/J1–J5/R1–R3/O1–O2/P1–P4/L1–L2; priorities 0/1: overloads select file/stream recovery, codecs, limits and disposal. Header/text/row interpretation belongs to containing parsers. Pure rendering has priority 2; re-entry/error translation remains L1/P3. |
Catalog |
Critical P2/P6/B3/B4/L2; priority 1: full object identity, properties, linked/saved metadata and security/catalog writes establish preservation/ownership authority. |
ComplexColumns |
Critical P3–P5/B3/L1; priority 1: parent/child/reference identity, payload/history/multivalue preservation and atomic mutations. |
CompoundFile |
Critical P6; priority 1: internal FAT/directory/container parsers still process hostile input. Package refusal is not proof of helper safety; output encoding needs B3/P6 correspondence. |
DelimitedText |
Critical P6; priority 1: external record/field parsing and retained buffers need bounded traversal/ownership. Pure delimiter/header normalization has priority 2 unless it affects resource/identity decisions. |
Encryption |
Critical R1–R3/P1/P6/B3; priorities 0/1: protocol policy. Cipher/password/hash/entropy primitives remain explicit contracts requiring native vectors, budget/cancellation and residual-trust review. |
Enums |
Dependent specifications for P/B/L behavior; priorities 1/2: format/storage/error/policy values affect admission. Passive labels have no independent effect theorem; policy/numeric changes require containing-path review. |
Exceptions |
Critical P1–P6/J5/L1 adapters, P1; pure formatting has priority 2: distinguish corruption/missing/I/O/cancellation/uncertainty without losing primary/cleanup failures. |
Indexes |
Critical P5/B1–B3; priority 1: codecs/comparisons/cursors, incremental and rebuild/splice/FK fallbacks establish membership and ownership. Numeric outward-bound, signed-zero and exact integral query-order admission execute generated scalar decisions under CLR/native comparison contracts; complete pure query planner semantics remain I9 at priority 2. |
Infrastructure |
Critical C1/P1/P6/O2/L1/L2 and dependencies; priorities 0/1: bounds/reads/gates/closures/paths/publication/caches need containing-path review; CRC/hash/shift helpers need checked-arithmetic review. |
Interfaces |
Contract boundaries of mapped behaviors; priorities 1/2: no independent effect in a declaration, but ownership/stream/decode/transaction contract changes alter specification adequacy. |
Linq |
Deferred semantic proof I9, P2; critical P1/P3/P5/L2 dependencies: operator results/evaluation order/capture/async faults remain tested obligations without persistent recovery authority. Unsafe parsers and ownership reached through queries remain in scope. |
LongValues |
Critical P4/B2/B3/L2; priority 1: descriptor/token identity, traversal, allocation/release and buffer ownership compose into public reads/writes. |
Maintenance |
Critical B4/P2–P5/B1/B2/R3; priorities 1/0: every builder/validator/budget/workspace and active/pinned/recovered alternative participates in potentially destructive compact decisions. Internal status does not exclude it. |
Mapping |
Critical P3/L2 decode/buffer/cache boundaries, P1; conversion fidelity has priority 2: reflection/generated materializers must propagate faults and honor lifetime/cache bounds; target/trim checks remain independent. |
Models |
Dependent representations of P/B/L behavior; priorities 1/2: pointer/ref/size/encryption/complex/constraint identities need representation review. Passive DTOs have no separate effect theorem; meaning changes alter containing specs. |
Pages including Paging |
Critical J1–J5/P1/P3/P5/B2/L1/L2; priorities 0/1: storage/journals/directories/allocator/maps/buffers supply all higher effect/ownership premises. |
Polyfills and root IsExternalInit |
Target/compiler contracts, priority 1 for behavioral polyfills and priority 2 for markers: target-specific behavior must not weaken bounds/exceptions/ownership; both assets remain CI obligations. |
Queries |
Deferred plan/operator semantic proof I9, P2; critical P1/P3/P5/L2 dependencies: closure/include/order/paging/aggregate/cache correctness remains required without granting recovery authority. |
Relationships |
Critical P2/P5/B1–B3/L1; priority 1: FK lookup/constraints, self/cyclic cascades, catalog links, fallback maintenance and rollback preserve identities/data. |
Schema |
Critical P2/P3/B1/B3/L2, P1; pure function fidelity under R4 has priority 2: codecs/properties/dependency projection are critical. Bounded non-executing interpretation, mutation authorization and native-error preservation stay P3/B3 scope. |
Tables |
Critical P3/P5/B1–B3/L1/L2; priority 1: public scans, snapshots, index/mutation/rewrite orchestration compose storage/semantic/resource contracts. |
Transactions |
Critical O1/O2/L1 and J/R composition; priorities 0/1: acquisition/serialization/savepoints/commit uncertainty/disposal retain or revoke authority. |
ValueDecoding |
Critical P3/P4/P6/L2; priority 1: string/object/typed/hybrid/calculated paths must preserve validation, I/O failures, limits and buffer ownership. |
ValueEncoding |
Critical B3/P3/P4/B1; priority 1: assigned/unassigned raw data, envelopes/text/numeric/LVAL encoding must validate before allocation and preserve native semantics. |
Verification |
Executable boundary plus trusted projection/compiler/runtime; priorities 0/1: generated source freshness is checked; caller/adapter/runtime assumptions remain explicit. |
The scaffold executable, FormatProbe, test support/tests, benchmark harnesses, repository scripts and CI are outside shipped runtime theorem scope. They remain evidence/trust inputs: scaffold-generated consumers require target/trimming/AOT checks; probes/DAO supply provenance/native observations; verifier/compiler/projection/pin/gate tooling requires trust review. Exclusion cannot turn failed harnesses, skipped DAO cases or broken benchmarks into successful evidence.
Deferred pure query/expression/coercion/presentation proofs retain I9/R4/compatibility requirements. Unknown providers/forms and platform qualification retain their F/E/S/I items. Classification or proof-scope revision does not close independent functionality/safety acceptance obligations.
Review each ID against public entry points and all listed alternatives. Keep success/refusal cases, faults, budget ownership, native forms and platform qualifiers attached when paths split. New modes/fallbacks/adapters require an explicit extension and matching evidence-map disposition. Grouped behaviors represent containment boundaries rather than an exhaustive static call graph.
The initial inventory is established when every named critical domain and alternative has a required property and an evidence-map disposition. Final V12 closure additionally requires machine-checked production composition for each in-scope decision, justified adapters, adequacy review with reachable successful operations/negative controls, and qualification of every advertised environmental guarantee. This inventory defines the scope for that review; it does not assert completion of the later obligations.