Hola.
Pueden definirse directamente en Actions.v (por ejemplo).
Si algún predicado de los que se precisan no te queda claro, avisame.
En particular va_mapped_to_ma expresa que la dirección vitual va está mapeada en la memoria a una dirección de máquina ma para un OS en un estado dado.
Saludos, Carlos