🚧 Under Active Development 🚧
Coverage is tracked by the owning PRDs and dated validation waypoints. Not production-ready.
Ahead-of-time Clef compiler producing native executables without managed runtime or garbage collection. Uses Clef Compiler Services (CCS) for type checking and semantic analysis, generates MLIR through Alex multi-targeting layer, produces native binaries via LLVM.
Lattice integration coordinates work across CCS, Composer, the VSCode and Neovim/Vim clients, grammar and helper repositories. This solution now includes CCS.Editor and the Lattice server, with a local HelloDimensionsProof editor demo. It shows dimensional hover, compiler diagnostics and expandable source obligations dispatched to cvc5. Compiler-branch reconciliation and the broader editor gates remain explicit in the integration design.
CCS architecture describes the compiler-owned facts that both lowering and editor queries consume. BAREWire and Fidelity.Platform supply contracts and target declarations used in that reasoning. Language requirements remain in the Clef specification.
Interactive compiler workbench and native REPL bridge is planned work alongside language completion. It starts with a bounded SageFS hosting evaluation, preserves Baker/Alex authority, and coordinates shared Lattice/MCP sessions, responsive design-time proof dispatch and native ORC execution. Its roadmap milestones do not assert an implemented adapter or JIT.
The sample counts and recent-change lists below retain their February 2026 dates; they are historical measurements, not results from the current tooling integration gates.
Proof composition and the Rocq toolchain records the design for automatically composing local, concurrent, distributed and device-level evidence. It identifies reusable Iris/Verdi-family foundations, their semantic integration requirements, the managed toolchain and the gates separating proposed coverage from demonstrated verification.
FPGA targeting and artifact verification is a dedicated roadmap for a Clef-fed Dynamatic fork, Colibri-centered circuit realization, direct VHDL-2008 output and an independently implemented VHDL-to-Rocq adapter. It shares admission and proof infrastructure with the existing compiler; its milestones distinguish planned circuit, mapped-netlist and bitstream verification from current evidence.
Working Samples: 3 of 16 console samples compile and execute correctly:
- ✅ 01_HelloWorldDirect (static strings, basic Console)
- ✅ 02_HelloWorldSaturated (mutable variables in loops, string interpolation)
- ✅ 03_HelloWorldHalfCurried (pipe operators, function values)
Recent Achievements:
- VarRef SSA Auto-Loading: Mutable variables used as memref indices now auto-load values compositionally
- CCS Contract Compliance: NativeStr.fromPointer honors substring extraction via allocate + memcpy
- Compositional Patterns: Element/Pattern/Witness stratification validated with cross-discipline composition
Known Limitations:
- 13 of 16 samples fail compilation (closure capture, higher-order functions, complex control flow)
- Managed mutability limited to local variables in simple loops
- Partial escape analysis (closure capture detection works, mutable lifetime integration pending)
- Generic instantiation and SRTP resolution issues remain
See: docs/PRDs/README.md for full feature roadmap and status.
CCS constructs the typed graph and Baker elaborates/saturates its computation and relationships. Composer consumes that graph through Alex and realizes the selected target. The pipeline overview is the current source map; older pass counts and FCS typed-tree-overlay diagrams are historical.
Clef source + project/library/platform inputs
-> CCS checking and typed PSG construction
-> Baker recipes / saturation / owning admission and obligation passes
-> Composer source-diagnostic and target gates
-> Alex ctx pull through graph/codata, coeffects and the Huet zipper
Elements -> Patterns -> Witnesses
admitted physical operations + required graph correspondence
-> declaration collection and bounded correspondence checks
-> selected backend
ELF: mlir-opt -> mlir-translate -> opt (target bitcode)
-> ld.lld (LLVM code generation and linking)
-> native artifact and its execution/verification gates
The direct LLVM/LLD backend invokes neither Clang nor a
separate llc. Native console deployment can use libc, startup objects and a
loader; other deployment modes retain their own runtime requirements. Avoiding
the .NET runtime does not imply zero native runtime dependencies.
- Baker settles; Alex witnesses. Source algorithms, evaluation relationships, captures, residence, layout and proof premises belong in their owning CCS/Baker stages. Missing semantics cannot be supplied by a late emitter or F#/C surrogate.
- Context pull preserves position. The Huet zipper holds focus, path and graph.
Program facts come from graph nodes/codata; current
TransferCoeffectsholds platform reads and target selection. Emission accumulators, scopes and visited sets are separate bookkeeping, not a semantic reconstruction layer. - Compose the physical vocabulary. Witnesses observe through
ctxand invoke Patterns, which compose Elements.module internalrestricts assembly visibility; it does not prohibit Witness-to-Element access within the Composer assembly. There is no correctness-bearing line-count limit for a Witness or Pattern. - Describe actual traversal. Registered witnesses are combined in one
post-order traversal with scope-owned callbacks. This is not independent parallel
traversal per witness.
Values.fsderives SSA names from node/role ordinals and block arguments; CCS does not run an SSA-preassignment pass. - Thin emission retains admitted structure. Structured operations and regions are compatible with flat/thin witnessing. Alex is target-aware; the admission key is expression family × platform/backend profile × witness form.
- Evidence has a scope. Graph tests, MLIR verification, solver answers and native oracles establish different boundaries. M-01 still owns planned general admission, target-path reconciliation and correlated fact/proof transport. Existing bounded checks do not establish complete coverage.
See Alex Architecture for the current implementation and Thin Middle End for its semantic boundary.
CCS's native type algebra retains Clef dimensions and declared representation requirements. Integer widths, layouts, callable environments and lifetimes must come from their owning language/platform contracts, not a host-language type or a convenient machine-width default. Alex reads those facts when selecting physical carriers.
Current CPU string patterns use byte memrefs, while settled static strings can share a BAREWire pool with exact offsets, bytes and obligation anchors. A memref is an MLIR carrier, not the source-language definition of a string or a universal promise about descriptor size. Closure, sequence and aggregate carriers likewise have separately admitted layout and residence requirements. The Alex component suite records the boundaries tested.
Internal TNativePtr plumbing is not a user-denotable general pointer API. The
FFI contract and
C-01 govern typed foreign boundaries and remaining
representation work. Earlier NativePtr examples or MLIR-shaped intrinsic
signatures are not Clef surface declarations.
The direct HelloWorld sample exercises static output through the ordinary pipeline:
module Examples.HelloWorldDirect
[<EntryPoint>]
let main argv =
Console.write "Hello, World!"
Console.writeln ""
0Its project selects a Fidelity.Platform dependency and CPU target. Use that declared profile when reproducing the sample; source syntax alone does not establish a target.
dotnet build src/Composer.fsproj
src/bin/Debug/net10.0/Composer compile samples/console/FidelityHelloWorld/01_HelloWorldDirect/HelloWorld.fidproj -k
samples/console/FidelityHelloWorld/01_HelloWorldDirect/targets/helloworldFor a new .fidproj, copy an existing project for the intended platform and
update its inputs. CPU projects use target = "cpu"; output_kind selects the
deployment/runtime contract rather than the compiler's semantic model. Cross
runtime/link inputs are documented in LLVM Backend.
Coordinate builds when Composer and CCS are shared with another task. The regression runner builds the compiler and runs sample/native-output cases sequentially:
cd tests/regression
dotnet fsi Runner.fsx
dotnet fsi Runner.fsx -- --verbose
dotnet fsi Runner.fsx -- --sample 02_HelloWorldSaturated--parallel is unsupported. Owning source admission,
Alex component, proof and native gates supplement
these regressions. A subset or a historical sample count is not a fresh full-suite
result.
With -k, retained artifacts in the sample's targets/intermediates/ include:
| Artifact | Boundary |
|---|---|
01_psg0.json |
Initial typed PSG/reachability view. |
02_intrinsic_recipes.json, 03_psg1.json |
Intrinsic elaboration and fold-in. |
04_saturation_recipes.json, 05_psg2.json |
Baker recipes and final graph view. |
07_output.mlir |
MLIR retained by the orchestrator. |
08_after_declaration_collection.mlir |
Post-witness declaration collection. |
09_obligations.mlir |
Optional emitted SMT module; not a discharge verdict. |
10_output.mlir |
Final middle-end serialization. |
08_output.ll and associated bitcode |
LLVM backend handoff. |
The old 06_coeffects.json identifier remains reserved in PhaseConfig; its name
does not establish an active separate Composer analysis pass. The obsolete four
middle-end pass sequence and its artifact names are not current output contracts.
src/
├── CLI/ Command-line interface
├── Core/ Pipeline/target orchestration and backend contracts
├── FrontEnd/ Calls CCS project checking
├── CCS.Editor/ Versioned compiler projection and proof dispatch
├── Lattice.Server/ Editor transport and scheduling
├── MiddleEnd/
│ ├── MLIRGeneration.fs Alex ingress, validation and serialization
│ └── Alex/
│ ├── Dialects/ Physical operations/types and serialization
│ ├── CodeGeneration/ Type and callable-symbol mapping
│ ├── Traversal/ Huet context, derived values, traversal and coverage
│ ├── XParsec/ Graph observation combinators
│ ├── Elements/ Atomic physical operations
│ ├── Patterns/ Composed admitted forms
│ ├── Witnesses/ Context-pulled graph observation
│ └── Pipeline/ Post-witness declaration collection
└── BackEnd/ Selected target realization and artifacts
Baker, graph construction and owning semantic analyses are in the companion
Clef repository, not an additional
Composer PSGElaboration pipeline.
The PRD index records current feature/target scope and acceptance evidence. Language Coverage Waypoints records coordinated revisions, remaining failures and native oracles. Existing CPU, MCU and other backend implementations must be distinguished from complete language/target admission; a portable MLIR vocabulary alone does not implement a new target.
Relevant workstreams include Cortex-M, FPGA, WebAssembly, JavaScript, M-01 dialect admission, and the interactive workbench. Follow their own status records; the February snapshot above is preserved as history.
| Document | Content |
|---|---|
| Pipeline overview | Current CCS/Baker/Alex/backend ownership and source map. |
| Baker contract | Construction, recipes, saturation and graph relationships. |
| Alex overview | Context pull, positional traversal, physical expression and evidence limits. |
| CCS architecture | Semantic service and graph facts. |
| Lattice integration | Repository map, editor transport and proof-view gates. |
| Workbench | Planned resident compiler and native REPL bridge. |
| LLVM backend | Direct LLVM/LLD realization and native runtime inputs. |
| PRD index | Feature statuses with scoped evidence. |
| C/F checkpoint | Verified September 26 scope, remaining work by C/F owner, and estimate provenance. |
Achievement: Local mutable variables in simple loops now work via TMemRef auto-loading.
What Works:
let mutable pos = 0→memref.alloca() : memref<1xindex>- Mutable variables as memref indices (auto-load value before use)
- Mutable variables in loop conditions (while, for)
- String operations honoring CCS contracts (substring extraction)
What Doesn't Work:
- Mutable variables captured in closures (closure detection exists, allocation strategy integration pending)
- Mutable variables passed across function boundaries (return/byref escape detection needed)
- Higher-order functions with mutable state
- Complex control flow with escaping mutables
Architectural Pattern Established: Compositional auto-loading via type-driven discrimination (Rule 9 in managed mutability architecture principles).
See: Serena memory managed_mutability_feb2026_milestone for complete details.
Areas of interest:
- MLIR dialect design for novel hardware targets
- Memory optimization patterns (escape analysis, loop unrolling)
- Nanopass transformations for advanced Clef features
- Closure capture and higher-order function support
- Graph-resident obligations, cvc5 dispatch and the planned proof-composition service
Dual-licensed under Apache License 2.0 and Commercial License. See Commercial.md for commercial use. Patent notice: U.S. Patent Application No. 63/786,247 "System and Method for Zero-Copy Inter-Process Communication Using BARE Protocol". See PATENTS.md.
- Don Syme and F# contributors: Language and compiler heritage used by the bootstrap implementation
- Clef contributors: Native language, graph and compiler development
- MLIR Community: Multi-level IR infrastructure
- LLVM Project: Robust code generation
- Nanopass Framework: Compiler architecture principles
- Triton-CPU: MLIR-based compilation patterns
- MLKit: Flat closure representation patterns