test(stm): add property tests for the IVC pure helpers

[hjeljeli32]

Content

proptest is established in halo2_snark but absent from halo2_ivc_snark, whose helpers and hand-written codecs are covered by examples driven by single fixtures that hide what the helper could get wrong: every rigid-preimage test runs on a zero aggregate key root with stake 1 and epoch 42, so seven of eight bytes in each integer slot are zero. This adds twelve properties across seven helpers, retires twelve examples a property subsumes, and costs 7.0 to 7.4 ms per property at 100 cases — some 6.9 ms of that process launch, so a few milliseconds inside the shared fast-tier process.

The properties found four defects in the two byte decoders, all fixed here because each fix turned out small: one commit apiece, directly after the test that found it. Nothing is left ignored.

Changes

• Decoder fixes (io.rs, aggregate_key.rs): mismatched point and scalar counts are rejected before reaching a constructor that asserts they agree; a fixed-base key length is read through take into a growing buffer, so an overstated prefix cannot size an allocation; a truncated point payload is gathered with read_exact first, using byte_length::<EmulatedCurve>(format) so no width is hardcoded and point validation is unchanged; and the legacy aggregate key decoder constructs its commitment directly instead of asking it to re-detect a format already classified, which had let a CBOR-shaped root decode to an empty one.
• Byte-level codecs (io.rs, types.rs, aggregate_key.rs): MSM and accumulator round trips preserve every component over arbitrary counts and key strings and consume the whole encoding; each preimage accessor equals the direct decode of its own range and ignores everything outside it; legacy aggregate keys survive the CBOR round trip on both paths, the fallback property constraining the byte after the version prefix since the prefix only selects the branch.
• Rigid preimage layout (protocol_message.rs, tests/encoding/positive.rs): all 190 bytes match expectations computed from the generated inputs, and the same array decodes back through the accessors, with the dynamic digest recomputed independently so the builder is not its own oracle. A deterministic test pins the range constants to literal ranges, which the accessor properties cannot do because they index through them.
• State transition helpers (prover_input_helpers.rs, rolling_state.rs): each next-state field equals its declared source under both transition types on the same tuple; the epoch relation selects same-epoch, next-epoch and both gap directions with typed payloads; the promotion guard rejects exactly the combinations where all three of its conditions hold.
• Constructed, not sampled: two independent u64 epochs are equal or adjacent with probability about 2⁻⁶⁴, and a nonzero step counter almost never lands on 1, so every boundary deciding a branch is forced — including a parameter pair sharing all but its last byte, which a comparison narrowed to the low 64 bits would call equal.
• Retired examples (tests/encoding/positive.rs, prover_input_helpers.rs): twelve single-fixture examples a property now covers over a value space, plus four helpers left without callers. The dynamic-digest example is kept — its 64-character hex value is the shape production sends, guaranteed every run rather than sampled.
• Not covered: the truncation fix addresses a short payload, not every malformed unchecked point, since read_raw_unchecked carries a second panic on the decode result. The allocation fix has no test observing allocation — the old code returned the same error once its allocation succeeded — so that rests on inspection.

Pre-submit checklist

• Branch
  • Tests are provided (if possible)
  • Crates versions are updated (if relevant)
  • CHANGELOG file is updated (if relevant)
  • Commit sequence broadly makes sense
  • Key commits have useful messages
• PR
  • All check jobs of the CI have succeeded
  • Self-reviewed the diff
  • Useful pull request description
  • Reviewer requested
• Documentation
  • No new TODOs introduced

Comments

Draft: seven of the helpers on the issue are covered, the rest follow.

Issue(s)

Relates to #3469

[github-actions]

Test Results

     5 files  ± 0     221 suites  ±0   1h 38m 34s ⏱️ - 1m 22s
 3 613 tests  - 24   3 613 ✅  - 24  0 💤 ±0  0 ❌ ±0 
11 741 runs   - 27  11 741 ✅  - 27  0 💤 ±0  0 ❌ ±0 

Results for commit 87759ab. ± Comparison against base commit cccb650.

This pull request removes 44 and adds 20 tests. Note that renamed tests count towards both.

mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::index_out_of_bounds
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::index_too_large_for_circuit_range
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::indices_not_increasing
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::leaf_merkle_path_mismatch
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::leaf_swap_keep_merkle_path
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::leaf_wrong_verification_key
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::merkle_path_corrupt_sibling
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::merkle_path_flip_position
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::merkle_path_length_long
mithril-stm ‑ circuits::halo2::tests::golden::cases::negative::slow::merkle_path_length_short
…

mithril-stm ‑ circuits::halo2_ivc::io::tests::a_declared_point_with_no_payload_is_rejected
mithril-stm ‑ circuits::halo2_ivc::io::tests::a_fixed_base_key_longer_than_the_input_is_rejected
mithril-stm ‑ circuits::halo2_ivc::io::tests::a_truncated_encoding_is_rejected
mithril-stm ‑ circuits::halo2_ivc::io::tests::accumulator_round_trip_preserves_both_sides
mithril-stm ‑ circuits::halo2_ivc::io::tests::mismatched_point_and_scalar_counts_are_rejected
mithril-stm ‑ circuits::halo2_ivc::io::tests::msm_round_trip_preserves_every_component
mithril-stm ‑ circuits::halo2_ivc::tests::encoding::positive::a_rigid_preimage_carries_every_value_at_its_literal_offset
mithril-stm ‑ circuits::halo2_ivc::tests::encoding::positive::a_rigid_preimage_decodes_back_to_the_values_it_was_built_from
mithril-stm ‑ circuits::halo2_ivc::tests::encoding::positive::preimage_range_constants_match_their_literal_ranges
mithril-stm ‑ circuits::halo2_ivc::types::protocol_message_preimage_tests::each_accessor_decodes_only_its_own_range
…

♻️ This comment has been updated with latest results.