Skip to main content

Aleo Instructions ABNF Specification

This chapter describes Aleo instructions by their formal syntax. The specification of the grammar is derived from the current implementation of the nom parser of Aleo instructions in snarkVM.

The grammar should recognize exactly the same language as the parser. The formulation of the rules for some constructs may not correspond to the parser implementation exactly; this is to highlight more structure to facilitate future changes, or because of inherent differences between the declarative nature of the grammar and the operational nature of the parser.

This grammar currently consists of one level, as opposed to two levels (lexical and syntactic). While two levels are typical for higher-level languages like Leo, one level are workable for lower-level languages like Aleo instructions. By not throwing away whitespace and comment when moving between the two levels, we can (as the current rules do) enforce requirements on where comments and whitespace may occur. The parser also is written according to a single level. All of this may be revisited in the future, if needed.

The grammar should be unambiguous if we take into account the extra-grammatical requirement that the longest match is used, which is a common extra-grammatical requirement, at least in lexical grammars of two-level grammars, but should also work for this one-level grammar. We plan to formally prove this eventually.

The rules below are separated into sections. The sections do not have a very deep significance, but are meant to group related rules. For instance, the first section gives names to characters that could not be otherwise denoted in ABNF strings; the second section categorizes the allowed characters; and so on.


horizontal tab
ht = %x9 ;
line feed
lf = %xA ;
carriage return
cr = %xD ;
space
sp = %x20 ;
double quotes
dq = %x22 ;

visible ascii
visible-ascii = %x21-7E
other ascii
other-ascii = %x0-8 / %xB-C / %xE-1F / %x7F
ascii
ascii = visible-ascii / ht / sp / lf / cr / other-ascii

Go to: cr, ht, lf, other-ascii, sp, visible-ascii;

safe nonascii
safe-nonascii = %x80-2029 / %x202F-2065 / %x206A-D7FF / %xE000-10FFFF
; excludes bidi embeddings/overrides/isolates
; and excludes high/low surrogates
bidi
bidi = %x202A-202E / %x2066-2069
surrogate
surrogate = %xD800-DFFF ; these are disallowed via UTF-8 decoding
nonascii
nonascii = safe-nonascii / bidi / surrogate

Go to: bidi, safe-nonascii, surrogate;

character
character = ascii / nonascii

Go to: ascii, nonascii;


escaped line feed
escaped-lf = "\" lf

Go to: lf;

plain whitespace
plain-ws = ht / sp / lf / cr ; plain (i.e. without escaped-lf) whitespace

Go to: cr, ht, lf, sp;

whitespace
ws = *( 1*plain-ws / escaped-lf ) ; whitespace

comment
comment = line-comment / block-comment

Go to: block-comment, line-comment;

line comment
line-comment = "//" *( escaped-lf / not-lf-or-cr )
not lf or cr
not-lf-or-cr = %x0-9 / %xB-C / %xE-10FFFF ; anything but lf or cr
block comment
block-comment = "/*" rest-of-block-comment

Go to: rest-of-block-comment;

rest of block comment
rest-of-block-comment = "*" rest-of-block-comment-after-star
/ not-star rest-of-block-comment

Go to: not-star, rest-of-block-comment-after-star, rest-of-block-comment;

not star
not-star = %x0-29 / %x2B-10FFFF ; anything but *
rest of block comment after star
rest-of-block-comment-after-star = "/"
/ "*" rest-of-block-comment-after-star
/ not-star-or-slash rest-of-block-comment

Go to: not-star-or-slash, rest-of-block-comment-after-star, rest-of-block-comment;

not star or slash
not-star-or-slash = %x0-29 / %x2B-2E / %x30-10FFFF ; anything but * or /

comments or whitespace
cws = ws *( comment / ws ) ; comments and/or whitespace

Go to: ws;


uppercase letter
uppercase-letter = %x41-5A ; A-Z
lowercase letter
lowercase-letter = %x61-7A ; a-z
letter
letter = uppercase-letter / lowercase-letter

Go to: lowercase-letter, uppercase-letter;


digit
digit = %x30-39 ; 0-9
hex digit
hex-digit = digit / "a" / "b" / "c" / "d" / "e" / "f" ; 0-9 A-F a-f

Go to: digit;


identifier
identifier = 1*letter *( letter / digit / "_" )
program id
program-id = identifier "." identifier

Go to: identifier;

locator
locator = program-id "/" identifier

Go to: identifier, program-id;


register
register = %s"r" 1*digit
register access
register-access = register *( "." identifier )

Go to: register;


signed literal
signed-literal = [ "-" ] 1*( digit *"_" ) signed-type

Go to: signed-type;

unsigned literal
unsigned-literal = [ "-" ] 1*( digit *"_" ) unsigned-type ; remove [ "-" ]

Go to: unsigned-type;

integer literal
integer-literal = signed-literal / unsigned-literal

