add missing ops from veir

RISCV/Instructions.lean

@@ -521,6 +521,43 @@ def ctz (rs1_val : BitVec 64) : BitVec 64 := BitVec.ctz rs1_val
 -/
 def ctzw (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.ctz (BitVec.extractLsb 31 0 rs1_val))
 
+/--
+  This instruction counts the number of 1’s (i.e., set bits) in the source register.
+-/
+def cpop (rs1_val : BitVec 64) : BitVec 64 := BitVec.cpop rs1_val
+
+/--
+  This instruction counts the number of 1’s (i.e., set bits) in the least-significant word of the
+  source register.
+-/
+def cpopw (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.cpop (BitVec.extractLsb 31 0 rs1_val))
+
+/--
+  Bitwise OR-combine of a single byte: the result is all zeros if the input byte is zero,
+  and all ones otherwise.
+-/
+def orcByte (b : BitVec 8) : BitVec 8 := if b = 0#8 then 0#8 else BitVec.allOnes 8
+
+/--
+  Combines the bits within each byte using bitwise logical OR. This sets the bits of each byte in
+  the result rd to all zeros if no bit within the respective byte of rs is set, or to all ones if
+  any bit within the respective byte of rs is set.
+-/
+def orcb (rs1_val : BitVec 64) : BitVec 64 :=
+  orcByte (BitVec.extractLsb 63 56 rs1_val) ++ orcByte (BitVec.extractLsb 55 48 rs1_val) ++
+  orcByte (BitVec.extractLsb 47 40 rs1_val) ++ orcByte (BitVec.extractLsb 39 32 rs1_val) ++
+  orcByte (BitVec.extractLsb 31 24 rs1_val) ++ orcByte (BitVec.extractLsb 23 16 rs1_val) ++
+  orcByte (BitVec.extractLsb 15 8 rs1_val) ++ orcByte (BitVec.extractLsb 7 0 rs1_val)
+
+/--
+  This instruction reverses the order of the bytes in rs.
+-/
+def rev8 (rs1_val : BitVec 64) : BitVec 64 :=
+  BitVec.extractLsb 7 0 rs1_val ++ BitVec.extractLsb 15 8 rs1_val ++
+  BitVec.extractLsb 23 16 rs1_val ++ BitVec.extractLsb 31 24 rs1_val ++
+  BitVec.extractLsb 39 32 rs1_val ++ BitVec.extractLsb 47 40 rs1_val ++
+  BitVec.extractLsb 55 48 rs1_val ++ BitVec.extractLsb 63 56 rs1_val
+
 /--
   This instruction performs a rotate right on the least-significant word of rs1 by the amount in the
   least-significant log2(XLEN) bits of shamt. The resulting word value is sign-extended by
