Skip to content

Commit 9839042

Browse files
committed
Add uint256 emulation program
1 parent 47ee66c commit 9839042

File tree

10 files changed

+520
-3
lines changed

10 files changed

+520
-3
lines changed

Cargo.lock

Lines changed: 3 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

ceno_emul/Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,16 +17,19 @@ elf = "0.7"
1717
ff_ext.workspace = true
1818
itertools.workspace = true
1919
multilinear_extensions.workspace = true
20+
num.workspace = true
2021
num-derive.workspace = true
2122
num-traits.workspace = true
2223
rrs_lib = { package = "rrs-succinct", version = "0.1.0" }
2324
secp.workspace = true
2425
serde.workspace = true
26+
sp1-curves.workspace = true
2527
strum.workspace = true
2628
strum_macros.workspace = true
2729
substrate-bn.workspace = true
2830
tiny-keccak.workspace = true
2931
tracing.workspace = true
32+
typenum = "1.19.0"
3033

3134
[features]
3235
default = ["forbid_overflow"]

ceno_emul/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ pub use syscalls::{
3838
Secp256k1DecompressSpec, Secp256k1DoubleSpec,
3939
},
4040
sha256::{SHA_EXTEND_WORDS, Sha256ExtendSpec},
41+
uint256::UINT256_WORDS_FIELD_ELEMENT,
4142
};
4243

4344
pub mod utils;

ceno_emul/src/syscalls.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ pub mod bn254;
55
pub mod keccak_permute;
66
pub mod secp256k1;
77
pub mod sha256;
8+
pub mod uint256;
89

910
// Using the same function codes as sp1:
1011
// https://github.com/succinctlabs/sp1/blob/013c24ea2fa15a0e7ed94f7d11a7ada4baa39ab9/crates/core/executor/src/syscalls/code.rs
@@ -13,7 +14,7 @@ pub use ceno_syscall::{
1314
BLS12381_ADD, BLS12381_DECOMPRESS, BLS12381_DOUBLE, BN254_ADD, BN254_DOUBLE, BN254_FP_ADD,
1415
BN254_FP_MUL, BN254_FP2_ADD, BN254_FP2_MUL, KECCAK_PERMUTE, SECP256K1_ADD,
1516
SECP256K1_DECOMPRESS, SECP256K1_DOUBLE, SECP256R1_ADD, SECP256R1_DECOMPRESS, SECP256R1_DOUBLE,
16-
SHA_EXTEND,
17+
SHA_EXTEND, UINT256_MUL,
1718
};
1819

1920
pub trait SyscallSpec {
@@ -42,6 +43,7 @@ pub fn handle_syscall(vm: &VMState, function_code: u32) -> Result<SyscallEffects
4243
BN254_FP_MUL => Ok(bn254::bn254_fp_mul(vm)),
4344
BN254_FP2_ADD => Ok(bn254::bn254_fp2_add(vm)),
4445
BN254_FP2_MUL => Ok(bn254::bn254_fp2_mul(vm)),
46+
UINT256_MUL => Ok(uint256::uint256_mul(vm)),
4547
// TODO: introduce error types.
4648
_ => Err(anyhow::anyhow!("Unknown syscall: {}", function_code)),
4749
}

