Skip to content

Commit bb9870f

Browse files
dreamATDdreamATD
committed
Merge branch 'tianyi/refactor-prover' into tianyi/keccak-opt
2 parents 7de6010 + cb0e275 commit bb9870f

File tree

20 files changed

+209
-116
lines changed

20 files changed

+209
-116
lines changed

‎.github/workflows/integration.yml

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,13 @@ jobs:
4848
key: integration-${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
4949
- uses: dtolnay/rust-toolchain@nightly
5050

51-
- name: Run fibonacci
51+
- name: Run fibonacci (debug)
5252
env:
5353
RUST_LOG: debug
5454
RUSTFLAGS: "-C opt-level=3"
55-
run: cargo run --package ceno_zkvm --bin e2e -- --platform=ceno --hints=10 --public-io=4191 examples/target/riscv32im-ceno-zkvm-elf/release/examples/fibonacci
55+
run: cargo run --package ceno_zkvm --bin e2e -- --platform=ceno --hints=10 --public-io=4191 examples/target/riscv32im-ceno-zkvm-elf/debug/examples/fibonacci
56+
57+
- name: Run fibonacci (release)
58+
env:
59+
RUSTFLAGS: "-C opt-level=3"
60+
run: cargo run --release --package ceno_zkvm --bin e2e -- --platform=ceno --hints=10 --public-io=4191 examples/target/riscv32im-ceno-zkvm-elf/release/examples/fibonacci

‎ceno_emul/src/elf.rs

Lines changed: 69 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,7 @@ impl Program {
104104
if segments.len() > 256 {
105105
bail!("Too many program headers");
106106
}
107+
let symbols = collect_addr_symbols_mapping(&elf)?;
107108
for (idx, segment) in segments
108109
.iter()
109110
.filter(|x| x.p_type == elf::abi::PT_LOAD)
@@ -148,29 +149,48 @@ impl Program {
148149
.p_offset
149150
.try_into()
150151
.map_err(|err| anyhow!("offset is larger than 32 bits. {err}"))?;
151-
for i in (0..mem_size).step_by(WORD_SIZE) {
152+
153+
// process initialized data
154+
(0..file_size).step_by(WORD_SIZE).try_for_each(|i| {
152155
let addr = vaddr.checked_add(i).context("Invalid segment vaddr")?;
153156
if addr >= max_mem {
154-
bail!(
155-
"Address [0x{addr:08x}] exceeds maximum address for guest programs [0x{max_mem:08x}]"
156-
);
157+
bail!("Address [0x{addr:x}] exceeds max [0x{max_mem:x}]");
157158
}
158-
if i >= file_size {
159-
// Past the file size and skip.
160-
} else {
161-
let mut word = 0;
162-
// Don't read past the end of the file.
163-
let len = core::cmp::min(file_size - i, WORD_SIZE as u32);
164-
for j in 0..len {
165-
let offset = (offset + i + j) as usize;
166-
let byte = input.get(offset).context("Invalid segment offset")?;
167-
word |= (*byte as u32) << (j * 8);
168-
}
169-
image.insert(addr, word);
170-
if (segment.p_flags & PF_X) != 0 {
171-
instructions.push(word);
172-
}
159+
160+
let word = (0..WORD_SIZE as u32)
161+
.take((file_size - i) as usize)
162+
.enumerate()
163+
.fold(0u32, |acc, (j, _)| {
164+
let offset = (offset + i + j as u32) as usize;
165+
let byte = *input.get(offset).unwrap_or(&0);
166+
acc | ((byte as u32) << (j * 8))
167+
});
168+
169+
image.insert(addr, word);
170+
if (segment.p_flags & PF_X) != 0 {
171+
instructions.push(word);
173172
}
173+
174+
Ok(())
175+
})?;
176+
177+
// only pad uninitialized region if a symbol exists in the range
178+
if let Some((max_addr, _)) = find_max_symbol_in_range(
179+
&symbols,
180+
vaddr as u64,
181+
vaddr.checked_add(mem_size).context("Invalid mem_size")? as u64,
182+
) {
183+
let zero_upper = (*max_addr as u32).saturating_sub(vaddr);
184+
(file_size..=zero_upper)
185+
.step_by(WORD_SIZE)
186+
.try_for_each(|i| {
187+
let addr = vaddr.checked_add(i).context("Invalid segment vaddr")?;
188+
if addr >= max_mem {
189+
bail!("zero-fill addr [0x{addr:x}] exceeds max [0x{max_mem:x}]");
190+
}
191+
image.insert(addr, 0);
192+
Ok(())
193+
})?;
174194
}
175195
}
176196

@@ -220,17 +240,10 @@ impl Program {
220240
}
221241

222242
// retrieve sheap from elf
223-
let sheap = elf
224-
.symbol_table()?
225-
.and_then(|(symtab, strtab)| {
226-
symtab.iter().find_map(|symbol| {
227-
strtab
228-
.get(symbol.st_name as usize)
229-
.ok()
230-
.filter(|&name| name == "_sheap")
231-
.map(|_| symbol.st_value)
232-
})
233-
})
243+
let sheap = symbols
244+
.iter()
245+
.find(|(_, v)| *v == "_sheap")
246+
.map(|(k, _)| *k)
234247
.ok_or_else(|| anyhow!("unable to find _sheap symbol"))? as u32;
235248

236249
// there should be no
@@ -249,3 +262,29 @@ impl Program {
249262
})
250263
}
251264
}
265+
266+
fn collect_addr_symbols_mapping<'data>(
267+
elf: &ElfBytes<'data, LittleEndian>,
268+
) -> Result<BTreeMap<u64, String>> {
269+
let mut symbols = BTreeMap::new();
270+
271+
if let Some((symtab, strtab)) = elf.symbol_table()? {
272+
for symbol in symtab.iter() {
273+
if let Ok(name) = strtab.get(symbol.st_name as usize) {
274+
if !name.is_empty() && symbol.st_value != 0 {
275+
symbols.insert(symbol.st_value, name.to_string());
276+
}
277+
}
278+
}
279+
}
280+
281+
Ok(symbols)
282+
}
283+
284+
fn find_max_symbol_in_range(
285+
symbols: &BTreeMap<u64, String>,
286+
start: u64,
287+
end: u64,
288+
) -> Option<(&u64, &String)> {
289+
symbols.range(start..end).max_by_key(|(&addr, _)| addr)
290+
}

