use bytes

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -234,8 +234,8 @@ checkAnomaRandomGeneratorInit f = do
   unless (f ^. axiomType === (nat_ --> gen)) $
     builtinsErrorText l "initRandomGenerator must be of type Nat -> AnomaRandomGenerator"
 
-checkAnomaRandomNextBits :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
-checkAnomaRandomNextBits f = do
+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

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

@@ -276,7 +276,7 @@ data BuiltinAxiom
   | BuiltinAnomaProveDelta
   | BuiltinAnomaRandomGenerator
   | BuiltinAnomaRandomGeneratorInit
-  | BuiltinAnomaRandomNextBits
+  | BuiltinAnomaRandomNextBytes
   | BuiltinAnomaRandomSplit
   | BuiltinAnomaIsCommitment
   | BuiltinAnomaIsNullifier
@@ -345,7 +345,7 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaProveDelta -> KNameFunction
     BuiltinAnomaRandomGenerator -> KNameInductive
     BuiltinAnomaRandomGeneratorInit -> KNameFunction
-    BuiltinAnomaRandomNextBits -> KNameFunction
+    BuiltinAnomaRandomNextBytes -> KNameFunction
     BuiltinAnomaRandomSplit -> KNameFunction
     BuiltinAnomaIsCommitment -> KNameFunction
     BuiltinAnomaIsNullifier -> KNameFunction
@@ -360,8 +360,8 @@ instance HasNameKind BuiltinAxiom where
     BuiltinByteArrayFromListByte -> KNameFunction
     BuiltinByteArrayLength -> KNameFunction
     BuiltinAnomaSet -> KNameInductive
-    BuiltinAnomaSetToList -> KNameInductive
-    BuiltinAnomaSetFromList -> KNameInductive
+    BuiltinAnomaSetToList -> KNameFunction
+    BuiltinAnomaSetFromList -> KNameFunction
   getNameKindPretty :: BuiltinAxiom -> NameKind
   getNameKindPretty = getNameKind
 
@@ -421,7 +421,7 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaProveAction -> Str.anomaProveAction
     BuiltinAnomaRandomGenerator -> Str.anomaRandomGenerator
     BuiltinAnomaRandomGeneratorInit -> Str.anomaRandomGeneratorInit
-    BuiltinAnomaRandomNextBits -> Str.anomaRandomNextBits
+    BuiltinAnomaRandomNextBytes -> Str.anomaRandomNextBytes
     BuiltinAnomaRandomSplit -> Str.anomaRandomSplit
     BuiltinAnomaIsCommitment -> Str.anomaIsCommitment
     BuiltinAnomaIsNullifier -> Str.anomaIsNullifier

src/Juvix/Compiler/Core/Evaluator.hs

@@ -240,7 +240,7 @@ geval opts herr tab env0 = eval' env0
       OpAnomaAddDelta -> normalizeOrUnsupported opcode
       OpAnomaSubDelta -> normalizeOrUnsupported opcode
       OpAnomaRandomGeneratorInit -> normalizeOrUnsupported opcode
-      OpAnomaRandomNextBits -> normalizeOrUnsupported opcode
+      OpAnomaRandomNextBytes -> normalizeOrUnsupported opcode
       OpAnomaRandomSplit -> normalizeOrUnsupported opcode
       OpAnomaIsCommitment -> normalizeOrUnsupported opcode
       OpAnomaIsNullifier -> normalizeOrUnsupported opcode

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

@@ -231,7 +231,7 @@ isDebugOp = \case
       OpAnomaAddDelta -> False
       OpAnomaSubDelta -> False
       OpAnomaRandomGeneratorInit -> False
-      OpAnomaRandomNextBits -> False
+      OpAnomaRandomNextBytes -> False
       OpAnomaRandomSplit -> False
       OpAnomaIsCommitment -> False
       OpAnomaIsNullifier -> False