ceno_emul/src/syscalls/uint256.rs

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
use crate::{
2+
Change, EmuContext, Platform, SyscallSpec, VMState, Word, WriteOp,
3+
syscalls::{SyscallEffects, SyscallWitness},
4+
utils::MemoryView,
5+
};
6+
7+
use super::UINT256_MUL;
8+
use itertools::Itertools;
9+
use num::{BigUint, One, Zero};
10+
use sp1_curves::{params::NumWords, uint256::U256Field};
11+
use typenum::marker_traits::Unsigned;
12+
13+
type WordsFieldElement = <U256Field as NumWords>::WordsFieldElement;
14+
pub const UINT256_WORDS_FIELD_ELEMENT: usize = WordsFieldElement::USIZE;
15+
const WORD_SIZE: usize = 4;
16+
17+
pub(crate) struct Uint256MulSpec;
18+
19+
impl SyscallSpec for Uint256MulSpec {
20+
const NAME: &'static str = "UINT256_MUL";
21+
22+
const REG_OPS_COUNT: usize = 2;
23+
const MEM_OPS_COUNT: usize = 3 * UINT256_WORDS_FIELD_ELEMENT; // x, y, modulus
24+
const CODE: u32 = ceno_rt::syscalls::UINT256_MUL;
25+
}
26+
27+
pub fn uint256_mul(vm: &VMState) -> SyscallEffects {
28+
let x_ptr = vm.peek_register(Platform::reg_arg0());
29+
let y_ptr = vm.peek_register(Platform::reg_arg1());
30+
let mod_ptr = y_ptr + UINT256_WORDS_FIELD_ELEMENT as u32 * WORD_SIZE as u32;
31+
32+
// Read the argument pointers
33+
let reg_ops = vec![
34+
WriteOp::new_register_op(
35+
Platform::reg_arg0(),
36+
Change::new(x_ptr, x_ptr),
37+
0, // Cycle set later in finalize().
38+
),
39+
WriteOp::new_register_op(
40+
Platform::reg_arg1(),
41+
Change::new(y_ptr, y_ptr),
42+
0, // Cycle set later in finalize().
43+
),
44+
];
45+
46+
// Memory segments of x, y, and modulus
47+
let [mut x_view, y_view, mod_view] =
48+
[x_ptr, y_ptr, mod_ptr].map(|start| MemoryView::<UINT256_WORDS_FIELD_ELEMENT>::new(vm, start));
49+
50+
// Read x and y from words via wrapper type
51+
let [x, y, modulus] = [&x_view, &y_view, &mod_view].map(|view| {
52+
BigUint::from_bytes_le(
53+
&view
54+
.words()
55+
.into_iter()
56+
.flat_map(|w| w.to_le_bytes())
57+
.collect_vec(),
58+
)
59+
});
60+
61+
// Perform the multiplication and take the result modulo the modulus.
62+
let result: BigUint = if modulus.is_zero() {
63+
let modulus = BigUint::one() << 256;
64+
(x * y) % modulus
65+
} else {
66+
(x * y) % modulus
67+
};
68+
let mut result_bytes = result.to_bytes_le();
69+
result_bytes.resize(32, 0u8); // Pad the result to 32 bytes.
70+
71+
// Convert the result to little endian u32 words.
72+
let result: [u32; 8] = {
73+
let mut iter = result_bytes
74+
.chunks_exact(4)
75+
.map(|chunk| u32::from_le_bytes(chunk.try_into().unwrap()));
76+
core::array::from_fn(|_| iter.next().unwrap())
77+
};
78+
x_view.write(result);
79+
80+
let mem_ops = x_view
81+
.mem_ops()
82+
.into_iter()
83+
.chain(y_view.mem_ops())
84+
.chain(mod_view.mem_ops())
85+
.collect_vec();
86+
87+
SyscallEffects {
88+
witness: SyscallWitness::new(mem_ops, reg_ops),
89+
next_pc: None,
90+
}
91+
}

ceno_host/tests/test_elf.rs

