|
|
@@ -4,15 +4,14 @@ 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 three sections: `constant`, `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.
|
|
|
+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 everything on the same stack, so we avoid having to
|
|
|
-deal with different types. Instead, we rely that the compiler does
|
|
|
-a proper parse and analysis of the source code, so we are sure that
|
|
|
-in the VM, when referenced, the types shall be correct.
|
|
|
+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:
|
|
|
|
|
|
@@ -23,13 +22,17 @@ BINARY_VERSION
|
|
|
CONSTANT_TYPE CONSTANT_NAME
|
|
|
CONSTANT_TYPE CONSTANT_NAME
|
|
|
...
|
|
|
+.literal
|
|
|
+LITERAL
|
|
|
+LITERAL
|
|
|
+...
|
|
|
.contract
|
|
|
WITNESS_TYPE
|
|
|
WITNESS_TYPE
|
|
|
...
|
|
|
.circuit
|
|
|
-OPCODE ARG_NUM STACK_INDEX ... STACK_INDEX
|
|
|
-OPCODE ARG_NUM STACK_INDEX ... STACK_INDEX
|
|
|
+OPCODE ARG_NUM STACK_TYPE STACK_INDEX ... STACK_TYPE STACK_INDEX
|
|
|
+OPCODE ARG_NUM STACK_TYPE STACK_INDEX ... STACK_TYPE STACK_INDEX
|
|
|
...
|
|
|
.debug
|
|
|
TBD
|
|
|
@@ -46,7 +49,7 @@ for our Rust implementation.
|
|
|
The magic bytes are the file signature consisting of four bytes used
|
|
|
to identify the zkas binary code. They consist of:
|
|
|
|
|
|
-> `0x0b` `0xxx` `0xb1` `0x35`
|
|
|
+> `0x0b` `0x01` `0xb1` `0x35`
|
|
|
|
|
|
|
|
|
### `BINARY_VERSION`
|
|
|
@@ -54,7 +57,7 @@ to identify the zkas binary code. They consist of:
|
|
|
The binary code also contains the binary version to allow parsing
|
|
|
potential different formats in the future.
|
|
|
|
|
|
-> `0x01`
|
|
|
+> `0x02`
|
|
|
|
|
|
### `.constant`
|
|
|
|
|
|
@@ -62,6 +65,12 @@ 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`
|
|
|
|
|
|
@@ -79,7 +88,7 @@ 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_INDEX ... STACK_INDEX`
|
|
|
+> `OPCODE ARG_NUM STACK_TYPE STACK_INDEX ... STACK_TYPE STACK_INDEX`
|
|
|
|
|
|
where:
|
|
|
|
|
|
@@ -88,6 +97,8 @@ where:
|
|
|
| `OPCODE` | The opcode we wish to execute |
|
|
|
| `ARG_NUM` | The number of arguments given to this opcode |
|
|
|
| | (Note the VM should be checking the correctness of this as well) |
|
|
|
+| `STACK_TYPE` | Type of the stack to do lookup from (variables or literals) |
|
|
|
+| | (This is prepended to every `STACK_INDEX`) |
|
|
|
| `STACK_INDEX` | The location of the argument on the stack. |
|
|
|
| | (This is supposed to be repeated `ARG_NUM` times) |
|
|
|
|
|
|
@@ -101,7 +112,7 @@ TBD
|
|
|
|
|
|
## Syntax Reference
|
|
|
|
|
|
-### Types
|
|
|
+### Variable Types
|
|
|
|
|
|
| Type | Description |
|
|
|
| ------------------ | ---------------------------------------------- |
|
|
|
@@ -116,6 +127,12 @@ TBD
|
|
|
| `Uint32` | Unsigned 32 Bit Integer. |
|
|
|
| `Uint64` | Unsigned 64 Bit Integer. |
|
|
|
|
|
|
+### Literal Types
|
|
|
+
|
|
|
+| Type | Description |
|
|
|
+| ------------------ | ---------------------------------------------- |
|
|
|
+| `Uint64` | Unsigned 64 Bit Integer.
|
|
|
+
|
|
|
### Opcodes
|
|
|
|
|
|
| Opcode | Description |
|
|
|
@@ -127,11 +144,13 @@ TBD
|
|
|
| `EcGetX` | Get X Coordinate of Elliptic Curve Point. |
|
|
|
| `EcGetY` | Get Y Coordinate of Elliptic Curve Point. |
|
|
|
| `PoseidonHash` | Poseidon Hash of N Elements. |
|
|
|
-| `CalculateMerkeRoot` | Compute a Merkle Root. |
|
|
|
+| `MerkleRoot` | Compute a Merkle Root. |
|
|
|
| `BaseAdd` | `Base` Addition. |
|
|
|
| `BaseMul` | `Base` Multiplication. |
|
|
|
| `BaseSub` | `Base` Subtraction. |
|
|
|
-| `GreaterThan` | Greater Than Operation of `Base`. |
|
|
|
+| `WitnessBase` | Witness an unsigned integer into a `Base`. |
|
|
|
+| `RangeCheck` | Perform a (either 64bit or 253bit) range check over some `Base` |
|
|
|
+| `LessThan` | Compare if `Base` a is lesser than `Base` b |
|
|
|
| `ConstrainInstance` | Constrain a `Base` to a Circuit's Public Input. |
|
|
|
|
|
|
### Built-in Opcode Wrappers
|
|
|
@@ -145,11 +164,13 @@ TBD
|
|
|
| `EcGetX` | `ec_get_x(EcPoint a)` | `(Base x)` |
|
|
|
| `EcGetY` | `ec_get_y(EcPoint a)` | `(Base y)` |
|
|
|
| `PoseidonHash` | `poseidon_hash(Base a, ..., Base n)` | `(Base h)` |
|
|
|
-| `CalculateMerkleRoot` | `calculate_merkle_root(Uint32 i, MerklePath p, Base a)` | `(Base r)` |
|
|
|
+| `MerkleRoot` | `merkle_root(Uint32 i, MerklePath p, Base a)` | `(Base r)` |
|
|
|
| `BaseAdd` | `base_add(Base a, Base b)` | `(Base c)` |
|
|
|
| `BaseMul` | `base_mul(Base a, Base b)` | `(Base c)` |
|
|
|
| `BaseSub` | `base_sub(Base a, Base b)` | `(Base c)` |
|
|
|
-| `GreaterThan` | `greater_than(Base a, Base b)` | `(Base gt)` |
|
|
|
+| `WitnessBase` | `witness_base(123)` | `(Base a)` |
|
|
|
+| `RangeCheck` | `range_check(64, Base a)` | `()` |
|
|
|
+| `LessThan` | `less_than(Base a, Base b)` | `()` |
|
|
|
| `ConstrainInstance` | `constrain_instance(Base a)` | `()` |
|
|
|
|
|
|
## Decoding the bincode
|
Luther Blissett