Skip to content

Commit dc9b8ae

Browse files
yi-sunyi-sun
authored
fix: remove incorrect nop transpilation for intrinsics (#1306)
* fix: remove incorrect nop transpilation for intrinsics * feat: document that iseqmod is a no-op if rd = x0 * feat: specify validity for setup_iseq
1 parent a7fc816 commit dc9b8ae

File tree

9 files changed

+139
-36
lines changed

9 files changed

+139
-36
lines changed

‎crates/toolchain/transpiler/src/util.rs‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,12 @@ pub fn from_r_type<F: PrimeField32>(
1919
opcode: usize,
2020
e_as: usize,
2121
dec_insn: &RType,
22+
allow_rd_zero: bool,
2223
) -> Instruction<F> {
23-
if dec_insn.rd == 0 {
24+
// If `rd` is not allowed to be zero, we transpile to `NOP` to prevent a write
25+
// to `x0`. In the cases where `allow_rd_zero` is true, it is the responsibility of
26+
// the caller to guarantee that the resulting instruction does not write to `rd`.
27+
if !allow_rd_zero && dec_insn.rd == 0 {
2428
return nop();
2529
}
2630
Instruction::new(

‎docs/specs/RISCV.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -89,8 +89,8 @@ We use `config.mod_idx(N)` to denote the index of `N` in this list. In the list
8989
| submod\<N\> | R | 0101011 | 000 | `idx*8+1` | `[rd: N::NUM_LIMBS]_2 = [rs1: N::NUM_LIMBS]_2 - [rs2: N::NUM_LIMBS]_2 (mod N)` |
9090
| mulmod\<N\> | R | 0101011 | 000 | `idx*8+2` | `[rd: N::NUM_LIMBS]_2 = [rs1: N::NUM_LIMBS]_2 * [rs2: N::NUM_LIMBS]_2 (mod N)` |
9191
| divmod\<N\> | R | 0101011 | 000 | `idx*8+3` | `[rd: N::NUM_LIMBS]_2 = [rs1: N::NUM_LIMBS]_2 / [rs2: N::NUM_LIMBS]_2 (mod N)` (undefined when `gcd([rs2: N::NUM_LIMBS]_2, N) != 1`) |
92-
| iseqmod\<N\> | R | 0101011 | 000 | `idx*8+4` | `rd = [rs1: N::NUM_LIMBS]_2 == [rs2: N::NUM_LIMBS]_2 (mod N) ? 1 : 0`. Enforces that `[rs1: N::NUM_LIMBS]_2` and `[rs2: N::NUM_LIMBS]_2` are both less than `N` and then sets `rd` equal to boolean comparison value. |
93-
| setup\<N\> | R | 0101011 | 000 | `idx*8+5` | `assert([rs1: N::NUM_LIMBS]_2 == N)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes something (can be anything) into `[rd: N::NUM_LIMBS]_2` if `ind(rs2) = 0,1` (for add_sub, mul_div) or it overwrites the register value of `rd` if `ind(rs2) = 2` (for iseq). |
92+
| iseqmod\<N\> | R | 0101011 | 000 | `idx*8+4` | `rd = [rs1: N::NUM_LIMBS]_2 == [rs2: N::NUM_LIMBS]_2 (mod N) ? 1 : 0`. If `rd != x0`, enforces that `[rs1: N::NUM_LIMBS]_2` and `[rs2: N::NUM_LIMBS]_2` are both less than `N` and then sets `rd` equal to boolean comparison value. If `rd = x0`, this is a no-op. |
93+
| setup\<N\> | R | 0101011 | 000 | `idx*8+5` | `assert([rs1: N::NUM_LIMBS]_2 == N)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes an unconstrained value into `[rd: N::NUM_LIMBS]_2` if `ind(rs2) = 0,1` (for add_sub, mul_div) or it overwrites the register value of `rd` with an unconstrained value if `ind(rs2) = 2` (for iseq). If `ind(rs2) = 2`, then the instruction is **invalid** if `rd = x0`. |
9494

9595
Since `funct7` is 7-bits, up to 16 moduli can be supported simultaneously. We use `idx*8` to leave some room for future expansion.
9696

@@ -104,7 +104,7 @@ Complex extension field arithmetic over `Fp2` depends on `Fp` where `-1` is not
104104
| subcomplex | R | 0101011 | 010 | `idx*8+1` | Read `x: Fp2` from `[rs1..]_2` and `y: Fp2` from `[rs2..]_2`. Write `x - y` to `[rd..]_2` |
105105
| mulcomplex | R | 0101011 | 010 | `idx*8+2` | Read `x: Fp2` from `[rs1..]_2` and `y: Fp2` from `[rs2..]_2`. Write `x * y` to `[rd..]_2` |
106106
| divcomplex | R | 0101011 | 010 | `idx*8+3` | Read `x: Fp2` from `[rs1..]_2` and `y: Fp2` from `[rs2..]_2`. Write `x / y` to `[rd..]_2` |
107-
| setupcomplex| R | 0101011 | 010 | `idx*8+4` | `assert([rs1: Fp::NUM_LIMBS]_2 == Fp::MODULUS)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes something (can be anything) into `[rd: Fp::NUM_LIMBS]_2`. |
107+
| setupcomplex| R | 0101011 | 010 | `idx*8+4` | `assert([rs1: Fp::NUM_LIMBS]_2 == Fp::MODULUS)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes an unconstrained value into `[rd: Fp::NUM_LIMBS]_2`. |
108108

109109
## Elliptic Curve Extension
110110

@@ -114,7 +114,7 @@ The elliptic curve extension supports arithmetic over short Weierstrass curves,
114114
| --------------- | --- | ----------- | ------ | --------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
115115
| sw_add_ne\<C\> | R | 0101011 | 001 | `idx*8` | `EcPoint([rd:2*C::COORD_SIZE]_2) = EcPoint([rs1:2*C::COORD_SIZE]_2) + EcPoint([rs2:2*C::COORD_SIZE]_2)`. Assumes that input affine points are not identity and do not have same x-coordinate. |
116116
| sw_double\<C\> | R | 0101011 | 001 | `idx*8+1` | `EcPoint([rd:2*C::COORD_SIZE]_2) = 2 * EcPoint([rs1:2*C::COORD_SIZE]_2)`. Assumes that input affine point is not identity. `rs2` is unused and must be set to `x0`. |
117-
| setup\<C\> | R | 0101011 | 001 | `idx*8+2` | `assert([rs1: C::COORD_SIZE]_2 == C::MODULUS)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes something (can be anything) into `[rd: 2*C::COORD_SIZE]_2`. If `ind(rs2) != 0`, then this instruction is setup for `sw_add_ne`. Otherwise it is setup for `sw_double`. When `ind(rs2) != 0` (add_ne), it is required for proper functionality that `[rs2: C::COORD_SIZE]_2 != [rs1: C::COORD_SIZE]_2`; otherwise (double), it is required that `[rs1 + C::COORD_SIZE: C::COORD_SIZE]_2 != C::Fp::ZERO` |
117+
| setup\<C\> | R | 0101011 | 001 | `idx*8+2` | `assert([rs1: C::COORD_SIZE]_2 == C::MODULUS)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes an unconstrained value into `[rd: 2*C::COORD_SIZE]_2`. If `ind(rs2) != 0`, then this instruction is setup for `sw_add_ne`. Otherwise it is setup for `sw_double`. When `ind(rs2) != 0` (add_ne), it is required for proper functionality that `[rs2: C::COORD_SIZE]_2 != [rs1: C::COORD_SIZE]_2`; otherwise (double), it is required that `[rs1 + C::COORD_SIZE: C::COORD_SIZE]_2 != C::Fp::ZERO` |
118118
| hint_decompress | R | 0101011 | 001 | `idx*8+3` | Read `x: C::Fp` from `[rs1: C::COORD_SIZE]_2` and `rec_id: u8` from `[rs2]_2`. Reset the hint stream to equal the unique `y: C::Fp` such that `(x, y)` is a point on `C` and `y` has the same parity as `rec_id`, if it exists. Otherwise reset hint stream to arbitrary `C::Fp`. `rd` should be `x0`. |
119119

120120
Since `funct7` is 7-bits, up to 16 curves can be supported simultaneously. We use `idx*8` to leave some room for future expansion.

‎extensions/algebra/transpiler/src/lib.rs‎

Lines changed: 22 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -84,16 +84,22 @@ impl<F: PrimeField32> TranspilerExtension<F> for ModularTranspilerExtension {
8484
2 => Rv32ModularArithmeticOpcode::SETUP_ISEQ,
8585
_ => panic!("invalid opcode"),
8686
};
87-
Some(Instruction::new(
88-
VmOpcode::from_usize(local_opcode.global_opcode().as_usize() + mod_idx_shift),
89-
F::from_canonical_usize(RV32_REGISTER_NUM_LIMBS * dec_insn.rd),
90-
F::from_canonical_usize(RV32_REGISTER_NUM_LIMBS * dec_insn.rs1),
91-
F::ZERO, // rs2 = 0
92-
F::ONE, // d_as = 1
93-
F::TWO, // e_as = 2
94-
F::ZERO,
95-
F::ZERO,
96-
))
87+
if local_opcode == Rv32ModularArithmeticOpcode::SETUP_ISEQ && dec_insn.rd == 0 {
88+
panic!("SETUP_ISEQ is not valid for rd = x0");
89+
} else {
90+
Some(Instruction::new(
91+
VmOpcode::from_usize(
92+
local_opcode.global_opcode().as_usize() + mod_idx_shift,
93+
),
94+
F::from_canonical_usize(RV32_REGISTER_NUM_LIMBS * dec_insn.rd),
95+
F::from_canonical_usize(RV32_REGISTER_NUM_LIMBS * dec_insn.rs1),
96+
F::ZERO, // rs2 = 0
97+
F::ONE, // d_as = 1
98+
F::TWO, // e_as = 2
99+
F::ZERO,
100+
F::ZERO,
101+
))
102+
}
97103
} else {
98104
let global_opcode = match ModArithBaseFunct7::from_repr(base_funct7) {
99105
Some(ModArithBaseFunct7::AddMod) => {
@@ -119,7 +125,11 @@ impl<F: PrimeField32> TranspilerExtension<F> for ModularTranspilerExtension {
119125
_ => unimplemented!(),
120126
};
121127
let global_opcode = global_opcode + mod_idx_shift;
122-
Some(from_r_type(global_opcode, 2, &dec_insn))
128+
// The only opcode in this extension which can write to rd is `IsEqMod`
129+
// so we cannot allow rd to be zero in this case.
130+
let allow_rd_zero =
131+
ModArithBaseFunct7::from_repr(base_funct7) != Some(ModArithBaseFunct7::IsEqMod);
132+
Some(from_r_type(global_opcode, 2, &dec_insn, allow_rd_zero))
123133
}
124134
};
125135
instruction.map(TranspilerOutput::one_to_one)
@@ -189,7 +199,7 @@ impl<F: PrimeField32> TranspilerExtension<F> for Fp2TranspilerExtension {
189199
_ => unimplemented!(),
190200
};
191201
let global_opcode = global_opcode + complex_idx_shift;
192-
Some(from_r_type(global_opcode, 2, &dec_insn))
202+
Some(from_r_type(global_opcode, 2, &dec_insn, true))
193203
}
194204
};
195205
instruction.map(TranspilerOutput::one_to_one)

‎extensions/bigint/transpiler/src/lib.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ impl<F: PrimeField32> TranspilerExtension<F> for Int256TranspilerExtension {
134134
}
135135
_ => unimplemented!(),
136136
};
137-
Some(from_r_type(global_opcode, 2, &dec_insn))
137+
Some(from_r_type(global_opcode, 2, &dec_insn, true))
138138
}
139139
BEQ256_FUNCT3 => {
140140
let dec_insn = BType::new(instruction_u32);

‎extensions/ecc/transpiler/src/lib.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ impl<F: PrimeField32> TranspilerExtension<F> for EccTranspilerExtension {
9595
_ => unimplemented!(),
9696
};
9797
let global_opcode = global_opcode + curve_idx_shift;
98-
Some(from_r_type(global_opcode, 2, &dec_insn))
98+
Some(from_r_type(global_opcode, 2, &dec_insn, true))
9999
}
100100
};
101101
instruction.map(TranspilerOutput::one_to_one)

