This issue proposes the introduction of a builtin Bytes type for use by Anoma and the Core evaluator that represents an array of bytes.
This is desirable for the Anoma backend for two main reasons.
We currently represent arrays of bytes as a Nat in the Anoma backend (an integer atom). This is ambiguous, for example the byte arrays { 0x10 }, { 0x10, 0x00 }, { 0x10, 0x00, 0x00 } (and any byte arrays that differ only by trailing zeroed bytes) are all encoded to the same integer (Anoma uses little endian encoding).
We'd prefer to use a more specific type (than Nat) for values that we want to interpret as bytes (in a Juvix program or on the Anoma stdlib APIs). It doesn't make sense for a user to perform arithmetic on a cryptographic signature for example.
In Anoma we have the following builtin:
axiom anomaSign : {A : Type} -> A -> Nat -> Nat;
This signs a message using a private key, it returns a signed message.
In Juvix programs the private key is provided as a Nat literal, e.g:
The reason Nat is used is because these data are represented as atoms in the nockma backend.
In Juvix programs we would like a more precise type to represent public, private keys and signatures. In Anoma Node these cryptographic functions actually operate on binary atoms.
Bytes builtin Proposal
The builtin bytes type:
builtin bytes
axiom Bytes : Type;
The type of anomaSign would be:
anomaSign : {A : Type} -> Bytes -> Bytes
We need support for byte literals, the following syntax is proposed:
Each element of the Bytes#[] list must be an integer literal (decimal or hex).
It's a compile-time error to use integer literals that don't fit into a byte:
-- error: 300 does not fit into one byte.
err : Bytes := Bytes#[300];
Backend Representation
Core
A new ConstantValue will be added ConstBytes !ByteString.
Nockma
Constant bytes will be transformed to a Nock cell with the head containing the length of the bytes and the tail containing the bytes payload, I.e the integer representing the bytes with little-endian byte ordering.
Calling Anoma stdlib functions in the nockma backend.
Anoma stdlib functions like sign, verify must be passed the the integer representing the bytes payload only (i.e without the length) for public, private key and signature arguments (these have a fixed length). In order to make these calls compatible with the proposed Bytes Nockma representation the payload (i.e the tail of the bytes cell) will be projected before calling the stdlib function.
The sign function returns a bytes payload representing a cryptographic signature. It is known to represent 64 bytes so the backend call will wrap the result in a cell with head value 64.
Native, Cairo
The design of the representation of Bytes is deferred.
This issue proposes the introduction of a builtin
Bytes
type for use by Anoma and the Core evaluator that represents an array of bytes.This is desirable for the Anoma backend for two main reasons.
We currently represent arrays of bytes as a
Nat
in the Anoma backend (an integer atom). This is ambiguous, for example the byte arrays{ 0x10 }
,{ 0x10, 0x00 }
,{ 0x10, 0x00, 0x00 }
(and any byte arrays that differ only by trailing zeroed bytes) are all encoded to the same integer (Anoma uses little endian encoding).We'd prefer to use a more specific type (than
Nat
) for values that we want to interpret as bytes (in a Juvix program or on the Anoma stdlib APIs). It doesn't make sense for a user to perform arithmetic on a cryptographic signature for example.In Anoma we have the following builtin:
This signs a message using a private key, it returns a signed message.
In Juvix programs the private key is provided as a Nat literal, e.g:
The reason
Nat
is used is because these data are represented as atoms in the nockma backend.In Juvix programs we would like a more precise type to represent public, private keys and signatures. In Anoma Node these cryptographic functions actually operate on binary atoms.
Bytes builtin Proposal
The builtin bytes type:
The type of
anomaSign
would be:We need support for byte literals, the following syntax is proposed:
Each element of the
Bytes#[]
list must be an integer literal (decimal or hex).It's a compile-time error to use integer literals that don't fit into a byte:
Backend Representation
Core
A new
ConstantValue
will be addedConstBytes !ByteString
.Nockma
Constant bytes will be transformed to a Nock cell with the head containing the length of the bytes and the tail containing the bytes payload, I.e the integer representing the bytes with little-endian byte ordering.
Calling Anoma stdlib functions in the nockma backend.
Anoma stdlib functions like
sign
,verify
must be passed the the integer representing the bytes payload only (i.e without the length) for public, private key and signature arguments (these have a fixed length). In order to make these calls compatible with the proposedBytes
Nockma representation the payload (i.e the tail of the bytes cell) will be projected before calling the stdlib function.The
sign
function returns a bytes payload representing a cryptographic signature. It is known to represent 64 bytes so the backend call will wrap the result in a cell with head value64
.Native, Cairo
The design of the representation of
Bytes
is deferred.