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.

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

Divide-by-zero and division overflow handling #498

Closed
randomsleep opened this issue Nov 7, 2024 · 3 comments
Closed

Divide-by-zero and division overflow handling #498

randomsleep opened this issue Nov 7, 2024 · 3 comments

Comments

@randomsleep
Copy link
Contributor

According to the RISC-V spec, divide-by-zero and division overflow won't raise exception. Instead, it will return specific values.

image

In Jolt DIV, DIVU, REM, and REMU instruction this is not handled. There is AssertValidDiv0Instruction but it seems it is not used.

@moodlezoup
Copy link
Collaborator

moodlezoup commented Nov 7, 2024

It should be handled, for the division and remainder instructions Jolt uses "virtual sequences" (see Section 6.2 of the Jolt paper and this section of the Jolt book). This is where e.g. the AssertValidDiv0Instruction arises (see div.rs). Feel free to reopen this issue if I'm missing something

@randomsleep
Copy link
Contributor Author

@moodlezoup Oh thanks! The code already handled that. The Jolt paper didn't mention these AssertValidDiv0Instruction instruction in DIV.

The sequence_output in divu and remu should be updated according to that?

fn sequence_output(x: u64, y: u64) -> u64 {
x / y
}

@moodlezoup
Copy link
Collaborator

moodlezoup commented Nov 8, 2024

Ah yes, nice catch. That method's only used in tests so not super urgent but will make a note to fix!

#499

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants