diff --git a/cranelift/codegen/src/isa/riscv64/inst.isle b/cranelift/codegen/src/isa/riscv64/inst.isle
index 9205446aee..ef6195fe72 100644
--- a/cranelift/codegen/src/isa/riscv64/inst.isle
+++ b/cranelift/codegen/src/isa/riscv64/inst.isle
@@ -761,6 +761,510 @@
       (_ Unit (emit (MInst.FloatSelect op rd tmp x y ty))))
     (writable_reg_to_reg rd)))
 
+
+;;;; Instruction Helpers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; RV32I Base Integer Instruction Set
+
+;; Helper for emitting the `add` instruction.
+;; rd ← rs1 + rs2
+(decl rv_add (Reg Reg) Reg)
+(rule (rv_add rs1 rs2)
+  (alu_rrr (AluOPRRR.Add) rs1 rs2))
+
+;; Helper for emitting the `addi` ("Add Immediate") instruction.
+;; rd ← rs1 + sext(imm)
+(decl rv_addi (Reg Imm12) Reg)
+(rule (rv_addi rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Addi) rs1 imm))
+
+;; Helper for emitting the `sub` instruction.
+;; rd ← rs1 - rs2
+(decl rv_sub (Reg Reg) Reg)
+(rule (rv_sub rs1 rs2)
+  (alu_rrr (AluOPRRR.Sub) rs1 rs2))
+
+;; Helper for emitting the `neg` instruction.
+;; This instruction is a mnemonic for `sub rd, zero, rs1`.
+(decl rv_neg (Reg) Reg)
+(rule (rv_neg rs1)
+  (alu_rrr (AluOPRRR.Sub) (zero_reg) rs1))
+
+;; Helper for emitting the `sll` ("Shift Left Logical") instruction.
+;; rd ← rs1 << rs2
+(decl rv_sll (Reg Reg) Reg)
+(rule (rv_sll rs1 rs2)
+  (alu_rrr (AluOPRRR.Sll) rs1 rs2))
+
+;; Helper for emitting the `slli` ("Shift Left Logical Immediate") instruction.
+;; rd ← rs1 << uext(imm)
+(decl rv_slli (Reg Imm12) Reg)
+(rule (rv_slli rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Slli) rs1 imm))
+
+;; Helper for emitting the `srl` ("Shift Right Logical") instruction.
+;; rd ← rs1 >> rs2
+(decl rv_srl (Reg Reg) Reg)
+(rule (rv_srl rs1 rs2)
+  (alu_rrr (AluOPRRR.Srl) rs1 rs2))
+
+;; Helper for emitting the `srli` ("Shift Right Logical Immediate") instruction.
+;; rd ← rs1 >> uext(imm)
+(decl rv_srli (Reg Imm12) Reg)
+(rule (rv_srli rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Srli) rs1 imm))
+
+;; Helper for emitting the `sra` ("Shift Right Arithmetic") instruction.
+;; rd ← rs1 >> rs2
+(decl rv_sra (Reg Reg) Reg)
+(rule (rv_sra rs1 rs2)
+  (alu_rrr (AluOPRRR.Sra) rs1 rs2))
+
+;; Helper for emitting the `srai` ("Shift Right Arithmetic Immediate") instruction.
+;; rd ← rs1 >> uext(imm)
+(decl rv_srai (Reg Imm12) Reg)
+(rule (rv_srai rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Srai) rs1 imm))
+
+;; Helper for emitting the `or` instruction.
+;; rd ← rs1 ∨ rs2
+(decl rv_or (Reg Reg) Reg)
+(rule (rv_or rs1 rs2)
+  (alu_rrr (AluOPRRR.Or) rs1 rs2))
+
+;; Helper for emitting the `ori` ("Or Immediate") instruction.
+;; rd ← rs1 ∨ uext(imm)
+(decl rv_ori (Reg Imm12) Reg)
+(rule (rv_ori rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Ori) rs1 imm))
+
+;; Helper for emitting the `xor` instruction.
+;; rd ← rs1 ⊕ rs2
+(decl rv_xor (Reg Reg) Reg)
+(rule (rv_xor rs1 rs2)
+  (alu_rrr (AluOPRRR.Xor) rs1 rs2))
+
+;; Helper for emitting the `xori` ("Exlusive Or Immediate") instruction.
+;; rd ← rs1 ⊕ uext(imm)
+(decl rv_xori (Reg Imm12) Reg)
+(rule (rv_xori rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Xori) rs1 imm))
+
+;; Helper for emitting the `not` instruction.
+;; This instruction is a mnemonic for `xori rd, rs1, -1`.
+(decl rv_not (Reg) Reg)
+(rule (rv_not rs1)
+  (rv_xori rs1 (imm12_const -1)))
+
+;; Helper for emitting the `and` instruction.
+;; rd ← rs1 ∧ rs2
+(decl rv_and (Reg Reg) Reg)
+(rule (rv_and rs1 rs2)
+  (alu_rrr (AluOPRRR.And) rs1 rs2))
+
+;; Helper for emitting the `andi` ("And Immediate") instruction.
+;; rd ← rs1 ∧ uext(imm)
+(decl rv_andi (Reg Imm12) Reg)
+(rule (rv_andi rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Andi) rs1 imm))
+
+;; Helper for emitting the `sltu` ("Set Less Than Unsigned") instruction.
+;; rd ← rs1 < rs2
+(decl rv_sltu (Reg Reg) Reg)
+(rule (rv_sltu rs1 rs2)
+  (alu_rrr (AluOPRRR.SltU) rs1 rs2))
+
+;; Helper for emiting the `sltiu` ("Set Less Than Immediate Unsigned") instruction.
+;; rd ← rs1 < imm
+(decl rv_sltiu (Reg Imm12) Reg)
+(rule (rv_sltiu rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.SltiU) rs1 imm))
+
+;; Helper for emitting the `seqz` instruction.
+;; This instruction is a mnemonic for `sltiu rd, rs, 1`.
+(decl rv_seqz (Reg) Reg)
+(rule (rv_seqz rs1)
+  (rv_sltiu rs1 (imm12_const 1)))
+
+
+;; RV64I Base Integer Instruction Set
+;; Unlike RV32I instructions these are only present in the 64bit ISA
+
+;; Helper for emitting the `addw` ("Add Word") instruction.
+;; rd ← sext32(rs1) + sext32(rs2)
+(decl rv_addw (Reg Reg) Reg)
+(rule (rv_addw rs1 rs2)
+  (alu_rrr (AluOPRRR.Addw) rs1 rs2))
+
+;; Helper for emitting the `addiw` ("Add Word Immediate") instruction.
+;; rd ← sext32(rs1) + imm
+(decl rv_addiw (Reg Imm12) Reg)
+(rule (rv_addiw rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Addiw) rs1 imm))
+
+;; Helper for emitting the `sext.w` ("Sign Extend Word") instruction.
+;; This instruction is a mnemonic for `addiw rd, rs, zero`.
+(decl rv_sextw (Reg) Reg)
+(rule (rv_sextw rs1)
+  (rv_addiw rs1 (imm12_const 0)))
+
+;; Helper for emitting the `subw` ("Subtract Word") instruction.
+;; rd ← sext32(rs1) - sext32(rs2)
+(decl rv_subw (Reg Reg) Reg)
+(rule (rv_subw rs1 rs2)
+  (alu_rrr (AluOPRRR.Subw) rs1 rs2))
+
+;; Helper for emitting the `sllw` ("Shift Left Logical Word") instruction.
+;; rd ← sext32(uext32(rs1) << rs2)
+(decl rv_sllw (Reg Reg) Reg)
+(rule (rv_sllw rs1 rs2)
+  (alu_rrr (AluOPRRR.Sllw) rs1 rs2))
+
+;; Helper for emitting the `slliw` ("Shift Left Logical Immediate Word") instruction.
+;; rd ← sext32(uext32(rs1) << imm)
+(decl rv_slliw (Reg Imm12) Reg)
+(rule (rv_slliw rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Slliw) rs1 imm))
+
+;; Helper for emitting the `srlw` ("Shift Right Logical Word") instruction.
+;; rd ← sext32(uext32(rs1) >> rs2)
+(decl rv_srlw (Reg Reg) Reg)
+(rule (rv_srlw rs1 rs2)
+  (alu_rrr (AluOPRRR.Srlw) rs1 rs2))
+
+;; Helper for emitting the `srliw` ("Shift Right Logical Immediate Word") instruction.
+;; rd ← sext32(uext32(rs1) >> imm)
+(decl rv_srliw (Reg Imm12) Reg)
+(rule (rv_srliw rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.SrliW) rs1 imm))
+
+;; Helper for emitting the `sraw` ("Shift Right Arithmetic Word") instruction.
+;; rd ← sext32(rs1 >> rs2)
+(decl rv_sraw (Reg Reg) Reg)
+(rule (rv_sraw rs1 rs2)
+  (alu_rrr (AluOPRRR.Sraw) rs1 rs2))
+
+;; Helper for emitting the `sraiw` ("Shift Right Arithmetic Immediate Word") instruction.
+;; rd ← sext32(rs1 >> imm)
+(decl rv_sraiw (Reg Imm12) Reg)
+(rule (rv_sraiw rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Sraiw) rs1 imm))
+
+
+;; RV32M Extension
+;; TODO: Enable these instructions only when we have the M extension
+
+;; Helper for emitting the `mul` instruction.
+;; rd ← rs1 × rs2
+(decl rv_mul (Reg Reg) Reg)
+(rule (rv_mul rs1 rs2)
+  (alu_rrr (AluOPRRR.Mul) rs1 rs2))
+
+;; Helper for emitting the `mulh` ("Multiply High Signed Signed") instruction.
+;; rd ← (sext(rs1) × sext(rs2)) » xlen
+(decl rv_mulh (Reg Reg) Reg)
+(rule (rv_mulh rs1 rs2)
+  (alu_rrr (AluOPRRR.Mulh) rs1 rs2))
+
+;; Helper for emitting the `mulhu` ("Multiply High Unsigned Unsigned") instruction.
+;; rd ← (uext(rs1) × uext(rs2)) » xlen
+(decl rv_mulhu (Reg Reg) Reg)
+(rule (rv_mulhu rs1 rs2)
+  (alu_rrr (AluOPRRR.Mulhu) rs1 rs2))
+
+;; Helper for emitting the `div` instruction.
+;; rd ← rs1 ÷ rs2
+(decl rv_div (Reg Reg) Reg)
+(rule (rv_div rs1 rs2)
+  (alu_rrr (AluOPRRR.Div) rs1 rs2))
+
+;; Helper for emitting the `divu` ("Divide Unsigned") instruction.
+;; rd ← rs1 ÷ rs2
+(decl rv_divu (Reg Reg) Reg)
+(rule (rv_divu rs1 rs2)
+  (alu_rrr (AluOPRRR.DivU) rs1 rs2))
+
+;; Helper for emitting the `rem` instruction.
+;; rd ← rs1 mod rs2
+(decl rv_rem (Reg Reg) Reg)
+(rule (rv_rem rs1 rs2)
+  (alu_rrr (AluOPRRR.Rem) rs1 rs2))
+
+;; Helper for emitting the `remu` ("Remainder Unsigned") instruction.
+;; rd ← rs1 mod rs2
+(decl rv_remu (Reg Reg) Reg)
+(rule (rv_remu rs1 rs2)
+  (alu_rrr (AluOPRRR.RemU) rs1 rs2))
+
+
+
+;; RV64M Extension
+;; TODO: Enable these instructions only when we have the M extension
+
+;; Helper for emitting the `mulw` ("Multiply Word") instruction.
+;; rd ← uext32(rs1) × uext32(rs2)
+(decl rv_mulw (Reg Reg) Reg)
+(rule (rv_mulw rs1 rs2)
+  (alu_rrr (AluOPRRR.Mulw) rs1 rs2))
+
+;; Helper for emitting the `divw` ("Divide Word") instruction.
+;; rd ← sext32(rs1) ÷ sext32(rs2)
+(decl rv_divw (Reg Reg) Reg)
+(rule (rv_divw rs1 rs2)
+  (alu_rrr (AluOPRRR.Divw) rs1 rs2))
+
+;; Helper for emitting the `divuw` ("Divide Unsigned Word") instruction.
+;; rd ← uext32(rs1) ÷ uext32(rs2)
+(decl rv_divuw (Reg Reg) Reg)
+(rule (rv_divuw rs1 rs2)
+  (alu_rrr (AluOPRRR.Divuw) rs1 rs2))
+
+;; Helper for emitting the `remw` ("Remainder Word") instruction.
+;; rd ← sext32(rs1) mod sext32(rs2)
+(decl rv_remw (Reg Reg) Reg)
+(rule (rv_remw rs1 rs2)
+  (alu_rrr (AluOPRRR.Remw) rs1 rs2))
+
+;; Helper for emitting the `remuw` ("Remainder Unsigned Word") instruction.
+;; rd ← uext32(rs1) mod uext32(rs2)
+(decl rv_remuw (Reg Reg) Reg)
+(rule (rv_remuw rs1 rs2)
+  (alu_rrr (AluOPRRR.Remuw) rs1 rs2))
+
+
+;; F and D Extensions
+;; TODO: Enable these instructions only when we have the F or D extensions
+
+;; Helper for emitting the `fadd` instruction.
+(decl rv_fadd (Type Reg Reg) Reg)
+(rule (rv_fadd $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FaddS) $F32 rs1 rs2))
+(rule (rv_fadd $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FaddD) $F64 rs1 rs2))
+
+;; Helper for emitting the `fsub` instruction.
+(decl rv_fsub (Type Reg Reg) Reg)
+(rule (rv_fsub $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FsubS) $F32 rs1 rs2))
+(rule (rv_fsub $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FsubD) $F64 rs1 rs2))
+
+;; Helper for emitting the `fmul` instruction.
+(decl rv_fmul (Type Reg Reg) Reg)
+(rule (rv_fmul $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FmulS) $F32 rs1 rs2))
+(rule (rv_fmul $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FmulD) $F64 rs1 rs2))
+
+;; Helper for emitting the `fdiv` instruction.
+(decl rv_fdiv (Type Reg Reg) Reg)
+(rule (rv_fdiv $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FdivS) $F32 rs1 rs2))
+(rule (rv_fdiv $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FdivD) $F64 rs1 rs2))
+
+;; Helper for emitting the `fsqrt` instruction.
+(decl rv_fsqrt (Type Reg) Reg)
+(rule (rv_fsqrt $F32 rs1) (fpu_rr (FpuOPRR.FsqrtS) $F32 rs1))
+(rule (rv_fsqrt $F64 rs1) (fpu_rr (FpuOPRR.FsqrtD) $F64 rs1))
+
+;; Helper for emitting the `fmadd` instruction.
+(decl rv_fmadd (Type Reg Reg Reg) Reg)
+(rule (rv_fmadd $F32 rs1 rs2 rs3) (fpu_rrrr (FpuOPRRRR.FmaddS) $F32 rs1 rs2 rs3))
+(rule (rv_fmadd $F64 rs1 rs2 rs3) (fpu_rrrr (FpuOPRRRR.FmaddD) $F64 rs1 rs2 rs3))
+
+;; Helper for emitting the `fcvt.d.s` ("Float Convert Double to Single") instruction.
+(decl rv_fcvtds (Reg) Reg)
+(rule (rv_fcvtds rs1) (fpu_rr (FpuOPRR.FcvtDS) $F32 rs1))
+
+;; Helper for emitting the `fcvt.s.d` ("Float Convert Single to Double") instruction.
+(decl rv_fcvtsd (Reg) Reg)
+(rule (rv_fcvtsd rs1) (fpu_rr (FpuOPRR.FcvtSD) $F64 rs1))
+
+;; Helper for emitting the `fsgnj` ("Floating Point Sign Injection") instruction.
+;; The output of this instruction is `rs1` with the sign bit from `rs2`
+;; This implements the `copysign` operation
+(decl rv_fsgnj (Type Reg Reg) Reg)
+(rule (rv_fsgnj $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FsgnjS) $F32 rs1 rs2))
+(rule (rv_fsgnj $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FsgnjD) $F64 rs1 rs2))
+
+;; Helper for emitting the `fsgnjn` ("Floating Point Sign Injection Negated") instruction.
+;; The output of this instruction is `rs1` with the negated sign bit from `rs2`
+;; When `rs1 == rs2` this implements the `neg` operation
+(decl rv_fsgnjn (Type Reg Reg) Reg)
+(rule (rv_fsgnjn $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FsgnjnS) $F32 rs1 rs2))
+(rule (rv_fsgnjn $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FsgnjnD) $F64 rs1 rs2))
+
+;; Helper for emitting the `fneg` ("Floating Point Negate") instruction.
+;; This instruction is a mnemonic for `fsgnjn rd, rs1, rs1`
+(decl rv_fneg (Type Reg) Reg)
+(rule (rv_fneg ty rs1) (rv_fsgnjn ty rs1 rs1))
+
+;; Helper for emitting the `fsgnjx` ("Floating Point Sign Injection Exclusive") instruction.
+;; The output of this instruction is `rs1` with the XOR of the sign bits from `rs1` and `rs2`.
+;; When `rs1 == rs2` this implements `fabs`
+(decl rv_fsgnjx (Type Reg Reg) Reg)
+(rule (rv_fsgnjx $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FsgnjxS) $F32 rs1 rs2))
+(rule (rv_fsgnjx $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FsgnjxD) $F64 rs1 rs2))
+
+;; Helper for emitting the `fabs` ("Floating Point Absolute") instruction.
+;; This instruction is a mnemonic for `fsgnjx rd, rs1, rs1`
+(decl rv_fabs (Type Reg) Reg)
+(rule (rv_fabs ty rs1) (rv_fsgnjx ty rs1 rs1))
+
+;; Helper for emitting the `feq` ("Float Equal") instruction.
+(decl rv_feq (Type Reg Reg) Reg)
+(rule (rv_feq $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FeqS) $I64 rs1 rs2))
+(rule (rv_feq $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FeqD) $I64 rs1 rs2))
+
+;; Helper for emitting the `flt` ("Float Less Than") instruction.
+(decl rv_flt (Type Reg Reg) Reg)
+(rule (rv_flt $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FltS) $I64 rs1 rs2))
+(rule (rv_flt $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FltD) $I64 rs1 rs2))
+
+;; Helper for emitting the `fle` ("Float Less Than or Equal") instruction.
+(decl rv_fle (Type Reg Reg) Reg)
+(rule (rv_fle $F32 rs1 rs2) (fpu_rrr (FpuOPRRR.FleS) $I64 rs1 rs2))
+(rule (rv_fle $F64 rs1 rs2) (fpu_rrr (FpuOPRRR.FleD) $I64 rs1 rs2))
+
+;; Helper for emitting the `fgt` ("Float Greater Than") instruction.
+;; Note: The arguments are reversed
+(decl rv_fgt (Type Reg Reg) Reg)
+(rule (rv_fgt ty rs1 rs2) (rv_flt ty rs2 rs1))
+
+;; Helper for emitting the `fge` ("Float Greater Than or Equal") instruction.
+;; Note: The arguments are reversed
+(decl rv_fge (Type Reg Reg) Reg)
+(rule (rv_fge ty rs1 rs2) (rv_fle ty rs2 rs1))
+
+
+;; `Zba` Extension Instructions
+
+;; Helper for emitting the `adduw` ("Add Unsigned Word") instruction.
+;; rd ← uext32(rs1) + uext32(rs2)
+(decl rv_adduw (Reg Reg) Reg)
+(rule (rv_adduw rs1 rs2)
+  (alu_rrr (AluOPRRR.Adduw) rs1 rs2))
+
+;; Helper for emitting the `zext.w` ("Zero Extend Word") instruction.
+;; This instruction is a mnemonic for `adduw rd, rs1, zero`.
+;; rd ← uext32(rs1)
+(decl rv_zextw (Reg) Reg)
+(rule (rv_zextw rs1)
+  (rv_adduw rs1 (zero_reg)))
+
+;; Helper for emitting the `slli.uw` ("Shift Left Logical Immediate Unsigned Word") instruction.
+;; rd ← uext32(rs1) << imm
+(decl rv_slliuw (Reg Imm12) Reg)
+(rule (rv_slliuw rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.SlliUw) rs1 imm))
+
+
+;; `Zbb` Extension Instructions
+
+;; Helper for emitting the `andn` ("And Negated") instruction.
+;; rd ← rs1 ∧ ~(rs2)
+(decl rv_andn (Reg Reg) Reg)
+(rule (rv_andn rs1 rs2)
+  (alu_rrr (AluOPRRR.Andn) rs1 rs2))
+
+;; Helper for emitting the `orn` ("Or Negated") instruction.
+;; rd ← rs1 ∨ ~(rs2)
+(decl rv_orn (Reg Reg) Reg)
+(rule (rv_orn rs1 rs2)
+  (alu_rrr (AluOPRRR.Orn) rs1 rs2))
+
+;; Helper for emitting the `clz` ("Count Leading Zero Bits") instruction.
+(decl rv_clz (Reg) Reg)
+(rule (rv_clz rs1)
+  (alu_rr_funct12 (AluOPRRI.Clz) rs1))
+
+;; Helper for emitting the `clzw` ("Count Leading Zero Bits in Word") instruction.
+(decl rv_clzw (Reg) Reg)
+(rule (rv_clzw rs1)
+  (alu_rr_funct12 (AluOPRRI.Clzw) rs1))
+
+;; Helper for emitting the `ctz` ("Count Trailing Zero Bits") instruction.
+(decl rv_ctz (Reg) Reg)
+(rule (rv_ctz rs1)
+  (alu_rr_funct12 (AluOPRRI.Ctz) rs1))
+
+;; Helper for emitting the `ctzw` ("Count Trailing Zero Bits in Word") instruction.
+(decl rv_ctzw (Reg) Reg)
+(rule (rv_ctzw rs1)
+  (alu_rr_funct12 (AluOPRRI.Ctzw) rs1))
+
+;; Helper for emitting the `cpop` ("Count Population") instruction.
+(decl rv_cpop (Reg) Reg)
+(rule (rv_cpop rs1)
+  (alu_rr_funct12 (AluOPRRI.Cpop) rs1))
+
+;; Helper for emitting the `max` instruction.
+(decl rv_max (Reg Reg) Reg)
+(rule (rv_max rs1 rs2)
+  (alu_rrr (AluOPRRR.Max) rs1 rs2))
+
+;; Helper for emitting the `sext.b` instruction.
+(decl rv_sextb (Reg) Reg)
+(rule (rv_sextb rs1)
+  (alu_rr_imm12 (AluOPRRI.Sextb) rs1 (imm12_const 0)))
+
+;; Helper for emitting the `sext.h` instruction.
+(decl rv_sexth (Reg) Reg)
+(rule (rv_sexth rs1)
+  (alu_rr_imm12 (AluOPRRI.Sexth) rs1 (imm12_const 0)))
+
+;; Helper for emitting the `zext.h` instruction.
+(decl rv_zexth (Reg) Reg)
+(rule (rv_zexth rs1)
+  (alu_rr_imm12 (AluOPRRI.Zexth) rs1 (imm12_const 0)))
+
+;; Helper for emitting the `rol` ("Rotate Left") instruction.
+(decl rv_rol (Reg Reg) Reg)
+(rule (rv_rol rs1 rs2)
+  (alu_rrr (AluOPRRR.Rol) rs1 rs2))
+
+;; Helper for emitting the `rolw` ("Rotate Left Word") instruction.
+(decl rv_rolw (Reg Reg) Reg)
+(rule (rv_rolw rs1 rs2)
+  (alu_rrr (AluOPRRR.Rolw) rs1 rs2))
+
+;; Helper for emitting the `ror` ("Rotate Right") instruction.
+(decl rv_ror (Reg Reg) Reg)
+(rule (rv_ror rs1 rs2)
+  (alu_rrr (AluOPRRR.Ror) rs1 rs2))
+
+;; Helper for emitting the `rorw` ("Rotate Right Word") instruction.
+(decl rv_rorw (Reg Reg) Reg)
+(rule (rv_rorw rs1 rs2)
+  (alu_rrr (AluOPRRR.Rorw) rs1 rs2))
+
+;; Helper for emitting the `rev8` ("Byte Reverse") instruction.
+(decl rv_rev8 (Reg) Reg)
+(rule (rv_rev8 rs1)
+  (alu_rr_funct12 (AluOPRRI.Rev8) rs1))
+
+;; Helper for emitting the `brev8` ("Bit Reverse Inside Bytes") instruction.
+;; TODO: This instruction is mentioned in some older versions of the
+;; spec, but has since disappeared, we should follow up on this.
+;; It probably was renamed to `rev.b` which seems to be the closest match.
+(decl rv_brev8 (Reg) Reg)
+(rule (rv_brev8 rs1)
+  (alu_rr_funct12 (AluOPRRI.Brev8) rs1))
+
+;; Helper for emitting the `bseti` ("Single-Bit Set Immediate") instruction.
+(decl rv_bseti (Reg Imm12) Reg)
+(rule (rv_bseti rs1 imm)
+  (alu_rr_imm12 (AluOPRRI.Bseti) rs1 imm))
+
+
+;; `Zbkb` Extension Instructions
+
+;; Helper for emitting the `pack` ("Pack low halves of registers") instruction.
+(decl rv_pack (Reg Reg) Reg)
+(rule (rv_pack rs1 rs2)
+  (alu_rrr (AluOPRRR.Pack) rs1 rs2))
+
+;; Helper for emitting the `packw` ("Pack low 16-bits of registers") instruction.
+(decl rv_packw (Reg Reg) Reg)
+(rule (rv_packw rs1 rs2)
+  (alu_rrr (AluOPRRR.Packw) rs1 rs2))
+
+
+
+
 ;; for load immediate
 (decl imm (Type u64) Reg)
 (extern constructor imm imm)
