Add property-based tests for the IVC pure helpers

[jpraynaud]

Why

proptest is established in halo2_snark (eligibility, clerk, message encoding) but absent from halo2_ivc_snark, despite several pure helpers with clear invariants.

What

Add proptest suites in the fast tier for the pure helpers and codecs. Case counts start at 100 for the byte-level and classification properties and stay low where a case decodes a verifying key; each target is measured as it lands, so the counts come from data rather than convention. Where a generated domain reaches an important case only by chance — an epoch pair that happens to be adjacent, a repeated name — that case is constructed rather than sampled. Per-helper scope and rationale are in the comment below.

How

Paths are relative to mithril-stm/src/.

• Accumulator and MSM byte codec (circuits/halo2_ivc/io.rs): round-trips preserve every component over arbitrary counts, fixed-base maps and key strings, and consume the whole encoding
• Preimage accessor range isolation (circuits/halo2_ivc/types.rs): each accessor decodes its own range, and is unchanged when every byte outside that range is altered
• Rigid preimage assembly (circuits/halo2_ivc/protocol_message.rs, circuits/halo2_ivc/types.rs): a preimage built from arbitrary inputs decodes back to them, and its whole 190-byte layout matches expectations computed from those inputs rather than from the helpers under test
• build_next_state (proof_system/halo2_ivc_snark/prover_input_helpers.rs): all seven next-state fields taken from their declared source, for both transition types on the same generated inputs, with step counters spanning the 32-bit boundary
• Epoch transition classification (proof_system/halo2_ivc_snark/rolling_state.rs): same-epoch, next-epoch and both gap directions constructed for each generated epoch, with the typed error payloads, plus deterministic (MAX - 1, MAX) and (MAX, MAX) cases for the overflow precedence
• Protocol parameter promotion guard (proof_system/halo2_ivc_snark/rolling_state.rs): a truth table over step counter, transition type, and whether the two parameter fields hold equal field values
• Aggregate verification key codec (proof_system/halo2_snark/aggregate_key.rs): legacy to CBOR preservation, a forced CBOR-version-byte root, and one property pairing the rigid slot layout with rejection of any decoded root that is not 32 bytes
• Input message matching (proof_system/halo2_ivc_snark/proof.rs): raw, lowercase, uppercase and mixed hex encodings of the same message are accepted, a message reducing to a different field element is rejected in every one of those forms, and malformed encodings are covered by a small example table
• State::as_public_input (circuits/halo2_ivc/state.rs): every field value at its row over full-width integers, with the four {0, MAX} boundary pairs
• trivial_accumulator (circuits/halo2_ivc/accumulator.rs): each distinct name once with a zero scalar, duplicates collapsed, empty left side, over a name pool small enough that duplicates actually occur
• Fixed-base availability guards (circuits/halo2_ivc/accumulator.rs): a name missing from either accumulator side is reported, and a correct label mapped to a different point is rejected
• IvcRollingState serde round-trip (proof_system/halo2_ivc_snark/rolling_state.rs, through AncillaryProverData): state values, proof bytes, accumulator components and signature compared field by field over non-genesis values
• IvcVerifierData (proof_system/halo2_ivc_snark/verifier_setup.rs): reject input without the CBOR version prefix, and preserve a nonzero genesis message
• MessageHash::try_from(&ProtocolMessagePreimage) (circuits/halo2_ivc/types.rs): the result is the field reduction of SHA-256 over all 190 input bytes, pinned by independently computed vectors
• Assess the gain and report it in the issue, with the measured per-case cost and the chosen case counts

[hjeljeli32]

Dear @jpraynaud @damrobi

Proposed coverage

