I'd like
   to run the following assertions past you: if there are any that are
   not valid, please let me know.

Your points are basically correct; I just want to emphasize a couple
of things.

   5. Routines called by softnet() are run at splnet.

Yes, but note that splnet() only blocks software interrupts, not
hardware interrupts.  It really should have been named splsoftnet().

   6. MGET, MFREE, etc., can be used at any spl level.

Yes, but only because they use splimp() internally.