@@ -778,7 +1282,7 @@
 (decl load_imm12 (i32) Reg)
 (rule
   (load_imm12 x)
-  (alu_rr_imm12 (AluOPRRI.Addi) (zero_reg) (imm12_const x)))
+  (rv_addi (zero_reg) (imm12_const x)))
   
 ;; for load immediate
 (decl imm_from_bits (u64) Imm12)
@@ -809,26 +1313,6 @@
 (extern extractor imm12_from_u64 imm12_from_u64)
 
 
-;;;; Instruction Helpers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-;; bseti: Set a single bit in a register, indexed by a constant.
-(decl bseti (Reg u64) Reg)
-(rule (bseti val bit)
-  (if-let $false (has_zbs))
-  (if-let $false (u64_le bit 12))
-  (let ((const Reg (load_u64_constant (u64_shl 1 bit))))
-    (alu_rrr (AluOPRRR.Or) val const)))
-
-(rule (bseti val bit)
-  (if-let $false (has_zbs))
-  (if-let $true (u64_le bit 12))
-  (alu_rr_imm12 (AluOPRRI.Ori) val (imm12_const (u64_as_i32 (u64_shl 1 bit)))))
-
-(rule (bseti val bit)
-  (if-let $true (has_zbs))
-  (alu_rr_imm12 (AluOPRRI.Bseti) val (imm12_const (u64_as_i32 bit))))
-
 
 ;; Float Helpers
 