Go to: signed-literal, unsigned-literal;

field literal
field-literal = [ "-" ] 1*( digit *"_" ) field-type

Go to: field-type;

group literal
group-literal = [ "-" ] 1*( digit *"_" ) group-type

Go to: group-type;

scalar literal
scalar-literal = [ "-" ] 1*( digit *"_" ) scalar-type

Go to: scalar-type;

arithmetic literal
arithmetic-literal = integer-literal
/ field-literal
/ group-literal
/ scalar-literal

Go to: field-literal, group-literal, integer-literal, scalar-literal;


address literal
address-literal = %s"aleo1" 1*( address-char *"_" )
address char
address-char = "0" / "2" / "3" / "4" / "5" / "6" / "7" / "8" / "9"
/ %s"a" / %s"c" / %s"d" / %s"e" / %s"f" / %s"g" / %s"h" / %s"j"
/ %s"k" / %s"l" / %s"m" / %s"n" / %s"p" / %s"q" / %s"r" / %s"s"
/ %s"t" / %s"u" / %s"v" / %s"w" / %s"x" / %s"y" / %s"z"

boolean literal
boolean-literal = %s"true" / %s"false"

string literal
string-literal = dq *string-element dq

Go to: dq;

string element
string-element = not-dq-or-backslash
/ escaped-char
/ escaped-ws

Go to: escaped-char, escaped-ws, not-dq-or-backslash;

not dq or backslash
not-dq-or-backslash = %x0-21 / %x23-5B / %x5D-10FFFF ; anything but " or \
escaped char
escaped-char = "\" ( dq
/ "\"
/ "/"
/ %s"n"
/ %s"r"
/ %s"t"
/ %s"b"
/ %s"f"
/ %s"u" "{" 1*6hex-digit "}" )

Go to: dq;

escaped whitespace
escaped-ws = "\" 1*plain-ws ; should the ws here start with a line terminator?

literal
literal = arithmetic-literal
/ address-literal
/ boolean-literal
/ string-literal

Go to: address-literal, arithmetic-literal, boolean-literal, string-literal;


operand
operand = literal / register-access / %s"self.caller" / program-id

Go to: literal, program-id, register-access;


unsigned type
unsigned-type = %s"u8" / %s"u16" / %s"u32" / %s"u64" / %s"u128"
signed type
signed-type = %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128"
integer type
integer-type = unsigned-type / signed-type

Go to: signed-type, unsigned-type;

field type
field-type = %s"field"
group type
group-type = %s"group"
scalar type
scalar-type = %s"scalar"
arithmetic type
arithmetic-type = integer-type / field-type / group-type / scalar-type

Go to: field-type, group-type, integer-type, scalar-type;

address type
address-type = %s"address"
boolean type
boolean-type = %s"boolean"
string type
string-type = %s"string"
literal type
literal-type = arithmetic-type / address-type / boolean-type / string-type

Go to: address-type, arithmetic-type, boolean-type, string-type;

plaintext type
plaintext-type = literal-type / identifier

Go to: identifier, literal-type;

value type
value-type = ( plaintext-type %s".constant"
/ plaintext-type %s".public"
/ plaintext-type %s".private"
/ identifier %s".record"
/ locator %s".record" )

Go to: identifier, locator, plaintext-type;

finalize type
finalize-type = ( plaintext-type %s".public"
/ identifier %s".record"
/ locator %s".record" )

Go to: identifier, locator, plaintext-type;

record entry type
entry-type = plaintext-type ( %s".constant" / %s".public" / %s".private" )

Go to: plaintext-type;

register type
register-type = ( locator %s".record"
/ identifier %s".record"
/ plaintext-type )

Go to: identifier, locator, plaintext-type;


import
import = cws %s"import" ws program-id ws ";"

Go to: cws, program-id, ws;


mapping
mapping = cws %s"mapping" ws identifier ws ":"
mapping-key
mapping-value

Go to: cws, identifier, mapping-key, mapping-value, ws;

mapping key
mapping-key = cws %s"key" ws identifier ws %s"as" ws finalize-type ws ";"

Go to: cws, finalize-type, identifier, ws;

mapping value
mapping-value = cws %s"value" ws identifier ws %s"as" ws finalize-type ws ";"

Go to: cws, finalize-type, identifier, ws;


interface
interface = cws %s"interface"  ws identifier ws ":" 1*tuple

Go to: cws, identifier, ws;

tuple
tuple = cws identifier ws %s"as" ws plaintext-type ws ";"

Go to: cws, identifier, plaintext-type, ws;


record
record = cws %s"record" ws identifier ws ":"
cws %s"owner" ws %s"as" ws
cws ( %s"address.public" / %s"address.private" ) ws ";"
cws %s"gates" ws %s"as" ws
cws ( %s"u64.public" / %s"u64.private" ) ws ";"
*entry

Go to: cws, identifier, ws;

