|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | += RSR Template-Applicability Policy |
| 3 | +Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +:toc: |
| 5 | +:toc-placement: preamble |
| 6 | + |
| 7 | +Canonical policy for *which parts of `rsr-template-repo` a given repository |
| 8 | +should carry*. It replaces "every repo looks like the full template" with a |
| 9 | +capability-gated model: a repo carries a template module only if it actually |
| 10 | +has the capability that module serves. |
| 11 | + |
| 12 | +== Why |
| 13 | + |
| 14 | +`rsr-template-repo` is maximal: it ships FFI/ABI seams, formal-proof trees, |
| 15 | +container scaffolding, service e2e, mobile shells, an AffineScript subtree, and |
| 16 | +the full governance trio — so that *some* repo can be scaffolded for *any* of |
| 17 | +them. The existing enforcement |
| 18 | +(`scripts/check-root-shape.sh` reading `.machine_readable/root-allow.txt`) |
| 19 | +encodes that maximum as **one canonical shape for all repos**. The result is |
| 20 | +over-scaffolding: a small Rust CLI is told `abi.ipkg`, `verification/`, |
| 21 | +`container/`, and `affinescript/` are "canonical" even though it has no ABI |
| 22 | +seam, no in-tree proofs, ships no container, and contains no AffineScript. |
| 23 | + |
| 24 | +Empty scaffolding is not neutral — it is vestigial cruft that misleads readers, |
| 25 | +invites drift, and dilutes the signal of the parts that are real. This policy |
| 26 | +makes "carry it only if you need it" a *rule with a test*, not a judgement call. |
| 27 | + |
| 28 | +== Model |
| 29 | + |
| 30 | +Three layers: |
| 31 | + |
| 32 | +. *Universal baseline* — modules every repo carries unconditionally (identity, |
| 33 | + community-health, machine-readable state, the licence invariant). |
| 34 | +. *Capability gates* — every other template module is tagged with the |
| 35 | + *capability* it serves. A repo carries the module **iff** it declares that |
| 36 | + capability. |
| 37 | +. *Presets* — named capability bundles (`rust-cli`, `rust-ffi-lib`, |
| 38 | + `rust-service`, `formal-proof-lib`, `docs-site`, …) a repo adopts as its base, |
| 39 | + then adjusts with explicit per-capability `add` / `remove`. (The "hybrid" |
| 40 | + layer: presets for ergonomics, gates for precision.) |
| 41 | + |
| 42 | +A repo's *profile* (`.machine_readable/rsr-profile.a2ml`) declares its preset |
| 43 | +and any adjustments. Its effective capability set drives everything else. |
| 44 | + |
| 45 | +== Capability taxonomy |
| 46 | + |
| 47 | +[cols="1,2,3"] |
| 48 | +|=== |
| 49 | +| Axis | Capability | A repo declares it when… |
| 50 | + |
| 51 | +.4+| Language |
| 52 | +| `rust` | it contains Rust/SPARK source (`Cargo.toml`, `*.rs`). |
| 53 | +| `zig` | it contains Zig source (FFI/gateway/SDK layer). |
| 54 | +| `agda` / `idris2` / `haskell` / `gleam` / `elixir` / `affinescript` / `julia` / `ocaml` |
| 55 | +| it contains source in that language *as its own code* (not merely consumes a tool written in it). |
| 56 | +| `bash` | it ships non-trivial shell scripts (almost universal; rarely gating). |
| 57 | + |
| 58 | +.5+| Interface / seam |
| 59 | +| `cli` | it ships a command-line binary. |
| 60 | +| `library` | it is consumed/published as a library. |
| 61 | +| `ffi` | it exposes or consumes a C-ABI FFI seam (Zig FFI scaffold). |
| 62 | +| `abi` | it has a *formally specified* ABI (Idris2 `abi.ipkg` + `src/interface/Abi/` proofs + `ffi/` + `generated/`). |
| 63 | +| `api-service` | it runs as a network service/daemon. |
| 64 | + |
| 65 | +| Verification |
| 66 | +| `formal-proofs` | it *contains* mechanised proofs in-tree (`verification/proofs/`). **Consuming** a prover (e.g. a tool that shells out to Agda) is *not* this capability. |
| 67 | + |
| 68 | +.3+| Surface |
| 69 | +| `mobile` | it ships a Tauri/Dioxus mobile app. |
| 70 | +| `web-ui` | it ships a browser UI. |
| 71 | +| `docs-site` | it publishes a static site (casket-ssg / Pages). |
| 72 | + |
| 73 | +.3+| Distribution |
| 74 | +| `published-package` | it publishes to a registry (crates.io / Hackage / JSR). |
| 75 | +| `container` | it ships a container image. |
| 76 | +| `reproducible-build` | it provides a Guix/Nix reproducible build. |
| 77 | + |
| 78 | +.2+| Governance tier |
| 79 | +| `governance-tier` | it is load-bearing/critical enough to carry the full `AUDIT` / `AFFIRMATION` / `GOVERNANCE` / `MAINTAINERS` trio. Small leaf repos may decline it. |
| 80 | +| `benchmarks` | it maintains a benchmark suite (`benches/`). |
| 81 | +|=== |
| 82 | + |
| 83 | +The machine-readable source of truth for capabilities, gates, and presets is |
| 84 | +`.machine_readable/template-capability-gates.toml`. The tables below mirror it |
| 85 | +for humans. |
| 86 | + |
| 87 | +== The gate table (module → capability) |
| 88 | + |
| 89 | +*Universal baseline* (gate = ∅; always carried): |
| 90 | + |
| 91 | +`README.adoc`, `EXPLAINME.adoc`, `LICENSE`, `SECURITY.md`, `CONTRIBUTING.md`, |
| 92 | +`CODE_OF_CONDUCT.md`, `CHANGELOG.md`, `0-AI-MANIFEST.a2ml`, |
| 93 | +`.machine_readable/6a2/{STATE,META,ECOSYSTEM,AGENTIC,NEUROSYM,PLAYBOOK}.a2ml`, |
| 94 | +`.machine_readable/rsr-profile.a2ml`, `.well-known/`, `.gitignore`, `Justfile`, |
| 95 | +and the SPDX licence invariant (`LICENCE-POLICY.adoc`). |
| 96 | + |
| 97 | +*Gated modules:* |
| 98 | + |
| 99 | +[cols="2,1"] |
| 100 | +|=== |
| 101 | +| Template module / path | Gating capability |
| 102 | + |
| 103 | +| `Cargo.toml`, `Cargo.lock`, `src/**/*.rs`, `.github/workflows/rust-ci.yml` | `rust` |
| 104 | +| `src/interface/ffi/**` (Zig) | `ffi` |
| 105 | +| `abi.ipkg`, `src/interface/Abi/**` (Idris2), `src/interface/generated/**` | `abi` |
| 106 | +| `verification/proofs/**`, proof-CI | `formal-proofs` |
| 107 | +| service e2e, `.github/workflows/e2e.yml` | `api-service` |
| 108 | +| `container/`, `Containerfile` | `container` |
| 109 | +| `build/guix.scm`, `flake.nix`, `.guix-channel` | `reproducible-build` |
| 110 | +| mobile shell (Tauri/Dioxus) | `mobile` |
| 111 | +| `affinescript/` subtree | `affinescript` |
| 112 | +| `benches/` | `benchmarks` |
| 113 | +| `AUDIT.adoc`, `AFFIRMATION.adoc`, `GOVERNANCE.adoc`, `MAINTAINERS.adoc` | `governance-tier` |
| 114 | +| `.github/workflows/release.yml`, registry metadata | `published-package` |
| 115 | +|=== |
| 116 | + |
| 117 | +== Presets |
| 118 | + |
| 119 | +[cols="1,3"] |
| 120 | +|=== |
| 121 | +| Preset | Base capabilities |
| 122 | + |
| 123 | +| `rust-cli` | `rust`, `cli`, `library` |
| 124 | +| `rust-ffi-lib` | `rust`, `zig`, `ffi`, `abi`, `library` |
| 125 | +| `rust-service` | `rust`, `api-service`, `container`, `reproducible-build` |
| 126 | +| `formal-proof-lib` | `agda` *or* `idris2`, `formal-proofs`, `library` |
| 127 | +| `docs-site` | `docs-site` |
| 128 | +| `affinescript-app` | `affinescript`, `web-ui` |
| 129 | +|=== |
| 130 | + |
| 131 | +A profile may `add` or `remove` individual capabilities on top of its preset |
| 132 | +(e.g. `rust-cli` + `add = ["published-package"]`). |
| 133 | + |
| 134 | +== The test |
| 135 | + |
| 136 | +Let `P` be a repo's effective capability set (`preset` ∪ `add` − `remove`). |
| 137 | + |
| 138 | +---- |
| 139 | +carries(M) ⟺ M ∈ baseline ∨ gate(M) ⊆ P |
| 140 | +---- |
| 141 | + |
| 142 | +For any tracked template-module path `X`: |
| 143 | + |
| 144 | +* *OK* — `carries(X)` and `X` is present. |
| 145 | +* *MISSING* — `carries(X)` but `X` is absent → add it. |
| 146 | +* *VESTIGIAL* — `X` is a known template module, present, but `gate(X) ⊄ P` → |
| 147 | + remove it *or* declare the missing capability (with justification). |
| 148 | +* *UNKNOWN* — `X` is project-specific (not a template module) → allowed; it is |
| 149 | + the repo's own content, governed by the root-shape allowlist as before. |
| 150 | + |
| 151 | +The key new verdict is **VESTIGIAL**: scaffolding present without the capability |
| 152 | +that justifies it. That is the thing this policy removes. |
| 153 | + |
| 154 | +== Per-repo profile |
| 155 | + |
| 156 | +`.machine_readable/rsr-profile.a2ml` (A2ML, TOML-like; SPDX `MPL-2.0`): |
| 157 | + |
| 158 | +[source,toml] |
| 159 | +---- |
| 160 | +[profile] |
| 161 | +preset = "rust-cli" |
| 162 | +add = [] # extra capabilities beyond the preset |
| 163 | +remove = [] # preset capabilities this repo does NOT have |
| 164 | +
|
| 165 | +[rationale] |
| 166 | +# One line per non-obvious add/remove or declined capability. |
| 167 | +no-abi = "language-agnostic engine; no C-ABI seam, no Idris2 ABI proofs" |
| 168 | +no-formal-proofs = "consumes Agda (shells out); contains no in-tree proofs" |
| 169 | +---- |
| 170 | + |
| 171 | +== Enforcement (how this evolves the existing machinery) |
| 172 | + |
| 173 | +`root-allow.txt` becomes *derived*, not hand-maintained as one shape: |
| 174 | + |
| 175 | +---- |
| 176 | +effective-allowlist(repo) = baseline ∪ { M : gate(M) ⊆ profile(repo).capabilities } |
| 177 | +---- |
| 178 | + |
| 179 | +* `scripts/check-rsr-profile.sh` (reference implementation, this repo) reads a |
| 180 | + repo's `rsr-profile.a2ml` + `template-capability-gates.toml` and reports |
| 181 | + `MISSING` / `VESTIGIAL` modules. |
| 182 | +* `check-root-shape.sh` / `validate-template.sh` evolve to consume |
| 183 | + `effective-allowlist(repo)` instead of a static `root-allow.txt` (follow-up; |
| 184 | + the static file remains valid as the `governance-tier` + all-capabilities |
| 185 | + maximum until then). |
| 186 | + |
| 187 | +A repo opts in by adding its `rsr-profile.a2ml` and running the check in CI. |
| 188 | + |
| 189 | +== Worked example — arghda-core (`rust-cli`) |
| 190 | + |
| 191 | +A small language-agnostic Rust CLI. Profile: `preset = "rust-cli"`, |
| 192 | +`remove = []`. Effective capabilities: `rust`, `cli`, `library`. |
| 193 | + |
| 194 | +* *Carries* (gate ⊆ P): the universal baseline + `Cargo.toml`/`Cargo.lock`/ |
| 195 | + `src/**/*.rs`/`rust-ci.yml` (`rust`). |
| 196 | +* *Correctly absent* (VESTIGIAL if present): `abi.ipkg` + `src/interface/` |
| 197 | + (`abi`/`ffi`), `verification/proofs/` (`formal-proofs` — arghda *consumes* |
| 198 | + Agda but contains no proofs), `container/` (`container`), `affinescript/` |
| 199 | + (`affinescript`), the `AUDIT`/`AFFIRMATION`/`GOVERNANCE`/`MAINTAINERS` trio |
| 200 | + (`governance-tier`, declined by a leaf tool). |
| 201 | + |
| 202 | +That is precisely the lean shape arghda-core ships — now justified by a rule |
| 203 | +rather than a judgement call. |
| 204 | + |
| 205 | +== Status |
| 206 | + |
| 207 | +DRAFT (first pass). Open items: fold `effective-allowlist` into |
| 208 | +`check-root-shape.sh`; confirm the `governance-tier` boundary (which repos must |
| 209 | +carry the full trio); enumerate the remaining maximal-template modules into the |
| 210 | +gate table as they are profiled. |
0 commit comments