Merge branch 'master' into o1vm/extract-get-all-constraints-from-main

.github/workflows/mips-build.yml

@@ -0,0 +1,51 @@
+name: MIPS Build and Package
+
+on:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        rust_toolchain_version: ["1.74"]
+
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        submodules: 'recursive'
+
+    - name: Cache apt packages
+      id: apt-cache
+      uses: actions/cache@v4
+      with:
+        path: |
+          /var/cache/apt/archives/*.deb
+        key: ${{ runner.os }}-apt-${{ hashFiles('.github/workflows/mips-build.yml') }}
+
+    - name: Install MIPS tools
+      run: |
+        sudo apt-get update
+        sudo apt-get install -y binutils-mips-linux-gnu
+
+    - name: Build MIPS programs
+      run: make build-mips-programs
+
+    - name: Use shared Rust toolchain setting up steps
+      uses: ./.github/actions/toolchain-shared
+      with:
+        rust_toolchain_version: ${{ matrix.rust_toolchain_version }}
+
+    - name: Test elf_loader against mips programs
+      run: ./o1vm/test-gen-state-json.sh
+
+    - name: Create tar archive
+      run: |
+        cd o1vm/resources/programs/mips
+        tar -czf mips-binaries.tar.gz bin/
+
+    - name: Upload artifacts
+      uses: actions/upload-artifact@v4
+      with:
+        name: mips-binaries
+        path: o1vm/resources/programs/mips/mips-binaries.tar.gz

.gitignore

@@ -39,6 +39,13 @@ o1vm/op-program-db*
 o1vm/state.json
 meta.json
 state.json
+o1vm/meta_test.json
 
 # Directory for the RISC-V 32bits toolchain
-_riscv32-gnu-toolchain
+_riscv32-gnu-toolchain
+o1vm/resources/programs/riscv32im/bin/*.o
+
+# modified assembly files generated from cannon's open mips tests
+o1vm/resources/programs/mips/src
+# mips binary files for open mips tests
+o1vm/resources/programs/mips/bin

Makefile

@@ -18,6 +18,13 @@ O1VM_RISCV32IM_BIN_DIR = ${O1VM_RESOURCES_PATH}/riscv32im/bin
 O1VM_RISCV32IM_BIN_FILES = $(patsubst ${O1VM_RISCV32IM_SOURCE_DIR}/%.S,${O1VM_RISCV32IM_BIN_DIR}/%.o,${O1VM_RISCV32IM_SOURCE_FILES})
 RISCV32_AS_FLAGS = --warn --fatal-warnings
 
+OPTIMISM_MIPS_SOURCE_DIR = $(shell pwd)/o1vm/ethereum-optimism/cannon/mipsevm/open_mips_tests/test
+OPTIMISM_MIPS_SOURCE_FILES = $(wildcard ${OPTIMISM_MIPS_SOURCE_DIR}/*.asm)
+O1VM_MIPS_SOURCE_DIR = ${O1VM_RESOURCES_PATH}/mips/src
+O1VM_MIPS_SOURCE_FILES = $(patsubst ${OPTIMISM_MIPS_SOURCE_DIR}/%.asm,${O1VM_MIPS_SOURCE_DIR}/%.asm,${OPTIMISM_MIPS_SOURCE_FILES})
+O1VM_MIPS_BIN_DIR = ${O1VM_RESOURCES_PATH}/mips/bin
+O1VM_MIPS_BIN_FILES = $(patsubst ${O1VM_MIPS_SOURCE_DIR}/%.asm,${O1VM_MIPS_BIN_DIR}/%.o,${O1VM_MIPS_SOURCE_FILES})
+
 # Default target
 all: release
 
@@ -47,8 +54,9 @@ install-test-deps: ## Install test dependencies
 
 
 clean: ## Clean the project
-		cargo clean
-		rm -rf $(O1VM_RISCV32IM_BIN_FILES)
+		@cargo clean
+		@rm -rf $(O1VM_RISCV32IM_BIN_FILES)
+		@rm -rf $(O1VM_MIPS_BIN_DIR)
 
 
 build: ## Build the project
@@ -166,7 +174,31 @@ ${O1VM_RISCV32IM_BIN_DIR}/%.o: ${O1VM_RISCV32IM_SOURCE_DIR}/%.S
 		${RISCV32_TOOLCHAIN_PATH}/build/bin/riscv32-unknown-elf-ld -s -o $(basename $@) $@
 		@echo ""
 
+build-mips-programs: ${O1VM_MIPS_SOURCE_FILES} ${O1VM_MIPS_BIN_FILES} ## Build all MIPS programs written for the o1vm
+
+${O1VM_MIPS_SOURCE_DIR}/%.asm: ${OPTIMISM_MIPS_SOURCE_DIR}/%.asm
+		@mkdir -p ${O1VM_MIPS_SOURCE_DIR}
+		@echo "Transforming $< to $@, making it compatible for o1vm"
+		@sed \
+				-e '/\.balign 4/d' \
+				-e '/\.set\s*noreorder/d' \
+				-e '/\.ent\s*test/d' \
+				-e '/\.end test/d' \
+				-e 's/\.section .test, "x"/.section .text/' \
+				-e 's/\s*\.section .text/.section .text/' \
+				-e 's/\.global test/.global __start/' \
+				-e "s/^\s*\.global __start/.global __start/" \
+				-e "s/test\:/__start:/" \
+				-e "/\.global __start/a\\" \
+				$< > $@
+
+${O1VM_MIPS_BIN_DIR}/%.o: ${O1VM_MIPS_SOURCE_DIR}/%.asm
+		@echo "Building the MIPS binary: $(basename $@) using $<"
+		@mkdir -p ${O1VM_MIPS_BIN_DIR}
+		@mips-linux-gnu-as -defsym big_endian=1 -march=mips32r2 -o $@ $<
+		@mips-linux-gnu-ld -s -o $(basename $@) $@
+
 fclean: clean ## Clean the tooling artefacts in addition to running clean
 		rm -rf ${RISCV32_TOOLCHAIN_PATH}
 
-.PHONY: all setup install-test-deps clean build release test-doc test-doc-with-coverage test test-with-coverage test-heavy test-heavy-with-coverage test-all test-all-with-coverage nextest nextest-with-coverage nextest-heavy nextest-heavy-with-coverage nextest-all nextest-all-with-coverage format lint generate-test-coverage-report generate-doc setup-riscv32-toolchain help fclean build-riscv32-programs
+.PHONY: all setup install-test-deps clean build release test-doc test-doc-with-coverage test test-with-coverage test-heavy test-heavy-with-coverage test-all test-all-with-coverage nextest nextest-with-coverage nextest-heavy nextest-heavy-with-coverage nextest-all nextest-all-with-coverage format lint generate-test-coverage-report generate-doc setup-riscv32-toolchain help fclean build-riscv32-programs build-mips-programs

README.md

@@ -88,6 +88,8 @@ You can visualize the documentation by opening the file `target/doc/index.html`.
   This workflow runs benchmarks when a pull request is labeled with "benchmark." It sets up the Rust and OCaml environments, installs necessary tools, and executes cargo criterion benchmarks on the kimchi crate. The benchmark results are then posted as a comment on the pull request for review.
 - [Deploy Specifications & Docs to GitHub Pages](.github/workflows/gh-page.yml).
   When CI passes on master, the documentation built from the rust code will be available by this [link](https://o1-labs.github.io/proof-systems/rustdoc) and the book will be available by this [link](https://o1-labs.github.io/proof-systems).
+- [MIPS Build and Package](.github/workflows/mips-build.yml)
+  This workflow runs the assembler and linker on the programs from the OpenMips test suite, and provides a link where you can download the artifacts (recommended if you don't have / can't install the required MIPS tooling). This workflow also runs the o1vm ELF parser on the artifacts to check that our parsing is working. Currently it is run via manual trigger only -- you can find the trigger in the [GitHub actions tab](https://github.com/o1-labs/proof-systems/actions/workflows/mips-build.yml) and the link to the artifacts will appear in logs of the `Upload Artifacts` stage.
 
 ## Nix for Dependencies (WIP)
 

book/src/SUMMARY.md

@@ -17,7 +17,7 @@
 - [Commitments](./fundamentals/zkbook_commitment.md)
 - [Polynomial Commitments](./plonk/polynomial_commitments.md)
   - [Inner Product Argument](./plonk/inner_product.md)
-  - [Different Functionnalities](./plonk/inner_product_api.md)
+  - [Different Functionalities](./plonk/inner_product_api.md)
 - [Two Party Computation](./fundamentals/zkbook_2pc/overview.md)
   - [Garbled Circuits](./fundamentals/zkbook_2pc/gc.md)
     - [Basics](./fundamentals/zkbook_2pc/basics.md)

book/src/pickles/diagrams.md

@@ -7,7 +7,7 @@ The legend of the diagrams is quite straightforward:
   - `MFNStep`/`MFNWrap` is an abbreviation from `MessagesForNextStep` and `MessagesForNextWrap` that is used for brevity. Most other datatypes are exactly the same as in the codebase.
 - The blue boxes are computations. Sometimes, when the computation is trivial or only vaguely indicated, it is denoted as a text sign directly on an arrow.
 - Arrows are blue by default and denote moving a piece of data from one place to another with no (or very little) change. Light blue arrows are denoting witness query that is implemented through the `handler` mechanism. The "chicken foot" connector means that this arrow accesses just one field in an array: such an arrow could connect e.g. a input field of type `old_a: A` in a structure `Vec<(A,B)>` to an output `new_a: A`, which just means that we are inside a `for` loop and this computation is done for all the elemnts in the vector/array.
-- Colour of the field is sometimes introduced and denotes how many steps ago was this piece of data created. The absense of the colour means either that (1) the data structure contains different subfields of different origin, or that (2) it was not coloured but it could be. The colours are assigned according to the following convention:
+- Colour of the field is sometimes introduced and denotes how many steps ago was this piece of data created. The absence of the colour means either that (1) the data structure contains different subfields of different origin, or that (2) it was not coloured but it could be. The colours are assigned according to the following convention:
 
 ![](./pickles_structure_legend_1.svg)
 

book/src/pickles/overview.md

@@ -27,4 +27,4 @@ We note that the Step circuit may repeat items 2-3 to handle the following case:
 
 The accumulator is an abstraction introduced for the purpose of this diagram. In practice, each kimchi proof consists of (1) commitments to polynomials, (2) evaluations of them, (3) and the opening proof. What we refer to as accumulator here is actually the commitment inside the opening proof. It is called `sg` in the implementation and is semantically a polynomial commitment to `h(X)` (`b_poly` in the code) --- the poly-sized polynomial that is built from IPA challenges. It's a very important polynomial -- it can be evaluated in log time, but the commitment verification takes poly time, so the fact that `sg` is a commitment to `h(X)` is never proven inside the circuit. For more details, see [Proof-Carrying Data from Accumulation Schemes](https://eprint.iacr.org/2020/499.pdf), Appendix A.2, where `sg` is called `U`.
 
-In pickles, what we do is that we "absorb" this commitment `sg` from the previous step while creating a new proof. That is, for example, Step 1 will produce this commitment that is denoted as `acc1` on the diagram, as part of its opening proof, and Step 2 will absorb this commitment. And this "absorbtion" is what Wrap 2 will prove (and, partially, Step 3 will also refer to the challenges used to build `acc1`, but this detail is completely avoided in this overview). In the end, `acc2` will be the result of Step 2, so in a way `acc2` "aggregates" `acc1` which somewhat justifies the language used.
+In pickles, what we do is that we "absorb" this commitment `sg` from the previous step while creating a new proof. That is, for example, Step 1 will produce this commitment that is denoted as `acc1` on the diagram, as part of its opening proof, and Step 2 will absorb this commitment. And this "absorption" is what Wrap 2 will prove (and, partially, Step 3 will also refer to the challenges used to build `acc1`, but this detail is completely avoided in this overview). In the end, `acc2` will be the result of Step 2, so in a way `acc2` "aggregates" `acc1` which somewhat justifies the language used.

book/src/plonk/zkpm.md

@@ -58,7 +58,7 @@ $$
   = Z(\omega h)[(a(h) + \beta S_{\sigma1}(h) + \gamma)(b(h) + \beta S_{\sigma2}(h) + \gamma)(c(h) + \beta S_{\sigma3}(h) + \gamma)]$$
 
 
-The modified permuation checks that ensures that the check is performed only on all the values except the last $k$ elements in the witness polynomials are as follows.
+The modified permutation checks that ensures that the check is performed only on all the values except the last $k$ elements in the witness polynomials are as follows.
 
 * For all $h \in H$, $L_1(h)(Z(h) - 1) = 0$
 * For all $h \in \blue{H\setminus \{h_{n-k}, \ldots, h_n\}}$, $$\begin{aligned}  & Z(h)[(a(h) + \beta h + \gamma)(b(h) + \beta k_1 h + \gamma)(c(h) + \beta k_2 h + \gamma)] \\

book/src/snarky/kimchi-backend.md

@@ -107,7 +107,7 @@ It is the role of the `add_constrain` logic to enforce that at this point consta
 This is done by adding enough generic gates (using the `reduce_lincom()` or `reduce_to_var()` functions).
 
 ```admonish
-This is a remnant of an optimization targetting R1CS (in which additions are for free).
+This is a remnant of an optimization targeting R1CS (in which additions are for free).
 An issue with this approach is the following: imagine that two circuit variables are created from the same circuit variable, imagine also that the original circuit variable contained a long AST, then both variables might end up creating the same constraints to convert that AST.
 Currently, snarkyjs and pickles expose a `seal()` function that allows you to reduce this issue, at the cost of some manual work and mental tracking on the developer.
 We should probably get rid of this, while making sure that we can continue to optimize generic gates 
@@ -142,7 +142,7 @@ The `finalization()` function of the kimchi backend does the following:
 
 * add as many generic rows as there are public inputs.
 * construct the permutation 
-* computes a cache of the circuit (TODO: this is so unecessary)
+* computes a cache of the circuit (TODO: this is so unnecessary)
 * and other things that are not that important
 
 ## Witness generation

book/src/snarky/snarky-wrapper.md

@@ -48,7 +48,7 @@ The wrapper is designed to be used in different ways, depending on the fields se
 
 ```admonish
 Ideally, we would like to only run this once and obtain a result that's an immutable compiled artifact.
-Currently, `public_input`, `private_input`, `eval_constriants`, `next_var`, and `mode` all need to be mutable.
+Currently, `public_input`, `private_input`, `eval_constraints`, `next_var`, and `mode` all need to be mutable.
 In the future these should be passed as arguments to functions, and should not exist in the state.
 ```
 

book/src/snarky/vars.md

@@ -18,7 +18,7 @@ where
     /// A constant.
     Constant(F),
 
-    /// A variable that can be refered to via a `usize`.
+    /// A variable that can be referred to via a `usize`.
     Var(usize),
 
     /// The addition of two other [FieldVar]s.
@@ -65,7 +65,7 @@ In some situations, we might not want to constrain the
 In general, a circuit variable only gets constrained by an assertion call like `assert` or `assert_equals`.
 
 When variables are added together, or scaled, they do not directly get constrained. 
-This is due to optimizations targetting R1CS (which we don't support anymore) that were implemented in the original snarky library, and that we have kept in snarky-rs.
+This is due to optimizations targeting R1CS (which we don't support anymore) that were implemented in the original snarky library, and that we have kept in snarky-rs.
 
 Imagine the following example:
 

o1vm/README-optimism.md

@@ -3,7 +3,7 @@
 Install the first dependencies:
 ```
 sudo apt update
-# chrony will ensure the system clock is open to date
+# chrony will ensure the system clock is up to date
 sudo apt install build-essential git vim chrony ufw -y
 ```
 

o1vm/README.md

@@ -55,7 +55,7 @@ gvm use go1.21s
 ```
 
 You also will need to install the [Foundry](https://getfoundry.sh/) toolkit
-in order to utilize applicaitons like `cast`.
+in order to utilize applications like `cast`.
 
 ```shell
 foundryup

o1vm/resources/programs/riscv32im/src/add_1.S

@@ -0,0 +1,29 @@
+.section .text
+.globl _start
+
+_start:
+    # Initialize registers
+    li t0, 0          # t0 will hold the running total (initialize to 0)
+    li t1, 1          # First number
+    li t2, 2          # Second number
+    li t3, 3          # Third number
+    li t4, 4          # Fourth number
+    li t5, 5          # Fifth number
+
+    # Perform additions
+    add t0, t0, t1    # t0 = t0 + t1 (0 + 1)
+    add t0, t0, t2    # t0 = t0 + t2 (1 + 2)
+    add t0, t0, t3    # t0 = t0 + t3 (3 + 3)
+    add t0, t0, t4    # t0 = t0 + t4 (6 + 4)
+    add t0, t0, t5    # t0 = t0 + t5 (10 + 5)
+
+    # Custom exit syscall
+    li a0, 0          # Set a0 to 0
+    li a1, 0          # Set a1 to 0
+    li a2, 0          # Set a2 to 0
+    li a3, 0          # Set a3 to 0
+    li a4, 0          # Set a4 to 0
+    li a5, 0          # Set a5 to 0
+    li a6, 0          # Set a6 to 0
+    li a7, 42         # Set a7 to 42 (custom ecall number)
+    ecall             # Trigger syscall

o1vm/resources/programs/riscv32im/src/add_2.S

@@ -0,0 +1,32 @@
+.section .text
+.globl _start
+
+_start:
+    # Initialize registers with some numbers
+    li t0, 123       # First number
+    li t1, 456       # Second number
+    li t2, 789       # Third number
+
+    # Perform first addition
+    add t3, t0, t1   # t3 = t0 + t1 (123 + 456 = 579)
+
+    # Perform second addition
+    add t4, t3, t2   # t4 = t3 + t2 (579 + 789 = 1368)
+
+    # Add all numbers in a more complex way for redundancy
+    add t5, t0, t2   # t5 = t0 + t2 (123 + 789 = 912)
+    add t6, t1, t5   # t6 = t1 + t5 (456 + 912 = 1368)
+
+    # Ensure final result matches expectations
+    add t6, t4, x0   # t6 = t4 + x0 (Copy t4 to t6 for validation)
+
+    # Custom exit syscall
+    li a0, 0         # Set a0 to 0
+    li a1, 0         # Set a1 to 0
+    li a2, 0         # Set a2 to 0
+    li a3, 0         # Set a3 to 0
+    li a4, 0         # Set a4 to 0
+    li a5, 0         # Set a5 to 0
+    li a6, 0         # Set a6 to 0
+    li a7, 42        # Set a7 to 42 (custom ecall number)
+    ecall            # Trigger syscall

o1vm/resources/programs/riscv32im/src/add_overflow.S

@@ -0,0 +1,31 @@
+# The addition performed by `add` is simply a bit-wise addition
+# The lowest 32 bits are kept, and no overflow bit is kept.
+.section .text
+.globl _start
+
+_start:
+    # Large positive values
+    # It is equal to
+    # 0b01111111111111111111111111111111 +
+    # 0b00000000000000000000000000000001 =
+    # 0b10000000000000000000000000000000 =
+    li t0, 2147483647    # t0 = 2147483647 (Max 32-bit signed int)
+    li t1, 1             # t1 = 1
+    add t2, t0, t1       # t2 = t0 + t1
+
+    # 0b11111111111111111111111111111111 +
+    # 0b00000000000000000000000000000001 =
+    # 0b00000000000000000000000000000000 =
+    li t3, 0b11111111111111111111111111111111
+    add t4, t3, t1       # t4 = t3 + t1 (Expected: overflow, wrap around)
+
+    # Custom exit syscall
+    li a0, 0
+    li a1, 0
+    li a2, 0
+    li a3, 0
+    li a4, 0
+    li a5, 0
+    li a6, 0
+    li a7, 42
+    ecall

o1vm/resources/programs/riscv32im/src/add_sub_swap.S

@@ -0,0 +1,22 @@
+.section .text
+.globl _start
+
+_start:
+    li t0, 5             # t0 = 5
+    li t1, 10            # t1 = 10
+
+    # Swap t0 and t1 using add
+    add t2, t0, t1       # t2 = t0 + t1 (t2 = 5 + 10 = 15)
+    sub t0, t2, t0       # t0 = t2 - t0 (t0 = 15 - 5 = 10)
+    sub t1, t2, t1       # t1 = t2 - t1 (t1 = 15 - 10 = 5)
+
+    # Custom exit syscall
+    li a0, 0
+    li a1, 0
+    li a2, 0
+    li a3, 0
+    li a4, 0
+    li a5, 0
+    li a6, 0
+    li a7, 42
+    ecall

o1vm/resources/programs/riscv32im/src/addi.S

@@ -0,0 +1,20 @@
+.section .text
+.globl _start
+
+_start:
+  # Initialize register
+  li t0, 10         # Load immediate value 10 into t0
+
+  # Perform addition
+  addi t0, t0, 5    # Add 5 to the value in t0 and store the result back in t0
+
+  # Custom exit syscall
+  li a0, 0          # Set a0 to 0
+  li a1, 0          # Set a1 to 0
+  li a2, 0          # Set a2 to 0
+  li a3, 0          # Set a3 to 0
+  li a4, 0          # Set a4 to 0
+  li a5, 0          # Set a5 to 0
+  li a6, 0          # Set a6 to 0
+  li a7, 42         # Set a7 to 42 (custom ecall number)
+  ecall

o1vm/resources/programs/riscv32im/src/addi_boundary_immediate.S

@@ -0,0 +1,20 @@
+.section .text
+.globl _start
+
+_start:
+    li t0, 100            # t0 = 100
+    addi t1, t0, 2047     # t1 = t0 + 2047 (Expected: t1 = 2147)
+
+    li t2, 1000           # t2 = 1000
+    addi t3, t2, -2048    # t3 = t2 + (-2048) (Expected: t1 = -1048)
+
+    # Custom exit syscall
+    li a0, 0
+    li a1, 0
+    li a2, 0
+    li a3, 0
+    li a4, 0
+    li a5, 0
+    li a6, 0
+    li a7, 42
+    ecall