Add keccak256, Secp256k1{Sign, Verify, PubKey} builtins (#3417)

Author: janmasrovira

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -109,6 +109,55 @@ checkAnomaByteArrayFromAnomaContents f = do
     (ftype === (nat_ --> nat_ --> byteArray))
     $ builtinsErrorText l "fromAnomaContents must be of type Nat -> Nat -> ByteArray"
 
+checkSecp256k1SignCompact ::
+  (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) =>
+  AxiomDef ->
+  Sem r ()
+checkSecp256k1SignCompact f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype `hasArguments` [nat_, nat_])
+    $ builtinsErrorText l (prettyText BuiltinAnomaSecp256k1SignCompact <> " must be of type Nat -> Nat -> _")
+
+checkSecp256k1PubKey ::
+  (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) =>
+  AxiomDef ->
+  Sem r ()
+checkSecp256k1PubKey f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype === (nat_ --> nat_))
+    $ builtinsErrorText l (prettyText BuiltinAnomaSecp256k1PubKey <> " must be of type Nat -> Nat")
+
+checkSecp256k1Verify ::
+  (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) =>
+  AxiomDef ->
+  Sem r ()
+checkSecp256k1Verify f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  bool_ <- getBuiltinNameScoper l BuiltinBool
+  unless
+    (ftype === (nat_ --> nat_ --> nat_ --> bool_))
+    $ builtinsErrorText l (prettyText BuiltinAnomaSecp256k1Verify <> " must be of type (msg signature pubKey : Nat) -> Bool")
+
+checkKeccak256 ::
+  (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) =>
+  AxiomDef ->
+  Sem r ()
+checkKeccak256 f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless
+    (ftype === (nat_ --> nat_))
+    $ builtinsErrorText l (prettyText BuiltinAnomaKeccak256 <> " must be of type Nat -> Nat")
+
 checkAnomaSha256 :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
 checkAnomaSha256 f = do
   let ftype = f ^. axiomType

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -332,6 +332,10 @@ data BuiltinAxiom
   | BuiltinByteArrayLength
   | BuiltinRangeCheck
   | BuiltinNockmaReify
+  | BuiltinAnomaKeccak256
+  | BuiltinAnomaSecp256k1SignCompact
+  | BuiltinAnomaSecp256k1Verify
+  | BuiltinAnomaSecp256k1PubKey
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance HasNameKind BuiltinAxiom where
@@ -405,6 +409,11 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaSetFromList -> KNameFunction
     BuiltinRangeCheck -> KNameFunction
     BuiltinNockmaReify -> KNameFunction
+    BuiltinAnomaKeccak256 -> KNameFunction
+    BuiltinAnomaSecp256k1SignCompact -> KNameFunction
+    BuiltinAnomaSecp256k1Verify -> KNameFunction
+    BuiltinAnomaSecp256k1PubKey -> KNameFunction
+
   getNameKindPretty :: BuiltinAxiom -> NameKind
   getNameKindPretty = getNameKind
 
@@ -485,6 +494,10 @@ instance Pretty BuiltinAxiom where
     BuiltinByteArrayLength -> Str.byteArrayLength
     BuiltinRangeCheck -> Str.rangeCheck
     BuiltinNockmaReify -> Str.nockmaReify
+    BuiltinAnomaKeccak256 -> Str.keccak256
+    BuiltinAnomaSecp256k1SignCompact -> Str.secp256k1SignCompact
+    BuiltinAnomaSecp256k1Verify -> Str.secp256k1Verify
+    BuiltinAnomaSecp256k1PubKey -> Str.secp256k1PubKey
 
 data BuiltinType
   = BuiltinTypeInductive BuiltinInductive

src/Juvix/Compiler/Core/Evaluator.hs

@@ -257,6 +257,10 @@ geval opts herr tab env0 = eval' env0
       OpUInt8FromInt -> uint8FromIntOp
       OpByteArrayFromListByte -> byteArrayFromListByteOp
       OpByteArrayLength -> byteArrayLengthOp
