Lua interface

caution

This entire chapter is for advanced users only, since typical users of the Cartesi platform will likely never need to programmatically control a Cartesi Machine.

The Lua interface to Cartesi Machines is available from the cartesi Lua module. In a properly setup installation (such as what is available in the playground Docker image), the module can be loaded with the require function

-- Load the Cartesi module
local cartesi = require"cartesi"

The most important field in the module is the cartesi.machine “class”, used to instantiate new local Cartesi Machines.

A Cartesi Machine instance is defined by its organization and the contents of its state. The organization specifies the amount of RAM and the layout of a number of flash drives (between 0 and 8) and rollup memory ranges. To support Cartesi Machine's transparency, flash drives are mapped into the machine's 64-bit physical memory address space. The layout defines each flash drive's start and length in the address space. The contents of the state include the values stored in ROM, RAM, and in all flash drives and rollup memory ranges, in addition to the values of all processor registers and device-specific state.

Cartesi Machines can be instantiated directly from a configuration structure, or loaded from a persistent state stored as a directory on disk.

Instantiation by configuration

machine_config ::= {
  rom ::= rom_config,
  ram ::= ram_config,
  flash_drive ::= {
    [1] ::= memory_range_config, -- flash drive 0
    [2] ::= memory_range_config, -- flash drive 1
    ...
    [n] ::= memory_range_config  -- flash drive n <= 7
  },
  processor ::= processor_config,
  clint ::= clint_config,
  htif ::= htif_config,
  rollup ::= rollup_config,
}

rom_config ::= {
    bootargs ::= string,
    image_filename ::= string
}

ram_config ::= {
    length ::= number,
    image_filename ::= string
}

htif_config ::= {
    fromhost ::= number,
    tohost ::= number,
    console_putchar ::= boolean,
    yield_manual ::= boolean,
    yield_automatic ::= boolean
}

clint_config ::= {
    mtimecmp ::= number,
}

rollup_config ::= {
  rx_buffer := memory_range_config,
  tx_buffer := memory_range_config,
  input_metadata := memory_range_config,
  voucher_hashes := memory_range_config,
  notice_hashes := memory_range_config
}

processor_config ::= {
  x = {
    [1]  ::= number, -- register x1
    [2]  ::= number, -- register x2
    ...
    [31] ::= number, -- register x31
  },
  pc ::= number,
  mvendorid ::= number,
  marchid ::= number,
  mimpid ::= number,
  mcycle ::= number,
  minstret ::= number,
  mstatus ::= number,
  mtvec ::= number,
  mscratch ::= number,
  mepc ::= number,
  mcause ::= number,
  mtval ::= number,
  misa ::= number,
  mie ::= number,
  mip ::= number,
  medeleg ::= number,
  mideleg ::= number,
  mcounteren ::= number,
  stvec ::= number,
  sscratch ::= number,
  sepc ::= number,
  scause ::= number,
  stval ::= number,
  satp ::= number,
  scounteren ::= number,
  ilrsc ::= number,
  iflags ::= number
},

memory_range_config ::= {
  start ::= number,
  length ::= number,
  image_filename ::= string,
  shared ::= boolean
}

The rom entry in machine_config is a table with two fields. Field bootargs gives a string of at most 2KiB that will be copied into the end (the last 2KiB) of ROM. Field image_filename gives the file name of an image that will be loaded into the beginning of ROM. This is where the ROM image rom.bin generated by the Emulator SDK is typically loaded. This is also where the machine starts execution, i.e., where the processor's program counter initially points to. This ROM image generates the devicetree that describes the hardware to Linux, passes the bootargs string as the kernel command-line parameters, then cedes control to the RAM image.

The ram entry in machine_config also has two fields. Field length gives the amount of RAM in bytes (RAM always starts at offset 0x80000000). This length should be a multiple of 4Ki, the length of a RISC-V memory page. Field image_filename gives the filename of an image that will be loaded at the start of RAM. This is where the RAM image linux.bin generated by the Emulator SDK (which contains the Berkeley Boot Loader linked with the Linux kernel) is typically loaded.

The flash_drive entry in machine_config is a list of memory_range_config entries, each of which contain a flash drive configuration. Each memory_range_config contains four fields. Fields start and length give the start and length of the flash drive in the machine's address space. Once again, the length must be a multiple of 4Ki, the length of a memory page. Field image_filename gives the file name of an image that will be mapped to this region. This is different from the ROM and RAM image files, which are simply copied into the Cartesi Machine memory, which has been allocated from the host memory. Flash drives use memory mapping because their image files can be very large. Mapping them instead of copying them saves host memory, as well as the time it would take to load the files from disk to host memory. Since flash drive image files are mapped, their sizes on disk must exactly match the length of the flash drive they are backing. Field shared contains a Boolean value that specifies whether changes to the flash drive that happen inside the target reflect in the image file that resides in the host file-system as well. If set to true, the image file will be modified accordingly. This is useful when a flash drive will hold the result of a computation. If set to false (the default), target modifications to the flash drive are not propagated to the image file that resides in the host filesystem. I.e., even though the flash drives may be read/write from the target perspective, the image file in the host is left unmodified.

The htif entry in machine_config has four fields, two of which are used only in rare occasions. The most commonly used field is the Boolean console_getchar. When set to true (the default is false), it instructs the emulator to monitor terminal input in the host and make it available to the target via the HTIF device. This is used in interactive sessions during prototyping, and should never be used when verifiability is needed. The yield_automatic and yield_manual Booleans instruct the emulator to honor automatic yield and manual yield commands received by the HTIF Yield device, respectively. Target applications use these commands to notify the host that the application has just produced output data for collection, or is ready to accept new input data for processing. There are two differences between the two types of yield command. First, an automatic yield sets the X flag in the iflags control and status register (CSR), whereas the manual yield sets the Y flag. Second, the X flag is automatically reset when the machine is resumed after an automatic yield. In contrast, Y flag must be manually reset after a manual yield, or the machine will not advance at all when resumed. Manual and automatic yields are the mechanism that control Cartesi Rollups input and output with Rolling Cartesi Machines. The fields tohost and fromhost in htif allow for the overriding of the default initial values of these CSRs (control and status registers).

The rollup entry in machine_config has five fields, each holding a memory_range_config entry. The Cartesi Machine support for Cartesi Rollups involves a variety of memory ranges. The first two, rx_buffer and tx_buffer are used to send data in and out of the machine, respectively. For example, the input payload to an advance-state request and the query payload to an inspect-state request are written to the rx_buffer memory range. Conversely, vouchers, notices, reports, and exceptions are written to the tx_buffer memory range. The input metadata for advance-state requests are written to the input_metadata memory range. The voucher_hashes and notice_hashes memory ranges are arrays on which the hash of each voucher or notice emitted during processing of an advance-state are appended, respectively. For more details on how exactly these memory ranges are used, please read the architecture section under the target perspective.

The remaining entries in the machine_config are used only in rare occasions. The devices and processor have a variety of control and status registers (CSRs), in addition to processor's general-purpose registers. Most of these are defined in volumes 1 and 2 of the ISA specification. The Cartesi-specific additions are described under the architecture section under the target perspective.

The clint entry has a single field, mtimecmp, which allows for the overriding of the default initial value of this CSR. Similarly, the fields in the processor entry allow for the overriding of the default initial value of all general-purpose registers and CSRs in the processor.

Configuration from command-line

The cartesi-machine command-line utility can be used to output machine configurations for Cartesi Machines that can be used directly by the Lua cartesi.machine constructor. Recall from an earlier example that the cartesi-machine command

cartesi-machine \
    --rom-image="/opt/cartesi/share/images/rom.bin" \
    --ram-length=64Mi \
    --ram-image="/opt/cartesi/share/images/linux.bin" \
    --flash-drive="label:root,filename:/opt/cartesi/share/images/rootfs.ext2" \
    --max-mcycle=0 \
    --store-config \
    -- "ls /bin"

builds a Cartesi Machine that, when run, lists the contents of the /bin/ directory before gracefully halting. The image files rom.bin, linux.bin, and rootfs.ext2 are generated by the Emulator SDK, and are available in the playground Docker image in directory /opt/cartesi/share/images/. The command-line option --max-mcycle=0 instructs the utility to stop execution at cycle 0 (mcycle is a CSR that starts at 0 and is advanced at every instruction cycle), i.e., before the machine even starts running. The key command-line option is --store-config, which causes the emulator to print the corresponding configuration to the standard output. To store directly to a file, use the --store-config=<filename> instead, in which case, the --load-config=<filename> command-line option can be used to load the stored config.

