Yes, as you found it follows straightforward binary numbering using the REX bit as the leading bit and the ModRM bits as the low 3 bits to encode the register number. 8 = 1000 in binary, so that's the encoding for R8.
https://wiki.osdev.org/X86-64_Instruction_Encoding#Encoding explains nicely, and https://wiki.osdev.org/X86-64_Instruction_Encoding#Registers even has a table.
I searched Intel's vol.2 PDF for r14 (which is not "special" for anything, and will probably only show up in tables). There are some tables in vol.2, but not one for simple ModRM itself. (The combined PDF is too huge to want to work with).
Vol.2 does clearly describe how REX fields combine with ModRM fields to make 4-bit register numbers. (e.g. Figure 2-4 showing the concatenation of REX.B and ModRM.rm, and REX.R with ModRM.r). I didn't check vol.1 - I wouldn't be surprised if some statement about register names (used by assemblers) matching binary register numbers could be found there. Names are only meaningful to assemblers, not in machine code, and that is clearly documented in vol.2.
However, the info is there in vol.2:
It does have Table 3-1. Register Codes Associated With +rb, +rw, +rd, +ro (Contd.) for instructions with no ModRM where the low 3 bits of the opcode byte are the low 3 bits of the register number. (Like the short encodings of push/pop r64).
| Reg |
REX.B |
Reg field |
| R13B |
Yes |
5 |
| R14B |
Yes |
6 |
And so on with rows for every register, and 3 more sets of columns for word, dword, and qword sizes for R14W, R14D, R14. So if you were in doubt about the fact that the binary numbers map to register names, that table makes it clear. (It would be insane to assume that register numbers work differently here than in other contexts.)
There's also the opcode map for one-byte opcodes, where push rSI/r14 share an entry (0x58), same for xchg-with-(e)ax, mov-immediate to byte-reg, pop, mov-immediate to word/dword/qword-reg, and bswap in the 2-byte opcode map. Again, it would be insane for these register numbers to work differently than register numbers in other places.
There is a full table Table 2-8. VEX.vvvv to register name mapping, with xmm/ymm0..15 and RAX/EAX .. R15/R15D. (VEX.vvvv can encode integer registers for BMI instructions like andn, and yes they are only documented for dword or qword, not overrideable to word operand size with a 66 prefix.)
Table 2-13. 32-Bit VSIB Addressing Forms of the SIB Byte is also relevant, showing columns like ESI/R14D. (In 64-bit mode, you normally wouldn't use a 67 address-size prefix with vpgatherdd or whatever, but you can. There isn't a separate table for 64-bit address-size.) The table doesn't explicitly mention how VEX.B selects between the two registers for a given value of bits 2:0, but that should be obviously from other cases.
