Skip to content

Commit

Permalink
WIP: integration test (#368)
Browse files Browse the repository at this point in the history
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 <info@nau.re>
Co-authored-by: naure <naure@users.noreply.github.com>
Co-authored-by: Ming <hero78119@gmail.com>
  • Loading branch information
4 people authored Nov 19, 2024
1 parent 2d02e9a commit 63ad6f9
Show file tree
Hide file tree
Showing 26 changed files with 889 additions and 351 deletions.
8 changes: 7 additions & 1 deletion .github/workflows/integration.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,4 +56,10 @@ jobs:
- name: Run example
env:
RAYON_NUM_THREADS: 2
run: cargo run --package ceno_zkvm --example riscv_opcodes --target ${{ matrix.target }} -- --start 10 --end 11
run: cargo run --release --package ceno_zkvm --example riscv_opcodes --target ${{ matrix.target }} -- --start 10 --end 11

- name: Run fibonacci
env:
RAYON_NUM_THREADS: 8
RUST_LOG: debug
run: cargo run --release --package ceno_zkvm --example fibonacci_elf --target ${{ matrix.target }} --
14 changes: 14 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ crossbeam-channel = "0.5"
ff = "0.13"
goldilocks = { git = "https://github.com/scroll-tech/ceno-Goldilocks" }
itertools = "0.13"
num-derive = "0.4"
num-traits = "0.2"
paste = "1"
plonky2 = "0.2"
poseidon = { path = "./poseidon" }
Expand Down
2 changes: 2 additions & 0 deletions ceno_emul/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ version.workspace = true
[dependencies]
anyhow = { version = "1.0", default-features = false }
elf = "0.7"
num-derive.workspace = true
num-traits.workspace = true
strum.workspace = true
strum_macros.workspace = true
tracing.workspace = true
Expand Down
16 changes: 8 additions & 8 deletions ceno_emul/src/elf.rs
Original file line number Diff line number Diff line change
Expand Up @@ -89,13 +89,6 @@ impl Program {
.filter(|x| x.p_type == elf::abi::PT_LOAD)
.enumerate()
{
tracing::debug!(
"loadable segement {}: PF_R={}, PF_W={}, PF_X={}",
idx,
segment.p_flags & PF_R != 0,
segment.p_flags & PF_W != 0,
segment.p_flags & PF_X != 0,
);
let file_size: u32 = segment
.p_filesz
.try_into()
Expand All @@ -114,7 +107,8 @@ impl Program {
.p_vaddr
.try_into()
.map_err(|err| anyhow!("vaddr is larger than 32 bits. {err}"))?;
if (segment.p_flags & PF_X) != 0 {
let p_flags = segment.p_flags;
if (p_flags & PF_X) != 0 {
if base_address.is_none() {
base_address = Some(vaddr);
} else {
Expand All @@ -124,6 +118,12 @@ impl Program {
if vaddr % WORD_SIZE as u32 != 0 {
bail!("vaddr {vaddr:08x} is unaligned");
}
tracing::debug!(
"ELF segment {idx}: {}{}{} vaddr=0x{vaddr:08x} file_size={file_size} mem_size={mem_size}",
if p_flags & PF_R != 0 { "R" } else { "-" },
if p_flags & PF_W != 0 { "W" } else { "-" },
if p_flags & PF_X != 0 { "X" } else { "-" },
);
let offset: u32 = segment
.p_offset
.try_into()
Expand Down
15 changes: 1 addition & 14 deletions ceno_emul/src/platform.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,15 +38,6 @@ impl Platform {
(self.rom_start()..=self.rom_end()).contains(&addr)
}

// TODO figure out proper region for program_data
pub const fn program_data_start(&self) -> Addr {
0x3000_0000
}

pub const fn program_data_end(&self) -> Addr {
0x3000_1000 - 1
}

// TODO figure out a proper region for public io
pub const fn public_io_start(&self) -> Addr {
0x3000_1000
Expand Down Expand Up @@ -86,10 +77,6 @@ impl Platform {
(self.public_io_start()..=self.public_io_end()).contains(&addr)
}

pub fn is_program_data(&self, addr: Addr) -> bool {
(self.program_data_start()..=self.program_data_end()).contains(&addr)
}

/// Virtual address of a register.
pub const fn register_vma(&self, index: RegIdx) -> Addr {
// Register VMAs are aligned, cannot be confused with indices, and readable in hex.
Expand All @@ -110,7 +97,7 @@ impl Platform {
// Permissions.

pub fn can_read(&self, addr: Addr) -> bool {
self.is_rom(addr) || self.is_ram(addr) || self.is_pub_io(addr) || self.is_program_data(addr)
self.is_rom(addr) || self.is_ram(addr) || self.is_pub_io(addr)
}

pub fn can_write(&self, addr: Addr) -> bool {
Expand Down
3 changes: 2 additions & 1 deletion ceno_emul/src/rv32im.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
// limitations under the License.

use anyhow::{Result, anyhow};
use num_derive::ToPrimitive;
use std::sync::OnceLock;
use strum_macros::EnumIter;

Expand Down Expand Up @@ -132,7 +133,7 @@ pub enum InsnFormat {
}
use InsnFormat::*;

#[derive(Clone, Copy, Debug, PartialEq, EnumIter)]
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, EnumIter, ToPrimitive)]
#[allow(clippy::upper_case_acronyms)]
pub enum InsnKind {
INVALID,
Expand Down
15 changes: 5 additions & 10 deletions ceno_emul/src/vm_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,16 +53,7 @@ impl VMState {

pub fn new_from_elf(platform: Platform, elf: &[u8]) -> Result<Self> {
let program = Program::load_elf(elf, u32::MAX)?;
let state = Self::new(platform, program);

if state.program.base_address != state.platform.rom_start() {
return Err(anyhow!(
"Invalid base_address {:x}",
state.program.base_address
));
}

Ok(state)
Ok(Self::new(platform, program))
}

pub fn halted(&self) -> bool {
Expand All @@ -73,6 +64,10 @@ impl VMState {
&self.tracer
}

pub fn platform(&self) -> &Platform {
&self.platform
}

pub fn program(&self) -> &Program {
self.program.deref()
}
Expand Down
1 change: 1 addition & 0 deletions ceno_zkvm/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ sumcheck = { version = "0", path = "../sumcheck" }
transcript = { path = "../transcript" }

itertools.workspace = true
num-traits.workspace = true
paste.workspace = true
prettytable-rs.workspace = true
strum.workspace = true
Expand Down
Binary file added ceno_zkvm/examples/fibonacci.elf
Binary file not shown.
Loading

0 comments on commit 63ad6f9

Please sign in to comment.