As stated in the question, I'm not certain about
how the integer part of the elements in the untyped_mmios array in devices.camkes are
You are right that the numbers represent the size of the untyped mmios being created,
0xF1000000:24 -> [0xF1000000, 0xF1000000 + 0x1000000).
In the example you gave, the four elements are defining a single ram region, but because
the objects being created are seL4 untypeds that the vmm uses to construct the RAM device,
there is an seL4 constraint that untyped objects can't be larger than their
So camkes wouldn't be able to create an untyped object defined as:
"0xF1000000:27" as this object would only have an alignment of 2^24 and seL4
would reject the retype invocation.
Hope this answers your question.