Md spec

.gitignore

@@ -3,6 +3,12 @@
 .vscode
 .DS_Store
 
+# Python
+__pycache__/
+*.pyc
+*.pyo
+.venv/
+
 # Compiled ELF artifacts (built by CI/make)
 executor/program_artifacts/
 

docs/spec/about_ecalls.md

@@ -0,0 +1,13 @@
+# About ECALL
+
+ECALLs provide system-level functionalities to the guest program.
+
+When `ECALL` is executed, it is assumed that: - register `A7` contains the system call number
+
+- the arguments are located in registers `A0`-`A6`, and - the return value is written to `A0`, where `A0`-`A7` are symbolic names for the registers `x10`-`x17`
+
+## ECALL number overview
+
+We provide a list of supported ECALL numbers. Negative numbers (represented as 2s complement 64-bit numbers), are used for our own custom accelerators/extensions.
+
+/ 64: `write` ([commit]) / 93: `exit` ([halt]) / -1: `SHA256` ([sha256]) / -2: `KECCAK` ([keccak])

docs/spec/add.md

@@ -0,0 +1,56 @@
+# ADD/SUB Template
+
+For ease of notation, we moreover introduce the  constraint template $
+
+$ in both conditional and unconditional versions. It constrains that ``diff` equiv `lhs` - `rhs` (mod 2^64)` when the expression `cond` is non-zero.
+
+## Variables
+
+This template introduces  interaction(s).
+
+### Input
+
+| Name | Type | Description |
+|------|------|-------------|
+| `lhs` | `DWordWL` | left-hand operator |
+| `rhs` | `DWordWL` | right-hand operator |
+
+### Output
+
+| Name | Type | Description |
+|------|------|-------------|
+| `sum` | `DWordWL` | $`lhs` + `rhs`$ |
+
+### Virtual
+
+| Name | Type | Description |
+|------|------|-------------|
+| `carry` | `Bit[2]` | Carry values used to constrain the addition |
+
+**Definition of `carry`:**
+```
+carry (when iter=0) := 2^-32 * (lhs[0] + rhs[0] - sum[0])
+carry (when iter=1) := 2^-32 * (lhs[1] + rhs[1] + carry[0] - sum[1])
+```
+
+### Condition
+
+| Name | Type | Description |
+|------|------|-------------|
+| `cond` | `BaseField` | Whether the relation should be enforced ($eq.not 0$) or not ($0$). |
+
+## Assumptions
+
+| Tag | Range | Description |
+|-----|-------|-------------|
+| `ADD-A1.i` | i ∈ [0, 1] | `IS_WORD[lhs[i]]` |
+| `ADD-A2.i` | i ∈ [0, 1] | `IS_WORD[rhs[i]]` |
+| `ADD-A3.i` | i ∈ [0, 1] | `IS_WORD[sum[i]]` |
+
+## Constraints
+
+This template introduces the following constraints
+
+| Tag | Range | Description |
+|-----|-------|-------------|
+| `ADD-C1.i` | i ∈ [0, 1] | cond ⇒ `IS_BIT<carry[i]>` |

docs/spec/bitwise.md

