Add frontend support for Anoma Resource Machine builtins

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -117,3 +117,106 @@ checkAnomaSha256 f = do
   unless
     (ftype == (nat_ --> byteArray))
     $ builtinsErrorText l "anomaSha256 must be of type Nat -> ByteArray"
+
+checkResource :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkResource d = do
+  let err = builtinsErrorText (getLoc d)
+  unless (null (d ^. inductiveParameters)) (err "AnomaResource should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "AnomaResource should be in the small universe")
+  unless (length (d ^. inductiveConstructors) == 1) (err "AnomaResource should have exactly one constructor")
+
+checkAction :: (Members '[Error ScoperError] r) => InductiveDef -> Sem r ()
+checkAction d = do
+  let err = builtinsErrorText (getLoc d)
+  unless (null (d ^. inductiveParameters)) (err "AnomaAction should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "AnomaAction should be in the small universe")
+  unless (length (d ^. inductiveConstructors) == 1) (err "AnomaAction should have exactly one constructor")
+
+checkDelta :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
+checkDelta d =
+  unless (isSmallUniverse' (d ^. axiomType)) $
+    builtinsErrorText (getLoc d) "AnomaDelta should be in the small universe"
+
+checkKind :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
+checkKind d =
+  unless (isSmallUniverse' (d ^. axiomType)) $
+    builtinsErrorText (getLoc d) "AnomaDelta should be in the small universe"
+
+checkResourceCommitment :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceCommitment f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper (getLoc f) BuiltinAnomaResource
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (resource --> nat_)) $
+    builtinsErrorText (getLoc f) "resourceCommitment must be of type AnomaResource -> Nat"
+
+checkResourceNullifier :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceNullifier f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper l BuiltinAnomaResource
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (resource --> nat_)) $
+    builtinsErrorText l "resourceNullifier must be of type AnomaResource -> Nat"
+
+checkResourceKind :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceKind f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper l BuiltinAnomaResource
+  kind <- getBuiltinNameScoper l BuiltinAnomaKind
+  unless (f ^. axiomType === (resource --> kind)) $
+    builtinsErrorText l "resourceNullifier must be of type AnomaResource -> Nat"
+
+checkResourceDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceDelta f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper l BuiltinAnomaResource
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === (resource --> delta)) $
+    builtinsErrorText l "resourceDelta must be of type AnomaResource -> AnomaDelta"
+
+checkProveAction :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkProveAction f = do
+  let l = getLoc f
+  action <- getBuiltinNameScoper l BuiltinAnomaAction
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (action --> nat_)) $
+    builtinsErrorText l "proveAction must be of type AnomaAction -> Nat"
+
+checkProveDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkProveDelta f = do
+  let l = getLoc f
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (delta --> nat_)) $
+    builtinsErrorText l "proveDelta must be of type AnomaDelta -> Nat"
+
+checkActionDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkActionDelta f = do
+  let l = getLoc f
+  action <- getBuiltinNameScoper l BuiltinAnomaAction
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === (action --> delta)) $
+    builtinsErrorText l "actionDelta must be of type AnomaAction -> AnomaDelta"
+
+checkActionsDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkActionsDelta f = do
+  let l = getLoc f
+  action <- getBuiltinNameScoper l BuiltinAnomaAction
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  list_ <- getBuiltinNameScoper l BuiltinList
+  unless (f ^. axiomType === (list_ @@ action --> delta)) $
+    builtinsErrorText l "actionsDelta must be of type List AnomaAction -> AnomaDelta"
+
+checkDeltaBinaryOp :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkDeltaBinaryOp f = do
+  let l = getLoc f
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === (delta --> delta --> delta)) $
+    builtinsErrorText l "deltaAdd must be of type AnomaDelta -> AnomaDelta -> AnomaDelta"
+
+checkZeroDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkZeroDelta f = do
+  let l = getLoc f
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === delta) $
+    builtinsErrorText (getLoc f) "zeroDelta must be of Delta"

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

@@ -57,6 +57,8 @@ builtinConstructors = \case
   BuiltinPair -> [BuiltinPairConstr]
   BuiltinPoseidonState -> [BuiltinMkPoseidonState]
   BuiltinEcPoint -> [BuiltinMkEcPoint]
+  BuiltinAnomaResource -> [BuiltinMkAnomaResource]
+  BuiltinAnomaAction -> [BuiltinMkAnomaAction]
 
 data BuiltinInductive
   = BuiltinNat
@@ -67,6 +69,8 @@ data BuiltinInductive
   | BuiltinPair
   | BuiltinPoseidonState
   | BuiltinEcPoint
