From 76777f487efd50b800604cab739c3a81fc715d59 Mon Sep 17 00:00:00 2001 From: Slava Barinov Date: Wed, 26 Aug 2026 00:55:26 +0900 Subject: [PATCH 01/10] feat: add the agent skill and plugin manifests - Package one skill directory for both Claude Code and Codex. - Add the `/anodized:spec` and `/anodized:check` commands. - Document the clause grammar, qualifiers, traits, loops, and data. - Cover migration from pre-0.6 syntax and from other contract crates. --- .agents/plugins/marketplace.json | 19 + .claude-plugin/marketplace.json | 32 ++ plugins/anodized/.claude-plugin/plugin.json | 25 ++ plugins/anodized/.codex-plugin/plugin.json | 26 ++ plugins/anodized/commands/check.md | 66 +++ plugins/anodized/commands/spec.md | 38 ++ plugins/anodized/skills/anodized/SKILL.md | 406 ++++++++++++++++++ .../anodized/skills/anodized/diagnostics.md | 163 +++++++ plugins/anodized/skills/anodized/examples.md | 300 +++++++++++++ plugins/anodized/skills/anodized/migration.md | 95 ++++ plugins/anodized/skills/anodized/reference.md | 158 +++++++ 11 files changed, 1328 insertions(+) create mode 100644 .agents/plugins/marketplace.json create mode 100644 .claude-plugin/marketplace.json create mode 100644 plugins/anodized/.claude-plugin/plugin.json create mode 100644 plugins/anodized/.codex-plugin/plugin.json create mode 100644 plugins/anodized/commands/check.md create mode 100644 plugins/anodized/commands/spec.md create mode 100644 plugins/anodized/skills/anodized/SKILL.md create mode 100644 plugins/anodized/skills/anodized/diagnostics.md create mode 100644 plugins/anodized/skills/anodized/examples.md create mode 100644 plugins/anodized/skills/anodized/migration.md create mode 100644 plugins/anodized/skills/anodized/reference.md diff --git a/.agents/plugins/marketplace.json b/.agents/plugins/marketplace.json new file mode 100644 index 00000000..68634100 --- /dev/null +++ b/.agents/plugins/marketplace.json @@ -0,0 +1,19 @@ +{ + "name": "anodized", + "interface": { + "displayName": "Anodized" + }, + "plugins": [ + { + "name": "anodized", + "source": { + "source": "local", + "path": "./plugins/anodized" + }, + "policy": { + "installation": "AVAILABLE" + }, + "category": "Developer Tools" + } + ] +} diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json new file mode 100644 index 00000000..0b11d250 --- /dev/null +++ b/.claude-plugin/marketplace.json @@ -0,0 +1,32 @@ +{ + "$schema": "https://anthropic.com/claude-code/marketplace.schema.json", + "name": "anodized", + "owner": { + "name": "anodized-rs" + }, + "metadata": { + "description": "The Anodized agent skill: write and review `#[spec]` specifications in Rust." + }, + "plugins": [ + { + "name": "anodized", + "source": "./plugins/anodized", + "description": "Write, review, and debug Anodized `#[spec]` specifications on Rust functions, traits, loops, structs, and enums, and run the runtime-check build configurations.", + "version": "0.6.0", + "author": { + "name": "anodized-rs" + }, + "homepage": "https://github.com/anodized-rs/anodized", + "repository": "https://github.com/anodized-rs/anodized", + "license": "MIT OR Apache-2.0", + "category": "development", + "keywords": [ + "anodized", + "rust", + "specification", + "design-by-contract", + "verification" + ] + } + ] +} diff --git a/plugins/anodized/.claude-plugin/plugin.json b/plugins/anodized/.claude-plugin/plugin.json new file mode 100644 index 00000000..434a73fe --- /dev/null +++ b/plugins/anodized/.claude-plugin/plugin.json @@ -0,0 +1,25 @@ +{ + "name": "anodized", + "version": "0.6.0", + "description": "Write, review, and debug Anodized `#[spec]` specifications on Rust functions, traits, loops, structs, and enums, and run the runtime-check build configurations.", + "author": { + "name": "anodized-rs" + }, + "homepage": "https://github.com/anodized-rs/anodized", + "repository": "https://github.com/anodized-rs/anodized", + "license": "MIT OR Apache-2.0", + "keywords": [ + "anodized", + "rust", + "specification", + "design-by-contract", + "verification" + ], + "skills": [ + "./skills/anodized" + ], + "commands": [ + "./commands/check.md", + "./commands/spec.md" + ] +} diff --git a/plugins/anodized/.codex-plugin/plugin.json b/plugins/anodized/.codex-plugin/plugin.json new file mode 100644 index 00000000..4205d30a --- /dev/null +++ b/plugins/anodized/.codex-plugin/plugin.json @@ -0,0 +1,26 @@ +{ + "name": "anodized", + "version": "0.6.0", + "description": "Write, review, and debug Anodized `#[spec]` specifications on Rust functions, traits, loops, structs, and enums, and run the runtime-check build configurations.", + "author": { + "name": "anodized-rs" + }, + "homepage": "https://github.com/anodized-rs/anodized", + "repository": "https://github.com/anodized-rs/anodized", + "license": "MIT OR Apache-2.0", + "keywords": [ + "anodized", + "rust", + "specification", + "design-by-contract", + "verification" + ], + "skills": "./skills/", + "interface": { + "displayName": "Anodized", + "shortDescription": "Write Anodized `#[spec]` specs in Rust", + "developerName": "anodized-rs", + "category": "Developer Tools", + "websiteURL": "https://github.com/anodized-rs/anodized" + } +} diff --git a/plugins/anodized/commands/check.md b/plugins/anodized/commands/check.md new file mode 100644 index 00000000..8275aabd --- /dev/null +++ b/plugins/anodized/commands/check.md @@ -0,0 +1,66 @@ +--- +description: Compile and test the current crate under every Anodized build configuration. +allowed-tools: Bash(cargo:*) +--- + +# Check every Anodized build configuration + +Anodized behavior is controlled entirely by `--cfg` flags, not Cargo features. A spec that +type-checks under one configuration can still fail under another, so verify all six — the same +set the Anodized CI matrix runs. + +Run each pass in order, from the current crate's directory: + +```bash +cargo test --no-fail-fast +cargo --config 'build.rustflags=["--cfg","anodized_discard_specs"]' test --no-fail-fast +cargo --config 'build.rustflags=["--cfg","anodized_print"]' test --no-fail-fast +cargo --config 'build.rustflags=["--cfg","anodized_panic"]' test --no-fail-fast +cargo --config 'build.rustflags=["--cfg","anodized_print","--cfg","anodized_panic"]' test --no-fail-fast +cargo --config 'build.rustflags=["--cfg","anodized_print","--cfg","anodized_panic","--cfg","anodized_try"]' test --no-fail-fast +``` + +What each pass proves: + +| Pass | Proves | +| --- | --- | +| no cfg | specs are embedded and type-checked; checks do not run | +| `anodized_discard_specs` | the code still builds with specs erased entirely | +| `anodized_print` | violations report to stderr and execution continues | +| `anodized_panic` | violations panic | +| `print` + `panic` | both, the usual configuration for a test suite | +| `print` + `panic` + `try` | additionally enables `try_call!` | + +Report the results as a table of pass versus outcome. For any failure: + +- `precondition failed: ` — the **caller** violated the contract. Fix the call site, or + the precondition if it was wrong. +- `postcondition failed: ` — the **implementation** violated its own contract. Fix the + body, or the postcondition if it was wrong. +- A compile error only under `anodized_discard_specs` means real code depends on something a + spec brought into scope. + +Never edit a clause just to make a pass go green. Which edit is legitimate depends on which +kind of check fired. + +A **postcondition** failure means the spec is false of the code. If the clause overclaimed, +weaken the postcondition, or strengthen the precondition so it no longer covers the inputs +where the guarantee does not hold. Either keeps the spec true without re-examining the body. + +A **precondition** failure means a caller broke an obligation; the spec is not thereby false +of the code, so the usual repair is at the call site. Weaken the precondition only when the +body demonstrably handles the input it rejected — that is a new claim about the body, so +verify it rather than assuming it. + +Only the passes with `anodized_print` name the failing expression; `anodized_panic` alone +reports the bare text, so reproduce with both before diagnosing. + +Before applying any of that, check which clause failed, because the message does not say. A +`maintains` clause is checked twice and reports as `precondition failed` on entry and +`postcondition failed` on exit, so a `precondition failed` may name an invariant rather than a +`requires`. Weakening a `maintains` relaxes the exit guarantee as well as the entry condition, +so it is not the safe edit that weakening a true precondition is. + +Note who each edit can hurt: weakening a genuine precondition cannot break an existing caller, +while strengthening a precondition, weakening a postcondition, or weakening an invariant can. +Say what you changed and why. diff --git a/plugins/anodized/commands/spec.md b/plugins/anodized/commands/spec.md new file mode 100644 index 00000000..94c68b5a --- /dev/null +++ b/plugins/anodized/commands/spec.md @@ -0,0 +1,38 @@ +--- +description: Add or tighten Anodized specs on the selected functions. +allowed-tools: Bash(cargo:*), Bash(anodized-fmt:*) +--- + +# Add Anodized specs + +Target: $ARGUMENTS (a path, a function name, or the current selection; if empty, ask what to +specify). + +Follow the `anodized` skill's decision rules. In short: + +1. Read the target and list what it actually requires of its caller and guarantees in return. + Look for existing `assert!`, `panic!`, and early `return Err` — those are preconditions + already written in another form. +2. Write the **smallest** spec that captures them. Skip anything the type system already + states: `requires: [x >= 0]` on a `u32` is noise, and so is a postcondition restating the + return type. +3. Keep clauses in the mandatory order — qualifiers, `requires`, `maintains`, `captures`, + `ensures` — and prefer several small clauses over one `&&` chain, so a failure names the + part that broke. +4. Bind the return value with an `ensures` closure (`ensures: |output| ...`). There is no + implicit `output` binding and no `old()`; entry-time values come from `captures`. +5. Verify with `cargo check`, then `cargo --config 'build.rustflags=["--cfg","anodized_print","--cfg","anodized_panic"]' test`. +6. Format with `anodized-fmt` if it is installed. + +Show the diff and explain each clause in one line. If a function needs no spec, say so rather +than inventing one — but prefer a bare `#[spec]` to no attribute at all. It records that the +contract is deliberately tautological, equivalent to `requires: true` and `ensures: true`, +which is not the same as nobody having considered it. On a function nested in a `trait` or an +`impl`, spell it `#[spec()]` — a nested attribute is read with `parse_args`, so the parentheses +are required even when empty. + +Some functions cannot carry a spec at all, because the macro evaluates the body in a closure: +returning `impl Trait` (`E0562`), `const fn` (`E0015`), and returning `&mut` borrowed from a +parameter all fail to compile. That list is not exhaustive — if adding a spec breaks the +build, the shape cannot carry one, and the fix is to drop the attribute rather than to work +around it. diff --git a/plugins/anodized/skills/anodized/SKILL.md b/plugins/anodized/skills/anodized/SKILL.md new file mode 100644 index 00000000..e6d06c3d --- /dev/null +++ b/plugins/anodized/skills/anodized/SKILL.md @@ -0,0 +1,406 @@ +--- +name: anodized +description: > + Write, review, and repair Anodized `#[spec]` specifications in Rust: preconditions + (`requires`), invariants (`maintains`), entry-time snapshots (`captures`), postconditions + (`ensures`), loop invariants and variants (`decreases`), refinements on `struct` and `enum`, + and the `fn` qualifier lattice. Use when adding or reviewing specs in a crate that depends + on `anodized`, when a `#[spec(...)]` fails to compile, when a precondition or postcondition + fires at runtime, when specifying a trait and its impls, or when choosing a + `--cfg anodized_*` build. Anodized has no `old()` and no implicit `output` binding, and its + 0.6 syntax broke from 0.5; this skill supplies the current forms. +when_to_use: > + Trigger on: `#[spec]`, anodized, requires:, ensures:, maintains:, captures:, decreases:, + precondition, postcondition, loop invariant, design by contract, add a contract to this + function, specify this trait, narrow a spec on an impl. Also: old(), "the old value", result + in a postcondition, old_x, "expression as pattern", binds:, inspects:, E0596 or E0425 inside + a spec, "qualifier is redundant", "qualifiers cannot be weaker", "unknown spec field", + "fields are out of order". Also migrating from contracts, Creusot, Prusti, Kani, or Verus. + Also anodized_panic, anodized_print, anodized_try, anodized_discard_specs, try_call!, + anodized-fmt, implies!, opaque!. +allowed-tools: Bash(cargo:*), Bash(anodized-fmt:*) +--- + + + +# Writing Anodized specifications + +A spec is ordinary Rust: every condition is a `bool` expression, and there is no separate +specification language to learn. Conditions on functions and on `struct` definitions are +type-checked by the compiler like any other code. Conditions on **loops and `enum` +definitions are not** — as of 0.6 they are parsed and then dropped, so a typo in one compiles +silently. Write those with extra care. What has to +be learned is the shape of the attribute, and the handful of places where that shape differs +from what every other contract system has trained you to expect. + +## Four things that are not what you expect + +**1. There is no `old()`.** Entry-time values come from `captures`, which are visible only to +postconditions. + +```rust,compile_fail +// EXPECT: E0425 +use anodized::spec; + +#[spec(ensures: |output| output == old(count) + 1)] +fn increment(count: u32) -> u32 { + count + 1 +} +``` + +```rust +use anodized::spec; + +#[spec( + requires: count < u32::MAX, + captures: before = count, + ensures: |output| output == before + 1, +)] +fn increment(count: u32) -> u32 { + count + 1 +} +``` + +**2. There is no implicit `output` or `result`.** A bare `ensures` expression cannot see the +return value at all; bind it with a closure. + +```rust,compile_fail +// EXPECT: E0425 +use anodized::spec; + +#[spec(ensures: output > 0)] +fn one() -> u32 { + 1 +} +``` + +```rust +use anodized::spec; + +#[spec(ensures: |output| output > 0)] +fn one() -> u32 { + 1 +} +``` + +**3. Conditions cannot mutate anything.** Each is coerced to `Fn() -> bool`, so touching a +`&mut` inside one is a borrow error, not a runtime surprise. + +```rust,compile_fail +// EXPECT: E0596 +use anodized::spec; + +#[spec(requires: buffer.pop().is_some())] +fn drain(buffer: &mut Vec) { + buffer.clear(); +} +``` + +**4. Anodized 0.6 broke from 0.5.** If you remember this crate at all, you probably remember +the old syntax. `old_x` bindings are gone, `captures` flipped to `pattern = expression`, and +output bindings moved into the `ensures` closure. + +```rust,compile_fail +// EXPECT: E0425 +use anodized::spec; + +#[spec(ensures: |output| output == old_count + 1)] +fn increment(count: u32) -> u32 { + count + 1 +} +``` + +| About to write | Write instead | +| --- | --- | +| `old(x)` or `old_x` | `captures: old_x = x` and read it in `ensures` | +| `ensures: output > 0` | `ensures: \|output\| output > 0` | +| `captures: x.len() as n` | `captures: n = x.len()` | +| `binds:` / `inspects:` | `ensures: \|PAT\| [EXPR, ...]` | +| `#[requires(...)]` / `#[ensures(...)]` | one `#[spec(requires: ..., ensures: ...)]` | + +## When to add a spec + +Add one when at least one is true: the function is `pub` or crosses a module boundary; its +inputs have a non-trivial valid domain; its output has a guaranteed property the type does not +state; or it holds a loop whose correctness rests on a non-obvious invariant. + +Do **not** add a clause that restates the type system. `requires: [n >= 0]` on a `u32` is +noise, and so is a postcondition asserting the return type. A spec that adds no information +costs the reader attention and buys nothing. Existing `assert!`, `panic!`, and early +`return Err` are preconditions already written in another form — those are the ones worth +lifting into `requires`. + +When a function genuinely has nothing to state, a bare `#[spec]` is still worth adding. It +records that the contract is deliberately tautological — equivalent to `requires: true` and +`ensures: true` — which is not the same as nobody having considered it. It is also what +enables loop specs inside the body, so it is not purely decorative. + +Not every function can carry one, though. The macro evaluates the body inside a closure, so +any shape the language will not let cross a closure boundary stops compiling the moment a spec +is attached — in every configuration except `anodized_discard_specs`, which drops specs before +they expand. Known cases: a function returning `impl Trait` (`E0562`), a `const fn` (`E0015`), +and a function returning `&mut` borrowed from a parameter (`captured variable cannot escape +`FnMut` closure body`, which carries no error code). Returning a shared `&` is fine. + +Treat that list as incomplete rather than exhaustive. The rule that generalizes is the closure: +if attaching a spec makes a function stop compiling, that shape cannot carry one, and the only +repair is to remove the attribute. None of these have a workaround. + +On a function nested inside a spec'd `trait` or `impl`, an empty spec is written `#[spec()]`, +not `#[spec]`. The attribute on a nested function is read with `parse_args`, which needs the +parentheses even when there is nothing between them; a bare one is rejected with `expected +attribute arguments in parentheses`. This applies to inherent impls, traits, and trait impls +alike. Omitting the attribute entirely is also valid there and means the same empty spec — the +parentheses only matter once you write the attribute down. + +Preconditions describe what callers **must** uphold. Recoverable failures are still `Result`; +a spec is not an error-handling mechanism. + +## Clause grammar + +Clauses appear in a fixed order, and the order is enforced: + +```rust,ignore +// fragment +#[spec( + pure, // qualifiers, bare + requires: [condition, condition], // preconditions + maintains: condition, // invariants, checked at entry and exit + captures: [name = expression], // entry-time values, at most one field + ensures: |output| [condition], // postconditions +)] +``` + + +| Clause | Takes | Allowed on | +| --- | --- | --- | +| `requires` | one condition, or a list | `fn` | +| `maintains` | one condition, or a list | `fn`, loop, `struct`, `enum` | +| `captures` | `pattern = expression`, or a list; at most one field | `fn` | +| `ensures` | a condition, `\|pattern\| condition`, or a list of either | `fn` | +| `decreases` | one expression; at most one field | loop only | + + +`requires`, `maintains`, and `ensures` may be repeated; the conditions accumulate. Prefer +several small clauses over one `&&` chain — a runtime failure names the clause it broke, so +smaller clauses give sharper messages. A trailing comma is optional everywhere. + +## `captures`: entry-time values + +At most **one** `captures` field per spec; use the list form for several. The right-hand side +is **moved**, so a non-`Copy` value needs an explicit `.clone()`. Captures are evaluated after +`requires` and before the body, and they are in scope **only** for postconditions — reading +one from `requires` or from the body is `E0425`. + +```rust +use anodized::spec; + +#[spec( + captures: [smallest = items.iter().copied().min(), count = items.len()], + ensures: |ref output| [output.len() == count, output.first().copied() == smallest], +)] +fn sorted(mut items: Vec) -> Vec { + items.sort_unstable(); + items +} +``` + +## `ensures`: binding the return value + +Four forms are accepted: + +| Form | Return value | +| --- | --- | +| `ensures: expr` | not bound | +| `ensures: \|pat\| expr` | bound by `pat` | +| `ensures: \|pat\| [a, b]` | bound by `pat` for the whole group | +| `ensures: [a, \|pat\| b]` | bound only inside that element | + +The closure takes the return value by move, so use `|ref output|` for a non-`Copy` type. The +pattern must be irrefutable: `|Ok(v)|` is not allowed, so test with `|ref out| out.is_ok()`. + +## Qualifiers + + +| Qualifier | Guarantees | +| --- | --- | +| `functional` | `deterministic`, `effectfree`, `infallible`, `terminating` | +| `pure` | `deterministic`, `effectfree` | +| `total` | `infallible`, `terminating` | +| `deterministic` | the return value depends only on the arguments | +| `effectfree` | no side effects | +| `infallible` | does not panic or abort | +| `terminating` | does not run forever | + + +Write them bare, before every value clause. Naming a composite together with one of its own +components is a hard error, not a warning: `pure, deterministic` is redundant because `pure` +already means `deterministic` and `effectfree`. Claim only what you can defend. + +## Item kinds + + +| Item | Clauses | How | +| --- | --- | --- | +| free `fn` | all clauses | `#[spec(...)]` on the `fn` | +| inherent `impl` | all clauses, per method | bare `#[spec]` on the `impl`, clauses on each `fn` | +| `trait` | all clauses, per method | bare `#[spec]` on the `trait`, clauses on each `fn` | +| `impl Trait for T` | all clauses, narrowing only | bare `#[spec]` on the `impl`, optional clauses on each `fn` | +| `while` / `for` | `maintains`, `decreases` | `#[spec(...)]` on the loop, inside a spec'd `fn` | +| `struct` | `maintains` | `#[spec(...)]` on the `struct` | +| `enum` | `maintains` | `#[spec(...)]` on the `enum` | + + +## Traits + +Specifying a trait takes up to four steps. The two structural ones, 1 and 3, are required. +Omitting the trait's gives a macro error naming the missing annotation; omitting an impl's +gives `E0046`, complaining that a generated `__anodized_` item is unimplemented. The other two +are optional: + +1. A **bare** `#[spec]` on the trait, with no clauses. +2. `#[spec(...)]` with clauses on the trait's functions, where a function has any. One + without an attribute simply has an empty spec. +3. A **bare** `#[spec]` on every `impl Trait for T`. +4. Optionally, `#[spec(...)]` on an impl's functions — which may only **narrow**: weaken a + precondition or strengthen a postcondition, never the reverse. + +Note that narrowing runs opposite to repairing a spec, and for a different reason: an impl is +a special case, so it may accept more and promise more than the trait did. Repairing a spec +must never claim more than the code delivers. + +Qualifier narrowing is checked at build time by a generated `const { assert!(...) }`, so an +impl claiming less than its trait fails to compile. Pre- and postcondition narrowing is +checked only at runtime. Items prefixed `__anodized_` are internal; never implement them. + +## Loops + +A loop spec takes `maintains` and `decreases`, and the enclosing function must itself carry +`#[spec]`. `decreases` is one expression that strictly decreases each iteration and is bounded +below — it is the termination argument. + +```rust +use anodized::spec; + +#[spec(requires: !items.is_empty())] +fn maximum(items: &[u32]) -> u32 { + let mut best = items[0]; + let mut index = 1; + #[spec( + maintains: index <= items.len(), + decreases: items.len() - index, + )] + while index < items.len() { + if items[index] > best { + best = items[index]; + } + index += 1; + } + best +} +``` + +Loop specs are **not** checked at runtime, and their conditions are **not type-checked** +either: a loop invariant naming a variable that does not exist still compiles. They document +intent and feed analysis backends. Do not rely on them catching anything today. + +## Data + +`struct` and `enum` take `maintains` only, describing what is always true of a value. `self` +is in scope, and enum variants are brought into scope automatically. Neither is checked at +runtime yet. A `struct` condition **is** type-checked; an `enum` condition is not. + +```rust +use anodized::spec; + +#[spec(maintains: self.low <= self.high)] +struct Range { + low: u32, + high: u32, +} +``` + +## Build configurations + + +| Build configuration | Effect | +| --- | --- | +| *(none)* | Specs embedded and type-checked; no check runs. `captures` still evaluate. | +| `--cfg anodized_discard_specs` | Specs are dropped entirely: not embedded, not type-checked. Fastest builds. | +| `--cfg anodized_print` | A violated condition reports to stderr and execution continues. | +| `--cfg anodized_panic` | A violated condition panics, without naming the condition. Pair with `anodized_print` to be told which expression failed. | +| `--cfg anodized_try` | Enables `try_call!`, which turns a violation into a `Result`. Requires `anodized_panic`. | + + +Turn checks on for tests: + +```bash +RUSTFLAGS="--cfg anodized_print --cfg anodized_panic" cargo test +``` + +`anodized_print` names the failing condition in the message, so pairing it with +`anodized_panic` is the usual choice; `anodized_panic` alone panics without saying which +clause broke. + +With no flag set, checks do not run — but the spec is not entirely free: `captures` +expressions are evaluated on every call regardless, because the capture and the body are bound +in one statement. A `.clone()` in a capture is a real clone in a release build. Use +`--cfg anodized_discard_specs` where you need the spec to cost exactly nothing. + +A condition may carry one `#[cfg(...)]` attribute — and only `cfg`, never anything else, and +never on `captures`. + +```rust,ignore +// fragment +#[spec( + requires: !items.is_empty(), + #[cfg(debug_assertions)] + maintains: items.is_sorted(), +)] +``` + +## Helpers + +`anodized-logic` supplies vocabulary for conditions: `implies!(p, q)` for lazy material +implication, `int` for unbounded arithmetic, and `opaque!` plus `forall`/`exists` for terms +meant only for static backends — the last three panic if actually evaluated. + +## Adding a spec to existing code + +Read the function and list its real obligations. Write the smallest spec that states them. +Check it compiles with `cargo check`, then run the suite with checks live +(`RUSTFLAGS="--cfg anodized_panic" cargo test`). Format with `anodized-fmt` if available. +Finally re-read: delete any clause that only repeats the type. + +If a check fires, fix the side that is wrong — the caller for a precondition, the body for a +postcondition. Edit the spec only when it was genuinely wrong, and mind which direction. + +A postcondition that overclaimed may be weakened, or the precondition strengthened to exclude +the inputs where the guarantee fails; both keep the spec true of the code. A precondition that +was too strong may be weakened, but only once you have checked that the body really handles +the inputs it was rejecting — that is a new claim, not a relaxation. Weakening a precondition +cannot break an existing caller; the other two edits can. + +First check which clause actually failed, because the message does not say. A `maintains` +clause is checked on entry and again on exit, and it reports as `precondition failed` on the +way in and `postcondition failed` on the way out. So a `precondition failed` naming a +`maintains` clause is not a precondition at all, and weakening it is not the safe edit — +it relaxes the exit guarantee too. + +Only `anodized_print` puts the failing expression in the message; under `anodized_panic` alone +you get the bare text and a location pointing at the attribute, which names the function but +not the clause. Reproduce with both flags before deciding what failed. Matching the quoted +expression usually identifies the clause, though it cannot when two clauses are textually +identical, and the message reprints the tokens with normalized spacing. Say what you changed +and why. + +## Reference files + +Open a sibling file when its situation applies, not by default: + +| Situation | File | +| --- | --- | +| A `#[spec]` fails to compile, or a check fires | `diagnostics.md` | +| Someone writes `old()`, `result`, or names another contract crate; code predates 0.6 | `migration.md` | +| You need the exact grammar, or the semantics behind a clause | `reference.md` | +| You need a correct spec for a given item kind to copy | `examples.md` | diff --git a/plugins/anodized/skills/anodized/diagnostics.md b/plugins/anodized/skills/anodized/diagnostics.md new file mode 100644 index 00000000..92003e09 --- /dev/null +++ b/plugins/anodized/skills/anodized/diagnostics.md @@ -0,0 +1,163 @@ +# Anodized diagnostics + +What the compiler tells you, what provoked it, and what to do. Three sources of error matter: +the macro's own messages, ordinary rustc errors reached *through* a spec, and runtime check +failures. + +## Macro errors + +The macro accumulates errors, so several clause problems surface at once. + + +| Message | Cause | Fix | +| --- | --- | --- | +| ``unknown spec field`` | A clause name the parser does not recognize, often a guess from another crate. | Use one of `requires`, `maintains`, `captures`, `ensures`, `decreases`, or a qualifier. | +| ``fields are out of order: the expected order is`` | Clauses are present but in the wrong sequence. | Reorder to qualifiers, `requires`, `maintains`, `captures`, `ensures`. | +| ``at most one `captures` field is allowed`` | Two `captures:` fields in one spec. | Merge them: `captures: [first = a, second = b]`. | +| ``no longer supported, use the following form instead`` | `binds:` or `inspects:`, both removed. | Write `ensures: |PAT| [EXPR, ...]` instead. | +| ``postcondition closure must have exactly one input`` | An `ensures` closure taking zero or several inputs. | Take exactly the return value: `ensures: |output| ...`. | +| ``qualifier does not take a value`` | A qualifier written as `pure: true`. | Write it bare: `pure,`. | +| ``this qualifier is redundant; remove it`` | A composite qualifier alongside one of its components. | Keep the composite alone; `pure` already implies `deterministic` and `effectfree`. | +| ``attributes are not supported here`` | An attribute on a qualifier. | Remove it; only conditions accept `#[cfg]`. | +| ``unsupported attribute; only `cfg` is allowed`` | An attribute other than `#[cfg]` on a clause. | Remove it. | +| ``multiple `cfg` attributes are not supported`` | Two `#[cfg]` attributes on one clause. | Combine them: `#[cfg(all(test, debug_assertions))]`. | +| ```cfg` attribute is not supported here`` | A `#[cfg]` on `captures`. | Gate the postconditions that read the capture instead. | +| ``multiple `decreases` fields are not allowed`` | Two loop variants. | Keep one expression. | +| ``multiple `#[spec]` attributes on a single item are not supported`` | Two `#[spec]` attributes stacked on one item. | Merge the clauses into one attribute. | +| ``expected an expression`` | A clause whose value is not an expression. | Supply a `bool` expression, or a list of them. | +| ``expected an assignment`` | A `captures` entry that is not `pattern = expression`. | Write `captures: name = expr`. | +| ``expected an assignment or block`` | A `captures` value that is neither an assignment nor a block. | Write `captures: name = expr`, or a list of assignments. | +| ``expected a single expression`` | `decreases` given a list. | Supply one expression. | +| ``not allowed here due to `#[spec]``` | A trait function parameter pattern the macro cannot forward. | Name the parameter; avoid `_`, `..`, `ref`, and macro patterns. | +| ``or-pattern not allowed here due to `#[spec]``` | An or-pattern in a trait function parameter. | Name the parameter and match inside the body. | +| ``The enclosing trait must have a `#[spec]` annotation.`` | Clauses on a trait function whose trait carries no `#[spec]`. | Add a bare `#[spec]` to the trait. | +| ``Unsupported spec element on trait.`` | Clauses on the `#[spec]` attached to a trait. | Keep the trait's attribute bare; put clauses on its functions. | +| ``Unsupported spec element on trait impl.`` | Clauses on the `#[spec]` attached to an `impl Trait for T`. | Keep it bare; put clauses on the functions. | +| ``Unsupported spec element on inherent impl.`` | Clauses on the `#[spec]` attached to an inherent `impl`. | Keep it bare; put clauses on the methods. | +| ``cannot be weaker than the qualifiers on the trait`` | An impl claiming fewer guarantees than the trait promised. | An impl may only narrow; restore the trait's qualifiers. | +| ``The #[spec] attribute doesn't yet support this item`` | `#[spec]` on an item kind with no support, such as `mod` or `type`. | Move it to a supported item. | +| ```try_call` needs the `anodized_try` build `cfg` to be enabled`` | `try_call!` without the build configuration that generates its entry points. | Build with `--cfg anodized_try` and `--cfg anodized_panic`. | +| ``precondition failed`` | At runtime: the caller broke the contract. | Fix the call site, or the precondition if it was wrong. | +| ``postcondition failed`` | At runtime: the implementation broke its own contract. | Fix the body, or the postcondition if it was wrong. | + + +One wording to be aware of: the out-of-order message for function fields still lists +`inspects`, a clause that no longer exists. Ignore that entry and use the order +qualifiers, `requires`, `maintains`, `captures`, `ensures`. + +## Rustc errors reached through a spec + +These are the confusing ones, because nothing in the message mentions Anodized. + +**`E0596: cannot borrow as mutable`** — a condition tried to mutate something. Every condition +is coerced to `Fn() -> bool` through `anodized::__::eval`, and an `FnMut` body cannot satisfy +`Fn`. Conditions must observe, never change. This includes the right-hand side of a +`captures` entry. + +**`E0425: cannot find value`** — one of three things. A capture was read from `requires` or +from the function body, where it is not in scope. Or a postcondition named `output` or +`result` without binding it, expecting an implicit binding that does not exist. Or the code +predates 0.6 and expects an automatic `old_` binding, which was removed. + +**`E0308: mismatched types`** — a condition is not `bool` (every one is checked as +`eval::`), or an `ensures` closure's pattern does not match the return type. Also +appears as *expected `bool`, found closure* when a closure is nested inside a list that is +already bound by a closure (`ensures: |pat| [a, |x| b]`), or when a pre-0.6 closure-form +precondition survives. Note that `ensures: [a, |pat| b]` is legal: a top-level element of an +unbound list may carry its own binding. + +**`E0562: `impl Trait` is not allowed in closure return types`** — the function returns +`impl Trait`. The macro evaluates the body inside a closure so that an early `return` cannot +skip the postconditions, and a closure cannot return `impl Trait`. There is no spelling of the +spec that avoids this: the function cannot carry `#[spec]` at all until it returns a named +type. Only `anodized_discard_specs`, which drops specs before they are expanded, still builds. + +```rust,compile_fail +// EXPECT: E0562 +use anodized::spec; + +#[spec] +fn counter() -> impl Iterator { + 0..3 +} +``` + +**`E0015: cannot call non-const closure in constant functions`** — the same closure wrapping, +reached from a `const fn`. The wrapper is not a const closure, so a `const fn` cannot carry a +spec either. As with `E0562`, the only build that survives is `anodized_discard_specs`. + +```rust,compile_fail +// EXPECT: E0015 +use anodized::spec; + +#[spec] +const fn double(value: u32) -> u32 { + value * 2 +} +``` + +**`captured variable cannot escape `FnMut` closure body`** — the same closure wrapping again, +reached from a function that returns a `&mut` borrowed from one of its parameters. The +reference cannot outlive the closure that produced it. Note this one carries **no error code**, +so it will not match a search by `E`-number. Returning a shared `&` is unaffected. + +```rust,compile_fail +// EXPECT: cannot escape `FnMut` closure body +use anodized::spec; + +#[spec] +fn first_mut(values: &mut Vec) -> &mut u8 { + &mut values[0] +} +``` + +**`E0046: not all trait items implemented, missing: `__anodized_...``** — an +`impl Trait for T` is missing its bare `#[spec]`. The trait's specs generate a mangled item the +impl is expected to supply, so the fix is to add `#[spec]` to the impl, never to implement the +named item yourself. + +**`E0507: cannot move out`** — an `ensures` closure took a non-`Copy` return value by move and +then used it in a way that needs ownership elsewhere. Bind by reference: `|ref output|`. + +## Runtime failures + +Checks only run when the build enables them. + +`precondition failed: ` means the **caller** broke the contract. Fix the call site, +unless the precondition was wrong. + +`postcondition failed: ` means the **implementation** broke its own contract. Fix the +body, unless the postcondition was wrong. + +Neither message names the clause kind, and a `maintains` clause borrows both: it is checked on +entry, where a violation reports as `precondition failed`, and again on exit, where it reports +as `postcondition failed`. Match the quoted expression against the spec before concluding +which kind of clause you are looking at — bearing in mind that the expression appears only +under `anodized_print`; `anodized_panic` alone reports the bare text with a location pointing +at the attribute, which identifies the function but not the clause. + +One consequence worth knowing under `anodized_print`, which continues after a violation: an +invariant already false on entry is reported again on exit, so a `postcondition failed` does +not always mean the body misbehaved — the body may never have had a valid starting state. + +Under `--cfg anodized_print` the message goes to stderr and execution continues. Under +`--cfg anodized_panic` it panics. Enabling both — the usual choice for a test suite — gives +the panic with the failing expression named in the printed message. To reproduce a report: + +```bash +RUSTFLAGS="--cfg anodized_print --cfg anodized_panic" cargo test +``` + +Never relax a clause to silence a check. Fix whichever side is actually wrong, and if the +clause really was wrong, say so explicitly in the commit message. + +## Loop and data specs do not fire + +Runtime checking is implemented for functions only. Loop invariants, loop variants, and +`struct` or `enum` invariants never execute, so a plainly false one will not fail a test — +never read a passing suite as evidence that one holds. + +Type-checking differs between them, which matters more than it sounds. A `struct` condition is +embedded and type-checked, so a typo in one is `E0425`. Loop and `enum` conditions are dropped +before they reach the compiler: a loop invariant naming an identifier that does not exist +anywhere compiles without complaint. Review those by eye; nothing else will. diff --git a/plugins/anodized/skills/anodized/examples.md b/plugins/anodized/skills/anodized/examples.md new file mode 100644 index 00000000..06ff3e85 --- /dev/null +++ b/plugins/anodized/skills/anodized/examples.md @@ -0,0 +1,300 @@ +# Anodized examples + +Correct, compiling specs for every supported item kind. Copy the shape closest to your case. +Every Rust block here is compiled by the workspace's test suite. + +## Free function + +```rust +use anodized::spec; + +#[spec( + requires: [!slice.is_empty(), index < slice.len()], + ensures: |output| output == slice[index], +)] +fn nth(slice: &[u32], index: usize) -> u32 { + slice[index] +} +``` + +## Capturing an entry-time value + +```rust +use anodized::spec; + +#[spec( + requires: counter < u32::MAX, + captures: before = counter, + ensures: |output| output == before + 1, +)] +fn bump(counter: u32) -> u32 { + counter + 1 +} +``` + +Several captures, and a clone for a non-`Copy` value: + +```rust +use anodized::spec; + +#[spec( + captures: [first = items.first().copied(), size = items.len()], + ensures: |ref output| [output.len() == size, output.last().copied() == first], +)] +fn reversed(items: Vec) -> Vec { + items.into_iter().rev().collect() +} +``` + +## Invariant on a mutable argument + +```rust +use anodized::spec; + +#[spec(maintains: !buffer.is_empty())] +fn overwrite_first(buffer: &mut Vec, value: u32) { + buffer[0] = value; +} +``` + +## Destructuring the return value + +```rust +use anodized::spec; + +#[spec( + requires: divisor != 0, + ensures: |(quotient, remainder)| remainder < divisor && quotient * divisor + remainder == dividend, +)] +fn divide(dividend: u32, divisor: u32) -> (u32, u32) { + (dividend / divisor, dividend % divisor) +} +``` + +## Returning a `Result` + +A non-`Copy` return value binds by reference: + +```rust +use anodized::spec; + +#[spec(ensures: |ref output| output.is_ok() == (divisor != 0))] +fn checked_divide(dividend: u32, divisor: u32) -> Result { + if divisor == 0 { + return Err("division by zero".to_owned()); + } + Ok(dividend / divisor) +} +``` + +## Several postconditions under one binding + +```rust +use anodized::spec; + +#[spec(ensures: |output| [output >= left, output >= right, output == left || output == right])] +fn larger(left: u32, right: u32) -> u32 { + if left > right { left } else { right } +} +``` + +## Qualifiers + +```rust +use anodized::spec; + +#[spec( + pure, + requires: exponent < 32, + ensures: |output| output >= 1, +)] +fn power_of_two(exponent: u32) -> u32 { + 1 << exponent +} +``` + +## Inherent `impl` + +The `impl` carries a bare attribute; the clauses live on the methods. + +```rust +use anodized::spec; + +struct Counter { + value: u32, +} + +#[spec] +impl Counter { + #[spec(ensures: |ref output| output.value == 0)] + fn new() -> Self { + Self { value: 0 } + } + + #[spec( + requires: self.value < u32::MAX, + captures: before = self.value, + ensures: |output| output == before + 1, + )] + fn increment(&mut self) -> u32 { + self.value += 1; + self.value + } +} +``` + +## Trait, with a narrowing impl + +```rust +use anodized::spec; + +#[spec] +trait Scale { + #[spec( + requires: factor > 0 && value <= u32::MAX / factor, + ensures: |output| output >= value, + )] + fn scale(&self, value: u32, factor: u32) -> u32; +} + +struct Doubling; + +#[spec] +impl Scale for Doubling { + fn scale(&self, value: u32, factor: u32) -> u32 { + value * factor + } +} + +struct Exact; + +#[spec] +impl Scale for Exact { + #[spec(ensures: |output| output == value * factor)] + fn scale(&self, value: u32, factor: u32) -> u32 { + value * factor + } +} +``` + +`Exact` narrows: it promises more than the trait did. An impl may never promise less. + +The second condition is doing real work. Without `value <= u32::MAX / factor` the trait would +accept inputs whose product does not fit in a `u32`, and the natural multiplying implementation +cannot honor `output >= value` for them — it overflows first. (A saturating implementation +could, which is the point: a precondition defines what every implementation must cope with.) A +precondition that admits inputs the body cannot serve is a spec that is false of its own code. + +Note that it is one `&&` condition rather than two list entries. Conditions in a list are +checked independently and do not short-circuit, so a separate `value <= u32::MAX / factor` +would divide by zero while being checked whenever `factor` is `0` — a spec that panics during +its own evaluation. When one condition guards another, join them with `&&`. + +## `while` loop + +```rust +use anodized::spec; + +#[spec(requires: !items.is_empty())] +fn maximum(items: &[u32]) -> u32 { + let mut best = items[0]; + let mut index = 1; + #[spec( + maintains: index <= items.len(), + decreases: items.len() - index, + )] + while index < items.len() { + if items[index] > best { + best = items[index]; + } + index += 1; + } + best +} +``` + +## `for` loop + +```rust +use anodized::spec; + +#[spec(ensures: |output| output <= items.len())] +fn count_zeros(items: &[u32]) -> usize { + let mut count = 0usize; + #[spec(maintains: count <= items.len())] + for item in items { + if *item == 0 { + count += 1; + } + } + count +} + +fn main() { + assert_eq!(count_zeros(&[]), 0); + assert_eq!(count_zeros(&[0, 0]), 2); + assert_eq!(count_zeros(&[1, 0, 3]), 1); +} +``` + +Note what the bound avoids. An upper bound like `u64::from(u32::MAX) * items.len() as u64` +reads naturally for a sum, but the condition itself would overflow on a long enough slice, and +a spec that can panic while being checked is worse than none. `count <= items.len()` cannot. + +The `fn main` is not decoration. Compiling an example proves its conditions are well-formed; +only running one proves they are true of the code beside them. Exercise the boundaries — here +the empty slice and the all-zero slice, which are exactly where a plausible-looking lower bound +on the sum would have been false. + +## `struct` refinement + +```rust +use anodized::spec; + +#[spec(maintains: self.low <= self.high)] +struct Bounds { + low: u32, + high: u32, +} +``` + +## `enum` refinement + +Variants are in scope inside the condition. + +```rust +use anodized::spec; + +#[spec(maintains: match self { Temperature::Celsius(degrees) => *degrees >= -273, Temperature::Kelvin(degrees) => *degrees >= 0 })] +enum Temperature { + Celsius(i32), + Kelvin(i32), +} +``` + +## A condition compiled only for tests + +```rust +use anodized::spec; + +#[spec( + requires: !items.is_empty(), + #[cfg(debug_assertions)] + ensures: |output| items.contains(&output), +)] +fn first(items: &[u32]) -> u32 { + items[0] +} +``` + +## Using `implies!` + +```rust +use anodized::spec; +use anodized::logic::implies; + +#[spec(ensures: |output| implies!(divisor != 0, output <= dividend))] +fn safe_divide(dividend: u32, divisor: u32) -> u32 { + if divisor == 0 { 0 } else { dividend / divisor } +} +``` diff --git a/plugins/anodized/skills/anodized/migration.md b/plugins/anodized/skills/anodized/migration.md new file mode 100644 index 00000000..22df0fe1 --- /dev/null +++ b/plugins/anodized/skills/anodized/migration.md @@ -0,0 +1,95 @@ +# Migrating to Anodized + +Every contract system spells the same ideas differently. This file translates. If you are +about to write something remembered from elsewhere, find it here first. + +## From Anodized 0.5 or earlier + +**Start here.** 0.6 changed the syntax, so a model's or a codebase's memory of this crate is +more likely to be stale than to be wrong about some other crate. + +| Before 0.6 | Now | +| --- | --- | +| `old_x` (automatic) | `captures: old_x = x`, read in `ensures` | +| `captures: x.len() as n` | `captures: n = x.len()` | +| `ensures: output > 0` | `ensures: \|output\| output > 0` | +| `binds: \|pat\| ...` | `ensures: \|pat\| [...]` | +| `inspects: ...` | `ensures: \|pat\| [...]` | +| `requires: \|\| condition` | `requires: condition` | + +The automatic `old_` binding is the one that bites hardest, because the replacement is not a +rename: captures must be declared, and they are visible only to postconditions. + +## From `contracts` + +| `contracts` | Anodized | +| --- | --- | +| `#[requires(x > 0)]` | `#[spec(requires: x > 0)]` | +| `#[ensures(ret > 0)]` | `#[spec(ensures: \|output\| output > 0)]` | +| `#[invariant(...)]` | `#[spec(maintains: ...)]` | +| `old(x)` | `captures: old_x = x` | +| separate attributes | one `#[spec(...)]` carrying every clause | + +## From Creusot + +| Creusot | Anodized | +| --- | --- | +| `#[requires(...)]` / `#[ensures(...)]` | clauses inside `#[spec(...)]` | +| `result` | the `ensures` closure's binding | +| `^x` (final value) | `maintains`, or a capture plus a postcondition | +| `pearlite!` terms | plain Rust expressions; `opaque!` for what cannot be written | +| `#[predicate]` / logic functions | ordinary pure Rust functions | + +## From Prusti + +| Prusti | Anodized | +| --- | --- | +| `#[requires(...)]` / `#[ensures(...)]` | clauses inside `#[spec(...)]` | +| `old(x)` | `captures: old_x = x` | +| `result` | the `ensures` closure's binding | +| `#[pure]` | the `pure` qualifier | +| `#[trusted]` | no equivalent; Anodized does not verify statically | +| `body_invariant!(...)` | `#[spec(maintains: ...)]` on the loop | + +## From Kani + +Closest cousin, and the closure form is genuinely similar — which makes the differences easy +to miss. + +| Kani | Anodized | +| --- | --- | +| `#[kani::requires(...)]` | `#[spec(requires: ...)]` | +| `#[kani::ensures(\|result\| ...)]` | `#[spec(ensures: \|output\| ...)]` | +| `old(...)` | `captures: name = ...` | +| `#[kani::modifies(...)]` | no equivalent | + +## From Verus + +| Verus | Anodized | +| --- | --- | +| `requires` / `ensures` blocks in the signature | clauses inside `#[spec(...)]` | +| `old(x)` | `captures: old_x = x` | +| `ret` | the `ensures` closure's binding | +| `invariant` on a loop | `#[spec(maintains: ...)]` | +| `decreases` on a loop | `#[spec(decreases: ...)]`, same idea | +| ghost/spec functions | ordinary Rust functions | + +## If you were about to write X + +| X | Write instead | +| --- | --- | +| `old(x)`, `old_x` | `captures: old_x = x` | +| `result`, bare `output` | `ensures: \|output\| ...` | +| `#[requires(...)]` above the fn | `#[spec(requires: ...)]` | +| `ensures: ret == ...` | `ensures: \|output\| output == ...` | +| `captures: expr as name` | `captures: name = expr` | +| `#[invariant(...)]` on a loop | `#[spec(maintains: ...)]` on the loop | +| a spec expression that mutates | rewrite it to observe only; conditions are `Fn` | +| `#[pure]` attribute | the bare `pure` qualifier inside `#[spec(...)]` | + +## What Anodized does not do + +It does not verify statically. `#[spec]` embeds a specification that the compiler type-checks +and that runtime checks can enforce; proving a postcondition for all inputs is the job of a +backend built on `anodized-core`, not of the macro. There is no `#[trusted]`, no proof +obligation, and no solver. diff --git a/plugins/anodized/skills/anodized/reference.md b/plugins/anodized/skills/anodized/reference.md new file mode 100644 index 00000000..2ac51f52 --- /dev/null +++ b/plugins/anodized/skills/anodized/reference.md @@ -0,0 +1,158 @@ +# Anodized reference + +Semantics behind the tables in `SKILL.md`. Read this when you need to know *why* a clause +behaves the way it does, or what exactly the parser accepts. + +## Grammar + + +```ebnf +fields = [ qualifiers ] + [ requires_fields ] + , [ maintains_fields ] + (* not a typo: at most one `captures:` *) + , [ captures_field ] + , [ ensures_fields ]; + +qualifiers = { qualifier }; +qualifier = `functional` | `pure` | `total` + | `deterministic` | `effectfree` | `infallible` | `terminating`; + +requires_fields = { requires_field }; +maintains_fields = { maintains_field }; +ensures_fields = { ensures_field }; + +requires_field = [ cfg_attr ] , `requires:` , conditions, `,`; +maintains_field = [ cfg_attr ] , `maintains:` , conditions, `,`; +captures_field = `captures:` , captures, `,`; +ensures_field = [ cfg_attr ] , `ensures:` , postconds, `,`; + +conditions = expr | condition_list; +condition_list = `[` , expr , { `,` , expr } , [ `,` ] , `]`; + +captures = capture_stmt | capture_list; +capture_list = `[` , capture_stmt , { `,` , capture_stmt } , [ `,` ] , `]`; +capture_stmt = pattern , `=` , expr; + +postconds = postcond_expr | postcond_list | postcond_list_closure; +postcond_list = `[` , postcond_expr , { `,` , postcond_expr } , [ `,` ] , `]`; +postcond_expr = expr | postcond_closure; +postcond_closure = `|` , pattern , `|` , expr; +postcond_list_closure = `|` , pattern , `|` , condition_list; + +cfg_attr = `#[cfg(` , settings , `)]`; +``` + + +Notes on reading it: `expr` is any Rust expression, `pattern` is any irrefutable Rust pattern, +and every field is parseable as a Rust struct-expression field — which is why the attribute +uses `name: value` and tolerates a trailing comma. `decreases` is absent from the function +fields on purpose: it belongs to loops only. + +## How a spec is instrumented + +The macro rewrites the body into something equivalent to this: + +1. Preconditions and invariants are checked. +2. Captures and the body are evaluated in a **single tuple assignment**, so the body cannot + see the captured values, and the body runs inside a closure so an early `return` cannot + skip the postconditions. +3. Invariants are checked again, then postconditions, with the captures and the return value + in scope. +4. The return value is produced. + +Two consequences follow, and both surface as ordinary compiler errors rather than as +Anodized-specific ones. Conditions are invoked through `anodized::__::eval`, which takes an +`impl Fn() -> T`: a condition that mutates anything cannot satisfy `Fn`, so it fails to +compile. And captures are bound in the same statement that runs the body, so they cannot be +named by the body or by a precondition. + +## Clauses + +**`requires`** — checked on entry, before captures. One condition or a list. + +**`maintains`** — checked twice, on entry and again on exit. On a `fn` it usually describes +`&self` or a `&mut` parameter. On a `struct` or `enum` it is a refinement on the type itself. + +**`captures`** — evaluated after `requires`, before the body. At most one field per spec; use +`captures: [a = x, b = y]` for several. The right-hand side is moved, not copied, so a +non-`Copy` value needs `.clone()`. The left-hand side is any irrefutable pattern, including +tuples and struct patterns. Captures are visible **only** to postconditions. + +**`ensures`** — checked after the body and after the exit invariants. The return value is +bound only by a closure pattern; a bare expression cannot see it. Within a list, each element +may carry its own closure. + +**`decreases`** — loops only, one expression, at most one field. States the quantity that +strictly decreases and is bounded below. + +Ordering is mandatory and enforced by the parser: qualifiers, `requires`, `maintains`, +`captures`, `ensures`; and for loops, `maintains` then `decreases`. Repeating `requires`, +`maintains`, or `ensures` is allowed, and the conditions accumulate. + +## Conditional compilation of a clause + +Any of `requires`, `maintains`, `ensures`, and `decreases` may carry exactly one `#[cfg(...)]` +attribute. No other attribute is accepted, and `captures` accepts none at all. A gated +condition is still type-checked when its check is compiled out, which is what makes +`#[cfg(test)]` and `#[cfg(debug_assertions)]` safe places to put an expensive invariant. + +## Traits + +Trait functions are rewritten to a `__anodized_`-prefixed name with a generated default that +carries the checks. That is why the two structural attributes are required: a bare +`#[spec]` on the trait, and a bare `#[spec]` on each impl. Clauses on the trait's functions and +narrowing clauses on an impl's functions are both optional — a function with no attribute +simply has an empty spec. Omitting an impl's bare `#[spec]` does not silently skip +instrumentation; it fails to compile with `E0046`, naming the generated `__anodized_` item as +unimplemented. + +Qualifiers on an impl may not be weaker than on the trait, and this is enforced at build time +by a generated `const { assert!(...) }`. Pre- and postcondition narrowing is a contract you +are trusted to honor; only runtime checks will catch a violation. + +Trait function parameters must be patterns the macro can forward: names, tuples, tuple +structs, struct patterns, slices, literals, paths, ranges, references. It rejects `_`, `..`, +or-patterns, macro patterns, `ref` bindings, and struct patterns with `..`. + +## `try_call!` and `anodized::result` + +With `--cfg anodized_try` (which requires `--cfg anodized_panic`), `try_call!` wraps a call so +a violation becomes a `Result` instead of a panic, distinguishing precondition from +postcondition failure. It accepts a method call or a **qualified** function call — +`path::f(..)`, `Type::f(..)`, `::f(..)`, `recv.m(..)` — but not a bare `f(x)`. This is +what lets property-based testing discard invalid inputs without also swallowing genuine +postcondition failures. + +## `anodized-logic` + +- `implies!(p, q)` — material implication, evaluating `q` lazily. A macro because arguments + are otherwise eager. +- `int` — unbounded integer with operator interop across the primitive integer types, for + conditions that would otherwise overflow. +- `opaque!(tokens)` — a term whose meaning is defined by an analysis backend. +- `forall` / `exists` — quantifiers for static backends. + +`opaque!`, `forall`, and `exists` **panic** if evaluated at runtime. They belong in conditions +that a backend interprets, not in ones a test executes. + +## `anodized-fmt` + +A formatter for `#[spec(...)]` blocks, configured by `anodized-fmt.toml`. Install with +`cargo install anodized-fmt`; it normalizes clause layout and ordering so specs read +consistently across a codebase. + +## Removed, or never there + +| Form | Status | +| --- | --- | +| `old(x)` | Never existed. Use `captures`. | +| `old_x` | Removed in 0.6. Use `captures: old_x = x`. | +| `result` / bare `output` | Never existed. Bind with an `ensures` closure. | +| `captures: expr as pattern` | Removed in 0.6. Now `pattern = expression`. | +| `binds:` / `inspects:` | Removed in 0.6. Use `ensures: \|PAT\| [EXPR, ...]`. | +| `#[requires(...)]` / `#[ensures(...)]` | Never existed. One unified `#[spec(...)]`. | +| Closure-form preconditions | Removed in 0.6. Write the expression directly. | + +The parser still recognizes `binds` and `inspects` purely so it can tell you what replaced +them; they are scheduled for deletion before 0.7. From e618e29816dd1460346e5e9cc971e7160a9646ba Mon Sep 17 00:00:00 2001 From: Slava Barinov Date: Wed, 26 Aug 2026 00:55:26 +0900 Subject: [PATCH 02/10] [anodized] docs: repair the examples in REFERENCE.md - Bind the return value; a bare `ensures` cannot see it. - Drop the `*output` deref, which no longer type-checks. - Guard the conditions that were false at an empty slice or a maximum. - Say that discarding specs, not merely disabling checks, costs nothing. --- crates/anodized/REFERENCE.md | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/crates/anodized/REFERENCE.md b/crates/anodized/REFERENCE.md index 44c01bd0..22b89b99 100644 --- a/crates/anodized/REFERENCE.md +++ b/crates/anodized/REFERENCE.md @@ -30,7 +30,7 @@ RUSTFLAGS="--cfg anodized_print" cargo test Disable embedding the specs as Rust code. -**Important:** This has **no effect on runtime performance** because the embedded specs are always dead code. On the other hand, it **prevents syntax/type checking** specs, so it may decrease compilation time. +**Important:** This is the only configuration in which a spec costs exactly nothing. Conditions are dead code whenever checks are disabled, but `captures` expressions are bound alongside the body and so are evaluated on every call regardless — a `.clone()` in a capture is a real clone. Discarding specs also **prevents syntax/type checking** them, so it may decrease compilation time. ## Runtime Checks @@ -67,12 +67,12 @@ use anodized::spec; // Runtime checks only in debug builds (like `debug_assert!`) #[cfg(debug_assertions)] - ensures: output.is_ok(), + ensures: |ref output| output.is_ok(), )] fn perform_complex_operation(input: i32) -> Result { todo!() } ``` -The `#[cfg]` attribute follows standard Rust semantics: when the configuration predicate is false, the runtime check for the condition is completely omitted. +The `#[cfg]` attribute follows standard Rust semantics: when the configuration predicate is false, the runtime check for the condition is completely omitted. This holds in every build configuration that runs checks, whether or not `anodized_print` is enabled. **Important:** Anodized guarantees that each condition remains syntactically valid and type-correct regardless of its `#[cfg]` settings. This prevents conditions from becoming invalid between different build configurations, and keeps the entire spec always visible to analysis tools. @@ -115,7 +115,7 @@ use anodized::spec; // Invariant: length never exceeds capacity maintains: vec.len() <= vec.capacity(), )] -fn push_checked(vec: &mut Vec, value: T) { todo!() } +fn push_checked(vec: &mut Vec, value: T) { vec.push(value) } ``` ### `captures`: Capture Entry-Time Values @@ -126,6 +126,7 @@ Sometimes postconditions need to compare the function's final state with its ini use anodized::spec; #[spec( + requires: !items.is_empty(), captures: [ // Copy types: captured directly orig_len = items.len(), @@ -187,6 +188,7 @@ reconstructed. use anodized::spec; #[spec( + requires: input < i32::MAX - 1, // Bind the return value to `output` for the entire group of postconditions. ensures: |output| [ output > input, @@ -223,7 +225,7 @@ fn sort_pair(pair: (i32, i32)) -> (i32, i32) { todo!() } use anodized::spec; #[spec( - requires: *balance >= amount, + requires: amount >= 0 && *balance >= amount, maintains: *balance >= 0, captures: initial_balance = *balance, ensures: |(new_balance, receipt_amount)| [ @@ -232,7 +234,7 @@ use anodized::spec; *balance == new_balance, ], )] -fn withdraw(balance: &mut u64, amount: u64) -> (u64, u64) { todo!() } +fn withdraw(balance: &mut i64, amount: i64) -> (i64, i64) { todo!() } ``` ### Loop Specs @@ -250,9 +252,10 @@ Loop specs support the following fields: use anodized::spec; #[spec( - ensures: [ - seq.iter().any(|elem| elem == output), - seq.iter().all(|elem| elem <= output), + requires: !seq.is_empty(), + ensures: |output| [ + seq.iter().any(|elem| *elem == output), + seq.iter().all(|elem| *elem <= output), ], )] fn find_maximum(seq: &[u8]) -> u8 { @@ -278,10 +281,10 @@ use anodized::spec; #[spec( requires: seq.is_sorted(), - ensures: [ - *output <= seq.len(), - seq[0..*output].iter().all(|item| item < value), - seq[*output..].iter().all(|item| item >= value), + ensures: |output| [ + output <= seq.len(), + seq[0..output].iter().all(|item| item < value), + seq[output..].iter().all(|item| item >= value), ], )] fn find_insert_position(seq: &[T], value: &T) -> usize { @@ -323,6 +326,7 @@ trait MonotonicGenerator { fn current(&self) -> i32; #[spec( + requires: self.current() < i32::MAX, captures: old_val = self.current(), ensures: self.current() > old_val, )] @@ -386,7 +390,6 @@ use anodized::spec; Descending(vec) => vec.iter().rev().is_sorted(), } )] -#[allow(unused)] enum MonotonicVec { Ascending(Vec), Descending(Vec), From eec470b4a3d30e5eb72194abf0ae4ad689694461 Mon Sep 17 00:00:00 2001 From: Slava Barinov Date: Wed, 26 Aug 2026 00:55:36 +0900 Subject: [PATCH 03/10] [skill-tools] feat: generate and validate the agent skill - Render the clause, qualifier, item, and `cfg` tables from the crates. - Match `Keyword` without a wildcard, so a new clause breaks the build. - Compile every Rust example, and drive each one over its admitted inputs with checks enabled, asserting what its spec refuses. - Assert the plugin manifests agree with the workspace version. --- Cargo.toml | 2 + crates/skill-tools/Cargo.toml | 17 + crates/skill-tools/src/bin/skill-gen.rs | 53 +++ crates/skill-tools/src/fences.rs | 196 +++++++++++ crates/skill-tools/src/generate.rs | 430 ++++++++++++++++++++++++ crates/skill-tools/src/lib.rs | 283 ++++++++++++++++ crates/skill-tools/src/scratch.rs | 122 +++++++ crates/skill-tools/tests/coverage.rs | 193 +++++++++++ crates/skill-tools/tests/drivers.rs | 252 ++++++++++++++ crates/skill-tools/tests/examples.rs | 257 ++++++++++++++ crates/skill-tools/tests/generated.rs | 48 +++ crates/skill-tools/tests/manifests.rs | 232 +++++++++++++ crates/skill-tools/tests/runtime.rs | 104 ++++++ 13 files changed, 2189 insertions(+) create mode 100644 crates/skill-tools/Cargo.toml create mode 100644 crates/skill-tools/src/bin/skill-gen.rs create mode 100644 crates/skill-tools/src/fences.rs create mode 100644 crates/skill-tools/src/generate.rs create mode 100644 crates/skill-tools/src/lib.rs create mode 100644 crates/skill-tools/src/scratch.rs create mode 100644 crates/skill-tools/tests/coverage.rs create mode 100644 crates/skill-tools/tests/drivers.rs create mode 100644 crates/skill-tools/tests/examples.rs create mode 100644 crates/skill-tools/tests/generated.rs create mode 100644 crates/skill-tools/tests/manifests.rs create mode 100644 crates/skill-tools/tests/runtime.rs diff --git a/Cargo.toml b/Cargo.toml index a8dac786..05f6e1d0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,6 +5,7 @@ members = [ "crates/anodized-fmt", "crates/anodized-logic", "crates/anodized-macros", + "crates/skill-tools", "crates/test-util", "fuzz", ] @@ -33,6 +34,7 @@ keywords = [ ] [workspace.dependencies] +anodized = { version = "0.6.0", path = "crates/anodized" } anodized-core = { version = "0.6.0", path = "crates/anodized-core" } anodized-fmt = { version = "0.6.0", path = "crates/anodized-fmt" } anodized-logic = { version = "0.6.0", path = "crates/anodized-logic" } diff --git a/crates/skill-tools/Cargo.toml b/crates/skill-tools/Cargo.toml new file mode 100644 index 00000000..be7c63ae --- /dev/null +++ b/crates/skill-tools/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "skill-tools" +description = "Generates and validates the Anodized agent skill and its plugin manifests" +publish = false + +version.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true +repository.workspace = true + +[dependencies] +anodized-core.workspace = true +serde_json = "1" + +[dev-dependencies] +anodized.workspace = true diff --git a/crates/skill-tools/src/bin/skill-gen.rs b/crates/skill-tools/src/bin/skill-gen.rs new file mode 100644 index 00000000..60b84bb1 --- /dev/null +++ b/crates/skill-tools/src/bin/skill-gen.rs @@ -0,0 +1,53 @@ +//! Rewrites, or verifies, the generated tables in the Anodized agent skill. + +use std::process::ExitCode; + +use skill_tools::generate; + +fn main() -> ExitCode { + let mode = std::env::args().nth(1); + match mode.as_deref() { + Some("--write") => run(write), + Some("--check") | None => run(check), + Some(other) => { + eprintln!("unknown argument `{other}`; expected `--write` or `--check`"); + ExitCode::FAILURE + } + } +} + +fn run(action: fn() -> skill_tools::Result) -> ExitCode { + match action() { + Ok(true) => ExitCode::SUCCESS, + Ok(false) => ExitCode::FAILURE, + Err(error) => { + eprintln!("error: {error}"); + ExitCode::FAILURE + } + } +} + +fn write() -> skill_tools::Result { + let changed = generate::write()?; + if changed.is_empty() { + println!("generated regions are already up to date"); + } else { + for file in changed { + println!("updated {file}"); + } + } + Ok(true) +} + +fn check() -> skill_tools::Result { + let stale = generate::check()?; + if stale.is_empty() { + println!("generated regions are up to date"); + return Ok(true); + } + for region in stale { + eprintln!("stale generated region: {region}"); + } + eprintln!("run `cargo run -p skill-tools --bin skill-gen -- --write`"); + Ok(false) +} diff --git a/crates/skill-tools/src/fences.rs b/crates/skill-tools/src/fences.rs new file mode 100644 index 00000000..b0f43394 --- /dev/null +++ b/crates/skill-tools/src/fences.rs @@ -0,0 +1,196 @@ +//! Extracts fenced code blocks from the skill's markdown. +//! +//! Every Rust block in the skill is compiled by the integration tests, so the info string on a +//! fence is a contract rather than a hint: it declares what the block is for, and an +//! unrecognized one is an error instead of a silent skip. + +use std::fmt; + +use crate::Result; + +/// What a fence's info string declares about its block. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Kind { + /// Rust that must compile, and — when it carries a `fn main` — must also run with checks + /// enabled without tripping one of its own conditions. + Pass, + /// Rust that must compile. Identical treatment to [`Kind::Pass`]; the tag exists because + /// `REFERENCE.md` already uses it. + CompileOnly, + /// Rust that must fail to compile, with the error code the block declares. + CompileFail, + /// A deliberate fragment, excluded from compilation. + Fragment, + /// Not Rust. + Other, +} + +/// A fenced block, with its position for error reporting. +#[derive(Debug, Clone)] +pub struct Fence { + /// The markdown file the block came from. + pub file: String, + /// The line the opening fence sits on, 1-based. + pub line: usize, + /// The info string, normalized. + pub info: String, + /// What the info string declares. + pub kind: Kind, + /// The block's contents, without the fences. + pub body: String, + /// The nearest `##` heading above the block. + pub heading: String, +} + +impl fmt::Display for Fence { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}:{}", self.file, self.line) + } +} + +impl Fence { + /// The rustc error code a `compile_fail` block declares on its first line. + /// + /// The declaration is what keeps the block honest: without it, a block that fails for an + /// unrelated reason would pass just as happily as one that fails for the documented one. + pub fn expected_error(&self) -> Result { + let first = self.body.lines().next().unwrap_or_default().trim(); + first + .strip_prefix("// EXPECT:") + .map(|code| code.trim().to_owned()) + .filter(|code| !code.is_empty()) + .ok_or_else(|| { + format!("{self}: a `compile_fail` block must start with `// EXPECT: `").into() + }) + } + + /// Whether a fragment declares itself as one. + #[must_use] + pub fn is_labelled_fragment(&self) -> bool { + self.body + .lines() + .next() + .is_some_and(|line| line.trim_start().starts_with("// fragment")) + } + + /// The nearest `##` heading above this block, used to key its driver. + #[must_use] + pub fn heading(&self) -> &str { + &self.heading + } + + /// Whether the block exercises itself, and so can be run rather than only compiled. + /// + /// Compiling proves a spec is well-formed. Only running it proves the spec is *true of the + /// code*: an example once shipped here promised `output >= items.len()` from a sum that is + /// zero for an all-zero slice, which compiled perfectly and panicked on the first honest + /// input. + #[must_use] + pub fn is_self_exercising(&self) -> bool { + self.body.contains("fn main(") + } + + /// The block as a compilable unit, with the import a snippet omits. + /// + /// No `fn main` is appended: blocks are compiled as a library, because they are item-level + /// and a binary crate would fail with `E0601` before reaching the spec. + #[must_use] + pub fn as_program(&self) -> String { + // Two lints are artifacts of a snippet being illustrative rather than complete: an + // example item nobody calls, and a `todo!()` body that never reads its parameters. + // Every other warning fails the build, so an example cannot teach code that warns — + // which is how the tautological `output >= 0` on a `u64` was caught. + let mut source = String::from("#![allow(dead_code, unused_variables)]\n"); + if !self.body.contains("use anodized::spec;") { + source.push_str("use anodized::spec;\n"); + } + source.push_str(&self.body); + source + } +} + +/// Classifies an info string, normalizing whitespace first. +/// +/// Normalization matters: `REFERENCE.md` writes `rust, no_run` with a space, and rejecting it +/// over the space would mean rewriting a dozen fences to gain nothing. +pub fn classify(info: &str) -> Result { + let normalized: String = info.chars().filter(|c| !c.is_whitespace()).collect(); + match normalized.as_str() { + "rust" => Ok(Kind::Pass), + "rust,no_run" => Ok(Kind::CompileOnly), + "rust,compile_fail" => Ok(Kind::CompileFail), + "rust,ignore" => Ok(Kind::Fragment), + "" | "text" | "toml" | "bash" | "sh" | "json" | "yaml" | "ebnf" | "diff" | "console" => { + Ok(Kind::Other) + } + other => Err(format!( + "unknown fence tag `{other}`; extend `skill_tools::fences::classify` deliberately \ + rather than adding an untracked tag" + ) + .into()), + } +} + +/// Extracts every fenced block from a markdown document. +/// +/// Blocks inside the YAML frontmatter are not fences and are skipped along with it. +pub fn extract(file: &str, text: &str) -> Result> { + let mut fences = Vec::new(); + let mut lines = text.lines().enumerate().peekable(); + + if text.starts_with("---\n") { + lines.next(); + for (_, line) in lines.by_ref() { + if line.trim_end() == "---" { + break; + } + } + } + + let mut heading = String::new(); + while let Some((index, line)) = lines.next() { + if let Some(title) = line.strip_prefix("## ") { + heading = title.trim().to_owned(); + } + let Some(info) = line.strip_prefix("```") else { + continue; + }; + let kind = classify(info)?; + let mut body = String::new(); + let mut closed = false; + for (_, inner) in lines.by_ref() { + if inner.starts_with("```") { + closed = true; + break; + } + body.push_str(inner); + body.push('\n'); + } + if !closed { + return Err(format!("{file}:{}: unclosed code fence", index + 1).into()); + } + fences.push(Fence { + file: file.to_owned(), + line: index + 1, + info: info.trim().to_owned(), + kind, + body, + heading: heading.clone(), + }); + } + + Ok(fences) +} + +/// Extracts the single block carrying the given info string. +pub fn extract_one(file: &str, text: &str, info: &str) -> Result { + let matching: Vec<_> = extract(file, text)? + .into_iter() + .filter(|fence| fence.info == info) + .collect(); + match matching.as_slice() { + [fence] => Ok(fence.body.clone()), + [] => Err(format!("{file}: expected one `{info}` block, found none").into()), + many => Err(format!("{file}: expected one `{info}` block, found {}", many.len()).into()), + } +} diff --git a/crates/skill-tools/src/generate.rs b/crates/skill-tools/src/generate.rs new file mode 100644 index 00000000..f8374bd7 --- /dev/null +++ b/crates/skill-tools/src/generate.rs @@ -0,0 +1,430 @@ +//! Renders the skill's factual tables from this workspace, and keeps them in sync. +//! +//! Only the tables are generated. The prose around them is written by hand, because the +//! reason a clause exists is not derivable from the enum that names it. Each table lives +//! between a pair of markers, and everything outside those markers is left untouched. + +use std::collections::BTreeSet; +use std::fmt::Write as _; + +use anodized_core::qualifiers::FnQualifiers; + +use crate::{ + CFG_FLAGS, DIAGNOSTICS, KeywordDoc, Result, all_keywords, documented_keyword, read, + read_skill_file, repo_root, skill_dir, +}; + +/// A generated region: the file that holds it and the identifier that names it. +/// +/// Each identifier appears exactly once. An earlier draft rendered the same table into two +/// files and added a test to prove the copies matched, which was machinery guarding a +/// duplication that told the reader nothing new the second time. +pub const REGIONS: &[(&str, &str)] = &[ + ("SKILL.md", "clauses"), + ("SKILL.md", "qualifiers"), + ("SKILL.md", "item-kinds"), + ("SKILL.md", "cfg-flags"), + ("reference.md", "ebnf"), + ("diagnostics.md", "diagnostics"), +]; + +/// Build configurations, paired with what each one does. +pub const CFG_EFFECTS: &[(&str, &str)] = &[ + ( + "anodized_discard_specs", + "Specs are dropped entirely: not embedded, not type-checked. Fastest builds.", + ), + ( + "anodized_print", + "A violated condition reports to stderr and execution continues.", + ), + ( + "anodized_panic", + "A violated condition panics, without naming the condition. Pair with \ + `anodized_print` to be told which expression failed.", + ), + ( + "anodized_try", + "Enables `try_call!`, which turns a violation into a `Result`. Requires `anodized_panic`.", + ), +]; + +/// Item kinds, with the clauses each accepts and how the attribute is applied. +pub const ITEM_KINDS: &[(&str, &str, &str)] = &[ + ("free `fn`", "all clauses", "`#[spec(...)]` on the `fn`"), + ( + "inherent `impl`", + "all clauses, per method", + "bare `#[spec]` on the `impl`, clauses on each `fn`", + ), + ( + "`trait`", + "all clauses, per method", + "bare `#[spec]` on the `trait`, clauses on each `fn`", + ), + ( + "`impl Trait for T`", + "all clauses, narrowing only", + "bare `#[spec]` on the `impl`, optional clauses on each `fn`", + ), + ( + "`while` / `for`", + "`maintains`, `decreases`", + "`#[spec(...)]` on the loop, inside a spec'd `fn`", + ), + ("`struct`", "`maintains`", "`#[spec(...)]` on the `struct`"), + ("`enum`", "`maintains`", "`#[spec(...)]` on the `enum`"), +]; + +/// Diagnostics, each with what provoked it and what to do about it. +/// +/// The message column is verbatim, so a test can assert both that `diagnostics.md` documents +/// it and that the macro still emits it. +pub const DIAGNOSTIC_DOCS: &[(&str, &str, &str)] = &[ + ( + "unknown spec field", + "A clause name the parser does not recognize, often a guess from another crate.", + "Use one of `requires`, `maintains`, `captures`, `ensures`, `decreases`, or a qualifier.", + ), + ( + "fields are out of order: the expected order is", + "Clauses are present but in the wrong sequence.", + "Reorder to qualifiers, `requires`, `maintains`, `captures`, `ensures`.", + ), + ( + "at most one `captures` field is allowed", + "Two `captures:` fields in one spec.", + "Merge them: `captures: [first = a, second = b]`.", + ), + ( + "no longer supported, use the following form instead", + "`binds:` or `inspects:`, both removed.", + "Write `ensures: |PAT| [EXPR, ...]` instead.", + ), + ( + "postcondition closure must have exactly one input", + "An `ensures` closure taking zero or several inputs.", + "Take exactly the return value: `ensures: |output| ...`.", + ), + ( + "qualifier does not take a value", + "A qualifier written as `pure: true`.", + "Write it bare: `pure,`.", + ), + ( + "this qualifier is redundant; remove it", + "A composite qualifier alongside one of its components.", + "Keep the composite alone; `pure` already implies `deterministic` and `effectfree`.", + ), + ( + "attributes are not supported here", + "An attribute on a qualifier.", + "Remove it; only conditions accept `#[cfg]`.", + ), + ( + "unsupported attribute; only `cfg` is allowed", + "An attribute other than `#[cfg]` on a clause.", + "Remove it.", + ), + ( + "multiple `cfg` attributes are not supported", + "Two `#[cfg]` attributes on one clause.", + "Combine them: `#[cfg(all(test, debug_assertions))]`.", + ), + ( + "`cfg` attribute is not supported here", + "A `#[cfg]` on `captures`.", + "Gate the postconditions that read the capture instead.", + ), + ( + "multiple `decreases` fields are not allowed", + "Two loop variants.", + "Keep one expression.", + ), + ( + "multiple `#[spec]` attributes on a single item are not supported", + "Two `#[spec]` attributes stacked on one item.", + "Merge the clauses into one attribute.", + ), + ( + "expected an expression", + "A clause whose value is not an expression.", + "Supply a `bool` expression, or a list of them.", + ), + ( + "expected an assignment", + "A `captures` entry that is not `pattern = expression`.", + "Write `captures: name = expr`.", + ), + ( + "expected an assignment or block", + "A `captures` value that is neither an assignment nor a block.", + "Write `captures: name = expr`, or a list of assignments.", + ), + ( + "expected a single expression", + "`decreases` given a list.", + "Supply one expression.", + ), + ( + "not allowed here due to `#[spec]`", + "A trait function parameter pattern the macro cannot forward.", + "Name the parameter; avoid `_`, `..`, `ref`, and macro patterns.", + ), + ( + "or-pattern not allowed here due to `#[spec]`", + "An or-pattern in a trait function parameter.", + "Name the parameter and match inside the body.", + ), + ( + "The enclosing trait must have a `#[spec]` annotation.", + "Clauses on a trait function whose trait carries no `#[spec]`.", + "Add a bare `#[spec]` to the trait.", + ), + ( + "Unsupported spec element on trait.", + "Clauses on the `#[spec]` attached to a trait.", + "Keep the trait's attribute bare; put clauses on its functions.", + ), + ( + "Unsupported spec element on trait impl.", + "Clauses on the `#[spec]` attached to an `impl Trait for T`.", + "Keep it bare; put clauses on the functions.", + ), + ( + "Unsupported spec element on inherent impl.", + "Clauses on the `#[spec]` attached to an inherent `impl`.", + "Keep it bare; put clauses on the methods.", + ), + ( + "cannot be weaker than the qualifiers on the trait", + "An impl claiming fewer guarantees than the trait promised.", + "An impl may only narrow; restore the trait's qualifiers.", + ), + ( + "The #[spec] attribute doesn't yet support this item", + "`#[spec]` on an item kind with no support, such as `mod` or `type`.", + "Move it to a supported item.", + ), + ( + "`try_call` needs the `anodized_try` build `cfg` to be enabled", + "`try_call!` without the build configuration that generates its entry points.", + "Build with `--cfg anodized_try` and `--cfg anodized_panic`.", + ), + ( + "precondition failed", + "At runtime: the caller broke the contract.", + "Fix the call site, or the precondition if it was wrong.", + ), + ( + "postcondition failed", + "At runtime: the implementation broke its own contract.", + "Fix the body, or the postcondition if it was wrong.", + ), +]; + +/// Renders the table named by `id`. +pub fn render(id: &str) -> Result { + match id { + "clauses" => Ok(render_clauses()), + "qualifiers" => Ok(render_qualifiers()), + "item-kinds" => Ok(render_item_kinds()), + "cfg-flags" => Ok(render_cfg_flags()), + "diagnostics" => Ok(render_diagnostics()), + "ebnf" => render_ebnf(), + other => Err(format!("no renderer for generated region `{other}`").into()), + } +} + +fn render_clauses() -> String { + let mut out = String::from("| Clause | Takes | Allowed on |\n| --- | --- | --- |\n"); + for keyword in all_keywords() { + if let KeywordDoc::Current { name, takes, items } = documented_keyword(&keyword) { + let _ = writeln!(out, "| `{name}` | {takes} | {items} |"); + } + } + out +} + +fn render_qualifiers() -> String { + let composites = [ + ("functional", FnQualifiers::FUNCTIONAL), + ("pure", FnQualifiers::PURE), + ("total", FnQualifiers::TOTAL), + ]; + let primitives = [ + ( + "deterministic", + FnQualifiers::DETERMINISTIC, + "the return value depends only on the arguments", + ), + ("effectfree", FnQualifiers::EFFECTFREE, "no side effects"), + ( + "infallible", + FnQualifiers::INFALLIBLE, + "does not panic or abort", + ), + ( + "terminating", + FnQualifiers::TERMINATING, + "does not run forever", + ), + ]; + + let mut out = String::from("| Qualifier | Guarantees |\n| --- | --- |\n"); + for (name, bits) in composites { + let parts: Vec<_> = primitives + .iter() + .filter(|(_, bit, _)| bits.contains(*bit)) + .map(|(part, _, _)| format!("`{part}`")) + .collect(); + let _ = writeln!(out, "| `{name}` | {} |", parts.join(", ")); + } + for (name, _, meaning) in primitives { + let _ = writeln!(out, "| `{name}` | {meaning} |"); + } + out +} + +fn render_item_kinds() -> String { + let mut out = String::from("| Item | Clauses | How |\n| --- | --- | --- |\n"); + for (item, clauses, how) in ITEM_KINDS { + let _ = writeln!(out, "| {item} | {clauses} | {how} |"); + } + out +} + +fn render_cfg_flags() -> String { + let mut out = String::from("| Build configuration | Effect |\n| --- | --- |\n"); + let _ = writeln!( + out, + "| *(none)* | Specs embedded and type-checked; no check runs. `captures` still \ + evaluate. |" + ); + for (flag, effect) in CFG_EFFECTS { + let _ = writeln!(out, "| `--cfg {flag}` | {effect} |"); + } + out +} + +fn render_diagnostics() -> String { + let mut out = String::from("| Message | Cause | Fix |\n| --- | --- | --- |\n"); + for (message, cause, fix) in DIAGNOSTIC_DOCS { + let _ = writeln!(out, "| ``{message}`` | {cause} | {fix} |"); + } + out +} + +fn render_ebnf() -> Result { + let path = repo_root()?.join("crates/anodized-core/README.md"); + let grammar = + crate::fences::extract_one("crates/anodized-core/README.md", &read(&path)?, "ebnf")?; + Ok(format!("```ebnf\n{grammar}```\n")) +} + +fn open_marker(id: &str) -> String { + format!("") +} + +fn close_marker(id: &str) -> String { + format!("") +} + +/// Replaces a region's contents, leaving everything outside the markers untouched. +/// +/// A missing or duplicated marker is an error rather than a skip: a region deleted by a bad +/// merge would otherwise look exactly like a region that is up to date. +pub fn splice(text: &str, id: &str, body: &str) -> Result { + let (open, close) = (open_marker(id), close_marker(id)); + let opens = text.matches(&open).count(); + let closes = text.matches(&close).count(); + if opens != 1 || closes != 1 { + return Err(format!( + "expected exactly one `{id}` region, found {opens} opening and {closes} closing markers" + ) + .into()); + } + let start = text.find(&open).ok_or("marker vanished")? + open.len(); + let end = text.find(&close).ok_or("marker vanished")?; + if end < start { + return Err(format!("the `{id}` region's markers are in the wrong order").into()); + } + Ok(format!("{}\n{}{}", &text[..start], body, &text[end..])) +} + +/// The files that hold generated regions. +#[must_use] +pub fn region_files() -> BTreeSet<&'static str> { + REGIONS.iter().map(|(file, _)| *file).collect() +} + +/// Renders every region and returns the resulting file contents, without writing. +pub fn rendered_files() -> Result> { + let mut results = Vec::new(); + for file in region_files() { + let current = read_skill_file(file)?; + let mut updated = current.clone(); + for (region_file, id) in REGIONS { + if *region_file == file { + updated = splice(&updated, id, &render(id)?)?; + } + } + results.push((file.to_owned(), current, updated)); + } + Ok(results) +} + +/// Rewrites every generated region in place, returning the files that changed. +pub fn write() -> Result> { + let mut changed = Vec::new(); + for (file, current, updated) in rendered_files()? { + if current != updated { + std::fs::write(skill_dir()?.join(&file), &updated)?; + changed.push(file); + } + } + Ok(changed) +} + +/// Returns the stale regions, as `file` and marker id. +pub fn check() -> Result> { + let mut stale = Vec::new(); + for (file, current, _) in rendered_files()? { + for (region_file, id) in REGIONS { + if *region_file != file { + continue; + } + if splice(¤t, id, &render(id)?)? != current { + stale.push(format!("{file}:{id}")); + } + } + } + Ok(stale) +} + +/// The diagnostics documented in the generated table. +#[must_use] +pub fn documented_diagnostics() -> BTreeSet<&'static str> { + DIAGNOSTIC_DOCS + .iter() + .map(|(message, _, _)| *message) + .collect() +} + +/// The diagnostics the tests assert against the sources. +#[must_use] +pub fn tracked_diagnostics() -> BTreeSet<&'static str> { + DIAGNOSTICS.iter().copied().collect() +} + +/// The build configurations documented in the generated table. +#[must_use] +pub fn documented_cfg_flags() -> BTreeSet<&'static str> { + CFG_EFFECTS.iter().map(|(flag, _)| *flag).collect() +} + +/// The build configurations the tests assert against the manifests. +#[must_use] +pub fn tracked_cfg_flags() -> BTreeSet<&'static str> { + CFG_FLAGS.iter().copied().collect() +} diff --git a/crates/skill-tools/src/lib.rs b/crates/skill-tools/src/lib.rs new file mode 100644 index 00000000..21c800e0 --- /dev/null +++ b/crates/skill-tools/src/lib.rs @@ -0,0 +1,283 @@ +//! Generates and validates the Anodized agent skill shipped under `plugins/anodized`. +//! +//! The skill is a distributed artifact whose factual tables are derived from this workspace. +//! This crate renders those tables ([`generate`]) and asserts, from the integration tests, +//! that nothing in the skill has drifted away from the code it documents. + +use std::error::Error; +use std::fs; +use std::path::{Path, PathBuf}; + +use anodized_core::annotate::syntax::Keyword; + +pub mod fences; +pub mod generate; +pub mod scratch; + +/// The result type used throughout, so callers propagate with `?` instead of panicking. +pub type Result = std::result::Result>; + +/// The workspace version, inherited via `version.workspace = true`. +/// +/// This is what couples the plugin manifests to the crates they document: the manifests carry +/// a version, and a test asserts it equals this one. +pub const VERSION: &str = env!("CARGO_PKG_VERSION"); + +/// Plugin manifests, relative to the repository root. +pub const MANIFESTS: &[&str] = &[ + ".claude-plugin/marketplace.json", + ".agents/plugins/marketplace.json", + "plugins/anodized/.claude-plugin/plugin.json", + "plugins/anodized/.codex-plugin/plugin.json", +]; + +/// The manifests carrying a `version` field, which must agree with [`VERSION`]. +pub const VERSIONED_MANIFESTS: &[&str] = &[ + ".claude-plugin/marketplace.json", + "plugins/anodized/.claude-plugin/plugin.json", + "plugins/anodized/.codex-plugin/plugin.json", +]; + +/// Slash commands, relative to the plugin root. +pub const COMMANDS: &[&str] = &["check.md", "spec.md"]; + +/// Every file the skill directory is allowed to contain. +pub const SKILL_FILES: &[&str] = &[ + "SKILL.md", + "reference.md", + "examples.md", + "diagnostics.md", + "migration.md", +]; + +/// Documents outside the skill whose Rust blocks are compiled by the same harness. +/// +/// `REFERENCE.md` is not doctested, and it drifted: before this was added it taught an +/// `ensures` form that stopped compiling in 0.6. +pub const VERIFIED_DOCS: &[&str] = &["crates/anodized/REFERENCE.md"]; + +/// The marker placed directly after the frontmatter, identifying the skill as ours. +pub const SENTINEL: &str = ""; + +/// The upper bound on `description` + `when_to_use`, past which the listing is truncated. +pub const FRONTMATTER_BUDGET: usize = 1536; + +/// Build configuration flags, which must match the `check-cfg` declarations. +pub const CFG_FLAGS: &[&str] = &[ + "anodized_discard_specs", + "anodized_panic", + "anodized_print", + "anodized_try", +]; + +/// Crate sources searched for the diagnostics in [`DIAGNOSTICS`]. +pub const DIAGNOSTIC_SOURCES: &[&str] = &["crates/anodized-core/src", "crates/anodized-macros/src"]; + +/// Diagnostics the macro emits verbatim, which `diagnostics.md` must document. +/// +/// Each is asserted to still exist in the sources listed by [`DIAGNOSTIC_SOURCES`], so that +/// rewording a message in the macro fails this crate's tests rather than silently turning the +/// documentation into a lie. +pub const DIAGNOSTICS: &[&str] = &[ + "unknown spec field", + "fields are out of order: the expected order is", + "at most one `captures` field is allowed", + "no longer supported, use the following form instead", + "postcondition closure must have exactly one input", + "qualifier does not take a value", + "this qualifier is redundant; remove it", + "attributes are not supported here", + "unsupported attribute; only `cfg` is allowed", + "multiple `cfg` attributes are not supported", + "`cfg` attribute is not supported here", + "multiple `decreases` fields are not allowed", + "multiple `#[spec]` attributes on a single item are not supported", + "expected an expression", + "expected an assignment", + "expected an assignment or block", + "expected a single expression", + "not allowed here due to `#[spec]`", + "or-pattern not allowed here due to `#[spec]`", + "The enclosing trait must have a `#[spec]` annotation.", + "Unsupported spec element on trait.", + "Unsupported spec element on trait impl.", + "Unsupported spec element on inherent impl.", + "cannot be weaker than the qualifiers on the trait", + "The #[spec] attribute doesn't yet support this item", + "`try_call` needs the `anodized_try` build `cfg` to be enabled", + "precondition failed", + "postcondition failed", +]; + +/// Rustc errors reached indirectly through a spec, which `diagnostics.md` must document. +pub const RUSTC_ERRORS: &[&str] = &[ + "E0015", "E0046", "E0308", "E0425", "E0507", "E0562", "E0596", +]; + +/// How a [`Keyword`] is presented to the reader of the skill. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum KeywordDoc { + /// A bare qualifier in the current syntax. + Qualifier { + /// The qualifier as written in a spec. + name: &'static str, + }, + /// A value clause in the current syntax, documented in `SKILL.md`. + Current { + /// The clause name as written in a spec. + name: &'static str, + /// What the clause takes. + takes: &'static str, + /// Where the clause may appear. + items: &'static str, + }, + /// A clause removed from the syntax, documented only as an error to recognize. + Removed { + /// The clause name as it used to be written. + name: &'static str, + /// What replaced it. + replacement: &'static str, + }, + /// Not a clause at all: the parser's catch-all for an unrecognized field. + NotAClause, +} + +/// Classifies a keyword for documentation. +/// +/// The `match` is exhaustive with no wildcard arm on purpose. Adding a variant to [`Keyword`] +/// breaks the build here, before any test runs, so a new clause cannot reach a release +/// undocumented. +#[must_use] +pub fn documented_keyword(keyword: &Keyword) -> KeywordDoc { + match keyword { + Keyword::Unknown(_) => KeywordDoc::NotAClause, + Keyword::Functional => qualifier("functional"), + Keyword::Pure => qualifier("pure"), + Keyword::Total => qualifier("total"), + Keyword::Deterministic => qualifier("deterministic"), + Keyword::Effectfree => qualifier("effectfree"), + Keyword::Infallible => qualifier("infallible"), + Keyword::Terminating => qualifier("terminating"), + Keyword::Requires => KeywordDoc::Current { + name: "requires", + takes: "one condition, or a list", + items: "`fn`", + }, + Keyword::Maintains => KeywordDoc::Current { + name: "maintains", + takes: "one condition, or a list", + items: "`fn`, loop, `struct`, `enum`", + }, + Keyword::Captures => KeywordDoc::Current { + name: "captures", + takes: "`pattern = expression`, or a list; at most one field", + items: "`fn`", + }, + Keyword::Binds => KeywordDoc::Removed { + name: "binds", + replacement: "`ensures: |PAT| [EXPR, ...]`", + }, + Keyword::Inspects => KeywordDoc::Removed { + name: "inspects", + replacement: "`ensures: |PAT| [EXPR, ...]`", + }, + Keyword::Ensures => KeywordDoc::Current { + name: "ensures", + takes: "a condition, `\\|pattern\\| condition`, or a list of either", + items: "`fn`", + }, + Keyword::Decreases => KeywordDoc::Current { + name: "decreases", + takes: "one expression; at most one field", + items: "loop only", + }, + } +} + +fn qualifier(name: &'static str) -> KeywordDoc { + KeywordDoc::Qualifier { name } +} + +/// Every keyword the parser recognizes, in declaration order. +/// +/// Declaration order is the parser's mandatory clause order, enforced by `Ord`. +#[must_use] +pub fn all_keywords() -> Vec { + vec![ + Keyword::Functional, + Keyword::Pure, + Keyword::Total, + Keyword::Deterministic, + Keyword::Effectfree, + Keyword::Infallible, + Keyword::Terminating, + Keyword::Requires, + Keyword::Maintains, + Keyword::Captures, + Keyword::Binds, + Keyword::Inspects, + Keyword::Ensures, + Keyword::Decreases, + ] +} + +/// The repository root, derived from this crate's location. +pub fn repo_root() -> Result { + Path::new(env!("CARGO_MANIFEST_DIR")) + .ancestors() + .nth(2) + .map(Path::to_path_buf) + .ok_or_else(|| "cannot locate the repository root above CARGO_MANIFEST_DIR".into()) +} + +/// The directory holding the skill. +pub fn skill_dir() -> Result { + Ok(repo_root()?.join("plugins/anodized/skills/anodized")) +} + +/// The plugin root. +pub fn plugin_dir() -> Result { + Ok(repo_root()?.join("plugins/anodized")) +} + +/// Reads a file, reporting the path when it cannot be read. +pub fn read(path: &Path) -> Result { + fs::read_to_string(path).map_err(|err| format!("cannot read {}: {err}", path.display()).into()) +} + +/// Reads and parses a JSON file. +pub fn read_json(path: &Path) -> Result { + let text = read(path)?; + serde_json::from_str(&text) + .map_err(|err| format!("cannot parse {} as JSON: {err}", path.display()).into()) +} + +/// Reads one of the skill's markdown files. +pub fn read_skill_file(name: &str) -> Result { + read(&skill_dir()?.join(name)) +} + +/// Concatenates every source file under the given repository-relative directories. +pub fn read_sources(dirs: &[&str]) -> Result { + let root = repo_root()?; + let mut combined = String::new(); + for dir in dirs { + collect_rust_sources(&root.join(dir), &mut combined)?; + } + Ok(combined) +} + +fn collect_rust_sources(dir: &Path, out: &mut String) -> Result<()> { + let entries = + fs::read_dir(dir).map_err(|err| format!("cannot read {}: {err}", dir.display()))?; + for entry in entries { + let path = entry?.path(); + if path.is_dir() { + collect_rust_sources(&path, out)?; + } else if path.extension().is_some_and(|ext| ext == "rs") { + out.push_str(&read(&path)?); + out.push('\n'); + } + } + Ok(()) +} diff --git a/crates/skill-tools/src/scratch.rs b/crates/skill-tools/src/scratch.rs new file mode 100644 index 00000000..bc0be56e --- /dev/null +++ b/crates/skill-tools/src/scratch.rs @@ -0,0 +1,122 @@ +//! A cargo project outside the workspace, used to compile snippets. + +use std::path::{Path, PathBuf}; +use std::process::Command; + +use crate::{Result, repo_root}; + +/// The outcome of one build. +#[derive(Debug)] +pub struct Outcome { + pub succeeded: bool, + pub stderr: String, +} + +/// A library crate that snippets are written into, one at a time. +/// +/// It is a library, not a binary: the snippets are item-level and carry no `main`, so a binary +/// crate would fail with `E0601` before the spec was ever exercised. The manifest declares an +/// empty `[workspace]`, or the parent workspace claims it — `CARGO_TARGET_TMPDIR` lives under +/// the workspace target directory. +pub struct Project { + dir: PathBuf, + rustflags: Option, +} + +impl Project { + /// Creates a scratch project with the default (unset) build configuration. + /// + /// `base` is the directory to build under; tests pass `CARGO_TARGET_TMPDIR`, which only + /// exists for test targets. + pub fn new(base: &Path, name: &str) -> Result { + Self::with_rustflags(base, name, None) + } + + /// Creates a scratch project built with the given `RUSTFLAGS`. + /// + /// Configurations get separate directories so flipping between them does not invalidate + /// the other's build cache on every run. + pub fn with_rustflags(base: &Path, name: &str, rustflags: Option<&str>) -> Result { + let dir = base.join(name); + std::fs::create_dir_all(dir.join("src"))?; + // Both targets are declared, so both files must exist even when only one is in use. + std::fs::write(dir.join("src/lib.rs"), "")?; + std::fs::write(dir.join("src/main.rs"), "fn main() {}\n")?; + + let anodized = repo_root()?.join("crates/anodized"); + std::fs::write( + dir.join("Cargo.toml"), + format!( + "[workspace]\nmembers = []\n\n\ + [package]\nname = \"skill-scratch\"\nversion = \"0.0.0\"\nedition = \"2024\"\n\ + publish = false\n\n\ + [lib]\npath = \"src/lib.rs\"\n\n\ + [[bin]]\nname = \"skill-scratch\"\npath = \"src/main.rs\"\n\n\ + [dependencies]\nanodized = {{ path = {:?} }}\n", + anodized + ), + )?; + + Ok(Self { + dir, + rustflags: rustflags.map(str::to_owned), + }) + } + + /// Compiles one snippet, returning whether it built and what rustc said. + pub fn build(&self, source: &str) -> Result { + std::fs::write(self.dir.join("src/lib.rs"), source)?; + std::fs::write(self.dir.join("src/main.rs"), "fn main() {}\n")?; + let output = self.cargo("build").arg("--lib").output()?; + Ok(Outcome { + succeeded: output.status.success(), + stderr: String::from_utf8_lossy(&output.stderr).into_owned(), + }) + } + + /// Builds and runs one snippet as a binary, returning whether it exited cleanly. + /// + /// Used for examples that exercise themselves, so a condition that is merely well-formed + /// but false of the code fails here instead of in a reader's crate. + pub fn run(&self, source: &str) -> Result { + std::fs::write(self.dir.join("src/lib.rs"), "")?; + std::fs::write(self.dir.join("src/main.rs"), source)?; + let output = self + .cargo("run") + .arg("--bin") + .arg("skill-scratch") + .output()?; + let mut stderr = String::from_utf8_lossy(&output.stderr).into_owned(); + stderr.push_str(&String::from_utf8_lossy(&output.stdout)); + Ok(Outcome { + succeeded: output.status.success(), + stderr, + }) + } + + /// Runs the project's tests, returning whether they passed and what was reported. + pub fn test(&self, source: &str) -> Result { + std::fs::write(self.dir.join("src/lib.rs"), source)?; + let output = self.cargo("test").output()?; + let mut stderr = String::from_utf8_lossy(&output.stderr).into_owned(); + stderr.push_str(&String::from_utf8_lossy(&output.stdout)); + Ok(Outcome { + succeeded: output.status.success(), + stderr, + }) + } + + fn cargo(&self, subcommand: &str) -> Command { + let mut command = Command::new(env!("CARGO")); + command.arg(subcommand).current_dir(&self.dir); + // Warnings are errors: a snippet that warns in this project would warn in the + // reader's crate too, and plenty of readers build with `-D warnings`. + let mut flags = String::from("-D warnings"); + if let Some(extra) = &self.rustflags { + flags.push(' '); + flags.push_str(extra); + } + command.env("RUSTFLAGS", flags); + command + } +} diff --git a/crates/skill-tools/tests/coverage.rs b/crates/skill-tools/tests/coverage.rs new file mode 100644 index 00000000..b0f06161 --- /dev/null +++ b/crates/skill-tools/tests/coverage.rs @@ -0,0 +1,193 @@ +//! Asserts the skill still documents what the crates actually do. + +use skill_tools::{ + CFG_FLAGS, DIAGNOSTIC_SOURCES, DIAGNOSTICS, KeywordDoc, RUSTC_ERRORS, Result, all_keywords, + documented_keyword, generate, read, read_skill_file, read_sources, repo_root, +}; + +#[test] +fn the_curated_order_matches_the_parser() -> Result<()> { + // `Keyword` derives `Ord` over its declaration order, and the parser rejects fields that + // are out of that order. The curated list drives the generated table, so if the two ever + // disagree the table teaches an order the compiler refuses. + let curated = all_keywords(); + let mut sorted = curated.clone(); + sorted.sort(); + assert_eq!(curated, sorted, "all_keywords() is out of parser order"); + + let mut seen = std::collections::BTreeSet::new(); + for keyword in &curated { + assert!( + seen.insert(format!("{keyword:?}")), + "duplicate: {keyword:?}" + ); + } + Ok(()) +} + +#[test] +fn every_current_keyword_is_documented() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + for keyword in all_keywords() { + if let KeywordDoc::Current { name, .. } = documented_keyword(&keyword) { + assert!( + skill.contains(&format!("`{name}`")), + "SKILL.md does not document `{name}`" + ); + } + } + Ok(()) +} + +#[test] +fn every_removed_keyword_is_documented_as_removed() -> Result<()> { + let diagnostics = read_skill_file("diagnostics.md")?; + let migration = read_skill_file("migration.md")?; + let reference = read_skill_file("reference.md")?; + for keyword in all_keywords() { + if let KeywordDoc::Removed { name, .. } = documented_keyword(&keyword) { + assert!( + migration.contains(name) && reference.contains(name), + "`{name}` is removed but migration.md and reference.md do not both say so" + ); + } + } + assert!(diagnostics.contains("no longer supported")); + Ok(()) +} + +#[test] +fn every_qualifier_is_documented() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + for keyword in all_keywords() { + if let KeywordDoc::Qualifier { name } = documented_keyword(&keyword) { + assert!( + skill.contains(&format!("`{name}`")), + "SKILL.md does not document the `{name}` qualifier" + ); + } + } + Ok(()) +} + +#[test] +fn every_cfg_flag_is_documented() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + for flag in CFG_FLAGS { + assert!(skill.contains(flag), "SKILL.md does not document `{flag}`"); + } + assert_eq!( + generate::documented_cfg_flags(), + generate::tracked_cfg_flags() + ); + Ok(()) +} + +#[test] +fn cfg_flag_list_matches_the_crate_manifests() -> Result<()> { + let root = repo_root()?; + let mut declared = std::collections::BTreeSet::new(); + for manifest in [ + "crates/anodized/Cargo.toml", + "crates/anodized-macros/Cargo.toml", + ] { + let text = read(&root.join(manifest))?; + let mut rest = text.as_str(); + while let Some(start) = rest.find("cfg(anodized_") { + rest = &rest[start + "cfg(".len()..]; + let end = rest.find(')').ok_or("unterminated cfg(")?; + declared.insert(rest[..end].to_owned()); + } + } + let known: std::collections::BTreeSet = + CFG_FLAGS.iter().map(|flag| (*flag).to_owned()).collect(); + assert_eq!(declared, known, "check-cfg and CFG_FLAGS disagree"); + Ok(()) +} + +#[test] +fn every_macro_diagnostic_appears_in_the_docs() -> Result<()> { + let diagnostics = read_skill_file("diagnostics.md")?; + for message in DIAGNOSTICS { + assert!( + diagnostics.contains(message), + "diagnostics.md does not document: {message}" + ); + } + assert_eq!( + generate::documented_diagnostics(), + generate::tracked_diagnostics() + ); + Ok(()) +} + +#[test] +fn every_macro_diagnostic_still_exists_in_the_source() -> Result<()> { + let sources = read_sources(DIAGNOSTIC_SOURCES)?; + for message in DIAGNOSTICS { + assert!( + sources.contains(message), + "no source emits this any more, so the documentation is now a lie: {message}" + ); + } + Ok(()) +} + +#[test] +fn indirect_rustc_errors_are_documented() -> Result<()> { + let diagnostics = read_skill_file("diagnostics.md")?; + for code in RUSTC_ERRORS { + assert!(diagnostics.contains(code), "diagnostics.md omits {code}"); + } + Ok(()) +} + +#[test] +fn ebnf_grammar_matches_anodized_core_readme() -> Result<()> { + let reference = read_skill_file("reference.md")?; + let source = read(&repo_root()?.join("crates/anodized-core/README.md"))?; + let grammar = skill_tools::fences::extract_one("README.md", &source, "ebnf")?; + assert!( + reference.contains(grammar.trim()), + "reference.md's grammar has drifted from anodized-core's" + ); + Ok(()) +} + +#[test] +fn every_item_kind_is_documented() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + for kind in [ + "free `fn`", + "inherent `impl`", + "`trait`", + "`while`", + "`struct`", + "`enum`", + ] { + assert!(skill.contains(kind), "SKILL.md omits {kind}"); + } + Ok(()) +} + +#[test] +fn skill_states_the_absence_of_old_and_implicit_output() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + assert!(skill.contains("There is no `old()`")); + assert!(skill.contains("There is no implicit `output`")); + Ok(()) +} + +#[test] +fn commands_reference_real_cargo_invocations() -> Result<()> { + let commands = repo_root()?.join("plugins/anodized/commands"); + for name in skill_tools::COMMANDS { + let body = read(&commands.join(name))?; + assert!(body.contains("cargo"), "{name} invokes no cargo command"); + } + let check = read(&commands.join("check.md"))?; + for flag in CFG_FLAGS { + assert!(check.contains(flag), "check.md omits the `{flag}` pass"); + } + Ok(()) +} diff --git a/crates/skill-tools/tests/drivers.rs b/crates/skill-tools/tests/drivers.rs new file mode 100644 index 00000000..0d55d665 --- /dev/null +++ b/crates/skill-tools/tests/drivers.rs @@ -0,0 +1,252 @@ +//! Drivers that exercise the skill's examples over their admitted inputs. +//! +//! A `fn main` inside an example proves the spec only on the values that `main` happens to +//! pass, and only for the examples an author remembered to write one for. Every defect found +//! in review so far hid at a boundary a tame driver would miss: a sum bound false only for an +//! all-zero slice, a trait promise false only where the product overflows, an increment false +//! only at `u32::MAX`. These drivers sweep the boundaries instead, and live here rather than in +//! the documents so the shipped examples stay readable. + +/// The documents whose examples must every one be driven or declared undriven. +/// +/// `reference.md`, `diagnostics.md`, and `migration.md` carry no runnable examples; +/// `REFERENCE.md` is excluded because most of its illustrations have `todo!()` bodies, which a +/// driver cannot execute. +pub const DRIVEN_FILES: &[&str] = &["examples.md", "SKILL.md"]; + +/// Prepended to every driven program. +/// +/// `rejects` is what lets a driver test a precondition rather than merely respect it. Sweeping +/// only admitted inputs proves a spec is not violated; it cannot prove the spec is strong +/// enough, because the input that would break the body is exactly the one the driver avoids. +/// Asserting that an out-of-domain call fails *as a precondition* — and not as an overflow or +/// a divide-by-zero from the body — is what catches a precondition that admits too much. +pub const PRELUDE: &str = r#" +fn rejects(call: impl FnOnce() -> T + std::panic::UnwindSafe) { + let previous = std::panic::take_hook(); + std::panic::set_hook(Box::new(|_| {})); + let outcome = std::panic::catch_unwind(call); + std::panic::set_hook(previous); + let payload = outcome.err().expect("the spec accepted an input it should reject"); + let message = payload + .downcast_ref::() + .map(String::as_str) + .or_else(|| payload.downcast_ref::<&str>().copied()) + .unwrap_or_default(); + assert!( + message.contains("precondition failed"), + "expected a precondition to reject this input; the body failed first with: {message}" + ); +} +"#; + +/// A driver for one example. +/// +/// Keyed by file and by a substring the example defines, rather than by its heading: two +/// examples can sit under one heading, and headings get rewritten. +pub struct Driver { + /// The document the example lives in. + pub file: &'static str, + /// A substring that appears in this example and no other in the same file. + pub defines: &'static str, + /// A `fn main` appended to the example's own source. + pub main: &'static str, +} + +/// Examples whose bodies are illustrative rather than real, so nothing can be run. +/// +/// These are verified by reading. Keeping them named here is what stops the set growing +/// silently: a new example must either be driven or be listed as deliberately undriven. +pub const UNDRIVEN: &[(&str, &str)] = &[ + // Data specs: `self` is in scope but there is nothing to call, and neither a `struct` nor + // an `enum` invariant is checked at runtime, so a driver would exercise nothing. + ("examples.md", "struct Bounds"), + ("examples.md", "enum Temperature"), + ("SKILL.md", "struct Range"), +]; + +/// The drivers, one per runnable example. +pub const DRIVERS: &[Driver] = &[ + Driver { + file: "examples.md", + defines: "fn nth", + main: r#"fn main() { + for slice in [&[7u32][..], &[1, 2, 3][..], &[0, 0][..]] { + for index in 0..slice.len() { + assert_eq!(nth(slice, index), slice[index]); + } + rejects(move || nth(slice, slice.len())); + } + }"#, + }, + Driver { + file: "examples.md", + defines: "fn bump", + main: r#"fn main() { + for counter in [0u32, 1, u32::MAX - 1] { + assert_eq!(bump(counter), counter + 1); + } + rejects(|| bump(u32::MAX)); + }"#, + }, + Driver { + file: "examples.md", + defines: "fn overwrite_first", + main: r#"fn main() { + let mut buffer = vec![1u32]; + overwrite_first(&mut buffer, 9); + assert_eq!(buffer[0], 9); + let mut longer = vec![1u32, 2, 3]; + overwrite_first(&mut longer, 0); + let mut empty: Vec = vec![]; + rejects(move || overwrite_first(&mut empty, 9)); + }"#, + }, + Driver { + file: "examples.md", + defines: "fn divide", + main: r#"fn main() { + for dividend in [0u32, 1, 7, u32::MAX] { + for divisor in [1u32, 2, 7, u32::MAX] { + let _ = divide(dividend, divisor); + } + } + rejects(|| divide(1, 0)); + }"#, + }, + Driver { + file: "examples.md", + defines: "fn checked_divide", + main: r#"fn main() { + for divisor in [0u32, 1, u32::MAX] { + let _ = checked_divide(10, divisor); + } + }"#, + }, + Driver { + file: "examples.md", + defines: "fn larger", + main: r#"fn main() { + for left in [0u32, 1, u32::MAX] { + for right in [0u32, 1, u32::MAX] { + let _ = larger(left, right); + } + } + }"#, + }, + Driver { + file: "examples.md", + defines: "fn power_of_two", + main: r#"fn main() { + for exponent in 0..32u32 { + let _ = power_of_two(exponent); + } + rejects(|| power_of_two(32)); + }"#, + }, + Driver { + file: "examples.md", + defines: "struct Counter", + main: r#"fn main() { + let mut counter = Counter::new(); + for _ in 0..3 { + let _ = counter.increment(); + } + let mut maxed = Counter::new(); + maxed.value = u32::MAX; + rejects(move || maxed.increment()); + }"#, + }, + Driver { + file: "examples.md", + defines: "trait Scale", + main: r#"fn main() { + for factor in 1..=8u32 { + for value in [0, 1, u32::MAX / factor] { + assert!(Doubling.scale(value, factor) >= value); + assert!(Exact.scale(value, factor) >= value); + } + } + assert_eq!(Doubling.scale(u32::MAX, 1), u32::MAX); + rejects(|| Doubling.scale(u32::MAX, 2)); + rejects(|| Doubling.scale(5, 0)); + }"#, + }, + Driver { + file: "examples.md", + defines: "fn maximum", + main: r#"fn main() { + assert_eq!(maximum(&[5]), 5); + assert_eq!(maximum(&[1, 9, 3]), 9); + assert_eq!(maximum(&[0, 0]), 0); + rejects(|| maximum(&[])); + }"#, + }, + Driver { + file: "examples.md", + defines: "fn first", + main: r#"fn main() { + assert_eq!(first(&[4]), 4); + assert_eq!(first(&[7, 8]), 7); + rejects(|| first(&[])); + }"#, + }, + Driver { + file: "examples.md", + defines: "fn safe_divide", + main: r#"fn main() { + for divisor in [0u32, 1, 3] { + let _ = safe_divide(9, divisor); + } + }"#, + }, + Driver { + file: "examples.md", + defines: "fn reversed", + main: r#"fn main() { + for items in [vec![], vec![7u32], vec![1, 2, 3], vec![0, 0]] { + let out = reversed(items.clone()); + assert_eq!(out.len(), items.len()); + assert_eq!(out.last().copied(), items.first().copied()); + } + }"#, + }, + Driver { + file: "SKILL.md", + defines: "captures: before = count", + main: r#"fn main() { + for count in [0u32, 1, u32::MAX - 1] { + assert_eq!(increment(count), count + 1); + } + rejects(|| increment(u32::MAX)); + }"#, + }, + Driver { + file: "SKILL.md", + defines: "fn one()", + main: r#"fn main() { + assert_eq!(one(), 1); + }"#, + }, + Driver { + file: "SKILL.md", + defines: "fn sorted", + main: r#"fn main() { + for items in [vec![], vec![5u32], vec![3, 1, 2], vec![0, 0]] { + let sorted_items = sorted(items.clone()); + assert_eq!(sorted_items.len(), items.len()); + assert!(sorted_items.windows(2).all(|w| w[0] <= w[1])); + } + }"#, + }, + Driver { + file: "SKILL.md", + defines: "fn maximum", + main: r#"fn main() { + assert_eq!(maximum(&[5]), 5); + assert_eq!(maximum(&[1, 9, 3]), 9); + assert_eq!(maximum(&[0, 0]), 0); + rejects(|| maximum(&[])); + }"#, + }, +]; diff --git a/crates/skill-tools/tests/examples.rs b/crates/skill-tools/tests/examples.rs new file mode 100644 index 00000000..a713616b --- /dev/null +++ b/crates/skill-tools/tests/examples.rs @@ -0,0 +1,257 @@ +//! Compiles every Rust block in the skill. +//! +//! A wrong example in an agent skill is worse than no example, because it is copied verbatim. +//! `REFERENCE.md` drifted exactly this way, teaching a form that stopped compiling in 0.6. + +mod drivers; + +use std::path::Path; + +use skill_tools::scratch; + +use skill_tools::fences::{Fence, Kind}; +use skill_tools::{Result, SKILL_FILES, VERIFIED_DOCS, read, read_skill_file, repo_root}; + +fn fences() -> Result> { + let mut all = Vec::new(); + for name in SKILL_FILES { + all.extend(skill_tools::fences::extract(name, &read_skill_file(name)?)?); + } + let root = repo_root()?; + for path in VERIFIED_DOCS { + all.extend(skill_tools::fences::extract( + path, + &read(&root.join(path))?, + )?); + } + Ok(all) +} + +#[test] +fn every_fence_uses_a_known_tag() -> Result<()> { + fences()?; + Ok(()) +} + +#[test] +fn every_fragment_is_labelled() -> Result<()> { + for fence in fences()?.iter().filter(|f| f.kind == Kind::Fragment) { + assert!( + fence.is_labelled_fragment(), + "{fence}: an `ignore` block must open with `// fragment`; wrong-form examples \ + belong in a `compile_fail` block instead" + ); + } + Ok(()) +} + +#[test] +fn every_rust_fence_compiles() -> Result<()> { + let project = scratch::Project::new(Path::new(env!("CARGO_TARGET_TMPDIR")), "examples")?; + for fence in &fences()? { + match fence.kind { + Kind::Pass | Kind::CompileOnly => { + let outcome = project.build(&fence.as_program())?; + assert!( + outcome.succeeded, + "{fence}: expected this to compile, but it did not:\n{}", + outcome.stderr + ); + } + Kind::CompileFail => { + let expected = fence.expected_error()?; + let outcome = project.build(&fence.as_program())?; + assert!( + !outcome.succeeded, + "{fence}: expected {expected}, but it compiled" + ); + assert!( + outcome.stderr.contains(&expected), + "{fence}: expected {expected}, got:\n{}", + outcome.stderr + ); + } + Kind::Fragment | Kind::Other => {} + } + } + Ok(()) +} + +/// Every runnable example is either driven or deliberately listed as undriven. +/// +/// Without this, coverage would depend on whether an author remembered to write a driver, and +/// a new example could join the document exercised by nothing at all. +#[test] +fn every_example_is_driven_or_declared_undriven() -> Result<()> { + for fence in fences()?.iter().filter(|f| f.kind == Kind::Pass) { + if !drivers::DRIVEN_FILES.contains(&fence.file.as_str()) || fence.is_self_exercising() { + continue; + } + let driven = drivers::DRIVERS + .iter() + .any(|d| d.file == fence.file && fence.body.contains(d.defines)); + let declared = drivers::UNDRIVEN + .iter() + .any(|(file, defines)| *file == fence.file && fence.body.contains(defines)); + assert!( + driven || declared, + "{fence}: the example under `{}` is never run. Add a driver in \ + tests/drivers.rs, or list it in UNDRIVEN with a reason.", + fence.heading() + ); + } + Ok(()) +} + +/// Every `UNDRIVEN` entry names exactly one example, and never one that is also driven. +/// +/// Without this the list is an unguarded escape hatch: a single loose substring such as +/// `use anodized::spec` would declare every present and future example deliberately undriven, +/// and an entry left behind by a deleted example would linger unnoticed. +#[test] +fn every_undriven_entry_names_exactly_one_example() -> Result<()> { + let all = fences()?; + for (file, defines) in drivers::UNDRIVEN { + let matched: Vec<_> = all + .iter() + .filter(|f| f.kind == Kind::Pass && f.file == *file && f.body.contains(defines)) + .collect(); + assert_eq!( + matched.len(), + 1, + "UNDRIVEN entry `{defines}` in {file} matches {} examples; it must name exactly one", + matched.len() + ); + let also_driven = drivers::DRIVERS + .iter() + .any(|d| d.file == *file && matched[0].body.contains(d.defines)); + assert!( + !also_driven, + "`{defines}` in {file} is both driven and declared undriven; keep one" + ); + } + Ok(()) +} + +/// A driven document may not park an example beyond the reach of the drivers. +/// +/// `Kind::CompileOnly` is compiled exactly like `Kind::Pass`, so retagging a fence +/// `rust, no_run` would quietly drop it from the driven-or-declared requirement. +#[test] +fn driven_files_contain_no_compile_only_examples() -> Result<()> { + for fence in fences()?.iter().filter(|f| f.kind == Kind::CompileOnly) { + assert!( + !drivers::DRIVEN_FILES.contains(&fence.file.as_str()), + "{fence}: `no_run` in a driven document exempts the example from being run; \ + tag it `rust` and give it a driver" + ); + } + Ok(()) +} + +/// Runs every driven example over the inputs its driver sweeps, with checks enabled. +#[test] +fn driven_examples_satisfy_their_own_specs() -> Result<()> { + let project = scratch::Project::with_rustflags( + Path::new(env!("CARGO_TARGET_TMPDIR")), + "examples-driven", + Some("--cfg anodized_print --cfg anodized_panic"), + )?; + let all = fences()?; + for driver in drivers::DRIVERS { + let matched: Vec<_> = all + .iter() + .filter(|f| { + f.kind == Kind::Pass && f.file == driver.file && f.body.contains(driver.defines) + }) + .collect(); + let fence = match matched.as_slice() { + [one] => *one, + [] => { + return Err(format!( + "driver `{}` in {} matches no example; its `defines` is stale", + driver.defines, driver.file + ) + .into()); + } + many => { + return Err(format!( + "driver `{}` in {} matches {} examples; make `defines` unique", + driver.defines, + driver.file, + many.len() + ) + .into()); + } + }; + assert!( + !fence.is_self_exercising(), + "{fence}: `{}` has both a driver and its own `fn main`; keep one", + driver.defines + ); + let program = format!( + "{}\n{}\n{}\n", + fence.as_program(), + drivers::PRELUDE, + driver.main + ); + let outcome = project.run(&program)?; + assert!( + outcome.succeeded, + "{fence}: `{}` trips its own spec:\n{}", + driver.defines, outcome.stderr + ); + } + Ok(()) +} + +/// Runs the examples that exercise themselves, with checks enabled. +/// +/// The compile pass proves a spec is well-formed; it cannot prove the spec is true of the code +/// beside it. An example here once promised `output >= items.len()` from a sum that is zero +/// for an all-zero slice: it compiled, and panicked on the first honest input. Any block that +/// carries a `fn main` is run under `anodized_print` and `anodized_panic`, so a condition that +/// is false of its own example fails the suite. +#[test] +fn self_exercising_examples_satisfy_their_own_specs() -> Result<()> { + let project = scratch::Project::with_rustflags( + Path::new(env!("CARGO_TARGET_TMPDIR")), + "examples-checked", + Some("--cfg anodized_print --cfg anodized_panic"), + )?; + let mut ran = 0; + for fence in fences()?.iter().filter(|f| f.kind == Kind::Pass) { + if !fence.is_self_exercising() { + continue; + } + let outcome = project.run(&fence.as_program())?; + assert!( + outcome.succeeded, + "{fence}: this example trips its own spec when run:\n{}", + outcome.stderr + ); + ran += 1; + } + assert!( + ran > 0, + "no example exercises itself; the runtime check is inert" + ); + Ok(()) +} + +#[test] +fn examples_cover_every_item_kind() -> Result<()> { + let examples = read_skill_file("examples.md")?; + for heading in [ + "## Free function", + "## Inherent `impl`", + "## Trait, with a narrowing impl", + "## `while` loop", + "## `for` loop", + "## `struct` refinement", + "## `enum` refinement", + ] { + assert!(examples.contains(heading), "examples.md omits {heading}"); + } + Ok(()) +} diff --git a/crates/skill-tools/tests/generated.rs b/crates/skill-tools/tests/generated.rs new file mode 100644 index 00000000..da230e90 --- /dev/null +++ b/crates/skill-tools/tests/generated.rs @@ -0,0 +1,48 @@ +//! Asserts the generated tables in the skill are current. + +use skill_tools::{Result, generate}; + +#[test] +fn generated_regions_are_up_to_date() -> Result<()> { + let stale = generate::check()?; + assert!( + stale.is_empty(), + "stale generated regions {stale:?}; run \ + `cargo run -p skill-tools --bin skill-gen -- --write`" + ); + Ok(()) +} + +#[test] +fn writing_is_idempotent() -> Result<()> { + for (file, _, once) in generate::rendered_files()? { + let mut twice = once.clone(); + for (region_file, id) in generate::REGIONS { + if *region_file == file { + twice = generate::splice(&twice, id, &generate::render(id)?)?; + } + } + assert_eq!(once, twice, "{file}: a second write is not a no-op"); + } + Ok(()) +} + +#[test] +fn every_region_is_declared_exactly_once() -> Result<()> { + for (file, id) in generate::REGIONS { + let text = skill_tools::read_skill_file(file)?; + let open = format!(""); + let close = format!(""); + assert_eq!( + text.matches(&open).count(), + 1, + "{file}: `{id}` opening marker" + ); + assert_eq!( + text.matches(&close).count(), + 1, + "{file}: `{id}` closing marker" + ); + } + Ok(()) +} diff --git a/crates/skill-tools/tests/manifests.rs b/crates/skill-tools/tests/manifests.rs new file mode 100644 index 00000000..64079d4d --- /dev/null +++ b/crates/skill-tools/tests/manifests.rs @@ -0,0 +1,232 @@ +//! Asserts the plugin manifests agree with each other and with the workspace. + +use serde_json::Value; +use skill_tools::{ + COMMANDS, FRONTMATTER_BUDGET, MANIFESTS, Result, SENTINEL, SKILL_FILES, VERSION, + VERSIONED_MANIFESTS, plugin_dir, read_json, read_skill_file, repo_root, skill_dir, +}; + +fn manifest(path: &str) -> Result { + read_json(&repo_root()?.join(path)) +} + +fn field<'a>(value: &'a Value, key: &str, path: &str) -> Result<&'a Value> { + value + .get(key) + .ok_or_else(|| format!("{path}: missing `{key}`").into()) +} + +fn text(value: &Value, key: &str, path: &str) -> Result { + field(value, key, path)? + .as_str() + .map(str::to_owned) + .ok_or_else(|| format!("{path}: `{key}` is not a string").into()) +} + +fn claude_plugin() -> Result { + manifest("plugins/anodized/.claude-plugin/plugin.json") +} + +fn codex_plugin() -> Result { + manifest("plugins/anodized/.codex-plugin/plugin.json") +} + +fn claude_entry() -> Result { + let marketplace = manifest(".claude-plugin/marketplace.json")?; + field(&marketplace, "plugins", "marketplace")? + .get(0) + .cloned() + .ok_or_else(|| "marketplace lists no plugins".into()) +} + +#[test] +fn all_manifests_are_valid_json() -> Result<()> { + for path in MANIFESTS { + let value = manifest(path)?; + assert!(value.is_object(), "{path}: not a JSON object"); + } + Ok(()) +} + +#[test] +fn all_manifests_share_the_workspace_version() -> Result<()> { + assert_eq!( + text(&claude_entry()?, "version", "marketplace entry")?, + VERSION + ); + for path in VERSIONED_MANIFESTS.iter().skip(1) { + assert_eq!(text(&manifest(path)?, "version", path)?, VERSION, "{path}"); + } + Ok(()) +} + +#[test] +fn all_manifests_share_a_description_prefix() -> Result<()> { + let reference = text(&claude_plugin()?, "description", "claude plugin")?; + let prefix: String = reference.chars().take(40).collect(); + for description in [ + text(&codex_plugin()?, "description", "codex plugin")?, + text(&claude_entry()?, "description", "marketplace entry")?, + ] { + assert!( + description.starts_with(&prefix), + "descriptions diverge: {description}" + ); + } + Ok(()) +} + +#[test] +fn marketplace_sources_point_at_the_plugin_directory() -> Result<()> { + assert_eq!( + text(&claude_entry()?, "source", "marketplace entry")?, + "./plugins/anodized" + ); + + let codex = manifest(".agents/plugins/marketplace.json")?; + let entry = field(&codex, "plugins", "codex marketplace")? + .get(0) + .cloned() + .ok_or("codex marketplace lists no plugins")?; + let source = field(&entry, "source", "codex entry")?.clone(); + assert_eq!(text(&source, "path", "codex source")?, "./plugins/anodized"); + assert!(plugin_dir()?.is_dir()); + Ok(()) +} + +#[test] +fn claude_plugin_lists_the_skill_directory() -> Result<()> { + let plugin = claude_plugin()?; + let skills = field(&plugin, "skills", "claude plugin")?; + assert_eq!(skills, &serde_json::json!(["./skills/anodized"])); + assert!(skill_dir()?.is_dir()); + Ok(()) +} + +#[test] +fn codex_plugin_lists_the_skills_parent() -> Result<()> { + assert_eq!( + text(&codex_plugin()?, "skills", "codex plugin")?, + "./skills/" + ); + Ok(()) +} + +#[test] +fn claude_plugin_lists_every_command_file() -> Result<()> { + let plugin = claude_plugin()?; + let listed: Vec = field(&plugin, "commands", "claude plugin")? + .as_array() + .ok_or("`commands` is not an array")? + .iter() + .filter_map(|value| value.as_str().map(str::to_owned)) + .collect(); + + for command in COMMANDS { + let entry = format!("./commands/{command}"); + assert!(listed.contains(&entry), "`{entry}` is not listed"); + assert!(plugin_dir()?.join("commands").join(command).is_file()); + } + + let on_disk = std::fs::read_dir(plugin_dir()?.join("commands"))?.count(); + assert_eq!(on_disk, listed.len(), "a command file is not listed"); + Ok(()) +} + +#[test] +fn every_skill_file_exists_and_nothing_else_does() -> Result<()> { + for name in SKILL_FILES { + let contents = read_skill_file(name)?; + assert!(!contents.trim().is_empty(), "{name} is empty"); + } + for entry in std::fs::read_dir(skill_dir()?)? { + let name = entry?.file_name().to_string_lossy().into_owned(); + assert!( + SKILL_FILES.contains(&name.as_str()), + "unlisted file: {name}" + ); + } + Ok(()) +} + +#[test] +fn license_and_repository_match_the_workspace() -> Result<()> { + for value in [claude_plugin()?, codex_plugin()?, claude_entry()?] { + assert_eq!(text(&value, "license", "manifest")?, "MIT OR Apache-2.0"); + assert_eq!( + text(&value, "repository", "manifest")?, + "https://github.com/anodized-rs/anodized" + ); + } + Ok(()) +} + +#[test] +fn skill_frontmatter_is_well_formed() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + assert!(skill.starts_with("---\n"), "SKILL.md has no frontmatter"); + let frontmatter = frontmatter(&skill)?; + assert!(frontmatter.contains("name: anodized")); + for key in ["description:", "when_to_use:", "allowed-tools:"] { + assert!(frontmatter.contains(key), "frontmatter lacks `{key}`"); + } + Ok(()) +} + +#[test] +fn frontmatter_fits_the_listing_budget() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + let frontmatter = frontmatter(&skill)?; + let described = folded(&frontmatter, "description:")? + &folded(&frontmatter, "when_to_use:")?; + assert!( + described.len() <= FRONTMATTER_BUDGET, + "description plus when_to_use is {} characters, over the {FRONTMATTER_BUDGET} the \ + listing keeps; triggers past the cut are silently discarded", + described.len() + ); + Ok(()) +} + +#[test] +fn skill_carries_the_ownership_sentinel() -> Result<()> { + let skill = read_skill_file("SKILL.md")?; + let body = skill + .split_once("\n---\n") + .ok_or("SKILL.md frontmatter is unterminated")? + .1; + assert_eq!(body.trim_start().lines().next(), Some(SENTINEL)); + Ok(()) +} + +#[test] +fn sibling_files_do_not_carry_frontmatter() -> Result<()> { + for name in SKILL_FILES.iter().filter(|name| **name != "SKILL.md") { + let contents = read_skill_file(name)?; + assert!( + !contents.starts_with("---"), + "{name} opens with frontmatter, which reads as a standalone skill" + ); + } + Ok(()) +} + +fn frontmatter(skill: &str) -> Result { + let rest = skill.strip_prefix("---\n").ok_or("no frontmatter")?; + let end = rest.find("\n---\n").ok_or("unterminated frontmatter")?; + Ok(rest[..end].to_owned()) +} + +fn folded(frontmatter: &str, key: &str) -> Result { + let start = frontmatter + .find(key) + .ok_or_else(|| format!("frontmatter lacks `{key}`"))?; + let mut value = String::new(); + for line in frontmatter[start..].lines().skip(1) { + if !line.starts_with(" ") { + break; + } + value.push_str(line.trim()); + value.push(' '); + } + Ok(value) +} diff --git a/crates/skill-tools/tests/runtime.rs b/crates/skill-tools/tests/runtime.rs new file mode 100644 index 00000000..ef2b033e --- /dev/null +++ b/crates/skill-tools/tests/runtime.rs @@ -0,0 +1,104 @@ +//! Asserts the runtime behavior `diagnostics.md` documents actually happens. +//! +//! The fence harness builds with no `anodized_*` configuration, where checks are embedded but +//! inert. Nothing there can catch a claim about what a violation *does*, so these cases build +//! with checks live and run them. + +use std::path::Path; + +use skill_tools::scratch; + +const CHECKS_ON: &str = "--cfg anodized_print --cfg anodized_panic"; + +// Each case gets its own scratch directory. They run in parallel and would otherwise +// overwrite one another's source file mid-build. + +fn case(body: &str) -> String { + format!("use anodized::spec;\n\n{body}\n") +} + +#[test] +fn a_violated_precondition_panics() -> skill_tools::Result<()> { + let project = scratch::Project::with_rustflags( + Path::new(env!("CARGO_TARGET_TMPDIR")), + "runtime-precondition", + Some(CHECKS_ON), + )?; + let outcome = project.test(&case( + r#" +#[spec(requires: divisor != 0)] +pub fn divide(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[cfg(test)] +mod tests { + #[test] + #[should_panic(expected = "precondition failed")] + fn rejects_zero() { + let _ = super::divide(1, 0); + } +} +"#, + ))?; + assert!(outcome.succeeded, "{}", outcome.stderr); + Ok(()) +} + +#[test] +fn a_violated_postcondition_panics() -> skill_tools::Result<()> { + let project = scratch::Project::with_rustflags( + Path::new(env!("CARGO_TARGET_TMPDIR")), + "runtime-postcondition", + Some(CHECKS_ON), + )?; + let outcome = project.test(&case( + r#" +#[spec(ensures: |output| output > 0)] +pub fn zero() -> u32 { + 0 +} + +#[cfg(test)] +mod tests { + #[test] + #[should_panic(expected = "postcondition failed")] + fn breaks_its_promise() { + let _ = super::zero(); + } +} +"#, + ))?; + assert!(outcome.succeeded, "{}", outcome.stderr); + Ok(()) +} + +#[test] +fn a_satisfied_spec_is_silent() -> skill_tools::Result<()> { + let project = scratch::Project::with_rustflags( + Path::new(env!("CARGO_TARGET_TMPDIR")), + "runtime-satisfied", + Some(CHECKS_ON), + )?; + let outcome = project.test(&case( + r#" +#[spec( + requires: divisor != 0, + ensures: |output| output <= dividend, +)] +pub fn divide(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[cfg(test)] +mod tests { + #[test] + fn accepts_valid_input() { + assert_eq!(super::divide(6, 2), 3); + } +} +"#, + ))?; + assert!(outcome.succeeded, "{}", outcome.stderr); + Ok(()) +} From 76723ba373f9b7ba9ac03fa03e0a063d3c638122 Mon Sep 17 00:00:00 2001 From: Slava Barinov Date: Wed, 26 Aug 2026 00:55:36 +0900 Subject: [PATCH 04/10] docs: add a contributor guide - Add `CLAUDE.md`, symlinked as `AGENTS.md` like `README.md` already is. - Describe how to install and use the skill in the README. - Lint and test `skill-tools` in CI. - Record that no test covers the meaning of the prose. --- .github/workflows/ci.yml | 19 ++++++++ .gitignore | 3 ++ AGENTS.md | 1 + CHANGELOG.md | 13 ++++++ CLAUDE.md | 97 +++++++++++++++++++++++++++++++++++++++ crates/anodized/README.md | 33 +++++++++++-- 6 files changed, 162 insertions(+), 4 deletions(-) create mode 120000 AGENTS.md create mode 100644 CLAUDE.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5a0c55c1..23c622ae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -110,6 +110,25 @@ jobs: - name: Integration test anodized-logic run: cargo test -p anodized-logic --tests --no-fail-fast + test-skill-tools: + name: Lint and test skill-tools + runs-on: ubuntu-latest + needs: fmt + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Install Rust toolchain + uses: dtolnay/rust-toolchain@1.95.0 + with: + components: clippy + + - name: Lint skill-tools + run: cargo clippy -p skill-tools --all-targets -- -D warnings + + - name: Validate the agent skill and plugin manifests + run: cargo test -p skill-tools --tests --no-fail-fast + test-test-util: name: Lint test-util runs-on: ubuntu-latest diff --git a/.gitignore b/.gitignore index e1ea2d46..49682d96 100644 --- a/.gitignore +++ b/.gitignore @@ -15,3 +15,6 @@ Cargo.lock # macOS specific files .DS_Store + +# Local agent configuration +.claude/ diff --git a/AGENTS.md b/AGENTS.md new file mode 120000 index 00000000..681311eb --- /dev/null +++ b/AGENTS.md @@ -0,0 +1 @@ +CLAUDE.md \ No newline at end of file diff --git a/CHANGELOG.md b/CHANGELOG.md index 26d8bc3a..9d585894 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## Unreleased +### Added + +- **[anodized] Agent skill and plugin** - The repository now ships an agent skill for Claude + Code and Codex under `plugins/anodized`, installable with + `claude plugin marketplace add anodized-rs/anodized`. Its factual tables are generated from + the crate sources and its examples are compiled, so it cannot drift from the syntax it + documents. + +### Fixed + +- **[anodized] Repaired the examples in `REFERENCE.md`** - Several examples still used the + pre-0.6 postcondition syntax and did not compile; others warned, or asserted a comparison + the type already guaranteed. ### Fixed - **[anodized-core] `#[cfg]` on a condition is honored in every check mode** - The guard was diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 00000000..28dd3769 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,97 @@ +# Working on Anodized + +This file is for agents changing *this repository*. The skill under +`plugins/anodized/skills/anodized/` is a different thing: it teaches people who *use* the +crate how to write specs. Both exist; do not confuse them. + +## Layout + +| Crate | Owns | +| --- | --- | +| `anodized` | The user-facing facade: re-exports `spec`, plus `result` and `try_call!`. | +| `anodized-macros` | The proc macro, and the `cfg` dispatch that decides what it emits. | +| `anodized-core` | Parsing and instrumentation. The real logic, and the tool interop layer. | +| `anodized-logic` | `int`, `implies!`, `opaque!`, `forall`, `exists`. | +| `anodized-fmt` | Formatter library and CLI for `#[spec(...)]`. | +| `test-util` | Internal test helpers. Not published. | +| `skill-tools` | Generates and validates the agent skill. Not published. | + +`README.md` is a symlink to `crates/anodized/README.md`, which is included as the crate's +rustdoc via `#![doc = include_str!]` — so **its examples are doctested**. + +## Build configurations + +There are **no Cargo features**. Behavior is controlled entirely by `--cfg` flags: + +| Flag | Effect | +| --- | --- | +| *(none)* | Specs embedded and type-checked; no checks run. | +| `anodized_discard_specs` | Specs dropped entirely. | +| `anodized_print` | Violations report to stderr and continue. | +| `anodized_panic` | Violations panic. | +| `anodized_try` | Enables `try_call!`. Requires `anodized_panic`. | + +CI passes them as `cargo --config 'build.rustflags=["--cfg","anodized_panic"]' test`. Adding a +new flag means updating `check-cfg` in **both** `crates/anodized/Cargo.toml` and +`crates/anodized-macros/Cargo.toml`; `skill-tools` fails if the documented set drifts. + +## Commands + +```bash +cargo fmt --all -- --check +cargo clippy -p --all-targets -- -D warnings +cargo test -p anodized --tests --no-fail-fast +cargo test -p skill-tools --tests --no-fail-fast +cargo run -p skill-tools --bin skill-gen -- --write +``` + +## Conventions + +Clippy must be clean. **No `#[allow]`** — fix the cause, or delete the code. No `unwrap`, +`expect`, or `panic!` in production paths; propagate with `?`. Files stay under 500 lines. + +Unit tests live in a sibling file, wired up with `#[cfg(test)] #[path = "x_tests.rs"] mod`. +Integration tests are one file per feature under `crates/anodized/tests/`. UI tests use +trybuild with `.stderr` goldens — regenerate with `TRYBUILD=overwrite`. `anodized-fmt` uses +golden fixtures under `tests/fixtures/`. + +## Editing the agent skill + +`plugins/anodized/skills/anodized/` is a shipped artifact. + +- Every ```` ```rust ```` block in it is compiled by `cargo test -p skill-tools`. So is every + block in `crates/anodized/REFERENCE.md`. +- The tables between `` markers are generated. Edit + `crates/skill-tools/src/generate.rs`, then run `skill-gen --write`. Do not hand-edit inside + the markers. +- Change a clause keyword, a qualifier, a `cfg` flag, or a macro error message and the tests + will name the document that needs updating. + +The harness has one blind spot worth knowing: loop and `enum` conditions are dropped before +they reach the compiler, so "every block compiles" proves nothing about the conditions inside +a loop or enum example. Read those by eye. + +**No test covers meaning.** The coverage tests assert that a term *appears*; they cannot tell +whether the sentence around it is still true. Changing spec semantics requires a manual read +of `SKILL.md` and `reference.md`. This is the residual risk and it is not automatable. + +## Which documents are verified + +| Document | Verified? | +| --- | --- | +| `crates/anodized/README.md` | Yes — doctested as crate rustdoc. | +| `crates/anodized/REFERENCE.md` | Examples only, via `skill-tools`. Prose is not. | +| The agent skill | Examples, tables, and runtime claims, via `skill-tools`. Prose is not. | + +When they disagree, the skill and the README win. + +## Releasing + +Bump, in one commit: `[workspace.package] version` and the `[workspace.dependencies]` +`anodized*` lines; the `anodized = "x.y.z"` snippet in `crates/anodized/README.md`; +`version` in `.claude-plugin/marketplace.json`, `plugins/anodized/.claude-plugin/plugin.json`, +and `plugins/anodized/.codex-plugin/plugin.json`; and `CHANGELOG.md`. + +The plugin version is always the workspace version. `skill-tools` reads its own +`CARGO_PKG_VERSION` — which is the workspace version — and fails if a manifest disagrees, so a +mismatched plugin cannot be released. diff --git a/crates/anodized/README.md b/crates/anodized/README.md index d060d29f..65721e0d 100644 --- a/crates/anodized/README.md +++ b/crates/anodized/README.md @@ -80,20 +80,45 @@ fn percentage_10_over_0() { } ``` -Use the `anodized_panic` setting to instrument the code with runtime checks. +Use the `anodized_panic` setting to instrument the code with runtime checks. Add +`anodized_print` to have the failing condition named as well. ```bash -RUSTFLAGS="--cfg anodized_panic" cargo test +RUSTFLAGS="--cfg anodized_print --cfg anodized_panic" cargo test ``` -A spec violation will cause a panic with a descriptive error message: +A spec violation reports the condition, then panics: ```text -thread 'main' panicked at 'Precondition failed: part <= whole', src/main.rs:17:5 +precondition failed: part <= whole +precondition failed: whole > 0.0 +thread 'main' panicked at src/main.rs:3:1: +precondition failed ``` +Conditions are checked independently rather than short-circuiting, so every violated one is +reported before the panic. + For more details and other approaches, see [The Anodized Reference](https://github.com/anodized-rs/anodized/blob/main/crates/anodized/REFERENCE.md). +## Using Anodized with a Coding Agent + +Anodized ships an agent skill, so an assistant writes current `#[spec]` syntax instead of guessing from other contract systems. + +```sh +# Claude Code +claude plugin marketplace add anodized-rs/anodized +claude plugin install anodized@anodized + +# Codex +codex plugin marketplace add anodized-rs/anodized +codex plugin add anodized@anodized +``` + +The skill loads by itself when you mention Anodized or `#[spec]`. It also adds two commands: `/anodized:spec` to add specs to code you point it at, and `/anodized:check` to run your tests under every build configuration. + +Using an agent with no plugin support? Point it at [the skill directory](https://github.com/anodized-rs/anodized/tree/main/plugins/anodized/skills/anodized). + ## Why Anodized Rust has a growing ecosystem of excellent verification tools - Aeneas, Creusot, Flux, Hax, Kani, Prusti, Verus, and more. Each one brings unique strengths. Anodized provides a shared specification layer so that these tools, and the developers who use them, do not have to go it alone. From 5002c7c3119f0deccde9159add551a57ecf9642b Mon Sep 17 00:00:00 2001 From: Slava Barinov Date: Wed, 26 Aug 2026 21:04:50 +0900 Subject: [PATCH 05/10] docs: organize repair guidance around what is wrong MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Name the three things a failure can implicate — call site, spec, body — and say a repair names one of them, rather than leading with which direction to edit a clause. - Say that `anodized_print` continues past a violation, so only the first reported failure is reliable. - Keep the model in `diagnostics.md`, which ships in the skill payload; the Codex manifest carries no commands, so guidance left in `check.md` alone would not reach those users. --- plugins/anodized/commands/check.md | 50 ++++++----------- plugins/anodized/skills/anodized/SKILL.md | 31 ++++------- .../anodized/skills/anodized/diagnostics.md | 55 ++++++++++++++++++- 3 files changed, 79 insertions(+), 57 deletions(-) diff --git a/plugins/anodized/commands/check.md b/plugins/anodized/commands/check.md index 8275aabd..7acc293c 100644 --- a/plugins/anodized/commands/check.md +++ b/plugins/anodized/commands/check.md @@ -31,36 +31,20 @@ What each pass proves: | `print` + `panic` | both, the usual configuration for a test suite | | `print` + `panic` + `try` | additionally enables `try_call!` | -Report the results as a table of pass versus outcome. For any failure: - -- `precondition failed: ` — the **caller** violated the contract. Fix the call site, or - the precondition if it was wrong. -- `postcondition failed: ` — the **implementation** violated its own contract. Fix the - body, or the postcondition if it was wrong. -- A compile error only under `anodized_discard_specs` means real code depends on something a - spec brought into scope. - -Never edit a clause just to make a pass go green. Which edit is legitimate depends on which -kind of check fired. - -A **postcondition** failure means the spec is false of the code. If the clause overclaimed, -weaken the postcondition, or strengthen the precondition so it no longer covers the inputs -where the guarantee does not hold. Either keeps the spec true without re-examining the body. - -A **precondition** failure means a caller broke an obligation; the spec is not thereby false -of the code, so the usual repair is at the call site. Weaken the precondition only when the -body demonstrably handles the input it rejected — that is a new claim about the body, so -verify it rather than assuming it. - -Only the passes with `anodized_print` name the failing expression; `anodized_panic` alone -reports the bare text, so reproduce with both before diagnosing. - -Before applying any of that, check which clause failed, because the message does not say. A -`maintains` clause is checked twice and reports as `precondition failed` on entry and -`postcondition failed` on exit, so a `precondition failed` may name an invariant rather than a -`requires`. Weakening a `maintains` relaxes the exit guarantee as well as the entry condition, -so it is not the safe edit that weakening a true precondition is. - -Note who each edit can hurt: weakening a genuine precondition cannot break an existing caller, -while strengthening a precondition, weakening a postcondition, or weakening an invariant can. -Say what you changed and why. +Report the results as a table of pass versus outcome. A compile error only under +`anodized_discard_specs` means real code depends on something a spec brought into scope. + +Never edit a clause just to make a pass go green. Which of three things is wrong — the call +site, the spec, or the body — decides the repair, and a repair names exactly one of them, +taking the other two as correct. A `precondition failed` points at the call site or a +too-strong `requires`; a `postcondition failed` points at the body or an overclaiming spec. + +Two things the message does not tell you. A `maintains` clause is checked on entry and exit +and reports as `precondition failed` one way and `postcondition failed` the other, so a +`precondition failed` may name an invariant. And only the `anodized_print` passes name the +failing expression, so reproduce with both flags before diagnosing — under `anodized_print` +execution also continues, so trust the first failure and presume the rest is fallout. + +The skill's `diagnostics.md` carries the full model, including which candidate each failure +rarely but genuinely admits, and which edits can break an existing caller. Read it before +changing a clause, and say what you changed and why. diff --git a/plugins/anodized/skills/anodized/SKILL.md b/plugins/anodized/skills/anodized/SKILL.md index e6d06c3d..548393d1 100644 --- a/plugins/anodized/skills/anodized/SKILL.md +++ b/plugins/anodized/skills/anodized/SKILL.md @@ -372,27 +372,16 @@ Check it compiles with `cargo check`, then run the suite with checks live (`RUSTFLAGS="--cfg anodized_panic" cargo test`). Format with `anodized-fmt` if available. Finally re-read: delete any clause that only repeats the type. -If a check fires, fix the side that is wrong — the caller for a precondition, the body for a -postcondition. Edit the spec only when it was genuinely wrong, and mind which direction. - -A postcondition that overclaimed may be weakened, or the precondition strengthened to exclude -the inputs where the guarantee fails; both keep the spec true of the code. A precondition that -was too strong may be weakened, but only once you have checked that the body really handles -the inputs it was rejecting — that is a new claim, not a relaxation. Weakening a precondition -cannot break an existing caller; the other two edits can. - -First check which clause actually failed, because the message does not say. A `maintains` -clause is checked on entry and again on exit, and it reports as `precondition failed` on the -way in and `postcondition failed` on the way out. So a `precondition failed` naming a -`maintains` clause is not a precondition at all, and weakening it is not the safe edit — -it relaxes the exit guarantee too. - -Only `anodized_print` puts the failing expression in the message; under `anodized_panic` alone -you get the bare text and a location pointing at the attribute, which names the function but -not the clause. Reproduce with both flags before deciding what failed. Matching the quoted -expression usually identifies the clause, though it cannot when two clauses are textually -identical, and the message reprints the tokens with normalized spacing. Say what you changed -and why. +When a check fires, never edit a clause just to make it pass. Three things can be wrong — the +call site, the spec, or the body — and a repair names exactly one of them as wrong, taking the +other two as correct. A `precondition failed` usually points at the call site or the `requires` +and a `postcondition failed` at the body or the spec, but neither rules its third candidate out +entirely. Edit the spec only when the spec is what is wrong, and say which you decided it was. + +Read `diagnostics.md` before acting on a failure: it carries the full model, and the message +alone is not enough to act on — it does not name the kind of clause that broke, only +`anodized_print` names the expression at all, and under that flag execution continues, so later +failures may be fallout from the first. ## Reference files diff --git a/plugins/anodized/skills/anodized/diagnostics.md b/plugins/anodized/skills/anodized/diagnostics.md index 92003e09..261873cf 100644 --- a/plugins/anodized/skills/anodized/diagnostics.md +++ b/plugins/anodized/skills/anodized/diagnostics.md @@ -136,9 +136,58 @@ which kind of clause you are looking at — bearing in mind that the expression under `anodized_print`; `anodized_panic` alone reports the bare text with a location pointing at the attribute, which identifies the function but not the clause. -One consequence worth knowing under `anodized_print`, which continues after a violation: an -invariant already false on entry is reported again on exit, so a `postcondition failed` does -not always mean the body misbehaved — the body may never have had a valid starting state. +Match it by reading, not by searching. The message reprints the condition from the parsed +tokens, so spacing is normalized and rarely matches your source — `!data.is_empty()` is +reported as `! data.is_empty()`. And when two clauses are textually identical, the expression +cannot tell them apart at all. + +`anodized_print` continues after a violation, which makes the reports after the first +unreliable. Trust the first and presume the rest is fallout until it is fixed. A violated +`requires` lets the body run on input it was meant to exclude, so whatever fails next is +usually downstream of that rather than an independent defect; and an invariant already false on +entry is simply reported a second time on exit. Either way a `postcondition failed` does not +always mean the body misbehaved — it may never have had a valid starting state. + +## Repairing what failed + +Never edit a clause just to make a check pass. Three things can be wrong — the call site, the +spec, or the body — and a repair names exactly one of them as wrong, taking the other two as +correct. Diagnosing two at once is how a spec stops describing the code and starts restating +it. Edits may still cascade: strengthening a `requires` obliges you to fix the callers that +relied on the looser contract, but each of those takes the corrected spec as ground truth. + +The failure narrows three candidates to two: + +| Failure | Either | Rarely | +| --- | --- | --- | +| `precondition failed` | the call site broke a correct obligation, or `requires` is too strong | the body | +| `postcondition failed` | the body is wrong, or the spec overclaims | the call site | + +The last column is rare rather than impossible. An entry-side `maintains` failure reports as +`precondition failed`, and the state it objects to may have been left there by an earlier call +into the same code; under `anodized_print` a later report may be fallout from any of that. + +Reach for the call site or the body first. Edit the spec only when the spec is the thing that +is wrong, and say which one you decided it was. Weakening a `requires` asserts that the body +handles inputs it used to reject — a new claim about the body, to be verified rather than +assumed. Where a postcondition overclaims, the alternative to weakening it is strengthening +`requires` so the guarantee no longer covers the failing inputs. + +Of every edit named here, weakening a genuine precondition is the only one that cannot break an +existing caller. + +Deciding which of the three is wrong is the hard part, and the message alone rarely settles it. +What usually does is context around the failure: + +- Several call sites break the same clause, and each looked reasonable — suspect the spec. A + contract nobody can satisfy is usually the contract's fault. +- One call site breaks it while others honor it — suspect that call site. +- The clause contradicts what the function's name or documentation promises — suspect the + clause; one of the two was written later and they have drifted apart. +- The spec is older than the last change to the body — suspect the body, and check whether the + change was meant to alter the contract. +- The failure appeared with no change to any of the three — suspect state reached through a + reference, which makes the culprit some earlier call rather than this one. Under `--cfg anodized_print` the message goes to stderr and execution continues. Under `--cfg anodized_panic` it panics. Enabling both — the usual choice for a test suite — gives From 54ea234baf1040d8f501f890d0f217259df5f3cc Mon Sep 17 00:00:00 2001 From: Slava Barinov Date: Fri, 28 Aug 2026 17:43:22 +0900 Subject: [PATCH 06/10] docs: follow the upstream invariant and output-pattern changes - Document `preinvariant failed` and `postinvariant failed` from #197, and that the group panic still reports neither. - Say a move pattern is reconstructed after each postcondition, per #196, so `|ref output|` is a stylistic choice rather than a workaround for a non-`Copy` return. - Add the rules that come with it: no mixing move and `ref`, and a `..` pattern binds the rest only by `ref`. - Replace the `E0507` entry with `E0005`, which is what a refutable output pattern now reports. --- crates/skill-tools/src/generate.rs | 16 ++++++- crates/skill-tools/src/lib.rs | 4 +- plugins/anodized/skills/anodized/SKILL.md | 10 ++++- .../anodized/skills/anodized/diagnostics.md | 42 ++++++++++++------- 4 files changed, 52 insertions(+), 20 deletions(-) diff --git a/crates/skill-tools/src/generate.rs b/crates/skill-tools/src/generate.rs index f8374bd7..d55dcced 100644 --- a/crates/skill-tools/src/generate.rs +++ b/crates/skill-tools/src/generate.rs @@ -213,14 +213,26 @@ pub const DIAGNOSTIC_DOCS: &[(&str, &str, &str)] = &[ ), ( "precondition failed", - "At runtime: the caller broke the contract.", + "At runtime: a `requires` was false on entry. The panic raised without \ + `anodized_print` also uses this for the whole entry group, invariants included.", "Fix the call site, or the precondition if it was wrong.", ), ( "postcondition failed", - "At runtime: the implementation broke its own contract.", + "At runtime: an `ensures` was false on exit. The panic raised without \ + `anodized_print` also uses this for the whole exit group, invariants included.", "Fix the body, or the postcondition if it was wrong.", ), + ( + "preinvariant failed", + "At runtime under `anodized_print`: a `maintains` was already false on entry.", + "The state was wrong before the call; look at whoever produced it.", + ), + ( + "postinvariant failed", + "At runtime under `anodized_print`: a `maintains` was false on exit.", + "The body broke an invariant it was required to preserve.", + ), ]; /// Renders the table named by `id`. diff --git a/crates/skill-tools/src/lib.rs b/crates/skill-tools/src/lib.rs index 21c800e0..9f50092c 100644 --- a/crates/skill-tools/src/lib.rs +++ b/crates/skill-tools/src/lib.rs @@ -107,11 +107,13 @@ pub const DIAGNOSTICS: &[&str] = &[ "`try_call` needs the `anodized_try` build `cfg` to be enabled", "precondition failed", "postcondition failed", + "preinvariant failed", + "postinvariant failed", ]; /// Rustc errors reached indirectly through a spec, which `diagnostics.md` must document. pub const RUSTC_ERRORS: &[&str] = &[ - "E0015", "E0046", "E0308", "E0425", "E0507", "E0562", "E0596", + "E0005", "E0015", "E0046", "E0308", "E0425", "E0562", "E0596", ]; /// How a [`Keyword`] is presented to the reader of the skill. diff --git a/plugins/anodized/skills/anodized/SKILL.md b/plugins/anodized/skills/anodized/SKILL.md index 548393d1..8718f391 100644 --- a/plugins/anodized/skills/anodized/SKILL.md +++ b/plugins/anodized/skills/anodized/SKILL.md @@ -216,8 +216,14 @@ Four forms are accepted: | `ensures: \|pat\| [a, b]` | bound by `pat` for the whole group | | `ensures: [a, \|pat\| b]` | bound only inside that element | -The closure takes the return value by move, so use `|ref output|` for a non-`Copy` type. The -pattern must be irrefutable: `|Ok(v)|` is not allowed, so test with `|ref out| out.is_ok()`. +A pattern may bind or destructure the return value directly, non-`Copy` included: a move +pattern is reconstructed after each postcondition, so the value still reaches the caller. +`|ref output|` is for when the condition reads more naturally as a borrow, not a workaround. + +Three rules the pattern must satisfy. It must be irrefutable — `|Ok(v)|` is rejected, so +inspect a `Result` with `|output| output.is_ok()`. It may not mix move and `ref` bindings. And +a pattern containing `..` may bind the rest only by `ref`, since what it omits cannot be +reconstructed. ## Qualifiers diff --git a/plugins/anodized/skills/anodized/diagnostics.md b/plugins/anodized/skills/anodized/diagnostics.md index 261873cf..ba3284ab 100644 --- a/plugins/anodized/skills/anodized/diagnostics.md +++ b/plugins/anodized/skills/anodized/diagnostics.md @@ -37,8 +37,10 @@ The macro accumulates errors, so several clause problems surface at once. | ``cannot be weaker than the qualifiers on the trait`` | An impl claiming fewer guarantees than the trait promised. | An impl may only narrow; restore the trait's qualifiers. | | ``The #[spec] attribute doesn't yet support this item`` | `#[spec]` on an item kind with no support, such as `mod` or `type`. | Move it to a supported item. | | ```try_call` needs the `anodized_try` build `cfg` to be enabled`` | `try_call!` without the build configuration that generates its entry points. | Build with `--cfg anodized_try` and `--cfg anodized_panic`. | -| ``precondition failed`` | At runtime: the caller broke the contract. | Fix the call site, or the precondition if it was wrong. | -| ``postcondition failed`` | At runtime: the implementation broke its own contract. | Fix the body, or the postcondition if it was wrong. | +| ``precondition failed`` | At runtime: a `requires` was false on entry. The panic raised without `anodized_print` also uses this for the whole entry group, invariants included. | Fix the call site, or the precondition if it was wrong. | +| ``postcondition failed`` | At runtime: an `ensures` was false on exit. The panic raised without `anodized_print` also uses this for the whole exit group, invariants included. | Fix the body, or the postcondition if it was wrong. | +| ``preinvariant failed`` | At runtime under `anodized_print`: a `maintains` was already false on entry. | The state was wrong before the call; look at whoever produced it. | +| ``postinvariant failed`` | At runtime under `anodized_print`: a `maintains` was false on exit. | The body broke an invariant it was required to preserve. | One wording to be aware of: the out-of-order message for function fields still lists @@ -116,8 +118,18 @@ fn first_mut(values: &mut Vec) -> &mut u8 { impl is expected to supply, so the fix is to add `#[spec]` to the impl, never to implement the named item yourself. -**`E0507: cannot move out`** — an `ensures` closure took a non-`Copy` return value by move and -then used it in a way that needs ownership elsewhere. Bind by reference: `|ref output|`. +**`E0005: refutable pattern`** — an output pattern that does not match every value, such as +`|Ok(v)|`. Bind the whole value and inspect it in the condition: `|output| output.is_ok()`. + +```rust,compile_fail +// EXPECT: E0005 +use anodized::spec; + +#[spec(ensures: |Ok(value)| value > 0)] +fn parse() -> Result { + Ok(1) +} +``` ## Runtime failures @@ -129,17 +141,17 @@ unless the precondition was wrong. `postcondition failed: ` means the **implementation** broke its own contract. Fix the body, unless the postcondition was wrong. -Neither message names the clause kind, and a `maintains` clause borrows both: it is checked on -entry, where a violation reports as `precondition failed`, and again on exit, where it reports -as `postcondition failed`. Match the quoted expression against the spec before concluding -which kind of clause you are looking at — bearing in mind that the expression appears only -under `anodized_print`; `anodized_panic` alone reports the bare text with a location pointing -at the attribute, which identifies the function but not the clause. - -Match it by reading, not by searching. The message reprints the condition from the parsed -tokens, so spacing is normalized and rarely matches your source — `!data.is_empty()` is -reported as `! data.is_empty()`. And when two clauses are textually identical, the expression -cannot tell them apart at all. +Under `anodized_print`, `maintains` reports separately at each end: `preinvariant failed` when +it is already false on entry, `postinvariant failed` when the body broke it. The distinction +matters, because an invariant false on entry is not this call's fault. The panic raised without +`anodized_print` makes no such distinction — it covers the whole entry or exit group, so an +invariant reads there as `precondition failed` or `postcondition failed`, and the location +points at the attribute, naming the function but not the clause. + +To tell two clauses of the same kind apart you still have only the expression, and only under +`anodized_print`. Match it by reading rather than searching: the message reprints from the +parsed tokens, so spacing is normalized and rarely matches your source — `!data.is_empty()` is +reported as `! data.is_empty()`. Two textually identical clauses cannot be told apart at all. `anodized_print` continues after a violation, which makes the reports after the first unreliable. Trust the first and presume the rest is fallout until it is fixed. A violated From c4922338dc53d37f82974025c5432aa98a6c26ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1t=C3=A9=20Kov=C3=A1cs?= <481354+mkovaxx@users.noreply.github.com> Date: Tue, 13 Oct 2026 22:10:49 +0900 Subject: [PATCH 07/10] Apply suggestion from @mkovaxx --- crates/skill-tools/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/skill-tools/src/lib.rs b/crates/skill-tools/src/lib.rs index 9f50092c..8661e262 100644 --- a/crates/skill-tools/src/lib.rs +++ b/crates/skill-tools/src/lib.rs @@ -8,7 +8,7 @@ use std::error::Error; use std::fs; use std::path::{Path, PathBuf}; -use anodized_core::annotate::syntax::Keyword; +use anodized_core::syntax::Keyword; pub mod fences; pub mod generate; From d38ea9209e3a67d84bda0171a6624636bfb82e64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1t=C3=A9=20Kov=C3=A1cs?= <481354+mkovaxx@users.noreply.github.com> Date: Thu, 15 Oct 2026 12:09:09 +0900 Subject: [PATCH 08/10] Apply batched suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Máté Kovács <481354+mkovaxx@users.noreply.github.com> --- crates/skill-tools/src/lib.rs | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/crates/skill-tools/src/lib.rs b/crates/skill-tools/src/lib.rs index 8661e262..2f17387e 100644 --- a/crates/skill-tools/src/lib.rs +++ b/crates/skill-tools/src/lib.rs @@ -175,14 +175,6 @@ pub fn documented_keyword(keyword: &Keyword) -> KeywordDoc { takes: "`pattern = expression`, or a list; at most one field", items: "`fn`", }, - Keyword::Binds => KeywordDoc::Removed { - name: "binds", - replacement: "`ensures: |PAT| [EXPR, ...]`", - }, - Keyword::Inspects => KeywordDoc::Removed { - name: "inspects", - replacement: "`ensures: |PAT| [EXPR, ...]`", - }, Keyword::Ensures => KeywordDoc::Current { name: "ensures", takes: "a condition, `\\|pattern\\| condition`, or a list of either", @@ -216,8 +208,6 @@ pub fn all_keywords() -> Vec { Keyword::Requires, Keyword::Maintains, Keyword::Captures, - Keyword::Binds, - Keyword::Inspects, Keyword::Ensures, Keyword::Decreases, ] From 1d347b56bbeb88787268070067a6005b7d2cd989 Mon Sep 17 00:00:00 2001 From: Maurice Scheffmacher Date: Thu, 15 Oct 2026 19:16:47 +0200 Subject: [PATCH 09/10] fix: align agent skill with current spec behavior --- .claude-plugin/marketplace.json | 2 +- CLAUDE.md | 11 +++-- crates/anodized/REFERENCE.md | 2 +- crates/skill-tools/src/generate.rs | 40 ++++++++--------- crates/skill-tools/src/lib.rs | 11 +++-- crates/skill-tools/tests/coverage.rs | 14 +++--- crates/skill-tools/tests/drivers.rs | 42 +++++++++++++---- plugins/anodized/.claude-plugin/plugin.json | 2 +- plugins/anodized/.codex-plugin/plugin.json | 2 +- plugins/anodized/commands/check.md | 16 ++++++- plugins/anodized/skills/anodized/SKILL.md | 24 +++++----- .../anodized/skills/anodized/diagnostics.md | 45 +++++++++---------- plugins/anodized/skills/anodized/migration.md | 2 + plugins/anodized/skills/anodized/reference.md | 4 +- 14 files changed, 127 insertions(+), 90 deletions(-) diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index 0b11d250..2db5504d 100644 --- a/.claude-plugin/marketplace.json +++ b/.claude-plugin/marketplace.json @@ -12,7 +12,7 @@ "name": "anodized", "source": "./plugins/anodized", "description": "Write, review, and debug Anodized `#[spec]` specifications on Rust functions, traits, loops, structs, and enums, and run the runtime-check build configurations.", - "version": "0.6.0", + "version": "0.7.0", "author": { "name": "anodized-rs" }, diff --git a/CLAUDE.md b/CLAUDE.md index 28dd3769..cf57cb30 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -26,7 +26,9 @@ There are **no Cargo features**. Behavior is controlled entirely by `--cfg` flag | Flag | Effect | | --- | --- | | *(none)* | Specs embedded and type-checked; no checks run. | -| `anodized_discard_specs` | Specs dropped entirely. | +| `anodized_discard_specs` | Specs dropped entirely; incompatible with all other flags. | +| `anodized_embed_specs` | Specs emitted as separate items for analysis; incompatible with runtime-check flags. | +| `anodized_charon` | Embedding with Charon contract attributes; requires nightly and Charon tool registration. | | `anodized_print` | Violations report to stderr and continue. | | `anodized_panic` | Violations panic. | | `anodized_try` | Enables `try_call!`. Requires `anodized_panic`. | @@ -67,9 +69,10 @@ golden fixtures under `tests/fixtures/`. - Change a clause keyword, a qualifier, a `cfg` flag, or a macro error message and the tests will name the document that needs updating. -The harness has one blind spot worth knowing: loop and `enum` conditions are dropped before -they reach the compiler, so "every block compiles" proves nothing about the conditions inside -a loop or enum example. Read those by eye. +Loop conditions are dropped before they reach the compiler, so "every block compiles" proves +nothing about their validity. Read them by eye. Both `struct` and `enum` conditions generate +a type-checked `Spec::predicate`; test that predicate or enforce it at a `Spec!(T)` function +boundary to check the invariant at runtime. **No test covers meaning.** The coverage tests assert that a term *appears*; they cannot tell whether the sentence around it is still true. Changing spec semantics requires a manual read diff --git a/crates/anodized/REFERENCE.md b/crates/anodized/REFERENCE.md index c73fd8a6..fc25b1ea 100644 --- a/crates/anodized/REFERENCE.md +++ b/crates/anodized/REFERENCE.md @@ -78,7 +78,7 @@ Use `#[cfg]` attributes on individual conditions to control when checks run (see When runtime checks are enabled, use the standard `#[cfg]` attribute to select build configurations under which a condition is checked. ```rust, no_run -use anodized::{spec, types::Spec}; +use anodized::spec; #[spec( // Runtime checks only during `cargo test`. diff --git a/crates/skill-tools/src/generate.rs b/crates/skill-tools/src/generate.rs index d55dcced..fd5486b3 100644 --- a/crates/skill-tools/src/generate.rs +++ b/crates/skill-tools/src/generate.rs @@ -30,6 +30,17 @@ pub const REGIONS: &[(&str, &str)] = &[ /// Build configurations, paired with what each one does. pub const CFG_EFFECTS: &[(&str, &str)] = &[ + ( + "anodized_embed_specs", + "Embeds specifications as separate items for analysis without changing function bodies. \ + Incompatible with `anodized_panic`, `anodized_print`, and `anodized_try`.", + ), + ( + "anodized_charon", + "Selects specification embedding and adds Charon contract attributes. Requires nightly \ + and `#![feature(register_tool)]` with `#![register_tool(charon)]` in the consuming crate. \ + Incompatible with runtime-check flags.", + ), ( "anodized_discard_specs", "Specs are dropped entirely: not embedded, not type-checked. Fastest builds.", @@ -83,8 +94,8 @@ pub const ITEM_KINDS: &[(&str, &str, &str)] = &[ pub const DIAGNOSTIC_DOCS: &[(&str, &str, &str)] = &[ ( "unknown spec field", - "A clause name the parser does not recognize, often a guess from another crate.", - "Use one of `requires`, `maintains`, `captures`, `ensures`, `decreases`, or a qualifier.", + "An unrecognized clause name, including the removed `binds:` and `inspects:` forms.", + "Use a current clause or qualifier. Replace `binds:` and `inspects:` with `ensures: \\|PAT\\| [EXPR, ...]`.", ), ( "fields are out of order: the expected order is", @@ -96,11 +107,6 @@ pub const DIAGNOSTIC_DOCS: &[(&str, &str, &str)] = &[ "Two `captures:` fields in one spec.", "Merge them: `captures: [first = a, second = b]`.", ), - ( - "no longer supported, use the following form instead", - "`binds:` or `inspects:`, both removed.", - "Write `ensures: |PAT| [EXPR, ...]` instead.", - ), ( "postcondition closure must have exactly one input", "An `ensures` closure taking zero or several inputs.", @@ -142,8 +148,8 @@ pub const DIAGNOSTIC_DOCS: &[(&str, &str, &str)] = &[ "Keep one expression.", ), ( - "multiple `#[spec]` attributes on a single item are not supported", - "Two `#[spec]` attributes stacked on one item.", + "multiple `#[{name}]` attributes are not allowed", + "Repeated attributes on one item; `{name}` is `spec` for specification attributes.", "Merge the clauses into one attribute.", ), ( @@ -182,19 +188,9 @@ pub const DIAGNOSTIC_DOCS: &[(&str, &str, &str)] = &[ "Add a bare `#[spec]` to the trait.", ), ( - "Unsupported spec element on trait.", - "Clauses on the `#[spec]` attached to a trait.", - "Keep the trait's attribute bare; put clauses on its functions.", - ), - ( - "Unsupported spec element on trait impl.", - "Clauses on the `#[spec]` attached to an `impl Trait for T`.", - "Keep it bare; put clauses on the functions.", - ), - ( - "Unsupported spec element on inherent impl.", - "Clauses on the `#[spec]` attached to an inherent `impl`.", - "Keep it bare; put clauses on the methods.", + "this `#[spec]` attribute must have no fields", + "Clauses on the attribute attached to a `trait` or `impl`.", + "Keep the enclosing attribute bare; put clauses on its functions or methods.", ), ( "cannot be weaker than the qualifiers on the trait", diff --git a/crates/skill-tools/src/lib.rs b/crates/skill-tools/src/lib.rs index 2f17387e..5500749c 100644 --- a/crates/skill-tools/src/lib.rs +++ b/crates/skill-tools/src/lib.rs @@ -64,7 +64,9 @@ pub const FRONTMATTER_BUDGET: usize = 1536; /// Build configuration flags, which must match the `check-cfg` declarations. pub const CFG_FLAGS: &[&str] = &[ + "anodized_charon", "anodized_discard_specs", + "anodized_embed_specs", "anodized_panic", "anodized_print", "anodized_try", @@ -73,7 +75,7 @@ pub const CFG_FLAGS: &[&str] = &[ /// Crate sources searched for the diagnostics in [`DIAGNOSTICS`]. pub const DIAGNOSTIC_SOURCES: &[&str] = &["crates/anodized-core/src", "crates/anodized-macros/src"]; -/// Diagnostics the macro emits verbatim, which `diagnostics.md` must document. +/// Diagnostic text and format templates, which `diagnostics.md` must document. /// /// Each is asserted to still exist in the sources listed by [`DIAGNOSTIC_SOURCES`], so that /// rewording a message in the macro fails this crate's tests rather than silently turning the @@ -82,7 +84,6 @@ pub const DIAGNOSTICS: &[&str] = &[ "unknown spec field", "fields are out of order: the expected order is", "at most one `captures` field is allowed", - "no longer supported, use the following form instead", "postcondition closure must have exactly one input", "qualifier does not take a value", "this qualifier is redundant; remove it", @@ -91,7 +92,7 @@ pub const DIAGNOSTICS: &[&str] = &[ "multiple `cfg` attributes are not supported", "`cfg` attribute is not supported here", "multiple `decreases` fields are not allowed", - "multiple `#[spec]` attributes on a single item are not supported", + "multiple `#[{name}]` attributes are not allowed", "expected an expression", "expected an assignment", "expected an assignment or block", @@ -99,9 +100,7 @@ pub const DIAGNOSTICS: &[&str] = &[ "not allowed here due to `#[spec]`", "or-pattern not allowed here due to `#[spec]`", "The enclosing trait must have a `#[spec]` annotation.", - "Unsupported spec element on trait.", - "Unsupported spec element on trait impl.", - "Unsupported spec element on inherent impl.", + "this `#[spec]` attribute must have no fields", "cannot be weaker than the qualifiers on the trait", "The #[spec] attribute doesn't yet support this item", "`try_call` needs the `anodized_try` build `cfg` to be enabled", diff --git a/crates/skill-tools/tests/coverage.rs b/crates/skill-tools/tests/coverage.rs index b0f06161..a5987525 100644 --- a/crates/skill-tools/tests/coverage.rs +++ b/crates/skill-tools/tests/coverage.rs @@ -44,15 +44,13 @@ fn every_removed_keyword_is_documented_as_removed() -> Result<()> { let diagnostics = read_skill_file("diagnostics.md")?; let migration = read_skill_file("migration.md")?; let reference = read_skill_file("reference.md")?; - for keyword in all_keywords() { - if let KeywordDoc::Removed { name, .. } = documented_keyword(&keyword) { - assert!( - migration.contains(name) && reference.contains(name), - "`{name}` is removed but migration.md and reference.md do not both say so" - ); - } + for name in ["binds", "inspects"] { + assert!( + migration.contains(name) && reference.contains(name) && diagnostics.contains(name), + "`{name}` is removed but its migration or diagnostic guidance is missing" + ); } - assert!(diagnostics.contains("no longer supported")); + assert!(diagnostics.contains("unknown spec field")); Ok(()) } diff --git a/crates/skill-tools/tests/drivers.rs b/crates/skill-tools/tests/drivers.rs index 0d55d665..cf534fa0 100644 --- a/crates/skill-tools/tests/drivers.rs +++ b/crates/skill-tools/tests/drivers.rs @@ -9,7 +9,8 @@ /// The documents whose examples must every one be driven or declared undriven. /// -/// `reference.md`, `diagnostics.md`, and `migration.md` carry no runnable examples; +/// `reference.md` and `migration.md` carry no runnable examples; the runnable example in +/// `diagnostics.md` exercises itself. /// `REFERENCE.md` is excluded because most of its illustrations have `todo!()` bodies, which a /// driver cannot execute. pub const DRIVEN_FILES: &[&str] = &["examples.md", "SKILL.md"]; @@ -57,16 +58,41 @@ pub struct Driver { /// /// These are verified by reading. Keeping them named here is what stops the set growing /// silently: a new example must either be driven or be listed as deliberately undriven. -pub const UNDRIVEN: &[(&str, &str)] = &[ - // Data specs: `self` is in scope but there is nothing to call, and neither a `struct` nor - // an `enum` invariant is checked at runtime, so a driver would exercise nothing. - ("examples.md", "struct Bounds"), - ("examples.md", "enum Temperature"), - ("SKILL.md", "struct Range"), -]; +pub const UNDRIVEN: &[(&str, &str)] = &[]; /// The drivers, one per runnable example. pub const DRIVERS: &[Driver] = &[ + Driver { + file: "examples.md", + defines: "struct Bounds", + main: r#"fn main() { + use anodized::types::Spec; + assert!(Bounds { low: 0, high: 0 }.predicate()); + assert!(Bounds { low: 0, high: u32::MAX }.predicate()); + assert!(!Bounds { low: 1, high: 0 }.predicate()); + }"#, + }, + Driver { + file: "examples.md", + defines: "enum Temperature", + main: r#"fn main() { + use anodized::types::Spec; + assert!(Temperature::Celsius(-273).predicate()); + assert!(!Temperature::Celsius(-274).predicate()); + assert!(Temperature::Kelvin(0).predicate()); + assert!(!Temperature::Kelvin(-1).predicate()); + }"#, + }, + Driver { + file: "SKILL.md", + defines: "struct Range", + main: r#"fn main() { + use anodized::types::Spec; + assert!(Range { low: 0, high: 0 }.predicate()); + assert!(Range { low: 0, high: u32::MAX }.predicate()); + assert!(!Range { low: 1, high: 0 }.predicate()); + }"#, + }, Driver { file: "examples.md", defines: "fn nth", diff --git a/plugins/anodized/.claude-plugin/plugin.json b/plugins/anodized/.claude-plugin/plugin.json index 434a73fe..f00e3ed9 100644 --- a/plugins/anodized/.claude-plugin/plugin.json +++ b/plugins/anodized/.claude-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "anodized", - "version": "0.6.0", + "version": "0.7.0", "description": "Write, review, and debug Anodized `#[spec]` specifications on Rust functions, traits, loops, structs, and enums, and run the runtime-check build configurations.", "author": { "name": "anodized-rs" diff --git a/plugins/anodized/.codex-plugin/plugin.json b/plugins/anodized/.codex-plugin/plugin.json index 4205d30a..e75a4bb0 100644 --- a/plugins/anodized/.codex-plugin/plugin.json +++ b/plugins/anodized/.codex-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "anodized", - "version": "0.6.0", + "version": "0.7.0", "description": "Write, review, and debug Anodized `#[spec]` specifications on Rust functions, traits, loops, structs, and enums, and run the runtime-check build configurations.", "author": { "name": "anodized-rs" diff --git a/plugins/anodized/commands/check.md b/plugins/anodized/commands/check.md index 7acc293c..2838d60d 100644 --- a/plugins/anodized/commands/check.md +++ b/plugins/anodized/commands/check.md @@ -6,8 +6,8 @@ allowed-tools: Bash(cargo:*) # Check every Anodized build configuration Anodized behavior is controlled entirely by `--cfg` flags, not Cargo features. A spec that -type-checks under one configuration can still fail under another, so verify all six — the same -set the Anodized CI matrix runs. +type-checks under one configuration can still fail under another, so verify the six runtime configurations below. +The CI matrix also checks specification embedding with Charon on nightly. Run each pass in order, from the current crate's directory: @@ -31,6 +31,18 @@ What each pass proves: | `print` + `panic` | both, the usual configuration for a test suite | | `print` + `panic` + `try` | additionally enables `try_call!` | +For static-analysis integration, also run the CI embedding configuration on nightly. The +consuming crate must register the Charon tool with `#![feature(register_tool)]` and +`#![register_tool(charon)]` when `anodized_charon` is enabled: + +```bash +cargo +nightly --config 'build.rustflags=["--cfg","anodized_embed_specs","--cfg","anodized_charon"]' test --no-fail-fast -- --skip compile_errors +``` + +This checks embedded specifications and Charon attributes. Compile-error goldens are skipped, +as in CI, because they target runtime instrumentation. Do not combine embedding flags with +`anodized_print`, `anodized_panic`, or `anodized_try`. + Report the results as a table of pass versus outcome. A compile error only under `anodized_discard_specs` means real code depends on something a spec brought into scope. diff --git a/plugins/anodized/skills/anodized/SKILL.md b/plugins/anodized/skills/anodized/SKILL.md index 8718f391..4b9871e5 100644 --- a/plugins/anodized/skills/anodized/SKILL.md +++ b/plugins/anodized/skills/anodized/SKILL.md @@ -26,12 +26,11 @@ allowed-tools: Bash(cargo:*), Bash(anodized-fmt:*) # Writing Anodized specifications A spec is ordinary Rust: every condition is a `bool` expression, and there is no separate -specification language to learn. Conditions on functions and on `struct` definitions are -type-checked by the compiler like any other code. Conditions on **loops and `enum` -definitions are not** — as of 0.6 they are parsed and then dropped, so a typo in one compiles -silently. Write those with extra care. What has to -be learned is the shape of the attribute, and the handful of places where that shape differs -from what every other contract system has trained you to expect. +specification language to learn. Conditions on functions, `struct` definitions, and `enum` +definitions are type-checked unless `anodized_discard_specs` is enabled. **Loop conditions +are not**: they are parsed and then dropped, so a typo in one compiles silently. Review loop +conditions by eye. What has to be learned is the shape of the attribute, and the handful of +places where that shape differs from what every other contract system has trained you to expect. ## Four things that are not what you expect @@ -138,9 +137,8 @@ enables loop specs inside the body, so it is not purely decorative. Not every function can carry one, though. The macro evaluates the body inside a closure, so any shape the language will not let cross a closure boundary stops compiling the moment a spec is attached — in every configuration except `anodized_discard_specs`, which drops specs before -they expand. Known cases: a function returning `impl Trait` (`E0562`), a `const fn` (`E0015`), -and a function returning `&mut` borrowed from a parameter (`captured variable cannot escape -`FnMut` closure body`, which carries no error code). Returning a shared `&` is fine. +they expand. Known cases: a function returning `impl Trait` (`E0562`) and a `const fn` +(`E0015`). Returning a shared `&` or a `&mut` borrowed from a parameter is supported. Treat that list as incomplete rather than exhaustive. The rule that generalizes is the closure: if attaching a spec makes a function stop compiling, that shape cannot carry one, and the only @@ -313,8 +311,10 @@ intent and feed analysis backends. Do not rely on them catching anything today. ## Data `struct` and `enum` take `maintains` only, describing what is always true of a value. `self` -is in scope, and enum variants are brought into scope automatically. Neither is checked at -runtime yet. A `struct` condition **is** type-checked; an `enum` condition is not. +is in scope, and enum variants are brought into scope automatically. Both generate a +type-checked `anodized::types::Spec::predicate` unless `anodized_discard_specs` is enabled. +Construction alone does not check the invariant. Call the predicate explicitly, or use +`Spec!(T)` at a spec'd function boundary with runtime checks enabled to enforce it. ```rust use anodized::spec; @@ -332,6 +332,8 @@ struct Range { | Build configuration | Effect | | --- | --- | | *(none)* | Specs embedded and type-checked; no check runs. `captures` still evaluate. | +| `--cfg anodized_embed_specs` | Embeds specifications as separate items for analysis without changing function bodies. Incompatible with `anodized_panic`, `anodized_print`, and `anodized_try`. | +| `--cfg anodized_charon` | Selects specification embedding and adds Charon contract attributes. Requires nightly and `#![feature(register_tool)]` with `#![register_tool(charon)]` in the consuming crate. Incompatible with runtime-check flags. | | `--cfg anodized_discard_specs` | Specs are dropped entirely: not embedded, not type-checked. Fastest builds. | | `--cfg anodized_print` | A violated condition reports to stderr and execution continues. | | `--cfg anodized_panic` | A violated condition panics, without naming the condition. Pair with `anodized_print` to be told which expression failed. | diff --git a/plugins/anodized/skills/anodized/diagnostics.md b/plugins/anodized/skills/anodized/diagnostics.md index ba3284ab..399739e5 100644 --- a/plugins/anodized/skills/anodized/diagnostics.md +++ b/plugins/anodized/skills/anodized/diagnostics.md @@ -11,10 +11,9 @@ The macro accumulates errors, so several clause problems surface at once. | Message | Cause | Fix | | --- | --- | --- | -| ``unknown spec field`` | A clause name the parser does not recognize, often a guess from another crate. | Use one of `requires`, `maintains`, `captures`, `ensures`, `decreases`, or a qualifier. | +| ``unknown spec field`` | An unrecognized clause name, including the removed `binds:` and `inspects:` forms. | Use a current clause or qualifier. Replace `binds:` and `inspects:` with `ensures: \|PAT\| [EXPR, ...]`. | | ``fields are out of order: the expected order is`` | Clauses are present but in the wrong sequence. | Reorder to qualifiers, `requires`, `maintains`, `captures`, `ensures`. | | ``at most one `captures` field is allowed`` | Two `captures:` fields in one spec. | Merge them: `captures: [first = a, second = b]`. | -| ``no longer supported, use the following form instead`` | `binds:` or `inspects:`, both removed. | Write `ensures: |PAT| [EXPR, ...]` instead. | | ``postcondition closure must have exactly one input`` | An `ensures` closure taking zero or several inputs. | Take exactly the return value: `ensures: |output| ...`. | | ``qualifier does not take a value`` | A qualifier written as `pure: true`. | Write it bare: `pure,`. | | ``this qualifier is redundant; remove it`` | A composite qualifier alongside one of its components. | Keep the composite alone; `pure` already implies `deterministic` and `effectfree`. | @@ -23,7 +22,7 @@ The macro accumulates errors, so several clause problems surface at once. | ``multiple `cfg` attributes are not supported`` | Two `#[cfg]` attributes on one clause. | Combine them: `#[cfg(all(test, debug_assertions))]`. | | ```cfg` attribute is not supported here`` | A `#[cfg]` on `captures`. | Gate the postconditions that read the capture instead. | | ``multiple `decreases` fields are not allowed`` | Two loop variants. | Keep one expression. | -| ``multiple `#[spec]` attributes on a single item are not supported`` | Two `#[spec]` attributes stacked on one item. | Merge the clauses into one attribute. | +| ``multiple `#[{name}]` attributes are not allowed`` | Repeated attributes on one item; `{name}` is `spec` for specification attributes. | Merge the clauses into one attribute. | | ``expected an expression`` | A clause whose value is not an expression. | Supply a `bool` expression, or a list of them. | | ``expected an assignment`` | A `captures` entry that is not `pattern = expression`. | Write `captures: name = expr`. | | ``expected an assignment or block`` | A `captures` value that is neither an assignment nor a block. | Write `captures: name = expr`, or a list of assignments. | @@ -31,9 +30,7 @@ The macro accumulates errors, so several clause problems surface at once. | ``not allowed here due to `#[spec]``` | A trait function parameter pattern the macro cannot forward. | Name the parameter; avoid `_`, `..`, `ref`, and macro patterns. | | ``or-pattern not allowed here due to `#[spec]``` | An or-pattern in a trait function parameter. | Name the parameter and match inside the body. | | ``The enclosing trait must have a `#[spec]` annotation.`` | Clauses on a trait function whose trait carries no `#[spec]`. | Add a bare `#[spec]` to the trait. | -| ``Unsupported spec element on trait.`` | Clauses on the `#[spec]` attached to a trait. | Keep the trait's attribute bare; put clauses on its functions. | -| ``Unsupported spec element on trait impl.`` | Clauses on the `#[spec]` attached to an `impl Trait for T`. | Keep it bare; put clauses on the functions. | -| ``Unsupported spec element on inherent impl.`` | Clauses on the `#[spec]` attached to an inherent `impl`. | Keep it bare; put clauses on the methods. | +| ``this `#[spec]` attribute must have no fields`` | Clauses on the attribute attached to a `trait` or `impl`. | Keep the enclosing attribute bare; put clauses on its functions or methods. | | ``cannot be weaker than the qualifiers on the trait`` | An impl claiming fewer guarantees than the trait promised. | An impl may only narrow; restore the trait's qualifiers. | | ``The #[spec] attribute doesn't yet support this item`` | `#[spec]` on an item kind with no support, such as `mod` or `type`. | Move it to a supported item. | | ```try_call` needs the `anodized_try` build `cfg` to be enabled`` | `try_call!` without the build configuration that generates its entry points. | Build with `--cfg anodized_try` and `--cfg anodized_panic`. | @@ -43,9 +40,8 @@ The macro accumulates errors, so several clause problems surface at once. | ``postinvariant failed`` | At runtime under `anodized_print`: a `maintains` was false on exit. | The body broke an invariant it was required to preserve. | -One wording to be aware of: the out-of-order message for function fields still lists -`inspects`, a clause that no longer exists. Ignore that entry and use the order -qualifiers, `requires`, `maintains`, `captures`, `ensures`. +For function fields, use the order qualifiers, `requires`, `maintains`, `captures`, `ensures`. +The removed `binds` and `inspects` clauses produce `unknown spec field`. ## Rustc errors reached through a spec @@ -98,19 +94,22 @@ const fn double(value: u32) -> u32 { } ``` -**`captured variable cannot escape `FnMut` closure body`** — the same closure wrapping again, -reached from a function that returns a `&mut` borrowed from one of its parameters. The -reference cannot outlive the closure that produced it. Note this one carries **no error code**, -so it will not match a search by `E`-number. Returning a shared `&` is unaffected. +Returning a mutable reference borrowed from a parameter is supported. This example compiles +and runs with runtime checks enabled: -```rust,compile_fail -// EXPECT: cannot escape `FnMut` closure body +```rust use anodized::spec; #[spec] fn first_mut(values: &mut Vec) -> &mut u8 { &mut values[0] } + +fn main() { + let mut values = vec![1]; + *first_mut(&mut values) = 2; + assert_eq!(values, vec![2]); +} ``` **`E0046: not all trait items implemented, missing: `__anodized_...``** — an @@ -212,13 +211,13 @@ RUSTFLAGS="--cfg anodized_print --cfg anodized_panic" cargo test Never relax a clause to silence a check. Fix whichever side is actually wrong, and if the clause really was wrong, say so explicitly in the commit message. -## Loop and data specs do not fire +## Loop and data specs need different checks -Runtime checking is implemented for functions only. Loop invariants, loop variants, and -`struct` or `enum` invariants never execute, so a plainly false one will not fail a test — -never read a passing suite as evidence that one holds. +Loop invariants and variants are parsed and dropped: they neither run nor reach the type +checker. An unknown identifier in a loop condition can compile silently. Review these by eye. -Type-checking differs between them, which matters more than it sounds. A `struct` condition is -embedded and type-checked, so a typo in one is `E0425`. Loop and `enum` conditions are dropped -before they reach the compiler: a loop invariant naming an identifier that does not exist -anywhere compiles without complaint. Review those by eye; nothing else will. +Both `struct` and `enum` invariants generate a type-checked `anodized::types::Spec::predicate` +unless `anodized_discard_specs` is enabled. An unknown name in either produces `E0425`. +Construction alone does not evaluate that predicate. Call it explicitly, or use `Spec!(T)` +at a spec'd function boundary with runtime checks enabled. A passing test that never evaluates +the predicate is not evidence that the invariant holds. diff --git a/plugins/anodized/skills/anodized/migration.md b/plugins/anodized/skills/anodized/migration.md index 22df0fe1..3786be44 100644 --- a/plugins/anodized/skills/anodized/migration.md +++ b/plugins/anodized/skills/anodized/migration.md @@ -17,6 +17,8 @@ more likely to be stale than to be wrong about some other crate. | `inspects: ...` | `ensures: \|pat\| [...]` | | `requires: \|\| condition` | `requires: condition` | +In 0.7, `binds` and `inspects` produce `unknown spec field`; use the replacements above. + The automatic `old_` binding is the one that bites hardest, because the replacement is not a rename: captures must be declared, and they are visible only to postconditions. diff --git a/plugins/anodized/skills/anodized/reference.md b/plugins/anodized/skills/anodized/reference.md index 2ac51f52..16338abe 100644 --- a/plugins/anodized/skills/anodized/reference.md +++ b/plugins/anodized/skills/anodized/reference.md @@ -154,5 +154,5 @@ consistently across a codebase. | `#[requires(...)]` / `#[ensures(...)]` | Never existed. One unified `#[spec(...)]`. | | Closure-form preconditions | Removed in 0.6. Write the expression directly. | -The parser still recognizes `binds` and `inspects` purely so it can tell you what replaced -them; they are scheduled for deletion before 0.7. +In 0.7, `binds` and `inspects` produce `unknown spec field`. Replace them with an `ensures` +closure; the parser no longer emits a dedicated migration diagnostic. From 63883e2f40b644201003fafcdbbdaeaf8b7b97e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1t=C3=A9=20Kov=C3=A1cs?= <481354+mkovaxx@users.noreply.github.com> Date: Sat, 17 Oct 2026 13:57:43 +0900 Subject: [PATCH 10/10] Apply batched suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Máté Kovács <481354+mkovaxx@users.noreply.github.com> --- crates/anodized/REFERENCE.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/crates/anodized/REFERENCE.md b/crates/anodized/REFERENCE.md index 6efefd3b..08f21ae0 100644 --- a/crates/anodized/REFERENCE.md +++ b/crates/anodized/REFERENCE.md @@ -135,7 +135,7 @@ use anodized::spec; // Invariant: length never exceeds capacity maintains: vec.len() <= vec.capacity(), )] -fn push_checked(vec: &mut Vec, value: T) { vec.push(value) } +fn push_checked(vec: &mut Vec, value: T) { todo!() } ``` ### `captures`: Capture Entry-Time Values @@ -208,7 +208,6 @@ reconstructed. use anodized::spec; #[spec( - requires: input < i32::MAX - 1, // Bind the return value to `output` for the entire group of postconditions. ensures: |output| [ output > input, @@ -245,7 +244,7 @@ fn sort_pair(pair: (i32, i32)) -> (i32, i32) { todo!() } use anodized::spec; #[spec( - requires: amount >= 0 && *balance >= amount, + requires: *balance >= amount, maintains: *balance >= 0, captures: initial_balance = *balance, ensures: |(new_balance, receipt_amount)| [ @@ -254,7 +253,7 @@ use anodized::spec; *balance == new_balance, ], )] -fn withdraw(balance: &mut i64, amount: i64) -> (i64, i64) { todo!() } +fn withdraw(balance: &mut u64, amount: u64) -> (u64, u64) { todo!() } ``` ### Loop Specs