Step ivp (#113)

* step ivp

* fix context clobbering in viz

Author: martyall

.claude/skills/kimchi-circuit-json-comparison/SKILL.md

@@ -142,6 +142,28 @@ describe "Kimchi gate matches" do
 npx spago test -p snarky-kimchi -- --example "CircuitJson"
 ```
 
+## Analysis Tools
+
+Two scripts in `tools/` help analyze circuit comparison results:
+
+### circuit-diff-summary.mjs
+Quick structural overview: gate counts, type breakdown, cached constants, first difference, section breakdown.
+
+```bash
+node tools/circuit-diff-summary.mjs packages/pickles-circuit-diffs/circuits/results/ivp_step_circuit.json
+```
+
+Use this FIRST to understand the shape of the diff (gate count mismatch? type mismatch? coefficient-only?).
+
+### circuit-r1cs-diff.mjs
+Unpacks Generic gates into individual R1CS constraints in generation order (right half = queued/first, left half = new/second) and finds the first divergence. Essential for diagnosing R1CS double-packing alignment issues where gate types match but coefficients differ.
+
+```bash
+node tools/circuit-r1cs-diff.mjs packages/pickles-circuit-diffs/circuits/results/ivp_step_circuit.json
+```
+
+The output shows the R1CS sequence side-by-side with decoded constraints, highlighting the first divergence. The divergent R1CS's constant coefficient often identifies which operation (seal, constant materialization, boolean check) is misplaced.
+
 ## Step 5: Iterate on Differences
 
 ### Extra boolean check constraints
@@ -165,6 +187,18 @@ OCaml may seal (reduce to single variable) inputs before passing to a gate. Chec
 
 **Seal at loop boundaries**: OCaml's `scale_fast_unpack` calls `seal base` once at the top, before the VarBaseMul loop. Without this, a complex CVar base point (e.g. from `groupMapCircuit`) gets re-reduced in every round, generating 2 extra GenericPlonk gates per round. PureScript's `varBaseMul` must `sealPoint base` before the loop.
 
+**Seal in sponge add_assign**: OCaml's sponge `add_assign` calls `Utils.seal` after every `state[i] += x`. PureScript's circuit sponge (`Snarky.Circuit.RandomOracle.Sponge.absorb`) must do the same. Without seal, complex CVars like `Add(Const 0, Var v)` accumulate in the sponge state and are only reduced during the Poseidon gate's `reduceToVariable` call. This changes the TIMING of R1CS generation: seal produces R1CS during absorption (as standalone `KimchiBasic` constraints), while deferred reduction produces R1CS inside the Poseidon `reduce`. The different timing shifts the R1CS double-packing alignment, causing every subsequent Generic gate's coefficient layout to differ from OCaml even though the same total R1CS exist. This is invisible in standalone sub-circuit tests (which start with an empty packing queue) and only manifests when composing sub-circuits (like the IVP).
+
+### R1CS double-packing alignment
+
+The Kimchi constraint system pairs consecutive R1CS constraints into a single Generic gate (2 R1CS per gate). The pending queue persists across ALL constraint types — non-Generic gates (Poseidon, CompleteAdd, VarBaseMul, etc.) do NOT flush the queue.
+
+This means: if any operation before a composed circuit boundary generates an ODD number of R1CS, all subsequent Generic gate coefficient layouts shift by one position. The circuits have the same gate kinds, same gate counts, same cached constants — but different coefficient pairings within Generic gates.
+
+**Diagnosis**: Extract R1CS in generation order by unpacking Generic gates (right half = first/queued, left half = second/new). Compare the two R1CS sequences to find the first divergence index. The diverging R1CS's constant coefficient often identifies which operation (seal, constant materialization, boolean check) is at the wrong position.
+
+**Prevention**: When translating OCaml code that modifies state with side effects (like sponge `add_assign`), check whether OCaml calls `seal` or `reduce_to_v` at that point. Missing a seal changes the R1CS generation timing.
+
 ### Different witness variable ordering
 
 If the gate structure matches but wires differ, the issue may be in the order variables are introduced via `exists`.

packages/pickles-circuit-diffs/test/Test/Pickles/CircuitDiffs/Main.purs

@@ -58,7 +58,7 @@ import Snarky.Curves.Pasta (PallasG, VestaG)
 import Snarky.Curves.Vesta as Vesta
 import Snarky.Data.EllipticCurve (AffinePoint)
 import Snarky.Types.Shifted (Type1(..))
-import Test.Spec (SpecT, beforeAll_, describe, it, pending)
+import Test.Spec (SpecT, beforeAll_, describe, it)
 import Test.Spec.Assertions (shouldEqual)
 import Test.Spec.Reporter.Console (consoleReporter)
 import Test.Spec.Runner.Node (runSpecAndExitProcess')
@@ -410,7 +410,6 @@ spec =
             { lagrangeComms: (coerce $ vestaSrsLagrangeCommitments stepSrs 16 30) :: Array (AffinePoint (F Fp))
             , blindingH: (coerce $ vestaSrsBlindingGenerator stepSrs) :: AffinePoint (F Fp)
             }
-        -- pending "xhat_step_circuit"
         exactMatch "xhat_step_circuit" (fromCompiledCircuit $ compileXhatStep stepSrsData)
       describe "Pickles Wrap sub-circuits" do
         exactMatch "finalize_other_proof_wrap_circuit" (fromCompiledCircuit compileFopWrap)
@@ -435,13 +434,13 @@ spec =
             }
         exactMatch "ivp_wrap_circuit" (fromCompiledCircuit $ compileIvpWrap wrapSrsData)
         let
-          stepSrs = pallasCrsCreate (2 `Int.pow` 16)
+          -- OCaml uses SRS.Fq.create (1 lsl 15) and domain Pow_2_roots_of_unity 15
+          stepSrs = pallasCrsCreate (2 `Int.pow` 15)
           stepSrsData =
-            { lagrangeComms: (coerce $ vestaSrsLagrangeCommitments stepSrs 16 175) :: Array (AffinePoint (F Fp))
+            { lagrangeComms: (coerce $ vestaSrsLagrangeCommitments stepSrs 15 175) :: Array (AffinePoint (F Fp))
             , blindingH: (coerce $ vestaSrsBlindingGenerator stepSrs) :: AffinePoint (F Fp)
             }
-        pending "ivp_step_circuit"
-      -- exactMatch "ivp_step_circuit" (fromCompiledCircuit $ compileIvpStep stepSrsData)
+        exactMatch "ivp_step_circuit" (fromCompiledCircuit $ compileIvpStep stepSrsData)
       describe "Linearization" do
         exactMatch "linearization_step_circuit" (fromCompiledCircuit compileLinearizationStep)
         exactMatch "linearization_wrap_circuit" (fromCompiledCircuit compileLinearizationWrap)

packages/pickles-circuit-diffs/visualizer/src/CircuitDiffTable.js

@@ -58,10 +58,13 @@ function GateTable({ title, gates, diffIndices, publicInputSize }) {
     count: gates.length,
     getScrollElement: () => parentRef.current,
     estimateSize: useCallback(
-      (idx) =>
-        expanded[idx]
-          ? 28 + 16 * Math.max(gates[idx]?.context?.length || 0, 1) + 8
-          : 28,
+      (idx) => {
+        if (!expanded[idx]) return 28;
+        const ctx = gates[idx]?.context || [];
+        // Estimate height: each context line may wrap (long OCaml paths ~120 chars,
+        // visible width ~60 chars at 11px monospace), so allow ~32px per line
+        return 28 + 32 * Math.max(ctx.length, 1) + 8;
+      },
       [expanded, gates]
     ),
     overscan: 20,
@@ -132,6 +135,7 @@ function GateTable({ title, gates, diffIndices, publicInputSize }) {
                     ? styles.virtualRowDiff
                     : "",
               hasContext ? styles.virtualRowClickable : "",
+              isExpanded ? styles.virtualRowExpanded : "",
             ]
               .filter(Boolean)
               .join(" ");

packages/pickles-circuit-diffs/visualizer/src/styles/gate-table.module.css

@@ -115,4 +115,10 @@
   color: #555;
   font-size: 11px;
   line-height: 16px;
+  word-break: break-all;
+}
+
+/* Expanded rows need higher z-index so context isn't hidden behind the next row */
+.virtualRowExpanded {
+  z-index: 1;
 }

packages/pickles/src/Pickles/Verify.purs

@@ -61,6 +61,7 @@ type IncrementallyVerifyProofParams f r =
   , endo :: f -- ^ EndoScalar constant for challenge expansion
   , groupMapParams :: GroupMapParams f
   , correctionMode :: CorrectionMode
+  , useOptSponge :: Boolean -- ^ true for Wrap (Opt_sponge), false for Step (regular sponge)
   | r
   }
 
@@ -108,7 +109,7 @@ type IncrementallyVerifyProofOutput d f =
 -- | - `g`: commitment curve group
 -- | - `sf`: shifted scalar type (Type1 or Type2)
 incrementallyVerifyProof
-  :: forall publicInput sgOldN d f f' @g sf t m _l3 r
+  :: forall publicInput sgOldN totalBases d f f' @g sf t m _l3 _l4 r
    . PrimeField f
   => FieldSizeInBits f 255
   => FieldSizeInBits f' 255
@@ -121,6 +122,8 @@ incrementallyVerifyProof
   => PublicInputCommit publicInput f
   => Reflectable d Int
   => Add 1 _l3 d
+  => Add sgOldN 45 totalBases
+  => Add 1 _l4 totalBases
   => IpaScalarOps f t m sf
   -> IncrementallyVerifyProofParams f r
   -> IncrementallyVerifyProofInput publicInput sgOldN d (FVar f) sf
@@ -147,27 +150,50 @@ incrementallyVerifyProof scalarOps params input = labelM "incrementally-verify-p
       -- Squeeze digest
       Sponge.squeeze
 
-  -- 2. Compute x_hat (public input commitment)
-  xHat <- liftSnarky $ label "ivp_xhat" $ publicInputCommit params input.publicInput
+  -- 2. Sponge transcript + x_hat
+  -- Step (regular sponge): absorb index_digest + sg_old BEFORE x_hat, matching
+  --   OCaml step_verifier.ml ordering. Uses regular sponge (not Opt_sponge).
+  -- Wrap (OptSponge): compute x_hat first, then run spongeTranscriptOptCircuit.
+  { xHat, beta, gamma, alphaChal, zetaChal, digest } <-
+    if params.useOptSponge then do
+      -- Wrap path: compute x_hat first, then OptSponge for all absorptions
+      xHat <- liftSnarky $ label "ivp_xhat" $ publicInputCommit params input.publicInput
+      let spongeInput = { indexDigest, sgOld: input.sgOld, publicComm: xHat, wComm: input.wComm, zComm: input.zComm, tComm: input.tComm }
+      result <- labelM "ivp_opt_sponge" $ spongeTranscriptOptCircuit endoParams spongeInput
+      pure { xHat, beta: result.beta, gamma: result.gamma, alphaChal: result.alphaChal, zetaChal: result.zetaChal, digest: result.digest }
+    else do
+      -- Step path: absorb index_digest + sg_old into main sponge BEFORE x_hat
+      -- Matches step_verifier.ml:528-530
+      Sponge.absorb indexDigest
+      for_ input.sgOld Sponge.absorbPoint
+      -- Compute x_hat
+      xHat <- liftSnarky $ label "ivp_xhat" $ publicInputCommit params input.publicInput
+      -- Continue sponge transcript: absorb x_hat, w_comm, squeeze beta/gamma, etc.
+      -- step_verifier.ml:551-568
+      Sponge.absorbPoint xHat
+      for_ input.wComm Sponge.absorbPoint
+      -- beta/gamma: squeeze_challenge (constrain_low_bits:true)
+      beta <- Sponge.squeezeScalarChallenge endoParams
+      gamma <- Sponge.squeezeScalarChallenge endoParams
+      -- z_comm: receive
+      Sponge.absorbPoint input.zComm
+      -- alpha: squeeze_scalar (constrain_low_bits:false)
+      alphaChal <- Sponge.squeezeScalar endoParams
+      -- t_comm: receive
+      for_ input.tComm Sponge.absorbPoint
+      -- zeta: squeeze_scalar (constrain_low_bits:false)
+      zetaChal <- Sponge.squeezeScalar endoParams
+      -- Copy sponge before squeezing digest (step_verifier.ml:559)
+      spongeBeforeEvals <- Sponge.getSponge
+      digest <- Sponge.squeeze
+      Sponge.putSponge spongeBeforeEvals
+      pure { xHat, beta, gamma, alphaChal, zetaChal, digest }
 
-  -- 3. Run Fq-sponge transcript
-  let
-    spongeInput =
-      { indexDigest
-      , sgOld: input.sgOld
-      , publicComm: xHat
-      , wComm: input.wComm
-      , zComm: input.zComm
-      , tComm: input.tComm
-      }
-  { beta, gamma, alphaChal, zetaChal, digest } <- labelM "ivp_opt_sponge" $
-    spongeTranscriptOptCircuit endoParams spongeInput
-
-  -- 4. Assert deferred values match sponge output (all 128-bit scalar challenges)
+  -- 3. Assert deferred values match sponge output (all 128-bit scalar challenges)
   liftSnarky $ label "ivp_assert_plonk" $
     assertEq { beta, gamma, alpha: alphaChal, zeta: zetaChal } (toPlonkMinimal input.deferredValues.plonk)
 
-  -- 5. Compute ft_comm
+  -- 4. Compute ft_comm
   ftCommResult <- liftSnarky $ label "ivp_ftcomm" $ ftComm
     scalarOps
     { sigmaLast: constPt params.sigmaCommLast
@@ -177,15 +203,18 @@ incrementallyVerifyProof scalarOps params input = labelM "incrementally-verify-p
     , zetaToDomainSize: input.deferredValues.plonk.zetaToDomainSize
     }
 
-  -- 5. Assemble 45 commitment bases in to_batch order
+  -- 5. Assemble commitment bases: sg_old + 45 fixed bases (to_batch order)
+  -- Matches OCaml: sg_old[0..1], x_hat, ft_comm, z_comm, index(6), w_comm(15), coeff(15), sigma(6)
   let
-    allBases :: Vector 45 (AffinePoint (FVar f))
+    allBases :: Vector totalBases (AffinePoint (FVar f))
     allBases =
-      (xHat :< ftCommResult :< input.zComm :< Vector.nil)
-        `Vector.append` map constPt params.columnComms.index
-        `Vector.append` input.wComm
-        `Vector.append` map constPt params.columnComms.coeff
-        `Vector.append` map constPt params.columnComms.sigma
+      input.sgOld `Vector.append`
+        ( (xHat :< ftCommResult :< input.zComm :< Vector.nil)
+            `Vector.append` map constPt params.columnComms.index
+            `Vector.append` input.wComm
+            `Vector.append` map constPt params.columnComms.coeff
+            `Vector.append` map constPt params.columnComms.sigma
+        )
 
   -- 6. Build CheckBulletproofInput and run checkBulletproof
   let
@@ -225,7 +254,7 @@ incrementallyVerifyProof scalarOps params input = labelM "incrementally-verify-p
 -- |
 -- | Reference: mina/src/lib/pickles/step_verifier.ml:1164-1222
 verify
-  :: forall publicInput sgOldN d f f' @g sf t m _l2 _l3 r
+  :: forall publicInput sgOldN totalBases d f f' @g sf t m _l2 _l3 _l4 r
    . PrimeField f
   => FieldSizeInBits f 255
   => FieldSizeInBits f' 255
@@ -239,6 +268,8 @@ verify
   => Reflectable d Int
   => Add 1 _l2 7
   => Add 1 _l3 d
+  => Add sgOldN 45 totalBases
+  => Add 1 _l4 totalBases
   => IpaScalarOps f t m sf
   -> IncrementallyVerifyProofParams f r
   -> IncrementallyVerifyProofInput publicInput sgOldN d (FVar f) sf

packages/pickles/src/Pickles/Wrap/Circuit.purs

@@ -81,6 +81,7 @@ type WrapParams f =
   -- Shared
   , endo :: f
   , correctionMode :: CorrectionMode
+  , useOptSponge :: Boolean
   }
 
 -- | The Wrap circuit: finalizes deferred values and verifies IPA opening.

packages/pickles/test/Test/Pickles/TestContext.purs

@@ -751,6 +751,7 @@ buildWrapCircuitParams ctx =
     , linearizationPoly: Linearization.vesta
     , groupMapParams: Kimchi.groupMapParams (Proxy @Vesta.G)
     , correctionMode: InCircuitCorrections
+    , useOptSponge: true
     }
 
 -------------------------------------------------------------------------------
@@ -1800,6 +1801,7 @@ buildStepIVPParams ctx =
     , endo: stepEndo
     , groupMapParams: Kimchi.groupMapParams (Proxy @Pallas.G)
     , correctionMode: PureCorrections
+    , useOptSponge: false
     }
 
 -- | Build IVP circuit input for an Fp circuit verifying a Wrap (Pallas) proof.

packages/random-oracle/src/Snarky/Circuit/RandomOracle/Sponge.purs

@@ -27,7 +27,7 @@ import Poseidon (class PoseidonField)
 import RandomOracle.Sponge (Sponge, SpongeState(..), create, rate, state) as ReExports
 import RandomOracle.Sponge (Sponge, SpongeState(..), rate)
 import RandomOracle.Sponge as Sponge
-import Snarky.Circuit.DSL (class CircuitM, FVar, Snarky, add_, const_)
+import Snarky.Circuit.DSL (class CircuitM, FVar, Snarky, add_, const_, seal)
 import Snarky.Circuit.Kimchi (poseidon)
 import Snarky.Constraint.Kimchi (KimchiConstraint)
 import Snarky.Curves.Class (class PrimeField)
@@ -54,21 +54,24 @@ absorb x sponge = case sponge.spongeState of
     if n == rate then do
       -- Rate limit reached, permute first then absorb
       newState <- poseidon sponge.state
-      let newState' = Vector.modifyAt p0 (add_ x) newState
+      -- OCaml: add_assign ~state i x = state.(i) <- Utils.seal Field.(state.(i) + x)
+      sealed <- seal (add_ x (Vector.index newState p0))
+      let newState' = Vector.updateAt p0 sealed newState
       pure { state: newState', spongeState: Absorbed p1 }
-    else
+    else do
       -- Add to current position (no permutation needed)
+      -- OCaml: add_assign ~state i x = state.(i) <- Utils.seal Field.(state.(i) + x)
+      sealed <- seal (add_ x (Vector.index sponge.state n))
       let
-        newState = Vector.modifyAt n (add_ x) sponge.state
+        newState = Vector.updateAt n sealed sponge.state
         pNext = unsafePartial fromJust $ succ n
-      in
-        pure { state: newState, spongeState: Absorbed pNext }
-  Squeezed _ ->
+      pure { state: newState, spongeState: Absorbed pNext }
+  Squeezed _ -> do
     -- Coming from squeezed state, add at position 0
-    let
-      newState = Vector.modifyAt p0 (add_ x) sponge.state
-    in
-      pure { state: newState, spongeState: Absorbed p1 }
+    -- OCaml: add_assign ~state i x = state.(i) <- Utils.seal Field.(state.(i) + x)
+    sealed <- seal (add_ x (Vector.index sponge.state p0))
+    let newState = Vector.updateAt p0 sealed sponge.state
+    pure { state: newState, spongeState: Absorbed p1 }
   where
   p0 :: Finite 3
   p0 = unsafeFinite 0