Right now all mappings of memory regions require a virtual address given by the user. Most of the time, especially in conjunction with setvar_vaddr, you as the user might not really care about the specific virtual address as long as it is valid.
I haven't thought about it too much but I don't see a reason to make it so that if the vaddr attribute is missing then Microkit auto-allocates a virtual address, since it knows about the program image and other mappings, it knows the whole layout of the address space and therefore can figure out a valid one.