@@ -0,0 +1,69 @@
+# BITWISE Chips
+
+The  chips deal with precomputed lookup tables for bitwise boolean operations and convenience functionalities over small domains.
+
+## Variables
+
+The  chip is comprised of  variables that are expressed using  columns. Of these, the _input_ and _output_ variables ( in total) are precomputed.
+
+### Input
+
+| Name | Type | Description |
+|------|------|-------------|
+| `X` | `Byte` |  |
+| `Y` | `Byte` |  |
+| `Z` | `B4` |  |
+
+### Output
+
+| Name | Type | Description |
+|------|------|-------------|
+| `AND` | `Byte` | the binary AND of `X` and `Y` |
+| `OR` | `Byte` | the binary OR of `X` and `Y` |
+| `XOR` | `Byte` | the binary XOR of `X` and `Y` |
+| `MSB8` | `Bit` | the most significant bit of `X` |
+| `MSB16` | `Bit` | the most significant bit of `Y` |
+| `ZERO` | `Bit` | whether $`X` = 0$, $`Y` = 0$ and $`Z` = 0$. |
+| `SLL` | `Half` | `X\|\|Y` logically left-shifted by `Z`: $((`X` + 256`Y`) `<<` `Z`) mod 2^16$ |
+| `SLLC` | `Half` | `X\|\|Y` logically right-shifted by `Z`: $(`X` + 256`Y`) `>>` (16 - `Z`)$ |
+
+### Multiplicity
+
+| Name | Type | Description |
+|------|------|-------------|
+| `μ_AND` | `BaseField` |  |
+| `μ_OR` | `BaseField` |  |
+| `μ_XOR` | `BaseField` |  |
+| `μ_MSB8` | `BaseField` |  |
+| `μ_MSB16` | `BaseField` |  |
+| `μ_ZERO` | `BaseField` |  |
+| `μ_IS_BYTE` | `BaseField` |  |
+| `μ_ARE_BYTES` | `BaseField` |  |
+| `μ_IS_HALF` | `BaseField` |  |
+| `μ_IS_B20` | `BaseField` |  |
+| `μ_HWSL` | `BaseField` |  |
+
+*Note*: This table contains one row for every possible value of `(X, Y, Z)`. As such, it has length `2^8 dot 2^8 dot 2^4 = 2^(20)`.
+
+We use the ALU operation descriptors from [decode] to identify the operations in the `BYTE_ALU` interaction. Since each of the three columns is only `2^16` rows long, they can be combined in a single `2^20` column (with room to spare).
+
+## Lookup
+
+This chip adds the following interactions to the lookup:
+
+| Tag | Description | Multiplicity |
+|-----|-------------|--------------|
+| `BITWISE-C1` | `BYTE_ALU[AND; ⧼AND⧽, X, Y]` | -μ_AND |
+| `BITWISE-C2` | `BYTE_ALU[OR; ⧼OR⧽, X, Y]` | -μ_OR |
+| `BITWISE-C3` | `BYTE_ALU[XOR; ⧼XOR⧽, X, Y]` | -μ_XOR |
+| `BITWISE-C4` | `MSB8[MSB8; X]` | -μ_MSB8 |
+| `BITWISE-C5` | `MSB16[MSB16; X + 256 * Y]` | -μ_MSB16 |
+| `BITWISE-C6` | `ZERO[ZERO; X + 256 * Y + 65536 * Z]` | -μ_ZERO |
+| `BITWISE-C7` | `ARE_BYTES[X, Y]` | -μ_ARE_BYTES |
+| `BITWISE-C8` | `IS_HALF[X + 256 * Y]` | -μ_IS_HALF |
+| `BITWISE-C9` | `IS_B20[X + 256 * Y + 65536 * Z]` | -μ_IS_B20 |
+| `BITWISE-C10` | `HWSL[[SLL, SLLC]; X + 256 * Y, Z]` | -μ_HWSL |
+
+## Notes/Optimizations
+
+The following ideas may prove to be optimizations for the  chip: + Drop `MSB8` column, and instead define the `MSB8` lookup as `MSB8<X> := MSB16[256X]`. Note: currently, `MSB8` also implicity range checks the input `X` (the lookup fails if `X` is not a `Byte`). This optimization should only be executed when all chips leveraging `MSB8` do _not_ need this implicit range check. + Place the 16-bit (`AND`, `OR`, `XOR`, `MSB16`, etc.) and 20-bit (`HWSL`, `IS_B20`, `ZERO`) lookups in separate tables.

docs/spec/branch.md

