Issue with GICv3 ICC_IGRPEN1_EL1.Enable bit in Foundation Platform

Running a simple custom baremetal application atop TF-A on Foundation Platform. I am having an issue with enabling group 1 interrupts in the GICv3 CPU interface registers.

The spec says "The Non-secure ICC_IGRPEN1_EL1.Enable bit is a read/write alias of the ICC_IGRPEN1_EL3.EnableGrp1NS bit.". However, when I write ICC_IGRPEN1_EL1.Enable from EL1 this view of the bit is updated, but ICC_IGRPEN1_EL3.EnableGrp1NS does not budge, and group 1 interrupts stay effectively disabled for EL1.

At first I thought this had something to do with some EL2 configuration (the baremetal app jumps from EL2 to EL1 as soon as it starts) . The spec states "Virtual accesses to this register update ICH_VMCR_EL2.VENG1.". However, this bit does also does not change.

Later I noticed that if an SMC call was made to TF-A after setting ICC_IGRPEN1_EL1.Enable,   ICC_IGRPEN1_EL3.EnableGrp1NS bit would be set when execution returned to EL1. I assumed TF-A was doing something that triggered this, but when debugging using step-by-step instruction, I noticed that as soon as the SMC instruction was executed, i.e. execution entered EL3, ICC_IGRPEN1_EL3.EnableGrp1NS  was updated.

Further I noticed that if I set ICC_IGRPEN1_EL1.Enable through the debugger register view, independtly of the exception level the debugger was stopped at, ICC_IGRPEN1_EL3.EnableGrp1NS is correctly updated.

Am I missing something, or might this be a bug in the model?