@@ -849,23 +1333,6 @@
             (_ Unit (emit (MInst.AluRRR op dst src1 src2))))
         dst))
 
-;; Helper for emit rd = rs1 + rs2 for Interger.
-(decl alu_add (Reg Reg) Reg)
-(rule
-  (alu_add rs1 rs2)
-  (alu_rrr (AluOPRRR.Add) rs1 rs2))
-
-(decl alu_and (Reg Reg) Reg)
-(rule
-  (alu_and rs1 rs2)
-  (alu_rrr (AluOPRRR.And) rs1 rs2))
-
-
-;; Helper for emit rd = rs1 - rs2 for Interger.
-(decl alu_sub (Reg Reg) Reg)
-(rule
-  (alu_sub rs1 rs2)
-  (alu_rrr (AluOPRRR.Sub) rs1 rs2))
 
 (decl pack_float_rounding_mode (FRM) OptionFloatRoundingMode)
 (extern constructor pack_float_rounding_mode pack_float_rounding_mode)
@@ -893,18 +1360,6 @@
             (_ Unit (emit (MInst.AluRRImm12 op dst src imm))))
         dst))
 
-(decl alu_andi (Reg i32) Reg)
-(rule (alu_andi r i)
-  (alu_rr_imm12 (AluOPRRI.Andi) r (imm12_const i)))
-
-
-(decl alu_slli (Reg i32) Reg)
-(rule (alu_slli r i)
-  (alu_rr_imm12 (AluOPRRI.Slli) r (imm12_const i)))
-(decl alu_srli (Reg i32) Reg)
-(rule (alu_srli r i)
-  (alu_rr_imm12 (AluOPRRI.Srli) r (imm12_const i)))
-
 ;; some instruction use imm12 as funct12.
 ;; so we don't need the imm12 paramter.
 (decl alu_rr_funct12 (AluOPRRI Reg) Reg)
@@ -913,31 +1368,19 @@
             (_ Unit (emit (MInst.AluRRImm12 op dst src (imm12_zero)))))
         dst))
 
-
 (decl select_addi (Type) AluOPRRI)
 (rule 1 (select_addi (fits_in_32 ty)) (AluOPRRI.Addiw))
 (rule (select_addi (fits_in_64 ty)) (AluOPRRI.Addi))
 
 
-;; Helper for emiting the `sltiu` instruction
-(decl sltiu (Reg Imm12) Reg)
-(rule (sltiu r imm)
-  (alu_rr_imm12 (AluOPRRI.SltiU) r imm))
-
-;; Helper for emiting the `seqz` mnemonic
-(decl seqz (Reg) Reg)
-(rule (seqz r)
-  (sltiu r (imm12_const 1)))
-
-
 (decl bnot_128 (ValueRegs) ValueRegs)
 (rule
   (bnot_128 val)
   (let
     (;; low part.
-      (low Reg (gen_bit_not (value_regs_get val 0)))
+      (low Reg (rv_not (value_regs_get val 0)))
       ;; high part.
-      (high Reg (gen_bit_not (value_regs_get val 1))))
+      (high Reg (rv_not (value_regs_get val 1))))
     (value_regs low high)))
 
 (decl lower_bit_reverse (Reg Type) Reg)
@@ -951,7 +1394,7 @@
   (let
     ((tmp Reg (gen_brev8 r $I16))
       (tmp2 Reg (gen_rev8 tmp))
-      (result Reg (alu_rr_imm12 (AluOPRRI.Srli) tmp2 (imm12_const 48))))
+      (result Reg (rv_srli tmp2 (imm12_const 48))))
     result))
 
 (rule
@@ -959,7 +1402,7 @@
   (let
     ((tmp Reg (gen_brev8 r $I32))
       (tmp2 Reg (gen_rev8 tmp))
-      (result Reg (alu_rr_imm12 (AluOPRRI.Srli) tmp2 (imm12_const 32))))
+      (result Reg (rv_srli tmp2 (imm12_const 32))))
     result))
 
 (rule
@@ -975,16 +1418,16 @@
 
 (rule 1 (lower_ctz (fits_in_16 ty) x)
   (if-let $true (has_zbb))
-  (let ((tmp Reg (bseti x (ty_bits ty))))
-    (alu_rr_funct12 (AluOPRRI.Ctzw) tmp)))
+  (let ((tmp Reg (gen_bseti x (ty_bits ty))))
+    (rv_ctzw tmp)))
 
 (rule 2 (lower_ctz $I32 x)
   (if-let $true (has_zbb))
-  (alu_rr_funct12 (AluOPRRI.Ctzw) x))
+  (rv_ctzw x))
 
 (rule 2 (lower_ctz $I64 x)
   (if-let $true (has_zbb))
-  (alu_rr_funct12 (AluOPRRI.Ctz) x))
+  (rv_ctz x))
 
 ;; Count trailing zeros from a i128 bit value.
 ;; We count both halves separately and conditionally add them if it makes sense.
@@ -997,11 +1440,9 @@
         (low Reg (lower_ctz $I64 x_lo))
         ;; Only add the top half if the bottom is zero
         (high Reg (gen_select_reg (IntCC.Equal) x_lo (zero_reg) high (zero_reg)))
-        (result Reg (alu_add low high)))
+        (result Reg (rv_add low high)))
     (zext result $I64 $I128)))
 
-
-
 (decl lower_clz (Type Reg) Reg)
 (rule (lower_clz ty rs)
   (gen_cltz $true rs ty))
@@ -1009,18 +1450,19 @@
 (rule 1 (lower_clz (fits_in_16 ty) r)
   (if-let $true (has_zbb))
   (let ((tmp Reg (zext r ty $I64))
-        (count Reg (alu_rr_funct12 (AluOPRRI.Clz) tmp))
+        (count Reg (rv_clz tmp))
         ;; We always do the operation on the full 64-bit register, so subtract 64 from the result.
-        (result Reg (alu_rr_imm12 (AluOPRRI.Addi) count (imm12_const_add (ty_bits ty) -64))))
+        (result Reg (rv_addi count (imm12_const_add (ty_bits ty) -64))))
     result))
 
 (rule 2 (lower_clz $I32 r)
   (if-let $true (has_zbb))
-  (alu_rr_funct12 (AluOPRRI.Clzw) r))
+  (rv_clzw r))
 
 (rule 2 (lower_clz $I64 r)
   (if-let $true (has_zbb))
-  (alu_rr_funct12 (AluOPRRI.Clz) r))
+  (rv_clz r))
+
 
 ;; Count leading zeros from a i128 bit value.
 ;; We count both halves separately and conditionally add them if it makes sense.
@@ -1033,16 +1475,16 @@
         (low Reg (lower_clz $I64 x_lo))
         ;; Only add the bottom zeros if the top half is zero
         (low Reg (gen_select_reg (IntCC.Equal) x_hi (zero_reg) low (zero_reg)))
-        (result Reg (alu_add high low)))
+        (result Reg (rv_add high low)))
     (zext result $I64 $I128)))
 
 
 (decl lower_cls (Type Reg) Reg)
 (rule (lower_cls ty r)
   (let ((tmp Reg (ext_int_if_need $true r ty))
-        (tmp2 Reg (gen_select_reg (IntCC.SignedLessThan) tmp (zero_reg) (gen_bit_not tmp) tmp))
+        (tmp2 Reg (gen_select_reg (IntCC.SignedLessThan) tmp (zero_reg) (rv_not tmp) tmp))
         (tmp3 Reg (lower_clz ty tmp2)))
-    (alu_rr_imm12 (AluOPRRI.Addi) tmp3 (imm12_const -1))))
+    (rv_addi tmp3 (imm12_const -1))))
 
 ;; If the sign bit is set, we count the leading zeros of the inverted value.
 ;; Otherwise we can just count the leading zeros of the original value.
@@ -1051,11 +1493,11 @@
 (rule (lower_cls_i128 x)
   (let ((low Reg (value_regs_get x 0))
         (high Reg (value_regs_get x 1))
-        (low Reg (gen_select_reg (IntCC.SignedLessThan) high (zero_reg) (gen_bit_not low) low))
-        (high Reg (gen_select_reg (IntCC.SignedLessThan) high (zero_reg) (gen_bit_not high) high))
+        (low Reg (gen_select_reg (IntCC.SignedLessThan) high (zero_reg) (rv_not low) low))
+        (high Reg (gen_select_reg (IntCC.SignedLessThan) high (zero_reg) (rv_not high) high))
         (tmp ValueRegs (lower_clz_i128 (value_regs low high)))
         (count Reg (value_regs_get tmp 0))
-        (result Reg (alu_rr_imm12 (AluOPRRI.Addi) count (imm12_const -1))))
+        (result Reg (rv_addi count (imm12_const -1))))
     (zext result $I64 $I128)))
 
 