return {
  processor = {
    x = {
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
      0x0, -- default
    },
    iflags = 0x18, -- default
    ilrsc = 0xffffffffffffffff, -- default
    marchid = 0xc, -- default
    mcause = 0x0, -- default
    mcounteren = 0x0, -- default
    mcycle = 0x0, -- default
    medeleg = 0x0, -- default
    mepc = 0x0, -- default
    mideleg = 0x0, -- default
    mie = 0x0, -- default
    mimpid = 0x1, -- default
    minstret = 0x0, -- default
    mip = 0x0, -- default
    misa = 0x8000000000141101, -- default
    mscratch = 0x0, -- default
    mstatus = 0xa00000000, -- default
    mtval = 0x0, -- default
    mtvec = 0x0, -- default
    mvendorid = 0x6361727465736920, -- default
    pc = 0x1000, -- default
    satp = 0x0, -- default
    scause = 0x0, -- default
    scounteren = 0x0, -- default
    sepc = 0x0, -- default
    sscratch = 0x0, -- default
    stval = 0x0, -- default
    stvec = 0x0, -- default
  },
  ram = {
    length = 0x4000000,
    image_filename = "/opt/cartesi/share/images/linux.bin",
  },
  rom = {
    image_filename = "/opt/cartesi/share/images/rom.bin",
    bootargs = "console=hvc0 rootfstype=ext2 root=/dev/mtdblock0 rw quiet swiotlb=noforce mtdparts=flash.0:-(root) -- ls /bin",
  },
  htif = {
    tohost = 0x0, -- default
    fromhost = 0x0, -- default
    console_getchar = false, -- default
    yield_automatic = false, -- default
    yield_manual = false, -- default
  },
  clint = {
    mtimecmp = 0x0, -- default
  },
  flash_drive = {
    {
      start = 0x8000000000000000,
      length = 0x5000000,
      image_filename = "/opt/cartesi/share/images/rootfs.ext2",
      shared = false, -- default
    },
  },
}

Cycles: 0

The resulting configuration includes a number of default values, conveniently marked as such by the cartesi-machine utility. It can be edited down to its essential, and stored into a file, for example as a Lua module:

config/ls-bin.lua

return {
  processor = {
    mvendorid = 0x6361727465736920,
    mimpid = 0x1,
    marchid = 0xc,
  },
  ram = {
    length = 0x4000000,
    image_filename = "/opt/cartesi/share/images/linux.bin",
  },
  rom = {
    image_filename = "/opt/cartesi/share/images/rom.bin",
    bootargs = "console=hvc0 rootfstype=ext2 root=/dev/mtdblock0 rw quiet swiotlb=noforce mtdparts=flash.0:-(root) -- ls /bin",
  },
  flash_drive = {
    {
      start = 0x8000000000000000,
      length = 0x5000000,
      image_filename = "/opt/cartesi/share/images/rootfs.ext2",
    },
  },
}

The only required values in the processor configuration are the mvendorid, mimpid, marchid CSRs. These are used to ensure the emulator version matches the version the configuration was generated for. If the emulator detects a mismatch, instantiation fails. During prototyping, these fields can be set to -1 to instantiate a machine with the values it expects. In production code, they should be hard-coded to match the release of the emulator in use.

Note how the utility automatically sets the ROM bootargs to include several kernel parameters. The ones seen in the example have the following meaning:

• console=hsvc0 sets the device to be used as console;
• rootfstype=ext2 sets the root filesystem type;
• root=/dev/mtdblock0 sets the device where the root filesystem can be found;
• rw instructs the kernel to mount the root filesystem read-write;
• quiet stops the kernel from printing initialization messages;
• swiotlb=noforce prevents the kernel from reserving memory for DMA bounce buffers.

The two remaining parameters deserve some elaboration. The mtdparts=flash.0:-(root) section is a kernel command-line parameter that provides the kernel with partitioning information for the flash drives. The format for the parameter is documented in the source-code for the kernel module responsible for parsing it. Here, (root) gives the partition label, and flash.0 refers to the first flash drive. The /bin/ls /bin command appears in the ROM bootargs after the -- separator. The Linux kernel passes anything that appears after the separator, verbatim, to /sbin/init. The Cartesi-provided /sbin/init then uses this information to run the desired command.

Recall the command-line utility can also run Cartesi Machines with additional drives. In that case, the resulting configuration automatically includes an entry for them in the mtdparts kernel command-line argument. Repeating another earlier example

mkdir foo
echo Hello world > foo/bar.txt
tar \
    --sort=name \
    --mtime="2022-01-01" \
    --owner=1000 \
    --group=1000 \
    --numeric-owner \
    -cf foo.tar \
    --directory=foo .
genext2fs \
    -f \
    -b 1024 \
    -a foo.tar \
    foo.ext2
cartesi-machine \
    --flash-drive=label:"foo,filename:foo.ext2" \
    --max-mcycle=0 \
    --store-config \
    -- "cat /mnt/foo/bar.txt"

produces the corresponding machine configuration. This can be edited down to its essential, and stored into a file, for example as a Lua module:

config/cat-foo-bar.lua

return {
  processor = {
    mvendorid = 0x6361727465736920,
    mimpid = 0x1,
    marchid = 0xc,
  },
  ram = {
    image_filename = "/opt/cartesi/share/images/linux.bin",
    length = 0x4000000,
  },
  rom = {
    bootargs = "console=hvc0 rootfstype=ext2 root=/dev/mtdblock0 rw quiet swiotlb=noforce mtdparts=flash.0:-(root);flash.1:-(foo) -- cat /mnt/foo/bar.txt",
    image_filename = "/opt/cartesi/share/images/rom.bin",
  },
  flash_drive = {
    {
      image_filename = "/opt/cartesi/share/images/rootfs.ext2",
      start = 0x8000000000000000,
      length = 0x5000000,
    },
    {
      image_filename = "foo.ext2",
      start = 0x9000000000000000,
      length = 0x100000,
    },
  },
}

Note the entry in mtdparts that causes flash.1, the flash drive containing the foo.ext2 file-system, to receive the label foo. When the Cartesi-provided /sbin/init detects a valid file-system in the flash drive, it automatically uses the label to mount it as /mnt/foo. It is there that the command cat /mnt/foo/bar.txt finds the file to dump to the console.

Additional sample configurations

Here are the (simplified) configurations for the other examples from the documentation of the cartesi-machine command-line utility.

A Cartesi Machine that has nothing to do:

cartesi-machine \
    --max-mcycle=0 \
    --store-config

config/nothing-to-do.lua

return {
  processor = {
    mvendorid = 0x6361727465736920, -- cartesi.machine.MVENDORID
    mimpid = 0x1, -- cartesi.machine.MIMPID
    marchid = 0xc, -- cartesi.machine.MARCHID
  },
  ram = {
    image_filename = "/opt/cartesi/share/images/linux.bin",
    length = 0x4000000,
  },
  rom = {
    image_filename = "/opt/cartesi/share/images/rom.bin",
    bootargs = "console=hvc0 rootfstype=ext2 root=/dev/mtdblock0 rw quiet swiotlb=noforce mtdparts=flash.0:-(root)",
  },
  flash_drive = {
    {
      image_filename = "/opt/cartesi/share/images/rootfs.ext2",
      start = 0x8000000000000000,
      length = 0x5000000,
    },
  },
}

A Cartesi Machine that periodically reports its progress using the HTIF Yield device:

cartesi-machine \
    --htif-yield-automatic \
    --max-mcycle=0 \
    --store-config \
    -- $'for i in $(seq 0 5 1000); do yield automatic progress $i; done'

config/progress.lua

return {
  processor = {
    mvendorid = 0x6361727465736920,
    mimpid = 0x1,
    marchid = 0xc,
  },
  ram = {
    length = 0x4000000,
    image_filename = "/opt/cartesi/share/images/linux.bin",
  },
  rom = {
    image_filename = "/opt/cartesi/share/images/rom.bin",
    bootargs = "console=hvc0 rootfstype=ext2 root=/dev/mtdblock0 rw quiet swiotlb=noforce mtdparts=flash.0:-(root) -- for i in $(seq 0 5 1000); do yield automatic progress $i; done",
  },
  htif = {
    yield_automatic = true,
  },
  flash_drive = {
    {
      start = 0x8000000000000000,
      length = 0x5000000,
      image_filename = "/opt/cartesi/share/images/rootfs.ext2",
      shared = false, -- default
    },
  },
}

A Cartesi Machine that computes the value of a generic mathematical expression:

cartesi-machine \
    --flash-drive="label:input,length:1<<12,filename:input.raw" \
    --flash-drive="label:output,length:1<<12,filename:output.raw,shared" \
    --max-mcycle=0 \
    --store-config \
    -- $'dd status=none if=$(flashdrive input) | lua -e \'print((string.unpack("z", io.read("a"))))\' | bc | dd status=none of=$(flashdrive output)'

config/calculator.lua

return {
  processor = {
    mvendorid = 0x6361727465736920, -- cartesi.machine.MVENDORID
    mimpid = 0x1, -- cartesi.machine.MIMPID
    marchid = 0xc, -- cartesi.machine.MARCHID
  },
  ram = {
    image_filename = "/opt/cartesi/share/images/linux.bin",
    length = 0x4000000,
  },
  rom = {
    image_filename = "/opt/cartesi/share/images/rom.bin",
    bootargs = "console=hvc0 rootfstype=ext2 root=/dev/mtdblock0 rw quiet swiotlb=noforce mtdparts=flash.0:-(root);flash.1:-(input);flash.2:-(output) -- dd status=none if=$(flashdrive input) | lua -e 'print((string.unpack(\"z\", io.read(\"a\"))))' | bc | dd status=none of=$(flashdrive output)",
  },
  flash_drive = {
    {
      image_filename = "/opt/cartesi/share/images/rootfs.ext2",
      start = 0x8000000000000000,
      length = 0x5000000,
    },
    {
      start = 0x9000000000000000,
      length = 0x1000,
    },
    {
      start = 0xa000000000000000,
      length = 0x1000,
    },
  },
}

