Integration test #368

kunxian-xia · 2024-10-12T16:06:18Z

Summary

This PR aims to add an integration test in which we proves the fibonacci rust program. The goal will be achieved by two steps:

We will only prove the fibonacci ELF compiled by SP1 rust toolchain in the first place;
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.

Performance

By running the command cargo run --example fibonacci_elf --release, we get the e2e proving time is 48.5s ¹ for 11538921 execution steps. This is equivalent to 237.9 kHz.

Configuration of the benchmark machine: AMD EPYC 9R14 (32 threads) + 64GB memory ↩

ceno_zkvm/examples/fibonacci-elf

ceno_emul/src/platform.rs

kunxian-xia · 2024-10-29T17:56:40Z

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

ceno_zkvm/src/instructions/riscv/jump/jalr.rs

ceno_zkvm/src/structs.rs

ceno_zkvm/src/scheme/prover.rs

ceno_emul/src/vm_state.rs

naure · 2024-11-18T09:37:59Z

~~Status: it still breaks starting from --max-steps=4097 with logup_sum != 0~~

… feat/guest-example

naure · 2024-11-18T17:27:24Z

Fixed a bug: missing padding in the program table witness.

That seems unrelated but it was just randomly triggered by changes in this PR.

@kunxian-xia Ready again.

kunxian-xia

The new changes look good to me!

hero78119 · 2024-11-19T17:49:05Z

ceno_zkvm/src/tables/ram/ram_impl.rs

        assert!(DVRAM::max_len().is_power_of_two());
-        let mut final_table =
-            RowMajorMatrix::<F>::new(final_mem.len().next_power_of_two(), num_witness);
+        let mut final_table = RowMajorMatrix::<F>::new(DVRAM::max_len(), num_witness);


Hi @naure , could you elaborate in new design how we achieve non-uniform overhead? previously the allocated memory in RowMajorMatrix are dynamic and cover final_ram which I assumed final ram size can be dynamic according to memory access "per proof". However It's not obvious to me for how it work in new design

This type is not used in the example program, so this change was maybe not necessary. We can revert it if that’s incorrect.

@kunxian-xia Which version do you think is right?

new version is incorrect to me. Original design is the key of our non-uniform memory overhead for RAM holding heap/stack.
Originally I thought the design was kept in some other places so I bring up this question.
(I was also a bit surprise how this type is not used in Fabonacci program 😮, will check detail for how Fabonacci works in this PR)

I think there was some minor bug in it but that was maybe not the right fix. Let me revert / fix this in a new PR.

The fibonacci program uses only a few predictable static addresses. So it works perfectly with NonVolatileRamCircuit and its addr: Fixed.

Revert: #601

I think the old design is wrong as it should not create the final_table based on the length of final_mem. For example, if the addresses in final_mem are vec![4, 16, 20, 128, 168], then the old assignment will create a final_table that only has 4 elements, while the correct final_table should has 168.next_power_of_two() = 256 elements.

old design:

final_mem can start on arbitrary offset address

final_mem are in dense and last is the max_access address

For example, if offset address is 0x12340000, and max access is 0x12340018
then address final_mem should be [0x12340000, 0x12340004, 0x12340008, 0x1234000c, 0x12340010, 0x12340014, 0x12340018]. In this case, final table size will be 7.next_power_of_two() = 8.

@kunxian-xia does the explanation make sense to you :) ?

Previously I didnt have clear documents on that so it cause misunderstanding, and at that moment emul mem design not settle yet, sorry for that

Will review on #601 and let settle the design there

Yeah, the above explanation makes sense to me. The main issue we have is we need to insert untouched memory records into final_mem manually. As in your example, if the real touched addresses are vec![0x12340000, 0x12340008, 0x12340018], then we need to insert vec![0x12340004, 0x1234000c, 0x12340010, 0x12340014] into final_mem manually, is this what you have in mind?

The main issue we have is we need to insert untouched memory

yes exactly, as I previously explanation we should be able to resolve unconsecutive mem access in imperfect but good enough version.

