Casual Sunday SHA256 Optimizations With Claude#395
Open
rot256 wants to merge 14 commits into
Open
Conversation
Add Clean/Utils/CostR1CS.lean: counts witness cells, assert (R1CS constraint) rows, and lookup rows of a circuit, recursing through subcircuits. Linear combinations are free in R1CS, so the assert-row count equals the constraint count. Add pLarge (2^36+31), a small certifiable prime above 2^33 used as a field-independent stand-in for large fields (e.g. BN254) when measuring circuit cost, keeping native_decide primality cheap.
Report witness, constraint, and lookup counts for the SHA-256 gadgets via the cost meter, instantiated at the large measurement prime. Records the pre-optimization baseline (block ~40280 witnesses / ~40880 constraints, no lookups).
Define addMod32: sums n<=8 32-bit bit-vector operands mod 2^32 in a single range reduction (32 output bits + 3 carry bits + 1 linear constraint), exploiting that linear combinations are free in R1CS. Includes the intended Assumptions/Spec. FormalCircuit soundness/completeness proofs are pending; nothing depends on this gadget yet.
Complete the FormalCircuit for the multi-operand modular adder: given normalized operands (n <= 8), the output equals their sum mod 2^32 and is normalized. Soundness lifts the single field linear constraint to the naturals using p > 2^35 (3-bit carry covers up to 8 operands). No sorry; only the standard Lean axioms.
Replace the three chained add32 calls in each schedule step with one 4-operand addMod32 reduction. Per-step cost drops from 227 to 163 witnesses (schedule total 10896 -> 7824); the spec is matched via the (a+b+c+d) mod 2^32 = add32 (add32 a b) (add32 c d) identity. Field hypothesis strengthened to p > 2^35 (required by addMod32; not a spec change). No sorry; standard axioms only.
Build new_a/new_e from the multi-operand addMod32 gadget instead of a chain of binary add32, and prove soundness and completeness for the round against the spec. Cuts the round from 455 to 294 witnesses.
Propagate the new round (294 witnesses, output offsets 259/224, requires p > 2^35) and message schedule (163 witnesses per word) through the 64-round loop and full block compression, restoring soundness and completeness. Block compression drops from 40280 to 26904 witnesses.
Correct the AddMod32 header note (its FormalCircuit is proved and now used by the round and schedule), and document the round-derived offset/length constants in the compression layer.
Arithmetize the four Sigma/sigma functions (3-input XOR) and Maj
using the full-adder identity for bits:
a + b + c = (a XOR b XOR c) + 2 * maj(a, b, c)
Witness a single carry bit per output bit with two boolean
constraints (q and the parity a+b+c-2q), which pin q to the
majority and the parity to the XOR. The XOR result is then fed to
the downstream AddMod32 as an un-witnessed linear combination
instead of a second witnessed bit vector. Soundness needs the
field characteristic outside {2,3}, supplied by the existing
p > 2^35 bound.
This halves the witness count of each Sigma/sigma (64 -> 32) and
Maj (64 -> 32); constraints are unchanged. Per-block witnesses for
the compression function drop from 26904 to 17688 (-34%),
constraints stay at 27088.
Soundness and completeness are reproved for the new gadgets and
the round/schedule/compress composition; the shared carry-save
lemmas live in the new CarrySave.lean.
Replace the carry-save 3-input XOR in the four SHA-256 Sigma/sigma functions with a single R1CS constraint per output bit: (o + 2a + 2b + 7c)(a + b - 4c + 1) = 6a + 6b - 24c The constraint is linear in the witnessed output o, with a multiplier that never vanishes on the boolean cube, so its unique root is exactly a XOR b XOR c. Soundness (xor3_unique) and completeness (xor3_complete) are proved by an 8-way case analysis plus the boolean relations; the coefficients come from an exhaustive search over small-integer encodings. The 3-input majority has no such encoding (full-rank residual quadratic form), so Maj keeps the carry-save form. Constraint count per compression block drops from 27088 to 19920 (-26%); witness count is unchanged at 17688. Still pure R1CS, no lookups.
Replace the carry-save Maj arithmetization (two R1CS rows per output bit:
a witnessed majority plus a parity-booleanity check) with a single
constraint per bit, matching the existing 3-input XOR trick:
(o + a + b - 9c + 3)(a + b + 6c - 4) = -12
This is linear in the witnessed output o with multiplier a + b + 6c - 4,
whose boolean-cube values are +-2, +-3, +-4 and so never vanish for
char not in {2,3} (already guaranteed by p > 2^35). Its unique root is
exactly maj(a,b,c). No symmetric single-constraint encoding exists, so
the -9c/6c asymmetry is unavoidable.
Maj32 drops from 64 to 32 constraints; witnesses unchanged. CompressBlock
falls from 19920 to 17872 constraints (-2048, -10.3%).
The multi-operand modular adder hardcoded 3 carry bits regardless of the operand count n. The operand sum is < n*2^32, so its quotient by 2^32 is at most n-1 and fits in cw bits whenever n <= 2^cw. Parameterize the gadget by the carry width cw (with n <= 2^cw and 2^cw <= 8) and let each caller pick the minimal value: the round adds (n=6,7) keep cw=3, while the message schedule add (n=4) drops to cw=2. This saves one carry witness and one boolean constraint on each of the 48 schedule steps, taking the compression block from 17688 witnesses / 17872 constraints to 17640 / 17824. Soundness depends only on 2^cw <= 8 (bounding any carry the prover can supply, so the linear constraint still lifts to the naturals without wraparound); completeness uses n <= 2^cw to bit-decompose the honest carry.
The R1CS cost meter charged one constraint per `assert` without checking that the asserted expression is actually a single rank-1 row. A degree-3 polynomial or a sum of two products such as `a*b + c*d` would be miscounted as one constraint, when in fact it needs an auxiliary witness plus a second product row. Add a structural recognizer (`degree`, `r1csProducts`, `isR1CSRow`) that accepts an expression iff, along its `add` spine, every summand is affine plus at most one product of two affine forms -- exactly the `A*B - C` shape. `operationsCost` now aborts if any `assert` fails the check, so a non-row can never be silently charged as one constraint. Also add `checkCost` to pin the exact witness/constraint/lookup triple (e.g. `lookups := 0` to lock in pure R1CS), and example evals covering the valid shapes and the rejected `a*b + c*d` / degree-3 cases.
Author
|
Btw, should this go in Clean or should we open a separate repo for a "circuit library"? |
Collaborator
|
@rot256 I think it should go in the clean repo, I like the monorepo style |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Who would win?
I got Claude to optimize (for R1CS) the verified implementation of SHA-256, that @gio54321 created. After a few rounds of
\goal Optimize the SHA-256 compression. Do not change the spec. Consider using cvc5 and Sagemaththe result is this PR. The primary tricks he came up with where:Instead of doing
AddMod32on separate operands, he simply adds multiple things unreduced over the field, then witnesses the carry bits and bit decomposition for the result.The other big win was the following two R1CS relations:
(o + 2a + 2b + 7c) * (a + b − 4c + 1) = 6a + 6b − 24c: XOR3, 3-way XOR in a single constraint.(o + a + b − 9c + 3) * (a + b + 6c − 4) = −12: MAJ3, majority gate in a single constraint.Which he discovered using Gröbner basis.
I haven't really looked at the code in detail, but the neat trick is that I don't have to: he did not change the spec and the proof passes, so he (Claude) could not possibly screw this up, so ¯\(ツ)/¯
Here is a table of different implementations that I / "Deep Research" could find:
In other words, this formally verified impl is SOTA, and by quite a margin.