Phase 0, Section 5: Implementation Infrastructure

Phase 0: Foundation — establishing the formal core calculus. Section 5 of 5: Implementation Infrastructure.

1. What this section commits to

The engineering plan to actually build what Sections 1–4 specify. Concretely:

• The three-language stack with specific tools, library choices, and versions.
• The repository layout, build orchestration, and FFI boundaries.
• Phase 0 deliverables and the exit criteria that mark Phase 0 complete.
• Phase 1 entry conditions — what has to be true before the shape-typed end-to-end work starts.

This is the section where decisions become buildable. After Section 5, the project either has an executable plan or it doesn't.

2. The three-language stack

Confirmed earlier: OCaml for the compiler, Rust for the runtime, Lean 4 for verification. Specific commitments:

2.1 OCaml — compiler frontend

• Version: OCaml 5.1 or later. The 5.x line for effect handlers (Phase 2 substrate); not strictly needed in Phase 0 but committing now avoids a migration later.
• Build system: Dune (3.x).
• Package manager: opam.
• Key libraries:
  • menhir — parser generator.
  • sedlex — Unicode-aware lexing.
  • z3 (ocaml-z3 bindings) — SMT discharge.
  • ppx_deriving, ppx_compare — ADT boilerplate.
  • alcotest — testing.
  • cmdliner — CLI argument parsing for the compiler driver.
• Code style: functional core, imperative shell. Pattern matching on IR nodes, no inheritance. The flight-sim DSL pipeline is the structural template.

2.2 Rust — runtime

• Version: Rust stable (1.78 or later).
• Build system: Cargo.
• Edition: 2021.
• Key crates (Phase 0 minimal):
  • libloading — dlopen the compiled .so.
  • bytemuck — safe casts for raw tensor memory.
  • thiserror — error types.
  • criterion — benchmarking (deferred to later phases but structurally present).
• Phase 0 scope: opaque tensor handles, a heap that allocates and tracks them, and a function to invoke a compiled artifact. Nothing else. CUDA, NCCL, and device management are Phase 3+ concerns.

2.3 Lean 4 — verification

• Version: Lean 4.7 or later.
• Build system: Lake.
• Toolchain pinning: lean-toolchain file in the verification subdirectory.
• Key dependencies:
  • mathlib4 — linear algebra foundations (eventually) and tactic library.
• Phase 0 scope: the type syntax, the typing judgment, the reduction relation, and the statements of subject reduction and progress. Proofs are deferred but the statements must type-check in Lean.

3. MLIR access: textual emission, subprocess invocation

A key engineering decision that simplifies the Phase 0 / Phase 1 implementation considerably.

3.1 The decision

The OCaml compiler does not call MLIR's C++ API directly. Instead:

1. The compiler builds its own typed IR in OCaml (ADTs, pattern matching).
2. It emits textual MLIR to a file or stdout.
3. It invokes the mlir-opt, mlir-translate, and llc binaries as subprocesses.
4. The final output is an LLVM-compiled shared object.

3.2 Why this works

