formal: the statement records are the circuit inputs, projected off the proof

[martyall]

Stacked on #378 (which is stacked on #377).

The fixture drivers fed the pickles gadgets through flat cell bundles (FopInput, GroupStepInput, …): every layout spelled twice, offset arithmetic in three places, and a proof reaching a gadget through a vector that was neither its wire form nor the gadget's record. The gadget records could not be the input type because their cell type was hard-wired to FVar F and their round-indexed fields were Lists.

The records

Three commits.

1. The records are polymorphic in their cell type and indexed by their sizes. PlonkInCircuit f sf, DeferredValues k f sf, UnfinalizedProof k f bc sf, the wrap statement family, AllEvals f, PlonkClaims f, IvpInput k f bc sf, BulletproofOpening k f sf, CheckBulletproofInput k f sf: f is a field element in a value and FVar F in a circuit (PureScript's letter; F stays the field), bc the boolean cell, and the round challenges, (L, R) pairs and mask are Vectors at their static sizes — PureScript's shape. Use sites say (FVar F) (BoolVar F) where they said F; no gadget or proof changed beyond .toList where a list is consumed, and GroupHalf carries the round index its claims have. Pickles.Encoding derives every record's CircuitType from its product decomposition, with the reading lemmas the gate demands.
2. The fop lanes run on StepFop k/WrapFop k, products of the gadgets' records; the driver projects them off the wrap statement and the checked proof. FopInput.lean is gone; the flat 151/148 harnesses stay for the dump comparison, which is byte-level against those layouts.
3. The group halves likewise: the step statement packs too (StepStatement.packed, its x_hat walk, beside WrapStatement.packed, with a boolean packed kind and packLeavesOf shared), StepGroup/WrapGroup are products of the statements, the unfinalized proof, IvpProof (a proof's commitments and opening, sized) and the sg_old points; ivpInputOf lays them out as the gadget's input with the key as constants. The wrap side reads its keep bits off the branch data and its booleanity checks off the packing. Group.lean loses its two bundles and their projections; the driver unpacks each statement once (wrapStatementOf, stepStatementOf) and every lane projects off them.

Not done

IvpInput's commitment lists stay List (the batch-order proofs use them at ~330 sites), so the group half's proof part is the sized tuple IvpProof beside the record rather than the record itself. Layout.lean's offset readers and Fop.lean's flat harnesses stay for check_cs.

Verified

Full build, check-cs (54 circuits), check-halves 37/37 on the records, dead-code, readings, shake on the CI list, runLinter on Pickles and PicklesFixture, style (the three long carry-lane lines belong to #378).

🤖 Generated with Claude Code

[greptile-apps]

Your trial has ended. Reactivate Greptile to resume code reviews.