record entry
entry = cws identifier ws %s"as" ws entry-type ws ";"

Go to: cws, entry-type, identifier, ws;


unary operator
unary-op = %s"abs" / %s"abs.w"
/ %s"double"
/ %s"inv"
/ %s"neg"
/ %s"not"
/ %s"square"
/ %s"sqrt"
binary operator
binary-op = %s"add" / %s"add.w"
/ %s"sub" / %s"sub.w"
/ %s"mul" / %s"mul.w"
/ %s"div" / %s"div.w"
/ %s"rem" / %s"rem.w"
/ %s"mod"
/ %s"pow" / %s"pow.w"
/ %s"shl" / %s"shl.w"
/ %s"shr" / %s"shr.w"
/ %s"and"
/ %s"or"
/ %s"xor"
/ %s"nand"
/ %s"nor"
/ %s"gt"
/ %s"gte"
/ %s"lt"
/ %s"lte"
ternary operator
ternary-op = %s"ternary"
is operator
is-op = %s"is.eq" / %s"is.neq"
assert operator
assert-op = %s"assert.eq" / %s"assert.neq"
commit operator
commit-op = %s"commit.bhp" ( "256" / "512" / "768" / "1024" )
/ %s"commit.ped" ( "64" / "128" )
hash operator
hash-op = %s"hash.bhp" ( "256" / "512" / "768" / "1024" )
/ %s"hash.ped" ( "64" / "128" )
/ %s"hash.psd" ( "2" / "4" / "8" )
unary
unary = unary-op ws ( operand ws ) %s"into" ws register

Go to: operand, register, unary-op, ws;

binary
binary = binary-op ws 2( operand ws ) %s"into" ws register

Go to: register, binary-op, ws;

ternary
ternary = ternary-op ws 3( operand ws ) %s"into" ws register

Go to: register, ternary-op, ws;

is
is = is-op ws operand ws operand ws %s"into" ws register

Go to: is-op, operand, register, ws;

assert
assert = assert-op ws operand ws operand

Go to: assert-op, operand, ws;

commit
commit = commit-op ws operand ws operand ws %s"into" ws register

Go to: commit-op, operand, register, ws;

hash
hash = hash-op ws operand ws %s"into" ws register

Go to: hash-op, operand, register, ws;

cast
cast = %s"cast" 1*( ws operand )
ws %s"into" ws register ws %s"as" ws register-type

Go to: register-type, register, ws;

call
call = %s"call" ws ( locator / identifier ) ws 1*( ws operand )
ws %s"into" ws 1*( ws register )

Go to: identifier, locator, ws;

instruction
instruction = cws
( unary
/ binary
/ ternary
/ is
/ assert
/ commit
/ hash
/ cast
/ call )
ws ";"

Go to: assert, binary, call, cast, commit, cws, hash, is, ternary, unary, ws;

decrement
decrement = cws %s"decrement"
ws identifier "[" ws operand ws "]"
ws %s"by" ws operand ws ";"

Go to: cws, identifier, operand, ws;

increment
increment = cws %s"increment"
ws identifier "[" ws operand ws "]"
ws %s"by" ws operand ws ";"

Go to: cws, identifier, operand, ws;

command
command = decrement / increment / instruction

Go to: decrement, increment, instruction;

finalize command
finalize-command = cws %s"finalize" *( ws operand ) cws ";"

Go to: cws;


closure
closure = cws %s"closure" ws identifier ws ":"
*closure-input
1*instruction
*closure-output

Go to: cws, identifier, ws;

closure input
closure-input = cws %s"input" ws register
ws %s"as" ws register-type ws ";"

Go to: cws, register-type, register, ws;

closure output
closure-output = cws %s"output" ws register-access
ws %s"as" ws register-type ws ";"

Go to: cws, register-access, register-type, ws;


function
function = cws %s"function" ws identifier ws ":"
*function-input
*instruction
*function-output
cws [ finalize-command finalize ]

Go to: cws, finalize-command, finalize, identifier, ws;

function input
function-input = cws %s"input" ws register
ws %s"as" ws value-type ws ";"

Go to: cws, register, value-type, ws;

function output
function-output = cws %s"output" ws register-access
ws %s"as" ws value-type ws ";"

Go to: cws, register-access, value-type, ws;

finalize
finalize = cws %s"finalize" ws identifier ws ":"
*finalize-input
1*command
*finalize-output

Go to: cws, identifier, ws;

finalize input
finalize-input = cws %s"input" ws register
ws %s"as" ws finalize-type ws ";"

Go to: cws, finalize-type, register, ws;

finalize output
finalize-output = cws %s"output" ws register-access
ws %s"as" ws finalize-type ws ";"

Go to: cws, finalize-type, register-access, ws;


program
program = *import
cws %s"program" ws program-id ws ";"
1*( mapping / interface / record / closure / function )
cws