[REQUIREMENTS][PATCH v2 5/6] reqs: add guest vITS requirements

[Mykola Kvach <mykola_kvach@xxxxxxxx>]

Add requirements for Xen's guest-visible virtual ITS model.

The requirements cover virtual ITS instance creation, guest-visible ITS
identification and capability registers, guest ITS table base programming,
guest command queue processing, guest command validation, MAPD, MAPC,
MAPTI, MAPI, INT, CLEAR, DISCARD, MOVI, INV and INVALL command semantics,
command failure containment and virtual ITS MMIO access-width handling.

Signed-off-by: Mykola Kvach <mykola_kvach@xxxxxxxx>
---
 .../arm64/index.rst                           |   1 +
 .../arm64/its.rst                             | 382 ++++++++++++++++++
 2 files changed, 383 insertions(+)
 create mode 100644 
software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/its.rst

diff --git 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
index 263fc09..7896770 100644
--- 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
+++ 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
@@ -8,5 +8,6 @@ Arm64
 
    generic_timer
    gicv3
+   its
    tee
    viommu
diff --git 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/its.rst
 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/its.rst
new file mode 100644
index 0000000..5258588
--- /dev/null
+++ 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/its.rst
@@ -0,0 +1,382 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+vITS requirements
+=================
+
+The following requirements define Xen's virtual ITS model exposed to the
+hardware domain. Non-hardware domain virtual ITS exposure is outside the scope
+of this requirement group.
+
+Assumption of use
+^^^^^^^^^^^^^^^^^
+
+Guest software virtual ITS command use
+--------------------------------------
+
+`XenAoU~arm64~vits_command_use~1`
+
+Description:
+Guest software using Xen's virtual ITS interface shall be compatible with a
+virtual ITS model where the following guest ITS command behaviours have limited
+guest-visible semantics:
+
+ - ``MOVALL`` is not used to move virtual LPI mappings between collections.
+
+Rationale:
+Xen exposes a virtual ITS ABI, not a complete emulation of every physical ITS
+command side effect.
+
+Xen maintains virtual LPI translation state through Xen's virtual ITS device,
+collection and event mapping state. Guest software is assumed to use the
+supported virtual ITS command subset rather than relying on unsupported command
+semantics or on asynchronous physical ITS command-processing behaviour.
+
+Software Safety Requirements
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Guest ITS instance creation
+---------------------------
+
+`XenSSR~arm64~vits_creation~1`
+
+Description:
+Xen shall create a virtual ITS instance for the hardware domain when the
+hardware domain is configured to observe an ITS.
+
+Rationale:
+A virtual ITS provides the guest-visible ITS register interface and command
+processing model used by the hardware domain to configure LPI translation.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest ITS identification and capability registers
+-------------------------------------------------
+
+`XenSSR~arm64~vits_ident_and_cap_regs~1`
+
+Description:
+Xen shall expose guest ITS identification and capability registers according to
+the virtual ITS model implemented for the hardware domain. This shall include
+use of:
+
+ - ``GITS_IIDR``
+ - ``GITS_TYPER``
+ - ``GITS_PIDR2``
+
+Rationale:
+The hardware domain uses the virtual ITS identification and capability
+registers to discover the virtual ITS interface, DeviceID width, EventID width,
+table entry size and supported translation behaviour.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest ITS control and quiescent state
+-------------------------------------
+
+`XenSSR~arm64~vits_ctlr_and_quiescent_state~1`
+
+Description:
+Xen shall process guest ITS commands and report guest ITS quiescent state
+according to the guest-visible ``GITS_CTLR`` state.
+
+Rationale:
+``GITS_CTLR.Enable`` controls guest-visible ITS command processing.
+``GITS_CTLR.Quiescent`` reports whether virtual ITS command queue processing
+has completed.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest ITS table base programming
+--------------------------------
+
+`XenSSR~arm64~vits_table_base_programming~1`
+
+Description:
+Xen shall apply guest ITS command queue and translation table base updates only
+while the virtual ITS is disabled. This shall include use of:
+
+ - ``GITS_CBASER``
+ - ``GITS_BASER0``
+ - ``GITS_BASER1``
+
+Rationale:
+Guest ``GITS_CBASER`` and ``GITS_BASER<n>`` values define the guest command
+queue and guest translation tables consumed by the virtual ITS model.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest ITS table model
+---------------------
+
+`XenSSR~arm64~vits_table_model~1`
+
+Description:
+Xen shall expose guest Device and Collection tables supported by Xen's virtual
+ITS model. This shall include use of:
+
+ - ``GITS_BASER0`` for the guest Device table
+ - ``GITS_BASER1`` for the guest Collection table
+
+Rationale:
+The virtual ITS uses guest Device and Collection table state to translate guest
+DeviceID, EventID and CollectionID values.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest command queue processing
+------------------------------
+
+`XenSSR~arm64~vits_command_queue_processing~1`
+
+Description:
+Xen shall process guest ITS commands from the command queue range described by
+guest ``GITS_CBASER``, ``GITS_CREADR`` and ``GITS_CWRITER`` and advance
+``GITS_CREADR`` for handled commands.
+
+Rationale:
+The guest command queue is guest memory. The queue base and command queue
+pointers define which commands the hardware domain submitted for processing,
+and ``GITS_CREADR`` is the guest-visible command progress indicator.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest ITS command validation
+----------------------------
+
+`XenSSR~arm64~vits_command_validation~1`
+
+Description:
+Xen shall reject guest ITS commands whose fields do not identify valid virtual
+ITS state visible to the hardware domain before applying the requested mapping
+change.
+
+Rationale:
+Guest ITS commands contain guest-controlled DeviceID, EventID, CollectionID,
+virtual LPI and table fields. Xen validates these fields before applying
+mapping changes so that invalid commands do not create invalid virtual ITS
+translation state.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest MAPD device mapping
+-------------------------
+
+`XenSSR~arm64~vits_mapd_device_mapping~1`
+
+Description:
+Xen shall apply a guest ``MAPD`` command with the valid bit set when the
+DeviceID, ITT address and event range describe a guest Device table entry
+supported by the virtual ITS model.
+
+Rationale:
+``MAPD`` with the valid bit set establishes the guest DeviceID-to-ITT
+relationship used by later event translation.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest MAPD device mapping removal
+---------------------------------
+
+`XenSSR~arm64~vits_mapd_device_mapping_removal~1`
+
+Description:
+Xen shall apply a guest MAPD command with the valid bit clear by removing
+the virtual ITS device mapping and the event mappings associated with that
+DeviceID.
+
+Rationale:
+MAPD with the valid bit clear removes the guest DeviceID-to-ITT
+relationship. Event mappings that depend on the removed device mapping cannot
+remain active after the device mapping has been removed.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest MAPC command
+------------------
+
+`XenSSR~arm64~vits_mapc_command~1`
+
+Description:
+Xen shall apply a guest ``MAPC`` command when the CollectionID is valid and the
+target Redistributor maps to a vCPU of the same hardware domain.
+
+Rationale:
+A collection selects the target vCPU for translated LPIs.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest MAPTI and MAPI commands
+-----------------------------
+
+`XenSSR~arm64~vits_mapti_and_mapi_commands~1`
+
+Description:
+Xen shall apply guest ``MAPTI`` or ``MAPI`` commands when the DeviceID,
+EventID, CollectionID and virtual LPI are valid for the hardware domain.
+
+Rationale:
+``MAPTI`` and ``MAPI`` create the guest event-to-virtual-LPI mapping used by
+later event delivery.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest INT command
+-----------------
+
+`XenSSR~arm64~vits_int_command~1`
+
+Description:
+Xen shall inject a guest ``INT`` command as the virtual LPI selected by the
+command's valid DeviceID and EventID translation.
+
+Rationale:
+``INT`` requests delivery of a translated guest ITS event.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest CLEAR command
+-------------------
+
+`XenSSR~arm64~vits_clear_command~1`
+
+Description:
+Xen shall apply a guest ``CLEAR`` command to the pending state of the virtual
+LPI selected by the command's DeviceID and EventID translation.
+
+Rationale:
+``CLEAR`` removes pending state for a translated LPI.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest DISCARD command
+---------------------
+
+`XenSSR~arm64~vits_discard_command~1`
+
+Description:
+Xen shall apply a guest ``DISCARD`` command by removing the virtual ITS mapping
+for the command's DeviceID and EventID.
+
+Rationale:
+``DISCARD`` makes the selected event unmapped in the guest ITS model and
+removes the associated virtual LPI state from the active event mapping.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest MOVI command
+------------------
+
+`XenSSR~arm64~vits_movi_command~1`
+
+Description:
+Xen shall apply a guest ``MOVI`` command to an existing mapped event when the
+destination CollectionID is valid for the same hardware domain.
+
+Rationale:
+``MOVI`` changes the collection target for a translated event.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest LPI property invalidation
+-------------------------------
+
+`XenSSR~arm64~vits_lpi_property_invalidation~1`
+
+Description:
+Xen shall apply guest LPI property-table changes to virtual LPIs selected by
+guest ``INV`` and ``INVALL`` commands. This shall include use of:
+
+ - ``INV``
+ - ``INVALL``
+
+Rationale:
+The guest LPI property table is the guest-visible source of LPI enable and
+priority state. ``INV`` refreshes one translated LPI and ``INVALL`` refreshes
+LPIs targeted to a selected collection.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest ITS MMIO access width
+---------------------------
+
+`XenSSR~arm64~vits_mmio_access_width~1`
+
+Description:
+Xen shall apply a guest ITS MMIO access to an implemented virtual ITS register
+only when the access width is supported by that register.
+
+Rationale:
+The virtual ITS MMIO interface has register-specific access widths. Xen uses
+the target register definition to decode guest accesses so that unsupported
+byte, halfword or unsupported-width accesses do not update implemented virtual
+ITS register state incorrectly.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
-- 
2.43.0