+      OpAnomaKeccak256 -> normalizeOrUnsupported opcode
+      OpAnomaSecp256k1SignCompact -> normalizeOrUnsupported opcode
+      OpAnomaSecp256k1Verify -> normalizeOrUnsupported opcode
+      OpAnomaSecp256k1PubKey -> normalizeOrUnsupported opcode
       where
         err :: Text -> a
         err msg = evalError msg n

src/Juvix/Compiler/Core/Extra/Base.hs

@@ -56,14 +56,17 @@ mkConstr' = mkConstr Info.empty
 mkLambda :: Info -> Binder -> Node -> Node
 mkLambda i bi b = NLam (Lambda i bi b)
 
+-- TODO use this in Core/Translation/FromInternal.hs
+
 -- | If b is a builtin with arguments ty1 ty2
 -- it returns: `\lambda (x1 : ty1) (x2 : ty2) := b x1 x2`
-mkBuiltinExpanded' :: [Type] -> BuiltinOp -> Node
-mkBuiltinExpanded' argTys b =
+mkBuiltinExpanded' :: BuiltinOp -> [Type] -> Node
+mkBuiltinExpanded' b argTys =
   let numArgs = length argTys
-      app = mkBuiltinApp' b [mkVar' argIx | argIx <- reverse [0 .. numArgs - 1]]
+      prefixTypes = length (takeWhile isUniverse argTys)
+      app = mkBuiltinApp' b [mkVar' argIx | argIx <- reverse [0 .. numArgs - 1 - prefixTypes]]
    in if
