diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index 9f19d6de32..73af0048a9 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -57,3 +57,29 @@ registerAnomaVerifyDetached f = do ((ftype ==% (u <>--> nat --> decodeT --> nat --> bool_)) freeVars) (error "anomaVerifyDetached must be of type {A : Type} -> Nat -> A -> Nat -> Bool") registerBuiltin BuiltinAnomaVerifyDetached (f ^. axiomName) + +registerAnomaSign :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () +registerAnomaSign f = do + let ftype = f ^. axiomType + u = ExpressionUniverse smallUniverseNoLoc + l = getLoc f + dataT <- freshVar l "dataT" + nat <- getBuiltinName (getLoc f) BuiltinNat + let freeVars = HashSet.fromList [dataT] + unless + ((ftype ==% (u <>--> dataT --> nat --> nat)) freeVars) + (error "anomaSign must be of type {A : Type} -> A -> Nat -> Nat") + registerBuiltin BuiltinAnomaSign (f ^. axiomName) + +registerAnomaVerify :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () +registerAnomaVerify f = do + let ftype = f ^. axiomType + u = ExpressionUniverse smallUniverseNoLoc + l = getLoc f + dataT <- freshVar l "dataT" + nat <- getBuiltinName (getLoc f) BuiltinNat + let freeVars = HashSet.fromList [dataT] + unless + ((ftype ==% (u <>--> nat --> nat --> dataT)) freeVars) + (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> A") + registerBuiltin BuiltinAnomaVerify (f ^. axiomName) diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 0bd340c56d..7707853a04 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -191,6 +191,8 @@ data BuiltinAxiom | BuiltinAnomaEncode | BuiltinAnomaDecode | BuiltinAnomaVerifyDetached + | BuiltinAnomaSign + | BuiltinAnomaVerify | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint @@ -229,6 +231,8 @@ instance Pretty BuiltinAxiom where BuiltinAnomaEncode -> Str.anomaEncode BuiltinAnomaDecode -> Str.anomaDecode BuiltinAnomaVerifyDetached -> Str.anomaVerifyDetached + BuiltinAnomaSign -> Str.anomaSign + BuiltinAnomaVerify -> Str.anomaVerify BuiltinPoseidon -> Str.cairoPoseidon BuiltinEcOp -> Str.cairoEcOp BuiltinRandomEcPoint -> Str.cairoRandomEcPoint diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 2a368e177d..e94ac0ab59 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -194,6 +194,8 @@ geval opts herr ctx env0 = eval' env0 OpAnomaEncode -> anomaEncodeOp OpAnomaDecode -> anomaDecodeOp OpAnomaVerifyDetached -> anomaVerifyDetachedOp + OpAnomaSign -> anomaSignOp + OpAnomaVerify -> anomaVerifyOp OpPoseidonHash -> poseidonHashOp OpEc -> ecOp OpRandomEcPoint -> randomEcPointOp @@ -367,6 +369,24 @@ geval opts herr ctx env0 = eval' env0 err "unsupported builtin operation: OpAnomaVerifyDetached" {-# INLINE anomaVerifyDetachedOp #-} + anomaSignOp :: [Node] -> Node + anomaSignOp = checkApply $ \arg1 arg2 -> + if + | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure -> + mkBuiltinApp' OpAnomaSign (eval' env <$> [arg1, arg2]) + | otherwise -> + err "unsupported builtin operation: OpAnomaSign" + {-# INLINE anomaSignOp #-} + + anomaVerifyOp :: [Node] -> Node + anomaVerifyOp = checkApply $ \arg1 arg2 -> + if + | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure -> + mkBuiltinApp' OpAnomaVerify (eval' env <$> [arg1, arg2]) + | otherwise -> + err "unsupported builtin operation: OpAnomaVerify" + {-# INLINE anomaVerifyOp #-} + poseidonHashOp :: [Node] -> Node poseidonHashOp = unary $ \arg -> if diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index 5ace542d78..33fa1f8ffd 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -427,6 +427,8 @@ builtinOpArgTypes = \case OpAnomaEncode -> [mkDynamic'] OpAnomaDecode -> [mkDynamic'] OpAnomaVerifyDetached -> [mkDynamic', mkDynamic', mkDynamic'] + OpAnomaSign -> [mkDynamic', mkDynamic'] + OpAnomaVerify -> [mkDynamic', mkDynamic'] OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] OpRandomEcPoint -> [] diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index cf3a6a46e6..b91a40daf3 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -30,6 +30,8 @@ data BuiltinOp | OpAnomaEncode | OpAnomaDecode | OpAnomaVerifyDetached + | OpAnomaSign + | OpAnomaVerify | OpPoseidonHash | OpEc | OpRandomEcPoint @@ -77,6 +79,8 @@ builtinOpArgsNum = \case OpAnomaEncode -> 1 OpAnomaDecode -> 1 OpAnomaVerifyDetached -> 3 + OpAnomaSign -> 2 + OpAnomaVerify -> 2 OpPoseidonHash -> 1 OpEc -> 3 OpRandomEcPoint -> 0 @@ -117,6 +121,8 @@ builtinIsFoldable = \case OpAnomaEncode -> False OpAnomaDecode -> False OpAnomaVerifyDetached -> False + OpAnomaSign -> False + OpAnomaVerify -> False OpPoseidonHash -> False OpEc -> False OpRandomEcPoint -> False @@ -134,4 +140,11 @@ builtinsCairo :: [BuiltinOp] builtinsCairo = [OpPoseidonHash, OpEc, OpRandomEcPoint] builtinsAnoma :: [BuiltinOp] -builtinsAnoma = [OpAnomaGet, OpAnomaEncode, OpAnomaDecode, OpAnomaVerifyDetached] +builtinsAnoma = + [ OpAnomaGet, + OpAnomaEncode, + OpAnomaDecode, + OpAnomaVerifyDetached, + OpAnomaSign, + OpAnomaVerify + ] diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 40c87ae7ab..e684758d04 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -56,6 +56,8 @@ instance PrettyCode BuiltinOp where OpAnomaEncode -> return primAnomaEncode OpAnomaDecode -> return primAnomaDecode OpAnomaVerifyDetached -> return primAnomaVerifyDetached + OpAnomaSign -> return primAnomaSign + OpAnomaVerify -> return primAnomaVerify OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc OpRandomEcPoint -> return primRandomEcPoint @@ -813,6 +815,12 @@ primAnomaDecode = primitive Str.anomaDecode primAnomaVerifyDetached :: Doc Ann primAnomaVerifyDetached = primitive Str.anomaVerifyDetached +primAnomaSign :: Doc Ann +primAnomaSign = primitive Str.anomaSign + +primAnomaVerify :: Doc Ann +primAnomaVerify = primitive Str.anomaVerify + primPoseidonHash :: Doc Ann primPoseidonHash = primitive Str.cairoPoseidon diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 3611c4b8f0..36b6bc7fc2 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -70,6 +70,8 @@ computeNodeTypeInfo md = umapL go OpAnomaEncode -> Info.getNodeType node OpAnomaDecode -> Info.getNodeType node OpAnomaVerifyDetached -> Info.getNodeType node + OpAnomaSign -> Info.getNodeType node + OpAnomaVerify -> Info.getNodeType node OpPoseidonHash -> case _builtinAppArgs of [arg] -> Info.getNodeType arg _ -> error "incorrect poseidon builtin application" diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 01456d23ee..a4960ceb3b 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -580,6 +580,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinAnomaEncode -> return () Internal.BuiltinAnomaDecode -> return () Internal.BuiltinAnomaVerifyDetached -> return () + Internal.BuiltinAnomaSign -> return () + Internal.BuiltinAnomaVerify -> return () Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () @@ -713,7 +715,6 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) mkSmallUniv (mkLambda' natType (mkBuiltinApp' OpAnomaDecode [mkVar' 0])) ) - -- ((ftype ==% (u <>--> nat --> decodeT --> nat --> bool_)) freeVars) Internal.BuiltinAnomaVerifyDetached -> do natType <- getNatType registerAxiomDef @@ -730,6 +731,32 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) ) ) ) + Internal.BuiltinAnomaSign -> do + natType <- getNatType + registerAxiomDef + ( mkLambda' + mkSmallUniv + ( mkLambda' + (mkVar' 0) + ( mkLambda' + natType + (mkBuiltinApp' OpAnomaSign [mkVar' 1, mkVar' 0]) + ) + ) + ) + Internal.BuiltinAnomaVerify -> do + natType <- getNatType + registerAxiomDef + ( mkLambda' + mkSmallUniv + ( mkLambda' + natType + ( mkLambda' + natType + (mkBuiltinApp' OpAnomaVerify [mkVar' 1, mkVar' 0]) + ) + ) + ) Internal.BuiltinPoseidon -> do psName <- getPoseidonStateName psSym <- getPoseidonStateSymbol @@ -1137,6 +1164,8 @@ goApplication a = do Just Internal.BuiltinAnomaEncode -> app Just Internal.BuiltinAnomaDecode -> app Just Internal.BuiltinAnomaVerifyDetached -> app + Just Internal.BuiltinAnomaSign -> app + Just Internal.BuiltinAnomaVerify -> app Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index b00efebe99..0413bf1783 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -99,6 +99,8 @@ fromCore fsize tab = BuiltinAnomaEncode -> False BuiltinAnomaDecode -> False BuiltinAnomaVerifyDetached -> False + BuiltinAnomaSign -> False + BuiltinAnomaVerify -> False BuiltinPoseidon -> False BuiltinEcOp -> False BuiltinRandomEcPoint -> False diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 2ae85d57eb..228c5a9516 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -572,6 +572,8 @@ registerBuiltinAxiom d = \case BuiltinAnomaEncode -> registerAnomaEncode d BuiltinAnomaDecode -> registerAnomaDecode d BuiltinAnomaVerifyDetached -> registerAnomaVerifyDetached d + BuiltinAnomaSign -> registerAnomaSign d + BuiltinAnomaVerify -> registerAnomaVerify d BuiltinPoseidon -> registerPoseidon d BuiltinEcOp -> registerEcOp d BuiltinRandomEcPoint -> registerRandomEcPoint d diff --git a/src/Juvix/Compiler/Nockma/Encoding/Ed25519.hs b/src/Juvix/Compiler/Nockma/Encoding/Ed25519.hs new file mode 100644 index 0000000000..4497c532e8 --- /dev/null +++ b/src/Juvix/Compiler/Nockma/Encoding/Ed25519.hs @@ -0,0 +1,9 @@ +module Juvix.Compiler.Nockma.Encoding.Ed25519 where + +import Data.ByteString qualified as BS +import Juvix.Prelude.Base + +-- | Remove the Ed25519 signature from a signed message. +-- The signaure of an Ed25519 message is the first 64 bytes of the signed message. +removeSignature :: ByteString -> ByteString +removeSignature = BS.drop 64 diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs index 7a159e4da6..a56382601d 100644 --- a/src/Juvix/Compiler/Nockma/Evaluator.hs +++ b/src/Juvix/Compiler/Nockma/Evaluator.hs @@ -10,6 +10,7 @@ import Crypto.Sign.Ed25519 import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Nockma.Encoding import Juvix.Compiler.Nockma.Encoding qualified as Encoding +import Juvix.Compiler.Nockma.Encoding.Ed25519 import Juvix.Compiler.Nockma.Evaluator.Error import Juvix.Compiler.Nockma.Evaluator.Options import Juvix.Compiler.Nockma.Evaluator.Storage @@ -239,7 +240,13 @@ evalProfile inistack initerm = TermCell {} -> throwDecodingFailed args' DecodingErrorExpectedAtom StdlibVerifyDetached -> case args' of TCell (TermAtom sig) (TCell (TermAtom message) (TermAtom pubKey)) -> goVerifyDetached sig message pubKey - _ -> error "expected a term of the form [signature (atom) message (term) public_key (atom)]" + _ -> error "expected a term of the form [signature (atom) message (encoded term) public_key (atom)]" + StdlibSign -> case args' of + TCell (TermAtom message) (TermAtom privKey) -> goSign message privKey + _ -> error "expected a term of the form [message (encoded term) private_key (atom)]" + StdlibVerify -> case args' of + TCell (TermAtom signedMessage) (TermAtom pubKey) -> goVerify signedMessage pubKey + _ -> error "expected a term of the form [signedMessage (atom) public_key (atom)]" where goVerifyDetached :: Atom a -> Atom a -> Atom a -> Sem r (Term a) goVerifyDetached sigT messageT pubKeyT = do @@ -249,6 +256,21 @@ evalProfile inistack initerm = let res = dverify pubKey message sig return (TermAtom (nockBool res)) + goSign :: Atom a -> Atom a -> Sem r (Term a) + goSign messageT privKeyT = do + privKey <- SecretKey <$> atomToByteString privKeyT + message <- atomToByteString messageT + res <- byteStringToAtom (sign privKey message) + return (TermAtom res) + + goVerify :: Atom a -> Atom a -> Sem r (Term a) + goVerify signedMessageT pubKeyT = do + pubKey <- PublicKey <$> atomToByteString pubKeyT + signedMessage <- atomToByteString signedMessageT + if + | verify pubKey signedMessage -> TermAtom <$> byteStringToAtom (removeSignature signedMessage) + | otherwise -> throwVerificationFailed signedMessageT pubKeyT + goAutoConsCell :: AutoConsCell a -> Sem r (Term a) goAutoConsCell c = do let w a = diff --git a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs index 69b9dca90e..c35c1a15c9 100644 --- a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs +++ b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs @@ -24,6 +24,7 @@ data NockEvalError a ErrAssignmentNotFound Text | ErrKeyNotInStorage (KeyNotInStorage a) | ErrDecodingFailed (DecodingFailed a) + | ErrVerificationFailed (VerificationFailed a) newtype GenericNockEvalError = GenericNockEvalError { _genericNockEvalErrorMessage :: AnsiText @@ -66,6 +67,12 @@ data DecodingFailed a = DecodingFailed _decodingFailedReason :: DecodingError } +data VerificationFailed a = VerificationFailed + { _verificationFailedCtx :: EvalCtx, + _verificationFailedMessage :: Atom a, + _verificationFailedPublicKey :: Atom a + } + throwInvalidNockOp :: (Members '[Error (NockEvalError a), Reader EvalCtx] r) => Atom a -> Sem r x throwInvalidNockOp a = do ctx <- ask @@ -128,6 +135,17 @@ throwDecodingFailed a e = do _decodingFailedReason = e } +throwVerificationFailed :: (Members '[Error (NockEvalError a), Reader EvalCtx] r) => Atom a -> Atom a -> Sem r x +throwVerificationFailed m k = do + ctx <- ask + throw $ + ErrVerificationFailed + VerificationFailed + { _verificationFailedCtx = ctx, + _verificationFailedMessage = m, + _verificationFailedPublicKey = k + } + instance PrettyCode NoStack where ppCode _ = return "Missing stack" @@ -178,6 +196,22 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (DecodingFailed a) where r <- ppCode _decodingFailedReason return (ctx <> "Decoding the term" <+> t <+> "failed with reason:" <> line <> r) +instance (PrettyCode a, NockNatural a) => PrettyCode (VerificationFailed a) where + ppCode VerificationFailed {..} = do + m <- ppCode _verificationFailedMessage + ctx <- ppCtx _verificationFailedCtx + k <- ppCode _verificationFailedPublicKey + return + ( ctx + <> "Signature verification failed for message atom:" + <> line + <> m + <> line + <> "and public key atom:" + <> line + <> k + ) + instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where ppCode = \case ErrInvalidPath e -> ppCode e @@ -188,3 +222,4 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (NockEvalError a) where ErrAssignmentNotFound e -> return (pretty e) ErrKeyNotInStorage e -> ppCode e ErrDecodingFailed e -> ppCode e + ErrVerificationFailed e -> ppCode e diff --git a/src/Juvix/Compiler/Nockma/StdlibFunction.hs b/src/Juvix/Compiler/Nockma/StdlibFunction.hs index 9b56be473f..0f565a9528 100644 --- a/src/Juvix/Compiler/Nockma/StdlibFunction.hs +++ b/src/Juvix/Compiler/Nockma/StdlibFunction.hs @@ -23,3 +23,5 @@ stdlibPath = \case StdlibEncode -> [nock| [9 22 0 3] |] StdlibDecode -> [nock| [9 94 0 3] |] StdlibVerifyDetached -> [nock| [9 22 0 1] |] + StdlibSign -> [nock| [9 10 0 1] |] + StdlibVerify -> [nock| [9 4 0 1] |] diff --git a/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs b/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs index 6d2550fbbe..5ef7130380 100644 --- a/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs +++ b/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs @@ -17,6 +17,8 @@ instance Pretty StdlibFunction where StdlibEncode -> "encode" StdlibDecode -> "decode" StdlibVerifyDetached -> "verify-detached" + StdlibSign -> "sign" + StdlibVerify -> "verify" data StdlibFunction = StdlibDec @@ -31,6 +33,8 @@ data StdlibFunction | StdlibEncode | StdlibDecode | StdlibVerifyDetached + | StdlibSign + | StdlibVerify deriving stock (Show, Lift, Eq, Bounded, Enum, Generic) instance Hashable StdlibFunction diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index 7ffee89737..f69aa54151 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -427,6 +427,8 @@ compile = \case Tree.OpAnomaEncode -> return (goAnomaEncode args) Tree.OpAnomaDecode -> return (goAnomaDecode args) Tree.OpAnomaVerifyDetached -> return (goAnomaVerifyDetached args) + Tree.OpAnomaSign -> return (goAnomaSign args) + Tree.OpAnomaVerify -> return (goAnomaVerify args) goUnop :: Tree.NodeUnop -> Sem r (Term Natural) goUnop Tree.NodeUnop {..} = do @@ -462,6 +464,16 @@ compile = \case [sig, message, pubKey] -> callStdlib StdlibVerifyDetached [sig, goAnomaEncode [message], pubKey] _ -> impossible + goAnomaSign :: [Term Natural] -> Term Natural + goAnomaSign = \case + [message, privKey] -> callStdlib StdlibSign [goAnomaEncode [message], privKey] + _ -> impossible + + goAnomaVerify :: [Term Natural] -> Term Natural + goAnomaVerify = \case + [signedMessage, pubKey] -> callStdlib StdlibDecode [callStdlib StdlibVerify [signedMessage, pubKey]] + _ -> impossible + goTrace :: Term Natural -> Sem r (Term Natural) goTrace arg = do enabled <- asks (^. compilerOptions . compilerOptionsEnableTrace) diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs index a9a8b1fddb..2b37e7a9d8 100644 --- a/src/Juvix/Compiler/Tree/Keywords.hs +++ b/src/Juvix/Compiler/Tree/Keywords.hs @@ -12,6 +12,8 @@ import Juvix.Data.Keyword.All kwAnomaDecode, kwAnomaEncode, kwAnomaGet, + kwAnomaSign, + kwAnomaVerify, kwAnomaVerifyDetached, kwArgsNum, kwAtoi, @@ -80,6 +82,8 @@ allKeywords = kwAnomaDecode, kwAnomaEncode, kwAnomaVerifyDetached, + kwAnomaSign, + kwAnomaVerify, kwPoseidon, kwEcOp, kwRandomEcPoint diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index cd34f19f26..49a1924e36 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -58,4 +58,8 @@ data AnomaOp OpAnomaDecode | -- | Verify a cryptogtaphic signature of an Anoma value OpAnomaVerifyDetached + | -- | Cryptographically sign an Anoma value using a secret key + OpAnomaSign + | -- | Verify a signature obtained from OpAnomaSign using a public key + OpAnomaVerify deriving stock (Eq) diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index 65ba5f9202..1b4e5fcd9b 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -246,6 +246,8 @@ instance PrettyCode AnomaOp where OpAnomaEncode -> Str.anomaEncode OpAnomaDecode -> Str.anomaDecode OpAnomaVerifyDetached -> Str.anomaVerifyDetached + OpAnomaSign -> Str.anomaSign + OpAnomaVerify -> Str.anomaVerify instance PrettyCode UnaryOpcode where ppCode = \case diff --git a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs index a83607b553..92a9a1b88d 100644 --- a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs +++ b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs @@ -15,6 +15,8 @@ checkNoAnoma = walkT checkNode OpAnomaEncode -> unsupportedErr "OpAnomaEncode" OpAnomaDecode -> unsupportedErr "OpAnomaDecode" OpAnomaVerifyDetached -> unsupportedErr "OpAnomaVerifyDetached" + OpAnomaSign -> unsupportedErr "OpAnomaSign" + OpAnomaVerify -> unsupportedErr "OpAnomaVerify" where unsupportedErr :: Text -> Sem r () unsupportedErr opName = diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index 6258e957ec..2fff5c899f 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -317,6 +317,8 @@ genCode infoTable fi = Core.OpAnomaEncode -> OpAnomaEncode Core.OpAnomaDecode -> OpAnomaDecode Core.OpAnomaVerifyDetached -> OpAnomaVerifyDetached + Core.OpAnomaSign -> OpAnomaSign + Core.OpAnomaVerify -> OpAnomaVerify _ -> impossible getArgsNum :: Symbol -> Int diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs index 5b51020047..4ec296c655 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs @@ -127,6 +127,8 @@ parseAnoma = <|> parseAnoma' kwAnomaDecode OpAnomaDecode <|> parseAnoma' kwAnomaEncode OpAnomaEncode <|> parseAnoma' kwAnomaVerifyDetached OpAnomaVerifyDetached + <|> parseAnoma' kwAnomaSign OpAnomaSign + <|> parseAnoma' kwAnomaVerify OpAnomaVerify parseAnoma' :: (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) => diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index 13b4136fec..6203d45f36 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -5,7 +5,6 @@ module Juvix.Data.Keyword.All where import Juvix.Data.Keyword -import Juvix.Extra.Strings qualified as Std import Juvix.Extra.Strings qualified as Str kwAs :: Keyword @@ -453,7 +452,13 @@ kwAnomaEncode :: Keyword kwAnomaEncode = asciiKw Str.anomaEncode kwAnomaVerifyDetached :: Keyword -kwAnomaVerifyDetached = asciiKw Std.anomaVerifyDetached +kwAnomaVerifyDetached = asciiKw Str.anomaVerifyDetached + +kwAnomaSign :: Keyword +kwAnomaSign = asciiKw Str.anomaSign + +kwAnomaVerify :: Keyword +kwAnomaVerify = asciiKw Str.anomaVerify delimBraceL :: Keyword delimBraceL = mkDelim Str.braceL diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index e7ef91d201..4347536591 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -338,6 +338,12 @@ anomaDecode = "anoma-decode" anomaVerifyDetached :: (IsString s) => s anomaVerifyDetached = "anoma-verify-detached" +anomaSign :: (IsString s) => s +anomaSign = "anoma-sign" + +anomaVerify :: (IsString s) => s +anomaVerify = "anoma-verify" + builtinSeq :: (IsString s) => s builtinSeq = "seq" diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index e6047f628e..26da948ea3 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -568,5 +568,13 @@ allTests = [] $ checkOutput [ [nock| true |] - ] + ], + let toSignAndVerify :: Term Natural = [nock| [1 2 nil] |] + in mkAnomaCallTest + "Test078: Anoma sign and verify" + $(mkRelDir ".") + $(mkRelFile "test078.juvix") + [OpQuote # toSignAndVerify] + $ checkOutput + [toSignAndVerify] ] diff --git a/test/Tree/Transformation/CheckNoAnoma.hs b/test/Tree/Transformation/CheckNoAnoma.hs index 5ff89bd83f..e1ee80c76f 100644 --- a/test/Tree/Transformation/CheckNoAnoma.hs +++ b/test/Tree/Transformation/CheckNoAnoma.hs @@ -75,5 +75,13 @@ tests = Eval.NegTest "anomaVerifyDetached" $(mkRelDir ".") - $(mkRelFile "test012.jvt") + $(mkRelFile "test012.jvt"), + Eval.NegTest + "anomaSign" + $(mkRelDir ".") + $(mkRelFile "test013.jvt"), + Eval.NegTest + "anomaVerify" + $(mkRelDir ".") + $(mkRelFile "test014.jvt") ] diff --git a/tests/Anoma/Compilation/positive/test078.juvix b/tests/Anoma/Compilation/positive/test078.juvix new file mode 100644 index 0000000000..c6ecde6dbb --- /dev/null +++ b/tests/Anoma/Compilation/positive/test078.juvix @@ -0,0 +1,17 @@ +module test078; + +import Stdlib.Prelude open; + +builtin anoma-sign +axiom anomaSign : {A : Type} -> A -> Nat -> Nat; + +builtin anoma-verify +axiom anomaVerify : {A : Type} -> Nat -> Nat -> A; + +privKey : Nat := + 0x3181f891cd2323ffe802dd8f36f7e77cd072e3bd8f49884e8b38a297646351e9015535fa1125ec092c85758756d51bf29eed86a118942135c1657bf4cb5c6fc9; + +pubKey : Nat := + 0x3181f891cd2323ffe802dd8f36f7e77cd072e3bd8f49884e8b38a297646351e9; + +main (input : List Nat) : List Nat := anomaVerify (anomaSign input privKey) pubKey; diff --git a/tests/Tree/negative/test013.jvt b/tests/Tree/negative/test013.jvt new file mode 100644 index 0000000000..f3dbd61873 --- /dev/null +++ b/tests/Tree/negative/test013.jvt @@ -0,0 +1,5 @@ +-- calling unsupported anoma-sign + +function main() : * { + anoma-sign(1,2) +} diff --git a/tests/Tree/negative/test014.jvt b/tests/Tree/negative/test014.jvt new file mode 100644 index 0000000000..b11fffaba1 --- /dev/null +++ b/tests/Tree/negative/test014.jvt @@ -0,0 +1,5 @@ +-- calling unsupported anoma-verify + +function main() : * { + anoma-verify(1,2) +}