There's good evidence for mask registers and x87 registers sharing the same hardware on recent Intel chips: https://travisdowns.github.io/blog/2020/05/26/kreg2.html