chore: claude-generated sha audit #19253
Draft
+31
−2
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
Author
This stack of pull requests is managed by Graphite. Learn more about stacking. |
Contributor
Author
|
And: Style Note: Inconsistent Lookup Column CountThe The extra column is |
dbanks12
commented
Dec 24, 2025
Comment on lines
-116
to
148
|
|
||
| #[LATCH_HAS_SEL_ON] // sel = 1 when latch = 1, sel = 0 at first row because of shift relations | ||
| #[LATCH_HAS_SEL_ON] | ||
| latch * (1 - sel) = 0; | ||
| // This is now guaranteed to be mututally exclusive because of the above condition and since sel = 0 at row = 0 (since it has shifts) | ||
|
|
||
| // LATCH_CONDITION is the sum of latch and first_row. We need to ensure these are mutually | ||
| // exclusive (i.e., LATCH_CONDITION is always 0 or 1, never 2) for start to remain boolean. | ||
| // | ||
| // Proof that latch = 0 when first_row = 1 (i.e., on row 0): | ||
| // | ||
| // For latch_0 = 1, the zero-check constraint (sha256.pil) requires rounds_remaining_0 = 0. | ||
| // Also, LATCH_HAS_SEL_ON requires sel_0 = 1. | ||
| // | ||
| // From START_AFTER_LAST on the last row (N-1): sel_0 * (start_0 - LATCH_CONDITION_{N-1}) = 0 | ||
| // Since sel_0 = 1: start_0 = LATCH_CONDITION_{N-1} | ||
| // | ||
| // Case A: LATCH_CONDITION_{N-1} = 1 (last row has latch = 1) | ||
| // - start_0 = 1 | ||
| // - Round initialization constraint: start * (rounds_remaining - 64) = 0 | ||
| // - This forces rounds_remaining_0 = 64 | ||
| // - CONTRADICTION: rounds_remaining_0 cannot be both 0 (for latch=1) and 64 (for start=1) | ||
| // - This case is impossible - constraints are unsatisfiable. | ||
| // | ||
| // Case B: LATCH_CONDITION_{N-1} = 0 (last row has latch = 0, boundary-spanning computation) | ||
| // - start_0 = 0 | ||
| // - LATCH_CONDITION_0 = latch_0 + first_row_0 = 1 + 1 = 2 | ||
| // - perform_round_0 = (1 - LATCH_CONDITION_0) * SEL_NO_ERR = (1 - 2) * 1 = -1 | ||
| // - sel_compute_w and other selectors derived from perform_round become non-boolean (-1) | ||
| // - Lookups using these selectors contribute -1 to the grand product | ||
| // - Destination selectors are boolean (0 or 1), so lookups CANNOT balance | ||
| // - This case fails lookup constraints - no valid proof can be generated. | ||
| // | ||
| // Therefore, latch = 1 on row 0 is impossible in any valid trace, and LATCH_CONDITION | ||
| // is guaranteed to be 0 or 1. | ||
| pol LATCH_CONDITION = latch + precomputed.first_row; |
Contributor
Author
There was a problem hiding this comment.
I think this was claude trying to justify mutual exclusivity
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Please read contributing guidelines and remove this line.
For audit-related pull requests, please use the audit PR template.