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 modulelocal cartesi = require"cartesi"
The most important field in the module is the cartesi.machine
“class”, used to instantiate new 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). 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, 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.
machine_config ::= { rom ::= rom_config, ram ::= ram_config, flash_drive ::= { [1] ::= flash_drive_config, -- flash drive 0 [2] ::= flash_drive_config, -- flash drive 1 ... [n] ::= flash_drive_config -- flash drive n <= 7 }, processor ::= processor_config, clint ::= clint_config, htif ::= htif_config}
rom_config ::= { bootargs ::= string, image_filename ::= string}
ram_config ::= { length ::= number, image_filename ::= string}
flash_drive_config ::= { start ::= number, length ::= number, image_filename ::= string, shared ::= boolean}
htif_config ::= { fromhost ::= number, tohost ::= number, console_putchar ::= boolean, yield_progress ::= boolean, yield_rollup ::= boolean}
clint_config ::= { mtimecmp ::= number,}
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},
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 containing flash drive configurations.
Each configuration 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.
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_progress
Boolean instructs the emulator to honor the progress command in the HTIF Yield subdevice.
This is used as a means for applications running in the target to inform the host about the current progress in the computation they are performing.
When set to false
(the default), the emulator continues execution past yield commands without returning control to the host.
Similarly, the yield_rollup
causes the emulator to honor the rollup command in the HTIF Yield subdevice.
This command is used by the applications running in the target to inform the host that they have processed all available input, produced the required output, and are therefore idle waiting for further instructions.
This mechanism is used by stateful Cartesi Machines.
The other 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 the RISC-V user-level ISA and privileged architecture specifications.
The Cartesi-specific additions are described under the target perspective architecture.
The fields tohost
and fromhost
in htif
allow for the overriding of the default initial values of these CSRs.
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.
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
playground:~$ 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 \ --dump-machine-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 clock cycle), i.e., before the machine even starts running.
The key command-line option is --dump-machine-config
, which cases the emulator to dump the corresponding configuration to screen:
machine_config = { 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 = 0x4, -- 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 mtdparts=flash.0:-(root) -- ls /bin", }, htif = { tohost = 0x0, -- default fromhost = 0x0, -- default console_getchar = false, -- default yield_progress = false, -- default yield_rollup = false, -- default }, clint = { mtimecmp = 0x0, -- default }, flash_drive = { { start = 0x8000000000000000, length = 0x3c00000, image_filename = "/opt/cartesi/share/images/rootfs.ext2", shared = false, -- default }, },}
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:
return { processor = { mvendorid = 0x6361727465736920, -- cartesi.machine.MVENDORID mimpid = 0x1, -- cartesi.machine.MIMPID marchid = 0x4, -- cartesi.machine.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 mtdparts=flash.0:-(root) -- ls /bin", }, flash_drive = { { start = 0x8000000000000000, length = 0x3c00000, 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 filled out from values exposed by the cartesi.machine
class itself.
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.
Most parameters are commonly found in typical Linux setups.
Two of them 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, and again omitting default values,
playground:~$ mkdir fooplayground:~$ echo Hello world > foo/bar.txtplayground:~$ genext2fs -b 1024 -d foo foo.ext2playground:~$ cartesi-machine \ --flash-drive=label:"foo,filename:foo.ext2" \ --max-mcycle=0 \ --dump-machine-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:
return { processor = { mvendorid = 0x6361727465736920, -- cartesi.machine.MVENDORID mimpid = 0x1, -- cartesi.machine.MIMPID marchid = 0x4, -- cartesi.machine.MARCHID }, ram = { image_filename = "/opt/cartesi/share/images/linux.bin", length = 0x4000000, }, rom = { bootargs = "console=hvc0 rootfstype=ext2 root=/dev/mtdblock0 rw quiet 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 = 0x3c00000, }, { 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 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.
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:
playground:~$ cartesi-machine \ --max-mcycle=0 \ --dump-machine-config
return { processor = { mvendorid = 0x6361727465736920, -- cartesi.machine.MVENDORID mimpid = 0x1, -- cartesi.machine.MIMPID marchid = 0x4, -- 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 mtdparts=flash.0:-(root)", }, flash_drive = { { image_filename = "/opt/cartesi/share/images/rootfs.ext2", start = 0x8000000000000000, length = 0x3c00000, }, },}
A Cartesi Machine that periodically reports its progress using the HTIF Yield device:
playground:~$ cartesi-machine \ --htif-yield-progress \ --max-mcycle=0 \ --dump-machine-config \ -- $'for i in $(seq 0 5 1000); do yield progress $i; done'
return { processor = { mvendorid = 0x6361727465736920, -- cartesi.machine.MVENDORID mimpid = 0x1, -- cartesi.machine.MIMPID marchid = 0x4, -- 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 mtdparts=flash.0:-(root) -- for i in $(seq 0 5 1000); do yield progress $i; done", }, htif = { yield_progress = true, }, flash_drive = { { image_filename = "/opt/cartesi/share/images/rootfs.ext2", start = 0x8000000000000000, length = 0x3c00000, }, },}
A Cartesi Machine that computes the value of a generic mathematical expression:
playground:~$ 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 \ --dump-machine-config \ -- $'dd status=none if=$(flashdrive input) | lua -e \'print((string.unpack("z", io.read("a"))))\' | bc | dd status=none of=$(flashdrive output)'
return { processor = { mvendorid = 0x6361727465736920, -- cartesi.machine.MVENDORID mimpid = 0x1, -- cartesi.machine.MIMPID marchid = 0x4, -- 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 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 = 0x3c00000, }, { start = 0x9000000000000000, length = 0x1000, }, { start = 0xa000000000000000, length = 0x1000, }, },}
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
-- Load the Cartesi modulelocal cartesi = require"cartesi"-- Instantiate machine from configurationlocal machine = cartesi.machine(require(arg[1]))-- Run machine until it haltswhile not machine:read_iflags_H() do machine:run(math.maxinteger)end
loads a machine configuration from the Lua module specified in the command-line (using require(arg[1])
), and then runs it.
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.
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.
The machine:read_iflags_H()
method returns the value of this bit, which is used to break the loop.
For example, to run the configuration stored in ./config/cat-foo-bar.lua
(assuming ./foo.ext2
is available) simply run
playground:~$ luapp5.3 run-config.lua config.cat-foo-bar
. / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESI \ / MACHINE 'Hello world!
The machine:get_initial_config()
returns the configuration that was used to create a Cartesi Machine instance.
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.
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.
-- Load the Cartesi modulelocal cartesi = require"cartesi"-- Instantiate machine from configurationlocal machine = cartesi.machine(require"config.cat-foo-bar")-- Store persistent state to directorymachine: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 the Cartesi modulelocal cartesi = require"cartesi"-- Instantiate machine from persistent state directorylocal machine = cartesi.machine("cat-foo-bar")-- Run machine until it haltswhile not machine:read_iflags_H() 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.
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
-- Load the Cartesi modulelocal cartesi = require"cartesi"-- Instantiate machine from configurationlocal machine = cartesi.machine(require(arg[1]))local CHUNK = 1000000 -- 1 million cycles-- Loop until machine is haltedwhile not machine:read_iflags_H() do -- Execute at most CHUNK cycles machine:run(machine:read_mcycle() + CHUNK) -- Potentially perform other tasksend-- Machine is now halted
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.
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 is 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 progress commands by means of the htif.yield_progress
Boolean field in the machine configuration.
When set to true, a progress command will cause the emulator to precociously return from a call to machine:run(<max_mcycle>)
.
Otherwise, progress commands are ignored to the extent 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:
-- Load the Cartesi modulelocal cartesi = require"cartesi"-- Writes formatted text to stderrlocal function stderr(fmt, ...) io.stderr:write(string.format(fmt, ...))end-- Instantiate machine from configurationlocal machine = cartesi.machine(require(arg[1]))local CHUNK = 1000000 -- 1 million cycleslocal max_mcycle = CHUNK-- Loop until machine is haltedwhile not machine:read_iflags_H() do -- Execute at most CHUNK cycles machine:run(max_mcycle) -- Check if machine yielded if machine:read_iflags_Y() then -- Check if yield was due to progress report if machine:read_htif_tohost_cmd() == cartesi.HTIF_YIELD_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 endend-- Machine is now haltedstderr("\nCycles: %u\n", machine:read_mcycle())
The loop repeats until the machine halts.
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 Y in CSR iflags
means the reason for returning was the Yield device.
That device accepts different commands, each potentially carrying data.
The command and the associated data can be found in the HTIF tohost
CSR.
A command cartesi.HTIF_YIELD_PROGRESS
corresponds to a progress report, and the data contains the progress in parts per mil.
The loop is aborted if the bit H in iflags
is set, which signals the machine is halted.
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
playground:~$ luapp5.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
playground:~$ cartesi-machine \ --htif-yield-progress \ -- $'for i in $(seq 0 5 1000); do yield progress $i; done'
which uses an equivalent mechanism for progress report.
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 the all processor's CSRs and general-purpose registers, the contents of RAM and ROM, of all flash drives, and of all other devices 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:
-- Load the Cartesi modulelocal cartesi = require"cartesi"-- Writes formatted text to stderrlocal function stderr(fmt, ...) io.stderr:write(string.format(fmt, ...))end-- Converts hash from binary to hexadecimal stringlocal function hexhash(hash) return (string.gsub(hash, ".", function(c) return string.format("%02x", string.byte(c)) end))end-- Instantiate machine from configurationstderr("Building machine: please wait\n")local machine = cartesi.machine(require(arg[1]))-- Print the initial hashmachine:update_merkle_tree()stderr("%u: %s\n", machine:read_mcycle(), hexhash(machine:get_root_hash()))-- Run machine until it haltswhile not machine:read_iflags_H() do machine:run(math.maxinteger)end-- Print cycle countstderr("\n\nCycles: %u\n", machine:read_mcycle())-- Print the final hashmachine:update_merkle_tree()stderr("%u: %s\n", machine:read_mcycle(), hexhash(machine:get_root_hash()))
State hashes are maintained in a lazy fashion.
If no state hashes are needed, negligible cost is incurred.
The performance penalty imposed on the emulator, were it required to keep state hashes up-to-date, would be unacceptable (by several orders of magnitude).
Before requesting a state hash, the method machine:update_merkle_tree()
must be called.
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.
Immediately after the call to machine:update_merkle_tree()
, state hashes are valid.
State hashes can be obtained with machine:get_root_hash()
method, which returns the corresponding Keccak-256 hash as a 32-byte binary string.
Before running the machine, the script updates the Merkle tree, obtains the initial state hash, converts it to hexadecimal, and prints the result. The script then runs the machine until it halts. Once the machine is halted, the script once again updates the Merkle tree before obtaining and printing the final state hash.
Initial state hashes can be used to ensure the machine created 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
playground:~$ luapp5.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.
playground:~$ cartesi-machine \ --initial-hash \ --final-hash
Building machine: please wait0: 2d4f30d5fe25e8a383ef6e871fb832a250a78d33d02d0fd1ea72bbeda7aaf645 . / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESI \ / MACHINE 'Nothing to do.Cycles: 6101333661013336: dd53c5ad395e31aacf1c2b8b80af3237d3645fd3b95b3ca9ddacbd23f146b885
0: 2d4f30d5fe25e8a383ef6e871fb832a250a78d33d02d0fd1ea72bbeda7aaf645 . / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESI \ / MACHINE 'Nothing to do.HaltedCycles: 6101333661013336: dd53c5ad395e31aacf1c2b8b80af3237d3645fd3b95b3ca9ddacbd23f146b885
Note that the initial state hashes and the final state hashes match, as expected.
Still need to add an example that uses the new machine:replace_flash_drive(flash_drive_config)
method.
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 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, and any of the flash drives.
The selected range must reside entirely inside ROM, entirely inside RAM, or entirely inside one of the flash drives.
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 already 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, and any of the flash drives.
Note that the bytes in the string <data>
must entirely fit inside ROM, inside RAM, or inside one of the flash drives.
The typical use case for machine:write_memory()
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:
-- Load the Cartesi modulelocal cartesi = require"cartesi"-- Instantiate machine from configurationlocal calculator_config = require"config.calculator"local machine = cartesi.machine(calculator_config)-- Write expression to input drivelocal input_drive = calculator_config.flash_drive[2]machine:write_memory(input_drive.start, table.concat(arg, " ") .. "\n")-- Run machine until it haltswhile not machine:read_iflags_H() do machine:run(math.maxinteger)endlocal 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.
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
playground:~$ luapp5.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×21024+3×2512.
Finally, external state modifications are useful in the setup of artificial, unexpected conditions in regression tests.
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 must be updated to account for state changes with a call to the machine:update_merkle_tree()
method prior to any call to machine:get_proof()
method.
Otherwise, the reported results will contain garbage concerning stale state data.
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 its 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 accept(<proof>)
exported by the cartesi.proof
module performs exactly this task.
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 hashendfunction _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")endreturn _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 2log2_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 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.
-- Load the Cartesi modulelocal cartesi = require"cartesi"-- Load the proof verifiction modulelocal proof = require"cartesi.proof"-- Instantiate machine from configurationlocal config = require"config.calculator"local machine = cartesi.machine(config)-- Write expression to input drivelocal input_drive = config.flash_drive[2]machine:write_memory(input_drive.start, table.concat(arg, " ") .. "\n")-- Run machine until it haltswhile not machine:read_iflags_H() do machine:run(math.maxinteger)end-- Obtain value proof for output flash drivemachine:update_merkle_tree()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 proofproof.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
playground:~$ luapp5.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
This is an advanced section, not needed by regular users of the Cartesi platform.
During verification, the blockchain mediates a verification game between the disputing parties. This process is explained in detail under the 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 is should include cryptographic proofs and annotations, 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 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.
When the log_type
includes the field annotations = true
, the access log includes a 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
contains 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>
:
-- Output formatted string with indentationlocal function indentout(f, indent, fmt, ...) f:write(string.rep(" ", indent), string.format(fmt, ...))end-- Take first 8 characters in hexadecimal hashlocal function hexhash8(hash) return string.sub(util.hexhash(hash), 1, 8)end-- Dump formatted log to filefunction _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 if ai.type == "read" then indentout(out, indent, "%d: read %s@0x%x(%u): 0x%x(%u)\n", i, notes[i] or "", ai.address, ai.address, ai.read, ai.read) else assert(ai.type == "write", "unknown access type") indentout(out, indent, "%d: write %s@0x%x(%u): 0x%x(%u) -> 0x%x(%u)\n", i, notes[i] or "", ai.address, ai.address, ai.read, ai.read, ai.written, ai.written) end i = i + 1 end endend
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:
-- Load the Cartesi moduleslocal cartesi = require"cartesi"local util = require"cartesi.util"-- Instantiate machine from configurationlocal machine = cartesi.machine(require"config.nothing-to-do")-- Run machine until it haltslocal max_mcycle = 698031while not machine:read_iflags_H() and machine:read_mcycle() < max_mcycle do machine:run(max_mcycle)endassert(machine:read_mcycle() == max_mcycle, "Machine halted early!")-- Obtain state hash before stepmachine:update_merkle_tree()local step_log = machine:step{ annotations = true, proofs = true }-- Dump access log to screenio.stderr:write(string.format("\nContents of step %u access log:\n\n", max_mcycle))util.dump_log(step_log, io.stderr)
produces the output:
. / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESIContents of step 698031 access log:begin step hash 7196d4de 1: read iflags.H@0x1d0(464): 0x18(24) hash 7196d4de 2: read iflags.Y@0x1d0(464): 0x18(24) begin raise_interrupt_if_any hash 7196d4de 3: read mip@0x170(368): 0x0(0) hash 7196d4de 4: read mie@0x168(360): 0x8(8) end raise_interrupt_if_any begin fetch_insn hash 7196d4de 5: read pc@0x100(256): 0x80002fb0(2147495856) begin translate_virtual_address hash 7196d4de 6: read iflags.PRV@0x1d0(464): 0x18(24) hash 7196d4de 7: read mstatus@0x130(304): 0xa00001800(42949679104) end translate_virtual_address begin find_pma_entry hash 7196d4de 8: read pma.istart@0x800(2048): 0x800000f9(2147483897) hash 7196d4de 9: read pma.ilength@0x808(2056): 0x4000000(67108864) end find_pma_entry hash 7196d4de 10: read memory@0x80002fb0(2147495856): 0x7378300f6b023(2031360633384995) end fetch_insn begin sd hash 7196d4de 11: read x@0x68(104): 0x40008000(1073774592) hash 7196d4de 12: read x@0x78(120): 0x10100000000000a(72339069014638602) begin translate_virtual_address hash 7196d4de 13: read iflags.PRV@0x1d0(464): 0x18(24) hash 7196d4de 14: read mstatus@0x130(304): 0xa00001800(42949679104) end translate_virtual_address begin find_pma_entry hash 7196d4de 15: read pma.istart@0x800(2048): 0x800000f9(2147483897) hash 7196d4de 16: read pma.ilength@0x808(2056): 0x4000000(67108864) hash 7196d4de 17: read pma.istart@0x810(2064): 0x1069(4201) hash 7196d4de 18: read pma.ilength@0x818(2072): 0xf000(61440) hash 7196d4de 19: read pma.istart@0x820(2080): 0x80000000000002d9(9223372036854776537) hash 7196d4de 20: read pma.ilength@0x828(2088): 0x3c00000(62914560) hash 7196d4de 21: read pma.istart@0x830(2096): 0x4000841a(1073775642) hash 7196d4de 22: read pma.ilength@0x838(2104): 0x1000(4096) end find_pma_entry hash 7196d4de 23: write htif.tohost@0x40008000(1073774592): 0x10100000000000d(72339069014638605) -> 0x10100000000000a(72339069014638602) hash 366dbfde 24: write htif.fromhost@0x40008008(1073774600): 0x0(0) -> 0x101000000000000(72339069014638592) hash efe626a4 25: write pc@0x100(256): 0x80002fb0(2147495856) -> 0x80002fb4(2147495860) end sd hash bc88864d 26: read minstret@0x128(296): 0xaa6ae(698030) hash bc88864d 27: write minstret@0x128(296): 0xaa6ae(698030) -> 0xaa6af(698031) hash a89db020 28: read mcycle@0x120(288): 0xaa6af(698031) hash a89db020 29: write mcycle@0x120(288): 0xaa6af(698031) -> 0xaa6b0(698032)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, was hand-picked for illustration purposes.
The RISC-V instruction being executed, sd
, writes the 64-bit word 0x010100000000000a
to address 0x40008000
(access #23).
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.
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 this 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>)
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 following script illustrates the verification of a state transition.
-- Load the Cartesi moduleslocal cartesi = require"cartesi"local util = require"cartesi.util"-- Instantiate machine from configurationlocal machine = cartesi.machine(require"config.nothing-to-do")-- Run machine until it haltslocal max_mcycle = 698031while not machine:read_iflags_H() and machine:read_mcycle() < max_mcycle do machine:run(max_mcycle)endassert(machine:read_mcycle() == max_mcycle, "Machine halted early!")-- Obtain state hash before stepmachine:update_merkle_tree()local hash_before_step = machine:get_root_hash()-- Obtain access loglocal step_log = machine:step{ annotations = true, proofs = true }-- Obtain state hash after stepmachine:update_merkle_tree()local hash_after_step = machine:get_root_hash()-- Potentially mess with state access to cause a verification failureif #arg > 0 then local env = { cartesi = cartesi, step_log = step_log } local f = assert(load(arg[1], arg[1], "t", env)) f()end-- Verify step access logassert(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.
playground:~$ luapp5.3 verify-step.lua . / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESIState 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 #23
23: write htif.tohost@0x40008000(1073774592): 0x10100000000000d(72339069014638605) -> 0x10100000000000a(72339069014638602)
from 0x40008000
to 0x100
causes the program to reject the state transition proof:
playground:~$ luapp5.3 verify-step.lua 'step_log.accesses[23].address = 0x100' . / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESIluapp5.3: verify-step.lua:31: expected access 23 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–23 in the <access_log>
, a true Cartesi Machine would have written to address 0x40008000
(helpfully labelled 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:
playground:~$ luapp5.3 verify-step.lua 'step_log.accesses[23].written = 0x1234' . / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESIluapp5.3: verify-step.lua:32: word value written in access 23 does not match logstack traceback: [C]: in function 'assert' verify-step.lua:32: in main chunk [C]: in ?
Changing the value read also causes the proof to be rejected because it will not match the target hash:
playground:~$ luapp5.3 verify-step.lua 'step_log.accesses[23].read = 0x1234' . / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESIluapp5.3: verify-step.lua:32: word value before write access 23 does not match target hashstack traceback: [C]: in function 'assert' verify-step.lua:32: 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:
playground:~$ luapp5.3 verify-step.lua 'local access = step_log.accesses[23];access.read = 0x1234; access.proof.target_hash = cartesi.keccak(access.read);' . / \ / \\---/---\ /----\ \ X \ \----/ \---/---\ \ / CARTESIluapp5.3: verify-step.lua:32: word value before write access 23 fails proofstack traceback: [C]: in function 'assert' verify-step.lua:32: in main chunk [C]: in ?
In a nutshell, only valid state transitions are accepted by the cartesi.machine.verify_state_transition()
function.