Compact reference
Compact is a 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 has four kinds of code:
- type declarations, to support all of the following
- a declaration 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
Types
Primitive types
The following are primitive types in Compact:
Boolean
, inhabited bytrue
andfalse
Void
, a pseudo-type that has no expressions inhabiting it, but may be used as a return typeField
, a single element in the scalar prime field of the zero-knowledge proving systemUnsigned Integer[n]
for ann
-bit unsigned integerUnsigned Integer[<= n]
for an unsigned integer less that or equal to the literaln
Bytes[n]
for a byte array ofn
bytesVector[n, T]
for a sequence of exactlyn
values of typeT
Opaque["name"]
for a value that is unknown to Compact and will be represented in circuits as the value's hash
User-defined types
Users can define two kinds of types themselves: structures and enumerations.
A struct
declaration may look like the following examples:
struct Thing {
triple: Vector[3, Field],
flag: Boolean,
}
struct NumberAnd[T] {
num: Unsigned Integer[32];
item: T;
}
The second example uses a type parameter, enclosed in square brackets.
Structure are records of related data, combined into a single value. Ordering matters here, as it is used in calling the structure's constructor. Note that a structure may not contain itself, either directly or indirectly; the following is invalid:
struct Left {
right: Right,
}
struct Right {
left: Left,
}
Declarations of enumerations follow the form:
enum Fruit { apple, pear, plum }
This defines the type Fruit
, with entries Fruit.apple
, Fruit.pear
, and Fruit.plum
,
which correspond to integers 0, 1, and 2 respectively.
Representations in TypeScript
Compact's primitive types are represented in TypeScript as follows:
Boolean
-boolean
Void
-void
Field
-bigint
with runtime bounds checksUnsigned Integer[n]
/Unsigned Integer[<= 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.
Runtime representations
Some Compact operations need a runtime type information to inform their
behavior. Because TypeScript erases types at runtime, and some TypeScript types
do not uniquely identify their corresponding Compact type, the
@midnight/compact-runtime
package provides explicit runtime types satisfying
the CompactType<T>
interface, where T
is the corresponding TypeScript type. This is
not user-facing most of the time, unless you wish to replicate the behavior
of the operations implemented in @midnight/compact-runtime
.
When creating a runtime type instance for a primitive type, the following constructors may be used:
Boolean
-new CompactTypeBoolean()
Void
- not implementedField
-new CompactTypeField()
Unsigned Integer[<= n]
-new CompactTypeUnsignedInteger(n, length)
, wherelength
is the number of bytes required to storen
Unsigned Integer[n]
- asUnsigned Integer[<= (2 ** n) - 1]
Bytes[n]
-new CompactTypeBytes(n)
Vector[n, T]
-new CompactTypeVector(n, rt_T)
, wherert_T
is the runtime type ofT
Opaque["String"]
-new CompactTypeString()
Opaque["Uint8Array"]
-new CompactTypeUint8Array()
.
For user-defined types, structures are not currently easily
constructed at runtime and require implementing CompactType<T>
manually or using compiler internals. Enumerations are exposed
through new CompactTypeEnum(maxValue, length)
, where maxValue
is
the maximum permissible integer assignable, and length
its
representation length in bytes (almost certainly 1).
Imports, includes, and modules
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. When encountered,
the Compact compiler will search for a Compact source file at
path/to/file.compact
, relative to any of the directories in the
:
-separated environment variable COMPACT_PATH
, as well as the
current directory. This file must be found and will be included
verbatim in place of the include
statement.
Compact's standard library std.compact
is typically included in this way, and
Compact has currently not been well-tested if used without it.
A module is a collection of definitions whose namespace is hidden from surrounding code. A module is defined with
module Mod1 {
...
}
module Mod2[T] {
...
}
Any definitions inside a module (including other modules) may be prefixed with
the export
keyword. Exports may also be defined separately, with the export
statement:
export { foo, bar, baz }
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
The circuits exported at the top level of the main file being compiled are the entry points of that file and may not take type arguments.
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 its
flow must end with a return
statement, unless the return type is Void
.
Pure vs 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.
At present, all external circuits defined in std.compact
are considered
pure, so calls to external circuits 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
statements - 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>
These are expanded to repeated instances of <statement>
for each entry in
<vector>
, or each integer 0, 1, 2, 3, and 4, with the loop variable bound to
the vector entry or integer value.
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 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
. 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 nested block:
circuit c(): Field {
const answer = 42;
{
const answer = 12;
}
return answer; // returns 42
}
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 |
| | false | |
| | nat | |
| | str | |
| | pad ( nat , str ) |
Boolean literals are the reserved words true
and false
.
The static type of a boolean literal is Boolean
.
It evaluates to one of the two boolean values.
Numeric literals are non-negative decimal integers. They are either
the number 0
or a sequence of digits starting with a non-zero digit.
The static type of a natural number literal n
is Unsigned Integer[<= n]
.
There is an implementation-defined maximum unsigned integer value. A numeric
literal larger than this value will have an invalid static type
Unsigned Integer[<= n]
for some n
larger than the maximum unsigned
integer. This expression will be a static type error unless the literal is
smaller than the maximum Field
value and is used in a type cast expression of
the form e as Field
.
A natural number literal evaluates to the unsigned integer value that it denotes.
String literals use TypeScript string literal syntax. Note that they can
therefore be enclosed in either single ('
) or double ("
) quotes, and they
can contain escaped characters. Strings are represented by their UTF-8
encoding. The length of a string is the length of its UTF-8 encoding.
The static type of a string literal is Bytes[n]
where n
is the length of
the string.
It evaluates to a byte array containing its UTF-8 encoding.
In addition, the expression pad(n, s)
is a string literal, where
pad
is a reserved word, n
is a natural number literal and s
is a string
literal whose length must be less than or equal to n
.
The static type of a padded string literal pad(n, s)
is Bytes[n]
.
It evaluates to a byte array containing the UTF-8 encoding of s
, followed by
0
bytes up to the padded length n
.
Identifier references
The syntax of Compact identifiers is the same as the syntax of TypeScript identifiers. Identifiers are bound by a declaration in the program, and their value and static type depends on the declaration binding them.
expr | → | id |
Circuit parameters are bound by circuit declarations. The static type of a circuit parameter reference is the declared static type given by the parameter declaration's type annotation. It evaluates to the value of the corresponding argument expression that was passed to the circuit call.
Constants are bound by const
binding statements.
If the binding statement has a type annotation, then the constant reference's
static type is the declared static type given by the type annotation. If the
binding statement does not have a type annotation, then the constant reference's
static type is the inferred static type (that is, the type of the binding
statement's initializer expression).
A constant reference evaluates to the value of the binding statement's
initializer expression.
Note that constant references can have ledger state types because they can be initialized with a ledger state type's default value.
Compact is an eager call-by-value language. Argument expressions are evaluated before performing a call, and constant initializer expressions are evaluated when the binding statement is executed. Identifier references look up the corresponding value and do not cause evaluation of argument or initializer expressions.
Default values of a type
Every Compact type and ledger state type has a default value.
expr | → | null ( type ) |
| | null ( ledger-adt ) |
The expression null(T)
, where T
is a Compact type or a ledger state type,
has static type T
.
It evaluates to the default value of that type.
Note that default value expressions can have ledger state types.
Circuit and witness calls
Circuits and witnesses are both like functions that can be called. The
expression f(e, ...)
is a call, where f
is a circuit or witness and e, ...
is a sequence of zero or more comma-separated argument expressions.
expr | → | fun ( [expr {, expr}] ) |
fun | → | id [targs] |
| | circuit ( [arg {, arg}] ) : return-type block | |
| | ( fun ) | |
targs | → | [ [targ {, targ}] ] |
targ | → | nat |
| | type | |
arg | → | id : type |
The circuit or witness can take several different forms:
A circuit name is the name of a circuit from a circuit declaration in scope. Generic circuits cannot be called without explicitly specializing them with type arguments enclosed in square brackets. Calls to generic circuits must be fully specialized: the number of type arguments must match the number of type parameters.
An anonymous circuit is an inline circuit literal having the form
circuit (id: T, ...): R { s; ... }
with zero or more comma-separated
parameters x: T
, return type R
, and body { s; ... }
. Each parameter
consists of an identifier id
(the parameter's name) and a required type
annotation : T
where T
is a non-void Compact type. The return type R
is a
(possibly Void
) Compact type. The body is a sequence of zero or more
semicolon-delimited statements enclosed in curly braces.
There is no syntax for generic anonymous circuits. This is because circuits are not first-class values: they cannot be passed around or stored in data structures, they must be called. And generic circuits must be specialized to call them, so anonymous generic circuits would have to be immediately specialized. In that case, the programmer can just write the non-generic version themselves.
A witness name is the name of a witness from a witness declaration in scope. Note that witnesses cannot be generic.
A parenthesized circuit or witness has the form (f)
where f
is a circuit
or witness as defined here, that is either a circuit name, an anonymous circuit,
a witness name, or a parenthesized circuit or witness.
Because circuits and witnesses are not first class, parameter names and constant names are not allowed as the circuit or witness part of a call. Nor are arbitrary expressions allowed, for the same reason.
The static type of a call expression is the return type of the circuit or witness.
It is a static type error if the number of arguments does not match the number of parameters from the declaration or circuit literal. It is a static type error if the static type of any argument expression is not a subtype of the declared type of the corresponding parameter from the declaration or circuit literal.
Calls are evaluated by evaluating the argument expressions in order from left to right. Then, if a circuit is being called, the statements in the body of the circuit are executed with the parameter names bound to the corresponding argument values. The value of a circuit call is the value returned from the execution of the body. If a witness is being called, then the Compact language will invoke the TypeScript or JavaScript witness function with the argument values. The value of a witness call is the value returned by the witness function.
Structure construction
Structure values are constructed using the keyword new
. The expression
new S(e, ...)
is a structure construction, where S
is a structure type and
e, ...
is a sequence of zero or more comma-separated argument expressions.
expr | → | new tref ( [expr {, expr}] ) |
tref | → | id [targs] |
The structure must be the name from a structure declaration in scope. If the structure is generic, then it must be explicitly specialized with type arguments enclosed in square brackets. Generic structure constructions must be fully specialized: the number of type arguments must match the number of type parameters.
The static type of a non-generic structure construction is the named structure type.
The type arguments to a generic structure can be types, natural number literals, or the names of type parameters in scope. A generic structure construction is typechecked by substituting the type arguments for the type parameters in the structure's definition. The static type of a generic structure construction is a structure with the same name as the generic type, and field types gotten from substituting the type arguments for the type parameters in the structure's declaration.
It is a static type error if the number of arguments does not match the number of members in the structure. It is a static type error if the static type of an argument expression is not a subtype of the corresponding field type from the specialized structure type.
A structure constructor expression is evaluated by evaluating the argument expressions in order from left to right. Its value is a structure value with the fields initialized to the values of the argument expressions.
Vector construction
Vector values are constructed with expressions of the form [e, ...]
where e, ...
is a sequence of zero or more comma-separated argument expressions. A
non-empty sequence can have an optional trailing comma.
expr | → | [ [expr {, expr}] [,] ] |
The static type of a vector construction exprssion is Vector[n, T]
where n
is the number of subexpressions and T
is the least upper bound of the static
types of the subexpressions.
It is evaluated by evaluating the subexpressions from left to right. Its value is a vector whose length is the number of subexpressions and whose elements are the subexpression values.
Parenthesized expressions
Compact allows parenthesized expressions of the form (e)
, where e
is an
expression. They can be used to control the order of evaluation.
expr | → | ( expr ) |
The type of the parenthesized expression is the type of the subexpression.
Its value is the value of the subexpression.
Sequence expressions
Expressions can be sequenced for their side effects. An expression of the form
(e0, e1, e2, ...)
where e0, e1, e2, ...
is a sequence of two or more
comma-separated expressions is a sequence expression.
expr | → | ( expr {, expr} , expr ) |
The static type of a sequence expression is the static type of the last subexpression.
It is evaluated by evaluating the subexpressions from left to right. Its value is the value of the last subexpression.
Ledger expressions
A Compact program interacts with its public state by invoking operations upon the ledger or ledger state types. There are two different forms of ledger calls.
Kernel operations are operations that do not depend on specific ledger
state. They are invoked by expressions of the form ledger.op(e, ...)
where
ledger
is a reserved word, op
is the name of a builtin kernel operation, and
e, ...
is a comma separated sequence of zero or more argument expressions.
Ledger ADT operations are operations on the program's public ledger state.
They are invoked by expressions of the form ledger.member.op(e, ...)....
where
ledger
is a reserved word, member
is the name of a member of the program's
public ledger, and .op(e, ...)....
are a sequence of zero or more ledger
ADT operation invocations where each op
is the name of a ledger ADT
operation and each e, ...
is a sequence of zero or more comma-separated
argument expressions.
expr | → | ledger ledger-accessor |
| | ledger . id {ledger-accessor} | |
ledger-accessor | → | . id ( [expr {, expr}] ) |
Note that ledger ADT operations can be chained, because the result of a ledger ADT operation might itself have a ledger state type. Kernel operations cannot be chained, because the kernel is not a ledger state type and is not returned by any operation.
The static type of a kernel operation expression is the return type of the corresponding kernel operation according to the ledger data types reference.
The static type of a ledger ADT operation expression is the return type of the corresponding ADT operation according to the ledger data types reference. Note that this might be a Compact type or it might be a ledger ADT type. Values of ledger ADT types can have ADT operations invoked (immediately) on them, but any other use would be a static type error.
Kernel operations are evaluated by evaluating the argument subexpressions in order from left to right and then invoking the corresponding kernel operation with the argument values.
A ledger ADT operation ledger.member
(that is not followed by a ledger
accessor) is implicitly an invocation of the read
operation. It is evaluated
as if it were ledger.member.read()
.
A ledger ADT operation ledger.member.op(e, ...)
is evaluated by evaluating the
argument subexpressions from left to right, and then invoking the operation
op
on the public ledger member member
with the argument values.
A ledger ADT operation adt.op(e, ...)
where adt
is itself a ledger ADT
operation is evaluated by first evaluating adt
, then evaluating the argument
subexpressions from left to right, and then invoking the operation op
on the
ledger ADT value of adt
with the argument values.
Element and member access expressions
Compact has expressions for accessing the elements of vector values and the
members of structure values. An expression of the form e[n]
where e
is an
expression and n
is a numeric literal is a vector element access. An
expression of the form e.id
where e
is an expression and id
is the name
of a structure member is a structure member access.
expr | → | expr [ nat ] |
| | expr . id |
Vector element accesses are type checked by checking the type of the
subexpression. It is a type error if this type is not a vector type
Vector[n, T]
. It is a type error if the size of the vector n
is less than
or equal to the numeric literal in the expression. The type of the expression
is the element type T
from the subexpression's vector type.
Vector element accesses are evaluated by evaluating the subexpression. The value of the expression will be the element value at the given zero-based index. The subexpression will have a vector value and the element access will not be out of bounds, because the expression is well-typed.
Member access expressions are type checked by checking the type of the subexpression. It is a type error if this type is not a structure type. It is a type error if the structure type does not contain a member with the same name as the name in the expression. The type of the expression is the type of the corresponding named member of the subexpression's structure type.
Member access expressions are evaluated by evaluating the subexpression. The value of the expression will be the member value with the given name. The subexpression will have a structure value and the name will exist, because the expression is well-typed.
Boolean negation expressions
Compact has unary boolean negation expressions of the form !e
where e
is an
expression.
expr | → | ! expr |
A boolean negation expression is type checked by checking the type of the
subexpression. It is a type error if this type is not Boolean
. The type of
the expression will be Boolean
.
Negation expressions are evaluated by evaluating the subexpression. The value
of the expression will be true
if the value of the subexpression is false
and vice versa. The subexpression will have a boolean value because the
expression is well-typed.
Binary arithmetic expressions
Binary arithmetic expressions are of the form e0 op e1
where e0
and e1
are expressions and op
is one of Compact's binary arithmetic operators. The
binary arithmetic operators are add (+
), subtract (-
) and
multiply (*
).
expr | → | expr + expr |
| | expr - expr | |
| | expr * expr |
Arithmetic expressions require the type of both subexpressions to be numeric
types, that is, either a Field
or an Unsigned Integer
. The type of the
result will depend on the types of the subexpressions as follows:
- If either subexpression has type
Field
, the result will have typeField
- Otherwise the left subexpression will have type
Unsigned Integer[<= m]
and the right subexpression will have typeUnsigned Integer[<= n]
for some boundsm
andn
. The type of the result depends on the operation as follows:- For add, the result will have type
Unsigned Integer[<= m+n]
- For subtract, the result will have type
Unsigned Integer[<= m]
- For multiply, the result will have type
Unsigned Integer[<= m*n]
- For add, the result will have type
For arithmetic operations with Unsigned Integer
result types, it is a
static type error if the result's bound would be greater than the maximum
unsigned integer.
Arithmetic expressions are evaluated by first evaluating the subexpressions in
order from left to right. Integer addition, subtraction, or
multiplication is then used on the subexpression values. The overflow and
underflow behavior differs for Field
and Unsigned Integer
operations:
Field
arithmetic overflow and underflow wraps aroundUnsigned Integer
addition and subtraction cannot overflow, the static type of the result will always be large enough to hold the result valueUnsigned Integer
subtraction checks if the value of the right subexpression is greater than the value of the left subexpression. If so, it is a runtime error (the result would be negative). Otherwise the unsigned subtraction is performed.
The static typing rules imply that if Field
arithmetic semantics is desired,
then at least one of the operands must have static type Field
.
Type cast expressions
Type cast expressions in Compact are of the form e as T
where e
is an
expression, as
is a reserved words, and T
is a Compact type.
Note that TypeScript-style casts of the form <T>e
are not supported in
Compact.
expr | → | expr as type |
Type cast expressions are type checked by checking the type of the
subexpression. If the cast from the subexpression's type to the
type T
named in the type cast is allowed, then the static type
of the expression will be T
. Otherwise, it is a static type
error.
The table below describes the allowed type casts. Casting between types not shown in the table is not allowed. The entries in the table can be one of:
- static: the type cast only changes the static type and does not have any effect at runtime
- conversion: the type cast always succeeds but has the runtime effect of converting between different source and target representations, which normally has a low cost
- checked: the type cast is checked at runtime and can fail
- no: the type cast is not allowed
- a number: see the corresponding note below the table
TO | |||||
---|---|---|---|---|---|
Field | Unsigned Integer[<= n] | Boolean | Bytes[n] | ||
FROM | Field | static | checked | 1 | 2 |
Unsigned Integer[<= m] | static | 3 | conversion | no | |
enum type | conversion | no | no | no | |
Boolean | conversion | 4 | no | no | |
Bytes[m] | 5 | no | no | 6 |
Field
toBoolean
: the value 0 is converted toFalse
and all other values are converted toTrue
.Field
toBytes[n]
: the value of the field is converted intoBytes
of the given length, with the least-significant byte of the field occurring first in theBytes
. TheBytes
will be padded to the length with trailing zeros. It is a runtime error if the field value does not fit in the length.Unsigned Integer[<= m]
toUnsigned Integer[<= n]
: ifm
is less than or equal ton
this is a static cast. Otherwise it is checked and will fail at runtime if the value is greater thann
.Boolean
toUnsigned Integer[<= n]
: Ifn
is not 0 then this is a conversion ofFalse
to 0 andTrue
to 1. Otherwise, it is checked and will fail at runtime if the value isTrue
(and convertFalse
to 0).Bytes[m]
toField
: the bytes are converted into a field with the least-significant byte of the field occurring first in theBytes
. It is a runtime error if the result would exceed the maximumField
value.Bytes[m]
toBytes[n]
: the cast is a static cast ifm
equalsn
, and is not allowed otherwise.
Allowed type casts are evaluated by first evaluating the subexpression.
Then, if the cast is static, the result is the subexpression's value
interpreted as the type T
mentioned in the cast expression. If the
cast is a conversion, the JavaScript representation of the subexpression's
value is converted into the representation of a value of type T
. If the
cast is checked, the check is performed before conversion and the cast
fails (at runtime) if the check fails. The exceptions noted in the table
are evaluated as described above after evaluating the subexpression.
Relational comparison expressions
Relational comparison expressions are of the form e0 op e1
where e0
and e1
are expressions and op
is one of Compact's relational operators.
The relational operators are equals (==
), not equals (!=
), less
than (<
), greater than (>
), less than or equals (<=
), and
greater than or equals (>=
).
expr | → | expr == expr |
| | expr != expr | |
| | expr < expr | |
| | expr > expr | |
| | expr <= expr | |
| | expr >= expr |
Equals and not equals require the types of the subexpressions to be in the
subtype realation. That is, the type of the first subexpression must be a
subtype of the type of the second subexpression, or else the type of the
second subexpression must be a subtype of the type of the first subexpression.
Additionally, equals and not equals require the type of both subexpressions
to be non-Void
. If the subexpressions have Vector
types then the element
types must both be non-Void
.
Less than, greater than, less than or equals, and greater than or equals
require the type of both subexpressions to be unsigned integer types (note that Field
cannot be compared with these operators).
The type of the result is Boolean
.
Relational comparison expressions are evaluated by evaluating the subexpressions in order from left to right. Then the comparison is performed as described below.
Equals
The comparison that is performed depends on the type of the operands:
Boolean
: if the operands have typeBoolean
, then the values must be the same boolean value. Both operands will have typeBoolean
due to the static typing rules.Unsigned Integer
: if the operands have unsigned integer types, then the integer values must be equal. Both operands will have unsigned integer types due to the static typing rules.Field
: if either operand has typeField
, then the integer values of the operands must be equal. Both operands will have numeric (Field
or unsigned integer) types due to the static typing rules.Bytes:
if the operands have bytes types, then the corresponding bytes at each index must be equal. Both operands will have bytes types and their lengths will be equal due to the static typing rules.Vector:
if the operands have vector types, then the corresponding element values at each index must be equal according to these rules, based on the static element types. Both operands will have vector types, they will have the the same length, and their element types will be in the subtype relation and non-Void
due to the static typing rules.Opaque:
if the operands have opaque types, then the runtime values must be equal according to JavaScript's strict equality (===
) operator. Both operands will have the same opaque type due to the static typing rules.- structure type: if the operands have structure types, then the corresponding values of each field must be equal according to these rules, based on the field types. Both operands will have the same struture type due to the static typing rules.
- enum type: if the operands have enum types, then they must be the same enum value. Both operands will have the same enum type due to the static typing rules.
Not equals
The operands are compared according to the rules for equals above, and then the boolean result is negated.
Less than, greater than, less than or equals, and greater than or equals
The integer values of the operands are compared according to the relational operation. Both operands will have unsigned integer types due to the static typing rules.
Short-circuit logical expressions
Compact supports short-circuit logical expressions of the form e0 op e1
where e0
and e1
are expressions and op
is one of the logical operators
or (||
) or and (&&
).
expr | → | expr || expr |
| | expr && expr |
Logical expressions require the type of the left subexpression to be
Boolean
. The type of the right subexpression must be a supertype of
Boolean
(including Boolean
itself). The entire expression will have
the same type as the type of the right subexpression.
Logical expressions are evaluated by first evaluating the left subexpression. Then, the value of that expression determines the value of the entire expression as follows:
- For or, if the value of the left subexpression is
false
then the right subexpression is evaluated and its value is the value of the entire expression. Otherwise, the right subexpression is not evaluated and the value of the left subexpression, implicitly cast to the type of the entire expression, is the value of the entire expression. - For and, if the left subexpression is
true
then the right subexpression is evaluated and its value is the value of the entire expression. Otherwise, the right subexpression is not evaluated and the value of the left subexpression, implicitly cast to the type of the entire expression, is the value of the entire expression.
Conditional expressions
Compact supports conditional expressions of the form e0 ? e1 : e2
where e0
,
e1
, and e2
are expressions.
expr | → | expr ? expr : expr |
Conditional expressions require the type of e0
to be Boolean
. The types of
e1
and e2
must be in the subtype relation. That is, either the type of
e1
is a subtype of the type of e2
or else the type of e2
is a subtype of
the type of e1
.
The type of the entire expression is the type of e2
if e1
is a subtype of
e2
and the type of e1
if e2
is a subtype of e1
.
Conditional expressions are evaluated by first evaluating e0
. Then, the
value of that expression determines which of the other subexpressions is
evaluated:
- if the value of
e0
istrue
, thene1
is evaluated and its value is the value of the entire expression - if the value of
e0
isfalse
, thene2
is evaluated and its value is the value of the entire expression
The evaluation rules ensure that no more than one of e1
and e2
will be
evaluated.
Map and fold expressions
Compact supports expressions that perform the higher-order operations map and (left) fold over vectors.
Map expressions have the form map f over v over v ...
where map
and over
are keywords, f
is a circuit or witness, and the v
s are expressions. A
circuit or witness taking n arguments can be mapped over n vectors by
providing n over
clauses.
Fold expressions have the form fold f e over v over v ...
where fold
and
over
are keywords, f
is a circuit or witness, and e
and the v
s are
expressions. A circuit or witness taking n+1 arguments can be folded over an
initial value e
and n vectors by providing n over
clauses.
expr | → | map fun over over |
| | fold fun expr over over | |
over | → | over expr |
The syntax of the circuit or witness is given by the grammar production for fun in the section Circuit and witness calls above.
A map expression is typechecked by checking the type of the witness or circuit
f
to find its parameter types and its return type R
. f
must have at least
one parameter. The map expression must have the same number of over
clauses
as the number of parameters of f
. Each of the over
subexpressions
must have a vector type and all these vector types must have the same length
n
. If the type of the ith parameter to f
is T
, then the type of the
ith over
subexpression must be Vector[n, S]
where S
is a subtype of
T
. The type of entire expression is Vector[n, R]
.
A fold expression is typechecked by checking the type of the witness or circuit
f
to find its parameter types and its return type R
. f
must have at
least two parameters, and the type of the first parameter must be the same type
as the return type R
. The fold expression must have one fewer over
clauses
than the number of parameters of f
. The subexpression e
gives the initial
value for the fold. It must have a type which is a subtype R
. Each of the
over
subexpressions must have a vector type and all these vector types must
have the same length n
. If the type of the i+1th parameter of f
is T
then the type of the ith over
subexpression must be Vector[n, S]
where
S
is a subtype of T
. The type of the entire expression is R
.
Map expressions are evaluated by evaluating the over
subexpressions from left
to right. These values are the input vector values. The witness or circuit
f
is then applied in turn, from index 0 up to index n
-1, to arguments taken
from the input vector values. The result is a vector of length n
where each
ith element is the result of applying f
to the ith elements of the
corresponding input vector values.
Fold expressions are evaluated by evaluating the initial value expression e
and then evaluating the over
subexpressions from left to right. The values
of the over
expressions are the input vector values. The witness or circuit
f
is then applied in turn, from index 0 up to index n
-1, to an accumulator
value argument and arguments taken from the input vector values. The 0th
(initial) accumulator value is the value of the expression e
, and each
subsequent i+1th accumulator value is the result of applying f
to the ith
accumulator value and to the ith elements of the corresponding input vector
values. The result is the n
th (final) accumulator value where n
is the
length of the input vectors.
Ledger assignment expressions
Compact has ledger assignment expressions. They have the form lhs op e
where
lhs
is a ledger expression as defined in the section Ledger expressions
above, op
is one of the assignment operators =
(assignment), +=
(addition
assigment), or -=
(subtraction assignment), and e
is an expression.
expr | → | ledger . id ledger-accessor = expr |
→ | ledger . id ledger-accessor += expr | |
→ | ledger . id ledger-accessor -= expr |
lhs = e
is shorthand for lhs.write(e)
. lhs += e
is shorthand for lhs. increment(e)
. lhs -= e
is shorthand for lhs.decrement(e)
.
Ledger assignment expressions are type checked exactly as if they were their longer equivalent invoking a ledger ADT operation.
They are evaluated exactly as if their longer equivalent were evaluated as a ledger expression.
Externals: ledger
and witness
Compact code can call code external to the zero-knowledge circuits in two ways:
- locally and unconstrained, through
witness
functions, - in the globally replicated ledger, through specific
ledger
data structures.
A witness
function declaration can appear anywhere a circuit
definition can, although a witness may not take type arguments for the
TypeScript target. A witness function does not
have a body, and its implementation is instead an input to
the contract in the TypeScript target. For instance:
witness something(x: Boolean): Field;
A witness
function can be called in the same way as a circuit
, but it does not
generate constraints in a circuit and merely obtains an output from the
local machine.
Do not assume in your contract that the code of any witness
function
is the code that you wrote in your own implementation. Any DApp may
provide any implmentation that it wants for your witness
functions.
Results from them should be treated as untrusted input.
In addition to witness
functions, an Compact program may have a
single ledger
declaration, defining the type of the information the
contract stores Midnight's public ledger. A ledger declaration looks
similar to a struct
, but it uses state types
instead of Compact types, and it does not have a name or type
parameters. For instance:
ledger {
val: Cell[Field],
cnt: Counter,
mapping: Map[Boolean, Field],
}
Ledger state types
In a ledger
declaration, the following types are valid:
Counter
Cell[T]
, for any Compact typeT
Set[T]
, for any Compact typeT
Map[K, T]
, for any Compact typesK
andT
Map[K, V]
, for any Compact typeK
and ledger state typeV
(see the following section)List[T]
, for any Compact typeT
MerkleTree[n, T]
, for a compile time integer1 < n <= 32
, and any Compact typeT
HistoricMerkleTree[n, T]
, for a compile time integer1 < n <= 32
, and any Compact typeT
Each ledger type supports a set of operations, which can be invoked with
ledger.<field name>.<operation>(<arguments ...>)
The read
, and write
operations of the Cell
type has syntactic
sugar. If x
is a Cell
field in the ledger, then you may write
ledger.x // equivalent to ledger.x.read()
ledger.x = val // equivalent to ledger.x.write(val)
The increment
and decrement
operations of type Counter
type also
has syntactic sugar. If c
is a Counter
field in the ledger, then you may write
ledger.c += val // equivalent to ledger.c.increment(val)
ledger.c -= val // equivalent to ledger.c.decrement(val)
A comprehensive list of operations can be found in the Compact ledger data type documentation.
Nested state types in the Map
type
The only ledger state type in which values of other state types may be
held is Map
. The key values in a Map
must be non-state types
(simple Compact types), but the mapped values may be counters, sets,
lists, other maps, and so on.
Here is a small example:
include 'std';
ledger {
fld: Map[Boolean, Map[Field, Counter]];
}
export circuit init_nested_map(b: Boolean): Void {
ledger.fld.insert(b, null(Map[Field, Counter]));
}
export circuit init_nested_counter(b: Boolean, n: Field): Void {
ledger.fld.lookup(b).insert(n, null(Counter));
}
export circuit increment_nested_counter(b: Boolean, n: Field, k: Unsigned Integer[16]): Void {
ledger.fld.lookup(b).lookup(n).increment(k);
}
export circuit read_nested_counter1(b: Boolean, n: Field): Unsigned Integer[64] {
return ledger.fld.lookup(b).lookup(n).read();
}
export circuit read_nested_counter2(b: Boolean, n: Field): Unsigned Integer[64] {
return ledger.fld.lookup(b).lookup(n);
}
In this example,
fld
is bound to aMap
fromBoolean
values toMap
s fromField
values toCounter
sinit_nested_map
can be used to create the innerMap
for a particular outer-Map
keyinit_nested_counter
can be used to create aCounter
for a given outer-Map
key and a given inner-Map
keyincrement_nested_counter
can be used to increment an existingCounter
for a given outer-Map
key and a given inner-Map
key- either
read_nested_counter1
orread_nested_counter2
can be used to read the value of an existingCounter
for a given outer-Map
key and a given inner-Map
key.
Notes:
- Nesting is permitted only within
Map
values. That is, nesting is not permitted inMap
keys or within any ledger state type other thanMap
. - Nested values must be initialized to null before first use. The
syntax
null(T)
is used to create null ledger state type values, just as it can be used to create null Compact type values. - Ledger state type values are not first-class objects, so when
accessing a nested value, the entire indirection chain must be
used. For example, the following will result in a compiler error:
export circuit increment_nested_counter(b: Boolean, n: Field, k: Unsigned Integer[16]): Void {
ledger.fld.lookup(b); // ERROR: incomplete chain of indirects
} - When the last lookup is a read of a base type one can omit the
explicit
read()
indirect, as illustrated by the definitions ofread_nested_counter1
andread_nested_counter2
above, which have the same behavior. - For convenience, local variables can hold null ledger state type
values, so the following definition of
init_nested_map
is equivalent to the one above.export circuit init_nested_map(b: Boolean): Void {
const t = null(Map[Field, Counter]);
ledger.fld.insert(b, t);
}
TypeScript target
When compiled, a contract generates several artifacts. Key to these
are the exported circuits from the contract's top level. These are
divided into two categories: those which contain ledger
or witness
calls and those which contain neither. Circuits which refer to the
ledger or to witness functions are referred to as impure. Circuits
which compute results using only their arguments, without referring to
the ledger or to local state, are referred to as pure.
A pure
modifier on a circuit definition does not affect whether the
compiler considers the circuit to be pure or impure; rather, it is merely
a way for the Contract program to declare that the circuit is pure, and
the only effect is that the compiler will complain if it is not pure.
For each of the impure circuits, a zero-knowledge prover/verifier key pair is
generated, as well as IR instructions for proof generation. These can be found
in the output directory's keys
and zkir
directories respectively.
In the contract
directory, the semantics of the contract is encoded in
TypeScript, in the form of a index.cjs
JavaScript implementation and a
index.d.cts
type declaration. For most uses, it is recommended to rely on the
information and interface provided in index.d.cts
.
Structure of the exported TypeScript
The exported TypeScript exposes a number of declarations that can be used
to interact with the contract from any TypeScript application. Some of these
will also require using the @midnight/compact-runtime
library, which all
contracts depend on and which implements key built-in behaviors.
A contract exports the following in the TypeScript module:
- For each exported user-defined type, it exports the corresponding type in TypeScript
- A
Witnesses<T>
type, which describes the format external witnesses must satisfy to instantiate the contract - A
ImpureCircuits<T>
type, which describes the set of exported impure circuits - A
PureCircuits
type, which describes the set of exported pure circuits - A
Circuits<T>
type, which describes the set of all exported circuits - A
Contract<T, W extends Witnesses<T> = Witnesses<T>>
class, which:- can be constructed by passing in an instance of
W
- exposes members
circuits: Circuits<T>
andimpureCircuits: ImpureCircuits<T>
- provides initial contract states via
initialState(privateState: T): [T, runtime.ContractState]
- can be constructed by passing in an instance of
- A constant
pureCircuits: PureCircuits
object, providing all pure circuits as pure functions - A
Ledger
type, providing views into a current ledger state, by permitting direct calls of all read functions ofledger
objects, as well of some TypeScript specific ones that cannot be called from Compact, such as iterators - A
ledger(state: runtime.StateValue): Ledger
constructor of theLedger
type
The argument T
for a number of these should be interpreted as the type of the
local/private state. For the most part, circuit
and witness
functions are
translated simply by translating their Compact types into corresponding
TypeScript types for parameters and return values. For PureCircuits
, this is
all that happens, for the other _Circuits
instances, they receive an
additional first parameter of type runtime.CircuitContext<T>
, and their
result type R
is wrapped in runtime.CircuitResults<T, R>
. For Witnesses
,
they receive an additional first parameter of type
runtime.WitnessContext<Ledger, T>
, and their result type R
is wrapped in
[T, R]
. See the runtime API docs for the details of
these types. This wrapping makes the entirety of the contract code
functional, ensuring calls have no hidden side effects.