-
Notifications
You must be signed in to change notification settings - Fork 100
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
Try zero #2357
base: main
Are you sure you want to change the base?
Conversation
f3dff12
to
0487eb6
Compare
Hmm, I'm not sure I agree with this: For example, if a block machine output is not constrained, don't we want the entire process to fail? To catch soundness bugs? Also, wouldn't this lead to the |
Hm, interesting! I was looking at this in the context of https://github.com/powdr-labs/powdr/pull/2357/files#diff-18909377b8656c5e03adf2051ea1b22bfbe3fcfcf95357c630319b99f6356f59R368 - where I think that we certainly need it (and I also think that such things occur as well). So essentially this is concerning constraints that are deactivated by some flags. Another example is a VM where an assignment register is not used by an instruction. |
Ok, maybe the solution for the case where the instruction does not use an assignment register is that assignment registers actually should not be assumed to be known on the previous row and should not be required to be computed in the next row. |
And the solution for the case where "operation_id = 0" is nonsensical would be that we either require it to be nonzero or we get an input constraint that disallows it. But the latter means that we need to provide input constraints for codegen, which extends the input space. Maybe we can try without input constraints first, and re-try with input constraints if it doesn't work? |
Not sure what you mean by that! I do think it makes sense to treat the operation ID like an input. |
This PR extends the check for "are we finished?" such that it still works if there are unknown variables left, but they are not constrained given the current state.