diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index 73af0048a9..bde6c1666e 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -83,3 +83,16 @@ registerAnomaVerify f = do ((ftype ==% (u <>--> nat --> nat --> dataT)) freeVars) (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> A") registerBuiltin BuiltinAnomaVerify (f ^. axiomName) + +registerAnomaSignDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () +registerAnomaSignDetached 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 "anomaSignDetached must be of type {A : Type} -> A -> Nat -> Nat") + registerBuiltin BuiltinAnomaSignDetached (f ^. axiomName) diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index a5bfb3f5bf..83f531bcb5 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -200,6 +200,7 @@ data BuiltinAxiom | BuiltinAnomaDecode | BuiltinAnomaVerifyDetached | BuiltinAnomaSign + | BuiltinAnomaSignDetached | BuiltinAnomaVerify | BuiltinPoseidon | BuiltinEcOp @@ -241,6 +242,7 @@ instance Pretty BuiltinAxiom where BuiltinAnomaEncode -> Str.anomaEncode BuiltinAnomaDecode -> Str.anomaDecode BuiltinAnomaVerifyDetached -> Str.anomaVerifyDetached + BuiltinAnomaSignDetached -> Str.anomaSignDetached BuiltinAnomaSign -> Str.anomaSign BuiltinAnomaVerify -> Str.anomaVerify BuiltinPoseidon -> Str.cairoPoseidon diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index e94ac0ab59..0e439b7907 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -195,6 +195,7 @@ geval opts herr ctx env0 = eval' env0 OpAnomaDecode -> anomaDecodeOp OpAnomaVerifyDetached -> anomaVerifyDetachedOp OpAnomaSign -> anomaSignOp + OpAnomaSignDetached -> anomaSignDetachedOp OpAnomaVerify -> anomaVerifyOp OpPoseidonHash -> poseidonHashOp OpEc -> ecOp @@ -378,6 +379,15 @@ geval opts herr ctx env0 = eval' env0 err "unsupported builtin operation: OpAnomaSign" {-# INLINE anomaSignOp #-} + anomaSignDetachedOp :: [Node] -> Node + anomaSignDetachedOp = checkApply $ \arg1 arg2 -> + if + | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure -> + mkBuiltinApp' OpAnomaSignDetached (eval' env <$> [arg1, arg2]) + | otherwise -> + err "unsupported builtin operation: OpAnomaSignDetached" + {-# INLINE anomaSignDetachedOp #-} + anomaVerifyOp :: [Node] -> Node anomaVerifyOp = checkApply $ \arg1 arg2 -> if diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index 33fa1f8ffd..e45843f2f4 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -428,6 +428,7 @@ builtinOpArgTypes = \case OpAnomaDecode -> [mkDynamic'] OpAnomaVerifyDetached -> [mkDynamic', mkDynamic', mkDynamic'] OpAnomaSign -> [mkDynamic', mkDynamic'] + OpAnomaSignDetached -> [mkDynamic', mkDynamic'] OpAnomaVerify -> [mkDynamic', mkDynamic'] OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index 1debafee76..ba45f8c122 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -31,6 +31,7 @@ data BuiltinOp | OpAnomaDecode | OpAnomaVerifyDetached | OpAnomaSign + | OpAnomaSignDetached | OpAnomaVerify | OpPoseidonHash | OpEc @@ -84,6 +85,7 @@ builtinOpArgsNum = \case OpAnomaDecode -> 1 OpAnomaVerifyDetached -> 3 OpAnomaSign -> 2 + OpAnomaSignDetached -> 2 OpAnomaVerify -> 2 OpPoseidonHash -> 1 OpEc -> 3 @@ -126,6 +128,7 @@ builtinIsFoldable = \case OpAnomaDecode -> False OpAnomaVerifyDetached -> False OpAnomaSign -> False + OpAnomaSignDetached -> False OpAnomaVerify -> False OpPoseidonHash -> False OpEc -> False @@ -150,5 +153,6 @@ builtinsAnoma = OpAnomaDecode, OpAnomaVerifyDetached, OpAnomaSign, - OpAnomaVerify + OpAnomaVerify, + OpAnomaSignDetached ] diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 194780635d..e9ac9824a1 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -57,6 +57,7 @@ instance PrettyCode BuiltinOp where OpAnomaDecode -> return primAnomaDecode OpAnomaVerifyDetached -> return primAnomaVerifyDetached OpAnomaSign -> return primAnomaSign + OpAnomaSignDetached -> return primAnomaSignDetached OpAnomaVerify -> return primAnomaVerify OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc @@ -815,6 +816,9 @@ primAnomaVerifyDetached = primitive Str.anomaVerifyDetached primAnomaSign :: Doc Ann primAnomaSign = primitive Str.anomaSign +primAnomaSignDetached :: Doc Ann +primAnomaSignDetached = primitive Str.anomaSignDetached + primAnomaVerify :: Doc Ann primAnomaVerify = primitive Str.anomaVerify diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 36b6bc7fc2..96f5825608 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -71,6 +71,7 @@ computeNodeTypeInfo md = umapL go OpAnomaDecode -> Info.getNodeType node OpAnomaVerifyDetached -> Info.getNodeType node OpAnomaSign -> Info.getNodeType node + OpAnomaSignDetached -> Info.getNodeType node OpAnomaVerify -> Info.getNodeType node OpPoseidonHash -> case _builtinAppArgs of [arg] -> Info.getNodeType arg diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index fc2e0d6e41..bba87ca07e 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -588,6 +588,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinAnomaDecode -> return () Internal.BuiltinAnomaVerifyDetached -> return () Internal.BuiltinAnomaSign -> return () + Internal.BuiltinAnomaSignDetached -> return () Internal.BuiltinAnomaVerify -> return () Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () @@ -751,6 +752,19 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) ) ) ) + Internal.BuiltinAnomaSignDetached -> do + natType <- getNatType + registerAxiomDef + ( mkLambda' + mkSmallUniv + ( mkLambda' + (mkVar' 0) + ( mkLambda' + natType + (mkBuiltinApp' OpAnomaSignDetached [mkVar' 1, mkVar' 0]) + ) + ) + ) Internal.BuiltinAnomaVerify -> do natType <- getNatType registerAxiomDef @@ -1172,6 +1186,7 @@ goApplication a = do Just Internal.BuiltinAnomaDecode -> app Just Internal.BuiltinAnomaVerifyDetached -> app Just Internal.BuiltinAnomaSign -> app + Just Internal.BuiltinAnomaSignDetached -> app Just Internal.BuiltinAnomaVerify -> app Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 0413bf1783..83fedea88e 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -100,6 +100,7 @@ fromCore fsize tab = BuiltinAnomaDecode -> False BuiltinAnomaVerifyDetached -> False BuiltinAnomaSign -> False + BuiltinAnomaSignDetached -> False BuiltinAnomaVerify -> False BuiltinPoseidon -> False BuiltinEcOp -> False diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 228c5a9516..eba5104bb8 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -573,6 +573,7 @@ registerBuiltinAxiom d = \case BuiltinAnomaDecode -> registerAnomaDecode d BuiltinAnomaVerifyDetached -> registerAnomaVerifyDetached d BuiltinAnomaSign -> registerAnomaSign d + BuiltinAnomaSignDetached -> registerAnomaSignDetached d BuiltinAnomaVerify -> registerAnomaVerify d BuiltinPoseidon -> registerPoseidon d BuiltinEcOp -> registerEcOp d diff --git a/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs b/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs index 446705eefc..e96fa25b38 100644 --- a/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs +++ b/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs @@ -6,9 +6,14 @@ import Data.ByteString.Builder qualified as BS import Juvix.Compiler.Nockma.Language import Juvix.Prelude.Base +-- | Encode an atom to little-endian bytes atomToByteString :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r ByteString atomToByteString = fmap naturalToByteString . nockNatural +-- | Encode an atom to little-endian bytes, padded with zeros up to a specified length +atomToByteStringLen :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Int -> Atom a -> Sem r ByteString +atomToByteStringLen len = fmap (padByteString len) . atomToByteString + byteStringToAtom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => ByteString -> Sem r (Atom a) byteStringToAtom = fmap mkEmptyAtom . fromNatural . byteStringToNatural @@ -48,3 +53,9 @@ mkEmptyAtom x = { _atomInfo = emptyAtomInfo, _atom = x } + +-- | Pad a ByteString with zeros up to a specified length +padByteString :: Int -> ByteString -> ByteString +padByteString n bs + | BS.length bs >= n = bs + | otherwise = BS.append bs (BS.replicate (n - BS.length bs) 0) diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs index 230017926f..d7efc19727 100644 --- a/src/Juvix/Compiler/Nockma/Evaluator.hs +++ b/src/Juvix/Compiler/Nockma/Evaluator.hs @@ -244,6 +244,9 @@ evalProfile inistack initerm = 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)]" + StdlibSignDetached -> case args' of + TCell (TermAtom message) (TermAtom privKey) -> goSignDetached 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)]" @@ -254,24 +257,41 @@ evalProfile inistack initerm = goCat :: Atom a -> Atom a -> Sem r (Term a) goCat arg1 arg2 = TermAtom . setAtomHint AtomHintString <$> atomConcatenateBytes arg1 arg2 + signatureLength :: Int + signatureLength = 64 + + publicKeyLength :: Int + publicKeyLength = 32 + + privateKeyLength :: Int + privateKeyLength = 64 + goVerifyDetached :: Atom a -> Atom a -> Atom a -> Sem r (Term a) goVerifyDetached sigT messageT pubKeyT = do - sig <- Signature <$> atomToByteString sigT - pubKey <- PublicKey <$> atomToByteString pubKeyT + sig <- Signature <$> atomToByteStringLen signatureLength sigT + pubKey <- PublicKey <$> atomToByteStringLen publicKeyLength pubKeyT message <- atomToByteString messageT 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 + privKey <- SecretKey <$> atomToByteStringLen privateKeyLength privKeyT message <- atomToByteString messageT res <- byteStringToAtom (sign privKey message) return (TermAtom res) + goSignDetached :: Atom a -> Atom a -> Sem r (Term a) + goSignDetached messageT privKeyT = do + privKey <- SecretKey <$> atomToByteStringLen privateKeyLength privKeyT + message <- atomToByteString messageT + let (Signature sig) = dsign privKey message + res <- byteStringToAtom sig + return (TermAtom res) + goVerify :: Atom a -> Atom a -> Sem r (Term a) goVerify signedMessageT pubKeyT = do - pubKey <- PublicKey <$> atomToByteString pubKeyT + pubKey <- PublicKey <$> atomToByteStringLen publicKeyLength pubKeyT signedMessage <- atomToByteString signedMessageT if | verify pubKey signedMessage -> TermAtom <$> byteStringToAtom (removeSignature signedMessage) diff --git a/src/Juvix/Compiler/Nockma/StdlibFunction.hs b/src/Juvix/Compiler/Nockma/StdlibFunction.hs index 30d70e81a5..fb3ac49fb0 100644 --- a/src/Juvix/Compiler/Nockma/StdlibFunction.hs +++ b/src/Juvix/Compiler/Nockma/StdlibFunction.hs @@ -24,6 +24,7 @@ stdlibPath = \case StdlibDecode -> [nock| [9 94 0 3] |] StdlibVerifyDetached -> [nock| [9 22 0 1] |] StdlibSign -> [nock| [9 10 0 1] |] + StdlibSignDetached -> [nock| [9 23 0 1] |] StdlibVerify -> [nock| [9 4 0 1] |] -- Obtained from the urbit dojo using: -- diff --git a/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs b/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs index 66600c3e96..38dbc34ba9 100644 --- a/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs +++ b/src/Juvix/Compiler/Nockma/StdlibFunction/Base.hs @@ -18,6 +18,7 @@ instance Pretty StdlibFunction where StdlibDecode -> "decode" StdlibVerifyDetached -> "verify-detached" StdlibSign -> "sign" + StdlibSignDetached -> "sign-detached" StdlibVerify -> "verify" StdlibCatBytes -> "cat" @@ -35,6 +36,7 @@ data StdlibFunction | StdlibDecode | StdlibVerifyDetached | StdlibSign + | StdlibSignDetached | StdlibVerify | StdlibCatBytes deriving stock (Show, Lift, Eq, Bounded, Enum, Generic) diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index 5b962361f8..c8d2700f76 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -438,6 +438,7 @@ compile = \case Tree.OpAnomaVerifyDetached -> return (goAnomaVerifyDetached args) Tree.OpAnomaSign -> return (goAnomaSign args) Tree.OpAnomaVerify -> return (goAnomaVerify args) + Tree.OpAnomaSignDetached -> return (goAnomaSignDetached args) goUnop :: Tree.NodeUnop -> Sem r (Term Natural) goUnop Tree.NodeUnop {..} = do @@ -478,6 +479,11 @@ compile = \case [message, privKey] -> callStdlib StdlibSign [goAnomaEncode [message], privKey] _ -> impossible + goAnomaSignDetached :: [Term Natural] -> Term Natural + goAnomaSignDetached = \case + [message, privKey] -> callStdlib StdlibSignDetached [goAnomaEncode [message], privKey] + _ -> impossible + goAnomaVerify :: [Term Natural] -> Term Natural goAnomaVerify = \case [signedMessage, pubKey] -> callStdlib StdlibDecode [callStdlib StdlibVerify [signedMessage, pubKey]] diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs index 2b37e7a9d8..e0b958c70d 100644 --- a/src/Juvix/Compiler/Tree/Keywords.hs +++ b/src/Juvix/Compiler/Tree/Keywords.hs @@ -13,6 +13,7 @@ import Juvix.Data.Keyword.All kwAnomaEncode, kwAnomaGet, kwAnomaSign, + kwAnomaSignDetached, kwAnomaVerify, kwAnomaVerifyDetached, kwArgsNum, @@ -83,6 +84,7 @@ allKeywords = kwAnomaEncode, kwAnomaVerifyDetached, kwAnomaSign, + kwAnomaSignDetached, kwAnomaVerify, kwPoseidon, kwEcOp, diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index 49a1924e36..94b58a585a 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -62,4 +62,6 @@ data AnomaOp OpAnomaSign | -- | Verify a signature obtained from OpAnomaSign using a public key OpAnomaVerify + | -- | Produce a cryptographic signature of an Anoma value + OpAnomaSignDetached deriving stock (Eq) diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index 1b4e5fcd9b..47ffbf544a 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -248,6 +248,7 @@ instance PrettyCode AnomaOp where OpAnomaVerifyDetached -> Str.anomaVerifyDetached OpAnomaSign -> Str.anomaSign OpAnomaVerify -> Str.anomaVerify + OpAnomaSignDetached -> Str.anomaSignDetached 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 92a9a1b88d..44561e0977 100644 --- a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs +++ b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs @@ -16,6 +16,7 @@ checkNoAnoma = walkT checkNode OpAnomaDecode -> unsupportedErr "OpAnomaDecode" OpAnomaVerifyDetached -> unsupportedErr "OpAnomaVerifyDetached" OpAnomaSign -> unsupportedErr "OpAnomaSign" + OpAnomaSignDetached -> unsupportedErr "OpAnomaSignDetached" OpAnomaVerify -> unsupportedErr "OpAnomaVerify" where unsupportedErr :: Text -> Sem r () diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index 2fff5c899f..9829d6b368 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -318,6 +318,7 @@ genCode infoTable fi = Core.OpAnomaDecode -> OpAnomaDecode Core.OpAnomaVerifyDetached -> OpAnomaVerifyDetached Core.OpAnomaSign -> OpAnomaSign + Core.OpAnomaSignDetached -> OpAnomaSignDetached Core.OpAnomaVerify -> OpAnomaVerify _ -> impossible diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs index 4ec296c655..b4b4d1d6a6 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs @@ -128,6 +128,7 @@ parseAnoma = <|> parseAnoma' kwAnomaEncode OpAnomaEncode <|> parseAnoma' kwAnomaVerifyDetached OpAnomaVerifyDetached <|> parseAnoma' kwAnomaSign OpAnomaSign + <|> parseAnoma' kwAnomaSignDetached OpAnomaSignDetached <|> parseAnoma' kwAnomaVerify OpAnomaVerify parseAnoma' :: diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index 6203d45f36..0c118377c1 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -457,6 +457,9 @@ kwAnomaVerifyDetached = asciiKw Str.anomaVerifyDetached kwAnomaSign :: Keyword kwAnomaSign = asciiKw Str.anomaSign +kwAnomaSignDetached :: Keyword +kwAnomaSignDetached = asciiKw Str.anomaSignDetached + kwAnomaVerify :: Keyword kwAnomaVerify = asciiKw Str.anomaVerify diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 178a147bdf..d31d659cab 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -344,6 +344,9 @@ anomaVerifyDetached = "anoma-verify-detached" anomaSign :: (IsString s) => s anomaSign = "anoma-sign" +anomaSignDetached :: (IsString s) => s +anomaSignDetached = "anoma-sign-detached" + anomaVerify :: (IsString s) => s anomaVerify = "anoma-verify" diff --git a/test/Tree/Transformation/CheckNoAnoma.hs b/test/Tree/Transformation/CheckNoAnoma.hs index e1ee80c76f..e36186bb4e 100644 --- a/test/Tree/Transformation/CheckNoAnoma.hs +++ b/test/Tree/Transformation/CheckNoAnoma.hs @@ -83,5 +83,9 @@ tests = Eval.NegTest "anomaVerify" $(mkRelDir ".") - $(mkRelFile "test014.jvt") + $(mkRelFile "test014.jvt"), + Eval.NegTest + "anomaSignDetached" + $(mkRelDir ".") + $(mkRelFile "test015.jvt") ] diff --git a/tests/Anoma/Compilation/positive/test077.juvix b/tests/Anoma/Compilation/positive/test077.juvix index 733d273507..eea1e004a2 100644 --- a/tests/Anoma/Compilation/positive/test077.juvix +++ b/tests/Anoma/Compilation/positive/test077.juvix @@ -3,6 +3,12 @@ module test077; import Stdlib.Prelude open; import Stdlib.Debug.Trace open; +builtin anoma-sign-detached +axiom anomaSignDetached : {A : Type} + -> A + -> Nat + -> Nat; + builtin anoma-verify-detached axiom anomaVerifyDetached : {A : Type} -> Nat @@ -10,11 +16,11 @@ axiom anomaVerifyDetached : {A : Type} -> Nat -> Bool; ---- dsign privateKey (anomaEncode 1) -sig : Nat := - 0x9dac7337633844c1df6af03431adec37b8b67331fbd0a36553dd11f8ac92107e58f0ca42d93d88f98a2f1181e81e1808842193af64a4abb42c6e57570fd7a5a; +privKey : Nat := + 0x3181f891cd2323ffe802dd8f36f7e77cd072e3bd8f49884e8b38a297646351e9015535fa1125ec092c85758756d51bf29eed86a118942135c1657bf4cb5c6fc9; -publicKey : Nat := - 0xd5d974196b220bc1fc3c11a0a04bfa46b2aba0c792daf2f3f6c2d6ac1064c463; +pubKey : Nat := + 0x3181f891cd2323ffe802dd8f36f7e77cd072e3bd8f49884e8b38a297646351e9; -main : Bool := anomaVerifyDetached sig 1 publicKey; +main : Bool := let msg : Nat := 1 in + anomaVerifyDetached (anomaSignDetached msg privKey) msg pubKey; diff --git a/tests/Tree/negative/test015.jvt b/tests/Tree/negative/test015.jvt new file mode 100644 index 0000000000..e6be335d05 --- /dev/null +++ b/tests/Tree/negative/test015.jvt @@ -0,0 +1,5 @@ +-- calling unsupported anoma-sign-detached + +function main() : * { + anoma-sign-detached(1,2) +}