Aura IoT Plugin

IoT/MMIO-oriented Nexus integration with verification-aware capability and register checks.

Scope

IoT/MMIO-oriented Nexus integration with verification-aware capability and register checks.

• The repository contains a dedicated aura-plugin-iot workspace component.
• Plugin diagnostics can carry verification-oriented offset/bitmask information where the configured model supports it.
• Hardware behavior and trusted native/platform boundaries remain outside a universal proof claim.

Enable

plugins = [
  { name = "aura-iot", trusted = true },
]

Marking a plugin as trusted places its trusted behavior inside the project trust boundary; it does not automatically prove external hardware or native libraries.

Example

import aura::hw

cell main() ->:
    val cap = hw.open("SPI_CTRL")
    val _ = hw.write_u32(cap, 0, 0x3FF)

Editor feedback

Where verification/plugin diagnostics are produced, aura-lsp can expose plugin-attributed information to Aura-aware clients such as Sentinel. Exact diagnostics depend on the current plugin implementation and configured project model.