So, the schematics are out, time to dig out this topic!
It turns out the USB host ports are powered by a TPS2505, a 1.1A boost converter. The chip has the capability to limit current per port, but the chosen resistor value is such that there's essentially no limiting; either port can sink all the boost converter's output, which can be quite a bit more than 1.1A. Should be plenty for a 2.5" HDD, even with a USB trinket also plugged in.
BTW, there's no direct path from either charging port to the host ports, contrary to what I wrote above.
As for a hypothetical upgrade to USB3, there's clearly not enough juice, on paper. But it's likely to work anyway. I guess the OS could be set up to not give a new USB device permission to increase power use if that would overstep the TPS2505's limit, but I think there's no need to be so anal about it. Let the user figure out that plugging two power guzzling gadgets into a handheld is a bad idea, especially when the battery voltage is already low (which is when the boost converter is going to have trouble providing 1.4A). Ideally, the OS would pop up a message if the ports are overloaded (and not just hide it in dmesg). There's also the possibility that a new CPU board would come with a new main board with a stronger chip, and a note that the new CPU board mated with an old main board can't meet USB spec.