• No FFI to C++. The flight-sim DSL pipeline already uses this pattern (OCaml emits LLVM IR text, llc consumes it). Same engineering effort, no new infrastructure.
• Debuggable. Textual MLIR can be inspected, diff'd, and hand-edited. Bug reports include the IR text directly.
• Decoupled from MLIR's API churn. MLIR's C++ API changes between versions; the textual format is more stable.
• Adequate for Phase 0 and Phase 1. Whole-program compilation through subprocess invocation is fine for ahead-of-time compilation. JIT compilation (Phase 2 onward, for AD's just-in-time gradient code generation) may eventually need direct API access; that can be added when needed.

3.3 The tradeoff

• Latency. Subprocess invocation costs milliseconds per compile. Acceptable for an AOT compiler; bad for JIT.
• No fine-grained control. Can't pass MLIR data structures around in OCaml. The compiler's internal IR is its own thing; MLIR is a serialization target.
• Pinned MLIR/LLVM version. The textual format and pass names depend on the LLVM/MLIR version. Pin to LLVM 18 (or the project's chosen baseline) and document the requirement.

3.4 Implementation outline

compiler/lib/mlir/
├── dialects.ml      — hardcoded knowledge of the dialects we emit (linalg, tensor, arith, func)
├── emitter.ml       — pretty-printer from internal IR to MLIR text
├── pipeline.ml      — subprocess invocations: mlir-opt --pass=... | mlir-translate --to=llvm | llc
└── tests/           — round-trip tests: emit, parse with mlir-opt, check structure

Pinning: LLVM_VERSION=18 in build configuration. Failure mode: if mlir-opt is missing or wrong version, the build fails at compile-time with a clear error.

4. Z3 access: OCaml bindings

Z3 has well-maintained OCaml bindings (ocaml-z3). These are direct bindings to the Z3 C API and are stable across Z3 minor versions.

4.1 The wrapper layer

A thin OCaml module wraps ocaml-z3 to:

• Convert internal Presburger expressions to Z3 ASTs.
• Convert internal predicates to Z3 boolean expressions.
• Manage Z3 contexts (one per type-checking session, recycled between unrelated obligations).
• Cache results by (context-hash, obligation-hash).
• Enforce the 2-second timeout from Section 2 §14.
• Surface counterexamples for failed obligations.

4.2 Implementation outline

compiler/lib/smt/
├── presburger.ml    — internal Presburger expression representation
├── z3_wrapper.ml    — translation to Z3 + context management
├── obligation.ml    — type for SMT obligations (assumption set + goal)
├── cache.ml         — memoization of discharge results
└── tests/           — discharge tests on known-good and known-bad obligations

The discharge function has signature:

val discharge :
  context:Context.t ->
  assumptions:Predicate.t list ->
  goal:Predicate.t ->
  (Discharged | Refuted of counterexample | Timeout)

Three outcomes — proven, refuted with counterexample, or timeout — match the type-checker's three-way decision logic.

5. Repository layout

The project is a polyglot monorepo with three top-level subprojects (compiler, runtime, verification) and specification directories at the repository root (alongside code), matching the canonical documentation layout used in this program’s artifact set.

Documentation-only checkouts. Some repositories contain only the markdown specs (design-memos/, phase-0/, phase-1/, companions/, forward-tracks/, implementation-roadmap.md) with no compiler/ tree yet. Paths in Sections 1–5 refer to the same folder names; only the presence of the code subprojects differs.

ai-native-lang/
├── README.md
├── ROADMAP.md
├── LICENSE
├── Justfile                          — top-level build orchestration
│
├── design-memos/                     — six design-space memos
├── phase-0/                          — Phase 0 spec, sections 1–5
├── phase-1/                          — Phase 1 implementation spec (eight sections)
├── companions/                       — Phase 0 walkthroughs (non-normative)
├── forward-tracks/                   — constraints on Phase 1+ (non-normative)
├── implementation-roadmap.md         — phased roadmap (optional filename: ROADMAP.md)
├── decisions/                        — ADRs (Architecture Decision Records)
├── milestones.md                     — exit criteria per phase (optional)
│
├── compiler/                         — OCaml
│   ├── dune-project
│   ├── lib/
│   │   ├── ast/                      — surface AST after parsing
│   │   ├── ir/                       — typed core IR (post-elaboration)
│   │   ├── parser/                   — menhir + sedlex
│   │   ├── elab/                     — elaboration / bidirectional type checker
│   │   ├── smt/                      — Z3 wrapper (this doc §4)
│   │   ├── mlir/                     — MLIR textual emission (§3)
│   │   └── util/                     — error formatting, source locations
│   ├── bin/
│   │   └── compiler.ml               — driver: file in, .so out
│   └── test/
│       ├── unit/                     — per-module tests
│       ├── integration/              — end-to-end compile-and-run
│       └── fixtures/                 — small example programs
│
├── runtime/                          — Rust
│   ├── Cargo.toml
│   ├── src/
│   │   ├── lib.rs
│   │   ├── tensor.rs                 — opaque tensor handles
│   │   ├── heap.rs                   — handle-to-data map; allocator
│   │   ├── dispatch.rs               — invoke compiled .so entry points
│   │   └── ffi.rs                    — C ABI surface (for future host-language interop)
│   └── tests/
│
├── verification/                     — Lean 4
│   ├── lakefile.lean
│   ├── lean-toolchain
│   ├── Spec/
│   │   ├── Types.lean                — Section 1 grammar mechanized
│   │   ├── Operations.lean           — Section 2 typing rules
│   │   ├── Subtyping.lean            — Section 3 subtyping
│   │   ├── Semantics.lean            — Section 4 reduction
│   │   └── Soundness.lean            — Phase 0 Section 4 §7 (soundness) statements
│   └── Proofs/
│       └── README.md                 — proof work goes here in Phase 6
│
├── examples/                         — programs in the language
│   ├── README.md
│   ├── 01-add.kina                 — placeholder extension; surface is Phase 7
│   ├── 02-matmul.kina
│   └── 03-mlp-forward.kina
│
└── scripts/
    ├── setup.sh                      — install OCaml, Rust, Lean toolchains
    ├── build-all.sh
    ├── test-all.sh
    └── ci.sh

Notes on the layout:

• The .kina extension is a placeholder. Surface syntax is Phase 7. For Phase 0 / 1, the parser accepts an S-expression-style IR directly; user-friendly syntax comes later.
• decisions/ for ADRs (at repo root next to specs). Architecture Decision Records, one per major commitment. Each decision in this section gets one. The ADR format is the standard one (Context, Decision, Consequences) and the discipline is a compounding investment.
• No central package directory. Each language manages its own dependencies. Cross-language dependencies are via build artifacts (compiler produces .so; runtime consumes it), not via shared packages.

6. Build orchestration

A top-level Justfile (or Makefile; just is the modern equivalent and works on Linux/macOS/Windows). Targets:

just setup                  # install toolchains, fetch dependencies
just build-compiler         # cd compiler && dune build
just build-runtime          # cd runtime && cargo build
just build-verification     # cd verification && lake build
just build                  # all three
just test-compiler          # dune test
just test-runtime           # cargo test
just test-verification      # lake test (compile-checks Lean files)
just test                   # all three
just fmt                    # ocamlformat, rustfmt, lean fmt
just lint                   # warnings as errors per language
just ci                     # what CI runs

CI runs everything on every push. Initial CI is GitHub Actions or GitLab CI; the choice is downstream.

6.1 Cross-language testing

Two integration test patterns:

1. Compile-and-run. The compiler emits a .so; the Rust runtime loads it and runs a smoke-test program. Verifies the OCaml→LLVM→Rust pipeline end-to-end.
2. Spec-compliance. A small set of programs whose typing behavior is asserted in both the OCaml type-checker and the Lean 4 spec. If they disagree, one of them is wrong. (In Phase 0, this is just the type-formation rules; later phases will add operational tests.)

These tests live in compiler/test/integration/ and verification/Spec/Tests/ respectively.

7. FFI boundaries

The languages communicate through artifacts and well-defined interfaces, not direct foreign function calls. Specifically:

Phase 0 has no direct OCaml ↔ Rust FFI. The compiler produces files; the runtime consumes them. This keeps the languages decoupled and the testing simple. A future phase may add direct FFI (e.g., for embedding the runtime in a Python host or for JIT compilation) — that's a deliberate addition with its own ADR, not an organic accumulation.

8. Phase 0 deliverables

What "Phase 0 complete" means concretely. Five categories:

8.1 Specification (this document set)

• ✅ Section 1: Type System Foundation
• ✅ Section 2: Core Operation Set & Typing Rules
• ✅ Section 3: Subtyping and Coercion
• ✅ Section 4: Operational Semantics
• ✅ Section 5: Implementation Infrastructure (this document)

8.2 Repository

• Repository created with the layout from §5.
• README explaining the project.
• ROADMAP referencing the design memos.
• Initial ADRs for each of the major decisions made in Phase 0 (one per section's "Decisions, summarized" table).

8.3 Compiler stub (OCaml)

• Project skeleton with Dune.
• Parser that accepts a small S-expression IR for tensor expressions (no shape arithmetic yet).
• Pretty-printer for the AST.
• Stub type-checker that recognizes well-formed types but does not yet discharge SMT obligations.
• Stub MLIR emitter that produces syntactically-valid (but semantically-stubbed) MLIR text.
• Tests: at least one round-trip test (parse → print → parse) and at least one type-check test on a hand-written well-formed program.

Repository status (non-normative). The compiler/ subproject exceeds the stub bullets above in places (full parse → structural type formation → MLIR emission for multiple example programs; ppx_expect pipeline tests; golden MLIR snapshots). It still does not implement the normative SMT story from Section 2 §14 or the full §02 operation surface. For a maintained gap list versus Section 2, see decisions/phase-0-reference-implementation-status.md. Section 2 §19 points here from the normative document side.

8.4 Runtime stub (Rust)

• Project skeleton with Cargo.
• Tensor and Heap types with allocation, lookup, and basic introspection.
• A function to load a .so via libloading and invoke an entry point. (No real compiled artifact yet; smoke-tested with a hand-written shared library.)
• Tests: heap behavior, dlopen flow.

8.5 Verification stub (Lean 4)

• Project skeleton with Lake.
• Spec/Types.lean mechanizing the Section 1 grammar.
• Spec/Operations.lean mechanizing the Section 2 typing rules (statements only; no proofs).
• Spec/Semantics.lean mechanizing the Section 4 reduction relation.
• Spec/Soundness.lean containing the soundness theorem statements (Phase 0 Section 4 §7), marked as theorem ... := sorry (Lean's "TODO" mechanism).
• All Lean files type-check. The proofs being sorry is acceptable for Phase 0; the statements must compile.

8.6 Build and CI

• just build succeeds for all three subprojects.
• just test runs all three test suites.
• CI configured and passing on push.

9. Phase 0 exit criteria

Phase 0 is complete when all of the following are true:

1. The five specification documents are written, reviewed (by the author at least; ideally by a second reader), and committed.
2. The repository skeleton exists and the build orchestration works.
3. The compiler stub parses, type-formation-checks, and emits syntactically-valid MLIR for at least three example programs.
4. The runtime stub allocates tensor handles and successfully loads and invokes a hand-built shared library.
5. The Lean 4 specification compiles cleanly (with sorry placeholders for proofs).
6. CI runs green on the main branch.
7. The author is willing to commit to Phase 1 — i.e., the foundation feels right, not just complete. This last criterion is judgment, not metric.

The seventh criterion is the most important. Phase 0 is the place to discover that the framework is wrong; if the foundation feels wrong at the end of Phase 0, the right move is to revise, not to plow ahead. The roadmap document's §12 abandonment criteria apply here.

10. Phase 1 entry conditions

Phase 1 (the shape-typed core compiled end-to-end through MLIR to LLVM) starts when Phase 0 is complete and:

• The author has decided to continue (per §9 criterion 7).
• A Phase 1 milestone document exists, listing concrete deliverables (e.g., "matmul of [B, M, K] × [B, K, N] compiles to working LLVM and produces correct results within FP tolerance for B, M, K, N up to 4096"). The Phase 1 milestone is not this section's responsibility; it's the first work item of Phase 1.

After Phase 1 entry, the OCaml compiler grows from "stub" to "actually works for shape-typed programs." That's roughly a 4–6 month project per the roadmap.

11. New open issues from this section

Three implementation concerns to track:

1. MLIR/LLVM version pinning policy. The textual format and pass names depend on version. Pin to a specific LLVM release (suggest LLVM 18 as baseline) and document the upgrade process. Re-evaluate every 12 months.

2. OCaml-Z3 bindings stability. ocaml-z3 is well-maintained but has occasional version-skew issues with Z3 itself. Pin a known-good combination and verify on CI. Failure mode if it breaks: vendor a known-good version of the bindings.

3. Lake / mathlib4 churn. Lean 4 is a young and rapidly evolving ecosystem; mathlib4 changes daily. Pin a specific mathlib commit, not the latest. Plan to update mathlib pin every 1–2 months as a deliberate maintenance task.

These are mundane but real. Each warrants an ADR (see decisions/toolchain-pins.md for a consolidated record).

Type-checker engineering (carryovers from Section 3 open issues).

4. Polymorphic subtyping vs SMT. Checking Γ ⊢ T₁ <: T₂ when free shape variables are effectively universally quantified can stress Z3. Mitigation: benchmark early; if needed, structurally unify shape variables before invoking the implication query (Section 3 §11 #1).

5. Mutual recursion. Functions that mention each other through subtyping obligations require greatest fixed-point (coinductive) subtyping with cycle detection on the obligation graph — standard technique; document the algorithm in the bidirectional checker design.

6. Negated refinements. Implementations may canonicalize predicates to keep negation shallow for the solver; timeouts and fallback behavior align with the global SMT policy (Section 2 §14).

12. Decisions, summarized

13. Phase 0 closing notes

This is the final section of Phase 0. The five documents together specify:

• What the language is (Sections 1–4): typed tensor algebra with refinement-typed shapes, ten core operations (reduce includes a keepdims typing rule; Section 2), refinement subtyping, real-valued operational semantics.
• How to build it (Section 5): three-language polyglot stack, MLIR via textual emission, Z3 via OCaml bindings, monorepo layout, exit criteria.

If Sections 1–4 read as a contract and Section 5 reads as an engineering plan, Phase 0 has done its job. The next decision is whether to start Phase 1.

The roadmap document recommends pausing here — finishing Phase 0, then deciding whether to continue based on whether the foundation feels right. That recommendation stands. The Phase 0 spec exists either way; it is a durable artifact even if no further work happens.

End of Phase 0, Section 5. End of Phase 0.