Axiom · dark

Targets, OS і hardware

Axiom відділяє семантику мови від конкретної ISA. Hardware capability з’являється пізно — у target model і стандартних модулях.

Ви не повинні писати драйвер дисплея на assembly лише тому, що це embedded. Assembly залишається для bring-up, reset vector, interrupt entry або інструкцій, які неможливо безпечно виразити Axiom.

GPIO/SPI driver на Axiom

Driver in AxiomAxiom

1display(Self):2    set_pixel(Self self, u16 x, u16 y, color c)3    flush(Self self) -> result<void, io_error>4END display56st7789:7    spi_bus bus8    gpio_pin dc9    gpio_pin reset1011    set_pixel(st7789 self, u16 x, u16 y, color c):12        require x < 24013        require y < 32014        // encode command/data into bounded transfer buffer15END st7789

Загальний display interface.

Concrete controller driver.

SPI capability — звичайний typed member.

GPIO pin для data/command.

Implementation методу.

Геометрична межа дисплея стає contract.

Друга межа. Після цього адресні обчислення можуть бути bounds-safe.

MMIO boundary

Низькорівневий модуль hardware.mmio може бути compiler-known privileged API. Він не видає програмі raw pointer; він видає typed register access, прив’язаний до target description. Саме тут можливий sus boundary, а решта драйвера знову звичайний аналізований Axiom.

Target description

Target задає ISA, ABI, endianness, register set, instruction capabilities, address spaces, privilege levels і hardware resources. Це дозволяє тому самому math.bit.crc32 або atomic API або lowering-нутися в реальну instruction, або дати compile-time capability error.

Assembly modules

.S/.asm можуть входити на object/link stage через symbols + relocations. Semantic analyzer ставиться до такого symbol як до trusted external contract: signature, clobbers, memory effects і pre/postconditions треба описати явно.

← Компілятор і CLI Практичні приклади →