Cairo shielded backend integration (#3357)

This PR adds complier support for the builtins needed to create shielded
transactions.

* Adds the `Json` builtin type with appropriate translation to Nockma.
In Nock, a term/noun has type `json` if it has one of the following
form:
   - `["a" p]` with `p` of type `list json`,
   - `["b" p]` with `p` a boolean atom,
   - `["o" p]` with `p` of type `list (pair string json)`,
   - `["n" p]` with `p` a number atom,
   - `["s" p]` with `p` a string atom.
* Adds the `ComplianceInputs` and `ShieldedTransaction` builtin types,
and the `createFromComplianceInputs` builtin function.

Author: lukaszcz

runtime/c/src/juvix/limits.h

@@ -18,7 +18,9 @@
 // have the value MAX_UIDS.
 #define MAX_UIDS 1048576U
 
-#define BUILTIN_UIDS_NUM 8U
+// Make sure this corresponds to the number of built-in UIDs in
+// Juvix/Compiler/Backend.hs.
+#define BUILTIN_UIDS_NUM 13U
 
 // Maximum number of different user constructors (globally).
 #define MAX_CONSTR_TAGS (MAX_UIDS - BUILTIN_UIDS_NUM)

runtime/c/src/juvix/object/object.h

@@ -154,12 +154,14 @@ STATIC_ASSERT(BUILTIN_UIDS_NUM > UID_READLN);
 
 #define FIRST_USER_UID BUILTIN_UIDS_NUM
 
-#define BUILTIN_UIDS_INFO                                   \
-    {"false", 0, APP_FIXITY}, {"true", 0, APP_FIXITY},      \
-        {"unit", 0, APP_FIXITY}, {"void", 0, APP_FIXITY},   \
-        {"return", 0, APP_FIXITY}, {"bind", 0, APP_FIXITY}, \
-        {"write", 0, APP_FIXITY}, {                         \
-        "readln", 0, APP_FIXITY                             \
+#define BUILTIN_UIDS_INFO                                                 \
+    {"false", 0, APP_FIXITY}, {"true", 0, APP_FIXITY},                    \
+        {"unit", 0, APP_FIXITY}, {"void", 0, APP_FIXITY},                 \
+        {"return", 0, APP_FIXITY}, {"bind", 0, APP_FIXITY},               \
+        {"write", 0, APP_FIXITY}, {"readln", 0, APP_FIXITY},              \
+        {"Json.array", 0, APP_FIXITY}, {"Json.bool", 0, APP_FIXITY},      \
+        {"Json.object", 0, APP_FIXITY}, {"Json.number", 0, APP_FIXITY}, { \
+        "Json.string", 0, APP_FIXITY                                      \
     }
 
 /*************************************************/

src/Juvix/Compiler/Backend.hs

@@ -55,7 +55,7 @@ getLimits tgt debug = case tgt of
         _limitsMaxStackDelta = 16368,
         _limitsMaxFunctionAlloc = 16368,
         _limitsDispatchStackSize = 4,
-        _limitsBuiltinUIDsNum = 8,
+        _limitsBuiltinUIDsNum = 13,
         _limitsSpecialisedApply = 3
       }
   TargetCNative64 ->
@@ -70,7 +70,7 @@ getLimits tgt debug = case tgt of
         _limitsMaxStackDelta = 8184,
         _limitsMaxFunctionAlloc = 8184,
         _limitsDispatchStackSize = 4,
-        _limitsBuiltinUIDsNum = 8,
+        _limitsBuiltinUIDsNum = 13,
         _limitsSpecialisedApply = 3
       }
   TargetCore ->
@@ -93,7 +93,7 @@ getLimits tgt debug = case tgt of
         _limitsMaxStackDelta = 16368,
         _limitsMaxFunctionAlloc = 16368,
         _limitsDispatchStackSize = 4,
-        _limitsBuiltinUIDsNum = 8,
+        _limitsBuiltinUIDsNum = 13,
         _limitsSpecialisedApply = 3
       }
   TargetAnoma ->
@@ -110,7 +110,7 @@ getLimits tgt debug = case tgt of
         _limitsMaxStackDelta = 0, -- irrelevant
         _limitsMaxFunctionAlloc = 0, -- irrelevant
         _limitsDispatchStackSize = 0, -- irrelevant
-        _limitsBuiltinUIDsNum = 8,
+        _limitsBuiltinUIDsNum = 13,
         _limitsSpecialisedApply = 3
       }
   TargetRust ->

src/Juvix/Compiler/Backend/C/Translation/FromReg/Base.hs

