Skip to content

feat: improve cpp to solidity conversion #95

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mpernambuco wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat: improve cpp to solidity conversion #95

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions .github/workflows/test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,16 @@ jobs:
with:
submodules: recursive

- name: Install gpp
run: sudo apt-get install -y gpp
- name: Install gpp and lua
run: sudo apt-get install -y gpp lua5.4 liblua5.4-dev luarocks

- name: Install LPEG
run: sudo luarocks --lua-version=5.4 install lpeg

- uses: ./.github/actions/setup

- name: Run all tests
run: make test-all
run: eval "$(luarocks --lua-version=5.4 path)" && make test-all

coverage-mock:
runs-on: ubuntu-24.04
Expand Down
45 changes: 38 additions & 7 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
EMULATOR_DIR ?= ../emulator
LUA ?= lua5.4
TEST_DIR := test
DOWNLOADDIR := downloads
SRC_DIR := src
Expand Down Expand Up @@ -36,18 +37,30 @@ help:
@echo ' generate-prod - generate production library code'
@echo ' generate-replay - generate replay tests'
@echo ' pretest - download necessary files for tests'
@echo ' local-dep - use test data from local emulator build'
@echo ' submodules - initialize and update git submodules'
@echo ' fmt - format solidity sources with forge fmt'
@echo ' test-all - test all'
@echo ' test-transpiler - test the C++ to Solidity transpiler'
@echo ' test-mock - test binary files with mock library'
@echo ' test-prod - test production code'
@echo ' test-replay - test log files'
@echo ' env-check - check that all required tools are installed'
@echo 'Coverage targets:'
@echo ' coverage-mock - generate coverage info for mock library tests'
@echo ' coverage-prod - generate coverage info for production code tests'
@echo ' coverage-report - aggregate coverage info and generate html report'


env-check:
@echo "Checking development environment..."
@$(LUA) -v 2>&1 || { echo "MISSING: lua5.4 -- see README.md"; exit 1; }
@$(LUA) -e 'require("lpeg")' 2>/dev/null || { echo "MISSING: lpeg -- see README.md"; exit 1; }
@forge --version 2>&1 || { echo "MISSING: foundry -- see README.md"; exit 1; }
@gpp --version >/dev/null 2>&1 || { echo "MISSING: gpp -- see README.md"; exit 1; }
@$(SED) --version >/dev/null 2>&1 || { echo "MISSING: GNU sed (set SED=gsed on macOS) -- see README.md"; exit 1; }
@echo "All tools found."

all: build test-all

build: generate-step generate-reset generate-send-cmio-response generate-constants generate-prod
Expand All @@ -58,7 +71,10 @@ clean:
rm -rf $(DEPDIRS) $(DOWNLOADDIR)
forge clean

test-all:
test-transpiler:
$(LUA) helper_scripts/test_generate_UArchSolidity.lua

test-all: test-transpiler
$(MAKE) test-mock
$(MAKE) test-replay
$(MAKE) test-prod
Expand Down Expand Up @@ -112,14 +128,19 @@ generate-replay:
generate-constants: $(EMULATOR_DIR)
EMULATOR_DIR=$(EMULATOR_DIR) ./helper_scripts/generate_EmulatorConstants.sh

generate-step: $(EMULATOR_DIR)/src/uarch-step.h $(EMULATOR_DIR)/src/uarch-step.cpp
EMULATOR_DIR=$(EMULATOR_DIR) ./helper_scripts/generate_UArchStep.sh
GEN_SOL = $(LUA) helper_scripts/generate_UArchSolidity.lua

generate-step: $(EMULATOR_DIR)/src/uarch-step.hpp $(EMULATOR_DIR)/src/uarch-step.cpp
$(GEN_SOL) $(EMULATOR_DIR)/src/uarch-step.cpp src/UArchStep.sol UArchStep step
forge fmt src/UArchStep.sol

generate-reset: $(EMULATOR_DIR)/src/uarch-reset-state.cpp
EMULATOR_DIR=$(EMULATOR_DIR) ./helper_scripts/generate_UArchReset.sh
$(GEN_SOL) $(EMULATOR_DIR)/src/uarch-reset-state.cpp src/UArchReset.sol UArchReset reset
forge fmt src/UArchReset.sol

