# CompPoly AI Agent Guide

Lean 4 library for formally verified computable polynomial operations over rings and
finite fields. Start with [`README.md`](README.md) for the public project overview.

`AGENTS.md` is the canonical root guide for AI agents and agent-oriented tooling.
Human contributors should usually start with [`README.md`](README.md),
[`CONTRIBUTING.md`](CONTRIBUTING.md), and [`docs/wiki/README.md`](docs/wiki/README.md).
`CLAUDE.md` is a symlink to this file.

## Fast Start

1. Run `lake build` for routine validation.
2. Run `lake test` when changing proofs, public APIs, or regression tests.
3. If you add, rename, or delete files under `CompPoly/`, run
   `./scripts/update-lib.sh` and then `./scripts/check-imports.sh`.
4. Use `./scripts/lint-style.sh` when touching Lean style-sensitive files.
5. If you touch repo docs or links, run `python3 ./scripts/check-docs-integrity.py`.

## Where To Work

- `CompPoly/Univariate/` - canonical univariate representation, quotient model,
  interpolation, and Mathlib bridges.
- `CompPoly/Multivariate/` - sparse computable multivariate polynomials,
  operations, renaming, restriction, and `MvPolynomial` equivalences.
- `CompPoly/Multilinear/` - coefficient and Boolean-hypercube evaluation forms for
  multilinear polynomials.
- `CompPoly/Bivariate/` - specialized bivariate layer built from nested
  univariate polynomials.
- `CompPoly/Fields/` - concrete field instances plus binary-field, GHASH, and
  additive-NTT infrastructure.
- `CompPoly/Data/` - reusable supporting lemmas and helper definitions.
- `CompPoly/ToMathlib/` - local bridge lemmas and Mathlib-facing support code.
- `tests/` - regression coverage under the `CompPolyTests` namespace.
- `scripts/` - repo utilities for import maintenance, linting, and CI support.

## Guardrails

- `CompPoly.lean` is generated by `./scripts/update-lib.sh`; do not hand-edit it.
- Edit source, not derived output under `.lake/`.
- If a PR changes commands, repo structure, generated outputs, or recurring repo
  guidance, update the matching page in [`docs/wiki/`](docs/wiki/README.md) in the
  same PR.
- Promote stable repo-specific guidance into [`docs/wiki/`](docs/wiki/README.md)
  instead of leaving it only in transient notes.

## Deeper Docs

- [`docs/wiki/README.md`](docs/wiki/README.md) - wiki hub and maintenance contract.
- [`docs/wiki/quickstart.md`](docs/wiki/quickstart.md) - validation commands and CI
  mapping.
- [`docs/wiki/repo-map.md`](docs/wiki/repo-map.md) - subtree map and task routing.
- [`docs/wiki/generated-files.md`](docs/wiki/generated-files.md) - source-of-truth
  rules for generated or derived outputs.
- [`docs/wiki/representations-and-bridges.md`](docs/wiki/representations-and-bridges.md)
  - main polynomial representations and Mathlib bridge layers.
- [`docs/wiki/typeclass-minimization.md`](docs/wiki/typeclass-minimization.md) -
  minimal typeclass assumptions and no-blanket-scope guidance.
- [`docs/wiki/binary-fields-and-ntt.md`](docs/wiki/binary-fields-and-ntt.md) -
  binary-field stack, GHASH, and additive NTT.

## Canonical Project Docs

- [`README.md`](README.md) - project overview and main exported surfaces.
- [`CONTRIBUTING.md`](CONTRIBUTING.md) - contribution process, naming, style,
  docstrings, and citations.
- [`ROADMAP.md`](ROADMAP.md) - planned directions and current phase priorities.
- [`tests/README.md`](tests/README.md) - test layout and test commands.
- [`scripts/README.md`](scripts/README.md) - script inventory and operator notes.

## Trusted Code Base (TCB) Policy

**`native_decide` is forbidden.** The project must not depend on `Lean.ofReduceBool`.
All proofs must be kernel-safe, verifiable by Lean's type-checker alone without
trusting the compiler.

- Use `decide` for decidable propositions.
- For expensive kernel computations such as BitVec arithmetic, use `Nat`-based
  structural recursion instead of `Finset.fold` over `BitVec`; see the `clMulNat`
  pattern in `CompPoly/Fields/Binary/BF128Ghash/Prelude.lean`.
- If `decide` is too slow, restructure the proposition, for example by batching
  checks into a single conjunction, rather than reaching for `native_decide`.

## Performance Guidelines

### Typeclass instances

- **Never** put `@[simp]` on `instance` declarations. Instances are found by
  typeclass synthesis, not `simp`. Marking them `@[simp]` registers equation lemmas
  that cause `simp` to unfold typeclass internals and balloon unification work.
- Prefer explicit instance constructions such as `Field.isDomain` over
  `inferInstance` when the synthesis path is long or ambiguous.
- State the minimal typeclass assumptions for each new `def`, `instance`,
  `lemma`, and `theorem`. Avoid blanket section-level `variable [...]`
  declarations unless every declaration in scope genuinely needs them; see
  [`docs/wiki/typeclass-minimization.md`](docs/wiki/typeclass-minimization.md).

### Tactics

- Prefer `simp only [...]` over bare `simp`; bare `simp` pulls in the full simp set.
- Avoid `grind` when a simpler tactic suffices, such as `omega`, `ring`,
  `simp only`, or `exact`. `grind` generates large proof terms via
  saturation-based reasoning.
- Use `decide` sparingly on large types; each `decide` must be kernel-evaluated.

### Certificate / computational proofs

- For proofs that reduce large arithmetic in the kernel, for example modular
  squaring certificates over finite fields, define kernel-efficient checkers using
  `Nat` primitives such as `Nat.testBit`, `Nat.xor`, and `Nat.shiftLeft` with
  structural recursion.
- Prove equivalence to the mathematically clean definition once, then use the fast
  checker in all certificate lemmas.
- Specialize operations where possible. For example, if a polynomial has few
  nonzero coefficients, hardcode the multiplication instead of iterating over all
  bits.

### Imports

- Avoid umbrella imports like `import Mathlib.Tactic`. Import only the specific
  modules you need, for example `Mathlib.Tactic.Ring` and
  `Mathlib.Tactic.Omega`.