Use structural recursion and rfl (leanprover#158)

### Description:

This PR changes well-founded recursion to structural recursion in
several functions and this allows us to use `rfl` for the tests that
associate with these functions.

Relevant PR: leanprover#151

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine? yes

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

---------

Co-authored-by: Shilpi Goel <shigoel@gmail.com>

Arm/BitVec.lean

@@ -294,7 +294,7 @@ abbrev partInstall (hi lo : Nat) (val : BitVec (hi - lo + 1)) (x : BitVec n): Bi
   let x_with_hole := x &&& mask_with_hole
   x_with_hole ||| val_aligned
 
-example : (partInstall 3 0 0xC#4 0xAB0D#16 = 0xAB0C#16) := by native_decide
+example : (partInstall 3 0 0xC#4 0xAB0D#16 = 0xAB0C#16) := rfl
 
 def flattenTR {n : Nat} (xs : List (BitVec n)) (i : Nat)
   (acc : BitVec len) (H : n > 0) : BitVec len :=
@@ -308,37 +308,30 @@ def flattenTR {n : Nat} (xs : List (BitVec n)) (i : Nat)
 /-- Reverse bits of a bit-vector. -/
 def reverse (x : BitVec n) : BitVec n :=
   let rec reverseTR (x : BitVec n) (i : Nat) (acc : BitVec n) :=
-    if i < n then
-      let xi := extractLsb i i x
-      have h : i - i + 1 = (n - i - 1) - (n - i - 1) + 1 := by omega
-      let acc := BitVec.partInstall (n - i - 1) (n - i - 1) (BitVec.cast h xi) acc
-      reverseTR x (i + 1) acc
-    else acc
-  reverseTR x 0 $ BitVec.zero n
-
-example : reverse 0b11101#5 = 0b10111#5 := by
-  -- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-  simp [reverse, reverse.reverseTR]
-  rfl
+    match i with
+    | 0 => acc
+    | j + 1 =>
+      let xi : BitVec 1 := extractLsb' (i - 1) 1 x
+      let acc := BitVec.partInstall (n - i) (n - i) (xi.cast (by omega)) acc
+      reverseTR x j acc
+  reverseTR x n $ BitVec.zero n
+
+example : reverse 0b11101#5 = 0b10111#5 := rfl
 
 /-- Split a bit-vector into sub vectors of size e. -/
 def split (x : BitVec n) (e : Nat) (h : 0 < e): List (BitVec e) :=
   let rec splitTR (x : BitVec n) (e : Nat) (h : 0 < e)
     (i : Nat) (acc : List (BitVec e)) : List (BitVec e) :=
-    if i < n/e then
-      let lo := i * e
-      let hi := lo + e - 1
-      have h₀ : hi - lo + 1 = e := by simp only [hi, lo]; omega
-      let part : BitVec e := BitVec.cast h₀ (extractLsb hi lo x)
+    match i with
+    | 0 => acc
+    | j + 1 =>
+      let lo := (n / e - i) * e
+      let part : BitVec e := extractLsb' lo e x
       let newacc := part :: acc
-      splitTR x e h (i + 1) newacc
-    else acc
-  splitTR x e h 0 []
+      splitTR x e h j newacc
+  splitTR x e h (n / e) []
 
-example : split 0xabcd1234#32 8 (by omega) = [0xab#8, 0xcd#8, 0x12#8, 0x34#8] :=
-  by
-  -- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-  simp [split, split.splitTR]
+example : split 0xabcd1234#32 8 (by omega) = [0xab#8, 0xcd#8, 0x12#8, 0x34#8] := rfl
 
 /-- Reverse a list of bit vectors and flatten the list. -/
 def revflat (x : List (BitVec n)) : BitVec (n * x.length) :=
@@ -398,10 +391,10 @@ theorem bitvec_zero_is_unique (x : BitVec 0) :
   simp only [Nat.pow_zero, Fin.fin_one_eq_zero, Nat.le_refl]
 
 theorem fin_bitvec_add (x y : BitVec n) :
-  (x.toFin + y.toFin) = (x + y).toFin := by rfl
+  (x.toFin + y.toFin) = (x + y).toFin := rfl
 
 theorem fin_bitvec_sub (x y : BitVec n) :
-  (x.toFin - y.toFin) = (x - y).toFin := by rfl
+  (x.toFin - y.toFin) = (x - y).toFin := rfl
 
 theorem fin_bitvec_or (x y : BitVec n) :
   (x ||| y).toFin = (x.toFin ||| y.toFin) := by

Arm/Decode.lean

@@ -172,156 +172,135 @@ def decode_raw_inst (i : BitVec 32) : Option ArmInst :=
 example : decode_raw_inst 0x91000421#32 =
           (ArmInst.DPI (DataProcImmInst.Add_sub_imm
           {sf := 1#1, op := 0#1, S := 0#1, sh := 0#1,
-            imm12 := 1#12, Rn := 1#5, Rd := 1#5})) := by
-        rfl
+            imm12 := 1#12, Rn := 1#5, Rd := 1#5})) := rfl
 
 -- adc x1, x1, x0
 example : decode_raw_inst 0b00011010000000000000000000100001#32 =
           (ArmInst.DPR (DataProcRegInst.Add_sub_carry
                { sf := 0#1, op := 0#1, S := 0#1, Rm := 0#5,
-                 Rn := 1#5, Rd := 1#5 })) := by
-        rfl
+                 Rn := 1#5, Rd := 1#5 })) := rfl
 
 -- sha512h q3, q5, v6.2d
 example : decode_raw_inst 0xce6680a3#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_three_reg_sha512
                { Rm := 6#5, O := 0#1, opcode := 0#2,
-                 Rn := 5#5, Rd := 3#5 })) := by
-        rfl
+                 Rn := 5#5, Rd := 3#5 })) := rfl
 
 -- sha512h2 q3, q1, v0.2d
 example : decode_raw_inst 0xce608423#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_three_reg_sha512
                { Rm := 0#5, O := 0#1, opcode := 1#2,
-                 Rn := 1#5, Rd := 3#5 })) := by
-        rfl
+                 Rn := 1#5, Rd := 3#5 })) := rfl
 
 -- sha512su1 v16.2d, v23.2d, v7.2d
 example : decode_raw_inst 0xce678af0#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_three_reg_sha512
           { Rm := 7#5, O := 0#1, opcode := 2#2,
-            Rn := 23#5, Rd := 16#5 })) := by
-        rfl
+            Rn := 23#5, Rd := 16#5 })) := rfl
 
 -- sha512su0 v16.2d, v17.2d
 example : decode_raw_inst 0xcec08230#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_two_reg_sha512
-               { opcode := 0#2, Rn := 17#5, Rd := 16#5 })) := by
-        rfl
+               { opcode := 0#2, Rn := 17#5, Rd := 16#5 })) := rfl
 
 -- ldr	q16, [x0], #16
 example : decode_raw_inst 0x3cc10410#32 =
           (ArmInst.LDST (LDSTInst.Reg_imm_post_indexed
                { size := 0x0#2, V := 0x1#1, opc := 0x3#2, imm9 := 0x010#9,
-                 Rn := 0x00#5, Rt := 0x10#5 })) := by
-        rfl
+                 Rn := 0x00#5, Rt := 0x10#5 })) := rfl
 
 -- stp	x29, x30, [sp, #-16]!
 example : decode_raw_inst 0xa9bf7bfd#32 =
           (ArmInst.LDST (LDSTInst.Reg_pair_pre_indexed
                { opc := 0x2#2, V := 0x0#1, L := 0x0#1, imm7 := 0x7e#7,
-                 Rt2 := 0x1e#5, Rn := 0x1f#5, Rt := 0x1d#5 })) := by
-        rfl
+                 Rt2 := 0x1e#5, Rn := 0x1f#5, Rt := 0x1d#5 })) := rfl
 
 -- ld1	{v16.16b-v19.16b}, [x1], #64
 example : decode_raw_inst 0x4cdf2030#32 =
           (ArmInst.LDST
                (LDSTInst.Advanced_simd_multiple_struct_post_indexed
                  { Q := 0x1#1, L := 0x1#1, Rm := 0x1f#5, opcode := 0x2#4,
-                   size := 0x0#2, Rn := 0x01#5, Rt := 0x10#5 })) := by
-        rfl
+                   size := 0x0#2, Rn := 0x01#5, Rt := 0x10#5 })) := rfl
 
 -- ld1	{v24.2d}, [x3], #16
 example : decode_raw_inst 0x4cdf7c78#32 =
           (ArmInst.LDST
                (LDSTInst.Advanced_simd_multiple_struct_post_indexed
                  { Q := 0x1#1, L := 0x1#1, Rm := 0x1f#5, opcode := 0x7#4,
-                   size := 0x3#2, Rn := 0x03#5, Rt := 0x18#5 })) := by
-        rfl
+                   size := 0x3#2, Rn := 0x03#5, Rt := 0x18#5 })) := rfl
 
 -- ld1	{v0.2d-v3.2d}, [x0]
 example : decode_raw_inst 0x4c402c00#32 =
           (ArmInst.LDST
           (LDSTInst.Advanced_simd_multiple_struct
             { Q := 0x1#1, L := 0x1#1, opcode := 0x2#4,
-              size := 0x3#2, Rn := 0x00#5, Rt := 0x00#5 })) := by
-        rfl
+              size := 0x3#2, Rn := 0x00#5, Rt := 0x00#5 })) := rfl
 
 -- st1	{v0.2d-v3.2d}, [x0]
 example :  decode_raw_inst 0x4c002c00#32 =
            (ArmInst.LDST
                 (LDSTInst.Advanced_simd_multiple_struct
                   { Q := 0x1#1, L := 0x0#1, opcode := 0x2#4, size := 0x3#2,
-                    Rn := 0x00#5, Rt := 0x00#5 })) := by rfl
+                    Rn := 0x00#5, Rt := 0x00#5 })) := rfl
 
 -- add	v24.2d, v24.2d, v16.2d
 example : decode_raw_inst 0x4ef08718#32 =
   (ArmInst.DPSFP (DataProcSFPInst.Advanced_simd_three_same
        { Q := 0x1#1, U := 0x0#1, size := 0x3#2, Rm := 0x10#5,
-         opcode := 0x10#5, Rn := 0x18#5, Rd := 0x18#5 })) := by
-  rfl
+         opcode := 0x10#5, Rn := 0x18#5, Rd := 0x18#5 })) := rfl
 
 -- adrp x3, ...
 example : decode_raw_inst 0xd0000463#32 =
           (ArmInst.DPI (DataProcImmInst.PC_rel_addressing
                { op := 0x1#1, immlo := 0x2#2, immhi := 0x00023#19,
-                 Rd := 0x03#5 })) := by
-        rfl
+                 Rd := 0x03#5 })) := rfl
 
 -- csel	x1, x1, x4, ne
 example : decode_raw_inst 0x9a841021#32 =
           (ArmInst.DPR (DataProcRegInst.Conditional_select
                { sf := 0x1#1, op := 0x0#1, S := 0x0#1, Rm := 0x04#5,
                  cond := 0x1#4, op2 := 0x0#2, Rn := 0x01#5,
-                 Rd := 0x01#5 })) := by
-        rfl
+                 Rd := 0x01#5 })) := rfl
 
 -- b ...
 example : decode_raw_inst 0x14000001#32 =
           (ArmInst.BR (BranchInst.Uncond_branch_imm
-               { op := 0x0#1, imm26 := 0x0000001#26 })) := by
-        rfl
+               { op := 0x0#1, imm26 := 0x0000001#26 })) := rfl
 
 -- b.le ...
 example : decode_raw_inst 0x5400000d#32 =
           (ArmInst.BR (BranchInst.Cond_branch_imm
-               { imm19 := 0x00000#19, o0 := 0, cond := 0xd#4})) := by
-        rfl
+               { imm19 := 0x00000#19, o0 := 0, cond := 0xd#4})) := rfl
 
 -- ret
 example : decode_raw_inst 0xd65f03c0#32 =
           (ArmInst.BR (BranchInst.Uncond_branch_reg
                { opc := 0x2#4, op2 := 0x1f#5, op3 := 0x00#6,
-                 Rn := 0x1e#5, op4 := 0x00#5 })) := by
-        rfl
+                 Rn := 0x1e#5, op4 := 0x00#5 })) := rfl
 
 -- cbnz	x2, ...
 example : decode_raw_inst 0xb5ffc382#32 =
           (ArmInst.BR (BranchInst.Compare_branch
                { sf := 0x1#1, op := 0x1#1, imm19 := 0x7fe1c#19,
-                 Rt := 0x02#5 })) := by
-        rfl
+                 Rt := 0x02#5 })) := rfl
 
 -- ext	v24.16b, v24.16b, v24.16b, #8
 example : decode_raw_inst 0x6e184318#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Advanced_simd_extract
                { Q := 0x1#1, op2 := 0x0#2, Rm := 0x18#5, imm4 := 0x8#4,
-                 Rn := 0x18#5, Rd := 0x18#5 })) := by
-        rfl
+                 Rn := 0x18#5, Rd := 0x18#5 })) := rfl
 
 -- mov	x29, sp
 example : decode_raw_inst 0x910003fd#32 =
           (ArmInst.DPI (DataProcImmInst.Add_sub_imm
                { sf := 0x1#1, op := 0x0#1, S := 0x0#1, sh := 0x0#1,
-                 imm12 := 0x000#12, Rn := 0x1f#5, Rd := 0x1d#5 })) := by
-        rfl
+                 imm12 := 0x000#12, Rn := 0x1f#5, Rd := 0x1d#5 })) := rfl
 
 -- ldr	q0, [x4]
 example : decode_raw_inst 0x3dc00080#32 =
           (ArmInst.LDST (LDSTInst.Reg_unsigned_imm
                { size := 0x0#2, V := 0x1#1, opc := 0x3#2,
-                 imm12 := 0x000#12, Rn := 0x04#5, Rt := 0x00#5 })) := by
-        rfl
+                 imm12 := 0x000#12, Rn := 0x04#5, Rt := 0x00#5 })) := rfl
 
 -- str	q4, [x2], #16
 example : decode_raw_inst 0x3c810444#32 =
@@ -335,29 +314,25 @@ example : decode_raw_inst 0x4e200800#32 =
           (ArmInst.DPSFP
                (DataProcSFPInst.Advanced_simd_two_reg_misc
                  { Q := 0x1#1, U := 0x0#1, size := 0x0#2, opcode := 0x00#5,
-                   Rn := 0x00#5, Rd := 0x00#5 })) := by
-        rfl
+                   Rn := 0x00#5, Rd := 0x00#5 })) := rfl
 
 -- aese	v0.16b, v16.16b
 example : decode_raw_inst 0x4e284a00#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_aes
                { size := 0x0#2, opcode := 0x04#5,
-                 Rn := 0x10#5, Rd := 0x00#5 })) := by
-        rfl
+                 Rn := 0x10#5, Rd := 0x00#5 })) := rfl
 
 -- aesmc v0.16b, v0.16b
 example : decode_raw_inst 0x4e286800#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_aes
                { size := 0x0#2, opcode := 0x06#5,
-                 Rn := 0x00#5, Rd := 0x00#5 })) := by
-        rfl
+                 Rn := 0x00#5, Rd := 0x00#5 })) := rfl
 
 -- mov	x28, v0.d[0]
 example : decode_raw_inst 0x4e083c1c#32 =
           ArmInst.DPSFP (DataProcSFPInst.Advanced_simd_copy
               { Q := 0x1#1, op := 0x0#1, imm5 := 0x08#5,
-                imm4 := 0x7#4, Rn := 0x00#5, Rd := 0x1c#5 }) := by
-        rfl
+                imm4 := 0x7#4, Rn := 0x00#5, Rd := 0x1c#5 }) := rfl
 
 -- ext v16.8B, v10.8B, v24.8B, #2
 example : decode_raw_inst 0x2e181150#32 =
@@ -368,8 +343,7 @@ example : decode_raw_inst 0x2e181150#32 =
               Rm := 0x18#5,
               imm4 := 0x2#4,
               Rn := 0x0a#5,
-              Rd := 0x10#5 })) := by
-        rfl
+              Rd := 0x10#5 })) := rfl
 
 -- lsr w0, w0, #1
 example : decode_raw_inst 0x53017c00#32 =
@@ -382,8 +356,7 @@ example : decode_raw_inst 0x53017c00#32 =
                 immr := 0x01#6,
                 imms := 0x1f#6,
                 Rn := 0x00#5,
-                Rd := 0x00#5 })) := by
-        rfl
+                Rd := 0x00#5 })) := rfl
 
 -- ands x30, x3, x17, asr #35
 example : decode_raw_inst 0xea918c7e#32 =
@@ -396,8 +369,7 @@ example : decode_raw_inst 0xea918c7e#32 =
             Rm := 0x11#5,
             imm6 := 0x23#6,
             Rn := 0x03#5,
-            Rd := 0x1e#5})) := by
-        rfl
+            Rd := 0x1e#5})) := rfl
 
 -- eor x15, x28, #0xffffc00000000001
 example : decode_raw_inst 0xd2524b8f#32 =
@@ -409,8 +381,7 @@ example : decode_raw_inst 0xd2524b8f#32 =
             immr := 0x12#6,
             imms := 0x12#6,
             Rn := 0x1c#5,
-            Rd := 0x0f#5 })) := by
-        rfl
+            Rd := 0x0f#5 })) := rfl
 
 -- sub x9, x27, x15, lsl #55
 example : decode_raw_inst 0xcb0fdf69 =
@@ -424,8 +395,7 @@ example : decode_raw_inst 0xcb0fdf69 =
             Rm := 0x0f#5,
             imm6 := 0x37#6,
             Rn := 0x1b#5,
-            Rd := 0x09#5 })) := by
-        rfl
+            Rd := 0x09#5 })) := rfl
 
 -- orr v5.8h, #0x77, lsl #8
 example : decode_raw_inst 0x4f03b6e5 =
@@ -446,8 +416,7 @@ example : decode_raw_inst 0x4f03b6e5 =
             f := 0x1#1,
             g := 0x1#1,
             h := 0x1#1,
-            Rd := 0x05#5 })) := by
-        rfl
+            Rd := 0x05#5 })) := rfl
 
 -- mov v10.h[0] v17.h[6]
 example : decode_raw_inst 0x6e026e2a =
@@ -462,8 +431,7 @@ example : decode_raw_inst 0x6e026e2a =
             imm4 := 0xd#4,
             _fixed4 := 0x1#1,
             Rn := 0x11#5,
-            Rd := 0x0a#5 })) := by
-          rfl
+            Rd := 0x0a#5 })) := rfl
 
 -- fmov v25.d[1], x5
 example : decode_raw_inst 0x9eaf00b9 =
@@ -479,8 +447,7 @@ example : decode_raw_inst 0x9eaf00b9 =
               opcode := 0x7#3,
               _fixed4 := 0x00#6,
               Rn := 0x05#5,
-              Rd := 0x19#5 })) := by
-            rfl
+              Rd := 0x19#5 })) := rfl
 
 -- rev x0, x25
 example : decode_raw_inst 0xdac00f20 =
@@ -493,10 +460,9 @@ example : decode_raw_inst 0xdac00f20 =
               opcode2 := 0x00#5,
               opcode := 0x03#6,
               Rn := 0x19#5,
-              Rd := 0x00#5 })) := by
-          rfl
+              Rd := 0x00#5 })) := rfl
 
 -- Unimplemented
-example : decode_raw_inst 0x00000000#32 = none := by rfl
+example : decode_raw_inst 0x00000000#32 = none := rfl
 
 end Decode

Arm/Exec.lean

@@ -132,8 +132,7 @@ def run (n : Nat) (s : ArmState) : ArmState :=
     run n' s'
 
 theorem run_opener_zero (s : ArmState) :
-  run 0 s = s := by
-  rfl
+  run 0 s = s := rfl
 
 theorem run_opener_general
   (n : Nat) (s : ArmState) :