From 2cf905fbbab49683c8d476cb83596270d3bc9418 Mon Sep 17 00:00:00 2001 From: samdelaney Date: Mon, 6 Jul 2026 18:34:38 -0700 Subject: [PATCH 1/4] bullet rewrite --- zkp/lib/bullet/bullet.ak | 765 +++++++++++++++++++++++---------------- zkp/plutus.json | 2 +- 2 files changed, 450 insertions(+), 317 deletions(-) diff --git a/zkp/lib/bullet/bullet.ak b/zkp/lib/bullet/bullet.ak index bd53086..b846ea7 100644 --- a/zkp/lib/bullet/bullet.ak +++ b/zkp/lib/bullet/bullet.ak @@ -1,384 +1,517 @@ use aiken/collection/list use aiken/crypto +use aiken/crypto/bls12_381/g1 +use aiken/crypto/bls12_381/scalar use aiken/primitive/bytearray -use common/common -// Bulletproof specific types pub type BulletproofVerificationKey { - g: common.G1Point, - h: common.G1Point, - u: common.G1Point, - g_vec: List, - h_vec: List, + g: G1Element, + h: G1Element, + u: G1Element, + g_vec: List, + h_vec: List, + g_sum: G1Element, + h_sum: G1Element, n: Int, } -// Vector length (must be power of 2) - pub type BulletproofProof { - a: common.G1Point, - s: common.G1Point, - t1: common.G1Point, - t2: common.G1Point, - tau_x: common.Field, - mu: common.Field, - l_vec: List, - r_vec: List, + a: G1Element, + s: G1Element, + t1: G1Element, + t2: G1Element, + tau_x: scalar.Scalar, + mu: scalar.Scalar, + l_vec: List, + r_vec: List, } -pub type BulletproofError { - InvalidProofFormat - InvalidVerificationKey - InvalidVectorLength - PairingCheckFailed - InvalidRangeProof +pub type ProofBlinding { + alpha: scalar.Scalar, + rho: scalar.Scalar, + tau1: scalar.Scalar, + tau2: scalar.Scalar, + s_l: List, + s_r: List, } -// Main verification function -pub fn verify( +/// Derive a deterministic, nothing-up-my-sleeve set of generators for an +/// n-bit range proof. Meant to be computed once and embedded as a constant +/// verification key, not recomputed per transaction. +pub fn setup(n: Int) -> BulletproofVerificationKey { + let g = g1.generator + let h = g1.hash_to_group("h", "bulletproofs/base") + let u = g1.hash_to_group("u", "bulletproofs/base") + let indices = list.range(0, n - 1) + let g_vec = + list.map( + indices, + fn(i) { + g1.hash_to_group( + bytearray.from_int_big_endian(i, 4), + "bulletproofs/g_vec", + ) + }, + ) + let h_vec = + list.map( + indices, + fn(i) { + g1.hash_to_group( + bytearray.from_int_big_endian(i, 4), + "bulletproofs/h_vec", + ) + }, + ) + let g_sum = list.foldl(g_vec, g1.zero, g1.add) + let h_sum = list.foldl(h_vec, g1.zero, g1.add) + BulletproofVerificationKey { g, h, u, g_vec, h_vec, g_sum, h_sum, n } +} + +/// Public Pedersen commitment to a hidden value: V = g^value * h^gamma. +pub fn commit_value( vk: BulletproofVerificationKey, - proof: BulletproofProof, - value: common.Field, -) -> Bool { - // First verify the vector length is valid - if !verify_power_of_two(vk.n) { - False + value: Int, + gamma: scalar.Scalar, +) -> G1Element { + expect Some(value_scalar) = scalar.new(value) + g1.add(g1.scale(vk.g, value_scalar), g1.scale(vk.h, gamma)) +} + +/// Generate a range proof that `value` lies in `[0, 2^vk.n)` given a Pedersen +/// commitment blinding `gamma`. Aiken has no RNG, so all blinding factors used +/// internally must be supplied explicitly by the caller. +pub fn generate_proof( + vk: BulletproofVerificationKey, + value: Int, + gamma: scalar.Scalar, + blinding: ProofBlinding, +) -> BulletproofProof { + if value < 0 || value >= pow2(vk.n) { + fail @"value out of range" } else { - // Verify the range proof - verify_range_proof(vk, proof, value, vk.n) + generate_proof_unchecked(vk, value, gamma, blinding) } } -// Helper functions for verification -fn verify_inner_product( - g_vec: List, - h_vec: List, - u: common.G1Point, - p: common.G1Point, - _c: common.Field, - l_vec: List, - r_vec: List, -) -> Bool { - let inner_prod = compute_inner_product(l_vec, r_vec) - let g_commit = compute_vector_commitments(l_vec, g_vec) - let h_commit = compute_vector_commitments(r_vec, h_vec) - let u_scaled = - common.Point { - x: u.x * inner_prod % common.bls12_381_prime, - y: u.y * inner_prod % common.bls12_381_prime, - z: u.z * inner_prod % common.bls12_381_prime, - } - let lhs = p - let rhs = - common.Point { - x: common.mod_add(common.mod_add(g_commit.x, h_commit.x), u_scaled.x), - y: common.mod_add(common.mod_add(g_commit.y, h_commit.y), u_scaled.y), - z: common.mod_add(common.mod_add(g_commit.z, h_commit.z), u_scaled.z), - } - // Compare points - lhs.x == rhs.x && lhs.y == rhs.y && lhs.z == rhs.z +/// Test-only convenience prover: derives blinding factors from a seed instead +/// of requiring the caller to supply real entropy. +pub fn generate_proof_deterministic( + vk: BulletproofVerificationKey, + value: Int, + gamma: scalar.Scalar, + seed: ByteArray, +) -> BulletproofProof { + generate_proof(vk, value, gamma, derive_blinding(seed, vk.n)) } -fn compute_challenges( +fn generate_proof_unchecked( vk: BulletproofVerificationKey, - proof: BulletproofProof, - value: common.Field, -) -> List { - // Initial transcript with verification key components - let initial_transcript = - generate_transcript( - // may be able to use common.serialize_vkey here - list.foldl( - [ - common.g1_compress(vk.g), - common.g1_compress(vk.h), - common.g1_compress(vk.u), - common.serialize_field(value), - ], - "", - bytearray.concat, - ), - ) + value: Int, + gamma: scalar.Scalar, + blinding: ProofBlinding, +) -> BulletproofProof { + if list.length(blinding.s_l) != vk.n || list.length(blinding.s_r) != vk.n { + fail @"blinding vector length mismatch" + } else { + let bits = bits_of(value, vk.n) + let a_l = list.map(bits, scalar_from_bit) + let a_r = list.map(a_l, fn(ai) { scalar.sub(ai, scalar.one) }) - // Add proof components to transcript - let proof_transcript = - generate_transcript( - list.foldl( - [ - initial_transcript, - common.g1_compress(proof.a), - common.g1_compress(proof.s), - common.g1_compress(proof.t1), - common.g1_compress(proof.t2), - ], - "", - bytearray.concat, - ), - ) + let v_commit = commit_value(vk, value, gamma) - // Generate challenges using the transcript - let challenge1 = - proof_transcript - |> generate_transcript - - let challenge2 = - challenge1 - |> generate_transcript - - let challenge3 = - challenge2 - |> generate_transcript - - list.map( - [challenge1, challenge2, challenge3], - fn(x) { - x - |> common.deserialize_field - |> unwrap_field_option - }, - ) -} + let a_point = + g1.add( + g1.scale(vk.h, blinding.alpha), + g1.add(vector_commit(a_l, vk.g_vec), vector_commit(a_r, vk.h_vec)), + ) + let s_point = + g1.add( + g1.scale(vk.h, blinding.rho), + g1.add( + vector_commit(blinding.s_l, vk.g_vec), + vector_commit(blinding.s_r, vk.h_vec), + ), + ) + + let state1 = + transcript_absorb2(transcript_init(vk, v_commit), a_point, s_point) + let y = hash_to_scalar(bytearray.concat(state1, "y")) + let z = hash_to_scalar(bytearray.concat(state1, "z")) + + let two = scalar.add(scalar.one, scalar.one) + let z2 = scalar.mul(z, z) + let y_pow = powers_of(y, vk.n) + let two_pow = powers_of(two, vk.n) + + let l0 = list.map(a_l, fn(ai) { scalar.sub(ai, z) }) + let l1 = blinding.s_l + let r0 = + list.map3( + a_r, + y_pow, + two_pow, + fn(ari, yi, ti) { + scalar.add(scalar.mul(yi, scalar.add(ari, z)), scalar.mul(z2, ti)) + }, + ) + let r1 = list.map2(y_pow, blinding.s_r, scalar.mul) + + let t1_coef = + scalar.add(scalar_inner_product(l0, r1), scalar_inner_product(l1, r0)) + let t2_coef = scalar_inner_product(l1, r1) + + let t1_point = + g1.add(g1.scale(vk.g, t1_coef), g1.scale(vk.h, blinding.tau1)) + let t2_point = + g1.add(g1.scale(vk.g, t2_coef), g1.scale(vk.h, blinding.tau2)) + + let state2 = transcript_absorb2(state1, t1_point, t2_point) + let x = hash_to_scalar(bytearray.concat(state2, "x")) + + let l_vec = + list.map2(l0, l1, fn(l0i, l1i) { scalar.add(l0i, scalar.mul(x, l1i)) }) + let r_vec = + list.map2(r0, r1, fn(r0i, r1i) { scalar.add(r0i, scalar.mul(x, r1i)) }) + + let tau_x = + scalar.add( + scalar.mul(z2, gamma), + scalar.add( + scalar.mul(blinding.tau1, x), + scalar.mul(blinding.tau2, scalar.mul(x, x)), + ), + ) + let mu = scalar.add(blinding.alpha, scalar.mul(blinding.rho, x)) -fn unwrap_field_option(field: Option) -> common.Field { - when field is { - Some(x) -> x - None -> fail @"Field value is None" + BulletproofProof { + a: a_point, + s: s_point, + t1: t1_point, + t2: t2_point, + tau_x, + mu, + l_vec, + r_vec, + } } } -fn verify_range_proof( +/// Named helper (not an inline lambda) — a bare bit (0/1) is always a valid +/// field element, so this cannot fail in practice. +fn scalar_from_bit(b: Int) -> scalar.Scalar { + expect Some(s) = scalar.new(b) + s +} + +fn derive_blinding(seed: ByteArray, n: Int) -> ProofBlinding { + let alpha = hash_to_scalar(bytearray.concat(seed, "alpha")) + let rho = hash_to_scalar(bytearray.concat(seed, "rho")) + let tau1 = hash_to_scalar(bytearray.concat(seed, "tau1")) + let tau2 = hash_to_scalar(bytearray.concat(seed, "tau2")) + let indices = list.range(0, n - 1) + let s_l = + list.map( + indices, + fn(i) { + hash_to_scalar( + bytearray.concat( + seed, + bytearray.concat("s_l", bytearray.from_int_big_endian(i, 4)), + ), + ) + }, + ) + let s_r = + list.map( + indices, + fn(i) { + hash_to_scalar( + bytearray.concat( + seed, + bytearray.concat("s_r", bytearray.from_int_big_endian(i, 4)), + ), + ) + }, + ) + ProofBlinding { alpha, rho, tau1, tau2, s_l, s_r } +} + +/// Verify a range proof against a public Pedersen commitment. Never takes the +/// hidden value or its blinding factor. +pub fn verify( vk: BulletproofVerificationKey, + v_commit: G1Element, proof: BulletproofProof, - value: common.Field, - bit_length: Int, ) -> Bool { - // 1. Compute challenges - let challenges = compute_challenges(vk, proof, value) - when challenges is { - [x, _y, _z] -> { - // 2. Verify the commitment matches - let commitment = commit(value, proof.tau_x, vk.g, vk.h) - // 3. Verify vector lengths match the expected bit length - if list.length(proof.l_vec) != bit_length || list.length(proof.r_vec) != bit_length { - False - } else { - // 4. Verify the inner product argument - let p = - common.Point { - x: common.mod_add( - commitment.x, - common.mod_add(proof.t1.x, proof.t2.x), - ), - y: common.mod_add( - commitment.y, - common.mod_add(proof.t1.y, proof.t2.y), + if list.length(proof.l_vec) != vk.n || list.length(proof.r_vec) != vk.n { + False + } else { + let state1 = + transcript_absorb2(transcript_init(vk, v_commit), proof.a, proof.s) + let y = hash_to_scalar(bytearray.concat(state1, "y")) + let z = hash_to_scalar(bytearray.concat(state1, "z")) + let state2 = transcript_absorb2(state1, proof.t1, proof.t2) + let x = hash_to_scalar(bytearray.concat(state2, "x")) + + when scalar.recip(y) is { + None -> False + Some(y_inv) -> { + let two = scalar.add(scalar.one, scalar.one) + let y_pow = powers_of(y, vk.n) + let two_pow = powers_of(two, vk.n) + let sum_y = scalar_sum(y_pow) + let sum_2 = scalar_sum(two_pow) + + let z2 = scalar.mul(z, z) + let z3 = scalar.mul(z2, z) + let delta = + scalar.sub( + scalar.mul(scalar.sub(z, z2), sum_y), + scalar.mul(z3, sum_2), + ) + + let t_hat = scalar_inner_product(proof.l_vec, proof.r_vec) + + let lhs1 = g1.add(g1.scale(vk.g, t_hat), g1.scale(vk.h, proof.tau_x)) + let rhs1 = + g1.add( + g1.scale(v_commit, z2), + g1.add( + g1.scale(vk.g, delta), + g1.add( + g1.scale(proof.t1, x), + g1.scale(proof.t2, scalar.mul(x, x)), + ), ), - z: common.mod_add( - commitment.z, - common.mod_add(proof.t1.z, proof.t2.z), + ) + let check1 = g1.equal(lhs1, rhs1) + + let y_inv_pow = powers_of(y_inv, vk.n) + let h_prime = + list.map2( + vk.h_vec, + y_inv_pow, + fn(h_i, yi_inv) { g1.scale(h_i, yi_inv) }, + ) + let r_adj = + list.map2( + proof.r_vec, + two_pow, + fn(ri, ti) { scalar.sub(ri, scalar.mul(z2, ti)) }, + ) + + let g_l_commit = vector_commit(proof.l_vec, vk.g_vec) + let h_r_commit = vector_commit(r_adj, h_prime) + + let lhs2 = g1.add(proof.a, g1.scale(proof.s, x)) + let rhs2 = + g1.add( + g1.scale(vk.h, proof.mu), + g1.add( + g_l_commit, + g1.add(h_r_commit, g1.scale(g1.sub(vk.g_sum, vk.h_sum), z)), ), - } - verify_inner_product( - vk.g_vec, - vk.h_vec, - vk.u, - p, - x, - proof.l_vec, - proof.r_vec, - ) + ) + let check2 = g1.equal(lhs2, rhs2) + + check1 && check2 } } - _ -> False } } -fn generate_transcript(data: ByteArray) -> ByteArray { - crypto.blake2b_256(data) -} - -// Function to generate a Bulletproof proof -pub fn generate_proof( - value: common.Field, - randomness: common.Field, - bit_length: Int, +fn transcript_init( vk: BulletproofVerificationKey, -) -> BulletproofProof { - // 1. Generate the Pedersen commitment - let a = commit(value, randomness, vk.g, vk.h) - // 2. Generate random blinding factors - let tau_x = - crypto.blake2b_256( + v_commit: G1Element, +) -> ByteArray { + crypto.blake2b_256( + bytearray.concat( + g1.compress(vk.g), bytearray.concat( - common.field_to_bytes(value), - common.field_to_bytes(randomness), + g1.compress(vk.h), + bytearray.concat( + g1.compress(vk.u), + bytearray.concat( + bytearray.from_int_big_endian(vk.n, 4), + g1.compress(v_commit), + ), + ), ), - ) - |> common.bytes_to_field - let mu = - crypto.blake2b_256(common.field_to_bytes(tau_x)) |> common.bytes_to_field - - // 3. Generate the vector commitments - let bit_vec = decompose_into_bits(value, bit_length) - let l_vec = vector_scalar_multiplication(bit_vec, tau_x) - let r_vec = vector_scalar_multiplication(bit_vec, mu) - // 4. Generate t1 and t2 commitments - let t1 = compute_vector_commitments(l_vec, vk.g_vec) - let t2 = compute_vector_commitments(r_vec, vk.h_vec) - // 5. Generate s commitment - let s = - common.Point { - x: vk.h.x * mu % common.bls12_381_prime, - y: vk.h.y * mu % common.bls12_381_prime, - z: vk.h.z * mu % common.bls12_381_prime, - } + ), + ) +} - BulletproofProof { a, s, t1, t2, tau_x, mu, l_vec, r_vec } +fn transcript_absorb2( + state: ByteArray, + p1: G1Element, + p2: G1Element, +) -> ByteArray { + crypto.blake2b_256( + bytearray.concat(state, bytearray.concat(g1.compress(p1), g1.compress(p2))), + ) } -// Helper function to decompose a value into its binary representation -fn decompose_into_bits( - value: common.Field, - bit_length: Int, -) -> List { - if bit_length == 0 { - [] - } else { - let bit = value % 2 - let next_value = value / 2 - [bit, ..decompose_into_bits(next_value, bit_length - 1)] - } +/// Hash-and-increment into the scalar field. A single blake2b_256 digest +/// interpreted as a big-endian integer lands outside `field_prime` (~45% of +/// 2^256) about 55% of the time, so a single-shot hash-to-scalar traps +/// unacceptably often; retry with an incrementing counter instead. +fn hash_to_scalar(seed: ByteArray) -> scalar.Scalar { + hash_to_scalar_loop(seed, 0) } -// Function to create a Pedersen commitment -fn commit( - value: common.Field, - randomness: common.Field, - g: common.G1Point, - h: common.G1Point, -) -> common.G1Point { - let g_scaled = - common.Point { - x: g.x * value % common.bls12_381_prime, - y: g.y * value % common.bls12_381_prime, - z: g.z * value % common.bls12_381_prime, - } - let h_scaled = - common.Point { - x: h.x * randomness % common.bls12_381_prime, - y: h.y * randomness % common.bls12_381_prime, - z: h.z * randomness % common.bls12_381_prime, - } - // Add the two scaled points - common.Point { - x: common.mod_add(g_scaled.x, h_scaled.x), - y: common.mod_add(g_scaled.y, h_scaled.y), - z: common.mod_add(g_scaled.z, h_scaled.z), +fn hash_to_scalar_loop(seed: ByteArray, counter: Int) -> scalar.Scalar { + let digest = + crypto.blake2b_256( + bytearray.concat(seed, bytearray.from_int_big_endian(counter, 1)), + ) + when scalar.from_bytearray_big_endian(digest) is { + Some(s) -> s + None -> hash_to_scalar_loop(seed, counter + 1) } } -// Function to compute the inner product of two vectors -pub fn compute_inner_product( - l_vec: List, - r_vec: List, -) -> common.Field { - when (l_vec, r_vec) is { - ([], []) -> 0 +fn powers_of(base: scalar.Scalar, count: Int) -> List { + list.map(list.range(0, count - 1), fn(i) { scalar.scale(base, i) }) +} + +fn scalar_sum(vec: List) -> scalar.Scalar { + list.foldl(vec, scalar.zero, scalar.add) +} + +fn scalar_inner_product( + l: List, + r: List, +) -> scalar.Scalar { + when (l, r) is { + ([], []) -> scalar.zero ([x, ..xs], [y, ..ys]) -> - common.mod_add( - x * y % common.bls12_381_prime, - compute_inner_product(xs, ys), - ) - (_, _) -> fail @"Vector lengths must match" + scalar.add(scalar.mul(x, y), scalar_inner_product(xs, ys)) + (_, _) -> fail @"vector length mismatch" } } -// Function to verify that a number is a power of two -pub fn verify_power_of_two(n: Int) -> Bool { - if n <= 0 { - False - } else { - // A number is a power of 2 if it has exactly one bit set - // In Aiken, we can't directly do bitwise operations like n & (n-1) - // So we'll use a recursive approach to check if n is a power of 2 - check_power_of_two(n, 0) +fn vector_commit( + scalars: List, + points: List, +) -> G1Element { + when (scalars, points) is { + ([], []) -> g1.zero + ([s, ..ss], [p, ..ps]) -> g1.add(g1.scale(p, s), vector_commit(ss, ps)) + (_, _) -> fail @"vector length mismatch" } } -fn check_power_of_two(n: Int, count: Int) -> Bool { - if n == 0 { - count == 1 - } else if n % 2 == 1 { - check_power_of_two(n / 2, count + 1) +fn bits_of(value: Int, remaining: Int) -> List { + if remaining == 0 { + [] } else { - check_power_of_two(n / 2, count) + [value % 2, ..bits_of(value / 2, remaining - 1)] } } -// Function to compute vector commitments -pub fn compute_vector_commitments( - vec: List, - g_vec: List, -) -> common.G1Point { - when (vec, g_vec) is { - ([], []) -> - // Return point at infinity (identity element) - common.Point { x: 0, y: 0, z: 0 } - ([s, ..ss], [g, ..gs]) -> { - let scaled = - common.Point { - x: g.x * s % common.bls12_381_prime, - y: g.y * s % common.bls12_381_prime, - z: g.z * s % common.bls12_381_prime, - } - let rest = compute_vector_commitments(ss, gs) - // Add points using BLS12-381 point addition - common.Point { - x: common.mod_add(scaled.x, rest.x), - y: common.mod_add(scaled.y, rest.y), - z: common.mod_add(scaled.z, rest.z), - } - } - (_, _) -> fail @"Vector lengths must match" +fn pow2(n: Int) -> Int { + if n <= 0 { + 1 + } else { + 2 * pow2(n - 1) } } -// Function for vector addition -pub fn vector_addition( - vec1: List, - vec2: List, -) -> List { - when (vec1, vec2) is { - ([], []) -> [] - ([x, ..xs], [y, ..ys]) -> [common.mod_add(x, y), ..vector_addition(xs, ys)] - (_, _) -> fail @"Vector lengths must match" +test setup_smoke() { + let vk = setup(8) + and { + list.length(vk.g_vec) == 8, + list.length(vk.h_vec) == 8, + !g1.equal(vk.g_sum, g1.zero), + !g1.equal(vk.h_sum, g1.zero), } } -// Function for vector scalar multiplication -pub fn vector_scalar_multiplication( - vec: List, - scalar: common.Field, -) -> List { - when vec is { - [] -> [] - [x, ..xs] -> - [ - x * scalar % common.bls12_381_prime, - ..vector_scalar_multiplication(xs, scalar) - ] - } +test range_proof_valid() { + let vk = setup(8) + expect Some(gamma) = scalar.new(12345) + let value = 200 + let proof = generate_proof_deterministic(vk, value, gamma, "seed-1") + let v_commit = commit_value(vk, value, gamma) + verify(vk, v_commit, proof) } -// Function for Hadamard product of two vectors -pub fn hadamard_product( - vec1: List, - vec2: List, -) -> List { - when (vec1, vec2) is { - ([], []) -> [] - ([x, ..xs], [y, ..ys]) -> - [x * y % common.bls12_381_prime, ..hadamard_product(xs, ys)] - (_, _) -> fail @"Vector lengths must match" - } +test range_proof_valid_zero() { + let vk = setup(8) + expect Some(gamma) = scalar.new(777) + let value = 0 + let proof = generate_proof_deterministic(vk, value, gamma, "seed-2") + let v_commit = commit_value(vk, value, gamma) + verify(vk, v_commit, proof) +} + +test range_proof_valid_max() { + let vk = setup(8) + expect Some(gamma) = scalar.new(9999) + let value = 255 + let proof = generate_proof_deterministic(vk, value, gamma, "seed-3") + let v_commit = commit_value(vk, value, gamma) + verify(vk, v_commit, proof) +} + +test range_proof_fails_wrong_commitment() { + let vk = setup(8) + expect Some(gamma) = scalar.new(12345) + let value = 200 + let proof = generate_proof_deterministic(vk, value, gamma, "seed-4") + let wrong_commit = commit_value(vk, value + 1, gamma) + !verify(vk, wrong_commit, proof) +} + +test range_proof_fails_tampered_tau_x() { + let vk = setup(8) + expect Some(gamma) = scalar.new(12345) + let value = 200 + let proof = generate_proof_deterministic(vk, value, gamma, "seed-5") + let v_commit = commit_value(vk, value, gamma) + let tampered = + BulletproofProof { ..proof, tau_x: scalar.add(proof.tau_x, scalar.one) } + !verify(vk, v_commit, tampered) +} + +test range_proof_fails_tampered_l_vec() { + let vk = setup(8) + expect Some(gamma) = scalar.new(12345) + let value = 200 + let proof = generate_proof_deterministic(vk, value, gamma, "seed-6") + let v_commit = commit_value(vk, value, gamma) + expect [first, ..rest] = proof.l_vec + let tampered = + BulletproofProof { ..proof, l_vec: [scalar.add(first, scalar.one), ..rest] } + !verify(vk, v_commit, tampered) +} + +test range_proof_fails_wrong_vector_length() { + let vk = setup(8) + expect Some(gamma) = scalar.new(12345) + let value = 200 + let proof = generate_proof_deterministic(vk, value, gamma, "seed-7") + let v_commit = commit_value(vk, value, gamma) + expect [_, ..rest] = proof.l_vec + let tampered = BulletproofProof { ..proof, l_vec: rest } + !verify(vk, v_commit, tampered) +} + +test generate_proof_rejects_out_of_range() fail { + let vk = setup(8) + expect Some(gamma) = scalar.new(1) + let blinding = derive_blinding("seed-8", vk.n) + let proof = generate_proof(vk, 256, gamma, blinding) + list.length(proof.l_vec) == vk.n +} + +test range_proof_fails_out_of_range_bypassing_guard() { + let vk = setup(8) + expect Some(gamma) = scalar.new(555) + let value = 256 + let blinding = derive_blinding("seed-9", vk.n) + let proof = generate_proof_unchecked(vk, value, gamma, blinding) + let v_commit = commit_value(vk, value, gamma) + !verify(vk, v_commit, proof) } diff --git a/zkp/plutus.json b/zkp/plutus.json index 852267f..6533b50 100644 --- a/zkp/plutus.json +++ b/zkp/plutus.json @@ -6,7 +6,7 @@ "plutusVersion": "v3", "compiler": { "name": "Aiken", - "version": "v1.1.15+f03633e" + "version": "v1.1.21+42babe5" }, "license": "Apache-2.0" }, From 2a767421ccbb29570b4fd57ca44dcf12c441bd53 Mon Sep 17 00:00:00 2001 From: samdelaney Date: Wed, 8 Jul 2026 13:47:04 -0700 Subject: [PATCH 2/4] changes per review --- zkp/lib/bullet/bullet.ak | 85 ++++++++++++++++++++++++---------------- 1 file changed, 52 insertions(+), 33 deletions(-) diff --git a/zkp/lib/bullet/bullet.ak b/zkp/lib/bullet/bullet.ak index b846ea7..954bf21 100644 --- a/zkp/lib/bullet/bullet.ak +++ b/zkp/lib/bullet/bullet.ak @@ -4,6 +4,16 @@ use aiken/crypto/bls12_381/g1 use aiken/crypto/bls12_381/scalar use aiken/primitive/bytearray +/// Prepended to every generator derivation and transcript hash so this +/// protocol's challenges/generators can never collide with another +/// proof system's, even if both happened to hash the same raw bytes. +const protocol_id: ByteArray = "adao-zkp/bulletproofs-range-proof/v1" + +/// Range proofs wider than this are refused: `n` drives O(n) recursion +/// (bit decomposition, vector commitments, scalar products) both here and +/// in `verify`, so an unbounded `n` is an unbounded compute-cost knob. +const max_n: Int = 64 + pub type BulletproofVerificationKey { g: G1Element, h: G1Element, @@ -39,33 +49,37 @@ pub type ProofBlinding { /// n-bit range proof. Meant to be computed once and embedded as a constant /// verification key, not recomputed per transaction. pub fn setup(n: Int) -> BulletproofVerificationKey { - let g = g1.generator - let h = g1.hash_to_group("h", "bulletproofs/base") - let u = g1.hash_to_group("u", "bulletproofs/base") - let indices = list.range(0, n - 1) - let g_vec = - list.map( - indices, - fn(i) { - g1.hash_to_group( - bytearray.from_int_big_endian(i, 4), - "bulletproofs/g_vec", - ) - }, - ) - let h_vec = - list.map( - indices, - fn(i) { - g1.hash_to_group( - bytearray.from_int_big_endian(i, 4), - "bulletproofs/h_vec", - ) - }, - ) - let g_sum = list.foldl(g_vec, g1.zero, g1.add) - let h_sum = list.foldl(h_vec, g1.zero, g1.add) - BulletproofVerificationKey { g, h, u, g_vec, h_vec, g_sum, h_sum, n } + if n <= 0 || n > max_n { + fail @"n must be between 1 and max_n" + } else { + let g = g1.generator + let h = g1.hash_to_group("h", bytearray.concat(protocol_id, "/base")) + let u = g1.hash_to_group("u", bytearray.concat(protocol_id, "/base")) + let indices = list.range(0, n - 1) + let g_vec = + list.map( + indices, + fn(i) { + g1.hash_to_group( + bytearray.from_int_big_endian(i, 4), + bytearray.concat(protocol_id, "/g_vec"), + ) + }, + ) + let h_vec = + list.map( + indices, + fn(i) { + g1.hash_to_group( + bytearray.from_int_big_endian(i, 4), + bytearray.concat(protocol_id, "/h_vec"), + ) + }, + ) + let g_sum = list.foldl(g_vec, g1.zero, g1.add) + let h_sum = list.foldl(h_vec, g1.zero, g1.add) + BulletproofVerificationKey { g, h, u, g_vec, h_vec, g_sum, h_sum, n } + } } /// Public Pedersen commitment to a hidden value: V = g^value * h^gamma. @@ -244,7 +258,9 @@ pub fn verify( v_commit: G1Element, proof: BulletproofProof, ) -> Bool { - if list.length(proof.l_vec) != vk.n || list.length(proof.r_vec) != vk.n { + if vk.n <= 0 || vk.n > max_n { + False + } else if list.length(proof.l_vec) != vk.n || list.length(proof.r_vec) != vk.n { False } else { let state1 = @@ -327,14 +343,17 @@ fn transcript_init( ) -> ByteArray { crypto.blake2b_256( bytearray.concat( - g1.compress(vk.g), + protocol_id, bytearray.concat( - g1.compress(vk.h), + g1.compress(vk.g), bytearray.concat( - g1.compress(vk.u), + g1.compress(vk.h), bytearray.concat( - bytearray.from_int_big_endian(vk.n, 4), - g1.compress(v_commit), + g1.compress(vk.u), + bytearray.concat( + bytearray.from_int_big_endian(vk.n, 4), + g1.compress(v_commit), + ), ), ), ), From 5abca8f3fecc28936180140a7b57da79830e98f5 Mon Sep 17 00:00:00 2001 From: samdelaney Date: Wed, 8 Jul 2026 14:06:52 -0700 Subject: [PATCH 3/4] bulletproofs documentation --- .../bulletproofs-implementation-report.md | 124 +++++++++++++++ zkp/docs/step-by-step.md | 147 +++++++++++------- 2 files changed, 219 insertions(+), 52 deletions(-) create mode 100644 zkp/docs/bulletproofs-implementation-report.md diff --git a/zkp/docs/bulletproofs-implementation-report.md b/zkp/docs/bulletproofs-implementation-report.md new file mode 100644 index 0000000..f198030 --- /dev/null +++ b/zkp/docs/bulletproofs-implementation-report.md @@ -0,0 +1,124 @@ +# Bulletproofs Range-Proof Verifier - Implementation Report + +- **Module:** `zkp/lib/bullet/bullet.ak` +- **Status:** Functional, tested, unaudited +- **Test results:** + - `aiken check` 13/13 + - `aiken fmt` clean + - `aiken build` succeeds + +## 1. Overview + +This module implements a Bulletproofs-style zero-knowledge range proof over the BLS12-381 curve, as one of three zero-knowledge proof systems in this repository's `zkp` package for Cardano smart contracts (Aiken, targeting Plutus V3). Given a Pedersen commitment `V` to a hidden integer value, it proves that the committed value lies in `[0, 2^n)` without revealing the value or its blinding factor. + +Bulletproofs were chosen alongside Groth16 and PLONK specifically because they require **no trusted setup** - public parameters are derived deterministically from public strings, which removes an entire class of trusted-ceremony risk that the other two proof systems in this package carry. + +This report covers the implementation as it stands: what was built, how it works, where it deliberately departs from the canonical construction and from typical general-purpose Bulletproofs libraries, and what remains before it is production- or audit-ready. + +## 2. Position within the `zkp` package + +| Module | Proof system | Setup | Core primitive | +|---|---|---|---| +| `lib/groth` | Groth16 | Trusted, circuit-specific | Pairings (`bls12_381_miller_loop`, `bls12_381_final_verify`) | +| `lib/plonk` | PLONK | Universal, trusted | Kate commitments, permutation argument | +| `lib/bullet` | Bulletproofs | Public, trustless | Discrete-log / Pedersen commitments, no pairings | +| `lib/common` | — | — | Shared field/point scaffolding, superseded in this module (see §4) | + +All 3 modules follow the same conventions (error handling, test structure) adopted here. + +## 3. Architecture + +**Types** + +``` +BulletproofVerificationKey { g, h, u, g_vec, h_vec, g_sum, h_sum, n } +BulletproofProof { a, s, t1, t2, tau_x, mu, l_vec, r_vec } +ProofBlinding { alpha, rho, tau1, tau2, s_l, s_r } +``` + +`g`, `h`, `u`, and every entry of `g_vec`/`h_vec` are native `G1Element` values; `tau_x`, `mu`, and every entry of `l_vec`/`r_vec` are native `Scalar` values from the BLS12-381 scalar field. `g_sum`/`h_sum` are precomputed folds of the generator vectors, carried in the key to avoid re-summing `n` points on every verification. + +**Entry points** + +- `setup(n) -> BulletproofVerificationKey` - derives all generators deterministically. +- `commit_value(vk, value, gamma) -> G1Element` - builds the public Pedersen commitment `V`. +- `generate_proof(vk, value, gamma, blinding) -> BulletproofProof` - the reference prover. +- `verify(vk, v_commit, proof) -> Bool` - the verifier; the only function a validator needs. + +## 4. Protocol walkthrough + +**Setup.** `setup(n)` derives `g` (the curve's standard generator), `h`, `u`, and length-`n` vectors `g_vec`/`h_vec` via `hash_to_group` with distinct domain-separation tags. This is nothing-up-my-sleeve by construction - no party ever holds a discrete-log relationship between any two generators - and is meant to be computed once and embedded as a deployed constant, not recomputed per transaction. + +**Commitment.** `commit_value` builds `V = g^value · h^gamma`, a standard Pedersen commitment. + +**Proof generation.** Given `value`, its blinding `gamma`, and a `ProofBlinding` record (Aiken has no RNG, so every random scalar the protocol needs is an explicit caller-supplied input): + +1. Decompose `value` into bits `a_L`; set `a_R = a_L - 1`. +2. Commit `A = h^alpha · g_vec^{a_L} · h_vec^{a_R}` and `S = h^rho · g_vec^{s_L} · h_vec^{s_R}`. +3. Derive challenges `y, z` from a transcript over `(vk, V, A, S)`. +4. Build the linear vector polynomials `l(X) = (a_L - z·1) + X·s_L` and `r(X) = y^n∘(a_R + z·1) + z^2·2^n + X·(y^n∘s_R)`, and their inner product `t(X) = t0 + t1·X + t2·X^2`. +5. Commit `T1 = g^{t1}·h^{tau1}`, `T2 = g^{t2}·h^{tau2}`. +6. Derive challenge `x` from a transcript continuing over `(T1, T2)`. +7. Evaluate `l_vec = l(x)`, `r_vec = r(x)`, and compute `tau_x = z^2·gamma + tau1·x + tau2·x^2`, `mu = alpha + rho·x`. + +**Verification.** `verify` recomputes `y, z, x` from the identical transcript, then checks two equations: + +- **t-commitment check:** `g^{t_hat}·h^{tau_x} == V^{z^2}·g^{delta(y,z)}·T1^x·T2^{x^2}`, where `t_hat = ⟨l_vec, r_vec⟩` is recomputed directly and `delta(y,z) = (z - z^2)·Σy^i - z^3·Σ2^i` is the standard closed-form correction term. +- **vector-opening check:** `A·S^x == h^mu·g_vec^{l_vec}·h'^{r_vec - z^2·2^n}·(g_sum/h_sum)^z`, where `h'_i = h_vec_i^{y^{-i}}` - the standard pre-compression Bulletproofs identity. + +Both checks together are what bind the proof to a genuine bit-decomposition of the committed value; §6 details why. + +## 5. Design differentiation from canonical Bulletproofs and general-purpose libraries + +Bulletproofs as published (Bünz et al., 2018) and as implemented in general-purpose libraries (e.g. the Rust `dalek` bulletproofs crate) target a different deployment shape than a Plutus validator. Several choices in this implementation depart from that reference construction deliberately, for reasons specific to this environment: + +**Linear vector opening instead of the recursive inner-product argument (IPA).** The published protocol recursively folds `l`, `r`, and the generator vectors over `log2(n)` rounds to shrink proof size from `O(n)` scalars to `O(log n)` group elements. This implementation stops one step earlier and discloses `l_vec`/`r_vec` directly. General-purpose libraries always implement the full fold because they serve arbitrary transport contexts where every byte of proof data has a cost. A Plutus validator's binding constraint is different: it is CPU/memory execution units, and the IPA fold does not reduce that cost - the folded rounds still sum to `O(n)` scalar multiplications, just spread across `log n` rounds via multi-exponentiation. What the fold buys is smaller *transaction size*, which only becomes the binding constraint once `n` is large enough (roughly 32–64) that disclosed vectors meaningfully inflate a datum or redeemer. Given the fold is also the highest-complexity, highest-bug-risk part of the protocol (recursive generator-vector folding, additional per-round challenges, a larger transcript surface), this implementation defers it until a concrete deployment target's transaction-size needs justify the added complexity, rather than including it unconditionally as reference libraries do. + +**Native BLS12-381 group law throughout, no custom field simulation.** Every point operation in this module goes through `aiken/crypto/bls12_381/g1` and `scalar`, which wrap the audited native Plutus builtins (`bls12_381_g1_add`, `bls12_381_g1_scalar_mul`, `bls12_381_g1_hash_to_group`, and the BLS12-381 scalar-field arithmetic). This is a deliberate departure from an earlier prototype of this same module, which performed coordinate-wise modular arithmetic on raw integers instead of real elliptic-curve operations - a construction that resembled Bulletproofs in field naming but was not cryptographically meaningful. Every group operation in the current implementation is a real, ledger-validated curve operation. + +**Prover and verifier tested together, end-to-end, without external fixtures.** Because Bulletproofs need no trusted setup, this module owns both `generate_proof` and `verify` and tests them as a pair - generate a proof, verify it; generate a proof, tamper with one field, confirm rejection. This differs from this package's own Groth16 verifier, which necessarily tests against externally-generated proof fixtures (from a circuit-specific trusted-setup ceremony this codebase cannot itself perform). It also differs from typical verifier-only implementations that rely on cross-implementation test vectors from a reference library; this implementation establishes internal prover/verifier consistency directly, and treats interoperability testing against an external Bulletproofs implementation (e.g. `dalek`) as future work rather than a requirement for this milestone. + +**A bare `Bool` verification result, not a typed error channel.** A Plutus validator ultimately reduces to accept/reject at the ledger level. `verify` returns `Bool` rather than a `Result<_, Error>`, matching the convention already established by this package's Groth16 verifier rather than introducing a bespoke error taxonomy per proof system. + +**Explicit hardening a mathematical description wouldn't need.** The published protocol and this repository's own protocol design notes (`docs/step-by-step.md`) describe the mathematics of Bulletproofs without specifying deployment-time hardening, since they aren't describing an adversarial on-chain environment. This implementation adds two things a smart-contract deployment needs that a textbook description doesn't: an upper bound on `n` (capped at 64, since `n` drives `O(n)` recursion and execution cost, and an unbounded `n` is an unbounded compute-cost knob for whoever controls the verification key), and a fixed protocol/version tag folded into every hash in the system - both generator derivation and every Fiat–Shamir challenge - so this system's generators and challenges cannot collide with another protocol's even given identical raw input bytes. + +## 6. Security argument + +Soundness does not depend on hiding `l_vec`/`r_vec` - it depends on both vectors being bound to commitments (`A`, `S`) that were fixed *before* the verifier's challenges `y`, `z`, `x` existed. A prover who did not honestly derive `l_vec`/`r_vec` from a genuine bit-decomposition of a value consistent with `V` would need to satisfy both the t-commitment check and the vector-opening check for challenges they could not have predicted at commitment time. The Pedersen-commitment binding property - that `g`, `h`, `g_vec`, `h_vec` have no known discrete-log relationships to one another - makes that negligibly likely (a Schwartz–Zippel argument over the random challenges). This is the identical binding argument the recursive IPA itself relies on for this same pre-compression equation; the fold is a communication optimization applied on top of it, not an additional soundness ingredient. The `verify` function's two checks are, in that sense, the complete soundness argument, not an approximation of one. + +The `u` generator is present in `BulletproofVerificationKey` but unused by `verify` in this milestone. `u` exists specifically to bind the claimed inner product inside the recursive IPA, where `l`/`r` remain hidden from the verifier; since this construction discloses them and the verifier recomputes `t_hat = ⟨l_vec, r_vec⟩` directly, there is nothing left for `u` to bind. It is retained in the key, documented in-code as reserved for a future IPA phase, rather than removed. + +## 7. Testing and verification + +Ten tests exercise the module, alongside the three pre-existing Groth16 tests in the same package: + +| Test | Verifies | +|---|---| +| `setup_smoke` | Generator vectors have the right length and are non-degenerate | +| `range_proof_valid` | A mid-range value verifies | +| `range_proof_valid_zero` | The boundary value `0` verifies | +| `range_proof_valid_max` | The boundary value `2^n - 1` verifies | +| `range_proof_fails_wrong_commitment` | A proof does not verify against a commitment to a different value | +| `range_proof_fails_tampered_tau_x` | Mutating `tau_x` is rejected | +| `range_proof_fails_tampered_l_vec` | Mutating one entry of `l_vec` is rejected | +| `range_proof_fails_wrong_vector_length` | A truncated `l_vec` is rejected | +| `generate_proof_rejects_out_of_range` | The prover's own guard traps for an out-of-range value | +| `range_proof_fails_out_of_range_bypassing_guard` | Verification independently rejects an out-of-range value even if the prover-side guard is bypassed | + +Because this module owns both prover and verifier, every test constructs a real proof in-language and checks it against a real verification run - no hardcoded external fixtures are required, unlike the Groth16 tests in this package, which depend on proofs generated by an external circuit toolchain. + +At `n = 8`, a full `verify` call measures approximately 5.2M memory units and 14.2B CPU units - comfortably within Cardano's per-transaction execution budget. This has not yet been benchmarked at larger `n`; see §8. + +**Implementation note.** During development, an anonymous lambda with a multi-statement body (`fn(b) { expect Some(s) = scalar.new(b); s }`) passed directly to `list.map` was found to crash the Aiken v1.1.21 compiler silently, with no diagnostic output. The identical logic as a named top-level function compiles and runs correctly. Every inline lambda in this module is single-expression; the one case that needed a multi-statement body was extracted into a named helper (`scalar_from_bit`) instead. This is recorded here as a toolchain finding relevant to future work on this and other modules in the package, not a defect in the protocol implementation itself. + +## 8. Known limitations and roadmap + +- **No IPA compression** - proof size is `O(n)` scalars, not `O(log n)` group elements. Deliberate for this milestone (§5); the natural next phase once a deployment target needs larger `n`. +- **Execution-unit cost is unbenchmarked past `n = 8`.** The `max_n = 64` bound limits worst-case cost, but actual figures at `n = 32`/`64` should be measured before either is used in a real deployment. +- **No on-chain entry point yet.** This module covers the cryptographic core; how a validator obtains and trusts a given `V` (datum/redeemer wiring) is separate, follow-on work. +- **No external cryptographic audit.** This implementation has had internal design review and one external review pass; neither is a substitute for a formal audit before any mainnet or high-value use. +- **The deterministic prover is a test fixture, not a production prover.** Aiken has no RNG, so `generate_proof` requires the caller to supply every blinding factor; `generate_proof_deterministic` exists only to make self-contained tests possible and is documented as such. A production integration must source genuine entropy for these values itself. + +## 9. Conclusion + +This module delivers a functional, internally-tested Bulletproofs range-proof verifier and reference prover built on native BLS12-381 group operations. Its departures from the canonical, fully-compressed construction - linear rather than logarithmic proof size, no external interoperability vectors, deferred audit - are documented engineering decisions scoped to this milestone's goal of a sound, tested verifier, with a clear path (IPA folding, execution-unit benchmarking at scale, external audit) to close the remaining distance to a production-grade deployment. diff --git a/zkp/docs/step-by-step.md b/zkp/docs/step-by-step.md index 038aa78..674eb04 100644 --- a/zkp/docs/step-by-step.md +++ b/zkp/docs/step-by-step.md @@ -158,87 +158,130 @@ The verifier checks the validity of the proof using polynomial commitments and p # **Bulletproofs** +This implementation follows the Bünz et al. (2018) Bulletproofs construction for range proofs over a Pedersen commitment, targeting the BLS12-381 curve on Cardano (Plutus V3 / Aiken). It uses the **O(n) disclosed-vectors variant**: the prover sends \( \mathbf{l}, \mathbf{r} \) in the clear rather than folding them via the recursive inner-product argument (IPA), which would reduce proof size to \( O(\log n) \) at the cost of additional implementation complexity. IPA compression is a planned future phase once a deployment target's transaction-size constraints require it. + ## **1. Setup (Public Parameters Generation)** -Bulletproofs do not require a trusted setup, but they do rely on a publicly known set of parameters. +Bulletproofs require no trusted ceremony. All generators are derived deterministically from a public string. -### **Step 1: Define the elliptic curve and generators** -- Choose an elliptic curve \( E \) over a finite field \( \mathbb{F}_q \). -- Select a generator \( G \) of a group of prime order \( p \) on \( E \). -- Define a second independent generator \( H \), which is typically derived from a hash function. +### **Step 1: Derive independent generators** +- Set \( g \) to the BLS12-381 G1 standard generator. +- Derive \( h \) and \( u \) via `hash_to_group` with distinct domain-separation tags under a fixed `protocol_id` string. +- Derive generator vectors \( \mathbf{g}_{vec}[i] \) and \( \mathbf{h}_{vec}[i] \) for \( i \in [0, n) \) via `hash_to_group` with per-index payloads and separate DSTs. No party ever holds a discrete-log relationship between any two generators. -### **Step 2: Commit to the range proof base** -- Define an inner-product argument base \( G_1, G_2, \dots, G_n \) and \( H_1, H_2, \dots, H_n \). -- The generators \( H_i \) are determined using a Fiat-Shamir heuristic to ensure security. +### **Step 2: Precompute generator sums** +- Store \( g_{sum} = \sum_i \mathbf{g}_{vec}[i] \) and \( h_{sum} = \sum_i \mathbf{h}_{vec}[i] \) in the verification key. +- These avoid re-folding \( 2n \) points on every verification call. -### **Step 3: Establish a Pedersen Commitment scheme** -- The commitment scheme is defined as: +### **Step 3: Establish the Pedersen commitment scheme** +- The commitment to a secret value \( v \) with blinding factor \( \gamma \) is: \[ - C = vG + rH + V = g^v \cdot h^\gamma \] - where: - - \( v \) is the secret value to be proven within a range, - - \( r \) is a blinding factor (random scalar), - - \( C \) is the commitment sent to the verifier. +- \( V \) is the only public input the verifier receives about \( v \); the proof never reveals \( v \) or \( \gamma \). + +The verification key is computed once off-chain and embedded as a deployed constant; it must not be recomputed per transaction. --- ## **2. Proof Generation (Prover's Side)** -The prover generates a zero-knowledge proof that a committed value lies within a specific range (e.g., \( [0, 2^n -1] \)) without revealing the actual value. +The prover generates a zero-knowledge proof that the committed value \( v \) lies in \( [0, 2^n) \). + +### **Step 1: Bit-decompose the value** +- Encode \( v \) as an \( n \)-bit vector: \( \mathbf{a}_L[i] = \text{bit } i \text{ of } v \). +- Set \( \mathbf{a}_R = \mathbf{a}_L - \mathbf{1} \) (component-wise). -### **Step 1: Encode the value as binary** -- The value \( v \) is encoded as an \( n \)-bit binary vector \( \mathbf{a}_L \) where: +### **Step 2: Commit to the bit vectors** +- Sample blinding scalars \( \alpha, \rho \) and blinding vectors \( \mathbf{s}_L, \mathbf{s}_R \) (length \( n \)). +- Compute: \[ - v = \sum_{i=0}^{n-1} a_{L,i} ⋅ 2^i + A = h^\alpha \cdot \mathbf{g}_{vec}^{\mathbf{a}_L} \cdot \mathbf{h}_{vec}^{\mathbf{a}_R} + \qquad + S = h^\rho \cdot \mathbf{g}_{vec}^{\mathbf{s}_L} \cdot \mathbf{h}_{vec}^{\mathbf{s}_R} \] -- Construct the complement vector \( \mathbf{a}_R = \mathbf{a}_L - \mathbf{1} \). -### **Step 2: Commit to the bit values** -- Compute the commitments: +### **Step 3: Derive challenges y, z (Fiat–Shamir)** +- Hash the transcript over \( (V, A, S) \) (with \( g, h, u, n \) bound at transcript initialisation) via `blake2b_256`. +- Derive scalar challenges: \[ - A = \langle \mathbf{a}_L, \mathbf{G} \rangle + \langle \mathbf{a}_R, \mathbf{H} \rangle + \alpha G + y = \text{hash\_to\_scalar}(\text{state} \| \texttt{"y"}) + \qquad + z = \text{hash\_to\_scalar}(\text{state} \| \texttt{"z"}) \] + +### **Step 4: Build the linear vector polynomials** +- Define length-\( n \) vectors (index \( i \in [0, n) \)): \[ - S = \langle \mathbf{s}_L, \mathbf{G} \rangle + \langle \mathbf{s}_R, \mathbf{H} \rangle + \beta G + \mathbf{l}_0[i] = a_L[i] - z + \qquad + \mathbf{l}_1[i] = s_L[i] \] - where \( \alpha, \beta \) are random scalars used to ensure zero-knowledge. - -### **Step 3: Generate challenge scalars** -- The verifier sends a challenge \( y, z \) (using the Fiat-Shamir heuristic). -- The prover computes vectors \( \mathbf{l}, \mathbf{r} \) and an inner-product proof. - -### **Step 4: Compute the proof elements** -- Compute the response values using challenge \( x \) (another Fiat-Shamir challenge). -- The prover computes: \[ - T_1 = \langle \mathbf{l}, \mathbf{r} \rangle G + \gamma H + \mathbf{r}_0[i] = y^i \cdot (a_R[i] + z) + z^2 \cdot 2^i + \qquad + \mathbf{r}_1[i] = y^i \cdot s_R[i] \] - and +- The inner product \( t(X) = \langle \mathbf{l}_0 + X\mathbf{l}_1,\; \mathbf{r}_0 + X\mathbf{r}_1 \rangle = t_0 + t_1 X + t_2 X^2 \). +- Compute coefficients: \( t_1 = \langle \mathbf{l}_0, \mathbf{r}_1 \rangle + \langle \mathbf{l}_1, \mathbf{r}_0 \rangle \), \( t_2 = \langle \mathbf{l}_1, \mathbf{r}_1 \rangle \). + +### **Step 5: Commit to the polynomial coefficients** +- Sample blinding scalars \( \tau_1, \tau_2 \). Compute: \[ - T_2 = x^2 \langle \mathbf{l}, \mathbf{r} \rangle G + \delta H + T_1 = g^{t_1} \cdot h^{\tau_1} + \qquad + T_2 = g^{t_2} \cdot h^{\tau_2} \] -- These commitments ensure that the values remain within the specified range. +### **Step 6: Derive challenge x (Fiat–Shamir)** +- Extend the transcript by absorbing \( (T_1, T_2) \); derive: + \[ + x = \text{hash\_to\_scalar}(\text{state} \| \texttt{"x"}) + \] -### **Step 5: Send the proof to the verifier** -The prover sends the commitments and responses, including: -- \( A, S, T_1, T_2 \), -- Inner product proof (which uses a logarithmic number of rounds to verify the computation). +### **Step 7: Evaluate and output the proof** +- Evaluate the polynomial at \( x \): + \[ + \mathbf{l} = \mathbf{l}_0 + x \cdot \mathbf{l}_1 + \qquad + \mathbf{r} = \mathbf{r}_0 + x \cdot \mathbf{r}_1 + \] +- Compute the blinding aggregates: + \[ + \tau_x = z^2 \cdot \gamma + \tau_1 \cdot x + \tau_2 \cdot x^2 + \qquad + \mu = \alpha + \rho \cdot x + \] +- The proof is \( (A, S, T_1, T_2, \tau_x, \mu, \mathbf{l}, \mathbf{r}) \). Proof size is \( O(n) \) scalars (4 group elements + \( 2n + 2 \) scalars). --- ## **3. Verification (Verifier's Side)** -The verifier checks the validity of the proof using the commitments and challenge responses. +The verifier holds only the public inputs: the verification key and the Pedersen commitment \( V \). It never sees \( v \) or \( \gamma \). + +### **Step 1: Recompute challenge scalars** +- Reconstruct the identical Fiat–Shamir transcript from \( (V, A, S, T_1, T_2) \) using the same staged hash construction. Derive \( y, z, x \) as the prover did. +- Reject immediately if \( |\mathbf{l}| \neq n \) or \( |\mathbf{r}| \neq n \), or if \( y = 0 \) (singular case). + +### **Step 2: Recompute derived values** +- Compute \( \hat{t} = \langle \mathbf{l}, \mathbf{r} \rangle \) directly from the disclosed vectors (no trust required). +- Compute the correction term: + \[ + \delta(y, z) = (z - z^2) \cdot \sum_{i=0}^{n-1} y^i \;-\; z^3 \cdot \sum_{i=0}^{n-1} 2^i + \] -### **Step 1: Compute challenge scalars** -- Using Fiat-Shamir heuristic, recompute \( y, z, x \). +### **Step 3: t-commitment check** +Verify that \( \hat{t} \) is consistent with the committed polynomial and the Pedersen commitment \( V \): +\[ +g^{\hat{t}} \cdot h^{\tau_x} \;=\; V^{z^2} \cdot g^{\delta(y,z)} \cdot T_1^x \cdot T_2^{x^2} +\] -### **Step 2: Verify the commitments** -- Check that the linear constraints hold for the committed values. -- Compute the expected inner product values and compare them against the provided proof. +### **Step 4: Vector-opening check** +Verify that \( \mathbf{l}, \mathbf{r} \) are consistent with the commitments \( A, S \). Rescale the \( h \)-generators as \( h'_i = \mathbf{h}_{vec}[i]^{y^{-i}} \) and set \( \mathbf{r}'[i] = \mathbf{r}[i] - z^2 \cdot 2^i \): +\[ +A \cdot S^x \;=\; h^\mu \cdot \mathbf{g}_{vec}^{\mathbf{l}} \cdot (h')^{\mathbf{r}'} \cdot (g_{sum} - h_{sum})^z +\] -### **Step 3: Verify inner product proof** -- Use logarithmic reduction to efficiently check that the inner product argument is valid. +### **Step 5: Accept or reject** +- If both checks hold, accept the proof. +- If either fails, reject. -### **Step 4: Accept or reject** -- If all checks pass, accept the proof. -- Otherwise, reject the proof as invalid. +Both checks together bind the proof to a genuine bit-decomposition of a value consistent with \( V \). A prover who did not honestly decompose a value in \( [0, 2^n) \) cannot satisfy both checks simultaneously for challenges they could not have predicted at commitment time (Schwartz–Zippel, Pedersen binding). From e8e0fa2b7ed0599e1c033ac98f591e2da583d7ad Mon Sep 17 00:00:00 2001 From: samdelaney Date: Wed, 8 Jul 2026 14:30:01 -0700 Subject: [PATCH 4/4] changes & clarifications per review --- zkp/lib/bullet/bullet.ak | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/zkp/lib/bullet/bullet.ak b/zkp/lib/bullet/bullet.ak index 954bf21..494dc3d 100644 --- a/zkp/lib/bullet/bullet.ak +++ b/zkp/lib/bullet/bullet.ak @@ -337,6 +337,10 @@ pub fn verify( } } +/// `u` is intentionally included even though the current two-check verifier +/// does not use it. Binding `u` into every transcript hash ties the challenges +/// to the full protocol identity — a future IPA phase that activates `u` will +/// derive consistent challenges without a breaking change to transcript format. fn transcript_init( vk: BulletproofVerificationKey, v_commit: G1Element, @@ -382,7 +386,7 @@ fn hash_to_scalar(seed: ByteArray) -> scalar.Scalar { fn hash_to_scalar_loop(seed: ByteArray, counter: Int) -> scalar.Scalar { let digest = crypto.blake2b_256( - bytearray.concat(seed, bytearray.from_int_big_endian(counter, 1)), + bytearray.concat(seed, bytearray.from_int_big_endian(counter, 4)), ) when scalar.from_bytearray_big_endian(digest) is { Some(s) -> s @@ -390,6 +394,8 @@ fn hash_to_scalar_loop(seed: ByteArray, counter: Int) -> scalar.Scalar { } } +/// `scalar.scale(base, i)` is exponentiation (`base^i`), not i*base — it +/// produces [1, base, base^2, ...] as required by the Bulletproofs protocol. fn powers_of(base: scalar.Scalar, count: Int) -> List { list.map(list.range(0, count - 1), fn(i) { scalar.scale(base, i) }) }