diff --git a/changes/02-bugfix/1544-riscv-ct-doit.md b/changes/02-bugfix/1544-riscv-ct-doit.md new file mode 100644 index 000000000..68675fccc --- /dev/null +++ b/changes/02-bugfix/1544-riscv-ct-doit.md @@ -0,0 +1,7 @@ +- On RISC-V, the `DIV`, `DIVU`, `REM` and `REMU` instructions are no longer + considered constant-time nor DOIT: they have data-dependent latency on + typical implementations and are excluded from the Zkt ("Data-Independent + Execution Latency") safe list of the RISC-V specification; every other + instruction keeps its classification, now documented against the Zkt list + ([PR 1544](https://github.com/jasmin-lang/jasmin/pull/1544); + fixes [#1013](https://github.com/jasmin-lang/jasmin/issues/1013)). diff --git a/compiler/CCT/fail/doit/riscv/div.jazz b/compiler/CCT/fail/doit/riscv/div.jazz new file mode 100644 index 000000000..b75a29a3c --- /dev/null +++ b/compiler/CCT/fail/doit/riscv/div.jazz @@ -0,0 +1,11 @@ +/* Unsigned division lowers to DIVU, which is not in the Zkt safe list, + hence not DOIT. */ +#[ct="secret -> secret"] +export fn div(reg u32 x) -> reg u32 { + reg u32 d q; + x = x; + d = 3; + q = x / d; + q = q; + return q; +} diff --git a/compiler/CCT/fail/doit/riscv/mod.jazz b/compiler/CCT/fail/doit/riscv/mod.jazz new file mode 100644 index 000000000..eff59b0b8 --- /dev/null +++ b/compiler/CCT/fail/doit/riscv/mod.jazz @@ -0,0 +1,11 @@ +/* Unsigned remainder lowers to REMU, which is not in the Zkt safe list, + hence not DOIT. */ +#[ct="secret -> secret"] +export fn mod(reg u32 x) -> reg u32 { + reg u32 d q; + x = x; + d = 3; + q = x % d; + q = q; + return q; +} diff --git a/compiler/CCT/fail/riscv/div_secret.jazz b/compiler/CCT/fail/riscv/div_secret.jazz new file mode 100644 index 000000000..c29a8e585 --- /dev/null +++ b/compiler/CCT/fail/riscv/div_secret.jazz @@ -0,0 +1,10 @@ +/* DIV has data-dependent latency, it is not constant-time. */ +#[ct="secret -> secret"] +export fn div_secret(reg u32 x) -> reg u32 { + reg u32 d q; + x = x; + d = 3; + q = #DIV(x, d); + q = q; + return q; +} diff --git a/compiler/CCT/fail/riscv/rem_secret.jazz b/compiler/CCT/fail/riscv/rem_secret.jazz new file mode 100644 index 000000000..60084a102 --- /dev/null +++ b/compiler/CCT/fail/riscv/rem_secret.jazz @@ -0,0 +1,10 @@ +/* REM has data-dependent latency, it is not constant-time. */ +#[ct="secret -> secret"] +export fn rem_secret(reg u32 x) -> reg u32 { + reg u32 d q; + x = x; + d = 3; + q = #REM(x, d); + q = q; + return q; +} diff --git a/compiler/CCT/success/doit/riscv/arith.jazz b/compiler/CCT/success/doit/riscv/arith.jazz new file mode 100644 index 000000000..1256c9bf3 --- /dev/null +++ b/compiler/CCT/success/doit/riscv/arith.jazz @@ -0,0 +1,15 @@ +/* MUL, ADD, XOR and SLLI are in the Zkt safe list; loads and stores of + secret data are also accepted (see the documentation of [id_doit] in + proofs/compiler/riscv_instr_decl.v). */ +#[ct="secret * secret -> secret"] +export fn arith(reg u32 a, reg u32 b) -> reg u32 { + stack u32 s; + reg u32 t; + t = a * b; + t += b; + t ^= a; + t <<= 2; + s = t; + t = s; + return t; +} diff --git a/compiler/CCT/success/riscv/div_public.jazz b/compiler/CCT/success/riscv/div_public.jazz new file mode 100644 index 000000000..60d10991f --- /dev/null +++ b/compiler/CCT/success/riscv/div_public.jazz @@ -0,0 +1,14 @@ +/* Division and remainder are allowed on public data. */ +#[ct="public -> public"] +export fn add_div_mod(reg u32 x) -> reg u32 { + reg u32 x1 x2 d q q1 r r1; + x1 = x; x2 = x; + d = 3; + q = x1 / d; + q1 = q; + r = x2 % d; + r = r1; + r = r + q1; + r = r; + return r; +} diff --git a/compiler/Makefile b/compiler/Makefile index a6ade6c98..fa0093cd7 100644 --- a/compiler/Makefile +++ b/compiler/Makefile @@ -17,7 +17,7 @@ CHECKCATS ?= \ arm-m4-stack-zero-unrolled \ risc-v-stack-zero-loop \ risc-v-stack-zero-unrolled \ - CCT CCT-DOIT SCT + CCT CCT-riscv CCT-DOIT CCT-DOIT-riscv SCT # -------------------------------------------------------------------- DESTDIR ?= diff --git a/compiler/config/tests.config b/compiler/config/tests.config index 052ec9537..6e9d01637 100644 --- a/compiler/config/tests.config +++ b/compiler/config/tests.config @@ -9,13 +9,26 @@ kodirs = tests/fail/nolea/x86-64 bin = ./jasmin-ct okdirs = CCT/success kodirs = CCT/fail -exclude = CCT/success/doit CCT/fail/doit +exclude = CCT/success/doit CCT/fail/doit CCT/success/riscv CCT/fail/riscv + +[test-CCT-riscv] +bin = ./jasmin-ct +args = --arch riscv +okdirs = CCT/success/riscv +kodirs = CCT/fail/riscv [test-CCT-DOIT] bin = ./jasmin-ct args = --doit okdirs = CCT/success/doit kodirs = CCT/fail/doit +exclude = CCT/success/doit/riscv CCT/fail/doit/riscv + +[test-CCT-DOIT-riscv] +bin = ./jasmin-ct +args = --doit --arch riscv +okdirs = CCT/success/doit/riscv +kodirs = CCT/fail/doit/riscv [test-SCT] bin = ./jasmin-ct diff --git a/compiler/src/riscv_arch_full.ml b/compiler/src/riscv_arch_full.ml index 5d292a561..8ff5aa26b 100644 --- a/compiler/src/riscv_arch_full.ml +++ b/compiler/src/riscv_arch_full.ml @@ -24,11 +24,19 @@ module Riscv_core = struct let alloc_stack_need_extra sz = not (Riscv_params_core.is_arith_small (Conv.cz_of_z sz)) - (* FIXME RISCV: check if everything is ct *) + (* Division and remainder have data-dependent latency on typical + implementations, and are explicitly excluded from the Zkt safe list of + the RISC-V specification ("Data-Independent Execution Latency Subset"); + see the documentation in proofs/compiler/riscv_instr_decl.v. + Every other instruction is assumed to be constant-time, as on the other + architectures. *) let is_ct_asm_op (o : asm_op) = match o with + | Riscv_instr_decl.DIV | DIVU | REM | REMU -> false | _ -> true + (* All of the extra ops compile into CT instructions (no DIV/REM): + SWAP into xor, add_large_imm into lui/addi/add. *) let is_ct_asm_extra (_o : extra_op) = true end diff --git a/docs/source/tools/ct.md b/docs/source/tools/ct.md index 401cbec5f..cbb1298d7 100644 --- a/docs/source/tools/ct.md +++ b/docs/source/tools/ct.md @@ -41,7 +41,7 @@ any pass, but the type system can be more precise after some step of compilation - `--doit` The usual leakage model for constant-time considers that only conditional instructions and load/store instructions leak. This option allows to consider a stronger model where non Data Independent Timing instructions -leak. In this model, secret data can only be applied to Data Independent Timing instructions ([DOIT](https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/best-practices/data-operand-independent-timing-isa-guidance.html) for Intel and [DIT](https://developer.arm.com/documentation/ddi0595/2020-12/AArch64-Registers/DIT--Data-Independent-Timing) for Arm). +leak. In this model, secret data can only be applied to Data Independent Timing instructions ([DOIT](https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/best-practices/data-operand-independent-timing-isa-guidance.html) for Intel, [DIT](https://developer.arm.com/documentation/ddi0595/2020-12/AArch64-Registers/DIT--Data-Independent-Timing) for Arm and [Zkt](https://github.com/riscv/riscv-crypto/blob/main/doc/scalar/riscv-crypto-scalar-zkt.adoc) for RISC-V). - `--infer` Infer security contracts. This can be used for development purpose but should not be used for production. - `--print` @@ -287,6 +287,10 @@ Third-party references: - [List of DOIT instructions on Intel platforms](https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/resources/data-operand-independent-timing-instructions.html) - [ARM documentation for DIT](https://developer.arm.com/documentation/ddi0601/2025-06/AArch64-Registers/DIT--Data-Independent-Timing) +- [RISC-V Zkt extension, “Data-Independent Execution Latency Subset”](https://github.com/riscv/riscv-crypto/blob/main/doc/scalar/riscv-crypto-scalar-zkt.adoc) + (RISC-V has no run-time flag akin to Intel DOIT or ARM DIT: Zkt is an + attestation, by the hardware vendor, that the listed instructions have + data-independent latency) More details can be found in the following paper: diff --git a/proofs/compiler/riscv_instr_decl.v b/proofs/compiler/riscv_instr_decl.v index d26b9b825..e16f23c32 100644 --- a/proofs/compiler/riscv_instr_decl.v +++ b/proofs/compiler/riscv_instr_decl.v @@ -41,11 +41,61 @@ Definition pp_name name args := - J type: imm -> reg (e.g.: JAL, update PC) *) -Definition RTypeInstruction ws semi jazz_name asm_name: instr_desc_t := +(* -------------------------------------------------------------------- *) +(* Data operand independent timing (field [id_doit]). + + Unlike x86 (Intel DOIT mode) and ARM (DIT bit), RISC-V has no + execution mode guaranteeing data operand independent timing. The + reference is instead the ratified Zkt extension, "Data-Independent + Execution Latency Subset" (chapter Zkt of the RISC-V Cryptography + Extensions Volume I: Scalar & Entropy Source Instructions, also a + chapter of the unprivileged ISA manual; + https://github.com/riscv/riscv-crypto). On a machine implementing + Zkt, the instructions of its safe list "do not leak information about + processed secret data through differences in execution latency". + + We set [id_doit := DOIT] exactly for the instructions of the Zkt safe + list, restricted to the RV32IM subset modelled here: + - RVI: lui, auipc, addi, slti, sltiu, xori, ori, andi, slli, srli, + srai, add, sub, sll, slt, sltu, xor, srl, sra, or, and; + - RVM: mul, mulh, mulhu, mulhsu. + Division and remainder (div, divu, rem, remu) are deliberately + excluded from Zkt — the spec notes that "cryptographers typically + assume division to be variable-time" — hence [NOT_DOIT]. For the + same reason they are not constant-time either, see [is_ct_asm_op] in + compiler/src/riscv_arch_full.ml. + + Assembler pseudo-instructions are classified according to their + canonical expansions, which only use Zkt-listed instructions: + MV -> addi, NOT -> xori, NEG -> sub, LI -> lui+addi, + LA -> auipc+addi. (An assembler may substitute compressed forms; + those are either themselves Zkt-listed — c.mv, c.addi, c.lui, ... — + or, like c.li, only take immediate operands, i.e. program constants, + so they cannot leak secret data either way.) + + Loads and stores are not in the Zkt list: their latency depends on + the address (state of the memory hierarchy). Jasmin's leakage model + already leaks the address of every memory access, so checked programs + never index memory with secret data. As on the other architectures + (Intel's DOIT list contains MOV, ARM's DIT covers LDR/STR), we + moreover assume that the latency of a memory access does not depend + on the transferred *values*, and mark LOAD and STORE as [DOIT]. + + Two caveats, both documented in the Zkt chapter: + - The latency requirement does not apply to HINT encodings of the + listed instructions (typically rd = x0). Jasmin never emits such + encodings: x0 is not part of the declared register file + (cf. riscv_decl.v), so it is never the destination of an + instruction. + - Zkt only constrains machines that implement it; on other machines + no instruction carries any timing guarantee, and checking a program + under the DOIT policy is only meaningful for Zkt hardware. *) + +Definition RTypeInstruction ws semi jazz_name asm_name (doit : doit_t) : instr_desc_t := let tin := [:: lreg; lword ws ] in {| id_valid := true; - id_doit := DOIT; + id_doit := doit; id_msb_flag := MSB_MERGE; id_tin := tin; id_in := [:: Ea 1; Ea 2 ]; @@ -64,11 +114,11 @@ Definition RTypeInstruction ws semi jazz_name asm_name: instr_desc_t := id_semi_safe := fun _ => sem_lprod_ok_safe tin semi; |}. -Definition ITypeInstruction chk_imm ws semi jazz_name asm_name : instr_desc_t := +Definition ITypeInstruction chk_imm ws semi jazz_name asm_name (doit : doit_t) : instr_desc_t := let tin := [:: lreg; lword ws ] in {| id_valid := true; - id_doit := DOIT; + id_doit := doit; id_msb_flag := MSB_MERGE; (* imm are coded on 12 bits, not 32 *) id_tin := tin; @@ -174,90 +224,90 @@ Notation ty_rr := (sem_ltuple [:: lreg; lreg ]) (only parsing). (* Arithmetic *) Definition riscv_add_semi (wn wm : ty_r) : ty_r := (wn + wm)%w. -Definition riscv_ADD_instr : instr_desc_t := RTypeInstruction riscv_add_semi "ADD" "add". +Definition riscv_ADD_instr : instr_desc_t := RTypeInstruction riscv_add_semi "ADD" "add" DOIT. Definition prim_ADD := ("ADD"%string, primM ADD). -Definition riscv_ADDI_instr : instr_desc_t := ITypeInstruction_12s riscv_add_semi "ADDI" "addi". +Definition riscv_ADDI_instr : instr_desc_t := ITypeInstruction_12s riscv_add_semi "ADDI" "addi" DOIT. Definition prim_ADDI := ("ADDI"%string, primM ADDI). Definition riscv_sub_semi (wn wm : ty_r) : ty_r := (wn - wm)%w. -Definition riscv_SUB_instr : instr_desc_t := RTypeInstruction riscv_sub_semi "SUB" "sub". +Definition riscv_SUB_instr : instr_desc_t := RTypeInstruction riscv_sub_semi "SUB" "sub" DOIT. Definition prim_SUB := ("SUB"%string, primM SUB). (* Set less *) Definition riscv_slt_semi (wn wm : ty_r) : ty_r := if (wlt Signed wn wm) then 1%w else 0%w. -Definition riscv_SLT_instr : instr_desc_t := RTypeInstruction riscv_slt_semi "SLT" "slt". +Definition riscv_SLT_instr : instr_desc_t := RTypeInstruction riscv_slt_semi "SLT" "slt" DOIT. Definition prim_SLT := ("SLT"%string, primM SLT). -Definition riscv_SLTI_instr : instr_desc_t := ITypeInstruction_12s riscv_slt_semi "SLTI" "slti". +Definition riscv_SLTI_instr : instr_desc_t := ITypeInstruction_12s riscv_slt_semi "SLTI" "slti" DOIT. Definition prim_SLTI := ("SLTI"%string, primM SLTI). Definition riscv_sltu_semi (wn wm : ty_r) : ty_r := if (wlt Unsigned wn wm) then 1%w else 0%w. -Definition riscv_SLTU_instr : instr_desc_t := RTypeInstruction riscv_sltu_semi "SLTU" "sltu". +Definition riscv_SLTU_instr : instr_desc_t := RTypeInstruction riscv_sltu_semi "SLTU" "sltu" DOIT. Definition prim_SLTU := ("SLTU"%string, primM SLTU). -Definition riscv_SLTIU_instr : instr_desc_t := ITypeInstruction_12s riscv_sltu_semi "SLTIU" "sltiu". +Definition riscv_SLTIU_instr : instr_desc_t := ITypeInstruction_12s riscv_sltu_semi "SLTIU" "sltiu" DOIT. Definition prim_SLTIU := ("SLTIU"%string, primM SLTIU). (* Logical *) Definition riscv_and_semi (wn wm : ty_r) : ty_r := wand wn wm. -Definition riscv_AND_instr : instr_desc_t := RTypeInstruction riscv_and_semi "AND" "and". +Definition riscv_AND_instr : instr_desc_t := RTypeInstruction riscv_and_semi "AND" "and" DOIT. Definition prim_AND := ("AND"%string, primM AND). -Definition riscv_ANDI_instr : instr_desc_t := ITypeInstruction_12s riscv_and_semi "ANDI" "andi". +Definition riscv_ANDI_instr : instr_desc_t := ITypeInstruction_12s riscv_and_semi "ANDI" "andi" DOIT. Definition prim_ANDI := ("ANDI"%string, primM ANDI). Definition riscv_or_semi (wn wm : ty_r) : ty_r := wor wn wm. -Definition riscv_OR_instr : instr_desc_t := RTypeInstruction riscv_or_semi "OR" "or". +Definition riscv_OR_instr : instr_desc_t := RTypeInstruction riscv_or_semi "OR" "or" DOIT. Definition prim_OR := ("OR"%string, primM OR). -Definition riscv_ORI_instr : instr_desc_t := ITypeInstruction_12s riscv_or_semi "ORI" "ori". +Definition riscv_ORI_instr : instr_desc_t := ITypeInstruction_12s riscv_or_semi "ORI" "ori" DOIT. Definition prim_ORI := ("ORI"%string, primM ORI). Definition riscv_xor_semi (wn wm : ty_r): ty_r := wxor wn wm. -Definition riscv_XOR_instr : instr_desc_t := RTypeInstruction riscv_xor_semi "XOR" "xor". +Definition riscv_XOR_instr : instr_desc_t := RTypeInstruction riscv_xor_semi "XOR" "xor" DOIT. Definition prim_XOR := ("XOR"%string, primM XOR). -Definition riscv_XORI_instr : instr_desc_t := ITypeInstruction_12s riscv_xor_semi "XORI" "xori". +Definition riscv_XORI_instr : instr_desc_t := ITypeInstruction_12s riscv_xor_semi "XORI" "xori" DOIT. Definition prim_XORI := ("XORI"%string, primM XORI). (* Shift *) Definition riscv_sll_semi (wn : ty_r) (wm : word U8) : ty_r := wshl wn (wunsigned (wand wm (wrepr U8 31))). -Definition riscv_SLL_instr : instr_desc_t := RTypeInstruction riscv_sll_semi "SLL" "sll". +Definition riscv_SLL_instr : instr_desc_t := RTypeInstruction riscv_sll_semi "SLL" "sll" DOIT. Definition prim_SLL := ("SLL"%string, primM SLL). -Definition riscv_SLLI_instr : instr_desc_t := ITypeInstruction_5u riscv_sll_semi "SLLI" "slli". +Definition riscv_SLLI_instr : instr_desc_t := ITypeInstruction_5u riscv_sll_semi "SLLI" "slli" DOIT. Definition prim_SLLI := ("SLLI"%string, primM SLLI). Definition riscv_srl_semi (wn : ty_r) (wm : word U8) : ty_r := wshr wn (wunsigned (wand wm (wrepr U8 31))). -Definition riscv_SRL_instr : instr_desc_t := RTypeInstruction riscv_srl_semi "SRL" "srl". +Definition riscv_SRL_instr : instr_desc_t := RTypeInstruction riscv_srl_semi "SRL" "srl" DOIT. Definition prim_SRL := ("SRL"%string, primM SRL). -Definition riscv_SRLI_instr : instr_desc_t := ITypeInstruction_5u riscv_srl_semi "SRLI" "srli". +Definition riscv_SRLI_instr : instr_desc_t := ITypeInstruction_5u riscv_srl_semi "SRLI" "srli" DOIT. Definition prim_SRLI := ("SRLI"%string, primM SRLI). Definition riscv_sra_semi (wn : ty_r) (wm : word U8) : ty_r := wsar wn (wunsigned (wand wm (wrepr U8 31))). -Definition riscv_SRA_instr : instr_desc_t := RTypeInstruction riscv_sra_semi "SRA" "sra". +Definition riscv_SRA_instr : instr_desc_t := RTypeInstruction riscv_sra_semi "SRA" "sra" DOIT. Definition prim_SRA := ("SRA"%string, primM SRA). -Definition riscv_SRAI_instr : instr_desc_t := ITypeInstruction_5u riscv_sra_semi "SRAI" "srai". +Definition riscv_SRAI_instr : instr_desc_t := ITypeInstruction_5u riscv_sra_semi "SRAI" "srai" DOIT. Definition prim_SRAI := ("SRAI"%string, primM SRAI). @@ -270,7 +320,7 @@ Definition riscv_MV_instr : instr_desc_t := let semi := riscv_MV_semi in {| id_valid := true; - id_doit := DOIT; + id_doit := DOIT; (* Expands to addi (Zkt-listed) *) id_msb_flag := MSB_MERGE; id_tin := tin; id_in := [:: Ea 1 ]; @@ -300,7 +350,7 @@ Definition riscv_LA_instr : instr_desc_t := let semi := riscv_LA_semi in {| id_valid := true; - id_doit := DOIT; + id_doit := DOIT; (* Expands to auipc + addi (Zkt-listed) *) id_msb_flag := MSB_MERGE; id_tin := [:: lreg ]; id_in := [:: Ec 1 ]; @@ -330,7 +380,7 @@ Definition riscv_LI_instr : instr_desc_t := let semi := riscv_LI_semi in {| id_valid := true; - id_doit := DOIT; + id_doit := DOIT; (* Expands to lui + addi (Zkt-listed) *) id_msb_flag := MSB_MERGE; id_tin := tin; id_in := [:: Ea 1 ]; @@ -361,7 +411,7 @@ Definition riscv_NOT_instr : instr_desc_t := let semi := riscv_NOT_semi in {| id_valid := true; - id_doit := DOIT; + id_doit := DOIT; (* Expands to xori (Zkt-listed) *) id_msb_flag := MSB_MERGE; id_tin := tin; id_in := [:: Ea 1 ]; @@ -391,7 +441,7 @@ Definition riscv_NEG_instr : instr_desc_t := let semi := riscv_NEG_semi in {| id_valid := true; - id_doit := DOIT; + id_doit := DOIT; (* Expands to sub (Zkt-listed) *) id_msb_flag := MSB_MERGE; id_tin := tin; id_in := [:: Ea 1 ]; @@ -441,7 +491,7 @@ Definition riscv_LOAD_instr s ws : instr_desc_t := let semi := @riscv_extend_semi s reg_size ws in {| id_valid := if s is Signed then (ws <= U32)%CMP else (ws <= U16)%CMP ; - id_doit := DOIT; + id_doit := DOIT; (* Assumed, not in Zkt: see the note above *) id_msb_flag := MSB_MERGE; id_tin := tin; id_in := [:: Eu 1 ]; @@ -475,7 +525,7 @@ Definition riscv_STORE_instr ws : instr_desc_t := let semi := @riscv_extend_semi Unsigned ws ws in {| id_valid := (ws <= U32)%CMP; - id_doit := DOIT; + id_doit := DOIT; (* Assumed, not in Zkt: see the note above *) id_msb_flag := MSB_MERGE; (* ? *) id_tin := [:: lword ws ]; id_in := [:: Ea 0 ]; @@ -499,19 +549,19 @@ Definition prim_STORE := ("STORE"%string, primP STORE). (* RISC-V 32M Multiply instructions (operators). *) Definition riscv_mul_semi (wn wm: ty_r) : ty_r := (wn * wm)%w. -Definition riscv_MUL_instr : instr_desc_t := RTypeInstruction riscv_mul_semi "MUL" "mul". +Definition riscv_MUL_instr : instr_desc_t := RTypeInstruction riscv_mul_semi "MUL" "mul" DOIT. Definition prim_MUL := ("MUL"%string, primM MUL). Definition riscv_mulh_semi (wn wm: ty_r) : ty_r := wmulhs wn wm. -Definition riscv_MULH_instr : instr_desc_t := RTypeInstruction riscv_mulh_semi "MULH" "mulh". +Definition riscv_MULH_instr : instr_desc_t := RTypeInstruction riscv_mulh_semi "MULH" "mulh" DOIT. Definition prim_MULH := ("MULH"%string, primM MULH). Definition riscv_mulhu_semi (wn wm: ty_r) : ty_r := wmulhu wn wm. -Definition riscv_MULHU_instr : instr_desc_t := RTypeInstruction riscv_mulhu_semi "MULHU" "mulhu". +Definition riscv_MULHU_instr : instr_desc_t := RTypeInstruction riscv_mulhu_semi "MULHU" "mulhu" DOIT. Definition prim_MULHU := ("MULHU"%string, primM MULHU). Definition riscv_mulhsu_semi (wn wm: ty_r) : ty_r := wmulhsu wn wm. -Definition riscv_MULHSU_instr : instr_desc_t := RTypeInstruction riscv_mulhsu_semi "MULHSU" "mulhsu". +Definition riscv_MULHSU_instr : instr_desc_t := RTypeInstruction riscv_mulhsu_semi "MULHSU" "mulhsu" DOIT. Definition prim_MULHSU := ("MULHSU"%string, primM MULHSU). @@ -520,21 +570,21 @@ Definition prim_MULHSU := ("MULHSU"%string, primM MULHSU). (* Division by zero is specified, it must return all bits set *) Definition riscv_div_semi (wn wm: ty_r) : ty_r := if wm == 0%w then (-1%w)%w else wdivi wn wm. -Definition riscv_DIV_instr : instr_desc_t := RTypeInstruction riscv_div_semi "DIV" "div". +Definition riscv_DIV_instr : instr_desc_t := RTypeInstruction riscv_div_semi "DIV" "div" NOT_DOIT. (* Not in Zkt *) Definition prim_DIV := ("DIV"%string, primM DIV). (* Division by zero is specified, it must return all bits set *) Definition riscv_divu_semi (wn wm: ty_r) : ty_r := if wm == 0%w then (-1%w)%w else wdiv wn wm. -Definition riscv_DIVU_instr : instr_desc_t := RTypeInstruction riscv_divu_semi "DIVU" "divu". +Definition riscv_DIVU_instr : instr_desc_t := RTypeInstruction riscv_divu_semi "DIVU" "divu" NOT_DOIT. (* Not in Zkt *) Definition prim_DIVU := ("DIVU"%string, primM DIVU). Definition riscv_rem_semi (wn wm: ty_r) : ty_r := wmodi wn wm. -Definition riscv_REM_instr : instr_desc_t := RTypeInstruction riscv_rem_semi "REM" "rem". +Definition riscv_REM_instr : instr_desc_t := RTypeInstruction riscv_rem_semi "REM" "rem" NOT_DOIT. (* Not in Zkt *) Definition prim_REM := ("REM"%string, primM REM). Definition riscv_remu_semi (wn wm: ty_r) : ty_r := wmod wn wm. -Definition riscv_REMU_instr : instr_desc_t := RTypeInstruction riscv_remu_semi "REMU" "remu". +Definition riscv_REMU_instr : instr_desc_t := RTypeInstruction riscv_remu_semi "REMU" "remu" NOT_DOIT. (* Not in Zkt *) Definition prim_REMU := ("REMU"%string, primM REMU).