Skip to content

Add stdlib wrappers for remaining BLS12-381 builtins#133

Merged
KtorZ merged 1 commit into
aiken-lang:mainfrom
logicalmechanism:feat/bls12_381-feature-complete
Jun 10, 2026
Merged

Add stdlib wrappers for remaining BLS12-381 builtins#133
KtorZ merged 1 commit into
aiken-lang:mainfrom
logicalmechanism:feat/bls12_381-feature-complete

Conversation

@logicalmechanism

Copy link
Copy Markdown
Contributor

What & why

This fills the last gaps in aiken/crypto/bls12_381 so that every BLS12-381 prelude builtin has a stdlib wrapper. Protocols building on pairings no longer have to blend raw builtin.bls12_381_* calls with the stdlib API.

Mapping all 17 BLS12-381 builtins to wrappers, three were missing:

Builtin Wrapper Before
bls12_381_g1_neg g1.neg only inlined inside g1.sub
bls12_381_g2_neg g2.neg only inlined inside g2.sub
bls12_381_mul_miller_loop_result pairing.mul no wrapper at all

All other builtins (add, scalar_mulscale, equal, compress, uncompress/decompress, hash_to_group, miller_loop, final_verifyfinal_exponentiation) were already wrapped.

Changes

  • g1.neg / g2.neg — additive inverse of a curve point, following each module's existing style (g1 untyped params, g2 typed). sub now reuses neg/add instead of calling the builtins directly.
  • pairing.mul — multiplies two MillerLoopResult, aggregating pairings into one result before a single final verification (leveraging bilinearity e(q1,p1)·e(q2,p2)).
  • Tests — added property tests:
    • g1/g2: P + (−P) = 0, −P = 0 − P, P − P = 0
    • pairing: e(P,Q)² = e(2P,Q) and e(P,Q)·e(P,Q′) = e(P, Q+Q′)
  • CHANGELOGvNEXT entry.

Verification

  • aiken check — green, 0 failures.
  • aiken fmt --check — clean.

🤖 Generated with Claude Code

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) <noreply@anthropic.com>
@KtorZ KtorZ merged commit 41f3c82 into aiken-lang:main Jun 10, 2026
10 of 11 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants