Fold revert-on-reject into the generated step code#98
Open
diegonehab wants to merge 5 commits into
Open
Conversation
The emulator now records the revert root hash as part of send_cmio_response, so the generated SendCmioResponse.sol takes a bytes32 revertRootHash argument and writes it via EmulatorCompat.writeRevertRootHash. Rename EmulatorCompat.getRevertRootHash and setRevertRootHash to readRevertRootHash and writeRevertRootHash to match the emulator naming. Update generate_SendCmioResponse.sh for the new C++ signature and explicit-instantiation layout. Fix generate_EmulatorConstants.lua to query the renamed cartesi.HTIF_YIELD_* Lua constants and regenerate EmulatorConstants.sol, which also picks up the new UARCH_PRISTINE_STATE_HASH. The SendCmioResponse test passes the catalog's initialRootHash as the revert root hash, matching the regenerated test logs.
Regenerate UArchReset.sol from the emulator. After resetting the uarch state, reset() now reads iflags.Y and conditionally htif.tohost, decodes the dev/cmd/reason fields, and on a rejected manual yield calls the new EmulatorCompat.revertState, which replaces currentRootHash with the value read from the revert root hash leaf. Callers need no substitution logic, the boundary transition in the dispute becomes just step and reset. Delete AdvanceStatus.sol. Its only consumer was Dave's revertIfNeeded, which the fold makes obsolete. Rename the EmulatorConstants yield reason trio from CMIO_YIELD_MANUAL_REASON_* to HTIF_YIELD_MANUAL_REASON_*, matching the emulator naming now that AdvanceStatus is gone, and add the HTIF field shift and mask constants plus HTIF_DEV_YIELD and HTIF_YIELD_CMD_MANUAL, all queried from the emulator by generate_EmulatorConstants.lua. CMIO_YIELD_REASON_ADVANCE_STATE keeps its name, Dave references it. Update generate_UArchReset.sh to prefix EmulatorConstants names like the other generators. Generalize the test json parser to derive per-access sibling counts and to emit the value followed by the leaf hash for leaf read accesses, so mixed-shape logs replay. UArchReset.t.sol now also replays the rejected-reset fixture, whose final root hash is the recorded revert root hash.
github-project-automation
Bot
moved this from Waiting Review
to Waiting Merge
in Machine Unit
The core send_cmio_response can no longer fail. If verification could fail for a reachable machine state and response, there would be states for which the honest party cannot produce a log that proves the resulting state transition. The iflags.Y and response-length checks now return without touching the state, like the advance-state yield check already did. The length check also moves ahead of the revert root hash write, where it can still prevent all state changes. iflags.Y remains the first access, so a no-op log is never empty, which replay requires. The host-facing machine::send_cmio_response still refuses misuse upfront. check_pending_cmio_request takes over the dropped checks, requiring a manual yield for every response reason and a response that fits in the rx buffer, with the same error messages as before. machine::log_send_cmio_response no longer fails for any machine state or response argument and logs a no-op instead.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of cartesi/machine-emulator#388. Companion to cartesi/machine-emulator#389, which must
be referenced for regenerating the constants and test fixtures.
Problem
The EVM verifiers had no way to accept the canonical state transition of a rejected
input. The revert hash was written by a separate
setCheckpointHash-era composition,and the substitution after a rejection was left to the caller (Dave's
revertIfNeeded, built on the in-repoAdvanceStatus.sol).Solution
SendCmioResponse.solis regenerated from the emulator.sendCmioResponsetakes abytes32 revertRootHashfirst argument and commits it into the revert root hash leafvia
EmulatorCompat.writeRevertRootHashas part of the proof(
EmulatorCompat.getRevertRootHash/setRevertRootHashare renamed toreadRevertRootHash/writeRevertRootHashto match the emulator naming).UArchReset.solis regenerated with the reversion folded in. After resetting theuarch state,
reset()readsiflags.Y, conditionally readshtif.tohost, decodesdev/cmd/reason, and on a rejected manual yield calls the new
EmulatorCompat.revertState, which replacescurrentRootHashwith the value readfrom the revert leaf. Callers need no substitution logic, Dave's boundary transition
becomes just
stepandreset, and its input boundary becomes a singlesendCmiocall.
AdvanceStatus.solis deleted, its only consumer wasrevertIfNeeded, which thefold makes obsolete.
EmulatorConstants.solis regenerated. The yield reason trio is renamed fromCMIO_YIELD_MANUAL_REASON_*toHTIF_YIELD_MANUAL_REASON_*, and the HTIF fieldshift/mask constants plus
HTIF_DEV_YIELDandHTIF_YIELD_CMD_MANUALare added,all queried from the emulator (
CMIO_YIELD_REASON_ADVANCE_STATEkeeps its name,Dave references it).
EmulatorConstantsnames inUArchReset.sol.Tests
The json log parser is generalized to derive per-access sibling counts and to emit the
value followed by the leaf hash for leaf read accesses, so mixed-shape logs replay.
SendCmioResponse.t.solpasses the catalog's initial root hash as the revert roothash, and
UArchReset.t.soladditionally replays the new rejected-reset fixture, whosefinal root hash is the recorded revert root hash. All 56 Foundry suites pass against
fixtures regenerated from the emulator PR (Foundry v1.4.3, as pinned by CI).