Skip to content

Extend the Rust skill catalogue with verification and supply-chain skills - #4

Merged
leynos merged 19 commits into
mainfrom
skill-refresh
May 29, 2026
Merged

Extend the Rust skill catalogue with verification and supply-chain skills#4
leynos merged 19 commits into
mainfrom
skill-refresh

Conversation

@leynos

@leynos leynos commented May 27, 2026

Copy link
Copy Markdown
Owner

Summary

This branch extends the Rust skill catalogue with the advanced
"impeccable software" stance: verification tooling, supply-chain
hygiene, and architectural decision records. It also imports the
upstream kani and verus deep-dive skills and rewires their
installation guidance to the new
rust-prover-tools CLI,
retiring the ad hoc install-verus.sh and run-verus.sh scripts.

Existing language skills gain four new reference pages on encapsulation
and RAII, UnsafeCell interior mutability, misuse-resistant APIs, and
rigorous benchmarking, plus the red flags and routing entries that
direct readers to them. A new CHANGELOG.md records the additions in
Common Changelog format.

Execplan:
docs/execplans/advanced-encapsulation-and-verification.md

Review walkthrough

Validation

  • find skills -name SKILL.md -print0 | xargs -0 wc -c | sort -n:
    17 SKILL.md files totalling 59 483 bytes; 11 compact skills sit
    between 1.3 KB and 4 KB. Only arch-crate-design (5.8 KB) and the
    imported kani (7.6 KB) and verus (10.2 KB) deep dives exceed the
    4 KB compact envelope, all justified by their role.
  • find skills -type f \( -name 'install-verus.sh' -o -name 'run-verus.sh' \): no matches; the retired shell scripts were not
    carried across.
  • grep -l rust-prover-tools skills/kani/SKILL.md skills/verus/SKILL.md skills/kani/references/installation-note.md skills/verus/references/installation-note.md: all four files match,
    confirming the rewiring covers both deep dives and both installation
    notes.
  • markdownlint-cli2 'docs/**/*.md' 'skills/**/*.md' 'README.md' 'CHANGELOG.md': 54 files linted, 0 errors.

Notes

  • The size envelope is satisfied: five new first-class skills
    (rust-verification, arch-supply-chain, arch-decision-records,
    kani, verus); no newly authored compact SKILL.md over 4 KB; no
    reference file over 8 KB. The deep-dive kani and verus SKILL.md
    files intentionally carry larger envelopes than the rest, matching
    the tolerance recorded in the execplan.
  • The README gains a single bullet pairing verification with
    supply-chain content; deeper detail lives in
    docs/skill-catalogue-status.md
    and the router.
  • rust-prover-tools does not currently provide a fallback installer
    for Verus comparable to the upstream cargo install kani-verifier
    route; the verus installation note documents that asymmetry.

Summary by Sourcery

Extend the Rust skill catalogue to cover advanced verification, supply-chain hygiene, and architectural decision records, and import deep-dive Kani and Verus skills wired through the shared rust-prover-tools CLI.

New Features:

  • Add a rust-verification skill that routes between Miri, sanitizers, property and mutation testing, deterministic concurrency exploration tools, Kani, and Verus by failure mode.
  • Introduce arch-supply-chain and arch-decision-records skills to cover dependency hygiene, auditing, SemVer guardrails, and Y-Statement-based architecture decision records.
  • Import Kani and Verus deep-dive skills, including neutralised example code and reference materials for harnesses and proofs.

Enhancements:

  • Enrich existing language and architecture skills with new reference material on encapsulation and RAII, UnsafeCell-based interior mutability, misuse-resistant APIs, and rigorous benchmarking practices.
  • Update the router, routing matrix, README, and catalogue-status documentation to surface the new skills and position verification and supply-chain content within the catalogue.
  • Adopt rust-prover-tools as the canonical installer/runner for Verus and Kani, retiring ad hoc install and run scripts in favour of version-pinned CLI flows.

Documentation:

  • Add a detailed exec plan documenting the design, scope, and validation of the advanced encapsulation and verification expansion, and introduce a Common Changelog-formatted CHANGELOG.md capturing these catalogue changes.