@@ -1106,7 +1548,7 @@
 (rule 0 (extend val extend_op (fits_in_32 from_ty) (fits_in_64 to_ty))
   (let ((val Reg (value_regs_get val 0))
         (shift Imm12 (imm_from_bits (u64_sub 64 (ty_bits from_ty))))
-        (left Reg (alu_rr_imm12 (AluOPRRI.Slli) val shift))
+        (left Reg (rv_slli val shift))
         (shift_op AluOPRRI (extend_shift_op extend_op))
         (right Reg (alu_rr_imm12 shift_op left shift)))
     right))
@@ -1114,13 +1556,13 @@
 ;; If we are zero extending a U8 we can use a `andi` instruction.
 (rule 1 (extend val (ExtendOp.Zero) $I8 (fits_in_64 to_ty))
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rr_imm12 (AluOPRRI.Andi) val (imm12_const 255))))
+    (rv_andi val (imm12_const 255))))
 
 ;; When signed extending from 32 to 64 bits we can use a
 ;; `addiw val 0`. Also known as a `sext.w`
 (rule 1 (extend val (ExtendOp.Signed) $I32 $I64)
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rr_imm12 (AluOPRRI.Addiw) val (imm12_const 0))))
+    (rv_sextw val)))
 
 
 ;; No point in trying to use `packh` here to zero extend 8 bit values
@@ -1130,45 +1572,45 @@
 (rule 1 (extend val (ExtendOp.Zero) $I16 (fits_in_64 _))
   (if-let $true (has_zbkb))
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rrr (AluOPRRR.Packw) val (zero_reg))))
+    (rv_packw val (zero_reg))))
 
 ;; If we have the `zbkb` extension `pack` can be used to zero extend 32 bit registers
 (rule 1 (extend val (ExtendOp.Zero) $I32 $I64)
   (if-let $true (has_zbkb))
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rrr (AluOPRRR.Pack) val (zero_reg))))
+    (rv_pack val (zero_reg))))
 
 
 ;; If we have the `zbb` extension we can use the dedicated `sext.b` instruction.
 (rule 1 (extend val (ExtendOp.Signed) $I8 (fits_in_64 _))
   (if-let $true (has_zbb))
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rr_imm12 (AluOPRRI.Sextb) val (imm12_const 0))))
+    (rv_sextb val)))
 
 ;; If we have the `zbb` extension we can use the dedicated `sext.h` instruction.
 (rule 1 (extend val (ExtendOp.Signed) $I16 (fits_in_64 _))
   (if-let $true (has_zbb))
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rr_imm12 (AluOPRRI.Sexth) val (imm12_const 0))))
+    (rv_sexth val)))
 
 ;; If we have the `zbb` extension we can use the dedicated `zext.h` instruction.
 (rule 2 (extend val (ExtendOp.Zero) $I16 (fits_in_64 _))
   (if-let $true (has_zbb))
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rr_imm12 (AluOPRRI.Zexth) val (imm12_const 0))))
+    (rv_zexth val)))
 
 ;; With `zba` we have a `zext.w` instruction
 (rule 2 (extend val (ExtendOp.Zero) $I32 $I64)
   (if-let $true (has_zba))
   (let ((val Reg (value_regs_get val 0)))
-    (alu_rrr (AluOPRRR.Adduw) val (zero_reg))))
+    (rv_zextw val)))
 
 ;;; Signed rules extending to I128
 ;; Extend the bottom part, and extract the sign bit from the bottom as the top
 (rule 3 (extend val (ExtendOp.Signed) (fits_in_64 from_ty) $I128)
   (let ((val Reg (value_regs_get val 0))
         (low Reg (extend val (ExtendOp.Signed) from_ty $I64))
-        (high Reg (alu_rr_imm12 (AluOPRRI.Srai) low (imm12_const 63))))
+        (high Reg (rv_srai low (imm12_const 63))))
     (value_regs low high)))
 
 ;;; Unsigned rules extending to I128
@@ -1197,24 +1639,24 @@
 (decl lower_umlhi (Type Reg Reg) Reg)
 (rule 1
   (lower_umlhi $I64 rs1 rs2)
-  (alu_rrr (AluOPRRR.Mulhu) rs1 rs2))
+  (rv_mulhu rs1 rs2))
 
 (rule
   (lower_umlhi ty rs1 rs2)
   (let
-    ((tmp Reg (alu_rrr (AluOPRRR.Mul) (ext_int_if_need $false rs1 ty) (ext_int_if_need $false rs2 ty))))
-    (alu_rr_imm12 (AluOPRRI.Srli) tmp (imm12_const (ty_bits ty)))))
+    ((tmp Reg (rv_mul (ext_int_if_need $false rs1 ty) (ext_int_if_need $false rs2 ty))))
+    (rv_srli tmp (imm12_const (ty_bits ty)))))
 
 (decl lower_smlhi (Type Reg Reg) Reg)
 (rule 1
   (lower_smlhi $I64 rs1 rs2)
-  (alu_rrr (AluOPRRR.Mulh) rs1 rs2))
+  (rv_mulh rs1 rs2))
 
 (rule
   (lower_smlhi ty rs1 rs2)
   (let
-    ((tmp Reg (alu_rrr (AluOPRRR.Mul) rs1 rs2)))
-    (alu_rr_imm12 (AluOPRRI.Srli) tmp (imm12_const (ty_bits ty)))))
+    ((tmp Reg (rv_mul rs1 rs2)))
+    (rv_srli tmp (imm12_const (ty_bits ty)))))
 
 
 (decl lower_rotl (Type Reg Reg) Reg)
@@ -1222,7 +1664,7 @@
 (rule 1
   (lower_rotl $I64 rs amount)
   (if-let $true (has_zbb))
-  (alu_rrr (AluOPRRR.Rol) rs amount))
+  (rv_rol rs amount))
 
 (rule
   (lower_rotl $I64 rs amount)
@@ -1232,7 +1674,7 @@
 (rule 1
   (lower_rotl $I32 rs amount)
   (if-let $true (has_zbb))
-  (alu_rrr (AluOPRRR.Rolw) rs amount))
+  (rv_rolw rs amount))
 
 (rule
   (lower_rotl $I32 rs amount)
@@ -1254,11 +1696,11 @@
       (shamt Reg (value_regs_get x 0))
       (len_sub_shamt Reg (value_regs_get x 1))
       ;;
-      (part1 Reg (alu_rrr (AluOPRRR.Sll) rs shamt))
+      (part1 Reg (rv_sll rs shamt))
       ;;
-      (part2 Reg (alu_rrr (AluOPRRR.Srl) rs len_sub_shamt))
+      (part2 Reg (rv_srl rs len_sub_shamt))
       (part3 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) part2)))
-    (alu_rrr (AluOPRRR.Or) part1 part3)))
+    (rv_or part1 part3)))
 
 
 ;;;; construct shift amount.rotl on i128 will use shift to implement. So can call this function.
@@ -1272,7 +1714,7 @@
 (rule 1
   (lower_rotr $I64 rs amount)
   (if-let $true (has_zbb))
-  (alu_rrr (AluOPRRR.Ror) rs amount))
+  (rv_ror rs amount))
 (rule
   (lower_rotr $I64 rs amount)
   (if-let $false (has_zbb))
@@ -1281,7 +1723,7 @@
 (rule 1
   (lower_rotr $I32 rs amount)
   (if-let $true (has_zbb))
-  (alu_rrr (AluOPRRR.Rorw) rs amount))
+  (rv_rorw rs amount))
 
 (rule
   (lower_rotr $I32 rs amount)
@@ -1302,12 +1744,31 @@
       (shamt Reg (value_regs_get x 0))
       (len_sub_shamt Reg (value_regs_get x 1))
       ;;
-      (part1 Reg (alu_rrr (AluOPRRR.Srl) rs shamt))
+      (part1 Reg (rv_srl rs shamt))
       ;;
-      (part2 Reg (alu_rrr (AluOPRRR.Sll) rs len_sub_shamt))
+      (part2 Reg (rv_sll rs len_sub_shamt))
       ;;
       (part3 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) part2)))
-    (alu_rrr (AluOPRRR.Or) part1 part3)))
+    (rv_or part1 part3)))
+
+
+
+;; bseti: Set a single bit in a register, indexed by a constant.
+(decl gen_bseti (Reg u64) Reg)
+(rule (gen_bseti val bit)
+  (if-let $false (has_zbs))
+  (if-let $false (u64_le bit 12))
+  (let ((const Reg (load_u64_constant (u64_shl 1 bit))))
+    (rv_or val const)))
+
+(rule (gen_bseti val bit)
+  (if-let $false (has_zbs))
+  (if-let $true (u64_le bit 12))
+  (rv_ori val (imm12_const (u64_as_i32 (u64_shl 1 bit)))))
+
+(rule (gen_bseti val bit)
+  (if-let $true (has_zbs))
+  (rv_bseti val (imm12_const (u64_as_i32 bit))))
 
 
 (decl gen_popcnt (Reg Type) Reg)
@@ -1321,9 +1782,9 @@
     (writable_reg_to_reg sum)))
 
 (decl lower_popcnt (Reg Type) Reg)
-(rule 1 (lower_popcnt rs ty )
+(rule 1 (lower_popcnt rs ty)
   (if-let $true (has_zbb))
-  (alu_rr_funct12 (AluOPRRI.Cpop) (ext_int_if_need $false rs ty)))
+  (rv_cpop (ext_int_if_need $false rs ty)))
 (rule (lower_popcnt rs ty)
   (if-let $false (has_zbb))
   (gen_popcnt rs ty))
@@ -1337,7 +1798,7 @@
       ;; high part.
       (high Reg (lower_popcnt (value_regs_get a 1) $I64))
       ;; add toghter.
-      (result Reg (alu_add low high)))
+      (result Reg (rv_add low high)))
     (value_regs result (load_u64_constant 0))))
 
 (decl lower_i128_rotl (ValueRegs ValueRegs) ValueRegs)
@@ -1348,19 +1809,19 @@
       (shamt Reg (value_regs_get tmp 0))
       (len_sub_shamt Reg (value_regs_get tmp 1))
       ;;
-      (low_part1 Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 0) shamt))
-      (low_part2 Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 1) len_sub_shamt))
+      (low_part1 Reg (rv_sll (value_regs_get x 0) shamt))
+      (low_part2 Reg (rv_srl (value_regs_get x 1) len_sub_shamt))
       ;;; if shamt == 0 low_part2 will overflow we should zero instead.
       (low_part3 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) low_part2))
-      (low Reg (alu_rrr (AluOPRRR.Or) low_part1 low_part3))
+      (low Reg (rv_or low_part1 low_part3))
       ;;
-      (high_part1 Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 1) shamt))
-      (high_part2 Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 0) len_sub_shamt))
+      (high_part1 Reg (rv_sll (value_regs_get x 1) shamt))
+      (high_part2 Reg (rv_srl (value_regs_get x 0) len_sub_shamt))
       (high_part3 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) high_part2))
-      (high Reg (alu_rrr (AluOPRRR.Or) high_part1 high_part3))
+      (high Reg (rv_or high_part1 high_part3))
       ;;
       (const64 Reg (load_u64_constant 64))
-      (shamt_128 Reg (alu_andi (value_regs_get y 0) 127)))
+      (shamt_128 Reg (rv_andi (value_regs_get y 0) (imm12_const 127))))
     ;; right now we only rotate less than 64 bits.
     ;; if shamt is greater than or equal 64 , we should switch low and high.
     (value_regs
@@ -1377,20 +1838,20 @@
       (shamt Reg (value_regs_get tmp 0))
       (len_sub_shamt Reg (value_regs_get tmp 1))
       ;;
-      (low_part1 Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 0) shamt))
-      (low_part2 Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 1) len_sub_shamt))
+      (low_part1 Reg (rv_srl (value_regs_get x 0) shamt))
+      (low_part2 Reg (rv_sll (value_regs_get x 1) len_sub_shamt))
       ;;; if shamt == 0 low_part2 will overflow we should zero instead.
       (low_part3 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) low_part2))
-      (low Reg (alu_rrr (AluOPRRR.Or) low_part1 low_part3))
+      (low Reg (rv_or low_part1 low_part3))
       ;;
-      (high_part1 Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 1) shamt))
-      (high_part2 Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 0) len_sub_shamt))
+      (high_part1 Reg (rv_srl (value_regs_get x 1) shamt))
+      (high_part2 Reg (rv_sll (value_regs_get x 0) len_sub_shamt))
       (high_part3 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) high_part2))
