From fc3597ef6c193c8fea2f1fa86f2a3831a4c1e876 Mon Sep 17 00:00:00 2001 From: logicalmechanism Date: Wed, 10 Jun 2026 12:12:30 -0700 Subject: [PATCH] Add stdlib wrappers for remaining BLS12-381 builtins Complete coverage of the BLS12-381 prelude builtins so protocols no longer need to blend raw builtins with stdlib: - g1.neg / g2.neg: additive inverse of a curve point (previously only inlined inside `sub`). `sub` now reuses `neg`/`add`. - pairing.mul: multiply two `MillerLoopResult` together, aggregating pairings before a final verification (wraps bls12_381_mul_miller_loop_result). Adds property tests: P + (-P) = 0, -P = 0 - P, P - P = 0, and pairing bilinearity (e(P,Q)^2 = e(2P,Q); e(P,Q)*e(P,Q') = e(P, Q+Q')). Co-Authored-By: Claude Opus 4.8 (1M context) --- CHANGELOG.md | 8 ++++++ lib/aiken/crypto/bls12_381/g1.ak | 8 +++++- lib/aiken/crypto/bls12_381/g1.test.ak | 19 ++++++++++++- lib/aiken/crypto/bls12_381/g2.ak | 8 +++++- lib/aiken/crypto/bls12_381/g2.test.ak | 19 ++++++++++++- lib/aiken/crypto/bls12_381/pairing.ak | 18 ++++++++++++- lib/aiken/crypto/bls12_381/pairing.test.ak | 31 +++++++++++++++++++++- 7 files changed, 105 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9433571..a4209ad 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,13 @@ # Changelog +## vNEXT + +### Added + +- New primitives for [`aiken/crypto/bls12_381`](https://aiken-lang.github.io/stdlib/aiken/crypto/bls12_381.html), completing coverage of the BLS12-381 builtins: + - [`g1.neg`](https://aiken-lang.github.io/stdlib/aiken/crypto/bls12_381/g1.html#neg) / [`g2.neg`](https://aiken-lang.github.io/stdlib/aiken/crypto/bls12_381/g2.html#neg): to compute the additive inverse of a curve point. + - [`pairing.mul`](https://aiken-lang.github.io/stdlib/aiken/crypto/bls12_381/pairing.html#mul): to multiply two `MillerLoopResult` together, aggregating pairings before a final verification. + ## v3.1.0 - 2026-04-25 ### Added diff --git a/lib/aiken/crypto/bls12_381/g1.ak b/lib/aiken/crypto/bls12_381/g1.ak index c1416a5..926777f 100644 --- a/lib/aiken/crypto/bls12_381/g1.ak +++ b/lib/aiken/crypto/bls12_381/g1.ak @@ -58,9 +58,15 @@ pub fn add(left, right) { builtin.bls12_381_g1_add(left, right) } +/// Negates a point in the G1 group, returning its additive inverse. +/// That is, `add(point, neg(point))` yields the [`zero`](#zero) point. +pub fn neg(point) { + builtin.bls12_381_g1_neg(point) +} + /// Subtracts one point in the G1 group from another. pub fn sub(left, right) { - builtin.bls12_381_g1_add(left, builtin.bls12_381_g1_neg(right)) + add(left, neg(right)) } /// Exponentiates a point in the G1 group with a `scalar`. diff --git a/lib/aiken/crypto/bls12_381/g1.test.ak b/lib/aiken/crypto/bls12_381/g1.test.ak index c41cca2..0bd5ab9 100644 --- a/lib/aiken/crypto/bls12_381/g1.test.ak +++ b/lib/aiken/crypto/bls12_381/g1.test.ak @@ -1,6 +1,6 @@ use aiken/builtin use aiken/crypto/bls12_381/g1.{ - add, compress, equal, generator, hash_to_group, scale, sub, zero, + add, compress, equal, generator, hash_to_group, neg, scale, sub, zero, } use aiken/crypto/bls12_381/scalar @@ -18,12 +18,29 @@ test equal_1() { equal(generator, generator) } +// ------------------------------------------------------------------------- neg + +test neg_1() { + // A point added to its negation yields the identity (zero) point. + add(generator, neg(generator)) == zero +} + +test neg_2() { + // Negation matches subtraction from the identity (zero) point. + neg(generator) == sub(zero, generator) +} + // ------------------------------------------------------------------------- sub test sub_1() { generator == sub(add(generator, generator), generator) } +test sub_2() { + // A point subtracted from itself yields the identity (zero) point. + sub(generator, generator) == zero +} + // ----------------------------------------------------------------------- scale test scale_1() { diff --git a/lib/aiken/crypto/bls12_381/g2.ak b/lib/aiken/crypto/bls12_381/g2.ak index 197dcaf..1464c3a 100644 --- a/lib/aiken/crypto/bls12_381/g2.ak +++ b/lib/aiken/crypto/bls12_381/g2.ak @@ -66,9 +66,15 @@ pub fn add(left: G2Element, right: G2Element) { builtin.bls12_381_g2_add(left, right) } +/// Negates a point in the G2 group, returning its additive inverse. +/// That is, `add(point, neg(point))` yields the [`zero`](#zero) point. +pub fn neg(point: G2Element) -> G2Element { + builtin.bls12_381_g2_neg(point) +} + /// Subtracts one point in the G2 group from another. pub fn sub(left: G2Element, right: G2Element) { - builtin.bls12_381_g2_add(left, builtin.bls12_381_g2_neg(right)) + add(left, neg(right)) } /// Exponentiates a point in the G2 group with a `scalar`. diff --git a/lib/aiken/crypto/bls12_381/g2.test.ak b/lib/aiken/crypto/bls12_381/g2.test.ak index 8490eec..28e1982 100644 --- a/lib/aiken/crypto/bls12_381/g2.test.ak +++ b/lib/aiken/crypto/bls12_381/g2.test.ak @@ -1,6 +1,6 @@ use aiken/builtin use aiken/crypto/bls12_381/g2.{ - add, compress, equal, generator, hash_to_group, scale, sub, zero, + add, compress, equal, generator, hash_to_group, neg, scale, sub, zero, } use aiken/crypto/bls12_381/scalar @@ -27,12 +27,29 @@ test equal_1() { ) } +// ------------------------------------------------------------------------- neg + +test neg_1() { + // A point added to its negation yields the identity (zero) point. + add(generator, neg(generator)) == zero +} + +test neg_2() { + // Negation matches subtraction from the identity (zero) point. + neg(generator) == sub(zero, generator) +} + // ------------------------------------------------------------------------- sub test sub_1() { generator == sub(add(generator, generator), generator) } +test sub_2() { + // A point subtracted from itself yields the identity (zero) point. + sub(generator, generator) == zero +} + // ----------------------------------------------------------------------- scale test scale_1() { diff --git a/lib/aiken/crypto/bls12_381/pairing.ak b/lib/aiken/crypto/bls12_381/pairing.ak index 01993f4..97d8a68 100644 --- a/lib/aiken/crypto/bls12_381/pairing.ak +++ b/lib/aiken/crypto/bls12_381/pairing.ak @@ -1,10 +1,26 @@ -use aiken/builtin.{bls12_381_final_verify, bls12_381_miller_loop} +use aiken/builtin.{ + bls12_381_final_verify, bls12_381_miller_loop, + bls12_381_mul_miller_loop_result, +} /// Computes a MillerLoop over the elements `q` and `p` pub fn miller_loop(q: G1Element, p: G2Element) -> MillerLoopResult { bls12_381_miller_loop(q, p) } +/// Multiplies two `MillerLoopResult` together. +/// +/// This aggregates several pairings into a single `MillerLoopResult` before a +/// final verification, relying on the bilinearity of the pairing `e`: +/// +/// ```aiken +/// // e(q1, p1) * e(q2, p2) +/// mul(miller_loop(q1, p1), miller_loop(q2, p2)) +/// ``` +pub fn mul(left: MillerLoopResult, right: MillerLoopResult) -> MillerLoopResult { + bls12_381_mul_miller_loop_result(left, right) +} + /// Final exponentiation against two `MillerLoopResult`. /// /// ```aiken diff --git a/lib/aiken/crypto/bls12_381/pairing.test.ak b/lib/aiken/crypto/bls12_381/pairing.test.ak index e8283ff..7b4911c 100644 --- a/lib/aiken/crypto/bls12_381/pairing.test.ak +++ b/lib/aiken/crypto/bls12_381/pairing.test.ak @@ -2,7 +2,7 @@ use aiken/crypto/bitwise.{State} use aiken/crypto/bls12_381.{domain_separation_tag_nul} use aiken/crypto/bls12_381/g1 use aiken/crypto/bls12_381/g2 -use aiken/crypto/bls12_381/pairing.{final_exponentiation, miller_loop} +use aiken/crypto/bls12_381/pairing.{final_exponentiation, miller_loop, mul} use aiken/crypto/bls12_381/scalar.{Scalar} // -------------------------------- simple_miller_loop_with_final_exponentiation @@ -27,3 +27,32 @@ test simple_miller_loop_with_final_exponentiation() { miller_loop(g1.generator, witness), ) } + +// ------------------------------------------------------------------------- mul + +// prove bilinearity via aggregation: e(p, q) * e(p, q) == e(2p, q) +test mul_aggregates_pairings() { + let two: State = scalar.from_int(2) + + let double_generator: G1Element = g1.generator |> g1.scale(two) + + final_exponentiation( + mul( + miller_loop(g1.generator, g2.generator), + miller_loop(g1.generator, g2.generator), + ), + miller_loop(double_generator, g2.generator), + ) +} + +// prove bilinearity in the second argument: e(p, q) * e(p, q') == e(p, q + q') +test mul_bilinear_in_second_argument() { + let p: G1Element = g1.generator + let q: G2Element = g2.generator + let q2: G2Element = #"face" |> g2.hash_to_group(domain_separation_tag_nul) + + final_exponentiation( + mul(miller_loop(p, q), miller_loop(p, q2)), + miller_loop(p, g2.add(q, q2)), + ) +}