Loading and running machines

The Lua interface to cartesi.machine can be used to instantiate Cartesi Machine based on any desired configuration. In particular, the configurations produced by the cartesi-machine utility, such as the examples above. This is, after all, the interface used internally by the cartesi-machine utility.

For example, the script

run-config.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Instantiate machine from configuration
local machine = cartesi.machine(require(arg[1]))

-- Run machine until it halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    machine:run(math.maxinteger)
end

loads a machine configuration from the Lua module specified in the command-line (using require(arg[1])). It then creates an instance by calling the cartesi.machine(<machine_config>) constructor, which it stores in the machine local variable.

The machine:run(<max_mcycle>) method of the Cartesi Machine instance runs the corresponding machine until the CSR mcycle reaches at most <max_mcycle>. The value of <max_mcycle> used in the script is a very large integer, providing the machine with enough cycles to run until it halts or yields manual. Note that the machine:run() method can return precociously for a variety of reasons (see below), so it should always be called inside a loop. The iflags CSR contains a bit H that is set to true whenever the machine is halted, and a bit Y that is set to true whenever the machine has yielded manual. The machine:read_iflags_H() and machine:read_iflags_Y() methods return the value of these bits, respectively, and the loop breaks if any of them is set.

For example, to run the configuration stored in ./config/cat-foo-bar.lua (assuming ./foo.ext2 is available) simply run

lua5.3 run-config.lua config.cat-foo-bar

(The function call require(argv[1]) translates the argument "config.cat-foo-bar" to "config/cat-foo-bar.lua" and loads that file.)

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI
        \ /   MACHINE
         '

Hello world!

The machine:get_initial_config() method returns the configuration that was used to create a Cartesi Machine instance.

Instantiation from persistent state

At any point in their execution, Cartesi Machines can be stored to disk. A stored machine can later be loaded to continue its execution from where it left off.

note

If the machine initialization involved large image files or a considerable amount of RAM, this operation may consume significant disk space. It will also take the time required by the copying of image files into the directory, and by the computation of the state hash.

To store a machine at its current state, use the machine:store(<directory>) method of the Cartesi Machine instance.

store-cat-foo-bar.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Instantiate machine from configuration
local machine = cartesi.machine(require"config.cat-foo-bar")

-- Store persistent state to directory
machine:store("cat-foo-bar")

To prevent persistent Cartesi Machines from being inadvertently overwritten, the function call fails when the directory already exists.

After the execution of the script above, the directory ./cat-foo-bar/ contains all the information needed to instantiate the same machine, including copies of all necessary image files. There are no external dependencies. In fact, running the following script

load-cat-foo-bar.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Instantiate machine from persistent state directory
local machine = cartesi.machine("cat-foo-bar")

-- Run machine until it halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    machine:run(math.maxinteger)
end

has exactly the same effect as the example above, where the machine was instantiated from the configuration and directly run until it halted.

As before, the configuration that was used to instantiate a Cartesi Machine can be obtained from the machine instance with the method machine:get_initial_config(). Note that this is not the configuration that was used to instantiate the machine for the first time, but rather the configuration used to instantiate a copy of the machine that was stored. More specifically, any image filenames point to modified copies that reside inside the storage directory. Likewise, the RAM image and the values of all registers will reflect the values as they were when stored.

Limiting execution

The machine:run(<max_mcycle>) method of a Cartesi Machine instance always returns when the machine halts. From the outside, however, it is impossible to predict how many cycles the emulator will need until the machine finally halts. One of the uses for the <max_mcycle> argument in production code is to ensure the call returns at a desired frequency, rather than potentially blocking the caller indefinitely.

The following script illustrates the process

run-config-in-chunks.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Instantiate machine from configuration
local machine = cartesi.machine(require(arg[1]))

local CHUNK = 1000000 -- 1 million cycles
-- Loop until machine halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    -- Execute at most CHUNK cycles
    machine:run(machine:read_mcycle() + CHUNK)
    -- Potentially perform other tasks
end
-- Machine is now halted or yielded manual

The loop conditional checks if the machine has yet to halt. If so, it runs the machine for at most an additional CHUNK cycles. The machine:read_mcycle() method returns the current value of the mcycle CSR. The current value of mcycle is used to set the new limit to mcycle+CHUNK. After the call to machine:run() returns, the application is free to perform other tasks.

Progress feedback

When the computation running inside a Cartesi Machine is intensive, it may be desirable to inform users of the progress, so they can plan accordingly. On its own, the current value of mcycle does not give any information concerning how much of the computation still remains. What is needed is the value of mcycle when the machine halts. This is, unfortunately, difficult to estimate from the outside. The target application is in a much better position to estimate its own progress. However, it needs a mechanism to communicate its progress back to the program controlling the emulator.

The command-line utility /opt/cartesi/bin/yield can be used for this purpose. Internally, the tool uses an ioctl system-call on the Cartesi-specific /dev/yield device. The protocols followed by the /opt/cartesi/bin/yield utility to interact with the /dev/yield driver, and by the driver itself to communicate with the HTIF Yield device are explained in detail under the target perspective. The focus here is on its effect on the host program controlling the emulator.

A Cartesi Machine can be configured to accept HTIF yield automatic commands by means of the htif.yield_automatic Boolean field in the machine configuration. When set to true, a yield automatic command will cause the emulator to precociously return from a call to machine:run(<max_mcycle>). Otherwise, yield automatic commands are ignored so that execution of the machine:run(<max_mcycle>) continues unimpeded until the machine halts or mcycle hits <max_mcycle>.

The following example illustrates how Lua scripts can receive progress information throughout a computation performed inside a Cartesi Machine:

run-config-in-chunks-with-progress.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Writes formatted text to stderr
local function stderr(fmt, ...)
    io.stderr:write(string.format(fmt, ...))
end

-- Instantiate machine from configuration
local machine = cartesi.machine(require(arg[1]))

local CHUNK = 1000000 -- 1 million cycles
local max_mcycle = CHUNK
-- Loop until machine halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    -- Execute at most CHUNK cycles
    machine:run(max_mcycle)
    -- Check if machine yielded automatic
    if machine:read_iflags_X() then
        -- Check if yield was due to progress report
        local reason = machine:read_htif_tohost_data() >> 32
        if reason == cartesi.machine.HTIF_YIELD_REASON_PROGRESS then
            local permil = machine:read_htif_tohost_data()
            -- Show progress feedback
            stderr("Progress: %6.2f\r", permil/10)
        end
    end
    if machine:read_mcycle() == max_mcycle then
        max_mcycle = max_mcycle + CHUNK
        -- Potentially perform other tasks
    end
end
-- Machine is now halted or yielded
stderr("\nCycles: %u\n", machine:read_mcycle())

The loop repeats until the machine halts or yields manual. As before, the computation is performed in chunks. At each iteration, the script tries to advance the computation until the end of the next chunk. When the call to machine:run() returns, a set bit X in CSR iflags means the reason for returning was the Yield automatic command. That command can be called for different reasons. The command and the associated data can be found in the HTIF tohost CSR. The cartesi.HTIF_YIELD_REASON_PROGRESS corresponds to a progress report, and the data contains the progress in parts per mil. The loop is aborted if the bits H or Y in iflags is set, which signals the machine is halted or yielded manual. Otherwise, the execution continues with the remaining of the current chunk, or a new chunk. In case of a new chunk, the script could perform any desired “per-chunk” tasks.

For example, running the script with the command-line

lua5.3 run-config-in-chunks-with-progress.lua config.progress

produces the output (shown at 44% completion) below

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI
        \ /   MACHINE
         '

Progress:  44.00

This is similar to the cartesi-machine command-line

cartesi-machine \
    --htif-yield-automatic \
    -- $'for i in $(seq 0 5 1000); do yield automatic progress $i; done'

which uses an equivalent mechanism for progress reports.

Cartesi Machine templates

Recall that, to instantiate a Cartesi Machine template, we first replace its flash drive place-holders with their actual content. After that, we can run the resulting machine. To save the simple calculator template into directory "calculator-template", we ran:

cartesi-machine \
    --flash-drive="label:input,length:1<<12" \
    --flash-drive="label:output,length:1<<12" \
    --max-mcycle=0 \
    --final-hash \
    --store="calculator-template" \
    -- $'dd status=none if=$(flashdrive input) | lua -e \'print((string.unpack("z", io.read("a"))))\' | bc | dd status=none of=$(flashdrive output)'

To instantiate and run the template with the cartesi-machine command line utility, we used the command-line option --replace-flash-drive:

cartesi-machine \
    --load="calculator-template" \
    --replace-flash-drive="start:0x9000000000000000,length:1<<12,filename:input.raw" \
    --replace-flash-drive="start:0xA000000000000000,length:1<<12,filename:output.raw,shared"

Internally, the utility uses the machine:replace_memory_range(<memory_range_config>) method of the Cartesi Machine instance to replace an existing flash drive. The start and length fields in the memory_range_config parameter must match those of an existing memory range in the Cartesi Machine instance. The following code snippet shows how to instantiate a Cartesi Machine template using the Lua API:

