$ scp -F dfbsd-qemu/config findings/poc/DF-4219/trigger.c dfbsd:/tmp/
trigger.c                              100% |********************************|  (guest scp ok)

$ vm.sh run_root 'cc -O2 -Wall -Wextra -o /tmp/df4219 /tmp/trigger.c && echo BUILD_4219_OK'
BUILD_4219_OK
(build 1 had a -Wunused-but-set-variable warning for a model-local variable;
fixed in place and rebuilt clean — see verdict.json poc_changes)

$ vm.sh run_root '/tmp/df4219; echo RC_4219=$?'
DF-4219 model: ae_rx_intr() for(;;) walk vs device-fed AE_RXD_UPDATE
(sys/dev/netif/ae/if_ae.c:643-668, ring=64)

[1] honest device (5 real frames): walk processed 5 descriptors, exited normally.

[2] device keeps AE_RXD_UPDATE ahead of the clear: MODEL SELF-CAP HIT
    after 1000000 descriptor iterations in ONE ae_rx_intr() call (1000000 device marks,
    ring wrapped 15625 times); guard :647 never went false.
    frame budget consulted by driver: 0 (none exists in if_ae.c -- ale(4) at least has dead ALE_PROC_* knobs)
    while looping: ifp->if_serializer held (:754), AE_MB_RXD_IDX_REG mailbox (:671) never updated,
    every iteration m_devget+if_input (:616/:625) -> CPU + softint livelock until reboot.

TRIGGER_RC=0 (model OK; hardware-gated on this guest: no Attansic L2 NIC)
RC_4219=0

(full untrimmed guest output of the decisive run)