docs(formal-verification): DMA memcpy

Makefile

@@ -630,6 +630,36 @@ fmt:
 	cargo fmt --all
 
 # Run clippy + fmt check (used by CI)
+.PHONY: verify-dma
+verify-dma: ## Run the DMA memcpy formal-verification gate (formal_verification/dma)
+	@# Oracle anchors + vector emission, the z3 soundness gate, and the
+	@# transcription audit. Needs `pip install z3-solver` (validated on 5.0.0);
+	@# the audit alone needs no solver.
+	@# Exit codes: 1 = failure (abort), 2 = ran but degraded (an external anchor
+	@# was unavailable). Only 1 should stop the run -- otherwise a machine without
+	@# a loadable libc would skip the audit and the gate, neither of which needs it.
+	python3 formal_verification/dma/test_ref.py || [ $$? -eq 2 ]
+	python3 formal_verification/dma/audit_transcription.py
+	@# The gate, then a freshness check on its committed transcript. Without the
+	@# diff, `verify.log` is a claim about a run nobody repeats -- it could drift
+	@# from the gate silently, which is the same "declared, not derived" defect the
+	@# audit script exists to catch. The `solver:` line is excluded because it names
+	@# the local z3 build: pinning it would turn any version bump into a spurious
+	@# red, and a spurious red is how a check gets deleted rather than fixed.
+	@out=$$(mktemp); st=$$(mktemp); \
+	{ python3 formal_verification/dma/z3_verify.py 2>&1; echo $$? > $$st; } | tee $$out; \
+	if [ "$$(cat $$st)" != "0" ]; then rm -f $$out $$st; exit 1; fi; \
+	grep -v '^  solver:' formal_verification/dma/verify.log > $$out.committed; \
+	grep -v '^  solver:' $$out > $$out.fresh; \
+	if diff -u $$out.committed $$out.fresh; then \
+		echo "  verify.log matches this run."; \
+	else \
+		echo "  FAIL: verify.log no longer matches the gate. Regenerate with:"; \
+		echo "        python3 formal_verification/dma/z3_verify.py > formal_verification/dma/verify.log"; \
+		rm -f $$out $$st $$out.committed $$out.fresh; exit 1; \
+	fi; \
+	rm -f $$out $$st $$out.committed $$out.fresh
+
 lint:
 	cargo fmt --check --all
 	cargo clippy --workspace --all-targets -- -D warnings -A clippy::op_ref

formal_verification/dma/canonical_dma_rows.txt

@@ -0,0 +1,70 @@
+# Generated by test_ref.py — do not edit by hand.
+# Consumed by prover/src/tests/dma_tests.rs via include_str!.
+# vector|name|dst|src|count|data_rows      row|src|dst|count|tail|width
+vector|empty|4096|8192|0|0
+vector|single byte|4096|8192|1|1
+row|8192|4096|1|1|1
+vector|one wide row|4096|8192|8|1
+row|8192|4096|8|0|8
+vector|wide plus tail|4096|8192|9|2
+row|8192|4096|9|0|8
+row|8200|4104|1|1|1
+vector|widest tail|4096|8192|7|7
+row|8192|4096|7|1|1
+row|8193|4097|6|1|1
+row|8194|4098|5|1|1
+row|8195|4099|4|1|1
+row|8196|4100|3|1|1
+row|8197|4101|2|1|1
+row|8198|4102|1|1|1
+vector|unaligned body and tail|8197|4099|27|6
+row|4099|8197|27|0|8
+row|4107|8205|19|0|8
+row|4115|8213|11|0|8
+row|4123|8221|3|1|1
+row|4124|8222|2|1|1
+row|4125|8223|1|1|1
+vector|forward overlap|12292|12288|24|3
+row|12288|12292|24|0|8
+row|12296|12300|16|0|8
+row|12304|12308|8|0|8
+vector|backward overlap|12288|12292|24|3
+row|12292|12288|24|0|8
+row|12300|12296|16|0|8
+row|12308|12304|8|0|8
+vector|page crossing|4092|8188|16|2
+row|8188|4092|16|0|8
+row|8196|4100|8|0|8
+vector|maximum chunk|4096|8192|256|32
+row|8192|4096|256|0|8
+row|8200|4104|248|0|8
+row|8208|4112|240|0|8
+row|8216|4120|232|0|8
+row|8224|4128|224|0|8
+row|8232|4136|216|0|8
+row|8240|4144|208|0|8
+row|8248|4152|200|0|8
+row|8256|4160|192|0|8
+row|8264|4168|184|0|8
+row|8272|4176|176|0|8
+row|8280|4184|168|0|8
+row|8288|4192|160|0|8
+row|8296|4200|152|0|8
+row|8304|4208|144|0|8
+row|8312|4216|136|0|8
+row|8320|4224|128|0|8
+row|8328|4232|120|0|8
+row|8336|4240|112|0|8
+row|8344|4248|104|0|8
+row|8352|4256|96|0|8
+row|8360|4264|88|0|8
+row|8368|4272|80|0|8
+row|8376|4280|72|0|8
+row|8384|4288|64|0|8
+row|8392|4296|56|0|8
+row|8400|4304|48|0|8
+row|8408|4312|40|0|8
+row|8416|4320|32|0|8
+row|8424|4328|24|0|8
+row|8432|4336|16|0|8
+row|8440|4344|8|0|8