diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index aa88a1f..83a40e1 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -33,11 +33,11 @@ jobs: - name: Checkout uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - name: Initialize CodeQL - uses: github/codeql-action/init@e4fba868fa4b1b91e1fdab776edc8cfbe6e9fb81 # v3.28.1 + uses: github/codeql-action/init@4187e74d05793876e9989daffde9c3e66b4acd07 # v3.37.3 with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@e4fba868fa4b1b91e1fdab776edc8cfbe6e9fb81 # v3.28.1 + uses: github/codeql-action/analyze@4187e74d05793876e9989daffde9c3e66b4acd07 # v3.37.3 with: category: "/language:${{ matrix.language }}" diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 607e3d8..ecf9d48 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -1,47 +1,100 @@ + + + # Architecture ## Overview -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. +my-lang is a Rust-implemented language with a mechanised proof core. +The repository is a Cargo workspace plus proof, dialect, and +conformance trees. This file describes the layout as it actually is; +for the authoritative state of the proofs, see `proofs/STATUS.md` +(that registry wins over any other prose, including this file). + +## The dialect containment hierarchy -## Directory Structure +The three real dialects are **nested subsets, not parallel languages**: ``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation +Solo ⊂ Duet ⊂ Ensemble ``` -## Design Principles +- **Solo** — the innermost kernel. +- **Duet** — everything in Solo plus more; mechanised as + "ensemble restricted to 2-party by projection" (S2 track). +- **Ensemble** — the full language (session-typed π-calculus core, + S1 track). +- **Me** — not a fourth layer: an on-the-fly projector that cuts the + hierarchy at a chosen point. Its Rust scaffolding is sidelined in + `_exploratory/me-scaffolding/` (see `SIDELINED.adoc` there) and is + **not** part of the active workspace. -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized +Audits must grade the layered stack, not three separate compilers: a +broken Solo breaks Duet and Ensemble by transitivity. -## Dependencies +## Directory structure -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility +``` +. +├── crates/ # Cargo workspace (15 members) +│ ├── my-lang/ # core: lexer/parser/checker (largest crate) +│ ├── my-cli/ # `my` binary +│ ├── my-parser/ # parser scaffolding +│ ├── my-hir/ # high-level IR +│ ├── my-mir/ # mid-level IR +│ ├── my-qtt/ # QTT verified-core checker (faithful port of +│ │ # the Coq R5 `check` / R5b `aff_type_dec`) +│ ├── my-llvm/ # LLVM codegen (needs system LLVM 21; excluded +│ │ # from coverage CI for hermeticity) +│ ├── my-lsp/ # language server +│ ├── my-dap/ # debug adapter +│ ├── my-debug/ # debugging support +│ ├── my-fmt/ # formatter +│ ├── my-lint/ # linter +│ ├── my-test/ # test harness +│ ├── my-pkg/ # package manager +│ └── my-ai/ # AI integration +├── proofs/ # Mechanised core — Coq (solo-core, SessionPi) +│ # + Idris2 tracks; STATUS.md is the registry +├── dialects/ # solo/ and duet/ compilers + examples +├── _exploratory/ # sidelined scaffolding (me-scaffolding/) +├── conformance/ # impl ⇄ verified-spec differential tests +├── spec/ # language specification +├── grammar.ebnf # surface grammar +├── examples/ # example programs +├── playground/ # demo playground (+ hives/) +├── my-ssg/ # site generator input +├── vscode-extension/ # editor support +├── docs/ # documentation (published via Ddraig SSG) +├── LICENSE # MPL-2.0 (code); CC-BY-SA-4.0 for docs +└── LICENSES/ # full licence texts (REUSE layout) +``` -## Security Considerations +## CI gates -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed +- `proofs.yml` — machine-checks the Coq solo-core and asserts the + soundness theorems, the usage-walk checker (R5/R5b), the me→solo + elaboration (M1), the session-π core (S1.x), and the + duet-by-projection results (S2) are **axiom-free** + (`Print Assumptions` must report "Closed under the global context"). +- `coverage.yml` — cargo-llvm-cov over the workspace excluding + `my-llvm`, with an enforced line-coverage floor. +- `checker-scaling.yml` — checker performance scaling gate. +- `codeql.yml`, `hypatia-scan.yml`, `secret-scanner.yml`, + `scorecard.yml`, `cflite_*.yml` — security/fuzzing gates. +- `governance.yml` — estate policy via hyperpolymath/standards + reusable workflows. +- `pages.yml` — docs deployment via Ddraig SSG. -## Maintainability +## Design principles -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently +- **No proof hole is ever described as "proved"** — statement-only + theorems are tracked obligations (`proofs/STATUS.md` vocabulary). +- **Layered dialects** — features land in the innermost layer that can + express them; outer layers add, never fork. +- **Hermetic CI** — the LLVM back end is isolated so every other gate + runs without a system toolchain. --- -*Last updated: 2026-07-18* +*Last updated: 2026-07-27*