formal: the deferred sg obligation is carried, and the driver checks the carry

[martyall]

Stacked on #377.

twoHalves_kimchiVerify carries SgOk as a hypothesis: pickles never checks a proof's own sg, it hands (sg, round challenges) to the next proof on the same curve as an old accumulator, and only the terminator checks the equation outright. The design doc says the obligation is "discharged by the olds mechanism"; nothing in the tree said it, and the halves driver read every proof's olds from the prover-stored list, so a prover who put an unrelated accumulator there would have passed every check we had.

Statements (TwoHalves.lean, beside SgOk)

def AccOk (σ : SRS C.Point) (a : Accumulator C σ.k) : Prop :=
  a.sg = msm C σ.g (bPolyCoefficients fun i => a.u[i])

def Carry (E : Env C) (cp : KimchiProof C 1 E.σ.k) (pub) (cp' : KimchiProof C 1 E.σ.k) (i : Fin cp'.olds.size) : Prop :=
  cp'.olds[i].sg = (runInput C E.σ E.cvk cp pub).proof.sg
  ∧ cp'.olds[i].u = (transcriptFrom C (runOracles C E.σ E.cvk cp pub).warm _).2.1   -- SgOk's vector

theorem sgOk_iff_accOk (h : Carry E cp pub cp' i) : SgOk E cp pub ↔ AccOk E.σ cp'.olds[i]

Carry names what the step and wrap mains force through their message digests (not modelled yet; the handover is between consecutive proofs on the same curve, the circuit in between only computes the challenges). sgOk_iff_accOk is the transport: the deferred equation becomes an equation on the next proof's input, decidable by one MSM without the first proof. accOk and carry are the decidable mirrors, reflected by accOk_iff and carry_iff. The four twoHalves_* theorems are unchanged.

The driver

check-halves gains a carry lane (on by default, HALVES=carry alone to run it). Per linked same-curve pair from the proof cache — wrap k−1 → wrap k through the step between them, step k−1 → step k through the wrap — it decides carry on the two checked proofs, accOk on the accumulator, sgOk on the predecessor, and requires the last two to agree (the lemma, confirmed on data). Unlinked accumulators (front pads, base-case slots) must satisfy accOk on their own: the dummy's sg commits the dummy challenges.

On SimpleChain.json: 14 carry runs (8 pairs, 6 pads), all green; about 50 s per pair (two proofs checked, the transcript and two MSMs), the corpus 37 runs in total. The CI lane picks it up unchanged.

Gates run locally: build, dead-code (three new roots), shake on the CI list, runLinter on Pickles, check-cs, check-halves.

🤖 Generated with Claude Code

[greptile-apps]

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