> For the complete documentation index, see [llms.txt](https://docs.cartesi.io/llms.txt)

---
title: 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
```lua
-- 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

<div class="grid md:grid-cols-2 gap-4">
<div>

<a name="machine_config"></a>

```lua
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,
}
```

<a name="rom_config"></a>

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

<a name="ram_config"></a>

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

<a name="htif_config"></a>

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

<a name="clint_config"></a>

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

<a name="rollup_config"></a>

```lua
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
}
```


</div>

<div class="col col--6">

<a name="processor_config"></a>

```lua
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
},
```

<a name="memory_range_config"></a>

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

</div>
</div>

The <a href="#rom_config">`rom`</a> 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](http://github.com/cartesi/machine-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*](http://devicetree.org/) that describes the hardware to Linux, passes the `bootargs` string as the kernel command-line parameters, then cedes control to the RAM image.

The <a href="#ram_config">`ram`</a> 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](http://github.com/cartesi/machine-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 <a href="#memory_range_config">`memory_range_config`</a> 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 <i>not</i> 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 <a href="#htif_config">`htif`</a> 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 <a href="#rollup_config">`rollup`</a> 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](../target/architecture.md) 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](https://riscv.org/technical/specifications/) of the  ISA specification.
The Cartesi-specific additions are described under the [architecture section](../target/architecture.md) under the target perspective.

The <a href="#clint_config">`clint`</a> entry has a single field, `mtimecmp`, which allows for the overriding of the default initial value of this CSR.
Similarly, the fields in the <a href="#processor_config">`processor`</a> 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](./cmdline.md#initialization) that the `cartesi-machine` command

```bash
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](https://github.com/cartesi/machine-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.

```lua
%machine.host.lua.config-dump-ls-bin
```

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:
```lua title="config/ls-bin.lua"
return {
  processor = {
    mvendorid = %machine.host.lua.config-mvendorid,
    mimpid = %machine.host.lua.config-mimpid,
    marchid = %machine.host.lua.config-marchid,
  },
  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](https://elixir.bootlin.com/linux/v5.5.19/source/drivers/mtd/parsers/cmdlinepart.c) 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](./cmdline.md#flash-drives)
```bash
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:
```lua title="config/cat-foo-bar.lua"
return {
  processor = {
    mvendorid = %machine.host.lua.config-mvendorid,
    mimpid = %machine.host.lua.config-mimpid,
    marchid = %machine.host.lua.config-marchid,
  },
  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:
```bash
cartesi-machine \
    --max-mcycle=0 \
    --store-config
```
```lua title="config/nothing-to-do.lua"
return {
  processor = {
    mvendorid = %machine.host.lua.config-mvendorid, -- cartesi.machine.MVENDORID
    mimpid = %machine.host.lua.config-mimpid, -- cartesi.machine.MIMPID
    marchid = %machine.host.lua.config-marchid, -- 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:
```bash
cartesi-machine \
    --htif-yield-automatic \
    --max-mcycle=0 \
    --store-config \
    -- $'for i in $(seq 0 5 1000); do yield automatic progress $i; done'
```
```lua title="config/progress.lua"
return {
  processor = {
    mvendorid = %machine.host.lua.config-mvendorid,
    mimpid = %machine.host.lua.config-mimpid,
    marchid = %machine.host.lua.config-marchid,
  },
  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:
```bash
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)'
```
```lua title="config/calculator.lua"
return {
  processor = {
    mvendorid = %machine.host.lua.config-mvendorid, -- cartesi.machine.MVENDORID
    mimpid = %machine.host.lua.config-mimpid, -- cartesi.machine.MIMPID
    marchid = %machine.host.lua.config-marchid, -- 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
```lua title="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.

<a id="run-cat-foo-bar"></a>

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

```bash
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.
```lua title="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
```lua title="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](#run-cat-foo-bar), 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
```lua title="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](../target/architecture.md).
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:
```lua title="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 &ldquo;per-chunk&rdquo; tasks.

For example, running the script with the command-line
```bash
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
```bash
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](./cmdline.md#cartesi-machine-templates), 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:
```bash
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`:
```bash
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:
```lua title="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,
```bash
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:
```lua title="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
```bash
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.
```bash
cartesi-machine \
    --initial-hash \
    --final-hash
```
<div class="grid md:grid-cols-2 gap-4">
<div>

```
%machine.host.lua.state-hashes-lua
```

</div>
<div>

```
%machine.host.lua.state-hashes-utility
```

</div>
</div>

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](https://content.riscv.org/wp-content/uploads/2017/05/riscv-spec-v2.2.pdf), and its [privileged architecture](https://content.riscv.org/wp-content/uploads/2017/05/riscv-privileged-v1.10.pdf).
Cartesi-specific registers are described under the target perspective sections that cover the [processor](../target/architecture.md#the-processor) and [board](../target/architecture.md#the-board) of the Cartesi Machine architecture.

The method `machine:read_x(<index>)`, where `<index>` is in 0&hellip;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&hellip;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:
```lua title="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

```bash
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&times;2<sup>1024</sup>+3&times;2<sup>512</sup>.

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&hellip;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:
```lua
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.

```lua title="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<sup>`log2_size`</sup> 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 &ldquo;overload&rdquo; `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.
```lua title="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

```bash
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:
```lua
semantic_version ::= {
  major ::= number,
  minor ::= number,
  patch ::= number,
  pre_release ::= string,
  build ::= string
}
```

The `remote.machine` field behaves just like the `cartesi.machine` &ldquo;class&rdquo;.
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.
```lua title="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
```bash
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
```bash
lua5.3 run-remote-config.lua \
    localhost:8080 \
    localhost:8081 \
    config.nothing-to-do

```
The client shell produces
```
%machine.host.lua.remote-client
```
The server shell produces
```
%machine.host.lua.remote-server
```

## 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](../target/architecture.md#rollup-format).)

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](../target/architecture.md#rollup-format).)

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](./cmdline.md#rolling-cartesi-machine-templates):

```lua title="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
```bash
remote-cartesi-machine \
    --server-address=localhost:8080
```

Then, run the `run-rolling-calculator.lua` client script in the other shell
```bash
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](../blockchain/vg.md).
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

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

The format of the access log returned is as follows:

<div class="grid md:grid-cols-2 gap-4">
<div>

```lua
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
  },
}
```

</div>

<div>

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

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

```
</div>

</div>

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](#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 &ldquo;inserted&rdquo;.

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>`:

```lua title="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 hexadecimal
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:

```lua title="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 = %machine.host.cmdline.cycles-limit-exec
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:
```bash
lua5.3 dump-step.lua
```
produces the output:
```
%machine.host.lua.state-transition-dump-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&nbsp;#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
```lua
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.

```lua title="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 = %machine.host.cmdline.cycles-limit-exec
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.
```bash
lua5.3 verify-step.lua
```
```
         .
        / \
      /    \
\---/---\  /----\
 \       X       \
  \----/  \---/---\
       \    / CARTESI


State transition accepted!
```

The script is much more interesting when the argument is used to &ldquo;mess&rdquo; 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:
```bash
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&ndash;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:
```bash
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:
```bash
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:
```bash
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.