Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

WIP: integration test #368

Open
wants to merge 60 commits into
base: master
Choose a base branch
from
Open

WIP: integration test #368

wants to merge 60 commits into from
+749 −261

Conversation

kunxian-xia
Copy link
Collaborator

@kunxian-xia kunxian-xia commented Oct 12, 2024 •
edited
Loading

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.

@kunxian-xia kunxian-xia self-assigned this Oct 12, 2024
@kunxian-xia kunxian-xia linked an issue Oct 12, 2024 that may be closed by this pull request
prove fibonacci program example to improve testing coverage #352
Open
2 tasks
@kunxian-xia kunxian-xia marked this pull request as draft October 12, 2024 16:08
@kunxian-xia kunxian-xia changed the base branch from master to feat/load_mem October 25, 2024 15:14
Base automatically changed from feat/load_mem to master October 28, 2024 11:47
@kunxian-xia kunxian-xia changed the base branch from master to feat/expose_insns_in_emul October 28, 2024 12:29
@kunxian-xia kunxian-xia mentioned this pull request Oct 29, 2024
Merged
Base automatically changed from feat/expose_insns_in_emul to master October 29, 2024 08:53
@kunxian-xia kunxian-xia marked this pull request as ready for review October 29, 2024 17:35
@kunxian-xia
Copy link
Collaborator Author

kunxian-xia commented Oct 29, 2024 •
edited
Loading

We need to resolve #245 to support writes to X0.

naure
naure reviewed Oct 30, 2024
View reviewed changes
ceno_zkvm/src/instructions/riscv/jump/jalr.rs Outdated Show resolved Hide resolved
ceno_zkvm/src/structs.rs Outdated Show resolved Hide resolved
ceno_zkvm/src/scheme/prover.rs Outdated Show resolved Hide resolved
@kunxian-xia kunxian-xia mentioned this pull request Oct 30, 2024
Closed
naure
naure reviewed Oct 30, 2024
View reviewed changes
ceno_emul/src/vm_state.rs Outdated Show resolved Hide resolved
@kunxian-xia kunxian-xia mentioned this pull request Nov 8, 2024
Merged
@kunxian-xia kunxian-xia mentioned this pull request Nov 15, 2024
Closed
@naure
Copy link
Collaborator

naure commented Nov 15, 2024

Summary of changes

  • The example program from sp1. It 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 MMU. Meanwhile, Rv32imConfig focuses on instruction circuits.
  • Fix assignment in memory circuits (NonVolatileRamCircuit) to be more flexible.
    • 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.
  • Refactor SetTableSpec to reflect that the address parameters are not relevant in the case FixedAddr.
  • Various debug logs and assertions.

@naure
Copy link
Collaborator

naure commented Nov 15, 2024

@kunxian-xia Ready for review.

kunxian-xia
kunxian-xia commented Nov 15, 2024
View reviewed changes
ceno_zkvm/src/tables/ram.rs
@@ -62,10 +62,15 @@ pub struct ProgramDataTable;
impl NonVolatileTable for ProgramDataTable {
const RAM_TYPE: RAMType = RAMType::Memory;
const V_LIMBS: usize = 1; // See `MemoryExpr`.
const WRITABLE: bool = false;
const WRITABLE: bool = true;
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why is this table writable?

ceno_emul/src/platform.rs
Comment on lines +43 to +47
0x4000_0000
}

pub const fn program_data_end(&self) -> Addr {
0x3000_1000 - 1
0x5000_0000 - 1
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe leave some comments for these two magic numbers.

ceno_zkvm/src/tables/ram/ram_impl.rs
"{} len {} must be a power of 2",
NVRAM::name(),
NVRAM::len()
);
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nitpick: It's also good to assert that NVRAM::OFFSET_ADDR and NVRAM::END_ADDR are divisible by 4.

ceno_zkvm/src/tables/ram/ram_impl.rs
let unused_addrs = (NVRAM::OFFSET_ADDR..NVRAM::END_ADDR)
.step_by(WORD_SIZE)
.filter(|&addr| !accessed_addrs.contains(&addr))
.take(NVRAM::len() - init_mem.len())
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(NVRAM::END_ADDR - NVRAM::OFFSET_ADDR) / 4 != NVRAM::len()?

ceno_zkvm/src/tables/ram/ram_impl.rs
@@ -111,7 +112,12 @@ impl<NVRAM: NonVolatileTable + Send + Sync + Clone> NonVolatileTableConfig<NVRAM
num_fixed: usize,
init_mem: &[MemInitRecord],
) -> RowMajorMatrix<F> {
assert!(NVRAM::len().is_power_of_two());
assert!(
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

According to L109, it's also good to assert that init_mem is sorted.

ceno_zkvm/src/tables/ram/ram_impl.rs
self.addr,
(NVRAM::addr(paddin_entry_start + i) as u64).into()
);
init_table
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the correct way to assign init_table is like this because the init_table.addr will not depend on init_mem.

init_table
  .par_iter_mut()
  .zip((NVRAM::OFFSET_ADDR..NVRAM::END_ADDR).step_by(WORD_SIZE).take(NVRAM::len()))
  .for_each(|(row, addr)| {
    if accessed_addrs.contains(addr) {
       // assign `init_mem.value` to `self.init_v` 
    } else {
       // assign zero to `self.init_v`
    }
  });

ceno_zkvm/src/tables/ram/ram_impl.rs
set_val!(row, self.final_cycle, 0u64);
});
}
final_table
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the assignment of final table is incorrect if [item.addr for item in init_mem] != [item.addr for item in final_mem]. For example, if the addresses in init_mem are vec![4, 12, 16] and the addresses in final_mem are vec![12, 16, 20], then this cause prod_r != prod_w error.

ceno_zkvm/src/tables/ram/ram_impl.rs
@@ -306,6 +317,15 @@ impl<NVRAM: NonVolatileTable + Send + Sync + Clone> PubIOTableConfig<NVRAM> {
set_val!(row, self.final_cycle, rec.cycle);
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the old assignment is incorrect as it assumes that

final_mem
  .iter()
  .enumerate()
  .for_each(|(i, rec)| {
    assert_eq!(NVRAM::addr(i), rec.addr);
  });

ceno_zkvm/src/tables/ram/ram_impl.rs
});
}
set_val!(row, self.addr, addr as u64);
}
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Forget to assign 0 to self.final_cycle?

ceno_zkvm/examples/fibonacci_elf.rs
Comment on lines +101 to +103
let stack_addrs = (1..=STACK_SIZE)
.map(|i| STACK_TOP - i * WORD_SIZE as u32)
.map(|addr| MemInitRecord { addr, value: 0 });
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why does stack occurs in program data section?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@naure naure naure left review comments

@matthiasgoergens matthiasgoergens matthiasgoergens left review comments

At least 1 approving review is required to merge this pull request.

Assignees

@kunxian-xia kunxian-xia

Labels
integration
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

prove fibonacci program example to improve testing coverage
4 participants
@kunxian-xia @naure @matthiasgoergens @hero78119