diff --git a/arm/proofs/decode.ml b/arm/proofs/decode.ml
index 328aa77df..4bd260f71 100644
--- a/arm/proofs/decode.ml
+++ b/arm/proofs/decode.ml
@@ -105,7 +105,10 @@ let arm_ldst3 = new_definition `arm_ldst3 ld Rt1 =
 let arm_adv_simd_expand_imm = new_definition
   `(arm_adv_simd_expand_imm:(8)word->(1)word->(4)word->((64)word)option)
       abcdefgh op cmode =
-    if val cmode = 14 /\ val op = 1 then
+    if val cmode = 14 /\ val op = 0 then
+      // MOVI byte: 8-bit immediate replicated to all bytes
+      SOME(word_duplicate abcdefgh:int64)
+    else if val cmode = 14 /\ val op = 1 then
       let rep8 = \(x:bool). if x then (word 255:(8)word) else (word 0) in
       let res: (64)word =
         word_join (rep8 (bit 7 abcdefgh))
@@ -511,6 +514,10 @@ let decode = new_definition `!w:int32. decode w =
     // BIT
     SOME (arm_BIT (QREG' Rd) (QREG' Rn) (QREG' Rm) (if q then 128 else 64))
 
+  | [0:1; q; 0b101110111:9; Rm:5; 0b000111:6; Rn:5; Rd:5] ->
+    // BIF
+    SOME (arm_BIF (QREG' Rd) (QREG' Rn) (QREG' Rm) (if q then 128 else 64))
+
   // Two sizes of FCSEL, not allowing FP16 case at all
   | [0b00011110:8; 0b00:2; 0b1:1; Rm:5; cond:4; 0b11:2; Rn:5; Rd:5] ->
     SOME (arm_FCSEL (QREG' Rd) (QREG' Rn) (QREG' Rm) (Condition cond) 32)
@@ -548,6 +555,16 @@ let decode = new_definition `!w:int32. decode w =
       SOME (arm_EXT (QREG' Rd) (QREG' Rn) (QREG' Rm) pos)
     else NONE
 
+  | [0:1; q; 0:1; 0b011110:6; 0b0000:4; abc:3; 0b1110:4; 0b01:2; defgh:5; Rd:5] ->
+    // MOVI (op=0, cmode=1110): 8-bit byte immediate replicated to all lanes
+    let abcdefgh:(8)word = word_join abc defgh in
+    let imm = arm_adv_simd_expand_imm abcdefgh (word 0:(1)word) (word 0b1110:(4)word) in
+    (match imm with
+    | SOME imm ->
+        if q then SOME (arm_MOVI (QREG' Rd) imm)
+        else SOME (arm_MOVI (DREG' Rd) imm)
+    | NONE -> NONE)
+
   | [0:1; q; 1:1; 0b011110:6; immh:4; abc:3; cmode:4; 0b01:2; defgh:5; Rd:5] ->
     // MOVI (op=1), USHR (Vector), USRA (Vector), SLI (Vector), SRI (vector)
     if val immh = 0 then
@@ -732,6 +749,13 @@ let decode = new_definition `!w:int32. decode w =
       let esize:(64)word = word_shl (word 0b1000: (64)word) (val size) in
       SOME (arm_REV64_VEC (QREG' Rd) (QREG' Rn) (val esize))
 
+  | [0:1; q; 0b101110:6; size:2; 0b100000000010:12; Rn:5; Rd:5] ->
+    // REV32 (vector)
+    if size = (word 0b10: (2)word) \/ size = (word 0b11: (2)word) then NONE
+    else
+      let esize:(64)word = word_shl (word 0b1000: (64)word) (val size) in
+      SOME (arm_REV32_VEC (QREG' Rd) (QREG' Rn) (val esize) (if q then 128 else 64))
+
   | [0b01101110000:11; imm5:5; 0:1; imm4:4; 1:1; Rn:5; Rd:5] ->
     // INS, or "MOV (element)"
     let size = word_ctz imm5 in
diff --git a/arm/proofs/instruction.ml b/arm/proofs/instruction.ml
index 9a6620907..6bdd6fa0e 100644
--- a/arm/proofs/instruction.ml
+++ b/arm/proofs/instruction.ml
@@ -988,6 +988,18 @@ let arm_BIT = define
           let out':(64)word = word_subword out (0,64) in
           (Rd := word_zx out':(128)word) s`;;
 
+let arm_BIF = define
+ `arm_BIF Rd Rn Rm datasize =
+    \s. let m = read Rm s
+        and n = read Rn s
+        and d = read Rd s in
+        let out:(128)word = word_or (word_and d m) (word_and n (word_not m)) in
+        if datasize = 128 then
+          (Rd := out) s
+        else
+          let out':(64)word = word_subword out (0,64) in
+          (Rd := word_zx out':(128)word) s`;;
+
 (*** As with x86, we have relative and absolute versions of branch & link ***)
 (*** The absolute one gives a natural way of handling linker-insertions.  ***)
 
@@ -1474,6 +1486,22 @@ let arm_REV64_VEC = define
           : (16)word) n_reversed16 in
         (Rd := n_reversed8) s`;;
 
+let arm_REV32_VEC = define
+ `arm_REV32_VEC Rd Rn esize datasize =
+    \s. let n:(128)word = read Rn (s:armstate) in
+        let n_reversed16 = usimd4 (\x. word_join
+          (word_subword x (0,16):(16)word) (word_subword x (16,16):(16)word)
+          : (32)word) n in
+        if esize = 16 then
+          if datasize = 128 then (Rd := n_reversed16) s
+          else (Rd := word_zx (word_subword n_reversed16 (0,64):(64)word):(128)word) s
+        else
+        let n_reversed8 = usimd8 (\x. word_join
+          (word_subword x (0,8):(8)word) (word_subword x (8,8):(8)word)
+          : (16)word) n_reversed16 in
+        if datasize = 128 then (Rd := n_reversed8) s
+        else (Rd := word_zx (word_subword n_reversed8 (0,64):(64)word):(128)word) s`;;
+
 let arm_RORV = define
  `arm_RORV Rd Rm Rn =
     \s. let m = read Rm s
@@ -3416,6 +3444,7 @@ let arm_PMUL_VEC_ALT =   EXPAND_SIMD_RULE arm_PMUL_VEC;;
 let arm_PMULL_VEC_ALT =  EXPAND_SIMD_RULE arm_PMULL_VEC;;
 let arm_PMULL2_VEC_ALT = EXPAND_SIMD_RULE arm_PMULL2_VEC;;
 let arm_REV64_VEC_ALT =  EXPAND_SIMD_RULE arm_REV64_VEC;;
+let arm_REV32_VEC_ALT =  EXPAND_SIMD_RULE arm_REV32_VEC;;
 let arm_SHL_VEC_ALT =    EXPAND_SIMD_RULE arm_SHL_VEC;;
 let arm_SSHR_VEC_ALT =   EXPAND_SIMD_RULE arm_SSHR_VEC;;
 let arm_SHRN_ALT =       EXPAND_SIMD_RULE arm_SHRN;;
@@ -3536,7 +3565,7 @@ let ARM_OPERATION_CLAUSES =
     (*** Alphabetically sorted, new alphabet appears in the next line ***)
       [arm_ADC; arm_ADCS_ALT; arm_ADD; arm_ADD_VEC_ALT; arm_ABS_VEC_ALT; arm_ADDS_ALT; arm_ADR;
        arm_ADRP; arm_AND; arm_AND_VEC; arm_ANDS; arm_ASR; arm_ASRV;
-       arm_B; arm_BCAX; arm_BFM; arm_BIC; arm_BIC_VEC; arm_BICS; arm_BIT;
+       arm_B; arm_BCAX; arm_BFM; arm_BIC; arm_BIC_VEC; arm_BICS; arm_BIF; arm_BIT;
        arm_BL; arm_BL_ABSOLUTE; arm_Bcond;
        arm_CBNZ_ALT; arm_CBZ_ALT; arm_CCMN; arm_CCMP; arm_CLZ;
        arm_CMGE_VEC_ALT; arm_CMGT_VEC_ALT; arm_CMHI_VEC_ALT; arm_CMLE_VEC_ZERO_ALT; arm_CNT_ALT;
@@ -3554,7 +3583,7 @@ let ARM_OPERATION_CLAUSES =
        arm_ORN; arm_ORR; arm_ORR_VEC;
        arm_PMUL_VEC_ALT;
        arm_PMULL_VEC_ALT; arm_PMULL2_VEC_ALT;
-       arm_RET; arm_REV; arm_REV64_VEC_ALT; arm_RORV;
+       arm_RET; arm_REV; arm_REV32_VEC_ALT; arm_REV64_VEC_ALT; arm_RORV;
        arm_SBC; arm_SBCS_ALT; arm_SBFM; arm_SHL_VEC_ALT; arm_SHRN_ALT;
        arm_SRSHR_VEC_ALT;
        arm_SSHR_VEC_ALT;