[BUG] ExecuteM64 does not truncate the operands of DIVW/DIVUW/REMW/REMUW to 32 bits

[tchajed]

The following bug was root-caused and confirmed by Fable 5. The section below was written by Claude Fable 5; it looks correct to me.

The basic issue is that divw (and friends) on rv64 are specified to be a division of only the lower 32-bits, but the Haskell semantics uses the entire 64 bits.

---

src/riscv/Spec/ExecuteM64.v
implements the RV64M W-form divisions by
dividing the full 64-bit register values and sign-extending only the
result. The ISA requires both operands to be truncated to their lower 32
bits before the division. The model therefore disagrees with hardware
(and qemu) whenever an operand of divw/divuw/remw/remuw has live
bits above bit 31 — for divuw/remuw even on canonical sign-extended
values.

Affected: current master (checked 2026-07-16) and the released opam
package coq-riscv.0.0.6. The bug appears to originate in the Haskell
source these files are generated from:
mit-plv/riscv-semantics's
src/Spec/ExecuteM64.hs
has the same structure, so a fix may belong in both places.

What the ISA says

RISC-V unprivileged spec, "M" extension, RV64M:

DIVW and DIVUW are RV64 instructions that divide the lower 32 bits of
rs1 by the lower 32 bits of rs2, treating them as signed and
unsigned integers respectively, placing the 32-bit quotient in rd,
sign-extended to 64 bits. REMW and REMUW are RV64 instructions that
provide the corresponding signed and unsigned remainder operations
respectively.

What ExecuteM64.v does

| Spec.Decode.Divuw rd rs1 rs2 =>
    Bind (Spec.Machine.getRegister rs1) (fun x =>
            Bind (Spec.Machine.getRegister rs2) (fun y =>
                    let q :=
                      if reg_eqb y (ZToReg 0) : bool then Utility.Utility.maxUnsigned else
                      Utility.Utility.divu x y in          (* <-- x, y are the full 64-bit registers *)
                    Spec.Machine.setRegister rd (Utility.Utility.s32 q)))

and analogously for Divw (div x y), Remw (rem x y), Remuw
(remu x y). With the standard MachineWidth_XLEN instance, divu is
word.divu on 64-bit words and s32 is word.sextend 32, so the only
32-bit truncation happens after the divide. The guards are wrong in the
same way:

• Divuw/Remuw's zero-divisor test is y == 0 on the full 64-bit y;
  it should test y[31:0] == 0.
• Divw/Remw's overflow test is x == minSigned && y == -1 against the
  64-bit minSigned (-2^63); it should be x[31:0] == -2^31 && y[31:0] == -1.

Concrete divergences (model vs. qemu-riscv64)

instruction	rs1	rs2	ExecuteM64	hardware / qemu
divuw	2^32	2	s32(2^32 / 2) = 0xFFFFFFFF80000000	lower32(rs1) = 0, 0/2 = 0
divuw	10	2^32	10 / 2^32 = 0	lower32(rs2) = 0 → div-by-zero = 0xFFFFFFFFFFFFFFFF
divuw	0xFFFFFFFF80000000	2	s32(0x7FFFFFFFC0000000) = 0xFFFFFFFFC0000000	0x80000000 / 2 = 0x40000000
remuw	2^32	3	s32(2^32 mod 3) = 1	0 mod 3 = 0
divw	0x500000064	0x0ABCDEF000000003	s32(0x500000064 / 0xABC…003) = 0	100 / 3 = 33

The third row is worth emphasizing: 0xFFFFFFFF80000000 is the
canonical sign-extended form of INT32_MIN, i.e. exactly the value an
RV64 register holds after any W-form instruction — so this is not just a
non-canonical-input corner case.

mulw is unaffected (the low 32 bits of a product depend only on the low
32 bits of the operands), which is probably why the bug went unnoticed.
srlw/sraw are fine too (they explicitly take regToShamt5/u32).

qemu reproduction

#include <stdio.h>
#include <stdint.h>
int main(void) {
  uint64_t x = 1ULL << 32, y = 2, q;
  asm("divuw %0, %1, %2" : "=r"(q) : "r"(x), "r"(y));
  printf("divuw(2^32, 2) = 0x%016lx\n", q);   /* prints 0x0000000000000000 */
  return 0;
}

$ riscv64-linux-gnu-gcc -static t.c -o t && qemu-riscv64 ./t
divuw(2^32, 2) = 0x0000000000000000

Coq reproduction

Require Import Coq.ZArith.ZArith.
Require Import riscv.Utility.Utility.
Require Import riscv.Utility.MkMachineWidth.
Require Import riscv.Utility.Words64Naive.
Require Import coqutil.Word.Interface coqutil.Word.Naive.
Local Open Scope Z_scope.

