== DCE12 REG() domain: REG(DC_GPIO_DDC1_A)=0x55a7 REG(DC_GPIO_DDCVGA_A)=0x55bf REG(DC_GPIO_I2CPAD_A)=0x55d7 ==
(VBIOS gpio_pin_lut data_a_reg_index stores these full offsets — bios_parser2.c:537-539)

== T1: DDC/VGA/I2CPAD offsets return success WITHOUT writing *id (DF-4945) ==
(dal_gpio_service_create_irq gpio_service.c:148 declares 'enum gpio_id id;' uninitialized)
offset_to_id(REG(DDCVGA),0x100) = true en=6(id==0x7b7b7b7b UNTOUCHED)
  -> BUG(DF-4945): success, *id never written; garbage id==GPIO_ID_HPD(3)
     => dal_gpio_create(HPD, en=6) with en>=6 indexes hpd_regs[6] OOB
offset_to_id(REG(I2CPAD),0x1)    = true en=7(id==0x7b7b7b7b UNTOUCHED)
  -> BUG(DF-4945): en=7 >= hpd_regs[6]: garbage-id==HPD path is OOB

== T2 (negative): no GPIOPAD case in DCE12 translate ==
    [ASSERT_CRITICAL hit]
offset_to_id(0x183,1<<20) = false (no GPIOPAD mapping -> rejected: OK; the dce80 cross-domain producer does not exist here)

2 contract-violation reproductions
RUN_EXIT=0