+  | BuiltinAnomaResource
+  | BuiltinAnomaAction
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinInductive
@@ -85,6 +89,8 @@ instance Pretty BuiltinInductive where
     BuiltinPair -> Str.pair
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
+    BuiltinAnomaResource -> Str.anomaResource
+    BuiltinAnomaAction -> Str.anomaAction
 
 instance Pretty BuiltinConstructor where
   pretty = \case
@@ -101,6 +107,8 @@ instance Pretty BuiltinConstructor where
     BuiltinPairConstr -> Str.pair
     BuiltinMkPoseidonState -> Str.cairoMkPoseidonState
     BuiltinMkEcPoint -> Str.cairoMkEcPoint
+    BuiltinMkAnomaResource -> Str.anomaMkResource
+    BuiltinMkAnomaAction -> Str.anomaMkAction
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -116,6 +124,8 @@ data BuiltinConstructor
   | BuiltinPairConstr
   | BuiltinMkPoseidonState
   | BuiltinMkEcPoint
+  | BuiltinMkAnomaResource
+  | BuiltinMkAnomaAction
   deriving stock (Show, Eq, Ord, Generic, Data)
 
 instance Hashable BuiltinConstructor
@@ -228,6 +238,19 @@ data BuiltinAxiom
   | BuiltinAnomaByteArrayToAnomaContents
   | BuiltinAnomaByteArrayFromAnomaContents
   | BuiltinAnomaSha256
+  | BuiltinAnomaDelta
+  | BuiltinAnomaKind
+  | BuiltinAnomaResourceCommitment
+  | BuiltinAnomaResourceNullifier
+  | BuiltinAnomaResourceKind
+  | BuiltinAnomaResourceDelta
+  | BuiltinAnomaActionDelta
+  | BuiltinAnomaActionsDelta
+  | BuiltinAnomaZeroDelta
+  | BuiltinAnomaAddDelta
+  | BuiltinAnomaSubDelta
+  | BuiltinAnomaProveAction
+  | BuiltinAnomaProveDelta
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -275,6 +298,19 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaByteArrayToAnomaContents -> KNameFunction
     BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction
     BuiltinAnomaSha256 -> KNameFunction
+    BuiltinAnomaDelta -> KNameInductive
+    BuiltinAnomaKind -> KNameInductive
+    BuiltinAnomaResourceCommitment -> KNameFunction
+    BuiltinAnomaResourceNullifier -> KNameFunction
+    BuiltinAnomaResourceKind -> KNameFunction
+    BuiltinAnomaResourceDelta -> KNameFunction
+    BuiltinAnomaActionDelta -> KNameFunction
+    BuiltinAnomaActionsDelta -> KNameFunction
+    BuiltinAnomaZeroDelta -> KNameFunction
+    BuiltinAnomaAddDelta -> KNameFunction
+    BuiltinAnomaSubDelta -> KNameFunction
+    BuiltinAnomaProveAction -> KNameFunction
+    BuiltinAnomaProveDelta -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -329,6 +365,19 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
     BuiltinAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
     BuiltinAnomaSha256 -> Str.anomaSha256
+    BuiltinAnomaDelta -> Str.anomaDelta
+    BuiltinAnomaKind -> Str.anomaKind
+    BuiltinAnomaResourceCommitment -> Str.anomaResourceCommitment
+    BuiltinAnomaResourceNullifier -> Str.anomaResourceNullifier
+    BuiltinAnomaResourceKind -> Str.anomaResourceKind
+    BuiltinAnomaResourceDelta -> Str.anomaResourceDelta
+    BuiltinAnomaActionDelta -> Str.anomaActionDelta
+    BuiltinAnomaActionsDelta -> Str.anomaActionsDelta
+    BuiltinAnomaZeroDelta -> Str.anomaZeroDelta
+    BuiltinAnomaAddDelta -> Str.anomaAddDelta
+    BuiltinAnomaSubDelta -> Str.anomaSubDelta
+    BuiltinAnomaProveDelta -> Str.anomaProveDelta
+    BuiltinAnomaProveAction -> Str.anomaProveAction
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs

@@ -63,6 +63,12 @@ getIntSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinInt
 getPoseidonStateSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
 getPoseidonStateSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinPoseidonState
 
+getAnomaResourceSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getAnomaResourceSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinAnomaResource
+
+getAnomaActionSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getAnomaActionSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinAnomaAction
+
 getEcPointSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
 getEcPointSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinEcPoint
 

src/Juvix/Compiler/Core/Evaluator.hs

