This may be not so well hidden as the boost color sensor reports an output mode called "IR Tx" with the following specs:
90842b0e7cad Port 01, mode 7, name IR Tx
90842b0e7cad Port 01, mode 7, RAW min 0, max 65535
90842b0e7cad Port 01, mode 7, PCT min 0, max 100
90842b0e7cad Port 01, mode 7, SI min 0, max 65535
90842b0e7cad Port 01, mode 7, SI symbol N/A
90842b0e7cad Port 01, mode 7, Value 1 x 16bit, Decimal format 5.0
The value is 16bit which is exactly the PF IR code size. I will try it out once I have some spare time.