emul: Runtime and build scripts #173

naure · 2024-08-29T19:49:59Z

Issue #179. This is an experimental setup to compile programs for the VM.

Runtime

Introduce a ceno_rt crate. It is a convention to provide a *_rt for the platform, to handle details of startup, memory, and IO.
Minimal linker and build scripts to put the code at the right location.
Example ceno_rt_mini that successfully halts.
Example ceno_rt_mem that uses the stack and a global variable.
Example ceno_rt_panic that panics. The emulator returns an error.

Emulator

Parse compiled VM programs. This uses the elf crate and a function taken from Risc0.
Load the code and data into ROM and RAM.
Execute the program with the emulator.

* emul-elf: introduce elf crate and risc0 load_elf() * emul-elf: load and execute a test program * emul-elf: use examples/ folder * runtime: example program using memory and stack --------- Co-authored-by: Aurélien Nicolas <[email protected]>

hero78119

Overall LGTM! I believe detail can be further adjust once we move to integration phase

just to bring up a question to discuss regarding to overflow handling: does compiler/toolchain seasoning unsigned overflow check in riscv by default?

naure · 2024-09-02T10:13:44Z

Overall LGTM! I believe detail can be further adjust once we move to integration phase

Absolutely, we can go back to the layout of virtual memory and decide what regions the VM provides and how we are going to implement them. Then reflect it in the linker script.

just to bring up a question to discuss regarding to overflow handling: does compiler/toolchain seasoning unsigned overflow check in riscv by default?

I just tried and it is disabled by default. A particular program can enable it with overflow-checks = true; it will cause a trap, and the emulator will return an error.

hero78119 · 2024-09-02T13:02:01Z

I just tried and it is disabled by default. A particular program can enable it with overflow-checks = true; it will cause a trap, and the emulator will return an error.

Thanks for the quick verified :) I think it make sense to disable overflow-checks by default in compiler. The reason, IIUC, having overflow-check will make the trace longer, for example, opcode add roughly contribute to 40% execution traces, and enable overflow-checks=true means those 40% execution trace will be double. For now, prover circuit already constrain overflow at add circuit, and this constraint introduce negligible overhead in favour of longer traces.

In other word, it's like we on purposely design circuit dissatisfy perfect completeness of emulator statement, because it means there $\exists$ valid statements of executor (program + IO), which we are unable to generate respective valid proofs, because those proof will not pass the verifier check due to those are use overflow & wrapping add to deal with program logic. I would claim our program will not have this scenario therefore this limitation will not bring any impact.

cc @kunxian-xia and @zemse

hero78119 · 2024-09-03T02:32:41Z

I just tried and it is disabled by default. A particular program can enable it with overflow-checks = true; it will cause a trap, and the emulator will return an error.

Thanks for the quick verified :) I think it make sense to disable overflow-checks by default in compiler. The reason, IIUC, having overflow-check will make the trace longer, for example, opcode add roughly contribute to 40% execution traces, and enable overflow-checks=true means those 40% execution trace will be double. For now, prover circuit already constrain overflow at add circuit, and this constraint introduce negligible overhead in favour of longer traces.

In other word, it's like we on purposely design circuit dissatisfy perfect completeness of emulator statement, because it means there ∃ valid statements of executor (program + IO), which we are unable to generate respective valid proofs, because those proof will not pass the verifier check due to those are use overflow & wrapping add to deal with program logic. I would claim our program will not have this scenario therefore this limitation will not bring any impact.

cc @kunxian-xia and @zemse

An updated: realized revm i256 wrapping_add -> calling ruint crates overflowing_add https://github.com/recmo/uint/blob/ff2d1a65500172ec3f29313d78c84a20b48490fc/src/add.rs#L62-L63
so I guess respective assembly code should reflect a list of riscv instruction which should allow overflow. So I have to fixed by above statement with

keep overflow-checks = false by default
expose overflow as witin for external assignment