-      (high Reg (alu_rrr (AluOPRRR.Or) high_part1 high_part3))
+      (high Reg (rv_or high_part1 high_part3))
 
       ;;
       (const64 Reg (load_u64_constant 64))
-      (shamt_128 Reg (alu_andi (value_regs_get y 0) 127)))
+      (shamt_128 Reg (rv_andi (value_regs_get y 0) (imm12_const 127))))
     ;; right now we only rotate less than 64 bits.
     ;; if shamt is greater than or equal 64 , we should switch low and high.
     (value_regs
@@ -1407,16 +1868,16 @@
       (shamt Reg (value_regs_get tmp 0))
       (len_sub_shamt Reg (value_regs_get tmp 1))
       ;;
-      (low Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 0) shamt))
+      (low Reg (rv_sll (value_regs_get x 0) shamt))
       ;; high part.
-      (high_part1 Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 0) len_sub_shamt))
+      (high_part1 Reg (rv_srl (value_regs_get x 0) len_sub_shamt))
       (high_part2 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) high_part1))
       ;;
-      (high_part3 Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 1) shamt))
-      (high Reg (alu_rrr (AluOPRRR.Or) high_part2 high_part3 ))
+      (high_part3 Reg (rv_sll (value_regs_get x 1) shamt))
+      (high Reg (rv_or high_part2 high_part3 ))
       ;;
       (const64 Reg (load_u64_constant 64))
-      (shamt_128 Reg (alu_andi (value_regs_get y 0) 127)))
+      (shamt_128 Reg (rv_andi (value_regs_get y 0) (imm12_const 127))))
     (value_regs
       (gen_select_reg (IntCC.UnsignedGreaterThanOrEqual) shamt_128 const64 (zero_reg) low)
       (gen_select_reg (IntCC.UnsignedGreaterThanOrEqual) shamt_128 const64 low high))))
@@ -1430,17 +1891,17 @@
       (len_sub_shamt Reg (value_regs_get tmp 1))
 
       ;; low part.
-      (low_part1 Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 1) len_sub_shamt))
+      (low_part1 Reg (rv_sll (value_regs_get x 1) len_sub_shamt))
       (low_part2 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) low_part1))
       ;;
-      (low_part3 Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 0) shamt))
-      (low Reg (alu_rrr (AluOPRRR.Or) low_part2 low_part3 ))
+      (low_part3 Reg (rv_srl (value_regs_get x 0) shamt))
+      (low Reg (rv_or low_part2 low_part3 ))
       ;;
       (const64 Reg (load_u64_constant 64))
 
       ;;
-      (high Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 1) shamt))
-      (shamt_128 Reg (alu_andi (value_regs_get y 0) 127)))
+      (high Reg (rv_srl (value_regs_get x 1) shamt))
+      (shamt_128 Reg (rv_andi (value_regs_get y 0) (imm12_const 127))))
     (value_regs
       (gen_select_reg (IntCC.UnsignedGreaterThanOrEqual) shamt_128 const64 high low)
       (gen_select_reg (IntCC.UnsignedGreaterThanOrEqual) shamt_128 const64 (zero_reg) high))))
@@ -1455,21 +1916,21 @@
       (len_sub_shamt Reg (value_regs_get tmp 1))
 
       ;; low part.
-      (low_part1 Reg (alu_rrr (AluOPRRR.Sll) (value_regs_get x 1) len_sub_shamt))
+      (low_part1 Reg (rv_sll (value_regs_get x 1) len_sub_shamt))
       (low_part2 Reg (gen_select_reg (IntCC.Equal) shamt (zero_reg) (zero_reg) low_part1))
       ;;
-      (low_part3 Reg (alu_rrr (AluOPRRR.Srl) (value_regs_get x 0) shamt))
-      (low Reg (alu_rrr (AluOPRRR.Or) low_part2 low_part3 ))
+      (low_part3 Reg (rv_srl (value_regs_get x 0) shamt))
+      (low Reg (rv_or low_part2 low_part3 ))
       ;;
       (const64 Reg (load_u64_constant 64))
       ;;
-      (high Reg (alu_rrr (AluOPRRR.Sra) (value_regs_get x 1) shamt))
+      (high Reg (rv_sra (value_regs_get x 1) shamt))
       ;;
       (const_neg_1 Reg (load_imm12 -1))
       ;;
       (high_replacement Reg (gen_select_reg (IntCC.SignedLessThan) (value_regs_get x 1) (zero_reg) const_neg_1 (zero_reg)))
       (const64 Reg (load_u64_constant 64))
-      (shamt_128 Reg (alu_andi (value_regs_get y 0) 127)))
+      (shamt_128 Reg (rv_andi (value_regs_get y 0) (imm12_const 127))))
     (value_regs
       (gen_select_reg (IntCC.UnsignedGreaterThanOrEqual) shamt_128 const64 high low)
       (gen_select_reg (IntCC.UnsignedGreaterThanOrEqual) shamt_128 const64 high_replacement high))))
@@ -1625,45 +2086,6 @@
   (side_effect (SideEffectNoResult.Inst (MInst.AtomicStore src ty p)))
 )
 
-;; helper function to inverse all bits.
-(decl gen_bit_not (Reg) Reg)
-(rule (gen_bit_not r)
-  (alu_rr_imm12 (AluOPRRI.Xori) r (imm12_const -1)))
-
-
-;; float arithmatic op
-(decl f_arithmatic_op (Type Opcode) FpuOPRRR)
-(rule
-  (f_arithmatic_op $F32 (Opcode.Fadd))
-  (FpuOPRRR.FaddS))
-
-(rule
-  (f_arithmatic_op $F64 (Opcode.Fadd))
-  (FpuOPRRR.FaddD))
-
-(rule
-  (f_arithmatic_op $F32 (Opcode.Fsub))
-  (FpuOPRRR.FsubS))
-(rule
-  (f_arithmatic_op $F64 (Opcode.Fsub))
-  (FpuOPRRR.FsubD))
-
-(rule
-  (f_arithmatic_op $F32 (Opcode.Fmul))
-  (FpuOPRRR.FmulS))
-
-(rule
-  (f_arithmatic_op $F64 (Opcode.Fmul))
-  (FpuOPRRR.FmulD))
-
-(rule
-  (f_arithmatic_op $F32 (Opcode.Fdiv))
-  (FpuOPRRR.FdivS))
-
-(rule
-  (f_arithmatic_op $F64 (Opcode.Fdiv))
-  (FpuOPRRR.FdivD))
-
 
 (decl move_f_to_x (Reg Type) Reg)
 (extern constructor move_f_to_x move_f_to_x)
@@ -1671,21 +2093,6 @@
 (decl move_x_to_f (Reg Type) Reg)
 (extern constructor move_x_to_f move_x_to_f)
 
-
-;;float copy sign bit op.
-(decl f_copysign_op (Type) FpuOPRRR)
-(rule (f_copysign_op $F32) (FpuOPRRR.FsgnjS))
-(rule (f_copysign_op $F64) (FpuOPRRR.FsgnjD))
-
-;;float copy neg sign bit op.
-(decl f_copy_neg_sign_op (Type) FpuOPRRR)
-(rule (f_copy_neg_sign_op $F32) (FpuOPRRR.FsgnjnS))
-(rule (f_copy_neg_sign_op $F64) (FpuOPRRR.FsgnjnD))
-
-(decl fabs_copy_sign (Type) FpuOPRRR)
-(rule (fabs_copy_sign $F32) (FpuOPRRR.FsgnjxS))
-(rule (fabs_copy_sign $F64) (FpuOPRRR.FsgnjxD))
-
 (decl gen_stack_addr (StackSlot Offset32) Reg )
 (extern constructor gen_stack_addr gen_stack_addr)
 
@@ -1734,13 +2141,13 @@
 (rule
   (gen_bitselect ty c x y)
   (let
-    ((tmp_x Reg (alu_rrr (AluOPRRR.And) c x))
+    ((tmp_x Reg (rv_and c x))
       ;;;inverse condition
-      (c_inverse Reg (gen_bit_not c))
+      (c_inverse Reg (rv_not c))
       ;;;get all y part.
-      (tmp_y Reg (alu_rrr (AluOPRRR.And) c_inverse y))
+      (tmp_y Reg (rv_and c_inverse y))
       ;;;get reuslt.
-      (result Reg (alu_rrr (AluOPRRR.Or) tmp_x tmp_y)))
+      (result Reg (rv_or tmp_x tmp_y)))
     result))
 
 (decl gen_int_select (Type IntSelectOP ValueRegs ValueRegs) ValueRegs)
@@ -1831,7 +2238,7 @@
     (;; move to x register.
       (tmp Reg (move_f_to_x x ty))
       ;; inverse all bits.
-      (tmp2 Reg (gen_bit_not tmp)))
+      (tmp2 Reg (rv_not tmp)))
     ;; move back to float register.
     (move_x_to_f tmp2 ty)))
 
@@ -1850,27 +2257,22 @@
   (i128_sub x y )
   (let
     (;; low part.
-      (low Reg (alu_rrr (AluOPRRR.Sub) (value_regs_get x 0) (value_regs_get y 0)))
+      (low Reg (rv_sub (value_regs_get x 0) (value_regs_get y 0)))
       ;; compute borrow.
-      (borrow Reg (alu_rrr (AluOPRRR.SltU) (value_regs_get x 0) low))
+      (borrow Reg (rv_sltu (value_regs_get x 0) low))
       ;;
-      (high_tmp Reg (alu_rrr (AluOPRRR.Sub) (value_regs_get x 1) (value_regs_get y 1)))
+      (high_tmp Reg (rv_sub (value_regs_get x 1) (value_regs_get y 1)))
       ;;
-      (high Reg (alu_rrr (AluOPRRR.Sub) high_tmp borrow)))
+      (high Reg (rv_sub high_tmp borrow)))
     (value_regs low high)))
 
 
-(decl gen_fabs (Reg Type) Reg)
-(rule
-  (gen_fabs x ty)
-  (fpu_rrr (fabs_copy_sign ty) ty x x))
-
 ;;; Returns the sum in the first register, and the overflow test in the second.
 (decl lower_uadd_overflow (Reg Reg Type) ValueRegs)
 
 (rule 1
   (lower_uadd_overflow x y $I64)
-  (let ((tmp Reg (alu_add x y))
+  (let ((tmp Reg (rv_add x y))
         (test Reg (gen_icmp (IntCC.UnsignedLessThan) tmp x $I64)))
     (value_regs tmp test)))
 
@@ -1878,8 +2280,8 @@
   (lower_uadd_overflow x y (fits_in_32 ty))
   (let ((tmp_x Reg (ext_int_if_need $false x ty))
         (tmp_y Reg (ext_int_if_need $false y ty))
-        (sum Reg (alu_add tmp_x tmp_y))
-        (test Reg (alu_srli sum (ty_bits ty))))
+        (sum Reg (rv_add tmp_x tmp_y))
+        (test Reg (rv_srli sum (imm12_const (ty_bits ty)))))
     (value_regs sum test)))
 
 (decl inst_output_get (InstOutput u8) ValueRegs)
@@ -1941,7 +2343,7 @@
 (rule 0 (truthy_to_reg $I128 regs)
       (let ((lo Reg (value_regs_get regs 0))
             (hi Reg (value_regs_get regs 1)))
-        (alu_rrr (AluOPRRR.Or) lo hi)))
+        (rv_or lo hi)))
 
 ;; Default behavior for branching based on an input value.
 (rule
@@ -1986,21 +2388,11 @@
 (decl load_ra () Reg)
 (extern constructor load_ra load_ra)
 
-;;;
-(decl gen_andn (Reg Reg) Reg)
-(rule 1 (gen_andn rs1 rs2)
-  (alu_rrr (AluOPRRR.Andn) rs1 rs2))
-
-;;;
-(decl gen_orn (Reg Reg) Reg)
-(rule 1 (gen_orn rs1 rs2)
-  (alu_rrr (AluOPRRR.Orn) rs1 rs2))
-
 (decl gen_rev8 (Reg) Reg)
 (rule 1
   (gen_rev8 rs)
   (if-let $true (has_zbb))
-  (alu_rr_funct12 (AluOPRRI.Rev8) rs))
+  (rv_rev8 rs))
 
 (rule
   (gen_rev8 rs)
@@ -2017,7 +2409,7 @@
 (rule 1
   (gen_brev8 rs _)
   (if-let $true (has_zbkb))
-  (alu_rr_funct12 (AluOPRRI.Brev8) rs))
+  (rv_brev8 rs))
 (rule
   (gen_brev8 rs ty)
   (if-let $false (has_zbkb))
@@ -2034,7 +2426,7 @@
 (decl neg (Type ValueRegs) ValueRegs)
 (rule 1 (neg (fits_in_64 (ty_int ty)) val)
   (value_reg
-    (alu_rrr (AluOPRRR.Sub) (zero_reg) (value_regs_get val 0))))
+    (rv_neg (value_regs_get val 0))))
 
 (rule 2 (neg $I128 val)
   (i128_sub (value_regs_zero) val))