Lines changed: 56 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use anyhow::Result;
44
use ceno_emul::{
55
BN254_FP_WORDS, BN254_FP2_WORDS, BN254_POINT_WORDS, CENO_PLATFORM, EmuContext, InsnKind,
66
Platform, Program, SECP256K1_ARG_WORDS, SECP256K1_COORDINATE_WORDS, SHA_EXTEND_WORDS,
7-
StepRecord, VMState, WORD_SIZE, Word, WordAddr, WriteOp,
7+
StepRecord, UINT256_WORDS_FIELD_ELEMENT, VMState, WORD_SIZE, Word, WordAddr, WriteOp,
88
host_utils::{read_all_messages, read_all_messages_as_words},
99
};
1010
use ceno_host::CenoStdin;
@@ -623,6 +623,61 @@ fn test_bn254_precompile() -> Result<()> {
623623
let program_elf = ceno_examples::bn254_precompile;
624624
let mut state = VMState::new_from_elf(unsafe_platform(), program_elf)?;
625625
let _ = run(&mut state)?;
626+
Ok(())
627+
}
628+
629+
fn test_uint256_mul() -> Result<()> {
630+
let mut state = VMState::new_from_elf(unsafe_platform(), program_elf)?;
631+
632+
let steps = run(&mut state)?;
633+
634+
let syscalls = steps.iter().filter_map(|step| step.syscall()).collect_vec();
635+
assert_eq!(syscalls.len(), 1);
636+
637+
let witness = syscalls[0];
638+
assert_eq!(witness.reg_ops.len(), 2);
639+
assert_eq!(witness.reg_ops[0].register_index(), Platform::reg_arg0());
640+
assert_eq!(witness.reg_ops[1].register_index(), Platform::reg_arg1());
641+
642+
let a_address = witness.reg_ops[0].value.after;
643+
assert_eq!(a_address, witness.reg_ops[0].value.before);
644+
let a_address: WordAddr = a_address.into();
645+
646+
let b_address = witness.reg_ops[1].value.after;
647+
assert_eq!(b_address, witness.reg_ops[1].value.before);
648+
let b_address: WordAddr = b_address.into();
649+
650+
const A_MUL_B: [u8; 65] = [
651+
4, 188, 11, 115, 232, 35, 63, 79, 186, 163, 11, 207, 165, 64, 247, 109, 81, 125, 56, 83,
652+
131, 221, 140, 154, 19, 186, 109, 173, 9, 127, 142, 169, 219, 108, 17, 216, 218, 125, 37,
653+
30, 87, 86, 194, 151, 20, 122, 64, 118, 123, 210, 29, 60, 209, 138, 131, 11, 247, 157, 212,
654+
209, 123, 162, 111, 197, 70,
655+
];
656+
let expect = bytes_to_words(A_MUL_B);
657+
658+
assert_eq!(witness.mem_ops.len(), 3 * UINT256_WORDS_FIELD_ELEMENT);
659+
// Expect first half to consist of read/writes on P
660+
for (i, write_op) in witness
661+
.mem_ops
662+
.iter()
663+
.take(UINT256_WORDS_FIELD_ELEMENT)
664+
.enumerate()
665+
{
666+
assert_eq!(write_op.addr, a_address + i);
667+
assert_eq!(write_op.value.after, expect[i]);
668+
}
669+
670+
// Expect second half to consist of reads on Q
671+
for (i, write_op) in witness
672+
.mem_ops
673+
.iter()
674+
.skip(UINT256_WORDS_FIELD_ELEMENT)
675+
.take(UINT256_WORDS_FIELD_ELEMENT * UINT256_WORDS_FIELD_ELEMENT)
676+
.enumerate()
677+
{
678+
assert_eq!(write_op.addr, b_address + i);
679+
assert_eq!(write_op.value.after, write_op.value.before);
680+
}
626681

627682
Ok(())
628683
}

ceno_syscall/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ pub const BLS12381_DOUBLE: u32 = 0x00_00_01_1F;
1818
pub const SECP256R1_ADD: u32 = 0x00_01_01_2C;
1919
pub const SECP256R1_DOUBLE: u32 = 0x00_00_01_2D;
2020
pub const SECP256R1_DECOMPRESS: u32 = 0x00_00_01_2E;
21+
pub const UINT256_MUL: u32 = 0x00_01_01_1D;
2122

2223
pub const KECCAK_STATE_WORDS: usize = 25;
2324

ceno_zkvm/src/instructions/riscv/ecall.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,13 @@ mod keccak;
33
mod weierstrass_add;
44
mod weierstrass_decompress;
55
mod weierstrass_double;
6+
mod uint256;
67

78
pub use keccak::KeccakInstruction;
89
pub use weierstrass_add::WeierstrassAddAssignInstruction;
910
pub use weierstrass_decompress::WeierstrassDecompressInstruction;
1011
pub use weierstrass_double::WeierstrassDoubleAssignInstruction;
12+
pub use uint256::U256MulInstruction;
1113

1214
use ceno_emul::InsnKind;
1315
pub use halt::HaltInstruction;

0 commit comments

Comments
 (0)