hero78119

Overall LGTM although not having all the check for the detail!

A suggestion: binary file will be better to compile on the fly instead of commit to repo. But since the size is small with just few kb, we can polishing it as enhancement later

hero78119 · 2024-09-06T07:25:21Z

build failed should be resolved after this #195
@naure please try to update to latest master branch

ceno_rt/src/lib.rs

naure · 2024-09-06T10:12:02Z

@hero78119 That worked, thank you!

@zemse

- Partially address issue #174 - fix under constraints - optimized constriants register read constraints check - address the discussion in #173 (comment) to support overflow/underflow arithmetics due to wrapping_add/sub in revm - `MockProver` move to test scope and load u16 table > Later we need to optimize and support table reuse across unittest to reduce overhead. cc @zemse :) - ~~all witness assignment use base field instead of ext field~~ done by #192 --------- Co-authored-by: kunxian xia <[email protected]>

_Based on #173._ This PR experiments with how Input / Output can work. It is based on MMIO - Memory-Mapped IO. It works by reading or writing to specific memory addresses. The system recognizes this and can commit to the content as part of the proof. This can also be used for debug statements during development: ``` 📜📜📜 Hello, World! 🌏🌍🌎 test test_ceno_rt_io ... ok ``` --------- Co-authored-by: Aurélien Nicolas <[email protected]>

_Based on #173._ - This PR provides a `GlobalAllocator` to support heap memory. - Example program using `Vec`. --------- Co-authored-by: Aurélien Nicolas <[email protected]> Co-authored-by: Ming <[email protected]>

_Issue #179._ This is an experimental setup to compile programs for the VM. ### Runtime - Introduce a `ceno_rt` crate. It is a convention to provide a `*_rt` for the platform, to handle details of startup, memory, and IO. - Minimal linker and build scripts to put the code at the right location. - Example `ceno_rt_mini` that successfully halts. - Example `ceno_rt_mem` that uses the stack and a global variable. - Example `ceno_rt_panic` that panics. The emulator returns an error. ### Emulator - Parse compiled VM programs. This uses the [elf crate](https://docs.rs/elf/latest/elf/) and a function taken from Risc0. - Load the code and data into ROM and RAM. - Execute the program with the emulator. --------- Co-authored-by: Aurélien Nicolas <[email protected]>

@zemse

- Partially address issue #174 - fix under constraints - optimized constriants register read constraints check - address the discussion in #173 (comment) to support overflow/underflow arithmetics due to wrapping_add/sub in revm - `MockProver` move to test scope and load u16 table > Later we need to optimize and support table reuse across unittest to reduce overhead. cc @zemse :) - ~~all witness assignment use base field instead of ext field~~ done by #192 --------- Co-authored-by: kunxian xia <[email protected]>

_Based on #173._ This PR experiments with how Input / Output can work. It is based on MMIO - Memory-Mapped IO. It works by reading or writing to specific memory addresses. The system recognizes this and can commit to the content as part of the proof. This can also be used for debug statements during development: ``` 📜📜📜 Hello, World! 🌏🌍🌎 test test_ceno_rt_io ... ok ``` --------- Co-authored-by: Aurélien Nicolas <[email protected]>

_Based on #173._ - This PR provides a `GlobalAllocator` to support heap memory. - Example program using `Vec`. --------- Co-authored-by: Aurélien Nicolas <[email protected]> Co-authored-by: Ming <[email protected]>

Aurélien Nicolas added 2 commits August 29, 2024 17:57

runtime: minimal compiled program

ca6adec

runtime: ecall halt

ef357f5

naure changed the title ~~Runtime~~ emul: Runtime and build scripts Aug 30, 2024

naure mentioned this pull request Aug 30, 2024

emul: Load and test an ELF #178

Merged

naure requested review from hero78119 and kunxian-xia August 30, 2024 10:24