@@ -2044,7 +2436,7 @@
 (decl max (Type Reg Reg) Reg)
 (rule (max (fits_in_64 (ty_int ty)) x y)
   (if-let $true (has_zbb))
-  (alu_rrr (AluOPRRR.Max) x y))
+  (rv_max x y))
 
 (rule (max (fits_in_64 (ty_int ty)) x y)
   (if-let $false (has_zbb))
@@ -2082,11 +2474,11 @@
   (gen_div_overflow rs1 rs2 ty)
   (let
     ((r_const_neg_1 Reg (load_imm12 -1))
-      (r_const_min Reg (alu_slli (load_imm12 1) 63))
+      (r_const_min Reg (rv_slli (load_imm12 1) (imm12_const 63)))
       (tmp_rs1 Reg (shift_int_to_most_significant rs1 ty))
       (t1 Reg (gen_icmp (IntCC.Equal) r_const_neg_1 rs2 ty))
       (t2 Reg (gen_icmp (IntCC.Equal) r_const_min tmp_rs1 ty))
-      (test Reg (alu_and t1 t2)))
+      (test Reg (rv_and t1 t2)))
     (gen_trapif test (TrapCode.IntegerOverflow))))
 
 (decl gen_div_by_zero (Reg) InstOutput)
@@ -2107,12 +2499,8 @@
 (rule
   (madd n m a)
   (let
-    ((t Reg (alu_rrr (AluOPRRR.Mul) n m)))
-    (alu_add t a)))
-
-(decl umulh (Reg Reg) Reg)
-(rule (umulh a b)
-  (alu_rrr (AluOPRRR.Mulhu) a b))
+    ((t Reg (rv_mul n m)))
+    (rv_add t a)))
 
 ;;;; Helpers for bmask ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
@@ -2136,7 +2524,7 @@
   (lower_bmask (fits_in_64 ty) $I128 val)
   (let ((lo Reg (value_regs_get val 0))
         (hi Reg (value_regs_get val 1))
-        (combined Reg (alu_rrr (AluOPRRR.Or) lo hi)))
+        (combined Reg (rv_or lo hi)))
     (lower_bmask ty $I64 (value_reg combined))))
 
 ;; Conversion of one 64-bit value to a 128-bit one. Duplicate the result of the
@@ -2188,37 +2576,13 @@
 ;;;; Helpers for floating point comparisons ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (decl not (Reg) Reg)
-(rule (not x) (alu_rr_imm12 (AluOPRRI.Xori) x (imm_from_bits 1)))
-
-(decl emit_or (Reg Reg) Reg)
-(rule (emit_or x y) (alu_rrr (AluOPRRR.Or) x y))
-
-(decl emit_and (Reg Reg) Reg)
-(rule (emit_and x y) (alu_rrr (AluOPRRR.And) x y))
+(rule (not x) (rv_xori x (imm_from_bits 1)))
 
 (decl is_not_nan (Type Reg) Reg)
-(rule (is_not_nan ty a) (feq ty a a))
-
-(decl feq (Type Reg Reg) Reg)
-(rule (feq $F32 a b) (fpu_rrr (FpuOPRRR.FeqS) $I64 a b))
-(rule (feq $F64 a b) (fpu_rrr (FpuOPRRR.FeqD) $I64 a b))
-
-(decl flt (Type Reg Reg) Reg)
-(rule (flt $F32 a b) (fpu_rrr (FpuOPRRR.FltS) $I64 a b))
-(rule (flt $F64 a b) (fpu_rrr (FpuOPRRR.FltD) $I64 a b))
-
-(decl fle (Type Reg Reg) Reg)
-(rule (fle $F32 a b) (fpu_rrr (FpuOPRRR.FleS) $I64 a b))
-(rule (fle $F64 a b) (fpu_rrr (FpuOPRRR.FleD) $I64 a b))
-
-(decl fgt (Type Reg Reg) Reg)
-(rule (fgt ty a b) (flt ty b a))
-
-(decl fge (Type Reg Reg) Reg)
-(rule (fge ty a b) (fle ty b a))
+(rule (is_not_nan ty a) (rv_feq ty a a))
 
 (decl ordered (Type Reg Reg) Reg)
-(rule (ordered ty a b) (emit_and (is_not_nan ty a) (is_not_nan ty b)))
+(rule (ordered ty a b) (rv_and (is_not_nan ty a) (is_not_nan ty b)))
 
 (type CmpResult (enum
                   (Result
@@ -2278,64 +2642,64 @@
 ;; a == b
 (rule
   (emit_fcmp (FloatCC.Equal) ty a b)
-  (cmp_result (feq ty a b)))
+  (cmp_result (rv_feq ty a b)))
 
 ;; a != b
 ;; == !(a == b)
 (rule
   (emit_fcmp (FloatCC.NotEqual) ty a b)
-  (cmp_result_invert (feq ty a b)))
+  (cmp_result_invert (rv_feq ty a b)))
 
 ;; a < b || a > b
 (rule
   (emit_fcmp (FloatCC.OrderedNotEqual) ty a b)
-  (cmp_result (emit_or (flt ty a b) (fgt ty a b))))
+  (cmp_result (rv_or (rv_flt ty a b) (rv_fgt ty a b))))
 
 ;; !(ordered a b) || a == b
 (rule
   (emit_fcmp (FloatCC.UnorderedOrEqual) ty a b)
-  (cmp_result (emit_or (not (ordered ty a b)) (feq ty a b))))
+  (cmp_result (rv_or (not (ordered ty a b)) (rv_feq ty a b))))
 
 ;; a < b
 (rule
   (emit_fcmp (FloatCC.LessThan) ty a b)
-  (cmp_result (flt ty a b)))
+  (cmp_result (rv_flt ty a b)))
 
 ;; a <= b
 (rule
   (emit_fcmp (FloatCC.LessThanOrEqual) ty a b)
-  (cmp_result (fle ty a b)))
+  (cmp_result (rv_fle ty a b)))
 
 ;; a > b
 (rule
   (emit_fcmp (FloatCC.GreaterThan) ty a b)
-  (cmp_result (fgt ty a b)))
+  (cmp_result (rv_fgt ty a b)))
 
 ;; a >= b
 (rule
   (emit_fcmp (FloatCC.GreaterThanOrEqual) ty a b)
-  (cmp_result (fge ty a b)))
+  (cmp_result (rv_fge ty a b)))
 
 ;; !(ordered a b) || a < b
 ;; == !(ordered a b && a >= b)
 (rule
   (emit_fcmp (FloatCC.UnorderedOrLessThan) ty a b)
-  (cmp_result_invert (emit_and (ordered ty a b) (fge ty a b))))
+  (cmp_result_invert (rv_and (ordered ty a b) (rv_fge ty a b))))
 
 ;; !(ordered a b) || a <= b
 ;; == !(ordered a b && a > b)
 (rule
   (emit_fcmp (FloatCC.UnorderedOrLessThanOrEqual) ty a b)
-  (cmp_result_invert (emit_and (ordered ty a b) (fgt ty a b))))
+  (cmp_result_invert (rv_and (ordered ty a b) (rv_fgt ty a b))))
 
 ;; !(ordered a b) || a > b
 ;; == !(ordered a b && a <= b)
 (rule
   (emit_fcmp (FloatCC.UnorderedOrGreaterThan) ty a b)
-  (cmp_result_invert (emit_and (ordered ty a b) (fle ty a b))))
+  (cmp_result_invert (rv_and (ordered ty a b) (rv_fle ty a b))))
 
 ;; !(ordered a b) || a >= b
 ;; == !(ordered a b && a < b)
 (rule
   (emit_fcmp (FloatCC.UnorderedOrGreaterThanOrEqual) ty a b)
-  (cmp_result_invert (emit_and (ordered ty a b) (flt ty a b))))
+  (cmp_result_invert (rv_and (ordered ty a b) (rv_flt ty a b))))
diff --git a/cranelift/codegen/src/isa/riscv64/lower.isle b/cranelift/codegen/src/isa/riscv64/lower.isle
index 4909269a16..3bc08aa704 100644
--- a/cranelift/codegen/src/isa/riscv64/lower.isle
+++ b/cranelift/codegen/src/isa/riscv64/lower.isle
@@ -29,7 +29,7 @@
 
 ;; Base case, simply adding things in registers.
 (rule 0 (lower (has_type (fits_in_64 ty) (iadd x y)))
-  (alu_add x y))
+  (rv_add x y))
 
 ;; Special cases for when one operand is an immediate that fits in 12 bits.
 (rule 1 (lower (has_type (fits_in_64 ty) (iadd x (imm12_from_value y))))
@@ -42,11 +42,11 @@
 ;; Needs `Zba`
 (rule 3 (lower (has_type $I64 (iadd x (uextend y @ (value_type $I32)))))
   (if-let $true (has_zba))
-  (alu_rrr (AluOPRRR.Adduw) y x))
+  (rv_adduw y x))
 
 (rule 4 (lower (has_type $I64 (iadd (uextend x @ (value_type $I32)) y)))
   (if-let $true (has_zba))
-  (alu_rrr (AluOPRRR.Adduw) x y))
+  (rv_adduw x y))
 
 ;; Add with const shift. We have a few of these instructions with `Zba`.
 (decl pure partial match_shnadd (Imm64) AluOPRRR)
@@ -88,13 +88,13 @@
 
 ;; I128 cases
 (rule 7 (lower (has_type $I128 (iadd x y)))
-  (let ((low Reg (alu_add (value_regs_get x 0) (value_regs_get y 0)))
+  (let ((low Reg (rv_add (value_regs_get x 0) (value_regs_get y 0)))
         ;; compute carry.
-        (carry Reg (alu_rrr (AluOPRRR.SltU) low (value_regs_get y 0)))
+        (carry Reg (rv_sltu low (value_regs_get y 0)))
         ;;
-        (high_tmp Reg (alu_add (value_regs_get x 1) (value_regs_get y 1)))
+        (high_tmp Reg (rv_add (value_regs_get x 1) (value_regs_get y 1)))
         ;; add carry.
-        (high Reg (alu_add high_tmp carry)))
+        (high Reg (rv_add high_tmp carry)))
     (value_regs low high)))
 
 ;;; Rules for `uadd_overflow_trap` ;;;;;;;;;;;;;
@@ -109,10 +109,10 @@
 ;; Base case, simply subtracting things in registers.
 
 (rule -2 (lower (has_type (fits_in_64 ty) (isub x y)))
-  (alu_rrr (AluOPRRR.Sub) x y))
+  (rv_sub x y))
 
 (rule -1 (lower (has_type (fits_in_32 ty) (isub x y)))
-  (alu_rrr (AluOPRRR.Subw) x y))
+  (rv_subw x y))
 
 (rule (lower (has_type $I128 (isub x y)))
   (i128_sub x y))
@@ -126,9 +126,9 @@
 ;;;; Rules for `imul` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (rule -2 (lower (has_type (fits_in_64 ty) (imul x y)))
-  (alu_rrr (AluOPRRR.Mul) x y))
+  (rv_mul x y))
 (rule -1 (lower (has_type (fits_in_32 ty) (imul x y)))
-  (alu_rrr (AluOPRRR.Mulw) x y))
+  (rv_mulw x y))
 
 ;;;; Rules for `smulhi` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule (lower (has_type (fits_in_64 ty) (smulhi x y)))
