Add a randomBytes builtin to generate cryptographically secure bytes

[paulcadman]

Depends on

• Add ByteArray builtin and Byte literal #2865

This issue proposes adding a builtin randomBytes function.

--- Generate a given number of cryptographically secure random bytes
builtin
axiom randomBytes : Nat -> Bytes

This is required to populate the rseed and nonce fields of an Anoma Resource. The types of these fields are not yet determined.

Backend Representation

Core

We can use a Haskell library e.g crypto-rng to implement the builtin.

Nockma

We can use the same implementation as Core in the Juvix Nockma evaluator.

We will need a randomBytes implementation in the Anoma Hoon stdlib in order to run programs containing this builtin in the Anoma Nock VM.

Native, Cairo, Risc0

The implementation of randomBytes for the native, Cairo and Risc0 backends is deferred.

[lukaszcz]

On this note, we should add a pragma that would indicate that a certain identifier is "volatile" to prevent the optimisations from moving it around, duplicating and/or merging calls to it (this can happen currently).

[paulcadman]

On this note, we should add a pragma that would indicate that a certain identifier is "volatile" to prevent the optimisations from moving it around, duplicating and/or merging calls to it (this can happen currently).

Could you describe this in more detail? Or raise an issue as it seems important.

[lukaszcz]

Yes, I'll raise an issue

[paulcadman]

Link to discussed issue:

• Add a "volatile" pragma #2907

[heueristik]

Does randomBytes : Nat -> Bytes fit with the arm-transparent definitions

type Nonce := mkNonce {unNonce : Nat};
type RandSeed := mkRandSeed {unRandSeed : Nat};

?

[paulcadman]

Does randomBytes : Nat -> Bytes fit with the arm-transparent definitions

type Nonce := mkNonce {unNonce : Nat};
type RandSeed := mkRandSeed {unRandSeed : Nat};

?

Current state of affairs:

• Anoma Node API for randomBytes is randomBytes (seed width : Nat) -> Nat: https://github.com/anoma/green/blob/b33771e50bcbf4b85a5360c09042f3d9bab28ec6/apps/anoma_lib/lib/examples/enock.ex#L475
• The nonce and rseed fields of a transaction are atoms so we must use Nat, or newtype wrapping a Nat: https://github.com/anoma/green/blob/0c49908623066705041efe8a0937aee4ace4b2c8/hoon/resource-machine.hoon#L25-L26

Consequences:

• The seed argument for randomBytes will have to be passed in to the main function that creates the transaction.
• Because neither the Anoma API randomBytes nor the transaction data structure uses ByteArray it doesn't make sense to use ByteArray in the library. We're better off just using a newtype type Bytes := mkBytes Nat.