Repository navigation
Run the PRT recipes on Dave's contracts, with durable Lua storage - #411
Draft
diegonehab wants to merge 109 commits into
Draft
diegonehab wants to merge 109 commits into
diegonehab wants to merge 109 commits into
Conversation
diegonehab
changed the title
Separate LRU hooks, page addresses, borrowed flags, and payload indices from cached pages and hashes within the existing single mapping. Load validation and map reconstruction now read only compact metadata, and conditional eviction exchanges payload indices instead of copying data. Use entry_metadata and entry_payload to name the two parts of each entry. Align the payload array and every payload to 4 KiB machine pages. Check capacity arithmetic, exact LRU node boundaries, bounded traversal, backlinks, active-entry membership, and unique in-range payload indices before using persisted metadata. Retain Boost intrusive lists and lazy payload access. Bump the stored-machine archive version to 9 and reject the previous PHTC layout tag. Cover malformed metadata, overflowing capacities, file-size mismatches, eviction without payload writes, and payload alignment across metadata page boundaries. Validated with backing-store, hash-tree, machine API, and C API suites, plus toolchain formatting and lint checks. A local APFS benchmark with a full 4096-entry cache (25 samples) reduced median fresh-clone loads from 125.64 to 1.50 ms with SHARING_NONE and 124.77 to 1.92 ms with SHARING_ALL. Warm loads measured 0.49 and 0.64 ms respectively.
diegonehab
force-pushed
the
feature/prt
branch
from
October 25, 2026 16:21
aa53ffb to
77880e1
Compare
There was no API to discard persisted hash caches and rebuild them from machine memory. Add clear_hash_tree across the machine APIs and CLI, resetting cached hashes and marking pages dirty for lazy rebuilding. Clearing preserves machine state, mappings and statistics. The CLI clears once by default, with an option to clear on subsequent loads too.
The Linux image and guest tools rootfs URLs were spelled out in tests/Makefile. Compose both once in the lock file from its tags.
The docs' host mode links the installed command names cartesi-machine and cartesi-machine-stored-hash to their scripts in the source tree so the recipes can run from the build tree.
encode_abi and decode_abi handle ABI tuples without a function selector, as used by event data and return values. Values follow the same conventions as encode_calldata, and decoded integers retain all 256 bits.
Move the test filesystem helpers into the installed native module cartesi.filesystem. Implement file operations and temporary-file ownership in os-filesystem, expose them through cm-filesystem.h and cm-filesystem.cpp, and keep the Lua binding thin. Use the existing C API argument checks, function-scope try blocks, error codes, and thread-local diagnostics so Lua raises errors only after the C++ exception has been handled. Package libcartesi_filesystem and libluacartesi_filesystem, including cartesi/filesystem.so, following the JSON-RPC library targets and dependency layout. Install cm-filesystem.h; no filesystem.lua wrapper is needed. Preserve binary reads, overwriting writes, replacement renames, and explicit sync semantics. write_durable_file writes and syncs a temporary file before renaming it; the caller syncs its directory. Reads do not lock backing files that may already belong to a running machine. write_file reports close errors. Temporary-file owners remove their path on close or collection unless renamed. Their Lua file view keeps the owner alive and updates it when closed, avoiding double closes. Expose the existing file, path, close, and rename interface. Directory listings use JSON arrays of Base64 names and the existing Lua Base64Array schema to preserve filename bytes. write_file takes data before its filename, matching util.write_file, and callers are updated accordingly. Cover C API validation and ownership, filename conversion, temporary-file lifetimes, binary operations, and exception lifetime across Lua pcall.
Move every caller of util.read_file and util.write_file to the same functions in cartesi.filesystem, and remove them from cartesi.util. The argument order is unchanged.
A forest can now keep its trees in a directory, one JSON file per tree named by its hash. A fixed-point tree file holds only its base values and a mixed tree file its two child hashes, so loading rebuilds each tree and checks its hash and height, failing on any mismatch. frontier_forest_store flushes pending values, stores the trees not yet in the directory, and writes the frontier to a separate file, so snapshots of a growing forest share their trees. frontier_forest_load reopens a forest from that file. Queries and expansions load a stored tree in place of a raw hash when they reach it, and an expansion of a stored forest also stores its new trees. Forests without a directory behave as before. Forest levels and mixed tree children now hold raw hashes directly, as fixed-point base values already did, instead of wrapping each one in a single-value fixed-point tree. A value is loaded and expanded in place the same way wherever it sits, so a store reaches every expansion. A stored or loaded forest cannot be a value of another forest, because some of its trees may exist only as files in its own directory, where the other forest would never find them. Trees with equal hashes can describe the same subtree differently and know different parts of it. A store that finds a file holding another representation merges into the tree what that file knows below the hash, opening the tree's opaque values with the file's subtrees, and replaces the file only after the files below it are durable. Each tree and frontier file is written to a uniquely named temporary file in its own directory, synced through the open file, and renamed into place. A store syncs its directory once before writing and syncing the frontier file, which therefore commits the store: a crash leaves the previous frontier intact. An expansion's files are synced before its top file, which makes it reachable, is written. A file left by an interrupted store may lack its children's files, so the forest records the trees a completed sync confirmed and those it loaded, and a store rewrites the missing files of every other tree. frontier_store and frontier_load do the same for a plain frontier, and the CLI uses them for its epoch frontier files.
The CLI constructors used make_ while other constructors use new_. Rename the revert, runner and computation builder constructors and their callers to follow that convention.
util.read_file and util.write_file are gone from cartesi.util. The recipes and the README call the same functions in cartesi.filesystem, with the same argument order.
The docs image supplies the cartesi-machine command, the default kernel and rootfs images, and GNU tools. With HOST=yes and the environment from make env, doc/Makefile provides them from the local emulator build and doc/build instead, so the recipe tests run without Docker and on filesystems with reflinks. doc/Makefile also adds its Lua paths to LUA_PATH_5_4, which make env sets and Lua 5.4 prefers over LUA_PATH. Rendering the README with HOST=yes puts GNU tools first on PATH, prints timestamps in UTC, and uses a hash of the emulator build, the lock file, and the rootfs in place of the docs image ID. The README takes the default images directory from pandoc metadata instead of naming /usr/share/cartesi-machine/images, and the proof_module include reaches cartesi.hash-tree through a link to wherever the environment's Lua finds it. A change of environment regenerates template.d. The docs image takes the kernel URL from dependencies.lock as a build argument. Server waits use netstat -ant, which also lists listening sockets on macOS. replace.lua creates directories through pandoc.system instead of the shell. The shell tests remove the exact names they create from their temporary directories and then rmdir them, so a leftover file fails the test. The fixture script removes the old template with remove_stored, and the clean rule removes the replace cache by its literal path.
The PRT and VG constructors are named new_, as in the CLI. What the machine caches hold are entries, so checkpoint is free for the state a sealed epoch leaves for the next one.
A wait for block D now settles block D - 1 and returns, so a request made then is answered at D. wait_until(D) has the same meaning. The referee's validators already reject answers received at a deadline, so the extra block only delayed the next request. The PRT referee used to send the timeout-win and elimination requests at the start of each turn, and honest players scheduled their answers for the deadlines those requests carried. The referee now sends each request only once its window opens: the timeout win when the on-turn request expires, and the elimination when the timeout win or the uarch proof expires. Players answer both at once, so their handlers become plain queries and no longer schedule responses. The events are renamed win_match_by_timeout and eliminate_match and no longer carry a deadline. No recipe waits with a lower bound anymore, so wait_at_least is gone from the transport and wait_at_most(FOREVER) suffices. The deadline tests check that each request is made exactly when its window opens, and how many are made in each scenario. Tests that pin absolute blocks follow, and tests of scheduled-response mechanics use test-local events.
A player's handler returns the payload of its answer, "nothing" when it has no answer to give, or "done" when it leaves the game. The transport sends both as the reply's value, in place of the skip and done flags, and "done" ends the client loop. Eliminating a match and asking for a missing output have nothing to answer. The quitter leaves at the first event after its claim, and the phase closer leaves once it closes the phase.
A player can continue the output history of previous epochs and, once its epoch is sealed, store a checkpoint (the final machine, its outputs frontier, and epoch.json) from which the next epoch's players start. Output proofs are computed on demand from the sealed epoch instead of at the seal. Given an epoch directory, the player runs on stored machines instead of forked servers. Its epoch pair snapshots by cloning the machine's directory, as the CLI's --revert-mode=stored does, and its machine cache keeps entries as stored machines. Inputs, outputs, claim forests, and the cache record live in the directory, and state.json, written last at each input boundary, at the seal, and for each uarch claim, is the only commit point. Reopening an existing directory brings the epoch machine back to the recorded boundary, removes whatever state.json does not reach, and restores an open epoch's builder or a sealed epoch's mcycle and uarch claims, so a player can be killed at any point and resume. remove_epoch_directory removes only the names the layout creates. A uarch bundle is now one whole mcycle, so a uarch claim stores one hash per mcycle instead of one per 2^16 uarch transitions. The tests cover crash recovery at every recorded cut point (on filesystems with reflinks), reopening sealed epochs and their disputes, and comparison with fork mode.
Dockerfile.prt builds an image with Anvil and Dave v3.0.0-alpha.6's contracts, patched for the recipe geometry. The demo deploys them, plays two epochs of the rolling calculator, and settles their disputes on chain. The chain runs in the container, and deployment, mining, narration, and every player run on the host, whose filesystem has reflinks. Each player runs in its own process with a bridge of its own. The bridge reads Dave's published tournament events, fetching the log history incrementally and paged to the provider's limits, and drives the player only through its event handlers. It waits for the configured confirmations, derives claim bindings from the chain, and attempts due jobs in order of expiry. Transactions are signed with cast, tracked until confirmed, replaced with bumped fees when stuck, and recorded in a pruned, durable journal per player. Every player starts each epoch from the checkpoint of the previous one, and the honest player runs in stored mode. PRT_TEST_RESTART=yes restarts it mid-epoch and mid-dispute, and PRT_TEST_REORG=yes reorganizes the chain during epoch 1's dispute. The bridge, transaction, and proof tests run in the PRT image. The proofs are checked on a chain of their own.
prt-lua-bridge.md explains how to run the on-chain PRT demo, and how its pieces fit: one process per player, the image and deployment, epochs and their checkpoints, how the bridge observes the dispute and turns contract events into calls on the player, proofs, transactions, the demo harness, validation, and the current limits.
The README described forests only in memory. Document storing and loading them, loading trees on demand, and why a forest with its own storage directory cannot be used as a value in another forest.
A new section after the verification game explains how PRT settles a dispute among many claims in a number of rounds logarithmic in their count, and runs prt.lua's model of Dave's contracts on the same epoch the verification game settled. It shows how the referee settles a missed turn and how a player reveals a bisection, quoting both from prt.lua. The hash-view section links to it. README.md is rendered from the template as it stands after this and the preceding changes.
The unreleased changelog omitted the new APIs and recipes. Record cache clearing, filesystem operations, forest persistence, ABI conversion and PRT support, along with the cache layout and archive version changes.
A computation hash is the root of the hash tree over periodically spaced state hashes, and a claim is a computation hash with its final state hash and, at the referee, its clock. prt.lua, its tests, and the README no longer speak of claim trees or computation trees, and call the descent of a match a bisection rather than a walk. build_uarch_claim becomes build_uarch_cycle_computation_hash, since it builds only the computation hash, and recover_epoch_machine becomes revert_interrupted_input. The comments above prt.lua's functions are shorter, and the story calls inside excerpted functions are hidden from the README, as in vg.lua. README.md is updated to match.
new_forked_player runs on forked servers and keeps its inputs and outputs in memory. new_stored_player runs on stored machines in its epoch directory, and its metatable overrides the methods that store inputs and outputs and commit the epoch state, so the event handlers no longer test for an epoch directory. Every player ignores events it already applied. A stored player created with a checkpoint directory stores the next epoch's checkpoint at the epoch seal, so epoch_sealed no longer takes one. new_machine_pair and new_machine_cache become new_forked_machine_pair and new_forked_machine_cache, and the checkpoint functions become store_first_epoch_checkpoint and load_epoch_checkpoint. The proof tests now run stored players. The README describes the two modes and why its demonstration runs in forked mode.
The uarch reset proof replaces the entire uarch state hash tree node with the pristine uarch state hash, which assumes the node holds only the shadow uarch state and the uarch RAM. Config validation only checked addressability and overlap, so a flash drive or nvram with an explicit start in the gap between them was accepted. Once it held non-zero data, reset_uarch and collect_uarch_cycle_root_hashes kept it, while the verifier wipes it, so the honest uarch reset could not be proven. machine_address_ranges::check() now rejects ranges that intersect the gap between the shadow uarch state and the uarch RAM, or the gap between the uarch RAM and the end of the node. Each check applies only when its gap is not empty. Ranges that hit the shadow uarch state or the uarch RAM are rejected by the existing overlap check.
…tree as misses The page hash-tree cache is persisted separately from the memory ranges it describes. When a range and the cache were persisted differently (a SHARING_CONFIG load of a machine whose shared flags differ between its ranges and its hash tree, or replace_memory_range on a machine with a shared hash tree), the stored cache could keep an entry for a page whose stored dirty-page tree said clean while its contents had changed. Later loads trusted that entry, so get_proof, get_node_hash and collect_uarch_cycle_root_hashes returned wrong hashes while the root hash and verify_hash_tree looked correct. Wherever a cached entry is used without first comparing it with memory (get_page_proof, get_dense_node_hash and update_words), it is now lent as a hit only when its root hash equals the page hash in the range's dense hash tree. Otherwise it is treated as a miss and refreshed from memory, which is what any caller already does when the entry has been evicted. This makes the sharing-based eviction at load and the eviction of clean pages on replace_memory_range unnecessary, so both are removed, together with page_hash_tree_cache::evict_entries_if.
frontier_next_proofs accepted more new leaves than the tree could hold and attempted to build proofs for them. Check the remaining capacity with frontier_padding_fits before allocating or constructing the proofs.
frontier_node obscured a simple lookup among an active range and its two outside values. Rename it get_or_outside and put the values, base and index first, updating the proof construction callers without changing behavior.
… trees taller than 64 Node indices in a tree of height 64 can set the sign bit, so signed comparisons selected the wrong sibling hashes. Compare indices as unsigned and reject taller trees, whose proof addresses cannot fit in 64 bits.
Lua longjmp from a C++ catch leaves the caught exception alive after pcall returns. Use block-level catches in the existing Lua binding functions, copy the exception message into a 1024-byte stack buffer with snprintf, and raise the Lua error only after the catch has finished. Messages longer than 1023 bytes are truncated and null-terminated. The diagnostic copy requires no userdata or C++ heap allocation and does not touch the C API's thread-local error storage. Actual C API calls keep reporting errors through cm_get_last_error_message. Preserve the existing error prefixes and the unknown-register-exception fallback. Create Lua cleanup owners before allocating C++ buffers and objects, and populate managed strings and JSON values after installing their owners. Remove the redundant catch around cm_new, which already handles exceptions. Add a native Lua regression covering repeated conversion, schema, register, and impossible-buffer-size failures, followed by successful conversions. Check that no caught C++ exception remains, existing C API diagnostics are preserved, and messages truncate correctly at the buffer boundary. Link the test to the Lua and C libraries together to exercise the same error storage. Register it with misc and parallel test targets. Validation: make; build-tests-misc; native exception and filesystem tests; JSON, hash, filesystem, and console specs; local machine-bind suite; toolchain formatting and clang-tidy on changed binding sources.
JSON keys were passed through terminated strings, truncating embedded NUL bytes. Input parsing could also accept only the prefix before a raw NUL. Preserve explicit string lengths when converting keys and reject raw NUL bytes before parsing Lua JSON or server requests.
ABI decoding added offsets and rounded lengths before checking bounds. Large values could wrap and pass those checks. Compare each offset, length and array head size with the remaining input before arithmetic, and derive tuple ends from the data actually decoded.
ArrayIndex conversion could overflow when subtracting one from a Lua index or adding one to a JSON index. Check the signed limits and reject unsigned JSON values that cannot become a Lua index before converting them.
Without a schema, sparse Lua arrays became JSON arrays containing invented null entries. Mixed keys could also reach object conversion, where numeric keys were coerced to strings during iteration. Require consecutive indices starting at 1 without a schema and accept only string keys in objects.
An empty Lua table always became a JSON array, even under an object schema. Let the schema select an empty object, and treat empty schema dictionaries and type definitions as objects while preserving empty tuple definitions.
Machine configuration conversion lacked schemas for containers, so empty configuration objects were serialized as arrays. Define the configuration container schemas and use them in the machine bindings and CLI configuration import and export.
Stored epoch state did not declare the type of uarch_claims, leaving an empty list ambiguous during JSON conversion. Add an array schema for that field so epochs with no uarch claims can be stored explicitly as an empty array.
The game transport decoded responses without their schema and encoded them again before delivery. That lost container distinctions and applied unnecessary conversions to payloads the transport did not inspect. Keep each payload as JSON encoded with its event schema, then decode it with that schema at delivery.
An empty Lua table has no keys to distinguish a JSON object from an array, but conversion silently chose an array. Require an explicit container schema for empty tables, including nested ones. Complete the access log and event argument schemas and parse schema definitions according to their own container rules.
JSON string conversion treated any matching schema field as an enum entry, so ordinary strings could become field schemas or other values. Translate a matching entry only when its schema value is an integer.
NaN and infinity were silently serialized as JSON null, changing the value and potentially removing an entry when decoded into Lua. Reject numbers that are not finite before assigning them to JSON.
Lua does not remove string keys from weak tables, so the signature cache retained every parsed signature. Use weak values and cache the parsed signature itself, with its selector and canonical name, so it can be collected once callers release it.
ABI array encoding relied on # and ipairs, which can ignore string keys or stop at gaps and silently omit values. Validate every key and require consecutive indices starting at 1 in a shared helper. Use the checked count for fixed sizes, encoded lengths and dynamic offsets.
The ABI parser consumed memory, calldata or storage at the start of a parameter name as a location keyword, changing the name. Require an identifier boundary after those keywords so names such as memorySize remain intact.
Frontier reconstruction trusted a supplied proof without checking that it authenticated a leaf in the tree. Validate its shape, hashes and address before reconstruction. Bound the scan for the lowest complete level so a proof of the last leaf in a tree of height 64 cannot loop forever when its count wraps to zero.
Frontier operations accepted invalid subtree heights, allowing bad indexing or partial mutation, and constructors accepted arbitrary cartesi members as hash functions. Check subtree heights before use and resolve hash names only from the supported Keccak and SHA functions.
Independent PRT claim forests shared files named only by hash. Different tree representations could collide, and a new store could replace files already used by a committed claim. Give each claim its own tree directory, update loading and cleanup, and bump the epoch state version to reject the old layout.
Temporary files were opened before FD_CLOEXEC was set, leaving a window in which another thread could spawn a child that inherited the descriptor. Use mkostemp with O_CLOEXEC on POSIX so the descriptor is protected from creation.
ABI decoding silently discarded nonzero upper bits of addresses and nonzero padding in fixed byte values. Check those bytes before returning the decoded value so malformed encodings are rejected.
The ABI hex decoder passed each pair to tonumber, which accepts signs and therefore treated pairs such as +1 as valid hex bytes. Require two hexadecimal digits before converting each pair.
Lua callers obtained a temporary pathname by creating and removing a file, then reused the name later. Another process could claim it in between. Create private temporary directories atomically and place new paths inside them, with scoped cleanup for tests and the existing owned file helpers for file data.
temp_pathname returned an unreserved name after deleting its temporary file, so callers could not safely create an object there. Remove the API from C++, C and Lua now that its callers use private temporary directories or owned temporary files.
The first padding pass could skip empty frontier slots until its shift reached 64, where the computed subtree size became zero. It could then merge occupied slots without consuming the count. Stop this scan at the count width and let the second pass install the remaining bits and propagate carries.
Oversized ABI integer strings could wrap during bint conversion and pass the later type range check as a different value. Bound the significant digit count for decimal, hexadecimal and binary strings before conversion, ignoring the sign, prefix and leading zeros. Keep the existing parser and exact type range checks.
diegonehab
force-pushed
the
feature/prt
branch
from
November 5, 2026 16:13
77880e1 to
495260e
Compare
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.
This PR runs the documentation's PRT players against Dave's real contracts on a local chain. It adds the Lua storage APIs a player needs to survive crashes, and two hash-tree cache improvements.
Emulator and Lua library
dependencies.lock. The kernel and rootfs download URLs are composed once in the lock file instead of being spelled out intests/Makefile.cartesi.evmu.encode_abianddecode_abihandle selectorless ABI tuples, as used by event data and return values.cartesi.filesystem. The file helpers the tests used become an installed module. A small C core adds what Lua cannot do itself (checking existence, creating and listing directories, cloning and truncating files, temporary files that clean up after themselves, and syncing files and directories withF_FULLFSYNCon macOS).cartesi.util.read_fileandwrite_fileare removed. Every caller now usescartesi.filesystem, with the same argument order.cartesi.hash-tree.frontier_forest_storeandfrontier_forest_loadkeep a frontier forest in a directory, one file per tree named by its hash. Snapshots of a growing forest share their trees. Writes go through synced temporary files, and the frontier file is the commit point, so a crash leaves the previous store intact.frontier_storeandfrontier_loaddo the same for a plain frontier, and the CLI uses them.new_.Documentation recipes
cartesi.filesystem.HOST=yes, the recipe tests run and the README renders against the local emulator build instead of the docs image. This is what lets stored machines use the host's reflinks."nothing", or"done".state.jsonas its only commit point, and reopens after being killed at any point. A uarch bundle is now one mcycle.doc/recipes/prt-lua-bridge.mddescribes the design and its current limits.Testing
Outside
doc/Recipes (host mode, after
eval $(make env))On-chain recipe
PRT_TEST_RESTART=yeskills and relaunches the honest player mid-epoch and mid-dispute, andPRT_TEST_REORG=yesreorganizes the chain during a dispute.