ceno_zkvm/examples/fibonacci.elf

matthiasgoergens · 2024-11-20T03:34:09Z

ceno_zkvm/examples/fibonacci_elf.rs

+        .map(|rs2| rs2.value);
+
+    let final_access = vm.tracer().final_accesses();
+    let end_cycle: u32 = vm.tracer().cycle().try_into().unwrap();


If PublicValues needs a u32 for end_cycle, then fn cycle should probably return a u32?

matthiasgoergens · 2024-11-20T03:36:29Z

ceno_zkvm/examples/fibonacci_elf.rs

+        .assign_table_circuit::<ExampleProgramTableCircuit<E>>(&zkvm_cs, &prog_config, vm.program())
+        .unwrap();
+
+    if std::env::var("MOCK_PROVING").is_ok() {


MOCK_PROVING=no ./run_my_programming would also result in this branch being taken? This might be a bit suprising.

.github/workflows/integration.yml

- Revert #368 for `DynVolatileRamTableConfig`. - Add padding of `final_cycle`. --------- Co-authored-by: Aurélien Nicolas <[email protected]>

kunxian-xia added the integration label Oct 12, 2024

kunxian-xia self-assigned this Oct 12, 2024

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

Closed

2 tasks

kunxian-xia marked this pull request as draft October 12, 2024 16:08

matthiasgoergens reviewed Oct 12, 2024

View reviewed changes

ceno_zkvm/examples/fibonacci-elf Outdated Show resolved Hide resolved

matthiasgoergens reviewed Oct 22, 2024

View reviewed changes

ceno_emul/src/platform.rs Outdated Show resolved Hide resolved

kunxian-xia force-pushed the feat/guest-example branch from 85fcacd to 6e3799c Compare October 25, 2024 15:13

kunxian-xia changed the base branch from master to feat/load_mem October 25, 2024 15:14

kunxian-xia force-pushed the feat/guest-example branch from 8c31993 to 80a1cd4 Compare October 25, 2024 15:19

Base automatically changed from feat/load_mem to master October 28, 2024 11:47

kunxian-xia force-pushed the feat/guest-example branch from b3648c9 to 447001f Compare October 28, 2024 12:22

kunxian-xia changed the base branch from master to feat/expose_insns_in_emul October 28, 2024 12:29

kunxian-xia mentioned this pull request Oct 29, 2024

Feat: expose base_address and instructions decoded from ELF #487

Merged

Base automatically changed from feat/expose_insns_in_emul to master October 29, 2024 08:53

kunxian-xia added 3 commits October 30, 2024 01:29

wip

f4ddd9a

wip

b24c98a

include all opcodes in rv32im config

9dd45db

kunxian-xia force-pushed the feat/guest-example branch from aed3b11 to 9dd45db Compare October 29, 2024 17:34

kunxian-xia marked this pull request as ready for review October 29, 2024 17:35

ignore ecall other than halt

05b46ca

kunxian-xia added 2 commits October 30, 2024 14:26

redirect X0 writes to X32

37d0666

taplo fmt

41cbb09

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 mentioned this pull request Oct 30, 2024

Degree >2 expression in JALR #502

Closed

naure reviewed Oct 30, 2024

View reviewed changes

ceno_emul/src/vm_state.rs Outdated Show resolved Hide resolved

kunxian-xia added 4 commits October 31, 2024 11:02

print out more info for debugging

3ec6bf7

Merge remote-tracking branch 'origin/master' into feat/guest-example

ab2c12b

commit opcode circuits first

71dfac6

debugging sumcheck prover hang

ea12939

naure force-pushed the feat/guest-example branch from b1078df to 9211c7a Compare November 18, 2024 09:10

feat/guest-example: remove Platform program_data

e52dd42

naure force-pushed the feat/guest-example branch from 9211c7a to e52dd42 Compare November 18, 2024 09:15

kunxian-xia mentioned this pull request Nov 18, 2024

Run CI on self-hosted machine #499

Merged

Aurélien Nicolas and others added 4 commits November 18, 2024 10:51

feat/guest-example: more info

307bf52

run examples under release mode

12abf35

feat/guest-example: assign cycle of unused dyn records

dc0f10e

Merge branch 'feat/guest-example' of github.com:scroll-tech/ceno into…

7e00fac

… feat/guest-example

naure mentioned this pull request Nov 18, 2024

Make the platform dynamic #566

Closed

Merge branch 'master' into feat/guest-example

40b2cc4

kunxian-xia requested a review from hero78119 November 18, 2024 14:55

feat/guest-example: pad program table witness

2d5198f

kunxian-xia commented Nov 19, 2024

View reviewed changes

Merge branch 'master' into feat/guest-example

1f6d187

naure approved these changes Nov 19, 2024

View reviewed changes

naure merged commit 63ad6f9 into master Nov 19, 2024
6 checks passed

naure deleted the feat/guest-example branch November 19, 2024 17:08

hero78119 reviewed Nov 19, 2024

View reviewed changes

naure pushed a commit that referenced this pull request Nov 19, 2024

revert-dyn-ram: revert #368 for DynVolatileRamTableConfig

0ac00f7

naure mentioned this pull request Nov 19, 2024

Revert dyn ram #601

Merged

kunxian-xia changed the title ~~WIP: integration test~~ Integration test Nov 20, 2024

matthiasgoergens reviewed Nov 20, 2024

View reviewed changes

ceno_zkvm/examples/fibonacci.elf Show resolved Hide resolved

matthiasgoergens reviewed Nov 20, 2024

View reviewed changes

matthiasgoergens added a commit that referenced this pull request Nov 20, 2024

Clean up after #368

da7472a

matthiasgoergens mentioned this pull request Nov 20, 2024

Clean up after 'WIP: integration test (#368)' #603

Open

matthiasgoergens reviewed Nov 20, 2024

View reviewed changes

.github/workflows/integration.yml Show resolved Hide resolved

hero78119 pushed a commit that referenced this pull request Nov 21, 2024

Revert dyn ram (#601)

25920cf

- Revert #368 for `DynVolatileRamTableConfig`. - Add padding of `final_cycle`. --------- Co-authored-by: Aurélien Nicolas <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Integration test #368

Integration test #368

kunxian-xia commented Oct 12, 2024 •

edited

Loading

kunxian-xia commented Oct 29, 2024 •

edited

Loading

naure commented Nov 18, 2024 •

edited

Loading

naure commented Nov 18, 2024

kunxian-xia left a comment

hero78119 Nov 19, 2024 •

edited

Loading

naure Nov 19, 2024

hero78119 Nov 19, 2024 •

edited

Loading

naure Nov 19, 2024

naure Nov 19, 2024 •

edited

Loading

naure Nov 19, 2024

kunxian-xia Nov 20, 2024

hero78119 Nov 20, 2024 •

edited

Loading

kunxian-xia Nov 20, 2024

hero78119 Nov 20, 2024

matthiasgoergens Nov 20, 2024

matthiasgoergens Nov 20, 2024

Integration test #368

Integration test #368

Conversation

kunxian-xia commented Oct 12, 2024 • edited Loading

Summary

Performance

Footnotes

kunxian-xia commented Oct 29, 2024 • edited Loading

naure commented Nov 18, 2024 • edited Loading

naure commented Nov 18, 2024

kunxian-xia left a comment

Choose a reason for hiding this comment

hero78119 Nov 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hero78119 Nov 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

naure Nov 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hero78119 Nov 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kunxian-xia commented Oct 12, 2024 •

edited

Loading

kunxian-xia commented Oct 29, 2024 •

edited

Loading

naure commented Nov 18, 2024 •

edited

Loading

hero78119 Nov 19, 2024 •

edited

Loading

hero78119 Nov 19, 2024 •

edited

Loading

naure Nov 19, 2024 •

edited

Loading

hero78119 Nov 20, 2024 •

edited

Loading