12.2 ios_copy_bytes

The ios_copy_bytes copies a range of bytes between IO spaces.

It has the following prototype:

fun ios_copy_bytes = (int<32> from_ios, int<32> to_ios,
                      offset<uint<64>,B> from,
                      offset<uint<64>,B> to,
                      offset<uint<64>,B> size) void

Where from_ios is the origin IO space, i.e. the IO space from which bytes are to be copied.

to_ios is the destination IO space, i.e. the IO space to which bytes are to be copied.

from is a byte offset in from_ios with the beginning of the range to copy.

to is a byte offset in to_ios where the bytes will be copied.

size is a byte offset specifying the amount of data to be copied.