zkas bincode

The bincode design for zkas is the compiled code in the form of a binary blob, that can be read by a program and fed into the VM.

Our programs consist of four sections: constant, literal, contract, and circuit. Our bincode represents the same. Additionally, there is an optional section called .debug which can hold debug info related to the binary.

We currently keep all variables on one stack, and literals on another stack. Therefore before each STACK_INDEX we prepend STACK_TYPE so the VM is able to know which stack it should do lookup from.

The compiled binary blob has the following layout:

MAGIC_BYTES
BINARY_VERSION
NAMESPACE
.constant
CONSTANT_TYPE CONSTANT_NAME 
CONSTANT_TYPE CONSTANT_NAME 
...
.literal
LITERAL
LITERAL
...
.contract
WITNESS_TYPE
WITNESS_TYPE
...
.circuit
OPCODE ARG_NUM STACK_TYPE STACK_INDEX ... STACK_TYPE STACK_INDEX
OPCODE ARG_NUM STACK_TYPE STACK_INDEX ... STACK_TYPE STACK_INDEX
...
.debug
TBD

Integers in the binary are encoded using variable-integer encoding. See the serial crate and module for our Rust implementation.

Sections

MAGIC_BYTES

The magic bytes are the file signature consisting of four bytes used to identify the zkas binary code. They consist of:

0x0b 0x01 0xb1 0x35

BINARY_VERSION

The binary code also contains the binary version to allow parsing potential different formats in the future.

0x02

NAMESPACE

This sector after MAGIC_BYTES and BINARY_VERSION contains the reference namespace of the code. This is the namespace used in the source code, e.g.:

constant "MyNamespace" { ... }
contract "MyNamespace" { ... }
circuit  "MyNamespace" { ... }

The string is serialized with variable-integer encoding.

.constant

The constants in the .constant section are declared with their type and name, so that the VM knows how to search for the builtin constant and add it to the stack.

.literal

The literals in the .literal section are currently unsigned integers that get parsed into a u64 type inside the VM. In the future this could be extended with signed integers, and strings.

.contract

The .contract section holds the circuit witness values in the form of WITNESS_TYPE. Their stack index is incremented for each witness as they're kept in order like in the source file. The witnesses that are of the same type as the circuit itself (typically Base) will be loaded into the circuit as private values using the Halo2 load_private API.

.circuit

The .circuit section holds the procedural logic of the ZK proof. In here we have statements with opcodes that are executed as understood by the VM. The statements are in the form of:

OPCODE ARG_NUM STACK_TYPE STACK_INDEX ... STACK_TYPE STACK_INDEX

where:

ElementDescription
OPCODEThe opcode we wish to execute
ARG_NUMThe number of arguments given to this opcode
(Note the VM should be checking the correctness of this as well)
STACK_TYPEType of the stack to do lookup from (variables or literals)
(This is prepended to every STACK_INDEX)
STACK_INDEXThe location of the argument on the stack.
(This is supposed to be repeated ARG_NUM times)

In case an opcode has a return value, the value shall be pushed to the stack and become available for later references.

.debug

TBD

Syntax Reference

Variable Types

TypeDescription
EcPointElliptic Curve Point.
EcFixedPointElliptic Curve Point (constant).
EcFixedPointBaseElliptic Curve Point in Base Field (constant).
BaseBase Field Element.
BaseArrayBase Field Element Array.
ScalarScalar Field Element.
ScalarArrayScalar Field Element Array.
MerklePathMerkle Tree Path.
Uint32Unsigned 32 Bit Integer.
Uint64Unsigned 64 Bit Integer.

Literal Types

TypeDescription
Uint64Unsigned 64 Bit Integer.

Opcodes

OpcodeDescription
EcAddElliptic Curve Addition.
EcMulElliptic Curve Multiplication.
EcMulBaseElliptic Curve Multiplication with Base.
EcMulShortElliptic Curve Multiplication with a u64 wrapped in a Scalar.
EcGetXGet X Coordinate of Elliptic Curve Point.
EcGetYGet Y Coordinate of Elliptic Curve Point.
PoseidonHashPoseidon Hash of N Elements.
MerkleRootCompute a Merkle Root.
BaseAddBase Addition.
BaseMulBase Multiplication.
BaseSubBase Subtraction.
WitnessBaseWitness an unsigned integer into a Base.
RangeCheckPerform a (either 64bit or 253bit) range check over some Base
LessThanStrictStrictly compare if Base a is lesser than Base b
LessThanLooseLoosely compare if Base a is lesser than Base b
BoolCheckEnforce that a Base fits in a boolean value (either 0 or 1)
ConstrainEqualBaseConstrain equality of two Base elements from the stack
ConstrainEqualPointConstrain equality of two EcPoint elements from the stack
ConstrainInstanceConstrain a Base to a Circuit's Public Input.

Built-in Opcode Wrappers

OpcodeFunctionReturn
EcAddec_add(EcPoint a, EcPoint b)(EcPoint c)
EcMulec_mul(EcPoint a, EcPoint c)(EcPoint c)
EcMulBaseec_mul_base(Base a, EcFixedPointBase b)(EcPoint c)
EcMulShortec_mul_short(Base a, EcFixedPointShort b)(EcPoint c)
EcGetXec_get_x(EcPoint a)(Base x)
EcGetYec_get_y(EcPoint a)(Base y)
PoseidonHashposeidon_hash(Base a, ..., Base n)(Base h)
MerkleRootmerkle_root(Uint32 i, MerklePath p, Base a)(Base r)
BaseAddbase_add(Base a, Base b)(Base c)
BaseMulbase_mul(Base a, Base b)(Base c)
BaseSubbase_sub(Base a, Base b)(Base c)
WitnessBasewitness_base(123)(Base a)
RangeCheckrange_check(64, Base a)()
LessThanStrictless_than_strict(Base a, Base b)()
LessThanLooseless_than_loose(Base a, Base b)()
BoolCheckbool_check(Base a)()
ConstrainEqualBaseconstrain_equal_base(Base a, Base b)()
ConstrainEqualPointconstrain_equal_point(EcPoint a, EcPoint b)()
ConstrainInstanceconstrain_instance(Base a)()

Decoding the bincode

An example decoder implementation can be found in zkas' decoder.rs module.