run-calculator-with-new-drives.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Instantiate machine from template
local machine = cartesi.machine("calculator-template")

-- Get initial config from template
local config = machine:get_initial_config()

-- Replace input flash drive
local input = config.flash_drive[2]
input.image_filename = assert(arg[1], "missing input image filename")
machine:replace_memory_range(input)

-- Replace output flash drive
local output = config.flash_drive[3]
output.image_filename = assert(arg[2], "missing output image filename")
output.shared = true
machine:replace_memory_range(output)

-- Run machine until it halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    machine:run(math.maxinteger)
end

The code starts by loading the calculator template from directory "calculator-template". It then queries the machine for its initial configuration. There, it finds the memory_range_config corresponding to the input flash drive (the second drive). After updating the image_filename field to point to the filename passed as the first argument to the script, it uses the machine:replace_memory_range(<memory_range_config>) method to update the machine with the new flash drive. Then, it obtains the memory_range_config corresponding to the output flash drive (the third drive). It updates the image_filename field to point to the filename passed as the second argument to the script, and sets the shared field to true so results can be read from the file after the machine is executed. The output flash drive is then updated with a second call to the machine:replace_memory_range(<memory_range_config>) method. Finally, the script runs the machine until it halts or yields manual.

To see the example running,

rm -f output.raw
truncate -s 4K output.raw
echo "6*2^1024 + 3*2^512" > input.raw
truncate -s 4K input.raw
lua5.3 run-calculator-with-new-drives.lua input.raw output.raw
lua5.3 -e 'print((string.unpack("z", io.read("a"))))' < output.raw

The result is, as expected,

10786158809173895446375831144734148401707861873653839436405804869463\
96054833005778796250863934445216126720683279228360145952738612886499\
73495708458383684478649003115037698421037988831222501494715481595948\
96901677837132352593468675094844090688678579236903861342030923488978\
36036892526733668721977278692363075584

State hashes

State hashes are Merkle tree root hashes of the entire 64-bit address space of the Cartesi Machine, where the leaves are aligned 64-bit words. Since Cartesi Machines are transparent, the contents of this address space encompass the entire machine state, including all the processor's CSRs and general-purpose registers, the contents of RAM and ROM, of all flash drives, and of all other devices or memory ranges connected to the board. State hashes therefore work as cryptographic signatures of the machine, and implicitly of the computation they are about to execute.

The following script shows how state hashes can be obtained from a Cartesi Machine instance:

run-config-with-hashes.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Writes formatted text to stderr
local function stderr(fmt, ...)
    io.stderr:write(string.format(fmt, ...))
end

-- Converts hash from binary to hexadecimal string
local function hexhash(hash)
    return (string.gsub(hash, ".", function(c)
        return string.format("%02x", string.byte(c))
    end))
end

-- Instantiate machine from configuration
local machine = cartesi.machine(require(arg[1]))

-- Print the initial hash
stderr("%u: %s\n", machine:read_mcycle(), hexhash(machine:get_root_hash()))

-- Run machine until it halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    machine:run(math.maxinteger)
end

-- Print machine status
if machine:read_iflags_H() then
    stderr("\nHalted\n")
else
    stderr("\nYielded manual\n")
end
-- Print cycle count
stderr("Cycles: %u\n", machine:read_mcycle())

-- Print the final hash
stderr("%u: %s\n", machine:read_mcycle(), hexhash(machine:get_root_hash()))

State hashes can be obtained with the machine:get_root_hash() method, which returns the corresponding Keccak-256 hash as a 32-byte binary string. State hashes are produced from an internal Merkle tree data structure that is maintained in a lazy fashion. The performance penalty imposed on the emulator, were it required to keep the Merkle tree up-to-date, would be unacceptable (by several orders of magnitude). If no state hashes are needed, the Merkle tree is not updated and negligible cost is incurred. However, depending on the extent to which the state was modified since the Merkle tree was last updated, the cost of implicitly updating it prior to returning the state hash can be substantial.

note

In previous releases, the machine:update_merkle_tree() method was public and had to be called explicitly. This method is now private and is called implicitly by public methods that need an up-to-date Merkle tree (e.g. machine:get_root_hash(), machine:get_proof(<address>, <log2_size>) etc). It goes over all changes to the state that are still unaccounted for since the tree was last updated, bringing the tree in sync with the current state.

Before running the machine, the script obtains the initial state hash, converts it to hexadecimal, and prints the result. The script then runs the machine until it halts or yields manual. Once the machine is halted, the script obtains and prints the final state hash.

Initial state hashes can be used to ensure the machine instantiated by the script indeed matches the machine created by the cartesi-machine utility, and final state hashes to verify that computations also agree. The output on the left was generated by the command

lua5.3 run-config-with-hashes.lua config.nothing-to-do

The output on the right was produced by running the same Cartesi Machine via the cartesi-machine utility.

cartesi-machine \
    --initial-hash \
    --final-hash

0: 1392f3d52dcaa5b070fa1e91b377e8d31fecf242a5ab4e3a84cd191d5699e456

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI
        \ /   MACHINE
         '

Nothing to do.

Halted
Cycles: 62388529
62388529: faa438df6e6dd027aab3710223852303964fe20f93af43c919120bc7ff3d27ba

0: 1392f3d52dcaa5b070fa1e91b377e8d31fecf242a5ab4e3a84cd191d5699e456

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI
        \ /   MACHINE
         '

Nothing to do.

Halted
Cycles: 62388529
62388529: faa438df6e6dd027aab3710223852303964fe20f93af43c919120bc7ff3d27ba

Note that the initial state hashes and the final state hashes match, as expected.

External state access

The entire Cartesi Machine state is transparently exposed to the controlling program. A variety of methods can be used to query a machine instance for any value in its state.

The method machine:read_memory(<start>, <length>) returns a string with <length> bytes from any memory range in the machine, starting at the physical-memory address <start>. Memory ranges include the ROM, the RAM, any of the flash drives, and any of the rollup memory ranges. The selected data must reside entirely inside a single memory range (i.e., it cannot straddle a memory range boundary).

There are also methods for reading individual registers. Most registers are part of the RISC-V ISA, and its privileged architecture. Cartesi-specific registers are described under the target perspective sections that cover the processor and board of the Cartesi Machine architecture.

The method machine:read_x(<index>), where <index> is in 0…31 returns the value of one of the 32 general-purpose processor registers.

The value of CSRs can be obtained by name, with the machine:read_csr("<csr>") method. Here, <csr> is any of the names pc mvendorid marchid mimpid mcycle minstret mstatus mtvec mscratch mepc mcause mtval misa mie mip medeleg mideleg mcounteren stvec sscratch sepc scause stval satp scounteren ilrsc iflags clint_mtimecmp htif_tohost htif_fromhost htif_ihalt htif_iconsole htif_iyield. The value of <csr> can also be obtained directly from method machine:read_<csr>(). (For example, the machine:read_mcycle() method has already been encountered several times.)

As already described, convenience methods machine:read_iflags_H() and machine:read_iflags_Y() are provided to directly read the most useful bits in the iflags CSR.

Conversely, any value in the state of a Cartesi Machine instance can be modified by the controlling program. In contrast to reading the state, writing to the state requires extreme care. First, for obvious reasons, external modifications to the state break the reproducibility of Cartesi Machines. Second, careless state modifications can easily panic the Linux kernel or crash any programs running under it. Nevertheless, there are a few scenarios where these modifications are safe and useful.

The machine:write_memory(<start>, <data>) method writes the string <data> into any memory range in the state, starting at the physical-memory address <start>. Memory ranges include the ROM, the RAM, any of the flash drives, and any of the rollup memory ranges. Note that the bytes in the string <data> must fit entirely inside a single memory range (i.e., it cannot straddle a memory range boundary).

The typical use for machine:write_memory() is when a new input to a Rolling Cartesi Machine has become available from Cartesi Rollups. Another use is when an input flash drive was instantiated without an image file, and is thus filled with zeros in the initial machine state. Before running the machine for the first time, it is safe to replace the contents of the flash drive with the desired input. (Note, however, that if a flash drive does have an associated shared image file, the machine:write_memory() method will modify the associated image file on disk as well as its mapping in the Cartesi Machine state.) Another use case is in low-level debugging sessions. For example, the gdb remote serial protocol requires the ability to externally modify the state.

General purpose registers can be written to with the method machine:write_register(<index>, <value>), where <index> is in 0…31.

The value of any CSR can be changed with the machine:write_csr("<csr>", <value>) method. (CSRs accept 64-bit integers as value.) Again, <csr> is any of the names pc mvendorid marchid mimpid mcycle minstret mstatus mtvec mscratch mepc mcause mtval misa mie mip medeleg mideleg mcounteren stvec sscratch sepc scause stval satp scounteren ilrsc iflags clint_mtimecmp htif_tohost htif_fromhost htif_ihalt htif_iconsole htif_iyield. The value of <csr> can also be changed directly with method machine:write_<csr>(<value>).

As an example, consider the following script, which uses the bc program running inside a Cartesi Machine to evaluate an arithmetic expression:

run-calculator.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Instantiate machine from configuration
local calculator_config = require"config.calculator"
local machine = cartesi.machine(calculator_config)

