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

Fix DynVolatileRamTable::max_len #716

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

Fix DynVolatileRamTable::max_len #716

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d9cc59b
Check: is `DynVolatileRamTable::max_len` broken?
matthiasgoergens Dec 9, 2024
52418da
Fix tests
matthiasgoergens Dec 9, 2024
cfb586c
Round paranoid
matthiasgoergens Dec 9, 2024
f580a0d
Clean up
matthiasgoergens Dec 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions ceno_zkvm/src/tables/ram.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,15 @@ impl DynVolatileRamTable for DynMemTable {
}
}

#[test]
fn test_dyn_mem_table() {
let mut params = ProgramParams::default();
params.platform.ram.start = 0;
params.platform.ram.end = 100;
let max_len_bytes = 4 * DynMemTable::max_len(&params);
assert_eq!(max_len_bytes, 128);
Copy link
Collaborator

Choose a reason for hiding this comment

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

correct result is 64. In dynamic memory case, we want to get prev_power_of_2

Copy link
Collaborator Author

@matthiasgoergens matthiasgoergens Dec 9, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

Could you please help me craft a comment to explain the logic we want here?

What is the supposed meaning of the result of the trait function max_len? It seems rather confusing to me.

It looks like it should be the number of rows we need to initialise the memory? Or something else?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Just illustrate with pic
image

next_pow2 is just to padding memory in used per proof to make sumcheck implementation work
prev_pow2 is to make (end - offset) aligned with power of 2. So the maximal in used mem can't exceed this range.

So current max_len logic fit above design, so we dont need this PR actually

Copy link
Collaborator Author

@matthiasgoergens matthiasgoergens Dec 10, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

Thanks for the explanation. You are pointing to a flaw in our design.

See in ceno_emul we define our 'platform':

/// The Platform struct holds the parameters of the VM.
/// It defines:
/// - the layout of virtual memory,
/// - special addresses, such as the initial PC,
/// - codes of environment calls.
#[derive(Clone, Debug)]
pub struct Platform {
    pub rom: Range<Addr>,
    pub ram: Range<Addr>,
    pub public_io: Range<Addr>,
    pub hints: Range<Addr>,
    pub stack_top: Addr,
    /// If true, ecall instructions are no-op instead of trap. Testing only.
    pub unsafe_ecall_nop: bool,
}

The doc comment suggests that everything in Platform::ram is available for read-write memory. And nothing in ceno_emul contradicts that.

However the logic in ceno_zkvm that you kindly explained means that in general, ie for ram sizes not powers of two, a program using the promised ram will run just fine in the emulator, but will fail to prove.

In the spriti of #630 I suggest we change the circuits so that an execution staying strictly within the promised platform capabilities will both run and prove.

(Concretely here, if the platform promises 100 bytes of RAM, we should deliver at least 100 bytes of RAM, not 64.)

Please correct me, if I am wrong.

Copy link
Collaborator

@hero78119 hero78119 Dec 10, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

I pretty agree that this is a good case that we should align both emul and circuit.
Circuit & proving system currently rely on pow 2 to succinctly evaluate address polynomial with respect to a random point.
So it will be better add check in toolchain/emulator to assure memory space are aligned with power 2 address.

Copy link
Collaborator Author

@matthiasgoergens matthiasgoergens Dec 10, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

Yes, we have two possibilities here:

  • Replace the whole computation here with an assertion that we are using a power of two. (And probably add an assertion in the emulator, too.)
  • Or make the change I suggested to round up to the next power of two.

Either way works for me. You seem to be happier with the assertions?

However, I would suggest that the circuits should only prepare RAM of the size that was actually used.

So even if our maximum RAM available is, say, 1GiB, the prover should look at the span between maximum and minimum address actually accessed as RAM during the execution and only do work accordingly (rounded up to the next power of two, of course).

What do you think?

Copy link
Collaborator

@hero78119 hero78119 Dec 10, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

[...] the prover should look at the span between maximum and minimum address actually accessed as RAM during the execution and only do work accordingly [...]

we already support this feature (non uniform design) now (seems I keep spreading this message in many PR 😅 ) max_len only call in circuit setup phase and those information will be extract to constrain system, encoding to verifier key for check

Replace the whole computation here with an assertion that we are using a power of two. (And probably add an assertion in the emulator, too.)

+1 as this make spirit align, plus keeping verifier logic simple

So this PR probably can probably go toward this

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks!

[...] the prover should look at the span between maximum and minimum address actually accessed as RAM during the execution and only do work accordingly [...]

we already support this feature (non uniform design) now (seems I keep spreading this message in many PR 😅 ) max_len only call in circuit setup phase and those information will be extract to constrain system, encoding to verifier key for check

Ok, now I'm really confused! If we already have this feature, why do we even look at this max_len derived from the platform here, and not just look at what the execution actually used?

What's the point of the value we are computing here? Why don't we use the actual memory used for the circuit setup?

Copy link
Collaborator

@hero78119 hero78119 Dec 10, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks!

}

pub type DynMemCircuit<E> = DynVolatileRamCircuit<E, DynMemTable>;

#[derive(Clone)]
Expand Down
6 changes: 3 additions & 3 deletions ceno_zkvm/src/tables/ram/ram_circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,9 +161,9 @@ pub trait DynVolatileRamTable {
fn name() -> &'static str;

fn max_len(params: &ProgramParams) -> usize {
let max_size =
(Self::end_addr(params) - Self::offset_addr(params)).div_ceil(WORD_SIZE as u32) as Addr;
1 << (u32::BITS - 1 - max_size.leading_zeros()) // prev_power_of_2
let max_size = (Self::end_addr(params) as usize).div_ceil(WORD_SIZE)
- (Self::offset_addr(params) as usize) / WORD_SIZE;
max_size.next_power_of_two()
}

fn addr(params: &ProgramParams, entry_index: usize) -> Addr {
Expand Down