And, even if not that, the 0x0000_0000_FFFF_FFFF constant could be generated via 2 instrs of

    li    a0, -1
    srli  a0, a0, 32