The selected hostile-file surface is LongValueStore.CopyPayloadAsync for an external chained descriptor. verification/LongValues/LongValueTraversal.dfy proves termination and resource bounds for its row schedule. Production calls the generated LongValueKernel.ChainVisitAdmission and ChainPayloadCount decisions. Its visited set uses generated PrepareVisitedAdd and CompleteVisitedGrowth methods, composing the exact ContainsVisited, AddVisited and RehashVisited array operations with occupied-count bookkeeping and growth decisions. Actual allocation, adapter sequencing, the complete C# parser, native row ownership and arbitrary locator/destination implementations remain separate contracts.
Descriptor admission first bounds the declared stored length L and configured row budget B. A null pointer, exhausted row budget or repeated row identity refuses before another acquisition. Successful distinct visits consume one row-budget unit. The generated payload selector admits only a nonempty bounded row payload and returns at most the remaining declared bytes. Each completed write therefore decreases the remaining payload L - copied by at least one. Traverse uses B - acquisitions as its loop rank, so a zero-payload row, absent row or invalid slice refuses after its single acquisition instead of permitting another iteration. The mathematical visited set contains exactly the distinct nonzero acquired identities.
Only the descriptor’s declared prefix is streamed. Pointers or padding after completion are not interpreted. This behavior cannot establish complete storage ownership or authorize reclamation. Single-page and inline paths retain their existing format rules; the arbitrary chained-graph proof concerns the external chained path.
For n attempted row acquisitions, including a final malformed row, the theorem establishes:
n <= min(L, B) and exactly n retained logical row identities;L, with each successful chunk bounded by the effective page length;pageSize * n;16 + 4*n unsigned-integer slots;32 + 8*n slots, counting every superseded array, hence at most 128 + 32*n bytes of array payload.The array-backed Traverse now invokes PrepareVisitedAdd and
CompleteVisitedGrowth directly. Erased ghost meters on their actual loops
compose deterministic resource bounds, including a final refusing preparation:
destination-table probes are at most 20*n*n + 92*n + 48, rehash source-loop
iterations are at most cumulative allocated slots, and peak simultaneously
owned old/new table payload is at most 24 + 6*n slots. Each lookup/insertion
charges its actual observed slots; rehash charges each source-loop iteration
and every destination probe. No randomized-hash assumption is used.
These meters distinguish probes, source-loop iterations and zero-filled array volume. They do not count every CPU instruction or prove CLR zero-initialization time, physical heap size, allocation success or cancellation latency. All meters and arithmetic are ghost-only; the shipping kernel has no executing counters.
LongValueVisitedSet allocates lazily with an initial 16-slot table and doubles at half occupancy. Generated PrepareVisitedAdd handles zero and duplicate identities, uses one AddVisited scan below half occupancy, and checks for a duplicate before requesting growth. CompleteVisitedGrowth rehashes into the requested distinct zero-filled array, inserts the absent identity and updates the count. Every successful growth adds exactly the new capacity to cumulative allocated slots; their sum is strictly less than twice the current capacity. During rehash, only the old/new arrays are referenced by the set, and their combined size is bounded by that cumulative sum. Retrying an identity does not allocate another table. Growth refuses before producing an array length beyond the bounded native selector. The C# adapter performs the requested CLR array allocation and publishes successful results. An allocation failure propagates before replacing the old table; successful allocation or sufficient machine memory is not assumed for termination by refusal.
The formulas count traversal-owned array payload, not CLR object/array headers, async frames, error strings, allocator bookkeeping or GC retention policies. The number of arrays is also bounded by their cumulative slots because every array has at least 16 slots. The parser does not allocate a buffer of size L; it awaits each borrowed row’s write and releases that row before the next acquisition. The locator may use pooled arrays larger than the effective page length; pageSize*n is acquisition work over admitted page prefixes, not an allocator-byte bound on locator internals. Locator/cache allocations and destination storage are independent contracts.
ProbeRankDecreases, ProbeResiduesAreDistinct, CircularProbeCoversEverySlot, NonfullProbeFindsEmpty and NativeProbeMatchesCircularStep establish bounded circular probing and coverage. Every production lookup/insertion has an explicit decreasing remaining-slot counter. Half occupancy provides empty slots, and rehash preserves the existing logical identities by inserting every nonzero old slot into the new array.
LongValueKernel.VisitedTable requires that every slot earlier on an occupied identity’s circular probe path is nonzero. The generated ContainsVisited loop proves exact nonzero membership, including safe early termination at an empty slot and an absent result for an empty array. This total empty-table case lets the controller refuse duplicates without a separate empty-array check. AddVisited performs one scan to distinguish an existing identity, a new insertion and a full table. Only insertion mutates the array; it preserves the probe-chain invariant, adds exactly the absent identity and increments occupied-slot count. RehashVisited constructs the invariant in a distinct, larger zero-filled destination and preserves exactly every nonzero source identity, including duplicate identities in the source. These contracts require no random-hash or expected-time assumption.
The ghost TrackedVisited predicate couples unallocated initial storage with distinct nonzero membership, exact occupied count, the probe-chain invariant, half occupancy, the native capacity ceiling and capacity <= 16 + 4*count. VisitedSnapshot treats null storage as empty; existing empty-array inputs remain admitted. PrepareVisitedAdd and CompleteVisitedGrowth preserve that representation while composing lookup, insertion, rehash and count/growth policy. The internal decision value carries only the selected operation’s payload: zero means unchanged, a positive count means insertion, the high flag plus capacity requests growth, and all bits set refuses exhausted capacity. Exact classification, payload inverses and EncodeAbstractVisitedDecision preserve the abstract status/count/capacity transition. Ghost effective projections retain the supplied previous count for unchanged, growth-request and refusal outcomes. The adapter returns immediately for zero and uses generated flag, exhaustion and payload decoders. Ghost membership/count expressions add no executing collection or recount. The adapter must retain the matching array/count pair, supply distinct correctly sized zero-filled growth storage, and publish successful results.
The containing model now uses concrete arrays and invokes the generated controllers; a ghost set records their exact membership. The public C# acquisition/budget schedule and actual allocation/adapter effects still require implementation refinement. LongValueTraversalTests independently compares generated lookup/insertion/rehash and wrapper membership through collisions, growth and duplicate reinsertion, tests repeated identities across growth boundaries, refuses every no-progress chained row size, and checks the generated slice selector against a wide-arithmetic boundary oracle. Existing LongValueStreamingTests cover exhaustion before another lookup, cycles, truncated chains, partial writes, cancellation, source/destination errors and delayed buffer release. These controls supplement the proof; they do not mechanically verify the complete containing parser or effect adapter. The model now bounds aggregate adversarial probes, source iterations and peak old/new overlap. Their public C# correspondence and cancellation latency inside synchronous probe/rehash operations remain open under V8/S1. Moving orchestration into generated code preserves the existing scan and allocation policy; hosted measurements remain necessary for timing acceptance.
The pure model assumes that each described row acquisition and successful write completes. Actual I/O may fail, and cancellation is checked before each acquisition/chunk. Failures can leave a partial destination; no rollback or destination flush is promised. A successful locator transfers its scoped page lease with the located row. The traversal disposes that location in finally, including invalid locations and failed writes, after the awaited output has completed. Both reader-cache and compact-discovery locators use this ownership path; there is no separate raw-buffer release callback. If the locator itself throws, it retains ownership. Actual buffer return and successful stream effects remain implementation contracts; the frame ownership ledger is a separate abstract specification with manual C# correspondence.
The row directory, page type, pointer/token interpretation, native format compatibility, cache ownership, rented-buffer sizing, destination persistence and concurrent mutation of borrowed bytes remain separate obligations. Native fixtures, malformed-file tests and fuzzing remain necessary. No whole-library hostile-file or crash-durability guarantee follows from these bounds.