Fast, proven Pasta arithmetic + fixture-check speedup

Zcash/Arithmetic.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Ironwood Contributors.
+Released under the Apache License, Version 2.0.
+-/
+import Zcash.Arithmetic.Field
+import Zcash.Arithmetic.Group
+
+/-!
+# The arithmetic tier, and the two names it lends the whole repository
+
+`Zcash/Arithmetic/` holds the objects every other tier is stated over: the scalar field, the
+verifier group's reference string, the fingerprint MSM and the fast kernels behind them. Most
+of those names are local vocabulary and stay qualified — a module that wants `bestFftG` or
+`omegaOf` opens `Zcash.Arithmetic` for exactly that name.
+
+`Fp` and `URS` are the exceptions. They appear in nearly every statement in the repository, so
+they are re-exported at the `Zcash` root: any module declaring inside `Zcash.*` finds them by
+the enclosing-namespace walk, with no `open` at all. Nothing else earns root vocabulary.
+
+There is deliberately no `G` here. The verifier group is a type *variable* throughout
+(`URS (G : Type*)`, `variable {G : Type*}`); the concrete instantiations bind their own `G`
+locally, so there is no declaration to export.
+-/
+
+namespace Zcash
+
+export Arithmetic (Fp URS)
+
+end Zcash

Zcash/Arithmetic/CommitLagrange.lean

