Support random API from the Anoma stdlib (#3129)

This PR adds frontend support for the Anoma Random API:

The frontend builtin APIs are:

```
builtin anoma-random-generator
axiom RandomGenerator : Type;

builtin anoma-random-generator-init
axiom randomGeneratorInit : Nat -> RandomGenerator;

builtin anoma-random-generator-split
axiom randomGeneratorSplit : RandomGenerator
  -> Pair RandomGenerator RandomGenerator;

builtin anoma-random-next-bytes
axiom randomNextBytes : Nat
  -> RandomGenerator
  -> Pair ByteArray RandomGenerator;
```

### Nockma Evaluator

The Nockma evaluator intercepts the corresponding Anoma random stdlib
calls using the
[System.Random](https://hackage.haskell.org/package/random-1.2.1.2/docs/System-Random.html)
API. The implementation uses the
[splitmix](https://hackage.haskell.org/package/splitmix-0.1.0.5/docs/System-Random-SplitMix.html)
generator directly because it has an API to destructure the generator
into a pair of integers. We can use this to serialise the generator.



* Closes https://github.com/anoma/juvix/issues/2902

package.yaml

@@ -90,11 +90,13 @@ dependencies:
   - prettyprinter-ansi-terminal == 1.1.*
   - primitive == 0.9.*
   - process == 1.6.*
+  - random == 1.2.*
   - safe == 0.3.*
   - scientific == 0.3.*
   - singletons == 3.0.*
   - singletons-base == 3.3.*
   - singletons-th == 3.3.*
+  - splitmix == 0.1.*
   - stm == 2.5.*
   - Stream == 0.4.*
   - string-interpolate == 0.3.*

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -220,3 +220,34 @@ checkZeroDelta f = do
   delta <- getBuiltinNameScoper l BuiltinAnomaDelta
   unless (f ^. axiomType === delta) $
     builtinsErrorText (getLoc f) "zeroDelta must be of Delta"
+
+checkAnomaRandomGenerator :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
+checkAnomaRandomGenerator d =
+  unless (isSmallUniverse' (d ^. axiomType)) $
+    builtinsErrorText (getLoc d) "AnomaRandomGenerator should be in the small universe"
+
+checkAnomaRandomGeneratorInit :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkAnomaRandomGeneratorInit f = do
+  let l = getLoc f
+  gen <- getBuiltinNameScoper l BuiltinAnomaRandomGenerator
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (nat_ --> gen)) $
+    builtinsErrorText l "initRandomGenerator must be of type Nat -> AnomaRandomGenerator"
+
+checkAnomaRandomNextBytes :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkAnomaRandomNextBytes f = do
+  let l = getLoc f
+  gen <- getBuiltinNameScoper l BuiltinAnomaRandomGenerator
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  bytearray <- getBuiltinNameScoper l BuiltinByteArray
+  pair_ <- getBuiltinNameScoper l BuiltinPair
+  unless (f ^. axiomType === (nat_ --> gen --> (pair_ @@ bytearray @@ gen))) $
+    builtinsErrorText l "nextBytes must be of type Nat -> AnomaRandomGenerator -> Pair ByteArray AnomaRandomGenerator"
+
+checkAnomaRandomSplit :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkAnomaRandomSplit f = do
+  let l = getLoc f
+  gen <- getBuiltinNameScoper l BuiltinAnomaRandomGenerator
+  pair_ <- getBuiltinNameScoper l BuiltinPair
+  unless (f ^. axiomType === (gen --> pair_ @@ gen @@ gen)) $
+    builtinsErrorText l "randomSplit must be of type AnomaRandomGenerator -> Pair AnomaRandomGenerator AnomaRandomGenerator"

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

@@ -251,6 +251,10 @@ data BuiltinAxiom
   | BuiltinAnomaSubDelta
   | BuiltinAnomaProveAction
   | BuiltinAnomaProveDelta
+  | BuiltinAnomaRandomGenerator
+  | BuiltinAnomaRandomGeneratorInit
+  | BuiltinAnomaRandomNextBytes
+  | BuiltinAnomaRandomSplit
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -311,6 +315,10 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaSubDelta -> KNameFunction
     BuiltinAnomaProveAction -> KNameFunction
     BuiltinAnomaProveDelta -> KNameFunction
+    BuiltinAnomaRandomGenerator -> KNameInductive
+    BuiltinAnomaRandomGeneratorInit -> KNameFunction
+    BuiltinAnomaRandomNextBytes -> KNameFunction
+    BuiltinAnomaRandomSplit -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -378,6 +386,10 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaSubDelta -> Str.anomaSubDelta
     BuiltinAnomaProveDelta -> Str.anomaProveDelta
     BuiltinAnomaProveAction -> Str.anomaProveAction
+    BuiltinAnomaRandomGenerator -> Str.anomaRandomGenerator
+    BuiltinAnomaRandomGeneratorInit -> Str.anomaRandomGeneratorInit
+    BuiltinAnomaRandomNextBytes -> Str.anomaRandomNextBytes
+    BuiltinAnomaRandomSplit -> Str.anomaRandomSplit
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint

src/Juvix/Compiler/Core/Evaluator.hs

@@ -239,6 +239,9 @@ geval opts herr tab env0 = eval' env0
       OpAnomaZeroDelta -> normalizeOrUnsupported opcode
       OpAnomaAddDelta -> normalizeOrUnsupported opcode
       OpAnomaSubDelta -> normalizeOrUnsupported opcode
+      OpAnomaRandomGeneratorInit -> normalizeOrUnsupported opcode
+      OpAnomaRandomNextBytes -> normalizeOrUnsupported opcode
+      OpAnomaRandomSplit -> normalizeOrUnsupported opcode
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp

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

@@ -208,6 +208,12 @@ mkTypeByteArray i = mkTypePrim i PrimByteArray
 mkTypeByteArray' :: Type
 mkTypeByteArray' = mkTypeByteArray Info.empty
 
+mkTypeRandomGenerator :: Info -> Type
+mkTypeRandomGenerator i = mkTypePrim i PrimRandomGenerator
+
+mkTypeRandomGenerator' :: Type
+mkTypeRandomGenerator' = mkTypeRandomGenerator Info.empty
+
 mkDynamic :: Info -> Type
 mkDynamic i = NDyn (DynamicTy i)
 

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

@@ -206,6 +206,9 @@ isDebugOp = \case
       OpAnomaZeroDelta -> False
       OpAnomaAddDelta -> False
       OpAnomaSubDelta -> False
+      OpAnomaRandomGeneratorInit -> False
+      OpAnomaRandomNextBytes -> False
+      OpAnomaRandomSplit -> False
       OpEc -> False
       OpFieldAdd -> False
       OpFieldDiv -> False
@@ -504,6 +507,9 @@ builtinOpArgTypes = \case
   OpAnomaZeroDelta -> []
   OpAnomaAddDelta -> [mkDynamic', mkDynamic']
   OpAnomaSubDelta -> [mkDynamic', mkDynamic']
+  OpAnomaRandomGeneratorInit -> [mkTypeInteger']
+  OpAnomaRandomNextBytes -> [mkTypeInteger', mkTypeRandomGenerator']
+  OpAnomaRandomSplit -> [mkTypeRandomGenerator']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []

src/Juvix/Compiler/Core/Keywords.hs

@@ -15,6 +15,9 @@ import Juvix.Data.Keyword.All
     kwAnomaEncode,
     kwAnomaProveAction,
     kwAnomaProveDelta,
+    kwAnomaRandomGeneratorInit,
+    kwAnomaRandomNextBytes,
+    kwAnomaRandomSplit,
     kwAnomaResourceCommitment,
     kwAnomaResourceDelta,
     kwAnomaResourceKind,

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -51,6 +51,9 @@ data BuiltinOp
   | OpAnomaZeroDelta
   | OpAnomaAddDelta
   | OpAnomaSubDelta
+  | OpAnomaRandomGeneratorInit
+  | OpAnomaRandomNextBytes
+  | OpAnomaRandomSplit
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -136,6 +139,9 @@ builtinOpArgsNum = \case
   OpAnomaZeroDelta -> 0
   OpAnomaAddDelta -> 2
   OpAnomaSubDelta -> 2
+  OpAnomaRandomGeneratorInit -> 1
+  OpAnomaRandomNextBytes -> 2
+  OpAnomaRandomSplit -> 1
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -198,6 +204,9 @@ builtinIsFoldable = \case
   OpAnomaAddDelta -> False
   OpAnomaSubDelta -> False
   OpAnomaSha256 -> False
+  OpAnomaRandomGeneratorInit -> False
+  OpAnomaRandomNextBytes -> False
+  OpAnomaRandomSplit -> False
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
@@ -234,7 +243,10 @@ builtinsAnoma =
     OpAnomaProveDelta,
     OpAnomaZeroDelta,
     OpAnomaAddDelta,
-    OpAnomaSubDelta
+    OpAnomaSubDelta,
+    OpAnomaRandomGeneratorInit,
+    OpAnomaRandomNextBytes,
+    OpAnomaRandomSplit
   ]
 
 builtinsUInt8 :: [BuiltinOp]

src/Juvix/Compiler/Core/Language/Primitives.hs

@@ -16,6 +16,7 @@ data Primitive
   | PrimString
   | PrimField
   | PrimByteArray
+  | PrimRandomGenerator
   deriving stock (Eq, Generic)
 
 primitiveUInt8 :: Primitive

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -75,6 +75,9 @@ instance PrettyCode BuiltinOp where
     OpAnomaZeroDelta -> return primZeroDelta
     OpAnomaAddDelta -> return primAddDelta
     OpAnomaSubDelta -> return primSubDelta
+    OpAnomaRandomGeneratorInit -> return primRandomGeneratorInit
+    OpAnomaRandomNextBytes -> return primRandomNextBytes
+    OpAnomaRandomSplit -> return primRandomSplit
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -105,6 +108,7 @@ instance PrettyCode Primitive where
     PrimBool _ -> return $ annotate (AnnKind KNameInductive) (pretty ("Bool" :: String))
     PrimString -> return $ annotate (AnnKind KNameInductive) (pretty ("String" :: String))
     PrimByteArray -> return $ annotate (AnnKind KNameInductive) (pretty ("ByteArray" :: String))
+    PrimRandomGenerator -> return $ annotate (AnnKind KNameInductive) (pretty ("RandomGenerator" :: String))
 
 ppName :: NameKind -> Text -> Sem r (Doc Ann)
 ppName kind name = return $ annotate (AnnKind kind) (pretty name)
@@ -954,6 +958,15 @@ primAddDelta = primitive Str.anomaAddDelta
 primSubDelta :: Doc Ann
 primSubDelta = primitive Str.anomaSubDelta
 
+primRandomGeneratorInit :: Doc Ann
+primRandomGeneratorInit = primitive Str.anomaRandomGeneratorInit
+
+primRandomNextBytes :: Doc Ann
+primRandomNextBytes = primitive Str.anomaRandomNextBytes
+
+primRandomSplit :: Doc Ann
+primRandomSplit = primitive Str.anomaRandomSplit
+
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon
 

src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs

@@ -61,6 +61,7 @@ checkCairo md = do
           PrimField {} -> True
           PrimString {} -> False
           PrimByteArray {} -> False
+          PrimRandomGenerator {} -> False
 
         isRecordOrList :: TypeConstr -> Bool
         isRecordOrList TypeConstr {..} = case ii ^. inductiveBuiltin of

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -92,6 +92,9 @@ computeNodeTypeInfo md = umapL go
           OpAnomaZeroDelta -> mkDynamic'
           OpAnomaAddDelta -> mkDynamic'
           OpAnomaSubDelta -> mkDynamic'
+          OpAnomaRandomGeneratorInit -> mkTypeRandomGenerator'
+          OpAnomaRandomNextBytes -> mkDynamic'
+          OpAnomaRandomSplit -> mkDynamic'
           OpPoseidonHash -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect poseidon builtin application"

src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs

@@ -21,6 +21,7 @@ convertNode md = umap go
           Just (BuiltinTypeAxiom BuiltinField) -> mkTypeField'
           Just (BuiltinTypeAxiom BuiltinByte) -> mkTypeUInt8'
           Just (BuiltinTypeAxiom BuiltinByteArray) -> mkTypeByteArray'
+          Just (BuiltinTypeAxiom BuiltinAnomaRandomGenerator) -> mkTypeRandomGenerator'
           _ -> node
         where
           ii = lookupInductiveInfo md _typeConstrSymbol

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -662,6 +662,10 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaZeroDelta -> return ()
       Internal.BuiltinAnomaAddDelta -> return ()
       Internal.BuiltinAnomaSubDelta -> return ()
+      Internal.BuiltinAnomaRandomGenerator -> registerInductiveAxiom (Just BuiltinAnomaRandomGenerator) []
+      Internal.BuiltinAnomaRandomGeneratorInit -> return ()
+      Internal.BuiltinAnomaRandomNextBytes -> return ()
+      Internal.BuiltinAnomaRandomSplit -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -952,6 +956,30 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
                   (mkBuiltinApp' OpAnomaSubDelta [mkVar' 1, mkVar' 0])
               )
           )
+      Internal.BuiltinAnomaRandomGenerator -> return ()
+      Internal.BuiltinAnomaRandomGeneratorInit -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              natType
+              (mkBuiltinApp' OpAnomaRandomGeneratorInit [mkVar' 0])
+          )
+      Internal.BuiltinAnomaRandomNextBytes -> do
+        natType <- getNatType
+        registerAxiomDef
+          ( mkLambda'
+              natType
+              ( mkLambda'
+                  mkDynamic'
+                  (mkBuiltinApp' OpAnomaRandomNextBytes [mkVar' 1, mkVar' 0])
+              )
+          )
+      Internal.BuiltinAnomaRandomSplit -> do
+        registerAxiomDef
+          ( mkLambda'
+              mkDynamic'
+              (mkBuiltinApp' OpAnomaRandomSplit [mkVar' 0])
+          )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
         psSym <- getPoseidonStateSymbol
@@ -1407,6 +1435,10 @@ goApplication a = do
         Just Internal.BuiltinAnomaSubDelta -> app
         Just Internal.BuiltinAnomaProveAction -> app
         Just Internal.BuiltinAnomaProveDelta -> app
+        Just Internal.BuiltinAnomaRandomGenerator -> app
+        Just Internal.BuiltinAnomaRandomGeneratorInit -> app
+        Just Internal.BuiltinAnomaRandomNextBytes -> app
+        Just Internal.BuiltinAnomaRandomSplit -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -596,6 +596,9 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwAnomaZeroDelta $> OpAnomaZeroDelta)
       <|> (kw kwAnomaAddDelta $> OpAnomaAddDelta)
       <|> (kw kwAnomaSubDelta $> OpAnomaSubDelta)
+      <|> (kw kwAnomaRandomGeneratorInit $> OpAnomaRandomGeneratorInit)
+      <|> (kw kwAnomaRandomNextBytes $> OpAnomaRandomNextBytes)
+      <|> (kw kwAnomaRandomSplit $> OpAnomaRandomSplit)
 
   args <- P.many (atom varsNum vars)
   return $ mkBuiltinApp' op args

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -125,6 +125,10 @@ fromCore fsize tab =
         BuiltinAnomaZeroDelta -> False
         BuiltinAnomaProveAction -> False
         BuiltinAnomaProveDelta -> False
+        BuiltinAnomaRandomGenerator -> False
+        BuiltinAnomaRandomGeneratorInit -> False
+        BuiltinAnomaRandomNextBytes -> False
+        BuiltinAnomaRandomSplit -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -616,6 +616,10 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaSubDelta -> checkDeltaBinaryOp d
   BuiltinAnomaProveDelta -> checkProveDelta d
   BuiltinAnomaProveAction -> checkProveAction d
+  BuiltinAnomaRandomGenerator -> checkAnomaRandomGenerator d
+  BuiltinAnomaRandomGeneratorInit -> checkAnomaRandomGeneratorInit d
+  BuiltinAnomaRandomNextBytes -> checkAnomaRandomNextBytes d
+  BuiltinAnomaRandomSplit -> checkAnomaRandomSplit d
   BuiltinPoseidon -> checkPoseidon d
   BuiltinEcOp -> checkEcOp d
   BuiltinRandomEcPoint -> checkRandomEcPoint d