-- Write expression to input drive
local input_drive = calculator_config.flash_drive[2]
machine:write_memory(input_drive.start, table.concat(arg, " ") .. "\n")

-- Run machine until it halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    machine:run(math.maxinteger)
end

local output_drive = calculator_config.flash_drive[3]
print((string.unpack("z", machine:read_memory(output_drive.start, output_drive.length))))

The script loads the config template from from its Lua module ./config/calculator.lua and instantiates a Cartesi Machine from it. The pristine input and output flash drives are described in the configuration at config.flash_drive[2] and config.flash_drive[3], respectively. (Entry config.flash_drive[1] describes the flash drive with the root file-system for the embedded Linux distribution.) The script concatenates its command-line arguments, line-terminates them, and writes them at the start of the raw input flash drive. The script then runs the machine until it halts or yields manual. Finally, it reads the output drive contents and extracts the first null-terminated string from it, and prints the results.

Running the script with the command-line

lua5.3 run-calculator.lua 6*2^1024 + 3*2^512

produces the output

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI
        \ /   MACHINE
         '

10786158809173895446375831144734148401707861873653839436405804869463\
96054833005778796250863934445216126720683279228360145952738612886499\
73495708458383684478649003115037698421037988831222501494715481595948\
96901677837132352593468675094844090688678579236903861342030923488978\
36036892526733668721977278692363075584

The number is indeed the value of the expression 6×2¹⁰²⁴+3×2⁵¹².

Finally, external state modifications are useful in the setup of artificial, unexpected conditions in regression tests.

State value proofs

Value proofs concerning the state of the Cartesi Machine can be obtained from any instance using the method machine:get_proof(<address>, <log2_size>).

State value proofs are proofs that a given node in the Merkle tree of the Cartesi Machine state has a given hash. Each Merkle tree node covers a contiguous range of the machine's 64-bit address space. The size of a range is always a power of 2 (given by the <log2_size> parameter). Since the leaves have size 8 (for 64-bits), the valid values for <log2_size> are 3…64. The range corresponding to each node starts at an <address> that is a multiple of its size.

Recall that the state Merkle is maintained in a lazy fashion. Therefore, just like with the machine:get_root_hash() method, the Merkle tree will be implicitly updated to account for state changes. This means the time it takes to obtain a proof depends on the extent to which the state has been modified since the Merkle tree was last updated.

The machine:get_proof() method returns a table with the following structure:

proof ::= {
  address ::= number,
  log2_size ::= number,
  root_hash ::= string,
  target_hash ::= string,
  sibling_hashes ::= {
    [1] ::= string,
    [2] ::= string,
    ...
    [64-log2_size] ::= string
  }
}

Fields address and log2_size come directly from the arguments passed to the method. Field root_hash has the same value as a call to machine:get_root_hash() would return, i.e., the value of the state hash. The target_hash field contains the hash of the node corresponding to address and log2_size.

To understand the contents of the sibling_hashes array, consider a path from the root, down the Merkle tree, all the way to the target hash. When this path is traversed, a number of nodes are visited. The sibling_hashes array contains the hashes of the siblings of all nodes visited (excluding the root, which has no sibling).

Using the data in a proof, it is possible to verify the claim that a Merkle tree with a given root hash contains a target node with a given hash at the position given by its address and size. The function slice_assert(<root_hash>, <proof>) exported by the cartesi.proof module performs exactly this task.

cartesi/proof.lua (excerpt)

local cartesi = require"cartesi"

local _M = {}

function _M.roll_hash_up_tree(proof, target_hash)
    local hash = target_hash
    for log2_size = proof.log2_size, 63 do
        local bit = (proof.address & (1 << log2_size)) ~= 0
        local first, second
        if bit then
            first, second = proof.sibling_hashes[64-log2_size], hash
        else
            first, second = hash, proof.sibling_hashes[64-log2_size]
        end
        hash = cartesi.keccak(first, second)
    end
    return hash
end

function _M.slice_assert(root_hash, proof)
    assert(root_hash == proof.root_hash, "proof root_hash mismatch")
    assert(_M.roll_hash_up_tree(proof, proof.target_hash) == root_hash,
        "node not in tree")
end

return _M

The bulk of work happens in the roll_hash_up_tree(<proof>, <target_hash>) function. In the first iteration of the loop, the function uses the bit with value 2^log2_size in address to determine if the sibling of the target node comes before or after it in the address space of the Cartesi Machine. It then computes the hash of the concatenation of the target node's hash and its sibling's hash (in the correct order). To do so, it uses the cartesi.keccak(<first-string>, <second-string>) function. The result must be the hash of the parent node to the target and its sibling. The loop then goes up the sibling_hashes array, and obtains the sibling of this parent node. This is again concatenated with the just-calculated hash of the parent node (in the correct order) to obtain what must be the hash of the grandparent node. This process is repeated until the hash of what must be the root node is found and returned. Function splice_assert(<root_hash>, <proof>) then compares this to the hash that was expected in the root node. If they match, the proof passes. Otherwise, something is amiss.

The function “overload” cartesi.keccak(<word>) can be used to obtain the hash for a 64-bit word (i.e., a tree leaf).

The following script verifies the state value proof for the output drive in the calculator example discussed above.

run-calculator-with-proof.lua

-- Load the Cartesi module
local cartesi = require"cartesi"

-- Load the proof verification module
local proof = require"cartesi.proof"

-- Instantiate machine from configuration
local config = require"config.calculator"
local machine = cartesi.machine(config)

-- Write expression to input drive
local input_drive = config.flash_drive[2]
machine:write_memory(input_drive.start, table.concat(arg, " ") .. "\n")

-- Run machine until it halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    machine:run(math.maxinteger)
end

-- Obtain value proof for output flash drive
local output_state_hash = machine:get_root_hash()
local output_drive = config.flash_drive[3]
local output_proof = machine:get_proof(output_drive.start, 12)

-- Verify proof
proof.slice_assert(output_state_hash, output_proof)
print("\nOutput drive proof accepted!\n")

print((string.unpack("z", machine:read_memory(output_drive.start, output_drive.length))))

Running the script with the command-line

lua5.3 run-calculator-with-proof.lua 6*2^1024 + 3*2^512

produces the output

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI
        \ /   MACHINE
         '


Output drive proof accepted!

10786158809173895446375831144734148401707861873653839436405804869463\
96054833005778796250863934445216126720683279228360145952738612886499\
73495708458383684478649003115037698421037988831222501494715481595948\
96901677837132352593468675094844090688678579236903861342030923488978\
36036892526733668721977278692363075584

Remote Cartesi Machines

The Lua API can also be used to control a Remote Cartesi Machine. The functionality is available as a separate Lua module, the cartesi.grpc submodule. (This is to avoid pulling in unnecessary gRPC dependencies where only local Cartesi Machines are needed.)

The cartesi.grpc.stub(<remote-address>, <checkin-address>) method opens and returns a client connection to an existing Remote Cartesi Machine server. The <remote-address> specifies the remote server to connect to, and the <checkin-address> specifies an address the server will use to notify the client when it is ready. The client connection returned by cartesi.grpc.stub(<remote-address>, <checkin-address>) functions as a remote version of the local cartesi module.

There are two new methods specific to remote connections. The remote.shutdown() method causes the remote server to shutdown. Note that this will, of course, terminate whatever Remote Cartesi Machine the server was managing. The remote.get_version() method returns a semantic_version object that contains the server version:

semantic_version ::= {
  major ::= number,
  minor ::= number,
  patch ::= number,
  pre_release ::= string,
  build ::= string
}

The remote.machine field behaves just like the cartesi.machine “class”. Likewise, the Remote Cartesi Machine instance returned by the remote.machine(<machine_config>) constructor follows the same interface as the local Cartesi Machine instance returned by the cartesi.machine(<machine_config>) constructor. Note that there can only be a single active Cartesi Machine instance per remote server. Therefore, use the machine:destroy() on the active instance machine before instantiating a new machine with the remote.machine(<machine_config>) constructor again.

The following script illustrates the use of the cartesi.grpc submodule.

run-remote-config.lua

-- No need to load the Cartesi module
local cartesi = {}
-- Load the gRPC submodule for Remote Cartesi Machines
cartesi.grpc = require"cartesi.grpc"

-- Writes formatted text to stderr
local function stderr(fmt, ...)
    io.stderr:write(string.format(fmt, ...))
end

-- Create connection to Remote Cartesi Machine server
local remote_address = assert(arg[1], "missing remote address")
local checkin_address = assert(arg[2], "missing checkin address")
stderr("Listening for checkin at '%s'\n", checkin_address)
stderr("Connecting to remote cartesi machine at '%s'\n", remote_address)
local remote = cartesi.grpc.stub(remote_address, checkin_address)

-- Print server version (and test connection)
local v = assert(remote.get_version())
stderr("Connected: remote version is %d.%d.%d\n", v.major, v.minor, v.patch)

-- Instantiate remote machine from configuration
local machine = remote.machine(require(arg[3]))

-- Run machine until it halts or yields
while not machine:read_iflags_H() and not machine:read_iflags_Y() do
    machine:run(math.maxinteger)
end