@@ -152,14 +152,14 @@
 
       ;; 128bit mul formula:
       ;;   dst_lo = x_lo * y_lo
-      ;;   dst_hi = umulhi(x_lo, y_lo) + (x_lo * y_hi) + (x_hi * y_lo)
+      ;;   dst_hi = mulhu(x_lo, y_lo) + (x_lo * y_hi) + (x_hi * y_lo)
       ;;
       ;; We can convert the above formula into the following
-      ;; umulh   dst_hi, x_lo, y_lo
+      ;; mulhu   dst_hi, x_lo, y_lo
       ;; madd    dst_hi, x_lo, y_hi, dst_hi
       ;; madd    dst_hi, x_hi, y_lo, dst_hi
       ;; madd    dst_lo, x_lo, y_lo, zero
-      (dst_hi1 Reg (umulh x_lo y_lo))
+      (dst_hi1 Reg (rv_mulhu x_lo y_lo))
       (dst_hi2 Reg (madd x_lo y_hi dst_hi1))
       (dst_hi Reg (madd x_hi y_lo dst_hi2))
       (dst_lo Reg (madd x_lo y_lo (zero_reg))))
@@ -172,7 +172,7 @@
   (let
     ((y2 Reg (ext_int_if_need $false y ty))
       (_ InstOutput (gen_div_by_zero y2)))
-    (alu_rrr (AluOPRRR.Divuw) (ext_int_if_need $false x ty) y2)))
+    (rv_divuw (ext_int_if_need $false x ty) y2)))
 
 (rule -1 (lower (has_type (fits_in_32 ty) (sdiv x y)))
   (let
@@ -180,18 +180,18 @@
       (b Reg (ext_int_if_need $true y ty))
       (_ InstOutput (gen_div_overflow a b ty))
       (_ InstOutput (gen_div_by_zero b)))
-    (alu_rrr (AluOPRRR.Divw) a b)))
+    (rv_divw a b)))
 
 (rule (lower (has_type $I64 (sdiv x y)))
   (let
     ((_ InstOutput (gen_div_overflow x y $I64))
       (_ InstOutput (gen_div_by_zero y))    )
-    (alu_rrr (AluOPRRR.Div) x y)))
+    (rv_div x y)))
 
 (rule (lower (has_type $I64 (udiv x y)))
   (let
     ((_ InstOutput (gen_div_by_zero y)))
-    (alu_rrr (AluOPRRR.DivU) x y)))
+    (rv_divu x y)))
 
 ;;;; Rules for `rem` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
@@ -199,46 +199,46 @@
   (let
     ((y2 Reg (ext_int_if_need $false y ty))
       (_ InstOutput (gen_div_by_zero y2)))
-    (alu_rrr (AluOPRRR.Remuw) (ext_int_if_need $false x ty) y2)))
+    (rv_remuw (ext_int_if_need $false x ty) y2)))
 
 (rule -1 (lower (has_type (fits_in_16 ty) (srem x y)))
   (let
     ((y2 Reg (ext_int_if_need $true y ty))
       (_ InstOutput (gen_div_by_zero y2)))
-    (alu_rrr (AluOPRRR.Remw) (ext_int_if_need $true x ty) y2)))
+    (rv_remw (ext_int_if_need $true x ty) y2)))
 
 (rule (lower (has_type $I32 (srem x y)))
   (let
     ((y2 Reg (ext_int_if_need $true y $I32))
       (_ InstOutput (gen_div_by_zero y2)))
-   (alu_rrr (AluOPRRR.Remw) x y2)))
+   (rv_remw x y2)))
 
 (rule (lower (has_type $I32 (urem x y)))
   (let
     ((y2 Reg (ext_int_if_need $false y $I32))
         (_ InstOutput (gen_div_by_zero y2)))
-    (alu_rrr (AluOPRRR.Remuw) x y2)))
+    (rv_remuw x y2)))
 
 (rule (lower (has_type $I64 (srem x y)))
   (let
     ((_ InstOutput (gen_div_by_zero y)))
-    (alu_rrr (AluOPRRR.Rem) x y)))
+    (rv_rem x y)))
 
 (rule (lower (has_type $I64 (urem x y)))
   (let
     ((_ InstOutput (gen_div_by_zero y)))
-    (alu_rrr (AluOPRRR.RemU) x y)))
+    (rv_remu x y)))
 
 ;;;; Rules for `and` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule -1 (lower (has_type (fits_in_64 (ty_int ty)) (band x y)))
-  (alu_rrr (AluOPRRR.And) x y))
+  (rv_and x y))
 
 ;; Special cases for when one operand is an immediate that fits in 12 bits.
 (rule 2 (lower (has_type (fits_in_64 (ty_int ty)) (band x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Andi) x y))
+  (rv_andi x y))
 
 (rule 1 (lower (has_type (fits_in_64 (ty_int ty)) (band (imm12_from_value x) y)))
-  (alu_rr_imm12 (AluOPRRI.Andi) y x))
+  (rv_andi y x))
 
 (rule (lower (has_type $I128 (band x y)))
   (lower_b128_binary (AluOPRRR.And) x y))
@@ -255,37 +255,37 @@
 
 (rule 3 (lower (has_type (fits_in_64 (ty_int ty)) (band x (bnot y))))
   (if-let $true (has_zbb))
-  (gen_andn x y))
+  (rv_andn x y))
 
 (rule 4 (lower (has_type (fits_in_64 (ty_int ty)) (band (bnot y) x)))
   (if-let $true (has_zbb))
-  (gen_andn x y))
+  (rv_andn x y))
 
 (rule 5 (lower (has_type $I128 (band x (bnot y))))
   (if-let $true (has_zbb))
   (let
-    ((low Reg (gen_andn (value_regs_get x 0) (value_regs_get y 0)))
-      (high Reg (gen_andn (value_regs_get x 1) (value_regs_get y 1))))
+    ((low Reg (rv_andn (value_regs_get x 0) (value_regs_get y 0)))
+      (high Reg (rv_andn (value_regs_get x 1) (value_regs_get y 1))))
     (value_regs low high)))
 
 (rule 6 (lower (has_type $I128 (band (bnot y) x)))
   (if-let $true (has_zbb))
   (let
-    ((low Reg (gen_andn (value_regs_get x 0) (value_regs_get y 0)))
-      (high Reg (gen_andn (value_regs_get x 1) (value_regs_get y 1))))
+    ((low Reg (rv_andn (value_regs_get x 0) (value_regs_get y 0)))
+      (high Reg (rv_andn (value_regs_get x 1) (value_regs_get y 1))))
     (value_regs low high)))
 
 
 ;;;; Rules for `or` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule -1 (lower (has_type (fits_in_64 (ty_int ty)) (bor x y)))
-  (alu_rrr (AluOPRRR.Or) x y))
+  (rv_or x y))
 
 ;; Special cases for when one operand is an immediate that fits in 12 bits.
 (rule 2 (lower (has_type (fits_in_64 (ty_int ty)) (bor x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Ori) x y))
+  (rv_ori x y))
 
 (rule 1 (lower (has_type (fits_in_64 (ty_int ty)) (bor (imm12_from_value x) y)))
-  (alu_rr_imm12 (AluOPRRI.Ori) y x))
+  (rv_ori y x))
 
 (rule (lower (has_type $I128 (bor x y)))
   (lower_b128_binary (AluOPRRR.Or) x y))
@@ -302,37 +302,37 @@
 
 (rule 3 (lower (has_type (fits_in_64 (ty_int ty)) (bor x (bnot y))))
   (if-let $true (has_zbb))
-  (gen_orn x y))
+  (rv_orn x y))
 
 (rule 4 (lower (has_type (fits_in_64 (ty_int ty)) (bor (bnot y) x)))
   (if-let $true (has_zbb))
-  (gen_orn x y))
+  (rv_orn x y))
 
 (rule 5 (lower (has_type $I128 (bor x (bnot y))))
   (if-let $true (has_zbb))
   (let
-    ((low Reg (gen_orn (value_regs_get x 0) (value_regs_get y 0)))
-      (high Reg (gen_orn (value_regs_get x 1) (value_regs_get y 1))))
+    ((low Reg (rv_orn (value_regs_get x 0) (value_regs_get y 0)))
+      (high Reg (rv_orn (value_regs_get x 1) (value_regs_get y 1))))
     (value_regs low high)))
 
 (rule 6 (lower (has_type $I128 (bor (bnot y) x)))
   (if-let $true (has_zbb))
   (let
-    ((low Reg (gen_orn (value_regs_get x 0) (value_regs_get y 0)))
-      (high Reg (gen_orn (value_regs_get x 1) (value_regs_get y 1))))
+    ((low Reg (rv_orn (value_regs_get x 0) (value_regs_get y 0)))
+      (high Reg (rv_orn (value_regs_get x 1) (value_regs_get y 1))))
     (value_regs low high)))
 
 
 ;;;; Rules for `xor` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule -1 (lower (has_type (fits_in_64 (ty_int ty)) (bxor x y)))
-  (alu_rrr (AluOPRRR.Xor) x y))
+  (rv_xor x y))
 
 ;; Special cases for when one operand is an immediate that fits in 12 bits.
 (rule 2 (lower (has_type (fits_in_64 (ty_int ty)) (bxor x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Xori) x y))
+  (rv_xori x y))
 
 (rule 1 (lower (has_type (fits_in_64 (ty_int ty)) (bxor (imm12_from_value x) y)))
-  (alu_rr_imm12 (AluOPRRI.Xori) y x))
+  (rv_xori y x))
 
 (rule (lower (has_type $I128 (bxor x y)))
   (lower_b128_binary (AluOPRRR.Xor) x y))
@@ -346,7 +346,7 @@
 
 ;;;; Rules for `bnot` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule -1 (lower (has_type (fits_in_64 (ty_int ty)) (bnot x)))
-  (alu_rr_imm12 (AluOPRRI.Xori) x (imm_from_neg_bits -1)))
+  (rv_xori x (imm_from_neg_bits -1)))
 
 (rule (lower (has_type $I128 (bnot x)))
   (bnot_128 x))
@@ -402,35 +402,35 @@
 ;; The instructions below are present in RV64I and sign-extend the result to 64 bits.
 
 (rule 1 (lower (has_type $I64 (sextend (has_type $I32 (iadd x y)))))
-  (alu_rrr (AluOPRRR.Addw) x y))
+  (rv_addw x y))
 
 (rule 1 (lower (has_type $I64 (sextend (has_type $I32 (isub x y)))))
-  (alu_rrr (AluOPRRR.Subw) x y))
+  (rv_subw x y))
 
 (rule 1 (lower (has_type $I64 (sextend (has_type $I32 (ishl x y)))))
-  (alu_rrr (AluOPRRR.Sllw) x (value_regs_get y 0)))
+  (rv_sllw x (value_regs_get y 0)))
 
 (rule 1 (lower (has_type $I64 (sextend (has_type $I32 (ushr x y)))))
-  (alu_rrr (AluOPRRR.Srlw) x (value_regs_get y 0)))
+  (rv_srlw x (value_regs_get y 0)))
 
 (rule 1 (lower (has_type $I64 (sextend (has_type $I32 (sshr x y)))))
-  (alu_rrr (AluOPRRR.Sraw) x (value_regs_get y 0)))
+  (rv_sraw x (value_regs_get y 0)))
 
 
 (rule 2 (lower (has_type $I64 (sextend (has_type $I32 (iadd x (imm12_from_value y))))))
-  (alu_rr_imm12 (AluOPRRI.Addiw) x y))
+  (rv_addiw x y))
 
 (rule 3 (lower (has_type $I64 (sextend (has_type $I32 (iadd (imm12_from_value x) y)))))
-  (alu_rr_imm12 (AluOPRRI.Addiw) y x))
+  (rv_addiw y x))
 
 (rule 2 (lower (has_type $I64 (sextend (has_type $I32 (ishl x (imm12_from_value y))))))
-  (alu_rr_imm12 (AluOPRRI.Slliw) x y))
+  (rv_slliw x y))
 
 (rule 2 (lower (has_type $I64 (sextend (has_type $I32 (ushr x (imm12_from_value y))))))
-  (alu_rr_imm12 (AluOPRRI.SrliW) x y))
+  (rv_srliw x y))
 
 (rule 2 (lower (has_type $I64 (sextend (has_type $I32 (sshr x (imm12_from_value y))))))
-  (alu_rr_imm12 (AluOPRRI.Sraiw) x y))
+  (rv_sraiw x y))
 
 ;;;; Rules for `popcnt` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule (lower (has_type (fits_in_64 ty) (popcnt x)))