‎ceno_emul/src/platform.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ pub struct Platform {
1717
pub stack: Range<Addr>,
1818
pub heap: Range<Addr>,
1919
pub hints: Range<Addr>,
20+
2021
/// If true, ecall instructions are no-op instead of trap. Testing only.
2122
pub unsafe_ecall_nop: bool,
2223
}

‎ceno_host/tests/test_elf.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ fn test_hints() -> Result<()> {
127127
for (i, msg) in enumerate(&all_messages) {
128128
println!("{i}: {msg}");
129129
}
130-
assert_eq!(all_messages[0], "3992003");
130+
assert_eq!(all_messages[3], "3992003");
131131
Ok(())
132132
}
133133

‎ceno_rt/ceno_link.x

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11

2-
_stack_start = ORIGIN(REGION_STACK) + LENGTH(REGION_STACK);
2+
_stack_start = ORIGIN(REGION_STACK) + 1024M;
33
_hints_start = ORIGIN(REGION_HINTS);
44
_hints_length = LENGTH(REGION_HINTS);
55
_lengths_of_hints_start = ORIGIN(REGION_HINTS);

‎ceno_rt/memory.x

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
MEMORY
22
{
3-
RAM : ORIGIN = 0x80000000, LENGTH = 1024M
4-
ROM : ORIGIN = 0x20000000, LENGTH = 128M
5-
HINTS : ORIGIN = 0x40000000, LENGTH = 256M
6-
PUBIO : ORIGIN = 0x30000000, LENGTH = 1K
3+
RAM (rw) : ORIGIN = 0x80000000, LENGTH = 0x40040000 /* 1024M heap/stack + 256k reserved for io */
4+
ROM (rx) : ORIGIN = 0x20000000, LENGTH = 128M
5+
HINTS (r) : ORIGIN = 0x40000000, LENGTH = 256M
6+
PUBIO (r) : ORIGIN = 0x30000000, LENGTH = 1K
77
}
88

99
REGION_ALIAS("REGION_TEXT", ROM);

‎ceno_rt/src/io.rs

Lines changed: 22 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,6 @@
1-
use crate::{INFO_OUT_ADDR, WORD_SIZE};
1+
use crate::WORD_SIZE;
22
use core::{cell::Cell, fmt, mem::size_of, slice};
33