-          | builtinOpArgsNum b == numArgs -> mkLambdas' argTys app
+          | builtinOpArgsNum b == numArgs - prefixTypes -> mkLambdas' argTys app
           | otherwise ->
               impossibleError
                 ( "unexpected number of args to builtin "

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -265,6 +265,10 @@ isDebugOp = \case
       OpIntSub -> False
       OpFieldToInt -> False
       OpShow -> False
+      OpAnomaKeccak256 -> False
+      OpAnomaSecp256k1SignCompact -> False
+      OpAnomaSecp256k1Verify -> False
+      OpAnomaSecp256k1PubKey -> False
   _ -> False
 
 -- | Check if the node contains `trace`, `fail` or `seq` (`>->`).
@@ -557,6 +561,10 @@ builtinOpArgTypes = \case
   OpUInt8FromInt -> [mkTypeInteger']
   OpByteArrayFromListByte -> [mkDynamic']
   OpByteArrayLength -> [mkTypeByteArray']
+  OpAnomaKeccak256 -> [mkTypeInteger']
+  OpAnomaSecp256k1PubKey -> [mkTypeInteger']
+  OpAnomaSecp256k1SignCompact -> [mkTypeInteger', mkTypeInteger']
+  OpAnomaSecp256k1Verify -> [mkTypeInteger', mkTypeInteger', mkTypeInteger']
 
 translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a
 translateCase translateIfFun dflt Case {..} = case _caseBranches of

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -77,6 +77,10 @@ builtinCategory = \case
   OpUInt8FromInt -> BuiltinCategoryUInt8
   OpByteArrayFromListByte -> BuiltinCategoryByteArray
   OpByteArrayLength -> BuiltinCategoryByteArray
+  OpAnomaKeccak256 -> BuiltinCategoryAnoma
+  OpAnomaSecp256k1SignCompact -> BuiltinCategoryAnoma
+  OpAnomaSecp256k1Verify -> BuiltinCategoryAnoma
+  OpAnomaSecp256k1PubKey -> BuiltinCategoryAnoma
 
 -- | Builtin operations which the evaluator and the code generator treat
 -- specially and non-uniformly.
@@ -133,6 +137,10 @@ data BuiltinOp
   | OpAnomaActionCreate
   | OpAnomaSetToList
   | OpAnomaSetFromList
+  | OpAnomaKeccak256
+  | OpAnomaSecp256k1SignCompact
+  | OpAnomaSecp256k1Verify
+  | OpAnomaSecp256k1PubKey
   | OpNockmaReify
   | OpPoseidonHash
   | OpEc
@@ -239,6 +247,10 @@ builtinOpArgsNum = \case
   OpAnomaProveDelta -> 1
   OpAnomaSetToList -> 1
   OpAnomaSetFromList -> 1
+  OpAnomaKeccak256 -> 1
+  OpAnomaSecp256k1PubKey -> 1
+  OpAnomaSecp256k1SignCompact -> 2
+  OpAnomaSecp256k1Verify -> 3
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -325,6 +337,10 @@ builtinIsFoldable = \case
   OpUInt8FromInt -> True
   OpByteArrayFromListByte -> False
   OpByteArrayLength -> False
+  OpAnomaKeccak256 -> False
+  OpAnomaSecp256k1SignCompact -> False
+  OpAnomaSecp256k1Verify -> False
+  OpAnomaSecp256k1PubKey -> False
 
 builtinsInCategory :: BuiltinCategory -> [BuiltinOp]
 builtinsInCategory c = filter ((== c) . builtinCategory) allElements

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -32,67 +32,71 @@ class PrettyCode c where
   ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)
 
 instance PrettyCode BuiltinOp where
-  ppCode = \case
-    OpIntAdd -> return primPlus
-    OpIntSub -> return primMinus
-    OpIntMul -> return primMul
-    OpIntDiv -> return primDiv
-    OpIntMod -> return primMod
-    OpIntLt -> return primLess
-    OpIntLe -> return primLessEquals
-    OpFieldAdd -> return primFieldAdd
-    OpFieldSub -> return primFieldSub
-    OpFieldMul -> return primFieldMul
-    OpFieldDiv -> return primFieldDiv
-    OpFieldFromInt -> return primFieldFromInt
-    OpFieldToInt -> return primFieldToInt
-    OpEq -> return primEquals
-    OpShow -> return primShow
-    OpStrConcat -> return primStrConcat
-    OpStrToInt -> return primStrToInt
-    OpAssert -> return primAssert
-    OpRangeCheck -> return primRangeCheck
-    OpSeq -> return primSeq
-    OpTrace -> return primTrace
-    OpFail -> return primFail
-    OpAnomaGet -> return primAnomaGet
-    OpAnomaEncode -> return primAnomaEncode
-    OpAnomaDecode -> return primAnomaDecode
-    OpAnomaVerifyDetached -> return primAnomaVerifyDetached
-    OpAnomaSign -> return primAnomaSign
-    OpAnomaSignDetached -> return primAnomaSignDetached
-    OpAnomaVerifyWithMessage -> return primAnomaVerifyWithMessage
-    OpAnomaByteArrayToAnomaContents -> return primAnomaByteArrayToAnomaContents
-    OpAnomaByteArrayFromAnomaContents -> return primAnomaByteArrayFromAnomaContents
-    OpAnomaSha256 -> return primAnomaSha256
-    OpAnomaResourceCommitment -> return primResourceCommitment
-    OpAnomaResourceNullifier -> return primResourceNullifier
-    OpAnomaResourceKind -> return primResourceKind
-    OpAnomaResourceDelta -> return primResourceDelta
-    OpAnomaActionDelta -> return primActionDelta
-    OpAnomaActionsDelta -> return primActionsDelta
-    OpAnomaZeroDelta -> return primZeroDelta
-    OpAnomaAddDelta -> return primAddDelta
-    OpAnomaSubDelta -> return primSubDelta
-    OpAnomaRandomGeneratorInit -> return primRandomGeneratorInit
-    OpAnomaRandomNextBytes -> return primRandomNextBytes
-    OpAnomaRandomSplit -> return primRandomSplit
-    OpAnomaIsCommitment -> return primIsCommitment
-    OpAnomaIsNullifier -> return primIsNullifier
-    OpAnomaCreateFromComplianceInputs -> return primAnomaCreateFromComplianceInputs
-    OpAnomaProveDelta -> return primAnomaProveDelta
-    OpAnomaActionCreate -> return primActionCreate
-    OpAnomaTransactionCompose -> return primTransactionCompose
-    OpAnomaSetToList -> return primAnomaSetToList
-    OpAnomaSetFromList -> return primAnomaSetFromList
-    OpNockmaReify -> return primNockmaReify
-    OpPoseidonHash -> return primPoseidonHash
-    OpEc -> return primEc
-    OpRandomEcPoint -> return primRandomEcPoint
-    OpUInt8ToInt -> return primUInt8ToInt
-    OpUInt8FromInt -> return primFieldFromInt
-    OpByteArrayFromListByte -> return primByteArrayFromListByte
-    OpByteArrayLength -> return primByteArrayLength
+  ppCode p = return $ case p of
+    OpIntAdd -> primPlus
+    OpIntSub -> primMinus
+    OpIntMul -> primMul
+    OpIntDiv -> primDiv
+    OpIntMod -> primMod
+    OpIntLt -> primLess
+    OpIntLe -> primLessEquals
+    OpFieldAdd -> primFieldAdd
+    OpFieldSub -> primFieldSub
+    OpFieldMul -> primFieldMul
+    OpFieldDiv -> primFieldDiv
+    OpFieldFromInt -> primFieldFromInt
+    OpFieldToInt -> primFieldToInt
+    OpEq -> primEquals
+    OpShow -> primShow
+    OpStrConcat -> primStrConcat
+    OpStrToInt -> primStrToInt
+    OpAssert -> primAssert
+    OpRangeCheck -> primRangeCheck
+    OpSeq -> primSeq
+    OpTrace -> primTrace
+    OpFail -> primFail
+    OpAnomaGet -> primAnomaGet
+    OpAnomaEncode -> primAnomaEncode
+    OpAnomaDecode -> primAnomaDecode
+    OpAnomaVerifyDetached -> primAnomaVerifyDetached
+    OpAnomaSign -> primAnomaSign
+    OpAnomaSignDetached -> primAnomaSignDetached
+    OpAnomaVerifyWithMessage -> primAnomaVerifyWithMessage
+    OpAnomaByteArrayToAnomaContents -> primAnomaByteArrayToAnomaContents
+    OpAnomaByteArrayFromAnomaContents -> primAnomaByteArrayFromAnomaContents
+    OpAnomaSha256 -> primAnomaSha256
+    OpAnomaResourceCommitment -> primResourceCommitment
+    OpAnomaResourceNullifier -> primResourceNullifier
+    OpAnomaResourceKind -> primResourceKind
+    OpAnomaResourceDelta -> primResourceDelta
+    OpAnomaActionDelta -> primActionDelta
+    OpAnomaActionsDelta -> primActionsDelta
+    OpAnomaZeroDelta -> primZeroDelta
+    OpAnomaAddDelta -> primAddDelta
+    OpAnomaSubDelta -> primSubDelta
+    OpAnomaRandomGeneratorInit -> primRandomGeneratorInit
+    OpAnomaRandomNextBytes -> primRandomNextBytes
+    OpAnomaRandomSplit -> primRandomSplit
+    OpAnomaIsCommitment -> primIsCommitment
+    OpAnomaIsNullifier -> primIsNullifier
+    OpAnomaCreateFromComplianceInputs -> primAnomaCreateFromComplianceInputs
+    OpAnomaProveDelta -> primAnomaProveDelta
+    OpAnomaActionCreate -> primActionCreate
+    OpAnomaTransactionCompose -> primTransactionCompose
+    OpAnomaSetToList -> primAnomaSetToList
+    OpAnomaSetFromList -> primAnomaSetFromList
+    OpNockmaReify -> primNockmaReify
+    OpPoseidonHash -> primPoseidonHash
+    OpEc -> primEc
+    OpRandomEcPoint -> primRandomEcPoint
+    OpUInt8ToInt -> primUInt8ToInt
+    OpUInt8FromInt -> primFieldFromInt
+    OpByteArrayFromListByte -> primByteArrayFromListByte
+    OpByteArrayLength -> primByteArrayLength
+    OpAnomaKeccak256 -> Str.keccak256
+    OpAnomaSecp256k1SignCompact -> primitive Str.secp256k1SignCompact
+    OpAnomaSecp256k1Verify -> primitive Str.secp256k1Verify
+    OpAnomaSecp256k1PubKey -> primitive Str.secp256k1PubKey
 
 instance PrettyCode BuiltinDataTag where
   ppCode = \case

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -124,6 +124,10 @@ computeNodeTypeInfo md = umapL go
           OpUInt8FromInt -> mkTypeUInt8'
           OpByteArrayFromListByte -> mkDynamic'
           OpByteArrayLength -> mkTypeInteger'
+          OpAnomaKeccak256 -> Info.getNodeType node
+          OpAnomaSecp256k1SignCompact -> Info.getNodeType node
+          OpAnomaSecp256k1Verify -> Info.getNodeType node
+          OpAnomaSecp256k1PubKey -> Info.getNodeType node
       NCtr Constr {..} ->
         let ci = lookupConstructorInfo md _constrTag
             ii = lookupInductiveInfo md (ci ^. constructorInductive)

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -729,6 +729,10 @@ builtinInductive a =
         Internal.BuiltinByteArrayLength -> Nothing
         Internal.BuiltinRangeCheck -> Nothing
         Internal.BuiltinNockmaReify -> Nothing
+        Internal.BuiltinAnomaKeccak256 -> Nothing
+        Internal.BuiltinAnomaSecp256k1SignCompact -> Nothing
+        Internal.BuiltinAnomaSecp256k1Verify -> Nothing
+        Internal.BuiltinAnomaSecp256k1PubKey -> Nothing
   where
     registerInductiveAxiom :: forall r. (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader InternalTyped.InfoTable, NameIdGen, Error BadScope] r) => Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
     registerInductiveAxiom ax ctrs = do
@@ -951,6 +955,21 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               natType
               (mkBuiltinApp' OpAnomaSha256 [mkVar' 0])
           )
+      Internal.BuiltinAnomaSecp256k1PubKey -> do
+        natType <- getNatType
+        registerAxiomDef
+          (mkBuiltinExpanded' OpAnomaSecp256k1PubKey [natType])
+      Internal.BuiltinAnomaSecp256k1Verify -> do
+        natType <- getNatType
+        registerAxiomDef
+          (mkBuiltinExpanded' OpAnomaSecp256k1Verify [natType, natType, natType])
+      Internal.BuiltinAnomaSecp256k1SignCompact -> do
+        natType <- getNatType
+        registerAxiomDef
+          (mkBuiltinExpanded' OpAnomaSecp256k1SignCompact [natType, natType])
+      Internal.BuiltinAnomaKeccak256 -> do
+        natType <- getNatType
+        registerAxiomDef (mkBuiltinExpanded' OpAnomaKeccak256 [natType])
       Internal.BuiltinAnomaDelta -> return ()
       Internal.BuiltinAnomaKind -> return ()
       Internal.BuiltinAnomaResourceCommitment -> do
@@ -1585,6 +1604,10 @@ goApplication a = do
           Internal.BuiltinByteArray -> app
           Internal.BuiltinByteArrayFromListByte -> app
           Internal.BuiltinByteArrayLength -> app
+          Internal.BuiltinAnomaKeccak256 -> app
+          Internal.BuiltinAnomaSecp256k1PubKey -> app
+          Internal.BuiltinAnomaSecp256k1SignCompact -> app
+          Internal.BuiltinAnomaSecp256k1Verify -> app
     Internal.ExpressionIden (Internal.IdenFunction n) -> do
       funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
       case funInfoBuiltin of

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -176,6 +176,10 @@ fromCore' tab =
         BuiltinByteArrayFromListByte -> False
         BuiltinByteArrayLength -> False
         BuiltinRangeCheck -> False
+        BuiltinAnomaKeccak256 -> False
+        BuiltinAnomaSecp256k1PubKey -> False
+        BuiltinAnomaSecp256k1Verify -> False
+        BuiltinAnomaSecp256k1SignCompact -> False
       BuiltinTypeInductive i -> case i of
         BuiltinNat -> False
         BuiltinInt -> False