@@ -440,31 +440,31 @@
 
 ;;;; Rules for `ishl` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule 1 (lower (has_type $I8 (ishl x y)))
-  (alu_rrr (AluOPRRR.Sllw) x (alu_andi (value_regs_get y 0) 7))
-)
+  (rv_sllw x (rv_andi (value_regs_get y 0) (imm12_const 7))))
+
 (rule 2 (lower (has_type $I8 (ishl x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Slliw) x (imm12_and y 7)))
+  (rv_slliw x (imm12_and y 7)))
 
 (rule 1 (lower (has_type $I16 (ishl x y)))
-  (alu_rrr (AluOPRRR.Sllw) x (alu_andi (value_regs_get y 0) 15))
-)
+  (rv_sllw x (rv_andi (value_regs_get y 0) (imm12_const 15))))
+
 (rule 2 (lower (has_type $I16 (ishl x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Slliw) x (imm12_and y 15)))
+  (rv_slliw x (imm12_and y 15)))
 
 (rule 1 (lower (has_type $I32 (ishl x y)))
-  (alu_rrr (AluOPRRR.Sllw) x (value_regs_get y 0)))
+  (rv_sllw x (value_regs_get y 0)))
 (rule 2 (lower (has_type $I32 (ishl x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Slliw) x y))
+  (rv_slliw x y))
 
 (rule 2 (lower (has_type $I64 (ishl x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Slli) x y))
+  (rv_slli x y))
 (rule 1 (lower (has_type $I64 (ishl x y)))
-  (alu_rrr (AluOPRRR.Sll) x (value_regs_get y 0)))
+  (rv_sll x (value_regs_get y 0)))
 
 ;; With `Zba` we have a shift that zero extends the LHS argument.
 (rule 3 (lower (has_type $I64 (ishl (uextend x @ (value_type $I32)) (maybe_uextend (imm12_from_value y)))))
   (if-let $true (has_zba))
-  (alu_rr_imm12 (AluOPRRI.SlliUw) x y))
+  (rv_slliuw x y))
 
 ;; I128 cases
 (rule 0 (lower (has_type $I128 (ishl x y)))
@@ -472,26 +472,26 @@
 
 ;;;; Rules for `ushr` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule 1 (lower (has_type $I8 (ushr x y)))
-  (alu_rrr (AluOPRRR.Srlw) (ext_int_if_need $false x $I8) (alu_andi (value_regs_get y 0) 7))
-)
+  (rv_srlw (ext_int_if_need $false x $I8) (rv_andi (value_regs_get y 0) (imm12_const 7))))
+
 (rule 2 (lower (has_type $I8 (ushr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.SrliW) (ext_int_if_need $false x $I8) (imm12_and y 7)))
+  (rv_srliw (ext_int_if_need $false x $I8) (imm12_and y 7)))
 
 (rule 1 (lower (has_type $I16 (ushr x y)))
-  (alu_rrr (AluOPRRR.Srlw) (ext_int_if_need $false x $I16) (alu_andi (value_regs_get y 0) 15))
-)
+  (rv_srlw (ext_int_if_need $false x $I16) (rv_andi (value_regs_get y 0) (imm12_const 15))))
+
 (rule 2 (lower (has_type $I16 (ushr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.SrliW) (ext_int_if_need $false x $I16) (imm12_and y 15)))
+  (rv_srliw (ext_int_if_need $false x $I16) (imm12_and y 15)))
 
 (rule 1 (lower (has_type $I32 (ushr x y)))
-  (alu_rrr (AluOPRRR.Srlw) x (value_regs_get y 0)))
+  (rv_srlw x (value_regs_get y 0)))
 (rule 2 (lower (has_type $I32 (ushr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.SrliW) x y))
+  (rv_srliw x y))
 
 (rule 2 (lower (has_type $I64 (ushr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Srli) x y))
+  (rv_srli x y))
 (rule 1 (lower (has_type $I64 (ushr x y)))
-  (alu_rrr (AluOPRRR.Srl) x (value_regs_get y 0)))
+  (rv_srl x (value_regs_get y 0)))
 
 (rule 0 (lower (has_type $I128 (ushr x y)))
   (lower_i128_ushr x y))
@@ -499,25 +499,25 @@
 
 ;;;; Rules for `sshr` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule 1 (lower (has_type $I8 (sshr x y)))
-  (alu_rrr (AluOPRRR.Sra) (ext_int_if_need $true x $I8) (alu_andi (value_regs_get y 0) 7))
-)
+  (rv_sra (ext_int_if_need $true x $I8) (rv_andi (value_regs_get y 0) (imm12_const 7))))
+
 (rule 2 (lower (has_type $I8 (sshr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Srai) (ext_int_if_need $true x $I8) (imm12_and y 7)))
+  (rv_srai (ext_int_if_need $true x $I8) (imm12_and y 7)))
 
 (rule 1 (lower (has_type $I16 (sshr x y)))
-  (alu_rrr (AluOPRRR.Sra) (ext_int_if_need $true x $I16) (alu_andi (value_regs_get y 0) 15))
-)
+  (rv_sra (ext_int_if_need $true x $I16) (rv_andi (value_regs_get y 0) (imm12_const 15))))
+
 (rule 2 (lower (has_type $I16 (sshr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Srai) (ext_int_if_need $true x $I16) (imm12_and y 15)))
+  (rv_srai (ext_int_if_need $true x $I16) (imm12_and y 15)))
 
 (rule 1 (lower (has_type $I32 (sshr x y)))
-  (alu_rrr (AluOPRRR.Sraw) x (value_regs_get y 0)))
+  (rv_sraw x (value_regs_get y 0)))
 (rule 2 (lower (has_type $I32 (sshr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Sraiw) x y))
+  (rv_sraiw x y))
 (rule 1 (lower (has_type $I64 (sshr x y)))
-  (alu_rrr (AluOPRRR.Sra) x (value_regs_get y 0)))
+  (rv_sra x (value_regs_get y 0)))
 (rule 2 (lower (has_type $I64 (sshr x (imm12_from_value y))))
-  (alu_rr_imm12 (AluOPRRI.Srai) x y))
+  (rv_srai x y))
 (rule 0 (lower (has_type $I128 (sshr x y)))
   (lower_i128_sshr x (value_regs_get y 0)))
 
@@ -538,32 +538,25 @@
 
 
 ;;;; Rules for `fabs` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(rule
-  (lower (has_type ty (fabs x)))
-  (gen_fabs x ty))
+(rule (lower (has_type ty (fabs x)))
+  (rv_fabs ty x))
 
 ;;;; Rules for `fneg` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(rule
-  (lower (has_type ty (fneg x)))
-  (fpu_rrr (f_copy_neg_sign_op ty) ty x x))
+(rule (lower (has_type ty (fneg x)))
+  (rv_fneg ty x))
 
 ;;;; Rules for `fcopysign` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (rule (lower (has_type ty (fcopysign x y)))
-  (fpu_rrr (f_copysign_op ty) ty x y))
+  (rv_fsgnj ty x y))
 
 ;;;; Rules for `fma` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(rule (lower (has_type $F32 (fma x y z)))
-  (fpu_rrrr (FpuOPRRRR.FmaddS) $F64 x y z))
-(rule (lower (has_type $F64 (fma x y z)))
-  (fpu_rrrr (FpuOPRRRR.FmaddD) $F64 x y z))
+(rule (lower (has_type ty (fma x y z)))
+  (rv_fmadd ty x y z))
 
 
 ;;;; Rules for `sqrt` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(rule (lower (has_type $F32 (sqrt x)))
-  (fpu_rr (FpuOPRR.FsqrtS) $F64 x))
-
-(rule (lower (has_type $F64 (sqrt x)))
-  (fpu_rr (FpuOPRR.FsqrtD) $F64 x))
+(rule (lower (has_type ty (sqrt x)))
+  (rv_fsqrt ty x))
 
 
 ;;;; Rules for `AtomicRMW` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -600,7 +593,7 @@
     (has_type (valid_atomic_transaction ty) (atomic_rmw flags (AtomicRmwOp.Sub) addr x)))
   (let
     ((tmp WritableReg (temp_writable_reg ty))
-      (x2 Reg (alu_rrr (AluOPRRR.Sub) (zero_reg) x)))
+     (x2 Reg (rv_neg x)))
     (gen_atomic (get_atomic_rmw_op ty (AtomicRmwOp.Add)) addr x2 (atomic_amo))))
 
 (decl gen_atomic_rmw_loop (AtomicRmwOp Type Reg Reg) Reg)
@@ -634,14 +627,14 @@
 
 (decl gen_atomic_offset (Reg Type) Reg)
 (rule 1 (gen_atomic_offset p (fits_in_16 ty))
-  (alu_slli (alu_andi p 3) 3))
+  (rv_slli (rv_andi p (imm12_const 3)) (imm12_const 3)))
 
 (rule (gen_atomic_offset p _)
   (zero_reg))
 
 (decl gen_atomic_p (Reg Type) Reg)
 (rule 1 (gen_atomic_p p (fits_in_16 ty))
-  (alu_andi p -4))
+  (rv_andi p (imm12_const -4)))
 
 (rule (gen_atomic_p p _)
   p)
@@ -662,28 +655,26 @@
   (gen_move2 (value_regs_get x 0) ty ty))
 
 ;;;;;  Rules for `fpromote`;;;;;;;;;;;;;;;;;
-(rule
-  (lower (has_type ty (fpromote x)))
-  (fpu_rr (FpuOPRR.FcvtDS) ty x))
+(rule (lower (fpromote x))
+  (rv_fcvtds x))
 
-(rule
-  (lower (has_type ty (fdemote x)))
-  (fpu_rr (FpuOPRR.FcvtSD) ty x))
+;;;;;  Rules for `fdemote`;;;;;;;;;;;;;;;;;;
+(rule (lower (fdemote x))
+  (rv_fcvtsd x))
 
 
-;;;;;  Rules for `for float arithmatic`
-(rule
-  (lower (has_type ty (fadd x y)))
-  (fpu_rrr (f_arithmatic_op ty (Opcode.Fadd)) ty x y))
-(rule
-  (lower (has_type ty (fsub x y)))
-  (fpu_rrr (f_arithmatic_op ty (Opcode.Fsub)) ty x y))
-(rule
-  (lower (has_type ty (fmul x y)))
-  (fpu_rrr (f_arithmatic_op ty (Opcode.Fmul)) ty x y))
-(rule
-  (lower (has_type ty (fdiv x y)))
-  (fpu_rrr (f_arithmatic_op ty (Opcode.Fdiv)) ty x y))
+;;;;;  Rules for for float arithmetic
+(rule (lower (has_type ty (fadd x y)))
+  (rv_fadd ty x y))
+
+(rule (lower (has_type ty (fsub x y)))
+  (rv_fsub ty x y))
+
+(rule (lower (has_type ty (fmul x y)))
+  (rv_fmul ty x y))
+
+(rule (lower (has_type ty (fdiv x y)))
+  (rv_fdiv ty x y))
 
 (rule
   (lower (has_type ty (fmin x y)))
@@ -710,13 +701,13 @@
 
 ;; Null references are represented by the constant value `0`.
 (rule (lower (is_null v))
-  (seqz v))
+  (rv_seqz v))
 
 ;;;;;  Rules for `is_invalid`;;;;;;;;;
 
 ;; Invalid references are represented by the constant value `-1`.
 (rule (lower (is_invalid v))
-  (seqz (alu_rr_imm12 (AluOPRRI.Addi) v (imm12_const 1))))
+  (rv_seqz (rv_addi v (imm12_const 1))))
 
 ;;;;;  Rules for `select`;;;;;;;;;
 (rule