-- Print machine status
if machine:read_iflags_H() then
    stderr("\nHalted\n")
else
    stderr("\nYielded manual\n")
end
-- Print cycle count
stderr("Cycles: %u\n", machine:read_mcycle())

-- Shutdown remote server
stderr("Shutting down remote cartesi machine\n")
remote.shutdown()

The script starts by loading the cartesi.grpc module. It then opens a client connection to the remote server using addresses specified as the first and second command-line arguments. It calls the remote.get_version() method to test the connection and prints the version number returned by the server. From then on, the code is virtually the same as it would be if everything was local.

The script creates a Remote Cartesi Machine instance using the remote.machine(<machine_config>) method, passing the configuration obtained from the third command-line argument. Note that, if the server has an active machine instance already, the call will fail. Furthermore, any resources referenced in the machine_config must be accessible to the server or the call will also fail. The script runs the returned remote machine instance until it halts or yields manual. It then prints the reason the machine stopped running and the cycle count at that point. Finally, it shuts down the server.

Recall that, to run a server inside the playground, we opened a separate shell into the same playground container (For example, by running docker exec -it <container-name> /bin/bash), and then ran the remote-cartesi-machine server in it

remote-cartesi-machine \
    --server-address=localhost:8080

Now, instead of using the cartesi-machine command-line utility to control it, run the run-remote-config.lua client script in the other shell

lua5.3 run-remote-config.lua \
    localhost:8080 \
    localhost:8081 \
    config.nothing-to-do

The client shell produces

Listening for checkin at 'localhost:8081'
Connecting to remote cartesi machine at 'localhost:8080'
Connected: remote version is 0.6.0

Halted
Cycles: 62388529
Shutting down remote cartesi machine

The server shell produces

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI
        \ /   MACHINE
         '

Nothing to do.

Rolling Cartesi Machines

Target applications running inside Rolling Cartesi Machines communicate with the outside world by using Cartesi Rollups. In production, the Server Manager is responsible for passing advance-state and inspect-state requests to the machine and collecting the responses (vouchers, notices, reports, and exceptions) that were generated while processing each request. When prototyping, the cartesi-machine command-line utility can be used to play the same part, loading sequentially-numbered requests from files and storing sequentially-numbered responses to files. As expected, the Lua interface can also be used to feed requests to a Rolling Cartesi Machine and obtain the responses it produces.

The target application (indirectly) raises the HTIF manual yield flag (machine:read_iflags_Y() == true) to notify the host it is done with the current request and ready for the next. While processing each request, it raises the HTIF automatic yield flag (machine:read_iflags_X() == true) for each new response it generates. In both cases, the reason for the yield is available from bits 47-32 in the tohost HTIF CSR (machine:read_tohost_data() >> 32). When transitioning between requests, the reason can take the values machine.HTIF_YIELD_REASON_RX_ACCEPTED (previous request was accepted), machine.HTIF_YIELD_REASON_RX_REJECTED (previous request was rejected), or machine.HTIF_YIELD_REASON_TX_EXCEPTION (an unrecoverable error was encountered). When generating a new response to a request, the reason can take the self-explanatory values machine.HTIF_YIELD_REASON_TX_VOUCHER, machine.HTIF_YIELD_REASON_TX_NOTICE, and machine.HTIF_YIELD_REASON_TX_REPORT.

The data associated with requests is sent to the machine in the rollup memory ranges defined by memory_range_config entries stored in the machine_config as rollup.rx_buffer and rollup.input_metadata. Conversely, the data associated with responses (or exceptions) is obtained from the machine in the rollup.tx_buffer rollup memory range. Finally, hashes for vouchers and notices produced in response to advance-state requests are written, respectively, to arrays in the rollup.voucher_hashes and rollup.notice_hashes rollup memory ranges, in the order they are produced.

Data in the input-metadata memory range consists of the following fields: a message sender (an EVM address), a block-number, a timestamp (seconds since the Unix epoch), the rollup epoch index, and the rollup input index. All entries are 256-bit big-endian unsigned integers. In practice, only the least-significant 20 bytes are used for the message sender address, and only the least-significant 8 bytes, or 64-bits, are used for the remaining number entries. (See the table in the target perspective architecture.)

Data for the input to an advance-state request, the query to an inspect-state request, exceptions, notices, and reports are all encoded in the same way: a 256-bit offset field (with value 32), then a 256-bit length field, directly followed by payload with length bytes. The offset and length fields are encoded as 256-bit big-endian unsigned integers. Data for vouchers start with an address field (an EVM address, again as the least-significant 20 bytes in a 256-bit big-endian unsigned integer) and then continue just like the others: and offset field (this time with value 64), then a 256-bit length field, directly followed by payload with length bytes. (See the table in the target perspective architecture.)