@@ -0,0 +1,104 @@
+# BRANCH Chip
+
+The  chip computes the target address of a branching instruction.
+
+## Variables
+
+The  chip is comprised of  variables that are expressed using  columns and leverages  interaction(s):
+
+### Input
+
+| Name | Type | Description |
+|------|------|-------------|
+| `pc` | `DWordWL` | The current pc, used as base address when `!JALR` |
+| `offset` | `DWordWL` | The offset from the base address to jump to |
+| `register` | `DWordWL` | The base address to use when `JALR` |
+| `JALR` | `Bit` | Selects between `pc` and `register` as base address, needed for the `JALR` instruction |
+
+### Output
+
+| Name | Type | Description |
+|------|------|-------------|
+| `next_pc_high` | `Half[3]` | The upper part of the next pc |
+| `next_pc_low` | `Byte[2]` | The lower part of the next pc |
+
+### Auxiliary
+
+| Name | Type | Description |
+|------|------|-------------|
+| `unmasked_low_byte` | `Byte` | The low byte of the next pc, before masking the LSB. Used to constraint the raw addition. |
+
+### Virtual
+
+| Name | Type | Description |
+|------|------|-------------|
+| `next_pc_unmasked` | `DWordWL` | The combination of `next_pc_high`, `next_pc_low[1]` and `unmasked_low_byte` to constrain the addition. This is the computed value for the next pc, before masking off the LSB as required by the ISA. |
+| `next_pc` | `DWordWL` | The computed next pc, after masking off the LSB as required by the ISA. |
+
+**Definition of `next_pc_unmasked`:**
+```
+next_pc_unmasked (when iter=0) := 2^16 * next_pc_high[0] + 2^8 * next_pc_low[1] + unmasked_low_byte
+next_pc_unmasked (when iter=1) := 2^16 * next_pc_high[2] + next_pc_high[1]
+```
+
+**Definition of `next_pc`:**
+```
+next_pc (when iter=0) := 2^16 * next_pc_high[0] + 2^8 * next_pc_low[1] + next_pc_low[0]
+next_pc (when iter=1) := 2^16 * next_pc_high[2] + next_pc_high[1]
+```
+
+### Multiplicity
+
+| Name | Type | Description |
+|------|------|-------------|
+| `μ` | `Bit` |  |
+
+## Assumptions
+
+| Tag | Range | Description |
+|-----|-------|-------------|
+| `BRANCH-A1.i` | i ∈ [0, 1] | `pc` is range checked, `IS_WORD[pc[i]]` |
+| `BRANCH-A2` |  | `offset` is range checked, `IS_WORD[offset]` |
+| `BRANCH-A3.i` | i ∈ [0, 1] | `register` is range checked, `IS_WORD[register[i]]` |
+| `BRANCH-A4` |  | `IS_BIT<JALR>` |
+
+Some of the assumptions can be checked with only arithmetic constraints, so we provide these below.
+
+| Tag | Description |
+|-----|-------------|
+| `BRANCH-C1` | `IS_BIT<JALR>` |
+
+## Constraints
+
+We constrain `next_pc` to be ``base_address` + `offset``, where `base_address` equals `pc` when ``JALR` = 0` and `register` otherwise.
+
+The range checks on `unmasked_low_byte` and `next_pc_low[0]` are performed implicitly by the `AND_BYTE` lookup.
+
+| Tag | Range | Description | Multiplicity |
+|-----|-------|-------------|--------------|
+| `BRANCH-C2` |  | 1 - JALR ⇒ `ADD<next_pc_unmasked; pc, offset::DWordWL>` |  |
+| `BRANCH-C3` |  | JALR ⇒ `ADD<next_pc_unmasked; register, offset::DWordWL>` |  |
+| `BRANCH-C4` |  | μ ⇒ `IS_BYTE<next_pc_low[1]>` |  |
+| `BRANCH-C5` |  | `BYTE_ALU[next_pc_low[0]; ⧼AND⧽, unmasked_low_byte, 254]` | μ |
+| `BRANCH-C6.i` | i ∈ [0, 2] | `IS_HALF[next_pc_high[i]]` | μ |
+
+This chip contributes the following to the lookup argument.
+
+| Tag | Description | Multiplicity |
+|-----|-------------|--------------|
+| `BRANCH-C7` | `BRANCH[next_pc; pc, offset, register, JALR]` | -μ |
+
+## Padding
+
+The table can be padded to the next power of two with the following value assignments:
+
+| Column | Padding value |
+|--------|---------------|
+| `pc` | `0` |
+| `offset` | `0` |
+| `register` | `0` |
+| `JALR` | `0` |
+| `next_pc_high` | `[0, 0, 0]` |
+| `next_pc_low` | `0` |
+| `unmasked_low_byte` | `0` |
+| `μ` | `0` |

docs/spec/bytewise.md

@@ -0,0 +1,46 @@
+# BYTEWISE Chip
+
+The  chip is an ALU chip that decomposes the input `DWordWL` values into bytes and performs a `BITWISE` operation pairwise (AND, OR, XOR). The `BITWISE` lookup inherently performs a range check, so no further constraints are necessary.
+
+## Variables
+
+The  chip is comprised of  variables that are expressed using  columns and leverages  interaction(s):
+
+### Input
+
+| Name | Type | Description |
+|------|------|-------------|
+| `a` | `DWordBL` | The first input |
+| `b` | `DWordBL` | The second input |
+| `op` | `Byte` | The operation to perform |
+
+### Output
+
+| Name | Type | Description |
+|------|------|-------------|
+| `res` | `DWordBL` | The result |
+
+### Multiplicity
+
+| Name | Type | Description |
+|------|------|-------------|
+| `μ` | `BaseField` |  |
+
+## Constraints
+
+| Tag | Range | Description | Multiplicity |
+|-----|-------|-------------|--------------|
+| `BYTEWISE-C1.i` | i ∈ [0, 7] | `BYTE_ALU[res[i]; op, a[i], b[i]]` | μ |
+| `BYTEWISE-C2` |  | `ALU[res::DWordWL; a::DWordWL, b::DWordWL, op]` | -μ |
+
+## Padding
+
+The chip can be padded with the following values:
+
+| Column | Padding value |
+|--------|---------------|
+| `a` | `0` |
+| `b` | `0` |
+| `op` | `0` |
+| `res` | `0` |
+| `μ` | `0` |