feat(scaffold): v2 six-language templates and a single-pass scanner (#186, #197) - #228
Merged
Merged
Conversation
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.
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.
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.
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.
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/<channel>/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.
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.
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.
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.
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.
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.
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.
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.
|
Navigate logical layers of code changes, visualize relationships, and explore their blast radius. Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (98)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
❌ Failed to create Coding Agent finishing-touch task. Please try again. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #186 and #197.
#186 — the scaffold emitted the retired v1 shape
aletheia/scripts/create-template.shnow generates the v2 project shape (.adocdocs,LICENSE+LICENSES/,0-AI-MANIFEST.a2ml,.machine_readable/rsr-profile.a2ml,.editorconfig,Dockerfile-free, noflake.nix/LICENSE.txt/v1justfile), for all sixTier-1 canon languages: Rust, Zig, Elixir, Haskell, Ada/SPARK, Agda.
Architecture is
templates/common/plus a per-language overlay, with an unresolved-@@placeholder guard that exits non-zero,
--list-languages,--verify,--forceand--no-git.A generated project reaches 26/26 (100%), Bronze + Silver ACHIEVED, with no hand edits, and
there is a regression test (
test_scaffold_passes_bronze_and_silver) that fails if that stopsbeing true. Each language genuinely builds and tests with its own compiler — the evidence is in
DELIVERY-186-197.md, per language.Two of the six also ship an opt-in proof gate as a template asset:
templates/rust/.github/workflows/proof.yml— Creusot,just prooftemplates/ada/.github/workflows/proof.yml— SPARK/gnatprove,just proofBoth are real gates, not labels: a false obligation fails them non-zero.
#197 — the scanner walked the tree seven times
ScanSetconsolidatesScanner::walk_filesinto a single traversal that feeds every check, withper-check budget semantics unchanged.
Found and fixed along the way: the scanner ignored
.gitignoreBuilding #186 surfaced a real bug: any build output in the tree flipped the compliance gate.
just checkfollowed byaletheia .on a generated Rust project went from 26/26 to 18/26,Bronze NOT MET, purely because
target/andobj/exist.checks.rsnow loads.gitignoreper directory during the single walk, andconfig.rsimplementsthe matching rules (comments,
!negation with last-match-wins, trailing-/directory-only rules,anchoring, and nested-file scoping). Repository
.gitignoresemantics are kept separate from theconfig file's
[ignore]section. Three integration tests cover it, including a negative control.Evidence
Both proofs were re-run on this exact branch's content after rebasing, through the real generator,
not in the template directory.
What this PR does not claim
proof.ymlfiles have never run on a GitHub runner. They are template assets: theylive under
aletheia/templates/..., so they run in generated projects, never in this repo.Pushing this branch cannot exercise them. Every command in them was run by hand against a
from-scratch toolchain — that is how three defects in the Rust job and one in the Ada job were
found and fixed (creusot-rustc resolved from the wrong place, missing provers and why3/why3find,
a stale hard-coded Why3 pin, and gnatprove installed without a compiler) — but "known-good
commands in the right order" is a weaker claim than a green run, and this PR does not claim the
stronger one.
templates/agda/.github/workflows/ci.ymlinstalls the distro Agda, while.tool-versionspins 2.6.4.3. They coincide on Debian 13; that is not evidence about another base image.
aletheia/LICENSEstill says PMPL-1.0-or-later while its sources say MPL-2.0. Pre-existing,not touched here.
absolute-zerosubmodule shows as deleted in the local clone used to build this; it is notpart of any commit here.
Full write-up, including the negative results and the false-gate investigation:
DELIVERY-186-197.md.Commits
12 commits, rebased onto current
main— no merge commit, no conflicts. The twofix(ci)commitsand three
docscommits in the middle exist because the proof workflows were wrong as firstwritten and reading them had not shown it.