improving the type for ehci_attach_td

[githwxi]

fun ehci_attach_td {l: agz} ( usbd: !usb_device, td: &ehci_td_ptr l >> ehci_td_ptr l' // if successful, consumes TD -- else it does not ): #[s: int] #[l': agez | s == 0 || l == l'] status s =

can be improved to

fun ehci_attach_td {l: agz} ( usbd: !usb_device, td: &ehci_td_ptr l >> ehci_td_ptr l' // if successful, consumes TD -- else it does not ): #[s: int;l':addr | (s == 0 && l' == null) || (s > 0 && l' == l)] status s =