Compact reference
Compact is a strongly statically typed, bounded smart contract language, designed to be used in combination with TypeScript for writing smart contracts for the three-part structure of Midnight, where contracts have the following components:
- a replicated component on a public ledger
- a zero-knowledge circuit component, confidentially proving the correctness of the former
- a local, off-chain component that can perform arbitrary code
Each contract in Compact can have four kinds of code:
- type declarations, to support all of the following
- declarations of the data that the contract stores in the public ledger
- declarations of
witness
functions, to be supplied in TypeScript circuit
definitions, that serve as the operational core of a smart contract
A contract can also include code from external files, and it can declare and import modules.
Like TypeScript, Compact is an eager call-by-value language.
Types
Compact is statically typed: every expression in a Compact program has a static type. Circuits and witnesses require a type annotation on each of their parameters, and they require a return type annotation. Constant binding statements can have an optional type annotation.
The language is strongly typed: the compiler will reject programs that do not type check. It will reject programs where a circuit or witness is called with incorrectly typed arguments. If a constant binding statement has a type annotation, the program will be rejected if the type of the constant initializer expression does not match the type annotation.
Types consist of built-in primitive types, user-defined types defined in the program, and generic parameters of generic modules, structures, and circuits.
Primitive types
The following are the primitive types of Compact:
-
Boolean
is the type of boolean values. There are only two values ofBoolean
type. They are the values of the expressionstrue
andfalse
. -
Uint<m..n>
, wherem
is the literal0
or a generic parameter in scope and bound to0
, and wheren
is a natural number literal or a generic parameter in scope, is the type of bounded unsigned integer values between0
andn
, both inclusive. (The lower bound is currently required to be0
.)Uint
types with different bounds0..n
are different types, although one may be a subtype of the other. In practice, there is a (large) maximum unsigned integer value determined by the zero-knowledge proving system. The Compact implementation will signal an error if aUint
type exceeds this maximum value. -
Uint<n>
, wheren
is a non-zero natural number literal or a generic parameter in scope and bound to a non-zero natural number, is the type of sized unsigned integer values with binary representations using up ton
bits. This is the same type asUint<0..m>
wherem
is equal to(2^n)-1
. Sized integer types can be seen as a convenience for programmers.Uint<32>
, for example, can be more obvious and less error-prone than the equivalentUint<0..4294967295>
. Any Compact program that uses sized integer types can be rewritten to one that uses only bounded integer types. -
Field
is the type of elements in the scalar prime field of the zero-knowledge proving system. -
Void
is the return type of circuits and witnesses that do not return a useful value. It can be used as a return type annotation. It cannot be used as a parameter type annotation, as a constant binding statement type annotation, or as a generic argument for specializing a generic type. -
Bytes<n>
, wheren
is a natural number literal or else a generic parameter in scope, is the type of byte array values of lengthn
.Bytes
types with different lengths are different types.Bytes
types are used in the Compact standard library for hashing. String literals in Compact also have aBytes
type, wheren
is the number of bytes in the UTF-8 encoding of the string. -
Vector<n, T>
, wheren
is a natural number literal or else a generic parameter in scope andT
is a non-void type or else a generic parameter in scope, is the type of vector values of lengthn
with elements of typeT
.Vector
types with different lengths or different element types are different types, although one may be a subtype of the other. -
Opaque<s>
, wheres
is a string literal, is the type of opaque values with tags
. The syntax of string literals in Compact is the same as in TypeScript.Opaque
types with different tags are different types. Opaque values can be manipulated in witnesses but they are opaque to circuits. They are represented in circuits as their hash. The allowed tags are currently only"string"
and"Uint8Array"
.
User-defined types
Users can define three kinds of types themselves: structures, enumerations, and contracts.
Structure types
Structure types are defined by a declaration beginning with the keyword
struct
. Here are some examples:
struct Thing {
triple: Vector<3, Field>,
flag: Boolean,
}
struct NumberAnd<T> {
num: Uint<32>;
item: T
}
A non-generic structure declaration introduces a named structure type, such as
Thing
in the first example above. Each non-generic structure declaration
introduces a distinct type, even when the content of the structure is identical
to another.
Structure declarations can also be generic structure declarations, such as
NumberAnd
in the second example above. They have a non-empty list of
comma-separated generic parameter names enclosed in square brackets. The generic
parameters of a generic structure declaration are in scope in its body.
Generic structure declarations do not introduce a type. To be used as a type,
they must be specialized by providing a comma-separated list of generic
arguments, e.g., NumberAnd<Uint<8>>
. Generic arguments must be non-void
types, natural number literals, or a generic parameter in scope. Generic
structures must be fully specialized: the number of generic arguments must match
the number of generic parameters.
- Specializations of the same generic structure to the same types are the same type.
- Specializations of the same generic structure to different types are different types.
- Specializations of different generic structures are always different types, even if the specializations are structurally equivalent.
- Specializations of generic structures are always different from non-generic structure types, even if the specialization is structurally equivalent to the non-generic type.
A structure declaration has a sequence of named fields which can be separated either by commas or by semicolons. Comma and semicolon separators cannot be mixed within a single structure declaration. A trailing separator is allowed, but not required.
Each structure field must have a type annotation.
A structure declaration implicitly introduces a constructor with the same
name. The arguments to the constructor are required to be in the same order and
have the same types as the corresponding field type annotations. Generic
structure declarations introduce generic constructors, which must be fully
specialized to non-void types to be invoked. Constructors are invoked with
either spread syntax or positional assignment,
so the constructors for the examples above could be invoked as
Thing {[0, 1, 2], true}
and NumberAnd<Uint<8>> {0, 255}
.
Structures may not contain fields of the same type as the structure, either directly or indirectly. For example, the Compact compiler rejects the following pair of declarations:
struct Even {
predecessor: Odd
}
struct Odd {
predecessor: Even
}
Enumeration types
Enumeration types are defined by a declaration beginning with the keyword
enum
. Here is an example:
enum Fruit { apple, pear, plum }
An enumeration declaration introduces a named enumeration type, such as Fruit
in the example above. Each enumeration declaration introduces a distinct type.
An enumeration declaration has a sequence of named values separated by commas. A trailing separator is allowed but not required.
In the example above, the type Fruit
has three values: Fruit.apple
,
Fruit.pear
, and Fruit.plum
.
Contract types
As of this writing, declarations of contracts and the cross-contract calls they support are
not yet fully implemented, but the keyword contract
used to declare contracts is reserved
for this use.
Generic parameter references
Generic parameters are declared in generic module declarations, generic structure
type declarations, generic circuit definitions, and generic witness declarations.
For generic modules, they are in scope within the module.
For generic structures, they are in scope for the structure's fields.
For generic circuits, they are in scope in the circuit's
parameters, its return type annotation, and its body. In
these scopes, a reference to a generic parameter (that is not otherwise shadowed by
some other identifier binding) is either a type or a natural-number size.
Subtyping
There is a subtyping relation on Compact types. Informally, if a type T
is a
subtype of a type S
then every value of type T
is also a value of type S
(equivalently, S
is a supertype of T
). In that case, Compact allows
implicitly using a value of type T
where a value of type S
is expected,
without any programmer-supplied conversion.
Subtyping is defined by the following rules:
-
Any type
T
is a subtype of itself (subtyping is reflexive) -
Uint<0..n>
is a subtype ofUint<0..m>
ifn
is less thanm
-
Uint<0..n>
is a subtype ofField
for alln
-
Vector<n, T>
is a subtype ofVector<m, S>
ifn
equalsm
andT
is a subtype ofS
A circuit or witness can be called with argument expressions whose types are subtypes of the corresponding parameter type annotations. A constant binding statement with a type annotation can be initialized with an expression whose type is a subtype of the type annotation.
Default values
Every non-void type in Compact has a default value of that type. The default values are as follows:
Boolean
: the value of the literalfalse
Uint<0..n>
andUint<n>
:0
Field
:0
Bytes<n>
: the byte array of lengthn
with all zero bytesVector<n, T>
: the vector of lengthn
with all default values of typeT
Opaque<"string">
: an empty string, i.e.,""
Opaque<"Uint8Array">
: a zero-lengthUint8Array
, i.e.,new Uint8Array(0)
- structure types: the struct with all fields set to the default value of their type
- enumeration types: the first value listed in the declaration
Representations in TypeScript
Compact's primitive types are represented in TypeScript as follows:
Boolean
-boolean
Void
-void
Field
-bigint
with runtime bounds checksUint<n>
/Uint<0..n>
-bigint
with runtime bounds checksBytes<n>
-Uint8Array
with runtime length checksVector<n, T>
-T[]
(with the TypeScript representation ofT
), with runtime length checksOpaque<"string">
-string
Opaque<"Uint8Array">
-Uint8Array
User-defined types are represented in TypeScript as follows:
enum
instances - anumber
with runtime membership checksstruct
instances with fieldsa: A, b: B, ...
- an object{ a: A, b: B, ... }
whereA
,B
, ... are the TypeScript representations of the Compact types.
Note that other Opaque
types are currently not supported.
Include files
Compact supports code separation and namespaces through separate files and modules. The most basic of these is the statement
include "path/to/file";
which may appear at the top level of a source file or module. When encountered,
the Compact compiler will search for a Compact source file at
path/to/file.compact
in the current directory and then
relative to any of the directories in the
:
-separated environment variable COMPACT_PATH
.
This file must be found and will be included
verbatim in place of the include
statement.
Modules, exports, and imports
A module is a collection of definitions whose namespace is hidden from surrounding code. A module is defined with
module Mod1 {
...
}
module Mod2<T> {
...
}
By default, identifiers defined within the body of a module are
visible only within the module, i.e., they are not exported from
the module. Any identifier defined at or imported into the top
level of a module can be exported from the module in one of two
ways: (1) by prefixing the definition with the export
keyword,
or by listing the identifier in a separate export
declaration.
For example, the following module exports G
and S
but not F
.
module M {
export { G };
export struct S { x: Uint<16>, y: Boolean }
circuit F(x: S): Boolean {
return S.y;
}
circuit G(x: S): Uint<16> {
return F(x) ? S.x : 0;
}
}
A module can be imported into another definition scope, bringing all its exported entries into that scope, potentially with a prefix. For instance:
module Runner {
export circuit run(): Void {}
}
import Runner;
// run is now in scope
import Runner prefix SomePrefix_;
// SomePrefix_run is now in scope
module Identity<T> {
export { id }
circuit id(x: T): T {
return x;
}
}
import Identity<Field>;
// id is now in scope, with Field as type T
Compact's standard library can be imported by import CompactStandardLibrary
.
The standard library defines a number of useful types and circuits along with
ledger ADTs such as Counter
, Map
, and MerkleTree
.
When importing module M
, if the program does not contain a visible module definition
the compiler looks in the file system in the relative path of the current directory for M.compact
.
In the case where a module is defined in a different program (file), the program must only contain
a top-level module definition. Otherwise, the compiler throws a static error stating that the program
does not contain a single module definition. For example, the program M.compact
below defines
a module:
module M {
export { F };
export struct S { x: Uint<16>, y: Boolean }
circuit F(x: S): Boolean {
return S.y;
}
}
// circuit cant_exists() : Void {}
// If cant_exists is uncommented, the compiler will throw an error when compiling
// test.compact
Then, test.compact
imports M
:
//module M {
// export { G };
// export struct S { x: Uint<16>, y: Boolean }
// circuit G(x: S): Boolean {
// return S.y;
// }
//}
// If M is uncommented, the compiler will import this module and not the one
// defined in M.compact. In this case, the compiler will throw an error for
// exporting F.
import M;
export { F };
The import syntax allows the module to be identified by a string pathname. In this case, the compiler
first looks for the imported module relative to the current directory (the path of the importing
program) and then in the directories identified by COMPACT_PATH
. Importing by a pathname allows
importing multiple modules with the same name. For example, consider the program M.compact
:
module M {
export { F };
export struct S { x: Uint<16>, y: Boolean }
circuit F(x: S): Boolean {
return S.y;
}
}
And the program A/M.compact
:
module M {
export { F };
export struct S { x: Uint<16>, y: Boolean }
circuit F(x: S): Boolean {
return S.y;
}
}
And finally the program test.compact
can export both $F
and A_F
but not $G
:
module M {
export { G };
export struct S { x: Uint<16>, y: Boolean }
circuit G(x: S): Boolean {
return S.y;
}
}
import "M" prefix $;
// this imports M.compact and not the module M defined above
import "A/M" prefix A_;
export { $F
,A_F
// ,$G
// uncommenting this will result in an error
};
Top-level exports
The circuits exported at the top level of a contract (i.e., not merely exported from a module) are the entry points of the contract and may not take generic arguments. Although multiple circuits with the same name are allowed generally to support function overloading, it is a static error if more than one circuit with the same name is exported from the top level.
User-defined types exported from the top level of the main file can be used to describe the argument and return types of witnesses and exported circuits; these may accept generic arguments, but generic arguments not actually used as types are dropped in the exported type. For example:
export struct S<#n, T> { v: Vector<n, T>; curidx: Uint<0..n> }
is exported for use as a TypeScript type with the T
parameter but not the n
parameter, i.e.,:
export type S<T> = { v: T[]; curidx: bigint }
Ledger field names exported from the top level are visible for direct inspection
by code outside of the contract via the generated TypeScript ledger()
function.
Circuits
The basic operational element in Compact is the circuit
. This corresponds
closely to a function in most languages but is compiled directly into a
zero-knowledge circuit. Circuits are declared as:
circuit c(a: A, b: B, ...): R {
...
}
circuit id<T>(value: T): T {
return value;
}
where A
, B
, ..., and R
are types (where R
may be Void
), and a
, b
are parameters. The circuit body itself is a sequence of statements, and each
path through the body must end with a return
statement, unless the return
type is Void
.
Pure and impure circuits
A Compact circuit is considered pure if it computes its outputs from its inputs without reference to or modification of public state (via the ledger) or private state (via witnesses). In practice, the compiler considers a circuit to be impure if the body of the circuit contains a ledger operation, a call to any impure circuit, or a call to a witness.
Some external circuits defined in CompactStandardLibrary
are witnesses;
calls to these make the caller impure.
The remainder are considered pure, so calls to those do not make the caller impure.
A Compact program can declare a circuit to be pure by prefixing the circuit
definition with the pure
modifier, which must follow the export
modifier,
if present, e.g.:
pure circuit c(a: Field): Field {
...
}
export pure circuit c(a: Field): Field {
...
}
The only effect of the pure
modifier is that the compiler will
flag the declaration as an error if its own analysis determines
that the circuit is actually impure.
The pure modifier allows an application to ensure that the circuit
will be present in the PureCircuits
type declaration and via the
pureCircuits
constant in the TypeScript module produced for a
(correct) Compact program by the Compact compiler.
Statements
A statement may be
- a
for
loop - an
if
statement - a
return
statement - an
assert
- a block - a sequence of statements in a nested scope, enclosed by curly braces
- a
const
binding statement - an expression
for
loop
A for
loop repeats for a fixed number of iterations, using one of the two
syntaxes below:
for i in <vector> do <statement>
for i = 0 to 5 do <statement>
if
statement
An if
statement is of one of the following forms:
if (testexpr)
<statement>
if (testexpr)
<statement>
else
<statement>
return
statement
If a circuit's return type is Void
,
return;
is a valid statment. Otherwise,
return <expr>;
for an expression <expr>
of the declared return type is a
valid return statement.
assert
statement
An assertion can be made with
assert <expr> "what constraint was violated";
where <expr>
should evaluate to a Boolean
. If <expr>
evaluates to
true, the assertion succeeds; if <expr>
evaluates to false, it fails
with the given message. Each assertion is
checked at runtime and constrained in-circuit.
const
binding statement
A new constant can be brought into scope with
const x = <expr>;
It may optionally be annotated with a type, in which case the type is checked with the expression.
const x: T = <expr>;
The name of a constant may not be reused within a block, and constants cannot be reassigned, although they can be shadowed in a nested block:
circuit c(): Field {
const answer = 42;
{
const answer = 12;
assert answer != 42 "shadowing didn't work!";
}
return answer; // returns 42
}
Constant initializer expressions are evaluated when the binding statement is executed.
Expressions
This section describes the syntax of Compact expressions and provides their static typing rules and their evaluation rules.
The syntax of expressions is given by an EBNF grammar. We use the following notational conventions in the grammar:
- Terminals are in bold monospaced font
- Non-terminals are in emphasized font
- Alternation is indicated by a vertical bar (
|
) - Repetition of zero or more items is indicated by enclosing them in curly
braces (
{
and}
) - Optional items are indicated by enclosing them in square brackets (
[
and]
)
A Compact expression either has a static type, or else it contains a type error. The static type of an expression, if it has one, is either a Compact type or else a ledger state type. If an expression in a program contains a type error, it means that the Compact compiler will not compile that program. Subexpressions of Compact expressions are always required to be well-typed (free from type errors).
Every Compact expression either evaluates to a value, or else it raises an exception. The evaluation of an expression is defined in terms of the evaluation of its subexpressions. If the evaluation of a subexpression raises an exception, then the evaluation of the containing expression will stop and raise the same exception.
Literals
Compact has syntax for boolean, numeric, and string literal expressions.
expr | → | true |
| |