@@ -23,6 +23,11 @@ getBuiltinUID = \case
   Reg.TagBind -> 5
   Reg.TagWrite -> 6
   Reg.TagReadLn -> 7
+  Reg.TagJsonArray -> 8
+  Reg.TagJsonBool -> 9
+  Reg.TagJsonObject -> 10
+  Reg.TagJsonNumber -> 11
+  Reg.TagJsonString -> 12
 
 getUID :: Reg.ExtraInfo -> Reg.Tag -> Int
 getUID info tag = case tag of

src/Juvix/Compiler/Backend/Rust/Translation/FromReg/Base.hs

@@ -22,6 +22,11 @@ getBuiltinUID = \case
   Reg.TagBind -> impossible
   Reg.TagWrite -> impossible
   Reg.TagReadLn -> impossible
+  Reg.TagJsonArray -> impossible
+  Reg.TagJsonBool -> impossible
+  Reg.TagJsonObject -> impossible
+  Reg.TagJsonNumber -> impossible
+  Reg.TagJsonString -> impossible
 
 getUID :: Reg.ExtraInfo -> Reg.Tag -> Int
 getUID info tag = case tag of

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -132,6 +132,20 @@ checkAction d = do
   unless (isSmallUniverse' (d ^. inductiveType)) (err "AnomaAction should be in the small universe")
   unless (length (d ^. inductiveConstructors) == 1) (err "AnomaAction should have exactly one constructor")
 
+checkComplianceInputs :: (Members '[Error ScoperError] r) => InductiveDef -> Sem r ()
+checkComplianceInputs d = do
+  let err = builtinsErrorText (getLoc d)
+  unless (null (d ^. inductiveParameters)) (err "ComplianceInputs should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "ComplianceInputs should be in the small universe")
+  unless (length (d ^. inductiveConstructors) == 1) (err "ComplianceInputs should have exactly one constructor")
+
+checkShieldedTransaction :: (Members '[Error ScoperError] r) => InductiveDef -> Sem r ()
+checkShieldedTransaction d = do
+  let err = builtinsErrorText (getLoc d)
+  unless (null (d ^. inductiveParameters)) (err "ShieldedTransaction should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "ShieldedTransaction should be in the small universe")
+  unless (length (d ^. inductiveConstructors) == 1) (err "ShieldedTransaction should have exactly one constructor")
+
 checkDelta :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
 checkDelta d =
   unless (isSmallUniverse' (d ^. axiomType)) $
@@ -268,6 +282,16 @@ checkAnomaIsNullifier f = do
   unless (f ^. axiomType === (nat_ --> bool_)) $
     builtinsErrorText l "isNullifier must be of type Nat -> Bool"
 
+checkAnomaCreateFromComplianceInputs :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkAnomaCreateFromComplianceInputs f = do
+  let l = getLoc f
+  json_ <- getBuiltinNameScoper l BuiltinJson
+  list_ <- getBuiltinNameScoper l BuiltinList
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  shieldedTransaction <- getBuiltinNameScoper l BuiltinAnomaShieldedTransaction
+  unless (f ^. axiomType === (list_ @@ json_ --> list_ @@ byteArray --> list_ @@ json_ --> list_ @@ byteArray --> list_ @@ json_ --> shieldedTransaction)) $
+    builtinsErrorText l "createFromComplianceInputs must be of type: List Json -> List ByteArray -> List Json -> List ByteArray -> List Json -> ShieldedTransaction"
+
 checkAnomaSet :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
 checkAnomaSet t = do
   let ty = t ^. axiomType

src/Juvix/Compiler/Builtins/Json.hs

@@ -0,0 +1,67 @@
+module Juvix.Compiler.Builtins.Json where
+
+import Juvix.Compiler.Internal.Builtins
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+checkJsonDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkJsonDef d = do
+  let err :: forall a. Text -> Sem r a
+      err = builtinsErrorText (getLoc d)
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "Json should be in the small universe")
+  unless (null (d ^. inductiveParameters)) (err "Json should have no type parameters")
+  case d ^. inductiveConstructors of
+    [constrJsonArray, constrJsonBool, constrJsonObject, constrJsonNumber, constrJsonString] ->
+      checkJsonArray constrJsonArray
+        >> checkJsonBool constrJsonBool
+        >> checkJsonObject constrJsonObject
+        >> checkJsonNumber constrJsonNumber
+        >> checkJsonString constrJsonString
+    _ -> err "Json should have exactly five constructors"
+
+checkJsonArray :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
+checkJsonArray d@ConstructorDef {..} = do
+  let ty = _inductiveConstructorType
+  json_ <- getBuiltinNameScoper (getLoc d) BuiltinJson
+  list_ <- getBuiltinNameScoper (getLoc d) BuiltinList
+  let cty = list_ @@ json_ --> json_
+  unless (ty === cty) $
+    builtinsErrorText (getLoc d) "json array constructor has the wrong type"
+
+checkJsonBool :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
+checkJsonBool d@ConstructorDef {..} = do
+  let ty = _inductiveConstructorType
+  json_ <- getBuiltinNameScoper (getLoc d) BuiltinJson
+  bool_ <- getBuiltinNameScoper (getLoc d) BuiltinBool
+  let cty = bool_ --> json_
+  unless (ty === cty) $
+    builtinsErrorText (getLoc d) "json bool constructor has the wrong type"
+
+checkJsonObject :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
+checkJsonObject d@ConstructorDef {..} = do
+  let ty = _inductiveConstructorType
+  json_ <- getBuiltinNameScoper (getLoc d) BuiltinJson
+  list_ <- getBuiltinNameScoper (getLoc d) BuiltinList
+  pair_ <- getBuiltinNameScoper (getLoc d) BuiltinPair
+  string_ <- getBuiltinNameScoper (getLoc d) BuiltinString
+  let cty = list_ @@ (pair_ @@ string_ @@ json_) --> json_
+  unless (ty === cty) $
+    builtinsErrorText (getLoc d) "json object constructor has the wrong type"
+
+checkJsonNumber :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
+checkJsonNumber d@ConstructorDef {..} = do
+  let ty = _inductiveConstructorType
+  json_ <- getBuiltinNameScoper (getLoc d) BuiltinJson
+  nat_ <- getBuiltinNameScoper (getLoc d) BuiltinNat
+  let cty = nat_ --> json_
+  unless (ty === cty) $
+    builtinsErrorText (getLoc d) "json number constructor has the wrong type"
+
+checkJsonString :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
+checkJsonString d@ConstructorDef {..} = do
+  let ty = _inductiveConstructorType
+  json_ <- getBuiltinNameScoper (getLoc d) BuiltinJson
+  string_ <- getBuiltinNameScoper (getLoc d) BuiltinString
+  let cty = string_ --> json_
+  unless (ty === cty) $
+    builtinsErrorText (getLoc d) "json string constructor has the wrong type"

src/Juvix/Compiler/Builtins/List.hs

@@ -13,7 +13,6 @@ checkListDef d = do
   param :: VarName <- case d ^. inductiveParameters of
     [v] -> return (v ^. inductiveParamName)
     _ -> err "List should have exactly one type parameter"
-
   case d ^. inductiveConstructors of
     [c1, c2] -> checkNil param c1 >> checkCons param c2
     _ -> err "List should have exactly two constructors"

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

@@ -55,10 +55,13 @@ builtinConstructors = \case
   BuiltinList -> [BuiltinListNil, BuiltinListCons]
   BuiltinMaybe -> [BuiltinMaybeNothing, BuiltinMaybeJust]
   BuiltinPair -> [BuiltinPairConstr]
+  BuiltinJson -> [BuiltinJsonArray, BuiltinJsonBool, BuiltinJsonObject, BuiltinJsonNumber, BuiltinJsonString]
   BuiltinPoseidonState -> [BuiltinMkPoseidonState]
   BuiltinEcPoint -> [BuiltinMkEcPoint]
   BuiltinAnomaResource -> [BuiltinMkAnomaResource]
   BuiltinAnomaAction -> [BuiltinMkAnomaAction]
+  BuiltinAnomaComplianceInputs -> [BuiltinMkAnomaComplianceInputs]
+  BuiltinAnomaShieldedTransaction -> [BuiltinMkAnomaShieldedTransaction]
   BuiltinEq -> [BuiltinMkEq]
   BuiltinOrd -> [BuiltinMkOrd]
   BuiltinOrdering -> [BuiltinOrderingLT, BuiltinOrderingEQ, BuiltinOrderingGT]
@@ -70,13 +73,16 @@ data BuiltinInductive
   | BuiltinList
   | BuiltinMaybe
   | BuiltinPair
+  | BuiltinJson
   | BuiltinEq
   | BuiltinOrd
   | BuiltinOrdering
   | BuiltinPoseidonState
   | BuiltinEcPoint
   | BuiltinAnomaResource
   | BuiltinAnomaAction
+  | BuiltinAnomaComplianceInputs
+  | BuiltinAnomaShieldedTransaction
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinInductive
@@ -93,13 +99,16 @@ instance Pretty BuiltinInductive where
     BuiltinList -> Str.list
     BuiltinMaybe -> Str.maybe_
     BuiltinPair -> Str.pair
+    BuiltinJson -> Str.json
     BuiltinEq -> Str.eq
     BuiltinOrd -> Str.ord
     BuiltinOrdering -> Str.ordering
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
     BuiltinAnomaResource -> Str.anomaResource
     BuiltinAnomaAction -> Str.anomaAction
+    BuiltinAnomaComplianceInputs -> Str.anomaComplianceInputs
+    BuiltinAnomaShieldedTransaction -> Str.anomaShieldedTransaction
 
 instance Pretty BuiltinConstructor where
   pretty = \case
@@ -114,10 +123,17 @@ instance Pretty BuiltinConstructor where
     BuiltinMaybeNothing -> Str.nothing
     BuiltinMaybeJust -> Str.just
     BuiltinPairConstr -> Str.pair
+    BuiltinJsonArray -> Str.jsonArray
+    BuiltinJsonBool -> Str.jsonBool
+    BuiltinJsonObject -> Str.jsonObject
+    BuiltinJsonNumber -> Str.jsonNumber
+    BuiltinJsonString -> Str.jsonString
     BuiltinMkPoseidonState -> Str.cairoMkPoseidonState
     BuiltinMkEcPoint -> Str.cairoMkEcPoint
     BuiltinMkAnomaResource -> Str.anomaMkResource
     BuiltinMkAnomaAction -> Str.anomaMkAction
+    BuiltinMkAnomaComplianceInputs -> Str.anomaMkComplianceInputs
+    BuiltinMkAnomaShieldedTransaction -> Str.anomaMkShieldedTransaction
     BuiltinMkEq -> Str.mkEq
     BuiltinMkOrd -> Str.mkOrd
     BuiltinOrderingLT -> Str.lt
@@ -141,10 +157,17 @@ data BuiltinConstructor
   | BuiltinMaybeNothing
   | BuiltinMaybeJust
   | BuiltinPairConstr
+  | BuiltinJsonArray
+  | BuiltinJsonBool
+  | BuiltinJsonObject
+  | BuiltinJsonNumber
+  | BuiltinJsonString
   | BuiltinMkPoseidonState
   | BuiltinMkEcPoint
   | BuiltinMkAnomaResource
   | BuiltinMkAnomaAction
+  | BuiltinMkAnomaComplianceInputs
+  | BuiltinMkAnomaShieldedTransaction
   deriving stock (Show, Eq, Ord, Generic, Data)
 
 instance Hashable BuiltinConstructor
@@ -280,6 +303,7 @@ data BuiltinAxiom
   | BuiltinAnomaRandomSplit
   | BuiltinAnomaIsCommitment
   | BuiltinAnomaIsNullifier
+  | BuiltinAnomaCreateFromComplianceInputs
   | BuiltinAnomaSet
   | BuiltinAnomaSetToList
   | BuiltinAnomaSetFromList
@@ -350,6 +374,7 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaRandomSplit -> KNameFunction
     BuiltinAnomaIsCommitment -> KNameFunction
     BuiltinAnomaIsNullifier -> KNameFunction
+    BuiltinAnomaCreateFromComplianceInputs -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -427,6 +452,7 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaRandomSplit -> Str.anomaRandomSplit
     BuiltinAnomaIsCommitment -> Str.anomaIsCommitment
     BuiltinAnomaIsNullifier -> Str.anomaIsNullifier
+    BuiltinAnomaCreateFromComplianceInputs -> Str.anomaCreateFromComplianceInputs
     BuiltinAnomaSet -> Str.anomaSet
     BuiltinAnomaSetToList -> Str.anomaSetToList
     BuiltinAnomaSetFromList -> Str.anomaSetFromList

src/Juvix/Compiler/Core/Evaluator.hs

@@ -245,6 +245,7 @@ geval opts herr tab env0 = eval' env0
       OpAnomaRandomSplit -> normalizeOrUnsupported opcode
       OpAnomaIsCommitment -> normalizeOrUnsupported opcode
       OpAnomaIsNullifier -> normalizeOrUnsupported opcode
+      OpAnomaCreateFromComplianceInputs -> normalizeOrUnsupported opcode
       OpAnomaSetToList -> normalizeOrUnsupported opcode
       OpAnomaSetFromList -> normalizeOrUnsupported opcode
       OpPoseidonHash -> poseidonHashOp