Fix DynVolatileRamTable::max_len

[matthiasgoergens]

The previous logic only ever worked for powers of two.

[matthiasgoergens]

I think I can fix this one relatively easily via something like max_size.next_power_of_two().div_ceil(WORD_SIZE as u32). But need to confirm that this is a problem, first.

[hero78119]

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

[matthiasgoergens]

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?

[hero78119]

Just illustrate with pic

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

[matthiasgoergens]

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.

[hero78119]

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.

[matthiasgoergens]

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?

[hero78119]

[...] 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

[matthiasgoergens]

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?

[hero78119]

• in circuit setup phase, we extract the max_len of specific memory type into the constrain system, so as verifier key https://github.com/scroll-tech/ceno/blob/master/ceno_zkvm/src/tables/ram/ram_impl.rs#L350

• per execution trace, verifier take this information to check memory min/max spanning not exceeding len encoded in vk https://github.com/scroll-tech/ceno/blob/master/ceno_zkvm/src/scheme/verifier.rs#L545

• per execution trace, prover only pay the cost on execution actually used, https://github.com/scroll-tech/ceno/blob/master/ceno_zkvm/src/tables/ram/ram_impl.rs#L370-L372

[matthiasgoergens]

Thanks!