diff --git a/.github/workflows/mips-build.yml b/.github/workflows/mips-build.yml new file mode 100644 index 0000000000..264a485ee4 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index 67a6dff458..4cdc7c90ff 100644 --- a/.gitignore +++ b/.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 \ No newline at end of file +_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 diff --git a/Makefile b/Makefile index c86e935ea1..43f57c5021 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index 68f0191f5f..8f6b42bb21 100644 --- a/README.md +++ b/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) diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index be318bb0a6..5c70bf9b8c 100644 --- a/book/src/SUMMARY.md +++ b/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) diff --git a/book/src/pickles/diagrams.md b/book/src/pickles/diagrams.md index 63783603a6..a2728c7c10 100644 --- a/book/src/pickles/diagrams.md +++ b/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) diff --git a/book/src/pickles/overview.md b/book/src/pickles/overview.md index 7d2d8bdb7a..7ec7f1b98a 100644 --- a/book/src/pickles/overview.md +++ b/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. diff --git a/book/src/plonk/zkpm.md b/book/src/plonk/zkpm.md index 4820a55095..e35dcff645 100644 --- a/book/src/plonk/zkpm.md +++ b/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)] \\ diff --git a/book/src/snarky/kimchi-backend.md b/book/src/snarky/kimchi-backend.md index 7ab2e38bb6..5035dc8dec 100644 --- a/book/src/snarky/kimchi-backend.md +++ b/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 diff --git a/book/src/snarky/snarky-wrapper.md b/book/src/snarky/snarky-wrapper.md index 9f652da76b..4a52fbaeb2 100644 --- a/book/src/snarky/snarky-wrapper.md +++ b/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. ``` diff --git a/book/src/snarky/vars.md b/book/src/snarky/vars.md index 41fabe82fd..69dced8d78 100644 --- a/book/src/snarky/vars.md +++ b/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: diff --git a/o1vm/README-optimism.md b/o1vm/README-optimism.md index 740d495a34..4ce5014df5 100644 --- a/o1vm/README-optimism.md +++ b/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 ``` diff --git a/o1vm/README.md b/o1vm/README.md index d8dbd5d3d0..9e728c4ad9 100644 --- a/o1vm/README.md +++ b/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 diff --git a/o1vm/resources/programs/riscv32im/bin/add_1 b/o1vm/resources/programs/riscv32im/bin/add_1 new file mode 100755 index 0000000000..6fc6fe9837 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/add_1 differ diff --git a/o1vm/resources/programs/riscv32im/bin/add_2 b/o1vm/resources/programs/riscv32im/bin/add_2 new file mode 100755 index 0000000000..6a35810533 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/add_2 differ diff --git a/o1vm/resources/programs/riscv32im/bin/add_overflow b/o1vm/resources/programs/riscv32im/bin/add_overflow new file mode 100755 index 0000000000..0af6dd1bcc Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/add_overflow differ diff --git a/o1vm/resources/programs/riscv32im/bin/add_sub_swap b/o1vm/resources/programs/riscv32im/bin/add_sub_swap new file mode 100755 index 0000000000..292b82f40d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/add_sub_swap differ diff --git a/o1vm/resources/programs/riscv32im/bin/addi b/o1vm/resources/programs/riscv32im/bin/addi new file mode 100755 index 0000000000..4ad4f72bab Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/addi differ diff --git a/o1vm/resources/programs/riscv32im/bin/addi_boundary_immediate b/o1vm/resources/programs/riscv32im/bin/addi_boundary_immediate new file mode 100755 index 0000000000..65f5381c3c Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/addi_boundary_immediate differ diff --git a/o1vm/resources/programs/riscv32im/bin/addi_negative b/o1vm/resources/programs/riscv32im/bin/addi_negative new file mode 100755 index 0000000000..5d3eca47c2 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/addi_negative differ diff --git a/o1vm/resources/programs/riscv32im/bin/addi_overflow b/o1vm/resources/programs/riscv32im/bin/addi_overflow new file mode 100755 index 0000000000..d6df4b003c Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/addi_overflow differ diff --git a/o1vm/resources/programs/riscv32im/bin/and b/o1vm/resources/programs/riscv32im/bin/and new file mode 100755 index 0000000000..4b645914a8 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/and differ diff --git a/o1vm/resources/programs/riscv32im/bin/div_by_zero b/o1vm/resources/programs/riscv32im/bin/div_by_zero new file mode 100755 index 0000000000..57cd40f70d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/div_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/divu_by_zero b/o1vm/resources/programs/riscv32im/bin/divu_by_zero new file mode 100755 index 0000000000..494eedac4b Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/divu_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/jal b/o1vm/resources/programs/riscv32im/bin/jal new file mode 100755 index 0000000000..4b662e82bf Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/jal differ diff --git a/o1vm/resources/programs/riscv32im/bin/mul_overflow b/o1vm/resources/programs/riscv32im/bin/mul_overflow new file mode 100755 index 0000000000..3dd27cf465 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/mul_overflow differ diff --git a/o1vm/resources/programs/riscv32im/bin/rem_by_zero b/o1vm/resources/programs/riscv32im/bin/rem_by_zero new file mode 100755 index 0000000000..293f8dd5a2 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/rem_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/remu_by_zero b/o1vm/resources/programs/riscv32im/bin/remu_by_zero new file mode 100755 index 0000000000..b6dc591d1d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/remu_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/sll b/o1vm/resources/programs/riscv32im/bin/sll index f5a7fc75b1..14d0b82f86 100755 Binary files a/o1vm/resources/programs/riscv32im/bin/sll and b/o1vm/resources/programs/riscv32im/bin/sll differ diff --git a/o1vm/resources/programs/riscv32im/bin/slt b/o1vm/resources/programs/riscv32im/bin/slt new file mode 100755 index 0000000000..4f8906dd86 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/slt differ diff --git a/o1vm/resources/programs/riscv32im/bin/sub b/o1vm/resources/programs/riscv32im/bin/sub new file mode 100755 index 0000000000..49411f110d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/sub differ diff --git a/o1vm/resources/programs/riscv32im/bin/sub_2 b/o1vm/resources/programs/riscv32im/bin/sub_2 new file mode 100755 index 0000000000..964e9c737a Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/sub_2 differ diff --git a/o1vm/resources/programs/riscv32im/bin/sub_3 b/o1vm/resources/programs/riscv32im/bin/sub_3 new file mode 100755 index 0000000000..2bd2bff544 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/sub_3 differ diff --git a/o1vm/resources/programs/riscv32im/bin/xor b/o1vm/resources/programs/riscv32im/bin/xor new file mode 100755 index 0000000000..2a9f659899 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/xor differ diff --git a/o1vm/resources/programs/riscv32im/src/add_1.S b/o1vm/resources/programs/riscv32im/src/add_1.S new file mode 100644 index 0000000000..845a3172c1 --- /dev/null +++ b/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 diff --git a/o1vm/resources/programs/riscv32im/src/add_2.S b/o1vm/resources/programs/riscv32im/src/add_2.S new file mode 100644 index 0000000000..83f4063ef1 --- /dev/null +++ b/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 diff --git a/o1vm/resources/programs/riscv32im/src/add_overflow.S b/o1vm/resources/programs/riscv32im/src/add_overflow.S new file mode 100644 index 0000000000..1d3616f36b --- /dev/null +++ b/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 diff --git a/o1vm/resources/programs/riscv32im/src/add_sub_swap.S b/o1vm/resources/programs/riscv32im/src/add_sub_swap.S new file mode 100644 index 0000000000..e09bf67b34 --- /dev/null +++ b/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 diff --git a/o1vm/resources/programs/riscv32im/src/addi.S b/o1vm/resources/programs/riscv32im/src/addi.S new file mode 100644 index 0000000000..f4e50282bf --- /dev/null +++ b/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 diff --git a/o1vm/resources/programs/riscv32im/src/addi_boundary_immediate.S b/o1vm/resources/programs/riscv32im/src/addi_boundary_immediate.S new file mode 100644 index 0000000000..241af6ea48 --- /dev/null +++ b/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 diff --git a/o1vm/resources/programs/riscv32im/src/addi_negative.S b/o1vm/resources/programs/riscv32im/src/addi_negative.S new file mode 100644 index 0000000000..1b94dfb420 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/addi_negative.S @@ -0,0 +1,25 @@ +.section .text +.globl _start + +_start: + li t0, 100 # t0 = 100 + + # Subtract 50 using addi (addi with negative immediate) + addi t1, t0, -50 # t1 = t0 + (-50) (Expected: t1 = 50) + + # Subtract 100 using addi (addi with negative immediate) + addi t2, t1, -100 # t2 = t1 + (-100) (Expected: t2 = -50) + + li t3, -1000 # t3 = -1000 + addi t4, t3, -500 # t4 = t0 + (-500) (Expected: t4 = -1500) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/addi_overflow.S b/o1vm/resources/programs/riscv32im/src/addi_overflow.S new file mode 100644 index 0000000000..c1539b05a4 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/addi_overflow.S @@ -0,0 +1,23 @@ +.section .text +.globl _start + +_start: + li t0, 2147483647 # t0 = 2147483647 (Max 32-bit signed int) + addi t1, t0, 1 # t1 = t0 + 1 (Expected: overflow to -2147483648) + + li t2, -2147483648 # t2 = -2147483648 (Min 32-bit signed int) + addi t3, t2, -1 # t3 = t2 + (-1) (Expected: overflow to 2147483647) + + li t4, 123456789 # t4 = 123456789 + addi t5, t4, 0 # t5 = t4 + 0 (Expected: t4 = 123456789) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/and.S b/o1vm/resources/programs/riscv32im/src/and.S new file mode 100644 index 0000000000..4bab937b9b --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/and.S @@ -0,0 +1,30 @@ +.section .text +.globl _start + +_start: + + # Simple AND + li t0, 0b1100 # t0 = 0b1100 + li t1, 0b1010 # t1 = 0b1010 + and t2, t0, t1 # t2 = t0 & t1 (Expected: t2 = 0b1000) + + # AND with zero (result always zero) + li t3, 0b1111 # t3 = 0b1111 + li t4, 0 # t4 = 0 + and t5, t3, t4 # t5 = t3 & t4 (Expected: t5 = 0) + + # AND of identical values (result same value) + li t6, 0b1010 # t6 = 0b1010 + li t0, 0b1010 # t0 = 0b1010 + and t1, t6, t0 # t1 = t6 & t0 (Expected: t1 = 0b1010) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/div_by_zero.S b/o1vm/resources/programs/riscv32im/src/div_by_zero.S new file mode 100644 index 0000000000..5f8c490924 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/div_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Signed division by zero (div) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + div t2, t0, t1 # t2 = t0 / t1 (Expected: division by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/divu_by_zero.S b/o1vm/resources/programs/riscv32im/src/divu_by_zero.S new file mode 100644 index 0000000000..b44ff50479 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/divu_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Unsigned division by zero (div) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + divu t2, t0, t1 # t2 = t0 / t1 (Expected: division by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/jal.S b/o1vm/resources/programs/riscv32im/src/jal.S new file mode 100644 index 0000000000..191cdfbb3e --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/jal.S @@ -0,0 +1,25 @@ +.section .text +.global _start + +# t0 <- t0 + t1 +add_t0_t1: + add t0, t0, t1 + ret + +_start: + li t0, 5 + li t1, 7 + # Could be jalr + # jal without offset + jal ra, add_t0_t1 + + # exit + 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 diff --git a/o1vm/resources/programs/riscv32im/src/mul_overflow.S b/o1vm/resources/programs/riscv32im/src/mul_overflow.S new file mode 100644 index 0000000000..c7cced4253 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/mul_overflow.S @@ -0,0 +1,18 @@ +.section .text +.globl _start + +_start: + li t0, 10000000 # Large number + li t1, 10000000 # Another large number + mul t2, t0, t1 # Test large multiplication (Expected overflow) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/rem_by_zero.S b/o1vm/resources/programs/riscv32im/src/rem_by_zero.S new file mode 100644 index 0000000000..bc9c4fb2eb --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/rem_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Signed remainder by zero (rem) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + rem t2, t0, t1 # t2 = t0 % t1 (Expected: remainder by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/remu_by_zero.S b/o1vm/resources/programs/riscv32im/src/remu_by_zero.S new file mode 100644 index 0000000000..fe11257f26 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/remu_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Unsigned remainder by zero (remu) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + remu t2, t0, t1 # t2 = t0 % t1 (Expected: remainder by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/sll.S b/o1vm/resources/programs/riscv32im/src/sll.S index 0f8cedd065..e343543e81 100644 --- a/o1vm/resources/programs/riscv32im/src/sll.S +++ b/o1vm/resources/programs/riscv32im/src/sll.S @@ -1,6 +1,10 @@ .global _start -exit_success: +_start: + # Load 2^12 in the register t0 + lui t0, 0b1 + # Multiply by 4 + sll t0, t0, 2 li a0, 0 li a1, 0 li a2, 0 @@ -10,8 +14,3 @@ exit_success: li a6, 0 li a7, 42 ecall - -_start: - lui t0, 0x42 - sll t0, t0, 2 - jal exit_success diff --git a/o1vm/resources/programs/riscv32im/src/slt.S b/o1vm/resources/programs/riscv32im/src/slt.S new file mode 100644 index 0000000000..42ff3e513e --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/slt.S @@ -0,0 +1,30 @@ +.section .text +.globl _start + +_start: + + # SLT with t0 < t1 (Expected: 1) + li t0, 100 # t0 = 100 + li t1, 200 # t1 = 200 + slt t2, t0, t1 # t2 = (t0 < t1) ? 1 : 0 (Expected: t2 = 1) + + # SLT with t3 > t4 (Expected: 0) + li t3, 300 # t3 = 300 + li t4, 200 # t4 = 200 + slt t5, t3, t4 # t5 = (t3 < t4) ? 1 : 0 (Expected: t5 = 0) + + # SLT with t0 == t1 (Expected: 0) + li t0, 150 # t6 = 150 + li t1, 150 # t7 = 150 + slt t6, t0, t1 # t6 = (t0 < t1) ? 1 : 0 (Expected: t6 = 0) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/sub.S b/o1vm/resources/programs/riscv32im/src/sub.S new file mode 100644 index 0000000000..53abe9bd17 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/sub.S @@ -0,0 +1,25 @@ +.section .text +.globl _start + +_start: + + # Test 1: Simple subtraction + li t0, 1000 # t0 = 1000 + li t1, 500 # t1 = 500 + sub t2, t0, t1 # t2 = t0 - t1 (Expected: t2 = 500) + + # Test 2: Subtracting from zero + li t3, 0 # t3 = 0 + li t4, 100 # t4 = 100 + sub t5, t3, t4 # t5 = t3 - t4 (Expected: t5 = -100) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/sub_2.S b/o1vm/resources/programs/riscv32im/src/sub_2.S new file mode 100644 index 0000000000..8ccadb14ba --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/sub_2.S @@ -0,0 +1,25 @@ +.section .text +.globl _start + +_start: + + # Test 3: Subtracting a larger value (result negative) + li t0, 300 # t0 = 300 + li t1, 500 # t1 = 500 + sub t2, t0, t1 # t2 = t0 - t1 (Expected: t2 = -200) + + # Test 4: Subtracting negative values (result positive) + li t3, 100 # t3 = 100 + li t4, -50 # t4 = -50 + sub t5, t3, t4 # t5 = t3 - t4 (Expected: t5 = 150) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/sub_3.S b/o1vm/resources/programs/riscv32im/src/sub_3.S new file mode 100644 index 0000000000..78e90cc011 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/sub_3.S @@ -0,0 +1,22 @@ +.section .text +.globl _start + +_start: + # Test 5: Result of subtracting from a register (using same value) + li t0, 1234 # t0 = 1234 + sub t1, t0, t0 # t1 = t0 - t0 (Expected: t1 = 0) + + # Test 6: Handling overflow (large subtraction result) + li t2, 2147483647 # t2 = 2147483647 (max positive signed 32-bit) + li t3, -1 # t3 = -1 + sub t4, t2, t3 # t4 = t2 - t3 (Expected: t0 = 2147483648, wraparound to -2147483648) + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/xor.S b/o1vm/resources/programs/riscv32im/src/xor.S new file mode 100644 index 0000000000..ea78a68cca --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/xor.S @@ -0,0 +1,30 @@ +.section .text +.globl _start + +_start: + + # Simple XOR + li t0, 0b1100 # t0 = 0b1100 + li t1, 0b1010 # t1 = 0b1010 + xor t2, t0, t1 # t2 = t0 ^ t1 (Expected: t2 = 0b0110) + + # XOR with zero (no change) + li t3, 0b1010 # t3 = 0b1010 + li t4, 0 # t4 = 0 + xor t5, t3, t4 # t5 = t3 ^ t4 (Expected: t5 = 0b1010) + + # XOR of identical values (result 0) + li t6, 0b1111 # t6 = 0b1111 + li t0, 0b1111 # t0 = 0b1111 + xor t1, t6, t0 # t1 = t6 ^ t0 (Expected: t1 = 0) + + # 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 diff --git a/o1vm/src/cannon.rs b/o1vm/src/cannon.rs index e9ae23d699..a87e5e92a4 100644 --- a/o1vm/src/cannon.rs +++ b/o1vm/src/cannon.rs @@ -209,7 +209,7 @@ pub struct HostProgram { pub struct VmConfiguration { pub input_state_file: String, pub output_state_file: String, - pub metadata_file: String, + pub metadata_file: Option, pub proof_at: StepFrequency, pub stop_at: StepFrequency, pub snapshot_state_at: StepFrequency, diff --git a/o1vm/src/cli/cannon.rs b/o1vm/src/cli/cannon.rs index 879036e083..9445be62d0 100644 --- a/o1vm/src/cli/cannon.rs +++ b/o1vm/src/cli/cannon.rs @@ -19,13 +19,8 @@ pub struct MipsVmConfigurationArgs { )] output: String, - #[arg( - long, - value_name = "FILE", - default_value = "meta.json", - help = "metadata file" - )] - meta: String, + #[arg(long, value_name = "FILE", help = "metadata file")] + meta: Option, #[arg( long = "proof-at", @@ -104,9 +99,25 @@ pub struct RunArgs { pub vm_cfg: MipsVmConfigurationArgs, } +#[derive(Parser, Debug, Clone)] +pub struct GenStateJsonArgs { + #[arg(short = 'i', long, value_name = "FILE", help = "input ELF file")] + pub input: String, + #[arg( + short = 'o', + long, + value_name = "FILE", + default_value = "state.json", + help = "output state.json file" + )] + pub output: String, +} + #[derive(Subcommand, Clone, Debug)] pub enum Cannon { Run(RunArgs), #[command(name = "test-optimism-preimage-read")] TestPreimageRead(RunArgs), + #[command(name = "gen-state-json")] + GenStateJson(GenStateJsonArgs), } diff --git a/o1vm/src/elf_loader.rs b/o1vm/src/elf_loader.rs index ecdaf895fe..b2e0e1009f 100644 --- a/o1vm/src/elf_loader.rs +++ b/o1vm/src/elf_loader.rs @@ -1,24 +1,19 @@ use crate::cannon::{Page, State, PAGE_SIZE}; -use elf::{endian::LittleEndian, section::SectionHeader, ElfBytes}; +use elf::{ + endian::{BigEndian, EndianParse, LittleEndian}, + section::SectionHeader, + ElfBytes, +}; use log::debug; use std::{collections::HashMap, path::Path}; -/// Parse an ELF file and return the parsed data as a structure that is expected -/// by the o1vm RISC-V 32 bits edition. -// FIXME: parametrize by an architecture. We should return a state depending on the -// architecture. In the meantime, we can have parse_riscv32i and parse_mips. -// FIXME: for now, we return a State structure, either for RISC-V 32i or MIPS. -// We should return a structure specifically built for the o1vm, and not tight -// to Cannon. It will be done in a future PR to avoid breaking the current code -// and have a huge diff. -pub fn parse_riscv32(path: &Path) -> Result { - debug!("Start parsing the ELF file to load a RISC-V 32i compatible state"); - let file_data = std::fs::read(path).expect("Could not read file."); - let slice = file_data.as_slice(); - let file = ElfBytes::::minimal_parse(slice).expect("Open ELF file failed."); +pub enum Architecture { + Mips, + RiscV32, +} +pub fn make_state(file: ElfBytes) -> Result { // Checking it is RISC-V - assert_eq!(file.ehdr.e_machine, 243); let (shdrs_opt, strtab_opt) = file .section_headers_with_strtab() @@ -51,9 +46,11 @@ pub fn parse_riscv32(path: &Path) -> Result { .section_data(text_section) .expect("Failed to read data from .text section"); + // address of starting instruction in code section let code_section_starting_address = text_section.sh_addr as usize; let code_section_size = text_section.sh_size as usize; - let code_section_end_address = code_section_starting_address + code_section_size; + // address of last instruction in code section + let code_section_end_address = code_section_starting_address + code_section_size - 1; debug!( "The executable code starts at address {}, has size {} bytes, and ends at address {}.", code_section_starting_address, code_section_size, code_section_end_address @@ -64,17 +61,22 @@ pub fn parse_riscv32(path: &Path) -> Result { let page_size_usize: usize = PAGE_SIZE.try_into().unwrap(); // Padding to get the right number of pages. We suppose that the memory // index starts at 0. + + // the address that the first page starts on let start_page_address: usize = (code_section_starting_address / page_size_usize) * page_size_usize; - let end_page_address = - (code_section_end_address / (page_size_usize - 1)) * page_size_usize + page_size_usize; + + // the address that the last page starts on + let end_page_address = (code_section_end_address / page_size_usize) * page_size_usize; let first_page_index = start_page_address / page_size_usize; - let last_page_index = (end_page_address - 1) / page_size_usize; + + let last_page_index = end_page_address / page_size_usize; + let mut data_offset = 0; (first_page_index..=last_page_index).for_each(|page_index| { let mut data = vec![0; page_size_usize]; - // Special case of only one page + // Special case where all code fits in one page if first_page_index == last_page_index { let data_length = code_section_end_address - code_section_starting_address; let page_offset = code_section_starting_address - start_page_address; @@ -83,7 +85,7 @@ pub fn parse_riscv32(path: &Path) -> Result { data_offset += data_length; } else { let data_length = if page_index == last_page_index { - code_section_end_address - (page_index * page_size_usize) + code_section_end_address - end_page_address } else { page_size_usize }; @@ -92,8 +94,9 @@ pub fn parse_riscv32(path: &Path) -> Result { } else { 0 }; - data[page_offset..] + data[page_offset..page_offset + data_length] .copy_from_slice(&text_section_data[data_offset..data_offset + data_length]); + data_offset += data_length; } let page = Page { @@ -143,3 +146,22 @@ pub fn parse_riscv32(path: &Path) -> Result { Ok(state) } + +pub fn parse_elf(arch: Architecture, path: &Path) -> Result { + debug!("Start parsing the ELF file to load a compatible state"); + let file_data = std::fs::read(path).expect("Could not read file."); + let slice = file_data.as_slice(); + match arch { + Architecture::Mips => { + let file = ElfBytes::::minimal_parse(slice).expect("Open ELF file failed."); + assert_eq!(file.ehdr.e_machine, 8); + make_state(file) + } + Architecture::RiscV32 => { + let file = + ElfBytes::::minimal_parse(slice).expect("Open ELF file failed."); + assert_eq!(file.ehdr.e_machine, 243); + make_state(file) + } + } +} diff --git a/o1vm/src/interpreters/mips/interpreter.rs b/o1vm/src/interpreters/mips/interpreter.rs index 0ea55c67ea..5ba96d9885 100644 --- a/o1vm/src/interpreters/mips/interpreter.rs +++ b/o1vm/src/interpreters/mips/interpreter.rs @@ -934,7 +934,13 @@ pub trait InterpreterEnv { let pos = self.alloc_scratch(); unsafe { self.bitmask(x, bitlength, bitlength - 1, pos) } }; - high_bit * Self::constant(((1 << (32 - bitlength)) - 1) << bitlength) + x.clone() + // Casting in u64 for special case of bitlength = 0 to avoid overflow. + // No condition for constant time execution. + // Decomposing the steps for readability. + let v: u64 = (1u64 << (32 - bitlength)) - 1; + let v: u64 = v << bitlength; + let v: u32 = v as u32; + high_bit * Self::constant(v) + x.clone() } fn report_exit(&mut self, exit_code: &Self::Variable); diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index 991b946c8d..b5fa8161a0 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -1143,7 +1143,7 @@ impl Env { pub fn step( &mut self, config: &VmConfiguration, - metadata: &Meta, + metadata: &Option, start: &Start, ) -> Instruction { self.reset_scratch_state(); @@ -1267,7 +1267,7 @@ impl Env { } } - fn pp_info(&mut self, at: &StepFrequency, meta: &Meta, start: &Start) { + fn pp_info(&mut self, at: &StepFrequency, meta: &Option, start: &Start) { if self.should_trigger_at(at) { let elapsed = start.time.elapsed(); // Compute the step number removing the MAX_ACC factor @@ -1286,8 +1286,9 @@ impl Env { let mem = self.memory_usage(); let name = meta - .find_address_symbol(pc) - .unwrap_or_else(|| "n/a".to_string()); + .as_ref() + .and_then(|m| m.find_address_symbol(pc)) + .unwrap_or("n/a".to_string()); info!( "processing step={} pc={:010x} insn={:010x} ips={:.2} pages={} mem={} name={}", diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index ba1633e1a7..e45099490e 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -77,8 +77,8 @@ impl InterpreterEnv for Env { // No-op, witness only } - fn check_boolean(_x: &Self::Variable) { - // No-op, witness only + fn assert_boolean(&mut self, x: &Self::Variable) { + self.add_constraint(x.clone() * x.clone() - x.clone()); } fn add_lookup(&mut self, lookup: Lookup) { diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index f27d89ec4e..91f100e911 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -598,14 +598,8 @@ pub trait InterpreterEnv { self.add_constraint(x - y); } - /// Check that the witness value `x` is a boolean (`0` or `1`); otherwise abort. - fn check_boolean(x: &Self::Variable); - /// Assert that the value `x` is boolean, and add a constraint in the proof system. - fn assert_boolean(&mut self, x: Self::Variable) { - Self::check_boolean(&x); - self.add_constraint(x.clone() * x.clone() - x); - } + fn assert_boolean(&mut self, x: &Self::Variable); fn add_lookup(&mut self, lookup: Lookup); @@ -1286,6 +1280,10 @@ pub trait InterpreterEnv { /// There are no constraints on the returned values; callers must manually add constraints to /// ensure that the pair of returned values correspond to the given values `x` and `y`, and /// that they fall within the desired range. + /// + /// Division by zero will create a panic! exception. The RISC-V + /// specification leaves the case unspecified, and therefore we prefer to + /// forbid this case while building the witness. unsafe fn div_signed( &mut self, x: &Self::Variable, @@ -1314,6 +1312,10 @@ pub trait InterpreterEnv { /// There are no constraints on the returned values; callers must manually add constraints to /// ensure that the pair of returned values correspond to the given values `x` and `y`, and /// that they fall within the desired range. + /// + /// Division by zero will create a panic! exception. The RISC-V + /// specification leaves the case unspecified, and therefore we prefer to + /// forbid this case while building the witness. unsafe fn div( &mut self, x: &Self::Variable, @@ -1388,12 +1390,19 @@ pub trait InterpreterEnv { /// Given a variable `x`, this function extends it to a signed integer of /// `bitlength` bits. fn sign_extend(&mut self, x: &Self::Variable, bitlength: u32) -> Self::Variable { + assert!(bitlength <= 32); // FIXME: Constrain `high_bit` let high_bit = { let pos = self.alloc_scratch(); unsafe { self.bitmask(x, bitlength, bitlength - 1, pos) } }; - high_bit * Self::constant(((1 << (32 - bitlength)) - 1) << bitlength) + x.clone() + // Casting in u64 for special case of bitlength = 0 to avoid overflow. + // No condition for constant time execution. + // Decomposing the steps for readability. + let v: u64 = (1u64 << (32 - bitlength)) - 1; + let v: u64 = v << bitlength; + let v: u32 = v as u32; + high_bit * Self::constant(v) + x.clone() } fn report_exit(&mut self, exit_code: &Self::Variable); @@ -1498,11 +1507,12 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) // add: x[rd] = x[rs1] + x[rs2] let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let overflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _overflow) = - env.add_witness(&local_rs1, &local_rs2, rd_scratch, overflow_scratch); + let local_rd = { + let overflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_rs2, rd_scratch, overflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1514,11 +1524,12 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sub: x[rd] = x[rs1] - x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let underflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _underflow) = - env.sub_witness(&local_rs1, &local_rs2, rd_scratch, underflow_scratch); + let local_rd = { + let underflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _underflow) = unsafe { + env.sub_witness(&local_rs1, &local_rs2, rd_scratch, underflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1530,9 +1541,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sll: x[rd] = x[rs1] << x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let rd_scratch = env.alloc_scratch(); - env.shift_left(&local_rs1, &local_rs2, rd_scratch) + unsafe { env.shift_left(&local_rs1, &local_rs2, rd_scratch) } }; env.write_register(&rd, local_rd); @@ -1543,9 +1554,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* slt: x[rd] = (x[rs1] < x[rs2]) ? 1 : 0 */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let rd_scratch = env.alloc_scratch(); - env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) + unsafe { env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) } }; env.write_register(&rd, local_rd); @@ -1556,9 +1567,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sltu: x[rd] = (x[rs1] < (u)x[rs2]) ? 1 : 0 */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.test_less_than(&local_rs1, &local_rs2, pos) + unsafe { env.test_less_than(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1569,9 +1580,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* xor: x[rd] = x[rs1] ^ x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.xor_witness(&local_rs1, &local_rs2, pos) + unsafe { env.xor_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1582,9 +1593,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* srl: x[rd] = x[rs1] >> x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.shift_right(&local_rs1, &local_rs2, pos) + unsafe { env.shift_right(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1595,9 +1606,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sra: x[rd] = x[rs1] >> x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.shift_right_arithmetic(&local_rs1, &local_rs2, pos) + unsafe { env.shift_right_arithmetic(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1608,9 +1619,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* or: x[rd] = x[rs1] | x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.or_witness(&local_rs1, &local_rs2, pos) + unsafe { env.or_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1621,9 +1632,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* and: x[rd] = x[rs1] & x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.and_witness(&local_rs1, &local_rs2, pos) + unsafe { env.and_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1886,11 +1897,12 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // addi: x[rd] = x[rs1] + sext(immediate) let local_rs1 = env.read_register(&(rs1.clone())); let local_imm = env.sign_extend(&imm, 12); - let overflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _overflow) = - env.add_witness(&local_rs1, &local_imm, rd_scratch, overflow_scratch); + let local_rd = { + let overflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_imm, rd_scratch, overflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1901,8 +1913,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // xori: x[rd] = x[rs1] ^ sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.xor_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.xor_witness(&local_rs1, &local_imm, rd_scratch) } + }; env.write_register(&rd, local_rd); env.set_instruction_pointer(next_instruction_pointer.clone()); env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); @@ -1911,8 +1925,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // ori: x[rd] = x[rs1] | sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.or_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.or_witness(&local_rs1, &local_imm, rd_scratch) } + }; env.write_register(&rd, local_rd); env.set_instruction_pointer(next_instruction_pointer.clone()); env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); @@ -1921,8 +1937,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // andi: x[rd] = x[rs1] & sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.and_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.and_witness(&local_rs1, &local_imm, rd_scratch) } + }; env.write_register(&rd, local_rd); env.set_instruction_pointer(next_instruction_pointer.clone()); env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); @@ -2132,8 +2150,7 @@ pub fn interpret_stype(env: &mut Env, instr: SInstruction) /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction) { let instruction_pointer = env.get_instruction_pointer(); - let _next_instruction_pointer = env.get_next_instruction_pointer(); - + let next_instruction_pointer = env.get_next_instruction_pointer(); let instruction = { let v0 = env.read_memory(&instruction_pointer); let v1 = env.read_memory(&(instruction_pointer.clone() + Env::constant(1))); @@ -2144,19 +2161,12 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction + (v1 * Env::constant(1 << 8)) + v0 }; - let opcode = { let pos = env.alloc_scratch(); unsafe { env.bitmask(&instruction, 7, 0, pos) } }; - env.range_check8(&opcode, 7); - // FIXME: trickier - let imm1 = { - let pos = env.alloc_scratch(); - unsafe { env.bitmask(&instruction, 12, 7, pos) } - }; - env.range_check8(&imm1, 5); + env.range_check8(&opcode, 7); let funct3 = { let pos = env.alloc_scratch(); @@ -2176,33 +2186,210 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction }; env.range_check8(&rs2, 5); - // FIXME: trickier - let imm2 = { - let pos = env.alloc_scratch(); - unsafe { env.bitmask(&instruction, 32, 25, pos) } - }; - env.range_check16(&imm2, 12); + let imm0_12 = { + let imm11 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 8, 7, pos) } + }; - // FIXME: check correctness of decomposition + env.assert_boolean(&imm11); + + let imm1_4 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 12, 8, pos) } + }; + env.range_check8(&imm1_4, 4); + + let imm5_10 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 31, 25, pos) } + }; + env.range_check8(&imm5_10, 6); + + let imm12 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 32, 31, pos) } + }; + env.assert_boolean(&imm12); + + // check correctness of decomposition of SB type function + env.add_constraint( + instruction.clone() + - (opcode * Env::constant(1 << 0)) // opcode at bits 0-7 + - (imm11.clone() * Env::constant(1 << 7)) // imm11 at bits 8 + - (imm1_4.clone() * Env::constant(1 << 8)) // imm1_4 at bits 9-11 + - (funct3 * Env::constant(1 << 11)) // funct3 at bits 11-14 + - (rs1.clone() * Env::constant(1 << 14)) // rs1 at bits 15-20 + - (rs2.clone() * Env::constant(1 << 19)) // rs2 at bits 20-24 + - (imm5_10.clone() * Env::constant(1 << 24)) // imm5_10 at bits 25-30 + - (imm12.clone() * Env::constant(1 << 31)), // imm12 at bits 31 + ); + + (imm12 * Env::constant(1 << 12)) + + (imm11 * Env::constant(1 << 11)) + + (imm5_10 * Env::constant(1 << 5)) + + (imm1_4 * Env::constant(1 << 1)) + }; + // extra bit is because the 0th bit in the immediate is always 0 i.e you cannot jump to an odd address + let imm0_12 = env.sign_extend(&imm0_12, 13); match instr { SBInstruction::BranchEq => { - unimplemented!("BranchEq") + // beq: if (x[rs1] == x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let equals = env.equal(&local_rs1, &local_rs2); + let offset = (Env::constant(1) - equals.clone()) * Env::constant(4) + equals * imm0_12; + let offset = env.sign_extend(&offset, 12); + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchNeq => { - unimplemented!("BranchNeq") + // bne: if (x[rs1] != x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let equals = env.equal(&local_rs1, &local_rs2); + let offset = equals.clone() * Env::constant(4) + (Env::constant(1) - equals) * imm0_12; + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchLessThan => { - unimplemented!("BranchLessThan") + // blt: if (x[rs1] < x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let less_than = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) } + }; + let offset = (less_than.clone()) * imm0_12 + + (Env::constant(1) - less_than.clone()) * Env::constant(4); + + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchGreaterThanEqual => { - unimplemented!("BranchGreaterThanEqual") + // bge: if (x[rs1] >= x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let less_than = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) } + }; + + let offset = + less_than.clone() * Env::constant(4) + (Env::constant(1) - less_than) * imm0_12; + // greater than equal is the negation of less than + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchLessThanUnsigned => { - unimplemented!("BranchLessThanUnsigned") + // bltu: if (x[rs1] { - unimplemented!("BranchGreaterThanEqualUnsigned") + // bgeu: if (x[rs1] >=u x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let rd_scratch = env.alloc_scratch(); + let less_than = unsafe { env.test_less_than(&local_rs1, &local_rs2, rd_scratch) }; + let offset = + less_than.clone() * Env::constant(4) + (Env::constant(1) - less_than) * imm0_12; + + // greater than equal is the negation of less than + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness(&instruction_pointer, &offset, res_scratch, overflow_scratch) + }; + res + }; + + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } }; } @@ -2260,8 +2447,10 @@ pub fn interpret_utype(env: &mut Env, instr: UInstruction) UInstruction::LoadUpperImmediate => { // lui: x[rd] = sext(immediate[31:12] << 12) let local_imm = { - let pos = env.alloc_scratch(); - let shifted_imm = unsafe { env.shift_left(&imm, &Env::constant(12), pos) }; + let shifted_imm = { + let pos = env.alloc_scratch(); + unsafe { env.shift_left(&imm, &Env::constant(12), pos) } + }; env.sign_extend(&shifted_imm, 32) }; env.write_register(&rd, local_imm); @@ -2293,14 +2482,30 @@ pub fn interpret_utype(env: &mut Env, instr: UInstruction) /// Interpret an UJ-type instruction. /// The encoding of an UJ-type instruction is as follows: /// ```text -/// | 31 12 | 11 7 | 6 0 | -/// | immediate | rd | opcode | +/// | 31 12 | 11 7 | 6 0 | +/// | imm[20|10:1|11|19:12] | rd | opcode | /// ``` /// Following the documentation found /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) +/// +/// The interpretation of the immediate is as follow: +/// ```text +/// imm_20 = instruction[31] +/// imm_10_1 = instruction[30..21] +/// imm_11 = instruction[20] +/// imm_19_12 = instruction[19..12] +/// +/// imm = imm_20 << 19 + +/// imm_19_12 << 11 + +/// imm_11 << 10 + +/// imm_10_1 +/// +/// # The immediate is then sign-extended. The sign-extension is in the bit imm20 +/// imm = imm << 1 +/// ``` pub fn interpret_ujtype(env: &mut Env, instr: UJInstruction) { let instruction_pointer = env.get_instruction_pointer(); - let _next_instruction_pointer = env.get_next_instruction_pointer(); + let next_instruction_pointer = env.get_next_instruction_pointer(); let instruction = { let v0 = env.read_memory(&instruction_pointer); @@ -2325,18 +2530,55 @@ pub fn interpret_ujtype(env: &mut Env, instr: UJInstruction }; env.range_check8(&rd, 5); - // FIXME: trickier - let _imm = { + let imm20 = { let pos = env.alloc_scratch(); - unsafe { env.bitmask(&instruction, 32, 12, pos) } + unsafe { env.bitmask(&instruction, 32, 31, pos) } + }; + env.assert_boolean(&imm20); + + let imm10_1 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 31, 21, pos) } + }; + env.range_check16(&imm10_1, 10); + + let imm11 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 21, 20, pos) } + }; + env.assert_boolean(&imm11); + + let imm19_12 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 20, 12, pos) } + }; + env.range_check8(&imm19_12, 8); + + let offset = { + imm10_1.clone() * Env::constant(1 << 1) + + imm11.clone() * Env::constant(1 << 11) + + imm19_12.clone() * Env::constant(1 << 12) + + imm20.clone() * Env::constant(1 << 20) }; // FIXME: check correctness of decomposition + match instr { UJInstruction::JumpAndLink => { - unimplemented!("JumpAndLink") + let offset = env.sign_extend(&offset, 21); + let new_addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness(&instruction_pointer, &offset, res_scratch, overflow_scratch) + }; + res + }; + env.write_register(&rd, next_instruction_pointer.clone()); + env.set_instruction_pointer(new_addr.clone()); + env.set_next_instruction_pointer(new_addr + Env::constant(4u32)); } - }; + } } pub fn interpret_syscall(env: &mut Env, _instr: SyscallInstruction) { diff --git a/o1vm/src/interpreters/riscv32im/mod.rs b/o1vm/src/interpreters/riscv32im/mod.rs index 59c855694b..ed6dd1b38a 100644 --- a/o1vm/src/interpreters/riscv32im/mod.rs +++ b/o1vm/src/interpreters/riscv32im/mod.rs @@ -1,7 +1,5 @@ /// The minimal number of columns required for the VM -// FIXME: the value will be updated when the interpreter is fully -// implemented. Using a small value for now. -pub const SCRATCH_SIZE: usize = 80; +pub const SCRATCH_SIZE: usize = 39; /// Number of instructions in the ISA pub const INSTRUCTION_SET_SIZE: usize = 48; diff --git a/o1vm/src/interpreters/riscv32im/registers.rs b/o1vm/src/interpreters/riscv32im/registers.rs index ca5906bd54..6a73eca625 100644 --- a/o1vm/src/interpreters/riscv32im/registers.rs +++ b/o1vm/src/interpreters/riscv32im/registers.rs @@ -64,3 +64,102 @@ impl IndexMut for Registers { } } } + +/// This enum provides aliases for the registers. +/// This is useful for debugging and for providing a more readable interface. +/// It can be used to index the registers in the witness. +pub enum RegisterAlias { + Zero, + /// Return address + Ra, + /// Stack pointer + Sp, + /// Global pointer + Gp, + /// Thread pointer + Tp, + /// Temporary/alternate register + T0, + /// Temporaries + T1, + T2, + /// Frame pointer/saved register. This is the same register. + Fp, + S0, + /// Saved registers + S1, + /// Function arguments/results + A0, + A1, + A2, + A3, + A4, + A5, + A6, + A7, + S2, + S3, + S4, + S5, + S6, + S7, + S8, + S9, + S10, + S11, + T3, + T4, + T5, + T6, + /// Current instruction pointer + Ip, + /// Next instruction pointer + NextIp, + HeapPointer, +} + +impl Index for Registers { + type Output = T; + + fn index(&self, index: RegisterAlias) -> &Self::Output { + match index { + RegisterAlias::Zero => &self.general_purpose[0], + RegisterAlias::Ra => &self.general_purpose[1], + RegisterAlias::Sp => &self.general_purpose[2], + RegisterAlias::Gp => &self.general_purpose[3], + RegisterAlias::Tp => &self.general_purpose[4], + RegisterAlias::T0 => &self.general_purpose[5], + RegisterAlias::T1 => &self.general_purpose[6], + RegisterAlias::T2 => &self.general_purpose[7], + // Frame pointer and first saved register are the same register. + RegisterAlias::Fp => &self.general_purpose[8], + RegisterAlias::S0 => &self.general_purpose[8], + RegisterAlias::S1 => &self.general_purpose[9], + RegisterAlias::A0 => &self.general_purpose[10], + RegisterAlias::A1 => &self.general_purpose[11], + RegisterAlias::A2 => &self.general_purpose[12], + RegisterAlias::A3 => &self.general_purpose[13], + RegisterAlias::A4 => &self.general_purpose[14], + RegisterAlias::A5 => &self.general_purpose[15], + RegisterAlias::A6 => &self.general_purpose[16], + RegisterAlias::A7 => &self.general_purpose[17], + RegisterAlias::S2 => &self.general_purpose[18], + RegisterAlias::S3 => &self.general_purpose[19], + RegisterAlias::S4 => &self.general_purpose[20], + RegisterAlias::S5 => &self.general_purpose[21], + RegisterAlias::S6 => &self.general_purpose[22], + RegisterAlias::S7 => &self.general_purpose[23], + RegisterAlias::S8 => &self.general_purpose[24], + RegisterAlias::S9 => &self.general_purpose[25], + RegisterAlias::S10 => &self.general_purpose[26], + RegisterAlias::S11 => &self.general_purpose[27], + RegisterAlias::T3 => &self.general_purpose[28], + RegisterAlias::T4 => &self.general_purpose[29], + RegisterAlias::T5 => &self.general_purpose[30], + RegisterAlias::T6 => &self.general_purpose[31], + RegisterAlias::Ip => &self.current_instruction_pointer, + RegisterAlias::NextIp => &self.next_instruction_pointer, + RegisterAlias::HeapPointer => &self.heap_pointer, + } + } +} diff --git a/o1vm/src/interpreters/riscv32im/tests.rs b/o1vm/src/interpreters/riscv32im/tests.rs index fcb923ed90..08c1634c5b 100644 --- a/o1vm/src/interpreters/riscv32im/tests.rs +++ b/o1vm/src/interpreters/riscv32im/tests.rs @@ -2,14 +2,14 @@ use super::{registers::Registers, witness::Env, INSTRUCTION_SET_SIZE, PAGE_SIZE, use crate::interpreters::riscv32im::{ constraints, interpreter::{ - IInstruction, Instruction, InterpreterEnv, MInstruction, RInstruction, SBInstruction, - SInstruction, SyscallInstruction, UInstruction, UJInstruction, + interpret_instruction, IInstruction, Instruction, InterpreterEnv, MInstruction, + RInstruction, SBInstruction, SInstruction, SyscallInstruction, UInstruction, UJInstruction, }, }; use ark_ff::Zero; use mina_curves::pasta::Fp; use rand::{CryptoRng, Rng, RngCore}; -use strum::EnumCount; +use strum::{EnumCount, IntoEnumIterator}; // Sanity check that we have as many selector as we have instructions #[test] @@ -735,3 +735,182 @@ pub fn test_instruction_decoding_remu() { let (opcode, _instruction) = env.decode_instruction(); assert_eq!(opcode, Instruction::MType(MInstruction::Remu)); } + +#[test] +fn test_regression_number_of_constraints_per_instruction() { + let mut env = constraints::Env::::default(); + let unimplemented_instructions = [ + Instruction::RType(RInstruction::Fence), + Instruction::RType(RInstruction::FenceI), + ]; + let instructions = Instruction::iter() + .flat_map(|x| x.into_iter()) + .filter(|x| !unimplemented_instructions.contains(x)); + for instruction in instructions { + interpret_instruction(&mut env, instruction); + println!("{:?}", instruction); + match instruction { + Instruction::RType(rtype) => match rtype { + RInstruction::Add => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::Sub => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::ShiftLeftLogical => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::SetLessThan => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::SetLessThanUnsigned => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::Xor => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::ShiftRightLogical => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::ShiftRightArithmetic => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::Or => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::And => { + assert_eq!(env.constraints.len(), 4); + } + RInstruction::Fence => { + unimplemented!("Fence should not be implemented"); + } + RInstruction::FenceI => { + unimplemented!("FenceI should not be implemented"); + } + }, + Instruction::IType(itype) => match itype { + IInstruction::LoadByte => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::LoadHalf => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::LoadWord => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::LoadByteUnsigned => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::LoadHalfUnsigned => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::AddImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::SetLessThanImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::SetLessThanImmediateUnsigned => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::XorImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::OrImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::AndImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::ShiftLeftLogicalImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::ShiftRightLogicalImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::ShiftRightArithmeticImmediate => { + assert_eq!(env.constraints.len(), 5); + } + IInstruction::JumpAndLinkRegister => { + assert_eq!(env.constraints.len(), 5); + } + }, + Instruction::SType(stype) => match stype { + SInstruction::StoreByte => { + assert_eq!(env.constraints.len(), 1); + } + SInstruction::StoreHalf => { + assert_eq!(env.constraints.len(), 1); + } + SInstruction::StoreWord => { + assert_eq!(env.constraints.len(), 1); + } + }, + Instruction::SBType(sbtype) => match sbtype { + SBInstruction::BranchEq => { + assert_eq!(env.constraints.len(), 5); + } + SBInstruction::BranchNeq => { + assert_eq!(env.constraints.len(), 5); + } + SBInstruction::BranchLessThan => { + assert_eq!(env.constraints.len(), 3); + } + SBInstruction::BranchLessThanUnsigned => { + assert_eq!(env.constraints.len(), 3); + } + SBInstruction::BranchGreaterThanEqual => { + assert_eq!(env.constraints.len(), 3); + } + SBInstruction::BranchGreaterThanEqualUnsigned => { + assert_eq!(env.constraints.len(), 3); + } + }, + Instruction::UType(utype) => match utype { + UInstruction::LoadUpperImmediate => { + assert_eq!(env.constraints.len(), 4); + } + UInstruction::AddUpperImmediate => { + assert_eq!(env.constraints.len(), 4); + } + }, + Instruction::UJType(ujtype) => match ujtype { + UJInstruction::JumpAndLink => { + assert_eq!(env.constraints.len(), 5); + } + }, + Instruction::SyscallType(syscall) => match syscall { + SyscallInstruction::SyscallSuccess => { + assert_eq!(env.constraints.len(), 0); + } + }, + Instruction::MType(mtype) => match mtype { + MInstruction::Mul => { + assert_eq!(env.constraints.len(), 4); + } + MInstruction::Mulh => { + assert_eq!(env.constraints.len(), 4); + } + MInstruction::Mulhsu => { + assert_eq!(env.constraints.len(), 4); + } + MInstruction::Mulhu => { + assert_eq!(env.constraints.len(), 4); + } + MInstruction::Div => { + assert_eq!(env.constraints.len(), 4); + } + MInstruction::Divu => { + assert_eq!(env.constraints.len(), 4); + } + MInstruction::Rem => { + assert_eq!(env.constraints.len(), 4); + } + MInstruction::Remu => { + assert_eq!(env.constraints.len(), 4); + } + }, + } + env.reset() + } +} diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index c02b240bb4..256de81687 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -88,8 +88,8 @@ impl InterpreterEnv for Env { assert_eq!(*x, *y); } - fn check_boolean(x: &Self::Variable) { - if !(*x == 0 || *x == 1) { + fn assert_boolean(&mut self, x: &Self::Variable) { + if *x != 0 && *x != 1 { panic!("The value {} is not a boolean", *x); } } @@ -214,6 +214,14 @@ impl InterpreterEnv for Env { lowest_bit: u32, position: Self::Position, ) -> Self::Variable { + assert!( + lowest_bit < highest_bit, + "The lowest bit must be strictly lower than the highest bit" + ); + assert!( + highest_bit <= 32, + "The interpreter is for a 32bits architecture" + ); let x: u32 = (*x).try_into().unwrap(); let res = (x >> lowest_bit) & ((1 << (highest_bit - lowest_bit)) - 1); let res = res as u64; diff --git a/o1vm/src/legacy/main.rs b/o1vm/src/legacy/main.rs index ade183ede2..e49de199a0 100644 --- a/o1vm/src/legacy/main.rs +++ b/o1vm/src/legacy/main.rs @@ -5,8 +5,8 @@ use kimchi::o1_utils; use kimchi_msm::{proof::ProofInputs, prover::prove, verifier::verify, witness::Witness}; use log::debug; use o1vm::{ - cannon::{self, Meta, Start, State}, - cli, + cannon::{self, Start, State}, + cli, elf_loader, interpreters::{ keccak::{ column::{Steps, N_ZKVM_KECCAK_COLS, N_ZKVM_KECCAK_REL_COLS, N_ZKVM_KECCAK_SEL_COLS}, @@ -33,7 +33,9 @@ use o1vm::{ test_preimage_read, }; use poly_commitment::SRS as _; -use std::{cmp::Ordering, collections::HashMap, fs::File, io::BufReader, process::ExitCode}; +use std::{ + cmp::Ordering, collections::HashMap, fs::File, io::BufReader, path::Path, process::ExitCode, +}; use strum::IntoEnumIterator; /// Domain size shared by the Keccak evaluations, MIPS evaluation and main @@ -50,18 +52,11 @@ pub fn cannon_main(args: cli::cannon::RunArgs) { // Read the JSON contents of the file as an instance of `State`. let state: State = serde_json::from_reader(reader).expect("Error reading input state file"); - let meta_file = File::open(&configuration.metadata_file).unwrap_or_else(|_| { - panic!( - "Could not open metadata file {}", - &configuration.metadata_file - ) - }); - - let meta: Meta = serde_json::from_reader(BufReader::new(meta_file)).unwrap_or_else(|_| { - panic!( - "Error deserializing metadata file {}", - &configuration.metadata_file - ) + let meta = &configuration.metadata_file.as_ref().map(|f| { + let meta_file = + File::open(f).unwrap_or_else(|_| panic!("Could not open metadata file {}", f)); + serde_json::from_reader(BufReader::new(meta_file)) + .unwrap_or_else(|_| panic!("Error deserializing metadata file {}", f)) }); let mut po = PreImageOracle::create(&configuration.host); @@ -124,7 +119,7 @@ pub fn cannon_main(args: cli::cannon::RunArgs) { } while !mips_wit_env.halt { - let instr = mips_wit_env.step(&configuration, &meta, &start); + let instr = mips_wit_env.step(&configuration, meta, &start); if let Some(ref mut keccak_env) = mips_wit_env.keccak_env { // Run all steps of hash @@ -327,6 +322,14 @@ pub fn cannon_main(args: cli::cannon::RunArgs) { // TODO: Logic } +fn gen_state_json(arg: cli::cannon::GenStateJsonArgs) -> Result<(), String> { + let path = Path::new(&arg.input); + let state = elf_loader::parse_elf(elf_loader::Architecture::Mips, path)?; + let file = File::create(&arg.output).expect("Error creating output state file"); + serde_json::to_writer_pretty(file, &state).expect("Error writing output state file"); + Ok(()) +} + pub fn main() -> ExitCode { env_logger::Builder::from_env(env_logger::Env::default().default_filter_or("info")).init(); let args = cli::Commands::parse(); @@ -338,6 +341,9 @@ pub fn main() -> ExitCode { cli::cannon::Cannon::TestPreimageRead(args) => { test_preimage_read::main(args); } + cli::cannon::Cannon::GenStateJson(args) => { + gen_state_json(args).expect("Error generating state.json"); + } }, } ExitCode::SUCCESS diff --git a/o1vm/src/lookups.rs b/o1vm/src/lookups.rs index eff69771f3..5085e0dae8 100644 --- a/o1vm/src/lookups.rs +++ b/o1vm/src/lookups.rs @@ -25,23 +25,29 @@ pub(crate) type LookupTable = LogupTable; /// All of the possible lookup table IDs used in the zkVM #[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)] pub enum LookupTableIDs { - // PadLookup ID is 0 because this is the only fixed table whose first entry is not 0. - // This way, it is guaranteed that the 0 value is not always in the tables after the - // randomization with the joint combiner is applied. - /// All [1..136] values of possible padding lengths, the value 2^len, and the 5 corresponding pad suffixes with the 10*1 rule + // PadLookup ID is 0 because this is the only fixed table whose first entry + // is not 0. This way, it is guaranteed that the 0 value is not always in + // the tables after the randomization with the joint combiner is applied. + /// All [1..136] values of possible padding lengths, the value 2^len, and + /// the 5 corresponding pad suffixes with the 10*1 rule PadLookup = 0, - /// 24-row table with all possible values for round and their round constant in expanded form (in big endian) [0..=23] + /// 24-row table with all possible values for round and their round constant + /// in expanded form (in big endian) [0..=23] RoundConstantsLookup = 1, /// Values from 0 to 4 to check the number of bytes read from syscalls AtMost4Lookup = 2, - /// All values that can be stored in a byte (amortized table, better than model as RangeCheck16 (x and scaled x) + /// All values that can be stored in a byte (amortized table, better than + /// model as RangeCheck16 (x and scaled x) ByteLookup = 3, - // Read tables come first to allow indexing with the table ID for the multiplicities + // Read tables come first to allow indexing with the table ID for the + // multiplicities /// Single-column table of all values in the range [0, 2^16) RangeCheck16Lookup = 4, - /// Single-column table of 2^16 entries with the sparse representation of all values + /// Single-column table of 2^16 entries with the sparse representation of + /// all values SparseLookup = 5, - /// Dual-column table of all values in the range [0, 2^16) and their sparse representation + /// Dual-column table of all values in the range [0, 2^16) and their sparse + /// representation ResetLookup = 6, // RAM Tables @@ -123,7 +129,8 @@ impl LookupTableID for LookupTableIDs { /// Trait that creates all the fixed lookup tables used in the VM pub(crate) trait FixedLookupTables { - /// Checks whether a value is in a table and returns the position if it is or None otherwise. + /// Checks whether a value is in a table and returns the position if it is + /// or None otherwise. fn is_in_table(table: &LookupTable, value: Vec) -> Option; /// Returns the pad table fn table_pad() -> LookupTable; @@ -144,7 +151,8 @@ pub(crate) trait FixedLookupTables { impl FixedLookupTables for LookupTable { fn is_in_table(table: &LookupTable, value: Vec) -> Option { let id = table.table_id; - // In these tables, the first value of the vector is related to the index within the table. + // In these tables, the first value of the vector is related to the + // index within the table. let idx = value[0] .to_bytes() .iter() diff --git a/o1vm/src/pickles/main.rs b/o1vm/src/pickles/main.rs index 9cc18f9790..a88042eb49 100644 --- a/o1vm/src/pickles/main.rs +++ b/o1vm/src/pickles/main.rs @@ -8,8 +8,8 @@ use mina_poseidon::{ sponge::{DefaultFqSponge, DefaultFrSponge}, }; use o1vm::{ - cannon::{self, Meta, Start, State}, - cli, + cannon::{self, Start, State}, + cli, elf_loader, interpreters::mips::{ column::N_MIPS_REL_COLS, constraints as mips_constraints, @@ -21,7 +21,7 @@ use o1vm::{ test_preimage_read, }; use poly_commitment::{ipa::SRS, SRS as _}; -use std::{fs::File, io::BufReader, process::ExitCode, time::Instant}; +use std::{fs::File, io::BufReader, path::Path, process::ExitCode, time::Instant}; pub const DOMAIN_SIZE: usize = 1 << 15; @@ -37,18 +37,11 @@ pub fn cannon_main(args: cli::cannon::RunArgs) { // Read the JSON contents of the file as an instance of `State`. let state: State = serde_json::from_reader(reader).expect("Error reading input state file"); - let meta_file = File::open(&configuration.metadata_file).unwrap_or_else(|_| { - panic!( - "Could not open metadata file {}", - &configuration.metadata_file - ) - }); - - let meta: Meta = serde_json::from_reader(BufReader::new(meta_file)).unwrap_or_else(|_| { - panic!( - "Error deserializing metadata file {}", - &configuration.metadata_file - ) + let meta = &configuration.metadata_file.as_ref().map(|f| { + let meta_file = + File::open(f).unwrap_or_else(|_| panic!("Could not open metadata file {}", f)); + serde_json::from_reader(BufReader::new(meta_file)) + .unwrap_or_else(|_| panic!("Error deserializing metadata file {}", f)) }); let mut po = PreImageOracle::create(&configuration.host); @@ -72,7 +65,7 @@ pub fn cannon_main(args: cli::cannon::RunArgs) { let mut curr_proof_inputs: ProofInputs = ProofInputs::new(DOMAIN_SIZE); while !mips_wit_env.halt { - let _instr: Instruction = mips_wit_env.step(&configuration, &meta, &start); + let _instr: Instruction = mips_wit_env.step(&configuration, meta, &start); for (scratch, scratch_chunk) in mips_wit_env .scratch_state .iter() @@ -134,6 +127,14 @@ pub fn cannon_main(args: cli::cannon::RunArgs) { } } +fn gen_state_json(arg: cli::cannon::GenStateJsonArgs) -> Result<(), String> { + let path = Path::new(&arg.input); + let state = elf_loader::parse_elf(elf_loader::Architecture::Mips, path)?; + let file = File::create(&arg.output).expect("Error creating output state file"); + serde_json::to_writer_pretty(file, &state).expect("Error writing output state file"); + Ok(()) +} + pub fn main() -> ExitCode { env_logger::Builder::from_env(env_logger::Env::default().default_filter_or("info")).init(); let args = cli::Commands::parse(); @@ -145,6 +146,9 @@ pub fn main() -> ExitCode { cli::cannon::Cannon::TestPreimageRead(args) => { test_preimage_read::main(args); } + cli::cannon::Cannon::GenStateJson(args) => { + gen_state_json(args).expect("Error generating state.json"); + } }, } ExitCode::SUCCESS diff --git a/o1vm/test-gen-state-json.sh b/o1vm/test-gen-state-json.sh new file mode 100755 index 0000000000..61a4387c7c --- /dev/null +++ b/o1vm/test-gen-state-json.sh @@ -0,0 +1,14 @@ +#!/bin/bash + +BIN_DIR=${1:-${BIN_DIR:-o1vm/resources/programs/mips/bin}} + +# Ensure the directory exists +if [[ ! -d "$BIN_DIR" ]]; then + echo "Error: Directory '$BIN_DIR' does not exist." + exit 1 +fi + +find "$BIN_DIR" -type f ! -name "*.o" | while read -r file; do + echo "Processing: $file" + cargo run --bin pickles_o1vm -- cannon gen-state-json -i "$file" +done diff --git a/o1vm/tests/test_elf_loader.rs b/o1vm/tests/test_elf_loader.rs index e473c38ccb..b248f8e79a 100644 --- a/o1vm/tests/test_elf_loader.rs +++ b/o1vm/tests/test_elf_loader.rs @@ -1,3 +1,5 @@ +use o1vm::elf_loader::Architecture; + #[test] // This test is used to check that the elf loader is working correctly. // We must export the code used in this test in a function that can be called by @@ -7,7 +9,7 @@ fn test_correctly_parsing_elf() { let path = curr_dir.join(std::path::PathBuf::from( "resources/programs/riscv32im/bin/fibonacci", )); - let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); // This is the output we get by running objdump -d fibonacci assert_eq!(state.pc, 69932); diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index 4152a5d4bc..556f01b708 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -1,10 +1,27 @@ use mina_curves::pasta::Fp; -use o1vm::interpreters::riscv32im::{ - interpreter::{IInstruction, Instruction, RInstruction}, - witness::Env, - PAGE_SIZE, +use o1vm::{ + elf_loader::Architecture, + interpreters::riscv32im::{ + interpreter::{IInstruction, Instruction, RInstruction}, + registers::RegisterAlias::*, + witness::Env, + PAGE_SIZE, + }, }; +#[test] +fn test_registers_indexed_by_alias() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/sll", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + assert_eq!(witness.registers[Ip], 65652); + assert_eq!(witness.registers[NextIp], 65656); +} + #[test] // Checking an instruction can be converted into a string. // It is mostly because we would want to use it to debug or write better error @@ -29,7 +46,7 @@ fn test_no_action() { let path = curr_dir.join(std::path::PathBuf::from( "resources/programs/riscv32im/bin/no-action", )); - let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); // This is the output we get by running objdump -d no-action assert_eq!(witness.registers.current_instruction_pointer, 69844); @@ -50,15 +67,13 @@ fn test_no_action() { assert_eq!(witness.registers.general_purpose[17], 42); } -// FIXME: stop ignoring when all the instructions are implemented. #[test] -#[ignore] fn test_fibonacci_7() { let curr_dir = std::env::current_dir().unwrap(); let path = curr_dir.join(std::path::PathBuf::from( "resources/programs/riscv32im/bin/fibonacci-7", )); - let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); // This is the output we get by running objdump -d fibonacci-7 assert_eq!(witness.registers.current_instruction_pointer, 69932); @@ -74,21 +89,364 @@ fn test_fibonacci_7() { } } -// FIXME: stop ignore when all the instructions necessary for running this -// program are implemented. #[test] -#[ignore] fn test_sll() { let curr_dir = std::env::current_dir().unwrap(); let path = curr_dir.join(std::path::PathBuf::from( "resources/programs/riscv32im/bin/sll", )); - let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + // Expected output of the program + assert_eq!(witness.registers.general_purpose[5], 1 << 14) +} + +#[test] +fn test_addi() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/addi", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 15); +} + +#[test] +fn test_add_1() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/add_1", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 15); +} + +#[test] +fn test_add_2() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/add_2", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 123); // First number + assert_eq!(witness.registers[T1], 456); // Second number + assert_eq!(witness.registers[T2], 789); // Third number + assert_eq!(witness.registers[T3], 579); // t3 = t0 + t1 + assert_eq!(witness.registers[T4], 1368); // t4 = t3 + t2 + assert_eq!(witness.registers[T5], 912); // t5 = t0 + t2 + assert_eq!(witness.registers[T6], 1368); // t6 = t4 + x0 (Copy t4 to t6) +} + +#[test] +fn test_add_overflow() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/add_overflow", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 0b01111111111111111111111111111111); + assert_eq!(witness.registers[T1], 0b00000000000000000000000000000001); + assert_eq!(witness.registers[T2], 0b10000000000000000000000000000000); + assert_eq!(witness.registers[T3], 0b11111111111111111111111111111111); + assert_eq!(witness.registers[T4], 0b00000000000000000000000000000000); +} + +#[test] +fn test_addi_negative() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/addi_negative", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 100); + assert_eq!(witness.registers[T1], 50); + assert_eq!(witness.registers[T2], (-50_i32) as u32); + assert_eq!(witness.registers[T3], (-1000_i32) as u32); + assert_eq!(witness.registers[T4], (-1500_i32) as u32); +} + +#[test] +fn test_add_sub_swap() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/add_sub_swap", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 10); + assert_eq!(witness.registers[T1], 5); + assert_eq!(witness.registers[T2], 15); +} + +#[test] +fn test_addi_overflow() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/addi_overflow", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T1], (-2147483648_i32) as u32); + assert_eq!(witness.registers[T3], 2147483647); + assert_eq!(witness.registers[T5], 123456789); +} + +#[test] +fn test_addi_boundary_immediate() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/addi_boundary_immediate", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T1], 2147); + assert_eq!(witness.registers[T3], (-1048_i32) as u32); +} + +#[test] +fn test_sub() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/sub", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 500); + assert_eq!(witness.registers[T5], (-100_i32) as u32); +} + +#[test] +fn test_sub_2() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/sub_2", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], -200_i32 as u32); + assert_eq!(witness.registers[T5], 150); +} + +#[test] +fn test_sub_3() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/sub_3", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T1], 0); + assert_eq!(witness.registers[T4], -2147483648_i32 as u32); +} + +#[test] +fn test_xor() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/xor", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 0b0110); // Result: t2 = 0b0110 + assert_eq!(witness.registers[T5], 0b1010); // Result: t5 = 0b1010 + assert_eq!(witness.registers[T1], 0); // Result: t1 = 0 +} + +#[test] +fn test_and() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/and", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 0b1000); + assert_eq!(witness.registers[T5], 0); + assert_eq!(witness.registers[T1], 0b1010); +} + +#[test] +fn test_slt() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/slt", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 1); + assert_eq!(witness.registers[T5], 0); + assert_eq!(witness.registers[T6], 0); +} + +#[test] +#[should_panic] +fn test_div_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/div_by_zero", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +#[should_panic] +fn test_divu_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/divu_by_zero", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +#[should_panic] +fn test_rem_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/rem_by_zero", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +#[should_panic] +fn test_remu_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/remu_by_zero", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +fn test_mul_overflow() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/mul_overflow", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 276447232); +} + +#[test] +fn test_jal() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/jal", + )); + let state = o1vm::elf_loader::parse_elf(Architecture::RiscV32, &path).unwrap(); let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); while !witness.halt { witness.step(); } - // FIXME: check the state of the registers after the program has run. + assert_eq!(witness.registers[T0], 12); + assert_eq!(witness.registers[T1], 7); }