docs(formal-verification): DMA memcpy

[nicole-graus]

Motivation

#874 adds a new fixed table, and nothing independently checks that its AIR proves what a memcpy actually is.

Description

Adds docs/verification/dma/:

• Oracle — a four-level reference model (byte semantics / row decomposition / MEMW multiset / guest chunking), anchored on libc memmove and CPython slice assignment over 3,855 differential cases each, plus an 8-mutant sensitivity sweep.
• Gate — a field-exact z3 model of the AIR: 6 row-level checks, 6 chain checks with DmaNext modelled as a free bijection rather than an assumed chain, 10 premise controls each with a named forgery, and a completeness sweep over every length 0–256.
• Audit — 100 executable claims tying the gate, the spec and the Rust together, mutation-tested against 6 source mutants.

Plus two Rust tests driving the real collect_dma_memcpy_ops against the oracle's emitted vectors, and a make verify-dma target.

No shipped constraint, column, bus interaction or executor path changes.

No soundness gap found. The first commit reported one; the second retracts it —DmaNext binds each 64-bit value as two 32-bit bus elements, not one packed field element, so the limbs are already pinned and the alias the gate exhibited is unreachable. The retraction is kept in the docs as the campaign's main lesson.

How to test

make verify-dma
cargo test -p lambda-vm-prover --lib dma

Needs pip install z3-solver (validated on 5.0.0; the audit alone needs no solver).