diff --git a/Test/Arith/identity.mlir b/Test/Arith/identity.mlir
index 88264b7..3b47a16 100644
--- a/Test/Arith/identity.mlir
+++ b/Test/Arith/identity.mlir
@@ -1,19 +1,65 @@
 // RUN: veir-opt %s | filecheck %s
 
 "builtin.module"() ({
-^bb0():
-  %5 = "arith.constant"() <{ value = 13 : i32 }> : () -> i32
+^4():
+  %5 = "arith.constant"() <{ "value" = 13 : i32 }> : () -> i32
   %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32
-  %7 = "arith.subi"(%5, %5) : (i32, i32) -> i32
-  %8 = "arith.muli"(%5, %5) : (i32, i32) -> i32
-  %9 = "arith.andi"(%5, %5) : (i32, i32) -> i32
+  %70, %71 = "arith.addui_extended"(%5, %5) : (i32, i32) -> (i32, i32)
+  %8 = "arith.andi"(%5, %5) : (i32, i32) -> i32
+  %9 = "arith.ceildivsi"(%5, %5) : (i32, i32) -> i32
+  %10 = "arith.ceildivui"(%5, %5) : (i32, i32) -> i32
+  %11 = "arith.cmpi"(%5, %5) : (i32, i32) -> i1
+  %12 = "arith.divsi"(%5, %5) : (i32, i32) -> i32
+  %13 = "arith.divui"(%5, %5) : (i32, i32) -> i32
+  %14 = "arith.extui"(%5) : (i32) -> i32
+  %15 = "arith.floordivsi"(%5, %5) : (i32, i32) -> i32
+  %16 = "arith.maxsi"(%5, %5) : (i32, i32) -> i32
+  %17 = "arith.maxui"(%5, %5) : (i32, i32) -> i32
+  %18 = "arith.minsi"(%5, %5) : (i32, i32) -> i32
+  %19 = "arith.minui"(%5, %5) : (i32, i32) -> i32
+  %20 = "arith.muli"(%5, %5) : (i32, i32) -> i32
+  %210, %211 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> (i32, i32)
+  %220, %221 = "arith.mului_extended"(%5, %5) : (i32, i32) -> (i32, i32)
+  %23 = "arith.ori"(%5, %5) : (i32, i32) -> i32
+  %24 = "arith.remsi"(%5, %5) : (i32, i32) -> i32
+  %25 = "arith.remui"(%5, %5) : (i32, i32) -> i32
+  %26 = "arith.select"(%11, %5, %5) : (i1, i32, i32) -> i32
+  %27 = "arith.shli"(%5, %5) : (i32, i32) -> i32
+  %28 = "arith.shrsi"(%5, %5) : (i32, i32) -> i32
+  %29 = "arith.shrui"(%5, %5) : (i32, i32) -> i32
+  %30 = "arith.subi"(%5, %5) : (i32, i32) -> i32
+  %31 = "arith.trunci"(%5) : (i32) -> i32
+  %32 = "arith.xori"(%5, %5) : (i32, i32) -> i32
 }) : () -> ()
 
 // CHECK:      "builtin.module"() ({
 // CHECK-NEXT: ^4():
-// CHECK-NEXT:    %5 = "arith.constant"() <{"value" = 13 : i32}> : () -> i32
-// CHECK-NEXT:    %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32
-// CHECK-NEXT:    %7 = "arith.subi"(%5, %5) : (i32, i32) -> i32
-// CHECK-NEXT:    %8 = "arith.muli"(%5, %5) : (i32, i32) -> i32
-// CHECK-NEXT:    %9 = "arith.andi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %5 = "arith.constant"() <{"value" = 13 : i32}> : () -> i32
+// CHECK-NEXT:   %6 = "arith.addi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %7_0, %7_1 = "arith.addui_extended"(%5, %5) : (i32, i32) -> (i32, i32)
+// CHECK-NEXT:   %8 = "arith.andi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %9 = "arith.ceildivsi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %10 = "arith.ceildivui"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %11 = "arith.cmpi"(%5, %5) : (i32, i32) -> i1
+// CHECK-NEXT:   %12 = "arith.divsi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %13 = "arith.divui"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %14 = "arith.extui"(%5) : (i32) -> i32
+// CHECK-NEXT:   %15 = "arith.floordivsi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %16 = "arith.maxsi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %17 = "arith.maxui"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %18 = "arith.minsi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %19 = "arith.minui"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %20 = "arith.muli"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %21_0, %21_1 = "arith.mulsi_extended"(%5, %5) : (i32, i32) -> (i32, i32)
+// CHECK-NEXT:   %22_0, %22_1 = "arith.mului_extended"(%5, %5) : (i32, i32) -> (i32, i32)
+// CHECK-NEXT:   %23 = "arith.ori"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %24 = "arith.remsi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %25 = "arith.remui"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %26 = "arith.select"(%11, %5, %5) : (i1, i32, i32) -> i32
+// CHECK-NEXT:   %27 = "arith.shli"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %28 = "arith.shrsi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %29 = "arith.shrui"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %30 = "arith.subi"(%5, %5) : (i32, i32) -> i32
+// CHECK-NEXT:   %31 = "arith.trunci"(%5) : (i32) -> i32
+// CHECK-NEXT:   %32 = "arith.xori"(%5, %5) : (i32, i32) -> i32
 // CHECK-NEXT: }) : () -> ()