leynos added 15 commits May 27, 2026 15:04
Plan extends the Rust skill catalogue with verification, supply-chain,
and decision-records skills, imports the upstream kani and verus deep
dives from agent-helper-scripts, and rewires their installation and
runner guidance to rust-prover-tools. Stage 0 is complete: records the
prover-tools CLI surface under Surprises & Discoveries so subsequent
stages can cite the canonical commands.
Add a new reference page covering ownership as architectural decoupling
and the Mutex/MutexGuard/Drop wireframe. Link to it from SKILL.md and
cross-link to the new UnsafeCell reference (added in a later commit)
so the interior-mutability story is reachable from both directions.
New reference explains why UnsafeCell is the only sound base for shared
mutation, lists the invariants any wrapper must enforce, and enumerates
common UB pitfalls. Cross-links to the future rust-verification skill
for Miri and loom guidance.
New reference covers typestate, hidden-inner newtypes, anti-boolean-
blindness with domain enums or options structs, the relevant Rust API
Guidelines tags (C-SEALED, C-NEWTYPE-HIDE, C-SMART-PTR,
C-STRUCT-PRIVATE), and SemVer tooling (cargo-semver-checks,
cargo-public-api). SKILL.md adds boolean blindness as a red flag and
points to the new page.
New reference covers paired benchmarking (Tango), deterministic profiling
(iai-callgrind), open-versus-closed system models, tail latency and CDFs,
and goodput. SKILL.md and benchmark-discipline.md link to it so the new
disciplines are reachable from both the trigger and the daily-hygiene
reference.
Add a single packaging-and-release bullet pointing at arch-supply-chain
for dependency auditing and SemVer guardrails so the boundary stays
clear: arch-crate-design owns 'should I split this?'; arch-supply-chain
owns 'how do I trust this dependency?'.
Bring the deep-dive Kani skill into the catalogue, retargeted at the
new rust-prover-tools install/check surface
(https://github.com/leynos/rust-prover-tools). The body is compressed
from 17.5 KB to 7.6 KB by trimming paragraphs that restate Rust basics
and moving worked harnesses into references/harness-examples.md.
HNSW-specific examples are replaced with neutral graph-with-
bidirectional-links placeholders. The reference Rust file is renamed
to drop product-specific symbols and to keep the file referenceable on
its own.
Adapt the upstream verus skill for the rust-skill catalogue. Replace the
in-tree install/run shell scripts with the prover-tools CLI, neutralise
the HNSW-specific naming (EdgeSpec/ItemSpec/SegmentSpec), and trim
content that restated Rust basics. Add three references: a worked
proof-examples walkthrough, a project-layout reference source, and an
installation note explaining the rust-prover-tools rationale.
Both stages of skill extension are now landed: the existing-skill
extensions from Stage A (five commits) and the kani/verus imports from
Stage A.5 (two commits).
A compact routing skill for picking the smallest verification adversary
that matches a failure mode: Miri/sanitizers for UB, proptest for input
gaps, cargo-mutants for test gaps, turmoil/loom/shuttle for schedule
chaos, kani for bounded structural invariants, verus for unbounded
algebraic properties. References cover per-tool rationale and the
determinism fences chaos tools require. Cross-links into the existing
kani and verus deep dives.
A compact skill that frames the dependency graph as a deliberately
shaped trust surface. Names the decision-by-question table
(cargo-audit, cargo-deny, cargo-vet, cargo-semver-checks,
cargo-public-api) and covers lockfile policy and SemVer guardrails at
the publishing boundary. References cover the cargo-vet trust model
(audits, imports, exemptions, criteria) and day-to-day hygiene
patterns (graph shrinking, duplication detection, risk isolation,
deny.toml policy).
A compact skill on writing immutable Y-Statement ADRs at the moment
a decision becomes hard to reverse. Rust-flavoured: ADRs encode the
invariants the type system already enforces (typestate edges, trait
bounds, unsafe contracts, verification-tool choice). The reference
holds the full file template and three worked examples (typestate,
verification-tool selection, unsafe alignment invariant).
Record the additions and changes from the advanced-encapsulation-and-
verification refresh in a single Unreleased block: the three new
first-class skills (rust-verification, arch-supply-chain,
arch-decision-records), the imported kani and verus deep dives, the
four new reference pages on existing skills, and the SKILL.md tweaks
that route into them.
Add one short bullet to README.md naming the new advanced-stance
content. Extend docs/skill-catalogue-status.md with a catalogue-contents
overview that mentions the imported kani/verus deep dives and the
rust-prover-tools install route. Update the rust-router SKILL and the
routing-matrix reference so the new skills (rust-verification,
arch-supply-chain, arch-decision-records, kani, verus) are reachable
from a one-line question.
Stages B (three new first-class skills), C (CHANGELOG), D (README,
router, catalogue status), and E (validation) are now all landed and
recorded. The validation transcript captures the four checks from the
plan: SKILL.md size distribution, absence of the retired shell scripts,
rust-prover-tools references across the kani and verus skills, and a
zero-error markdownlint sweep.
@coderabbitai

coderabbitai Bot commented May 27, 2026

Copy link
Copy Markdown

Review Change Stack

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 512db3e8-1306-4404-831f-2d2e3f00a5cf

📥 Commits

Reviewing files that changed from the base of the PR and between 4b6857b and 96d86d6.

📒 Files selected for processing (1)
  • docs/users-guide.md

Extend Rust Skill Catalogue with Verification and Supply‑Chain Skills

This PR extends the Rust skill catalogue with verification, supply‑chain hygiene and ADR practice, governed by the new living execplan at docs/execplans/advanced-encapsulation-and-verification.md (staged rollout, validation rules, size envelopes and acceptance criteria). The execplan and repository validation checks (including references to rust-prover-tools in the imported Kani/Verus materials) are present in-tree.

New first‑class skills

  • rust-verification — guidance for selecting and layering verification tools by failure mode (Miri, sanitizers, proptest, cargo‑mutants, loom, shuttle, turmoil, Kani, Verus). Includes tool‑selection and deterministic‑chaos references. Kani/Verus installation/run documented via rust-prover-tools.
  • arch-supply-chain — dependency‑hygiene and trust shaping (cargo-audit, cargo-deny, cargo-vet, cargo-semver-checks, cargo-public-api), Cargo.lock/MSRV/SemVer guidance, dependency‑hygiene patterns and red flags.
  • arch-decision-records — Y‑Statement ADR template (six clauses), file shape, quality red flags, supersession rules, and three Rust‑flavoured worked examples.

Imported verification deep‑dives and proptest

  • kani — deep dive added (SKILL, harness examples, installation via rust-prover-tools with a documented fallback when prover-tools cannot be installed).
  • verus — deep dive added (SKILL, proof examples). Verus install/run flow is rewired to rust-prover-tools; previous in-repo install-verus.sh / run-verus.sh helpers are retired and Verus is explicitly documented as requiring prover-tools (no fallback installer).
  • proptest — new deep‑dive skill added (installed as a Cargo dev‑dependency, not via rust-prover-tools). Routing updated so rust-verification escalates into proptest, kani and verus.

Expanded references added to existing skills

  • Encapsulation & RAII: skills/rust-memory-and-state/references/encapsulation-and-raii.md
  • UnsafeCell & interior mutability: skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md
  • Misuse‑resistant APIs: skills/rust-types-and-apis/references/misuse-resistant-apis.md
  • Rigorous benchmarking: skills/rust-performance-and-layout/references/rigorous-benchmarking.md

Docs, routing and changelog

  • CHANGELOG.md added using Common Changelog style documenting the new skills/imports and references.
  • README updated to mention verification tools, supply‑chain guardrails and Y‑Statement ADRs.
  • docs/skill-catalogue-status.md updated to list catalogue contents and note larger size envelopes for imported deep dives.
  • rust-router SKILL and routing-matrix extended to route verification, supply‑chain and irreversible/ADR decisions appropriately.
  • docs/users-guide.md added/updated with operator‑facing guidance for the new entry points and tool workflows.

Cross‑linking and red flags

  • arch-crate-design points to arch-supply-chain for dependency‑audit guidance.
  • rust-unsafe-and-ffi flags shared mutation without UnsafeCell and links to the interior‑mutability guide.
  • rust-types-and-apis adds a boolean‑blindness red flag and links to misuse‑resistant APIs.
  • rust-performance-and-layout links to rigorous benchmarking.

Validation & governance artefacts

  • ExecPlan present: docs/execplans/advanced-encapsulation-and-verification.md (records staged rollout, acceptance criteria, risk register and completed validation steps).
  • SKILL.md size envelope checks recorded; larger envelopes for imported deep dives noted.
  • Retired scripts removed: previous install-verus.sh and run-verus.sh helpers retired.
  • grep/validation confirms rust-prover-tools / prover-tools references in Kani/Verus files and installation notes.
  • markdownlint and other lint/validation steps reported as run (zero markdownlint errors recorded).

Notable choices and scope notes

  • Prover tooling asymmetry: Kani retains a documented fallback install route where useful; Verus is documented as requiring rust-prover-tools with no fallback installer—this is recorded in the execplan and the Verus installation note.
  • Documentation-first: no exported/public API entities were modified. Example/proof/harness files are provided as reference material (non‑compilable or documentation snippets where applicable).

Walkthrough

Extend the Rust skill catalogue with verification, supply‑chain hygiene, and ADR guidance; add rust-verification/proptest/kani/verus skills and references; rewire prover installs to rust-prover-tools; update router, ExecPlan, CHANGELOG, README and an operator users’ guide.

Changes

Verification and Supply-Chain Skill Catalogue Expansion

Layer / File(s) Summary
Governance: ExecPlan, catalogue status, and changelog
docs/execplans/advanced-encapsulation-and-verification.md, docs/skill-catalogue-status.md, CHANGELOG.md
Add a living ExecPlan defining stages, constraints, validation steps, catalogue-status content listing new skills, and a Common Changelog Unreleased recording all additions.
Router integration and users guide
skills/rust-router/SKILL.md, skills/rust-router/references/routing-matrix.md, docs/users-guide.md, README.md
Add routing bullets and matrix criteria for verification/supply-chain/ADR cases; add operator users’ guide and update README Learn/Features bullets.
Architectural Decision Records: skill and template
skills/arch-decision-records/SKILL.md, skills/arch-decision-records/references/y-statement-template.md
Add arch-decision-records skill with Y‑Statement six-clause template, file-shape rules, red flags and three Rust-focused examples plus practical authoring rules.
Supply-chain hygiene: skill and references
skills/arch-supply-chain/SKILL.md, skills/arch-supply-chain/references/cargo-vet-and-trust.md, skills/arch-supply-chain/references/dependency-hygiene.md, skills/arch-crate-design/SKILL.md
Add arch-supply-chain skill mapping trust questions to cargo tools, cargo-vet trust-model guide, and dependency-hygiene patterns; cross-link arch-crate-design.
Rust verification: skill and deterministic-chaos/tool-selection
skills/rust-verification/SKILL.md, skills/rust-verification/references/tool-selection.md, skills/rust-verification/references/deterministic-chaos.md
Add rust-verification skill with failure-mode tool layering, deterministic-chaos injection patterns, and per-tool selection guidance.
Kani bounded model checking: skill, install, harnesses
skills/kani/SKILL.md, skills/kani/references/installation-note.md, skills/kani/references/harness-examples.md, skills/kani/references/kani-harness-example.rs
Add Kani skill, installation via prover-tools, harness examples and a reference harness file with three harnesses and helpers.
Verus deductive verification: skill, install, proof examples
skills/verus/SKILL.md, skills/verus/references/installation-note.md, skills/verus/references/proof-examples.md, skills/verus/references/verus-proof-example.rs
Add Verus skill, install/run via prover-tools, proof-pattern templates, and a Verus reference file with spec types, predicates and lemmas.
Proptest property testing: skill and examples
skills/proptest/SKILL.md, skills/proptest/references/installation-note.md, skills/proptest/references/proptest-example.rs, skills/proptest/references/strategy-examples.md
Add proptest skill, installation guidance, a full example Rust proptest file and a strategy-examples reference covering common patterns and state-machine sketches.
Types, unsafe, memory and performance references
skills/rust-types-and-apis/references/misuse-resistant-apis.md, skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md, skills/rust-memory-and-state/references/encapsulation-and-raii.md, skills/rust-performance-and-layout/references/rigorous-benchmarking.md
Add misuse-resistant API patterns, UnsafeCell/interior-mutability guidance, encapsulation-and-RAII reference, and rigorous benchmarking discipline.
README features
README.md
Update Features and Learn more bullets to surface verification, supply-chain, and ADR tooling and link to users’ guide.

Sequence Diagram(s)
(Skipped — changes are documentation additions and routing updates without a multi-component runtime control flow that benefits from a sequence diagram.)

"Ship the docs, pin the toolchain tight,
ADRs to capture the architect’s sight,
Provers centralised for reproducible night,
Supply chains trimmed and benchmarks right. 🧭✨"

Suggest labels

Roadmap

You are an AI agent. Summarise any follow-up validation commands to run locally: run markdownlint, git diff --check, grep for retired install scripts, and verify README/CHANGELOG links.
✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch skill-refresh

@sourcery-ai

sourcery-ai Bot commented May 27, 2026

Copy link
Copy Markdown

Reviewer's Guide

Extends the Rust skill catalogue with an advanced verification/supply-chain/ADR stance by adding new first-class skills (including imported Kani/Verus deep dives wired through rust-prover-tools), several focused reference pages, and routing/README/Changelog updates that integrate these into the existing router and language/architecture skills.

Sequence diagram for routing verification questions to Kani/Verus via rust-prover-tools

sequenceDiagram
    actor User
    participant RustRouter as rust_router
    participant RustVerification as rust_verification
    participant KaniSkill as kani
    participant VerusSkill as verus
    participant ProverTools as rust_prover_tools

    User->>RustRouter: ask_about("prove property / verification")
    RustRouter->>RustVerification: route_to_skill("rust-verification")

    RustVerification->>RustVerification: select_tool_by_failure_mode
    alt bounded_state_or_structural_invariant
        RustVerification->>KaniSkill: load_skill("kani")
        KaniSkill->>ProverTools: prover-tools_kani_install
        KaniSkill->>ProverTools: prover-tools_kani_check-version
        KaniSkill-->>User: guidance_on_kani_harnesses
    else unbounded_algebraic_property
        RustVerification->>VerusSkill: load_skill("verus")
        VerusSkill->>ProverTools: prover-tools_verus_install
        VerusSkill->>ProverTools: prover-tools_verus_run_proof_file
        VerusSkill-->>User: guidance_on_verus_proofs
    end
Loading

File-Level Changes

Change Details Files
Introduce new verification, supply-chain, and ADR skills plus their supporting references, and import the Kani/Verus deep-dive skills
  • Add rust-verification skill to route between Miri, sanitizers, property testing, mutation testing, concurrency chaos tools, Kani, and Verus, with detailed selection/determinism references
  • Add arch-supply-chain skill for dependency hygiene, auditing, SemVer guardrails, with cargo-vet and dependency-hygiene reference pages
  • Add arch-decision-records skill defining Y-Statement ADR practice with a Rust-focused template/example reference
  • Import and adapt kani deep-dive skill, including harness structure and installation notes, plus reference examples
  • Import and adapt verus deep-dive skill, including installation/running guidance, proof-structure examples, and reference code
skills/rust-verification/SKILL.md
skills/rust-verification/references/tool-selection.md
skills/rust-verification/references/deterministic-chaos.md
skills/arch-supply-chain/SKILL.md
skills/arch-supply-chain/references/cargo-vet-and-trust.md
skills/arch-supply-chain/references/dependency-hygiene.md
skills/arch-decision-records/SKILL.md
skills/arch-decision-records/references/y-statement-template.md
skills/kani/SKILL.md
skills/kani/references/installation-note.md
skills/kani/references/harness-examples.md
skills/kani/references/kani-harness-example.rs
skills/verus/SKILL.md
skills/verus/references/installation-note.md
skills/verus/references/proof-examples.md
skills/verus/references/verus-proof-example.rs
Extend existing language and performance skills with advanced encapsulation, UnsafeCell, misuse-resistant API, and benchmarking guidance
  • Add encapsulation/RAII reference and link from memory-and-state skill, emphasizing ownership as an architectural lever and Mutex/Guard/Drop patterns
  • Add UnsafeCell/interior-mutability reference and link from unsafe-and-ffi skill; flag missing-UnsafeCell shared mutation; point to verification tools for unsafe review
  • Add misuse-resistant-APIs reference and link from types-and-apis skill; add boolean-blindness red flag and describe typestate/newtype/API-guideline/SemVer-tooling ties
  • Add rigorous-benchmarking reference and link from performance-and-layout skill and benchmark-discipline reference, covering Tango, iai-callgrind, load models, tail latency, and goodput
skills/rust-memory-and-state/SKILL.md
skills/rust-memory-and-state/references/encapsulation-and-raii.md
skills/rust-unsafe-and-ffi/SKILL.md
skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md
skills/rust-types-and-apis/SKILL.md
skills/rust-types-and-apis/references/misuse-resistant-apis.md
skills/rust-performance-and-layout/SKILL.md
skills/rust-performance-and-layout/references/rigorous-benchmarking.md
skills/rust-performance-and-layout/references/benchmark-discipline.md
Update routing, catalogue documentation, and README to surface the new skills and deep dives
  • Expand router SKILL and routing matrix to direct verification/supply-chain/ADR questions to new skills and route into Kani/Verus when proofs are required
  • Update skill catalogue status doc to enumerate router, language, architecture/domain, verification, and focused skills, and document Kani/Verus envelopes and rust-prover-tools usage
  • Add README bullet describing the advanced "impeccable software" stance, pairing verification tools with supply-chain and ADR content
skills/rust-router/SKILL.md
skills/rust-router/references/routing-matrix.md
docs/skill-catalogue-status.md
README.md
Introduce an execplan and Common Changelog entry governing the advanced verification and encapsulation work
  • Add detailed execplan capturing constraints, tolerances, risks, validation, and staged implementation for the verification/supply-chain/ADR and Kani/Verus import work
  • Create initial Common Changelog file documenting the newly added skills, references, and key changes to existing skills
docs/execplans/advanced-encapsulation-and-verification.md
CHANGELOG.md

Tips and commands

Interacting with Sourcery

  • Trigger a new review: Comment @sourcery-ai review on the pull request.
  • Continue discussions: Reply directly to Sourcery's review comments.
  • Generate a GitHub issue from a review comment: Ask Sourcery to create an
    issue from a review comment by replying to it. You can also reply to a
    review comment with @sourcery-ai issue to create an issue from it.
  • Generate a pull request title: Write @sourcery-ai anywhere in the pull
    request title to generate a title at any time. You can also comment
    @sourcery-ai title on the pull request to (re-)generate the title at any time.
  • Generate a pull request summary: Write @sourcery-ai summary anywhere in
    the pull request body to generate a PR summary at any time exactly where you
    want it. You can also comment @sourcery-ai summary on the pull request to
    (re-)generate the summary at any time.
  • Generate reviewer's guide: Comment @sourcery-ai guide on the pull
    request to (re-)generate the reviewer's guide at any time.
  • Resolve all Sourcery comments: Comment @sourcery-ai resolve on the
    pull request to resolve all Sourcery comments. Useful if you've already
    addressed all the comments and don't want to see them anymore.
  • Dismiss all Sourcery reviews: Comment @sourcery-ai dismiss on the pull
    request to dismiss all existing Sourcery reviews. Especially useful if you
    want to start fresh with a new review - don't forget to comment
    @sourcery-ai review to trigger a new review!

Customizing Your Experience

Access your dashboard to:

  • Enable or disable review features such as the Sourcery-generated pull request
    summary, the reviewer's guide, and others.
  • Change the review language.
  • Add, remove or edit custom review instructions.
  • Adjust other review settings.

Getting Help

@leynos
leynos marked this pull request as ready for review May 27, 2026 16:07

@sourcery-ai sourcery-ai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry @leynos, you have reached your weekly rate limit of 2500000 diff characters.

Please try again later or upgrade to continue using Sourcery

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ec239693ab

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread skills/verus/references/verus-proof-example.rs
@coderabbitai coderabbitai Bot added the Roadmap label May 27, 2026

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 9

🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@skills/arch-decision-records/references/y-statement-template.md`:
- Around line 8-12: The Y-Statement template and its worked examples use
first-person pronouns ("we", "our"); update the template (the Y-Statement block)
and the example sections referenced (around the Y-Statement and worked examples)
to use neutral, third-person constructions (e.g., "The team decided", "Decision:
<option>", or passive/impersonal phrasing like "Decided: <option>") and remove
any "we/our" occurrences in lines corresponding to the Y-Statement and examples
so they comply with the repository markdown style rules.

In `@skills/arch-decision-records/SKILL.md`:
- Line 3: The front-matter description contains a trigger sentence using the
first-person pronoun "we"; update the `description` field in SKILL.md to
rephrase that trigger without first- or second-person pronouns while preserving
intent (e.g., change "Use when we..." to "Use when a choice is hard to
reverse..." or similar). Locate the `description:` front-matter line and replace
the clause that starts with the quoted trigger so it avoids "we"/"I"/"you" but
keeps references to scenarios like typestate, trait bounds, public API shape,
`unsafe` invariants, runtime selection, and verification tooling.

In `@skills/arch-supply-chain/references/dependency-hygiene.md`:
- Line 13: The phrase "you need" in the markdown should be rewritten to remove
the second-person pronoun — replace the instance of "you need" with a neutral
phrase such as "required features" or "project-required features" (or similar
context-appropriate wording) and scan the document for other occurrences of
second-person/first-person pronouns to convert them to neutral phrasing; update
the sentence containing "you need" so it reads grammatically with the chosen
neutral term.

In `@skills/arch-supply-chain/SKILL.md`:
- Around line 26-28: Update the decision-surface questions to remove
first-person phrasing: replace "someone I trust" with a neutral phrase such as
"trusted reviewer" and replace "my public API" with "the crate's public API"
(these appear in the table cells containing "Has this crate been reviewed by
someone I trust?" and "Does this PR break my public API?"); also scan nearby
question text for any other first- or second-person pronouns and convert them to
neutral wording to comply with the markdown docstyle guideline.

In `@skills/rust-memory-and-state/references/encapsulation-and-raii.md`:
- Line 44: Change the British oxendict variant "generalises" to the oxendict
-ize spelling "generalizes" in the sentence fragment "resource) generalises to
transaction handles, file locks, span guards," so the document uses the
repository's mandated en-GB-oxendict style; update that single word in the line
containing that fragment and run a quick grep for other occurrences of
"generalises" to ensure consistency.

In `@skills/rust-performance-and-layout/references/rigorous-benchmarking.md`:
- Around line 15-18: The paragraph starting "Use Tango when the change is a
swap..." uses second-person phrasing ("you can ship", "are you benchmarking");
rewrite those sentences into neutral declarative voice so they follow the
Markdown style policy—for example change "you can ship as evidence" to "it can
be presented as evidence" and change the question form "are you benchmarking..."
to a neutral statement like "the question is which implementation is faster on
this input"; apply the same transformation to the similar wording around lines
73–75 so all instances avoid "you"/"we"/"I".

In `@skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md`:
- Line 15: Replace the British -iser/-ised spellings with the repository's
en-GB-oxendict -ize/-ized forms in this document: change “optimiser” to
“optimizer” in the sentence containing “the language level—the optimiser can and
will reorder reads, hoist them out”, change “initialised” to “initialized” where
it appears (around Line 33), and change both occurrences of “serialise” to
“serialize” (around Lines 41 and 43); update only the word spellings preserving
surrounding punctuation and sentence flow so examples, headings, and code-like
snippets remain intact.

In `@skills/rust-verification/references/tool-selection.md`:
- Around line 34-38: The sentence uses second-person voice ("Use it
periodically...")—change Lines 37–38 to neutral, instruction-free phrasing:
reword the clause about running cargo-mutants to passive/impersonal voice (e.g.,
"Run periodically on important modules" → "Run periodically on important
modules" or "Run periodically on modules of interest") and rephrase the report
description to avoid "tells you" (e.g., "the report indicates which assertions
require strengthening, not which production code should be changed"); update the
sentence that follows the `cargo-mutants` description so it remains factually
identical but removes all second-person pronouns.

In `@skills/verus/references/proof-examples.md`:
- Around line 3-10: Replace Oxford -isation/-ising spellings with
-ization/-izing in the affected headings and sentences: change
"canonicalisation" to "canonicalization" in the document title and "##
Canonicalisation: ordering an unordered pair", and change "normalising" to
"normalizing" in the sentence beginning "A common pattern is normalising an edge
or pair..."; ensure the replacements occur for those exact tokens so the file
uses en-GB-oxendict (-ize) spelling consistently.
🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 86a3b446-b21d-48fa-a9c6-f3fa2f720608

📥 Commits

Reviewing files that changed from the base of the PR and between c643fda and ec23969.

📒 Files selected for processing (32)
  • CHANGELOG.md
  • README.md
  • docs/execplans/advanced-encapsulation-and-verification.md
  • docs/skill-catalogue-status.md
  • skills/arch-crate-design/SKILL.md
  • skills/arch-decision-records/SKILL.md
  • skills/arch-decision-records/references/y-statement-template.md
  • skills/arch-supply-chain/SKILL.md
  • skills/arch-supply-chain/references/cargo-vet-and-trust.md
  • skills/arch-supply-chain/references/dependency-hygiene.md
  • skills/kani/SKILL.md
  • skills/kani/references/harness-examples.md
  • skills/kani/references/installation-note.md
  • skills/kani/references/kani-harness-example.rs
  • skills/rust-memory-and-state/SKILL.md
  • skills/rust-memory-and-state/references/encapsulation-and-raii.md
  • skills/rust-performance-and-layout/SKILL.md
  • skills/rust-performance-and-layout/references/benchmark-discipline.md
  • skills/rust-performance-and-layout/references/rigorous-benchmarking.md
  • skills/rust-router/SKILL.md
  • skills/rust-router/references/routing-matrix.md
  • skills/rust-types-and-apis/SKILL.md
  • skills/rust-types-and-apis/references/misuse-resistant-apis.md
  • skills/rust-unsafe-and-ffi/SKILL.md
  • skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md
  • skills/rust-verification/SKILL.md
  • skills/rust-verification/references/deterministic-chaos.md
  • skills/rust-verification/references/tool-selection.md
  • skills/verus/SKILL.md
  • skills/verus/references/installation-note.md
  • skills/verus/references/proof-examples.md
  • skills/verus/references/verus-proof-example.rs

Comment thread skills/arch-decision-records/references/y-statement-template.md
Comment thread skills/arch-decision-records/SKILL.md
Comment thread skills/arch-supply-chain/references/dependency-hygiene.md
Comment thread skills/arch-supply-chain/SKILL.md
Comment thread skills/rust-memory-and-state/references/encapsulation-and-raii.md Outdated
Comment thread skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md Outdated
Comment thread skills/rust-verification/references/tool-selection.md
Comment thread skills/verus/references/proof-examples.md Outdated
Three review findings flagged Oxford -ise/-ised spellings in new
documentation that should follow the repository's mandated
en-GB-oxendict (-ize) style:

- encapsulation-and-raii.md: generalises → generalizes
- unsafecell-and-interior-mutability.md: optimiser → optimizer (twice),
  initialised → initialized, serialise → serialize
- proof-examples.md: canonicalisation → canonicalization (twice in
  prose; the spec-fn name stays untouched), normalising → normalizing

Two additional generalise(s) occurrences in y-statement-template.md and
the execplan are corrected too, since the first finding asked for a
consistency sweep on that word.

Out-of-scope -ise occurrences in tool-selection.md, verus/SKILL.md, and
elsewhere in the execplan are left unchanged because they were not part
of any provided finding.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)
skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md (1)

6-7: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Eliminate second-person pronouns.

Lines 6-7 use "you" twice: "If you reach for interior mutability without one of those wrappers, you are committing to proving...". Rewrite using imperative or impersonal constructions:

"Reaching for interior mutability without one of those wrappers commits the author to proving that the bespoke construction upholds the same rules."

or

"Custom interior mutability requires proving the construction upholds the same rules the standard wrappers guarantee."

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: Avoid 2nd person or 1st person pronouns ('I', 'you', 'we'), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md`
around lines 6 - 7, Replace the second-person phrasing in the sentence within
unsafecell-and-interior-mutability.md (the line beginning "If you reach for
interior mutability...") with an impersonal or imperative construction; for
example, change it to "Reaching for interior mutability without one of those
wrappers commits the author to proving that the bespoke construction upholds the
same rules" or "Custom interior mutability requires proving the construction
upholds the same rules the standard wrappers guarantee" so that the text avoids
"you" and follows the project's docstyle.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Outside diff comments:
In `@skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md`:
- Around line 6-7: Replace the second-person phrasing in the sentence within
unsafecell-and-interior-mutability.md (the line beginning "If you reach for
interior mutability...") with an impersonal or imperative construction; for
example, change it to "Reaching for interior mutability without one of those
wrappers commits the author to proving that the bespoke construction upholds the
same rules" or "Custom interior mutability requires proving the construction
upholds the same rules the standard wrappers guarantee" so that the text avoids
"you" and follows the project's docstyle.

ℹ️ Review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 6b3113b0-a4f5-4be1-ada7-40a289ad9a20

📥 Commits

Reviewing files that changed from the base of the PR and between ec23969 and e508d64.

📒 Files selected for processing (5)
  • docs/execplans/advanced-encapsulation-and-verification.md
  • skills/arch-decision-records/references/y-statement-template.md
  • skills/rust-memory-and-state/references/encapsulation-and-raii.md
  • skills/rust-unsafe-and-ffi/references/unsafecell-and-interior-mutability.md
  • skills/verus/references/proof-examples.md

- New docs/users-guide.md: operator-facing guide covering catalogue
  installation, router invocation, the rust-prover-tools install route
  for kani/verus, and the decision points the new verification,
  supply-chain, and decision-record skills address.
- README links to the guide from "Learn more".
- CHANGELOG records the new doc under Documentation.
- ExecPlan: flip the first Progress item to [x] with a note that the
  user approved the revised plan.

Addresses the two PR check warnings: User-Facing Documentation
(create users' guide) and Developer Documentation (mark approval
Progress item complete).

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@docs/users-guide.md`:
- Around line 82-84: The sentence "`rust-router` routes by the concrete problem
in front of you, not by the file you happen to be editing." uses second-person
phrasing; update it to neutral wording per docstyle rules by removing "you" and
rephrasing (e.g., "`rust-router` routes by the concrete problem at hand, not by
the file being edited.")—locate and replace this string in the router
description section so the documentation avoids 2nd-person pronouns.
🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 84275ce8-fc6d-48e4-a82b-2803dd8546c6

📥 Commits

Reviewing files that changed from the base of the PR and between e508d64 and 734d27c.

📒 Files selected for processing (4)
  • CHANGELOG.md
  • README.md
  • docs/execplans/advanced-encapsulation-and-verification.md
  • docs/users-guide.md

Comment thread docs/users-guide.md Outdated
Introduce skills/proptest/ as a third verification deep dive alongside
kani and verus. The skill covers strategy design with prop_compose!,
the filtering trap and its compositional fix, ProptestConfig knobs,
regression-file discipline, the proptest-derive vs test-strategy
choice, and proptest-state-machine. References hold the installation
note (Cargo dev-dependency rather than rust-prover-tools), worked
strategy patterns, and a self-contained Rust example.

Routing is updated in rust-router, the routing-matrix, rust-verification,
and tool-selection so the verification skill routes into all three
deep dives. The catalogue-status doc, users' guide, README, and
CHANGELOG mention proptest and distinguish its Cargo install from the
prover-tools install used by kani and verus. The execplan records the
new Stage F, extends the deep-dive tolerance exception to cover the
third deep dive, and notes the lint stumbles encountered during the
write.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 10

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (8)
docs/execplans/advanced-encapsulation-and-verification.md (8)

113-151: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Rewrite imperative escalation triggers as conditional clauses.

The Tolerances section uses 2nd person imperatives:

  • Line 115: "Stop and escalate if" → "Work must stop and be escalated if"
  • Line 138: "present the options before committing" → "the options must be presented before committing"
  • Line 141: "If so, prefer linking" → "If so, linking should be preferred"

Rewrite escalation triggers using modal auxiliaries rather than direct commands.

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 113 -
151, The Tolerances section uses 2nd-person imperatives; rewrite those
escalation triggers to use modal auxiliaries and passive/neutral phrasing—for
example change "Stop and escalate if" to "Work must stop and be escalated if",
"present the options before committing" to "the options must be presented before
committing", and "If so, prefer linking" to "If so, linking should be
preferred"; update the headings/lines inside the "Tolerances (exception
triggers)" block so all imperative sentences are converted to equivalent modal
forms and ensure phrasing remains consistent with the project docstyle rule
against 1st/2nd person pronouns.

408-411: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Rewrite imperative as passive instruction.

Line 410: "Record significant decisions inline" uses 2nd person imperative. Rewrite as: "Significant decisions are recorded inline with the format used in the prior execplan."

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 408 -
411, In the "## Decision Log" section replace the imperative sentence "Record
significant decisions inline with the format used in the prior execplan
(numbered list with rationale)." with a passive construction such as
"Significant decisions are recorded inline with the format used in the prior
execplan (numbered list with rationale)." to comply with the docstyle rule
avoiding 2nd person; update the line that currently begins "Record significant
decisions inline..." accordingly.

236-287: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Rewrite stage descriptions as infinitive or gerund phrases.

The Progress section uses 2nd person imperatives in stage descriptions:

  • Line 238: "Draft this ExecPlan and obtain user approval" → "Drafting the ExecPlan and obtaining user approval" or "Draft the ExecPlan..."
  • Line 242: "confirm tool names" → "confirming tool names" or "Tool names confirmed"

Also eliminate 1st person pronouns:

  • Line 238: "this ExecPlan" → "the ExecPlan"

Rewrite stage descriptions consistently as either gerund phrases (progress tracking) or completed passive statements (for done items).

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 236 -
287, Update the Progress stage descriptions in
docs/execplans/advanced-encapsulation-and-verification.md to use either gerund
phrases or infinitive phrasing and remove all 1st/2nd-person pronouns;
specifically edit the Stage lines (Stage 0, Stage A, Stage A.5, Stage B, Stage
C, Stage D, Stage E, Stage F) so phrases like "Draft this ExecPlan and obtain
user approval" become "Drafting the ExecPlan and obtaining user approval" (or
"Draft the ExecPlan and obtain user approval") and "confirm tool names" becomes
"confirming tool names" or "Tool names confirmed", ensuring consistent
tense/voice across all checked items and replacing occurrences of "this
ExecPlan", "we", or "you" with neutral nouns like "the ExecPlan" or
passive/gerund constructions.

292-297: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Rewrite imperative as passive instruction.

Line 293: "Record discoveries here as work proceeds" uses 2nd person imperative. Rewrite as: "Discoveries are recorded here as work proceeds."

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 292 -
297, In the "## Surprises & Discoveries" section update the sentence "Record
discoveries here as work proceeds." to passive voice—replace it with
"Discoveries are recorded here as work proceeds." so the document conforms to
the markdown guideline avoiding 2nd person; locate the sentence under the "##
Surprises & Discoveries" header and make the one-line substitution.

3-6: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Replace 1st person pronoun with neutral description.

Line 3: "This ExecPlan" uses 1st person pronoun. Rewrite as: "The ExecPlan (execution plan) is a living document."

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 3 -
6, Replace the first-person/demonstrative phrasing in the document header by
changing the sentence "This ExecPlan (execution plan) is a living document." to
a neutral description—use "The ExecPlan (execution plan) is a living document."
Update the content where the phrase occurs (look for the exact string "This
ExecPlan (execution plan) is a living document.") to conform to the repo
docstyle rule against 1st/2nd person pronouns.

523-947: ⚠️ Potential issue | 🟠 Major | 🏗️ Heavy lift

Systemic 2nd person imperative usage throughout operational sections.

The Plan of work section (lines 523-947) contains hundreds of 2nd person imperatives:

  • Line 530: "Confirm canonical names"
  • Line 561: "Add a brief reference pointer"
  • Line 604: "Copy the upstream skills"
  • Line 692: "Default choices"
  • Line 772: "Create CHANGELOG.md"
  • Line 899: "Execute each stage"

The entire operational plan uses imperative mood throughout stage descriptions, concrete steps, and validation instructions. Whilst the execplan genre is inherently procedural, the coding guidelines make no exception for operational documents. The entire section requires rewriting as either:

  1. Modal obligations: "Canonical names must be confirmed", "A brief reference pointer should be added"
  2. Infinitive phrases: "Confirming canonical names", "Adding a brief reference pointer"
  3. Passive instructions: "Canonical names are confirmed", "A brief reference pointer is added"

Given the scale, prioritise rewriting the most user-facing sections (Constraints, Tolerances, Risks) first, then address the internal operational content.

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 523 -
947, The Plan of work section uses pervasive 2nd-person imperatives (e.g.,
"Confirm canonical names", "Add a brief reference pointer", "Copy the upstream
skills", "Create CHANGELOG.md", "Execute each stage"); rewrite these operational
sentences into the approved style by converting imperative verbs in headings and
step lists across Stage 0, Stage A (and substeps), Stage A.5, Stage B, Stage C,
Stage D, Stage E, and the "Concrete steps" block into modal obligations
("must"/"should"), infinitive phrases ("Confirming canonical names", "Adding a
brief reference pointer"), or passive constructions ("Canonical names are to be
confirmed"), prioritizing user-facing sections named Constraints, Tolerances,
and Risks first, and apply the same voice changes consistently to validation and
command examples so the document no longer addresses the reader as "you" or uses
1st/2nd-person pronouns.

67-111: ⚠️ Potential issue | 🟠 Major | 🏗️ Heavy lift

Rewrite imperative constraints as modal obligations.

The Constraints section contains numerous 2nd person imperatives:

  • Line 76: "Keep every newly authored" → "Every newly authored... must be kept short"
  • Line 100: "Use English only. Do not reintroduce" → "English only must be used. Multilingual trigger catalogues must not be reintroduced"
  • Line 101: "Do not copy verbatim" → "Verbatim copying must not occur"
  • Line 103: "Do not modify" → "The current-skills/ directory must not be modified"
  • Line 111: "Do not start implementation work until the user approves this plan" → "Implementation work must not start until the user approves the plan"

Rewrite all imperative constraints using modal verbs (must/must not/should) in 3rd person.

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 67 -
111, Rewrite the Constraints section to eliminate 2nd-person imperatives and
express each constraint as a 3rd-person modal obligation using "must"/"must
not"/"should" — e.g., change "Keep every newly authored..." to "Every newly
authored compact SKILL.md must be kept short", change "Use English only. Do not
reintroduce multilingual trigger catalogues." to "English only must be used;
multilingual trigger catalogues must not be reintroduced", change "Do not copy
verbatim" to "Verbatim copying must not occur", change "Do not modify
`current-skills/`" to "The `current-skills/` directory must not be modified",
and change "Do not start implementation work until the user approves this plan"
to "Implementation work must not start until the user approves the plan"; make
analogous modal rewrites for any other imperative lines so the whole Constraints
section consistently uses 3rd-person modal language.

153-228: ⚠️ Potential issue | 🟠 Major | 🏗️ Heavy lift

Rewrite mitigation imperatives as declarative strategies.

The Risks section uses 2nd person imperatives in mitigation statements:

  • Line 159: "write each SKILL.md" → "each SKILL.md should be written"
  • Line 161: "Move worked examples" → "Worked examples should be moved"
  • Line 169: "anchor the decision surface" → "the decision surface should be anchored"
  • Line 178: "extend existing skills" → "existing skills should be extended"

Rewrite all mitigation imperatives using modal recommendations.

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/execplans/advanced-encapsulation-and-verification.md` around lines 153 -
228, The mitigation lines in the Risks section use 2nd-person imperatives;
update every mitigation sentence to a modal recommendation (use "should" or
passive voice) to avoid 2nd-person phrasing. Specifically, replace phrases like
"write each `SKILL.md`" → "each `SKILL.md` should be written", "Move worked
examples" → "Worked examples should be moved", "anchor the decision surface" →
"the decision surface should be anchored", and "extend existing skills" →
"existing skills should be extended", and similarly convert "Only create a new
first-class skill when..." to "A new first-class skill should only be created
when...", "focus on the durable patterns" to "the focus should be on durable
patterns", "keep the new content Rust-flavoured" to "the new content should be
kept Rust-flavoured", and "Stage A.5 begins with a confirmation step..." to
"Stage A.5 should begin with a confirmation step..."; apply this modal style
consistently to all Mitigation bullets in the Risks section.
♻️ Duplicate comments (2)
skills/rust-verification/references/tool-selection.md (1)

39-39: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Remove second-person pronoun from the mutation-testing description.

Rewrite "the report tells you which assertions to strengthen" to neutral voice (e.g., "the report identifies which assertions require strengthening").

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: Avoid 2nd person or 1st person pronouns ('I', 'you', 'we'), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@skills/rust-verification/references/tool-selection.md` at line 39, Change the
second-person phrasing in the mutation-testing sentence by replacing "the report
tells you which assertions to strengthen" with a neutral voice variant such as
"the report identifies which assertions require strengthening"; update the
mutation-testing description so it avoids "you" and matches the docstyle
guideline (search for the exact phrase "the report tells you which assertions to
strengthen" in the mutation-testing section and replace it).
docs/users-guide.md (1)

86-88: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Remove second-person pronouns from the router decision description.

Rewrite "rust-router routes by the concrete problem in front of you, not by the file you happen to be editing" to neutral phrasing (e.g., "rust-router routes by the concrete problem at hand, not by the file currently being edited").

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: Avoid 2nd person or 1st person pronouns ('I', 'you', 'we'), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@docs/users-guide.md` around lines 86 - 88, Replace the second-person phrasing
in the sentence "`rust-router` routes by the concrete problem in front of you,
not by the file you happen to be editing" with neutral wording; update it to
something like "`rust-router` routes by the concrete problem at hand, not by the
file currently being edited" (keep the surrounding sentence and decision table
intact and apply similar neutral phrasing elsewhere in that paragraph to remove
"you"/"your" usage).
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@skills/proptest/references/installation-note.md`:
- Around line 3-117: Rewrite the markdown to remove 1st- and 2nd-person phrasing
by converting instructional sentences to passive/3rd-person voice: e.g. change
"Stick with `proptest` plus one of the derive crates by default" to "Projects
should use `proptest` plus one of the derive crates by default", "Pick a small
set explicitly" to "A small set should be chosen explicitly", "Raise it for
nightly runs; do not lower it to hide a flake" to "The value may be raised for
nightly runs but must not be lowered to hide a flake", "This note does not
install" to "Installation beyond the provided `Cargo.toml` snippet is not
covered", and "load [`../rust-verification/SKILL.md`]" to "See
[`../rust-verification/SKILL.md`]"; apply the same conversion wherever pronouns
or imperatives appear (notably around the headings "Crates and what they are
for", "Feature flags worth knowing", "Environment variables", and the example
bash block) so the entire file complies with the `**/*.md` docstyle rule.

In `@skills/proptest/references/strategy-examples.md`:
- Around line 51-56: The sentence "Construct only valid values from the seed
instead." in the section titled "The filtering trap: before and after" should be
rewritten to avoid 2nd person imperative; replace it with "Only valid values
should be constructed from the seed instead." so the line uses passive voice and
complies with the docstyle rule for Markdown files.
- Around line 102-104: Change the imperative phrasing "Note the second `Just(b)`
— `prop_compose!` rebinds `b`..." to a declarative sentence: replace it with
something like "The second `Just(b)` is necessary because `prop_compose!`
rebinds `b` in the second clause from the strategy expression, so it must be
passed through explicitly," ensuring the sentence mentions `Just(b)` and
`prop_compose!` exactly as identifiers and removes second-person voice.
- Around line 3-7: Replace the 2nd-person imperative sentence "The names are
deliberately generic — adapt them to the production module being tested." with a
3rd-person phrasing, e.g. "The names are deliberately generic and should be
adapted to the production module under test," so the document avoids 2nd-person
voice and follows the project's Markdown style guidelines.

In `@skills/proptest/SKILL.md`:
- Around line 104-112: Change the imperative sentences on lines referencing
prop_filter and prop_assume! to passive, declarative recommendations: rephrase
"Replace a `prop_filter` that keeps even numbers with a strategy that draws half
the range and doubles it; replace a `prop_assume!` that demands `a < b` with a
strategy that draws `b` then draws `a` from `0..b`" into passive form like "A
`prop_filter` that keeps even numbers should be replaced with a strategy that
draws half the range and doubles it; a `prop_assume!` that demands `a < b`
should be replaced with a strategy that draws `b` then draws `a` from `0..b`,"
and keep the reference to `references/strategy-examples.md` intact.
- Around line 8-12: Rewrite the imperatives and pronouns in the SKILL.md
description to third-person declarative form: replace "Load the
`rust-verification` skill first for the selection rules; load this skill once
proptest is the chosen tool." with "The `rust-verification` skill should be
loaded first for the selection rules; the `proptest` skill should be loaded once
proptest is the chosen tool." Ensure the rest of the paragraph remains unchanged
and uses no 1st/2nd-person pronouns.
- Around line 113-133: In the "Anti-patterns" section rewrite all second-person
imperative phrasing into passive/modal forms: replace "Use `prop_assert*`" with
"The `prop_assert*` family should be used", "Pair it with a real property" with
"It should be paired with a real property", "Use a structurally different
oracle" with "A structurally different oracle should be used", and "Investigate;
do not lower the case count." with "Investigation is required; the case count
must not be lowered"; ensure all other similar imperatives in the same list
follow the same passive/modal style while preserving meaning and punctuation.
- Around line 147-160: Update the "Project integration" section to eliminate
2nd-person imperative phrasing and replace each bullet with a declarative or
passive/modal recommendation: change "Check `proptest-regressions/` into version
control" to "The `proptest-regressions/` directory should be checked into
version control", "Promote shrunk failures to named unit tests" to "Shrunk
failures should be promoted to named unit tests", "Tier the runs. Keep the
default `cases = 256`..." to "Runs should be tiered. The default should be kept
at `cases = 256` for `cargo test`, with a nightly job using
`PROPTEST_CASES=10000`", and "Validate every property with a deliberate
mutation. Break the production code, confirm the property fails..., then
restore." to "Every property should be validated with a deliberate mutation: the
production code can be temporarily altered to confirm the property fails with a
useful shrunk input, then restored; `cargo-mutants` may be used to automate
this." Ensure all bullets in the "Project integration" section use passive/modal
constructions and avoid 1st/2nd person pronouns.
- Around line 190-206: In the "Hard-won lessons" bulleted section under the
"Hard-won lessons" header in SKILL.md, remove 2nd-person and imperative
phrasing: change "what you test" to "what is tested"; rephrase the imperatives
"Never panic or `unwrap` inside the body; never tune `cases` to hide a failure;
never filter when you can compose" to a passive/third-person version such as
"Panicking or unwrapping inside the body should never occur; `cases` should not
be tuned to hide a failure; filtering should be avoided when composition is
possible"; and change "Pair with `cargo-mutants`." to a third-person form like
"Should be paired with `cargo-mutants`." Ensure all bullet items in this
"Hard-won lessons" list use third-person or passive constructions consistently.
- Around line 14-28: Rename the section heading "When to apply" to
"Applicability" and replace imperative phrases "Apply when" and "Do not apply
when" with declarative statements (e.g., "Proptest is applicable when a pure
function has an algebraic property..." and "Proptest is not applicable when the
property requires exhaustive coverage..."); update the two bullet groups so each
entry starts with a declarative clause and avoids 2nd-person pronouns,
preserving the same examples and tool recommendations (Kani, Verus,
loom/shuttle/turmoil, Miri) and overall meaning.

---

Outside diff comments:
In `@docs/execplans/advanced-encapsulation-and-verification.md`:
- Around line 113-151: The Tolerances section uses 2nd-person imperatives;
rewrite those escalation triggers to use modal auxiliaries and passive/neutral
phrasing—for example change "Stop and escalate if" to "Work must stop and be
escalated if", "present the options before committing" to "the options must be
presented before committing", and "If so, prefer linking" to "If so, linking
should be preferred"; update the headings/lines inside the "Tolerances
(exception triggers)" block so all imperative sentences are converted to
equivalent modal forms and ensure phrasing remains consistent with the project
docstyle rule against 1st/2nd person pronouns.
- Around line 408-411: In the "## Decision Log" section replace the imperative
sentence "Record significant decisions inline with the format used in the prior
execplan (numbered list with rationale)." with a passive construction such as
"Significant decisions are recorded inline with the format used in the prior
execplan (numbered list with rationale)." to comply with the docstyle rule
avoiding 2nd person; update the line that currently begins "Record significant
decisions inline..." accordingly.
- Around line 236-287: Update the Progress stage descriptions in
docs/execplans/advanced-encapsulation-and-verification.md to use either gerund
phrases or infinitive phrasing and remove all 1st/2nd-person pronouns;
specifically edit the Stage lines (Stage 0, Stage A, Stage A.5, Stage B, Stage
C, Stage D, Stage E, Stage F) so phrases like "Draft this ExecPlan and obtain
user approval" become "Drafting the ExecPlan and obtaining user approval" (or
"Draft the ExecPlan and obtain user approval") and "confirm tool names" becomes
"confirming tool names" or "Tool names confirmed", ensuring consistent
tense/voice across all checked items and replacing occurrences of "this
ExecPlan", "we", or "you" with neutral nouns like "the ExecPlan" or
passive/gerund constructions.
- Around line 292-297: In the "## Surprises & Discoveries" section update the
sentence "Record discoveries here as work proceeds." to passive voice—replace it
with "Discoveries are recorded here as work proceeds." so the document conforms
to the markdown guideline avoiding 2nd person; locate the sentence under the "##
Surprises & Discoveries" header and make the one-line substitution.
- Around line 3-6: Replace the first-person/demonstrative phrasing in the
document header by changing the sentence "This ExecPlan (execution plan) is a
living document." to a neutral description—use "The ExecPlan (execution plan) is
a living document." Update the content where the phrase occurs (look for the
exact string "This ExecPlan (execution plan) is a living document.") to conform
to the repo docstyle rule against 1st/2nd person pronouns.
- Around line 523-947: The Plan of work section uses pervasive 2nd-person
imperatives (e.g., "Confirm canonical names", "Add a brief reference pointer",
"Copy the upstream skills", "Create CHANGELOG.md", "Execute each stage");
rewrite these operational sentences into the approved style by converting
imperative verbs in headings and step lists across Stage 0, Stage A (and
substeps), Stage A.5, Stage B, Stage C, Stage D, Stage E, and the "Concrete
steps" block into modal obligations ("must"/"should"), infinitive phrases
("Confirming canonical names", "Adding a brief reference pointer"), or passive
constructions ("Canonical names are to be confirmed"), prioritizing user-facing
sections named Constraints, Tolerances, and Risks first, and apply the same
voice changes consistently to validation and command examples so the document no
longer addresses the reader as "you" or uses 1st/2nd-person pronouns.
- Around line 67-111: Rewrite the Constraints section to eliminate 2nd-person
imperatives and express each constraint as a 3rd-person modal obligation using
"must"/"must not"/"should" — e.g., change "Keep every newly authored..." to
"Every newly authored compact SKILL.md must be kept short", change "Use English
only. Do not reintroduce multilingual trigger catalogues." to "English only must
be used; multilingual trigger catalogues must not be reintroduced", change "Do
not copy verbatim" to "Verbatim copying must not occur", change "Do not modify
`current-skills/`" to "The `current-skills/` directory must not be modified",
and change "Do not start implementation work until the user approves this plan"
to "Implementation work must not start until the user approves the plan"; make
analogous modal rewrites for any other imperative lines so the whole Constraints
section consistently uses 3rd-person modal language.
- Around line 153-228: The mitigation lines in the Risks section use 2nd-person
imperatives; update every mitigation sentence to a modal recommendation (use
"should" or passive voice) to avoid 2nd-person phrasing. Specifically, replace
phrases like "write each `SKILL.md`" → "each `SKILL.md` should be written",
"Move worked examples" → "Worked examples should be moved", "anchor the decision
surface" → "the decision surface should be anchored", and "extend existing
skills" → "existing skills should be extended", and similarly convert "Only
create a new first-class skill when..." to "A new first-class skill should only
be created when...", "focus on the durable patterns" to "the focus should be on
durable patterns", "keep the new content Rust-flavoured" to "the new content
should be kept Rust-flavoured", and "Stage A.5 begins with a confirmation
step..." to "Stage A.5 should begin with a confirmation step..."; apply this
modal style consistently to all Mitigation bullets in the Risks section.

---

Duplicate comments:
In `@docs/users-guide.md`:
- Around line 86-88: Replace the second-person phrasing in the sentence
"`rust-router` routes by the concrete problem in front of you, not by the file
you happen to be editing" with neutral wording; update it to something like
"`rust-router` routes by the concrete problem at hand, not by the file currently
being edited" (keep the surrounding sentence and decision table intact and apply
similar neutral phrasing elsewhere in that paragraph to remove "you"/"your"
usage).

In `@skills/rust-verification/references/tool-selection.md`:
- Line 39: Change the second-person phrasing in the mutation-testing sentence by
replacing "the report tells you which assertions to strengthen" with a neutral
voice variant such as "the report identifies which assertions require
strengthening"; update the mutation-testing description so it avoids "you" and
matches the docstyle guideline (search for the exact phrase "the report tells
you which assertions to strengthen" in the mutation-testing section and replace
it).
🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 413f48cc-f0ca-47d1-af97-ff1bb71db3f7

📥 Commits

Reviewing files that changed from the base of the PR and between 734d27c and 4b6857b.

📒 Files selected for processing (13)
  • CHANGELOG.md
  • README.md
  • docs/execplans/advanced-encapsulation-and-verification.md
  • docs/skill-catalogue-status.md
  • docs/users-guide.md
  • skills/proptest/SKILL.md
  • skills/proptest/references/installation-note.md
  • skills/proptest/references/proptest-example.rs
  • skills/proptest/references/strategy-examples.md
  • skills/rust-router/SKILL.md
  • skills/rust-router/references/routing-matrix.md
  • skills/rust-verification/SKILL.md
  • skills/rust-verification/references/tool-selection.md

Comment thread skills/proptest/references/installation-note.md
Comment on lines +3 to +7
Five worked patterns that come up in almost every property suite:
the round-trip over a composed struct, the filtering-trap fix, the
oracle comparison, a field-dependent strategy via `test-strategy`,
and a `ReferenceStateMachine` sketch. The names are deliberately
generic — adapt them to the production module being tested.

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Rewrite the imperative instruction in 3rd person.

Line 7 uses 2nd person imperative ("adapt them to the production module being tested"). Rewrite as 3rd person, for example: "The names are deliberately generic and should be adapted to the production module under test."

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@skills/proptest/references/strategy-examples.md` around lines 3 - 7, Replace
the 2nd-person imperative sentence "The names are deliberately generic — adapt
them to the production module being tested." with a 3rd-person phrasing, e.g.
"The names are deliberately generic and should be adapted to the production
module under test," so the document avoids 2nd-person voice and follows the
project's Markdown style guidelines.

Comment on lines +51 to +56
## The filtering trap: before and after

Filtering invalid inputs out hurts both runtime (rejection budget)
and shrinking (the runner cannot tell rejection from success).
Construct only valid values from the seed instead.

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Rewrite imperative as passive voice.

Line 56: "Construct only valid values from the seed instead" uses 2nd person imperative. Rewrite as: "Only valid values should be constructed from the seed instead."

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@skills/proptest/references/strategy-examples.md` around lines 51 - 56, The
sentence "Construct only valid values from the seed instead." in the section
titled "The filtering trap: before and after" should be rewritten to avoid 2nd
person imperative; replace it with "Only valid values should be constructed from
the seed instead." so the line uses passive voice and complies with the docstyle
rule for Markdown files.

Comment on lines +102 to +104
Note the second `Just(b)` — `prop_compose!` rebinds `b` in the
second clause from the strategy expression, so it has to be passed
through explicitly.

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Rewrite imperative as declarative statement.

Line 102: "Note the second Just(b)" uses 2nd person imperative. Rewrite as: "The second Just(b) is necessary because prop_compose! rebinds b in the second clause..."

Triage: [type:docstyle]

As per coding guidelines: "**/*.md: - Avoid 2nd person or 1st person pronouns ("I", "you", "we"), exceptions: README.md, BDD .feature files."

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@skills/proptest/references/strategy-examples.md` around lines 102 - 104,
Change the imperative phrasing "Note the second `Just(b)` — `prop_compose!`
rebinds `b`..." to a declarative sentence: replace it with something like "The
second `Just(b)` is necessary because `prop_compose!` rebinds `b` in the second
clause from the strategy expression, so it must be passed through explicitly,"
ensuring the sentence mentions `Just(b)` and `prop_compose!` exactly as
identifiers and removes second-person voice.

Comment thread skills/proptest/SKILL.md
Comment thread skills/proptest/SKILL.md
Comment thread skills/proptest/SKILL.md
Comment thread skills/proptest/SKILL.md
Comment thread skills/proptest/SKILL.md
Comment thread skills/proptest/SKILL.md
Reword "in front of you, not by the file you happen to be editing" to
neutral "at hand, not by the file being edited" in the "How the router
decides" section, per docstyle rules that bar 2nd-person pronouns in
documentation.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant