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