diff --git a/Veir/OpCode.lean b/Veir/OpCode.lean
index 48d07ac..dd2ad35 100644
--- a/Veir/OpCode.lean
+++ b/Veir/OpCode.lean
@@ -17,11 +17,34 @@ namespace Veir
 
 @[opcodes]
 inductive Arith where
-| constant
 | addi
-| subi
-| muli
+| addui_extended
 | andi
+| ceildivsi
+| ceildivui
+| cmpi
+| constant
+| divsi
+| divui
+| extui
+| floordivsi
+| maxsi
+| maxui
+| minsi
+| minui
+| muli
+| mulsi_extended
+| mului_extended
+| ori
+| remsi
+| remui
+| select
+| shli
+| shrsi
+| shrui
+| subi
+| trunci
+| xori
 
 @[opcodes]
 inductive Builtin where
@@ -152,6 +175,7 @@ public section
   An operation code (OpCode) identifies the type of an operation.
   Each OpCode corresponds to a specific operation.
 -/
+set_option maxRecDepth 100000
 #generate_op_codes
 
 end
diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean
index d1b3184..ec1f4e5 100644
--- a/Veir/Verifier.lean
+++ b/Veir/Verifier.lean
@@ -16,6 +16,66 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op
   match op.getOpType ctx opIn with
   | .builtin_unregistered => pure ()
   /- ARITH -/
+  | .arith_addi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_addui_extended => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 2 then
+      throw "Expected 2 results"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_andi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_ceildivsi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_ceildivui => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_cmpi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
   | .arith_constant => do
     if op.getNumOperands ctx opIn ≠ 0 then
       throw "Expected 0 operands"
@@ -26,7 +86,7 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op
     if op.getNumSuccessors ctx opIn ≠ 0 then
       throw "Expected 0 successors"
     pure ()
-  | .arith_addi => do
+  | .arith_divsi => do
     if op.getNumOperands ctx opIn ≠ 2 then
       throw "Expected 2 operands"
     if op.getNumResults ctx opIn ≠ 1 then
@@ -36,7 +96,67 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op
     if op.getNumSuccessors ctx opIn ≠ 0 then
       throw "Expected 0 successors"
     pure ()
-  | .arith_subi => do
+  | .arith_divui => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_extui => do
+    if op.getNumOperands ctx opIn ≠ 1 then
+      throw "Expected 1 operand"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_floordivsi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_maxsi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_maxui => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_minsi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_minui => do
     if op.getNumOperands ctx opIn ≠ 2 then
       throw "Expected 2 operands"
     if op.getNumResults ctx opIn ≠ 1 then
@@ -56,7 +176,117 @@ def OperationPtr.verifyLocalInvariants (op : OperationPtr) (ctx : IRContext) (op
     if op.getNumSuccessors ctx opIn ≠ 0 then
       throw "Expected 0 successors"
     pure ()
-  | .arith_andi => do
+  | .arith_mulsi_extended => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 2 then
+      throw "Expected 2 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_mului_extended => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 2 then
+      throw "Expected 2 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_ori => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_remsi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_remui => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_select => do
+    if op.getNumOperands ctx opIn ≠ 3 then
+      throw "Expected 3 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_shli => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_shrsi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_shrui => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_subi => do
+    if op.getNumOperands ctx opIn ≠ 2 then
+      throw "Expected 2 operands"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_trunci => do
+    if op.getNumOperands ctx opIn ≠ 1 then
+      throw "Expected 1 operand"
+    if op.getNumResults ctx opIn ≠ 1 then
+      throw "Expected 1 result"
+    if op.getNumRegions ctx opIn ≠ 0 then
+      throw "Expected 0 regions"
+    if op.getNumSuccessors ctx opIn ≠ 0 then
+      throw "Expected 0 successors"
+    pure ()
+  | .arith_xori => do
     if op.getNumOperands ctx opIn ≠ 2 then
       throw "Expected 2 operands"
     if op.getNumResults ctx opIn ≠ 1 then