The entry applies when a proof about Wasm code must keep an array's representation across stores, allocations, or memory growth, or must show that code fills an array word by word. LeanExe.ProofKit.UInt64Array.At store ptr xs is the layout of an Array UInt64 in memory: the length word at ptr, element i at UInt64Array.wordAddress ptr (i + 1), and bounds that keep every word inside 32-bit addresses and inside memory. Heap.Borrowed and Heap.Owned hold it as their field values, so the runtime's proofs and the verified compiler's code proofs keep it whenever they keep an array.
UInt64Array.At.frame keeps the layout across a change that does not shrink memory and leaves the array's bytes unchanged, which covers an allocation that grows memory or writes a block elsewhere. At.writesRange applies it to a Memory.WritesRange whose interval lies apart from the array, as the entry on write ranges describes. At.frameBefore covers changes at or above a cutoff that the array ends below, with the page count unchanged, and At.write64After covers one store at or above the cutoff. At.elementRead and At.elementBound give an element's word and the memory bound of its address.
The verified compiler's copy loops keep At of a changing array. UInt64Array.writeElement store ptr k v is the store after the write of element k, and UInt64Array.At.writeElement, in Verified/ArrayCopy.lean, gives At of xs.set k v in it. A loop that copies xs into the positions from k of the array words carries At store' pdst (Verified.overlay words xs k i) after i passes: Verified.overlay_zero starts the invariant at words, and Verified.overlay_succ rewrites the array after one more write. UInt64Array.writeElement_frame states that the write changes only bytes inside the array, which the loop's write-range invariant needs. Verified.element_address rewrites the address that the code computes, (ptr + (UInt64.ofNat k + 1) * 8).toUInt32, to wordAddress ptr (k + 1), and UInt64Array.At.writeLength gives the first n elements after a store of a length n no larger than the array's.
UInt64Array.PrefixAt store ptr xs count is the other method for code that writes an array in index order after its length word: it records the final length and the first count elements. PrefixAt.empty starts after the length store, PrefixAt.elementBound gives the next store's memory bound, PrefixAt.write_next extends the prefix by one writeElement, and PrefixAt.complete gives At. The verified compiler's proofs do not use PrefixAt.
For a goal that reads a word after nested write64 stores, the tactic word_reads of LeanExe.ProofKit.Memory rewrites a read at a written address with Memory.read64_write64 and a read eight or more bytes away with Memory.read64_write64_disjoint, proving the separation by omega. Apply read64_write64_disjoint directly when omega needs facts outside the context, as UInt64Array.At.writeElement does after rewriting both addresses with UInt64Array.wordAddress_toNat. These facts describe memory and indexing only, so a loop's invariant and the equation of its output come from the proof of the loop.
Packed bytes have their own layout, Verified.Bytes.At mem root bytes, with byte i at root + i. Verified.Bytes.At.frame and Verified.Bytes.At.writesRange are its forms of At.frame and At.writesRange. A proof that keeps a byte buffer across a write therefore follows the steps above with these lemmas.
Verified.wpX_copyInto proves the loop of copyIntoCode with the overlay invariant, a write range on the destination array, and At.writesRange for the source. Verified.wpX_copyDown and Verified.wpX_shiftUp move words inside one array and keep its layout in the same way. Their forms without the alignment flag are Verified.wp_copyInto, Verified.wp_copyDown, and Verified.wp_shiftUp.