Formalize Pedersen hash + commitment using BLAKE3 generators

Lampe/Lampe.lean

@@ -13,6 +13,7 @@ import Lampe.Builtin.Crypto.Ecdsa
 import Lampe.Builtin.Crypto.EmbeddedCurve
 import Lampe.Builtin.Crypto.Hash
 import Lampe.Builtin.Crypto.Keccak
+import Lampe.Builtin.Crypto.Pedersen
 import Lampe.Builtin.Crypto.Sha256
 import Lampe.Builtin.Field
 import Lampe.Builtin.Lens
@@ -27,10 +28,12 @@ import Lampe.Crypto.Blake2s
 import Lampe.Crypto.Blake3
 import Lampe.Crypto.Bn254
 import Lampe.Crypto.Bn254.Prime
+import Lampe.Crypto.Bn254.Sqrt
 import Lampe.Crypto.Ecdsa
 import Lampe.Crypto.EmbeddedCurve
 import Lampe.Crypto.Keccak
 import Lampe.Crypto.MathlibBridge
+import Lampe.Crypto.Pedersen
 import Lampe.Crypto.Poseidon2
 import Lampe.Crypto.Poseidon2.BN254T4
 import Lampe.Crypto.Secp256k1

Lampe/Lampe/Builtin/Crypto/EmbeddedCurve.lean

@@ -20,18 +20,32 @@ def embeddedCurveAdd := newGenericPureBuiltin
         ⟨[encodeCurvePoint ((curvePoint? p1).get h1 + (curvePoint? p2).get h2)], by simp⟩⟩)
 
 /--
-Noir's `multi_scalar_mul_array_return` foreign builtin. The result is
-`∑ᵢ (scalarValueNat sᵢ) • Pᵢ` computed via Mathlib's `+` and `nsmul`.
-On-curve obligation is a precondition: every input point must lift
-through `curvePoint?`.
+Noir's `multi_scalar_mul_array_return` foreign builtin.
+
+Two preconditions, both modelling actual circuit constraints emitted by
+the Barretenberg MSM gadget:
+
+- **On-curve**: every input point lifts through `curvePoint?`. The
+  gadget's curve-relation constraint inside `cycle_group::batch_mul`
+  enforces this on each input.
+- **Canonical scalars**: every input scalar satisfies `Scalar.Canonical`
+  (`lo.val < 2^128 ∧ hi.val < 2^126`). The gadget's
+  `create_limbed_range_constraint` emits this on every input scalar via
+  `straus_scalar_slice.cpp:59`, with `LO_BITS`/`HI_BITS` pinned in
+  `cycle_scalar.hpp:38-44`.
+
+The `predicate` parameter is ignored; the Noir surface wrapper
+`multi_scalar_mul` (file `embedded_curve_ops.nr`) hardcodes
+`predicate = true`.
 -/
 def multiScalarMul := newGenericPureBuiltin
   (fun n => ⟨[.array pointTp n, .array scalarTp n, .bool], .array pointTp 1⟩)
   (fun {p} n h![points, scalars, _] =>
-    ⟨∀ i, (curvePoint? (points.get i)).isSome,
+    ⟨(∀ i, (curvePoint? (points.get i)).isSome)
+      ∧ (∀ i, Scalar.Canonical (scalars.get i)),
       fun h =>
         let acc : (affineCurve p).Point :=
-          ∑ i, scalarValueNat (scalars.get i) • (curvePoint? (points.get i)).get (h i)
+          ∑ i, Scalar.valueNat (scalars.get i) • (curvePoint? (points.get i)).get (h.1 i)
         ⟨[encodeCurvePoint acc], by simp⟩⟩)
 
 end Lampe.Builtin

Lampe/Lampe/Builtin/Crypto/Pedersen.lean

@@ -0,0 +1,46 @@
+import Lampe.Builtin.Basic
+import Lampe.Crypto.Pedersen
+import Lampe.Data.HList
+import Lampe.Data.Field
+
+namespace Lampe.Builtin
+
+open Lampe.Crypto.EmbeddedCurve
+open Lampe.Crypto.Pedersen
+
+/-- Convert a length-`M` byte vector to the `List (BitVec 8)` used as
+the opaque domain-separator key by `derivePedersenGenerators`. -/
+def bytesToList {p M} (bs : Tp.denote p ((Tp.u 8).array M)) : List (BitVec 8) :=
+  bs.toList
+
+/--
+Noir's `derive_pedersen_generators` foreign builtin, generic in the
+pair `(N, M)` of array sizes per the Noir signature
+`<let N: u32, let M: u32>`.
+
+Inputs:
+- `domain_separator_bytes : [u8; M]` — domain separator string
+- `starting_index : u32`             — absolute starting index
+
+Output:
+- `[EmbeddedCurvePoint; N]` — `N` distinct Grumpkin generator points
+
+Modeled by the concrete BLAKE3-driven hash-to-curve construction in
+`Lampe.Crypto.Pedersen.derivePedersenGenerators` (see that file for the
+construction; it transcribes the standard `derive_generators` algorithm
+that any Noir backend must implement).
+-/
+def derivePedersenGenerators := newGenericTotalPureBuiltin
+  (fun (nm : U 32 × U 32) =>
+    let N := nm.1
+    let M := nm.2
+    ⟨[(Tp.u 8).array M, Tp.u 32], pointTp.array N⟩)
+  (fun {p} nm h![domainBytes, startIdx] =>
+    let N := nm.1
+    let M := nm.2
+    Lampe.Crypto.Pedersen.derivePedersenGenerators p
+      (bytesToList (M := M) domainBytes)
+      startIdx.toNat
+      N.toNat)
+
+end Lampe.Builtin

Lampe/Lampe/Builtin/Runtime.lean

@@ -7,7 +7,18 @@ Returns whether the execution is performed in an unconstrained context.
 
 Note we always return false, as otherwise we would be unable to reason about the code.
 -/
-def isUnconstrained := newTotalPureBuiltin 
+def isUnconstrained := newTotalPureBuiltin
   ([], .bool)
   (fun _ => false)
 
+/--
+Noir's `#[builtin(assert_constant)]` compiler hint.
+
+Semantically a no-op: takes any value of any type and returns `unit`.
+The Noir compiler uses this to mark values that must be constant at
+proof-generation time; the Lampe model ignores the runtime hint.
+-/
+def assertConstant := newGenericTotalPureBuiltin
+  (fun (tp : Tp) => ⟨[tp], .unit⟩)
+  (fun _ _ => ())
+

Lampe/Lampe/Builtin/Stubs.lean

@@ -30,10 +30,8 @@ def stub : Builtin := {
 -- to match the name in extracted code that comes from Noir.
 def arrayRefcount := stub
 def asWitness := stub
-def assertConstant := stub
 def blackBox := stub
 def checkedTransmute := stub
-def derivePedersenGenerators := stub
 def fmtstrAsCtstring := stub
 def mkFormatString := stub
 def recursiveAggregation := stub

Lampe/Lampe/Crypto/Bn254.lean

@@ -34,9 +34,6 @@ def plo : Nat := 53438638232309528389504892708671455233
 /-- High limb of the BN254 scalar-field prime: `r_scalar / 2^128`. -/
 def phi : Nat := 64323764613183177041862057485226039389
 
-/-- Limb base `2^128`. -/
-def pow128 : Nat := 2 ^ 128
-
 /-- The numeric content of `Bn254.Prime`: the prime decomposes as
 `plo + 2^128 * phi`. Equivalent to `p.natVal = r_scalar`. -/
 private lemma r_scalar_eq_limbs : r_scalar = plo + pow128 * phi := by