generate-send-cmio-response: $(EMULATOR_DIR)/src/uarch-reset-state.cpp
EMULATOR_DIR=$(EMULATOR_DIR) ./helper_scripts/generate_SendCmioResponse.sh
generate-send-cmio-response: $(EMULATOR_DIR)/src/send-cmio-response.cpp
$(GEN_SOL) $(EMULATOR_DIR)/src/send-cmio-response.cpp src/SendCmioResponse.sol SendCmioResponse sendCmioResponse
forge fmt src/SendCmioResponse.sol

fmt:
forge fmt src test
Expand All @@ -130,6 +151,16 @@ pretest: dep

dep: $(DEPDIRS)

EMULATOR_TESTS_DIR = $(EMULATOR_DIR)/tests
EMULATOR_UARCH_BIN_DIR = $(EMULATOR_TESTS_DIR)/build/uarch
EMULATOR_UARCH_LOG_DIR = $(EMULATOR_TESTS_DIR)/build/uarch-riscv-tests-json-logs

local-dep: $(EMULATOR_UARCH_BIN_DIR) $(EMULATOR_UARCH_LOG_DIR)
rm -rf $(TESTS_DATA_DIR) $(LOG_TEST_DIR)
mkdir -p $(TESTS_DATA_DIR) $(LOG_TEST_DIR)
cp $(EMULATOR_UARCH_BIN_DIR)/*.bin $(TESTS_DATA_DIR)/
cp $(EMULATOR_UARCH_LOG_DIR)/*.json $(LOG_TEST_DIR)/

$(DOWNLOADDIR):
@mkdir -p $(DOWNLOADDIR)
@wget -nc $(TESTS_DATA_DOWNLOAD_URL) -P $(DOWNLOADDIR)
Expand All @@ -154,4 +185,4 @@ $(LOG_TEST_DIR): | download
submodules:
git submodule update --init --recursive

.PHONY: help all build clean checksum-download shasum-download fmt generate-mock generate-prod generate-replay generate-step download pretest dep submodules test-all test-mock test-prod test-replay generate-constants generate-reset generate-send-cmio-response coverage-mock coverage-prod coverage-report
.PHONY: help all build clean checksum-download shasum-download fmt generate-mock generate-prod generate-replay generate-step download pretest dep local-dep submodules test-all test-mock test-prod test-replay test-transpiler env-check generate-constants generate-reset generate-send-cmio-response coverage-mock coverage-prod coverage-report
178 changes: 113 additions & 65 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,104 +1,152 @@
# Cartesi RISC-V Solidity Emulator

The Cartesi RISC-V Solidity Emulator is the on-chain host implementation of the Cartesi Machine Specification. The libraries and contracts are written in Solidity, and the testing scripts are written in Solidity (with the help of [Foundry](https://github.com/foundry-rs/foundry)). **_Do not recommend running `forge` command directly, as there are many scripts and templates working together. Please use `make` instead._**
On-chain Solidity implementation of the [Cartesi Machine](https://github.com/cartesi/machine-emulator) state transition function. The core libraries (`UArchStep`, `UArchReset`, `SendCmioResponse`) are transpiled directly from the emulator's C++ sources to guarantee bit-exact equivalence.

For Cartesi's design to work, this implementation must have the exact transition function as the off-chain [Cartesi RISC-V Emulator](https://github.com/cartesi/machine-emulator), meaning that if given the same initial state (s[i]) both implementation's step functions should reach a bit by bit consistent state s[i + 1].
> Use `make` for all build and test operations -- code generation must run before compilation.

Since the cost of storing a full Cartesi Machine state within the blockchain is prohibitive, all machine states are represented in the blockchain as cryptographic hashes. The contents of those states and memory represented by those hashes are only known off-chain.
## Quick start

Cartesi uses Merkle tree operations and properties to ensure that the blockchain has the ability to correctly verify a state transition without having full state-access. However, the RISC-V Solidity emulator abstracts these operations away and acts as if it knows the full contents of a machine state - it uses the Memory Manager interface to fetch or write any necessary words to memory.
Set up your environment, then build and test:

## AccessLogs
export EMULATOR_DIR=../machine-emulator # path to machine-emulator checkout
export SED=gsed # macOS only (brew install gnu-sed)

The `AccessLogs.Context` struct is consumed by the RISC-V Solidity emulator as if the entire state content was available - since the off and on-chain emulators match down to the order in which accesses are logged. When a dispute arises, Alice packs her off-chain state access log referent to the disagreement step in an struct `AccessLogs.Context`, which will guide the execution of a `step` (i.e state transition function).

The `AccessLogs` library implements the RISC-V Solidity emulator all necessary read and write operations.
make submodules
make build
make test-all

It also makes sure that all accesses performed by the `step` function match the ones provided by Alice and are consistent with the Merkle proofs provided by her. If that is not the case, Alice loses the dispute.
## Prerequisites

## Step function
make env-check # verify everything is installed

`MetaStep.step` is the top-level state transition function, it is meant to take the machine from state s[i] to state[i + 1], using the `AccessLogs` as an assistant. It receives a `counter` and an `AccessLogs.Context` - the latter populated with the access log generated by the emulator off-chain - and returns a `UArchStepStatus` signaling the result of its execution. Internally it runs one micro-step via `UArchStep.step` and, every `1 << LOG2_CYCLES_TO_RESET` cycles, also runs `UArchReset.reset` to reset the micro-architecture state.
- [Foundry](https://book.getfoundry.sh/) 1.4.3
- GNU Make >= 3.81
- Lua 5.4, LuaRocks, LPEG
- GNU sed (gsed on macOS)
- GPP >= 2.27

During a `MetaStep.step` execution, every necessary read or write (be it to memory, registers etc) is processed and verified by the `AccessLogs`.
<details>
<summary>macOS (Homebrew)</summary>

## Execute Instruction
brew install lua luarocks gpp gnu-sed
luarocks install lpeg
curl -L https://foundry.paradigm.xyz | bash
foundryup -i v1.4.3

The `UArchStep` library implements a single micro-architecture instruction step (`UArchStep.step`), and is invoked by `MetaStep.step`. It consists of the machine instruction logic, such as decoding, executing, opcode matching and etc. The Solidity implementation is converted from the Cpp implementation directly through a translator script. This is to assure that the implementations in two languages are identical. Yet the low level differences in two languages are wrapped in the Compatibility Layer.
Add to your shell profile:

## Compatibility Layer
eval "$(luarocks path)"

The `EmulatorCompat` contract is taking care of all the differences in the two implementations. Ranging from programming languages (Cpp versus Solidity) to architectural differences (RISC-V versus EVM).
</details>

## Getting Started
<details>
<summary>macOS (MacPorts)</summary>

Run `make help` for a list of target options. Here are some of them:
sudo port install lua54 luarocks gpp gsed
luarocks install lpeg
curl -L https://foundry.paradigm.xyz | bash
foundryup -i v1.4.3

```
Cleaning targets:
clean - clean the cache artifacts and generated files
Generic targets:
* all - build solidity code. To build from a clean clone, run: make submodules all
build - build solidity code
generate-step - generate solidity-step code from cpp
generate-reset - generate solidity-reset code from cpp
generate-send-cmio-response - generate solidity-send-cmio-response code from cpp
generate-constants - generate solidity-constants code by querying the cartesi machine
generate-mock - generate mock library code
generate-prod - generate production library code
generate-replay - generate replay tests
pretest - download necessary files for tests
submodules - initialize and update git submodules
fmt - format solidity sources with forge fmt
test-all - test all
test-mock - test binary files with mock library
test-prod - test production code
test-replay - test log files
Coverage targets:
coverage-mock - generate coverage info for mock library tests
coverage-prod - generate coverage info for production code tests
coverage-report - aggregate coverage info and generate html report
```
Add to your shell profile:

### Prerequisite
eval "$(luarocks path)"
export SED=gsed

- Build [Cartesi docker image](https://github.com/cartesi/machine-emulator#getting-started)
</details>

### Requirements
<details>
<summary>Linux (Ubuntu/Debian)</summary>

- Foundry 1.4.3
- GNU Make >= 3.81
- GNU sed >= 4.9
- GPP >= 2.27
sudo apt install lua5.4 liblua5.4-dev luarocks gpp
sudo luarocks install lpeg
curl -L https://foundry.paradigm.xyz | bash
foundryup -i v1.4.3

Different version of tools maybe working but is not guaranteed.
Add to your shell profile:

### Install
eval "$(luarocks path)"

Install dependencies and build:
</details>

make submodules all
## Testing

### Run tests
make test-transpiler # transpiler unit tests (fast)
make test-mock # rv64i instruction tests against mock AccessLogs
make test-prod # production AccessLogs integration tests
make test-replay # replay 56 emulator step logs with full Merkle verification (~1 min)
make test-all # all of the above

There are two types of tests that can be run on the Solidity Emulator.
### Using local emulator test data

1. Load binary rv64i test programs in Solidity and verify the execution result
2. Collect step logs and proofs of a test program and replay them in Solidity, verify all accesses and proofs.
By default, test data (binaries and JSON step logs) is downloaded from a
GitHub release. When developing against a local emulator build, generate and
use local test data instead:

Run all tests:
# one-time: generate step logs in the emulator repo
make -C $EMULATOR_DIR/tests test-generate-uarch-logs

# use them here
make local-dep
make test-all

(**_target test-replay is very time consuming_**)
This ensures the constants and test data come from the same emulator build.

## Contributing
### Coverage

make coverage-mock
make coverage-prod
make coverage-report # html report in coverage/

## Code generation

The build step runs these automatically; you only need them when
iterating on a specific piece:

make generate-step # uarch-step.cpp -> UArchStep.sol
make generate-reset # uarch-reset-state.cpp -> UArchReset.sol
make generate-send-cmio-response # send-cmio-response.cpp -> SendCmioResponse.sol
make generate-constants # EmulatorConstants.sol (from emulator Lua bindings)
make generate-mock # mock AccessLogs library
make generate-prod # production AccessLogs library

## Architecture

This implementation must produce the exact same state transition as the
off-chain emulator: given initial state s[i], both must reach s[i+1] bit for
bit. Machine states live on-chain as Merkle tree root hashes; their contents
are only known off-chain. Merkle proofs let the blockchain verify individual
transitions without storing the full state.

Thank you for your interest in Cartesi! Head over to our [Contributing Guidelines](CONTRIBUTING.md) for instructions on how to sign our Contributors Agreement and get started with Cartesi!
### Components

**MetaStep** -- Entry point. Runs one micro-step via `UArchStep.step` and
periodically resets the micro-architecture via `UArchReset.reset`.

**UArchStep** -- One micro-architecture instruction step (transpiled from
`uarch-step.cpp`). Decodes and executes RISC-V opcodes.

**UArchReset** -- Resets micro-architecture state (transpiled from
`uarch-reset-state.cpp`).

**SendCmioResponse** -- Handles CMIO yield responses (transpiled from
`send-cmio-response.cpp`).

**AccessLogs** -- Provides Merkle-verified read/write access to machine state.
During a dispute, the claimant supplies an access log with sibling hashes;
every read and write is checked against the Merkle root. Inconsistencies mean
the claimant loses.

**EmulatorCompat** -- Bridges C++/Solidity differences (endianness, type
widths, calling conventions).

**EmulatorConstants** -- Addresses, sizes, and hashes auto-generated from the
emulator's Lua bindings.

## Contributing

Please note we have a [Code of Conduct](CODE_OF_CONDUCT.md), please follow it in all your interactions with the project.
See [Contributing Guidelines](CONTRIBUTING.md) and our
[Code of Conduct](CODE_OF_CONDUCT.md).

## License

The machine-solidity-step repository and all contributions are licensed under
[APACHE 2.0](https://www.apache.org/licenses/LICENSE-2.0). Please review our [LICENSE](LICENSE) file.
[Apache 2.0](https://www.apache.org/licenses/LICENSE-2.0). See [LICENSE](LICENSE).
54 changes: 0 additions & 54 deletions helper_scripts/generate_SendCmioResponse.sh
View file
Open in desktop

This file was deleted.

Loading
Loading