@@ -0,0 +1,113 @@
+import CompElliptic.Curves.Pasta.Fast.ProjectiveMontEquiv
+
+/-!
+# The fast Lagrange commitment
+
+`commit_lagrange` — a Pedersen vector commitment against a fixed basis, plus a blind — is the
+operation the verifying-key derivation runs 44 times over 2048-term columns, and it dominates
+that computation. This module gives the fast evaluation path for it (`commitLagrangeMontWith`)
+together with the PROVEN equality to the naive spec (`commitLagrangeMontWith_eq`), so a caller
+gets the speed without the statement ever mentioning the fast route.
+
+The speed comes from running the MSM over the **proven eight-limb Montgomery field**:
+`CompElliptic.Curves.Pasta.Fast.ProjectiveMontDefs` is the core-only twin of the group kernels
+(RCB addition, double-and-add, scatter Pippenger) there, compiled to native code through the
+`FastFieldNative` `precompileModules` leaf. This module is mathlib-side and deliberately NOT in
+that leaf's glob: it holds the `ZMod`-typed entry points — coordinates into Montgomery form,
+kernel, affine reading back — and chains the kernel's simulation theorem `msmM_spec` into the
+`_eq` ladder that lands on `Msm.commitLagrangeSpec`.
+
+`ofPVesM` must never be compared definitionally: unfolding it exposes the CIOS (Coarsely
+Integrated Operand Scanning) rounds, so the equalities below are stated and proved by rewriting only.
+-/
+
+namespace Zcash.Arithmetic
+
+open CompElliptic.Curves.Pasta.Fast
+open CompElliptic.Curves.Pasta.Fast.ProjectiveMont
+open CompElliptic.Curves.Pasta.Fast.ProjectiveMont (PM)
+open Montgomery.Native64x8
+open CompElliptic.Curves.Pasta.Fast.Projective
+open CompElliptic.Curves.Pasta.Fast.Projective.PVes
+-- The vendored `Msm` imported ironwood's scalar field, so `Fp` used to arrive here through the
+-- enclosing namespace. Upstream's `Msm` is standalone and carries its own (reducibly equal)
+-- `Fp := CompElliptic.Fields.Pasta.VestaScalarField`, which this module takes instead of
+-- importing `Zcash.Arithmetic.Field`.
+open CompElliptic.Curves.Pasta.Fast.Msm (Fp)
+
+local instance : Inhabited G := ⟨0⟩
+
+/-- Every `Fp` value's canonical representative is a 256-bit scalar. -/
+theorem val_lt_two_pow_256 (a : Fp) : a.val < 2 ^ 256 :=
+  lt_of_lt_of_le (ZMod.val_lt a) (by decide)
+
+/-- `PVes → PM`: each coordinate's canonical representative, entered into Montgomery form. -/
+def ofPVesM (P : PVes) : PM :=
+  ⟨VestaFq.ofNat P.X.val, VestaFq.ofNat P.Y.val, VestaFq.ofNat P.Z.val⟩
+
+theorem wfp_ofPVesM (P : PVes) : WFP (ofPVesM P) :=
+  ⟨wf_ofNat (ZMod.val_lt _), wf_ofNat (ZMod.val_lt _), wf_ofNat (ZMod.val_lt _)⟩
+
+theorem toPVesM_ofPVesM (P : PVes) : toPVesM (ofPVesM P) = P := by
+  cases P with
+  | mk X Y Z =>
+    simp only [toPVesM, ofPVesM, PVes.mk.injEq]
+    refine ⟨?_, ?_, ?_⟩ <;>
+      rw [montVal_ofNat (ZMod.val_lt _)]
+    exacts [ZMod.natCast_rightInverse X, ZMod.natCast_rightInverse Y, ZMod.natCast_rightInverse Z]
+
+theorem toGM_ofPVesM_ofAffine (g : G) : toGM (ofPVesM (ofAffine g)) = g := by
+  rw [toGM, toPVesM_ofPVesM, toAffine_ofAffine]
+
+theorem valid_toPVesM_ofPVesM_ofAffine (g : G) : Valid (toPVesM (ofPVesM (ofAffine g))) := by
+  rw [toPVesM_ofPVesM]
+  exact valid_ofAffine g
+
+/-- Entering Montgomery form and reading back is the identity, pointwise along a list.  Stated
+and proved by `rw` alone: the elaborator must never be asked for a *definitional* comparison
+across `ofPVesM`, since unfolding it exposes the CIOS rounds. -/
+theorem map_toGM_ofPVesM_ofAffine :
+    ∀ l : List G, (l.map fun g => ofPVesM (ofAffine g)).map toGM = l
+  | [] => rfl
+  | a :: l => by
+    rw [List.map_cons, List.map_cons, map_toGM_ofPVesM_ofAffine l, toGM_ofPVesM_ofAffine]
+
+/-- `commit_lagrange` through the Montgomery-lane kernel MSM. -/
+def commitLagrangeMontWith (c : ℕ) (blind : G) (basis : List G)
+    (coeffs : List Fp) : G :=
+  toGM (PM.msm c
+    ((coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map
+      fun t => (t.1.val, ofPVesM (ofAffine t.2)))) + blind
+
+/-- **The Montgomery committer equals the naive `commit_lagrange` spec.** -/
+theorem commitLagrangeMontWith_eq (c : ℕ) (hc : 0 < c)
+    (blind : G) (basis : List G) (coeffs : List Fp) :
+    commitLagrangeMontWith c blind basis coeffs
+      = Msm.commitLagrangeSpec blind basis coeffs := by
+  unfold commitLagrangeMontWith
+  rw [toGM, ProjectiveMont.msmM_spec c hc _
+    (by intro t ht
+        rw [List.mem_map] at ht
+        obtain ⟨s, -, rfl⟩ := ht
+        exact wfp_ofPVesM _)
+    (by intro t ht
+        rw [List.mem_map] at ht
+        obtain ⟨s, -, rfl⟩ := ht
+        exact valid_toPVesM_ofPVesM_ofAffine s.2)
+    (by intro t ht
+        rw [List.mem_map] at ht
+        obtain ⟨s, -, rfl⟩ := ht
+        exact val_lt_two_pow_256 s.1)]
+  have hterms :
+      ((coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map
+          fun t => (t.1.val, ofPVesM (ofAffine t.2))).map
+        (fun t => (t.1, toAffine (toPVesM t.2)))
+      = (coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map
+          fun t => (t.1.val, t.2) := by
+    rw [List.map_map]
+    refine List.map_congr_left fun t _ => ?_
+    simp only [Function.comp_apply, toPVesM_ofPVesM, toAffine_ofAffine]
+  rw [hterms, Msm.zip_terms_eq, Msm.pippenger_eq_msm c hc, List.map_map]
+  rfl
+
+end Zcash.Arithmetic

Zcash/Arithmetic/Domain.lean

@@ -0,0 +1,117 @@
+import CompElliptic.Curves.Pasta
+import Zcash.Arithmetic.Field
+
+/-!
+# Evaluation-domain scalars (pasta `Fp` constants and facts)
+
+halo2's domain data as pure functions: binary exponentiation (`powFast`), the size-`2^k`
+domain root of unity `omegaOf` (pasta `Fp::GENERATOR = 5`, `ROOT_OF_UNITY` squared down,
+`EvaluationDomain::new`), `Fp::DELTA`, and the domain facts (primitive-root, power
+injectivity, size nonvanishing) bridged once to CompElliptic's certified Pasta root.
+Moved out of `Zcash/Bridge` per the Clean-boundary architecture
+(`Zcash/Circuits/Integration/clean-boundary.md`): these are verifier-native arithmetic
+facts, not bridge plumbing.
+-/
+
+namespace Zcash.Arithmetic
+
+/-- Binary exponentiation (`Monoid.npow`'s default recursion is linear — unusable for
+exponents of order `p/2^k`). -/
+def powFast (b : Fp) (n : ℕ) : Fp :=
+  if n = 0 then 1
+  else
+    let r := powFast (b * b) (n / 2)
+    if n % 2 = 1 then b * r else r
+  decreasing_by omega
+
+/-- Binary exponentiation agrees with the field's ordinary natural power. -/
+theorem powFast_eq_pow (b : Fp) (n : ℕ) :
+    powFast b n = b ^ n := by
+  induction n using Nat.strong_induction_on generalizing b with
+  | h n ih =>
+      rw [powFast]
+      by_cases hn : n = 0
+      · simp [hn]
+      · rw [if_neg hn]
+        have hhalf : n / 2 < n := Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (by norm_num)
+        rw [ih (n / 2) hhalf]
+        by_cases hodd : n % 2 = 1
+        · rw [if_pos hodd]
+          have hn_split : n = 2 * (n / 2) + 1 := by omega
+          calc
+            b * (b * b) ^ (n / 2) =
+                b * (b ^ 2) ^ (n / 2) := by rw [pow_two]
+            _ = b ^ (2 * (n / 2) + 1) := by
+              rw [pow_add, pow_mul, pow_one]
+              ring
+            _ = b ^ n := congrArg (b ^ ·) hn_split.symm
+        · have heven : n % 2 = 0 := by omega
+          rw [if_neg hodd]
+          have hn_split : n = 2 * (n / 2) := by omega
+          calc
+            (b * b) ^ (n / 2) = (b ^ 2) ^ (n / 2) := by rw [pow_two]
+            _ = b ^ (2 * (n / 2)) := by rw [pow_mul]
+            _ = b ^ n := congrArg (b ^ ·) hn_split.symm
+
+/-- The size-`2^k` domain's root of unity: pasta `Fp::GENERATOR = 5`,
+`ROOT_OF_UNITY = 5^((p−1)/2^32)`, and `EvaluationDomain::new` squares it down `32 − k`
+times — so `omega = 5^((p−1)/2^k)`. Certified against the captured VK in `VkMatch`. -/
+def omegaOf (k : ℕ) : Fp :=
+  powFast 5 ((scalarFieldOrder - 1) / 2 ^ k)
+
+/--
+The executable generator spelling of every supported `omegaOf` agrees with powers of
+CompElliptic's certified Pasta root. This is the sole native-tier bridge in the domain
+facts below; `omegaOf` itself remains pure data and does not infect assignment
+definitions with the certificate's native axiom.
+-/
+private theorem omegaOf_eq_certifiedRootPow :
+    ∀ k : Fin 33,
+      omegaOf k =
+        powFast CompElliptic.Fields.Pasta.pallasBase.rootOfUnity
+          (2 ^ (32 - (k : ℕ))) := by
+  native_decide
+
+/-- `omegaOf k` is a primitive size-`2^k` domain root for every supported exponent. -/
+theorem omegaOf_isPrimitiveRoot (k : ℕ) (hk : k ≤ 32) :
+    IsPrimitiveRoot (omegaOf k) (2 ^ k) := by
+  have hroot :
+      IsPrimitiveRoot
+        CompElliptic.Fields.Pasta.pallasBase.rootOfUnity (2 ^ 32) :=
+    IsPrimitiveRoot.iff_orderOf.mpr
+      CompElliptic.Fields.Pasta.pallasBase.valid.rootOfUnity_order
+  rw [omegaOf_eq_certifiedRootPow ⟨k, Nat.lt_succ_of_le hk⟩, powFast_eq_pow]
+  apply IsPrimitiveRoot.pow (by positivity) hroot
+  rw [← pow_add, Nat.sub_add_cancel hk]
+
+/-- Every point `omegaOf k ^ row` lies in the size-`2^k` evaluation domain. -/
+theorem omegaOf_domain (k row : ℕ) (hk : k ≤ 32) :
+    (omegaOf k ^ row) ^ (2 ^ k) = 1 := by
+  rw [← pow_mul, mul_comm, pow_mul]
+  rw [(omegaOf_isPrimitiveRoot k hk).pow_eq_one, one_pow]
+
+/-- Distinct row indices below `2^k` name distinct evaluation-domain points. -/
+theorem omegaOf_powers_injective (k : ℕ) (hk : k ≤ 32) :
+    Function.Injective fun row : Fin (2 ^ k) => omegaOf k ^ (row : ℕ) := by
+  intro left right heq
+  apply Fin.ext
+  exact (omegaOf_isPrimitiveRoot k hk).pow_inj left.isLt right.isLt heq
+
+/-- The supported evaluation-domain size is nonzero when cast into `Fp`. -/
+theorem domainSize_cast_ne_zero (k : ℕ) (hk : k ≤ 32) :
+    ((2 ^ k : ℕ) : Fp) ≠ 0 := by
+  intro hzero
+  have hdiv : scalarFieldOrder ∣ 2 ^ k :=
+    (ZMod.natCast_eq_zero_iff (2 ^ k) scalarFieldOrder).mp hzero
+  apply Nat.not_dvd_of_pos_of_lt (by positivity) _ hdiv
+  calc
+    2 ^ k ≤ 2 ^ 32 := Nat.pow_le_pow_right (by omega) hk
+    _ < scalarFieldOrder := by
+      norm_num [scalarFieldOrder,
+        CompElliptic.Fields.Pasta.PALLAS_BASE_CARD]
+
+/-- pasta `Fp::DELTA = GENERATOR^(2^S) = 5^(2^32)`. -/
+def deltaFp : Fp := powFast 5 (2 ^ 32)
+
+
+end Zcash.Arithmetic

Zcash/Arithmetic/FastMsm.lean

@@ -0,0 +1,57 @@
+import Zcash.Arithmetic.Msm
+import CompElliptic.Curves.Pasta.Fast.Msm
+
+/-!
+# Fast compiled evaluation for the fingerprint MSM
+
+`Msm.evalNat` — the executable natural-scalar MSM the captured-fixture fingerprint
+checks evaluate (`capturedMsm_eval_eq_zero`) — is spelled as the specification: a
+`Finset` sum of per-generator `nsmul`s. Evaluated naively that is ~2050 binary
+double-and-add scalar multiplications (each paying one field inversion per affine
+point addition), which dominated the fixture modules' build times.
+
+`Msm.evalNatFast` computes the same value through the PROVEN windowed Pippenger
+accelerator (`CompElliptic.Curves.Pasta.Fast.Msm.pippengerFast`, generic over any
+`AddCommMonoid`), and `Msm.evalNat_eq_evalNatFast` is a kernel-checked equality
+registered with `@[csimp]`:
+the compiler substitutes the fast implementation at every subsequently compiled call
+site — in particular inside the fixtures' `native_decide` auxiliaries — while the
+statement surface and the kernel-level meaning of `evalNat` are untouched. This is
+the proven-equality counterpart of `implemented_by` (which is forbidden here because
+it is unchecked).
+-/
+
+namespace Zcash.Arithmetic.Msm
+
+open CompElliptic.Curves.Pasta.Fast.Msm (defaultWindow pippengerFastPar
+  pippengerFastPar_eq pippengerFast_eq pippenger_eq_msm)
+
+/-- `evalNat` through the proven windowed Pippenger accelerator, with the ~32 independent
+windows evaluated in parallel (`CompElliptic.Curves.Pasta.Fast.Msm.pippengerFastPar`):
+one bucketed MSM over the generator terms, the blinding/inner-product generators, and
+the extra term list.
+
+The replacement must stay generic over `[AddCommGroup G]` (a `@[csimp]` lemma replaces the
+whole constant), so the *affine* windows-parallel accelerator is the fastest admissible form
+here; the Vesta-specific projective interior
+(`CompElliptic.Curves.Pasta.Fast.MsmProj.pippengerProjScatterPar`) cannot be dispatched
+from a generic `G`. -/
+def evalNatFast {p : ℕ} {G : Type*} [AddCommGroup G]
+    (urs : URS G) (m : Msm urs.k (ZMod p) G) : G :=
+  pippengerFastPar defaultWindow
+    ((List.ofFn fun i => ((m.gScalars i).val, urs.g i))
+      ++ (m.wScalar.val, urs.w) :: (m.uScalar.val, urs.u)
+        :: m.other.map fun t => (t.1.val, t.2))
+
+/-- **The fast MSM evaluation is `evalNat`** — registered with `@[csimp]` so compiled
+code (including the fixtures' `native_decide` auxiliaries) runs the windows-parallel
+Pippenger form. -/
+@[csimp] theorem evalNat_eq_evalNatFast : @evalNat = @evalNatFast := by
+  funext p G inst urs m
+  unfold evalNat evalNatFast
+  rw [pippengerFastPar_eq, pippengerFast_eq, pippenger_eq_msm _ (by decide)]
+  simp only [List.map_append, List.map_cons, List.map_ofFn, List.map_map,
+    List.sum_append, List.sum_cons, List.sum_ofFn, Function.comp_def]
+  abel
+
+end Zcash.Arithmetic.Msm