Helper or codec	Covered today	What a property adds
Rigid preimage assembly against the preimage accessors — halo2_ivc/protocol_message.rs, halo2_ivc/types.rs	Nine examples, all from one value tuple: a zero aggregate-key root, stake 1, epoch 42	Builder offsets and decoder ranges must agree, and today they are shown to agree at a single point. The root and its pad are 36 consecutive zero bytes in every example, so nothing pins the root's placement inside the slot. Note the builder is #[cfg(test)] since #3385 withdrew its public entry point, so this ties the production decoder to a test-only assembly of the same layout; it does not close the three-copy parity gap
Preimage accessor range isolation — halo2_ivc/types.rs	Five examples: the three ranges, the zero preimage, a maximum-value reduction	No test shows an accessor ignores bytes outside its own range
build_next_state field selection — halo2_ivc_snark/prover_input_helpers.rs	Five examples, one value tuple each; the full field plumbing is asserted for one transition type only	The function selects, per output field, between the rolling state and the protocol message. States that rule instead of sampling it, for both transition types on the same inputs, and at step counters either side of the 32-bit boundary
Accumulator and MSM byte codec — halo2_ivc/io.rs	One asset-derived round-trip and two golden files: one shape, one value	Hand-written length-prefixed codec on a public deserialization path. Arbitrary counts, maps, and empty or multi-byte keys are unexercised
Epoch-transition classification — halo2_ivc_snark/rolling_state.rs	Eight examples. The only rejection case reaching classification uses last epoch 3 against incoming 10; the backward pair that exists is intercepted by the overflow check before it classifies	Pins same, next and both gap directions with their typed error payloads, and whether overflow outranks a same-epoch certificate. The epoch relations are constructed per generated epoch rather than sampled: independent random pairs are equal or adjacent with probability about 2⁻⁶⁴, so a naive generator would only ever exercise gaps
Protocol parameter promotion guard — halo2_ivc_snark/rolling_state.rs	Two asset-driven integration cases, same-epoch and next-epoch	A direct truth table over step counter, transition type, and whether the two parameter fields hold equal field values, including unequal values that share their low limbs
Aggregate verification key codec — halo2_snark/aggregate_key.rs	Five examples, including three goldens and one legacy root beginning with the CBOR version byte	Generalises the CBOR and legacy fallback across roots and stakes, and pairs the rigid slot layout with rejection of a decoded root that is not 32 bytes. The width has to be judged on the decoded root, not the input length: a 40-byte legacy-looking input can decode to an empty root, and a valid CBOR key need not be 40 bytes
Input-message matching — halo2_ivc_snark/proof.rs	Two examples: one stored message and a corrupted copy, both raw	The hex branch has no test at all. Acceptance and typed rejection are both needed and in every encoding — raw, lowercase, uppercase, mixed — since an implementation that returned early after decoding hex would satisfy any positive-only equivalence check while accepting an unrelated message
State::as_public_input — halo2_ivc/state.rs	Three tests pin the field order, one asserting the sentinel set equals StateField::ALL	The order is pinned, but the values are narrow: the examples use 1 to 7 and 11 to 77, so the step counter and epoch are never seen at full width and u64::MAX never appears. Adds full-width integers with the {0, MAX} boundary pairs, and independently varied values for the other five fields
trivial_accumulator — halo2_ivc/accumulator.rs	Encoding length pinned at zero against three names; production compatibility pinned against the committed genesis asset	Arbitrary name counts, and duplicate names collapsing in the BTreeMap, which is untested. Names are drawn from a small pool so duplicates actually occur
Fixed-base availability guards — halo2_ivc/accumulator.rs	Two examples, both built on a trivial accumulator, whose left side carries no names	These guards run ahead of library calls that panic rather than return. Neither a name missing from the left side nor a correct label mapped to a different point is covered today
MessageHash::try_from(&ProtocolMessagePreimage) — halo2_ivc/types.rs	None directly; added by #3516 and exercised only through its four call sites in off_circuit_checker.rs and proof.rs	States the contract exactly — the field reduction of SHA-256 over all 190 bytes — with independently computed vectors so the expectation does not come from the conversion under test
IvcRollingState serde round-trip — halo2_ivc_snark/rolling_state.rs	One round-trip, of the genesis state only: zero fields, empty proof bytes, trivial accumulator, and the oracle is re-serialized byte equality	Every non-trivial field is unexercised — arbitrary state values, non-empty proof bytes of varying length, both accumulator sides populated — and the restored components are compared directly rather than through their bytes
IvcVerifierData round-trip — halo2_ivc_snark/verifier_setup.rs	Four guards, all using MessageHash::ZERO (#3513 added the fourth)	A nonzero genesis message. The narrowest of the set: the two verifying keys are fixed by the stored asset, so the message is the only input that varies, and every case decodes both keys. Kept deterministic for that reason

Two branches are covered by plain examples rather than properties, since each is a single point: IvcVerifierData::from_bytes rejecting input with no CBOR version prefix, which is untested today, and the (u64::MAX, u64::MAX) epoch pair, which settles whether the overflow check outranks a same-epoch certificate.

On case counts

The ticket suggests 10 to 20 cases. Having looked at the existing suites I would go higher for most of these. The closest precedent is membership_commitment/merkle_tree/tree.rs, which runs three 100-case properties in the fast tier, completing in roughly 0.07 s to 0.5 s. Against that, capping pure byte-manipulation properties at 10 to 20 covers far less range than the cost justifies. (The crate also has a 300-case property, but it is inside mod slow, so it shows large runs are permitted rather than that they belong in the fast tier.)

Proposal: 100 or more for the byte-level and classification properties, and low counts only where a case decodes a verifying key. Each target is measured as it lands, so the count is chosen from data rather than convention.

Everything stays in the fast tier with bounded inputs. No proving, key generation, SRS or asset regeneration.

[hjeljeli32]

@jpraynaud @damrobi

1 — Accumulator and MSM wire format (circuits/halo2_ivc/io.rs)

Background. An MSM is a list of inline (point, scalar) pairs plus a map of scalars held by name, resolved later against the verifying key's fixed bases. An accumulator is two of them, lhs and rhs.

Covered today. The three existing tests exercise two committed shapes. lhs is one inline pair with no named scalars in both; rhs is either 51 pairs with 64 named scalars, or one pair with 96. Every name is nonempty ASCII.

Property	Invariant	Status
msm_round_trip_preserves_every_component	read(write(m)) returns the same points, scalars and named-scalar map, and consumes exactly the encoding	passes
accumulator_round_trip_preserves_both_sides	The same per side, with the side lengths forced apart so a swapped lhs/rhs fails	passes
a_truncated_encoding_is_rejected	Every strict prefix of a valid MSM encoding returns an error	ignored — panics
mismatched_point_and_scalar_counts_are_rejected	An encoding declaring different point and scalar counts returns an error	ignored — panics

Generated inputs. 0 to 4 inline pairs over four distinct non-identity points, 0 to 8 named entries with empty, ASCII and multi-byte names. 100 cases, fast tier.

Three defects, all in the reader. The route from AncillaryProverData::from_bytes exists under future_snark; the byte counts below are inner MSM payloads, which a public input reaches wrapped in the ancillary-data CBOR envelope.

1. A truncated point payload panics rather than returning an error — the unchecked point reader calls expect on a short read (midnight-curves, bls12_381/g1.rs:442). Four bytes declaring one point and supplying none are enough.
2. Point and scalar counts are decoded independently and passed to a constructor that asserts they are equal (midnight-circuits, verifier/msm.rs:88), so a mismatch panics. Proptest shrank this to zero points and one scalar, a 44-byte input.
3. A key length prefix is unvalidated, so a 16-byte input can request roughly 4 GiB before discovering the payload is absent.

The first two are recorded as ignored properties that assert rejection; enable them after fixing the decoder. The third needs a resource contract first: an error-only oracle cannot distinguish early rejection from rejection after an excessive allocation. I would put all three in one codec-hardening follow-up.

Cost. About 0.01 s each at 100 cases.

[hjeljeli32]

2 — Preimage accessor ranges (circuits/halo2_ivc/types.rs)

Background. Three accessors read the epoch at 182..190, the announced Merkle tree commitment at 69..101 and the announced protocol parameters at 137..169 out of the 190-byte protocol message preimage.

Covered today. Five direct accessor examples, each starting from a zeroed array and populating at most one range. In all five, the 118 bytes outside all three ranges stay zero — so an accessor that read its own range and also mixed in a byte from outside would satisfy every one of them.

Property	Invariant	Status
each_accessor_decodes_only_its_own_range	Over arbitrary 190-byte arrays, each accessor equals the direct decode of its own range	passes
flipping_every_byte_outside_a_range_leaves_that_accessor_unchanged	XORing every byte outside a range with the same nonzero mask preserves that accessor's output	passes

Generated inputs. Arbitrary 190-byte arrays and a nonzero mask, so every byte outside the range under test changes while the range itself is untouched. 100 cases, fast tier.

Both properties use the production range constants, so neither pins an absolute offset; the rigid-preimage layout tests in circuits/halo2_ivc/tests/encoding/positive.rs already assert those constants equal 69..101, 137..169 and 182..190.

The two are complementary rather than redundant. The mask property alone cannot see a defect that depends on exterior bytes in a way the shared mask cancels — reading bytes[0] ^ bytes[1], for instance, is unchanged when both are flipped by the same mask. The direct-decode property catches that.

Cost. 13 ms and 10 ms at 100 cases.

[hjeljeli32]

3 — Rigid preimage assembly (circuits/halo2_ivc/protocol_message.rs, circuits/halo2_ivc/types.rs)

Background. The builder assembles the 190-byte preimage by walking a cursor over four labels and the four value slots between them. The circuit hashes the whole array, but only three slots are decoded back out, through absolute range constants. Writer and reader are independent, and nothing forces the two to agree.

Covered today. Nine examples, all from one fixture: a zero aggregate key root, stake 1, parameters [7; 32], epoch 42. The root and its four-byte pad are 36 consecutive zero bytes, and seven of the eight epoch bytes and seven of the eight stake bytes are zero — so a slot losing its high bytes leaves no trace.

Test	Invariant	Status
a_rigid_preimage_carries_every_value_at_its_literal_offset	Over generated inputs, all 190 bytes match expectations computed from those inputs — four labels, the dynamic hash, the root, the zero pad, the little-endian stake, the parameters, the little-endian epoch	passes
a_rigid_preimage_decodes_back_to_the_values_it_was_built_from	The three accessors return the values the builder was given, on the same array	passes
preimage_range_constants_match_their_literal_ranges	Deterministic: the three range constants equal their literal ranges, so the reader offsets stay pinned whatever a run generates	passes

Generated inputs. The snapshot digest takes one of four shapes — absent, present but empty, a 64-character hex string, or one to 32 characters including multi-byte ones; absence and emptiness hash differently, since one hashes nothing and the other the key spelling. Stake and epoch are full-width, parameters arbitrary, and the aggregate key root avoids the CBOR version byte, which belongs to the aggregate key codec item. 100 cases each, fast tier.

Every expectation is recomputed from the generated inputs, never read back from the builder or the projection helper it called.

Cost. 7.4 ms and 7.1 ms at 100 cases.

[hjeljeli32]

4 — build_next_state (proof_system/halo2_ivc_snark/prover_input_helpers.rs)

Background. The helper assembles the next state from the rolling state, the two certificate arguments and the protocol message preimage. Its job is choosing, per output field, which source the value comes from; only protocol_parameters depends on the transition type.

Covered today. Five examples. All seven fields are asserted in one of them, under NextEpoch only; the same-epoch examples assert the parameters, the counter and the typed overflow. Every counter is small apart from the overflow case.

Property	Invariant	Status
every_next_state_field_comes_from_its_declared_source	Each of the seven output fields equals its declared source, for both transition types on the same generated tuple	passes

Generated inputs. Twelve: a rolling state built field by field, two certificate values, and the preimage's epoch and two 32-byte slots — each varied independently, so a wrong choice is not masked by two sources holding the same value. Step counters span small values, the 32-bit boundary and the last advanceable value. 100 cases, fast tier.

Expectations are computed from the generated bytes, not from the preimage accessors, which would only restate that the helper calls them.

Cost. 7.1 ms at 100 cases.

[hjeljeli32]

5 — Epoch transition classification (proof_system/halo2_ivc_snark/rolling_state.rs)

Background. validate_transition checks overflow first, then lets the relation between the last committed epoch and the incoming certificate's epoch select the branch — equal is same-epoch, exactly one greater is next-epoch, anything else is a gap — and only then applies that branch's state guards.

Covered today. Eight examples. Only one pair reaches the gap branch, (3, 10), and it is forward. The one backward pair, (MAX, 4), is intercepted by the overflow check before classification, so nothing exercises how a certificate from an earlier epoch is classified.

Property	Invariant	Status
the_epoch_relation_selects_the_transition	For a generated last committed epoch: the equal epoch classifies as same-epoch, one greater as next-epoch, and four rejected epochs — the two nearest on either side plus a sampled backward and forward one — each carry the typed gap error with both payloads	passes

Two deterministic examples cover boundaries a sampled epoch would miss: (MAX - 1, MAX) still advances, and (MAX, MAX) is rejected as an overflow — the existing maximum example only shows overflow outranking a gap, not a same-epoch certificate.

Generated inputs. One epoch below the maximum, with a backward and a forward offset drawn from the range each admits. Every relation is constructed from that epoch rather than sampled, because a uniform pair of u64 values rarely lands on any of the relations that matter. The two nearest rejected epochs are forced for the same reason at a smaller scale: sampling a distance almost never picks one behind or two ahead, which is exactly where an off-by-one acceptance would sit. 100 cases, fast tier.

Cost. 7.0 ms at 100 cases.

[hjeljeli32]

6 — Protocol parameter promotion guard (proof_system/halo2_ivc_snark/rolling_state.rs)

Background. assert_protocol_parameters_unchanged rejects a step only when three conditions hold together: the state is past genesis, the transition is next-epoch, and the two protocol parameter fields hold different field values. A same-epoch step never consumes the lookahead, so a chain already carrying a divergence can finish the epoch it appeared in; only the promotion into a new epoch is rejected.

Covered today. No direct test. Four asset-driven checker cases reach the guard, all at step counter 4, with the committed state carrying equal parameters and the divergence fixture changing one of them. Neither the genesis exemption nor the precision of the comparison is pinned.

Property	Invariant	Status
only_a_next_epoch_step_past_genesis_with_diverged_parameters_is_rejected	Over generated parameter pairs, the guard rejects exactly the combinations where all three conditions hold, with the typed error, across both transition types at step counters 0, 1 and a generated one	passes

Generated inputs. A parameter pair in one of three shapes: equal, two independent values, or two canonical values sharing every byte but the last. The third is forced because a comparison narrowed to the low 64 bits would call such a pair equal and promote a changed parameter; two independent arrays reach that shape with negligible probability. Step counter 1 is forced for the same reason — the neighbouring is_not_first_step means greater than one, so a guard reaching for it by mistake would exempt the first step past genesis, which a sampled counter never visits. 100 cases, fast tier.

Equality is compared on the reduced field values the wrapper holds, since distinct byte arrays can reduce to the same element.

Cost. 7.0 ms at 100 cases.