@@ -228,6 +228,17 @@ geval opts herr tab env0 = eval' env0
       OpAnomaByteArrayToAnomaContents -> anomaByteArrayToAnomaContents
       OpAnomaByteArrayFromAnomaContents -> anomaByteArrayFromAnomaContents
       OpAnomaSha256 -> anomaSha256
+      OpAnomaResourceCommitment -> normalizeOrUnsupported opcode
+      OpAnomaResourceNullifier -> normalizeOrUnsupported opcode
+      OpAnomaResourceKind -> normalizeOrUnsupported opcode
+      OpAnomaResourceDelta -> normalizeOrUnsupported opcode
+      OpAnomaActionDelta -> normalizeOrUnsupported opcode
+      OpAnomaActionsDelta -> normalizeOrUnsupported opcode
+      OpAnomaProveAction -> normalizeOrUnsupported opcode
+      OpAnomaProveDelta -> normalizeOrUnsupported opcode
+      OpAnomaZeroDelta -> normalizeOrUnsupported opcode
+      OpAnomaAddDelta -> normalizeOrUnsupported opcode
+      OpAnomaSubDelta -> normalizeOrUnsupported opcode
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -384,6 +395,15 @@ geval opts herr tab env0 = eval' env0
                           Exception.throw (EvalError ("assertion failed: " <> printNode val) Nothing)
         {-# INLINE assertOp #-}
 
+        normalizeOrUnsupported :: BuiltinOp -> [Node] -> Node
+        normalizeOrUnsupported op args =
+          if
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                  mkBuiltinApp' op (eval' env <$> args)
+              | otherwise ->
+                  err ("unsupported builtin operation: " <> show op)
+        {-# INLINE normalizeOrUnsupported #-}
+
         anomaGetOp :: [Node] -> Node
         anomaGetOp = unary $ \arg ->
           if

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

@@ -195,6 +195,17 @@ isDebugOp = \case
       OpAnomaSignDetached -> False
       OpAnomaVerifyDetached -> False
       OpAnomaVerifyWithMessage -> False
+      OpAnomaResourceCommitment -> False
+      OpAnomaResourceNullifier -> False
+      OpAnomaResourceKind -> False
+      OpAnomaResourceDelta -> False
+      OpAnomaActionDelta -> False
+      OpAnomaActionsDelta -> False
+      OpAnomaProveAction -> False
+      OpAnomaProveDelta -> False
+      OpAnomaZeroDelta -> False
+      OpAnomaAddDelta -> False
+      OpAnomaSubDelta -> False
       OpEc -> False
       OpFieldAdd -> False
       OpFieldDiv -> False
@@ -482,6 +493,17 @@ builtinOpArgTypes = \case
   OpAnomaByteArrayToAnomaContents -> [mkDynamic']
   OpAnomaByteArrayFromAnomaContents -> [mkTypeInteger', mkTypeInteger']
   OpAnomaSha256 -> [mkTypeInteger']
+  OpAnomaResourceCommitment -> [mkDynamic']
+  OpAnomaResourceNullifier -> [mkDynamic']
+  OpAnomaResourceKind -> [mkDynamic']
+  OpAnomaResourceDelta -> [mkDynamic']
+  OpAnomaActionDelta -> [mkDynamic']
+  OpAnomaActionsDelta -> [mkDynamic']
+  OpAnomaProveAction -> [mkDynamic']
+  OpAnomaProveDelta -> [mkDynamic']
+  OpAnomaZeroDelta -> []
+  OpAnomaAddDelta -> [mkDynamic', mkDynamic']
+  OpAnomaSubDelta -> [mkDynamic', mkDynamic']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

src/Juvix/Compiler/Core/Keywords.hs

@@ -8,13 +8,24 @@ where
 import Juvix.Data.Keyword
 import Juvix.Data.Keyword.All
   ( delimSemicolon,
+    kwAnomaActionDelta,
+    kwAnomaActionsDelta,
+    kwAnomaAddDelta,
     kwAnomaDecode,
     kwAnomaEncode,
+    kwAnomaProveAction,
+    kwAnomaProveDelta,
+    kwAnomaResourceCommitment,
+    kwAnomaResourceDelta,
+    kwAnomaResourceKind,
+    kwAnomaResourceNullifier,
     kwAnomaSha256,
     kwAnomaSign,
     kwAnomaSignDetached,
+    kwAnomaSubDelta,
     kwAnomaVerifyDetached,
     kwAnomaVerifyWithMessage,
+    kwAnomaZeroDelta,
     kwAny,
     kwAssert,
     kwAssign,