Further enhance LEM's witness generation speed #783
Conversation
|
Note: it would be easier to review this if many of the changes weren't cosmetic/renaming. If those are important and need to happen here, it would be simpler if the substantial changes were in isolated commits. This is just an informational note about the reviewer experience. |
arthurpaulino
force-pushed
the
lem-perf-attempt-5
branch
from
86f6a88 to
198da0b
Compare
| let preallocated_preimg: Vec<_> = (0..slot_type.preimg_size()) | ||
| .map(|component_idx| { | ||
| AllocatedNum::alloc_infallible( | ||
| cs.namespace(|| format!("component {component_idx} slot {slot}")), | ||
| || F::ZERO, | ||
| ) | ||
| }) | ||
| .collect(); |
There was a problem hiding this comment.
Although I don't think it's introduced in this PR, it seems that the handling of preimage values is smudging the bellpepper API. When we are synthesizing shapes without data, we should not be specifying concrete values. Even if we get away with it here, this is sloppy and may end up biting us.
There was a problem hiding this comment.
My point is not that the above code will always run in a context where no real value exist — only that I think it sometimes will.
There was a problem hiding this comment.
Maybe I'm missing the point, but this is not to synthesize the shape without data. It's to synthesize slots that weren't visited during interpretation with dummy data
There was a problem hiding this comment.
Right, which is what I mentioned in my second comment. But the point is that when synthesizing without data, one of the two branches of this conditional will have to be taken, and they both allocate infallibly, as far as I can tell. Is there some third code path that is used to synthesize when creating a shape? If so, that's also not the standard usage.
There was a problem hiding this comment.
No, this is the only code that's used to create the shape. But I think this is getting into territory @gabriel-barrett understands better
There was a problem hiding this comment.
It has come up elsewhere, and I'm reiterating the point here.
There was a problem hiding this comment.
Can you create an issue for it please? I don't think I understand the problem well enough yet.
arthurpaulino
force-pushed
the
lem-perf-attempt-5
branch
from
198da0b to
b50c017
Compare
arthurpaulino
force-pushed
the
lem-perf-attempt-5
branch
from
b50c017 to
3476747
Compare
arthurpaulino
force-pushed
the
lem-perf-attempt-5
branch
from
3476747 to
9c7aabc
Compare
github-merge-queue
bot
removed this pull request from the merge queue due to failed status checks
arthurpaulino
force-pushed
the
lem-perf-attempt-5
branch
from
9c7aabc to
de02574
Compare
This PR is the result of a long iterative process of improvements on LEM's witness generation algorithm.
rayonto generate the witnesses for all frames in parallel and it can make a better use of the CPUs than if we try to teach it how to do it💅🏼
GlobalstoRecursiveContextbecause it better represents its role