From 764728eedbb3567a779a0de129cbb49c300aeee1 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Sat, 7 Dec 2024 15:34:59 +0000 Subject: [PATCH] Add support for Anoma RM is-commitment and is-nullifier These functions are required to translate the RM proof record self-tag field to a Juvix type that differentiates between nullifiers and commitments. This information is required when writing logic functions. --- src/Juvix/Compiler/Builtins/Anoma.hs | 16 ++++++++++++++++ src/Juvix/Compiler/Concrete/Data/Builtins.hs | 6 ++++++ src/Juvix/Compiler/Core/Evaluator.hs | 2 ++ src/Juvix/Compiler/Core/Extra/Utils.hs | 4 ++++ src/Juvix/Compiler/Core/Keywords.hs | 2 ++ src/Juvix/Compiler/Core/Language/Builtins.hs | 6 ++++++ src/Juvix/Compiler/Core/Pretty/Base.hs | 8 ++++++++ .../Core/Transformation/ComputeTypeInfo.hs | 2 ++ .../Compiler/Core/Translation/FromInternal.hs | 18 ++++++++++++++++++ .../Compiler/Core/Translation/FromSource.hs | 2 ++ .../Core/Translation/Stripped/FromCore.hs | 2 ++ .../Internal/Translation/FromConcrete.hs | 2 ++ src/Juvix/Compiler/Nockma/AnomaLib.hs | 2 ++ src/Juvix/Compiler/Nockma/AnomaLib/Base.hs | 4 ++++ .../Compiler/Nockma/Translation/FromTree.hs | 2 ++ src/Juvix/Compiler/Tree/Keywords.hs | 2 ++ src/Juvix/Compiler/Tree/Language/Builtins.hs | 4 ++++ src/Juvix/Compiler/Tree/Pretty/Base.hs | 2 ++ .../Compiler/Tree/Translation/FromCore.hs | 2 ++ .../Compiler/Tree/Translation/FromSource.hs | 2 ++ src/Juvix/Data/Keyword/All.hs | 6 ++++++ src/Juvix/Extra/Strings.hs | 6 ++++++ test/Anoma/Compilation/Positive.hs | 4 ++++ .../test085/client/ResourceMachine.juvix | 6 ++++++ .../Compilation/positive/test085/delta.juvix | 11 +++++++---- 25 files changed, 119 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index efa03b1272..5b802fc27f 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -251,3 +251,19 @@ checkAnomaRandomSplit f = do pair_ <- getBuiltinNameScoper l BuiltinPair unless (f ^. axiomType === (gen --> pair_ @@ gen @@ gen)) $ builtinsErrorText l "randomSplit must be of type AnomaRandomGenerator -> Pair AnomaRandomGenerator AnomaRandomGenerator" + +checkAnomaIsCommitment :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () +checkAnomaIsCommitment f = do + let l = getLoc f + nat_ <- getBuiltinNameScoper l BuiltinNat + bool_ <- getBuiltinNameScoper l BuiltinBool + unless (f ^. axiomType == (nat_ --> bool_)) $ + builtinsErrorText l "isCommitment must be of type Nat -> Bool" + +checkAnomaIsNullifier :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () +checkAnomaIsNullifier f = do + let l = getLoc f + nat_ <- getBuiltinNameScoper l BuiltinNat + bool_ <- getBuiltinNameScoper l BuiltinBool + unless (f ^. axiomType == (nat_ --> bool_)) $ + builtinsErrorText l "isNullifier must be of type Nat -> Bool" diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 27ef4f43d3..0e5aed62ad 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -278,6 +278,8 @@ data BuiltinAxiom | BuiltinAnomaRandomGeneratorInit | BuiltinAnomaRandomNextBytes | BuiltinAnomaRandomSplit + | BuiltinAnomaIsCommitment + | BuiltinAnomaIsNullifier | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint @@ -342,6 +344,8 @@ instance HasNameKind BuiltinAxiom where BuiltinAnomaRandomGeneratorInit -> KNameFunction BuiltinAnomaRandomNextBytes -> KNameFunction BuiltinAnomaRandomSplit -> KNameFunction + BuiltinAnomaIsCommitment -> KNameFunction + BuiltinAnomaIsNullifier -> KNameFunction BuiltinPoseidon -> KNameFunction BuiltinEcOp -> KNameFunction BuiltinRandomEcPoint -> KNameFunction @@ -413,6 +417,8 @@ instance Pretty BuiltinAxiom where BuiltinAnomaRandomGeneratorInit -> Str.anomaRandomGeneratorInit BuiltinAnomaRandomNextBytes -> Str.anomaRandomNextBytes BuiltinAnomaRandomSplit -> Str.anomaRandomSplit + BuiltinAnomaIsCommitment -> Str.anomaIsCommitment + BuiltinAnomaIsNullifier -> Str.anomaIsNullifier 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 6ce93016fc..95dbd24689 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -242,6 +242,8 @@ geval opts herr tab env0 = eval' env0 OpAnomaRandomGeneratorInit -> normalizeOrUnsupported opcode OpAnomaRandomNextBytes -> normalizeOrUnsupported opcode OpAnomaRandomSplit -> normalizeOrUnsupported opcode + OpAnomaIsCommitment -> normalizeOrUnsupported opcode + OpAnomaIsNullifier -> normalizeOrUnsupported opcode OpPoseidonHash -> poseidonHashOp OpEc -> ecOp OpRandomEcPoint -> randomEcPointOp diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index ef334ab043..720d736bf9 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -233,6 +233,8 @@ isDebugOp = \case OpAnomaRandomGeneratorInit -> False OpAnomaRandomNextBytes -> False OpAnomaRandomSplit -> False + OpAnomaIsCommitment -> False + OpAnomaIsNullifier -> False OpEc -> False OpFieldAdd -> False OpFieldDiv -> False @@ -534,6 +536,8 @@ builtinOpArgTypes = \case OpAnomaRandomGeneratorInit -> [mkTypeInteger'] OpAnomaRandomNextBytes -> [mkTypeInteger', mkTypeRandomGenerator'] OpAnomaRandomSplit -> [mkTypeRandomGenerator'] + OpAnomaIsCommitment -> [mkTypeInteger'] + OpAnomaIsNullifier -> [mkTypeInteger'] OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] OpRandomEcPoint -> [] diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs index e73c20997e..083dcf764d 100644 --- a/src/Juvix/Compiler/Core/Keywords.hs +++ b/src/Juvix/Compiler/Core/Keywords.hs @@ -13,6 +13,8 @@ import Juvix.Data.Keyword.All kwAnomaAddDelta, kwAnomaDecode, kwAnomaEncode, + kwAnomaIsCommitment, + kwAnomaIsNullifier, kwAnomaProveAction, kwAnomaProveDelta, kwAnomaRandomGeneratorInit, diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index 1991f62b73..a8b0de4bb6 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -54,6 +54,8 @@ data BuiltinOp | OpAnomaRandomGeneratorInit | OpAnomaRandomNextBytes | OpAnomaRandomSplit + | OpAnomaIsCommitment + | OpAnomaIsNullifier | OpPoseidonHash | OpEc | OpRandomEcPoint @@ -142,6 +144,8 @@ builtinOpArgsNum = \case OpAnomaRandomGeneratorInit -> 1 OpAnomaRandomNextBytes -> 2 OpAnomaRandomSplit -> 1 + OpAnomaIsCommitment -> 1 + OpAnomaIsNullifier -> 1 OpPoseidonHash -> 1 OpEc -> 3 OpRandomEcPoint -> 0 @@ -207,6 +211,8 @@ builtinIsFoldable = \case OpAnomaRandomGeneratorInit -> False OpAnomaRandomNextBytes -> False OpAnomaRandomSplit -> False + OpAnomaIsCommitment -> False + OpAnomaIsNullifier -> False OpPoseidonHash -> False OpEc -> False OpRandomEcPoint -> False diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index e602a4e09f..7802c862bb 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -78,6 +78,8 @@ instance PrettyCode BuiltinOp where OpAnomaRandomGeneratorInit -> return primRandomGeneratorInit OpAnomaRandomNextBytes -> return primRandomNextBytes OpAnomaRandomSplit -> return primRandomSplit + OpAnomaIsCommitment -> return primIsCommitment + OpAnomaIsNullifier -> return primIsNullifier OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc OpRandomEcPoint -> return primRandomEcPoint @@ -1015,6 +1017,12 @@ primRandomNextBytes = primitive Str.anomaRandomNextBytes primRandomSplit :: Doc Ann primRandomSplit = primitive Str.anomaRandomSplit +primIsCommitment :: Doc Ann +primIsCommitment = primitive Str.anomaIsCommitment + +primIsNullifier :: Doc Ann +primIsNullifier = primitive Str.anomaIsNullifier + 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 e5972ccb50..2a070c30d2 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -103,6 +103,8 @@ computeNodeTypeInfo md = umapL go OpAnomaRandomGeneratorInit -> mkTypeRandomGenerator' OpAnomaRandomNextBytes -> mkDynamic' OpAnomaRandomSplit -> mkDynamic' + OpAnomaIsCommitment -> mkTypeBool' + OpAnomaIsNullifier -> mkTypeBool' 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 c2aa512222..1fba4a93d7 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -672,6 +672,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinAnomaRandomGeneratorInit -> return () Internal.BuiltinAnomaRandomNextBytes -> return () Internal.BuiltinAnomaRandomSplit -> return () + Internal.BuiltinAnomaIsCommitment -> return () + Internal.BuiltinAnomaIsNullifier -> return () Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () @@ -986,6 +988,20 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) mkDynamic' (mkBuiltinApp' OpAnomaRandomSplit [mkVar' 0]) ) + Internal.BuiltinAnomaIsCommitment -> do + natType <- getNatType + registerAxiomDef + ( mkLambda' + natType + (mkBuiltinApp' OpAnomaIsCommitment [mkVar' 0]) + ) + Internal.BuiltinAnomaIsNullifier -> do + natType <- getNatType + registerAxiomDef + ( mkLambda' + natType + (mkBuiltinApp' OpAnomaIsNullifier [mkVar' 0]) + ) Internal.BuiltinPoseidon -> do psName <- getPoseidonStateName psSym <- getPoseidonStateSymbol @@ -1447,6 +1463,8 @@ goApplication a = do Just Internal.BuiltinAnomaRandomGeneratorInit -> app Just Internal.BuiltinAnomaRandomNextBytes -> app Just Internal.BuiltinAnomaRandomSplit -> app + Just Internal.BuiltinAnomaIsCommitment -> app + Just Internal.BuiltinAnomaIsNullifier -> app Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index efe997765e..893a61a2d9 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -599,6 +599,8 @@ builtinAppExpr varsNum vars = do <|> (kw kwAnomaRandomGeneratorInit $> OpAnomaRandomGeneratorInit) <|> (kw kwAnomaRandomNextBytes $> OpAnomaRandomNextBytes) <|> (kw kwAnomaRandomSplit $> OpAnomaRandomSplit) + <|> (kw kwAnomaIsCommitment $> OpAnomaIsCommitment) + <|> (kw kwAnomaIsNullifier $> OpAnomaIsNullifier) args <- P.many (atom varsNum vars) return $ mkBuiltinApp' op args diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 32c56501e0..7f4ef11dd3 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -136,6 +136,8 @@ fromCore fsize tab = BuiltinAnomaRandomGeneratorInit -> False BuiltinAnomaRandomNextBytes -> False BuiltinAnomaRandomSplit -> False + BuiltinAnomaIsCommitment -> False + BuiltinAnomaIsNullifier -> 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 a88d4116af..1d2494bd15 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -1142,6 +1142,8 @@ checkBuiltinAxiom d b = localBuiltins $ case b of BuiltinAnomaRandomGeneratorInit -> checkAnomaRandomGeneratorInit d BuiltinAnomaRandomNextBytes -> checkAnomaRandomNextBytes d BuiltinAnomaRandomSplit -> checkAnomaRandomSplit d + BuiltinAnomaIsCommitment -> checkAnomaIsCommitment d + BuiltinAnomaIsNullifier -> checkAnomaIsNullifier d BuiltinPoseidon -> checkPoseidon d BuiltinEcOp -> checkEcOp d BuiltinRandomEcPoint -> checkRandomEcPoint d diff --git a/src/Juvix/Compiler/Nockma/AnomaLib.hs b/src/Juvix/Compiler/Nockma/AnomaLib.hs index d6548156e9..9d90e563de 100644 --- a/src/Juvix/Compiler/Nockma/AnomaLib.hs +++ b/src/Juvix/Compiler/Nockma/AnomaLib.hs @@ -116,5 +116,7 @@ anomaLibPath = \case RmActionDelta -> [nock| [9 4 0 1] |] RmMakeDelta -> [nock| [9 1.494 0 1] |] RmProveDelta -> [nock| [9 1.535 0 1] |] + RmIsCommitment -> [nock| [9 1.526 0 1] |] + RmIsNullifier -> [nock| [9 372 0 1] |] AnomaLibValue (AnomaRmValue v) -> case v of RmZeroDelta -> [nock| [9 20 0 1] |] diff --git a/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs b/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs index a02c79599d..9865eea7e7 100644 --- a/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs +++ b/src/Juvix/Compiler/Nockma/AnomaLib/Base.hs @@ -56,6 +56,8 @@ data RmFunction | RmActionDelta | RmMakeDelta | RmProveDelta + | RmIsCommitment + | RmIsNullifier deriving stock (Show, Lift, Eq, Bounded, Enum, Generic) instance Hashable RmFunction @@ -128,6 +130,8 @@ instance Pretty RmFunction where RmActionDelta -> "action-delta" RmMakeDelta -> "make-delta" RmProveDelta -> "prove-delta" + RmIsCommitment -> "is-commitment" + RmIsNullifier -> "is-nullifier" instance Pretty RmValue where pretty = \case diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index b6eb4a4777..a13de9789d 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -585,6 +585,8 @@ compile = \case Tree.OpAnomaRandomGeneratorInit -> callStdlib StdlibRandomInitGen args Tree.OpAnomaRandomNextBytes -> goAnomaRandomNextBytes args Tree.OpAnomaRandomSplit -> callStdlib StdlibRandomSplit args + Tree.OpAnomaIsCommitment -> callRm RmIsCommitment args + Tree.OpAnomaIsNullifier -> callRm RmIsNullifier args goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural) goByteArrayOp Tree.NodeByteArray {..} = do diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs index 0f8db23620..c8b4379070 100644 --- a/src/Juvix/Compiler/Tree/Keywords.hs +++ b/src/Juvix/Compiler/Tree/Keywords.hs @@ -17,6 +17,8 @@ import Juvix.Data.Keyword.All kwAnomaDecode, kwAnomaEncode, kwAnomaGet, + kwAnomaIsCommitment, + kwAnomaIsNullifier, kwAnomaProveAction, kwAnomaProveDelta, kwAnomaRandomGeneratorInit, diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index dceae07ab2..b06263e1a9 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -130,4 +130,8 @@ data AnomaOp OpAnomaRandomNextBytes | -- | Split a pseudorandom number generator into two uncorrelated generators OpAnomaRandomSplit + | -- | Returns true if its argument is a commitment + OpAnomaIsCommitment + | -- | Returns true if its argument is a nullifier + OpAnomaIsNullifier deriving stock (Eq, Show) diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index 19b7b065a0..44f54c4c80 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -303,6 +303,8 @@ instance PrettyCode AnomaOp where OpAnomaRandomGeneratorInit -> Str.anomaRandomGeneratorInit OpAnomaRandomNextBytes -> Str.anomaRandomNextBytes OpAnomaRandomSplit -> Str.anomaRandomSplit + OpAnomaIsCommitment -> Str.anomaIsCommitment + OpAnomaIsNullifier -> Str.anomaIsNullifier instance PrettyCode UnaryOpcode where ppCode = \case diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index f7d869ea95..1de590d2ce 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -73,6 +73,8 @@ toTreeOp = \case Core.OpAnomaRandomGeneratorInit -> TreeAnomaOp OpAnomaRandomGeneratorInit Core.OpAnomaRandomNextBytes -> TreeAnomaOp OpAnomaRandomNextBytes Core.OpAnomaRandomSplit -> TreeAnomaOp OpAnomaRandomSplit + Core.OpAnomaIsCommitment -> TreeAnomaOp OpAnomaIsCommitment + Core.OpAnomaIsNullifier -> TreeAnomaOp OpAnomaIsNullifier -- TreeCairoOp Core.OpPoseidonHash -> TreeCairoOp OpCairoPoseidon Core.OpEc -> TreeCairoOp OpCairoEc diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs index 38b9791e98..f754f58a9e 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs @@ -170,6 +170,8 @@ parseAnoma = <|> parseAnoma' kwAnomaRandomGeneratorInit OpAnomaRandomGeneratorInit <|> parseAnoma' kwAnomaRandomNextBytes OpAnomaRandomNextBytes <|> parseAnoma' kwAnomaRandomSplit OpAnomaRandomSplit + <|> parseAnoma' kwAnomaIsCommitment OpAnomaIsCommitment + <|> parseAnoma' kwAnomaIsNullifier OpAnomaIsNullifier 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 cfac78a381..95ae770655 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -574,6 +574,12 @@ kwAnomaRandomNextBytes = asciiKw Str.anomaRandomNextBytes kwAnomaRandomSplit :: Keyword kwAnomaRandomSplit = asciiKw Str.anomaRandomSplit +kwAnomaIsCommitment :: Keyword +kwAnomaIsCommitment = asciiKw Str.anomaIsCommitment + +kwAnomaIsNullifier :: Keyword +kwAnomaIsNullifier = asciiKw Str.anomaIsNullifier + delimBraceL :: Keyword delimBraceL = mkDelim Str.braceL diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 36df2a8be6..239908a262 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -446,6 +446,12 @@ anomaRandomNextBytes = "anoma-random-next-bytes" anomaRandomSplit :: (IsString s) => s anomaRandomSplit = "anoma-random-generator-split" +anomaIsCommitment :: (IsString s) => s +anomaIsCommitment = "anoma-is-commitment" + +anomaIsNullifier :: (IsString s) => s +anomaIsNullifier = "anoma-is-nullifier" + builtinSeq :: (IsString s) => s builtinSeq = "seq" diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index 80fd95238e..08bfb3d110 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -1027,6 +1027,10 @@ allTests = [ [nock| 0 |], [nock| 0 |], [nock| 0 |], + [nock| true |], + [nock| true |], + [nock| false |], + [nock| false |], [nock| 0 |] ], mkAnomaTest diff --git a/tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix b/tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix index 7e98d1fed8..188ca3a71f 100644 --- a/tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix +++ b/tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix @@ -118,6 +118,12 @@ axiom addDelta : Delta -> Delta -> Delta; builtin anoma-sub-delta axiom subDelta : Delta -> Delta -> Delta; +builtin anoma-is-commitment +axiom isCommitment : Nat -> Bool; + +builtin anoma-is-nullifier +axiom isNullifier : Nat -> Bool; + Commitment-Root : Type := Nat; type Transaction := diff --git a/tests/Anoma/Compilation/positive/test085/delta.juvix b/tests/Anoma/Compilation/positive/test085/delta.juvix index 7bbb7b2401..3cce95599e 100644 --- a/tests/Anoma/Compilation/positive/test085/delta.juvix +++ b/tests/Anoma/Compilation/positive/test085/delta.juvix @@ -24,12 +24,11 @@ main : Delta := proofs := []; app-data := 1; }; + resCommitment : Nat := commitment resource; + resNullifier : Nat := nullifier resource; in -- Most of these call return large nouns that are not appropritate for testing. -- This test checks that these functions do not crash. - commitment - resource - >-> nullifier resource - >-> kind resource + kind resource >-> addDelta (resource-delta resource) (resource-delta resource) >-> addDelta (resource-delta resource) (resource-delta resource) >-> proveDelta zeroDelta @@ -37,4 +36,8 @@ main : Delta := >-> trace (addDelta zeroDelta zeroDelta) >-> proveAction action >-> trace (actionDelta action) + >-> trace (isCommitment resCommitment) + >-> trace (isNullifier resNullifier) + >-> trace (isCommitment resNullifier) + >-> trace (isNullifier resCommitment) >-> actionsDelta [action];