Add support for Anoma RM is-commitment and is-nullifier (#3242)

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

@@ -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"

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

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

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 -> []

src/Juvix/Compiler/Core/Keywords.hs

@@ -13,6 +13,8 @@ import Juvix.Data.Keyword.All
     kwAnomaAddDelta,
     kwAnomaDecode,
     kwAnomaEncode,
+    kwAnomaIsCommitment,
+    kwAnomaIsNullifier,
     kwAnomaProveAction,
     kwAnomaProveDelta,
     kwAnomaRandomGeneratorInit,

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

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
 

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"

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

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

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

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

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] |]

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

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

src/Juvix/Compiler/Tree/Keywords.hs

@@ -17,6 +17,8 @@ import Juvix.Data.Keyword.All
     kwAnomaDecode,
     kwAnomaEncode,
     kwAnomaGet,
+    kwAnomaIsCommitment,
+    kwAnomaIsNullifier,
     kwAnomaProveAction,
     kwAnomaProveDelta,
     kwAnomaRandomGeneratorInit,

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)

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

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

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) =>

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
 

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"
 

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

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 :=

tests/Anoma/Compilation/positive/test085/delta.juvix

@@ -24,17 +24,20 @@ 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
     >-> trace (subDelta zeroDelta zeroDelta)
     >-> trace (addDelta zeroDelta zeroDelta)
     >-> proveAction action
     >-> trace (actionDelta action)
+    >-> trace (isCommitment resCommitment)
+    >-> trace (isNullifier resNullifier)
+    >-> trace (isCommitment resNullifier)
+    >-> trace (isNullifier resCommitment)
     >-> actionsDelta [action];