Prove revert-on-reject state transitions#389
Open
diegonehab wants to merge 137 commits into
Open
Conversation
The dtc interrupt-provider checker warns that interrupt providers must declare both #address-cells and #interrupt-cells. The per-CPU riscv,cpu-intc node only set #interrupt-cells, surfacing a lint warning whenever the DTB was decompiled (e.g. via dtc -I dtb -O dts /sys/firmware/fdt inside a running machine). The node has no addressable children, so #address-cells = <0> is the right value and Linux's behaviour is unchanged. The DTB bytes do change, so every freshly-instantiated machine's state hash shifts going forward.
Expose the revert_root_hash shadow register (at AR_SHADOW_REVERT_ROOT_HASH_START) through all API layers: machine, i_machine/local_machine (NVI pattern), JSON-RPC client/server, cm.h C API, and Lua bindings. Previously the only way to reach this register from Lua or the C API was write_memory/read_memory against the magic offset.
Add cm_pma_did enum to cm.h with all device IDs (empty, memory, shadow state, flash drive, CLINT, HTIF, PLIC, CMIO RX/TX, uarch shadow, VirtIO, NVRAM). Static asserts in cm.cpp verify the values against pmas-defines.h. Expose all constants as cartesi.PMA_*_DID in the Lua API via clua-cartesi.cpp.
Before: DTB_BOOTARGS_ROOT glued the kernel `root=` and `init=`
arguments into one string, and DTB_BOOTARGS_INIT was the combined
default for dtb.bootargs. cm.h mirrored that shape with CM_ prefix.
Two issues. The atom set (CONSOLE / UIO / ROOT / INIT in cm.h) was
asymmetric: ROOT covered two kernel arguments, so splicing one
without the other required parsing. And the project-wide <NAME>_INIT
convention ("initial value of NAME", as in PC_INIT, MCYCLE_INIT,
MARCHID_INIT) collides with any symmetrisation that puts INIT on the
init= atom.
After: one atom per kernel argument, suffixed _PART; DTB_BOOTARGS_INIT
returns to meaning the combined initial value.
DTB_BOOTARGS_CONSOLE_PART "quiet earlycon=sbi console=hvc0 "
DTB_BOOTARGS_UIO_PART "uio_pdrv_genirq.of_id=generic-uio "
DTB_BOOTARGS_ROOT_PART "root=/dev/pmem0 rw"
DTB_BOOTARGS_INIT_PART "init=/usr/sbin/cartesi-init"
DTB_BOOTARGS_INIT (CONSOLE_PART UIO_PART ROOT_PART INIT_PART)
cm.h mirrors with CM_ prefix; cm.cpp's static_asserts match the new
set. clua-cartesi.cpp exposes the four _PART atoms alongside the
unchanged DTB_BOOTARGS_INIT. cartesi-machine.lua's
--no-root-flash-drive handler now strips both ROOT_PART and
INIT_PART (the previous single gsub against the glued DTB_BOOTARGS_ROOT
covered both); the spec-cm-cli.lua assertion that `pmem0` and `init=`
are absent after the flag continues to pass.
- Add docgen.lua filter that executes {pipe=sh} blocks and spans,
splicing command stdout back into the document.
- Add host-replacements/_build_all.sh orchestrator that runs every
expensive helper once and caches outputs under $CACHE_DIR, so every
block/span reduces to a `cat` of a pre-computed file.
- Rewrite README.md.template: %machine.* placeholders replaced with
pipe spans (or printf forms for mixed-content backtick spans).
- Simplify Dockerfile around cartesi/machine-emulator:$TAG: drop the
panpipe stage, install pandoc + net-tools + genext2fs, symlink
doc-local images into /usr/share/cartesi-machine/images so the
emulator finds them at its default paths.
- Update Makefile rule to invoke pandoc with --lua-filter docgen.lua.
- Remove panpipe.diff.
Compatibility fixes uncovered along the way:
- Lua 5.4: cartesi.machine(require "X") now passes require's two
return values; split into a local + call in every helper script.
- Use sha256sum (Debian) instead of shasum.
- Add `printf --` terminator so spans starting with `--flag=...`
aren't parsed as printf options.
Mirror the DEV_ENV_HAS_TOOLCHAIN dispatch pattern from src/Makefile: - Add DEV_ENV_HAS_DOCGEN ?= no to doc/Makefile. The README.md rule delegates to playground-exec when unset, and falls through to the direct pandoc invocation (_README.md.local) when set to "yes". - Set ENV DEV_ENV_HAS_DOCGEN=yes in doc/Dockerfile so the recursive make README.md call inside the container takes the local branch without looping. - Fix playground-exec: use $(PLAYGROUND_IMAGE):$(TAG) (was cartesi/machine-emulator:linux-env), mount doc/ at /work (was /opt/cartesi/machine-emulator, leaving the Dockerfile symlinks dangling), rename hostname to playground. - Install make in the playground image. - Drop the empty images: phony target.
A Makefile under doc/recipes/ replaces the 226-line bash orchestrator. Required cache files are auto-detected from the template, and script- to-script dependencies are auto-derived by grep'ing each recipe for $CACHE_DIR reads. Default convention is one script per cache key (cache.<key>.sh -> $CACHE_DIR/<key>.out); five multi-output workloads (rolling-ioctl-echo-loop, rolling-calc-template, remote, remote-end, lua.remote) use grouped targets. Retarget to cartesi/playground:0.5.0, the pre-uarch version the docs were written for. Switch pandoc to the markdown reader (2.9.2.1 lacks gfm+attributes), convert template fence attrs to pandoc syntax, and revert addresses to the long-form layout used by 0.5.0. Move CACHE_DIR under doc/recipes/cache so it persists via the existing $(CURDIR) bind mount instead of the ephemeral /tmp/ path.
Add a `cache=FILE` attribute handled by the lua filter that reads
$CACHE_DIR/FILE and substitutes the contents - collapsing the most
common pipeline pattern from a 3-line ```{pipe=sh}\ncat ...\n```
fence to a 2-line ```{cache=X.out}\n``` fence (42 block sites).
Inline forms use an empty bracketed Span: []{cache=X.out} for a
plain substitution, [...]{cache=X.out} for a value with a literal
trailing ellipsis. The Span body becomes the suffix and the whole
thing renders as inline Code, so hashes etc. stay monospace inline
(27 inline sites).
Inline `pipe=sh` Code now keeps its Code wrapper instead of being
replaced by a plain Str, so the few remaining inline shell
substitutions also render as monospace.
Pandoc 2.9.2.1's gfm writer renders unattributed CodeBlocks as
4-space-indented; give classless substitutions a synthetic .text
class so they emit as fenced ``` blocks consistently.
recipes/Makefile auto-detection picks up `cache=KEY.out` references
alongside the existing `$CACHE_DIR/KEY.out` reads.
Each cache.*.sh now declares its own outputs and reads as bash arrays before sourcing lib.sh, which emits a self-contained make rule to stdout when invoked with --emit-deps. The Makefile shrinks to ~25 lines: one pattern rule generates each .d sidecar, a second pattern rule runs single-output scripts, and -include pulls everything in. docgen.lua emits template.d as a standard make rule augmenting the all target's prereqs directly. Also replace the &&-chained subshells in 20 scripts with flat command sequences: set -euo pipefail (inherited from lib.sh) handles abort-on-error correctly, and trap '...' EXIT guarantees artifact cleanup on both success and failure.
- Fold strip-ansi.sh's sed/tr pipe into docgen.lua's read_cache(); cache .out files now hold raw output and 34 cache.*.sh scripts drop the trailing | bash strip-ansi.sh pipe. - Move `cd "$HERE"` from 20 cache scripts into lib.sh, after the --emit-deps early exit. - Add .DELETE_ON_ERROR: to recipes/Makefile so a failed recipe does not leave a stale target that Make treats as up-to-date; drop the $@.tmp && mv atomic-write workaround from the %.sh.d rule. - Add .NOTPARALLEL: to recipes/Makefile because cache scripts share files in $HERE and bind fixed localhost ports, so make -jN would corrupt state or fail with EADDRINUSE. - Inline the _README.md.local helper target into README.md and add a clean target in doc/Makefile.
- Add `script=<KEY> [name=<NAME>] [subst=VAR->KEY,...]` attribute to
docgen.lua. It extracts a `# docs:begin/end` region from
`recipes/cache.<KEY>.sh`, strips the trailing `> "$out" 2>&1` redirect,
and substitutes `$VAR` references with the value of `cache/<KEY>.out`.
Eliminates the duplication where the README hand-typed a command above
the cached output of a script that ran a different command.
- Rename the existing `cache=<KEY>.out` attribute to `output=<KEY>`. The
`.out` extension was an internal cache-layout detail.
- Promote RECIPES_DIR to the canonical, configurable env var; CACHE_DIR
is unconditionally derived as `$(RECIPES_DIR)/cache`. Both Makefiles
and docgen.lua now share this anchor.
- Add `# docs:begin/end` markers and convert 16 README blocks to the new
form (limit-exec, nothing, persistent-flash, persistent-machine,
persistent-stored-hash, proofs-pristine-run, rarely-append-bootargs-
loglevel, rarely-append-bootargs-single-id, rarely-id, rarely-periodic-
hashes, rarely-step, remote, rolling-ioctl-echo-loop, state-hashes-
limit-exec, state-hashes-no-limit, templates-store).
- persistent-{machine,stored-hash} now name the store directory after the
final state hash (`machine-$hash`) so the displayed
`--load="machine-<HASH>"` matches what actually runs.
Continues the script= migration. Each conversion replaces a hand-typed fenced bash block in README.md.template with a script= attribute that extracts the displayed command from the same cache.<KEY>.sh file that produces the cached output, eliminating prose/recipe drift. - ls: trivial single-region wrap. - flash: recipe is now self-contained — runs mkdir foo and writes bar.txt at build time inside named "setup" / "run" regions, so the README displays the same multi-step pipeline the prose previously hand-typed. The pre-existing recipes/foo/ orphan is removed; trap cleans up foo, foo.tar, foo.ext2. - templates-run: split into templates-run.sh (cartesi-machine invocation, persists output.raw which is gitignored) and a new templates-run-result.sh (depends on it via reads=, runs the displayed lua5.3 line). The long decimal result, previously hand-typed in the template as a constant, is now driven by the cached output of templates-run-result. - proofs-output-run: wrap the post-setup truncate-through-cartesi- machine section. Template's leading "rm -f output.raw" is dropped (recipe trap handles cleanup). - interactive-ls: intentionally not converted; recipe heredoc form would mislead readers about how to use interactive mode. Header comment in the recipe documents the decision. Also fix bugs in three cache recipes - templates-hash: redirections were in the wrong order (2>&1 > "$out"), letting stderr leak to the terminal and capturing only stdout. Fixed to > "$out" 2>&1. - remote-begin-client: the recipe ran --remote-shutdown so the background server would terminate, but the prose at this section shows --no-remote-destroy. The captured "shutting down" message was therefore wrong relative to what the README displays. Folded the capture into remote-end.sh (which already runs the prose-correct first invocation) and removed the divergent recipe. - rolling-calc-template: the printf-built JSON missed a comma after the "msg_sender" line; same typo lived in the prose heredocs. rollup-memory-range happened to accept both, but the input is still invalid JSON. Added the comma in all four locations.
Convert templates-hash, templates-run-result, proofs-input-json,
remote-end (begin/end-client), rolling-calc-template
(template/client), and rolling-ioctl-echo-loop (encode) blocks to
script= filter invocations using # docs:begin/end region markers.
Also fix the parallel JSON missing-comma bug in
rolling-ioctl-echo-loop msg_sender (matching the Tier 3
rolling-calc-template fix), align payload strings with prose
("hello from input N!" with trailing !), and make
persistent-flash.sh self-contained so it no longer depends on
flash.sh leaving foo/ behind.
Bash bodies move from doc/recipes/*.sh into the doc template itself as keyed code blocks. Each block carries its dependencies, outputs, and render directive (replace=output|source|null) inline -- no more matching identifiers between *.sh files and the template, no more .null declarations, no more separate inputs=/outputs= attributes layered on the reference site. docgen.lua walks the template in document order, hashing each resolved body, writing recipes/cache/<hash>/script.sh, and emitting a Make 3.81 fragment with primary+sibling rules for multi-output scripts. The $K substitution resolves to the dep's cache directory using longest-key matching against the in-memory key map, so dotted/dashed keys parse unambiguously. Cache invalidation is structural: a body change rehashes it; a dep change rehashes consumers because dep paths are textually substituted into the body before hashing. The lib.sh preamble is gone -- docgen.lua prepends the preamble to each cached script directly. The 74 doc/recipes/*.sh files and lib.sh are deleted.
docgen.lua - Replace the single-pass walk with two passes. Pass 1 records every key= block body into `pending` via pandoc.walk_block. Pass 2 walks in document order; each ref=K (or subst=...->K) calls ensure_defined(K), which lazily defines K via DFS through depends=. Both ref= and depends= are now order-independent within the template -- a key= block may sit anywhere relative to the prose and the inline references that use it. - Make replace= required on every key=/ref= site. No more implicit "source" / "output" defaults that hid intent. - Document the full pipeline in the file header: dry-run with DEPS_FILE emits a self-contained makefile fragment; the outer Makefile includes it so `make` populates the cache via topological execution of cache/<hash>/script.sh recipes; the real run reads the cached outputs and renders the final document. - Simplify the script PREAMBLE: drop the $HERE indirection. Scripts now cd into their own cache directory and use a relative `out` variable, which matches what authors actually write in block bodies. README.md.template - Replace seven hardcoded hashes (three 64-hex command outputs, four trunc-8 inline references) with derived ref= blocks driven by merkle-tree-hash recipes. With the order-independent filter, every key= definition now lives at its visual location. - Consolidate the "create the calculator template" setup that had been duplicated across seven keys. The canonical instance lives on templates-store as outputs=out,calculator-template; consumers reach the artifact via depends=templates-store/calculator-template plus a one-line ln -s symlink prelude. This caught a latent bug where the duplicated copies had been silently omitting --append-rom-bootargs="single=yes". - Convert the remaining inline backtick-form ref placeholders to the empty-Span form for consistency. Build infrastructure - doc/Makefile: add a run-playground target for an interactive shell in the playground container. - doc/recipes/Makefile: drop .NOTPARALLEL -- recipes are independent and safe to run in parallel under make. - doc/recipes/find-htif-putchar.lua: switch to require"config.nothing-to-do" to match the directory layout. - doc/recipes/config/nothing-to-do.lua: regenerate as a full dumped config (baseline refresh).
Validate that every base key (key=, depends=, subst=, ref=) matches [a-zA-Z_][a-zA-Z0-9_]* at parse time, so dots and hyphens are caught immediately with a named-offender error rather than failing later with a confusing pattern mismatch. Add a postamble in build_script_content that checks each declared output exists after the body runs. Without this, a missing "> "$out"" redirect produces either a cryptic "cannot open .../out" from the downstream consumer or a "No rule to make target" from make -- both blaming the wrong place. The postamble exits with "key=<name>: declared output "<sub>" was not created" pointing at the producing block. The postamble is only in the generated script; sources[key] (used by replace=source) holds the substituted body only, so rendered source blocks are unaffected.
Replaces the old "every block redirects to $out, strip_redirect scrubs
it from rendered source" scheme with a uniform addressing system and
runner-side capture.
docgen.lua
- PREAMBLE now self-captures all three streams via process substitution:
exec > >(tee stdout >> both) 2> >(tee stderr >> both)
so script bodies are pure code in their own language. The combined
`both` file is roughly time-ordered (two parallel tees, not byte-exact
kernel ordering); good enough for current consumers, swap to script(1)
if a block ever needs precise interleaving.
- The PREAMBLE EXIT trap closes FDs 1/2 *before* `wait` so the tees see
EOF and exit; without the close, `wait` deadlocks (trap runs while the
shell still holds the tee pipes open, tees never EOF).
- Reserved names {stdout, stderr, both, source, null} cannot appear in
outputs=. Single addressing scheme covers display, references, and
substitutions:
replace=<thing> -- own stream/artifact/source
replace=K/<thing> -- cross-block
replace=null -- drop
subst=VAR->K[/<thing>] -- substitute in rendered source
`ref=` and `block=` are folded into the slash-form. `subst=` and
`depends=` defaults updated (both -> stream, stdout -> stream prereq).
- emit_rule emits stdout/stderr/both as siblings; declared artifacts
remain. strip_redirect, resolve_ref, sub_to_filename, and the per-out
variable emission are gone.
README.md.template
- Big-bang migration of all ~88 key blocks and ~60 inline references:
cmd > "$out" 2>&1 -> cmd, plus replace=both
cmd > "$out" -> cmd, plus replace=stdout
cmd 2> "$out" -> cmd, plus replace=stderr (rarely_step)
> "$out_X" 2>&1 -> > X 2>&1 (cwd is the cache dir)
ref=K replace=output -> replace=K/<thing>
block=R replace=source -> replace=source/R
- Multi-output blocks (cmdline_remote, cmdline_remote_end,
rolling_ioctl_echo_loop, rolling_calc_template) wrap their per-region
cartesi-machine commands in `{ ... } > <artifact> 2>&1` braces with
# docs:begin/end *inside* the braces, so the redirect stays out of the
rendered source without needing strip_redirect.
- Cycle/hash readers that flow through last-cycles.sh / find-hash.sh now
read /both (cartesi-machine prints these to stderr); blocks whose own
primary output is on stdout (printf, find-lua-val.sh, ...) keep
/stdout.
Verified by `make README.md TAG=0.5.0` from a clean cache; rendered
prose differs from the previous render only in expected places (cycle
counts, e2ls cosmetics for the new mtime/owner-pinned foo_ext2 recipe,
and the rarely_step splash interleaving noted above).
…unners Rename doc/docgen.lua to doc/replace.lua and extend it with multi-language runner support, docs:begin/end null regions, \$_REPLACE_KEY substitution, and runner-content hashing. Add the per-language runners doc/run-bash.sh and doc/run-lua.sh, and add doc/alerts.lua (pandoc filter for GitHub-style alerts). Update doc/Makefile, doc/README.md.template, and doc/recipes/Makefile accordingly.
Make `make README.md` work again on the 0.20 branch by rebasing the
docs container on a locally-built emulator and adding an opt-in
mechanism that lets snippets be migrated to the 0.20 surface one at
a time instead of all at once.
Container:
- doc/Dockerfile: FROM cartesi/playground:0.5.0 → cartesi/machine-emulator:$TAG.
The released cartesi/machine-emulator:0.20.0 binary cannot drive
tests/dependencies' kernel (built against this branch's unreleased
emulator with UIO/etc.), so the docs image must layer on top of
what `build-emulator-image` produces locally.
- doc/Makefile: rename PLAYGROUND_IMAGE → DOCS_IMAGE; TAG default
0.5.0 → devel (matches root Makefile); build-docs-image now first
invokes `$(MAKE) -C .. build-emulator-image TAG=$(TAG)`.
Per-block enable/disable:
- doc/replace.lua: add `enabled=yes|no` block attribute and read
`-M default-replace=` from doc.meta. Disabled blocks render their
body verbatim (no execution, no region trimming, no cache rules);
cross-block replace= sites for disabled keys render empty;
ensure_defined errors if an enabled block depends on a disabled one.
- doc/{Makefile,recipes/Makefile}: pass `-M default-replace=false` to
every pandoc invocation. With no per-block enabled=, the README
renders source-only against pandoc alone — the container is only
needed for blocks explicitly opted in.
First batch of opted-in snippets:
- doc/README.md.template: enabled=yes on `help`, `linux_sha`,
`rootfs_sha`, `nothing`; image paths /opt/cartesi/share/images →
/usr/share/cartesi-machine/images. Rewrite cmdline_interactive_ls
to feed input via --console-io=input_source:from_file: 0.20's `-i`
defaults console.input_source to from_stdin which calls open_tty()
and fails in a non-TTY container; from_file goes through fopen()
and /sbin/init halts the machine when the user shell exits.
Update the Initialization section: drop --rom-image (ROM is gone), update image paths to /usr/share/cartesi-machine/images/, rename filename: to data_filename: in --flash-drive, and replace the Emulator SDK reference with machine-linux-image and machine-guest-tools. Point readers to the cartesi/machine-emulator-docs image for sample files. Enable the ls, foo_ext2, flash, not_shared_flash, e2ls_not_shared_foo_ext2, shared_flash, and e2ls_shared_foo_ext2 snippets. Update the Persistent flash drives section: drop the ROM mention, rename --dump-pmas to --dump-address-ranges. Add a note explaining that /sbin/init runs commands as the unprivileged user dapp, that flash drives are mounted with root ownership by default, and that user:dapp must be passed to --flash-drive to allow writes (with --user=root as a non-preferred alternative). Add user:dapp to the not_shared_flash and shared_flash examples accordingly.
Update recipes/find-htif-putchar.lua to use the generic read_reg("name")
API introduced in 0.19, replacing the removed per-accessor methods
read_iflags_H/Y(), read_htif_tohost(), and read_mcycle().
Enable config_dump_nothing, cycles_limit_exec, max_mcycle_arg, limit_exec,
and all state_hashes_* blocks. Also add enabled=yes to the inline
[]{replace=...} spans in the surrounding prose.
Enable the persistent_machine_cmd, machine_dirname, persistent_machine, and persistent_stored_hash blocks (plus the cross-block replace= sites and inline spans they reference). Rewrite the prose claim that --store writes the state hash inside the directory and --load verifies it: in 0.20 the store directory contains config.json, per-AR data files, and hash_tree.sht/.phtc, but no separate hash file. --load verifies the archive format version recorded in config.json instead. The pre-store and post-load state hashes still match because the same machine state is restored.
Drop --htif-yield-automatic from the example command (automatic yield is now the default). Rephrase the surrounding prose to reflect the inverted model: the emulator honors automatic yields by default, and --no-htif-yield-automatic disables them (with a note that doing so prevents Rolling Cartesi Machines from generating outputs). Replace the gRPC interface reference with JSON-RPC. Drop the now-redundant mention of --htif-yield-manual from the closing sentence.
Replace --append-rom-bootargs="single=yes" with --user=root, switch flash-drive filename: to data_filename:, swap --replace-flash-drive for --replace-memory-range using labels, and bump lua5.3 to lua5.4. Add mke2fs:false,mount:false to the raw flash drives so init does not try to format and mount them, plus a prose paragraph explaining the default init behavior. Replace gRPC with JSON-RPC in the interfaces sentence, and rewrite the --replace-memory-range explanation now that labels identify drives. Also port the dtc example.
mpernambuco
previously approved these changes
Jun 13, 2026
When iflags.Y is set but the manual yield reason is RX_ACCEPTED, reset_uarch does not revert to the revert root hash, so the final root hash is the ordinary post-reset state. The new create_json_reset_accepted_log generator captures this path and registers its context alongside the existing plain and rejected reset fixtures. This gives the EVM step verifier a fixture that exercises the branch where tohost is decoded but no revert occurs, mirroring the accepted/noop symmetry already present on the send-cmio-response side.
snapshot.ubuntu.com mirrors binary packages before their matching source index is published, so gather-dpkg.sh could silently emit a WARNING instead of a real Source block depending on when regeneration ran. That made the CI check for a byte-identical committed report a lottery. gather-dpkg.sh now distinguishes provenance. If apt-cache madison shows a package is available from a repository, its source must resolve; the script retries and then exits with an error rather than falling through to the WARNING path. The WARNING is kept only for packages with no repository availability, i.e. those installed from a local .deb such as machine-guest-tools. scan-local.sh and build-rootfs-docs-license.sh were updated to let that non-zero exit propagate: build-rootfs-docs-license.sh now captures the scan into a variable so set -e sees the failure instead of the pipeline tail masking it. The Ubuntu snapshot is rolled back from 20260529T000000Z to 20260421T000000Z, the latest date at which every repository source resolves under the hard fail. The ext2 was rebuilt at that snapshot and the report regenerated; two consecutive runs now produce byte-identical output.
Replace the per-entry Lua-pattern dispatch table with plain string option names (trailing "=" marks a value-taking option) and a single dispatch loop. Short value options now use docker-style space form (-v host:guest, -p port, -u name, -e K=V, -w dir, -h host); long options take their value only via --name=value. parse_options gains a positional sub-key (keys[1]) so bare comma items (no colon, not a declared key name) are routed to a named sub-key rather than rejected. This lets --load/--store take a directory, --log-step a filename, --periodic-hashes and --dense-uarch-hashes a period/count, and --store-config/--load-config a filename, all as unadorned first arguments. --log-step argument order changes from count,file to file,count:<n>. --periodic-hashes and --dense-uarch-hashes change the optional second argument from a bare number to start:<mcycle>. --virtio-9p changes from tag:dir positional form to tag:t,host_directory:d. --volume and --port-forward long forms change to key:value sub-options; short -v/-p remain docker-compatible. The four *-json-* option twins (--initial-json-proof, --final-json-proof, --store-json-config, --load-json-config) are removed. Their role is taken by a format:<lua|json> sub-key on --initial-proof, --final-proof, --store-config, and --load-config. When format: is absent the serializer is inferred from the filename extension (.json or .lua), defaulting to Lua. -h is reassigned from a help alias to the hostname short option; a bare -h now prints a hint pointing at --help. bash.lua completion generator is updated to work from plain names and the positional sub-key. Tests, README template, and risc0 Makefile are updated to the new syntax.
The option handlers mutated nine separate config-holder locals (processor, ram, dtb, tlb, virtio, cmio, pmas, uarch, hash_tree) that were later collected into the machine config passed to machine:create. Collapse them into one cmdline_config table built up front, so handlers mutate cmdline_config.<field> directly, and rename the read-back config (get_initial_config) from main_config to initial_config. This frees the bare hash_tree name and makes the build-vs-read-back distinction explicit: cmdline_config is the configuration requested on the command line, initial_config is the machine's actual configuration at instantiation.
Promote doc/recipes/hash-tree.lua to the installed module
src/cartesi/hash-tree.lua and extend it with a frontier-based
incremental keccak Merkle accumulator (frontier, frontier_push_back,
frontier_get_root_hash, frontier_next_proofs). The accumulator matches
the fixed-height outputs tree used by libcmt.
The roll_hash_up_tree function now iterates up to proof.log2_root_size
instead of HASH_TREE_LOG2_ROOT_SIZE, so it works for both whole-machine
proofs and the shallower outputs-tree proofs. Recipe files that pass
whole-machine proofs add an assertion on log2_root_size to make the
assumption explicit.
Add CM_CMIO_LOG2_MAX_OUTPUT_COUNT (63) to cm.h, the matching C++
constant to send-cmio-response.hpp, and expose both to Lua as
cartesi.CMIO_LOG2_MAX_OUTPUT_COUNT.
Wire new --cmio-advance-state sub-options:
output_proof per-accepted-output Merkle proof against the epoch
outputs root, written after all inputs are processed
rejected_output output files for outputs of rejected inputs, which
never enter the outputs tree
last_output_proof
a previous epoch's last output proof that seeds the
frontier so this epoch continues the same genesis-
rooted tree at the running global output index
check_output_hashes_root_hash
cross-check the host frontier root against the root
the guest wrote to the tx buffer on each accepted
input (default on)
Outputs are now buffered until the input's accept/reject verdict
arrives. Accepted outputs enter the frontier and accumulate for the
end-of-epoch proof batch. Rejected outputs go to rejected_output and
never advance the global output index.
BREAKING CHANGE: the default output filename pattern changes from
"input-%i-output-%o.bin" to "output-%o-input-%i.bin", and %o is now
the global output index across all accepted inputs rather than a per-
input counter. Callers that rely on the old pattern or on %o resetting
to zero on each accepted input must update their filenames.
Add util.read_file and util.write_file to cartesi.util and switch all
ad-hoc open/read/write/close sequences in cartesi-machine.lua to them.
Add spec-hash-tree-lua.lua covering frontier proofs, push-back root
tracking, epoch-split equivalence, and verify_slice rejection, and
extend spec-cm-cli.lua with tests for the new sub-options including a
two-epoch continuation with a mid-epoch reject.
The docgen engine (doc/replace.lua) gains a new capability: when a block
is defined with include=, its body (with docs:begin/end markers retained)
is now also stored as the key's source. Consumers can therefore write
replace=K/source/<region> to render a named region straight out of the
included file. The published cache/<K>/both stream is still marker-free;
a source reference records a dependency on it so consumers invalidate when
the included file changes. The spec comment and cross_read guard are
updated to match.
doc/README.md.template is updated to use the new capability and to track
the output-proofs feature already committed:
- The proof_module include block now points at the installed module path
(../../usr/share/lua/5.4/cartesi/hash-tree.lua) so the file is included
once; the four function-excerpt blocks (roll_hash_up_tree, verify_slice,
verify_splice, get_root_hash) switch to replace=proof_module/source/<region>
instead of four separate include= keys.
- The four recipe scripts no longer symlink hash-tree.lua from the recipes
directory, and all four change their require to require("cartesi.hash-tree").
- Rollups-walkthrough output filenames follow the new global output-index
scheme (output-%o-input-%i.bin). A prose note explains that rejected
outputs are saved under a rejected-output-* name for debugging.
- doc/README.md is regenerated to reflect all of the above (it had been
accidentally dropped by the feature commit; this restores it).
--cmio-advance-state output_proof files are now written as Lua chunks by default instead of JSON. Any caller that reads the proof files by extension or assumes .json content must add format:json or rename the pattern explicitly. Add a format:<lua|json> sub-option to --cmio-advance-state that selects the serialization for output_proof and last_output_proof. When output_proof is left at its default pattern, the filename extension tracks format (format:json yields a .json file). An explicit output_proof filename is left as written while format still controls the content. read_proof and save_cmio_output_proofs thread the format value through resolve_format so explicit format always wins over the extension heuristic. Add two spec tests: "output proof format" confirms the default produces a valid Lua chunk (round-tripped via load) and that format:json forces JSON content regardless of a .lua filename; "output hashes root hash accumulates across inputs" guards against a per-accept tree reset in the guest rollup utility by verifying that after two accepted inputs the guest-written root covers both inputs' outputs, not just the second's. This test caught a real bug in guest-tools v0.18.0-test3, fixed in test4. Bump machine-guest-tools to v0.18.0-test4 across tests/dependencies, tests/dependencies.sha256, doc/Dockerfile, doc/recipes/Dockerfile.rootfs-docs, and the rebuilt doc/recipes/rootfs-docs.ext2. The guest-tools fix is required by the accumulation test and by the two-epoch doc walkthrough. The Rolling Calculator Machine walkthrough in doc/README.md.template now spans two epochs against a single kept-alive server. Six inputs are encoded via an encode_input shell function. Epoch 1 processes inputs 1-3 (valid, rejected, valid) with --no-remote-destroy to leave the server and machine alive. Epoch 2 passes --no-remote-create to reuse the live machine and seeds last_output_proof with epoch 1's last proof so the host can rebuild its outputs tree copy and emit proofs at the correct global indices. The decode example now shows the sqrt(2) result from epoch 2. doc/README.md is the regenerated output.
Promote the calc example as the primary worked example under "Rolling Cartesi Machines". It now runs directly from a flash drive across two epochs, carrying the full yield-and-hash walkthrough that was previously attached to puppet. The second epoch run adds an inspect-state query (the golden ratio) and decodes its report, with a note that inspect- state reverts all state changes and cannot emit verifiable outputs. The introductory paragraph about /dev/cmio, HTIF, and CMIO RX/TX buffers is replaced with a short forward reference to "Communication between guest and host" in the guest perspective, keeping unexplained internals out of the command-line chapter. "Rolling Cartesi Machine templates" is reframed as the genesis of a Rollups application. The section now stores the calc machine as a template and replays the same inputs through it, confirming the outputs are identical to the direct run. puppet moves down to "The libcmt library" where its source is shown, and gets its own live run there. calc.sh is rewritten without the advance_state branch: an associative array maps the request type to the emit verb (notice or report), so the single pipeline handles both advance-state and inspect-state. Verification-game server ports are shifted to 8087/8088 so all examples can run in parallel without port conflicts.
run-bash.sh and run-lua.sh create both/stdout/stderr before the block body runs, so a block that produces no output keeps a start-of-run mtime older than the artifacts the body writes. A consumer that orders off the producer's both marker could then build against stale artifacts on an incremental parallel make, needing make clean to recover. Touch the markers after tee flushes so the ordering edge always advances and stays newer than the block's artifacts.
The output proof format case did not redirect output_hashes_root_hash, so the cmio advance wrote its default to a cwd-relative path. That fails on a read-only working directory, as in CI. Disable the file in the two runs that only inspect proofs.
Add an output_hashes_root_hash_proof sub-option to --cmio-advance-state. On each accepted input the guest writes the output hashes root hash to the first word of the cmio tx buffer, so a state value proof of that word ties the root hash, against which the per-output proofs are built, back into the machine state hash. The proof is captured at the accept yield and serialized like output_proof (Lua default, json sub-option). Extract frontier_copy in the hash-tree module for the shallow frontier copy the running-root check needs, replacing the inline table.unpack.
Add --initial-hash=<filename> and --final-hash=<filename> forms that write the raw 32-byte state hash to a file, matching the raw form used for the output hashes root hash. The bare flags still print the hash. This lets a rolling run publish the machine state hash an epoch settles on, which a verifier needs to check output proofs against. Also tidy the output_hashes_root_hash_proof help text to say "tx buffer", as elsewhere.
Add an Output proofs section to the Lua interface that generates an epoch's per-output proofs and the tx-buffer-word proof from a rolling calculator run (run-rolling-calculator-output-proofs.lua). Add an Output verification example to the Blockchain perspective (verify-output-proof.lua) that checks an output against those two proofs from the settled machine state hash alone, with no machine. Wire the rolling calculator CLI walkthrough to save the settled state hash with --final-hash, and regenerate README.md.
Break the combined Merkle tree operations section in two. "Slicing and splicing" keeps the word-leaf state-tree mechanics and precedes its applications, Template instantiation and Result extraction, now promoted to siblings. A new "The outputs tree" section explains the keccak256-leaf outputs tree and its frontier operations (frontier_node, frontier_push_back, frontier_get_root_hash, frontier, frontier_next_proofs), and precedes Output verification. Repoint the three cross-references that each meant one half or the other, and capture the outputs-tree height and leaf size from cm.h. Also make the verification-game example deterministic: the players are told apart only by connection order, so wait on an established connection to the server before launching the dishonest player, in both vg_run and vg_run_reset.
Add a figure to the outputs tree section showing the three regions frontier_node reads left to right: the frontier supplying a complete left subtree (AB), this epoch's new outputs as the active region (C-F), and pristine padding (GH). The frontier and pristine subtrees enter whole at aligned boundaries, drawn collapsed, so only the active outputs are individual leaves, mirroring frontier_node and frontier_next_proofs. The figure renders from a committed Graphviz source, images/outputs-tree.dot, into images/outputs-tree.svg. A pattern rule drives dot, and the svg is an order-only prerequisite of README.md so a render refreshes it only when the source changes, and never forces a re-render when just the image bytes do. Add graphviz to the docs image so dot is available in the pinned container. Regenerate README.md.
Add the physical-memory attributes of each address range to its address_range_description, so callers can tell memory from devices and inspect access permissions. The new fields are is_memory, is_device, is_readable, is_writeable, is_executable, is_read_idempotent, is_write_idempotent, and driver_id, each read from the matching address_range accessor. get_address_ranges still returns every range, devices included, since callers need the whole occupied address space to check for overlap. The fields flow through to_json, ju_get_opt_field, and the JSON-RPC AddressRangeDescription schema. Use the new is_memory flag in --dump-address-ranges to write a file only for memory ranges. Device ranges are not memory-backed and hash as pristine, so dumping their bytes produced meaningless files. Update the cm-cli test to expect a file per memory range and none for devices.
Add two tested SVG figures to the documentation. In "Hash-view of state", a state hash-tree figure draws a real machine's state as a Merkle tree over the address space, generated by images/state-tree.lua, which instantiates a machine and reads its memory ranges. In "The outputs tree", a frontier figure shows the frontier holding completed left subtrees while the active region and pristine padding fill the rest, from images/outputs-tree.dot. Both render through the images/ diagram rules as order-only prerequisites of README.md, so a render refreshes them without forcing a rebuild. state-tree is a Lua program that emits SVG directly; outputs-tree pins its node positions and renders with neato -n.
apt-get source --print-uris emits whichever location currently serves each file. While a version is still in the pool that is the live mirror with a SHA256 digest, and once it has been superseded it is the pinned snapshot host with a SHA512 digest. The committed report therefore drifted whenever Ubuntu published a security update that pushed an installed package out of the live pool, even with the snapshot date and the rootfs unchanged, and the CI sync check failed. The two forms cannot be reconciled as text because the digest algorithms differ and SHA512 cannot be derived from SHA256. Normalize every captured source URI to the durable snapshot host and drop the digest field, which is not required to satisfy the source distribution obligation. The report now depends only on the committed ext2 and the snapshot pin, so it stays byte stable until one of those changes.
…rfaces The microarchitecture had a dedicated ECALL (function code 3) that let uarch interpreter code mark a physical page dirty. This was the wrong abstraction layer. The uarch should not know about dirty-page tracking, and exposing the call through i_state_access bloated the interface for every accessor that had nothing to do with dirty pages. Pull the responsibility up to the machine layer. Introduce i_accept_dirty_pages as an opt-in capability interface, mirroring i_accept_counters, and guard the mark call in write_ram_uint64 with is_an_i_accept_dirty_pages_v. Add machine::mark_write_tlb_dirty_page so the write-TLB eviction path and the overwrite path both mark the outgoing page through a single spot. Remove the host-address overload of machine::mark_dirty_page so all callers pass a physical address. On the uarch side, delete the ECALL handler, its constants, and all plumbing that threaded do_mark_dirty_page through every accessor implementation. Function code 3 is left as an intentional gap in the ECALL table. Replace the ecall-mark-page-dirty assembly test with ecall-removed-mark-page-dirty, which issues fn=3 and asserts it traps, keeping the gap behavior under test.
Address reviewer confusion in the output proofs and output hashes tree sections without changing any behavior. Define what an output index is and how an output is verified from a proof that its hash is the leaf at that index. Note that the report command takes the same input format as notice but has no index to print, because reports are not verifiable. Drop the vague "shared accessor", "running accumulator", and "matching reader" labels in favor of the plain function names. Spell out the frontier_node argument placeholders and define is_proof where the frontier constructor uses it. Make explicit that the outputs and their proofs live outside the machine, in the Cartesi Node, and that the machine state commits to them through the output hashes root hash alone. Add that proofs for a past epoch are produced when that epoch is finalized and are checked against the hash settled then, not against a later one. Rename "outputs tree" to "output hashes tree" and "rolling calculator" to "Rolling Cartesi Machine calculator" throughout, and unify the root name as "output hashes root hash", removing the stray "output-hashes Merkle root" from the guest pseudocode.
The option only writes a file for memory ranges. Device ranges hold no state and are always pristine, so they are skipped, which makes "memory ranges" the accurate name. This reverts the rename made earlier in this unreleased cycle and restores the 0.20.0 spelling. Rename the option, its handler variable, and the dump function, and align the help text, the spec-cm-cli coverage, and the doc prose, fixing the prose that claimed all mapped spans in the address space were dumped.
The static verify_step, verify_step_uarch, verify_reset_uarch, and verify_send_cmio_response now take their root-hash inputs as const_machine_hash_view instead of const machine_hash &, matching the revert-hash parameter that already used the view. A view is a non-owning borrow that suits a consumed parameter, while owning hashes are still returned by value or const reference. The uarch and send-cmio replay context constructors take the view as well, which lets the verify bodies pass the parameter straight through with no materialization copy. Comparisons of an owning machine_hash against a view use std::ranges::equal. Also rename the freestanding std::vector guard in machine-hash.hpp from the ZKARCHITECTURE/MICROARCHITECTURE pair to a single NO_STD_VECTOR, defined by the uarch and risc0 builds, so the include site names the actual constraint instead of inferring it from the architecture.
mpernambuco
previously approved these changes
Jun 26, 2026
mpernambuco
left a comment
mpernambuco
left a comment
Collaborator
There was a problem hiding this comment.
LGTM Nice call with i_accept_dirty_pages
| // Overwrite the processor shadow state with the provided data | ||
| static_assert(AR_SHADOW_STATE_LENGTH == sizeof(m_s->shadow)); | ||
| // NOLINTNEXTLINE(cppcoreguidelines-pro-type-reinterpret-cast) | ||
| memcpy(reinterpret_cast<unsigned char *>(&m_s->shadow), data, sizeof(m_s->shadow)); |
Collaborator
There was a problem hiding this comment.
since this overwrites the shadow tlb without going through write_??verified_tlb, could a pending write-tlb dirty page be lost here? should it mark_write_tlb_dirty_pages() before the memcpy?
Contributor
Author
There was a problem hiding this comment.
You are right, if you call this function when the machine already has some hot entries. I'll fix it.
…stdin htif-console.lua now passes input_source = "from_buffer" in the runtime config and calls machine:write_console_input to supply the test string, removing the dependency on host stdin. Because run() breaks early with BREAK_REASON_CONSOLE_INPUT when the buffer drains, the test loops until iflags_H is set. run-lua-tests.sh drops the echo pipe that was feeding stdin to every test script, since only htif-console.lua ever consumed it.
diegonehab
force-pushed
the
feature/revert-root-hash
branch
from
9b3880f to
b1988c5
Compare
machine::write_memory has a special case that replaces the entire shadow state and reinitializes the hot TLB. Pages written by the guest through the write TLB are dirtied in host memory but only tracked by the write TLB until the next hash update flushes them into the dirty-page tree. Resetting the hot TLB and overwriting the shadow TLB discarded that pending information, so any such page lost its dirty mark. A later incremental hash then failed to recompute it and produced a root hash that did not reflect actual memory. Flush the write TLB dirty pages into the dirty-page tree before replacing the shadow, matching what update_hash_tree and verify_hash_tree already do. Add a regression test that runs a small program whose store dirties a page through the write TLB, overwrites the shadow state, and checks that the root hash still matches the hash computed directly from memory. The test fails before this change and passes after.
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
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 #388 (the issue stays open for the Dave integration items). The companion PR regenerates the Solidity side: cartesi/machine-solidity-step#98
Problem
When the guest rejects an advance-state input, the canonical machine state goes back to
the pre-input state, but dispute verifiers could not prove that transition. The
pre-input root hash was poked into the machine by the host through a separate,
unverified
write_revert_root_hash()call, and no verifier ever substituted it for themachine root hash after a rejection.
Solution
The first commit implements the write side.
send_cmio_response,log_send_cmio_response, andverify_send_cmio_responsetake the revert root hash astheir first argument, threaded as
const_machine_hash_viewthrough every interfacelayer (machine, i_machine, local and jsonrpc machines, the JSON-RPC wire protocol, the
C API, and the Lua bindings) and as a
bytes32alias in the Solidity-translatablecore. The core commits the hash into the
revert_root_hashshadow leaf as a singlefull-leaf logged write right after the
iflags.Yprecondition check, so the valuebecomes part of the proof. The record/replay rx-buffer write logic is hoisted into
label-parameterized helpers shared with the new accessor.
The second commit implements the read side.
uarch_reset_stateresets the uarch asbefore, then reads
iflags.Y, conditionally readshtif.tohost, decodes thedev/cmd/reason fields, and on a rejected manual yield calls the new
revert_state()accessor, which reads the revert leaf (one logged access carrying the value) and
switches the canonical root hash atomically. The replay accessor replaces its context
root hash, so
verify_reset_uarchis untouched. The record accessor reports theresulting hash through a caller-owned context, so
log_reset_uarchneeds no branch.For the ZK path,
replay_step_state_access::finish()applies the same rule, readingthe revert leaf from the shadow registers page that every step log already contains,
and
log_steprecords the substituted hash in the log header. The risc0 guest inheritsthe behavior with no source changes. Unknown yield reasons (GIO domains, accepted,
exception) cause no substitution and no error. The physical machine is never reverted,
a rejected
log_reset_uarchstill resets the uarch.cm.h gains the HTIF tohost/fromhost field shifts and masks, exposed through the Lua
module so the machine-solidity-step constants generator can query them.
Tests
step round trips against the revert hash, tampered revert leaf values, and the
accepted-reason control case.
machine-solidity-step Foundry tests.
cross-build, and the risc0 cpp guest cross-build.