Add stdlib wrappers for remaining BLS12-381 builtins

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

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`.

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() {

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`.

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() {

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

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> = 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)),
+  )
+}