@@ -628,3 +665,78 @@ def packw (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
 /-! ## Zbkc: Carry-less multiplication for Cryptography -/
 
 /-! ## Zbkx: Carry-less multiplication for Cryptography -/
+
+/-! # "Zicond" Extension for Integer Conditional Operations -/
+
+/--
+  If rs2 contains the value zero, this instruction writes the value zero to rd. Otherwise, this
+  instruction copies the contents of rs1 to rd.
+-/
+def czeroeqz (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
+  if rs2_val = 0#64 then 0#64 else rs1_val
+
+/--
+  If rs2 contains a nonzero value, this instruction writes the value zero to rd. Otherwise, this
+  instruction copies the contents of rs1 to rd.
+-/
+def czeronez (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
+  if rs2_val = 0#64 then rs1_val else 0#64
+
+/-! # Pseudo-instructions -/
+
+/--
+  Copy register rs1 into rd (`addi rd, rs1, 0`).
+-/
+def mv (rs1_val : BitVec 64) : BitVec 64 := rs1_val
+
+/--
+  Two's complement negation (`sub rd, x0, rs1`).
+-/
+def neg (rs1_val : BitVec 64) : BitVec 64 := 0#64 - rs1_val
+
+/--
+  Two's complement negation of the least-significant word, sign-extended to 64 bits
+  (`subw rd, x0, rs1`).
+-/
+def negw (rs1_val : BitVec 64) : BitVec 64 :=
+  BitVec.signExtend 64 (0#32 - BitVec.extractLsb 31 0 rs1_val)
+
+/--
+  One's complement (`xori rd, rs1, -1`).
+-/
+def not (rs1_val : BitVec 64) : BitVec 64 := ~~~rs1_val
+
+/--
+  Set rd to 1 if rs1 is equal to zero, else 0 (`sltiu rd, rs1, 1`).
+-/
+def seqz (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.ofBool (rs1_val == 0#64))
+
+/--
+  Set rd to 1 if rs1 is not equal to zero, else 0 (`sltu rd, x0, rs1`).
+-/
+def snez (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.ofBool (rs1_val != 0#64))
+
+/--
+  Set rd to 1 if rs1 is less than zero (signed), else 0 (`slt rd, rs1, x0`).
+-/
+def sltz (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.ofBool (rs1_val.slt 0#64))
+
+/--
+  Set rd to 1 if rs1 is greater than zero (signed), else 0 (`slt rd, x0, rs1`).
+-/
+def sgtz (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.ofBool ((0#64).slt rs1_val))
+
+/--
+  Sign-extend the least-significant word of rs1 (`addiw rd, rs1, 0`).
+-/
+def sextw (rs1_val : BitVec 64) : BitVec 64 := BitVec.signExtend 64 (BitVec.extractLsb 31 0 rs1_val)
+
+/--
+  Zero-extend the least-significant byte of rs1 (`andi rd, rs1, 255`).
+-/
+def zextb (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.extractLsb 7 0 rs1_val)
+
+/--
+  Zero-extend the least-significant word of rs1 (`add.uw rd, rs1, x0`).
+-/
+def zextw (rs1_val : BitVec 64) : BitVec 64 := BitVec.zeroExtend 64 (BitVec.extractLsb 31 0 rs1_val)

RISCV/SailPure.lean

@@ -184,6 +184,42 @@ def zbb_ctz (rs1 : BitVec 64) : BitVec 64 :=
 def zbb_ctzw (rs1 : BitVec 64) : BitVec 64 :=
   to_bits (l := 64) (Sail.BitVec.countTrailingZeros (Sail.BitVec.extractLsb rs1 31 0))
 
+
+
+/-- Monad-free version of `LeanRV64D.Functions.count_ones` (without the overflow assertion). -/
+def count_ones_pure (x : BitVec k_n) : Nat := Id.run do
+  let count : Nat := 0
+  let loop_i_lower := 0
+  let loop_i_upper := ((Sail.BitVec.length x) -i 1)
+  let mut loop_vars := count
+  for i in [loop_i_lower:loop_i_upper:1]i do
+    let count := loop_vars
+    loop_vars := if (((Sail.BitVec.access x i) == 1#1) : Bool) then (count +i 1) else count
+  pure loop_vars
+
+def zbb_cpop (rs1 : BitVec 64) : BitVec 64 :=
+  to_bits (l := 64) (count_ones_pure rs1)
+
+def zbb_cpopw (rs1 : BitVec 64) : BitVec 64 :=
+  to_bits (l := 64) (count_ones_pure (Sail.BitVec.extractLsb rs1 31 0))
+
+def zbb_orcb (rs1_val : BitVec 64) : BitVec 64 := Id.run do
+  let result : xlenbits := (zeros (n := 64))
+  let loop_i_lower := 0
+  let loop_i_upper := (LeanRV64D.Functions.xlen -i 8)
+  let mut loop_vars := result
+  for i in [loop_i_lower:loop_i_upper:8]i do
+    let result := loop_vars
+    loop_vars :=
+      (Sail.BitVec.updateSubrange result (i +i 7) i
+        (if (((Sail.BitVec.extractLsb rs1_val (i +i 7) i) == (zeros (n := (((i +i 7) -i i) +i 1)))) : Bool)
+        then 0x00#8
+        else 0xFF#8))
+  pure loop_vars
+
+def zbb_rev8 (rs1_val : BitVec 64) : BitVec 64 :=
+  rev8 rs1_val
+
 def zbb_roriw (shamt : BitVec 5) (rs1 : BitVec 64) :=
   sign_extend (m := 64) (rotate_bits_right (Sail.BitVec.extractLsb rs1 31 0) shamt)
 
@@ -233,3 +269,47 @@ def zbkb_packw (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
 /-! ## Zbkc: Carry-less multiplication for Cryptography -/
 
 /-! ## Zbkx: Carry-less multiplication for Cryptography -/
+
+/-! # "Zicond" Extension for Integer Conditional Operations -/
+
+def zicond_rtype (rs2_val : BitVec 64) (rs1_val : BitVec 64) (op : zicondop) : BitVec 64 :=
+  let condition : Bool :=
+    match op with
+    | .CZERO_EQZ => rs2_val == (zeros (n := 64))
+    | .CZERO_NEZ => rs2_val != (zeros (n := 64))
+  if condition then (zeros (n := 64)) else rs1_val
+
+/-! # Pseudo-instructions -/
+
+def mv (rs1_val : BitVec 64) : BitVec 64 :=
+  itype 0#12 rs1_val iop.ADDI
+
+def neg (rs1_val : BitVec 64) : BitVec 64 :=
+  rtype rop.SUB rs1_val (zeros (n := 64))
+
+def negw (rs1_val : BitVec 64) : BitVec 64 :=
+  rtypew ropw.SUBW rs1_val (zeros (n := 64))
+
+def not (rs1_val : BitVec 64) : BitVec 64 :=
+  itype 0xFFF#12 rs1_val iop.XORI
+
+def seqz (rs1_val : BitVec 64) : BitVec 64 :=
+  itype 1#12 rs1_val iop.SLTIU
+
+def snez (rs1_val : BitVec 64) : BitVec 64 :=
+  rtype rop.SLTU rs1_val (zeros (n := 64))
+
+def sltz (rs1_val : BitVec 64) : BitVec 64 :=
+  rtype rop.SLT (zeros (n := 64)) rs1_val
+
+def sgtz (rs1_val : BitVec 64) : BitVec 64 :=
+  rtype rop.SLT rs1_val (zeros (n := 64))
+
+def sextw (rs1_val : BitVec 64) : BitVec 64 :=
+  addiw 0#12 rs1_val
+
+def zextb (rs1_val : BitVec 64) : BitVec 64 :=
+  itype 0xFF#12 rs1_val iop.ANDI
+
+def zextw (rs1_val : BitVec 64) : BitVec 64 :=
+  zba_rtypeuw (zeros (n := 64)) rs1_val 0#2