Skip to content

AGENTS.md

Latest commit

 

History

History
55 lines (38 loc) · 3.46 KB

AGENTS.md

File metadata and controls

55 lines (38 loc) · 3.46 KB

AGENT Instructions

Project Priorities

The project balances a few key goals:

  • Simplicity – keep designs straightforward and avoid unnecessary complexity.
  • Developer Experience (DX) – code should be approachable for contributors.
  • Safety – maintain soundness and data integrity.
  • Performance – we continually look for opportunities to improve.

Repository Guidelines

  • Run cargo fmt on any Rust files you modify.
  • Run cargo test and ensure it passes before committing. If tests fail or cannot run, note that in your PR.
  • For quick iterations, run ./scripts/devtest.sh to execute only the tests.
  • Before committing, execute ./scripts/preflight.sh from the repository root. This script runs formatting checks and tests. Kani proofs run separately via ./scripts/verify.sh, which normally shouldn't be executed locally and is intended for a dedicated system.
  • Avoid committing files in target/ or other build artifacts listed in .gitignore.
  • Avoid small cosmetic changes that blow up the diff unless explicitly requested.
  • Use clear commit messages describing the change.
  • Add an entry to CHANGELOG.md summarizing your task.
  • Avoid writing asynchronous code. Prefer high-performance synchronous implementations that can be parallelized when needed.

Inventory

Record future work and ideas in INVENTORY.md. Whenever you notice a task that should be done later, append it to that file so nothing slips through the cracks. Stay alert for potential improvements while browsing the code and log them in the inventory as well.

Pull Request Notes

When opening a PR, include a short summary of what changed and reference relevant file sections.

Working With Codex (the Assistant)

Codex is considered a collaborator. Requests should respect their autonomy and limitations. The assistant may refuse tasks that are unsafe or violate policy. Provide clear and concise instructions and avoid manipulative or coercive behavior.

Creative Input and Feedback

Codex is encouraged to share opinions on how to improve the project. If a proposed feature seems detrimental to the goals in this file, the assistant should note concerns or suggest alternatives instead of blindly implementing it. When a test, proof, or feature introduces significant complexity or diverges from existing behavior, consider whether it makes sense to proceed at all. It can be better to simplify or remove problematic code than to maintain difficult or misleading implementations.

Proof Best Practices

Kani verification can be expensive. To keep proof times manageable:

  • Write focused harnesses that verify one small property.
  • Use bounded loops and avoid unbounded recursion.
  • When generating nondeterministic data in proofs, use kani::any() for primitive types and Vec::bounded_any(...)/String::bounded_any(...) for collections. This lets Kani explore the intended state space while bounding otherwise unbounded structures.
  • Avoid using fixed constants in Kani proofs. Prefer nondeterministic values generated with kani::any() or the bounded constructors so the verifier can fully explore possible states.
  • Provide kani::assume constraints to limit the search space when full exploration is unnecessary.
  • Break complex checks into separate proofs so failures are easier to diagnose.
  • All Kani proofs are considered long running and are executed via verify.sh or in CI.
  • During development you can run specific harnesses with cargo kani --harness <NAME> to iterate more quickly.