4-
static INFO_OUT: IOWriter = IOWriter::new(INFO_OUT_ADDR);
5-
6-
pub fn info_out() -> &'static IOWriter {
7-
&INFO_OUT
8-
}
9-
104
pub struct IOWriter {
115
cursor: Cell<*mut u32>,
126
}
@@ -16,6 +10,7 @@ pub struct IOWriter {
1610
unsafe impl Sync for IOWriter {}
1711

1812
impl IOWriter {
13+
#[cfg(debug_assertions)]
1914
const fn new(addr: u32) -> Self {
2015
assert!(addr % WORD_SIZE as u32 == 0);
2116
IOWriter {
@@ -60,18 +55,34 @@ impl fmt::Write for &IOWriter {
6055
}
6156
}
6257

58+
#[cfg(debug_assertions)]
59+
use crate::INFO_OUT_ADDR;
60+
#[cfg(debug_assertions)]
61+
static INFO_OUT: IOWriter = IOWriter::new(INFO_OUT_ADDR);
62+
63+
#[cfg(debug_assertions)]
64+
pub fn info_out() -> &'static IOWriter {
65+
&INFO_OUT
66+
}
67+
6368
mod macros {
6469
#[macro_export]
65-
macro_rules! print {
70+
macro_rules! debug_print {
6671
($($arg:tt)*) => {
67-
let _ = core::write!($crate::info_out(), $($arg)*);
72+
#[cfg(debug_assertions)]
73+
{
74+
let _ = core::write!($crate::info_out(), $($arg)*);
75+
}
6876
};
6977
}
7078

7179
#[macro_export]
72-
macro_rules! println {
80+
macro_rules! debug_println {
7381
($($arg:tt)*) => {
74-
let _ = core::writeln!($crate::info_out(), $($arg)*);
82+
#[cfg(debug_assertions)]
83+
{
84+
let _ = core::writeln!($crate::info_out(), $($arg)*);
85+
}
7586
};
7687
}
7788
}

‎ceno_rt/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ mod mmio;
1717
pub use mmio::{commit, read, read_slice};
1818

1919
mod io;
20+
#[cfg(debug_assertions)]
2021
pub use io::info_out;
2122

2223
mod params;

‎ceno_rt/src/params.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
pub const WORD_SIZE: usize = 4;
22

3-
// Now it's defined within RAM
4-
// TODO define a specific region for it and avoid mixup with ram to achieve non-uniform design on heap/stack
3+
/// address defined in `memory.x` under RAM section.
54
pub const INFO_OUT_ADDR: u32 = 0xC000_0000;

‎ceno_zkvm/src/e2e.rs

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ use crate::{
1616
};
1717
use ceno_emul::{
1818
ByteAddr, CENO_PLATFORM, EmuContext, InsnKind, IterAddresses, Platform, Program, StepRecord,
19-
Tracer, VMState, WORD_SIZE, WordAddr,
19+
Tracer, VMState, WORD_SIZE, WordAddr, host_utils::read_all_messages,
2020
};
2121
use clap::ValueEnum;
2222
use ff_ext::ExtensionField;
@@ -119,6 +119,17 @@ fn emulate_program(
119119
.collect::<Result<Vec<StepRecord>, _>>()
120120
.expect("vm exec failed");
121121

122+
if cfg!(debug_assertions) {
123+
// show io message if have
124+
let all_messages = &read_all_messages(&vm)
125+
.iter()
126+
.map(|msg| String::from_utf8_lossy(msg).to_string())
127+
.collect::<Vec<String>>();
128+
for msg in all_messages {
129+
tracing::info!("{}", msg);
130+
}
131+
}
132+
122133
// Find the exit code from the HALT step, if halting at all.
123134
let exit_code = all_records
124135
.iter()
@@ -190,6 +201,7 @@ fn emulate_program(
190201
})
191202
.collect_vec();
192203

204+
// Find the final hints IO cycles.
193205
let hints_final = hints_init
194206
.iter()
195207
.map(|rec| MemFinalRecord {
@@ -200,11 +212,11 @@ fn emulate_program(
200212
.collect_vec();
201213

202214
// get stack access by min/max range
203-
let stack_final = if let Some((start, end)) = vm
215+
let stack_final = if let Some((start, _)) = vm
204216
.tracer()
205217
.probe_min_max_address_by_start_addr(ByteAddr::from(platform.stack.start).waddr())
206218
{
207-
(start..end)
219+
(start..ByteAddr::from(platform.stack.end).waddr())
208220
// stack record collect in reverse order
209221
.rev()
210222
.map(|vma| {
@@ -225,6 +237,7 @@ fn emulate_program(
225237
.tracer()
226238
.probe_min_max_address_by_start_addr(ByteAddr::from(platform.heap.start).waddr())
227239
{
240+
assert_eq!(start, ByteAddr::from(platform.heap.start).waddr());
228241
(start..end)
229242
.map(|vma| {
230243
let byte_addr = vma.baddr();
@@ -282,7 +295,14 @@ pub fn setup_platform(
282295
};
283296

284297
let prog_data = program.image.keys().copied().collect::<BTreeSet<_>>();
285-
let stack = preset.stack.end - stack_size..preset.stack.end;
298+
299+
let stack = if cfg!(debug_assertions) {
300+
// reserve some extra space for io
301+
// thus memory consistent check could be satisfied
302+
preset.stack.end - stack_size..(preset.stack.end + 0x4000)
303+
} else {
304+
preset.stack.end - stack_size..preset.stack.end
305+
};
286306

287307
let heap = {
288308
// Detect heap as starting after program data.

‎ceno_zkvm/src/tables/ram/ram_impl.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -408,7 +408,13 @@ impl<DVRAM: DynVolatileRamTable + Send + Sync + Clone> DynVolatileRamTableConfig
408408
.zip(final_mem)
409409
.enumerate()
410410
.for_each(|(i, ((row, structural_row), rec))| {
411-
assert_eq!(rec.addr, DVRAM::addr(&self.params, i));
411+
assert_eq!(
412+
rec.addr,
413+
DVRAM::addr(&self.params, i),
414+
"rec.addr {:x} != expected {:x}",
415+
rec.addr,
416+
DVRAM::addr(&self.params, i),
417+
);
412418

413419
if self.final_v.len() == 1 {
414420
// Assign value directly.

‎examples-builder/build.rs

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -23,21 +23,26 @@ fn build_elfs() {
2323
let _ = remove_file(&dest_path);
2424
let mut dest = File::create(&dest_path).expect("failed to create vars.rs");
2525

26-
// TODO(Matthias): skip building the elfs if we are in clippy or check mode.
27-
// See git history for an attempt to do this.
26+
let is_release = std::env::var("PROFILE").unwrap() == "release";
27+
let mut args = vec!["build", "--examples", "--target-dir", "target"];
28+
if is_release {
29+
args.insert(1, "--release"); // insert --release after "build"
30+
}
31+
2832
let output = Command::new("cargo")
29-
.args(["build", "--release", "--examples", "--target-dir", "target"])
33+
.args(args)
3034
.current_dir("../examples")
3135
.env_clear()
3236
.envs(std::env::vars().filter(|x| !x.0.starts_with("CARGO_")))
3337
.output()
3438
.expect("cargo command failed to run");
39+
3540
if !output.status.success() {
3641
io::stdout().write_all(&output.stdout).unwrap();
3742
io::stderr().write_all(&output.stderr).unwrap();
3843
panic!("cargo build of examples failed.");
3944
}
40-
// Contact Matthias, if your examples get complicated enough to need their own crates, instead of just being one file.
45+
4146
for example in glob("../examples/examples/*.rs")
4247
.unwrap()
4348
.map(Result::unwrap)
@@ -47,14 +52,15 @@ fn build_elfs() {
4752
dest,
4853
r#"#[allow(non_upper_case_globals)]
4954
pub const {example}: &[u8] =
50-
include_bytes!(r"{CARGO_MANIFEST_DIR}/../examples/target/riscv32im-ceno-zkvm-elf/release/examples/{example}");"#
51-
).expect("failed to write vars.rs");
55+
include_bytes!(r"{CARGO_MANIFEST_DIR}/../examples/target/riscv32im-ceno-zkvm-elf/{}/examples/{example}");"#,
56+
std::env::var("PROFILE").unwrap()).expect("failed to write vars.rs");
5257
}
5358
rerun_all_but_target(Path::new("../examples"));
5459
rerun_all_but_target(Path::new("../ceno_rt"));
5560
}
5661

5762
fn main() {
5863
println!("cargo:rerun-if-changed=build.rs");
64+
println!("cargo:rerun-if-env-changed=PROFILE");
5965
build_elfs();
6066
}

0 commit comments

Comments
 (0)