‎extensions/keccak256/transpiler/src/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ impl<F: PrimeField32> TranspilerExtension<F> for Keccak256TranspilerExtension {
3838
Rv32KeccakOpcode::KECCAK256.global_opcode().as_usize(),
3939
2,
4040
&dec_insn,
41+
true,
4142
);
4243
Some(TranspilerOutput::one_to_one(instruction))
4344
}

‎extensions/pairing/transpiler/src/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,7 @@ impl<F: PrimeField32> TranspilerExtension<F> for PairingTranspilerExtension {
146146
global_opcode,
147147
2,
148148
&dec_insn,
149+
true,
149150
)))
150151
}
151152
}

‎extensions/rv32im/transpiler/src/rrs.rs‎

Lines changed: 103 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -24,67 +24,112 @@ impl<F: PrimeField32> InstructionProcessor for InstructionTranspiler<F> {
2424
type InstructionResult = Instruction<F>;
2525

2626
fn process_add(&mut self, dec_insn: RType) -> Self::InstructionResult {
27-
from_r_type(BaseAluOpcode::ADD.global_opcode().as_usize(), 1, &dec_insn)
27+
from_r_type(
28+
BaseAluOpcode::ADD.global_opcode().as_usize(),
29+
1,
30+
&dec_insn,
31+
false,
32+
)
2833
}
2934

3035
fn process_addi(&mut self, dec_insn: IType) -> Self::InstructionResult {
3136
from_i_type(BaseAluOpcode::ADD.global_opcode().as_usize(), &dec_insn)
3237
}
3338

3439
fn process_sub(&mut self, dec_insn: RType) -> Self::InstructionResult {
35-
from_r_type(BaseAluOpcode::SUB.global_opcode().as_usize(), 1, &dec_insn)
40+
from_r_type(
41+
BaseAluOpcode::SUB.global_opcode().as_usize(),
42+
1,
43+
&dec_insn,
44+
false,
45+
)
3646
}
3747

3848
fn process_xor(&mut self, dec_insn: RType) -> Self::InstructionResult {
39-
from_r_type(BaseAluOpcode::XOR.global_opcode().as_usize(), 1, &dec_insn)
49+
from_r_type(
50+
BaseAluOpcode::XOR.global_opcode().as_usize(),
51+
1,
52+
&dec_insn,
53+
false,
54+
)
4055
}
4156

4257
fn process_xori(&mut self, dec_insn: IType) -> Self::InstructionResult {
4358
from_i_type(BaseAluOpcode::XOR.global_opcode().as_usize(), &dec_insn)
4459
}
4560

4661
fn process_or(&mut self, dec_insn: RType) -> Self::InstructionResult {
47-
from_r_type(BaseAluOpcode::OR.global_opcode().as_usize(), 1, &dec_insn)
62+
from_r_type(
63+
BaseAluOpcode::OR.global_opcode().as_usize(),
64+
1,
65+
&dec_insn,
66+
false,
67+
)
4868
}
4969

5070
fn process_ori(&mut self, dec_insn: IType) -> Self::InstructionResult {
5171
from_i_type(BaseAluOpcode::OR.global_opcode().as_usize(), &dec_insn)
5272
}
5373

5474
fn process_and(&mut self, dec_insn: RType) -> Self::InstructionResult {
55-
from_r_type(BaseAluOpcode::AND.global_opcode().as_usize(), 1, &dec_insn)
75+
from_r_type(
76+
BaseAluOpcode::AND.global_opcode().as_usize(),
77+
1,
78+
&dec_insn,
79+
false,
80+
)
5681
}
5782

5883
fn process_andi(&mut self, dec_insn: IType) -> Self::InstructionResult {
5984
from_i_type(BaseAluOpcode::AND.global_opcode().as_usize(), &dec_insn)
6085
}
6186

6287
fn process_sll(&mut self, dec_insn: RType) -> Self::InstructionResult {
63-
from_r_type(ShiftOpcode::SLL.global_opcode().as_usize(), 1, &dec_insn)
88+
from_r_type(
89+
ShiftOpcode::SLL.global_opcode().as_usize(),
90+
1,
91+
&dec_insn,
92+
false,
93+
)
6494
}
6595

6696
fn process_slli(&mut self, dec_insn: ITypeShamt) -> Self::InstructionResult {
6797
from_i_type_shamt(ShiftOpcode::SLL.global_opcode().as_usize(), &dec_insn)
6898
}
6999

70100
fn process_srl(&mut self, dec_insn: RType) -> Self::InstructionResult {
71-
from_r_type(ShiftOpcode::SRL.global_opcode().as_usize(), 1, &dec_insn)
101+
from_r_type(
102+
ShiftOpcode::SRL.global_opcode().as_usize(),
103+
1,
104+
&dec_insn,
105+
false,
106+
)
72107
}
73108

74109
fn process_srli(&mut self, dec_insn: ITypeShamt) -> Self::InstructionResult {
75110
from_i_type_shamt(ShiftOpcode::SRL.global_opcode().as_usize(), &dec_insn)
76111
}
77112

78113
fn process_sra(&mut self, dec_insn: RType) -> Self::InstructionResult {
79-
from_r_type(ShiftOpcode::SRA.global_opcode().as_usize(), 1, &dec_insn)
114+
from_r_type(
115+
ShiftOpcode::SRA.global_opcode().as_usize(),
116+
1,
117+
&dec_insn,
118+
false,
119+
)
80120
}
81121

82122
fn process_srai(&mut self, dec_insn: ITypeShamt) -> Self::InstructionResult {
83123
from_i_type_shamt(ShiftOpcode::SRA.global_opcode().as_usize(), &dec_insn)
84124
}
85125

86126
fn process_slt(&mut self, dec_insn: RType) -> Self::InstructionResult {
87-
from_r_type(LessThanOpcode::SLT.global_opcode().as_usize(), 1, &dec_insn)
127+
from_r_type(
128+
LessThanOpcode::SLT.global_opcode().as_usize(),
129+
1,
130+
&dec_insn,
131+
false,
132+
)
88133
}
89134

90135
fn process_slti(&mut self, dec_insn: IType) -> Self::InstructionResult {
@@ -96,6 +141,7 @@ impl<F: PrimeField32> InstructionProcessor for InstructionTranspiler<F> {
96141
LessThanOpcode::SLTU.global_opcode().as_usize(),
97142
1,
98143
&dec_insn,
144+
false,
99145
)
100146
}
101147

@@ -239,35 +285,75 @@ impl<F: PrimeField32> InstructionProcessor for InstructionTranspiler<F> {
239285
}
240286

241287
fn process_mul(&mut self, dec_insn: RType) -> Self::InstructionResult {
242-
from_r_type(MulOpcode::MUL.global_opcode().as_usize(), 0, &dec_insn)
288+
from_r_type(
289+
MulOpcode::MUL.global_opcode().as_usize(),
290+
0,
291+
&dec_insn,
292+
false,
293+
)
243294
}
244295

245296
fn process_mulh(&mut self, dec_insn: RType) -> Self::InstructionResult {
246-
from_r_type(MulHOpcode::MULH.global_opcode().as_usize(), 0, &dec_insn)
297+
from_r_type(
298+
MulHOpcode::MULH.global_opcode().as_usize(),
299+
0,
300+
&dec_insn,
301+
false,
302+
)
247303
}
248304

249305
fn process_mulhu(&mut self, dec_insn: RType) -> Self::InstructionResult {
250-
from_r_type(MulHOpcode::MULHU.global_opcode().as_usize(), 0, &dec_insn)
306+
from_r_type(
307+
MulHOpcode::MULHU.global_opcode().as_usize(),
308+
0,
309+
&dec_insn,
310+
false,
311+
)
251312
}
252313

253314
fn process_mulhsu(&mut self, dec_insn: RType) -> Self::InstructionResult {
254-
from_r_type(MulHOpcode::MULHSU.global_opcode().as_usize(), 0, &dec_insn)
315+
from_r_type(
316+
MulHOpcode::MULHSU.global_opcode().as_usize(),
317+
0,
318+
&dec_insn,
319+
false,
320+
)
255321
}
256322

257323
fn process_div(&mut self, dec_insn: RType) -> Self::InstructionResult {
258-
from_r_type(DivRemOpcode::DIV.global_opcode().as_usize(), 0, &dec_insn)
324+
from_r_type(
325+
DivRemOpcode::DIV.global_opcode().as_usize(),
326+
0,
327+
&dec_insn,
328+
false,
329+
)
259330
}
260331

261332
fn process_divu(&mut self, dec_insn: RType) -> Self::InstructionResult {
262-
from_r_type(DivRemOpcode::DIVU.global_opcode().as_usize(), 0, &dec_insn)
333+
from_r_type(
334+
DivRemOpcode::DIVU.global_opcode().as_usize(),
335+
0,
336+
&dec_insn,
337+
false,
338+
)
263339
}
264340

265341
fn process_rem(&mut self, dec_insn: RType) -> Self::InstructionResult {
266-
from_r_type(DivRemOpcode::REM.global_opcode().as_usize(), 0, &dec_insn)
342+
from_r_type(
343+
DivRemOpcode::REM.global_opcode().as_usize(),
344+
0,
345+
&dec_insn,
346+
false,
347+
)
267348
}
268349

269350
fn process_remu(&mut self, dec_insn: RType) -> Self::InstructionResult {
270-
from_r_type(DivRemOpcode::REMU.global_opcode().as_usize(), 0, &dec_insn)
351+
from_r_type(
352+
DivRemOpcode::REMU.global_opcode().as_usize(),
353+
0,
354+
&dec_insn,
355+
false,
356+
)
271357
}
272358

273359
fn process_fence(&mut self, dec_insn: IType) -> Self::InstructionResult {

‎extensions/sha256/transpiler/src/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ impl<F: PrimeField32> TranspilerExtension<F> for Sha256TranspilerExtension {
3939
Rv32Sha256Opcode::SHA256.global_opcode().as_usize(),
4040
RV32_MEMORY_AS as usize,
4141
&dec_insn,
42+
true,
4243
);
4344
Some(TranspilerOutput::one_to_one(instruction))
4445
}

0 commit comments

Comments
 (0)