Leyendo el paper, la precondición de Read se define de la siguiente manera:
Sin embargo, en el paper dice:
The precondition of the action read va requires that va is accessible by the active OS, that there exists a machine address ma to which va is mapped, that the active OS is running and that the page indexed by the machine address ma is readable/writable.
La parte en negrita nos da a entender que el predicado os_accessible debería encargarse de verificar que el OS activo es quien tiene acceso a 'va' y no simplemente que algún OS tenga acceso a la misma (lo que se haría simplemente verificando con ctxt_vadd_accessible), pero no es posible sin que el predicado os_accessible reciba el estado actual.
La duda concreta es: ¿es un error del texto decir que tiene que ser accesible por el OS activo ó el predicado os_accessible debería recibir el estado actual para poder hacer la verificación?
Nosotros verificamos esto en va_mapped_to_ma, pero tiene sentido que eso lo verificara os_accessible, tal cual está dicho en el texto.