Axiom · dark
Компілятор і CLI
Повний цільовий CLI контракт: build, analyze, asm/disassembly audit, target selection, proof reports і binary layout.
Axiom compiler — не лише parser + code generator. Він об’єднує роль компілятора, SPARK-подібного proof analyzer, частини GNAT tooling, target checker і binary writer.
Bootstrap policyДо self-hosting кожна компіляція під час розробки Axiom повинна перевіряти generated ASM/disassembly. Runtime PASS сам по собі недостатній.
Найчастіші команди
ShellCLI
axiom build src/main.ax --target x86_64-linux -o app
axiom check src/main.ax
axiom asm src/main.ax --target x86_64-linux
axiom disasm app
axiom explain src/main.ax --proof bounds --at 42:17Цільові опції
| Опція | Що робить |
|---|---|
build <file|module> | Повний pipeline до executable/object/image. |
check | Parse + semantic analysis + contracts/proofs без binary emission. |
asm | Показує compiler-generated assembly до encoding або canonical textual MIR lowering. |
disasm <binary> | Дизасемблює фактичний encoded output для обов’язкового audit. |
explain | Пояснює, чому proof пройшов/не пройшов, звідки взявся range/lifetime/effect. |
--target <triple> | Напр. x86_64-linux, aarch64-linux, aarch64-invariant-rpi5. |
--cpu <name> | Уточнює concrete CPU/capabilities. |
--emit ast|sir|tir|mir|asm|obj|elf|pe|raw | Зберігає вибраний етап pipeline. |
-o <path> | Output path. |
--module-path <dir> | Додає корінь пошуку Axiom modules. |
--proof-report <path> | Записує contracts, discharged obligations і unresolved diagnostics. |
--memory-report <path> | Regions, bundle interference, peak RAM, stack upper bounds. |
--effects-report <path> | Inferred read/write/sync effects і parallel conflicts. |
--layout-report <path> | Sections, symbols, addresses, relocations, ABI layout. |
--deny-sus | Будь-який trusted/sus boundary робить build помилкою. |
--list-sus | Друкує всі assume/MMIO/external-ABI/trusted ділянки. |
--no-color | Plain diagnostics для CI. |
--diagnostic-format text|json | Людський або machine-readable output. |
--verify-encoding | Після instruction encoding декодує machine code назад і звіряє MIR/relocations. |
--reproducible | Забороняє nondeterministic metadata/timestamps і перевіряє reproducible output. |
Pipeline, який варто бачити
source → lexer/parser → AST → semantic analysis → Semantic IR → semantic linking → Target IR → Machine IR → encoding → relocatable code/data → binary layout/link → ELF/PE/raw.
ASM audit
Shelltypical workflow
axiom build math.ax --target x86_64-linux -o math
axiom asm math.ax --target x86_64-linux > math.s
axiom disasm math > math.dis
axiom check math.ax --proof-report proof.txt --memory-report memory.txtНа bootstrap-етапі ви дивитеся, чи source function boundaries збереглися, чи ABI arguments лежать там, де очікується, чи немає зайвих moves, дивного stack frame або silent widening. До self-hosting aggressive inlining не є метою.