Skip to content

Commit 63ad6f9

Browse files
kunxian-xiaAurélien Nicolasnaurehero78119
authored
WIP: integration test (#368)
This PR aims to add an integration test in which we proves the `fibonacci` rust program. The goal will be achieved by two steps: 1. We will only prove the fibonacci ELF compiled by SP1 rust toolchain in the first place; 2. We will prove the fibonacci rust guest program once our toolchain is ready. This PR currently builds on top of the changes to `ceno_emul` in #487. _naure:_ **Summary of changes** - The new example program from sp1 is similar to the existing example except: - This uses a fixed set of memory addresses: the data segments from the ELF and the stack. - This accepts ECALLs as NOPs. - Move the circuits for memory initialization into their own module called `MmuConfig` (Memory Management Unit). Meanwhile, `Rv32imConfig` focuses on instruction circuits. - Make assignment in memory circuits (`NonVolatileRamCircuit`) more flexible. - Simplify the assign functions. - Move the flexibility of memory initialization to a dedicated type `MemPadder`. - Pad with valid addresses and zero values. - Do _not_ assume that the table covers the whole range of valid addresses. Instead, it is only as large as necessary which is much smaller. - Removed the notion of _program data_ out of circuits and generalize it as _static memory_. That is memory with a static set of addresses. - Refactor `SetTableSpec` to reflect that the address parameters are not relevant in the case `FixedAddr`. - Fix missing padding of the program table witness. - Various debug logs and assertions. --------- Co-authored-by: Aurélien Nicolas <[email protected]> Co-authored-by: naure <[email protected]> Co-authored-by: Ming <[email protected]>
1 parent 2d02e9a commit 63ad6f9

26 files changed

+889
-351
lines changed

.github/workflows/integration.yml

+7-1
Original file line numberDiff line numberDiff line change
@@ -56,4 +56,10 @@ jobs:
5656
- name: Run example
5757
env:
5858
RAYON_NUM_THREADS: 2
59-
run: cargo run --package ceno_zkvm --example riscv_opcodes --target ${{ matrix.target }} -- --start 10 --end 11
59+
run: cargo run --release --package ceno_zkvm --example riscv_opcodes --target ${{ matrix.target }} -- --start 10 --end 11
60+
61+
- name: Run fibonacci
62+
env:
63+
RAYON_NUM_THREADS: 8
64+
RUST_LOG: debug
65+
run: cargo run --release --package ceno_zkvm --example fibonacci_elf --target ${{ matrix.target }} --

Cargo.lock

+14
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

+2
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,8 @@ crossbeam-channel = "0.5"
2626
ff = "0.13"
2727
goldilocks = { git = "https://github.com/scroll-tech/ceno-Goldilocks" }
2828
itertools = "0.13"
29+
num-derive = "0.4"
30+
num-traits = "0.2"
2931
paste = "1"
3032
plonky2 = "0.2"
3133
poseidon = { path = "./poseidon" }

ceno_emul/Cargo.toml

+2
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ version.workspace = true
77
[dependencies]
88
anyhow = { version = "1.0", default-features = false }
99
elf = "0.7"
10+
num-derive.workspace = true
11+
num-traits.workspace = true
1012
strum.workspace = true
1113
strum_macros.workspace = true
1214
tracing.workspace = true

ceno_emul/src/elf.rs

+8-8
Original file line numberDiff line numberDiff line change
@@ -89,13 +89,6 @@ impl Program {
8989
.filter(|x| x.p_type == elf::abi::PT_LOAD)
9090
.enumerate()
9191
{
92-
tracing::debug!(
93-
"loadable segement {}: PF_R={}, PF_W={}, PF_X={}",
94-
idx,
95-
segment.p_flags & PF_R != 0,
96-
segment.p_flags & PF_W != 0,
97-
segment.p_flags & PF_X != 0,
98-
);
9992
let file_size: u32 = segment
10093
.p_filesz
10194
.try_into()
@@ -114,7 +107,8 @@ impl Program {
114107
.p_vaddr
115108
.try_into()
116109
.map_err(|err| anyhow!("vaddr is larger than 32 bits. {err}"))?;
117-
if (segment.p_flags & PF_X) != 0 {
110+
let p_flags = segment.p_flags;
111+
if (p_flags & PF_X) != 0 {
118112
if base_address.is_none() {
119113
base_address = Some(vaddr);
120114
} else {
@@ -124,6 +118,12 @@ impl Program {
124118
if vaddr % WORD_SIZE as u32 != 0 {
125119
bail!("vaddr {vaddr:08x} is unaligned");
126120
}
121+
tracing::debug!(
122+
"ELF segment {idx}: {}{}{} vaddr=0x{vaddr:08x} file_size={file_size} mem_size={mem_size}",
123+
if p_flags & PF_R != 0 { "R" } else { "-" },
124+
if p_flags & PF_W != 0 { "W" } else { "-" },
125+
if p_flags & PF_X != 0 { "X" } else { "-" },
126+
);
127127
let offset: u32 = segment
128128
.p_offset
129129
.try_into()

ceno_emul/src/platform.rs

+1-14
Original file line numberDiff line numberDiff line change
@@ -38,15 +38,6 @@ impl Platform {
3838
(self.rom_start()..=self.rom_end()).contains(&addr)
3939
}
4040

41-
// TODO figure out proper region for program_data
42-
pub const fn program_data_start(&self) -> Addr {
43-
0x3000_0000
44-
}
45-
46-
pub const fn program_data_end(&self) -> Addr {
47-
0x3000_1000 - 1
48-
}
49-
5041
// TODO figure out a proper region for public io
5142
pub const fn public_io_start(&self) -> Addr {
5243
0x3000_1000
@@ -86,10 +77,6 @@ impl Platform {
8677
(self.public_io_start()..=self.public_io_end()).contains(&addr)
8778
}
8879

89-
pub fn is_program_data(&self, addr: Addr) -> bool {
90-
(self.program_data_start()..=self.program_data_end()).contains(&addr)
91-
}
92-
9380
/// Virtual address of a register.
9481
pub const fn register_vma(&self, index: RegIdx) -> Addr {
9582
// Register VMAs are aligned, cannot be confused with indices, and readable in hex.
@@ -110,7 +97,7 @@ impl Platform {
11097
// Permissions.
11198

11299
pub fn can_read(&self, addr: Addr) -> bool {
113-
self.is_rom(addr) || self.is_ram(addr) || self.is_pub_io(addr) || self.is_program_data(addr)
100+
self.is_rom(addr) || self.is_ram(addr) || self.is_pub_io(addr)
114101
}
115102

116103
pub fn can_write(&self, addr: Addr) -> bool {

ceno_emul/src/rv32im.rs

+2-1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
// limitations under the License.
1616

1717
use anyhow::{Result, anyhow};
18+
use num_derive::ToPrimitive;
1819
use std::sync::OnceLock;
1920
use strum_macros::EnumIter;
2021

@@ -132,7 +133,7 @@ pub enum InsnFormat {
132133
}
133134
use InsnFormat::*;
134135

135-
#[derive(Clone, Copy, Debug, PartialEq, EnumIter)]
136+
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, EnumIter, ToPrimitive)]
136137
#[allow(clippy::upper_case_acronyms)]
137138
pub enum InsnKind {
138139
INVALID,

ceno_emul/src/vm_state.rs

+5-10
Original file line numberDiff line numberDiff line change
@@ -53,16 +53,7 @@ impl VMState {
5353

5454
pub fn new_from_elf(platform: Platform, elf: &[u8]) -> Result<Self> {
5555
let program = Program::load_elf(elf, u32::MAX)?;
56-
let state = Self::new(platform, program);
57-
58-
if state.program.base_address != state.platform.rom_start() {
59-
return Err(anyhow!(
60-
"Invalid base_address {:x}",
61-
state.program.base_address
62-
));
63-
}
64-
65-
Ok(state)
56+
Ok(Self::new(platform, program))
6657
}
6758

6859
pub fn halted(&self) -> bool {
@@ -73,6 +64,10 @@ impl VMState {
7364
&self.tracer
7465
}
7566

67+
pub fn platform(&self) -> &Platform {
68+
&self.platform
69+
}
70+
7671
pub fn program(&self) -> &Program {
7772
self.program.deref()
7873
}

ceno_zkvm/Cargo.toml

+1
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ sumcheck = { version = "0", path = "../sumcheck" }
2222
transcript = { path = "../transcript" }
2323

2424
itertools.workspace = true
25+
num-traits.workspace = true
2526
paste.workspace = true
2627
prettytable-rs.workspace = true
2728
strum.workspace = true

ceno_zkvm/examples/fibonacci.elf

78.9 KB
Binary file not shown.

0 commit comments

Comments
 (0)