Skip to main content

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 by true and false
  • Void, a pseudo-type that has no expressions inhabiting it, but may be used as a return type
  • Field, a single element in the scalar prime field of the zero-knowledge proving system
  • Unsigned Integer[n] for an n-bit unsigned integer
  • Unsigned Integer[<= n] for an unsigned integer less that or equal to the literal n
  • Bytes[n] for a byte array of n bytes
  • Vector[n, T] for a sequence of exactly n values of type T
  • 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 checks
  • Unsigned Integer[n] / Unsigned Integer[<= n] - bigint with runtime bounds checks
  • Bytes[n] - Uint8Array with runtime length checks
  • Vector[n, T] - T[] (with the TypeScript representation of T), with runtime length checks
  • Opaque["string"] - string
  • Opaque["Uint8Array"] - Uint8Array

User-defined types are represented in TypeScript as follows:

  • enum instances - a number with runtime membership checks
  • struct instances with fields a: A, b: B, ... - an object { a: A, b: B, ... } where A, 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 implemented
  • Field - new CompactTypeField()
  • Unsigned Integer[<= n] - new CompactTypeUnsignedInteger(n, length), where length is the number of bytes required to store n
  • Unsigned Integer[n] - as Unsigned Integer[<= (2 ** n) - 1]
  • Bytes[n] - new CompactTypeBytes(n)
  • Vector[n, T] - new CompactTypeVector(n, rt_T), where rt_T is the runtime type of T
  • 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 type Field
  • Otherwise the left subexpression will have type Unsigned Integer[<= m] and the right subexpression will have type Unsigned Integer[<= n] for some bounds m and n. 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 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 around
  • Unsigned Integer addition and subtraction cannot overflow, the static type of the result will always be large enough to hold the result value
  • Unsigned 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
FieldUnsigned Integer[<= n]BooleanBytes[n]
FROMFieldstaticchecked12
Unsigned Integer[<= m]static3conversionno
enum typeconversionnonono
Booleanconversion4nono
Bytes[m]5nono6
  1. Field to Boolean: the value 0 is converted to False and all other values are converted to True.
  2. Field to Bytes[n]: the value of the field is converted into Bytes of the given length, with the least-significant byte of the field occurring first in the Bytes. The Bytes will be padded to the length with trailing zeros. It is a runtime error if the field value does not fit in the length.
  3. Unsigned Integer[<= m] to Unsigned Integer[<= n]: if m is less than or equal to n this is a static cast. Otherwise it is checked and will fail at runtime if the value is greater than n.
  4. Boolean to Unsigned Integer[<= n]: If n is not 0 then this is a conversion of False to 0 and True to 1. Otherwise, it is checked and will fail at runtime if the value is True (and convert False to 0).
  5. Bytes[m] to Field: the bytes are converted into a field with the least-significant byte of the field occurring first in the Bytes. It is a runtime error if the result would exceed the maximum Field value.
  6. Bytes[m] to Bytes[n]: the cast is a static cast if m equals n, 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 type Boolean, then the values must be the same boolean value. Both operands will have type Boolean 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 type Field, 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 is true, then e1 is evaluated and its value is the value of the entire expression
  • if the value of e0 is false, then e2 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 vs 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 vs 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 nth (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.

danger

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 type T
  • Set[T], for any Compact type T
  • Map[K, T], for any Compact types K and T
  • Map[K, V], for any Compact type K and ledger state type V (see the following section)
  • List[T], for any Compact type T
  • MerkleTree[n, T], for a compile time integer 1 < n <= 32, and any Compact type T
  • HistoricMerkleTree[n, T], for a compile time integer 1 < n <= 32, and any Compact type T

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 a Map from Boolean values to Maps from Field values to Counters
  • init_nested_map can be used to create the inner Map for a particular outer-Map key
  • init_nested_counter can be used to create a Counter for a given outer-Map key and a given inner-Map key
  • increment_nested_counter can be used to increment an existing Counter for a given outer-Map key and a given inner-Map key
  • either read_nested_counter1 or read_nested_counter2 can be used to read the value of an existing Counter for a given outer-Map key and a given inner-Map key.

Notes:

  1. Nesting is permitted only within Map values. That is, nesting is not permitted in Map keys or within any ledger state type other than Map.
  2. 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.
  3. 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 
    }
  4. When the last lookup is a read of a base type one can omit the explicit read() indirect, as illustrated by the definitions of read_nested_counter1 and read_nested_counter2 above, which have the same behavior.
  5. 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> and impureCircuits: ImpureCircuits<T>
    • provides initial contract states via initialState(privateState: T): [T, runtime.ContractState]
  • 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 of ledger 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 the Ledger 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.