Add ARM NEON instructions BIF and REV32 (vector)

[nebeid]

Adds decode + semantics + simulator entries for two ARM NEON instructions
needed for verification of the AES-GCM optimised implementation:

• BIF (Bitwise Insert if False) — 0q101110111 Rm 000111 Rn Rd
• REV32 (vector, reverse within 32-bit elements) — 0q101110 size 100000000010 Rn Rd

Changes

• arm/proofs/decode.ml: bit-pattern decode entries
• arm/proofs/instruction.ml: semantic definitions, ALT rules, operation list
• arm/proofs/simulator_iclasses.ml: sematest entries

Testing

Focused sematest (only BIF + REV32 in iclasses): 13,413 random instances
across 4 parallel processes, 0 failures. Cosimulated against hardware on
AArch64.

[jargh]

I believe this is all absolutely functionally correct, thank you! However, I would like to suggest a stylistic modification to the core arm_REV32_VEC function as follows:

let arm_REV32_VEC = define
 `arm_REV32_VEC Rd Rn esize =
    \s. let n:(128)word = read Rn (s:armstate) in
        let n_reversed = usimd4 (word_reversefields esize) n in
        (Rd := n_reversed) s`;;

This is using the word library's word_reversefields, which I think gives a more clear and simple implementation than the explicit word joining used currently.