You're right about your assumptions.
The OS writes to in configuration space and configures the BAR0..5
The spaces sizes are not set in the INF file but are determined by the OS by writing/reading the BAR0..5 registers (some bits in the BAR registers are read-only, and other are writable, and that determines the size of each space).
I hardcoded the IO space in some files to make it easier to start the PCI project. The latest file (not published but part of the Dragon kit) is not hardcoded but implements the configuration space registers instead (used in combination with Dragon's WDM PCI driver).