The following script illustrates how the Lua API can be used to send advance-state requests to a Rolling Cartesi Machine, and how it can be used to collect the notices produced as responses (We will use the server calculator example:

run-rolling-calculator.lua

-- No need to load the Cartesi module
local cartesi = {}
cartesi.grpc = require"cartesi.grpc"

-- Writes formatted text to stderr
local function stderr(fmt, ...)
    io.stderr:write(string.format(fmt, ...))
end

-- Create connection to Remote Cartesi Machine server
local remote_address = assert(arg[1], "missing remote address")
local checkin_address = assert(arg[2], "missing checkin address")
stderr("Listening for checkin at '%s'\n", checkin_address)
stderr("Connecting to remote cartesi machine at '%s'\n", remote_address)
local remote = cartesi.grpc.stub(remote_address, checkin_address)

-- Print server version (and test connection)
local v = assert(remote.get_version())
stderr("Connected: remote version is %d.%d.%d\n", v.major, v.minor, v.patch)

-- Instantiate machine from template
local machine = remote.machine("rolling-calculator-template")

-- Get initial config from template
local config = machine:get_initial_config()

-- Print a string splitting it into multiple lines
local function fold(str, w)
    local i = 1
    while i <= #str do
        print(str:sub(i, i+w-1))
        i = i + w
    end
end

-- Encode an unsigned integer into 256-bit big-endian
local function encode_be256(value)
    return string.rep("\0", 32-8)..string.pack(">I8", value)
end

-- Write the input metadata memory range
local function write_input_metadata(machine, input_metadata, i)
    machine:write_memory(input_metadata.start,
        encode_be256(0) .. -- msg_sender
        encode_be256(0) .. -- block_number
        encode_be256(os.time()) .. -- time_stamp
        encode_be256(0) .. -- epoch_index
        encode_be256(i) -- input_index"
    )
end

-- Write the input into the rx_buffer memory range
local function write_input(machine, rx_buffer, input)
    machine:write_memory(rx_buffer.start,
        encode_be256(32) .. -- offset
        encode_be256(#input) .. -- length
        input -- input itself
    )
end

-- Read a notice from the tx_buffer memory range
local function read_notice(machine, tx_buffer, str)
    -- Get length of output, skipping offset
    local length = string.unpack(">I8",
        machine:read_memory(tx_buffer.start+32+24, 8))
    -- Get output itself, skipping offset and length
    return machine:read_memory(tx_buffer.start+64, length)
end

-- Obtain the relevant rollup memory ranges from the initial config
assert(config.rollup, "rollup not enabled in machine")
local rx_buffer = config.rollup.rx_buffer
local tx_buffer = config.rollup.tx_buffer
local input_metadata = config.rollup.input_metadata

-- Run machine until it halts
local i = 0
while not machine:read_iflags_H() do
    machine:run(math.maxinteger)
    local reason = machine:read_htif_tohost_data() >> 32
    -- Machine yielded manual
    if machine:read_iflags_Y() then
        -- Send new request if previous was accepted
        if reason == remote.machine.HTIF_YIELD_REASON_RX_ACCEPTED then
            -- Otherwise, obtain expression from stdin
            stderr("type expression\n") -- prompt for expression
            local expr = io.read()
            if not expr then
                break
            end
            machine:snapshot()
            i = i + 1
            -- Write expression as the input
            write_input(machine, rx_buffer, expr)
            -- Write the input metadata
            write_input_metadata(machine, input_metadata, i)
            -- Tell machine this is an advance-state request
            machine:write_htif_fromhost_data(0)
            -- Reset the Y flag so machine can proceed
            machine:reset_iflags_Y()
        -- Otherwise, rollback to state before processing was attempted
        elseif i > 0 then
            stderr("input rejected\n")
            machine:rollback()
        else
            stderr("machine initialization failed\n")
            break
        end
    -- Machine yielded automatic
    elseif machine:read_iflags_X() then
        -- It output a notice
        if reason == remote.machine.HTIF_YIELD_REASON_TX_NOTICE then
            -- Read notice and print it
            stderr("result is\n")
            fold(read_notice(machine, tx_buffer), 68)
        end
    end
end

-- Shutdown remote server
stderr("Shutting down remote cartesi machine\n")
remote.shutdown()

Rolling Cartesi Machines must be rolled-back to the state they were at before they received an advance-state request they later rejected. This requires the machine:snapshot() and machine:rollback() methods available only in Remote Cartesi Machines. Therefore, the script uses the cartesi.grpc module to instantiate a remote machine based on the "rolling-calculator-template".

After defining a variety of helper functions, the script obtains from the machine configuration the rollup memory ranges it will later use to exchange data with the Rolling Cartesi Machine: rollup.rx_buffer, rollup.tx_buffer, and rollup.input_metadata.

It then enters its main loop, which is executed until the machine halts. For each iteration, the script invokes machine:run(math.maxinteger) to run the machine until it yields or halts. When the call returns, it checks if the machine yielded manual. If so, it checks the reason for the yield.

If the reason was machine.HTIF_YIELD_REASON_RX_ACCEPTED, the application accepted the previous request and is ready for the next. The script then attempts to obtain a mathematical expression from the console. If the user provides one, it creates a new snapshot and then writes the expression as the input payload into rollup.rx_buffer and the input metadata to rollup.input_metadata, both in the appropriate encoding. Before continuing with the next loop iteration, the script informs the server that the new request is an advance-state request by writing 0 to the data field of the HTIF tohost CSR (as opposed to 1, which would signify an inspect-state request). It also clears the Y flag in the iflags CSR to release the machine for execution. If, however, the reason was anythying else, the script rolls back the machine and continues with the next loop iteration.

If the machine yielded automatic, the script once again checks for the yield reason. If the reason was machine.HTIF_YIELD_REASON_TX_NOTICE, the script decoes the notice payload from rollup.tx_buffer and prints the formatted result to the console.

Here is what a session looks like. First, open an separate shell into the same playground container (For example, by running docker exec -it <container-name> /bin/bash) and run the remote-cartesi-machine server in it

remote-cartesi-machine \
    --server-address=localhost:8080

Then, run the run-rolling-calculator.lua client script in the other shell

lua run-rolling-calculator.lua localhost:8080 localhost:8081

The client prints the connection status to the console

Listening for checkin at 'localhost:8081'
Connecting to remote cartesi machine at 'localhost:8080'
Connected: remote version is 0.5.0

and prompts us to type an expression. Entering 6*2^1024 + 3*2^512 causes the expected result to be printed:

type expression
6*2^1024 + 3*2^512
result is
10786158809173895446375831144734148401707861873653839436405804869463
96054833005778796250863934445216126720683279228360145952738612886499
73495708458383684478649003115037698421037988831222501494715481595948
96901677837132352593468675094844090688678579236903861342030923488978
36036892526733668721977278692363075584

The client then asks for a new expression. Entering an invalid expression 1+( causes the calc.sh script running inside the Rolling Cartesi Machine to reject the input:

type expression
1+(
input rejected

Finally, entering ^D causes the client script to shutdown the server and exit.

type expression
^D
Shutting down remote cartesi machine

The remote console shows only the error generated when the invalid expression 1+( was entered:

bc: bad expression at '('
[json.exception.parse_error.101] parse error at line 1, column 1: syntax error while parsing value - unexpected end of
input; expected '[', '{', or a literal

State transition proofs

During verification, the blockchain mediates a verification game between the disputing parties. This process is explained in detail under the blockchain perspective. In a nutshell, both parties started from a Cartesi Machine that has a known and agreed upon initial state hash. (E.g., an agreed upon template that was instantiated with an agreed upon input drive.) At the end of the computation, these parties now disagree on the state hash for the halted machine. The state hash evolves as the machine executes steps in its fetch-execute loop. The first stage of the verification game therefore searches for the step of disagreement: the particular cycle such that the parties agree on the state hash before the step, but disagree on the state hash after the step. Once this step of disagreement is identified, one of the parties sends to the blockchain a log of state accesses that happen along the step, including cryptographic proofs for every value read from or written to the state. This log proves to the blockchain that the execution of the step transitions the state in such a way that it finally reaches the state hash claimed by the submitting party.

To obtain the access log for the next step in the execution of a Cartesi Machine instance, use the machine:step(<log_type>) function. Note that the function indeed performs the step, and therefore advances the state, in addition to collecting the access log. The <log_type> argument specifies if the access log should include annotations and cryptographic proofs, or only the accesses themselves. It is a table in the format

log_type ::= {
  proofs ::= boolean,
  annotations ::= boolean
}

The format of the access log returned is as follows:

access_log ::= {
  accesses ::= {
    [1] ::= word_access,
    [2] ::= word_access,
    ...
    [n] ::= word_access
  },
  notes ::= {
    [1] ::= string,
    [2] ::= string,
    ...
    [n] ::= string,
  },
  brackets ::= {
    [1] ::= bracket,
    [2] ::= bracket,
    ...
    [m] ::= bracket
  },
}

word_access ::= {
  type ::= "read" | "write",
  address ::= number,
  read ::= number,
  written ::= number
  proof ::= proof
}

bracket ::= {
  type ::= "begin" | "end",
  where ::= number,
  text ::= string
}

The word accesses array records, in order, all accesses to the machine state performed during the execution of the next step in the evolution of the Cartesi Machine state. Word accesses can be of type either "read" or "write". The address field specifies the physical address of the corresponding (aligned) 64-bit word accessed. Read accesses contain the value read for the word. Write accesses contain, in the read field, the value that was in the state before it was overwritten by the value in the written field. The proof field is used when verifying state transitions.

Inspecting access logs

When the log_type includes the field annotations = true, the access log includes annotations that help put each access into a larger context.

The notes array contains a string corresponding to each entry in the accesses array, describing the word access. The brackets contain information that groups ranges of word accesses into scopes. Each bracket entry type field tells if the entry marks the "begin" or "end" of a scope. The where field gives the position in the accesses array where the bracket should be “inserted”.

The dump_log(<log>, <out>) function in the cartesi.util module uses these annotations to dump a detailed description of the access <log> into file <out>:

cartesi/util.lua (excerpt)

-- Output formatted string with indentation
local function indentout(f, indent, fmt, ...)
    f:write(string.rep("  ", indent), string.format(fmt, ...))
end

-- Convert string to hex
local function hexstring(hash)
    return (string.gsub(hash, ".", function(c)
        return string.format("%02x", string.byte(c))
    end))
end

-- Take first 8 characters in hexadecimal hash
local function hexhash8(hash)
    return string.sub(hexstring(hash), 1, 8)
end

-- Convert binary data to number or to start and end as hexdecimal
local function accessdatastring(data, log2_size)
    if log2_size == 3 then
        data = string.unpack("<I8", data)
        return string.format("0x%x(%u)", data, data)
    else
        return string.format("%s...%s(2^%d bytes)",
            hexstring(string.sub(data, 1, 3)),
            hexstring(string.sub(data, -3, -1)), log2_size)
    end
end

-- Dump formatted log to file
function _M.dump_log(log, out)
    local indent = 0
    local j = 1 -- Bracket index
    local i = 1 -- Access index
    local brackets = log.brackets or {}
    local notes = log.notes or {}
    local accesses = log.accesses
    -- Loop until accesses and brackets are exhausted
    while true do
        local bj = brackets[j]
        local ai = accesses[i]
        if not bj and not ai then break end
        -- If bracket points before current access, output bracket
        if bj and bj.where <= i then
            if bj.type == "begin" then
                indentout(out, indent, "begin %s\n", bj.text)
                indent = indent + 1 -- Increase indentation before bracket
            elseif bj.type == "end" then
                indent = indent - 1 -- Decrease indentation after bracket
                indentout(out, indent, "end %s\n", bj.text)
            end
            j = j + 1
        -- Otherwise, output access
        elseif ai then
            if ai.proof then
                indentout(out, indent, "hash %s\n",
                    hexhash8(ai.proof.root_hash))
            end
            local read = accessdatastring(ai.read, ai.log2_size)
            if ai.type == "read" then
                indentout(out, indent, "%d: read %s@0x%x(%u): %s\n", i,
                    notes[i] or "", ai.address, ai.address, read)
            else
                assert(ai.type == "write", "unknown access type")
                local written = accessdatastring(ai.written, ai.log2_size)
                indentout(out, indent, "%d: write %s@0x%x(%u): %s -> %s\n", i,
                    notes[i] or "", ai.address, ai.address, read, written)
            end
            i = i + 1
        end
    end
end

The function indents each access according to the number of enclosing scopes. It uses the notes to print the meaning of each word being accessed: Is it a register, a CSR, memory? Addresses and values are printed in hexadecimal and decimal. If the log was generated with the proofs = true option, then the current state hash before each access is also printed.

Running the dump-step.lua program:

dump-step.lua

-- Load the Cartesi modules
local cartesi = require"cartesi"
local util = require"cartesi.util"

-- Instantiate machine from configuration
local machine = cartesi.machine(require"config.nothing-to-do")

-- Run machine until it halts or yields
local max_mcycle = 46598940
while not machine:read_iflags_H() and not machine:read_iflags_Y() and machine:read_mcycle() < max_mcycle do
    machine:run(max_mcycle)
end
assert(machine:read_mcycle() == max_mcycle, "Machine halted or yielded early!")

-- Obtain state hash before step
local step_log = machine:step{ annotations = true, proofs = true }

-- Dump access log to screen
io.stderr:write(string.format("\nContents of step %u access log:\n\n", max_mcycle))
util.dump_log(step_log, io.stderr)

with command:

lua5.3 dump-step.lua

produces the output:

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI


Contents of step 46598940 access log:

begin step
  hash a00da7eb
  1: read mcycle@0x120(288): 0x2c70b1c(46598940)
  hash a00da7eb
  2: read iflags.H@0x1d0(464): 0x18(24)
  hash a00da7eb
  3: read iflags.Y@0x1d0(464): 0x18(24)
  hash a00da7eb
  4: read iflags.X (superfluous)@0x1d0(464): 0x18(24)
  hash a00da7eb
  5: write iflags.X@0x1d0(464): 0x18(24) -> 0x18(24)
  begin set_rtc_interrupt
  end set_rtc_interrupt
  begin raise_interrupt_if_any
    hash a00da7eb
    6: read mip@0x170(368): 0x0(0)
    hash a00da7eb
    7: read mie@0x168(360): 0x2aa(682)
  end raise_interrupt_if_any
  begin fetch_insn
    hash a00da7eb
    8: read pc@0x100(256): 0x80002fa0(2147495840)
    begin translate_virtual_address
      hash a00da7eb
      9: read iflags.PRV@0x1d0(464): 0x18(24)
      hash a00da7eb
      10: read mstatus@0x130(304): 0xa00000820(42949675040)
    end translate_virtual_address
    begin find_pma_entry
      hash a00da7eb
      11: read pma.istart@0x800(2048): 0x800000f9(2147483897)
      hash a00da7eb
      12: read pma.ilength@0x808(2056): 0x4000000(67108864)
    end find_pma_entry
    hash a00da7eb
    13: read memory@0x80002fa0(2147495840): 0x7378300f6b023(2031360633384995)
  end fetch_insn
  begin sd
    hash a00da7eb
    14: read x@0x68(104): 0x40008000(1073774592)
    hash a00da7eb
    15: read x@0x78(120): 0x10100000000000a(72339069014638602)
    begin translate_virtual_address
      hash a00da7eb
      16: read iflags.PRV@0x1d0(464): 0x18(24)
      hash a00da7eb
      17: read mstatus@0x130(304): 0xa00000820(42949675040)
    end translate_virtual_address
    begin find_pma_entry
      hash a00da7eb
      18: read pma.istart@0x800(2048): 0x800000f9(2147483897)
      hash a00da7eb
      19: read pma.ilength@0x808(2056): 0x4000000(67108864)
      hash a00da7eb
      20: read pma.istart@0x810(2064): 0x1069(4201)
      hash a00da7eb
      21: read pma.ilength@0x818(2072): 0xf000(61440)
      hash a00da7eb
      22: read pma.istart@0x820(2080): 0x80000000000002d9(9223372036854776537)
      hash a00da7eb
      23: read pma.ilength@0x828(2088): 0x5000000(83886080)
      hash a00da7eb
      24: read pma.istart@0x830(2096): 0x4000841a(1073775642)
      hash a00da7eb
      25: read pma.ilength@0x838(2104): 0x1000(4096)
    end find_pma_entry
    hash a00da7eb
    26: write htif.tohost@0x40008000(1073774592): 0x10100000000000d(72339069014638605) -> 0x10100000000000a(72339069014638602)
    hash 8ebc16f9
    27: read htif.iconsole@0x40008018(1073774616): 0x2(2)
    hash 8ebc16f9
    28: write htif.fromhost@0x40008008(1073774600): 0x0(0) -> 0x101000000000000(72339069014638592)
    hash 7fa4fe27
    29: write pc@0x100(256): 0x80002fa0(2147495840) -> 0x80002fa4(2147495844)
  end sd
  hash bac08fcc
  30: read minstret@0x128(296): 0x2c70aef(46598895)
  hash bac08fcc
  31: write minstret@0x128(296): 0x2c70aef(46598895) -> 0x2c70af0(46598896)
  hash 65519976
  32: read mcycle@0x120(288): 0x2c70b1c(46598940)
  hash 65519976
  33: write mcycle@0x120(288): 0x2c70b1c(46598940) -> 0x2c70b1d(46598941)
end step

Understanding these logs in detail is unnecessary for all but the most low-level internal development at Cartesi. It requires deep knowledge of not only RISC-V architecture, but also how Cartesi's emulator implements it. The material is beyond the scope of this document. In this particular example, however, it was hand-picked for illustration purposes. The RISC-V instruction being executed, sd, writes the 64-bit word 0x010100000000000a to address 0x40008000 (access #26). This is the memory-mapped address of HTIF's tohost CSR. The value refers to the console subdevice (DEV=0x01) , command putchar (CMD=0x01), and causes the device to output a line-feed (DATA=0x0a). I.e., the instruction is completing the row \ / CARTESI in the splash screen.

Verifying state transitions

When the log_type includes the field proofs = true, each word access comes with a proof field containing the proof for the value read. Using the known state hash before the access, it is possible to verify that the value reported read was indeed the value stored at the physical address in the machine state. For a "read" access, the state hash does not change. However, for a "write" access, the sibling_hashes in the proof (which have just been verified to be truthful along with the value read) can be used to compute the new state hash. The new hash is simply

new_hash = proof.roll_hash_up_tree(access.proof, cartesi.keccak(access.written))

In this way, the accesses can be processed one by one, until the new state hash at the end of the step has been obtained.

The process described above can only verify that, should these accesses be performed starting from the state as it was before the step, a given state hash would obtain. To ensure that the accesses indeed correspond to the operation of a Cartesi Machine starting from that state, knowledge of the Cartesi Machine architecture as implemented by the emulator is needed. The function cartesi.machine.verify_state_transition(<state_hash_before>, <access_log>, <state_hash_after>, <runtime_config>) uses this knowledge to verify that the <access_log> transitions from <state_hash_before> to <state_hash_after>. Note there is no need for a Cartesi Machine instance to verify a transition. All required state information is in the access log. (The <machine_runtime_config>

The following script illustrates the verification of a state transition.

verify-step.lua

-- Load the Cartesi modules
local cartesi = require"cartesi"
local util = require"cartesi.util"

-- Instantiate machine from configuration
local machine = cartesi.machine(require"config.nothing-to-do")

-- Run machine until it halts or yields
local max_mcycle = 46598940
while not machine:read_iflags_H() and not machine:read_iflags_Y() and machine:read_mcycle() < max_mcycle do
    machine:run(max_mcycle)
end
assert(machine:read_mcycle() == max_mcycle, "Machine halted early!")

-- Obtain state hash before step
local hash_before_step = machine:get_root_hash()
-- Obtain access log
local step_log = machine:step{ annotations = true, proofs = true }
-- Obtain state hash after step
local hash_after_step = machine:get_root_hash()

-- Potentially mess with state access to cause a verification failure
if #arg > 0 then
    local env = { string = string, cartesi = cartesi, step_log = step_log }
    local f = assert(load(arg[1], arg[1], "t", env))
    f()
end

-- Verify step access log
assert(cartesi.machine.verify_state_transition(hash_before_step, step_log, hash_after_step, {}))
io.stderr:write("State transition accepted!\n")

Running the script without arguments accepts the valid state transition.

lua5.3 verify-step.lua

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI


State transition accepted!

The script is much more interesting when the argument is used to “mess” with the access log before verification. For example, changing the address of access #26

26: write htif.tohost@0x40008000(1073774592): 0x10100000000000d(72339069014638605) -> 0x10100000000000a(72339069014638602)

from 0x40008000 to 0x100 causes the program to reject the state transition proof:

lua5.3 verify-step.lua 'step_log.accesses[26].address = 0x100'

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI

lua5.3: verify-step.lua:31: expected access 26 to write htif.tohost at address 0x40008000(1073774592)
stack traceback:
    [C]: in function 'assert'
    verify-step.lua:31: in main chunk
    [C]: in ?

The error message states that, starting from the <state_hash_before> and given accesses 1–26 in the <access_log>, a true Cartesi Machine would have written to address 0x40008000 (helpfully labeled as the CSR htif.tohost), rather than address 0x100 claimed by our corrupt access log.

Changing the value written also causes the proof to fail, because the earlier entries completely determine the value a true Cartesi Machine would have written:

lua5.3 verify-step.lua 'step_log.accesses[26].written = string.pack(">I8", 0x1234)'

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI

lua5.3: verify-step.lua:30: word value written in access 26 does not match log
stack traceback:
    [C]: in function 'assert'
    verify-step.lua:30: in main chunk
    [C]: in ?

Changing the value read also causes the proof to be rejected because it will not match the target hash:

lua5.3 verify-step.lua 'step_log.accesses[26].read = string.pack(">I8", 0x1234)'

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI

lua5.3: verify-step.lua:30: word value before write access 26 does not match target hash
stack traceback:
    [C]: in function 'assert'
    verify-step.lua:30: in main chunk
    [C]: in ?

Changing the target hash to match the false value read causes the proof to be rejected because rolling the target hash up the tree will not result in the expected root hash:

lua5.3 verify-step.lua 'local access = step_log.accesses[26];access.read = 0x1234; access.proof.target_hash = cartesi.keccak(access.read);'

         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI

lua5.3: verify-step.lua:30: word value before write access 26 fails proof
stack traceback:
    [C]: in function 'assert'
    verify-step.lua:30: in main chunk
    [C]: in ?

In a nutshell, only valid state transitions are accepted by the cartesi.machine.verify_state_transition() function.