(* ExecuteM64's Divuw data path: s32 (if y = 0 then maxUnsigned else divu x y) *)
Definition model_divuw (x y : Z) : Z :=
  let x' := word.of_Z (word := word64) x in
  let y' := word.of_Z (word := word64) y in
  word.unsigned (s32 (if reg_eqb y' (ZToReg 0) then maxUnsigned else divu x' y')).

Eval vm_compute in model_divuw (2^32) 2.
(* = 18446744071562067968 (0xFFFFFFFF80000000); hardware: 0 *)
Eval vm_compute in model_divuw 10 (2^32).
(* = 0; hardware: 18446744073709551615 (division by zero: lower32(rs2) = 0) *)

Impact

Any proof built on this spec can certify a binary whose divw-family
behavior differs from real hardware, and conversely a correct binary can
be unprovable against the model. The divergence is silent: it only
manifests when an operand's bits 63:32 matter, which compilers routinely
produce (e.g. a 64-bit induction variable divided with a W-form
instruction after the compiler proves the value fits in 32 bits — the
register may still hold history above bit 31 on paths the model and
hardware then disagree about).

Suggested fix

Truncate both operands first and test the guards on the truncated values
(sketch; u32 x := ZToReg (bitSlice (regToZ_unsigned x) 0 32) or
equivalent, s32 as today):

| Spec.Decode.Divuw rd rs1 rs2 => ...
    let x' := u32 x in let y' := u32 y in
    let q := if reg_eqb y' (ZToReg 0) then maxUnsigned else divu x' y' in
    setRegister rd (s32 q)

| Spec.Decode.Divw rd rs1 rs2 => ...
    let x' := s32 x in let y' := s32 y in
    let q := if andb (reg_eqb x' (s32 (ZToReg (2^31)))) (reg_eqb y' (negate (ZToReg 1)))
             then x'
             else if reg_eqb y' (ZToReg 0) then negate (ZToReg 1)
             else div x' y' in
    setRegister rd (s32 q)

(and analogously for Remw/Remuw). With sign-extended (s32) operands
the 64-bit signed div/rem coincides with 32-bit division, and with
zero-extended (u32) operands the 64-bit divu/remu coincides with
32-bit unsigned division, so the final s32 on the result then matches
the ISA. If the fix should instead go through the hs-to-coq pipeline, the
corresponding change lands in riscv-semantics's ExecuteM64.hs.

---

Would riscv-tests have caught this?

(this section was human written)

The upstream tests in riscv-tests do cover this issue in the rv64um suite, even in the pinned commit, but riscv-coq doesn't use that particular suite (it builds only rv64mi rv64si rv64ui rv64uf). That said, even upstream the coverage for this particular issue is poor: divw/remw/remuw need new
vectors with live bits above bit 31 to get proper coverage.

[samuelgruetter]

Nice find!

Right now I need my Fable trial quota for something else, but if you wanna give it a try, I'd be curious to hear if Fable can fix it in the Haskell riscv-semantics, download and install the right ghc and hs-to-coq version, and rerun hs-to-coq by invoking make convert in riscv-coq. (Note that riscv-coq puts hs-to-coq-generated .v files under version control so that not everyone needs to run hs-to-coq). The expected riscv-semantics version is "pinned" using the text file deps/riscv-semantics and will need to be changed, while the expected hs-to-coq version ("pinned" using deps/hs-to-coq) can probably be kept.

[JasonGross]

Fixed end to end:

• riscv-semantics: Fix RV64 divw/divuw/remw/remuw to truncate operands to 32 bits riscv-semantics#36 — divw/divuw/remw/remuw now truncate both operands to 32 bits first (s32 for the signed ops, u32 for the unsigned ones) and test the zero-divisor / signed-overflow guards on the truncated values, matching the RV64M spec.
• riscv-coq: Fix RV64 divw/divuw/remw/remuw to truncate operands to 32 bits (regenerated) #49 — ExecuteM64.v regenerated by rerunning make convert with the pinned hs-to-coq (deps/hs-to-coq unchanged); the diff is just the div/rem definitions plus the deps/riscv-semantics bump. That pin points at the riscv-semantics PR head and should be updated to the upstream commit once Please create a tag for Coq 8.19 in Coq Platform 2024.01 #36 merges.

The regenerated spec compiles, and its div/rem data paths reproduce the hardware values for every row of the divergence table above (plus overflow / div-by-zero corner cases).

Written by Claude (Anthropic AI) at the request of and under the supervision of @JasonGross.