diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index fea7027b..c02505cf 100644 --- a/Lampe/Lampe.lean +++ b/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 diff --git a/Lampe/Lampe/Builtin/Crypto/EmbeddedCurve.lean b/Lampe/Lampe/Builtin/Crypto/EmbeddedCurve.lean index 9db928cc..f46d00cb 100644 --- a/Lampe/Lampe/Builtin/Crypto/EmbeddedCurve.lean +++ b/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 diff --git a/Lampe/Lampe/Builtin/Crypto/Pedersen.lean b/Lampe/Lampe/Builtin/Crypto/Pedersen.lean new file mode 100644 index 00000000..af5e96d8 --- /dev/null +++ b/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 +``. + +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 diff --git a/Lampe/Lampe/Builtin/Runtime.lean b/Lampe/Lampe/Builtin/Runtime.lean index 062f2c21..624383c5 100644 --- a/Lampe/Lampe/Builtin/Runtime.lean +++ b/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 _ _ => ()) + diff --git a/Lampe/Lampe/Builtin/Stubs.lean b/Lampe/Lampe/Builtin/Stubs.lean index 45b1d9d2..d1aeda41 100644 --- a/Lampe/Lampe/Builtin/Stubs.lean +++ b/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 diff --git a/Lampe/Lampe/Crypto/Bn254.lean b/Lampe/Lampe/Crypto/Bn254.lean index 45d5fb77..89576e5c 100644 --- a/Lampe/Lampe/Crypto/Bn254.lean +++ b/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 diff --git a/Lampe/Lampe/Crypto/Bn254/Sqrt.lean b/Lampe/Lampe/Crypto/Bn254/Sqrt.lean new file mode 100644 index 00000000..81fab942 --- /dev/null +++ b/Lampe/Lampe/Crypto/Bn254/Sqrt.lean @@ -0,0 +1,711 @@ +import Lampe.Data.Field +import Lampe.Crypto.Bn254 +import Mathlib.FieldTheory.Finite.Basic + +/-! +# Tonelli–Shanks square root over the BN254 scalar field + +`sqrt : Fp p → Option (Fp p)` for `p` carrying the BN254 scalar-prime +instance `[Lampe.Crypto.Bn254.Prime p]`. Returns `some y` with +`y * y = a` when `a` is a quadratic residue, `none` otherwise. + +Plain Tonelli–Shanks specialised to BN254 (where `r - 1 = 2^28 · q'` +with `q'` odd). Proved correct: TS produces a square root on +QR inputs; the Euler gate short-circuits to `none` on +non-residues. + +References: +- Tonelli, *Bemerkung über die Auflösung quadratischer Congruenzen*, 1891. +- Shanks, *Five number-theoretic algorithms*, 1972. +- https://en.wikipedia.org/wiki/Tonelli%E2%80%93Shanks_algorithm +-/ + +namespace Lampe.Crypto.Bn254.Sqrt + +open Lampe + +/-! ### BN254 scalar-field constants + +The BN254 scalar-field prime is + +``` +r := 21888242871839275222246405745257275088548364400416034343698204186575808495617 +``` + +with `r - 1 = 2^28 * q'` and `q'` odd; The smallest quadratic non-residue is `5`. -/ + +/-- 2-adic valuation of `r_scalar - 1`. -/ +def twoAdicity : Nat := 28 + +/-- The odd part of `r - 1`, i.e. `q' = (r - 1) / 2^28`. -/ +def oddPart : Nat := + 81540058820840996586704275553141814055101440848469862132140264610111 + +/-- A quadratic non-residue modulo `r`. -/ +def nonResidue : Nat := 5 + +/-- Verification: `q'` is odd. -/ +theorem oddPart_odd : oddPart % 2 = 1 := by + unfold oddPart + decide + +/-! ### Square-and-multiply exponentiation + +Fast modular exponentiation on `ZMod n` via repeated squaring, with a +bounded `fuel` argument. The hot path in `tonelliCandidate` (and the +`nonResidue_euler` verification below) uses this so the kernel sees an +`O(log exp)` structural recursion on `fuel` instead of the +`O(exp)` recursion of `Monoid.npow`. + +Defined generically over `ZMod n` rather than over `Fp p`: every +`Fp p`-typed argument works via the definitional equality +`Fp p := ZMod p.natVal`, and `nonResidue_euler` (which doesn't have a +`Lampe.Prime` in scope) can use the same definition. -/ + +/-- Recursive square-and-multiply, structural on `fuel`. Provably equal +to `base ^ exp` whenever `exp < 2^fuel`. -/ +def fpowR {n : Nat} (base : ZMod n) (exp fuel : Nat) : ZMod n := + match fuel with + | 0 => 1 + | fuel + 1 => + let half := fpowR (base * base) (exp / 2) fuel + if exp % 2 = 1 then base * half else half + +/-- When `fuel` exceeds the bit-length of the exponent, `fpowR` agrees +with the monoid power `base ^ exp`. -/ +theorem fpowR_eq_pow {n : Nat} (base : ZMod n) : + ∀ (exp fuel : Nat), exp < 2 ^ fuel → fpowR base exp fuel = base ^ exp := by + intro exp fuel + induction fuel generalizing base exp with + | zero => + intro h + have : exp = 0 := by + have : exp < 1 := by simpa using h + omega + subst this + simp [fpowR] + | succ fuel ih => + intro h + have hhalf : exp / 2 < 2 ^ fuel := by + have hpow : (2 : Nat) ^ (fuel + 1) = 2 * 2 ^ fuel := by + rw [pow_succ, Nat.mul_comm] + rw [hpow] at h + exact Nat.div_lt_of_lt_mul h + have ih' := ih (base * base) (exp / 2) hhalf + unfold fpowR + rw [ih'] + have hsq : (base * base) ^ (exp / 2) = base ^ (2 * (exp / 2)) := by + rw [show (base * base) = base ^ 2 from by ring, ← pow_mul, Nat.mul_comm] + rw [hsq] + by_cases hpar : exp % 2 = 1 + · have hexp : exp = 2 * (exp / 2) + 1 := by + have := Nat.div_add_mod exp 2 + omega + simp [hpar] + conv_rhs => rw [hexp] + rw [pow_succ, mul_comm (base ^ _) base] + · have hexp : exp = 2 * (exp / 2) := by + have := Nat.div_add_mod exp 2 + have : exp % 2 = 0 := by omega + omega + simp [hpar] + conv_rhs => rw [hexp] + +set_option maxRecDepth 4096 in +set_option exponentiation.threshold 1024 in +/-- Verification: 5 is a quadratic non-residue mod `r`. Rewritten via +`fpowR` so the kernel sees a 512-step structural recursion instead of +the 2^253-step `Monoid.npow` recursion. Each step is ~254-bit `ZMod` +arithmetic. -/ +theorem nonResidue_euler : + (nonResidue : ZMod r_scalar) ^ ((r_scalar - 1) / 2) = -1 := by + rw [← fpowR_eq_pow (nonResidue : ZMod r_scalar) _ 512 + (by have h1 : (r_scalar - 1) / 2 < 2 ^ 254 := by unfold r_scalar; decide + have h2 : (2 : Nat) ^ 254 ≤ 2 ^ 512 := + Nat.pow_le_pow_right (by decide) (by decide) + omega)] + unfold nonResidue r_scalar + decide + +/-! ### Tonelli–Shanks: candidate root computation + +We express Tonelli–Shanks as a structurally-recursive function on +`fuel`. The outer fuel is at most `twoAdicity = 28` (each iteration strictly +decreases `M`). The inner search for the smallest `i ∈ [1, M)` with +`t^(2^i) = 1` is also expressed recursively. -/ + +/-- Inner search: given a current power `acc = t^(2^i)`, find the +smallest `j ≥ i` with `t^(2^j) = 1`, bounded by `M`. Returns +`M` if no such `j` exists in `[i, M)`. -/ +def findOrder {p : Lampe.Prime} (acc : Fp p) (i M fuel : Nat) : Nat := + match fuel with + | 0 => M + | fuel + 1 => + if i ≥ M then M + else if acc = 1 then i + else findOrder (acc * acc) (i + 1) M fuel + +/-- One outer iteration of the Tonelli–Shanks loop. Given `(M, c, t, R)` +with `t ≠ 1`, computes the next quadruple. If no admissible inner +index exists (no `i ∈ [1, M)` with `t^(2^i) = 1`), returns the input +unchanged; the `sqrt` post-verification rules out false positives. -/ +def tsStep {p : Lampe.Prime} (M : Nat) (c t R : Fp p) : + Nat × Fp p × Fp p × Fp p := + let iFound := findOrder (t * t) 1 M M + if iFound ≥ M then (M, c, t, R) + else + -- b = c^(2^(M - iFound - 1)) + let b : Fp p := fpowR c (2 ^ (M - iFound - 1)) (M + 1) + let M' := iFound + let c' := b * b + let t' := t * (b * b) + let R' := R * b + (M', c', t', R') + +/-- Tonelli–Shanks main loop. Each outer iteration strictly decreases +`M`, so `twoAdicity = 28` iterations suffice. -/ +def tonelliLoop {p : Lampe.Prime} (a : Fp p) (fuel : Nat) (M : Nat) (c t R : Fp p) : Fp p := + match fuel with + | 0 => R + | fuel + 1 => + if t = 1 then R + else + let (M', c', t', R') := tsStep M c t R + tonelliLoop a fuel M' c' t' R' + +/-- Tonelli–Shanks candidate. Computes the initial state, then runs +`tonelliLoop` for `twoAdicity = 28` iterations. -/ +def tonelliCandidate {p : Lampe.Prime} [Lampe.Crypto.Bn254.Prime p] (a : Fp p) : Fp p := + let c0 : Fp p := fpowR ((nonResidue : Fp p)) oddPart 512 + let t0 : Fp p := fpowR a oddPart 512 + let R0 : Fp p := fpowR a ((oddPart + 1) / 2) 512 + tonelliLoop a twoAdicity twoAdicity c0 t0 R0 + +/-! ### Euler's criterion (Mathlib bridge) + +For a finite field `F` of odd characteristic, `a` is a square iff +`a ^ (Fintype.card F / 2) = 1` (`FiniteField.isSquare_iff`). We +specialise that to `Fp p` with `[Lampe.Crypto.Bn254.Prime p]`, using the fact that +`r_scalar` is odd to turn `Fintype.card F / 2 = r_scalar / 2` into the +exponent `(r_scalar - 1) / 2` that classical references use. -/ + +/-- `r_scalar` is odd; needed to align `r / 2` with `(r - 1) / 2`. -/ +theorem r_scalar_odd : r_scalar % 2 = 1 := by + unfold r_scalar + decide + +/-- `r_scalar` is not equal to `2`; needed to conclude +`ringChar (Fp p) ≠ 2` from `p.natVal = r_scalar`. -/ +theorem r_scalar_ne_two : r_scalar ≠ 2 := by + unfold r_scalar + decide + +/-- For a non-zero `a : Fp p` with `[Lampe.Crypto.Bn254.Prime p]`, the existence of +a square root implies the Euler character `a ^ ((r_scalar - 1)/2) = 1`. -/ +theorem euler_one_of_exists_sqrt {p : Lampe.Prime} [hBn : Lampe.Crypto.Bn254.Prime p] + {a : Fp p} (ha : a ≠ 0) (h : ∃ y : Fp p, y * y = a) : + a ^ ((r_scalar - 1) / 2) = 1 := by + have hcard : Fintype.card (Fp p) = r_scalar := by + have : Fintype.card (Fp p) = p.natVal := by + simp [ZMod.card p.natVal] + rw [this, hBn.natVal_eq_r_scalar] + have hchar : ringChar (Fp p) ≠ 2 := by + have : ringChar (Fp p) = p.natVal := by + simpa using ZMod.ringChar_zmod_n p.natVal + rw [this, hBn.natVal_eq_r_scalar] + exact r_scalar_ne_two + have hsq : IsSquare a := by + obtain ⟨y, hy⟩ := h + exact ⟨y, hy.symm⟩ + have hpow : a ^ (Fintype.card (Fp p) / 2) = 1 := + (FiniteField.isSquare_iff (F := Fp p) hchar ha).mp hsq + have hodd_div : r_scalar / 2 = (r_scalar - 1) / 2 := by + have hodd := r_scalar_odd + omega + have hexp : Fintype.card (Fp p) / 2 = (r_scalar - 1) / 2 := by + rw [hcard]; exact hodd_div + rw [hexp] at hpow + exact hpow + +/-! ### Public `sqrt` + +`sqrt` gates Tonelli–Shanks behind an Euler-criterion check so that +non-quadratic-residue inputs return `none` in `O(log r)` field +operations. On QR inputs, Tonelli–Shanks is *proved* to return a +correct square root, so the post-verification `R * R = a` always +succeeds. -/ + +/-- Tonelli–Shanks square root with an Euler-criterion gate. + +Returns `some y` with `y * y = a` whenever `a` is a quadratic +residue (including `a = 0`), and `none` otherwise. + +Algorithmic structure: +1. If `a = 0`, return `some 0`. +2. Compute `χ := a ^ ((r - 1) / 2)` via fast exponentiation. If + `χ ≠ 1`, return `none` (Euler's criterion: `a` is not a QR). +3. Otherwise run Tonelli–Shanks and verify the candidate by squaring. +4. If verification fails (mathematically impossible on a QR input), + return `none`. -/ +def sqrt {p : Lampe.Prime} [Lampe.Crypto.Bn254.Prime p] (a : Fp p) : Option (Fp p) := + if a = 0 then + some 0 + else + let chi := fpowR a ((r_scalar - 1) / 2) 512 + if chi ≠ 1 then + none + else + let R := tonelliCandidate a + if R * R = a then + some R + else + none + +theorem fpowR_euler_eq_pow {p : Lampe.Prime} (a : Fp p) : + fpowR a ((r_scalar - 1) / 2) 512 = a ^ ((r_scalar - 1) / 2) := by + apply fpowR_eq_pow + have h1 : (r_scalar - 1) / 2 < 2 ^ 254 := by unfold r_scalar; decide + have h2 : (2 : Nat) ^ 254 ≤ 2 ^ 512 := by + apply Nat.pow_le_pow_right (by norm_num) (by norm_num) + exact lt_of_lt_of_le h1 h2 + +/-! ### Correctness -/ + +/-- Soundness of `sqrt`: a `some` result squares to the input. +Model-fidelity assurance for the `sqrt` definition; has no +downstream consumers by design. -/ +theorem sqrt_correct {p : Lampe.Prime} [Lampe.Crypto.Bn254.Prime p] {a y : Fp p} + (h : sqrt a = some y) : y * y = a := by + unfold sqrt at h + by_cases hz : a = 0 + · simp [hz] at h + simp [hz, ← h] + · simp [hz] at h + by_cases hEuler : fpowR a ((r_scalar - 1) / 2) 512 = 1 + · simp [hEuler] at h + by_cases hv : tonelliCandidate a * tonelliCandidate a = a + · simp [hv] at h + rw [← h] + exact hv + · simp [hv] at h + · simp [hEuler] at h + +/-! ### Completeness: the Tonelli–Shanks correctness proof + +This is the heart of the file. We show that on a QR input, +`tonelliCandidate a * tonelliCandidate a = a`. The proof goes via +a loop invariant `TSInv` that is preserved by `tsStep` and witnesses +the desired equation at termination. -/ + +/-- The Tonelli–Shanks loop invariant. + +At every iteration with state `(M, c, t, R)` for input `a`, we have: + +- `R * R = a * t` (the candidate squared, modulo `t`) +- `t^(2^(M-1)) = 1` (so `ord t` divides `2^(M-1)`) +- `c^(2^(M-1)) = -1` (so `c` has order exactly `2^M`) +- `1 ≤ M` + +The fourth conjunct keeps the third meaningful (otherwise `M - 1` +underflows in `Nat`). -/ +structure TSInv {p : Lampe.Prime} (a : Fp p) (M : Nat) (c t R : Fp p) : Prop where + Msq : R * R = a * t + tpow : t ^ (2 ^ (M - 1)) = 1 + cpow : c ^ (2 ^ (M - 1)) = -1 + Mge : 1 ≤ M + +/-! ### Initial state: TSInv holds at `(twoAdicity, c0, t0, R0)` + +We need: +- `R0 * R0 = a * t0` where `R0 = a^((q'+1)/2)`, `t0 = a^q'`. Since + `q' + 1` is even, `(q'+1)/2 + (q'+1)/2 = q'+1`, and `R0² = a^(q'+1) = a · a^q' = a · t0`. +- `t0^(2^(twoAdicity-1)) = 1`. This is the Euler condition: `t0^(2^(twoAdicity-1)) = a^(q' · 2^(twoAdicity-1)) = a^((r-1)/2)`, which equals `1` because `a` is a QR. +- `c0^(2^(twoAdicity-1)) = -1`. This is `nonResidue^(q' · 2^(twoAdicity-1)) = nonResidue^((r-1)/2) = -1` by `nonResidue_euler`. +-/ + +/-- Key identity: `q' · 2^(twoAdicity - 1) = (r_scalar - 1) / 2`. -/ +theorem oddPart_mul_two_pow_eq : oddPart * 2 ^ (twoAdicity - 1) = (r_scalar - 1) / 2 := by + unfold oddPart twoAdicity r_scalar + decide + +/-- `nonResidue_euler` transported to `Fp p` when `p.natVal = r_scalar`. + +Done by viewing the goal as an equality between `Eq.mpr`-cast versions of +the corresponding `ZMod r_scalar` statement. -/ +theorem nonResidue_euler_fp {p : Lampe.Prime} [hBn : Lampe.Crypto.Bn254.Prime p] : + (nonResidue : Fp p) ^ ((r_scalar - 1) / 2) = -1 := by + have hp : p.natVal = r_scalar := hBn.natVal_eq_r_scalar + have hzn : (nonResidue : ZMod r_scalar) ^ ((r_scalar - 1) / 2) = -1 := nonResidue_euler + have hpsym : r_scalar = p.natVal := hp.symm + have hcast : (ZMod p.natVal) = (ZMod r_scalar) := by rw [hp] + revert hzn + rw [hpsym] + intro hzn + exact hzn + +theorem c0_inv_pow {p : Lampe.Prime} [hBn : Lampe.Crypto.Bn254.Prime p] : + ((nonResidue : Fp p) ^ oddPart) ^ (2 ^ (twoAdicity - 1)) = -1 := by + rw [← pow_mul, oddPart_mul_two_pow_eq] + exact nonResidue_euler_fp + +theorem t0_pow_eq_one {p : Lampe.Prime} [hBn : Lampe.Crypto.Bn254.Prime p] + {a : Fp p} (ha : a ≠ 0) (hQR : ∃ y : Fp p, y * y = a) : + (a ^ oddPart) ^ (2 ^ (twoAdicity - 1)) = 1 := by + rw [← pow_mul, oddPart_mul_two_pow_eq] + exact euler_one_of_exists_sqrt ha hQR + +theorem R0_sq {p : Lampe.Prime} (a : Fp p) : + (a ^ ((oddPart + 1) / 2)) * (a ^ ((oddPart + 1) / 2)) = a * (a ^ oddPart) := by + rw [← pow_add] + have heven : (oddPart + 1) % 2 = 0 := by + have hq := oddPart_odd + omega + have hsum : (oddPart + 1) / 2 + (oddPart + 1) / 2 = oddPart + 1 := by + have := Nat.div_add_mod (oddPart + 1) 2 + omega + rw [hsum, pow_succ, mul_comm] + +theorem tsInv_init {p : Lampe.Prime} [hBn : Lampe.Crypto.Bn254.Prime p] + {a : Fp p} (ha : a ≠ 0) (hQR : ∃ y : Fp p, y * y = a) : + TSInv a twoAdicity + ((nonResidue : Fp p) ^ oddPart) + (a ^ oddPart) + (a ^ ((oddPart + 1) / 2)) := by + refine ⟨?_, ?_, ?_, ?_⟩ + · exact R0_sq a + · exact t0_pow_eq_one ha hQR + · exact c0_inv_pow + · unfold twoAdicity; decide + +/-! ### Step preservation + +The hardest piece: one iteration of `tsStep` preserves `TSInv` and +strictly decreases `M`. The key lemma is that from `t ≠ 1` and +`t^(2^(M-1)) = 1`, we can find a least `i ∈ [1, M)` with `t^(2^i) = 1`. +This `i` is the new `M'`. +-/ + +/-- Specification of `findOrder`: given `acc = t^(2^i)`, `findOrder acc i M fuel` +returns some `j ∈ [i, M]` such that, if `j < M`, then `t^(2^j) = 1`, and `j` +is the smallest such index. Requires `fuel ≥ M - i`. -/ +theorem findOrder_spec {p : Lampe.Prime} (t : Fp p) : + ∀ (fuel : Nat) (i M : Nat), M ≤ i + fuel → i ≤ M → + let j := findOrder (t ^ (2 ^ i)) i M fuel + i ≤ j ∧ j ≤ M ∧ + (j < M → t ^ (2 ^ j) = 1) ∧ + (∀ k, i ≤ k → k < j → t ^ (2 ^ k) ≠ 1) := by + intro fuel + induction fuel with + | zero => + intro i M hfuel hStart + simp only [findOrder] + have hi_eq : i = M := by omega + refine ⟨hStart, le_refl _, ?_, ?_⟩ + · intro h; omega + · intro k hk hkM; omega + | succ fuel ih => + intro i M hfuel hStart + simp only [findOrder] + by_cases hiM : i ≥ M + · rw [if_pos hiM] + refine ⟨hStart, le_refl _, ?_, ?_⟩ + · intro h; omega + · intro k hk hkM; omega + · rw [if_neg hiM] + by_cases hacc : t ^ (2 ^ i) = 1 + · rw [if_pos hacc] + refine ⟨le_refl _, by omega, ?_, ?_⟩ + · intro _; exact hacc + · intro k hk hkM; omega + · rw [if_neg hacc] + have hi1 : i + 1 ≤ M := by omega + have hfuel' : M ≤ (i + 1) + fuel := by omega + have hpow : (t ^ (2 ^ i)) * (t ^ (2 ^ i)) = t ^ (2 ^ (i + 1)) := by + rw [← pow_add, pow_succ] + congr 1 + ring + rw [hpow] + have ih' := ih (i + 1) M hfuel' hi1 + simp only at ih' + obtain ⟨hi1j, hjM, hjfound, hjmin⟩ := ih' + refine ⟨by omega, hjM, hjfound, ?_⟩ + intro k hk hkM + by_cases hki : k = i + · subst hki; exact hacc + · have hkge : i + 1 ≤ k := by omega + exact hjmin k hkge hkM + +theorem findOrder_init_spec {p : Lampe.Prime} (t : Fp p) (M : Nat) (hM : 1 ≤ M) : + let j := findOrder (t * t) 1 M M + 1 ≤ j ∧ j ≤ M ∧ + (j < M → t ^ (2 ^ j) = 1) ∧ + (∀ k, 1 ≤ k → k < j → t ^ (2 ^ k) ≠ 1) := by + have heq : t * t = t ^ (2 ^ 1) := by + show t * t = t ^ 2 + ring + rw [heq] + exact findOrder_spec t M 1 M (by omega) hM + +/-- If `t ≠ 1`, `t^(2^(M-1)) = 1`, `c^(2^(M-1)) = -1`, and `M ≥ 1`, then the +inner search finds a `j ∈ [1, M)`. -/ +theorem findOrder_found_of_tsInv {p : Lampe.Prime} + {a : Fp p} {M : Nat} {c t R : Fp p} (inv : TSInv a M c t R) + (ht : t ≠ 1) : + let j := findOrder (t * t) 1 M M + 1 ≤ j ∧ j < M ∧ t ^ (2 ^ j) = 1 ∧ + (∀ k, 1 ≤ k → k < j → t ^ (2 ^ k) ≠ 1) := by + have hspec := findOrder_init_spec t M inv.Mge + obtain ⟨h1, hM, hfound, hmin⟩ := hspec + -- We need to rule out j = M. + -- If j = M, then we never found, meaning all k ∈ [1, M) satisfy t^(2^k) ≠ 1. + -- But t^(2^(M-1)) = 1 from invariant. + -- If M = 1, then t^(2^0) = t = 1, contradiction with t ≠ 1. + -- If M ≥ 2, then M - 1 ∈ [1, M), so the search must find at most M - 1. + by_cases hM1 : M = 1 + · subst hM1 + -- TSInv has t^(2^0) = 1, i.e., t = 1, contradiction. + have : t = 1 := by + have := inv.tpow + simpa using this + exact absurd this ht + · have hM2 : M ≥ 2 := by omega + have hMm1 : M - 1 < M := by omega + have hMm1_pos : 1 ≤ M - 1 := by omega + -- Suppose findOrder returns M. + -- Then for all k ∈ [1, M), t^(2^k) ≠ 1, contradicting t^(2^(M-1)) = 1. + set j := findOrder (t * t) 1 M M with hjdef + have hjM : j ≤ M := hM + by_cases hjeqM : j = M + · -- contradiction: hmin says no k < M = j satisfies, but inv.tpow does + have := hmin (M - 1) hMm1_pos (by omega) + exact absurd inv.tpow this + · have hjltM : j < M := lt_of_le_of_ne hjM hjeqM + exact ⟨h1, hjltM, hfound hjltM, hmin⟩ + +/-! ### Algebraic step lemmas + +Given the invariants and the found index `j = M' < M`, we now check +that the new state `(M', c', t', R')` produced by `tsStep` satisfies +`TSInv`. The arithmetic facts we need: + +Let `b = c^(2^(M - j - 1))`. Then: +- `c' = b² = c^(2^(M - j))`. We show `c'^(2^(M' - 1)) = -1`, i.e., + `c^(2^(M - j) · 2^(M' - 1)) = c^(2^(M - 1)) = -1`. This holds because + `(M - j) + (M' - 1) = (M - j) + (j - 1) = M - 1`. +- `t' = t · b²`. We show `t'^(2^(M' - 1)) = 1`, i.e., + `t^(2^(M' - 1)) · c^(2^(M - 1)) = 1`. We have `t^(2^(M' - 1)) = t^(2^(j - 1))`. + Squaring this gives `t^(2^j) = 1`, so `t^(2^(j - 1))` is a square root of 1, + i.e., ±1. We must rule out +1 by the minimality of `j`: `t^(2^(j-1)) ≠ 1`. + So `t^(2^(j - 1)) = -1`, and the product is `(-1) · (-1) = 1`. +- `R' = R · b`. We show `R'² = R² · b² = (a · t) · b² = a · (t · b²) = a · t'`. +-/ + +private theorem t_half_sq_eq_one {p : Lampe.Prime} {t : Fp p} {j : Nat} (hj : 1 ≤ j) + (ht : t ^ (2 ^ j) = 1) : (t ^ (2 ^ (j - 1))) ^ 2 = 1 := by + rw [← pow_mul] + have hpow : 2 ^ (j - 1) * 2 = 2 ^ j := by + have : j = (j - 1) + 1 := by omega + conv_rhs => rw [this] + rw [pow_succ] + rw [hpow]; exact ht + +private theorem sq_eq_one_imp_pm_one {p : Lampe.Prime} {x : Fp p} (h : x ^ 2 = 1) : + x = 1 ∨ x = -1 := by + have hfact : (x - 1) * (x + 1) = 0 := by + have hid : (x - 1) * (x + 1) = x ^ 2 - 1 := by ring + rw [hid, h]; ring + rcases mul_eq_zero.mp hfact with h1 | h2 + · left + have : x = 1 := by + have : x - 1 + 1 = 0 + 1 := by rw [h1] + linear_combination h1 + exact this + · right + have : x = -1 := by linear_combination h2 + exact this + +/-- `t^(2^(j-1))` is `-1` when `j` is the minimal positive index with `t^(2^j) = 1` +and `t ≠ 1`. (The case `j = 1` uses `t ≠ 1` to rule out the `+1` branch.) -/ +private theorem t_half_eq_neg_one_of_min {p : Lampe.Prime} {t : Fp p} {j : Nat} (hj : 1 ≤ j) + (ht1 : t ≠ 1) (ht : t ^ (2 ^ j) = 1) (hmin : ∀ k, 1 ≤ k → k < j → t ^ (2 ^ k) ≠ 1) : + t ^ (2 ^ (j - 1)) = -1 := by + have hsq := t_half_sq_eq_one hj ht + rcases sq_eq_one_imp_pm_one hsq with h1 | hneg + · -- t^(2^(j-1)) = 1; need contradiction. + by_cases hj1 : j = 1 + · subst hj1 + -- t^(2^0) = t = 1, contradicts t ≠ 1 + simp at h1 + exact absurd h1 ht1 + · -- j ≥ 2: hmin (j-1) gives contradiction with h1 + have h1' : t ^ (2 ^ (j - 1)) ≠ 1 := hmin (j - 1) (by omega) (by omega) + exact absurd h1 h1' + · exact hneg + +/-! ### Step preservation: one `tsStep` preserves `TSInv` and decreases `M`. -/ + +/-- The auxiliary `b` value used by `tsStep` equals `c ^ (2 ^ (M - j - 1))`. -/ +private theorem tsStep_b_eq {p : Lampe.Prime} (c : Fp p) (M j : Nat) (hjlt : j < M) : + fpowR c (2 ^ (M - j - 1)) (M + 1) = c ^ (2 ^ (M - j - 1)) := by + apply fpowR_eq_pow + -- 2 ^ (M - j - 1) < 2 ^ (M + 1): since M - j - 1 ≤ M - 1 < M + 1. + apply Nat.pow_lt_pow_right (by decide : 1 < 2) + omega + +/-- Step preservation: `tsStep` preserves `TSInv` and gives a strictly smaller `M`. -/ +theorem tsStep_preserves {p : Lampe.Prime} + {a : Fp p} {M : Nat} {c t R : Fp p} + (inv : TSInv a M c t R) (ht : t ≠ 1) : + let (M', c', t', R') := tsStep M c t R + TSInv a M' c' t' R' ∧ M' < M := by + -- Unpack invariants. + have hRsq := inv.Msq + have htpow := inv.tpow + have hcpow := inv.cpow + have hMge := inv.Mge + -- Find the inner index. + have hfound := findOrder_found_of_tsInv inv ht + set j := findOrder (t * t) 1 M M with hjdef + obtain ⟨hj1, hjltM, htj, hjmin⟩ := hfound + -- Compute tsStep with the found j. + simp only [tsStep, ← hjdef] + rw [if_neg (by omega : ¬ j ≥ M)] + -- Define b. + have hb_eq : fpowR c (2 ^ (M - j - 1)) (M + 1) = c ^ (2 ^ (M - j - 1)) := + tsStep_b_eq c M j hjltM + rw [hb_eq] + set b : Fp p := c ^ (2 ^ (M - j - 1)) with hbdef + -- Now the state is (j, b*b, t*(b*b), R*b). + -- Show TSInv a j (b*b) (t*(b*b)) (R*b). + refine ⟨⟨?_, ?_, ?_, hj1⟩, hjltM⟩ + -- (1) R' * R' = a * t'. + · -- (R*b) * (R*b) = (R*R) * (b*b) = a*t * (b*b) = a * (t * (b*b)). + have : (R * b) * (R * b) = (R * R) * (b * b) := by ring + rw [this, hRsq] + ring + -- (2) t'^(2^(j-1)) = 1. + · -- t' = t * (b*b), t'^(2^(j-1)) = t^(2^(j-1)) * (b*b)^(2^(j-1)) + -- = t^(2^(j-1)) * c^(2^(M-1)) + -- = (-1) * (-1) = 1, since t^(2^(j-1)) = -1 by minimality and c^(2^(M-1)) = -1 by inv. + have h_thalf : t ^ (2 ^ (j - 1)) = -1 := + t_half_eq_neg_one_of_min hj1 ht htj hjmin + -- Compute (b*b)^(2^(j-1)) = c^(2^(M-1)) = -1. + have hbb_pow : (b * b) ^ (2 ^ (j - 1)) = -1 := by + -- (b*b)^(2^(j-1)) = b^(2 * 2^(j-1)) = b^(2^j) = c^(2^(M-j-1) * 2^j) = c^(2^(M-1)) + have hbb : b * b = b ^ 2 := by ring + rw [hbb, ← pow_mul] + have hexp : 2 * 2 ^ (j - 1) = 2 ^ j := by + have hjsucc : j = (j - 1) + 1 := by omega + conv_rhs => rw [hjsucc] + rw [pow_succ, Nat.mul_comm] + rw [hexp] + -- Goal: b^(2^j) = -1, where b = c^(2^(M-j-1)). + rw [hbdef, ← pow_mul] + -- Goal: c^(2^(M-j-1) * 2^j) = -1. + have hexp2 : 2 ^ (M - j - 1) * 2 ^ j = 2 ^ (M - 1) := by + rw [← pow_add] + congr 1 + omega + rw [hexp2] + exact hcpow + -- Now expand t'^(2^(j-1)). + have : (t * (b * b)) ^ (2 ^ (j - 1)) = + t ^ (2 ^ (j - 1)) * (b * b) ^ (2 ^ (j - 1)) := by + rw [mul_pow] + rw [this, h_thalf, hbb_pow] + ring + -- (3) c'^(2^(j-1)) = -1. + · -- c' = b*b, c'^(2^(j-1)) = b^(2 * 2^(j-1)) = b^(2^j) = c^(2^(M-1)) = -1. + have hbb : b * b = b ^ 2 := by ring + rw [hbb, ← pow_mul] + have hexp : 2 * 2 ^ (j - 1) = 2 ^ j := by + have hjsucc : j = (j - 1) + 1 := by omega + conv_rhs => rw [hjsucc] + rw [pow_succ, Nat.mul_comm] + rw [hexp, hbdef, ← pow_mul] + have hexp2 : 2 ^ (M - j - 1) * 2 ^ j = 2 ^ (M - 1) := by + rw [← pow_add] + congr 1 + omega + rw [hexp2] + exact hcpow + +/-! ### Loop termination + +The loop terminates within `twoAdicity` iterations and produces `R` with `R*R = a`. -/ + +/-- If `TSInv a M c t R` and `t = 1`, then `R * R = a`. -/ +theorem tsInv_terminal {p : Lampe.Prime} {a : Fp p} {M : Nat} {c t R : Fp p} + (inv : TSInv a M c t R) (ht : t = 1) : R * R = a := by + have := inv.Msq + rw [ht, mul_one] at this + exact this + +/-- The main loop preserves the invariant and terminates: after enough fuel, +the result `R` satisfies `R * R = a`. We do strong induction on `M` (which +decreases each non-terminal iteration). -/ +theorem tonelliLoop_correct {p : Lampe.Prime} {a : Fp p} : + ∀ (fuel : Nat) (M : Nat) (c t R : Fp p), + TSInv a M c t R → M ≤ fuel → + let R' := tonelliLoop a fuel M c t R + R' * R' = a := by + intro fuel + induction fuel with + | zero => + intro M c t R inv hM + -- M ≤ 0 means M = 0, but M ≥ 1 from invariant. Contradiction. + have : M ≥ 1 := inv.Mge + omega + | succ fuel ih => + intro M c t R inv hM + simp only [tonelliLoop] + by_cases ht : t = 1 + · rw [if_pos ht] + exact tsInv_terminal inv ht + · rw [if_neg ht] + -- Apply tsStep_preserves. + have hstep := tsStep_preserves inv ht + -- Destructure the tsStep result. + rcases hstep_eq : tsStep M c t R with ⟨M', c', t', R'⟩ + rw [hstep_eq] at hstep + simp only at hstep + obtain ⟨inv', hMlt⟩ := hstep + have hM' : M' ≤ fuel := by omega + exact ih M' c' t' R' inv' hM' + +set_option exponentiation.threshold 1024 in +/-- Tonelli–Shanks candidate, applied to a QR input, squares to the input. -/ +theorem tonelliCandidate_sq {p : Lampe.Prime} [Lampe.Crypto.Bn254.Prime p] + {a : Fp p} (ha : a ≠ 0) (hQR : ∃ y : Fp p, y * y = a) : + tonelliCandidate a * tonelliCandidate a = a := by + unfold tonelliCandidate + -- oddPart has ~226 bits; bridge via 2^254 to dodge the kernel's + -- exponentiation threshold for `decide`. + have h_bridge : (2 : Nat) ^ 254 ≤ 2 ^ 512 := + Nat.pow_le_pow_right (by omega) (by omega) + have hq : oddPart < 2 ^ 512 := + lt_of_lt_of_le (by unfold oddPart; decide) h_bridge + have hq1 : (oddPart + 1) / 2 < 2 ^ 512 := + lt_of_lt_of_le (by unfold oddPart; decide : (oddPart + 1) / 2 < 2 ^ 254) h_bridge + rw [fpowR_eq_pow _ _ _ hq, fpowR_eq_pow _ _ _ hq, fpowR_eq_pow _ _ _ hq1] + exact tonelliLoop_correct twoAdicity twoAdicity _ _ _ (tsInv_init ha hQR) (le_refl _) + +/-! ### Completeness -/ + +/-- Completeness of `sqrt`: every quadratic residue yields a `some`. +Model-fidelity assurance for the `sqrt` definition; has no downstream +consumers by design. -/ +theorem sqrt_complete {p : Lampe.Prime} [Lampe.Crypto.Bn254.Prime p] {a : Fp p} + (h : ∃ y : Fp p, y * y = a) : (sqrt a).isSome := by + unfold sqrt + by_cases hz : a = 0 + · simp [hz] + · simp [hz] + have hEuler : fpowR a ((r_scalar - 1) / 2) 512 = 1 := by + rw [fpowR_euler_eq_pow] + exact euler_one_of_exists_sqrt hz h + simp [hEuler] + have htc := tonelliCandidate_sq hz h + simp [htc] + +end Lampe.Crypto.Bn254.Sqrt diff --git a/Lampe/Lampe/Crypto/EmbeddedCurve.lean b/Lampe/Lampe/Crypto/EmbeddedCurve.lean index e3a65dc5..c4f175df 100644 --- a/Lampe/Lampe/Crypto/EmbeddedCurve.lean +++ b/Lampe/Lampe/Crypto/EmbeddedCurve.lean @@ -1,4 +1,5 @@ import Lampe.Tp +import Lampe.Crypto.Bn254 import Lampe.Crypto.MathlibBridge import Mathlib.Tactic.Ring @@ -38,8 +39,11 @@ def pointX {p : Prime} (pt : Point p) : Fp p := pt.1 def pointY {p : Prime} (pt : Point p) : Fp p := pt.2.1 def pointIsInfinite {p : Prime} (pt : Point p) : Bool := pt.2.2.1 -def scalarLo {p : Prime} (s : Scalar p) : Fp p := s.1 -def scalarHi {p : Prime} (s : Scalar p) : Fp p := s.2.1 +def Scalar.lo {p : Prime} (s : Scalar p) : Fp p := s.1 +def Scalar.hi {p : Prime} (s : Scalar p) : Fp p := s.2.1 + +@[reducible] +def mkScalar {p : Prime} (lo hi : Fp p) : Scalar p := (lo, hi, ()) @[reducible] def mkPoint {p : Prime} (x y : Fp p) (isInfinite : Bool) : Point p := (x, y, isInfinite, ()) @@ -76,13 +80,409 @@ lemma affineCurve_addY {p : Prime} (x₁ x₂ y₁ slope : Fp p) : simp [WeierstrassCurve.Affine.addY, WeierstrassCurve.Affine.negAddY] ring -def pow128 : Nat := 2 ^ 128 - -def scalarValueNat {p : Prime} (s : Scalar p) : Nat := - (scalarLo s).val + pow128 * (scalarHi s).val +namespace Scalar + +def valueNat {p : Prime} (s : Scalar p) : Nat := + s.lo.val + Lampe.pow128 * s.hi.val + +/-- Per-scalar limb-range canonicality matching the in-circuit constraints +that Barretenberg's MSM gadget (`cycle_group::batch_mul`) emits on every +input scalar via `create_limbed_range_constraint`: + +- `s.lo.val < 2^128` (`LO_BITS = 128`) +- `s.hi.val < 2^126` (`HI_BITS = 126`) + +Together the bounds guarantee a *unique* limb decomposition of a value +below `2^254`. Note `2^254` exceeds the (≈ 254-bit) scalar modulus, so +this is limb-uniqueness, not modular canonicity: a value may still +represent a scalar above the modulus. + +Justified against Barretenberg @ aztec-packages 7e94c2c0e32820e25e20d39a426d546dae56a34f: +* widths: LO_BITS = 128, HI_BITS = 126 (static_asserted), stdlib/primitives/group/cycle_scalar.hpp#L38-L44 +* enforcement: `batch_mul` range-constrains each witness limb via `create_limbed_range_constraint` + (variable-base: straus_scalar_slice.cpp#L58-L60; fixed-base: 128/126-bit plookup multitables, + fixed_base_params.hpp#L30-L31; constant-infinity-point carve-out: cycle_group.cpp#L1266-L1275) +* caveat: scalars whose limbs are both circuit constants are trusted unchecked (Noir only validates + constants against the 254-bit Field width); the bound is backend-enforced only for witness limbs. -/ +def Canonical {p : Prime} (s : Scalar p) : Prop := + s.lo.val < Lampe.pow128 ∧ s.hi.val < 2 ^ 126 + +instance {p : Prime} (s : Scalar p) : Decidable (Canonical s) := by + unfold Canonical + exact instDecidableAnd + +/-! ### Canonical scalar decomposition: existence and uniqueness + +Under `[Bn254.Prime p]`, every field element `f : Fp p` admits a +*unique* canonical limb decomposition `(lo, hi)` that satisfies +`Canonical`, satisfies the canonical-range disjunction enforced +by the stdlib's `from_field_unsafe` (lexicographic comparison against +the prime's own limbs `(plo, phi)`), and sums to `f = lo + 2^128 · hi`. +Existence is constructive: `canonicalDecomp f` is the standard split +`(f.val % 2^128, f.val / 2^128)`. Uniqueness is the Nat-level +uniqueness of binary-expansion limbs. +-/ --- Decidability of `Equation` / `Nonsingular` comes from the generic instances --- in `Lampe.Crypto.MathlibBridge`. +/-- The canonical 128-bit-limb decomposition of a field element: split +`f.val` as `(f.val % 2^128, f.val / 2^128)` and re-embed both halves +into `Fp p`. This is the unique `Canonical` witness whose limbs +sum to `f` (see `canonicalDecomp_unique`). -/ +def canonicalDecomp {p : Prime} (f : Fp p) : Scalar p := + mkScalar + ((f.val % Lampe.pow128 : Nat) : Fp p) + ((f.val / Lampe.pow128 : Nat) : Fp p) + +/-- Limb-value injectivity on canonical scalars: two `Canonical` +scalars with the same `valueNat` have identical limbs. -/ +lemma valueNat_inj_canonical {p : Prime} {s t : Scalar p} + (hs : Canonical s) (ht : Canonical t) + (h : valueNat s = valueNat t) : + s.lo = t.lo ∧ s.hi = t.hi := by + obtain ⟨hslo, hshi⟩ := hs + obtain ⟨htlo, hthi⟩ := ht + simp [valueNat] at h + -- h : (lo s).val + pow128 * (hi s).val = (lo t).val + pow128 * (hi t).val + -- with both .val low limbs < pow128. Apply Nat-level uniqueness, then + -- ZMod.val_injective. + have hval : (lo s).val = (lo t).val ∧ + (hi s).val = (hi t).val := by + refine ⟨?_, ?_⟩ + · -- mod pow128 of both sides extracts lo + have : ((lo s).val + Lampe.pow128 * (hi s).val) % Lampe.pow128 = + ((lo t).val + Lampe.pow128 * (hi t).val) % Lampe.pow128 := by + rw [h] + simp [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hslo, + Nat.mod_eq_of_lt htlo] at this + exact this + · -- div pow128 of both sides extracts hi + have hpos : 0 < Lampe.pow128 := by + simp [Lampe.pow128] + have hdiv : ((lo s).val + Lampe.pow128 * (hi s).val) / Lampe.pow128 = + ((lo t).val + Lampe.pow128 * (hi t).val) / Lampe.pow128 := by + rw [h] + rw [Nat.add_mul_div_left _ _ hpos, Nat.add_mul_div_left _ _ hpos, + Nat.div_eq_of_lt hslo, Nat.div_eq_of_lt htlo] at hdiv + simpa using hdiv + exact ⟨ZMod.val_injective _ hval.1, ZMod.val_injective _ hval.2⟩ + +private lemma p_lt_pow128_sq {p : Prime} [Bn254.Prime p] : + p.natVal < Lampe.pow128 * Lampe.pow128 := by + have hmod : p.natVal = Bn254.plo + Lampe.pow128 * Bn254.phi := + Bn254.Prime.natVal_eq_limbs + have hplo : Bn254.plo < Lampe.pow128 := by + unfold Bn254.plo Lampe.pow128 + decide + have hphi : Bn254.phi < Lampe.pow128 := by + unfold Bn254.phi Lampe.pow128 + decide + -- plo + pow128 * phi < pow128 + pow128 * (pow128 - 1) = pow128 * pow128 + have hphi_le : Bn254.phi + 1 ≤ Lampe.pow128 := + Nat.succ_le_of_lt hphi + have h1 : Bn254.plo + Lampe.pow128 * Bn254.phi + < Lampe.pow128 + Lampe.pow128 * Bn254.phi := + Nat.add_lt_add_right hplo _ + have h2 : Lampe.pow128 + Lampe.pow128 * Bn254.phi = + Lampe.pow128 * (Bn254.phi + 1) := by ring + have h3 : Lampe.pow128 * (Bn254.phi + 1) ≤ Lampe.pow128 * Lampe.pow128 := + Nat.mul_le_mul_left _ hphi_le + calc p.natVal = Bn254.plo + Lampe.pow128 * Bn254.phi := hmod + _ < Lampe.pow128 + Lampe.pow128 * Bn254.phi := h1 + _ = Lampe.pow128 * (Bn254.phi + 1) := h2 + _ ≤ Lampe.pow128 * Lampe.pow128 := h3 + +/-- `canonicalDecomp f` satisfies `Canonical`: the low limb fits +in 128 bits and the high limb in 126 bits. -/ +theorem canonicalDecomp_Canonical {p : Prime} [Bn254.Prime p] + (f : Fp p) : Canonical (canonicalDecomp f) := by + unfold canonicalDecomp Canonical lo hi + refine ⟨?_, ?_⟩ + · -- (((f.val % pow128 : Nat) : Fp p)).val < pow128 + have hmod_lt : f.val % Lampe.pow128 < Lampe.pow128 := by + apply Nat.mod_lt + unfold Lampe.pow128 + decide + have hmod_lt_p : f.val % Lampe.pow128 < p.natVal := + lt_of_lt_of_le hmod_lt (le_of_lt (Bn254.pow128_lt_prime (p := p))) + have : (((f.val % Lampe.pow128 : Nat) : Fp p)).val = f.val % Lampe.pow128 := + ZMod.val_natCast_of_lt hmod_lt_p + rw [this] + exact hmod_lt + · -- (((f.val / pow128 : Nat) : Fp p)).val < 2 ^ 126. + -- f.val < p = plo + pow128 * phi < pow128 * 2^126, so + -- f.val / pow128 < 2^126 — matches the gadget's `HI_BITS = 126`. + have hpos : 0 < Lampe.pow128 := by + unfold Lampe.pow128 + decide + have hf : f.val < p.natVal := f.val_lt + have hmod : p.natVal = Bn254.plo + Lampe.pow128 * Bn254.phi := + Bn254.Prime.natVal_eq_limbs + have hplo_lt_pow : Bn254.plo < Lampe.pow128 := by + unfold Bn254.plo Lampe.pow128 + decide + have hphi_lt_2_126 : Bn254.phi < 2 ^ 126 := by + unfold Bn254.phi + decide + have hphi_succ_le : Bn254.phi + 1 ≤ 2 ^ 126 := + Nat.succ_le_of_lt hphi_lt_2_126 + -- f.val < p ≤ pow128 * (phi + 1) ≤ pow128 * 2^126. + have hp_lt_mul : p.natVal < Lampe.pow128 * (Bn254.phi + 1) := by + have hexp : Lampe.pow128 * (Bn254.phi + 1) = + Lampe.pow128 + Lampe.pow128 * Bn254.phi := by ring + omega + have hp_lt_2_126 : p.natVal < Lampe.pow128 * 2 ^ 126 := + lt_of_lt_of_le hp_lt_mul (Nat.mul_le_mul_left _ hphi_succ_le) + have hf_lt_2_126 : f.val < Lampe.pow128 * 2 ^ 126 := + lt_trans hf hp_lt_2_126 + have hdiv_lt : f.val / Lampe.pow128 < 2 ^ 126 := + Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using hf_lt_2_126) + -- The weaker `< pow128` bound (used to map into Fp via val_natCast_of_lt). + have h2_126_lt_pow128 : (2 : Nat) ^ 126 < Lampe.pow128 := by + unfold Lampe.pow128 + decide + have hdiv_lt_pow : f.val / Lampe.pow128 < Lampe.pow128 := + lt_trans hdiv_lt h2_126_lt_pow128 + have hdiv_lt_p : f.val / Lampe.pow128 < p.natVal := + lt_of_lt_of_le hdiv_lt_pow (le_of_lt (Bn254.pow128_lt_prime (p := p))) + have hval : (((f.val / Lampe.pow128 : Nat) : Fp p)).val = f.val / Lampe.pow128 := + ZMod.val_natCast_of_lt hdiv_lt_p + rw [hval] + exact hdiv_lt + +/-- The canonical decomposition is a decomposition: its limbs sum (in +`Fp p`) to the original field element. -/ +theorem canonicalDecomp_decomposes {p : Prime} [Bn254.Prime p] + (f : Fp p) : + f = (canonicalDecomp f).lo + + ((Lampe.pow128 : Nat) : Fp p) * (canonicalDecomp f).hi := by + unfold canonicalDecomp lo hi + -- Lift the Nat identity `f.val = f.val % pow128 + pow128 * (f.val / pow128)` + -- to `Fp p`. + have hNat : f.val = + f.val % Lampe.pow128 + Lampe.pow128 * (f.val / Lampe.pow128) := by + have := Nat.div_add_mod f.val Lampe.pow128 + omega + have hf : ((f.val : Nat) : Fp p) = f := ZMod.natCast_zmod_val f + calc f = ((f.val : Nat) : Fp p) := hf.symm + _ = ((f.val % Lampe.pow128 + + Lampe.pow128 * (f.val / Lampe.pow128) : Nat) : Fp p) := by rw [← hNat] + _ = ((f.val % Lampe.pow128 : Nat) : Fp p) + + ((Lampe.pow128 * (f.val / Lampe.pow128) : Nat) : Fp p) := by push_cast; ring + _ = ((f.val % Lampe.pow128 : Nat) : Fp p) + + ((Lampe.pow128 : Nat) : Fp p) * + ((f.val / Lampe.pow128 : Nat) : Fp p) := by push_cast; ring + +/-- Nat-level bound: under the `from_field_unsafe` canonical-range +disjunction together with `Canonical`, the Nat sum +`lo.val + pow128 * hi.val` lies in `[0, p)` — i.e. matches `f.val` +without modular wrap. Used by `canonicalDecomp_unique` below. + +The disjunction is essential: branch 1 (`hi = phi ∧ lo.val < plo`) forces +the sum into `[pow128 * phi, p)`; branch 2 (`hi.val < phi`) plus +canonical `lo` forces it into `[0, pow128 * phi)`. Either way, `< p`. -/ +private lemma valueNat_lt_p_of_canonical_disj {p : Prime} + [Bn254.Prime p] {s : Scalar p} + (hcanon : Canonical s) + (hdisj : (s.hi = ((Bn254.phi : Nat) : Fp p) + ∧ s.lo.val < Bn254.plo) + ∨ s.hi.val < Bn254.phi) : + s.lo.val + Lampe.pow128 * s.hi.val < p.natVal := by + obtain ⟨hslo, hshi⟩ := hcanon + have hmod : p.natVal = Bn254.plo + Lampe.pow128 * Bn254.phi := + Bn254.Prime.natVal_eq_limbs + have hphi_lt_pow : Bn254.phi < Lampe.pow128 := by + unfold Bn254.phi Lampe.pow128 + decide + -- (phi : Fp p).val = phi (since phi < pow128 < p). + have hphi_val : ((Bn254.phi : Nat) : Fp p).val = Bn254.phi := by + have hphi_lt_p : Bn254.phi < p.natVal := by + have := Bn254.pow128_lt_prime (p := p) + omega + exact ZMod.val_natCast_of_lt hphi_lt_p + rcases hdisj with ⟨hhi_eq, hlo_lt_plo⟩ | hhi_lt_phi + · -- Branch 1: lo.val < plo, hi.val = phi. + have hhi_val : (hi s).val = Bn254.phi := by + rw [hhi_eq] + exact hphi_val + rw [hhi_val] + omega + · -- Branch 2: hi.val < phi (so + 1 ≤ phi), with lo.val < pow128. + have hbound : (lo s).val + Lampe.pow128 * (hi s).val < + Lampe.pow128 * ((hi s).val + 1) := by + have hexp : Lampe.pow128 * ((hi s).val + 1) = + Lampe.pow128 + Lampe.pow128 * (hi s).val := by ring + rw [hexp] + omega + have hmul_le : Lampe.pow128 * ((hi s).val + 1) ≤ + Lampe.pow128 * Bn254.phi := + Nat.mul_le_mul_left _ hhi_lt_phi + have hle_p : Lampe.pow128 * Bn254.phi ≤ p.natVal := by + rw [hmod] + omega + linarith + +/-- The two main consequences used by uniqueness, packaged as the +`valueNat`-vs-`Fp p`-val bridge: under disjunction + canonical, +the prover's Nat sum equals `f.val`. -/ +private lemma valueNat_eq_val_of_canonical_disj {p : Prime} + [Bn254.Prime p] {f : Fp p} {s : Scalar p} + (hcanon : Canonical s) + (hdisj : (s.hi = ((Bn254.phi : Nat) : Fp p) + ∧ s.lo.val < Bn254.plo) + ∨ s.hi.val < Bn254.phi) + (hdecomp : f = s.lo + ((Lampe.pow128 : Nat) : Fp p) * s.hi) : + valueNat s = f.val := by + have hpow_val : ((Lampe.pow128 : Nat) : Fp p).val = Lampe.pow128 := + Bn254.pow128_val (p := p) + have hsum_lt_p : (lo s).val + Lampe.pow128 * (hi s).val < p.natVal := + valueNat_lt_p_of_canonical_disj hcanon hdisj + have hmul_lt : Lampe.pow128 * (hi s).val < p.natVal := by + have := Nat.le_add_left (Lampe.pow128 * (hi s).val) (lo s).val + omega + have hmul_lt' : ((Lampe.pow128 : Nat) : Fp p).val * (hi s).val < p.natVal := by + rw [hpow_val] + exact hmul_lt + have hmul_val : (((Lampe.pow128 : Nat) : Fp p) * hi s).val = + Lampe.pow128 * (hi s).val := by + rw [ZMod.val_mul_of_lt hmul_lt', hpow_val] + have hsum_lt : (lo s).val + + (((Lampe.pow128 : Nat) : Fp p) * hi s).val < p.natVal := by + rw [hmul_val] + exact hsum_lt_p + have hsum_val : (lo s + ((Lampe.pow128 : Nat) : Fp p) * hi s).val = + (lo s).val + (((Lampe.pow128 : Nat) : Fp p) * hi s).val := + ZMod.val_add_of_lt hsum_lt + have hf_val : f.val = (lo s).val + Lampe.pow128 * (hi s).val := by + have := congrArg ZMod.val hdecomp + rw [hsum_val, hmul_val] at this + exact this + unfold valueNat + omega + +/-- **Canonical-limb uniqueness**: any decomposition `s` of a field +element `f` that is `Canonical` AND satisfies the +`from_field_unsafe` canonical-range disjunction agrees with +`canonicalDecomp f`. + +Combined with `canonicalDecomp_Canonical` and `canonicalDecomp_decomposes`, +this is the existence-and-uniqueness statement +`∃! s, Canonical s ∧ disj s ∧ f = s.lo + 2^128 · s.hi` from the +MSM canonicalization plan. + +The canonical-range disjunction is essential — *both* `Canonical` +limbs alone do not suffice for uniqueness over BN254 (where +`pow128^2 ≈ 4·p`, so a canonical pair can decompose `0` either as +`(0, 0)` or as `(plo, phi)`). The disjunction breaks the tie. -/ +theorem canonicalDecomp_unique {p : Prime} [Bn254.Prime p] + {f : Fp p} {s : Scalar p} + (hcanon : Canonical s) + (hdisj : (s.hi = ((Bn254.phi : Nat) : Fp p) + ∧ s.lo.val < Bn254.plo) + ∨ s.hi.val < Bn254.phi) + (hdecomp : f = s.lo + ((Lampe.pow128 : Nat) : Fp p) * s.hi) : + s = canonicalDecomp f := by + -- Both s and canonicalDecomp f are canonical decomps of f whose Nat sums + -- lie in [0, p). Hence their Nat sums equal f.val, so they agree as + -- `valueNat`. Then `valueNat_inj_canonical` gives equal limbs. + have hcanon' : Canonical (canonicalDecomp f) := + canonicalDecomp_Canonical f + have hf_decomp : f = lo (canonicalDecomp f) + + ((Lampe.pow128 : Nat) : Fp p) * hi (canonicalDecomp f) := + canonicalDecomp_decomposes f + -- canonicalDecomp's limbs satisfy the disjunction: its Nat sum equals f.val < p, + -- which forces either hi = phi ∧ lo < plo (when f.val ≥ pow128*phi) + -- or hi.val < phi (when f.val < pow128*phi). + have hd_disj : + (hi (canonicalDecomp f) = ((Bn254.phi : Nat) : Fp p) + ∧ (lo (canonicalDecomp f)).val < Bn254.plo) + ∨ (hi (canonicalDecomp f)).val < Bn254.phi := by + -- Argue from f.val < p = plo + pow128*phi. + have hmod : p.natVal = Bn254.plo + Lampe.pow128 * Bn254.phi := + Bn254.Prime.natVal_eq_limbs + have hpow_pos : 0 < Lampe.pow128 := by + unfold Lampe.pow128 + decide + have hf_lt : f.val < p.natVal := f.val_lt + -- (lo, hi) = (f.val % pow128, f.val / pow128). Use Nat.div_add_mod. + have hdm : f.val % Lampe.pow128 + Lampe.pow128 * (f.val / Lampe.pow128) = f.val := by + have := Nat.div_add_mod f.val Lampe.pow128 + omega + -- Identify lo.val and hi.val on the canonicalDecomp side. + have hlo_val : (lo (canonicalDecomp f)).val = f.val % Lampe.pow128 := by + unfold canonicalDecomp lo mkScalar + have hmod_lt_p : f.val % Lampe.pow128 < p.natVal := by + have := Nat.mod_lt f.val hpow_pos + have := Bn254.pow128_lt_prime (p := p) + omega + exact ZMod.val_natCast_of_lt hmod_lt_p + have hhi_val : (hi (canonicalDecomp f)).val = f.val / Lampe.pow128 := by + unfold canonicalDecomp hi mkScalar + have hp_sq := p_lt_pow128_sq (p := p) + have hf_lt_sq : f.val < Lampe.pow128 * Lampe.pow128 := lt_trans hf_lt hp_sq + have hdiv_lt : f.val / Lampe.pow128 < Lampe.pow128 := + Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using hf_lt_sq) + have hdiv_lt_p : f.val / Lampe.pow128 < p.natVal := by + have := Bn254.pow128_lt_prime (p := p) + omega + exact ZMod.val_natCast_of_lt hdiv_lt_p + -- Now case-split on whether f.val < pow128 * phi. + by_cases hcase : f.val < Lampe.pow128 * Bn254.phi + · right + rw [hhi_val] + -- f.val < pow128 * phi ⟹ f.val / pow128 < phi. + exact Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using hcase) + · left + replace hcase : Lampe.pow128 * Bn254.phi ≤ f.val := Nat.le_of_not_lt hcase + -- f.val ≥ pow128 * phi and f.val < p = plo + pow128*phi. + -- So f.val = pow128*phi + r where r ∈ [0, plo). + have hr_lo : f.val - Lampe.pow128 * Bn254.phi < Bn254.plo := by + omega + -- f.val / pow128 = phi when pow128*phi ≤ f.val < pow128*(phi+1), + -- and the upper bound is f.val < pow128*phi + pow128 (follows from r < plo < pow128). + have hplo_lt_pow : Bn254.plo < Lampe.pow128 := by + unfold Bn254.plo Lampe.pow128 + decide + have hf_lt' : f.val < Lampe.pow128 * (Bn254.phi + 1) := by + have : Lampe.pow128 * (Bn254.phi + 1) = + Lampe.pow128 * Bn254.phi + Lampe.pow128 := by ring + omega + have hdiv_eq : f.val / Lampe.pow128 = Bn254.phi := by + apply Nat.div_eq_of_lt_le + · rw [Nat.mul_comm] + exact hcase + · rw [Nat.mul_comm] + exact hf_lt' + refine ⟨?_, ?_⟩ + · -- Goal: hi (canonicalDecomp f) = (↑phi : Fp p). Since + -- hi := ((f.val / pow128 : Nat) : Fp p) and f.val / pow128 = phi. + unfold canonicalDecomp hi mkScalar + rw [hdiv_eq] + · -- Goal: (lo (canonicalDecomp f)).val < plo. + rw [hlo_val] + -- f.val % pow128 = f.val - pow128*phi (since pow128*phi ≤ f.val < pow128*(phi+1)). + have hmod_eq : f.val % Lampe.pow128 = f.val - Lampe.pow128 * Bn254.phi := by + have hsub : f.val = (f.val - Lampe.pow128 * Bn254.phi) + + Lampe.pow128 * Bn254.phi := by omega + conv_lhs => rw [hsub] + rw [Nat.add_mul_mod_self_left, + Nat.mod_eq_of_lt (lt_of_lt_of_le hr_lo (le_of_lt hplo_lt_pow))] + omega + -- Both sides have equal valueNat (= f.val). + have hs_val_eq : valueNat s = f.val := + valueNat_eq_val_of_canonical_disj hcanon hdisj hdecomp + have hd_val_eq : valueNat (canonicalDecomp f) = f.val := + valueNat_eq_val_of_canonical_disj hcanon' hd_disj hf_decomp + -- Combine: valueNat agrees, so limbs agree. + have hv_eq : valueNat s = valueNat (canonicalDecomp f) := by + rw [hs_val_eq, hd_val_eq] + obtain ⟨hlo_eq, hhi_eq⟩ := valueNat_inj_canonical hcanon hcanon' hv_eq + -- s and canonicalDecomp f are 3-tuples (lo, hi, ()); equality of lo, hi + -- gives equality. + obtain ⟨slo, shi, ⟨⟩⟩ := s + simp only [lo, hi] at hlo_eq hhi_eq + show ((slo, shi, PUnit.unit) : Scalar p) = canonicalDecomp f + rw [hlo_eq, hhi_eq] + +end Scalar def curvePoint? {p : Prime} (pt : Point p) : Option ((affineCurve p).Point) := if pointIsInfinite pt then diff --git a/Lampe/Lampe/Crypto/Pedersen.lean b/Lampe/Lampe/Crypto/Pedersen.lean new file mode 100644 index 00000000..93c77830 --- /dev/null +++ b/Lampe/Lampe/Crypto/Pedersen.lean @@ -0,0 +1,299 @@ +import Lampe.Tp +import Lampe.Crypto.EmbeddedCurve +import Lampe.Crypto.Blake3 +import Lampe.Crypto.Bn254 +import Lampe.Crypto.Bn254.Sqrt + +/-! +# Pedersen generator derivation — concrete model + +This module formalizes Noir's `derive_pedersen_generators` foreign +builtin (stdlib `std::hash::derive_generators`). The Noir compiler +dispatches this builtin to Barretenberg's `derive_generators` +routine, which deterministically hashes a domain-separator byte +string together with an index to produce a stream of points on +Grumpkin (`y^2 = x^3 - 17`) via a hash-to-curve construction +(BLAKE3 + try-and-increment). + +The implementation transcribes Barretenberg's +`affine_element::hash_to_curve` (file +`barretenberg/cpp/src/barretenberg/ecc/groups/affine_element_impl.hpp`) +and the surrounding `derive_generators` wrapper. The generator +returned by `pedersenGeneratorPoint p domain index` is: + +1. Build a 64-byte preimage `BLAKE3(domain) || BE32(index) || zeros(28)`. +2. For `attempt = 0, 1, …` (bounded by 256): + - Compute `hash_hi = BLAKE3(preimage ‖ attempt ‖ 0)` and + `hash_lo = BLAKE3(preimage ‖ attempt ‖ 1)`. + - Read both as big-endian 256-bit integers, concatenate as + `n_hi · 2^256 + n_lo`, and reduce modulo `p` to obtain + `x : Fp p`. + - Take the parity bit from the top bit of `hash_hi[0]`. + - Compute `yy = x^3 + curveB` (curveB = -17 for Grumpkin) and + attempt `sqrt yy` via Tonelli-Shanks. + - On success, pick the candidate root whose parity matches the + parity bit; verify via `curvePoint?` that the resulting + `(x, y, false)` lies on the affine curve. If yes, return the + corresponding Mathlib point. + +The Tonelli-Shanks square root (`Lampe.Crypto.Bn254.Sqrt.sqrt`) is only +defined when `p` is the BN254 scalar-field prime. For other primes +the function returns the point at infinity (a meaningless +placeholder; downstream specs always instantiate `p` to the BN254 +scalar prime). This is encoded via a dependent-`if` on +`p.natVal = r_scalar`, with the `Lampe.Crypto.Bn254.Prime p` instance derived +from the equality witness on the success branch. +-/ + +namespace Lampe.Crypto.Pedersen + +open Lampe.Crypto.EmbeddedCurve +open Lampe.Crypto.Blake3 +open Lampe.Crypto.Bn254 (r_scalar) +open Lampe.Crypto.Bn254.Sqrt + +/-! ### Byte-buffer plumbing -/ + +/-- Read the first 32 bytes of `bytes` as a big-endian 256-bit +unsigned integer. Positions past the array bound are treated as +zero. -/ +private def bytesToBigEndianU256 (bytes : Array (BitVec 8)) : Nat := Id.run do + let mut acc : Nat := 0 + for i in [:32] do + let b : Nat := (bytes.getD i 0).toNat + acc := acc * 256 + b + return acc + +private def domainListToBytes (domain : List (BitVec 8)) : Array (BitVec 8) := + domain.toArray + +/-- Build the 64-byte preimage `BLAKE3(domain) ‖ BE32(index) ‖ 0×28` +that seeds the per-index hash-to-curve loop. -/ +private def makePreimage (domain : List (BitVec 8)) (index : Nat) : Array (BitVec 8) := Id.run do + let domainBytes := domainListToBytes domain + let domainHash := blake3HashBytes domainBytes + let mut preimage : Array (BitVec 8) := Array.replicate 64 0 + -- First 32 bytes: BLAKE3(domain). + for i in [:32] do + preimage := preimage.set! i (domainHash.getD i 0) + -- Bytes [32, 36): big-endian u32 encoding of `index`. + preimage := preimage.set! 32 (BitVec.ofNat 8 ((index >>> 24) &&& 0xff)) + preimage := preimage.set! 33 (BitVec.ofNat 8 ((index >>> 16) &&& 0xff)) + preimage := preimage.set! 34 (BitVec.ofNat 8 ((index >>> 8) &&& 0xff)) + preimage := preimage.set! 35 (BitVec.ofNat 8 (index &&& 0xff)) + -- Bytes [36, 64) are already zero from `Array.replicate`. + return preimage + +/-- Append the attempt counter and a 1-byte tag (0 for the high half, +1 for the low half) to the 64-byte preimage to produce the 66-byte +BLAKE3 input for one hash-to-curve attempt. -/ +private def makeAttemptSeed (preimage : Array (BitVec 8)) + (count tag : Nat) : Array (BitVec 8) := + preimage.push (BitVec.ofNat 8 count) |>.push (BitVec.ofNat 8 tag) + +/-! ### Hash-to-curve inner loop -/ + +/-- Try to lift `(x, y)` to a Mathlib affine point with the requested +parity, retrying with `-y` if needed. Returns `none` when the +candidate `(x, ±y)` fails the on-curve check. -/ +private def liftWithParity {p : Prime} (x y : Fp p) (signBit : Bool) : + Option ((affineCurve p).Point) := + let y_final : Fp p := + if (y.val % 2 == 1) == signBit then y else (-y) + curvePoint? (mkPoint x y_final false) + +/-- +Single hash-to-curve attempt for `(preimage, attempt)`. Builds the +two BLAKE3 outputs, derives an `x` coordinate, attempts to compute +`y = sqrt(x^3 + B)`, and lifts to a Mathlib point with the parity +encoded in the high bit of `hash_hi[0]`. +-/ +private def hashToCurveAttempt {p : Prime} [Lampe.Crypto.Bn254.Prime p] + (preimage : Array (BitVec 8)) (attempt : Nat) : + Option ((affineCurve p).Point) := + let seedHi := makeAttemptSeed preimage attempt 0 + let seedLo := makeAttemptSeed preimage attempt 1 + let hashHi := blake3HashBytes seedHi + let hashLo := blake3HashBytes seedLo + let nHi : Nat := bytesToBigEndianU256 hashHi + let nLo : Nat := bytesToBigEndianU256 hashLo + let combined : Nat := nHi * (2 ^ 256) + nLo + let x : Fp p := (combined : Nat) + let signBit : Bool := (hashHi.getD 0 0).toNat >>> 7 == 1 + let yy : Fp p := x * x * x + curveB + match sqrt yy with + | some yCand => liftWithParity x yCand signBit + | none => none + +/-- Hash-to-curve loop, bounded by 256 attempts. The probability that +a uniformly random `x` is the x-coordinate of a Grumpkin point is +≈ 1/2, so the expected number of iterations is 2; 256 attempts is +astronomically generous. -/ +private def hashToCurve {p : Prime} [Lampe.Crypto.Bn254.Prime p] + (preimage : Array (BitVec 8)) : (affineCurve p).Point := Id.run do + for attempt in [:256] do + match hashToCurveAttempt preimage attempt with + | some pt => return pt + | none => continue + -- Statistically unreachable: the probability of failing 256 times + -- is ≈ 2^(-256). Fall through with the identity element. + return 0 + +/-- Concrete BN254-scalar generator builder. Combines `makePreimage` +with the bounded `hashToCurve` loop. -/ +def pedersenGenerator {p : Prime} [Lampe.Crypto.Bn254.Prime p] + (domain : List (BitVec 8)) (index : Nat) : (affineCurve p).Point := + hashToCurve (makePreimage domain index) + +/-! ### Public per-index generator -/ + +/-- +Per-index Pedersen generator derivation. + +When `p` is the BN254 scalar prime, this runs Barretenberg's +hash-to-curve algorithm (BLAKE3 + Tonelli-Shanks) and returns the +encoded Grumpkin generator. For any other prime, the function +returns the point at infinity; downstream specs only instantiate +`p` at BN254, so the non-BN254 branch is never observed. +-/ +def pedersenGeneratorPoint (p : Prime) (domain : List (BitVec 8)) (index : Nat) : Point p := + if h : p.natVal = r_scalar then + haveI : Lampe.Crypto.Bn254.Prime p := ⟨h⟩ + encodeCurvePoint (pedersenGenerator (p := p) domain index) + else + pointAtInfinity + +/-- Bridge: `pedersenGeneratorPoint` is the encoding of `pedersenGenerator` +under any `Lampe.Crypto.Bn254.Prime p` instance. Used by stdlib specs to discharge the +`encodeCurvePoint (Ps.get i) = pedersenGeneratorPoint …` obligation that +`multi_scalar_mul_spec` expects. -/ +@[simp] theorem pedersenGeneratorPoint_eq {p : Prime} [Lampe.Crypto.Bn254.Prime p] + (domain : List (BitVec 8)) (index : Nat) : + pedersenGeneratorPoint p domain index = + encodeCurvePoint (pedersenGenerator (p := p) domain index) := by + unfold pedersenGeneratorPoint + have h : p.natVal = r_scalar := Lampe.Crypto.Bn254.Prime.natVal_eq_r_scalar + rw [dif_pos h] + +/-- Build a length-`N` vector of generators starting at `startIndex`. -/ +def derivePedersenGeneratorsList (p : Prime) (domain : List (BitVec 8)) (startIndex N : Nat) : + List (Point p) := + (List.range N).map (fun i => pedersenGeneratorPoint p domain (startIndex + i)) + +theorem derivePedersenGeneratorsList_length (p : Prime) (domain : List (BitVec 8)) + (startIndex N : Nat) : + (derivePedersenGeneratorsList p domain startIndex N).length = N := by + simp [derivePedersenGeneratorsList] + +/-- The semantic model used by the builtin descriptor: a `List.Vector` +of exactly `N` generators. -/ +def derivePedersenGenerators (p : Prime) (domain : List (BitVec 8)) (startIndex N : Nat) : + List.Vector (Point p) N := + ⟨derivePedersenGeneratorsList p domain startIndex N, + derivePedersenGeneratorsList_length p domain startIndex N⟩ + +@[simp] theorem derivePedersenGenerators_get (p : Prime) (domain : List (BitVec 8)) + (startIndex N : Nat) (i : Fin N) : + (derivePedersenGenerators p domain startIndex N).get i = + pedersenGeneratorPoint p domain (startIndex + i.val) := by + simp [derivePedersenGenerators, derivePedersenGeneratorsList, + List.Vector.get, List.get_eq_getElem] + +@[simp] theorem derivePedersenGenerators_toList (p : Prime) (domain : List (BitVec 8)) + (startIndex N : Nat) : + (derivePedersenGenerators p domain startIndex N).toList = + derivePedersenGeneratorsList p domain startIndex N := rfl + +/-- Bridging lemma: a generator vector derived by +`derivePedersenGenerators` is the `encodeCurvePoint`-image of any +Mathlib point vector `Ps` that agrees with `pedersenGeneratorPoint` +index-wise. Used by stdlib specs to discharge the encoded-points +hypothesis that `multi_scalar_mul_spec` expects. -/ +theorem derivePedersenGenerators_h_enc {p : Prime} {n : Nat} + {domain : List (BitVec 8)} {start : Nat} + {Ps : List.Vector (affineCurve p).Point n} + (h_gen : ∀ i, + encodeCurvePoint (Ps.get i) = + pedersenGeneratorPoint p domain (start + i.val)) : + (derivePedersenGenerators p domain start n).toList = + Ps.toList.map encodeCurvePoint := by + rw [← List.Vector.toList_map] + apply congrArg List.Vector.toList + apply List.Vector.ext + intro i + rw [derivePedersenGenerators_get, + List.Vector.get_map, ← h_gen i] + +/-! ### Pure Pedersen commitment and hash -/ + +/-- ASCII byte vector for the literal `"DEFAULT_DOMAIN_SEPARATOR"` +(24 bytes). Used by `pedersen_commitment_with_separator` and +`pedersen_hash_with_separator`. -/ +def defaultDomainBytes : List (BitVec 8) := + [68, 69, 70, 65, 85, 76, 84, 95, -- "DEFAULT_" + 68, 79, 77, 65, 73, 78, 95, -- "DOMAIN_" + 83, 69, 80, 65, 82, 65, 84, 79, 82] -- "SEPARATOR" + +/-- ASCII byte vector for the literal `"pedersen_hash_length"` +(20 bytes). Used by `pedersen_hash_with_separator` for the +length-slot generator. -/ +def pedersenHashLengthBytes : List (BitVec 8) := + [112, 101, 100, 101, 114, 115, 101, 110, 95, -- "pedersen_" + 104, 97, 115, 104, 95, -- "hash_" + 108, 101, 110, 103, 116, 104] -- "length" + +/-- Pure Pedersen commitment: canonically decompose each input field +element into limbs, scale the per-index generator +`pedersenGenerator domain (separator + i)` by the limb value, sum, and +encode the resulting curve point. This is the exact closed form that +the stdlib `pedersen_commitment*_spec_canonical` theorems guarantee +for Noir's `std::hash::pedersen_commitment_with_separator`. -/ +def pedersenCommitment (p : Prime) [Lampe.Crypto.Bn254.Prime p] + (domain : List (BitVec 8)) {n : Nat} + (inputs : List.Vector (Fp p) n) (separator : Nat) : Point p := + encodeCurvePoint + (∑ i : Fin n, + Scalar.valueNat (Scalar.canonicalDecomp (inputs.get i)) • + pedersenGenerator (p := p) domain (separator + i.val)) + +/-- Unfolding lemma for `pedersenCommitment`, in the shape produced by +the stdlib `_spec_canonical` proofs. -/ +theorem pedersenCommitment_eq (p : Prime) [Lampe.Crypto.Bn254.Prime p] + (domain : List (BitVec 8)) {n : Nat} + (inputs : List.Vector (Fp p) n) (separator : Nat) : + pedersenCommitment p domain inputs separator = + encodeCurvePoint + (∑ i : Fin n, + Scalar.valueNat (Scalar.canonicalDecomp (inputs.get i)) • + pedersenGenerator (p := p) domain (separator + i.val)) := rfl + +/-- Pure Pedersen hash: the x-coordinate of the Pedersen commitment +MSM extended with the length-slot term +`n • pedersenGenerator pedersenHashLengthBytes 0` (the length-slot +domain is fixed by Barretenberg regardless of `domain`). This is the +exact closed form that the stdlib `pedersen_hash*_spec_canonical` +theorems guarantee for Noir's `std::hash::pedersen_hash_with_separator`. -/ +def pedersenHash (p : Prime) [Lampe.Crypto.Bn254.Prime p] + (domain : List (BitVec 8)) {n : Nat} + (inputs : List.Vector (Fp p) n) (separator : Nat) : Fp p := + pointX + (encodeCurvePoint + ((∑ i : Fin n, + Scalar.valueNat (Scalar.canonicalDecomp (inputs.get i)) • + pedersenGenerator (p := p) domain (separator + i.val)) + + n • pedersenGenerator (p := p) pedersenHashLengthBytes 0)) + +/-- Unfolding lemma for `pedersenHash`, in the shape produced by the +stdlib `_spec_canonical` proofs. -/ +theorem pedersenHash_eq (p : Prime) [Lampe.Crypto.Bn254.Prime p] + (domain : List (BitVec 8)) {n : Nat} + (inputs : List.Vector (Fp p) n) (separator : Nat) : + pedersenHash p domain inputs separator = + pointX + (encodeCurvePoint + ((∑ i : Fin n, + Scalar.valueNat (Scalar.canonicalDecomp (inputs.get i)) • + pedersenGenerator (p := p) domain (separator + i.val)) + + n • pedersenGenerator (p := p) pedersenHashLengthBytes 0)) := rfl + +end Lampe.Crypto.Pedersen diff --git a/Lampe/Lampe/Data/Field.lean b/Lampe/Lampe/Data/Field.lean index b8fa0d5e..0051c0a6 100644 --- a/Lampe/Lampe/Data/Field.lean +++ b/Lampe/Lampe/Data/Field.lean @@ -87,6 +87,12 @@ instance {n : ℕ} {p : Prime} [BitsGT p (n + 1)] : BitsGT p n where end Prime +/-- `2^128` as a `Nat`. Shared between BN254 limb decomposition and the +embedded-curve scalar split: both Noir's `from_field_unsafe` BN254 split +and Barretenberg's MSM gadget (`cycle_group::batch_mul`) use this constant +as the low-limb base. -/ +def pow128 : Nat := 2 ^ 128 + @[reducible] def Fp (P : Prime) := ZMod P.natVal instance : DecidableEq (Fp P) := inferInstanceAs (DecidableEq (ZMod P.natVal)) diff --git a/Lampe/Lampe/Tactic/Steps.lean b/Lampe/Lampe/Tactic/Steps.lean index 7789dadf..8cd1584e 100644 --- a/Lampe/Lampe/Tactic/Steps.lean +++ b/Lampe/Lampe/Tactic/Steps.lean @@ -204,6 +204,9 @@ def getClosingTerm (val : Lean.Expr) : TacticM (Option (TSyntax `term)) := withT | ``Lampe.Builtin.zeroed => return some (←``(genericTotalPureBuiltin_intro Builtin.zeroed rfl)) + | ``Lampe.Builtin.assertConstant => + return some (←``(genericTotalPureBuiltin_intro Builtin.assertConstant (a := _) rfl)) + | _ => return none | _ => return none diff --git a/Lampe/Tests/EmbeddedCurveOps.lean b/Lampe/Tests/EmbeddedCurveOps.lean new file mode 100644 index 00000000..8d32b8d8 --- /dev/null +++ b/Lampe/Tests/EmbeddedCurveOps.lean @@ -0,0 +1,115 @@ +import Lampe.Crypto.Bn254.Prime +import Lampe.Crypto.EmbeddedCurve + +/-! +# Canonical-decomposition validation vectors + +Concrete `native_decide` tests on the `Scalar.canonicalDecomp` / +`Scalar.Canonical` machinery introduced for the Pedersen wrapper +deterministic corollaries. Tests cover edge cases (`f = 0`, `f = 1`, +`f = p - 1`, the boundary `pow128`, and the `(plo, phi)` collision +point that the uniqueness lemma rules out) plus a handful of +random-looking values. + +The tests verify three properties for each chosen `f`: + +1. `Scalar.canonicalDecomp f` satisfies `Scalar.Canonical` + (limb-range canonicality: `lo.val < 2^128 ∧ hi.val < 2^126`). +2. `Scalar.canonicalDecomp f` recovers `f` via the limb identity + `f = lo + 2^128 · hi`. +3. `Scalar.canonicalDecomp` agrees with the explicit `(0, 0)` decomposition + on `f = 0`, ruling out the spurious `(plo, phi)` alternative. + +These exercise the machinery the Pedersen `_spec_canonical` corollaries +depend on (`Scalar.canonicalDecomp_unique`, `Scalar.canonicalDecomp_decomposes`, +`Scalar.canonicalDecomp_Canonical`). +-/ + +namespace Tests.EmbeddedCurveOps + +open Lampe (Fp Prime) +open Lampe.Crypto.EmbeddedCurve + +/-- BN254 scalar field prime — the field for embedded-curve scalars. -/ +abbrev P : Lampe.Prime := Lampe.Crypto.Bn254.prime + +/-! ### `Scalar.Canonical` holds on `Scalar.canonicalDecomp` -/ + +/-- `Scalar.canonicalDecomp 0 = (0, 0)` and is canonical. -/ +example : Scalar.Canonical (Scalar.canonicalDecomp (0 : Fp P)) := by + native_decide + +/-- `Scalar.canonicalDecomp 1 = (1, 0)` and is canonical. -/ +example : Scalar.Canonical (Scalar.canonicalDecomp (1 : Fp P)) := by + native_decide + +/-- `Scalar.canonicalDecomp (p - 1) = (plo - 1, phi)` and is canonical (high +limb is `phi`, just below the `2^126` bound; low limb is `plo - 1`, +just below the `2^128` bound). -/ +example : Scalar.Canonical (Scalar.canonicalDecomp (-1 : Fp P)) := by + native_decide + +/-- `Scalar.canonicalDecomp (pow128) = (0, 1)` — boundary between low- and +high-limb regimes. -/ +example : + Scalar.Canonical (Scalar.canonicalDecomp ((Lampe.pow128 : Nat) : Fp P)) := by + native_decide + +/-- `Scalar.canonicalDecomp (pow128 - 1) = (pow128 - 1, 0)` — largest pure-low +value. -/ +example : + Scalar.Canonical (Scalar.canonicalDecomp ((Lampe.pow128 - 1 : Nat) : Fp P)) := by + native_decide + +/-- `Scalar.canonicalDecomp (pow128 * phi) = (0, phi)` — top of the +canonical-range branch (a) boundary. -/ +example : + Scalar.Canonical + (Scalar.canonicalDecomp + ((Lampe.pow128 * Lampe.Crypto.Bn254.phi : Nat) : Fp P)) := by + native_decide + +/-- A random-looking value in the middle of the field. -/ +example : + Scalar.Canonical + (Scalar.canonicalDecomp + ((12345678901234567890123456789012345678901234567890123456789012345 : Nat) : Fp P)) := by + native_decide + +/-! ### `Scalar.canonicalDecomp` recovers `f` via the limb identity -/ + +/-- The limb identity `f = lo + 2^128 · hi` holds on `f = pow128 + 7`. -/ +example : + let f : Fp P := ((Lampe.pow128 + 7 : Nat) : Fp P) + let s := Scalar.canonicalDecomp f + f = Scalar.lo s + ((Lampe.pow128 : Nat) : Fp P) * Scalar.hi s := by + native_decide + +/-- The limb identity holds on `f = p - 1` (the wraparound edge case). -/ +example : + let f : Fp P := (-1 : Fp P) + let s := Scalar.canonicalDecomp f + f = Scalar.lo s + ((Lampe.pow128 : Nat) : Fp P) * Scalar.hi s := by + native_decide + +/-! ### Uniqueness corner case: `f = 0` resolves to `(0, 0)`, not `(plo, phi)` -/ + +/-- On `f = 0`, `Scalar.canonicalDecomp` picks the `(0, 0)` witness, not the +arithmetically-equivalent `(plo, phi)` witness. This is the +counterexample to "any canonical-range decomposition of a field +element is unique" — the `Scalar.canonicalDecomp_unique` lemma's +`hdisj` hypothesis breaks the tie. -/ +example : + (Scalar.lo (Scalar.canonicalDecomp (0 : Fp P))).val = 0 ∧ + (Scalar.hi (Scalar.canonicalDecomp (0 : Fp P))).val = 0 := by + native_decide + +/-- The spurious `(plo, phi)` witness is **not** what `Scalar.canonicalDecomp` +returns on `f = 0`, even though it satisfies the limb identity +`plo + 2^128 · phi = p ≡ 0 (mod p)`. -/ +example : + (Scalar.lo (Scalar.canonicalDecomp (0 : Fp P))).val ≠ Lampe.Crypto.Bn254.plo ∨ + (Scalar.hi (Scalar.canonicalDecomp (0 : Fp P))).val ≠ Lampe.Crypto.Bn254.phi := by + native_decide + +end Tests.EmbeddedCurveOps diff --git a/Lampe/Tests/Pedersen.lean b/Lampe/Tests/Pedersen.lean new file mode 100644 index 00000000..c5c6b7fa --- /dev/null +++ b/Lampe/Tests/Pedersen.lean @@ -0,0 +1,205 @@ +import Lampe.Crypto.Bn254.Prime +import Lampe.Crypto.Pedersen + +/-! +# Pedersen reference vectors + +Verifies the pure `pedersenCommitment` and `pedersenHash` functions +(`Lampe.Crypto.Pedersen`) — the exact closed +forms guaranteed by the stdlib `_spec_canonical` theorems — against +Aztec's published test vectors (from `assert_pedersen` in the Noir +stdlib, extracted at +`stdlib/lampe/std-1.0.0-beta.14/Extracted/Hash/Mod.lean` starting at +line 251). + +Inputs are `[1, 2, ..., N]` as Fields, separator = N. Outputs are +the published Aztec curve points (for commitment) and field elements +(for hash). Negative literals are field elements expressed as their +signed representative; the `Int` → `Fp P` cast reduces them mod `p`. +-/ + +namespace Tests.Pedersen + +open Lampe (Fp Prime) +open Lampe.Crypto.EmbeddedCurve +open Lampe.Crypto.Pedersen + +/-- BN254 scalar field prime — the field for Pedersen scalars and the +base field for Grumpkin. -/ +abbrev P : Lampe.Prime := Lampe.Crypto.Bn254.prime + +/-- The test-vector input `[1, 2, ..., n]` as field elements. -/ +def inputs (n : Nat) : List.Vector (Fp P) n := + List.Vector.ofFn (fun i : Fin n => ((i.val + 1 : Nat) : Fp P)) + +-- N = 1 + +/-- pedersen_hash_with_separator<1>([1], 1) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 1) 1 = + ((-9563966249275741675388072609438711537348680428347819854678797696612266004386 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<1>([1], 1) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 1) 1 = + mkPoint + ((2393473289045184898987089634332637236754766663897650125720167164137088869378 : Int) : Fp P) + ((-7135402912423807765050323395026152633898511180575289670895350565966806597339 : Int) : Fp P) + false := by + native_decide + +-- N = 2 + +/-- pedersen_hash_with_separator<2>([1..2], 2) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 2) 2 = + ((-4514641934080458214240751313245257091597283372119704256508270041112972328364 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<2>([1..2], 2) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 2) 2 = + mkPoint + ((-1005469533000889117657666498472954572857833872027279582301287737791321798830 : Int) : Fp P) + ((-197930408253518363600434091261593976805802346006803044607495721019065268361 : Int) : Fp P) + false := by + native_decide + +-- N = 3 + +/-- pedersen_hash_with_separator<3>([1..3], 3) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 3) 3 = + ((5326303462429251635333445553787815334884504473158538697533567972354818497508 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<3>([1..3], 3) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 3) 3 = + mkPoint + ((-7445492827528947374509602945629683494533192071041804482180938699494227714940 : Int) : Fp P) + ((-346969586742294743999106690738565516862306986837138292504091779330690805808 : Int) : Fp P) + false := by + native_decide + +-- N = 4 + +/-- pedersen_hash_with_separator<4>([1..4], 4) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 4) 4 = + ((386725976317305842536127973743796063021078557104668993698335256486699462108 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<4>([1..4], 4) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 4) 4 = + mkPoint + ((3474050104565946163748262682994355436071725368663608454945085151569694677961 : Int) : Fp P) + ((4969143737471383592015577254419974288705429190161323890019554309538525237268 : Int) : Fp P) + false := by + native_decide + +-- N = 5 + +/-- pedersen_hash_with_separator<5>([1..5], 5) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 5) 5 = + ((445627510378474786942205982382342880084933256779806571759234109296077544482 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<5>([1..5], 5) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 5) 5 = + mkPoint + ((10552833461612204383225982278685649771700648236894998952452362214619168226089 : Int) : Fp P) + ((-1251131729610909206337824637802607977413231765663205492654376476649374713610 : Int) : Fp P) + false := by + native_decide + +-- N = 6 + +/-- pedersen_hash_with_separator<6>([1..6], 6) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 6) 6 = + ((10217545977856619241380062255630350521414270790482717416408002401121937565042 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<6>([1..6], 6) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 6) 6 = + mkPoint + ((11335069702571578236117888955050736139682779524214984889155721704928197387927 : Int) : Fp P) + ((-7733361908666485801415200275635877656445756448956549185022038133647049615622 : Int) : Fp P) + false := by + native_decide + +-- N = 7 + +/-- pedersen_hash_with_separator<7>([1..7], 7) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 7) 7 = + ((8389099894375185114295483291630893019224023442848409888108611454294869536227 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<7>([1..7], 7) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 7) 7 = + mkPoint + ((601182919381464537093882307577577658521785998356796832152269409048770009401 : Int) : Fp P) + ((-8704984668101593449807889537070046830501821124601109099832679891796819531525 : Int) : Fp P) + false := by + native_decide + +-- N = 8 + +/-- pedersen_hash_with_separator<8>([1..8], 8) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 8) 8 = + ((-364414833671337260860436705614307386127212237115043515297237560718972836517 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<8>([1..8], 8) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 8) 8 = + mkPoint + ((10105395258059943854471547573391327707179901153940064586773125525172385465411 : Int) : Fp P) + ((-7764172381957047914625405480055519449068901615240110013280942913930205438090 : Int) : Fp P) + false := by + native_decide + +-- N = 9 + +/-- pedersen_hash_with_separator<9>([1..9], 9) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 9) 9 = + ((5694292929090063810102755351119629986122166830204542196709417013467308391399 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<9>([1..9], 9) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 9) 9 = + mkPoint + ((4630760469979870165820917922898436050077118370325830990580986530746633543789 : Int) : Fp P) + ((445421188486227550820408419830973545028032672242093648088931561027838255858 : Int) : Fp P) + false := by + native_decide + +-- N = 10 + +/-- pedersen_hash_with_separator<10>([1..10], 10) — Aztec reference. -/ +example : + pedersenHash P defaultDomainBytes (inputs 10) 10 = + ((-1612865150156425111011383725280441289912228955196006102547487828548180279661 : Int) : Fp P) := by + native_decide + +/-- pedersen_commitment_with_separator<10>([1..10], 10) — Aztec reference. -/ +example : + pedersenCommitment P defaultDomainBytes (inputs 10) 10 = + mkPoint + ((-311556882567474412576811669014419164866085063813982345701073780395111226613 : Int) : Fp P) + ((-163948955461070038478898748306472919392980231474444415480716967232318545340 : Int) : Fp P) + false := by + native_decide + +end Tests.Pedersen diff --git a/stdlib/lampe/Stdlib.lean b/stdlib/lampe/Stdlib.lean index 40da82dd..89b642e1 100644 --- a/stdlib/lampe/Stdlib.lean +++ b/stdlib/lampe/Stdlib.lean @@ -28,6 +28,7 @@ import Stdlib.Field.Basic import Stdlib.Field.Bn254 import Stdlib.Field.Mod import Stdlib.Hash.Mod +import Stdlib.Hash.Pedersen import Stdlib.Hash.Poseidon2 import Stdlib.Integer import Stdlib.Lib diff --git a/stdlib/lampe/Stdlib/EmbeddedCurveOps.lean b/stdlib/lampe/Stdlib/EmbeddedCurveOps.lean index c7dcb9f4..7d7db229 100644 --- a/stdlib/lampe/Stdlib/EmbeddedCurveOps.lean +++ b/stdlib/lampe/Stdlib/EmbeddedCurveOps.lean @@ -6,6 +6,7 @@ import Stdlib.Hash.Mod namespace Lampe.Stdlib.EmbeddedCurveOps open «std-1.0.0-beta.14» +open Lampe.Crypto.EmbeddedCurve /-! ### Spec layering convention @@ -16,9 +17,8 @@ return shape admits a high-level semantic statement has **two specs**: - A **`private theorem foo_concrete_spec`** — faithfully restates the imperative Noir source (e.g. `r = Scalar.eq self other`, - `r = Lampe.Crypto.EmbeddedCurve.add self other`). Used as a proof - building-block when chaining bigger specs together; not part of the - public interface. + `r = Point.neg self`). Used as a proof building-block when chaining + bigger specs together; not part of the public interface. - The **public `theorem foo_spec`** — the canonical interface callers consume. Stated against semantic projections (`Scalar.valueNat`, `Point.extEq`, Mathlib's `WeierstrassCurve.Affine.Point.add` / @@ -50,19 +50,19 @@ def type := «std-1.0.0-beta.14::embedded_curve_ops::EmbeddedCurvePoint».tp h![ @[reducible] def denote (p : Prime) := Tp.denote p type -@[simp] theorem type_eq_crypto_pointTp : Point.type = Lampe.Crypto.EmbeddedCurve.pointTp := rfl +@[simp] theorem type_eq_crypto_pointTp : Point.type = pointTp := rfl def mk {p} (x y : Fp p) (isInfinite : Bool) : Point.denote p := - Lampe.Crypto.EmbeddedCurve.mkPoint x y isInfinite + mkPoint x y isInfinite -def x {p} (self : Point.denote p) : Fp p := Lampe.Crypto.EmbeddedCurve.pointX self +def x {p} (self : Point.denote p) : Fp p := pointX self -def y {p} (self : Point.denote p) : Fp p := Lampe.Crypto.EmbeddedCurve.pointY self +def y {p} (self : Point.denote p) : Fp p := pointY self def isInfinite {p} (self : Point.denote p) : Bool := - Lampe.Crypto.EmbeddedCurve.pointIsInfinite self + pointIsInfinite self -def infinity {p} : Point.denote p := Lampe.Crypto.EmbeddedCurve.pointAtInfinity +def infinity {p} : Point.denote p := pointAtInfinity def generator {p} : Point.denote p := Point.mk 1 17631683881184975370165255887551781615748388533673675138860 false @@ -114,28 +114,28 @@ def neg {p} (self : Point.denote p) : Point.denote p := group negation under the encoding. Used to bridge `point_sub_spec` to the Mathlib `P - Q` form. -/ theorem neg_encodeCurvePoint {p} - (P : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point) : - Point.neg (Lampe.Crypto.EmbeddedCurve.encodeCurvePoint P) = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (-P) := by + (P : (affineCurve p).Point) : + Point.neg (encodeCurvePoint P) = + encodeCurvePoint (-P) := by rcases P with _ | @⟨x, y, hNs⟩ - · show Point.neg (Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - (0 : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point)) = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - (-(0 : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point)) + · show Point.neg (encodeCurvePoint + (0 : (affineCurve p).Point)) = + encodeCurvePoint + (-(0 : (affineCurve p).Point)) rw [neg_zero] - simp [Point.neg, Lampe.Crypto.EmbeddedCurve.encodeCurvePoint, - Lampe.Crypto.EmbeddedCurve.pointAtInfinity, - Lampe.Crypto.EmbeddedCurve.mkPoint, + simp [Point.neg, encodeCurvePoint, + pointAtInfinity, + mkPoint, Point.x, Point.y, Point.isInfinite, Point.mk, - Lampe.Crypto.EmbeddedCurve.pointX, - Lampe.Crypto.EmbeddedCurve.pointY, - Lampe.Crypto.EmbeddedCurve.pointIsInfinite] + pointX, + pointY, + pointIsInfinite] · simp [Point.neg, Point.x, Point.y, Point.isInfinite, Point.mk, - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint, - Lampe.Crypto.EmbeddedCurve.mkPoint, - Lampe.Crypto.EmbeddedCurve.pointX, - Lampe.Crypto.EmbeddedCurve.pointY, - Lampe.Crypto.EmbeddedCurve.pointIsInfinite] + encodeCurvePoint, + mkPoint, + pointX, + pointY, + pointIsInfinite] def eq {p} (a b : Point.denote p) : Bool := (Point.isInfinite a && Point.isInfinite b) || @@ -154,33 +154,10 @@ def type := «std-1.0.0-beta.14::embedded_curve_ops::EmbeddedCurveScalar».tp h! @[reducible] def denote (p : Prime) := Tp.denote p type -@[simp] theorem type_eq_crypto_scalarTp : Scalar.type = Lampe.Crypto.EmbeddedCurve.scalarTp := rfl +@[simp] theorem type_eq_crypto_scalarTp : Scalar.type = scalarTp := rfl def mk {p} (lo hi : Fp p) : Scalar.denote p := (lo, hi, ()) -def lo {p} (self : Scalar.denote p) : Fp p := Lampe.Crypto.EmbeddedCurve.scalarLo self - -def hi {p} (self : Scalar.denote p) : Fp p := Lampe.Crypto.EmbeddedCurve.scalarHi self - -def valueNat {p} (self : Scalar.denote p) : Nat := - (Scalar.lo self).val + Lampe.Crypto.Bn254.pow128 * (Scalar.hi self).val - -/-- Bridge: stdlib `Scalar.valueNat` agrees with the crypto-side -`scalarValueNat`. The two definitions are equal modulo unfolding the -two `pow128` constants, neither of which is `@[reducible]`. -/ -theorem valueNat_eq_scalarValueNat {p} (self : Scalar.denote p) : - Scalar.valueNat self = Lampe.Crypto.EmbeddedCurve.scalarValueNat self := by - simp [Scalar.valueNat, Scalar.lo, Scalar.hi, - Lampe.Crypto.EmbeddedCurve.scalarValueNat, - Lampe.Crypto.Bn254.pow128, Lampe.Crypto.EmbeddedCurve.pow128] - -/-- The canonical-representative predicate: each limb fits in 128 bits. -This is the well-formedness condition under which `Scalar.eq` agrees -with `Scalar.valueNat` equality. -/ -def Canonical {p} (self : Scalar.denote p) : Prop := - (Scalar.lo self).val < Lampe.Crypto.Bn254.pow128 ∧ - (Scalar.hi self).val < Lampe.Crypto.Bn254.pow128 - def validOffset (offset : U 32) : Prop := offset.toNat < 33 @@ -227,7 +204,7 @@ def fromBytes? {p} (bytes : Tp.denote p ((Tp.u 8).array (64 : U 32))) @[simp] theorem valueNat_mk {p} {lo hi : Fp p} : Scalar.valueNat (Scalar.mk lo hi) = - lo.val + Lampe.Crypto.Bn254.pow128 * hi.val := by + lo.val + Lampe.pow128 * hi.val := by rfl theorem fromBytes?_eq_some_of_validOffset {p} @@ -304,12 +281,12 @@ private theorem point_neg_concrete_spec {p} {self : Point.denote p} : /-- Canonical spec for `Neg::neg` on `EmbeddedCurvePoint`: under an encoded-input hypothesis, negation agrees with Mathlib's group `-P`. -/ theorem point_neg_spec {p} {self : Point.denote p} - {P : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point} - (hself : self = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint P) : + {P : (affineCurve p).Point} + (hself : self = encodeCurvePoint P) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::ops::arith::Neg».neg h![] Point.type h![] h![] h![self]) - (fun r => r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (-P)) := by - have hEq : Point.neg self = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (-P) := by + (fun r => r = encodeCurvePoint (-P)) := by + have hEq : Point.neg self = encodeCurvePoint (-P) := by subst hself exact Point.neg_encodeCurvePoint P have h := point_neg_concrete_spec (p := p) (self := self) @@ -341,9 +318,9 @@ theorem point_eq_spec {p} {self other : Point.denote p} : obtain ⟨ox, oy, oinf, ⟨⟩⟩ := other cases sinf <;> cases oinf <;> simp [Point.eq, Point.extEq, Point.canonicalizeInfinity, Point.infinity, - Point.x, Point.y, Point.isInfinite, Lampe.Crypto.EmbeddedCurve.pointX, - Lampe.Crypto.EmbeddedCurve.pointY, Lampe.Crypto.EmbeddedCurve.pointIsInfinite, - Lampe.Crypto.EmbeddedCurve.pointAtInfinity, Lampe.Crypto.EmbeddedCurve.mkPoint, + Point.x, Point.y, Point.isInfinite, pointX, + pointY, pointIsInfinite, + pointAtInfinity, mkPoint, Bool.and_eq_true, decide_eq_true_eq] -- After simp, three residual goals remain (cases produced in order ff, ft, tf, tt): -- false.false: sx=ox ∧ sy=oy ↔ (sx,sy,false,()) = (ox,oy,false,()) @@ -372,38 +349,6 @@ private theorem scalar_eq_concrete_spec {p} {self other : Scalar.denote p} : simp [Scalar.eq, Scalar.hi, Scalar.lo, eq_comm] rfl -private lemma scalar_valueNat_inj_canonical {p} - {self other : Scalar.denote p} - (hself : Scalar.Canonical self) (hother : Scalar.Canonical other) - (h : Scalar.valueNat self = Scalar.valueNat other) : - Scalar.lo self = Scalar.lo other ∧ Scalar.hi self = Scalar.hi other := by - obtain ⟨hslo, hshi⟩ := hself - obtain ⟨holo, hohi⟩ := hother - simp [Scalar.valueNat] at h - -- h : (lo self).val + pow128 * (hi self).val = (lo other).val + pow128 * (hi other).val - -- with all four .val terms < pow128. Apply Nat-level uniqueness, then ZMod.val_injective. - have hlo : (Scalar.lo self).val = (Scalar.lo other).val ∧ - (Scalar.hi self).val = (Scalar.hi other).val := by - refine ⟨?_, ?_⟩ - · -- mod pow128 of both sides extracts lo - have : ((Scalar.lo self).val + Lampe.Crypto.Bn254.pow128 * (Scalar.hi self).val) - % Lampe.Crypto.Bn254.pow128 = - ((Scalar.lo other).val + Lampe.Crypto.Bn254.pow128 * (Scalar.hi other).val) - % Lampe.Crypto.Bn254.pow128 := by rw [h] - simp [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hslo, Nat.mod_eq_of_lt holo] at this - exact this - · -- div pow128 of both sides extracts hi - have hpos : 0 < Lampe.Crypto.Bn254.pow128 := by - simp [Lampe.Crypto.Bn254.pow128] - have hdiv : ((Scalar.lo self).val + Lampe.Crypto.Bn254.pow128 * (Scalar.hi self).val) - / Lampe.Crypto.Bn254.pow128 = - ((Scalar.lo other).val + Lampe.Crypto.Bn254.pow128 * (Scalar.hi other).val) - / Lampe.Crypto.Bn254.pow128 := by rw [h] - rw [Nat.add_mul_div_left _ _ hpos, Nat.add_mul_div_left _ _ hpos, - Nat.div_eq_of_lt hslo, Nat.div_eq_of_lt holo] at hdiv - simpa using hdiv - exact ⟨ZMod.val_injective _ hlo.1, ZMod.val_injective _ hlo.2⟩ - /-- Canonical spec for `Eq::eq` on `EmbeddedCurveScalar`: under canonical-limb hypotheses, Noir's bitwise scalar equality reflects semantic value-equality. -/ @@ -419,27 +364,28 @@ theorem scalar_eq_spec {p} {self other : Scalar.denote p} · rintro ⟨hhi, hlo⟩ simp [Scalar.valueNat, hhi, hlo] · intro h - obtain ⟨hlo, hhi⟩ := scalar_valueNat_inj_canonical hself hother h + obtain ⟨hlo, hhi⟩ := + Scalar.valueNat_inj_canonical hself hother h exact ⟨hhi, hlo⟩ theorem embedded_curve_add_builtin_spec {p} {point1 point2 : Point.denote p} (hOnCurve : - (Lampe.Crypto.EmbeddedCurve.curvePoint? point1).isSome ∧ - (Lampe.Crypto.EmbeddedCurve.curvePoint? point2).isSome) : + (curvePoint? point1).isSome ∧ + (curvePoint? point2).isSome) : STHoare p env ⟦⟧ (.callBuiltin [Point.type, Point.type, .bool] (Point.type.array 1) Builtin.embeddedCurveAdd h![point1, point2, true]) (fun r => r = - (⟨[Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? point1).get hOnCurve.1 + - (Lampe.Crypto.EmbeddedCurve.curvePoint? point2).get hOnCurve.2)], + (⟨[encodeCurvePoint + ((curvePoint? point1).get hOnCurve.1 + + (curvePoint? point2).get hOnCurve.2)], by simp⟩ : Tp.denote p (Point.type.array 1))) := by unfold Builtin.embeddedCurveAdd show STHoare p env _ - (.callBuiltin [Lampe.Crypto.EmbeddedCurve.pointTp, Lampe.Crypto.EmbeddedCurve.pointTp, .bool] - (Lampe.Crypto.EmbeddedCurve.pointTp.array 1) _ h![point1, point2, true]) _ + (.callBuiltin [pointTp, pointTp, .bool] + (pointTp.array 1) _ h![point1, point2, true]) _ apply STHoare.pureBuiltin_intro_consequence (a := ()) any_goals rfl rintro ⟨h1, h2⟩ @@ -448,15 +394,15 @@ theorem embedded_curve_add_builtin_spec {p} theorem embedded_curve_add_inner_spec {p} {point1 point2 : Point.denote p} (hOnCurve : - (Lampe.Crypto.EmbeddedCurve.curvePoint? point1).isSome ∧ - (Lampe.Crypto.EmbeddedCurve.curvePoint? point2).isSome) : + (curvePoint? point1).isSome ∧ + (curvePoint? point2).isSome) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::embedded_curve_add_inner».call h![] h![point1, point2]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? point1).get hOnCurve.1 + - (Lampe.Crypto.EmbeddedCurve.curvePoint? point2).get hOnCurve.2)) := by + r = encodeCurvePoint + ((curvePoint? point1).get hOnCurve.1 + + (curvePoint? point2).get hOnCurve.2)) := by enter_decl steps [embedded_curve_add_builtin_spec (hOnCurve := hOnCurve)] simpa @@ -464,15 +410,15 @@ theorem embedded_curve_add_inner_spec {p} theorem embedded_curve_add_spec {p} {point1 point2 : Point.denote p} (hOnCurve : - (Lampe.Crypto.EmbeddedCurve.curvePoint? point1).isSome ∧ - (Lampe.Crypto.EmbeddedCurve.curvePoint? point2).isSome) : + (curvePoint? point1).isSome ∧ + (curvePoint? point2).isSome) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::embedded_curve_add».call h![] h![point1, point2]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? point1).get hOnCurve.1 + - (Lampe.Crypto.EmbeddedCurve.curvePoint? point2).get hOnCurve.2)) := by + r = encodeCurvePoint + ((curvePoint? point1).get hOnCurve.1 + + (curvePoint? point2).get hOnCurve.2)) := by enter_decl steps all_goals try exact () @@ -482,14 +428,14 @@ theorem embedded_curve_add_spec {p} private theorem point_add_concrete_spec {p} {self other : Point.denote p} (hOnCurve : - (Lampe.Crypto.EmbeddedCurve.curvePoint? self).isSome ∧ - (Lampe.Crypto.EmbeddedCurve.curvePoint? other).isSome) : + (curvePoint? self).isSome ∧ + (curvePoint? other).isSome) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::ops::arith::Add».add h![] Point.type h![] h![] h![self, other]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve.1 + - (Lampe.Crypto.EmbeddedCurve.curvePoint? other).get hOnCurve.2)) := by + r = encodeCurvePoint + ((curvePoint? self).get hOnCurve.1 + + (curvePoint? other).get hOnCurve.2)) := by resolve_trait steps [embedded_curve_add_spec (hOnCurve := hOnCurve)] assumption @@ -498,25 +444,25 @@ private theorem point_add_concrete_spec {p} {self other : Point.denote p} encoded-input hypotheses, Noir's point addition agrees with Mathlib's affine short-Weierstrass group law on `(affineCurve p).Point`. -/ theorem point_add_spec {p} {self other : Point.denote p} - {P Q : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point} - (hself : self = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint P) - (hother : other = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint Q) : + {P Q : (affineCurve p).Point} + (hself : self = encodeCurvePoint P) + (hother : other = encodeCurvePoint Q) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::ops::arith::Add».add h![] Point.type h![] h![] h![self, other]) - (fun r => r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (P + Q)) := by + (fun r => r = encodeCurvePoint (P + Q)) := by have hOnCurve : - (Lampe.Crypto.EmbeddedCurve.curvePoint? self).isSome ∧ - (Lampe.Crypto.EmbeddedCurve.curvePoint? other).isSome := by + (curvePoint? self).isSome ∧ + (curvePoint? other).isSome := by subst hself subst hother simp have h := point_add_concrete_spec (p := p) (self := self) (other := other) (hOnCurve := hOnCurve) have hEq : - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve.1 + - (Lampe.Crypto.EmbeddedCurve.curvePoint? other).get hOnCurve.2) = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (P + Q) := by + encodeCurvePoint + ((curvePoint? self).get hOnCurve.1 + + (curvePoint? other).get hOnCurve.2) = + encodeCurvePoint (P + Q) := by subst hself subst hother congr 1 @@ -525,13 +471,13 @@ theorem point_add_spec {p} {self other : Point.denote p} exact h private theorem point_double_concrete_spec {p} {self : Point.denote p} - (hOnCurve : (Lampe.Crypto.EmbeddedCurve.curvePoint? self).isSome) : + (hOnCurve : (curvePoint? self).isSome) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::EmbeddedCurvePoint::double».call h![] h![self]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve + - (Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve)) := by + r = encodeCurvePoint + ((curvePoint? self).get hOnCurve + + (curvePoint? self).get hOnCurve)) := by enter_decl steps [embedded_curve_add_spec (hOnCurve := ⟨hOnCurve, hOnCurve⟩)] assumption @@ -539,20 +485,20 @@ private theorem point_double_concrete_spec {p} {self : Point.denote p} /-- Canonical spec for `EmbeddedCurvePoint::double`: under an encoded-input hypothesis, doubling agrees with Mathlib's `P + P`. -/ theorem point_double_spec {p} {self : Point.denote p} - {P : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point} - (hself : self = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint P) : + {P : (affineCurve p).Point} + (hself : self = encodeCurvePoint P) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::EmbeddedCurvePoint::double».call h![] h![self]) - (fun r => r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (P + P)) := by - have hOnCurve : (Lampe.Crypto.EmbeddedCurve.curvePoint? self).isSome := by + (fun r => r = encodeCurvePoint (P + P)) := by + have hOnCurve : (curvePoint? self).isSome := by subst hself simp have h := point_double_concrete_spec (p := p) (self := self) (hOnCurve := hOnCurve) have hEq : - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve + - (Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve) = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (P + P) := by + encodeCurvePoint + ((curvePoint? self).get hOnCurve + + (curvePoint? self).get hOnCurve) = + encodeCurvePoint (P + P) := by subst hself congr 1 simp @@ -561,14 +507,14 @@ theorem point_double_spec {p} {self : Point.denote p} private theorem point_sub_concrete_spec {p} {self other : Point.denote p} (hOnCurve : - (Lampe.Crypto.EmbeddedCurve.curvePoint? self).isSome ∧ - (Lampe.Crypto.EmbeddedCurve.curvePoint? (Point.neg other)).isSome) : + (curvePoint? self).isSome ∧ + (curvePoint? (Point.neg other)).isSome) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::ops::arith::Sub».sub h![] Point.type h![] h![] h![self, other]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve.1 + - (Lampe.Crypto.EmbeddedCurve.curvePoint? (Point.neg other)).get hOnCurve.2)) := by + r = encodeCurvePoint + ((curvePoint? self).get hOnCurve.1 + + (curvePoint? (Point.neg other)).get hOnCurve.2)) := by resolve_trait steps [point_neg_concrete_spec, point_add_concrete_spec (hOnCurve := hOnCurve)] simpa [Point.neg] @@ -577,15 +523,15 @@ private theorem point_sub_concrete_spec {p} {self other : Point.denote p} encoded-input hypotheses, point subtraction agrees with Mathlib's group `P - Q` (equivalently `P + (-Q)`). -/ theorem point_sub_spec {p} {self other : Point.denote p} - {P Q : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point} - (hself : self = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint P) - (hother : other = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint Q) : + {P Q : (affineCurve p).Point} + (hself : self = encodeCurvePoint P) + (hother : other = encodeCurvePoint Q) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::ops::arith::Sub».sub h![] Point.type h![] h![] h![self, other]) - (fun r => r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (P + (-Q))) := by + (fun r => r = encodeCurvePoint (P + (-Q))) := by have hOnCurve : - (Lampe.Crypto.EmbeddedCurve.curvePoint? self).isSome ∧ - (Lampe.Crypto.EmbeddedCurve.curvePoint? (Point.neg other)).isSome := by + (curvePoint? self).isSome ∧ + (curvePoint? (Point.neg other)).isSome := by subst hself subst hother refine ⟨by simp, ?_⟩ @@ -594,10 +540,10 @@ theorem point_sub_spec {p} {self other : Point.denote p} have h := point_sub_concrete_spec (p := p) (self := self) (other := other) (hOnCurve := hOnCurve) have hEq : - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - ((Lampe.Crypto.EmbeddedCurve.curvePoint? self).get hOnCurve.1 + - (Lampe.Crypto.EmbeddedCurve.curvePoint? (Point.neg other)).get hOnCurve.2) = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (P + (-Q)) := by + encodeCurvePoint + ((curvePoint? self).get hOnCurve.1 + + (curvePoint? (Point.neg other)).get hOnCurve.2) = + encodeCurvePoint (P + (-Q)) := by subst hself subst hother simp only [Point.neg_encodeCurvePoint] @@ -702,6 +648,34 @@ theorem point_hash_spec {p H stateRef} (h_x_write := h_x_write) (h_y_write := h_y_write) +/-- A limb decomposition of a field value is automatically canonical: +`scalar.val < r_scalar < 2^254` forces the high limb below `2^126`. -/ +private lemma canonical_mk_of_decomp {p} [Lampe.Crypto.Bn254.Prime p] + {scalar lo hi : Fp p} + (hlo : lo.val < Lampe.pow128) + (heq : scalar.val = lo.val + Lampe.pow128 * hi.val) : + Scalar.Canonical (Scalar.mk lo hi) := by + have hval_lt : scalar.val < p.natVal := ZMod.val_lt scalar + have hp : p.natVal = Lampe.Crypto.Bn254.r_scalar := + Lampe.Crypto.Bn254.Prime.natVal_eq_r_scalar + have hr : Lampe.Crypto.Bn254.r_scalar < 2 ^ 254 := by + unfold Lampe.Crypto.Bn254.r_scalar + decide + have hpow : Lampe.pow128 = 2 ^ 128 := rfl + have hhi : hi.val < 2 ^ 126 := by + have h1 : Lampe.pow128 * hi.val < 2 ^ 254 := by omega + rw [hpow] at h1 + have h2 : (2 : Nat) ^ 254 = 2 ^ 128 * 2 ^ 126 := by norm_num + rw [h2] at h1 + exact Nat.lt_of_mul_lt_mul_left h1 + exact ⟨hlo, hhi⟩ + +/-- Spec for `EmbeddedCurveScalar::from_field`. Besides the limb +decomposition that the body's `decompose` call enforces, the +postcondition carries `Scalar.Canonical (Scalar.mk lo hi)`: since +`scalar.val < p < 2^254`, the `Nat` equation already forces +`hi.val < 2^126`, so callers get the MSM gadget's canonicality +precondition for free. -/ theorem scalar_from_field_spec {p} [Lampe.Crypto.Bn254.Prime p] {scalar : Fp p} : STHoare p env ⟦⟧ @@ -710,14 +684,15 @@ theorem scalar_from_field_spec {p} [Lampe.Crypto.Bn254.Prime p] (fun r => ∃∃ lo hi, r = Scalar.mk lo hi ∧ - lo.val < Lampe.Crypto.Bn254.pow128 ∧ - hi.val < Lampe.Crypto.Bn254.pow128 ∧ - scalar.val = lo.val + Lampe.Crypto.Bn254.pow128 * hi.val) := by + lo.val < Lampe.pow128 ∧ + hi.val < Lampe.pow128 ∧ + scalar.val = lo.val + Lampe.pow128 * hi.val ∧ + Scalar.Canonical (Scalar.mk lo hi)) := by enter_decl steps [Lampe.Stdlib.Field.Bn254.decompose_intro (p := p)] simp [SLP.exists_pure] at * sl - all_goals aesop + all_goals aesop (add safe forward canonical_mk_of_decomp) set_option maxRecDepth 4096 in /-- Success spec for `EmbeddedCurveScalar::from_bytes`. @@ -843,28 +818,36 @@ structure). -/ private def msmAccFinRange {p : Prime} {N : U 32} (points : Tp.denote p (Point.type.array N)) (scalars : Tp.denote p (Scalar.type.array N)) - (h : ∀ i, (Lampe.Crypto.EmbeddedCurve.curvePoint? (points.get i)).isSome) : - (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point := - ∑ i, Lampe.Crypto.EmbeddedCurve.scalarValueNat (scalars.get i) • - (Lampe.Crypto.EmbeddedCurve.curvePoint? (points.get i)).get (h i) - + (h : ∀ i, (curvePoint? (points.get i)).isSome) : + (affineCurve p).Point := + ∑ i, Scalar.valueNat (scalars.get i) • + (curvePoint? (points.get i)).get (h i) + +/-- Builtin-level MSM spec — result equation only. + +The builtin's underlying precondition includes `Scalar.Canonical` +(modelling the gadget's `create_limbed_range_constraint`); we discharge +that canonicality requirement inside the proof but do not surface it +here. Callers that also need the canonicality fact (notably the +Pedersen `_spec_canonical` proofs) consume +`multi_scalar_mul_builtin_combined_spec` instead. -/ theorem multi_scalar_mul_builtin_spec {p N} {points : Tp.denote p (Point.type.array N)} {scalars : Tp.denote p (Scalar.type.array N)} - (hOnCurve : ∀ i, (Lampe.Crypto.EmbeddedCurve.curvePoint? (points.get i)).isSome) : + (hOnCurve : ∀ i, (curvePoint? (points.get i)).isSome) : STHoare p env ⟦⟧ (.callBuiltin [Point.type.array N, Scalar.type.array N, .bool] (Point.type.array 1) Builtin.multiScalarMul h![points, scalars, true]) (fun r => r = - (⟨[Lampe.Crypto.EmbeddedCurve.encodeCurvePoint + (⟨[encodeCurvePoint (msmAccFinRange points scalars hOnCurve)], by simp⟩ : Tp.denote p (Point.type.array 1))) := by unfold Builtin.multiScalarMul show STHoare p env _ - (.callBuiltin [Lampe.Crypto.EmbeddedCurve.pointTp.array N, - Lampe.Crypto.EmbeddedCurve.scalarTp.array N, .bool] - (Lampe.Crypto.EmbeddedCurve.pointTp.array 1) _ h![points, scalars, true]) _ + (.callBuiltin [pointTp.array N, + scalarTp.array N, .bool] + (pointTp.array 1) _ h![points, scalars, true]) _ apply STHoare.pureBuiltin_intro_consequence (a := N) any_goals rfl intro h @@ -873,19 +856,19 @@ theorem multi_scalar_mul_builtin_spec {p N} private theorem multi_scalar_mul_concrete_spec {p N} {points : Tp.denote p (Point.type.array N)} {scalars : Tp.denote p (Scalar.type.array N)} - (hOnCurve : ∀ i, (Lampe.Crypto.EmbeddedCurve.curvePoint? (points.get i)).isSome) : + (hOnCurve : ∀ i, (curvePoint? (points.get i)).isSome) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::multi_scalar_mul».call h![N] h![points, scalars]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint + r = encodeCurvePoint (msmAccFinRange points scalars hOnCurve)) := by enter_decl steps apply STHoare.letIn_intro (Q := fun r : Tp.denote p (Point.type.array 1) => ⟦r = - (⟨[Lampe.Crypto.EmbeddedCurve.encodeCurvePoint + (⟨[encodeCurvePoint (msmAccFinRange points scalars hOnCurve)], by simp⟩ : Tp.denote p (Point.type.array 1))⟧) · exact multi_scalar_mul_builtin_spec (p := p) (N := N) @@ -895,14 +878,44 @@ private theorem multi_scalar_mul_concrete_spec {p N} subst_vars rfl +/-- Combined builtin spec: result equation **and** canonicality +(the gadget's `create_limbed_range_constraint` postcondition, +`LO_BITS = 128`, `HI_BITS = 126`, composable with the downstream +uniqueness machinery `Scalar.canonicalDecomp_unique`). This is +the spec callers use when they need both facts without going through +two separate spec applications. The proof is direct because the +builtin's precondition gives us both `onCurve` and canonicality. -/ +theorem multi_scalar_mul_builtin_combined_spec {p N} + {points : Tp.denote p (Point.type.array N)} + {scalars : Tp.denote p (Scalar.type.array N)} + (hOnCurve : ∀ i, (curvePoint? (points.get i)).isSome) : + STHoare p env ⟦⟧ + (.callBuiltin [Point.type.array N, Scalar.type.array N, .bool] (Point.type.array 1) + Builtin.multiScalarMul h![points, scalars, true]) + (fun r => + (∀ i, Scalar.Canonical (scalars.get i)) ∧ + r = + (⟨[encodeCurvePoint + (msmAccFinRange points scalars hOnCurve)], + by simp⟩ : Tp.denote p (Point.type.array 1))) := by + unfold Builtin.multiScalarMul + show STHoare p env _ + (.callBuiltin [pointTp.array N, + scalarTp.array N, .bool] + (pointTp.array 1) _ h![points, scalars, true]) _ + apply STHoare.pureBuiltin_intro_consequence (a := N) + any_goals rfl + rintro ⟨_, hCan⟩ + exact ⟨hCan, rfl⟩ + /-- Helper: if `points.toList = Ps.toList.map encodeCurvePoint`, then `points.get i = encodeCurvePoint (Ps.get i)` for every `i`. -/ private lemma points_get_eq_encode {p : Prime} {N : U 32} {points : Tp.denote p (Point.type.array N)} - {Ps : List.Vector (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point N.toNat} - (h_enc : points.toList = Ps.toList.map Lampe.Crypto.EmbeddedCurve.encodeCurvePoint) + {Ps : List.Vector (affineCurve p).Point N.toNat} + (h_enc : points.toList = Ps.toList.map encodeCurvePoint) (i : Fin N.toNat) : - points.get i = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint (Ps.get i) := by + points.get i = encodeCurvePoint (Ps.get i) := by have hi_pts : i.val < points.toList.length := by rw [List.Vector.toList_length]; exact i.isLt have hi_Ps : i.val < Ps.toList.length := by @@ -925,35 +938,35 @@ the MSM accumulator equals the canonical sum private lemma msmAccFinRange_eq_sum {p : Prime} {N : U 32} {points : Tp.denote p (Point.type.array N)} {scalars : Tp.denote p (Scalar.type.array N)} - {Ps : List.Vector (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point N.toNat} - (h_enc : points.toList = Ps.toList.map Lampe.Crypto.EmbeddedCurve.encodeCurvePoint) - (hOnCurve : ∀ i, (Lampe.Crypto.EmbeddedCurve.curvePoint? (points.get i)).isSome) : + {Ps : List.Vector (affineCurve p).Point N.toNat} + (h_enc : points.toList = Ps.toList.map encodeCurvePoint) + (hOnCurve : ∀ i, (curvePoint? (points.get i)).isSome) : msmAccFinRange points scalars hOnCurve = ∑ i, Scalar.valueNat (scalars.get i) • Ps.get i := by unfold msmAccFinRange refine Finset.sum_congr rfl (fun i _ => ?_) have hSome : - Lampe.Crypto.EmbeddedCurve.curvePoint? (points.get i) = some (Ps.get i) := by + curvePoint? (points.get i) = some (Ps.get i) := by rw [points_get_eq_encode h_enc i]; simp - rw [Option.get_of_eq_some _ hSome, ← Scalar.valueNat_eq_scalarValueNat] + rw [Option.get_of_eq_some _ hSome] -/-- Canonical spec for `multi_scalar_mul`: when each input point is -the encoding of a Mathlib `WeierstrassCurve.Affine.Point`, the MSM -result is the encoding of `∑ᵢ Scalar.valueNat (scalars i) • Ps i`. -/ +/-- Result-equation spec for `multi_scalar_mul`. When each input point is +the encoding of a Mathlib `WeierstrassCurve.Affine.Point`, the result is +`encodeCurvePoint (∑ Scalar.valueNat (scalars i) • Ps i)`. -/ theorem multi_scalar_mul_spec {p N} {points : Tp.denote p (Point.type.array N)} {scalars : Tp.denote p (Scalar.type.array N)} - {Ps : List.Vector (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point N.toNat} + {Ps : List.Vector (affineCurve p).Point N.toNat} (h_enc : - points.toList = Ps.toList.map Lampe.Crypto.EmbeddedCurve.encodeCurvePoint) : + points.toList = Ps.toList.map encodeCurvePoint) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::multi_scalar_mul».call h![N] h![points, scalars]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint + r = encodeCurvePoint (∑ i, Scalar.valueNat (scalars.get i) • Ps.get i)) := by have hOnCurve : - ∀ i, (Lampe.Crypto.EmbeddedCurve.curvePoint? (points.get i)).isSome := by + ∀ i, (curvePoint? (points.get i)).isSome := by intro i rw [points_get_eq_encode h_enc i] simp @@ -962,17 +975,70 @@ theorem multi_scalar_mul_spec {p N} rw [msmAccFinRange_eq_sum h_enc hOnCurve] at h exact h +/-- Combined wrapper spec: result equation and canonicality together. +Used by Pedersen `_spec_canonical` proofs to extract both facts in a +single `steps` invocation. -/ +theorem multi_scalar_mul_combined_spec {p N} + {points : Tp.denote p (Point.type.array N)} + {scalars : Tp.denote p (Scalar.type.array N)} + {Ps : List.Vector (affineCurve p).Point N.toNat} + (h_enc : + points.toList = Ps.toList.map encodeCurvePoint) : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::embedded_curve_ops::multi_scalar_mul».call + h![N] h![points, scalars]) + (fun r => + (∀ i, Scalar.Canonical (scalars.get i)) ∧ + r = encodeCurvePoint + (∑ i, Scalar.valueNat (scalars.get i) • Ps.get i)) := by + have hOnCurve : + ∀ i, (curvePoint? (points.get i)).isSome := by + intro i + rw [points_get_eq_encode h_enc i] + simp + -- Compose result-eq spec and canon spec at the wrapper level by + -- proving inline: re-run the body of multi_scalar_mul (which is + -- multi_scalar_mul_array_return(...)[0]) using the combined builtin + -- spec for the body's builtin call. + enter_decl + steps + apply STHoare.letIn_intro + (Q := fun r : Tp.denote p (Point.type.array 1) => + ⟦(∀ i, Scalar.Canonical (scalars.get i)) ∧ + r = + (⟨[encodeCurvePoint + (msmAccFinRange points scalars hOnCurve)], + by simp⟩ : Tp.denote p (Point.type.array 1))⟧) + · exact multi_scalar_mul_builtin_combined_spec (p := p) (N := N) + (points := points) (scalars := scalars) (hOnCurve := hOnCurve) + · intro r + steps + -- After steps, the conjunction `(canon ∧ r = ⟨[...], _⟩)` is in + -- scope. Extract and rebuild the goal's conjunction with the + -- bridged sum form. + have hPair : + (∀ i, Scalar.Canonical (scalars.get i)) ∧ + r = (⟨[encodeCurvePoint + (msmAccFinRange points scalars hOnCurve)], + by simp⟩ : Tp.denote p (Point.type.array 1)) := by assumption + obtain ⟨hCan, hr⟩ := hPair + refine ⟨hCan, ?_⟩ + subst hr + subst_vars + rw [msmAccFinRange_eq_sum h_enc hOnCurve] + rfl + private theorem fixed_base_scalar_mul_concrete_spec {p} {scalar : Scalar.denote p} - {Pgen : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point} + {Pgen : (affineCurve p).Point} (h_gen : (Point.generator : Point.denote p) = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint Pgen) : + encodeCurvePoint Pgen) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::fixed_base_scalar_mul».call h![] h![scalar]) (fun r => - r = Lampe.Crypto.EmbeddedCurve.encodeCurvePoint - (Lampe.Crypto.EmbeddedCurve.scalarValueNat scalar • Pgen)) := by + r = encodeCurvePoint + (Scalar.valueNat scalar • Pgen)) := by enter_decl -- The MSM here is over the singleton arrays `[generator]` and `[scalar]`. We prove -- the on-curve hypothesis specialised to that singleton (knowing the only entry is @@ -983,7 +1049,7 @@ private theorem fixed_base_scalar_mul_concrete_spec {p} ⟨[scalar], by simp⟩ with hscalarsVec have hOnCurve : ∀ i, - (Lampe.Crypto.EmbeddedCurve.curvePoint? + (curvePoint? (List.Vector.get pointsVec i)).isSome := by intro i have hgi : List.Vector.get pointsVec i = Point.generator := by @@ -992,8 +1058,8 @@ private theorem fixed_base_scalar_mul_concrete_spec {p} interval_cases k rfl have hcp : - Lampe.Crypto.EmbeddedCurve.curvePoint? (List.Vector.get pointsVec i) = - Lampe.Crypto.EmbeddedCurve.curvePoint? Point.generator := + curvePoint? (List.Vector.get pointsVec i) = + curvePoint? Point.generator := congrArg _ hgi rw [hcp, h_gen] simp @@ -1002,22 +1068,18 @@ private theorem fixed_base_scalar_mul_concrete_spec {p} (points := pointsVec) (scalars := scalarsVec) (hOnCurve := hOnCurve)] - -- The hypothesis a✝ states v = encodeCurvePoint (msmAccFinRange pointsVec scalarsVec hOnCurve). - -- Reduce via the bridge lemma + `Fin.sum_univ_one` for the singleton. have hmsm : msmAccFinRange pointsVec scalarsVec hOnCurve = - Lampe.Crypto.EmbeddedCurve.scalarValueNat scalar • Pgen := by - let Ps : List.Vector (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point ((1 : U 32).toNat) := + Scalar.valueNat scalar • Pgen := by + let Ps : List.Vector (affineCurve p).Point ((1 : U 32).toNat) := ⟨[Pgen], rfl⟩ - have h_enc : pointsVec.toList = Ps.toList.map Lampe.Crypto.EmbeddedCurve.encodeCurvePoint := by - show [Point.generator] = [Lampe.Crypto.EmbeddedCurve.encodeCurvePoint Pgen] + have h_enc : pointsVec.toList = Ps.toList.map encodeCurvePoint := by + show [Point.generator] = [encodeCurvePoint Pgen] rw [h_gen]; rfl rw [msmAccFinRange_eq_sum (Ps := Ps) h_enc hOnCurve] show (∑ i : Fin 1, Scalar.valueNat (scalarsVec.get i) • Ps.get i) = _ rw [Fin.sum_univ_one] - show Scalar.valueNat scalar • Pgen = - Lampe.Crypto.EmbeddedCurve.scalarValueNat scalar • Pgen - rw [Scalar.valueNat_eq_scalarValueNat] + rfl rename_i hRet rw [hmsm] at hRet exact hRet @@ -1030,20 +1092,19 @@ generator `Point.generator` is the encoding of some Mathlib The hypothesis `h_gen` is a side condition because proving `(affineCurve p).Nonsingular 1 ` for an arbitrary `p` requires knowing the concrete characteristic; downstream callers -that pin `p` to BN254 discharge it directly. -/ +that pin `p` to BN254 discharge it directly (see +`Lampe.Stdlib.EmbeddedCurveOps.Bn254.fixed_base_scalar_mul_bn254_spec`). -/ theorem fixed_base_scalar_mul_spec {p} {scalar : Scalar.denote p} - {Pgen : (Lampe.Crypto.EmbeddedCurve.affineCurve p).Point} + {Pgen : (affineCurve p).Point} (h_gen : (Point.generator : Point.denote p) = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint Pgen) : + encodeCurvePoint Pgen) : STHoare p env ⟦⟧ («std-1.0.0-beta.14::embedded_curve_ops::fixed_base_scalar_mul».call h![] h![scalar]) (fun r => r = - Lampe.Crypto.EmbeddedCurve.encodeCurvePoint + encodeCurvePoint (Scalar.valueNat scalar • Pgen)) := by - have h := fixed_base_scalar_mul_concrete_spec (p := p) (scalar := scalar) + exact fixed_base_scalar_mul_concrete_spec (p := p) (scalar := scalar) (Pgen := Pgen) (h_gen := h_gen) - rw [Scalar.valueNat_eq_scalarValueNat] - exact h diff --git a/stdlib/lampe/Stdlib/EmbeddedCurveOps/Bn254.lean b/stdlib/lampe/Stdlib/EmbeddedCurveOps/Bn254.lean index 04d798b4..6e21b242 100644 --- a/stdlib/lampe/Stdlib/EmbeddedCurveOps/Bn254.lean +++ b/stdlib/lampe/Stdlib/EmbeddedCurveOps/Bn254.lean @@ -45,7 +45,7 @@ theorem fixed_base_scalar_mul_bn254_spec («std-1.0.0-beta.14::embedded_curve_ops::fixed_base_scalar_mul».call h![] h![scalar]) (fun r => r = encodeCurvePoint - (Lampe.Stdlib.EmbeddedCurveOps.Scalar.valueNat scalar • generatorPoint)) := + (Scalar.valueNat scalar • generatorPoint)) := Lampe.Stdlib.EmbeddedCurveOps.fixed_base_scalar_mul_spec (Pgen := generatorPoint) generator_eq_encodeCurvePoint diff --git a/stdlib/lampe/Stdlib/Field/Bn254.lean b/stdlib/lampe/Stdlib/Field/Bn254.lean index ad077b54..08aa0a67 100644 --- a/stdlib/lampe/Stdlib/Field/Bn254.lean +++ b/stdlib/lampe/Stdlib/Field/Bn254.lean @@ -20,7 +20,8 @@ namespace Lampe.Stdlib.Field.Bn254 open Lampe open Lampe.Crypto open «std-1.0.0-beta.14» (env) -open Lampe.Crypto.Bn254 (plo phi pow128 pow128_lt_prime pow128_val +open Lampe (pow128) +open Lampe.Crypto.Bn254 (plo phi pow128_lt_prime pow128_val val_add_one_of_lt limbs_gt_of_hi_gt sub_val_gt_pow128_of_lt) abbrev PLO := «std-1.0.0-beta.14::field::bn254::PLO» diff --git a/stdlib/lampe/Stdlib/Hash/Pedersen.lean b/stdlib/lampe/Stdlib/Hash/Pedersen.lean new file mode 100644 index 00000000..533be661 --- /dev/null +++ b/stdlib/lampe/Stdlib/Hash/Pedersen.lean @@ -0,0 +1,760 @@ +import «std-1.0.0-beta.14».Extracted +import Lampe +import Stdlib.EmbeddedCurveOps +import Stdlib.Field.Bn254 +import Stdlib.Hash.Mod + +namespace Lampe.Stdlib.Hash.Pedersen + +open «std-1.0.0-beta.14» +open Lampe.Builtin (bytesToList) +open Lampe.Crypto.EmbeddedCurve +open Lampe.Crypto.Pedersen +open Lampe.Stdlib.EmbeddedCurveOps + +/-- Alias for the BN254 high limb (`PHI` field constant) as a `Nat`. +Not `private`: it appears in the public `from_field_unsafe_spec` statement. -/ +abbrev phi : Nat := Lampe.Crypto.Bn254.phi + +/-- Alias for the BN254 low limb (`PLO` field constant) as a `Nat`. +Not `private`: it appears in the public `from_field_unsafe_spec` statement. -/ +abbrev plo : Nat := Lampe.Crypto.Bn254.plo + +/-- Alias for `2^128` as a `Nat`. +Not `private`: it appears in the public `from_field_unsafe_spec` statement. -/ +abbrev pow128 : Nat := Lampe.pow128 + +/-! +# Stdlib specs for `std::hash` Pedersen wrappers + +This module proves STHoare triples for all 5 Noir stdlib functions +that sit on top of the `derive_pedersen_generators` foreign builtin: + +- `derive_generators_spec` — pass-through wrapper around the builtin +- `from_field_unsafe_spec` — ∃-limbs decomposition `scalar = xlo + 2^128 * xhi` +- `pedersen_commitment_with_separator_spec_canonical` — substantive MSM spec +- `pedersen_hash_with_separator_spec_canonical` — substantive + MSM-then-`pointX` spec +- `pedersen_commitment_spec_canonical`, `pedersen_hash_spec_canonical` — + wrappers at `separator = 0` + +The public `_spec_canonical` theorems express the result as the pure +closed forms `pedersenCommitment` / +`pedersenHash` (BLAKE3 hash-to-curve + Tonelli-Shanks generators, with +each input collapsed to its canonical limb decomposition). They are +derived from private existential `_spec` intermediates that expose the +per-slot `from_field_unsafe` output as an existential `Ss` witness +satisfying `FromFieldUnsafeWitness` (limb relation, canonical-range +disjunction, and limb-range canonicality). +-/ + +/-! ### `derive_pedersen_generators` builtin spec -/ + +private theorem derivePedersenGenerators_builtin_spec {p} + {N M : U 32} + {domainBytes : Tp.denote p ((Tp.u 8).array M)} + {startIdx : U 32} : + STHoare p env ⟦⟧ + (.callBuiltin [(Tp.u 8).array M, Tp.u 32] (pointTp.array N) + Builtin.derivePedersenGenerators h![domainBytes, startIdx]) + (fun r => + r = derivePedersenGenerators p + (bytesToList (M := M) domainBytes) + startIdx.toNat + N.toNat) := by + exact STHoare.genericTotalPureBuiltin_intro Builtin.derivePedersenGenerators rfl + (N, M) p env h![domainBytes, startIdx] + +/-! ### `derive_generators` wrapper spec -/ + +theorem derive_generators_spec {p} {N M : U 32} + {domainBytes : Tp.denote p ((Tp.u 8).array M)} + {startIdx : U 32} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::derive_generators».call h![N, M] + h![domainBytes, startIdx]) + (fun r => + r = derivePedersenGenerators p + (bytesToList (M := M) domainBytes) + startIdx.toNat + N.toNat) := by + enter_decl + steps [derivePedersenGenerators_builtin_spec (p := p) (N := N) (M := M) + (domainBytes := domainBytes) (startIdx := startIdx)] + assumption + +/-! ### Bridging lemmas -/ + +private lemma strAsBytes_default_domain_eq {p} : + bytesToList (p := p) (M := (24 : U 32)) + (Lampe.NoirStr.of "DEFAULT_DOMAIN_SEPARATOR") = defaultDomainBytes := by + rfl + +private lemma strAsBytes_hash_length_eq {p} : + bytesToList (p := p) (M := (20 : U 32)) + (Lampe.NoirStr.of "pedersen_hash_length") = pedersenHashLengthBytes := by + rfl + +/-! ### `from_field_unsafe` wrapper spec -/ + +/-- Spec for `std::hash::from_field_unsafe`. The body decomposes +`scalar` into two field limbs `xlo, xhi` via the `decompose_hint` +oracle and then enforces + +``` +scalar = xlo + 2^128 * xhi -- limb decomposition +(xhi, xlo) <ₗₑₓ (PHI, PLO) -- canonical-range +``` + +where `PLO + 2^128 * PHI = p` is the BN254 scalar-field prime +limb decomposition. The output `EmbeddedCurveScalar` is +`Scalar.mk xlo xhi`. + +Unlike `decompose`, `from_field_unsafe` does **not** call +`assert_max_bit_size<128>` on the limbs, so the per-limb bounds +`xlo.val, xhi.val < 2^128` are *not* part of the postcondition; +the constraint enforced is the canonical-range disjunction +below. -/ +theorem from_field_unsafe_spec {p} [Lampe.Crypto.Bn254.Prime p] + {scalar : Fp p} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::from_field_unsafe».call h![] h![scalar]) + (fun r => + ∃∃ xlo xhi, + r = Scalar.mk xlo xhi ∧ + scalar = xlo + (pow128 : Fp p) * xhi ∧ + ((xhi = (phi : Fp p) ∧ xlo.val < plo) ∨ xhi.val < phi)) := by + enter_decl + apply STHoare.letIn_intro + (Q := fun (_ : Tp.denote p (Tp.tuple none [Tp.field, Tp.field])) => ⟦⟧) + · steps [Lampe.Stdlib.Field.Bn254.decompose_hint_intro (p := p)] + intro xlo_xhi + steps [Lampe.Stdlib.Field.Bn254.two_pow_128_spec (p := p), + Lampe.Stdlib.Field.Bn254.phi_spec (p := p), + Lampe.Stdlib.Field.Bn254.plo_spec (p := p), + Lampe.Stdlib.Field.Bn254.assert_lt_intro (p := p)] + rename_i hxlo hxhi _ hassert + -- Bind the ite result and case-split on the condition. + apply STHoare.letIn_intro + (Q := fun (v : Tp.denote p (Tp.tuple none [Tp.field, Tp.field])) => + ⟦v = (if decide (xhi = (phi : Fp p)) then (xlo, (plo : Fp p), ()) + else (xhi, (phi : Fp p), ()))⟧) + · -- Prove the ite produces the expected tuple. + apply STHoare.ite_intro + · intro h_eq + steps [Lampe.Stdlib.Field.Bn254.plo_spec (p := p)] + subst_vars + simp_all + · intro h_ne + steps [Lampe.Stdlib.Field.Bn254.phi_spec (p := p)] + subst_vars + simp_all + -- Bridge lemma: `(plo : Fp p).val = plo` under `[Bn254.Prime p]`. Used by the xhi=phi branch via aesop. + have hplo_val : ((plo : Nat) : Fp p).val = plo := by + have hplo_lt : (plo : Nat) < p.natVal := by + have : (plo : Nat) < Lampe.pow128 := by decide + linarith [this, Lampe.Crypto.Bn254.pow128_lt_prime (p := p)] + simpa using (ZMod.val_natCast_of_lt hplo_lt) + have hphi_val : ((phi : Nat) : Fp p).val = phi := by + have hphi_lt : (phi : Nat) < p.natVal := by + have : (phi : Nat) < Lampe.pow128 := by decide + linarith [this, Lampe.Crypto.Bn254.pow128_lt_prime (p := p)] + simpa using (ZMod.val_natCast_of_lt hphi_lt) + intro v + -- Discharge the ⟦ v = ... ⟧ pure precondition and split on the bool. + by_cases h_xhi : xhi = (phi : Fp p) + · -- Branch: xhi = phi, so v = (xlo, plo, ()). After assert_lt(xlo, plo) we get xlo.val < plo. + have h_xhi_eq : decide (xhi = (phi : Fp p)) = true := by simp [h_xhi] + simp only [h_xhi_eq, if_true] at * + steps [Lampe.Stdlib.Field.Bn254.assert_lt_intro (p := p)] + simp [SLP.exists_pure] at * + sl + aesop + · -- Branch: xhi ≠ phi, so v = (xhi, phi, ()). After assert_lt(xhi, phi) we get xhi.val < phi. + have h_xhi_eq : decide (xhi = (phi : Fp p)) = false := by simp [h_xhi] + rw [h_xhi_eq] at * + simp only [Bool.false_eq_true, if_false] at * + steps [Lampe.Stdlib.Field.Bn254.assert_lt_intro (p := p)] + rename_i _ hv_eq ha_eq hb_eq hab vret hret + have ha_xhi : a = xhi := by rw [ha_eq, hv_eq]; rfl + have hb_phi : b = ((phi : Nat) : Fp p) := by rw [hb_eq, hv_eq]; rfl + have h_xhi_val_lt : xhi.val < phi := by + have := hab + rw [ha_xhi, hb_phi] at this + simpa [hphi_val] using this + have hassert_eq : scalar = xlo + ((Lampe.pow128 : Nat) : Fp p) * xhi := by + simpa [decide_eq_true_eq] using hassert + have hret_mk : vret = Scalar.mk xlo xhi := by + simpa [Scalar.mk, HList.toTuple] using hret + simp only [SLP.exists_pure] + sl + refine ⟨xhi, hret_mk, ?_, Or.inr h_xhi_val_lt⟩ + show scalar = xlo + ((Lampe.pow128 : Nat) : Fp p) * xhi + exact hassert_eq + +/-! ### `pedersen_commitment_with_separator` substantive spec -/ + +/-- Relation enforced by the body of `from_field_unsafe` on its output +scalar `s` for input `x`: the limb relation `x = lo + 2^128 * hi` and +the canonical-range disjunction enforced by the `assert_lt`. Used as +the per-slot loop invariant of the scalar-buffer loops below. -/ +private def fromFieldUnsafeRel {p} [Lampe.Crypto.Bn254.Prime p] + (x : Fp p) (s : Scalar.denote p) : Prop := + x = s.1 + ((pow128 : Nat) : Fp p) * s.2.1 + ∧ ((s.2.1 = ((phi : Nat) : Fp p) ∧ s.1.val < plo) + ∨ s.2.1.val < phi) + +/-- Everything the Pedersen wrappers learn about one `from_field_unsafe` +output scalar `s` for input `x`: `fromFieldUnsafeRel` plus the MSM +gadget's limb-range canonicality. This is the per-slot witness carried +by the existential `_spec` intermediates and consumed (via +`Scalar.canonicalDecomp_unique`) by the `_spec_canonical` proofs. -/ +private def FromFieldUnsafeWitness {p} [Lampe.Crypto.Bn254.Prime p] + (x : Fp p) (s : Scalar.denote p) : Prop := + fromFieldUnsafeRel x s ∧ Scalar.Canonical s + +/-- Existential intermediate for +`std::hash::pedersen_commitment_with_separator`, consumed only by the +public `_spec_canonical` theorem below. The witness `Ss` records the +per-slot `from_field_unsafe` outputs, each satisfying +`FromFieldUnsafeWitness`. -/ +private theorem pedersen_commitment_with_separator_spec {p N} + [Lampe.Crypto.Bn254.Prime p] + {input : Tp.denote p (Tp.field.array N)} + {separator : U 32} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::pedersen_commitment_with_separator».call h![N] + h![input, separator]) + (fun r => + ∃∃ Ss : List.Vector (Scalar.denote p) N.toNat, + r = encodeCurvePoint + (∑ i, Scalar.valueNat (Ss.get i) + • pedersenGenerator (p := p) + defaultDomainBytes + (separator.toNat + i.val)) + ∧ ∀ i, FromFieldUnsafeWitness (input.get i) (Ss.get i)) := by + let Ps : List.Vector (affineCurve p).Point N.toNat := + List.Vector.ofFn (fun i => pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val)) + have h_gen : ∀ i, + encodeCurvePoint (Ps.get i) = + pedersenGeneratorPoint p defaultDomainBytes + (separator.toNat + i.val) := by + intro i + simp [Ps, List.Vector.get_ofFn, pedersenGeneratorPoint_eq] + enter_decl + steps + loop_inv nat fun (i : Nat) _ _ => + ∃∃ v : Tp.denote p (Scalar.type.array N), + [points ↦ ⟨Scalar.type.array N, v⟩] ⋆ + ⟦∀ (j : Nat) (hj : j < i) (hjN : j < N.toNat), + fromFieldUnsafeRel (input.get ⟨j, hjN⟩) (v.get ⟨j, hjN⟩)⟧ + · sl + intro j hj _ + simp at hj + · simp + · intro i hlo hhi + steps [from_field_unsafe_spec (p := p)] + simp_all only [BitVec.toNat_intCast, Int.reducePow, EuclideanDomain.zero_mod, Int.toNat_zero, + zero_le, Builtin.CastTp.cast, + BitVec.truncate_eq_setWidth, BitVec.setWidth_eq, BitVec.toNat_ofNatLT, + Lens.modify, Access.modify, Lens.get, Option.bind_eq_bind, Option.bind_some, + dite_true, Option.get_some] + rename_i v_prev hPrefix hCastLt xlo xhi _hModSome _ hRes + obtain ⟨_h_mk, h_scalar, h_range⟩ := hRes + intro j hj hjN + by_cases h_eq : j = i + · subst h_eq + unfold fromFieldUnsafeRel + have hSetGet : + (List.Vector.set v_prev ⟨j, hCastLt⟩ (Scalar.mk xlo xhi)).get ⟨j, hjN⟩ = + Scalar.mk xlo xhi := by + rw [List.Vector.get_set_same] + rw [hSetGet] + simp only [Scalar.mk] + refine ⟨h_scalar, h_range⟩ + · have hjlt : j < i := by omega + have hne : (⟨i, hCastLt⟩ : Fin N.toNat) ≠ ⟨j, hjN⟩ := by + intro hh + have : i = j := by exact (Fin.mk.injEq _ _ _ _).mp hh + exact h_eq this.symm + have hSetGet : + (List.Vector.set v_prev ⟨i, hCastLt⟩ (Scalar.mk xlo xhi)).get ⟨j, hjN⟩ = + v_prev.get ⟨j, hjN⟩ := + List.Vector.get_set_of_ne (v := v_prev) hne (Scalar.mk xlo xhi) + unfold fromFieldUnsafeRel + rw [hSetGet] + exact hPrefix j hjlt hjN + steps [derive_generators_spec (p := p) (N := N) (M := (24 : U 32)) + (startIdx := separator)] + rename_i _hLo vFinal hInv _strLen hGen + -- Bridge: bytesToList (strAsBytes "DEFAULT_DOMAIN_SEPARATOR") = defaultDomainBytes. + have hDomain : + bytesToList (p := p) (M := (24 : U 32)) + (Lampe.NoirStr.of "DEFAULT_DOMAIN_SEPARATOR").bytes = defaultDomainBytes := + strAsBytes_default_domain_eq (p := p) + rw [hDomain] at hGen + have h_enc : + generators.toList = Ps.toList.map encodeCurvePoint := by + rw [hGen] + exact derivePedersenGenerators_h_enc (p := p) (n := N.toNat) + (domain := defaultDomainBytes) (start := separator.toNat) (Ps := Ps) h_gen + steps [multi_scalar_mul_combined_spec (p := p) (N := N) + (points := generators) (scalars := vFinal) (Ps := Ps) h_enc] + case v => exact vFinal + rename_i hMsm + obtain ⟨hCanon, hSum⟩ := hMsm + refine ⟨?_, ?_⟩ + · + have hPs_get : ∀ i : Fin N.toNat, + Ps.get i = pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val) := by + intro i + simp [Ps, List.Vector.get_ofFn] + simp only [hPs_get] at hSum + exact hSum + · + intro i + exact ⟨hInv i.val i.isLt i.isLt, hCanon i⟩ + +/-- Deterministic closed-form of `pedersen_commitment_with_separator_spec`: +the result is the pure `pedersenCommitment` (the +MSM with each input collapsed to its canonical limb decomposition). -/ +theorem pedersen_commitment_with_separator_spec_canonical {p N} + [Lampe.Crypto.Bn254.Prime p] + {input : Tp.denote p (Tp.field.array N)} + {separator : U 32} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::pedersen_commitment_with_separator».call h![N] + h![input, separator]) + (fun r => + r = pedersenCommitment p defaultDomainBytes input separator.toNat) := by + apply STHoare.consequence (h_pre_conseq := SLP.entails_self) ?_ + (pedersen_commitment_with_separator_spec (p := p) (N := N) + (input := input) (separator := separator)) + intro r + rw [← SLP.star_exists] + apply SLP.exists_intro_l + intro Ss + apply SLP.pure_left + rintro ⟨h_eq, h_wit⟩ + have h_unique : ∀ i, Ss.get i = Scalar.canonicalDecomp (input.get i) := fun i => + Scalar.canonicalDecomp_unique (h_wit i).2 (h_wit i).1.2 (h_wit i).1.1 + have hSumEq : + (∑ i : Fin N.toNat, + Scalar.valueNat (Ss.get i) + • pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val)) = + ∑ i : Fin N.toNat, + Scalar.valueNat + (Scalar.canonicalDecomp (input.get i)) + • pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val) := + Finset.sum_congr rfl (fun i _ => by rw [h_unique i]) + apply SLP.pure_right + · rw [pedersenCommitment_eq, h_eq, hSumEq] + · exact SLP.entails_top + +/-! ### `pedersen_hash_with_separator` spec -/ + +set_option maxHeartbeats 300000 in +/-- Existential intermediate for `std::hash::pedersen_hash_with_separator`, +consumed only by the public `_spec_canonical` theorem below. The body adds +a length-slot scalar `(N, 0)` at position `N`, derives the corresponding +generator from `"pedersen_hash_length"` (with `starting_index = 0`), +and returns the x-coordinate of the singleton MSM result. The witness +`Ss` records the per-slot `from_field_unsafe` outputs, each satisfying +`FromFieldUnsafeWitness`. -/ +private theorem pedersen_hash_with_separator_spec {p N} + [Lampe.Crypto.Bn254.Prime p] + {input : Tp.denote p (Tp.field.array N)} + {separator : U 32} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::pedersen_hash_with_separator».call h![N] + h![input, separator]) + (fun r => + ∃∃ Ss : List.Vector (Scalar.denote p) N.toNat, + r = pointX + (encodeCurvePoint + ((∑ i : Fin N.toNat, + Scalar.valueNat (Ss.get i) + • pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val)) + + (N.toNat : ℕ) • pedersenGenerator (p := p) + pedersenHashLengthBytes 0)) + ∧ ∀ i, FromFieldUnsafeWitness (input.get i) (Ss.get i)) := by + let Ps : List.Vector (affineCurve p).Point (N.toNat + 1) := + List.Vector.ofFn (fun i : Fin (N.toNat + 1) => + if h : i.val < N.toNat then + pedersenGenerator (p := p) defaultDomainBytes + (separator.toNat + i.val) + else + pedersenGenerator (p := p) pedersenHashLengthBytes 0) + have h_gen : ∀ (i : Fin N.toNat), + encodeCurvePoint + (Ps.get ⟨i.val, Nat.lt_succ_of_lt i.isLt⟩) = + pedersenGeneratorPoint p defaultDomainBytes + (separator.toNat + i.val) := by + intro i + simp [Ps, List.Vector.get_ofFn, i.isLt, + pedersenGeneratorPoint_eq] + have h_len_gen : + encodeCurvePoint + (Ps.get ⟨N.toNat, Nat.lt_succ_self _⟩) = + pedersenGeneratorPoint p pedersenHashLengthBytes 0 := by + simp [Ps, List.Vector.get_ofFn, + pedersenGeneratorPoint_eq] + have hPs_get_lt : ∀ (i : Fin N.toNat), + Ps.get ⟨i.val, Nat.lt_succ_of_lt i.isLt⟩ = + pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val) := by + intro i + simp [Ps, List.Vector.get_ofFn, i.isLt] + have hPs_get_last : + Ps.get ⟨N.toNat, Nat.lt_succ_self _⟩ = + pedersenGenerator (p := p) + pedersenHashLengthBytes 0 := by + simp [Ps, List.Vector.get_ofFn] + enter_decl + steps [point_at_infinity_spec (p := p), + derive_generators_spec (p := p) (N := N) (M := (24 : U 32)) + (startIdx := separator)] + rename_i _hu domain_generators hDom + loop_inv nat fun (i : Nat) _ _ => + ∃∃ (s : Tp.denote p (Scalar.type.array (N + 1))) + (g : Tp.denote p (Point.type.array (N + 1))), + [scalars ↦ ⟨Scalar.type.array (N + 1), s⟩] ⋆ + [generators ↦ ⟨Point.type.array (N + 1), g⟩] ⋆ + ⟦∀ (j : Nat) (hj : j < i) (hjN : j < N.toNat) + (hjN1 : j < (N + 1).toNat), + fromFieldUnsafeRel (input.get ⟨j, hjN⟩) (s.get ⟨j, hjN1⟩) + ∧ g.get ⟨j, hjN1⟩ = domain_generators.get ⟨j, hjN⟩⟧ + · sl + sl + intro j hj _ _ + simp at hj + · simp + · intro i hlo hhi + steps [from_field_unsafe_spec (p := p)] + sl + rename_i s_prev g_prev hPrefix hCast1 xlo xhi hRes hModS hCast2 hModG _ + obtain ⟨h_mk, h_scalar, h_range⟩ := hRes + intro j hj hjN hjN1 + simp_all only [Lens.modify, Access.modify, Lens.get, + Option.bind_eq_bind, Option.bind_some, + Builtin.CastTp.cast, BitVec.toNat_intCast, BitVec.truncate_eq_setWidth, + BitVec.setWidth_eq, BitVec.toNat_ofNatLT] + have hiN1 : i < (BitVec.toNat N + 1) % 4294967296 := by + by_contra hcontra + simp [Nat.not_lt.mpr (Nat.le_of_not_lt hcontra)] at hModS + have hGoalBdd : i < (BitVec.add N 1).toNat := hiN1 + simp only [dif_pos hGoalBdd, Option.bind_some, Option.get_some] at * + by_cases h_eq : j = i + · subst h_eq + refine ⟨?_, ?_⟩ + · rw [List.Vector.get_set_same] + simp only [Scalar.mk] + exact ⟨h_scalar, h_range⟩ + · rw [List.Vector.get_set_same] + · have hjlt : j < i := by omega + have hne : (⟨i, hGoalBdd⟩ : Fin (BitVec.add N 1).toNat) ≠ ⟨j, hjN1⟩ := by + intro hh; exact h_eq ((Fin.mk.injEq _ _ _ _).mp hh).symm + rw [List.Vector.get_set_of_ne (v := s_prev) hne, + List.Vector.get_set_of_ne (v := g_prev) hne] + exact hPrefix j hjlt hjN hjN1 + steps [derive_generators_spec (p := p) (N := (1 : U 32)) (M := (20 : U 32)) + (startIdx := (0 : U 32))] + rename_i _hLo sFinal gFinal hInv hModSN _strLen hLenGen hLgBdd hModGN + simp only [Lens.modify, Access.modify, Lens.get, + Option.bind_eq_bind, Option.bind_some] at hModSN hModGN ⊢ + -- Extract `N.toNat < (BitVec.add N 1).toNat` from hModSN. + have hNlt_dite : N.toNat < (BitVec.toNat N + 1) % 4294967296 := by + by_contra hcontra + have hge : (BitVec.toNat N + 1) % 4294967296 ≤ N.toNat := Nat.le_of_not_lt hcontra + simp [Nat.not_lt.mpr hge] at hModSN + have hNlt : N.toNat < (BitVec.add N 1).toNat := hNlt_dite + simp only [dif_pos hNlt, Option.bind_some, Option.get_some] at hModSN hModGN ⊢ + -- The constraint `N.toNat < (N+1).toNat` together with the wrap-around behaviour + -- of `BitVec.add` forces `N.toNat + 1 < 2^32`. + have hN1_eq : (N + 1).toNat = N.toNat + 1 := by + -- (N + 1).toNat = (N.toNat + 1) % 2^32. The loop-bound hypothesis + -- `hNlt_dite : N.toNat < (N.toNat + 1) % 2^32` rules out wraparound. + have hadd : (N + 1).toNat = (N.toNat + 1) % 4294967296 := by + show BitVec.toNat (N + 1) = _ + simp [BitVec.toNat_add, BitVec.toNat_ofNat] + have hNbnd : N.toNat < 4294967296 := N.isLt + have hbnd : N.toNat + 1 < 4294967296 := by + rcases Nat.lt_or_ge (N.toNat + 1) 4294967296 with h | h + · exact h + · exfalso + have : N.toNat + 1 = 4294967296 := by omega + rw [this, Nat.mod_self] at hNlt_dite + omega + rw [hadd, Nat.mod_eq_of_lt hbnd] + let Ss : List.Vector (Scalar.denote p) N.toNat := + ⟨List.ofFn fun j : Fin N.toNat => sFinal.get ⟨j.val, by rw [hN1_eq]; omega⟩, + by simp⟩ + have hSs_get : ∀ (i : Fin N.toNat), + Ss.get i = sFinal.get ⟨i.val, by rw [hN1_eq]; omega⟩ := by + intro i + rw [List.Vector.get_eq_get_toList] + show (List.ofFn _).get _ = _ + simp + set lenScalar : Tp.denote p Scalar.type := + HList.toTuple p h![(Builtin.CastTp.cast N : Fp p), (Builtin.CastTp.cast ↑(0 : Fp p) : Fp p)] + (some «std-1.0.0-beta.14::embedded_curve_ops::EmbeddedCurveScalar».name) with hLenScalar_def + set lenGen : Tp.denote p Point.type := + length_generator.get ⟨BitVec.toNat ↑(0 : U 32), hLgBdd⟩ with hLenGen_def + set sFull : Tp.denote p (Scalar.type.array (N + 1)) := + sFinal.set ⟨N.toNat, hNlt⟩ lenScalar with hsFull_def + set gFull : Tp.denote p (Point.type.array (N + 1)) := + gFinal.set ⟨N.toNat, hNlt⟩ lenGen with hgFull_def + have hsFull_get : ∀ (i : Fin N.toNat) (hi : i.val < (N + 1).toNat), + sFull.get ⟨i.val, hi⟩ = sFinal.get ⟨i.val, by rw [hN1_eq]; omega⟩ := by + intro i hi + show (sFinal.set ⟨N.toNat, hNlt⟩ lenScalar).get _ = _ + rw [List.Vector.get_set_of_ne] + intro hh + have h_eq : N.toNat = i.val := (Fin.mk.injEq _ _ _ _).mp hh + have := i.isLt; omega + have hLenScalar_value : Scalar.valueNat lenScalar = N.toNat := by + show (Scalar.lo lenScalar).val + + pow128 * + (Scalar.hi lenScalar).val = N.toNat + show ((Builtin.CastTp.cast N : Fp p)).val + + pow128 * + ((Builtin.CastTp.cast ↑(0 : Fp p) : Fp p)).val = N.toNat + have hcast_zero : ((Builtin.CastTp.cast ↑(0 : Fp p) : Fp p)).val = 0 := by + show ((0 : Fp p)).val = 0 + simp + rw [hcast_zero, Nat.mul_zero, Nat.add_zero] + show ((Builtin.CastTp.cast N : Fp p)).val = N.toNat + show ((N.toNat : Fp p)).val = N.toNat + rw [ZMod.val_natCast] + apply Nat.mod_eq_of_lt + have hNbnd : N.toNat < 2^32 := N.isLt + have hp128 : (2^32 : Nat) < Lampe.pow128 := by decide + have hpprime := Lampe.Crypto.Bn254.pow128_lt_prime (p := p) + omega + set Ps_full : List.Vector (affineCurve p).Point (N + 1).toNat := + ⟨Ps.toList, by rw [List.Vector.toList_length]; exact hN1_eq.symm⟩ with hPs_full_def + have hPs_full_get : ∀ (k : Nat) (hk : k < (N + 1).toNat) (hk' : k < N.toNat + 1), + Ps_full.get ⟨k, hk⟩ = Ps.get ⟨k, hk'⟩ := by + intro k hk hk' + simp [Ps_full, List.Vector.get, List.Vector.toList] + have h_enc : gFull.toList = Ps_full.toList.map encodeCurvePoint := by + rw [← List.Vector.toList_map] + apply congrArg List.Vector.toList + apply List.Vector.ext + rintro ⟨k, hk⟩ + have hkSucc : k < N.toNat + 1 := by omega + by_cases h_isN : k = N.toNat + · + have hsetget : gFull.get ⟨k, hk⟩ = lenGen := by + show (gFinal.set ⟨N.toNat, hNlt⟩ lenGen).get ⟨k, hk⟩ = lenGen + have : (⟨k, hk⟩ : Fin (N + 1).toNat) = ⟨N.toNat, hNlt⟩ := by + apply Fin.ext; exact h_isN + rw [this, List.Vector.get_set_same] + rw [hsetget] + have hlg : lenGen = + pedersenGeneratorPoint p pedersenHashLengthBytes 0 := by + show length_generator.get _ = _ + rw [hLenGen] + simp only [strAsBytes_hash_length_eq (p := p)] + show (derivePedersenGenerators p pedersenHashLengthBytes 0 1).get + ⟨0, by decide⟩ = _ + rw [derivePedersenGenerators_get] + simp + rw [hlg] + symm + calc (Ps_full.map encodeCurvePoint).get ⟨k, hk⟩ + = encodeCurvePoint (Ps_full.get ⟨k, hk⟩) := by + simp [List.Vector.get_map] + _ = encodeCurvePoint (Ps.get ⟨k, hkSucc⟩) := by + rw [hPs_full_get k hk hkSucc] + _ = encodeCurvePoint + (Ps.get ⟨N.toNat, Nat.lt_succ_self _⟩) := by + congr 1; apply congrArg; apply Fin.ext; exact h_isN + _ = _ := h_len_gen + · have hkN : k < N.toNat := by omega + have hsetget : gFull.get ⟨k, hk⟩ = gFinal.get ⟨k, hk⟩ := by + show (gFinal.set ⟨N.toNat, hNlt⟩ lenGen).get ⟨k, hk⟩ = gFinal.get ⟨k, hk⟩ + rw [List.Vector.get_set_of_ne] + intro hh + exact h_isN ((Fin.mk.injEq _ _ _ _).mp hh).symm + rw [hsetget, (hInv k hkN hkN hk).2, hDom] + symm + calc (Ps_full.map encodeCurvePoint).get ⟨k, hk⟩ + = encodeCurvePoint (Ps_full.get ⟨k, hk⟩) := by + simp [List.Vector.get_map] + _ = encodeCurvePoint (Ps.get ⟨k, hkSucc⟩) := by + rw [hPs_full_get k hk hkSucc] + _ = pedersenGeneratorPoint p defaultDomainBytes + (BitVec.toNat separator + (⟨k, hkN⟩ : Fin N.toNat).val) := h_gen ⟨k, hkN⟩ + _ = (derivePedersenGenerators p defaultDomainBytes + (BitVec.toNat separator) N.toNat).get ⟨k, hkN⟩ := by + rw [derivePedersenGenerators_get] + have hGetEnc : ∀ i : Fin (N + 1).toNat, gFull.get i = + encodeCurvePoint (Ps_full.get i) := by + intro i + have hi_gFull : i.val < gFull.toList.length := by simp [List.Vector.toList_length] + have hi_Ps : i.val < Ps_full.toList.length := by simp [List.Vector.toList_length] + have hgFull_get_eq : gFull.get i = gFull.toList[i.val]'hi_gFull := by + rw [List.Vector.get_eq_get_toList]; rfl + have hPs_get_eq : Ps_full.get i = Ps_full.toList[i.val]'hi_Ps := by + rw [List.Vector.get_eq_get_toList]; rfl + rw [hgFull_get_eq, hPs_get_eq] + have h' := congrArg (fun l : List _ => l[i.val]?) h_enc + simp only at h' + rw [List.getElem?_eq_getElem hi_gFull, + List.getElem?_eq_getElem (by simp)] at h' + simp only [Option.some.injEq] at h' + rw [h'] + simp [List.getElem_map] + have hOnCurve : ∀ i : Fin (N + 1).toNat, + (curvePoint? (gFull.get i)).isSome = true := by + intro i + rw [hGetEnc i] + simp + have hSumEq : + (∑ i : Fin (N + 1).toNat, + Scalar.valueNat (sFull.get i) + • (curvePoint? (gFull.get i)).get (hOnCurve i)) = + ∑ i : Fin (N + 1).toNat, + Scalar.valueNat (sFull.get i) • Ps_full.get i := by + refine Finset.sum_congr rfl (fun i _ => ?_) + have hCp : curvePoint? (gFull.get i) = some (Ps_full.get i) := by + rw [hGetEnc i]; simp + rw [Option.get_of_eq_some _ hCp] + steps [Lampe.Stdlib.EmbeddedCurveOps.multi_scalar_mul_builtin_combined_spec + (p := p) (N := N + 1) (points := gFull) (scalars := sFull) hOnCurve] + case v => exact Ss + rcases (‹(∀ _, _) ∧ _› : + (∀ i, Scalar.Canonical (sFull.get i)) ∧ _) + with ⟨hCanonFull, hSumRes⟩ + refine ⟨?_, ?_⟩ + · + subst hSumRes + subst_vars + show pointX + (encodeCurvePoint _) = _ + congr 1 + congr 1 + show (∑ i : Fin (N + 1).toNat, + Scalar.valueNat (sFull.get i) + • (curvePoint? (gFull.get i)).get (hOnCurve i)) = _ + rw [hSumEq] + have hSumSplit : + (∑ i : Fin (N + 1).toNat, + Scalar.valueNat (sFull.get i) • Ps_full.get i) = + ∑ j : Fin (N.toNat + 1), + Scalar.valueNat + (sFull.get ⟨j.val, by rw [hN1_eq]; exact j.isLt⟩) • + Ps_full.get ⟨j.val, by rw [hN1_eq]; exact j.isLt⟩ := by + apply Finset.sum_equiv (finCongr hN1_eq) + (fun _ => Iff.intro (fun _ => Finset.mem_univ _) (fun _ => Finset.mem_univ _)) + (fun _ _ => by congr 2) + rw [hSumSplit] + rw [Fin.sum_univ_castSucc] + congr 1 + · + refine Finset.sum_congr rfl (fun i _ => ?_) + have hi_N1 : i.val < (N + 1).toNat := by rw [hN1_eq]; omega + have hcs_idx : (⟨(i.castSucc).val, by rw [hN1_eq]; exact (i.castSucc).isLt⟩ : + Fin (N + 1).toNat) = ⟨i.val, hi_N1⟩ := Fin.ext rfl + rw [hcs_idx, hsFull_get i hi_N1, + hPs_full_get i.val hi_N1 (Nat.lt_succ_of_lt i.isLt), + hPs_get_lt i, hSs_get i] + · + have hN_lt_N1 : N.toNat < (N + 1).toNat := hNlt + have hsFull_last : sFull.get ⟨N.toNat, hN_lt_N1⟩ = lenScalar := by + show (sFinal.set ⟨N.toNat, hNlt⟩ lenScalar).get _ = _ + rw [List.Vector.get_set_same] + have hPsFull_last : Ps_full.get ⟨N.toNat, hN_lt_N1⟩ = + Ps.get ⟨N.toNat, Nat.lt_succ_self _⟩ := + hPs_full_get N.toNat _ (Nat.lt_succ_self _) + have hidx : (⟨(Fin.last N.toNat).val, + by rw [hN1_eq]; exact (Fin.last N.toNat).isLt⟩ : + Fin (N + 1).toNat) = ⟨N.toNat, hN_lt_N1⟩ := Fin.ext rfl + rw [hidx, hsFull_last, hPsFull_last, hPs_get_last, hLenScalar_value] + · + intro i + have hi_N1 : i.val < (N + 1).toNat := by rw [hN1_eq]; omega + refine ⟨?_, ?_⟩ + · + rw [hSs_get i] + exact (hInv i.val i.isLt i.isLt (by omega)).1 + · + rw [hSs_get i, ← hsFull_get i hi_N1] + exact hCanonFull ⟨i.val, hi_N1⟩ + +/-- Deterministic closed-form of `pedersen_hash_with_separator_spec`: +the result is the pure `pedersenHash` (the +x-coordinate of the canonical-decomposition MSM, plus the length-slot +term `N • pedersenGenerator pedersenHashLengthBytes 0`). -/ +theorem pedersen_hash_with_separator_spec_canonical {p N} + [Lampe.Crypto.Bn254.Prime p] + {input : Tp.denote p (Tp.field.array N)} + {separator : U 32} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::pedersen_hash_with_separator».call h![N] + h![input, separator]) + (fun r => + r = pedersenHash p defaultDomainBytes input separator.toNat) := by + apply STHoare.consequence (h_pre_conseq := SLP.entails_self) ?_ + (pedersen_hash_with_separator_spec (p := p) (N := N) + (input := input) (separator := separator)) + intro r + rw [← SLP.star_exists] + apply SLP.exists_intro_l + intro Ss + apply SLP.pure_left + rintro ⟨h_eq, h_wit⟩ + have h_unique : ∀ i, Ss.get i = Scalar.canonicalDecomp (input.get i) := fun i => + Scalar.canonicalDecomp_unique (h_wit i).2 (h_wit i).1.2 (h_wit i).1.1 + have hSumEq : + (∑ i : Fin N.toNat, + Scalar.valueNat (Ss.get i) + • pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val)) = + ∑ i : Fin N.toNat, + Scalar.valueNat + (Scalar.canonicalDecomp (input.get i)) + • pedersenGenerator (p := p) + defaultDomainBytes (separator.toNat + i.val) := + Finset.sum_congr rfl (fun i _ => by rw [h_unique i]) + apply SLP.pure_right + · rw [pedersenHash_eq, h_eq, hSumEq] + · exact SLP.entails_top + +/-! ### `pedersen_commitment` wrapper spec -/ + +theorem pedersen_commitment_spec_canonical {p N} + [Lampe.Crypto.Bn254.Prime p] + {input : Tp.denote p (Tp.field.array N)} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::pedersen_commitment».call h![N] h![input]) + (fun r => + r = pedersenCommitment p defaultDomainBytes input 0) := by + enter_decl + steps [pedersen_commitment_with_separator_spec_canonical (p := p) (N := N) + (input := input) (separator := (0 : U 32))] + rename_i hPost + simpa using hPost + +/-! ### `pedersen_hash` wrapper spec -/ + +theorem pedersen_hash_spec_canonical {p N} + [Lampe.Crypto.Bn254.Prime p] + {input : Tp.denote p (Tp.field.array N)} : + STHoare p env ⟦⟧ + («std-1.0.0-beta.14::hash::pedersen_hash».call h![N] h![input]) + (fun r => + r = pedersenHash p defaultDomainBytes input 0) := by + enter_decl + steps [pedersen_hash_with_separator_spec_canonical (p := p) (N := N) + (input := input) (separator := (0 : U 32))] + rename_i hPost + simpa using hPost + +end Lampe.Stdlib.Hash.Pedersen