dfet: === go=2: dispatching REAL kernel handlers (built-in 'device et'): et_intr=0xffffffff804b8bd0 et_txeof=0xffffffff804b6740 et_stop=0xffffffff804b5ed0 et_tick=0xffffffff804b87d0 et_newbuf_hdr=0xffffffff804b9450 et_newbuf_cluster=0xffffffff804b9460 ===
dfet: S2: ET_TX_DONE_POS index=600 wrap=0 (ET_TX_DONE_POS_INDEX=10-bit vs ET_TX_NDESC=512: 600 is UNREACHABLE by tbd_start_index), tbd_used=1; dispatching REAL et_txeof(sc, 0) (et_start:1223 call shape)
dfet: S2: if the guest PANICS with KKASSERT "tbd_used > 0" (if_et.c:2050), DF-4056-TX is proven
panic: assertion "tbd->tbd_used > 0" failed in et_txeof at /usr/src/sys/dev/netif/et/if_et.c:2050
cpuid = 2
Trace beginning at frame 0xfffff801183676b8
et_txeof() at et_txeof+0x1cb 0xffffffff804b690b 
et_txeof() at et_txeof+0x1cb 0xffffffff804b690b 
df_sysctl_go() at df_sysctl_go+0xc14 0xffffffff82600f04 
sysctl_root.isra.5() at sysctl_root.isra.5+0x166 0xffffffff80683d06 
userland_sysctl() at userland_sysctl+0x111 0xffffffff806840a1 
sys___sysctl() at sys___sysctl+0x74 0xffffffff80684204 
Debugger("panic")