diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md new file mode 100644 index 0000000..584ed41 --- /dev/null +++ b/DELIVERY-186-197.md @@ -0,0 +1,853 @@ +# Delivering the two open issues in `hyperpolymath/maa-framework` + +**Status:** both delivered and verified in the working tree. **Nothing is committed yet.** +**Date:** 2026-09-22 · **Repo:** `hyperpolymath/maa-framework` (commit `939b8c3`) + +Your two additions to the brief — *make it standalone* and *Rust here is always Rust/Creusot* — are both built in. +One correction I need to flag on the licence, in the last section. + +--- + +## TL;DR + +| Issue | Status | Headline evidence | +|---|---|---| +| **#186** `create-template.sh` scaffolds retired v1 shape | **Delivered** — exceeds acceptance | Fresh scaffold now scores **26/26, Bronze + Silver ACHIEVED, exit 0** (was 14/26, NOT MET) | +| **#197** consolidate `Scanner::walk_files` traversals | **Delivered** | 7 traversals → 1; **212 ms → 150 ms** on an 18,602-file tree; verdicts byte-identical | + +Suite went from 68+47 to **72+48 = 120 tests**, clippy `-D warnings` clean, `cargo fmt --check` clean, `just check` exit 0. + +--- + +## Issue #186 — the generator emitted the retired v1 shape + +### Reproduced first + +I scaffolded with the unmodified generator and ran the unmodified checker: + +``` +$ create-template.sh repro-project rust && aletheia repro-project +Score: 14/26 checks passed (53.8%) +Bronze-level RSR compliance: NOT MET +``` + +Failing Bronze checks: `.github/`, `LICENSE` (it wrote `LICENSE.txt`), `.gitignore`+`.gitattributes`, +SPDX headers, CI pipeline. Exactly as filed. + +### What changed + +**1. A real v2 template** — `aletheia/templates/bronze-rust/`, 30 files replacing the single stale +`README-template.adoc`: + +``` +LICENSE + LICENSES/ MPL-2.0 + CC-BY-SA-4.0, full texts shipped in-tree +Justfile capital J, real recipes, no silent-skip +Cargo.toml zero dependencies, offline by construction +src/, tests/ working code + 8 tests +verification/ Rust/Creusot proof crate (see below) +.github/workflows/ ci.yml, hypatia-scan.yml, governance.yml, actions.lock +.machine_readable/ rsr-profile.a2ml capability declaration +.well-known/ security.txt, ai.txt, humans.txt +0-AI-MANIFEST.a2ml agent front door + README/SECURITY/CONTRIBUTING/CoC/CHANGELOG/MAINTAINERS .adoc +``` + +**2. A rewritten generator** — `scripts/create-template.sh`, 832 lines changed down to 334. +It now renders the template tree with 11 `@@PLACEHOLDER@@` tokens, and its help text documents both +what the v2 shape *is* and what it deliberately no longer emits. + +**3. A regression guard** — `test_scaffold_passes_bronze_and_silver` in `tests/integration_tests.rs`. +It runs the real generator, asserts no v1 artefact reappears, asserts no unresolved placeholder is +left, and runs the real checker over the output. The acceptance criterion is now enforced by CI, so +the template and the checker can't drift apart again without the suite going red. + +### Acceptance — met and exceeded + +The issue asked for "Bronze (ideally Silver)". A fresh scaffold now gets: + +``` +Score: 26/26 checks passed (100.0%) +Bronze-level RSR compliance: ACHIEVED +Silver-level RSR compliance: ACHIEVED ← the "ideally" +✅ No silent-skip in recipes [Gold] ← Gold's only check passes too +``` + +with **no hand edits**, and `just check` (build, test, fmt, clippy, deps-check) exits 0. + +### "Standalone" — nothing to download, and I proved it + +The generated project fetches nothing, and neither does the generator: + +- licence texts are **shipped in the template**, not `curl`ed (the old script fetched MIT from + opensource.org and Apache from apache.org, falling back to writing stub files on failure) +- no `flake.nix`, no Python/`flake8`, no Makefile, no Dockerfile +- the dead `gitlab.com/maa-framework/...` install URL is gone; the v1 GitLab mirror 403 is not + reintroduced anywhere +- zero dependencies, so `cargo build --offline` always succeeds + +Proven by running generation *and* build inside a network namespace with no network at all: + +``` +lo DOWN ; ping 1.1.1.1 → Network is unreachable + +GENERATED: 30 files +$ cargo build ← note: no --offline flag, and no network to fall back on + Finished `dev` profile +$ cargo test + test result: ok. 5 passed ... ok. 3 passed +``` + +### "Rust is always Rust/Creusot" — built in + +`verification/` is a Creusot proof crate carrying real `#[requires]` / `#[ensures]` obligations for +two functions in the main crate. It is **deliberately detached** from the Cargo workspace +(`exclude = ["verification"]`), because Creusot needs `creusot-contracts` + Why3 and the main crate +must stay zero-dependency. `just proof` / `just proof-prove` drive it; `just check` never needs it. + +Two honest caveats, both documented in `verification/README.adoc` rather than papered over: + +- **The obligations are not wired into CI yet.** Creusot is research software tracking a specific + nightly; a CI job would be non-reproducible until that nightly and the SMT solver set are pinned. + Shipping a job that can't run reproducibly would be the fake gate this estate explicitly bans. +- **The specs are mirrors, not single-source.** Creusot must see the annotated source, so + `verification/src/lib.rs` mirrors `src/`. Change one, change the other in the same commit. The + README notes the tighter `#[cfg_attr(creusot, …)]` + `include!` option if you want single-source later. + +--- + +## Issue #197 — consolidate `Scanner::walk_files` + +### Design: one traversal, four buckets + +Each check used to call `walk_files` for itself — seven full walks of the same tree in the same +order, differing only in which files they collected. Now one traversal fills a `ScanSet` with four +buckets (`all`, `spdx`, `secret`, `banned`), memoised in a `OnceCell` on the `Scanner`, so the seven +call sites read from it instead of re-walking. + +The saving is in the traversal (`read_dir` + `file_type` per entry), not the extension filter applied +afterwards. That's why the buckets pay off: `.rs` is an SPDX-header *and* a secret-scan extension, and +`.py` is secret-scanned *and* banned — one file now serves several checks in one pass. + +### Budget semantics + +The issue required **identical budget semantics**, so this is where the care went. A bucket accepts at +most `MAX_SCAN_FILES` *matches of its own* — mirroring the old behaviour where +`walk_files(Some(exts))` counted only files passing its filter, not every file seen. When a bucket +fills it stops growing and the traversal continues, so the other buckets still get their own first +50,000 matches. `MAX_SCAN_DEPTH`, `SKIP_DIR_NAMES`, submodule boundaries, `[ignore]` globs and the +never-follow-symlinks rule are untouched. The symlink sweep keeps its own separate budget. + +Four unit tests pin this, including that filling `all` does **not** consume the filtered buckets' budgets. + +One deliberate refinement, called out because it is a real (benign) difference: the truncation warning +now fires when a file is actually *refused*, rather than when a walk happens to pass the cap. Same +trigger condition in practice, but it now means "results really are partial". + +### Evidence + +**Fewer traversals, measured** on a synthetic tree of 18,602 files across 673 directories, best-of-10 +with release binaries: + +| | time | +|---|---| +| baseline (7 walks) | **212 ms** | +| new (1 walk) | **150 ms** | +| | **~29% faster overall; traversal itself ~7× reduced** | + +**Semantics preserved, checked** — old vs new binary on five repositories, comparing full output with +the timestamp line stripped: + +``` +IDENTICAL bigtree (18k files) IDENTICAL demo-service (fresh scaffold) +IDENTICAL maa-framework IDENTICAL aletheia +IDENTICAL standards (29 MB) +exit codes match: bigtree 1/1, demo-service 0/0, aletheia 0/0 +``` + +**Suite green** — 72 unit + 48 integration = 120 tests; clippy `-D warnings` clean; `cargo fmt --check` clean; +estate root `just check` exit 0; `just self-verify` 26/26. + +--- + +## What is left + +1. **Push the branch and open the PR.** Everything is committed locally — three commits, messages + below — but I have no push credentials, so nothing is on the remote yet. See "Commits". +2. **Rotate the GitHub token you pasted into chat.** Please treat it as compromised — see the note below. +3. **Decide on the remaining Tier-1 language templates.** The v1 generator offered `python`, + `typescript` and `go`. Those extensions are *banned* by the v2 estate language policy, so those + paths could never pass Bronze — I removed them rather than port them. Zig, Elixir, Haskell, Ada, + Agda and AffineScript are Tier-1 per your `standards` canon and are reasonable follow-on templates. +4. **Wire the proof gates into CI.** **Partly done in this pass.** Both templates ship an opt-in + `.github/workflows/proof.yml`. Attempting to execute them from scratch (below) found one real + defect in the Rust one, now fixed. Neither has run on a GitHub runner yet, so the templates + still do not claim CI-verified proofs — the first green run is what makes them load-bearing. +5. **Close #186 and #197** with the acceptance evidence above. + +--- + +## Two things worth your attention + +### 1. Your MPL-2.0 correction exposes drift inside `aletheia` itself + +You said MPL-2.0, and the estate agrees — but the checker's own directory disagrees with itself. +I first wrote PMPL-1.0 into the template from `aletheia/LICENSE`; you corrected it to MPL-2.0. Counting +the actual usage across the repo: + +``` +128 × MPL-2.0 ← dominant, and what aletheia's own src/*.rs headers say + 36 × CC-BY-SA-4.0 ← docs, consistent + 2 × PMPL-1.0-or-later ← the outliers +``` + +`aletheia/LICENSE` declares **Palimpsest PMPL-1.0-or-later**; `aletheia/LICENSES/` ships +`PMPL-1.0-or-later.txt` instead of `MPL-2.0.txt`; yet **aletheia's own source files carry +`SPDX-License-Identifier: MPL-2.0`**. The root repo is clean (full MPL-2.0 `LICENSE` text, +`LICENSES/{MPL-2.0,CC-BY-SA-4.0,AGPL-3.0-or-later}.txt`), so the drift is confined to the nested +`aletheia/` crate. + +Worth knowing that **`aletheia` cannot currently catch this**: `KNOWN_LICENSE_IDS` accepts both +`"Palimpsest"`/`"PMPL-1.0"` and `"Mozilla Public License"`/`"MPL-2.0"`, so `check_licence_class` +passes either way. That's a deliberate structural check (it only asserts *something* known is named), +and real classification is the hypatia oracle's job — but it means nothing in this repo will flag the +inconsistency. The template now emits MPL-2.0 throughout, per your correction. + +This is a separate piece of work from #186/#197, so I have **not** touched `aletheia/LICENSE`. +Say the word and I'll align it. + +### 2. That GitHub token + +`github_pat_11ABTSLTI0QYB…` — you pasted it mid-conversation. I did not use it, write it to any file, +or add it to any remote: everything I needed (your repo, MaaXYZ, `standards`) was readable +anonymously, and the repo path you gave turned out to be redundant once you supplied the URL. +**Please revoke it at github.com/settings/tokens and issue a fresh one.** It lives in this +transcript now, and fine-grained PATs are exactly the credential the estate's own secret-scanner +workflow exists to catch. + +--- + +## Verification log + +Every claim above is reproducible. The commands, run in order: + +```bash +# #186 — reproduce the filed failure +bash aletheia/scripts/create-template.sh repro-project rust +aletheia repro-project # 14/26, NOT MET + +# #186 — after the fix +bash aletheia/scripts/create-template.sh demo-service -d "A demo service" +aletheia demo-service # 26/26, Bronze + Silver, exit 0 +cd demo-service && just check # exit 0 +cargo fmt --check && cargo clippy --offline --all-targets -- -D warnings + +# #186 — air-gap proof +unshare -rn bash -c 'cd /tmp/nettest && create-template.sh isolated-demo && cd isolated-demo && cargo build && cargo test' + +# #197 — correctness and cost +cargo test # 120 passed +cargo clippy --all-targets -- -D warnings # clean +diff <(baseline /tmp/bigtree) <(new /tmp/bigtree) # identical + +# estate gate +cd .. && just check && just self-verify # 26/26 +``` + +--- + +## Files touched + +``` +M aletheia/scripts/create-template.sh (six languages, fixed MOD_ADA derivation) +M aletheia/src/checks.rs (ScanSet + single traversal, +238/-…) +M aletheia/tests/integration_tests.rs (+82 scaffold guard, +143 six-language guard) +D aletheia/templates/bronze-rust/README-template.adoc (superseded) ++ aletheia/templates/common/** (16 shared files) ++ aletheia/templates/{rust,zig,elixir,haskell,ada,agda}/** (per-language overlays) +``` + +The follow-on touched, within those overlays: + +``` +rust src/impl.rs (new, single source of truth) src/lib.rs src/main.rs Cargo.toml + tests/integration_test.rs Justfile .gitignore README.adoc + verification/{Cargo.toml, src/lib.rs, why3find.json, README.adoc} +ada src/.ads src/.adb src/main.adb tests/run_tests.adb + .gpr tests/tests.gpr Justfile .gitignore README.adoc +zig test/integration_test.zig .github/workflows/ci.yml +elixir, haskell .github/workflows/ci.yml haskell/Justfile (@@ARGS@@ -> {{ARGS}}) +``` + +Environment note: `rust`, `just` and the release builds were installed into this sandbox, not committed. + +--- + +# Follow-on: the six-language template set, with proofs that actually run + +You asked two things after the first delivery: make `Rust/Creusot` and `Ada/SPARK` **real** rather +than aspirational, and get **all six** templates to 26/26. Both are done, and both were verified by +making the provers themselves give a verdict — including negative controls, so you can see the gates +actually fail when the claim is false. + +## Headline + +| | Result | +|---|---| +| Six-language sweep (real generator) | **rust · zig · elixir · haskell · ada · agda — all 26/26, Bronze + Silver, `just check` exit 0** | +| Rust/Creusot | **`Proved (2 files) ✔`** — Creusot 0.14 translates and Why3 discharges every obligation | +| Ada/SPARK | **35 checks, 100% proved** — `gnatprove --level=2`, Z3 + Alt-Ergo + CVC5 | +| Negative controls | Breaking either specification makes the corresponding `just proof` **exit 1** | +| aletheia suite | **72 + 49 = 121 tests**, clippy `-D warnings` clean, `cargo fmt --check` clean | +| Estate gate | root `just check` exit 0; `just self-verify` **26/26** | + +## Rust/Creusot is real now + +The first delivery shipped `verification/` with `#[requires]`/`#[ensures]` that had **never been run**. +It also used the pre-0.14 contract crate and a floating git branch. All of that is replaced. + +### The toolchain actually works + +Getting there took real work, because Creusot does not use released Why3: it pins forks. + +``` +nightly-2026-08-03 (rustup, + rustc-dev) # Creusot's rust-toolchain pin +opam switch → why3 # pinned to git-c369bc4c + git+https://gitlab.inria.fr/why3/why3.git +why3find # pinned to git-0f054b93 + git+https://github.com/creusot-rs/why3find.git +z3 4.13.3, cvc5 1.1.2 # 7 provers detected +cargo-creusot, creusot-rustc # from the Creusot tree +``` + +Three specific traps, recorded so nobody repeats them: + +1. **Released `why3` cannot even parse Creusot's output.** With stock Why3 1.8.2 the generated + `.coma` dies with `syntax error`; with the pinned commit it proves. The pin is not optional. +2. **Released `why3find` will not compile against the pinned Why3** (`Unbound record field + "Why3.Term.t_loc"`). Creusot's fork is required, in lockstep. +3. **`cargo-creusot` looks for `why3find` inside its own data dir**, not on `PATH`, and loads + provers from `$XDG_DATA_HOME/creusot/creusot_why3.conf`. This is where "Package 'creusot' not + found" came from: why3find resolves packages through `DUNE_DIR_LOCATIONS`, which `cargo-creusot` + sets — running `why3find` by hand does not. + +### The design: the proof cannot drift from the code + +The obvious Creusot layout is a second, annotated copy of the functions. That copy drifts, and then +the proof describes code that no longer exists — worse than no proof. This template removes the +possibility: + +```rust +// src/impl.rs — the single source of truth +#[cfg(creusot)] +use creusot_std::prelude::*; + +#[cfg_attr(creusot, requires(lo@ <= hi@))] +#[cfg_attr(creusot, ensures(lo@ <= result@ && result@ <= hi@))] +pub fn clamp(value: u32, lo: u32, hi: u32) -> u32 { ... } + +// src/lib.rs (main crate) include!("impl.rs"); +// verification/src/lib.rs (Creusot crate) include!("../../src/impl.rs"); +``` + +`creusot-rustc` is the only thing that sets `--cfg creusot`. Under plain `cargo build` every +`#[cfg_attr]` vanishes and the Creusot prelude is never imported, so the main crate keeps its +**zero-dependency, air-gapped** build. Under `cargo creusot`, Creusot verifies the *actual* function +bodies — the failure messages name `../../src/impl.rs`, which is the real file. + +### Evidence + +``` +$ just proof +Proved (verif/proj_rust_verification_rlib/clamp.coma) ✔ +Proved (verif/proj_rust_verification_rlib/midpoint.coma) ✔ +Proved (2 files) ✔ # exit 0 + +# negative control 1 — clamp: result <= hi - 1 +File ".../src/impl.rs", line 27: proof failed Goal Coma.vc_clamp: ✘ (2/3) +Error: 1 unproved file # exit 1 + +# negative control 2 — midpoint: result == (a + b) / 2 + 1 +File ".../src/impl.rs", line 45: proof failed Goal Coma.vc_midpoint: ✘ (4/5) +Error: 1 unproved file # exit 1 +``` + +### One specification had to change, and here is the honest reason + +The sample `mean_floor` was `(a & b) + ((a ^ b) >> 1)` — a neat overflow-free mean. **Creusot 0.14 +cannot verify it, and cannot verify anything about it.** The `@` view operator maps an integer to a +mathematical `Int`, and `creusot_std::logic` provides no `BitAnd`, `BitXor` or `Shr` for it; there is +no bitvector theory in the backend. This is not a missing postcondition — even with *no* `ensures` at +all, Creusot still has to discharge overflow-freedom for the `+`, and fails: + +``` +Goal Coma.vc_mean_floor: ✘ (1/2) # a function with no contract at all +``` + +So the template ships `midpoint` — the same idea as `a + (b - a) / 2`, which needs only linear +arithmetic and whose exact half-sum identity **is** proved: + +```rust +#[cfg_attr(creusot, requires(a@ <= b@))] +#[cfg_attr(creusot, ensures(a@ <= result@ && result@ <= b@))] +#[cfg_attr(creusot, ensures(result@ == (a@ + b@) / 2))] +pub fn midpoint(a: u32, b: u32) -> u32 { a + (b - a) / 2 } +``` + +This is written up in `verification/README.adoc` with the failing example, so the boundary is +documented rather than quietly worked around. + +## Ada/SPARK is real now + +The first delivery called it Ada/SPARK while the sources had **no `SPARK_Mode` and no `gnatprove`** — +only Ada 2012 runtime contracts, and `src/main.adb` full of `Ada.Text_IO`, exceptions and +`'Value`/`'Image`, none of which are in the SPARK subset. + +Now the core package declares `pragma SPARK_Mode (On);` and its contracts are statically proved: + +```ada +function Clamp (Value, Lo, Hi : U32) return U32 + with Pre => Lo <= Hi, + Post => Clamp'Result in Lo .. Hi; + +function Midpoint (A, B : U32) return U32 + with Pre => A <= B, + Post => Midpoint'Result in A .. B + and then BI (Midpoint'Result) = (BI (A) + BI (B)) / 2; +``` + +`BI` is a ghost function over `Ada.Numerics.Big_Numbers.Big_Integers.Unsigned_Conversions`, which is +how SPARK states a *mathematical* half-sum — U32 arithmetic would wrap. + +**The same exact-identity obligation that Rust proves, SPARK proves too.** That took four `pragma +Assert` stepping stones in the body (modular subtraction and division agreeing with their exact +integer counterparts, and the final addition not wrapping); without them the provers returned +"medium: postcondition might fail". + +### A fake gate, caught + +`gnatprove` **exits 0 when a check is unproved.** With a deliberately false postcondition it printed +`high: postcondition might fail` and still returned success — `just proof` would have been decorative +and every template would have looked green forever. The fix is `--checks-as-errors`, which now lives +in the GPR so a bare `gnatprove -P .gpr` is already correct: + +``` +$ just proof # false postcondition: Post => Clamp'Result in Lo .. Hi - 1 +proj_ada.ads:36:19: high: postcondition might fail +gnatprove: unproved check messages considered as errors +error: recipe `proof` failed on line 39 with exit code 1 # exit 1 + +$ just proof # restored +Total 35 . 35 (100%) # Z3, Alt-Ergo, CVC5 # exit 0 +``` + +Note also what is *not* proved: `src/main.adb` is `pragma SPARK_Mode (Off);` on purpose — the I/O +boundary is outside the SPARK subset. gnatprove skips it rather than pretending to verify it, and +that is stated in the README. + +## Three defects found while doing this that the first pass had missed + +These are the reason the follow-on was worth doing rather than just relabelling. + +1. **`@@ARGS@@` broke Haskell generation outright.** `templates/haskell/Justfile` used `@@ARGS@@`, + which is not a placeholder the generator knows. The generator's own unresolved-placeholder guard + then aborted: `create-template.sh foo -l haskell` exited 1 with *"the generator and the template + tree are out of sync"*. It is now `{{ARGS}}`, matching the other five templates. My earlier probe + had rendered templates directly and so had never exercised the guard. + +2. **`MOD_ADA` derivation was wrong for single-letter segments.** `g-ada` produced the Ada unit + `GAda`, but the template ships `g_ada.ads`; GNAT then looked for `gada.ads` and failed with + `file "gada.ads" not found`. Fixed by deriving the unit name from the project name directly + (`G_Ada`, `Proj_Ada`, `My_Neat_Project`) instead of inserting underscores at case boundaries in + the camel form. Verified clean across `g-ada`, `proj-ada`, `my-neat-project`, `ab-cd`, `a-b`, + `wtest` — with no `Naming` workaround needed. + +3. **`zig fmt --check` rejected the template's own test file** (a multi-line array literal needing + zig's column alignment). Restructured to one element per line, which formats stably. Zig is now + 26/26 instead of 25/26. + +Plus the Silver miss: **the three remaining actions are now genuinely SHA-pinned**, resolved from +real tags rather than invented: + +``` +mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2 → v2.2.1 +erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124 # v1 → v1.24.1 +haskell-actions/setup@0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d # v2 → v2.12.1 +``` + +`actions/checkout@v7.0.1` is left as-is: it is the estate's canonical ref and is covered by +`.github/workflows/actions.lock`, which is the lock mechanism the checker itself implements. + +## Build output no longer breaks the gate + +The one finding from the follow-on that was worth fixing immediately, rather than leaving as an +issue. Reproducing it first: + +``` +# a minimal compliant project, freshly built +$ aletheia . +Score: 20/26 checks passed (76.9%) Bronze-level RSR compliance: ACHIEVED + +# same tree, `.gitignore` present but not honoured by the scanner +$ aletheia . +Score: 18/26 checks passed (69.2%) Bronze-level RSR compliance: NOT MET +Fix Suggestions: + - SPDX license headers: Add SPDX-License-Identifier headers (first 10 lines) to: + obj/b__main.ads, obj/deep/gen.rs; v2 4.1.1. +``` + +Two things were wrong with that. The obvious one is that the gate was only meaningful on a clean +checkout. The dangerous one is that **any CI job running the gate after a build would fail**, which +is exactly the order the estate's own `just check` uses — so the gate was quietly unusable in the +arrangement it was most wanted. + +The scanner now reads `.gitignore` as it descends. Rules are pushed when the walk enters a +directory and popped on the way out, so a nested `.gitignore` stays scoped to its own subtree. +A directory-only rule (`obj/`) is evaluated against the entry's real file type, so it skips the +directory *without* exempting a file of the same name — a path string alone cannot tell those +apart, which is why the walk asks the type-aware question. + +Implemented: comments, blank lines, `!` negation with last-match-wins, trailing slash, +leading-slash anchoring, `*` crossing directory boundaries (matching this crate's existing +`glob_match`). **Not** implemented, and not claimed: character classes, backslash escapes, and +re-inclusion inside an ignored directory. + +It stays separate from the existing `[ignore]` config on purpose: `[ignore]` is a choice made in +aletheia's own configuration, whereas `.gitignore` is the repository's declaration of what is not +part of the published artefact. + +Evidence, on a freshly generated Rust template: + +``` +$ just check # builds, tests, lints — leaves target/ full of artefacts +$ aletheia . +Score: 26/26 checks passed (100.0%) Bronze + Silver ACHIEVED +``` + +Three integration tests and ten unit tests cover it, including the negative controls: a +non-ignored file with no SPDX header still reports, and a file whose name matches a directory-only +rule is still audited. + +--- + +## Commits + +Six commits, split so each is coherent and individually green when checked out. `#197` and the +`.gitignore` work share a file *and* interleave within the same function, so they are one commit +rather than a fabricated split. + +``` +47d9e3b perf(scanner): one traversal, and honour the repository's .gitignore + aletheia/src/checks.rs, aletheia/src/config.rs + +8327b13 feat(scaffold): emit the v2 six-language template set + aletheia/templates/**, aletheia/scripts/create-template.sh, + aletheia/tests/integration_tests.rs + +123710a docs: delivery write-up for #186 and #197 +de3e2e9 docs: explain why the six templates do not share one sample API + +b28e539 fix(ci): the Rust proof workflow could not have worked as written +a318d02 fix(ci): finish the Creusot install, and stop hard-coding the Why3 pin + aletheia/templates/rust/.github/workflows/proof.yml + + docs: record what running the proof workflows actually found + DELIVERY-186-197.md +``` + +The last two exist because the first version of that workflow was wrong and no amount of reading it +had shown that — see "Proof workflows: what *not yet executed* was hiding". + +Two things were deliberately left uncommitted: + +* `absolute-zero` shows as a deleted submodule. It was never initialised in this sandbox (there is + no network checkout of it), so committing the deletion would be wrong. `git submodule update + --init` restores it. +* The lost executable bits on `setup.sh`, the `.github/hooks/*` scripts and + `aletheia/scripts/install.sh` are restored, not committed — they changed because the sandbox + restore does not preserve modes, not because anything meant to change. + +--- + +## Proof workflows: what "not yet executed" was hiding + +Both proof workflows shipped with a caveat: written from commands run by hand, never executed as +workflows. Exercising them properly meant rebuilding the Creusot toolchain from nothing, because +this sandbox had lost it. That was worth doing — the Rust one was wrong in three separate ways. + +**What already held up.** Every command in the toolchain half ran exactly as written: the apt list, +`git clone`, `rustup toolchain install --component rustc-dev,llvm-tools`, `opam init --bare +--disable-sandboxing`, `opam switch create creusot ocaml-system`, and both `opam pin` commands for +Creusot's forks of why3 and why3find. + +One of those was already fixed for the right reason. Creusot's `rust-toolchain` file is TOML — +`channel = "nightly-2026-08-03"` — but has no `.toml` extension, so the obvious `head -1` yields +`[toolchain]` and the job installs the wrong toolchain. The workflow parses the key and fails +loudly if it cannot; Creusot's own installer parses the same key, so this is not just belt-and-braces. + +**What was wrong.** + +1. *It never installed `creusot-rustc` where `cargo creusot` looks.* Not on `PATH` — under its data + dir, along with the prelude and the generated `why3.conf`: + + ``` + creusot-rustc not found (expected at + "/home/user/.local/share/creusot/toolchains/nightly-2026-08-03/bin/creusot-rustc"). + You should reinstall Creusot. + ``` + + Installing the two binaries and running `cargo creusot config --update` leaves all three pieces + missing. Fixed by running Creusot's own installer for the rest. + +2. *It never installed the provers, or why3/why3find in the data dir either.* This is the + interesting one, because it fails much later and more confusingly. `why3` is launched with the + data dir's `bin` **first on `PATH`**, and `creusot_why3.conf` names provers by bare name + (`alt-ergo --timelimit %.t %f`). So: + + ``` + $ just proof + Error: 'why3find prove' failed to launch + Caused by: No such file or directory (os error 2) + ``` + + That is `alt-ergo` not existing. `cargo creusot` also resolves `why3` and `why3find` themselves + as `$XDG_DATA_HOME/creusot/bin/why3[find]`, not from `PATH` — so having them in an opam switch + is not enough either. The installer's `provers` component fetches the exact versions the drivers + name (alt-ergo 2.6.2, z3 4.15.3, cvc4 1.8, cvc5 1.3.1); apt `z3` is a different build behind the + same driver name, which is a quiet way to get different answers from the same proof. The + workflow now installs those, provides `why3`/`why3find` the way the installer's own `why3` + component does (it builds a second opam switch inside the data dir and pulls in the GTK why3 + IDE for the privilege; its last act is to symlink those two binaries, so we do that directly), + and asserts `cargo creusot version` resolves all four provers before attempting to prove. + +3. *Its Why3 pin was already stale.* The workflow hard-coded the fork commits; the checkout now + declares a different Why3 commit. A proof gate that silently changes toolchain underneath a + passing build is not a gate. The workflow now pins the Creusot revision and **derives** both + forks from that revision's `creusot-deps.opam`, failing if the parse comes up empty. + +**The gate, run for real.** On the rebuilt toolchain, `cargo creusot version` resolves all four +provers, and `just proof` in the generated template reports: + +``` +$ just proof +Proved (2 files) ✔ +exit 0 +``` + +with Why3 pinned to the same commit the workflow will use. The negative control — a false +postcondition, `result@ == (a@ + b@) / 2 + 1` — gives: + +``` +File ".../src/impl.rs", line 45: proof failed +Goal Coma.vc_midpoint: ✘ (4/5) +Error: 1 unproved file +Error: 'why3find prove' failed +exit 1 +``` + +**A false pass, and why it is written down here.** My first attempt at that negative control +reported `Proved (2 files)` and exit 0 — a false gate, which is the one result that must never be +waved away. It reproduced, deliberately: take a tree *together with its build output and its +`verif/` directory*, plant a false obligation in the shared `src/impl.rs`, run `just proof`, and +the run finishes in 0.01 s and reports success without re-translating the changed source file. Hit +the same tree after forcing a re-translation (`touch verification/src/lib.rs`) and it fails +correctly, as it does on a freshly generated tree. + +The practical consequence is small, and the templates are already safe: `verification/verif/`, +`verification/target/`, `*.coma` and `.why3find/` are all in the templates' `.gitignore`, so a +clone or a CI checkout never starts with stale proof state — CI runs from a clean tree by +construction. Locally, the lesson is to treat proof artefacts as build output: don't move a tree +around with them attached, and if a proof result looks wrong, force re-translation before believing +it. `cargo creusot clean` is a no-op in the healthy case ("No dangling files found", exit 0). + +**The Ada workflow had the same kind of hole.** Not the same hole — the same *species*. `gnatprove` +is a frontend, not a toolchain: the release archive that job downloads contains a single binary, no +compiler and no `gprbuild`. Nothing in `proof.yml` installed those, so the job would have failed at +`gprbuild --version` one step later. `ci.yml` in the same template has installed `gnat gprbuild` +since it was written; `proof.yml` was added later and forgot. Both files being in the same directory +is what makes that findable — and it is not findable by reading either one alone. + +**Ada, re-checked on the rebuilt toolchain.** The `gnatprove` asset the Ada workflow installs was +downloaded and its SHA-256 checked against the value hard-coded in the workflow +(`28fc3583…f4017` — matched), then the proof was run end-to-end on a freshly generated template: +**35 checks proved, 0 unproved, exit 0** (`Adafix.Clamp` 1 check, `Adafix.Midpoint` 34). The +negative control fails as it should: + +``` +$ just proof # false postcondition: Clamp'Result in Lo .. Hi - 1 +neg_ada.ads:36:19: high: postcondition might fail +gnatprove: unproved check messages considered as errors +exit 1 +``` + +**Two environment traps that look like template bugs and are not.** Worth recording because both +cost time here and will cost time for anyone else running these proofs in a small container: + +- *Memory.* Translating `creusot-std` on a 2 GB, swapless box gets SIGKILLed ("signal: 9") partway + through — it looks like a slow build, then dies. Dropping debuginfo for the proof run + (`CARGO_PROFILE_DEV_DEBUG=0 CARGO_INCREMENTAL=0`) makes it fit, and translation then takes about + 35 seconds. CI runners have room; a small local VM may not. +- *Disk.* `/tmp` here is a 993 MB tmpfs, and filling it with build trees makes the **generator** + fail with `cp: error writing '…/.gitattributes': No space left on device`. That reads as a + template defect and is nothing of the sort: a full disk fails whichever step needs to write next. + Generate and build under a directory on the main filesystem, and check `df` before diagnosing. + +**Re-verified on the rebased tree.** Before this was handed over, the commits were rebased onto +current upstream `main` (upstream had moved on by seven commits, all of them CHANGELOG churn). A +rebase is a rewrite, so nothing was assumed about it: the whole toolchain was rebuilt from nothing +and both proofs plus both negative controls were re-run *through the generator*, on the rebased +tree, rather than in the repo's template directory. + +``` +tree under test: a35ef12 (= upstream main + the delivery commits) + +rust positive : "Proved (2 files) ✔" exit 0 +rust negative : false postcondition (half-sum + 1) exit 1 +ada positive : Total 35 checks, 35 (100%) proved exit 0 +ada negative : false postcondition (Clamp'Result in Lo .. Hi - 1) exit 1 + +aletheia : 83 + 52 = 135 tests pass, fmt clean, clippy -D warnings clean +estate : just check exit 0; just self-verify 26/26, Bronze + Silver ACHIEVED +``` + +That also closes the gap this document previously carried about the rebased tree not having been +tested. Two things the rebuild taught, both now in `toolchain-rebuild/rebuild-toolchain.sh`: + +- `cargo creusot` resolves `creusot-rustc` at + `$XDG_DATA_HOME/creusot/toolchains//bin/creusot-rustc` and refuses to run without it, + even when the binary is installed and on `PATH`. Installing Creusot's own binaries is not enough + on its own; the toolchain-dir placement is part of the contract. +- `rustup toolchain install stable --component rustfmt clippy` fails with "invalid toolchain name: + 'clippy'" — the second value is read as a toolchain, not a component. Several components need one + comma-separated value. This is the same failure mode as the `rust-toolchain` parsing bug in the CI + job, in a different disguise: a tool argument silently reinterpreted. + +**Still unproven.** Neither workflow has run on a GitHub runner. That caveat stays until it does: +the commands are known-good, but "known-good commands in the right order in a YAML file" is a +weaker claim than a green run, and the templates are not claiming the stronger one. + + +--- + +## Findings I did not fix, for your judgement + +1. ~~**`aletheia` does not honour `.gitignore` when scanning.**~~ **Fixed in this pass** — see + "Build output no longer breaks the gate" below. It turned out to be worse than a clean-tree + annoyance: it also meant the gate would fail in any CI job that ran it after a build. + +2. ~~**The sample-function names now differ across templates.**~~ **Looked at again, and kept — + the difference is load-bearing.** Rust and Ada use `midpoint` (`a + (b - a) / 2`, precondition + `a ≤ b`); Zig, Elixir and Haskell use `meanFloor` (`(a & b) + ((a ^ b) >> 1)`, *total*, no + precondition). Agda is a proofs library rather than a sample API, and always was. + + The split follows the toolchains, not taste. The bit-trick is the better API — it is total, and + it is the reason it was chosen originally — but Creusot has no bitvector theory and SPARK's + provers cannot discharge the identity, so a proof-carrying template cannot ship it. Unifying + would mean adding an `a ≤ b` precondition to three languages that do not need one, purely for + cosmetic symmetry, and would make those three strictly worse. + + So the six templates are not identical on purpose. Each README states which formulation it ships + and why; if you would rather have uniformity over totality, say so and it is a small change. + +3. **`agda/.github/workflows/ci.yml` installs the distro's Agda**, not the 2.6.4.3 that + `agda/.tool-versions` pins. They happened to be the same version here (Debian 13's `agda` is + 2.6.4.3), so the local run says nothing either way about a different base image. The typecheck + is simple enough that a patch-level difference is unlikely to matter, but it is a pin the + workflow does not honour. Building 2.6.4.3 from source in CI would take longer than the job's + whole timeout, so the fix would be to relax the pin in `.tool-versions` rather than chase it. + +4. **`aletheia/LICENSE` still says PMPL-1.0-or-later** while its sources say MPL-2.0. Carried over + from the first delivery; unchanged, since you had not asked for it. + +## Where the toolchains live + +Everything heavy is installed under `/usr/local/` (Rust at `/usr/local/cargo` + `/usr/local/rustup`, +Zig at `/usr/local/zig`, `just` at `/usr/local/bin`; the language packages come from apt). Nothing +in the repo depends on any of it — the templates need a prover only to run `just proof`, and that is +the point of the standalone requirement. + +**Correction, recorded because the first version of this section was wrong.** It said that installing +outside `/home/user` meant the toolchain would survive between sessions. That was tested by the +sandbox resetting, and it is false: everything outside the workspace was reclaimed — Rust, Cargo, +`just`, Zig, opam, Creusot, `gnatprove` — leaving only the workspace itself. The practical position +is that **no toolchain location is durable here**, so the recipes below are written to be re-run, not +to be relied on. What makes that survivable is the repo's own property: nothing in it needs any of +this until you ask for a proof or a real-language build. + +For the record, the layout the rebuild scripts create, so a re-run lands in the same place: + +| Piece | Location | +|---|---| +| Rust stable + pinned nightly | `/usr/local/rustup`, `/usr/local/cargo` | +| `just`, Zig | `/usr/local/bin`, `/usr/local/zig` | +| gnatprove 13.2.0-1 | `/usr/local/gnatprove` (release archive; it is not an Alire component and `alr install` does not exist) | +| Creusot source | `/usr/local/creusot` | +| Creusot's opam switch | `/usr/local/opam` (switch `creusot`) | +| Creusot runtime layout | `/usr/local/share/creusot` — `bin/{why3,why3find,alt-ergo,z3,cvc4,cvc5}`, `toolchains//bin/creusot-rustc`, `share/why3find/packages/creusot` | + +Two settings in that layout are load-bearing and easy to miss. `XDG_DATA_HOME` decides where +`cargo-creusot` looks for *everything* — `why3`, `why3find`, the prover binaries and `creusot-rustc` +itself — and the default (`~/.local/share`) is excluded from the workspace snapshot, so a Creusot +runtime installed there is doubly lost. Point it at `/usr/local/share` (or anywhere you control) and +`cargo creusot version` can be made to resolve all four provers. The second is `RUSTUP_TOOLCHAIN`: +`creusot-rustc` and `cargo creusot` must both run under Creusot's pinned nightly, not the default one. + +`gnatprove`'s CI asset is pinned by URL **and verifies its SHA-256** (`28fc3583…f4017`, checked +against the real download). + +## Follow-on verification log + +```bash +# all six, via the real generator, gated on a clean tree +for L in rust zig elixir haskell ada agda; do + create-template.sh "g-$L" -l "$L" && cd "g-$L" + aletheia . # Score: 26/26 (100.0%) — Bronze + Silver ACHIEVED + just check # exit 0 +done + +# proofs +cd g-rust && just proof # Proved (2 files) ✔ exit 0 +cd g-ada && just proof # Total 35 . 35 (100%) exit 0 + +# negative controls — both must fail +# (clamp postcondition weakened) → proof failed, exit 1 +# (midpoint identity + 1) → proof failed, exit 1 +# (Clamp postcondition weakened) → "unproved check messages considered as errors", exit 1 + +# air-gap, no network namespace at all +unshare -rn bash -c 'cd airrust && cargo build --offline && cargo test --offline' # ok +unshare -rn bash -c 'cd airada && gprbuild -p -P airada.gpr' # ok + +# aletheia itself +cargo test # 83 + 52 = 135 passed +cargo clippy --all-targets -- -D warnings # clean +cargo fmt --check # clean +cd .. && just check && just self-verify # exit 0, 26/26 + +# the .gitignore fix, end to end +just check && aletheia . # 26/26 AFTER a build (was 18/26, Bronze NOT MET) +# negative control: remove .gitignore from the same tree + # 18/26, Bronze NOT MET, flags obj/b__main.ads + +# the Creusot toolchain, rebuilt from nothing and then used +cargo creusot version # alt-ergo 2.6.2 / z3 4.15.3 / cvc4 1.8 / cvc5 1.3.1 — all resolved + # (before the `provers` component: all four "not found") +cd g-rust && just proof # Proved (2 files) ✔ exit 0 + # re-run after re-pinning Why3 to the commit creusot-deps.opam + # declares: Proved (2 files) ✔ exit 0 +# negative control on a fresh tree: midpoint identity + 1 + # Goal Coma.vc_midpoint: ✘ (4/5), 1 unproved file, exit 1 +# same negative control on a tree copied WITH its verif/ + target/: "Proved (2 files)", exit 0 + # then `touch verification/src/lib.rs` → fails correctly, exit 1 + # (templates .gitignore verif/ and target/, so CI never sees this) + +# the Ada proof, re-run on a regenerated template after fixing proof.yml +rm -rf obj/gnatprove && just proof # exit 0 +# obj/gnatprove/gnatprove.out: Clamp 1 check + Midpoint 34 checks proved, 0 unproved + +# the proof workflows: commands run for real, not simulated +python3 -c "import yaml; yaml.safe_load(open('.../proof.yml'))" # valid YAML for both +# rust-toolchain channel parsed from the clone → nightly-2026-08-03 +# why3/why3find pins derived from creusot-deps.opam (the hard-coded one had gone stale) +# gnatprove asset sha256 verified against the workflow's pinned value +# four defects found (three Rust, one Ada) — all fixed; neither job has run on a runner yet +``` diff --git a/aletheia/scripts/create-template.sh b/aletheia/scripts/create-template.sh index 0009f38..5579558 100755 --- a/aletheia/scripts/create-template.sh +++ b/aletheia/scripts/create-template.sh @@ -1,572 +1,492 @@ #!/usr/bin/env bash # SPDX-License-Identifier: MPL-2.0 -# Script to create RSR Bronze-compliant project template -# Usage: ./create-template.sh +# Copyright (c) Jonathan D.A. Jewell +# +# create-template.sh — scaffold an RSR v2 project for a Tier-1 estate language. +# +# STANDALONE BY CONSTRUCTION: this generator reads only the template tree +# that ships beside it and writes only into the target directory. It makes +# no network calls, runs no package manager, and downloads nothing. A +# scaffolded project consequently passes `aletheia` Bronze AND Silver on +# day one with no hand edits, for every language it supports. +# +# Retired v1 shape this script no longer produces (see issue #186): +# LICENSE.txt / lowercase justfile / flake.nix / .gitlab-ci.yml / +# Python + flake8 / remote `curl` of licence texts. set -euo pipefail -# Colors -RED='\033[0;31m' -GREEN='\033[0;32m' -YELLOW='\033[1;33m' -BLUE='\033[0;34m' -NC='\033[0m' +# Colours (suppressed when not a terminal, so CI logs stay clean) +if [ -t 1 ]; then + RED='\033[0;31m'; GREEN='\033[0;32m'; YELLOW='\033[1;33m' + BLUE='\033[0;34m'; NC='\033[0m' +else + RED=''; GREEN=''; YELLOW=''; BLUE=''; NC='' +fi -# Configuration -SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -TEMPLATE_DIR="$(dirname "$SCRIPT_DIR")/templates" - -log_info() { echo -e "${GREEN}[INFO]${NC} $1"; } -log_warn() { echo -e "${YELLOW}[WARN]${NC} $1"; } -log_error() { echo -e "${RED}[ERROR]${NC} $1"; } -log_step() { echo -e "${BLUE}[STEP]${NC} $1"; } - -usage() { - cat < [language] - -Create an RSR Bronze-compliant project from template. +log_info() { printf '%b\n' "${GREEN}[INFO]${NC} $1"; } +log_warn() { printf '%b\n' "${YELLOW}[WARN]${NC} $1"; } +log_error() { printf '%b\n' "${RED}[ERROR]${NC} $1" >&2; } +log_step() { printf '%b\n' "${BLUE}[STEP]${NC} $1"; } -Arguments: - project-name Name of the new project - language Programming language (rust, python, typescript, go) - Default: rust - -Examples: - $0 my-awesome-project rust - $0 data-analyzer python - $0 web-app typescript - -Supported Languages: - - rust Rust project with Cargo - - python Python project with pyproject.toml - - typescript TypeScript project with package.json - - go Go project with go.mod - -This will create: - - All required RSR Bronze documentation - - .well-known directory with security.txt - - Build automation (Justfile, flake.nix) - - Basic CI/CD configuration - - Source structure (src/, tests/) - - License files (MIT + Apache-2.0) -EOF - exit 1 +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +ALETHEIA_DIR="$(dirname "$SCRIPT_DIR")" +TEMPLATE_ROOT="$ALETHEIA_DIR/templates" + +# --------------------------------------------------------------------------- +# Language table +# +# Every language shares templates/common/ (docs, licence texts, .well-known, +# the estate CI gates) and adds templates// on top. The values below +# are the only things that differ; keeping them here means the estate's +# language policy is stated once, not six times. +# +# Tier-1 languages per hyperpolymath/standards (RSR_OUTLINE: "Tier 1 (Gold): +# Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda"). +# --------------------------------------------------------------------------- +LANGS="rust zig elixir haskell ada agda" + +lang_display() { + case "$1" in + rust) echo "Rust/Creusot" ;; + zig) echo "Zig" ;; + elixir) echo "Elixir" ;; + haskell) echo "Haskell" ;; + ada) echo "Ada/SPARK" ;; + agda) echo "Agda" ;; + esac } -create_directory_structure() { - local project_name=$1 - - log_step "Creating directory structure..." - - mkdir -p "$project_name"/{src,tests,.well-known,docs,scripts} - - log_info "Directory structure created" +lang_policy() { + case "$1" in + rust) echo 'Rust here is always *Rust/Creusot*: Rust plus the Creusot deductive verifier. `just proof` translates `+src/impl.rs+` and discharges every obligation with Why3/Z3/CVC5, exiting non-zero on any unproved goal; the main crate stays zero-dependency because the specifications are gated behind `+cfg(creusot)+`.' ;; + zig) echo 'Zig is a Tier-1 estate language. The build is dependency-free: `zig build` compiles from this tree alone, and the Zig compiler ships its own libc, so there is nothing else to install.' ;; + elixir) echo 'Elixir is a Tier-1 estate language (BEAM/OTP). The project carries no Hex dependencies, so `mix compile` and `mix test` run with no network and nothing to fetch.' ;; + haskell) echo 'Haskell is a Tier-1 estate language. The package depends only on `base`, which ships with GHC, so `cabal build --offline` resolves with no package index and no network.' ;; + ada) echo 'Ada here is *Ada/SPARK*: the core package declares `+pragma SPARK_Mode (On);+` and its contracts are statically proved by `gnatprove` at proof level 2, not merely checked at run time. The project builds with GNAT and plain GPR projects — no Alire, no crate index, nothing to fetch.' ;; + agda) echo 'Agda is a Tier-1 estate language, and the estate formal-methods emphasis (Coq, Agda, SPARK) makes it a first-class target. Typechecking *is* the verification: these modules import only `Agda.Builtin`, so there is no stdlib to resolve and `agda` proves them offline.' ;; + esac } -create_documentation() { - local project_name=$1 - - log_step "Creating documentation files..." - - # README.md - cat > "$project_name/README.md" < RSR Bronze-compliant project template - -## 🚀 Quick Start - -\`\`\`bash -# Build -just build - -# Test -just test - -# Verify RSR compliance -aletheia . -\`\`\` - -## 📊 RSR Compliance - -**Level**: Bronze ✅ - -This project maintains RSR Bronze-level compliance: -- ✅ Type Safety -- ✅ Memory Safety -- ✅ Complete Documentation -- ✅ Security-First (.well-known) -- ✅ Build System -- ✅ Testing - -## 🤝 Contributing - -See [CONTRIBUTING.md](../../.github/CONTRIBUTING.md) - -## 📜 License - -Dual-licensed under MIT OR Apache-2.0 - -See [LICENSE-MIT.txt](LICENSE-MIT.txt) and [LICENSE-APACHE.txt](LICENSE-APACHE.txt) -EOF - - # LICENSE files - curl -sSf https://opensource.org/licenses/MIT -o "$project_name/LICENSE-MIT.txt" 2>/dev/null || \ - echo "MIT License" > "$project_name/LICENSE-MIT.txt" - - curl -sSf https://www.apache.org/licenses/LICENSE-2.0.txt -o "$project_name/LICENSE-APACHE.txt" 2>/dev/null || \ - echo "Apache License 2.0" > "$project_name/LICENSE-APACHE.txt" - - cat > "$project_name/LICENSE.txt" < "$project_name/SECURITY.md" < "$project_name/CONTRIBUTING.md" < "$project_name/CODE_OF_CONDUCT.md" < "$project_name/MAINTAINERS.md" < "$project_name/CHANGELOG.md" < "$project_name/.well-known/security.txt" < "$project_name/.well-known/ai.txt" < "$project_name/.well-known/humans.txt" < "$project_name/justfile" < "$project_name/justfile" < "$project_name/justfile" < "$project_name/flake.nix" < [options] - log_step "Creating $language-specific files..." +Scaffold an RSR v2-compliant project for a Tier-1 estate language. The +generated tree passes `aletheia` Bronze AND Silver with no hand edits, and +needs no network: the scaffold embeds every licence text and downloads +nothing. - case "$language" in - rust) - cat > "$project_name/Cargo.toml" < Template language (default: rust) + --list-languages List supported languages and exit + -d, --description One-line project description + --author Copyright holder / maintainer name + --email Maintainer email + --repo-url Canonical repository URL + --security-contact Vulnerability disclosure contact + --conduct-contact Code-of-conduct contact + --no-git Do not initialise a git repository + --verify Run `aletheia` on the result (must be on PATH) + --force Write into a directory that already exists + -h, --help Show this message + +Supported languages (Tier-1 per hyperpolymath/standards): + rust Rust/Creusot — zero-dependency crate + Creusot proof crate + zig Zig 0.16 — build.zig, no package manager in the build path + elixir Elixir 1.18 / OTP 27 — mix, empty deps + haskell GHC 9.6 — cabal, `base` only + ada Ada — GNAT + plain GPR projects (no Alire) + agda Agda — machine-checked proofs, Agda.Builtin only + +Every template provides (v2 shape): + LICENSE + LICENSES/ MPL-2.0 (+ CC-BY-SA-4.0 for docs), full texts + Justfile capital J, real recipes, failing loudly + source + tests working code and a real test gate + .github/workflows/ CI, hypatia-scan, governance (actions.lock) + .machine_readable/ rsr-profile.a2ml capability declaration + .well-known/ security.txt, ai.txt, humans.txt + 0-AI-MANIFEST.a2ml agent front door + Documentation README.adoc, SECURITY, CONTRIBUTING, CoC, + CHANGELOG, MAINTAINERS + +Every template deliberately does NOT provide (retired v1 shape): + LICENSE.txt, lowercase justfile, flake.nix, .gitlab-ci.yml, + Makefile/Dockerfile, remote licence downloads + +NOT SUPPORTED, deliberately: + AffineScript — the estate successor to ReScript (`.res` -> `.affine`). + It has no verifiable toolchain yet, so a scaffold could not pass its own + `just check`; shipping one would be exactly the fake gate this estate + bans. Add it here once its compiler is installable and pinned. -[dependencies] -# Zero dependencies for RSR Bronze compliance +Examples: + create-template.sh my-service + create-template.sh my-service -l zig -d "A small service" --verify + create-template.sh my-service --no-git --repo-url https://codeberg.org/me/my-service EOF - - cat > "$project_name/src/main.rs" < "$project_name/tests/integration_test.rs" < "$project_name/pyproject.toml" < "$project_name/src/__init__.py" <<'EOF' -"""Package initialization.""" -EOF - - cat > "$project_name/src/main.py" <<'EOF' -"""Main module.""" - -def main() -> None: - """Main entry point.""" - print("Hello!") - -if __name__ == "__main__": - main() -EOF - - cat > "$project_name/tests/test_main.py" <<'EOF' -"""Tests for main module.""" - -def test_example() -> None: - """Example test.""" - assert True -EOF - ;; - esac - log_info "$language files created" +# --------------------------------------------------------------------------- +# Validation +# --------------------------------------------------------------------------- +lang_supported() { + for l in $LANGS; do [ "$l" = "$1" ] && return 0; done + return 1 } -create_ci_cd() { - local project_name=$1 - - log_step "Creating CI/CD configuration..." +validate() { + case "$PROJECT_NAME" in + *[!a-zA-Z0-9._-]*|"") + log_error "invalid project name: '$PROJECT_NAME'" + log_error "use letters, digits, dot, underscore or hyphen" + exit 2 ;; + -*) + log_error "project name may not start with a hyphen: '$PROJECT_NAME'" + exit 2 ;; + esac - cat > "$project_name/.gitlab-ci.yml" < stdout. +subst() { + sed \ + -e "s|@@PROJECT_NAME@@|$E_PROJECT_NAME|g" \ + -e "s|@@MOD_NAME@@|$E_MOD_NAME|g" \ + -e "s|@@CRATE_NAME@@|$E_MOD_NAME|g" \ + -e "s|@@MOD_CAMEL@@|$E_MOD_CAMEL|g" \ + -e "s|@@MOD_ADA@@|$E_MOD_ADA|g" \ + -e "s|@@VERSION@@|0.1.0|g" \ + -e "s|@@PROJECT_DESCRIPTION@@|$E_DESCRIPTION|g" \ + -e "s|@@REPO_URL@@|$E_REPO_URL|g" \ + -e "s|@@AUTHOR_NAME@@|$E_AUTHOR_NAME|g" \ + -e "s|@@AUTHOR_EMAIL@@|$E_AUTHOR_EMAIL|g" \ + -e "s|@@SECURITY_CONTACT@@|$E_SECURITY_CONTACT|g" \ + -e "s|@@CONDUCT_CONTACT@@|$E_CONDUCT_CONTACT|g" \ + -e "s|@@DATE@@|$E_DATE|g" \ + -e "s|@@SECURITY_EXPIRES@@|$E_SECURITY_EXPIRES|g" \ + -e "s|@@LANG_DISPLAY@@|$E_LANG_DISPLAY|g" \ + -e "s|@@LANG_POLICY@@|$E_LANG_POLICY|g" \ + -e "s|@@LANG_INVARIANT@@|$E_LANG_INVARIANT|g" \ + -e "s|@@DEP_INVARIANT@@|$E_DEP_INVARIANT|g" \ + -e "s|@@STANDALONE_INVARIANT@@|$E_STANDALONE|g" \ + -e "s|@@LANG_GITATTR_LINE@@|$E_LANG_GITATTR|g" +} - log_step "Finalizing project..." +# Copy one template layer into the target, then render every file. Called +# once for templates/common and once for templates/; the language +# layer is copied second so it wins where both define a path. +copy_layer() { + local layer="$1" target="$2" + local src rel + while IFS= read -r src; do + rel="${src#"$layer"/}" + # Recreate the directory skeleton (mkdir -p handles nesting). + mkdir -p "$target/$(dirname "$rel")" + cp "$src" "$target/$rel" + # Preserve the executable bit. Written as an `if`, not + # `[ -x ] && chmod`, because under `set -e` a failing test as the + # last command of a loop body would abort the whole render. + if [ -x "$src" ]; then + chmod +x "$target/$rel" + fi + done < <(find "$layer" -type f) +} - cd "$project_name" - git init - git add . - git commit -m "chore: initial RSR Bronze-compliant project structure" +render_tree() { + local target="$1" + + # File contents. + local f + while IFS= read -r f; do + subst < "$f" > "$f.tmp" + mv "$f.tmp" "$f" + done < <(find "$target" -type f) + + # Path names, deepest first, so renamed directories stay consistent. + local p new + while IFS= read -r p; do + new="$(printf '%s' "$p" | subst)" + if [ "$p" != "$new" ]; then + mv "$p" "$new" + fi + done < <(find "$target" -depth -name '*@@*') +} - log_info "Git repository initialized" +finish() { + local target="$1" + + if [ "$INIT_GIT" -eq 1 ]; then + log_step "Initialising git repository..." + ( cd "$target" + git init -q 2>/dev/null || true + # Only set local identity when the user has none, so the initial + # commit cannot fail on a fresh machine. + git config user.email >/dev/null 2>&1 || git config user.email "$AUTHOR_EMAIL" + git config user.name >/dev/null 2>&1 || git config user.name "$AUTHOR_NAME" + git add -A + git commit -q -m "chore: initial commit from aletheia v2 Bronze template" \ + || log_warn "initial commit skipped" + ) + log_info "Git repository initialised" + fi - echo "" - log_info "✅ Project created successfully!" - echo "" - echo "Next steps:" - echo " 1. cd $project_name" - echo " 2. Update contact information in:" - echo " - .well-known/security.txt" - echo " - SECURITY.md" - echo " - MAINTAINERS.md" - echo " 3. Build: just build" - echo " 4. Test: just test" - echo " 5. Verify RSR compliance: aletheia ." - echo "" + if [ "$RUN_VERIFY" -eq 1 ]; then + log_step "Verifying RSR compliance..." + if command -v aletheia >/dev/null 2>&1; then + if aletheia "$target"; then + log_info "Compliance check passed" + else + log_warn "Compliance check reported failures (see output above)" + fi + else + log_warn "aletheia not on PATH — skipping verification" + log_warn "build it with: just build (from the maa-framework root)" + fi + fi } main() { - if [ $# -lt 1 ]; then - usage + parse_args "$@" + validate + + # Derived values + MOD_NAME="$(printf '%s' "$PROJECT_NAME" | tr '[:upper:]' '[:lower:]' | tr '-' '_')" + MOD_CAMEL="$(printf '%s' "$PROJECT_NAME" | sed -E 's/[^a-zA-Z0-9]+/ /g' \ + | awk '{ for (i = 1; i <= NF; i++) printf toupper(substr($i,1,1)) substr($i,2) }')" + # Ada unit names are underscore-joined capitalised segments. Deriving this + # from MOD_CAMEL by inserting underscores at case boundaries is wrong for + # single-letter segments ("g-ada" would give "GAda", not "G_Ada"), which + # then makes GNAT look for gada.ads while the template ships g_ada.ads. + MOD_ADA="$(printf '%s' "$PROJECT_NAME" | sed -E 's/[^a-zA-Z0-9]+/ /g' \ + | awk '{ for (i = 1; i <= NF; i++) printf "%s%s", (i > 1 ? "_" : ""), toupper(substr($i,1,1)) substr($i,2) }')" + + if [ -z "$DESCRIPTION" ]; then + DESCRIPTION="An RSR v2-compliant $(lang_display "$LANGUAGE") project." fi - - local project_name=$1 - local language=${2:-rust} - - if [ -d "$project_name" ]; then - log_error "Directory '$project_name' already exists" + if [ -z "$REPO_URL" ]; then + REPO_URL="https://github.com/hyperpolymath/$PROJECT_NAME" + fi + if [ -z "$SECURITY_CONTACT" ]; then + SECURITY_CONTACT="$AUTHOR_EMAIL" + fi + if [ -z "$CONDUCT_CONTACT" ]; then + CONDUCT_CONTACT="$AUTHOR_EMAIL" + fi + DATE="$(date -u +%Y-%m-%d)" + SECURITY_EXPIRES="$(date -u -d '+1 year' +%Y-%m-%dT%H:%M:%S.000Z 2>/dev/null \ + || date -u -v+1y +%Y-%m-%dT%H:%M:%S.000Z)" + + E_PROJECT_NAME="$(sed_escape "$PROJECT_NAME")" + E_MOD_NAME="$(sed_escape "$MOD_NAME")" + E_MOD_CAMEL="$(sed_escape "$MOD_CAMEL")" + E_MOD_ADA="$(sed_escape "$MOD_ADA")" + E_DESCRIPTION="$(sed_escape "$DESCRIPTION")" + E_REPO_URL="$(sed_escape "$REPO_URL")" + E_AUTHOR_NAME="$(sed_escape "$AUTHOR_NAME")" + E_AUTHOR_EMAIL="$(sed_escape "$AUTHOR_EMAIL")" + E_SECURITY_CONTACT="$(sed_escape "$SECURITY_CONTACT")" + E_CONDUCT_CONTACT="$(sed_escape "$CONDUCT_CONTACT")" + E_DATE="$(sed_escape "$DATE")" + E_SECURITY_EXPIRES="$(sed_escape "$SECURITY_EXPIRES")" + E_LANG_DISPLAY="$(sed_escape "$(lang_display "$LANGUAGE")")" + E_LANG_POLICY="$(sed_escape "$(lang_policy "$LANGUAGE")")" + E_LANG_INVARIANT="$(sed_escape "$(lang_invariant "$LANGUAGE")")" + E_DEP_INVARIANT="$(sed_escape "$(lang_dep_invariant "$LANGUAGE")")" + E_STANDALONE="$(sed_escape 'the build fetches nothing. Do not add network calls to the build, test, or scaffolding path.')" + E_LANG_GITATTR="$(sed_escape "$(lang_gitattr "$LANGUAGE")")" + + log_info "Creating RSR v2 project: $PROJECT_NAME ($LANGUAGE — $(lang_display "$LANGUAGE"))" + log_info "Template: v2 Bronze (standalone — no downloads)" + printf '\n' + + if [ -e "$PROJECT_NAME" ]; then + rm -rf "$PROJECT_NAME" + fi + mkdir -p "$PROJECT_NAME" + + log_step "Rendering template tree..." + copy_layer "$TEMPLATE_ROOT/common" "$PROJECT_NAME" + copy_layer "$TEMPLATE_ROOT/$LANGUAGE" "$PROJECT_NAME" + render_tree "$PROJECT_NAME" + + # A leftover placeholder means a template file references a token the + # generator does not know about. Fail loudly rather than ship it. + if grep -rl '@@' "$PROJECT_NAME" >/dev/null 2>&1; then + log_error "unresolved template placeholder(s) in:" + grep -rl '@@' "$PROJECT_NAME" | sed 's/^/ /' >&2 + log_error "the generator and the template tree are out of sync" exit 1 fi + log_info "Rendered $(find "$PROJECT_NAME" -type f | wc -l | tr -d ' ') files" - log_info "Creating RSR Bronze-compliant project: $project_name ($language)" - echo "" + finish "$PROJECT_NAME" - create_directory_structure "$project_name" - create_documentation "$project_name" - create_well_known "$project_name" - create_build_system "$project_name" "$language" - create_language_specific "$project_name" "$language" - create_ci_cd "$project_name" - finalize "$project_name" + printf '\n' + log_info "Project created: $PROJECT_NAME" + printf '\n' + echo "Next steps:" + echo " cd $PROJECT_NAME" + echo " just check # build, test, lint (offline)" + echo " just verify # RSR compliance with aletheia" + echo "" + echo "Language: $(lang_display "$LANGUAGE") — see README.adoc for the" + echo "toolchain and the offline guarantees." + echo "" + echo "Before publishing, review:" + echo " .well-known/security.txt disclosure contact and expiry" + echo " .machine_readable/rsr-profile.a2ml declared capabilities" + echo " MAINTAINERS.adoc ownership" + echo "" } main "$@" diff --git a/aletheia/src/checks.rs b/aletheia/src/checks.rs index e2e7e61..69f0925 100644 --- a/aletheia/src/checks.rs +++ b/aletheia/src/checks.rs @@ -14,11 +14,11 @@ //! explicitly out of scope and deferred to the hypatia oracle; see //! [`LOCAL_SUBSET_NOTE`]. Aletheia is non-normative by design. -use std::cell::Cell; +use std::cell::{Cell, OnceCell}; use std::fs; use std::path::{Path, PathBuf}; -use crate::config::{Config, IgnoreConfig}; +use crate::config::{Config, GitIgnore, IgnoreConfig}; use crate::types::*; /// Provenance of the check inventory: the upstream single source of @@ -368,6 +368,72 @@ fn read_head(path: &Path, max_bytes: u64) -> Option { Some(content) } +/// One traversal's results, bucketed by the extension filters the checks +/// need (issue #197). +/// +/// WHY BUCKETS: each check used to run its own `walk_files`, so a single +/// `verify` performed seven full directory traversals. All seven walked the +/// same tree in the same order and differed only in which files they +/// collected, so a single traversal can fill every bucket at once. The +/// saving is in the traversal itself — `read_dir` plus `file_type` per +/// entry — not in the cheap extension filter applied afterwards. +/// +/// BUDGET SEMANTICS ARE UNCHANGED. A bucket accepts at most +/// `MAX_SCAN_FILES` *matches of its own*, exactly as +/// `walk_files(Some(exts))` counted only files passing its filter rather +/// than every file seen. When a bucket is full it stops growing, and the +/// traversal continues so the remaining buckets still receive their own +/// first `MAX_SCAN_FILES` matches — which is what the separate walks gave +/// them. +#[derive(Default)] +struct ScanSet { + /// Every file (checks with no extension filter). + all: Vec, + /// `SPDX_EXTENSIONS` matches. + spdx: Vec, + /// `SECRET_SCAN_EXTENSIONS` matches. + secret: Vec, + /// `BANNED_LANGUAGE_EXTENSIONS` matches. + banned: Vec, + /// Set once a file was refused because its bucket was full — i.e. the + /// results really are partial. Drives the truncation warning. + capped: bool, + /// `.gitignore` rules covering the directories walked so far. Maintained + /// as a stack: rules are pushed when the walk enters a directory and + /// truncated on the way out, so a nested file only governs its own + /// subtree. Filled during the single traversal, which is why this lives + /// here rather than in a second pass over the tree (issue #197). + ignores: GitIgnore, +} + +impl ScanSet { + /// Offer one file to every bucket whose filter accepts it. + /// + /// Extensionless files (empty `ext`) land only in `all`, matching the + /// old filtered walks, which skipped them. + fn offer(&mut self, path: &Path, ext: &str) { + Self::push(&mut self.all, path, &mut self.capped); + if SPDX_EXTENSIONS.contains(&ext) { + Self::push(&mut self.spdx, path, &mut self.capped); + } + if SECRET_SCAN_EXTENSIONS.contains(&ext) { + Self::push(&mut self.secret, path, &mut self.capped); + } + if BANNED_LANGUAGE_EXTENSIONS.contains(&ext) { + Self::push(&mut self.banned, path, &mut self.capped); + } + } + + /// Push into one bucket unless it has reached its per-check budget. + fn push(bucket: &mut Vec, path: &Path, capped: &mut bool) { + if bucket.len() < MAX_SCAN_FILES { + bucket.push(path.to_path_buf()); + } else { + *capped = true; + } + } +} + /// Filesystem scanner: bounded recursive walks honouring skip dirs, /// submodule boundaries and `[ignore]` globs. Never follows symlinks. struct Scanner<'a> { @@ -375,6 +441,9 @@ struct Scanner<'a> { ignore: &'a IgnoreConfig, submodules: &'a [String], truncated: Cell, + /// Memoised single-traversal file buckets (issue #197). Filled on first + /// use; every check then reads from it instead of re-walking the tree. + files: OnceCell, } impl<'a> Scanner<'a> { @@ -395,24 +464,26 @@ impl<'a> Scanner<'a> { rel.is_empty() || self.under_submodule(rel) || self.ignore.is_ignored(rel) } - /// Recursive walk collecting files. `exts`, when `Some`, restricts - /// to those (lowercased) extensions; `None` collects every file. - fn walk_into(&self, dir: &Path, depth: u32, exts: Option<&[&str]>, out: &mut Vec) { - if depth > MAX_SCAN_DEPTH || out.len() >= MAX_SCAN_FILES { - if out.len() >= MAX_SCAN_FILES { - self.truncated.set(true); - } + /// Recursive walk filling every bucket in one pass. Depth, skip-dir, + /// submodule and ignore rules are identical to the former per-check + /// walks, so each bucket receives exactly the files its own walk saw. + fn walk_into_set(&self, dir: &Path, depth: u32, set: &mut ScanSet) { + if depth > MAX_SCAN_DEPTH { return; } let entries = match fs::read_dir(dir) { Ok(entries) => entries, Err(_) => return, }; + // Rules from this directory's `.gitignore` apply to everything at or + // below it, so load them before visiting any entry. Popping on the way + // out keeps a nested file scoped to its own subtree. + let mark = set.ignores.len(); + if let Ok(text) = fs::read_to_string(dir.join(".gitignore")) { + let base = self.rel(dir); + set.ignores.push_file(&base, &text); + } for entry in entries.flatten() { - if out.len() >= MAX_SCAN_FILES { - self.truncated.set(true); - return; - } let path = entry.path(); let rel = self.rel(&path); if self.skipped(&rel) { @@ -426,44 +497,81 @@ impl<'a> Scanner<'a> { if file_type.is_symlink() { continue; } + // Ask the type-aware question: a directory-only rule such as + // `obj/` must match the directory `obj` but not a file of the + // same name. + let ignored = if file_type.is_dir() { + set.ignores.is_ignored_dir(&rel) + } else { + set.ignores.is_ignored(&rel) + }; + if ignored { + continue; + } if file_type.is_dir() { let skip = path .file_name() .and_then(|name| name.to_str()) .is_some_and(|name| SKIP_DIR_NAMES.contains(&name)); if !skip { - self.walk_into(&path, depth + 1, exts, out); + self.walk_into_set(&path, depth + 1, set); } } else if file_type.is_file() { - if let Some(wanted) = exts { - let ext = path - .extension() - .and_then(|e| e.to_str()) - .unwrap_or_default() - .to_ascii_lowercase(); - if !wanted.iter().any(|w| *w == ext) { - continue; - } - } - out.push(path); + let ext = path + .extension() + .and_then(|e| e.to_str()) + .unwrap_or_default() + .to_ascii_lowercase(); + set.offer(&path, &ext); } } + set.ignores.truncate(mark); } - fn walk_files(&self, exts: Option<&[&str]>) -> Vec { - let mut out = Vec::new(); - self.walk_into(self.root, 0, exts, &mut out); - out + /// The repository's files, bucketed. Computed once per `Scanner`, so + /// the seven checks that need file lists share one traversal. + fn files(&self) -> &ScanSet { + self.files.get_or_init(|| { + let mut set = ScanSet::default(); + self.walk_into_set(self.root, 0, &mut set); + if set.capped { + self.truncated.set(true); + } + set + }) + } + + /// Every file (checks with no extension filter). + fn all_files(&self) -> &[PathBuf] { + &self.files().all + } + + /// Files with an extension scanned for SPDX headers. + fn spdx_files(&self) -> &[PathBuf] { + &self.files().spdx + } + + /// Files with an extension additionally scanned for secrets. + fn secret_files(&self) -> &[PathBuf] { + &self.files().secret + } + + /// Files with an estate-banned language extension. + fn banned_files(&self) -> &[PathBuf] { + &self.files().banned } /// Look up a file under several candidate relative paths. fn presence(&self, candidates: &[&str]) -> Presence { + // Forces the (memoised) traversal so the `.gitignore` rules are loaded; + // this is a no-op once the scan has run. + let ignores = &self.files().ignores; let mut saw_ignored = false; for candidate in candidates { if file_exists(self.root, candidate) { return Presence::Found; } - if self.ignore.is_ignored(candidate) { + if self.ignore.is_ignored(candidate) || ignores.is_ignored(candidate) { saw_ignored = true; } } @@ -660,13 +768,13 @@ fn check_justfile(scanner: &Scanner) -> Outcome { /// 1.1.3 no-makefile (+ Mustfile: no Dockerfiles). fn check_no_makefile(scanner: &Scanner) -> Outcome { let mut offenders = Vec::new(); - for path in scanner.walk_files(None) { + for path in scanner.all_files() { if path .file_name() .and_then(|name| name.to_str()) .is_some_and(|name| BANNED_BUILD_FILES.contains(&name)) { - offenders.push(scanner.rel(&path)); + offenders.push(scanner.rel(path)); } } if offenders.is_empty() { @@ -750,8 +858,8 @@ fn check_gitignore(scanner: &Scanner) -> Outcome { /// 4.1.1 spdx-headers: SPDX headers on all scanned source files. fn check_spdx_headers(scanner: &Scanner) -> Outcome { let mut missing = Vec::new(); - for path in scanner.walk_files(Some(SPDX_EXTENSIONS)) { - let headed = read_head(&path, SPDX_HEAD_BYTES) + for path in scanner.spdx_files() { + let headed = read_head(path, SPDX_HEAD_BYTES) .map(|content| { content .lines() @@ -760,7 +868,7 @@ fn check_spdx_headers(scanner: &Scanner) -> Outcome { }) .unwrap_or(false); if !headed { - missing.push(scanner.rel(&path)); + missing.push(scanner.rel(path)); } } if missing.is_empty() { @@ -784,20 +892,20 @@ fn check_spdx_headers(scanner: &Scanner) -> Outcome { /// 4.1.2 no-secrets: no committed secret files or key material. fn check_no_secrets(scanner: &Scanner) -> Outcome { let mut offenders = Vec::new(); - for path in scanner.walk_files(None) { + for path in scanner.all_files() { if path .file_name() .and_then(|name| name.to_str()) .is_some_and(|name| SECRET_FILENAMES.contains(&name)) { - offenders.push(scanner.rel(&path)); + offenders.push(scanner.rel(path)); } } let markers = secret_markers(); - for path in scanner.walk_files(Some(SECRET_SCAN_EXTENSIONS)) { - if let Some(content) = read_head(&path, MAX_CONTENT_BYTES) { + for path in scanner.secret_files() { + if let Some(content) = read_head(path, MAX_CONTENT_BYTES) { if markers.iter().any(|m| content.contains(m)) { - offenders.push(scanner.rel(&path)); + offenders.push(scanner.rel(path)); } } } @@ -817,7 +925,7 @@ fn check_no_secrets(scanner: &Scanner) -> Outcome { /// 5.1.1–5.1.5 language bans: no Python/TS/ReScript/Go/V sources. fn check_language_policy(scanner: &Scanner) -> Outcome { let mut offenders = Vec::new(); - for path in scanner.walk_files(Some(BANNED_LANGUAGE_EXTENSIONS)) { + for path in scanner.banned_files() { let ext = path .extension() .and_then(|e| e.to_str()) @@ -825,14 +933,14 @@ fn check_language_policy(scanner: &Scanner) -> Outcome { .to_ascii_lowercase(); if ext == "v" { // `.v` is shared with Coq: only flag likely V-lang. - let suspect = read_head(&path, MAX_CONTENT_BYTES) + let suspect = read_head(path, MAX_CONTENT_BYTES) .is_some_and(|content| v_file_is_suspect(&content)); if suspect { - offenders.push(scanner.rel(&path)); + offenders.push(scanner.rel(path)); } continue; } - offenders.push(scanner.rel(&path)); + offenders.push(scanner.rel(path)); } if offenders.is_empty() { Outcome::pass() @@ -852,15 +960,15 @@ fn check_language_policy(scanner: &Scanner) -> Outcome { /// governance): runtime deps accompanied by a Bun lockfile pass. fn check_no_node_runtime(scanner: &Scanner) -> Outcome { let mut offenders = Vec::new(); - for path in scanner.walk_files(None) { + for path in scanner.all_files() { if path .file_name() .and_then(|name| name.to_str()) .is_some_and(|name| name == "package.json") { - if let Some(content) = read_head(&path, MAX_CONTENT_BYTES) { - if package_json_has_runtime_deps(&content) && !has_bun_lockfile(&path) { - offenders.push(scanner.rel(&path)); + if let Some(content) = read_head(path, MAX_CONTENT_BYTES) { + if package_json_has_runtime_deps(&content) && !has_bun_lockfile(path) { + offenders.push(scanner.rel(path)); } } } @@ -1249,7 +1357,7 @@ fn check_reuse(scanner: &Scanner) -> Outcome { /// 6.1.5 no-silent-skip (Gold): no `|| echo SKIP` silent-green recipes. fn check_no_silent_skip(scanner: &Scanner) -> Outcome { let mut offenders = Vec::new(); - for path in scanner.walk_files(None) { + for path in scanner.all_files() { let is_recipe = path .file_name() .and_then(|name| name.to_str()) @@ -1260,9 +1368,9 @@ fn check_no_silent_skip(scanner: &Scanner) -> Outcome { if !(is_recipe || is_script) { continue; } - if let Some(content) = read_head(&path, MAX_CONTENT_BYTES) { + if let Some(content) = read_head(path, MAX_CONTENT_BYTES) { if content.lines().any(silent_skip_line) { - offenders.push(scanner.rel(&path)); + offenders.push(scanner.rel(path)); } } } @@ -1347,6 +1455,7 @@ pub fn verify_repository(repo_path: &Path, config: &Config) -> ComplianceReport ignore: &config.ignore, submodules: &submodules, truncated: Cell::new(false), + files: OnceCell::new(), }; // (id, category, item, tier, check). Display order follows this table. @@ -1928,6 +2037,66 @@ mod tests { assert!(parse_gitmodules_content("path =\n").is_empty()); } + #[test] + fn test_scan_set_cap_is_per_bucket() { + // Filling `all` to its cap must not consume the budget of the + // extension-filtered buckets: each check keeps its own allowance, + // exactly as the per-check walks did (issue #197). + let mut set = ScanSet::default(); + for _ in 0..(MAX_SCAN_FILES + 25) { + set.offer(Path::new("/repo/extensionless"), ""); + } + assert_eq!(set.all.len(), MAX_SCAN_FILES); + assert_eq!(set.spdx.len(), 0); + assert_eq!(set.secret.len(), 0); + assert_eq!(set.banned.len(), 0); + assert!(set.capped, "refusing a file must flag truncation"); + } + + #[test] + fn test_scan_set_filtered_buckets_cap_independently() { + // `.rs` matches the SPDX and secret buckets; `.go` matches only the + // banned bucket. Each fills to its own cap, and one reaching the + // limit does not shorten another's list. + let mut set = ScanSet::default(); + for _ in 0..(MAX_SCAN_FILES + 25) { + set.offer(Path::new("/repo/main.rs"), "rs"); + set.offer(Path::new("/repo/app.go"), "go"); + } + assert_eq!(set.all.len(), MAX_SCAN_FILES); + assert_eq!(set.spdx.len(), MAX_SCAN_FILES); + assert_eq!(set.secret.len(), MAX_SCAN_FILES); + assert_eq!(set.banned.len(), MAX_SCAN_FILES); + assert!(set.capped); + } + + #[test] + fn test_scan_set_extensionless_files_only_reach_all() { + let mut set = ScanSet::default(); + set.offer(Path::new("/repo/Makefile"), ""); + set.offer(Path::new("/repo/Justfile"), ""); + assert_eq!(set.all.len(), 2); + assert!(set.spdx.is_empty() && set.secret.is_empty() && set.banned.is_empty()); + } + + #[test] + fn test_scan_set_routes_each_extension_to_its_buckets() { + // One file can serve several buckets. `py` is an SPDX-header, + // secret-scan *and* banned extension; `rs` is SPDX + secret; + // `txt` is in no filtered set, so it reaches `all` alone. This is + // the sharing that makes one traversal cheaper than three. + let mut set = ScanSet::default(); + set.offer(Path::new("/repo/main.rs"), "rs"); + set.offer(Path::new("/repo/app.py"), "py"); + set.offer(Path::new("/repo/data.txt"), "txt"); + let rs = PathBuf::from("/repo/main.rs"); + let py = PathBuf::from("/repo/app.py"); + assert_eq!(set.all.len(), 3); + assert_eq!(set.spdx, vec![rs.clone(), py.clone()]); + assert_eq!(set.secret, vec![rs, py.clone()]); + assert_eq!(set.banned, vec![py]); + } + #[test] fn test_compliance_level_equality() { assert_eq!(ComplianceLevel::Bronze, ComplianceLevel::Bronze); diff --git a/aletheia/src/config.rs b/aletheia/src/config.rs index 5f195c8..923bdc4 100644 --- a/aletheia/src/config.rs +++ b/aletheia/src/config.rs @@ -85,13 +85,197 @@ pub struct IgnoreConfig { impl IgnoreConfig { /// Whether a repo-relative path is ignored by any pattern. - pub fn is_ignored(&self, rel_path: &str) -> bool { + pub(crate) fn is_ignored(&self, rel_path: &str) -> bool { self.patterns .iter() .any(|pat| crate::checks::glob_match(pat, rel_path)) } } +/// GITIGNORE SUPPORT: the repository's own `.gitignore` rules, honoured by +/// the scanner so that build output (`target/`, `obj/`, `_build/`, …) does +/// not pollute the audit. +/// +/// Deliberately separate from [`IgnoreConfig`]: `[ignore]` patterns come from +/// aletheia's own configuration and are a *choice*, whereas `.gitignore` is +/// the repository's own declaration of what is not part of the published +/// artefact. Auditing a tree that has just been built should produce the same +/// verdict as auditing a clean checkout. +/// +/// Implemented (a documented subset of git's behaviour): +/// * `#` comments and blank lines are skipped; +/// * `!pattern` re-includes, and the *last* matching rule wins; +/// * a trailing `/` restricts the rule to directories and their contents; +/// * a pattern containing `/` is anchored to the directory holding the +/// `.gitignore`; otherwise it matches at any depth below that directory; +/// * `*` crosses directory boundaries, matching this crate's `glob_match`. +/// +/// Not implemented, and not claimed: character classes (`[a-z]`), backslash +/// escapes, and re-inclusion of a file *inside* an ignored directory (git +/// itself forbids the last one). +#[derive(Debug, Clone, Default)] +pub struct GitIgnore { + rules: Vec, +} + +#[derive(Debug, Clone)] +struct GitIgnoreRule { + pattern: String, + negated: bool, + /// Rule carried a trailing `/`: matches directories, so it also covers + /// everything beneath them. + dir_only: bool, + /// Rule contained a `/`, making it relative to `base` rather than + /// matching at any depth. + anchored: bool, + /// Repo-relative directory holding the `.gitignore` that declared the + /// rule ("" for the repository root). + base: String, +} + +impl GitIgnore { + /// Add the rules from one `.gitignore` file. + /// + /// `base` is the repo-relative directory containing it. Rules are stored + /// in load order, and [`GitIgnore::is_ignored`] resolves conflicts by + /// last-match-wins, so a nested file overrides the root one. + pub(crate) fn push_file(&mut self, base: &str, contents: &str) { + for raw in contents.lines() { + // Trailing whitespace is not significant in git; leading whitespace + // is (it is part of the pattern), so only trim the end. + let line = raw.trim_end(); + if line.is_empty() || line.starts_with('#') { + continue; + } + let (negated, body) = match line.strip_prefix('!') { + Some(rest) => (true, rest), + None => (false, line), + }; + let body = body.trim_end(); + if body.is_empty() { + continue; + } + let (dir_only, body) = match body.strip_suffix('/') { + Some(rest) => (true, rest), + None => (false, body), + }; + if body.is_empty() { + continue; + } + // A leading `/` anchors without appearing in the pattern; a `/` + // anywhere else does the same thing by virtue of being present. + let stripped = body.strip_prefix('/').unwrap_or(body); + let anchored = body.starts_with('/') || stripped.contains('/'); + self.rules.push(GitIgnoreRule { + pattern: stripped.to_string(), + negated, + dir_only, + anchored, + base: base.to_string(), + }); + } + } + + /// Whether a repo-relative *file* path is ignored. Last matching rule + /// wins, so a later `!rule` can re-include something an earlier rule + /// excluded. + pub fn is_ignored(&self, rel_path: &str) -> bool { + self.decide(rel_path, false) + } + + /// Whether a repo-relative *directory* path is ignored. + /// + /// Separate from [`GitIgnore::is_ignored`] because a directory-only rule + /// (`obj/`) matches a directory named `obj` but not a file of that name, + /// and a path string alone cannot tell the two apart. The scanner knows + /// the entry's file type, so it can ask the precise question. + pub(crate) fn is_ignored_dir(&self, rel_path: &str) -> bool { + self.decide(rel_path, true) + } + + fn decide(&self, rel_path: &str, is_dir: bool) -> bool { + if rel_path.is_empty() { + return false; + } + let mut verdict = false; + let mut matched = false; + for rule in &self.rules { + if rule.matches(rel_path, is_dir) { + verdict = !rule.negated; + matched = true; + } + } + matched && verdict + } + + /// Drop rules back to an earlier [`GitIgnore::len`]. The scanner uses this + /// to pop a directory's rules when the walk leaves that directory, so a + /// nested `.gitignore` cannot leak into sibling subtrees. + pub(crate) fn truncate(&mut self, len: usize) { + self.rules.truncate(len); + } + + /// Number of rules loaded. Used by tests and diagnostics. + pub(crate) fn len(&self) -> usize { + self.rules.len() + } +} + +impl GitIgnoreRule { + fn matches(&self, path: &str, is_dir: bool) -> bool { + // A rule only governs paths at or below the directory that declared it. + let sub = match self.base.as_str() { + "" => path, + base => match path.strip_prefix(base) { + Some(rest) => match rest.strip_prefix('/') { + Some(rest) => rest, + None => return false, + }, + None => return false, + }, + }; + if sub.is_empty() { + return false; + } + if self.anchored { + return self.test(sub, is_dir); + } + // Unanchored: try at every depth below `base`, i.e. at every component + // boundary of the remaining path. + let mut candidate = sub; + loop { + if self.test(candidate, is_dir) { + return true; + } + match candidate.find('/') { + Some(i) => candidate = &candidate[i + 1..], + None => return false, + } + } + } + + /// Match one candidate path. + /// + /// A pattern that matches a *directory* excludes everything beneath it, so + /// every ancestor directory is a match candidate too — that is how `obj/` + /// comes to ignore `obj/x.o`. A directory-only rule may only match a real + /// directory: a proper ancestor always is one, but the path itself counts + /// only when the caller says so. + fn test(&self, candidate: &str, is_dir: bool) -> bool { + if (is_dir || !self.dir_only) && crate::checks::glob_match(&self.pattern, candidate) { + return true; + } + let mut node = candidate; + while let Some(i) = node.rfind('/') { + node = &node[..i]; + if crate::checks::glob_match(&self.pattern, node) { + return true; + } + } + false + } +} + /// COMPLIANCE CONFIG: toggles for specific verification checks. /// /// The five named fields are the historical category toggles; `extra` @@ -345,6 +529,120 @@ fn strip_comment(line: &str) -> &str { mod tests { use super::*; + // --- .gitignore support ------------------------------------------------- + // The scanner honours the repository's own `.gitignore`, so auditing a + // freshly built tree gives the same verdict as auditing a clean checkout. + + /// Build a rule set from one root-level `.gitignore`. + fn gi(contents: &str) -> GitIgnore { + let mut ig = GitIgnore::default(); + ig.push_file("", contents); + ig + } + + #[test] + fn gitignore_matches_build_output_directories() { + let ig = gi("target/\nobj/\ndist-newstyle/\n"); + // Files beneath an ignored directory are ignored. + assert!(ig.is_ignored("target/debug/app")); + assert!(ig.is_ignored("crate/obj/b__main.ads"), "nested obj/"); + assert!(ig.is_ignored("dist-newstyle/build/x/y")); + // And the directory itself is ignored — asked as a directory, because + // `target/` does not match a *file* called `target`. + assert!(ig.is_ignored_dir("target")); + assert!(ig.is_ignored_dir("crate/obj")); + // Nothing else is touched. + assert!(!ig.is_ignored("src/main.adb")); + assert!(!ig.is_ignored_dir("src")); + } + + #[test] + fn gitignore_plain_pattern_that_matches_a_directory_covers_its_subtree() { + // git ignores everything under a directory any rule matches, even + // without a trailing slash. + let ig = gi("/build\n"); + assert!(ig.is_ignored_dir("build")); + assert!(ig.is_ignored("build/x.coma")); + assert!(!ig.is_ignored("src/build/x.coma"), "anchored to the root"); + } + + #[test] + fn gitignore_dir_only_rule_does_not_match_a_file_of_that_name() { + // `obj/` ignores the directory; a *file* called `obj` is untouched. + let ig = gi("obj/\n"); + assert!(ig.is_ignored("obj/x.o")); + assert!(!ig.is_ignored("obj")); + } + + #[test] + fn gitignore_skips_comments_and_blank_lines() { + let ig = gi("# a comment\n\n \n/build/\n"); + assert_eq!(ig.len(), 1); + assert!(ig.is_ignored("build/x")); + } + + #[test] + fn gitignore_leading_slash_anchors_to_the_root() { + let ig = gi("/build\n"); + assert!(ig.is_ignored("build/x")); + assert!(!ig.is_ignored("src/build/x"), "anchored, so not at depth"); + } + + #[test] + fn gitignore_unanchored_pattern_matches_at_any_depth() { + let ig = gi("*.coma\n"); + assert!(ig.is_ignored("a.coma")); + assert!(ig.is_ignored("deep/nested/b.coma")); + assert!(!ig.is_ignored("a.rs")); + } + + #[test] + fn gitignore_wildcard_crosses_directories() { + let ig = gi("verification/verif/\n"); + assert!(ig.is_ignored("verification/verif/x/y.coma")); + } + + #[test] + fn gitignore_negation_reincludes_and_last_rule_wins() { + let ig = gi("*.log\n!keep.log\n"); + assert!(ig.is_ignored("debug.log")); + assert!(!ig.is_ignored("keep.log"), "negated by the later rule"); + + // Order matters: a later ignore beats an earlier negation. + let ig2 = gi("!keep.log\n*.log\n"); + assert!(ig2.is_ignored("keep.log")); + } + + #[test] + fn gitignore_nested_file_is_scoped_to_its_own_subtree() { + let mut ig = GitIgnore::default(); + ig.push_file("", ""); + ig.push_file("vendor", "*.md\n"); + assert!(ig.is_ignored("vendor/README.md")); + assert!( + !ig.is_ignored("docs/README.md"), + "nested rule must not escape" + ); + assert!( + !ig.is_ignored("vendor"), + "the directory itself is not matched" + ); + } + + #[test] + fn gitignore_empty_and_root_paths_are_never_ignored() { + let ig = gi("*\n"); + assert!(!ig.is_ignored(""), "the repo root is not a file"); + assert!(ig.is_ignored("anything.txt")); + } + + #[test] + fn gitignore_with_only_comments_ignores_nothing() { + let ig = gi("# nothing here\n\n"); + assert_eq!(ig.len(), 0); + assert!(!ig.is_ignored("target/x")); + } + #[test] fn test_config_default() { let config = Config::default(); diff --git a/aletheia/templates/ada/.editorconfig b/aletheia/templates/ada/.editorconfig new file mode 100644 index 0000000..8718995 --- /dev/null +++ b/aletheia/templates/ada/.editorconfig @@ -0,0 +1,19 @@ +# @@PROJECT_NAME@@ - Editor Configuration +# https://editorconfig.org + +root = true + +[*] +charset = utf-8 +end_of_line = lf +indent_size = 3 +indent_style = space +insert_final_newline = true +trim_trailing_whitespace = true + +[*.adoc] +trim_trailing_whitespace = false + +[Justfile] +indent_style = space +indent_size = 4 diff --git a/aletheia/templates/ada/.github/workflows/ci.yml b/aletheia/templates/ada/.github/workflows/ci.yml new file mode 100644 index 0000000..1cca4ca --- /dev/null +++ b/aletheia/templates/ada/.github/workflows/ci.yml @@ -0,0 +1,40 @@ +# SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. +name: CI + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +jobs: + check: + name: Build, test, lint (offline) + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Install GNAT and gprbuild + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends gnat gprbuild + + - name: Build + run: gprbuild -p -P @@MOD_NAME@@.gpr + + - name: Test + run: | + gprbuild -p -P tests/tests.gpr + ./obj-tests/run_tests diff --git a/aletheia/templates/ada/.github/workflows/proof.yml b/aletheia/templates/ada/.github/workflows/proof.yml new file mode 100644 index 0000000..eb09412 --- /dev/null +++ b/aletheia/templates/ada/.github/workflows/proof.yml @@ -0,0 +1,92 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPARK proof gate. Separate from ci.yml on purpose: the offline Bronze job +# must stay fast and dependency-free, while proving needs gnatprove. +# +# This workflow is a real gate — `gnatprove` runs with --checks-as-errors (set +# in the project's Prove package), so an unproved check fails the job instead +# of exiting 0. It is deliberately *not* part of `just check`. +name: Proof (SPARK) + +on: + push: + branches: [main, master] + paths: + - 'src/**' + - 'tests/**' + - '*.gpr' + - 'Justfile' + - '.github/workflows/proof.yml' + pull_request: + branches: [main, master] + paths: + - 'src/**' + - 'tests/**' + - '*.gpr' + - 'Justfile' + - '.github/workflows/proof.yml' + workflow_dispatch: + +concurrency: + group: proof-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +jobs: + spark: + name: Prove SPARK units (gnatprove) + runs-on: ubuntu-24.04 + timeout-minutes: 30 + steps: + # Pinned to a full SHA rather than relying on actions.lock: only two of + # the six templates ship this opt-in workflow, and a lock entry for a + # file the other four do not have would be noise in a shared file. + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + + # gnatprove is a frontend, not a toolchain: the archive below contains + # one binary, no compiler and no gprbuild. It needs GNAT and gprbuild to + # be present, exactly as ci.yml installs them - without this step the job + # dies at `gprbuild --version` in the next step. + - name: Install GNAT and gprbuild + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends gnat gprbuild + + # gnatprove ships its own Why3 and versions of Alt-Ergo/CVC5, so there is + # no solver version to drift. Pinned by URL and checksum: this artefact is + # a release asset, not a mutable tag. + - name: Install gnatprove 13.2.0 + run: | + set -euo pipefail + url="https://github.com/alire-project/GNAT-FSF-builds/releases/download/gnatprove-13.2.0-1/gnatprove-x86_64-linux-13.2.0-1.tar.gz" + curl -fsSL -o /tmp/gnatprove.tar.gz "$url" + echo "28fc3583d2364c1e10790fe258c408faffa42d7ff77bb81dc18d4907608f4017 /tmp/gnatprove.tar.gz" | sha256sum -c - + sudo mkdir -p /opt/gnatprove + sudo tar xzf /tmp/gnatprove.tar.gz -C /opt/gnatprove --strip-components=1 + echo "/opt/gnatprove/bin" >> "$GITHUB_PATH" + + - name: Show toolchain + run: | + gnatprove --version + gprbuild --version | head -1 + + # The GPR's Prove package carries --level=2 and --checks-as-errors, so + # this fails on any unproved check. `just proof` runs gnatprove on the + # same project; the explicit gprbuild first builds the object directory + # the prover reads. + - name: Prove + run: | + gprbuild -p -P @@MOD_NAME@@.gpr + gnatprove -P @@MOD_NAME@@.gpr + + - name: Proof summary + if: always() + run: | + if [ -f obj/gnatprove/gnatprove.out ]; then + tail -25 obj/gnatprove/gnatprove.out + else + echo "no proof summary produced" + fi diff --git a/aletheia/templates/ada/.gitignore b/aletheia/templates/ada/.gitignore new file mode 100644 index 0000000..48b1f25 --- /dev/null +++ b/aletheia/templates/ada/.gitignore @@ -0,0 +1,24 @@ +# SPDX-License-Identifier: MPL-2.0 +# Build artefacts +/obj/ +/obj-tests/ +*.ali +*.o +*.bexch + +# gnatprove / SPARK proof artefacts +*.siv +*.mlw +*.spark +obj/gnatprove/ + +# Editors and OS +.DS_Store +.idea/ +.vscode/ +*.swp +*~ + +# Local environment +.env +.env.local diff --git a/aletheia/templates/ada/.machine_readable/rsr-profile.a2ml b/aletheia/templates/ada/.machine_readable/rsr-profile.a2ml new file mode 100644 index 0000000..111f25f --- /dev/null +++ b/aletheia/templates/ada/.machine_readable/rsr-profile.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# RSR capability profile for @@PROJECT_NAME@@. Declares what this repo +# carries so the capability gates compute the applicable criterion set. +[profile] +capabilities = ["ada", "cli", "docs"] + +[rationale] +ada = "true: GPR project, GNAT 14.2 / gprbuild" +cli = "true: src/main.adb produces an executable" +docs = "true: README + SECURITY + CONTRIBUTING + CODE_OF_CONDUCT + CHANGELOG" +no-library = "shared: the library units are part of the same GPR project" +no-container = "true: no Containerfile in the scaffold" diff --git a/aletheia/templates/ada/.tool-versions b/aletheia/templates/ada/.tool-versions new file mode 100644 index 0000000..dbf45d2 --- /dev/null +++ b/aletheia/templates/ada/.tool-versions @@ -0,0 +1,3 @@ +# Toolchain pins, asdf/mise compatible. +gnat 14.2.0 +gprbuild 2025.0.0 diff --git a/aletheia/templates/ada/@@MOD_NAME@@.gpr b/aletheia/templates/ada/@@MOD_NAME@@.gpr new file mode 100644 index 0000000..e6e837c --- /dev/null +++ b/aletheia/templates/ada/@@MOD_NAME@@.gpr @@ -0,0 +1,37 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- GPR project for @@PROJECT_NAME@@. +-- +-- Plain GPR rather than Alire: no crate index, nothing to fetch, so the +-- build works with no network at all. +-- +-- The switches are the static-analysis gate for this language: +-- -gnatwa all warnings on +-- -gnatwe warnings are errors (a warning fails the build) +-- -gnata assertions and preconditions checked at run time +project @@MOD_ADA@@ is + for Source_Dirs use ("src"); + for Object_Dir use "obj"; + for Exec_Dir use "obj"; + for Main use ("main.adb"); + + -- -gnat2022 Big_Integers (used by the contracts) is an Ada 2022 unit + package Compiler is + for Default_Switches ("Ada") use ("-gnat2022", "-gnatwa", "-gnatwe", "-gnata"); + end Compiler; + + package Builder is + -- Name the artefact after the project, not after main.adb. + for Executable ("main.adb") use "@@PROJECT_NAME@@"; + end Builder; + + -- Default proof settings, so a bare `gnatprove -P @@MOD_NAME@@.gpr` + -- already means "prove everything, and treat unproved checks as + -- failure". `just proof` relies on this. + package Prove is + -- --level=2 prove absence of run-time errors as well + -- --checks-as-errors without this gnatprove still exits 0 when a + -- check is unproved, which would make the gate + -- decorative. It is what makes `just proof` fail. + for Proof_Switches ("Ada") use ("--level=2", "--checks-as-errors"); + end Prove; +end @@MOD_ADA@@; diff --git a/aletheia/templates/ada/Justfile b/aletheia/templates/ada/Justfile new file mode 100644 index 0000000..c534c2f --- /dev/null +++ b/aletheia/templates/ada/Justfile @@ -0,0 +1,50 @@ +# SPDX-License-Identifier: MPL-2.0 +# Justfile — build automation for @@PROJECT_NAME@@. +# See: https://github.com/casey/just +# +# Every recipe here is offline: this project has no external dependencies, +# so nothing is fetched at build time. Recipes fail loudly — a recipe that +# echoes a message and exits 0 would be a fake gate (RSR v2 6.1.5, Gold). + +default: + @just --list + +# Build the executable into obj/ +build: + gprbuild -p -P @@MOD_NAME@@.gpr + +# Run the program; pass arguments after the recipe name +run *ARGS: + ./obj/@@PROJECT_NAME@@ {{ARGS}} + +# Build and run the test executable +test: + gprbuild -p -P tests/tests.gpr + ./obj-tests/run_tests + +# The static-analysis gate for this language. The switches live in the GPR +# files (`-gnatwa -gnatwe`: all warnings on, warnings as errors), so a +# warning fails the build rather than scrolling past. +lint: + gprbuild -p -P @@MOD_NAME@@.gpr + gprbuild -p -P tests/tests.gpr + +# --- SPARK deductive verification (opt-in) ---------------------------- +# Needs gnatprove. The default build never requires it — `gnatprove` only +# reads the sources and the GPR's Prove package (--level=2), so `just +# check` stays a plain GNAT build. See README.adoc. + +# Statically prove every SPARK unit. Exits non-zero on any unproved check. +proof: + gnatprove -P @@MOD_NAME@@.gpr + +# Remove gnatprove artefacts (obj/gnatprove, *.siv/*.mlw) +proof-clean: + gnatprove -P @@MOD_NAME@@.gpr --clean + +# Verify RSR compliance using the estate checker +verify: + aletheia . + +# Everything the CI gate runs, in the same order +check: build test lint diff --git a/aletheia/templates/ada/README.adoc b/aletheia/templates/ada/README.adoc new file mode 100644 index 0000000..d3d40cb --- /dev/null +++ b/aletheia/templates/ada/README.adoc @@ -0,0 +1,118 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += @@PROJECT_NAME@@ +:toc: +:icons: font + +____ +@@PROJECT_DESCRIPTION@@ +____ + +== Quick Start + +[source,bash] +---- +# Build (offline — nothing is downloaded) +just build + +# Test +just test + +# Verify RSR compliance +just verify +---- + +This project is *standalone by construction*: the scaffold fetches nothing, +the build has no external dependencies, and the licence texts ship in-tree +under `+LICENSES/+`. + +== RSR Compliance + +[cols="1,3"] +|=== +|Bronze |Documentation, security policy, SPDX headers, CI, licence classification +|Silver |`.editorconfig`, `.tool-versions`, machine-readable manifests, SHA-pinned CI, `+LICENSES/+` +|Gold |No silent-skip recipes +|=== + +Verify with the estate's own checker: + +[source,bash] +---- +aletheia . +---- + +== Language: @@LANG_DISPLAY@@ + +@@LANG_POLICY@@ + +== Verification: SPARK + +The core package (`+src/@@MOD_NAME@@.ads+`, `+src/@@MOD_NAME@@.adb+`) is in the +SPARK subset — it declares `+pragma SPARK_Mode (On);+` — and its contracts are +*statically proved*, not merely checked at run time: + +[source,ada] +---- +function Clamp (Value, Lo, Hi : U32) return U32 + with Pre => Lo <= Hi, + Post => Clamp'Result in Lo .. Hi; + +function Midpoint (A, B : U32) return U32 + with Pre => A <= B, + Post => Midpoint'Result in A .. B + and then BI (Midpoint'Result) = (BI (A) + BI (B)) / 2; +---- + +`+just proof+` runs `gnatprove` at proof level 2 (contracts *and* absence of +run-time errors) and passes `--checks-as-errors`, so an unproved check fails +the recipe. Without that switch `gnatprove` still exits `0` on an unproved +check, which would make the gate decorative. + +[source,bash] +---- +just proof # prove every SPARK unit; non-zero exit on anything unproved +just proof-clean # remove gnatprove artefacts +---- + +The command-line entry point (`+src/main.adb+`) is deliberately +`+pragma SPARK_Mode (Off);+`: `Ada.Text_IO`, exceptions and `'Value`/`'Image` +are outside the SPARK subset. gnatprove skips it rather than pretending to +verify it. The logic it calls is the part that is proved. + +== Documentation +== Documentation + +* link:SECURITY.adoc[Security Policy] — vulnerability disclosure +* link:CONTRIBUTING.adoc[Contributing Guide] — how to contribute +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] — community standards +* link:MAINTAINERS.adoc[Maintainers] — ownership and decisions +* link:CHANGELOG.adoc[Changelog] — version history + +== Layout + +.... +. +├── Justfile # build automation (capital J — v2 shape) +├── LICENSE # licence statement +├── LICENSES/ # full licence texts (REUSE style) +├── src/ # source (layout follows the language's conventions) +├── .github/workflows/ # CI + estate gates +├── .machine_readable/ # machine-readable metadata +└── .well-known/ # security.txt, ai.txt, humans.txt +.... + +== Contributing + +See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc]. + +== License + +Code is licensed under the Mozilla Public License, version 2.0 +(`+MPL-2.0+`). Documentation is licensed under Creative Commons +Attribution-ShareAlike 4.0 International (`+CC-BY-SA-4.0+`). + +See link:LICENSE[LICENSE] and the `+LICENSES/+` directory for full texts. + +''''' + +_Created from the aletheia v2 Bronze template._ diff --git a/aletheia/templates/ada/src/@@MOD_NAME@@.adb b/aletheia/templates/ada/src/@@MOD_NAME@@.adb new file mode 100644 index 0000000..f01d409 --- /dev/null +++ b/aletheia/templates/ada/src/@@MOD_NAME@@.adb @@ -0,0 +1,31 @@ +-- SPDX-License-Identifier: MPL-2.0 +pragma SPARK_Mode (On); + +package body @@MOD_ADA@@ is + + function Clamp (Value, Lo, Hi : U32) return U32 is + Result : U32 := Value; + begin + if Result < Lo then + Result := Lo; + end if; + if Result > Hi then + Result := Hi; + end if; + return Result; + end Clamp; + + function Midpoint (A, B : U32) return U32 is + D : constant U32 := B - A; + begin + -- Stepping stones for the provers: modular subtraction and division + -- agree with their exact-integer counterparts on this domain, and + -- the final addition cannot wrap because the result is at most B. + pragma Assert (BI (D) = BI (B) - BI (A)); + pragma Assert (BI (D / 2) = BI (D) / 2); + pragma Assert (BI (A + D / 2) = BI (A) + BI (D) / 2); + pragma Assert (BI (A) + (BI (B) - BI (A)) / 2 = (BI (A) + BI (B)) / 2); + return A + D / 2; + end Midpoint; + +end @@MOD_ADA@@; diff --git a/aletheia/templates/ada/src/@@MOD_NAME@@.ads b/aletheia/templates/ada/src/@@MOD_NAME@@.ads new file mode 100644 index 0000000..03c577d --- /dev/null +++ b/aletheia/templates/ada/src/@@MOD_NAME@@.ads @@ -0,0 +1,50 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Core library for @@PROJECT_NAME@@. +-- +-- This package is in the SPARK subset: `SPARK_Mode (On)` below means +-- `gnatprove` analyses it, and every contract here is *statically proved*, +-- not merely checked at run time. See README.adoc for the proof recipe. +-- +-- Replace these sample subprograms with your own. Adding a subprogram here +-- adds it to gnatprove's remit automatically. + +pragma SPARK_Mode (On); + +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + +package @@MOD_ADA@@ is + + -- Unsigned 32-bit. Modular arithmetic wraps rather than raising, which + -- makes the shift/divide forms below total. + type U32 is mod 2 ** 32; + + -- Exact-integer view of U32. Contracts must reason about the + -- *mathematical* half-sum; U32 arithmetic would wrap. This is the + -- SPARK idiom for that, and the generated functions are ghost. + package U32_Big is new Unsigned_Conversions (U32); + + -- Shorthand so the contracts below read like specifications. + function BI (X : U32) return Big_Integer is (U32_Big.To_Big_Integer (X)) + with Ghost; + + -- Clamp Value into the inclusive range Lo .. Hi. + -- + -- Proved: given Lo <= Hi, the result is always inside Lo .. Hi. + function Clamp (Value, Lo, Hi : U32) return U32 + with Pre => Lo <= Hi, + Post => Clamp'Result in Lo .. Hi; + + -- Overflow-free midpoint of A and B, rounded towards zero. + -- + -- The naive (A + B) / 2 wraps for large inputs; this form cannot, + -- because it never materialises the sum. + -- + -- Proved: given A <= B, the result lies in A .. B and equals the exact + -- half-sum (A + B) / 2 as a mathematical integer. + function Midpoint (A, B : U32) return U32 + with Pre => A <= B, + Post => Midpoint'Result in A .. B + and then BI (Midpoint'Result) = (BI (A) + BI (B)) / 2; + +end @@MOD_ADA@@; diff --git a/aletheia/templates/ada/src/main.adb b/aletheia/templates/ada/src/main.adb new file mode 100644 index 0000000..b639a37 --- /dev/null +++ b/aletheia/templates/ada/src/main.adb @@ -0,0 +1,82 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- @@PROJECT_NAME@@ — command-line entry point. +-- +-- SPARK_Mode is Off here on purpose: this unit is the I/O boundary, and +-- Ada.Text_IO, exceptions and 'Value/'Image are all outside the SPARK +-- subset. The logic it calls lives in @@MOD_NAME@@.ads, which is SPARK and +-- fully proved. gnatprove skips this file rather than pretending to verify +-- it — see README.adoc. +pragma SPARK_Mode (Off); + +with Ada.Command_Line; +with Ada.Text_IO; +with @@MOD_ADA@@; + +procedure Main is + use Ada.Command_Line; + use Ada.Text_IO; + use @@MOD_ADA@@; + + Usage : constant String := + "@@PROJECT_NAME@@ @@VERSION@@" & ASCII.LF & + "" & ASCII.LF & + "usage:" & ASCII.LF & + " @@PROJECT_NAME@@ clamp clamp a value into a range" & ASCII.LF & + " @@PROJECT_NAME@@ mid midpoint, rounded down (a <= b)" & ASCII.LF & + " @@PROJECT_NAME@@ --help show this message" & ASCII.LF & + "" & ASCII.LF & + "All arguments are unsigned 32-bit integers."; + + procedure Unrecognised is + begin + Put_Line (Standard_Error, "error: unrecognised arguments"); + New_Line (Standard_Error); + Put_Line (Standard_Error, Usage); + Set_Exit_Status (Failure); + end Unrecognised; + +begin + if Argument_Count = 0 or else Argument (1) = "--help" or else Argument (1) = "-h" then + Put_Line (Usage); + return; + end if; + + if Argument_Count = 4 and then Argument (1) = "clamp" then + declare + Value : constant U32 := U32'Value (Argument (2)); + Lo : constant U32 := U32'Value (Argument (3)); + Hi : constant U32 := U32'Value (Argument (4)); + begin + if Lo > Hi then + Unrecognised; + return; + end if; + Put_Line (U32'Image (Clamp (Value, Lo, Hi))); + return; + exception + when Constraint_Error => + Unrecognised; + return; + end; + end if; + + if Argument_Count = 3 and then Argument (1) = "mid" then + declare + A : constant U32 := U32'Value (Argument (2)); + B : constant U32 := U32'Value (Argument (3)); + begin + if A > B then + Unrecognised; + return; + end if; + Put_Line (U32'Image (Midpoint (A, B))); + return; + exception + when Constraint_Error => + Unrecognised; + return; + end; + end if; + + Unrecognised; +end Main; diff --git a/aletheia/templates/ada/tests/run_tests.adb b/aletheia/templates/ada/tests/run_tests.adb new file mode 100644 index 0000000..da1913a --- /dev/null +++ b/aletheia/templates/ada/tests/run_tests.adb @@ -0,0 +1,64 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Test runner for @@PROJECT_NAME@@. +-- +-- Dependency-free by design: no AUnit, just a counter and a non-zero exit +-- status on failure, so the suite needs nothing beyond the GNAT runtime. +-- +-- These are *runtime* tests. They complement, and do not replace, the +-- static proof in @@MOD_NAME@@.ads — see README.adoc. +with Ada.Command_Line; +with Ada.Text_IO; +with @@MOD_ADA@@; + +procedure Run_Tests is + use Ada.Text_IO; + use @@MOD_ADA@@; + + Failures : Natural := 0; + + procedure Check (Label : String; Condition : Boolean) is + begin + if not Condition then + Put_Line ("FAIL: " & Label); + Failures := Failures + 1; + end if; + end Check; + +begin + -- Clamp: below, inside and above the range + Check ("clamp keeps an in-range value", Clamp (5, 0, 10) = 5); + Check ("clamp lifts a low value", Clamp (0, 1, 10) = 1); + Check ("clamp drops a high value", Clamp (99, 0, 10) = 10); + Check ("clamp handles a degenerate range", Clamp (7, 7, 7) = 7); + + -- Clamp: idempotent, and always inside the range + for Value in U32 range 0 .. 128 loop + declare + Once : constant U32 := Clamp (Value, 10, 100); + begin + Check ("clamp is idempotent", Clamp (Once, 10, 100) = Once); + Check ("clamp result is in range", Once >= 10 and then Once <= 100); + end; + end loop; + + -- Midpoint: agrees with the naive form wherever that form is safe + for A in U32 range 0 .. 63 loop + for B in U32 range A .. 63 loop + Check ("midpoint matches naive", Midpoint (A, B) = (A + B) / 2); + end loop; + end loop; + + -- Midpoint: stays inside the inputs, and cannot overflow + Check ("midpoint bounded (0, max)", Midpoint (0, U32'Last) = U32'Last / 2); + Check ("midpoint bounded (max, max)", Midpoint (U32'Last, U32'Last) = U32'Last); + Check ("midpoint (8, 11)", Midpoint (8, 11) = 9); + Check ("midpoint (7, 9)", Midpoint (7, 9) = 8); + Check ("midpoint (0, 0)", Midpoint (0, 0) = 0); + + if Failures = 0 then + Put_Line ("All tests passed."); + else + Put_Line (Natural'Image (Failures) & " test(s) failed."); + Ada.Command_Line.Set_Exit_Status (Ada.Command_Line.Failure); + end if; +end Run_Tests; diff --git a/aletheia/templates/ada/tests/tests.gpr b/aletheia/templates/ada/tests/tests.gpr new file mode 100644 index 0000000..2c2fcc9 --- /dev/null +++ b/aletheia/templates/ada/tests/tests.gpr @@ -0,0 +1,13 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Test project for @@PROJECT_NAME@@. Compiles the library sources +-- alongside the test runner, so the tests exercise the real units. +project Tests is + for Source_Dirs use ("../src", "."); + for Object_Dir use "../obj-tests"; + for Exec_Dir use "../obj-tests"; + for Main use ("run_tests.adb"); + + package Compiler is + for Default_Switches ("Ada") use ("-gnat2022", "-gnatwa", "-gnatwe", "-gnata"); + end Compiler; +end Tests; diff --git a/aletheia/templates/agda/.editorconfig b/aletheia/templates/agda/.editorconfig new file mode 100644 index 0000000..7520e0f --- /dev/null +++ b/aletheia/templates/agda/.editorconfig @@ -0,0 +1,19 @@ +# @@PROJECT_NAME@@ - Editor Configuration +# https://editorconfig.org + +root = true + +[*] +charset = utf-8 +end_of_line = lf +indent_size = 2 +indent_style = space +insert_final_newline = true +trim_trailing_whitespace = true + +[*.adoc] +trim_trailing_whitespace = false + +[Justfile] +indent_style = space +indent_size = 4 diff --git a/aletheia/templates/agda/.github/workflows/ci.yml b/aletheia/templates/agda/.github/workflows/ci.yml new file mode 100644 index 0000000..134fb0a --- /dev/null +++ b/aletheia/templates/agda/.github/workflows/ci.yml @@ -0,0 +1,41 @@ +# SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. +name: CI + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +jobs: + check: + name: Build, test, lint (offline) + runs-on: ubuntu-latest + timeout-minutes: 20 + env: + # Agda source is Unicode; pin the locale so the gate is deterministic. + LC_ALL: C.UTF-8 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Install Agda + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends agda + + - name: Typecheck (this is the build) + run: agda src/@@MOD_CAMEL@@.agda + + - name: Typecheck the proofs + run: agda src/Properties.agda diff --git a/aletheia/templates/agda/.gitignore b/aletheia/templates/agda/.gitignore new file mode 100644 index 0000000..88e6819 --- /dev/null +++ b/aletheia/templates/agda/.gitignore @@ -0,0 +1,4 @@ +# SPDX-License-Identifier: MPL-2.0 +/_build/ +/MAlonzo/ +*.agdai diff --git a/aletheia/templates/agda/.machine_readable/rsr-profile.a2ml b/aletheia/templates/agda/.machine_readable/rsr-profile.a2ml new file mode 100644 index 0000000..a08296f --- /dev/null +++ b/aletheia/templates/agda/.machine_readable/rsr-profile.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# RSR capability profile for @@PROJECT_NAME@@. Declares what this repo +# carries so the capability gates compute the applicable criterion set. +[profile] +capabilities = ["agda", "proofs", "docs"] + +[rationale] +agda = "true: .agda-lib project, Agda 2.6.4.3" +proofs = "true: src/ contains machine-checked proofs, not tests" +docs = "true: README + SECURITY + CONTRIBUTING + CODE_OF_CONDUCT + CHANGELOG" +no-library = "shared: modules are proof library, not published as a package" +no-container = "true: no Containerfile in the scaffold" diff --git a/aletheia/templates/agda/.tool-versions b/aletheia/templates/agda/.tool-versions new file mode 100644 index 0000000..f509ae3 --- /dev/null +++ b/aletheia/templates/agda/.tool-versions @@ -0,0 +1,2 @@ +# Toolchain pins, asdf/mise compatible. +agda 2.6.4.3 diff --git a/aletheia/templates/agda/@@PROJECT_NAME@@.agda-lib b/aletheia/templates/agda/@@PROJECT_NAME@@.agda-lib new file mode 100644 index 0000000..d947beb --- /dev/null +++ b/aletheia/templates/agda/@@PROJECT_NAME@@.agda-lib @@ -0,0 +1,2 @@ +name: @@PROJECT_NAME@@ +include: src diff --git a/aletheia/templates/agda/Justfile b/aletheia/templates/agda/Justfile new file mode 100644 index 0000000..6a5b299 --- /dev/null +++ b/aletheia/templates/agda/Justfile @@ -0,0 +1,36 @@ +# SPDX-License-Identifier: MPL-2.0 +# Justfile — build automation for @@PROJECT_NAME@@. +# See: https://github.com/casey/just +# +# Every recipe here is offline: this project has no external dependencies, +# so nothing is fetched at build time. Recipes fail loudly — a recipe that +# echoes a message and exits 0 would be a fake gate (RSR v2 6.1.5, Gold). + +# Agda source is written in Unicode (≡, ∀, ×, ˡ). Without a UTF-8 locale +# the checker cannot read its own files and fails with a locale error +# rather than a type error, so pin it here rather than leave it to the +# ambient environment. +export LC_ALL := "C.UTF-8" + +default: + @just --list + +# Typecheck the main module. In Agda, typechecking IS the build. +build: + agda src/@@MOD_CAMEL@@.agda + +# NOTE: there is no `run` recipe. This is a proof library, not a program: +# there is no executable to run, and inventing one would be a fake gate. +# Add a `main : IO ⊤` module and a compile recipe if you need one. + +# Typecheck the proof suite. There is no separate test runner: a proof +# that does not typecheck fails, which is the strongest form of "test". +test: + agda src/Properties.agda + +# Verify RSR compliance using the estate checker +verify: + aletheia . + +# Everything the CI gate runs, in the same order +check: build test diff --git a/aletheia/templates/agda/README.adoc b/aletheia/templates/agda/README.adoc new file mode 100644 index 0000000..1e89576 --- /dev/null +++ b/aletheia/templates/agda/README.adoc @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += @@PROJECT_NAME@@ +:toc: +:icons: font + +____ +@@PROJECT_DESCRIPTION@@ +____ + +== Quick Start + +[source,bash] +---- +# Build (offline — nothing is downloaded) +just build + +# Test +just test + +# Verify RSR compliance +just verify +---- + +This project is *standalone by construction*: the scaffold fetches nothing, +the build has no external dependencies, and the licence texts ship in-tree +under `+LICENSES/+`. + +== RSR Compliance + +[cols="1,3"] +|=== +|Bronze |Documentation, security policy, SPDX headers, CI, licence classification +|Silver |`.editorconfig`, `.tool-versions`, machine-readable manifests, SHA-pinned CI, `+LICENSES/+` +|Gold |No silent-skip recipes +|=== + +Verify with the estate's own checker: + +[source,bash] +---- +aletheia . +---- + +== Language: @@LANG_DISPLAY@@ + +@@LANG_POLICY@@ + +== Documentation + +* link:SECURITY.adoc[Security Policy] — vulnerability disclosure +* link:CONTRIBUTING.adoc[Contributing Guide] — how to contribute +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] — community standards +* link:MAINTAINERS.adoc[Maintainers] — ownership and decisions +* link:CHANGELOG.adoc[Changelog] — version history + +== Layout + +.... +. +├── Justfile # build automation (capital J — v2 shape) +├── LICENSE # licence statement +├── LICENSES/ # full licence texts (REUSE style) +├── src/ # source (layout follows the language's conventions) +├── .github/workflows/ # CI + estate gates +├── .machine_readable/ # machine-readable metadata +└── .well-known/ # security.txt, ai.txt, humans.txt +.... + +== Contributing + +See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc]. + +== License + +Code is licensed under the Mozilla Public License, version 2.0 +(`+MPL-2.0+`). Documentation is licensed under Creative Commons +Attribution-ShareAlike 4.0 International (`+CC-BY-SA-4.0+`). + +See link:LICENSE[LICENSE] and the `+LICENSES/+` directory for full texts. + +''''' + +_Created from the aletheia v2 Bronze template._ diff --git a/aletheia/templates/agda/src/@@MOD_CAMEL@@.agda b/aletheia/templates/agda/src/@@MOD_CAMEL@@.agda new file mode 100644 index 0000000..5e81fda --- /dev/null +++ b/aletheia/templates/agda/src/@@MOD_CAMEL@@.agda @@ -0,0 +1,52 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Core proofs for @@PROJECT_NAME@@. +-- +-- Self-contained by design: only Agda.Builtin is imported, so there is no +-- standard-library dependency to fetch. Replace these with your own +-- definitions and theorems. +module @@MOD_CAMEL@@ where + +open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) +open import Agda.Builtin.Equality using (_≡_; refl) + +------------------------------------------------------------------------ +-- Equality helpers +-- +-- Agda.Builtin.Equality ships only _≡_ and refl, and we do not want a +-- stdlib dependency just for these two. Every argument is annotated with +-- its type: `m ≡ n` with untyped `m`/`n` leaves the type index of _≡_ +-- ambiguous, and Agda reports unsolved metas rather than guessing. +------------------------------------------------------------------------ + +sym : ∀ {m n : Nat} → m ≡ n → n ≡ m +sym refl = refl + +trans : ∀ {l m n : Nat} → l ≡ m → m ≡ n → l ≡ n +trans refl refl = refl + +cong-suc : ∀ {m n : Nat} → m ≡ n → suc m ≡ suc n +cong-suc refl = refl + +------------------------------------------------------------------------ +-- Theorems about addition +------------------------------------------------------------------------ + +-- zero is a left identity for _+_. Holds by computation — no induction +-- needed — so `refl` is already a complete proof. ++-identityˡ : ∀ (n : Nat) → zero + n ≡ n ++-identityˡ n = refl + +-- suc commutes with _+_ on the right. This needs induction, because _+_ +-- recurses on its *first* argument. +suc-+ : ∀ (m n : Nat) → suc (m + n) ≡ m + suc n +suc-+ zero n = refl +suc-+ (suc m) n = cong-suc (suc-+ m n) + +-- zero is a right identity for _+_. Also inductive, for the same reason. ++-identityʳ : ∀ (n : Nat) → n + zero ≡ n ++-identityʳ zero = refl ++-identityʳ (suc n) = cong-suc (+-identityʳ n) + +-- A worked use of all three: zero commutes through addition. ++-zero-comm : ∀ (n : Nat) → n + zero ≡ zero + n ++-zero-comm n = trans (+-identityʳ n) (sym (+-identityˡ n)) diff --git a/aletheia/templates/agda/src/Properties.agda b/aletheia/templates/agda/src/Properties.agda new file mode 100644 index 0000000..2f2f290 --- /dev/null +++ b/aletheia/templates/agda/src/Properties.agda @@ -0,0 +1,29 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Derived results for @@PROJECT_NAME@@. +-- +-- This module is a *consumer* of the core library: it proves new facts +-- from the exported lemmas, so a regression in the core shows up here as +-- a typecheck failure rather than passing unnoticed. +module Properties where + +open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) +open import Agda.Builtin.Equality using (_≡_) + +-- Pairs. Agda.Builtin does not export _×_, so declare it here rather than +-- pull in the standard library for one constructor. +data _×_ (A B : Set) : Set where + _,_ : A → B → A × B + +open import @@MOD_CAMEL@@ using (sym; trans; +-identityˡ; +-identityʳ; suc-+) + +-- zero is an identity for _+_ on both sides at once. ++-zero-identity : ∀ (n : Nat) → ((n + zero) ≡ n) × ((zero + n) ≡ n) ++-zero-identity n = (+-identityʳ n , +-identityˡ n) + +-- Adding zero on the right, twice, is still adding zero once. ++-zero-twice : ∀ (n : Nat) → (n + zero) + zero ≡ n ++-zero-twice n = trans (+-identityʳ (n + zero)) (+-identityʳ n) + +-- The general suc-+ lemma, instantiated at m = suc zero. +suc-+-concrete : ∀ (n : Nat) → suc (suc zero + n) ≡ suc zero + suc n +suc-+-concrete n = suc-+ (suc zero) n diff --git a/aletheia/templates/bronze-rust/README-template.adoc b/aletheia/templates/bronze-rust/README-template.adoc deleted file mode 100644 index 838f45a..0000000 --- a/aletheia/templates/bronze-rust/README-template.adoc +++ /dev/null @@ -1,83 +0,0 @@ -== maa-framework - -____ -\{\{PROJECT_DESCRIPTION}} -____ - -=== 🚀 Quick Start - -[source,bash] ----- -# Clone the repository -git clone {{REPOSITORY_URL}} -cd maa-framework - -# Build -cargo build --release - -# Run -cargo run - -# Test -cargo test ----- - -=== 📊 RSR Compliance - -*Level*: Bronze ✅ - -This project maintains RSR Bronze-level compliance: - -* ✅ Type Safety: Rust compile-time guarantees -* ✅ Memory Safety: Ownership model, zero unsafe blocks -* ✅ Zero Dependencies: Only standard library -* ✅ Offline-First: No network dependencies -* ✅ Complete Documentation: All required docs present -* ✅ Security: RFC 9116 compliant security.txt -* ✅ Build System: Justfile, flake.nix, CI/CD -* ✅ Testing: Comprehensive test suite - -Verify compliance: - -[source,bash] ----- -aletheia . ----- - -=== 🎯 Features - -* Feature 1: \{\{FEATURE_1_DESCRIPTION}} -* Feature 2: \{\{FEATURE_2_DESCRIPTION}} -* Feature 3: \{\{FEATURE_3_DESCRIPTION}} - -=== 📖 Documentation - -* link:SECURITY.md[Security Policy] - Vulnerability disclosure -* link:../../../.github/CONTRIBUTING.md[Contributing Guide] - How to contribute -* link:CODE_OF_CONDUCT.md[Code of Conduct] - Community standards -* link:CHANGELOG.md[Changelog] - Version history - -=== 🤝 Contributing - -We welcome contributions! See CONTRIBUTING.md for guidelines. - -=== 📜 License - -Dual-licensed under: - MIT License - See LICENSE-MIT.txt - -\{\{ALTERNATIVE_LICENSE}} - See LICENSE-%7B%7BALTERNATIVE%7D%7D.txt - -=== 🙏 Acknowledgments - -* Built with https://www.rust-lang.org/[Rust] -* RSR compliant via -https://gitlab.com/maa-framework/6-the-foundation/aletheia[Aletheia] - -=== 📞 Contact - -* *Repository*: \{\{REPOSITORY_URL}} -* *Issues*: \{\{ISSUES_URL}} -* *Security*: See SECURITY.md - -''''' - -_\{\{PROJECT_TAGLINE}}_ diff --git a/aletheia/templates/common/.gitattributes b/aletheia/templates/common/.gitattributes new file mode 100644 index 0000000..c74ab88 --- /dev/null +++ b/aletheia/templates/common/.gitattributes @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: MPL-2.0 +* text=auto eol=lf + +@@LANG_GITATTR_LINE@@ +*.adoc text eol=lf +*.a2ml text eol=lf +*.yml text eol=lf +*.yaml text eol=lf +*.toml text eol=lf + +LICENSES/* text eol=lf diff --git a/aletheia/templates/common/.github/workflows/actions.lock b/aletheia/templates/common/.github/workflows/actions.lock new file mode 100644 index 0000000..523511c --- /dev/null +++ b/aletheia/templates/common/.github/workflows/actions.lock @@ -0,0 +1,9 @@ +# This file is machine-generated by `gh actions-lock`. +# Do not edit by hand; run `gh actions-lock` to update. +# Docs: https://gh.io/actions-lockfile +version: 'v0.0.2' +workflows: + '.github/workflows/ci.yml': + - 'actions/checkout@v7.0.1' + '.github/workflows/governance.yml': [] + '.github/workflows/hypatia-scan.yml': [] diff --git a/aletheia/templates/common/.github/workflows/governance.yml b/aletheia/templates/common/.github/workflows/governance.yml new file mode 100644 index 0000000..5c808fe --- /dev/null +++ b/aletheia/templates/common/.github/workflows/governance.yml @@ -0,0 +1,18 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +name: Governance + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + workflow_dispatch: + +permissions: + actions: read + contents: read + +jobs: + governance: + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813 diff --git a/aletheia/templates/common/.github/workflows/hypatia-scan.yml b/aletheia/templates/common/.github/workflows/hypatia-scan.yml new file mode 100644 index 0000000..f839298 --- /dev/null +++ b/aletheia/templates/common/.github/workflows/hypatia-scan.yml @@ -0,0 +1,21 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +name: Hypatia Security Scan + +on: + push: + branches: [main, master, develop] + pull_request: + branches: [main, master] + schedule: + - cron: '0 0 * * 0' + workflow_dispatch: + +permissions: + actions: read + contents: read + security-events: write + +jobs: + hypatia: + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a diff --git a/aletheia/templates/common/.well-known/ai.txt b/aletheia/templates/common/.well-known/ai.txt new file mode 100644 index 0000000..d30fbd9 --- /dev/null +++ b/aletheia/templates/common/.well-known/ai.txt @@ -0,0 +1,15 @@ +# SPDX-License-Identifier: MPL-2.0 +# ai.txt - AI interaction policy + +User-Agent: * +Disallow-Training: yes +Disallow-Summarization: no +Disallow-Generation: yes + +# This project's code is licensed under MPL-2.0. +# AI agents may read and analyse this code to assist contributors. +# AI agents must NOT use this code for model training without explicit consent. +# +# Agent integration instructions: +# 0-AI-MANIFEST.a2ml (universal AI entry point) +# .machine_readable/ (structured project state) diff --git a/aletheia/templates/common/.well-known/humans.txt b/aletheia/templates/common/.well-known/humans.txt new file mode 100644 index 0000000..75d2bc2 --- /dev/null +++ b/aletheia/templates/common/.well-known/humans.txt @@ -0,0 +1,13 @@ +# SPDX-License-Identifier: MPL-2.0 +# humanstxt.org + +/* TEAM */ +Maintainer: @@AUTHOR_NAME@@ +Contact: @@AUTHOR_EMAIL@@ + +/* SITE */ +Last update: @@DATE@@ +Standards: RSR (Rhodium Standard Repository) +Language: Rust/Creusot +License: MPL-2.0 +Tools: just, cargo diff --git a/aletheia/templates/common/.well-known/security.txt b/aletheia/templates/common/.well-known/security.txt new file mode 100644 index 0000000..8ce5343 --- /dev/null +++ b/aletheia/templates/common/.well-known/security.txt @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: MPL-2.0 +# RFC 9116 - security.txt +# https://securitytxt.org/ + +Contact: mailto:@@SECURITY_CONTACT@@ +Expires: @@SECURITY_EXPIRES@@ +Preferred-Languages: en +Canonical: @@REPO_URL@@/blob/main/.well-known/security.txt +Policy: @@REPO_URL@@/blob/main/SECURITY.adoc diff --git a/aletheia/templates/common/0-AI-MANIFEST.a2ml b/aletheia/templates/common/0-AI-MANIFEST.a2ml new file mode 100644 index 0000000..f0a203c --- /dev/null +++ b/aletheia/templates/common/0-AI-MANIFEST.a2ml @@ -0,0 +1,52 @@ +# SPDX-License-Identifier: MPL-2.0 +# @@PROJECT_NAME@@ — universal AI agent entry point. + +# THIS FILE MUST BE READ FIRST BY ALL AI AGENTS + +## What Is This? + +The AI manifest for **@@PROJECT_NAME@@**. It declares canonical file +locations and the invariants an agent must not violate. + +## Canonical Locations + +### Machine-Readable Metadata: `.machine_readable/` ONLY + +* `.machine_readable/rsr-profile.a2ml` — capability declaration driving the + applicable RSR criterion set + +If any machine-readable metadata appears in the repository root, that is an +error: the root must contain only the agent front door +(`0-AI-MANIFEST.a2ml`). + +### Agent Instructions + +* `0-AI-MANIFEST.a2ml` — THIS FILE (universal entry point) +* `.claude/CLAUDE.md` — Claude-specific patterns (if present) + +## Core Invariants + +1. *No metadata duplication* — `.machine_readable/` is the single source of truth. +2. *Standalone by construction* — @@STANDALONE_INVARIANT@@ +3. *Dependency budget* — @@DEP_INVARIANT@@ +4. *Language policy* — @@LANG_INVARIANT@@ +5. *No fake gates* — a recipe that echoes a message and exits 0 is a + violation. Fail loudly. +6. *SPDX headers* — every source file carries an `SPDX-License-Identifier` + within its first ten lines. Code is `MPL-2.0`; docs are `CC-BY-SA-4.0`. +7. *Licence consistency* — MPL-2.0 across the repository. + +## Session Startup Checklist + +* Read THIS file first. +* Read `.machine_readable/rsr-profile.a2ml` for declared capabilities. +* Run `just check` to confirm the tree is green before changing anything. +* State understanding of canonical locations before writing files. + +## Attestation + +After reading this file, state: + +**"I have read the AI manifest. Machine-readable metadata lives in +`.machine_readable/` only, the build is standalone, and @@LANG_DISPLAY@@ +means what the estate language policy says it means."** diff --git a/aletheia/templates/common/CHANGELOG.adoc b/aletheia/templates/common/CHANGELOG.adoc new file mode 100644 index 0000000..ae8a126 --- /dev/null +++ b/aletheia/templates/common/CHANGELOG.adoc @@ -0,0 +1,19 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Changelog + +All notable changes to this project are documented in this file. + +The format is based on https://keepachangelog.com/[Keep a Changelog], and +this project adheres to https://semver.org/[Semantic Versioning]. + +== [Unreleased] + +=== Added + +* Initial project structure. + +== [0.1.0] - @@DATE@@ + +=== Added + +* Initial release. diff --git a/aletheia/templates/common/CODE_OF_CONDUCT.adoc b/aletheia/templates/common/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd0ca64 --- /dev/null +++ b/aletheia/templates/common/CODE_OF_CONDUCT.adoc @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Code of Conduct +:toc: + +== Our Pledge + +We pledge to make participation in this project a harassment-free +experience for everyone, regardless of age, body size, disability, +ethnicity, gender identity and expression, level of experience, +nationality, personal appearance, race, religion, or sexual identity and +orientation. + +== Our Standards + +Examples of behaviour that creates a positive environment: + +* Being respectful of differing viewpoints and experiences +* Giving and accepting constructive feedback +* Focusing on what is best for the community +* Showing empathy towards other community members + +Examples of unacceptable behaviour: + +* Harassment, trolling, or insulting comments +* Publishing others' private information without permission +*Other conduct which could reasonably be considered inappropriate + +== Enforcement + +Report violations to **@@CONDUCT_CONTACT@@**. All complaints will be +reviewed and investigated promptly and fairly. Maintainers are obligated to +respect the privacy and security of the reporter. + +== Attribution + +Adapted from the Contributor Covenant, version 2.1. diff --git a/aletheia/templates/common/CONTRIBUTING.adoc b/aletheia/templates/common/CONTRIBUTING.adoc new file mode 100644 index 0000000..2609bcc --- /dev/null +++ b/aletheia/templates/common/CONTRIBUTING.adoc @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Contributing +:toc: + +== Getting Started + +[source,bash] +---- +git clone @@REPO_URL@@ +cd @@PROJECT_NAME@@ +just check +---- + +`just check` is the same gate CI runs. It must pass before you open a pull +request. + +== Workflow + +. Fork the repository. +. Create a branch: `+git checkout -b feat/my-feature+`. +. Make your change, with tests. +. Run `+just check+`. +. Commit using Conventional Commits (`+feat:+`, `+fix:+`, `+docs:+`, `+chore:+`). +. Open a pull request. + +== Standards + +This project follows the RSR (Rhodium Standard Repository) criteria. Two +rules bite most often: + +* *No silent skips.* A recipe that echoes a message and exits 0 is a fake + gate. Fail loudly. +* *SPDX headers.* Every source file carries an `+SPDX-License-Identifier+` + in its first ten lines. + +== Language Policy + +@@LANG_POLICY@@ + +== Review + +Pull requests require review before merge. See link:MAINTAINERS.adoc[MAINTAINERS.adoc] +for decision-making. diff --git a/aletheia/templates/common/LICENSE b/aletheia/templates/common/LICENSE new file mode 100644 index 0000000..b306f89 --- /dev/null +++ b/aletheia/templates/common/LICENSE @@ -0,0 +1,9 @@ +Mozilla Public License Version 2.0 (MPL-2.0) + +Code in this repository is licensed under the Mozilla Public License, +version 2.0. Documentation is licensed under Creative Commons +Attribution-ShareAlike 4.0 International (CC-BY-SA-4.0). + +See the LICENSES/ directory for the full license texts. + +SPDX-License-Identifier: MPL-2.0 diff --git a/aletheia/templates/common/LICENSES/CC-BY-SA-4.0.txt b/aletheia/templates/common/LICENSES/CC-BY-SA-4.0.txt new file mode 100644 index 0000000..2d58298 --- /dev/null +++ b/aletheia/templates/common/LICENSES/CC-BY-SA-4.0.txt @@ -0,0 +1,428 @@ +Attribution-ShareAlike 4.0 International + +======================================================================= + +Creative Commons Corporation ("Creative Commons") is not a law firm and +does not provide legal services or legal advice. Distribution of +Creative Commons public licenses does not create a lawyer-client or +other relationship. Creative Commons makes its licenses and related +information available on an "as-is" basis. Creative Commons gives no +warranties regarding its licenses, any material licensed under their +terms and conditions, or any related information. Creative Commons +disclaims all liability for damages resulting from their use to the +fullest extent possible. + +Using Creative Commons Public Licenses + +Creative Commons public licenses provide a standard set of terms and +conditions that creators and other rights holders may use to share +original works of authorship and other material subject to copyright +and certain other rights specified in the public license below. The +following considerations are for informational purposes only, are not +exhaustive, and do not form part of our licenses. + + Considerations for licensors: Our public licenses are + intended for use by those authorized to give the public + permission to use material in ways otherwise restricted by + copyright and certain other rights. Our licenses are + irrevocable. Licensors should read and understand the terms + and conditions of the license they choose before applying it. + Licensors should also secure all rights necessary before + applying our licenses so that the public can reuse the + material as expected. Licensors should clearly mark any + material not subject to the license. This includes other CC- + licensed material, or material used under an exception or + limitation to copyright. More considerations for licensors: + wiki.creativecommons.org/Considerations_for_licensors + + Considerations for the public: By using one of our public + licenses, a licensor grants the public permission to use the + licensed material under specified terms and conditions. If + the licensor's permission is not necessary for any reason--for + example, because of any applicable exception or limitation to + copyright--then that use is not regulated by the license. Our + licenses grant only permissions under copyright and certain + other rights that a licensor has authority to grant. Use of + the licensed material may still be restricted for other + reasons, including because others have copyright or other + rights in the material. A licensor may make special requests, + such as asking that all changes be marked or described. + Although not required by our licenses, you are encouraged to + respect those requests where reasonable. More considerations + for the public: + wiki.creativecommons.org/Considerations_for_licensees + +======================================================================= + +Creative Commons Attribution-ShareAlike 4.0 International Public +License + +By exercising the Licensed Rights (defined below), You accept and agree +to be bound by the terms and conditions of this Creative Commons +Attribution-ShareAlike 4.0 International Public License ("Public +License"). To the extent this Public License may be interpreted as a +contract, You are granted the Licensed Rights in consideration of Your +acceptance of these terms and conditions, and the Licensor grants You +such rights in consideration of benefits the Licensor receives from +making the Licensed Material available under these terms and +conditions. + + +Section 1 -- Definitions. + + a. Adapted Material means material subject to Copyright and Similar + Rights that is derived from or based upon the Licensed Material + and in which the Licensed Material is translated, altered, + arranged, transformed, or otherwise modified in a manner requiring + permission under the Copyright and Similar Rights held by the + Licensor. For purposes of this Public License, where the Licensed + Material is a musical work, performance, or sound recording, + Adapted Material is always produced where the Licensed Material is + synched in timed relation with a moving image. + + b. Adapter's License means the license You apply to Your Copyright + and Similar Rights in Your contributions to Adapted Material in + accordance with the terms and conditions of this Public License. + + c. BY-SA Compatible License means a license listed at + creativecommons.org/compatiblelicenses, approved by Creative + Commons as essentially the equivalent of this Public License. + + d. Copyright and Similar Rights means copyright and/or similar rights + closely related to copyright including, without limitation, + performance, broadcast, sound recording, and Sui Generis Database + Rights, without regard to how the rights are labeled or + categorized. For purposes of this Public License, the rights + specified in Section 2(b)(1)-(2) are not Copyright and Similar + Rights. + + e. Effective Technological Measures means those measures that, in the + absence of proper authority, may not be circumvented under laws + fulfilling obligations under Article 11 of the WIPO Copyright + Treaty adopted on December 20, 1996, and/or similar international + agreements. + + f. Exceptions and Limitations means fair use, fair dealing, and/or + any other exception or limitation to Copyright and Similar Rights + that applies to Your use of the Licensed Material. + + g. License Elements means the license attributes listed in the name + of a Creative Commons Public License. The License Elements of this + Public License are Attribution and ShareAlike. + + h. Licensed Material means the artistic or literary work, database, + or other material to which the Licensor applied this Public + License. + + i. Licensed Rights means the rights granted to You subject to the + terms and conditions of this Public License, which are limited to + all Copyright and Similar Rights that apply to Your use of the + Licensed Material and that the Licensor has authority to license. + + j. Licensor means the individual(s) or entity(ies) granting rights + under this Public License. + + k. Share means to provide material to the public by any means or + process that requires permission under the Licensed Rights, such + as reproduction, public display, public performance, distribution, + dissemination, communication, or importation, and to make material + available to the public including in ways that members of the + public may access the material from a place and at a time + individually chosen by them. + + l. Sui Generis Database Rights means rights other than copyright + resulting from Directive 96/9/EC of the European Parliament and of + the Council of 11 March 1996 on the legal protection of databases, + as amended and/or succeeded, as well as other essentially + equivalent rights anywhere in the world. + + m. You means the individual or entity exercising the Licensed Rights + under this Public License. Your has a corresponding meaning. + + +Section 2 -- Scope. + + a. License grant. + + 1. Subject to the terms and conditions of this Public License, + the Licensor hereby grants You a worldwide, royalty-free, + non-sublicensable, non-exclusive, irrevocable license to + exercise the Licensed Rights in the Licensed Material to: + + a. reproduce and Share the Licensed Material, in whole or + in part; and + + b. produce, reproduce, and Share Adapted Material. + + 2. Exceptions and Limitations. For the avoidance of doubt, where + Exceptions and Limitations apply to Your use, this Public + License does not apply, and You do not need to comply with + its terms and conditions. + + 3. Term. The term of this Public License is specified in Section + 6(a). + + 4. Media and formats; technical modifications allowed. The + Licensor authorizes You to exercise the Licensed Rights in + all media and formats whether now known or hereafter created, + and to make technical modifications necessary to do so. The + Licensor waives and/or agrees not to assert any right or + authority to forbid You from making technical modifications + necessary to exercise the Licensed Rights, including + technical modifications necessary to circumvent Effective + Technological Measures. For purposes of this Public License, + simply making modifications authorized by this Section 2(a) + (4) never produces Adapted Material. + + 5. Downstream recipients. + + a. Offer from the Licensor -- Licensed Material. Every + recipient of the Licensed Material automatically + receives an offer from the Licensor to exercise the + Licensed Rights under the terms and conditions of this + Public License. + + b. Additional offer from the Licensor -- Adapted Material. + Every recipient of Adapted Material from You + automatically receives an offer from the Licensor to + exercise the Licensed Rights in the Adapted Material + under the conditions of the Adapter's License You apply. + + c. No downstream restrictions. You may not offer or impose + any additional or different terms or conditions on, or + apply any Effective Technological Measures to, the + Licensed Material if doing so restricts exercise of the + Licensed Rights by any recipient of the Licensed + Material. + + 6. No endorsement. Nothing in this Public License constitutes or + may be construed as permission to assert or imply that You + are, or that Your use of the Licensed Material is, connected + with, or sponsored, endorsed, or granted official status by, + the Licensor or others designated to receive attribution as + provided in Section 3(a)(1)(A)(i). + + b. Other rights. + + 1. Moral rights, such as the right of integrity, are not + licensed under this Public License, nor are publicity, + privacy, and/or other similar personality rights; however, to + the extent possible, the Licensor waives and/or agrees not to + assert any such rights held by the Licensor to the limited + extent necessary to allow You to exercise the Licensed + Rights, but not otherwise. + + 2. Patent and trademark rights are not licensed under this + Public License. + + 3. To the extent possible, the Licensor waives any right to + collect royalties from You for the exercise of the Licensed + Rights, whether directly or through a collecting society + under any voluntary or waivable statutory or compulsory + licensing scheme. In all other cases the Licensor expressly + reserves any right to collect such royalties. + + +Section 3 -- License Conditions. + +Your exercise of the Licensed Rights is expressly made subject to the +following conditions. + + a. Attribution. + + 1. If You Share the Licensed Material (including in modified + form), You must: + + a. retain the following if it is supplied by the Licensor + with the Licensed Material: + + i. identification of the creator(s) of the Licensed + Material and any others designated to receive + attribution, in any reasonable manner requested by + the Licensor (including by pseudonym if + designated); + + ii. a copyright notice; + + iii. a notice that refers to this Public License; + + iv. a notice that refers to the disclaimer of + warranties; + + v. a URI or hyperlink to the Licensed Material to the + extent reasonably practicable; + + b. indicate if You modified the Licensed Material and + retain an indication of any previous modifications; and + + c. indicate the Licensed Material is licensed under this + Public License, and include the text of, or the URI or + hyperlink to, this Public License. + + 2. You may satisfy the conditions in Section 3(a)(1) in any + reasonable manner based on the medium, means, and context in + which You Share the Licensed Material. For example, it may be + reasonable to satisfy the conditions by providing a URI or + hyperlink to a resource that includes the required + information. + + 3. If requested by the Licensor, You must remove any of the + information required by Section 3(a)(1)(A) to the extent + reasonably practicable. + + b. ShareAlike. + + In addition to the conditions in Section 3(a), if You Share + Adapted Material You produce, the following conditions also apply. + + 1. The Adapter's License You apply must be a Creative Commons + license with the same License Elements, this version or + later, or a BY-SA Compatible License. + + 2. You must include the text of, or the URI or hyperlink to, the + Adapter's License You apply. You may satisfy this condition + in any reasonable manner based on the medium, means, and + context in which You Share Adapted Material. + + 3. You may not offer or impose any additional or different terms + or conditions on, or apply any Effective Technological + Measures to, Adapted Material that restrict exercise of the + rights granted under the Adapter's License You apply. + + +Section 4 -- Sui Generis Database Rights. + +Where the Licensed Rights include Sui Generis Database Rights that +apply to Your use of the Licensed Material: + + a. for the avoidance of doubt, Section 2(a)(1) grants You the right + to extract, reuse, reproduce, and Share all or a substantial + portion of the contents of the database; + + b. if You include all or a substantial portion of the database + contents in a database in which You have Sui Generis Database + Rights, then the database in which You have Sui Generis Database + Rights (but not its individual contents) is Adapted Material, + including for purposes of Section 3(b); and + + c. You must comply with the conditions in Section 3(a) if You Share + all or a substantial portion of the contents of the database. + +For the avoidance of doubt, this Section 4 supplements and does not +replace Your obligations under this Public License where the Licensed +Rights include other Copyright and Similar Rights. + + +Section 5 -- Disclaimer of Warranties and Limitation of Liability. + + a. UNLESS OTHERWISE SEPARATELY UNDERTAKEN BY THE LICENSOR, TO THE + EXTENT POSSIBLE, THE LICENSOR OFFERS THE LICENSED MATERIAL AS-IS + AND AS-AVAILABLE, AND MAKES NO REPRESENTATIONS OR WARRANTIES OF + ANY KIND CONCERNING THE LICENSED MATERIAL, WHETHER EXPRESS, + IMPLIED, STATUTORY, OR OTHER. THIS INCLUDES, WITHOUT LIMITATION, + WARRANTIES OF TITLE, MERCHANTABILITY, FITNESS FOR A PARTICULAR + PURPOSE, NON-INFRINGEMENT, ABSENCE OF LATENT OR OTHER DEFECTS, + ACCURACY, OR THE PRESENCE OR ABSENCE OF ERRORS, WHETHER OR NOT + KNOWN OR DISCOVERABLE. WHERE DISCLAIMERS OF WARRANTIES ARE NOT + ALLOWED IN FULL OR IN PART, THIS DISCLAIMER MAY NOT APPLY TO YOU. + + b. TO THE EXTENT POSSIBLE, IN NO EVENT WILL THE LICENSOR BE LIABLE + TO YOU ON ANY LEGAL THEORY (INCLUDING, WITHOUT LIMITATION, + NEGLIGENCE) OR OTHERWISE FOR ANY DIRECT, SPECIAL, INDIRECT, + INCIDENTAL, CONSEQUENTIAL, PUNITIVE, EXEMPLARY, OR OTHER LOSSES, + COSTS, EXPENSES, OR DAMAGES ARISING OUT OF THIS PUBLIC LICENSE OR + USE OF THE LICENSED MATERIAL, EVEN IF THE LICENSOR HAS BEEN + ADVISED OF THE POSSIBILITY OF SUCH LOSSES, COSTS, EXPENSES, OR + DAMAGES. WHERE A LIMITATION OF LIABILITY IS NOT ALLOWED IN FULL OR + IN PART, THIS LIMITATION MAY NOT APPLY TO YOU. + + c. The disclaimer of warranties and limitation of liability provided + above shall be interpreted in a manner that, to the extent + possible, most closely approximates an absolute disclaimer and + waiver of all liability. + + +Section 6 -- Term and Termination. + + a. This Public License applies for the term of the Copyright and + Similar Rights licensed here. However, if You fail to comply with + this Public License, then Your rights under this Public License + terminate automatically. + + b. Where Your right to use the Licensed Material has terminated under + Section 6(a), it reinstates: + + 1. automatically as of the date the violation is cured, provided + it is cured within 30 days of Your discovery of the + violation; or + + 2. upon express reinstatement by the Licensor. + + For the avoidance of doubt, this Section 6(b) does not affect any + right the Licensor may have to seek remedies for Your violations + of this Public License. + + c. For the avoidance of doubt, the Licensor may also offer the + Licensed Material under separate terms or conditions or stop + distributing the Licensed Material at any time; however, doing so + will not terminate this Public License. + + d. Sections 1, 5, 6, 7, and 8 survive termination of this Public + License. + + +Section 7 -- Other Terms and Conditions. + + a. The Licensor shall not be bound by any additional or different + terms or conditions communicated by You unless expressly agreed. + + b. Any arrangements, understandings, or agreements regarding the + Licensed Material not stated herein are separate from and + independent of the terms and conditions of this Public License. + + +Section 8 -- Interpretation. + + a. For the avoidance of doubt, this Public License does not, and + shall not be interpreted to, reduce, limit, restrict, or impose + conditions on any use of the Licensed Material that could lawfully + be made without permission under this Public License. + + b. To the extent possible, if any provision of this Public License is + deemed unenforceable, it shall be automatically reformed to the + minimum extent necessary to make it enforceable. If the provision + cannot be reformed, it shall be severed from this Public License + without affecting the enforceability of the remaining terms and + conditions. + + c. No term or condition of this Public License will be waived and no + failure to comply consented to unless expressly agreed to by the + Licensor. + + d. Nothing in this Public License constitutes or may be interpreted + as a limitation upon, or waiver of, any privileges and immunities + that apply to the Licensor or You, including from the legal + processes of any jurisdiction or authority. + + +======================================================================= + +Creative Commons is not a party to its public +licenses. Notwithstanding, Creative Commons may elect to apply one of +its public licenses to material it publishes and in those instances +will be considered the “Licensor.” The text of the Creative Commons +public licenses is dedicated to the public domain under the CC0 Public +Domain Dedication. Except for the limited purpose of indicating that +material is shared under a Creative Commons public license or as +otherwise permitted by the Creative Commons policies published at +creativecommons.org/policies, Creative Commons does not authorize the +use of the trademark "Creative Commons" or any other trademark or logo +of Creative Commons without its prior written consent including, +without limitation, in connection with any unauthorized modifications +to any of its public licenses or any other arrangements, +understandings, or agreements concerning use of licensed material. For +the avoidance of doubt, this paragraph does not form part of the +public licenses. + +Creative Commons may be contacted at creativecommons.org. + diff --git a/aletheia/templates/common/LICENSES/MPL-2.0.txt b/aletheia/templates/common/LICENSES/MPL-2.0.txt new file mode 100644 index 0000000..d0a1fa1 --- /dev/null +++ b/aletheia/templates/common/LICENSES/MPL-2.0.txt @@ -0,0 +1,373 @@ +Mozilla Public License Version 2.0 +================================== + +1. Definitions +-------------- + +1.1. "Contributor" + means each individual or legal entity that creates, contributes to + the creation of, or owns Covered Software. + +1.2. "Contributor Version" + means the combination of the Contributions of others (if any) used + by a Contributor and that particular Contributor's Contribution. + +1.3. "Contribution" + means Covered Software of a particular Contributor. + +1.4. "Covered Software" + means Source Code Form to which the initial Contributor has attached + the notice in Exhibit A, the Executable Form of such Source Code + Form, and Modifications of such Source Code Form, in each case + including portions thereof. + +1.5. "Incompatible With Secondary Licenses" + means + + (a) that the initial Contributor has attached the notice described + in Exhibit B to the Covered Software; or + + (b) that the Covered Software was made available under the terms of + version 1.1 or earlier of the License, but not also under the + terms of a Secondary License. + +1.6. "Executable Form" + means any form of the work other than Source Code Form. + +1.7. "Larger Work" + means a work that combines Covered Software with other material, in + a separate file or files, that is not Covered Software. + +1.8. "License" + means this document. + +1.9. "Licensable" + means having the right to grant, to the maximum extent possible, + whether at the time of the initial grant or subsequently, any and + all of the rights conveyed by this License. + +1.10. "Modifications" + means any of the following: + + (a) any file in Source Code Form that results from an addition to, + deletion from, or modification of the contents of Covered + Software; or + + (b) any new file in Source Code Form that contains any Covered + Software. + +1.11. "Patent Claims" of a Contributor + means any patent claim(s), including without limitation, method, + process, and apparatus claims, in any patent Licensable by such + Contributor that would be infringed, but for the grant of the + License, by the making, using, selling, offering for sale, having + made, import, or transfer of either its Contributions or its + Contributor Version. + +1.12. "Secondary License" + means either the GNU General Public License, Version 2.0, the GNU + Lesser General Public License, Version 2.1, the GNU Affero General + Public License, Version 3.0, or any later versions of those + licenses. + +1.13. "Source Code Form" + means the form of the work preferred for making modifications. + +1.14. "You" (or "Your") + means an individual or a legal entity exercising rights under this + License. For legal entities, "You" includes any entity that + controls, is controlled by, or is under common control with You. For + purposes of this definition, "control" means (a) the power, direct + or indirect, to cause the direction or management of such entity, + whether by contract or otherwise, or (b) ownership of more than + fifty percent (50%) of the outstanding shares or beneficial + ownership of such entity. + +2. License Grants and Conditions +-------------------------------- + +2.1. Grants + +Each Contributor hereby grants You a world-wide, royalty-free, +non-exclusive license: + +(a) under intellectual property rights (other than patent or trademark) + Licensable by such Contributor to use, reproduce, make available, + modify, display, perform, distribute, and otherwise exploit its + Contributions, either on an unmodified basis, with Modifications, or + as part of a Larger Work; and + +(b) under Patent Claims of such Contributor to make, use, sell, offer + for sale, have made, import, and otherwise transfer either its + Contributions or its Contributor Version. + +2.2. Effective Date + +The licenses granted in Section 2.1 with respect to any Contribution +become effective for each Contribution on the date the Contributor first +distributes such Contribution. + +2.3. Limitations on Grant Scope + +The licenses granted in this Section 2 are the only rights granted under +this License. No additional rights or licenses will be implied from the +distribution or licensing of Covered Software under this License. +Notwithstanding Section 2.1(b) above, no patent license is granted by a +Contributor: + +(a) for any code that a Contributor has removed from Covered Software; + or + +(b) for infringements caused by: (i) Your and any other third party's + modifications of Covered Software, or (ii) the combination of its + Contributions with other software (except as part of its Contributor + Version); or + +(c) under Patent Claims infringed by Covered Software in the absence of + its Contributions. + +This License does not grant any rights in the trademarks, service marks, +or logos of any Contributor (except as may be necessary to comply with +the notice requirements in Section 3.4). + +2.4. Subsequent Licenses + +No Contributor makes additional grants as a result of Your choice to +distribute the Covered Software under a subsequent version of this +License (see Section 10.2) or under the terms of a Secondary License (if +permitted under the terms of Section 3.3). + +2.5. Representation + +Each Contributor represents that the Contributor believes its +Contributions are its original creation(s) or it has sufficient rights +to grant the rights to its Contributions conveyed by this License. + +2.6. Fair Use + +This License is not intended to limit any rights You have under +applicable copyright doctrines of fair use, fair dealing, or other +equivalents. + +2.7. Conditions + +Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted +in Section 2.1. + +3. Responsibilities +------------------- + +3.1. Distribution of Source Form + +All distribution of Covered Software in Source Code Form, including any +Modifications that You create or to which You contribute, must be under +the terms of this License. You must inform recipients that the Source +Code Form of the Covered Software is governed by the terms of this +License, and how they can obtain a copy of this License. You may not +attempt to alter or restrict the recipients' rights in the Source Code +Form. + +3.2. Distribution of Executable Form + +If You distribute Covered Software in Executable Form then: + +(a) such Covered Software must also be made available in Source Code + Form, as described in Section 3.1, and You must inform recipients of + the Executable Form how they can obtain a copy of such Source Code + Form by reasonable means in a timely manner, at a charge no more + than the cost of distribution to the recipient; and + +(b) You may distribute such Executable Form under the terms of this + License, or sublicense it under different terms, provided that the + license for the Executable Form does not attempt to limit or alter + the recipients' rights in the Source Code Form under this License. + +3.3. Distribution of a Larger Work + +You may create and distribute a Larger Work under terms of Your choice, +provided that You also comply with the requirements of this License for +the Covered Software. If the Larger Work is a combination of Covered +Software with a work governed by one or more Secondary Licenses, and the +Covered Software is not Incompatible With Secondary Licenses, this +License permits You to additionally distribute such Covered Software +under the terms of such Secondary License(s), so that the recipient of +the Larger Work may, at their option, further distribute the Covered +Software under the terms of either this License or such Secondary +License(s). + +3.4. Notices + +You may not remove or alter the substance of any license notices +(including copyright notices, patent notices, disclaimers of warranty, +or limitations of liability) contained within the Source Code Form of +the Covered Software, except that You may alter any license notices to +the extent required to remedy known factual inaccuracies. + +3.5. Application of Additional Terms + +You may choose to offer, and to charge a fee for, warranty, support, +indemnity or liability obligations to one or more recipients of Covered +Software. However, You may do so only on Your own behalf, and not on +behalf of any Contributor. You must make it absolutely clear that any +such warranty, support, indemnity, or liability obligation is offered by +You alone, and You hereby agree to indemnify every Contributor for any +liability incurred by such Contributor as a result of warranty, support, +indemnity or liability terms You offer. You may include additional +disclaimers of warranty and limitations of liability specific to any +jurisdiction. + +4. Inability to Comply Due to Statute or Regulation +--------------------------------------------------- + +If it is impossible for You to comply with any of the terms of this +License with respect to some or all of the Covered Software due to +statute, judicial order, or regulation then You must: (a) comply with +the terms of this License to the maximum extent possible; and (b) +describe the limitations and the code they affect. Such description must +be placed in a text file included with all distributions of the Covered +Software under this License. Except to the extent prohibited by statute +or regulation, such description must be sufficiently detailed for a +recipient of ordinary skill to be able to understand it. + +5. Termination +-------------- + +5.1. The rights granted under this License will terminate automatically +if You fail to comply with any of its terms. However, if You become +compliant, then the rights granted under this License from a particular +Contributor are reinstated (a) provisionally, unless and until such +Contributor explicitly and finally terminates Your grants, and (b) on an +ongoing basis, if such Contributor fails to notify You of the +non-compliance by some reasonable means prior to 60 days after You have +come back into compliance. Moreover, Your grants from a particular +Contributor are reinstated on an ongoing basis if such Contributor +notifies You of the non-compliance by some reasonable means, this is the +first time You have received notice of non-compliance with this License +from such Contributor, and You become compliant prior to 30 days after +Your receipt of the notice. + +5.2. If You initiate litigation against any entity by asserting a patent +infringement claim (excluding declaratory judgment actions, +counter-claims, and cross-claims) alleging that a Contributor Version +directly or indirectly infringes any patent, then the rights granted to +You by any and all Contributors for the Covered Software under Section +2.1 of this License shall terminate. + +5.3. In the event of termination under Sections 5.1 or 5.2 above, all +end user license agreements (excluding distributors and resellers) which +have been validly granted by You or Your distributors under this License +prior to termination shall survive termination. + +************************************************************************ +* * +* 6. Disclaimer of Warranty * +* ------------------------- * +* * +* Covered Software is provided under this License on an "as is" * +* basis, without warranty of any kind, either expressed, implied, or * +* statutory, including, without limitation, warranties that the * +* Covered Software is free of defects, merchantable, fit for a * +* particular purpose or non-infringing. The entire risk as to the * +* quality and performance of the Covered Software is with You. * +* Should any Covered Software prove defective in any respect, You * +* (not any Contributor) assume the cost of any necessary servicing, * +* repair, or correction. This disclaimer of warranty constitutes an * +* essential part of this License. No use of any Covered Software is * +* authorized under this License except under this disclaimer. * +* * +************************************************************************ + +************************************************************************ +* * +* 7. Limitation of Liability * +* -------------------------- * +* * +* Under no circumstances and under no legal theory, whether tort * +* (including negligence), contract, or otherwise, shall any * +* Contributor, or anyone who distributes Covered Software as * +* permitted above, be liable to You for any direct, indirect, * +* special, incidental, or consequential damages of any character * +* including, without limitation, damages for lost profits, loss of * +* goodwill, work stoppage, computer failure or malfunction, or any * +* and all other commercial damages or losses, even if such party * +* shall have been informed of the possibility of such damages. This * +* limitation of liability shall not apply to liability for death or * +* personal injury resulting from such party's negligence to the * +* extent applicable law prohibits such limitation. Some * +* jurisdictions do not allow the exclusion or limitation of * +* incidental or consequential damages, so this exclusion and * +* limitation may not apply to You. * +* * +************************************************************************ + +8. Litigation +------------- + +Any litigation relating to this License may be brought only in the +courts of a jurisdiction where the defendant maintains its principal +place of business and such litigation shall be governed by laws of that +jurisdiction, without reference to its conflict-of-law provisions. +Nothing in this Section shall prevent a party's ability to bring +cross-claims or counter-claims. + +9. Miscellaneous +---------------- + +This License represents the complete agreement concerning the subject +matter hereof. If any provision of this License is held to be +unenforceable, such provision shall be reformed only to the extent +necessary to make it enforceable. Any law or regulation which provides +that the language of a contract shall be construed against the drafter +shall not be used to construe this License against a Contributor. + +10. Versions of the License +--------------------------- + +10.1. New Versions + +Mozilla Foundation is the license steward. Except as provided in Section +10.3, no one other than the license steward has the right to modify or +publish new versions of this License. Each version will be given a +distinguishing version number. + +10.2. Effect of New Versions + +You may distribute the Covered Software under the terms of the version +of the License under which You originally received the Covered Software, +or under the terms of any subsequent version published by the license +steward. + +10.3. Modified Versions + +If you create software not governed by this License, and you want to +create a new license for such software, you may create and use a +modified version of this License if you rename the license and remove +any references to the name of the license steward (except to note that +such modified license differs from this License). + +10.4. Distributing Source Code Form that is Incompatible With Secondary +Licenses + +If You choose to distribute Source Code Form that is Incompatible With +Secondary Licenses under the terms of this version of the License, the +notice described in Exhibit B of this License must be attached. + +Exhibit A - Source Code Form License Notice +------------------------------------------- + + This Source Code Form is subject to the terms of the Mozilla Public + License, v. 2.0. If a copy of the MPL was not distributed with this + file, You can obtain one at https://mozilla.org/MPL/2.0/. + +If it is not possible or desirable to put the notice in a particular +file, then You may include the notice in a location (such as a LICENSE +file in a relevant directory) where a recipient would be likely to look +for such a notice. + +You may add additional accurate notices of copyright ownership. + +Exhibit B - "Incompatible With Secondary Licenses" Notice +--------------------------------------------------------- + + This Source Code Form is "Incompatible With Secondary Licenses", as + defined by the Mozilla Public License, v. 2.0. diff --git a/aletheia/templates/common/MAINTAINERS.adoc b/aletheia/templates/common/MAINTAINERS.adoc new file mode 100644 index 0000000..7d3fa72 --- /dev/null +++ b/aletheia/templates/common/MAINTAINERS.adoc @@ -0,0 +1,29 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Maintainers + +== Current Maintainers + +* *@@AUTHOR_NAME@@* — Project Lead — @@AUTHOR_EMAIL@@ + +== Responsibilities + +Maintainers review pull requests, triage issues, cut releases, and uphold +the project's security and conduct policies. + +== Becoming a Maintainer + +Maintainers are invited based on sustained, constructive contribution. + +== Decision Making + +[cols="1,2"] +|=== +|Minor change |one maintainer approval +|Major change |consensus among maintainers +|Security fix |one maintainer approval, expedited +|=== + +== Contact + +Use the repository's issue tracker for project questions, and +@@SECURITY_CONTACT@@ for security matters. diff --git a/aletheia/templates/common/SECURITY.adoc b/aletheia/templates/common/SECURITY.adoc new file mode 100644 index 0000000..f346b3d --- /dev/null +++ b/aletheia/templates/common/SECURITY.adoc @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Security Policy +:toc: + +== Reporting a Vulnerability + +Report vulnerabilities privately to **@@SECURITY_CONTACT@@**. + +**Do not** open a public issue for a security vulnerability. + +== Response Timeline + +[cols="1,2"] +|=== +|Acknowledgment |within 48 hours +|Assessment |within 7 days +|Fix (critical) |within 30 days +|Fix (other) |within 90 days +|=== + +== Scope + +This policy covers the source code in this repository and the artefacts it +publishes. It does not cover third-party dependencies, which are governed +by their own policies. + +== Supported Versions + +The latest release on the default branch receives security fixes. + +== Machine-Readable Form + +An RFC 9116 `+security.txt+` is published at link:.well-known/security.txt[.well-known/security.txt]. diff --git a/aletheia/templates/elixir/.editorconfig b/aletheia/templates/elixir/.editorconfig new file mode 100644 index 0000000..7520e0f --- /dev/null +++ b/aletheia/templates/elixir/.editorconfig @@ -0,0 +1,19 @@ +# @@PROJECT_NAME@@ - Editor Configuration +# https://editorconfig.org + +root = true + +[*] +charset = utf-8 +end_of_line = lf +indent_size = 2 +indent_style = space +insert_final_newline = true +trim_trailing_whitespace = true + +[*.adoc] +trim_trailing_whitespace = false + +[Justfile] +indent_style = space +indent_size = 4 diff --git a/aletheia/templates/elixir/.formatter.exs b/aletheia/templates/elixir/.formatter.exs new file mode 100644 index 0000000..8769554 --- /dev/null +++ b/aletheia/templates/elixir/.formatter.exs @@ -0,0 +1,5 @@ +# SPDX-License-Identifier: MPL-2.0 +# Used by `mix format`. +[ + inputs: ["{mix,.formatter}.exs", "{config,lib,test}/**/*.{ex,exs}"] +] diff --git a/aletheia/templates/elixir/.github/workflows/ci.yml b/aletheia/templates/elixir/.github/workflows/ci.yml new file mode 100644 index 0000000..20e1465 --- /dev/null +++ b/aletheia/templates/elixir/.github/workflows/ci.yml @@ -0,0 +1,42 @@ +# SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. +name: CI + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +jobs: + check: + name: Build, test, lint (offline) + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Install Erlang and Elixir + uses: erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124 # v1 + with: + otp-version: '27.3' + elixir-version: '1.18.3' + + - name: Compile (no deps to fetch) + run: mix compile --warnings-as-errors + + - name: Test + run: mix test + + - name: Check formatting + run: mix format --check-formatted diff --git a/aletheia/templates/elixir/.gitignore b/aletheia/templates/elixir/.gitignore new file mode 100644 index 0000000..f9b9e3f --- /dev/null +++ b/aletheia/templates/elixir/.gitignore @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: MPL-2.0 +/_build/ +/cover/ +/deps/ +/doc/ +/.fetch +erl_crash.dump +*.ez +*.beam diff --git a/aletheia/templates/elixir/.machine_readable/rsr-profile.a2ml b/aletheia/templates/elixir/.machine_readable/rsr-profile.a2ml new file mode 100644 index 0000000..33b2fd5 --- /dev/null +++ b/aletheia/templates/elixir/.machine_readable/rsr-profile.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# RSR capability profile for @@PROJECT_NAME@@. Declares what this repo +# carries so the capability gates compute the applicable criterion set. +[profile] +capabilities = ["elixir", "cli", "docs"] + +[rationale] +elixir = "true: mix project, Elixir 1.18 / OTP 27" +cli = "true: lib//cli.ex exposes a main/1 entry point" +docs = "true: README + SECURITY + CONTRIBUTING + CODE_OF_CONDUCT + CHANGELOG" +no-library = "shared: the app is a library plus a CLI wrapper, not published to Hex" +no-container = "true: no Containerfile in the scaffold" diff --git a/aletheia/templates/elixir/.tool-versions b/aletheia/templates/elixir/.tool-versions new file mode 100644 index 0000000..40ad142 --- /dev/null +++ b/aletheia/templates/elixir/.tool-versions @@ -0,0 +1,3 @@ +# Toolchain pins, asdf/mise compatible. +erlang 27.3 +gelixir 1.18.3 diff --git a/aletheia/templates/elixir/Justfile b/aletheia/templates/elixir/Justfile new file mode 100644 index 0000000..a09faf1 --- /dev/null +++ b/aletheia/templates/elixir/Justfile @@ -0,0 +1,37 @@ +# SPDX-License-Identifier: MPL-2.0 +# Justfile — build automation for @@PROJECT_NAME@@. +# See: https://github.com/casey/just +# +# Every recipe here is offline: this project has no external dependencies, +# so nothing is fetched at build time. Recipes fail loudly — a recipe that +# echoes a message and exits 0 would be a fake gate (RSR v2 6.1.5, Gold). + +default: + @just --list + +# Compile the project, treating warnings as errors +build: + mix compile --warnings-as-errors + +# Run the program; pass arguments after the recipe name +run *ARGS: + mix run -e '@@MOD_CAMEL@@.CLI.main(System.argv())' -- {{ARGS}} + +# Run the test suite +test: + mix test + +# Check formatting (does not modify files) +fmt: + mix format --check-formatted + +# Apply formatting +fmt-fix: + mix format + +# Verify RSR compliance using the estate checker +verify: + aletheia . + +# Everything the CI gate runs, in the same order +check: build test fmt diff --git a/aletheia/templates/elixir/README.adoc b/aletheia/templates/elixir/README.adoc new file mode 100644 index 0000000..1e89576 --- /dev/null +++ b/aletheia/templates/elixir/README.adoc @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += @@PROJECT_NAME@@ +:toc: +:icons: font + +____ +@@PROJECT_DESCRIPTION@@ +____ + +== Quick Start + +[source,bash] +---- +# Build (offline — nothing is downloaded) +just build + +# Test +just test + +# Verify RSR compliance +just verify +---- + +This project is *standalone by construction*: the scaffold fetches nothing, +the build has no external dependencies, and the licence texts ship in-tree +under `+LICENSES/+`. + +== RSR Compliance + +[cols="1,3"] +|=== +|Bronze |Documentation, security policy, SPDX headers, CI, licence classification +|Silver |`.editorconfig`, `.tool-versions`, machine-readable manifests, SHA-pinned CI, `+LICENSES/+` +|Gold |No silent-skip recipes +|=== + +Verify with the estate's own checker: + +[source,bash] +---- +aletheia . +---- + +== Language: @@LANG_DISPLAY@@ + +@@LANG_POLICY@@ + +== Documentation + +* link:SECURITY.adoc[Security Policy] — vulnerability disclosure +* link:CONTRIBUTING.adoc[Contributing Guide] — how to contribute +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] — community standards +* link:MAINTAINERS.adoc[Maintainers] — ownership and decisions +* link:CHANGELOG.adoc[Changelog] — version history + +== Layout + +.... +. +├── Justfile # build automation (capital J — v2 shape) +├── LICENSE # licence statement +├── LICENSES/ # full licence texts (REUSE style) +├── src/ # source (layout follows the language's conventions) +├── .github/workflows/ # CI + estate gates +├── .machine_readable/ # machine-readable metadata +└── .well-known/ # security.txt, ai.txt, humans.txt +.... + +== Contributing + +See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc]. + +== License + +Code is licensed under the Mozilla Public License, version 2.0 +(`+MPL-2.0+`). Documentation is licensed under Creative Commons +Attribution-ShareAlike 4.0 International (`+CC-BY-SA-4.0+`). + +See link:LICENSE[LICENSE] and the `+LICENSES/+` directory for full texts. + +''''' + +_Created from the aletheia v2 Bronze template._ diff --git a/aletheia/templates/elixir/lib/@@MOD_NAME@@.ex b/aletheia/templates/elixir/lib/@@MOD_NAME@@.ex new file mode 100644 index 0000000..62a12ce --- /dev/null +++ b/aletheia/templates/elixir/lib/@@MOD_NAME@@.ex @@ -0,0 +1,47 @@ +# SPDX-License-Identifier: MPL-2.0 +defmodule @@MOD_CAMEL@@ do + @moduledoc """ + Core library for @@PROJECT_NAME@@. + + Replace these sample functions with your own. + """ + + @doc """ + Clamp `value` into the inclusive range `lo..hi`. + + Raises if `lo > hi`, because an inverted range is a programming error + rather than a silent no-op. + + ## Examples + + iex> @@MOD_CAMEL@@.clamp(5, 0, 10) + 5 + iex> @@MOD_CAMEL@@.clamp(99, 0, 10) + 10 + """ + @spec clamp(non_neg_integer(), non_neg_integer(), non_neg_integer()) :: non_neg_integer() + def clamp(value, lo, hi) when lo <= hi do + value |> max(lo) |> min(hi) + end + + @doc """ + Integer mean of two non-negative integers, rounded towards zero. + + The naive `div(a + b, 2)` is fine on the BEAM, where integers are + arbitrary precision; this form is kept because it is explicit about + intent and mirrors the other templates in this estate. + + ## Examples + + iex> @@MOD_CAMEL@@.mean_floor(8, 11) + 9 + """ + @spec mean_floor(non_neg_integer(), non_neg_integer()) :: non_neg_integer() + def mean_floor(a, b) do + Bitwise.band(a, b) + Bitwise.bsr(Bitwise.bxor(a, b), 1) + end + + @doc "Returns the project version." + @spec version() :: String.t() + def version, do: "0.1.0" +end diff --git a/aletheia/templates/elixir/lib/@@MOD_NAME@@/cli.ex b/aletheia/templates/elixir/lib/@@MOD_NAME@@/cli.ex new file mode 100644 index 0000000..e3864d5 --- /dev/null +++ b/aletheia/templates/elixir/lib/@@MOD_NAME@@/cli.ex @@ -0,0 +1,62 @@ +# SPDX-License-Identifier: MPL-2.0 +defmodule @@MOD_CAMEL@@.CLI do + @moduledoc """ + Command-line entry point for @@PROJECT_NAME@@. + """ + + @usage """ + @@PROJECT_NAME@@ 0.1.0 + + usage: + @@PROJECT_NAME@@ clamp clamp a value into a range + @@PROJECT_NAME@@ mean integer mean, rounded down + @@PROJECT_NAME@@ --help show this message + """ + + @doc """ + Runs the CLI with the given argument list. + + Returns an exit status. The Justfile's `run` recipe wires this up via + `mix run -e '@@MOD_CAMEL@@.CLI.main(System.argv())'`, which exits with + the status this returns. + """ + @spec main([String.t()]) :: non_neg_integer() + def main([]) do + IO.puts(@usage) + 0 + end + + def main([flag]) when flag in ["--help", "-h"] do + IO.puts(@usage) + 0 + end + + def main(["clamp", value, lo, hi]) do + with {value, ""} <- Integer.parse(value), + {lo, ""} <- Integer.parse(lo), + {hi, ""} <- Integer.parse(hi), + true <- lo <= hi do + IO.puts(@@MOD_CAMEL@@.clamp(value, lo, hi)) + 0 + else + _ -> fail() + end + end + + def main(["mean", a, b]) do + with {a, ""} <- Integer.parse(a), + {b, ""} <- Integer.parse(b) do + IO.puts(@@MOD_CAMEL@@.mean_floor(a, b)) + 0 + else + _ -> fail() + end + end + + def main(_), do: fail() + + defp fail do + IO.puts(:stderr, "error: unrecognised arguments\n\n#{@usage}") + 1 + end +end diff --git a/aletheia/templates/elixir/mix.exs b/aletheia/templates/elixir/mix.exs new file mode 100644 index 0000000..c226942 --- /dev/null +++ b/aletheia/templates/elixir/mix.exs @@ -0,0 +1,21 @@ +# SPDX-License-Identifier: MPL-2.0 +defmodule @@MOD_CAMEL@@.MixProject do + use Mix.Project + + def project do + [ + app: :@@MOD_NAME@@, + version: "0.1.0", + elixir: "~> 1.18", + start_permanent: Mix.env() == :prod, + # EMPTY BY DESIGN: no Hex dependencies, so nothing is fetched at + # build time and `mix compile` works with no network access. + # See 0-AI-MANIFEST.a2ml, invariant 2. + deps: [] + ] + end + + def application do + [extra_applications: [:logger]] + end +end diff --git a/aletheia/templates/elixir/test/@@MOD_NAME@@_test.exs b/aletheia/templates/elixir/test/@@MOD_NAME@@_test.exs new file mode 100644 index 0000000..469dd07 --- /dev/null +++ b/aletheia/templates/elixir/test/@@MOD_NAME@@_test.exs @@ -0,0 +1,45 @@ +# SPDX-License-Identifier: MPL-2.0 +defmodule @@MOD_CAMEL@@Test do + use ExUnit.Case, async: true + + doctest @@MOD_CAMEL@@ + + describe "clamp/3" do + test "keeps a value already inside the range" do + assert @@MOD_CAMEL@@.clamp(5, 0, 10) == 5 + end + + test "lifts a value below the range to the lower bound" do + assert @@MOD_CAMEL@@.clamp(0, 1, 10) == 1 + end + + test "drops a value above the range to the upper bound" do + assert @@MOD_CAMEL@@.clamp(99, 0, 10) == 10 + end + + test "handles a degenerate range" do + assert @@MOD_CAMEL@@.clamp(7, 7, 7) == 7 + end + + test "is idempotent" do + for value <- [0, 1, 5, 42, 10_000] do + once = @@MOD_CAMEL@@.clamp(value, 10, 100) + assert @@MOD_CAMEL@@.clamp(once, 10, 100) == once + end + end + end + + describe "mean_floor/2" do + test "matches the naive form on small inputs" do + for a <- 0..63, b <- 0..63 do + assert @@MOD_CAMEL@@.mean_floor(a, b) == div(a + b, 2) + end + end + + test "never exceeds either input" do + for {a, b} <- [{0, 0}, {1, 2}, {7, 9}, {10_000, 0}] do + assert @@MOD_CAMEL@@.mean_floor(a, b) <= max(a, b) + end + end + end +end diff --git a/aletheia/templates/elixir/test/test_helper.exs b/aletheia/templates/elixir/test/test_helper.exs new file mode 100644 index 0000000..5a57034 --- /dev/null +++ b/aletheia/templates/elixir/test/test_helper.exs @@ -0,0 +1,2 @@ +# SPDX-License-Identifier: MPL-2.0 +ExUnit.start() diff --git a/aletheia/templates/haskell/.editorconfig b/aletheia/templates/haskell/.editorconfig new file mode 100644 index 0000000..7520e0f --- /dev/null +++ b/aletheia/templates/haskell/.editorconfig @@ -0,0 +1,19 @@ +# @@PROJECT_NAME@@ - Editor Configuration +# https://editorconfig.org + +root = true + +[*] +charset = utf-8 +end_of_line = lf +indent_size = 2 +indent_style = space +insert_final_newline = true +trim_trailing_whitespace = true + +[*.adoc] +trim_trailing_whitespace = false + +[Justfile] +indent_style = space +indent_size = 4 diff --git a/aletheia/templates/haskell/.github/workflows/ci.yml b/aletheia/templates/haskell/.github/workflows/ci.yml new file mode 100644 index 0000000..7a2d2e0 --- /dev/null +++ b/aletheia/templates/haskell/.github/workflows/ci.yml @@ -0,0 +1,39 @@ +# SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. +name: CI + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +jobs: + check: + name: Build, test, lint (offline) + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Install GHC and Cabal + uses: haskell-actions/setup@0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d # v2 + with: + ghc-version: '9.6.6' + cabal-version: '3.10.3.0' + + - name: Build (offline, base only) + run: cabal build --offline + + - name: Test + run: cabal test --offline --test-show-details=direct diff --git a/aletheia/templates/haskell/.gitignore b/aletheia/templates/haskell/.gitignore new file mode 100644 index 0000000..b4a1619 --- /dev/null +++ b/aletheia/templates/haskell/.gitignore @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +/dist-newstyle/ +dist-newstyle/ +*.hi +*.o +*.hie +.ghc.environment.* diff --git a/aletheia/templates/haskell/.machine_readable/rsr-profile.a2ml b/aletheia/templates/haskell/.machine_readable/rsr-profile.a2ml new file mode 100644 index 0000000..15107b4 --- /dev/null +++ b/aletheia/templates/haskell/.machine_readable/rsr-profile.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# RSR capability profile for @@PROJECT_NAME@@. Declares what this repo +# carries so the capability gates compute the applicable criterion set. +[profile] +capabilities = ["haskell", "cli", "docs"] + +[rationale] +haskell = "true: cabal package, GHC 9.6.6" +cli = "true: app/Main.hs produces an executable" +docs = "true: README + SECURITY + CONTRIBUTING + CODE_OF_CONDUCT + CHANGELOG" +no-library = "shared: src/ is a library component of the same package, not published to Hackage" +no-container = "true: no Containerfile in the scaffold" diff --git a/aletheia/templates/haskell/.tool-versions b/aletheia/templates/haskell/.tool-versions new file mode 100644 index 0000000..66b7d5d --- /dev/null +++ b/aletheia/templates/haskell/.tool-versions @@ -0,0 +1,3 @@ +# Toolchain pins, asdf/mise compatible. +ghc 9.6.6 +cabal 3.10.3.0 diff --git a/aletheia/templates/haskell/@@PROJECT_NAME@@.cabal b/aletheia/templates/haskell/@@PROJECT_NAME@@.cabal new file mode 100644 index 0000000..15bafdc --- /dev/null +++ b/aletheia/templates/haskell/@@PROJECT_NAME@@.cabal @@ -0,0 +1,44 @@ +cabal-version: 2.4 +-- SPDX-License-Identifier: MPL-2.0 +name: @@PROJECT_NAME@@ +version: 0.1.0 +synopsis: @@PROJECT_DESCRIPTION@@ +license: MPL-2.0 +license-file: LICENSE +build-type: Simple + +-- Zero external dependencies: only `base`, which ships with GHC. That is +-- what lets `cabal build --offline` resolve with no package index and no +-- network. See 0-AI-MANIFEST.a2ml, invariant 2. + +common warnings + ghc-options: -Wall + -Wcompat + -Widentities + -Wincomplete-record-updates + -Wincomplete-uni-patterns + -Wredundant-constraints + +library + import: warnings + exposed-modules: Core + hs-source-dirs: src + build-depends: base >=4.14 && <5 + default-language: Haskell2010 + +executable @@PROJECT_NAME@@ + import: warnings + main-is: Main.hs + hs-source-dirs: app + build-depends: base, + @@PROJECT_NAME@@ + default-language: Haskell2010 + +test-suite @@PROJECT_NAME@@-test + import: warnings + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + build-depends: base, + @@PROJECT_NAME@@ + default-language: Haskell2010 diff --git a/aletheia/templates/haskell/Justfile b/aletheia/templates/haskell/Justfile new file mode 100644 index 0000000..adcc632 --- /dev/null +++ b/aletheia/templates/haskell/Justfile @@ -0,0 +1,35 @@ +# SPDX-License-Identifier: MPL-2.0 +# Justfile — build automation for @@PROJECT_NAME@@. +# See: https://github.com/casey/just +# +# Every recipe here is offline: this project has no external dependencies, +# so nothing is fetched at build time. Recipes fail loudly — a recipe that +# echoes a message and exits 0 would be a fake gate (RSR v2 6.1.5, Gold). + +default: + @just --list + +# Build the package (offline: only `base` from GHC is needed) +build: + cabal build --offline + +# Run the program; pass arguments after the recipe name +run *ARGS: + cabal run --offline @@PROJECT_NAME@@ -- {{ARGS}} + +# Run the test suite +test: + cabal test --offline --test-show-details=direct + +# Build with all warnings enabled and promoted to errors. This is the +# static-analysis gate for this language: GHC's own warning set, no extra +# tooling to install. +lint: + cabal build --offline --ghc-options="-Wall -Wcompat -Werror" + +# Verify RSR compliance using the estate checker +verify: + aletheia . + +# Everything the CI gate runs, in the same order +check: build test diff --git a/aletheia/templates/haskell/README.adoc b/aletheia/templates/haskell/README.adoc new file mode 100644 index 0000000..1e89576 --- /dev/null +++ b/aletheia/templates/haskell/README.adoc @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += @@PROJECT_NAME@@ +:toc: +:icons: font + +____ +@@PROJECT_DESCRIPTION@@ +____ + +== Quick Start + +[source,bash] +---- +# Build (offline — nothing is downloaded) +just build + +# Test +just test + +# Verify RSR compliance +just verify +---- + +This project is *standalone by construction*: the scaffold fetches nothing, +the build has no external dependencies, and the licence texts ship in-tree +under `+LICENSES/+`. + +== RSR Compliance + +[cols="1,3"] +|=== +|Bronze |Documentation, security policy, SPDX headers, CI, licence classification +|Silver |`.editorconfig`, `.tool-versions`, machine-readable manifests, SHA-pinned CI, `+LICENSES/+` +|Gold |No silent-skip recipes +|=== + +Verify with the estate's own checker: + +[source,bash] +---- +aletheia . +---- + +== Language: @@LANG_DISPLAY@@ + +@@LANG_POLICY@@ + +== Documentation + +* link:SECURITY.adoc[Security Policy] — vulnerability disclosure +* link:CONTRIBUTING.adoc[Contributing Guide] — how to contribute +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] — community standards +* link:MAINTAINERS.adoc[Maintainers] — ownership and decisions +* link:CHANGELOG.adoc[Changelog] — version history + +== Layout + +.... +. +├── Justfile # build automation (capital J — v2 shape) +├── LICENSE # licence statement +├── LICENSES/ # full licence texts (REUSE style) +├── src/ # source (layout follows the language's conventions) +├── .github/workflows/ # CI + estate gates +├── .machine_readable/ # machine-readable metadata +└── .well-known/ # security.txt, ai.txt, humans.txt +.... + +== Contributing + +See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc]. + +== License + +Code is licensed under the Mozilla Public License, version 2.0 +(`+MPL-2.0+`). Documentation is licensed under Creative Commons +Attribution-ShareAlike 4.0 International (`+CC-BY-SA-4.0+`). + +See link:LICENSE[LICENSE] and the `+LICENSES/+` directory for full texts. + +''''' + +_Created from the aletheia v2 Bronze template._ diff --git a/aletheia/templates/haskell/app/Main.hs b/aletheia/templates/haskell/app/Main.hs new file mode 100644 index 0000000..86c375d --- /dev/null +++ b/aletheia/templates/haskell/app/Main.hs @@ -0,0 +1,51 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- | @@PROJECT_NAME@@ — command-line entry point. +module Main (main) where + +import Core (clamp, meanFloor) +import System.IO (hPutStrLn, stderr) +import System.Environment (getArgs) +import System.Exit (exitFailure, exitSuccess) +import Text.Read (readMaybe) + +usage :: String +usage = + unlines + [ "@@PROJECT_NAME@@ 0.1.0" + , "" + , "usage:" + , " @@PROJECT_NAME@@ clamp clamp a value into a range" + , " @@PROJECT_NAME@@ mean integer mean, rounded down" + , " @@PROJECT_NAME@@ --help show this message" + , "" + , "All arguments are non-negative integers." + ] + +parseWord :: String -> Maybe Word +parseWord raw = case readMaybe raw of + Just n | n >= 0 -> Just n + _ -> Nothing + +main :: IO () +main = do + args <- getArgs + case args of + [] -> putStr usage >> exitSuccess + ["--help"] -> putStr usage >> exitSuccess + ["-h"] -> putStr usage >> exitSuccess + ["clamp", value, lo, hi] -> + case (parseWord value, parseWord lo, parseWord hi) of + (Just v, Just l, Just h) | l <= h -> print (clamp v l h) >> exitSuccess + _ -> unrecognised + ["mean", a, b] -> + case (parseWord a, parseWord b) of + (Just x, Just y) -> print (meanFloor x y) >> exitSuccess + _ -> unrecognised + _ -> unrecognised + +unrecognised :: IO a +unrecognised = do + hPutStrLn stderr "error: unrecognised arguments" + hPutStrLn stderr "" + hPutStrLn stderr usage + exitFailure diff --git a/aletheia/templates/haskell/cabal.project b/aletheia/templates/haskell/cabal.project new file mode 100644 index 0000000..f63a681 --- /dev/null +++ b/aletheia/templates/haskell/cabal.project @@ -0,0 +1,2 @@ +-- SPDX-License-Identifier: MPL-2.0 +packages: . diff --git a/aletheia/templates/haskell/src/Core.hs b/aletheia/templates/haskell/src/Core.hs new file mode 100644 index 0000000..d339dc2 --- /dev/null +++ b/aletheia/templates/haskell/src/Core.hs @@ -0,0 +1,24 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- | Core library for @@PROJECT_NAME@@. +-- +-- Replace these sample functions with your own. +module Core + ( clamp + , meanFloor + ) where + +import Data.Bits (shiftR, xor, (.&.)) + +-- | Clamp @value@ into the inclusive range @[lo, hi]@. +-- +-- If @lo > hi@ the range is empty; the upper bound wins, so the result is +-- @hi@. Callers that care should check their range first. +clamp :: Ord a => a -> a -> a -> a +clamp value lo hi = min hi (max lo value) + +-- | Integer mean of two 'Word's, rounded towards zero. +-- +-- The naive @(a + b) \`div\` 2@ overflows for large inputs; this form +-- cannot, because it never materialises the sum. +meanFloor :: Word -> Word -> Word +meanFloor a b = (a .&. b) + ((a `xor` b) `shiftR` 1) diff --git a/aletheia/templates/haskell/test/Main.hs b/aletheia/templates/haskell/test/Main.hs new file mode 100644 index 0000000..c49d7a6 --- /dev/null +++ b/aletheia/templates/haskell/test/Main.hs @@ -0,0 +1,45 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- | Test suite for @@PROJECT_NAME@@. +-- +-- Deliberately dependency-free: a plain exitcode-stdio runner rather than +-- a framework, so the package still needs only `base`. +module Main (main) where + +import Control.Monad (forM_, unless) +import Core (clamp, meanFloor) +import Data.IORef (modifyIORef', newIORef, readIORef) +import System.Exit (exitFailure, exitSuccess) + +main :: IO () +main = do + failures <- newIORef (0 :: Int) + let check label condition = + unless condition $ do + putStrLn ("FAIL: " ++ label) + modifyIORef' failures (+ 1) + + -- clamp: values inside, below and above the range + check "clamp keeps an in-range value" (clamp (5 :: Int) 0 10 == 5) + check "clamp lifts a low value" (clamp (0 :: Int) 1 10 == 1) + check "clamp drops a high value" (clamp (99 :: Int) 0 10 == 10) + check "clamp handles a degenerate range" (clamp (7 :: Int) 7 7 == 7) + + -- clamp: idempotent and always in range + forM_ [0, 1, 5, 42, 10000 :: Int] $ \value -> do + let once = clamp value 10 100 + check "clamp is idempotent" (clamp once 10 100 == once) + check "clamp result is in range" (once >= 10 && once <= 100) + + -- meanFloor: agrees with the naive form where the naive form is safe + forM_ [0 .. 63 :: Word] $ \a -> + forM_ [0 .. 63 :: Word] $ \b -> + check "meanFloor matches naive" (meanFloor a b == (a + b) `div` 2) + + -- meanFloor: never exceeds either input, and cannot overflow + forM_ [(0, 0), (1, 2), (7, 9), (maxBound, 0), (maxBound, maxBound)] $ + \(a, b) -> check "meanFloor bounded" (meanFloor a b <= max a b) + + total <- readIORef failures + if total == 0 + then putStrLn "All tests passed." >> exitSuccess + else putStrLn (show total ++ " test(s) failed.") >> exitFailure diff --git a/aletheia/templates/rust/.editorconfig b/aletheia/templates/rust/.editorconfig new file mode 100644 index 0000000..32de1c9 --- /dev/null +++ b/aletheia/templates/rust/.editorconfig @@ -0,0 +1,22 @@ +# @@PROJECT_NAME@@ - Editor Configuration +# https://editorconfig.org + +root = true + +[*] +charset = utf-8 +end_of_line = lf +indent_size = 2 +indent_style = space +insert_final_newline = true +trim_trailing_whitespace = true + +[*.adoc] +trim_trailing_whitespace = false + +[*.rs] +indent_size = 4 + +[Justfile] +indent_style = space +indent_size = 4 diff --git a/aletheia/templates/rust/.github/workflows/ci.yml b/aletheia/templates/rust/.github/workflows/ci.yml new file mode 100644 index 0000000..e1f26e6 --- /dev/null +++ b/aletheia/templates/rust/.github/workflows/ci.yml @@ -0,0 +1,51 @@ +# SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. +name: CI + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +jobs: + check: + name: Build, test, lint (offline) + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Ensure clippy and rustfmt are present + run: rustup component add clippy rustfmt + + - name: Build (offline, zero dependencies) + run: cargo build --offline + + - name: Test + run: cargo test --offline + + - name: Check formatting + run: cargo fmt --check + + - name: Lint (warnings denied) + run: cargo clippy --offline --all-targets -- -D warnings + + - name: Enforce zero dependencies + run: | + if cargo tree --offline --depth 1 | tail -n +2 | grep -q '[a-z]'; then + echo "ERROR: dependencies detected — this crate must stay zero-dependency." + cargo tree --offline --depth 1 + exit 1 + fi + echo "OK: zero dependencies" diff --git a/aletheia/templates/rust/.github/workflows/proof.yml b/aletheia/templates/rust/.github/workflows/proof.yml new file mode 100644 index 0000000..b02e49d --- /dev/null +++ b/aletheia/templates/rust/.github/workflows/proof.yml @@ -0,0 +1,184 @@ +# SPDX-License-Identifier: MPL-2.0 +# Creusot proof gate. Separate from ci.yml on purpose: the offline Bronze job +# must stay fast and dependency-free, while proving needs a pinned nightly +# plus Creusot's forks of Why3 and why3find. +# +# This is a real gate — `cargo creusot` exits non-zero when any obligation is +# unproved. It is deliberately *not* part of `just check`. +# +# It has not yet run on a GitHub runner: treat the first green run as the +# moment it becomes load-bearing. It is not blind, though — every step below +# was executed by hand against a from-scratch toolchain, and three defects it +# used to have (a bad rust-toolchain parse, a stale hard-coded Why3 pin, and a +# setup that could never find creusot-rustc) were found that way. +name: Proof (Creusot) + +on: + push: + branches: [main, master] + paths: + - 'src/**' + - 'verification/**' + - 'Cargo.toml' + - 'Justfile' + - '.github/workflows/proof.yml' + pull_request: + branches: [main, master] + paths: + - 'src/**' + - 'verification/**' + - 'Cargo.toml' + - 'Justfile' + - '.github/workflows/proof.yml' + workflow_dispatch: + +concurrency: + group: proof-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +env: + # Pinned rather than tracking master. A proof gate that changes its toolchain + # underneath a passing build is not a gate; bump this deliberately, with a + # proof run to go with it. The Why3/why3find forks are *derived* from this + # revision's creusot-deps.opam below — hard-coding them here is how the + # previous version of this file went stale. + CREUSOT_REV: de6f4acdaeabf8d81784676f848f99c0c1db1851 + +jobs: + creusot: + name: Translate and discharge (Creusot + Why3) + runs-on: ubuntu-24.04 + timeout-minutes: 120 + steps: + # Pinned to a full SHA rather than relying on actions.lock: only two of + # the six templates ship this opt-in workflow, and a lock entry for a + # file the other four do not have would be noise in a shared file. + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + + # No z3/cvc5 here: the `provers` installer component fetches the exact + # versions Creusot's why3.conf names in its drivers (alt-ergo 2.6.2, + # z3 4.15.3, cvc4 1.8, cvc5 1.3.1). An apt z3 is a different version + # behind the same driver name, which is a silent way to get different + # results from the same proof. + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends \ + opam ocaml build-essential pkg-config libgmp-dev zlib1g-dev autoconf curl + + - name: Clone Creusot at the pinned revision + run: | + set -euo pipefail + mkdir -p "$RUNNER_TEMP/creusot" + cd "$RUNNER_TEMP/creusot" + git init -q + git remote add origin https://github.com/creusot-rs/creusot + git fetch -q --depth 1 origin "$CREUSOT_REV" + git checkout -q FETCH_HEAD + echo "creusot at $(git rev-parse HEAD)" + + # Creusot pins its own nightly; read it from the clone rather than + # duplicating a second copy that can drift. + - name: Install the pinned Rust toolchain + run: | + set -euo pipefail + # Creusot pins the channel in a `rust-toolchain` file: TOML, but + # without the .toml extension. The obvious `head -1` yields + # "[toolchain]" and installs the wrong toolchain entirely. + channel=$(sed -n 's/^[[:space:]]*channel[[:space:]]*=[[:space:]]*"\(.*\)"/\1/p' \ + "$RUNNER_TEMP/creusot/rust-toolchain") + if [ -z "$channel" ]; then + echo "::error::could not read the channel from creusot's rust-toolchain file" + exit 1 + fi + echo "Creusot pins $channel" + rustup toolchain install "$channel" --component rustc-dev,llvm-tools + rustup default "$channel" + + - name: Install Why3 and why3find (Creusot's forks) + run: | + set -euo pipefail + cd "$RUNNER_TEMP/creusot" + # Derive the forks from the revision we checked out. A stock Why3 + # cannot parse the Coma a given Creusot emits, and a stock why3find + # does not compile against the pinned Why3. + WHY3_PIN=$(grep -oE 'git\+https://gitlab\.inria\.fr/why3/why3\.git#[0-9a-f]{40}' creusot-deps.opam | head -1) + WHY3FIND_PIN=$(grep -oE 'git\+https://github\.com/creusot-rs/why3find\.git#[0-9a-f]{40}' creusot-deps.opam | head -1) + if [ -z "$WHY3_PIN" ] || [ -z "$WHY3FIND_PIN" ]; then + echo "::error::could not read the why3/why3find pins from creusot-deps.opam" + exit 1 + fi + echo "why3 -> $WHY3_PIN" + echo "why3find -> $WHY3FIND_PIN" + opam init --bare --disable-sandboxing -y + opam switch create creusot ocaml-system -y + eval "$(opam env --switch=creusot --set-switch)" + opam pin add -y why3 "$WHY3_PIN" + opam install -y why3 + opam pin add -y why3find "$WHY3FIND_PIN" + opam install -y why3find + why3 --version + why3find --version + opam env --switch=creusot --set-switch >> "$GITHUB_ENV" + + # `cargo creusot` does not look for its tools on PATH. It resolves them + # inside its own data dir ($XDG_DATA_HOME/creusot): + # bin/why3, bin/why3find, bin/ (why3_launcher.rs puts bin first on PATH) + # toolchains//bin/creusot-rustc + # share/why3find/packages/creusot (the prelude) + # Installing the two binaries by hand and stopping there is not enough: + # proving then dies with "creusot-rustc not found (expected at ...)". + # This one call lays out the prelude, the why3 config, the four provers, + # the toolchain-local creusot-rustc, and the cargo config patch for the + # creusot-std path dependency. + - name: Install Creusot (prelude, provers, toolchain, cargo config) + working-directory: ${{ runner.temp }}/creusot + run: | + set -euo pipefail + eval "$(opam env --switch=creusot --set-switch)" + cargo run --quiet --release --bin creusot-install -- \ + prelude why3-conf provers creusot-rustc cargo-creusot cargo-creusot-config + + # The installer also has a `why3` component that provides these two, but + # it builds a second opam switch from creusot-deps.opam inside the data + # dir, which drags in the GTK-based why3 IDE. The component's last act is + # to symlink these two binaries into the data dir (see + # creusot-install/src/main.rs), so do the same from the switch we already + # have — same end state, no GTK, no second switch. + - name: Provide why3 and why3find in the Creusot data dir + run: | + set -euo pipefail + eval "$(opam env --switch=creusot --set-switch)" + data_dir="$HOME/.local/share/creusot" + mkdir -p "$data_dir/bin" + ln -sf "$(command -v why3)" "$data_dir/bin/why3" + ln -sf "$(command -v why3find)" "$data_dir/bin/why3find" + ls -l "$data_dir/bin" + + # Checks what cargo-creusot actually resolves at runtime, instead of + # assuming the install worked. A "not found" prover here means the proof + # step would fail confusingly several minutes later. + - name: Check the Creusot install + run: | + set -euo pipefail + eval "$(opam env --switch=creusot --set-switch)" + cargo creusot version + if cargo creusot version | grep -qi 'not found'; then + echo "::error::cargo creusot cannot resolve its tools" + exit 1 + fi + + # Fails the job if any goal is unproved. Mirrors `just proof`, which is + # exactly this one command in verification/. + - name: Prove + working-directory: verification + run: cargo creusot + + - name: Proof artefacts + if: always() + run: find verification/verif -name '*.coma' -o -name 'proof.json' 2>/dev/null | head -50 || true diff --git a/aletheia/templates/rust/.gitignore b/aletheia/templates/rust/.gitignore new file mode 100644 index 0000000..469d74f --- /dev/null +++ b/aletheia/templates/rust/.gitignore @@ -0,0 +1,23 @@ +# SPDX-License-Identifier: MPL-2.0 +# Build artefacts +/target/ +**/target/ +Cargo.lock + +# Creusot/Why3 proof artefacts +*.coma +*.mlcfg +verification/verif/ +verification/target/ +.why3find/ + +# Editors and OS +.DS_Store +.idea/ +.vscode/ +*.swp +*~ + +# Local environment +.env +.env.local diff --git a/aletheia/templates/rust/.machine_readable/rsr-profile.a2ml b/aletheia/templates/rust/.machine_readable/rsr-profile.a2ml new file mode 100644 index 0000000..60c1323 --- /dev/null +++ b/aletheia/templates/rust/.machine_readable/rsr-profile.a2ml @@ -0,0 +1,16 @@ +# SPDX-License-Identifier: MPL-2.0 +# RSR capability profile for @@PROJECT_NAME@@. Declares what this repo +# carries so the capability gates compute the applicable criterion set. +[profile] +capabilities = ["rust", "cli", "docs"] + +[rationale] +rust = "true: a Rust 2021 crate (MSRV 1.80) with zero dependencies" +cli = "true: src/main.rs produces a binary" +docs = "true: README.adoc + SECURITY.adoc + CONTRIBUTING.adoc + CODE_OF_CONDUCT.adoc + CHANGELOG.adoc" +no-library = "DECLINED unless a lib target is added; src/lib.rs currently backs the binary's tests" +no-bash = "true: no tracked *.sh; all automation is in the Justfile" +no-container = "true: no Containerfile in the scaffold" +no-reproducible-build = "true: no guix.scm; the zero-dependency crate is offline-buildable via `cargo build --offline`" +no-formal-proofs = "PARTIAL: verification/ carries Creusot proof obligations, but they are not wired into CI until the Creusot toolchain is pinned (see verification/README.adoc)" +no-docs-site = "true: no pages workflow" diff --git a/aletheia/templates/rust/.tool-versions b/aletheia/templates/rust/.tool-versions new file mode 100644 index 0000000..a87d31a --- /dev/null +++ b/aletheia/templates/rust/.tool-versions @@ -0,0 +1,5 @@ +# Toolchain pins, asdf/mise compatible. +# The main crate builds on stable with zero dependencies; verification/ +# additionally needs the Creusot toolchain (nightly Rust + Why3), which is +# pinned separately in verification/README.adoc. +rust 1.98.1 diff --git a/aletheia/templates/rust/Cargo.toml b/aletheia/templates/rust/Cargo.toml new file mode 100644 index 0000000..6648724 --- /dev/null +++ b/aletheia/templates/rust/Cargo.toml @@ -0,0 +1,32 @@ +[package] +name = "@@PROJECT_NAME@@" +version = "0.1.0" +edition = "2021" +rust-version = "1.80" +license = "MPL-2.0" +description = "@@PROJECT_DESCRIPTION@@" +repository = "@@REPO_URL@@" + +# ZERO DEPENDENCIES — keeps this crate buildable with no network at all +# (`cargo build --offline`) and RSR-Bronze compliant. Adding a dependency +# breaks both. See 0-AI-MANIFEST.a2ml, invariant 3. +[dependencies] + +# `src/impl.rs` gates its Creusot specifications behind `#[cfg(creusot)]`. +# Telling rustc that `creusot` is a known cfg keeps the unexpected_cfgs lint +# quiet without weakening it for genuinely misspelled cfgs. +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(creusot)"] } + +[workspace] +# The Creusot proof crate is deliberately detached from this workspace: it +# needs `creusot-std` plus the Creusot/Why3 toolchain, which the main crate +# must never require. Excluding it here keeps `cargo build` zero-dependency +# and air-gapped. See verification/README.adoc. +exclude = ["verification"] + +[profile.release] +opt-level = 3 +lto = true +codegen-units = 1 +strip = true diff --git a/aletheia/templates/rust/Justfile b/aletheia/templates/rust/Justfile new file mode 100644 index 0000000..c77b416 --- /dev/null +++ b/aletheia/templates/rust/Justfile @@ -0,0 +1,69 @@ +# SPDX-License-Identifier: MPL-2.0 +# Justfile — build automation for @@PROJECT_NAME@@. +# See: https://github.com/casey/just +# +# Every recipe here is offline: the crate has zero dependencies, so +# `--offline` always succeeds. Recipes fail loudly — a recipe that echoes a +# message and exits 0 would be a fake gate (RSR v2 6.1.5, Gold). + +default: + @just --list + +# Build the crate (debug) +build: + cargo build --offline + +# Build the crate in release mode +build-release: + cargo build --offline --release + +# Run the binary; pass arguments after the recipe name +run *ARGS: + cargo run --offline --quiet -- {{ARGS}} + +# Run the full test suite (unit + integration) +test: + cargo test --offline + +# Check formatting without modifying files +fmt: + cargo fmt --check + +# Apply formatting +fmt-fix: + cargo fmt + +# Lint with warnings denied +lint: + cargo clippy --offline --all-targets -- -D warnings + +# Enforce the zero-dependency guarantee (RSR Bronze, air-gapped build) +deps-check: + #!/usr/bin/env bash + set -euo pipefail + if cargo tree --offline --depth 1 | tail -n +2 | grep -q '[a-z]'; then + echo "ERROR: dependencies detected — this crate must stay zero-dependency." + cargo tree --offline --depth 1 + exit 1 + fi + echo "OK: zero dependencies" + +# Verify RSR compliance using the estate checker +verify: + aletheia . + +# --- Rust/Creusot deductive verification (opt-in) --------------------- +# These recipes need the Creusot toolchain (nightly Rust + Why3 + SMT +# solvers). The default build never needs it — see verification/README.adoc. + +# Translate the annotated source to Coma and discharge every obligation +# with Why3. Fails loudly on any unproved goal — this is a real gate. +proof: + cd verification && cargo creusot + +# Remove generated Creusot/Why3 artefacts +proof-clean: + cd verification && cargo creusot clean + +# Everything the CI gate runs, in the same order +check: build test fmt lint deps-check diff --git a/aletheia/templates/rust/README.adoc b/aletheia/templates/rust/README.adoc new file mode 100644 index 0000000..4fdd4e8 --- /dev/null +++ b/aletheia/templates/rust/README.adoc @@ -0,0 +1,112 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += @@PROJECT_NAME@@ +:toc: +:icons: font + +____ +@@PROJECT_DESCRIPTION@@ +____ + +== Quick Start + +[source,bash] +---- +# Build (offline, zero dependencies) +just build + +# Test +just test + +# Verify RSR compliance +just verify +---- + +This project is *standalone by construction*: the scaffold fetches nothing. +`cargo build --offline` works on a machine with no network, because the +crate has zero dependencies and the licence texts ship in-tree under +`+LICENSES/+`. + +== RSR Compliance + +[cols="1,3"] +|=== +|Bronze |Documentation, security policy, SPDX headers, CI, licence classification +|Silver |`.editorconfig`, `.tool-versions`, machine-readable manifests, SHA-pinned CI, `+LICENSES/+` +|Gold |No silent-skip recipes +|=== + +Verify with the estate's own checker: + +[source,bash] +---- +aletheia . +---- + +== Language: Rust/Creusot + +Per the estate language policy, Rust in this estate is always *Rust/Creusot* +— Rust plus https://github.com/creusot-rs/creusot[Creusot], the deductive +verifier that translates annotated Rust to Why3 and discharges proof +obligations with SMT solvers. + +The verification crate lives in `+verification/+` and is *deliberately +detached from the default Cargo workspace*, so the main crate stays +zero-dependency and air-gapped. Only `just proof` needs the Creusot +toolchain (nightly Rust + Why3 + SMT solvers), and only when you actually +run it. + +`+src/impl.rs+` is a single source of truth: both `+src/lib.rs+` and +`+verification/src/lib.rs+` `include!` it, so what Creusot verifies is the +code that ships. The specifications are gated behind `+cfg(creusot)+`, which +only `+creusot-rustc+` sets: + +[source,rust] +---- +#[cfg_attr(creusot, requires(lo@ <= hi@))] +#[cfg_attr(creusot, ensures(lo@ <= result@ && result@ <= hi@))] +pub fn clamp(value: u32, lo: u32, hi: u32) -> u32 { ... } +---- + +`+just proof+` translates and discharges both obligations; it exits non-zero +if any goal is unproved. + +See link:verification/README.adoc[verification/README.adoc] for setup. + +== Documentation + +* link:SECURITY.adoc[Security Policy] — vulnerability disclosure +* link:CONTRIBUTING.adoc[Contributing Guide] — how to contribute +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] — community standards +* link:MAINTAINERS.adoc[Maintainers] — ownership and decisions +* link:CHANGELOG.adoc[Changelog] — version history + +== Layout + +.... +. +├── Justfile # build automation (capital J — v2 shape) +├── LICENSE # licence statement +├── LICENSES/ # full licence texts (REUSE style) +├── src/ # crate source +├── tests/ # integration tests +├── verification/ # Rust/Creusot proof crate (detached from workspace) +├── .github/workflows/ # CI + estate gates +├── .machine_readable/ # machine-readable metadata +└── .well-known/ # security.txt, ai.txt, humans.txt +.... + +== Contributing + +See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc]. + +== License + +Code is licensed under the Mozilla Public License, version 2.0 +(`+MPL-2.0+`). Documentation is licensed under Creative Commons +Attribution-ShareAlike 4.0 International (`+CC-BY-SA-4.0+`). + +See link:LICENSE[LICENSE] and the `+LICENSES/+` directory for full texts. + +''''' + +_Created from the aletheia v2 Bronze template._ diff --git a/aletheia/templates/rust/src/impl.rs b/aletheia/templates/rust/src/impl.rs new file mode 100644 index 0000000..46b6833 --- /dev/null +++ b/aletheia/templates/rust/src/impl.rs @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: MPL-2.0 +// Implementation shared verbatim by the main crate and the Creusot crate. +// +// This file is the *single source of truth*. `src/lib.rs` and +// `verification/src/lib.rs` both `include!` it, so the specifications can +// never drift from the code they describe. +// +// The contract attributes are gated behind `cfg(creusot)`, which only +// `creusot-rustc` sets. Under a normal `cargo build` every `#[cfg_attr]` +// below vanishes and the Creusot prelude is never imported, so the main +// crate stays zero-dependency and builds air-gapped. + +#[cfg(creusot)] +use creusot_std::prelude::*; + +/// Clamp `value` into the inclusive range `[lo, hi]`. +/// +/// # Panics +/// +/// Panics if `lo > hi`, which would make the range incoherent. +/// +/// Creusot proves that, given `lo <= hi`, the result always lies within +/// `[lo, hi]`. +#[cfg_attr(creusot, requires(lo@ <= hi@))] +#[cfg_attr(creusot, ensures(lo@ <= result@ && result@ <= hi@))] +#[must_use] +pub fn clamp(value: u32, lo: u32, hi: u32) -> u32 { + assert!(lo <= hi, "incoherent range"); + value.max(lo).min(hi) +} + +/// Overflow-free midpoint of `a` and `b`, rounded towards zero. +/// +/// The naive `(a + b) / 2` overflows when both inputs are large; this form +/// cannot, because it never materialises the sum. Creusot proves the result +/// lies in `[a, b]` and equals the exact half-sum `(a + b) / 2`. +/// +/// # Panics +/// +/// Panics if `a > b` (the subtraction would underflow). +#[cfg_attr(creusot, requires(a@ <= b@))] +#[cfg_attr(creusot, ensures(a@ <= result@ && result@ <= b@))] +#[cfg_attr(creusot, ensures(result@ == (a@ + b@) / 2))] +#[must_use] +pub fn midpoint(a: u32, b: u32) -> u32 { + a + (b - a) / 2 +} diff --git a/aletheia/templates/rust/src/lib.rs b/aletheia/templates/rust/src/lib.rs new file mode 100644 index 0000000..9c92261 --- /dev/null +++ b/aletheia/templates/rust/src/lib.rs @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Core library for @@PROJECT_NAME@@. +//! +//! Replace these sample functions with your own. They are deliberately small +//! but carry *real* preconditions: Creusot discharges the matching proof +//! obligations, and those obligations are written against this very file — +//! `src/lib.rs` includes `impl.rs`, and so does `verification/src/lib.rs`. +//! +//! To change behaviour, edit `src/impl.rs`: both builds pick the change up, +//! so the proof can never drift from the implementation. + +include!("impl.rs"); + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn clamp_keeps_value_within_range() { + assert_eq!(clamp(5, 0, 10), 5); + assert_eq!(clamp(0, 1, 10), 1); + assert_eq!(clamp(99, 0, 10), 10); + } + + #[test] + fn clamp_handles_degenerate_range() { + assert_eq!(clamp(7, 7, 7), 7); + } + + #[test] + #[should_panic(expected = "incoherent range")] + fn clamp_rejects_inverted_range() { + let _ = clamp(5, 10, 0); + } + + #[test] + fn midpoint_matches_naive_on_small_inputs() { + for a in 0..64u32 { + for b in a..64u32 { + assert_eq!(midpoint(a, b), (a + b) / 2, "a={a} b={b}"); + } + } + } + + #[test] + fn midpoint_does_not_overflow() { + assert_eq!(midpoint(u32::MAX, u32::MAX), u32::MAX); + assert_eq!(midpoint(0, u32::MAX), u32::MAX / 2); + } + + #[test] + #[should_panic] + fn midpoint_rejects_inverted_inputs() { + let _ = midpoint(10, 0); + } +} diff --git a/aletheia/templates/rust/src/main.rs b/aletheia/templates/rust/src/main.rs new file mode 100644 index 0000000..c827d83 --- /dev/null +++ b/aletheia/templates/rust/src/main.rs @@ -0,0 +1,68 @@ +// SPDX-License-Identifier: MPL-2.0 +//! @@PROJECT_NAME@@ — command-line entry point. +//! +//! Replace this with your own CLI. It is dependency-free by design: no +//! argument-parsing crate, no network access. + +use std::process::ExitCode; + +use @@CRATE_NAME@@::{clamp, midpoint}; + +const USAGE: &str = "\ +@@PROJECT_NAME@@ @@VERSION@@ + +usage: + @@PROJECT_NAME@@ clamp clamp a value into a range + @@PROJECT_NAME@@ mid midpoint, rounded down (a <= b) + @@PROJECT_NAME@@ --help show this message + +All arguments are unsigned 32-bit integers."; + +fn parse_u32(raw: &str, what: &str) -> Result { + raw.parse::() + .map_err(|_| format!("{what} must be an unsigned integer, got {raw:?}")) +} + +fn main() -> ExitCode { + let args: Vec = std::env::args().skip(1).collect(); + + let result = match args.as_slice() { + [] => { + println!("{USAGE}"); + return ExitCode::SUCCESS; + } + [flag] if flag == "--help" || flag == "-h" => { + println!("{USAGE}"); + return ExitCode::SUCCESS; + } + [cmd, value, lo, hi] if cmd == "clamp" => (|| { + let value = parse_u32(value, "value")?; + let lo = parse_u32(lo, "lo")?; + let hi = parse_u32(hi, "hi")?; + if lo > hi { + return Err(format!("lo ({lo}) must not exceed hi ({hi})")); + } + Ok(clamp(value, lo, hi).to_string()) + })(), + [cmd, a, b] if cmd == "mid" => (|| { + let a = parse_u32(a, "a")?; + let b = parse_u32(b, "b")?; + if a > b { + return Err(format!("a ({a}) must not exceed b ({b})")); + } + Ok(midpoint(a, b).to_string()) + })(), + _ => Err(format!("unrecognised arguments\n\n{USAGE}")), + }; + + match result { + Ok(output) => { + println!("{output}"); + ExitCode::SUCCESS + } + Err(message) => { + eprintln!("error: {message}"); + ExitCode::FAILURE + } + } +} diff --git a/aletheia/templates/rust/tests/integration_test.rs b/aletheia/templates/rust/tests/integration_test.rs new file mode 100644 index 0000000..f56de40 --- /dev/null +++ b/aletheia/templates/rust/tests/integration_test.rs @@ -0,0 +1,51 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Integration tests: exercise the public API exactly as a consumer would. + +use @@CRATE_NAME@@::{clamp, midpoint}; + +#[test] +fn clamp_is_idempotent() { + for value in [0u32, 1, 5, 42, u32::MAX] { + let once = clamp(value, 10, 100); + assert_eq!(clamp(once, 10, 100), once, "clamping twice changed {value}"); + } +} + +#[test] +fn clamp_result_always_in_range() { + let (lo, hi) = (10u32, 100u32); + for value in [0u32, 9, 10, 55, 100, 101, u32::MAX] { + let got = clamp(value, lo, hi); + assert!( + got >= lo && got <= hi, + "clamp({value}) = {got} out of range" + ); + } +} + +#[test] +fn midpoint_stays_between_inputs() { + let cases = [ + (0u32, 0u32), + (1, 2), + (0, u32::MAX), + (u32::MAX, u32::MAX), + (7, 9), + ]; + for (a, b) in cases { + let mid = midpoint(a, b); + assert!( + mid >= a && mid <= b, + "midpoint({a}, {b}) = {mid} out of range" + ); + } +} + +#[test] +fn midpoint_is_the_half_sum() { + let cases = [(0u32, 0u32), (1, 2), (0, u32::MAX), (u32::MAX, u32::MAX)]; + for (a, b) in cases { + let expected = a / 2 + b / 2 + (a % 2 + b % 2) / 2; + assert_eq!(midpoint(a, b), expected, "midpoint({a}, {b})"); + } +} diff --git a/aletheia/templates/rust/verification/Cargo.toml b/aletheia/templates/rust/verification/Cargo.toml new file mode 100644 index 0000000..f565881 --- /dev/null +++ b/aletheia/templates/rust/verification/Cargo.toml @@ -0,0 +1,21 @@ +[package] +name = "@@PROJECT_NAME@@-verification" +version = "0.1.0" +edition = "2024" +license = "MPL-2.0" +description = "Creusot proof obligations for @@PROJECT_NAME@@" +publish = false + +# This crate is deliberately NOT part of the main workspace (see the root +# Cargo.toml `exclude`), so the main crate stays zero-dependency. +# +# `creusot-std` is resolved locally by the Creusot toolchain: `cargo creusot +# config --update` writes a `[patch.crates-io]` entry into your cargo config +# pointing at the installed copy. Nothing is fetched from a git remote here. +[dependencies] +creusot-std = "0.14.0-dev" + +# `src/impl.rs` (included below) gates its specifications behind +# `#[cfg(creusot)]`; declare the cfg so the lint stays meaningful. +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(creusot)"] } diff --git a/aletheia/templates/rust/verification/README.adoc b/aletheia/templates/rust/verification/README.adoc new file mode 100644 index 0000000..615b2f3 --- /dev/null +++ b/aletheia/templates/rust/verification/README.adoc @@ -0,0 +1,125 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Creusot Verification +:toc: + +Per the estate language policy, *Rust here means Rust/Creusot*: Rust plus +https://github.com/creusot-rs/creusot[Creusot], the deductive verifier that +lowers annotated Rust to Why3 and discharges the resulting proof obligations +with SMT solvers. + +These obligations are *real and discharged*. `just proof` translates the +source and runs the solvers; it exits non-zero if any goal is unproved. +Nothing in this directory is aspirational. + +== One Source, Not A Mirror + +The usual way to verify Rust with Creusot is to keep a second, annotated copy +of the functions — which then drifts from the code that ships, so the proof +describes something that no longer exists. + +This template avoids that. `src/impl.rs` is the single source of truth, and +it is `include!`d by both crates: + +[source,rust] +---- +// src/lib.rs (main crate, zero dependencies) +include!("impl.rs"); + +// verification/src/lib.rs (Creusot crate) +include!("../../src/impl.rs"); +---- + +The specifications live inline in `src/impl.rs`, gated behind `cfg(creusot)`: + +[source,rust] +---- +#[cfg(creusot)] +use creusot_std::prelude::*; + +#[cfg_attr(creusot, requires(lo@ <= hi@))] +#[cfg_attr(creusot, ensures(lo@ <= result@ && result@ <= hi@))] +pub fn clamp(value: u32, lo: u32, hi: u32) -> u32 { ... } +---- + +`creusot-rustc` is the only thing that sets `--cfg creusot`. Under a plain +`cargo build` every `#[cfg_attr]` disappears and the Creusot prelude is never +imported, so the main crate keeps its zero-dependency, air-gapped build. +Under `cargo creusot` the attributes become live specifications verified +against the *actual* compiled function bodies. + +== Toolchain + +Creusot is research software pinned to a specific nightly Rust, and it pins +matching forks of Why3 and why3find. Install all four together — installing +stock `why3`/`why3find` from a package manager will not work: + +[source,bash] +---- +git clone --depth 1 https://github.com/creusot-rs/creusot +cd creusot && rustup toolchain install "$(cat rust-toolchain)" # + rustc-dev, llvm-tools +opam switch create 4.14.1 +# why3 and why3find are the *pinned forks* declared in creusot-deps.opam +cargo run --bin creusot-install -- --external z3 --external cvc5 \ + prelude cargo-creusot creusot-rustc why3-conf +cargo creusot config --update # patches creusot-std into your cargo config +---- + +The exact pins at the time of writing were `why3` commit `c369bc4c` +(`gitlab.inria.fr/why3/why3`) and `why3find` commit `0f054b93` +(`github.com/creusot-rs/why3find`). Verify with `why3 --version` that the +pinned build is active before trusting a proof run: a stock Why3 release +cannot even parse the Coma that a given Creusot emits. + +Then, from the repository root: + +[source,bash] +---- +just proof # translate + discharge; non-zero exit on any unproved goal +just proof-clean # remove generated artefacts +---- + +== What Is Proved + +[cols="1,1,2"] +|=== +|`clamp` |`lo <= hi` |the result always lies within `[lo, hi]` + +|`midpoint` |`a <= b` |the result lies in `[a, b]`, and equals the exact half-sum `(a + b) / 2` — with no intermediate overflow +|=== + +Both obligations are discharged by Z3 and CVC5. `just proof` is a real gate: +change either function so that a postcondition no longer holds and it fails +with `proof failed` and a non-zero exit code. + +== Scope And Honest Limitations + +*Creusot 0.14 cannot reason about bitwise operations.* The `@` ("view") +operator maps an integer to a mathematical `Int`, and `creusot_std::logic` +provides no `BitAnd`/`BitXor`/`Shr` for it. A function such as + +[source,rust] +---- +pub fn mean_floor(a: u32, b: u32) -> u32 { + (a & b) + ((a ^ b) >> 1) // overflow-free mean, but unprovable here +} +---- + +is *rejected*, and not merely because no postcondition is stated: Creusot +still has to discharge overflow-freedom for the `+`, and it has no +bitvector theory to do so with. That is why `midpoint` — the same idea, +expressed as `a + (b - a) / 2`, which needs only linear arithmetic — is the +sample that ships. If you need a bit-twiddling kernel verified, it will have +to wait for bitvector support upstream, or move behind a proven wrapper. + +*The main crate is not itself verified.* Only the functions in +`src/impl.rs` are. Adding a function there adds it to Creusot's remit +automatically: it will be translated and, if it contains arithmetic, must +have its overflow-freedom proved too. Functions that cannot be proved +belong outside `src/impl.rs`, and the reason belongs in a comment. + +*CI does not run the proofs yet.* The Bronze/Silver gate runs `just check`, +which is `build test fmt lint deps-check` — all offline, zero-dependency. +Creusot needs a nightly toolchain plus three pinned forks, which is too heavy +and too non-reproducible to put in a default CI job. Wiring `just proof` into +a dedicated, pinned CI job is a deliberate follow-on, and until then this +template does not claim CI-verified proofs. diff --git a/aletheia/templates/rust/verification/src/lib.rs b/aletheia/templates/rust/verification/src/lib.rs new file mode 100644 index 0000000..21d1bdf --- /dev/null +++ b/aletheia/templates/rust/verification/src/lib.rs @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Creusot proof obligations for @@PROJECT_NAME@@. +//! +//! This crate contains no code of its own. It `include!`s the parent crate's +//! `src/impl.rs`, and under `creusot-rustc` the `#[cfg(creusot)]` attributes +//! in that file come alive as Creusot specifications. The implementations +//! being verified are therefore the *real* ones, not a mirrored copy: there +//! is nothing here that can drift out of sync with `../src/`. +//! +//! Run `just proof` from the repository root to translate and discharge the +//! obligations. See `../README.adoc` for the toolchain setup. + +include!("../../src/impl.rs"); diff --git a/aletheia/templates/rust/verification/why3find.json b/aletheia/templates/rust/verification/why3find.json new file mode 100644 index 0000000..3e051cc --- /dev/null +++ b/aletheia/templates/rust/verification/why3find.json @@ -0,0 +1,9 @@ +{ + "fast": 0.2, + "time": 1, + "depth": 6, + "packages": ["creusot"], + "provers": ["z3", "cvc5"], + "tactics": ["compute_specified", "split_vc"], + "warnoff": ["unused_variable", "axiom_abstract"] +} diff --git a/aletheia/templates/zig/.editorconfig b/aletheia/templates/zig/.editorconfig new file mode 100644 index 0000000..a5b818b --- /dev/null +++ b/aletheia/templates/zig/.editorconfig @@ -0,0 +1,19 @@ +# @@PROJECT_NAME@@ - Editor Configuration +# https://editorconfig.org + +root = true + +[*] +charset = utf-8 +end_of_line = lf +indent_size = 4 +indent_style = space +insert_final_newline = true +trim_trailing_whitespace = true + +[*.adoc] +trim_trailing_whitespace = false + +[Justfile] +indent_style = space +indent_size = 4 diff --git a/aletheia/templates/zig/.github/workflows/ci.yml b/aletheia/templates/zig/.github/workflows/ci.yml new file mode 100644 index 0000000..553830f --- /dev/null +++ b/aletheia/templates/zig/.github/workflows/ci.yml @@ -0,0 +1,41 @@ +# SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. +name: CI + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + actions: read + contents: read + +jobs: + check: + name: Build, test, lint (offline) + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Install Zig + uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2 + with: + version: 0.16.0 + + - name: Build + run: zig build + + - name: Test + run: zig build test + + - name: Check formatting + run: zig fmt --check build.zig src test diff --git a/aletheia/templates/zig/.gitignore b/aletheia/templates/zig/.gitignore new file mode 100644 index 0000000..b20e72f --- /dev/null +++ b/aletheia/templates/zig/.gitignore @@ -0,0 +1,5 @@ +# SPDX-License-Identifier: MPL-2.0 +/.zig-cache/ +.zig-cache/ +/zig-out/ +zig-out/ diff --git a/aletheia/templates/zig/.machine_readable/rsr-profile.a2ml b/aletheia/templates/zig/.machine_readable/rsr-profile.a2ml new file mode 100644 index 0000000..85d42c5 --- /dev/null +++ b/aletheia/templates/zig/.machine_readable/rsr-profile.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# RSR capability profile for @@PROJECT_NAME@@. Declares what this repo +# carries so the capability gates compute the applicable criterion set. +[profile] +capabilities = ["zig", "cli", "docs"] + +[rationale] +zig = "true: build.zig targets Zig 0.16 (see .tool-versions)" +cli = "true: src/main.zig produces an executable" +docs = "true: README + SECURITY + CONTRIBUTING + CODE_OF_CONDUCT + CHANGELOG" +no-library = "shared: src/root.zig is an importable module, but not published as a package" +no-container = "true: no Containerfile in the scaffold" diff --git a/aletheia/templates/zig/.tool-versions b/aletheia/templates/zig/.tool-versions new file mode 100644 index 0000000..1fa0956 --- /dev/null +++ b/aletheia/templates/zig/.tool-versions @@ -0,0 +1,2 @@ +# Toolchain pins, asdf/mise compatible. +zig 0.16.0 diff --git a/aletheia/templates/zig/Justfile b/aletheia/templates/zig/Justfile new file mode 100644 index 0000000..f731a6f --- /dev/null +++ b/aletheia/templates/zig/Justfile @@ -0,0 +1,37 @@ +# SPDX-License-Identifier: MPL-2.0 +# Justfile — build automation for @@PROJECT_NAME@@. +# See: https://github.com/casey/just +# +# Every recipe here is offline: this project has no external dependencies, +# so nothing is fetched at build time. Recipes fail loudly — a recipe that +# echoes a message and exits 0 would be a fake gate (RSR v2 6.1.5, Gold). + +default: + @just --list + +# Build the executable into zig-out/bin/ +build: + zig build + +# Run the program; pass arguments after the recipe name +run *ARGS: + zig build run -- {{ARGS}} + +# Run unit and integration tests +test: + zig build test + +# Check formatting (does not modify files) +fmt: + zig fmt --check build.zig src test + +# Apply formatting +fmt-fix: + zig fmt build.zig src test + +# Verify RSR compliance using the estate checker +verify: + aletheia . + +# Everything the CI gate runs, in the same order +check: build test fmt diff --git a/aletheia/templates/zig/README.adoc b/aletheia/templates/zig/README.adoc new file mode 100644 index 0000000..1e89576 --- /dev/null +++ b/aletheia/templates/zig/README.adoc @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += @@PROJECT_NAME@@ +:toc: +:icons: font + +____ +@@PROJECT_DESCRIPTION@@ +____ + +== Quick Start + +[source,bash] +---- +# Build (offline — nothing is downloaded) +just build + +# Test +just test + +# Verify RSR compliance +just verify +---- + +This project is *standalone by construction*: the scaffold fetches nothing, +the build has no external dependencies, and the licence texts ship in-tree +under `+LICENSES/+`. + +== RSR Compliance + +[cols="1,3"] +|=== +|Bronze |Documentation, security policy, SPDX headers, CI, licence classification +|Silver |`.editorconfig`, `.tool-versions`, machine-readable manifests, SHA-pinned CI, `+LICENSES/+` +|Gold |No silent-skip recipes +|=== + +Verify with the estate's own checker: + +[source,bash] +---- +aletheia . +---- + +== Language: @@LANG_DISPLAY@@ + +@@LANG_POLICY@@ + +== Documentation + +* link:SECURITY.adoc[Security Policy] — vulnerability disclosure +* link:CONTRIBUTING.adoc[Contributing Guide] — how to contribute +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] — community standards +* link:MAINTAINERS.adoc[Maintainers] — ownership and decisions +* link:CHANGELOG.adoc[Changelog] — version history + +== Layout + +.... +. +├── Justfile # build automation (capital J — v2 shape) +├── LICENSE # licence statement +├── LICENSES/ # full licence texts (REUSE style) +├── src/ # source (layout follows the language's conventions) +├── .github/workflows/ # CI + estate gates +├── .machine_readable/ # machine-readable metadata +└── .well-known/ # security.txt, ai.txt, humans.txt +.... + +== Contributing + +See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc]. + +== License + +Code is licensed under the Mozilla Public License, version 2.0 +(`+MPL-2.0+`). Documentation is licensed under Creative Commons +Attribution-ShareAlike 4.0 International (`+CC-BY-SA-4.0+`). + +See link:LICENSE[LICENSE] and the `+LICENSES/+` directory for full texts. + +''''' + +_Created from the aletheia v2 Bronze template._ diff --git a/aletheia/templates/zig/build.zig b/aletheia/templates/zig/build.zig new file mode 100644 index 0000000..1139f72 --- /dev/null +++ b/aletheia/templates/zig/build.zig @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Build graph for @@PROJECT_NAME@@. +//! +//! Zero dependencies and no network use: `zig build` compiles from this +//! tree alone, which is why the scaffold works air-gapped. +//! +//! NOTE ON build.zig.zon: there is none. Zig 0.16 requires a package +//! `fingerprint` in it, and — correctly — refuses a fingerprint that was +//! not generated for that package name, so a template cannot ship one +//! without guessing. It is not needed to build: run +//! `zig fetch --save ` when you add your first dependency and Zig +//! will create build.zig.zon with a valid fingerprint for you. + +const std = @import("std"); + +pub fn build(b: *std.Build) void { + const target = b.standardTargetOptions(.{}); + const optimize = b.standardOptimizeOption(.{}); + + // The library module — business logic, importable and testable. + const lib = b.addModule("@@MOD_NAME@@", .{ + .root_source_file = b.path("src/root.zig"), + .target = target, + .optimize = optimize, + }); + + // The CLI, which imports the library under the project's own name. + const exe = b.addExecutable(.{ + .name = "@@PROJECT_NAME@@", + .root_module = b.createModule(.{ + .root_source_file = b.path("src/main.zig"), + .target = target, + .optimize = optimize, + .imports = &.{ + .{ .name = "@@MOD_NAME@@", .module = lib }, + }, + }), + }); + b.installArtifact(exe); + + const run_step = b.step("run", "Run the app"); + const run_cmd = b.addRunArtifact(exe); + run_cmd.step.dependOn(b.getInstallStep()); + if (b.args) |args| run_cmd.addArgs(args); + run_step.dependOn(&run_cmd.step); + + // Unit tests live beside the code they exercise. + const lib_tests = b.addTest(.{ .root_module = lib }); + const run_lib_tests = b.addRunArtifact(lib_tests); + + const exe_tests = b.addTest(.{ .root_module = exe.root_module }); + const run_exe_tests = b.addRunArtifact(exe_tests); + + // Integration tests exercise the public API as a consumer would. + const integration_tests = b.addTest(.{ + .root_module = b.createModule(.{ + .root_source_file = b.path("test/integration_test.zig"), + .target = target, + .optimize = optimize, + .imports = &.{ + .{ .name = "@@MOD_NAME@@", .module = lib }, + }, + }), + }); + const run_integration_tests = b.addRunArtifact(integration_tests); + + const test_step = b.step("test", "Run unit and integration tests"); + test_step.dependOn(&run_lib_tests.step); + test_step.dependOn(&run_exe_tests.step); + test_step.dependOn(&run_integration_tests.step); +} diff --git a/aletheia/templates/zig/src/main.zig b/aletheia/templates/zig/src/main.zig new file mode 100644 index 0000000..20a6320 --- /dev/null +++ b/aletheia/templates/zig/src/main.zig @@ -0,0 +1,73 @@ +// SPDX-License-Identifier: MPL-2.0 +//! @@PROJECT_NAME@@ — command-line entry point. +//! +//! Written against the Zig 0.16 I/O API (`std.process.Init` + `std.Io`). + +const std = @import("std"); +const Io = std.Io; +const core = @import("@@MOD_NAME@@"); + +const usage = + \\@@PROJECT_NAME@@ @@VERSION@@ + \\ + \\usage: + \\ @@PROJECT_NAME@@ clamp clamp a value into a range + \\ @@PROJECT_NAME@@ mean integer mean, rounded down + \\ @@PROJECT_NAME@@ --help show this message + \\ + \\All arguments are unsigned 32-bit integers. +; + +pub fn main(init: std.process.Init) !void { + const arena: std.mem.Allocator = init.arena.allocator(); + const io = init.io; + const args = try init.minimal.args.toSlice(arena); + + var stdout_buffer: [1024]u8 = undefined; + var stdout_file_writer: Io.File.Writer = .init(.stdout(), io, &stdout_buffer); + const stdout = &stdout_file_writer.interface; + + var stderr_buffer: [1024]u8 = undefined; + var stderr_file_writer: Io.File.Writer = .init(.stderr(), io, &stderr_buffer); + const stderr = &stderr_file_writer.interface; + + if (args.len < 2) { + try stdout.print("{s}\n", .{usage}); + try stdout.flush(); + return; + } + + const cmd = args[1]; + if (std.mem.eql(u8, cmd, "--help") or std.mem.eql(u8, cmd, "-h")) { + try stdout.print("{s}\n", .{usage}); + try stdout.flush(); + return; + } + + if (std.mem.eql(u8, cmd, "clamp")) { + if (args.len == 5) { + const value = std.fmt.parseInt(u32, args[2], 10) catch null; + const lo = std.fmt.parseInt(u32, args[3], 10) catch null; + const hi = std.fmt.parseInt(u32, args[4], 10) catch null; + if (value != null and lo != null and hi != null and lo.? <= hi.?) { + try stdout.print("{d}\n", .{core.clamp(value.?, lo.?, hi.?)}); + try stdout.flush(); + return; + } + } + } else if (std.mem.eql(u8, cmd, "mean")) { + if (args.len == 4) { + const a = std.fmt.parseInt(u32, args[2], 10) catch null; + const b = std.fmt.parseInt(u32, args[3], 10) catch null; + if (a != null and b != null) { + try stdout.print("{d}\n", .{core.meanFloor(a.?, b.?)}); + try stdout.flush(); + return; + } + } + } + + try stderr.print("error: unrecognised arguments\n\n{s}\n", .{usage}); + try stderr.flush(); + std.process.exit(1); +} diff --git a/aletheia/templates/zig/src/root.zig b/aletheia/templates/zig/src/root.zig new file mode 100644 index 0000000..b9cf682 --- /dev/null +++ b/aletheia/templates/zig/src/root.zig @@ -0,0 +1,48 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Core library for @@PROJECT_NAME@@. +//! +//! Replace these sample functions with your own. + +const std = @import("std"); + +/// Clamp `value` into the inclusive range `[lo, hi]`. +/// +/// Asserts `lo <= hi`; an inverted range is a programming error, not a +/// silent no-op. +pub fn clamp(value: u32, lo: u32, hi: u32) u32 { + std.debug.assert(lo <= hi); + return @min(@max(value, lo), hi); +} + +/// Integer mean of two `u32`s, rounded towards zero. +/// +/// The naive `(a + b) / 2` overflows for large inputs; this form cannot, +/// because it never materialises the sum. +pub fn meanFloor(a: u32, b: u32) u32 { + return (a & b) + ((a ^ b) >> 1); +} + +test "clamp keeps value within range" { + try std.testing.expectEqual(@as(u32, 5), clamp(5, 0, 10)); + try std.testing.expectEqual(@as(u32, 1), clamp(0, 1, 10)); + try std.testing.expectEqual(@as(u32, 10), clamp(99, 0, 10)); +} + +test "clamp handles a degenerate range" { + try std.testing.expectEqual(@as(u32, 7), clamp(7, 7, 7)); +} + +test "meanFloor matches the naive form on small inputs" { + var a: u32 = 0; + while (a < 64) : (a += 1) { + var b: u32 = 0; + while (b < 64) : (b += 1) { + try std.testing.expectEqual((a + b) / 2, meanFloor(a, b)); + } + } +} + +test "meanFloor does not overflow" { + try std.testing.expectEqual(std.math.maxInt(u32), meanFloor(std.math.maxInt(u32), std.math.maxInt(u32))); + try std.testing.expectEqual(std.math.maxInt(u32) / 2, meanFloor(std.math.maxInt(u32), 0)); +} diff --git a/aletheia/templates/zig/test/integration_test.zig b/aletheia/templates/zig/test/integration_test.zig new file mode 100644 index 0000000..f256d3e --- /dev/null +++ b/aletheia/templates/zig/test/integration_test.zig @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Integration tests: exercise the public API as a consumer would. + +const std = @import("std"); +const core = @import("@@MOD_NAME@@"); + +test "clamp is idempotent" { + const values = [_]u32{ 0, 1, 5, 42, std.math.maxInt(u32) }; + for (values) |value| { + const once = core.clamp(value, 10, 100); + try std.testing.expectEqual(once, core.clamp(once, 10, 100)); + } +} + +test "clamp result is always inside the range" { + const lo: u32 = 10; + const hi: u32 = 100; + const values = [_]u32{ 0, 9, 10, 55, 100, 101, std.math.maxInt(u32) }; + for (values) |value| { + const got = core.clamp(value, lo, hi); + try std.testing.expect(got >= lo and got <= hi); + } +} + +test "meanFloor never exceeds either input" { + const cases = [_][2]u32{ + .{ 0, 0 }, + .{ 1, 2 }, + .{ std.math.maxInt(u32), 0 }, + .{ std.math.maxInt(u32), std.math.maxInt(u32) }, + .{ 7, 9 }, + }; + for (cases) |case| { + const mean = core.meanFloor(case[0], case[1]); + try std.testing.expect(mean <= @max(case[0], case[1])); + } +} diff --git a/aletheia/tests/integration_tests.rs b/aletheia/tests/integration_tests.rs index 3bba16a..7a8eda6 100644 --- a/aletheia/tests/integration_tests.rs +++ b/aletheia/tests/integration_tests.rs @@ -1331,3 +1331,387 @@ fn test_bun_lockfile_carveout() { ); fs::remove_dir_all(bare).ok(); } + +/// REGRESSION GUARD (issue #186): a freshly scaffolded project must pass +/// aletheia Bronze (and Silver) with no hand edits. +/// +/// The v1-era generator emitted the retired shape — `LICENSE.txt`, +/// lowercase `justfile`, `flake.nix`, `.gitlab-ci.yml` — which failed +/// Bronze on day one. This test runs the real generator and audits its +/// real output, so the template and the checker cannot drift apart again +/// without the suite going red. +#[test] +fn test_scaffold_passes_bronze_and_silver() { + let pid = std::process::id(); + let work = std::env::temp_dir().join(format!("aletheia_scaffold_{pid}")); + if work.exists() { + fs::remove_dir_all(&work).ok(); + } + fs::create_dir_all(&work).expect("Failed to create scaffold workspace"); + + let generator = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("scripts") + .join("create-template.sh"); + + // `--no-git` keeps the probe hermetic: it does not depend on the + // machine having a configured git identity. + let generated = Command::new("bash") + .arg(&generator) + .arg("scaffold-probe") + .arg("--no-git") + .arg("-d") + .arg("Regression probe for the v2 scaffold") + .current_dir(&work) + .output() + .expect("Failed to run create-template.sh"); + + assert!( + generated.status.success(), + "generator failed (exit {:?}): {}", + generated.status.code(), + String::from_utf8_lossy(&generated.stderr) + ); + + let project = work.join("scaffold-probe"); + assert!(project.is_dir(), "generator produced no project directory"); + + // The retired v1 shape must never come back. + for stale in ["LICENSE.txt", "justfile", "flake.nix", ".gitlab-ci.yml"] { + assert!( + !project.join(stale).exists(), + "retired v1 artefact regenerated: {stale} (issue #186)" + ); + } + + // The generator must leave no unresolved template placeholder behind. + let readme = fs::read_to_string(project.join("README.adoc")) + .expect("scaffold should contain README.adoc"); + assert!( + !readme.contains("@@"), + "unresolved template placeholder left in README.adoc" + ); + + let output = aletheia() + .arg(project.to_str().unwrap()) + .output() + .expect("Failed to run aletheia"); + let stdout = String::from_utf8_lossy(&output.stdout); + + assert!( + stdout.contains("Bronze-level RSR compliance: ACHIEVED"), + "fresh scaffold must pass Bronze with no hand edits (issue #186): {stdout}" + ); + assert!( + stdout.contains("Silver-level RSR compliance: ACHIEVED"), + "fresh scaffold should also reach Silver: {stdout}" + ); + assert_eq!( + output.status.code(), + Some(0), + "a compliant scaffold must exit 0: {stdout}" + ); + + fs::remove_dir_all(&work).ok(); +} + +/// Build output must not change the verdict. +/// +/// Reported after the #186/#197 work: running the gate on a tree that had just +/// been built made it fail, because the scanner counted generated files +/// (`obj/b__main.ads`, `target/...`, `_build/...`) as sources lacking SPDX +/// headers. The scanner now honours the repository's own `.gitignore`, so +/// auditing a freshly built tree gives the same answer as auditing a clean +/// checkout. +#[test] +fn test_gitignore_keeps_build_output_out_of_the_audit() { + let repo = create_test_repo("gitignore_build_output"); + + // A minimal compliant project. + create_file(&repo, "README.md", "# Probe\n"); + create_file(&repo, "LICENSE", "MPL-2.0\n"); + create_file(&repo, ".gitattributes", "* text=auto\n"); + create_file(&repo, ".editorconfig", "root = true\n"); + create_file(&repo, "justfile", "default:\n @true\n"); + create_file(&repo, "SECURITY.md", "# Security\n"); + create_file(&repo, "CONTRIBUTING.md", "# Contributing\n"); + create_file(&repo, "CHANGELOG.md", "# Changelog\n"); + create_file(&repo, "CODE_OF_CONDUCT.md", "# CoC\n"); + create_file( + &repo, + ".well-known/security.txt", + "Contact: x@example.org\n", + ); + create_file(&repo, ".well-known/ai.txt", "ai\n"); + create_file(&repo, ".well-known/humans.txt", "humans\n"); + create_file(&repo, ".github/workflows/ci.yml", PINNED_WORKFLOW); + create_file( + &repo, + "src/main.rs", + "// SPDX-License-Identifier: MPL-2.0\nfn main() {}\n", + ); + create_file(&repo, ".gitignore", "target/\nobj/\ndist-newstyle/\n"); + + let clean = aletheia() + .arg(repo.to_str().unwrap()) + .output() + .expect("run"); + let clean_out = String::from_utf8_lossy(&clean.stdout); + assert!( + clean_out.contains("Bronze-level RSR compliance: ACHIEVED"), + "the clean tree should be compliant: {clean_out}" + ); + + // Now simulate a build: generated files, no SPDX headers, inside ignored + // directories. This is exactly what broke the gate in practice. + create_file(&repo, "target/debug/build.rs", "fn generated() {}\n"); + create_file( + &repo, + "obj/b__main.ads", + "package B__Main is end B__Main;\n", + ); + create_file(&repo, "dist-newstyle/build/x.rs", "fn y() {}\n"); + + let built = aletheia() + .arg(repo.to_str().unwrap()) + .output() + .expect("run"); + let built_out = String::from_utf8_lossy(&built.stdout); + + // The verdict must be identical to the clean run — same score, and the + // generated files must not appear in any suggestion. + assert!( + !built_out.contains("b__main.ads") + && !built_out.contains("dist-newstyle") + && !built_out.contains("target/debug/build.rs"), + "ignored build output leaked back into the audit: {built_out}" + ); + assert!( + built_out.contains("Bronze-level RSR compliance: ACHIEVED"), + "a built tree must give the clean-tree verdict: {built_out}" + ); + assert_eq!( + built.status.code(), + clean.status.code(), + "exit code changed after a build" + ); + + // A file that is *not* ignored must still be audited: the mechanism must + // not become a blanket exemption. + create_file(&repo, "src/unheadered.rs", "fn no_header() {}\n"); + let leaky = aletheia() + .arg(repo.to_str().unwrap()) + .output() + .expect("run"); + let leaky_out = String::from_utf8_lossy(&leaky.stdout); + assert!( + leaky_out.contains("unheadered.rs"), + "a non-ignored file must still be scanned: {leaky_out}" + ); + + fs::remove_dir_all(&repo).ok(); +} + +/// A directory-only rule must not exempt a *file* of the same name. +/// +/// `Makefile/` in git matches a directory called `Makefile`; a regular file +/// called `Makefile` is untouched. The scanner asks the type-aware question, +/// so it inherits that behaviour instead of blanket-skipping the name. Uses +/// the banned-build-files check as the probe, because it reports file names +/// and therefore makes the difference observable. +#[test] +fn test_gitignore_directory_rule_does_not_exempt_same_named_file() { + let repo = create_test_repo("gitignore_dir_only"); + + create_file(&repo, ".gitignore", "Makefile/\n"); + // A regular file whose name matches a directory-only rule. + create_file(&repo, "Makefile", "all:\n\t@true\n"); + + let output = aletheia() + .arg(repo.to_str().unwrap()) + .output() + .expect("run"); + let stdout = String::from_utf8_lossy(&output.stdout); + assert!( + stdout.contains("Makefile"), + "a file named `Makefile` must still be audited despite the `Makefile/` rule: {stdout}" + ); + + fs::remove_dir_all(&repo).ok(); +} + +/// The same name as a real directory *is* skipped, contents and all. +#[test] +fn test_gitignore_directory_rule_skips_the_directory_and_its_contents() { + let repo = create_test_repo("gitignore_dir_real"); + + create_file(&repo, ".gitignore", "vendored/\n"); + // Unmistakably generated, unmistakably headerless — if the scanner reads + // this, the score drops and the path shows up in a suggestion. + create_file( + &repo, + "vendored/generated_helper.adb", + "package Generated_Helper is end;\n", + ); + create_file( + &repo, + "vendored/deep/nested/deep_generated.adb", + "package Deep is end;\n", + ); + + let output = aletheia() + .arg(repo.to_str().unwrap()) + .output() + .expect("run"); + let stdout = String::from_utf8_lossy(&output.stdout); + assert!( + !stdout.contains("generated_helper.adb") && !stdout.contains("deep_generated.adb"), + "contents of an ignored directory must be skipped: {stdout}" + ); + + // And the same file in a directory that is NOT ignored still reports, so + // the rule is scoped and not a blanket exemption. + create_file( + &repo, + "src/not_ignored_helper.adb", + "package Not_Ignored is end;\n", + ); + let output = aletheia() + .arg(repo.to_str().unwrap()) + .output() + .expect("run"); + let stdout = String::from_utf8_lossy(&output.stdout); + assert!( + stdout.contains("not_ignored_helper.adb"), + "a file outside the ignored directory must still be audited: {stdout}" + ); + + fs::remove_dir_all(&repo).ok(); +} + +/// Regression probe for the six-language template set (follow-on to #186). +/// +/// Every language `create-template.sh` advertises must scaffold cleanly and +/// reach Bronze *and* Silver with no hand edits. The single-language probe +/// above covers the generator's default; this one covers the whole set, so a +/// template that regresses under a language overlay cannot slip through. +/// +/// Note on scope: this asserts the *build-time* contract only — file shape, +/// placeholder resolution and the RSR gate. It does not run Creusot or +/// gnatprove; those need nightly Rust plus pinned Why3 forks, and a pinned +/// GNAT, which a unit test must not require. The proof gates are exercised by +/// `just proof` in each template, and their negative controls live with them. +#[test] +fn test_every_language_template_reaches_bronze_and_silver() { + /// Recursively collect files containing an unresolved `@@` placeholder. + fn files_with_placeholders(dir: &Path, found: &mut Vec) { + let Ok(entries) = fs::read_dir(dir) else { + return; + }; + for entry in entries.flatten() { + let path = entry.path(); + if path.file_name().is_some_and(|n| n == ".git") { + continue; + } + if path.is_dir() { + files_with_placeholders(&path, found); + } else if fs::read_to_string(&path).is_ok_and(|body| body.contains("@@")) { + found.push(path); + } + } + } + + const LANGS: &[&str] = &["rust", "zig", "elixir", "haskell", "ada", "agda"]; + + let pid = std::process::id(); + let work = std::env::temp_dir().join(format!("aletheia_langs_{pid}")); + if work.exists() { + fs::remove_dir_all(&work).ok(); + } + fs::create_dir_all(&work).expect("Failed to create scaffold workspace"); + + let generator = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("scripts") + .join("create-template.sh"); + + for lang in LANGS { + let name = format!("probe-{lang}"); + + // `--no-git` keeps the probe hermetic: no git identity is needed, and + // a working tree without .git exercises the same file set. + let generated = Command::new("bash") + .arg(&generator) + .arg(&name) + .arg("-l") + .arg(lang) + .arg("--no-git") + .current_dir(&work) + .output() + .unwrap_or_else(|e| panic!("Failed to run create-template.sh for {lang}: {e}")); + + assert!( + generated.status.success(), + "[{lang}] generator failed (exit {:?}): {}", + generated.status.code(), + String::from_utf8_lossy(&generated.stderr) + ); + + let project = work.join(&name); + assert!(project.is_dir(), "[{lang}] no project directory produced"); + + let mut stragglers = Vec::new(); + files_with_placeholders(&project, &mut stragglers); + assert!( + stragglers.is_empty(), + "[{lang}] unresolved template placeholders in: {stragglers:?}" + ); + + let output = aletheia() + .arg(project.to_str().unwrap()) + .output() + .unwrap_or_else(|e| panic!("Failed to run aletheia for {lang}: {e}")); + let stdout = String::from_utf8_lossy(&output.stdout); + + assert!( + stdout.contains("Score: 26/26 checks passed (100.0%)"), + "[{lang}] template must reach 26/26 with no hand edits: {stdout}" + ); + assert!( + stdout.contains("Bronze-level RSR compliance: ACHIEVED"), + "[{lang}] Bronze not achieved: {stdout}" + ); + assert!( + stdout.contains("Silver-level RSR compliance: ACHIEVED"), + "[{lang}] Silver not achieved: {stdout}" + ); + assert_eq!( + output.status.code(), + Some(0), + "[{lang}] a compliant scaffold must exit 0: {stdout}" + ); + } + + // The estate's two proof-carrying templates must actually carry the + // markers that make their language label true. + let rust_manifest = fs::read_to_string(work.join("probe-rust/verification/Cargo.toml")) + .expect("rust template should ship verification/Cargo.toml"); + assert!( + rust_manifest.contains("creusot-std"), + "Rust means Rust/Creusot: the verification crate must depend on creusot-std" + ); + + let rust_impl = fs::read_to_string(work.join("probe-rust/src/impl.rs")) + .expect("rust template should ship src/impl.rs"); + assert!( + rust_impl.contains("cfg(creusot)") && rust_impl.contains("requires("), + "rust template must carry Creusot contracts gated behind cfg(creusot)" + ); + + let ada_spec = fs::read_to_string(work.join("probe-ada/src/probe_ada.ads")) + .expect("ada template should ship its package spec"); + assert!( + ada_spec.contains("pragma SPARK_Mode (On)"), + "Ada means Ada/SPARK: the core package must declare SPARK_Mode (On)" + ); + + fs::remove_dir_all(&work).ok(); +}