AGENTS.md

CompPoly AI Agent Guide

Lean 4 library for formally verified computable polynomial operations over rings and finite fields. Start with 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, CONTRIBUTING.md, and 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/ in the same PR.
• Promote stable repo-specific guidance into docs/wiki/ instead of leaving it only in transient notes.

Deeper Docs

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

Canonical Project Docs

• README.md - project overview and main exported surfaces.
• CONTRIBUTING.md - contribution process, naming, style, docstrings, and citations.
• ROADMAP.md - planned directions and current phase priorities.
• tests/README.md - test layout and test commands.
• 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.

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.