Skip to content

Commit 2544c0c

Browse files
kwxmkwxm
authored
Add BLS12-381 MSM builtins to metatheory (#7339)
1 parent 30e8304 commit 2544c0c

File tree

25 files changed

+4043
-1854
lines changed

25 files changed

+4043
-1854
lines changed

‎plutus-metatheory/src/Algorithmic/CEK.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -350,6 +350,8 @@ BUILTIN expModInteger (base $ V-con b $ V-con e $ V-con m) with expModINTEGER b
350350
... | just r = inj₂ (V-con r)
351351
... | nothing = inj₁ (con (ne (^ (atomic aInteger))))
352352
BUILTIN dropList (Λ̂ A $ V-con n $ V-con l) = inj₂ (V-con (dropLIST n l))
353+
BUILTIN bls12-381-G1-multiScalarMul (base $ V-con is $ V-con es) = inj₂ (V-con (BLS12-381-G1-multiScalarMul (toList is) (toList es)))
354+
BUILTIN bls12-381-G2-multiScalarMul (base $ V-con is $ V-con es) = inj₂ (V-con (BLS12-381-G2-multiScalarMul (toList is) (toList es)))
353355
354356
BUILTIN' : ∀ b {A}
355357
→ ∀{tn} → {pt : tn ∔ 0 ≣ fv (signature b)}

‎plutus-metatheory/src/Builtin.lagda.md‎

Lines changed: 72 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ data Builtin : Set where
118118
mkPairData : Builtin
119119
mkNilData : Builtin
120120
mkNilPairData : Builtin
121-
-- BLS12_381
121+
-- Initial BLS12-381 operations
122122
-- G1
123123
bls12-381-G1-add : Builtin
124124
bls12-381-G1-neg : Builtin
@@ -162,6 +162,10 @@ data Builtin : Set where
162162
expModInteger : Builtin
163163
-- DropList
164164
dropList : Builtin
165+
-- BLS12-381 multi-scalar-multiplication
166+
bls12-381-G1-multiScalarMul : Builtin
167+
bls12-381-G2-multiScalarMul : Builtin
168+
165169
```
166170

167171
## Signatures
@@ -350,6 +354,8 @@ sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
350354
signature findFirstSetBit = ∙ [ bytestring ↑ ]⟶ integer ↑
351355
signature expModInteger = ∙ [ integer ↑ , integer ↑ , integer ↑ ]⟶ integer ↑
352356
signature dropList = ∀a [ integer ↑ , list a ]⟶ list a
357+
signature bls12-381-G1-multiScalarMul = ∙ [ list integer , list bls12-381-g1-element ]⟶ bls12-381-g1-element ↑
358+
signature bls12-381-G2-multiScalarMul = ∙ [ list integer , list bls12-381-g2-element ]⟶ bls12-381-g2-element ↑
353359
354360
open SugaredSignature using (signature) public
355361
@@ -462,6 +468,8 @@ Each Agda built-in name must be mapped to a Haskell name.
462468
| Ripemd_160
463469
| ExpModInteger
464470
| DropList
471+
| Bls12_381_G1_multiScalarMul
472+
| Bls12_381_G2_multiScalarMul
465473
) #-}
466474
```
467475

@@ -472,64 +480,66 @@ whose semantics are provided by a Haskell function.
472480

473481
```
474482
postulate
475-
lengthBS : ByteString → Int
476-
index : ByteString → Int → Int
477-
div : Int → Int → Int
478-
quot : Int → Int → Int
479-
rem : Int → Int → Int
480-
mod : Int → Int → Int
481-
482-
TRACE : {a : Set} → String → a → a
483-
484-
concat : ByteString → ByteString → ByteString
485-
cons : Int → ByteString → Maybe ByteString
486-
slice : Int → Int → ByteString → ByteString
487-
B< : ByteString → ByteString → Bool
488-
B<= : ByteString → ByteString → Bool
489-
SHA2-256 : ByteString → ByteString
490-
SHA3-256 : ByteString → ByteString
491-
BLAKE2B-256 : ByteString → ByteString
492-
verifyEd25519Sig : ByteString → ByteString → ByteString → Maybe Bool
493-
verifyEcdsaSecp256k1Sig : ByteString → ByteString → ByteString → Maybe Bool
494-
verifySchnorrSecp256k1Sig : ByteString → ByteString → ByteString → Maybe Bool
495-
equals : ByteString → ByteString → Bool
496-
ENCODEUTF8 : String → ByteString
497-
DECODEUTF8 : ByteString → Maybe String
498-
serialiseDATA : DATA → ByteString
499-
BLS12-381-G1-add : Bls12-381-G1-Element → Bls12-381-G1-Element → Bls12-381-G1-Element
500-
BLS12-381-G1-neg : Bls12-381-G1-Element → Bls12-381-G1-Element
501-
BLS12-381-G1-scalarMul : Int → Bls12-381-G1-Element → Bls12-381-G1-Element
502-
BLS12-381-G1-equal : Bls12-381-G1-Element → Bls12-381-G1-Element → Bool
503-
BLS12-381-G1-hashToGroup : ByteString → ByteString → Maybe Bls12-381-G1-Element
504-
BLS12-381-G1-compress : Bls12-381-G1-Element → ByteString
505-
BLS12-381-G1-uncompress : ByteString → Maybe Bls12-381-G1-Element -- FIXME: this really returns Either BLSTError Element
506-
BLS12-381-G2-add : Bls12-381-G2-Element → Bls12-381-G2-Element → Bls12-381-G2-Element
507-
BLS12-381-G2-neg : Bls12-381-G2-Element → Bls12-381-G2-Element
508-
BLS12-381-G2-scalarMul : Int → Bls12-381-G2-Element → Bls12-381-G2-Element
509-
BLS12-381-G2-equal : Bls12-381-G2-Element → Bls12-381-G2-Element → Bool
510-
BLS12-381-G2-hashToGroup : ByteString → ByteString → Maybe Bls12-381-G2-Element
511-
BLS12-381-G2-compress : Bls12-381-G2-Element → ByteString
512-
BLS12-381-G2-uncompress : ByteString → Maybe Bls12-381-G2-Element -- FIXME: this really returns Either BLSTError Element
513-
BLS12-381-millerLoop : Bls12-381-G1-Element → Bls12-381-G2-Element → Bls12-381-MlResult
514-
BLS12-381-mulMlResult : Bls12-381-MlResult → Bls12-381-MlResult → Bls12-381-MlResult
515-
BLS12-381-finalVerify : Bls12-381-MlResult → Bls12-381-MlResult → Bool
516-
KECCAK-256 : ByteString → ByteString
517-
BLAKE2B-224 : ByteString → ByteString
518-
BStoI : Bool -> ByteString -> Int
519-
ItoBS : Bool -> Int -> Int -> Maybe ByteString
520-
andBYTESTRING : Bool -> ByteString -> ByteString -> ByteString
521-
orBYTESTRING : Bool -> ByteString -> ByteString -> ByteString
522-
xorBYTESTRING : Bool -> ByteString -> ByteString -> ByteString
523-
complementBYTESTRING : ByteString -> ByteString
524-
readBIT : ByteString -> Int -> Maybe Bool
525-
writeBITS : ByteString -> List Int -> Bool -> Maybe ByteString
526-
replicateBYTE : Int -> Int -> Maybe ByteString
527-
shiftBYTESTRING : ByteString -> Int -> ByteString
528-
rotateBYTESTRING : ByteString -> Int -> ByteString
529-
countSetBITS : ByteString -> Int
530-
findFirstSetBIT : ByteString -> Int
531-
RIPEMD-160 : ByteString → ByteString
532-
expModINTEGER : Int -> Int -> Int -> Maybe Int
483+
lengthBS : ByteString → Int
484+
index : ByteString → Int → Int
485+
div : Int → Int → Int
486+
quot : Int → Int → Int
487+
rem : Int → Int → Int
488+
mod : Int → Int → Int
489+
490+
TRACE : {a : Set} → String → a → a
491+
492+
concat : ByteString → ByteString → ByteString
493+
cons : Int → ByteString → Maybe ByteString
494+
slice : Int → Int → ByteString → ByteString
495+
B< : ByteString → ByteString → Bool
496+
B<= : ByteString → ByteString → Bool
497+
SHA2-256 : ByteString → ByteString
498+
SHA3-256 : ByteString → ByteString
499+
BLAKE2B-256 : ByteString → ByteString
500+
verifyEd25519Sig : ByteString → ByteString → ByteString → Maybe Bool
501+
verifyEcdsaSecp256k1Sig : ByteString → ByteString → ByteString → Maybe Bool
502+
verifySchnorrSecp256k1Sig : ByteString → ByteString → ByteString → Maybe Bool
503+
equals : ByteString → ByteString → Bool
504+
ENCODEUTF8 : String → ByteString
505+
DECODEUTF8 : ByteString → Maybe String
506+
serialiseDATA : DATA → ByteString
507+
BLS12-381-G1-add : Bls12-381-G1-Element → Bls12-381-G1-Element → Bls12-381-G1-Element
508+
BLS12-381-G1-neg : Bls12-381-G1-Element → Bls12-381-G1-Element
509+
BLS12-381-G1-scalarMul : Int → Bls12-381-G1-Element → Bls12-381-G1-Element
510+
BLS12-381-G1-equal : Bls12-381-G1-Element → Bls12-381-G1-Element → Bool
511+
BLS12-381-G1-hashToGroup : ByteString → ByteString → Maybe Bls12-381-G1-Element
512+
BLS12-381-G1-compress : Bls12-381-G1-Element → ByteString
513+
BLS12-381-G1-uncompress : ByteString → Maybe Bls12-381-G1-Element -- FIXME: this really returns Either BLSTError Element
514+
BLS12-381-G2-add : Bls12-381-G2-Element → Bls12-381-G2-Element → Bls12-381-G2-Element
515+
BLS12-381-G2-neg : Bls12-381-G2-Element → Bls12-381-G2-Element
516+
BLS12-381-G2-scalarMul : Int → Bls12-381-G2-Element → Bls12-381-G2-Element
517+
BLS12-381-G2-equal : Bls12-381-G2-Element → Bls12-381-G2-Element → Bool
518+
BLS12-381-G2-hashToGroup : ByteString → ByteString → Maybe Bls12-381-G2-Element
519+
BLS12-381-G2-compress : Bls12-381-G2-Element → ByteString
520+
BLS12-381-G2-uncompress : ByteString → Maybe Bls12-381-G2-Element -- FIXME: this really returns Either BLSTError Element
521+
BLS12-381-millerLoop : Bls12-381-G1-Element → Bls12-381-G2-Element → Bls12-381-MlResult
522+
BLS12-381-mulMlResult : Bls12-381-MlResult → Bls12-381-MlResult → Bls12-381-MlResult
523+
BLS12-381-finalVerify : Bls12-381-MlResult → Bls12-381-MlResult → Bool
524+
KECCAK-256 : ByteString → ByteString
525+
BLAKE2B-224 : ByteString → ByteString
526+
BStoI : Bool -> ByteString -> Int
527+
ItoBS : Bool -> Int -> Int -> Maybe ByteString
528+
andBYTESTRING : Bool -> ByteString -> ByteString -> ByteString
529+
orBYTESTRING : Bool -> ByteString -> ByteString -> ByteString
530+
xorBYTESTRING : Bool -> ByteString -> ByteString -> ByteString
531+
complementBYTESTRING : ByteString -> ByteString
532+
readBIT : ByteString -> Int -> Maybe Bool
533+
writeBITS : ByteString -> List Int -> Bool -> Maybe ByteString
534+
replicateBYTE : Int -> Int -> Maybe ByteString
535+
shiftBYTESTRING : ByteString -> Int -> ByteString
536+
rotateBYTESTRING : ByteString -> Int -> ByteString
537+
countSetBITS : ByteString -> Int
538+
findFirstSetBIT : ByteString -> Int
539+
RIPEMD-160 : ByteString → ByteString
540+
expModINTEGER : Int -> Int -> Int -> Maybe Int
541+
BLS12-381-G1-multiScalarMul : List Int → List Bls12-381-G1-Element → Bls12-381-G1-Element
542+
BLS12-381-G2-multiScalarMul : List Int → List Bls12-381-G2-Element → Bls12-381-G2-Element
533543
```
534544

535545
### What builtin operations should be compiled to if we compile to Haskell
@@ -661,6 +671,9 @@ postulate
661671
then Nothing
662672
else fmap fromIntegral $ builtinResultToMaybe $ ExpMod.expMod b e (fromIntegral m) #-}
663673
674+
{-# COMPILE GHC BLS12-381-G1-multiScalarMul = G1.multiScalarMul #-}
675+
{-# COMPILE GHC BLS12-381-G2-multiScalarMul = G2.multiScalarMul #-}
676+
664677
-- no binding needed for appendStr
665678
-- no binding needed for traceStr
666679
-- See Utils.List for the implementation of dropList

0 commit comments

Comments
 (0)