chore: transcript+codec+poseidon2 fixes#19419
chore: transcript+codec+poseidon2 fixes#19419iakovenkos merged 26 commits intomerge-train/barretenbergfrom
Conversation
| EXPECT_TRUE(CircuitChecker::check(builder)); | ||
| } | ||
|
|
||
| /** |
barretenberg/cpp/src/barretenberg/stdlib/hash/poseidon2/poseidon2.test.cpp
Show resolved
Hide resolved
suyash67
left a comment
There was a problem hiding this comment.
Looks good. Thanks for adding the codec readme, its very useful!
| // Cases 2 and 3: a bigfield/goblin_field element is reconstructed from low and high limbs. | ||
| } else if constexpr (IsAnyOf<T, bigfield_ct>) { | ||
| // Case 2: bigfield is reconstructed from low and high limbs with in-field validation. | ||
| // This ensures aliased values (>= Fq::modulus) are rejected. |
| |---------|-------|--------|----------------| | ||
| | **Native** | All | `for each limb: if (limb != 0) return false` | Direct limb-by-limb zero check. | | ||
| | **Circuit** | BN254 | `sum(limbs) == 0` | Sum of 4 valid limbs (2×136-bit + 2×118-bit) ≤ 2^138, cannot wrap to 0 mod Fr (254 bits). Only all-zero limbs satisfy this. | | ||
| | **Circuit** | Grumpkin | `x² + 5y² == 0` | Equation `x² = -5y²` requires -5 to be a quadratic residue. Since -5 is not a square mod p, only `(0,0)` satisfies this. | |
| return (fr::accumulate(std::vector<fr>(fr_vec.begin(), fr_vec.end())).is_zero()); | ||
| } else { | ||
| // For Grumpkin infinity check: verify that Fr modulus p ≡ 2 mod 5 | ||
| static_assert(bb::fr::modulus % 5 == 2, "Grumpkin infinity check requires Fr modulus p ≡ 2 mod 5"); |
There was a problem hiding this comment.
@arielgabizon + added compile-time check
There was a problem hiding this comment.
umm is this the right check? I thought it was p-1 =1 mod 4. Is this equivalent?
There was a problem hiding this comment.
i updated the condition to check
There was a problem hiding this comment.
But it looks like you're checking is 2 mod 5 - not 2 or 3.
Besides qr says (p/5)(5/p)= -1^((p-1)/2).
So I'm not sure it's equivalent to p being non-residue mod 5
(which seems to be what you're implying)
There was a problem hiding this comment.
This points to an outdated code snippet, you'd need to go to the diff to see the current state
You're missing (5-1)/2 in the exponent -- we have
There was a problem hiding this comment.
I think it's (p/5)(5/p)= -1^((p-1)/2) * -1^((5-1)/2) = -1^((p-1)/2).
There was a problem hiding this comment.
nvm - I got the qr formula wrong, this looks good!
|
|
||
| | Codec | Enforcement | Method | | ||
| |-------|-------------|--------| | ||
| | `FrCodec` | Native assertion | `BB_ASSERT_LT(value, fq::modulus)` | |
…i/transcript-post-audit-fixes
…i/transcript-post-audit-fixes
| transcript->add_element_frs_to_hash_buffer(derived_label, proof_span.subspan(proof_idx, num_frs_comm)); | ||
| proof_idx += num_frs_comm; | ||
| [[maybe_unused]] auto _ = | ||
| transcript->template receive_from_prover<GoblinStdlibProofCommitment>(derived_label); |
There was a problem hiding this comment.
Why is this Goblin while the previous isn't?
Flakey Tests🤖 says: This CI run detected 2 tests that failed, but were tolerated due to a .test_patterns.yml entry. |
BEGIN_COMMIT_OVERRIDE feat: support JSON input files for bb verify command (#19800) fix: update bootstrap.sh to use new JSON field names chore: Update `index.js` so that `HAS_ZK` and `PUBLIC_INPUTS` variables must always be set in tests (#19884) chore: pippenger int audit (#19302) chore: deduplicate batch affine addition trick (#19788) chore: transcript+codec+poseidon2 fixes (#19419) chore!: explicitly constrain inputs and intermediate witnesses (#19826) fix: exclude nlohmann/json from WASM builds in json_output.hpp chore: translator circuit builder and flavor audit (#19798) Revert "fix: exclude nlohmann/json from WASM builds in json_output.hpp" Revert "feat: support JSON input files for bb verify command (#19800)" Revert "fix: update bootstrap.sh to use new JSON field names" END_COMMIT_OVERRIDE
### Summary This PR addresses findings from the external audit of the Transcript and Poseidon2 components. The changes ensure consistent behavior between native and in-circuit verification, particularly around field element serialization/deserialization. #### 1. Field Element Serialization/Deserialization (Issues 5, 6, 9, 10, 11) Problem: Inconsistent handling of field elements during serialization, particularly around edge cases involving the field modulus and aliased values. - `validate_split_in_field_unsafe` now properly rejects `hi||lo == field_modulus` (Issue 5) - Replaced hardcoded $254$ with generically calculated `max_bits` (Issue 6) - Added proper borrow boolean check even when `lo` is constant (Issue 10) - Unified deserialization behavior: both `FrCodec` (native) and `StdlibCodec` (in-circuit) now use `assert_is_in_field()` to reject unreduced values (Issues 9 & 11) - For `Mega` arithmetization, validation is deferred to `Translator+ECCVM`; for `Ultra`, strict validation happens immediately via `bigfield` #### 2. Transcript Round Tracking (Issues 3, 4) - Removed redundant `round_number` field, now using only `round_index` (Issue 4) - Consecutive challenges with no data between them now stay in the same round - `prover_init_empty` and `verifier_init_empty` are now properly marked as testing methods (Issue 3) #### 3. Poseidon2 Cleanup (Issues 1, 2, 7, 8) Strategy: - Not marking the first element of the sponge state as `used`. - Added documentation for $-1$ offset in `internal_matrix_diagonal` (Issue 2) - Removed unnecessary normalization assert in `matrix_multiplication_external` (Issue 7) - Fixed transcript initialization in circuit failure tests (Issue 8) --- #### Commits: - Issue 1 (68011cc): First element of of `FieldSponge::hash_internal` is **not** marked as used - Issue 2 (2dd4197): Missing annotation about $-1$ offset in poseidon2 `internal_matrix_diagonal` - Issue 3 (1dddf54): `prover_init_empty` and `verifier_init_empty` are testing methods - Issue 4 (ced1a88): `round_number` is redundant with `round_index` - Issues 5 & 6 (e4fa3c5): `validate_split_in_field_unsafe` accepts `hi||lo == modulus` + hardcoded $254$ - Issue 7 (dd1f644): Unnecessary assert for matrix_multiplication_external output normalization - Issue 8 (d064598): Verification in poseidon2.circuit.failure.test.cpp fails on valid input - Issues 9 & 11 (7f1cb65): `deserialize_from_fields` rejects unreduced `fq`s + (fq_modulus, fq_modulus) handling - Issue 10 (98178c5): `validate_split_in_field_unsafe` skips borrow check when `lo` is constant --- #### Documentation Added barretenberg/cpp/src/barretenberg/stdlib/primitives/field/CODEC_README.md documenting: - Codec architecture (FrCodec, StdlibCodec, U256Codec) - Field element encoding (2-limb representation for fq) - Canonical representation requirements and point at infinity handling - Ultra vs Mega arithmetization differences - Threat model: why native/recursive consistency matters - Mega/Goblin deferred validation flow and ECCVM↔Translator translation check --- #### New Tests field_utils.test.cpp (new file): - ValidateSplitRejectsModulus — Issue 5: split rejects hi||lo == modulus - ValidateSplitAcceptsModulusMinusOne — edge case: modulus - 1 is valid - SplitUniqueRejectsModulus — Issue 5: unique split rejects modulus - SplitUniqueMaxValue — edge case handling - ValidateSplitConstantLoWitnessHiRejectsModulus — Issue 10: constant lo with witness hi - ValidateSplitWitnessLoConstantHiRejectsModulus — Issue 10: witness lo with constant hi field_conversion.test.cpp: - BigfieldDeserializationFailsOnLimbOverflow — limb bounds validation - BothCodecsRejectPointAtInfinityAlias — Issue 11: aliased infinity rejected - BothCodecsAcceptCanonicalRejectAlias — Issues 9, 11: native/circuit consistency - AcceptCanonicalPointAtInfinity — canonical infinity accepted - RejectPointNotOnCurve — off-curve points rejected poseidon2.test.cpp: - PointCoordinatesVsAliasProduceDifferentHashes — aliased coords produce different hashes poseidon2.circuit.failure.test.cpp: - ValidCircuitVerifies — Issue 8: baseline validity check
Summary
This PR addresses findings from the external audit of the Transcript and Poseidon2 components. The changes ensure consistent behavior between native and in-circuit verification, particularly around field element serialization/deserialization.
1. Field Element Serialization/Deserialization (Issues 5, 6, 9, 10, 11)
Problem: Inconsistent handling of field elements during serialization, particularly around edge cases involving the field modulus and aliased values.
validate_split_in_field_unsafenow properly rejectshi||lo == field_modulus(Issue 5)max_bits(Issue 6)lois constant (Issue 10)FrCodec(native) andStdlibCodec(in-circuit) now useassert_is_in_field()to reject unreduced values (Issues 9 & 11)Megaarithmetization, validation is deferred toTranslator+ECCVM; forUltra, strict validation happens immediately viabigfield2. Transcript Round Tracking (Issues 3, 4)
round_numberfield, now using onlyround_index(Issue 4)prover_init_emptyandverifier_init_emptyare now properly marked as testing methods (Issue 3)3. Poseidon2 Cleanup (Issues 1, 2, 7, 8)
Strategy:
used.internal_matrix_diagonal(Issue 2)matrix_multiplication_external(Issue 7)Commits:
FieldSponge::hash_internalis not marked as usedinternal_matrix_diagonalprover_init_emptyandverifier_init_emptyare testing methodsround_numberis redundant withround_indexvalidate_split_in_field_unsafeacceptshi||lo == modulus+ hardcodeddeserialize_from_fieldsrejects unreducedfqs + (fq_modulus, fq_modulus) handlingvalidate_split_in_field_unsafeskips borrow check whenlois constantDocumentation
Added barretenberg/cpp/src/barretenberg/stdlib/primitives/field/CODEC_README.md documenting:
New Tests
field_utils.test.cpp (new file):
field_conversion.test.cpp:
poseidon2.test.cpp:
poseidon2.circuit.failure.test.cpp: