Bug in ARMv9.4-A specification

[soomin-kim]

Hi,

It seems this line is buggy.

val Reduce__1 : forall 'N 'esize,
  ('N in {16, 32, 64, 128, 256, 512, 1024, 2048} & 'esize in {8, 16, 32, 64} & 'N >= 'esize).
  (ReduceOp, bits('N), int('esize), bool) -> bits('esize)

...

function Reduce__1 (op, input, esize, altfp) = {
    assert(esize == 8 | esize == 16 | esize == 32 | esize == 64);
    result : bits('esize) = undefined;
    if 'N == esize then {
        return(input[esize - 1 .. 0])
    };
    let 'half = DIV('N, 2);
    assert(constraint((('N - 1 - 'half + 1 == 16 | 'N - 1 - 'half + 1 == 32 | 'N - 1 - 'half + 1 == 64 | 'N - 1 - 'half + 1 == 128 | 'N - 1 - 'half + 1 == 256 | 'N - 1 - 'half + 1 == 512 | 'N - 1 - 'half + 1 == 1024 | 'N - 1 - 'half + 1 == 2048) & 'esize in {8, 16, 32, 64} & 'N - 1 - 'half + 1 >= 'esize)));
    ...

In particular, the constraint should include 'N - 1 - 'half + 1 == 8 which can also be valid when 'N == 16 and 'esize == 8.

Thank you.