From 67fa68230dfda9de47c40f1b0f7b97c55d51a6db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=B4me=20LE=20BRETON?= Date: Wed, 26 Aug 2026 16:16:53 +0200 Subject: [PATCH] riscv: DIV, DIVU, REM and REMU are neither constant-time nor DOIT They have data-dependent latency on typical implementations and are deliberately excluded from the Zkt ("Data-Independent Execution Latency Subset") safe list of the RISC-V specification, which is the reference for data operand independent timing on this architecture. The DOIT classification of every RISC-V instruction is now written explicitly in the instruction descriptors and documented against the Zkt list. Loads and stores, which Zkt does not cover, keep the same assumption as on the other architectures: the address is leaked, and the latency is assumed not to depend on the transferred values. Pseudo-instructions are classified according to their canonical expansions. Zkt exempts HINT encodings (rd = x0) from the latency requirement, but Jasmin cannot emit them: x0 is not part of the declared register file. Fixes #1013 --- changes/02-bugfix/1544-riscv-ct-doit.md | 7 ++ compiler/CCT/fail/doit/riscv/div.jazz | 11 ++ compiler/CCT/fail/doit/riscv/mod.jazz | 11 ++ compiler/CCT/fail/riscv/div_secret.jazz | 10 ++ compiler/CCT/fail/riscv/rem_secret.jazz | 10 ++ compiler/CCT/success/doit/riscv/arith.jazz | 15 +++ compiler/CCT/success/riscv/div_public.jazz | 14 +++ compiler/Makefile | 2 +- compiler/config/tests.config | 15 ++- compiler/src/riscv_arch_full.ml | 10 +- docs/source/tools/ct.md | 6 +- proofs/compiler/riscv_instr_decl.v | 126 ++++++++++++++------- 12 files changed, 195 insertions(+), 42 deletions(-) create mode 100644 changes/02-bugfix/1544-riscv-ct-doit.md create mode 100644 compiler/CCT/fail/doit/riscv/div.jazz create mode 100644 compiler/CCT/fail/doit/riscv/mod.jazz create mode 100644 compiler/CCT/fail/riscv/div_secret.jazz create mode 100644 compiler/CCT/fail/riscv/rem_secret.jazz create mode 100644 compiler/CCT/success/doit/riscv/arith.jazz create mode 100644 compiler/CCT/success/riscv/div_public.jazz 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).