src/Juvix/Compiler/Nockma/AnomaLib.hs

@@ -92,6 +92,18 @@ anomaLibPath = \case
                 1
               ]
       |]
+    -- Obtained from the urbit dojo using:
+    --
+    -- =>  rm  !=  |=  [seed=@]  ~(. og seed)
+    StdlibRandomInitGen -> [nock| [8 [1 0] [1 8 [9 47 0 31] 10 [6 0 14] 0 2] 0 1] |]
+    -- obtained from the urbit dojo using:
+    --
+    -- =>  rm  !=  |=  [rng=* width=@]   (raws:`_og`rng width)
+    StdlibRandomNextBytes -> [nock| [8 [1 0 0] [1 8 [7 [0 12] 9 4 0 1] 9 2 10 [6 0 29] 0 2] 0 1] |]
+    -- obtained from the urbit dojo using:
+    --
+    -- =>  rm  !=  |=  [rng=*]  split:`_og`rng
+    StdlibRandomSplit -> [nock| [8 [1 0] [1 7 [0 6] 9 21 0 1] 0 1] |]
   AnomaLibFunction (AnomaRmFunction f) -> case f of
     RmCommit -> [nock| [9 94 0 1] |]
     RmNullify -> [nock| [9 350 0 1] |]

src/Juvix/Compiler/Nockma/AnomaLib/Base.hs

