EmitPastaLadderThread.lean

/-
SCRATCH executable: emit the honest MULTI-ROW threaded trace for
`Dregg2.Circuit.Emit.PastaLadderThread.{pallas,vesta}ThreadDesc`.

  lake env lean --run EmitPastaLadderThread.lean pallastrace > ../circuit/tests/fixtures/pasta-pallas-rcb-thread-trace.txt
  lake env lean --run EmitPastaLadderThread.lean vestatrace  > ../circuit/tests/fixtures/pasta-vesta-rcb-thread-trace.txt

⚑ **THE TRACE IS THREADED, WHICH IS THE WHOLE POINT.** `EmitPastaCurveSound`'s fixture repeats ONE
honest row eight times — legal there, because the standalone row's constraints are row-local. Here
the 96 `.transition` legs relate consecutive rows, so eight copies of one row would satisfy them
only at a FIXED POINT of the group law, which `G + G` is not. Row `r` computes `acc_r + G` and row
`r+1`'s accumulator input is row `r`'s output, generated by the same `rcbSoundRow` the standalone
fixture uses and chained by `PastaCurveComplete.rcbAddM`. The accumulator therefore walks
`2G, 3G, 4G, …` down the trace — a real ladder, eight rows of it.

The last row's `.transition` legs do not fire (`when_transition()` is every row BUT the last), so
the eighth row's output is unconstrained by the thread and the trace is exactly 8 rows with no
padding convention needed.

This file only RENDERS; it authors nothing.
-/
import Dregg2.Circuit.Emit.PastaLadderThread

open Dregg2.Circuit.Emit.PastaCurveSound (rcbSoundRow)
open Dregg2.Circuit.Emit.PastaCurveComplete (rcbAddM curveB3)
open Dregg2.Circuit.Emit.PastaFieldSound (pLimb qLimb)
open Dregg2.Circuit.Emit.PastaField (pN qN)

/-- `n` chained rows: row `r` adds the fixed addend `Q` to the running accumulator, and the
accumulator of row `r+1` IS the output of row `r`. -/
def threadRows (M b3 : Nat) (pl : Nat → ℤ) (Q : Nat × Nat × Nat) :
    (Nat × Nat × Nat) → Nat → List (List ℤ)
  | _, 0 => []
  | P, (n + 1) =>
      rcbSoundRow M b3 pl P.1 P.2.1 P.2.2 Q.1 Q.2.1 Q.2.2
        :: threadRows M b3 pl Q (rcbAddM M b3 P Q) n

def traceText (rows : List (List ℤ)) : String :=
  String.intercalate "\n" (rows.map (fun r => String.intercalate " " (r.map toString))) ++ "\n"

/-- The Pallas generator in projective coordinates. -/
def Gpallas : Nat × Nat × Nat :=
  (Dregg2.Circuit.Emit.PastaCurve.Gp.1, Dregg2.Circuit.Emit.PastaCurve.Gp.2, 1)
/-- The Vesta generator in projective coordinates. -/
def Gvesta : Nat × Nat × Nat :=
  (Dregg2.Circuit.Emit.PastaCurve.Gv.1, Dregg2.Circuit.Emit.PastaCurve.Gv.2, 1)

/-- ⚑ **THE FALSIFIER, AND IT ISOLATES THE THREAD GATE.**

Seven honestly chained rows, then a LAST row that is itself perfectly honest — `rcbSoundRow` at
`(G, G)`, every coefficient gate satisfied, every limb a real byte, every range lookup held — but
whose accumulator input is `G` where row 6's output is `8G`. So:

* nothing is refused by an arithmetic gate: the forged row's own 4 476 constraints all hold;
* nothing is refused by a range lookup: every cell is a genuine limb of a genuine field element,
  well inside the declared 8-bit width — the forgery is INSIDE the limb width by construction;
* the ONLY constraint that can refuse it is a `.transition` window gate.

That is the point of the fixture. A trace of independently-honest rows is exactly what a ladder
looks like when the accumulator is re-pinned instead of threaded, and this is the object that shows
the thread is what refuses it. -/
def forgedRows (M b3 : Nat) (pl : Nat → ℤ) (Q P0 : Nat × Nat × Nat) : List (List ℤ) :=
  threadRows M b3 pl Q P0 7
    ++ [rcbSoundRow M b3 pl P0.1 P0.2.1 P0.2.2 Q.1 Q.2.1 Q.2.2]

def main (args : List String) : IO Unit :=
  match args with
  | ["pallastrace"] =>
      IO.print (traceText (threadRows pN curveB3 pLimb Gpallas Gpallas 8))
  | ["vestatrace"] =>
      IO.print (traceText (threadRows qN curveB3 qLimb Gvesta Gvesta 8))
  | ["pallasforged"] =>
      IO.print (traceText (forgedRows pN curveB3 pLimb Gpallas Gpallas))
  | ["vestaforged"] =>
      IO.print (traceText (forgedRows qN curveB3 qLimb Gvesta Gvesta))
  | _ => IO.eprintln
      "usage: EmitPastaLadderThread.lean (pallastrace|vestatrace|pallasforged|vestaforged)"