naure marked this pull request as ready for review August 30, 2024 10:29

naure and others added 4 commits August 30, 2024 12:30

Merge branch 'master' into runtime

33cdf96

runtime: move to examples/

5390280

emul: Load and test an ELF (#178)

1d7f95d

* emul-elf: introduce elf crate and risc0 load_elf() * emul-elf: load and execute a test program * emul-elf: use examples/ folder * runtime: example program using memory and stack --------- Co-authored-by: Aurélien Nicolas <[email protected]>

runtime: use .init section

ef1839c

naure force-pushed the runtime branch 2 times, most recently from c5ad53a to 963d504 Compare September 2, 2024 07:40

runtime: startup code in the crate

2b84514

naure force-pushed the runtime branch from 963d504 to 2b84514 Compare September 2, 2024 07:44

Aurélien Nicolas added 2 commits September 2, 2024 09:47

Merge branch 'master' into runtime

72c4c59

runtime: detect busy loops

8982cc7

naure force-pushed the runtime branch from 6dc3975 to 8982cc7 Compare September 2, 2024 08:22

hero78119 reviewed Sep 2, 2024

View reviewed changes

runtime: test panic

8285d59

runtime: consolidate tests

c6b9c6f

naure force-pushed the runtime branch from c7ae04b to c6b9c6f Compare September 2, 2024 16:24

Aurélien Nicolas added 2 commits September 2, 2024 18:24

Merge branch 'master' into runtime

e7aae7a

runtime: clippy

c95e1a0

hero78119 mentioned this pull request Sep 3, 2024

allow wrapping_add/sub and fix under-constraints #181

Merged

naure requested a review from hero78119 September 4, 2024 14:01

Merge branch 'master' into runtime

62d1dbe

runtime: fix after merge

8cc8850

This was referenced Sep 4, 2024

Runtime IO #189

Merged

Runtime Alloc #190

Merged

kunxian-xia added the runtime label Sep 5, 2024

naure and others added 2 commits September 5, 2024 17:09

Merge branch 'master' into runtime

1bc1539

runtime: skip tests for RISC-V crate

9a94428

hero78119 mentioned this pull request Sep 6, 2024

ci skip riscv32im target #195

Merged

hero78119 approved these changes Sep 6, 2024

View reviewed changes

Merge branch 'master' into runtime

bb990c8

chaosma reviewed Sep 6, 2024

View reviewed changes

ceno_rt/src/lib.rs Show resolved Hide resolved

naure merged commit 41aa9f8 into master Sep 6, 2024
4 checks passed

naure deleted the runtime branch September 6, 2024 10:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

emul: Runtime and build scripts #173

emul: Runtime and build scripts #173

naure commented Aug 29, 2024 •

edited

Loading

hero78119 left a comment

naure commented Sep 2, 2024 •

edited

Loading

hero78119 commented Sep 2, 2024 •

edited

Loading

hero78119 commented Sep 3, 2024 •

edited

Loading

hero78119 left a comment •

edited

Loading

hero78119 commented Sep 6, 2024

naure commented Sep 6, 2024

emul: Runtime and build scripts #173

emul: Runtime and build scripts #173

Conversation

naure commented Aug 29, 2024 • edited Loading

Runtime

Emulator

hero78119 left a comment

Choose a reason for hiding this comment

naure commented Sep 2, 2024 • edited Loading

hero78119 commented Sep 2, 2024 • edited Loading

hero78119 commented Sep 3, 2024 • edited Loading

hero78119 left a comment • edited Loading

Choose a reason for hiding this comment

hero78119 commented Sep 6, 2024

naure commented Sep 6, 2024

naure commented Aug 29, 2024 •

edited

Loading

naure commented Sep 2, 2024 •

edited

Loading

hero78119 commented Sep 2, 2024 •

edited

Loading

hero78119 commented Sep 3, 2024 •

edited

Loading

hero78119 left a comment •

edited

Loading