Compiler Internals

Advanced topic. This page explains how CK turns source code into output and how its optimizer checks transformations. You do not need these details to write or run CK programs.

From source to artifact#

.ck source
  → lexer, parser, type checker, contracts
  → semantic MIR
  → mode- and consumer-specific KIR
  → verified O0–O3 optimization
  → Native LLVM / C source / WAT or WASM

The frontend produces stable diagnostics. Semantic MIR preserves evaluation order and possible checked failures. KIR adds explicit guards, effects, memory information, and proof-carrying facts for optimization.

Verified optimization#

At O0 the compiler constructs and verifies KIR without optional transforms. O1 adds control-flow simplification and scalar propagation. O2 adds effect-aware inlining and memory optimizations. O3 adds bounded specialization, loop work, unrolling, SLP, and supported Native fixed-width vectorization.

Transforms that need a proof are checked against the current KIR state. A speculative candidate is accepted as a complete verified state or leaves the previous state intact. Unknown safety facts cause conservative output.

ckc emit-mir kernel.ck
ckc emit-kir kernel.ck -O3 --print-facts --explain-optimization

The emit-kir inspection view is deterministic. Native inspection can select a specific consumer and CPU policy. C and WebAssembly currently consume verified scalar KIR; Native may use supported Vector KIR.

Profiles guide cost, not correctness#

CK workload profiles may influence the expected benefit of an optimization. They cannot establish a range, no-alias, alignment, bounds, or other safety fact. Profile identity is validated before use. Learn more in PGO & CPU Variants.

For implementation details, read the compiler architecture and optimizer reference.