Axiom · dark
Compiler and CLI
The target CLI contract covers building, proof analysis, assembly audit, target selection, and binary layout.
The Axiom compiler combines a compiler, SPARK-like proof analyzer, target checker, and binary writer.
Bootstrap policyBefore self-hosting, every compiler change is expected to inspect generated assembly/disassembly. A runtime PASS alone is not enough.
Common commands
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:17Target CLI options
| Option | Purpose |
|---|---|
build <file|module> | Run the full pipeline to an executable/object/image. |
check | Parse, semantic analysis, contracts, and proofs without emitting a binary. |
asm | Show compiler-generated assembly/canonical machine lowering. |
disasm <binary> | Disassemble the actual encoded output. |
explain | Explain a proof, range, lifetime, or effect result. |
--target <triple> | Choose target triple. |
--cpu <name> | Select concrete CPU capabilities. |
--emit ast|sir|tir|mir|asm|obj|elf|pe|raw | Persist a pipeline stage. |
-o <path> | Output path. |
--module-path <dir> | Add module search root. |
--proof-report <path> | Write proof obligations and discharged facts. |
--memory-report <path> | Write regions, bundle interference, peak RAM, and stack bounds. |
--effects-report <path> | Write inferred effects and parallel conflicts. |
--layout-report <path> | Write sections, symbols, addresses, and relocations. |
--deny-sus | Fail on every trusted/sus boundary. |
--list-sus | List assume/MMIO/external ABI boundaries. |
--no-color | Plain CI output. |
--diagnostic-format text|json | Human or machine-readable diagnostics. |
--verify-encoding | Decode emitted machine code and compare against MIR/relocations. |
--reproducible | Reject nondeterministic metadata and enforce reproducible output. |
The visible 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.