From bb151f928db14481a3542ea8b984e1bf19253e68 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:28:17 +0100 Subject: [PATCH 1/3] docs: correct two files that misstate the code they describe MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROOF-NEEDS.md claimed "1 `Admitted` in proofs/coq/lambda/LambdaCNO.v". Measured against absolute-zero @87902bb7: there are ZERO `Admitted` anywhere. `y_not_cno` is a KEPT AXIOM with a written rationale (LambdaCNO.v:388-399). The old wording was wrong in both directions — it overstated the incompleteness and understated the trusted base by a factor of 23. There are 23 `Axiom` declarations across 6 .v files, already classified by an in-source AXIOM AUDIT (end of physics/LandauerDerivation.v), which this file now points at as the authoritative record instead of duplicating it. Operationally the distinction matters: an `Axiom` PASSES a "no sorry / no Admitted" gate silently, so counting only `Admitted` measures the wrong thing. Promoted to the top of "What Needs Proving": the audit's own SOUNDNESS WARNINGS — `prob_nonneg`, `prob_normalized` (false over unconstrained function-type distributions) and `shannon_entropy_maximum` (stated inequality is backwards). All three are currently unused, which makes them cheap to fix now and expensive to discover later. Removed `y_not_cno` from that list: the in-source rationale explains it needs an invariant closed under the full reduction congruence, or a coinductive argument — out of scope, not "concrete and closable". aletheia/CLAUDE.md said all logic lives in src/main.rs (~950 lines) and "don't split into modules unless >1000 lines". It has been 5 modules / 995 lines for a while, with main.rs at 121. That instruction would have told the next agent to undo the existing structure. Also corrected: 23 workflows -> 16, flake.nix listed but absent, 18 integration tests -> 32. Added to aletheia/CLAUDE.md a prominent warning that those 16 nested workflows have NEVER run (Actions reads .github/workflows/ at the repo root only) — the fault that let this crate stay uncompilable for a month — and a note on the #124/#125 gap explaining why the integration suite is a UI contract, not a spec. Co-Authored-By: Claude Opus 5 --- PROOF-NEEDS.md | 56 ++++++++++++++++++++++++++++---- aletheia/CLAUDE.md | 81 +++++++++++++++++++++++++++++++++++++--------- 2 files changed, 115 insertions(+), 22 deletions(-) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 68c5948..4ce5099 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -6,29 +6,73 @@ Copyright (c) Jonathan D.A. Jewell ## Current State +*Re-measured 2026-07-27 against the `absolute-zero` submodule at `87902bb7`.* + - **src/abi/*.idr**: NO -- **Dangerous patterns**: 1 `Admitted` in `proofs/coq/lambda/LambdaCNO.v` (y_not_cno theorem) +- **`Admitted` count**: **0** (`grep -rn Admitted absolute-zero --include=*.v`) +- **Trusted base**: **23 `Axiom` declarations across 6 `.v` files**, each classified + in-source. See the **AXIOM AUDIT** block at the end of + `proofs/coq/physics/LandauerDerivation.v` — that audit, not this file, is the + authoritative record. - **LOC**: ~22,700 (Rust + Coq) - **ABI layer**: Missing -- **Existing proofs**: Coq proofs for lambda CNO (3/4 proven), quantum mechanics exactness +- **Existing proofs**: Coq proofs for lambda CNO, Landauer derivation chain, + quantum mechanics exactness + +> **Correction (2026-07-27).** This file previously claimed *"1 `Admitted` in +> `proofs/coq/lambda/LambdaCNO.v` (y_not_cno)"*. There are **zero** `Admitted` +> anywhere. `y_not_cno` is a **KEPT AXIOM** — a declared trust assumption with a +> written rationale (`LambdaCNO.v:388-399`), not an unproven hole. The old wording was +> wrong in both directions: it overstated the incompleteness *and* understated the +> trusted base by a factor of 23. +> +> The distinction matters operationally: an `Axiom` **passes** a "no `sorry` / +> no `Admitted`" gate silently, so counting only `Admitted` measures the wrong thing. +> Any proof gate for this repo must scan for `Axiom` too. + +### Axiom classification (summarised from the in-source audit) + +| Class | Count | Meaning | +|---|---|---| +| METAL-BOUNDARY | 6 | genuine empirical physics, not derivable (k_B, temperature, Second Law, isothermal work bound, Landauer lower bound, reversible ⇒ zero dissipation) | +| SPECIFICATION | 4 | sound, but not dischargeable while `shannon_entropy` / `product_dist` stay opaque | +| NOT-YET-DISCHARGED (class A) | 2 | `cno_preserves_shannon_entropy`, `cno_zero_energy_dissipation_derived` | +| SOUNDNESS WARNINGS | 3 | **false as stated**, currently **unused** — see below | + +The audit is notably self-critical: it records that +`cno_zero_energy_dissipation_derived` is an axiom **despite its `_derived` name**, and +that the triage docs' "DISCHARGE" marks on it and on `reversible_zero_dissipation` are +**inaccurate**. Both are kept honestly rather than fake-derived. ## What Needs Proving | Component | What | Why | |-----------|------|-----| -| Y combinator non-CNO (y_not_cno) | Close the remaining Admitted proof | 1 of 4 lambda CNO theorems is incomplete | +| **Unsound-but-unused axioms** | Fix or delete `prob_nonneg`, `prob_normalized` (false over unconstrained function-type distributions — need a bundled distribution type) and `shannon_entropy_maximum` (**stated inequality is backwards** — asserts uniform *minimises* entropy) | They are false. Unused today, so harmless today; the moment anything cites one, it proves anything. **Highest priority.** | +| `cno_preserves_shannon_entropy` | Discharge, or accept as a stated postulate | class A — carrier/quotient issue | +| `cno_zero_energy_dissipation_derived` | Rename, or supply `internal_energy` CNO-invariance | `internal_energy` is an opaque `Parameter` with no preservation law, so this cannot be a pure derivation | | Absolute-zero brainfuck interpreter | Interpreter preserves CNO properties | Claims of computational zero need formal backing | -| Absolute-zero whitespace interpreter | Same as brainfuck — CNO preservation | Both esoteric interpreters need same guarantee | +| Absolute-zero whitespace interpreter | Same as brainfuck — CNO preservation | Both esoteric interpreters need the same guarantee | | Aletheia verification checks | Verification pipeline produces sound results | Rhodibot extraction depends on correct checks | | Quantum mechanics proofs | Extend QuantumMechanicsExact.v coverage | Existing proofs are partial | +**Not on this list: `y_not_cno`.** It is not a "concrete, closable proof obligation". +The in-source rationale explains why: a rigorous proof must rule out reaching the +argument under *every* interleaving of `beta_reduce` (which permits reduction under +binders and on either side of an application), requiring an invariant closed under the +full reduction congruence, or a coinductive / step-indexed non-termination argument. +Genuinely out of scope, not merely tedious. + ## Recommended Prover -**Coq** — Existing proof infrastructure is in Coq. The `y_not_cno` Admitted needs to be closed in Coq. Aletheia (Rust) verification would benefit from an **Idris2** ABI layer. +**Coq** — the existing proof infrastructure is in Coq. Aletheia (Rust) verification +would benefit from an **Idris2** ABI layer. ## Priority -**MEDIUM** — Has existing proof infrastructure with one known gap. The Admitted y_not_cno is a concrete, closable proof obligation. Aletheia verification correctness is more important long-term. +**MEDIUM** — the proof infrastructure is real and its trusted base is honestly +documented. The one genuinely urgent item is the three **unsound** axioms: they are +currently unused, so this is cheap to fix now and expensive to discover later. ## Template ABI Cleanup (2026-03-29) diff --git a/aletheia/CLAUDE.md b/aletheia/CLAUDE.md index dd378d6..e105977 100644 --- a/aletheia/CLAUDE.md +++ b/aletheia/CLAUDE.md @@ -49,15 +49,24 @@ Aletheia maintains **zero unsafe blocks** for RSR compliance. ## Architecture Principles -### Single-File Implementation +### Module Layout (updated 2026-07-27 — this section was stale) -All core logic lives in `src/main.rs` (~950 lines). This design is intentional: +> **This file used to say "all core logic lives in `src/main.rs` (~950 lines)" and +> "don't split into modules unless >1000 lines". Both were out of date.** The crate has +> been split for some time. Measured 2026-07-27: -**Benefits**: -- Easy to audit (one file to read) -- Minimal complexity -- Clear code flow -- No hidden abstractions +| File | Lines | Contents | +|---|---|---| +| `src/main.rs` | 121 | CLI entry, arg parsing, `verify_repository`, exit policy | +| `src/checks.rs` | 316 | `check_documentation`, `check_spdx_headers`, `check_workflow_pins`, `check_path_security`, glob matching | +| `src/config.rs` | 243 | `.aletheia.toml` loading, hand-rolled TOML parse | +| `src/output.rs` | 226 | human / JSON / SARIF report printing, date+time formatting | +| `src/types.rs` | 89 | `ComplianceLevel`, `CheckResult`, `ComplianceReport`, … | +| **total** | **995** | | + +The single-file rationale still applies *in spirit* — prefer few, auditable files over +deep abstraction — but do not "restore" the single-file layout, and do not treat 1000 +lines as a threshold that has not yet been crossed. **When to add more files**: - Integration tests in `tests/` directory @@ -65,10 +74,31 @@ All core logic lives in `src/main.rs` (~950 lines). This design is intentional: - Documentation in `docs/` directory **When NOT to add files**: -- Don't split into modules unless >1000 lines - Don't create abstractions prematurely - Don't add utility files for one-off functions +### Known gap: the CLI is unfinished (issues #124 / #125) + +`main.rs` parses only `` plus `--json` / `--sarif`, and wires **three** +checks. `tests/integration_tests.rs` is 806 lines / 32 tests describing a much larger +tool (16 Bronze checks plus Silver, `--help`, `--version`, `--verbose`, `--badge`, +`--init-hook`, `--format=`, HTML output). **2 pass, 27 fail.** + +Two things to know before touching it: + +1. **Those tests assert on stdout substrings**, e.g. + `assert!(stdout.contains("Bronze-level RSR compliance: ACHIEVED"))`. They pin the + *wording* of the report and say nothing about what the checks must verify — so they + can be satisfied by checks that verify nothing. Treat them as a UI contract, not a + specification. +2. **A definition of RSR conformance already exists** elsewhere in the estate (hypatia's + `rsr-conformance` oracle). Writing checks to satisfy these strings risks creating a + second, divergent definition. Resolve the source-of-truth question first. + +Most of the clippy findings in #125 are dead code that exists *because* those modules +are unwired. **Do not silence them with `#![allow(dead_code)]`** — the root Rust CI +header forbids it, and that dead code is the specification of the missing feature. + ### Type Safety First Leverage Rust's type system: @@ -274,10 +304,14 @@ When making changes, ensure these remain true: ``` aletheia/ -├── src/ -│ └── main.rs # Core implementation (~950 lines) +├── src/ # 5 modules, 995 lines total — see Module Layout above +│ ├── main.rs # CLI entry (121) +│ ├── checks.rs # compliance checks (316) +│ ├── config.rs # .aletheia.toml (243) +│ ├── output.rs # human/JSON/SARIF (226) +│ └── types.rs # core types (89) ├── tests/ -│ └── integration_tests.rs # Integration tests (18 tests) +│ └── integration_tests.rs # 32 tests — 2 pass, 27 fail (issue #124) ├── benches/ # Performance benchmarks ├── examples/ # Usage examples ├── fuzz/ # Fuzzing infrastructure @@ -285,12 +319,11 @@ aletheia/ │ ├── security.txt # RFC 9116 security contact │ ├── ai.txt # AI training policies │ └── humans.txt # Human attribution -├── .github/workflows/ # 23 GitHub Actions workflows +├── .github/workflows/ # 16 files — ⚠ ALL INERT, see below ├── Cargo.toml # Zero dependencies, MSRV 1.80 ├── Cargo.lock # Lock file (commit this) ├── Justfile # Build automation -├── flake.nix # Nix reproducible builds -├── .gitlab-ci.yml # CI/CD pipeline +├── .gitlab-ci.yml # CI/CD pipeline (GitLab mirror) ├── .gitignore # Git ignore patterns ├── README.adoc # User documentation (AsciiDoc) ├── SECURITY.md # Security policy @@ -305,6 +338,22 @@ aletheia/ └── META.scm # Project metadata and ADRs ``` +### ⚠ The 16 workflows in `aletheia/.github/workflows/` have NEVER run + +`aletheia/` is **vendored into `maa-framework` as plain tracked files** (mode 100644), +not a submodule, and GitHub Actions reads `.github/workflows/` **at the repository root +only**. There is no standalone `hyperpolymath/aletheia` repo running them either — it was +deleted around January 2026 and its content vendored here. + +Consequence: editing anything under `aletheia/.github/workflows/` has **no effect on +CI whatsoever**. This is not hypothetical — it is how commit `b5322c2` (2026-06-17) left +this crate **failing to compile for over a month** with nobody noticing. + +**The real gate is `/.github/workflows/rust-ci.yml` at the repository root.** It runs +`cargo build` (debug + release), `cargo test`, `cargo fmt --check` and a zero-dependency +assertion, with `working-directory: aletheia`. Add gates there, not here. See +`aletheia/.github/workflows/README.md`. + ## Troubleshooting ### "Dependency detected" error @@ -368,7 +417,7 @@ For questions about this document or Aletheia development: --- -**Last Updated**: 2026-02-05 -**Version**: 1.1 +**Last Updated**: 2026-07-27 +**Version**: 1.2 *"Alētheia is not just absence of falsehood, but active unconcealment of truth."* From 50ab7f416f89c25689dde4661cb88052f1fdd2dc Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:28:36 +0100 Subject: [PATCH 2/3] fix(aletheia): SHA-pinning check could never fail; make it real MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `check_workflow_pins` decided a line was unpinned with: if line.contains("@v") && !line.contains("@") { `contains("@v")` implies `contains("@")`, so the second clause is always false and `has_unpinned` could never be set. Every repository passed the check unconditionally, including ones with `@v4` or `@master` refs. Verified with a standalone binary before changing anything: uses: actions/checkout@v4 old_detects_unpinned=false This is aletheia's Silver-level "GitHub Actions SHA pinning" check — a gate that has never been able to fail. It is also, pointedly, the exact check that would have caught `SonarSource/sonarqube-scan-action@master`, the unpinned action that broke this repo's Governance and CodeQL in #139. Replaced with `uses_line_is_pinned`, which requires the ref after the final `@` to be 40 hex characters, and: - accepts both `uses:` and list form `- uses:` (the estate's existing workflow linter anchors to line-start and misses the inline form) - ignores a trailing `# v7.0.1` provenance comment, so a correctly pinned line with a stale version comment is not a false positive - exempts `./…` local actions/reusable workflows and `docker://` refs, which cannot carry a Git SHA Also replaced `assert!(true)` in test_file_exists with a real assertion. It had given up on CWD-dependence; anchoring on `env!("CARGO_MANIFEST_DIR")` makes it deterministic, and it now covers the negative case and the is_file()-not- exists() distinction. Verified: 29 unit tests pass (was 26), `cargo fmt --check` clean, clippy 25 -> 23 findings. End-to-end `cargo run -- .` against this repo now reports `[FAIL] GitHub Actions SHA pinning`, correctly identifying the one genuinely unpinned action, where before the fix it reported a pass. Refs #125. Co-Authored-By: Claude Opus 5 --- aletheia/src/checks.rs | 120 +++++++++++++++++++++++++++++++++++------ 1 file changed, 103 insertions(+), 17 deletions(-) diff --git a/aletheia/src/checks.rs b/aletheia/src/checks.rs index c212eea..60872af 100644 --- a/aletheia/src/checks.rs +++ b/aletheia/src/checks.rs @@ -141,17 +141,8 @@ pub fn check_workflow_pins(report: &mut ComplianceReport, repo_path: &Path) { { checked_files += 1; if let Ok(content) = fs::read_to_string(&path) { - // Check if all 'uses:' lines have SHA pinning (40 hex chars) - let mut has_unpinned = false; - for line in content.lines() { - if line.trim().starts_with("uses:") { - // Simple check: if it contains @v (like @v4), it's unpinned - if line.contains("@v") && !line.contains("@") { - has_unpinned = true; - break; - } - } - } + let has_unpinned = + content.lines().any(|line| !uses_line_is_pinned(line)); if !has_unpinned { valid_files += 1; } @@ -176,6 +167,49 @@ fn file_exists(repo_path: &Path, filename: &str) -> bool { repo_path.join(filename).is_file() } +/// SECURITY: Decide whether one workflow line satisfies SHA pinning. +/// +/// Returns `true` for any line that is not a `uses:` line, so callers can apply +/// this with `.any(|l| !uses_line_is_pinned(l))` over a whole file. +/// +/// A `uses:` value is pinned only when the ref after the final `@` is exactly +/// 40 hexadecimal characters (a full-length Git SHA-1). `@v4`, `@main`, +/// `@master` and a bare action with no `@` at all are all unpinned. +/// +/// Exempt (not pinnable, so treated as pinned): +/// - local actions and local reusable workflows — `./…` +/// - `docker://` image references, which use a different digest syntax +/// +/// A trailing `# v4` provenance comment is ignored, so +/// `uses: actions/checkout@3d3c42e5… # v7.0.1` is correctly seen as pinned. +fn uses_line_is_pinned(line: &str) -> bool { + let trimmed = line.trim(); + // Accept both `uses:` and list form `- uses:`. + let rest = match trimmed + .strip_prefix("uses:") + .or_else(|| trimmed.strip_prefix("- uses:")) + { + Some(r) => r, + None => return true, // not a uses: line — nothing to judge + }; + + // Strip the trailing provenance comment, then surrounding quotes. + let value = rest.split('#').next().unwrap_or("").trim(); + let value = value.trim_matches(|c| c == '"' || c == '\''); + + if value.is_empty() { + return true; + } + if value.starts_with("./") || value.starts_with(".\\") || value.starts_with("docker://") { + return true; + } + + match value.rsplit_once('@') { + Some((_, git_ref)) => git_ref.len() == 40 && git_ref.chars().all(|c| c.is_ascii_hexdigit()), + None => false, // no ref at all — unpinned + } +} + /// Helper: Recursive implementation of glob_match. fn glob_match_recursive(pattern: &[char], text: &[char], pi: usize, ti: usize) -> bool { if pi >= pattern.len() && ti >= text.len() { @@ -300,12 +334,64 @@ mod tests { #[test] fn test_file_exists() { - // file_exists checks if path.join(filename).is_file() - // Since we're testing with temp dir, check something that exists - let current_dir = std::env::current_dir().expect("TODO: handle error"); - let exists = file_exists(¤t_dir, "Cargo.toml"); - // May or may not exist depending on CWD, so just check it doesn't panic - assert!(true); // Test passed if no panic + // Anchor on CARGO_MANIFEST_DIR rather than the process working directory: + // the crate root is fixed at compile time, so this is deterministic no + // matter where the test binary is invoked from. + let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")); + + assert!( + file_exists(root, "Cargo.toml"), + "Cargo.toml exists at the crate root" + ); + assert!(!file_exists(root, "no-such-file.does-not-exist")); + // `is_file()`, not `exists()` — a directory must not count as a file. + assert!(!file_exists(root, "src"), "a directory is not a file"); + } + + #[test] + fn test_uses_line_is_pinned_accepts_full_sha() { + // Real pins taken from this repository's own workflows. + assert!(uses_line_is_pinned( + " - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1" + )); + // A trailing provenance comment must not defeat the check. + assert!(uses_line_is_pinned( + " uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5.0.0" + )); + } + + #[test] + fn test_uses_line_is_pinned_rejects_tags_and_branches() { + // REGRESSION: the previous implementation was `line.contains("@v") + // && !line.contains("@")`, which is unsatisfiable — every one of these + // was silently reported as pinned. + assert!(!uses_line_is_pinned(" uses: actions/checkout@v4")); + assert!(!uses_line_is_pinned( + " - uses: actions/checkout@v7.0.1" + )); + assert!(!uses_line_is_pinned(" uses: some/action@main")); + // The exact line that broke Governance and CodeQL on this repo. + assert!(!uses_line_is_pinned( + " uses: SonarSource/sonarqube-scan-action@master" + )); + // A short/abbreviated SHA is not a full-length pin. + assert!(!uses_line_is_pinned(" uses: foo/bar@3d3c42e")); + // No ref at all. + assert!(!uses_line_is_pinned(" uses: foo/bar")); + } + + #[test] + fn test_uses_line_is_pinned_ignores_non_uses_and_exempt_forms() { + assert!(uses_line_is_pinned(" - name: Checkout")); + assert!(uses_line_is_pinned(" run: cargo test")); + assert!(uses_line_is_pinned("")); + // Local actions and local reusable workflows cannot be SHA-pinned. + assert!(uses_line_is_pinned(" - uses: ./.github/actions/setup")); + assert!(uses_line_is_pinned( + " uses: ./.github/workflows/reusable.yml" + )); + // Docker refs use a different digest syntax; out of scope. + assert!(uses_line_is_pinned(" uses: docker://alpine:3.20")); } #[test] From 38fdc9b3c877b748922c659e93412690b13942e4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:29:01 +0100 Subject: [PATCH 3/3] fix(#99): wire the root Justfile to real cargo targets MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Every build-ish recipe was a fake gate: build: @echo "Build not configured yet" `just build`, `test`, `fmt`, `lint` and `clean` all printed a string and exited 0, so any caller — human or CI — got a pass for doing nothing. Wired to the same commands the root rust-ci.yml gate runs, in the same order, so `just check` locally means what CI means: build -> cargo build --locked --all-targets, then --release test -> cargo test --locked --bins fmt -> cargo fmt --check (fmt-fix applies) lint -> cargo clippy --locked --all-targets deps-check -> the zero-dependency assertion, copied from rust-ci.yml check -> build test fmt deps-check self-verify -> run aletheia against this repository Two deliberate limits, documented in the recipes so nobody "fixes" them: - `test` is `--bins` only. The integration suite is a specification for a CLI that does not exist yet; 27 of 29 fail by design (#124). Adding `--tests` here would make the bar green by breaking it. - `lint` is not yet `-D warnings`; 23 findings remain (#125). When that closes, `-D warnings` must be added HERE AND to rust-ci.yml in the same change, so local and CI never disagree about what "lint passes" means. Verified by running them, not by reading them: just --list parses; just deps-check -> "OK: zero dependencies"; just test -> 29 passed; just check -> exit 0. And verified the gate can actually FAIL, which is the whole point: appending badly-formatted Rust makes `just fmt` exit 1 while `just build` still exits 0, and reverting restores exit 0. Closes #99. Co-Authored-By: Claude Opus 5 --- Justfile | 53 ++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 44 insertions(+), 9 deletions(-) diff --git a/Justfile b/Justfile index 6fdd912..8c7294f 100644 --- a/Justfile +++ b/Justfile @@ -8,25 +8,60 @@ import? "contractile.just" default: @just --list -# Build the project +# These recipes mirror the root `.github/workflows/rust-ci.yml` gate exactly, so +# `just check` locally means the same thing as CI. They MUST fail loudly — a recipe +# that echoes and exits 0 is a fake gate (issue #99 was exactly that). + +# Build aletheia (debug + release, locked) build: - @echo "Build not configured yet" + cd aletheia && cargo build --locked --all-targets + cd aletheia && cargo build --locked --release -# Run tests +# Run aletheia's unit tests (--bins only; see #124 note in recipe) test: - @echo "Tests not configured yet" + # `--bins` is deliberate. The integration suite is a specification for a CLI + # that has not been built yet — 27 of 29 fail by design (issue #124). + # Do NOT add `--tests` here to make the bar look green. + cd aletheia && cargo test --locked --bins -# Format code +# Check formatting (does not modify files) fmt: - @echo "Formatting not configured yet" + cd aletheia && cargo fmt --check + +# Apply formatting +fmt-fix: + cd aletheia && cargo fmt -# Lint code +# Lint aletheia (not yet -D warnings — issue #125) lint: - @echo "Linting not configured yet" + # 23 findings remain, mostly dead code that exists because the CLI is + # unwired (#124). When #125 closes, add `-- -D warnings` here AND to + # rust-ci.yml in the same change, so local and CI never disagree about + # what "lint passes" means. + cd aletheia && cargo clippy --locked --all-targets + +# Enforce the zero-dependency RSR Bronze constraint (mirrors rust-ci.yml) +deps-check: + #!/usr/bin/env bash + set -euo pipefail + cd aletheia + if cargo tree --depth 1 | tail -n +2 | grep -q '[a-z]'; then + echo "ERROR: Aletheia must have zero dependencies (see aletheia/CLAUDE.md)" + cargo tree --depth 1 + exit 1 + fi + echo "OK: zero dependencies" + +# Everything the root CI gate runs, in the same order +check: build test fmt deps-check + +# Self-verify: run aletheia against this repository +self-verify: + cd aletheia && cargo run --locked --quiet -- .. # Clean build artifacts clean: - @echo "Clean not configured yet" + cd aletheia && cargo clean # Run panic-attacker pre-commit scan assail: