Proving dup_aux_0_4_32

pennyannn · Sep 30, 2024 · a7d3c77 · a7d3c77
1 parent f16261d
commit a7d3c77
Showing 1 changed file with 12 additions and 1 deletion.
diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean
@@ -29,7 +29,18 @@ def dup_aux (e : Nat) (elements : Nat) (esize : Nat)
 theorem dup_aux_0_4_32 (element : BitVec 32) (result : BitVec 128) :
   dup_aux 0 4 32 element result (by omega)
   = element ++ element ++ element ++ element := by
-  sorry
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  simp [state_simp_rules]
+  bv_decide
 
 @[state_simp_rules]
 def exec_dup_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :=