Make hint padding 'inaccessible'

[matthiasgoergens]

In our VM we have reserved a specific memory region that the prover/host can map private hint data into.

The size of that region is an upper limit, but most of the time we have less data. In that case here's what we are currently doing:

• We map the provided data, so that its start aligns with the start of the memory region.
• In the emulator, we fill the rest of the entire hint memory region with zeroes.
• In the prover/circuits, we pad the end of the given data with zeroes to hit the next power of two in size, then we fill the rest of the hint memory region with 'inaccessible'.

(To be clear, most of that 'filling' happens lazily behind the scenes, ie memory reads act as-if we filled the memory as described.)

'Inaccessible' means that trying to access the memory in question leads to a program abort / failure to prove.

I suggest we unify that behaviour, amongst other things, to make guest development easier: if it runs, it should prove.

For technical reasons, our circuits will always fill the vast majority of the unused hint memory with 'inaccessible'. Thus the simplest unification is:

• Fill the entire rest of the memory region with 'inaccessible'

That means treat both prover and emulator the same, and also don't worry our users about padding to a power of two. That's a much simpler interface.

(As far as I can tell, for technical reasons we have to pad to the next power of two internally in the circuits, but we can pad that with 'inaccessible', instead of padding with 0.)

Original thread at https://github.com/scroll-tech/ceno/pull/622/files#r1855846990

[hero78119]

In the emulator: we collect max access address per execution trace, let say this time is 0xaabbccdd. Emulator just assure it within upper limit.
In the circuit assignment: we respect 0xaabbccdd, then find 0xaabbccdd.next_power_of_2() and padding rest with 0 => this padding is just for sumcheck "implementation" to work properly, so the padding also agnostic to guest development and also doesn't matter.

Right now we exactly support "if it runs (in emulator), it should prove (in circuit)", to be frankly I dont quite get the idea for what this issue for, could you please clarify for what the key point of this proposal?

[matthiasgoergens]

@hero78119 Thanks for your write-up. Let me write some simple guest programs to verify my understanding, then I'll come back to you on this.

@naure Do we have any example / test using your new private hint functionality? I’m trying to run some experiments to verify my understanding. Thanks!

(If yes, could you please point me to the example? Thanks!)