Manual contradicts the tool on three x86 `irq` attributes (confirmed on Microkit 2.3.0)

[SuperTarantaMQ]

Manual contradicts the tool on three x86 irq attributes (confirmed on Microkit 2.3.0)

Component: tool/microkit + microkit_user_manual.pdf
Version: SDK 2.1.0, board x86_64_generic, config debug
Impact: following the manual produces a build error. The error messages do not point back
to the manual, so the reader has no way to know which of the two is right.

Summary

Section 7.1 of the user manual shipped inside the SDK describes the irq element attributes for
X86_64 IOAPIC interrupts. Three of them do not match what the microkit binary shipped in the
same SDK accepts.

Manual says	Tool accepts	Error when following the manual
level — "(optional) Whether the IRQ is level triggered (1) or edge triggered (0). Defaults to level (1)."	trigger — "level" / "edge"	Error: invalid attribute 'level' on element 'irq'
polarity — "(optional) Whether the line polarity is high (1) or low (0). Defaults to high (1)."	polarity — "high" / "low"	Error: polarity must be either 'low' or 'high' on element 'irq'
id — "The channel identifier. Must be at least 0 and less than 63."	id must be < 62	Error: id must be < 62 on element 'irq'

Reproduction

Three system descriptions, one attribute each. Any valid PD ELF works as program_image.

level instead of trigger:

<system>
  <protection_domain name="probe" priority="100" stack_size="0x4000">
    <program_image path="probe.elf"/>
    <irq id="0" ioapic="0" pin="11" vector="43" level="1" polarity="1"/>
  </protection_domain>
</system>

$ microkit min.system --board x86_64_generic --config debug --search-path elf -o out.img
Error: invalid attribute 'level' on element 'irq': min.system:5:5

Numeric polarity:

<irq id="0" ioapic="0" pin="11" vector="43" trigger="level" polarity="1"/>

Error: polarity must be either 'low' or 'high' on element 'irq': min.system:5:5

id="63", which the manual says is out of range only at 63 and above:

<irq id="63" pin="11" vector="43"/>

Error: id must be < 62 on element 'irq': min.system:5:5

What does work

<irq id="0" pin="11" vector="43" trigger="level" polarity="low"/>

and the shorter form, which defaults to ioapic="0", trigger="level", polarity="high":

<irq id="0" pin="11" vector="43"/>

Suggested fix

Update section 7.1 of the manual to document trigger ("level" / "edge") instead of level,
polarity as "high" / "low" instead of 1 / 0, and id < 62. Alternatively, accept the
documented spellings in the tool for backward compatibility.

A related note for the ARM/RISC-V section: on x86 the hardware line attribute is pin, not
irq. Using the ARM spelling irq="11" fails with

Error: ARM and RISC-V IRQs are not supported on x86 on element 'irq'

which is accurate but does not say what to write instead. Naming pin in that message would
save readers a trip through the manual.

[midnightveil]

Please don't use AI to contribute to Microkit.

These are minor documentation issues, not any kind of security bug. I'll try to fix these at some point before the next release.