Perna/solidity step

[mpernambuco]

Binary step logs, verified by host, zkVM, and Solidity

One binary log format now describes every provable state transition: N machine
cycles, N uarch cycles, a uarch reset, or a CMIO response. The same log file is
verified by three independent implementations — the C++ host, the RISC0 zkVM
guest, and a Solidity library that now lives in this repo and is transpiled from
the emulator's own sources. The per-access JSON log is gone from the machine
API, and this replaces the separate machine-solidity-step repo.

Highlights:

• One wire format, three verifiers. Record once, verify anywhere: host
  (verify_step, verify_step_uarch, verify_reset_uarch,
  verify_send_cmio_response), RISC0 guest (Groth16 receipt, ~300k gas to
  verify on-chain regardless of cycle count), Solidity (direct re-execution).
• The Solidity verifier is generated, not ported. UArchStep, UArchReset
  and SendCmioResponse are transpiled from the C++ interpreter sources and
  committed; CI fails on drift (make -C solidity-step check-gen-all). The
  two-repo divergence problem is gone by construction.
• Dispute read path for rejected inputs. send_cmio_response takes a revert
  root hash and stores it in a machine shadow slot; when an input is rejected,
  reset_uarch reverts the machine to that recorded state. All of it is
  witnessed by the log, so the on-chain verifier replays it without trusting
  the prover.
• Cheaper on-chain verification. One uarch step: 0.75M gas avg (was 1.04M,
  -28%) and 10 KB calldata (was ~15 KB, -32%) versus the old access-log
  verifier.
• Fixtures are recorded, not committed. Every fixture is regenerated from
  the emulator in seconds, self-checked at record time, and indexed by a
  per-directory manifest. An adversarial corpus of tampered logs must be
  rejected by C++ and Solidity with the same named error.

Step-log anatomy

A step log is a sparse Merkle witness of a state transition (any number of
steps, or a single operation): only the touched parts of the state tree, enough
to recompute the root before and after.

• Page = a 4 KiB leaf, carries the full pre-write data. e.g. p1 = uarch shadow state, p2 = uarch RAM
• Node = a subtree, carries only hash_before + hash_after (no data) — witnesses a bulk write. e.g. n1 = cmio rx buffer
• Sibling = a single hash for an untouched subtree, supplied so the root can still be folded
• Node sources: reset_uarch → uarch-state subtree (hash_after = pristine); send_cmio_response → rx-buffer subtree
• Roots: pages' pre-data + nodes' hash_before (+ siblings) → root before; mutated pages + nodes' hash_after (+ siblings) → root after
• Soundness: every node must be consumed by a real write

Wire format (header + page/node/sibling entries) is specified in
src/step-log.hpp, which is also the shared decoder used by
the host and zkVM replays. The savings over the per-access format come from
amortizing sibling hashes across the whole log instead of repeating ~59 of them
for every read and write.

Scope of the on-chain verifier

solidity-step/ verifies exactly one uarch cycle per log (plus reset and CMIO
response) — the same dispute granularity as the old access-log model.
Multi-cycle logs are a host/zkVM feature; the Solidity entry point rejects them
by design (requested_cycle_count must be 1). The decoder recomputes the
pre-state root from the witnessed tree before replaying and the post-state root
after, so the log bytes are untrusted input throughout.

CLI: cartesi-machine.lua

New / reshaped options that produce binary step logs:

• --log-step-uarch=<filename>[,count:<uarch-cycle-count>][,pretty]
  Log <uarch-cycle-count> microarchitecture cycles (default 1) to a binary
  step log (was a single fixed micro-step). Logging stops early at the uarch
  halt, so a count at or above the per-mcycle budget records one whole mcycle.
  Append ,pretty to also emit a human-readable printout to stderr. The
  printout replaces the old access-log dump (one cycle shown; a log that fails
  the final root check still prints, plus a trailing WARNING):

  1: read uarch.cycle@0x400008: 0x0
  2: read uarch.halt_flag@0x400000: 0x0
  3: read uarch.pc@0x400010: 0x600000
  4: read @0x600000: 0x2002b700600137
  begin lui
    5: write uarch.x2@0x400028: 0x0 -> 0x600000
    6: write uarch.pc@0x400010: 0x600000 -> 0x600004
  end lui
  7: write uarch.cycle@0x400008: 0x0 -> 0x1
  

