[gavinying]

Summary

Full audit TM ───┐
                 ├── modsim TCP → identical selected register values
Public audit TM ─┘

Evidence

• Before: The pinned interpreter rejected models declaring the audit extension.
• After: The released a4 interpreter accepts both forms. The simulator checks selected values, excluded spans, denied writes and clean stop.

Merge Danger

Door: Two-way before tagging.

Blast Radius: Model interpretation in the v2 simulator preview.