docs(formal-verification): DMA memcpy - #926

Open

nicole-graus wants to merge 9 commits into

feat/dma-memcpyfrom

feat/dma-memcpy-formal-verification

Commits on Aug 11, 2026

Add a py model and a z3 soundness gate for DMA memcpy and a transcription audit
nicole-graus
committed
5819f0b
Bind DmaNext per 32-bit limb in the DMA gate
nicole-graus
committed
8d5130d

Commits on Aug 12, 2026

Correct the forged_wide_tail attribution and make the DMA audit, oracle sweep and Rust tests catch the mutations they claimed to
nicole-graus
committed
c0c0755
Move the DMA verification gate to formal_verification/dma and consolidate it into one README
nicole-graus
committed
c3f5b8a
widen the packing guard to every compound arm, pin is_read directly, and make verify-dma fail on a stale verify.log
nicole-graus
committed
48b507a

Commits on Sep 2, 2026

Correct the DMA gate's README and a stray comment
jotabulacios
committed
81ad3a3

Commits on Sep 3, 2026

Pin the DMA audit claims to what they name
jotabulacios
committed
3fbb5ff
Check the DMA trace columns against the oracle
jotabulacios
committed
015fae1

Commits on Sep 4, 2026

Update the DMA campaign README for the audit fixes
jotabulacios
committed
dfc525b