From 86d8f90712b9540ba5b3d0eeaa18cbb8537ddbeb Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 21:19:41 +0000 Subject: [PATCH 01/12] perf(scanner): one traversal, and honour the repository's .gitignore Two changes to the same walk. #197: the seven file-list checks each walked the tree separately. They now share a single memoised traversal filling four buckets in one pass. Depth, skip-dir, submodule and per-check budget semantics are unchanged, so each bucket receives exactly the files its own walk saw. Measured on 18,602 files / 673 dirs, best of 10: 212 ms -> 150 ms. Verdicts are byte-identical to the previous binary across five repositories. New: the walk reads `.gitignore` as it descends, so generated build output no longer counts as source. Previously `aletheia .` on a tree that had just been built reported Bronze NOT MET, flagging `obj/b__main.ads` and friends for missing SPDX headers - the gate was only valid on a clean checkout, and any CI job running it after a build would fail. Rules are pushed as 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. Implemented: comments, blank lines, `!` negation with last-match-wins, trailing slash, leading-slash anchoring, and `*` 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. .gitignore is kept separate from the existing [ignore] config: [ignore] is a choice made in aletheia's config, whereas .gitignore is the repository's own declaration of what is not part of the published artefact. --- aletheia/src/checks.rs | 271 ++++++++++++++++++++++++++++++------- aletheia/src/config.rs | 300 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 519 insertions(+), 52 deletions(-) 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(); From 2d9df0cd4caf4a48fb12e339891c8f7dcaa88d6b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 21:19:46 +0000 Subject: [PATCH 02/12] feat(scaffold): emit the v2 six-language template set Closes #186. `create-template.sh` scaffolded the retired v1 shape (LICENSE.txt / justfile / flake.nix) and no fresh project could pass Bronze. The template tree is now shared files plus a per-language overlay, and the generator renders six Tier-1 languages: rust, zig, elixir, haskell, ada, agda. Languages banned or outside Tier-1 are rejected with the estate reasoning rather than scaffolded into something that cannot pass. Every language reaches Bronze + Silver (26/26) with no hand edits, builds and tests with its real toolchain, and needs no network: `cargo build --offline`, `zig build`, `mix test`, `cabal build --offline`, `gprbuild`, `agda` all succeed inside `unshare -rn`. Rust here means Rust/Creusot and Ada here means Ada/SPARK, and both are actually verified rather than labelled: * Rust: Creusot 0.14 translates and Why3 discharges every obligation ("Proved (2 files)"), exit 0. `src/impl.rs` is a single source of truth `include!`d by both the zero-dependency main crate and the verification crate, with contracts gated behind `cfg(creusot)`, so the proof cannot drift from the shipped code. `clamp` and `midpoint` carry real preconditions and postconditions, including the exact half-sum identity. * Ada: the core package declares `pragma SPARK_Mode (On)` and gnatprove discharges 35 checks, 100% proved (Z3/Alt-Ergo/CVC5), exit 0. The GPR sets --level=2 and --checks-as-errors; without the latter gnatprove exits 0 even when a check is unproved, which would make the gate decorative. Both `just proof` recipes fail with exit 1 on a deliberately false postcondition, verified in both directions. Also fixed here, each found while proving the templates rather than assumed: * haskell/Justfile used `@@ARGS@@`, an unknown placeholder, so the generator's own unresolved-placeholder guard aborted: `-l haskell` exited 1. Now `{{ARGS}}`, matching the other five. * MOD_ADA was derived by inserting underscores at case boundaries in the camel form, which is wrong for single-letter segments: `g-ada` produced the unit `GAda` while the template ships `g_ada.ads`, and GNAT failed with `file "gada.ads" not found`. Now derived from the project name directly. * zig: the template's own test file failed `zig fmt --check`. * Unpinned setup actions are now pinned to full SHAs resolved from real tags: mlugg/setup-zig, erlef/setup-beam, haskell-actions/setup. New opt-in proof workflows (`.github/workflows/proof.yml`) for rust and ada. They are pinned and match the commands verified by hand, but they have not yet run on a GitHub runner - their first green run is what makes them load-bearing, and the templates do not claim CI-verified proofs until then. --- aletheia/scripts/create-template.sh | 960 ++++++++---------- aletheia/templates/ada/.editorconfig | 19 + .../templates/ada/.github/workflows/ci.yml | 40 + .../templates/ada/.github/workflows/proof.yml | 81 ++ aletheia/templates/ada/.gitignore | 24 + .../ada/.machine_readable/rsr-profile.a2ml | 12 + aletheia/templates/ada/.tool-versions | 3 + aletheia/templates/ada/@@MOD_NAME@@.gpr | 37 + aletheia/templates/ada/Justfile | 50 + aletheia/templates/ada/README.adoc | 118 +++ aletheia/templates/ada/src/@@MOD_NAME@@.adb | 31 + aletheia/templates/ada/src/@@MOD_NAME@@.ads | 50 + aletheia/templates/ada/src/main.adb | 82 ++ aletheia/templates/ada/tests/run_tests.adb | 64 ++ aletheia/templates/ada/tests/tests.gpr | 13 + aletheia/templates/agda/.editorconfig | 19 + .../templates/agda/.github/workflows/ci.yml | 41 + aletheia/templates/agda/.gitignore | 4 + .../agda/.machine_readable/rsr-profile.a2ml | 12 + aletheia/templates/agda/.tool-versions | 2 + .../templates/agda/@@PROJECT_NAME@@.agda-lib | 2 + aletheia/templates/agda/Justfile | 36 + aletheia/templates/agda/README.adoc | 83 ++ .../templates/agda/src/@@MOD_CAMEL@@.agda | 52 + aletheia/templates/agda/src/Properties.agda | 29 + .../bronze-rust/README-template.adoc | 83 -- aletheia/templates/common/.gitattributes | 11 + .../common/.github/workflows/actions.lock | 9 + .../common/.github/workflows/governance.yml | 18 + .../common/.github/workflows/hypatia-scan.yml | 21 + aletheia/templates/common/.well-known/ai.txt | 15 + .../templates/common/.well-known/humans.txt | 13 + .../templates/common/.well-known/security.txt | 9 + aletheia/templates/common/0-AI-MANIFEST.a2ml | 52 + aletheia/templates/common/CHANGELOG.adoc | 19 + .../templates/common/CODE_OF_CONDUCT.adoc | 36 + aletheia/templates/common/CONTRIBUTING.adoc | 43 + aletheia/templates/common/LICENSE | 9 + .../common/LICENSES/CC-BY-SA-4.0.txt | 428 ++++++++ .../templates/common/LICENSES/MPL-2.0.txt | 373 +++++++ aletheia/templates/common/MAINTAINERS.adoc | 29 + aletheia/templates/common/SECURITY.adoc | 33 + aletheia/templates/elixir/.editorconfig | 19 + aletheia/templates/elixir/.formatter.exs | 5 + .../templates/elixir/.github/workflows/ci.yml | 42 + aletheia/templates/elixir/.gitignore | 9 + .../elixir/.machine_readable/rsr-profile.a2ml | 12 + aletheia/templates/elixir/.tool-versions | 3 + aletheia/templates/elixir/Justfile | 37 + aletheia/templates/elixir/README.adoc | 83 ++ aletheia/templates/elixir/lib/@@MOD_NAME@@.ex | 47 + .../templates/elixir/lib/@@MOD_NAME@@/cli.ex | 62 ++ aletheia/templates/elixir/mix.exs | 21 + .../elixir/test/@@MOD_NAME@@_test.exs | 45 + .../templates/elixir/test/test_helper.exs | 2 + aletheia/templates/haskell/.editorconfig | 19 + .../haskell/.github/workflows/ci.yml | 39 + aletheia/templates/haskell/.gitignore | 7 + .../.machine_readable/rsr-profile.a2ml | 12 + aletheia/templates/haskell/.tool-versions | 3 + .../templates/haskell/@@PROJECT_NAME@@.cabal | 44 + aletheia/templates/haskell/Justfile | 35 + aletheia/templates/haskell/README.adoc | 83 ++ aletheia/templates/haskell/app/Main.hs | 51 + aletheia/templates/haskell/cabal.project | 2 + aletheia/templates/haskell/src/Core.hs | 24 + aletheia/templates/haskell/test/Main.hs | 45 + aletheia/templates/rust/.editorconfig | 22 + .../templates/rust/.github/workflows/ci.yml | 51 + .../rust/.github/workflows/proof.yml | 122 +++ aletheia/templates/rust/.gitignore | 23 + .../rust/.machine_readable/rsr-profile.a2ml | 16 + aletheia/templates/rust/.tool-versions | 5 + aletheia/templates/rust/Cargo.toml | 32 + aletheia/templates/rust/Justfile | 69 ++ aletheia/templates/rust/README.adoc | 112 ++ aletheia/templates/rust/src/impl.rs | 47 + aletheia/templates/rust/src/lib.rs | 56 + aletheia/templates/rust/src/main.rs | 68 ++ .../templates/rust/tests/integration_test.rs | 51 + .../templates/rust/verification/Cargo.toml | 21 + .../templates/rust/verification/README.adoc | 125 +++ .../templates/rust/verification/src/lib.rs | 13 + .../templates/rust/verification/why3find.json | 9 + aletheia/templates/zig/.editorconfig | 19 + .../templates/zig/.github/workflows/ci.yml | 41 + aletheia/templates/zig/.gitignore | 5 + .../zig/.machine_readable/rsr-profile.a2ml | 12 + aletheia/templates/zig/.tool-versions | 2 + aletheia/templates/zig/Justfile | 37 + aletheia/templates/zig/README.adoc | 83 ++ aletheia/templates/zig/build.zig | 71 ++ aletheia/templates/zig/src/main.zig | 73 ++ aletheia/templates/zig/src/root.zig | 48 + .../templates/zig/test/integration_test.zig | 37 + aletheia/tests/integration_tests.rs | 384 +++++++ 96 files changed, 4867 insertions(+), 603 deletions(-) create mode 100644 aletheia/templates/ada/.editorconfig create mode 100644 aletheia/templates/ada/.github/workflows/ci.yml create mode 100644 aletheia/templates/ada/.github/workflows/proof.yml create mode 100644 aletheia/templates/ada/.gitignore create mode 100644 aletheia/templates/ada/.machine_readable/rsr-profile.a2ml create mode 100644 aletheia/templates/ada/.tool-versions create mode 100644 aletheia/templates/ada/@@MOD_NAME@@.gpr create mode 100644 aletheia/templates/ada/Justfile create mode 100644 aletheia/templates/ada/README.adoc create mode 100644 aletheia/templates/ada/src/@@MOD_NAME@@.adb create mode 100644 aletheia/templates/ada/src/@@MOD_NAME@@.ads create mode 100644 aletheia/templates/ada/src/main.adb create mode 100644 aletheia/templates/ada/tests/run_tests.adb create mode 100644 aletheia/templates/ada/tests/tests.gpr create mode 100644 aletheia/templates/agda/.editorconfig create mode 100644 aletheia/templates/agda/.github/workflows/ci.yml create mode 100644 aletheia/templates/agda/.gitignore create mode 100644 aletheia/templates/agda/.machine_readable/rsr-profile.a2ml create mode 100644 aletheia/templates/agda/.tool-versions create mode 100644 aletheia/templates/agda/@@PROJECT_NAME@@.agda-lib create mode 100644 aletheia/templates/agda/Justfile create mode 100644 aletheia/templates/agda/README.adoc create mode 100644 aletheia/templates/agda/src/@@MOD_CAMEL@@.agda create mode 100644 aletheia/templates/agda/src/Properties.agda delete mode 100644 aletheia/templates/bronze-rust/README-template.adoc create mode 100644 aletheia/templates/common/.gitattributes create mode 100644 aletheia/templates/common/.github/workflows/actions.lock create mode 100644 aletheia/templates/common/.github/workflows/governance.yml create mode 100644 aletheia/templates/common/.github/workflows/hypatia-scan.yml create mode 100644 aletheia/templates/common/.well-known/ai.txt create mode 100644 aletheia/templates/common/.well-known/humans.txt create mode 100644 aletheia/templates/common/.well-known/security.txt create mode 100644 aletheia/templates/common/0-AI-MANIFEST.a2ml create mode 100644 aletheia/templates/common/CHANGELOG.adoc create mode 100644 aletheia/templates/common/CODE_OF_CONDUCT.adoc create mode 100644 aletheia/templates/common/CONTRIBUTING.adoc create mode 100644 aletheia/templates/common/LICENSE create mode 100644 aletheia/templates/common/LICENSES/CC-BY-SA-4.0.txt create mode 100644 aletheia/templates/common/LICENSES/MPL-2.0.txt create mode 100644 aletheia/templates/common/MAINTAINERS.adoc create mode 100644 aletheia/templates/common/SECURITY.adoc create mode 100644 aletheia/templates/elixir/.editorconfig create mode 100644 aletheia/templates/elixir/.formatter.exs create mode 100644 aletheia/templates/elixir/.github/workflows/ci.yml create mode 100644 aletheia/templates/elixir/.gitignore create mode 100644 aletheia/templates/elixir/.machine_readable/rsr-profile.a2ml create mode 100644 aletheia/templates/elixir/.tool-versions create mode 100644 aletheia/templates/elixir/Justfile create mode 100644 aletheia/templates/elixir/README.adoc create mode 100644 aletheia/templates/elixir/lib/@@MOD_NAME@@.ex create mode 100644 aletheia/templates/elixir/lib/@@MOD_NAME@@/cli.ex create mode 100644 aletheia/templates/elixir/mix.exs create mode 100644 aletheia/templates/elixir/test/@@MOD_NAME@@_test.exs create mode 100644 aletheia/templates/elixir/test/test_helper.exs create mode 100644 aletheia/templates/haskell/.editorconfig create mode 100644 aletheia/templates/haskell/.github/workflows/ci.yml create mode 100644 aletheia/templates/haskell/.gitignore create mode 100644 aletheia/templates/haskell/.machine_readable/rsr-profile.a2ml create mode 100644 aletheia/templates/haskell/.tool-versions create mode 100644 aletheia/templates/haskell/@@PROJECT_NAME@@.cabal create mode 100644 aletheia/templates/haskell/Justfile create mode 100644 aletheia/templates/haskell/README.adoc create mode 100644 aletheia/templates/haskell/app/Main.hs create mode 100644 aletheia/templates/haskell/cabal.project create mode 100644 aletheia/templates/haskell/src/Core.hs create mode 100644 aletheia/templates/haskell/test/Main.hs create mode 100644 aletheia/templates/rust/.editorconfig create mode 100644 aletheia/templates/rust/.github/workflows/ci.yml create mode 100644 aletheia/templates/rust/.github/workflows/proof.yml create mode 100644 aletheia/templates/rust/.gitignore create mode 100644 aletheia/templates/rust/.machine_readable/rsr-profile.a2ml create mode 100644 aletheia/templates/rust/.tool-versions create mode 100644 aletheia/templates/rust/Cargo.toml create mode 100644 aletheia/templates/rust/Justfile create mode 100644 aletheia/templates/rust/README.adoc create mode 100644 aletheia/templates/rust/src/impl.rs create mode 100644 aletheia/templates/rust/src/lib.rs create mode 100644 aletheia/templates/rust/src/main.rs create mode 100644 aletheia/templates/rust/tests/integration_test.rs create mode 100644 aletheia/templates/rust/verification/Cargo.toml create mode 100644 aletheia/templates/rust/verification/README.adoc create mode 100644 aletheia/templates/rust/verification/src/lib.rs create mode 100644 aletheia/templates/rust/verification/why3find.json create mode 100644 aletheia/templates/zig/.editorconfig create mode 100644 aletheia/templates/zig/.github/workflows/ci.yml create mode 100644 aletheia/templates/zig/.gitignore create mode 100644 aletheia/templates/zig/.machine_readable/rsr-profile.a2ml create mode 100644 aletheia/templates/zig/.tool-versions create mode 100644 aletheia/templates/zig/Justfile create mode 100644 aletheia/templates/zig/README.adoc create mode 100644 aletheia/templates/zig/build.zig create mode 100644 aletheia/templates/zig/src/main.zig create mode 100644 aletheia/templates/zig/src/root.zig create mode 100644 aletheia/templates/zig/test/integration_test.zig 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/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..2125c13 --- /dev/null +++ b/aletheia/templates/ada/.github/workflows/proof.yml @@ -0,0 +1,81 @@ +# 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 ships its own Why3 and versions of Alt-Ergo/CVC5, so there is + # nothing else to install and 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 the same command. + - 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..9afc3ea --- /dev/null +++ b/aletheia/templates/rust/.github/workflows/proof.yml @@ -0,0 +1,122 @@ +# 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`. +# +# Every command below was run by hand against this template before being +# written down here; the pins are the ones Creusot declares in +# creusot-deps.opam. It has not yet been executed on a GitHub runner, so treat +# its first green run as the moment it becomes load-bearing. +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: + # Keep these in step with the forks pinned in creusot-deps.opam. A stock + # Why3 cannot even parse the Coma that a given Creusot emits, and a stock + # why3find will not compile against the pinned Why3. + WHY3_PIN: git+https://gitlab.inria.fr/why3/why3.git#c369bc4cdc22d1e714255bb3675a2ce6b7242f19 + WHY3FIND_PIN: git+https://github.com/creusot-rs/why3find.git#0f054b93c86ac7ba20bca7df5d1563a9a4434a30 + +jobs: + creusot: + name: Translate and discharge (Creusot + Why3) + runs-on: ubuntu-24.04 + timeout-minutes: 90 + 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 + + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends \ + opam ocaml z3 cvc5 build-essential pkg-config libgmp-dev + + # Creusot pins its own nightly; read it from the clone rather than + # hard-coding a second copy that can drift. + - name: Clone Creusot + run: git clone --depth 1 https://github.com/creusot-rs/creusot "$RUNNER_TEMP/creusot" + + - 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). Parse it rather than duplicating the + # version here, where it would silently drift. + 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 + 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 pin add -y why3find "$WHY3FIND_PIN" + opam install -y why3 why3find + opam env --switch=creusot --set-switch >> "$GITHUB_ENV" + # The fork must be the one in use; a stock release fails much later, + # with a confusing parse error. + why3 --version + + - name: Install Creusot + run: | + set -euo pipefail + eval "$(opam env --switch=creusot --set-switch)" + cargo install --locked --path "$RUNNER_TEMP/creusot/cargo-creusot" + cargo install --locked --path "$RUNNER_TEMP/creusot/creusot-rustc" + + - name: Point cargo at the local creusot-std + run: cargo creusot config --update + + - name: Detect provers + run: why3 config detect + + # Fails the job if any goal is unproved. Mirrors `just proof`. + - 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(); +} From 138ae976c96b4ef991b4ed36a91992f8fa456a98 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 21:20:04 +0000 Subject: [PATCH 03/12] docs: delivery write-up for #186 and #197 Records what was delivered and, more usefully, what was not: the specification Creusot could not verify and why, the fake gate gnatprove would have given without --checks-as-errors, and the three template defects found only by running the real toolchains. Includes the reproduction and the negative control for the .gitignore fix, the commit split, and the two things deliberately left uncommitted (the uninitialised `absolute-zero` submodule, and the executable bits the sandbox restore dropped). No claims are made for the two proof workflows beyond what has been run: they are pinned, their shell logic was exercised, and they have not yet executed on a GitHub runner. --- DELIVERY-186-197.md | 629 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 629 insertions(+) create mode 100644 DELIVERY-186-197.md diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md new file mode 100644 index 0000000..294961c --- /dev/null +++ b/DELIVERY-186-197.md @@ -0,0 +1,629 @@ +# 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 now ship an + opt-in `.github/workflows/proof.yml`, pinned and matching commands that were run by hand. They + have not yet executed on a GitHub runner, 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 + +Three 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 + + docs: delivery write-up + DELIVERY-186-197.md +``` + +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. + +--- + +## 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.** Rust and Ada use `midpoint` (because + Creusot forces a provable formulation); Zig, Elixir, Haskell and Agda still use `meanFloor`. All + six pass, so this is coherence rather than correctness — worth a decision before the set is + published as canon. + +3. **`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`. + +That location is deliberate. The first pass kept the toolchains under `/home/user/build/`, which is +excluded from the workspace snapshot; between sessions the directory was reclaimed and the whole +toolchain went with it. Reinstalling outside `/home/user` means the install survives, and — more to +the point — that a toolchain can no longer be lost in a way that looks like a repo problem. + +`gnatprove` is not currently installed in this sandbox; the Ada proof evidence above was produced +with `gnatprove 13.2.0` from `alire-project/GNAT-FSF-builds`, and the CI workflow installs that same +release asset 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 proof workflows are valid and their shell logic was exercised +python3 -c "import yaml; yaml.safe_load(open('.../proof.yml'))" # valid YAML for both +# (steps simulated with stub rustup/cargo; channel parses to nightly-2026-08-03; +# the apt package list and opam commands ran for real) +``` From 599d6bea26d76a845578e4ed9c1dba90b8772a84 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 21:21:05 +0000 Subject: [PATCH 04/12] docs: explain why the six templates do not share one sample API The divergence between `midpoint` and `meanFloor` follows the toolchains, not taste: Creusot has no bitvector theory and SPARK's provers cannot discharge the identity, so the proof-carrying templates use the formulation that can be proved. Unifying would add an unnecessary precondition to three languages. Kept, with the reasoning recorded, rather than changed for symmetry. --- DELIVERY-186-197.md | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md index 294961c..510cf09 100644 --- a/DELIVERY-186-197.md +++ b/DELIVERY-186-197.md @@ -564,10 +564,19 @@ Two things were deliberately left uncommitted: "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.** Rust and Ada use `midpoint` (because - Creusot forces a provable formulation); Zig, Elixir, Haskell and Agda still use `meanFloor`. All - six pass, so this is coherence rather than correctness — worth a decision before the set is - published as canon. +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. **`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. From f28ad4c1af26e79c6164990de1d609780fa75c01 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 22:43:58 +0000 Subject: [PATCH 05/12] fix(ci): the Rust proof workflow could not have worked as written Found by rebuilding the Creusot toolchain from scratch, which meant running the workflow's own commands by hand. `cargo creusot` does not look for `creusot-rustc` on PATH - it wants it under $XDG_DATA_HOME/creusot/toolchains//bin/, alongside the Creusot prelude installed as a why3find package and a generated why3.conf. Installing the two binaries and running `cargo creusot config --update` leaves all three missing, and the job dies with: creusot-rustc not found (expected at ".../toolchains/nightly-2026-08-03/bin/creusot-rustc") The workflow now runs Creusot's own installer for those pieces (prelude, why3-conf, creusot-rustc, cargo-creusot, cargo-creusot-config), and checks the result with `cargo creusot version` before attempting a proof. Every other command in the toolchain half was verified to run as written: the apt list, the clone, the rustup toolchain install, opam init and switch, and both opam pins for Creusot's why3/why3find forks. Reading the channel out of Creusot's `rust-toolchain` is now tested too - it is TOML without the .toml extension, so `head -1` silently yields "[toolchain]" and installs the wrong toolchain. Also records the Ada re-verification (35/35 checks, negative control exits 1) and why the first negative-control attempt looked like a false gate when it was a stale PIPESTATUS in my own shell. --- DELIVERY-186-197.md | 71 +++++++++++++++++-- .../rust/.github/workflows/proof.yml | 34 ++++++--- 2 files changed, 93 insertions(+), 12 deletions(-) diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md index 510cf09..1aa30fe 100644 --- a/DELIVERY-186-197.md +++ b/DELIVERY-186-197.md @@ -178,10 +178,10 @@ estate root `just check` exit 0; `just self-verify` 26/26. `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 now ship an - opt-in `.github/workflows/proof.yml`, pinned and matching commands that were run by hand. They - have not yet executed on a GitHub runner, so the templates still do not claim CI-verified - proofs — the first green run is what makes them load-bearing. +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. --- @@ -558,6 +558,69 @@ Two things were deliberately left uncommitted: --- +## Proof workflows: what "not yet executed" was hiding + +When the two `.github/workflows/proof.yml` files went in, they were flagged as unvalidated. They +have been exercised since, because the sandbox lost the Creusot toolchain between sessions and +rebuilding it meant running the workflow's own commands by hand. That turned out to be worth the +trouble. + +**What held up.** Every command in the toolchain half executed exactly as written and succeeded: +the apt package list, `git clone --depth 1`, reading the channel out of Creusot's `rust-toolchain` +file, `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 only correct because it was tested. Creusot's `rust-toolchain` file is TOML — +`channel = "nightly-2026-08-03"` — but without the `.toml` extension, so the obvious first parse +(`head -1`) yields `[toolchain]` and the whole job installs the wrong toolchain. The workflow now +parses the `channel` key and fails loudly if it cannot. + +**What was wrong.** The Rust workflow installed the two binaries and stopped. That is not enough, +because `cargo creusot` does not look for `creusot-rustc` on `PATH`: + +``` +creusot-rustc not found (expected at + "/home/user/.local/share/creusot/toolchains/nightly-2026-08-03/bin/creusot-rustc"). +You should reinstall Creusot. +``` + +It wants its own data-dir layout: the binary under `toolchains//bin/`, the Creusot prelude +installed as a why3find package, and a generated `why3.conf`. Installing the binaries by hand +leaves all three missing. The workflow now runs Creusot's own installer for exactly those pieces: + +```yaml +cargo run --quiet --release --bin creusot-install -- \ + --external z3 --external cvc5 \ + prelude why3-conf creusot-rustc cargo-creusot cargo-creusot-config +``` + +A second gap: `creusot-rustc` **must** be built on Creusot's pinned nightly. On stable it fails to +compile (`why3` binding errors). The workflow already set `rustup default "$channel"` before the +installs, so it was right — but only a real run shows that it needed to be. + +Neither of these would have surfaced from reading the file. That is the argument for the caveat +that was written on them. + +**Ada.** The `gnatprove` release asset the Ada workflow installs was downloaded and its SHA-256 +checked against the value hard-coded in the workflow (`28fc3583…f4017` — matched), and the proof +was re-run end-to-end on the freshly generated template: **35 checks, 100% proved, exit 0**, with +the negative control failing 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 +``` + +The first attempt at that negative control reported exit 0 and looked alarming. It was a stale +`PIPESTATUS` in the shell I typed, not a false gate: rerun from a clean proof state, with the exit +code captured directly, it fails correctly. Worth recording, because "the gate looked green when it +should not have" is the one result that must never be waved away. + +--- + ## Findings I did not fix, for your judgement 1. ~~**`aletheia` does not honour `.gitignore` when scanning.**~~ **Fixed in this pass** — see diff --git a/aletheia/templates/rust/.github/workflows/proof.yml b/aletheia/templates/rust/.github/workflows/proof.yml index 9afc3ea..dfccf65 100644 --- a/aletheia/templates/rust/.github/workflows/proof.yml +++ b/aletheia/templates/rust/.github/workflows/proof.yml @@ -99,18 +99,36 @@ jobs: # with a confusing parse error. why3 --version - - name: Install Creusot + # `cargo creusot` does not just want the two binaries on PATH. It looks + # for creusot-rustc inside its own data dir + # ($XDG_DATA_HOME/creusot/toolchains//bin) and for the Creusot + # prelude as a why3find package. Running the project's own installer is + # the supported way to lay all of that out; installing the binaries by + # hand leaves `cargo creusot` failing with "creusot-rustc not found + # (expected at ...)". + # + # `--external z3 --external cvc5` uses the apt solvers rather than + # downloading Creusot's pinned copies. This step compiles Creusot for the + # install prefix, so it is the slowest part of the job. + - name: Install Creusot (binaries, prelude, why3 config) + working-directory: ${{ runner.temp }}/creusot run: | set -euo pipefail eval "$(opam env --switch=creusot --set-switch)" - cargo install --locked --path "$RUNNER_TEMP/creusot/cargo-creusot" - cargo install --locked --path "$RUNNER_TEMP/creusot/creusot-rustc" + cargo run --quiet --release --bin creusot-install -- \ + --external z3 --external cvc5 \ + prelude why3-conf creusot-rustc cargo-creusot cargo-creusot-config - - name: Point cargo at the local creusot-std - run: cargo creusot config --update - - - name: Detect provers - run: why3 config detect + # Verifies the pieces cargo-creusot resolves at runtime, rather than + # assuming the installer worked. Empty output for a prover here means the + # proof step will fail confusingly, so check first. + - name: Check the Creusot install + run: | + set -euo pipefail + eval "$(opam env --switch=creusot --set-switch)" + cargo creusot version + why3 --version + command -v z3 cvc5 # Fails the job if any goal is unproved. Mirrors `just proof`. - name: Prove From 3bfd4c8e01049fe469d282204aa70d2acdc57655 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 22:56:07 +0000 Subject: [PATCH 06/12] fix(ci): finish the Creusot install, and stop hard-coding the Why3 pin Second pass on the Rust proof workflow, after actually building the toolchain on a clean box and driving `just proof` to a green run. Three more things it was missing: 1. The provers. Creusot's why3.conf names tools by bare name and why3 is run with the data dir's bin/ first on PATH, so alt-ergo/cvc4 being absent is a hard failure at the first prove. The `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/cvc5 is a different build behind the same driver name. `cargo creusot version` now resolves all four, and the job asserts it does. 2. why3 and why3find in the data dir. cargo-creusot resolves them as $XDG_DATA_HOME/creusot/bin/why3[find], not from PATH. The installer has a `why3` component, but it builds a second opam switch from creusot-deps.opam inside the data dir, which pulls in the GTK why3 IDE; its last act is to symlink those two binaries, so do the same from the switch we already have. 3. Pins derived, not duplicated. The hard-coded why3 commit went stale - the checkout now declares a different one - and a workflow that silently changes toolchain under a passing build is not a gate. Creusot itself is pinned (CREUSOT_REV) and both forks are read out of that revision's creusot-deps.opam, failing loudly if the parse comes up empty. Verified by running the whole thing here: `just proof` reports "Proved (2 files)" with why3 pinned to the same commit the workflow will use, and a planted false postcondition fails the gate with "Goal Coma.vc_midpoint: x (4/5) / 1 unproved file" and exit 1. --- .../rust/.github/workflows/proof.yml | 128 ++++++++++++------ 1 file changed, 86 insertions(+), 42 deletions(-) diff --git a/aletheia/templates/rust/.github/workflows/proof.yml b/aletheia/templates/rust/.github/workflows/proof.yml index dfccf65..b02e49d 100644 --- a/aletheia/templates/rust/.github/workflows/proof.yml +++ b/aletheia/templates/rust/.github/workflows/proof.yml @@ -6,10 +6,11 @@ # This is a real gate — `cargo creusot` exits non-zero when any obligation is # unproved. It is deliberately *not* part of `just check`. # -# Every command below was run by hand against this template before being -# written down here; the pins are the ones Creusot declares in -# creusot-deps.opam. It has not yet been executed on a GitHub runner, so treat -# its first green run as the moment it becomes load-bearing. +# 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: @@ -40,17 +41,18 @@ permissions: contents: read env: - # Keep these in step with the forks pinned in creusot-deps.opam. A stock - # Why3 cannot even parse the Coma that a given Creusot emits, and a stock - # why3find will not compile against the pinned Why3. - WHY3_PIN: git+https://gitlab.inria.fr/why3/why3.git#c369bc4cdc22d1e714255bb3675a2ce6b7242f19 - WHY3FIND_PIN: git+https://github.com/creusot-rs/why3find.git#0f054b93c86ac7ba20bca7df5d1563a9a4434a30 + # 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: 90 + 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 @@ -58,23 +60,36 @@ jobs: - 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 z3 cvc5 build-essential pkg-config libgmp-dev + opam ocaml build-essential pkg-config libgmp-dev zlib1g-dev autoconf curl - # Creusot pins its own nightly; read it from the clone rather than - # hard-coding a second copy that can drift. - - name: Clone Creusot - run: git clone --depth 1 https://github.com/creusot-rs/creusot "$RUNNER_TEMP/creusot" + - 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). Parse it rather than duplicating the - # version here, where it would silently drift. + # 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 @@ -88,49 +103,78 @@ jobs: - 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 why3 why3find - opam env --switch=creusot --set-switch >> "$GITHUB_ENV" - # The fork must be the one in use; a stock release fails much later, - # with a confusing parse error. + opam install -y why3find why3 --version + why3find --version + opam env --switch=creusot --set-switch >> "$GITHUB_ENV" - # `cargo creusot` does not just want the two binaries on PATH. It looks - # for creusot-rustc inside its own data dir - # ($XDG_DATA_HOME/creusot/toolchains//bin) and for the Creusot - # prelude as a why3find package. Running the project's own installer is - # the supported way to lay all of that out; installing the binaries by - # hand leaves `cargo creusot` failing with "creusot-rustc not found - # (expected at ...)". - # - # `--external z3 --external cvc5` uses the apt solvers rather than - # downloading Creusot's pinned copies. This step compiles Creusot for the - # install prefix, so it is the slowest part of the job. - - name: Install Creusot (binaries, prelude, why3 config) + # `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 -- \ - --external z3 --external cvc5 \ - prelude why3-conf creusot-rustc cargo-creusot cargo-creusot-config + prelude why3-conf provers creusot-rustc cargo-creusot cargo-creusot-config - # Verifies the pieces cargo-creusot resolves at runtime, rather than - # assuming the installer worked. Empty output for a prover here means the - # proof step will fail confusingly, so check first. + # 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 - why3 --version - command -v z3 cvc5 + 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`. + # 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 From 27a280aba95cd4e8140e7cba059e461d3948e345 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 22:57:09 +0000 Subject: [PATCH 07/12] docs: record what running the proof workflows actually found The two proof workflows shipped with a caveat that they had never been executed. Rebuilding the Creusot toolchain from nothing to exercise them turned up three defects in the Rust one, all now fixed: creusot-rustc installed where cargo-creusot looks, the provers and why3/why3find in the data dir, and the Why3 pin derived from creusot-deps.opam instead of hard-coded (the hard-coded one had already gone stale). Also writes down two results that matter more than the happy path: the negative control on a fresh tree (Goal Coma.vc_midpoint: x (4/5), exit 1), and the one time it wrongly reported "Proved (2 files)" on a false obligation - reproduced deliberately, traced to a tree copied along with its verif/ and target/, and neutralised by the templates' already-ignoring those paths. The caveat that neither workflow has run on a GitHub runner stays. --- DELIVERY-186-197.md | 180 +++++++++++++++++++++++++++++++++----------- 1 file changed, 135 insertions(+), 45 deletions(-) diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md index 1aa30fe..8bf6fe0 100644 --- a/DELIVERY-186-197.md +++ b/DELIVERY-186-197.md @@ -531,7 +531,7 @@ rule is still audited. ## Commits -Three commits, split so each is coherent and individually green when checked out. `#197` and the +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. @@ -543,10 +543,20 @@ rather than a fabricated split. aletheia/templates/**, aletheia/scripts/create-template.sh, aletheia/tests/integration_tests.rs - docs: delivery write-up +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 @@ -560,52 +570,99 @@ Two things were deliberately left uncommitted: ## Proof workflows: what "not yet executed" was hiding -When the two `.github/workflows/proof.yml` files went in, they were flagged as unvalidated. They -have been exercised since, because the sandbox lost the Creusot toolchain between sessions and -rebuilding it meant running the workflow's own commands by hand. That turned out to be worth the -trouble. +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 held up.** Every command in the toolchain half executed exactly as written and succeeded: -the apt package list, `git clone --depth 1`, reading the channel out of Creusot's `rust-toolchain` -file, `rustup toolchain install --component rustc-dev,llvm-tools`, `opam init --bare +**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 only correct because it was tested. Creusot's `rust-toolchain` file is TOML — -`channel = "nightly-2026-08-03"` — but without the `.toml` extension, so the obvious first parse -(`head -1`) yields `[toolchain]` and the whole job installs the wrong toolchain. The workflow now -parses the `channel` key and fails loudly if it cannot. +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) + ``` -**What was wrong.** The Rust workflow installed the two binaries and stopped. That is not enough, -because `cargo creusot` does not look for `creusot-rustc` on `PATH`: + 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: ``` -creusot-rustc not found (expected at - "/home/user/.local/share/creusot/toolchains/nightly-2026-08-03/bin/creusot-rustc"). -You should reinstall Creusot. +$ just proof +Proved (2 files) ✔ +exit 0 ``` -It wants its own data-dir layout: the binary under `toolchains//bin/`, the Creusot prelude -installed as a why3find package, and a generated `why3.conf`. Installing the binaries by hand -leaves all three missing. The workflow now runs Creusot's own installer for exactly those pieces: +with Why3 pinned to the same commit the workflow will use. The negative control — a false +postcondition, `result@ == (a@ + b@) / 2 + 1` — gives: -```yaml -cargo run --quiet --release --bin creusot-install -- \ - --external z3 --external cvc5 \ - prelude why3-conf creusot-rustc cargo-creusot cargo-creusot-config +``` +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 second gap: `creusot-rustc` **must** be built on Creusot's pinned nightly. On stable it fails to -compile (`why3` binding errors). The workflow already set `rustup default "$channel"` before the -installs, so it was right — but only a real run shows that it needed to be. +**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. -Neither of these would have surfaced from reading the file. That is the argument for the caveat -that was written on them. +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). -**Ada.** The `gnatprove` release asset the Ada workflow installs was downloaded and its SHA-256 -checked against the value hard-coded in the workflow (`28fc3583…f4017` — matched), and the proof -was re-run end-to-end on the freshly generated template: **35 checks, 100% proved, exit 0**, with -the negative control failing as it should: +**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, 100% proved, exit 0**. The negative control fails as it should: ``` $ just proof # false postcondition: Clamp'Result in Lo .. Hi - 1 @@ -614,10 +671,22 @@ gnatprove: unproved check messages considered as errors exit 1 ``` -The first attempt at that negative control reported exit 0 and looked alarming. It was a stale -`PIPESTATUS` in the shell I typed, not a false gate: rerun from a clean proof state, with the exit -code captured directly, it fails correctly. Worth recording, because "the gate looked green when it -should not have" is the one result that must never be waved away. +**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. + +**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. + --- @@ -655,10 +724,18 @@ excluded from the workspace snapshot; between sessions the directory was reclaim toolchain went with it. Reinstalling outside `/home/user` means the install survives, and — more to the point — that a toolchain can no longer be lost in a way that looks like a repo problem. -`gnatprove` is not currently installed in this sandbox; the Ada proof evidence above was produced -with `gnatprove 13.2.0` from `alire-project/GNAT-FSF-builds`, and the CI workflow installs that same -release asset by URL **and verifies its SHA-256** (`28fc3583…f4017`, checked against the real -download). +`gnatprove` lives at `/usr/local/gnatprove` (13.2.0-1, from `alire-project/GNAT-FSF-builds` — it is +not an Alire toolchain component and `alr install` does not exist, so the release archive is the +only route). The CI workflow installs that same asset by URL **and verifies its SHA-256** +(`28fc3583…f4017`, checked against the real download). + +Creusot is the one that needs care. It is at `/usr/local/creusot` (source) with the pinned nightly +in `/usr/local/rustup`, an opam switch at `/usr/local/opam`, and its runtime layout under +`/usr/local/share/creusot` (`bin/{why3,why3find,alt-ergo,z3,cvc4,cvc5}`, `toolchains//`, +`share/why3find/packages/creusot`). That last part matters: `XDG_DATA_HOME` decides where +`cargo-creusot` looks, and the default (`~/.local/share`) is *excluded from this sandbox's workspace +snapshot*, so a toolchain installed there evaporates between sessions. Pointing `XDG_DATA_HOME` at +`/usr/local/share` makes it survive. ## Follow-on verification log @@ -694,8 +771,21 @@ 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 proof workflows are valid and their shell logic was exercised +# 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 proof workflows: commands run for real, not simulated python3 -c "import yaml; yaml.safe_load(open('.../proof.yml'))" # valid YAML for both -# (steps simulated with stub rustup/cargo; channel parses to nightly-2026-08-03; -# the apt package list and opam commands ran for real) +# 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 ``` From 48a887a3cfac58ab07dd59ca3a5196d344216cbc Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 22:57:58 +0000 Subject: [PATCH 08/12] fix(ci): the Ada proof job never installed a compiler Same species of defect as the Rust one: the workflow assumed a tool the runner does not have. gnatprove is a frontend, not a toolchain - the release archive the job downloads contains a single binary, no compiler, no gprbuild - so the job would have died at `gprbuild --version` in the step after the install. ci.yml already installs `gnat gprbuild` and has done since the template was written; proof.yml, which was added later, did not, and reading the two files side by side is what shows it. --- .../templates/ada/.github/workflows/proof.yml | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/aletheia/templates/ada/.github/workflows/proof.yml b/aletheia/templates/ada/.github/workflows/proof.yml index 2125c13..eb09412 100644 --- a/aletheia/templates/ada/.github/workflows/proof.yml +++ b/aletheia/templates/ada/.github/workflows/proof.yml @@ -46,9 +46,18 @@ jobs: - 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 - # nothing else to install and no solver version to drift. Pinned by URL - # and checksum: this artefact is a release asset, not a mutable tag. + # 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 @@ -65,7 +74,9 @@ jobs: 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 the same command. + # 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 From 92f5e4585d6f84d4a6a0457576bf691e0e41cc32 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 22:58:43 +0000 Subject: [PATCH 09/12] docs: the Ada proof job had the same kind of hole as the Rust one Four defects across the two workflows now: three in the Rust job (creusot-rustc location, missing provers/why3, stale hard-coded pin) and one in the Ada job (GNAT and gprbuild never installed). The Ada proof is re-run on a regenerated template: 35 checks proved, 0 unproved, exit 0. --- DELIVERY-186-197.md | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md index 8bf6fe0..eb3f375 100644 --- a/DELIVERY-186-197.md +++ b/DELIVERY-186-197.md @@ -659,10 +659,18 @@ construction. Locally, the lesson is to treat proof artefacts as build output: d 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, 100% proved, exit 0**. The negative control fails as it should: +**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 @@ -783,9 +791,14 @@ cd g-rust && just proof # 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 ``` From 7ef549c4c63b6c1cfc7bb83062bb7f0c6167a002 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 23 Sep 2026 22:59:32 +0000 Subject: [PATCH 10/12] docs: note the Agda pin that ci.yml does not honour Auditing every workflow for the defect just found in the Ada and Rust proof jobs (a step using a tool nothing installed) turned up one honest gap rather than a bug: agda/ci.yml installs the distro's Agda while .tool-versions pins 2.6.4.3. They coincide on Debian 13, which is not evidence about any other base image. --- DELIVERY-186-197.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md index eb3f375..e83004a 100644 --- a/DELIVERY-186-197.md +++ b/DELIVERY-186-197.md @@ -718,7 +718,14 @@ weaker claim than a green run, and the templates are not claiming the stronger o 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. **`aletheia/LICENSE` still says PMPL-1.0-or-later** while its sources say MPL-2.0. Carried over +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 From 23798e8e964e1d9a93fba44e546205937e4e9e72 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 24 Sep 2026 00:35:45 +0000 Subject: [PATCH 11/12] docs: correct the claim that toolchains survive outside the workspace The section said installing to /usr/local meant the toolchain outlived the session, unlike /home/user/build. The sandbox then reclaimed everything outside the workspace - Rust, Cargo, just, Zig, opam, Creusot, gnatprove - which is a clean refutation. No location here is durable. The rebuild recipes are unchanged in substance and are the reason this is survivable rather than fatal; what changes is that they must be treated as re-runnable, not as a one-off. Also records the two settings that are easy to lose and hard to diagnose: XDG_DATA_HOME decides where cargo-creusot looks for its tools (why3, why3find, provers and creusot-rustc itself), and both creusot-rustc and cargo creusot must run under Creusot's pinned nightly. --- DELIVERY-186-197.md | 50 ++++++++++++++++++++++++++++----------------- 1 file changed, 31 insertions(+), 19 deletions(-) diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md index e83004a..e7b1f99 100644 --- a/DELIVERY-186-197.md +++ b/DELIVERY-186-197.md @@ -732,25 +732,37 @@ weaker claim than a green run, and the templates are not claiming the stronger o 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`. - -That location is deliberate. The first pass kept the toolchains under `/home/user/build/`, which is -excluded from the workspace snapshot; between sessions the directory was reclaimed and the whole -toolchain went with it. Reinstalling outside `/home/user` means the install survives, and — more to -the point — that a toolchain can no longer be lost in a way that looks like a repo problem. - -`gnatprove` lives at `/usr/local/gnatprove` (13.2.0-1, from `alire-project/GNAT-FSF-builds` — it is -not an Alire toolchain component and `alr install` does not exist, so the release archive is the -only route). The CI workflow installs that same asset by URL **and verifies its SHA-256** -(`28fc3583…f4017`, checked against the real download). - -Creusot is the one that needs care. It is at `/usr/local/creusot` (source) with the pinned nightly -in `/usr/local/rustup`, an opam switch at `/usr/local/opam`, and its runtime layout under -`/usr/local/share/creusot` (`bin/{why3,why3find,alt-ergo,z3,cvc4,cvc5}`, `toolchains//`, -`share/why3find/packages/creusot`). That last part matters: `XDG_DATA_HOME` decides where -`cargo-creusot` looks, and the default (`~/.local/share`) is *excluded from this sandbox's workspace -snapshot*, so a toolchain installed there evaporates between sessions. Pointing `XDG_DATA_HOME` at -`/usr/local/share` makes it survive. +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 From e4c7a115fc6261630e103f97c310bc4aef41a83b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 24 Sep 2026 00:56:29 +0000 Subject: [PATCH 12/12] docs: re-verify both proofs on the rebased tree, through the generator A rebase is a rewrite, so the rebased commits were not assumed to be equivalent to the tested ones. The toolchain was rebuilt from nothing and both proofs were re-run through the generator on the rebased tree: rust positive Proved (2 files), exit 0 rust negative false postcondition, exit 1 ada positive 35/35 checks proved, exit 0 ada negative false postcondition, exit 1 and the suite: 135 tests, fmt and clippy clean, `just check` exit 0, `just self-verify` 26/26. Two toolchain lessons recorded, both of which cost time here: cargo creusot resolves creusot-rustc inside its data dir and refuses to run without it even when the binary is on PATH, and `--component a b` makes rustup read `b` as a toolchain name rather than a second component. --- DELIVERY-186-197.md | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/DELIVERY-186-197.md b/DELIVERY-186-197.md index e7b1f99..584ed41 100644 --- a/DELIVERY-186-197.md +++ b/DELIVERY-186-197.md @@ -691,6 +691,36 @@ cost time here and will cost time for anyone else running these proofs in a smal 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.