|
| 1 | +<!-- SPDX-License-Identifier: CC-BY-SA-4.0 --> |
| 2 | +<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
1 | 4 | # Architecture |
2 | 5 |
|
3 | 6 | ## Overview |
4 | 7 |
|
5 | | -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. |
| 8 | +my-lang is a Rust-implemented language with a mechanised proof core. |
| 9 | +The repository is a Cargo workspace plus proof, dialect, and |
| 10 | +conformance trees. This file describes the layout as it actually is; |
| 11 | +for the authoritative state of the proofs, see `proofs/STATUS.md` |
| 12 | +(that registry wins over any other prose, including this file). |
| 13 | + |
| 14 | +## The dialect containment hierarchy |
6 | 15 |
|
7 | | -## Directory Structure |
| 16 | +The three real dialects are **nested subsets, not parallel languages**: |
8 | 17 |
|
9 | 18 | ``` |
10 | | -. |
11 | | -├── src/ # Source code |
12 | | -├── tests/ # Test suites |
13 | | -├── docs/ # Documentation |
14 | | -├── scripts/ # Utility scripts |
15 | | -├── config/ # Configuration files |
16 | | -├── LICENSE # License file |
17 | | -├── LICENSES/ # Full license texts |
18 | | -└── README.adoc # Project documentation |
| 19 | +Solo ⊂ Duet ⊂ Ensemble |
19 | 20 | ``` |
20 | 21 |
|
21 | | -## Design Principles |
| 22 | +- **Solo** — the innermost kernel. |
| 23 | +- **Duet** — everything in Solo plus more; mechanised as |
| 24 | + "ensemble restricted to 2-party by projection" (S2 track). |
| 25 | +- **Ensemble** — the full language (session-typed π-calculus core, |
| 26 | + S1 track). |
| 27 | +- **Me** — not a fourth layer: an on-the-fly projector that cuts the |
| 28 | + hierarchy at a chosen point. Its Rust scaffolding is sidelined in |
| 29 | + `_exploratory/me-scaffolding/` (see `SIDELINED.adoc` there) and is |
| 30 | + **not** part of the active workspace. |
22 | 31 |
|
23 | | -- **Separation of Concerns**: Each module has a single responsibility |
24 | | -- **Testability**: Code is written to be easily testable |
25 | | -- **Documentation**: All public APIs are documented |
26 | | -- **Configuration**: Environment-specific settings are externalized |
| 32 | +Audits must grade the layered stack, not three separate compilers: a |
| 33 | +broken Solo breaks Duet and Ensemble by transitivity. |
27 | 34 |
|
28 | | -## Dependencies |
| 35 | +## Directory structure |
29 | 36 |
|
30 | | -- External dependencies are minimized and clearly declared |
31 | | -- Version pinning is used for reproducibility |
| 37 | +``` |
| 38 | +. |
| 39 | +├── crates/ # Cargo workspace (15 members) |
| 40 | +│ ├── my-lang/ # core: lexer/parser/checker (largest crate) |
| 41 | +│ ├── my-cli/ # `my` binary |
| 42 | +│ ├── my-parser/ # parser scaffolding |
| 43 | +│ ├── my-hir/ # high-level IR |
| 44 | +│ ├── my-mir/ # mid-level IR |
| 45 | +│ ├── my-qtt/ # QTT verified-core checker (faithful port of |
| 46 | +│ │ # the Coq R5 `check` / R5b `aff_type_dec`) |
| 47 | +│ ├── my-llvm/ # LLVM codegen (needs system LLVM 21; excluded |
| 48 | +│ │ # from coverage CI for hermeticity) |
| 49 | +│ ├── my-lsp/ # language server |
| 50 | +│ ├── my-dap/ # debug adapter |
| 51 | +│ ├── my-debug/ # debugging support |
| 52 | +│ ├── my-fmt/ # formatter |
| 53 | +│ ├── my-lint/ # linter |
| 54 | +│ ├── my-test/ # test harness |
| 55 | +│ ├── my-pkg/ # package manager |
| 56 | +│ └── my-ai/ # AI integration |
| 57 | +├── proofs/ # Mechanised core — Coq (solo-core, SessionPi) |
| 58 | +│ # + Idris2 tracks; STATUS.md is the registry |
| 59 | +├── dialects/ # solo/ and duet/ compilers + examples |
| 60 | +├── _exploratory/ # sidelined scaffolding (me-scaffolding/) |
| 61 | +├── conformance/ # impl ⇄ verified-spec differential tests |
| 62 | +├── spec/ # language specification |
| 63 | +├── grammar.ebnf # surface grammar |
| 64 | +├── examples/ # example programs |
| 65 | +├── playground/ # demo playground (+ hives/) |
| 66 | +├── my-ssg/ # site generator input |
| 67 | +├── vscode-extension/ # editor support |
| 68 | +├── docs/ # documentation (published via Ddraig SSG) |
| 69 | +├── LICENSE # MPL-2.0 (code); CC-BY-SA-4.0 for docs |
| 70 | +└── LICENSES/ # full licence texts (REUSE layout) |
| 71 | +``` |
32 | 72 |
|
33 | | -## Security Considerations |
| 73 | +## CI gates |
34 | 74 |
|
35 | | -- Sensitive data is never committed to the repository |
36 | | -- Secrets are managed through environment variables or secure vaults |
37 | | -- Regular dependency audits are performed |
| 75 | +- `proofs.yml` — machine-checks the Coq solo-core and asserts the |
| 76 | + soundness theorems, the usage-walk checker (R5/R5b), the me→solo |
| 77 | + elaboration (M1), the session-π core (S1.x), and the |
| 78 | + duet-by-projection results (S2) are **axiom-free** |
| 79 | + (`Print Assumptions` must report "Closed under the global context"). |
| 80 | +- `coverage.yml` — cargo-llvm-cov over the workspace excluding |
| 81 | + `my-llvm`, with an enforced line-coverage floor. |
| 82 | +- `checker-scaling.yml` — checker performance scaling gate. |
| 83 | +- `codeql.yml`, `hypatia-scan.yml`, `secret-scanner.yml`, |
| 84 | + `scorecard.yml`, `cflite_*.yml` — security/fuzzing gates. |
| 85 | +- `governance.yml` — estate policy via hyperpolymath/standards |
| 86 | + reusable workflows. |
| 87 | +- `pages.yml` — docs deployment via Ddraig SSG. |
38 | 88 |
|
39 | | -## Maintainability |
| 89 | +## Design principles |
40 | 90 |
|
41 | | -- Code follows consistent style guidelines |
42 | | -- Pull requests require review and CI checks |
43 | | -- Issues and discussions are tracked transparently |
| 91 | +- **No proof hole is ever described as "proved"** — statement-only |
| 92 | + theorems are tracked obligations (`proofs/STATUS.md` vocabulary). |
| 93 | +- **Layered dialects** — features land in the innermost layer that can |
| 94 | + express them; outer layers add, never fork. |
| 95 | +- **Hermetic CI** — the LLVM back end is isolated so every other gate |
| 96 | + runs without a system toolchain. |
44 | 97 |
|
45 | 98 | --- |
46 | 99 |
|
47 | | -*Last updated: 2026-07-18* |
| 100 | +*Last updated: 2026-07-27* |
0 commit comments