Welcome to LQ.
As one of the few hardware heads about here, let me have a go at this.
Am I correct in assuming the relevant figures are highlighted?
Code:
0x0000000010008000 0x0000000010009000 0x0000000000040200
That, indeed gives some dubious multiple of 4096 on a calculator, but in fact 4097 in hardware- my calculator is very odd. This one
Code:
10008000-10008fff : 0000:00:00.0
The first of those gives 0x7fff of a difference, the second 0x0fff, or 4095; when you look at that from a hardware perspective, it's 4096, remembering the days of limited address lines, number ranges go from 0x00-0xFF for 256 addressable bits with 8 lines. 0x00 is a valid address, 255 is the top address, giving 256 bits
Applying this logic to your figures, the output of /sys/devices/pci0000:00/0000:00:00.0/resource is suspect. You notice the address 0x0000000010008000 is assigned to both blocks? I suspect it shouldn't be. That looks like a kernel bug or system bug to me.
For your purposes, treat it as 0x0000 - 7FFF & 8000 - 8fff, and report the bug. There's a time penalty in doing that, but pay it.
I must say in passing, that I expected to be fingering your code, and not the kernel.