[SeaBIOS] [RFC 2/3] Transitions to and from 64 bits