Feat: Implement JAL opcode #305

bgillesp · 2024-10-03T21:26:13Z

Implement a J-type instruction base type and the JAL opcode.

Still requires tests and integration

matthiasgoergens · 2024-10-07T00:11:16Z

ceno_zkvm/examples/riscv_opcodes.rs

-                add_records.push(record.clone());
-            } else if kind == BLTU {
-                bltu_records.push(record.clone());
+            match kind {


Yes, matching is better than chains of if-else.

matthiasgoergens · 2024-10-07T00:12:26Z

ceno_zkvm/examples/riscv_opcodes.rs

    // func7   rs2   rs1   f3  rd    opcode
    0b_0000000_00100_00001_000_00100_0110011, // add x4, x4, x1 <=> addi x4, x4, 1
    0b_0000000_00011_00010_000_00011_0110011, // add x3, x3, x2 <=> addi x3, x3, -1
    0b_1_111111_00011_00000_110_1100_1_1100011, // bltu x0, x3, -8
+    0b_0_0000000010_0_00000000_00001_1101111, // jal x1, 4


Not something introduced in this PR, but:

This style of specifying test data is approximately unreadable. At least for me. I can't (easily) tell whether these binary numbers here make any sense.

We can test the decoding from binary to something symbolic one by one for each instruction, but then when we test multiple instructions together, we should use the symbolic form as an intermediary input.

Great point, and strong agree that we could use a better way to encode this data -- it's challenging both to read and write instructions like this. I propose leaving the formatting as is in this PR, and follow up with at least a small rework to make these values more legible and less error-prone.

Issue to keep track of the improvement: #331

matthiasgoergens · 2024-10-07T00:13:04Z

ceno_zkvm/examples/riscv_opcodes.rs

@@ -118,6 +120,7 @@ fn main() {
    let mut zkvm_fixed_traces = ZKVMFixedTraces::default();
    zkvm_fixed_traces.register_opcode_circuit::<AddInstruction<E>>(&zkvm_cs);
    zkvm_fixed_traces.register_opcode_circuit::<BltuInstruction>(&zkvm_cs);
+    zkvm_fixed_traces.register_opcode_circuit::<JalInstruction<E>>(&zkvm_cs);


Continued: See, we even already have some symbolic form for AddInstruction and JlaInstruction etc, so might as well make use of them.

matthiasgoergens · 2024-10-07T00:14:48Z

ceno_zkvm/src/instructions/riscv/j_insn.rs

+        // Fetch instruction
+        circuit_builder.lk_fetch(&InsnRecord::new(
+            vm_state.pc.expr(),
+            (insn_kind.codes().opcode as usize).into(),


This seems a bit suspicious. Why do we need to cast as usize to just run .into() afterwards? Can't we provide an Into / From from instance that would let us get by without as usize?

Fair point! The into call here relies on the implementation of From<usize> for the Expression type right now, but it looks like it's a little complicated to specify generic behavior over all primitive integer types (as far as I can tell). I'll put an implementation of this into a separate small PR in case folks have opinions on how this should be handled.

See PR: #333

matthiasgoergens · 2024-10-07T00:16:13Z

ceno_zkvm/src/scheme/mock_prover.rs

@@ -76,6 +76,8 @@ pub const MOCK_PROGRAM: &[u32] = &[
    0b_1_111111 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b_111 << 12 | 0b_1100_1 << 7 | 0x63,
    // bge x2, x3, -8
    0b_1_111111 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b_101 << 12 | 0b_1100_1 << 7 | 0x63,
+    // jal x4, 0x10004
+    0b_0_0000000010_0_00010000 << 12 | MOCK_RD << 7 | 0x6f,


As said above, putting binary numbers into the test data here basically impossible to read.

bgillesp · 2024-10-07T23:18:40Z

Note: I realized that there is an issue with the handling of immediates and pc in the JAL opcode in this PR -- representing these as native WitIn values instead of as UInts means that the addition does not wrap properly mod 2^32. The fix is not too bad, and I should be able to push an update tonight or tomorrow morning US time.

Previously JAL addition of pc with immediate used unqualified WitIn objects which would not behave properly in terms of wrapping behavior. UInt addition handles mod 2^32 wrapping directly by using table lookups to verify 16-bit limbs.

bgillesp · 2024-10-08T17:41:08Z

Okay, the most recent commits should fix the issue I mentioned -- PR should be ready again for review.

…ant (#333) Current implementation only provides `From<usize>`, which requires explicit type conversions in various locations. This PR provides support for type conversions for arbitrary primitive integer types, specifically: `u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize` In reference to [this comment](#305 (comment)). --------- Co-authored-by: Bryan Gillespie <[email protected]> Co-authored-by: Ming <[email protected]>

ceno_zkvm/src/instructions/riscv/jump/jal.rs

kunxian-xia

Proposed another approach to use 4 witIns only.

ceno_zkvm/src/instructions/riscv/jump/jal.rs

ceno_zkvm/examples/riscv_opcodes.rs

kunxian-xia · 2024-10-10T10:57:07Z

Note: I realized that there is an issue with the handling of immediates and pc in the JAL opcode in this PR -- representing these as native WitIn values instead of as UInts means that the addition does not wrap properly mod 2^32. The fix is not too bad, and I should be able to push an update tonight or tomorrow morning US time.

The case pc + imm wraps mod 2^32 happens most due to imm is negative signed number. If we encode negative number in prime field then we can avoid this UInt overhead. For example, previously -1 is encoded as 0xffffffff_u32 notation, if we store pc with native witIn and encode -1 as p - 1 then it's easy to see this is equivalent to UInt approach.

bgillesp · 2024-10-10T16:44:39Z

So the question I see here is definitely "is it possible for the JAL pc arithmetic to result in either an underflow or an overflow mod 2^32" -- can we make any explicit assumptions about the range of values for the program counter in our VM? The possible offsets for JAL range between -2^20 and 2^20 - 2, so if we can be sure that pc for an instruction can't be smaller than 2^20 or larger than 2^32 - (2^20 - 2), then there's no issue of mod 2^32 arithmetic.

Digging a little deeper, in ceno_emul/src/platform.rs the spec gives 0x2000_0000 to 0x3000_0000 - 1 for the start and end addresses for the ROM, which would certainly do it -- does anyone know if this program address range is enforced in the program lookup table logic?

bgillesp · 2024-10-10T20:26:58Z

Okay, I revised the implementation to use native WitIns for the pc and immediate values as suggested -- under the assumption that program code lies in the expected address range 0x2000_0000 to 0x3000_000 - 1, I agree that the mod 2^32 pc arithmetic shouldn't be an issue.

naure · 2024-10-11T09:31:00Z

ceno_zkvm/src/instructions/riscv/j_insn.rs

+pub struct JInstructionConfig<E: ExtensionField> {
+    pub vm_state: StateInOut<E>,
+    pub rd: WriteRD<E>,
+    pub imm: WitIn,


Technically the imm witness is redundant since it equals a degree-1 expression (next_pc - pc). You could use the expression directly.

~~Or we can use StateInOut::construct_circuit(circuit_builder, false)?; to initialize vm_state which is more natural.~~

Nice find @naure! We can't use StateInOut::construct_circuit(circuit_builder, false) @kunxian-xia because it imposes the constraint next_pc = pc + 4, but we can put this direct check into the J-type instruction gadget since JAL is the only opcode that uses it. Pushing a commit with this change now.

Nice! This is ready to merge from my side.

Saves 1 WitIn due to not having to represent the immediate value directly.

…pcode

bgillesp changed the base branch from master to bg-refactor-instruction-types October 3, 2024 21:28

bgillesp changed the title ~~[WIP] Feat: JAL~~ [WIP] Feat: Implement JAL opcode Oct 4, 2024

Base automatically changed from bg-refactor-instruction-types to master October 4, 2024 01:56

Initial implementation of J-type instructions and JAL opcode

f8f76ce

Still requires tests and integration

bgillesp force-pushed the feat/jal-opcode branch from b10b9aa to f8f76ce Compare October 4, 2024 17:43

Bryan Gillespie added 3 commits October 5, 2024 15:30

Small fixes to JAL and J-type instructions, add mock prover test

b9c3462

Add test file forgotten in previous commit

6328196

Update names and structure of JAL circuit type definitions

3e1bdbd

bgillesp force-pushed the feat/jal-opcode branch from ddae3bc to 3e1bdbd Compare October 5, 2024 22:11

Bryan Gillespie added 2 commits October 5, 2024 16:15

Incorporate JAL opcode into riscv_opcodes example program

1ab9496

Fix comment in J-type instruction circuit

e785ebf

bgillesp changed the title ~~[WIP] Feat: Implement JAL opcode~~ Feat: Implement JAL opcode Oct 5, 2024

bgillesp marked this pull request as ready for review October 5, 2024 22:24

bgillesp requested a review from naure October 5, 2024 22:24

matthiasgoergens reviewed Oct 7, 2024

View reviewed changes

This was referenced Oct 7, 2024

Improve legibility and methodology for testing opcode circuits #331

Open

Add support for generic integer type conversions to Expression::Constant #333

Merged

kunxian-xia self-requested a review October 8, 2024 06:06

Bryan Gillespie added 2 commits October 8, 2024 11:35

Switch JAL pc representation to UInt

0bbffb8

Previously JAL addition of pc with immediate used unqualified WitIn objects which would not behave properly in terms of wrapping behavior. UInt addition handles mod 2^32 wrapping directly by using table lookups to verify 16-bit limbs.

Remove errant println statements from two opcode tests

2f338d1

Merge branch 'master' into feat/jal-opcode

d9ba48c

hero78119 reviewed Oct 10, 2024

View reviewed changes

ceno_zkvm/src/instructions/riscv/jump/jal.rs Outdated Show resolved Hide resolved

ceno_zkvm/src/instructions/riscv/jump/jal.rs Outdated Show resolved Hide resolved

ceno_zkvm/src/instructions/riscv/jump/jal.rs Outdated Show resolved Hide resolved

kunxian-xia reviewed Oct 10, 2024

View reviewed changes

ceno_zkvm/src/instructions/riscv/jump/jal.rs Outdated Show resolved Hide resolved

ceno_zkvm/examples/riscv_opcodes.rs Outdated Show resolved Hide resolved

ceno_zkvm/examples/riscv_opcodes.rs Outdated Show resolved Hide resolved

kunxian-xia linked an issue Oct 10, 2024 that may be closed by this pull request

jal: Jump and link #124

Closed

kunxian-xia added the opcode circuit label Oct 10, 2024

kunxian-xia assigned bgillesp Oct 10, 2024

Bryan Gillespie added 3 commits October 10, 2024 14:12

Revise JAL circuit gadget to use native WitIns for pc arithmetic

12555fc

Small fix in riscv_opcodes.rs example program prover

b8209a6

Merge branch 'master' into feat/jal-opcode

d2750ec

Bryan Gillespie and others added 2 commits October 10, 2024 14:42

Refactor JAL immediate into J-type instruction gadget

d4734c7

Merge branch 'master' into feat/jal-opcode

639e7c6

naure approved these changes Oct 11, 2024

View reviewed changes

Bryan Gillespie added 2 commits October 11, 2024 07:22

Wire JAL pc and next_pc directly into instruction table lookup

0e5d14b

Saves 1 WitIn due to not having to represent the immediate value directly.

Merge remote-tracking branch 'origin/feat/jal-opcode' into feat/jal-o…

928f40a

…pcode

kunxian-xia merged commit cdb771a into master Oct 11, 2024
6 checks passed

kunxian-xia deleted the feat/jal-opcode branch October 11, 2024 14:50

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: Implement JAL opcode #305

Feat: Implement JAL opcode #305

bgillesp commented Oct 3, 2024

matthiasgoergens Oct 7, 2024

matthiasgoergens Oct 7, 2024

bgillesp Oct 7, 2024

matthiasgoergens Oct 7, 2024

matthiasgoergens Oct 7, 2024

bgillesp Oct 7, 2024

bgillesp Oct 7, 2024

matthiasgoergens Oct 7, 2024

bgillesp commented Oct 7, 2024

bgillesp commented Oct 8, 2024

kunxian-xia left a comment

kunxian-xia commented Oct 10, 2024

bgillesp commented Oct 10, 2024

bgillesp commented Oct 10, 2024

naure Oct 11, 2024

kunxian-xia Oct 11, 2024 •

edited

Loading

bgillesp Oct 11, 2024

naure Oct 11, 2024

Feat: Implement JAL opcode #305

Feat: Implement JAL opcode #305

Conversation

bgillesp commented Oct 3, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bgillesp commented Oct 7, 2024

bgillesp commented Oct 8, 2024

kunxian-xia left a comment

Choose a reason for hiding this comment

kunxian-xia commented Oct 10, 2024

bgillesp commented Oct 10, 2024

bgillesp commented Oct 10, 2024

Choose a reason for hiding this comment

kunxian-xia Oct 11, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kunxian-xia Oct 11, 2024 •

edited

Loading