• --log-reset-uarch=<filename>
  Reset the microarchitecture state and write a binary step log.

• --log-send-cmio-response=reason:<n>,filename:<path>,(file:<path>|hex:<0x…>|str:<text>)
  Send a CMIO response into the rx buffer and write a binary step log. Response
  bytes come from exactly one of file: / hex: / str:. Expects the machine
  yielded (iflags.Y == 1); otherwise the logged transition is a no-op.

Cost of verifying one uarch cycle in Solidity

All uarch cycles of the rv64ui-uarch-add test program, measured in both
formats — same unit of work (one uarch step per log), so apples to apples:

                  old access-log   new binary log   delta
exec gas, worst   1.16M            0.90M            -22%
exec gas, avg     1.04M            0.72M            -31%
calldata          ~15 KB           10 KB            -32%

Cheaper to run and a third less calldata — cheaper on L1, much more so on L2.

Testing

• The full rv64ui-uarch catalog is replayed per-cycle through the Solidity
  verifier, chained root-to-root across each program. Fixture expectations are
  captured from the live recording machine, never from log headers, so a
  corrupted header cannot vouch for itself.
• Reject fixtures are valid logs tampered one field at a time; each carries the
  name of the rejection it must trigger, and both the C++ and Solidity
  verifiers must fail with exactly that error.
• The RISC0 path proves and verifies the same fixtures end to end:
  prove → verify → Groth16 compress → seal verification against the on-chain
  Verifier Router (Sepolia fork).

Building and testing everything from scratch

make distclean
make submodules
make                                       
make build-tests-all
make test

make -C solidity-step                       # needs Foundry (forge version pinned; see README)
make -C solidity-step check-gen-all         # committed transpiled .sol must match the C++ sources
make -C solidity-step fixtures
make -C solidity-step test
make -C solidity-step coverage

make -C risc0                               # needs Docker + rzup toolchains (see risc0/README.md)
make -C risc0 fixtures
make -C risc0 test
make -C risc0 coverage                      # needs cargo-llvm-cov + llvm-tools

Coverage

╭--------------------------+--------------------+--------------------+------------------+------------------╮
| File                     | % Lines            | % Statements       | % Branches       | % Funcs          |
+==========================================================================================================+
| src/HashTree.sol         | 83.33% (35/42)     | 87.50% (49/56)     | 100.00% (5/5)    | 100.00% (3/3)    |
|--------------------------+--------------------+--------------------+------------------+------------------|
| src/SendCmioResponse.sol | 96.00% (24/25)     | 96.77% (30/31)     | 87.50% (7/8)     | 100.00% (1/1)    |
|--------------------------+--------------------+--------------------+------------------+------------------|
| src/StateAccess.sol      | 88.57% (124/140)   | 87.42% (132/151)   | 62.50% (10/16)   | 97.50% (39/40)   |
|--------------------------+--------------------+--------------------+------------------+------------------|
| src/StepLog.sol          | 92.49% (160/173)   | 92.77% (218/235)   | 81.08% (30/37)   | 100.00% (13/13)  |
|--------------------------+--------------------+--------------------+------------------+------------------|
| src/UArchReset.sol       | 100.00% (8/8)      | 100.00% (8/8)      | 100.00% (2/2)    | 100.00% (1/1)    |
|--------------------------+--------------------+--------------------+------------------+------------------|
| src/UArchStep.sol        | 99.70% (661/663)   | 99.79% (962/964)   | 88.52% (108/122) | 100.00% (79/79)  |
|--------------------------+--------------------+--------------------+------------------+------------------|
| src/Verify.sol           | 100.00% (37/37)    | 100.00% (35/35)    | 100.00% (15/15)  | 100.00% (3/3)    |
|--------------------------+--------------------+--------------------+------------------+------------------|
| Total                    | 96.42% (1049/1088) | 96.89% (1434/1480) | 86.34% (177/205) | 99.29% (139/140) |
╰--------------------------+--------------------+--------------------+------------------+------------------╯
mpernam