@@ -34,6 +34,9 @@ data StdlibFunction
   | StdlibLengthBytes
   | StdlibCurry
   | StdlibSha256
+  | StdlibRandomInitGen
+  | StdlibRandomNextBytes
+  | StdlibRandomSplit
   deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
 
 instance Hashable StdlibFunction
@@ -108,6 +111,9 @@ instance Pretty StdlibFunction where
     StdlibLengthBytes -> "length-bytes"
     StdlibCurry -> "curry"
     StdlibSha256 -> "sha256"
+    StdlibRandomInitGen -> "random-init"
+    StdlibRandomNextBytes -> "random-next-bytes"
+    StdlibRandomSplit -> "random-split"
 
 instance Pretty RmFunction where
   pretty = \case

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -18,6 +18,8 @@ import Juvix.Compiler.Nockma.Evaluator.Storage
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty
 import Juvix.Prelude hiding (Atom, Path)
+import System.Random qualified as R
+import System.Random.SplitMix qualified as R
 
 newtype OpCounts = OpCounts
   { _opCountsMap :: HashMap NockOp Int
@@ -275,7 +277,49 @@ evalProfile inistack initerm =
               StdlibSha256 -> case args' of
                 TermAtom a -> TermAtom <$> goSha256 a
                 _ -> error "StdlibSha256 expects to be called with an atom"
+              StdlibRandomInitGen -> case args' of
+                TermAtom a -> goRandomInitGen a
+                _ -> error "StdlibRandomInitGen must be called with an atom"
+              StdlibRandomNextBytes -> case args' of
+                TermCell (Cell (TermAtom n) g) -> goRandomNextBytes n g
+                _ -> error "StdlibRandomNextBytes must be called with a cell containing an atom and a term"
+              StdlibRandomSplit -> goRandomSplit args'
           where
+            serializeSMGen :: R.SMGen -> Term a
+            serializeSMGen s =
+              let (seed, gamma) = R.unseedSMGen s
+                  seedAtom = TermAtom (mkEmptyAtom (fromIntegral seed))
+                  gammaAtom = TermAtom (mkEmptyAtom (fromIntegral gamma))
+               in TermCell (Cell seedAtom gammaAtom)
+
+            deserializeSMGen :: Term a -> Sem r (R.SMGen)
+            deserializeSMGen = \case
+              TermCell (Cell (TermAtom s) (TermAtom g)) -> do
+                seed :: Word64 <- fromIntegral <$> nockNatural s
+                gamma :: Word64 <- fromIntegral <$> nockNatural g
+                return (R.seedSMGen' (seed, gamma))
+              _ -> error "deserializeSMGen must be called with a cell containing two atoms"
+
+            goRandomNextBytes :: Atom a -> Term a -> Sem r (Term a)
+            goRandomNextBytes n g = do
+              gen <- deserializeSMGen g
+              len :: Int <- fromIntegral <$> nockNatural n
+              let (bs, newGen) = R.genByteString len gen
+                  newGenTerm = serializeSMGen newGen
+              atomBs <- TermAtom <$> byteStringToAtom bs
+              return (TermCell (Cell atomBs newGenTerm))
+
+            goRandomInitGen :: Atom a -> Sem r (Term a)
+            goRandomInitGen s = do
+              seed :: Word64 <- fromIntegral <$> nockNatural s
+              return (serializeSMGen (R.mkSMGen seed))
+
+            goRandomSplit :: Term a -> Sem r (Term a)
+            goRandomSplit gt = do
+              gen <- deserializeSMGen gt
+              let (g1, g2) = R.splitSMGen gen
+              return (TermCell (Cell (serializeSMGen g1) (serializeSMGen g2)))
+
             goCat :: Atom a -> Atom a -> Sem r (Term a)
             goCat arg1 arg2 = TermAtom . setAtomHint AtomHintString <$> atomConcatenateBytes arg1 arg2
 

src/Juvix/Compiler/Nockma/Translation/FromTree.hs

@@ -582,6 +582,9 @@ compile = \case
         Tree.OpAnomaZeroDelta -> rmValue RmZeroDelta
         Tree.OpAnomaAddDelta -> callRm RmDeltaAdd args
         Tree.OpAnomaSubDelta -> callRm RmDeltaSub args
+        Tree.OpAnomaRandomGeneratorInit -> callStdlib StdlibRandomInitGen args
+        Tree.OpAnomaRandomNextBytes -> goAnomaRandomNextBytes args
+        Tree.OpAnomaRandomSplit -> callStdlib StdlibRandomSplit args
 
     goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural)
     goByteArrayOp Tree.NodeByteArray {..} = do
@@ -643,6 +646,9 @@ compile = \case
     mkByteArray :: Term Natural -> Term Natural -> Term Natural
     mkByteArray len payload = len # payload
 
+    mkPair :: Term Natural -> Term Natural -> Term Natural
+    mkPair t1 t2 = t1 # t2
+
     goAnomaVerifyDetached :: [Term Natural] -> Sem r (Term Natural)
     goAnomaVerifyDetached = \case
       [sig, message, pubKey] -> do
@@ -708,6 +714,30 @@ compile = \case
         sha256HashLength :: Integer
         sha256HashLength = 64
 
+    goAnomaRandomNextBytes :: [Term Natural] -> Sem r (Term Natural)
+    goAnomaRandomNextBytes args = case args of
+      [n, g] -> do
+        withTemp (n # g) $ \argsRef -> do
+          argRefAddress <- tempRefPath argsRef
+          next <-
+            callStdlib
+              StdlibRandomNextBytes
+              [ opAddress "args-n" (argRefAddress ++ [L]),
+                opAddress "args-g" (argRefAddress ++ [R])
+              ]
+          withTemp next $ \nextRef -> do
+            nextRefPath <- tempRefPath nextRef
+            argRefAddress' <- tempRefPath argsRef
+            return
+              ( mkPair
+                  ( mkByteArray
+                      (opAddress "args-n" (argRefAddress' ++ [L]))
+                      (opAddress "nextbytes-result-fst" (nextRefPath ++ [L]))
+                  )
+                  (opAddress "nextBytes-result-snd" (nextRefPath ++ [R]))
+              )
+      _ -> impossible
+
     -- Conceptually this function is:
     -- anomaDecode <$> verify signedMessage pubKey
     --

src/Juvix/Compiler/Tree/Extra/Type.hs

@@ -67,6 +67,7 @@ isSubtype ty1 ty2 =
         (TyString, TyString) -> True
         (TyField, TyField) -> True
         (TyByteArray, TyByteArray) -> True
+        (TyRandomGenerator, TyRandomGenerator) -> True
         (TyUnit, TyUnit) -> True
         (TyVoid, TyVoid) -> True
         (TyInductive {}, TyInductive {}) -> ty1 == ty2
@@ -82,6 +83,8 @@ isSubtype ty1 ty2 =
         (_, TyField) -> False
         (TyByteArray, _) -> False
         (_, TyByteArray) -> False
+        (TyRandomGenerator, _) -> False
+        (_, TyRandomGenerator) -> False
         (TyBool {}, _) -> False
         (_, TyBool {}) -> False
         (TyFun {}, _) -> False
@@ -127,6 +130,7 @@ unifyTypes ty1 ty2 =
         (TyString, TyString) -> return TyString
         (TyField, TyField) -> return TyField
         (TyByteArray, TyByteArray) -> return TyByteArray
+        (TyRandomGenerator, TyRandomGenerator) -> return TyRandomGenerator
         (TyUnit, TyUnit) -> return TyUnit
         (TyVoid, TyVoid) -> return TyVoid
         (TyInductive {}, TyInductive {})
@@ -143,6 +147,8 @@ unifyTypes ty1 ty2 =
         (_, TyField) -> err
         (TyByteArray, _) -> err
         (_, TyByteArray) -> err
+        (TyRandomGenerator, _) -> err
+        (_, TyRandomGenerator) -> err
         (TyBool {}, _) -> err
         (_, TyBool {}) -> err
         (TyFun {}, _) -> err

src/Juvix/Compiler/Tree/Keywords.hs

@@ -19,6 +19,9 @@ import Juvix.Data.Keyword.All
     kwAnomaGet,
     kwAnomaProveAction,
     kwAnomaProveDelta,
+    kwAnomaRandomGeneratorInit,
+    kwAnomaRandomNextBytes,
+    kwAnomaRandomSplit,
     kwAnomaResourceCommitment,
     kwAnomaResourceDelta,
     kwAnomaResourceKind,

src/Juvix/Compiler/Tree/Language/Builtins.hs

@@ -124,4 +124,10 @@ data AnomaOp
     OpAnomaAddDelta
   | -- | Subtract Deltas
     OpAnomaSubDelta
+  | -- | Initialize a pseudorandom number generator
+    OpAnomaRandomGeneratorInit
+  | -- | Generate the n random bytes using the pseudorandom number generator
+    OpAnomaRandomNextBytes
+  | -- | Split a pseudorandom number generator into two uncorrelated generators
+    OpAnomaRandomSplit
   deriving stock (Eq, Show)

src/Juvix/Compiler/Tree/Language/Type.hs

@@ -9,6 +9,7 @@ data Type
   | TyString
   | TyField
   | TyByteArray
+  | TyRandomGenerator
   | TyUnit
   | TyVoid
   | TyInductive TypeInductive
@@ -83,6 +84,7 @@ instance HasAtomicity Type where
     TyUnit -> Atom
     TyVoid -> Atom
     TyByteArray -> Atom
+    TyRandomGenerator -> Atom
     TyInductive x -> atomicity x
     TyConstr x -> atomicity x
     TyFun x -> atomicity x

src/Juvix/Compiler/Tree/Pretty/Base.hs

@@ -143,6 +143,8 @@ instance PrettyCode Type where
       return $ annotate (AnnKind KNameInductive) Str.field
     TyByteArray {} ->
       return $ annotate (AnnKind KNameInductive) Str.byteArray
+    TyRandomGenerator {} ->
+      return $ annotate (AnnKind KNameInductive) Str.randomGenerator
     TyBool {} ->
       return $ annotate (AnnKind KNameInductive) Str.bool
     TyString ->
@@ -298,6 +300,9 @@ instance PrettyCode AnomaOp where
     OpAnomaZeroDelta -> Str.anomaZeroDelta
     OpAnomaAddDelta -> Str.anomaAddDelta
     OpAnomaSubDelta -> Str.anomaSubDelta
+    OpAnomaRandomGeneratorInit -> Str.anomaRandomGeneratorInit
+    OpAnomaRandomNextBytes -> Str.anomaRandomNextBytes
+    OpAnomaRandomSplit -> Str.anomaRandomSplit
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case

src/Juvix/Compiler/Tree/Translation/FromCore.hs

@@ -70,6 +70,9 @@ toTreeOp = \case
   Core.OpAnomaZeroDelta -> TreeAnomaOp OpAnomaZeroDelta
   Core.OpAnomaAddDelta -> TreeAnomaOp OpAnomaAddDelta
   Core.OpAnomaSubDelta -> TreeAnomaOp OpAnomaSubDelta
+  Core.OpAnomaRandomGeneratorInit -> TreeAnomaOp OpAnomaRandomGeneratorInit
+  Core.OpAnomaRandomNextBytes -> TreeAnomaOp OpAnomaRandomNextBytes
+  Core.OpAnomaRandomSplit -> TreeAnomaOp OpAnomaRandomSplit
   -- TreeCairoOp
   Core.OpPoseidonHash -> TreeCairoOp OpCairoPoseidon
   Core.OpEc -> TreeCairoOp OpCairoEc
@@ -382,6 +385,8 @@ convertPrimitiveType = \case
     TyField
   Core.PrimByteArray ->
     TyByteArray
+  Core.PrimRandomGenerator ->
+    TyRandomGenerator
 
 -- | `convertNestedType` ensures that the conversion of a type with Dynamic in the
 -- target is curried. The result of `convertType 0 ty` is always uncurried.

src/Juvix/Compiler/Tree/Translation/FromSource.hs

@@ -167,6 +167,9 @@ parseAnoma =
     <|> parseAnoma' kwAnomaZeroDelta OpAnomaZeroDelta
     <|> parseAnoma' kwAnomaAddDelta OpAnomaAddDelta
     <|> parseAnoma' kwAnomaSubDelta OpAnomaSubDelta
+    <|> parseAnoma' kwAnomaRandomGeneratorInit OpAnomaRandomGeneratorInit
+    <|> parseAnoma' kwAnomaRandomNextBytes OpAnomaRandomNextBytes
+    <|> parseAnoma' kwAnomaRandomSplit OpAnomaRandomSplit
 
 parseAnoma' ::
   (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) =>

src/Juvix/Data/Keyword/All.hs

@@ -535,6 +535,15 @@ kwAnomaAddDelta = asciiKw Str.anomaAddDelta
 kwAnomaSubDelta :: Keyword
 kwAnomaSubDelta = asciiKw Str.anomaSubDelta
 
+kwAnomaRandomGeneratorInit :: Keyword
+kwAnomaRandomGeneratorInit = asciiKw Str.anomaRandomGeneratorInit
+
+kwAnomaRandomNextBytes :: Keyword
+kwAnomaRandomNextBytes = asciiKw Str.anomaRandomNextBytes
+
+kwAnomaRandomSplit :: Keyword
+kwAnomaRandomSplit = asciiKw Str.anomaRandomSplit
+
 delimBraceL :: Keyword
 delimBraceL = mkDelim Str.braceL
 

src/Juvix/Extra/Strings.hs

@@ -197,6 +197,9 @@ byteArrayFromListByte = "bytearray-from-list-byte"
 byteArrayLength :: (IsString s) => s
 byteArrayLength = "bytearray-length"
 
+randomGenerator :: (IsString s) => s
+randomGenerator = "randomgenerator"
+
 nat :: (IsString s) => s
 nat = "nat"
 
@@ -431,6 +434,18 @@ anomaProveDelta = "anoma-prove-delta"
 anomaProveAction :: (IsString s) => s
 anomaProveAction = "anoma-prove-action"
 
+anomaRandomGenerator :: (IsString s) => s
+anomaRandomGenerator = "anoma-random-generator"
+
+anomaRandomGeneratorInit :: (IsString s) => s
+anomaRandomGeneratorInit = "anoma-random-generator-init"
+
+anomaRandomNextBytes :: (IsString s) => s
+anomaRandomNextBytes = "anoma-random-next-bytes"
+
+anomaRandomSplit :: (IsString s) => s
+anomaRandomSplit = "anoma-random-generator-split"
+
 builtinSeq :: (IsString s) => s
 builtinSeq = "seq"
 

test/Anoma/Compilation/Positive.hs

@@ -667,5 +667,16 @@ allTests =
             [nock| 478793196187462788804451 |],
             [nock| 418565088612 |],
             [nock| 0 |]
+          ],
+      mkAnomaCallTest
+        "Test086: Anoma Random"
+        $(mkRelDir ".")
+        $(mkRelFile "test086.juvix")
+        []
+        $ checkOutput
+          [ [nock| [2 30764] |],
+            [nock| [3 10689019] |],
+            [nock| [2 20159] |],
+            [nock| [4 4187579825] |]
           ]
     ]

test/Nockma/Eval/Positive.hs

@@ -53,6 +53,7 @@ allTests =
     [ testGroup "Unit" (map mkNockmaTest unitTests),
       testGroup "Juvix calling convention" (map mkNockmaTest juvixCallingConventionTests),
       testGroup "Anoma calling convention" (map mkNockmaTest anomaCallingConventionTests),
+      testGroup "Anoma stldib intercept-only" (map mkNockmaTest anomaStdlibInterceptOnlyTests),
       testGroup "Anoma serialization tests" (map mkNockmaTest serializationTests)
     ]
   where
@@ -399,6 +400,33 @@ juvixCallingConventionTests =
            compilerTestM "zero-delta == 0" (rmValue RmZeroDelta) (eqNock [nock| 0 |])
          ]
 
+-- These tests can only be run with stdlib interception as running the raw nock code is too slow
+anomaStdlibInterceptOnlyTests :: [Test]
+anomaStdlibInterceptOnlyTests =
+  [True]
+    <**> [ compilerTestM
+             "call next bytes in sequence"
+             ( do
+                 gen <- callStdlib StdlibRandomInitGen [nockNatLiteral 777]
+                 rgen1 <- callStdlib StdlibRandomNextBytes [nockNatLiteral 1, gen]
+                 rgen2 <- callStdlib StdlibRandomNextBytes [nockNatLiteral 1, rgen1 >># OpAddress # [R]]
+                 return ((rgen1 >># OpAddress # [L]) # (rgen2 >># OpAddress # [L]))
+             )
+             (eqNock [nock| [44 251] |]),
+           compilerTestM
+             "call next bytes on each generator returned by split"
+             ( do
+                 gen <- callStdlib StdlibRandomInitGen [nockNatLiteral 777]
+                 g1g2 <- callStdlib StdlibRandomSplit [gen]
+                 n1 <- callStdlib StdlibRandomNextBytes [nockNatLiteral 1, g1g2 >># OpAddress # [L]]
+                 n2 <- callStdlib StdlibRandomNextBytes [nockNatLiteral 1, g1g2 >># OpAddress # [R]]
+                 return ((n1 >># OpAddress # [L]) # (n2 >># OpAddress # [L]))
+             )
+             ( eqNock
+                 [nock| [102 42] |]
+             )
+         ]
+
 unitTests :: [Test]
 unitTests =
   [ test "address" [nock| [0 1] |] [nock| [[@ R] [@ L]] |] (eqNock [nock| [1 0] |]),

tests/Anoma/Compilation/positive/test086.juvix

@@ -0,0 +1,39 @@
+module test086;
+
+import Stdlib.Prelude open;
+import Stdlib.Debug.Trace open;
+
+builtin bytearray
+axiom ByteArray : Type;
+
+builtin bytearray-length
+axiom bytearrayLength : ByteArray -> Nat;
+
+builtin anoma-random-generator
+axiom RandomGenerator : Type;
+
+builtin anoma-random-generator-init
+axiom randomGeneratorInit : Nat -> RandomGenerator;
+
+builtin anoma-random-generator-split
+axiom randomGeneratorSplit : RandomGenerator
+  -> Pair RandomGenerator RandomGenerator;
+
+builtin anoma-random-next-bytes
+axiom randomNextBytes : Nat
+  -> RandomGenerator
+  -> Pair ByteArray RandomGenerator;
+
+main : ByteArray :=
+  let
+    gen : RandomGenerator := randomGeneratorInit 777;
+    next1 : Pair ByteArray RandomGenerator := randomNextBytes 2 gen;
+    next2 : Pair ByteArray RandomGenerator := randomNextBytes 3 (snd next1);
+    split : Pair RandomGenerator RandomGenerator :=
+      randomGeneratorSplit (snd next2);
+    next3 : Pair ByteArray RandomGenerator := randomNextBytes 2 (snd split);
+    next4 : Pair ByteArray RandomGenerator := randomNextBytes 4 (fst split);
+  in trace (fst next1)
+    >-> trace (fst next2)
+    >-> trace (fst next3)
+    >-> fst next4;