ZIR-353: Keccak circuit is fully deterministic #205
Conversation
github-actions
bot
changed the title
jacobdweightman
force-pushed
the
jacob/picus-v2
branch
9 times, most recently
from
2114b03 to
9447bf2
Compare
jacobdweightman
force-pushed
the
jacob/picus-v2
branch
from
9447bf2 to
792f158
Compare
jacobdweightman
force-pushed
the
jacob/picus-v2
branch
from
792f158 to
fcb3724
Compare
|
Do these changes cause the |
|
I just reran the zirgen repo's |
| AttrTypeReplacer replacer; | ||
| replacer.addReplacement([&](StructType t) { return typeReplacer(replacer, t); }); | ||
| replacer.addReplacement([&](LayoutType t) { return typeReplacer(replacer, t); }); | ||
| // replacer.addReplacement(attrReplacer); // TODO: I should optimize the attributes too! |
There was a problem hiding this comment.
is this TODO left intentionally?
| SmallVector<std::pair<size_t, size_t>> merges; | ||
| for (size_t i = 0; i < members.size(); i++) { | ||
| for (size_t j = i + 1; j < members.size(); j++) { | ||
| if (members[i] == members[j]) { |
There was a problem hiding this comment.
This nested loop makes me nervous, and I wonder if you've considered using a multimap instead. Or can we be sure that N is always small enough that it won't matter?
There was a problem hiding this comment.
This pass looks at the return value of a constructor, and if it is a PackOp then it searches for members that are the same. This is O(number_of_members^2), but in practice our components tend not to have very many members. I'm not entirely sure how a multimap helps with this, could you say a bit more?
There was a problem hiding this comment.
I was thinking you'd iterate over the members once to build a map from members to indexes, then iterate over the map to deduplicate - but if the number of members is small, it doesn't matter.
| // operations must also be in the first mux arm. | ||
| auto it = mux.getRegion(0).op_begin(); | ||
| while (it != mux->getRegion(0).op_end()) { | ||
| Operation& op = *(it++); |
There was a problem hiding this comment.
This looks to my eyes like a decomposed for loop, and I wonder whether iterating over Region::getOps wouldn't be simpler? Perhaps there's a good reason it's done this way, but a comment explaining the unusual structure might be nice.
There was a problem hiding this comment.
Because hoisting moves operations out of arm 0, this iteration scheme avoids losing track of which operation in the region we're looking at, so using a for loop doesn't work. I've updated the comment to reflect this, I realize this was not as clear as it could be, so thanks for the feedback!
| @@ -224,6 +224,14 @@ auto reduce(std::array<T1, N> elems, T2 start, const BoundLayout<T3>& b, F f) { | |||
| // All the extern handling | |||
| #define INVOKE_EXTERN(ctx, name, ...) extern_##name(ctx, ##__VA_ARGS__) | |||
|
|
|||
| // TODO: release mode that removes assertions | |||
There was a problem hiding this comment.
is this todo still relevant?
There was a problem hiding this comment.
Unfortunately. I'm planning to come back to that in a followup.
|
I also ran bootstrap locally to see if this would break anything, and since it's just source location changes in comments, I approved. |
|
Thanks for the feedback, @mars-risc0 and @flaub! I'm in a bit of a hurry to get this merged, so I'm going to follow up on a flag for stripping out asserts and the |
This PR contains a lot of changes to complete the Picus proof of deteterminism for the Keccak circuit.
--emit=zhltoptcode size.AliasLayoutOps used "across" mux arms are translated into linear combinations instead of arm-local assertionsPicusInputdirective to declare actual circuit inputs (which otherwise look nondeterministic)PicusHintEqdirective to help Picus reason about "non-local" constraintsAssertRangeandAssumeRangedirectives@layoutmembers in Picus translationexterns thepicus_inlineattribute by default