@@ -536,7 +536,7 @@ builtinOpArgTypes = \case
   OpAnomaAddDelta -> [mkDynamic', mkDynamic']
   OpAnomaSubDelta -> [mkDynamic', mkDynamic']
   OpAnomaRandomGeneratorInit -> [mkTypeInteger']
-  OpAnomaRandomNextBits -> [mkTypeInteger', mkTypeRandomGenerator']
+  OpAnomaRandomNextBytes -> [mkTypeInteger', mkTypeRandomGenerator']
   OpAnomaRandomSplit -> [mkTypeRandomGenerator']
   OpAnomaIsCommitment -> [mkTypeInteger']
   OpAnomaIsNullifier -> [mkTypeInteger']

src/Juvix/Compiler/Core/Keywords.hs

@@ -18,7 +18,7 @@ import Juvix.Data.Keyword.All
     kwAnomaProveAction,
     kwAnomaProveDelta,
     kwAnomaRandomGeneratorInit,
-    kwAnomaRandomNextBits,
+    kwAnomaRandomNextBytes,
     kwAnomaRandomSplit,
     kwAnomaResourceCommitment,
     kwAnomaResourceDelta,

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

@@ -52,7 +52,7 @@ data BuiltinOp
   | OpAnomaAddDelta
   | OpAnomaSubDelta
   | OpAnomaRandomGeneratorInit
-  | OpAnomaRandomNextBits
+  | OpAnomaRandomNextBytes
   | OpAnomaRandomSplit
   | OpAnomaIsCommitment
   | OpAnomaIsNullifier
@@ -144,7 +144,7 @@ builtinOpArgsNum = \case
   OpAnomaAddDelta -> 2
   OpAnomaSubDelta -> 2
   OpAnomaRandomGeneratorInit -> 1
-  OpAnomaRandomNextBits -> 2
+  OpAnomaRandomNextBytes -> 2
   OpAnomaRandomSplit -> 1
   OpAnomaIsCommitment -> 1
   OpAnomaIsNullifier -> 1
@@ -213,7 +213,7 @@ builtinIsFoldable = \case
   OpAnomaSubDelta -> False
   OpAnomaSha256 -> False
   OpAnomaRandomGeneratorInit -> False
-  OpAnomaRandomNextBits -> False
+  OpAnomaRandomNextBytes -> False
   OpAnomaRandomSplit -> False
   OpAnomaIsCommitment -> False
   OpAnomaIsNullifier -> False
@@ -257,7 +257,7 @@ builtinsAnoma =
     OpAnomaAddDelta,
     OpAnomaSubDelta,
     OpAnomaRandomGeneratorInit,
-    OpAnomaRandomNextBits,
+    OpAnomaRandomNextBytes,
     OpAnomaRandomSplit,
     OpAnomaSetToList,
     OpAnomaSetFromList

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

@@ -76,7 +76,7 @@ instance PrettyCode BuiltinOp where
     OpAnomaAddDelta -> return primAddDelta
     OpAnomaSubDelta -> return primSubDelta
     OpAnomaRandomGeneratorInit -> return primRandomGeneratorInit
-    OpAnomaRandomNextBits -> return primRandomNextBits
+    OpAnomaRandomNextBytes -> return primRandomNextBytes
     OpAnomaRandomSplit -> return primRandomSplit
     OpAnomaIsCommitment -> return primIsCommitment
     OpAnomaIsNullifier -> return primIsNullifier
@@ -1003,8 +1003,8 @@ primSubDelta = primitive Str.anomaSubDelta
 primRandomGeneratorInit :: Doc Ann
 primRandomGeneratorInit = primitive Str.anomaRandomGeneratorInit
 
-primRandomNextBits :: Doc Ann
-primRandomNextBits = primitive Str.anomaRandomNextBits
+primRandomNextBytes :: Doc Ann
+primRandomNextBytes = primitive Str.anomaRandomNextBytes
 
 primRandomSplit :: Doc Ann
 primRandomSplit = primitive Str.anomaRandomSplit

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

@@ -101,7 +101,7 @@ computeNodeTypeInfo md = umapL go
           OpAnomaAddDelta -> mkDynamic'
           OpAnomaSubDelta -> mkDynamic'
           OpAnomaRandomGeneratorInit -> mkTypeRandomGenerator'
-          OpAnomaRandomNextBits -> mkDynamic'
+          OpAnomaRandomNextBytes -> mkDynamic'
           OpAnomaRandomSplit -> mkDynamic'
           OpAnomaIsCommitment -> mkTypeBool'
           OpAnomaIsNullifier -> mkTypeBool'

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

@@ -693,7 +693,7 @@ builtinInductive a =
         Internal.BuiltinAnomaSubDelta -> Nothing
         Internal.BuiltinAnomaRandomGenerator -> Just (registerInductiveAxiom (Just BuiltinAnomaRandomGenerator) [])
         Internal.BuiltinAnomaRandomGeneratorInit -> Nothing
-        Internal.BuiltinAnomaRandomNextBits -> Nothing
+        Internal.BuiltinAnomaRandomNextBytes -> Nothing
         Internal.BuiltinAnomaRandomSplit -> Nothing
         Internal.BuiltinAnomaIsCommitment -> Nothing
         Internal.BuiltinAnomaIsNullifier -> Nothing
@@ -1008,14 +1008,14 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               natType
               (mkBuiltinApp' OpAnomaRandomGeneratorInit [mkVar' 0])
           )
-      Internal.BuiltinAnomaRandomNextBits -> do
+      Internal.BuiltinAnomaRandomNextBytes -> do
         natType <- getNatType
         registerAxiomDef
           ( mkLambda'
               natType
               ( mkLambda'
                   mkDynamic'
-                  (mkBuiltinApp' OpAnomaRandomNextBits [mkVar' 1, mkVar' 0])
+                  (mkBuiltinApp' OpAnomaRandomNextBytes [mkVar' 1, mkVar' 0])
               )
           )
       Internal.BuiltinAnomaRandomSplit -> do
@@ -1454,15 +1454,14 @@ goApplication a = do
         Just Internal.BuiltinIOSequence -> do
           ioSym <- getIOSymbol
           as <- exprArgs
-          case as of
+          return $ case as of
             (arg1 : arg2 : xs) ->
-              return $
-                mkApps'
-                  ( mkConstr'
-                      (BuiltinTag TagBind)
-                      [arg1, mkLambda' (mkTypeConstr (setInfoName Str.io mempty) ioSym []) (shift 1 arg2)]
-                  )
-                  xs
+              mkApps'
+                ( mkConstr'
+                    (BuiltinTag TagBind)
+                    [arg1, mkLambda' (mkTypeConstr (setInfoName Str.io mempty) ioSym []) (shift 1 arg2)]
+                )
+                xs
             _ -> error "internal to core: >> must be called with 2 arguments"
         Just Internal.BuiltinIOReadline -> app
         Just Internal.BuiltinStringConcat -> app
@@ -1510,7 +1509,7 @@ goApplication a = do
         Just Internal.BuiltinAnomaProveDelta -> app
         Just Internal.BuiltinAnomaRandomGenerator -> app
         Just Internal.BuiltinAnomaRandomGeneratorInit -> app
-        Just Internal.BuiltinAnomaRandomNextBits -> app
+        Just Internal.BuiltinAnomaRandomNextBytes -> app
         Just Internal.BuiltinAnomaRandomSplit -> app
         Just Internal.BuiltinAnomaIsCommitment -> app
         Just Internal.BuiltinAnomaIsNullifier -> app

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

@@ -607,7 +607,7 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwAnomaAddDelta $> OpAnomaAddDelta)
       <|> (kw kwAnomaSubDelta $> OpAnomaSubDelta)
       <|> (kw kwAnomaRandomGeneratorInit $> OpAnomaRandomGeneratorInit)
-      <|> (kw kwAnomaRandomNextBits $> OpAnomaRandomNextBits)
+      <|> (kw kwAnomaRandomNextBytes $> OpAnomaRandomNextBytes)
       <|> (kw kwAnomaRandomSplit $> OpAnomaRandomSplit)
       <|> (kw kwAnomaIsCommitment $> OpAnomaIsCommitment)
       <|> (kw kwAnomaIsNullifier $> OpAnomaIsNullifier)

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

@@ -134,7 +134,7 @@ fromCore fsize tab =
         BuiltinAnomaProveDelta -> False
         BuiltinAnomaRandomGenerator -> False
         BuiltinAnomaRandomGeneratorInit -> False
-        BuiltinAnomaRandomNextBits -> False
+        BuiltinAnomaRandomNextBytes -> False
         BuiltinAnomaRandomSplit -> False
         BuiltinAnomaIsCommitment -> False
         BuiltinAnomaIsNullifier -> False

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

@@ -1145,7 +1145,7 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaProveAction -> checkProveAction d
   BuiltinAnomaRandomGenerator -> checkAnomaRandomGenerator d
   BuiltinAnomaRandomGeneratorInit -> checkAnomaRandomGeneratorInit d
-  BuiltinAnomaRandomNextBits -> checkAnomaRandomNextBits d
+  BuiltinAnomaRandomNextBytes -> checkAnomaRandomNextBytes d
   BuiltinAnomaRandomSplit -> checkAnomaRandomSplit d
   BuiltinAnomaIsCommitment -> checkAnomaIsCommitment d
   BuiltinAnomaIsNullifier -> checkAnomaIsNullifier d

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

@@ -236,6 +236,13 @@ withTemp value f = do
   body' <- local (over compilerStackHeight (+ 1)) $ f (TempRef stackHeight)
   return $ OpPush # value # body'
 
+withTempM ::
+  (Member (Reader CompilerCtx) r) =>
+  Sem r (Term Natural) ->
+  (TempRef -> Sem r (Term Natural)) ->
+  Sem r (Term Natural)
+withTempM valueM f = valueM >>= (`withTemp` f)
+
 -- | Pushes a temporary value onto the subject stack, associates the resulting
 -- stack reference with the next JuvixTree temporary variable, and continues
 -- compilation.
@@ -560,7 +567,7 @@ compile = \case
         Tree.OpAnomaAddDelta -> callRm RmDeltaAdd args
         Tree.OpAnomaSubDelta -> callRm RmDeltaSub args
         Tree.OpAnomaRandomGeneratorInit -> callStdlib StdlibRandomInitGen args
-        Tree.OpAnomaRandomNextBits -> goAnomaRandomNextBits args
+        Tree.OpAnomaRandomNextBytes -> goAnomaRandomNextBytes args
         Tree.OpAnomaRandomSplit -> callStdlib StdlibRandomSplit args
         Tree.OpAnomaIsCommitment -> callRm RmIsCommitment args
         Tree.OpAnomaIsNullifier -> callRm RmIsNullifier args
@@ -697,36 +704,39 @@ compile = \case
         sha256HashLength :: Integer
         sha256HashLength = 32
 
-    goAnomaRandomNextBits :: [Term Natural] -> Sem r (Term Natural)
-    goAnomaRandomNextBits args = case args of
+    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
-              StdlibRandomNextBits
-              [ opAddress "args-g" (argRefAddress ++ [R]),
-                opAddress "numbits" (argRefAddress ++ [L])
-              ]
-          withTemp next $ \nextRef -> do
-            argRefAddress'' <- tempRefPath argsRef
-            numBytes <-
-              callStdlib
-                StdlibDiv
-                [ opAddress "args-n" (argRefAddress'' ++ [L]),
+          withTempM
+            ( callStdlib
+                StdlibMul
+                [ opAddress "args-n" (argRefAddress ++ [L]),
                   nockNatLiteral 8
                 ]
-            withTemp numBytes $ \numBytesRef -> do
-              numBytesRefAddress' <- tempRefPath numBytesRef
-              nextRefPath <- tempRefPath nextRef
-              return
-                ( mkPair
-                    ( mkByteArray
-                        (opAddress "args-n" numBytesRefAddress')
-                        (opAddress "nextbytes-result-fst" (nextRefPath ++ [L]))
-                    )
-                    (opAddress "nextBytes-result-snd" (nextRefPath ++ [R]))
+            )
+            $ \numBitsRef -> do
+              argRefAddress' <- tempRefPath argsRef
+              numBits <- tempRefPath numBitsRef
+              withTempM
+                ( callStdlib
+                    StdlibRandomNextBits
+                    [ opAddress "args-g" numBits,
+                      opAddress "numbits" (argRefAddress' ++ [L])
+                    ]
                 )
+                $ \nextRef -> do
+                  argRefAddress'' <- tempRefPath argsRef
+                  nextRefPath <- tempRefPath nextRef
+                  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:

src/Juvix/Compiler/Tree/Keywords.hs

@@ -22,7 +22,7 @@ import Juvix.Data.Keyword.All
     kwAnomaProveAction,
     kwAnomaProveDelta,
     kwAnomaRandomGeneratorInit,
-    kwAnomaRandomNextBits,
+    kwAnomaRandomNextBytes,
     kwAnomaRandomSplit,
     kwAnomaResourceCommitment,
     kwAnomaResourceDelta,

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

@@ -126,8 +126,8 @@ data AnomaOp
     OpAnomaSubDelta
   | -- | Initialize a pseudorandom number generator
     OpAnomaRandomGeneratorInit
-  | -- | Generate the n random bytes using the pseudorandom number generator
-    OpAnomaRandomNextBits
+  | -- | Generate n random bytes using the pseudorandom number generator
+    OpAnomaRandomNextBytes
   | -- | Split a pseudorandom number generator into two uncorrelated generators
     OpAnomaRandomSplit
   | -- | Returns true if its argument is a commitment

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

@@ -301,7 +301,7 @@ instance PrettyCode AnomaOp where
     OpAnomaAddDelta -> Str.anomaAddDelta
     OpAnomaSubDelta -> Str.anomaSubDelta
     OpAnomaRandomGeneratorInit -> Str.anomaRandomGeneratorInit
-    OpAnomaRandomNextBits -> Str.anomaRandomNextBits
+    OpAnomaRandomNextBytes -> Str.anomaRandomNextBytes
     OpAnomaRandomSplit -> Str.anomaRandomSplit
     OpAnomaIsCommitment -> Str.anomaIsCommitment
     OpAnomaIsNullifier -> Str.anomaIsNullifier

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

@@ -71,7 +71,7 @@ toTreeOp = \case
   Core.OpAnomaAddDelta -> TreeAnomaOp OpAnomaAddDelta
   Core.OpAnomaSubDelta -> TreeAnomaOp OpAnomaSubDelta
   Core.OpAnomaRandomGeneratorInit -> TreeAnomaOp OpAnomaRandomGeneratorInit
-  Core.OpAnomaRandomNextBits -> TreeAnomaOp OpAnomaRandomNextBits
+  Core.OpAnomaRandomNextBytes -> TreeAnomaOp OpAnomaRandomNextBytes
   Core.OpAnomaRandomSplit -> TreeAnomaOp OpAnomaRandomSplit
   Core.OpAnomaIsCommitment -> TreeAnomaOp OpAnomaIsCommitment
   Core.OpAnomaIsNullifier -> TreeAnomaOp OpAnomaIsNullifier

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

@@ -168,7 +168,7 @@ parseAnoma =
     <|> parseAnoma' kwAnomaAddDelta OpAnomaAddDelta
     <|> parseAnoma' kwAnomaSubDelta OpAnomaSubDelta
     <|> parseAnoma' kwAnomaRandomGeneratorInit OpAnomaRandomGeneratorInit
-    <|> parseAnoma' kwAnomaRandomNextBits OpAnomaRandomNextBits
+    <|> parseAnoma' kwAnomaRandomNextBytes OpAnomaRandomNextBytes
     <|> parseAnoma' kwAnomaRandomSplit OpAnomaRandomSplit
     <|> parseAnoma' kwAnomaIsCommitment OpAnomaIsCommitment
     <|> parseAnoma' kwAnomaIsNullifier OpAnomaIsNullifier

src/Juvix/Data/Keyword/All.hs

@@ -568,8 +568,8 @@ kwAnomaSubDelta = asciiKw Str.anomaSubDelta
 kwAnomaRandomGeneratorInit :: Keyword
 kwAnomaRandomGeneratorInit = asciiKw Str.anomaRandomGeneratorInit
 
-kwAnomaRandomNextBits :: Keyword
-kwAnomaRandomNextBits = asciiKw Str.anomaRandomNextBits
+kwAnomaRandomNextBytes :: Keyword
+kwAnomaRandomNextBytes = asciiKw Str.anomaRandomNextBytes
 
 kwAnomaRandomSplit :: Keyword
 kwAnomaRandomSplit = asciiKw Str.anomaRandomSplit

src/Juvix/Extra/Strings.hs

@@ -440,8 +440,8 @@ anomaRandomGenerator = "anoma-random-generator"
 anomaRandomGeneratorInit :: (IsString s) => s
 anomaRandomGeneratorInit = "anoma-random-generator-init"
 
-anomaRandomNextBits :: (IsString s) => s
-anomaRandomNextBits = "anoma-random-next-bits"
+anomaRandomNextBytes :: (IsString s) => s
+anomaRandomNextBytes = "anoma-random-next-bytes"
 
 anomaRandomSplit :: (IsString s) => s
 anomaRandomSplit = "anoma-random-generator-split"