CPS3: value-level atomic binds — the proof state as the do-block, at values

[mitschabaude-bot]

The idea

CPS2 (atomic binds, Clean/Halo2/atomic-binds-design.md) made the proof state mirror the do-block: every used bind appears under its do-binder name, contracts are stated about those atoms, and concrete spellings appear once each on the defining-equation side. But at the region level the atoms CPS2 can mint are cell addresses (AssignedCell.of self (offset+n) cfg.z), while everything a proof actually reasons about — gate polynomials, witness equations, helper lemmas, Spec/extract — speaks cell values under the environment. Address-level atoms at the region level were tried (the universal mint gate) and reverted: five of seven region proofs had to open by un-minting them, because gates rebind cells by (column, rotation) and the helper-lemma layer speaks values.

CPS3 is the resolution: mirror the do-block at the value level. Every named region bind mints an atom for the evaluation of what it produced, the framework states every derived fact at those value atoms, and the helper-lemma layer is re-spelled over abstract values. The proof state then matches the circuit spelling 1:1 — let w ← readState cfg offset produces w : State Fp, and the gate's constraints arrive as facts about w.z, w.base.x, … — with pure-exact user halves as the endpoint.

What it looks like

For MulIncompleteRound.round:

w : State Fp                        -- let w ← readState cfg offset
w_eq : eval env (reads cfg offset self) = w
out : State Fp                      -- the terminal readState (offset+1)
out_eq : eval env (reads cfg (offset+1) self) = out
region_0 : w.base.x - out.base.x = 0 ∧ … ∧ <gate polys over w.*, out.*>
⊢ ∃ k, out.z = 2 * w.z + (if k then 1 else 0) ∧ out.base = w.base ∧ …

and the soundness proof is

obtain ⟨hxpc, hypc, hbool, hg1, hsec, hg2⟩ := region_0
exact sound_step hxpc hypc hbool hg1 hsec hg2

with sound_step : {w out : State Fp} → … → <the Spec> — no naming equations passed, no simp, no spelling bridge anywhere, because there is only one spelling.

Why this is the natural endpoint

• The Specs already live at values: Spec input output wit and extract are value-level by the framework-free contract; the knowledge-soundness convention (state the Spec at the extracted witness) is value-level; input_eq/output_eq already name values. CPS3 extends the naming that already exists at the circuit boundary to every interior named bind.
• The witness side is already value-shaped: completeness row facts land as <cell read> = <program value>; with value atoms they become out.z = (w.step k k').z-style — the .step-form equations the round port already produces are a preview.
• The helper-lemma layer wants it: the sound_step re-spell ({w out : State Fp}-ish hypotheses, boundary fact as hypothesis, conclusion = the Spec) is a working preview; CPS3 removes even the boundary-fact hypothesis because the atom is the value.
• The address↔value bridge is paid once, at mint time, in the defining equation — with a forced direction (naming equation). Today the bridge is re-derived ad hoc in every proof that meets both spellings.

Design sketch

1. Mint at eval-images. For a used raw region bind, generalize eval env <output cells> (the value), not the cell record. The defining equation eval env (reads …) = w is the single address↔value bridge; it joins the landing rules with the other naming equations (input_eq/output_eq discipline — the only hypothesis-rules the tactic wields).
2. Land every derived fact at value atoms. Gate poly chunks and witness equations get the naming equations applied (pass-2 targets, as today) — they arrive spelled at w.*/out.* projections instead of env.advice reads. Because the naming equation's LHS is the eval of a concrete cell, the per-cell rules needed for gate-queried spellings are its componentwise consequences (record injEq/projection congruence) — derived once by the tactic, not per proof.
3. Granularity: whole-value atoms + projections. w : State Fp with consumers writing w.z — matching Spec spelling and the AbstractOutputs granularity finding. No per-field value atoms.
4. Re-spell the helper-lemma layer. sound_step, step_gates, last_gates, sound_last_step, spec_of_polysZero, polysZero_of_spec, … restated over abstract values ({w out : State Fp}, plain Fp variables for single cells). This is the bulk of the work and is per-file mechanical; the sound_step re-spell is the template.
5. Rollout: a new entry point (circuit_proof_start3), opt-in per proof, exemplar-first — MulIncompleteRound.round, then Add, then the loop composites — coexisting with CPS2. Layouter-level behavior is untouched (cell atoms are correct there: no gates, every consumer opacity-respecting — see the mint-gate section of the design doc). Retire the CPS2 region path on empty corpus.

Open questions

• Completeness goal side: the constraints-to-prove also spell env.advice reads; landing them at value atoms needs the naming equations to fire on the goal (they already do) — verify the honest-env extension facts keep their .step-form RHS under the value spelling.
• Loops: the per-iteration ∀-chunks quantify over rows; the natural value atom is a row-family function (st : ℕ → State Fp with st_eq : ∀ r, eval env (reads cfg (offset+r) self) = st r) — this is exactly the rowFam that the loop proofs define by hand today, so CPS3 would mint what the proofs already invent.
• Extract: the extract value is the Spec's witness argument; it should share the entering-state atom (w), not get a second one.
• Hint cells (λ, α, β, γ, δ): unused binders mint nothing (unchanged); their gate occurrences stay concrete — fine, they are only ever passed positionally to value-generic lemmas.

Measure

Same bar as CPS2: no proof longer or uglier than its predecessor — with the CPS3-specific target that leaf user halves degenerate to obtain + exact <lemma> …, and that no proof contains a spelling-bridge line (← *_eq, Point.mk.injEq, orientation simps) at all.

[mitschabaude-bot]

Named test case for the row-family value atom question: MulComplete (now converted to a bundled round + RegionCircuit.foldRange, commit 23cc89f). Its accumulator threads through return values rather than fixed positions, so the CPS2 proof state carries eval (foldAcc … i self) families that the parent instantiates by hand into fold_sound/fold_complete — under CPS3 these are exactly the value atoms the tactic should mint (acc : ℕ → Point Fp with the per-round step facts), and the two eval flavors (point_eval_toEnvironment bridging in the completeness proof) should collapse into the single value-level spelling. A better stress test than MulIncomplete, whose state is position-threaded.