Architecture

Architecture

Canonical in-repo document: ARCHITECTURE.md.

The workspace

All live compiler code is in crates/ — a 15-member Cargo workspace with a virtual manifest (no [package] at the root).

Crate	Role
my-lang	The real compiler: lexer, parser.rs (~100 KB), checker.rs (~73 KB), interpreter, stdlib.rs (~68 KB), and qtt_bridge.rs
my-qtt	The QTT kernel — the Rust port of the Coq-verified check (R5) and aff_type_dec (R5b)
my-hir → my-mir → my-llvm	Lowering pipeline to native code (LLVM 21; excluded from default build)
my-cli	The my binary
my-fmt, my-lint, my-lsp, my-dap, my-debug, my-pkg, my-test	Tooling, at varying maturity
my-ai	AI-assist surface — mock operations only
my-parser	⚠️ A 58-line stub whose parse functions return Ok(()) unconditionally. The real parser is in my-lang.

Pipeline

source.my
   │  lexer          crates/my-lang/src/lexer.rs
   ▼
 tokens
   │  parser         crates/my-lang/src/parser.rs
   ▼
  AST
   │  checker        crates/my-lang/src/checker.rs
   │  + QTT kernel   crates/my-qtt/          ← the verified core
   ▼
 typed AST ──► interpreter        (crates/my-lang/src/interpreter.rs)
   │
   │  lowering
   ▼
  HIR ──► MIR ──► LLVM IR ──► native   (x86_64, aarch64)

Where the proofs sit

proofs/
├── STATUS.md                    ← authoritative proof-status registry
├── verification/coq/solo-core/  ← 13 .v files, ~8.7 kLOC
│     SoloCore.v      the functor SoloCoreF (M : ORDERED_SEMIRING)
│     ResourceAlgebra.v  Module Type SEMIRING / ORDERED_SEMIRING
│     Tropical.v      min-plus instance (infinite carrier)
│     SessionPi.v     session-typed π-calculus (~3.5 kLOC)
└── verification/idris/solo-core/  ← 8 .idr files, ~2.5 kLOC (twin track)

crates/my-qtt is the hand-port of the Coq check; qtt_bridge.rs wires it into the real checker. Keeping those in correspondence is the open #typeck obligation.

Trees that are not the compiler

Two significant traps for readers and greps:

• Root src/ and lib/ — ~7,300 LOC of stale, divergent, unbuilt duplicates of crates/my-lang/src/ and crates/my-lang/lib/. No manifest references them. Some older documentation describes these as the compiler. Tracked as debt C-1.
• dialects/solo/compiler — outside the workspace; every stage is TODO(#parser) / TODO(#typeck) / TODO(#codegen). This is the artefact the verified check_correct spec exists for, but nothing builds it yet.

Also outside the workspace: _exploratory/, playground/hives/, frontier-practices/, my-ssg/, fuzz/.

Machine-readable layer

.machine_readable/ carries the state a tool should read rather than infer:

• 6a2/STATE.a2ml — authoritative project state, proof status, milestones, blockers, security posture
• 6a2/META.a2ml — ADRs and development practices
• 6a2/ECOSYSTEM.a2ml — sibling/upstream repositories
• contractiles/ — Mustfile/Trustfile/Intentfile invariant contracts
• self-validating/my-lang-metadata.k9.ncl — K9/Nickel invariants

Known inconsistencies in this layer are tracked as M-1–M-5 in DEBT.md.